IC SCM in {(IC SCM)} by TARSKI:def 1;
then A1: IC SCM in (Data-Locations SCM) \/ {(IC SCM)} by XBOOLE_0:def 3;
let s1, s2 be State of SCM; :: thesis: ( s1 | ((Data-Locations SCM) \/ {(IC SCM)}) = s2 | ((Data-Locations SCM) \/ {(IC SCM)}) implies for l being Instruction of SCM holds (Exec (l,s1)) | ((Data-Locations SCM) \/ {(IC SCM)}) = (Exec (l,s2)) | ((Data-Locations SCM) \/ {(IC SCM)}) )
assume A2: s1 | ((Data-Locations SCM) \/ {(IC SCM)}) = s2 | ((Data-Locations SCM) \/ {(IC SCM)}) ; :: thesis: for l being Instruction of SCM holds (Exec (l,s1)) | ((Data-Locations SCM) \/ {(IC SCM)}) = (Exec (l,s2)) | ((Data-Locations SCM) \/ {(IC SCM)})
A3: (Data-Locations SCM) \/ {(IC SCM)} c= the carrier of SCM by AMI_3:4, AMI_3:72, XBOOLE_1:7;
then (Data-Locations SCM) \/ {(IC SCM)} c= dom s2 by PARTFUN1:def 4;
then A4: IC SCM in dom (s2 | ((Data-Locations SCM) \/ {(IC SCM)})) by A1, RELAT_1:91;
(Data-Locations SCM) \/ {(IC SCM)} c= dom s1 by A3, PARTFUN1:def 4;
then IC SCM in dom (s1 | ((Data-Locations SCM) \/ {(IC SCM)})) by A1, RELAT_1:91;
then A5: IC s1 = (s2 | ((Data-Locations SCM) \/ {(IC SCM)})) . (IC SCM) by A2, FUNCT_1:70
.= IC s2 by A4, FUNCT_1:70 ;
let l be Instruction of SCM; :: thesis: (Exec (l,s1)) | ((Data-Locations SCM) \/ {(IC SCM)}) = (Exec (l,s2)) | ((Data-Locations SCM) \/ {(IC SCM)})
A6: ( dom (Exec (l,s1)) = the carrier of SCM & dom (Exec (l,s2)) = the carrier of SCM ) by PARTFUN1:def 4;
A7: Data-Locations SCM c= (Data-Locations SCM) \/ {(IC SCM)} by XBOOLE_1:7;

per cases ( InsCode l = 0 or InsCode l = 1 or InsCode l = 2 or InsCode l = 3 or InsCode l = 4 or InsCode l = 5 or InsCode l = 6 or InsCode l = 7 or InsCode l = 8 ) by Th36, NAT_1:33;

suppose InsCode l = 0 ; :: thesis: (Exec (l,s1)) | ((Data-Locations SCM) \/ {(IC SCM)}) = (Exec (l,s2)) | ((Data-Locations SCM) \/ {(IC SCM)})

then A8: l = halt SCM by Th46;
hence (Exec (l,s1)) | ((Data-Locations SCM) \/ {(IC SCM)}) = s2 | ((Data-Locations SCM) \/ {(IC SCM)}) by A2, EXTPRO_1:def 3
.= (Exec (l,s2)) | ((Data-Locations SCM) \/ {(IC SCM)}) by A8, EXTPRO_1:def 3 ;
:: thesis: verum

end;

suppose InsCode l = 1 ; :: thesis: (Exec (l,s1)) | ((Data-Locations SCM) \/ {(IC SCM)}) = (Exec (l,s2)) | ((Data-Locations SCM) \/ {(IC SCM)})

then consider da, db being Data-Location such that
A9: l = da := db by Th47;
A10: for x being set st x in (Data-Locations SCM) \ {da} holds
((Exec (l,s1)) | ((Data-Locations SCM) \ {da})) . x = ((Exec (l,s2)) | ((Data-Locations SCM) \ {da})) . x

proof

let x be set ; :: thesis: ( x in (Data-Locations SCM) \ {da} implies ((Exec (l,s1)) | ((Data-Locations SCM) \ {da})) . x = ((Exec (l,s2)) | ((Data-Locations SCM) \ {da})) . x )
assume A11: x in (Data-Locations SCM) \ {da} ; :: thesis: ((Exec (l,s1)) | ((Data-Locations SCM) \ {da})) . x = ((Exec (l,s2)) | ((Data-Locations SCM) \ {da})) . x
then A12: x in Data-Locations SCM by XBOOLE_0:def 5;
then reconsider a = x as Data-Location by AMI_3:72, AMI_3:def 2;
A13: a in (Data-Locations SCM) \/ {(IC SCM)} by A12, XBOOLE_0:def 3;
not x in {da} by A11, XBOOLE_0:def 5;
then A14: a <> da by TARSKI:def 1;
thus ((Exec (l,s1)) | ((Data-Locations SCM) \ {da})) . x = (Exec (l,s1)) . a by A11, FUNCT_1:72
.= s1 . a by A9, A14, AMI_3:8
.= (s1 | ((Data-Locations SCM) \/ {(IC SCM)})) . a by A13, FUNCT_1:72
.= s2 . a by A2, A13, FUNCT_1:72
.= (Exec (l,s2)) . a by A9, A14, AMI_3:8
.= ((Exec (l,s2)) | ((Data-Locations SCM) \ {da})) . x by A11, FUNCT_1:72 ; :: thesis: verum

