[Termtools] Certified ERROR for TRS/ARroVE/improved_usable.trs

[Koprowski, A.]

  Well, it seems that you are using the improved version of dependency pairs (ignoring those pairs where rhs is a subterm of lhs). This has not been formalized in CoLoR (yet) and hence the "classical" version is used. Sorry, I forgot to tell you about that :-(. But it should be made clear that it's not a bug in TTT2 nor in CoLoR/Rainbow.

  Best wishes,
   Adam

-----Original Message-----
From: termtools-bounces at lists.lri.fr on behalf of Christian Sternagel
Sent: Tue 6/5/2007 20:59
To: termtools
Subject: [Termtools] Certified ERROR for TRS/ARroVE/improved_usable.trs
 
There is obviously an error when certifying the proof of improved_usable.trs.
And I get the same error when certifying on my mashine.
The only problem is that I can not find an error in neither the text-proof nor
the xml-proof produced by ttt2.
These two outputs are not provided on the competition homepage, so I attached
them. Since I'm not a Coq expert at all I do not know the exact problem, maybe
one of the experts could have a look?

cheers

christian