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

proof

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

per cases ( I = [0 ,{} ] or ex a, b being Data-Location of R st I = a := b or ex a, b being Data-Location of R st I = AddTo a,b or ex a, b being Data-Location of R st I = SubFrom a,b or ex a, b being Data-Location of R st I = MultBy a,b or ex i1 being Instruction-Location of SCM R st I = goto i1 or ex a being Data-Location of R ex i1 being Instruction-Location of SCM R st I = a =0_goto i1 or ex a being Data-Location of R ex r being Element of R st I = a := r ) by SCMRING2:8;

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

then I = halt (SCM R) by SCMRING2:30;
hence I is IC-good ; :: thesis: verum

end;

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

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

end;

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

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

end;

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

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

end;

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

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

end;

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

then consider i1 being Instruction-Location of SCM R such that
A5: 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 R) holds
( not b₂ = b₁ +* ((IC (SCM R)) .--> ((IC b₁) + k)) or (IC (Exec I,b₁)) + k = IC (Exec (IncAddr I,k),b₂) )
let s1, s2 be State of (SCM R); :: thesis: ( not s2 = s1 +* ((IC (SCM R)) .--> ((IC s1) + k)) or (IC (Exec I,s1)) + k = IC (Exec (IncAddr I,k),s2) )
assume s2 = s1 +* ((IC (SCM R)) .--> ((IC s1) + k)) ; :: thesis: (IC (Exec I,s1)) + k = IC (Exec (IncAddr I,k),s2)
IC (Exec I,s1) = i1 by A5, SCMRING2:17;
hence (IC (Exec I,s1)) + k = IC (Exec (goto (il. (SCM R),((locnum i1) + k))),s2) by SCMRING2:17
.= IC (Exec (IncAddr I,k),s2) by A5, Th69 ;
:: thesis: verum

end;

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

then consider a being Data-Location of R, i1 being Instruction-Location of SCM R such that
A6: 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 R) holds
( not b₂ = b₁ +* ((IC (SCM R)) .--> ((IC b₁) + k)) or (IC (Exec I,b₁)) + k = IC (Exec (IncAddr I,k),b₂) )
let s1, s2 be State of (SCM R); :: thesis: ( not s2 = s1 +* ((IC (SCM R)) .--> ((IC s1) + k)) or (IC (Exec I,s1)) + k = IC (Exec (IncAddr I,k),s2) )
assume A7: s2 = s1 +* ((IC (SCM R)) .--> ((IC s1) + k)) ; :: thesis: (IC (Exec I,s1)) + k = IC (Exec (IncAddr I,k),s2)
A8: a <> IC (SCM R) by Th3;
dom ((IC (SCM R)) .--> ((IC s1) + k)) = {(IC (SCM R))} by FUNCOP_1:19;
then not a in dom ((IC (SCM R)) .--> ((IC s1) + k)) by A8, TARSKI:def 1;
then A9: s1 . a = s2 . a by A7, FUNCT_4:12;

now

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

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

then IC (Exec I,s1) = i1 by A6, SCMRING2:18;
hence (IC (Exec I,s1)) + k = IC (Exec (a =0_goto (il. (SCM R),((locnum i1) + k))),s2) by A9, A10, SCMRING2:18
.= IC (Exec (IncAddr I,k),s2) by A6, Th70 ;
:: thesis: verum

end;

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

dom ((IC (SCM R)) .--> ((IC s1) + k)) = {(IC (SCM R))} by FUNCOP_1:19;
then IC (SCM R) in dom ((IC (SCM R)) .--> ((IC s1) + k)) by TARSKI:def 1;
then A12: IC s2 = ((IC (SCM R)) .--> ((IC s1) + k)) . (IC (SCM R)) by A7, FUNCT_4:14
.= il. (SCM R),((locnum (IC s1)) + k) by FUNCOP_1:87 ;
A13: IC (Exec I,s2) = Next (IC s2) by A6, A9, A11, SCMRING2:18
.= NextLoc (IC s2) by Th68
.= il. (SCM R),(((locnum (IC s1)) + k) + 1) by A12, AMISTD_1:def 13
.= il. (SCM R),(((locnum (IC s1)) + 1) + k) ;
IC (Exec I,s1) = Next (IC s1) by A6, A11, SCMRING2:18
.= NextLoc (IC s1) by Th68
.= il. (SCM R),((locnum (IC s1)) + 1) ;
hence (IC (Exec I,s1)) + k = (Exec I,s2) . (IC (SCM R)) by A13, AMISTD_1:def 13
.= Next (IC s2) by A6, A9, A11, SCMRING2:18
.= IC (Exec (a =0_goto (il. (SCM R),((locnum i1) + k))),s2) by A9, A11, SCMRING2:18
.= IC (Exec (IncAddr I,k),s2) by A6, Th70 ;
:: 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 of R ex r being Element of R st I = a := r ; :: thesis: I is IC-good

