APPLICATION ::= application OP-SYMB TERMS OP-SYMB ::= OP-NAME | QUAL-OP-NAME QUAL-OP-NAME ::= qual-op-name OP-NAME OP-TYPE TERMS ::= terms TERM*
An application of an operation symbol OS to some argument terms is written:
OS(T1, ..., Tn)When PS is a mixfix identifier, consisting of a sequence `t0__...__tn' of tokens or spaces ti separated by place-holders `__', the application may also be written:
t0T1t1...TntnWhen the operation symbol is a constant with no argument terms, its application is simply written `OS'.
Declaring different mixfix identifiers that involve some common tokens may lead to ambiguity, with different candidate groupings of the same sequence of tokens and terms. Such ambiguity prevents the enclosing atomic formula from being well-formed, irrespective of the declared profiles of the symbols involved, and generally has to be eliminated by use of explicit grouping parentheses. However, to allow the omission of some parentheses, infix identifiers are given weaker precedence than prefix identifiers, which in turn are given weaker precedence than postfix identifiers.
A qualified operation name QUAL-OP-NAME with type T is written:
(op ON:T)An unqualified operation name is simply written `ON'.
The application is well-sorted for some particular sort when there is a declaration of the operation name (with the argument and result sorts indicated by the type, if specified) such that all the argument terms are well-sorted for the respective argument sorts, and the result sort is the required sort. It then expands to an application of the qualified operation name to the fully-qualified expansions of the argument terms for those sorts.