(VAR x)
(RULES
f(x,x) -> s(s(x))
infty -> s(infty)
)