PRINT-DOC-START-COLUMN

printing the one-liner
```Major Section:  MISCELLANEOUS
```

```Examples:
(assign print-doc-start-column nil)
(assign print-doc-start-column 17)
```

This state global variable controls the column in which the ``one-liner'' of a formatted documentation string is printed. Generally, when `:``doc` is used to print a documentation string, the name of the documented concept is printed and then `:``doc` tabs over to `print-doc-start-column` and prints the one-liner. If the name extends past the desired column, `:``doc` outputs a carriage return and then tabs over to the column. If `print-doc-start-column` is `nil`, `:``doc` just starts the one-liner two spaces from the end of the name, on the same line. The initial value of `print-doc-start-column` is 15.

PROMPT

the prompt printed by `ld`
```Major Section:  MISCELLANEOUS
```

The prompt printed by ACL2 conveys information about various ``modes.'' See default-print-prompt and see ld-prompt for details.

PROOF-OF-WELL-FOUNDEDNESS

a proof that `e0-ord-<` is well-founded on `e0-ordinalp`s
```Major Section:  MISCELLANEOUS
```

The soundness of ACL2 rests in part on the well-foundedness of `e0-ord-<` on `e0-ordinalp`s. This can be taken as obvious if one is willing to grant that those concepts are simply encodings of the standard mathematical notions of the ordinals below `epsilon-0` and its natural ordering relation. But it is possible to prove that `e0-ord-<` is well-founded on `e0-ordinalp`s without having to assert any connection to the ordinals and that is what we do here.

We first observe three facts about `e0-ord-<` on ordinals that have been proved by ACL2 using only structural induction on lists.

```(defthm transitivity
(implies (and (e0-ordinalp x)
(e0-ordinalp y)
(e0-ordinalp z)
(e0-ord-< x y)
(e0-ord-< y z))
(e0-ord-< x z))
:rule-classes nil)

(defthm non-circularity
(implies (and (e0-ordinalp x)
(e0-ordinalp y)
(e0-ord-< x y))
(not (e0-ord-< y x)))
:rule-classes nil)

(defthm trichotomy
(implies (and (e0-ordinalp x)
(e0-ordinalp y))
(or (equal x y)
(e0-ord-< x y)
(e0-ord-< y x)))
:rule-classes nil)
```
These three properties establish that `e0-ord-<` orders the `e0-ordinalp`s. To put such a statement in the most standard mathematical nomenclature, we can define the function:
```(defun e0-ord-<= (x y)
(or (equal x y) (e0-ord-< x y)))
```
and then establish that `e0-ord-<=` is a relation that is a simple, complete (i.e., total) order on ordinals by the following three lemmas, which have been proved:
```(defthm antisymmetry
(implies (and (e0-ordinalp x)
(e0-ordinalp y)
(e0-ord-<= x y)
(e0-ord-<= y x))
(equal x y))
:rule-classes nil
:hints (("Goal" :use non-circularity)))

(defthm e0-ord-<=-transitivity
(implies (and (e0-ordinalp x)
(e0-ordinalp y)
(e0-ordinalp z)
(e0-ord-<= x y)
(e0-ord-<= y z))
(e0-ord-<= x z))
:rule-classes nil
:hints (("Goal" :use transitivity)))

(defthm trichotomy-of-e0-ord-<
(implies (and (e0-ordinalp x)
(e0-ordinalp y))
(or (e0-ord-<= x y)
(e0-ord-<= y x)))
:rule-classes nil
:hints (("Goal" :use trichotomy)))
```
Crucially important to the proof of the well-foundedness of `e0-ord-<` on `e0-ordinalp`s is the concept of ordinal-depth, abbreviated `od`:
```(defun od (l) (if (atom l) 0 (1+ (od (car l)))))
```
If the `od` of an `e0-ordinalp` `x` is smaller than that of an `e0-ordinalp` `y`, then `x` is `e0-ord-<` `y`:
```(defthm od-implies-ordlessp
(implies (and (e0-ordinalp x) (e0-ordinalp y)
(< (od x) (od y)))
(e0-ord-< x y)))
```
Remark. A consequence of this lemma is the fact that if `s = s(1)`, `s(2)`, ... is an infinite, `e0-ord-<` descending sequence, then `od(s(1))`, `od(s(2))`, ... is a ``weakly'' descending sequence of non-negative integers: `od(s(i))` is greater than or equal to `od(s(i+1))`.

