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