• BASIC-SPEC
• BASIC-ITEMS
• SIG-ITEMS
• SORT-ITEM
• OP-ITEM
• OP-TYPE
• SORT-LIST
• OP-ATTR
• OP-HEAD
• ARG-DECL
• PRED-ITEM
• PRED-TYPE
• PRED-HEAD
• DATATYPE-DECL
• ALTERNATIVE
• COMPONENTS
• VAR-DECL
• FORMULA
• QUANTIFIER
• PRED-SYMB
• TERMS
• TERM
• OP-SYMB
• SORT
• OP-NAME
• PRED-NAME
• VAR
• ID
• TOKEN-ID
• MIXFIX-ID
• TOKEN-PLACES
• TOKEN-OR-PLACE
• TOKEN
• SIMPLE-ID

BASIC-SPEC

• BASIC-SPEC ::= "basic-spec" BASIC-ITEMS*
  ==>
  basic-spec(BASIC-ITEMS*([BASIC-ITEMS]))

BASIC-ITEMS

• BASIC-ITEMS ::= SIG-ITEMS
  ==>
  SIG-ITEMS(SIG-ITEMS)
• BASIC-ITEMS ::= "free-datatype" DATATYPE-DECL+
  ==>
  free-datatype(DATATYPE-DECL+([DATATYPE-DECL]))
• BASIC-ITEMS ::= "var-items" VAR-DECL+
  ==>
  var-items(VAR-DECL+([VAR-DECL]))
• BASIC-ITEMS ::= "local-var-axioms" VAR-DECL+ FORMULA+
  ==>
  local-var-axioms(VAR-DECL+([VAR-DECL]),FORMULA+([FORMULA]))
• BASIC-ITEMS ::= "axiom-items" FORMULA+
  ==>
  axiom-items(FORMULA+([FORMULA]))
• BASIC-ITEMS ::= "sort-gen" SIG-ITEMS+
  ==>
  sort-gen(SIG-ITEMS+([SIG-ITEMS]))

SIG-ITEMS

• SIG-ITEMS ::= "sort-items" SORT-ITEM+
  ==>
  sort-items(SORT-ITEM+([SORT-ITEM]))
• SIG-ITEMS ::= "op-items" OP-ITEM+
  ==>
  op-items(OP-ITEM+([OP-ITEM]))
• SIG-ITEMS ::= "pred-items" PRED-ITEM+
  ==>
  pred-items(PRED-ITEM+([PRED-ITEM]))
• SIG-ITEMS ::= "datatype-items" DATATYPE-DECL+
  ==>
  datatype-items(DATATYPE-DECL+([DATATYPE-DECL]))

SORT-ITEM

• SORT-ITEM ::="sort-decl" SORT+
  ==>
  sort-decl(SORT+([SORT]))
• SORT-ITEM ::="subsort-decl" SORT+ SORT
  ==>
  subsort-decl(SORT+([SORT]),SORT)
• SORT-ITEM ::="subsort-defn" SORT VAR SORT FORMULA
  ==>
  subsort-defn(SORT,VAR,SORT,FORMULA)
• SORT-ITEM ::= "iso-decl" SORT+
  ==>
  iso-decl(SORT+([SORT]))

OP-ITEM

• OP-ITEM ::= "op-decl" OP-NAME+ OP-TYPE OP-ATTR*
  ==>
  op-decl(OP-NAME+([OP-NAME]),OP-TYPE,OP-ATTR*([OP-ATTR]))
• OP-ITEM ::= "op-defn" OP-NAME OP-HEAD TERM
  ==>
  op-defn(OP-NAME,OP-HEAD,TERM)

OP-TYPE

• OP-TYPE ::= "total-op-type" SORT-LIST SORT
  ==>
  total-op-type(SORT-LIST,SORT)
• OP-TYPE ::= "partial-op-type" SORT-LIST SORT
  ==>
  partial-op-type(SORT-LIST,SORT)

SORT-LIST

• SORT-LIST ::= "sort-list" SORT*
  ==>
  sort-list(SORT*([SORT]))

OP-ATTR

• OP-ATTR ::= "associative"
  ==>
  associative
• OP-ATTR ::= "commutative"
  ==>
  commutative
• OP-ATTR ::= "idempotent"
  ==>
  idempotent
• OP-ATTR ::= "unit-op-attr" TERM
  ==>
  unit-op-attr(TERM)

OP-HEAD

• OP-HEAD ::= "total-op-head" ARG-DECL* SORT
  ==>
  total-op-head(ARG-DECL*([ARG-DECL]),SORT)
• OP-HEAD ::= "partial-op-head" ARG-DECL* SORT
  ==>
  partial-op-head(ARG-DECL*([ARG-DECL]),SORT)

ARG-DECL

• ARG-DECL ::= "arg-decl" VAR+ SORT
  ==>
  arg-decl(VAR+([VAR]),SORT)

PRED-ITEM

• PRED-ITEM ::= "pred-decl" PRED-NAME+ PRED-TYPE
  ==>
  pred-decl(PRED-NAME+([PRED-NAME]),PRED-TYPE)
• PRED-ITEM ::= "pred-defn" PRED-NAME PRED-HEAD FORMULA
  ==>
  pred-defn(PRED-NAME,PRED-HEAD,FORMULA)

PRED-TYPE

• PRED-TYPE ::= "pred-type" SORT-LIST
  ==>
  pred-type(SORT-LIST)

PRED-HEAD

