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