let s be State of SCMPDS; :: thesis: for i being Instruction of SCMPDS
for l being Element of NAT holds (Exec (i,s)) . l = s . l
let i be Instruction of SCMPDS; :: thesis: for l being Element of NAT holds (Exec (i,s)) . l = s . l
let l be Element of NAT ; :: thesis: (Exec (i,s)) . l = s . l
reconsider c = i as Element of SCMPDS-Instr ;
reconsider S = s as Element of product SCMPDS-OK by PBOOLE:155;
reconsider l9 = l as Element of NAT ;

now

per cases ( c in { [0,{},<*k1*>] where k1 is Element of INT : verum } or c in { [1,{},<*d1*>] where d1 is Element of SCM-Data-Loc : verum } or c in { [I1,{},<*d2,k2*>] where I1 is Element of Segm 14, d2 is Element of SCM-Data-Loc , k2 is Element of INT : I1 in {2,3} } or c in { [I2,{},<*d3,k3,k4*>] where I2 is Element of Segm 14, d3 is Element of SCM-Data-Loc , k3, k4 is Element of INT : I2 in {4,5,6,7,8} } or c in { [I3,{},<*d4,d5,k5,k6*>] where I3 is Element of Segm 14, d4, d5 is Element of SCM-Data-Loc , k5, k6 is Element of INT : I3 in {9,10,11,12,13} } ) by Lm1;

case c in { [0,{},<*k1*>] where k1 is Element of INT : verum } ; :: thesis: (SCM-Exec-Res (c,S)) . l9 = S . l9

then ex k1 being Element of INT st c = [0,{},<*k1*>] ;
hence (SCM-Exec-Res (c,S)) . l9 = (SCM-Chg (S,(jump_address (S,(c const_INT))))) . l9 by SCMPDS_1:def 24
.= S . l9 by SCMPDS_1:28 ;
:: thesis: verum

end;

case A1: c in { [1,{},<*d1*>] where d1 is Element of SCM-Data-Loc : verum } ; :: thesis: (SCM-Exec-Res (c,S)) . l9 = S . l9

set SS = SCM-Chg (S,(c address_1),(S . (Address_Add (S,(c address_1),RetSP))));
ex d1 being Element of SCM-Data-Loc st c = [1,{},<*d1*>] by A1;
hence (SCM-Exec-Res (c,S)) . l9 = (SCM-Chg ((SCM-Chg (S,(c address_1),(S . (Address_Add (S,(c address_1),RetSP))))),(PopInstrLoc (S,(Address_Add (S,(c address_1),RetIC)))))) . l9 by SCMPDS_1:def 24
.= (SCM-Chg (S,(c address_1),(S . (Address_Add (S,(c address_1),RetSP))))) . l9 by SCMPDS_1:28
.= S . l9 by SCMPDS_1:32 ;
:: thesis: verum

end;

case A2: c in { [I1,{},<*d2,k2*>] where I1 is Element of Segm 14, d2 is Element of SCM-Data-Loc , k2 is Element of INT : I1 in {2,3} } ; :: thesis: (SCM-Exec-Res (c,S)) . l9 = S . l9

set SS = SCM-Chg (S,(c P21address),(c P22const));
consider I1 being Element of Segm 14, d1 being Element of SCM-Data-Loc , k1 being Element of INT such that
A3: c = [I1,{},<*d1,k1*>] and
A4: I1 in {2,3} by A2;

now

per cases ( I1 = 2 or I1 = 3 ) by A4, TARSKI:def 2;

case I1 = 2 ; :: thesis: (SCM-Exec-Res (c,S)) . l9 = S . l9

hence (SCM-Exec-Res (c,S)) . l9 = (SCM-Chg ((SCM-Chg (S,(c P21address),(c P22const))),(succ (IC S)))) . l9 by A3, SCMPDS_1:def 24
.= (SCM-Chg (S,(c P21address),(c P22const))) . l9 by SCMPDS_1:28
.= S . l9 by SCMPDS_1:32 ;
:: thesis: verum

end;

