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