let s1, s2 be State of SCM+FSA ; :: thesis: ( s1 | ((Int-Locations \/ FinSeq-Locations ) \/ {(IC SCM+FSA )}) = s2 | ((Int-Locations \/ FinSeq-Locations ) \/ {(IC SCM+FSA )}) implies for l being Instruction of SCM+FSA holds (Exec l,s1) | ((Int-Locations \/ FinSeq-Locations ) \/ {(IC SCM+FSA )}) = (Exec l,s2) | ((Int-Locations \/ FinSeq-Locations ) \/ {(IC SCM+FSA )}) )
assume A1: s1 | ((Int-Locations \/ FinSeq-Locations ) \/ {(IC SCM+FSA )}) = s2 | ((Int-Locations \/ FinSeq-Locations ) \/ {(IC SCM+FSA )}) ; :: thesis: for l being Instruction of SCM+FSA holds (Exec l,s1) | ((Int-Locations \/ FinSeq-Locations ) \/ {(IC SCM+FSA )}) = (Exec l,s2) | ((Int-Locations \/ FinSeq-Locations ) \/ {(IC SCM+FSA )})
let l be Instruction of SCM+FSA ; :: thesis: (Exec l,s1) | ((Int-Locations \/ FinSeq-Locations ) \/ {(IC SCM+FSA )}) = (Exec l,s2) | ((Int-Locations \/ FinSeq-Locations ) \/ {(IC SCM+FSA )})
IC SCM+FSA in {(IC SCM+FSA )} by TARSKI:def 1;
then A2: IC SCM+FSA in (Int-Locations \/ FinSeq-Locations ) \/ {(IC SCM+FSA )} by XBOOLE_0:def 3;
A3: (Int-Locations \/ FinSeq-Locations ) \/ {(IC SCM+FSA )} c= the carrier of SCM+FSA ;
then (Int-Locations \/ FinSeq-Locations ) \/ {(IC SCM+FSA )} c= dom s1 by AMI_1:79;
then A4: IC SCM+FSA in dom (s1 | ((Int-Locations \/ FinSeq-Locations ) \/ {(IC SCM+FSA )})) by A2, RELAT_1:91;
(Int-Locations \/ FinSeq-Locations ) \/ {(IC SCM+FSA )} c= dom s2 by A3, AMI_1:79;
then A5: IC SCM+FSA in dom (s2 | ((Int-Locations \/ FinSeq-Locations ) \/ {(IC SCM+FSA )})) by A2, RELAT_1:91;
A6: IC s1 = (s2 | ((Int-Locations \/ FinSeq-Locations ) \/ {(IC SCM+FSA )})) . (IC SCM+FSA ) by A1, A4, FUNCT_1:70
.= IC s2 by A5, FUNCT_1:70 ;
A7: dom (Exec l,s1) = the carrier of SCM+FSA by AMI_1:79;
A8: dom (Exec l,s2) = the carrier of SCM+FSA by AMI_1:79;
A9: dom (Exec l,s1) = dom (Exec l,s2) by A7, AMI_1:79;
A10: Int-Locations \/ FinSeq-Locations c= (Int-Locations \/ FinSeq-Locations ) \/ {(IC SCM+FSA )} by XBOOLE_1:7;
A11: InsCode l <= 11 + 1 by SCMFSA_2:35;
A12: ( not InsCode l <= 10 + 1 or InsCode l <= 10 or InsCode l = 11 ) by NAT_1:8;
A13: ( not InsCode l <= 9 + 1 or InsCode l <= 8 + 1 or InsCode l = 10 ) by NAT_1:8;

per cases ( InsCode l <= 8 or InsCode l = 9 or InsCode l = 10 or InsCode l = 11 or InsCode l = 12 ) by A11, A12, A13, NAT_1:8;

suppose InsCode l <= 8 ; :: thesis: (Exec l,s1) | ((Int-Locations \/ FinSeq-Locations ) \/ {(IC SCM+FSA )}) = (Exec l,s2) | ((Int-Locations \/ FinSeq-Locations ) \/ {(IC SCM+FSA )})

then reconsider I = l as Instruction of SCM by SCMFSA_2:34;
reconsider S1 = (s1 | the carrier of SCM ) +* (NAT --> I), S2 = (s2 | the carrier of SCM ) +* (NAT --> I) as State of SCM by SCMFSA_2:73;
A14: dom (NAT --> I) = NAT by FUNCOP_1:19;

now

assume IC SCM in NAT ; :: thesis: contradiction
then reconsider l = IC SCM as Instruction-Location of SCM by AMI_1:def 4;
l = IC SCM ;
hence contradiction by AMI_1:48; :: thesis: verum

end;

