(VAR x )
(RULES 
        f(s(x)) -> f(x)
        inf ->= s(inf)
)