(VAR x) (RULES F(x,x) -> A F(x,G(x)) -> B C -> G(C) ) (COMMENT from p.813 of \cite{Hue80})