end;

( dom ((Exec (l,s1)) | ((Data-Locations SCM) \ {da})) = (Data-Locations SCM) \ {da} & dom ((Exec (l,s2)) | ((Data-Locations SCM) \ {da})) = (Data-Locations SCM) \ {da} ) by A6, RELAT_1:91;
then A15: (Exec (l,s1)) | ((Data-Locations SCM) \ {da}) = (Exec (l,s2)) | ((Data-Locations SCM) \ {da}) by A10, FUNCT_1:9;
A16: db in Data-Locations SCM by AMI_3:72, AMI_3:def 2;
(Exec (l,s1)) . (IC SCM) = succ (IC s1) by A9, AMI_3:8
.= (Exec (l,s2)) . (IC SCM) by A5, A9, AMI_3:8 ;
then A17: (Exec (l,s1)) | {(IC SCM)} = (Exec (l,s2)) | {(IC SCM)} by A6, GRFUNC_1:90;
da in Data-Locations SCM by AMI_3:72, AMI_3:def 2;
then A18: Data-Locations SCM = (Data-Locations SCM) \/ {da} by ZFMISC_1:46
.= ((Data-Locations SCM) \ {da}) \/ {da} by XBOOLE_1:39 ;
(Exec (l,s1)) . da = s1 . db by A9, AMI_3:8
.= (s1 | ((Data-Locations SCM) \/ {(IC SCM)})) . db by A7, A16, FUNCT_1:72
.= s2 . db by A2, A7, A16, FUNCT_1:72
.= (Exec (l,s2)) . da by A9, AMI_3:8 ;
then (Exec (l,s1)) | {da} = (Exec (l,s2)) | {da} by A6, GRFUNC_1:90;
then DataPart (Exec (l,s1)) = DataPart (Exec (l,s2)) by A18, A15, RELAT_1:185;
hence (Exec (l,s1)) | ((Data-Locations SCM) \/ {(IC SCM)}) = (Exec (l,s2)) | ((Data-Locations SCM) \/ {(IC SCM)}) by A17, RELAT_1:185; :: thesis: verum

end;

suppose InsCode l = 2 ; :: thesis: (Exec (l,s1)) | ((Data-Locations SCM) \/ {(IC SCM)}) = (Exec (l,s2)) | ((Data-Locations SCM) \/ {(IC SCM)})

then consider da, db being Data-Location such that
A19: l = AddTo (da,db) by Th48;
A20: for x being set st x in (Data-Locations SCM) \ {da} holds
((Exec (l,s1)) | ((Data-Locations SCM) \ {da})) . x = ((Exec (l,s2)) | ((Data-Locations SCM) \ {da})) . x

proof

let x be set ; :: thesis: ( x in (Data-Locations SCM) \ {da} implies ((Exec (l,s1)) | ((Data-Locations SCM) \ {da})) . x = ((Exec (l,s2)) | ((Data-Locations SCM) \ {da})) . x )
assume A21: x in (Data-Locations SCM) \ {da} ; :: thesis: ((Exec (l,s1)) | ((Data-Locations SCM) \ {da})) . x = ((Exec (l,s2)) | ((Data-Locations SCM) \ {da})) . x
then A22: x in Data-Locations SCM by XBOOLE_0:def 5;
then reconsider a = x as Data-Location by AMI_3:72, AMI_3:def 2;
A23: a in (Data-Locations SCM) \/ {(IC SCM)} by A22, XBOOLE_0:def 3;
not x in {da} by A21, XBOOLE_0:def 5;
then A24: a <> da by TARSKI:def 1;
thus ((Exec (l,s1)) | ((Data-Locations SCM) \ {da})) . x = (Exec (l,s1)) . a by A21, FUNCT_1:72
.= s1 . a by A19, A24, AMI_3:9
.= (s1 | ((Data-Locations SCM) \/ {(IC SCM)})) . a by A23, FUNCT_1:72
.= s2 . a by A2, A23, FUNCT_1:72
.= (Exec (l,s2)) . a by A19, A24, AMI_3:9
.= ((Exec (l,s2)) | ((Data-Locations SCM) \ {da})) . x by A21, FUNCT_1:72 ; :: thesis: verum

end;

