**Go up to** 4.2 Axioms

**Go forward to** 4.2.2 Terms

### 4.2.1 Atomic Formulae

ATOM ::= ... | MEMBERSHIP

As for many-sorted specifications, an atomic formula is well-formed
(with respect to the current declarations) if it is well-sorted and
expands to a unique atomic formula for constructing sentences of the
underlying institution--but now for subsorted specifications,
uniqueness is required only up to an *equivalence* on atomic
formulae and terms.
This equivalence is the least one including fully-qualified terms that
are the same up to profiles of operation symbols in the overloading
relation * *__<__ _{F} and embedding, and fully-qualified atomic formulae
that are the same up to the profiles of predicate symbols in the
overloading relation * *__<__ _{P} and embedding.

The notions of when an atomic formula or term is *well-sorted*
and of its *expansion* are indicated below for the various
subsorting constructs. Due not only to overloading of predicate
and/or operation symbols, but also to implicit embeddings from
subsorts into supersorts, a well-sorted atomic formula
**[CHANGED:]** may have several non-equivalent expansions, preventing it from being
well-formed. Qualifications on operation and predicate symbols, or
explicit sorts on terms, may be used to determine the intended
expansion (up to the equivalence indicated above) and make
the enclosing formula
**[]** well-formed.

CoFI
Document: CASL/Summary-v1.0 -- Version: 1.0 -- 22 October 1998.

Comments to cofi-language@brics.dk