let k be Element of NAT ; :: 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 EXTPRO_1:def 10 :: thesis: ( not Relocated (p,k) c= t or ProgramPart t halts_on t )
assume A4: Relocated (p,k) c= t ; :: thesis: ProgramPart t halts_on t
set s = t +* p;
reconsider s3 = (t +* p) +* (DataPart t) as State of (SCM R) ;
A5: p c= t +* p by FUNCT_4:26;
then ProgramPart (t +* p) halts_on t +* p by A3, EXTPRO_1:def 10;
then consider u being Element of NAT such that
A6: CurInstr ((ProgramPart (t +* p)),(Comput ((ProgramPart (t +* p)),(t +* p),u))) = halt (SCM R) by EXTPRO_1:30;
TX: ProgramPart (t +* p) = ProgramPart (Comput ((ProgramPart (t +* p)),(t +* p),u)) by AMI_1:123;
take u ; :: according to EXTPRO_1:def 7 :: thesis: ( IC (Comput ((ProgramPart t),t,u)) in proj1 (ProgramPart t) & CurInstr ((ProgramPart t),(Comput ((ProgramPart t),t,u))) = halt (SCM R) )
IC (Comput ((ProgramPart t),t,u)) in NAT ;
hence IC (Comput ((ProgramPart t),t,u)) in dom (ProgramPart t) by COMPOS_1:34; :: thesis: CurInstr ((ProgramPart t),(Comput ((ProgramPart t),t,u))) = halt (SCM R)
NX: ProgramPart t = ProgramPart (Comput ((ProgramPart t),t,u)) by AMI_1:123;
s3 = s3 ;
then CurInstr ((ProgramPart t),(Comput ((ProgramPart t),t,u))) = IncAddr ((halt (SCM R)),k) by A1, A2, A4, A5, A6, Th35, TX, NX
.= halt (SCM R) by COMPOS_1:92 ;
hence CurInstr ((ProgramPart t),(Comput ((ProgramPart t),t,u))) = halt (SCM R) ; :: thesis: verum

end;

end;

assume A7: Relocated (p,k) is halting ; :: thesis: p is halting
let t be State of (SCM R); :: according to EXTPRO_1:def 10 :: thesis: ( not p c= t or ProgramPart t halts_on t )
reconsider s = t +* (Relocated (p,k)) as State of (SCM R) ;
A8: Relocated (p,k) c= t +* (Relocated (p,k)) by FUNCT_4:26;
then ProgramPart s halts_on s by A7, EXTPRO_1:def 10;
then consider u being Element of NAT such that
A9: CurInstr ((ProgramPart s),(Comput ((ProgramPart s),s,u))) = halt (SCM R) by EXTPRO_1:30;
TX: ProgramPart s = ProgramPart (Comput ((ProgramPart s),s,u)) by AMI_1:123;
reconsider s3 = t +* (DataPart s) as State of (SCM R) ;
assume A10: p c= t ; :: thesis: ProgramPart t halts_on t
take u ; :: according to EXTPRO_1:def 7 :: thesis: ( IC (Comput ((ProgramPart t),t,u)) in proj1 (ProgramPart t) & CurInstr ((ProgramPart t),(Comput ((ProgramPart t),t,u))) = halt (SCM R) )
IC (Comput ((ProgramPart t),t,u)) in NAT ;
hence IC (Comput ((ProgramPart t),t,u)) in dom (ProgramPart t) by COMPOS_1:34; :: thesis: CurInstr ((ProgramPart t),(Comput ((ProgramPart t),t,u))) = halt (SCM R)
NX: ProgramPart t = ProgramPart (Comput ((ProgramPart t),t,u)) by AMI_1:123;
s3 = s3 ;
then IncAddr ((CurInstr ((ProgramPart t),(Comput ((ProgramPart t),t,u)))),k) = halt (SCM R) by A1, A2, A10, A8, A9, Th35, TX, NX;
hence CurInstr ((ProgramPart t),(Comput ((ProgramPart t),t,u))) = halt (SCM R) by COMPOS_1:96; :: thesis: verum