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