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