case A5: I1 = 3 ; :: thesis: (SCM-Exec-Res (c,S)) . l9 = S . l9

set SS = SCM-Chg (S,(Address_Add (S,(c P21address),(c P22const))),(IC S));
thus (SCM-Exec-Res (c,S)) . l9 = (SCM-Chg ((SCM-Chg (S,(Address_Add (S,(c P21address),(c P22const))),(IC S))),(succ (IC S)))) . l9 by A3, A5, SCMPDS_1:def 24
.= (SCM-Chg (S,(Address_Add (S,(c P21address),(c P22const))),(IC S))) . l9 by SCMPDS_1:28
.= S . l9 by SCMPDS_1:32 ; :: thesis: verum

end;

end;

end;

hence (SCM-Exec-Res (c,S)) . l9 = S . l9 ; :: thesis: verum

end;

case c in { [I2,{},<*d3,k3,k4*>] where I2 is Element of Segm 14, d3 is Element of SCM-Data-Loc , k3, k4 is Element of INT : I2 in {4,5,6,7,8} } ; :: thesis: (SCM-Exec-Res (c,S)) . l9 = S . l9

then consider I1 being Element of Segm 14, d1 being Element of SCM-Data-Loc , k1, k2 being Element of INT such that
A6: c = [I1,{},<*d1,k1,k2*>] and
A7: I1 in {4,5,6,7,8} ;

now

per cases ( I1 = 4 or I1 = 5 or I1 = 6 or I1 = 7 or I1 = 8 ) by A7, ENUMSET1:def 3;

case I1 = 4 ; :: thesis: (SCM-Exec-Res (c,S)) . l9 = S . l9

hence (SCM-Exec-Res (c,S)) . l9 = (SCM-Chg (S,(IFEQ ((S . (Address_Add (S,(c P31address),(c P32const)))),0,(succ (IC S)),(jump_address (S,(c P33const))))))) . l9 by A6, SCMPDS_1:def 24
.= S . l9 by SCMPDS_1:28 ;
:: thesis: verum

end;

case I1 = 5 ; :: thesis: (SCM-Exec-Res (c,S)) . l9 = S . l9

hence (SCM-Exec-Res (c,S)) . l9 = (SCM-Chg (S,(IFGT ((S . (Address_Add (S,(c P31address),(c P32const)))),0,(succ (IC S)),(jump_address (S,(c P33const))))))) . l9 by A6, SCMPDS_1:def 24
.= S . l9 by SCMPDS_1:28 ;
:: thesis: verum

end;

case I1 = 6 ; :: thesis: (SCM-Exec-Res (c,S)) . l9 = S . l9

hence (SCM-Exec-Res (c,S)) . l9 = (SCM-Chg (S,(IFGT (0,(S . (Address_Add (S,(c P31address),(c P32const)))),(succ (IC S)),(jump_address (S,(c P33const))))))) . l9 by A6, SCMPDS_1:def 24
.= S . l9 by SCMPDS_1:28 ;
:: thesis: verum

end;

case A8: I1 = 7 ; :: thesis: (SCM-Exec-Res (c,S)) . l9 = S . l9

set SS = SCM-Chg (S,(Address_Add (S,(c P31address),(c P32const))),(c P33const));
thus (SCM-Exec-Res (c,S)) . l9 = (SCM-Chg ((SCM-Chg (S,(Address_Add (S,(c P31address),(c P32const))),(c P33const))),(succ (IC S)))) . l9 by A6, A8, SCMPDS_1:def 24
.= (SCM-Chg (S,(Address_Add (S,(c P31address),(c P32const))),(c P33const))) . l9 by SCMPDS_1:28
.= S . l9 by SCMPDS_1:32 ; :: thesis: verum

end;

case A9: I1 = 8 ; :: thesis: (SCM-Exec-Res (c,S)) . l9 = S . l9

