Proving termination of higher-order rewrite systems / J.C. van de Pol
Proving termination of higher-order rewrite systems