Simplifying termination proofs for rewrite systems by preprocessing
Bernhard Gramlich · 2000
We p r o ve some new results that simplify termination proofs for non-overlapping term rewriting systems.The rst one is a re ned modularity result (for not necessarily disjoint systems).The second, more important one, gives conditions under which the simpli cation of right-hand sides (using rules of the original system) is a sound preprocessing step, in the sense that termination of the original system is equivalent to termination of the simpli ed system, and that the equational theory is preserved.The proofs are based on some powerful structural properties known for nonoverlapping systems.Finally, we show how to (partially) extend these results, in particular, to the case of conditional rewrite systems where we additionally treat simpli cation of conditions of rules.The presented results provide the theoretical basis for sound (and automatic) preprocessing steps when proving termination of (possibly conditional) non-overlapping rewrite systems and equational programs de ned by s u c h systems.Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page.To copy otherwise, to republish, to post on servers or to redistribute to lists, requires prior specific