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