(VAR x y )
(STRATEGY INNERMOST)
(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))
        
)