:: deftheorem defines SCM-Exec-Res SCMPDS_1:def 20 :
for x being Element of SCMPDS-Instr
for s being SCM-State holds
( ( InsCode x = 14 implies SCM-Exec-Res (x,s) = SCM-Chg (s,(jump_address (s,(x const_INT)))) ) & ( InsCode x = 2 implies SCM-Exec-Res (x,s) = SCM-Chg ((SCM-Chg (s,(x P21address),(x P22const))),((IC s) + 1)) ) & ( InsCode x = 3 implies SCM-Exec-Res (x,s) = SCM-Chg ((SCM-Chg (s,(Address_Add (s,(x P21address),(x P22const))),(IC s))),((IC s) + 1)) ) & ( InsCode x = 1 implies SCM-Exec-Res (x,s) = SCM-Chg ((SCM-Chg (s,(x address_1),(s . (Address_Add (s,(x address_1),RetSP))))),(PopInstrLoc (s,(Address_Add (s,(x address_1),RetIC))))) ) & ( InsCode x = 4 implies SCM-Exec-Res (x,s) = SCM-Chg (s,(IFEQ ((s . (Address_Add (s,(x P31address),(x P32const)))),0,((IC s) + 1),(jump_address (s,(x P33const)))))) ) & ( InsCode x = 5 implies SCM-Exec-Res (x,s) = SCM-Chg (s,(IFGT ((s . (Address_Add (s,(x P31address),(x P32const)))),0,((IC s) + 1),(jump_address (s,(x P33const)))))) ) & ( InsCode x = 6 implies SCM-Exec-Res (x,s) = SCM-Chg (s,(IFGT (0,(s . (Address_Add (s,(x P31address),(x P32const)))),((IC s) + 1),(jump_address (s,(x P33const)))))) ) & ( InsCode x = 7 implies SCM-Exec-Res (x,s) = SCM-Chg ((SCM-Chg (s,(Address_Add (s,(x P31address),(x P32const))),(x P33const))),((IC s) + 1)) ) & ( InsCode x = 8 implies SCM-Exec-Res (x,s) = SCM-Chg ((SCM-Chg (s,(Address_Add (s,(x P31address),(x P32const))),((s . (Address_Add (s,(x P31address),(x P32const)))) + (x P33const)))),((IC s) + 1)) ) & ( InsCode x = 9 implies SCM-Exec-Res (x,s) = SCM-Chg ((SCM-Chg (s,(Address_Add (s,(x P41address),(x P43const))),((s . (Address_Add (s,(x P41address),(x P43const)))) + (s . (Address_Add (s,(x P42address),(x P44const))))))),((IC s) + 1)) ) & ( InsCode x = 10 implies SCM-Exec-Res (x,s) = SCM-Chg ((SCM-Chg (s,(Address_Add (s,(x P41address),(x P43const))),((s . (Address_Add (s,(x P41address),(x P43const)))) - (s . (Address_Add (s,(x P42address),(x P44const))))))),((IC s) + 1)) ) & ( InsCode x = 11 implies SCM-Exec-Res (x,s) = SCM-Chg ((SCM-Chg (s,(Address_Add (s,(x P41address),(x P43const))),((s . (Address_Add (s,(x P41address),(x P43const)))) * (s . (Address_Add (s,(x P42address),(x P44const))))))),((IC s) + 1)) ) & ( InsCode x = 13 implies SCM-Exec-Res (x,s) = SCM-Chg ((SCM-Chg (s,(Address_Add (s,(x P41address),(x P43const))),(s . (Address_Add (s,(x P42address),(x P44const)))))),((IC s) + 1)) ) & ( InsCode x = 12 implies SCM-Exec-Res (x,s) = SCM-Chg ((SCM-Chg ((SCM-Chg (s,(Address_Add (s,(x P41address),(x P43const))),((s . (Address_Add (s,(x P41address),(x P43const)))) div (s . (Address_Add (s,(x P42address),(x P44const))))))),(Address_Add (s,(x P42address),(x P44const))),((s . (Address_Add (s,(x P41address),(x P43const)))) mod (s . (Address_Add (s,(x P42address),(x P44const))))))),((IC s) + 1)) ) & ( not InsCode x = 14 & not InsCode x = 2 & not InsCode x = 3 & not InsCode x = 1 & not InsCode x = 4 & not InsCode x = 5 & not InsCode x = 6 & not InsCode x = 7 & not InsCode x = 8 & not InsCode x = 9 & not InsCode x = 10 & not InsCode x = 11 & not InsCode x = 13 & not InsCode x = 12 implies SCM-Exec-Res (x,s) = s ) );