Exercise logic.propositional.dnf

Description
Proposition to DNF

Derivation

Final term is not finished
(((F || ~q) /\ ~(p -> q)) -> p) || ~((F || ~q) /\ ~(p -> q)) || p
logic.propositional.falsezeroor
(((F || ~q) /\ ~(p -> q)) -> p) || ~(~q /\ ~(p -> q)) || p
logic.propositional.demorganand
(((F || ~q) /\ ~(p -> q)) -> p) || ~~q || ~~(p -> q) || p
logic.propositional.notnot
(((F || ~q) /\ ~(p -> q)) -> p) || q || ~~(p -> q) || p
logic.propositional.notnot
(((F || ~q) /\ ~(p -> q)) -> p) || q || (p -> q) || p
logic.propositional.defimpl
(((F || ~q) /\ ~(p -> q)) -> p) || q || ~p || q || p