let i be Instruction of SCM+FSA ; :: thesis: 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 ; :: thesis: ( DataPart s1 = DataPart s2 implies DataPart (Exec i,s1) = DataPart (Exec i,s2) )
assume A1: DataPart s1 = DataPart s2 ; :: thesis: DataPart (Exec i,s1) = DataPart (Exec i,s2)
A2: ( not InsCode i <= 9 + 1 or InsCode i <= 8 + 1 or InsCode i = 10 ) by NAT_1:8;
A3: ( not InsCode i <= 10 + 1 or InsCode i <= 10 or InsCode i = 11 ) by NAT_1:8;
set l = i;
A4: InsCode i <= 11 + 1 by SCMFSA_2:35;
A5: dom (Exec i,s1) = the carrier of SCM+FSA by PARTFUN1:def 4;
then A6: dom (Exec i,s1) = dom (Exec i,s2) by PARTFUN1:def 4;
A7: dom ((Exec i,s1) | (Int-Locations \/ FinSeq-Locations )) = Int-Locations \/ FinSeq-Locations by A5, RELAT_1:91;
A8: dom (Exec i,s2) = the carrier of SCM+FSA by PARTFUN1:def 4;
then A9: dom ((Exec i,s2) | (Int-Locations \/ FinSeq-Locations )) = Int-Locations \/ FinSeq-Locations by RELAT_1:91;

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 A4, A3, A2, NAT_1:8, NAT_1:33;

suppose InsCode i = 0 ; :: thesis: DataPart (Exec i,s1) = DataPart (Exec i,s2)

then A10: i = halt SCM+FSA by SCMFSA_2:122;
then Exec i,s1 = s1 by AMI_1:def 8;
hence DataPart (Exec i,s1) = DataPart (Exec i,s2) by A1, A10, AMI_1:def 8; :: thesis: verum

end;

suppose InsCode i = 1 ; :: thesis: DataPart (Exec i,s1) = DataPart (Exec i,s2)

then consider db, da being Int-Location such that
A11: i = db := da by SCMFSA_2:54;
A12: for x being set st x in (Int-Locations \/ FinSeq-Locations ) \ {db} holds
((Exec i,s1) | ((Int-Locations \/ FinSeq-Locations ) \ {db})) . x = ((Exec i,s2) | ((Int-Locations \/ FinSeq-Locations ) \ {db})) . x

proof

let x be set ; :: thesis: ( x in (Int-Locations \/ FinSeq-Locations ) \ {db} implies ((Exec i,s1) | ((Int-Locations \/ FinSeq-Locations ) \ {db})) . x = ((Exec i,s2) | ((Int-Locations \/ FinSeq-Locations ) \ {db})) . x )
assume A13: x in (Int-Locations \/ FinSeq-Locations ) \ {db} ; :: thesis: ((Exec i,s1) | ((Int-Locations \/ FinSeq-Locations ) \ {db})) . x = ((Exec i,s2) | ((Int-Locations \/ FinSeq-Locations ) \ {db})) . x
then A14: x in Int-Locations \/ FinSeq-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, XBOOLE_0:def 3;

suppose x in Int-Locations ; :: thesis: ((Exec i,s1) | ((Int-Locations \/ FinSeq-Locations ) \ {db})) . x = ((Exec i,s2) | ((Int-Locations \/ FinSeq-Locations ) \ {db})) . x

then reconsider a = x as Int-Location by SCMFSA_2:11;
A16: a <> db by A15, TARSKI:def 1;
thus ((Exec i,s1) | ((Int-Locations \/ FinSeq-Locations ) \ {db})) . x = (Exec i,s1) . a by A13, FUNCT_1:72
.= s1 . a by A11, A16, SCMFSA_2:89
.= (DataPart s1) . a by A14, FUNCT_1:72, SCMFSA_2:127
.= s2 . a by A1, A14, FUNCT_1:72, SCMFSA_2:127
.= (Exec i,s2) . a by A11, A16, SCMFSA_2:89
.= ((Exec i,s2) | ((Int-Locations \/ FinSeq-Locations ) \ {db})) . x by A13, FUNCT_1:72 ; :: thesis: verum

end;

suppose x in FinSeq-Locations ; :: thesis: ((Exec i,s1) | ((Int-Locations \/ FinSeq-Locations ) \ {db})) . x = ((Exec i,s2) | ((Int-Locations \/ FinSeq-Locations ) \ {db})) . x

then reconsider a = x as FinSeq-Location by SCMFSA_2:12;
thus ((Exec i,s1) | ((Int-Locations \/ FinSeq-Locations ) \ {db})) . x = (Exec i,s1) . a by A13, FUNCT_1:72
.= s1 . a by A11, SCMFSA_2:89
.= (DataPart s1) . a by A14, FUNCT_1:72, SCMFSA_2:127
.= s2 . a by A1, A14, FUNCT_1:72, SCMFSA_2:127
.= (Exec i,s2) . a by A11, SCMFSA_2:89
.= ((Exec i,s2) | ((Int-Locations \/ FinSeq-Locations ) \ {db})) . x by A13, FUNCT_1:72 ; :: thesis: verum

end;

end;

end;

A17: dom ((Exec i,s2) | ((Int-Locations \/ FinSeq-Locations ) \ {db})) = (Int-Locations \/ FinSeq-Locations ) \ {db} by A8, RELAT_1:91;
dom ((Exec i,s1) | ((Int-Locations \/ FinSeq-Locations ) \ {db})) = (Int-Locations \/ FinSeq-Locations ) \ {db} by A5, RELAT_1:91;
then A18: (Exec i,s1) | ((Int-Locations \/ FinSeq-Locations ) \ {db}) = (Exec i,s2) | ((Int-Locations \/ FinSeq-Locations ) \ {db}) by A17, A12, FUNCT_1:9;
db in Int-Locations by SCMFSA_2:9;
then db in Int-Locations \/ FinSeq-Locations by XBOOLE_0:def 3;
then A19: Int-Locations \/ FinSeq-Locations = (Int-Locations \/ FinSeq-Locations ) \/ {db} by ZFMISC_1:46
.= ((Int-Locations \/ FinSeq-Locations ) \ {db}) \/ {db} by XBOOLE_1:39 ;
A20: (Exec i,s2) . db = s2 . da by A11, SCMFSA_2:89;
A21: (Exec i,s1) . db = s1 . da by A11, SCMFSA_2:89;
da in Int-Locations by SCMFSA_2:9;
then A22: da in Int-Locations \/ FinSeq-Locations by XBOOLE_0:def 3;
then s1 . da = (DataPart s1) . da by FUNCT_1:72, SCMFSA_2:127
.= s2 . da by A1, A22, FUNCT_1:72, SCMFSA_2:127 ;
then (Exec i,s1) | {db} = (Exec i,s2) | {db} by A6, A21, A20, GRFUNC_1:90;
hence DataPart (Exec i,s1) = DataPart (Exec i,s2) by A19, A18, RELAT_1:185, SCMFSA_2:127; :: thesis: verum

end;

suppose InsCode i = 2 ; :: thesis: 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:55;
A24: for x being set st x in (Int-Locations \/ FinSeq-Locations ) \ {db} holds
((Exec i,s1) | ((Int-Locations \/ FinSeq-Locations ) \ {db})) . x = ((Exec i,s2) | ((Int-Locations \/ FinSeq-Locations ) \ {db})) . x

proof

let x be set ; :: thesis: ( x in (Int-Locations \/ FinSeq-Locations ) \ {db} implies ((Exec i,s1) | ((Int-Locations \/ FinSeq-Locations ) \ {db})) . x = ((Exec i,s2) | ((Int-Locations \/ FinSeq-Locations ) \ {db})) . x )
assume A25: x in (Int-Locations \/ FinSeq-Locations ) \ {db} ; :: thesis: ((Exec i,s1) | ((Int-Locations \/ FinSeq-Locations ) \ {db})) . x = ((Exec i,s2) | ((Int-Locations \/ FinSeq-Locations ) \ {db})) . x
then A26: x in Int-Locations \/ FinSeq-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, XBOOLE_0:def 3;

