# Is there a name for this property of a term rewriting system?

Given TRS let's call it top-reducible or left-reducible if no rule's right hand side is contained in any rule's left hand side non-trivially.

A term A is contained in an other one B trivially if they overlap at their roots e.g. 2(y) is contained in 1(2(x)) non-trivially while 1(y) is contained in 1(2(x)) trivially) (I also don't know if this 'containment' has a name)

E.g.

• A TRS with a single rule 1(2(x)) -> 2(x) is not top-reducible.
• A TRS with rules 1(2(x)) -> 3(x), 4(3(5(x,y))) -> 1(5(x,y)) is not top-reducible.
• I don't know if your property on rewriting rule has a name, but I'm not sure I completely understand your notion of "trivial containment". Is $a(b,x)$ trivially contained in $a(y,c)$? ($a,b,c$ are function symbols, $x,y$ variables). If yes, then I think what you call "trivial containment" is a symmetric notion (so the terminology "containment" is perhaps a bit misleading) and it's usually called unifiability. – Damiano Mazza Nov 26 '17 at 15:23
• Usually, people refer to "top reducible" as "head reducible" or "having a head redex". Likewise, "contained" should be "matches". The relation is not symmetric, as @DamianoMazza points out. – cody Nov 26 '17 at 18:06

$${\cal R} = \{a \rightarrow b, f(b)\rightarrow f(a)\}$$ (I'm using letters for function symbols instead of numbers, as is traditional). In this case $f(a)$, the right hand side of the second rule, does not match any rule at it's head, but it may match the second rule if you apply the $a\rightarrow b$ reduction inside.
• this is exactly a case I would like to exclude as there is a rule $a\rightarrow b$ which has its rhs $b$ contained non-trivially in an other rule’s lhs $f(b)$, would the first rule be $a\rightarrow f(b)$ it would be okay as then the containment would be trivial – Adam Nov 27 '17 at 20:46