let IL be non empty set ; :: thesis: for N being with_non-empty_elements set
for S being non empty stored-program halting IC-Ins-separated steady-programmed definite AMI-Struct of IL,N
for s being State of S holds
( s is halting iff ex k being Element of NAT st s halts_at IC (Computation s,k) )
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 IL,N
for s being State of S holds
( s is halting iff ex k being Element of NAT st s halts_at IC (Computation s,k) )
let S be non empty stored-program halting IC-Ins-separated steady-programmed definite AMI-Struct of IL,N; :: thesis: for s being State of S holds
( s is halting iff ex k being Element of NAT st s halts_at IC (Computation s,k) )
let s be State of S; :: thesis: ( s is halting iff ex k being Element of NAT st s halts_at IC (Computation s,k) )

hereby :: thesis: ( ex k being Element of NAT st s halts_at IC (Computation s,k) implies s is halting )

assume s is halting ; :: thesis: ex k being Element of NAT st s halts_at IC (Computation s,k)
then consider k being Element of NAT such that
A1: CurInstr (Computation s,k) = halt S by Def20;
take k = k; :: thesis: s halts_at IC (Computation s,k)
s . (IC (Computation s,k)) = halt S by A1, Th54;
hence s halts_at IC (Computation s,k) by Def42; :: thesis: verum

end;

given k being Element of NAT such that A2: s halts_at IC (Computation s,k) ; :: thesis: s is halting
take k ; :: according to AMI_1:def 20 :: thesis: CurInstr (Computation s,k) = halt S
thus CurInstr (Computation s,k) = s . (IC (Computation s,k)) by Th54
.= halt S by A2, Def42 ; :: thesis: verum