suppose x in Int-Locations ; :: thesis: ((Exec i,s1) | ((Int-Locations \/ FinSeq-Locations ) \ {db})) . x = ((Exec i,s2) | ((Int-Locations \/ FinSeq-Locations ) \ {db})) . x

then reconsider a = x as Int-Location by SCMFSA_2:11;
A28: a <> db by A27, TARSKI:def 1;
thus ((Exec i,s1) | ((Int-Locations \/ FinSeq-Locations ) \ {db})) . x = (Exec i,s1) . a by A25, FUNCT_1:72
.= s1 . a by A23, A28, SCMFSA_2:90
.= (DataPart s1) . a by A26, FUNCT_1:72, SCMFSA_2:127
.= s2 . a by A1, A26, FUNCT_1:72, SCMFSA_2:127
.= (Exec i,s2) . a by A23, A28, SCMFSA_2:90
.= ((Exec i,s2) | ((Int-Locations \/ FinSeq-Locations ) \ {db})) . x by A25, FUNCT_1:72 ; :: thesis: verum

end;

suppose x in FinSeq-Locations ; :: thesis: ((Exec i,s1) | ((Int-Locations \/ FinSeq-Locations ) \ {db})) . x = ((Exec i,s2) | ((Int-Locations \/ FinSeq-Locations ) \ {db})) . x

then reconsider a = x as FinSeq-Location by SCMFSA_2:12;
thus ((Exec i,s1) | ((Int-Locations \/ FinSeq-Locations ) \ {db})) . x = (Exec i,s1) . a by A25, FUNCT_1:72
.= s1 . a by A23, SCMFSA_2:90
.= (DataPart s1) . a by A26, FUNCT_1:72, SCMFSA_2:127
.= s2 . a by A1, A26, FUNCT_1:72, SCMFSA_2:127
.= (Exec i,s2) . a by A23, SCMFSA_2:90
.= ((Exec i,s2) | ((Int-Locations \/ FinSeq-Locations ) \ {db})) . x by A25, FUNCT_1:72 ; :: thesis: verum

end;

end;

end;

A29: dom ((Exec i,s2) | ((Int-Locations \/ FinSeq-Locations ) \ {db})) = (Int-Locations \/ FinSeq-Locations ) \ {db} by A8, RELAT_1:91;
dom ((Exec i,s1) | ((Int-Locations \/ FinSeq-Locations ) \ {db})) = (Int-Locations \/ FinSeq-Locations ) \ {db} by A5, RELAT_1:91;
then A30: (Exec i,s1) | ((Int-Locations \/ FinSeq-Locations ) \ {db}) = (Exec i,s2) | ((Int-Locations \/ FinSeq-Locations ) \ {db}) by A29, A24, FUNCT_1:9;
db in Int-Locations by SCMFSA_2:9;
then db in Int-Locations \/ FinSeq-Locations by XBOOLE_0:def 3;
then A31: Int-Locations \/ FinSeq-Locations = (Int-Locations \/ FinSeq-Locations ) \/ {db} by ZFMISC_1:46
.= ((Int-Locations \/ FinSeq-Locations ) \ {db}) \/ {db} by XBOOLE_1:39 ;
A32: (Exec i,s2) . db = (s2 . db) + (s2 . da) by A23, SCMFSA_2:90;
A33: (Exec i,s1) . db = (s1 . db) + (s1 . da) by A23, SCMFSA_2:90;
db in Int-Locations by SCMFSA_2:9;
then A34: db in Int-Locations \/ FinSeq-Locations by XBOOLE_0:def 3;
then A35: s1 . db = (DataPart s1) . db by FUNCT_1:72, SCMFSA_2:127
.= s2 . db by A1, A34, FUNCT_1:72, SCMFSA_2:127 ;
da in Int-Locations by SCMFSA_2:9;
then A36: da in Int-Locations \/ FinSeq-Locations by XBOOLE_0:def 3;
then s1 . da = (DataPart s1) . da by FUNCT_1:72, SCMFSA_2:127
.= s2 . da by A1, A36, FUNCT_1:72, SCMFSA_2:127 ;
then (Exec i,s1) | {db} = (Exec i,s2) | {db} by A6, A33, A32, A35, GRFUNC_1:90;
hence DataPart (Exec i,s1) = DataPart (Exec i,s2) by A31, A30, RELAT_1:185, SCMFSA_2:127; :: thesis: verum

end;

suppose InsCode i = 3 ; :: thesis: 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:56;
A38: for x being set st x in (Int-Locations \/ FinSeq-Locations ) \ {db} holds
((Exec i,s1) | ((Int-Locations \/ FinSeq-Locations ) \ {db})) . x = ((Exec i,s2) | ((Int-Locations \/ FinSeq-Locations ) \ {db})) . x

proof

let x be set ; :: thesis: ( x in (Int-Locations \/ FinSeq-Locations ) \ {db} implies ((Exec i,s1) | ((Int-Locations \/ FinSeq-Locations ) \ {db})) . x = ((Exec i,s2) | ((Int-Locations \/ FinSeq-Locations ) \ {db})) . x )
assume A39: x in (Int-Locations \/ FinSeq-Locations ) \ {db} ; :: thesis: ((Exec i,s1) | ((Int-Locations \/ FinSeq-Locations ) \ {db})) . x = ((Exec i,s2) | ((Int-Locations \/ FinSeq-Locations ) \ {db})) . x
then A40: x in Int-Locations \/ FinSeq-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, XBOOLE_0:def 3;

suppose x in Int-Locations ; :: thesis: ((Exec i,s1) | ((Int-Locations \/ FinSeq-Locations ) \ {db})) . x = ((Exec i,s2) | ((Int-Locations \/ FinSeq-Locations ) \ {db})) . x

then reconsider a = x as Int-Location by SCMFSA_2:11;
A42: a <> db by A41, TARSKI:def 1;
thus ((Exec i,s1) | ((Int-Locations \/ FinSeq-Locations ) \ {db})) . x = (Exec i,s1) . a by A39, FUNCT_1:72
.= s1 . a by A37, A42, SCMFSA_2:91
.= (DataPart s1) . a by A40, FUNCT_1:72, SCMFSA_2:127
.= s2 . a by A1, A40, FUNCT_1:72, SCMFSA_2:127
.= (Exec i,s2) . a by A37, A42, SCMFSA_2:91
.= ((Exec i,s2) | ((Int-Locations \/ FinSeq-Locations ) \ {db})) . x by A39, FUNCT_1:72 ; :: thesis: verum

end;

suppose x in FinSeq-Locations ; :: thesis: ((Exec i,s1) | ((Int-Locations \/ FinSeq-Locations ) \ {db})) . x = ((Exec i,s2) | ((Int-Locations \/ FinSeq-Locations ) \ {db})) . x

then reconsider a = x as FinSeq-Location by SCMFSA_2:12;
thus ((Exec i,s1) | ((Int-Locations \/ FinSeq-Locations ) \ {db})) . x = (Exec i,s1) . a by A39, FUNCT_1:72
.= s1 . a by A37, SCMFSA_2:91
.= (DataPart s1) . a by A40, FUNCT_1:72, SCMFSA_2:127
.= s2 . a by A1, A40, FUNCT_1:72, SCMFSA_2:127
.= (Exec i,s2) . a by A37, SCMFSA_2:91
.= ((Exec i,s2) | ((Int-Locations \/ FinSeq-Locations ) \ {db})) . x by A39, FUNCT_1:72 ; :: thesis: verum

end;

end;

end;

