YES TRS: g(a()) -> g(b()) b() -> f(a(),a()) f(a(),a()) -> g(d()) linear polynomial interpretations on N: g_A(x1) = 0 g#_A(x1) = x1 + 2 a_A = 4 a#_A = 1 b_A = 0 b#_A = 5 f_A(x1,x2) = 0 f#_A(x1,x2) = 4 d_A = 1 d#_A = 0 precedence: a > b > f > g = d