Dummy elimination: Making termination easier

Abstract

We investigate a technique whose goal is to simplify the task of proving termination of term rewriting systems. The technique consists of a transformation which eliminates function symbols considered “useless” and simplifies the rewrite rules. We show that the transformation is sound, i. e., termination of the original system can be inferred from termination of the transformed one. For proving this result we use a new notion of lifting of orders that is a generalization of the multiset construction.