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