(VAR x)
(RULES
  f(a) -> f(f(a))
  f(x) -> f(a)
)
(COMMENT
doi:10.1109/LICS.2002.1029852
[25] Example 3
submitted by: Takahito Aoto, Junichi Yoshida, and Yoshihito Toyama
)