InsCode (Divide a,k1,b,k2) = 12 by SCMPDS_2:33;
hence Divide a,k1,b,k2 is shiftable by Def13; :: thesis: verum