This is documentation for ACL2 Version 3.6
Copyright (C) 2009  University of Texas at Austin

This program is free software; you can redistribute it and/or modify
it under the terms of the GNU General Public License as published by
the Free Software Foundation; either version 2 of the License, or
(at your option) any later version.

This program is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
GNU General Public License for more details.

You should have received a copy of the GNU General Public License
along with this program; if not, write to the Free Software
Foundation, Inc., 675 Mass Ave, Cambridge, MA 02139, USA.

Written by:  Matt Kaufmann and J Strother Moore
Department of Computer Sciences
University of Texas at Austin
Austin, TX 78712-1188 U.S.A.

ASSOC-STRING-EQUAL    look up key, a string, in association list

(Assoc-string-equal x alist) is similar to assoc-equal.  However, for
string x and alist alist, the comparison of x with successive keys in
alist is done using string-equal rather than equal.

The guard for assoc-string-equal requires that x is a string and alist
is an alist.

ATOM    recognizer for atoms

(atom x) is true if and only if x is an atom, i.e., not a cons pair.

Atom has a guard of t, and is a Common Lisp function.  See any Common
Lisp documentation for more information.

ATOM-LISTP    recognizer for a true list of atoms

The predicate atom-listp tests whether its argument is a true-listp of
atoms, i.e., of non-conses.

BINARY-*    multiplication function

Completion Axiom:

     (equal (binary-* x y)
            (if (acl2-numberp x)
                (if (acl2-numberp y)
                    (binary-* x y)
                  0)
              0))

Guard for (binary-* x y):

     (and (acl2-numberp x) (acl2-numberp y))

Notice that like all arithmetic functions, binary-* treats non-numeric
inputs as 0.

Calls of the macro * expand to calls of binary-*; see *.

BINARY-+    addition function

Completion Axiom:

     (equal (binary-+ x y)
            (if (acl2-numberp x)
                (if (acl2-numberp y)
                    (binary-+ x y)
                  x)
              (if (acl2-numberp y)
                  y
                0)))

Guard for (binary-+ x y):

     (and (acl2-numberp x) (acl2-numberp y))

Notice that like all arithmetic functions, binary-+ treats non-numeric
inputs as 0.

Calls of the macro + expand to calls of binary-+; see +.

BINARY-APPEND    concatenate two lists

This binary function implements append, which is a macro in ACL2.  See
APPEND

The guard for binary-append requires the first argument to be a
true-listp.

BOOLE$    perform a bit-wise logical operation on 2 two's complement integers

