Exercise logic.propositional.dnf
Description
Proposition to DNF
Derivation
F || q || (~p -> (~~p || (F /\ r))) || q
⇒ logic.propositional.falsezeroandF || q || (~p -> (~~p || F)) || q
⇒ logic.propositional.falsezeroorq || (~p -> (~~p || F)) || q
⇒ logic.propositional.falsezeroorq || (~p -> ~~p) || q
⇒ logic.propositional.notnotq || (~p -> p) || q
⇒ logic.propositional.defimplq || ~~p || p || q
⇒ logic.propositional.notnotq || p || p || q
⇒ logic.propositional.idemporq || p || q