Unapply all active rewrite rules

A --> B, and apply all active rewrite rules B <--> A in the backward

direction. (i.e. subformulas A are rewritten to B, modulo any functions

attached to the rules, so that the original gwff will be a rewrite

instance of the resulting gwff.)

The calling scheme for SIMPLIFY-UP* is:

(SIMPLIFY-UP* GWFF)

"GWFF"

The result is of type GWFF.

The arguments have the following meaning:

GWFF : gwff after rewriting

© 1988-99, Carnegie Mellon University.