let N be non empty with_non-empty_elements set ; :: thesis: for S being non empty stored-program IC-Ins-separated definite realistic standard-ins homogeneous regular J/A-independent proper-halt halting Exec-preserving relocable IC-recognized relocable1 AMI-Struct of N st S is relocable1 & S is relocable2 & S is CurIns-recognized holds
for p being non program-free autonomic halting FinPartState of S st IC in dom p holds
for k being Element of NAT holds DataPart (Result ((ProgramPart p),p)) = DataPart (Result ((Reloc ((ProgramPart p),k)),(Relocated (p,k))))
let S be non empty stored-program IC-Ins-separated definite realistic standard-ins homogeneous regular J/A-independent proper-halt halting Exec-preserving relocable IC-recognized relocable1 AMI-Struct of N; :: thesis: ( S is relocable1 & S is relocable2 & S is CurIns-recognized implies for p being non program-free autonomic halting FinPartState of S st IC in dom p holds
for k being Element of NAT holds DataPart (Result ((ProgramPart p),p)) = DataPart (Result ((Reloc ((ProgramPart p),k)),(Relocated (p,k)))) )
assume A1: ( S is relocable1 & S is relocable2 & S is CurIns-recognized ) ; :: thesis: for p being non program-free autonomic halting FinPartState of S st IC in dom p holds
for k being Element of NAT holds DataPart (Result ((ProgramPart p),p)) = DataPart (Result ((Reloc ((ProgramPart p),k)),(Relocated (p,k))))
let p be non program-free autonomic halting FinPartState of S; :: thesis: ( IC in dom p implies for k being Element of NAT holds DataPart (Result ((ProgramPart p),p)) = DataPart (Result ((Reloc ((ProgramPart p),k)),(Relocated (p,k)))) )
assume A2: IC in dom p ; :: thesis: for k being Element of NAT holds DataPart (Result ((ProgramPart p),p)) = DataPart (Result ((Reloc ((ProgramPart p),k)),(Relocated (p,k))))
let k be Element of NAT ; :: thesis: DataPart (Result ((ProgramPart p),p)) = DataPart (Result ((Reloc ((ProgramPart p),k)),(Relocated (p,k))))
RE: Reloc ((ProgramPart p),k) = ProgramPart (Relocated (p,k)) by COMPOS_1:116;
consider s being State of S such that
A4: p c= s by PBOOLE:156;
B4: NPP p c= s by A4, XBOOLE_1:1;
A5: ProgramPart p c= ProgramPart s by A4, RELAT_1:105;
A6: ( Relocated (p,k) is halting & Relocated (p,k) is autonomic ) by A2, Th12, Th11, A1;
(Relocated (p,k)) +* (Reloc ((ProgramPart p),k)) = Relocated (p,k) by FUNCT_4:99;
then A7: Relocated (p,k) is Autonomy of Reloc ((ProgramPart p),k) by A6, EXTPRO_1:def 11;
ProgramPart s halts_on s by A5, B4, EXTPRO_1:def 10;
then consider j1 being Element of NAT such that
A8: Result ((ProgramPart s),s) = Comput ((ProgramPart s),s,j1) and
A9: CurInstr ((ProgramPart s),(Result ((ProgramPart s),s))) = halt S by EXTPRO_1:def 8;
consider t being State of S such that
A10: Relocated (p,k) c= t by PBOOLE:156;
B10: NPP (Relocated (p,k)) c= t by A10, XBOOLE_1:1;
A11: Reloc ((ProgramPart p),k) c= ProgramPart t by A10, RE, RELAT_1:105;
(ProgramPart t) . (IC (Comput ((ProgramPart t),t,j1))) = t . (IC (Comput ((ProgramPart t),t,j1))) by COMPOS_1:2
.= CurInstr ((ProgramPart t),(Comput ((ProgramPart t),t,j1))) by COMPOS_1:38
.= IncAddr ((CurInstr ((ProgramPart s),(Comput ((ProgramPart s),s,j1)))),k) by A2, Def5, A5, A11, B4, B10
.= halt S by A8, A9, COMPOS_1:93 ;
then A12: Result ((ProgramPart t),t) = Comput ((ProgramPart t),t,j1) by EXTPRO_1:8;
A13: (Comput ((ProgramPart t),t,j1)) | (dom (DataPart p)) = (Comput ((ProgramPart s),s,j1)) | (dom (DataPart p)) by A2, A1, Def6, A11, A5, B10, B4;
DPDP: DataPart (Relocated (p,k)) = DataPart p by COMPOS_1:115;
p +* (ProgramPart p) = p by FUNCT_4:80;
then p is Autonomy of ProgramPart p by EXTPRO_1:def 11;
hence DataPart (Result ((ProgramPart p),p)) = DataPart ((Result ((ProgramPart s),s)) | (dom (NPP p))) by A4, A5, EXTPRO_1:def 12
.= (Result ((ProgramPart s),s)) | ((dom (NPP p)) /\ (Data-Locations S)) by RELAT_1:100
.= (Result ((ProgramPart s),s)) | (dom (DataPart p)) by COMPOS_1:182
.= (Result ((ProgramPart t),t)) | ((dom (NPP (Relocated (p,k)))) /\ (Data-Locations S)) by A8, A12, A13, DPDP, COMPOS_1:182
.= ((Result ((ProgramPart t),t)) | (dom (NPP (Relocated (p,k))))) | (Data-Locations S) by RELAT_1:100
.= DataPart (Result ((Reloc ((ProgramPart p),k)),(Relocated (p,k)))) by A10, A7, RE, A11, EXTPRO_1:def 12 ;
:: thesis: verum