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