then NAT misses {(IC SCM )} by ZFMISC_1:56;
then NAT misses SCM-Data-Loc \/ {(IC SCM )} by AMI_2:29, XBOOLE_1:70;
then A15: (NAT --> I) | (SCM-Data-Loc \/ {(IC SCM )}) = {} by A14, RELAT_1:95;
A16: SCM-Data-Loc c= Int-Locations \/ FinSeq-Locations by XBOOLE_1:7;
A17: S1 | (SCM-Data-Loc \/ {(IC SCM )}) = ((s1 | the carrier of SCM ) | (SCM-Data-Loc \/ {(IC SCM )})) +* {} by A15, FUNCT_4:75
.= (s1 | the carrier of SCM ) | (SCM-Data-Loc \/ {(IC SCM )}) by FUNCT_4:22
.= s1 | (SCM-Data-Loc \/ {(IC SCM )}) by AMI_5:23, RELAT_1:103, XBOOLE_1:7
.= (s1 | ((Int-Locations \/ FinSeq-Locations ) \/ {(IC SCM+FSA )})) | (SCM-Data-Loc \/ {(IC SCM )}) by A16, AMI_3:4, RELAT_1:103, SCMFSA_2:7, XBOOLE_1:9
.= s2 | (SCM-Data-Loc \/ {(IC SCM )}) by A1, A16, AMI_3:4, RELAT_1:103, SCMFSA_2:7, XBOOLE_1:9
.= (s2 | the carrier of SCM ) | (SCM-Data-Loc \/ {(IC SCM )}) by AMI_5:23, RELAT_1:103, XBOOLE_1:7
.= ((s2 | the carrier of SCM ) | (SCM-Data-Loc \/ {(IC SCM )})) +* {} by FUNCT_4:22
.= S2 | (SCM-Data-Loc \/ {(IC SCM )}) by A15, FUNCT_4:75 ;
A18: the carrier of SCM /\ FinSeq-Locations = {} by SCMFSA_1:33, XBOOLE_0:def 7;

now

assume IC SCM+FSA in NAT ; :: thesis: contradiction
then reconsider l = IC SCM+FSA as Instruction-Location of SCM+FSA by AMI_1:def 4;
l = IC SCM+FSA ;
hence contradiction by AMI_1:48; :: thesis: verum

end;

then A19: NAT misses {(IC SCM+FSA )} by ZFMISC_1:56;
NAT misses Int-Locations \/ FinSeq-Locations by SCMFSA_2:13, SCMFSA_2:14, XBOOLE_1:70;
then NAT misses (Int-Locations \/ FinSeq-Locations ) \/ {(IC SCM+FSA )} by A19, XBOOLE_1:70;
then A20: NAT /\ ((Int-Locations \/ FinSeq-Locations ) \/ {(IC SCM+FSA )}) = {} by XBOOLE_0:def 7;
A21: (s1 | NAT ) | ((Int-Locations \/ FinSeq-Locations ) \/ {(IC SCM+FSA )}) = s1 | (NAT /\ ((Int-Locations \/ FinSeq-Locations ) \/ {(IC SCM+FSA )})) by RELAT_1:100
.= {} by A20 ;
(dom (Exec I,S1)) /\ FinSeq-Locations = {} by A18, AMI_1:79;
then dom (Exec I,S1) misses FinSeq-Locations by XBOOLE_0:def 7;
then A22: (Exec I,S1) | FinSeq-Locations = {} by RELAT_1:95;
A23: (Exec I,S1) | ((Int-Locations \/ FinSeq-Locations ) \/ {(IC SCM+FSA )}) = ((Exec I,S1) | (Int-Locations \/ FinSeq-Locations )) +* ((Exec I,S1) | {(IC SCM+FSA )}) by FUNCT_4:83
.= ((DataPart (Exec I,S1)) +* {} ) +* ((Exec I,S1) | {(IC SCM+FSA )}) by A22, AMI_3:72, FUNCT_4:83
.= (DataPart (Exec I,S1)) +* ((Exec I,S1) | {(IC SCM+FSA )}) by FUNCT_4:22
.= (Exec I,S1) | (SCM-Data-Loc \/ {(IC SCM )}) by AMI_3:4, AMI_3:72, FUNCT_4:83, SCMFSA_2:7 ;
A24: (s2 | NAT ) | ((Int-Locations \/ FinSeq-Locations ) \/ {(IC SCM+FSA )}) = s2 | (NAT /\ ((Int-Locations \/ FinSeq-Locations ) \/ {(IC SCM+FSA )})) by RELAT_1:100
.= {} by A20 ;
(dom (Exec I,S2)) /\ FinSeq-Locations = {} by A18, AMI_1:79;
then dom (Exec I,S2) misses FinSeq-Locations by XBOOLE_0:def 7;
then A25: (Exec I,S2) | FinSeq-Locations = {} by RELAT_1:95;
A26: (Exec I,S2) | ((Int-Locations \/ FinSeq-Locations ) \/ {(IC SCM+FSA )}) = ((Exec I,S2) | (Int-Locations \/ FinSeq-Locations )) +* ((Exec I,S2) | {(IC SCM+FSA )}) by FUNCT_4:83
.= ((DataPart (Exec I,S2)) +* {} ) +* ((Exec I,S2) | {(IC SCM+FSA )}) by A25, AMI_3:72, FUNCT_4:83
.= (DataPart (Exec I,S2)) +* ((Exec I,S2) | {(IC SCM+FSA )}) by FUNCT_4:22
.= (Exec I,S2) | (SCM-Data-Loc \/ {(IC SCM )}) by AMI_3:4, AMI_3:72, FUNCT_4:83, SCMFSA_2:7 ;
thus (Exec l,s1) | ((Int-Locations \/ FinSeq-Locations ) \/ {(IC SCM+FSA )}) = ((s1 +* (Exec I,S1)) +* (s1 | NAT )) | ((Int-Locations \/ FinSeq-Locations ) \/ {(IC SCM+FSA )}) by SCMFSA_2:75
.= ((s1 +* (Exec I,S1)) | ((Int-Locations \/ FinSeq-Locations ) \/ {(IC SCM+FSA )})) +* {} by A21, FUNCT_4:75
.= (s1 +* (Exec I,S1)) | ((Int-Locations \/ FinSeq-Locations ) \/ {(IC SCM+FSA )}) by FUNCT_4:22
.= (s1 | ((Int-Locations \/ FinSeq-Locations ) \/ {(IC SCM+FSA )})) +* ((Exec I,S1) | (SCM-Data-Loc \/ {(IC SCM )})) by A23, FUNCT_4:75
.= (s2 | ((Int-Locations \/ FinSeq-Locations ) \/ {(IC SCM+FSA )})) +* ((Exec I,S2) | (SCM-Data-Loc \/ {(IC SCM )})) by A1, A17, AMI_5:58
.= (s2 +* (Exec I,S2)) | ((Int-Locations \/ FinSeq-Locations ) \/ {(IC SCM+FSA )}) by A26, FUNCT_4:75
.= ((s2 +* (Exec I,S2)) | ((Int-Locations \/ FinSeq-Locations ) \/ {(IC SCM+FSA )})) +* {} by FUNCT_4:22
.= ((s2 +* (Exec I,S2)) +* (s2 | NAT )) | ((Int-Locations \/ FinSeq-Locations ) \/ {(IC SCM+FSA )}) by A24, FUNCT_4:75
.= (Exec l,s2) | ((Int-Locations \/ FinSeq-Locations ) \/ {(IC SCM+FSA )}) by SCMFSA_2:75 ; :: thesis: verum

