¹As usual, the ground Church-Rosser and termination assumptions should be understood modulo any axioms $A\subseteq E$ which in Maude are declared as equational attributes of operators.