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) max/plus interpretations on N: f_A(x1) = max{0, x1} f#_A(x1) = max{0, x1} a_A = 0 a#_A = 0 b_A = 0 b#_A = 0 c_A = 0 c#_A = 0 d_A = 0 d#_A = 0 g_A(x1,x2) = max{0, x1, x2} g#_A(x1,x2) = max{0, x1, x2} h_A(x1,x2) = max{0, x1, x2} h#_A(x1,x2) = max{0, x1, x2} e_A = 0 e#_A = 0 precedence: a > b > f = c > d = g = e > h