YES
Time: 0.002429
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:
  DP:
   {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)}
  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}
  EDG:
   {(*#(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)))
    (minus# +(x, y) -> minus# y, minus# +(x, y) -> minus# y)
    (minus# +(x, y) -> minus# y, minus# +(x, y) -> minus# x)
    (minus# +(x, y) -> minus# y, minus# +(x, y) -> +#(minus y, minus x))
    (*#(x, +(y, z)) -> *#(x, z), *#(x, minus y) -> *#(x, y))
    (*#(x, +(y, z)) -> *#(x, z), *#(x, minus y) -> minus# *(x, y))
    (*#(x, +(y, z)) -> *#(x, z), *#(x, +(y, z)) -> *#(x, z))
    (*#(x, +(y, z)) -> *#(x, z), *#(x, +(y, z)) -> *#(x, y))
    (*#(x, +(y, z)) -> *#(x, z), *#(x, +(y, z)) -> +#(*(x, y), *(x, z)))
    (*#(x, minus y) -> minus# *(x, y), minus# +(x, y) -> +#(minus y, minus x))
    (*#(x, minus y) -> minus# *(x, y), minus# +(x, y) -> minus# x)
    (*#(x, minus y) -> minus# *(x, y), minus# +(x, y) -> minus# y)
    (*#(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)}
   SCCS (2):
    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 (3):
     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, y),
        *#(x, +(y, z)) -> *#(x, z)}
      EDG:
       {(*#(x, +(y, z)) -> *#(x, z), *#(x, +(y, z)) -> *#(x, z))
        (*#(x, +(y, z)) -> *#(x, z), *#(x, +(y, z)) -> *#(x, y))
        (*#(x, +(y, z)) -> *#(x, y), *#(x, +(y, z)) -> *#(x, y))
        (*#(x, +(y, z)) -> *#(x, y), *#(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, 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, 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, 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 (2):
     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 (1):
        Scc:
         {minus# +(x, y) -> minus# y}
        SCC (1):
         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