then consider a being Data-Location of R, r being Element of R such that
A14: I = a := r ;
thus I is IC-good by A14; :: thesis: verum

end;

end;

end;

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

per cases ( I = [0 ,{} ] or ex a, b being Data-Location of R st I = a := b or ex a, b being Data-Location of R st I = AddTo a,b or ex a, b being Data-Location of R st I = SubFrom a,b or ex a, b being Data-Location of R st I = MultBy a,b or ex i1 being Instruction-Location of SCM R st I = goto i1 or ex a being Data-Location of R ex i1 being Instruction-Location of SCM R st I = a =0_goto i1 or ex a being Data-Location of R ex r being Element of R st I = a := r ) by SCMRING2:8;

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

then I = halt (SCM R) by SCMRING2:30;
hence Exec I,s1, Exec I,s2 equal_outside NAT by A15, AMISTD_2:def 19; :: thesis: verum

end;

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

then consider a, b being Data-Location of R such that
A20: 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 A21: x in (dom (Exec I,s1)) \ NAT ; :: thesis: (Exec I,s1) . x = (Exec I,s2) . x
then A22: not x in NAT by XBOOLE_0:def 5;

per cases ( x = IC (SCM R) or x = a or ( x is Data-Location of R & x <> a ) ) by A16, A18, A21, A22, Th5;

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

hence (Exec I,s1) . x = Next (IC s1) by A20, SCMRING2:13
.= (Exec I,s2) . x by A19, A20, A23, SCMRING2:13 ;
:: thesis: verum

end;

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

hence (Exec I,s1) . x = s1 . b by A20, SCMRING2:13
.= s2 . b by A15, Th7
.= (Exec I,s2) . x by A20, A24, SCMRING2:13 ;
:: thesis: verum

end;

suppose that A25: x is Data-Location of R and
A26: x <> a ; :: thesis: (Exec I,s1) . x = (Exec I,s2) . x

thus (Exec I,s1) . x = s1 . x by A20, A25, A26, SCMRING2:13
.= s2 . x by A15, A25, Th7
.= (Exec I,s2) . x by A20, A25, A26, SCMRING2:13 ; :: thesis: verum

end;

end;

end;

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

end;

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

then consider a, b being Data-Location of R such that
A27: 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 A28: x in (dom (Exec I,s1)) \ NAT ; :: thesis: (Exec I,s1) . x = (Exec I,s2) . x
then A29: not x in NAT by XBOOLE_0:def 5;

per cases ( x = IC (SCM R) or x = a or ( x is Data-Location of R & x <> a ) ) by A16, A18, A28, A29, Th5;

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

hence (Exec I,s1) . x = Next (IC s1) by A27, SCMRING2:14
.= (Exec I,s2) . x by A19, A27, A30, SCMRING2:14 ;
:: thesis: verum

end;

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

hence (Exec I,s1) . x = (s1 . a) + (s1 . b) by A27, SCMRING2:14
.= (s1 . a) + (s2 . b) by A15, Th7
.= (s2 . a) + (s2 . b) by A15, Th7
.= (Exec I,s2) . x by A27, A31, SCMRING2:14 ;
:: thesis: verum

end;

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

thus (Exec I,s1) . x = s1 . x by A27, A32, A33, SCMRING2:14
.= s2 . x by A15, A32, Th7
.= (Exec I,s2) . x by A27, A32, A33, SCMRING2:14 ; :: thesis: verum

end;

end;

end;

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

end;

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

then consider a, b being Data-Location of R such that
A34: 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 A35: x in (dom (Exec I,s1)) \ NAT ; :: thesis: (Exec I,s1) . x = (Exec I,s2) . x
then A36: not x in NAT by XBOOLE_0:def 5;

per cases ( x = IC (SCM R) or x = a or ( x is Data-Location of R & x <> a ) ) by A16, A18, A35, A36, Th5;

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

hence (Exec I,s1) . x = Next (IC s1) by A34, SCMRING2:15
.= (Exec I,s2) . x by A19, A34, A37, SCMRING2:15 ;
:: thesis: verum

end;

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

hence (Exec I,s1) . x = (s1 . a) - (s1 . b) by A34, SCMRING2:15
.= (s1 . a) - (s2 . b) by A15, Th7
.= (s2 . a) - (s2 . b) by A15, Th7
.= (Exec I,s2) . x by A34, A38, SCMRING2:15 ;
:: thesis: verum

end;

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

thus (Exec I,s1) . x = s1 . x by A34, A39, A40, SCMRING2:15
.= s2 . x by A15, A39, Th7
.= (Exec I,s2) . x by A34, A39, A40, SCMRING2:15 ; :: thesis: verum

end;

end;

end;

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

end;

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