end;

suppose InsCode l = 9 ; :: thesis: (Exec l,s1) | ((Int-Locations \/ FinSeq-Locations ) \/ {(IC SCM+FSA )}) = (Exec l,s2) | ((Int-Locations \/ FinSeq-Locations ) \/ {(IC SCM+FSA )})

then consider da, db being Int-Location , fa being FinSeq-Location such that
A27: l = db := fa,da by SCMFSA_2:62;
db in Int-Locations by SCMFSA_2:9;
then db in Int-Locations \/ FinSeq-Locations by XBOOLE_0:def 3;
then A28: Int-Locations \/ FinSeq-Locations = (Int-Locations \/ FinSeq-Locations ) \/ {db} by ZFMISC_1:46
.= ((Int-Locations \/ FinSeq-Locations ) \ {db}) \/ {db} by XBOOLE_1:39 ;
A29: dom ((Exec l,s1) | ((Int-Locations \/ FinSeq-Locations ) \ {db})) = (Int-Locations \/ FinSeq-Locations ) \ {db} by A7, RELAT_1:91;
A30: dom ((Exec l,s2) | ((Int-Locations \/ FinSeq-Locations ) \ {db})) = (Int-Locations \/ FinSeq-Locations ) \ {db} by A8, RELAT_1:91;
for x being set st x in (Int-Locations \/ FinSeq-Locations ) \ {db} holds
((Exec l,s1) | ((Int-Locations \/ FinSeq-Locations ) \ {db})) . x = ((Exec l,s2) | ((Int-Locations \/ FinSeq-Locations ) \ {db})) . x

proof

let x be set ; :: thesis: ( x in (Int-Locations \/ FinSeq-Locations ) \ {db} implies ((Exec l,s1) | ((Int-Locations \/ FinSeq-Locations ) \ {db})) . x = ((Exec l,s2) | ((Int-Locations \/ FinSeq-Locations ) \ {db})) . x )
assume A31: x in (Int-Locations \/ FinSeq-Locations ) \ {db} ; :: thesis: ((Exec l,s1) | ((Int-Locations \/ FinSeq-Locations ) \ {db})) . x = ((Exec l,s2) | ((Int-Locations \/ FinSeq-Locations ) \ {db})) . x
then A32: x in Int-Locations \/ FinSeq-Locations by XBOOLE_0:def 5;
A33: not x in {db} by A31, XBOOLE_0:def 5;

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

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

