<!ELEMENT specification (start,(fragment_pi|fragment_sigma)?,(variables|distinct_variables)?,(constants|unary|binary|union|sequence|binary_sym|binary_sym_neq|binary_neq|constants_set)+)>

<!ELEMENT start EMPTY>

<!ELEMENT variables (symbol+)>
<!ELEMENT distinct_variables EMPTY>

<!ELEMENT fragment_pi EMPTY>
<!ELEMENT fragment_sigma EMPTY>

<!ELEMENT constants (symbol+)>

<!ELEMENT unary (symbol,child)>
<!ELEMENT binary (symbol,child,child)>
<!ELEMENT union (child+)>
<!ELEMENT sequence (symbol,child+)>

<!ELEMENT binary_sym (symbol,child)>
<!ELEMENT binary_sym_neq (symbol,child)>
<!ELEMENT binary_neq (symbol,child)>

<!ELEMENT constants_set (child)>

<!ELEMENT child EMPTY>
<!ELEMENT symbol EMPTY>

<!ATTLIST constants id ID #REQUIRED>
<!ATTLIST variables id ID #REQUIRED>
<!ATTLIST distinct_variables id ID #REQUIRED>

<!ATTLIST unary id ID #REQUIRED>
<!ATTLIST binary id ID #REQUIRED>
<!ATTLIST union id ID #REQUIRED>
<!ATTLIST sequence id ID #REQUIRED>

<!ATTLIST binary_sym id ID #REQUIRED>
<!ATTLIST binary_sym_neq id ID #REQUIRED>
<!ATTLIST binary_neq id ID #REQUIRED>

<!ATTLIST constants_set id ID #REQUIRED>
<!ATTLIST constants_set size CDATA #IMPLIED>

<!ATTLIST child idref IDREF #REQUIRED>
<!ATTLIST symbol value CDATA #REQUIRED>

<!ATTLIST start idref IDREF #REQUIRED>
<!ATTLIST fragment_pi value CDATA #REQUIRED>
<!ATTLIST fragment_sigma value CDATA #REQUIRED>