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