let N be non empty with_non-empty_elements set ; :: thesis: for S being non empty IC-Ins-separated halting AMI-Struct of N
for P being Instruction-Sequence of S
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 IC-Ins-separated halting AMI-Struct of N; :: thesis: for P being Instruction-Sequence of S
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 Instruction-Sequence of S; :: 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
A1: CurInstr (P,(Comput (P,s,k))) = halt S ; :: according to EXTPRO_1:def 8 :: 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 12; :: thesis: CurInstr (P,(Comput (P,s,k))) = halt S
thus CurInstr (P,(Comput (P,s,k))) = halt S by A1; :: thesis: verum

end;

given k being Element of NAT such that A2: CurInstr (P,(Comput (P,s,k))) = halt S ; :: thesis: P halts_on s
take k ; :: according to EXTPRO_1:def 8 :: 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 2; :: thesis: CurInstr (P,(Comput (P,s,k))) = halt S
thus CurInstr (P,(Comput (P,s,k))) = halt S by A2; :: thesis: verum