BASIC-SPEC ::= BASIC-ITEMS...BASIC-ITEMS | { }
BASIC-ITEMS ::= SIG-ITEMS
| free type/types DATATYPE-DECL ;...; DATATYPE-DECL ;/
| generated type/types DATATYPE-DECL ;...; DATATYPE-DECL ;/
| generated { SIG-ITEMS...SIG-ITEMS } ;/
| var/vars VAR-DECL ;...; VAR-DECL ;/
| var/vars VAR-DECL ;...; VAR-DECL
"." FORMULA "."..."." FORMULA ;/
| axiom/axioms FORMULA ;...; FORMULA ;/
SIG-ITEMS ::= sort/sorts SORT-ITEM ;...; SORT-ITEM ;/
| op/ops OP-ITEM ;...; OP-ITEM ;/
| pred/preds PRED-ITEM ;...; PRED-ITEM ;/
| type/types DATATYPE-DECL ;...; DATATYPE-DECL ;/
SORT-ITEM ::= SORT ,..., SORT
| SORT ,..., SORT < SORT
| SORT = { VAR : SORT "." FORMULA }
| SORT =...= SORT
OP-ITEM ::= OP-NAME ,..., OP-NAME : OP-TYPE
| OP-NAME ,..., OP-NAME : OP-TYPE , OP-ATTR ,..., OP-ATTR
| OP-NAME OP-HEAD = TERM
OP-TYPE ::= SOME-SORTS -> SORT | SORT
| SOME-SORTS ->? SORT | ? SORT
SOME-SORTS ::= SORT *...* SORT
OP-ATTR ::= assoc | comm | idem | unit TERM
OP-HEAD ::= ( ARG-DECL ;...; ARG-DECL ) : SORT | : SORT
| ( ARG-DECL ;...; ARG-DECL ) :? SORT | :? SORT
ARG-DECL ::= VAR ,..., VAR : SORT
PRED-ITEM ::= PRED-NAME ,..., PRED-NAME : PRED-TYPE
| PRED-NAME PRED-HEAD <=> FORMULA
| PRED-NAME <=> FORMULA
PRED-TYPE ::= SOME-SORTS | ( )
PRED-HEAD ::= ( ARG-DECL ;...; ARG-DECL )
DATATYPE-DECL ::= SORT "::=" ALTERNATIVE "|"..."|" ALTERNATIVE
ALTERNATIVE ::= OP-NAME ( COMPONENT ;...; COMPONENT )
| OP-NAME ( COMPONENT ;...; COMPONENT )?
| OP-NAME
| sort/sorts SORT ,..., SORT
COMPONENT ::= OP-NAME ,..., OP-NAME : SORT
| OP-NAME ,..., OP-NAME :? SORT
| SORT
VAR-DECL ::= VAR ,..., VAR : SORT
FORMULA ::= QUANTIFIER VAR-DECL ;...; VAR-DECL "." FORMULA
| FORMULA /\ FORMULA /\.../\ FORMULA
| FORMULA \/ FORMULA \/...\/ FORMULA
| FORMULA => FORMULA
| FORMULA if FORMULA
| FORMULA <=> FORMULA
| not FORMULA
| true | false
| PRED-SYMB
| PRED-SYMB ( TERMS )
| TERM TERM...TERM
| def TERM
| TERM =e= TERM
| TERM = TERM
| TERM in SORT
| ( FORMULA )
QUANTIFIER ::= forall | exists | exists!
PRED-SYMB ::= PRED-NAME | ( pred QUAL-PRED-NAME )
QUAL-PRED-NAME ::= PRED-NAME : PRED-TYPE
TERMS ::= TERM ,..., TERM
TERM ::= SIMPLE-TERM...SIMPLE-TERM
SIMPLE-TERM ::= ID
| ( var VAR : SORT )
| ( op QUAL-OP-NAME )
| OP-SYMB ( TERMS )
| SIMPLE-TERM : SORT
| SIMPLE-TERM as SORT
| TERM when FORMULA else TERM
| ( TERM )
OP-SYMB ::= OP-NAME | ( op QUAL-OP-NAME )
QUAL-OP-NAME ::= OP-NAME : OP-TYPE
SORT ::= TOKEN-ID
OP-NAME ::= ID
PRED-NAME ::= ID
VAR ::= SIMPLE-ID
ID ::= TOKEN-ID | MIXFIX-ID
TOKEN-ID ::= TOKEN
MIXFIX-ID ::= TOKEN-OR-PLACE...TOKEN-OR-PLACE
TOKEN-OR-PLACE ::= TOKEN | PLACE
TOKEN ::= WORDS | SIGNS | DOT-WORDS
SIMPLE-ID ::= WORDS
