Converts a term already in negation normal form into disjunctive normal form.
DESCRIPTION
When applied to a term already in negation normal form (see NNF_CONV),
meaning that all other propositional connectives have been eliminated in favour
of disjunction, disjunction and negation, and negation is only applied to
atomic formulas, DNF_CONV puts the term into an equivalent disjunctive normal
form, which is a right-associated disjunction of conjunctions without
repetitions. No reduction by subsumption is performed, however, e.g. from
a \/ a /\ b to just a).
FAILURE CONDITIONS
Never fails; non-Boolean terms will just yield a reflexive theorem.
EXAMPLE
# DNF_CONV `(a \/ b) /\ (a \/ c /\ e)`;;
val it : thm =
|- (a \/ b) /\ (a \/ c /\ e) <=> a \/ a /\ b \/ a /\ c /\ e \/ b /\ c /\ e