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

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:38, SCMPDS_2:15;

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

then consider k1 being Integer such that
A11: l = goto k1 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 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:9;
thus (DataPart (Exec (l,s1))) . x = (Exec (l,s1)) . a by A12, FUNCT_1:72, SCMPDS_2:100
.= s1 . a by A11, SCMPDS_2:66
.= (DataPart s1) . a by A12, FUNCT_1:72, SCMPDS_2:100
.= s2 . a by A3, A12, FUNCT_1:72, SCMPDS_2:100
.= (Exec (l,s2)) . a by A11, SCMPDS_2:66
.= (DataPart (Exec (l,s2))) . x by A12, FUNCT_1:72, SCMPDS_2:100 ; :: thesis: verum

end;

then A13: (Exec (l,s1)) | SCM-Data-Loc = (Exec (l,s2)) | SCM-Data-Loc by A10, A9, FUNCT_1:9, SCMPDS_2:100;
(Exec (l,s1)) . (IC SCMPDS) = ICplusConst (s1,k1) by A11, SCMPDS_2:66
.= ICplusConst (s2,k1) by A6, Th2
.= (Exec (l,s2)) . (IC SCMPDS) by A11, SCMPDS_2:66 ;
then (Exec (l,s1)) | {(IC SCMPDS)} = (Exec (l,s2)) | {(IC SCMPDS)} by A8, GRFUNC_1:90;
hence (Exec (l,s1)) | (SCM-Data-Loc \/ {(IC SCMPDS)}) = (Exec (l,s2)) | (SCM-Data-Loc \/ {(IC SCMPDS)}) by A13, RELAT_1:185; :: thesis: verum

end;

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

then consider a being Int_position such that
A14: l = return a 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 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:9;

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:72, SCMPDS_2:100
.= s1 . b by A14, A16, SCMPDS_2:70
.= (DataPart s1) . b by A15, FUNCT_1:72, SCMPDS_2:100
.= s2 . b by A3, A15, FUNCT_1:72, SCMPDS_2:100
.= (Exec (l,s2)) . b by A14, A16, SCMPDS_2:70
.= (DataPart (Exec (l,s2))) . x by A15, FUNCT_1:72, SCMPDS_2:100 ; :: 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:72, SCMPDS_2:100
.= s1 . (DataLoc ((s1 . a),RetSP)) by A14, A17, SCMPDS_2:70
.= s2 . (DataLoc ((s2 . a),RetSP)) by A3, Th3
.= (Exec (l,s2)) . b by A14, A17, SCMPDS_2:70
.= (DataPart (Exec (l,s2))) . x by A15, FUNCT_1:72, SCMPDS_2:100 ; :: thesis: verum

end;

end;

end;

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

end;

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

then consider a being Int_position , k1 being Integer such that
A19: l = a := k1 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 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:9;

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:72, SCMPDS_2:100
.= s1 . b by A19, A21, SCMPDS_2:57
.= (DataPart s1) . b by A20, FUNCT_1:72, SCMPDS_2:100
.= s2 . b by A3, A20, FUNCT_1:72, SCMPDS_2:100
.= (Exec (l,s2)) . b by A19, A21, SCMPDS_2:57
.= (DataPart (Exec (l,s2))) . x by A20, FUNCT_1:72, SCMPDS_2:100 ; :: 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:72, SCMPDS_2:100
.= k1 by A19, A22, SCMPDS_2:57
.= (Exec (l,s2)) . b by A19, A22, SCMPDS_2:57
.= (DataPart (Exec (l,s2))) . x by A20, FUNCT_1:72, SCMPDS_2:100 ; :: thesis: verum

end;

end;

end;

then A23: (Exec (l,s1)) | SCM-Data-Loc = (Exec (l,s2)) | SCM-Data-Loc by A10, A9, FUNCT_1:9, SCMPDS_2:100;
(Exec (l,s1)) . (IC SCMPDS) = succ (IC s2) by A6, A19, SCMPDS_2:57
.= (Exec (l,s2)) . (IC SCMPDS) by A19, SCMPDS_2:57 ;
then (Exec (l,s1)) | {(IC SCMPDS)} = (Exec (l,s2)) | {(IC SCMPDS)} by A8, GRFUNC_1:90;
hence (Exec (l,s1)) | (SCM-Data-Loc \/ {(IC SCMPDS)}) = (Exec (l,s2)) | (SCM-Data-Loc \/ {(IC SCMPDS)}) by A23, RELAT_1:185; :: thesis: verum

end;

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

