Unconditional memberships

Unconditional membership axioms specify terms as having a given sort. They are declared with the keyword mb followed by a term, followed by `:', followed by a sort (that must always be in the same kind as that of the term), followed by a period. As equations, memberships can optionally have statement attributes (see Section 4.5).

  mb $\langle$Term$\rangle$ : $\langle$Sort$\rangle$ [$\langle$StatementAttributes$\rangle$] .

To illustrate this, consider the module 3*NAT with the basic Peano number declarations as in the NUMBERS module and a new sort 3*Nat.

The fact that 3*Nat consists of multiples of 3 is expressed using the subsort declaration Zero < 3*Nat < Nat and the membership statement mb (s s s M3) : 3*Nat for M3 a variable of sort 3*Nat.

  fmod 3*NAT is
    sort Zero Nat .
    subsort Zero < Nat .
    op zero : -> Zero .
    op s_ : Nat -> Nat .

    sort 3*Nat .
    subsorts Zero < 3*Nat < Nat .
    var M3 : 3*Nat .
    mb (s s s M3) : 3*Nat  .
  endfm

Memberships axioms can interact in undesirable ways with operators that are declared with the assoc or iter attributes (see later Sections 4.4.1 and 4.4.2, respectively). This is explained and illustrated with examples in Sections 13.2.8 and 13.2.9.