A variable declaration VAR-DECL determines sorted variables for use in axioms; it does not contribute to the signature. Such a declaration of a variable as a BASIC-ITEM abbreviates adding a universal quantification on that variable to all axioms in the enclosing BASIC-SPEC. The variables in the list VAR+ must be distinct, and distinct from the variables previously declared by other VAR-DECLs in the same list of basic items A simple identifier SIMPLE-ID for a variable may not be used simultaneously as the identifier of a sort, function, or predicate.VAR-DECL ::= var-decl VAR+ SORT VAR ::= SIMPLE-ID