Equations and rewrite rules can also be conditional rules, which means they have to fulfill some criteria to be applied to the term (other than just matching the left hand side of the rewrite rule).

The rules are applied at "random" by the Maude system, meaning that you can not be sure that one rule is applied before another rule and so on. If an equation can be applied to the term, it will always be applied before any rewrite rule. Maude's built-in search can look for unwanted states and show that no such states can be reached. Maude