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