then reconsider a = x as Int-Location by SCMFSA_2:11;
A34: a <> db by A33, TARSKI:def 1;
A35: a in (Int-Locations \/ FinSeq-Locations ) \/ {(IC SCM+FSA )} by A32, XBOOLE_0:def 3;
thus ((Exec l,s1) | ((Int-Locations \/ FinSeq-Locations ) \ {db})) . x = (Exec l,s1) . a by A31, FUNCT_1:72
.= s1 . a by A27, A34, SCMFSA_2:98
.= (s1 | ((Int-Locations \/ FinSeq-Locations ) \/ {(IC SCM+FSA )})) . a by A35, FUNCT_1:72
.= s2 . a by A1, A35, FUNCT_1:72
.= (Exec l,s2) . a by A27, A34, SCMFSA_2:98
.= ((Exec l,s2) | ((Int-Locations \/ FinSeq-Locations ) \ {db})) . x by A31, FUNCT_1:72 ; :: thesis: verum

end;

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

then reconsider a = x as FinSeq-Location by SCMFSA_2:12;
A36: a in (Int-Locations \/ FinSeq-Locations ) \/ {(IC SCM+FSA )} by A32, XBOOLE_0:def 3;
thus ((Exec l,s1) | ((Int-Locations \/ FinSeq-Locations ) \ {db})) . x = (Exec l,s1) . a by A31, FUNCT_1:72
.= s1 . a by A27, SCMFSA_2:98
.= (s1 | ((Int-Locations \/ FinSeq-Locations ) \/ {(IC SCM+FSA )})) . a by A36, FUNCT_1:72
.= s2 . a by A1, A36, FUNCT_1:72
.= (Exec l,s2) . a by A27, SCMFSA_2:98
.= ((Exec l,s2) | ((Int-Locations \/ FinSeq-Locations ) \ {db})) . x by A31, FUNCT_1:72 ; :: thesis: verum

end;

end;

end;

then A37: (Exec l,s1) | ((Int-Locations \/ FinSeq-Locations ) \ {db}) = (Exec l,s2) | ((Int-Locations \/ FinSeq-Locations ) \ {db}) by A29, A30, FUNCT_1:9;
da in Int-Locations by SCMFSA_2:9;
then A38: da in Int-Locations \/ FinSeq-Locations by XBOOLE_0:def 3;
consider k1 being Element of NAT such that
A39: k1 = abs (s1 . da) and
A40: (Exec l,s1) . db = (s1 . fa) /. k1 by A27, SCMFSA_2:98;
consider k2 being Element of NAT such that
A41: k2 = abs (s2 . da) and
A42: (Exec l,s2) . db = (s2 . fa) /. k2 by A27, SCMFSA_2:98;
A43: s1 . da = (s1 | ((Int-Locations \/ FinSeq-Locations ) \/ {(IC SCM+FSA )})) . da by A10, A38, FUNCT_1:72
.= s2 . da by A1, A10, A38, FUNCT_1:72 ;
fa in FinSeq-Locations by SCMFSA_2:10;
then fa in Int-Locations \/ FinSeq-Locations by XBOOLE_0:def 3;
then A44: fa in (Int-Locations \/ FinSeq-Locations ) \/ {(IC SCM+FSA )} by XBOOLE_0:def 3;
then s1 . fa = (s1 | ((Int-Locations \/ FinSeq-Locations ) \/ {(IC SCM+FSA )})) . fa by FUNCT_1:72
.= s2 . fa by A1, A44, FUNCT_1:72 ;
then (Exec l,s1) | {db} = (Exec l,s2) | {db} by A9, A39, A40, A41, A42, A43, GRFUNC_1:90;
then A45: DataPart (Exec l,s1) = DataPart (Exec l,s2) by A28, A37, RELAT_1:185, SCMFSA_2:127;
(Exec l,s1) . (IC SCM+FSA ) = Next (IC s1) by A27, SCMFSA_2:98
.= (Exec l,s2) . (IC SCM+FSA ) by A6, A27, SCMFSA_2:98 ;
then (Exec l,s1) | {(IC SCM+FSA )} = (Exec l,s2) | {(IC SCM+FSA )} by A7, A8, GRFUNC_1:90;
hence (Exec l,s1) | ((Int-Locations \/ FinSeq-Locations ) \/ {(IC SCM+FSA )}) = (Exec l,s2) | ((Int-Locations \/ FinSeq-Locations ) \/ {(IC SCM+FSA )}) by A45, RELAT_1:185, SCMFSA_2:127; :: thesis: verum

end;

suppose InsCode l = 10 ; :: thesis: (Exec l,s1) | ((Int-Locations \/ FinSeq-Locations ) \/ {(IC SCM+FSA )}) = (Exec l,s2) | ((Int-Locations \/ FinSeq-Locations ) \/ {(IC SCM+FSA )})

