Exercise logic.propositional.dnf
Description
Proposition to DNF
Derivation
(~~~(~q /\ ~~~p /\ ~q /\ ~~~p) /\ r /\ T /\ T) || (~(~q /\ ~~~p /\ ~q /\ ~~~p) /\ (~~q || (~~~~p /\ ~(~q /\ ~~~p /\ ~q /\ ~~~p) /\ ~~~~p)))
⇒ logic.propositional.idempand(~~~(~q /\ ~~~p /\ ~q /\ ~~~p) /\ r /\ T) || (~(~q /\ ~~~p /\ ~q /\ ~~~p) /\ (~~q || (~~~~p /\ ~(~q /\ ~~~p /\ ~q /\ ~~~p) /\ ~~~~p)))
⇒ logic.propositional.idempand(~~~(~q /\ ~~~p /\ ~q /\ ~~~p) /\ r /\ T) || (~(~q /\ ~~~p) /\ (~~q || (~~~~p /\ ~(~q /\ ~~~p /\ ~q /\ ~~~p) /\ ~~~~p)))
⇒ logic.propositional.idempand(~~~(~q /\ ~~~p /\ ~q /\ ~~~p) /\ r /\ T) || (~(~q /\ ~~~p) /\ (~~q || (~~~~p /\ ~(~q /\ ~~~p) /\ ~~~~p)))
⇒ logic.propositional.notnot(~~~(~q /\ ~~~p /\ ~q /\ ~~~p) /\ r /\ T) || (~(~q /\ ~p) /\ (~~q || (~~~~p /\ ~(~q /\ ~~~p) /\ ~~~~p)))
⇒ logic.propositional.notnot(~~~(~q /\ ~~~p /\ ~q /\ ~~~p) /\ r /\ T) || (~(~q /\ ~p) /\ (q || (~~~~p /\ ~(~q /\ ~~~p) /\ ~~~~p)))
⇒ logic.propositional.notnot(~~~(~q /\ ~~~p /\ ~q /\ ~~~p) /\ r /\ T) || (~(~q /\ ~p) /\ (q || (~~p /\ ~(~q /\ ~~~p) /\ ~~~~p)))
⇒ logic.propositional.notnot(~~~(~q /\ ~~~p /\ ~q /\ ~~~p) /\ r /\ T) || (~(~q /\ ~p) /\ (q || (p /\ ~(~q /\ ~~~p) /\ ~~~~p)))
⇒ logic.propositional.notnot(~~~(~q /\ ~~~p /\ ~q /\ ~~~p) /\ r /\ T) || (~(~q /\ ~p) /\ (q || (p /\ ~(~q /\ ~p) /\ ~~~~p)))
⇒ logic.propositional.notnot(~~~(~q /\ ~~~p /\ ~q /\ ~~~p) /\ r /\ T) || (~(~q /\ ~p) /\ (q || (p /\ ~(~q /\ ~p) /\ ~~p)))
⇒ logic.propositional.notnot(~~~(~q /\ ~~~p /\ ~q /\ ~~~p) /\ r /\ T) || (~(~q /\ ~p) /\ (q || (p /\ ~(~q /\ ~p) /\ p)))
⇒ logic.propositional.demorganand(~~~(~q /\ ~~~p /\ ~q /\ ~~~p) /\ r /\ T) || ((~~q || ~~p) /\ (q || (p /\ ~(~q /\ ~p) /\ p)))
⇒ logic.propositional.notnot(~~~(~q /\ ~~~p /\ ~q /\ ~~~p) /\ r /\ T) || ((q || ~~p) /\ (q || (p /\ ~(~q /\ ~p) /\ p)))
⇒ logic.propositional.notnot(~~~(~q /\ ~~~p /\ ~q /\ ~~~p) /\ r /\ T) || ((q || p) /\ (q || (p /\ ~(~q /\ ~p) /\ p)))
⇒ logic.propositional.demorganand(~~~(~q /\ ~~~p /\ ~q /\ ~~~p) /\ r /\ T) || ((q || p) /\ (q || (p /\ (~~q || ~~p) /\ p)))
⇒ logic.propositional.notnot(~~~(~q /\ ~~~p /\ ~q /\ ~~~p) /\ r /\ T) || ((q || p) /\ (q || (p /\ (q || ~~p) /\ p)))
⇒ logic.propositional.notnot(~~~(~q /\ ~~~p /\ ~q /\ ~~~p) /\ r /\ T) || ((q || p) /\ (q || (p /\ (q || p) /\ p)))
⇒ logic.propositional.absorpand(~~~(~q /\ ~~~p /\ ~q /\ ~~~p) /\ r /\ T) || ((q || p) /\ (q || (p /\ p)))
⇒ logic.propositional.idempand(~~~(~q /\ ~~~p /\ ~q /\ ~~~p) /\ r /\ T) || ((q || p) /\ (q || p))
⇒ logic.propositional.idempand(~~~(~q /\ ~~~p /\ ~q /\ ~~~p) /\ r /\ T) || q || p
⇒ logic.propositional.truezeroand(~~~(~q /\ ~~~p /\ ~q /\ ~~~p) /\ r) || q || p
⇒ logic.propositional.notnot(~(~q /\ ~~~p /\ ~q /\ ~~~p) /\ r) || q || p
⇒ logic.propositional.idempand(~(~q /\ ~~~p) /\ r) || q || p
⇒ logic.propositional.notnot(~(~q /\ ~p) /\ r) || q || p
⇒ logic.propositional.demorganand((~~q || ~~p) /\ r) || q || p
⇒ logic.propositional.notnot((q || ~~p) /\ r) || q || p
⇒ logic.propositional.notnot((q || p) /\ r) || q || p
⇒ logic.propositional.absorporq || p