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
  Usable Rule Processor:
   DPs:
    minux#(+(x,y)) -> minus#(x)
    minux#(+(x,y)) -> minus#(y)
    minux#(+(x,y)) -> +#(minus(y),minus(x))
   TRS:
    minus(minus(x)) -> x
   Arctic Interpretation Processor:
    dimension: 1
    usable rules:
     minus(minus(x)) -> x
    interpretation:
     [+#](x0, x1) = -8x0 + 4x1 + -16,
     
     [minux#](x0) = x0 + 8,
     
     [minus#](x0) = 0,
     
     [+](x0, x1) = 7x0 + x1,
     
     [minus](x0) = 2x0 + 0
    orientation:
     minux#(+(x,y)) = 7x + y + 8 >= 0 = minus#(x)
     
     minux#(+(x,y)) = 7x + y + 8 >= 0 = minus#(y)
     
     minux#(+(x,y)) = 7x + y + 8 >= 6x + -6y + 4 = +#(minus(y),minus(x))
     
     minus(minus(x)) = 4x + 2 >= x = x
    problem:
     DPs:
      
     TRS:
      minus(minus(x)) -> x
    Qed