IC in {(IC )} by TARSKI:def 1;
then A1: IC in SCM-Data-Loc \/ {(IC )} by XBOOLE_0:def 3;
let s1, s2 be State of SCMPDS; :: thesis: ( s1 | (SCM-Data-Loc \/ {(IC )}) = s2 | (SCM-Data-Loc \/ {(IC )}) implies for l being Instruction of SCMPDS holds (Exec (l,s1)) | (SCM-Data-Loc \/ {(IC )}) = (Exec (l,s2)) | (SCM-Data-Loc \/ {(IC )}) )
assume A2: s1 | (SCM-Data-Loc \/ {(IC )}) = s2 | (SCM-Data-Loc \/ {(IC )}) ; :: thesis: for l being Instruction of SCMPDS holds (Exec (l,s1)) | (SCM-Data-Loc \/ {(IC )}) = (Exec (l,s2)) | (SCM-Data-Loc \/ {(IC )})
A3: DataPart s1 = DataPart s2 by A2, RELAT_1:153, SCMPDS_2:84, XBOOLE_1:7;
A4: SCM-Data-Loc \/ {(IC )} c= the carrier of SCMPDS by AMI_3:1;
then SCM-Data-Loc \/ {(IC )} c= dom s2 by PARTFUN1:def 2;
then A5: IC in dom (s2 | (SCM-Data-Loc \/ {(IC )})) by A1, RELAT_1:62;
SCM-Data-Loc \/ {(IC )} c= dom s1 by A4, PARTFUN1:def 2;
then IC in dom (s1 | (SCM-Data-Loc \/ {(IC )})) by A1, RELAT_1:62;
then A6: IC s1 = (s2 | (SCM-Data-Loc \/ {(IC )})) . (IC ) by A2, FUNCT_1:47
.= IC s2 by A5, FUNCT_1:47 ;
let l be Instruction of SCMPDS; :: thesis: (Exec (l,s1)) | (SCM-Data-Loc \/ {(IC )}) = (Exec (l,s2)) | (SCM-Data-Loc \/ {(IC )})
A7: dom (Exec (l,s1)) = the carrier of SCMPDS by PARTFUN1:def 2;
then A8: dom (Exec (l,s1)) = dom (Exec (l,s2)) by PARTFUN1:def 2;
dom (Exec (l,s2)) = the carrier of SCMPDS by PARTFUN1:def 2;
then A9: dom (DataPart (Exec (l,s2))) = SCM-Data-Loc by RELAT_1:62, SCMPDS_2:84;
A10: dom (DataPart (Exec (l,s1))) = SCM-Data-Loc by A7, RELAT_1:62, SCMPDS_2:84;

per cases ( InsCode l = 0 or InsCode l = 1 or InsCode l = 2 or InsCode l = 3 or InsCode l = 4 or InsCode l = 5 or InsCode l = 6 or InsCode l = 7 or InsCode l = 8 or InsCode l = 9 or InsCode l = 10 or InsCode l = 11 or InsCode l = 12 or InsCode l = 13 ) by NAT_1:37, SCMPDS_2:6;

suppose InsCode l = 0 ; :: thesis: (Exec (l,s1)) | (SCM-Data-Loc \/ {(IC )}) = (Exec (l,s2)) | (SCM-Data-Loc \/ {(IC )})

then consider k1 being Integer such that
A11: l = goto k1 by SCMPDS_2:26;
for x being set st x in SCM-Data-Loc holds
(DataPart (Exec (l,s1))) . x = (DataPart (Exec (l,s2))) . x

proof

let x be set ; :: thesis: ( x in SCM-Data-Loc implies (DataPart (Exec (l,s1))) . x = (DataPart (Exec (l,s2))) . x )
assume A12: x in SCM-Data-Loc ; :: thesis: (DataPart (Exec (l,s1))) . x = (DataPart (Exec (l,s2))) . x
then reconsider a = x as Int_position by SCMPDS_2:3;
thus (DataPart (Exec (l,s1))) . x = (Exec (l,s1)) . a by A12, FUNCT_1:49, SCMPDS_2:84
.= s1 . a by A11, SCMPDS_2:54
.= (DataPart s1) . a by A12, FUNCT_1:49, SCMPDS_2:84
.= s2 . a by A3, A12, FUNCT_1:49, SCMPDS_2:84
.= (Exec (l,s2)) . a by A11, SCMPDS_2:54
.= (DataPart (Exec (l,s2))) . x by A12, FUNCT_1:49, SCMPDS_2:84 ; :: thesis: verum

end;

then A13: (Exec (l,s1)) | SCM-Data-Loc = (Exec (l,s2)) | SCM-Data-Loc by A10, A9, FUNCT_1:2, SCMPDS_2:84;
(Exec (l,s1)) . (IC ) = ICplusConst (s1,k1) by A11, SCMPDS_2:54
.= ICplusConst (s2,k1) by A6, Th2
.= (Exec (l,s2)) . (IC ) by A11, SCMPDS_2:54 ;
then (Exec (l,s1)) | {(IC )} = (Exec (l,s2)) | {(IC )} by A8, GRFUNC_1:29;
hence (Exec (l,s1)) | (SCM-Data-Loc \/ {(IC )}) = (Exec (l,s2)) | (SCM-Data-Loc \/ {(IC )}) by A13, RELAT_1:150; :: thesis: verum

end;

suppose InsCode l = 1 ; :: thesis: (Exec (l,s1)) | (SCM-Data-Loc \/ {(IC )}) = (Exec (l,s2)) | (SCM-Data-Loc \/ {(IC )})

then consider a being Int_position such that
A14: l = return a by SCMPDS_2:27;
for x being set st x in SCM-Data-Loc holds
(DataPart (Exec (l,s1))) . x = (DataPart (Exec (l,s2))) . x

proof

let x be set ; :: thesis: ( x in SCM-Data-Loc implies (DataPart (Exec (l,s1))) . x = (DataPart (Exec (l,s2))) . x )
assume A15: x in SCM-Data-Loc ; :: thesis: (DataPart (Exec (l,s1))) . x = (DataPart (Exec (l,s2))) . x
then reconsider b = x as Int_position by SCMPDS_2:3;

per cases ( b <> a or b = a ) ;

suppose A16: b <> a ; :: thesis: (DataPart (Exec (l,s1))) . x = (DataPart (Exec (l,s2))) . x

