BASIC-SPEC ::= basic-spec BASIC-ITEMS*
BASIC-ITEMS ::= SIG-ITEMS | FREE-DATATYPE | SORT-GEN
| VAR-ITEMS | LOCAL-VAR-AXIOMS | AXIOM-ITEMS
SIG-ITEMS ::= SORT-ITEMS | OP-ITEMS | PRED-ITEMS
| DATATYPE-ITEMS
SORT-ITEMS ::= sort-items SORT-ITEM+
SORT-ITEM ::= SORT-DECL
SORT-DECL ::= sort-decl SORT+
OP-ITEMS ::= op-items OP-ITEM+
OP-ITEM ::= OP-DECL | OP-DEFN
OP-DECL ::= op-decl OP-NAME+ OP-TYPE OP-ATTR*
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*
OP-ATTR ::= BINARY-OP-ATTR | UNIT-OP-ATTR
BINARY-OP-ATTR ::= associative | commutative | idempotent
UNIT-OP-ATTR ::= unit-op-attr TERM
OP-DEFN ::= op-defn OP-NAME OP-HEAD TERM
OP-HEAD ::= TOTAL-OP-HEAD | PARTIAL-OP-HEAD
TOTAL-OP-HEAD ::= total-op-head ARG-DECL* SORT
PARTIAL-OP-HEAD ::= partial-op-head ARG-DECL* SORT
ARG-DECL ::= arg-decl VAR+ SORT
PRED-ITEMS ::= pred-items PRED-ITEM+
PRED-ITEM ::= PRED-DECL | PRED-DEFN
PRED-DECL ::= pred-decl PRED-NAME+ PRED-TYPE
PRED-TYPE ::= pred-type SORTS
PRED-DEFN ::= pred-defn PRED-NAME PRED-HEAD FORMULA
PRED-HEAD ::= pred-head ARG-DECL*
DATATYPE-ITEMS ::= datatype-items DATATYPE-DECL+
DATATYPE-DECL ::= datatype-decl SORT ALTERNATIVE+
ALTERNATIVE ::= TOTAL-CONSTRUCT | PARTIAL-CONSTRUCT
TOTAL-CONSTRUCT ::= total-construct OP-NAME COMPONENTS*
PARTIAL-CONSTRUCT::= partial-construct OP-NAME COMPONENTS*
COMPONENTS ::= TOTAL-SELECT | PARTIAL-SELECT | SORT
TOTAL-SELECT ::= total-select OP-NAME+ SORT
PARTIAL-SELECT ::= partial-select OP-NAME+ SORT
FREE-DATATYPE ::= free-datatype DATATYPE-ITEMS
SORT-GEN ::= sort-gen SIG-ITEMS+
VAR-ITEMS ::= var-items VAR-DECL+
VAR-DECL ::= var-decl VAR+ SORT
LOCAL-VAR-AXIOMS ::= local-var-axioms VAR-DECL+ AXIOM+
AXIOM-ITEMS ::= axiom-items AXIOM+
AXIOM ::= FORMULA
FORMULA ::= QUANTIFICATION | CONJUNCTION | DISJUNCTION
| IMPLICATION | EQUIVALENCE | NEGATION | ATOM
QUANTIFICATION ::= quantification QUANTIFIER VAR-DECL+ FORMULA
QUANTIFIER ::= forall | exists | exists-uniquely
CONJUNCTION ::= conjunction FORMULA+
DISJUNCTION ::= disjunction FORMULA+
IMPLICATION ::= implication FORMULA FORMULA
EQUIVALENCE ::= equivalence FORMULA FORMULA
NEGATION ::= negation FORMULA
ATOM ::= TRUTH | PREDICATION | DEFINEDNESS
| EXISTL-EQUATION | STRONG-EQUATION
TRUTH ::= true | false
PREDICATION ::= predication PRED-SYMB TERMS
PRED-SYMB ::= PRED-NAME | QUAL-PRED-NAME
QUAL-PRED-NAME ::= qual-pred-name PRED-NAME PRED-TYPE
DEFINEDNESS ::= definedness TERM
EXISTL-EQUATION ::= existl-equation TERM TERM
STRONG-EQUATION ::= strong-equation TERM TERM
TERMS ::= terms TERM*
TERM ::= SIMPLE-ID | QUAL-VAR | APPLICATION
| SORTED-TERM | CONDITIONAL
QUAL-VAR ::= qual-var VAR SORT
APPLICATION ::= application OP-SYMB TERMS
OP-SYMB ::= OP-NAME | QUAL-OP-NAME
QUAL-OP-NAME ::= qual-op-name OP-NAME OP-TYPE
SORTED-TERM ::= sorted-term TERM SORT
CONDITIONAL ::= conditional TERM FORMULA TERM
SORT ::= TOKEN-ID
OP-NAME ::= ID
PRED-NAME ::= ID
VAR ::= SIMPLE-ID
ID ::= TOKEN-ID | MIXFIX-ID
TOKEN-ID ::= TOKEN
MIXFIX-ID ::= TOKEN-PLACES
TOKEN-PLACES ::= token-places TOKEN-OR-PLACE+
TOKEN-OR-PLACE ::= TOKEN | PLACE
TOKEN ::= WORDS | SIGNS | DOT-WORDS
SIMPLE-ID ::= WORDS
