### Abstract

This Isabelle/HOL formalization defines recursive path orders (RPOs) for higher-order terms without lambda-abstraction and proves many useful properties about them. The main order fully coincides with the standard RPO on first-order terms also in the presence of currying, distinguishing it from previous work. An optimized variant is formalized as well. It appears promising as the basis of a higher-order superposition calculus.

BSD License### Depends On

### Used by

- Saturation_Framework
- Higher_Order_Terms
- Functional_Ordered_Resolution_Prover
- Lambda_Free_EPO
- Lambda_Free_KBOs