let p be autonomic FinPartState of SCM+FSA ; :: thesis: for k being Element of NAT st IC SCM+FSA in dom p holds
( p is halting iff Relocated p,k is halting )
let k be Element of NAT ; :: thesis: ( IC SCM+FSA in dom p implies ( p is halting iff Relocated p,k is halting ) )
A1: not 0 in {6,7,8} ;
assume A2: IC SCM+FSA 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+FSA ; :: according to AMI_1:def 26 :: 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
reconsider s = t +* p as State of SCM+FSA ;
A5: p c= t +* p by FUNCT_4:26;
then ProgramPart s halts_on s by A3, AMI_1:def 26;
then consider u being Element of NAT such that
A6: CurInstr (ProgramPart (Comput (ProgramPart s),s,u)),(Comput (ProgramPart s),s,u) = halt SCM+FSA by AMI_1:146;
take u ; :: according to AMI_1:def 20 :: thesis: ( IC (Comput (ProgramPart t),t,u) in proj1 (ProgramPart t) & (ProgramPart t) /. (IC (Comput (ProgramPart t),t,u)) = halt SCM+FSA )
IC (Comput (ProgramPart t),t,u) in NAT ;
hence IC (Comput (ProgramPart t),t,u) in dom (ProgramPart t) by AMI_1:143; :: thesis: (ProgramPart t) /. (IC (Comput (ProgramPart t),t,u)) = halt SCM+FSA
CurInstr (ProgramPart (Comput (ProgramPart t),t,u)),(Comput (ProgramPart t),t,u) = IncAddr (halt SCM+FSA ),k by A2, A4, A5, A6, Th12
.= halt SCM+FSA by SCMFSA_4:8 ;
hence (ProgramPart t) /. (IC (Comput (ProgramPart t),t,u)) = halt SCM+FSA by AMI_1:145; :: thesis: verum
reconsider s3 = s +* (DataPart t) as State of SCM+FSA ;

end;

end;

assume A7: Relocated p,k is halting ; :: thesis: p is halting
let t be State of SCM+FSA ; :: according to AMI_1:def 26 :: thesis: ( not p c= t or ProgramPart t halts_on t )
reconsider s = t +* (Relocated p,k) as State of SCM+FSA ;
A8: Relocated p,k c= t +* (Relocated p,k) by FUNCT_4:26;
then ProgramPart s halts_on s by A7, AMI_1:def 26;
then consider u being Element of NAT such that
A9: CurInstr (ProgramPart (Comput (ProgramPart s),s,u)),(Comput (ProgramPart s),s,u) = halt SCM+FSA by AMI_1:146;
assume p c= t ; :: thesis: ProgramPart t halts_on t
then A10: IncAddr (CurInstr (ProgramPart (Comput (ProgramPart t),t,u)),(Comput (ProgramPart t),t,u)),k = halt SCM+FSA by A2, A8, A9, Th12;
take u ; :: according to AMI_1:def 20 :: thesis: ( IC (Comput (ProgramPart t),t,u) in proj1 (ProgramPart t) & (ProgramPart t) /. (IC (Comput (ProgramPart t),t,u)) = halt SCM+FSA )
IC (Comput (ProgramPart t),t,u) in NAT ;
hence IC (Comput (ProgramPart t),t,u) in dom (ProgramPart t) by AMI_1:143; :: thesis: (ProgramPart t) /. (IC (Comput (ProgramPart t),t,u)) = halt SCM+FSA
InsCode (CurInstr (ProgramPart (Comput (ProgramPart t),t,u)),(Comput (ProgramPart t),t,u)) = 0 by A10, SCMFSA_2:124, SCMFSA_4:22;
then CurInstr (ProgramPart (Comput (ProgramPart t),t,u)),(Comput (ProgramPart t),t,u) = halt SCM+FSA by A10, A1, SCMFSA_4:def 3;
hence (ProgramPart t) /. (IC (Comput (ProgramPart t),t,u)) = halt SCM+FSA by AMI_1:145; :: thesis: verum
reconsider s3 = t +* (DataPart s) as State of SCM+FSA ;