higher-order prover のこと（４）

勿論

echo 'thf(nat,type,nat : $tType).
thf(z,type,z : nat).
thf(suc,type,suc : nat > nat).
thf(nat_induction,axiom,( ! [P : nat > $o] :
	(((P @ z) & (! [N : nat] : ((P @ N) => (P @ (suc @ N))))) =>
         (! [N : nat] : (P @ N))) )).
thf(f,type,f : nat > $o).
thf(gl,conjecture,( 
	( (((f @ z) & (f @ (suc @ z))) &
           (! [N : nat] : (((f @ N) & (f @ (suc @ N))) => (f @ (suc @ (suc @ N)))))) =>
          (! [N : nat] : ((f @ N) & (f @ (suc @ N))) )) )).
'> demo3.p
satallax -p coqscript -c ./demo3.v ./demo3.p
coqide ./demo3.v

も通りますが，結論を

(! [N : nat] : (f @ N) )

だけにするとやはり帰って来ません．この辺り，TPS（ http://gtps.math.cmu.edu/tps.html ）だと

% SZS status Theorem
+++ TPS proved gl using mode MODE-THM122-PR97 in 0 seconds. +++

と答えてくれるのは年季の違いでしょう．