YES
Time: 0.008583
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)}
  UR:
   {*(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))}
    STATUS:
     arrows: 0.000000
     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:
         *(x, *(minus y, y)) -> *(minus *(y, y), x)
         2 + 2y + 1x >= 2 + 2y + 1x
       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:
           *(x, *(minus y, y)) -> *(minus *(y, y), x)
           1 + 0y + 0x >= 1 + 0y + 0x
         Qed