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