²Coherence of E modulo Ax is very closely related to the notion of coherence of rules relative to equations explained in Section 5.3; see [66] for the precise definition of coherence in the equational case. The main role of coherence of E modulo Ax is to get the effect of rewriting in Ax-equivalence classes with E. For example, for Ax = AC, coherence modulo AC is easily achieved by adding to each equation in E with a top AC function symbol in its lefthand side a similar equation with an extra “extension variable” argument added to the AC function symbol, as explained in Section 4.8. Section 4.8 also explains how, for rewriting modulo axioms Ax supported by Maude, Maude automatically performs such a coherence completion in an implicit, built-in way using extension variables and “extension aware” Ax-matching algorithms.