YES
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:
   Strict:
    {+#(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)}
   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}
   EDG:
    {(+#(x, +(y, z)) -> +#(x, y), +#(x, +(y, z)) -> +#(+(x, y), z))
     (+#(x, +(y, z)) -> +#(x, y), +#(x, +(y, z)) -> +#(x, y))
     (+#(x, +(y, z)) -> +#(x, y), +#(x, minus(y)) -> +#(minus(x), y))
     (+#(x, +(y, z)) -> +#(x, y), +#(x, minus(y)) -> minus#(+(minus(x), y)))
     (+#(x, +(y, z)) -> +#(x, y), +#(x, minus(y)) -> minus#(x))
     (+#(x, minus(y)) -> +#(minus(x), y), +#(x, +(y, z)) -> +#(+(x, y), z))
     (+#(x, minus(y)) -> +#(minus(x), y), +#(x, +(y, z)) -> +#(x, y))
     (+#(x, minus(y)) -> +#(minus(x), y), +#(x, minus(y)) -> +#(minus(x), y))
     (+#(x, minus(y)) -> +#(minus(x), y), +#(x, minus(y)) -> minus#(+(minus(x), y)))
     (+#(x, minus(y)) -> +#(minus(x), y), +#(x, minus(y)) -> minus#(x))
     (+#(x, +(y, z)) -> +#(+(x, y), z), +#(x, minus(y)) -> minus#(x))
     (+#(x, +(y, z)) -> +#(+(x, y), z), +#(x, minus(y)) -> minus#(+(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))
     (+#(x, +(y, z)) -> +#(+(x, y), z), +#(x, +(y, z)) -> +#(+(x, y), z))}
    SCCS:
     Scc:
      {+#(x, minus(y)) -> +#(minus(x), y),
        +#(x, +(y, z)) -> +#(x, y),
        +#(x, +(y, z)) -> +#(+(x, y), z)}
     SCC:
      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, +(y, z)) -> +#(+(x, y), z), +#(x, +(y, z)) -> +#(+(x, y), z))
         (+#(x, +(y, z)) -> +#(+(x, y), z), +#(x, minus(y)) -> +#(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), z))}
        SCCS:
         Scc:
          {+#(x, minus(y)) -> +#(minus(x), y),
            +#(x, +(y, z)) -> +#(+(x, y), z)}
         SCC:
          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:
             Scc:
              {+#(x, +(y, z)) -> +#(+(x, y), z)}
             SCC:
              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