YES TRS: f(s(X)) -> f(X) g(cons(0(),Y)) -> g(Y) g(cons(s(X),Y)) -> s(X) h(cons(X,Y)) -> h(g(cons(X,Y))) max/plus interpretations on N: f_A(x1) = max{0, 0} f#_A(x1) = max{11, 14} s_A(x1) = max{3, 1} s#_A(x1) = max{12, 13} g_A(x1) = max{3, -8 + x1} g#_A(x1) = max{10, 5 + x1} cons_A(x1,x2) = max{4, -1, 6 + x2} cons#_A(x1,x2) = max{7, 6, 14 + x2} 0_A = 1 0#_A = 0 h_A(x1) = max{0, 5 + x1} h#_A(x1) = max{0, 5 + x1} precedence: cons > h > f = g > s = 0