IC SCM+FSA in {(IC SCM+FSA )} by TARSKI:def 1;
then A1: IC SCM+FSA in (Int-Locations \/ FinSeq-Locations ) \/ {(IC SCM+FSA )} by XBOOLE_0:def 3;
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 A2: 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 )})
A3: (Int-Locations \/ FinSeq-Locations ) \/ {(IC SCM+FSA )} c= the carrier of SCM+FSA ;
then (Int-Locations \/ FinSeq-Locations ) \/ {(IC SCM+FSA )} c= dom s2 by PARTFUN1:def 4;
then A4: IC SCM+FSA in dom (s2 | ((Int-Locations \/ FinSeq-Locations ) \/ {(IC SCM+FSA )})) by A1, RELAT_1:91;
(Int-Locations \/ FinSeq-Locations ) \/ {(IC SCM+FSA )} c= dom s1 by A3, PARTFUN1:def 4;
then IC SCM+FSA in dom (s1 | ((Int-Locations \/ FinSeq-Locations ) \/ {(IC SCM+FSA )})) by A1, RELAT_1:91;
then A5: IC s1 = (s2 | ((Int-Locations \/ FinSeq-Locations ) \/ {(IC SCM+FSA )})) . (IC SCM+FSA ) by A2, FUNCT_1:70
.= IC s2 by A4, FUNCT_1:70 ;
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 )})
A6: dom (Exec l,s2) = the carrier of SCM+FSA by PARTFUN1:def 4;
A7: ( not InsCode l <= 9 + 1 or InsCode l <= 8 + 1 or InsCode l = 10 ) by NAT_1:8;
A8: ( not InsCode l <= 10 + 1 or InsCode l <= 10 or InsCode l = 11 ) by NAT_1:8;
A9: InsCode l <= 11 + 1 by SCMFSA_2:35;
A10: dom (Exec l,s1) = the carrier of SCM+FSA by PARTFUN1:def 4;
then A11: dom (Exec l,s1) = dom (Exec l,s2) by PARTFUN1:def 4;
A12: Int-Locations \/ FinSeq-Locations c= (Int-Locations \/ FinSeq-Locations ) \/ {(IC SCM+FSA )} by XBOOLE_1:7;

