! BASIC-SPEC ::= basic-spec BASIC-ITEMS*
! BASIC-ITEMS ::= SIG-ITEMS
! | var-items VAR-DECL+
! | local-var-axioms VAR-DECL+ FORMULA+
! | axiom-items FORMULA+
! | sort-gen SIG-ITEMS+
! | free-datatype DATATYPE-DECL+
! 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
! QUAL-PRED-NAME ::= qual-pred-name PRED-NAME PRED-TYPE
TERMS ::= terms TERM*
! TERM ::= VAR-OR-CONST
! | qual-var VAR SORT
| application OP-SYMB TERMS
| sorted-term TERM SORT
| cast TERM SORT
! OP-SYMB ::= OP-NAME | QUAL-OP-NAME
! QUAL-OP-NAME ::= qual-op-name OP-NAME OP-TYPE
SORT ::= ID
OP-NAME ::= ID
PRED-NAME ::= ID
VAR ::= SIMPLE-ID
! VAR-OR-CONST ::= SIMPLE-ID
ID ::= SIMPLE-ID
SIMPLE-ID ::= ...
