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) || ~~q || ~~F || ~(~~(p /\ ~q) /\ ~F /\ T) || ~(T /\ ~~T) || ~(p /\ p) || ~~~~~(p /\ ~q))
⇒ logic.propositional.idempand~(~(((T /\ ~~q) || ~r) /\ ~q) || ~~q || ~~F || ~(~~(p /\ ~q) /\ ~F /\ T) || ~(T /\ ~~T) || ~p || ~~~~~(p /\ ~q))
⇒ logic.propositional.notnot~(~(((T /\ ~~q) || ~r) /\ ~q) || q || ~~F || ~(~~(p /\ ~q) /\ ~F /\ T) || ~(T /\ ~~T) || ~p || ~~~~~(p /\ ~q))
⇒ logic.propositional.notnot~(~(((T /\ ~~q) || ~r) /\ ~q) || q || F || ~(~~(p /\ ~q) /\ ~F /\ T) || ~(T /\ ~~T) || ~p || ~~~~~(p /\ ~q))
⇒ logic.propositional.falsezeroor~(~(((T /\ ~~q) || ~r) /\ ~q) || q || ~(~~(p /\ ~q) /\ ~F /\ T) || ~(T /\ ~~T) || ~p || ~~~~~(p /\ ~q))
⇒ logic.propositional.notnot~(~(((T /\ ~~q) || ~r) /\ ~q) || q || ~(~~(p /\ ~q) /\ ~F /\ T) || ~(T /\ ~~T) || ~p || ~~~(p /\ ~q))
⇒ logic.propositional.notnot~(~(((T /\ ~~q) || ~r) /\ ~q) || q || ~(~~(p /\ ~q) /\ ~F /\ T) || ~(T /\ ~~T) || ~p || ~(p /\ ~q))
⇒ logic.propositional.demorganand~(~(((T /\ ~~q) || ~r) /\ ~q) || q || ~(~~(p /\ ~q) /\ ~F /\ T) || ~(T /\ ~~T) || ~p || ~p || ~~q)
⇒ logic.propositional.idempor~(~(((T /\ ~~q) || ~r) /\ ~q) || q || ~(~~(p /\ ~q) /\ ~F /\ T) || ~(T /\ ~~T) || ~p || ~~q)
⇒ logic.propositional.notnot~(~(((T /\ ~~q) || ~r) /\ ~q) || q || ~(~~(p /\ ~q) /\ ~F /\ T) || ~(T /\ ~~T) || ~p || q)
⇒ logic.propositional.truezeroand~(~((~~q || ~r) /\ ~q) || q || ~(~~(p /\ ~q) /\ ~F /\ T) || ~(T /\ ~~T) || ~p || q)
⇒ logic.propositional.notnot~(~((q || ~r) /\ ~q) || q || ~(~~(p /\ ~q) /\ ~F /\ T) || ~(T /\ ~~T) || ~p || q)
⇒ logic.propositional.andoveror~(~((q /\ ~q) || (~r /\ ~q)) || q || ~(~~(p /\ ~q) /\ ~F /\ T) || ~(T /\ ~~T) || ~p || q)
⇒ logic.propositional.compland~(~(F || (~r /\ ~q)) || q || ~(~~(p /\ ~q) /\ ~F /\ T) || ~(T /\ ~~T) || ~p || q)
⇒ logic.propositional.falsezeroor~(~(~r /\ ~q) || q || ~(~~(p /\ ~q) /\ ~F /\ T) || ~(T /\ ~~T) || ~p || q)
⇒ logic.propositional.demorganand~(~~r || ~~q || q || ~(~~(p /\ ~q) /\ ~F /\ T) || ~(T /\ ~~T) || ~p || q)
⇒ logic.propositional.notnot~(r || ~~q || q || ~(~~(p /\ ~q) /\ ~F /\ T) || ~(T /\ ~~T) || ~p || q)
⇒ logic.propositional.notnot~(r || q || q || ~(~~(p /\ ~q) /\ ~F /\ T) || ~(T /\ ~~T) || ~p || q)
⇒ logic.propositional.idempor~(r || q || ~(~~(p /\ ~q) /\ ~F /\ T) || ~(T /\ ~~T) || ~p || q)
⇒ logic.propositional.truezeroand~(r || q || ~(~~(p /\ ~q) /\ ~F) || ~(T /\ ~~T) || ~p || q)
⇒ logic.propositional.notfalse~(r || q || ~(~~(p /\ ~q) /\ T) || ~(T /\ ~~T) || ~p || q)
⇒ logic.propositional.truezeroand~(r || q || ~~~(p /\ ~q) || ~(T /\ ~~T) || ~p || q)
⇒ logic.propositional.notnot~(r || q || ~(p /\ ~q) || ~(T /\ ~~T) || ~p || q)
⇒ logic.propositional.demorganand~(r || q || ~p || ~~q || ~(T /\ ~~T) || ~p || q)
⇒ logic.propositional.notnot~(r || q || ~p || q || ~(T /\ ~~T) || ~p || q)
⇒ logic.propositional.truezeroand~(r || q || ~p || q || ~~~T || ~p || q)
⇒ logic.propositional.notnot~(r || q || ~p || q || ~T || ~p || q)
⇒ logic.propositional.nottrue~(r || q || ~p || q || F || ~p || q)
⇒ logic.propositional.falsezeroor~(r || q || ~p || q || ~p || q)
⇒ logic.propositional.idempor~(r || q || ~p || q)