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{7, 2 + x1} f#_A(x1) = max{7, 2 + x1} 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) = max{4, x1, x2} g#_A(x1,x2) = max{4, x1, x2} h_A(x1,x2) = max{1, 1 + x1, x2} h#_A(x1,x2) = max{1, 1 + x1, x2} e_A = 1 e#_A = 1 precedence: a = c > b = d > f > g > h = e