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