UNAPPLY-RRULE-1* : WFFOPUNAPPLY-RRULE-1* is a wff operation.
Unapply a rewrite rule (active or inactive) repeatedly to
the current edwff. (i.e. apply it in the reverse direction).
If the rule is bidirectional, you will be prompted about
which direction to apply it in.
CAUTION: may not terminate.
The calling scheme for UNAPPLY-RRULE-1* is:
(UNAPPLY-RRULE-1* GWFF RULE)
The result is of type GWFF.
The arguments have the following meaning:
GWFF : gwff after rewriting
RULE : name of rule
TPS documentation homepage