let k be natural number ; :: thesis: for R being good Ring st not R is trivial holds
for p being autonomic FinPartState of (SCM R) st IC (SCM R) in dom p holds
( p is halting iff Relocated p,k is halting )
let R be good Ring; :: thesis: ( not R is trivial implies for p being autonomic FinPartState of (SCM R) st IC (SCM R) in dom p holds
( p is halting iff Relocated p,k is halting ) )
assume A1: not R is trivial ; :: thesis: for p being autonomic FinPartState of (SCM R) st IC (SCM R) in dom p holds
( p is halting iff Relocated p,k is halting )
let p be autonomic FinPartState of (SCM R); :: thesis: ( IC (SCM R) in dom p implies ( p is halting iff Relocated p,k is halting ) )
assume A2: IC (SCM R) in dom p ; :: thesis: ( p is halting iff Relocated p,k is halting )

hereby :: thesis: ( Relocated p,k is halting implies p is halting )

assume A3: p is halting ; :: thesis: Relocated p,k is halting
thus Relocated p,k is halting :: thesis: verum

proof

let t be State of (SCM R); :: according to AMI_1:def 26 :: thesis: ( not Relocated p,k c= t or t is halting )
assume A4: Relocated p,k c= t ; :: thesis: t is halting
set s = t +* p;
A5: p c= t +* p by FUNCT_4:26;
then t +* p is halting by A3, AMI_1:def 26;
then consider u being Element of NAT such that
A6: CurInstr (Computation (t +* p),u) = halt (SCM R) by AMI_1:def 20;
reconsider s3 = (t +* p) +* (DataPart t) as State of (SCM R) ;
s3 = s3 ;
then A7: CurInstr (Computation t,u) = IncAddr (halt (SCM R)),k by A1, A2, A4, A5, A6, Th59
.= halt (SCM R) by AMISTD_2:29 ;
take u ; :: according to AMI_1:def 20 :: thesis: CurInstr (Computation t,u) = halt (SCM R)
thus CurInstr (Computation t,u) = halt (SCM R) by A7; :: thesis: verum

end;

end;

assume A8: Relocated p,k is halting ; :: thesis: p is halting
let t be State of (SCM R); :: according to AMI_1:def 26 :: thesis: ( not p c= t or t is halting )
assume A9: p c= t ; :: thesis: t is halting
reconsider s = t +* (Relocated p,k) as State of (SCM R) ;
A10: Relocated p,k c= t +* (Relocated p,k) by FUNCT_4:26;
then s is halting by A8, AMI_1:def 26;
then consider u being Element of NAT such that
A11: CurInstr (Computation s,u) = halt (SCM R) by AMI_1:def 20;
reconsider s3 = t +* (DataPart s) as State of (SCM R) ;
s3 = s3 ;
then A12: IncAddr (CurInstr (Computation t,u)),k = halt (SCM R) by A1, A2, A9, A10, A11, Th59;
take u ; :: according to AMI_1:def 20 :: thesis: CurInstr (Computation t,u) = halt (SCM R)
thus CurInstr (Computation t,u) = halt (SCM R) by A12, AMISTD_2:35; :: thesis: verum