let N be non empty with_non-empty_elements set ; :: thesis: for S being non empty stored-program halting IC-Ins-separated definite AMI-Struct of N
for p being NAT -defined the Instructions of b₁ -valued finite Function
for s being State of S holds
( p halts_on s iff ex k being Nat st p halts_at IC (Comput p,s,k) )
let S be non empty stored-program halting IC-Ins-separated definite AMI-Struct of N; :: thesis: for p being NAT -defined the Instructions of S -valued finite Function
for s being State of S holds
( p halts_on s iff ex k being Nat st p halts_at IC (Comput p,s,k) )
let p be NAT -defined the Instructions of S -valued finite Function; :: thesis: for s being State of S holds
( p halts_on s iff ex k being Nat st p halts_at IC (Comput p,s,k) )
let s be State of S; :: thesis: ( p halts_on s iff ex k being Nat st p halts_at IC (Comput p,s,k) )

hereby :: thesis: ( ex k being Nat st p halts_at IC (Comput p,s,k) implies p halts_on s )

assume p halts_on s ; :: thesis: ex k being Nat st p halts_at IC (Comput p,s,k)
then consider k being Nat such that
A0: IC (Comput p,s,k) in dom p and
A1: CurInstr p,(Comput p,s,k) = halt S by Def8;
take k = k; :: thesis: p halts_at IC (Comput p,s,k)
p . (IC (Comput p,s,k)) = halt S by A1, A0, PARTFUN1:def 8;
hence p halts_at IC (Comput p,s,k) by A0, Def15; :: thesis: verum

end;

given k being Nat such that A2: p halts_at IC (Comput p,s,k) ; :: thesis: p halts_on s
take k ; :: according to SCMNORM:def 8 :: thesis: ( IC (Comput p,s,k) in dom p & CurInstr p,(Comput p,s,k) = halt S )
thus K: IC (Comput p,s,k) in dom p by A2, Def15; :: thesis: CurInstr p,(Comput p,s,k) = halt S
thus CurInstr p,(Comput p,s,k) = p /. (IC (Comput p,s,k))
.= p . (IC (Comput p,s,k)) by K, PARTFUN1:def 8
.= halt S by A2, Def15 ; :: thesis: verum