This paper extends the termination proof techniques based on reduction orderings to a higher-order setting, by adapting the recursive path ordering definition to higher-order simply-typed lambda-terms. The main result ...