let N be non empty with_non-empty_elements set ; :: thesis: for S being non empty stored-program IC-Ins-separated definite halting 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 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 EXTPRO_1:def 7 :: 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 EXTPRO_1:def 7 :: 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