InsCode (a := k1) = 2 by SCMPDS_2:14;
hence a := k1 is shiftable by Def13; :: thesis: verum