When an argument of an ac operator has that operator as its principal operator, LP replaces it by its arguments. For example, when + is ac, (a + b) + (c + d) flattens to a + b + c + d.
Furthermore, when a flattened term involving an ac operator has more than two arguments, LP sorts the arguments lexicographically; for example, when + is ac, (c + b) + a flattens to a + b + c.
Two-argument terms such as q <=> p, where <=> is the hardwired ac operator for boolean equivalence, are not flattened to p <=> q. This enables LP to orient them into rewrite rules in the direction the user (may have) intended.