defpred S1[ 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 S1[k]
by A2;
consider k being Nat such that
A4:
( S1[k] & ( for n being Nat st S1[n] holds
k <= n ) )
from NAT_1:sch 5(A3);
reconsider k = k as Nat ;
take
k
; ( 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; verum