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