set SS = SCM-Chg (S,(Address_Add (S,(c P31address),(c P32const))),((S . (Address_Add (S,(c P31address),(c P32const)))) + (c P33const)));
thus (SCM-Exec-Res (c,S)) . l9 = (SCM-Chg ((SCM-Chg (S,(Address_Add (S,(c P31address),(c P32const))),((S . (Address_Add (S,(c P31address),(c P32const)))) + (c P33const)))),(succ (IC S)))) . l9 by A6, A9, SCMPDS_1:def 24
.= (SCM-Chg (S,(Address_Add (S,(c P31address),(c P32const))),((S . (Address_Add (S,(c P31address),(c P32const)))) + (c P33const)))) . l9 by SCMPDS_1:28
.= S . l9 by SCMPDS_1:32 ; :: thesis: verum

end;

end;

end;

hence (SCM-Exec-Res (c,S)) . l9 = S . l9 ; :: thesis: verum

end;

case c in { [I3,{},<*d4,d5,k5,k6*>] where I3 is Element of Segm 14, d4, d5 is Element of SCM-Data-Loc , k5, k6 is Element of INT : I3 in {9,10,11,12,13} } ; :: thesis: (SCM-Exec-Res (c,S)) . l9 = S . l9

then consider I1 being Element of Segm 14, d1, d2 being Element of SCM-Data-Loc , k1, k2 being Element of INT such that
A10: c = [I1,{},<*d1,d2,k1,k2*>] and
A11: I1 in {9,10,11,12,13} ;

now

per cases ( I1 = 9 or I1 = 10 or I1 = 11 or I1 = 12 or I1 = 13 ) by A11, ENUMSET1:def 3;

case A12: I1 = 9 ; :: thesis: (SCM-Exec-Res (c,S)) . l9 = S . l9

set SS = SCM-Chg (S,(Address_Add (S,(c P41address),(c P43const))),((S . (Address_Add (S,(c P41address),(c P43const)))) + (S . (Address_Add (S,(c P42address),(c P44const))))));
thus (SCM-Exec-Res (c,S)) . l9 = (SCM-Chg ((SCM-Chg (S,(Address_Add (S,(c P41address),(c P43const))),((S . (Address_Add (S,(c P41address),(c P43const)))) + (S . (Address_Add (S,(c P42address),(c P44const))))))),(succ (IC S)))) . l9 by A10, A12, SCMPDS_1:def 24
.= (SCM-Chg (S,(Address_Add (S,(c P41address),(c P43const))),((S . (Address_Add (S,(c P41address),(c P43const)))) + (S . (Address_Add (S,(c P42address),(c P44const))))))) . l9 by SCMPDS_1:28
.= S . l9 by SCMPDS_1:32 ; :: thesis: verum

end;

case A13: I1 = 10 ; :: thesis: (SCM-Exec-Res (c,S)) . l9 = S . l9

set SS = SCM-Chg (S,(Address_Add (S,(c P41address),(c P43const))),((S . (Address_Add (S,(c P41address),(c P43const)))) - (S . (Address_Add (S,(c P42address),(c P44const))))));
thus (SCM-Exec-Res (c,S)) . l9 = (SCM-Chg ((SCM-Chg (S,(Address_Add (S,(c P41address),(c P43const))),((S . (Address_Add (S,(c P41address),(c P43const)))) - (S . (Address_Add (S,(c P42address),(c P44const))))))),(succ (IC S)))) . l9 by A10, A13, SCMPDS_1:def 24
.= (SCM-Chg (S,(Address_Add (S,(c P41address),(c P43const))),((S . (Address_Add (S,(c P41address),(c P43const)))) - (S . (Address_Add (S,(c P42address),(c P44const))))))) . l9 by SCMPDS_1:28
.= S . l9 by SCMPDS_1:32 ; :: thesis: verum

end;

case A14: I1 = 11 ; :: thesis: (SCM-Exec-Res (c,S)) . l9 = S . l9

