SIMPLIFY-UP : WFFOPSIMPLIFY-UP is a wff operation.
Apply any one active rewrite rule 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:
The result is of type GWFF.
The arguments have the following meaning:
GWFF : gwff after rewriting
TPS documentation homepage