Exercise logic.propositional.dnf
Description
Proposition to DNF
Derivation
Final term is not finished~(~((p || q) /\ (r <-> p)) || F)
⇒ logic.propositional.defequiv~(~((p || q) /\ ((r /\ p) || (~r /\ ~p))) || F)
⇒ logic.propositional.demorganand~(~(p || q) || ~((r /\ p) || (~r /\ ~p)) || F)
⇒ logic.propositional.demorganor~((~p /\ ~q) || ~((r /\ p) || (~r /\ ~p)) || F)
⇒ logic.propositional.demorganor~((~p /\ ~q) || (~(r /\ p) /\ ~(~r /\ ~p)) || F)
⇒ logic.propositional.demorganand~((~p /\ ~q) || (~(r /\ p) /\ (~~r || ~~p)) || F)
⇒ logic.propositional.falsezeroor~((~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))