let N be non empty with_non-empty_elements set ; :: thesis:
let S be non empty stored-program IC-Ins-separated definite realistic standard-ins homogeneous regular J/A-independent halting Exec-preserving relocable IC-recognized AMI-Struct of N; :: thesis:
assume A1: S is CurIns-recognized ; :: thesis:
let p be FinPartState of S; :: thesis:
assume A2: IC in dom p ; :: thesis:
let k be Element of NAT ; :: thesis:
RE: Reloc ((ProgramPart p),k) = ProgramPart (Relocated (p,k)) by COMPOS_1:116;

hereby :: thesis:

assume A4: p is autonomic ; :: thesis:
thus Relocated (p,k) is autonomic :: thesis:

proof

let P, Q be the Instructions of S -valued ManySortedSet of NAT ; :: according to EXTPRO_1:def 9 :: thesis:
assume that
A5: ProgramPart (Relocated (p,k)) c= P and
A6: ProgramPart (Relocated (p,k)) c= Q ; :: thesis:
let s1, s2 be State of S; :: thesis:
assume that
A7: NPP (Relocated (p,k)) c= s1 and
A8: NPP (Relocated (p,k)) c= s2 ; :: thesis:
let i be Element of NAT ; :: thesis:
A9: NPP (Comput (P,s1,i)) = NPP (IncIC ((Comput ((P +* (ProgramPart p)),(s1 +* (NPP p)),i)),k)) by A2, A4, A7, Th9, A1, A5, RE;
A12: dom (Start-At (((IC (Comput ((Q +* (ProgramPart p)),(s2 +* (NPP p)),i))) + k),S)) = {(IC )} by FUNCOP_1:19;
then A13: dom (DataPart p) misses dom (Start-At (((IC (Comput ((Q +* (ProgramPart p)),(s2 +* (NPP p)),i))) + k),S)) by COMPOS_1:13;
A14: dom (Start-At (((IC (Comput ((P +* (ProgramPart p)),(s1 +* (NPP p)),i))) + k),S)) = {(IC )} by FUNCOP_1:19;
then A15: dom (DataPart p) misses dom (Start-At (((IC (Comput ((P +* (ProgramPart p)),(s1 +* (NPP p)),i))) + k),S)) by COMPOS_1:13;
A16: NPP (Comput (Q,s2,i)) = NPP (IncIC ((Comput ((Q +* (ProgramPart p)),(s2 +* (NPP p)),i)),k)) by A2, A4, A8, Th9, A1, A6, RE;
A17: ( ProgramPart p c= P +* (ProgramPart p) & ProgramPart p c= Q +* (ProgramPart p) ) by FUNCT_4:26;
( NPP p c= s1 +* (NPP p) & NPP p c= s2 +* (NPP p) ) by FUNCT_4:26;
then A18: (Comput ((P +* (ProgramPart p)),(s1 +* (NPP p)),i)) | (dom (NPP p)) = (Comput ((Q +* (ProgramPart p)),(s2 +* (NPP p)),i)) | (dom (NPP p)) by A4, A17, EXTPRO_1:def 9;
A19: DataPart p c= NPP p by COMPOS_1:169;
A21: (Comput (P,s1,i)) | (dom (DataPart p)) = (NPP (Comput (P,s1,i))) | (dom (DataPart p)) by COMPOS_1:241
.= (NPP (IncIC ((Comput ((P +* (ProgramPart p)),(s1 +* (NPP p)),i)),k))) | (dom (DataPart p)) by A9
.= (IncIC ((Comput ((P +* (ProgramPart p)),(s1 +* (NPP p)),i)),k)) | (dom (DataPart p)) by COMPOS_1:241
.= (Comput ((P +* (ProgramPart p)),(s1 +* (NPP p)),i)) | (dom (DataPart p)) by A15, FUNCT_4:76
.= (Comput ((Q +* (ProgramPart p)),(s2 +* (NPP p)),i)) | (dom (DataPart p)) by A18, A19, RELAT_1:25, RELAT_1:188
.= (IncIC ((Comput ((Q +* (ProgramPart p)),(s2 +* (NPP p)),i)),k)) | (dom (DataPart p)) by A13, FUNCT_4:76
.= (NPP (IncIC ((Comput ((Q +* (ProgramPart p)),(s2 +* (NPP p)),i)),k))) | (dom (DataPart p)) by COMPOS_1:241
.= (NPP (Comput (Q,s2,i))) | (dom (DataPart p)) by A16
.= (Comput (Q,s2,i)) | (dom (DataPart p)) by COMPOS_1:241 ;
IC in dom (NPP p) by A2, COMPOS_1:179;
then A22: {(IC )} c= dom (NPP p) by ZFMISC_1:37;
A23: Start-At ((IC (Comput ((P +* (ProgramPart p)),(s1 +* (NPP p)),i))),S) = (Comput ((P +* (ProgramPart p)),(s1 +* (NPP p)),i)) | {(IC )} by COMPOS_1:10
.= (Comput ((Q +* (ProgramPart p)),(s2 +* (NPP p)),i)) | {(IC )} by A18, A22, RELAT_1:188
.= Start-At ((IC (Comput ((Q +* (ProgramPart p)),(s2 +* (NPP p)),i))),S) by COMPOS_1:10 ;
A24: dom (Start-At (((IC p) + k),S)) = {(IC )} by FUNCOP_1:19;
then A26: (Comput (P,s1,i)) | (dom (Start-At (((IC p) + k),S))) = (NPP (Comput (P,s1,i))) | (dom (Start-At (((IC p) + k),S))) by COMPOS_1:242
.= (NPP (IncIC ((Comput ((P +* (ProgramPart p)),(s1 +* (NPP p)),i)),k))) | (dom (Start-At (((IC p) + k),S))) by A9
.= (IncIC ((Comput ((P +* (ProgramPart p)),(s1 +* (NPP p)),i)),k)) | (dom (Start-At (((IC p) + k),S))) by A24, COMPOS_1:242
.= Start-At (((IC (Comput ((P +* (ProgramPart p)),(s1 +* (NPP p)),i))) + k),S) by A24, A14, FUNCT_4:24
.= Start-At (((IC (Comput ((Q +* (ProgramPart p)),(s2 +* (NPP p)),i))) + k),S) by A23, COMPOS_1:43
.= (IncIC ((Comput ((Q +* (ProgramPart p)),(s2 +* (NPP p)),i)),k)) | (dom (Start-At (((IC p) + k),S))) by A24, A12, FUNCT_4:24
.= (NPP (IncIC ((Comput ((Q +* (ProgramPart p)),(s2 +* (NPP p)),i)),k))) | (dom (Start-At (((IC p) + k),S))) by A24, COMPOS_1:242
.= (NPP (Comput (Q,s2,i))) | (dom (Start-At (((IC p) + k),S))) by A16
.= (Comput (Q,s2,i)) | (dom (Start-At (((IC p) + k),S))) by A24, COMPOS_1:242 ;
A27: dom (Start-At (((IC p) + k),S)) = {(IC )} by FUNCOP_1:19;
A28: dom (NPP p) = {(IC )} \/ (dom (DataPart p)) by A2, COMPOS_1:70;
A29: (Comput (P,s1,i)) | (dom (NPP p)) = ((Comput (P,s1,i)) | {(IC )}) \/ ((Comput (P,s1,i)) | (dom (DataPart p))) by A28, RELAT_1:107
.= (Comput (Q,s2,i)) | (dom (NPP p)) by A28, A27, A21, A26, RELAT_1:107 ;
A30: dom (IncIC ((NPP p),k)) = (dom (NPP p)) \/ (dom (Start-At (((IC (NPP p)) + k),S))) by FUNCT_4:def 1
.= (dom (NPP p)) \/ (dom (Start-At (((IC p) + k),S))) by A2, COMPOS_1:72 ;
A31: (Comput (P,s1,i)) | (dom (IncIC ((NPP p),k))) = ((Comput (P,s1,i)) | (dom (NPP p))) \/ ((Comput (P,s1,i)) | (dom (Start-At (((IC p) + k),S)))) by A30, RELAT_1:107
.= (Comput (Q,s2,i)) | (dom (IncIC ((NPP p),k))) by A30, A26, A29, RELAT_1:107 ;
thus (Comput (P,s1,i)) | (dom (NPP (Relocated (p,k)))) = (Comput (P,s1,i)) | (dom (IncIC ((NPP p),k))) by COMPOS_1:180
.= (Comput (Q,s2,i)) | (dom (NPP (Relocated (p,k)))) by A31, COMPOS_1:180 ; :: thesis:

end;