YES TRS: a__f(a(),X,X) -> a__f(X,a__b(),b()) a__b() -> a() mark(f(X1,X2,X3)) -> a__f(X1,mark(X2),X3) mark(b()) -> a__b() mark(a()) -> a() a__f(X1,X2,X3) -> f(X1,X2,X3) a__b() -> b() linear polynomial interpretations on N: a__f_A(x1,x2,x3) = x1 + x2 + x3 a__f#_A(x1,x2,x3) = x1 + x3 + 2 a_A = 1 a#_A = 1 a__b_A = 1 a__b#_A = 2 b_A = 0 b#_A = 0 mark_A(x1) = x1 + 1 mark#_A(x1) = x1 + 3 f_A(x1,x2,x3) = x1 + x2 + x3 f#_A(x1,x2,x3) = x3 + 1 precedence: f > mark > a__f > a__b > a > b