Exercise logic.propositional.dnf
Description
Proposition to DNF
Derivation
Final term is not finished
T /\ ((~q /\ ~~(T /\ (F || ~~p) /\ ~q)) -> p) /\ T
⇒ logic.propositional.truezeroandT /\ ((~q /\ ~~(T /\ (F || ~~p) /\ ~q)) -> p)
⇒ logic.propositional.notnotT /\ ((~q /\ T /\ (F || ~~p) /\ ~q) -> p)
⇒ logic.propositional.truezeroandT /\ ((~q /\ (F || ~~p) /\ ~q) -> p)
⇒ logic.propositional.falsezeroorT /\ ((~q /\ ~~p /\ ~q) -> p)
⇒ logic.propositional.notnotT /\ ((~q /\ p /\ ~q) -> p)
⇒ logic.propositional.defimplT /\ (~(~q /\ p /\ ~q) || p)
⇒ logic.propositional.gendemorganandT /\ (~~q || ~p || ~~q || p)
⇒ logic.propositional.notnotT /\ (q || ~p || ~~q || p)
⇒ logic.propositional.notnotT /\ (q || ~p || q || p)