then consider da, db being Int-Location , fa being FinSeq-Location such that
A46: l = fa,da := db by SCMFSA_2:63;
fa in FinSeq-Locations by SCMFSA_2:10;
then fa in Int-Locations \/ FinSeq-Locations by XBOOLE_0:def 3;
then A47: Int-Locations \/ FinSeq-Locations = (Int-Locations \/ FinSeq-Locations ) \/ {fa} by ZFMISC_1:46
.= ((Int-Locations \/ FinSeq-Locations ) \ {fa}) \/ {fa} by XBOOLE_1:39 ;
A48: dom ((Exec l,s1) | ((Int-Locations \/ FinSeq-Locations ) \ {fa})) = (Int-Locations \/ FinSeq-Locations ) \ {fa} by A7, RELAT_1:91;
A49: dom ((Exec l,s2) | ((Int-Locations \/ FinSeq-Locations ) \ {fa})) = (Int-Locations \/ FinSeq-Locations ) \ {fa} by A8, RELAT_1:91;
for x being set st x in (Int-Locations \/ FinSeq-Locations ) \ {fa} holds
((Exec l,s1) | ((Int-Locations \/ FinSeq-Locations ) \ {fa})) . x = ((Exec l,s2) | ((Int-Locations \/ FinSeq-Locations ) \ {fa})) . x

proof

let x be set ; :: thesis: ( x in (Int-Locations \/ FinSeq-Locations ) \ {fa} implies ((Exec l,s1) | ((Int-Locations \/ FinSeq-Locations ) \ {fa})) . x = ((Exec l,s2) | ((Int-Locations \/ FinSeq-Locations ) \ {fa})) . x )
assume A50: x in (Int-Locations \/ FinSeq-Locations ) \ {fa} ; :: thesis: ((Exec l,s1) | ((Int-Locations \/ FinSeq-Locations ) \ {fa})) . x = ((Exec l,s2) | ((Int-Locations \/ FinSeq-Locations ) \ {fa})) . x
then A51: x in Int-Locations \/ FinSeq-Locations by XBOOLE_0:def 5;
A52: not x in {fa} by A50, XBOOLE_0:def 5;

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

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

then reconsider a = x as Int-Location by SCMFSA_2:11;
A53: a in (Int-Locations \/ FinSeq-Locations ) \/ {(IC SCM+FSA )} by A51, XBOOLE_0:def 3;
thus ((Exec l,s1) | ((Int-Locations \/ FinSeq-Locations ) \ {fa})) . x = (Exec l,s1) . a by A50, FUNCT_1:72
.= s1 . a by A46, SCMFSA_2:99
.= (s1 | ((Int-Locations \/ FinSeq-Locations ) \/ {(IC SCM+FSA )})) . a by A53, FUNCT_1:72
.= s2 . a by A1, A53, FUNCT_1:72
.= (Exec l,s2) . a by A46, SCMFSA_2:99
.= ((Exec l,s2) | ((Int-Locations \/ FinSeq-Locations ) \ {fa})) . x by A50, FUNCT_1:72 ; :: thesis: verum

end;

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

then reconsider a = x as FinSeq-Location by SCMFSA_2:12;
A54: a <> fa by A52, TARSKI:def 1;
A55: a in (Int-Locations \/ FinSeq-Locations ) \/ {(IC SCM+FSA )} by A51, XBOOLE_0:def 3;
thus ((Exec l,s1) | ((Int-Locations \/ FinSeq-Locations ) \ {fa})) . x = (Exec l,s1) . a by A50, FUNCT_1:72
.= s1 . a by A46, A54, SCMFSA_2:99
.= (s1 | ((Int-Locations \/ FinSeq-Locations ) \/ {(IC SCM+FSA )})) . a by A55, FUNCT_1:72
.= s2 . a by A1, A55, FUNCT_1:72
.= (Exec l,s2) . a by A46, A54, SCMFSA_2:99
.= ((Exec l,s2) | ((Int-Locations \/ FinSeq-Locations ) \ {fa})) . x by A50, FUNCT_1:72 ; :: thesis: verum

end;

end;

end;

