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