thus SCM is IC-good :: thesis: SCM is Exec-preserving

proof

let I be Instruction of SCM ; :: according to AMISTD_2:def 18 :: thesis: I is IC-good

per cases ( I = [0 ,{} ] or ex a, b being Data-Location st I = a := b or ex a, b being Data-Location st I = AddTo a,b or ex a, b being Data-Location st I = SubFrom a,b or ex a, b being Data-Location st I = MultBy a,b or ex a, b being Data-Location st I = Divide a,b or ex i1 being Instruction-Location of SCM st I = goto i1 or ex a being Data-Location ex i1 being Instruction-Location of SCM st I = a =0_goto i1 or ex a being Data-Location ex i1 being Instruction-Location of SCM st I = a >0_goto i1 ) by AMI_3:69;

suppose I = [0 ,{} ] ; :: thesis: I is IC-good

hence I is IC-good by AMI_3:71; :: thesis: verum

end;

suppose ex a, b being Data-Location st I = a := b ; :: thesis: I is IC-good

then consider a, b being Data-Location such that
A1: I = a := b ;
thus I is IC-good by A1; :: thesis: verum

end;

suppose ex a, b being Data-Location st I = AddTo a,b ; :: thesis: I is IC-good

then consider a, b being Data-Location such that
A2: I = AddTo a,b ;
thus I is IC-good by A2; :: thesis: verum

end;

suppose ex a, b being Data-Location st I = SubFrom a,b ; :: thesis: I is IC-good

then consider a, b being Data-Location such that
A3: I = SubFrom a,b ;
thus I is IC-good by A3; :: thesis: verum

end;

suppose ex a, b being Data-Location st I = MultBy a,b ; :: thesis: I is IC-good

then consider a, b being Data-Location such that
A4: I = MultBy a,b ;
thus I is IC-good by A4; :: thesis: verum

end;

suppose ex a, b being Data-Location st I = Divide a,b ; :: thesis: I is IC-good

then consider a, b being Data-Location such that
A5: I = Divide a,b ;
thus I is IC-good by A5; :: thesis: verum

end;

suppose ex i1 being Instruction-Location of SCM st I = goto i1 ; :: thesis: I is IC-good

then consider i1 being Instruction-Location of SCM such that
A6: I = goto i1 ;
let k be natural number ; :: according to AMISTD_2:def 17 :: thesis: for b₁, b₂ being Element of product the Object-Kind of SCM holds
( not b₂ = b₁ +* ((IC SCM ) .--> ((IC b₁) + k)) or (IC (Exec I,b₁)) + k = IC (Exec (IncAddr I,k),b₂) )
let s1, s2 be State of SCM ; :: thesis: ( not s2 = s1 +* ((IC SCM ) .--> ((IC s1) + k)) or (IC (Exec I,s1)) + k = IC (Exec (IncAddr I,k),s2) )
assume s2 = s1 +* ((IC SCM ) .--> ((IC s1) + k)) ; :: thesis: (IC (Exec I,s1)) + k = IC (Exec (IncAddr I,k),s2)
IC (Exec I,s1) = i1 by A6, AMI_3:13;
hence (IC (Exec I,s1)) + k = IC (Exec (goto (il. SCM ,((locnum i1) + k))),s2) by AMI_3:13
.= IC (Exec (IncAddr I,k),s2) by A6, Th57 ;
:: thesis: verum

end;

suppose ex a being Data-Location ex i1 being Instruction-Location of SCM st I = a =0_goto i1 ; :: thesis: I is IC-good

then consider a being Data-Location , i1 being Instruction-Location of SCM such that
A7: I = a =0_goto i1 ;
let k be natural number ; :: according to AMISTD_2:def 17 :: thesis: for b₁, b₂ being Element of product the Object-Kind of SCM holds
( not b₂ = b₁ +* ((IC SCM ) .--> ((IC b₁) + k)) or (IC (Exec I,b₁)) + k = IC (Exec (IncAddr I,k),b₂) )
let s1, s2 be State of SCM ; :: thesis: ( not s2 = s1 +* ((IC SCM ) .--> ((IC s1) + k)) or (IC (Exec I,s1)) + k = IC (Exec (IncAddr I,k),s2) )
assume A8: s2 = s1 +* ((IC SCM ) .--> ((IC s1) + k)) ; :: thesis: (IC (Exec I,s1)) + k = IC (Exec (IncAddr I,k),s2)
A9: a <> IC SCM by AMI_5:20;
dom ((IC SCM ) .--> ((IC s1) + k)) = {(IC SCM )} by FUNCOP_1:19;
then not a in dom ((IC SCM ) .--> ((IC s1) + k)) by A9, TARSKI:def 1;
then A10: s1 . a = s2 . a by A8, FUNCT_4:12;

