OP-DECL ::= op-decl OP-NAME+ OP-TYPE OP-ATTR* OP-NAME ::= ID
An operation declaration OP-DECL is written:
f1, ..., fn : T,
A1, ..., Am
 When the list A1, ..., Am is empty, the declaration
is written simply:
f1, ..., fn : T
It declares each operation name f1, ..., fn as a total or partial operation, with profile as specified by the operation type T, and as having the attributes A1, ..., Am (if any).
OP-TYPE ::= TOTAL-OP-TYPE | PARTIAL-OP-TYPE TOTAL-OP-TYPE ::= total-op-type SORTS SORT PARTIAL-OP-TYPE ::= partial-op-type SORTS SORT SORTS ::= sorts SORT*
A total operation type TOTAL-OP-TYPE with some argument sorts is written:
s1×...×sn -> sWhen the list of argument sorts is empty, the type is simply written `s'. The sign displayed as `×' may be input as `×' in ISO Latin-1, or as `*' in ASCII. The sign displayed as an arrow in LaTeX is input as `->'.
A partial operation type PARTIAL-OP-TYPE with some argument sorts is written:
s1×...×sn ->? sWhen the list of argument sorts is empty, the type is simply written [CHANGED:] `? s'.  The operation profile determined by the type has argument sorts s1, ..., sn and result sort s.
OP-ATTR ::= BINARY-OP-ATTR | UNIT-OP-ATTR BINARY-OP-ATTR ::= associative | commutative | idempotent UNIT-OP-ATTR ::= unit-op-attr TERM
Operation attributes assert that the operations being declared (which must be binary) have certain common properties, which are characterized by strong equations, universally quantified over variables of the appropriate sort. [CHANGED:] (This can also be used to add attributes to operations that have previously been declared without them.)  The attribute associative is written `assoc'. It asserts the associativity of an operation f:
f(x, f(y,z)) = f(f(x,y),z)The attribute of associativity moreover implies a parsing annotation that allows an [CHANGED:] infix operation f of the form  `__t__' (or `__ __') to be iterated without explicit grouping parentheses.
The attribute commutative is written `comm'. It asserts the commutativity of an operation f:
f(x,y) = f(y,x)
The attribute idempotent is written `idem'. It asserts the idempotency of an operation f:
f(x,x) = x
The attribute UNIT-OP-ATTR is written `unitT'. It asserts that the value of the term T is the unit (left and right) of an operation f:
f(T,x) = x /\ f(x, T) = xIn practice, the unit T is normally a constant. [CHANGED:] In any case, T must not contain any variables.  The declaration enclosing an operation attribute is ill-formed unless the operation profile has exactly two argument sorts, both the same as the result sort.