theorem :: SCMPDS_2:38
for ins being Instruction of SCMPDS st InsCode ins = 12 holds
ex a, b being Int_position ex k1, k2 being Integer st ins = Divide (a,k1,b,k2)