thus (DataPart (Exec (l,s1))) . x = (Exec (l,s1)) . b by A15, FUNCT_1:49, SCMPDS_2:84
.= s1 . b by A14, A16, SCMPDS_2:58
.= (DataPart s1) . b by A15, FUNCT_1:49, SCMPDS_2:84
.= s2 . b by A3, A15, FUNCT_1:49, SCMPDS_2:84
.= (Exec (l,s2)) . b by A14, A16, SCMPDS_2:58
.= (DataPart (Exec (l,s2))) . x by A15, FUNCT_1:49, SCMPDS_2:84 ; :: thesis: verum

end;

suppose A17: b = a ; :: thesis: (DataPart (Exec (l,s1))) . x = (DataPart (Exec (l,s2))) . x

thus (DataPart (Exec (l,s1))) . x = (Exec (l,s1)) . b by A15, FUNCT_1:49, SCMPDS_2:84
.= s1 . (DataLoc ((s1 . a),RetSP)) by A14, A17, SCMPDS_2:58
.= s2 . (DataLoc ((s2 . a),RetSP)) by A3, Th3
.= (Exec (l,s2)) . b by A14, A17, SCMPDS_2:58
.= (DataPart (Exec (l,s2))) . x by A15, FUNCT_1:49, SCMPDS_2:84 ; :: thesis: verum

end;

end;

end;

then A18: (Exec (l,s1)) | SCM-Data-Loc = (Exec (l,s2)) | SCM-Data-Loc by A10, A9, FUNCT_1:2, SCMPDS_2:84;
(Exec (l,s1)) . (IC ) = (abs (s1 . (DataLoc ((s1 . a),RetIC)))) + 2 by A14, SCMPDS_2:58
.= (abs (s2 . (DataLoc ((s2 . a),RetIC)))) + 2 by A3, Th3
.= (Exec (l,s2)) . (IC ) by A14, SCMPDS_2:58 ;
then (Exec (l,s1)) | {(IC )} = (Exec (l,s2)) | {(IC )} by A8, GRFUNC_1:29;
hence (Exec (l,s1)) | (SCM-Data-Loc \/ {(IC )}) = (Exec (l,s2)) | (SCM-Data-Loc \/ {(IC )}) by A18, RELAT_1:150; :: thesis: verum

end;

suppose InsCode l = 2 ; :: thesis: (Exec (l,s1)) | (SCM-Data-Loc \/ {(IC )}) = (Exec (l,s2)) | (SCM-Data-Loc \/ {(IC )})

then consider a being Int_position , k1 being Integer such that
A19: l = a := k1 by SCMPDS_2:28;
for x being set st x in SCM-Data-Loc holds
(DataPart (Exec (l,s1))) . x = (DataPart (Exec (l,s2))) . x

proof

let x be set ; :: thesis: ( x in SCM-Data-Loc implies (DataPart (Exec (l,s1))) . x = (DataPart (Exec (l,s2))) . x )
assume A20: x in SCM-Data-Loc ; :: thesis: (DataPart (Exec (l,s1))) . x = (DataPart (Exec (l,s2))) . x
then reconsider b = x as Int_position by SCMPDS_2:3;

per cases ( b <> a or b = a ) ;

suppose A21: b <> a ; :: thesis: (DataPart (Exec (l,s1))) . x = (DataPart (Exec (l,s2))) . x

thus (DataPart (Exec (l,s1))) . x = (Exec (l,s1)) . b by A20, FUNCT_1:49, SCMPDS_2:84
.= s1 . b by A19, A21, SCMPDS_2:45
.= (DataPart s1) . b by A20, FUNCT_1:49, SCMPDS_2:84
.= s2 . b by A3, A20, FUNCT_1:49, SCMPDS_2:84
.= (Exec (l,s2)) . b by A19, A21, SCMPDS_2:45
.= (DataPart (Exec (l,s2))) . x by A20, FUNCT_1:49, SCMPDS_2:84 ; :: thesis: verum

end;

suppose A22: b = a ; :: thesis: (DataPart (Exec (l,s1))) . x = (DataPart (Exec (l,s2))) . x

thus (DataPart (Exec (l,s1))) . x = (Exec (l,s1)) . b by A20, FUNCT_1:49, SCMPDS_2:84
.= k1 by A19, A22, SCMPDS_2:45
.= (Exec (l,s2)) . b by A19, A22, SCMPDS_2:45
.= (DataPart (Exec (l,s2))) . x by A20, FUNCT_1:49, SCMPDS_2:84 ; :: thesis: verum

end;

end;

end;

then A23: (Exec (l,s1)) | SCM-Data-Loc = (Exec (l,s2)) | SCM-Data-Loc by A10, A9, FUNCT_1:2, SCMPDS_2:84;
(Exec (l,s1)) . (IC ) = succ (IC s2) by A6, A19, SCMPDS_2:45
.= (Exec (l,s2)) . (IC ) by A19, SCMPDS_2:45 ;
then (Exec (l,s1)) | {(IC )} = (Exec (l,s2)) | {(IC )} by A8, GRFUNC_1:29;
hence (Exec (l,s1)) | (SCM-Data-Loc \/ {(IC )}) = (Exec (l,s2)) | (SCM-Data-Loc \/ {(IC )}) by A23, RELAT_1:150; :: thesis: verum

end;

suppose InsCode l = 3 ; :: thesis: (Exec (l,s1)) | (SCM-Data-Loc \/ {(IC )}) = (Exec (l,s2)) | (SCM-Data-Loc \/ {(IC )})

then consider a being Int_position , k1 being Integer such that
A24: l = saveIC (a,k1) by SCMPDS_2:29;
for x being set st x in SCM-Data-Loc holds
(DataPart (Exec (l,s1))) . x = (DataPart (Exec (l,s2))) . x

proof

let x be set ; :: thesis: ( x in SCM-Data-Loc implies (DataPart (Exec (l,s1))) . x = (DataPart (Exec (l,s2))) . x )
assume A25: x in SCM-Data-Loc ; :: thesis: (DataPart (Exec (l,s1))) . x = (DataPart (Exec (l,s2))) . x
then reconsider b = x as Int_position by SCMPDS_2:3;

per cases ( b <> DataLoc ((s1 . a),k1) or b = DataLoc ((s1 . a),k1) ) ;

suppose A26: b <> DataLoc ((s1 . a),k1) ; :: thesis: (DataPart (Exec (l,s1))) . x = (DataPart (Exec (l,s2))) . x

