YES
TRS:
 {        *(*(x, y), z) -> *(x, *(y, z)),
  +(*(x, y), *(a(), y)) -> *(+(x, a()), y)}
 DP:
  Strict:
   {        *#(*(x, y), z) -> *#(x, *(y, z)),
            *#(*(x, y), z) -> *#(y, z),
    +#(*(x, y), *(a(), y)) -> *#(+(x, a()), y),
    +#(*(x, y), *(a(), y)) -> +#(x, a())}
  Weak:
  {        *(*(x, y), z) -> *(x, *(y, z)),
   +(*(x, y), *(a(), y)) -> *(+(x, a()), y)}
  EDG:
   {(*#(*(x, y), z) -> *#(y, z), *#(*(x, y), z) -> *#(y, z))
    (*#(*(x, y), z) -> *#(y, z), *#(*(x, y), z) -> *#(x, *(y, z)))
    (*#(*(x, y), z) -> *#(x, *(y, z)), *#(*(x, y), z) -> *#(x, *(y, z)))
    (*#(*(x, y), z) -> *#(x, *(y, z)), *#(*(x, y), z) -> *#(y, z))}
   SCCS:
    Scc:
     {*#(*(x, y), z) -> *#(x, *(y, z)),
      *#(*(x, y), z) -> *#(y, z)}
    SCC:
     Strict:
      {*#(*(x, y), z) -> *#(x, *(y, z)),
       *#(*(x, y), z) -> *#(y, z)}
     Weak:
     {        *(*(x, y), z) -> *(x, *(y, z)),
      +(*(x, y), *(a(), y)) -> *(+(x, a()), y)}
     SPSC:
      Simple Projection:
       pi(*#) = 0
      Strict:
       {*#(*(x, y), z) -> *#(y, z)}
      EDG:
       {(*#(*(x, y), z) -> *#(y, z), *#(*(x, y), z) -> *#(y, z))}
       SCCS:
        Scc:
         {*#(*(x, y), z) -> *#(y, z)}
        SCC:
         Strict:
          {*#(*(x, y), z) -> *#(y, z)}
         Weak:
         {        *(*(x, y), z) -> *(x, *(y, z)),
          +(*(x, y), *(a(), y)) -> *(+(x, a()), y)}
         SPSC:
          Simple Projection:
           pi(*#) = 0
          Strict:
           {}
          Qed