YES TRS: f(x) -> s(x) f(s(s(x))) -> s(f(f(x))) linear polynomial interpretations on N: f_A(x1) = x1 + 1 f#_A(x1) = x1 + 1 s_A(x1) = x1 + 1 s#_A(x1) = x1 + 1 precedence: f > s