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