Outermost-Fair Rewriting


A rewrite sequence is said to be outermost-fair if every outermost redex occurrence is eventually eliminated. O'Donnell has shown that outermost-fair rewriting is normalising for almost orthogonal first-order term rewriting systems. In this paper we extend this result to the higher-order case.