now

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

suppose A11: s1 . a = 0 ; :: thesis: (IC (Exec I,s1)) + k = IC (Exec (IncAddr I,k),s2)

then IC (Exec I,s1) = i1 by A7, AMI_3:14;
hence (IC (Exec I,s1)) + k = IC (Exec (a =0_goto (il. SCM ,((locnum i1) + k))),s2) by A10, A11, AMI_3:14
.= IC (Exec (IncAddr I,k),s2) by A7, Th58 ;
:: thesis: verum

end;

suppose A12: s1 . a <> 0 ; :: thesis: (IC (Exec I,s1)) + k = IC (Exec (IncAddr I,k),s2)

dom ((IC SCM ) .--> ((IC s1) + k)) = {(IC SCM )} by FUNCOP_1:19;
then IC SCM in dom ((IC SCM ) .--> ((IC s1) + k)) by TARSKI:def 1;
then A13: IC s2 = ((IC SCM ) .--> ((IC s1) + k)) . (IC SCM ) by A8, FUNCT_4:14
.= il. SCM ,((locnum (IC s1)) + k) by FUNCOP_1:87 ;
A14: IC (Exec I,s2) = Next by A7, A10, A12, AMI_3:14
.= NextLoc (IC s2) by Th56
.= il. SCM ,(((locnum (IC s1)) + k) + 1) by A13, AMISTD_1:def 13
.= il. SCM ,(((locnum (IC s1)) + 1) + k) ;
IC (Exec I,s1) = Next by A7, A12, AMI_3:14
.= NextLoc (IC s1) by Th56
.= il. SCM ,((locnum (IC s1)) + 1) ;
hence (IC (Exec I,s1)) + k = (Exec I,s2) . (IC SCM ) by A14, AMISTD_1:def 13
.= Next by A7, A10, A12, AMI_3:14
.= IC (Exec (a =0_goto (il. SCM ,((locnum i1) + k))),s2) by A10, A12, AMI_3:14
.= IC (Exec (IncAddr I,k),s2) by A7, Th58 ;
:: thesis: verum

end;

end;

end;

hence (IC (Exec I,s1)) + k = IC (Exec (IncAddr I,k),s2) ; :: thesis: verum

end;

suppose ex a being Data-Location ex i1 being Instruction-Location of SCM st I = a >0_goto i1 ; :: thesis: I is IC-good

then consider a being Data-Location , i1 being Instruction-Location of SCM such that
A15: I = a >0_goto i1 ;
let k be natural number ; :: according to AMISTD_2:def 17 :: thesis: for b₁, b₂ being Element of product the Object-Kind of SCM holds
( not b₂ = b₁ +* ((IC SCM ) .--> ((IC b₁) + k)) or (IC (Exec I,b₁)) + k = IC (Exec (IncAddr I,k),b₂) )
let s1, s2 be State of SCM ; :: thesis: ( not s2 = s1 +* ((IC SCM ) .--> ((IC s1) + k)) or (IC (Exec I,s1)) + k = IC (Exec (IncAddr I,k),s2) )
assume A16: s2 = s1 +* ((IC SCM ) .--> ((IC s1) + k)) ; :: thesis: (IC (Exec I,s1)) + k = IC (Exec (IncAddr I,k),s2)
A17: a <> IC SCM by AMI_5:20;
dom ((IC SCM ) .--> ((IC s1) + k)) = {(IC SCM )} by FUNCOP_1:19;
then not a in dom ((IC SCM ) .--> ((IC s1) + k)) by A17, TARSKI:def 1;
then A18: s1 . a = s2 . a by A16, FUNCT_4:12;

now

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

suppose A19: s1 . a > 0 ; :: thesis: (IC (Exec I,s1)) + k = IC (Exec (IncAddr I,k),s2)

then IC (Exec I,s1) = i1 by A15, AMI_3:15;
hence (IC (Exec I,s1)) + k = IC (Exec (a >0_goto (il. SCM ,((locnum i1) + k))),s2) by A18, A19, AMI_3:15
.= IC (Exec (IncAddr I,k),s2) by A15, Th59 ;
:: thesis: verum