( dom ((Exec (l,s1)) | ((Data-Locations SCM) \ {da})) = (Data-Locations SCM) \ {da} & dom ((Exec (l,s2)) | ((Data-Locations SCM) \ {da})) = (Data-Locations SCM) \ {da} ) by A6, RELAT_1:91;
then A25: (Exec (l,s1)) | ((Data-Locations SCM) \ {da}) = (Exec (l,s2)) | ((Data-Locations SCM) \ {da}) by A20, FUNCT_1:9;
da in Data-Locations SCM by AMI_3:72, AMI_3:def 2;
then A26: Data-Locations SCM = (Data-Locations SCM) \/ {da} by ZFMISC_1:46
.= ((Data-Locations SCM) \ {da}) \/ {da} by XBOOLE_1:39 ;
(Exec (l,s1)) . (IC SCM) = succ (IC s1) by A19, AMI_3:9
.= (Exec (l,s2)) . (IC SCM) by A5, A19, AMI_3:9 ;
then A27: (Exec (l,s1)) | {(IC SCM)} = (Exec (l,s2)) | {(IC SCM)} by A6, GRFUNC_1:90;
A28: da in Data-Locations SCM by AMI_3:72, AMI_3:def 2;
then A29: s1 . da = (s1 | ((Data-Locations SCM) \/ {(IC SCM)})) . da by A7, FUNCT_1:72
.= s2 . da by A2, A7, A28, FUNCT_1:72 ;
A30: db in Data-Locations SCM by AMI_3:72, AMI_3:def 2;
then A31: s1 . db = (s1 | ((Data-Locations SCM) \/ {(IC SCM)})) . db by A7, FUNCT_1:72
.= s2 . db by A2, A7, A30, FUNCT_1:72 ;
(Exec (l,s1)) . da = (s1 . da) + (s1 . db) by A19, AMI_3:9
.= (Exec (l,s2)) . da by A19, A29, A31, AMI_3:9 ;
then (Exec (l,s1)) | {da} = (Exec (l,s2)) | {da} by A6, GRFUNC_1:90;
then DataPart (Exec (l,s1)) = DataPart (Exec (l,s2)) by A26, A25, RELAT_1:185;
hence (Exec (l,s1)) | ((Data-Locations SCM) \/ {(IC SCM)}) = (Exec (l,s2)) | ((Data-Locations SCM) \/ {(IC SCM)}) by A27, RELAT_1:185; :: thesis: verum

end;

suppose InsCode l = 3 ; :: thesis: (Exec (l,s1)) | ((Data-Locations SCM) \/ {(IC SCM)}) = (Exec (l,s2)) | ((Data-Locations SCM) \/ {(IC SCM)})

then consider da, db being Data-Location such that
A32: l = SubFrom (da,db) by Th49;
A33: for x being set st x in (Data-Locations SCM) \ {da} holds
((Exec (l,s1)) | ((Data-Locations SCM) \ {da})) . x = ((Exec (l,s2)) | ((Data-Locations SCM) \ {da})) . x

proof

let x be set ; :: thesis: ( x in (Data-Locations SCM) \ {da} implies ((Exec (l,s1)) | ((Data-Locations SCM) \ {da})) . x = ((Exec (l,s2)) | ((Data-Locations SCM) \ {da})) . x )
assume A34: x in (Data-Locations SCM) \ {da} ; :: thesis: ((Exec (l,s1)) | ((Data-Locations SCM) \ {da})) . x = ((Exec (l,s2)) | ((Data-Locations SCM) \ {da})) . x
then A35: x in Data-Locations SCM by XBOOLE_0:def 5;
then reconsider a = x as Data-Location by AMI_3:72, AMI_3:def 2;
A36: a in (Data-Locations SCM) \/ {(IC SCM)} by A35, XBOOLE_0:def 3;
not x in {da} by A34, XBOOLE_0:def 5;
then A37: a <> da by TARSKI:def 1;
thus ((Exec (l,s1)) | ((Data-Locations SCM) \ {da})) . x = (Exec (l,s1)) . a by A34, FUNCT_1:72
.= s1 . a by A32, A37, AMI_3:10
.= (s1 | ((Data-Locations SCM) \/ {(IC SCM)})) . a by A36, FUNCT_1:72
.= s2 . a by A2, A36, FUNCT_1:72
.= (Exec (l,s2)) . a by A32, A37, AMI_3:10
.= ((Exec (l,s2)) | ((Data-Locations SCM) \ {da})) . x by A34, FUNCT_1:72 ; :: thesis: verum

end;

