(from AG01 4.18) (VAR x) (RULES a(b(a(b(x)))) -> b(a(b(a(a(b(x)))))) )