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