set SS = SCM-Chg (S,(Address_Add (S,(c P41address),(c P43const))),((S . (Address_Add (S,(c P41address),(c P43const)))) * (S . (Address_Add (S,(c P42address),(c P44const))))));
thus (SCM-Exec-Res (c,S)) . l9 = (SCM-Chg ((SCM-Chg (S,(Address_Add (S,(c P41address),(c P43const))),((S . (Address_Add (S,(c P41address),(c P43const)))) * (S . (Address_Add (S,(c P42address),(c P44const))))))),(succ (IC S)))) . l9 by A10, A14, SCMPDS_1:def 24
.= (SCM-Chg (S,(Address_Add (S,(c P41address),(c P43const))),((S . (Address_Add (S,(c P41address),(c P43const)))) * (S . (Address_Add (S,(c P42address),(c P44const))))))) . l9 by SCMPDS_1:28
.= S . l9 by SCMPDS_1:32 ; :: thesis: verum

end;

case A15: I1 = 12 ; :: thesis: (SCM-Exec-Res (c,S)) . l9 = S . l9

set SA = SCM-Chg (S,(Address_Add (S,(c P41address),(c P43const))),((S . (Address_Add (S,(c P41address),(c P43const)))) div (S . (Address_Add (S,(c P42address),(c P44const))))));
set SB = SCM-Chg ((SCM-Chg (S,(Address_Add (S,(c P41address),(c P43const))),((S . (Address_Add (S,(c P41address),(c P43const)))) div (S . (Address_Add (S,(c P42address),(c P44const))))))),(Address_Add (S,(c P42address),(c P44const))),((S . (Address_Add (S,(c P41address),(c P43const)))) mod (S . (Address_Add (S,(c P42address),(c P44const))))));
thus (SCM-Exec-Res (c,S)) . l9 = (SCM-Chg ((SCM-Chg ((SCM-Chg (S,(Address_Add (S,(c P41address),(c P43const))),((S . (Address_Add (S,(c P41address),(c P43const)))) div (S . (Address_Add (S,(c P42address),(c P44const))))))),(Address_Add (S,(c P42address),(c P44const))),((S . (Address_Add (S,(c P41address),(c P43const)))) mod (S . (Address_Add (S,(c P42address),(c P44const))))))),(succ (IC S)))) . l9 by A10, A15, SCMPDS_1:def 24
.= (SCM-Chg ((SCM-Chg (S,(Address_Add (S,(c P41address),(c P43const))),((S . (Address_Add (S,(c P41address),(c P43const)))) div (S . (Address_Add (S,(c P42address),(c P44const))))))),(Address_Add (S,(c P42address),(c P44const))),((S . (Address_Add (S,(c P41address),(c P43const)))) mod (S . (Address_Add (S,(c P42address),(c P44const))))))) . l9 by SCMPDS_1:28
.= (SCM-Chg (S,(Address_Add (S,(c P41address),(c P43const))),((S . (Address_Add (S,(c P41address),(c P43const)))) div (S . (Address_Add (S,(c P42address),(c P44const))))))) . l9 by SCMPDS_1:32
.= S . l9 by SCMPDS_1:32 ; :: thesis: verum

end;

case A16: I1 = 13 ; :: thesis: (SCM-Exec-Res (c,S)) . l9 = S . l9

set SS = SCM-Chg (S,(Address_Add (S,(c P41address),(c P43const))),(S . (Address_Add (S,(c P42address),(c P44const)))));
thus (SCM-Exec-Res (c,S)) . l9 = (SCM-Chg ((SCM-Chg (S,(Address_Add (S,(c P41address),(c P43const))),(S . (Address_Add (S,(c P42address),(c P44const)))))),(succ (IC S)))) . l9 by A10, A16, SCMPDS_1:def 24
.= (SCM-Chg (S,(Address_Add (S,(c P41address),(c P43const))),(S . (Address_Add (S,(c P42address),(c P44const)))))) . l9 by SCMPDS_1:28
.= S . l9 by SCMPDS_1:32 ; :: thesis: verum

end;

end;

end;

hence (SCM-Exec-Res (c,S)) . l9 = S . l9 ; :: thesis: verum

end;

end;

end;

hence (Exec (i,s)) . l = s . l by SCMPDS_1:def 25; :: thesis: verum