YES

Problem:
 minus(minus(x)) -> x
 minus(h(x)) -> h(minus(x))
 minus(f(x,y)) -> f(minus(y),minus(x))

Proof:
 DP Processor:
  DPs:
   minus#(h(x)) -> minus#(x)
   minus#(f(x,y)) -> minus#(x)
   minus#(f(x,y)) -> minus#(y)
  TRS:
   minus(minus(x)) -> x
   minus(h(x)) -> h(minus(x))
   minus(f(x,y)) -> f(minus(y),minus(x))
  Usable Rule Processor:
   DPs:
    minus#(h(x)) -> minus#(x)
    minus#(f(x,y)) -> minus#(x)
    minus#(f(x,y)) -> minus#(y)
   TRS:
    
   Arctic Interpretation Processor:
    dimension: 1
    usable rules:
     
    interpretation:
     [minus#](x0) = x0,
     
     [f](x0, x1) = 1x0 + 3x1 + -1,
     
     [h](x0) = 1x0
    orientation:
     minus#(h(x)) = 1x >= x = minus#(x)
     
     minus#(f(x,y)) = 1x + 3y + -1 >= x = minus#(x)
     
     minus#(f(x,y)) = 1x + 3y + -1 >= y = minus#(y)
    problem:
     DPs:
      
     TRS:
      
    Qed