then A27: b <> DataLoc ((s2 . a),k1) by A3, Th4;
thus (DataPart (Exec (l,s1))) . x = (Exec (l,s1)) . b by A25, FUNCT_1:49, SCMPDS_2:84
.= s1 . b by A24, A26, SCMPDS_2:59
.= (DataPart s1) . b by A25, FUNCT_1:49, SCMPDS_2:84
.= s2 . b by A3, A25, FUNCT_1:49, SCMPDS_2:84
.= (Exec (l,s2)) . b by A24, A27, SCMPDS_2:59
.= (DataPart (Exec (l,s2))) . x by A25, FUNCT_1:49, SCMPDS_2:84 ; :: thesis: verum

end;

suppose A28: b = DataLoc ((s1 . a),k1) ; :: thesis: (DataPart (Exec (l,s1))) . x = (DataPart (Exec (l,s2))) . x

then A29: b = DataLoc ((s2 . a),k1) by A3, Th4;
thus (DataPart (Exec (l,s1))) . x = (Exec (l,s1)) . b by A25, FUNCT_1:49, SCMPDS_2:84
.= IC s2 by A6, A24, A28, SCMPDS_2:59
.= (Exec (l,s2)) . b by A24, A29, SCMPDS_2:59
.= (DataPart (Exec (l,s2))) . x by A25, FUNCT_1:49, SCMPDS_2:84 ; :: thesis: verum

end;

end;

end;

then A30: (Exec (l,s1)) | SCM-Data-Loc = (Exec (l,s2)) | SCM-Data-Loc by A10, A9, FUNCT_1:2, SCMPDS_2:84;
(Exec (l,s1)) . (IC ) = succ (IC s2) by A6, A24, SCMPDS_2:59
.= (Exec (l,s2)) . (IC ) by A24, SCMPDS_2:59 ;
then (Exec (l,s1)) | {(IC )} = (Exec (l,s2)) | {(IC )} by A8, GRFUNC_1:29;
hence (Exec (l,s1)) | (SCM-Data-Loc \/ {(IC )}) = (Exec (l,s2)) | (SCM-Data-Loc \/ {(IC )}) by A30, RELAT_1:150; :: thesis: verum

end;

suppose InsCode l = 4 ; :: thesis: (Exec (l,s1)) | (SCM-Data-Loc \/ {(IC )}) = (Exec (l,s2)) | (SCM-Data-Loc \/ {(IC )})

then consider a being Int_position , k1, k2 being Integer such that
A31: l = (a,k1) <>0_goto k2 by SCMPDS_2:30;

now

per cases ( s1 . (DataLoc ((s1 . a),k1)) <> 0 or s1 . (DataLoc ((s1 . a),k1)) = 0 ) ;

suppose A32: s1 . (DataLoc ((s1 . a),k1)) <> 0 ; :: thesis: (Exec (l,s1)) . (IC ) = (Exec (l,s2)) . (IC )

then A33: s2 . (DataLoc ((s2 . a),k1)) <> 0 by A3, Th3;
thus (Exec (l,s1)) . (IC ) = ICplusConst (s1,k2) by A31, A32, SCMPDS_2:55
.= ICplusConst (s2,k2) by A6, Th2
.= (Exec (l,s2)) . (IC ) by A31, A33, SCMPDS_2:55 ; :: thesis: verum

end;

suppose A34: s1 . (DataLoc ((s1 . a),k1)) = 0 ; :: thesis: (Exec (l,s1)) . (IC ) = (Exec (l,s2)) . (IC )

then A35: s2 . (DataLoc ((s2 . a),k1)) = 0 by A3, Th3;
thus (Exec (l,s1)) . (IC ) = succ (IC s2) by A6, A31, A34, SCMPDS_2:55
.= (Exec (l,s2)) . (IC ) by A31, A35, SCMPDS_2:55 ; :: thesis: verum

end;

end;

end;

then A36: (Exec (l,s1)) | {(IC )} = (Exec (l,s2)) | {(IC )} by A8, GRFUNC_1:29;
for x being set st x in SCM-Data-Loc holds
(DataPart (Exec (l,s1))) . x = (DataPart (Exec (l,s2))) . x

proof

let x be set ; :: thesis: ( x in SCM-Data-Loc implies (DataPart (Exec (l,s1))) . x = (DataPart (Exec (l,s2))) . x )
assume A37: x in SCM-Data-Loc ; :: thesis: (DataPart (Exec (l,s1))) . x = (DataPart (Exec (l,s2))) . x
then reconsider b = x as Int_position by SCMPDS_2:3;
thus (DataPart (Exec (l,s1))) . x = (Exec (l,s1)) . b by A37, FUNCT_1:49, SCMPDS_2:84
.= s1 . b by A31, SCMPDS_2:55
.= (DataPart s1) . b by A37, FUNCT_1:49, SCMPDS_2:84
.= s2 . b by A3, A37, FUNCT_1:49, SCMPDS_2:84
.= (Exec (l,s2)) . b by A31, SCMPDS_2:55
.= (DataPart (Exec (l,s2))) . x by A37, FUNCT_1:49, SCMPDS_2:84 ; :: thesis: verum

end;

then (Exec (l,s1)) | SCM-Data-Loc = (Exec (l,s2)) | SCM-Data-Loc by A10, A9, FUNCT_1:2, SCMPDS_2:84;
hence (Exec (l,s1)) | (SCM-Data-Loc \/ {(IC )}) = (Exec (l,s2)) | (SCM-Data-Loc \/ {(IC )}) by A36, RELAT_1:150; :: thesis: verum

end;

suppose InsCode l = 5 ; :: thesis: (Exec (l,s1)) | (SCM-Data-Loc \/ {(IC )}) = (Exec (l,s2)) | (SCM-Data-Loc \/ {(IC )})

then consider a being Int_position , k1, k2 being Integer such that
A38: l = (a,k1) <=0_goto k2 by SCMPDS_2:31;

now

per cases ( s1 . (DataLoc ((s1 . a),k1)) <= 0 or s1 . (DataLoc ((s1 . a),k1)) > 0 ) ;

suppose A39: s1 . (DataLoc ((s1 . a),k1)) <= 0 ; :: thesis: (Exec (l,s1)) . (IC ) = (Exec (l,s2)) . (IC )

then A40: s2 . (DataLoc ((s2 . a),k1)) <= 0 by A3, Th3;
thus (Exec (l,s1)) . (IC ) = ICplusConst (s1,k2) by A38, A39, SCMPDS_2:56
.= ICplusConst (s2,k2) by A6, Th2
.= (Exec (l,s2)) . (IC ) by A38, A40, SCMPDS_2:56 ; :: thesis: verum

