Exercise logic.propositional.dnf
Description
Proposition to DNF
Derivation
((~(~(q /\ ~q) /\ ~(p /\ ~q)) /\ T /\ q /\ q) || (T /\ ~r)) /\ ((~(~(q /\ ~q) /\ ~(p /\ ~q)) /\ T /\ q /\ q) || (~r /\ ~(~(q /\ ~q) /\ ~(p /\ ~q)))) /\ ((~(~(q /\ ~q) /\ ~(p /\ ~q)) /\ T /\ q /\ q) || (~(~(q /\ ~q) /\ ~(p /\ ~q)) /\ ~r))
⇒ logic.propositional.compland((~(~(q /\ ~q) /\ ~(p /\ ~q)) /\ T /\ q /\ q) || (T /\ ~r)) /\ ((~(~(q /\ ~q) /\ ~(p /\ ~q)) /\ T /\ q /\ q) || (~r /\ ~(~F /\ ~(p /\ ~q)))) /\ ((~(~(q /\ ~q) /\ ~(p /\ ~q)) /\ T /\ q /\ q) || (~(~(q /\ ~q) /\ ~(p /\ ~q)) /\ ~r))
⇒ logic.propositional.compland((~(~(q /\ ~q) /\ ~(p /\ ~q)) /\ T /\ q /\ q) || (T /\ ~r)) /\ ((~(~(q /\ ~q) /\ ~(p /\ ~q)) /\ T /\ q /\ q) || (~r /\ ~(~F /\ ~(p /\ ~q)))) /\ ((~(~(q /\ ~q) /\ ~(p /\ ~q)) /\ T /\ q /\ q) || (~(~F /\ ~(p /\ ~q)) /\ ~r))
⇒ logic.propositional.idempand((~(~(q /\ ~q) /\ ~(p /\ ~q)) /\ T /\ q) || (T /\ ~r)) /\ ((~(~(q /\ ~q) /\ ~(p /\ ~q)) /\ T /\ q /\ q) || (~r /\ ~(~F /\ ~(p /\ ~q)))) /\ ((~(~(q /\ ~q) /\ ~(p /\ ~q)) /\ T /\ q /\ q) || (~(~F /\ ~(p /\ ~q)) /\ ~r))
⇒ logic.propositional.idempand((~(~(q /\ ~q) /\ ~(p /\ ~q)) /\ T /\ q) || (T /\ ~r)) /\ ((~(~(q /\ ~q) /\ ~(p /\ ~q)) /\ T /\ q) || (~r /\ ~(~F /\ ~(p /\ ~q)))) /\ ((~(~(q /\ ~q) /\ ~(p /\ ~q)) /\ T /\ q /\ q) || (~(~F /\ ~(p /\ ~q)) /\ ~r))
⇒ logic.propositional.idempand((~(~(q /\ ~q) /\ ~(p /\ ~q)) /\ T /\ q) || (T /\ ~r)) /\ ((~(~(q /\ ~q) /\ ~(p /\ ~q)) /\ T /\ q) || (~r /\ ~(~F /\ ~(p /\ ~q)))) /\ ((~(~(q /\ ~q) /\ ~(p /\ ~q)) /\ T /\ q) || (~(~F /\ ~(p /\ ~q)) /\ ~r))
⇒ logic.propositional.notfalse((~(~(q /\ ~q) /\ ~(p /\ ~q)) /\ T /\ q) || (T /\ ~r)) /\ ((~(~(q /\ ~q) /\ ~(p /\ ~q)) /\ T /\ q) || (~r /\ ~(T /\ ~(p /\ ~q)))) /\ ((~(~(q /\ ~q) /\ ~(p /\ ~q)) /\ T /\ q) || (~(~F /\ ~(p /\ ~q)) /\ ~r))
⇒ logic.propositional.notfalse((~(~(q /\ ~q) /\ ~(p /\ ~q)) /\ T /\ q) || (T /\ ~r)) /\ ((~(~(q /\ ~q) /\ ~(p /\ ~q)) /\ T /\ q) || (~r /\ ~(T /\ ~(p /\ ~q)))) /\ ((~(~(q /\ ~q) /\ ~(p /\ ~q)) /\ T /\ q) || (~(T /\ ~(p /\ ~q)) /\ ~r))
⇒ logic.propositional.truezeroand((~(~(q /\ ~q) /\ ~(p /\ ~q)) /\ q) || (T /\ ~r)) /\ ((~(~(q /\ ~q) /\ ~(p /\ ~q)) /\ T /\ q) || (~r /\ ~(T /\ ~(p /\ ~q)))) /\ ((~(~(q /\ ~q) /\ ~(p /\ ~q)) /\ T /\ q) || (~(T /\ ~(p /\ ~q)) /\ ~r))
⇒ logic.propositional.compland((~(~F /\ ~(p /\ ~q)) /\ q) || (T /\ ~r)) /\ ((~(~(q /\ ~q) /\ ~(p /\ ~q)) /\ T /\ q) || (~r /\ ~(T /\ ~(p /\ ~q)))) /\ ((~(~(q /\ ~q) /\ ~(p /\ ~q)) /\ T /\ q) || (~(T /\ ~(p /\ ~q)) /\ ~r))
⇒ logic.propositional.notfalse((~(T /\ ~(p /\ ~q)) /\ q) || (T /\ ~r)) /\ ((~(~(q /\ ~q) /\ ~(p /\ ~q)) /\ T /\ q) || (~r /\ ~(T /\ ~(p /\ ~q)))) /\ ((~(~(q /\ ~q) /\ ~(p /\ ~q)) /\ T /\ q) || (~(T /\ ~(p /\ ~q)) /\ ~r))
⇒ logic.propositional.truezeroand((~~(p /\ ~q) /\ q) || (T /\ ~r)) /\ ((~(~(q /\ ~q) /\ ~(p /\ ~q)) /\ T /\ q) || (~r /\ ~(T /\ ~(p /\ ~q)))) /\ ((~(~(q /\ ~q) /\ ~(p /\ ~q)) /\ T /\ q) || (~(T /\ ~(p /\ ~q)) /\ ~r))
⇒ logic.propositional.notnot((p /\ ~q /\ q) || (T /\ ~r)) /\ ((~(~(q /\ ~q) /\ ~(p /\ ~q)) /\ T /\ q) || (~r /\ ~(T /\ ~(p /\ ~q)))) /\ ((~(~(q /\ ~q) /\ ~(p /\ ~q)) /\ T /\ q) || (~(T /\ ~(p /\ ~q)) /\ ~r))
⇒ logic.propositional.compland((p /\ F) || (T /\ ~r)) /\ ((~(~(q /\ ~q) /\ ~(p /\ ~q)) /\ T /\ q) || (~r /\ ~(T /\ ~(p /\ ~q)))) /\ ((~(~(q /\ ~q) /\ ~(p /\ ~q)) /\ T /\ q) || (~(T /\ ~(p /\ ~q)) /\ ~r))
⇒ logic.propositional.falsezeroand(F || (T /\ ~r)) /\ ((~(~(q /\ ~q) /\ ~(p /\ ~q)) /\ T /\ q) || (~r /\ ~(T /\ ~(p /\ ~q)))) /\ ((~(~(q /\ ~q) /\ ~(p /\ ~q)) /\ T /\ q) || (~(T /\ ~(p /\ ~q)) /\ ~r))
⇒ logic.propositional.falsezeroorT /\ ~r /\ ((~(~(q /\ ~q) /\ ~(p /\ ~q)) /\ T /\ q) || (~r /\ ~(T /\ ~(p /\ ~q)))) /\ ((~(~(q /\ ~q) /\ ~(p /\ ~q)) /\ T /\ q) || (~(T /\ ~(p /\ ~q)) /\ ~r))
⇒ logic.propositional.truezeroand~r /\ ((~(~(q /\ ~q) /\ ~(p /\ ~q)) /\ T /\ q) || (~r /\ ~(T /\ ~(p /\ ~q)))) /\ ((~(~(q /\ ~q) /\ ~(p /\ ~q)) /\ T /\ q) || (~(T /\ ~(p /\ ~q)) /\ ~r))
⇒ logic.propositional.truezeroand~r /\ ((~(~(q /\ ~q) /\ ~(p /\ ~q)) /\ q) || (~r /\ ~(T /\ ~(p /\ ~q)))) /\ ((~(~(q /\ ~q) /\ ~(p /\ ~q)) /\ T /\ q) || (~(T /\ ~(p /\ ~q)) /\ ~r))
⇒ logic.propositional.compland~r /\ ((~(~F /\ ~(p /\ ~q)) /\ q) || (~r /\ ~(T /\ ~(p /\ ~q)))) /\ ((~(~(q /\ ~q) /\ ~(p /\ ~q)) /\ T /\ q) || (~(T /\ ~(p /\ ~q)) /\ ~r))
⇒ logic.propositional.notfalse~r /\ ((~(T /\ ~(p /\ ~q)) /\ q) || (~r /\ ~(T /\ ~(p /\ ~q)))) /\ ((~(~(q /\ ~q) /\ ~(p /\ ~q)) /\ T /\ q) || (~(T /\ ~(p /\ ~q)) /\ ~r))
⇒ logic.propositional.truezeroand~r /\ ((~~(p /\ ~q) /\ q) || (~r /\ ~(T /\ ~(p /\ ~q)))) /\ ((~(~(q /\ ~q) /\ ~(p /\ ~q)) /\ T /\ q) || (~(T /\ ~(p /\ ~q)) /\ ~r))
⇒ logic.propositional.notnot~r /\ ((p /\ ~q /\ q) || (~r /\ ~(T /\ ~(p /\ ~q)))) /\ ((~(~(q /\ ~q) /\ ~(p /\ ~q)) /\ T /\ q) || (~(T /\ ~(p /\ ~q)) /\ ~r))
⇒ logic.propositional.compland~r /\ ((p /\ F) || (~r /\ ~(T /\ ~(p /\ ~q)))) /\ ((~(~(q /\ ~q) /\ ~(p /\ ~q)) /\ T /\ q) || (~(T /\ ~(p /\ ~q)) /\ ~r))
⇒ logic.propositional.falsezeroand~r /\ (F || (~r /\ ~(T /\ ~(p /\ ~q)))) /\ ((~(~(q /\ ~q) /\ ~(p /\ ~q)) /\ T /\ q) || (~(T /\ ~(p /\ ~q)) /\ ~r))
⇒ logic.propositional.falsezeroor~r /\ ~r /\ ~(T /\ ~(p /\ ~q)) /\ ((~(~(q /\ ~q) /\ ~(p /\ ~q)) /\ T /\ q) || (~(T /\ ~(p /\ ~q)) /\ ~r))
⇒ logic.propositional.idempand~r /\ ~(T /\ ~(p /\ ~q)) /\ ((~(~(q /\ ~q) /\ ~(p /\ ~q)) /\ T /\ q) || (~(T /\ ~(p /\ ~q)) /\ ~r))
⇒ logic.propositional.truezeroand~r /\ ~~(p /\ ~q) /\ ((~(~(q /\ ~q) /\ ~(p /\ ~q)) /\ T /\ q) || (~(T /\ ~(p /\ ~q)) /\ ~r))
⇒ logic.propositional.notnot~r /\ p /\ ~q /\ ((~(~(q /\ ~q) /\ ~(p /\ ~q)) /\ T /\ q) || (~(T /\ ~(p /\ ~q)) /\ ~r))
⇒ logic.propositional.truezeroand~r /\ p /\ ~q /\ ((~(~(q /\ ~q) /\ ~(p /\ ~q)) /\ q) || (~(T /\ ~(p /\ ~q)) /\ ~r))
⇒ logic.propositional.compland~r /\ p /\ ~q /\ ((~(~F /\ ~(p /\ ~q)) /\ q) || (~(T /\ ~(p /\ ~q)) /\ ~r))
⇒ logic.propositional.notfalse~r /\ p /\ ~q /\ ((~(T /\ ~(p /\ ~q)) /\ q) || (~(T /\ ~(p /\ ~q)) /\ ~r))
⇒ logic.propositional.truezeroand~r /\ p /\ ~q /\ ((~~(p /\ ~q) /\ q) || (~(T /\ ~(p /\ ~q)) /\ ~r))
⇒ logic.propositional.notnot~r /\ p /\ ~q /\ ((p /\ ~q /\ q) || (~(T /\ ~(p /\ ~q)) /\ ~r))
⇒ logic.propositional.compland~r /\ p /\ ~q /\ ((p /\ F) || (~(T /\ ~(p /\ ~q)) /\ ~r))
⇒ logic.propositional.falsezeroand~r /\ p /\ ~q /\ (F || (~(T /\ ~(p /\ ~q)) /\ ~r))
⇒ logic.propositional.falsezeroor~r /\ p /\ ~q /\ ~(T /\ ~(p /\ ~q)) /\ ~r
⇒ logic.propositional.truezeroand~r /\ p /\ ~q /\ ~~(p /\ ~q) /\ ~r
⇒ logic.propositional.notnot~r /\ p /\ ~q /\ p /\ ~q /\ ~r
⇒ logic.propositional.idempand~r /\ p /\ ~q /\ ~r