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)) SCC Processor: #sccs: 2 #rules: 2 #arcs: 4/9 DPs: f#(a,cons(x,k)) -> f#(cons(x,a),k) 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)) Subterm Criterion Processor: simple projection: pi(f#) = 1 problem: DPs: 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)) Qed DPs: 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)) Subterm Criterion Processor: simple projection: pi(g#) = 0 problem: DPs: 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)) Qed