end;

suppose A41: s1 . (DataLoc ((s1 . a),k1)) > 0 ; :: thesis: (Exec (l,s1)) . (IC ) = (Exec (l,s2)) . (IC )

then A42: s2 . (DataLoc ((s2 . a),k1)) > 0 by A3, Th3;
thus (Exec (l,s1)) . (IC ) = succ (IC s2) by A6, A38, A41, SCMPDS_2:56
.= (Exec (l,s2)) . (IC ) by A38, A42, SCMPDS_2:56 ; :: thesis: verum

end;

end;

end;

then A43: (Exec (l,s1)) | {(IC )} = (Exec (l,s2)) | {(IC )} by A8, GRFUNC_1:29;
for x being set st x in SCM-Data-Loc holds
(DataPart (Exec (l,s1))) . x = (DataPart (Exec (l,s2))) . x

proof

let x be set ; :: thesis: ( x in SCM-Data-Loc implies (DataPart (Exec (l,s1))) . x = (DataPart (Exec (l,s2))) . x )
assume A44: x in SCM-Data-Loc ; :: thesis: (DataPart (Exec (l,s1))) . x = (DataPart (Exec (l,s2))) . x
then reconsider b = x as Int_position by SCMPDS_2:3;
thus (DataPart (Exec (l,s1))) . x = (Exec (l,s1)) . b by A44, FUNCT_1:49, SCMPDS_2:84
.= s1 . b by A38, SCMPDS_2:56
.= (DataPart s1) . b by A44, FUNCT_1:49, SCMPDS_2:84
.= s2 . b by A3, A44, FUNCT_1:49, SCMPDS_2:84
.= (Exec (l,s2)) . b by A38, SCMPDS_2:56
.= (DataPart (Exec (l,s2))) . x by A44, FUNCT_1:49, SCMPDS_2:84 ; :: thesis: verum

end;

then (Exec (l,s1)) | SCM-Data-Loc = (Exec (l,s2)) | SCM-Data-Loc by A10, A9, FUNCT_1:2, SCMPDS_2:84;
hence (Exec (l,s1)) | (SCM-Data-Loc \/ {(IC )}) = (Exec (l,s2)) | (SCM-Data-Loc \/ {(IC )}) by A43, RELAT_1:150; :: thesis: verum

end;

suppose InsCode l = 6 ; :: thesis: (Exec (l,s1)) | (SCM-Data-Loc \/ {(IC )}) = (Exec (l,s2)) | (SCM-Data-Loc \/ {(IC )})

then consider a being Int_position , k1, k2 being Integer such that
A45: l = (a,k1) >=0_goto k2 by SCMPDS_2:32;

now

per cases ( s1 . (DataLoc ((s1 . a),k1)) >= 0 or s1 . (DataLoc ((s1 . a),k1)) < 0 ) ;

suppose A46: s1 . (DataLoc ((s1 . a),k1)) >= 0 ; :: thesis: (Exec (l,s1)) . (IC ) = (Exec (l,s2)) . (IC )

then A47: s2 . (DataLoc ((s2 . a),k1)) >= 0 by A3, Th3;
thus (Exec (l,s1)) . (IC ) = ICplusConst (s1,k2) by A45, A46, SCMPDS_2:57
.= ICplusConst (s2,k2) by A6, Th2
.= (Exec (l,s2)) . (IC ) by A45, A47, SCMPDS_2:57 ; :: thesis: verum

end;

suppose A48: s1 . (DataLoc ((s1 . a),k1)) < 0 ; :: thesis: (Exec (l,s1)) . (IC ) = (Exec (l,s2)) . (IC )

then A49: s2 . (DataLoc ((s2 . a),k1)) < 0 by A3, Th3;
thus (Exec (l,s1)) . (IC ) = succ (IC s2) by A6, A45, A48, SCMPDS_2:57
.= (Exec (l,s2)) . (IC ) by A45, A49, SCMPDS_2:57 ; :: thesis: verum

end;

end;

end;

then A50: (Exec (l,s1)) | {(IC )} = (Exec (l,s2)) | {(IC )} by A8, GRFUNC_1:29;
for x being set st x in SCM-Data-Loc holds
(DataPart (Exec (l,s1))) . x = (DataPart (Exec (l,s2))) . x

proof

let x be set ; :: thesis: ( x in SCM-Data-Loc implies (DataPart (Exec (l,s1))) . x = (DataPart (Exec (l,s2))) . x )
assume A51: x in SCM-Data-Loc ; :: thesis: (DataPart (Exec (l,s1))) . x = (DataPart (Exec (l,s2))) . x
then reconsider b = x as Int_position by SCMPDS_2:3;
thus (DataPart (Exec (l,s1))) . x = (Exec (l,s1)) . b by A51, FUNCT_1:49, SCMPDS_2:84
.= s1 . b by A45, SCMPDS_2:57
.= (DataPart s1) . b by A51, FUNCT_1:49, SCMPDS_2:84
.= s2 . b by A3, A51, FUNCT_1:49, SCMPDS_2:84
.= (Exec (l,s2)) . b by A45, SCMPDS_2:57
.= (DataPart (Exec (l,s2))) . x by A51, FUNCT_1:49, SCMPDS_2:84 ; :: thesis: verum

end;

then (Exec (l,s1)) | SCM-Data-Loc = (Exec (l,s2)) | SCM-Data-Loc by A10, A9, FUNCT_1:2, SCMPDS_2:84;
hence (Exec (l,s1)) | (SCM-Data-Loc \/ {(IC )}) = (Exec (l,s2)) | (SCM-Data-Loc \/ {(IC )}) by A50, RELAT_1:150; :: thesis: verum

end;

suppose InsCode l = 7 ; :: thesis: (Exec (l,s1)) | (SCM-Data-Loc \/ {(IC )}) = (Exec (l,s2)) | (SCM-Data-Loc \/ {(IC )})

then consider a being Int_position , k1, k2 being Integer such that
A52: l = (a,k1) := k2 by SCMPDS_2:33;
for x being set st x in SCM-Data-Loc holds
(DataPart (Exec (l,s1))) . x = (DataPart (Exec (l,s2))) . x

proof

let x be set ; :: thesis: ( x in SCM-Data-Loc implies (DataPart (Exec (l,s1))) . x = (DataPart (Exec (l,s2))) . x )
assume A53: x in SCM-Data-Loc ; :: thesis: (DataPart (Exec (l,s1))) . x = (DataPart (Exec (l,s2))) . x
then reconsider b = x as Int_position by SCMPDS_2:3;

