let k be Element of NAT ; :: thesis: for R being non trivial good Ring
for l being Element of NAT
for p being b₂ -started non program-free autonomic halting FinPartState of (SCM R) st IC (SCM R) in dom p holds
DataPart (Result ((ProgramPart p),p)) = DataPart (Result ((ProgramPart (Relocated (p,k))),(Relocated (p,k))))
let R be non trivial good Ring; :: thesis: for l being Element of NAT
for p being b₁ -started non program-free autonomic halting FinPartState of (SCM R) st IC (SCM R) in dom p holds
DataPart (Result ((ProgramPart p),p)) = DataPart (Result ((ProgramPart (Relocated (p,k))),(Relocated (p,k))))
let l be Element of NAT ; :: thesis: for p being l -started non program-free autonomic halting FinPartState of (SCM R) st IC (SCM R) in dom p holds
DataPart (Result ((ProgramPart p),p)) = DataPart (Result ((ProgramPart (Relocated (p,k))),(Relocated (p,k))))
A1: Data-Locations (SCM R) = Data-Locations SCM by SCMRING2:31;
let p be l -started non program-free autonomic halting FinPartState of (SCM R); :: thesis: ( IC (SCM R) in dom p implies DataPart (Result ((ProgramPart p),p)) = DataPart (Result ((ProgramPart (Relocated (p,k))),(Relocated (p,k)))) )
assume A3: IC (SCM R) in dom p ; :: thesis: DataPart (Result ((ProgramPart p),p)) = DataPart (Result ((ProgramPart (Relocated (p,k))),(Relocated (p,k))))
A4: ( Relocated (p,k) is halting & Relocated (p,k) is autonomic ) by A3, Th40;
consider s being State of (SCM R) such that
A5: p c= s by PBOOLE:156;
p +* (ProgramPart p) = p by FUNCT_4:80;
then B5: p is Autonomy of ProgramPart p by EXTPRO_1:def 11;
(Relocated (p,k)) +* (ProgramPart (Relocated (p,k))) = Relocated (p,k) by FUNCT_4:80;
then B8: Relocated (p,k) is Autonomy of ProgramPart (Relocated (p,k)) by A4, EXTPRO_1:def 11;
ProgramPart s halts_on s by A5, EXTPRO_1:def 10;
then consider j1 being Element of NAT such that
A6: Result ((ProgramPart s),s) = Comput ((ProgramPart s),s,j1) and
A7: CurInstr ((ProgramPart s),(Result ((ProgramPart s),s))) = halt (SCM R) by EXTPRO_1:def 8;
consider t being State of (SCM R) such that
A8: Relocated (p,k) c= t by PBOOLE:156;
reconsider s3 = s +* (DataPart t) as State of (SCM R) ;
A9: s3 = s3 ;
Y: (ProgramPart (Comput ((ProgramPart t),t,j1))) /. (IC (Comput ((ProgramPart t),t,j1))) = (Comput ((ProgramPart t),t,j1)) . (IC (Comput ((ProgramPart t),t,j1))) by COMPOS_1:38;
TX: ProgramPart s = ProgramPart (Comput ((ProgramPart s),s,j1)) by AMI_1:123;
(ProgramPart t) . (IC (Comput ((ProgramPart t),t,j1))) = t . (IC (Comput ((ProgramPart t),t,j1))) by COMPOS_1:2
.= CurInstr ((ProgramPart (Comput ((ProgramPart t),t,j1))),(Comput ((ProgramPart t),t,j1))) by Y, AMI_1:54
.= IncAddr ((CurInstr ((ProgramPart s),(Comput ((ProgramPart s),s,j1)))),k) by A3, A5, A8, A9, Th35, TX
.= halt (SCM R) by A6, A7, COMPOS_1:92 ;
then A10: Result ((ProgramPart t),t) = Comput ((ProgramPart t),t,j1) by EXTPRO_1:8;
thus DataPart (Result ((ProgramPart p),p)) = DataPart ((Result ((ProgramPart s),s)) | (dom p)) by A5, B5, EXTPRO_1:def 12
.= (Result ((ProgramPart s),s)) | ((dom p) /\ (Data-Locations SCM)) by A1, RELAT_1:100
.= (Result ((ProgramPart s),s)) | (dom (DataPart p)) by A1, RELAT_1:90
.= (Result ((ProgramPart t),t)) | (dom (DataPart (Relocated (p,k)))) by A3, A5, A6, A8, A9, A10, Th35
.= (Result ((ProgramPart t),t)) | ((dom (Relocated (p,k))) /\ (Data-Locations SCM)) by A1, RELAT_1:90
.= DataPart ((Result ((ProgramPart t),t)) | (dom (Relocated (p,k)))) by A1, RELAT_1:100
.= DataPart (Result ((ProgramPart (Relocated (p,k))),(Relocated (p,k)))) by A8, B8, EXTPRO_1:def 12 ; :: thesis: verum