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