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