orthogonal term rewriting system
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
(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,
(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.
"orthogonal term rewriting system." A Dictionary of Computing. . Encyclopedia.com. (March 26, 2019). https://www.encyclopedia.com/computing/dictionaries-thesauruses-pictures-and-press-releases/orthogonal-term-rewriting-system
"orthogonal term rewriting system." A Dictionary of Computing. . Retrieved March 26, 2019 from Encyclopedia.com: https://www.encyclopedia.com/computing/dictionaries-thesauruses-pictures-and-press-releases/orthogonal-term-rewriting-system