An Improved Recursive Decomposition Ordering for Term Rewriting Systems Revisited
Munehiro Iwami · 2005
Simplification orderings, like the recursive path ordering and the improved recursive decomposition ordering, are widely used for proving the termination property of term rewriting systems. The improved recursive decomposition ordering is known as the most powerful simplification ordering. In this paper, we investigate the improved recursive decomposition ordering for proving termination of term rewriting systems. We completely show that the improved recursive decomposition ordering is closed under substitutions.