Lemma Main. For each non-negative integer `n`, `e0-ord-<` well-orders the set of `e0-ordinalp`s with `od` less than or equal to `n` .

``` Base Case.  n = 0.  The e0-ordinalps with 0 od are the non-negative
integers.  On the non-negative integers, e0-ord-< is the same as <.

Induction Step.  n > 0.  We assume that e0-ord-< well-orders the
e0-ordinalps with od less than n.

If e0-ord-< does not well-order the e0-ordinalps with od less
than or equal to n, we may let O be the e0-ord-<-least
e0-ordinalp which is the car of the first member of an infinite,
e0-ord-< descending sequence of e0-ordinalps of od less than or
equal to n.  The od of O is n-1.

Let k be the least integer > 0 such that for some infinite,
e0-ord-< descending sequence s of e0-ordinalps with od less than
or equal to n, the first element of s begins with k occurrences
of O but not k+1 occurrences of O.

Having fixed O and k, let s = s(1), s(2), ... be an infinite,
e0-ord-< descending sequence of e0-ordinalps with od less than
or equal to n such that O occurs exactly k times at the
beginning of s(1).

O occurs exactly k times at the beginning of each s(i).
For suppose that s(j) is the first member of s with exactly
m occurrences of O at the beginning, m /= k.  If m = 0,
then the first member of s(j) must be e0-ord-< O,
contradicting the minimality of O.  If 0 < m < k, then the
fact that the sequence beginning at s(j) is infinitely
descending contradicts the minimality of k.  If m > k, then
s(j) is greater than its predecessor, which has only k
occurrences of O at the beginning; but this contradicts the
fact that s is descending.

Let t = t(1), t(2), ... be the sequence of e0-ordinalps
that is obtained by letting t(i) be the result of removing
O from the front of s(i) exactly k times.  t is infinitely
descending.  Furthermore, t(1) begins with an e0-ordinalp
O' that is e0-ord-< O, and hence has od at most N-1 by the
lemma od-implies-ordlessp.  But this contradicts the
minimality of O. Q.E.D.
```
Theorem. `e0-ord-<` well-orders the `e0-ordinalp`s. Proof. Every infinite,` e0-ord-<` descending sequence of `e0-ordinalp`s has the property that each member has `od` less than or equal to the `od`, `n`, of the first member of the sequence. This contradicts Lemma Main. Q.E.D.

PSEUDO-TERMP

a predicate for recognizing term-like s-expressions
```Major Section:  MISCELLANEOUS
```

```Example Forms:
(pseudo-termp '(car (cons x 'nil)))      ; has value t
(pseudo-termp '(car x y z))              ; also has value t!
(pseudo-termp '(delta (h x)))            ; has value t
(pseudo-termp '(delta (h x) . 7))        ; has value nil (not a true-listp)
(pseudo-termp '((lambda (x) (car x)) b)) ; has value t
(pseudo-termp '(if x y 123))             ; has value nil (123 is not quoted)
(pseudo-termp '(if x y '123))            ; has value t
```
If `x` is the quotation of a term, then `(pseudo-termp x)` is `t`. However, if `x` is not the quotation of a term it is not necessarily the case that `(pseudo-termp x)` is `nil`.

See term for a discussion of the various meanings of the word ``term'' in ACL2. In its most strict sense, a term is either a legal variable symbol, a quoted constant, or the application of an `n`-ary function symbol or closed `lambda`-expression to `n` terms. By ``legal variable symbol'' we exclude constant symbols, such as `t`, `nil`, and `*ts-rational*`. By ``quoted constants'' we include `'t` (aka `(quote t)`), `'nil`, `'31`, etc., and exclude constant names such as `t`, `nil` and `*ts-rational*`, unquoted constants such as `31` or `1/2`, and ill-formed `quote` expressions such as `(quote 3 4)`. By ``closed lambda expression'' we exclude expressions, such as `(lambda (x) (cons x y))`, containing free variables in their bodies. Terms typed by the user are translated into strict terms for internal use in ACL2.

