Recursive path ordering (RPO) is a well-known reduction ordering introduced by Dershowitz, that is useful for proving termination of term rewriting systems (TRSs). Jouannaud and Rubio generalized this ordering to the higher-order case thus creating the higher-order recursive path ordering (HORPO). They proved that this ordering can be used for proving termination of higher-order TRSs which essentially comes down to proving well-foundedness of the union of HORPO and the bete reduction relation of the simply typed lambda calculus. This result entails well-foundedness of RPO and termination of simply typed lambda calculus.

This paper describes author's undertaking of providing a complete, axiom-free, fully constructive formalization of those results in the theorem prover Coq. Formalization is complete and hence it contains all the dependant results. It can be divided into three parts:

• finite multisets and two variants of multiset extensions of a relation,
• simply typed lambda calculus with termination of beta-reduction as the main result,
• HORPO with proof of well-foundedness of its union with beta-reduction. Also decidability of HORPO has been proven and due to the constructive nature of this proof a certified algorithm to verify whether two terms can be oriented with HORPO can be extracted from this proof.