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