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