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