YES Problem: -(x,0()) -> x -(s(x),s(y)) -> -(x,y) p(s(x)) -> x f(s(x),y) -> f(p(-(s(x),y)),p(-(y,s(x)))) f(x,s(y)) -> f(p(-(x,s(y))),p(-(s(y),x))) Proof: DP Processor: DPs: -#(s(x),s(y)) -> -#(x,y) f#(s(x),y) -> -#(y,s(x)) f#(s(x),y) -> p#(-(y,s(x))) f#(s(x),y) -> -#(s(x),y) f#(s(x),y) -> p#(-(s(x),y)) f#(s(x),y) -> f#(p(-(s(x),y)),p(-(y,s(x)))) f#(x,s(y)) -> -#(s(y),x) f#(x,s(y)) -> p#(-(s(y),x)) f#(x,s(y)) -> -#(x,s(y)) f#(x,s(y)) -> p#(-(x,s(y))) f#(x,s(y)) -> f#(p(-(x,s(y))),p(-(s(y),x))) TRS: -(x,0()) -> x -(s(x),s(y)) -> -(x,y) p(s(x)) -> x f(s(x),y) -> f(p(-(s(x),y)),p(-(y,s(x)))) f(x,s(y)) -> f(p(-(x,s(y))),p(-(s(y),x))) Usable Rule Processor: DPs: -#(s(x),s(y)) -> -#(x,y) f#(s(x),y) -> -#(y,s(x)) f#(s(x),y) -> p#(-(y,s(x))) f#(s(x),y) -> -#(s(x),y) f#(s(x),y) -> p#(-(s(x),y)) f#(s(x),y) -> f#(p(-(s(x),y)),p(-(y,s(x)))) f#(x,s(y)) -> -#(s(y),x) f#(x,s(y)) -> p#(-(s(y),x)) f#(x,s(y)) -> -#(x,s(y)) f#(x,s(y)) -> p#(-(x,s(y))) f#(x,s(y)) -> f#(p(-(x,s(y))),p(-(s(y),x))) TRS: -(s(x),s(y)) -> -(x,y) -(x,0()) -> x p(s(x)) -> x Arctic Interpretation Processor: dimension: 1 usable rules: -(s(x),s(y)) -> -(x,y) -(x,0()) -> x p(s(x)) -> x interpretation: [f#](x0, x1) = x0 + x1 + 0, [p#](x0) = -4x0 + 0, [-#](x0, x1) = -2x1 + 0, [p](x0) = -5x0 + 4, [s](x0) = 6x0 + 6, [-](x0, x1) = 1x0 + 1x1 + 0, [0] = 0 orientation: -#(s(x),s(y)) = 4y + 4 >= -2y + 0 = -#(x,y) f#(s(x),y) = 6x + y + 6 >= 4x + 4 = -#(y,s(x)) f#(s(x),y) = 6x + y + 6 >= 3x + -3y + 3 = p#(-(y,s(x))) f#(s(x),y) = 6x + y + 6 >= -2y + 0 = -#(s(x),y) f#(s(x),y) = 6x + y + 6 >= 3x + -3y + 3 = p#(-(s(x),y)) f#(s(x),y) = 6x + y + 6 >= 2x + -4y + 4 = f#(p(-(s(x),y)),p(-(y,s(x)))) f#(x,s(y)) = x + 6y + 6 >= -2x + 0 = -#(s(y),x) f#(x,s(y)) = x + 6y + 6 >= -3x + 3y + 3 = p#(-(s(y),x)) f#(x,s(y)) = x + 6y + 6 >= 4y + 4 = -#(x,s(y)) f#(x,s(y)) = x + 6y + 6 >= -3x + 3y + 3 = p#(-(x,s(y))) f#(x,s(y)) = x + 6y + 6 >= -4x + 2y + 4 = f#(p(-(x,s(y))),p(-(s(y),x))) -(s(x),s(y)) = 7x + 7y + 7 >= 1x + 1y + 0 = -(x,y) -(x,0()) = 1x + 1 >= x = x p(s(x)) = 1x + 4 >= x = x problem: DPs: TRS: -(s(x),s(y)) -> -(x,y) -(x,0()) -> x p(s(x)) -> x Qed