end;

suppose A20: s1 . a <= 0 ; :: thesis: (IC (Exec I,s1)) + k = IC (Exec (IncAddr I,k),s2)

dom ((IC SCM ) .--> ((IC s1) + k)) = {(IC SCM )} by FUNCOP_1:19;
then IC SCM in dom ((IC SCM ) .--> ((IC s1) + k)) by TARSKI:def 1;
then A21: IC s2 = ((IC SCM ) .--> ((IC s1) + k)) . (IC SCM ) by A16, FUNCT_4:14
.= il. SCM ,((locnum (IC s1)) + k) by FUNCOP_1:87 ;
A22: IC (Exec I,s2) = Next by A15, A18, A20, AMI_3:15
.= NextLoc (IC s2) by Th56
.= il. SCM ,(((locnum (IC s1)) + k) + 1) by A21, AMISTD_1:def 13
.= il. SCM ,(((locnum (IC s1)) + 1) + k) ;
IC (Exec I,s1) = Next by A15, A20, AMI_3:15
.= NextLoc (IC s1) by Th56
.= il. SCM ,((locnum (IC s1)) + 1) ;
hence (IC (Exec I,s1)) + k = (Exec I,s2) . (IC SCM ) by A22, AMISTD_1:def 13
.= Next by A15, A18, A20, AMI_3:15
.= IC (Exec (a >0_goto (il. SCM ,((locnum i1) + k))),s2) by A18, A20, AMI_3:15
.= IC (Exec (IncAddr I,k),s2) by A15, Th59 ;
:: thesis: verum

end;

end;

end;

hence (IC (Exec I,s1)) + k = IC (Exec (IncAddr I,k),s2) ; :: thesis: verum

end;

end;

end;

let I be Instruction of SCM ; :: according to AMISTD_2:def 20 :: thesis: I is Exec-preserving
let s1, s2 be State of SCM ; :: according to AMISTD_2:def 19 :: thesis: ( not s1,s2 equal_outside NAT or Exec I,s1, Exec I,s2 equal_outside NAT )
assume A23: s1,s2 equal_outside NAT ; :: thesis: Exec I,s1, Exec I,s2 equal_outside NAT
A24: dom (Exec I,s1) = dom the Object-Kind of SCM by CARD_3:18;
then A25: dom (Exec I,s1) = dom (Exec I,s2) by CARD_3:18;
A26: dom the Object-Kind of SCM = the carrier of SCM by FUNCT_2:def 1;
A27: IC s1 = IC s2 by A23, AMI_1:121;

per cases ( I = [0 ,{} ] or ex a, b being Data-Location st I = a := b or ex a, b being Data-Location st I = AddTo a,b or ex a, b being Data-Location st I = SubFrom a,b or ex a, b being Data-Location st I = MultBy a,b or ex a, b being Data-Location st I = Divide a,b or ex i1 being Instruction-Location of SCM st I = goto i1 or ex a being Data-Location ex i1 being Instruction-Location of SCM st I = a =0_goto i1 or ex a being Data-Location ex i1 being Instruction-Location of SCM st I = a >0_goto i1 ) by AMI_3:69;

suppose I = [0 ,{} ] ; :: thesis: Exec I,s1, Exec I,s2 equal_outside NAT

hence Exec I,s1, Exec I,s2 equal_outside NAT by A23, AMISTD_2:def 19, AMI_3:71; :: thesis: verum

end;

suppose ex a, b being Data-Location st I = a := b ; :: thesis: Exec I,s1, Exec I,s2 equal_outside NAT

then consider a, b being Data-Location such that
A28: I = a := b ;
for x being set st x in (dom (Exec I,s1)) \ NAT holds
(Exec I,s1) . x = (Exec I,s2) . x

proof

let x be set ; :: thesis: ( x in (dom (Exec I,s1)) \ NAT implies (Exec I,s1) . x = (Exec I,s2) . x )
assume A29: x in (dom (Exec I,s1)) \ NAT ; :: thesis: (Exec I,s1) . x = (Exec I,s2) . x
then A30: not x in NAT by XBOOLE_0:def 5;

per cases ( x = IC SCM or x = a or ( x is Data-Location & x <> a ) ) by A24, A26, A29, A30, Th3;

suppose A31: x = IC SCM ; :: thesis: (Exec I,s1) . x = (Exec I,s2) . x

