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