³Note the use of the equivalent single-identifier-form for on-the-fly declarations of variables; as we will see in Section 15.5, this is one of the syntactic restrictions of Full Maude.