InsCode (AddTo a,k1,b,k2) = 9 by SCMPDS_2:30;
hence AddTo a,k1,b,k2 is shiftable by Def13; :: thesis: verum