YES Problem: d(0()) -> 0() d(s(x)) -> s(s(d(x))) e(0()) -> s(0()) e(r(x)) -> d(e(x)) Proof: DP Processor: DPs: d#(s(x)) -> d#(x) e#(r(x)) -> e#(x) e#(r(x)) -> d#(e(x)) TRS: d(0()) -> 0() d(s(x)) -> s(s(d(x))) e(0()) -> s(0()) e(r(x)) -> d(e(x)) TDG Processor: DPs: d#(s(x)) -> d#(x) e#(r(x)) -> e#(x) e#(r(x)) -> d#(e(x)) TRS: d(0()) -> 0() d(s(x)) -> s(s(d(x))) e(0()) -> s(0()) e(r(x)) -> d(e(x)) graph: e#(r(x)) -> e#(x) -> e#(r(x)) -> d#(e(x)) e#(r(x)) -> e#(x) -> e#(r(x)) -> e#(x) e#(r(x)) -> d#(e(x)) -> 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#(r(x)) -> e#(x) TRS: d(0()) -> 0() d(s(x)) -> s(s(d(x))) e(0()) -> s(0()) e(r(x)) -> d(e(x)) Arctic Interpretation Processor: dimension: 1 interpretation: [e#](x0) = -8x0 + 2, [r](x0) = 8x0 + 12, [e](x0) = -7x0 + 4, [s](x0) = 0, [d](x0) = x0 + 2, [0] = 0 orientation: e#(r(x)) = x + 4 >= -8x + 2 = e#(x) d(0()) = 2 >= 0 = 0() d(s(x)) = 2 >= 0 = s(s(d(x))) e(0()) = 4 >= 0 = s(0()) e(r(x)) = 1x + 5 >= -7x + 4 = d(e(x)) problem: DPs: TRS: d(0()) -> 0() d(s(x)) -> s(s(d(x))) e(0()) -> s(0()) e(r(x)) -> d(e(x)) Qed DPs: d#(s(x)) -> d#(x) TRS: d(0()) -> 0() d(s(x)) -> s(s(d(x))) e(0()) -> s(0()) e(r(x)) -> d(e(x)) LPO Processor: argument filtering: pi(0) = [] pi(d) = [0] pi(s) = [0] pi(e) = [0] pi(r) = [0] pi(d#) = 0 precedence: e > d > d# ~ r ~ s ~ 0 problem: DPs: TRS: d(0()) -> 0() d(s(x)) -> s(s(d(x))) e(0()) -> s(0()) e(r(x)) -> d(e(x)) Qed