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)) Matrix Interpretation Processor: dim=1 usable rules: d(0()) -> 0() d(s(x)) -> s(s(d(x))) e(0()) -> s(0()) e(r(x)) -> d(e(x)) interpretation: [e#](x0) = x0 + 6, [d#](x0) = x0, [r](x0) = 4x0 + 4, [e](x0) = 4x0, [s](x0) = x0 + 1, [d](x0) = 2x0 + 1, [0] = 1 orientation: d#(s(x)) = x + 1 >= x = d#(x) e#(r(x)) = 4x + 10 >= x + 6 = e#(x) e#(r(x)) = 4x + 10 >= 4x = d#(e(x)) d(0()) = 3 >= 1 = 0() d(s(x)) = 2x + 3 >= 2x + 3 = s(s(d(x))) e(0()) = 4 >= 2 = s(0()) e(r(x)) = 16x + 16 >= 8x + 1 = 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