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)
  Matrix Interpretation Processor:
   dimension: 1
   interpretation:
    [*#](x0, x1) = x0 + x1 + 1,
    
    [*](x0, x1) = x0 + x1,
    
    [minus](x0) = x0 + 1
   orientation:
    *#(x,*(minus(y),y)) = x + 2y + 2 >= 2y + 1 = *#(y,y)
    
    *#(x,*(minus(y),y)) = x + 2y + 2 >= x + 2y + 2 = *#(minus(*(y,y)),x)
    
    *(x,*(minus(y),y)) = x + 2y + 1 >= x + 2y + 1 = *(minus(*(y,y)),x)
   problem:
    DPs:
     *#(x,*(minus(y),y)) -> *#(minus(*(y,y)),x)
    TRS:
     *(x,*(minus(y),y)) -> *(minus(*(y,y)),x)
   Matrix Interpretation Processor:
    dimension: 1
    interpretation:
     [*#](x0, x1) = x0 + x1,
     
     [*](x0, x1) = 1,
     
     [minus](x0) = 0
    orientation:
     *#(x,*(minus(y),y)) = x + 1 >= x = *#(minus(*(y,y)),x)
     
     *(x,*(minus(y),y)) = 1 >= 1 = *(minus(*(y,y)),x)
    problem:
     DPs:
      
     TRS:
      *(x,*(minus(y),y)) -> *(minus(*(y,y)),x)
    Qed