YES Problem: d(0()) -> 0() d(s(x)) -> s(s(d(x))) e(s(x),y) -> e(x,d(y)) sup(s(x),e(0(),y)) -> sup(x,e(y,s(0()))) Proof: DP Processor: DPs: d#(s(x)) -> d#(x) e#(s(x),y) -> d#(y) e#(s(x),y) -> e#(x,d(y)) sup#(s(x),e(0(),y)) -> e#(y,s(0())) sup#(s(x),e(0(),y)) -> sup#(x,e(y,s(0()))) TRS: d(0()) -> 0() d(s(x)) -> s(s(d(x))) e(s(x),y) -> e(x,d(y)) sup(s(x),e(0(),y)) -> sup(x,e(y,s(0()))) TDG Processor: DPs: d#(s(x)) -> d#(x) e#(s(x),y) -> d#(y) e#(s(x),y) -> e#(x,d(y)) sup#(s(x),e(0(),y)) -> e#(y,s(0())) sup#(s(x),e(0(),y)) -> sup#(x,e(y,s(0()))) TRS: d(0()) -> 0() d(s(x)) -> s(s(d(x))) e(s(x),y) -> e(x,d(y)) sup(s(x),e(0(),y)) -> sup(x,e(y,s(0()))) graph: sup#(s(x),e(0(),y)) -> sup#(x,e(y,s(0()))) -> sup#(s(x),e(0(),y)) -> sup#(x,e(y,s(0()))) sup#(s(x),e(0(),y)) -> sup#(x,e(y,s(0()))) -> sup#(s(x),e(0(),y)) -> e#(y,s(0())) sup#(s(x),e(0(),y)) -> e#(y,s(0())) -> e#(s(x),y) -> e#(x,d(y)) sup#(s(x),e(0(),y)) -> e#(y,s(0())) -> e#(s(x),y) -> d#(y) 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: 3 #rules: 3 #arcs: 8/25 DPs: sup#(s(x),e(0(),y)) -> sup#(x,e(y,s(0()))) TRS: d(0()) -> 0() d(s(x)) -> s(s(d(x))) e(s(x),y) -> e(x,d(y)) sup(s(x),e(0(),y)) -> sup(x,e(y,s(0()))) Subterm Criterion Processor: simple projection: pi(sup#) = 0 problem: DPs: TRS: d(0()) -> 0() d(s(x)) -> s(s(d(x))) e(s(x),y) -> e(x,d(y)) sup(s(x),e(0(),y)) -> sup(x,e(y,s(0()))) Qed DPs: e#(s(x),y) -> e#(x,d(y)) TRS: d(0()) -> 0() d(s(x)) -> s(s(d(x))) e(s(x),y) -> e(x,d(y)) sup(s(x),e(0(),y)) -> sup(x,e(y,s(0()))) Subterm Criterion Processor: simple projection: pi(e#) = 0 problem: DPs: TRS: d(0()) -> 0() d(s(x)) -> s(s(d(x))) e(s(x),y) -> e(x,d(y)) sup(s(x),e(0(),y)) -> sup(x,e(y,s(0()))) Qed DPs: d#(s(x)) -> d#(x) TRS: d(0()) -> 0() d(s(x)) -> s(s(d(x))) e(s(x),y) -> e(x,d(y)) sup(s(x),e(0(),y)) -> sup(x,e(y,s(0()))) Subterm Criterion Processor: simple projection: pi(d#) = 0 problem: DPs: TRS: d(0()) -> 0() d(s(x)) -> s(s(d(x))) e(s(x),y) -> e(x,d(y)) sup(s(x),e(0(),y)) -> sup(x,e(y,s(0()))) Qed