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 A1:
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 )})
A2:
DataPart s1 = DataPart s2
by A1, RELAT_1:188, SCMPDS_2:100, XBOOLE_1:7;
IC SCMPDS in {(IC SCMPDS )}
by TARSKI:def 1;
then A3:
IC SCMPDS in SCM-Data-Loc \/ {(IC SCMPDS )}
by XBOOLE_0:def 3;
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 s1
by AMI_1:79;
then A5:
IC SCMPDS in dom (s1 | (SCM-Data-Loc \/ {(IC SCMPDS )}))
by A3, RELAT_1:91;
SCM-Data-Loc \/ {(IC SCMPDS )} c= dom s2
by A4, AMI_1:79;
then A6:
IC SCMPDS in dom (s2 | (SCM-Data-Loc \/ {(IC SCMPDS )}))
by A3, RELAT_1:91;
A7: IC s1 =
(s2 | (SCM-Data-Loc \/ {(IC SCMPDS )})) . (IC SCMPDS )
by A1, A5, FUNCT_1:70
.=
IC s2
by A6, 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 )})
A8:
dom (Exec l,s1) = the carrier of SCMPDS
by AMI_1:79;
A9:
dom (Exec l,s2) = the carrier of SCMPDS
by AMI_1:79;
A10:
dom (Exec l,s1) = dom (Exec l,s2)
by A8, AMI_1:79;
A11:
dom (DataPart (Exec l,s1)) = SCM-Data-Loc
by A8, RELAT_1:91, SCMPDS_2:100;
A12:
dom (DataPart (Exec l,s2)) = SCM-Data-Loc
by A9, 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 A13:
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 A14:
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 A14, FUNCT_1:72, SCMPDS_2:100
.=
s1 . a
by A13, SCMPDS_2:66
.=
(DataPart s1) . a
by A14, FUNCT_1:72, SCMPDS_2:100
.=
s2 . a
by A2, A14, FUNCT_1:72, SCMPDS_2:100
.=
(Exec l,s2) . a
by A13, SCMPDS_2:66
.=
(DataPart (Exec l,s2)) . x
by A14, FUNCT_1:72, SCMPDS_2:100
;
:: thesis: verum
end; then A15:
(Exec l,s1) | SCM-Data-Loc = (Exec l,s2) | SCM-Data-Loc
by A11, A12, FUNCT_1:9, SCMPDS_2:100;
(Exec l,s1) . (IC SCMPDS ) =
ICplusConst s1,
k1
by A13, SCMPDS_2:66
.=
ICplusConst s2,
k1
by A7, Th2
.=
(Exec l,s2) . (IC SCMPDS )
by A13, SCMPDS_2:66
;
then
(Exec l,s1) | {(IC SCMPDS )} = (Exec l,s2) | {(IC SCMPDS )}
by A10, GRFUNC_1:90;
hence
(Exec l,s1) | (SCM-Data-Loc \/ {(IC SCMPDS )}) = (Exec l,s2) | (SCM-Data-Loc \/ {(IC SCMPDS )})
by A15, 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 A16:
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 A17:
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 A18:
b <> a
;
:: thesis: (DataPart (Exec l,s1)) . x = (DataPart (Exec l,s2)) . xthus (DataPart (Exec l,s1)) . x =
(Exec l,s1) . b
by A17, FUNCT_1:72, SCMPDS_2:100
.=
s1 . b
by A16, A18, SCMPDS_2:70
.=
(DataPart s1) . b
by A17, FUNCT_1:72, SCMPDS_2:100
.=
s2 . b
by A2, A17, FUNCT_1:72, SCMPDS_2:100
.=
(Exec l,s2) . b
by A16, A18, SCMPDS_2:70
.=
(DataPart (Exec l,s2)) . x
by A17, FUNCT_1:72, SCMPDS_2:100
;
:: thesis: verum end; suppose A19:
b = a
;
:: thesis: (DataPart (Exec l,s1)) . x = (DataPart (Exec l,s2)) . xthus (DataPart (Exec l,s1)) . x =
(Exec l,s1) . b
by A17, FUNCT_1:72, SCMPDS_2:100
.=
s1 . (DataLoc (s1 . a),RetSP )
by A16, A19, SCMPDS_2:70
.=
s2 . (DataLoc (s2 . a),RetSP )
by A2, Th3
.=
(Exec l,s2) . b
by A16, A19, SCMPDS_2:70
.=
(DataPart (Exec l,s2)) . x
by A17, FUNCT_1:72, SCMPDS_2:100
;
:: thesis: verum end;
end; then A20:
(Exec l,s1) | SCM-Data-Loc = (Exec l,s2) | SCM-Data-Loc
by A11, A12, FUNCT_1:9, SCMPDS_2:100;
(Exec l,s1) . (IC SCMPDS ) =
(abs (s1 . (DataLoc (s1 . a),RetIC ))) + 2
by A16, SCMPDS_2:70
.=
(abs (s2 . (DataLoc (s2 . a),RetIC ))) + 2
by A2, Th3
.=
(Exec l,s2) . (IC SCMPDS )
by A16, SCMPDS_2:70
;
then
(Exec l,s1) | {(IC SCMPDS )} = (Exec l,s2) | {(IC SCMPDS )}
by A10, GRFUNC_1:90;
hence
(Exec l,s1) | (SCM-Data-Loc \/ {(IC SCMPDS )}) = (Exec l,s2) | (SCM-Data-Loc \/ {(IC SCMPDS )})
by A20, 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 A21:
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 A22:
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 A23:
b <> a
;
:: thesis: (DataPart (Exec l,s1)) . x = (DataPart (Exec l,s2)) . xthus (DataPart (Exec l,s1)) . x =
(Exec l,s1) . b
by A22, FUNCT_1:72, SCMPDS_2:100
.=
s1 . b
by A21, A23, SCMPDS_2:57
.=
(DataPart s1) . b
by A22, FUNCT_1:72, SCMPDS_2:100
.=
s2 . b
by A2, A22, FUNCT_1:72, SCMPDS_2:100
.=
(Exec l,s2) . b
by A21, A23, SCMPDS_2:57
.=
(DataPart (Exec l,s2)) . x
by A22, FUNCT_1:72, SCMPDS_2:100
;
:: thesis: verum end; suppose A24:
b = a
;
:: thesis: (DataPart (Exec l,s1)) . x = (DataPart (Exec l,s2)) . xthus (DataPart (Exec l,s1)) . x =
(Exec l,s1) . b
by A22, FUNCT_1:72, SCMPDS_2:100
.=
k1
by A21, A24, SCMPDS_2:57
.=
(Exec l,s2) . b
by A21, A24, SCMPDS_2:57
.=
(DataPart (Exec l,s2)) . x
by A22, FUNCT_1:72, SCMPDS_2:100
;
:: thesis: verum end;
end; then A25:
(Exec l,s1) | SCM-Data-Loc = (Exec l,s2) | SCM-Data-Loc
by A11, A12, FUNCT_1:9, SCMPDS_2:100;
(Exec l,s1) . (IC SCMPDS ) =
Next (IC s2)
by A7, A21, SCMPDS_2:57
.=
(Exec l,s2) . (IC SCMPDS )
by A21, SCMPDS_2:57
;
then
(Exec l,s1) | {(IC SCMPDS )} = (Exec l,s2) | {(IC SCMPDS )}
by A10, GRFUNC_1:90;
hence
(Exec l,s1) | (SCM-Data-Loc \/ {(IC SCMPDS )}) = (Exec l,s2) | (SCM-Data-Loc \/ {(IC SCMPDS )})
by A25, 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 A26:
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 A27:
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 A28:
b <> DataLoc (s1 . a),
k1
;
:: thesis: (DataPart (Exec l,s1)) . x = (DataPart (Exec l,s2)) . xthen A29:
b <> DataLoc (s2 . a),
k1
by A2, Th4;
thus (DataPart (Exec l,s1)) . x =
(Exec l,s1) . b
by A27, FUNCT_1:72, SCMPDS_2:100
.=
s1 . b
by A26, A28, SCMPDS_2:71
.=
(DataPart s1) . b
by A27, FUNCT_1:72, SCMPDS_2:100
.=
s2 . b
by A2, A27, FUNCT_1:72, SCMPDS_2:100
.=
(Exec l,s2) . b
by A26, A29, SCMPDS_2:71
.=
(DataPart (Exec l,s2)) . x
by A27, FUNCT_1:72, SCMPDS_2:100
;
:: thesis: verum end; suppose A30:
b = DataLoc (s1 . a),
k1
;
:: thesis: (DataPart (Exec l,s1)) . x = (DataPart (Exec l,s2)) . xthen A31:
b = DataLoc (s2 . a),
k1
by A2, Th4;
thus (DataPart (Exec l,s1)) . x =
(Exec l,s1) . b
by A27, FUNCT_1:72, SCMPDS_2:100
.=
IC s2
by A7, A26, A30, SCMPDS_2:71
.=
(Exec l,s2) . b
by A26, A31, SCMPDS_2:71
.=
(DataPart (Exec l,s2)) . x
by A27, FUNCT_1:72, SCMPDS_2:100
;
:: thesis: verum end;
end; then A32:
(Exec l,s1) | SCM-Data-Loc = (Exec l,s2) | SCM-Data-Loc
by A11, A12, FUNCT_1:9, SCMPDS_2:100;
(Exec l,s1) . (IC SCMPDS ) =
Next (IC s2)
by A7, A26, SCMPDS_2:71
.=
(Exec l,s2) . (IC SCMPDS )
by A26, SCMPDS_2:71
;
then
(Exec l,s1) | {(IC SCMPDS )} = (Exec l,s2) | {(IC SCMPDS )}
by A10, GRFUNC_1:90;
hence
(Exec l,s1) | (SCM-Data-Loc \/ {(IC SCMPDS )}) = (Exec l,s2) | (SCM-Data-Loc \/ {(IC SCMPDS )})
by A32, 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 A33:
l = a,
k1 <>0_goto 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 A34:
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 A34, FUNCT_1:72, SCMPDS_2:100
.=
s1 . b
by A33, SCMPDS_2:67
.=
(DataPart s1) . b
by A34, FUNCT_1:72, SCMPDS_2:100
.=
s2 . b
by A2, A34, FUNCT_1:72, SCMPDS_2:100
.=
(Exec l,s2) . b
by A33, SCMPDS_2:67
.=
(DataPart (Exec l,s2)) . x
by A34, FUNCT_1:72, SCMPDS_2:100
;
:: thesis: verum
end; then A35:
(Exec l,s1) | SCM-Data-Loc = (Exec l,s2) | SCM-Data-Loc
by A11, A12, FUNCT_1:9, SCMPDS_2:100;
now per cases
( s1 . (DataLoc (s1 . a),k1) <> 0 or s1 . (DataLoc (s1 . a),k1) = 0 )
;
suppose A36:
s1 . (DataLoc (s1 . a),k1) <> 0
;
:: thesis: (Exec l,s1) . (IC SCMPDS ) = (Exec l,s2) . (IC SCMPDS )then A37:
s2 . (DataLoc (s2 . a),k1) <> 0
by A2, Th3;
thus (Exec l,s1) . (IC SCMPDS ) =
ICplusConst s1,
k2
by A33, A36, SCMPDS_2:67
.=
ICplusConst s2,
k2
by A7, Th2
.=
(Exec l,s2) . (IC SCMPDS )
by A33, A37, SCMPDS_2:67
;
:: thesis: verum end; then
(Exec l,s1) | {(IC SCMPDS )} = (Exec l,s2) | {(IC SCMPDS )}
by A10, GRFUNC_1:90;
hence
(Exec l,s1) | (SCM-Data-Loc \/ {(IC SCMPDS )}) = (Exec l,s2) | (SCM-Data-Loc \/ {(IC SCMPDS )})
by A35, 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 A40:
l = a,
k1 <=0_goto k2
by SCMPDS_2:40;
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 A41:
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 A41, FUNCT_1:72, SCMPDS_2:100
.=
s1 . b
by A40, SCMPDS_2:68
.=
(DataPart s1) . b
by A41, FUNCT_1:72, SCMPDS_2:100
.=
s2 . b
by A2, A41, FUNCT_1:72, SCMPDS_2:100
.=
(Exec l,s2) . b
by A40, SCMPDS_2:68
.=
(DataPart (Exec l,s2)) . x
by A41, FUNCT_1:72, SCMPDS_2:100
;
:: thesis: verum
end; then A42:
(Exec l,s1) | SCM-Data-Loc = (Exec l,s2) | SCM-Data-Loc
by A11, A12, FUNCT_1:9, SCMPDS_2:100;
now per cases
( s1 . (DataLoc (s1 . a),k1) <= 0 or s1 . (DataLoc (s1 . a),k1) > 0 )
;
suppose A43:
s1 . (DataLoc (s1 . a),k1) <= 0
;
:: thesis: (Exec l,s1) . (IC SCMPDS ) = (Exec l,s2) . (IC SCMPDS )then A44:
s2 . (DataLoc (s2 . a),k1) <= 0
by A2, Th3;
thus (Exec l,s1) . (IC SCMPDS ) =
ICplusConst s1,
k2
by A40, A43, SCMPDS_2:68
.=
ICplusConst s2,
k2
by A7, Th2
.=
(Exec l,s2) . (IC SCMPDS )
by A40, A44, SCMPDS_2:68
;
:: thesis: verum end; then
(Exec l,s1) | {(IC SCMPDS )} = (Exec l,s2) | {(IC SCMPDS )}
by A10, GRFUNC_1:90;
hence
(Exec l,s1) | (SCM-Data-Loc \/ {(IC SCMPDS )}) = (Exec l,s2) | (SCM-Data-Loc \/ {(IC SCMPDS )})
by A42, 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 A47:
l = a,
k1 >=0_goto k2
by SCMPDS_2:41;
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 A48:
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 A48, FUNCT_1:72, SCMPDS_2:100
.=
s1 . b
by A47, SCMPDS_2:69
.=
(DataPart s1) . b
by A48, FUNCT_1:72, SCMPDS_2:100
.=
s2 . b
by A2, A48, FUNCT_1:72, SCMPDS_2:100
.=
(Exec l,s2) . b
by A47, SCMPDS_2:69
.=
(DataPart (Exec l,s2)) . x
by A48, FUNCT_1:72, SCMPDS_2:100
;
:: thesis: verum
end; then A49:
(Exec l,s1) | SCM-Data-Loc = (Exec l,s2) | SCM-Data-Loc
by A11, A12, FUNCT_1:9, SCMPDS_2:100;
now per cases
( s1 . (DataLoc (s1 . a),k1) >= 0 or s1 . (DataLoc (s1 . a),k1) < 0 )
;
suppose A50:
s1 . (DataLoc (s1 . a),k1) >= 0
;
:: thesis: (Exec l,s1) . (IC SCMPDS ) = (Exec l,s2) . (IC SCMPDS )then A51:
s2 . (DataLoc (s2 . a),k1) >= 0
by A2, Th3;
thus (Exec l,s1) . (IC SCMPDS ) =
ICplusConst s1,
k2
by A47, A50, SCMPDS_2:69
.=
ICplusConst s2,
k2
by A7, Th2
.=
(Exec l,s2) . (IC SCMPDS )
by A47, A51, SCMPDS_2:69
;
:: thesis: verum end; then
(Exec l,s1) | {(IC SCMPDS )} = (Exec l,s2) | {(IC SCMPDS )}
by A10, GRFUNC_1:90;
hence
(Exec l,s1) | (SCM-Data-Loc \/ {(IC SCMPDS )}) = (Exec l,s2) | (SCM-Data-Loc \/ {(IC SCMPDS )})
by A49, 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 A54:
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 A55:
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 A56:
b <> DataLoc (s1 . a),
k1
;
:: thesis: (DataPart (Exec l,s1)) . x = (DataPart (Exec l,s2)) . xthen A57:
b <> DataLoc (s2 . a),
k1
by A2, Th4;
thus (DataPart (Exec l,s1)) . x =
(Exec l,s1) . b
by A55, FUNCT_1:72, SCMPDS_2:100
.=
s1 . b
by A54, A56, SCMPDS_2:58
.=
(DataPart s1) . b
by A55, FUNCT_1:72, SCMPDS_2:100
.=
s2 . b
by A2, A55, FUNCT_1:72, SCMPDS_2:100
.=
(Exec l,s2) . b
by A54, A57, SCMPDS_2:58
.=
(DataPart (Exec l,s2)) . x
by A55, FUNCT_1:72, SCMPDS_2:100
;
:: thesis: verum end; suppose A58:
b = DataLoc (s1 . a),
k1
;
:: thesis: (DataPart (Exec l,s1)) . x = (DataPart (Exec l,s2)) . xthen A59:
b = DataLoc (s2 . a),
k1
by A2, Th4;
thus (DataPart (Exec l,s1)) . x =
(Exec l,s1) . b
by A55, FUNCT_1:72, SCMPDS_2:100
.=
k2
by A54, A58, SCMPDS_2:58
.=
(Exec l,s2) . b
by A54, A59, SCMPDS_2:58
.=
(DataPart (Exec l,s2)) . x
by A55, FUNCT_1:72, SCMPDS_2:100
;
:: thesis: verum end;
end; then A60:
(Exec l,s1) | SCM-Data-Loc = (Exec l,s2) | SCM-Data-Loc
by A11, A12, FUNCT_1:9, SCMPDS_2:100;
(Exec l,s1) . (IC SCMPDS ) =
Next (IC s2)
by A7, A54, SCMPDS_2:58
.=
(Exec l,s2) . (IC SCMPDS )
by A54, SCMPDS_2:58
;
then
(Exec l,s1) | {(IC SCMPDS )} = (Exec l,s2) | {(IC SCMPDS )}
by A10, GRFUNC_1:90;
hence
(Exec l,s1) | (SCM-Data-Loc \/ {(IC SCMPDS )}) = (Exec l,s2) | (SCM-Data-Loc \/ {(IC SCMPDS )})
by A60, 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 A61:
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 A62:
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 A63:
b <> DataLoc (s1 . a),
k1
;
:: thesis: (DataPart (Exec l,s1)) . x = (DataPart (Exec l,s2)) . xthen A64:
b <> DataLoc (s2 . a),
k1
by A2, Th4;
thus (DataPart (Exec l,s1)) . x =
(Exec l,s1) . b
by A62, FUNCT_1:72, SCMPDS_2:100
.=
s1 . b
by A61, A63, SCMPDS_2:60
.=
(DataPart s1) . b
by A62, FUNCT_1:72, SCMPDS_2:100
.=
s2 . b
by A2, A62, FUNCT_1:72, SCMPDS_2:100
.=
(Exec l,s2) . b
by A61, A64, SCMPDS_2:60
.=
(DataPart (Exec l,s2)) . x
by A62, FUNCT_1:72, SCMPDS_2:100
;
:: thesis: verum end; suppose A65:
b = DataLoc (s1 . a),
k1
;
:: thesis: (DataPart (Exec l,s1)) . x = (DataPart (Exec l,s2)) . xthen A66:
b = DataLoc (s2 . a),
k1
by A2, Th4;
thus (DataPart (Exec l,s1)) . x =
(Exec l,s1) . b
by A62, FUNCT_1:72, SCMPDS_2:100
.=
(s1 . (DataLoc (s1 . a),k1)) + k2
by A61, A65, SCMPDS_2:60
.=
(s2 . (DataLoc (s2 . a),k1)) + k2
by A2, Th3
.=
(Exec l,s2) . b
by A61, A66, SCMPDS_2:60
.=
(DataPart (Exec l,s2)) . x
by A62, FUNCT_1:72, SCMPDS_2:100
;
:: thesis: verum end;
end; then A67:
(Exec l,s1) | SCM-Data-Loc = (Exec l,s2) | SCM-Data-Loc
by A11, A12, FUNCT_1:9, SCMPDS_2:100;
(Exec l,s1) . (IC SCMPDS ) =
Next (IC s2)
by A7, A61, SCMPDS_2:60
.=
(Exec l,s2) . (IC SCMPDS )
by A61, SCMPDS_2:60
;
then
(Exec l,s1) | {(IC SCMPDS )} = (Exec l,s2) | {(IC SCMPDS )}
by A10, GRFUNC_1:90;
hence
(Exec l,s1) | (SCM-Data-Loc \/ {(IC SCMPDS )}) = (Exec l,s2) | (SCM-Data-Loc \/ {(IC SCMPDS )})
by A67, 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 A68:
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 A69:
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 A70:
c <> DataLoc (s1 . a),
k1
;
:: thesis: (DataPart (Exec l,s1)) . x = (DataPart (Exec l,s2)) . xthen A71:
c <> DataLoc (s2 . a),
k1
by A2, Th4;
thus (DataPart (Exec l,s1)) . x =
(Exec l,s1) . c
by A69, FUNCT_1:72, SCMPDS_2:100
.=
s1 . c
by A68, A70, SCMPDS_2:61
.=
(DataPart s1) . c
by A69, FUNCT_1:72, SCMPDS_2:100
.=
s2 . c
by A2, A69, FUNCT_1:72, SCMPDS_2:100
.=
(Exec l,s2) . c
by A68, A71, SCMPDS_2:61
.=
(DataPart (Exec l,s2)) . x
by A69, FUNCT_1:72, SCMPDS_2:100
;
:: thesis: verum end; suppose A72:
c = DataLoc (s1 . a),
k1
;
:: thesis: (DataPart (Exec l,s1)) . x = (DataPart (Exec l,s2)) . xthen A73:
c = DataLoc (s2 . a),
k1
by A2, Th4;
thus (DataPart (Exec l,s1)) . x =
(Exec l,s1) . c
by A69, FUNCT_1:72, SCMPDS_2:100
.=
(s1 . (DataLoc (s1 . a),k1)) + (s1 . (DataLoc (s1 . b),k2))
by A68, A72, SCMPDS_2:61
.=
(s2 . (DataLoc (s2 . a),k1)) + (s1 . (DataLoc (s1 . b),k2))
by A2, Th3
.=
(s2 . (DataLoc (s2 . a),k1)) + (s2 . (DataLoc (s2 . b),k2))
by A2, Th3
.=
(Exec l,s2) . c
by A68, A73, SCMPDS_2:61
.=
(DataPart (Exec l,s2)) . x
by A69, FUNCT_1:72, SCMPDS_2:100
;
:: thesis: verum end;
end; then A74:
(Exec l,s1) | SCM-Data-Loc = (Exec l,s2) | SCM-Data-Loc
by A11, A12, FUNCT_1:9, SCMPDS_2:100;
(Exec l,s1) . (IC SCMPDS ) =
Next (IC s2)
by A7, A68, SCMPDS_2:61
.=
(Exec l,s2) . (IC SCMPDS )
by A68, SCMPDS_2:61
;
then
(Exec l,s1) | {(IC SCMPDS )} = (Exec l,s2) | {(IC SCMPDS )}
by A10, GRFUNC_1:90;
hence
(Exec l,s1) | (SCM-Data-Loc \/ {(IC SCMPDS )}) = (Exec l,s2) | (SCM-Data-Loc \/ {(IC SCMPDS )})
by A74, 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 A75:
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 A76:
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 A77:
c <> DataLoc (s1 . a),
k1
;
:: thesis: (DataPart (Exec l,s1)) . x = (DataPart (Exec l,s2)) . xthen A78:
c <> DataLoc (s2 . a),
k1
by A2, Th4;
thus (DataPart (Exec l,s1)) . x =
(Exec l,s1) . c
by A76, FUNCT_1:72, SCMPDS_2:100
.=
s1 . c
by A75, A77, SCMPDS_2:62
.=
(DataPart s1) . c
by A76, FUNCT_1:72, SCMPDS_2:100
.=
s2 . c
by A2, A76, FUNCT_1:72, SCMPDS_2:100
.=
(Exec l,s2) . c
by A75, A78, SCMPDS_2:62
.=
(DataPart (Exec l,s2)) . x
by A76, FUNCT_1:72, SCMPDS_2:100
;
:: thesis: verum end; suppose A79:
c = DataLoc (s1 . a),
k1
;
:: thesis: (DataPart (Exec l,s1)) . x = (DataPart (Exec l,s2)) . xthen A80:
c = DataLoc (s2 . a),
k1
by A2, Th4;
thus (DataPart (Exec l,s1)) . x =
(Exec l,s1) . c
by A76, FUNCT_1:72, SCMPDS_2:100
.=
(s1 . (DataLoc (s1 . a),k1)) - (s1 . (DataLoc (s1 . b),k2))
by A75, A79, SCMPDS_2:62
.=
(s2 . (DataLoc (s2 . a),k1)) - (s1 . (DataLoc (s1 . b),k2))
by A2, Th3
.=
(s2 . (DataLoc (s2 . a),k1)) - (s2 . (DataLoc (s2 . b),k2))
by A2, Th3
.=
(Exec l,s2) . c
by A75, A80, SCMPDS_2:62
.=
(DataPart (Exec l,s2)) . x
by A76, FUNCT_1:72, SCMPDS_2:100
;
:: thesis: verum end;
end; then A81:
DataPart (Exec l,s1) = DataPart (Exec l,s2)
by A11, A12, FUNCT_1:9;
(Exec l,s1) . (IC SCMPDS ) =
Next (IC s2)
by A7, A75, SCMPDS_2:62
.=
(Exec l,s2) . (IC SCMPDS )
by A75, SCMPDS_2:62
;
then
(Exec l,s1) | {(IC SCMPDS )} = (Exec l,s2) | {(IC SCMPDS )}
by A10, GRFUNC_1:90;
hence
(Exec l,s1) | (SCM-Data-Loc \/ {(IC SCMPDS )}) = (Exec l,s2) | (SCM-Data-Loc \/ {(IC SCMPDS )})
by A81, 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 A82:
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 A83:
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 A84:
c <> DataLoc (s1 . a),
k1
;
:: thesis: (DataPart (Exec l,s1)) . x = (DataPart (Exec l,s2)) . xthen A85:
c <> DataLoc (s2 . a),
k1
by A2, Th4;
thus (DataPart (Exec l,s1)) . x =
(Exec l,s1) . c
by A83, FUNCT_1:72, SCMPDS_2:100
.=
s1 . c
by A82, A84, SCMPDS_2:63
.=
(DataPart s1) . c
by A83, FUNCT_1:72, SCMPDS_2:100
.=
s2 . c
by A2, A83, FUNCT_1:72, SCMPDS_2:100
.=
(Exec l,s2) . c
by A82, A85, SCMPDS_2:63
.=
(DataPart (Exec l,s2)) . x
by A83, FUNCT_1:72, SCMPDS_2:100
;
:: thesis: verum end; suppose A86:
c = DataLoc (s1 . a),
k1
;
:: thesis: (DataPart (Exec l,s1)) . x = (DataPart (Exec l,s2)) . xthen A87:
c = DataLoc (s2 . a),
k1
by A2, Th4;
thus (DataPart (Exec l,s1)) . x =
(Exec l,s1) . c
by A83, FUNCT_1:72, SCMPDS_2:100
.=
(s1 . (DataLoc (s1 . a),k1)) * (s1 . (DataLoc (s1 . b),k2))
by A82, A86, SCMPDS_2:63
.=
(s2 . (DataLoc (s2 . a),k1)) * (s1 . (DataLoc (s1 . b),k2))
by A2, Th3
.=
(s2 . (DataLoc (s2 . a),k1)) * (s2 . (DataLoc (s2 . b),k2))
by A2, Th3
.=
(Exec l,s2) . c
by A82, A87, SCMPDS_2:63
.=
(DataPart (Exec l,s2)) . x
by A83, FUNCT_1:72, SCMPDS_2:100
;
:: thesis: verum end;
end; then A88:
DataPart (Exec l,s1) = DataPart (Exec l,s2)
by A11, A12, FUNCT_1:9;
(Exec l,s1) . (IC SCMPDS ) =
Next (IC s2)
by A7, A82, SCMPDS_2:63
.=
(Exec l,s2) . (IC SCMPDS )
by A82, SCMPDS_2:63
;
then
(Exec l,s1) | {(IC SCMPDS )} = (Exec l,s2) | {(IC SCMPDS )}
by A10, GRFUNC_1:90;
hence
(Exec l,s1) | (SCM-Data-Loc \/ {(IC SCMPDS )}) = (Exec l,s2) | (SCM-Data-Loc \/ {(IC SCMPDS )})
by A88, 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 A89:
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 A90:
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 A91:
c = DataLoc (s1 . b),
k2
;
:: thesis: (DataPart (Exec l,s1)) . x = (DataPart (Exec l,s2)) . xthen A92:
c = DataLoc (s2 . b),
k2
by A2, Th4;
thus (DataPart (Exec l,s1)) . x =
(Exec l,s1) . c
by A90, FUNCT_1:72, SCMPDS_2:100
.=
(s1 . (DataLoc (s1 . a),k1)) mod (s1 . (DataLoc (s1 . b),k2))
by A89, A91, SCMPDS_2:64
.=
(s2 . (DataLoc (s2 . a),k1)) mod (s1 . (DataLoc (s1 . b),k2))
by A2, Th3
.=
(s2 . (DataLoc (s2 . a),k1)) mod (s2 . (DataLoc (s2 . b),k2))
by A2, Th3
.=
(Exec l,s2) . c
by A89, A92, SCMPDS_2:64
.=
(DataPart (Exec l,s2)) . x
by A90, FUNCT_1:72, SCMPDS_2:100
;
:: thesis: verum end; suppose A93:
c <> DataLoc (s1 . b),
k2
;
:: thesis: (DataPart (Exec l,s1)) . x = (DataPart (Exec l,s2)) . xthen A94:
c <> DataLoc (s2 . b),
k2
by A2, Th4;
hereby :: thesis: verum
per cases
( c <> DataLoc (s1 . a),k1 or c = DataLoc (s1 . a),k1 )
;
suppose A95:
c <> DataLoc (s1 . a),
k1
;
:: thesis: (DataPart (Exec l,s1)) . x = (DataPart (Exec l,s2)) . xthen A96:
c <> DataLoc (s2 . a),
k1
by A2, Th4;
thus (DataPart (Exec l,s1)) . x =
(Exec l,s1) . c
by A90, FUNCT_1:72, SCMPDS_2:100
.=
s1 . c
by A89, A93, A95, SCMPDS_2:64
.=
s2 . c
by A2, Th4
.=
(Exec l,s2) . c
by A89, A94, A96, SCMPDS_2:64
.=
(DataPart (Exec l,s2)) . x
by A90, FUNCT_1:72, SCMPDS_2:100
;
:: thesis: verum end; suppose A97:
c = DataLoc (s1 . a),
k1
;
:: thesis: (DataPart (Exec l,s1)) . x = (DataPart (Exec l,s2)) . xthen A98:
c = DataLoc (s2 . a),
k1
by A2, Th4;
thus (DataPart (Exec l,s1)) . x =
(Exec l,s1) . c
by A90, FUNCT_1:72, SCMPDS_2:100
.=
(s1 . (DataLoc (s1 . a),k1)) div (s1 . (DataLoc (s1 . b),k2))
by A89, A93, A97, SCMPDS_2:64
.=
(s2 . (DataLoc (s2 . a),k1)) div (s1 . (DataLoc (s1 . b),k2))
by A2, Th3
.=
(s2 . (DataLoc (s2 . a),k1)) div (s2 . (DataLoc (s2 . b),k2))
by A2, Th3
.=
(Exec l,s2) . c
by A89, A94, A98, SCMPDS_2:64
.=
(DataPart (Exec l,s2)) . x
by A90, FUNCT_1:72, SCMPDS_2:100
;
:: thesis: verum end; end;
end; then A99:
DataPart (Exec l,s1) = DataPart (Exec l,s2)
by A11, A12, FUNCT_1:9;
(Exec l,s1) . (IC SCMPDS ) =
Next (IC s2)
by A7, A89, SCMPDS_2:64
.=
(Exec l,s2) . (IC SCMPDS )
by A89, SCMPDS_2:64
;
then
(Exec l,s1) | {(IC SCMPDS )} = (Exec l,s2) | {(IC SCMPDS )}
by A10, GRFUNC_1:90;
hence
(Exec l,s1) | (SCM-Data-Loc \/ {(IC SCMPDS )}) = (Exec l,s2) | (SCM-Data-Loc \/ {(IC SCMPDS )})
by A99, 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 A100:
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 A101:
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 A102:
c <> DataLoc (s1 . a),
k1
;
:: thesis: (DataPart (Exec l,s1)) . x = (DataPart (Exec l,s2)) . xthen A103:
c <> DataLoc (s2 . a),
k1
by A2, Th4;
thus (DataPart (Exec l,s1)) . x =
(Exec l,s1) . c
by A101, FUNCT_1:72, SCMPDS_2:100
.=
s1 . c
by A100, A102, SCMPDS_2:59
.=
(DataPart s1) . c
by A101, FUNCT_1:72, SCMPDS_2:100
.=
s2 . c
by A2, A101, FUNCT_1:72, SCMPDS_2:100
.=
(Exec l,s2) . c
by A100, A103, SCMPDS_2:59
.=
(DataPart (Exec l,s2)) . x
by A101, FUNCT_1:72, SCMPDS_2:100
;
:: thesis: verum end; suppose A104:
c = DataLoc (s1 . a),
k1
;
:: thesis: (DataPart (Exec l,s1)) . x = (DataPart (Exec l,s2)) . xthen A105:
c = DataLoc (s2 . a),
k1
by A2, Th4;
thus (DataPart (Exec l,s1)) . x =
(Exec l,s1) . c
by A101, FUNCT_1:72, SCMPDS_2:100
.=
s1 . (DataLoc (s1 . b),k2)
by A100, A104, SCMPDS_2:59
.=
s2 . (DataLoc (s2 . b),k2)
by A2, Th3
.=
(Exec l,s2) . c
by A100, A105, SCMPDS_2:59
.=
(DataPart (Exec l,s2)) . x
by A101, FUNCT_1:72, SCMPDS_2:100
;
:: thesis: verum end;
end; then A106:
DataPart (Exec l,s1) = DataPart (Exec l,s2)
by A11, A12, FUNCT_1:9;
(Exec l,s1) . (IC SCMPDS ) =
Next (IC s2)
by A7, A100, SCMPDS_2:59
.=
(Exec l,s2) . (IC SCMPDS )
by A100, SCMPDS_2:59
;
then
(Exec l,s1) | {(IC SCMPDS )} = (Exec l,s2) | {(IC SCMPDS )}
by A10, GRFUNC_1:90;
hence
(Exec l,s1) | (SCM-Data-Loc \/ {(IC SCMPDS )}) = (Exec l,s2) | (SCM-Data-Loc \/ {(IC SCMPDS )})
by A106, RELAT_1:185, SCMPDS_2:100;
:: thesis: verum end;