A43: dom ((Exec i,s2) | ((Int-Locations \/ FinSeq-Locations ) \ {db})) = (Int-Locations \/ FinSeq-Locations ) \ {db} by A8, RELAT_1:91;
dom ((Exec i,s1) | ((Int-Locations \/ FinSeq-Locations ) \ {db})) = (Int-Locations \/ FinSeq-Locations ) \ {db} by A5, RELAT_1:91;
then A44: (Exec i,s1) | ((Int-Locations \/ FinSeq-Locations ) \ {db}) = (Exec i,s2) | ((Int-Locations \/ FinSeq-Locations ) \ {db}) by A43, A38, FUNCT_1:9;
db in Int-Locations by SCMFSA_2:9;
then db in Int-Locations \/ FinSeq-Locations by XBOOLE_0:def 3;
then A45: Int-Locations \/ FinSeq-Locations = (Int-Locations \/ FinSeq-Locations ) \/ {db} by ZFMISC_1:46
.= ((Int-Locations \/ FinSeq-Locations ) \ {db}) \/ {db} by XBOOLE_1:39 ;
A46: (Exec i,s2) . db = (s2 . db) - (s2 . da) by A37, SCMFSA_2:91;
A47: (Exec i,s1) . db = (s1 . db) - (s1 . da) by A37, SCMFSA_2:91;
db in Int-Locations by SCMFSA_2:9;
then A48: db in Int-Locations \/ FinSeq-Locations by XBOOLE_0:def 3;
then A49: s1 . db = (DataPart s1) . db by FUNCT_1:72, SCMFSA_2:127
.= s2 . db by A1, A48, FUNCT_1:72, SCMFSA_2:127 ;
da in Int-Locations by SCMFSA_2:9;
then A50: da in Int-Locations \/ FinSeq-Locations by XBOOLE_0:def 3;
then s1 . da = (DataPart s1) . da by FUNCT_1:72, SCMFSA_2:127
.= s2 . da by A1, A50, FUNCT_1:72, SCMFSA_2:127 ;
then (Exec i,s1) | {db} = (Exec i,s2) | {db} by A6, A47, A46, A49, GRFUNC_1:90;
hence DataPart (Exec i,s1) = DataPart (Exec i,s2) by A45, A44, RELAT_1:185, SCMFSA_2:127; :: thesis: verum

end;

suppose InsCode i = 4 ; :: thesis: 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:57;
A52: for x being set st x in (Int-Locations \/ FinSeq-Locations ) \ {db} holds
((Exec i,s1) | ((Int-Locations \/ FinSeq-Locations ) \ {db})) . x = ((Exec i,s2) | ((Int-Locations \/ FinSeq-Locations ) \ {db})) . x

proof

let x be set ; :: thesis: ( x in (Int-Locations \/ FinSeq-Locations ) \ {db} implies ((Exec i,s1) | ((Int-Locations \/ FinSeq-Locations ) \ {db})) . x = ((Exec i,s2) | ((Int-Locations \/ FinSeq-Locations ) \ {db})) . x )
assume A53: x in (Int-Locations \/ FinSeq-Locations ) \ {db} ; :: thesis: ((Exec i,s1) | ((Int-Locations \/ FinSeq-Locations ) \ {db})) . x = ((Exec i,s2) | ((Int-Locations \/ FinSeq-Locations ) \ {db})) . x
then A54: x in Int-Locations \/ FinSeq-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, XBOOLE_0:def 3;

suppose x in Int-Locations ; :: thesis: ((Exec i,s1) | ((Int-Locations \/ FinSeq-Locations ) \ {db})) . x = ((Exec i,s2) | ((Int-Locations \/ FinSeq-Locations ) \ {db})) . x

then reconsider a = x as Int-Location by SCMFSA_2:11;
A56: a <> db by A55, TARSKI:def 1;
thus ((Exec i,s1) | ((Int-Locations \/ FinSeq-Locations ) \ {db})) . x = (Exec i,s1) . a by A53, FUNCT_1:72
.= s1 . a by A51, A56, SCMFSA_2:92
.= (DataPart s1) . a by A54, FUNCT_1:72, SCMFSA_2:127
.= s2 . a by A1, A54, FUNCT_1:72, SCMFSA_2:127
.= (Exec i,s2) . a by A51, A56, SCMFSA_2:92
.= ((Exec i,s2) | ((Int-Locations \/ FinSeq-Locations ) \ {db})) . x by A53, FUNCT_1:72 ; :: thesis: verum

end;

suppose x in FinSeq-Locations ; :: thesis: ((Exec i,s1) | ((Int-Locations \/ FinSeq-Locations ) \ {db})) . x = ((Exec i,s2) | ((Int-Locations \/ FinSeq-Locations ) \ {db})) . x

then reconsider a = x as FinSeq-Location by SCMFSA_2:12;
thus ((Exec i,s1) | ((Int-Locations \/ FinSeq-Locations ) \ {db})) . x = (Exec i,s1) . a by A53, FUNCT_1:72
.= s1 . a by A51, SCMFSA_2:92
.= (DataPart s1) . a by A54, FUNCT_1:72, SCMFSA_2:127
.= s2 . a by A1, A54, FUNCT_1:72, SCMFSA_2:127
.= (Exec i,s2) . a by A51, SCMFSA_2:92
.= ((Exec i,s2) | ((Int-Locations \/ FinSeq-Locations ) \ {db})) . x by A53, FUNCT_1:72 ; :: thesis: verum

end;

end;

end;

A57: dom ((Exec i,s2) | ((Int-Locations \/ FinSeq-Locations ) \ {db})) = (Int-Locations \/ FinSeq-Locations ) \ {db} by A8, RELAT_1:91;
dom ((Exec i,s1) | ((Int-Locations \/ FinSeq-Locations ) \ {db})) = (Int-Locations \/ FinSeq-Locations ) \ {db} by A5, RELAT_1:91;
then A58: (Exec i,s1) | ((Int-Locations \/ FinSeq-Locations ) \ {db}) = (Exec i,s2) | ((Int-Locations \/ FinSeq-Locations ) \ {db}) by A57, A52, FUNCT_1:9;
db in Int-Locations by SCMFSA_2:9;
then db in Int-Locations \/ FinSeq-Locations by XBOOLE_0:def 3;
then A59: Int-Locations \/ FinSeq-Locations = (Int-Locations \/ FinSeq-Locations ) \/ {db} by ZFMISC_1:46
.= ((Int-Locations \/ FinSeq-Locations ) \ {db}) \/ {db} by XBOOLE_1:39 ;
A60: (Exec i,s2) . db = (s2 . db) * (s2 . da) by A51, SCMFSA_2:92;
A61: (Exec i,s1) . db = (s1 . db) * (s1 . da) by A51, SCMFSA_2:92;
db in Int-Locations by SCMFSA_2:9;
then A62: db in Int-Locations \/ FinSeq-Locations by XBOOLE_0:def 3;
then A63: s1 . db = (DataPart s1) . db by FUNCT_1:72, SCMFSA_2:127
.= s2 . db by A1, A62, FUNCT_1:72, SCMFSA_2:127 ;
da in Int-Locations by SCMFSA_2:9;
then A64: da in Int-Locations \/ FinSeq-Locations by XBOOLE_0:def 3;
then s1 . da = (DataPart s1) . da by FUNCT_1:72, SCMFSA_2:127
.= s2 . da by A1, A64, FUNCT_1:72, SCMFSA_2:127 ;
then (Exec i,s1) | {db} = (Exec i,s2) | {db} by A6, A61, A60, A63, GRFUNC_1:90;
hence DataPart (Exec i,s1) = DataPart (Exec i,s2) by A59, A58, RELAT_1:185, SCMFSA_2:127; :: thesis: verum

end;

suppose InsCode i = 5 ; :: thesis: 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:58;

hereby :: thesis: verum

per cases ( da <> db or da = db ) ;

suppose A66: da <> db ; :: thesis: DataPart (Exec i,s1) = DataPart (Exec i,s2)

A67: for x being set st x in (Int-Locations \/ FinSeq-Locations ) \ {db,da} holds
((Exec i,s1) | ((Int-Locations \/ FinSeq-Locations ) \ {db,da})) . x = ((Exec i,s2) | ((Int-Locations \/ FinSeq-Locations ) \ {db,da})) . x

proof

