YES Problem: 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)) Proof: DP Processor: DPs: f#(a,empty()) -> g#(a,empty()) f#(a,cons(x,k)) -> f#(cons(x,a),k) g#(cons(x,k),d) -> g#(k,cons(x,d)) 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)) Usable Rule Processor: DPs: f#(a,empty()) -> g#(a,empty()) f#(a,cons(x,k)) -> f#(cons(x,a),k) g#(cons(x,k),d) -> g#(k,cons(x,d)) TRS: CDG Processor: DPs: f#(a,empty()) -> g#(a,empty()) f#(a,cons(x,k)) -> f#(cons(x,a),k) g#(cons(x,k),d) -> g#(k,cons(x,d)) TRS: graph: Qed