ALTERNATIVE ::= ... | SUBSORTS
SUBSORTS ::= subsorts SORT+
A subsorts alternative is written:
sorts s1, ..., snAs with sort declarations, the plural keyword may be written in the singular (regardless of the number of sorts).
The sorts si, which must be already declared in the local environment, are declared to be embedded as subsorts of the sort declared by the enclosing datatype declaration. (`sorts s1, ..., sn' and `sort s1 | ... | sort sn' are equivalent.)
In a free datatype declaration, all the sorts that are embedded in the declared sort by the alternatives must have no common subsorts. When the alternatives of a free datatype declaration are all subsorts, the declared sort corresponds to the [CHANGED:] disjoint [] union of the subsorts. [CHANGED:] Finally, the constructors of a free datatype must neither be in the overloading relation with each other nor with functions in the local environment. In particular, this condition is fulfilled if the operation names introduced by the free datatype construct are new and distinct from each other. []