A sufficient condition for the termination of the direct sum of term rewriting systems
Aart Middeldorp · 2003
The author proves a conjecture by Rusinowitch (1987) stating that the direct sum of two terminating term-rewriting systems is terminating if one of the systems contains neither collapsing nor duplicating rules.>