YES TRS: f(a(),h(x)) -> f(g(x),h(x)) h(g(x)) -> h(a()) g(h(x)) -> g(x) h(h(x)) -> x max/plus interpretations on N: f_A(x1,x2) = max{0, 7 + x1, 0} f#_A(x1,x2) = max{3, x1, 2} a_A = 4 a#_A = 0 h_A(x1) = max{5, 1 + x1} h#_A(x1) = max{9, 5 + x1} g_A(x1) = max{1, -6} g#_A(x1) = max{1, -1} precedence: h > f > g > a