Exercise logic.propositional.dnf
Description
Proposition to DNF
Derivation
(~T /\ r) || ~(~~~F /\ ~(q /\ T) /\ T /\ ~~T /\ T /\ ~~~p /\ ~(q /\ T) /\ ~~~F /\ T)
⇒ logic.propositional.nottrue(F /\ r) || ~(~~~F /\ ~(q /\ T) /\ T /\ ~~T /\ T /\ ~~~p /\ ~(q /\ T) /\ ~~~F /\ T)
⇒ logic.propositional.falsezeroandF || ~(~~~F /\ ~(q /\ T) /\ T /\ ~~T /\ T /\ ~~~p /\ ~(q /\ T) /\ ~~~F /\ T)
⇒ logic.propositional.falsezeroor~(~~~F /\ ~(q /\ T) /\ T /\ ~~T /\ T /\ ~~~p /\ ~(q /\ T) /\ ~~~F /\ T)
⇒ logic.propositional.truezeroand~(~~~F /\ ~(q /\ T) /\ ~~T /\ T /\ ~~~p /\ ~(q /\ T) /\ ~~~F /\ T)
⇒ logic.propositional.truezeroand~(~~~F /\ ~(q /\ T) /\ ~~T /\ ~~~p /\ ~(q /\ T) /\ ~~~F /\ T)
⇒ logic.propositional.truezeroand~(~~~F /\ ~(q /\ T) /\ ~~T /\ ~~~p /\ ~(q /\ T) /\ ~~~F)
⇒ logic.propositional.notnot~(~F /\ ~(q /\ T) /\ ~~T /\ ~~~p /\ ~(q /\ T) /\ ~~~F)
⇒ logic.propositional.notfalse~(T /\ ~(q /\ T) /\ ~~T /\ ~~~p /\ ~(q /\ T) /\ ~~~F)
⇒ logic.propositional.truezeroand~(~(q /\ T) /\ ~~T /\ ~~~p /\ ~(q /\ T) /\ ~~~F)
⇒ logic.propositional.notnot~(~(q /\ T) /\ T /\ ~~~p /\ ~(q /\ T) /\ ~~~F)
⇒ logic.propositional.truezeroand~(~(q /\ T) /\ ~~~p /\ ~(q /\ T) /\ ~~~F)
⇒ logic.propositional.notnot~(~(q /\ T) /\ ~p /\ ~(q /\ T) /\ ~~~F)
⇒ logic.propositional.notnot~(~(q /\ T) /\ ~p /\ ~(q /\ T) /\ ~F)
⇒ logic.propositional.notfalse~(~(q /\ T) /\ ~p /\ ~(q /\ T) /\ T)
⇒ logic.propositional.truezeroand~(~(q /\ T) /\ ~p /\ ~(q /\ T))
⇒ logic.propositional.truezeroand~(~q /\ ~p /\ ~(q /\ T))
⇒ logic.propositional.truezeroand~(~q /\ ~p /\ ~q)
⇒ logic.propositional.gendemorganand~~q || ~~p || ~~q
⇒ logic.propositional.notnotq || ~~p || ~~q
⇒ logic.propositional.notnotq || p || ~~q
⇒ logic.propositional.notnotq || p || q