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
   usable rules:
    *(x,*(minus(y),y)) -> *(minus(*(y,y)),x)
   interpretation:
    [*#](x0, x1) = 2x0 + 1x1 + 0,
    
    [*](x0, x1) = 4x0 + 2x1,
    
    [minus](x0) = -7x0 + 0
   orientation:
    *#(x,*(minus(y),y)) = 2x + 3y + 5 >= 2y + 0 = *#(y,y)
    
    *#(x,*(minus(y),y)) = 2x + 3y + 5 >= 1x + -1y + 2 = *#(minus(*(y,y)),x)
    
    *(x,*(minus(y),y)) = 4x + 4y + 6 >= 2x + 1y + 4 = *(minus(*(y,y)),x)
   problem:
    DPs:
     
    TRS:
     *(x,*(minus(y),y)) -> *(minus(*(y,y)),x)
   Qed