The predicate `termp` checks this strict sense of ``term'' with respect to a given ACL2 logical world; See world. Many ACL2 functions, such as the rewriter, require certain of their arguments to satisfy `termp`. However, as of this writing, `termp` is in `:``program` mode and thus cannot be used effectively in conjectures to be proved. Furthermore, if regarded simply from the perspective of an effective guard for a term-processing function, `termp` checks many irrelevant things. (Does it really matter that the variable symbols encountered never start and end with an asterisk?) For these reasons, we have introduced the notion of a ``pseudo-term'' and embodied it in the predicate `pseudo-termp`, which is easier to check, does not require the logical world as input, has `:``logic` mode, and is often perfectly suitable as a guard on term-processing functions.

A `pseudo-termp` is either a symbol, a true list of length 2 beginning with the word `quote`, the application of an `n`-ary pseudo-`lambda` expression to a true list of `n` pseudo-terms, or the application of a symbol to a true list of `n` `pseudo-termp`s. By an ```n`-ary pseudo-`lambda` expression'' we mean an expression of the form `(lambda (v1 ... vn) pterm)`, where the `vi` are symbols (but not necessarily distinct legal variable symbols) and `pterm` is a `pseudo-termp`.

Metafunctions may use `pseudo-termp` as a guard.

REDEF

a common way to set ld-redefinition-action
```Major Section:  MISCELLANEOUS
```

```Example and General Form:
ACL2 !>:redef
```
This command sets `ld-redefinition-action` to `'(:query . :overwrite)`.

As explained elsewhere (see ld-redefinition-action), this allows redefinition of functions and other events without undoing. A query will be made every time a redefinition is commanded; the user must explicitly acknowledge that the redefinition is intentional. It is possible to set `ld-redefinition-action` so that the redefinition of non-system functions occurs quietly. See ld-redefinition-action.

REDEF!

system hacker's redefinition command
```Major Section:  MISCELLANEOUS
```

```Example and General Form:
ACL2 !>:redef!
ACL2 p!>
```
This command sets `ld-redefinition-action` to `'(:warn! . :overwrite)` and sets the default defun-mode to `:``program`.

This is the ACL2 system hacker's redefinition command. Note that even system functions can be redefined with a mere warning. Be careful!

REDEFINED-NAMES

to collect the names that have been redefined
```Major Section:  MISCELLANEOUS
```

```Example and General Forms:
(redefined-names state)
```

This function collects names that have been redefined in the current ACL2 state. `:``Program` mode functions that were reclassified to `:``logic` functions are not collected, since such reclassification cannot imperil soundness because it is allowed only when the new and old definitions are identical.

Thus, if `(redefined-names state)` returns `nil` then no unsafe definitions have been made, regardless of `ld-redefinition-action`. See ld-redefinition-action.

REDUNDANT-EVENTS

allowing a name to be introduced ``twice''
```Major Section:  MISCELLANEOUS
```

Sometimes an event will announce that it is ``redundant''. When this happens, no change to the logical world has occurred. This happens when the logical name being defined is already defined and has exactly the same definition, from the logical point of view. This feature permits two independent books, each of which defines some name, to be included sequentially provided they use exactly the same definition.

When are two logical-name definitions considered exactly the same? It depends upon the kind of name being defined.

A `deflabel` event is never redundant. This means that if you have a `deflabel` in a book and that book has been included (without error), then references to that label denote the point in history at which the book introduced the label. See the note about shifting logical names, below.

A `defun` or `mutual-recursion` (or `defuns`) event is redundant if for each function to be introduced, there has already been introduced a function with the same name, the same formals, and syntactically identical `guard`, type declarations, and `body` (before macroexpansion).

A `verify-guards` event is redundant if the function has already had its guards verified.

A `defaxiom` or `defthm` event is redundant if there is already an axiom or theorem of the given name and both the formula (after macroexpansion) and the rule-classes are syntactically identical. Note that a `defaxiom` can make a subsequent `defthm` redundant, and a `defthm` can make a subsequent `defaxiom` redundant as well.

A `defconst` is redundant if the name has been defined to have the same value.

A `defmacro` is redundant if there is already a macro defined with the same name and syntactically identical arguments, guard, and body.

A `defpkg` is redundant if a package of the same name with exactly the same imports has been defined.

A `deftheory` is never redundant. The ``natural'' notion of equivalent `deftheory`s is that the names and values of the two theory expressions are the same. But since most theory expressions are sensitive to the context in which they occur, it seems unlikely to us that two `deftheory`s coming from two sequentially included books will ever have the same values. So we prohibit redundant theory definitions. If you try to define the same theory name twice, you will get a ``name in use'' error.

An `in-theory` event is never redundant because it doesn't define any name.

