YES TRS: f(x,0()) -> s(0()) f(s(x),s(y)) -> s(f(x,y)) g(0(),x) -> g(f(x,x),x) max/plus interpretations on N: f_A(x1,x2) = max{1, -2, -2} f#_A(x1,x2) = max{1, -4, -5} 0_A = 5 0#_A = 0 s_A(x1) = max{1, 1} s#_A(x1) = max{1, -4 + x1} g_A(x1,x2) = max{0, x1, 0} g#_A(x1,x2) = max{2, -2 + x1, 0} precedence: g > f > 0 = s