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