let x be set ; :: thesis: ( x in (Int-Locations \/ FinSeq-Locations ) \ {db,da} implies ((Exec i,s1) | ((Int-Locations \/ FinSeq-Locations ) \ {db,da})) . x = ((Exec i,s2) | ((Int-Locations \/ FinSeq-Locations ) \ {db,da})) . x )
assume A68: x in (Int-Locations \/ FinSeq-Locations ) \ {db,da} ; :: thesis: ((Exec i,s1) | ((Int-Locations \/ FinSeq-Locations ) \ {db,da})) . x = ((Exec i,s2) | ((Int-Locations \/ FinSeq-Locations ) \ {db,da})) . x
then A69: x in Int-Locations \/ FinSeq-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, XBOOLE_0:def 3;

suppose x in Int-Locations ; :: thesis: ((Exec i,s1) | ((Int-Locations \/ FinSeq-Locations ) \ {db,da})) . x = ((Exec i,s2) | ((Int-Locations \/ FinSeq-Locations ) \ {db,da})) . x

then reconsider a = x as Int-Location by SCMFSA_2:11;
A71: a <> da by A70, TARSKI:def 2;
A72: a <> db by A70, TARSKI:def 2;
thus ((Exec i,s1) | ((Int-Locations \/ FinSeq-Locations ) \ {db,da})) . x = (Exec i,s1) . a by A68, FUNCT_1:72
.= s1 . a by A65, A71, A72, SCMFSA_2:93
.= (DataPart s1) . a by A69, FUNCT_1:72, SCMFSA_2:127
.= s2 . a by A1, A69, FUNCT_1:72, SCMFSA_2:127
.= (Exec i,s2) . a by A65, A71, A72, SCMFSA_2:93
.= ((Exec i,s2) | ((Int-Locations \/ FinSeq-Locations ) \ {db,da})) . x by A68, FUNCT_1:72 ; :: thesis: verum

end;

suppose x in FinSeq-Locations ; :: thesis: ((Exec i,s1) | ((Int-Locations \/ FinSeq-Locations ) \ {db,da})) . x = ((Exec i,s2) | ((Int-Locations \/ FinSeq-Locations ) \ {db,da})) . x

then reconsider a = x as FinSeq-Location by SCMFSA_2:12;
thus ((Exec i,s1) | ((Int-Locations \/ FinSeq-Locations ) \ {db,da})) . x = (Exec i,s1) . a by A68, FUNCT_1:72
.= s1 . a by A65, SCMFSA_2:93
.= (DataPart s1) . a by A69, FUNCT_1:72, SCMFSA_2:127
.= s2 . a by A1, A69, FUNCT_1:72, SCMFSA_2:127
.= (Exec i,s2) . a by A65, SCMFSA_2:93
.= ((Exec i,s2) | ((Int-Locations \/ FinSeq-Locations ) \ {db,da})) . x by A68, FUNCT_1:72 ; :: thesis: verum

end;

end;

end;

A73: dom ((Exec i,s2) | ((Int-Locations \/ FinSeq-Locations ) \ {db,da})) = (Int-Locations \/ FinSeq-Locations ) \ {db,da} by A8, RELAT_1:91;
dom ((Exec i,s1) | ((Int-Locations \/ FinSeq-Locations ) \ {db,da})) = (Int-Locations \/ FinSeq-Locations ) \ {db,da} by A5, RELAT_1:91;
then A74: (Exec i,s1) | ((Int-Locations \/ FinSeq-Locations ) \ {db,da}) = (Exec i,s2) | ((Int-Locations \/ FinSeq-Locations ) \ {db,da}) by A73, A67, FUNCT_1:9;
A75: (Exec i,s2) . da = (s2 . db) mod (s2 . da) by A65, SCMFSA_2:93;
db in Int-Locations by SCMFSA_2:9;
then A76: db in Int-Locations \/ FinSeq-Locations by XBOOLE_0:def 3;
then A77: s1 . db = (DataPart s1) . db by FUNCT_1:72, SCMFSA_2:127
.= s2 . db by A1, A76, FUNCT_1:72, SCMFSA_2:127 ;
da in Int-Locations by SCMFSA_2:9;
then A78: da in Int-Locations \/ FinSeq-Locations by XBOOLE_0:def 3;
db in Int-Locations by SCMFSA_2:9;
then db in Int-Locations \/ FinSeq-Locations by XBOOLE_0:def 3;
then A79: Int-Locations \/ FinSeq-Locations = (Int-Locations \/ FinSeq-Locations ) \/ {db,da} by A78, ZFMISC_1:48
.= ((Int-Locations \/ FinSeq-Locations ) \ {db,da}) \/ {db,da} by XBOOLE_1:39 ;
A80: (Exec i,s1) . da = (s1 . db) mod (s1 . da) by A65, SCMFSA_2:93;
A81: (Exec i,s2) . db = (s2 . db) div (s2 . da) by A65, A66, SCMFSA_2:93;
A82: (Exec i,s1) . db = (s1 . db) div (s1 . da) by A65, A66, SCMFSA_2:93;
da in Int-Locations by SCMFSA_2:9;
then A83: da in Int-Locations \/ FinSeq-Locations by XBOOLE_0:def 3;
then s1 . da = (DataPart s1) . da by FUNCT_1:72, SCMFSA_2:127
.= s2 . da by A1, A83, FUNCT_1:72, SCMFSA_2:127 ;
then (Exec i,s1) | {db,da} = (Exec i,s2) | {db,da} by A6, A82, A80, A81, A75, A77, GRFUNC_1:91;
hence DataPart (Exec i,s1) = DataPart (Exec i,s2) by A79, A74, RELAT_1:185, SCMFSA_2:127; :: thesis: verum

end;

suppose A84: da = db ; :: thesis: DataPart (Exec i,s1) = DataPart (Exec i,s2)

A85: for x being set st x in (Int-Locations \/ FinSeq-Locations ) \ {db} holds
((Exec i,s1) | ((Int-Locations \/ FinSeq-Locations ) \ {db})) . x = ((Exec i,s2) | ((Int-Locations \/ FinSeq-Locations ) \ {db})) . x

proof

let x be set ; :: thesis: ( x in (Int-Locations \/ FinSeq-Locations ) \ {db} implies ((Exec i,s1) | ((Int-Locations \/ FinSeq-Locations ) \ {db})) . x = ((Exec i,s2) | ((Int-Locations \/ FinSeq-Locations ) \ {db})) . x )
assume A86: x in (Int-Locations \/ FinSeq-Locations ) \ {db} ; :: thesis: ((Exec i,s1) | ((Int-Locations \/ FinSeq-Locations ) \ {db})) . x = ((Exec i,s2) | ((Int-Locations \/ FinSeq-Locations ) \ {db})) . x
then A87: x in Int-Locations \/ FinSeq-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, XBOOLE_0:def 3;

suppose x in Int-Locations ; :: thesis: ((Exec i,s1) | ((Int-Locations \/ FinSeq-Locations ) \ {db})) . x = ((Exec i,s2) | ((Int-Locations \/ FinSeq-Locations ) \ {db})) . x

then reconsider a = x as Int-Location by SCMFSA_2:11;
A89: a <> db by A88, TARSKI:def 1;
thus ((Exec i,s1) | ((Int-Locations \/ FinSeq-Locations ) \ {db})) . x = (Exec i,s1) . a by A86, FUNCT_1:72
.= s1 . a by A65, A84, A89, SCMFSA_2:94
.= (DataPart s1) . a by A87, FUNCT_1:72, SCMFSA_2:127
.= s2 . a by A1, A87, FUNCT_1:72, SCMFSA_2:127
.= (Exec i,s2) . a by A65, A84, A89, SCMFSA_2:94
.= ((Exec i,s2) | ((Int-Locations \/ FinSeq-Locations ) \ {db})) . x by A86, FUNCT_1:72 ; :: thesis: verum

end;

suppose x in FinSeq-Locations ; :: thesis: ((Exec i,s1) | ((Int-Locations \/ FinSeq-Locations ) \ {db})) . x = ((Exec i,s2) | ((Int-Locations \/ FinSeq-Locations ) \ {db})) . x

