let N be with_non-empty_elements set ; :: thesis: for S being non empty stored-program halting IC-Ins-separated steady-programmed definite AMI-Struct of N
for s being State of S holds
( ProgramPart s halts_on s iff ex k being Element of NAT st CurInstr (Computation s,k) = halt S )
let S be non empty stored-program halting IC-Ins-separated steady-programmed definite AMI-Struct of N; :: thesis: for s being State of S holds
( ProgramPart s halts_on s iff ex k being Element of NAT st CurInstr (Computation s,k) = halt S )
let s be State of S; :: thesis: ( ProgramPart s halts_on s iff ex k being Element of NAT st CurInstr (Computation s,k) = halt S )
thus ( ProgramPart s halts_on s implies ex k being Element of NAT st CurInstr (Computation s,k) = halt S ) :: thesis: ( ex k being Element of NAT st CurInstr (Computation s,k) = halt S implies ProgramPart s halts_on s )

proof

given k being Element of NAT such that G1: IC (Computation s,k) in dom (ProgramPart s) and
G2: (ProgramPart s) . (IC (Computation s,k)) = halt S ; :: according to AMI_1:def 20 :: thesis: ex k being Element of NAT st CurInstr (Computation s,k) = halt S
take k ; :: thesis: CurInstr (Computation s,k) = halt S
thus CurInstr (Computation s,k) = halt S by G2, LmX; :: thesis: verum

end;

given k being Element of NAT such that G: CurInstr (Computation s,k) = halt S ; :: thesis: ProgramPart s halts_on s
take k ; :: according to AMI_1:def 20 :: thesis: ( IC (Computation s,k) in dom (ProgramPart s) & (ProgramPart s) . (IC (Computation s,k)) = halt S )
IC (Computation s,k) in NAT by Def4;
hence IC (Computation s,k) in dom (ProgramPart s) by LmU; :: thesis: (ProgramPart s) . (IC (Computation s,k)) = halt S
thus (ProgramPart s) . (IC (Computation s,k)) = halt S by G, LmX; :: thesis: verum