• PRED-HEAD ::= "pred-head" ARG-DECL*
  ==>
  pred-head(ARG-DECL*([ARG-DECL]))

DATATYPE-DECL

• DATATYPE-DECL ::= "datatype-decl" SORT ALTERNATIVE+
  ==>
  datatype-decl(SORT,ALTERNATIVE+([ALTERNATIVE]))

ALTERNATIVE

• ALTERNATIVE ::= "total-construct" OP-NAME COMPONENTS*
  ==>
  total-construct(OP-NAME,COMPONENTS*([COMPONENTS]))
• ALTERNATIVE ::= "partial-construct" OP-NAME COMPONENTS+
  ==>
  partial-construct(OP-NAME,COMPONENTS+([COMPONENTS]))
• ALTERNATIVE ::= "subsorts" SORT+
  ==>
  subsorts(SORT+([SORT]))

COMPONENTS

• COMPONENTS ::= "total-select" OP-NAME+ SORT
  ==>
  total-select(OP-NAME+([OP-NAME]),SORT)
• COMPONENTS ::= "partial-select" OP-NAME+ SORT
  ==>
  partial-select(OP-NAME+([OP-NAME]),SORT)
• COMPONENTS ::= SORT
  ==>
  SORT(SORT)

VAR-DECL

• VAR-DECL ::= "var-decl" VAR+ SORT
  ==>
  var-decl(VAR+([VAR]),SORT)

FORMULA

• FORMULA ::= "quantification" QUANTIFIER VAR-DECL+ FORMULA
  ==>
  quantification(QUANTIFIER,VAR-DECL+([VAR-DECL]),FORMULA)
• FORMULA ::= "conjunction" FORMULA+
  ==>
  conjunction(FORMULA+[FORMULA])
• FORMULA ::= "disjunction" FORMULA+
  ==>
  disjunction(FORMULA+[FORMULA])
• FORMULA ::= "implication" FORMULA FORMULA
  ==>
  implication(FORMULA,FORMULA)
• FORMULA ::= "equivalence" FORMULA FORMULA
  ==>
  equivalence(FORMULA,FORMULA)
• FORMULA ::= "negation" FORMULA
  ==>
  negation(FORMULA)
• FORMULA ::= "true-atom"
  ==>
  true-atom
• FORMULA ::= "false-atom"
  ==>
  false-atom
• FORMULA ::= "predication" PRED-SYMB TERMS
  ==>
  predication(PRED-SYMB,TERMS)
• FORMULA ::= "definedness" TERM
  ==>
  definedness(TERM)
• FORMULA ::= "existl-equation" TERM TERM
  ==>
  existl-equation(TERM,TERM)
• FORMULA ::= "strong-equation" TERM TERM
  ==>
  strong-equation(TERM,TERM)
• FORMULA ::= "membership" TERM SORT
  ==>
  membership(TERM,SORT)

QUANTIFIER

PRED-SYMB

• PRED-SYMB ::= PRED-NAME
  ==>
  PRED-NAME(PRED-NAME)
• PRED-SYMB ::= "qual-pred-name" PRED-NAME PRED-TYPE
  ==>
  qual-pred-name(PRED-NAME,PRED-TYPE)

TERMS

• TERMS ::= "terms" TERM*
  ==>
  terms(TERM*([TERM]))

TERM

• TERM ::= ID
  ==>
  ID(ID)
• TERM ::= "qual-var" VAR SORT
  ==>
  qual-var(VAR,SORT)
• TERM ::= "application" OP-SYMB TERMS
  ==>
  application(OP-SYMB,TERMS)
• TERM ::= "sorted-term" TERM SORT
  ==>
  sorted-term(TERM,SORT)
• TERM ::= "cast" TERM SORT
  ==>
  cast(TERM,SORT)
• TERM ::= "conditional" TERM FORMULA TERM
  ==>
  conditional(TERM,FORMULA,TERM)

OP-SYMB

• OP-SYMB ::= OP-NAME
  ==>
  OP-NAME(OP-NAME)
• OP-SYMB ::= "qual-op-name" OP-NAME OP-TYPE
  ==>
  qual-op-name(OP-NAME,OP-TYPE)

SORT

• SORT ::= TOKEN-ID
  ==>
  TOKEN-ID(TOKEN-ID)

OP-NAME

• OP-NAME ::= ID
  ==>
  ID(ID)

PRED-NAME

• PRED-NAME ::= ID
  ==>
  ID(ID)

VAR

• VAR ::= SIMPLE-ID
  ==>
  SIMPLE-ID(SIMPLE-ID)

ID

• ID ::= TOKEN-ID
  ==>
  TOKEN-ID(TOKEN-ID)
• ID ::= MIXFIX-ID
  ==>
  MIXFIX-ID(MIXFIX-ID)

TOKEN-ID

• TOKEN-ID ::= TOKEN
  ==>
  TOKEN(TOKEN)

MIXFIX-ID

• MIXFIX-ID ::= TOKEN-PLACES
  ==>
  TOKEN-PLACES %% Maybe it should be TOKEN-PLACES(TOKEN-PLACES)

TOKEN-PLACES

• TOKEN-PLACES ::= "token-places" TOKEN-OR-PLACE+
  ==>
  token-places(TOKEN-OR-PLACE+([TOKEN-OR-PLACE]))

TOKEN-OR-PLACE

• TOKEN-OR-PLACE ::= TOKEN
  ==>
  TOKEN(TOKEN)
• TOKEN-OR-PLACE ::= PLACE
  ==>
  __

TOKEN

SIMPLE-ID