The Coq mailing list

[Thery Laurent <thery AT ns.di.univaq.it>]

Hi,

> while competing with other provers at the ICMS conference, I was quite 
> embarassed by some bugs in the fourier procedure. Here are some examples:

For those interested by the competition, here is the link:

http://www.cs.ru.nl/~freek/demos/index.html

please have a go to reduce the De-Bruijn factor (the factor between
the size of the formalized proof and the pen and paper proof).
I'm sure we can do much better than my poor 2.0.

--
Laurent