per cases ( b <> DataLoc ((s1 . a),k1) or b = DataLoc ((s1 . a),k1) ) ;

suppose A54: b <> DataLoc ((s1 . a),k1) ; :: thesis: (DataPart (Exec (l,s1))) . x = (DataPart (Exec (l,s2))) . x

then A55: b <> DataLoc ((s2 . a),k1) by A3, Th4;
thus (DataPart (Exec (l,s1))) . x = (Exec (l,s1)) . b by A53, FUNCT_1:49, SCMPDS_2:84
.= s1 . b by A52, A54, SCMPDS_2:46
.= (DataPart s1) . b by A53, FUNCT_1:49, SCMPDS_2:84
.= s2 . b by A3, A53, FUNCT_1:49, SCMPDS_2:84
.= (Exec (l,s2)) . b by A52, A55, SCMPDS_2:46
.= (DataPart (Exec (l,s2))) . x by A53, FUNCT_1:49, SCMPDS_2:84 ; :: thesis: verum

end;

suppose A56: b = DataLoc ((s1 . a),k1) ; :: thesis: (DataPart (Exec (l,s1))) . x = (DataPart (Exec (l,s2))) . x

then A57: b = DataLoc ((s2 . a),k1) by A3, Th4;
thus (DataPart (Exec (l,s1))) . x = (Exec (l,s1)) . b by A53, FUNCT_1:49, SCMPDS_2:84
.= k2 by A52, A56, SCMPDS_2:46
.= (Exec (l,s2)) . b by A52, A57, SCMPDS_2:46
.= (DataPart (Exec (l,s2))) . x by A53, FUNCT_1:49, SCMPDS_2:84 ; :: thesis: verum

end;

end;

end;

then A58: (Exec (l,s1)) | SCM-Data-Loc = (Exec (l,s2)) | SCM-Data-Loc by A10, A9, FUNCT_1:2, SCMPDS_2:84;
(Exec (l,s1)) . (IC ) = succ (IC s2) by A6, A52, SCMPDS_2:46
.= (Exec (l,s2)) . (IC ) by A52, SCMPDS_2:46 ;
then (Exec (l,s1)) | {(IC )} = (Exec (l,s2)) | {(IC )} by A8, GRFUNC_1:29;
hence (Exec (l,s1)) | (SCM-Data-Loc \/ {(IC )}) = (Exec (l,s2)) | (SCM-Data-Loc \/ {(IC )}) by A58, RELAT_1:150; :: thesis: verum

end;

suppose InsCode l = 8 ; :: thesis: (Exec (l,s1)) | (SCM-Data-Loc \/ {(IC )}) = (Exec (l,s2)) | (SCM-Data-Loc \/ {(IC )})

then consider a being Int_position , k1, k2 being Integer such that
A59: l = AddTo (a,k1,k2) by SCMPDS_2:34;
for x being set st x in SCM-Data-Loc holds
(DataPart (Exec (l,s1))) . x = (DataPart (Exec (l,s2))) . x

proof

let x be set ; :: thesis: ( x in SCM-Data-Loc implies (DataPart (Exec (l,s1))) . x = (DataPart (Exec (l,s2))) . x )
assume A60: x in SCM-Data-Loc ; :: thesis: (DataPart (Exec (l,s1))) . x = (DataPart (Exec (l,s2))) . x
then reconsider b = x as Int_position by SCMPDS_2:3;

per cases ( b <> DataLoc ((s1 . a),k1) or b = DataLoc ((s1 . a),k1) ) ;

suppose A61: b <> DataLoc ((s1 . a),k1) ; :: thesis: (DataPart (Exec (l,s1))) . x = (DataPart (Exec (l,s2))) . x

then A62: b <> DataLoc ((s2 . a),k1) by A3, Th4;
thus (DataPart (Exec (l,s1))) . x = (Exec (l,s1)) . b by A60, FUNCT_1:49, SCMPDS_2:84
.= s1 . b by A59, A61, SCMPDS_2:48
.= (DataPart s1) . b by A60, FUNCT_1:49, SCMPDS_2:84
.= s2 . b by A3, A60, FUNCT_1:49, SCMPDS_2:84
.= (Exec (l,s2)) . b by A59, A62, SCMPDS_2:48
.= (DataPart (Exec (l,s2))) . x by A60, FUNCT_1:49, SCMPDS_2:84 ; :: thesis: verum

end;

suppose A63: b = DataLoc ((s1 . a),k1) ; :: thesis: (DataPart (Exec (l,s1))) . x = (DataPart (Exec (l,s2))) . x

then A64: b = DataLoc ((s2 . a),k1) by A3, Th4;
thus (DataPart (Exec (l,s1))) . x = (Exec (l,s1)) . b by A60, FUNCT_1:49, SCMPDS_2:84
.= (s1 . (DataLoc ((s1 . a),k1))) + k2 by A59, A63, SCMPDS_2:48
.= (s2 . (DataLoc ((s2 . a),k1))) + k2 by A3, Th3
.= (Exec (l,s2)) . b by A59, A64, SCMPDS_2:48
.= (DataPart (Exec (l,s2))) . x by A60, FUNCT_1:49, SCMPDS_2:84 ; :: thesis: verum

end;

end;

end;

then A65: (Exec (l,s1)) | SCM-Data-Loc = (Exec (l,s2)) | SCM-Data-Loc by A10, A9, FUNCT_1:2, SCMPDS_2:84;
(Exec (l,s1)) . (IC ) = succ (IC s2) by A6, A59, SCMPDS_2:48
.= (Exec (l,s2)) . (IC ) by A59, SCMPDS_2:48 ;
then (Exec (l,s1)) | {(IC )} = (Exec (l,s2)) | {(IC )} by A8, GRFUNC_1:29;
hence (Exec (l,s1)) | (SCM-Data-Loc \/ {(IC )}) = (Exec (l,s2)) | (SCM-Data-Loc \/ {(IC )}) by A65, RELAT_1:150; :: thesis: verum

end;

suppose InsCode l = 9 ; :: thesis: (Exec (l,s1)) | (SCM-Data-Loc \/ {(IC )}) = (Exec (l,s2)) | (SCM-Data-Loc \/ {(IC )})

then consider a, b being Int_position , k1, k2 being Integer such that
A66: l = AddTo (a,k1,b,k2) by SCMPDS_2:35;
for x being set st x in SCM-Data-Loc holds
(DataPart (Exec (l,s1))) . x = (DataPart (Exec (l,s2))) . x