per cases ( InsCode l <= 8 or InsCode l = 9 or InsCode l = 10 or InsCode l = 11 or InsCode l = 12 ) by A9, A8, A7, 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;
A13: SCM-Data-Loc c= Int-Locations \/ FinSeq-Locations by XBOOLE_1:7;
not IC SCM+FSA in NAT by COMPOS_1:3;
then A14: 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 A14, XBOOLE_1:70;
then A15: NAT /\ ((Int-Locations \/ FinSeq-Locations ) \/ {(IC SCM+FSA )}) = {} by XBOOLE_0:def 7;
not IC SCM in NAT by COMPOS_1:3;
then NAT misses {(IC SCM )} by ZFMISC_1:56;
then ( dom (NAT --> I) = NAT & NAT misses SCM-Data-Loc \/ {(IC SCM )} ) by AMI_2:29, FUNCOP_1:19, XBOOLE_1:70;
then A16: (NAT --> I) | (SCM-Data-Loc \/ {(IC SCM )}) = {} by RELAT_1:95;
then A17: S1 | (SCM-Data-Loc \/ {(IC SCM )}) = ((s1 | the carrier of SCM ) | (SCM-Data-Loc \/ {(IC SCM )})) +* {} by 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 A13, AMI_3:4, RELAT_1:103, SCMFSA_2:7, XBOOLE_1:9
.= s2 | (SCM-Data-Loc \/ {(IC SCM )}) by A2, A13, 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 A16, FUNCT_4:75 ;
A18: the carrier of SCM /\ FinSeq-Locations = {} by SCMFSA_1:33, XBOOLE_0:def 7;
then (dom (Exec I,S1)) /\ FinSeq-Locations = {} by PARTFUN1:def 4;
then dom (Exec I,S1) misses FinSeq-Locations by XBOOLE_0:def 7;
then A19: (Exec I,S1) | FinSeq-Locations = {} by RELAT_1:95;
A20: (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 A19, 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 ;
A21: (s1 | NAT ) | ((Int-Locations \/ FinSeq-Locations ) \/ {(IC SCM+FSA )}) = s1 | (NAT /\ ((Int-Locations \/ FinSeq-Locations ) \/ {(IC SCM+FSA )})) by RELAT_1:100
.= {} by A15 ;
(dom (Exec I,S2)) /\ FinSeq-Locations = {} by A18, PARTFUN1:def 4;
then dom (Exec I,S2) misses FinSeq-Locations by XBOOLE_0:def 7;
then A22: (Exec I,S2) | FinSeq-Locations = {} by RELAT_1:95;
A23: (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 A22, 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 ;
A24: (s2 | NAT ) | ((Int-Locations \/ FinSeq-Locations ) \/ {(IC SCM+FSA )}) = s2 | (NAT /\ ((Int-Locations \/ FinSeq-Locations ) \/ {(IC SCM+FSA )})) by RELAT_1:100
.= {} by A15 ;
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 A20, FUNCT_4:75
.= (s2 | ((Int-Locations \/ FinSeq-Locations ) \/ {(IC SCM+FSA )})) +* ((Exec I,S2) | (SCM-Data-Loc \/ {(IC SCM )})) by A2, A17, AMI_5:58
.= (s2 +* (Exec I,S2)) | ((Int-Locations \/ FinSeq-Locations ) \/ {(IC SCM+FSA )}) by A23, 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
A25: l = db := fa,da by SCMFSA_2:62;
A26: 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 A27: 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 A28: x in Int-Locations \/ FinSeq-Locations by XBOOLE_0:def 5;
A29: not x in {db} by A27, XBOOLE_0:def 5;

per cases ( x in Int-Locations or x in FinSeq-Locations ) by A28, 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;
A30: a <> db by A29, TARSKI:def 1;
A31: a in (Int-Locations \/ FinSeq-Locations ) \/ {(IC SCM+FSA )} by A28, XBOOLE_0:def 3;
thus ((Exec l,s1) | ((Int-Locations \/ FinSeq-Locations ) \ {db})) . x = (Exec l,s1) . a by A27, FUNCT_1:72
.= s1 . a by A25, A30, SCMFSA_2:98
.= (s1 | ((Int-Locations \/ FinSeq-Locations ) \/ {(IC SCM+FSA )})) . a by A31, FUNCT_1:72
.= s2 . a by A2, A31, FUNCT_1:72
.= (Exec l,s2) . a by A25, A30, SCMFSA_2:98
.= ((Exec l,s2) | ((Int-Locations \/ FinSeq-Locations ) \ {db})) . x by A27, 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;
A32: a in (Int-Locations \/ FinSeq-Locations ) \/ {(IC SCM+FSA )} by A28, XBOOLE_0:def 3;
thus ((Exec l,s1) | ((Int-Locations \/ FinSeq-Locations ) \ {db})) . x = (Exec l,s1) . a by A27, FUNCT_1:72
.= s1 . a by A25, SCMFSA_2:98
.= (s1 | ((Int-Locations \/ FinSeq-Locations ) \/ {(IC SCM+FSA )})) . a by A32, FUNCT_1:72
.= s2 . a by A2, A32, FUNCT_1:72
.= (Exec l,s2) . a by A25, SCMFSA_2:98
.= ((Exec l,s2) | ((Int-Locations \/ FinSeq-Locations ) \ {db})) . x by A27, FUNCT_1:72 ; :: thesis: verum

end;

end;

end;

( dom ((Exec l,s1) | ((Int-Locations \/ FinSeq-Locations ) \ {db})) = (Int-Locations \/ FinSeq-Locations ) \ {db} & dom ((Exec l,s2) | ((Int-Locations \/ FinSeq-Locations ) \ {db})) = (Int-Locations \/ FinSeq-Locations ) \ {db} ) by A10, A6, RELAT_1:91;
then A33: (Exec l,s1) | ((Int-Locations \/ FinSeq-Locations ) \ {db}) = (Exec l,s2) | ((Int-Locations \/ FinSeq-Locations ) \ {db}) by A26, FUNCT_1:9;
db in Int-Locations by SCMFSA_2:9;
then db in Int-Locations \/ FinSeq-Locations by XBOOLE_0:def 3;
then A34: Int-Locations \/ FinSeq-Locations = (Int-Locations \/ FinSeq-Locations ) \/ {db} by ZFMISC_1:46
.= ((Int-Locations \/ FinSeq-Locations ) \ {db}) \/ {db} by XBOOLE_1:39 ;
(Exec l,s1) . (IC SCM+FSA ) = succ (IC s1) by A25, SCMFSA_2:98
.= (Exec l,s2) . (IC SCM+FSA ) by A5, A25, SCMFSA_2:98 ;
then A35: (Exec l,s1) | {(IC SCM+FSA )} = (Exec l,s2) | {(IC SCM+FSA )} by A10, A6, GRFUNC_1:90;
A36: ( ex k1 being Element of NAT st
( k1 = abs (s1 . da) & (Exec l,s1) . db = (s1 . fa) /. k1 ) & ex k2 being Element of NAT st
( k2 = abs (s2 . da) & (Exec l,s2) . db = (s2 . fa) /. k2 ) ) by A25, SCMFSA_2:98;
fa in FinSeq-Locations by SCMFSA_2:10;
then fa in Int-Locations \/ FinSeq-Locations by XBOOLE_0:def 3;
then A37: fa in (Int-Locations \/ FinSeq-Locations ) \/ {(IC SCM+FSA )} by XBOOLE_0:def 3;
then A38: s1 . fa = (s1 | ((Int-Locations \/ FinSeq-Locations ) \/ {(IC SCM+FSA )})) . fa by FUNCT_1:72
.= s2 . fa by A2, A37, FUNCT_1:72 ;
da in Int-Locations by SCMFSA_2:9;
then A39: da in Int-Locations \/ FinSeq-Locations by XBOOLE_0:def 3;
then s1 . da = (s1 | ((Int-Locations \/ FinSeq-Locations ) \/ {(IC SCM+FSA )})) . da by A12, FUNCT_1:72
.= s2 . da by A2, A12, A39, FUNCT_1:72 ;
then (Exec l,s1) | {db} = (Exec l,s2) | {db} by A11, A36, A38, GRFUNC_1:90;
then DataPart (Exec l,s1) = DataPart (Exec l,s2) by A34, A33, RELAT_1:185, SCMFSA_2:127;
hence (Exec l,s1) | ((Int-Locations \/ FinSeq-Locations ) \/ {(IC SCM+FSA )}) = (Exec l,s2) | ((Int-Locations \/ FinSeq-Locations ) \/ {(IC SCM+FSA )}) by A35, 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
A40: l = fa,da := db by SCMFSA_2:63;
A41: 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 A42: 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 A43: x in Int-Locations \/ FinSeq-Locations by XBOOLE_0:def 5;
A44: not x in {fa} by A42, XBOOLE_0:def 5;

per cases ( x in Int-Locations or x in FinSeq-Locations ) by A43, 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;
A45: a in (Int-Locations \/ FinSeq-Locations ) \/ {(IC SCM+FSA )} by A43, XBOOLE_0:def 3;
thus ((Exec l,s1) | ((Int-Locations \/ FinSeq-Locations ) \ {fa})) . x = (Exec l,s1) . a by A42, FUNCT_1:72
.= s1 . a by A40, SCMFSA_2:99
.= (s1 | ((Int-Locations \/ FinSeq-Locations ) \/ {(IC SCM+FSA )})) . a by A45, FUNCT_1:72
.= s2 . a by A2, A45, FUNCT_1:72
.= (Exec l,s2) . a by A40, SCMFSA_2:99
.= ((Exec l,s2) | ((Int-Locations \/ FinSeq-Locations ) \ {fa})) . x by A42, 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;
A46: a <> fa by A44, TARSKI:def 1;
A47: a in (Int-Locations \/ FinSeq-Locations ) \/ {(IC SCM+FSA )} by A43, XBOOLE_0:def 3;
thus ((Exec l,s1) | ((Int-Locations \/ FinSeq-Locations ) \ {fa})) . x = (Exec l,s1) . a by A42, FUNCT_1:72
.= s1 . a by A40, A46, SCMFSA_2:99
.= (s1 | ((Int-Locations \/ FinSeq-Locations ) \/ {(IC SCM+FSA )})) . a by A47, FUNCT_1:72
.= s2 . a by A2, A47, FUNCT_1:72
.= (Exec l,s2) . a by A40, A46, SCMFSA_2:99
.= ((Exec l,s2) | ((Int-Locations \/ FinSeq-Locations ) \ {fa})) . x by A42, FUNCT_1:72 ; :: thesis: verum

end;

end;

end;

( dom ((Exec l,s1) | ((Int-Locations \/ FinSeq-Locations ) \ {fa})) = (Int-Locations \/ FinSeq-Locations ) \ {fa} & dom ((Exec l,s2) | ((Int-Locations \/ FinSeq-Locations ) \ {fa})) = (Int-Locations \/ FinSeq-Locations ) \ {fa} ) by A10, A6, RELAT_1:91;
then A48: (Exec l,s1) | ((Int-Locations \/ FinSeq-Locations ) \ {fa}) = (Exec l,s2) | ((Int-Locations \/ FinSeq-Locations ) \ {fa}) by A41, FUNCT_1:9;
fa in FinSeq-Locations by SCMFSA_2:10;
then fa in Int-Locations \/ FinSeq-Locations by XBOOLE_0:def 3;
then A49: 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 fa in Int-Locations \/ FinSeq-Locations by XBOOLE_0:def 3;
then A50: fa in (Int-Locations \/ FinSeq-Locations ) \/ {(IC SCM+FSA )} by XBOOLE_0:def 3;
then A51: s1 . fa = (s1 | ((Int-Locations \/ FinSeq-Locations ) \/ {(IC SCM+FSA )})) . fa by FUNCT_1:72
.= s2 . fa by A2, A50, FUNCT_1:72 ;
db in Int-Locations by SCMFSA_2:9;
then A52: db in Int-Locations \/ FinSeq-Locations by XBOOLE_0:def 3;
then A53: s1 . db = (s1 | ((Int-Locations \/ FinSeq-Locations ) \/ {(IC SCM+FSA )})) . db by A12, FUNCT_1:72
.= s2 . db by A2, A12, A52, FUNCT_1:72 ;
(Exec l,s1) . (IC SCM+FSA ) = succ (IC s1) by A40, SCMFSA_2:99
.= (Exec l,s2) . (IC SCM+FSA ) by A5, A40, SCMFSA_2:99 ;
then A54: (Exec l,s1) | {(IC SCM+FSA )} = (Exec l,s2) | {(IC SCM+FSA )} by A10, A6, GRFUNC_1:90;
A55: ( ex k1 being Element of NAT st
( k1 = abs (s1 . da) & (Exec l,s1) . fa = (s1 . fa) +* k1,(s1 . db) ) & ex k2 being Element of NAT st
( k2 = abs (s2 . da) & (Exec l,s2) . fa = (s2 . fa) +* k2,(s2 . db) ) ) by A40, SCMFSA_2:99;
da in Int-Locations by SCMFSA_2:9;
then A56: da in Int-Locations \/ FinSeq-Locations by XBOOLE_0:def 3;
then s1 . da = (s1 | ((Int-Locations \/ FinSeq-Locations ) \/ {(IC SCM+FSA )})) . da by A12, FUNCT_1:72
.= s2 . da by A2, A12, A56, FUNCT_1:72 ;
then (Exec l,s1) | {fa} = (Exec l,s2) | {fa} by A11, A55, A53, A51, GRFUNC_1:90;
then DataPart (Exec l,s1) = DataPart (Exec l,s2) by A49, A48, RELAT_1:185, SCMFSA_2:127;
hence (Exec l,s1) | ((Int-Locations \/ FinSeq-Locations ) \/ {(IC SCM+FSA )}) = (Exec l,s2) | ((Int-Locations \/ FinSeq-Locations ) \/ {(IC SCM+FSA )}) by A54, 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
A57: l = da :=len fa by SCMFSA_2:64;
fa in FinSeq-Locations by SCMFSA_2:10;
then fa in Int-Locations \/ FinSeq-Locations by XBOOLE_0:def 3;
then A58: 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 A2, A58, FUNCT_1:72 ;
then (Exec l,s1) . da = len (s2 . fa) by A57, SCMFSA_2:100
.= (Exec l,s2) . da by A57, SCMFSA_2:100 ;
then A59: (Exec l,s1) | {da} = (Exec l,s2) | {da} by A10, A6, GRFUNC_1:90;
da in Int-Locations by SCMFSA_2:9;
then da in Int-Locations \/ FinSeq-Locations by XBOOLE_0:def 3;
then A60: Int-Locations \/ FinSeq-Locations = (Int-Locations \/ FinSeq-Locations ) \/ {da} by ZFMISC_1:46
.= ((Int-Locations \/ FinSeq-Locations ) \ {da}) \/ {da} by XBOOLE_1:39 ;
A61: 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 A62: 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 A63: x in Int-Locations \/ FinSeq-Locations by XBOOLE_0:def 5;
A64: not x in {da} by A62, XBOOLE_0:def 5;

per cases ( x in Int-Locations or x in FinSeq-Locations ) by A63, 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;
A65: a <> da by A64, TARSKI:def 1;
A66: a in (Int-Locations \/ FinSeq-Locations ) \/ {(IC SCM+FSA )} by A63, XBOOLE_0:def 3;
thus ((Exec l,s1) | ((Int-Locations \/ FinSeq-Locations ) \ {da})) . x = (Exec l,s1) . a by A62, FUNCT_1:72
.= s1 . a by A57, A65, SCMFSA_2:100
.= (s1 | ((Int-Locations \/ FinSeq-Locations ) \/ {(IC SCM+FSA )})) . a by A66, FUNCT_1:72
.= s2 . a by A2, A66, FUNCT_1:72
.= (Exec l,s2) . a by A57, A65, SCMFSA_2:100
.= ((Exec l,s2) | ((Int-Locations \/ FinSeq-Locations ) \ {da})) . x by A62, 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;
A67: a in (Int-Locations \/ FinSeq-Locations ) \/ {(IC SCM+FSA )} by A63, XBOOLE_0:def 3;
thus ((Exec l,s1) | ((Int-Locations \/ FinSeq-Locations ) \ {da})) . x = (Exec l,s1) . a by A62, FUNCT_1:72
.= s1 . a by A57, SCMFSA_2:100
.= (s1 | ((Int-Locations \/ FinSeq-Locations ) \/ {(IC SCM+FSA )})) . a by A67, FUNCT_1:72
.= s2 . a by A2, A67, FUNCT_1:72
.= (Exec l,s2) . a by A57, SCMFSA_2:100
.= ((Exec l,s2) | ((Int-Locations \/ FinSeq-Locations ) \ {da})) . x by A62, FUNCT_1:72 ; :: thesis: verum

end;

end;

end;

(Exec l,s1) . (IC SCM+FSA ) = succ (IC s1) by A57, SCMFSA_2:100
.= (Exec l,s2) . (IC SCM+FSA ) by A5, A57, SCMFSA_2:100 ;
then A68: (Exec l,s1) | {(IC SCM+FSA )} = (Exec l,s2) | {(IC SCM+FSA )} by A10, A6, GRFUNC_1:90;
( dom ((Exec l,s1) | ((Int-Locations \/ FinSeq-Locations ) \ {da})) = (Int-Locations \/ FinSeq-Locations ) \ {da} & dom ((Exec l,s2) | ((Int-Locations \/ FinSeq-Locations ) \ {da})) = (Int-Locations \/ FinSeq-Locations ) \ {da} ) by A10, A6, RELAT_1:91;
then (Exec l,s1) | ((Int-Locations \/ FinSeq-Locations ) \ {da}) = (Exec l,s2) | ((Int-Locations \/ FinSeq-Locations ) \ {da}) by A61, FUNCT_1:9;
then DataPart (Exec l,s1) = DataPart (Exec l,s2) by A60, A59, RELAT_1:185, SCMFSA_2:127;
hence (Exec l,s1) | ((Int-Locations \/ FinSeq-Locations ) \/ {(IC SCM+FSA )}) = (Exec l,s2) | ((Int-Locations \/ FinSeq-Locations ) \/ {(IC SCM+FSA )}) by A68, 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
A69: l = fa :=<0,...,0> da by SCMFSA_2:65;
A70: 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 A71: 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 A72: x in Int-Locations \/ FinSeq-Locations by XBOOLE_0:def 5;
A73: not x in {fa} 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 ) \ {fa})) . x = ((Exec l,s2) | ((Int-Locations \/ FinSeq-Locations ) \ {fa})) . x

