YES Problem: a__f(0()) -> cons(0(),f(s(0()))) a__f(s(0())) -> a__f(a__p(s(0()))) a__p(s(0())) -> 0() mark(f(X)) -> a__f(mark(X)) mark(p(X)) -> a__p(mark(X)) mark(0()) -> 0() mark(cons(X1,X2)) -> cons(mark(X1),X2) mark(s(X)) -> s(mark(X)) a__f(X) -> f(X) a__p(X) -> p(X) Proof: DP Processor: DPs: a__f#(s(0())) -> a__p#(s(0())) a__f#(s(0())) -> a__f#(a__p(s(0()))) mark#(f(X)) -> mark#(X) mark#(f(X)) -> a__f#(mark(X)) mark#(p(X)) -> mark#(X) mark#(p(X)) -> a__p#(mark(X)) mark#(cons(X1,X2)) -> mark#(X1) mark#(s(X)) -> mark#(X) TRS: a__f(0()) -> cons(0(),f(s(0()))) a__f(s(0())) -> a__f(a__p(s(0()))) a__p(s(0())) -> 0() mark(f(X)) -> a__f(mark(X)) mark(p(X)) -> a__p(mark(X)) mark(0()) -> 0() mark(cons(X1,X2)) -> cons(mark(X1),X2) mark(s(X)) -> s(mark(X)) a__f(X) -> f(X) a__p(X) -> p(X) CDG Processor: DPs: a__f#(s(0())) -> a__p#(s(0())) a__f#(s(0())) -> a__f#(a__p(s(0()))) mark#(f(X)) -> mark#(X) mark#(f(X)) -> a__f#(mark(X)) mark#(p(X)) -> mark#(X) mark#(p(X)) -> a__p#(mark(X)) mark#(cons(X1,X2)) -> mark#(X1) mark#(s(X)) -> mark#(X) TRS: a__f(0()) -> cons(0(),f(s(0()))) a__f(s(0())) -> a__f(a__p(s(0()))) a__p(s(0())) -> 0() mark(f(X)) -> a__f(mark(X)) mark(p(X)) -> a__p(mark(X)) mark(0()) -> 0() mark(cons(X1,X2)) -> cons(mark(X1),X2) mark(s(X)) -> s(mark(X)) a__f(X) -> f(X) a__p(X) -> p(X) graph: Qed