DIST-EXP* : EDOPDIST-EXP* is an editor command.
Recursively apply the distributive laws to a wff 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 command format for DIST-EXP* is:
The result replaces the current wff.
TPS documentation homepage