`Table` and `defdoc` events are never redundant because they don't define any name.

An `encapsulate` event is redundant if and only if a syntactically identical `encapsulate` has already been executed under the same `default-defun-mode`.

An `include-book` is redundant if the book has already been included.

Note About Shifting Logical Names:

Suppose a book defines a function `fn` and later uses `fn` as a logical name in a theory expression. Consider the value of that theory expression in two different sessions. In session A, the book is included in a world in which `fn` is not already defined, i.e., in a world in which the book's definition of `fn` is not redundant. In session B, the book is included in a world in which `fn` is already identically defined. In session B, the book's definition of `fn` is redundant. When `fn` is used as a logical name in a theory expression, it denotes the point in history at which `fn` was introduced. Observe that those points are different in the two sessions. Hence, it is likely that theory expressions involving `fn` will have different values in session A than in session B.

This may adversely affect the user of your book. For example, suppose your book creates a theory via `deftheory` that is advertised just to contain the names generated by the book. But suppose you compute the theory as the very last event in the book using:

```(set-difference-theories (universal-theory :here)
(universal-theory fn))
```
where `fn` is the very first event in the book and happens to be a `defun` event. This expression returns the advertised set if `fn` is not already defined when the book is included. But if `fn` were previously (identically) defined, the theory is larger than advertised.

The moral of this is simple: when building books that other people will use, it is best to describe your theories in terms of logical names that will not shift around when the books are included. The best such names are those created by `deflabel`.

SAVING-AND-RESTORING

saving and restoring your logical state
```Major Section:  MISCELLANEOUS
```

```Examples:
ACL2 !>:Q
>(make-lib "file")
...
>(note-lib "file")
>(LP)
ACL2 !>
```

To save the current ACL2 logical world to a file, exit ACL2 with `:``q` and invoke `(make-lib "file")` in Common Lisp. This creates a file `"file.lib"` and a file `"file.lisp"`. The latter will be compiled. It generally takes half an hour to save an ACL2 logical world and creates a 20Mb file. All things considered it is probably better to just save your core image.

To restore such a saved ACL2 world, invoke `(note-lib "file")` from Common Lisp, and then enter ACL2 with `(lp)`. We do not save the `io` system, the stacks, or the global table, hence bindings of your globals will not be restored.

This save/restore mechanism is a temporary expedient. We know of faster mechanisms, mechanisms that consume less disk space, and mechanisms that provide more functionality. We don't know of good compromises between these various desirable features.

SIGNATURE

how to specify the arity of a constrained function
```Major Section:  MISCELLANEOUS
```

```Examples:
(hd (x) t)
(printer (x state) (mv t t state))
(printer (x state) (mv er-flg val state))

General Form:
(fn formals result)
```
where `fn` is the constrained function symbol, `formals` is a suitable list of formal parameters for it, and `result` is either a symbol denoting that the function returns one result (which is a state object or not depending on whether the symbol is `state`) or else result is an `mv` expression, `(mv s1 ... sn)`, where `n>1`, each `si` is a symbol, and at most one of the `si` is the symbol `state`. The latter form of result indicates that the function returns `n` results and indicates which of them (if any) is a state object. The non-`state` `si` are just place holders and may all be identical, e.g., `t`, though we often use symbols that suggest the type of the corresponding value. It is illegal for `state` to be used in result if `state` does not appear in `formals`.

SIMPLE

`:``definition` and `:``rewrite` rules used in preprocessing
```Major Section:  MISCELLANEOUS
```

```Example of simple rewrite rule:
(equal (car (cons x y)) x)

Examples of simple definition:
(defun file-clock-p (x) (integerp x))
(defun naturalp (x)
(and (integerp x) (>= x 0)))
```

The theorem prover output sometimes refers to ``simple'' definitions and rewrite rules. These rules can be used by the preprocessor, which is one of the theorem prover's ``processes'' understood by the `:do-not` hint; see hints.

The preprocessor expands certain definitions and uses certain rewrite rules that it considers to be ``fast''. There are two ways to qualify as fast. One is to be an ``abbreviation'', where a rewrite rule with no hypotheses or loop stopper is an ``abbreviation'' if the right side contains no more variable occurrences than the left side, and the right side does not call the functions `if`, `not` or `implies`. Definitions and rewrite rules can both be abbreviations; the criterion for definitions is similar, except that the definition must not be recursive. The other way to qualify applies only to a non-recursive definition, and applies when its body is a disjunction or conjunction, according to a perhaps subtle criterion that is intended to avoid case splits.

