Recursively apply the following law to a formula:

A implies B --> not A or B.

The calling scheme for WFF-SUB-IMPLIES* is:

(WFF-SUB-IMPLIES* GWFF)

"GWFF"

The result is of type GWFF.

The arguments have the following meaning:

GWFF : Wff

© 1988-99, Carnegie Mellon University.