8An alternative specification is available in Maude’s prelude, see Section 8.15.