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 /\ ~~~~p /\ ~(~q /\ ~~~p /\ ~q /\ ~~~p))
⇒ logic.propositional.idempand(~~~(~q /\ ~~~p /\ ~q /\ ~~~p) /\ r /\ T /\ T) || (~(~q /\ ~~~p /\ ~q /\ ~~~p) /\ ~~q) || (~(~q /\ ~~~p /\ ~q /\ ~~~p) /\ ~~~~p /\ ~(~q /\ ~~~p /\ ~q /\ ~~~p))
⇒ logic.propositional.idempand(~~~(~q /\ ~~~p /\ ~q /\ ~~~p) /\ r /\ T /\ T) || (~(~q /\ ~~~p /\ ~q /\ ~~~p) /\ ~~q) || (~(~q /\ ~~~p) /\ ~~~~p /\ ~(~q /\ ~~~p /\ ~q /\ ~~~p))
⇒ logic.propositional.idempand(~~~(~q /\ ~~~p /\ ~q /\ ~~~p) /\ r /\ T /\ T) || (~(~q /\ ~~~p /\ ~q /\ ~~~p) /\ ~~q) || (~(~q /\ ~~~p) /\ ~~~~p /\ ~(~q /\ ~~~p))
⇒ logic.propositional.notnot(~~~(~q /\ ~~~p /\ ~q /\ ~~~p) /\ r /\ T /\ T) || (~(~q /\ ~~~p /\ ~q /\ ~~~p) /\ ~~q) || (~(~q /\ ~p) /\ ~~~~p /\ ~(~q /\ ~~~p))
⇒ logic.propositional.notnot(~~~(~q /\ ~~~p /\ ~q /\ ~~~p) /\ r /\ T /\ T) || (~(~q /\ ~~~p /\ ~q /\ ~~~p) /\ ~~q) || (~(~q /\ ~p) /\ ~~p /\ ~(~q /\ ~~~p))
⇒ logic.propositional.notnot(~~~(~q /\ ~~~p /\ ~q /\ ~~~p) /\ r /\ T /\ T) || (~(~q /\ ~~~p /\ ~q /\ ~~~p) /\ ~~q) || (~(~q /\ ~p) /\ p /\ ~(~q /\ ~~~p))
⇒ logic.propositional.notnot(~~~(~q /\ ~~~p /\ ~q /\ ~~~p) /\ r /\ T /\ T) || (~(~q /\ ~~~p /\ ~q /\ ~~~p) /\ ~~q) || (~(~q /\ ~p) /\ p /\ ~(~q /\ ~p))
⇒ logic.propositional.demorganand(~~~(~q /\ ~~~p /\ ~q /\ ~~~p) /\ r /\ T /\ T) || (~(~q /\ ~~~p /\ ~q /\ ~~~p) /\ ~~q) || ((~~q || ~~p) /\ p /\ ~(~q /\ ~p))
⇒ logic.propositional.notnot(~~~(~q /\ ~~~p /\ ~q /\ ~~~p) /\ r /\ T /\ T) || (~(~q /\ ~~~p /\ ~q /\ ~~~p) /\ ~~q) || ((q || ~~p) /\ p /\ ~(~q /\ ~p))
⇒ logic.propositional.notnot(~~~(~q /\ ~~~p /\ ~q /\ ~~~p) /\ r /\ T /\ T) || (~(~q /\ ~~~p /\ ~q /\ ~~~p) /\ ~~q) || ((q || p) /\ p /\ ~(~q /\ ~p))
⇒ logic.propositional.absorpand(~~~(~q /\ ~~~p /\ ~q /\ ~~~p) /\ r /\ T /\ T) || (~(~q /\ ~~~p /\ ~q /\ ~~~p) /\ ~~q) || (p /\ ~(~q /\ ~p))
⇒ logic.propositional.demorganand(~~~(~q /\ ~~~p /\ ~q /\ ~~~p) /\ r /\ T /\ T) || (~(~q /\ ~~~p /\ ~q /\ ~~~p) /\ ~~q) || (p /\ (~~q || ~~p))
⇒ logic.propositional.notnot(~~~(~q /\ ~~~p /\ ~q /\ ~~~p) /\ r /\ T /\ T) || (~(~q /\ ~~~p /\ ~q /\ ~~~p) /\ ~~q) || (p /\ (q || ~~p))
⇒ logic.propositional.notnot(~~~(~q /\ ~~~p /\ ~q /\ ~~~p) /\ r /\ T /\ T) || (~(~q /\ ~~~p /\ ~q /\ ~~~p) /\ ~~q) || (p /\ (q || p))
⇒ logic.propositional.absorpand(~~~(~q /\ ~~~p /\ ~q /\ ~~~p) /\ r /\ T /\ T) || (~(~q /\ ~~~p /\ ~q /\ ~~~p) /\ ~~q) || p