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