(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) G(B',B) -> F(A,A) G(B,B') -> F(A,A) F(A,A') -> G(B,B) F(A',A) -> G(B,B) G(B',B') -> F(A,A) F(A',A') -> G(B,B) )