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