Exercise logic.propositional.dnf
Description
Proposition to DNF
Derivation
Final term is not finished
T /\ ((T /\ p /\ p /\ ~(T /\ ~p) /\ T) || q || F)
⇒ logic.propositional.idempandT /\ ((T /\ p /\ ~(T /\ ~p) /\ T) || q || F)
⇒ logic.propositional.truezeroandT /\ ((p /\ ~(T /\ ~p) /\ T) || q || F)
⇒ logic.propositional.truezeroandT /\ ((p /\ ~(T /\ ~p)) || q || F)
⇒ logic.propositional.truezeroandT /\ ((p /\ ~~p) || q || F)
⇒ logic.propositional.notnotT /\ ((p /\ p) || q || F)
⇒ logic.propositional.idempandT /\ (p || q || F)