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