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