(VAR x ) (RULES f(g(x)) -> f(a(g(g(f(x))), g(f(x)))) )