[Termtools] Rainbow: new release

[Frederic Blanqui]

Hello!

On http://color.inria.fr, you will find a new release of Rainbow, an 
automated verifier of termination certificates.

Since the last release on March 16, Rainbow can now:

- supports the following termination problem formats: the old TPDB 
formats .trs/.srs, the new TPDB format.xtc and its own format .pb.

- supports the following termination certificates formats: the format 
.xtc and its own format .prf.

- verify loops for relative (including modulo AC) TRSs or SRSs (in CPF, 
use an attribute [type="rel"] for relative or AC steps).

- verify all argument filterings (including collapsing ones, but without 
permutation of arguments) both as system transformations or for defining 
reduction orderings.

- flat context closure, root labelling and unlabelling.

- verify RPO proofs by using the Coccinelle library 
(http://a3pat.ensiie.fr/).

Finally, Rainbow efficiency in Coq has been improved. Some recent 
experiments show that Rainbow can verify more than 700 certificates 
obtained from TRS problems (instead of 558 in last year competition), 
each certificate being verified in about 6s in average (0.5s for loops), 
that is about 25% of the time required for finding the certificate.

Feedbacks on using Rainbow are very welcome!