( dom ((Exec (l,s1)) | ((Data-Locations SCM) \ {da})) = (Data-Locations SCM) \ {da} & dom ((Exec (l,s2)) | ((Data-Locations SCM) \ {da})) = (Data-Locations SCM) \ {da} ) by A6, RELAT_1:91;
then A38: (Exec (l,s1)) | ((Data-Locations SCM) \ {da}) = (Exec (l,s2)) | ((Data-Locations SCM) \ {da}) by A33, FUNCT_1:9;
da in Data-Locations SCM by AMI_3:72, AMI_3:def 2;
then A39: Data-Locations SCM = (Data-Locations SCM) \/ {da} by ZFMISC_1:46
.= ((Data-Locations SCM) \ {da}) \/ {da} by XBOOLE_1:39 ;
(Exec (l,s1)) . (IC SCM) = succ (IC s1) by A32, AMI_3:10
.= (Exec (l,s2)) . (IC SCM) by A5, A32, AMI_3:10 ;
then A40: (Exec (l,s1)) | {(IC SCM)} = (Exec (l,s2)) | {(IC SCM)} by A6, GRFUNC_1:90;
A41: da in Data-Locations SCM by AMI_3:72, AMI_3:def 2;
then A42: s1 . da = (s1 | ((Data-Locations SCM) \/ {(IC SCM)})) . da by A7, FUNCT_1:72
.= s2 . da by A2, A7, A41, FUNCT_1:72 ;
A43: db in Data-Locations SCM by AMI_3:72, AMI_3:def 2;
then A44: s1 . db = (s1 | ((Data-Locations SCM) \/ {(IC SCM)})) . db by A7, FUNCT_1:72
.= s2 . db by A2, A7, A43, FUNCT_1:72 ;
(Exec (l,s1)) . da = (s1 . da) - (s1 . db) by A32, AMI_3:10
.= (Exec (l,s2)) . da by A32, A42, A44, AMI_3:10 ;
then (Exec (l,s1)) | {da} = (Exec (l,s2)) | {da} by A6, GRFUNC_1:90;
then DataPart (Exec (l,s1)) = DataPart (Exec (l,s2)) by A39, A38, RELAT_1:185;
hence (Exec (l,s1)) | ((Data-Locations SCM) \/ {(IC SCM)}) = (Exec (l,s2)) | ((Data-Locations SCM) \/ {(IC SCM)}) by A40, RELAT_1:185; :: thesis: verum

end;

suppose InsCode l = 4 ; :: thesis: (Exec (l,s1)) | ((Data-Locations SCM) \/ {(IC SCM)}) = (Exec (l,s2)) | ((Data-Locations SCM) \/ {(IC SCM)})

then consider da, db being Data-Location such that
A45: l = MultBy (da,db) by Th50;
A46: for x being set st x in (Data-Locations SCM) \ {da} holds
((Exec (l,s1)) | ((Data-Locations SCM) \ {da})) . x = ((Exec (l,s2)) | ((Data-Locations SCM) \ {da})) . x

proof

let x be set ; :: thesis: ( x in (Data-Locations SCM) \ {da} implies ((Exec (l,s1)) | ((Data-Locations SCM) \ {da})) . x = ((Exec (l,s2)) | ((Data-Locations SCM) \ {da})) . x )
assume A47: x in (Data-Locations SCM) \ {da} ; :: thesis: ((Exec (l,s1)) | ((Data-Locations SCM) \ {da})) . x = ((Exec (l,s2)) | ((Data-Locations SCM) \ {da})) . x
then A48: x in Data-Locations SCM by XBOOLE_0:def 5;
then reconsider a = x as Data-Location by AMI_3:72, AMI_3:def 2;
A49: a in (Data-Locations SCM) \/ {(IC SCM)} by A48, XBOOLE_0:def 3;
not x in {da} by A47, XBOOLE_0:def 5;
then A50: a <> da by TARSKI:def 1;
thus ((Exec (l,s1)) | ((Data-Locations SCM) \ {da})) . x = (Exec (l,s1)) . a by A47, FUNCT_1:72
.= s1 . a by A45, A50, AMI_3:11
.= (s1 | ((Data-Locations SCM) \/ {(IC SCM)})) . a by A49, FUNCT_1:72
.= s2 . a by A2, A49, FUNCT_1:72
.= (Exec (l,s2)) . a by A45, A50, AMI_3:11
.= ((Exec (l,s2)) | ((Data-Locations SCM) \ {da})) . x by A47, FUNCT_1:72 ; :: thesis: verum

end;

( dom ((Exec (l,s1)) | ((Data-Locations SCM) \ {da})) = (Data-Locations SCM) \ {da} & dom ((Exec (l,s2)) | ((Data-Locations SCM) \ {da})) = (Data-Locations SCM) \ {da} ) by A6, RELAT_1:91;
then A51: (Exec (l,s1)) | ((Data-Locations SCM) \ {da}) = (Exec (l,s2)) | ((Data-Locations SCM) \ {da}) by A46, FUNCT_1:9;
da in Data-Locations SCM by AMI_3:72, AMI_3:def 2;
then A52: Data-Locations SCM = (Data-Locations SCM) \/ {da} by ZFMISC_1:46
.= ((Data-Locations SCM) \ {da}) \/ {da} by XBOOLE_1:39 ;
(Exec (l,s1)) . (IC SCM) = succ (IC s1) by A45, AMI_3:11
.= (Exec (l,s2)) . (IC SCM) by A5, A45, AMI_3:11 ;
then A53: (Exec (l,s1)) | {(IC SCM)} = (Exec (l,s2)) | {(IC SCM)} by A6, GRFUNC_1:90;
A54: da in Data-Locations SCM by AMI_3:72, AMI_3:def 2;
then A55: s1 . da = (s1 | ((Data-Locations SCM) \/ {(IC SCM)})) . da by A7, FUNCT_1:72
.= s2 . da by A2, A7, A54, FUNCT_1:72 ;
A56: db in Data-Locations SCM by AMI_3:72, AMI_3:def 2;
then A57: s1 . db = (s1 | ((Data-Locations SCM) \/ {(IC SCM)})) . db by A7, FUNCT_1:72
.= s2 . db by A2, A7, A56, FUNCT_1:72 ;
(Exec (l,s1)) . da = (s1 . da) * (s1 . db) by A45, AMI_3:11
.= (Exec (l,s2)) . da by A45, A55, A57, AMI_3:11 ;
then (Exec (l,s1)) | {da} = (Exec (l,s2)) | {da} by A6, GRFUNC_1:90;
then DataPart (Exec (l,s1)) = DataPart (Exec (l,s2)) by A52, A51, RELAT_1:185;
hence (Exec (l,s1)) | ((Data-Locations SCM) \/ {(IC SCM)}) = (Exec (l,s2)) | ((Data-Locations SCM) \/ {(IC SCM)}) by A53, RELAT_1:185; :: thesis: verum

