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