Erasure and Termination in Higher-Order Rewriting
Jeroen Ketema, Femke van Raamsdonk · 2004
Abstract. Two applications of the Erasure Lemma for first-order orthogonal term rewriting systems are: weak innermost termination implies termination, and weak normalization implies strong normalization for non-erasing systems. We discuss these two results in the setting of higher-order rewriting. 1