Exercise logic.propositional.dnf
Description
Proposition to DNF
Derivation
T /\ ((q /\ T /\ ~~~(q /\ q)) || (T /\ ~~(p /\ ~r) /\ ~~(p /\ ~r) /\ T /\ ~~~(q /\ q))) /\ T /\ ~~~(q /\ q)
⇒ logic.propositional.truezeroand((q /\ T /\ ~~~(q /\ q)) || (T /\ ~~(p /\ ~r) /\ ~~(p /\ ~r) /\ T /\ ~~~(q /\ q))) /\ T /\ ~~~(q /\ q)
⇒ logic.propositional.truezeroand((q /\ T /\ ~~~(q /\ q)) || (T /\ ~~(p /\ ~r) /\ ~~(p /\ ~r) /\ T /\ ~~~(q /\ q))) /\ ~~~(q /\ q)
⇒ logic.propositional.idempand((q /\ T /\ ~~~(q /\ q)) || (T /\ ~~(p /\ ~r) /\ T /\ ~~~(q /\ q))) /\ ~~~(q /\ q)
⇒ logic.propositional.notnot((q /\ T /\ ~~~(q /\ q)) || (T /\ ~~(p /\ ~r) /\ T /\ ~~~(q /\ q))) /\ ~(q /\ q)
⇒ logic.propositional.idempand((q /\ T /\ ~~~(q /\ q)) || (T /\ ~~(p /\ ~r) /\ T /\ ~~~(q /\ q))) /\ ~q
⇒ logic.propositional.truezeroand((q /\ ~~~(q /\ q)) || (T /\ ~~(p /\ ~r) /\ T /\ ~~~(q /\ q))) /\ ~q
⇒ logic.propositional.notnot((q /\ ~(q /\ q)) || (T /\ ~~(p /\ ~r) /\ T /\ ~~~(q /\ q))) /\ ~q
⇒ logic.propositional.idempand((q /\ ~q) || (T /\ ~~(p /\ ~r) /\ T /\ ~~~(q /\ q))) /\ ~q
⇒ logic.propositional.compland(F || (T /\ ~~(p /\ ~r) /\ T /\ ~~~(q /\ q))) /\ ~q
⇒ logic.propositional.falsezeroorT /\ ~~(p /\ ~r) /\ T /\ ~~~(q /\ q) /\ ~q
⇒ logic.propositional.truezeroand~~(p /\ ~r) /\ T /\ ~~~(q /\ q) /\ ~q
⇒ logic.propositional.truezeroand~~(p /\ ~r) /\ ~~~(q /\ q) /\ ~q
⇒ logic.propositional.notnotp /\ ~r /\ ~~~(q /\ q) /\ ~q
⇒ logic.propositional.notnotp /\ ~r /\ ~(q /\ q) /\ ~q
⇒ logic.propositional.idempandp /\ ~r /\ ~q /\ ~q
⇒ logic.propositional.idempandp /\ ~r /\ ~q