proof

let x be set ; :: thesis: ( x in SCM-Data-Loc implies (DataPart (Exec (l,s1))) . x = (DataPart (Exec (l,s2))) . x )
assume A67: x in SCM-Data-Loc ; :: thesis: (DataPart (Exec (l,s1))) . x = (DataPart (Exec (l,s2))) . x
then reconsider c = x as Int_position by SCMPDS_2:3;

per cases ( c <> DataLoc ((s1 . a),k1) or c = DataLoc ((s1 . a),k1) ) ;

suppose A68: c <> DataLoc ((s1 . a),k1) ; :: thesis: (DataPart (Exec (l,s1))) . x = (DataPart (Exec (l,s2))) . x

then A69: c <> DataLoc ((s2 . a),k1) by A3, Th4;
thus (DataPart (Exec (l,s1))) . x = (Exec (l,s1)) . c by A67, FUNCT_1:49, SCMPDS_2:84
.= s1 . c by A66, A68, SCMPDS_2:49
.= (DataPart s1) . c by A67, FUNCT_1:49, SCMPDS_2:84
.= s2 . c by A3, A67, FUNCT_1:49, SCMPDS_2:84
.= (Exec (l,s2)) . c by A66, A69, SCMPDS_2:49
.= (DataPart (Exec (l,s2))) . x by A67, FUNCT_1:49, SCMPDS_2:84 ; :: thesis: verum

end;

suppose A70: c = DataLoc ((s1 . a),k1) ; :: thesis: (DataPart (Exec (l,s1))) . x = (DataPart (Exec (l,s2))) . x

then A71: c = DataLoc ((s2 . a),k1) by A3, Th4;
thus (DataPart (Exec (l,s1))) . x = (Exec (l,s1)) . c by A67, FUNCT_1:49, SCMPDS_2:84
.= (s1 . (DataLoc ((s1 . a),k1))) + (s1 . (DataLoc ((s1 . b),k2))) by A66, A70, SCMPDS_2:49
.= (s2 . (DataLoc ((s2 . a),k1))) + (s1 . (DataLoc ((s1 . b),k2))) by A3, Th3
.= (s2 . (DataLoc ((s2 . a),k1))) + (s2 . (DataLoc ((s2 . b),k2))) by A3, Th3
.= (Exec (l,s2)) . c by A66, A71, SCMPDS_2:49
.= (DataPart (Exec (l,s2))) . x by A67, FUNCT_1:49, SCMPDS_2:84 ; :: thesis: verum

end;

end;

end;

then A72: (Exec (l,s1)) | SCM-Data-Loc = (Exec (l,s2)) | SCM-Data-Loc by A10, A9, FUNCT_1:2, SCMPDS_2:84;
(Exec (l,s1)) . (IC ) = succ (IC s2) by A6, A66, SCMPDS_2:49
.= (Exec (l,s2)) . (IC ) by A66, SCMPDS_2:49 ;
then (Exec (l,s1)) | {(IC )} = (Exec (l,s2)) | {(IC )} by A8, GRFUNC_1:29;
hence (Exec (l,s1)) | (SCM-Data-Loc \/ {(IC )}) = (Exec (l,s2)) | (SCM-Data-Loc \/ {(IC )}) by A72, RELAT_1:150; :: thesis: verum

end;

suppose InsCode l = 10 ; :: thesis: (Exec (l,s1)) | (SCM-Data-Loc \/ {(IC )}) = (Exec (l,s2)) | (SCM-Data-Loc \/ {(IC )})

then consider a, b being Int_position , k1, k2 being Integer such that
A73: l = SubFrom (a,k1,b,k2) by SCMPDS_2:36;
for x being set st x in SCM-Data-Loc holds
(DataPart (Exec (l,s1))) . x = (DataPart (Exec (l,s2))) . x

proof

let x be set ; :: thesis: ( x in SCM-Data-Loc implies (DataPart (Exec (l,s1))) . x = (DataPart (Exec (l,s2))) . x )
assume A74: x in SCM-Data-Loc ; :: thesis: (DataPart (Exec (l,s1))) . x = (DataPart (Exec (l,s2))) . x
then reconsider c = x as Int_position by SCMPDS_2:3;

per cases ( c <> DataLoc ((s1 . a),k1) or c = DataLoc ((s1 . a),k1) ) ;

suppose A75: c <> DataLoc ((s1 . a),k1) ; :: thesis: (DataPart (Exec (l,s1))) . x = (DataPart (Exec (l,s2))) . x

then A76: c <> DataLoc ((s2 . a),k1) by A3, Th4;
thus (DataPart (Exec (l,s1))) . x = (Exec (l,s1)) . c by A74, FUNCT_1:49, SCMPDS_2:84
.= s1 . c by A73, A75, SCMPDS_2:50
.= (DataPart s1) . c by A74, FUNCT_1:49, SCMPDS_2:84
.= s2 . c by A3, A74, FUNCT_1:49, SCMPDS_2:84
.= (Exec (l,s2)) . c by A73, A76, SCMPDS_2:50
.= (DataPart (Exec (l,s2))) . x by A74, FUNCT_1:49, SCMPDS_2:84 ; :: thesis: verum

end;

suppose A77: c = DataLoc ((s1 . a),k1) ; :: thesis: (DataPart (Exec (l,s1))) . x = (DataPart (Exec (l,s2))) . x

then A78: c = DataLoc ((s2 . a),k1) by A3, Th4;
thus (DataPart (Exec (l,s1))) . x = (Exec (l,s1)) . c by A74, FUNCT_1:49, SCMPDS_2:84
.= (s1 . (DataLoc ((s1 . a),k1))) - (s1 . (DataLoc ((s1 . b),k2))) by A73, A77, SCMPDS_2:50
.= (s2 . (DataLoc ((s2 . a),k1))) - (s1 . (DataLoc ((s1 . b),k2))) by A3, Th3
.= (s2 . (DataLoc ((s2 . a),k1))) - (s2 . (DataLoc ((s2 . b),k2))) by A3, Th3
.= (Exec (l,s2)) . c by A73, A78, SCMPDS_2:50
.= (DataPart (Exec (l,s2))) . x by A74, FUNCT_1:49, SCMPDS_2:84 ; :: thesis: verum

end;

end;

end;

