Lambda extensions of rewrite orderings

In this work we provide a new proof of the result by Gallier and Tannen that the combination of an arbitrary terminating first-order rewrite system with the simply typed lambda calculus is strongly normalizing. This proof proceeds via the explicit lifting of a rewrite ordering on first-order terms to a rewrite ordering on (first-order) algebraic lambda-terms. For the definition of the ordering, we have used a technique developed by Kfoury and Wells, in order to delay the erasing beta-reductions (also called K-reductions) which may destroy the monotonicity property. This technique is extended to be able to handle the extensionality rule. As a particular case, the above construction yields an extension of the recursive path ordering of Dershowitz to a rewrite-ordering on (first-order) algebraic lambda-terms which contains simply typed lambda-derivations