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