hence (Exec I,s1) . x = Next by A28, AMI_3:8
.= (Exec I,s2) . x by A27, A28, A31, AMI_3:8 ;
:: thesis: verum

end;

suppose A32: x = a ; :: thesis: (Exec I,s1) . x = (Exec I,s2) . x

hence (Exec I,s1) . x = s1 . b by A28, AMI_3:8
.= s2 . b by A23, Th5
.= (Exec I,s2) . x by A28, A32, AMI_3:8 ;
:: thesis: verum

end;

suppose that A33: x is Data-Location and
A34: x <> a ; :: thesis: (Exec I,s1) . x = (Exec I,s2) . x

thus (Exec I,s1) . x = s1 . x by A28, A33, A34, AMI_3:8
.= s2 . x by A23, A33, Th5
.= (Exec I,s2) . x by A28, A33, A34, AMI_3:8 ; :: thesis: verum

end;

end;

end;

hence (Exec I,s1) | ((dom (Exec I,s1)) \ NAT ) = (Exec I,s2) | ((dom (Exec I,s2)) \ NAT ) by A25, FUNCT_1:165; :: according to FUNCT_7:def 2 :: thesis: verum

end;

suppose ex a, b being Data-Location st I = AddTo a,b ; :: thesis: Exec I,s1, Exec I,s2 equal_outside NAT

then consider a, b being Data-Location such that
A35: I = AddTo a,b ;
for x being set st x in (dom (Exec I,s1)) \ NAT holds
(Exec I,s1) . x = (Exec I,s2) . x

proof

let x be set ; :: thesis: ( x in (dom (Exec I,s1)) \ NAT implies (Exec I,s1) . x = (Exec I,s2) . x )
assume A36: x in (dom (Exec I,s1)) \ NAT ; :: thesis: (Exec I,s1) . x = (Exec I,s2) . x
then A37: not x in NAT by XBOOLE_0:def 5;

per cases ( x = IC SCM or x = a or ( x is Data-Location & x <> a ) ) by A24, A26, A36, A37, Th3;

suppose A38: x = IC SCM ; :: thesis: (Exec I,s1) . x = (Exec I,s2) . x

hence (Exec I,s1) . x = Next by A35, AMI_3:9
.= (Exec I,s2) . x by A27, A35, A38, AMI_3:9 ;
:: thesis: verum

end;

suppose A39: x = a ; :: thesis: (Exec I,s1) . x = (Exec I,s2) . x

hence (Exec I,s1) . x = (s1 . a) + (s1 . b) by A35, AMI_3:9
.= (s1 . a) + (s2 . b) by A23, Th5
.= (s2 . a) + (s2 . b) by A23, Th5
.= (Exec I,s2) . x by A35, A39, AMI_3:9 ;
:: thesis: verum

end;

suppose that A40: x is Data-Location and
A41: x <> a ; :: thesis: (Exec I,s1) . x = (Exec I,s2) . x

thus (Exec I,s1) . x = s1 . x by A35, A40, A41, AMI_3:9
.= s2 . x by A23, A40, Th5
.= (Exec I,s2) . x by A35, A40, A41, AMI_3:9 ; :: thesis: verum

end;

end;

end;

hence (Exec I,s1) | ((dom (Exec I,s1)) \ NAT ) = (Exec I,s2) | ((dom (Exec I,s2)) \ NAT ) by A25, FUNCT_1:165; :: according to FUNCT_7:def 2 :: thesis: verum

end;

suppose ex a, b being Data-Location st I = SubFrom a,b ; :: thesis: Exec I,s1, Exec I,s2 equal_outside NAT

then consider a, b being Data-Location such that
A42: I = SubFrom a,b ;
for x being set st x in (dom (Exec I,s1)) \ NAT holds
(Exec I,s1) . x = (Exec I,s2) . x

proof

let x be set ; :: thesis: ( x in (dom (Exec I,s1)) \ NAT implies (Exec I,s1) . x = (Exec I,s2) . x )
assume A43: x in (dom (Exec I,s1)) \ NAT ; :: thesis: (Exec I,s1) . x = (Exec I,s2) . x
then A44: not x in NAT by XBOOLE_0:def 5;

per cases ( x = IC SCM or x = a or ( x is Data-Location & x <> a ) ) by A24, A26, A43, A44, Th3;

suppose A45: x = IC SCM ; :: thesis: (Exec I,s1) . x = (Exec I,s2) . x

