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 EXTPRO_1:def 10 :: thesis: ( not Relocated (p,k) c= t or ProgramPart t halts_on t )
assume A3: Relocated (p,k) c= t ; :: thesis: ProgramPart t halts_on t
reconsider s = t +* p as State of SCM ;
p c= t +* p by FUNCT_4:26;
then ProgramPart s halts_on s by A2, EXTPRO_1:def 10;
then consider u being Element of NAT such that
A4: CurInstr ((ProgramPart s),(Comput ((ProgramPart s),s,u))) = halt SCM by EXTPRO_1:30;
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 )
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
CurInstr ((ProgramPart t),(Comput ((ProgramPart t),t,u))) = IncAddr ((halt SCM),k) by A1, A3, A4, Th35, FUNCT_4:26
.= halt SCM by COMPOS_1:93 ;
hence CurInstr ((ProgramPart t),(Comput ((ProgramPart t),t,u))) = halt SCM ; :: thesis: verum

end;

end;

assume A5: Relocated (p,k) is halting ; :: thesis: p is halting
let t be State of SCM; :: 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 ;
Relocated (p,k) c= t +* (Relocated (p,k)) by FUNCT_4:26;
then ProgramPart s halts_on s by A5, EXTPRO_1:def 10;
then consider u being Element of NAT such that
A6: CurInstr ((ProgramPart s),(Comput ((ProgramPart s),s,u))) = halt SCM by EXTPRO_1:30;
assume A7: 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 )
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
IncAddr ((CurInstr ((ProgramPart t),(Comput ((ProgramPart t),t,u)))),k) = halt SCM by A1, A7, A6, Th35, FUNCT_4:26;
hence CurInstr ((ProgramPart t),(Comput ((ProgramPart t),t,u))) = halt SCM by Th14, AMI_5:37; :: thesis: verum