then consider a, b being Data-Location of R such that
A41: 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 A42: x in (dom (Exec I,s1)) \ NAT ; :: thesis: (Exec I,s1) . x = (Exec I,s2) . x
then A43: not x in NAT by XBOOLE_0:def 5;

per cases ( x = IC (SCM R) or x = a or ( x is Data-Location of R & x <> a ) ) by A16, A18, A42, A43, Th5;

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

hence (Exec I,s1) . x = Next (IC s1) by A41, SCMRING2:16
.= (Exec I,s2) . x by A19, A41, A44, SCMRING2:16 ;
:: thesis: verum

end;

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

hence (Exec I,s1) . x = (s1 . a) * (s1 . b) by A41, SCMRING2:16
.= (s1 . a) * (s2 . b) by A15, Th7
.= (s2 . a) * (s2 . b) by A15, Th7
.= (Exec I,s2) . x by A41, A45, SCMRING2:16 ;
:: thesis: verum

end;

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

thus (Exec I,s1) . x = s1 . x by A41, A46, A47, SCMRING2:16
.= s2 . x by A15, A46, Th7
.= (Exec I,s2) . x by A41, A46, A47, SCMRING2:16 ; :: thesis: verum

end;

end;

end;

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

end;

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

then consider i1 being Instruction-Location of SCM R such that
A48: 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 A49: x in (dom (Exec I,s1)) \ NAT ; :: thesis: (Exec I,s1) . x = (Exec I,s2) . x
then A50: not x in NAT by XBOOLE_0:def 5;

per cases ( x = IC (SCM R) or x is Data-Location of R ) by A16, A18, A49, A50, Th5;

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

hence (Exec I,s1) . x = i1 by A48, SCMRING2:17
.= (Exec I,s2) . x by A48, A51, SCMRING2:17 ;
:: thesis: verum

end;

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

hence (Exec I,s1) . x = s1 . x by A48, SCMRING2:17
.= s2 . x by A15, A52, Th7
.= (Exec I,s2) . x by A48, A52, SCMRING2:17 ;
:: thesis: verum

end;

end;

end;

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

end;

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

then consider a being Data-Location of R, i1 being Instruction-Location of SCM R such that
A53: 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 A54: x in (dom (Exec I,s1)) \ NAT ; :: thesis: (Exec I,s1) . x = (Exec I,s2) . x
then A55: not x in NAT by XBOOLE_0:def 5;
A56: s1 . a = s2 . a by A15, Th7;

per cases ( ( x = IC (SCM R) & s1 . a = 0. R ) or ( x = IC (SCM R) & s1 . a <> 0. R ) or x is Data-Location of R ) by A16, A18, A54, A55, Th5;

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

thus (Exec I,s1) . x = i1 by A53, A57, A58, SCMRING2:18
.= (Exec I,s2) . x by A53, A56, A57, A58, SCMRING2:18 ; :: thesis: verum

end;

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

thus (Exec I,s1) . x = Next (IC s1) by A53, A59, A60, SCMRING2:18
.= (Exec I,s2) . x by A19, A53, A56, A59, A60, SCMRING2:18 ; :: thesis: verum

end;

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

hence (Exec I,s1) . x = s1 . x by A53, SCMRING2:18
.= s2 . x by A15, A61, Th7
.= (Exec I,s2) . x by A53, A61, SCMRING2:18 ;
:: thesis: verum

end;

end;

end;

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

end;

suppose ex a being Data-Location of R ex r being Element of R st I = a := r ; :: thesis: Exec I,s1, Exec I,s2 equal_outside NAT

then consider a being Data-Location of R, r being Element of R such that
A62: I = a := r ;
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 A63: x in (dom (Exec I,s1)) \ NAT ; :: thesis: (Exec I,s1) . x = (Exec I,s2) . x
then A64: not x in NAT by XBOOLE_0:def 5;

per cases ( x = IC (SCM R) or x = a or ( x is Data-Location of R & x <> a ) ) by A16, A18, A63, A64, Th5;

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

hence (Exec I,s1) . x = Next (IC s1) by A62, SCMRING2:19
.= (Exec I,s2) . x by A19, A62, A65, SCMRING2:19 ;
:: thesis: verum

end;

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

hence (Exec I,s1) . x = r by A62, SCMRING2:19
.= (Exec I,s2) . x by A62, A66, SCMRING2:19 ;
:: thesis: verum

end;

suppose that A67: x is Data-Location of R and
A68: x <> a ; :: thesis: (Exec I,s1) . x = (Exec I,s2) . x

thus (Exec I,s1) . x = s1 . x by A62, A67, A68, SCMRING2:19
.= s2 . x by A15, A67, Th7
.= (Exec I,s2) . x by A62, A67, A68, SCMRING2:19 ; :: thesis: verum

end;

end;

end;

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

end;

end;