then reconsider a = x as Int-Location by SCMFSA_2:11;
A74: a in (Int-Locations \/ FinSeq-Locations ) \/ {(IC SCM+FSA )} by A72, XBOOLE_0:def 3;
thus ((Exec l,s1) | ((Int-Locations \/ FinSeq-Locations ) \ {fa})) . x = (Exec l,s1) . a by A71, FUNCT_1:72
.= s1 . a by A69, SCMFSA_2:101
.= (s1 | ((Int-Locations \/ FinSeq-Locations ) \/ {(IC SCM+FSA )})) . a by A74, FUNCT_1:72
.= s2 . a by A2, A74, FUNCT_1:72
.= (Exec l,s2) . a by A69, SCMFSA_2:101
.= ((Exec l,s2) | ((Int-Locations \/ FinSeq-Locations ) \ {fa})) . x by A71, 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;
A75: a <> fa by A73, TARSKI:def 1;
A76: a in (Int-Locations \/ FinSeq-Locations ) \/ {(IC SCM+FSA )} by A72, XBOOLE_0:def 3;
thus ((Exec l,s1) | ((Int-Locations \/ FinSeq-Locations ) \ {fa})) . x = (Exec l,s1) . a by A71, FUNCT_1:72
.= s1 . a by A69, A75, SCMFSA_2:101
.= (s1 | ((Int-Locations \/ FinSeq-Locations ) \/ {(IC SCM+FSA )})) . a by A76, FUNCT_1:72
.= s2 . a by A2, A76, FUNCT_1:72
.= (Exec l,s2) . a by A69, A75, SCMFSA_2:101
.= ((Exec l,s2) | ((Int-Locations \/ FinSeq-Locations ) \ {fa})) . x by A71, FUNCT_1:72 ; :: thesis: verum

