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