then reconsider a = x as FinSeq-Location by SCMFSA_2:12;
thus ((Exec i,s1) | ((Int-Locations \/ FinSeq-Locations ) \ {db})) . x = (Exec i,s1) . a by A86, FUNCT_1:72
.= s1 . a by A65, A84, SCMFSA_2:94
.= (s1 | (Int-Locations \/ FinSeq-Locations )) . a by A87, FUNCT_1:72
.= s2 . a by A1, A87, FUNCT_1:72, SCMFSA_2:127
.= (Exec i,s2) . a by A65, A84, SCMFSA_2:94
.= ((Exec i,s2) | ((Int-Locations \/ FinSeq-Locations ) \ {db})) . x by A86, FUNCT_1:72 ; :: thesis: verum

end;

end;

end;

A90: dom ((Exec i,s2) | ((Int-Locations \/ FinSeq-Locations ) \ {db})) = (Int-Locations \/ FinSeq-Locations ) \ {db} by A8, RELAT_1:91;
dom ((Exec i,s1) | ((Int-Locations \/ FinSeq-Locations ) \ {db})) = (Int-Locations \/ FinSeq-Locations ) \ {db} by A5, RELAT_1:91;
then A91: (Exec i,s1) | ((Int-Locations \/ FinSeq-Locations ) \ {db}) = (Exec i,s2) | ((Int-Locations \/ FinSeq-Locations ) \ {db}) by A90, A85, FUNCT_1:9;
db in Int-Locations by SCMFSA_2:9;
then db in Int-Locations \/ FinSeq-Locations by XBOOLE_0:def 3;
then A92: Int-Locations \/ FinSeq-Locations = (Int-Locations \/ FinSeq-Locations ) \/ {db} by ZFMISC_1:46
.= ((Int-Locations \/ FinSeq-Locations ) \ {db}) \/ {db} by XBOOLE_1:39 ;
A93: (Exec i,s2) . db = (s2 . db) mod (s2 . da) by A65, A84, SCMFSA_2:94;
A94: (Exec i,s1) . db = (s1 . db) mod (s1 . da) by A65, A84, SCMFSA_2:94;
db in Int-Locations by SCMFSA_2:9;
then A95: db in Int-Locations \/ FinSeq-Locations by XBOOLE_0:def 3;
then A96: s1 . db = (DataPart s1) . db by FUNCT_1:72, SCMFSA_2:127
.= s2 . db by A1, A95, FUNCT_1:72, SCMFSA_2:127 ;
da in Int-Locations by SCMFSA_2:9;
then A97: da in Int-Locations \/ FinSeq-Locations by XBOOLE_0:def 3;
then s1 . da = (DataPart s1) . da by FUNCT_1:72, SCMFSA_2:127
.= s2 . da by A1, A97, FUNCT_1:72, SCMFSA_2:127 ;
then (Exec i,s1) | {db} = (Exec i,s2) | {db} by A6, A94, A93, A96, GRFUNC_1:90;
hence DataPart (Exec i,s1) = DataPart (Exec i,s2) by A92, A91, RELAT_1:185, SCMFSA_2:127; :: thesis: verum

end;

end;

end;

end;

suppose InsCode i = 6 ; :: thesis: DataPart (Exec i,s1) = DataPart (Exec i,s2)

then A98: ex l1 being Element of NAT st i = goto l1 by SCMFSA_2:59;
for x being set st x in Int-Locations \/ FinSeq-Locations holds
(DataPart (Exec i,s1)) . x = (DataPart (Exec i,s2)) . x

proof

let x be set ; :: thesis: ( x in Int-Locations \/ FinSeq-Locations implies (DataPart (Exec i,s1)) . x = (DataPart (Exec i,s2)) . x )
assume A99: x in Int-Locations \/ FinSeq-Locations ; :: thesis: (DataPart (Exec i,s1)) . x = (DataPart (Exec i,s2)) . x

per cases ( x in Int-Locations or x in FinSeq-Locations ) by A99, XBOOLE_0:def 3;

suppose x in Int-Locations ; :: thesis: (DataPart (Exec i,s1)) . x = (DataPart (Exec i,s2)) . x

then reconsider a = x as Int-Location by SCMFSA_2:11;
thus (DataPart (Exec i,s1)) . x = (Exec i,s1) . a by A99, FUNCT_1:72, SCMFSA_2:127
.= s1 . a by A98, SCMFSA_2:95
.= (DataPart s1) . a by A99, FUNCT_1:72, SCMFSA_2:127
.= s2 . a by A1, A99, FUNCT_1:72, SCMFSA_2:127
.= (Exec i,s2) . a by A98, SCMFSA_2:95
.= (DataPart (Exec i,s2)) . x by A99, FUNCT_1:72, SCMFSA_2:127 ; :: thesis: verum

end;

suppose x in FinSeq-Locations ; :: thesis: (DataPart (Exec i,s1)) . x = (DataPart (Exec i,s2)) . x

then reconsider a = x as FinSeq-Location by SCMFSA_2:12;
thus (DataPart (Exec i,s1)) . x = (Exec i,s1) . a by A99, FUNCT_1:72, SCMFSA_2:127
.= s1 . a by A98, SCMFSA_2:95
.= (DataPart s1) . a by A99, FUNCT_1:72, SCMFSA_2:127
.= s2 . a by A1, A99, FUNCT_1:72, SCMFSA_2:127
.= (Exec i,s2) . a by A98, SCMFSA_2:95
.= (DataPart (Exec i,s2)) . x by A99, FUNCT_1:72, SCMFSA_2:127 ; :: thesis: verum

end;

end;

end;

hence DataPart (Exec i,s1) = DataPart (Exec i,s2) by A7, A9, FUNCT_1:9, SCMFSA_2:127; :: thesis: verum

end;

suppose InsCode i = 7 ; :: thesis: 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:60;
for x being set st x in Int-Locations \/ FinSeq-Locations holds
(DataPart (Exec i,s1)) . x = (DataPart (Exec i,s2)) . x

proof

let x be set ; :: thesis: ( x in Int-Locations \/ FinSeq-Locations implies (DataPart (Exec i,s1)) . x = (DataPart (Exec i,s2)) . x )
assume A101: x in Int-Locations \/ FinSeq-Locations ; :: thesis: (DataPart (Exec i,s1)) . x = (DataPart (Exec i,s2)) . x

per cases ( x in Int-Locations or x in FinSeq-Locations ) by A101, XBOOLE_0:def 3;

suppose x in Int-Locations ; :: thesis: (DataPart (Exec i,s1)) . x = (DataPart (Exec i,s2)) . x

then reconsider a = x as Int-Location by SCMFSA_2:11;
thus (DataPart (Exec i,s1)) . x = (Exec i,s1) . a by A101, FUNCT_1:72, SCMFSA_2:127
.= s1 . a by A100, SCMFSA_2:96
.= (DataPart s1) . a by A101, FUNCT_1:72, SCMFSA_2:127
.= s2 . a by A1, A101, FUNCT_1:72, SCMFSA_2:127
.= (Exec i,s2) . a by A100, SCMFSA_2:96
.= (DataPart (Exec i,s2)) . x by A101, FUNCT_1:72, SCMFSA_2:127 ; :: thesis: verum

end;

suppose x in FinSeq-Locations ; :: thesis: (DataPart (Exec i,s1)) . x = (DataPart (Exec i,s2)) . x

then reconsider a = x as FinSeq-Location by SCMFSA_2:12;
thus (DataPart (Exec i,s1)) . x = (Exec i,s1) . a by A101, FUNCT_1:72, SCMFSA_2:127
.= s1 . a by A100, SCMFSA_2:96
.= (DataPart s1) . a by A101, FUNCT_1:72, SCMFSA_2:127
.= s2 . a by A1, A101, FUNCT_1:72, SCMFSA_2:127
.= (Exec i,s2) . a by A100, SCMFSA_2:96
.= (DataPart (Exec i,s2)) . x by A101, FUNCT_1:72, SCMFSA_2:127 ; :: thesis: verum

end;

end;

end;

