YES
Time: 0.003259
TRS:
 {    p s x -> x,
      s p x -> x,
  +(p x, y) -> p +(x, y),
  +(s x, y) -> s +(x, y),
  +(0(), y) -> y,
  minus p x -> s minus x,
  minus s x -> p minus x,
  minus 0() -> 0(),
  *(p x, y) -> +(*(x, y), minus y),
  *(s x, y) -> +(*(x, y), y),
  *(0(), y) -> 0()}
 DP:
  DP:
   {+#(p x, y) -> p# +(x, y),
    +#(p x, y) -> +#(x, y),
    +#(s x, y) -> s# +(x, y),
    +#(s x, y) -> +#(x, y),
    minus# p x -> s# minus x,
    minus# p x -> minus# x,
    minus# s x -> p# minus x,
    minus# s x -> minus# x,
    *#(p x, y) -> +#(*(x, y), minus y),
    *#(p x, y) -> minus# y,
    *#(p x, y) -> *#(x, y),
    *#(s x, y) -> +#(*(x, y), y),
    *#(s x, y) -> *#(x, y)}
  TRS:
  {    p s x -> x,
       s p x -> x,
   +(p x, y) -> p +(x, y),
   +(s x, y) -> s +(x, y),
   +(0(), y) -> y,
   minus p x -> s minus x,
   minus s x -> p minus x,
   minus 0() -> 0(),
   *(p x, y) -> +(*(x, y), minus y),
   *(s x, y) -> +(*(x, y), y),
   *(0(), y) -> 0()}
  EDG:
   {(+#(s x, y) -> +#(x, y), +#(s x, y) -> +#(x, y))
    (+#(s x, y) -> +#(x, y), +#(s x, y) -> s# +(x, y))
    (+#(s x, y) -> +#(x, y), +#(p x, y) -> +#(x, y))
    (+#(s x, y) -> +#(x, y), +#(p x, y) -> p# +(x, y))
    (*#(s x, y) -> *#(x, y), *#(s x, y) -> *#(x, y))
    (*#(s x, y) -> *#(x, y), *#(s x, y) -> +#(*(x, y), 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))
    (minus# p x -> minus# x, minus# s x -> minus# x)
    (minus# p x -> minus# x, minus# s x -> p# minus x)
    (minus# p x -> minus# x, minus# p x -> minus# x)
    (minus# p x -> minus# x, minus# p x -> s# minus x)
    (*#(p x, y) -> minus# y, minus# s x -> minus# x)
    (*#(p x, y) -> minus# y, minus# s x -> p# minus x)
    (*#(p x, y) -> minus# y, minus# p x -> minus# x)
    (*#(p x, y) -> minus# y, minus# p x -> s# minus x)
    (*#(p x, y) -> +#(*(x, y), minus y), +#(p x, y) -> p# +(x, y))
    (*#(p x, y) -> +#(*(x, y), minus y), +#(p x, y) -> +#(x, y))
    (*#(p x, y) -> +#(*(x, y), minus y), +#(s x, y) -> s# +(x, y))
    (*#(p x, y) -> +#(*(x, y), minus y), +#(s x, y) -> +#(x, y))
    (minus# s x -> minus# x, minus# p x -> s# minus x)
    (minus# s x -> minus# x, minus# p x -> minus# x)
    (minus# s x -> minus# x, minus# s x -> p# minus x)
    (minus# s x -> minus# x, minus# s x -> minus# x)
    (*#(s x, y) -> +#(*(x, y), y), +#(p x, y) -> p# +(x, y))
    (*#(s x, y) -> +#(*(x, y), y), +#(p x, y) -> +#(x, y))
    (*#(s x, y) -> +#(*(x, y), y), +#(s x, y) -> s# +(x, y))
    (*#(s x, y) -> +#(*(x, y), y), +#(s x, y) -> +#(x, y))
    (*#(p x, y) -> *#(x, y), *#(p x, y) -> +#(*(x, y), minus y))
    (*#(p x, y) -> *#(x, y), *#(p x, y) -> minus# y)
    (*#(p x, y) -> *#(x, y), *#(p x, y) -> *#(x, y))
    (*#(p x, y) -> *#(x, y), *#(s x, y) -> +#(*(x, y), y))
    (*#(p x, y) -> *#(x, y), *#(s x, y) -> *#(x, y))
    (+#(p x, y) -> +#(x, y), +#(p x, y) -> p# +(x, y))
    (+#(p x, y) -> +#(x, y), +#(p x, y) -> +#(x, y))
    (+#(p x, y) -> +#(x, y), +#(s x, y) -> s# +(x, y))
    (+#(p x, y) -> +#(x, y), +#(s x, y) -> +#(x, y))}
   SCCS (3):
    Scc:
     {*#(p x, y) -> *#(x, y),
      *#(s x, y) -> *#(x, y)}
    Scc:
     {minus# p x -> minus# x,
      minus# s x -> minus# x}
    Scc:
     {+#(p x, y) -> +#(x, y),
      +#(s x, y) -> +#(x, y)}
    SCC (2):
     Strict:
      {*#(p x, y) -> *#(x, y),
       *#(s x, y) -> *#(x, y)}
     Weak:
     {    p s x -> x,
          s p x -> x,
      +(p x, y) -> p +(x, y),
      +(s x, y) -> s +(x, y),
      +(0(), y) -> y,
      minus p x -> s minus x,
      minus s x -> p minus x,
      minus 0() -> 0(),
      *(p x, y) -> +(*(x, y), minus y),
      *(s x, y) -> +(*(x, y), y),
      *(0(), y) -> 0()}
     SPSC:
      Simple Projection:
       pi(*#) = 0
      Strict:
       {*#(s x, y) -> *#(x, y)}
      EDG:
       {(*#(s x, y) -> *#(x, y), *#(s x, y) -> *#(x, y))}
       SCCS (1):
        Scc:
         {*#(s x, y) -> *#(x, y)}
        SCC (1):
         Strict:
          {*#(s x, y) -> *#(x, y)}
         Weak:
         {    p s x -> x,
              s p x -> x,
          +(p x, y) -> p +(x, y),
          +(s x, y) -> s +(x, y),
          +(0(), y) -> y,
          minus p x -> s minus x,
          minus s x -> p minus x,
          minus 0() -> 0(),
          *(p x, y) -> +(*(x, y), minus y),
          *(s x, y) -> +(*(x, y), y),
          *(0(), y) -> 0()}
         SPSC:
          Simple Projection:
           pi(*#) = 0
          Strict:
           {}
          Qed
    SCC (2):
     Strict:
      {minus# p x -> minus# x,
       minus# s x -> minus# x}
     Weak:
     {    p s x -> x,
          s p x -> x,
      +(p x, y) -> p +(x, y),
      +(s x, y) -> s +(x, y),
      +(0(), y) -> y,
      minus p x -> s minus x,
      minus s x -> p minus x,
      minus 0() -> 0(),
      *(p x, y) -> +(*(x, y), minus y),
      *(s x, y) -> +(*(x, y), y),
      *(0(), y) -> 0()}
     SPSC:
      Simple Projection:
       pi(minus#) = 0
      Strict:
       {minus# s x -> minus# x}
      EDG:
       {(minus# s x -> minus# x, minus# s x -> minus# x)}
       SCCS (1):
        Scc:
         {minus# s x -> minus# x}
        SCC (1):
         Strict:
          {minus# s x -> minus# x}
         Weak:
         {    p s x -> x,
              s p x -> x,
          +(p x, y) -> p +(x, y),
          +(s x, y) -> s +(x, y),
          +(0(), y) -> y,
          minus p x -> s minus x,
          minus s x -> p minus x,
          minus 0() -> 0(),
          *(p x, y) -> +(*(x, y), minus y),
          *(s x, y) -> +(*(x, y), y),
          *(0(), y) -> 0()}
         SPSC:
          Simple Projection:
           pi(minus#) = 0
          Strict:
           {}
          Qed
    SCC (2):
     Strict:
      {+#(p x, y) -> +#(x, y),
       +#(s x, y) -> +#(x, y)}
     Weak:
     {    p s x -> x,
          s p x -> x,
      +(p x, y) -> p +(x, y),
      +(s x, y) -> s +(x, y),
      +(0(), y) -> y,
      minus p x -> s minus x,
      minus s x -> p minus x,
      minus 0() -> 0(),
      *(p x, y) -> +(*(x, y), minus y),
      *(s x, y) -> +(*(x, y), y),
      *(0(), y) -> 0()}
     SPSC:
      Simple Projection:
       pi(+#) = 0
      Strict:
       {+#(s x, y) -> +#(x, y)}
      EDG:
       {(+#(s x, y) -> +#(x, y), +#(s x, y) -> +#(x, y))}
       SCCS (1):
        Scc:
         {+#(s x, y) -> +#(x, y)}
        SCC (1):
         Strict:
          {+#(s x, y) -> +#(x, y)}
         Weak:
         {    p s x -> x,
              s p x -> x,
          +(p x, y) -> p +(x, y),
          +(s x, y) -> s +(x, y),
          +(0(), y) -> y,
          minus p x -> s minus x,
          minus s x -> p minus x,
          minus 0() -> 0(),
          *(p x, y) -> +(*(x, y), minus y),
          *(s x, y) -> +(*(x, y), y),
          *(0(), y) -> 0()}
         SPSC:
          Simple Projection:
           pi(+#) = 0
          Strict:
           {}
          Qed