let p be autonomic FinPartState of SCM ; :: thesis: for k being Element of NAT st IC SCM in dom p holds
( p is halting iff Relocated p,k is halting )
let k be Element of NAT ; :: thesis: ( IC SCM in dom p implies ( p is halting iff Relocated p,k is halting ) )
assume A1: IC SCM 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 A2: p is halting ; :: thesis: Relocated p,k is halting
thus Relocated p,k is halting :: thesis: verum

proof

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

end;

end;

assume A7: Relocated p,k is halting ; :: thesis: p is halting
let t be State of SCM ; :: according to AMI_1:def 26 :: thesis: ( not p c= t or t is halting )
assume A8: p c= t ; :: thesis: t is halting
reconsider s = t +* (Relocated p,k) as State of SCM ;
Relocated p,k c= t +* (Relocated p,k) by FUNCT_4:26;
then s is halting by A7, AMI_1:def 26;
then consider u being Element of NAT such that
A10: CurInstr (Computation s,u) = halt SCM by AMI_1:def 20;
A11: IncAddr (CurInstr (Computation t,u)),k = halt SCM by A1, A8, A10, Th34B, FUNCT_4:26;
take u ; :: according to AMI_1:def 20 :: thesis: CurInstr (Computation t,u) = halt SCM
thus CurInstr (Computation t,u) = halt SCM by A11, Th14, AMI_5:37; :: thesis: verum