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