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