YES
TRS:
 {          i(0()) -> 0(),
           i(i(x)) -> x,
        i(+(x, y)) -> +(i(x), i(y)),
         +(x, 0()) -> x,
        +(x, i(x)) -> 0(),
     +(x, +(y, z)) -> +(+(x, y), z),
         +(0(), y) -> y,
        +(i(x), x) -> 0(),
  +(+(x, y), i(y)) -> x,
  +(+(x, i(y)), y) -> x}
 DP:
  Strict:
   {   i#(+(x, y)) -> i#(y),
       i#(+(x, y)) -> i#(x),
       i#(+(x, y)) -> +#(i(x), i(y)),
    +#(x, +(y, z)) -> +#(x, y),
    +#(x, +(y, z)) -> +#(+(x, y), z)}
  Weak:
  {          i(0()) -> 0(),
            i(i(x)) -> x,
         i(+(x, y)) -> +(i(x), i(y)),
          +(x, 0()) -> x,
         +(x, i(x)) -> 0(),
      +(x, +(y, z)) -> +(+(x, y), z),
          +(0(), y) -> y,
         +(i(x), x) -> 0(),
   +(+(x, y), i(y)) -> x,
   +(+(x, i(y)), y) -> x}
  EDG:
   {(i#(+(x, y)) -> i#(x), i#(+(x, y)) -> +#(i(x), i(y)))
    (i#(+(x, y)) -> i#(x), i#(+(x, y)) -> i#(x))
    (i#(+(x, y)) -> i#(x), i#(+(x, y)) -> i#(y))
    (+#(x, +(y, z)) -> +#(x, y), +#(x, +(y, z)) -> +#(+(x, y), z))
    (+#(x, +(y, z)) -> +#(x, y), +#(x, +(y, z)) -> +#(x, y))
    (i#(+(x, y)) -> +#(i(x), i(y)), +#(x, +(y, z)) -> +#(x, y))
    (i#(+(x, y)) -> +#(i(x), i(y)), +#(x, +(y, z)) -> +#(+(x, y), z))
    (+#(x, +(y, z)) -> +#(+(x, y), z), +#(x, +(y, z)) -> +#(x, y))
    (+#(x, +(y, z)) -> +#(+(x, y), z), +#(x, +(y, z)) -> +#(+(x, y), z))
    (i#(+(x, y)) -> i#(y), i#(+(x, y)) -> i#(y))
    (i#(+(x, y)) -> i#(y), i#(+(x, y)) -> i#(x))
    (i#(+(x, y)) -> i#(y), i#(+(x, y)) -> +#(i(x), i(y)))}
   SCCS:
    Scc:
     {+#(x, +(y, z)) -> +#(x, y),
      +#(x, +(y, z)) -> +#(+(x, y), z)}
    Scc:
     {i#(+(x, y)) -> i#(y),
      i#(+(x, y)) -> i#(x)}
    SCC:
     Strict:
      {+#(x, +(y, z)) -> +#(x, y),
       +#(x, +(y, z)) -> +#(+(x, y), z)}
     Weak:
     {          i(0()) -> 0(),
               i(i(x)) -> x,
            i(+(x, y)) -> +(i(x), i(y)),
             +(x, 0()) -> x,
            +(x, i(x)) -> 0(),
         +(x, +(y, z)) -> +(+(x, y), z),
             +(0(), y) -> y,
            +(i(x), x) -> 0(),
      +(+(x, y), i(y)) -> x,
      +(+(x, i(y)), y) -> x}
     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:
         {          i(0()) -> 0(),
                   i(i(x)) -> x,
                i(+(x, y)) -> +(i(x), i(y)),
                 +(x, 0()) -> x,
                +(x, i(x)) -> 0(),
             +(x, +(y, z)) -> +(+(x, y), z),
                 +(0(), y) -> y,
                +(i(x), x) -> 0(),
          +(+(x, y), i(y)) -> x,
          +(+(x, i(y)), y) -> x}
         SPSC:
          Simple Projection:
           pi(+#) = 1
          Strict:
           {}
          Qed
    SCC:
     Strict:
      {i#(+(x, y)) -> i#(y),
       i#(+(x, y)) -> i#(x)}
     Weak:
     {          i(0()) -> 0(),
               i(i(x)) -> x,
            i(+(x, y)) -> +(i(x), i(y)),
             +(x, 0()) -> x,
            +(x, i(x)) -> 0(),
         +(x, +(y, z)) -> +(+(x, y), z),
             +(0(), y) -> y,
            +(i(x), x) -> 0(),
      +(+(x, y), i(y)) -> x,
      +(+(x, i(y)), y) -> x}
     SPSC:
      Simple Projection:
       pi(i#) = 0
      Strict:
       {i#(+(x, y)) -> i#(x)}
      EDG:
       {(i#(+(x, y)) -> i#(x), i#(+(x, y)) -> i#(x))}
       SCCS:
        Scc:
         {i#(+(x, y)) -> i#(x)}
        SCC:
         Strict:
          {i#(+(x, y)) -> i#(x)}
         Weak:
         {          i(0()) -> 0(),
                   i(i(x)) -> x,
                i(+(x, y)) -> +(i(x), i(y)),
                 +(x, 0()) -> x,
                +(x, i(x)) -> 0(),
             +(x, +(y, z)) -> +(+(x, y), z),
                 +(0(), y) -> y,
                +(i(x), x) -> 0(),
          +(+(x, y), i(y)) -> x,
          +(+(x, i(y)), y) -> x}
         SPSC:
          Simple Projection:
           pi(i#) = 0
          Strict:
           {}
          Qed