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