YES
Time: 0.007310
TRS:
 {*(x, *(minus y, y)) -> *(minus *(y, y), x)}
 DP:
  DP:
   {*#(x, *(minus y, y)) -> *#(y, y),
    *#(x, *(minus y, y)) -> *#(minus *(y, y), x)}
  TRS:
  {*(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 (1):
    Scc:
     {*#(x, *(minus y, y)) -> *#(y, y),
      *#(x, *(minus y, y)) -> *#(minus *(y, y), x)}
    SCC (2):
     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:
      Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
      Interpretation:
       [*](x0, x1) = x0 + x1 + 1,
       
       [minus](x0) = x0,
       
       [*#](x0, x1) = x0 + x1
      Strict:
       *#(x, *(minus y, y)) -> *#(minus *(y, y), x)
       1 + 2y + 1x >= 1 + 2y + 1x
       *#(x, *(minus y, y)) -> *#(y, y)
       1 + 2y + 1x >= 0 + 2y
      Weak:
       
     EDG:
      {(*#(x, *(minus y, y)) -> *#(minus *(y, y), x), *#(x, *(minus y, y)) -> *#(minus *(y, y), x))}
      SCCS (1):
       Scc:
        {*#(x, *(minus y, y)) -> *#(minus *(y, y), x)}
       SCC (1):
        Strict:
         {*#(x, *(minus y, y)) -> *#(minus *(y, y), x)}
        Weak:
        {*(x, *(minus y, y)) -> *(minus *(y, y), x)}
        POLY:
         Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
         Interpretation:
          [*](x0, x1) = 1,
          
          [minus](x0) = 0,
          
          [*#](x0, x1) = x0 + x1
         Strict:
          *#(x, *(minus y, y)) -> *#(minus *(y, y), x)
          1 + 0y + 1x >= 0 + 0y + 1x
         Weak:
          
        Qed