InsCode (AddTo (a,k1,k2)) = 8 by SCMPDS_2:20;
hence AddTo (a,k1,k2) is shiftable by Def13; :: thesis: verum