[Termtools] New elements in CPF

[René Thiemann]

Dear all,

some elements have been added to the certification problem format (CPF) in the area of
termination proofs.


- conditional rewrite systems and unravellings.
- removal of non-applicable rules for innermost rewriting
- general reduction pair processor / bounded increase.

Comments are welcome, and if there are none, then these elements will be fixed by January 15, 2013.

See http://cl-informatik.uibk.ac.at/software/cpf/#devel for more details.

Best regards,
René