YES
Time: 0.029202
TRS:
 {  +(x, 0()) -> x,
    +(x, s y) -> s +(x, y),
  +(0(), s y) -> s y,
  s +(0(), y) -> s y}
 DP:
  DP:
   {  +#(x, s y) -> +#(x, y),
      +#(x, s y) -> s# +(x, y),
    s# +(0(), y) -> s# y}
  TRS:
  {  +(x, 0()) -> x,
     +(x, s y) -> s +(x, y),
   +(0(), s y) -> s y,
   s +(0(), y) -> s y}
  UR:
   {  +(x, 0()) -> x,
      +(x, s y) -> s +(x, y),
    +(0(), s y) -> s y,
    s +(0(), y) -> s y}
   EDG:
    {(+#(x, s y) -> s# +(x, y), s# +(0(), y) -> s# y)
     (+#(x, s y) -> +#(x, y), +#(x, s y) -> +#(x, y))
     (+#(x, s y) -> +#(x, y), +#(x, s y) -> s# +(x, y))
     (s# +(0(), y) -> s# y, s# +(0(), y) -> s# y)}
    STATUS:
     arrows: 0.555556
     SCCS (2):
      Scc:
       {+#(x, s y) -> +#(x, y)}
      Scc:
       {s# +(0(), y) -> s# y}
      
      SCC (1):
       Strict:
        {+#(x, s y) -> +#(x, y)}
       Weak:
       {  +(x, 0()) -> x,
          +(x, s y) -> s +(x, y),
        +(0(), s y) -> s y,
        s +(0(), y) -> s y}
       POLY:
        Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
        Interpretation:
         [+](x0, x1) = x0 + 1,
         
         [s](x0) = x0 + 1,
         
         [0] = 1,
         
         [+#](x0, x1) = x0
        Strict:
         +#(x, s y) -> +#(x, y)
         1 + 0x + 1y >= 0 + 0x + 1y
        Weak:
         s +(0(), y) -> s y
         2 + 1y >= 1 + 1y
         +(0(), s y) -> s y
         2 + 1y >= 1 + 1y
         +(x, s y) -> s +(x, y)
         2 + 0x + 1y >= 2 + 0x + 1y
         +(x, 0()) -> x
         2 + 0x >= 1x
       Qed
     
     SCC (1):
      Strict:
       {s# +(0(), y) -> s# y}
      Weak:
      {  +(x, 0()) -> x,
         +(x, s y) -> s +(x, y),
       +(0(), s y) -> s y,
       s +(0(), y) -> s y}
      POLY:
       Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
       Interpretation:
        [+](x0, x1) = x0 + x1,
        
        [s](x0) = 0,
        
        [0] = 1,
        
        [s#](x0) = x0
       Strict:
        s# +(0(), y) -> s# y
        1 + 1y >= 0 + 1y
       Weak:
        s +(0(), y) -> s y
        0 + 0y >= 0 + 0y
        +(0(), s y) -> s y
        1 + 0y >= 0 + 0y
        +(x, s y) -> s +(x, y)
        0 + 1x + 0y >= 0 + 0x + 0y
        +(x, 0()) -> x
        1 + 1x >= 1x
      Qed