! BASIC-SPEC ::= BASIC-ITEMS...
BASIC-ITEMS ::= SORT-ITEMS | OP-ITEMS | SORT-GEN-ITEMS
| VAR-ITEMS | AXIOM-ITEMS
! SORT-ITEMS ::= SORT-S SORT-ITEM;...
SORT-S ::= sort | sorts
SORT-ITEM ::= SORT-DECL | SUBSORT-DECL | SUBSORT-DEFN
| ISO-DECL | DATATYPE-DECL
SORT-DECL ::= SORT,...,SORT
SUBSORT-DECL ::= SORT,...,SORT < SORT
SUBSORT-DEFN ::= SORT = { VAR : SORT . FORMULA }
ISO-DECL ::= SORT,...,SORT = SORT
! DATATYPE-DECL ::= SORT "::=" ALTERNATIVE "|"..."|" ALTERNATIVE
ALTERNATIVE ::= CONSTRUCT | SUBSORTS
CONSTRUCT ::= FUN-NAME : COMPONENT *...* COMPONENT | FUN-NAME
! | FUN-NAME :? COMPONENT *...* COMPONENT
! COMPONENT ::= ( FUN-NAME,...,FUN-NAME : SORT ) | SORT
! | ( FUN-NAME,...,FUN-NAME :? SORT )
SUBSORTS ::= SORT-S SORT,...,SORT
! OP-ITEMS ::= OP-S OP-ITEM;...
OP-S ::= op | ops
! OP-ITEM ::= FUN-DECL | FUN-DEFN | PRED-DECL | PRED-DEFN
! FUN-DECL ::= FUN-NAME,...,FUN-NAME : FUN-TYPE FUN-ATTRS
! FUN-TYPE ::= TOTAL-FUN-TYPE | PARTIAL-FUN-TYPE | ( FUN-TYPE )
TOTAL-FUN-TYPE ::= SORTS -> SORT | SORT
PARTIAL-FUN-TYPE ::= SORTS ->? SORT | ? SORT
SORTS ::= SORT *...* SORT
FUN-DEFN ::= FUN-NAME FUN-HEAD = TERM
FUN-HEAD ::= TOTAL-FUN-HEAD | PARTIAL-FUN-HEAD
TOTAL-FUN-HEAD ::= ( ARG-DECLS ) : SORT | : SORT
PARTIAL-FUN-HEAD ::= ( ARG-DECLS ) :? SORT | :? SORT
ARG-DECLS ::= ARG-DECL;...;ARG-DECL
ARG-DECL ::= VAR,...,VAR : SORT
! FUN-ATTRS ::= ,FUN-ATTR,...,FUN-ATTR | EMPTY
! FUN-ATTR ::= assoc | comm | idem | unit FUN-SYMB
PRED-DECL ::= PRED-NAME,...,PRED-NAME : PRED-TYPE
PRED-TYPE ::= pred ( SORTS ) | pred ( )
PRED-DEFN ::= PRED-NAME PRED-HEAD <=> FORMULA
PRED-HEAD ::= ( ARG-DECLS ) | EMPTY
! SORT-GEN-ITEMS ::= OPT-FREELY generated SIG-DECL-GROUP
! OPT-FREELY ::= freely | EMPTY
! SIG-DECL-GROUP ::= { SIG-DECL-ITEMS;... }
| SORT-S SORT-ITEM | OP-S OP-ITEM
SIG-DECL-ITEMS ::= SORT-ITEMS | OP-ITEMS
! VAR-ITEMS ::= VAR-S VAR-DECL;...
VAR-S ::= var | vars
VAR-DECL ::= VAR,...,VAR : SORT
! AXIOM-ITEMS ::= AXIOM-S; ATOM;... | AXIOM-S; | AXIOM-S
! AXIOM-S ::= axiom AXIOM | axioms AXIOM | QUANTIFICATION
AXIOM ::= FORMULA
! FORMULA ::= QUANTIFICATION | CONJUNCTION | DISJUNCTION
! | IMPLICATION | EQUIVALENCE | NEGATION | ATOM
| (FORMULA)
! QUANTIFICATION ::= QUANTIFIER VAR-DECL;... . FORMULA . ... . FORMULA
! QUANTIFIER ::= forall | exists | exists!
CONJUNCTION ::= FORMULA /\ FORMULA /\.../\ FORMULA
DISJUNCTION ::= FORMULA \/ FORMULA \/...\/ FORMULA
IMPLICATION ::= FORMULA => FORMULA | FORMULA if FORMULA
EQUIVALENCE ::= FORMULA <=> FORMULA
NEGATION ::= not FORMULA
ATOM ::= TRUTH | PREDICATION | DEFINEDNESS
| EXISTL-EQUATION | STRONG-EQUATION | MEMBERSHIP
TRUTH ::= true | false
PREDICATION ::= PRED-SYMB ( TERMS ) | PRED-SYMB | MIXFIX-TERMS
! PRED-SYMB ::= PRED-NAME : PRED-TYPE | PRED-NAME | ( PRED-SYMB )
! DEFINEDNESS ::= defined TERM
! EXISTL-EQUATION ::= TERM =.= TERM
STRONG-EQUATION ::= TERM = TERM
MEMBERSHIP ::= TERM in SORT
TERMS ::= TERM,...,TERM
! MIXFIX-TERMS ::= MIX-TERM MIX-TERM ... MIX-TERM
! MIX-TERM ::= MIX-ID | TERM
TERM ::= VAR | APPLICATION | SORTED-TERM | CAST
| ( TERM )
APPLICATION ::= FUN-SYMB ( TERMS ) | FUN-SYMB | MIXFIX-TERMS
! FUN-SYMB ::= FUN-NAME : FUN-TYPE | FUN-NAME | ( FUN-SYMB )
SORTED-TERM ::= TERM : SORT
CAST ::= TERM as SORT
! SORT ::= WORDS-ID
FUN-NAME ::= ID
PRED-NAME ::= ID
! VAR ::= WORDS
EMPTY ::=
