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