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 19 :: 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 Element of NAT st I = goto i1,R or ex a being Data-Location of R ex i1 being Element of NAT 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 A1: ex i1 being Element of NAT st I = goto i1,R ; :: thesis: I is IC-good
let k be natural number ; :: according to AMISTD_2:def 18 :: thesis: for b1 being set holds (IC (Exec I,b1)) + k = IC (Exec (IncAddr I,k),(IncrIC b1,k))
let s1 be State of (SCM R); :: thesis: (IC (Exec I,s1)) + k = IC (Exec (IncAddr I,k),(IncrIC s1,k))
set s2 = IncrIC s1,k;
consider i1 being Element of NAT such that
A2: I = goto i1,R by A1;
IC (Exec I,s1) = i1 by A2, SCMRING2:17;
hence (IC (Exec I,s1)) + k = IC (Exec (goto (i1 + k),R),(IncrIC s1,k)) by SCMRING2:17
.= IC (Exec (IncAddr I,k),(IncrIC s1,k)) by A2, Th69 ;
:: thesis: verum
end;
suppose ex a being Data-Location of R ex i1 being Element of NAT st I = a =0_goto i1 ; :: thesis: I is IC-good
then consider a being Data-Location of R, i1 being Element of NAT such that
A3: I = a =0_goto i1 ;
let k be natural number ; :: according to AMISTD_2:def 18 :: thesis: for b1 being set holds (IC (Exec I,b1)) + k = IC (Exec (IncAddr I,k),(IncrIC b1,k))
let s1 be State of (SCM R); :: thesis: (IC (Exec I,s1)) + k = IC (Exec (IncAddr I,k),(IncrIC s1,k))
set s2 = IncrIC s1,k;
( a <> IC (SCM R) & dom ((IC (SCM R)) .--> ((IC s1) + k)) = {(IC (SCM R))} ) by Th3, FUNCOP_1:19;
then not a in dom ((IC (SCM R)) .--> ((IC s1) + k)) by TARSKI:def 1;
then A5: s1 . a = (IncrIC s1,k) . a by FUNCT_4:12;
now
per cases ( s1 . a = 0. R or s1 . a <> 0. R ) ;
suppose A6: s1 . a = 0. R ; :: thesis: (IC (Exec I,s1)) + k = IC (Exec (IncAddr I,k),(IncrIC s1,k))
then IC (Exec I,s1) = i1 by A3, SCMRING2:18;
hence (IC (Exec I,s1)) + k = IC (Exec (a =0_goto (i1 + k)),(IncrIC s1,k)) by A5, A6, SCMRING2:18
.= IC (Exec (IncAddr I,k),(IncrIC s1,k)) by A3, Th70 ;
:: thesis: verum
end;
suppose A7: s1 . a <> 0. R ; :: thesis: (IC (Exec I,s1)) + k = IC (Exec (IncAddr I,k),(IncrIC s1,k))
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 A8: IC (IncrIC s1,k) = ((IC (SCM R)) .--> ((IC s1) + k)) . (IC (SCM R)) by FUNCT_4:14
.= (IC s1) + k by FUNCOP_1:87 ;
A9: IC (Exec I,s1) = succ (IC s1) by A3, A7, SCMRING2:18
.= (IC s1) + 1 ;
IC (Exec I,(IncrIC s1,k)) = succ (IC (IncrIC s1,k)) by A3, A5, A7, SCMRING2:18
.= ((IC s1) + k) + 1 by A8 ;
hence (IC (Exec I,s1)) + k = succ (IC (IncrIC s1,k)) by A3, A5, A7, A9, SCMRING2:18
.= IC (Exec (a =0_goto (i1 + k)),(IncrIC s1,k)) by A5, A7, SCMRING2:18
.= IC (Exec (IncAddr I,k),(IncrIC s1,k)) by A3, Th70 ;
:: thesis: verum
end;
end;
end;
hence (IC (Exec I,s1)) + k = IC (Exec (IncAddr I,k),(IncrIC s1,k)) ; :: 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
hence I is IC-good ; :: thesis: verum
end;
end;
end;
let I be Instruction of (SCM R); :: according to AMISTD_2:def 21 :: thesis: I is Exec-preserving
let s1, s2 be State of (SCM R); :: according to AMISTD_2:def 20 :: thesis: ( not s1,s2 equal_outside NAT or Exec I,s1, Exec I,s2 equal_outside NAT )
assume A11: s1,s2 equal_outside NAT ; :: thesis: Exec I,s1, Exec I,s2 equal_outside NAT
A12: IC s1 = IC s2 by A11, COMPOS_1:24;
A13: dom (Exec I,s1) = the carrier of (SCM R) by PARTFUN1:def 4;
then A14: dom (Exec I,s1) = dom (Exec I,s2) by PARTFUN1:def 4;
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 Element of NAT st I = goto i1,R or ex a being Data-Location of R ex i1 being Element of NAT 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 A11, AMISTD_2:def 20; :: 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
A15: 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 A16: x in (dom (Exec I,s1)) \ NAT ; :: thesis: (Exec I,s1) . x = (Exec I,s2) . x
then A17: 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 A13, A16, A17, Th5;
suppose A18: x = IC (SCM R) ; :: thesis: (Exec I,s1) . x = (Exec I,s2) . x
hence (Exec I,s1) . x = succ (IC s1) by A15, SCMRING2:13
.= (Exec I,s2) . x by A12, A15, A18, SCMRING2:13 ;
:: thesis: verum
end;
suppose A19: x = a ; :: thesis: (Exec I,s1) . x = (Exec I,s2) . x
hence (Exec I,s1) . x = s1 . b by A15, SCMRING2:13
.= s2 . b by A11, Th7
.= (Exec I,s2) . x by A15, A19, SCMRING2:13 ;
:: thesis: verum
end;
suppose that A20: x is Data-Location of R and
A21: x <> a ; :: thesis: (Exec I,s1) . x = (Exec I,s2) . x
thus (Exec I,s1) . x = s1 . x by A15, A20, A21, SCMRING2:13
.= s2 . x by A11, A20, Th7
.= (Exec I,s2) . x by A15, A20, A21, 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 A14, 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
A22: 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 A23: x in (dom (Exec I,s1)) \ NAT ; :: thesis: (Exec I,s1) . x = (Exec I,s2) . x
then A24: 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 A13, A23, A24, Th5;
suppose A25: x = IC (SCM R) ; :: thesis: (Exec I,s1) . x = (Exec I,s2) . x
hence (Exec I,s1) . x = succ (IC s1) by A22, SCMRING2:14
.= (Exec I,s2) . x by A12, A22, A25, SCMRING2:14 ;
:: thesis: verum
end;
suppose A26: x = a ; :: thesis: (Exec I,s1) . x = (Exec I,s2) . x
hence (Exec I,s1) . x = (s1 . a) + (s1 . b) by A22, SCMRING2:14
.= (s1 . a) + (s2 . b) by A11, Th7
.= (s2 . a) + (s2 . b) by A11, Th7
.= (Exec I,s2) . x by A22, A26, SCMRING2:14 ;
:: thesis: verum
end;
suppose that A27: x is Data-Location of R and
A28: x <> a ; :: thesis: (Exec I,s1) . x = (Exec I,s2) . x
thus (Exec I,s1) . x = s1 . x by A22, A27, A28, SCMRING2:14
.= s2 . x by A11, A27, Th7
.= (Exec I,s2) . x by A22, A27, A28, 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 A14, 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
A29: 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 A30: x in (dom (Exec I,s1)) \ NAT ; :: thesis: (Exec I,s1) . x = (Exec I,s2) . x
then A31: 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 A13, A30, A31, Th5;
suppose A32: x = IC (SCM R) ; :: thesis: (Exec I,s1) . x = (Exec I,s2) . x
hence (Exec I,s1) . x = succ (IC s1) by A29, SCMRING2:15
.= (Exec I,s2) . x by A12, A29, A32, SCMRING2:15 ;
:: thesis: verum
end;
suppose A33: x = a ; :: thesis: (Exec I,s1) . x = (Exec I,s2) . x
hence (Exec I,s1) . x = (s1 . a) - (s1 . b) by A29, SCMRING2:15
.= (s1 . a) - (s2 . b) by A11, Th7
.= (s2 . a) - (s2 . b) by A11, Th7
.= (Exec I,s2) . x by A29, A33, SCMRING2:15 ;
:: thesis: verum
end;
suppose that A34: x is Data-Location of R and
A35: x <> a ; :: thesis: (Exec I,s1) . x = (Exec I,s2) . x
thus (Exec I,s1) . x = s1 . x by A29, A34, A35, SCMRING2:15
.= s2 . x by A11, A34, Th7
.= (Exec I,s2) . x by A29, A34, A35, 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 A14, 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
A36: 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 A37: x in (dom (Exec I,s1)) \ NAT ; :: thesis: (Exec I,s1) . x = (Exec I,s2) . x
then A38: 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 A13, A37, A38, Th5;
suppose A39: x = IC (SCM R) ; :: thesis: (Exec I,s1) . x = (Exec I,s2) . x
hence (Exec I,s1) . x = succ (IC s1) by A36, SCMRING2:16
.= (Exec I,s2) . x by A12, A36, A39, SCMRING2:16 ;
:: thesis: verum
end;
suppose A40: x = a ; :: thesis: (Exec I,s1) . x = (Exec I,s2) . x
hence (Exec I,s1) . x = (s1 . a) * (s1 . b) by A36, SCMRING2:16
.= (s1 . a) * (s2 . b) by A11, Th7
.= (s2 . a) * (s2 . b) by A11, Th7
.= (Exec I,s2) . x by A36, A40, SCMRING2:16 ;
:: thesis: verum
end;
suppose that A41: x is Data-Location of R and
A42: x <> a ; :: thesis: (Exec I,s1) . x = (Exec I,s2) . x
thus (Exec I,s1) . x = s1 . x by A36, A41, A42, SCMRING2:16
.= s2 . x by A11, A41, Th7
.= (Exec I,s2) . x by A36, A41, A42, 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 A14, FUNCT_1:165; :: according to FUNCT_7:def 2 :: thesis: verum
end;
suppose ex i1 being Element of NAT st I = goto i1,R ; :: thesis: Exec I,s1, Exec I,s2 equal_outside NAT
then consider i1 being Element of NAT such that
A43: I = goto i1,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 A44: x in (dom (Exec I,s1)) \ NAT ; :: thesis: (Exec I,s1) . x = (Exec I,s2) . x
then A45: not x in NAT by XBOOLE_0:def 5;
per cases ( x = IC (SCM R) or x is Data-Location of R ) by A13, A44, A45, Th5;
suppose A46: x = IC (SCM R) ; :: thesis: (Exec I,s1) . x = (Exec I,s2) . x
hence (Exec I,s1) . x = i1 by A43, SCMRING2:17
.= (Exec I,s2) . x by A43, A46, SCMRING2:17 ;
:: thesis: verum
end;
suppose A47: x is Data-Location of R ; :: thesis: (Exec I,s1) . x = (Exec I,s2) . x
hence (Exec I,s1) . x = s1 . x by A43, SCMRING2:17
.= s2 . x by A11, A47, Th7
.= (Exec I,s2) . x by A43, A47, 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 A14, FUNCT_1:165; :: according to FUNCT_7:def 2 :: thesis: verum
end;
suppose ex a being Data-Location of R ex i1 being Element of NAT 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 Element of NAT such that
A48: 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 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;
A51: s1 . a = s2 . a by A11, 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 A13, A49, A50, Th5;
suppose A52: ( x = IC (SCM R) & s1 . a = 0. R ) ; :: thesis: (Exec I,s1) . x = (Exec I,s2) . x
thus (Exec I,s1) . x = i1 by A48, A52, SCMRING2:18
.= (Exec I,s2) . x by A48, A51, A52, SCMRING2:18 ; :: thesis: verum
end;
suppose A53: ( x = IC (SCM R) & s1 . a <> 0. R ) ; :: thesis: (Exec I,s1) . x = (Exec I,s2) . x
thus (Exec I,s1) . x = succ (IC s1) by A48, A53, SCMRING2:18
.= (Exec I,s2) . x by A12, A48, A51, A53, SCMRING2:18 ; :: thesis: verum
end;
suppose A54: 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:18
.= s2 . x by A11, A54, Th7
.= (Exec I,s2) . x by A48, A54, 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 A14, 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
A55: 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 A56: x in (dom (Exec I,s1)) \ NAT ; :: thesis: (Exec I,s1) . x = (Exec I,s2) . x
then A57: 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 A13, A56, A57, Th5;
suppose A58: x = IC (SCM R) ; :: thesis: (Exec I,s1) . x = (Exec I,s2) . x
hence (Exec I,s1) . x = succ (IC s1) by A55, SCMRING2:19
.= (Exec I,s2) . x by A12, A55, A58, SCMRING2:19 ;
:: thesis: verum
end;
suppose A59: x = a ; :: thesis: (Exec I,s1) . x = (Exec I,s2) . x
hence (Exec I,s1) . x = r by A55, SCMRING2:19
.= (Exec I,s2) . x by A55, A59, SCMRING2:19 ;
:: thesis: verum
end;
suppose that A60: x is Data-Location of R and
A61: x <> a ; :: thesis: (Exec I,s1) . x = (Exec I,s2) . x
thus (Exec I,s1) . x = s1 . x by A55, A60, A61, SCMRING2:19
.= s2 . x by A11, A60, Th7
.= (Exec I,s2) . x by A55, A60, A61, 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 A14, FUNCT_1:165; :: according to FUNCT_7:def 2 :: thesis: verum
end;
end;