hence (Exec I,s1) . x = Next by A42, AMI_3:10
.= (Exec I,s2) . x by A27, A42, A45, AMI_3:10 ;
:: thesis: verum

end;

suppose A46: x = a ; :: thesis: (Exec I,s1) . x = (Exec I,s2) . x

hence (Exec I,s1) . x = (s1 . a) - (s1 . b) by A42, AMI_3:10
.= (s1 . a) - (s2 . b) by A23, Th5
.= (s2 . a) - (s2 . b) by A23, Th5
.= (Exec I,s2) . x by A42, A46, AMI_3:10 ;
:: thesis: verum

end;

suppose that A47: x is Data-Location and
A48: x <> a ; :: thesis: (Exec I,s1) . x = (Exec I,s2) . x

thus (Exec I,s1) . x = s1 . x by A42, A47, A48, AMI_3:10
.= s2 . x by A23, A47, Th5
.= (Exec I,s2) . x by A42, A47, A48, AMI_3:10 ; :: thesis: verum

end;

end;

end;

hence (Exec I,s1) | ((dom (Exec I,s1)) \ NAT ) = (Exec I,s2) | ((dom (Exec I,s2)) \ NAT ) by A25, FUNCT_1:165; :: according to FUNCT_7:def 2 :: thesis: verum

end;

suppose ex a, b being Data-Location st I = MultBy a,b ; :: thesis: Exec I,s1, Exec I,s2 equal_outside NAT

then consider a, b being Data-Location such that
A49: I = MultBy a,b ;
for x being set st x in (dom (Exec I,s1)) \ NAT holds
(Exec I,s1) . x = (Exec I,s2) . x

proof

let x be set ; :: thesis: ( x in (dom (Exec I,s1)) \ NAT implies (Exec I,s1) . x = (Exec I,s2) . x )
assume A50: x in (dom (Exec I,s1)) \ NAT ; :: thesis: (Exec I,s1) . x = (Exec I,s2) . x
then A51: not x in NAT by XBOOLE_0:def 5;

per cases ( x = IC SCM or x = a or ( x is Data-Location & x <> a ) ) by A24, A26, A50, A51, Th3;

suppose A52: x = IC SCM ; :: thesis: (Exec I,s1) . x = (Exec I,s2) . x

hence (Exec I,s1) . x = Next by A49, AMI_3:11
.= (Exec I,s2) . x by A27, A49, A52, AMI_3:11 ;
:: thesis: verum

end;

suppose A53: x = a ; :: thesis: (Exec I,s1) . x = (Exec I,s2) . x

hence (Exec I,s1) . x = (s1 . a) * (s1 . b) by A49, AMI_3:11
.= (s1 . a) * (s2 . b) by A23, Th5
.= (s2 . a) * (s2 . b) by A23, Th5
.= (Exec I,s2) . x by A49, A53, AMI_3:11 ;
:: thesis: verum

end;

suppose that A54: x is Data-Location and
A55: x <> a ; :: thesis: (Exec I,s1) . x = (Exec I,s2) . x

thus (Exec I,s1) . x = s1 . x by A49, A54, A55, AMI_3:11
.= s2 . x by A23, A54, Th5
.= (Exec I,s2) . x by A49, A54, A55, AMI_3:11 ; :: thesis: verum

end;

end;

end;

hence (Exec I,s1) | ((dom (Exec I,s1)) \ NAT ) = (Exec I,s2) | ((dom (Exec I,s2)) \ NAT ) by A25, FUNCT_1:165; :: according to FUNCT_7:def 2 :: thesis: verum

end;

suppose ex a, b being Data-Location st I = Divide a,b ; :: thesis: Exec I,s1, Exec I,s2 equal_outside NAT

then consider a, b being Data-Location such that
A56: I = Divide a,b ;
for x being set st x in (dom (Exec I,s1)) \ NAT holds
(Exec I,s1) . x = (Exec I,s2) . x

proof

let x be set ; :: thesis: ( x in (dom (Exec I,s1)) \ NAT implies (Exec I,s1) . x = (Exec I,s2) . x )
assume A57: x in (dom (Exec I,s1)) \ NAT ; :: thesis: (Exec I,s1) . x = (Exec I,s2) . x
then A58: not x in NAT by XBOOLE_0:def 5;

per cases ( x = IC SCM or x is Data-Location ) by A24, A26, A57, A58, Th3;

