(VAR x ) (RULES a(a(f(b, a(x)))) -> f(a(a(a(x))), b) a(a(x)) -> f(b, a(f(a(x), b))) f(a(x), b) -> f(b, a(x)) )