YES Problem: 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))) Proof: DP Processor: DPs: f#(s(X)) -> f#(X) g#(cons(0(),Y)) -> g#(Y) h#(cons(X,Y)) -> g#(cons(X,Y)) h#(cons(X,Y)) -> h#(g(cons(X,Y))) 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))) CDG Processor: DPs: f#(s(X)) -> f#(X) g#(cons(0(),Y)) -> g#(Y) h#(cons(X,Y)) -> g#(cons(X,Y)) h#(cons(X,Y)) -> h#(g(cons(X,Y))) 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))) graph: Qed