YES Problem: -(-(neg(x),neg(x)),-(neg(y),neg(y))) -> -(-(x,y),-(x,y)) Proof: DP Processor: DPs: -#(-(neg(x),neg(x)),-(neg(y),neg(y))) -> -#(x,y) -#(-(neg(x),neg(x)),-(neg(y),neg(y))) -> -#(-(x,y),-(x,y)) TRS: -(-(neg(x),neg(x)),-(neg(y),neg(y))) -> -(-(x,y),-(x,y)) Arctic Interpretation Processor: dimension: 1 usable rules: -(-(neg(x),neg(x)),-(neg(y),neg(y))) -> -(-(x,y),-(x,y)) interpretation: [-#](x0, x1) = x0 + x1, [-](x0, x1) = x1 + -8, [neg](x0) = 4x0 + 0 orientation: -#(-(neg(x),neg(x)),-(neg(y),neg(y))) = 4x + 4y + 0 >= x + y = -#(x,y) -#(-(neg(x),neg(x)),-(neg(y),neg(y))) = 4x + 4y + 0 >= y + -8 = -#(-(x,y),-(x,y)) -(-(neg(x),neg(x)),-(neg(y),neg(y))) = 4y + 0 >= y + -8 = -(-(x,y),-(x,y)) problem: DPs: TRS: -(-(neg(x),neg(x)),-(neg(y),neg(y))) -> -(-(x,y),-(x,y)) Qed