# Preface to the Hypertext Edition

This edition is intended primarily as an on-line user's manual for the associated ACL2 library of register-transfer logic and computer arithmetic, which is publicly available as a part of the standard ACL2 release through the University of Texas Web site, at

Specifically, it may be found in the /books/rtl subdirectory of the ACL2 sources.

This document was generated using the LaTeX2HTML translator in order to facilitate its navigation with a Web browser. One feature provided by LaTeX2HTML is a hypertext link associated with every reference to a definition, lemma, or other labeled location in the text, thereby providing for its immediate retrieval. For example, this link to Lemma 11.2.1 of Chapter 11 may be followed with a click of the mouse, after which the browser's back button may be used to return the user to this preface.

Furthermore, for the purpose of this document, the HTML translation has been extended with a second pass, consisting of several Perl scripts that generate Javascript code and embed it in the HTML. This code implements a number of navigation features that are not provided by LaTeX2HTML. The most important of these is a facility for connecting the results appearing in this exposition with corresponding events in the ACL2 code. Each chapter of this document corresponds to a book, i.e., a file of events, in the ACL2 library, and each definition or lemma that is listed here relates to one or more ACL2 events. In most cases, this correspondence is one-one and the order of events in a book is preserved in the corresponding chapter.

Every definition or result is labeled with the name of the corresponding ACL2 event, as illustrated below.

(flt-4) There exist no positive integers , , and such that

PROOF: This result is easily established by the method of infinite descent.

Definition 0.0.1   (primep) A prime is an integer greater than 1 that has no proper divisors.

(flt-prime) If p is an odd prime, then there exist no positive integers , , and such that

PROOF: I have discovered a truly marvelous proof to this, which this page is too small to contain.

(flt) If is an integer greater than 2, then there exist no positive integers , , and such that

PROOF: Suppose we have a counterexample, , where . Then either is a power of 2, in which case it is divisible by 4, or is divisible by an odd prime . In the first case, we may write and hence,

contradicting Lemma 0.0.1. Similarly, in the second case, and

Note that these event names are mouse-sensitive. When the user clicks on an event name in this window, the event appears in a second window, which is automatically created for the purpose of displaying ACL2 code. Similarly, clicking on the name of an event in the code window causes the informal version to appear in this window.

The events of interest are of two classes: defun and defthm. Definitions in the text usually correspond to defun events (although there are exceptions, e.g., Definition 1.1.1), and all derived results correspond to defthm events. Most results are labelled as lemmas, but several are classified instead as theorems for the sake of emphasis, and some as corollaries to suggest their dependence on preceding results. This classification is somewhat arbitrary has no significance from the formal (ACL2) perspective.

It is an important aspect of the theory that it has been completely formalized in the ACL2 logic. Consequently, every result appearing in the text is represented in the ACL2 code. In general, the formalization is straightforward, as illustrated by the foregoing example, with the caveat discussed in the preface: a hypothesis in the text version of a lemma stipulating that a variable is real-valued is replaced in the formalization by (rationalp x). In some cases, on the other hand, the user will notice that the hypotheses of ACL2 events are weaker than the informal versions: a hypothesis that is an integer might also be replaced by (rationalp x), or even omitted altogether. Thus, the statement that was proved mechanically is actually stronger than that which is claimed in the text. When this occurs, it may be assumed that the text version captures the cases of interest, while the weakening of hypotheses in the formal version may serve to speed up the application of the lemma by simplifying the task of the rewriter.

Moreover, the correspondence between informal results and defthm events is not quite bijective. Some events that are included for technical reasons are not sufficiently interesting from the reader's perspective to be represented in the text, although the ACL2 user is encouraged to examine the event files more closely. In other cases, for the sake of readability, several ACL2 events are combined into a single lemma. When this occurs, the events are grouped together in the ACL2 file and the text lemma is linked to the first event in the group.

Another Javascript enhancement to the HTML translation is a facility for enabling and disabling the display of proofs. It is anticipated that some users may be interested in reading and applying the results contained in this exposition without being encumbered by their proofs. Therefore, no proofs are displayed when a section is first read into the browser window. In order to exhibit the proof of a result, the reader may click on its name, e.g., Corollary 0.0.2 above. The display of a proof may then be disabled by clicking on the red box () appearing at its end.

This effort is my first experience with each of three languages--LaTeX2HTML, Perl, and Javascript--all of which continue to hold considerable mystery for me. After a lot of trial and error, it all seems to work well enough with the Web browsers that I've tried, but I suspect that others may yield different results. Please report any problems to david@russinoff.com.

D.M.R.
Block Island, Rhode Island
November, 2005

David Russinoff 2017-08-01