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.