YES
TRS:
 {    +(0(), y) -> y,
   +(s(x), 0()) -> s(x),
  +(s(x), s(y)) -> s(+(s(x), +(y, 0())))}
 DP:
  Strict:
   {+#(s(x), s(y)) -> +#(y, 0()),
    +#(s(x), s(y)) -> +#(s(x), +(y, 0()))}
  Weak:
  {    +(0(), y) -> y,
    +(s(x), 0()) -> s(x),
   +(s(x), s(y)) -> s(+(s(x), +(y, 0())))}
  EDG:
   {(+#(s(x), s(y)) -> +#(s(x), +(y, 0())), +#(s(x), s(y)) -> +#(y, 0()))
    (+#(s(x), s(y)) -> +#(s(x), +(y, 0())), +#(s(x), s(y)) -> +#(s(x), +(y, 0())))}
   SCCS:
    Scc:
     {+#(s(x), s(y)) -> +#(s(x), +(y, 0()))}
    SCC:
     Strict:
      {+#(s(x), s(y)) -> +#(s(x), +(y, 0()))}
     Weak:
     {    +(0(), y) -> y,
       +(s(x), 0()) -> s(x),
      +(s(x), s(y)) -> s(+(s(x), +(y, 0())))}
     POLY:
      Argument Filtering:
       pi(s) = [0], pi(0) = [], pi(+#) = 1, pi(+) = [0,1]
      Usable Rules:
       {}
      Interpretation:
       [+](x0, x1) = x0 + x1,
       [s](x0) = x0 + 1,
       [0] = 0
      Strict:
       {}
      Weak:
       {    +(0(), y) -> y,
         +(s(x), 0()) -> s(x),
        +(s(x), s(y)) -> s(+(s(x), +(y, 0())))}
      Qed