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