Exercise logic.propositional.dnf
Description
Proposition to DNF
Derivation
((q || (~(~p /\ ~p) /\ p)) /\ (q || T)) || (~(~p /\ ~p) /\ p /\ T)
⇒ logic.propositional.idempand((q || (~~p /\ p)) /\ (q || T)) || (~(~p /\ ~p) /\ p /\ T)
⇒ logic.propositional.notnot((q || (p /\ p)) /\ (q || T)) || (~(~p /\ ~p) /\ p /\ T)
⇒ logic.propositional.idempand((q || p) /\ (q || T)) || (~(~p /\ ~p) /\ p /\ T)
⇒ logic.propositional.truezeroand((q || p) /\ (q || T)) || (~(~p /\ ~p) /\ p)
⇒ logic.propositional.idempand((q || p) /\ (q || T)) || (~~p /\ p)
⇒ logic.propositional.notnot((q || p) /\ (q || T)) || (p /\ p)
⇒ logic.propositional.idempand((q || p) /\ (q || T)) || p
⇒ logic.propositional.truezeroor((q || p) /\ T) || p
⇒ logic.propositional.truezeroandq || p || p
⇒ logic.propositional.idemporq || p