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