(VAR x)
(RULES
  f(g(x)) -> f(h(x,x))
  g(a) -> g(g(a))
  h(a,a) -> g(g(a))
)
(COMMENT from p.28 of \cite{Gra96thesis})