end;

suppose InsCode l = 5 ; :: thesis: (Exec (l,s1)) | ((Data-Locations SCM) \/ {(IC SCM)}) = (Exec (l,s2)) | ((Data-Locations SCM) \/ {(IC SCM)})

then consider da, db being Data-Location such that
A58: l = Divide (da,db) by Th51;
thus (Exec (l,s1)) | ((Data-Locations SCM) \/ {(IC SCM)}) = (Exec (l,s2)) | ((Data-Locations SCM) \/ {(IC SCM)}) :: thesis: verum

proof

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

suppose A59: da = db ; :: thesis: (Exec (l,s1)) | ((Data-Locations SCM) \/ {(IC SCM)}) = (Exec (l,s2)) | ((Data-Locations SCM) \/ {(IC SCM)})

A60: for x being set st x in (Data-Locations SCM) \ {da} holds
((Exec (l,s1)) | ((Data-Locations SCM) \ {da})) . x = ((Exec (l,s2)) | ((Data-Locations SCM) \ {da})) . x

proof

let x be set ; :: thesis: ( x in (Data-Locations SCM) \ {da} implies ((Exec (l,s1)) | ((Data-Locations SCM) \ {da})) . x = ((Exec (l,s2)) | ((Data-Locations SCM) \ {da})) . x )
assume A61: x in (Data-Locations SCM) \ {da} ; :: thesis: ((Exec (l,s1)) | ((Data-Locations SCM) \ {da})) . x = ((Exec (l,s2)) | ((Data-Locations SCM) \ {da})) . x
then A62: x in Data-Locations SCM by XBOOLE_0:def 5;
then reconsider a = x as Data-Location by AMI_3:72, AMI_3:def 2;
A63: a in (Data-Locations SCM) \/ {(IC SCM)} by A62, XBOOLE_0:def 3;
not x in {da} by A61, XBOOLE_0:def 5;
then A64: a <> da by TARSKI:def 1;
thus ((Exec (l,s1)) | ((Data-Locations SCM) \ {da})) . x = (Exec (l,s1)) . a by A61, FUNCT_1:72
.= s1 . a by A58, A59, A64, AMI_3:12
.= (s1 | ((Data-Locations SCM) \/ {(IC SCM)})) . a by A63, FUNCT_1:72
.= s2 . a by A2, A63, FUNCT_1:72
.= (Exec (l,s2)) . a by A58, A59, A64, AMI_3:12
.= ((Exec (l,s2)) | ((Data-Locations SCM) \ {da})) . x by A61, FUNCT_1:72 ; :: thesis: verum

end;

( dom ((Exec (l,s1)) | ((Data-Locations SCM) \ {da})) = (Data-Locations SCM) \ {da} & dom ((Exec (l,s2)) | ((Data-Locations SCM) \ {da})) = (Data-Locations SCM) \ {da} ) by A6, RELAT_1:91;
then A65: (Exec (l,s1)) | ((Data-Locations SCM) \ {da}) = (Exec (l,s2)) | ((Data-Locations SCM) \ {da}) by A60, FUNCT_1:9;
da in Data-Locations SCM by AMI_3:72, AMI_3:def 2;
then A66: Data-Locations SCM = (Data-Locations SCM) \/ {da} by ZFMISC_1:46
.= ((Data-Locations SCM) \ {da}) \/ {da} by XBOOLE_1:39 ;
(Exec (l,s1)) . (IC SCM) = succ (IC s1) by A58, AMI_3:12
.= (Exec (l,s2)) . (IC SCM) by A5, A58, AMI_3:12 ;
then A67: (Exec (l,s1)) | {(IC SCM)} = (Exec (l,s2)) | {(IC SCM)} by A6, GRFUNC_1:90;
A68: da in Data-Locations SCM by AMI_3:72, AMI_3:def 2;
then A69: s1 . da = (s1 | ((Data-Locations SCM) \/ {(IC SCM)})) . da by A7, FUNCT_1:72
.= s2 . da by A2, A7, A68, FUNCT_1:72 ;
(Exec (l,s1)) . da = (s1 . da) mod (s1 . da) by A58, A59, AMI_3:12
.= (Exec (l,s2)) . da by A58, A59, A69, AMI_3:12 ;
then (Exec (l,s1)) | {da} = (Exec (l,s2)) | {da} by A6, GRFUNC_1:90;
then DataPart (Exec (l,s1)) = DataPart (Exec (l,s2)) by A66, A65, RELAT_1:185;
hence (Exec (l,s1)) | ((Data-Locations SCM) \/ {(IC SCM)}) = (Exec (l,s2)) | ((Data-Locations SCM) \/ {(IC SCM)}) by A67, RELAT_1:185; :: thesis: verum

