MAYBE
MAYBE
TRS:
 {
                              minus(x, 0()) -> x,
                          minus(s(x), s(y)) -> minus(x, y),
                            quot(0(), s(y)) -> 0(),
                           quot(s(x), s(y)) -> s(quot(minus(x, y), s(y))),
  plus(minus(x, s(0())), minus(y, s(s(z)))) ->
  plus(minus(y, s(s(z))), minus(x, s(0()))),
                               plus(0(), y) -> y,
                              plus(s(x), y) -> s(plus(x, y)),
    plus(plus(x, s(0())), plus(y, s(s(z)))) ->
  plus(plus(y, s(s(z))), plus(x, s(0())))
 }
 DUP: We consider a duplicating system.
  Trs:
   {
                                minus(x, 0()) -> x,
                            minus(s(x), s(y)) -> minus(x, y),
                              quot(0(), s(y)) -> 0(),
                             quot(s(x), s(y)) -> s(quot(minus(x, y), s(y))),
    plus(minus(x, s(0())), minus(y, s(s(z)))) ->
    plus(minus(y, s(s(z))), minus(x, s(0()))),
                                 plus(0(), y) -> y,
                                plus(s(x), y) -> s(plus(x, y)),
      plus(plus(x, s(0())), plus(y, s(s(z)))) ->
    plus(plus(y, s(s(z))), plus(x, s(0())))
   }
  Fail