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: Data-Locations SCM c= Int-Locations \/ FinSeq-Locations by AMI_3:72, 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 (Data-Locations SCM) \/ {(IC SCM)} ) by AMI_2:29, AMI_3:72, FUNCOP_1:19, XBOOLE_1:70;
then A16: (NAT --> I) | ((Data-Locations SCM) \/ {(IC SCM)}) = {} by RELAT_1:95;
then A17: S1 | ((Data-Locations SCM) \/ {(IC SCM)}) = ((s1 | the carrier of SCM) | ((Data-Locations SCM) \/ {(IC SCM)})) +* {} by FUNCT_4:75
.= (s1 | the carrier of SCM) | ((Data-Locations SCM) \/ {(IC SCM)}) by FUNCT_4:22
.= s1 | ((Data-Locations SCM) \/ {(IC SCM)}) by RELAT_1:103
.= (s1 | ((Int-Locations \/ FinSeq-Locations) \/ {(IC SCM+FSA)})) | ((Data-Locations SCM) \/ {(IC SCM)}) by A13, AMI_3:4, RELAT_1:103, SCMFSA_2:7, XBOOLE_1:9
.= s2 | ((Data-Locations SCM) \/ {(IC SCM)}) by A2, A13, AMI_3:4, RELAT_1:103, SCMFSA_2:7, XBOOLE_1:9
.= (s2 | the carrier of SCM) | ((Data-Locations SCM) \/ {(IC SCM)}) by RELAT_1:103
.= ((s2 | the carrier of SCM) | ((Data-Locations SCM) \/ {(IC SCM)})) +* {} by FUNCT_4:22
.= S2 | ((Data-Locations SCM) \/ {(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)) | ((Data-Locations SCM) \/ {(IC SCM)}) by AMI_3:4, 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)) | ((Data-Locations SCM) \/ {(IC SCM)}) by AMI_3:4, 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)) | ((Data-Locations SCM) \/ {(IC SCM)})) by A20, FUNCT_4:75
.= (s2 | ((Int-Locations \/ FinSeq-Locations) \/ {(IC SCM+FSA)})) +* ((Exec (I,S2)) | ((Data-Locations SCM) \/ {(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;