(VAR X X1 X2 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(n__div(n__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)
        div(X1, X2) -> n__div(X1, X2)
        minus(X1, X2) -> n__minus(X1, X2)
        activate(n__0) -> 0
        activate(n__s(X)) -> s(activate(X))
        activate(n__div(X1, X2)) -> div(activate(X1), X2)
        activate(n__minus(X1, X2)) -> minus(X1, X2)
        activate(X) -> X
        
)