let N be non empty 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 s halts_at IC (Comput (ProgramPart s),s,k) )
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 s halts_at IC (Comput (ProgramPart s),s,k) )
let s be State of S; :: thesis: ( ProgramPart s halts_on s iff ex k being Element of NAT st s halts_at IC (Comput (ProgramPart s),s,k) )

hereby :: thesis: ( ex k being Element of NAT st s halts_at IC (Comput (ProgramPart s),s,k) implies ProgramPart s halts_on s )

assume ProgramPart s halts_on s ; :: thesis: ex k being Element of NAT st s halts_at IC (Comput (ProgramPart s),s,k)
then consider k being Element of NAT such that
IC (Comput (ProgramPart s),s,k) in dom (ProgramPart s) and
A1: (ProgramPart s) /. (IC (Comput (ProgramPart s),s,k)) = halt S by Def20;
take k = k; :: thesis: s halts_at IC (Comput (ProgramPart s),s,k)
Y: (ProgramPart (Comput (ProgramPart s),s,k)) /. (IC (Comput (ProgramPart s),s,k)) = (Comput (ProgramPart s),s,k) . (IC (Comput (ProgramPart s),s,k)) by BWL1;
(ProgramPart s) /. (IC (Comput (ProgramPart s),s,k)) = CurInstr (ProgramPart (Comput (ProgramPart s),s,k)),(Comput (ProgramPart s),s,k) by LmX;
then s . (IC (Comput (ProgramPart s),s,k)) = halt S by A1, Th54, Y;
hence s halts_at IC (Comput (ProgramPart s),s,k) by Def42; :: thesis: verum

end;

given k being Element of NAT such that A2: s halts_at IC (Comput (ProgramPart s),s,k) ; :: thesis: ProgramPart s halts_on s
take k ; :: according to AMI_1:def 20 :: thesis: ( IC (Comput (ProgramPart s),s,k) in dom (ProgramPart s) & (ProgramPart s) /. (IC (Comput (ProgramPart s),s,k)) = halt S )
Y: (ProgramPart (Comput (ProgramPart s),s,k)) /. (IC (Comput (ProgramPart s),s,k)) = (Comput (ProgramPart s),s,k) . (IC (Comput (ProgramPart s),s,k)) by BWL1;
IC (Comput (ProgramPart s),s,k) in NAT ;
hence IC (Comput (ProgramPart s),s,k) in dom (ProgramPart s) by LmU; :: thesis: (ProgramPart s) /. (IC (Comput (ProgramPart s),s,k)) = halt S
CurInstr (ProgramPart (Comput (ProgramPart s),s,k)),(Comput (ProgramPart s),s,k) = s . (IC (Comput (ProgramPart s),s,k)) by Th54, Y
.= halt S by A2, Def42 ;
hence (ProgramPart s) /. (IC (Comput (ProgramPart s),s,k)) = halt S by LmX; :: thesis: verum