When integers x and y are viewed in their two's complement
representation, (boole$ op x y) returns the result of applying the
bit-wise logical operation specified by op.  The following table is
adapted from documentation for analogous Common Lisp function boole in
the Common Lisp HyperSpec
(`http://www.lisp.org/HyperSpec/Body/fun_boole.html#boole').  Note that
the values of op for boole$ are ACL2 constants, rather than
corresponding values of op for the Common Lisp function boole.

     op               result
     -----------      ---------
     *boole-1*        x
     *boole-2*        y
     *boole-andc1*    and complement of x with y
     *boole-andc2*    and x with complement of y
     *boole-and*      and
     *boole-c1*       complement of x
     *boole-c2*       complement of y
     *boole-clr*      the constant 0 (all zero bits)
     *boole-eqv*      equivalence (exclusive nor)
     *boole-ior*      inclusive or
     *boole-nand*     not-and
     *boole-nor*      not-or
     *boole-orc1*     or complement of x with y
     *boole-orc2*     or x with complement of y
     *boole-set*      the constant -1 (all one bits)
     *boole-xor*      exclusive or

The guard of boole$ specifies that op is the value of one of the
constants above and that x and y are integers.

See any Common Lisp documentation for analogous information about
Common Lisp function boole.

BOOLEANP    recognizer for booleans

(Booleanp x) is t if x is t or nil, and is nil otherwise.

See GENERALIZED-BOOLEANS for a discussion of a potential
soundness problem for ACL2 related to the question:  Which Common Lisp
functions are known to return Boolean values?

BUTLAST    all but a final segment of a list

(Butlast l n) is the list obtained by removing the last n elements from
the true list l.  The following is a theorem (though it takes some
effort, including lemmas, to get ACL2 to prove it).

     (implies (and (integerp n)
                   (<= 0 n)
                   (true-listp l))
              (equal (length (butlast l n))
                     (if (< n (length l))
                         (- (length l) n)
                       0)))

For related functions, see TAKE and see NTHCDR.

The guard for (butlast l n) requires that n is a nonnegative integer
and lst is a true list.

Butlast is a Common Lisp function.  See any Common Lisp documentation
for more information.  Note:  In Common Lisp the second argument of
butlast is optional, but in ACL2 it is required.

CAAAAR    car of the caaar

See any Common Lisp documentation for details.

CAAADR    car of the caadr

See any Common Lisp documentation for details.

CAAAR    car of the caar

See any Common Lisp documentation for details.

CAADAR    car of the cadar

See any Common Lisp documentation for details.

CAADDR    car of the caddr

See any Common Lisp documentation for details.

CAADR    car of the cadr

See any Common Lisp documentation for details.

CAAR    car of the car

See any Common Lisp documentation for details.

CADAAR    car of the cdaar

See any Common Lisp documentation for details.

CADADR    car of the cdadr

See any Common Lisp documentation for details.

CADAR    car of the cdar

See any Common Lisp documentation for details.

CADDAR    car of the cddar

See any Common Lisp documentation for details.

CADDDR    car of the cdddr

See any Common Lisp documentation for details.

CADDR    car of the cddr

See any Common Lisp documentation for details.

CADR    car of the cdr

See any Common Lisp documentation for details.

CAR    returns the first element of a non-empty list, else nil

Completion Axiom:

     (equal (car x)
            (cond
             ((consp x)
              (car x))
             (t nil)))

Guard:

     (or (consp x) (equal x nil))

Notice that in the ACL2 logic, car returns nil for every atom.

CASE    conditional based on if-then-else using eql

     Example Form:
     (case typ
       ((:character foo)
        (open file-name :direction :output))
       (bar (open-for-bar file-name))
       (otherwise
        (my-error "Illegal.")))

is the same as

     (cond ((member typ '(:character foo))
            (open file-name :direction :output))
           ((eql typ 'bar)
            (open-for-bar file-name))
           (t (my-error "Illegal.")))

which in turn is the same as

     (if (member typ '(:character foo))
         (open file-name :direction :output)
         (if (eql typ 'bar)
             (open-for-bar file-name)
             (my-error "Illegal.")))

Notice the quotations that appear in the example above: '(:character
foo) and 'bar.

     General Forms:
     (case expr
       (x1 val-1)
       ...
       (xk val-k)
       (otherwise val-k+1))

     (case expr
       (x1 val-1)
       ...
       (xk val-k)
       (t val-k+1))

     (case expr
       (x1 val-1)
       ...
       (xk val-k))

where each xi is either eqlablep or a true list of eqlablep objects.
The final otherwise or t case is optional.

Case is defined in Common Lisp.  See any Common Lisp documentation for
more information.

CASE-MATCH    pattern matching or destructuring

     General Form:
     (case-match x
       (pat1 dcl1 body1)
       ...
       (patk dclk bodyk))

where x is a variable symbol, the pati are structural patterns as
described below, the dcli are optional declare forms and the bodyi are
terms.  Return the value(s) of the bodyi corresponding to the first
pati matching x, or nil if none matches.

Pattern Language:
With the few special exceptions described below, matching requires that
the cons structure of x be isomorphic to that of the pattern, down to
the atoms in the pattern.  Non-symbol atoms in the pattern match only
themselves.  Symbols in the pattern denote variables which match
anything and which are bound by a successful match to the corresponding
substructure of x.  Variables that occur more than once must match the
same (EQUAL) structure in every occurrence.

     Exceptions:
     &               Matches anything and is not bound.  Repeated
                       occurrences of & in a pattern may match different
                       structures.
     nil, t, *sym*   These symbols cannot be bound and match only their
                       global values.
     !sym            where sym is a symbol that is already bound in the
                       context of the case-match, matches only the
                       current binding of sym.
     'obj            Matches only itself.

Some examples are shown below.

Below we show some sample patterns and examples of things they match
and do not match.

     pattern       matches         non-matches
     (x y y)       (ABC 3 3)       (ABC 3 4)    ; 3 is not 4
     (fn x . rst)  (P (A I) B C)   (ABC)        ; NIL is not (x . rst)
                   (J (A I))                    ; rst matches nil
     ('fn (g x) 3) (FN (H 4) 3)    (GN (G X) 3) ; 'fn matches only itself
     (& t & !x)    ((A) T (B) (C))              ; provided x is '(C)

Consider the two binary trees that contain three leaves.  They might be
described as (x . (y . z)) and ((x . y) . z), where x, y, and z are
atomic.  Suppose we wished to recognize those trees.  The following
case-match would do:

     (case-match tree
       ((x . (y . z))
        (and (atom x) (atom y) (atom z)))
       (((x . y) . z)
        (and (atom x) (atom y) (atom z))))

Suppose we wished to recognize such trees where all three tips are
identical.  Suppose further we wish to return the tip if the tree is
one of those recognized ones and to return the number 7 otherwise.

     (case-match tree
       ((x . (x . x))
        (if (atom x) x 7))
       (((x . x) . x)
        (if (atom x) x 7))
       (& 7))

Note that case-match returns nil if no pati matches.  Thus if we must
return 7 in that case, we have to add as the final pattern the &, which
always matches anything.

CDAAAR    cdr of the caaar

See any Common Lisp documentation for details.

CDAADR    cdr of the caadr

See any Common Lisp documentation for details.

CDAAR    cdr of the caar

See any Common Lisp documentation for details.

CDADAR    cdr of the cadar

See any Common Lisp documentation for details.

CDADDR    cdr of the caddr

See any Common Lisp documentation for details.

CDADR    cdr of the cadr

See any Common Lisp documentation for details.

CDAR    cdr of the car

See any Common Lisp documentation for details.

CDDAAR    cdr of the cdaar

See any Common Lisp documentation for details.

CDDADR    cdr of the cdadr

See any Common Lisp documentation for details.

CDDAR    cdr of the cdar

See any Common Lisp documentation for details.

CDDDAR    cdr of the cddar

See any Common Lisp documentation for details.

CDDDDR    cdr of the cdddr

See any Common Lisp documentation for details.

CDDDR    cdr of the cddr

See any Common Lisp documentation for details.

CDDR    cdr of the cdr

See any Common Lisp documentation for details.

CDR    returns the second element of a cons pair, else nil

Completion Axiom:

     (equal (cdr x)
            (cond
             ((consp x)
              (cdr x))
             (t nil)))

Guard:

     (or (consp x) (equal x nil))

Notice that in the ACL2 logic, cdr returns nil for every atom.

CEILING    division returning an integer by truncating toward positive infinity

     Example Forms:
     ACL2 !>(ceiling 14 3)
     5
     ACL2 !>(ceiling -14 3)
     -4
     ACL2 !>(ceiling 14 -3)
     -4
     ACL2 !>(ceiling -14 -3)
     5
     ACL2 !>(ceiling -15 -3)
     5

(Ceiling i j) is the result of taking the quotient of i and j and
returning the smallest integer that is at least as great as that
quotient.  For example, the quotient of -14 by 3 is -4 2/3, and the
smallest integer at least that great is -4.

The guard for (ceiling i j) requires that i and j are rational (real,
in ACL2(r)) numbers and j is non-zero.

Ceiling is a Common Lisp function.  See any Common Lisp documentation
for more information.  However, note that unlike Common Lisp, the ACL2
ceiling function returns only a single value,

CHAR    the nth element (zero-based) of a string

(Char s n) is the nth element of s, zero-based.  If n is greater than
or equal to the length of s, then char returns nil.

(Char s n) has a guard that n is a non-negative integer and s is a
stringp.

Char is a Common Lisp function.  See any Common Lisp documentation for
more information.

CHAR-CODE    the numeric code for a given character

Completion Axiom:

     (equal (char-code x)
            (if (characterp x)
                (char-code x)
              0))

Guard for (char-code x):

     (characterp x)

This function maps all non-characters to 0.

CHAR-DOWNCASE    turn upper-case characters into lower-case characters

(Char-downcase x) is equal to #a when x is #A, #b when x is #B, ...,
and #z when x is #Z, and is x for any other character.

The guard for char-downcase requires its argument to be a standard
character (see STANDARD-CHAR-P).

Char-downcase is a Common Lisp function.  See any Common Lisp
documentation for more information.

CHAR-EQUAL    character equality without regard to case

For characters x and y, (char-equal x y) is true if and only if x and y
are the same except perhaps for their case.

The guard on char-equal requires that its arguments are both standard
characters (see STANDARD-CHAR-P).

Char-equal is a Common Lisp function.  See any Common Lisp
documentation for more information.

CHAR-UPCASE    turn lower-case characters into upper-case characters

(Char-upcase x) is equal to #A when x is #a, #B when x is #b, ..., and
#Z when x is #z, and is x for any other character.

The guard for char-upcase requires its argument to be a standard
character (see STANDARD-CHAR-P).

Char-upcase is a Common Lisp function.  See any Common Lisp
documentation for more information.

CHAR<    less-than test for characters

(char< x y) is true if and only if the character code of x is less than
that of y.  See CHAR-CODE.

The guard for char< specifies that its arguments are characters.

Char< is a Common Lisp function.  See any Common Lisp documentation for
more information.

CHAR<=    less-than-or-equal test for characters

(char<= x y) is true if and only if the character code of x is less
than or equal to that of y.  See CHAR-CODE.

The guard for char<= specifies that its arguments are characters.

Char<= is a Common Lisp function.  See any Common Lisp documentation
for more information.

CHAR>    greater-than test for characters

(char> x y) is true if and only if the character code of x is greater
than that of y.  See CHAR-CODE.

The guard for char> specifies that its arguments are characters.

Char> is a Common Lisp function.  See any Common Lisp documentation for
more information.

CHAR>=    greater-than-or-equal test for characters

(char>= x y) is true if and only if the character code of x is greater
than or equal to that of y.  See CHAR-CODE.

The guard for char>= specifies that its arguments are characters.

Char>= is a Common Lisp function.  See any Common Lisp documentation
for more information.

CHARACTER-ALISTP    recognizer for association lists with characters as keys

(Character-alistp x) is true if and only if x is a list of pairs of the
form (cons key val) where key is a characterp.

CHARACTER-LISTP    recognizer for a true list of characters

The predicate character-listp tests whether its argument is a true list
of characters.

CHARACTERP    recognizer for characters

(characterp x) is true if and only if x is a character.

CHARACTERS    characters in ACL2

ACL2 accepts 256 distinct characters, which are the characters obtained
by applying the function code-char to each integer from 0 to 255.
Among these, Common Lisp designates certain ones as _standard
characters_, namely those of the form (code-char n) where n is from 33
to 126, together with #\Newline and #\Space.  The actual standard
characters may be viewed by evaluating the defconst *standard-chars*.

To be more precise, Common Lisp does not specify the precise
relationship between code-char and the standard characters.  However,
we check that the underlying Common Lisp implementation uses a
particular relationship that extends the usual ASCII coding of
characters.  We also check that Space, Tab, Newline, Page, and Rubout
correspond to characters with respective char-codes 32, 9, 10, 12, and
127.

Code-char has an inverse, char-code.  Thus, when char-code is applied
to an ACL2 character, c, it returns a number n between 0 and 255
inclusive such that (code-char n) = c.

The preceding paragraph implies that there is only one ACL2 character
with a given character code.  CLTL allows for "attributes" for
characters, which could allow distinct characters with the same code,
but ACL2 does not allow this.

_The Character Reader_

ACL2 supports the `#\' notation for characters provided by Common Lisp,
with some restrictions.  First of all, for every character c, the
notation

     #\c

may be used to denote the character object c.  That is, the user may
type in this notation and ACL2 will read it as denoting the character
object c.  In this case, the character immediately following c must be
one of the following "terminating characters": a Tab, a Newline, a Page
character, a space, or one of the characters:

     "  '  (  )  ;  `  ,

Other than the notation above, ACL2 accepts alternate notation for five
characters.

     #\Space
     #\Tab
     #\Newline
     #\Page
     #\Rubout

Again, in each of these cases the next character must be from among the
set of "terminating characters" described in the single-character case.
Our implementation is consistent with IS0-8859, even though we don't
provide #\ syntax for entering characters other than that described
above.

Finally, we note that it is our intention that any object printed by
ACL2's top-level-loop may be read back into ACL2.  Please notify the
implementors if you find a counterexample to this claim.

CLOSE-INPUT-CHANNEL    See IO.

CLOSE-OUTPUT-CHANNEL    See IO.

CODE-CHAR    the character corresponding to a given numeric code

Completion Axiom:

     (equal (code-char x)
            (if (and (integerp x)
                     (>= x 0)
                     (< x 256))
                (code-char x)
              (code-char 0)))

Guard for (code-char x):

     (and (integerp x)
          (>= x 0)
          (< x 256))

ACL2 supports 8-bit characters.  Inputs not between 0 and 255 are
treated as 0.

COERCE    coerce a character list to a string and a string to a list

Completion Axiom:

     (equal (coerce x y)
            (cond
             ((equal y 'list)
              (if (stringp x)
                  (coerce x 'list)
                nil))
             (t
              (coerce (make-character-list x) 'string))))

Guard for (coerce x y):

     (if (equal y 'list)
         (stringp x)
       (if (equal y 'string)
           (character-listp x)
         nil))

Also see distributed book books/misc/fast-coerce.lisp, contributed by
Jared Davis, for a version of coerce that may be faster for Common Lisp
implementations other than CCL 1.3 or later, if the second argument is
'list (for coercing a string to a list).

COMPILATION    compiling ACL2 functions

ACL2 has several mechanisms to speed up the evaluation of function
calls by _compiling_ functions: see COMP, see
SET-COMPILE-FNS, and see CERTIFY-BOOK.  The intention is that
compilation never changes the value returned by a function call, though
it could cause the call to succeed rather than fail, for example by
avoiding a stack overflow.

The state global variable 'suppress-compile is set automatically when
the system is built, according to the underlying Lisp implementation.  A
non-nil value of this variable -- that is, a nonnil value of (@
suppress-compile) -- avoids all explicit calls to the compiler:
include-book and certify-book coerce their compilation arguments to
nil, and both comp and set-compile-fns are no-ops.  When this is the
case, it is because our experience is that performance on the given
platform when explicit compilation is suppressed may be slightly better
than when the compiler is invoked explicitly.  For example, this
situation is the case when the underlying Lisp is CCL (OpenMCL).  A key
is that CCL compiles on-the-fly even when the compiler is not called
explicitly, and our observation has been that compiling a file in CCL
does not seem to improve appreciably the efficiency of the generated
code.

COMPLEX    create an ACL2 number

     Examples:
     (complex x 3) ; x + 3i, where i is the principal square root of -1
     (complex x y) ; x + yi
     (complex x 0) ; same as x, for rational numbers x

The function complex takes two rational number arguments and returns an
ACL2 number.  This number will be of type (complex rational) [as
defined in the Common Lisp language], except that if the second
argument is zero, then complex returns its first argument.  The
function complex-rationalp is a recognizer for complex rational
numbers, i.e. for ACL2 numbers that are not rational numbers.

The reader macro #C (which is the same as #c) provides a convenient way
for typing in complex numbers.  For explicit rational numbers x and y,
#C(x y) is read to the same value as (complex x y).

The functions realpart and imagpart return the real and imaginary parts
(respectively) of a complex (possibly rational) number.  So for
example, (realpart #C(3 4)) = 3, (imagpart #C(3 4)) = 4, (realpart 3/4)
= 3/4, and (imagpart 3/4) = 0.

The following built-in axiom may be useful for reasoning about complex
numbers.

     (defaxiom complex-definition
       (implies (and (real/rationalp x)
                     (real/rationalp y))
                (equal (complex x y)
                       (+ x (* #c(0 1) y))))
       :rule-classes nil)

A completion axiom that shows what complex returns on arguments
violating its guard (which says that both arguments are rational
numbers) is the following.

     (equal (complex x y)
            (complex (if (rationalp x) x 0)
                     (if (rationalp y) y 0)))

COMPLEX-RATIONALP    recognizes complex rational numbers

     Examples:
     (complex-rationalp 3)       ; nil, as 3 is rational, not complex rational
     (complex-rationalp #c(3 0)) ; nil, since #c(3 0) is the same as 3
     (complex-rationalp t)       ; nil
     (complex-rationalp #c(3 1)) ; t, as #c(3 1) is the complex number 3 + i

See COMPLEX for more about complex rationals in ACL2.

COMPLEX/COMPLEX-RATIONALP    recognizer for complex numbers

For most ACL2 users, this is a macro abbreviating complex-rationalp;
see COMPLEX-RATIONALP.  In  ACL2(r) (see REAL), a
complex number x may have irrational real and imaginary parts.  This
macro abbreviates the predicate complexp in ACL2(r), which holds for
such x.  Most ACL2 users can ignore this macro and use complex-rationalp
instead.  Some books in the ACL2 distribution use
complex/complex-rationalp so that they are suitable for ACL2(r) as well.

CONCATENATE    concatenate lists or strings together

     Examples:
     (concatenate 'string "ab" "cd" "ef")     ; equals "abcdef"
     (concatenate 'string "ab")               ; equals "ab"
     (concatenate 'list '(a b) '(c d) '(e f)) ; equals '(a b c d e f)
     (concatenate 'list)                      ; equals nil

     General Form:
     (concatenate result-type x1 x2 ... xn)

where n >= 0 and either:  result-type is 'string and each xi is a
string; or result-type is 'list and each xi is a true list.
Concatenate simply concatenates its arguments to form the result string
or list.  Also see APPEND and see STRING-APPEND, though
concatenate is probably preferable to string-append for efficiency.

Note:  We do *not* try to comply with the Lisp language's insistence
that concatenate copies its arguments.  Not only are we in an
applicative setting, where this issue shouldn't matter for the logic,
but also we do not actually modify the underlying lisp implementation
of concatenate; we merely provide a definition for it.

Concatenate is a Common Lisp function.  See any Common Lisp
documentation for more information.

COND    conditional based on if-then-else

Cond is the construct for IF, THEN, ELSE IF, ...  The test is against
nil.  The argument list for cond is a list of "clauses", each of which
is a list.  In ACL2, clauses must have length 1 or 2.

Cond is a Common Lisp macro.  See any Common Lisp documentation for
more information.

CONJUGATE    complex number conjugate

Conjugate takes an ACL2 number as an argument, and returns its complex
conjugate (i.e., the result of negating its imaginary part.).

Conjugate is a Common Lisp function.  See any Common Lisp documentation
for more information.

CONS    pair and list constructor

(cons x y) is a pair whose first component is x and second component is
y.  If y is a list, then (cons x y) is a list that has an addtional
element x on the front.

CONSP    recognizer for cons pairs

(consp x) is true if and only if x is a cons pair.

CPU-CORE-COUNT    the number of cpu cores

Unless the ACL2 executable supports parallel evaluation (see
PARALLELISM), this function returns (mv 1 state).  Otherwise:

(Cpu-core-count state) returns (mv core-count state), where core-count
is the number of cpu cores if ACL2 can get that information from the
underlying Common Lisp implementation.  Otherwise an error occurs,
unless global 'cpu-core-count is assigned to a positive integer value
(see ASSIGN), in which case that value is returned as the
core-count.

     Example:
     (cpu-core-count state) ==> (mv 4 state)
.

CW    print to the comment window

Example:

     (cw "The goal is ~p0 and the alist is ~x1.~%"
         (untranslate term t nil)
         unify-subst)

Logically, this expression is equivalent to nil.  However, it has the
effect of first printing to the so-called "comment window" the fmt
string as indicated.  Thus, cw is like fmt (see FMT) except in
three important ways.  First, it is a :logic mode function.  Second, it
neither takes nor returns the ACL2 state;  logically cw simply returns
nil, although it prints to a _comment window_ that just happens to
share the terminal screen with the standard character output
*standard-co*.  Third, its fmt args are positional references, so that
for example

     (cw "Answers: ~p0 and ~p1" ans1 ans2)

prints in the same manner as:

     (fmt "Answers: ~p0 and ~p1"
          (list (cons #\0 ans1) (cons #\1 ans2))
          *standard-co* state nil)

Typically, calls of cw are embedded in prog2$ forms, e.g.,

     (prog2$ (cw ...)
             (mv a b c))

which has the side-effect of printing to the comment window and
logically returning (mv a b c).

     General Form:
     (cw fmt-string arg1 arg2 ... argn)

where n is between 0 and 9 (inclusive).  The macro uses
fmt-to-comment-window, passing it the column 0 and evisc-tuple nil,
after assembling the appropriate alist binding the fmt vars #\0 through
#\9; see FMT.  If you want

     (a) more than 10 vars,
     (b) vars other than the digit chars,
     (c) a different column, or
     (d) a different evisc-tuple,

then call fmt-to-comment-window instead.

Also see CW!, which is useful if you want to be able to read
the printed forms back in.

CW!    print to the comment window

This is the same as cw, except that cw inserts backslash (\) characters
when forced to print past the right margin, in order to make the output
a bit clearer in that case.  Use cw! instead if you want to be able to
read the forms back in.

DECLARE    declarations

     Examples:
     (declare (ignore x y z))
     (declare (ignorable x y z)
              (type integer i j k)
              (type (satisfies integerp) m1 m2))
     (declare (xargs :guard (and (integerp i)
                                 (<= 0 i))
                     :guard-hints (("Goal" :use (:instance lemma3
                                                   (x (+ i j)))))))

     General Form:
     (declare d1 ... dn)
     where, in ACL2, each di is of one of the following forms:

       (ignore v1 ... vn) -- where each vi is a variable introduced in
       the immediately superior lexical environment.  These variables must not
       occur free in the scope of the declaration.

       (ignorable v1 ... vn) -- where each vi is a variable introduced in
       the immediately superior lexical environment.  These variables need not
       occur free in the scope of the declaration.  This declaration can be useful
       for inhibiting compiler warnings.

       (type type-spec v1 ... vn) -- where each vi is a variable introduced in the
       immediately superior lexical environment and type-spec is a type specifier
       (as described in the documentation for type-spec).

       (xargs :key1 val1 ... :keyn valn) -- where the legal values of the keyi's
       and their respective vali's are described in the documentation for
       xargs.

       (optimize ...) -- for example, (optimize (safety 3)).  This is allowed
       only at the top level of defun forms.  See any Common Lisp
       documentation for more information.

Declarations in ACL2 may occur only where dcl occurs below:

       (DEFUN name args doc-string dcl ... dcl body)
       (DEFMACRO name args doc-string dcl ... dcl body)
       (LET ((v1 t1) ...) dcl ... dcl body)
       (MV-LET (v1 ...) term dcl ... dcl body)

Of course, if a form macroexpands into one of these (as let* expands
into nested lets and our er-let* expands into nested mv-lets) then
declarations are permitted as handled by the macros involved.

Declare is defined in Common Lisp.  See any Common Lisp documentation
for more information.

DEFN    definition with guard t

Defn is defun with guard t.

DENOMINATOR    divisor of a ratio in lowest terms

Completion Axiom:

     (equal (denominator x)
            (if (rationalp x)
                (denominator x)
              1))

Guard for (denominator x):

     (rationalp x)

DIGIT-CHAR-P    the number, if any, corresponding to a given character

(digit-char-p ch) is the integer corresponding to the character ch in
base 10.  For example, (digit-char-p #\3) is equal to the integer 3.
More generally, an optional second argument specifies the radix
(default 10, as indicated above).

The guard for digit-char-p (more precisely, for the function
our-digit-char-p that calls of this macro expand to) requires its
second argument to be an integer between 2 and 36, inclusive, and its
first argument to be a character.

Digit-char-p is a Common Lisp function, though it is implemented in the
ACL2 logic as an ACL2 macro.  See any Common Lisp documentation for
more information.

DIGIT-TO-CHAR    map a digit to a character

     Example:
     ACL2 !>(digit-to-char 8)
     #\8

For an integer n from 0 to 15, (digit-to-char n) is the character
corresponding to n in hex notation, using uppercase letters for digits
exceeding 9.  If n is in the appropriate range, that result is of course
also the binary, octal, and decimal digit.

The guard for digit-to-char requires its argument to be an integer
between 0 and 15, inclusive.

E0-ORD-<    the old ordering function for ACL2 ordinals

See O< for the current new ordering function for ACL2 ordinals.

The functions e0-ordinalp and e0-ord-< were replaced in ACL2
Version_2.8 by o-p and o<, respectively.  However, books created before
that version used the earlier functions for termination proofs; the old
functions might be of use in these cases.  To use the old functions in
termination proofs, include the book books/ordinals/e0-ordinal and
execute the event (set-well-founded-relation e0-ord-<) (see
SET-WELL-FOUNDED-RELATION).  For a more thorough discussion of these
functions, see the documentation at the end of
books/ordinals/e0-ordinal.lisp.

E0-ORDINALP    the old recognizer for ACL2 ordinals

See O-P for the current recognizer for ACL2 ordinals.

The functions e0-ordinalp and e0-ord-< were replaced in ACL2
Version_2.8 by o-p and o<, respectively.  However, books created before
that version used the earlier functions for termination proofs; the old
functions might be of use in these cases.  To use the old functions in
termination proofs, include the book books/ordinals/e0-ordinal and
execute the event (set-well-founded-relation e0-ord-<) (see
SET-WELL-FOUNDED-RELATION).  For a more thorough discussion of these
functions, see the documentation at the end of
books/ordinals/e0-ordinal.lisp.

EC-CALL    execute a call in the ACL2 logic instead of raw Lisp

The name "ec-call" represents "executable-counterpart call."  This
utility is intended for users who are familiar with guards.  See
GUARD for a general discussion of guards.

Logically, ec-call is the identity function; indeed, during proofs it
behaves more like the identity macro, in the sense that (ec-call TERM)
is typically replaced quickly by TERM during a proof attempt.  However,
ec-call causes function calls to be evaluated in the ACL2 logic rather
than raw Lisp, as explained below.

     General Form:
     (ec-call (fn term1 ... termk))

where fn is a known function symbol other than those in the list that is
the value of the constant *ec-call-bad-ops*.  Semantically, (ec-call
(fn term1 ... termk)) equals (fn term1 ... termk).  However, this use
of ec-call has two effects.

     (1) Guard verification generates no proof obligations from the
     guard of fn for this call.  Indeed, guards need not have been
     verified for fn.

     (2) During evaluation, after the arguments of fn are evaluated as
     usual, the executable counterpart of fn is called, rather than fn
     as defined in raw Lisp.  That is, the call of fn is made on its
     evaluated arguments as though this call is being made in the ACL2
     top-level loop, rather than in raw Lisp.  In particular, the guard
     of fn is checked, at least by default (see
     SET-GUARD-CHECKING.

Note that in the term (ec-call (fn term1 ... termk)), only the indicated
call of fn is made in the logic; each termi is evaluated in the normal
manner.  If you want an entire term evaluated in the logic, wrap
ec-call around each function call in the term (other than calls of if
and ec-call).

Here is a small example.  We define foo recursively but with guard
verification inhibited on the recursive call, which is to be evaluated
in the ACL2 logic.

     ACL2 !>(defun foo (x y)
             (declare (xargs :guard (consp y)))
             (if (consp x)
                 (cons (car x) (ec-call (foo (cdr x) (cdr y))))
               (car y)))

     The admission of FOO is trivial, using the relation O< (which is known
     to be well-founded on the domain recognized by O-P) and the measure
     (ACL2-COUNT X).  We could deduce no constraints on the type of FOO.

     Computing the guard conjecture for FOO....

     The guard conjecture for FOO is trivial to prove.  FOO is compliant
     with Common Lisp.

     Summary
     Form:  ( DEFUN FOO ...)
     Rules: NIL
     Warnings:  None
     Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
      FOO
     ACL2 !>(foo '(2 3 4 5) '(6 7))

     ACL2 Error in TOP-LEVEL:  The guard for the function symbol FOO, which
     is (CONSP Y), is violated by the arguments in the call (FOO '(4 5) NIL).
     See :DOC trace for a useful debugging utility.  See :DOC set-guard-
     checking for information about suppressing this check with (set-guard-
     checking :none), as recommended for new users.

The error above arises because eventually, foo recurs down to a value of
parameter y that violates the guard.  This is clear from tracing (see
TRACE$ and see TRACE).  Each call of the executable
counterpart of foo (the so-called "*1*" function for foo) checks the
guard and then invokes the raw Lisp version of foo.  The raw Lisp
version calls the executable counterpart on the recursive call.  When
the guard check fails we get a violation.

     ACL2 !>(trace$ foo)
      ((FOO))
     ACL2 !>(foo '(2 3 4 5) '(6 7))
     1> (ACL2_*1*_ACL2::FOO (2 3 4 5) (6 7))
       2> (FOO (2 3 4 5) (6 7))
         3> (ACL2_*1*_ACL2::FOO (3 4 5) (7))
           4> (FOO (3 4 5) (7))
             5> (ACL2_*1*_ACL2::FOO (4 5) NIL)

     ACL2 Error in TOP-LEVEL:  The guard for the function symbol FOO, which
     is (CONSP Y), is violated by the arguments in the call (FOO '(4 5) NIL).
     See :DOC trace for a useful debugging utility.  See :DOC set-guard-
     checking for information about suppressing this check with (set-guard-
     checking :none), as recommended for new users.

     ACL2 !>

If we turn off guard errors then we can see the trace as above, but
where we avoid calling the raw Lisp function when the guard fails to
hold.

     ACL2 !>:set-guard-checking nil

     Masking guard violations but still checking guards except for self-
     recursive calls.  To avoid guard checking entirely, :SET-GUARD-CHECKING
     :NONE.  See :DOC set-guard-checking.

     ACL2 >(foo '(2 3 4 5) '(6 7))
     1> (ACL2_*1*_ACL2::FOO (2 3 4 5) (6 7))
       2> (FOO (2 3 4 5) (6 7))
         3> (ACL2_*1*_ACL2::FOO (3 4 5) (7))
           4> (FOO (3 4 5) (7))
             5> (ACL2_*1*_ACL2::FOO (4 5) NIL)
               6> (ACL2_*1*_ACL2::FOO (5) NIL)
                 7> (ACL2_*1*_ACL2::FOO NIL NIL)
                 <7 (ACL2_*1*_ACL2::FOO NIL)
               <6 (ACL2_*1*_ACL2::FOO (5))
             <5 (ACL2_*1*_ACL2::FOO (4 5))
           <4 (FOO (3 4 5))
         <3 (ACL2_*1*_ACL2::FOO (3 4 5))
       <2 (FOO (2 3 4 5))
     <1 (ACL2_*1*_ACL2::FOO (2 3 4 5))
     (2 3 4 5)
     ACL2 >

EIGHTH    eighth member of the list

See any Common Lisp documentation for details.

ENDP    recognizer for empty lists

In the ACL2 logic, (endp x) is the same as (atom x).  See ATOM.

Unlike atom, the guard for endp requires that x is a cons pair or is
nil.  Thus, endp is typically used as a termination test for functions
that recur on a true-listp argument.  See GUARD for general
information about guards.

Endp is a Common Lisp function.  See any Common Lisp documentation for
more information.

EQ    equality of symbols

Eq is the function for determining whether two objects are identical
(i.e., have the exact same store address in the current von Neumann
implementation of Common Lisp).  It is the same as equal in the ACL2
logic.

Eq is a Common Lisp function.  In order to ensure conformance with
Common Lisp, the ACL2 guard on eq requires at least one of the
arguments to eq to be a symbol.  Common Lisp guarantees that if x is a
symbol, then x is eq to y if and only if x is equal to y.  Thus, the
ACL2 user should think of eq as nothing besides a fast means for
checking equal when one argument is known to be a symbol.  In
particular, it is possible that an eq test will not even require the
cost of a function call but will be as fast as a single machine
instruction.

EQL    test equality (of two numbers, symbols, or characters)

(eql x y) is logically equivalent to (equal x y).

Unlike equal, eql has a guard requiring at least one of its arguments
to be a number, a symbol, or a character.  Generally, eql is executed
more efficiently than equal.

For a discussion of the various ways to test against 0, See
ZERO-TEST-IDIOMS.

Eql is a Common Lisp function.  See any Common Lisp documentation for
more information.

EQLABLE-ALISTP    recognizer for a true list of pairs whose cars are suitable for eql

The predicate eqlable-alistp tests whether its argument is a true-listp
of consp objects whose cars all satisfy eqlablep.

EQLABLE-LISTP    recognizer for a true list of objects each suitable for eql

The predicate eqlable-listp tests whether its argument is a true-listp
of objects satisfying eqlablep.

EQLABLEP    the guard for the function eql

The predicate eqlablep tests whether its argument is suitable for eql,
at least one of whose arguments must satisfy this predicate in Common
Lisp.  (Eqlablep x) is true if and only if its argument is a number, a
symbol, or a character.

EQUAL    true equality

(equal x y) is equal to t or nil, according to whether or not x and y
are the same value.

For a discussion of the various idioms for testing against 0, See
ZERO-TEST-IDIOMS.

ER    print an error message and "cause an error"

     Example Forms:
     (er hard  'top-level "Illegal inputs, ~x0 and ~x1." a b)
     (er hard? 'top-level "Illegal inputs, ~x0 and ~x1." a b)
     (er soft  'top-level "Illegal inputs, ~x0 and ~x1." a b)

The examples above all print an error message to standard output saying
that a and b are illegal inputs.  However, the first two abort
evaluation after printing an error message, while the third returns (mv
t nil state) after printing an error message.  The result in the third
case can be interpreted as an "error" when programming with the ACL2
state, something most ACL2 users will probably not want to do; see
LD-ERROR-TRIPLES and see ER-PROGN.

The difference between the hard and hard? forms is one of guards.  Use
hard if you want the call to generate a (clearly impossible) guard
proof obligation of (essentially) NIL.  But use hard? if you want to be
able to call this function in guard-verified code, since the call
generates a (trivially satisfied) guard proof obligation of T.

Er is a macro, and the above three examples expand to calls of ACL2
functions, as shown below.  See ILLEGAL, see
HARD-ERROR, and see ERROR1.  The first two have guards of
(essentially) NIL and T, respectively, while error1 is in :program mode.

     General forms:
     (er hard  ctx fmt-string arg1 arg2 ... argk)
       ==> {macroexpands, in essence, to:}
     (ILLEGAL    CTX FMT-STRING
                 (LIST (CONS #\0 ARG1) (CONS #\1 ARG2) ... (CONS #\k ARGk)))

     (er hard? ctx fmt-string arg1 arg2 ... argk)
       ==> {macroexpands, in essence, to:}
     (HARD-ERROR CTX FMT-STRING
                 (LIST (CONS #\0 ARG1) (CONS #\1 ARG2) ... (CONS #\k ARGk)))

     (er soft  ctx fmt-string arg1 arg2 ... argk)
       ==> {macroexpands, in essence, to:}
     (ERROR1     CTX FMT-STRING
                 (LIST (CONS #\0 ARG1) (CONS #\1 ARG2) ... (CONS #\k ARGk)))

ER-PROGN    perform a sequence of state-changing "error triples"

     Example:
     (er-progn (check-good-foo-p (f-get-global 'my-foo state) state)
               (value (* (f-get-global 'my-foo state)
                         (f-get-global 'bar state))))

This sequencing primitive is only useful when programming with state,
something that very few users will probably want to do.  See
STATE.

Er-progn is used much the way that progn is used in Common Lisp, except
that it expects each form within it to evaluate to an "error triple" of
the form (mv erp val state).  The first such form, if any, that
evaluates to such a triple where erp is not nil yields the error triple
returned by the er-progn.  If there is no such form, then the last form
returns the value of the er-progn form.

We intend to write more about this topic, especially if there are
requests to do so.

ERROR1    print an error message and cause a "soft error"

(Error1 ctx str alist) returns (mv t nil state).  An error message is
first printed using the the "context" ctx, as well as the string str
and alist alist that are of the same kind as expected by fmt.  See
FMT.

Error1 can be interpreted as causing an "error" when programming with
the ACL2 state, something most ACL2 users will probably not want to do;
see LD-ERROR-TRIPLES and see ER-PROGN.  In order to
cause errors with :logic mode functions, see HARD-ERROR and see
ILLEGAL.  Better yet, see ER for a macro that provides
a unified way of signaling errors.

As mentioned above, error1 always returns (mv t nil state).  But if a
call (error1 ctx str alist) is encountered during evaluation, then the
string str is first printed using the association list alist (as in
fmt).  Here is a trivial, contrived example.

     ACL2 !>(error1 'my-context
                    "Printing 4: ~n0"
                    (list (cons #\0 4))
                    state)

     ACL2 Error in MY-CONTEXT:  Printing 4: four

     ACL2 !>

EVENP    test whether an integer is even

(evenp x) is true if and only if the integer x is even.  Actually, in
the ACL2 logic (evenp x) is defined to be true when x/2 is an integer.

The guard for evenp requires its argument to be an integer.

Evenp is a Common Lisp function.  See any Common Lisp documentation for
more information.

EXPLODE-NONNEGATIVE-INTEGER    the list of characters in the radix-r form of a number

     Examples:
     ACL2 !>(explode-nonnegative-integer 925 10 nil)
     (#9 #2 #5)
     ACL2 !>(explode-nonnegative-integer 325 16 nil)
     (#3 #9 #D)

For a non-negative integer n, (explode-nonnegative-integer n r nil) is
the list of characters in the radix-r (base-r) representation of n.

The guard for explode-nonnegative-integer requires the first argument
to be a nonnegative integer and second argument to be a valid radix for
ACL2 (2, 8, 10, or 16).

EXPT    exponential function

(Expt r i) is the result of raising the number r to the integer power i.

The guard for (expt r i) is that r is a number and i is an integer, and
furthermore, if r is 0 then i is nonnegative.  When the type
requirements of the guard aren't met, (expt r i) first coerces r to a
number and i to an integer.

Expt is a Common Lisp function.  See any Common Lisp documentation for
more information.  Note that r can be a complex number; this is
consistent with Common lisp.

FIFTH    fifth member of the list

See any Common Lisp documentation for details.

FIRST    first member of the list

See any Common Lisp documentation for details.

FIX    coerce to a number

Fix simply returns any numeric argument unchanged, returning 0 on a
non-numeric argument.  Also see NFIX, see IFIX, and see
RFIX for analogous functions that coerce to a natural number,
an integer, and a rational number, respectively.

Fix has a guard of t.

FIX-TRUE-LIST    coerce to a true list

Fix-true-list is the identity function on true-listp objects.  It
converts every list to a true list by dropping the final cdr, and it
converts every atom to nil.

FLET    local binding of function symbols

     Example Form:
     ; The following evaluates to (mv 7 10):
     (flet ((f (x)
               (+ x 3))
            (g (x)
               (declare (type integer x))
               (* x 2)))
       (mv (f 4) (g 5)))

     General Form:
     (flet (def1 ... defk) body)

where body is a term, and each defi is a definition as in defun but
with the leading defun symbol omitted.  See DEFUN.  The
innermost flet-binding of a function symbol, f, above a call of f, is
the one that provides the definition of f for that call.  Note that
flet does not provide recursion.  Consider the following example.

     (defun f (x) (+ x 3))
     (flet ((f (x) (cons x (f (1+ x)))))
       (f 4))

In the above term (cons x (f (1+ x))), f refers to the global
definition of f above the flet expression.  However, (f 4) refers to
the flet-binding of f, (f (x) (cons x (f x))).  The result of the flet
expression is thus obtained by evaluating (f 4) where (f 4) is (cons 4
(f (1+ 4))), where the latter call of f refers to the global
definition; thus we have (cons 4 (f 5)), which evaluates to (4 . 8).

Although flet behaves in ACL2 essentially as it does in Common Lisp,
ACL2 imposes the following restrictions and qualifications.

     o Every declare form for a local definition (def1 through defk,
     above) must be an ignore, ignorable, or type expression.

     o Each defi must bind a different function symbol.

     o Each defi must bind a symbol that is a legal name for an ACL2
     function symbol.  In particular, the symbol may not be in the
     keyword package or the main Lisp package.  Moreover, the symbol
     may not be a built-in ACL2 function or macro.

     o Every variable occurring in the body of a defi must be a formal
     parameter of that defi.  (This restriction is not enforced in
     Common Lisp.  If the restriction is inconvenient for you, the ACL2
     implementors may be able to remove it, with some effort, if you
     ask.)

     o If the flet-binding defi is in the body of a function f, then
     the stobj inputs for defi are implicitly those of its inputs that
     are declared stobj inputs of f.

Flet bindings are evaluated in parallel.  Consider the following
example.

     (defun f (x) x)
     (flet ((f (x) (cons x x))
            (g (x) (f x)))
       (g 3))

The binding of g refers to the global value of f, not the flet-binding
of f.  Thus, the flet expression evaluates to 3.  Compare the flet
expression above to the following one, which instead evaluates to (3 .
3).

     (defun f (x) x)
     (flet ((f (x) (cons x x)))
       (flet ((g (x) (f x)))
         (g 3)))

Under the hood, ACL2 translates flet bindings to lambda expressions
(see TERM).  The following example illustrates this point.

     ACL2 !>:trans (flet ((f (x) (cons x x))
                          (g (x y) (+ x y)))
                     (f (g 3 4)))

     ((LAMBDA (X) (CONS X X))
      ((LAMBDA (X Y) (BINARY-+ X Y)) '3 '4))

     => *

     ACL2 !>

Flet is part of Common Lisp.  See any Common Lisp documentation for
more information.  We conclude by pointing out an important aspect of
flet shared by ACL2 and Common Lisp: The binding is lexical, not
dynamic.  That is, the flet binding of a function symbol only applies to
calls of that function symbol in the body of the flet, not other calls
made in the course of evaluation.  Consider the following example.
Suppose we define:

     (defun f (x) x)
     (defun g (x) x)
     (defun h (x)
       (flet ((f (x) (cons x x)))
         (g x)))

Then evaluation of (h 3) results in 3, not in the cons pair (3 . 3),
because the flet binding of f only applies to calls of f that appear in
the body of that flet.  In this case, only g is called in the body of
that flet.

FLOOR    division returning an integer by truncating toward negative infinity

     Example Forms:
     ACL2 !>(floor 14 3)
     4
     ACL2 !>(floor -14 3)
     -5
     ACL2 !>(floor 14 -3)
     -5
     ACL2 !>(floor -14 -3)
     4
     ACL2 !>(floor -15 -3)
     5

(Floor i j) returns the result of taking the quotient of i and j and
returning the greatest integer not exceeding that quotient.  For
example, the quotient of -14 by 3 is -4 2/3, and the largest integer
not exceeding that rational number is -5.

The guard for (floor i j) requires that i and j are rational (real, in
ACL2(r)) numbers and j is non-zero.

Floor is a Common Lisp function.  See any Common Lisp documentation for
more information.  However, note that unlike Common Lisp, the ACL2
floor function returns only a single value,

FMS    :(str alist co-channel state evisc) => state

See FMT for further explanation, including documentation of the
tilde-directives.

FMS!    :(str alist co-channel state evisc) => state

This function is nearly identical to fms; see FMS.  The only
difference is that fms may insert backslash (\) characters when forced
to print past the right margin in order to make the output a bit
clearer in that case.  Use fms! instead if you want to be able to read
the forms back in.

FMT    formatted printing

ACL2 provides the functions fmt, fmt1, and fms as substitutes for Common
Lisp's format function.  Also see FMT!, see FMT1!, and
see FMS! for versions of these functions that write forms to
files in a manner that allows them to be read, by avoiding using
backslash (\) to break long lines.

All three print a given string under an alist pairing character objects
with values, interpreting certain "tilde-directives" in the string.
Channel must be a character output channel (e.g., *standard-co*).

     General Forms:                                            result
     (fms string alist channel state evisc-tuple)         ; state
     (fmt string alist channel state evisc-tuple)         ; (mv col state)
     (fmt1 string alist column channel state evisc-tuple) ; (mv col state)

Fms and fmt print an initial newline to put channel in column 0; Fmt1
requires the current column as input.  Columns are numbered from 0.
The current column is the column into which the next character will be
printed.  (Thus, the current column number is also the number of
characters printed since the last newline.)  The col returned by fmt
and fmt1 is the current column at the conclusion of the formatting.
Evisc-tuple must be either nil (meaning no abbreviations are used when
objects are printed) or an "evisceration tuple"; see
EVISC-TUPLE.

We list the tilde-directives below.  The notation is explained after
the chart.

     ~xx  pretty print vx (maybe after printing a newline)
     ~yx  pretty print vx starting in current column; end with newline
     ~Xxy like ~xx but use vy as the evisceration tuple
     ~Yxy like ~yx but use vy as the evisceration tuple
     ~@x  if vx is a string, "str",  recursively format "str"
          if vx is ("str" . a), recursively format "str" under a+
     ~#x~[...~/...~/ ... ~/...~] cases on vx
          ^    ^     ...   ^  if 0<=vx<=k, choose vxth alternative
          0    1     ...   k  if vx is a list of length 1, case 0; else 1
     ~*x  iterator: vx must be of the form
          ("str0" "str1" "str2" "str3" lst . a);
          if lst is initially empty, format "str0" under a+; otherwise,
          bind #\* successively to the elements of lst and then
          recursively format "stri" under a+, where i=1 if there is one
          element left to process, i=2 if there are two left, and i=3
          otherwise.
     ~&x  print elements of vx with ~x, separated by commas and a
          final ``and''
     ~vx  print elements of vx with ~x, separated by commas and a
          final ``or''
     ~nx  if vx is a small positive integer, print it as a word, e.g.,
          seven;
          if vx is a singleton containing a small positive integer, print
            the corresponding ordinal as a word, e.g., seventh
     ~Nx  like ~nx but the word is capitalized, e.g., Seven or Seventh
     ~tx  tab out to column vx; newline first if at or past column vx
     ~cx  vx is (n . w), print integer n right justified in field of
          width w
     ~fx  print object vx flat over as many lines as necessary
     ~Fx  same as ~f, except that subsequent lines are indented to
          start one character to the right of the first character printed
     ~sx  if vx is a symbol, print vx, breaking on hyphens; if vx is a
          string, print the characters in it, breaking on hyphens; else
          vx is a number, to be printed using the current print-base
     ~    tilde space: print a space
     ~_x  print vx spaces
     ~
          tilde newline: skip following whitespace
     ~%   output a newline
     ~|   output a newline unless already on left margin
     ~~   print a tilde
     ~-   if close to rightmargin, output a hyphen and newline; else
          skip this char

If x is a character, then vx is the value of #\x under the current
alist.  When we say "format str under a+" we mean recursively process
the given string under an alist obtained by appending a to the current
alist.

Note:  ~p, ~q, ~P, and ~Q are also currently supported, but are
deprecated.  These are respectively the same as ~x, ~y, ~X, and ~Y,
except that their arguments are expected to be terms, preferably
untranslated (user-level) terms, that could be printed using infix
notation in certain environments.  Infix printing is not currently
supported but may be if there is sufficient need for it.

ACL2's formatting functions print to the indicated channel, keeping
track of which column they are in.  Fmt1 can be used if the caller
knows which column the channel is in (i.e., how many characters have
been printed since the last newline).  Otherwise, fmt or fms must be
used, both of which output a newline so as to establish the column
position at 0.  Unlike Common Lisp's format routine, fmt and its
relatives break the output into lines so as to try to avoid printing
past column 77.  That number is built-into the definitions of ACL2's
formatting functions.  Line breaks are automatically inserted as
necessary in place of spaces and after hyphens in the text being
printed.

The formatting functions scan the string from left to right, printing
each successive character unless it is a tilde (~).  Upon encountering
tildes the formatters take action determined by the character or
characters immediately following the tilde.  The typical
tilde-directive is a group of three successive characters from the
string being printed.  For example, ~x0 is a 3 character
tilde-directive.  The first character in a tilde-directive is always
the tilde character itself.  The next character is called the "command"
character.  The character after that is usually taken as the name of a
"format variable" that is bound in the alist under which the string is
being printed.  Format variables are, by necessity, characters.  The
objects actually printed by a tilde-directive are the objects obtained
by looking up the command's format variables in the alist.  Typical
format variable names are 0, 1, 2, ..., 9, a, b, c, etc., and if a
tilde-directive uses the format variable 0, as in ~x0, then the
character #\0 must be bound in the alist.  Some tilde commands take no
arguments and others take more than one, so some directives are of
length two and others are longer.

It should be noted that this use of characters in the string to denote
arguments is another break from Common Lisp's format routine.  In
Common Lisp, the directives refer implicitly to the "next item to be
printed."  But in ACL2 the directives name each item explicitly with
our format variables.

The following text contains examples that can be evaluated.  To make
this process easier, we use a macro which is defined as part of ACL2
just for this documentation.  The macro is named fmx and it takes up to
eleven arguments, the first of which is a format string, str, and the
others of which are taken as the values of format variables.  The
variables used are #\0 through #\9.  The macro constructs an
appropriate alist, a, and then evaluates (fmt str a *standard-co* state
nil).

Thus,

     (fmx "Here is v0, ~x0, and here is v1, ~x1."
          (cons 'value 0)
          (cons 'value 1))

is just an abbreviation for

     (fmt "Here is v0, ~x0, and here is v1, ~x1."
          (list (cons #\0 (cons 'value 0))
                (cons #\1 (cons 'value 1)))
          *standard-co*
          state
          nil)

which returns (mv 53 state) after printing the line

        Here is v0, (VALUE . 0), and here is v1, (VALUE . 1).

We now devote special attention to three of the tilde-directives whose
use is non-obvious.

_The Case Statement_

~#x is essentially a "case statement" in the language of fmt.  The
proper form of the statement is

     ~#x~[case-0~/case-1~/ ... ~/case-k~],

where each of the case-i is a format string.  In the most common use,
the variable x has an integer value, vx, between 0 and k, inclusive.
The effect of formatting the directive is to format case-vx.

For example

     (fmx "Go ~#0~[North~/East~/South~/West~].~%" 1)

will print "Go East." followed by a newline and will return

(mv 0 state), while if you change the 1 above to 3 (the maximum legal
value), it will print "Go West."

In order to make it easier to print such phrases as "there are seven
cases" requiring agreement between subject and verb based on the number
of elements of a list, the case statement allows its variable to take a
list as its value and selects case-0 if the list has length 1 and
case-1 otherwise.

     (let ((cases '(a b c)))
       (fmx "There ~#0~[is ~n1 case~/are ~n1 cases~]."
            cases
            (length cases)))

will print "There are three cases." but if you change the

'(a b c) above simply to '(a) it will print "There is one case." and if
you change it to nil it will print "There are zero cases."

_Indirection_

Roughly speaking, ~@ will act as though the value of its argument is a
format string and splice it into the current string at the current
position.  It is often used when the phrase to be printed must be
computed.  For example,

     (let ((ev 'DEFUN))
      (fmx "~x0 is an event~@1."
           'foo
           (if (member-eq ev '(defun defstub encapsulate))
               " that may introduce a function symbol"
               "")))

will print "foo is an event that may introduce a function symbol," but
if the value of ev is changed from 'defun to 'defthm, it prints "foo is
an event."  The ~@ directive "splices" in the computed phrase (which
might be empty).  Of course, this particular example could be done with
the case statement

     ~#1~[~/ that may introduce a function symbol~]

where the value of #\1 is appropriately computed to be 0 or 1.

If the argument to ~@ is a pair, it is taken to be a format string
consed onto an alist, i.e., ("str" . a), and the alist, a, is used to
extend the current one before "str" is recursively processed.  This
feature of fmt can be used to pass around "phrases" that contain
computed contextual information in a.  The most typical use is as
"error messages."  For example, suppose you are writing a function
which does not have access to state and so cannot print an error
message.  It may nevertheless be necessary for it to signal an error to
its caller, say by returning two results, the first of which is
interpreted as an error message if non-nil.  Our convention is to use a
~@ pair to represent such messages.  For example, the error value might
be produced by the code:

     (cons
       "Error:  The instruction ~x0 is illegal when the stack is ~x1.~%"
       (list (cons #\0 (current-instruction st))
             (cons #\1 (i-stack st))))

If the current-instruction and i-stack (whatever they are) are '(popi
3) and '(a b) when the cons above is evaluated, then it produces

     '("Error:  The instruction ~x0 is illegal when the stack is ~x1.~%"
       (#\0 POPI 3)
       (#\1 A B))

and if this pair is made the value of the fmt variable 0, then ~@0 will
print

        Error:  The instruction (POPI 3) is illegal when the stack is (A B).

For example, evaluate

     (let
      ((pair
       '("Error:  The instruction ~x0 is illegal when the stack is ~x1.~%"
         (#\0 POPI 3)
         (#\1 A B))))
      (fmx "~@0" pair)).

Thus, even though the function that produced the "error" could not
print it, it could specify exactly what error message and data are to
be printed.

This example raises another issue.  Sometimes it is desirable to break
lines in your format strings so as to make your source code more
attractive.  That is the purpose of the tilde-newline directive.  The
following code produces exactly the same output as described above.

     (let ((pair '("Error:  The instruction ~x0 ~
                   is illegal when the stack is ~
                   ~x1.~%"
                   (#\0 POPI 3)
                   (#\1 A B))))
      (fmx "~@0" pair)).

Finally, observe that when ~@0 extends the current alist, alist, with
the one, a, in its argument, the bindings from a are added to the front
of alist, overriding the current values of any shared variables.  This
ensures that the variable values seen by the recursively processed
string, "str", are those from a, but if "str" uses variables not bound
in a, their values are as specified in the original alist.
Intuitively, variables bound in a are local to the processing of ("str"
. a) but "str" may use "global variables."  The example above
illustrates this because when the ~@0 is processed, #\0 is bound to the
error message pair.  But when the ~x0 in the error string is processed,
#\0 is bound to the illegal instruction.

_Iteration_

The ~* directive is used to process each element of a list.  For
example,

     (let ((lst '(a b c d e f g h))) ; a true-list whose elements we exhibit
      (fmx "~*0"
           `("Whoa!"          ; what to print if there's nothing to print
             "~x*!"           ; how to print the last element
             "~x* and "       ; how to print the 2nd to last element
             "~x*, "          ; how to print all other elements
             ,lst)))          ; the list of elements to print

will print "A, B, C, D, E, F, G and H!".  Try this example with other
true list values of lst, such as '(a b), '(a), and nil.  The
tilde-directives ~&0 and ~v0, which take a true list argument and
display its elements separated by commas and a final "and" or "or," are
implemented in terms of the more general ~*.

The ~* directive allows the 5-tuple to specify in its final cdr an
alist with which to extend the current one before processing the
individual elements.

We often use ~* to print a series of phrases, separated by suitable
punctuation, whitespace and noise words.  In such use, the ~* handles
the separation of the phrases and each phrase is generally printed by
~@.

Here is a complex example.  In the let*, below, we bind phrases to a
list of ~@ pairs and then we create a ~* 5-tuple to print out the
conjunction of the phrases with a parenthetical "finally!" if the
series is longer than 3.

     (let* ((phrases
             (list (list "simplifying with the replacement rules ~&0"
                         (cons #\0 '(rewrite-rule1
                                     rewrite-rule2
                                     rewrite-rule3)))
                   (list "destructor elimination using ~x0"
                         (cons #\0 'elim-rule))
                   (list "generalizing the terms ~&0"
                         (cons #\0 '((rev x) (app u v))))
                   (list "inducting on ~x0"
                         (cons #\0 'I))))
            (5-tuple
             (list
              "magic"                            ; no phrases
              "~@*"                              ; last phrase
              "~@*, and~#f~[~/ (finally!)~] "    ; second to last phrase
              "~@*, "                            ; other phrases
              phrases                            ; the phrases themselves
              (cons #\f
                    (if (>(length phrases) 3) 1 0))))) ;print ``finally''?
       (fmx "We did it by ~*0." 5-tuple))

This let* prints

        We did it by simplifying with the replacement rules REWRITE-RULE1,
        REWRITE-RULE2 and REWRITE-RULE3, destructor elimination using ELIM-
        RULE, generalizing the terms (REV X) and (APP U V), and (finally!)
        inducting on I.

You might wish to try evaluating the let* after removing elements of
phrases.

Most of the output produced by ACL2 is produced via fmt statements.
Thus, inspection of the source code will yield many examples.  A
complicated example is the code that explains the simplifier's work.
See :pc simplify-clause-msg1.  An ad hoc example is provided by the
function fmt-doc-example, which takes two arguments: an arbitrary true
list and state.  To see how fmt-doc-example works, :pe fmt-doc-example.

     (fmt-doc-example '(a b c d e f g h i j k l m n o p) state)

will produce the output

        Here is a true list:  (A B C D E F G H I J K L M N O P).  It has 16
        elements, the third of which is C.

        We could print each element in square brackets:
        ([A], [B], [C], [D], [E], [F], [G], [H], [I], [J], [K], [L], [M], [N],
        [almost there: O], [the end: P]).  And if we wished to itemize them
        into column 15 we could do it like this
        0123456789012345
            0 (zeroth) A
            1 (first)  B
            2 (second) C
            3 (third)  D
            4 (fourth) E
            5 (fifth)  F
            6 (sixth)  G
            7 (seventh)
                       H
            8 (eighth) I
            9 (ninth)  J
           10 (tenth)  K
           11 (eleventh)
                       L
           12 (twelfth)
                       M
           13 (thirteenth)
                       N
           14 (14th)   O
           15 (15th)   P
        End of example.

and return (mv 15 state).

Finally, we should remind the reader that fmt and its subfunctions,
most importantly fmt0, are written entirely in ACL2.  We make this
comment for two reasons.  First, it illustrates the fact that quite low
level code can be efficiently written in the language.  Second, it
means that as a last resort for documentation purposes you can read the
source code without changing languages.

FMT!    :(str alist co-channel state evisc) => state

This function is nearly identical to fmt; see FMT.  The only
difference is that fmt may insert backslash (\) characters when forced
to print past the right margin in order to make the output a bit
clearer in that case.  Use fmt! instead if you want to be able to read
the forms back in.

FMT-TO-COMMENT-WINDOW    print to the comment window

See CW for an introduction to the comment window and the usual
way to print it.

Function fmt-to-comment-window is identical to fmt1 (see FMT),
except that the channel is in essence *standard-co* and the ACL2 state
is neither an input nor an output.  An analogous function,
fmt-to-comment-window!, prints with fmt! instead of fmt, in order to
avoid insertion of backslash (\) characters for margins; also see
CW!.

     General Form:
     (fmt-to-comment-window fmt-string alist col evisc-tuple)

where these arguments are as desribed for fmt1; see FMT.

FMT1    :(str alist col co-channel state evisc) => (mv col state)

See FMT for further explanation, including documentation of the
tilde-directives.

FMT1!    :(str alist col channel state evisc) => (mv col state)

This function is nearly identical to fmt1; see FMT1.  The only
difference is that fmt1 may insert backslash (\) characters when forced
to print past the right margin in order to make the output a bit
clearer in that case.  Use fmt1! instead if you want to be able to read
the forms back in.

FOURTH    fourth member of the list

See any Common Lisp documentation for details.

GETENV$    read an environment variable

(Getenv$ str state), where str is a string, reads the value of
environment variable str, returning nil if none is found or if the read
fails.  The formal story is that getenv$ reads its value from the
oracle field of the ACL2 state.  The return value is thus a triple of
the form (mv erp val state), where erp will always be nil in practice,
val is the value that has been read, and state is the new state, which
is obtained by popping val from the top of the state's oracle.

     Example:
     (getenv$ "PWD" state) ==> (mv nil "/u/joe/work" state)

Also see SETENV$.

GETPROP    access fast property lists

     General form:
     (getprop symb key default world-name world-alist)

See books/misc/getprop.lisp for an example that illustrates the use of
ACL2 utilities getprop and putprop to take advantage of under-the-hood
Lisp (hashed) property lists.

HARD-ERROR    print an error message and stop execution

(Hard-error ctx str alist) causes evaluation to halt with a short
message using the "context" ctx.  An error message is first printed
using the string str and alist alist that are of the same kind as
expected by fmt.  See FMT.  Also see ER for a macro
that provides a unified way of signaling errors.

Hard-error has a guard of t.  Also see ILLEGAL for a similar
capability which however has a guard of nil that supports static
checking using guard verification, rather than using dynamic (run-time)
checking.   This distinction is illustrated elsewhere: see
PROG2$ for examples.

Semantically, hard-error ignores its arguments and always returns nil.
But if a call (hard-error ctx str alist) is encountered during
evaluation, then the string str is printed using the association list
alist (as in fmt), after which evaluation halts immediately.  Here is a
trivial, contrived example.

     ACL2 !>(cons 3 (hard-error 'my-context
                                 "Printing 4: ~n0"
                                 (list (cons #\0 4))))

     HARD ACL2 ERROR in MY-CONTEXT:  Printing 4: four

     ACL2 Error in TOP-LEVEL:  Evaluation aborted.

     ACL2 !>

IDENTITY    the identity function

(Identity x) equals x; what else can we say?

Identity is a Common Lisp function.  See any Common Lisp documentation
for more information.

IF    if-then-else function

(if x y z) is equal to y if x is any value other than nil, and is equal
to z if x is nil.

Only one of y, z is evaluated when (if x y z) is evaluated.

If has a guard of t.

If is part of Common Lisp.  See any Common Lisp documentation for more
information.

IFF    logical "if and only if"

Iff is the ACL2 biconditional, "if and only if".  (iff P Q) means that
either P and Q are both false (i.e., nil) or both true (i.e., not nil).

IFIX    coerce to an integer

Ifix simply returns any integer argument unchanged, returning 0 on a
non-integer argument.  Also see NFIX, see RFIX, see
REALFIX and see FIX for analogous functions that coerce
to a natural number, a rational number, a real, and a number,
respectively.

Ifix has a guard of t.

IGNORABLE    See DECLARE.

IGNORE    See DECLARE.

ILLEGAL    print an error message and stop execution

(Illegal ctx str alist) causes evaluation to halt with a short message
using the "context" ctx.  An error message is first printed using the
string str and alist alist that are of the same kind as expected by
fmt.  See FMT, and see PROG2$ for an example of how to
use a related function, hard-error (see HARD-ERROR).  Also see
ER for a macro that provides a unified way of signaling errors.

The difference between illegal and hard-error is that the former has a
guard of nil while the latter has a guard of t.  Thus, you may want to
use illegal rather than hard-error when you intend to do guard
verification at some point, and you expect the guard to guarantee that
the illegal call is never executed.  See PROG2$ for an example.

IMAGPART    imaginary part of a complex number

Completion Axiom:

     (equal (imagpart x)
            (if (acl2-numberp x)
                (imagpart x)
              0))

Guard for (imagpart x):

     (acl2-numberp x)

IMPLIES    logical implication

Implies is the ACL2 implication function.  (implies P Q) means that
either P is false (i.e., nil) or Q is true (i.e., not nil).

IMPROPER-CONSP    recognizer for improper (non-null-terminated) non-empty lists

Improper-consp is the function that checks whether its argument is a
non-empty list that ends in other than nil.  See PROPER-CONSP
and also see TRUE-LISTP.

INT=    test equality of two integers

(int= x y) is logically equivalent to (equal x y).

Unlike equal, int= requires its arguments to be numbers (or else causes
a guard violation; see GUARD).  Generally, int= is executed
more efficiently than equal or = on integers.

INTEGER-LENGTH    number of bits in two's complement integer representation

For non-negative integers, (integer-length i) is the minimum number of
bits needed to represent the integer.  Any integer can be represented
as a signed two's complement field with a minimum of (+ (integer-length
i) 1) bits.

The guard for integer-length requires its argument to be an integer.
Integer-length is defined in Common Lisp.  See any Common Lisp
documentation for more information.

INTEGER-LISTP    recognizer for a true list of integers

The predicate integer-listp tests whether its argument is a true list
of integers.

INTEGERP    recognizer for whole numbers

(integerp x) is true if and only if x is an integer.

INTERN    create a new symbol in a given package

(intern symbol-name symbol-package-name) returns a symbol with the
given symbol-name and the given symbol-package-name.  We restrict
Common Lisp's intern so that the second argument is either the symbol
*main-lisp-package-name*, the value of that constant, or is one of
"ACL2", "ACL2-INPUT-CHANNEL", "ACL2-OUTPUT-CHANNEL", or "KEYWORD".  To
avoid that restriction, see INTERN$.

In ACL2 intern is actually implemented as a macro that expands to a
call of a similar function whose second argument is a symbol.  Invoke
:pe intern to see the definition, or see
INTERN-IN-PACKAGE-OF-SYMBOL.

To see why is intern so restricted consider (intern "X" "P").  In
particular, is it a symbol and if so, what is its symbol-package-name?
One is tempted to say "yes, it is a symbol in the package "P"."  But if
package "P" has not yet been defined, that would be premature because
the imports to the package are unknown.  For example, if "P" were
introduced with

     (defpkg "P" '(LISP::X))

then in Common Lisp (symbol-package-name (intern "X" "P")) returns
"LISP".

The obvious restriction on intern is that its second argument be the
name of a package known to ACL2.  We cannot express such a restriction
(except, for example, by limiting it to those packages known at some
fixed time, as we do).  Instead, we provide intern-in-package-of-symbol
which requires a "witness symbol" for the package instead of the
package.  The witness symbol is any symbol (expressible in ACL2) and
uniquely specifies a package necessarily known to ACL2.

INTERN$    create a new symbol in a given package

Intern$ is a macro that behaves the same as the macro intern, except
for weakening the restriction to a fixed set of package names so that
any package name other than "" is legal.  See INTERN.  Note
that if you evaluate a call (intern$ x y) for which there is no package
with name y that is known to ACL2, you will get an error.

(Intern$ x y) expands to:

     (intern-in-package-of-symbol x (pkg-witness y))

See INTERN-IN-PACKAGE-OF-SYMBOL and see PKG-WITNESS.

INTERN-IN-PACKAGE-OF-SYMBOL    create a symbol with a given name

Completion Axiom:

     (equal (intern-in-package-of-symbol x y)
            (if (and (stringp x)
                     (symbolp y))
                (intern-in-package-of-symbol x y)
              nil))

Guard for (intern-in-package-of-symbol x y):

     (and (stringp x) (symbolp y))

Intuitively, (intern-in-package-of-symbol x y) creates a symbol with
symbol-name x interned in the package containing y.  More precisely,
suppose x is a string, y is a symbol with symbol-package-name pkg and
that the defpkg event creating pkg had the list of symbols imports as
the value of its second argument.  Then (intern-in-package-of-symbol x
y) returns a symbol, ans, the symbol-name of ans is x, and the
symbol-package-name of ans is pkg, unless x is the symbol-name of some
member of imports with symbol-package-name ipkg, in which case the
symbol-package-name of ans is ipkg.  Because defpkg requires that there
be no duplications among the symbol-names of the imports,
intern-in-package-of-symbol is uniquely defined.

For example, suppose "MY-PKG" was created by

     (defpkg "MY-PKG" '(ACL2::ABC LISP::CAR)).

Let w be 'my-pkg::witness.  Observe that

     (symbolp w) is t                     ; w is a symbol
     (symbol-name w) is "WITNESS"         ; w's name is "WITNESS"
     (symbol-package-name w) is "MY-PKG"  ; w is in the package "MY-PKG"

The construction of w illustrates one way to obtain a symbol in a given
package:  write it down as a constant using the double-colon notation.

But another way to obtain a symbol in a given package is to create it
with intern-in-package-of-symbol.

     (intern-in-package-of-symbol "XYZ" w) is MY-PKG::XYZ

     (intern-in-package-of-symbol "ABC" w) is ACL2::ABC

     (intern-in-package-of-symbol "CAR" w) is LISP::CAR

     (intern-in-package-of-symbol "car" w) is MY-PKG::|car|

INTERSECTP    test whether two lists of eqlablep objects intersect

See INTERSECTP-EQUAL, which is logically the same function.

(Intersectp x y) has a guard that x and y are lists containing only
numbers, symbols, and characters.

INTERSECTP-EQ    test whether two lists of symbols intersect

See INTERSECTP-EQUAL, which is logically the same function.

(Intersectp-eq x y) has a guard that x and y are lists of symbols.

INTERSECTP-EQUAL    test whether two lists intersect

(Intersectp-equal x y) returns t if x and y have a member in common,
else it returns nil.  Also see INTERSECTP-EQ, which is
logically the same but can be more efficient since it uses eq instead
of equal to look for members common to the two given lists.

(Intersectp-equal x y) has a guard that x and y are true lists.

IRRELEVANT-FORMALS    formals that are used but only insignificantly

Let fn be a function of n arguments.  Let x be the ith formal of fn.
We say x is "irrelevant in fn" if x is not involved in either the guard
or the measure for fn, x is used in the body, but the value of (fn
a1...ai...an) is independent of ai.

The easiest way to define a function with an irrelevant formal is
simply not to use the formal in the body of the function.  Such formals
are said to be "ignored" by Common Lisp and a special declaration is
provided to allow ignored formals.  ACL2 makes a distinction between
ignored and irrelevant formals.  Note however that if a variable is
declared ignored or ignorable, then it will not be reported as
irrelevant.

An example of an irrelevant formal is x in the definition of fact below.

     (defun fact (i x)
       (declare (xargs :guard (and (integerp i) (<= 0 i))))
       (if (zerop i) 0 (* i (fact (1- i) (cons i x))))).

Observe that x is only used in recursive calls of fact; it never "gets
out" into the result.  ACL2 can detect some irrelevant formals by a
closure analysis on how the formals are used.  For example, if the ith
formal is only used in the ith argument position of recursive calls,
then it is irrelevant.  This is how x is used above.

It is possible for a formal to appear only in recursive calls but still
be relevant.  For example, x is *not* irrelevant below, even though it
only appears in the recursive call.

     (defun fn (i x) (if (zerop i) 0 (fn x (1- i))))

The key observation above is that while x only appears in a recursive
call, it appears in an argument position, namely i's, that is relevant.
(The function above can be admitted with a :guard requiring both
arguments to be nonnegative integers and the :measure (+ i x).)

Establishing that a formal is irrelevant, in the sense defined above,
can be an arbitrarily hard problem because it requires theorem proving.
For example, is x irrelevant below?

     (defun test (i j k x) (if (p i j k) 0 x))

Note that the value of (test i j k x) is independent of x -- thus
making x irrelevant -- precisely if (p i j k) is a theorem.  ACL2's
syntactic analysis of a definition does not guarantee to notice all
irrelevant formals.

We regard the presence of irrelevant formals as an indication that
something is wrong with the definition.  We cause an error on such
definitions and suggest that you recode the definition so as to
eliminate the irrelevant formals.  If you must have an irrelevant
formal, one way to "trick" ACL2 into accepting the definition, without
slowing down the execution of your function, is to use the formal in an
irrelevant way in the guard.  For example, to admit fact, above, with
its irrelevant x one might use

     (defun fact (i x)
       (declare (xargs :guard (and (integerp i) (<= 0 i) (equal x x))))
       (if (zerop i) 0 (* i (fact (1- i) (cons i x)))))

For those who really want to turn off this feature, we have provided a
way to use the acl2-defaults-table for this purpose; see
SET-IRRELEVANT-FORMALS-OK.

KEYWORD-VALUE-LISTP    recognizer for true lists whose even-position elements are keywords

(keyword-value-listp l) is true if and only if l is a list of even
length of the form (k1 a1 k2 a2 ... kn an), where each ki is a keyword.

KEYWORDP    recognizer for keywords

(Keywordp x) is true if and only if x is a keyword, i.e., a symbol in
the "KEYWORD" package.  Such symbols are typically printed using a colon
(:) followed by the symbol-name of the symbol.

Keywordp has a guard of t.

Keywordp is a Common Lisp function.  See any Common Lisp documentation
for more information.  The following log may be illuminating.

     ACL2 !>(intern "ABC" "KEYWORD")
     :ABC
     ACL2 !>(symbol-name ':ABC)
     "ABC"
     ACL2 !>(symbol-package-name ':ABC)
     "KEYWORD"
     ACL2 !>

KWOTE    quote an arbitrary object

For any object x, (kwote x) returns the two-element list whose elements
are the symbol quote and the given x, respectively.  The guard of
(kwote x) is t.

KWOTE-LST    quote an arbitrary true list of objects

The function kwote-lst applies the function kwote to each element of a
given list.  The guard of (kwote-lst lst) is (true-listp lst).

LAST    the last cons (not element) of a list

(Last l) is the last cons of a list.  Here are examples.

     ACL2 !>(last '(a b . c))
     (B . C)
     ACL2 !>(last '(a b c))
     (C)

(Last l) has a guard of (listp l); thus, l need not be a true-listp.

Last is a Common Lisp function.  See any Common Lisp documentation for
more information.  Unlike Common Lisp, we do not allow an optional
second argument for last.

LEN    length of a list

Len returns the length of a list.

A Common Lisp function that is appropriate for both strings and proper
lists is length; see LENGTH.  The guard for len is t.

(Low-level implementation note.  ACL2 provides a highly-optimized
implementation of len, which is tail-recursive and fixnum-aware, that
differs from its simple ACL2 definition.)

LENGTH    length of a string or proper list

Length is the function for determining the length of a sequence.  In
ACL2, the argument is required to be either a true-listp or a string.

Length is a Common Lisp function.  See any Common Lisp documentation
for more information.

LET    binding of lexically scoped (local) variables

     Example LET Form:
     (let ((x (* x x))
           (y (* 2 x)))
      (list x y))

If the form above is executed in an environment in which x has the
value -2, then the result is '(4 -4).

Let expressions bind variables so that their "local" values, the values
they have when the "body" of the let is evaluated, are possibly
different than their "global" values, the values they have in the
context in which the let expression appears.  In the let expression
above, the local variables bound by the let are x and y.  They are
locally bound to the values delivered by the two forms (* x x) and (* 2
x), respectively, that appear in the "bindings" of the let.  The body
of the let is (list x y).

Suppose that the let expression above occurs in a context in which x
has the value -2.  (The global value of y is irrelevant to this
example.)  For example, one might imagine that the let form above
occurs as the body of some function, fn, with the formal parameter x
and we are evaluating (fn -2).

To evaluate the let above in a context in which x is -2, we first
evaluate the two forms specifying the local values of the variables.
Thus, (* x x) is evaluated and produces 4 (because x is -2) and (* 2 x)
is evaluated and produces -4 (because x is -2).  Then x and y are bound
to these values and the body of the let is evaluated.  Thus, when the
body, (list x y) is evaluated, x is 4 and y is -4.  Thus, the body
produces '(4 -4).

Note that the binding of y, which is written after the binding of x and
which mentions x, nevertheless uses the global value of x, not the new
local value.  That is, the local variables of the let are bound "in
parallel" rather than "sequentially." In contrast, if the

     Example LET* Form:
     (let* ((x (* x x))
            (y (* 2 x)))
      (list x y))

is evaluated when the global value of x is -2, then the result is '(4
8), because the local value of y is computed after x has been bound to
4.  Let* binds its local variables "sequentially."

     General LET Forms:
     (let ((var1 term1) ... (varn termn)) body)
     and
     (let ((var1 term1) ... (varn termn))
      (declare ...) ... (declare ...)
      body)

where the vari are distinct variables, the termi are terms involving
only variables bound in the environment containing the let, and body is
a term involving only the vari plus the variables bound in the
environment containing the let.  Each vari must be used in body or else
declared ignored.

A let form is evaluated by first evaluating each of the termi,
obtaining for each a vali.  Then, each vari is bound to the
corresponding vali and body is evaluated.

Actually, let forms are just abbreviations for certain uses of lambda
notation.  In particular

     (let ((var1 term1) ... (varn termn)) (declare ...) body)

is equivalent to

     ((lambda (var1 ... varn)
        (declare ...)
        body)
      term1 ... termn).

Let* forms are used when it is desired to bind the vari sequentially,
i.e., when the local values of preceding varj are to be used in the
computation of the local value for vari.

     General LET* Forms:
     (let* ((var1 term1) ... (varn termn)) body)
     and
     (let* ((var1 term1) ... (varn termn))
      (declare (ignore x1 ... xm))
      body)

where the vari are variables (not necessarily distinct), the termi are
terms involving only variables bound in the environment containing the
let* and those varj such that j<i, and body is a term involving only
the vari plus the variables bound in the environment containing the
let*.  Each vari must be used either in some subsequent termj or in
body, except that in the second form above we make an exception when
vari is among the xk, in which case vari must not be thus used.  Note
that let* does not permit the inclusion of any declare forms other than
one as shown above.  In the second general form above, every xk must be
among the vari, and furthermore, xk may not equal vari and varj for
distinct i, j.

The first let* above is equivalent to

     (let ((var1 term1))
      ...
      (let ((varn termn)) body)...)

Thus, the termi are evaluated successively and after each evaluation
the corresponding vali is bound to the value of termi.  The second let*
is similarly expanded, except that each for each vari that is among the
(x1 ... xm), the form (declare (ignore vari)) is inserted immediately
after (vari termi).

Each (vari termi) pair in a let or let* form is called a "binding" of
vari and the vari are called the "local variables" of the let or let*.
The common use of let and let* is to save the values of certain
expressions (the termi) so that they may be referenced several times in
the body without suggesting their recomputation.

Let is part of Common Lisp.  See any Common Lisp documentation for more
information.

LET*    binding of lexically scoped (local) variables

     Example LET* Forms:
     (let* ((x (* x x))
            (y (* 2 x)))
      (list x y))

     (let* ((x (* x x))
            (y (* 2 x))
            (x (* x y))
            (a (* x x)))
      (declare (ignore a))
      (list x y))

If the forms above are executed in an environment in which x has the
value -2, then the respective results are '(4 8) and '(32 8).  See
LET for a discussion of both let and let*, or read on for a
briefer discussion.

The difference between let and let* is that the former binds its local
variables in parallel while the latter binds them sequentially.  Thus,
in let*, the term evaluated to produce the local value of one of the
locally bound variables is permitted to reference any locally bound
variable occurring earlier in the binding list and the value so
obtained is the newly computed local value of that variable.  See
LET.

In ACL2 the only declare forms allowed for a let* form are ignore,
ignorable, and type.  See DECLARE.  Moreover, no variable
declared ignored or ignorable may be bound more than once.  A variable
with a type declaration may be bound more than once, in which case the
type declaration is treated by ACL2 as applying to each binding
occurrence of that variable.  It seems unclear from the Common Lisp spec
whether the underlying Lisp implementation is expected to apply such a
declaration to more than one binding occurrence, however, so
performance in such cases may depend on the underlying Lisp.

Let* is a Common Lisp macro.  See any Common Lisp documentation for
more information.

LEXORDER    total order on ACL2 objects

Lexorder is a non-strict total order, a "less than or equal," on ACL2
objects.  Also see ALPHORDER, the restriction of lexorder to
atoms; the notion of "non-strict total order" is defined there.

Lexorder has a guard of t.

For lexorder, an atom and a cons are ordered so that the atom comes
first, and two conses are ordered so that the one with the recursively
smaller car comes first, with the cdrs being compared only if the cars
are equal.   Lexorder compares two atoms by using alphorder.

LIST    build a list

List is the macro for building a list of objects.  For example, (list 5
6 7) returns a list of length 3 whose elements are 5, 6, and 7
respectively.  Also see LIST*.

List is defined in Common Lisp.  See any Common Lisp documentation for
more information.

LIST*    build a list

List* is the Common Lisp macro for building a list of objects from
given elements and a tail.  For example, (list* 5 6 '(7 8 9)) equals
the list '(5 6 7 8 9).  Also see LIST.

List* is a Common Lisp function.  See any Common Lisp documentation for
more information.

LISTP    recognizer for (not necessarily proper) lists

(listp x) is true when x is either a cons pair or is nil.

Listp has no guard, i.e., its guard is t.

Listp is a Common Lisp function.  See any Common Lisp documentation for
more information.

LOGAND    bitwise logical `and' of zero or more integers

When integers are viewed in their two's complement representation,
logand returns their bitwise logical `and'.  In ACL2 logand is a macro
that expands into calls of the binary function binary-logand, except
that (logand) expands to -1 and (logand x) expands to x.

The guard for binary-logand requires its arguments to be integers.
Logand is defined in Common Lisp.  See any Common Lisp documentation
for more information.

LOGANDC1    bitwise logical `and' of two ints, complementing the first

When integers are viewed in their two's complement representation,
logandc1 returns the bitwise logical `and' of the second with the
bitwise logical `not' of the first.

The guard for logandc1 requires its arguments to be integers.  Logandc1
is defined in Common Lisp.  See any Common Lisp documentation for more
information.

LOGANDC2    bitwise logical `and' of two ints, complementing the second

When integers are viewed in their two's complement representation,
logandc2 returns the bitwise logical `and' of the first with the
bitwise logical `not' of the second.

The guard for logandc2 requires its arguments to be integers.  Logandc2
is defined in Common Lisp.  See any Common Lisp documentation for more
information.

LOGBITP    the ith bit of an integer

For a nonnegative integer i and an integer j, (logbitp i j) is the
value of the ith bit in the two's complement representation of j.

(Logbitp i j) has a guard that i is a nonnegative integer and j is an
integer.

Logbitp is a Common Lisp function.  See any Common Lisp documentation
for more information.

LOGCOUNT    number of "on" bits in a two's complement number

(Logcount x) is the number of "on" bits in the two's complement
representation of x.

(Logcount x) has a guard of (integerp x).

Logcount is a Common Lisp function.  See any Common Lisp documentation
for more information.

LOGEQV    bitwise logical equivalence of zero or more integers

When integers are viewed in their two's complement representation,
logeqv returns their bitwise logical equivalence.  In ACL2 logeqv is a
macro that expands into calls of the binary function binary-logeqv,
except that (logeqv) expands to -1 and (logeqv x) expands to x.

The guard for binary-logeqv requires its arguments to be integers.
Logeqv is defined in Common Lisp.  See any Common Lisp documentation
for more information.

LOGIOR    bitwise logical inclusive or of zero or more integers

When integers are viewed in their two's complement representation,
logior returns their bitwise logical inclusive or.  In ACL2 logior is a
macro that expands into calls of the binary function binary-logior,
except that (logior) expands to 0 and (logior x) expands to x.

The guard for binary-logior requires its arguments to be integers.
Logior is defined in Common Lisp.  See any Common Lisp documentation
for more information.

LOGNAND    bitwise logical `nand' of two integers

When integers are viewed in their two's complement representation,
lognand returns their bitwise logical `nand'.

The guard for lognand requires its arguments to be integers.  Lognand
is defined in Common Lisp.  See any Common Lisp documentation for more
information.

LOGNOR    bitwise logical `nor' of two integers

When integers are viewed in their two's complement representation,
lognor returns the bitwise logical `nor' of the first with the second.

The guard for lognor requires its arguments to be integers.  Lognor is
defined in Common Lisp.  See any Common Lisp documentation for more
information.

LOGNOT    bitwise not of a two's complement number

(lognot i) is the two's complement bitwise `not' of the integer i.

Lognot is actually defined by coercing its argument to an integer (see
IFIX), negating the result, and then subtracting 1.

The guard for lognot requires its argument to be an integer.

Lognot is a Common Lisp function.  See any Common Lisp documentation
for more information.

LOGORC1    bitwise logical inclusive or of two ints, complementing the first

When integers are viewed in their two's complement representation,
logorc1 returns the bitwise logical inclusive or of the second with the
bitwise logical `not' of the first.

The guard for logorc1 requires its arguments to be integers.  Logorc1
is defined in Common Lisp.  See any Common Lisp documentation for more
information.

LOGORC2    bitwise logical inclusive or of two ints, complementing the second

When integers are viewed in their two's complement representation,
logorc2 returns the bitwise logical inclusive or of the first with the
bitwise logical `not' of the second.

The guard for logorc2 requires its arguments to be integers.  Logorc2
is defined in Common Lisp.  See any Common Lisp documentation for more
information.

LOGTEST    test if two integers share a `1' bit

When integers x and y are viewed in their two's complement
representation, (logtest x y) is true if and only if there is some
position for which both x and y have a `1' bit in that position.

The guard for logtest requires its arguments to be integers.  Logtest
is defined in Common Lisp.  See any Common Lisp documentation for more
information.

LOGXOR    bitwise logical exclusive or of zero or more integers

When integers are viewed in their two's complement representation,
logxor returns their bitwise logical exclusive or.  In ACL2 logxor is a
macro that expands into calls of the binary function binary-logxor,
except that (logxor) expands to 0 and (logxor x) expands to x.

The guard for binary-logxor requires its arguments to be integers.
Logxor is defined in Common Lisp.  See any Common Lisp documentation
for more information.

LOWER-CASE-P    recognizer for lower case characters

(Lower-case-p x) is true if and only if x is a lower case character,
i.e., a member of the list #A, #B, ..., #Z.

The guard for lower-case-p requires its argument to be a standard
character (see STANDARD-CHAR-P).

Lower-case-p is a Common Lisp function.  See any Common Lisp
documentation for more information.

MAKE-CHARACTER-LIST    coerce to a list of characters

Non-characters in the given list are coerced to the character with code
0.

MAKE-LIST    make a list of a given size

For a nonnegative integer size, (Make-list size) is a list of elements
of length size, each of which is initialized to the :initial-element
(which defaults to nil).

Make-list is a macro in ACL2, defined in terms of a tail recursive
function make-list-ac whose guard requires size to be a nonnegative
integer.  Make-list is a Common Lisp function.  See any Common Lisp
documentation for more information.

MAKE-ORD    a constructor for ordinals.

Make-ord is the ordinal constructor.  Its use is recommended instead of
using cons to make ordinals.  For a discussion of ordinals, see
ORDINALS.

For any ordinal, alpha < epsilon-0, there exist natural numbers p and
n, positive integers x1, x2, ..., xn and ordinals a1 > a2 > ... > an >
0 such that alpha > a1 and alpha = w^(a1)x1 + w^(a2)x2 + ... + w^(an)xn
+ p.  We call a1 the "first exponent", x1 the "first coefficient", and
the remainder (w^(a2)x2 + ... + w^(an)xn + p) the "rest" of alpha.

(Make-ord fe fco rst) corresponds to the ordinal (w^fe)fco + rst.  Thus
the first infinite ordinal, w (omega), is constructed by

     (make-ord 1 1 0)

and, for example, the ordinal (w^2)5 + w2 + 7 is constructed by:

     (make-ord 2 5 (make-ord 1 2 7)) .

The reason make-ord is used rather than cons is that it allows us to
reason more abstractly about the ordinals, without having to worry
about the underlying representation.

MAX    the larger of two numbers

(Max x y) is the larger of the numbers x and y.

The guard for max requires its arguments to be rational (real, in
ACL2(r)) numbers.

Max is a Common Lisp function.  See any Common Lisp documentation for
more information.

MBE    attach code for execution

The macro mbe ("must be equal") can be used in function definitions in
order to cause evaluation to use alternate code to that provided for the
logic.  An example is given below.  However, the use of mbe can lead to
non-terminating computations.  See DEFEXEC, perhaps after
reading the present documentation, for a way to guarantee termination
(at least theoretically).

In the ACL2 logic, (mbe :exec exec-code :logic logic-code) equals
logic-code; the value of exec-code is ignored.  However, in raw Lisp it
is the other way around:  this form macroexpands simply to exec-code.
ACL2's guard verification mechanism ensures that the raw Lisp code is
only evaluated when appropriate, since the guard proof obligations
generated for this call of mbe are (equal exec-code logic-code)
together with the guard proof obligations from exec-code.  See
VERIFY-GUARDS and, for general discussion of guards, see
GUARD.

Warning for nested mbe calls: The equality of :exec and :logic code is
not checked in the scope of superior :logic code, as for the equality
of x and y in the following.

     (mbe :logic
          (mbe :logic x :exec y)
          :exec
          z)

The form (mbe :exec exec-code :logic logic-code) expands in the logic to
the function call (must-be-equal logic-code exec-code).  The guard for
(must-be-equal logic exec) is (equal logic exec).  We recommend that
you use mbe instead of must-be-equal because the use of keywords
eliminates errors caused by unintentially reversing the order of
arguments.  The :exec and the :logic code in an mbe call must have the
same return type; for example, one cannot return (mv * *) while the
other returns just a single value.

Also see MBT, which stands for "must be true."  You may find it
more natural to use mbt for certain applications, as described in its
documentation.

Related topics other than immediate subtopics:

Here is an example of the use of mbe.  Suppose that you want to define
factorial in the usual recursive manner, as follows.

     (defun fact (n)
       (if (zp n)
           1
         (* n (fact (1- n)))))

But perhaps you want to be able to execute calls of fact on large
arguments that cause stack overflows, perhaps during proofs.  (This
isn't a particularly realistic example, but it should serve.)  So,
instead you can define this tail-recursive version of factorial:

     (defun fact1 (n acc)
       (declare (xargs :guard (and (integerp n) (>= n 0) (integerp acc))))
       (if (zp n)
           acc
         (fact1 (1- n) (* n acc))))

We are now ready to define fact using mbe.  Our intention is that
logically, fact is as shown in the first definition above, but that
fact should be executed by calling fact1.  Notice that we defer guard
verification, since we are not ready to prove the correspondence
between fact1 and fact.

     (defun fact (n)
       (declare (xargs :guard (and (integerp n) (>= n 0))
                       :verify-guards nil))
       (mbe :exec  (fact1 n 1)
            :logic (if (zp n)
                       1
                     (* n (fact (1- n))))))

Next, we prove the necessary correspondence lemmas.  Notice the
inclusion of a standard book to help with the arithmetic reasoning.

     (include-book "books/arithmetic/top-with-meta")

     (defthm fact1-fact
       (implies (integerp acc)
                (equal (fact1 n acc)
                       (* acc (fact n)))))

We may now do guard verification for fact, which will allow the
execution of the raw Lisp fact function, where the above mbe call
expands simply to (fact1 n 1).

     (verify-guards fact)

Now that guards have been verified, a trace of function calls
illustrates that the evaluation of calls of fact is passed to
evaluation of calls of fact1.  The outermost call below is of the
logical function stored for the definition of fact; all the others are
of actual raw Common Lisp functions.

     ACL2 !>(trace$ fact fact1)
     NIL
     ACL2 !>(fact 3)
     1> (ACL2_*1*_ACL2::FACT 3)
       2> (FACT 3)
         3> (FACT1 3 1)
           4> (FACT1 2 3)
             5> (FACT1 1 6)
               6> (FACT1 0 6)
               <6 (FACT1 6)
             <5 (FACT1 6)
           <4 (FACT1 6)
         <3 (FACT1 6)
       <2 (FACT 6)
     <1 (ACL2_*1*_ACL2::FACT 6)
     6
     ACL2 !>

You may occasionally get warnings when you compile functions defined
using mbe.  (For commands that invoke the compiler, see
COMPILATION.)  These can be inhibited by using an ignorable declare
form.  Here is a simple but illustrative example.  Note that the
declarations can optionally be separated into two declare forms.

     (defun foo (x y)
       (declare (ignorable x)
                (xargs :guard (equal x y)))
       (mbe :logic x :exec y))

Finally, we observe that when the body of a function contains a term of
the form (mbe :exec exec-code :logic logic-code), the user is very
unlikely to see any logical difference than if this were replaced by
logic-code.  ACL2 takes various steps to ensure this.  For example, the
proof obligations generated for admitting a function treat the above
mbe term simply as logic-code.  Function expansion, :use hints,
:definition rules, generation of constraints for functional
instantiation, and creation of rules of class :rewrite and
:forward-chaining also treat mbe calls as their :logic code.

MBT    introduce a test not to be evaluated

The macro mbt ("must be true") can be used in order to add code in
order to admit function definitions in :logic mode, without paying a
cost in execution efficiency.  Examples below illustrate its intended
use.

Semantically, (mbt x) equals x.  However, in raw Lisp (mbt x) ignores x
entirely, and macroexpands to t.  ACL2's guard verification mechanism
ensures that the raw Lisp code is only evaluated when appropriate,
since a guard proof obligation (equal x t) is generated.  See
VERIFY-GUARDS and, for general discussion of guards, see
GUARD.

Also see MBE, which stands for "must be equal."  Although mbt
is more natural in many cases, mbe has more general applicability.  In
fact, (mbt x) is essentially defined to be (mbe :logic x :exec t).

We can illustrate the use of mbt on the following generic example, where
<g>, <test>, <rec-x>, and <base> are intended to be terms involving
only the variable x.

     (defun foo (x)
       (declare (xargs :guard <g>))
       (if <test>
           (foo <rec-x>)
         <base>))

In order to admit this function, ACL2 needs to discharge the proof
obligation that <rec-x> is smaller than x, namely:

     (implies <test>
              (o< (acl2-count <rec-x>)
                   (acl2-count x)))

But suppose we need to know that <g> is true in order to prove this.
Since <g> is only the guard, it is not part of the logical definition
of foo.  A solution is to add the guard to the definition of foo, as
follows.

     (defun foo (x)
       (declare (xargs :guard <g>))
       (if (mbt <g>)
           (if <test>
               (foo <rec-x>)
             <base>)
         nil))

If we do this using <g> rather than (mbt <g>), then evaluation of every
recursive call of foo will cause the evaluation of (the appropriate
instance of) <g>.  But since (mbt <g>) expands to t in raw Lisp, then
once we verify the guards of foo, the evaluations of <g> will be
avoided (except at the top level, when we check the guard before
allowing evaluation to take place in Common Lisp).

Other times, the guard isn't the issue, but rather, the problem is that
a recursive call has an argument that itself is a recursive call.  For
example, suppose that <rec-x> is of the form (foo <expr>).  There is no
way we can hope to discharge the termination proof obligation shown
above.  A standard solution is to add some version of this test:

     (mbt (o< (acl2-count <rec-x>) (acl2-count x)))

Here is a specific example based on one sent by Vernon Austel.

     (defun recurX2 (n)
       (declare (xargs :guard (and (integerp n) (<= 0 n))
                       :verify-guards nil))
       (cond ((zp n) 0)
             (t (let ((call (recurX2 (1- n))))
                  (if (mbt (< (acl2-count call) n))
                      (recurX2 call)
                    1 ;; this branch is never actually taken
                    )))))

     (defthm recurX2-0
      (equal (recurX2 n) 0))

     (verify-guards recurX2)

If you (trace$ acl2-count), you will see that evaluation of (recurX2 2)
causes several calls of acl2-count before the verify-guards.  But this
evaluation does not call acl2-count after the verify-guards, because
the ACL2 evaluation mechanism uses raw Lisp to do the evaluation, and
the form (mbt (< (acl2-count call) n)) macroexpands to t in Common Lisp.

You may occasionally get warnings when you compile functions defined
using mbt.  (For commands that invoke the compiler, see
COMPILATION.)  These can be inhibited by using an ignorable declare
form.  Here is a simple but illustrative example.  Note that the
declarations can optionally be separated into two declare forms.

     (defun foo (x y)
       (declare (ignorable x)
                (xargs :guard (equal x t)))
       (and (mbt x) y))

MEMBER    membership predicate, using eql as test

(Member x l) equals the longest tail of l that begins with x, or else
nil if no such tail exists.

(Member x l) is provably the same in the ACL2 logic as (member-equal x
l).  It has a stronger guard than member-equal because uses eql to test
for whether x is equal to a given member of l.  Its guard requires that
l is a true list, and moreover, either (eqlablep x) or all members of l
are eqlablep.  See MEMBER-EQUAL and see MEMBER-EQ.

Member is a Common Lisp function.  See any Common Lisp documentation
for more information.  Since ACL2 functions cannot take keyword
arguments (though macros can), the ACL2 functions member-equal and
member-eq are defined to correspond to calls of the Common Lisp
function member whose keyword argument :test is equal or eq,
respectively.

MEMBER-EQ    membership predicate, using eq as test

(Member-eq x lst) equals the longest tail of lst that begins with x, or
else nil if no such tail exists.

(Member-eq x lst) is provably the same in the ACL2 logic as (member x
lst) and (member-equal x lst), but it has a stronger guard because it
uses eq for a more efficient test for whether x is equal to a given
member of lst.  Its guard requires that lst is a true list, and
moreover, either x is a symbol or lst is a list of symbols.  See
MEMBER-EQUAL and see MEMBER.

MEMBER-EQUAL    membership predicate

(Member-equal x lst) equals the longest tail of lst that begins with x,
or else nil if no such tail exists.

(Member-equal x lst) has a guard of (true-listp lst).  Member-equal has
the same functionality as the Common Lisp function member, except that
it uses the equal function to test whether x is the same as each
successive element of lst.  See MEMBER and see
MEMBER-EQ.

MIN    the smaller of two numbers

(Min x y) is the smaller of the numbers x and y.

The guard for min requires its arguments to be rational (real, in
ACL2(r)) numbers.

Min is a Common Lisp function.  See any Common Lisp documentation for
more information.

MINUSP    test whether a number is negative

(Minusp x) is true if and only if x < 0.

The guard of minusp requires its argument to be a rational (real, in
ACL2(r)) number.

Minusp is a Common Lisp function.  See any Common Lisp documentation
for more information.

MOD    remainder using floor

     ACL2 !>(mod 14 3)
     2
     ACL2 !>(mod -14 3)
     1
     ACL2 !>(mod 14 -3)
     -1
     ACL2 !>(mod -14 -3)
     -2
     ACL2 !>(mod -15 -3)
     0
     ACL2 !>

(Mod i j) is that number k that (* j (floor i j)) added to k equals i.

The guard for (mod i j) requires that i and j are rational (real, in
ACL2(r)) numbers and j is non-zero.

Mod is a Common Lisp function.  See any Common Lisp documentation for
more information.

MOD-EXPT    exponential function

(mod-expt r i m) is the result of raising the number r to the integer
power i and then taking the residue mod m.  That is, (mod-expt r i m)
is equal to (mod (expt r i) m).

The guard for (mod-expt r i m) is that r is a rational number and i is
an integer; if r is 0 then i is nonnegative; and m is a non-zero
rational number.

In some implementations (GCL Version 2.7.0 as of this writing), this
function is highly optimized when r and i are natural numbers, not both
zero, and m is a positive integer.  For other Lisp implementations,
consider using function mod-expt-fast, defined in the book
arithmetic-3/floor-mod/mod-expt-fast.lisp, which should still provide
significantly improved performance over this function.

MUST-BE-EQUAL    attach code for execution

The form (must-be-equal logic exec) evaluates to logic in the ACL2
logic but evaluates to exec in raw Lisp.  The point is to be able to
write one definition to reason about logically but another for
evaluation.  Please see MBE and see MBT for appropriate
macros to use, rather than calling must-be-equal directly, since it is
easy to commute the arguments of must-be-equal by accident.

The guard for (must-be-equal x y) is (equal x y).

MV    returning a multiple value

Mv is the mechanism provided by ACL2 for returning two or more values.
Logically, (mv x1 x2 ... xn) is the same as (list x1 x2 ... xn), a list
of the indicated values.  However, ACL2 avoids the cost of building
this list structure, with the cost that mv may only be used in a
certain style in definitions:  if a function ever returns using mv
(either directly, or by calling another function that returns a
multiple value), then this function must always return the same number
of values.

For more explanation of the multiple value mechanism, see
MV-LET.

ACL2 does not support the Common Lisp construct values, whose logical
meaning seems difficult to characterize.  Mv is the ACL2 analogue of
that construct.

MV-LET    calling multi-valued ACL2 functions

     Example Form:
     (mv-let (x y z)              ; local variables
             (mv 1 2 3)           ; multi-valued expression
             (declare (ignore y)) ; optional declarations
             (cons x z))          ; body

The form above binds the three "local variables," x, y, and z, to the
three results returned by the multi-valued expression and then
evaluates the body.  The result is '(1 . 3).  The second local, y, is
declared ignored.  The multi-valued expression can be any ACL2
expression that returns k results, where k is the number of local
variables listed.  Often however it is simply the application of a
k-valued function.  Mv-let is the standard way to invoke a multi-valued
function when the caller must manipulate the vector of results returned.

     General Form:
     (mv-let (var1 ... vark)
             term
             body)
     or
     (mv-let (var1 ... vark)
             term
             (declare ...) ... (declare ...)
             body)

where the vari are distinct variables, term is a term that returns k
results and mentions only variables bound in the environment containing
the mv-let expression, and body is a term mentioning only the vari and
variables bound in the environment containing the mv-let.  Each vari
must occur in body unless it is declared ignored or ignorable in one of
the optional declare forms, unless this requirement is turned off; see
SET-IGNORE-OK.  The value of the mv-let term is the result of
evaluating body in an environment in which the vari are bound, in
order, to the k results obtained by evaluating term in the environment
containing the mv-let.

Here is an extended example that illustrates both the definition of a
multi-valued function and the use of mv-let to call it.  Consider a
simple binary tree whose interior nodes are conses and whose leaves are
non-conses.  Suppose we often need to know the number, n, of interior
nodes of such a tree; the list, syms, of symbols that occur as leaves;
and the list, ints, of integers that occur as leaves.  (Observe that
there may be leaves that are neither symbols nor integers.)  Using a
multi-valued function we can collect all three results in one pass.

Here is the first of two definitions of the desired function.  This
definition is "primitive recursive" in that it has only one argument
and that argument is reduced in size on every recursion.

     (defun count-and-collect (x)

     ; We return three results, (mv n syms ints) as described above.

       (cond ((atom x)

     ; X is a leaf.  Thus, there are 0 interior nodes, and depending on
     ; whether x is a symbol, an integer, or something else, we return
     ; the list containing x in as the appropriate result.

              (cond ((symbolp x) (mv 0 (list x) nil))
                    ((integerp x)(mv 0 nil      (list x)))
                    (t           (mv 0 nil      nil))))
             (t

     ; X is an interior node.  First we process the car, binding n1, syms1, and
     ; ints1 to the answers.

                (mv-let (n1 syms1 ints1)
                        (count-and-collect (car x))

     ; Next we process the cdr, binding n2, syms2, and ints2.

                        (mv-let (n2 syms2 ints2)
                                (count-and-collect (car x))

     ; Finally, we compute the answer for x from those obtained for its car
     ; and cdr, remembering to increment the node count by one for x itself.

                                (mv (1+ (+ n1 n2))
                                    (append syms1 syms2)
                                    (append ints1 ints2)))))))

This use of a multiple value to "do several things at once" is very
common in ACL2.  However, the function above is inefficient because it
appends syms1 to syms2 and ints1 to ints2, copying the list structures
of syms1 and ints1 in the process.  By adding "accumulators" to the
function, we can make the code more efficient.

     (defun count-and-collect1 (x n syms ints)
       (cond ((atom x)
              (cond ((symbolp x) (mv n (cons x syms) ints))
                    ((integerp x) (mv n syms (cons x ints)))
                    (t (mv n syms ints))))
             (t (mv-let (n2 syms2 ints2)
                        (count-and-collect1 (cdr x) (1+ n) syms ints)
                        (count-and-collect1 (car x) n2 syms2 ints2)))))

We claim that (count-and-collect x) returns the same triple of results
as (count-and-collect1 x 0 nil nil).  The reader is urged to study this
claim until convinced that it is true and that the latter method of
computing the results is more efficient.  One might try proving the
theorem

     (defthm count-and-collect-theorem
       (equal (count-and-collect1 x 0 nil nil) (count-and-collect x))).

Hint:  the inductive proof requires attacking a more general theorem.

ACL2 does not support the Common Lisp construct multiple-value-bind,
whose logical meaning seems difficult to characterize.  Mv-let is the
ACL2 analogue of that construct.

MV-NTH    the mv-nth element (zero-based) of a list

(Mv-nth n l) is the nth element of l, zero-based.  If n is greater than
or equal to the length of l, then mv-nth returns nil.

(Mv-nth n l) has a guard that n is a non-negative integer and l is a
true-listp.

Mv-nth is equivalent to the Common Lisp function nth, but is used by
ACL2 to access the nth value returned by a multiply valued expression.
For an example of the use of mv-nth, try

     ACL2 !>:trans1 (mv-let (erp val state)
                            (read-object ch state)
                            (value (list erp val)))

NATP    a recognizer for the natural numbers

The natural numbers is the set of all non-negative integers,
{0,1,2,3,...}.  Natp returns t if and only its argument is a   natural
number, and nil otherwise.  We recommend the file
books/arithmetic/natp-posp.lisp as a book for reasoning about posp
and natp.  This book is included in books/arithmetic/top and
books/arithmetic/top-with-meta.

NFIX    coerce to a natural number

Nfix simply returns any natural number argument unchanged, returning 0
on an argument that is not a natural number.  Also see IFIX,
see RFIX, see REALFIX, and see FIX for
analogous functions that coerce to an integer, a rational number, a
real, and a number, respectively.

Nfix has a guard of t.

NINTH    ninth member of the list

See any Common Lisp documentation for details.

NO-DUPLICATESP    check for duplicates in a list (using eql for equality)

(no-duplicatesp l) is true if and only if no member of l occurs twice
in l.

(no-duplicatesp l) has a guard of (eqlable-listp l).  Membership is
tested using member, hence using eql as the test.

NO-DUPLICATESP-EQUAL    check for duplicates in a list (using equal for equality)

(no-duplicatesp-equal l) is true if and only if no member of l occurs
twice in l.

(no-duplicatesp-equal l) has a guard of (true-listp l).  Membership is
tested using member-equal, hence using equal as the test.

NONNEGATIVE-INTEGER-QUOTIENT    natural number division function

     Example Forms:
     (nonnegative-integer-quotient 14 3) ; equals 4
     (nonnegative-integer-quotient 15 3) ; equals 5

(nonnegative-integer-quotient i j) returns the integer quotient of the
integers i and (non-zero) j, i.e., the largest k such that (* j k) is
less than or equal to i.  Also see FLOOR, see CEILING
and see TRUNCATE, which are derived from this function and
apply to rational numbers.

The guard of (nonnegative-integer-quotient i j) requires that i is a
nonnegative integer and j is a positive integer.

NOT    logical negation

Not is the ACL2 negation function.  The negation of nil is t and the
negation of anything else is nil.

Not is a Common Lisp function.  See any Common Lisp documentation for
more information.

NTH    the nth element (zero-based) of a list

(Nth n l) is the nth element of l, zero-based.  If n is greater than or
equal to the length of l, then nth returns nil.

(Nth n l) has a guard that n is a non-negative integer and l is a
true-listp.

Nth is a Common Lisp function.  See any Common Lisp documentation for
more information.

NTHCDR    final segment of a list

(Nthcdr n l) removes the first n elements from the list l.

The following is a theorem.

     (implies (and (integerp n)
                   (<= 0 n)
                   (true-listp l))
              (equal (length (nthcdr n l))
                     (if (<= n (length l))
                         (- (length l) n)
                       0)))

For related functions, see TAKE and see BUTLAST.

The guard of (nthcdr n l) requires that n is a nonnegative integer and
l is a true list.

Nthcdr is a Common Lisp function.  See any Common Lisp documentation
for more information.

NULL    recognizer for the empty list

Null is the function that checks whether its argument is nil.  For
recursive definitions it is often preferable to test for the end of a
list using endp instead of null; see ENDP.

Null is a Common Lisp function.  See any Common Lisp documentation for
more information.

NUMERATOR    dividend of a ratio in lowest terms

Completion Axiom:

     (equal (numerator x)
            (if (rationalp x)
                (numerator x)
              0))

Guard for (numerator x):

     (rationalp x)

O-FINP    recognizes if an ordinal is finite

We introduce the function o-finp which returns t for any ordinal that
is finite, else nil.  This function is equivalent to the function atom,
and is introduced so that we can disable its definition when dealing
with ordinals (also see MAKE-ORD).

O-FIRST-COEFF    returns the first coefficient of an ordinal

An ACL2 ordinal is either a natural number or, for an infinite ordinal,
a list whose elements are exponent-coefficient pairs (see O-P).
In the latter case, this function returns the cdr of the first pair in
the list.  In the case of a natural number, this function returns the
ordinal itself (since a natural number, n, can be thought of as (w^0)n).

For the corresponding exponent, see O-FIRST-EXPT.

O-FIRST-EXPT    the first exponent of an ordinal

An ACL2 ordinal is either a natural number or, for an infinite ordinal,
a list whose elements are exponent-coefficient pairs (see O-P).
In the latter case, this function returns the car of the first pair in
the list.  In the case of a natural number, the value returned is 0
(since a natural number, n, can be thought of as (w^0)n).

For the corresponding coefficient, see O-FIRST-COEFF.

O-INFP    recognizes if an ordinal is infinite

O-infp is a macro.  (O-infp x) opens up to (not (o-finp x)) (see
O-FINP).

O-P    a recognizer for the ordinals up to epsilon-0

Using the nonnegative integers and lists we can represent the ordinals
up to epsilon-0. The ordinal representation used in ACL2 has changed as
of Version_2.8 from that of Nqthm-1992, courtesy of Pete Manolios and
Daron Vroon; additional discussion may be found in "Ordinal Arithmetic
in ACL2", proceedings of ACL2 Workshop 2003,
`http://www.cs.utexas.edu/users/moore/acl2/workshop-2003/'.  Previously,
ACL2's notion of ordinal was very similar to the development given in
"New Version of the Consistency Proof for Elementary Number Theory" in
The Collected Papers of Gerhard Gentzen, ed. M.E. Szabo, North-Holland
Publishing Company, Amsterdam, 1969, pp 132-213.

The following essay is intended to provide intuition about ordinals.
The truth, of course, lies simply in the ACL2 definitions of o-p and o<.

Very intuitively, think of each non-zero natural number as by being
denoted by a series of the appropriate number of strokes, i.e.,

     0             0
     1             |
     2             ||
     3             |||
     4             ||||
     ...           ...

Then "omega," here written as w, is the ordinal that might be written as

     w             |||||...,

i.e., an infinite number of strokes.  Addition here is just
concatenation.  Observe that adding one to the front of w in the
picture above produces w again, which gives rise to a standard
definition of w:  w is the least ordinal such that adding another
stroke at the beginning does not change the ordinal.

We denote by w+w or w*2 the "doubly infinite" sequence that we might
write as follows.

     w*2           |||||... |||||...

One way to think of w*2 is that it is obtained by replacing each stroke
in 2 (||) by w.  Thus, one can imagine w*3, w*4, etc., which leads
ultimately to the idea of "w*w," the ordinal obtained by replacing each
stroke in w by w.  This is also written as "omega squared" or w^2, or:

      2
     w             |||||... |||||... |||||... |||||... |||||... ...

We can analogously construct w^3 by replacing each stroke in w by w^2
(which, it turns out, is the same as replacing each stroke in w^2 by
w).  That is, we can construct w^3 as w copies of w^2,

      3              2       2       2       2
     w              w  ...  w  ...  w  ...  w ... ...

Then we can construct w^4 as w copies of w^3, w^5 as w copies of w^4,
etc., ultimately suggesting w^w.  We can then stack omegas, i.e.,
(w^w)^w etc.  Consider the "limit" of all of those stacks, which we
might display as follows.

            .
           .
          .
         w
        w
       w
      w
     w

That is epsilon-0.

Below we begin listing some ordinals up to epsilon-0; the reader can
fill in the gaps at his or her leisure.  We show in the left column the
conventional notation, using w as "omega," and in the right column the
ACL2 object representing the corresponding ordinal.

       ordinal            ACL2 representation

       0                  0
       1                  1
       2                  2
       3                  3
       ...                ...
       w                 '((1 . 1) . 0)
       w+1               '((1 . 1) . 1)
       w+2               '((1 . 1) . 2)
       ...                ...
       w*2               '((1 . 2) . 0)
       (w*2)+1           '((1 . 2) . 1)
       ...                ...
       w*3               '((1 . 3) . 0)
       (w*3)+1           '((1 . 3) . 1)
       ...                ...

        2
       w                 '((2 . 1) . 0)
       ...                ...

        2
       w +w*4+3          '((2 . 1) (1 . 4) . 3)
       ...                ...

        3
       w                 '((3 . 1) . 0)
       ...                ...

        w
       w                 '((((1 . 1) . 0) . 1) . 0)
       ...                ...

        w  99
       w +w  +w4+3       '((((1 . 1) . 0) . 1) (99 . 1) (1 . 4) . 3)
       ...                ...

         2
        w
       w                 '((((2 . 1) . 0) . 1) . 0)

       ...                ...

         w
        w
       w                 '((((((1 . 1) . 0) . 1) . 0) . 1) . 0)
       ...               ...

Observe that the sequence of o-ps starts with the natural numbers
(which are recognized by natp). This is convenient because it means
that if a term, such as a measure expression for justifying a recursive
function (see O<) must produce an o-p, it suffices for it to
produce a natural number.

The ordinals listed above are listed in ascending order.  This is the
ordering tested by o<.

The "epsilon-0 ordinals" of ACL2 are recognized by the recursively
defined function o-p.  The base case of the recursion tells us that
natural numbers are epsilon-0 ordinals.  Otherwise, an epsilon-0
ordinal is a list of cons pairs whose final cdr is a natural number,
((a1 . x1) (a2 . x2) ... (an . xn) . p).  This corresponds to the
ordinal (w^a1)x1 + (w^a2)x2 + ... + (w^an)xn + p.  Each ai is an
ordinal in the ACL2 representation that is not equal to 0.  The
sequence of the ai's is strictly decreasing (as defined by o<). Each xi
is a positive integer (as recognized by posp).

Note that infinite ordinals should generally be created using the
ordinal constructor, make-ord, rather than cons. The functions
o-first-expt, o-first-coeff, and o-rst are ordinals destructors.
Finally, the function o-finp and the macro o-infp tell whether an
ordinal is finite or infinite, respectively.

The function o< compares two epsilon-0 ordinals, x and y.  If both are
integers, (o< x y) is just x<y.  If one is an integer and the other is
a cons, the integer is the smaller.  Otherwise, o< recursively compares
the o-first-expts of the ordinals to determine which is smaller.  If
they are the same, the o-first-coeffs of the ordinals are compared.  If
they are equal, the o-rsts of the ordinals are recursively compared.

Fundamental to ACL2 is the fact that o< is well-founded on epsilon-0
ordinals.  That is, there is no "infinitely descending chain" of such
ordinals.  See PROOF-OF-WELL-FOUNDEDNESS.

O-RST    returns the rest of an infinite ordinal

An ACL2 infinite ordinal is a list whose elements are
exponent-coefficient pairs (see O-P and see O-INFP).
The first exponent and first coefficient of an ordinal can be obtained
by using o-first-expt and o-first-coeff respectively.  To obtain the
rest of the ordinal (for recursive analysis), use the o-rst function.
It returns the rest of the ordinal after the first exponent and
coefficient are removed.

O<    the well-founded less-than relation on ordinals up to epsilon-0

If x and y are both o-ps (see O-P) then (o< x y) is true iff x
is strictly less than y.  o< is well-founded on the o-ps.  When x and y
are both nonnegative integers, o< is just the familiar "less than"
relation (<).

o< plays a key role in the formal underpinnings of the ACL2 logic.  In
order for a recursive definition to be admissible it must be proved to
"terminate."  By terminate we mean that the arguments to the function
"get smaller" as the function recurses and this sense of size
comparison must be such that there is no "infinitely descending"
sequence of ever smaller arguments.  That is, the relation used to
compare successive arguments must be well-founded on the domain being
measured.

The most basic way ACL2 provides to prove termination requires the user
to supply (perhaps implicitly) a mapping of the argument tuples into
the ordinals with some "measure" expression in such a way that the
measures of the successive argument tuples produced by recursion
decrease according to the relation o<.  The validity of this method
rests on the well-foundedness of o< on the o-ps.

Without loss of generality, suppose the definition in question
introduces the function f, with one formal parameter x (which might be
a list of objects).  Then we require that there exist a measure
expression, (m x), that always produces an o-p.  Furthermore, consider
any recursive call, (f (d x)), in the body of the definition.  Let hyps
be the conjunction of terms, each of which is either the test of an if
in the body or else the negation of such a test, describing the path
through the body to the recursive call in question.  Then it must be a
theorem that

       (IMPLIES hyps (O< (m (d x)) (m x))).

When we say o< is "well-founded" on the o-ps we mean that there is no
infinite sequence of o-ps such that each is smaller than its
predecessor in the sequence.  Thus, the theorems that must be proved
about f when it is introduced establish that it cannot recur forever
because each time a recursive call is taken (m x) gets smaller.  From
this, and the syntactic restrictions on definitions, it can be shown
(as on page 44 in "A Computational Logic", Boyer and Moore, Academic
Press, 1979) that there exists a function satisfying the definition;
intuitively, the value assigned to any given x by the alleged function
is that computed by a sufficiently large machine.  Hence, the logic is
consistent if the axiom defining f is added.

See O-P for a discussion of the ordinals and how to compare two
ordinals.

The definitional principle permits the use of relations other than o<
but they must first be proved to be well-founded on some domain.  See
WELL-FOUNDED-RELATION.  Roughly put, alternative relations are
shown well-founded by providing an order-preserving mapping from their
domain into the ordinals.  See DEFUN for details on how to
specify which well-founded relation is to be used.

O<=    the less-than-or-equal relation for the ordinals

o<= is a macro and (o<= x y) expands to (not (o< y x)).  See O<.

O>    the greater-than relation for the ordinals

O> is a macro and (o> x y) expands to (o< y x).  See O<.

O>=    the greater-than-or-equal relation for the ordinals

O>= is a macro and (o>= x y) expands to (not (o< x y)).  See O<.

ODDP    test whether an integer is odd

(oddp x) is true if and only if x is odd, i.e., not even in the sense
of evenp.

The guard for oddp requires its argument to be an integer.

Oddp is a Common Lisp function.  See any Common Lisp documentation for
more information.

OPEN-INPUT-CHANNEL    See IO.

OPEN-INPUT-CHANNEL-P    See IO.

OPEN-OUTPUT-CHANNEL    See IO.

OPEN-OUTPUT-CHANNEL-P    See IO.

OPTIMIZE    See DECLARE.

OR    disjunction

Or is the macro for disjunctions.  Or takes any number of arguments and
returns the first that is non-nil, or nil if there is no non-nil
element.

In the ACL2 logic, the macroexpansion of (or x y) is an IF term that
appears to cause x to be evaluated twice:

     ACL2 !>:trans (or x y)

     (IF X X Y)

     => *

     ACL2 !>

If x were replaced by an expression whose evaluation takes a long time,
then such an expansion would be ineffecient.  However, don't be fooled:
you can expect Common Lisp implementations to avoid this problem, say by
generating a new variable, for example:

     ACL2 !>:q ; Exit the ACL2 loop and go into raw Common Lisp

     Exiting the ACL2 read-eval-print loop.  To re-enter, execute (LP).
     ACL2>(macroexpand '(or x y))

     (LET ((#:G5374 X)) (IF #:G5374 #:G5374 Y))
     T

     ACL2>

Or is a Common Lisp macro.  See any Common Lisp documentation for more
information.

PAIRLIS    See PAIRLIS$

The Common Lisp language allows its pairlis function to construct an
alist in any order!  So we have to define our own version: See
PAIRLIS$.

PAIRLIS$    zipper together two lists

The Common Lisp language allows its pairlis function to construct an
alist in any order!  So we have to define our own version, pairlis$.
It returns the list of pairs obtained by consing together successive
respective members of the given lists until the first list runs out.
(Hence in particular, if the second argument is nil then each element
of the first argument is paired with nil.)

The guard for pairlis$ requires that its arguments are true lists.

PEEK-CHAR$    See IO.

PKG-WITNESS    return a specific symbol in the indicated package

For any string pkg that names a package currently known to ACL2,
(pkg-witness pkg) is a symbol in that package whose symbol-name is the
value of constant *pkg-witness-name*.  Logically, this is the case even
if the package is not currently known to ACL2.  However, if pkg-witness
is called on a string that is not the name of a package known to ACL2,
a hard Lisp error will result.

(Pkg-witness pkg) has a guard of (and (stringp pkg) (not (equal pkg
""))).  If pkg is not a string, then (pkg-witness pkg) is equal to
(pkg-witness "ACL2")

PLUSP    test whether a number is positive

(Plusp x) is true if and only if x > 0.

The guard of plusp requires its argument to be a rational (real, in
ACL2(r)) number.

Plusp is a Common Lisp function.  See any Common Lisp documentation for
more information.

POSITION    position of an item in a string or a list, using eql as test

(Position item seq) is the least index (zero-based) of the element item
in the string or list seq, if in fact item is an element of seq.
Otherwise (position item seq) is nil.

(Position item lst) is provably the same in the ACL2 logic as
(position-equal item lst).  It has a stronger guard than position-equal
because uses eql to test equality of item with members of lst.  Its
guard requires that either lst is a string, or else lst is a true list
such that either (eqlablep item) or all members of lst are eqlablep.
See POSITION-EQUAL and see POSITION-EQ.

Position is a Common Lisp function.  See any Common Lisp documentation
for more information.  Since ACL2 functions cannot take keyword
arguments (though macros can), the ACL2 functions position-equal and
position-eq are defined to correspond to calls of the Common Lisp
function position whose keyword argument :test is equal or eq,
respectively.

POSITION-EQ    position of an item in a string or a list, using eq as test

(Position-eq item seq) is the least index (zero-based) of the element
item in the list seq, if in fact item is an element of seq.  Otherwise
(position-eq item seq) is nil.

(Position-eq item lst) is provably the same in the ACL2 logic as
(position item lst) and (position-equal item lst) when lst is a true
list, but it has a stronger guard because it uses eq for a more
efficient test for whether item is equal to a given member of lst.  Its
guard requires that lst is a true list, and moreover, either item is a
symbol or lst is a list of symbols.  See POSITION-EQUAL and see
POSITION, which unlike position-eq have guards that allow the
second argument to be a string.

POSITION-EQUAL    position of an item in a string or a list

(Position item seq) is the least index (zero-based) of the element item
in the string or list seq, if in fact item is an element of seq.
Otherwise (position item seq) is nil.

(Position-equal item lst) has a guard of (true-listp lst).
Position-equal has the same functionality as the Common Lisp function
position, except that it uses the equal function to test whether item
is the same as each successive element of lst.  See POSITION
and see POSITION-EQ.

POSP    a recognizer for the positive integers

(posp x) is logically equivalent to (not (zp x)) (see ZP) and
also   to (and (natp x) (not (equal x 0))).  We recommend the file
books/ordinals/natp-posp as a book for reasoning about posp and   natp.
This book is included in books/arithmetic/top and
books/arithmetic/top-with-meta.

PPROGN    evaluate a sequence of forms that return state

     Example Form:
     (pprogn
      (cond ((or (equal (car l) #\) (equal (car l) slash-char))
             (princ$ #\ channel state))
            (t state))
      (princ$ (car l) channel state)
      (mv (cdr l) state))

The convention for pprogn usage is to give it a non-empty sequence of
forms, each of which (except possibly for the last) returns state (see
STATE) as its only value.  The state returned by each but the
last is passed on to the next.  The value or values of the last form
are returned as the value of the pprogn.

If you are using single-threaded objects you may wish to define an
analogue of this function for your own stobj.

General Form:

     (PPROGN form1
             form2
             ...
             formk
             result-form)

This general form is equivalent, via macro expansion, to:

     (LET ((STATE form1))
          (LET ((STATE form2))
               ...
               (LET ((STATE formk))
                    result-form)))

PRINT-OBJECT$    See IO.

PROG2$    execute two forms and return the value of the second one

See HARD-ERROR, see ILLEGAL, and see CW for
examples of functions to call in the first argument of prog2$.

Semantically, (Prog2$ x y) equals y; the value of x is ignored.
However, x is first evaluated for side effect.  Since the ACL2
programming language is applicative, there can be no logical impact of
evaluating x.  However, x may involve a call of a function such as
hard-error or illegal, which can cause so-called "hard errors", or a
call of cw to perform output.

Here is a simple, contrived example using hard-error.  The intention is
to check at run-time that the input is appropriate before calling
function bar.

     (defun foo-a (x)
       (declare (xargs :guard (consp x)))
       (prog2$
        (or (good-car-p (car x))
            (hard-error 'foo-a
                        "Bad value for x: ~p0"
                        (list (cons #\0 x))))
        (bar x)))

The following similar function uses illegal instead of hard-error.
Since illegal has a guard of nil, guard verification would guarantee
that the call of illegal below will never be made (at least when guard
checking is on; see SET-GUARD-CHECKING).

     (defun foo-b (x)
       (declare (xargs :guard (and (consp x) (good-car-p (car x)))))
       (prog2$
        (or (good-car-p (car x))
            (illegal 'foo-b
                     "Bad value for x: ~p0"
                     (list (cons #\0 x))))
        (bar x)))

We conclude with a simple example using cw from the ACL2 sources.

     (defun print-terms (terms iff-flg wrld)

     ; Print untranslations of the given terms with respect to iff-flg, following
     ; each with a newline.

     ; We use cw instead of the fmt functions because we want to be able to use this
     ; function in print-type-alist-segments (used in brkpt1), which does not return
     ; state.

       (if (endp terms)
           terms
         (prog2$
          (cw "~q0" (untranslate (car terms) iff-flg wrld))
          (print-terms (cdr terms) iff-flg wrld))))

PROOFS-CO    the proofs character output channel

Proofs-co is an ld special (see LD).  The accessor is
(proofs-co state) and the updater is (set-proofs-co val state).
Proofs-co must be an open character output channel.  It is to this
channel that defun, defthm, and the other event commands print their
commentary.

"Proofs-co" stands for "proofs character output." The initial value of
proofs-co is the same as the value of *standard-co* (see
*STANDARD-CO*).

PROPER-CONSP    recognizer for proper (null-terminated) non-empty lists

Proper-consp is the function that checks whether its argument is a
non-empty list that ends in nil.  Also see TRUE-LISTP.

PUT-ASSOC-EQ    modify an association list by associating a value with a key

(Put-assoc-eq name val alist) returns an alist that is the same as the
list alist, except that the first pair in alist with a car of name is
replaced by (cons name val), if there is one.  If there is no such
pair, then (cons name val) is added at the end.  Note that the order of
the keys occurring in alist is unchanged (though a new key may be
added).

The guard of (put-assoc-eq name val alist) requires that alist is an
alistp, and moreover, either name is a symbol or alist is a
symbol-alistp.

PUT-ASSOC-EQL    modify an association list by associating a value with a key

(Put-assoc-eql name val alist) returns an alist that is the same as the
list alist, except that the first pair in alist with a car of name is
replaced by (cons name val), if there is one.  If there is no such
pair, then (cons name val) is added at the end.  Note that the order of
the keys occurring in alist is unchanged (though a new key may be
added).

The guard of (put-assoc-eql name val alist) requires that alist is an
alistp, and moreover, either name is eqlablep or alist is an
eqlable-alistp.

PUT-ASSOC-EQUAL    modify an association list by associating a value with a key

(Put-assoc-equal name val alist) returns an alist that is the same as
the list alist, except that the first pair in alist with a car of name
is replaced by (cons name val), if there is one.  If there is no such
pair, then (cons name val) is added at the end.

The guard of (put-assoc-equal name val alist) requires that alist is an
alistp.

PUTPROP    update fast property lists

     General form:
     (putprop symbol key value world-alist)

See books/misc/getprop.lisp for an example that illustrates the use of
ACL2 utilities getprop and putprop to take advantage of under-the-hood
Lisp (hashed) property lists.

RANDOM$    obtain a random value

     Example:
     (random$ 10 state) ==> (mv 7 <state>)

(Random$ limit state), where limit is a positive integer, returns a
random non-negative integer together with a new state.  Logically, it
simply returns the first element of a list that is a field of the ACL2
state, called the acl2-oracle, together with the new state resulting
from removing that element from that list.  (Except, if that element is
not in range as specified above, then 0 is returned.)  However, random$
actually invokes a Common Lisp function to choose the integer returned.
Quoting from the Common Lisp HyperSpec(TM),
`http://www.lispworks.com/documentation/HyperSpec/Front': "An
approximately uniform choice distribution is used...  each of the
possible results occurs with (approximate) probability 1/limit."

Consider enabling rules natp-random$ and random$-linear if you want to
reason about random$.

RASSOC    look up value in association list, using eql as test

(Rassoc x alist) is similar to (assoc x alist), the difference being
that it looks for the first pair in the given alist whose cdr, rather
than car, is eql to x.  See ASSOC.

The guard of rassoc requires its second argument to be an alist, and in
addition, that either its first argument is eqlablep or else all second
components of pairs belonging to the second argument are eqlablep.  See
EQLABLEP.

Rassoc is a Common Lisp function.  See any Common Lisp documentation
for more information.

RASSOC-EQ    look up value in association list, using eq as test

(Rassoc-eq x alist) is similar to (assoc-eq x alist), the difference
being that it looks for the first pair in the given alist whose cdr,
rather than car, is eq to x.  See ASSOC.

The guard of rassoc-eq requires its second argument to be an alist, and
in addition, that either its first argument is a symbolp or else all
second components of pairs belonging to the second argument are
symbolps.

Rassoc is a Common Lisp function.  See any Common Lisp documentation
for more information.

RASSOC-EQUAL    look up value in association list, using equal as test

(Rassoc-equal x alist) is similar to (assoc-equal x alist), the
difference being that it looks for the first pair in the given alist
whose cdr, rather than car, is equal to x.  See ASSOC-EQUAL.

The guard of rassoc-equal requires its second argument to be an alist.
See RASSOC and see RASSOC-EQ.

RATIONAL-LISTP    recognizer for a true list of rational numbers

The predicate rational-listp tests whether its argument is a true list
of rational numbers.

RATIONALP    recognizer for rational numbers (ratios and integers)

(rationalp x) is true if and only if x is an rational number.

READ-BYTE$    See IO.

READ-CHAR$    See IO.

READ-OBJECT    See IO.

REAL/RATIONALP    recognizer for rational numbers (including real number in ACL2(r))

For most ACL2 users, this is a macro abbreviating rationalp.  In
ACL2(r) (see REAL), this macro abbreviates the predicate realp,
which holds for real numbers as well (including rationals).  Most ACL2
users can ignore this macro and use rationalp instead, but many books
in the ACL2 distribution use real/rationalp so that these books will be
suitable for ACL2(r) as well.

REALFIX    coerce to a real number

Realfix simply returns any real number argument unchanged, returning 0
on a non-real argument.  Also see NFIX, see IFIX, see
RFIX, and see FIX for analogous functions that coerce
to a natural number, an integer, a rational, and a number, respectively.

Realfix has a guard of t.

REALPART    real part of a complex number

Completion Axiom:

     (equal (realpart x)
            (if (acl2-numberp x)
                (realpart x)
              0))

Guard for (realpart x):

     (acl2-numberp x)

REDEFINING-PROGRAMS    an explanation of why we restrict redefinitions

ACL2 does not in general allow the redefinition of functions because
logical inconsistency can result:  previously stored theorems can be
rendered invalid if the axioms defining the functions involved are
changed.  However, to permit prototyping of both :program and :logic
mode systems, ACL2 permits redefinition if the user has accepted
logical responsibility for the consequences by setting
ld-redefinition-action to an appropriate non-nil value.  The refusal of
ACL2 to support the unrestricted redefinition of :program mode
functions may appear somewhat capricious.  After all, what are the
logical consequences of changing a definition if no axioms are involved?

Three important points should be made before we discuss redefinition
further.

The first is that ACL2 does support redefinition (of both :program and
:logic functions) when ld-redefinition-action is non-nil.

The second is that a "redefinition" that does not change the mode,
formals, guards, type declarations, stobjs, or body of a function is
considered redundant and is permitted even when ld-redefinition-action
is nil.  We recognize and permit redundant definitions because it is not
uncommon for two distinct books to share identical function
definitions.  When determining whether the body of a function is
changed by a proposed redefinition, we actually compare the
untranslated versions of the two bodies.  See TERM.  For
example, redundancy is not recognized if the old body is (list a b) and
the new body is (cons a (cons b nil)).  We use the untranslated bodies
because of the difficulty of translating the new body in the presence
of the old syntactic information, given the possibility that the
redefinition might attempt to change the signature of the function,
i.e., the number of formals, the number of results, or the position of
single-threaded objects in either.

The third important point is that a "redefinition" that preserves the
formals, guard, types, stobjs, and body but changes the mode from
:program to :logic is permitted even when ld-redefinition-action is
nil.  That is what verify-termination does.

This note addresses the temptation to allow redefinition of :program
functions in situations other than the three described above.
Therefore, suppose ld-redefinition-action is nil and consider the cases.

Case 1.  Suppose the new definition attempts to change the formals or
more generally the signature of the function.  Accepting such a
redefinition would render ill-formed other :program functions which
call the redefined function.  Subsequent attempts to evaluate those
callers could arbitrarily damage the Common Lisp image.  Thus,
redefinition of :program functions under these circumstances requires
the user's active approval, as would be sought with
ld-redefinition-action '(:query . :overwrite).

Case 2.  Suppose the new definition attempts to change the body (even
though it preserves the signature).  At one time we believed this was
acceptable and ACL2 supported the quiet redefinition of :program mode
functions in this circumstance.  However, because such functions can be
used in macros and redundancy checking is based on untranslated bodies,
this turns out to be unsound!  (Aside: Perhaps this is not an issue if
the function takes state or a user-defined stobj argument; but we do
not further consider this distinction.)  Such redefinition is therefore
now prohibited.  We illustrate such an unsoundness below.  Let
foo-thm1.lisp be a book with the following contents.

     (in-package "ACL2")
     (defun p1 (x) (declare (xargs :mode :program)) (list 'if x 't 'nil))
     (defmacro p (x) (p1 x))
     (defun foo (x) (p x))
     (defthm foo-thm1 (iff (foo x) x) :rule-classes nil)

Note that the macro form (p x) translates to (if x t nil).  The
:program function p1 is used to generate this translation.  The
function foo is defined so that (foo x) is (p x) and a theorem about
foo is proved, namely, that (foo x) is true iff x is true.

Now let foo-thm2.lisp be a book with the following contents.

     (in-package "ACL2")
     (defun p1 (x) (declare (xargs :mode :program)) (list 'if x 'nil 't))
     (defmacro p (x) (p1 x))
     (defun foo (x) (p x))
     (defthm foo-thm2 (iff (foo x) (not x)) :rule-classes nil)

In this book, the :program function p1 is defined so that (p x) means
just the negation of what it meant in the first book, namely, (if x nil
t).  The function foo is defined identically -- more precisely, the
untranslated body of foo is identical in the two books, but because of
the difference between the two versions of the :program function p1 the
axioms defining the two foos are different.  In the second book we prove
the theorem that (foo x) is true iff x is nil.

Now consider what would happen if the signature-preserving redefinition
of :program functions were permitted and these two books were included.
When the second book is included the redefinition of p1 would be
permitted since the signature is preserved and p1 is just a :program.
But then when the redefinition of foo is processed it would be
considered redundant and thus be permitted.  The result would be a
logic in which it was possible to prove that (foo x) is equivalent to
both x and (not x).  In particular, the following sequence leads to a
proof of nil:

     (include-book "foo-thm1")
     (include-book "foo-thm2")
     (thm nil :hints (("Goal" :use (foo-thm1 foo-thm2))))

It might be possible to loosen the restrictions on the redefinition of
:program functions by allowing signature-preserving redefinition of
:program functions not involved in macro definitions.  Alternatively,
we could implement definition redundancy checking based on the
translated bodies of functions (though that is quite problematic).
Barring those two changes, we believe it is necessary simply to impose
the same restrictions on the redefinition of :program mode functions as
we do on :logic mode functions.

REM    remainder using truncate

     ACL2 !>(rem 14 3)
     2
     ACL2 !>(rem -14 3)
     -2
     ACL2 !>(rem 14 -3)
     2
     ACL2 !>(rem -14 -3)
     -2
     ACL2 !>(rem -15 -3)
     0
     ACL2 !>

(Rem i j) is that number k for which (* j (truncate i j)) added to k
equals i.

The guard for (rem i j) requires that i and j are rational (real, in
ACL2(r)) numbers and j is non-zero.

Rem is a Common Lisp function.  See any Common Lisp documentation for
more information.

REMOVE    remove all occurrences, testing using eql

(remove x l) is l if x is not a member of l, else is the result of
removing all occurrences of x from l.

The guard for (remove x l) requires l to be a true list and moreover,
either x is eqlablep or all elements of l are eqlablep.

Remove is a Common Lisp function.  See any Common Lisp documentation
for more information.  Note that we do not allow keyword arguments
(such as test) in ACL2 functions, in particular, in remove.

Also see REMOVE1, see REMOVE-EQUAL, and see
REMOVE-EQ.

REMOVE-DUPLICATES    remove duplicates from a string or (using eql) a list

Remove-duplicates returns the result of deleting duplicate elements
from the beginning of the given string or true list, i.e., leaving the
last element in place.  For example,

     (remove-duplicates '(1 2 3 2 4))

is equal to '(1 3 2 4).

The guard for Remove-duplicates requires that its argument is a string
or a true-list of eqlablep objects.  It uses the function eql to test
for equality between elements of its argument.

Remove-duplicates is a Common Lisp function.  See any Common Lisp
documentation for more information.  Note that we do not allow keyword
arguments (such as test) in ACL2 functions, in particular, in
remove-duplicates.  But see REMOVE-DUPLICATES-EQUAL, which is
similar but uses the function equal to test for duplicate elements.

REMOVE-DUPLICATES-EQUAL    remove duplicates from a list

Remove-duplicates-equal is the same as remove-duplicates, except that
its argument must be a true list (not a string), and equal is used to
check membership rather than eql.  See REMOVE-DUPLICATES.

The guard for Remove-duplicates-equal requires that its argument is a
true list.  Note that unlike remove-duplicates, it does not allow
string arguments.

REMOVE-EQ    remove all occurrences, testing using eq

(remove-eq x l) is l if x is not a member of l as tested with
member-eq, else is the result of removing all occurrences of x from l.

The guard for (remove-eq x l) requires l to be a true list and
moreover, either x is a symbolp or all elements of l are symbols (i.e.,
l is a symbol-listp).

Also see REMOVE1-EQ, see REMOVE, and see
REMOVE-EQUAL.

REMOVE-EQUAL    remove all occurrences, testing using equal

(remove-equal x l) is l if x is not a member of l as tested with
member-equal, else is the result of removing all occurrences of x from
l.

The guard for (remove-equal x l) requires l to be a true list.

Also see REMOVE1-EQUAL, see REMOVE, and see
REMOVE-EQ.

REMOVE1    remove first occurrences, testing using eql

(remove1 x l) is l if x is not a member of l, else is the result of
removing the first occurrence of x from l.

The guard for (remove1 x l) requires l to be a true list and moreover,
either x is eqlablep or all elements of l are eqlablep.

Also see REMOVE, see REMOVE1-EQUAL, and see
REMOVE1-EQ.

REMOVE1-EQ    remove first occurrences, testing using eq

(remove1-eq x l) is l if x is not a member of l as tested with
member-eq, else is the result of removing the first occurrences of x
from l.

The guard for (remove1-eq x l) requires l to be a true list and
moreover, either x is a symbolp or all elements of l are symbols (i.e.,
l is a symbol-listp).

Also see REMOVE-EQ, see REMOVE1, and see
REMOVE1-EQUAL.

REMOVE1-EQUAL    remove first occurrences, testing using equal

(remove1-equal x l) is l if x is not a member of l as tested with
member-equal, else is the result of removing the first occurrence of x
from l.

The guard for (remove1-equal x l) requires l to be a true list.

Also see REMOVE-EQUAL, see REMOVE1, and see
REMOVE1-EQ.

REST    rest (cdr) of the list

In the logic, rest is just a macro for cdr.

Rest is a Common Lisp function.  See any Common Lisp documentation for
more information.

REVAPPEND    concatentate the reverse of one list to another

(Revappend x y) concatenates the reverse of the list x to y, which is
also typically a list.

The following theorem characterizes this English description.

     (equal (revappend x y)
            (append (reverse x) y))

Hint:  This lemma follows immediately from the definition of reverse
and the following lemma.

     (defthm revappend-append
       (equal (append (revappend x y) z)
              (revappend x (append y z))))

The guard for (revappend x y) requires that x is a true list.

Revappend is defined in Common Lisp.  See any Common Lisp documentation
for more information.

REVERSE    reverse a list or string

(Reverse x) is the result of reversing the order of the elements of the
list or string x.

The guard for reverse requires that its argument is a true list or a
string.

Reverse is defined in Common Lisp.  See any Common Lisp documentation
for more information.

RFIX    coerce to a rational number

Rfix simply returns any rational number argument unchanged, returning 0
on a non-rational argument.  Also see NFIX, see IFIX,
see REALFIX, and see FIX for analogous functions that
coerce to a natural number, an integer, a real, and a number,
respectively.

Rfix has a guard of t.

ROUND    division returning an integer by rounding off

     Example Forms:
     ACL2 !>(round 14 3)
     5
     ACL2 !>(round -14 3)
     -5
     ACL2 !>(round 14 -3)
     -5
     ACL2 !>(round -14 -3)
     5
     ACL2 !>(round 13 3)
     4
     ACL2 !>(round -13 3)
     -4
     ACL2 !>(round 13 -3)
     -4
     ACL2 !>(round -13 -3)
     4
     ACL2 !>(round -15 -3)
     5
     ACL2 !>(round 15 -2)
     -8

(Round i j) is the result of taking the quotient of i and j and
rounding off to the nearest integer.  When the quotient is exactly
halfway between consecutive integers, it rounds to the even one.

The guard for (round i j) requires that i and j are rational (real, in
ACL2(r)) numbers and j is non-zero.

Round is a Common Lisp function.  See any Common Lisp documentation for
more information.  However, note that unlike Common Lisp, the ACL2 round
function returns only a single value,

SEARCH    search for a string or list in another string or list

     Example Forms:
     (search "cd" "Cdabcdefcde")                   ; = 4, index of first match
     (search "cd" "Cdabcdefcde" :test 'equal)      ; same as above
     (search "cd" "Cdabcdefcde" :from-end t)       ; = 8, index of last match
     (search "cd" "Cdabcdefcde" :start1 1)         ; = 1
     (search "cd" "Cdabcdefcde" :start2 5)         ; = 8
     (search "cd" "Cdabcdefcde" :test 'char-equal) ; = 0 (case-insensitive)
     (search "ac" "Cdabcdefcde")                   ; = nil
     (search '(a b) '(9 8 a b 7 6))                    ; = 2

     General Form:
     (search seq1 seq2 &key from-end test start1 start2 end1 end2)

Search indicates whether one string or list occurs as a (contiguous)
subsequence of another string or list, respectively.  It returns nil if
no such match is found; otherwise it returns the (zero-based) index of
the first match by default, but a non-nil value of keyword argument
:from-end causes it to return the last match.  The :test is equal by
default.  The other legal value for :test is char-equal, which can be
given only for two strings, in which case the match is case-insensitive.
Finally, values of :start1 and :end1 for the first sequence, and of
:start2 and [:end2] for the second sequence, bound the portion of the
respective sequence used for deciding on a match, though the index
returned is always an index into the second sequence as a whole.

The guard for calls of search is given by a function, search-fn-guard,
which has the following requirements.

     o The two arguments much both satisfy true-listp or else must both
     be strings consisting of standard characters (see
     STANDARD-CHAR-P).

     o The :test must evaluate to one of the symbols equal or
     char-equal, where the latter is only allowed if the (first) two
     arguments are strings.

     o The values of :start1, :start2, :end1, and :end2 must all be
     natural numbers, where if omitted they default to 0, 0, the length
     len1 of the first argument, and the length len2 of the second
     argument, respectively.

     o If start1 is the value of :start1, defaulting as described just
     above, and similarly for the other start and end keywords and for
     lengths len1 and len2 as described just above, then: start1 <=
     end1 <= len1 and start2 <= end2 <= len2.

Search is a Common Lisp function (actually, a macro in ACL2).  See any
Common Lisp documentation for more information.

SECOND    second member of the list

See any Common Lisp documentation for details.

SET-DIFFERENCE-EQ    elements of one list that are not elements of another

(Set-difference-eq x y) is logically equivalent to
set-difference-equal, except that the guard requires not only that the
two arguments are true-listps but also that at least one is a
symbol-listp.  Also see SET-DIFFERENCE-EQUAL.

SET-DIFFERENCE-EQUAL    elements of one list that are not elements of another

(Set-difference-equal x y) equals a list whose members (see
MEMBER-EQUAL) contains the members of x that are not members of y.
More precisely, the resulting list is the same as one gets by deleting
the members of y from x, leaving the remaining elements in the same
order as they had in x.

The guard for set-difference-equal requires both arguments to be true
lists.  Essentially, set-difference-equal has the same functionality as
the Common Lisp function set-difference, except that it uses the equal
function to test membership rather than eql.  However, we do not
include the function set-difference in ACL2, because the Common Lisp
language does not specify the order of the elements in the list that it
returns.

Also see SET-DIFFERENCE-EQ for a semantically equivalent
function that executes more efficiently on lists of symbols.

SETENV$    set an environment variable

(Setenv$ str val), where str and val are strings, sets the environment
variable str to have value val, for subsequent read by getenv$ (see
GETENV$), and returns nil.  Or, if this operation is not
implemented for the host Common Lisp, an error will occur.

     Example:
     (setenv$ "FOO" "BAR")

SEVENTH    seventh member of the list

See any Common Lisp documentation for details.

SIGNUM    indicator for positive, negative, or zero

(Signum x) is 0 if x is 0, -1 if x is negative, and is 1 otherwise.

The guard for signum requires its argument to be rational (real, in
ACL2(r)) number.

Signum is a Common Lisp function.  See any Common Lisp documentation
for more information.

From "Common Lisp the Language" page 206, we see a definition of signum
in terms of abs.  As explained elsewhere (see ABS), the guard
for abs requires its argument to be a rational (real, in ACL2(r))
number; hence, we make the same restriction for signum.

SIXTH    sixth member of the list

See any Common Lisp documentation for details.

STANDARD-CHAR-LISTP    recognizer for a true list of standard characters

(standard-char-listp x) is true if and only if x is a null-terminated
list all of whose members are standard characters.  See
STANDARD-CHAR-P.

Standard-char-listp has a guard of t.

STANDARD-CHAR-P    recognizer for standard characters

(Standard-char-p x) is true if and only if x is a "standard" character,
i.e., a member of the list *standard-chars*.  This list includes
#Newline and #Space characters, as well as the usual punctuation and
alphanumeric characters.

Standard-char-p has a guard requiring its argument to be a character.

Standard-char-p is a Common Lisp function.  See any Common Lisp
documentation for more information.

STANDARD-CO    the character output channel to which ld prints

Standard-co is an ld special (see LD).  The accessor is
(standard-co state) and the updater is (set-standard-co val state).
Standard-co must be an open character output channel.  It is to this
channel that ld prints the prompt, the form to be evaluated, and the
results.  The event commands such as defun, defthm, etc., which print
extensive commentary do not print to standard-co but rather to a
different channel, proofs-co, so that you may redirect this commentary
while still interacting via standard-co.  See PROOFS-CO.

"Standard-co" stands for "standard character output." The initial value
of standard-co is the same as the value of *standard-co* (see
*STANDARD-CO*).

STANDARD-OI    the standard object input "channel"

Standard-oi is an ld special (see LD).  The accessor is
(standard-oi state) and the updater is (set-standard-oi val state).
Standard-oi must be an open object input channel, a true list of
objects, or a list of objects whose last cdr is an open object input
channel.  It is from this source that ld takes the input forms to
process.  When ld is called, if the value specified for standard-oi is
a string or a list of objects whose last cdr is a string, then ld
treats the string as a file name and opens an object input channel from
that file, where the connected book directory (see CBD) is used
to resolve relative pathnames.  The channel opened by ld is closed by
ld upon termination.

"Standard-oi" stands for "standard object input." The read-eval-print
loop in ld reads the objects in standard-oi and treats them as forms to
be evaluated.  The initial value of standard-oi is the same as the
value of *standard-oi* (see *STANDARD-OI*).

STANDARD-STRING-ALISTP    recognizer for association lists with standard strings as keys

(Standard-string-alistp x) is true if and only if x is a list of pairs
of the form (cons key val) where key is a string all of whose
characters are standard (see STANDARD-CHAR-P).

Standard-string-alistp has a guard of t.

STRING    coerce to a string

(String x) coerces x to a string.  If x is already a string, then it is
returned unchanged; if x is a symbol, then its symbol-name is returned;
and if x is a character, the corresponding one-character string is
returned.

The guard for string requires its argument to be a string, a symbol, or
a character.

String is a Common Lisp function.  See any Common Lisp documentation
for more information.

STRING-APPEND    concatenate two strings

String-append takes two arguments, which are both strings (if the guard
is to be met), and returns a string obtained concatenating together the
characters in the first string followed by those in the second.  Also
see CONCATENATE, noting that the macro call

     (concatenate 'string str1 str2).

expands to the call

     (string-append str1 str2).

STRING-DOWNCASE    in a given string, turn upper-case characters into lower-case

For a string x, (string-downcase x) is the result of applying
char-downcase to each character in x.

The guard for string-downcase requires its argument to be a string
containing only standard characters.

String-downcase is a Common Lisp function.  See any Common Lisp
documentation for more information.

STRING-EQUAL    string equality without regard to case

For strings str1 and str2, (string-equal str1 str2) is true if and only
str1 and str2 are the same except perhaps for the cases of their
characters.

The guard on string-equal requires that its arguments are strings
consisting of standard characters (see STANDARD-CHAR-LISTP).

String-equal is a Common Lisp function.  See any Common Lisp
documentation for more information.

STRING-LISTP    recognizer for a true list of strings

The predicate string-listp tests whether its argument is a true-listp
of strings.

STRING-UPCASE    in a given string, turn lower-case characters into upper-case

For a string x, (string-upcase x) is the result of applying char-upcase
to each character in x.

The guard for string-upcase requires its argument to be a string
containing only standard characters.

String-upcase is a Common Lisp function.  See any Common Lisp
documentation for more information.

STRING<    less-than test for strings

(String< str1 str2) is non-nil if and only if the string str1 precedes
the string str2 lexicographically, where character inequalities are
tested using char<.  When non-nil, (string< str1 str2) is the first
position (zero-based) at which the strings differ.  Here are some
examples.

     ACL2 !>(string< "abcd" "abu")
     2
     ACL2 !>(string< "abcd" "Abu")
     NIL
     ACL2 !>(string< "abc" "abcde")
     3
     ACL2 !>(string< "abcde" "abc")
     NIL

The guard for string< specifies that its arguments are strings.

String< is a Common Lisp function.  See any Common Lisp documentation
for more information.

STRING<=    less-than-or-equal test for strings

(String<= str1 str2) is non-nil if and only if the string str1 precedes
the string str2 lexicographically or the strings are equal.  When
non-nil, (string<= str1 str2) is the first position (zero-based) at
which the strings differ, if they differ, and otherwise is their common
length.  See STRING<.

The guard for string<= specifies that its arguments are strings.

String<= is a Common Lisp function.  See any Common Lisp documentation
for more information.

STRING>    greater-than test for strings

(String> str1 str2) is non-nil if and only if str2 precedes str1
lexicographically.  When non-nil, (string> str1 str2) is the first
position (zero-based) at which the strings differ.  See STRING<.

String> is a Common Lisp function.  See any Common Lisp documentation
for more information.

STRING>=    less-than-or-equal test for strings

(String>= str1 str2) is non-nil if and only if the string str2 precedes
the string str1 lexicographically or the strings are equal.  When
non-nil, (string>= str1 str2) is the first position (zero-based) at
which the strings differ, if they differ, and otherwise is their common
length.  See STRING>.

The guard for string>= specifies that its arguments are strings.

String>= is a Common Lisp function.  See any Common Lisp documentation
for more information.

STRINGP    recognizer for strings

(stringp x) is true if and only if x is a string.

STRIP-CARS    collect up all first components of pairs in a list

(strip-cars x) is the list obtained by walking through the list x and
collecting up all first components (cars).  This function is
implemented in a tail-recursive way, despite its logical definition.

(strip-cars x) has a guard of (alistp x).

STRIP-CDRS    collect up all second components of pairs in a list

(strip-cdrs x) has a guard of (alistp x), and returns the list obtained
by walking through the list x and collecting up all second components
(cdrs).  This function is implemented in a tail-recursive way, despite
its logical definition.

SUBLIS    substitute an alist into a tree

(Sublis alist tree) is obtained by replacing every leaf of tree with
the result of looking that leaf up in the association list alist.
However, a leaf is left unchanged if it is not found as a key in alist.

Leaves are lookup up using the function assoc.  The guard for (sublis
alist tree) requires (eqlable-alistp alist).  This guard ensures that
the guard for assoc will be met for each lookup generated by sublis.

Sublis is defined in Common Lisp.  See any Common Lisp documentation
for more information.

SUBSEQ    subsequence of a string or list

For any natural numbers start and end, where start <= end <= (length
seq), (subseq seq start end) is the subsequence of seq from index start
up to, but not including, index end.  End may be nil, which which case
it is treated as though it is (length seq), i.e., we obtain the
subsequence of seq from index start all the way to the end.

The guard for (subseq seq start end) is that seq is a true list or a
string, start and end are integers (except, end may be nil, in which
case it is treated as (length seq) for the rest of this discussion),
and 0 <= start <= end <= (length seq).

Subseq is a Common Lisp function.  See any Common Lisp documentation
for more information.  Note:  In Common Lisp the third argument of
subseq is optional, but in ACL2 it is required, though it may be nil as
explained above.

SUBSETP    test if every member of one list is a member of the other

(Subsetp x y) is true if and only if every member of the list x is a
member of the list y.

Membership is tested using the function member.  Thus, the guard for
subsetp requires that its arguments are true lists, and moreover, at
least one satisfies eqlable-listp.  This guard ensures that the guard
for member will be met for each call generated by subsetp.

Subsetp is defined in Common Lisp.  See any Common Lisp documentation
for more information.

SUBSETP-EQUAL    check if all members of one list are members of the other

(Subsetp-equal x y) returns t if every member of x is a member of y,
where membership is tested using member-equal.

The guard for subsetp-equal requires both arguments to be true lists.
Subsetp-equal has the same functionality as the Common Lisp function
subsetp, except that it uses the equal function to test membership
rather than eql.

SUBST    a single substitution into a tree

(Subst new old tree) is obtained by substituting new for every
occurence of old in the given tree.

Equality to old is determined using the function eql.  The guard for
(subst new old tree) requires (eqlablep old), which ensures that the
guard for eql will be met for each comparison generated by subst.

Subst is defined in Common Lisp.  See any Common Lisp documentation for
more information.

SUBSTITUTE    substitute into a string or a list, using eql as test

(Substitute new old seq) is the result of replacing each occurrence of
old in seq, which is a list or a string, with new.

The guard for substitute requires that either seq is a string and new
is a character, or else:  seq is a true-listp such that either all of
its members are eqlablep or old is eqlablep.

Substitute is a Common Lisp function.  See any Common Lisp
documentation for more information.  Since ACL2 functions cannot take
keyword arguments (though macros can), the test used in substitute is
eql.

SYMBOL-<    less-than test for symbols

(symbol-< x y) is non-nil if and only if either the symbol-name of the
symbol x lexicographially precedes the symbol-name of the symbol y (in
the sense of string<) or else the symbol-names are equal and the
symbol-package-name of x lexicographically precedes that of y (in the
same sense).  So for example, (symbol-< 'abcd 'abce) and (symbol-<
'acl2::abcd 'foo::abce) are true.

The guard for symbol specifies that its arguments are symbols.

SYMBOL-ALISTP    recognizer for association lists with symbols as keys

(Symbol-alistp x) is true if and only if x is a list of pairs of the
form (cons key val) where key is a symbolp.

SYMBOL-LISTP    recognizer for a true list of symbols

The predicate symbol-listp tests whether its argument is a true list of
symbols.

SYMBOL-NAME    the name of a symbol (a string)

Completion Axiom:

     (equal (symbol-name x)
            (if (symbolp x)
                (symbol-name x)
              ""))

Guard for (symbol-name x):

     (symbolp x)

SYMBOL-PACKAGE-NAME    the name of the package of a symbol (a string)

Completion Axiom:

     (equal (symbol-package-name x)
            (if (symbolp x)
                (symbol-package-name x)
              ""))

Guard for (symbol-package-name x):

     (symbolp x)

Note:  If the ACL2 image is built on GCL, then symbol-package-name
diverges from the name of the symbol's package in raw Lisp, in the case
that this package is the main Lisp package.  For example,
(symbol-package-name 'car) evaluates to "COMMON-LISP" regardless of of
the underlying Lisp implementation, even though the name of the main
Lisp package in GCL is "LISP".

SYMBOLP    recognizer for symbols

(symbolp x) is true if and only if x is a symbol.

SYS-CALL    make a system call to the host operating system

     Example Forms:
     (sys-call "cp" '("foo.lisp" "foo-copied.lisp"))
     (prog2$ (sys-call "cp" '("foo.lisp" "foo-copied.lisp"))
             (sys-call-status state))

The first argument of sys-call is a command for the host operating
system, and the second argument is a list of strings that are the
arguments for that command.  In GCL and perhaps other lisps, you can
put the arguments with the command; but this is not the case, for
example, in Allegro CL running on Linux.

The use of prog2$ above is optional, but illustrates a typical sort of
use when one wishes to get the return status.  See
SYS-CALL-STATUS.

     General Form:
     (sys-call cmd args)

This function logically returns nil.  However, it makes the indicated
call to the host operating system, as described above, using a function
supplied "under the hood" by the underlying Lisp system.  On occasions
where one wishes to obtain the numeric status returned by the host
operating system (or more precisely, by the Lisp function under the
hood that passes the system call to the host operating system), one may
do so;  see SYS-CALL-STATUS.  The status value is the value
returned by that Lisp function, which may well be the same numeric
value returned by the host operating system for the underlying system
call.

Note that sys-call does not touch the ACL2 state; however,
sys-call-status updates the file-clock field of the state.  One may
view that update as modifying the fileclock to be at least as recent as
the time of the most recent sys-call.

Be careful if you use sys-call!  It can be used for example to overwrite
files, or worse!  The following example from Bob Boyer shows how to use
sys-call to execute, in effect, arbitrary Lisp forms.  ACL2 provides a
"trust tag" mechanism that requires execution of a defttag form before
you can use sys-call; see DEFTTAG.  (Note: The setting of the
raw Lisp variable *features* below is just to illustrate that any such
mischief is possible.  Normally *features* is a list with more than a
few elements.)

     % cat foo
     print *0x85d2064=0x838E920
     detach
     q
     % acl2
     ... boilerplate deleted
     ACL2 !>(sys-call "gdb -p $PPID -w < foo >& /dev/null " nil)
     NIL
     ACL2 !>:q

     Exiting the ACL2 read-eval-print loop.  To re-enter, execute (LP).
     ACL2>*features*

     (:AKCL-SET-MV)

     ACL2>

Finally, we make a comment about output redirection, which also applies
to other related features that one may expect of a shell.  Sys-call
does not directly support output redirection.  If you want to run a
program, P, and redirect its output, we suggest that you create a
wrapper script, W to call instead.  Thus W might be a shell script
containing the line:

     P $* >& foo.out

If this sort of solution proves inadequate, please contact the ACL2
implementors and perhaps we can come up with a solution.

SYS-CALL-STATUS    exit status from the preceding system call

This function returns two values, (mv status state).  The first is the
status returned by the most recent invocation of function sys-call; see
SYS-CALL.  The second is the ACL2 state object, which is also
the input to this function.

The function sys-call makes a system call to the host operating system
using a function supplied "under the hood" by the underlying Lisp
system.  The status value is the value returned by that Lisp function,
which may well be the same numeric value returned by the host operating
system for the underlying system call.  For more information, see
SYS-CALL.

TAKE    initial segment of a list

For any natural number n not exceeding the length of l, (take n l)
collects the first n elements of the list l.

The following is a theorem (though it takes some effort, including
lemmas, to get ACL2 to prove it):

     (equal (length (take n l)) (nfix n))

If n is is an integer greater than the length of l, then take pads the
list with the appropriate number of nil elements.  Thus, the following
is also a theorem.

     (implies (and (integerp n)
                   (true-listp l)
                   (<= (length l) n))
              (equal (take n l)
                     (append l (make-list (- n (length l))))))

For related functions, see NTHCDR and see BUTLAST.

The guard for (take n l) is that n is a nonnegative integer and l is a
true list.

TENTH    tenth member of the list

See any Common Lisp documentation for details.

THE    run-time type check

(The typ val) checks that val satisfies the type specification typ (see
TYPE-SPEC).  An error is caused if the check fails, and
otherwise, val is the value of this expression.  Here are some examples.

     (the integer 3)       ; returns 3
     (the (integer 0 6) 3) ; returns 3
     (the (integer 0 6) 7) ; causes an error

See TYPE-SPEC for a discussion of the legal type specifications.

The is defined in Common Lisp.  See any Common Lisp documentation for
more information.

THIRD    third member of the list

See any Common Lisp documentation for details.

TRUE-LIST-LISTP    recognizer for true (proper) lists of true lists

True-list-listp is the function that checks whether its argument is a
list that ends in, or equals, nil, and furthermore, all of its elements
have that property.  Also see TRUE-LISTP.

TRUE-LISTP    recognizer for proper (null-terminated) lists

True-listp is the function that checks whether its argument is a list
that ends in, or equals, nil.

TRUNCATE    division returning an integer by truncating toward 0

     Example Forms:
     ACL2 !>(truncate 14 3)
     4
     ACL2 !>(truncate -14 3)
     -4
     ACL2 !>(truncate 14 -3)
     -4
     ACL2 !>(truncate -14 -3)
     4
     ACL2 !>(truncate -15 -3)
     5

(Truncate i j) is the result of taking the quotient of i and j and
dropping the fraction.  For example, the quotient of -14 by 3 is -4
2/3, so dropping the fraction 2/3, we obtain a result for (truncate -14
3) of -4.

The guard for (truncate i j) requires that i and j are rational (real,
in ACL2(r)) numbers and j is non-zero.

Truncate is a Common Lisp function.  However, note that unlike Common
Lisp, the ACL2 truncate function returns only a single value,

TYPE    See DECLARE.

TYPE-SPEC    type specifiers in declarations

     Examples:
     The symbol INTEGER in (declare (type INTEGER i j k)) is a type-spec.  Other
     type-specs supported by ACL2 include RATIONAL, COMPLEX, (INTEGER 0 127),
     (RATIONAL 1 *), CHARACTER, and ATOM.

The type-specs and their meanings (when applied to the variable x as in
(declare (type type-spec x)) are given below.

     type-spec              meaning
     (AND type1 ... typek)  (AND (p1 X) ... (pk X))
                            where (pj x) is the meaning for type-spec typej
     ATOM                   (ATOM X)
     BIT                    (OR (EQUAL X 1) (EQUAL X 0))
     CHARACTER              (CHARACTERP X)
     COMPLEX,               (AND (COMPLEX-RATIONALP X)
     (COMPLEX RATIONAL)          (RATIONALP (REALPART X))
                                 (RATIONALP (IMAGPART X)))
     (COMPLEX type)         (AND (COMPLEX-RATIONALP X)
                                 (p (REALPART X))
                                 (p (IMAGPART X)))
                            where (p x) is the meaning for type-spec type
     CONS                   (CONSP X)
     INTEGER                (INTEGERP X)
     (INTEGER i j)          (AND (INTEGERP X)   ; See notes below
                                 (<= i X)
                                 (<= X j))
     (MEMBER x1 ... xn)     (MEMBER X '(x1 ... xn))
     (MOD i)                same as (INTEGER 0 i-1)
     NIL                    NIL
     (NOT type)             (NOT (p X))
                            where (p x) is the meaning for type-spec type
     NULL                   (EQ X NIL)
     (OR type1 ... typek)   (OR (p1 X) ... (pk X))
                            where (pj x) is the meaning for type-spec typej
     RATIO                  (AND (RATIONALP X) (NOT (INTEGERP X)))
     RATIONAL               (RATIONALP X)
     (RATIONAL i j)         (AND (RATIONALP X)  ; See notes below
                                 (<= i X)
                                 (<= X j))
     REAL                   (RATIONALP X)       ; (REALP X) in ACL2(r)
     (REAL i j)             (AND (RATIONALP X)  ; See notes below
                                 (<= i X)
                                 (<= X j))
     (SATISFIES pred)       (pred X) ; Lisp requires a unary function, not a macro
     SIGNED-BYTE            (INTEGERP X)
     (SIGNED-BYTE i)        same as (INTEGER -2**i-1 (2**i-1)-1)
     STANDARD-CHAR          (STANDARD-CHARP X)
     STRING                 (STRINGP X)
     (STRING max)           (AND (STRINGP X) (EQUAL (LENGTH X) max))
     SYMBOL                 (SYMBOLP X)
     T                      T
     UNSIGNED-BYTE          same as (INTEGER 0 *)
     (UNSIGNED-BYTE i)      same as (INTEGER 0 (2**i)-1)

_Notes:_

In general, (integer i j) means

          (AND (INTEGERP X)
               (<= i X)
               (<= X j)).

But if i is the symbol *, the first inequality is omitted.  If j is the
symbol *, the second inequality is omitted.  If instead of being an
integer, the second element of the type specification is a list
containing an integer, (i), then the first inequality is made strict.
An analogous remark holds for the (j) case.  The RATIONAL and REAL type
specifiers are similarly generalized.

UNARY-    arithmetic negation function

Completion Axiom:

     (equal (unary-- x)
            (if (acl2-numberp x)
                (unary-- x)
              0))

Guard for (unary- x):

     (acl2-numberp x)

Notice that like all arithmetic functions, unary- treats non-numeric
inputs as 0.

Calls of the macro - on one argument expand to calls of unary-; see
-.

UNARY-/    reciprocal function

Completion Axiom:

     (equal (unary-/ x)
            (if (and (acl2-numberp x)
                     (not (equal x 0)))
                (unary-/ x)
              0))

Guard for (unary-/ x):

     (and (acl2-numberp x)
          (not (equal x 0)))

Notice that like all arithmetic functions, unary-/ treats non-numeric
inputs as 0.

Calls of the macro / on one argument expand to calls of unary-/; see
/.

UNION-EQ    union of two lists of symbols

(Union-eq x y) equals a list whose members (see MEMBER-EQ)
contains the members of x and the members of y.  More precisely, the
resulting list is the same as one would get by first deleting the
members of y from x, and then concatenating the result to the front of
y.

The guard for union-eq requires both arguments to be true lists, but in
fact further requires the first list to contain only symbols, as the
function member-eq is used to test membership (with eq).  See
UNION-EQUAL.

UNION-EQUAL    union of two lists

(Union-equal x y) equals a list whose members (see
MEMBER-EQUAL) contains the members of x and the members of y.  More
precisely, the resulting list is the same as one would get by first
deleting the members of y from x, and then concatenating the result to
the front of y.

The guard for union-equal requires both arguments to be true lists.
Essentially, union-equal has the same functionality as the Common Lisp
function union, except that it uses the equal function to test
membership rather than eql.  However, we do not include the function
union in ACL2, because the Common Lisp language does not specify the
order of the elements in the list that it returns.

UPDATE-NTH    modify a list by putting the given value at the given position

(Update-nth key val l) returns a list that is the same as the list l,
except that the value at the 0-based position key (a natural number) is
val.

If key is an integer at least as large as the length of l, then l will
be padded with the appropriate number of nil elements, as illustrated
by the following example.

     ACL2 !>(update-nth 8 'z '(a b c d e))
     (A B C D E NIL NIL NIL Z)

We have the following theorem.

     (implies (and (true-listp l)
                   (integerp key)
                   (<= 0 key))
              (equal (length (update-nth key val l))
                     (if (< key (length l))
                         (length l)
                       (+ 1 key))))

The guard of update-nth requires that its first (position) argument is
a natural number and its last (list) argument is a true list.

UPPER-CASE-P    recognizer for upper case characters

(Upper-case-p x) is true if and only if x is an upper case character,
i.e., a member of the list #A, #B, ..., #Z.

The guard for upper-case-p requires its argument to be a standard
character (see STANDARD-CHAR-P).

Upper-case-p is a Common Lisp function.  See any Common Lisp
documentation for more information.

WRITE-BYTE$    See IO.

XOR    logical "exclusive or"

Xor is the ACL2 exclusive-or function.  (xor P Q) means that either P
or Q, but not both, is false (i.e., nil).

ZERO-TEST-IDIOMS    how to test for 0

Below are six commonly used idioms for testing whether x is 0.  Zip and
zp are the preferred termination tests for recursions down the integers
and naturals, respectively.

     idiom       logical              guard                 primary
                 meaning                                 compiled code*

     (equal x 0) (equal x 0)          t                   (equal x 0)

     (eql x 0)   (equal x 0)          t                   (eql x 0)

     (zerop x)   (equal x 0)          x is a number       (= x 0)

     (= x 0)     (equal x 0)          x is a number       (= x 0)

     (zip x)     (equal (ifix x) 0)   x is an integer     (= x 0)

     (zp x)      (equal (nfix x) 0)   x is a natural      (int= x 0)

     (zpf x)     (equal (nfix x) 0)   x is a fixnum >= 0  (eql (the-fixnum x) 0)

*See GUARDS-AND-EVALUATION, especially the subsection titled
"Guards and evaluation V: efficiency issues".  Primary code is relevant
only if guards are verified.  The "compiled code" shown is only
suggestive.

The first four idioms all have the same logical meaning and differ only
with respect to their executability and efficiency.  In the absence of
compiler optimizing, (= x 0) is probably the most efficient, (equal x
0) is probably the least efficient, and (eql x 0) is in between.
However, an optimizing compiler could always choose to compile (equal x
0) as (eql x 0) and, in situations where x is known at compile-time to
be numeric, (eql x 0) as (= x 0).  So efficiency considerations must, of
course, be made in the context of the host compiler.

Note also that (zerop x) and (= x 0) are indistinguishable.  They have
the same meaning and the same guard, and can reasonably be expected to
generate equally efficient code.

Note that (zip x) and (zp x) do not have the same logical meanings as
the others or each other.  They are not simple tests for equality to 0.
They each coerce x into a restricted domain, zip to the integers and
zp to the natural numbers, choosing 0 for x when x is outside the
domain.  Thus, 1/2, #c(1 3), and 'abc, for example, are all
"recognized" as zero by both zip and zp.  But zip reports that -1 is
different from 0 while zp reports that -1 "is" 0.  More precisely, (zip
-1) is nil while (zp -1) is t.

Note that the last five idioms all have guards that restrict their
Common Lisp executability.  If these last five are used in situations
in which guards are to be verified, then proof obligations are incurred
as the price of using them.  If guard verification is not involved in
your project, then the first five can be thought of as synonymous.

Zip and zp are not provided by Common Lisp but are ACL2-specific
functions.  Why does ACL2 provide these functions?  The answer has to
do with the admission of recursively defined functions and efficiency.
Zp is provided as the zero-test in situations where the controlling
formal parameter is understood to be a natural number.  Zip is
analogously provided for the integer case.  We illustrate below.

Here is an admissible definition of factorial

     (defun fact (n) (if (zp n) 1 (* n (fact (1- n)))))

Observe the classic recursion scheme: a test against 0 and recursion by
1-.  Note however that the test against 0 is expressed with the zp
idiom.  Note also the absence of a guard making explicit our intention
that n is a natural number.

This definition of factorial is readily admitted because when (zp n)

is false (i.e., nil) then n is a natural number other than 0 and so (1-
n) is less than n.  The base case, where (zp n) is true, handles all
the "unexpected" inputs, such as arise with (fact -1) and (fact 'abc).
When calls of fact are evaluated, (zp n) checks (integerp n) and (> n
0).  Guard verification is unsuccessful for this definition of fact
because zp requires its argument to be a natural number and there is no
guard on fact, above.  Thus the primary raw lisp for fact is
inaccessible and only the :logic definition (which does runtime "type"
checking) is used in computation.  In summary, this definition of
factorial is easily admitted and easily manipulated by the prover but
is not executed as efficiently as it could be.

Runtime efficiency can be improved by adding a guard to the definition.

     (defun fact (n)
       (declare (xargs :guard (and (integerp n) (>= n 0))))
       (if (zp n) 1 (* n (fact (1- n)))))

This guarded definition has the same termination conditions as before -
termination is not sensitive to the guard.  But the guards can be
verified.  This makes the primary raw lisp definition accessible during
execution.  In that definition, the (zp n) above is compiled as (= n
0), because n will always be a natural number when the primary code is
executed.  Thus, by adding a guard and verifying it, the elegant and
easily used definition of factorial is also efficiently executed on
natural numbers.

Now let us consider an alternative definition of factorial in which (=
n 0) is used in place of (zp n).

     (defun fact (n) (if (= n 0) 1 (* n (fact (1- n)))))

This definition does not terminate.  For example (fact -1) gives rise
to a call of (fact -2), etc.  Hence, this alternative is inadmissible.
A plausible response is the addition of a guard restricting n to the
naturals:

     (defun fact (n)
      (declare (xargs :guard (and (integerp n) (>= n 0))))
      (if (= n 0) 1 (* n (fact (1- n)))))

But because the termination argument is not sensitive to the guard, it
is still impossible to admit this definition.  To influence the
termination argument one must change the conditions tested.  Adding a
runtime test that n is a natural number would suffice and allow both
admission and guard verification.  But such a test would slow down the
execution of the compiled function.

The use of (zp n) as the test avoids this dilemma.  Zp provides the
logical equivalent of a runtime test that n is a natural number but the
execution efficiency of a direct = comparison with 0, at the expense of
a guard conjecture to prove.  In addition, if guard verification and
most-efficient execution are not needed, then the use of (zp n) allows
the admission of the function without a guard or other extraneous
verbiage.

While general rules are made to be broken, it is probably a good idea
to get into the habit of using (zp n) as your terminating "0 test"
idiom when recursing down the natural numbers.  It provides the logical
power of testing that n is a non-0 natural number and allows efficient
execution.

We now turn to the analogous function, zip.  Zip is the preferred
0-test idiom when recursing through the integers toward 0.  Zip
considers any non-integer to be 0 and otherwise just recognizes 0.  A
typical use of zip is in the definition of integer-length, shown below.
(ACL2 can actually accept this definition, but only after appropriate
lemmas have been proved.)

     (defun integer-length (i)
       (declare (xargs :guard (integerp i)))
       (if (zip i)
           0
         (if (= i -1)
           0
           (+ 1 (integer-length (floor i 2))))))

Observe that the function recurses by (floor i 2).  Hence, calling the
function on 25 causes calls on 12, 6, 3, 1, and 0, while calling it on
-25 generates calls on -13, -7, -4, -2, and -1.  By making (zip i) the
first test, we terminate the recursion immediately on non-integers.
The guard, if present, can be verified and allows the primary raw lisp
definition to check (= i 0) as the first terminating condition (because
the primary code is executed only on integers).

ZEROP    test an acl2-number against 0

(zerop x) is t if x is 0 and is nil otherwise.  Thus, it is logically
equivalent to (equal x 0).

(Zerop x) has a guard requiring x to be numeric and can be expected to
execute more efficiently than (equal x 0) in properly guarded compiled
code.

In recursions down the natural numbers, (zp x) is preferred over (zerop
x) because the former coerces x to a natural and allows the termination
proof.  In recursions through the integers, (zip x) is preferred.  See
ZERO-TEST-IDIOMS.

Zerop is a Common Lisp function.  See any Common Lisp documentation for
more information.

ZIP    testing an "integer" against 0

(Zip i) is logically equivalent to (equal (ifix i) 0) and is the
preferred termination test for recursion through the integers.  (Zip i)
returns t if i is 0 or not an integer; it returns nil otherwise.  Thus,

        i         (zip i)
        3         nil
        0         t
        -2        nil
        5/2       t
        #c(1 3)   t
        'abc      t

(Zip i) has a guard requiring i to be an integer.

For a discussion of the various idioms for testing against 0, see
ZERO-TEST-IDIOMS.

Zip is typically used as the termination test in recursions through the
integers.  It has the advantage of "coercing" its argument to an
integer and hence allows the definition to be admitted without an
explicit type check in the body.  Guard verification allows zip to be
compiled as a direct =-comparision with 0.

ZP    testing a "natural" against 0

(Zp n) is logically equivalent to (equal (nfix n) 0) and is the
preferred termination test for recursion down the natural numbers. (Zp
n) returns t if n is 0 or not a natural number; it returns nil
otherwise.  Thus, in the ACL2 logic (ignoring the issue of guards):

         n       (zp n)
        3         nil
        0         t
        -1        t
        5/2       t
        #c(1 3)   t
        'abc      t

(Zp n) has a guard requiring n to be a natural number.

For a discussion of the various idioms for testing against 0, see
ZERO-TEST-IDIOMS.

Zp is typically used as the termination test in recursions down the
natural numbers.  It has the advantage of "coercing" its argument to a
natural and hence allows the definition to be admitted without an
explicit type check in the body.  Guard verification allows zp to be
compiled as a direct =-comparision with 0.

ZPF    testing a nonnegative fixnum against 0

Zpf is exactly the same as zp, except that zpf is intended for, and
faster for, fixnum arguments.  Its guard is specified with a type
declaration, (type (unsigned-byte 29) x).  (See DECLARE and see
TYPE-SPEC.)  Also see ZP.

PROOF-CHECKER    support for low-level interaction

Call this up with (verify ...).

This is an interactive system for checking theorems in ACL2.  One
enters it using VERIFY; see VERIFY.  The result of an
interactive session is a defthm event with an :instructions parameter
supplied; see the documentation for proof-checker command exit (in
package "ACL2-PC").  Such an event can be replayed later in a new ACL2
session with the "proof-checker" loaded.

A tutorial is available on the world-wide web:
`http://www.cs.utexas.edu/users/kaufmann/tutorial/rev3.html'.
The tutorial illustrates more than just the proof-checker.  The portion
relevant to the proof-checker may be accessed directly:
`http://www.cs.utexas.edu/users/kaufmann/tutorial/rev3.html#slide29'

See SET-EVISC-TUPLE for how to arrange that output is printed
in abbreviated form.  In general, the proof-checker uses the :TERM
evisc-tuple described in that documentation.

Individual proof-checker commands are documented in subsection
proof-checker-commands.

DEFINE-PC-HELP    define a macro command whose purpose is to print something

     Example:
     (define-pc-help pp ()
       (if (goals t)
           (io? proof-checker nil state
                (state-stack)
                (fms0 "~|~y0~|"
                      (list (cons #0
                                  (fetch-term (conc t)
                                              (current-addr t))))))
         (print-all-goals-proved-message state)))

     General Form:
     (define-pc-help name args &rest body)

This defines a macro command named name, as explained further below.
The body should (after removing optional declarations) be a form that
returns state as its single value.   Typically, it will just print
something.

What (define-pc-help name args &rest body) really does is to create a
call of define-pc-macro that defines name to take arguments args, to
have the declarations indicated by all but the last form in body, and
to have a body that (via pprogn) first executes the form in the last
element of body and then returns a call to the command skip (which will
return (mv nil t state)).

DEFINE-PC-MACRO    define a proof-checker macro command

     Example:
     (define-pc-macro ib (&optional term)
       (value
        (if term
            `(then (induct ,term) bash)
          `(then induct bash))))

The example above captures a common paradigm:  one attempts to prove
the current goal by inducting and then simplifying the resulting goals.
(see PROOF-CHECKER-COMMANDS for documentation of the command
then, which is itself a pc-macro command, and commands induct and
bash.)  Rather than issuing (then induct bash), or worse yet issuing
induct and then issuing bash for each resulting goals, the above
definition of ib would let you issue ib and get the same effect.

     General Form:
     (define-pc-macro cmd args doc-string dcl ... dcl body)

where cmd is the name of the pc-macro than you want to define, args is
its list of formal parameters.  Args may include lambda-list keywords
&optional and &rest; see MACRO-ARGS, but note that here, args
may not include &key or &whole.

The value of body should be an ACL2 "error triple," i.e., have the form
(mv erp xxx state) for some erp and xxx.  If erp is nil, then xxx is
handed off to the proof-checker's instruction interpreter.  Otherwise,
evaluation typically halts.  We may write more on the full story later
if there is interest in reading it.

DEFINE-PC-META    define a proof-checker meta command

Built-in proof-checker meta commands include undo and restore, and
others (lisp, exit, and sequence); see PROOF-CHECKER-COMMANDS.
The advanced proof-checker user can define these as well.  See ACL2
source file proof-checker-b.lisp for examples, and contact the ACL2
implementors if those examples do not provide sufficient documentation.

INSTRUCTIONS    instructions to the proof checker

     Example:
     :instructions (induct prove promote (dive 1) x
                           (dive 2) = top (drop 2) prove)

See DEFTHM for the role of :instructions in place of :hints.
As illustrated by the example above, the value associated with
:instructions is a list of proof-checker commands.  At the moment the
best way to understand the idea of the interactive proof-checker (see
PROOF-CHECKER and see VERIFY) is probably to read the
first 11 pages of CLI Technical Report 19, which describes the
corresponding facility for Nqthm.

When inside the interactive loop (i.e., after executing verify), use
help to get a list of legal instructions and (help instr) to get help
for the instruction instr.

MACRO-COMMAND    compound command for the proof-checker

The proof-checker (see PROOF-CHECKER) allows the user to supply
interactive commands.  Compound commands, called macro commands, may be
defined; these expand into zero or more other commands.  Some of these
are "atomic" macro commands; these are viewed as a single command step
when completed successfully.

More documentation will be written on the proof-checker.  For now, we
simply point out that there are lots of examples of the use of
define-pc-macro and define-pc-atomic-macro in the ACL2 source file
"proof-checker-b.lisp".  The former is used to create macro commands,
which can be submitted to the interactive loop (see VERIFY) and
will "expand" into zero or more commands.  The latter is similar,
except that the undoing mechanism (see ACL2-PC||UNDO)
understands atomic macro commands to represent single interactive
commands.  Also see ACL2-PC||COMM and see
ACL2-PC||COMMANDS for a discussion of the display of interactive
commands.

Also see TOGGLE-PC-MACRO for how to change a macro command to
an atomic macro command, and vice versa.

PROOF-CHECKER-COMMANDS    list of commands for the proof-checker

This documentation section contains documentation for individual
commands that can be given inside the interactive proof-checker loop
that is entered using verify.

attempt an equality (or equivalence) substitution

same as (lisp x)

add an abbreviation

call the ACL2 theorem prover's simplifier

prove the current goal using bdds

move backward one argument in the enclosing term

insert matching ``bookends'' comments

split into two cases

change to another goal.

change to another goal.

same as clause-processor

add a new hypothesis

use a clause-processor

display instructions from the current interactive session

display instructions from the current interactive session

insert a comment

same as contrapose

switch a hypothesis with the conclusion, negating both

move top-level hypotheses to the conclusion

move to the indicated subterm

run the given instructions

run the given instructions, halting once there is a ``failure''

run the given instructions, halting once there is a ``failure''

drop top-level hypotheses

move to the indicated subterm

call the ACL2 theorem prover's elimination process

attempt an equality (or congruence-based) substitution

exit after possibly saving the state

exit the interactive proof-checker

expand the current function call without simplification

cause a failure

forward chain from an implication in the hyps

create a ``free variable''

perform a generalization

list the names of goals on the stack

proof-checker help facility

proof-checker help facility

same as help!

print the hypotheses

illegal instruction

set the current proof-checker theory

generate subgoals using induction

print the runes (definitions, lemmas, ...) used

evaluate the given form in Lisp

proof-checker help facility

proof-checker help facility

run the given instructions, and ``succeed'' if and only if they ``fail''

used for interpreting control-d

run instructions with output

move forward one argument in the enclosing term

run the first instruction; if (and only if) it ``fails'', run the
second

prettyprint the current term

prettyprint the conclusion, highlighting the current term

prettyprint the current term

print the result of evaluating the given form

print all the conclusions of (as yet unproved) goals

print all the (as yet unproved) goals

print the original goal

repeatedly apply promote

move antecedents of conclusion's implies term to top-level
hypotheses

run the given instructions, reverting to existing state upon
failure

call the ACL2 theorem prover to prove the current goal

print the most recent proof attempt from inside the proof-checker

print the most recent proof attempt from inside the proof-checker

print the most recent proof attempt from inside the proof-checker

substitute for a ``free variable''

run instructions without output

same as rewrite

call the ACL2 theorem prover's simplifier

call the ACL2 prover without induction, after going into
induction

remove one or more abbreviations

repeat the given instruction until it ``fails''

auxiliary to repeat

replay one or more instructions

remove the effect of an UNDO command

drop all *but* the indicated top-level hypotheses

re-enter the proof-checker

apply a rewrite rule

auxiliary to THEN

auxiliary to then

print the runes (definitions, lemmas, ...) used

simplify the current subterm

simplify propositionally

save the proof-checker state (state-stack)

run the given list of instructions according to a multitude of
options

display the current abbreviations

display the applicable rewrite rules

``succeed'' without doing anything

simplify with lemmas

split the current goal into cases

same as SHOW-REWRITES

run the given instructions, and ``succeed''

print the top-level hypotheses and the current subterm

apply one instruction to current goal and another to new subgoals

move to the top of the goal

display the type-alist from the current context

undo some instructions

remove a proof-checker state

move to the parent (or some ancestor) of the current subterm

use a lemma instance

execute the indicated instructions and combine all the new goals

same as induct, but create a single goal

combine goals into a single goal

expand and (maybe) simplify function call at the current subterm

expand function call at the current subterm, without simplifying

ACL2-PC||=    (atomic macro)
attempt an equality (or equivalence) substitution

     Examples:
     =     -- replace the current subterm by a term equated to it in
              one of the hypotheses (if such a term exists)
     (= x) -- replace the current subterm by x, assuming that the prover
              can show that they are equal
     (= (+ x y) z)
           -- replace the term (+ x y) by the term z inside the current
              subterm, assuming that the prover can prove
              (equal (+ x y) z) from the current top-level hypotheses
              or that this term or (equal z (+ x y)) is among the
              current top-level hypotheses or the current governors
     (= & z)
           -- exactly the same as above, if (+ x y) is the current
              subterm
     (= (+ x y) z :hints :none)
           -- same as (= (+ x y) z), except that a new subgoal is
              created with the current goal's hypotheses and governors
              as its top-level hypotheses and (equal (+ x y) z) as its
              conclusion
     (= (+ x y) z 0)
           -- exactly the same as immediately above
     (= (p x)
        (p y)
        :equiv iff
        :otf-flg t
        :hints (("Subgoal 2" :BY FOO) ("Subgoal 1" :use bar)))
           -- same as (= (+ x y) z), except that the prover uses
              the indicated values for otf-flg and hints, and only
              propositional (iff) equivalence is used (however, it
              must be that only propositional equivalence matters at
              the current subterm)

     General Form:
     (= &optional x y &rest keyword-args)

If terms x and y are supplied, then replace x by y inside the current
subterm if they are "known" to be "equal".  Here "known" means the
following:  the prover is called as in the prove command (using
keyword-args) to prove (equal x y), except that a keyword argument
:equiv is allowed, in which case (equiv x y) is proved instead, where
equiv is that argument.  (See below for how governors are handled.)

Actually, keyword-args is either a single non-keyword or is a list of
the form ((kw-1 x-1) ... (kw-n x-n)), where each kw-i is one of the
keywords :equiv, :otf-flg, :hints.  Here :equiv defaults to equal if
the argument is not supplied or is nil, and otherwise should be the
name of an ACL2 equivalence relation.  :Otf-flg and :hints give
directives to the prover, as explained above and in the documentation
for the prove command; however, no prover call is made if :hints is a
non-nil atom or if keyword-args is a single non-keyword (more on this
below).

_Remarks on defaults_

(1) If there is only one argument, say a, then x defaults to the
current subterm, in the sense that x is taken to be the current subterm
and y is taken to be a.

(2) If there are at least two arguments, then x may be the symbol &,
which then represents the current subterm.  Thus, (= a) is equivalent
to (= & a).  (Obscure point:  actually, & can be in any package, except
the keyword package.)

(3) If there are no arguments, then we look for a top-level hypothesis
or a governor of the form (equal c u) or (equal u c), where c is the
current subterm.  In that case we replace the current subterm by u.

As with the prove command, we allow goals to be given "bye"s in the
proof, which may be generated by a :hints keyword argument in
keyword-args.  These result in the creation of new subgoals.

A proof is attempted unless the :hints argument is a non-nil atom other
than :none, or unless there is one element of keyword-args and it is
not a keyword.  In that case, if there are any hypotheses in the
current goal, then what is attempted is a proof of the implication
whose antecedent is the conjunction of the current hypotheses and
governors and whose conclusion is the appropriate equal term.

*Remarks:*  (1) It is allowed to use abbreviations in the hints.  (2)
The keyword :none has the special role as a value of :hints that is
shown clearly in an example above.  (3) If there are governors, then
the new subgoal has as additional hypotheses the current governors.

ACL2-PC||ACL2-WRAP    (macro)
same as (lisp x)

     Example:
     (acl2-wrap (pe :here))

     General Form:
     (acl2-wrap form)

Same as (lisp form).  This is provided for interface tools that want to
be able to execute the same form in raw Lisp, in the proof-checker, or
in the ACL2 top-level loop (lp).

ACL2-PC||ADD-ABBREVIATION    (primitive)
add an abbreviation

Example:  (add-abbreviation v (* x y)) causes future occurrences of (*
x y) to be printed as (? v), until (unless) a corresponding invocation
of remove-abbreviations occurs.  In this case we say that v
"abbreviates" (* x y).

     General Form:
     (add-abbreviation var &optional raw-term)

Let var be an abbreviation for raw-term, if raw-term is supplied, else
for the current subterm.  Note that var must be a variable that does
not already abbreviate some term.

A way to think of abbreviations is as follows.  Imagine that whenever
an abbreviation is added, say v abbreviates expr, an entry associating
v to expr is made in an association list, which we will call
"*abbreviations-alist*".  Then simply imagine that ? is a function
defined by something like:

     (defun ? (v)
       (let ((pair (assoc v *abbreviations-alist*)))
         (if pair (cdr pair)
           (error ...))))

Of course the implementation isn't exactly like that, since the
"constant" *abbreviations-alist* actually changes each time an
add-abbreviation instruction is successfully invoked.  Nevertheless, if
one imagines an appropriate redefinition of the "constant"
*abbreviations-alist* each time an add-abbreviation is invoked, then
one will have a clear model of the meaning of such an instruction.

The effect of abbreviations on output is that before printing a term,
each subterm that is abbreviated by a variable v is first replaced by
(? v).

The effect of abbreviations on input is that every built-in
proof-checker command accepts abbreviations wherever a term is expected
as an argument, i.e., accepts the syntax (? v) whenever v abbreviates a
term.  For example, the second argument of add-abbreviation may itself
use abbreviations that have been defined by previous add-abbreviation
instructions.

See also remove-abbreviations and show-abbreviations.

ACL2-PC||BASH    (atomic macro)
call the ACL2 theorem prover's simplifier

     Examples:
     bash -- attempt to prove the current goal by simplification alone
     (bash ("Subgoal 2" :by foo) ("Subgoal 1" :use bar))
          -- attempt to prove the current goal by simplification alone,
             with the indicated hints

     General Form:
     (bash &rest hints)

Call the theorem prover's simplifier, creating a subgoal for each
resulting goal.

Notice that unlike prove, the arguments to bash are spread out, and are
all hints.

Bash is similar to reduce in that neither of these allows induction.
But bash only allows simplification, while reduce allows processes
eliminate-destructors, fertilize, generalize, and eliminate-irrelevance.

*Remark:*  All forcing rounds will be skipped (unless there are more
than 15 subgoals generated in the first forcing round, an injustice
that should be rectified by the next release).

ACL2-PC||BDD    (atomic macro)
prove the current goal using bdds

     Examples:
     bdd
     (bdd :vars nil :bdd-constructors (cons) :prove t :literal :all)

The general form is as shown in the latter example above, but with any
keyword-value pairs omitted and with values as described for the :bdd
hint; see HINTS.

This command simply calls the theorem prover with the indicated bdd
hint for the top-level goal.  Note that if :prove is t (the default),
then the proof will succeed entirely using bdds or else it will fail
immediately.  See BDD.

ACL2-PC||BK    (atomic macro)
move backward one argument in the enclosing term

     Example and General Form:
     bk

For example, if the conclusion is (= x (* (- y) z)) and the current
subterm is (* (- y) z), then after executing bk, the current subterm
will be x.

Move to the previous argument of the enclosing term.

This is the same as up followed by (dive n-1), where n is the position
of the current subterm in its parent term in the conclusion.  Thus in
particular, the nx command fails if one is already at the top of the
conclusion.

See also up, dive, top, and bk.

ACL2-PC||BOOKMARK    (macro)
insert matching "bookends" comments

     Example:
     (bookmark final-goal)

     General Form:
     (bookmark name &rest instruction-list)

Run the instructions in instruction-list (as though this were a call of
do-all; see the documentation for do-all), but first insert a begin
bookend with the given name and then, when the instructions have been
completed, insert an end bookend with that same name.  See the
documentation of comm for an explanation of bookends and how they can
affect the display of instructions.

ACL2-PC||CASESPLIT    (primitive)
split into two cases

     Example:
     (casesplit (< x y)) -- assuming that we are at the top of the
                            conclusion, add (< x y) as a new top-level
                            hypothesis in the current goal, and create a
                            subgoal identical to the current goal except
                            that it has (not (< x y)) as a new top-level
                            hypothesis

     General Form:
     (casesplit expr &optional use-hyps-flag do-not-flatten-flag)

When the current subterm is the entire conclusion, this instruction
adds expr as a new top-level hypothesis, and create a subgoal identical
to the existing current goal except that it has the negation of expr as
a new top-level hypothesis.  See also claim.  The optional arguments
control the use of governors and the "flattening" of new hypotheses, as
we now explain.

The argument use-hyps-flag is only of interest when there are
governors.  (To read about governors, see the documentation for the
command hyps).  In that case, if use-hyps-flag is not supplied or is
nil, then the description above is correct; but otherwise, it is not
expr but rather it is (implies govs expr) that is added as a new
top-level hypothesis (and whose negation is added as a top-level
hypothesis for the new goal), where govs is the conjunction of the
governors.

If do-not-flatten-flag is supplied and not nil, then that is all there
is to this command.  Otherwise (thus this is the default), when the
claimed term (first argument) is a conjunction (and) of terms and the
claim instruction succeeds, then each (nested) conjunct of the claimed
term is added as a separate new top-level hypothesis.  Consider the
following example, assuming there are no governors.

     (casesplit (and (and (< x y) (integerp a)) (equal r s)) t)

Three new top-level hypotheses are added to the current goal, namely (<
x y), (integerp a), and (equal r s).  In that case, only one hypothesis
is added to create the new goal, namely the negation of (and (< x y)
(integerp a) (equal r s)).  If the negation of this term had been
claimed, then it would be the other way around:  the current goal would
get a single new hypothesis while the new goal would be created by
adding three hypotheses.

*Remark:*  It is allowed to use abbreviations in the hints.

ACL2-PC||CG    (macro)
change to another goal.

     Examples:
     (cg (main . 1)) -- change to the goal (main . 1)
     cg              -- change to the next-to-top goal

     General Form:
     (CG &OPTIONAL goal-name)

Same as (change-goal goal-name t), i.e. change to the indicated and
move the current goal to the end of the goal stack.

ACL2-PC||CHANGE-GOAL    (primitive)
change to another goal.

     Examples:
     (change-goal (main . 1)) -- change to the goal (main . 1)
     change-goal              -- change to the next-to-top goal

     General Form:
     (change-goal &optional goal-name end-flg)

Change to the goal with the name goal-name, i.e. make it the current
goal.  However, if goal-name is nil or is not supplied, then it
defaults to the next-to-top goal, i.e., the second goal in the stack of
goals.  If end-flg is supplied and not nil, then move the current goal
to the end of the goal stack; else merely swap it with the next-to-top
goal.  Also see documentation for cg.

ACL2-PC||CL-PROC    (macro)
same as clause-processor

See the documentation for proof-checker command clause-processor, which
is identical to cl-proc.

ACL2-PC||CLAIM    (atomic macro)
add a new hypothesis

     Examples:
     (claim (< x y))   -- attempt to prove (< x y) from the current
                          top-level hypotheses and if successful, then
                          add (< x y) as a new top-level hypothesis in
                          the current goal
     (claim (< x y)
            :otf-flg t
            :hints (("Goal" :induct t)))
                       -- as above, but call the prover using the
                          indicated values for the otf-flg and hints
     (claim (< x y) 0) -- as above, except instead of attempting to
                          prove (< x y), create a new subgoal with the
                          same top-level hypotheses as the current goal
                          that has (< x y) as its conclusion
     (claim (< x y) :hints :none)
                       -- same as immediately above

     General Form:
     (claim expr &rest rest-args)

This command creates a new subgoal with the same top-level hypotheses
as the current goal but with a conclusion of expr.  If rest-args is a
non-empty list headed by a non-keyword, then there will be no proof
attempted for the new subgoal.  With that possible exception, rest-args
should consist of keyword arguments.  The keyword argument
:do-not-flatten controls the "flattening" of new hypotheses, just as
with the casesplit command (as described in its documentation).  The
remaining rest-args are used with a call the prove command on the new
subgoal, except that if :hints is a non-nil atom, then the prover is
not called -- rather, this is the same as the situation described
above, where rest-args is a non-empty list headed by a non-keyword.

*Remarks:*  (1) Unlike the casesplit command, the claim command is
completely insensitive to governors. (2) It is allowed to use
abbreviations in the hints.  (3) The keyword :none has the special role
as a value of :hints that is shown clearly in an example above.

ACL2-PC||CLAUSE-PROCESSOR    (atomic macro)
use a clause-processor

     Example:
     (cl-proc :function
     	   note-fact-clause-processor
     	  :hint
     	  '(equal a a))
     -- Invoke the indicated clause processor function with the indicated hint
     argument (see the beginning of file
     books/clause-processors/basic-examples.lisp.

     General Form:
     (cl-proc &rest cl-proc-args)

Invoke a clause-processor as indicated by cl-proc-args, which is a list
of arguments that can serve as the value of a :clause-processor hint;
see HINTS.

This command calls the prove command, and hence should only be used at
the top of the conclusion.

ACL2-PC||COMM    (macro)
display instructions from the current interactive session

     Examples:
     comm
     (comm 10)

     General Form:
     (comm &optional n)

Prints out instructions in reverse order.  This is actually the same as
(commands n t) -- or, (commands nil t) if n is not supplied.  As
explained in the documentation for commands, the final argument of t
causes suppression of instructions occurring between so-called
"matching bookends," which we now explain.

A "begin bookend" is an instruction of the form

     (COMMENT :BEGIN x . y).

Similarly, an "end bookend" is an instruction of the form

     (COMMENT :END x' . y').

The "name" of the first bookend is x and the "name" of the second
bookend is x'.  When such a pair of instructions occurs in the current
state-stack, we call them "matching bookends" provided that they have
the same name (i.e. x equals x') and if no other begin or end bookend
with name x occurs between them.  The idea now is that comm hides
matching bookends together with the instructions they enclose.  Here is
a more precise explanation of this "hiding"; probably there is no value
in reading on!

A comm instruction hides bookends in the following manner.  (So does a
comment instruction when its second optional argument is supplied and
non-nil.)  First, if the first argument n is supplied and not nil, then
we consider only the last n instructions from the state-stack;
otherwise, we consider them all.  Now the resulting list of
instructions is replaced by the result of applying the following
process to each pair of matching bookends:  the pair is removed,
together with everything in between the begin and end bookend of the
pair, and all this is replaced by the "instruction"

     ("***HIDING***" :COMMENT :BEGIN name ...)

where (comment begin name ...) is the begin bookend of the pair.
Finally, after applying this process to each pair of matching bookends,
each begin bookend of the form (comment begin name ...)  that remains
is replaced by

     ("***UNFINISHED***" :COMMENT :BEGIN name ...) .

ACL2-PC||COMMANDS    (macro)
display instructions from the current interactive session

     Examples:
     commands
     (commands 10 t)

     General Forms:

     commands or (commands nil)
     Print out all the instructions (in the current state-stack) in
     reverse order, i.e. from the most recent instruction to the starting
     instruction.

     (commands n) [n a positive integer]
     Print out the most recent n instructions (in the current
     state-stack), in reverse order.

     (commands x abbreviate-flag)
     Same as above, but if abbreviate-flag is non-NIL, then do not
     display commands between ``matching bookends''.  See documentation
     for comm for an explanation of matching bookends.

*Remark*:  If there are more than n instructions in the state-stack,
then (commands n) is the same as commands (and also, (commands n abb)
is the same as (commands nil abb)).

ACL2-PC||COMMENT    (primitive)
insert a comment

     Example:
     (comment now begin difficult final goal)

     General Form:
     (comment &rest x)

This instruction makes no change in the state except to insert the
comment instruction.

Some comments can be used to improve the display of commands; see
documentation for comm.

ACL2-PC||CONTRADICT    (macro)
same as contrapose

see documentation for contrapose

ACL2-PC||CONTRAPOSE    (primitive)
switch a hypothesis with the conclusion, negating both

     Example:
     (contrapose 3)

     General Form:
     (contrapose &optional n)

The (optional) argument n should be a positive integer that does not
exceed the number of hypotheses.  Negate the current conclusion and
make it the nth hypothesis, while negating the current nth hypothesis
and making it the current conclusion.  If no argument is supplied then
the effect is the same as for (contrapose 1).

*Remark:* By "negate" we mean an operation that replaces nil by t, x by
nil for any other explicit value x, (not x) by x, and any other x by
(not x).

ACL2-PC||DEMOTE    (primitive)
move top-level hypotheses to the conclusion

     Examples:
     demote        -- demote all top-level hypotheses
     (demote 3 5)  -- demote hypotheses 3 and 5

For example, if the top-level hypotheses are x and y and the conclusion
is z, then after execution of demote, the conclusion will be (implies
(and x y) z) and there will be no (top-level) hypotheses.

     General Form:
     (demote &rest hyps-indices)

Eliminate the indicated (top-level) hypotheses, but replace the
conclusion conc with (implies hyps conc) where hyps is the conjunction
of the hypotheses that were eliminated.  If no arguments are supplied,
then all hypotheses are demoted, i.e. demote is the same as (demote 1 2
... n) where n is the number of top-level hypotheses.

*Remark*:  You must be at the top of the conclusion in order to use
this command.  Otherwise, first invoke top.  Also, demote fails if
there are no top-level hypotheses or if indices are supplied that are
out of range.

ACL2-PC||DIVE    (primitive)
move to the indicated subterm

     Examples:
     (DIVE 1)    -- assign the new current subterm to be the first
                    argument of the existing current subterm
     (DIVE 1 2)  -- assign the new current subterm to be the result of
                    first taking the 1st argument of the existing
                    current subterm, and then the 2nd argument of that

For example, if the current subterm is

     (* (+ a b) c),

then after (dive 1) it is

     (+ a b).

If after that, then (dive 2) is invoked, the new current subterm will be

     b.

Instead of (dive 1) followed by (dive 2), the same current subterm
could be obtained by instead submitting the single instruction (dive 1
2).

     General Form:
     (dive &rest naturals-list)

If naturals-list is a non-empty list (n_1 ... n_k) of natural numbers,
let the new current subterm be the result of selecting the n_1-st
argument of the current subterm, and then the n_2-th subterm of that,
..., finally the n_k-th subterm.

*Remark:*  Dive is related to the command pp, in that the diving is
done according to raw (translated, internal form) syntax.  Use the
command dv if you want to dive according to the syntax displayed by the
command p.  Note that (dv n) can be abbreviated by simply n.

ACL2-PC||DO-ALL    (macro)
run the given instructions

     Example:
     (do-all induct p prove)

     General Form:
     (do-all &rest instruction-list)

Run the indicated instructions until there is a hard "failure".  The
instruction "succeeds" if and only if each instruction in
instruction-list does.  (See the documentation for sequence for an
explanation of "success" and "failure.")  As each instruction is
executed, the system will print the usual prompt followed by that
instruction, unless the global state variable
print-prompt-and-instr-flg is nil.

*Remark:*  If do-all "fails", then the failure is hard if and only if
the last instruction it runs has a hard "failure".

Obscure point:  For the record, (do-all ins_1 ins_2 ... ins_k) is the
same as (sequence (ins_1 ins_2 ... ins_k)).

ACL2-PC||DO-ALL-NO-PROMPT    (macro)
run the given instructions, halting once there is a "failure"

     Example:
     (do-all-no-prompt induct p prove)

     General Form:
     (do-all-no-prompt &rest instruction-list)

Do-all-no-prompt is the same as do-all, except that the prompt and
instruction are not printed each time, regardless of the value of
print-prompt-and-instr-flg.  Also, restoring is disabled.  See the
documentation for do-all.

ACL2-PC||DO-STRICT    (macro)
run the given instructions, halting once there is a "failure"

     Example:
     (do-strict induct p prove)

     General Form:
     (do-strict &rest instruction-list)

Run the indicated instructions until there is a (hard or soft)
"failure".  In fact do-strict is identical in effect to do-all, except
that do-all only halts once there is a hard "failure".  See the
documentation for do-all.

ACL2-PC||DROP    (primitive)
drop top-level hypotheses

     Examples:
     (drop 2 3) -- drop the second and third hypotheses
     drop       -- drop all top-level hypotheses

     General Forms:
     (drop n1 n2 ...) -- Drop the hypotheses with the indicated indices.

     drop             -- Drop all the top-level hypotheses.

*Remark:*  If there are no top-level hypotheses, then the instruction
drop will fail.  If any of the indices is out of range, i.e. is not an
integer between one and the number of top-level hypotheses (inclusive),
then (drop n1 n2 ...) will fail.

ACL2-PC||DV    (atomic macro)
move to the indicated subterm

     Examples:
     (dv 1)    -- assign the new current subterm to be the first argument
                  of the existing current subterm
     (dv 1 2)  -- assign the new current subterm to be the result of
                  first taking the 1st argument of the existing
                  current subterm, and then the 2nd argument of that

For example, if the current subterm is

     (* (+ a b) c),

then after (dv 1) it is

     (+ a b).

If after that, then (dv 2) is invoked, the new current subterm will be

     b.

Instead of (dv 1) followed by (dv 2), the same current subterm could be
obtained by instead submitting the single instruction (dv 1 2).

     General Form:
     (dv &rest naturals-list)

If naturals-list is a non-empty list (n_1 ... n_k) of natural numbers,
let the new current subterm be the result of selecting the n_1-st
argument of the current subterm, and then the n_2-th subterm of that,
..., finally the n_k-th subterm.

*Remark:*  (dv n) may be abbreviated by simply n, so we could have
typed 1 instead of (dv 1) in the first example above.

*Remark:*  See also dive, which is related to the command pp, in that
the diving is done according to raw (translated, internal form) syntax.
Use the command dv if you want to dive according to the syntax
displayed by the command p.  Thus, the command "up" is the inverse of
dive, not of dv.  The following example illustrates this point.

     ACL2 !>(verify (equal (* a b c) x))
     ->: p ; print user-level term
     (EQUAL (* A B C) X)
     ->: pp ; print internal-form (translated) term
     (EQUAL (BINARY-* A (BINARY-* B C)) X)
     ->: exit
     Exiting....
      NIL
     ACL2 !>(verify (equal (* a b c) x))
     ->: p
     (EQUAL (* A B C) X)
     ->: 1 ; same as (dv 1)
     ->: p ; print user-level term
     (* A B C)
     ->: pp ; print internal-form (translated) term
     (BINARY-* A (BINARY-* B C))
     ->: 3 ; dive to third argument of (* A B C)
     ->: p
     C
     ->: up ; go up one level in (BINARY-* A (BINARY-* B C))
     ->: p
     (* B C)
     ->: pp
     (BINARY-* B C)
     ->:

ACL2-PC||ELIM    (atomic macro)
call the ACL2 theorem prover's elimination process

     Example and General Form:
     elim

Upon running the elim command, the system will create a subgoal will be
created for each goal that would have been pushed for proof by
induction in an ordinary proof, where *only* elimination is used; not
even simplification is used!

ACL2-PC||EQUIV    (primitive)
attempt an equality (or congruence-based) substitution

     Examples:
     (equiv (* x y) 3) -- replace (* x y) by 3 everywhere inside the
                          current subterm, if their equality is among the
                          top-level hypotheses or the governors
     (equiv x t iff)   -- replace x by t everywhere inside the current
                          subterm, where only propositional equivalence
                          needs to be maintained at each occurrence of x

     General form:
     (equiv old new &optional relation)

Substitute new for old everywhere inside the current subterm, provided
that either (relation old new) or (relation new old) is among the
top-level hypotheses or the governors (possibly by way of backchaining
and/or refinement; see below).  If relation is nil or is not supplied,
then it defaults to equal.  See also the command =, which is much more
flexible.  Note that this command fails if no substitution is actually
made.

*Remark:*  No substitution takes place inside explicit values.  So for
example, the instruction (equiv 3 x) will cause 3 to be replaced by x
if the current subterm is, say, (* 3 y), but not if the current subterm
is (* 4 y) even though 4 = (1+ 3).

The following remarks are quite technical and mostly describe a certain
weak form of "backchaining" that has been implemented for equiv in
order to support the = command.  In fact neither the term (relation old
new) nor the term (relation new old) needs to be *explicitly* among the
current "assumptions", i.e., the top-level hypothesis or the governors.
Rather, there need only be such an assumption that "tells us" (r old
new) or (r new old), for *some* equivalence relation r that *refines*
relation.  Here, "tells us" means that either one of the indicated
terms is among those assumptions, or else there is an assumption that
is an implication whose conclusion is one of the indicated terms and
whose hypotheses (gathered up by appropriately flattening the first
argument of the implies term) are all among the current assumptions.

ACL2-PC||EX    (macro)
exit after possibly saving the state

     Example and General Form:
     ex

Same as exit, except that first the instruction save is executed.

If save queries the user and is answered negatively, then the exit is
aborted.

ACL2-PC||EXIT    (meta)
exit the interactive proof-checker

     Examples:
     exit                        -- exit the interactive proof-checker
     (exit append-associativity) -- exit and create a defthm
                                    event named append-associativity

     General Forms:

     exit --  Exit without storing an event.

     (exit event-name &optional rule-classes do-it-flg)
     Exit, and store an event.

The command exit returns you to the ACL2 loop.  At a later time,
(verify) may be executed to get back into the same proof-checker state,
as long as there hasn't been an intervening use of the proof-checker
(otherwise see save).

When given one or more arguments as shown above, exit still returns you
to the ACL2 loop, but first, if the interactive proof is complete, then
it attempts create a defthm event with the specified event-name and
rule-classes (which defaults to (:rewrite) if not supplied).  The event
will be printed to the terminal, and then normally the user will be
queried whether an event should really be created.  However, if the
final optional argument do-it-flg is supplied and not nil, then an
event will be made without a query.

For example, the form

     (exit top-pop-elim (:elim :rewrite) t)

causes a defthm event named top-pop-elim to be created with
rule-classes (:elim :rewrite), without a query to the user (because of
the argument t).

*Remark:* it is permitted for event-name to be nil.  In that case, the
name of the event will be the name supplied during the original call of
verify.  (See the documentation for verify and commands.)  Also in that
case, if rule-classes is not supplied then it defaults to the
rule-classes supplied in the original call of verify.

Comments on "success" and "failure".  An exit instruction will always
"fail", so for example, if it appears as an argument of a do-strict
instruction then none of the later (instruction) arguments will be
executed.  Moreover, the "failure" will be "hard" if an event is
successfully created or if the instruction is simply exit; otherwise it
will be "soft".  See the documentation for sequence for an explanation
of hard and soft "failures".  An obscure but potentially important fact
is that if the "failure" is hard, then the error signal is a special
signal that the top-level interactive loop can interpret as a request
to exit.  Thus for example, a sequencing command that turns an error
triple (mv erp val state) into (mv t val state) would never cause an
exit from the interactive loop.

If the proof is not complete, then (exit event-name ...) will not cause
an exit from the interactive loop.  However, in that case it will print
out the original user-supplied goal (the one that was supplied with the
call to verify) and the current list of instructions.

ACL2-PC||EXPAND    (primitive)
expand the current function call without simplification

     Examples:
     expand -- expand and do not simplify.

For example, if the current subterm is (append a b), then after (expand
t) the current subterm will be the term:

     (if (true-listp x)
         (if x
             (cons (car x) (append (cdr x) y))
           y)
       (apply 'binary-append (list x y)))

regardless of the top-level hypotheses and the governors.

     General Form:
     (expand &optional do-not-expand-lambda-flg)

Expand the function call at the current subterm, and do not simplify.
The options have the following meanings:

     do-not-expand-lambda-flg:   default is nil; otherwise, the result
                                 should be a lambda expression

See also x, which allows simplification.

ACL2-PC||FAIL    (macro)
cause a failure

     Examples:
     fail
     (fail t)

     General Form:
     (fail &optional hard)

This is probably only of interest to writers of macro commands.  The
only function of fail is to fail to "succeed".

The full story is that fail and (fail nil) simply return (mv nil nil
state), while (fail hard) returns (mv hard nil state) if hard is not
nil.  See also do-strict, do-all, and sequence.

ACL2-PC||FORWARDCHAIN    (atomic macro)
forward chain from an implication in the hyps

     Example:
     (forwardchain 2) ; Second hypothesis should be of the form
                      ; (IMPLIES hyp concl), and the result is to replace
                      ; that hypothesis with concl.

     General Forms:
     (forwardchain hypothesis-number)
     (forwardchain hypothesis-number hints)
     (forwardchain hypothesis-number hints quiet-flg)

This command replaces the hypothesis corresponding to given index,
which should be of the form (IMPLIES hyp concl), with its consequent
concl.  In fact, the given hypothesis is dropped, and the replacement
hypothesis will appear as the final hypothesis after this command is
executed.

The prover must be able to prove the indicated hypothesis from the
other hypotheses, or else the command will fail.  The :hints argument
is used in this prover call, and should have the usual syntax of hints
to the prover.

Output is suppressed if quiet-flg is supplied and not nil.

ACL2-PC||FREE    (atomic macro)
create a "free variable"

     Example:
     (free x)

     General Form:
     (free var)

Mark var as a "free variable".  Free variables are only of interest for
the put command; see its documentation for an explanation.

ACL2-PC||GENERALIZE    (primitive)
perform a generalization

     Example:
     (generalize
      ((and (true-listp x) (true-listp y)) 0)
      ((append x y) w))

     General Form:
     (generalize &rest substitution)

Generalize using the indicated substitution, which should be a
non-empty list.  Each element of that list should be a two-element list
of the form (term variable), where term may use abbreviations.  The
effect of the instruction is to replace each such term in the current
goal by the corresponding variable.  This replacement is carried out by
a parallel substitution, outside-in in each hypothesis and in the
conclusion.  More generally, actually, the "variable" (second)
component of each pair may be nil or a number, which causes the system
to generate a new name of the form _ or _n, with n a natural number;
more on this below.  However, when a variable is supplied, it must not
occur in any goal of the current proof-checker state.

When the "variable" above is nil, the system will treat it as the
variable |_| if that variable does not occur in any goal of the current
proof-checker state.  Otherwise it treats it as |_0|, or |_1|, or |_2|,
and so on, until one of these is not among the variables of the current
proof-checker state.  If the "variable" is a non-negative integer n,
then the system treats it as |_n| unless that variable already occurs
among the current goals, in which case it increments n just as above
until it obtains a new variable.

*Remark:*  The same variable may not occur as the variable component of
two different arguments (though nil may occur arbitrarily many times,
as may a positive integer).

ACL2-PC||GOALS    (macro)
list the names of goals on the stack

     Example and General Form:
     goals

Goals lists the names of all goals that remain to be proved.  They are
listed in the order in which they appear on the stack of remaining
goals, which is relevant for example to the effect of a change-goal
instruction.

ACL2-PC||HELP    (macro)
proof-checker help facility

     Examples:

     (help rewrite) -- partial documentation on the rewrite command; the
                       rest is available using more or more!

     (help! rewrite) -- full documentation on the rewrite command

     help, help!     -- this documentation (in part, or in totality,
                        respectively)

     General Forms:
     (help &optional command)
     (help! &optional command)
     more
     more!

The proof checker supports the same kind of documentation as does ACL2
proper.  The main difference is that you need to type

     (help command)

in a list rather than :doc command.  So, to get all the documentation
on command, type (help! command) inside the interactive loop, but to
get only a one-line description of the command together with some
examples, type (help command).  In the latter case, you can get the
rest of the help by typing more!; or type more if you don't necessarily
want all the rest of the help at once.  (Then keep typing more if you
want to keep getting more of the help for that command.)

To summarize:  as with ACL2, you can type either of the following:

     more, more!
     -- to obtain more (or, all the rest of) the documentation last
        requested by help (or, outside the proof-checker's loop, :doc)

It has been arranged that the use of (help command) will tell you just
about everything you could want to know about command, almost always by
way of examples.  For more details about a command, use help!, more, or
more!.

We use the word "command" to refer to the name itself, e.g.  rewrite.
We use the word "instruction" to refer to an input to the interactive
system, e.g. (rewrite foo) or (help split).  Of course, we allow
commands with no arguments as instructions in many cases, e.g. rewrite.
In such cases, command is treated identically to (command).

ACL2-PC||HELP!    (macro)
proof-checker help facility

Same as help, except that the entire help message is printed without
any need to invoke more! or more.

Invoke help for documentation about the proof-checker help facility.

ACL2-PC||HELP-LONG    (macro)
same as help!

See the documentation for help!.

Help-long has been included in addition to help! for historical
reasons.  (Such a command is included in Pc-Nqthm).

ACL2-PC||HYPS    (macro)
print the hypotheses

     Examples:
     hyps               -- print all (top-level) hypotheses
     (hyps (1 3) (2 4)) -- print hypotheses 1 and 3 and governors 2 and 4
     (hyps (1 3) t)     -- print hypotheses 1 and 3 and all governors

     General Form:
     (hyps &optional hyps-indices govs-indices)

Print the indicated top-level hypotheses and governors.  (The notion of
"governors" is defined below.)  Here, hyps-indices and govs-indices
should be lists of indices of hypotheses and governors (respectively),
except that the atom t may be used to indicate that one wants all
hypotheses or governors (respectively).

The list of "governors" is defined as follows.  Actually, we define
here the notion of the governors for a pair of the form <term,
address>]; we're interested in the special case where the term is the
conclusion and the address is the current address.  If the address is
nil, then there are no governors, i.e., the list of governors is nil.
If the term is of the form (if x y z) and the address is of the form (2
. rest) or (3 . rest), then the list of governors is the result of
consing x or its negation (respectively) onto the list of governors for
the pair <y, rest> or the pair <z, rest> (respectively).  If the term
is of the form (implies x y) and the address is of the form (2 . rest),
then the list of governors is the result of consing x onto the list of
governors for the pair <y, rest>.  Otherwise, the list of governors for
the pair <term, (n .  rest)> is exactly the list of governors for the
pair <argn, rest> where argn is the nth argument of term.

If all goals have been proved, a message saying so will be printed.
(as there will be no current hypotheses or governors!).

The hyps command never causes an error.  It "succeeds" (in fact its
value is t) if the arguments (when supplied) are appropriate, i.e.
either t or lists of indices of hypotheses or governors, respectively.
Otherwise it "fails" (its value is nil).

ACL2-PC||ILLEGAL    (macro)
illegal instruction

     Example:
     (illegal -3)

     General Form:
     (illegal instruction)

Probably not of interest to most users; always "fails" since it expands
to the fail command.

The illegal command is used mainly in the implementation.  For example,
the instruction 0 is "read" as (illegal 0), since dive expects positive
integers.

ACL2-PC||IN-THEORY    (primitive)
set the current proof-checker theory

     Example:
     (in-theory
        (union-theories (theory 'minimal-theory) '(true-listp binary-append)))

     General Form:
     (in-theory &optional atom-or-theory-expression)

If the argument is not supplied, then this command sets the current
proof-checker theory (see below for explanation) to agree with the
current ACL2 theory.  Otherwise, the argument should be a theory
expression, and in that case the proof-checker theory is set to the
value of that theory expression.

The current proof-checker theory is used in all calls to the ACL2
theorem prover and rewriter from inside the proof-checker.  Thus, the
most recent in-theory instruction in the current state-stack has an
effect in the proof-checker totally analogous to the effect caused by
an in-theory hint or event in ACL2.  All in-theory instructions before
the last are ignored, because they refer to the current theory in the
ACL2 state, not to the existing proof-checker theory.  For example:

        ACL2 !>:trans1 (enable bar)
         (UNION-THEORIES (CURRENT-THEORY :HERE)
                         '(BAR))
        ACL2 !>:trans1 (CURRENT-THEORY :HERE)
         (CURRENT-THEORY-FN :HERE WORLD)
        ACL2 !>

Thus (in-theory (enable bar)) modifies the current theory of the current
ACL2 world.  So for example, suppose that foo is disabled outside the
proof checker and you execute the following instructions, in this order.

        (in-theory (enable foo))
        (in-theory (enable bar))

Then after the second of these, bar will be enabled in the
proof-checker, but foo will be disabled.  The reason is that (in-theory
(enable bar)) instructs the proof-checker to modify the current theory
(from outside the proof-checker, not from inside the proof-checker) by
enabling bar.

Note that in-theory instructions in the proof-checker have no effect
outside the proof-checker's interactive loop.

If the most recent in-theory instruction in the current state of the
proof-checker has no arguments, or if there is no in-theory instruction
in the current state of the proof-checker, then the proof-checker will
use the current ACL2 theory.  This is true even if the user has
interrupted the interactive loop by exiting and changing the global
ACL2 theory.  However, if the most recent in-theory instruction in the
current state of the proof-checker had an argument, then global changes
to the current theory will have no effect on the proof-checker state.