(VAR x y )
(RULES 
        ge(0, 0) -> true
        ge(s(x), 0) -> ge(x, 0)
        ge(0, s(0)) -> false
        ge(0, s(s(x))) -> ge(0, s(x))
        ge(s(x), s(y)) -> ge(x, y)
        minus(0, 0) -> 0
        minus(0, s(x)) -> minus(0, x)
        minus(s(x), 0) -> s(minus(x, 0))
        minus(s(x), s(y)) -> minus(x, y)
        plus(0, 0) -> 0
        plus(0, s(x)) -> s(plus(0, x))
        plus(s(x), y) -> s(plus(x, y))
        div(x, y) -> ify(ge(y, s(0)), x, y)
        ify(false, x, y) -> divByZeroError
        ify(true, x, y) -> if(ge(x, y), x, y)
        if(false, x, y) -> 0
        if(true, x, y) -> s(div(minus(x, y), y))
        
)