Exercise logic.propositional.dnf
Description
Proposition to DNF
Derivation
(T /\ (q || r)) || ~(q -> r)
⇒ logic.propositional.defimpl(T /\ (q || r)) || ~(~q || r)
⇒ logic.propositional.demorganor(T /\ (q || r)) || (~~q /\ ~r)
⇒ logic.propositional.notnot(T /\ (q || r)) || (q /\ ~r)
⇒ logic.propositional.truezeroandq || r || (q /\ ~r)