(from AG01 3.26) (VAR x) (RULES f(x) -> s(x) f(s(s(x))) -> s(f(f(x))) )