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 NAT -defined the Instructions of b₁ -valued Function
for s being State of S holds
( p halts_on s iff ex i being Element of NAT st p halts_at IC (Comput (p,s,i)) )
let S be non empty IC-Ins-separated halting AMI-Struct of N; :: thesis: for p being NAT -defined the Instructions of S -valued Function
for s being State of S holds
( p halts_on s iff ex i being Element of NAT st p halts_at IC (Comput (p,s,i)) )
let p be NAT -defined the Instructions of S -valued Function; :: thesis: for s being State of S holds
( p halts_on s iff ex i being Element of NAT st p halts_at IC (Comput (p,s,i)) )
let s be State of S; :: thesis: ( p halts_on s iff ex i being Element of NAT st p halts_at IC (Comput (p,s,i)) )

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

assume p halts_on s ; :: thesis: ex i being Element of NAT st p halts_at IC (Comput (p,s,i))
then consider i being Nat such that
A1: IC (Comput (p,s,i)) in dom p and
A2: CurInstr (p,(Comput (p,s,i))) = halt S by Def7;
reconsider i = i as Element of NAT by ORDINAL1:def 12;
take i = i; :: thesis: p halts_at IC (Comput (p,s,i))
p . (IC (Comput (p,s,i))) = halt S by A1, A2, PARTFUN1:def 6;
hence p halts_at IC (Comput (p,s,i)) by A1, COMPOS_1:def 6; :: thesis: verum

end;

given i being Element of NAT such that A3: p halts_at IC (Comput (p,s,i)) ; :: thesis: p halts_on s
A4: IC (Comput (p,s,i)) in dom p by A3, COMPOS_1:def 6;
A5: p . (IC (Comput (p,s,i))) = halt S by A3, COMPOS_1:def 6;
take i ; :: according to EXTPRO_1:def 8 :: thesis: ( IC (Comput (p,s,i)) in dom p & CurInstr (p,(Comput (p,s,i))) = halt S )
thus IC (Comput (p,s,i)) in dom p by A3, COMPOS_1:def 6; :: thesis: CurInstr (p,(Comput (p,s,i))) = halt S
thus CurInstr (p,(Comput (p,s,i))) = halt S by A4, A5, PARTFUN1:def 6; :: thesis: verum