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

proof

given k being Nat such that IC (Comput P,s,k) in dom P and
G2: CurInstr P,(Comput P,s,k) = halt S ; :: according to AMI_1:def 20 :: thesis: ex k being Element of NAT st CurInstr P,(Comput P,s,k) = halt S
take k ; :: thesis: ( k is Element of NAT & CurInstr P,(Comput P,s,k) = halt S )
thus k is Element of NAT by ORDINAL1:def 13; :: thesis: CurInstr P,(Comput P,s,k) = halt S
thus CurInstr P,(Comput P,s,k) = halt S by G2; :: thesis: verum

end;

given k being Element of NAT such that G: CurInstr P,(Comput P,s,k) = halt S ; :: thesis: P halts_on s
take k ; :: according to AMI_1:def 20 :: thesis: ( IC (Comput P,s,k) in dom P & CurInstr P,(Comput P,s,k) = halt S )
IC (Comput P,s,k) in NAT ;
hence IC (Comput P,s,k) in dom P by PARTFUN1:def 4; :: thesis: CurInstr P,(Comput P,s,k) = halt S
thus CurInstr P,(Comput P,s,k) = halt S by G; :: thesis: verum