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

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

end;

suppose InsCode l = 1 ; :: thesis: (Exec l,s1) | (SCM-Data-Loc \/ {(IC SCM )}) = (Exec l,s2) | (SCM-Data-Loc \/ {(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 SCM-Data-Loc \ {da} holds
((Exec l,s1) | (SCM-Data-Loc \ {da})) . x = ((Exec l,s2) | (SCM-Data-Loc \ {da})) . x

proof

let x be set ; :: thesis: ( x in SCM-Data-Loc \ {da} implies ((Exec l,s1) | (SCM-Data-Loc \ {da})) . x = ((Exec l,s2) | (SCM-Data-Loc \ {da})) . x )
assume A11: x in SCM-Data-Loc \ {da} ; :: thesis: ((Exec l,s1) | (SCM-Data-Loc \ {da})) . x = ((Exec l,s2) | (SCM-Data-Loc \ {da})) . x
then A12: x in SCM-Data-Loc by XBOOLE_0:def 5;
then reconsider a = x as Data-Location by AMI_3:def 2;
A13: a in SCM-Data-Loc \/ {(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) | (SCM-Data-Loc \ {da})) . x = (Exec l,s1) . a by A11, FUNCT_1:72
.= s1 . a by A9, A14, AMI_3:8
.= (s1 | (SCM-Data-Loc \/ {(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) | (SCM-Data-Loc \ {da})) . x by A11, FUNCT_1:72 ; :: thesis: verum

end;

( dom ((Exec l,s1) | (SCM-Data-Loc \ {da})) = SCM-Data-Loc \ {da} & dom ((Exec l,s2) | (SCM-Data-Loc \ {da})) = SCM-Data-Loc \ {da} ) by A6, RELAT_1:91;
then A15: (Exec l,s1) | (SCM-Data-Loc \ {da}) = (Exec l,s2) | (SCM-Data-Loc \ {da}) by A10, FUNCT_1:9;
A16: db in SCM-Data-Loc by 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 SCM-Data-Loc by AMI_3:def 2;
then A18: SCM-Data-Loc = SCM-Data-Loc \/ {da} by ZFMISC_1:46
.= (SCM-Data-Loc \ {da}) \/ {da} by XBOOLE_1:39 ;
(Exec l,s1) . da = s1 . db by A9, AMI_3:8
.= (s1 | (SCM-Data-Loc \/ {(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, AMI_3:72, RELAT_1:185;
hence (Exec l,s1) | (SCM-Data-Loc \/ {(IC SCM )}) = (Exec l,s2) | (SCM-Data-Loc \/ {(IC SCM )}) by A17, AMI_3:72, RELAT_1:185; :: thesis: verum

end;

suppose InsCode l = 2 ; :: thesis: (Exec l,s1) | (SCM-Data-Loc \/ {(IC SCM )}) = (Exec l,s2) | (SCM-Data-Loc \/ {(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 SCM-Data-Loc \ {da} holds
((Exec l,s1) | (SCM-Data-Loc \ {da})) . x = ((Exec l,s2) | (SCM-Data-Loc \ {da})) . x

proof

let x be set ; :: thesis: ( x in SCM-Data-Loc \ {da} implies ((Exec l,s1) | (SCM-Data-Loc \ {da})) . x = ((Exec l,s2) | (SCM-Data-Loc \ {da})) . x )
assume A21: x in SCM-Data-Loc \ {da} ; :: thesis: ((Exec l,s1) | (SCM-Data-Loc \ {da})) . x = ((Exec l,s2) | (SCM-Data-Loc \ {da})) . x
then A22: x in SCM-Data-Loc by XBOOLE_0:def 5;
then reconsider a = x as Data-Location by AMI_3:def 2;
A23: a in SCM-Data-Loc \/ {(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) | (SCM-Data-Loc \ {da})) . x = (Exec l,s1) . a by A21, FUNCT_1:72
.= s1 . a by A19, A24, AMI_3:9
.= (s1 | (SCM-Data-Loc \/ {(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) | (SCM-Data-Loc \ {da})) . x by A21, FUNCT_1:72 ; :: thesis: verum

end;

( dom ((Exec l,s1) | (SCM-Data-Loc \ {da})) = SCM-Data-Loc \ {da} & dom ((Exec l,s2) | (SCM-Data-Loc \ {da})) = SCM-Data-Loc \ {da} ) by A6, RELAT_1:91;
then A25: (Exec l,s1) | (SCM-Data-Loc \ {da}) = (Exec l,s2) | (SCM-Data-Loc \ {da}) by A20, FUNCT_1:9;
da in SCM-Data-Loc by AMI_3:def 2;
then A26: SCM-Data-Loc = SCM-Data-Loc \/ {da} by ZFMISC_1:46
.= (SCM-Data-Loc \ {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 SCM-Data-Loc by AMI_3:def 2;
then A29: s1 . da = (s1 | (SCM-Data-Loc \/ {(IC SCM )})) . da by A7, FUNCT_1:72
.= s2 . da by A2, A7, A28, FUNCT_1:72 ;
A30: db in SCM-Data-Loc by AMI_3:def 2;
then A31: s1 . db = (s1 | (SCM-Data-Loc \/ {(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, AMI_3:72, RELAT_1:185;
hence (Exec l,s1) | (SCM-Data-Loc \/ {(IC SCM )}) = (Exec l,s2) | (SCM-Data-Loc \/ {(IC SCM )}) by A27, AMI_3:72, RELAT_1:185; :: thesis: verum

end;

suppose InsCode l = 3 ; :: thesis: (Exec l,s1) | (SCM-Data-Loc \/ {(IC SCM )}) = (Exec l,s2) | (SCM-Data-Loc \/ {(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 SCM-Data-Loc \ {da} holds
((Exec l,s1) | (SCM-Data-Loc \ {da})) . x = ((Exec l,s2) | (SCM-Data-Loc \ {da})) . x

proof

let x be set ; :: thesis: ( x in SCM-Data-Loc \ {da} implies ((Exec l,s1) | (SCM-Data-Loc \ {da})) . x = ((Exec l,s2) | (SCM-Data-Loc \ {da})) . x )
assume A34: x in SCM-Data-Loc \ {da} ; :: thesis: ((Exec l,s1) | (SCM-Data-Loc \ {da})) . x = ((Exec l,s2) | (SCM-Data-Loc \ {da})) . x
then A35: x in SCM-Data-Loc by XBOOLE_0:def 5;
then reconsider a = x as Data-Location by AMI_3:def 2;
A36: a in SCM-Data-Loc \/ {(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) | (SCM-Data-Loc \ {da})) . x = (Exec l,s1) . a by A34, FUNCT_1:72
.= s1 . a by A32, A37, AMI_3:10
.= (s1 | (SCM-Data-Loc \/ {(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) | (SCM-Data-Loc \ {da})) . x by A34, FUNCT_1:72 ; :: thesis: verum

end;

( dom ((Exec l,s1) | (SCM-Data-Loc \ {da})) = SCM-Data-Loc \ {da} & dom ((Exec l,s2) | (SCM-Data-Loc \ {da})) = SCM-Data-Loc \ {da} ) by A6, RELAT_1:91;
then A38: (Exec l,s1) | (SCM-Data-Loc \ {da}) = (Exec l,s2) | (SCM-Data-Loc \ {da}) by A33, FUNCT_1:9;
da in SCM-Data-Loc by AMI_3:def 2;
then A39: SCM-Data-Loc = SCM-Data-Loc \/ {da} by ZFMISC_1:46
.= (SCM-Data-Loc \ {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 SCM-Data-Loc by AMI_3:def 2;
then A42: s1 . da = (s1 | (SCM-Data-Loc \/ {(IC SCM )})) . da by A7, FUNCT_1:72
.= s2 . da by A2, A7, A41, FUNCT_1:72 ;
A43: db in SCM-Data-Loc by AMI_3:def 2;
then A44: s1 . db = (s1 | (SCM-Data-Loc \/ {(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, AMI_3:72, RELAT_1:185;
hence (Exec l,s1) | (SCM-Data-Loc \/ {(IC SCM )}) = (Exec l,s2) | (SCM-Data-Loc \/ {(IC SCM )}) by A40, AMI_3:72, RELAT_1:185; :: thesis: verum

end;

suppose InsCode l = 4 ; :: thesis: (Exec l,s1) | (SCM-Data-Loc \/ {(IC SCM )}) = (Exec l,s2) | (SCM-Data-Loc \/ {(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 SCM-Data-Loc \ {da} holds
((Exec l,s1) | (SCM-Data-Loc \ {da})) . x = ((Exec l,s2) | (SCM-Data-Loc \ {da})) . x

proof

let x be set ; :: thesis: ( x in SCM-Data-Loc \ {da} implies ((Exec l,s1) | (SCM-Data-Loc \ {da})) . x = ((Exec l,s2) | (SCM-Data-Loc \ {da})) . x )
assume A47: x in SCM-Data-Loc \ {da} ; :: thesis: ((Exec l,s1) | (SCM-Data-Loc \ {da})) . x = ((Exec l,s2) | (SCM-Data-Loc \ {da})) . x
then A48: x in SCM-Data-Loc by XBOOLE_0:def 5;
then reconsider a = x as Data-Location by AMI_3:def 2;
A49: a in SCM-Data-Loc \/ {(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) | (SCM-Data-Loc \ {da})) . x = (Exec l,s1) . a by A47, FUNCT_1:72
.= s1 . a by A45, A50, AMI_3:11
.= (s1 | (SCM-Data-Loc \/ {(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) | (SCM-Data-Loc \ {da})) . x by A47, FUNCT_1:72 ; :: thesis: verum

end;

( dom ((Exec l,s1) | (SCM-Data-Loc \ {da})) = SCM-Data-Loc \ {da} & dom ((Exec l,s2) | (SCM-Data-Loc \ {da})) = SCM-Data-Loc \ {da} ) by A6, RELAT_1:91;
then A51: (Exec l,s1) | (SCM-Data-Loc \ {da}) = (Exec l,s2) | (SCM-Data-Loc \ {da}) by A46, FUNCT_1:9;
da in SCM-Data-Loc by AMI_3:def 2;
then A52: SCM-Data-Loc = SCM-Data-Loc \/ {da} by ZFMISC_1:46
.= (SCM-Data-Loc \ {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 SCM-Data-Loc by AMI_3:def 2;
then A55: s1 . da = (s1 | (SCM-Data-Loc \/ {(IC SCM )})) . da by A7, FUNCT_1:72
.= s2 . da by A2, A7, A54, FUNCT_1:72 ;
A56: db in SCM-Data-Loc by AMI_3:def 2;
then A57: s1 . db = (s1 | (SCM-Data-Loc \/ {(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, AMI_3:72, RELAT_1:185;
hence (Exec l,s1) | (SCM-Data-Loc \/ {(IC SCM )}) = (Exec l,s2) | (SCM-Data-Loc \/ {(IC SCM )}) by A53, AMI_3:72, RELAT_1:185; :: thesis: verum

end;

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

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

proof

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

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

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

proof

let x be set ; :: thesis: ( x in SCM-Data-Loc \ {da} implies ((Exec l,s1) | (SCM-Data-Loc \ {da})) . x = ((Exec l,s2) | (SCM-Data-Loc \ {da})) . x )
assume A61: x in SCM-Data-Loc \ {da} ; :: thesis: ((Exec l,s1) | (SCM-Data-Loc \ {da})) . x = ((Exec l,s2) | (SCM-Data-Loc \ {da})) . x
then A62: x in SCM-Data-Loc by XBOOLE_0:def 5;
then reconsider a = x as Data-Location by AMI_3:def 2;
A63: a in SCM-Data-Loc \/ {(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) | (SCM-Data-Loc \ {da})) . x = (Exec l,s1) . a by A61, FUNCT_1:72
.= s1 . a by A58, A59, A64, AMI_3:12
.= (s1 | (SCM-Data-Loc \/ {(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) | (SCM-Data-Loc \ {da})) . x by A61, FUNCT_1:72 ; :: thesis: verum

end;

( dom ((Exec l,s1) | (SCM-Data-Loc \ {da})) = SCM-Data-Loc \ {da} & dom ((Exec l,s2) | (SCM-Data-Loc \ {da})) = SCM-Data-Loc \ {da} ) by A6, RELAT_1:91;
then A65: (Exec l,s1) | (SCM-Data-Loc \ {da}) = (Exec l,s2) | (SCM-Data-Loc \ {da}) by A60, FUNCT_1:9;
da in SCM-Data-Loc by AMI_3:def 2;
then A66: SCM-Data-Loc = SCM-Data-Loc \/ {da} by ZFMISC_1:46
.= (SCM-Data-Loc \ {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 SCM-Data-Loc by AMI_3:def 2;
then A69: s1 . da = (s1 | (SCM-Data-Loc \/ {(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, AMI_3:72, RELAT_1:185;
hence (Exec l,s1) | (SCM-Data-Loc \/ {(IC SCM )}) = (Exec l,s2) | (SCM-Data-Loc \/ {(IC SCM )}) by A67, AMI_3:72, RELAT_1:185; :: thesis: verum

end;

suppose A70: da <> db ; :: thesis: (Exec l,s1) | (SCM-Data-Loc \/ {(IC SCM )}) = (Exec l,s2) | (SCM-Data-Loc \/ {(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 SCM-Data-Loc by AMI_3:def 2;
then A73: s1 . db = (s1 | (SCM-Data-Loc \/ {(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 SCM-Data-Loc \ {da,db} holds
((Exec l,s1) | (SCM-Data-Loc \ {da,db})) . x = ((Exec l,s2) | (SCM-Data-Loc \ {da,db})) . x

proof

let x be set ; :: thesis: ( x in SCM-Data-Loc \ {da,db} implies ((Exec l,s1) | (SCM-Data-Loc \ {da,db})) . x = ((Exec l,s2) | (SCM-Data-Loc \ {da,db})) . x )
assume A75: x in SCM-Data-Loc \ {da,db} ; :: thesis: ((Exec l,s1) | (SCM-Data-Loc \ {da,db})) . x = ((Exec l,s2) | (SCM-Data-Loc \ {da,db})) . x
then A76: x in SCM-Data-Loc by XBOOLE_0:def 5;
then reconsider a = x as Data-Location by AMI_3:def 2;
A77: a in SCM-Data-Loc \/ {(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) | (SCM-Data-Loc \ {da,db})) . x = (Exec l,s1) . a by A75, FUNCT_1:72
.= s1 . a by A58, A78, AMI_3:12
.= (s1 | (SCM-Data-Loc \/ {(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) | (SCM-Data-Loc \ {da,db})) . x by A75, FUNCT_1:72 ; :: thesis: verum

end;

( dom ((Exec l,s1) | (SCM-Data-Loc \ {da,db})) = SCM-Data-Loc \ {da,db} & dom ((Exec l,s2) | (SCM-Data-Loc \ {da,db})) = SCM-Data-Loc \ {da,db} ) by A6, RELAT_1:91;
then A79: (Exec l,s1) | (SCM-Data-Loc \ {da,db}) = (Exec l,s2) | (SCM-Data-Loc \ {da,db}) by A74, FUNCT_1:9;
( da in SCM-Data-Loc & db in SCM-Data-Loc ) by AMI_3:def 2;
then A80: SCM-Data-Loc = SCM-Data-Loc \/ {da,db} by ZFMISC_1:48
.= (SCM-Data-Loc \ {da,db}) \/ {da,db} by XBOOLE_1:39 ;
A81: da in SCM-Data-Loc by AMI_3:def 2;
then A82: s1 . da = (s1 | (SCM-Data-Loc \/ {(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, AMI_3:72, RELAT_1:185;
hence (Exec l,s1) | (SCM-Data-Loc \/ {(IC SCM )}) = (Exec l,s2) | (SCM-Data-Loc \/ {(IC SCM )}) by A71, AMI_3:72, RELAT_1:185; :: thesis: verum

end;

end;

end;

end;

suppose InsCode l = 6 ; :: thesis: (Exec l,s1) | (SCM-Data-Loc \/ {(IC SCM )}) = (Exec l,s2) | (SCM-Data-Loc \/ {(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 SCM-Data-Loc holds
(DataPart (Exec l,s1)) . x = (DataPart (Exec l,s2)) . x

proof

let x be set ; :: thesis: ( x in SCM-Data-Loc implies (DataPart (Exec l,s1)) . x = (DataPart (Exec l,s2)) . x )
assume A86: x in SCM-Data-Loc ; :: thesis: (DataPart (Exec l,s1)) . x = (DataPart (Exec l,s2)) . x
then reconsider a = x as Data-Location by AMI_3:def 2;
A87: a in SCM-Data-Loc \/ {(IC SCM )} by A86, XBOOLE_0:def 3;
thus (DataPart (Exec l,s1)) . x = (Exec l,s1) . a by A86, AMI_3:72, FUNCT_1:72
.= s1 . a by A84, AMI_3:13
.= (s1 | (SCM-Data-Loc \/ {(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, AMI_3:72, 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)) = SCM-Data-Loc & dom (DataPart (Exec l,s2)) = SCM-Data-Loc ) by A6, AMI_3:72, RELAT_1:91;
then (Exec l,s1) | SCM-Data-Loc = (Exec l,s2) | SCM-Data-Loc by A85, AMI_3:72, FUNCT_1:9;
hence (Exec l,s1) | (SCM-Data-Loc \/ {(IC SCM )}) = (Exec l,s2) | (SCM-Data-Loc \/ {(IC SCM )}) by A88, RELAT_1:185; :: thesis: verum

end;

suppose InsCode l = 7 ; :: thesis: (Exec l,s1) | (SCM-Data-Loc \/ {(IC SCM )}) = (Exec l,s2) | (SCM-Data-Loc \/ {(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 SCM-Data-Loc by AMI_3:def 2;
then A91: s1 . da = (s1 | (SCM-Data-Loc \/ {(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 SCM-Data-Loc holds
(DataPart (Exec l,s1)) . x = (DataPart (Exec l,s2)) . x

proof

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

end;

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

end;

suppose InsCode l = 8 ; :: thesis: (Exec l,s1) | (SCM-Data-Loc \/ {(IC SCM )}) = (Exec l,s2) | (SCM-Data-Loc \/ {(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 SCM-Data-Loc by AMI_3:def 2;
then A100: s1 . da = (s1 | (SCM-Data-Loc \/ {(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 SCM-Data-Loc holds
(DataPart (Exec l,s1)) . x = (DataPart (Exec l,s2)) . x

proof

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

end;

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

end;

end;