:: SCMPDS_1 semantic presentation

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
let d be Element of SCM-Data-Loc ; ::_thesis: d in SCM-Data-Loc \/ INT
 SCM-Data-Loc c= SCM-Data-Loc \/ INT by XBOOLE_1:7;
hence  d in SCM-Data-Loc \/ INT by TARSKI:def_3; ::_thesis: verum
end;

begin

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
let y be set ; :: according to TARSKI:def_3,FINSEQ_1:def_4 ::_thesis: ( not y in rng <*d,s*> or y in SCM-Data-Loc \/ INT )
A1: dom <*d,s*> = {1,2} by FINSEQ_1:2, FINSEQ_1:89;
assume  y in rng <*d,s*> ; ::_thesis: y in SCM-Data-Loc \/ INT
then consider x being set  such that
A2: x in dom <*d,s*> and
A3: <*d,s*> . x = y by FUNCT_1:def_3;
percases ( x = 1 or x = 2 ) by A2, A1, TARSKI:def_2;
suppose x = 1 ; ::_thesis: y in SCM-Data-Loc \/ INT
then  y = d by A3, FINSEQ_1:44;
hence  y in SCM-Data-Loc \/ INT by XBOOLE_0:def_3; ::_thesis: verum
end;
supposeA4: x = 2 ; ::_thesis: y in SCM-Data-Loc \/ INT
A5: s in INT by INT_1:def_2;
 y = s by A3, A4, FINSEQ_1:44;
hence  y in SCM-Data-Loc \/ INT by A5, XBOOLE_0:def_3; ::_thesis: verum
end;
end;
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;

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
consider f being Function of [:SCMPDS-Instr,(product (SCM-VAL * SCM-OK)):],(product (SCM-VAL * SCM-OK)) such that
A1: for x being Element of SCMPDS-Instr
for y being SCM-State holds f . (x,y) = SCM-Exec-Res (x,y) from BINOP_1:sch_4();
take  curry f ; ::_thesis: for x being Element of SCMPDS-Instr
for y being SCM-State holds ((curry f) . x) . y = SCM-Exec-Res (x,y)
let x be Element of SCMPDS-Instr ; ::_thesis: for y being SCM-State holds ((curry f) . x) . y = SCM-Exec-Res (x,y)
let y be SCM-State; ::_thesis: ((curry f) . x) . y = SCM-Exec-Res (x,y)
thus ((curry f) . x) . y = f . (x,y) by FUNCT_5:69
.= SCM-Exec-Res (x,y) by A1 ; ::_thesis: verum
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
let f, g be Action of SCMPDS-Instr,(product (SCM-VAL * SCM-OK)); ::_thesis: ( ( for x being Element of SCMPDS-Instr
for y being SCM-State holds (f . x) . y = SCM-Exec-Res (x,y) ) & ( for x being Element of SCMPDS-Instr
for y being SCM-State holds (g . x) . y = SCM-Exec-Res (x,y) ) implies f = g )
assume that
A2: for x being Element of SCMPDS-Instr
for y being SCM-State holds (f . x) . y = SCM-Exec-Res (x,y) and
A3: for x being Element of SCMPDS-Instr
for y being SCM-State holds (g . x) . y = SCM-Exec-Res (x,y) ; ::_thesis: f = g
now__::_thesis:_for_x_being_Element_of_SCMPDS-Instr_holds_f_._x_=_g_._x
let x be Element of SCMPDS-Instr ; ::_thesis: f . x = g . x
reconsider gx = g . x, fx = f . x as Function of (product (SCM-VAL * SCM-OK)),(product (SCM-VAL * SCM-OK)) by FUNCT_2:66;
now__::_thesis:_for_y_being_SCM-State_holds_fx_._y_=_gx_._y
let y be SCM-State; ::_thesis: fx . y = gx . y
thus fx . y = SCM-Exec-Res (x,y) by A2
.= gx . y by A3 ; ::_thesis: verum
end;
hence  f . x = g . x by FUNCT_2:63; ::_thesis: verum
end;
hence  f = g by FUNCT_2:63; ::_thesis: verum
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) );