YES
Time: 0.002661
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:
  DP:
   {    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)}
  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}
  EDG:
   {(+#(x, +(y, z)) -> +#(+(x, y), z), +#(x, +(y, z)) -> +#(+(x, y), z))
    (+#(x, +(y, z)) -> +#(+(x, y), z), +#(x, +(y, z)) -> +#(x, y))
    (i# +(x, y) -> +#(i x, i y), +#(x, +(y, z)) -> +#(+(x, y), z))
    (i# +(x, y) -> +#(i x, i y), +#(x, +(y, z)) -> +#(x, y))
    (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))
    (+#(x, +(y, z)) -> +#(x, y), +#(x, +(y, z)) -> +#(x, y))
    (+#(x, +(y, z)) -> +#(x, y), +#(x, +(y, z)) -> +#(+(x, y), z))
    (i# +(x, y) -> i# x, i# +(x, y) -> i# y)
    (i# +(x, y) -> i# x, i# +(x, y) -> i# x)
    (i# +(x, y) -> i# x, i# +(x, y) -> +#(i x, i y))}
   SCCS (2):
    Scc:
     {+#(x, +(y, z)) -> +#(x, y),
      +#(x, +(y, z)) -> +#(+(x, y), z)}
    Scc:
     {i# +(x, y) -> i# y,
      i# +(x, y) -> i# x}
    SCC (2):
     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 (1):
        Scc:
         {+#(x, +(y, z)) -> +#(+(x, y), z)}
        SCC (1):
         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 (2):
     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 (1):
        Scc:
         {i# +(x, y) -> i# x}
        SCC (1):
         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