end;

end;

end;

( dom ((Exec l,s1) | ((Int-Locations \/ FinSeq-Locations ) \ {fa})) = (Int-Locations \/ FinSeq-Locations ) \ {fa} & dom ((Exec l,s2) | ((Int-Locations \/ FinSeq-Locations ) \ {fa})) = (Int-Locations \/ FinSeq-Locations ) \ {fa} ) by A10, A6, RELAT_1:91;
then A77: (Exec l,s1) | ((Int-Locations \/ FinSeq-Locations ) \ {fa}) = (Exec l,s2) | ((Int-Locations \/ FinSeq-Locations ) \ {fa}) by 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: Int-Locations \/ FinSeq-Locations = (Int-Locations \/ FinSeq-Locations ) \/ {fa} by ZFMISC_1:46
.= ((Int-Locations \/ FinSeq-Locations ) \ {fa}) \/ {fa} by XBOOLE_1:39 ;
(Exec l,s1) . (IC SCM+FSA ) = succ (IC s1) by A69, SCMFSA_2:101
.= (Exec l,s2) . (IC SCM+FSA ) by A5, A69, SCMFSA_2:101 ;
then A79: (Exec l,s1) | {(IC SCM+FSA )} = (Exec l,s2) | {(IC SCM+FSA )} by A10, A6, GRFUNC_1:90;
A80: ( ex k1 being Element of NAT st
( k1 = abs (s1 . da) & (Exec l,s1) . fa = k1 |-> 0 ) & ex k2 being Element of NAT st
( k2 = abs (s2 . da) & (Exec l,s2) . fa = k2 |-> 0 ) ) by A69, SCMFSA_2:101;
da in Int-Locations by SCMFSA_2:9;
then A81: da in Int-Locations \/ FinSeq-Locations by XBOOLE_0:def 3;
then s1 . da = (s1 | ((Int-Locations \/ FinSeq-Locations ) \/ {(IC SCM+FSA )})) . da by A12, FUNCT_1:72
.= s2 . da by A2, A12, A81, FUNCT_1:72 ;
then (Exec l,s1) | {fa} = (Exec l,s2) | {fa} by A11, A80, GRFUNC_1:90;
then DataPart (Exec l,s1) = DataPart (Exec l,s2) by A78, A77, RELAT_1:185, SCMFSA_2:127;
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;

end;