Type introduction for equational rewriting

Type introduction is a useful technique for simplifying the task of proving properties of rewrite systems by restricting the set of terms that have to be considered to the well-typed terms according to any many-sorted type di scipline which is compatible with the rewrite system under consideration. A property of rewrite systems for which type introduction is correct is call ed persistent. Zantema showed that termination is a persistent property of noncollapsing rewrite systems and non-duplicating rewrite systems. We exten d his result to the more complicated case of equational rewriting. As a sim ple application we prove the undecidability of AC-termination for terminati ng rewrite systems. We also present sufficient conditions for the persisten ce of acyclicity and non-loopingness, two properties which guarantee the ab sence of certain kinds of infinite rewrite sequences. In the final part of the paper we show how our results on persistence give rise to new modularit y results.