then consider a being Int_position , k1 being Integer such that
A24: l = saveIC (a,k1) 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 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:9;

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:72, SCMPDS_2:100
.= s1 . b by A24, A26, SCMPDS_2:71
.= (DataPart s1) . b by A25, FUNCT_1:72, SCMPDS_2:100
.= s2 . b by A3, A25, FUNCT_1:72, SCMPDS_2:100
.= (Exec (l,s2)) . b by A24, A27, SCMPDS_2:71
.= (DataPart (Exec (l,s2))) . x by A25, FUNCT_1:72, SCMPDS_2:100 ; :: 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:72, SCMPDS_2:100
.= IC s2 by A6, A24, A28, SCMPDS_2:71
.= (Exec (l,s2)) . b by A24, A29, SCMPDS_2:71
.= (DataPart (Exec (l,s2))) . x by A25, FUNCT_1:72, SCMPDS_2:100 ; :: thesis: verum

end;

end;

end;

then A30: (Exec (l,s1)) | SCM-Data-Loc = (Exec (l,s2)) | SCM-Data-Loc by A10, A9, FUNCT_1:9, SCMPDS_2:100;
(Exec (l,s1)) . (IC SCMPDS) = succ (IC s2) by A6, A24, SCMPDS_2:71
.= (Exec (l,s2)) . (IC SCMPDS) by A24, SCMPDS_2:71 ;
then (Exec (l,s1)) | {(IC SCMPDS)} = (Exec (l,s2)) | {(IC SCMPDS)} by A8, GRFUNC_1:90;
hence (Exec (l,s1)) | (SCM-Data-Loc \/ {(IC SCMPDS)}) = (Exec (l,s2)) | (SCM-Data-Loc \/ {(IC SCMPDS)}) by A30, RELAT_1:185; :: thesis: verum

end;

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

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

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 SCMPDS) = (Exec (l,s2)) . (IC SCMPDS)

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

end;

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

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

end;

end;

end;

then A36: (Exec (l,s1)) | {(IC SCMPDS)} = (Exec (l,s2)) | {(IC SCMPDS)} by A8, GRFUNC_1:90;
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:9;
thus (DataPart (Exec (l,s1))) . x = (Exec (l,s1)) . b by A37, FUNCT_1:72, SCMPDS_2:100
.= s1 . b by A31, SCMPDS_2:67
.= (DataPart s1) . b by A37, FUNCT_1:72, SCMPDS_2:100
.= s2 . b by A3, A37, FUNCT_1:72, SCMPDS_2:100
.= (Exec (l,s2)) . b by A31, SCMPDS_2:67
.= (DataPart (Exec (l,s2))) . x by A37, FUNCT_1:72, SCMPDS_2:100 ; :: thesis: verum

end;

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

end;

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

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

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 SCMPDS) = (Exec (l,s2)) . (IC SCMPDS)

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

end;

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

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

end;

end;

end;

then A43: (Exec (l,s1)) | {(IC SCMPDS)} = (Exec (l,s2)) | {(IC SCMPDS)} by A8, GRFUNC_1:90;
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:9;
thus (DataPart (Exec (l,s1))) . x = (Exec (l,s1)) . b by A44, FUNCT_1:72, SCMPDS_2:100
.= s1 . b by A38, SCMPDS_2:68
.= (DataPart s1) . b by A44, FUNCT_1:72, SCMPDS_2:100
.= s2 . b by A3, A44, FUNCT_1:72, SCMPDS_2:100
.= (Exec (l,s2)) . b by A38, SCMPDS_2:68
.= (DataPart (Exec (l,s2))) . x by A44, FUNCT_1:72, SCMPDS_2:100 ; :: thesis: verum

end;

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

end;

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

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

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 SCMPDS) = (Exec (l,s2)) . (IC SCMPDS)

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

end;

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

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

end;

end;

end;

then A50: (Exec (l,s1)) | {(IC SCMPDS)} = (Exec (l,s2)) | {(IC SCMPDS)} by A8, GRFUNC_1:90;
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:9;
thus (DataPart (Exec (l,s1))) . x = (Exec (l,s1)) . b by A51, FUNCT_1:72, SCMPDS_2:100
.= s1 . b by A45, SCMPDS_2:69
.= (DataPart s1) . b by A51, FUNCT_1:72, SCMPDS_2:100
.= s2 . b by A3, A51, FUNCT_1:72, SCMPDS_2:100
.= (Exec (l,s2)) . b by A45, SCMPDS_2:69
.= (DataPart (Exec (l,s2))) . x by A51, FUNCT_1:72, SCMPDS_2:100 ; :: thesis: verum

