Well-foundedness of the recursive path ordering in Coq (2004)
Nicole De Kleijn, Adam Koprowski, Femke Van Raamsdonk
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...