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