(VAR x y )
(RULES 
        f(x, y) -> cond(and(isNat(x), isNat(y)), x, y)
        cond(tt, x, y) -> f(s(x), s(y))
        isNat(s(x)) -> isNat(x)
        isNat(0) -> tt
        and(tt, tt) -> tt
        and(ff, x) -> ff
        and(x, ff) -> ff
        
)