Exercise logic.propositional.dnf
Description
Proposition to DNF
Derivation
(((~~~(~q /\ ~~~p /\ ~q /\ ~~~p) /\ r) || (~(~q /\ ~~~p /\ ~q /\ ~~~p) /\ ~~q)) /\ ((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) || (~(~q /\ ~~~p) /\ ~~q)) /\ ((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) || (~(~q /\ ~~~p) /\ ~~q)) /\ (T || (~(~q /\ ~~~p /\ ~q /\ ~~~p) /\ ~~q))) || (~(~q /\ ~~~p /\ ~q /\ ~~~p) /\ ~~~~p /\ ~(~q /\ ~~~p /\ ~q /\ ~~~p) /\ ~~~~p)
⇒ logic.propositional.idempand(((~~~(~q /\ ~~~p /\ ~q /\ ~~~p) /\ r) || (~(~q /\ ~~~p) /\ ~~q)) /\ (T || (~(~q /\ ~~~p /\ ~q /\ ~~~p) /\ ~~q))) || (~(~q /\ ~~~p /\ ~q /\ ~~~p) /\ ~~~~p)
⇒ logic.propositional.idempand(((~~~(~q /\ ~~~p /\ ~q /\ ~~~p) /\ r) || (~(~q /\ ~~~p) /\ ~~q)) /\ (T || (~(~q /\ ~~~p /\ ~q /\ ~~~p) /\ ~~q))) || (~(~q /\ ~~~p) /\ ~~~~p)
⇒ logic.propositional.notnot(((~(~q /\ ~~~p /\ ~q /\ ~~~p) /\ r) || (~(~q /\ ~~~p) /\ ~~q)) /\ (T || (~(~q /\ ~~~p /\ ~q /\ ~~~p) /\ ~~q))) || (~(~q /\ ~~~p) /\ ~~~~p)
⇒ logic.propositional.idempand(((~(~q /\ ~~~p) /\ r) || (~(~q /\ ~~~p) /\ ~~q)) /\ (T || (~(~q /\ ~~~p /\ ~q /\ ~~~p) /\ ~~q))) || (~(~q /\ ~~~p) /\ ~~~~p)
⇒ logic.propositional.notnot(((~(~q /\ ~p) /\ r) || (~(~q /\ ~~~p) /\ ~~q)) /\ (T || (~(~q /\ ~~~p /\ ~q /\ ~~~p) /\ ~~q))) || (~(~q /\ ~~~p) /\ ~~~~p)
⇒ logic.propositional.notnot(((~(~q /\ ~p) /\ r) || (~(~q /\ ~p) /\ ~~q)) /\ (T || (~(~q /\ ~~~p /\ ~q /\ ~~~p) /\ ~~q))) || (~(~q /\ ~~~p) /\ ~~~~p)
⇒ logic.propositional.notnot(((~(~q /\ ~p) /\ r) || (~(~q /\ ~p) /\ q)) /\ (T || (~(~q /\ ~~~p /\ ~q /\ ~~~p) /\ ~~q))) || (~(~q /\ ~~~p) /\ ~~~~p)
⇒ logic.propositional.notnot(((~(~q /\ ~p) /\ r) || (~(~q /\ ~p) /\ q)) /\ (T || (~(~q /\ ~~~p /\ ~q /\ ~~~p) /\ ~~q))) || (~(~q /\ ~p) /\ ~~~~p)
⇒ logic.propositional.notnot(((~(~q /\ ~p) /\ r) || (~(~q /\ ~p) /\ q)) /\ (T || (~(~q /\ ~~~p /\ ~q /\ ~~~p) /\ ~~q))) || (~(~q /\ ~p) /\ ~~p)
⇒ logic.propositional.notnot(((~(~q /\ ~p) /\ r) || (~(~q /\ ~p) /\ q)) /\ (T || (~(~q /\ ~~~p /\ ~q /\ ~~~p) /\ ~~q))) || (~(~q /\ ~p) /\ p)
⇒ logic.propositional.demorganand(((~(~q /\ ~p) /\ r) || (~(~q /\ ~p) /\ q)) /\ (T || (~(~q /\ ~~~p /\ ~q /\ ~~~p) /\ ~~q))) || ((~~q || ~~p) /\ p)
⇒ logic.propositional.notnot(((~(~q /\ ~p) /\ r) || (~(~q /\ ~p) /\ q)) /\ (T || (~(~q /\ ~~~p /\ ~q /\ ~~~p) /\ ~~q))) || ((q || ~~p) /\ p)
⇒ logic.propositional.notnot(((~(~q /\ ~p) /\ r) || (~(~q /\ ~p) /\ q)) /\ (T || (~(~q /\ ~~~p /\ ~q /\ ~~~p) /\ ~~q))) || ((q || p) /\ p)
⇒ logic.propositional.absorpand(((~(~q /\ ~p) /\ r) || (~(~q /\ ~p) /\ q)) /\ (T || (~(~q /\ ~~~p /\ ~q /\ ~~~p) /\ ~~q))) || p
⇒ logic.propositional.truezeroor(((~(~q /\ ~p) /\ r) || (~(~q /\ ~p) /\ q)) /\ T) || p
⇒ logic.propositional.truezeroand(~(~q /\ ~p) /\ r) || (~(~q /\ ~p) /\ q) || p
⇒ logic.propositional.demorganand((~~q || ~~p) /\ r) || (~(~q /\ ~p) /\ q) || p
⇒ logic.propositional.demorganand((~~q || ~~p) /\ r) || ((~~q || ~~p) /\ q) || p
⇒ logic.propositional.notnot((q || ~~p) /\ r) || ((~~q || ~~p) /\ q) || p
⇒ logic.propositional.notnot((q || p) /\ r) || ((~~q || ~~p) /\ q) || p
⇒ logic.propositional.andoveror(q /\ r) || (p /\ r) || ((~~q || ~~p) /\ q) || p
⇒ logic.propositional.notnot(q /\ r) || (p /\ r) || ((q || ~~p) /\ q) || p
⇒ logic.propositional.absorpand(q /\ r) || (p /\ r) || q || p