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