[Termtools] oops

[Johannes Waldmann]

Matchbox just "proved" termination of
TRS/TRCSR/Ex1_2_Luc02c_L.trs = (VAR X Y  )
(RULES 2nd ( cons ( X ) ) -> Y  from ( X ) -> cons ( X ) )
and of course Coq rejected that.

Somehow this restores my faith in verification,
and I'm happy to withdraw matchbox from the category.

(Its performance isn't too exciting anyway, so the purpose
of avdertising Color is better served by Aprove's results.)

Best regards, Johannes.



-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 257 bytes
Desc: OpenPGP digital signature
Url : http://lists.lri.fr/pipermail/termtools/attachments/20081111/68cc0f7e/attachment.pgp