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