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