let s1, s2 be State of SCM ; :: thesis: ( s1 | (SCM-Data-Loc \/ {(IC SCM )}) = s2 | (SCM-Data-Loc \/ {(IC SCM )}) implies for l being Instruction of SCM holds (Exec l,s1) | (SCM-Data-Loc \/ {(IC SCM )}) = (Exec l,s2) | (SCM-Data-Loc \/ {(IC SCM )}) )
assume A1:
s1 | (SCM-Data-Loc \/ {(IC SCM )}) = s2 | (SCM-Data-Loc \/ {(IC SCM )})
; :: thesis: for l being Instruction of SCM holds (Exec l,s1) | (SCM-Data-Loc \/ {(IC SCM )}) = (Exec l,s2) | (SCM-Data-Loc \/ {(IC SCM )})
IC SCM in {(IC SCM )}
by TARSKI:def 1;
then A2:
IC SCM in SCM-Data-Loc \/ {(IC SCM )}
by XBOOLE_0:def 3;
A3:
SCM-Data-Loc \/ {(IC SCM )} c= the carrier of SCM
by AMI_3:4, XBOOLE_1:7;
then
SCM-Data-Loc \/ {(IC SCM )} c= dom s1
by AMI_1:79;
then A4:
IC SCM in dom (s1 | (SCM-Data-Loc \/ {(IC SCM )}))
by A2, RELAT_1:91;
SCM-Data-Loc \/ {(IC SCM )} c= dom s2
by A3, AMI_1:79;
then A5:
IC SCM in dom (s2 | (SCM-Data-Loc \/ {(IC SCM )}))
by A2, RELAT_1:91;
A6: IC s1 =
(s2 | (SCM-Data-Loc \/ {(IC SCM )})) . (IC SCM )
by A1, A4, FUNCT_1:70
.=
IC s2
by A5, FUNCT_1:70
;
let l be Instruction of SCM ; :: thesis: (Exec l,s1) | (SCM-Data-Loc \/ {(IC SCM )}) = (Exec l,s2) | (SCM-Data-Loc \/ {(IC SCM )})
A7:
dom (Exec l,s1) = the carrier of SCM
by AMI_1:79;
A8:
dom (Exec l,s2) = the carrier of SCM
by AMI_1:79;
A9:
SCM-Data-Loc c= SCM-Data-Loc \/ {(IC SCM )}
by XBOOLE_1:7;
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 )
by Th36, NAT_1:33;
suppose
InsCode l = 1
;
:: thesis: (Exec l,s1) | (SCM-Data-Loc \/ {(IC SCM )}) = (Exec l,s2) | (SCM-Data-Loc \/ {(IC SCM )})then consider da,
db being
Data-Location such that A11:
l = da := db
by Th47;
da in SCM-Data-Loc
by AMI_3:def 2;
then A12:
SCM-Data-Loc =
SCM-Data-Loc \/ {da}
by ZFMISC_1:46
.=
(SCM-Data-Loc \ {da}) \/ {da}
by XBOOLE_1:39
;
A13:
dom ((Exec l,s1) | (SCM-Data-Loc \ {da})) = SCM-Data-Loc \ {da}
by A7, RELAT_1:91;
A14:
dom ((Exec l,s2) | (SCM-Data-Loc \ {da})) = SCM-Data-Loc \ {da}
by A8, RELAT_1:91;
for
x being
set st
x in SCM-Data-Loc \ {da} holds
((Exec l,s1) | (SCM-Data-Loc \ {da})) . x = ((Exec l,s2) | (SCM-Data-Loc \ {da})) . x
proof
let x be
set ;
:: thesis: ( x in SCM-Data-Loc \ {da} implies ((Exec l,s1) | (SCM-Data-Loc \ {da})) . x = ((Exec l,s2) | (SCM-Data-Loc \ {da})) . x )
assume A15:
x in SCM-Data-Loc \ {da}
;
:: thesis: ((Exec l,s1) | (SCM-Data-Loc \ {da})) . x = ((Exec l,s2) | (SCM-Data-Loc \ {da})) . x
then A16:
x in SCM-Data-Loc
by XBOOLE_0:def 5;
A17:
not
x in {da}
by A15, XBOOLE_0:def 5;
reconsider a =
x as
Data-Location by A16, AMI_3:def 2;
A18:
a <> da
by A17, TARSKI:def 1;
A19:
a in SCM-Data-Loc \/ {(IC SCM )}
by A16, XBOOLE_0:def 3;
thus ((Exec l,s1) | (SCM-Data-Loc \ {da})) . x =
(Exec l,s1) . a
by A15, FUNCT_1:72
.=
s1 . a
by A11, A18, AMI_3:8
.=
(s1 | (SCM-Data-Loc \/ {(IC SCM )})) . a
by A19, FUNCT_1:72
.=
s2 . a
by A1, A19, FUNCT_1:72
.=
(Exec l,s2) . a
by A11, A18, AMI_3:8
.=
((Exec l,s2) | (SCM-Data-Loc \ {da})) . x
by A15, FUNCT_1:72
;
:: thesis: verum
end; then A20:
(Exec l,s1) | (SCM-Data-Loc \ {da}) = (Exec l,s2) | (SCM-Data-Loc \ {da})
by A13, A14, FUNCT_1:9;
A21:
db in SCM-Data-Loc
by AMI_3:def 2;
(Exec l,s1) . da =
s1 . db
by A11, AMI_3:8
.=
(s1 | (SCM-Data-Loc \/ {(IC SCM )})) . db
by A9, A21, FUNCT_1:72
.=
s2 . db
by A1, A9, A21, FUNCT_1:72
.=
(Exec l,s2) . da
by A11, AMI_3:8
;
then
(Exec l,s1) | {da} = (Exec l,s2) | {da}
by A7, A8, GRFUNC_1:90;
then A22:
DataPart (Exec l,s1) = DataPart (Exec l,s2)
by A12, A20, AMI_3:72, RELAT_1:185;
(Exec l,s1) . (IC SCM ) =
Next (IC s1)
by A11, AMI_3:8
.=
(Exec l,s2) . (IC SCM )
by A6, A11, AMI_3:8
;
then
(Exec l,s1) | {(IC SCM )} = (Exec l,s2) | {(IC SCM )}
by A7, A8, GRFUNC_1:90;
hence
(Exec l,s1) | (SCM-Data-Loc \/ {(IC SCM )}) = (Exec l,s2) | (SCM-Data-Loc \/ {(IC SCM )})
by A22, AMI_3:72, RELAT_1:185;
:: thesis: verum end; suppose
InsCode l = 2
;
:: thesis: (Exec l,s1) | (SCM-Data-Loc \/ {(IC SCM )}) = (Exec l,s2) | (SCM-Data-Loc \/ {(IC SCM )})then consider da,
db being
Data-Location such that A23:
l = AddTo da,
db
by Th48;
da in SCM-Data-Loc
by AMI_3:def 2;
then A24:
SCM-Data-Loc =
SCM-Data-Loc \/ {da}
by ZFMISC_1:46
.=
(SCM-Data-Loc \ {da}) \/ {da}
by XBOOLE_1:39
;
A25:
dom ((Exec l,s1) | (SCM-Data-Loc \ {da})) = SCM-Data-Loc \ {da}
by A7, RELAT_1:91;
A26:
dom ((Exec l,s2) | (SCM-Data-Loc \ {da})) = SCM-Data-Loc \ {da}
by A8, RELAT_1:91;
for
x being
set st
x in SCM-Data-Loc \ {da} holds
((Exec l,s1) | (SCM-Data-Loc \ {da})) . x = ((Exec l,s2) | (SCM-Data-Loc \ {da})) . x
proof
let x be
set ;
:: thesis: ( x in SCM-Data-Loc \ {da} implies ((Exec l,s1) | (SCM-Data-Loc \ {da})) . x = ((Exec l,s2) | (SCM-Data-Loc \ {da})) . x )
assume A27:
x in SCM-Data-Loc \ {da}
;
:: thesis: ((Exec l,s1) | (SCM-Data-Loc \ {da})) . x = ((Exec l,s2) | (SCM-Data-Loc \ {da})) . x
then A28:
x in SCM-Data-Loc
by XBOOLE_0:def 5;
A29:
not
x in {da}
by A27, XBOOLE_0:def 5;
reconsider a =
x as
Data-Location by A28, AMI_3:def 2;
A30:
a <> da
by A29, TARSKI:def 1;
A31:
a in SCM-Data-Loc \/ {(IC SCM )}
by A28, XBOOLE_0:def 3;
thus ((Exec l,s1) | (SCM-Data-Loc \ {da})) . x =
(Exec l,s1) . a
by A27, FUNCT_1:72
.=
s1 . a
by A23, A30, AMI_3:9
.=
(s1 | (SCM-Data-Loc \/ {(IC SCM )})) . a
by A31, FUNCT_1:72
.=
s2 . a
by A1, A31, FUNCT_1:72
.=
(Exec l,s2) . a
by A23, A30, AMI_3:9
.=
((Exec l,s2) | (SCM-Data-Loc \ {da})) . x
by A27, FUNCT_1:72
;
:: thesis: verum
end; then A32:
(Exec l,s1) | (SCM-Data-Loc \ {da}) = (Exec l,s2) | (SCM-Data-Loc \ {da})
by A25, A26, FUNCT_1:9;
A33:
db in SCM-Data-Loc
by AMI_3:def 2;
A34:
da in SCM-Data-Loc
by AMI_3:def 2;
then A35:
s1 . da =
(s1 | (SCM-Data-Loc \/ {(IC SCM )})) . da
by A9, FUNCT_1:72
.=
s2 . da
by A1, A9, A34, FUNCT_1:72
;
A36:
s1 . db =
(s1 | (SCM-Data-Loc \/ {(IC SCM )})) . db
by A9, A33, FUNCT_1:72
.=
s2 . db
by A1, A9, A33, FUNCT_1:72
;
(Exec l,s1) . da =
(s1 . da) + (s1 . db)
by A23, AMI_3:9
.=
(Exec l,s2) . da
by A23, A35, A36, AMI_3:9
;
then
(Exec l,s1) | {da} = (Exec l,s2) | {da}
by A7, A8, GRFUNC_1:90;
then A37:
DataPart (Exec l,s1) = DataPart (Exec l,s2)
by A24, A32, AMI_3:72, RELAT_1:185;
(Exec l,s1) . (IC SCM ) =
Next (IC s1)
by A23, AMI_3:9
.=
(Exec l,s2) . (IC SCM )
by A6, A23, AMI_3:9
;
then
(Exec l,s1) | {(IC SCM )} = (Exec l,s2) | {(IC SCM )}
by A7, A8, GRFUNC_1:90;
hence
(Exec l,s1) | (SCM-Data-Loc \/ {(IC SCM )}) = (Exec l,s2) | (SCM-Data-Loc \/ {(IC SCM )})
by A37, AMI_3:72, RELAT_1:185;
:: thesis: verum end; suppose
InsCode l = 3
;
:: thesis: (Exec l,s1) | (SCM-Data-Loc \/ {(IC SCM )}) = (Exec l,s2) | (SCM-Data-Loc \/ {(IC SCM )})then consider da,
db being
Data-Location such that A38:
l = SubFrom da,
db
by Th49;
da in SCM-Data-Loc
by AMI_3:def 2;
then A39:
SCM-Data-Loc =
SCM-Data-Loc \/ {da}
by ZFMISC_1:46
.=
(SCM-Data-Loc \ {da}) \/ {da}
by XBOOLE_1:39
;
A40:
dom ((Exec l,s1) | (SCM-Data-Loc \ {da})) = SCM-Data-Loc \ {da}
by A7, RELAT_1:91;
A41:
dom ((Exec l,s2) | (SCM-Data-Loc \ {da})) = SCM-Data-Loc \ {da}
by A8, RELAT_1:91;
for
x being
set st
x in SCM-Data-Loc \ {da} holds
((Exec l,s1) | (SCM-Data-Loc \ {da})) . x = ((Exec l,s2) | (SCM-Data-Loc \ {da})) . x
proof
let x be
set ;
:: thesis: ( x in SCM-Data-Loc \ {da} implies ((Exec l,s1) | (SCM-Data-Loc \ {da})) . x = ((Exec l,s2) | (SCM-Data-Loc \ {da})) . x )
assume A42:
x in SCM-Data-Loc \ {da}
;
:: thesis: ((Exec l,s1) | (SCM-Data-Loc \ {da})) . x = ((Exec l,s2) | (SCM-Data-Loc \ {da})) . x
then A43:
x in SCM-Data-Loc
by XBOOLE_0:def 5;
A44:
not
x in {da}
by A42, XBOOLE_0:def 5;
reconsider a =
x as
Data-Location by A43, AMI_3:def 2;
A45:
a <> da
by A44, TARSKI:def 1;
A46:
a in SCM-Data-Loc \/ {(IC SCM )}
by A43, XBOOLE_0:def 3;
thus ((Exec l,s1) | (SCM-Data-Loc \ {da})) . x =
(Exec l,s1) . a
by A42, FUNCT_1:72
.=
s1 . a
by A38, A45, AMI_3:10
.=
(s1 | (SCM-Data-Loc \/ {(IC SCM )})) . a
by A46, FUNCT_1:72
.=
s2 . a
by A1, A46, FUNCT_1:72
.=
(Exec l,s2) . a
by A38, A45, AMI_3:10
.=
((Exec l,s2) | (SCM-Data-Loc \ {da})) . x
by A42, FUNCT_1:72
;
:: thesis: verum
end; then A47:
(Exec l,s1) | (SCM-Data-Loc \ {da}) = (Exec l,s2) | (SCM-Data-Loc \ {da})
by A40, A41, FUNCT_1:9;
A48:
db in SCM-Data-Loc
by AMI_3:def 2;
A49:
da in SCM-Data-Loc
by AMI_3:def 2;
then A50:
s1 . da =
(s1 | (SCM-Data-Loc \/ {(IC SCM )})) . da
by A9, FUNCT_1:72
.=
s2 . da
by A1, A9, A49, FUNCT_1:72
;
A51:
s1 . db =
(s1 | (SCM-Data-Loc \/ {(IC SCM )})) . db
by A9, A48, FUNCT_1:72
.=
s2 . db
by A1, A9, A48, FUNCT_1:72
;
(Exec l,s1) . da =
(s1 . da) - (s1 . db)
by A38, AMI_3:10
.=
(Exec l,s2) . da
by A38, A50, A51, AMI_3:10
;
then
(Exec l,s1) | {da} = (Exec l,s2) | {da}
by A7, A8, GRFUNC_1:90;
then A52:
DataPart (Exec l,s1) = DataPart (Exec l,s2)
by A39, A47, AMI_3:72, RELAT_1:185;
(Exec l,s1) . (IC SCM ) =
Next (IC s1)
by A38, AMI_3:10
.=
(Exec l,s2) . (IC SCM )
by A6, A38, AMI_3:10
;
then
(Exec l,s1) | {(IC SCM )} = (Exec l,s2) | {(IC SCM )}
by A7, A8, GRFUNC_1:90;
hence
(Exec l,s1) | (SCM-Data-Loc \/ {(IC SCM )}) = (Exec l,s2) | (SCM-Data-Loc \/ {(IC SCM )})
by A52, AMI_3:72, RELAT_1:185;
:: thesis: verum end; suppose
InsCode l = 4
;
:: thesis: (Exec l,s1) | (SCM-Data-Loc \/ {(IC SCM )}) = (Exec l,s2) | (SCM-Data-Loc \/ {(IC SCM )})then consider da,
db being
Data-Location such that A53:
l = MultBy da,
db
by Th50;
da in SCM-Data-Loc
by AMI_3:def 2;
then A54:
SCM-Data-Loc =
SCM-Data-Loc \/ {da}
by ZFMISC_1:46
.=
(SCM-Data-Loc \ {da}) \/ {da}
by XBOOLE_1:39
;
A55:
dom ((Exec l,s1) | (SCM-Data-Loc \ {da})) = SCM-Data-Loc \ {da}
by A7, RELAT_1:91;
A56:
dom ((Exec l,s2) | (SCM-Data-Loc \ {da})) = SCM-Data-Loc \ {da}
by A8, RELAT_1:91;
for
x being
set st
x in SCM-Data-Loc \ {da} holds
((Exec l,s1) | (SCM-Data-Loc \ {da})) . x = ((Exec l,s2) | (SCM-Data-Loc \ {da})) . x
proof
let x be
set ;
:: thesis: ( x in SCM-Data-Loc \ {da} implies ((Exec l,s1) | (SCM-Data-Loc \ {da})) . x = ((Exec l,s2) | (SCM-Data-Loc \ {da})) . x )
assume A57:
x in SCM-Data-Loc \ {da}
;
:: thesis: ((Exec l,s1) | (SCM-Data-Loc \ {da})) . x = ((Exec l,s2) | (SCM-Data-Loc \ {da})) . x
then A58:
x in SCM-Data-Loc
by XBOOLE_0:def 5;
A59:
not
x in {da}
by A57, XBOOLE_0:def 5;
reconsider a =
x as
Data-Location by A58, AMI_3:def 2;
A60:
a <> da
by A59, TARSKI:def 1;
A61:
a in SCM-Data-Loc \/ {(IC SCM )}
by A58, XBOOLE_0:def 3;
thus ((Exec l,s1) | (SCM-Data-Loc \ {da})) . x =
(Exec l,s1) . a
by A57, FUNCT_1:72
.=
s1 . a
by A53, A60, AMI_3:11
.=
(s1 | (SCM-Data-Loc \/ {(IC SCM )})) . a
by A61, FUNCT_1:72
.=
s2 . a
by A1, A61, FUNCT_1:72
.=
(Exec l,s2) . a
by A53, A60, AMI_3:11
.=
((Exec l,s2) | (SCM-Data-Loc \ {da})) . x
by A57, FUNCT_1:72
;
:: thesis: verum
end; then A62:
(Exec l,s1) | (SCM-Data-Loc \ {da}) = (Exec l,s2) | (SCM-Data-Loc \ {da})
by A55, A56, FUNCT_1:9;
A63:
db in SCM-Data-Loc
by AMI_3:def 2;
A64:
da in SCM-Data-Loc
by AMI_3:def 2;
then A65:
s1 . da =
(s1 | (SCM-Data-Loc \/ {(IC SCM )})) . da
by A9, FUNCT_1:72
.=
s2 . da
by A1, A9, A64, FUNCT_1:72
;
A66:
s1 . db =
(s1 | (SCM-Data-Loc \/ {(IC SCM )})) . db
by A9, A63, FUNCT_1:72
.=
s2 . db
by A1, A9, A63, FUNCT_1:72
;
(Exec l,s1) . da =
(s1 . da) * (s1 . db)
by A53, AMI_3:11
.=
(Exec l,s2) . da
by A53, A65, A66, AMI_3:11
;
then
(Exec l,s1) | {da} = (Exec l,s2) | {da}
by A7, A8, GRFUNC_1:90;
then A67:
DataPart (Exec l,s1) = DataPart (Exec l,s2)
by A54, A62, AMI_3:72, RELAT_1:185;
(Exec l,s1) . (IC SCM ) =
Next (IC s1)
by A53, AMI_3:11
.=
(Exec l,s2) . (IC SCM )
by A6, A53, AMI_3:11
;
then
(Exec l,s1) | {(IC SCM )} = (Exec l,s2) | {(IC SCM )}
by A7, A8, GRFUNC_1:90;
hence
(Exec l,s1) | (SCM-Data-Loc \/ {(IC SCM )}) = (Exec l,s2) | (SCM-Data-Loc \/ {(IC SCM )})
by A67, AMI_3:72, RELAT_1:185;
:: thesis: verum end; suppose
InsCode l = 5
;
:: thesis: (Exec l,s1) | (SCM-Data-Loc \/ {(IC SCM )}) = (Exec l,s2) | (SCM-Data-Loc \/ {(IC SCM )})then consider da,
db being
Data-Location such that A68:
l = Divide da,
db
by Th51;
thus
(Exec l,s1) | (SCM-Data-Loc \/ {(IC SCM )}) = (Exec l,s2) | (SCM-Data-Loc \/ {(IC SCM )})
:: thesis: verumproof
per cases
( da = db or da <> db )
;
suppose A69:
da = db
;
:: thesis: (Exec l,s1) | (SCM-Data-Loc \/ {(IC SCM )}) = (Exec l,s2) | (SCM-Data-Loc \/ {(IC SCM )})
da in SCM-Data-Loc
by AMI_3:def 2;
then A70:
SCM-Data-Loc =
SCM-Data-Loc \/ {da}
by ZFMISC_1:46
.=
(SCM-Data-Loc \ {da}) \/ {da}
by XBOOLE_1:39
;
A71:
dom ((Exec l,s1) | (SCM-Data-Loc \ {da})) = SCM-Data-Loc \ {da}
by A7, RELAT_1:91;
A72:
dom ((Exec l,s2) | (SCM-Data-Loc \ {da})) = SCM-Data-Loc \ {da}
by A8, RELAT_1:91;
for
x being
set st
x in SCM-Data-Loc \ {da} holds
((Exec l,s1) | (SCM-Data-Loc \ {da})) . x = ((Exec l,s2) | (SCM-Data-Loc \ {da})) . x
proof
let x be
set ;
:: thesis: ( x in SCM-Data-Loc \ {da} implies ((Exec l,s1) | (SCM-Data-Loc \ {da})) . x = ((Exec l,s2) | (SCM-Data-Loc \ {da})) . x )
assume A73:
x in SCM-Data-Loc \ {da}
;
:: thesis: ((Exec l,s1) | (SCM-Data-Loc \ {da})) . x = ((Exec l,s2) | (SCM-Data-Loc \ {da})) . x
then A74:
x in SCM-Data-Loc
by XBOOLE_0:def 5;
A75:
not
x in {da}
by A73, XBOOLE_0:def 5;
reconsider a =
x as
Data-Location by A74, AMI_3:def 2;
A76:
a <> da
by A75, TARSKI:def 1;
A77:
a in SCM-Data-Loc \/ {(IC SCM )}
by A74, XBOOLE_0:def 3;
thus ((Exec l,s1) | (SCM-Data-Loc \ {da})) . x =
(Exec l,s1) . a
by A73, FUNCT_1:72
.=
s1 . a
by A68, A69, A76, AMI_3:12
.=
(s1 | (SCM-Data-Loc \/ {(IC SCM )})) . a
by A77, FUNCT_1:72
.=
s2 . a
by A1, A77, FUNCT_1:72
.=
(Exec l,s2) . a
by A68, A69, A76, AMI_3:12
.=
((Exec l,s2) | (SCM-Data-Loc \ {da})) . x
by A73, FUNCT_1:72
;
:: thesis: verum
end; then A78:
(Exec l,s1) | (SCM-Data-Loc \ {da}) = (Exec l,s2) | (SCM-Data-Loc \ {da})
by A71, A72, FUNCT_1:9;
A79:
da in SCM-Data-Loc
by AMI_3:def 2;
then A80:
s1 . da =
(s1 | (SCM-Data-Loc \/ {(IC SCM )})) . da
by A9, FUNCT_1:72
.=
s2 . da
by A1, A9, A79, FUNCT_1:72
;
(Exec l,s1) . da =
(s1 . da) mod (s1 . da)
by A68, A69, AMI_3:12
.=
(Exec l,s2) . da
by A68, A69, A80, AMI_3:12
;
then
(Exec l,s1) | {da} = (Exec l,s2) | {da}
by A7, A8, GRFUNC_1:90;
then A81:
DataPart (Exec l,s1) = DataPart (Exec l,s2)
by A70, A78, AMI_3:72, RELAT_1:185;
(Exec l,s1) . (IC SCM ) =
Next (IC s1)
by A68, AMI_3:12
.=
(Exec l,s2) . (IC SCM )
by A6, A68, AMI_3:12
;
then
(Exec l,s1) | {(IC SCM )} = (Exec l,s2) | {(IC SCM )}
by A7, A8, GRFUNC_1:90;
hence
(Exec l,s1) | (SCM-Data-Loc \/ {(IC SCM )}) = (Exec l,s2) | (SCM-Data-Loc \/ {(IC SCM )})
by A81, AMI_3:72, RELAT_1:185;
:: thesis: verum end; suppose A82:
da <> db
;
:: thesis: (Exec l,s1) | (SCM-Data-Loc \/ {(IC SCM )}) = (Exec l,s2) | (SCM-Data-Loc \/ {(IC SCM )})A83:
da in SCM-Data-Loc
by AMI_3:def 2;
db in SCM-Data-Loc
by AMI_3:def 2;
then A84:
SCM-Data-Loc =
SCM-Data-Loc \/ {da,db}
by A83, ZFMISC_1:48
.=
(SCM-Data-Loc \ {da,db}) \/ {da,db}
by XBOOLE_1:39
;
A85:
dom ((Exec l,s1) | (SCM-Data-Loc \ {da,db})) = SCM-Data-Loc \ {da,db}
by A7, RELAT_1:91;
A86:
dom ((Exec l,s2) | (SCM-Data-Loc \ {da,db})) = SCM-Data-Loc \ {da,db}
by A8, RELAT_1:91;
for
x being
set st
x in SCM-Data-Loc \ {da,db} holds
((Exec l,s1) | (SCM-Data-Loc \ {da,db})) . x = ((Exec l,s2) | (SCM-Data-Loc \ {da,db})) . x
proof
let x be
set ;
:: thesis: ( x in SCM-Data-Loc \ {da,db} implies ((Exec l,s1) | (SCM-Data-Loc \ {da,db})) . x = ((Exec l,s2) | (SCM-Data-Loc \ {da,db})) . x )
assume A87:
x in SCM-Data-Loc \ {da,db}
;
:: thesis: ((Exec l,s1) | (SCM-Data-Loc \ {da,db})) . x = ((Exec l,s2) | (SCM-Data-Loc \ {da,db})) . x
then A88:
x in SCM-Data-Loc
by XBOOLE_0:def 5;
A89:
not
x in {da,db}
by A87, XBOOLE_0:def 5;
reconsider a =
x as
Data-Location by A88, AMI_3:def 2;
A90:
(
a <> da &
a <> db )
by A89, TARSKI:def 2;
A91:
a in SCM-Data-Loc \/ {(IC SCM )}
by A88, XBOOLE_0:def 3;
thus ((Exec l,s1) | (SCM-Data-Loc \ {da,db})) . x =
(Exec l,s1) . a
by A87, FUNCT_1:72
.=
s1 . a
by A68, A90, AMI_3:12
.=
(s1 | (SCM-Data-Loc \/ {(IC SCM )})) . a
by A91, FUNCT_1:72
.=
s2 . a
by A1, A91, FUNCT_1:72
.=
(Exec l,s2) . a
by A68, A90, AMI_3:12
.=
((Exec l,s2) | (SCM-Data-Loc \ {da,db})) . x
by A87, FUNCT_1:72
;
:: thesis: verum
end; then A92:
(Exec l,s1) | (SCM-Data-Loc \ {da,db}) = (Exec l,s2) | (SCM-Data-Loc \ {da,db})
by A85, A86, FUNCT_1:9;
A93:
db in SCM-Data-Loc
by AMI_3:def 2;
A94:
da in SCM-Data-Loc
by AMI_3:def 2;
then A95:
s1 . da =
(s1 | (SCM-Data-Loc \/ {(IC SCM )})) . da
by A9, FUNCT_1:72
.=
s2 . da
by A1, A9, A94, FUNCT_1:72
;
A96:
s1 . db =
(s1 | (SCM-Data-Loc \/ {(IC SCM )})) . db
by A9, A93, FUNCT_1:72
.=
s2 . db
by A1, A9, A93, FUNCT_1:72
;
A97:
(Exec l,s1) . da =
(s1 . da) div (s1 . db)
by A68, A82, AMI_3:12
.=
(Exec l,s2) . da
by A68, A82, A95, A96, AMI_3:12
;
(Exec l,s1) . db =
(s1 . da) mod (s1 . db)
by A68, AMI_3:12
.=
(Exec l,s2) . db
by A68, A95, A96, AMI_3:12
;
then
(Exec l,s1) | {da,db} = (Exec l,s2) | {da,db}
by A7, A8, A97, GRFUNC_1:91;
then A98:
DataPart (Exec l,s1) = DataPart (Exec l,s2)
by A84, A92, AMI_3:72, RELAT_1:185;
(Exec l,s1) . (IC SCM ) =
Next (IC s1)
by A68, AMI_3:12
.=
(Exec l,s2) . (IC SCM )
by A6, A68, AMI_3:12
;
then
(Exec l,s1) | {(IC SCM )} = (Exec l,s2) | {(IC SCM )}
by A7, A8, GRFUNC_1:90;
hence
(Exec l,s1) | (SCM-Data-Loc \/ {(IC SCM )}) = (Exec l,s2) | (SCM-Data-Loc \/ {(IC SCM )})
by A98, AMI_3:72, RELAT_1:185;
:: thesis: verum end;
end; end; suppose
InsCode l = 6
;
:: thesis: (Exec l,s1) | (SCM-Data-Loc \/ {(IC SCM )}) = (Exec l,s2) | (SCM-Data-Loc \/ {(IC SCM )})then consider loc being
Instruction-Location of
SCM such that A99:
l = goto loc
by Th52;
A100:
dom (DataPart (Exec l,s1)) = SCM-Data-Loc
by A7, AMI_3:72, RELAT_1:91;
A101:
dom (DataPart (Exec l,s2)) = SCM-Data-Loc
by A8, AMI_3:72, RELAT_1:91;
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 A102:
x in SCM-Data-Loc
;
:: thesis: (DataPart (Exec l,s1)) . x = (DataPart (Exec l,s2)) . x
then reconsider a =
x as
Data-Location by AMI_3:def 2;
A103:
a in SCM-Data-Loc \/ {(IC SCM )}
by A102, XBOOLE_0:def 3;
thus (DataPart (Exec l,s1)) . x =
(Exec l,s1) . a
by A102, AMI_3:72, FUNCT_1:72
.=
s1 . a
by A99, AMI_3:13
.=
(s1 | (SCM-Data-Loc \/ {(IC SCM )})) . a
by A103, FUNCT_1:72
.=
s2 . a
by A1, A103, FUNCT_1:72
.=
(Exec l,s2) . a
by A99, AMI_3:13
.=
(DataPart (Exec l,s2)) . x
by A102, AMI_3:72, FUNCT_1:72
;
:: thesis: verum
end; then A104:
(Exec l,s1) | SCM-Data-Loc = (Exec l,s2) | SCM-Data-Loc
by A100, A101, AMI_3:72, FUNCT_1:9;
(Exec l,s1) . (IC SCM ) =
loc
by A99, AMI_3:13
.=
(Exec l,s2) . (IC SCM )
by A99, AMI_3:13
;
then
(Exec l,s1) | {(IC SCM )} = (Exec l,s2) | {(IC SCM )}
by A7, A8, GRFUNC_1:90;
hence
(Exec l,s1) | (SCM-Data-Loc \/ {(IC SCM )}) = (Exec l,s2) | (SCM-Data-Loc \/ {(IC SCM )})
by A104, RELAT_1:185;
:: thesis: verum end; suppose
InsCode l = 7
;
:: thesis: (Exec l,s1) | (SCM-Data-Loc \/ {(IC SCM )}) = (Exec l,s2) | (SCM-Data-Loc \/ {(IC SCM )})then consider loc being
Instruction-Location of
SCM ,
da being
Data-Location such that A105:
l = da =0_goto loc
by Th53;
A106:
dom (DataPart (Exec l,s1)) = SCM-Data-Loc
by A7, AMI_3:72, RELAT_1:91;
A107:
dom (DataPart (Exec l,s2)) = SCM-Data-Loc
by A8, AMI_3:72, RELAT_1:91;
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 A108:
x in SCM-Data-Loc
;
:: thesis: (DataPart (Exec l,s1)) . x = (DataPart (Exec l,s2)) . x
then reconsider a =
x as
Data-Location by AMI_3:def 2;
A109:
a in SCM-Data-Loc \/ {(IC SCM )}
by A108, XBOOLE_0:def 3;
thus (DataPart (Exec l,s1)) . x =
(Exec l,s1) . a
by A108, AMI_3:72, FUNCT_1:72
.=
s1 . a
by A105, AMI_3:14
.=
(s1 | (SCM-Data-Loc \/ {(IC SCM )})) . a
by A109, FUNCT_1:72
.=
s2 . a
by A1, A109, FUNCT_1:72
.=
(Exec l,s2) . a
by A105, AMI_3:14
.=
(DataPart (Exec l,s2)) . x
by A108, AMI_3:72, FUNCT_1:72
;
:: thesis: verum
end; then A110:
(Exec l,s1) | SCM-Data-Loc = (Exec l,s2) | SCM-Data-Loc
by A106, A107, AMI_3:72, FUNCT_1:9;
(Exec l,s1) . (IC SCM ) = (Exec l,s2) . (IC SCM )
then
(Exec l,s1) | {(IC SCM )} = (Exec l,s2) | {(IC SCM )}
by A7, A8, GRFUNC_1:90;
hence
(Exec l,s1) | (SCM-Data-Loc \/ {(IC SCM )}) = (Exec l,s2) | (SCM-Data-Loc \/ {(IC SCM )})
by A110, RELAT_1:185;
:: thesis: verum end; suppose
InsCode l = 8
;
:: thesis: (Exec l,s1) | (SCM-Data-Loc \/ {(IC SCM )}) = (Exec l,s2) | (SCM-Data-Loc \/ {(IC SCM )})then consider loc being
Instruction-Location of
SCM ,
da being
Data-Location such that A115:
l = da >0_goto loc
by Th54;
A116:
dom (DataPart (Exec l,s1)) = SCM-Data-Loc
by A7, AMI_3:72, RELAT_1:91;
A117:
dom (DataPart (Exec l,s2)) = SCM-Data-Loc
by A8, AMI_3:72, RELAT_1:91;
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 A118:
x in SCM-Data-Loc
;
:: thesis: (DataPart (Exec l,s1)) . x = (DataPart (Exec l,s2)) . x
then reconsider a =
x as
Data-Location by AMI_3:def 2;
A119:
a in SCM-Data-Loc \/ {(IC SCM )}
by A118, XBOOLE_0:def 3;
thus (DataPart (Exec l,s1)) . x =
(Exec l,s1) . a
by A118, AMI_3:72, FUNCT_1:72
.=
s1 . a
by A115, AMI_3:15
.=
(s1 | (SCM-Data-Loc \/ {(IC SCM )})) . a
by A119, FUNCT_1:72
.=
s2 . a
by A1, A119, FUNCT_1:72
.=
(Exec l,s2) . a
by A115, AMI_3:15
.=
(DataPart (Exec l,s2)) . x
by A118, AMI_3:72, FUNCT_1:72
;
:: thesis: verum
end; then A120:
(Exec l,s1) | SCM-Data-Loc = (Exec l,s2) | SCM-Data-Loc
by A116, A117, AMI_3:72, FUNCT_1:9;
(Exec l,s1) . (IC SCM ) = (Exec l,s2) . (IC SCM )
then
(Exec l,s1) | {(IC SCM )} = (Exec l,s2) | {(IC SCM )}
by A7, A8, GRFUNC_1:90;
hence
(Exec l,s1) | (SCM-Data-Loc \/ {(IC SCM )}) = (Exec l,s2) | (SCM-Data-Loc \/ {(IC SCM )})
by A120, RELAT_1:185;
:: thesis: verum end;