BASIC-SPEC ::= basic-spec BASIC-ITEMS*
BASIC-ITEMS ::= SIG-ITEMS
| free-datatype DATATYPE-DECL+
| sort-gen SIG-ITEMS+
| var-items VAR-DECL+
| local-var-axioms VAR-DECL+ FORMULA+
| axiom-items FORMULA+
SIG-ITEMS ::= sort-items SORT-ITEM+
| op-items OP-ITEM+
| pred-items PRED-ITEM+
| datatype-items DATATYPE-DECL+
SORT-ITEM ::= sort-decl SORT+
| subsort-decl SORT+ SORT
| subsort-defn SORT VAR SORT FORMULA
| iso-decl SORT+
OP-ITEM ::= op-decl OP-NAME+ OP-TYPE OP-ATTR*
| op-defn OP-NAME OP-HEAD TERM
OP-TYPE ::= total-op-type SORTS SORT
| partial-op-type SORTS SORT
SORTS ::= sorts SORT*
OP-ATTR ::= associative | commutative | idempotent
| unit-op-attr TERM
OP-HEAD ::= total-op-head ARG-DECL* SORT
| partial-op-head ARG-DECL* SORT
ARG-DECL ::= arg-decl VAR+ SORT
PRED-ITEM ::= pred-decl PRED-NAME+ PRED-TYPE
| pred-defn PRED-NAME PRED-HEAD FORMULA
PRED-TYPE ::= pred-type SORTS
PRED-HEAD ::= pred-head ARG-DECL*
DATATYPE-DECL ::= datatype-decl SORT ALTERNATIVE+
ALTERNATIVE ::= total-construct OP-NAME COMPONENTS*
| partial-construct OP-NAME COMPONENTS*
| subsorts SORT+
COMPONENTS ::= total-select OP-NAME+ SORT
| partial-select OP-NAME+ SORT
| SORT
VAR-DECL ::= var-decl VAR+ SORT
FORMULA ::= quantification QUANTIFIER VAR-DECL+ FORMULA
| conjunction FORMULA+
| disjunction FORMULA+
| implication FORMULA FORMULA
| equivalence FORMULA FORMULA
| negation FORMULA
| true | false
| predication PRED-SYMB TERMS
| definedness TERM
| existl-equation TERM TERM
| strong-equation TERM TERM
| membership TERM SORT
QUANTIFIER ::= forall | exists | exists-uniquely
! PRED-SYMB ::= PRED-NAME | qual-pred-name PRED-NAME PRED-TYPE
TERMS ::= terms TERM*
TERM ::= SIMPLE-ID
| qual-var VAR SORT
| application OP-SYMB TERMS
| sorted-term TERM SORT
| cast TERM SORT
| conditional TERM FORMULA TERM
! OP-SYMB ::= OP-NAME | qual-op-name OP-NAME OP-TYPE
SORT ::= TOKEN-ID
OP-NAME ::= ID
PRED-NAME ::= ID
VAR ::= SIMPLE-ID
