How to prove Equ iva lence o f Term Rewr i t ing Sys tems w i thout Induct ion

A simple method is proposed for testing equivalence in a restricted omain of two given term rewriting systems. By using the Church-Rosser p operty and the teachability of term rewriting systems, the method allows us to prove equivalence of these systems without the explicit use of induction; this proof usually requires ome kind of induction. The method proposed is a general extension of inductionless induction methods developed by Musser, Goguen, Huet and HuUot, and allows us to extend inductionless induetior ~ concepts to not only term rewriting systems with the termination property, but also various reduction systems: term rewriting systems without the termination property, string rewriting systems, graph rewriting systems, combinatory eduction systems, and resolution systems. This method is applied to test equivalence of term rewriting systems, to prove the inductive theorems, and to derive a new term rewriting system from a given system by using equivalence transformation rules. 1