⁵Note that the _+_ operator has no identity attribute. Operationally, "" works as an identity when adding ground strings, but it is not an identity in the usual Maude sense. Thus, the term X:String + "" does not reduce.