let p be non program-free autonomic halting FinPartState of SCM; :: thesis: ( IC SCM 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 A1: IC SCM 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))))
consider s being State of SCM such that
A2: p c= s by PBOOLE:156;
A3: ( Relocated (p,k) is halting & Relocated (p,k) is autonomic ) by A1, Th38, Th41;
(Relocated (p,k)) +* (Reloc ((ProgramPart p),k)) = Relocated (p,k) by FUNCT_4:99;
then B3: Relocated (p,k) is Autonomy of Reloc ((ProgramPart p),k) by A3, EXTPRO_1:def 11;
ProgramPart s halts_on s by A2, EXTPRO_1:def 10;
then consider j1 being Element of NAT such that
A4: Result ((ProgramPart s),s) = Comput ((ProgramPart s),s,j1) and
A5: CurInstr ((ProgramPart s),(Result ((ProgramPart s),s))) = halt SCM by EXTPRO_1:def 8;
consider t being State of SCM such that
A6: Relocated (p,k) c= t by PBOOLE:156;
(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 A1, A2, A6, Lm1
.= halt SCM by A4, A5, COMPOS_1:93 ;
then A7: Result ((ProgramPart t),t) = Comput ((ProgramPart t),t,j1) by EXTPRO_1:8;
A8: (Comput ((ProgramPart t),t,j1)) | (dom (DataPart (Relocated (p,k)))) = (Comput ((ProgramPart s),s,j1)) | (dom (DataPart p)) by A1, A2, A6, Lm1;
X: Reloc ((ProgramPart p),k) = ProgramPart (Relocated (p,k)) by COMPOS_1:116;
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 p)) by A2, EXTPRO_1:def 12
.= (Result ((ProgramPart s),s)) | ((dom p) /\ (Data-Locations SCM)) by RELAT_1:100
.= (Result ((ProgramPart s),s)) | (dom (DataPart p)) by RELAT_1:90
.= (Result ((ProgramPart t),t)) | ((dom (Relocated (p,k))) /\ (Data-Locations SCM)) by A4, A7, A8, RELAT_1:90
.= ((Result ((ProgramPart t),t)) | (dom (Relocated (p,k)))) | (Data-Locations SCM) by RELAT_1:100
.= DataPart (Result ((Reloc ((ProgramPart p),k)),(Relocated (p,k)))) by X, A6, EXTPRO_1:def 12, B3 ;
:: thesis: verum