! BASIC-SPEC ::= BASIC-ITEMS... | { }
BASIC-ITEMS ::= SIG-ITEMS
| var/vars VAR-DECL;...;VAR-DECL ;/
| var/vars VAR-DECL;...;VAR-DECL
"." FORMULA"."..."."FORMULA ;/
| axiom/axioms FORMULA;...;FORMULA ;/
| generated { SIG-ITEMS... } ;/
| generated type/types DATATYPE-DECL;...;DATATYPE-DECL ;/
| free type/types DATATYPE-DECL;...;DATATYPE-DECL ;/
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;... "." 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...
| 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
