DNF Rewrite Rules

To obtain DNF, we can preform a series of transformations:

$$\begin{array}{rl}F\to G& \Rightarrow \neg F\vee G\\ F⟺G& \Rightarrow (F\to G)\vee (G\to F)\\ \neg (F\vee G)& \Rightarrow \neg F\wedge \neg G\\ \neg (F\wedge G)& \Rightarrow \neg F\vee \neg G\\ \neg \neg F& \Rightarrow F\\ F\wedge (G\vee H)& \Rightarrow (F\wedge G)\vee (F\wedge H)\\ (F\vee G)\wedge H& \Rightarrow (F\wedge H)\vee (G\wedge H)\end{array}$$