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