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