suppose A59: x = IC SCM ; :: thesis: (Exec I,s1) . x = (Exec I,s2) . x

hence (Exec I,s1) . x = Next by A56, AMI_3:12
.= (Exec I,s2) . x by A27, A56, A59, AMI_3:12 ;
:: thesis: verum

end;

suppose A60: x is Data-Location ; :: thesis: (Exec I,s1) . x = (Exec I,s2) . x

A61: ( s1 . a = s2 . a & s1 . b = s2 . b ) by A23, Th5;

now

let c be Data-Location ; :: thesis: (Exec I,s1) . b₁ = (Exec I,s2) . b₁

per cases ( c = b or ( c = a & c <> b ) or ( c <> a & c <> b ) ) ;

suppose A62: c = b ; :: thesis: (Exec I,s1) . b₁ = (Exec I,s2) . b₁

hence (Exec I,s1) . c = (s2 . a) mod (s2 . b) by A56, A61, AMI_3:12
.= (Exec I,s2) . c by A56, A62, AMI_3:12 ;
:: thesis: verum

end;

suppose A63: ( c = a & c <> b ) ; :: thesis: (Exec I,s1) . b₁ = (Exec I,s2) . b₁

hence (Exec I,s1) . c = (s2 . a) div (s2 . b) by A56, A61, AMI_3:12
.= (Exec I,s2) . c by A56, A63, AMI_3:12 ;
:: thesis: verum

end;

suppose A64: ( c <> a & c <> b ) ; :: thesis: (Exec I,s1) . b₁ = (Exec I,s2) . b₁

hence (Exec I,s1) . c = s1 . c by A56, AMI_3:12
.= s2 . c by A23, Th5
.= (Exec I,s2) . c by A56, A64, AMI_3:12 ;
:: thesis: verum

end;

end;

end;

hence (Exec I,s1) . x = (Exec I,s2) . x by A60; :: thesis: verum

end;

end;

end;

hence (Exec I,s1) | ((dom (Exec I,s1)) \ NAT ) = (Exec I,s2) | ((dom (Exec I,s2)) \ NAT ) by A25, FUNCT_1:165; :: according to FUNCT_7:def 2 :: thesis: verum

end;

suppose ex i1 being Instruction-Location of SCM st I = goto i1 ; :: thesis: Exec I,s1, Exec I,s2 equal_outside NAT

then consider i1 being Instruction-Location of SCM such that
A65: I = goto i1 ;
for x being set st x in (dom (Exec I,s1)) \ NAT holds
(Exec I,s1) . x = (Exec I,s2) . x

proof

let x be set ; :: thesis: ( x in (dom (Exec I,s1)) \ NAT implies (Exec I,s1) . x = (Exec I,s2) . x )
assume A66: x in (dom (Exec I,s1)) \ NAT ; :: thesis: (Exec I,s1) . x = (Exec I,s2) . x
then A67: not x in NAT by XBOOLE_0:def 5;

per cases ( x = IC SCM or x is Data-Location ) by A24, A26, A66, A67, Th3;

suppose A68: x = IC SCM ; :: thesis: (Exec I,s1) . x = (Exec I,s2) . x

hence (Exec I,s1) . x = i1 by A65, AMI_3:13
.= (Exec I,s2) . x by A65, A68, AMI_3:13 ;
:: thesis: verum

end;

suppose A69: x is Data-Location ; :: thesis: (Exec I,s1) . x = (Exec I,s2) . x

hence (Exec I,s1) . x = s1 . x by A65, AMI_3:13
.= s2 . x by A23, A69, Th5
.= (Exec I,s2) . x by A65, A69, AMI_3:13 ;
:: thesis: verum

end;

end;

end;

hence (Exec I,s1) | ((dom (Exec I,s1)) \ NAT ) = (Exec I,s2) | ((dom (Exec I,s2)) \ NAT ) by A25, FUNCT_1:165; :: according to FUNCT_7:def 2 :: thesis: verum

end;

suppose ex a being Data-Location ex i1 being Instruction-Location of SCM st I = a =0_goto i1 ; :: thesis: Exec I,s1, Exec I,s2 equal_outside NAT

then consider a being Data-Location , i1 being Instruction-Location of SCM such that
A70: I = a =0_goto i1 ;
for x being set st x in (dom (Exec I,s1)) \ NAT holds
(Exec I,s1) . x = (Exec I,s2) . x

