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