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