Exercise logic.propositional.dnf
Description
Proposition to DNF
Derivation
Final term is not finishedT /\ ~(F || ~((q || ~r) /\ ~(~(q /\ ~q) /\ ~(~~p /\ ~q) /\ ~(~~p /\ ~q))))
⇒ logic.propositional.falsezeroorT /\ ~~((q || ~r) /\ ~(~(q /\ ~q) /\ ~(~~p /\ ~q) /\ ~(~~p /\ ~q)))
⇒ logic.propositional.idempandT /\ ~~((q || ~r) /\ ~(~(q /\ ~q) /\ ~(~~p /\ ~q)))
⇒ logic.propositional.complandT /\ ~~((q || ~r) /\ ~(~F /\ ~(~~p /\ ~q)))
⇒ logic.propositional.notfalseT /\ ~~((q || ~r) /\ ~(T /\ ~(~~p /\ ~q)))
⇒ logic.propositional.truezeroandT /\ ~~((q || ~r) /\ ~~(~~p /\ ~q))
⇒ logic.propositional.notnotT /\ ~~((q || ~r) /\ ~~p /\ ~q)
⇒ logic.propositional.notnotT /\ ~~((q || ~r) /\ p /\ ~q)
⇒ logic.propositional.gendemorganandT /\ ~(~(q || ~r) || ~p || ~~q)
⇒ logic.propositional.demorganorT /\ ~((~q /\ ~~r) || ~p || ~~q)
⇒ logic.propositional.notnotT /\ ~((~q /\ r) || ~p || ~~q)
⇒ logic.propositional.notnotT /\ ~((~q /\ r) || ~p || q)