WFF-DIST-CONTRACT* : WFFOPWFF-DIST-CONTRACT* is a wff operation.
Recursively apply distributivity laws to a formula 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 calling scheme for WFF-DIST-CONTRACT* is:
The result is of type GWFF.
The arguments have the following meaning:
GWFF : Wff
TPS documentation homepage