PREDICATION ::= predication PRED-SYMB TERMS PRED-SYMB ::= PRED-NAME | QUAL-PRED-NAME QUAL-PRED-NAME ::= qual-pred-name PRED-NAME PRED-TYPE TERMS ::= terms TERM*
An application of a predicate symbol PS to some argument terms is written:
PS(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 predicate symbol is a constant with no argument terms, its application is simply written `PS'.
A qualified predicate name QUAL-PRED-NAME with type T is written:
(pred p:T)An unqualified predicate name PRED-NAME is simply written `p'.
The application of the predicate symbol is well-sorted when there is a declaration of the predicate name (with the argument sorts indicated by the indicated type in the case of a qualified predicate name) such that all the argument terms are well-sorted for the respective argument sorts. It then expands to an application of the qualified predicate name to the fully-qualified expansions of the argument terms for those sorts.