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