let k be natural number ; :: thesis: for R being good Ring
for p being FinPartState of (SCM R) st not R is trivial & IC (SCM R) in dom p holds
( p is autonomic iff Relocated p,k is autonomic )
let R be good Ring; :: thesis: for p being FinPartState of (SCM R) st not R is trivial & IC (SCM R) in dom p holds
( p is autonomic iff Relocated p,k is autonomic )
let p be FinPartState of (SCM R); :: thesis: ( not R is trivial & IC (SCM R) in dom p implies ( p is autonomic iff Relocated p,k is autonomic ) )
assume that
A1:
not R is trivial
and
A2:
IC (SCM R) in dom p
; :: thesis: ( p is autonomic iff Relocated p,k is autonomic )
hereby :: thesis: ( Relocated p,k is autonomic implies p is autonomic )
assume A3:
p is
autonomic
;
:: thesis: Relocated p,k is autonomic thus
Relocated p,
k is
autonomic
:: thesis: verumproof
let s1,
s2 be
State of
(SCM R);
:: according to AMI_1:def 25 :: thesis: ( not Relocated p,k c= s1 or not Relocated p,k c= s2 or for b1 being Element of NAT holds (Computation s1,b1) | (dom (Relocated p,k)) = (Computation s2,b1) | (dom (Relocated p,k)) )
assume A4:
(
Relocated p,
k c= s1 &
Relocated p,
k c= s2 )
;
:: thesis: for b1 being Element of NAT holds (Computation s1,b1) | (dom (Relocated p,k)) = (Computation s2,b1) | (dom (Relocated p,k))
let i be
Element of
NAT ;
:: thesis: (Computation s1,i) | (dom (Relocated p,k)) = (Computation s2,i) | (dom (Relocated p,k))
A5:
Computation s1,
i = (((Computation (s1 +* p),i) +* (Start-At ((IC (Computation (s1 +* p),i)) + k))) +* (s1 | (dom (ProgramPart p)))) +* (ProgramPart (Relocated p,k))
by A1, A2, A3, A4, Th62;
A6:
Computation s2,
i = (((Computation (s2 +* p),i) +* (Start-At ((IC (Computation (s2 +* p),i)) + k))) +* (s2 | (dom (ProgramPart p)))) +* (ProgramPart (Relocated p,k))
by A1, A2, A3, A4, Th62;
(
p c= s1 +* p &
p c= s2 +* p )
by FUNCT_4:26;
then A7:
(Computation (s1 +* p),i) | (dom p) = (Computation (s2 +* p),i) | (dom p)
by A3, AMI_1:def 25;
A8:
dom (Start-At ((IC p) + k)) = {(IC (SCM R))}
by FUNCOP_1:19;
A9:
dom (Start-At ((IC (Computation (s1 +* p),i)) + k)) = {(IC (SCM R))}
by FUNCOP_1:19;
A10:
dom (Start-At ((IC (Computation (s2 +* p),i)) + k)) = {(IC (SCM R))}
by FUNCOP_1:19;
A11:
{(IC (SCM R))} c= dom p
by A2, ZFMISC_1:37;
A12:
Start-At (IC (Computation (s1 +* p),i)) =
(Computation (s1 +* p),i) | {(IC (SCM R))}
by AMI_1:95
.=
(Computation (s2 +* p),i) | {(IC (SCM R))}
by A7, A11, RELAT_1:188
.=
Start-At (IC (Computation (s2 +* p),i))
by AMI_1:95
;
A13:
dom (Start-At ((IC p) + k)) misses dom (ProgramPart (Relocated p,k))
by A8, AMI_1:103;
dom [(ProgramPart p)] c= the
carrier of
(SCM R)
by AMI_1:80;
then
dom (ProgramPart p) c= dom s1
by AMI_1:79;
then A14:
dom (s1 | (dom (ProgramPart p))) = dom (ProgramPart p)
by RELAT_1:91;
dom [(ProgramPart p)] c= the
carrier of
(SCM R)
by AMI_1:80;
then
dom (ProgramPart p) c= dom s2
by AMI_1:79;
then A15:
dom (s2 | (dom (ProgramPart p))) = dom (ProgramPart p)
by RELAT_1:91;
A16:
(Computation s1,i) | (dom (Start-At ((IC p) + k))) =
(((Computation (s1 +* p),i) +* (Start-At ((IC (Computation (s1 +* p),i)) + k))) +* (s1 | (dom (ProgramPart p)))) | (dom (Start-At ((IC p) + k)))
by A5, A13, FUNCT_4:76
.=
((Computation (s1 +* p),i) +* (Start-At ((IC (Computation (s1 +* p),i)) + k))) | (dom (Start-At ((IC p) + k)))
by A8, A14, AMI_1:103, FUNCT_4:76
.=
Start-At ((IC (Computation (s1 +* p),i)) + k)
by A8, A9, FUNCT_4:24
.=
Start-At ((IC (Computation (s2 +* p),i)) + k)
by A12, AMISTD_1:63
.=
((Computation (s2 +* p),i) +* (Start-At ((IC (Computation (s2 +* p),i)) + k))) | (dom (Start-At ((IC p) + k)))
by A8, A10, FUNCT_4:24
.=
(((Computation (s2 +* p),i) +* (Start-At ((IC (Computation (s2 +* p),i)) + k))) +* (s2 | (dom (ProgramPart p)))) | (dom (Start-At ((IC p) + k)))
by A8, A15, AMI_1:103, FUNCT_4:76
.=
(Computation s2,i) | (dom (Start-At ((IC p) + k)))
by A6, A13, FUNCT_4:76
;
A17:
(Computation s1,i) | (dom (IncAddr (Shift [(ProgramPart p)],k),k)) =
(Computation s1,i) | (dom (ProgramPart (Relocated p,k)))
by AMISTD_2:69
.=
ProgramPart (Relocated p,k)
by A5, FUNCT_4:24
.=
(Computation s2,i) | (dom (ProgramPart (Relocated p,k)))
by A6, FUNCT_4:24
.=
(Computation s2,i) | (dom (IncAddr (Shift [(ProgramPart p)],k),k))
by AMISTD_2:69
;
DataPart p c= p
by RELAT_1:88;
then A18:
dom (DataPart p) c= dom p
by GRFUNC_1:8;
A19:
dom (DataPart p) misses dom (ProgramPart (Relocated p,k))
by AMI_1:104;
A20:
dom (DataPart p) misses dom (Start-At ((IC (Computation (s1 +* p),i)) + k))
by A9, AMI_1:102;
A21:
dom (DataPart p) misses dom (Start-At ((IC (Computation (s2 +* p),i)) + k))
by A10, AMI_1:102;
A22:
(Computation s1,i) | (dom (DataPart p)) =
(((Computation (s1 +* p),i) +* (Start-At ((IC (Computation (s1 +* p),i)) + k))) +* (s1 | (dom (ProgramPart p)))) | (dom (DataPart p))
by A5, A19, FUNCT_4:76
.=
((Computation (s1 +* p),i) +* (Start-At ((IC (Computation (s1 +* p),i)) + k))) | (dom (DataPart p))
by A14, AMI_1:104, FUNCT_4:76
.=
(Computation (s1 +* p),i) | (dom (DataPart p))
by A20, FUNCT_4:76
.=
(Computation (s2 +* p),i) | (dom (DataPart p))
by A7, A18, RELAT_1:188
.=
((Computation (s2 +* p),i) +* (Start-At ((IC (Computation (s2 +* p),i)) + k))) | (dom (DataPart p))
by A21, FUNCT_4:76
.=
(((Computation (s2 +* p),i) +* (Start-At ((IC (Computation (s2 +* p),i)) + k))) +* (s2 | (dom (ProgramPart p)))) | (dom (DataPart p))
by A15, AMI_1:104, FUNCT_4:76
.=
(Computation s2,i) | (dom (DataPart p))
by A6, A19, FUNCT_4:76
;
A23:
(Computation s1,i) | (dom ((Start-At ((IC p) + k)) +* (IncAddr (Shift [(ProgramPart p)],k),k))) =
(Computation s1,i) | ((dom (Start-At ((IC p) + k))) \/ (dom (IncAddr (Shift [(ProgramPart p)],k),k)))
by FUNCT_4:def 1
.=
((Computation s2,i) | (dom (Start-At ((IC p) + k)))) \/ ((Computation s2,i) | (dom (IncAddr (Shift [(ProgramPart p)],k),k)))
by A16, A17, RELAT_1:107
.=
(Computation s2,i) | ((dom (Start-At ((IC p) + k))) \/ (dom (IncAddr (Shift [(ProgramPart p)],k),k)))
by RELAT_1:107
.=
(Computation s2,i) | (dom ((Start-At ((IC p) + k)) +* (IncAddr (Shift [(ProgramPart p)],k),k)))
by FUNCT_4:def 1
;
thus (Computation s1,i) | (dom (Relocated p,k)) =
(Computation s1,i) | ((dom ((Start-At ((IC p) + k)) +* (IncAddr (Shift [(ProgramPart p)],k),k))) \/ (dom (DataPart p)))
by FUNCT_4:def 1
.=
((Computation s2,i) | (dom ((Start-At ((IC p) + k)) +* (IncAddr (Shift [(ProgramPart p)],k),k)))) \/ ((Computation s2,i) | (dom (DataPart p)))
by A22, A23, RELAT_1:107
.=
(Computation s2,i) | ((dom ((Start-At ((IC p) + k)) +* (IncAddr (Shift [(ProgramPart p)],k),k))) \/ (dom (DataPart p)))
by RELAT_1:107
.=
(Computation s2,i) | (dom (Relocated p,k))
by FUNCT_4:def 1
;
:: thesis: verum
end;
end;
assume A24:
Relocated p,k is autonomic
; :: thesis: p is autonomic
let s1, s2 be State of (SCM R); :: according to AMI_1:def 25 :: thesis: ( not p c= s1 or not p c= s2 or for b1 being Element of NAT holds (Computation s1,b1) | (dom p) = (Computation s2,b1) | (dom p) )
assume A25:
( p c= s1 & p c= s2 )
; :: thesis: for b1 being Element of NAT holds (Computation s1,b1) | (dom p) = (Computation s2,b1) | (dom p)
let i be Element of NAT ; :: thesis: (Computation s1,i) | (dom p) = (Computation s2,i) | (dom p)
A26:
Computation s1,i = (((Computation (s1 +* (Relocated p,k)),i) +* (Start-At ((IC (Computation (s1 +* (Relocated p,k)),i)) -' k))) +* (s1 | (dom (ProgramPart (Relocated p,k))))) +* (ProgramPart p)
by A1, A2, A24, A25, Th63;
A27:
Computation s2,i = (((Computation (s2 +* (Relocated p,k)),i) +* (Start-At ((IC (Computation (s2 +* (Relocated p,k)),i)) -' k))) +* (s2 | (dom (ProgramPart (Relocated p,k))))) +* (ProgramPart p)
by A1, A2, A24, A25, Th63;
( Relocated p,k c= s1 +* (Relocated p,k) & Relocated p,k c= s2 +* (Relocated p,k) )
by FUNCT_4:26;
then A28:
(Computation (s1 +* (Relocated p,k)),i) | (dom (Relocated p,k)) = (Computation (s2 +* (Relocated p,k)),i) | (dom (Relocated p,k))
by A24, AMI_1:def 25;
A29:
dom (Start-At (IC p)) = {(IC (SCM R))}
by FUNCOP_1:19;
A30:
dom (Start-At ((IC (Computation (s1 +* (Relocated p,k)),i)) -' k)) = {(IC (SCM R))}
by FUNCOP_1:19;
A31:
dom (Start-At ((IC (Computation (s2 +* (Relocated p,k)),i)) -' k)) = {(IC (SCM R))}
by FUNCOP_1:19;
IC (SCM R) in dom (Relocated p,k)
by AMISTD_2:72;
then A32:
{(IC (SCM R))} c= dom (Relocated p,k)
by ZFMISC_1:37;
A33: Start-At (IC (Computation (s1 +* (Relocated p,k)),i)) =
(Computation (s1 +* (Relocated p,k)),i) | {(IC (SCM R))}
by AMI_1:95
.=
(Computation (s2 +* (Relocated p,k)),i) | {(IC (SCM R))}
by A28, A32, RELAT_1:188
.=
Start-At (IC (Computation (s2 +* (Relocated p,k)),i))
by AMI_1:95
;
A34:
dom (Start-At (IC p)) misses dom (ProgramPart p)
by A29, AMI_1:103;
dom [(ProgramPart (Relocated p,k))] c= the carrier of (SCM R)
by AMI_1:80;
then
dom (ProgramPart (Relocated p,k)) c= dom s1
by AMI_1:79;
then A35:
dom (s1 | (dom (ProgramPart (Relocated p,k)))) = dom (ProgramPart (Relocated p,k))
by RELAT_1:91;
dom [(ProgramPart (Relocated p,k))] c= the carrier of (SCM R)
by AMI_1:80;
then
dom (ProgramPart (Relocated p,k)) c= dom s2
by AMI_1:79;
then A36:
dom (s2 | (dom (ProgramPart (Relocated p,k)))) = dom (ProgramPart (Relocated p,k))
by RELAT_1:91;
A37: (Computation s1,i) | (dom (Start-At (IC p))) =
(((Computation (s1 +* (Relocated p,k)),i) +* (Start-At ((IC (Computation (s1 +* (Relocated p,k)),i)) -' k))) +* (s1 | (dom (ProgramPart (Relocated p,k))))) | (dom (Start-At (IC p)))
by A26, A34, FUNCT_4:76
.=
((Computation (s1 +* (Relocated p,k)),i) +* (Start-At ((IC (Computation (s1 +* (Relocated p,k)),i)) -' k))) | (dom (Start-At (IC p)))
by A29, A35, AMI_1:103, FUNCT_4:76
.=
Start-At ((IC (Computation (s1 +* (Relocated p,k)),i)) -' k)
by A29, A30, FUNCT_4:24
.=
Start-At ((IC (Computation (s2 +* (Relocated p,k)),i)) -' k)
by A33, AMISTD_1:64
.=
((Computation (s2 +* (Relocated p,k)),i) +* (Start-At ((IC (Computation (s2 +* (Relocated p,k)),i)) -' k))) | (dom (Start-At (IC p)))
by A29, A31, FUNCT_4:24
.=
(((Computation (s2 +* (Relocated p,k)),i) +* (Start-At ((IC (Computation (s2 +* (Relocated p,k)),i)) -' k))) +* (s2 | (dom (ProgramPart (Relocated p,k))))) | (dom (Start-At (IC p)))
by A29, A36, AMI_1:103, FUNCT_4:76
.=
(Computation s2,i) | (dom (Start-At (IC p)))
by A27, A34, FUNCT_4:76
;
A38: (Computation s1,i) | (dom (ProgramPart p)) =
ProgramPart p
by A26, FUNCT_4:24
.=
(Computation s2,i) | (dom (ProgramPart p))
by A27, FUNCT_4:24
;
DataPart (Relocated p,k) c= Relocated p,k
by RELAT_1:88;
then
DataPart p c= Relocated p,k
by AMISTD_2:68;
then A39:
dom (DataPart p) c= dom (Relocated p,k)
by GRFUNC_1:8;
A40:
dom (DataPart p) misses dom (ProgramPart p)
by AMI_1:104;
A41:
dom (DataPart p) misses dom (Start-At ((IC (Computation (s1 +* (Relocated p,k)),i)) -' k))
by A30, AMI_1:102;
A42:
dom (DataPart p) misses dom (Start-At ((IC (Computation (s2 +* (Relocated p,k)),i)) -' k))
by A31, AMI_1:102;
A43: (Computation s1,i) | (dom (DataPart p)) =
(((Computation (s1 +* (Relocated p,k)),i) +* (Start-At ((IC (Computation (s1 +* (Relocated p,k)),i)) -' k))) +* (s1 | (dom (ProgramPart (Relocated p,k))))) | (dom (DataPart p))
by A26, A40, FUNCT_4:76
.=
((Computation (s1 +* (Relocated p,k)),i) +* (Start-At ((IC (Computation (s1 +* (Relocated p,k)),i)) -' k))) | (dom (DataPart p))
by A35, AMI_1:104, FUNCT_4:76
.=
(Computation (s1 +* (Relocated p,k)),i) | (dom (DataPart p))
by A41, FUNCT_4:76
.=
(Computation (s2 +* (Relocated p,k)),i) | (dom (DataPart p))
by A28, A39, RELAT_1:188
.=
((Computation (s2 +* (Relocated p,k)),i) +* (Start-At ((IC (Computation (s2 +* (Relocated p,k)),i)) -' k))) | (dom (DataPart p))
by A42, FUNCT_4:76
.=
(((Computation (s2 +* (Relocated p,k)),i) +* (Start-At ((IC (Computation (s2 +* (Relocated p,k)),i)) -' k))) +* (s2 | (dom (ProgramPart (Relocated p,k))))) | (dom (DataPart p))
by A36, AMI_1:104, FUNCT_4:76
.=
(Computation s2,i) | (dom (DataPart p))
by A27, A40, FUNCT_4:76
;
A44: (Computation s1,i) | (dom ((Start-At (IC p)) +* (ProgramPart p))) =
(Computation s1,i) | ((dom (Start-At (IC p))) \/ (dom (ProgramPart p)))
by FUNCT_4:def 1
.=
((Computation s2,i) | (dom (Start-At (IC p)))) \/ ((Computation s2,i) | (dom (ProgramPart p)))
by A37, A38, RELAT_1:107
.=
(Computation s2,i) | ((dom (Start-At (IC p))) \/ (dom (ProgramPart p)))
by RELAT_1:107
.=
(Computation s2,i) | (dom ((Start-At (IC p)) +* (ProgramPart p)))
by FUNCT_4:def 1
;
thus (Computation s1,i) | (dom p) =
(Computation s1,i) | (dom (((Start-At (IC p)) +* (ProgramPart p)) +* (DataPart p)))
by A2, AMI_1:108
.=
(Computation s1,i) | ((dom ((Start-At (IC p)) +* (ProgramPart p))) \/ (dom (DataPart p)))
by FUNCT_4:def 1
.=
((Computation s2,i) | (dom ((Start-At (IC p)) +* (ProgramPart p)))) \/ ((Computation s2,i) | (dom (DataPart p)))
by A43, A44, RELAT_1:107
.=
(Computation s2,i) | ((dom ((Start-At (IC p)) +* (ProgramPart p))) \/ (dom (DataPart p)))
by RELAT_1:107
.=
(Computation s2,i) | (dom (((Start-At (IC p)) +* (ProgramPart p)) +* (DataPart p)))
by FUNCT_4:def 1
.=
(Computation s2,i) | (dom p)
by A2, AMI_1:108
; :: thesis: verum