consider k being Nat such that
IC (Comput p,s,k) in dom p and
W: CurInstr p,(Comput p,s,k) = halt S by A1, Def20;
k in NAT by ORDINAL1:def 13;
hence ex b₁ being State of S ex k being Element of NAT st
( b₁ = Comput p,s,k & CurInstr p,b₁ = halt S ) by W; :: thesis: verum