SPECIOUS-SIMPLIFICATION

nonproductive proof steps
```Major Section:  MISCELLANEOUS
```

Occasionally the ACL2 theorem prover reports that the current goal simplifies to itself or to a set including itself. Such simplifications are said to be ``specious'' and are ignored in the sense that the theorem prover acts as though no simplification were possible and tries the next available proof technique. Specious simplifications are almost always caused by forcing.

The simplification of a formula proceeds primarily by the local application of `:``rewrite`, `:``type-prescription`, and other rules to its various subterms. If no rewrite rules apply, the formula cannot be simplified and is passed to the next ACL2 proof technique, which is generally the elimination of destructors. The experienced ACL2 user pays special attention to such ``maximally simplified'' formulas; the presence of unexpected terms in them indicates the need for additional rules or the presence of some conflict that prevents existing rules from working harmoniously together.

However, consider the following interesting possibility: local rewrite rules apply but, when applied, reproduce the goal as one of its own subgoals. How can rewrite rules apply and reproduce the goal? Of course, one way is for one rule application to undo the effect of another, as when commutativity is applied twice in succession to the same term. Another kind of example is when rules conflict and undermine each other. For example, under suitable hypotheses, `(length x)` might be rewritten to `(+ 1 (length (cdr x)))` by the `:``definition` of `length` and then a `:``rewrite` rule might be used to ``fold'' that back to `(length x)`. Generally speaking the presence of such ``looping'' rewrite rules causes ACL2's simplifier either to stop gracefully because of heuristics such as that described in the documentation for `loop-stopper` or to cause a stack overflow because of indefinite recursion.

A more insidious kind of loop can be imagined: two rewrites in different parts of the formula undo each other's effects ``at a distance,'' that is, without ever being applied to one another's output. For example, perhaps the first hypothesis of the formula is simplified to the second, but then the second is simplified to the first, so that the end result is a formula propositionally equivalent to the original one but with the two hypotheses commuted. This is thought to be impossible unless forcing or case-splitting occurs, but if those features are exploited (see force and see case-split) it can be made to happen relatively easily.

Here is a simple example. Declare `foo` to be a function of one argument returning one result:

```(defstub foo (x) t)
```
Add the following `:``type-prescription` rule about `foo`:
```(defaxiom forcer
(implies (force (not (true-listp x)))
(equal (foo x) t))
:rule-classes :type-prescription)
```
Note that we could define a `foo` with this property; `defstub` and `defaxiom` are only used here to get to the gist of the problem immediately. Consider the proof attempt for the following formula.
```(thm (implies (and (consp x)              ; hyp 1
(true-listp (cdr x))   ; hyp 2
(true-listp x))        ; hyp 3
(foo x)))                   ; concl
```
When we simplify this goal, `hyp 1` cannot be simplified. `Hyp 2` simplifies to `t`, because `x` is known to be a non-`nil` true list so its `cdr` is a true list by type reasoning; because true hypotheses are dropped, `hyp 2` simply disappears. `Hyp 3` simplifies to `(true-listp (cdr x))` by opening up the `:``definition` of `true-listp`. Note that `hyp 3` has simplified to the old `hyp 2`. So at this point, the ``current (intermediate) goal'' is
```(implies (and (consp x)                   ; rewritten hyp 1
(true-listp (cdr x)))       ; rewritten hyp 3
(foo x))                         ; unrewritten concl
```
and we are working on `(foo x)`. But the `:``type-prescription` rule above tells us that `(foo x)` is `t` if the hypothesis of the rule is true. Thus, in the case that the hypothesis of the rule is true, we are done. It remains to prove the current intermediate goal under the assumption that the hypothesis of the rule is false. This is done by adding the negation of the `:``type-prescription` rule's hypothesis to the current intermediate goal. This is what `force` does in this situation. The negation of the hypothesis is `(true-listp x)`. Adding it to the current goal produces the subgoal
```(implies (and (consp x)                   ; rewritten hyp 1
(true-listp (cdr x))        ; rewritten hyp 3
(true-listp x))             ; FORCEd hyp
(foo x)).                        ; unrewritten concl
```
Observe that this is just our original goal. Despite all the rewriting, no progress was made! In more common cases, the original goal may simplify to a set of subgoals, one of which includes the original goal.

