YES TRS: f(a,empty()) -> g(a,empty()) f(a,cons(x,k)) -> f(cons(x,a),k) g(empty(),d) -> d g(cons(x,k),d) -> g(k,cons(x,d)) linear polynomial interpretations on N: f_A(x1,x2) = x1 + x2 f#_A(x1,x2) = x2 + 2 empty_A = 0 empty#_A = 0 g_A(x1,x2) = x1 + x2 g#_A(x1,x2) = 1 cons_A(x1,x2) = x2 + 1 cons#_A(x1,x2) = 0 precedence: empty > f > g > cons