(VAR x )
(RULES 
        f(tt,x) -> f(isNat(x),s(s(x)))
        isNat(s(x)) -> isNat(x)
        isNat(0) -> tt
        
)