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