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;