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