Apply distributivity laws to a formula in the expanding direction:

A and (B or C) --> (A and B) or (A and C)

A or (B and C) --> (A or B) and (A or C)

(B or C) and A --> (B and A) or (C and A)

(B and C) or A --> (B or A) and (C or A).

The calling scheme for WFF-DIST-EXPAND is:

(WFF-DIST-EXPAND GWFF)

"GWFF"

The result is of type GWFF.

The arguments have the following meaning:

GWFF : Wff

© 1988-99, Carnegie Mellon University.