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)) )
X: Data-Locations (SCM R) = SCM-Data-Loc by SCMRING2:31;
assume A1: 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 A2: IC (SCM R) in dom p ; :: thesis: DataPart (Result p) = DataPart (Result (Relocated p,k))
consider s being State of (SCM R) such that
A3: p c= s by CARD_3:97;
s is halting by A3, AMI_1:def 26;
then consider j1 being Element of NAT such that
A4: Result s = Computation s,j1 and
A5: CurInstr (Result s) = halt (SCM R) by AMI_1:def 22;
consider t being State of (SCM R) such that
A6: Relocated p,k c= t by CARD_3:97;
reconsider s3 = s +* (DataPart t) as State of (SCM R) ;
A7: s3 = s3 ;
t . (IC (Computation t,j1)) = CurInstr (Computation t,j1) by AMI_1:54
.= IncAddr (CurInstr (Computation s,j1)),k by A1, A2, A3, A6, A7, Th59
.= halt (SCM R) by A4, A5, AMISTD_2:29 ;
then A8: Result t = Computation t,j1 by AMI_1:56;
A9: ( Relocated p,k is halting & Relocated p,k is autonomic ) by A1, A2, Th60, Th64;
thus DataPart (Result p) = DataPart ((Result s) | (dom p)) by A3, AMI_1:def 28
.= (Result s) | ((dom p) /\ SCM-Data-Loc ) by X, RELAT_1:100
.= (Result s) | (dom (DataPart p)) by X, RELAT_1:90
.= (Result t) | (dom (DataPart (Relocated p,k))) by A1, A2, A3, A4, A6, A7, A8, Th59
.= (Result t) | ((dom (Relocated p,k)) /\ SCM-Data-Loc ) by X, RELAT_1:90
.= DataPart ((Result t) | (dom (Relocated p,k))) by X, RELAT_1:100
.= DataPart (Result (Relocated p,k)) by A6, A9, AMI_1:def 28 ; :: thesis: verum