thus SCM is IC-relocable :: thesis: SCM is Exec-preserving
proof
let I be Instruction of SCM; :: according to AMISTD_2:def 19 :: thesis: I is IC-relocable
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 k being natural number st I = SCM-goto k or ex a being Data-Location ex k being natural number st I = a =0_goto k or ex a being Data-Location ex k being natural number st I = a >0_goto k ) by AMI_3:69;
suppose A1: ex k being natural number st I = SCM-goto k ; :: thesis: I is IC-relocable
let j, k be Nat; :: 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; :: thesis: (IC (Exec ((IncAddr (I,j)),s1))) + k = IC (Exec ((IncAddr (I,(j + k))),(IncIC (s1,k))))
set s2 = IncIC (s1,k);
consider k1 being natural number such that
A2: I = SCM-goto k1 by A1;
reconsider i1 = k1 as Element of NAT by ORDINAL1:def 13;
IC (Exec (I,s1)) = k1 by A2, AMI_3:13;
hence (IC (Exec ((IncAddr (I,j)),s1))) + k = (IC (Exec ((SCM-goto (j + k1)),s1))) + k by A2, Th59
.= (j + k1) + k by AMI_3:13
.= IC (Exec ((SCM-goto ((j + i1) + k)),(IncIC (s1,k)))) by AMI_3:13
.= IC (Exec ((SCM-goto ((j + k) + i1)),(IncIC (s1,k))))
.= IC (Exec ((IncAddr (I,(j + k))),(IncIC (s1,k)))) by A2, Th59 ;
:: thesis: verum
end;
suppose ex a being Data-Location ex k being natural number st I = a =0_goto k ; :: thesis: I is IC-relocable
then consider a being Data-Location , k1 being natural number such that
A3: I = a =0_goto k1 ;
reconsider i1 = k1 as Element of NAT by ORDINAL1:def 13;
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; :: 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 AMI_5:20, 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;
now
per cases ( s1 . a = 0 or s1 . a <> 0 ) ;
suppose A5: s1 . a = 0 ; :: thesis: (IC (Exec ((IncAddr (I,j)),s1))) + k = IC (Exec ((IncAddr (I,(j + k))),(IncIC (s1,k))))
then IC (Exec (I,s1)) = k1 by A3, AMI_3:14;
hence (IC (Exec ((IncAddr (I,j)),s1))) + k = (IC (Exec ((a =0_goto (j + k1)),s1))) + k by A3, Th60
.= (j + k1) + k by A5, AMI_3:14
.= IC (Exec ((a =0_goto ((j + i1) + k)),(IncIC (s1,k)))) by A4, A5, AMI_3:14
.= IC (Exec ((a =0_goto ((j + k) + i1)),(IncIC (s1,k))))
.= IC (Exec ((IncAddr (I,(j + k))),(IncIC (s1,k)))) by A3, Th60 ;
:: thesis: verum
end;
suppose A6: s1 . a <> 0 ; :: 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, Th60;
A8: IncAddr (I,(j + k)) = a =0_goto (i1 + (j + k)) by A3, Th60;
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, AMI_3:14
.= ((IC s1) + 1) + k
.= succ (IC (IncIC (s1,k))) by A9
.= IC (Exec ((IncAddr (I,(j + k))),(IncIC (s1,k)))) by A8, A6, A4, AMI_3:14 ; :: thesis: verum
end;
end;
end;
hence (IC (Exec ((IncAddr (I,j)),s1))) + k = IC (Exec ((IncAddr (I,(j + k))),(IncIC (s1,k)))) ; :: thesis: verum
end;
suppose ex a being Data-Location ex k being natural number st I = a >0_goto k ; :: thesis: I is IC-relocable
then consider a being Data-Location , k1 being natural number such that
A10: I = a >0_goto k1 ;
reconsider i1 = k1 as Element of NAT by ORDINAL1:def 13;
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; :: 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 AMI_5:20, FUNCOP_1:19;
then not a in dom ((IC ) .--> ((IC s1) + k)) by TARSKI:def 1;
then A11: s1 . a = (IncIC (s1,k)) . a by FUNCT_4:12;
per cases ( s1 . a > 0 or s1 . a <= 0 ) ;
suppose A12: s1 . a > 0 ; :: thesis: (IC (Exec ((IncAddr (I,j)),s1))) + k = IC (Exec ((IncAddr (I,(j + k))),(IncIC (s1,k))))
then IC (Exec (I,s1)) = k1 by A10, AMI_3:15;
hence (IC (Exec ((IncAddr (I,j)),s1))) + k = (IC (Exec ((a >0_goto (j + k1)),s1))) + k by A10, Th61
.= (j + k1) + k by A12, AMI_3:15
.= IC (Exec ((a >0_goto ((j + i1) + k)),(IncIC (s1,k)))) by A11, A12, AMI_3:15
.= IC (Exec ((a >0_goto ((j + k) + i1)),(IncIC (s1,k))))
.= IC (Exec ((IncAddr (I,(j + k))),(IncIC (s1,k)))) by A10, Th61 ;
:: thesis: verum
end;
suppose A13: s1 . a <= 0 ; :: thesis: (IC (Exec ((IncAddr (I,j)),s1))) + k = IC (Exec ((IncAddr (I,(j + k))),(IncIC (s1,k))))
A14: IncAddr (I,j) = a >0_goto (i1 + j) by A10, Th61;
A15: IncAddr (I,(j + k)) = a >0_goto (i1 + (j + k)) by A10, Th61;
dom ((IC ) .--> ((IC s1) + k)) = {(IC )} by FUNCOP_1:19;
then IC in dom ((IC ) .--> ((IC s1) + k)) by TARSKI:def 1;
then A16: 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 A14, A13, AMI_3:15
.= ((IC s1) + 1) + k
.= succ (IC (IncIC (s1,k))) by A16
.= IC (Exec ((IncAddr (I,(j + k))),(IncIC (s1,k)))) by A15, A13, A11, AMI_3:15 ; :: thesis: verum
end;
end;
end;
end;
end;
let I be Instruction of SCM; :: according to AMISTD_2:def 21 :: thesis: I is Exec-preserving
let s1, s2 be State of SCM; :: according to AMISTD_2:def 20 :: thesis: ( not NPP s1 = NPP s2 or NPP (Exec (I,s1)) = NPP (Exec (I,s2)) )
assume A17: NPP s1 = NPP s2 ; :: thesis: NPP (Exec (I,s1)) = NPP (Exec (I,s2))
A18: IC s1 = IC s2 by A17, COMPOS_1:230;
A19: dom (Exec (I,s1)) = the carrier of SCM by PARTFUN1:def 4;
then A20: dom (Exec (I,s1)) = dom (Exec (I,s2)) by PARTFUN1:def 4;
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 k being natural number st I = SCM-goto k or ex a being Data-Location ex k being natural number st I = a =0_goto k or ex a being Data-Location ex k being natural number st I = a >0_goto k ) by AMI_3:69;
suppose I = [0,{},{}] ; :: thesis: NPP (Exec (I,s1)) = NPP (Exec (I,s2))
hence NPP (Exec (I,s1)) = NPP (Exec (I,s2)) by A17, AMISTD_2:def 20, AMI_3:71; :: thesis: verum
end;
suppose ex a, b being Data-Location st I = a := b ; :: thesis: NPP (Exec (I,s1)) = NPP (Exec (I,s2))
then consider a, b being Data-Location such that
A21: 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 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 & x <> a ) ) by A19, A22, A23, Th3;
suppose A24: x = IC ; :: thesis: (Exec (I,s1)) . x = (Exec (I,s2)) . x
hence (Exec (I,s1)) . x = succ (IC s1) by A21, AMI_3:8
.= (Exec (I,s2)) . x by A18, A21, A24, AMI_3:8 ;
:: thesis: verum
end;
suppose A25: x = a ; :: thesis: (Exec (I,s1)) . x = (Exec (I,s2)) . x
hence (Exec (I,s1)) . x = s1 . b by A21, AMI_3:8
.= s2 . b by A17, Th5
.= (Exec (I,s2)) . x by A21, A25, AMI_3:8 ;
:: thesis: verum
end;
suppose that A26: x is Data-Location and
A27: x <> a ; :: thesis: (Exec (I,s1)) . x = (Exec (I,s2)) . x
thus (Exec (I,s1)) . x = s1 . x by A21, A26, A27, AMI_3:8
.= s2 . x by A17, A26, Th5
.= (Exec (I,s2)) . x by A21, A26, A27, AMI_3:8 ; :: thesis: verum
end;
end;
end;
then (Exec (I,s1)) | ((dom (Exec (I,s1))) \ NAT) = (Exec (I,s2)) | ((dom (Exec (I,s2))) \ NAT) by A20, FUNCT_1:165;
hence NPP (Exec (I,s1)) = NPP (Exec (I,s2)) by COMPOS_1:233; :: thesis: verum
end;
suppose ex a, b being Data-Location st I = AddTo (a,b) ; :: thesis: NPP (Exec (I,s1)) = NPP (Exec (I,s2))
then consider a, b being Data-Location such that
A28: 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 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 & x <> a ) ) by A19, A29, A30, Th3;
suppose A31: x = IC ; :: thesis: (Exec (I,s1)) . x = (Exec (I,s2)) . x
hence (Exec (I,s1)) . x = succ (IC s1) by A28, AMI_3:9
.= (Exec (I,s2)) . x by A18, A28, A31, AMI_3:9 ;
:: 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, AMI_3:9
.= (s1 . a) + (s2 . b) by A17, Th5
.= (s2 . a) + (s2 . b) by A17, Th5
.= (Exec (I,s2)) . x by A28, A32, AMI_3:9 ;
:: 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:9
.= s2 . x by A17, A33, Th5
.= (Exec (I,s2)) . x by A28, A33, A34, AMI_3:9 ; :: thesis: verum
end;
end;
end;
then (Exec (I,s1)) | ((dom (Exec (I,s1))) \ NAT) = (Exec (I,s2)) | ((dom (Exec (I,s2))) \ NAT) by A20, FUNCT_1:165;
hence NPP (Exec (I,s1)) = NPP (Exec (I,s2)) by COMPOS_1:233; :: thesis: verum
end;
suppose ex a, b being Data-Location st I = SubFrom (a,b) ; :: thesis: NPP (Exec (I,s1)) = NPP (Exec (I,s2))
then consider a, b being Data-Location such that
A35: 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 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 & x <> a ) ) by A19, A36, A37, Th3;
suppose A38: x = IC ; :: thesis: (Exec (I,s1)) . x = (Exec (I,s2)) . x
hence (Exec (I,s1)) . x = succ (IC s1) by A35, AMI_3:10
.= (Exec (I,s2)) . x by A18, A35, A38, AMI_3:10 ;
:: 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:10
.= (s1 . a) - (s2 . b) by A17, Th5
.= (s2 . a) - (s2 . b) by A17, Th5
.= (Exec (I,s2)) . x by A35, A39, AMI_3:10 ;
:: 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:10
.= s2 . x by A17, A40, Th5
.= (Exec (I,s2)) . x by A35, A40, A41, AMI_3:10 ; :: thesis: verum
end;
end;
end;
then (Exec (I,s1)) | ((dom (Exec (I,s1))) \ NAT) = (Exec (I,s2)) | ((dom (Exec (I,s2))) \ NAT) by A20, FUNCT_1:165;
hence NPP (Exec (I,s1)) = NPP (Exec (I,s2)) by COMPOS_1:233; :: thesis: verum
end;
suppose ex a, b being Data-Location st I = MultBy (a,b) ; :: thesis: NPP (Exec (I,s1)) = NPP (Exec (I,s2))
then consider a, b being Data-Location such that
A42: 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 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 = a or ( x is Data-Location & x <> a ) ) by A19, A43, A44, Th3;
suppose A45: x = IC ; :: thesis: (Exec (I,s1)) . x = (Exec (I,s2)) . x
hence (Exec (I,s1)) . x = succ (IC s1) by A42, AMI_3:11
.= (Exec (I,s2)) . x by A18, A42, A45, AMI_3:11 ;
:: 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:11
.= (s1 . a) * (s2 . b) by A17, Th5
.= (s2 . a) * (s2 . b) by A17, Th5
.= (Exec (I,s2)) . x by A42, A46, AMI_3:11 ;
:: 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:11
.= s2 . x by A17, A47, Th5
.= (Exec (I,s2)) . x by A42, A47, A48, AMI_3:11 ; :: thesis: verum
end;
end;
end;
then (Exec (I,s1)) | ((dom (Exec (I,s1))) \ NAT) = (Exec (I,s2)) | ((dom (Exec (I,s2))) \ NAT) by A20, FUNCT_1:165;
hence NPP (Exec (I,s1)) = NPP (Exec (I,s2)) by COMPOS_1:233; :: thesis: verum
end;
suppose ex a, b being Data-Location st I = Divide (a,b) ; :: thesis: NPP (Exec (I,s1)) = NPP (Exec (I,s2))
then consider a, b being Data-Location such that
A49: 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 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 or x is Data-Location ) by A19, A50, A51, Th3;
suppose A52: x = IC ; :: thesis: (Exec (I,s1)) . x = (Exec (I,s2)) . x
hence (Exec (I,s1)) . x = succ (IC s1) by A49, AMI_3:12
.= (Exec (I,s2)) . x by A18, A49, A52, AMI_3:12 ;
:: thesis: verum
end;
suppose A53: x is Data-Location ; :: thesis: (Exec (I,s1)) . x = (Exec (I,s2)) . x
A54: ( s1 . a = s2 . a & s1 . b = s2 . b ) by A17, Th5;
now
let c be Data-Location ; :: thesis: (Exec (I,s1)) . b1 = (Exec (I,s2)) . b1
per cases ( c = b or ( c = a & c <> b ) or ( c <> a & c <> b ) ) ;
suppose A55: c = b ; :: thesis: (Exec (I,s1)) . b1 = (Exec (I,s2)) . b1
hence (Exec (I,s1)) . c = (s2 . a) mod (s2 . b) by A49, A54, AMI_3:12
.= (Exec (I,s2)) . c by A49, A55, AMI_3:12 ;
:: thesis: verum
end;
suppose A56: ( c = a & c <> b ) ; :: thesis: (Exec (I,s1)) . b1 = (Exec (I,s2)) . b1
hence (Exec (I,s1)) . c = (s2 . a) div (s2 . b) by A49, A54, AMI_3:12
.= (Exec (I,s2)) . c by A49, A56, AMI_3:12 ;
:: thesis: verum
end;
suppose A57: ( c <> a & c <> b ) ; :: thesis: (Exec (I,s1)) . b1 = (Exec (I,s2)) . b1
hence (Exec (I,s1)) . c = s1 . c by A49, AMI_3:12
.= s2 . c by A17, Th5
.= (Exec (I,s2)) . c by A49, A57, AMI_3:12 ;
:: thesis: verum
end;
end;
end;
hence (Exec (I,s1)) . x = (Exec (I,s2)) . x by A53; :: thesis: verum
end;
end;
end;
then (Exec (I,s1)) | ((dom (Exec (I,s1))) \ NAT) = (Exec (I,s2)) | ((dom (Exec (I,s2))) \ NAT) by A20, FUNCT_1:165;
hence NPP (Exec (I,s1)) = NPP (Exec (I,s2)) by COMPOS_1:233; :: thesis: verum
end;
suppose ex k being natural number st I = SCM-goto k ; :: thesis: NPP (Exec (I,s1)) = NPP (Exec (I,s2))
then consider k1 being natural number such that
A58: I = SCM-goto k1 ;
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 A59: x in (dom (Exec (I,s1))) \ NAT ; :: thesis: (Exec (I,s1)) . x = (Exec (I,s2)) . x
then A60: not x in NAT by XBOOLE_0:def 5;
per cases ( x = IC or x is Data-Location ) by A19, A59, A60, Th3;
suppose A61: x = IC ; :: thesis: (Exec (I,s1)) . x = (Exec (I,s2)) . x
hence (Exec (I,s1)) . x = k1 by A58, AMI_3:13
.= (Exec (I,s2)) . x by A58, A61, AMI_3:13 ;
:: thesis: verum
end;
suppose A62: x is Data-Location ; :: thesis: (Exec (I,s1)) . x = (Exec (I,s2)) . x
hence (Exec (I,s1)) . x = s1 . x by A58, AMI_3:13
.= s2 . x by A17, A62, Th5
.= (Exec (I,s2)) . x by A58, A62, AMI_3:13 ;
:: thesis: verum
end;
end;
end;
then (Exec (I,s1)) | ((dom (Exec (I,s1))) \ NAT) = (Exec (I,s2)) | ((dom (Exec (I,s2))) \ NAT) by A20, FUNCT_1:165;
hence NPP (Exec (I,s1)) = NPP (Exec (I,s2)) by COMPOS_1:233; :: thesis: verum
end;
suppose ex a being Data-Location ex k being natural number st I = a =0_goto k ; :: thesis: NPP (Exec (I,s1)) = NPP (Exec (I,s2))
then consider a being Data-Location , k1 being natural number such that
A63: I = a =0_goto k1 ;
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 A64: x in (dom (Exec (I,s1))) \ NAT ; :: thesis: (Exec (I,s1)) . x = (Exec (I,s2)) . x
then A65: not x in NAT by XBOOLE_0:def 5;
A66: s1 . a = s2 . a by A17, Th5;
per cases ( ( x = IC & s1 . a = 0 ) or ( x = IC & s1 . a <> 0 ) or x is Data-Location ) by A19, A64, A65, Th3;
suppose A67: ( x = IC & s1 . a = 0 ) ; :: thesis: (Exec (I,s1)) . x = (Exec (I,s2)) . x
thus (Exec (I,s1)) . x = k1 by A63, A67, AMI_3:14
.= (Exec (I,s2)) . x by A63, A66, A67, AMI_3:14 ; :: thesis: verum
end;
suppose A68: ( x = IC & s1 . a <> 0 ) ; :: thesis: (Exec (I,s1)) . x = (Exec (I,s2)) . x
thus (Exec (I,s1)) . x = succ (IC s1) by A63, A68, AMI_3:14
.= (Exec (I,s2)) . x by A18, A63, A66, A68, AMI_3:14 ; :: 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 A63, AMI_3:14
.= s2 . x by A17, A69, Th5
.= (Exec (I,s2)) . x by A63, A69, AMI_3:14 ;
:: thesis: verum
end;
end;
end;
then (Exec (I,s1)) | ((dom (Exec (I,s1))) \ NAT) = (Exec (I,s2)) | ((dom (Exec (I,s2))) \ NAT) by A20, FUNCT_1:165;
hence NPP (Exec (I,s1)) = NPP (Exec (I,s2)) by COMPOS_1:233; :: thesis: verum
end;
suppose ex a being Data-Location ex k being natural number st I = a >0_goto k ; :: thesis: NPP (Exec (I,s1)) = NPP (Exec (I,s2))
then consider a being Data-Location , k being natural number such that
A70: I = a >0_goto k ;
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 A17, Th5;
per cases ( ( x = IC & s1 . a > 0 ) or ( x = IC & s1 . a <= 0 ) or x is Data-Location ) by A19, A71, A72, Th3;
suppose A74: ( x = IC & s1 . a > 0 ) ; :: thesis: (Exec (I,s1)) . x = (Exec (I,s2)) . x
thus (Exec (I,s1)) . x = k by A70, A74, AMI_3:15
.= (Exec (I,s2)) . x by A70, A73, A74, AMI_3:15 ; :: thesis: verum
end;
suppose A75: ( x = IC & s1 . a <= 0 ) ; :: thesis: (Exec (I,s1)) . x = (Exec (I,s2)) . x
thus (Exec (I,s1)) . x = succ (IC s1) by A70, A75, AMI_3:15
.= (Exec (I,s2)) . x by A18, A70, A73, A75, AMI_3:15 ; :: thesis: verum
end;
suppose A76: x is Data-Location ; :: thesis: (Exec (I,s1)) . x = (Exec (I,s2)) . x
hence (Exec (I,s1)) . x = s1 . x by A70, AMI_3:15
.= s2 . x by A17, A76, Th5
.= (Exec (I,s2)) . x by A70, A76, AMI_3:15 ;
:: thesis: verum
end;
end;
end;
then (Exec (I,s1)) | ((dom (Exec (I,s1))) \ NAT) = (Exec (I,s2)) | ((dom (Exec (I,s2))) \ NAT) by A20, FUNCT_1:165;
hence NPP (Exec (I,s1)) = NPP (Exec (I,s2)) by COMPOS_1:233; :: thesis: verum
end;
end;