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