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
  TDG 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
   graph:
    
   Qed