defpred S1[ Nat] means F . $1 = F . ($1 + 1);
hereby :: thesis: ( not F is halting implies ex b1 being Element of NAT st b1 = 0 )
assume F is halting ; :: thesis: ex IT being Element of NAT st
( S1[IT] & ( for n being Nat st S1[n] holds
IT <= n ) )
then A1: ex n being Nat st S1[n] ;
ex IT being Nat st
( S1[IT] & ( for n being Nat st S1[n] holds
IT <= n ) ) from NAT_1:sch 5(A1);
then consider IT being Nat such that
A2: ( S1[IT] & ( for n being Nat st S1[n] holds
IT <= n ) ) ;
IT in NAT by ORDINAL1:def 12;
hence ex IT being Element of NAT st
( S1[IT] & ( for n being Nat st S1[n] holds
IT <= n ) ) by A2; :: thesis: verum
end;
thus ( not F is halting implies ex b1 being Element of NAT st b1 = 0 ) ; :: thesis: verum