ex k being Nat st
( IC (Comput f,s,k) in dom f & CurInstr f,(Comput f,s,k) = halt S ) by A1, Def8;
hence ex b₁ being State of S ex k being Nat st
( b₁ = Comput f,s,k & CurInstr f,b₁ = halt S ) ; :: thesis: verum