then A79: DataPart (Exec (l,s1)) = DataPart (Exec (l,s2)) by A10, A9, FUNCT_1:2;
(Exec (l,s1)) . (IC ) = succ (IC s2) by A6, A73, SCMPDS_2:50
.= (Exec (l,s2)) . (IC ) by A73, SCMPDS_2:50 ;
then (Exec (l,s1)) | {(IC )} = (Exec (l,s2)) | {(IC )} by A8, GRFUNC_1:29;
hence (Exec (l,s1)) | (SCM-Data-Loc \/ {(IC )}) = (Exec (l,s2)) | (SCM-Data-Loc \/ {(IC )}) by A79, RELAT_1:150, SCMPDS_2:84; :: thesis: verum

end;

suppose InsCode l = 11 ; :: thesis: (Exec (l,s1)) | (SCM-Data-Loc \/ {(IC )}) = (Exec (l,s2)) | (SCM-Data-Loc \/ {(IC )})

then consider a, b being Int_position , k1, k2 being Integer such that
A80: l = MultBy (a,k1,b,k2) by SCMPDS_2:37;
for x being set st x in SCM-Data-Loc holds
(DataPart (Exec (l,s1))) . x = (DataPart (Exec (l,s2))) . x

proof

let x be set ; :: thesis: ( x in SCM-Data-Loc implies (DataPart (Exec (l,s1))) . x = (DataPart (Exec (l,s2))) . x )
assume A81: x in SCM-Data-Loc ; :: thesis: (DataPart (Exec (l,s1))) . x = (DataPart (Exec (l,s2))) . x
then reconsider c = x as Int_position by SCMPDS_2:3;

per cases ( c <> DataLoc ((s1 . a),k1) or c = DataLoc ((s1 . a),k1) ) ;

suppose A82: c <> DataLoc ((s1 . a),k1) ; :: thesis: (DataPart (Exec (l,s1))) . x = (DataPart (Exec (l,s2))) . x

then A83: c <> DataLoc ((s2 . a),k1) by A3, Th4;
thus (DataPart (Exec (l,s1))) . x = (Exec (l,s1)) . c by A81, FUNCT_1:49, SCMPDS_2:84
.= s1 . c by A80, A82, SCMPDS_2:51
.= (DataPart s1) . c by A81, FUNCT_1:49, SCMPDS_2:84
.= s2 . c by A3, A81, FUNCT_1:49, SCMPDS_2:84
.= (Exec (l,s2)) . c by A80, A83, SCMPDS_2:51
.= (DataPart (Exec (l,s2))) . x by A81, FUNCT_1:49, SCMPDS_2:84 ; :: thesis: verum

end;

suppose A84: c = DataLoc ((s1 . a),k1) ; :: thesis: (DataPart (Exec (l,s1))) . x = (DataPart (Exec (l,s2))) . x

then A85: c = DataLoc ((s2 . a),k1) by A3, Th4;
thus (DataPart (Exec (l,s1))) . x = (Exec (l,s1)) . c by A81, FUNCT_1:49, SCMPDS_2:84
.= (s1 . (DataLoc ((s1 . a),k1))) * (s1 . (DataLoc ((s1 . b),k2))) by A80, A84, SCMPDS_2:51
.= (s2 . (DataLoc ((s2 . a),k1))) * (s1 . (DataLoc ((s1 . b),k2))) by A3, Th3
.= (s2 . (DataLoc ((s2 . a),k1))) * (s2 . (DataLoc ((s2 . b),k2))) by A3, Th3
.= (Exec (l,s2)) . c by A80, A85, SCMPDS_2:51
.= (DataPart (Exec (l,s2))) . x by A81, FUNCT_1:49, SCMPDS_2:84 ; :: thesis: verum

end;

end;

end;

then A86: DataPart (Exec (l,s1)) = DataPart (Exec (l,s2)) by A10, A9, FUNCT_1:2;
(Exec (l,s1)) . (IC ) = succ (IC s2) by A6, A80, SCMPDS_2:51
.= (Exec (l,s2)) . (IC ) by A80, SCMPDS_2:51 ;
then (Exec (l,s1)) | {(IC )} = (Exec (l,s2)) | {(IC )} by A8, GRFUNC_1:29;
hence (Exec (l,s1)) | (SCM-Data-Loc \/ {(IC )}) = (Exec (l,s2)) | (SCM-Data-Loc \/ {(IC )}) by A86, RELAT_1:150, SCMPDS_2:84; :: thesis: verum

end;

suppose InsCode l = 12 ; :: thesis: (Exec (l,s1)) | (SCM-Data-Loc \/ {(IC )}) = (Exec (l,s2)) | (SCM-Data-Loc \/ {(IC )})

then consider a, b being Int_position , k1, k2 being Integer such that
A87: l = Divide (a,k1,b,k2) by SCMPDS_2:38;
for x being set st x in SCM-Data-Loc holds
(DataPart (Exec (l,s1))) . x = (DataPart (Exec (l,s2))) . x

proof

let x be set ; :: thesis: ( x in SCM-Data-Loc implies (DataPart (Exec (l,s1))) . x = (DataPart (Exec (l,s2))) . x )
assume A88: x in SCM-Data-Loc ; :: thesis: (DataPart (Exec (l,s1))) . x = (DataPart (Exec (l,s2))) . x
then reconsider c = x as Int_position by SCMPDS_2:3;

per cases ( c = DataLoc ((s1 . b),k2) or c <> DataLoc ((s1 . b),k2) ) ;

suppose A89: c = DataLoc ((s1 . b),k2) ; :: thesis: (DataPart (Exec (l,s1))) . x = (DataPart (Exec (l,s2))) . x

then A90: c = DataLoc ((s2 . b),k2) by A3, Th4;
thus (DataPart (Exec (l,s1))) . x = (Exec (l,s1)) . c by A88, FUNCT_1:49, SCMPDS_2:84
.= (s1 . (DataLoc ((s1 . a),k1))) mod (s1 . (DataLoc ((s1 . b),k2))) by A87, A89, SCMPDS_2:52
.= (s2 . (DataLoc ((s2 . a),k1))) mod (s1 . (DataLoc ((s1 . b),k2))) by A3, Th3
.= (s2 . (DataLoc ((s2 . a),k1))) mod (s2 . (DataLoc ((s2 . b),k2))) by A3, Th3
.= (Exec (l,s2)) . c by A87, A90, SCMPDS_2:52
.= (DataPart (Exec (l,s2))) . x by A88, FUNCT_1:49, SCMPDS_2:84 ; :: thesis: verum

end;

