Exercise logic.propositional.dnf
Description
Proposition to DNF
Derivation
Final term is not finished
~~(~(q -> r) /\ ~(q -> r)) || ~~q || r
⇒ logic.propositional.idempand~~~(q -> r) || ~~q || r
⇒ logic.propositional.defimpl~~~(~q || r) || ~~q || r
⇒ logic.propositional.demorganor~~(~~q /\ ~r) || ~~q || r
⇒ logic.propositional.notnot~~(q /\ ~r) || ~~q || r