A Formalization of the Exponential Blowup in the Transformations between CNF and DNF by Leon Raffael Schulz, Martin Desharnais-Schäfer and Jan Johannsen Jun 15