A total AC-compatible reduction ordering on higher-order terms.

The higher-order rewriting in presence of associative and commutative (AC) symbols is considered. A higher-order reduction ordering which allows to state the termination of a given rewriting system is presented. This ordering is an AC-extensiou of λ-RPO and is defined on simply-typed λ-terms in Β-normal η-long form. It is total on ground terms. [ABSTRACT FROM AUTHOR]