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