let k be natural number ; :: 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 p) = DataPart (Result (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 p) = DataPart (Result (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 p) = DataPart (Result (Relocated p,k))
let p be autonomic halting FinPartState of (SCM R); :: thesis: ( IC (SCM R) in dom p implies DataPart (Result p) = DataPart (Result (Relocated p,k)) )
assume A3: IC (SCM R) in dom p ; :: thesis: DataPart (Result p) = DataPart (Result (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 s = Comput (ProgramPart s),s,j1 and
A7: CurInstr (ProgramPart (Result s)),(Result 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 AMI_1:150;
t . (IC (Comput (ProgramPart t),t,j1)) = CurInstr (ProgramPart (Comput (ProgramPart t),t,j1)),(Comput (ProgramPart t),t,j1) by AMI_1:54, Y
.= IncAddr (CurInstr (ProgramPart (Comput (ProgramPart s),s,j1)),(Comput (ProgramPart s),s,j1)),k by A2, A3, A5, A8, A9, Th35
.= halt (SCM R) by A6, A7, AMISTD_2:29 ;
then A10: Result t = Comput (ProgramPart t),t,j1 by AMI_1:56;
thus DataPart (Result p) = DataPart ((Result s) | (dom p)) by A5, AMI_1:def 28
.= (Result s) | ((dom p) /\ SCM-Data-Loc ) by A1, RELAT_1:100
.= (Result s) | (dom (DataPart p)) by A1, RELAT_1:90
.= (Result t) | (dom (DataPart (Relocated p,k))) by A2, A3, A5, A6, A8, A9, A10, Th35
.= (Result t) | ((dom (Relocated p,k)) /\ SCM-Data-Loc ) by A1, RELAT_1:90
.= DataPart ((Result t) | (dom (Relocated p,k))) by A1, RELAT_1:100
.= DataPart (Result (Relocated p,k)) by A8, A4, AMI_1:def 28 ; :: thesis: verum