:: 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
proof end;

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
proof end;
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)
proof end;
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
proof end;
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) );