then A56: (Exec l,s1) | ((Int-Locations \/ FinSeq-Locations ) \ {fa}) = (Exec l,s2) | ((Int-Locations \/ FinSeq-Locations ) \ {fa}) by A48, A49, FUNCT_1:9;
da in Int-Locations by SCMFSA_2:9;
then A57: da in Int-Locations \/ FinSeq-Locations by XBOOLE_0:def 3;
consider k1 being Element of NAT such that
A58: k1 = abs (s1 . da) and
A59: (Exec l,s1) . fa = (s1 . fa) +* k1,(s1 . db) by A46, SCMFSA_2:99;
consider k2 being Element of NAT such that
A60: k2 = abs (s2 . da) and
A61: (Exec l,s2) . fa = (s2 . fa) +* k2,(s2 . db) by A46, SCMFSA_2:99;
A62: s1 . da = (s1 | ((Int-Locations \/ FinSeq-Locations ) \/ {(IC SCM+FSA )})) . da by A10, A57, FUNCT_1:72
.= s2 . da by A1, A10, A57, FUNCT_1:72 ;
db in Int-Locations by SCMFSA_2:9;
then A63: db in Int-Locations \/ FinSeq-Locations by XBOOLE_0:def 3;
then A64: s1 . db = (s1 | ((Int-Locations \/ FinSeq-Locations ) \/ {(IC SCM+FSA )})) . db by A10, FUNCT_1:72
.= s2 . db by A1, A10, A63, FUNCT_1:72 ;
fa in FinSeq-Locations by SCMFSA_2:10;
then fa in Int-Locations \/ FinSeq-Locations by XBOOLE_0:def 3;
then A65: fa in (Int-Locations \/ FinSeq-Locations ) \/ {(IC SCM+FSA )} by XBOOLE_0:def 3;
then s1 . fa = (s1 | ((Int-Locations \/ FinSeq-Locations ) \/ {(IC SCM+FSA )})) . fa by FUNCT_1:72
.= s2 . fa by A1, A65, FUNCT_1:72 ;
then (Exec l,s1) | {fa} = (Exec l,s2) | {fa} by A9, A58, A59, A60, A61, A62, A64, GRFUNC_1:90;
then A66: DataPart (Exec l,s1) = DataPart (Exec l,s2) by A47, A56, RELAT_1:185, SCMFSA_2:127;
(Exec l,s1) . (IC SCM+FSA ) = Next (IC s1) by A46, SCMFSA_2:99
.= (Exec l,s2) . (IC SCM+FSA ) by A6, A46, SCMFSA_2:99 ;
then (Exec l,s1) | {(IC SCM+FSA )} = (Exec l,s2) | {(IC SCM+FSA )} by A7, A8, GRFUNC_1:90;
hence (Exec l,s1) | ((Int-Locations \/ FinSeq-Locations ) \/ {(IC SCM+FSA )}) = (Exec l,s2) | ((Int-Locations \/ FinSeq-Locations ) \/ {(IC SCM+FSA )}) by A66, RELAT_1:185, SCMFSA_2:127; :: thesis: verum

end;

suppose InsCode l = 11 ; :: thesis: (Exec l,s1) | ((Int-Locations \/ FinSeq-Locations ) \/ {(IC SCM+FSA )}) = (Exec l,s2) | ((Int-Locations \/ FinSeq-Locations ) \/ {(IC SCM+FSA )})

then consider da being Int-Location , fa being FinSeq-Location such that
A67: l = da :=len fa by SCMFSA_2:64;
da in Int-Locations by SCMFSA_2:9;
then da in Int-Locations \/ FinSeq-Locations by XBOOLE_0:def 3;
then A68: Int-Locations \/ FinSeq-Locations = (Int-Locations \/ FinSeq-Locations ) \/ {da} by ZFMISC_1:46
.= ((Int-Locations \/ FinSeq-Locations ) \ {da}) \/ {da} by XBOOLE_1:39 ;
A69: dom ((Exec l,s1) | ((Int-Locations \/ FinSeq-Locations ) \ {da})) = (Int-Locations \/ FinSeq-Locations ) \ {da} by A7, RELAT_1:91;
A70: dom ((Exec l,s2) | ((Int-Locations \/ FinSeq-Locations ) \ {da})) = (Int-Locations \/ FinSeq-Locations ) \ {da} by A8, RELAT_1:91;
for x being set st x in (Int-Locations \/ FinSeq-Locations ) \ {da} holds
((Exec l,s1) | ((Int-Locations \/ FinSeq-Locations ) \ {da})) . x = ((Exec l,s2) | ((Int-Locations \/ FinSeq-Locations ) \ {da})) . x

proof

let x be set ; :: thesis: ( x in (Int-Locations \/ FinSeq-Locations ) \ {da} implies ((Exec l,s1) | ((Int-Locations \/ FinSeq-Locations ) \ {da})) . x = ((Exec l,s2) | ((Int-Locations \/ FinSeq-Locations ) \ {da})) . x )
assume A71: x in (Int-Locations \/ FinSeq-Locations ) \ {da} ; :: thesis: ((Exec l,s1) | ((Int-Locations \/ FinSeq-Locations ) \ {da})) . x = ((Exec l,s2) | ((Int-Locations \/ FinSeq-Locations ) \ {da})) . x
then A72: x in Int-Locations \/ FinSeq-Locations by XBOOLE_0:def 5;
A73: not x in {da} by A71, XBOOLE_0:def 5;

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

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