end;

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

end;

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

then consider a being Int_position , k1, k2 being Integer such that
A52: l = (a,k1) := k2 by SCMPDS_2:42;
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:9;

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:72, SCMPDS_2:100
.= s1 . b by A52, A54, SCMPDS_2:58
.= (DataPart s1) . b by A53, FUNCT_1:72, SCMPDS_2:100
.= s2 . b by A3, A53, FUNCT_1:72, SCMPDS_2:100
.= (Exec (l,s2)) . b by A52, A55, SCMPDS_2:58
.= (DataPart (Exec (l,s2))) . x by A53, FUNCT_1:72, SCMPDS_2:100 ; :: 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:72, SCMPDS_2:100
.= k2 by A52, A56, SCMPDS_2:58
.= (Exec (l,s2)) . b by A52, A57, SCMPDS_2:58
.= (DataPart (Exec (l,s2))) . x by A53, FUNCT_1:72, SCMPDS_2:100 ; :: thesis: verum

end;

end;

end;

then A58: (Exec (l,s1)) | SCM-Data-Loc = (Exec (l,s2)) | SCM-Data-Loc by A10, A9, FUNCT_1:9, SCMPDS_2:100;
(Exec (l,s1)) . (IC SCMPDS) = succ (IC s2) by A6, A52, SCMPDS_2:58
.= (Exec (l,s2)) . (IC SCMPDS) by A52, SCMPDS_2:58 ;
then (Exec (l,s1)) | {(IC SCMPDS)} = (Exec (l,s2)) | {(IC SCMPDS)} by A8, GRFUNC_1:90;
hence (Exec (l,s1)) | (SCM-Data-Loc \/ {(IC SCMPDS)}) = (Exec (l,s2)) | (SCM-Data-Loc \/ {(IC SCMPDS)}) by A58, RELAT_1:185; :: thesis: verum

end;

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

then consider a being Int_position , k1, k2 being Integer such that
A59: l = AddTo (a,k1,k2) by SCMPDS_2:43;
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:9;

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:72, SCMPDS_2:100
.= s1 . b by A59, A61, SCMPDS_2:60
.= (DataPart s1) . b by A60, FUNCT_1:72, SCMPDS_2:100
.= s2 . b by A3, A60, FUNCT_1:72, SCMPDS_2:100
.= (Exec (l,s2)) . b by A59, A62, SCMPDS_2:60
.= (DataPart (Exec (l,s2))) . x by A60, FUNCT_1:72, SCMPDS_2:100 ; :: 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:72, SCMPDS_2:100
.= (s1 . (DataLoc ((s1 . a),k1))) + k2 by A59, A63, SCMPDS_2:60
.= (s2 . (DataLoc ((s2 . a),k1))) + k2 by A3, Th3
.= (Exec (l,s2)) . b by A59, A64, SCMPDS_2:60
.= (DataPart (Exec (l,s2))) . x by A60, FUNCT_1:72, SCMPDS_2:100 ; :: thesis: verum

end;

end;

end;

then A65: (Exec (l,s1)) | SCM-Data-Loc = (Exec (l,s2)) | SCM-Data-Loc by A10, A9, FUNCT_1:9, SCMPDS_2:100;
(Exec (l,s1)) . (IC SCMPDS) = succ (IC s2) by A6, A59, SCMPDS_2:60
.= (Exec (l,s2)) . (IC SCMPDS) by A59, SCMPDS_2:60 ;
then (Exec (l,s1)) | {(IC SCMPDS)} = (Exec (l,s2)) | {(IC SCMPDS)} by A8, GRFUNC_1:90;
hence (Exec (l,s1)) | (SCM-Data-Loc \/ {(IC SCMPDS)}) = (Exec (l,s2)) | (SCM-Data-Loc \/ {(IC SCMPDS)}) by A65, RELAT_1:185; :: thesis: verum

end;

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

