(VAR x) (RULES a -> b a -> f(a, a) f(x, a) -> a ) (COMMENT p.29 of \cite{IWC16} GWCR & ~WCR & ~GCR )