end;

suppose A70: da <> db ; :: thesis: (Exec (l,s1)) | ((Data-Locations SCM) \/ {(IC SCM)}) = (Exec (l,s2)) | ((Data-Locations SCM) \/ {(IC SCM)})

(Exec (l,s1)) . (IC SCM) = succ (IC s1) by A58, AMI_3:12
.= (Exec (l,s2)) . (IC SCM) by A5, A58, AMI_3:12 ;
then A71: (Exec (l,s1)) | {(IC SCM)} = (Exec (l,s2)) | {(IC SCM)} by A6, GRFUNC_1:90;
A72: db in Data-Locations SCM by AMI_3:72, AMI_3:def 2;
then A73: s1 . db = (s1 | ((Data-Locations SCM) \/ {(IC SCM)})) . db by A7, FUNCT_1:72
.= s2 . db by A2, A7, A72, FUNCT_1:72 ;
A74: for x being set st x in (Data-Locations SCM) \ {da,db} holds
((Exec (l,s1)) | ((Data-Locations SCM) \ {da,db})) . x = ((Exec (l,s2)) | ((Data-Locations SCM) \ {da,db})) . x

proof

let x be set ; :: thesis: ( x in (Data-Locations SCM) \ {da,db} implies ((Exec (l,s1)) | ((Data-Locations SCM) \ {da,db})) . x = ((Exec (l,s2)) | ((Data-Locations SCM) \ {da,db})) . x )
assume A75: x in (Data-Locations SCM) \ {da,db} ; :: thesis: ((Exec (l,s1)) | ((Data-Locations SCM) \ {da,db})) . x = ((Exec (l,s2)) | ((Data-Locations SCM) \ {da,db})) . x
then A76: x in Data-Locations SCM by XBOOLE_0:def 5;
then reconsider a = x as Data-Location by AMI_3:72, AMI_3:def 2;
A77: a in (Data-Locations SCM) \/ {(IC SCM)} by A76, XBOOLE_0:def 3;
not x in {da,db} by A75, XBOOLE_0:def 5;
then A78: ( a <> da & a <> db ) by TARSKI:def 2;
thus ((Exec (l,s1)) | ((Data-Locations SCM) \ {da,db})) . x = (Exec (l,s1)) . a by A75, FUNCT_1:72
.= s1 . a by A58, A78, AMI_3:12
.= (s1 | ((Data-Locations SCM) \/ {(IC SCM)})) . a by A77, FUNCT_1:72
.= s2 . a by A2, A77, FUNCT_1:72
.= (Exec (l,s2)) . a by A58, A78, AMI_3:12
.= ((Exec (l,s2)) | ((Data-Locations SCM) \ {da,db})) . x by A75, FUNCT_1:72 ; :: thesis: verum

end;

( dom ((Exec (l,s1)) | ((Data-Locations SCM) \ {da,db})) = (Data-Locations SCM) \ {da,db} & dom ((Exec (l,s2)) | ((Data-Locations SCM) \ {da,db})) = (Data-Locations SCM) \ {da,db} ) by A6, RELAT_1:91;
then A79: (Exec (l,s1)) | ((Data-Locations SCM) \ {da,db}) = (Exec (l,s2)) | ((Data-Locations SCM) \ {da,db}) by A74, FUNCT_1:9;
( da in Data-Locations SCM & db in Data-Locations SCM ) by AMI_3:72, AMI_3:def 2;
then A80: Data-Locations SCM = (Data-Locations SCM) \/ {da,db} by ZFMISC_1:48
.= ((Data-Locations SCM) \ {da,db}) \/ {da,db} by XBOOLE_1:39 ;
A81: da in Data-Locations SCM by AMI_3:72, AMI_3:def 2;
then A82: s1 . da = (s1 | ((Data-Locations SCM) \/ {(IC SCM)})) . da by A7, FUNCT_1:72
.= s2 . da by A2, A7, A81, FUNCT_1:72 ;
A83: (Exec (l,s1)) . db = (s1 . da) mod (s1 . db) by A58, AMI_3:12
.= (Exec (l,s2)) . db by A58, A82, A73, AMI_3:12 ;
(Exec (l,s1)) . da = (s1 . da) div (s1 . db) by A58, A70, AMI_3:12
.= (Exec (l,s2)) . da by A58, A70, A82, A73, AMI_3:12 ;
then (Exec (l,s1)) | {da,db} = (Exec (l,s2)) | {da,db} by A6, A83, GRFUNC_1:91;
then DataPart (Exec (l,s1)) = DataPart (Exec (l,s2)) by A80, A79, RELAT_1:185;
hence (Exec (l,s1)) | ((Data-Locations SCM) \/ {(IC SCM)}) = (Exec (l,s2)) | ((Data-Locations SCM) \/ {(IC SCM)}) by A71, RELAT_1:185; :: thesis: verum