then reconsider a = x as Int-Location by SCMFSA_2:11;
A74: a <> da by A73, TARSKI:def 1;
A75: a in (Int-Locations \/ FinSeq-Locations ) \/ {(IC SCM+FSA )} by A72, XBOOLE_0:def 3;
thus ((Exec l,s1) | ((Int-Locations \/ FinSeq-Locations ) \ {da})) . x = (Exec l,s1) . a by A71, FUNCT_1:72
.= s1 . a by A67, A74, SCMFSA_2:100
.= (s1 | ((Int-Locations \/ FinSeq-Locations ) \/ {(IC SCM+FSA )})) . a by A75, FUNCT_1:72
.= s2 . a by A1, A75, FUNCT_1:72
.= (Exec l,s2) . a by A67, A74, SCMFSA_2:100
.= ((Exec l,s2) | ((Int-Locations \/ FinSeq-Locations ) \ {da})) . x by A71, FUNCT_1:72 ; :: thesis: verum

end;

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

then reconsider a = x as FinSeq-Location by SCMFSA_2:12;
A76: a in (Int-Locations \/ FinSeq-Locations ) \/ {(IC SCM+FSA )} by A72, XBOOLE_0:def 3;
thus ((Exec l,s1) | ((Int-Locations \/ FinSeq-Locations ) \ {da})) . x = (Exec l,s1) . a by A71, FUNCT_1:72
.= s1 . a by A67, SCMFSA_2:100
.= (s1 | ((Int-Locations \/ FinSeq-Locations ) \/ {(IC SCM+FSA )})) . a by A76, FUNCT_1:72
.= s2 . a by A1, A76, FUNCT_1:72
.= (Exec l,s2) . a by A67, SCMFSA_2:100
.= ((Exec l,s2) | ((Int-Locations \/ FinSeq-Locations ) \ {da})) . x by A71, FUNCT_1:72 ; :: thesis: verum

end;

end;

end;

then A77: (Exec l,s1) | ((Int-Locations \/ FinSeq-Locations ) \ {da}) = (Exec l,s2) | ((Int-Locations \/ FinSeq-Locations ) \ {da}) by A69, A70, FUNCT_1:9;
fa in FinSeq-Locations by SCMFSA_2:10;
then fa in Int-Locations \/ FinSeq-Locations by XBOOLE_0:def 3;
then A78: fa in (Int-Locations \/ FinSeq-Locations ) \/ {(IC SCM+FSA )} by XBOOLE_0:def 3;
then s1 . fa = (s1 | ((Int-Locations \/ FinSeq-Locations ) \/ {(IC SCM+FSA )})) . fa by FUNCT_1:72
.= s2 . fa by A1, A78, FUNCT_1:72 ;
then (Exec l,s1) . da = len (s2 . fa) by A67, SCMFSA_2:100
.= (Exec l,s2) . da by A67, SCMFSA_2:100 ;
then (Exec l,s1) | {da} = (Exec l,s2) | {da} by A7, A8, GRFUNC_1:90;
then A79: DataPart (Exec l,s1) = DataPart (Exec l,s2) by A68, A77, RELAT_1:185, SCMFSA_2:127;
(Exec l,s1) . (IC SCM+FSA ) = Next (IC s1) by A67, SCMFSA_2:100
.= (Exec l,s2) . (IC SCM+FSA ) by A6, A67, SCMFSA_2:100 ;
then (Exec l,s1) | {(IC SCM+FSA )} = (Exec l,s2) | {(IC SCM+FSA )} by A7, A8, GRFUNC_1:90;
hence (Exec l,s1) | ((Int-Locations \/ FinSeq-Locations ) \/ {(IC SCM+FSA )}) = (Exec l,s2) | ((Int-Locations \/ FinSeq-Locations ) \/ {(IC SCM+FSA )}) by A79, RELAT_1:185, SCMFSA_2:127; :: thesis: verum

end;

suppose InsCode l = 12 ; :: thesis: (Exec l,s1) | ((Int-Locations \/ FinSeq-Locations ) \/ {(IC SCM+FSA )}) = (Exec l,s2) | ((Int-Locations \/ FinSeq-Locations ) \/ {(IC SCM+FSA )})

then consider da being Int-Location , fa being FinSeq-Location such that
A80: l = fa :=<0,...,0> da by SCMFSA_2:65;
fa in FinSeq-Locations by SCMFSA_2:10;
then fa in Int-Locations \/ FinSeq-Locations by XBOOLE_0:def 3;
then A81: Int-Locations \/ FinSeq-Locations = (Int-Locations \/ FinSeq-Locations ) \/ {fa} by ZFMISC_1:46
.= ((Int-Locations \/ FinSeq-Locations ) \ {fa}) \/ {fa} by XBOOLE_1:39 ;
A82: dom ((Exec l,s1) | ((Int-Locations \/ FinSeq-Locations ) \ {fa})) = (Int-Locations \/ FinSeq-Locations ) \ {fa} by A7, RELAT_1:91;
A83: dom ((Exec l,s2) | ((Int-Locations \/ FinSeq-Locations ) \ {fa})) = (Int-Locations \/ FinSeq-Locations ) \ {fa} by A8, RELAT_1:91;
for x being set st x in (Int-Locations \/ FinSeq-Locations ) \ {fa} holds
((Exec l,s1) | ((Int-Locations \/ FinSeq-Locations ) \ {fa})) . x = ((Exec l,s2) | ((Int-Locations \/ FinSeq-Locations ) \ {fa})) . x

