let k be Element of NAT ; :: 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: verum

proof

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 b₁ being Element of NAT holds (Comput (ProgramPart s1),s1,b₁) | (proj1 (Relocated p,k)) = (Comput (ProgramPart s2),s2,b₁) | (proj1 (Relocated p,k)) )
assume that
A4: Relocated p,k c= s1 and
A5: Relocated p,k c= s2 ; :: thesis: for b₁ being Element of NAT holds (Comput (ProgramPart s1),s1,b₁) | (proj1 (Relocated p,k)) = (Comput (ProgramPart s2),s2,b₁) | (proj1 (Relocated p,k))
let i be Element of NAT ; :: thesis: (Comput (ProgramPart s1),s1,i) | (proj1 (Relocated p,k)) = (Comput (ProgramPart s2),s2,i) | (proj1 (Relocated p,k))
A6: Comput (ProgramPart s1),s1,i = (((Comput (ProgramPart (s1 +* p)),(s1 +* p),i) +* (Start-At ((IC (Comput (ProgramPart (s1 +* p)),(s1 +* p),i)) + k),(SCM R))) +* (s1 | (dom (ProgramPart p)))) +* (ProgramPart (Relocated p,k)) by A1, A2, A3, A4, Th38;
dom (ProgramPart p) c= the carrier of (SCM R) by RELAT_1:def 18;
then dom (ProgramPart p) c= dom s2 by PARTFUN1:def 4;
then A7: dom (s2 | (dom (ProgramPart p))) = dom (ProgramPart p) by RELAT_1:91;
dom (ProgramPart p) c= the carrier of (SCM R) by RELAT_1:def 18;
then dom (ProgramPart p) c= dom s1 by PARTFUN1:def 4;
then A8: dom (s1 | (dom (ProgramPart p))) = dom (ProgramPart p) by RELAT_1:91;
A9: dom (Start-At ((IC (Comput (ProgramPart (s2 +* p)),(s2 +* p),i)) + k),(SCM R)) = {(IC (SCM R))} by FUNCOP_1:19;
then A10: dom (DataPart p) misses dom (Start-At ((IC (Comput (ProgramPart (s2 +* p)),(s2 +* p),i)) + k),(SCM R)) by COMPOS_1:13;
A11: dom (Start-At ((IC (Comput (ProgramPart (s1 +* p)),(s1 +* p),i)) + k),(SCM R)) = {(IC (SCM R))} by FUNCOP_1:19;
then A12: dom (DataPart p) misses dom (Start-At ((IC (Comput (ProgramPart (s1 +* p)),(s1 +* p),i)) + k),(SCM R)) by COMPOS_1:13;
A13: Comput (ProgramPart s2),s2,i = (((Comput (ProgramPart (s2 +* p)),(s2 +* p),i) +* (Start-At ((IC (Comput (ProgramPart (s2 +* p)),(s2 +* p),i)) + k),(SCM R))) +* (s2 | (dom (ProgramPart p)))) +* (ProgramPart (Relocated p,k)) by A1, A2, A3, A5, Th38;
A14: (Comput (ProgramPart s1),s1,i) | (dom (IncAddr (Shift (ProgramPart p),k),k)) = (Comput (ProgramPart s1),s1,i) | (dom (ProgramPart (Relocated p,k))) by AMISTD_2:69
.= ProgramPart (Relocated p,k) by A6, FUNCT_4:24
.= (Comput (ProgramPart s2),s2,i) | (dom (ProgramPart (Relocated p,k))) by A13, FUNCT_4:24
.= (Comput (ProgramPart s2),s2,i) | (dom (IncAddr (Shift (ProgramPart p),k),k)) by AMISTD_2:69 ;
DataPart p c= p by RELAT_1:88;
then A15: dom (DataPart p) c= dom p by GRFUNC_1:8;
( p c= s1 +* p & p c= s2 +* p ) by FUNCT_4:26;
then A16: (Comput (ProgramPart (s1 +* p)),(s1 +* p),i) | (dom p) = (Comput (ProgramPart (s2 +* p)),(s2 +* p),i) | (dom p) by A3, AMI_1:def 25;
A17: dom (DataPart p) misses dom (ProgramPart (Relocated p,k)) by COMPOS_1:15;
then A18: (Comput (ProgramPart s1),s1,i) | (dom (DataPart p)) = (((Comput (ProgramPart (s1 +* p)),(s1 +* p),i) +* (Start-At ((IC (Comput (ProgramPart (s1 +* p)),(s1 +* p),i)) + k),(SCM R))) +* (s1 | (dom (ProgramPart p)))) | (dom (DataPart p)) by A6, FUNCT_4:76
.= ((Comput (ProgramPart (s1 +* p)),(s1 +* p),i) +* (Start-At ((IC (Comput (ProgramPart (s1 +* p)),(s1 +* p),i)) + k),(SCM R))) | (dom (DataPart p)) by A8, COMPOS_1:15, FUNCT_4:76
.= (Comput (ProgramPart (s1 +* p)),(s1 +* p),i) | (dom (DataPart p)) by A12, FUNCT_4:76
.= (Comput (ProgramPart (s2 +* p)),(s2 +* p),i) | (dom (DataPart p)) by A16, A15, RELAT_1:188
.= ((Comput (ProgramPart (s2 +* p)),(s2 +* p),i) +* (Start-At ((IC (Comput (ProgramPart (s2 +* p)),(s2 +* p),i)) + k),(SCM R))) | (dom (DataPart p)) by A10, FUNCT_4:76
.= (((Comput (ProgramPart (s2 +* p)),(s2 +* p),i) +* (Start-At ((IC (Comput (ProgramPart (s2 +* p)),(s2 +* p),i)) + k),(SCM R))) +* (s2 | (dom (ProgramPart p)))) | (dom (DataPart p)) by A7, COMPOS_1:15, FUNCT_4:76
.= (Comput (ProgramPart s2),s2,i) | (dom (DataPart p)) by A13, A17, FUNCT_4:76 ;
A19: {(IC (SCM R))} c= dom p by A2, ZFMISC_1:37;
A20: Start-At (IC (Comput (ProgramPart (s1 +* p)),(s1 +* p),i)),(SCM R) = (Comput (ProgramPart (s1 +* p)),(s1 +* p),i) | {(IC (SCM R))} by COMPOS_1:10
.= (Comput (ProgramPart (s2 +* p)),(s2 +* p),i) | {(IC (SCM R))} by A16, A19, RELAT_1:188
.= Start-At (IC (Comput (ProgramPart (s2 +* p)),(s2 +* p),i)),(SCM R) by COMPOS_1:10 ;
A21: dom (Start-At ((IC p) + k),(SCM R)) = {(IC (SCM R))} by FUNCOP_1:19;
then A22: dom (Start-At ((IC p) + k),(SCM R)) misses dom (ProgramPart (Relocated p,k)) by COMPOS_1:14;
then A23: (Comput (ProgramPart s1),s1,i) | (dom (Start-At ((IC p) + k),(SCM R))) = (((Comput (ProgramPart (s1 +* p)),(s1 +* p),i) +* (Start-At ((IC (Comput (ProgramPart (s1 +* p)),(s1 +* p),i)) + k),(SCM R))) +* (s1 | (dom (ProgramPart p)))) | (dom (Start-At ((IC p) + k),(SCM R))) by A6, FUNCT_4:76
.= ((Comput (ProgramPart (s1 +* p)),(s1 +* p),i) +* (Start-At ((IC (Comput (ProgramPart (s1 +* p)),(s1 +* p),i)) + k),(SCM R))) | (dom (Start-At ((IC p) + k),(SCM R))) by A21, A8, COMPOS_1:14, FUNCT_4:76
.= Start-At ((IC (Comput (ProgramPart (s1 +* p)),(s1 +* p),i)) + k),(SCM R) by A21, A11, FUNCT_4:24
.= Start-At ((IC (Comput (ProgramPart (s2 +* p)),(s2 +* p),i)) + k),(SCM R) by A20, COMPOS_1:43
.= ((Comput (ProgramPart (s2 +* p)),(s2 +* p),i) +* (Start-At ((IC (Comput (ProgramPart (s2 +* p)),(s2 +* p),i)) + k),(SCM R))) | (dom (Start-At ((IC p) + k),(SCM R))) by A21, A9, FUNCT_4:24
.= (((Comput (ProgramPart (s2 +* p)),(s2 +* p),i) +* (Start-At ((IC (Comput (ProgramPart (s2 +* p)),(s2 +* p),i)) + k),(SCM R))) +* (s2 | (dom (ProgramPart p)))) | (dom (Start-At ((IC p) + k),(SCM R))) by A21, A7, COMPOS_1:14, FUNCT_4:76
.= (Comput (ProgramPart s2),s2,i) | (dom (Start-At ((IC p) + k),(SCM R))) by A13, A22, FUNCT_4:76 ;
U2: dom (Start-At ((IC p) + k),(SCM R)) = {(IC (SCM R))} by FUNCOP_1:19;
U: dom (NPP p) = {(IC (SCM R))} \/ (dom (DataPart p)) by A2, COMPOS_1:70;
Y1: (Comput (ProgramPart s1),s1,i) | (dom (NPP p)) = ((Comput (ProgramPart s1),s1,i) | {(IC (SCM R))}) \/ ((Comput (ProgramPart s1),s1,i) | (dom (DataPart p))) by U, RELAT_1:107
.= (Comput (ProgramPart s2),s2,i) | (dom (NPP p)) by U, U2, A23, A18, RELAT_1:107 ;
Y: dom (IncrIC (NPP p),k) = (dom (NPP p)) \/ (dom (Start-At ((IC (NPP p)) + k),(SCM R))) by FUNCT_4:def 1
.= (dom (NPP p)) \/ (dom (Start-At ((IC p) + k),(SCM R))) by A2, COMPOS_1:72 ;
X1: (Comput (ProgramPart s1),s1,i) | (dom (IncrIC (NPP p),k)) = ((Comput (ProgramPart s1),s1,i) | (dom (NPP p))) \/ ((Comput (ProgramPart s1),s1,i) | (dom (Start-At ((IC p) + k),(SCM R)))) by Y, RELAT_1:107
.= (Comput (ProgramPart s2),s2,i) | (dom (IncrIC (NPP p),k)) by Y, Y1, A23, RELAT_1:107 ;
X: dom (Relocated p,k) = (dom (IncrIC (NPP p),k)) \/ (dom (Reloc (ProgramPart p),k)) by FUNCT_4:def 1;
hence (Comput (ProgramPart s1),s1,i) | (dom (Relocated p,k)) = ((Comput (ProgramPart s1),s1,i) | (dom (IncrIC (NPP p),k))) \/ ((Comput (ProgramPart s1),s1,i) | (dom (Reloc (ProgramPart p),k))) by RELAT_1:107
.= (Comput (ProgramPart s2),s2,i) | (dom (Relocated p,k)) by X1, A14, X, RELAT_1:107 ;
:: thesis: verum

