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