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{4, 2 + x1} f#_A(x1) = max{7, -3 + x1} a_A = 1 a#_A = 9 b_A = 4 b#_A = 8 c_A = 1 c#_A = 1 d_A = 4 d#_A = 0 g_A(x1,x2) = max{11, 1 + x1, x2} g#_A(x1,x2) = max{1, -8 + x1, -1} h_A(x1,x2) = max{10, 1 + x1, x2} h#_A(x1,x2) = max{1, 1, -9} e_A = 1 e#_A = 0 precedence: a > b > f > d = g > c = h = e