end;

end;

assume A25: 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 b₁ being Element of NAT holds (Comput (ProgramPart s1),s1,b₁) | (proj1 p) = (Comput (ProgramPart s2),s2,b₁) | (proj1 p) )
assume that
A26: p c= s1 and
A27: p c= s2 ; :: thesis: for b₁ being Element of NAT holds (Comput (ProgramPart s1),s1,b₁) | (proj1 p) = (Comput (ProgramPart s2),s2,b₁) | (proj1 p)
let i be Element of NAT ; :: thesis: (Comput (ProgramPart s1),s1,i) | (proj1 p) = (Comput (ProgramPart s2),s2,i) | (proj1 p)
A28: Comput (ProgramPart s2),s2,i = (((Comput (ProgramPart (s2 +* (Relocated p,k))),(s2 +* (Relocated p,k)),i) +* (Start-At ((IC (Comput (ProgramPart (s2 +* (Relocated p,k))),(s2 +* (Relocated p,k)),i)) -' k),(SCM R))) +* (s2 | (dom (ProgramPart (Relocated p,k))))) +* (ProgramPart p) by A1, A2, A25, A27, Th39;
DataPart (Relocated p,k) c= Relocated p,k by RELAT_1:88;
then DataPart p c= Relocated p,k by AMISTD_2:68;
then A29: dom (DataPart p) c= dom (Relocated p,k) by GRFUNC_1:8;
A30: dom (Start-At ((IC (Comput (ProgramPart (s1 +* (Relocated p,k))),(s1 +* (Relocated p,k)),i)) -' k),(SCM R)) = {(IC (SCM R))} by FUNCOP_1:19;
then A31: dom (DataPart p) misses dom (Start-At ((IC (Comput (ProgramPart (s1 +* (Relocated p,k))),(s1 +* (Relocated p,k)),i)) -' k),(SCM R)) by COMPOS_1:13;
dom (ProgramPart (Relocated p,k)) c= the carrier of (SCM R) by RELAT_1:def 18;
then dom (ProgramPart (Relocated p,k)) c= dom s1 by PARTFUN1:def 4;
then A32: dom (s1 | (dom (ProgramPart (Relocated p,k)))) = dom (ProgramPart (Relocated p,k)) by RELAT_1:91;
A33: Comput (ProgramPart s1),s1,i = (((Comput (ProgramPart (s1 +* (Relocated p,k))),(s1 +* (Relocated p,k)),i) +* (Start-At ((IC (Comput (ProgramPart (s1 +* (Relocated p,k))),(s1 +* (Relocated p,k)),i)) -' k),(SCM R))) +* (s1 | (dom (ProgramPart (Relocated p,k))))) +* (ProgramPart p) by A1, A2, A25, A26, Th39;
then A34: (Comput (ProgramPart s1),s1,i) | (dom (ProgramPart p)) = ProgramPart p by FUNCT_4:24
.= (Comput (ProgramPart s2),s2,i) | (dom (ProgramPart p)) by A28, FUNCT_4:24 ;
( Relocated p,k c= s1 +* (Relocated p,k) & Relocated p,k c= s2 +* (Relocated p,k) ) by FUNCT_4:26;
then A35: (Comput (ProgramPart (s1 +* (Relocated p,k))),(s1 +* (Relocated p,k)),i) | (dom (Relocated p,k)) = (Comput (ProgramPart (s2 +* (Relocated p,k))),(s2 +* (Relocated p,k)),i) | (dom (Relocated p,k)) by A25, AMI_1:def 25;
dom (ProgramPart (Relocated p,k)) c= the carrier of (SCM R) by RELAT_1:def 18;
then dom (ProgramPart (Relocated p,k)) c= dom s2 by PARTFUN1:def 4;
then A36: dom (s2 | (dom (ProgramPart (Relocated p,k)))) = dom (ProgramPart (Relocated p,k)) by RELAT_1:91;
A37: dom (Start-At ((IC (Comput (ProgramPart (s2 +* (Relocated p,k))),(s2 +* (Relocated p,k)),i)) -' k),(SCM R)) = {(IC (SCM R))} by FUNCOP_1:19;
then A38: dom (DataPart p) misses dom (Start-At ((IC (Comput (ProgramPart (s2 +* (Relocated p,k))),(s2 +* (Relocated p,k)),i)) -' k),(SCM R)) by COMPOS_1:13;
A39: dom (DataPart p) misses dom (ProgramPart p) by COMPOS_1:15;
then A40: (Comput (ProgramPart s1),s1,i) | (dom (DataPart p)) = (((Comput (ProgramPart (s1 +* (Relocated p,k))),(s1 +* (Relocated p,k)),i) +* (Start-At ((IC (Comput (ProgramPart (s1 +* (Relocated p,k))),(s1 +* (Relocated p,k)),i)) -' k),(SCM R))) +* (s1 | (dom (ProgramPart (Relocated p,k))))) | (dom (DataPart p)) by A33, FUNCT_4:76
.= ((Comput (ProgramPart (s1 +* (Relocated p,k))),(s1 +* (Relocated p,k)),i) +* (Start-At ((IC (Comput (ProgramPart (s1 +* (Relocated p,k))),(s1 +* (Relocated p,k)),i)) -' k),(SCM R))) | (dom (DataPart p)) by A32, COMPOS_1:15, FUNCT_4:76
.= (Comput (ProgramPart (s1 +* (Relocated p,k))),(s1 +* (Relocated p,k)),i) | (dom (DataPart p)) by A31, FUNCT_4:76
.= (Comput (ProgramPart (s2 +* (Relocated p,k))),(s2 +* (Relocated p,k)),i) | (dom (DataPart p)) by A35, A29, RELAT_1:188
.= ((Comput (ProgramPart (s2 +* (Relocated p,k))),(s2 +* (Relocated p,k)),i) +* (Start-At ((IC (Comput (ProgramPart (s2 +* (Relocated p,k))),(s2 +* (Relocated p,k)),i)) -' k),(SCM R))) | (dom (DataPart p)) by A38, FUNCT_4:76
.= (((Comput (ProgramPart (s2 +* (Relocated p,k))),(s2 +* (Relocated p,k)),i) +* (Start-At ((IC (Comput (ProgramPart (s2 +* (Relocated p,k))),(s2 +* (Relocated p,k)),i)) -' k),(SCM R))) +* (s2 | (dom (ProgramPart (Relocated p,k))))) | (dom (DataPart p)) by A36, COMPOS_1:15, FUNCT_4:76
.= (Comput (ProgramPart s2),s2,i) | (dom (DataPart p)) by A28, A39, FUNCT_4:76 ;
IC (SCM R) in dom (Relocated p,k) by AMISTD_2:72;
then A41: {(IC (SCM R))} c= dom (Relocated p,k) by ZFMISC_1:37;
A42: Start-At (IC (Comput (ProgramPart (s1 +* (Relocated p,k))),(s1 +* (Relocated p,k)),i)),(SCM R) = (Comput (ProgramPart (s1 +* (Relocated p,k))),(s1 +* (Relocated p,k)),i) | {(IC (SCM R))} by COMPOS_1:10
.= (Comput (ProgramPart (s2 +* (Relocated p,k))),(s2 +* (Relocated p,k)),i) | {(IC (SCM R))} by A35, A41, RELAT_1:188
.= Start-At (IC (Comput (ProgramPart (s2 +* (Relocated p,k))),(s2 +* (Relocated p,k)),i)),(SCM R) by COMPOS_1:10 ;
A43: dom (Start-At (IC p),(SCM R)) = {(IC (SCM R))} by FUNCOP_1:19;
then A44: dom (Start-At (IC p),(SCM R)) misses dom (ProgramPart p) by COMPOS_1:14;
then A45: (Comput (ProgramPart s1),s1,i) | (dom (Start-At (IC p),(SCM R))) = (((Comput (ProgramPart (s1 +* (Relocated p,k))),(s1 +* (Relocated p,k)),i) +* (Start-At ((IC (Comput (ProgramPart (s1 +* (Relocated p,k))),(s1 +* (Relocated p,k)),i)) -' k),(SCM R))) +* (s1 | (dom (ProgramPart (Relocated p,k))))) | (dom (Start-At (IC p),(SCM R))) by A33, FUNCT_4:76
.= ((Comput (ProgramPart (s1 +* (Relocated p,k))),(s1 +* (Relocated p,k)),i) +* (Start-At ((IC (Comput (ProgramPart (s1 +* (Relocated p,k))),(s1 +* (Relocated p,k)),i)) -' k),(SCM R))) | (dom (Start-At (IC p),(SCM R))) by A43, A32, COMPOS_1:14, FUNCT_4:76
.= Start-At ((IC (Comput (ProgramPart (s1 +* (Relocated p,k))),(s1 +* (Relocated p,k)),i)) -' k),(SCM R) by A43, A30, FUNCT_4:24
.= Start-At ((IC (Comput (ProgramPart (s2 +* (Relocated p,k))),(s2 +* (Relocated p,k)),i)) -' k),(SCM R) by A42, COMPOS_1:44
.= ((Comput (ProgramPart (s2 +* (Relocated p,k))),(s2 +* (Relocated p,k)),i) +* (Start-At ((IC (Comput (ProgramPart (s2 +* (Relocated p,k))),(s2 +* (Relocated p,k)),i)) -' k),(SCM R))) | (dom (Start-At (IC p),(SCM R))) by A43, A37, FUNCT_4:24
.= (((Comput (ProgramPart (s2 +* (Relocated p,k))),(s2 +* (Relocated p,k)),i) +* (Start-At ((IC (Comput (ProgramPart (s2 +* (Relocated p,k))),(s2 +* (Relocated p,k)),i)) -' k),(SCM R))) +* (s2 | (dom (ProgramPart (Relocated p,k))))) | (dom (Start-At (IC p),(SCM R))) by A43, A36, COMPOS_1:14, FUNCT_4:76
.= (Comput (ProgramPart s2),s2,i) | (dom (Start-At (IC p),(SCM R))) by A28, A44, FUNCT_4:76 ;
A46: (Comput (ProgramPart s1),s1,i) | (dom ((Start-At (IC p),(SCM R)) +* (ProgramPart p))) = (Comput (ProgramPart s1),s1,i) | ((dom (Start-At (IC p),(SCM R))) \/ (dom (ProgramPart p))) by FUNCT_4:def 1
.= ((Comput (ProgramPart s2),s2,i) | (dom (Start-At (IC p),(SCM R)))) \/ ((Comput (ProgramPart s2),s2,i) | (dom (ProgramPart p))) by A45, A34, RELAT_1:107
.= (Comput (ProgramPart s2),s2,i) | ((dom (Start-At (IC p),(SCM R))) \/ (dom (ProgramPart p))) by RELAT_1:107
.= (Comput (ProgramPart s2),s2,i) | (dom ((Start-At (IC p),(SCM R)) +* (ProgramPart p))) by FUNCT_4:def 1 ;
thus (Comput (ProgramPart s1),s1,i) | (dom p) = (Comput (ProgramPart s1),s1,i) | (dom (((Start-At (IC p),(SCM R)) +* (ProgramPart p)) +* (DataPart p))) by A2, COMPOS_1:18
.= (Comput (ProgramPart s1),s1,i) | ((dom ((Start-At (IC p),(SCM R)) +* (ProgramPart p))) \/ (dom (DataPart p))) by FUNCT_4:def 1
.= ((Comput (ProgramPart s2),s2,i) | (dom ((Start-At (IC p),(SCM R)) +* (ProgramPart p)))) \/ ((Comput (ProgramPart s2),s2,i) | (dom (DataPart p))) by A40, A46, RELAT_1:107
.= (Comput (ProgramPart s2),s2,i) | ((dom ((Start-At (IC p),(SCM R)) +* (ProgramPart p))) \/ (dom (DataPart p))) by RELAT_1:107
.= (Comput (ProgramPart s2),s2,i) | (dom (((Start-At (IC p),(SCM R)) +* (ProgramPart p)) +* (DataPart p))) by FUNCT_4:def 1
.= (Comput (ProgramPart s2),s2,i) | (dom p) by A2, COMPOS_1:18 ; :: thesis: verum