⁴Maude 1 did not allow multiple membership axioms on associative operators. In Maude 3 this works, although it will be extremely inefficient for large terms, since matching the extra membership essentially amounts to expanding out the equivalence class.