YES
TRS:
 {      +(+(x, y), z) -> +(x, +(y, z)),
  +(f(x), +(f(y), z)) -> +(f(+(x, y)), z),
        +(f(x), f(y)) -> f(+(x, y))}
 DP:
  Strict:
   {      +#(+(x, y), z) -> +#(x, +(y, z)),
          +#(+(x, y), z) -> +#(y, z),
    +#(f(x), +(f(y), z)) -> +#(x, y),
    +#(f(x), +(f(y), z)) -> +#(f(+(x, y)), z),
          +#(f(x), f(y)) -> +#(x, y)}
  Weak:
  {      +(+(x, y), z) -> +(x, +(y, z)),
   +(f(x), +(f(y), z)) -> +(f(+(x, y)), z),
         +(f(x), f(y)) -> f(+(x, y))}
  EDG:
   {(+#(+(x, y), z) -> +#(x, +(y, z)), +#(f(x), f(y)) -> +#(x, y))
    (+#(+(x, y), z) -> +#(x, +(y, z)), +#(f(x), +(f(y), z)) -> +#(f(+(x, y)), z))
    (+#(+(x, y), z) -> +#(x, +(y, z)), +#(f(x), +(f(y), z)) -> +#(x, y))
    (+#(+(x, y), z) -> +#(x, +(y, z)), +#(+(x, y), z) -> +#(y, z))
    (+#(+(x, y), z) -> +#(x, +(y, z)), +#(+(x, y), z) -> +#(x, +(y, z)))
    (+#(f(x), +(f(y), z)) -> +#(f(+(x, y)), z), +#(f(x), f(y)) -> +#(x, y))
    (+#(f(x), +(f(y), z)) -> +#(f(+(x, y)), z), +#(f(x), +(f(y), z)) -> +#(f(+(x, y)), z))
    (+#(f(x), +(f(y), z)) -> +#(f(+(x, y)), z), +#(f(x), +(f(y), z)) -> +#(x, y))
    (+#(f(x), f(y)) -> +#(x, y), +#(+(x, y), z) -> +#(x, +(y, z)))
    (+#(f(x), f(y)) -> +#(x, y), +#(+(x, y), z) -> +#(y, z))
    (+#(f(x), f(y)) -> +#(x, y), +#(f(x), +(f(y), z)) -> +#(x, y))
    (+#(f(x), f(y)) -> +#(x, y), +#(f(x), +(f(y), z)) -> +#(f(+(x, y)), z))
    (+#(f(x), f(y)) -> +#(x, y), +#(f(x), f(y)) -> +#(x, y))
    (+#(f(x), +(f(y), z)) -> +#(x, y), +#(+(x, y), z) -> +#(x, +(y, z)))
    (+#(f(x), +(f(y), z)) -> +#(x, y), +#(+(x, y), z) -> +#(y, z))
    (+#(f(x), +(f(y), z)) -> +#(x, y), +#(f(x), +(f(y), z)) -> +#(x, y))
    (+#(f(x), +(f(y), z)) -> +#(x, y), +#(f(x), +(f(y), z)) -> +#(f(+(x, y)), z))
    (+#(f(x), +(f(y), z)) -> +#(x, y), +#(f(x), f(y)) -> +#(x, y))
    (+#(+(x, y), z) -> +#(y, z), +#(+(x, y), z) -> +#(x, +(y, z)))
    (+#(+(x, y), z) -> +#(y, z), +#(+(x, y), z) -> +#(y, z))
    (+#(+(x, y), z) -> +#(y, z), +#(f(x), +(f(y), z)) -> +#(x, y))
    (+#(+(x, y), z) -> +#(y, z), +#(f(x), +(f(y), z)) -> +#(f(+(x, y)), z))
    (+#(+(x, y), z) -> +#(y, z), +#(f(x), f(y)) -> +#(x, y))}
   SCCS:
    Scc:
     {      +#(+(x, y), z) -> +#(x, +(y, z)),
            +#(+(x, y), z) -> +#(y, z),
      +#(f(x), +(f(y), z)) -> +#(x, y),
      +#(f(x), +(f(y), z)) -> +#(f(+(x, y)), z),
            +#(f(x), f(y)) -> +#(x, y)}
    SCC:
     Strict:
      {      +#(+(x, y), z) -> +#(x, +(y, z)),
             +#(+(x, y), z) -> +#(y, z),
       +#(f(x), +(f(y), z)) -> +#(x, y),
       +#(f(x), +(f(y), z)) -> +#(f(+(x, y)), z),
             +#(f(x), f(y)) -> +#(x, y)}
     Weak:
     {      +(+(x, y), z) -> +(x, +(y, z)),
      +(f(x), +(f(y), z)) -> +(f(+(x, y)), z),
            +(f(x), f(y)) -> f(+(x, y))}
     POLY:
      Argument Filtering:
       pi(f) = [0], pi(+#) = [0,1], pi(+) = [0,1]
      Usable Rules:
       {}
      Interpretation:
       [+#](x0, x1) = x0 + x1,
       [+](x0, x1) = x0 + x1,
       [f](x0) = x0 + 1
      Strict:
       {+#(+(x, y), z) -> +#(x, +(y, z)),
        +#(+(x, y), z) -> +#(y, z)}
      Weak:
       {      +(+(x, y), z) -> +(x, +(y, z)),
        +(f(x), +(f(y), z)) -> +(f(+(x, y)), z),
              +(f(x), f(y)) -> f(+(x, y))}
      EDG:
       {(+#(+(x, y), z) -> +#(y, z), +#(+(x, y), z) -> +#(y, z))
        (+#(+(x, y), z) -> +#(y, z), +#(+(x, y), z) -> +#(x, +(y, z)))
        (+#(+(x, y), z) -> +#(x, +(y, z)), +#(+(x, y), z) -> +#(x, +(y, z)))
        (+#(+(x, y), z) -> +#(x, +(y, z)), +#(+(x, y), z) -> +#(y, z))}
       SCCS:
        Scc:
         {+#(+(x, y), z) -> +#(x, +(y, z)),
          +#(+(x, y), z) -> +#(y, z)}
        SCC:
         Strict:
          {+#(+(x, y), z) -> +#(x, +(y, z)),
           +#(+(x, y), z) -> +#(y, z)}
         Weak:
         {      +(+(x, y), z) -> +(x, +(y, z)),
          +(f(x), +(f(y), z)) -> +(f(+(x, y)), z),
                +(f(x), f(y)) -> f(+(x, y))}
         SPSC:
          Simple Projection:
           pi(+#) = 0
          Strict:
           {+#(+(x, y), z) -> +#(y, z)}
          EDG:
           {(+#(+(x, y), z) -> +#(y, z), +#(+(x, y), z) -> +#(y, z))}
           SCCS:
            Scc:
             {+#(+(x, y), z) -> +#(y, z)}
            SCC:
             Strict:
              {+#(+(x, y), z) -> +#(y, z)}
             Weak:
             {      +(+(x, y), z) -> +(x, +(y, z)),
              +(f(x), +(f(y), z)) -> +(f(+(x, y)), z),
                    +(f(x), f(y)) -> f(+(x, y))}
             SPSC:
              Simple Projection:
               pi(+#) = 0
              Strict:
               {}
              Qed