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