If ACL2 were to adopt the new set of subgoals, it would loop indefinitely. Therefore, it checks whether the input goal is a member of the output subgoals. If so, it announces that the simplification is ``specious'' and pretends that no simplification occurred.

``Maximally simplified'' formulas that produce specious simplifications are maximally simplified in a very technical sense: were ACL2 to apply every applicable rule to them, no progress would be made. Since ACL2 can only apply every applicable rule, it cannot make further progress with the formula. But the informed user can perhaps identify some rule that should not be applied and make it inapplicable by disabling it, allowing the simplifier to apply all the others and thus make progress.

When specious simplifications are a problem it might be helpful to disable all forcing (including case-splits) and resubmit the formula to observe whether forcing is involved in the loop or not. See force. The commands

```ACL2 !>:disable-forcing
and
ACL2 !>:enable-forcing
```
disable and enable the pragmatic effects of both `force` and `case-split`. If the loop is broken when forcing is disabled, then it is very likely some forced hypothesis of some rule is ``undoing'' a prior simplification. The most common cause of this is when we force a hypothesis that is actually false but whose falsity is somehow temporarily hidden (more below). To find the offending rule, compare the specious simplification with its non-specious counterpart and look for rules that were speciously applied that are not applied in the non-specious case. Most likely you will find at least one such rule and it will have a `force`d hypothesis. By disabling that rule, at least for the subgoal in question, you may allow the simplifier to make progress on the subgoal.

To illustrate what we mean by the claim that specious simplifications often arise because the system forces a false hypothesis, reconsider the example above. At the time we used the `:``type-prescription` rule, the known assumptions were `(consp x)` and `(true-listp (cdr x))`. Observe that this tells us that `x` is a true list. But the hypothesis forced to be true was `(not (true-listp x))`. Why was the falsity of this hypothesis missed? The most immediate reason is that the encoding of the two assumptions above does not produce a context (``type-alist'') in which `x` is recorded to be a true-list. When we look up `(not (true-listp x))` in that context, we are not told that it is false. More broadly, the problem stems from the fact that when we force a hypothesis we do not bring to bear on it all of the resources of the theorem prover. Thus it could be -- as here -- that the hypothesis could be proved false in the current context but is not obviously so. No matter how sophisticated we made the forcing mechanism, the unavoidable incompleteness of the theorem prover would still permit the occasional specious simplification. While that does not excuse us from trying to avoid specious simplifications when we can -- and we may well strengthen the type mechanism to deal with the problem illustrated here -- specious simplifications will probably remain a problem deserving of the user's attention.

STATE

the von Neumannesque ACL2 state object
```Major Section:  MISCELLANEOUS
```

The ACL2 state object is used extensively in programming the ACL2 system, and has been used in other ACL2 programs as well. However, most users, especially those interested in specification and verification (as opposed to programming per se), need not be aware of the role of the state object in ACL2, and will not write functions that use it explicitly. We say more about this point at the end of this documentation topic.

The global table is perhaps the most visible portion of the state object. Using the interface functions `@` and `assign`, a user will bind global variables to the results of function evaluations (much as an Nqthm user exploits the Nqthm utility `r-loop`). See @ and see assign.

ACL2 supports several facilities of a truly von Neumannesque state machine character, including file io and global variables. Logically speaking, the state is a true list of the 14 components as described below. There is a ``current'' state object at the top-level of the ACL2 command loop. This object is understood to be the value of what would otherwise be the free variable `state` appearing in top-level input. When any command returns a state object as one of its values, that object becomes the new current state. But ACL2 provides von Neumann style speed for state operations by maintaining only one physical (as opposed to logical) state object. Operations on the state are in fact destructive. This implementation does not violate the applicative semantics because we enforce certain draconian syntactic rules regarding the use of state objects. For example, one cannot ``hold on'' to an old state, access the components of a state arbitrarily, or ``modify'' a state object without passing it on to subsequent state-sensitive functions.

Every routine that uses the state facilities (e.g. does io, or calls a routine that does io), must be passed a ``state object.'' And a routine must return a state object if the routine modifies the state in any way. Rigid syntactic rules governing the use of state objects are enforced by the function `translate`, through which all ACL2 user input first passes. State objects can only be ``held'' in the formal parameter `state`, never in any other formal parameter and never in any structure (excepting a multiple-values return list field which is always a state object). State objects can only be accessed with the primitives we specifically permit. Thus, for example, one cannot ask, in code to be executed, for the length of `state` or the `car` of `state`. In the statement and proof of theorems, there are no syntactic rules prohibiting arbitrary treatment of state objects.

