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