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