YES
Time: 0.005678
TRS:
 {  +(0(), y) -> y,
  +(s x, 0()) -> s x,
  +(s x, s y) -> s +(s x, +(y, 0()))}
 DP:
  DP:
   {+#(s x, s y) -> +#(y, 0()),
    +#(s x, s y) -> +#(s x, +(y, 0()))}
  TRS:
  {  +(0(), y) -> y,
   +(s x, 0()) -> s x,
   +(s x, s y) -> s +(s x, +(y, 0()))}
  UR:
   {  +(0(), y) -> y,
    +(s x, 0()) -> s x}
   EDG:
    {(+#(s x, s y) -> +#(y, 0()), +#(s x, s y) -> +#(s x, +(y, 0())))
     (+#(s x, s y) -> +#(y, 0()), +#(s x, s y) -> +#(y, 0()))
     (+#(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())))}
    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())))}
     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())))}
      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())))}
       STATUS:
        arrows: 0.500000
        SCCS (1):
         Scc:
          {+#(s x, s y) -> +#(s x, +(y, 0()))}
         
         SCC (1):
          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:
           Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
           Interpretation:
            [+](x0, x1) = x0 + x1,
            
            [s](x0) = x0 + 1,
            
            [0] = 0,
            
            [+#](x0, x1) = x0 + x1 + 1
           Strict:
            +#(s x, s y) -> +#(s x, +(y, 0()))
            3 + 1y + 1x >= 2 + 1y + 1x
           Weak:
            +(s x, s y) -> s +(s x, +(y, 0()))
            2 + 1y + 1x >= 2 + 1y + 1x
            +(s x, 0()) -> s x
            1 + 1x >= 1 + 1x
            +(0(), y) -> y
            0 + 1y >= 1y
          Qed