YES TRS: a(c(d(x))) -> c(x) u(b(d(d(x)))) -> b(x) v(a(a(x))) -> u(v(x)) v(a(c(x))) -> u(b(d(x))) v(c(x)) -> b(x) w(a(a(x))) -> u(w(x)) w(a(c(x))) -> u(b(d(x))) w(c(x)) -> b(x) linear polynomial interpretations on N: a_A(x1) = x1 + 1 a#_A(x1) = x1 + 1 c_A(x1) = x1 + 1 c#_A(x1) = x1 + 1 d_A(x1) = x1 d#_A(x1) = x1 u_A(x1) = x1 u#_A(x1) = x1 b_A(x1) = x1 + 1 b#_A(x1) = x1 + 1 v_A(x1) = x1 v#_A(x1) = x1 w_A(x1) = x1 w#_A(x1) = x1 precedence: a > c = b > v = w > d = u