CHANGE-TOP : WFFOPCHANGE-TOP is a wff operation.
Change the top connective of a formula. For example,
"cntop or" will change "A and B" into "A or B";
"cntop exists" will change "forall x P x" into "exists x P x".
The calling scheme for CHANGE-TOP is:
(CHANGE-TOP CONN GWFF)
The result is of type GWFF.
The arguments have the following meaning:
CONN : Connective or Quantifier
GWFF : Wff
TPS documentation homepage