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