defpred S₁[ Nat] means CurInstr (p,(Comput (p,s,$1))) = halt S;
consider k being Nat such that
IC (Comput (p,s,k)) in dom p and
A2: CurInstr (p,(Comput (p,s,k))) = halt S by A1;
A3: ex k being Nat st S₁[k] by A2;
consider k being Nat such that
A4: ( S₁[k] & ( for n being Nat st S₁[n] holds
k <= n ) ) from NAT_1:sch 5(A3);
reconsider k = k as Nat ;
take k ; :: thesis: ( CurInstr (p,(Comput (p,s,k))) = halt S & ( for k being Nat st CurInstr (p,(Comput (p,s,k))) = halt S holds
k <= k ) )
thus ( CurInstr (p,(Comput (p,s,k))) = halt S & ( for k being Nat st CurInstr (p,(Comput (p,s,k))) = halt S holds
k <= k ) ) by A4; :: thesis: verum