(VAR X Y )
(RULES 
        p(0) -> 0
        p(s(X)) -> X
        leq(0, Y) -> true
        leq(s(X), 0) -> false
        leq(s(X), s(Y)) -> leq(X, Y)
        if(true, X, Y) -> activate(X)
        if(false, X, Y) -> activate(Y)
        diff(X, Y) -> if(leq(X, Y), n__0, n__s(diff(p(X), Y)))
        0 -> n__0
        s(X) -> n__s(X)
        activate(n__0) -> 0
        activate(n__s(X)) -> s(X)
        activate(X) -> X
        
)