YES
Time: 0.006741
TRS:
 {        *(*(x, y), z) -> *(x, *(y, z)),
  +(*(x, y), *(a(), y)) -> *(+(x, a()), y)}
 DP:
  DP:
   {        *#(*(x, y), z) -> *#(x, *(y, z)),
            *#(*(x, y), z) -> *#(y, z),
    +#(*(x, y), *(a(), y)) -> *#(+(x, a()), y),
    +#(*(x, y), *(a(), y)) -> +#(x, a())}
  TRS:
  {        *(*(x, y), z) -> *(x, *(y, z)),
   +(*(x, y), *(a(), y)) -> *(+(x, a()), y)}
  UR:
   {*(*(x, y), z) -> *(x, *(y, z))}
   EDG:
    {(*#(*(x, y), z) -> *#(y, z), *#(*(x, y), z) -> *#(x, *(y, z)))
     (*#(*(x, y), z) -> *#(y, z), *#(*(x, y), z) -> *#(y, z))}
    STATUS:
     arrows: 0.875000
     SCCS (1):
      Scc:
       {*#(*(x, y), z) -> *#(y, z)}
      
      
      SCC (1):
       Strict:
        {*#(*(x, y), z) -> *#(y, z)}
       Weak:
       {        *(*(x, y), z) -> *(x, *(y, z)),
        +(*(x, y), *(a(), y)) -> *(+(x, a()), y)}
       POLY:
        Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
        Interpretation:
         [*](x0, x1) = x0 + x1 + 1,
         
         [+](x0, x1) = 0,
         
         [a] = 1,
         
         [*#](x0, x1) = x0
        Strict:
         *#(*(x, y), z) -> *#(y, z)
         1 + 1x + 1y + 0z >= 0 + 1y + 0z
        Weak:
         +(*(x, y), *(a(), y)) -> *(+(x, a()), y)
         0 + 0x + 0y >= 1 + 0x + 1y
         *(*(x, y), z) -> *(x, *(y, z))
         2 + 1x + 1y + 1z >= 2 + 1x + 1y + 1z
       Qed