YES
TRS:
 {*(x, *(minus(y), y)) -> *(minus(*(y, y)), x)}
 DP:
  Strict:
   {*#(x, *(minus(y), y)) -> *#(y, y),
    *#(x, *(minus(y), y)) -> *#(minus(*(y, y)), x)}
  Weak:
  {*(x, *(minus(y), y)) -> *(minus(*(y, y)), x)}
  EDG:
   {(*#(x, *(minus(y), y)) -> *#(minus(*(y, y)), x), *#(x, *(minus(y), y)) -> *#(minus(*(y, y)), x))
    (*#(x, *(minus(y), y)) -> *#(minus(*(y, y)), x), *#(x, *(minus(y), y)) -> *#(y, y))
    (*#(x, *(minus(y), y)) -> *#(y, y), *#(x, *(minus(y), y)) -> *#(y, y))
    (*#(x, *(minus(y), y)) -> *#(y, y), *#(x, *(minus(y), y)) -> *#(minus(*(y, y)), x))}
   SCCS:
    Scc:
     {*#(x, *(minus(y), y)) -> *#(y, y),
      *#(x, *(minus(y), y)) -> *#(minus(*(y, y)), x)}
    SCC:
     Strict:
      {*#(x, *(minus(y), y)) -> *#(y, y),
       *#(x, *(minus(y), y)) -> *#(minus(*(y, y)), x)}
     Weak:
     {*(x, *(minus(y), y)) -> *(minus(*(y, y)), x)}
     POLY:
      Argument Filtering:
       pi(minus) = [0], pi(*#) = [0,1], pi(*) = [0,1]
      Usable Rules:
       {}
      Interpretation:
       [*#](x0, x1) = x0 + x1 + 1,
       [*](x0, x1) = x0 + x1,
       [minus](x0) = x0 + 1
      Strict:
       {*#(x, *(minus(y), y)) -> *#(minus(*(y, y)), x)}
      Weak:
       {*(x, *(minus(y), y)) -> *(minus(*(y, y)), x)}
      EDG:
       {(*#(x, *(minus(y), y)) -> *#(minus(*(y, y)), x), *#(x, *(minus(y), y)) -> *#(minus(*(y, y)), x))}
       SCCS:
        Scc:
         {*#(x, *(minus(y), y)) -> *#(minus(*(y, y)), x)}
        SCC:
         Strict:
          {*#(x, *(minus(y), y)) -> *#(minus(*(y, y)), x)}
         Weak:
         {*(x, *(minus(y), y)) -> *(minus(*(y, y)), x)}
         POLY:
          Argument Filtering:
           pi(minus) = [], pi(*#) = [0,1], pi(*) = [1]
          Usable Rules:
           {}
          Interpretation:
           [*#](x0, x1) = x0 + x1,
           [*](x0) = x0 + 1,
           [minus] = 0
          Strict:
           {}
          Weak:
           {*(x, *(minus(y), y)) -> *(minus(*(y, y)), x)}
          Qed