YES TRS: f(h(x)) -> f(i(x)) g(i(x)) -> g(h(x)) h(a()) -> b() i(a()) -> b() linear polynomial interpretations on N: f_A(x1) = x1 f#_A(x1) = x1 + 1 h_A(x1) = x1 + 2 h#_A(x1) = 1 i_A(x1) = x1 + 1 i#_A(x1) = 2 g_A(x1) = 0 g#_A(x1) = 3 a_A = 1 a#_A = 1 b_A = 0 b#_A = 0 precedence: f > i > g > h = a > b