Logically speaking, a state object is a true list whose members are as follows:

`Open-input-channels`, an alist with keys that are symbols in package `"ACL2-INPUT-CHANNEL"`. The value (`cdr`) of each pair has the form `((:header type file-name open-time) . elements)`, where `type` is one of `:character`, `:byte`, or `:object` and `elements` is a list of things of the corresponding `type`, i.e. characters, integers of type `(mod 255)`, or lisp objects in our theory. `File-name` is a string. `Open-time` is an integer. See io.

`Open-output-channels`, an alist with keys that are symbols in package `"ACL2-OUTPUT-CHANNEL"`. The value of a pair has the form `((:header type file-name open-time) . current-contents)`. See io.

`Global-table`, an alist associating symbols (to be used as ``global variables'') with values. See @, and see assign.

`T-stack`, a list of arbitrary objects accessed and changed by the functions `aref-t-stack` and `aset-t-stack`.

`32-bit-integer-stack`, a list of arbitrary 32-bit-integers accessed and changed by the functions `aref-32-bit-integer-stack` and `aset-32-bit-integer-stack`.

`Big-clock-entry`, an integer, that is used logically to bound the amount of effort spent to evaluate a quoted form.

`Idates`, a list of dates and times, used to implement the function `print-current-idate`, which prints the date and time.

`Run-times`, a list of integers, used to implement the functions that let ACL2 report how much time was used, but inaccessible to the user.

`File-clock`, an integer that is increased on every file opening and closing and used to maintain the consistency of the `io` primitives.

`Readable-files`, an alist whose keys have the form `(string type time)`, where `string` is a file name and `time` is an integer. The value associated with such a key is a list of characters, bytes, or objects, according to `type`. The `time` field is used in the following way: when it comes time to open a file for input, we will only look for a file of the specified name and `type` whose time field is that of `file-clock`. This permits us to have a ``probe-file'' aspect to `open-file`: one can ask for a file, find it does not exist, but come back later and find that it does now exist.

`Written-files`, an alist whose keys have the form `(string type time1 time2)`, where `string` is a file name, `type` is one of `:character`, `:byte` or `:object`, and `time1` and `time2` are integers. `Time1` and `time2` correspond to the `file-clock` time at which the channel for the file was opened and closed. This field is write-only; the only operation that affects this field is `close-output-channel`, which `cons`es a new entry on the front.

`Read-files`, a list of the form `(string type time1 time2)`, where `string` is a file name and `time1` and `time2` were the times at which the file was opened for reading and closed. This field is write only.

`Writeable-files`, an alist whose keys have the form `(string type time)`. To open a file for output, we require that the name, type, and time be on this list.

`List-all-package-names-lst`, a list of `true-listps`. Roughly speaking, the `car` of this list is the list of all package names known to this Common Lisp right now and the `cdr` of this list is the value of this `state` variable after you look at its `car`. The function, `list-all-package-names`, which takes the state as an argument, returns the `car` and `cdr`s the list (returning a new state too). This essentially gives ACL2 access to what is provided by CLTL's `list-all-packages`. `Defpkg` uses this feature to insure that the about-to-be-created package is new in this lisp. Thus, for example, in `akcl` it is impossible to create the package `"COMPILER"` with `defpkg` because it is on the list, while in Lucid that package name is not initially on the list.

We recommend avoiding the use of the state object when writing ACL2 code intended to be used as a formal model of some system, for several reasons. First, the state object is complicated and contains many components that are oriented toward implementation and are likely to be irrelevant to the model in question. Second, there is currently not much support for reasoning about ACL2 functions that manipulate the state object. Third, the documentation about state is not as complete as one might wish for serious programming that uses state.

If a user is building a model that includes a system state, it is better to represent that state explicitly in the model rather than use the ACL2 state object. ACL2 functions that manipulate association lists (for example, see assoc) can be used in place of `@` and `assign` to access and update the state component of the model. As of this writing, the `"books"` directory of the ACL2 distribution contains a number of theorems already proved about such functions.

A consequence of this recommendation is that ACL2 constructs like `pprogn` and `er-progn` that depend on the state object will not appear in user-built models.