InsCode (MultBy a,k1,b,k2) = 11 by SCMPDS_2:32;
hence MultBy a,k1,b,k2 is shiftable by Def13; :: thesis: verum