MIN-QUANTIFIER-SCOPE : FLAGMIN-QUANTIFIER-SCOPE is a flag or parameter.
When this flag is T, the scope of quantifiers is minimized before
starting expansion proofs.
If an eproof is found with this flag set to T, during the translation
of the eproof to an ND proof RULEQ is called to fill the gap between
the theorem as originally stated and its min-quantifier-scope version.
MIN-QUANTIFIER-SCOPE takes values of type BOOLEAN.
It belongs to subjects MS98-1 MS93-1 MS92-9 MS91-7 MS91-6 MS90-9 MS90-3 MS89 MS88 MATING-SEARCH ETREES .
Its default value is NIL
Its current value is NIL.
TPS documentation homepage