(VAR x)
(RULES
  F(A,A) -> G(B,B)
  A -> A'
  F(A',x) -> F(x,x)
  F(x,A') -> F(x,x)
  G(B,B) -> F(A,A)
  B -> B'
  G(B',x) -> G(x,x)
  G(x,B') -> G(x,x)
)
(COMMENT
doi:10.1145/322217.322230
[12] p. 814, attributed to Levy
submitted by: Takahito Aoto, Junichi Yoshida, and Yoshihito Toyama
)