SIMPLIFY-UP* : WFFOP

SIMPLIFY-UP* is a wff operation.
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

TPS documentation homepage


© 1988-99, Carnegie Mellon University.

TPS homepage