:: A Small Computer Model with Push-Down Stack :: by JingChao Chen :: :: Received June 15, 1999 :: Copyright (c) 1999-2012 Association of Mizar Users begin theorem :: SCMPDS_1:1 canceled; theorem :: SCMPDS_1:2 canceled; theorem :: SCMPDS_1:3 for d being Element of SCM-Data-Loc holds d in SCM-Data-Loc \/ INT proofend; begin :: [0,goto L] :: [1,return sp<-sp+0,count<-(sp)+2] :: [2,a:=c(constant)] :: [3,saveIC (a,k)] :: [4,if(a,k)<>0 goto L ] :: [5,if(a,k)<=0 goto L ] :: [6,if(a,k)>=0 goto L ] :: [7,(a,k):=c(constant) ] :: [8,(a,k1)+k2] :: [9, (a1,k1)+(a2,k2)] :: [10,(a1,k1)-(a2,k2)] :: [11,(a1,k1)*(a2,k2)] :: [12,(a1,k1)/(a2,k2)] :: [13,(a1,k1):=(a2,k2)] definition canceled; canceled; canceled; canceled; canceled; let s be SCM-State; let a be Element of SCM-Data-Loc ; let n be Integer; func Address_Add (s,a,n) -> Element of SCM-Data-Loc equals :: SCMPDS_1:def 6 [1,(abs ((s . a) + n))]; coherence [1,(abs ((s . a) + n))] is Element of SCM-Data-Loc by AMI_2:24; end; :: deftheorem SCMPDS_1:def_1_:_ canceled; :: deftheorem SCMPDS_1:def_2_:_ canceled; :: deftheorem SCMPDS_1:def_3_:_ canceled; :: deftheorem SCMPDS_1:def_4_:_ canceled; :: deftheorem SCMPDS_1:def_5_:_ canceled; :: deftheorem defines Address_Add SCMPDS_1:def_6_:_ for s being SCM-State for a being Element of SCM-Data-Loc for n being Integer holds Address_Add (s,a,n) = [1,(abs ((s . a) + n))]; definition let s be SCM-State; let n be Integer; func jump_address (s,n) -> Element of NAT equals :: SCMPDS_1:def 7 abs ((IC s) + n); coherence abs ((IC s) + n) is Element of NAT ; end; :: deftheorem defines jump_address SCMPDS_1:def_7_:_ for s being SCM-State for n being Integer holds jump_address (s,n) = abs ((IC s) + n); definition let d be Element of SCM-Data-Loc ; let s be Integer; :: original:<* redefine func<*d,s*> -> FinSequence of SCM-Data-Loc \/ INT; coherence <*d,s*> is FinSequence of SCM-Data-Loc \/ INT proofend; end; definition canceled; canceled; canceled; canceled; canceled; canceled; canceled; canceled; canceled; canceled; canceled; let s be SCM-State; let a be Element of SCM-Data-Loc ; func PopInstrLoc (s,a) -> Element of NAT equals :: SCMPDS_1:def 19 (abs (s . a)) + 2; coherence (abs (s . a)) + 2 is Element of NAT ; end; :: deftheorem SCMPDS_1:def_8_:_ canceled; :: deftheorem SCMPDS_1:def_9_:_ canceled; :: deftheorem SCMPDS_1:def_10_:_ canceled; :: deftheorem SCMPDS_1:def_11_:_ canceled; :: deftheorem SCMPDS_1:def_12_:_ canceled; :: deftheorem SCMPDS_1:def_13_:_ canceled; :: deftheorem SCMPDS_1:def_14_:_ canceled; :: deftheorem SCMPDS_1:def_15_:_ canceled; :: deftheorem SCMPDS_1:def_16_:_ canceled; :: deftheorem SCMPDS_1:def_17_:_ canceled; :: deftheorem SCMPDS_1:def_18_:_ canceled; :: deftheorem defines PopInstrLoc SCMPDS_1:def_19_:_ for s being SCM-State for a being Element of SCM-Data-Loc holds PopInstrLoc (s,a) = (abs (s . a)) + 2; :: RetSP: Return Stack Pointer :: RetIC: Return Instruction-Counter definition canceled; canceled; end; :: deftheorem SCMPDS_1:def_20_:_ canceled; :: deftheorem SCMPDS_1:def_21_:_ canceled; definition let x be Element of SCMPDS-Instr ; let s be SCM-State; func SCM-Exec-Res (x,s) -> SCM-State equals :: SCMPDS_1:def 22 SCM-Chg (s,(jump_address (s,(x const_INT)))) if InsCode x = 14 SCM-Chg ((SCM-Chg (s,(x P21address),(x P22const))),(succ (IC s))) if InsCode x = 2 SCM-Chg ((SCM-Chg (s,(Address_Add (s,(x P21address),(x P22const))),(IC s))),(succ (IC s))) if InsCode x = 3 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))))) if InsCode x = 1 SCM-Chg (s,(IFEQ ((s . (Address_Add (s,(x P31address),(x P32const)))),0,(succ (IC s)),(jump_address (s,(x P33const)))))) if InsCode x = 4 SCM-Chg (s,(IFGT ((s . (Address_Add (s,(x P31address),(x P32const)))),0,(succ (IC s)),(jump_address (s,(x P33const)))))) if InsCode x = 5 SCM-Chg (s,(IFGT (0,(s . (Address_Add (s,(x P31address),(x P32const)))),(succ (IC s)),(jump_address (s,(x P33const)))))) if InsCode x = 6 SCM-Chg ((SCM-Chg (s,(Address_Add (s,(x P31address),(x P32const))),(x P33const))),(succ (IC s))) if InsCode x = 7 SCM-Chg ((SCM-Chg (s,(Address_Add (s,(x P31address),(x P32const))),((s . (Address_Add (s,(x P31address),(x P32const)))) + (x P33const)))),(succ (IC s))) if InsCode x = 8 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))))))),(succ (IC s))) if InsCode x = 9 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))))))),(succ (IC s))) if InsCode x = 10 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))))))),(succ (IC s))) if InsCode x = 11 SCM-Chg ((SCM-Chg (s,(Address_Add (s,(x P41address),(x P43const))),(s . (Address_Add (s,(x P42address),(x P44const)))))),(succ (IC s))) if InsCode x = 13 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))))))),(succ (IC s))) if InsCode x = 12 otherwise s; coherence ( ( InsCode x = 14 implies SCM-Chg (s,(jump_address (s,(x const_INT)))) is SCM-State ) & ( InsCode x = 2 implies SCM-Chg ((SCM-Chg (s,(x P21address),(x P22const))),(succ (IC s))) is SCM-State ) & ( InsCode x = 3 implies SCM-Chg ((SCM-Chg (s,(Address_Add (s,(x P21address),(x P22const))),(IC s))),(succ (IC s))) is SCM-State ) & ( InsCode x = 1 implies 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))))) is SCM-State ) & ( InsCode x = 4 implies SCM-Chg (s,(IFEQ ((s . (Address_Add (s,(x P31address),(x P32const)))),0,(succ (IC s)),(jump_address (s,(x P33const)))))) is SCM-State ) & ( InsCode x = 5 implies SCM-Chg (s,(IFGT ((s . (Address_Add (s,(x P31address),(x P32const)))),0,(succ (IC s)),(jump_address (s,(x P33const)))))) is SCM-State ) & ( InsCode x = 6 implies SCM-Chg (s,(IFGT (0,(s . (Address_Add (s,(x P31address),(x P32const)))),(succ (IC s)),(jump_address (s,(x P33const)))))) is SCM-State ) & ( InsCode x = 7 implies SCM-Chg ((SCM-Chg (s,(Address_Add (s,(x P31address),(x P32const))),(x P33const))),(succ (IC s))) is SCM-State ) & ( InsCode x = 8 implies SCM-Chg ((SCM-Chg (s,(Address_Add (s,(x P31address),(x P32const))),((s . (Address_Add (s,(x P31address),(x P32const)))) + (x P33const)))),(succ (IC s))) is SCM-State ) & ( InsCode x = 9 implies 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))))))),(succ (IC s))) is SCM-State ) & ( InsCode x = 10 implies 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))))))),(succ (IC s))) is SCM-State ) & ( InsCode x = 11 implies 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))))))),(succ (IC s))) is SCM-State ) & ( InsCode x = 13 implies SCM-Chg ((SCM-Chg (s,(Address_Add (s,(x P41address),(x P43const))),(s . (Address_Add (s,(x P42address),(x P44const)))))),(succ (IC s))) is SCM-State ) & ( InsCode x = 12 implies 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))))))),(succ (IC s))) is SCM-State ) & ( 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 s is SCM-State ) ) ; consistency for b1 being SCM-State holds ( ( InsCode x = 14 & InsCode x = 2 implies ( b1 = SCM-Chg (s,(jump_address (s,(x const_INT)))) iff b1 = SCM-Chg ((SCM-Chg (s,(x P21address),(x P22const))),(succ (IC s))) ) ) & ( InsCode x = 14 & InsCode x = 3 implies ( b1 = SCM-Chg (s,(jump_address (s,(x const_INT)))) iff b1 = SCM-Chg ((SCM-Chg (s,(Address_Add (s,(x P21address),(x P22const))),(IC s))),(succ (IC s))) ) ) & ( InsCode x = 14 & InsCode x = 1 implies ( b1 = SCM-Chg (s,(jump_address (s,(x const_INT)))) iff b1 = 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 = 14 & InsCode x = 4 implies ( b1 = SCM-Chg (s,(jump_address (s,(x const_INT)))) iff b1 = SCM-Chg (s,(IFEQ ((s . (Address_Add (s,(x P31address),(x P32const)))),0,(succ (IC s)),(jump_address (s,(x P33const)))))) ) ) & ( InsCode x = 14 & InsCode x = 5 implies ( b1 = SCM-Chg (s,(jump_address (s,(x const_INT)))) iff b1 = SCM-Chg (s,(IFGT ((s . (Address_Add (s,(x P31address),(x P32const)))),0,(succ (IC s)),(jump_address (s,(x P33const)))))) ) ) & ( InsCode x = 14 & InsCode x = 6 implies ( b1 = SCM-Chg (s,(jump_address (s,(x const_INT)))) iff b1 = SCM-Chg (s,(IFGT (0,(s . (Address_Add (s,(x P31address),(x P32const)))),(succ (IC s)),(jump_address (s,(x P33const)))))) ) ) & ( InsCode x = 14 & InsCode x = 7 implies ( b1 = SCM-Chg (s,(jump_address (s,(x const_INT)))) iff b1 = SCM-Chg ((SCM-Chg (s,(Address_Add (s,(x P31address),(x P32const))),(x P33const))),(succ (IC s))) ) ) & ( InsCode x = 14 & InsCode x = 8 implies ( b1 = SCM-Chg (s,(jump_address (s,(x const_INT)))) iff b1 = SCM-Chg ((SCM-Chg (s,(Address_Add (s,(x P31address),(x P32const))),((s . (Address_Add (s,(x P31address),(x P32const)))) + (x P33const)))),(succ (IC s))) ) ) & ( InsCode x = 14 & InsCode x = 9 implies ( b1 = SCM-Chg (s,(jump_address (s,(x const_INT)))) iff b1 = 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))))))),(succ (IC s))) ) ) & ( InsCode x = 14 & InsCode x = 10 implies ( b1 = SCM-Chg (s,(jump_address (s,(x const_INT)))) iff b1 = 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))))))),(succ (IC s))) ) ) & ( InsCode x = 14 & InsCode x = 11 implies ( b1 = SCM-Chg (s,(jump_address (s,(x const_INT)))) iff b1 = 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))))))),(succ (IC s))) ) ) & ( InsCode x = 14 & InsCode x = 13 implies ( b1 = SCM-Chg (s,(jump_address (s,(x const_INT)))) iff b1 = SCM-Chg ((SCM-Chg (s,(Address_Add (s,(x P41address),(x P43const))),(s . (Address_Add (s,(x P42address),(x P44const)))))),(succ (IC s))) ) ) & ( InsCode x = 14 & InsCode x = 12 implies ( b1 = SCM-Chg (s,(jump_address (s,(x const_INT)))) iff b1 = 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))))))),(succ (IC s))) ) ) & ( InsCode x = 2 & InsCode x = 3 implies ( b1 = SCM-Chg ((SCM-Chg (s,(x P21address),(x P22const))),(succ (IC s))) iff b1 = SCM-Chg ((SCM-Chg (s,(Address_Add (s,(x P21address),(x P22const))),(IC s))),(succ (IC s))) ) ) & ( InsCode x = 2 & InsCode x = 1 implies ( b1 = SCM-Chg ((SCM-Chg (s,(x P21address),(x P22const))),(succ (IC s))) iff b1 = 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 = 2 & InsCode x = 4 implies ( b1 = SCM-Chg ((SCM-Chg (s,(x P21address),(x P22const))),(succ (IC s))) iff b1 = SCM-Chg (s,(IFEQ ((s . (Address_Add (s,(x P31address),(x P32const)))),0,(succ (IC s)),(jump_address (s,(x P33const)))))) ) ) & ( InsCode x = 2 & InsCode x = 5 implies ( b1 = SCM-Chg ((SCM-Chg (s,(x P21address),(x P22const))),(succ (IC s))) iff b1 = SCM-Chg (s,(IFGT ((s . (Address_Add (s,(x P31address),(x P32const)))),0,(succ (IC s)),(jump_address (s,(x P33const)))))) ) ) & ( InsCode x = 2 & InsCode x = 6 implies ( b1 = SCM-Chg ((SCM-Chg (s,(x P21address),(x P22const))),(succ (IC s))) iff b1 = SCM-Chg (s,(IFGT (0,(s . (Address_Add (s,(x P31address),(x P32const)))),(succ (IC s)),(jump_address (s,(x P33const)))))) ) ) & ( InsCode x = 2 & InsCode x = 7 implies ( b1 = SCM-Chg ((SCM-Chg (s,(x P21address),(x P22const))),(succ (IC s))) iff b1 = SCM-Chg ((SCM-Chg (s,(Address_Add (s,(x P31address),(x P32const))),(x P33const))),(succ (IC s))) ) ) & ( InsCode x = 2 & InsCode x = 8 implies ( b1 = SCM-Chg ((SCM-Chg (s,(x P21address),(x P22const))),(succ (IC s))) iff b1 = SCM-Chg ((SCM-Chg (s,(Address_Add (s,(x P31address),(x P32const))),((s . (Address_Add (s,(x P31address),(x P32const)))) + (x P33const)))),(succ (IC s))) ) ) & ( InsCode x = 2 & InsCode x = 9 implies ( b1 = SCM-Chg ((SCM-Chg (s,(x P21address),(x P22const))),(succ (IC s))) iff b1 = 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))))))),(succ (IC s))) ) ) & ( InsCode x = 2 & InsCode x = 10 implies ( b1 = SCM-Chg ((SCM-Chg (s,(x P21address),(x P22const))),(succ (IC s))) iff b1 = 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))))))),(succ (IC s))) ) ) & ( InsCode x = 2 & InsCode x = 11 implies ( b1 = SCM-Chg ((SCM-Chg (s,(x P21address),(x P22const))),(succ (IC s))) iff b1 = 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))))))),(succ (IC s))) ) ) & ( InsCode x = 2 & InsCode x = 13 implies ( b1 = SCM-Chg ((SCM-Chg (s,(x P21address),(x P22const))),(succ (IC s))) iff b1 = SCM-Chg ((SCM-Chg (s,(Address_Add (s,(x P41address),(x P43const))),(s . (Address_Add (s,(x P42address),(x P44const)))))),(succ (IC s))) ) ) & ( InsCode x = 2 & InsCode x = 12 implies ( b1 = SCM-Chg ((SCM-Chg (s,(x P21address),(x P22const))),(succ (IC s))) iff b1 = 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))))))),(succ (IC s))) ) ) & ( InsCode x = 3 & InsCode x = 1 implies ( b1 = SCM-Chg ((SCM-Chg (s,(Address_Add (s,(x P21address),(x P22const))),(IC s))),(succ (IC s))) iff b1 = 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 = 3 & InsCode x = 4 implies ( b1 = SCM-Chg ((SCM-Chg (s,(Address_Add (s,(x P21address),(x P22const))),(IC s))),(succ (IC s))) iff b1 = SCM-Chg (s,(IFEQ ((s . (Address_Add (s,(x P31address),(x P32const)))),0,(succ (IC s)),(jump_address (s,(x P33const)))))) ) ) & ( InsCode x = 3 & InsCode x = 5 implies ( b1 = SCM-Chg ((SCM-Chg (s,(Address_Add (s,(x P21address),(x P22const))),(IC s))),(succ (IC s))) iff b1 = SCM-Chg (s,(IFGT ((s . (Address_Add (s,(x P31address),(x P32const)))),0,(succ (IC s)),(jump_address (s,(x P33const)))))) ) ) & ( InsCode x = 3 & InsCode x = 6 implies ( b1 = SCM-Chg ((SCM-Chg (s,(Address_Add (s,(x P21address),(x P22const))),(IC s))),(succ (IC s))) iff b1 = SCM-Chg (s,(IFGT (0,(s . (Address_Add (s,(x P31address),(x P32const)))),(succ (IC s)),(jump_address (s,(x P33const)))))) ) ) & ( InsCode x = 3 & InsCode x = 7 implies ( b1 = SCM-Chg ((SCM-Chg (s,(Address_Add (s,(x P21address),(x P22const))),(IC s))),(succ (IC s))) iff b1 = SCM-Chg ((SCM-Chg (s,(Address_Add (s,(x P31address),(x P32const))),(x P33const))),(succ (IC s))) ) ) & ( InsCode x = 3 & InsCode x = 8 implies ( b1 = SCM-Chg ((SCM-Chg (s,(Address_Add (s,(x P21address),(x P22const))),(IC s))),(succ (IC s))) iff b1 = SCM-Chg ((SCM-Chg (s,(Address_Add (s,(x P31address),(x P32const))),((s . (Address_Add (s,(x P31address),(x P32const)))) + (x P33const)))),(succ (IC s))) ) ) & ( InsCode x = 3 & InsCode x = 9 implies ( b1 = SCM-Chg ((SCM-Chg (s,(Address_Add (s,(x P21address),(x P22const))),(IC s))),(succ (IC s))) iff b1 = 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))))))),(succ (IC s))) ) ) & ( InsCode x = 3 & InsCode x = 10 implies ( b1 = SCM-Chg ((SCM-Chg (s,(Address_Add (s,(x P21address),(x P22const))),(IC s))),(succ (IC s))) iff b1 = 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))))))),(succ (IC s))) ) ) & ( InsCode x = 3 & InsCode x = 11 implies ( b1 = SCM-Chg ((SCM-Chg (s,(Address_Add (s,(x P21address),(x P22const))),(IC s))),(succ (IC s))) iff b1 = 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))))))),(succ (IC s))) ) ) & ( InsCode x = 3 & InsCode x = 13 implies ( b1 = SCM-Chg ((SCM-Chg (s,(Address_Add (s,(x P21address),(x P22const))),(IC s))),(succ (IC s))) iff b1 = SCM-Chg ((SCM-Chg (s,(Address_Add (s,(x P41address),(x P43const))),(s . (Address_Add (s,(x P42address),(x P44const)))))),(succ (IC s))) ) ) & ( InsCode x = 3 & InsCode x = 12 implies ( b1 = SCM-Chg ((SCM-Chg (s,(Address_Add (s,(x P21address),(x P22const))),(IC s))),(succ (IC s))) iff b1 = 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))))))),(succ (IC s))) ) ) & ( InsCode x = 1 & InsCode x = 4 implies ( b1 = 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))))) iff b1 = SCM-Chg (s,(IFEQ ((s . (Address_Add (s,(x P31address),(x P32const)))),0,(succ (IC s)),(jump_address (s,(x P33const)))))) ) ) & ( InsCode x = 1 & InsCode x = 5 implies ( b1 = 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))))) iff b1 = SCM-Chg (s,(IFGT ((s . (Address_Add (s,(x P31address),(x P32const)))),0,(succ (IC s)),(jump_address (s,(x P33const)))))) ) ) & ( InsCode x = 1 & InsCode x = 6 implies ( b1 = 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))))) iff b1 = SCM-Chg (s,(IFGT (0,(s . (Address_Add (s,(x P31address),(x P32const)))),(succ (IC s)),(jump_address (s,(x P33const)))))) ) ) & ( InsCode x = 1 & InsCode x = 7 implies ( b1 = 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))))) iff b1 = SCM-Chg ((SCM-Chg (s,(Address_Add (s,(x P31address),(x P32const))),(x P33const))),(succ (IC s))) ) ) & ( InsCode x = 1 & InsCode x = 8 implies ( b1 = 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))))) iff b1 = SCM-Chg ((SCM-Chg (s,(Address_Add (s,(x P31address),(x P32const))),((s . (Address_Add (s,(x P31address),(x P32const)))) + (x P33const)))),(succ (IC s))) ) ) & ( InsCode x = 1 & InsCode x = 9 implies ( b1 = 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))))) iff b1 = 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))))))),(succ (IC s))) ) ) & ( InsCode x = 1 & InsCode x = 10 implies ( b1 = 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))))) iff b1 = 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))))))),(succ (IC s))) ) ) & ( InsCode x = 1 & InsCode x = 11 implies ( b1 = 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))))) iff b1 = 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))))))),(succ (IC s))) ) ) & ( InsCode x = 1 & InsCode x = 13 implies ( b1 = 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))))) iff b1 = SCM-Chg ((SCM-Chg (s,(Address_Add (s,(x P41address),(x P43const))),(s . (Address_Add (s,(x P42address),(x P44const)))))),(succ (IC s))) ) ) & ( InsCode x = 1 & InsCode x = 12 implies ( b1 = 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))))) iff b1 = 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))))))),(succ (IC s))) ) ) & ( InsCode x = 4 & InsCode x = 5 implies ( b1 = SCM-Chg (s,(IFEQ ((s . (Address_Add (s,(x P31address),(x P32const)))),0,(succ (IC s)),(jump_address (s,(x P33const)))))) iff b1 = SCM-Chg (s,(IFGT ((s . (Address_Add (s,(x P31address),(x P32const)))),0,(succ (IC s)),(jump_address (s,(x P33const)))))) ) ) & ( InsCode x = 4 & InsCode x = 6 implies ( b1 = SCM-Chg (s,(IFEQ ((s . (Address_Add (s,(x P31address),(x P32const)))),0,(succ (IC s)),(jump_address (s,(x P33const)))))) iff b1 = SCM-Chg (s,(IFGT (0,(s . (Address_Add (s,(x P31address),(x P32const)))),(succ (IC s)),(jump_address (s,(x P33const)))))) ) ) & ( InsCode x = 4 & InsCode x = 7 implies ( b1 = SCM-Chg (s,(IFEQ ((s . (Address_Add (s,(x P31address),(x P32const)))),0,(succ (IC s)),(jump_address (s,(x P33const)))))) iff b1 = SCM-Chg ((SCM-Chg (s,(Address_Add (s,(x P31address),(x P32const))),(x P33const))),(succ (IC s))) ) ) & ( InsCode x = 4 & InsCode x = 8 implies ( b1 = SCM-Chg (s,(IFEQ ((s . (Address_Add (s,(x P31address),(x P32const)))),0,(succ (IC s)),(jump_address (s,(x P33const)))))) iff b1 = SCM-Chg ((SCM-Chg (s,(Address_Add (s,(x P31address),(x P32const))),((s . (Address_Add (s,(x P31address),(x P32const)))) + (x P33const)))),(succ (IC s))) ) ) & ( InsCode x = 4 & InsCode x = 9 implies ( b1 = SCM-Chg (s,(IFEQ ((s . (Address_Add (s,(x P31address),(x P32const)))),0,(succ (IC s)),(jump_address (s,(x P33const)))))) iff b1 = 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))))))),(succ (IC s))) ) ) & ( InsCode x = 4 & InsCode x = 10 implies ( b1 = SCM-Chg (s,(IFEQ ((s . (Address_Add (s,(x P31address),(x P32const)))),0,(succ (IC s)),(jump_address (s,(x P33const)))))) iff b1 = 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))))))),(succ (IC s))) ) ) & ( InsCode x = 4 & InsCode x = 11 implies ( b1 = SCM-Chg (s,(IFEQ ((s . (Address_Add (s,(x P31address),(x P32const)))),0,(succ (IC s)),(jump_address (s,(x P33const)))))) iff b1 = 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))))))),(succ (IC s))) ) ) & ( InsCode x = 4 & InsCode x = 13 implies ( b1 = SCM-Chg (s,(IFEQ ((s . (Address_Add (s,(x P31address),(x P32const)))),0,(succ (IC s)),(jump_address (s,(x P33const)))))) iff b1 = SCM-Chg ((SCM-Chg (s,(Address_Add (s,(x P41address),(x P43const))),(s . (Address_Add (s,(x P42address),(x P44const)))))),(succ (IC s))) ) ) & ( InsCode x = 4 & InsCode x = 12 implies ( b1 = SCM-Chg (s,(IFEQ ((s . (Address_Add (s,(x P31address),(x P32const)))),0,(succ (IC s)),(jump_address (s,(x P33const)))))) iff b1 = 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))))))),(succ (IC s))) ) ) & ( InsCode x = 5 & InsCode x = 6 implies ( b1 = SCM-Chg (s,(IFGT ((s . (Address_Add (s,(x P31address),(x P32const)))),0,(succ (IC s)),(jump_address (s,(x P33const)))))) iff b1 = SCM-Chg (s,(IFGT (0,(s . (Address_Add (s,(x P31address),(x P32const)))),(succ (IC s)),(jump_address (s,(x P33const)))))) ) ) & ( InsCode x = 5 & InsCode x = 7 implies ( b1 = SCM-Chg (s,(IFGT ((s . (Address_Add (s,(x P31address),(x P32const)))),0,(succ (IC s)),(jump_address (s,(x P33const)))))) iff b1 = SCM-Chg ((SCM-Chg (s,(Address_Add (s,(x P31address),(x P32const))),(x P33const))),(succ (IC s))) ) ) & ( InsCode x = 5 & InsCode x = 8 implies ( b1 = SCM-Chg (s,(IFGT ((s . (Address_Add (s,(x P31address),(x P32const)))),0,(succ (IC s)),(jump_address (s,(x P33const)))))) iff b1 = SCM-Chg ((SCM-Chg (s,(Address_Add (s,(x P31address),(x P32const))),((s . (Address_Add (s,(x P31address),(x P32const)))) + (x P33const)))),(succ (IC s))) ) ) & ( InsCode x = 5 & InsCode x = 9 implies ( b1 = SCM-Chg (s,(IFGT ((s . (Address_Add (s,(x P31address),(x P32const)))),0,(succ (IC s)),(jump_address (s,(x P33const)))))) iff b1 = 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))))))),(succ (IC s))) ) ) & ( InsCode x = 5 & InsCode x = 10 implies ( b1 = SCM-Chg (s,(IFGT ((s . (Address_Add (s,(x P31address),(x P32const)))),0,(succ (IC s)),(jump_address (s,(x P33const)))))) iff b1 = 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))))))),(succ (IC s))) ) ) & ( InsCode x = 5 & InsCode x = 11 implies ( b1 = SCM-Chg (s,(IFGT ((s . (Address_Add (s,(x P31address),(x P32const)))),0,(succ (IC s)),(jump_address (s,(x P33const)))))) iff b1 = 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))))))),(succ (IC s))) ) ) & ( InsCode x = 5 & InsCode x = 13 implies ( b1 = SCM-Chg (s,(IFGT ((s . (Address_Add (s,(x P31address),(x P32const)))),0,(succ (IC s)),(jump_address (s,(x P33const)))))) iff b1 = SCM-Chg ((SCM- Chg (s,(Address_Add (s,(x P41address),(x P43const))),(s . (Address_Add (s,(x P42address),(x P44const)))))),(succ (IC s))) ) ) & ( InsCode x = 5 & InsCode x = 12 implies ( b1 = SCM-Chg (s,(IFGT ((s . (Address_Add (s,(x P31address),(x P32const)))),0,(succ (IC s)),(jump_address (s,(x P33const)))))) iff b1 = 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))))))),(succ (IC s))) ) ) & ( InsCode x = 6 & InsCode x = 7 implies ( b1 = SCM-Chg (s,(IFGT (0,(s . (Address_Add (s,(x P31address),(x P32const)))),(succ (IC s)),(jump_address (s,(x P33const)))))) iff b1 = SCM-Chg ((SCM-Chg (s,(Address_Add (s,(x P31address),(x P32const))),(x P33const))),(succ (IC s))) ) ) & ( InsCode x = 6 & InsCode x = 8 implies ( b1 = SCM-Chg (s,(IFGT (0,(s . (Address_Add (s,(x P31address),(x P32const)))),(succ (IC s)),(jump_address (s,(x P33const)))))) iff b1 = SCM-Chg ((SCM-Chg (s,(Address_Add (s,(x P31address),(x P32const))),((s . (Address_Add (s,(x P31address),(x P32const)))) + (x P33const)))),(succ (IC s))) ) ) & ( InsCode x = 6 & InsCode x = 9 implies ( b1 = SCM-Chg (s,(IFGT (0,(s . (Address_Add (s,(x P31address),(x P32const)))),(succ (IC s)),(jump_address (s,(x P33const)))))) iff b1 = 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))))))),(succ (IC s))) ) ) & ( InsCode x = 6 & InsCode x = 10 implies ( b1 = SCM-Chg (s,(IFGT (0,(s . (Address_Add (s,(x P31address),(x P32const)))),(succ (IC s)),(jump_address (s,(x P33const)))))) iff b1 = 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))))))),(succ (IC s))) ) ) & ( InsCode x = 6 & InsCode x = 11 implies ( b1 = SCM-Chg (s,(IFGT (0,(s . (Address_Add (s,(x P31address),(x P32const)))),(succ (IC s)),(jump_address (s,(x P33const)))))) iff b1 = 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))))))),(succ (IC s))) ) ) & ( InsCode x = 6 & InsCode x = 13 implies ( b1 = SCM-Chg (s,(IFGT (0,(s . (Address_Add (s,(x P31address),(x P32const)))),(succ (IC s)),(jump_address (s,(x P33const)))))) iff b1 = SCM-Chg ((SCM-Chg (s,(Address_Add (s,(x P41address),(x P43const))),(s . (Address_Add (s,(x P42address),(x P44const)))))),(succ (IC s))) ) ) & ( InsCode x = 6 & InsCode x = 12 implies ( b1 = SCM-Chg (s,(IFGT (0,(s . (Address_Add (s,(x P31address),(x P32const)))),(succ (IC s)),(jump_address (s,(x P33const)))))) iff b1 = 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))))))),(succ (IC s))) ) ) & ( InsCode x = 7 & InsCode x = 8 implies ( b1 = SCM-Chg ((SCM-Chg (s,(Address_Add (s,(x P31address),(x P32const))),(x P33const))),(succ (IC s))) iff b1 = SCM-Chg ((SCM-Chg (s,(Address_Add (s,(x P31address),(x P32const))),((s . (Address_Add (s,(x P31address),(x P32const)))) + (x P33const)))),(succ (IC s))) ) ) & ( InsCode x = 7 & InsCode x = 9 implies ( b1 = SCM-Chg ((SCM-Chg (s,(Address_Add (s,(x P31address),(x P32const))),(x P33const))),(succ (IC s))) iff b1 = 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))))))),(succ (IC s))) ) ) & ( InsCode x = 7 & InsCode x = 10 implies ( b1 = SCM-Chg ((SCM-Chg (s,(Address_Add (s,(x P31address),(x P32const))),(x P33const))),(succ (IC s))) iff b1 = 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))))))),(succ (IC s))) ) ) & ( InsCode x = 7 & InsCode x = 11 implies ( b1 = SCM-Chg ((SCM-Chg (s,(Address_Add (s,(x P31address),(x P32const))),(x P33const))),(succ (IC s))) iff b1 = 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))))))),(succ (IC s))) ) ) & ( InsCode x = 7 & InsCode x = 13 implies ( b1 = SCM-Chg ((SCM-Chg (s,(Address_Add (s,(x P31address),(x P32const))),(x P33const))),(succ (IC s))) iff b1 = SCM-Chg ((SCM-Chg (s,(Address_Add (s,(x P41address),(x P43const))),(s . (Address_Add (s,(x P42address),(x P44const)))))),(succ (IC s))) ) ) & ( InsCode x = 7 & InsCode x = 12 implies ( b1 = SCM-Chg ((SCM-Chg (s,(Address_Add (s,(x P31address),(x P32const))),(x P33const))),(succ (IC s))) iff b1 = 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))))))),(succ (IC s))) ) ) & ( InsCode x = 8 & InsCode x = 9 implies ( b1 = SCM-Chg ((SCM-Chg (s,(Address_Add (s,(x P31address),(x P32const))),((s . (Address_Add (s,(x P31address),(x P32const)))) + (x P33const)))),(succ (IC s))) iff b1 = 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))))))),(succ (IC s))) ) ) & ( InsCode x = 8 & InsCode x = 10 implies ( b1 = SCM-Chg ((SCM-Chg (s,(Address_Add (s,(x P31address),(x P32const))),((s . (Address_Add (s,(x P31address),(x P32const)))) + (x P33const)))),(succ (IC s))) iff b1 = 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))))))),(succ (IC s))) ) ) & ( InsCode x = 8 & InsCode x = 11 implies ( b1 = SCM-Chg ((SCM-Chg (s,(Address_Add (s,(x P31address),(x P32const))),((s . (Address_Add (s,(x P31address),(x P32const)))) + (x P33const)))),(succ (IC s))) iff b1 = 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))))))),(succ (IC s))) ) ) & ( InsCode x = 8 & InsCode x = 13 implies ( b1 = SCM-Chg ((SCM-Chg (s,(Address_Add (s,(x P31address),(x P32const))),((s . (Address_Add (s,(x P31address),(x P32const)))) + (x P33const)))),(succ (IC s))) iff b1 = SCM-Chg ((SCM-Chg (s,(Address_Add (s,(x P41address),(x P43const))),(s . (Address_Add (s,(x P42address),(x P44const)))))),(succ (IC s))) ) ) & ( InsCode x = 8 & InsCode x = 12 implies ( b1 = SCM-Chg ((SCM-Chg (s,(Address_Add (s,(x P31address),(x P32const))),((s . (Address_Add (s,(x P31address),(x P32const)))) + (x P33const)))),(succ (IC s))) iff b1 = 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))))))),(succ (IC s))) ) ) & ( InsCode x = 9 & InsCode x = 10 implies ( b1 = 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))))))),(succ (IC s))) iff b1 = 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))))))),(succ (IC s))) ) ) & ( InsCode x = 9 & InsCode x = 11 implies ( b1 = 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))))))),(succ (IC s))) iff b1 = 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))))))),(succ (IC s))) ) ) & ( InsCode x = 9 & InsCode x = 13 implies ( b1 = 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))))))),(succ (IC s))) iff b1 = SCM-Chg ((SCM-Chg (s,(Address_Add (s,(x P41address),(x P43const))),(s . (Address_Add (s,(x P42address),(x P44const)))))),(succ (IC s))) ) ) & ( InsCode x = 9 & InsCode x = 12 implies ( b1 = 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))))))),(succ (IC s))) iff b1 = 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))))))),(succ (IC s))) ) ) & ( InsCode x = 10 & InsCode x = 11 implies ( b1 = 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))))))),(succ (IC s))) iff b1 = 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))))))),(succ (IC s))) ) ) & ( InsCode x = 10 & InsCode x = 13 implies ( b1 = 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))))))),(succ (IC s))) iff b1 = SCM-Chg ((SCM-Chg (s,(Address_Add (s,(x P41address),(x P43const))),(s . (Address_Add (s,(x P42address),(x P44const)))))),(succ (IC s))) ) ) & ( InsCode x = 10 & InsCode x = 12 implies ( b1 = 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))))))),(succ (IC s))) iff b1 = 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))))))),(succ (IC s))) ) ) & ( InsCode x = 11 & InsCode x = 13 implies ( b1 = 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))))))),(succ (IC s))) iff b1 = SCM-Chg ((SCM-Chg (s,(Address_Add (s,(x P41address),(x P43const))),(s . (Address_Add (s,(x P42address),(x P44const)))))),(succ (IC s))) ) ) & ( InsCode x = 11 & InsCode x = 12 implies ( b1 = 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))))))),(succ (IC s))) iff b1 = 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))))))),(succ (IC s))) ) ) & ( InsCode x = 13 & InsCode x = 12 implies ( b1 = SCM-Chg ((SCM-Chg (s,(Address_Add (s,(x P41address),(x P43const))),(s . (Address_Add (s,(x P42address),(x P44const)))))),(succ (IC s))) iff b1 = 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))))))),(succ (IC s))) ) ) ) ; end; :: deftheorem defines SCM-Exec-Res SCMPDS_1:def_22_:_ 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))),(succ (IC s))) ) & ( InsCode x = 3 implies SCM-Exec-Res (x,s) = SCM-Chg ((SCM-Chg (s,(Address_Add (s,(x P21address),(x P22const))),(IC s))),(succ (IC s))) ) & ( 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,(succ (IC s)),(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,(succ (IC s)),(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)))),(succ (IC s)),(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))),(succ (IC s))) ) & ( 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)))),(succ (IC s))) ) & ( 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))))))),(succ (IC s))) ) & ( 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))))))),(succ (IC s))) ) & ( 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))))))),(succ (IC s))) ) & ( 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)))))),(succ (IC s))) ) & ( 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))))))),(succ (IC s))) ) & ( 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 ) ); definition func SCMPDS-Exec -> Action of SCMPDS-Instr,(product (SCM-VAL * SCM-OK)) means :: SCMPDS_1:def 23 for x being Element of SCMPDS-Instr for y being SCM-State holds (it . x) . y = SCM-Exec-Res (x,y); existence ex b1 being Action of SCMPDS-Instr,(product (SCM-VAL * SCM-OK)) st for x being Element of SCMPDS-Instr for y being SCM-State holds (b1 . x) . y = SCM-Exec-Res (x,y) proofend; uniqueness for b1, b2 being Action of SCMPDS-Instr,(product (SCM-VAL * SCM-OK)) st ( for x being Element of SCMPDS-Instr for y being SCM-State holds (b1 . x) . y = SCM-Exec-Res (x,y) ) & ( for x being Element of SCMPDS-Instr for y being SCM-State holds (b2 . x) . y = SCM-Exec-Res (x,y) ) holds b1 = b2 proofend; end; :: deftheorem defines SCMPDS-Exec SCMPDS_1:def_23_:_ for b1 being Action of SCMPDS-Instr,(product (SCM-VAL * SCM-OK)) holds ( b1 = SCMPDS-Exec iff for x being Element of SCMPDS-Instr for y being SCM-State holds (b1 . x) . y = SCM-Exec-Res (x,y) );