end;

end;

end;

end;

suppose InsCode l = 6 ; :: thesis: (Exec (l,s1)) | ((Data-Locations SCM) \/ {(IC SCM)}) = (Exec (l,s2)) | ((Data-Locations SCM) \/ {(IC SCM)})

then consider loc being Element of NAT such that
A84: l = SCM-goto loc by Th52;
A85: for x being set st x in Data-Locations SCM holds
(DataPart (Exec (l,s1))) . x = (DataPart (Exec (l,s2))) . x

proof

let x be set ; :: thesis: ( x in Data-Locations SCM implies (DataPart (Exec (l,s1))) . x = (DataPart (Exec (l,s2))) . x )
assume A86: x in Data-Locations SCM ; :: thesis: (DataPart (Exec (l,s1))) . x = (DataPart (Exec (l,s2))) . x
then reconsider a = x as Data-Location by AMI_3:72, AMI_3:def 2;
A87: a in (Data-Locations SCM) \/ {(IC SCM)} by A86, XBOOLE_0:def 3;
thus (DataPart (Exec (l,s1))) . x = (Exec (l,s1)) . a by A86, FUNCT_1:72
.= s1 . a by A84, AMI_3:13
.= (s1 | ((Data-Locations SCM) \/ {(IC SCM)})) . a by A87, FUNCT_1:72
.= s2 . a by A2, A87, FUNCT_1:72
.= (Exec (l,s2)) . a by A84, AMI_3:13
.= (DataPart (Exec (l,s2))) . x by A86, FUNCT_1:72 ; :: thesis: verum

end;

(Exec (l,s1)) . (IC SCM) = loc by A84, AMI_3:13
.= (Exec (l,s2)) . (IC SCM) by A84, AMI_3:13 ;
then A88: (Exec (l,s1)) | {(IC SCM)} = (Exec (l,s2)) | {(IC SCM)} by A6, GRFUNC_1:90;
( dom (DataPart (Exec (l,s1))) = Data-Locations SCM & dom (DataPart (Exec (l,s2))) = Data-Locations SCM ) by A6, RELAT_1:91;
then (Exec (l,s1)) | (Data-Locations SCM) = (Exec (l,s2)) | (Data-Locations SCM) by A85, FUNCT_1:9;
hence (Exec (l,s1)) | ((Data-Locations SCM) \/ {(IC SCM)}) = (Exec (l,s2)) | ((Data-Locations SCM) \/ {(IC SCM)}) by A88, RELAT_1:185; :: thesis: verum

end;

suppose InsCode l = 7 ; :: thesis: (Exec (l,s1)) | ((Data-Locations SCM) \/ {(IC SCM)}) = (Exec (l,s2)) | ((Data-Locations SCM) \/ {(IC SCM)})

then consider loc being Element of NAT , da being Data-Location such that
A89: l = da =0_goto loc by Th53;
(Exec (l,s1)) . (IC SCM) = (Exec (l,s2)) . (IC SCM)

proof

A90: da in Data-Locations SCM by AMI_3:72, AMI_3:def 2;
then A91: s1 . da = (s1 | ((Data-Locations SCM) \/ {(IC SCM)})) . da by A7, FUNCT_1:72
.= s2 . da by A2, A7, A90, FUNCT_1:72 ;

per cases ( s1 . da = 0 or s1 . da <> 0 ) ;

suppose A92: s1 . da = 0 ; :: thesis: (Exec (l,s1)) . (IC SCM) = (Exec (l,s2)) . (IC SCM)

hence (Exec (l,s1)) . (IC SCM) = loc by A89, AMI_3:14
.= (Exec (l,s2)) . (IC SCM) by A89, A91, A92, AMI_3:14 ;
:: thesis: verum

end;

suppose A93: s1 . da <> 0 ; :: thesis: (Exec (l,s1)) . (IC SCM) = (Exec (l,s2)) . (IC SCM)

hence (Exec (l,s1)) . (IC SCM) = succ (IC s1) by A89, AMI_3:14
.= (Exec (l,s2)) . (IC SCM) by A5, A89, A91, A93, AMI_3:14 ;
:: thesis: verum

end;

end;

end;

then A94: (Exec (l,s1)) | {(IC SCM)} = (Exec (l,s2)) | {(IC SCM)} by A6, GRFUNC_1:90;
A95: for x being set st x in Data-Locations SCM holds
(DataPart (Exec (l,s1))) . x = (DataPart (Exec (l,s2))) . x

proof

