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