YES TRS: f(x,c(y)) -> f(x,s(f(y,y))) f(s(x),s(y)) -> f(x,s(c(s(y)))) linear polynomial interpretations on N: f_A(x1,x2) = 1 f#_A(x1,x2) = x2 c_A(x1) = x1 + 4 c#_A(x1) = 1 s_A(x1) = 3 s#_A(x1) = 2 precedence: f > c > s