On termination of the direct sum of term rewriting systems

Michaël Rusinowitch (1)

1 INRIA Lorraine

Some sufficient conditions are given for the termination of the direct sum of two term rewriting systems: either no right-hand-side of a rule is a variable, or no right-hand-side contains more occurences of a variable than the corresponding left-hand-side.

Domaines: Autre [cs.OH]

Michaël Rusinowitch. On termination of the direct sum of term rewriting systems. [Research Report] RR-0679, INRIA. 1987, pp.10. ⟨inria-00075874⟩