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