MIN-QUANT-SCOPE : WFFOPMIN-QUANT-SCOPE is a wff operation.
Minimize the scope of quantifiers in a gwff. Deletes vacuous
quantifiers. During proof transformation, the gap between a formula
and its min-quant-scope version is filled by RULEQ.
The calling scheme for MIN-QUANT-SCOPE is:
The result is of type GVAR.
TPS documentation homepage