YES

Problem:
 minus(minus(x)) -> x
 minux(+(x,y)) -> +(minus(y),minus(x))
 +(minus(x),+(x,y)) -> y
 +(+(x,y),minus(y)) -> x

Proof:
 DP Processor:
  DPs:
   minux#(+(x,y)) -> minus#(x)
   minux#(+(x,y)) -> minus#(y)
   minux#(+(x,y)) -> +#(minus(y),minus(x))
  TRS:
   minus(minus(x)) -> x
   minux(+(x,y)) -> +(minus(y),minus(x))
   +(minus(x),+(x,y)) -> y
   +(+(x,y),minus(y)) -> x
  Arctic Interpretation Processor:
   dimension: 1
   interpretation:
    [+#](x0, x1) = 0,
    
    [minux#](x0) = x0 + 0,
    
    [minus#](x0) = 1,
    
    [minux](x0) = 2x0 + 0,
    
    [+](x0, x1) = 1x0 + 1x1 + 2,
    
    [minus](x0) = 1x0
   orientation:
    minux#(+(x,y)) = 1x + 1y + 2 >= 1 = minus#(x)
    
    minux#(+(x,y)) = 1x + 1y + 2 >= 1 = minus#(y)
    
    minux#(+(x,y)) = 1x + 1y + 2 >= 0 = +#(minus(y),minus(x))
    
    minus(minus(x)) = 2x >= x = x
    
    minux(+(x,y)) = 3x + 3y + 4 >= 2x + 2y + 2 = +(minus(y),minus(x))
    
    +(minus(x),+(x,y)) = 2x + 2y + 3 >= y = y
    
    +(+(x,y),minus(y)) = 2x + 2y + 3 >= x = x
   problem:
    DPs:
     
    TRS:
     minus(minus(x)) -> x
     minux(+(x,y)) -> +(minus(y),minus(x))
     +(minus(x),+(x,y)) -> y
     +(+(x,y),minus(y)) -> x
   Qed