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