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)) TDG 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)) graph: g#(cons(x,k),d) -> g#(k,cons(x,d)) -> g#(cons(x,k),d) -> g#(k,cons(x,d)) f#(a,cons(x,k)) -> f#(cons(x,a),k) -> f#(a,cons(x,k)) -> f#(cons(x,a),k) f#(a,cons(x,k)) -> f#(cons(x,a),k) -> f#(a,empty()) -> g#(a,empty()) f#(a,empty()) -> g#(a,empty()) -> g#(cons(x,k),d) -> g#(k,cons(x,d)) 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: 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)) graph: Qed