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