[Termtools] future of termination competitions - discussion at WST

[Frederic Blanqui]

hello. i suggest the following points:

- run the certifying competition also on srs, fp, etc. (well, if at least one
tool can handle these systems)

- in statistics of the certifying competition, print also the size of the
coq proofs

- add a new category: simply-typed higher-order rewriting
. albert rubio has a running implementation of horpo
. i would like to write a prototype for this category too
. other people may be interested
. we should collect various examples: i believe that femke van raamsdonk has a
list on her web page