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