YES Problem: f(empty(),l) -> l f(cons(x,k),l) -> g(k,l,cons(x,k)) g(a,b,c) -> f(a,cons(b,c)) Proof: DP Processor: DPs: f#(cons(x,k),l) -> g#(k,l,cons(x,k)) g#(a,b,c) -> f#(a,cons(b,c)) TRS: f(empty(),l) -> l f(cons(x,k),l) -> g(k,l,cons(x,k)) g(a,b,c) -> f(a,cons(b,c)) TDG Processor: DPs: f#(cons(x,k),l) -> g#(k,l,cons(x,k)) g#(a,b,c) -> f#(a,cons(b,c)) TRS: f(empty(),l) -> l f(cons(x,k),l) -> g(k,l,cons(x,k)) g(a,b,c) -> f(a,cons(b,c)) graph: g#(a,b,c) -> f#(a,cons(b,c)) -> f#(cons(x,k),l) -> g#(k,l,cons(x,k)) f#(cons(x,k),l) -> g#(k,l,cons(x,k)) -> g#(a,b,c) -> f#(a,cons(b,c)) Subterm Criterion Processor: simple projection: pi(f#) = 0 pi(g#) = 0 problem: DPs: g#(a,b,c) -> f#(a,cons(b,c)) TRS: f(empty(),l) -> l f(cons(x,k),l) -> g(k,l,cons(x,k)) g(a,b,c) -> f(a,cons(b,c)) SCC Processor: #sccs: 0 #rules: 0 #arcs: 2/1