Exercise logic.propositional.dnf

Description
Proposition to DNF

Derivation

~~((q || (~~~(r /\ T) /\ ~~~(r /\ T))) /\ T /\ ~~((q /\ ~q) || (p /\ ~q))) || ~(T /\ T /\ ~F /\ T /\ ~F)
logic.propositional.idempand
~~((q || (~~~(r /\ T) /\ ~~~(r /\ T))) /\ T /\ ~~((q /\ ~q) || (p /\ ~q))) || ~(T /\ ~F /\ T /\ ~F)
logic.propositional.idempand
~~((q || (~~~(r /\ T) /\ ~~~(r /\ T))) /\ T /\ ~~((q /\ ~q) || (p /\ ~q))) || ~(T /\ ~F)
logic.propositional.notnot
((q || (~~~(r /\ T) /\ ~~~(r /\ T))) /\ T /\ ~~((q /\ ~q) || (p /\ ~q))) || ~(T /\ ~F)
logic.propositional.truezeroand
((q || (~~~(r /\ T) /\ ~~~(r /\ T))) /\ ~~((q /\ ~q) || (p /\ ~q))) || ~(T /\ ~F)
logic.propositional.idempand
((q || ~~~(r /\ T)) /\ ~~((q /\ ~q) || (p /\ ~q))) || ~(T /\ ~F)
logic.propositional.notnot
((q || ~(r /\ T)) /\ ~~((q /\ ~q) || (p /\ ~q))) || ~(T /\ ~F)
logic.propositional.notnot
((q || ~(r /\ T)) /\ ((q /\ ~q) || (p /\ ~q))) || ~(T /\ ~F)
logic.propositional.compland
((q || ~(r /\ T)) /\ (F || (p /\ ~q))) || ~(T /\ ~F)
logic.propositional.falsezeroor
((q || ~(r /\ T)) /\ p /\ ~q) || ~(T /\ ~F)
logic.propositional.truezeroand
((q || ~r) /\ p /\ ~q) || ~(T /\ ~F)
logic.propositional.andoveror
(q /\ p /\ ~q) || (~r /\ p /\ ~q) || ~(T /\ ~F)
logic.propositional.truezeroand
(q /\ p /\ ~q) || (~r /\ p /\ ~q) || ~~F
logic.propositional.notnot
(q /\ p /\ ~q) || (~r /\ p /\ ~q) || F
logic.propositional.falsezeroor
(q /\ p /\ ~q) || (~r /\ p /\ ~q)