YES TRS: f(a()) -> g(h(a())) h(g(x)) -> g(h(f(x))) k(x,h(x),a()) -> h(x) k(f(x),y,x) -> f(x) linear polynomial interpretations on N: f_A(x1) = x1 + 1 f#_A(x1) = x1 a_A = 5 a#_A = 0 g_A(x1) = 2 g#_A(x1) = x1 + 1 h_A(x1) = 2 h#_A(x1) = 4 k_A(x1,x2,x3) = x1 + x3 k#_A(x1,x2,x3) = x1 + 5 precedence: k > h > g > f > a