²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 [75, 96] 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=\mathit{\text{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.