hence DataPart (Exec i,s1) = DataPart (Exec i,s2) by A7, A9, FUNCT_1:9, SCMFSA_2:127; :: thesis: verum

end;

suppose InsCode i = 8 ; :: thesis: 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:61;
for x being set st x in Int-Locations \/ FinSeq-Locations holds
(DataPart (Exec i,s1)) . x = (DataPart (Exec i,s2)) . x

proof

let x be set ; :: thesis: ( x in Int-Locations \/ FinSeq-Locations implies (DataPart (Exec i,s1)) . x = (DataPart (Exec i,s2)) . x )
assume A103: x in Int-Locations \/ FinSeq-Locations ; :: thesis: (DataPart (Exec i,s1)) . x = (DataPart (Exec i,s2)) . x

per cases ( x in Int-Locations or x in FinSeq-Locations ) by A103, XBOOLE_0:def 3;

suppose x in Int-Locations ; :: thesis: (DataPart (Exec i,s1)) . x = (DataPart (Exec i,s2)) . x

then reconsider a = x as Int-Location by SCMFSA_2:11;
thus (DataPart (Exec i,s1)) . x = (Exec i,s1) . a by A103, FUNCT_1:72, SCMFSA_2:127
.= s1 . a by A102, SCMFSA_2:97
.= (DataPart s1) . a by A103, FUNCT_1:72, SCMFSA_2:127
.= s2 . a by A1, A103, FUNCT_1:72, SCMFSA_2:127
.= (Exec i,s2) . a by A102, SCMFSA_2:97
.= (DataPart (Exec i,s2)) . x by A103, FUNCT_1:72, SCMFSA_2:127 ; :: thesis: verum

end;

suppose x in FinSeq-Locations ; :: thesis: (DataPart (Exec i,s1)) . x = (DataPart (Exec i,s2)) . x

then reconsider a = x as FinSeq-Location by SCMFSA_2:12;
thus (DataPart (Exec i,s1)) . x = (Exec i,s1) . a by A103, FUNCT_1:72, SCMFSA_2:127
.= s1 . a by A102, SCMFSA_2:97
.= (DataPart s1) . a by A103, FUNCT_1:72, SCMFSA_2:127
.= s2 . a by A1, A103, FUNCT_1:72, SCMFSA_2:127
.= (Exec i,s2) . a by A102, SCMFSA_2:97
.= (DataPart (Exec i,s2)) . x by A103, FUNCT_1:72, SCMFSA_2:127 ; :: thesis: verum

end;

end;

end;

hence DataPart (Exec i,s1) = DataPart (Exec i,s2) by A7, A9, FUNCT_1:9, SCMFSA_2:127; :: thesis: verum

end;

suppose InsCode i = 9 ; :: thesis: 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:62;
A105: for x being set st x in (Int-Locations \/ FinSeq-Locations ) \ {db} holds
((Exec i,s1) | ((Int-Locations \/ FinSeq-Locations ) \ {db})) . x = ((Exec i,s2) | ((Int-Locations \/ FinSeq-Locations ) \ {db})) . x

proof

let x be set ; :: thesis: ( x in (Int-Locations \/ FinSeq-Locations ) \ {db} implies ((Exec i,s1) | ((Int-Locations \/ FinSeq-Locations ) \ {db})) . x = ((Exec i,s2) | ((Int-Locations \/ FinSeq-Locations ) \ {db})) . x )
assume A106: x in (Int-Locations \/ FinSeq-Locations ) \ {db} ; :: thesis: ((Exec i,s1) | ((Int-Locations \/ FinSeq-Locations ) \ {db})) . x = ((Exec i,s2) | ((Int-Locations \/ FinSeq-Locations ) \ {db})) . x
then A107: x in Int-Locations \/ FinSeq-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, XBOOLE_0:def 3;

suppose x in Int-Locations ; :: thesis: ((Exec i,s1) | ((Int-Locations \/ FinSeq-Locations ) \ {db})) . x = ((Exec i,s2) | ((Int-Locations \/ FinSeq-Locations ) \ {db})) . x

then reconsider a = x as Int-Location by SCMFSA_2:11;
A109: a <> db by A108, TARSKI:def 1;
thus ((Exec i,s1) | ((Int-Locations \/ FinSeq-Locations ) \ {db})) . x = (Exec i,s1) . a by A106, FUNCT_1:72
.= s1 . a by A104, A109, SCMFSA_2:98
.= (DataPart s1) . a by A107, FUNCT_1:72, SCMFSA_2:127
.= s2 . a by A1, A107, FUNCT_1:72, SCMFSA_2:127
.= (Exec i,s2) . a by A104, A109, SCMFSA_2:98
.= ((Exec i,s2) | ((Int-Locations \/ FinSeq-Locations ) \ {db})) . x by A106, FUNCT_1:72 ; :: thesis: verum

end;

suppose x in FinSeq-Locations ; :: thesis: ((Exec i,s1) | ((Int-Locations \/ FinSeq-Locations ) \ {db})) . x = ((Exec i,s2) | ((Int-Locations \/ FinSeq-Locations ) \ {db})) . x

then reconsider a = x as FinSeq-Location by SCMFSA_2:12;
thus ((Exec i,s1) | ((Int-Locations \/ FinSeq-Locations ) \ {db})) . x = (Exec i,s1) . a by A106, FUNCT_1:72
.= s1 . a by A104, SCMFSA_2:98
.= (DataPart s1) . a by A107, FUNCT_1:72, SCMFSA_2:127
.= s2 . a by A1, A107, FUNCT_1:72, SCMFSA_2:127
.= (Exec i,s2) . a by A104, SCMFSA_2:98
.= ((Exec i,s2) | ((Int-Locations \/ FinSeq-Locations ) \ {db})) . x by A106, FUNCT_1:72 ; :: thesis: verum

end;

end;

end;

