let i be Instruction of SCM+FSA; for s1, s2 being State of SCM+FSA st DataPart s1 = DataPart s2 holds
DataPart (Exec (i,s1)) = DataPart (Exec (i,s2))
let s1, s2 be State of SCM+FSA; ( DataPart s1 = DataPart s2 implies DataPart (Exec (i,s1)) = DataPart (Exec (i,s2)) )
assume A1:
DataPart s1 = DataPart s2
; DataPart (Exec (i,s1)) = DataPart (Exec (i,s2))
set l = i;
A5:
dom (Exec (i,s1)) = the carrier of SCM+FSA
by PARTFUN1:def 2;
then A6:
dom (Exec (i,s1)) = dom (Exec (i,s2))
by PARTFUN1:def 2;
A7:
dom ((Exec (i,s1)) | (Data-Locations )) = Data-Locations
by A5, RELAT_1:62;
A8:
dom (Exec (i,s2)) = the carrier of SCM+FSA
by PARTFUN1:def 2;
then A9:
dom ((Exec (i,s2)) | (Data-Locations )) = Data-Locations
by RELAT_1:62;
per cases
( InsCode i = 0 or InsCode i = 1 or InsCode i = 2 or InsCode i = 3 or InsCode i = 4 or InsCode i = 5 or InsCode i = 6 or InsCode i = 7 or InsCode i = 8 or InsCode i = 9 or InsCode i = 10 or InsCode i = 11 or InsCode i = 12 )
by NAT_1:36, SCMFSA_2:16;
suppose
InsCode i = 1
;
DataPart (Exec (i,s1)) = DataPart (Exec (i,s2))then consider db,
da being
Int-Location such that A11:
i = db := da
by SCMFSA_2:30;
A12:
for
x being
set st
x in (Data-Locations ) \ {db} holds
((Exec (i,s1)) | ((Data-Locations ) \ {db})) . x = ((Exec (i,s2)) | ((Data-Locations ) \ {db})) . x
proof
let x be
set ;
( x in (Data-Locations ) \ {db} implies ((Exec (i,s1)) | ((Data-Locations ) \ {db})) . x = ((Exec (i,s2)) | ((Data-Locations ) \ {db})) . x )
assume A13:
x in (Data-Locations ) \ {db}
;
((Exec (i,s1)) | ((Data-Locations ) \ {db})) . x = ((Exec (i,s2)) | ((Data-Locations ) \ {db})) . x
then A14:
x in Data-Locations
by XBOOLE_0:def 5;
A15:
not
x in {db}
by A13, XBOOLE_0:def 5;
per cases
( x in Int-Locations or x in FinSeq-Locations )
by A14, SCMFSA_2:100, XBOOLE_0:def 3;
suppose
x in Int-Locations
;
((Exec (i,s1)) | ((Data-Locations ) \ {db})) . x = ((Exec (i,s2)) | ((Data-Locations ) \ {db})) . xthen reconsider a =
x as
Int-Location by SCMFSA_2:4;
A16:
a <> db
by A15, TARSKI:def 1;
thus ((Exec (i,s1)) | ((Data-Locations ) \ {db})) . x =
(Exec (i,s1)) . a
by A13, FUNCT_1:49
.=
s1 . a
by A11, A16, SCMFSA_2:63
.=
(DataPart s1) . a
by A14, FUNCT_1:49
.=
s2 . a
by A1, A14, FUNCT_1:49
.=
(Exec (i,s2)) . a
by A11, A16, SCMFSA_2:63
.=
((Exec (i,s2)) | ((Data-Locations ) \ {db})) . x
by A13, FUNCT_1:49
;
verum end; suppose
x in FinSeq-Locations
;
((Exec (i,s1)) | ((Data-Locations ) \ {db})) . x = ((Exec (i,s2)) | ((Data-Locations ) \ {db})) . xthen reconsider a =
x as
FinSeq-Location by SCMFSA_2:5;
thus ((Exec (i,s1)) | ((Data-Locations ) \ {db})) . x =
(Exec (i,s1)) . a
by A13, FUNCT_1:49
.=
s1 . a
by A11, SCMFSA_2:63
.=
(DataPart s1) . a
by A14, FUNCT_1:49
.=
s2 . a
by A1, A14, FUNCT_1:49
.=
(Exec (i,s2)) . a
by A11, SCMFSA_2:63
.=
((Exec (i,s2)) | ((Data-Locations ) \ {db})) . x
by A13, FUNCT_1:49
;
verum end;
end; A17:
dom ((Exec (i,s2)) | ((Data-Locations ) \ {db})) = (Data-Locations ) \ {db}
by A8, RELAT_1:62;
dom ((Exec (i,s1)) | ((Data-Locations ) \ {db})) = (Data-Locations ) \ {db}
by A5, RELAT_1:62;
then A18:
(Exec (i,s1)) | ((Data-Locations ) \ {db}) = (Exec (i,s2)) | ((Data-Locations ) \ {db})
by A17, A12, FUNCT_1:2;
db in Int-Locations
by SCMFSA_2:2;
then
db in Data-Locations
by SCMFSA_2:100, XBOOLE_0:def 3;
then A19:
Data-Locations =
(Data-Locations ) \/ {db}
by ZFMISC_1:40
.=
((Data-Locations ) \ {db}) \/ {db}
by XBOOLE_1:39
;
A20:
(Exec (i,s2)) . db = s2 . da
by A11, SCMFSA_2:63;
A21:
(Exec (i,s1)) . db = s1 . da
by A11, SCMFSA_2:63;
da in Int-Locations
by SCMFSA_2:2;
then A22:
da in Data-Locations
by SCMFSA_2:100, XBOOLE_0:def 3;
then s1 . da =
(DataPart s1) . da
by FUNCT_1:49
.=
s2 . da
by A1, A22, FUNCT_1:49
;
then
(Exec (i,s1)) | {db} = (Exec (i,s2)) | {db}
by A6, A21, A20, GRFUNC_1:29;
hence
DataPart (Exec (i,s1)) = DataPart (Exec (i,s2))
by A19, A18, RELAT_1:150;
verum end; suppose
InsCode i = 2
;
DataPart (Exec (i,s1)) = DataPart (Exec (i,s2))then consider db,
da being
Int-Location such that A23:
i = AddTo (
db,
da)
by SCMFSA_2:31;
A24:
for
x being
set st
x in (Data-Locations ) \ {db} holds
((Exec (i,s1)) | ((Data-Locations ) \ {db})) . x = ((Exec (i,s2)) | ((Data-Locations ) \ {db})) . x
proof
let x be
set ;
( x in (Data-Locations ) \ {db} implies ((Exec (i,s1)) | ((Data-Locations ) \ {db})) . x = ((Exec (i,s2)) | ((Data-Locations ) \ {db})) . x )
assume A25:
x in (Data-Locations ) \ {db}
;
((Exec (i,s1)) | ((Data-Locations ) \ {db})) . x = ((Exec (i,s2)) | ((Data-Locations ) \ {db})) . x
then A26:
x in Data-Locations
by XBOOLE_0:def 5;
A27:
not
x in {db}
by A25, XBOOLE_0:def 5;
per cases
( x in Int-Locations or x in FinSeq-Locations )
by A26, SCMFSA_2:100, XBOOLE_0:def 3;
suppose
x in Int-Locations
;
((Exec (i,s1)) | ((Data-Locations ) \ {db})) . x = ((Exec (i,s2)) | ((Data-Locations ) \ {db})) . xthen reconsider a =
x as
Int-Location by SCMFSA_2:4;
A28:
a <> db
by A27, TARSKI:def 1;
thus ((Exec (i,s1)) | ((Data-Locations ) \ {db})) . x =
(Exec (i,s1)) . a
by A25, FUNCT_1:49
.=
s1 . a
by A23, A28, SCMFSA_2:64
.=
(DataPart s1) . a
by A26, FUNCT_1:49
.=
s2 . a
by A1, A26, FUNCT_1:49
.=
(Exec (i,s2)) . a
by A23, A28, SCMFSA_2:64
.=
((Exec (i,s2)) | ((Data-Locations ) \ {db})) . x
by A25, FUNCT_1:49
;
verum end; suppose
x in FinSeq-Locations
;
((Exec (i,s1)) | ((Data-Locations ) \ {db})) . x = ((Exec (i,s2)) | ((Data-Locations ) \ {db})) . xthen reconsider a =
x as
FinSeq-Location by SCMFSA_2:5;
thus ((Exec (i,s1)) | ((Data-Locations ) \ {db})) . x =
(Exec (i,s1)) . a
by A25, FUNCT_1:49
.=
s1 . a
by A23, SCMFSA_2:64
.=
(DataPart s1) . a
by A26, FUNCT_1:49
.=
s2 . a
by A1, A26, FUNCT_1:49
.=
(Exec (i,s2)) . a
by A23, SCMFSA_2:64
.=
((Exec (i,s2)) | ((Data-Locations ) \ {db})) . x
by A25, FUNCT_1:49
;
verum end;
end; A29:
dom ((Exec (i,s2)) | ((Data-Locations ) \ {db})) = (Data-Locations ) \ {db}
by A8, RELAT_1:62;
dom ((Exec (i,s1)) | ((Data-Locations ) \ {db})) = (Data-Locations ) \ {db}
by A5, RELAT_1:62;
then A30:
(Exec (i,s1)) | ((Data-Locations ) \ {db}) = (Exec (i,s2)) | ((Data-Locations ) \ {db})
by A29, A24, FUNCT_1:2;
db in Int-Locations
by SCMFSA_2:2;
then
db in Data-Locations
by SCMFSA_2:100, XBOOLE_0:def 3;
then A31:
Data-Locations =
(Data-Locations ) \/ {db}
by ZFMISC_1:40
.=
((Data-Locations ) \ {db}) \/ {db}
by XBOOLE_1:39
;
A32:
(Exec (i,s2)) . db = (s2 . db) + (s2 . da)
by A23, SCMFSA_2:64;
A33:
(Exec (i,s1)) . db = (s1 . db) + (s1 . da)
by A23, SCMFSA_2:64;
db in Int-Locations
by SCMFSA_2:2;
then A34:
db in Data-Locations
by SCMFSA_2:100, XBOOLE_0:def 3;
then A35:
s1 . db =
(DataPart s1) . db
by FUNCT_1:49
.=
s2 . db
by A1, A34, FUNCT_1:49
;
da in Int-Locations
by SCMFSA_2:2;
then A36:
da in Data-Locations
by SCMFSA_2:100, XBOOLE_0:def 3;
then s1 . da =
(DataPart s1) . da
by FUNCT_1:49
.=
s2 . da
by A1, A36, FUNCT_1:49
;
then
(Exec (i,s1)) | {db} = (Exec (i,s2)) | {db}
by A6, A33, A32, A35, GRFUNC_1:29;
hence
DataPart (Exec (i,s1)) = DataPart (Exec (i,s2))
by A31, A30, RELAT_1:150;
verum end; suppose
InsCode i = 3
;
DataPart (Exec (i,s1)) = DataPart (Exec (i,s2))then consider db,
da being
Int-Location such that A37:
i = SubFrom (
db,
da)
by SCMFSA_2:32;
A38:
for
x being
set st
x in (Data-Locations ) \ {db} holds
((Exec (i,s1)) | ((Data-Locations ) \ {db})) . x = ((Exec (i,s2)) | ((Data-Locations ) \ {db})) . x
proof
let x be
set ;
( x in (Data-Locations ) \ {db} implies ((Exec (i,s1)) | ((Data-Locations ) \ {db})) . x = ((Exec (i,s2)) | ((Data-Locations ) \ {db})) . x )
assume A39:
x in (Data-Locations ) \ {db}
;
((Exec (i,s1)) | ((Data-Locations ) \ {db})) . x = ((Exec (i,s2)) | ((Data-Locations ) \ {db})) . x
then A40:
x in Data-Locations
by XBOOLE_0:def 5;
A41:
not
x in {db}
by A39, XBOOLE_0:def 5;
per cases
( x in Int-Locations or x in FinSeq-Locations )
by A40, SCMFSA_2:100, XBOOLE_0:def 3;
suppose
x in Int-Locations
;
((Exec (i,s1)) | ((Data-Locations ) \ {db})) . x = ((Exec (i,s2)) | ((Data-Locations ) \ {db})) . xthen reconsider a =
x as
Int-Location by SCMFSA_2:4;
A42:
a <> db
by A41, TARSKI:def 1;
thus ((Exec (i,s1)) | ((Data-Locations ) \ {db})) . x =
(Exec (i,s1)) . a
by A39, FUNCT_1:49
.=
s1 . a
by A37, A42, SCMFSA_2:65
.=
(DataPart s1) . a
by A40, FUNCT_1:49
.=
s2 . a
by A1, A40, FUNCT_1:49
.=
(Exec (i,s2)) . a
by A37, A42, SCMFSA_2:65
.=
((Exec (i,s2)) | ((Data-Locations ) \ {db})) . x
by A39, FUNCT_1:49
;
verum end; suppose
x in FinSeq-Locations
;
((Exec (i,s1)) | ((Data-Locations ) \ {db})) . x = ((Exec (i,s2)) | ((Data-Locations ) \ {db})) . xthen reconsider a =
x as
FinSeq-Location by SCMFSA_2:5;
thus ((Exec (i,s1)) | ((Data-Locations ) \ {db})) . x =
(Exec (i,s1)) . a
by A39, FUNCT_1:49
.=
s1 . a
by A37, SCMFSA_2:65
.=
(DataPart s1) . a
by A40, FUNCT_1:49
.=
s2 . a
by A1, A40, FUNCT_1:49
.=
(Exec (i,s2)) . a
by A37, SCMFSA_2:65
.=
((Exec (i,s2)) | ((Data-Locations ) \ {db})) . x
by A39, FUNCT_1:49
;
verum end;
end; A43:
dom ((Exec (i,s2)) | ((Data-Locations ) \ {db})) = (Data-Locations ) \ {db}
by A8, RELAT_1:62;
dom ((Exec (i,s1)) | ((Data-Locations ) \ {db})) = (Data-Locations ) \ {db}
by A5, RELAT_1:62;
then A44:
(Exec (i,s1)) | ((Data-Locations ) \ {db}) = (Exec (i,s2)) | ((Data-Locations ) \ {db})
by A43, A38, FUNCT_1:2;
db in Int-Locations
by SCMFSA_2:2;
then
db in Data-Locations
by SCMFSA_2:100, XBOOLE_0:def 3;
then A45:
Data-Locations =
(Data-Locations ) \/ {db}
by ZFMISC_1:40
.=
((Data-Locations ) \ {db}) \/ {db}
by XBOOLE_1:39
;
A46:
(Exec (i,s2)) . db = (s2 . db) - (s2 . da)
by A37, SCMFSA_2:65;
A47:
(Exec (i,s1)) . db = (s1 . db) - (s1 . da)
by A37, SCMFSA_2:65;
db in Int-Locations
by SCMFSA_2:2;
then A48:
db in Data-Locations
by SCMFSA_2:100, XBOOLE_0:def 3;
then A49:
s1 . db =
(DataPart s1) . db
by FUNCT_1:49
.=
s2 . db
by A1, A48, FUNCT_1:49
;
da in Int-Locations
by SCMFSA_2:2;
then A50:
da in Data-Locations
by SCMFSA_2:100, XBOOLE_0:def 3;
then s1 . da =
(DataPart s1) . da
by FUNCT_1:49
.=
s2 . da
by A1, A50, FUNCT_1:49
;
then
(Exec (i,s1)) | {db} = (Exec (i,s2)) | {db}
by A6, A47, A46, A49, GRFUNC_1:29;
hence
DataPart (Exec (i,s1)) = DataPart (Exec (i,s2))
by A45, A44, RELAT_1:150;
verum end; suppose
InsCode i = 4
;
DataPart (Exec (i,s1)) = DataPart (Exec (i,s2))then consider db,
da being
Int-Location such that A51:
i = MultBy (
db,
da)
by SCMFSA_2:33;
A52:
for
x being
set st
x in (Data-Locations ) \ {db} holds
((Exec (i,s1)) | ((Data-Locations ) \ {db})) . x = ((Exec (i,s2)) | ((Data-Locations ) \ {db})) . x
proof
let x be
set ;
( x in (Data-Locations ) \ {db} implies ((Exec (i,s1)) | ((Data-Locations ) \ {db})) . x = ((Exec (i,s2)) | ((Data-Locations ) \ {db})) . x )
assume A53:
x in (Data-Locations ) \ {db}
;
((Exec (i,s1)) | ((Data-Locations ) \ {db})) . x = ((Exec (i,s2)) | ((Data-Locations ) \ {db})) . x
then A54:
x in Data-Locations
by XBOOLE_0:def 5;
A55:
not
x in {db}
by A53, XBOOLE_0:def 5;
per cases
( x in Int-Locations or x in FinSeq-Locations )
by A54, SCMFSA_2:100, XBOOLE_0:def 3;
suppose
x in Int-Locations
;
((Exec (i,s1)) | ((Data-Locations ) \ {db})) . x = ((Exec (i,s2)) | ((Data-Locations ) \ {db})) . xthen reconsider a =
x as
Int-Location by SCMFSA_2:4;
A56:
a <> db
by A55, TARSKI:def 1;
thus ((Exec (i,s1)) | ((Data-Locations ) \ {db})) . x =
(Exec (i,s1)) . a
by A53, FUNCT_1:49
.=
s1 . a
by A51, A56, SCMFSA_2:66
.=
(DataPart s1) . a
by A54, FUNCT_1:49
.=
s2 . a
by A1, A54, FUNCT_1:49
.=
(Exec (i,s2)) . a
by A51, A56, SCMFSA_2:66
.=
((Exec (i,s2)) | ((Data-Locations ) \ {db})) . x
by A53, FUNCT_1:49
;
verum end; suppose
x in FinSeq-Locations
;
((Exec (i,s1)) | ((Data-Locations ) \ {db})) . x = ((Exec (i,s2)) | ((Data-Locations ) \ {db})) . xthen reconsider a =
x as
FinSeq-Location by SCMFSA_2:5;
thus ((Exec (i,s1)) | ((Data-Locations ) \ {db})) . x =
(Exec (i,s1)) . a
by A53, FUNCT_1:49
.=
s1 . a
by A51, SCMFSA_2:66
.=
(DataPart s1) . a
by A54, FUNCT_1:49
.=
s2 . a
by A1, A54, FUNCT_1:49
.=
(Exec (i,s2)) . a
by A51, SCMFSA_2:66
.=
((Exec (i,s2)) | ((Data-Locations ) \ {db})) . x
by A53, FUNCT_1:49
;
verum end;
end; A57:
dom ((Exec (i,s2)) | ((Data-Locations ) \ {db})) = (Data-Locations ) \ {db}
by A8, RELAT_1:62;
dom ((Exec (i,s1)) | ((Data-Locations ) \ {db})) = (Data-Locations ) \ {db}
by A5, RELAT_1:62;
then A58:
(Exec (i,s1)) | ((Data-Locations ) \ {db}) = (Exec (i,s2)) | ((Data-Locations ) \ {db})
by A57, A52, FUNCT_1:2;
db in Int-Locations
by SCMFSA_2:2;
then
db in Data-Locations
by SCMFSA_2:100, XBOOLE_0:def 3;
then A59:
Data-Locations =
(Data-Locations ) \/ {db}
by ZFMISC_1:40
.=
((Data-Locations ) \ {db}) \/ {db}
by XBOOLE_1:39
;
A60:
(Exec (i,s2)) . db = (s2 . db) * (s2 . da)
by A51, SCMFSA_2:66;
A61:
(Exec (i,s1)) . db = (s1 . db) * (s1 . da)
by A51, SCMFSA_2:66;
db in Int-Locations
by SCMFSA_2:2;
then A62:
db in Data-Locations
by SCMFSA_2:100, XBOOLE_0:def 3;
then A63:
s1 . db =
(DataPart s1) . db
by FUNCT_1:49
.=
s2 . db
by A1, A62, FUNCT_1:49
;
da in Int-Locations
by SCMFSA_2:2;
then A64:
da in Data-Locations
by SCMFSA_2:100, XBOOLE_0:def 3;
then s1 . da =
(DataPart s1) . da
by FUNCT_1:49
.=
s2 . da
by A1, A64, FUNCT_1:49
;
then
(Exec (i,s1)) | {db} = (Exec (i,s2)) | {db}
by A6, A61, A60, A63, GRFUNC_1:29;
hence
DataPart (Exec (i,s1)) = DataPart (Exec (i,s2))
by A59, A58, RELAT_1:150;
verum end; suppose
InsCode i = 5
;
DataPart (Exec (i,s1)) = DataPart (Exec (i,s2))then consider db,
da being
Int-Location such that A65:
i = Divide (
db,
da)
by SCMFSA_2:34;
hereby verum
per cases
( da <> db or da = db )
;
suppose A66:
da <> db
;
DataPart (Exec (i,s1)) = DataPart (Exec (i,s2))A67:
for
x being
set st
x in (Data-Locations ) \ {db,da} holds
((Exec (i,s1)) | ((Data-Locations ) \ {db,da})) . x = ((Exec (i,s2)) | ((Data-Locations ) \ {db,da})) . x
proof
let x be
set ;
( x in (Data-Locations ) \ {db,da} implies ((Exec (i,s1)) | ((Data-Locations ) \ {db,da})) . x = ((Exec (i,s2)) | ((Data-Locations ) \ {db,da})) . x )
assume A68:
x in (Data-Locations ) \ {db,da}
;
((Exec (i,s1)) | ((Data-Locations ) \ {db,da})) . x = ((Exec (i,s2)) | ((Data-Locations ) \ {db,da})) . x
then A69:
x in Data-Locations
by XBOOLE_0:def 5;
A70:
not
x in {db,da}
by A68, XBOOLE_0:def 5;
per cases
( x in Int-Locations or x in FinSeq-Locations )
by A69, SCMFSA_2:100, XBOOLE_0:def 3;
suppose
x in Int-Locations
;
((Exec (i,s1)) | ((Data-Locations ) \ {db,da})) . x = ((Exec (i,s2)) | ((Data-Locations ) \ {db,da})) . xthen reconsider a =
x as
Int-Location by SCMFSA_2:4;
A71:
a <> da
by A70, TARSKI:def 2;
A72:
a <> db
by A70, TARSKI:def 2;
thus ((Exec (i,s1)) | ((Data-Locations ) \ {db,da})) . x =
(Exec (i,s1)) . a
by A68, FUNCT_1:49
.=
s1 . a
by A65, A71, A72, SCMFSA_2:67
.=
(DataPart s1) . a
by A69, FUNCT_1:49
.=
s2 . a
by A1, A69, FUNCT_1:49
.=
(Exec (i,s2)) . a
by A65, A71, A72, SCMFSA_2:67
.=
((Exec (i,s2)) | ((Data-Locations ) \ {db,da})) . x
by A68, FUNCT_1:49
;
verum end; suppose
x in FinSeq-Locations
;
((Exec (i,s1)) | ((Data-Locations ) \ {db,da})) . x = ((Exec (i,s2)) | ((Data-Locations ) \ {db,da})) . xthen reconsider a =
x as
FinSeq-Location by SCMFSA_2:5;
thus ((Exec (i,s1)) | ((Data-Locations ) \ {db,da})) . x =
(Exec (i,s1)) . a
by A68, FUNCT_1:49
.=
s1 . a
by A65, SCMFSA_2:67
.=
(DataPart s1) . a
by A69, FUNCT_1:49
.=
s2 . a
by A1, A69, FUNCT_1:49
.=
(Exec (i,s2)) . a
by A65, SCMFSA_2:67
.=
((Exec (i,s2)) | ((Data-Locations ) \ {db,da})) . x
by A68, FUNCT_1:49
;
verum end;
end; A73:
dom ((Exec (i,s2)) | ((Data-Locations ) \ {db,da})) = (Data-Locations ) \ {db,da}
by A8, RELAT_1:62;
dom ((Exec (i,s1)) | ((Data-Locations ) \ {db,da})) = (Data-Locations ) \ {db,da}
by A5, RELAT_1:62;
then A74:
(Exec (i,s1)) | ((Data-Locations ) \ {db,da}) = (Exec (i,s2)) | ((Data-Locations ) \ {db,da})
by A73, A67, FUNCT_1:2;
A75:
(Exec (i,s2)) . da = (s2 . db) mod (s2 . da)
by A65, SCMFSA_2:67;
db in Int-Locations
by SCMFSA_2:2;
then A76:
db in Data-Locations
by SCMFSA_2:100, XBOOLE_0:def 3;
then A77:
s1 . db =
(DataPart s1) . db
by FUNCT_1:49
.=
s2 . db
by A1, A76, FUNCT_1:49
;
da in Int-Locations
by SCMFSA_2:2;
then A78:
da in Data-Locations
by SCMFSA_2:100, XBOOLE_0:def 3;
db in Int-Locations
by SCMFSA_2:2;
then
db in Data-Locations
by SCMFSA_2:100, XBOOLE_0:def 3;
then A79:
Data-Locations =
(Data-Locations ) \/ {db,da}
by A78, ZFMISC_1:42
.=
((Data-Locations ) \ {db,da}) \/ {db,da}
by XBOOLE_1:39
;
A80:
(Exec (i,s1)) . da = (s1 . db) mod (s1 . da)
by A65, SCMFSA_2:67;
A81:
(Exec (i,s2)) . db = (s2 . db) div (s2 . da)
by A65, A66, SCMFSA_2:67;
A82:
(Exec (i,s1)) . db = (s1 . db) div (s1 . da)
by A65, A66, SCMFSA_2:67;
da in Int-Locations
by SCMFSA_2:2;
then A83:
da in Data-Locations
by SCMFSA_2:100, XBOOLE_0:def 3;
then s1 . da =
(DataPart s1) . da
by FUNCT_1:49
.=
s2 . da
by A1, A83, FUNCT_1:49
;
then
(Exec (i,s1)) | {db,da} = (Exec (i,s2)) | {db,da}
by A6, A82, A80, A81, A75, A77, GRFUNC_1:30;
hence
DataPart (Exec (i,s1)) = DataPart (Exec (i,s2))
by A79, A74, RELAT_1:150;
verum end; suppose A84:
da = db
;
DataPart (Exec (i,s1)) = DataPart (Exec (i,s2))A85:
for
x being
set st
x in (Data-Locations ) \ {db} holds
((Exec (i,s1)) | ((Data-Locations ) \ {db})) . x = ((Exec (i,s2)) | ((Data-Locations ) \ {db})) . x
proof
let x be
set ;
( x in (Data-Locations ) \ {db} implies ((Exec (i,s1)) | ((Data-Locations ) \ {db})) . x = ((Exec (i,s2)) | ((Data-Locations ) \ {db})) . x )
assume A86:
x in (Data-Locations ) \ {db}
;
((Exec (i,s1)) | ((Data-Locations ) \ {db})) . x = ((Exec (i,s2)) | ((Data-Locations ) \ {db})) . x
then A87:
x in Data-Locations
by XBOOLE_0:def 5;
A88:
not
x in {db}
by A86, XBOOLE_0:def 5;
per cases
( x in Int-Locations or x in FinSeq-Locations )
by A87, SCMFSA_2:100, XBOOLE_0:def 3;
suppose
x in Int-Locations
;
((Exec (i,s1)) | ((Data-Locations ) \ {db})) . x = ((Exec (i,s2)) | ((Data-Locations ) \ {db})) . xthen reconsider a =
x as
Int-Location by SCMFSA_2:4;
A89:
a <> db
by A88, TARSKI:def 1;
thus ((Exec (i,s1)) | ((Data-Locations ) \ {db})) . x =
(Exec (i,s1)) . a
by A86, FUNCT_1:49
.=
s1 . a
by A65, A84, A89, SCMFSA_2:68
.=
(DataPart s1) . a
by A87, FUNCT_1:49
.=
s2 . a
by A1, A87, FUNCT_1:49
.=
(Exec (i,s2)) . a
by A65, A84, A89, SCMFSA_2:68
.=
((Exec (i,s2)) | ((Data-Locations ) \ {db})) . x
by A86, FUNCT_1:49
;
verum end; suppose
x in FinSeq-Locations
;
((Exec (i,s1)) | ((Data-Locations ) \ {db})) . x = ((Exec (i,s2)) | ((Data-Locations ) \ {db})) . xthen reconsider a =
x as
FinSeq-Location by SCMFSA_2:5;
thus ((Exec (i,s1)) | ((Data-Locations ) \ {db})) . x =
(Exec (i,s1)) . a
by A86, FUNCT_1:49
.=
s1 . a
by A65, A84, SCMFSA_2:68
.=
(s1 | (Data-Locations )) . a
by A87, FUNCT_1:49
.=
s2 . a
by A1, A87, FUNCT_1:49
.=
(Exec (i,s2)) . a
by A65, A84, SCMFSA_2:68
.=
((Exec (i,s2)) | ((Data-Locations ) \ {db})) . x
by A86, FUNCT_1:49
;
verum end;
end; A90:
dom ((Exec (i,s2)) | ((Data-Locations ) \ {db})) = (Data-Locations ) \ {db}
by A8, RELAT_1:62;
dom ((Exec (i,s1)) | ((Data-Locations ) \ {db})) = (Data-Locations ) \ {db}
by A5, RELAT_1:62;
then A91:
(Exec (i,s1)) | ((Data-Locations ) \ {db}) = (Exec (i,s2)) | ((Data-Locations ) \ {db})
by A90, A85, FUNCT_1:2;
db in Int-Locations
by SCMFSA_2:2;
then
db in Data-Locations
by SCMFSA_2:100, XBOOLE_0:def 3;
then A92:
Data-Locations =
(Data-Locations ) \/ {db}
by ZFMISC_1:40
.=
((Data-Locations ) \ {db}) \/ {db}
by XBOOLE_1:39
;
A93:
(Exec (i,s2)) . db = (s2 . db) mod (s2 . da)
by A65, A84, SCMFSA_2:68;
A94:
(Exec (i,s1)) . db = (s1 . db) mod (s1 . da)
by A65, A84, SCMFSA_2:68;
db in Int-Locations
by SCMFSA_2:2;
then A95:
db in Data-Locations
by SCMFSA_2:100, XBOOLE_0:def 3;
then A96:
s1 . db =
(DataPart s1) . db
by FUNCT_1:49
.=
s2 . db
by A1, A95, FUNCT_1:49
;
da in Int-Locations
by SCMFSA_2:2;
then A97:
da in Data-Locations
by SCMFSA_2:100, XBOOLE_0:def 3;
then s1 . da =
(DataPart s1) . da
by FUNCT_1:49
.=
s2 . da
by A1, A97, FUNCT_1:49
;
then
(Exec (i,s1)) | {db} = (Exec (i,s2)) | {db}
by A6, A94, A93, A96, GRFUNC_1:29;
hence
DataPart (Exec (i,s1)) = DataPart (Exec (i,s2))
by A92, A91, RELAT_1:150;
verum end; end; suppose
InsCode i = 6
;
DataPart (Exec (i,s1)) = DataPart (Exec (i,s2))then A98:
ex
l1 being
Element of
NAT st
i = goto l1
by SCMFSA_2:35;
for
x being
set st
x in Data-Locations holds
(DataPart (Exec (i,s1))) . x = (DataPart (Exec (i,s2))) . x
proof
let x be
set ;
( x in Data-Locations implies (DataPart (Exec (i,s1))) . x = (DataPart (Exec (i,s2))) . x )
assume A99:
x in Data-Locations
;
(DataPart (Exec (i,s1))) . x = (DataPart (Exec (i,s2))) . x
per cases
( x in Int-Locations or x in FinSeq-Locations )
by A99, SCMFSA_2:100, XBOOLE_0:def 3;
suppose
x in Int-Locations
;
(DataPart (Exec (i,s1))) . x = (DataPart (Exec (i,s2))) . xthen reconsider a =
x as
Int-Location by SCMFSA_2:4;
thus (DataPart (Exec (i,s1))) . x =
(Exec (i,s1)) . a
by A99, FUNCT_1:49
.=
s1 . a
by A98, SCMFSA_2:69
.=
(DataPart s1) . a
by A99, FUNCT_1:49
.=
s2 . a
by A1, A99, FUNCT_1:49
.=
(Exec (i,s2)) . a
by A98, SCMFSA_2:69
.=
(DataPart (Exec (i,s2))) . x
by A99, FUNCT_1:49
;
verum end; suppose
x in FinSeq-Locations
;
(DataPart (Exec (i,s1))) . x = (DataPart (Exec (i,s2))) . xthen reconsider a =
x as
FinSeq-Location by SCMFSA_2:5;
thus (DataPart (Exec (i,s1))) . x =
(Exec (i,s1)) . a
by A99, FUNCT_1:49
.=
s1 . a
by A98, SCMFSA_2:69
.=
(DataPart s1) . a
by A99, FUNCT_1:49
.=
s2 . a
by A1, A99, FUNCT_1:49
.=
(Exec (i,s2)) . a
by A98, SCMFSA_2:69
.=
(DataPart (Exec (i,s2))) . x
by A99, FUNCT_1:49
;
verum end;
end; hence
DataPart (Exec (i,s1)) = DataPart (Exec (i,s2))
by A7, A9, FUNCT_1:2;
verum end; suppose
InsCode i = 7
;
DataPart (Exec (i,s1)) = DataPart (Exec (i,s2))then A100:
ex
l1 being
Element of
NAT ex
a being
Int-Location st
i = a =0_goto l1
by SCMFSA_2:36;
for
x being
set st
x in Data-Locations holds
(DataPart (Exec (i,s1))) . x = (DataPart (Exec (i,s2))) . x
proof
let x be
set ;
( x in Data-Locations implies (DataPart (Exec (i,s1))) . x = (DataPart (Exec (i,s2))) . x )
assume A101:
x in Data-Locations
;
(DataPart (Exec (i,s1))) . x = (DataPart (Exec (i,s2))) . x
per cases
( x in Int-Locations or x in FinSeq-Locations )
by A101, SCMFSA_2:100, XBOOLE_0:def 3;
suppose
x in Int-Locations
;
(DataPart (Exec (i,s1))) . x = (DataPart (Exec (i,s2))) . xthen reconsider a =
x as
Int-Location by SCMFSA_2:4;
thus (DataPart (Exec (i,s1))) . x =
(Exec (i,s1)) . a
by A101, FUNCT_1:49
.=
s1 . a
by A100, SCMFSA_2:70
.=
(DataPart s1) . a
by A101, FUNCT_1:49
.=
s2 . a
by A1, A101, FUNCT_1:49
.=
(Exec (i,s2)) . a
by A100, SCMFSA_2:70
.=
(DataPart (Exec (i,s2))) . x
by A101, FUNCT_1:49
;
verum end; suppose
x in FinSeq-Locations
;
(DataPart (Exec (i,s1))) . x = (DataPart (Exec (i,s2))) . xthen reconsider a =
x as
FinSeq-Location by SCMFSA_2:5;
thus (DataPart (Exec (i,s1))) . x =
(Exec (i,s1)) . a
by A101, FUNCT_1:49
.=
s1 . a
by A100, SCMFSA_2:70
.=
(DataPart s1) . a
by A101, FUNCT_1:49
.=
s2 . a
by A1, A101, FUNCT_1:49
.=
(Exec (i,s2)) . a
by A100, SCMFSA_2:70
.=
(DataPart (Exec (i,s2))) . x
by A101, FUNCT_1:49
;
verum end;
end; hence
DataPart (Exec (i,s1)) = DataPart (Exec (i,s2))
by A7, A9, FUNCT_1:2;
verum end; suppose
InsCode i = 8
;
DataPart (Exec (i,s1)) = DataPart (Exec (i,s2))then A102:
ex
l1 being
Element of
NAT ex
a being
Int-Location st
i = a >0_goto l1
by SCMFSA_2:37;
for
x being
set st
x in Data-Locations holds
(DataPart (Exec (i,s1))) . x = (DataPart (Exec (i,s2))) . x
proof
let x be
set ;
( x in Data-Locations implies (DataPart (Exec (i,s1))) . x = (DataPart (Exec (i,s2))) . x )
assume A103:
x in Data-Locations
;
(DataPart (Exec (i,s1))) . x = (DataPart (Exec (i,s2))) . x
per cases
( x in Int-Locations or x in FinSeq-Locations )
by A103, SCMFSA_2:100, XBOOLE_0:def 3;
suppose
x in Int-Locations
;
(DataPart (Exec (i,s1))) . x = (DataPart (Exec (i,s2))) . xthen reconsider a =
x as
Int-Location by SCMFSA_2:4;
thus (DataPart (Exec (i,s1))) . x =
(Exec (i,s1)) . a
by A103, FUNCT_1:49
.=
s1 . a
by A102, SCMFSA_2:71
.=
(DataPart s1) . a
by A103, FUNCT_1:49
.=
s2 . a
by A1, A103, FUNCT_1:49
.=
(Exec (i,s2)) . a
by A102, SCMFSA_2:71
.=
(DataPart (Exec (i,s2))) . x
by A103, FUNCT_1:49
;
verum end; suppose
x in FinSeq-Locations
;
(DataPart (Exec (i,s1))) . x = (DataPart (Exec (i,s2))) . xthen reconsider a =
x as
FinSeq-Location by SCMFSA_2:5;
thus (DataPart (Exec (i,s1))) . x =
(Exec (i,s1)) . a
by A103, FUNCT_1:49
.=
s1 . a
by A102, SCMFSA_2:71
.=
(DataPart s1) . a
by A103, FUNCT_1:49
.=
s2 . a
by A1, A103, FUNCT_1:49
.=
(Exec (i,s2)) . a
by A102, SCMFSA_2:71
.=
(DataPart (Exec (i,s2))) . x
by A103, FUNCT_1:49
;
verum end;
end; hence
DataPart (Exec (i,s1)) = DataPart (Exec (i,s2))
by A7, A9, FUNCT_1:2;
verum end; suppose
InsCode i = 9
;
DataPart (Exec (i,s1)) = DataPart (Exec (i,s2))then consider da,
db being
Int-Location ,
fa being
FinSeq-Location such that A104:
i = db := (
fa,
da)
by SCMFSA_2:38;
A105:
for
x being
set st
x in (Data-Locations ) \ {db} holds
((Exec (i,s1)) | ((Data-Locations ) \ {db})) . x = ((Exec (i,s2)) | ((Data-Locations ) \ {db})) . x
proof
let x be
set ;
( x in (Data-Locations ) \ {db} implies ((Exec (i,s1)) | ((Data-Locations ) \ {db})) . x = ((Exec (i,s2)) | ((Data-Locations ) \ {db})) . x )
assume A106:
x in (Data-Locations ) \ {db}
;
((Exec (i,s1)) | ((Data-Locations ) \ {db})) . x = ((Exec (i,s2)) | ((Data-Locations ) \ {db})) . x
then A107:
x in Data-Locations
by XBOOLE_0:def 5;
A108:
not
x in {db}
by A106, XBOOLE_0:def 5;
per cases
( x in Int-Locations or x in FinSeq-Locations )
by A107, SCMFSA_2:100, XBOOLE_0:def 3;
suppose
x in Int-Locations
;
((Exec (i,s1)) | ((Data-Locations ) \ {db})) . x = ((Exec (i,s2)) | ((Data-Locations ) \ {db})) . xthen reconsider a =
x as
Int-Location by SCMFSA_2:4;
A109:
a <> db
by A108, TARSKI:def 1;
thus ((Exec (i,s1)) | ((Data-Locations ) \ {db})) . x =
(Exec (i,s1)) . a
by A106, FUNCT_1:49
.=
s1 . a
by A104, A109, SCMFSA_2:72
.=
(DataPart s1) . a
by A107, FUNCT_1:49
.=
s2 . a
by A1, A107, FUNCT_1:49
.=
(Exec (i,s2)) . a
by A104, A109, SCMFSA_2:72
.=
((Exec (i,s2)) | ((Data-Locations ) \ {db})) . x
by A106, FUNCT_1:49
;
verum end; suppose
x in FinSeq-Locations
;
((Exec (i,s1)) | ((Data-Locations ) \ {db})) . x = ((Exec (i,s2)) | ((Data-Locations ) \ {db})) . xthen reconsider a =
x as
FinSeq-Location by SCMFSA_2:5;
thus ((Exec (i,s1)) | ((Data-Locations ) \ {db})) . x =
(Exec (i,s1)) . a
by A106, FUNCT_1:49
.=
s1 . a
by A104, SCMFSA_2:72
.=
(DataPart s1) . a
by A107, FUNCT_1:49
.=
s2 . a
by A1, A107, FUNCT_1:49
.=
(Exec (i,s2)) . a
by A104, SCMFSA_2:72
.=
((Exec (i,s2)) | ((Data-Locations ) \ {db})) . x
by A106, FUNCT_1:49
;
verum end;
end; A110:
dom ((Exec (i,s2)) | ((Data-Locations ) \ {db})) = (Data-Locations ) \ {db}
by A8, RELAT_1:62;
dom ((Exec (i,s1)) | ((Data-Locations ) \ {db})) = (Data-Locations ) \ {db}
by A5, RELAT_1:62;
then A111:
(Exec (i,s1)) | ((Data-Locations ) \ {db}) = (Exec (i,s2)) | ((Data-Locations ) \ {db})
by A110, A105, FUNCT_1:2;
db in Int-Locations
by SCMFSA_2:2;
then
db in Data-Locations
by SCMFSA_2:100, XBOOLE_0:def 3;
then A112:
Data-Locations =
(Data-Locations ) \/ {db}
by ZFMISC_1:40
.=
((Data-Locations ) \ {db}) \/ {db}
by XBOOLE_1:39
;
A113:
ex
k2 being
Element of
NAT st
(
k2 = abs (s2 . da) &
(Exec (i,s2)) . db = (s2 . fa) /. k2 )
by A104, SCMFSA_2:72;
A114:
ex
k1 being
Element of
NAT st
(
k1 = abs (s1 . da) &
(Exec (i,s1)) . db = (s1 . fa) /. k1 )
by A104, SCMFSA_2:72;
fa in FinSeq-Locations
by SCMFSA_2:3;
then A115:
fa in Data-Locations
by SCMFSA_2:100, XBOOLE_0:def 3;
then A116:
s1 . fa =
(DataPart s1) . fa
by FUNCT_1:49
.=
s2 . fa
by A1, A115, FUNCT_1:49
;
da in Int-Locations
by SCMFSA_2:2;
then A117:
da in Data-Locations
by SCMFSA_2:100, XBOOLE_0:def 3;
then s1 . da =
(DataPart s1) . da
by FUNCT_1:49
.=
s2 . da
by A1, A117, FUNCT_1:49
;
then
(Exec (i,s1)) | {db} = (Exec (i,s2)) | {db}
by A6, A114, A113, A116, GRFUNC_1:29;
hence
DataPart (Exec (i,s1)) = DataPart (Exec (i,s2))
by A112, A111, RELAT_1:150;
verum end; suppose
InsCode i = 10
;
DataPart (Exec (i,s1)) = DataPart (Exec (i,s2))then consider da,
db being
Int-Location ,
fa being
FinSeq-Location such that A118:
i = (
fa,
da)
:= db
by SCMFSA_2:39;
A119:
for
x being
set st
x in (Data-Locations ) \ {fa} holds
((Exec (i,s1)) | ((Data-Locations ) \ {fa})) . x = ((Exec (i,s2)) | ((Data-Locations ) \ {fa})) . x
proof
let x be
set ;
( x in (Data-Locations ) \ {fa} implies ((Exec (i,s1)) | ((Data-Locations ) \ {fa})) . x = ((Exec (i,s2)) | ((Data-Locations ) \ {fa})) . x )
assume A120:
x in (Data-Locations ) \ {fa}
;
((Exec (i,s1)) | ((Data-Locations ) \ {fa})) . x = ((Exec (i,s2)) | ((Data-Locations ) \ {fa})) . x
then A121:
x in Data-Locations
by XBOOLE_0:def 5;
A122:
not
x in {fa}
by A120, XBOOLE_0:def 5;
per cases
( x in Int-Locations or x in FinSeq-Locations )
by A121, SCMFSA_2:100, XBOOLE_0:def 3;
suppose
x in Int-Locations
;
((Exec (i,s1)) | ((Data-Locations ) \ {fa})) . x = ((Exec (i,s2)) | ((Data-Locations ) \ {fa})) . xthen reconsider a =
x as
Int-Location by SCMFSA_2:4;
thus ((Exec (i,s1)) | ((Data-Locations ) \ {fa})) . x =
(Exec (i,s1)) . a
by A120, FUNCT_1:49
.=
s1 . a
by A118, SCMFSA_2:73
.=
(DataPart s1) . a
by A121, FUNCT_1:49
.=
s2 . a
by A1, A121, FUNCT_1:49
.=
(Exec (i,s2)) . a
by A118, SCMFSA_2:73
.=
((Exec (i,s2)) | ((Data-Locations ) \ {fa})) . x
by A120, FUNCT_1:49
;
verum end; suppose
x in FinSeq-Locations
;
((Exec (i,s1)) | ((Data-Locations ) \ {fa})) . x = ((Exec (i,s2)) | ((Data-Locations ) \ {fa})) . xthen reconsider a =
x as
FinSeq-Location by SCMFSA_2:5;
A123:
a <> fa
by A122, TARSKI:def 1;
thus ((Exec (i,s1)) | ((Data-Locations ) \ {fa})) . x =
(Exec (i,s1)) . a
by A120, FUNCT_1:49
.=
s1 . a
by A118, A123, SCMFSA_2:73
.=
(DataPart s1) . a
by A121, FUNCT_1:49
.=
s2 . a
by A1, A121, FUNCT_1:49
.=
(Exec (i,s2)) . a
by A118, A123, SCMFSA_2:73
.=
((Exec (i,s2)) | ((Data-Locations ) \ {fa})) . x
by A120, FUNCT_1:49
;
verum end;
end; A124:
dom ((Exec (i,s2)) | ((Data-Locations ) \ {fa})) = (Data-Locations ) \ {fa}
by A8, RELAT_1:62;
dom ((Exec (i,s1)) | ((Data-Locations ) \ {fa})) = (Data-Locations ) \ {fa}
by A5, RELAT_1:62;
then A125:
(Exec (i,s1)) | ((Data-Locations ) \ {fa}) = (Exec (i,s2)) | ((Data-Locations ) \ {fa})
by A124, A119, FUNCT_1:2;
fa in FinSeq-Locations
by SCMFSA_2:3;
then
fa in Data-Locations
by SCMFSA_2:100, XBOOLE_0:def 3;
then A126:
Data-Locations =
(Data-Locations ) \/ {fa}
by ZFMISC_1:40
.=
((Data-Locations ) \ {fa}) \/ {fa}
by XBOOLE_1:39
;
fa in FinSeq-Locations
by SCMFSA_2:3;
then A127:
fa in Data-Locations
by SCMFSA_2:100, XBOOLE_0:def 3;
then A128:
s1 . fa =
(DataPart s1) . fa
by FUNCT_1:49
.=
s2 . fa
by A1, A127, FUNCT_1:49
;
db in Int-Locations
by SCMFSA_2:2;
then A129:
db in Data-Locations
by SCMFSA_2:100, XBOOLE_0:def 3;
then A130:
s1 . db =
(DataPart s1) . db
by FUNCT_1:49
.=
s2 . db
by A1, A129, FUNCT_1:49
;
A131:
ex
k2 being
Element of
NAT st
(
k2 = abs (s2 . da) &
(Exec (i,s2)) . fa = (s2 . fa) +* (
k2,
(s2 . db)) )
by A118, SCMFSA_2:73;
A132:
ex
k1 being
Element of
NAT st
(
k1 = abs (s1 . da) &
(Exec (i,s1)) . fa = (s1 . fa) +* (
k1,
(s1 . db)) )
by A118, SCMFSA_2:73;
da in Int-Locations
by SCMFSA_2:2;
then A133:
da in Data-Locations
by SCMFSA_2:100, XBOOLE_0:def 3;
then s1 . da =
(DataPart s1) . da
by FUNCT_1:49
.=
s2 . da
by A1, A133, FUNCT_1:49
;
then
(Exec (i,s1)) | {fa} = (Exec (i,s2)) | {fa}
by A6, A132, A131, A130, A128, GRFUNC_1:29;
hence
DataPart (Exec (i,s1)) = DataPart (Exec (i,s2))
by A126, A125, RELAT_1:150;
verum end; suppose
InsCode i = 11
;
DataPart (Exec (i,s1)) = DataPart (Exec (i,s2))then consider da being
Int-Location ,
fa being
FinSeq-Location such that A134:
i = da :=len fa
by SCMFSA_2:40;
A135:
for
x being
set st
x in (Data-Locations ) \ {da} holds
((Exec (i,s1)) | ((Data-Locations ) \ {da})) . x = ((Exec (i,s2)) | ((Data-Locations ) \ {da})) . x
proof
let x be
set ;
( x in (Data-Locations ) \ {da} implies ((Exec (i,s1)) | ((Data-Locations ) \ {da})) . x = ((Exec (i,s2)) | ((Data-Locations ) \ {da})) . x )
assume A136:
x in (Data-Locations ) \ {da}
;
((Exec (i,s1)) | ((Data-Locations ) \ {da})) . x = ((Exec (i,s2)) | ((Data-Locations ) \ {da})) . x
then A137:
x in Data-Locations
by XBOOLE_0:def 5;
A138:
not
x in {da}
by A136, XBOOLE_0:def 5;
per cases
( x in Int-Locations or x in FinSeq-Locations )
by A137, SCMFSA_2:100, XBOOLE_0:def 3;
suppose
x in Int-Locations
;
((Exec (i,s1)) | ((Data-Locations ) \ {da})) . x = ((Exec (i,s2)) | ((Data-Locations ) \ {da})) . xthen reconsider a =
x as
Int-Location by SCMFSA_2:4;
A139:
a <> da
by A138, TARSKI:def 1;
thus ((Exec (i,s1)) | ((Data-Locations ) \ {da})) . x =
(Exec (i,s1)) . a
by A136, FUNCT_1:49
.=
s1 . a
by A134, A139, SCMFSA_2:74
.=
(DataPart s1) . a
by A137, FUNCT_1:49
.=
s2 . a
by A1, A137, FUNCT_1:49
.=
(Exec (i,s2)) . a
by A134, A139, SCMFSA_2:74
.=
((Exec (i,s2)) | ((Data-Locations ) \ {da})) . x
by A136, FUNCT_1:49
;
verum end; suppose
x in FinSeq-Locations
;
((Exec (i,s1)) | ((Data-Locations ) \ {da})) . x = ((Exec (i,s2)) | ((Data-Locations ) \ {da})) . xthen reconsider a =
x as
FinSeq-Location by SCMFSA_2:5;
thus ((Exec (i,s1)) | ((Data-Locations ) \ {da})) . x =
(Exec (i,s1)) . a
by A136, FUNCT_1:49
.=
s1 . a
by A134, SCMFSA_2:74
.=
(DataPart s1) . a
by A137, FUNCT_1:49
.=
s2 . a
by A1, A137, FUNCT_1:49
.=
(Exec (i,s2)) . a
by A134, SCMFSA_2:74
.=
((Exec (i,s2)) | ((Data-Locations ) \ {da})) . x
by A136, FUNCT_1:49
;
verum end;
end;
da in Int-Locations
by SCMFSA_2:2;
then
da in Data-Locations
by SCMFSA_2:100, XBOOLE_0:def 3;
then A140:
Data-Locations =
(Data-Locations ) \/ {da}
by ZFMISC_1:40
.=
((Data-Locations ) \ {da}) \/ {da}
by XBOOLE_1:39
;
fa in FinSeq-Locations
by SCMFSA_2:3;
then A141:
fa in Data-Locations
by SCMFSA_2:100, XBOOLE_0:def 3;
then s1 . fa =
(s1 | (Data-Locations )) . fa
by FUNCT_1:49
.=
s2 . fa
by A1, A141, FUNCT_1:49
;
then (Exec (i,s1)) . da =
len (s2 . fa)
by A134, SCMFSA_2:74
.=
(Exec (i,s2)) . da
by A134, SCMFSA_2:74
;
then A142:
(Exec (i,s1)) | {da} = (Exec (i,s2)) | {da}
by A5, A8, GRFUNC_1:29;
A143:
dom ((Exec (i,s2)) | ((Data-Locations ) \ {da})) = (Data-Locations ) \ {da}
by A8, RELAT_1:62;
dom ((Exec (i,s1)) | ((Data-Locations ) \ {da})) = (Data-Locations ) \ {da}
by A5, RELAT_1:62;
then
(Exec (i,s1)) | ((Data-Locations ) \ {da}) = (Exec (i,s2)) | ((Data-Locations ) \ {da})
by A143, A135, FUNCT_1:2;
hence
DataPart (Exec (i,s1)) = DataPart (Exec (i,s2))
by A140, A142, RELAT_1:150;
verum end; suppose
InsCode i = 12
;
DataPart (Exec (i,s1)) = DataPart (Exec (i,s2))then consider da being
Int-Location ,
fa being
FinSeq-Location such that A144:
i = fa :=<0,...,0> da
by SCMFSA_2:41;
set l =
i;
A145:
dom ((Exec (i,s2)) | ((Data-Locations ) \ {fa})) = (Data-Locations ) \ {fa}
by A8, RELAT_1:62;
A146:
ex
k2 being
Element of
NAT st
(
k2 = abs (s2 . da) &
(Exec (i,s2)) . fa = k2 |-> 0 )
by A144, SCMFSA_2:75;
A147:
ex
k1 being
Element of
NAT st
(
k1 = abs (s1 . da) &
(Exec (i,s1)) . fa = k1 |-> 0 )
by A144, SCMFSA_2:75;
A148:
for
x being
set st
x in (Data-Locations ) \ {fa} holds
((Exec (i,s1)) | ((Data-Locations ) \ {fa})) . x = ((Exec (i,s2)) | ((Data-Locations ) \ {fa})) . x
proof
let x be
set ;
( x in (Data-Locations ) \ {fa} implies ((Exec (i,s1)) | ((Data-Locations ) \ {fa})) . x = ((Exec (i,s2)) | ((Data-Locations ) \ {fa})) . x )
assume A149:
x in (Data-Locations ) \ {fa}
;
((Exec (i,s1)) | ((Data-Locations ) \ {fa})) . x = ((Exec (i,s2)) | ((Data-Locations ) \ {fa})) . x
then A150:
x in Data-Locations
by XBOOLE_0:def 5;
A151:
not
x in {fa}
by A149, XBOOLE_0:def 5;
per cases
( x in Int-Locations or x in FinSeq-Locations )
by A150, SCMFSA_2:100, XBOOLE_0:def 3;
suppose
x in Int-Locations
;
((Exec (i,s1)) | ((Data-Locations ) \ {fa})) . x = ((Exec (i,s2)) | ((Data-Locations ) \ {fa})) . xthen reconsider a =
x as
Int-Location by SCMFSA_2:4;
thus ((Exec (i,s1)) | ((Data-Locations ) \ {fa})) . x =
(Exec (i,s1)) . a
by A149, FUNCT_1:49
.=
s1 . a
by A144, SCMFSA_2:75
.=
(DataPart s1) . a
by A150, FUNCT_1:49
.=
s2 . a
by A1, A150, FUNCT_1:49
.=
(Exec (i,s2)) . a
by A144, SCMFSA_2:75
.=
((Exec (i,s2)) | ((Data-Locations ) \ {fa})) . x
by A149, FUNCT_1:49
;
verum end; suppose
x in FinSeq-Locations
;
((Exec (i,s1)) | ((Data-Locations ) \ {fa})) . x = ((Exec (i,s2)) | ((Data-Locations ) \ {fa})) . xthen reconsider a =
x as
FinSeq-Location by SCMFSA_2:5;
A152:
a <> fa
by A151, TARSKI:def 1;
thus ((Exec (i,s1)) | ((Data-Locations ) \ {fa})) . x =
(Exec (i,s1)) . a
by A149, FUNCT_1:49
.=
s1 . a
by A144, A152, SCMFSA_2:75
.=
(DataPart s1) . a
by A150, FUNCT_1:49
.=
s2 . a
by A1, A150, FUNCT_1:49
.=
(Exec (i,s2)) . a
by A144, A152, SCMFSA_2:75
.=
((Exec (i,s2)) | ((Data-Locations ) \ {fa})) . x
by A149, FUNCT_1:49
;
verum end;
end;
dom ((Exec (i,s1)) | ((Data-Locations ) \ {fa})) = (Data-Locations ) \ {fa}
by A5, RELAT_1:62;
then A153:
(Exec (i,s1)) | ((Data-Locations ) \ {fa}) = (Exec (i,s2)) | ((Data-Locations ) \ {fa})
by A145, A148, FUNCT_1:2;
fa in FinSeq-Locations
by SCMFSA_2:3;
then
fa in Data-Locations
by SCMFSA_2:100, XBOOLE_0:def 3;
then A154:
Data-Locations =
(Data-Locations ) \/ {fa}
by ZFMISC_1:40
.=
((Data-Locations ) \ {fa}) \/ {fa}
by XBOOLE_1:39
;
da in Int-Locations
by SCMFSA_2:2;
then A155:
da in Data-Locations
by SCMFSA_2:100, XBOOLE_0:def 3;
then s1 . da =
(DataPart s1) . da
by FUNCT_1:49
.=
s2 . da
by A1, A155, FUNCT_1:49
;
then
(Exec (i,s1)) | {fa} = (Exec (i,s2)) | {fa}
by A6, A147, A146, GRFUNC_1:29;
hence
DataPart (Exec (i,s1)) = DataPart (Exec (i,s2))
by A154, A153, RELAT_1:150;
verum end;