theorem Th49: :: SCMPDS_2:52

for s being State of SCMPDS
for k1, k2 being Integer
for a, b being Int_position holds
( (Exec ((Divide (a,k1,b,k2)),s)) . (IC ) = (IC s) + 1 & ( DataLoc ((s . a),k1) <> DataLoc ((s . b),k2) implies (Exec ((Divide (a,k1,b,k2)),s)) . (DataLoc ((s . a),k1)) = (s . (DataLoc ((s . a),k1))) div (s . (DataLoc ((s . b),k2))) ) & (Exec ((Divide (a,k1,b,k2)),s)) . (DataLoc ((s . b),k2)) = (s . (DataLoc ((s . a),k1))) mod (s . (DataLoc ((s . b),k2))) & ( for c being Int_position st c <> DataLoc ((s . a),k1) & c <> DataLoc ((s . b),k2) holds
(Exec ((Divide (a,k1,b,k2)),s)) . c = s . c ) )