### Abstract

This Isabelle/HOL formalization defines the Embedding Path Order (EPO)
for higher-order terms without lambda-abstraction and proves many
useful properties about it. In contrast to the lambda-free recursive
path orders, it does not fully coincide with RPO on first-order terms,
but it is compatible with arbitrary higher-order contexts.

BSD License