An Isabelle/HOL Formalization of Rewriting 
for Certified Termination Analysis 


From version 1.12 onwards, CeTA uses the CPF format, version 2.x as input. CeTA versions 1.06 - 1.11 use CPF version 1.0 as input. Older versions of CeTA use this proof format.

Since most elements of CPF are fully supported, we just list some items which might be useful to know when creating proofs that should be read by CeTA.

The archive containing the sources of IsaFoR/CeTA contains a number of examples in the CPF format.