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