YES TRS: f(a()) -> b() f(c()) -> d() f(g(x,y)) -> g(f(x),f(y)) f(h(x,y)) -> g(h(y,f(x)),h(x,f(y))) g(x,x) -> h(e(),x) linear polynomial interpretations on N: f_A(x1) = x1 + 1 f#_A(x1) = 2 a_A = 1 a#_A = 1 b_A = 0 b#_A = 0 c_A = 1 c#_A = 1 d_A = 0 d#_A = 0 g_A(x1,x2) = 1 g#_A(x1,x2) = 1 h_A(x1,x2) = 1 h#_A(x1,x2) = 0 e_A = 1 e#_A = 0 precedence: g > f = c = e > b = d = h > a