Well-foundedness of the Recursive Path Ordering in Coq
N. de Kleijn, Adam Koprowski, Femke van Raamsdonk · 2004
The recursive path ordering due to Dershowitz is one of the important methods to prove termination of first-order term rewriting. The generalization to the higher-order case is due to Jouannaud and Rubio. This work is concerned with a formalization in Coq of the proof of wellfoundedness of both the first- and the higher-order version of the recursive path ordering. The proof does not rely on Kruskal’s tree theorem. 1