YES TRS: a__f(g(X),Y) -> a__f(mark(X),f(g(X),Y)) mark(f(X1,X2)) -> a__f(mark(X1),X2) mark(g(X)) -> g(mark(X)) a__f(X1,X2) -> f(X1,X2) linear polynomial interpretations on N: a__f_A(x1,x2) = x1 + 2 a__f#_A(x1,x2) = x1 + 1 g_A(x1) = x1 + 2 g#_A(x1) = 2 mark_A(x1) = x1 + 1 mark#_A(x1) = x1 + 1 f_A(x1,x2) = x1 + 2 f#_A(x1,x2) = 0 precedence: a__f > f > mark > g