Exercise logic.propositional.dnf
Description
Proposition to DNF
Derivation
Final term is not finished(~T || ~(~(q /\ ~q) /\ ~F /\ ~(p /\ ~q))) /\ ((~r /\ T /\ T) || (q /\ T))
⇒ logic.propositional.compland(~T || ~(~F /\ ~F /\ ~(p /\ ~q))) /\ ((~r /\ T /\ T) || (q /\ T))
⇒ logic.propositional.idempand(~T || ~(~F /\ ~(p /\ ~q))) /\ ((~r /\ T /\ T) || (q /\ T))
⇒ logic.propositional.notfalse(~T || ~(T /\ ~(p /\ ~q))) /\ ((~r /\ T /\ T) || (q /\ T))
⇒ logic.propositional.nottrue(F || ~(T /\ ~(p /\ ~q))) /\ ((~r /\ T /\ T) || (q /\ T))
⇒ logic.propositional.falsezeroor~(T /\ ~(p /\ ~q)) /\ ((~r /\ T /\ T) || (q /\ T))
⇒ logic.propositional.truezeroand~~(p /\ ~q) /\ ((~r /\ T /\ T) || (q /\ T))
⇒ logic.propositional.notnotp /\ ~q /\ ((~r /\ T /\ T) || (q /\ T))