Exercise logic.propositional.dnf
Description
Proposition to DNF
Derivation
Final term is not finished
~(~((p || q) /\ (r <-> (T /\ p))) /\ ~((p || q) /\ (r <-> (T /\ p))))
⇒ logic.propositional.idempand~~((p || q) /\ (r <-> (T /\ p)))
⇒ logic.propositional.truezeroand~~((p || q) /\ (r <-> p))
⇒ logic.propositional.defequiv~~((p || q) /\ ((r /\ p) || (~r /\ ~p)))
⇒ logic.propositional.demorganand~(~(p || q) || ~((r /\ p) || (~r /\ ~p)))
⇒ logic.propositional.demorganor~((~p /\ ~q) || ~((r /\ p) || (~r /\ ~p)))
⇒ logic.propositional.demorganor~((~p /\ ~q) || (~(r /\ p) /\ ~(~r /\ ~p)))
⇒ logic.propositional.demorganand~((~p /\ ~q) || (~(r /\ p) /\ (~~r || ~~p)))
⇒ logic.propositional.notnot~((~p /\ ~q) || (~(r /\ p) /\ (r || ~~p)))
⇒ logic.propositional.notnot~((~p /\ ~q) || (~(r /\ p) /\ (r || p)))
⇒ logic.propositional.demorganand~((~p /\ ~q) || ((~r || ~p) /\ (r || p)))
⇒ logic.propositional.andoveror~((~p /\ ~q) || ((~r || ~p) /\ r) || ((~r || ~p) /\ p))
⇒ logic.propositional.andoveror~((~p /\ ~q) || (~r /\ r) || (~p /\ r) || ((~r || ~p) /\ p))
⇒ logic.propositional.andoveror~((~p /\ ~q) || (~r /\ r) || (~p /\ r) || (~r /\ p) || (~p /\ p))
⇒ logic.propositional.compland~((~p /\ ~q) || F || (~p /\ r) || (~r /\ p) || (~p /\ p))
⇒ logic.propositional.compland~((~p /\ ~q) || F || (~p /\ r) || (~r /\ p) || F)
⇒ logic.propositional.falsezeroor~((~p /\ ~q) || (~p /\ r) || (~r /\ p) || F)
⇒ logic.propositional.falsezeroor~((~p /\ ~q) || (~p /\ r) || (~r /\ p))