TRS:
 {    minus(X, 0()) -> X,
  minus(s(X), s(Y)) -> p(minus(X, Y)),
            p(s(X)) -> X,
     div(0(), s(Y)) -> 0(),
    div(s(X), s(Y)) -> s(div(minus(X, Y), s(Y)))}
 Fail