proof

let x be set ; :: thesis: ( x in (dom (Exec I,s1)) \ NAT implies (Exec I,s1) . x = (Exec I,s2) . x )
assume A71: x in (dom (Exec I,s1)) \ NAT ; :: thesis: (Exec I,s1) . x = (Exec I,s2) . x
then A72: not x in NAT by XBOOLE_0:def 5;
A73: s1 . a = s2 . a by A23, Th5;

per cases ( ( x = IC SCM & s1 . a = 0 ) or ( x = IC SCM & s1 . a <> 0 ) or x is Data-Location ) by A24, A26, A71, A72, Th3;

suppose that A74: x = IC SCM and
A75: s1 . a = 0 ; :: thesis: (Exec I,s1) . x = (Exec I,s2) . x

thus (Exec I,s1) . x = i1 by A70, A74, A75, AMI_3:14
.= (Exec I,s2) . x by A70, A73, A74, A75, AMI_3:14 ; :: thesis: verum

end;

suppose that A76: x = IC SCM and
A77: s1 . a <> 0 ; :: thesis: (Exec I,s1) . x = (Exec I,s2) . x

thus (Exec I,s1) . x = Next by A70, A76, A77, AMI_3:14
.= (Exec I,s2) . x by A27, A70, A73, A76, A77, AMI_3:14 ; :: thesis: verum

end;

suppose A78: x is Data-Location ; :: thesis: (Exec I,s1) . x = (Exec I,s2) . x

hence (Exec I,s1) . x = s1 . x by A70, AMI_3:14
.= s2 . x by A23, A78, Th5
.= (Exec I,s2) . x by A70, A78, AMI_3:14 ;
:: thesis: verum

end;

end;

end;

hence (Exec I,s1) | ((dom (Exec I,s1)) \ NAT ) = (Exec I,s2) | ((dom (Exec I,s2)) \ NAT ) by A25, FUNCT_1:165; :: according to FUNCT_7:def 2 :: thesis: verum

end;

suppose ex a being Data-Location ex i1 being Instruction-Location of SCM st I = a >0_goto i1 ; :: thesis: Exec I,s1, Exec I,s2 equal_outside NAT

then consider a being Data-Location , i1 being Instruction-Location of SCM such that
A79: I = a >0_goto i1 ;
for x being set st x in (dom (Exec I,s1)) \ NAT holds
(Exec I,s1) . x = (Exec I,s2) . x

proof

let x be set ; :: thesis: ( x in (dom (Exec I,s1)) \ NAT implies (Exec I,s1) . x = (Exec I,s2) . x )
assume A80: x in (dom (Exec I,s1)) \ NAT ; :: thesis: (Exec I,s1) . x = (Exec I,s2) . x
then A81: not x in NAT by XBOOLE_0:def 5;
A82: s1 . a = s2 . a by A23, Th5;

per cases ( ( x = IC SCM & s1 . a > 0 ) or ( x = IC SCM & s1 . a <= 0 ) or x is Data-Location ) by A24, A26, A80, A81, Th3;

suppose that A83: x = IC SCM and
A84: s1 . a > 0 ; :: thesis: (Exec I,s1) . x = (Exec I,s2) . x

thus (Exec I,s1) . x = i1 by A79, A83, A84, AMI_3:15
.= (Exec I,s2) . x by A79, A82, A83, A84, AMI_3:15 ; :: thesis: verum

end;

suppose that A85: x = IC SCM and
A86: s1 . a <= 0 ; :: thesis: (Exec I,s1) . x = (Exec I,s2) . x

thus (Exec I,s1) . x = Next by A79, A85, A86, AMI_3:15
.= (Exec I,s2) . x by A27, A79, A82, A85, A86, AMI_3:15 ; :: thesis: verum

end;

suppose A87: x is Data-Location ; :: thesis: (Exec I,s1) . x = (Exec I,s2) . x

hence (Exec I,s1) . x = s1 . x by A79, AMI_3:15
.= s2 . x by A23, A87, Th5
.= (Exec I,s2) . x by A79, A87, AMI_3:15 ;
:: thesis: verum

end;

end;

end;

hence (Exec I,s1) | ((dom (Exec I,s1)) \ NAT ) = (Exec I,s2) | ((dom (Exec I,s2)) \ NAT ) by A25, FUNCT_1:165; :: according to FUNCT_7:def 2 :: thesis: verum

end;

end;