An ATTRIBUTION of some properties to some function symbols FUN-SYMB+ abbreviates evident axioms asserting that each of the functions is to have each of the specified properties. Here, a FUN-SYMB that is just a FUN-NAME (without an explicit FUN-TYPE) abbreviates the list of all those function symbols declared in the local environment whose name has the same identifier as the specified FUN-NAME. The ATTRIBUTION is well-formed just when the axioms that it abbreviates are well-formed--in particular, this generally requires that each specified function symbol takes two arguments, both of the same sort.BASIC-ITEM ::= ... | ATTRIBUTION ATTRIBUTION ::= attribution PROPERTY+ FUN-SYMB+ PROPERTY ::= SIMPLE-PROPERTY | UNIT-PROPERTY SIMPLE-PROPERTY ::= associative | commutative | idempotent UNIT-PROPERTY ::= unit-property FUN-SYMB