There are several useful conditions on the set E of equations defining a term rewriting system that lead to a well-behaved reduction system →_E. A commonly used condition is orthogonality. If a set E of equations is orthogonal then its term rewriting system →_E is Church–Rosser. A set of equations is orthogonal if it is left-linear and nonoverlapping:

the set E of equations is left-linear if for all t = t′ ∊ E, each variable that appears in t does so only once;

the set E of equations is nonoverlapping if

1. (a) for any pair of different equations t = t′, r = r′ ∊ E, the terms t and r do not overlap in the following sense—there exist closed substitutions τ‎ ρ‎ of t, r such that ρ‎(r) is a subterm of τ‎(t) and the outermost function symbol of ρ‎(r) occurs as part of t,

2. (b) for any rule t = t′ ∊ E, t does not overlap with itself in the following sense—there exist closed substitutions τ‎, ρ‎ of t such that τ‎(t) is a proper subterm of ρ‎(t) and the outermost function symbol of τ‎(t) occurs as a part of t.