defpred S_{1}[ 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_{1}[k]
by A2;

consider k being Nat such that

A4: ( S_{1}[k] & ( for n being Nat st S_{1}[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

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

consider k being Nat such that

A4: ( S

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