let x be set ; :: thesis: ( x in Data-Locations SCM implies (DataPart (Exec (l,s1))) . x = (DataPart (Exec (l,s2))) . x )
assume A96: x in Data-Locations SCM ; :: thesis: (DataPart (Exec (l,s1))) . x = (DataPart (Exec (l,s2))) . x
then reconsider a = x as Data-Location by AMI_3:72, AMI_3:def 2;
A97: a in (Data-Locations SCM) \/ {(IC SCM)} by A96, XBOOLE_0:def 3;
thus (DataPart (Exec (l,s1))) . x = (Exec (l,s1)) . a by A96, FUNCT_1:72
.= s1 . a by A89, AMI_3:14
.= (s1 | ((Data-Locations SCM) \/ {(IC SCM)})) . a by A97, FUNCT_1:72
.= s2 . a by A2, A97, FUNCT_1:72
.= (Exec (l,s2)) . a by A89, AMI_3:14
.= (DataPart (Exec (l,s2))) . x by A96, FUNCT_1:72 ; :: thesis: verum

end;

( dom (DataPart (Exec (l,s1))) = Data-Locations SCM & dom (DataPart (Exec (l,s2))) = Data-Locations SCM ) by A6, RELAT_1:91;
then (Exec (l,s1)) | (Data-Locations SCM) = (Exec (l,s2)) | (Data-Locations SCM) by A95, FUNCT_1:9;
hence (Exec (l,s1)) | ((Data-Locations SCM) \/ {(IC SCM)}) = (Exec (l,s2)) | ((Data-Locations SCM) \/ {(IC SCM)}) by A94, RELAT_1:185; :: thesis: verum

end;

suppose InsCode l = 8 ; :: thesis: (Exec (l,s1)) | ((Data-Locations SCM) \/ {(IC SCM)}) = (Exec (l,s2)) | ((Data-Locations SCM) \/ {(IC SCM)})

then consider loc being Element of NAT , da being Data-Location such that
A98: l = da >0_goto loc by Th54;
(Exec (l,s1)) . (IC SCM) = (Exec (l,s2)) . (IC SCM)

proof

A99: da in Data-Locations SCM by AMI_3:72, AMI_3:def 2;
then A100: s1 . da = (s1 | ((Data-Locations SCM) \/ {(IC SCM)})) . da by A7, FUNCT_1:72
.= s2 . da by A2, A7, A99, FUNCT_1:72 ;

per cases ( s1 . da > 0 or s1 . da <= 0 ) ;

suppose A101: s1 . da > 0 ; :: thesis: (Exec (l,s1)) . (IC SCM) = (Exec (l,s2)) . (IC SCM)

hence (Exec (l,s1)) . (IC SCM) = loc by A98, AMI_3:15
.= (Exec (l,s2)) . (IC SCM) by A98, A100, A101, AMI_3:15 ;
:: thesis: verum

end;

suppose A102: s1 . da <= 0 ; :: thesis: (Exec (l,s1)) . (IC SCM) = (Exec (l,s2)) . (IC SCM)

hence (Exec (l,s1)) . (IC SCM) = succ (IC s1) by A98, AMI_3:15
.= (Exec (l,s2)) . (IC SCM) by A5, A98, A100, A102, AMI_3:15 ;
:: thesis: verum

end;

end;

end;

then A103: (Exec (l,s1)) | {(IC SCM)} = (Exec (l,s2)) | {(IC SCM)} by A6, GRFUNC_1:90;
A104: for x being set st x in Data-Locations SCM holds
(DataPart (Exec (l,s1))) . x = (DataPart (Exec (l,s2))) . x

proof

let x be set ; :: thesis: ( x in Data-Locations SCM implies (DataPart (Exec (l,s1))) . x = (DataPart (Exec (l,s2))) . x )
assume A105: x in Data-Locations SCM ; :: thesis: (DataPart (Exec (l,s1))) . x = (DataPart (Exec (l,s2))) . x
then reconsider a = x as Data-Location by AMI_3:72, AMI_3:def 2;
A106: a in (Data-Locations SCM) \/ {(IC SCM)} by A105, XBOOLE_0:def 3;
thus (DataPart (Exec (l,s1))) . x = (Exec (l,s1)) . a by A105, FUNCT_1:72
.= s1 . a by A98, AMI_3:15
.= (s1 | ((Data-Locations SCM) \/ {(IC SCM)})) . a by A106, FUNCT_1:72
.= s2 . a by A2, A106, FUNCT_1:72
.= (Exec (l,s2)) . a by A98, AMI_3:15
.= (DataPart (Exec (l,s2))) . x by A105, FUNCT_1:72 ; :: thesis: verum

end;

( dom (DataPart (Exec (l,s1))) = Data-Locations SCM & dom (DataPart (Exec (l,s2))) = Data-Locations SCM ) by A6, RELAT_1:91;
then (Exec (l,s1)) | (Data-Locations SCM) = (Exec (l,s2)) | (Data-Locations SCM) by A104, FUNCT_1:9;
hence (Exec (l,s1)) | ((Data-Locations SCM) \/ {(IC SCM)}) = (Exec (l,s2)) | ((Data-Locations SCM) \/ {(IC SCM)}) by A103, RELAT_1:185; :: thesis: verum

end;

end;