proof

let x be set ; :: thesis: ( x in (Int-Locations \/ FinSeq-Locations ) \ {fa} implies ((Exec l,s1) | ((Int-Locations \/ FinSeq-Locations ) \ {fa})) . x = ((Exec l,s2) | ((Int-Locations \/ FinSeq-Locations ) \ {fa})) . x )
assume A84: x in (Int-Locations \/ FinSeq-Locations ) \ {fa} ; :: thesis: ((Exec l,s1) | ((Int-Locations \/ FinSeq-Locations ) \ {fa})) . x = ((Exec l,s2) | ((Int-Locations \/ FinSeq-Locations ) \ {fa})) . x
then A85: x in Int-Locations \/ FinSeq-Locations by XBOOLE_0:def 5;
A86: not x in {fa} by A84, XBOOLE_0:def 5;

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

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

then reconsider a = x as Int-Location by SCMFSA_2:11;
A87: a in (Int-Locations \/ FinSeq-Locations ) \/ {(IC SCM+FSA )} by A85, XBOOLE_0:def 3;
thus ((Exec l,s1) | ((Int-Locations \/ FinSeq-Locations ) \ {fa})) . x = (Exec l,s1) . a by A84, FUNCT_1:72
.= s1 . a by A80, SCMFSA_2:101
.= (s1 | ((Int-Locations \/ FinSeq-Locations ) \/ {(IC SCM+FSA )})) . a by A87, FUNCT_1:72
.= s2 . a by A1, A87, FUNCT_1:72
.= (Exec l,s2) . a by A80, SCMFSA_2:101
.= ((Exec l,s2) | ((Int-Locations \/ FinSeq-Locations ) \ {fa})) . x by A84, FUNCT_1:72 ; :: thesis: verum

end;

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

then reconsider a = x as FinSeq-Location by SCMFSA_2:12;
A88: a <> fa by A86, TARSKI:def 1;
A89: a in (Int-Locations \/ FinSeq-Locations ) \/ {(IC SCM+FSA )} by A85, XBOOLE_0:def 3;
thus ((Exec l,s1) | ((Int-Locations \/ FinSeq-Locations ) \ {fa})) . x = (Exec l,s1) . a by A84, FUNCT_1:72
.= s1 . a by A80, A88, SCMFSA_2:101
.= (s1 | ((Int-Locations \/ FinSeq-Locations ) \/ {(IC SCM+FSA )})) . a by A89, FUNCT_1:72
.= s2 . a by A1, A89, FUNCT_1:72
.= (Exec l,s2) . a by A80, A88, SCMFSA_2:101
.= ((Exec l,s2) | ((Int-Locations \/ FinSeq-Locations ) \ {fa})) . x by A84, FUNCT_1:72 ; :: thesis: verum

end;

end;

end;

then A90: (Exec l,s1) | ((Int-Locations \/ FinSeq-Locations ) \ {fa}) = (Exec l,s2) | ((Int-Locations \/ FinSeq-Locations ) \ {fa}) by A82, A83, FUNCT_1:9;
da in Int-Locations by SCMFSA_2:9;
then A91: da in Int-Locations \/ FinSeq-Locations by XBOOLE_0:def 3;
consider k1 being Element of NAT such that
A92: k1 = abs (s1 . da) and
A93: (Exec l,s1) . fa = k1 |-> 0 by A80, SCMFSA_2:101;
consider k2 being Element of NAT such that
A94: k2 = abs (s2 . da) and
A95: (Exec l,s2) . fa = k2 |-> 0 by A80, SCMFSA_2:101;
s1 . da = (s1 | ((Int-Locations \/ FinSeq-Locations ) \/ {(IC SCM+FSA )})) . da by A10, A91, FUNCT_1:72
.= s2 . da by A1, A10, A91, FUNCT_1:72 ;
then (Exec l,s1) | {fa} = (Exec l,s2) | {fa} by A9, A92, A93, A94, A95, GRFUNC_1:90;
then A96: DataPart (Exec l,s1) = DataPart (Exec l,s2) by A81, A90, RELAT_1:185, SCMFSA_2:127;
(Exec l,s1) . (IC SCM+FSA ) = Next (IC s1) by A80, SCMFSA_2:101
.= (Exec l,s2) . (IC SCM+FSA ) by A6, A80, SCMFSA_2:101 ;
then (Exec l,s1) | {(IC SCM+FSA )} = (Exec l,s2) | {(IC SCM+FSA )} by A7, A8, GRFUNC_1:90;
hence (Exec l,s1) | ((Int-Locations \/ FinSeq-Locations ) \/ {(IC SCM+FSA )}) = (Exec l,s2) | ((Int-Locations \/ FinSeq-Locations ) \/ {(IC SCM+FSA )}) by A96, RELAT_1:185, SCMFSA_2:127; :: thesis: verum

end;

end;