let k be Element of NAT ; :: thesis: for R being good Ring st not R is trivial holds
for p being 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 good Ring; :: thesis: ( not R is trivial implies for p being 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) = SCM-Data-Loc by SCMRING2:31;
assume A2: not R is trivial ; :: thesis: for p being 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 p be 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 A2, A3, Th36, Th40;
consider s being State of (SCM R) such that
A5: p c= s by PBOOLE:156;
ProgramPart s halts_on s by A5, AMI_1:def 26;
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 AMI_1:def 22;
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 A2, A3, A5, A8, A9, Th35, TX
.= halt (SCM R) by A6, A7, AMISTD_2:29 ;
then A10: Result (ProgramPart t),t = Comput (ProgramPart t),t,j1 by AMI_1:56;
thus DataPart (Result (ProgramPart p),p) = DataPart ((Result (ProgramPart s),s) | (dom p)) by A5, AMI_1:def 29
.= (Result (ProgramPart s),s) | ((dom p) /\ SCM-Data-Loc ) 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 A2, A3, A5, A6, A8, A9, A10, Th35
.= (Result (ProgramPart t),t) | ((dom (Relocated p,k)) /\ SCM-Data-Loc ) 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, A4, AMI_1:def 29 ; :: thesis: verum