Maybe finish with CNF section.
Add Brian as an author.
Space <<= slightly more generously.
Correct error in CNF section (bases must be > 1, not just non-zero).
Write up the fixpoints_exist theorem.