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)) -&gt; 2(x) is not top-reducible.
A TRS with rules 1(2(x)) -&gt; 3(x), 4(3(5(x,y))) -&gt; 1(5(x,y)) is not top-reducible.
I'm not sure there is a name for this specific property, though I would say "All right-hand sides are in head-normal form".

To be honest, this seems like a very strange property to request, especially since an inner reduction may provoke a head reduction, like so:

$$ {\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.