Exercise logic.propositional.dnf
Description
Proposition to DNF
Derivation
Final term is not finished((~p || ~p) <-> ((p /\ q) || (p /\ q))) || (~p <-> ((p /\ q) || (p /\ q)))
⇒ logic.propositional.idempor(~p <-> ((p /\ q) || (p /\ q))) || (~p <-> ((p /\ q) || (p /\ q)))