suppose A91: c <> DataLoc ((s1 . b),k2) ; :: thesis: (DataPart (Exec (l,s1))) . x = (DataPart (Exec (l,s2))) . x

then A92: c <> DataLoc ((s2 . b),k2) by A3, Th4;

hereby :: thesis: verum

per cases ( c <> DataLoc ((s1 . a),k1) or c = DataLoc ((s1 . a),k1) ) ;

suppose A93: c <> DataLoc ((s1 . a),k1) ; :: thesis: (DataPart (Exec (l,s1))) . x = (DataPart (Exec (l,s2))) . x

then A94: c <> DataLoc ((s2 . a),k1) by A3, Th4;
thus (DataPart (Exec (l,s1))) . x = (Exec (l,s1)) . c by A88, FUNCT_1:49, SCMPDS_2:84
.= s1 . c by A87, A91, A93, SCMPDS_2:52
.= s2 . c by A3, Th4
.= (Exec (l,s2)) . c by A87, A92, A94, SCMPDS_2:52
.= (DataPart (Exec (l,s2))) . x by A88, FUNCT_1:49, SCMPDS_2:84 ; :: thesis: verum

end;

suppose A95: c = DataLoc ((s1 . a),k1) ; :: thesis: (DataPart (Exec (l,s1))) . x = (DataPart (Exec (l,s2))) . x

then A96: c = DataLoc ((s2 . a),k1) by A3, Th4;
thus (DataPart (Exec (l,s1))) . x = (Exec (l,s1)) . c by A88, FUNCT_1:49, SCMPDS_2:84
.= (s1 . (DataLoc ((s1 . a),k1))) div (s1 . (DataLoc ((s1 . b),k2))) by A87, A91, A95, SCMPDS_2:52
.= (s2 . (DataLoc ((s2 . a),k1))) div (s1 . (DataLoc ((s1 . b),k2))) by A3, Th3
.= (s2 . (DataLoc ((s2 . a),k1))) div (s2 . (DataLoc ((s2 . b),k2))) by A3, Th3
.= (Exec (l,s2)) . c by A87, A92, A96, SCMPDS_2:52
.= (DataPart (Exec (l,s2))) . x by A88, FUNCT_1:49, SCMPDS_2:84 ; :: thesis: verum

end;

end;

end;

end;

end;

end;

then A97: DataPart (Exec (l,s1)) = DataPart (Exec (l,s2)) by A10, A9, FUNCT_1:2;
(Exec (l,s1)) . (IC ) = succ (IC s2) by A6, A87, SCMPDS_2:52
.= (Exec (l,s2)) . (IC ) by A87, SCMPDS_2:52 ;
then (Exec (l,s1)) | {(IC )} = (Exec (l,s2)) | {(IC )} by A8, GRFUNC_1:29;
hence (Exec (l,s1)) | (SCM-Data-Loc \/ {(IC )}) = (Exec (l,s2)) | (SCM-Data-Loc \/ {(IC )}) by A97, RELAT_1:150, SCMPDS_2:84; :: thesis: verum

end;

suppose InsCode l = 13 ; :: thesis: (Exec (l,s1)) | (SCM-Data-Loc \/ {(IC )}) = (Exec (l,s2)) | (SCM-Data-Loc \/ {(IC )})

then consider a, b being Int_position , k1, k2 being Integer such that
A98: l = (a,k1) := (b,k2) by SCMPDS_2:39;
for x being set st x in SCM-Data-Loc holds
(DataPart (Exec (l,s1))) . x = (DataPart (Exec (l,s2))) . x

proof

let x be set ; :: thesis: ( x in SCM-Data-Loc implies (DataPart (Exec (l,s1))) . x = (DataPart (Exec (l,s2))) . x )
assume A99: x in SCM-Data-Loc ; :: thesis: (DataPart (Exec (l,s1))) . x = (DataPart (Exec (l,s2))) . x
then reconsider c = x as Int_position by SCMPDS_2:3;

per cases ( c <> DataLoc ((s1 . a),k1) or c = DataLoc ((s1 . a),k1) ) ;

suppose A100: c <> DataLoc ((s1 . a),k1) ; :: thesis: (DataPart (Exec (l,s1))) . x = (DataPart (Exec (l,s2))) . x

then A101: c <> DataLoc ((s2 . a),k1) by A3, Th4;
thus (DataPart (Exec (l,s1))) . x = (Exec (l,s1)) . c by A99, FUNCT_1:49, SCMPDS_2:84
.= s1 . c by A98, A100, SCMPDS_2:47
.= (DataPart s1) . c by A99, FUNCT_1:49, SCMPDS_2:84
.= s2 . c by A3, A99, FUNCT_1:49, SCMPDS_2:84
.= (Exec (l,s2)) . c by A98, A101, SCMPDS_2:47
.= (DataPart (Exec (l,s2))) . x by A99, FUNCT_1:49, SCMPDS_2:84 ; :: thesis: verum

end;

suppose A102: c = DataLoc ((s1 . a),k1) ; :: thesis: (DataPart (Exec (l,s1))) . x = (DataPart (Exec (l,s2))) . x

then A103: c = DataLoc ((s2 . a),k1) by A3, Th4;
thus (DataPart (Exec (l,s1))) . x = (Exec (l,s1)) . c by A99, FUNCT_1:49, SCMPDS_2:84
.= s1 . (DataLoc ((s1 . b),k2)) by A98, A102, SCMPDS_2:47
.= s2 . (DataLoc ((s2 . b),k2)) by A3, Th3
.= (Exec (l,s2)) . c by A98, A103, SCMPDS_2:47
.= (DataPart (Exec (l,s2))) . x by A99, FUNCT_1:49, SCMPDS_2:84 ; :: thesis: verum

end;

end;

end;

then A104: DataPart (Exec (l,s1)) = DataPart (Exec (l,s2)) by A10, A9, FUNCT_1:2;
(Exec (l,s1)) . (IC ) = succ (IC s2) by A6, A98, SCMPDS_2:47
.= (Exec (l,s2)) . (IC ) by A98, SCMPDS_2:47 ;
then (Exec (l,s1)) | {(IC )} = (Exec (l,s2)) | {(IC )} by A8, GRFUNC_1:29;
hence (Exec (l,s1)) | (SCM-Data-Loc \/ {(IC )}) = (Exec (l,s2)) | (SCM-Data-Loc \/ {(IC )}) by A104, RELAT_1:150, SCMPDS_2:84; :: thesis: verum

end;

end;