Tree lifting orderings for termination transformations of term rewriting systems
Takahito Aoto, Yoshihito Toyama · 1997
A technique to prove the termination of a given term rewriting system (TRS, for short) is presented. We propose tree lifting orderings by which from a given TRS R candidates for the termination of R can be obtained---the termination of (at least) one of these candidates guarantees the termination of R. It should be remarked that for a given finite TRS all its candidates can be computed automatically.