In section 1 we present the basic ideas from Nuprl needed for this article. Surprisingly little is required, and we claim that this basic material is mostly as ``readable'' as the mathematical preliminaries in any undergraduate textbook at the level of Hopcroft and Ullman. Section 3 corresponds to Hopcroft and Ullman's Chapter 1. We try to follow that account closely. Section 4 provides the preliminaries on automata, following Hopcroft and Ullman very closely. Section 5 proves the Myhill/Nerode Theorem. Section 6 discusses proofs of state minimization, filling in an omission in their proof, and simplifying, thereby showing an advantage of formalization.
The key ideas of the formalization are presented here in a self-contained way, but the reader will understand the issues more thoroughly by reading either the Web library (www.cs.cornell.edu/Info/Pro-jects/NuPrl/nuprl.html) or using the Nuprl system to read the actual libraries. Indeed, the article was originally written as an html document to accompany the actual on-line theorems. Various references are made to Nuprl libraries in the text. In the html version these were hot references (one could click on them to open the referenced files).