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 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.