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))) linear polynomial interpretations on N: f_A(x1) = 0 f#_A(x1) = 0 s_A(x1) = 1 s#_A(x1) = 1 g_A(x1) = 1 g#_A(x1) = 2 cons_A(x1,x2) = x1 + x2 + 2 cons#_A(x1,x2) = x2 + 4 0_A = 1 0#_A = 0 h_A(x1) = x1 h#_A(x1) = x1 + 1 precedence: h > cons > g = 0 > s > f