YES

Problem:
 *(x,*(minus(y),y)) -> *(minus(*(y,y)),x)

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