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