/home/nowonder/forschung/aprove/TPDB05/TRS/Rubio/gm.trs

The program

(VAR X Y)
(RULES

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)))

)

Submit to AProVE Web Frontend

Edit in AProVE Web Frontend