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