WFF-SUB-IMPLIES* : WFFOPWFF-SUB-IMPLIES* is a wff operation.
Recursively apply the following law to a formula:
A implies B --> not A or B.
The calling scheme for WFF-SUB-IMPLIES* is:
The result is of type GWFF.
The arguments have the following meaning:
GWFF : Wff
TPS documentation homepage