Exercise logic.propositional.dnf
Description
Proposition to DNF
Derivation
Final term is not finishedT /\ ~(~(~~q /\ ~q) /\ ~~~(p /\ ~q)) /\ ((T /\ ~~(q /\ q /\ q /\ T /\ T /\ q /\ T)) || (~r /\ ~r))
⇒ logic.propositional.notnotT /\ ~(~(~~q /\ ~q) /\ ~(p /\ ~q)) /\ ((T /\ ~~(q /\ q /\ q /\ T /\ T /\ q /\ T)) || (~r /\ ~r))
⇒ logic.propositional.demorganandT /\ ~(~(~~q /\ ~q) /\ (~p || ~~q)) /\ ((T /\ ~~(q /\ q /\ q /\ T /\ T /\ q /\ T)) || (~r /\ ~r))
⇒ logic.propositional.notnotT /\ ~(~(~~q /\ ~q) /\ (~p || q)) /\ ((T /\ ~~(q /\ q /\ q /\ T /\ T /\ q /\ T)) || (~r /\ ~r))