Exercise logic.propositional.dnf

Description
Proposition to DNF

Derivation

((F || ~p) -> (F /\ r)) || q
logic.propositional.falsezeroand
((F || ~p) -> F) || q
logic.propositional.falsezeroor
(~p -> F) || q
logic.propositional.defimpl
~~p || F || q
logic.propositional.falsezeroor
~~p || q
logic.propositional.notnot
p || q