then consider a, b being Int_position , k1, k2 being Integer such that
A66: l = AddTo (a,k1,b,k2) by SCMPDS_2:44;
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:9;

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:72, SCMPDS_2:100
.= s1 . c by A66, A68, SCMPDS_2:61
.= (DataPart s1) . c by A67, FUNCT_1:72, SCMPDS_2:100
.= s2 . c by A3, A67, FUNCT_1:72, SCMPDS_2:100
.= (Exec (l,s2)) . c by A66, A69, SCMPDS_2:61
.= (DataPart (Exec (l,s2))) . x by A67, FUNCT_1:72, SCMPDS_2:100 ; :: 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:72, SCMPDS_2:100
.= (s1 . (DataLoc ((s1 . a),k1))) + (s1 . (DataLoc ((s1 . b),k2))) by A66, A70, SCMPDS_2:61
.= (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:61
.= (DataPart (Exec (l,s2))) . x by A67, FUNCT_1:72, SCMPDS_2:100 ; :: thesis: verum

end;

end;

end;

then A72: (Exec (l,s1)) | SCM-Data-Loc = (Exec (l,s2)) | SCM-Data-Loc by A10, A9, FUNCT_1:9, SCMPDS_2:100;
(Exec (l,s1)) . (IC SCMPDS) = succ (IC s2) by A6, A66, SCMPDS_2:61
.= (Exec (l,s2)) . (IC SCMPDS) by A66, SCMPDS_2:61 ;
then (Exec (l,s1)) | {(IC SCMPDS)} = (Exec (l,s2)) | {(IC SCMPDS)} by A8, GRFUNC_1:90;
hence (Exec (l,s1)) | (SCM-Data-Loc \/ {(IC SCMPDS)}) = (Exec (l,s2)) | (SCM-Data-Loc \/ {(IC SCMPDS)}) by A72, RELAT_1:185; :: thesis: verum

end;

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

then consider a, b being Int_position , k1, k2 being Integer such that
A73: l = SubFrom (a,k1,b,k2) by SCMPDS_2:45;
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:9;

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:72, SCMPDS_2:100
.= s1 . c by A73, A75, SCMPDS_2:62
.= (DataPart s1) . c by A74, FUNCT_1:72, SCMPDS_2:100
.= s2 . c by A3, A74, FUNCT_1:72, SCMPDS_2:100
.= (Exec (l,s2)) . c by A73, A76, SCMPDS_2:62
.= (DataPart (Exec (l,s2))) . x by A74, FUNCT_1:72, SCMPDS_2:100 ; :: 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:72, SCMPDS_2:100
.= (s1 . (DataLoc ((s1 . a),k1))) - (s1 . (DataLoc ((s1 . b),k2))) by A73, A77, SCMPDS_2:62
.= (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:62
.= (DataPart (Exec (l,s2))) . x by A74, FUNCT_1:72, SCMPDS_2:100 ; :: thesis: verum

end;

end;

end;

then A79: DataPart (Exec (l,s1)) = DataPart (Exec (l,s2)) by A10, A9, FUNCT_1:9;
(Exec (l,s1)) . (IC SCMPDS) = succ (IC s2) by A6, A73, SCMPDS_2:62
.= (Exec (l,s2)) . (IC SCMPDS) by A73, SCMPDS_2:62 ;
then (Exec (l,s1)) | {(IC SCMPDS)} = (Exec (l,s2)) | {(IC SCMPDS)} by A8, GRFUNC_1:90;
hence (Exec (l,s1)) | (SCM-Data-Loc \/ {(IC SCMPDS)}) = (Exec (l,s2)) | (SCM-Data-Loc \/ {(IC SCMPDS)}) by A79, RELAT_1:185, SCMPDS_2:100; :: thesis: verum

end;

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

then consider a, b being Int_position , k1, k2 being Integer such that
A80: l = MultBy (a,k1,b,k2) by SCMPDS_2:46;
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:9;

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:72, SCMPDS_2:100
.= s1 . c by A80, A82, SCMPDS_2:63
.= (DataPart s1) . c by A81, FUNCT_1:72, SCMPDS_2:100
.= s2 . c by A3, A81, FUNCT_1:72, SCMPDS_2:100
.= (Exec (l,s2)) . c by A80, A83, SCMPDS_2:63
.= (DataPart (Exec (l,s2))) . x by A81, FUNCT_1:72, SCMPDS_2:100 ; :: 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:72, SCMPDS_2:100
.= (s1 . (DataLoc ((s1 . a),k1))) * (s1 . (DataLoc ((s1 . b),k2))) by A80, A84, SCMPDS_2:63
.= (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:63
.= (DataPart (Exec (l,s2))) . x by A81, FUNCT_1:72, SCMPDS_2:100 ; :: thesis: verum

end;

end;

end;

then A86: DataPart (Exec (l,s1)) = DataPart (Exec (l,s2)) by A10, A9, FUNCT_1:9;
(Exec (l,s1)) . (IC SCMPDS) = succ (IC s2) by A6, A80, SCMPDS_2:63
.= (Exec (l,s2)) . (IC SCMPDS) by A80, SCMPDS_2:63 ;
then (Exec (l,s1)) | {(IC SCMPDS)} = (Exec (l,s2)) | {(IC SCMPDS)} by A8, GRFUNC_1:90;
hence (Exec (l,s1)) | (SCM-Data-Loc \/ {(IC SCMPDS)}) = (Exec (l,s2)) | (SCM-Data-Loc \/ {(IC SCMPDS)}) by A86, RELAT_1:185, SCMPDS_2:100; :: thesis: verum

end;

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

then consider a, b being Int_position , k1, k2 being Integer such that
A87: l = Divide (a,k1,b,k2) by SCMPDS_2:47;
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:9;

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:72, SCMPDS_2:100
.= (s1 . (DataLoc ((s1 . a),k1))) mod (s1 . (DataLoc ((s1 . b),k2))) by A87, A89, SCMPDS_2:64
.= (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:64
.= (DataPart (Exec (l,s2))) . x by A88, FUNCT_1:72, SCMPDS_2:100 ; :: 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:72, SCMPDS_2:100
.= s1 . c by A87, A91, A93, SCMPDS_2:64
.= s2 . c by A3, Th4
.= (Exec (l,s2)) . c by A87, A92, A94, SCMPDS_2:64
.= (DataPart (Exec (l,s2))) . x by A88, FUNCT_1:72, SCMPDS_2:100 ; :: 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:72, SCMPDS_2:100
.= (s1 . (DataLoc ((s1 . a),k1))) div (s1 . (DataLoc ((s1 . b),k2))) by A87, A91, A95, SCMPDS_2:64
.= (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:64
.= (DataPart (Exec (l,s2))) . x by A88, FUNCT_1:72, SCMPDS_2:100 ; :: thesis: verum

end;

end;

end;

end;

end;

end;

then A97: DataPart (Exec (l,s1)) = DataPart (Exec (l,s2)) by A10, A9, FUNCT_1:9;
(Exec (l,s1)) . (IC SCMPDS) = succ (IC s2) by A6, A87, SCMPDS_2:64
.= (Exec (l,s2)) . (IC SCMPDS) by A87, SCMPDS_2:64 ;
then (Exec (l,s1)) | {(IC SCMPDS)} = (Exec (l,s2)) | {(IC SCMPDS)} by A8, GRFUNC_1:90;
hence (Exec (l,s1)) | (SCM-Data-Loc \/ {(IC SCMPDS)}) = (Exec (l,s2)) | (SCM-Data-Loc \/ {(IC SCMPDS)}) by A97, RELAT_1:185, SCMPDS_2:100; :: thesis: verum

end;

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

then consider a, b being Int_position , k1, k2 being Integer such that
A98: l = (a,k1) := (b,k2) by SCMPDS_2:48;
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:9;

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:72, SCMPDS_2:100
.= s1 . c by A98, A100, SCMPDS_2:59
.= (DataPart s1) . c by A99, FUNCT_1:72, SCMPDS_2:100
.= s2 . c by A3, A99, FUNCT_1:72, SCMPDS_2:100
.= (Exec (l,s2)) . c by A98, A101, SCMPDS_2:59
.= (DataPart (Exec (l,s2))) . x by A99, FUNCT_1:72, SCMPDS_2:100 ; :: 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:72, SCMPDS_2:100
.= s1 . (DataLoc ((s1 . b),k2)) by A98, A102, SCMPDS_2:59
.= s2 . (DataLoc ((s2 . b),k2)) by A3, Th3
.= (Exec (l,s2)) . c by A98, A103, SCMPDS_2:59
.= (DataPart (Exec (l,s2))) . x by A99, FUNCT_1:72, SCMPDS_2:100 ; :: thesis: verum

end;

end;

end;

then A104: DataPart (Exec (l,s1)) = DataPart (Exec (l,s2)) by A10, A9, FUNCT_1:9;
(Exec (l,s1)) . (IC SCMPDS) = succ (IC s2) by A6, A98, SCMPDS_2:59
.= (Exec (l,s2)) . (IC SCMPDS) by A98, SCMPDS_2:59 ;
then (Exec (l,s1)) | {(IC SCMPDS)} = (Exec (l,s2)) | {(IC SCMPDS)} by A8, GRFUNC_1:90;
hence (Exec (l,s1)) | (SCM-Data-Loc \/ {(IC SCMPDS)}) = (Exec (l,s2)) | (SCM-Data-Loc \/ {(IC SCMPDS)}) by A104, RELAT_1:185, SCMPDS_2:100; :: thesis: verum

end;

end;