package logtk

flatten_ac f l flattens the list of terms l by deconstructing all its elements that have f as head symbol. For instance, if l=1+2; 3+(4+5) with f="+", this will return 1;2;3;4;5, perhaps in a different order

normal form of the term modulo AC

Check whether the two terms are AC-equal. Optional arguments specify which symbols are AC or commutative (by default by looking at attr_ac and attr_commut).

Set of symbols occurring in the terms, that are AC