Recursively apply the distributive laws to a wff in

the contracting direction:

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

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

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

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

The command format for DIST-CTR* is:

<Ed>DIST-CTR* <<GWFF>>

<<GWFF>>

The result replaces the current wff.

© 1988-99, Carnegie Mellon University.