(VAR X Y )
(RULES 
        minus(0, Y) -> 0
        minus(s(X), s(Y)) -> minus(X, Y)
        geq(X, 0) -> true
        geq(0, s(Y)) -> false
        geq(s(X), s(Y)) -> geq(X, Y)
        div(0, s(Y)) -> 0
        div(s(X), s(Y)) -> if(geq(X, Y), s(div(minus(X, Y), s(Y))), 0)
        if(true, X, Y) -> X
        if(false, X, Y) -> Y
        
)