[Termtools] SRS-standard-certifying

[Julien Forest]

Dear all, 


On Sat, 8 Nov 2008 12:01:28 +0100
Simon Bailey <simon.bailey at uibk.ac.at> wrote:

> coqc was hung in an endless loop trying to certify AProVE's output. i  
> had to manually kill that coq process.
> 
> this is the output:
> http://colo5-c703.uibk.ac.at:8080/termcomp/competition/resultDetail.seam?resultId=30355&cid=10511
> 
> maybe somebody can see if that proof is even valid?

The proof is valid but the built-in coq tactic seems to be very very
slow on some goals. 
After a little modification of the script in order to bypass this case,
the proof is checked by coq in 4.32 minutes on my 3GHz computer. 
J.