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