YES Problem: d(0()) -> 0() d(s(x)) -> s(s(d(x))) e(0(),x) -> x e(s(x),y) -> e(x,d(y)) Proof: DP Processor: DPs: d#(s(x)) -> d#(x) e#(s(x),y) -> d#(y) e#(s(x),y) -> e#(x,d(y)) TRS: d(0()) -> 0() d(s(x)) -> s(s(d(x))) e(0(),x) -> x e(s(x),y) -> e(x,d(y)) TDG Processor: DPs: d#(s(x)) -> d#(x) e#(s(x),y) -> d#(y) e#(s(x),y) -> e#(x,d(y)) TRS: d(0()) -> 0() d(s(x)) -> s(s(d(x))) e(0(),x) -> x e(s(x),y) -> e(x,d(y)) graph: e#(s(x),y) -> e#(x,d(y)) -> e#(s(x),y) -> e#(x,d(y)) e#(s(x),y) -> e#(x,d(y)) -> e#(s(x),y) -> d#(y) e#(s(x),y) -> d#(y) -> d#(s(x)) -> d#(x) d#(s(x)) -> d#(x) -> d#(s(x)) -> d#(x) SCC Processor: #sccs: 2 #rules: 2 #arcs: 4/9 DPs: e#(s(x),y) -> e#(x,d(y)) TRS: d(0()) -> 0() d(s(x)) -> s(s(d(x))) e(0(),x) -> x e(s(x),y) -> e(x,d(y)) Subterm Criterion Processor: simple projection: pi(e#) = 0 problem: DPs: TRS: d(0()) -> 0() d(s(x)) -> s(s(d(x))) e(0(),x) -> x e(s(x),y) -> e(x,d(y)) Qed DPs: d#(s(x)) -> d#(x) TRS: d(0()) -> 0() d(s(x)) -> s(s(d(x))) e(0(),x) -> x e(s(x),y) -> e(x,d(y)) Subterm Criterion Processor: simple projection: pi(d#) = 0 problem: DPs: TRS: d(0()) -> 0() d(s(x)) -> s(s(d(x))) e(0(),x) -> x e(s(x),y) -> e(x,d(y)) Qed