A110: dom ((Exec i,s2) | ((Int-Locations \/ FinSeq-Locations ) \ {db})) = (Int-Locations \/ FinSeq-Locations ) \ {db} by A8, RELAT_1:91;
dom ((Exec i,s1) | ((Int-Locations \/ FinSeq-Locations ) \ {db})) = (Int-Locations \/ FinSeq-Locations ) \ {db} by A5, RELAT_1:91;
then A111: (Exec i,s1) | ((Int-Locations \/ FinSeq-Locations ) \ {db}) = (Exec i,s2) | ((Int-Locations \/ FinSeq-Locations ) \ {db}) by A110, A105, FUNCT_1:9;
db in Int-Locations by SCMFSA_2:9;
then db in Int-Locations \/ FinSeq-Locations by XBOOLE_0:def 3;
then A112: Int-Locations \/ FinSeq-Locations = (Int-Locations \/ FinSeq-Locations ) \/ {db} by ZFMISC_1:46
.= ((Int-Locations \/ FinSeq-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:98;
A114: ex k1 being Element of NAT st
( k1 = abs (s1 . da) & (Exec i,s1) . db = (s1 . fa) /. k1 ) by A104, SCMFSA_2:98;
fa in FinSeq-Locations by SCMFSA_2:10;
then A115: fa in Int-Locations \/ FinSeq-Locations by XBOOLE_0:def 3;
then A116: s1 . fa = (DataPart s1) . fa by FUNCT_1:72, SCMFSA_2:127
.= s2 . fa by A1, A115, FUNCT_1:72, SCMFSA_2:127 ;
da in Int-Locations by SCMFSA_2:9;
then A117: da in Int-Locations \/ FinSeq-Locations by XBOOLE_0:def 3;
then s1 . da = (DataPart s1) . da by FUNCT_1:72, SCMFSA_2:127
.= s2 . da by A1, A117, FUNCT_1:72, SCMFSA_2:127 ;
then (Exec i,s1) | {db} = (Exec i,s2) | {db} by A6, A114, A113, A116, GRFUNC_1:90;
hence DataPart (Exec i,s1) = DataPart (Exec i,s2) by A112, A111, RELAT_1:185, SCMFSA_2:127; :: thesis: verum

end;

suppose InsCode i = 10 ; :: thesis: 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:63;
A119: for x being set st x in (Int-Locations \/ FinSeq-Locations ) \ {fa} holds
((Exec i,s1) | ((Int-Locations \/ FinSeq-Locations ) \ {fa})) . x = ((Exec i,s2) | ((Int-Locations \/ FinSeq-Locations ) \ {fa})) . x

proof

let x be set ; :: thesis: ( x in (Int-Locations \/ FinSeq-Locations ) \ {fa} implies ((Exec i,s1) | ((Int-Locations \/ FinSeq-Locations ) \ {fa})) . x = ((Exec i,s2) | ((Int-Locations \/ FinSeq-Locations ) \ {fa})) . x )
assume A120: x in (Int-Locations \/ FinSeq-Locations ) \ {fa} ; :: thesis: ((Exec i,s1) | ((Int-Locations \/ FinSeq-Locations ) \ {fa})) . x = ((Exec i,s2) | ((Int-Locations \/ FinSeq-Locations ) \ {fa})) . x
then A121: x in Int-Locations \/ FinSeq-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, XBOOLE_0:def 3;

suppose x in Int-Locations ; :: thesis: ((Exec i,s1) | ((Int-Locations \/ FinSeq-Locations ) \ {fa})) . x = ((Exec i,s2) | ((Int-Locations \/ FinSeq-Locations ) \ {fa})) . x

then reconsider a = x as Int-Location by SCMFSA_2:11;
thus ((Exec i,s1) | ((Int-Locations \/ FinSeq-Locations ) \ {fa})) . x = (Exec i,s1) . a by A120, FUNCT_1:72
.= s1 . a by A118, SCMFSA_2:99
.= (DataPart s1) . a by A121, FUNCT_1:72, SCMFSA_2:127
.= s2 . a by A1, A121, FUNCT_1:72, SCMFSA_2:127
.= (Exec i,s2) . a by A118, SCMFSA_2:99
.= ((Exec i,s2) | ((Int-Locations \/ FinSeq-Locations ) \ {fa})) . x by A120, FUNCT_1:72 ; :: thesis: verum

end;

suppose x in FinSeq-Locations ; :: thesis: ((Exec i,s1) | ((Int-Locations \/ FinSeq-Locations ) \ {fa})) . x = ((Exec i,s2) | ((Int-Locations \/ FinSeq-Locations ) \ {fa})) . x

then reconsider a = x as FinSeq-Location by SCMFSA_2:12;
A123: a <> fa by A122, TARSKI:def 1;
thus ((Exec i,s1) | ((Int-Locations \/ FinSeq-Locations ) \ {fa})) . x = (Exec i,s1) . a by A120, FUNCT_1:72
.= s1 . a by A118, A123, SCMFSA_2:99
.= (DataPart s1) . a by A121, FUNCT_1:72, SCMFSA_2:127
.= s2 . a by A1, A121, FUNCT_1:72, SCMFSA_2:127
.= (Exec i,s2) . a by A118, A123, SCMFSA_2:99
.= ((Exec i,s2) | ((Int-Locations \/ FinSeq-Locations ) \ {fa})) . x by A120, FUNCT_1:72 ; :: thesis: verum

end;

end;

end;

A124: dom ((Exec i,s2) | ((Int-Locations \/ FinSeq-Locations ) \ {fa})) = (Int-Locations \/ FinSeq-Locations ) \ {fa} by A8, RELAT_1:91;
dom ((Exec i,s1) | ((Int-Locations \/ FinSeq-Locations ) \ {fa})) = (Int-Locations \/ FinSeq-Locations ) \ {fa} by A5, RELAT_1:91;
then A125: (Exec i,s1) | ((Int-Locations \/ FinSeq-Locations ) \ {fa}) = (Exec i,s2) | ((Int-Locations \/ FinSeq-Locations ) \ {fa}) by A124, A119, FUNCT_1:9;
fa in FinSeq-Locations by SCMFSA_2:10;
then fa in Int-Locations \/ FinSeq-Locations by XBOOLE_0:def 3;
then A126: Int-Locations \/ FinSeq-Locations = (Int-Locations \/ FinSeq-Locations ) \/ {fa} by ZFMISC_1:46
.= ((Int-Locations \/ FinSeq-Locations ) \ {fa}) \/ {fa} by XBOOLE_1:39 ;
fa in FinSeq-Locations by SCMFSA_2:10;
then A127: fa in Int-Locations \/ FinSeq-Locations by XBOOLE_0:def 3;
then A128: s1 . fa = (DataPart s1) . fa by FUNCT_1:72, SCMFSA_2:127
.= s2 . fa by A1, A127, FUNCT_1:72, SCMFSA_2:127 ;
db in Int-Locations by SCMFSA_2:9;
then A129: db in Int-Locations \/ FinSeq-Locations by XBOOLE_0:def 3;
then A130: s1 . db = (DataPart s1) . db by FUNCT_1:72, SCMFSA_2:127
.= s2 . db by A1, A129, FUNCT_1:72, SCMFSA_2:127 ;
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:99;
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:99;
da in Int-Locations by SCMFSA_2:9;
then A133: da in Int-Locations \/ FinSeq-Locations by XBOOLE_0:def 3;
then s1 . da = (DataPart s1) . da by FUNCT_1:72, SCMFSA_2:127
.= s2 . da by A1, A133, FUNCT_1:72, SCMFSA_2:127 ;
then (Exec i,s1) | {fa} = (Exec i,s2) | {fa} by A6, A132, A131, A130, A128, GRFUNC_1:90;
hence DataPart (Exec i,s1) = DataPart (Exec i,s2) by A126, A125, RELAT_1:185, SCMFSA_2:127; :: thesis: verum

end;

suppose InsCode i = 11 ; :: thesis: 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:64;
A135: for x being set st x in (Int-Locations \/ FinSeq-Locations ) \ {da} holds
((Exec i,s1) | ((Int-Locations \/ FinSeq-Locations ) \ {da})) . x = ((Exec i,s2) | ((Int-Locations \/ FinSeq-Locations ) \ {da})) . x

proof

let x be set ; :: thesis: ( x in (Int-Locations \/ FinSeq-Locations ) \ {da} implies ((Exec i,s1) | ((Int-Locations \/ FinSeq-Locations ) \ {da})) . x = ((Exec i,s2) | ((Int-Locations \/ FinSeq-Locations ) \ {da})) . x )
assume A136: x in (Int-Locations \/ FinSeq-Locations ) \ {da} ; :: thesis: ((Exec i,s1) | ((Int-Locations \/ FinSeq-Locations ) \ {da})) . x = ((Exec i,s2) | ((Int-Locations \/ FinSeq-Locations ) \ {da})) . x
then A137: x in Int-Locations \/ FinSeq-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, XBOOLE_0:def 3;

suppose x in Int-Locations ; :: thesis: ((Exec i,s1) | ((Int-Locations \/ FinSeq-Locations ) \ {da})) . x = ((Exec i,s2) | ((Int-Locations \/ FinSeq-Locations ) \ {da})) . x

then reconsider a = x as Int-Location by SCMFSA_2:11;
A139: a <> da by A138, TARSKI:def 1;
thus ((Exec i,s1) | ((Int-Locations \/ FinSeq-Locations ) \ {da})) . x = (Exec i,s1) . a by A136, FUNCT_1:72
.= s1 . a by A134, A139, SCMFSA_2:100
.= (DataPart s1) . a by A137, FUNCT_1:72, SCMFSA_2:127
.= s2 . a by A1, A137, FUNCT_1:72, SCMFSA_2:127
.= (Exec i,s2) . a by A134, A139, SCMFSA_2:100
.= ((Exec i,s2) | ((Int-Locations \/ FinSeq-Locations ) \ {da})) . x by A136, FUNCT_1:72 ; :: thesis: verum

end;

suppose x in FinSeq-Locations ; :: thesis: ((Exec i,s1) | ((Int-Locations \/ FinSeq-Locations ) \ {da})) . x = ((Exec i,s2) | ((Int-Locations \/ FinSeq-Locations ) \ {da})) . x

then reconsider a = x as FinSeq-Location by SCMFSA_2:12;
thus ((Exec i,s1) | ((Int-Locations \/ FinSeq-Locations ) \ {da})) . x = (Exec i,s1) . a by A136, FUNCT_1:72
.= s1 . a by A134, SCMFSA_2:100
.= (DataPart s1) . a by A137, FUNCT_1:72, SCMFSA_2:127
.= s2 . a by A1, A137, FUNCT_1:72, SCMFSA_2:127
.= (Exec i,s2) . a by A134, SCMFSA_2:100
.= ((Exec i,s2) | ((Int-Locations \/ FinSeq-Locations ) \ {da})) . x by A136, FUNCT_1:72 ; :: thesis: verum

end;

end;

end;

da in Int-Locations by SCMFSA_2:9;
then da in Int-Locations \/ FinSeq-Locations by XBOOLE_0:def 3;
then A140: Int-Locations \/ FinSeq-Locations = (Int-Locations \/ FinSeq-Locations ) \/ {da} by ZFMISC_1:46
.= ((Int-Locations \/ FinSeq-Locations ) \ {da}) \/ {da} by XBOOLE_1:39 ;
fa in FinSeq-Locations by SCMFSA_2:10;
then A141: fa in Int-Locations \/ FinSeq-Locations by XBOOLE_0:def 3;
then s1 . fa = (s1 | (Int-Locations \/ FinSeq-Locations )) . fa by FUNCT_1:72
.= s2 . fa by A1, A141, FUNCT_1:72, SCMFSA_2:127 ;
then (Exec i,s1) . da = len (s2 . fa) by A134, SCMFSA_2:100
.= (Exec i,s2) . da by A134, SCMFSA_2:100 ;
then A142: (Exec i,s1) | {da} = (Exec i,s2) | {da} by A5, A8, GRFUNC_1:90;
A143: dom ((Exec i,s2) | ((Int-Locations \/ FinSeq-Locations ) \ {da})) = (Int-Locations \/ FinSeq-Locations ) \ {da} by A8, RELAT_1:91;
dom ((Exec i,s1) | ((Int-Locations \/ FinSeq-Locations ) \ {da})) = (Int-Locations \/ FinSeq-Locations ) \ {da} by A5, RELAT_1:91;
then (Exec i,s1) | ((Int-Locations \/ FinSeq-Locations ) \ {da}) = (Exec i,s2) | ((Int-Locations \/ FinSeq-Locations ) \ {da}) by A143, A135, FUNCT_1:9;
hence DataPart (Exec i,s1) = DataPart (Exec i,s2) by A140, A142, RELAT_1:185, SCMFSA_2:127; :: thesis: verum

end;

suppose InsCode i = 12 ; :: thesis: 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:65;
set l = i;
A145: dom ((Exec i,s2) | ((Int-Locations \/ FinSeq-Locations ) \ {fa})) = (Int-Locations \/ FinSeq-Locations ) \ {fa} by A8, RELAT_1:91;
A146: ex k2 being Element of NAT st
( k2 = abs (s2 . da) & (Exec i,s2) . fa = k2 |-> 0 ) by A144, SCMFSA_2:101;
A147: ex k1 being Element of NAT st
( k1 = abs (s1 . da) & (Exec i,s1) . fa = k1 |-> 0 ) by A144, SCMFSA_2:101;
A148: for x being set st x in (Int-Locations \/ FinSeq-Locations ) \ {fa} holds
((Exec i,s1) | ((Int-Locations \/ FinSeq-Locations ) \ {fa})) . x = ((Exec i,s2) | ((Int-Locations \/ FinSeq-Locations ) \ {fa})) . x

proof

let x be set ; :: thesis: ( x in (Int-Locations \/ FinSeq-Locations ) \ {fa} implies ((Exec i,s1) | ((Int-Locations \/ FinSeq-Locations ) \ {fa})) . x = ((Exec i,s2) | ((Int-Locations \/ FinSeq-Locations ) \ {fa})) . x )
assume A149: x in (Int-Locations \/ FinSeq-Locations ) \ {fa} ; :: thesis: ((Exec i,s1) | ((Int-Locations \/ FinSeq-Locations ) \ {fa})) . x = ((Exec i,s2) | ((Int-Locations \/ FinSeq-Locations ) \ {fa})) . x
then A150: x in Int-Locations \/ FinSeq-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, XBOOLE_0:def 3;

suppose x in Int-Locations ; :: thesis: ((Exec i,s1) | ((Int-Locations \/ FinSeq-Locations ) \ {fa})) . x = ((Exec i,s2) | ((Int-Locations \/ FinSeq-Locations ) \ {fa})) . x

then reconsider a = x as Int-Location by SCMFSA_2:11;
thus ((Exec i,s1) | ((Int-Locations \/ FinSeq-Locations ) \ {fa})) . x = (Exec i,s1) . a by A149, FUNCT_1:72
.= s1 . a by A144, SCMFSA_2:101
.= (DataPart s1) . a by A150, FUNCT_1:72, SCMFSA_2:127
.= s2 . a by A1, A150, FUNCT_1:72, SCMFSA_2:127
.= (Exec i,s2) . a by A144, SCMFSA_2:101
.= ((Exec i,s2) | ((Int-Locations \/ FinSeq-Locations ) \ {fa})) . x by A149, FUNCT_1:72 ; :: thesis: verum

end;

suppose x in FinSeq-Locations ; :: thesis: ((Exec i,s1) | ((Int-Locations \/ FinSeq-Locations ) \ {fa})) . x = ((Exec i,s2) | ((Int-Locations \/ FinSeq-Locations ) \ {fa})) . x

then reconsider a = x as FinSeq-Location by SCMFSA_2:12;
A152: a <> fa by A151, TARSKI:def 1;
thus ((Exec i,s1) | ((Int-Locations \/ FinSeq-Locations ) \ {fa})) . x = (Exec i,s1) . a by A149, FUNCT_1:72
.= s1 . a by A144, A152, SCMFSA_2:101
.= (DataPart s1) . a by A150, FUNCT_1:72, SCMFSA_2:127
.= s2 . a by A1, A150, FUNCT_1:72, SCMFSA_2:127
.= (Exec i,s2) . a by A144, A152, SCMFSA_2:101
.= ((Exec i,s2) | ((Int-Locations \/ FinSeq-Locations ) \ {fa})) . x by A149, FUNCT_1:72 ; :: thesis: verum

end;

end;

end;

dom ((Exec i,s1) | ((Int-Locations \/ FinSeq-Locations ) \ {fa})) = (Int-Locations \/ FinSeq-Locations ) \ {fa} by A5, RELAT_1:91;
then A153: (Exec i,s1) | ((Int-Locations \/ FinSeq-Locations ) \ {fa}) = (Exec i,s2) | ((Int-Locations \/ FinSeq-Locations ) \ {fa}) by A145, A148, FUNCT_1:9;
fa in FinSeq-Locations by SCMFSA_2:10;
then fa in Int-Locations \/ FinSeq-Locations by XBOOLE_0:def 3;
then A154: Int-Locations \/ FinSeq-Locations = (Int-Locations \/ FinSeq-Locations ) \/ {fa} by ZFMISC_1:46
.= ((Int-Locations \/ FinSeq-Locations ) \ {fa}) \/ {fa} by XBOOLE_1:39 ;
da in Int-Locations by SCMFSA_2:9;
then A155: da in Int-Locations \/ FinSeq-Locations by XBOOLE_0:def 3;
then s1 . da = (DataPart s1) . da by FUNCT_1:72, SCMFSA_2:127
.= s2 . da by A1, A155, FUNCT_1:72, SCMFSA_2:127 ;
then (Exec i,s1) | {fa} = (Exec i,s2) | {fa} by A6, A147, A146, GRFUNC_1:90;
hence DataPart (Exec i,s1) = DataPart (Exec i,s2) by A154, A153, RELAT_1:185, SCMFSA_2:127; :: thesis: verum

end;

end;