A sort-generation constraint SORT-GEN is well-formed when all the sorts and function symbols specified in it are declared in the local environment (it does not itself declare any sorts and function symbols). It then determines the corresponding sentence. Here, a FUN-SYMB that is just a FUN-NAME (without an explicit FUN-TYPE) abbreviates the list of all those declared function symbols whose name has the same identifier as the specified FUN-NAME.SORT-GEN ::= sort-gen SORT+ FUN-SYMB+