YES Problem: f(s(X),Y) -> h(s(f(h(Y),X))) Proof: DP Processor: DPs: f#(s(X),Y) -> f#(h(Y),X) TRS: f(s(X),Y) -> h(s(f(h(Y),X))) Arctic Interpretation Processor: dimension: 1 interpretation: [f#](x0, x1) = 2x0 + 0, [h](x0) = 0, [f](x0, x1) = 2x1 + 6, [s](x0) = x0 + 2 orientation: f#(s(X),Y) = 2X + 4 >= 2 = f#(h(Y),X) f(s(X),Y) = 2Y + 6 >= 0 = h(s(f(h(Y),X))) problem: DPs: TRS: f(s(X),Y) -> h(s(f(h(Y),X))) Qed