This is documentation for ACL2 Version 5.0
Copyright (C) 2012  University of Texas at Austin

This program is free software; you can redistribute it and/or modify
it under the terms of Version 2 of the GNU General Public License as
published by the Free Software Foundation.

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.

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.

CHECK-SUM    assigning "often unique" integers to files and objects

A "check sum" is an integer in some fixed range computed from the
printed representation of an object, e.g., the sum, modulo 2**32, of
the ascii codes of all the characters in the printed representation.

Ideally, you would like the check sum of an object to be uniquely
associated with that object, like a fingerprint.  It could then be used
as a convenient way to recognize the object in the future: you could
remember the check sum (which is relatively small) and when an object
is presented to you and alleged to be the special one you could compute
its check sum and see if indeed it was.  Alas, there are many more
objects than check sums (after all, each check sum is an object, and
then there's t).  So you try to design a check sum algorithm that maps
similar looking objects far apart, in the hopes that corruptions and
counterfeits -- which appear to be similar to the object -- have
different check sums.  Nevertheless, the best you can do is a
many-to-one map.  If an object with a different check sum is presented,
you can be positive it is not the special object.  But if an object
with the same check sum is presented, you have no grounds for positive
identification.

The basic check sum algorithm in ACL2 is called check-sum-obj, which
computes the check sum of an ACL2 object.  Roughly speaking, we scan
the print representation of the object and, for each character
encountered, we multiply the ascii code of the character times its
position in the stream (modulo a certain prime) and then add (modulo a
certain prime) that into the running sum.  This is inaccurate in many
senses (for example, we don't always use the ascii code and we see
numbers as though they were printed in base 127) but indicates the
basic idea.

ACL2 uses check sums to increase security in the books mechanism; see
CERTIFICATE.

CLOSE-INPUT-CHANNEL    See IO.

CLOSE-OUTPUT-CHANNEL    See IO.

CODE-CHAR    the character corresponding to a given numeric code

Completion Axiom (completion-of-code-char):

     (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 (completion-of-coerce):

     (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).

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, named completion-of-complex.

     (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.  (The
latter immediately generates a call to concatenate when applied to
strings.)

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.

To see the ACL2 definition of this function, see PF.

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.

COUNT    count the number of occurrences of an item in a string or true-list

     Example Forms:
     (count #\D "DabcDefcDe")                 ; = 3
     (count #\D "DabcDefcDe" :start 1)        ; = 2
     (count #\D "DabcDefcDe" :start 1 :end 5) ; = 1
     (count #\D "DabcDefcDe" :start 1 :end 4) ; = 0
     (count #\z "DabcDefcDe")                 ; = 0
     (count '(a b) '(17 (a b) 23 (a b) (c d)))   ; = 2

     General Form:
     (count item sequence &key start end)

(Count item sequence) returns the number of times item occurs in
sequence.  The guard for calls of count (which is actually a macro in
ACL2) specifies that sequence is a string or a true-list, and that
start, which defaults to 0, and end, which defaults to the length of
sequence, are valid indices into sequence.

See any Common Lisp documentation for more information about count,
which is a Common Lisp utility.  At this time ACL2 does not support
keyword arguments for count other than :start and :end; we may add
support for the :from-end keyword upon request.

CPU-CORE-COUNT    the number of cpu cores

This documentation topic relates to the experimental extension of ACL2
supporting parallel execution and proof; see PARALLELISM.

Unless the ACL2 executable supports parallel execution (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 macro whose calls expand to calls
of 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.

Finally, we discuss another way to create formatted output that also
avoids the need to pass in the ACL2 state.  The idea is to use
wormholes; see WORMHOLE.  Below is a function you can write,
along with some calls, providing an illustration of this approach.

     (defun my-fmt-to-comment-window (str alist)
       (wormhole 'my-fmt-to-comment-window
                 '(lambda (whs) whs)
                 (list str alist)
                 '(pprogn
                   (fms (car (@ wormhole-input))
                        (cadr (@ wormhole-input))
                        *standard-co*
                        state
                        nil)
                   (value :q))
                 :ld-verbose nil
                 :ld-error-action :return ; harmless return on error
                 :ld-prompt nil))

     ; A non-erroneous call:
     (my-fmt-to-comment-window "Here is ~x0 for your inspection~%"
                               (list (cons #\0 'foo)))

     ; An error inside the fmt string (unbound fmt var); note that even
     ; with the error, the wormhole is exited.
     (my-fmt-to-comment-window "Here is ~x1 for your inspection~%"
                               (list (cons #\0 'foo)))

     ; A guard violation in the binding; note that even with the error,
     ; the wormhole is exited.
     (my-fmt-to-comment-window "Here is ~x0 for your inspection~%"
                               (list (cons #\0 (car 'foo))))

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.

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

     General Forms:
     (delete-assoc key alist)
     (delete-assoc key alist :test 'eql)   ; same as above (eql as equality test)
     (delete-assoc key alist :test 'eq)    ; same, but eq is equality test
     (delete-assoc key alist :test 'equal) ; same, but equal is equality test

(Delete-assoc key alist) returns an alist that is the same as the list
alist, except that the first pair in alist with a car of key is
deleted, if there is one; otherwise alist is returned.  Note that the
order of the elements of alist is unchanged (though one may be deleted).

The guard for a call of delete-assoc depends on the test.  In all
cases, the second argument must satisfy alistp.  If the test is eql,
then either the first argument must be suitable for eql (see
EQLABLEP) or the second argument must satisfy eqlable-alistp.  If the
test is eq, then either the first argument must be a symbol or the
second argument must satisfy symbol-alistp.

See EQUALITY-VARIANTS for a discussion of the relation between
delete-assoc and its variants:

     (delete-assoc-eq key alist) is equivalent to (delete-assoc key
     alist :test 'eq);

     (delete-assoc-equal key alist) is equivalent to (delete-assoc key
     alist :test 'equal).

In particular, reasoning about any of these primitives reduces to
reasoning about the function delete-assoc-equal.

DELETE-ASSOC-EQ    See DELETE-ASSOC.

DELETE-ASSOC-EQUAL    See DELETE-ASSOC.

DENOMINATOR    divisor of a ratio in lowest terms

Completion Axiom (completion-of-denominator):

     (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.

To see the ACL2 definition of this function, see PF.

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 behaves like the identity macro; during proofs,
(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*.  In particular, fn is not
a macro.  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).

*Technical Remark* (probably best ignored).  During evaluation of a call
of defconst or defpkg in raw Lisp, a form (ec-call (fn term1 ...
termk)) is treated as (fn term1 ... termk), that is, without calling
the executable counterpart of fn.  This situation occurs when loading a
compiled file (or expansion file) on behalf of an include-book event.
The reason is technical: executable counterparts are defined below a
book's events in the book's compiled file.  End of Technical Remark.

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 call (FOO X Y),
     which is (CONSP Y), is violated by the arguments in the call
     (FOO '(4 5) NIL).  To debug see :DOC print-gv, see :DOC trace, and
     see :DOC wet.  See :DOC set-guard-checking for information about suppressing
     this check with (set-guard-checking :none), as recommended for new
     users.

     ACL2 !>

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 call (FOO X Y),
     which is (CONSP Y), is violated by the arguments in the call
     (FOO '(4 5) NIL).  To debug see :DOC print-gv, see :DOC trace, and
     see :DOC wet.  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.

To see the ACL2 definition of this function, see PF.

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.

To see the ACL2 definition of this function, see PF.

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.

To see the ACL2 definition of this function, see PF.

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.

To see the ACL2 definition of this function, see PF.

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 logically returning
nil, though in ordinary evaluation the return value is never seen);
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 unless they are building systems of some sort;
see PROGRAMMING-WITH-STATE.  If state is not available in the
current context then you will probably want to use (er hard ...) or (er
hard? ...) to cause an error; for example, if you are returning two
values, you may write (mv (er hard ...) nil).

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.

     General Form:
     (er-progn <expr1> ... <exprk>)

where each <expri> is an expression that evaluates to an error triple
(see PROGRAMMING-WITH-STATE).  The above form is essentially
equivalent to the following ("essentially" because in fact, care is
taken to avoid variable capture).

     (mv-let (erp val state)
             <expr1>
             (cond (erp (mv erp val state))
                   (t (mv-let (erp val state)
                              <expr2>
                              (cond (erp (mv erp val state))
                                    (t ...
                                           (mv-let (erp val state)
                                                   <expr{k-1}>
                                                   (cond (erp (mv erp val state))
                                                         (t <exprk>)))))))))

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.

To see the ACL2 definition of this function, see PF.

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).

To see the ACL2 definition of this function, see PF.

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.

To see the ACL2 definition of this function, see PF.

F-GET-GLOBAL    get the value of a global variable in state

     Examples:
     (+ (f-get-global 'y state) 1)
     (f-put-global 'a
                   (aset1 'ascii-map-array
                          (f-get-global 'a state)
                          66
                          'Upper-case-B)
                   state)

     General Form:
     (f-get-global 'symbol state)

where symbol is any symbol to which you have assigned a global value.

The macro @ is closely related to f-get-global: (@ var) macroexpands to
(f-get-global 'var state).

The macro f-get-global makes it convenient to set the value of a
symbol.  The :ubt operation has no effect on the global-table of state.
Thus, you may use these globals to hang onto useful data structures
even though you may undo back past where you computed and saved them.

F-PUT-GLOBAL    assign to a global variable in state

     Examples:
     (f-put-global 'x (expt 2 10) state)
     (f-put-global 'a (aset1 'ascii-map-array (@ a) 66 'Upper-case-B) state)

     General Form:
     (f-put-global (quote symbol) term state)

where symbol is any symbol (with certain enforced exclusions to avoid
overwriting ACL2 system "globals") and term is any ACL2 term that could
be evaluated at the top-level.  F-put-global evaluates the term, stores
the result as the value of the given symbol in the global-table of
state, and returns the new state.  (Note:  the actual implementation of
the storage of this value is much more efficient than this discussion
of the logic might suggest.)

The macro assign is closely related to f-put-global: (assign var val)
macroexpands to (f-put-global 'var val state).

The macros @ and f-get-global give convenient access to the value of
such globals.  The :ubt operation has no effect on the global-table of
state.  Thus, you may use these globals to hang onto useful data
structures even though you may undo back past where you computed and
saved them.

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.

To see the ACL2 definition of this function, see PF.

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.

To see the ACL2 definition of this function, see PF.

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,

To see the ACL2 definition of this function, see PF.

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.

FMS!-TO-STRING    See PRINTING-TO-STRINGS.

FMS-TO-STRING    See PRINTING-TO-STRINGS.

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.  There are also
analogues of these functions that return a string without taking state
as an argument; see PRINTING-TO-STRINGS.

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 (unless the
          symbol would normally be printed with surrounding vertical bar
          characters (|), in which case print as with ~fx); 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 that, by default, an attempt
is made to avoid printing past column 77.  See
SET-FMT-HARD-RIGHT-MARGIN for a discussion of how linebreaks are
inserted and how to change the relevant default settings.

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-STRING    See PRINTING-TO-STRINGS.

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.

FMT-TO-STRING    See PRINTING-TO-STRINGS.

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.

FMT1!-TO-STRING    See PRINTING-TO-STRINGS.

FMT1-TO-STRING    See PRINTING-TO-STRINGS.

FOURTH    fourth member of the list

See any Common Lisp documentation for details.

GET-OUTPUT-STREAM-STRING$    See IO.

GETENV$    read an environment variable

(Getenv$ str state), where str is a string, reads the value of
environment variable str, returning a value of nil if none is found or
if the read fails.  The logical 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, and logically, val is the top of the acl2-oracle field of the
state and the returned state has the updated (popped) acl2-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.

To see the ACL2 definition of this function, see PF.

GOOD-ATOM-LISTP    recognizer for a true list of "good" atoms

The predicate good-atom-listp tests whether its argument is a
true-listp of "good" atoms, i.e., where each element is a number, a
symbol, a character, or a string.

Also see ATOM-LISTP.

To see the ACL2 definition of this function, see PF.

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).

To see the ACL2 definition of this function, see PF.

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.

To see the ACL2 definition of this function, see PF.

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 (completion-of-imagpart):

     (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).

To see the ACL2 definition of this function, see PF.

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.

To see the ACL2 definition of this function, see PF.

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.

To see the ACL2 definition of this function, see PF.

INTEGER-LISTP    recognizer for a true list of integers

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

To see the ACL2 definition of this function, see PF.

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 (completion-of-intern-in-package-of-symbol):

     (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|

INTERSECTION$    elements of one list that are not elements of another

     General Forms:
     (intersection$ l1 l2 ... lk)
     (intersection$ l1 l2 ... lk :test 'eql) ; same as above
     (intersection$ l1 l2 ... lk :test 'eq)    ; same, but eq is equality test
     (intersection$ l1 l2 ... lk :test 'equal) ; same, but equal is equality test

(Intersection$ x y) equals a list that contains the members of x that
are also members of y.  More precisely, the resulting list is the
result of deleting from x those members that that are not members of y.
The optional keyword, :TEST, has no effect logically, but provides the
test (default eql) used for comparing members of the two lists.

Intersection$ need not take exactly two arguments, though it must take
at least one argument: (intersection$ x) is x,  (intersection$ x y z
... :test test) is (intersection$ x (intersection$ y z ... :test test)
:test test), and if :TEST is not supplied, then (intersection$ x y z
...)  is (intersection$ x (intersection$ y z ...)).  For the discussion
below we restrict ourselves, then, to the cases (intersection$ x y) and
(intersection$ x y :test test).

The guard for a call of intersection$ (in the two cases just above)
depends on the test.  In all cases, both arguments must satisfy
true-listp.  If the test is eql, then one of the arguments must satisfy
eqlable-listp.  If the test is eq, then one of the arguments must
satisfy symbol-listp.

See EQUALITY-VARIANTS for a discussion of the relation between
intersection$ and its variants:

     (intersection-eq x lst) is equivalent to (intersection$ x lst
     :test 'eq);

     (intersection-equal x lst) is equivalent to (intersection$ x lst
     :test 'equal).

In particular, reasoning about any of these primitives reduces to
reasoning about the function intersection-equal.

Note that intersection-eq can take any positive number of arguments, in
analogy to intersection$; indeed, (intersection-eq ...) expands to
(intersection$ ... :test 'eq).  However, intersection-equal is a
function, not a macro, and takes exactly two arguments.

Intersection$ is similar to the Common Lisp primitive intersection.
However, Common Lisp does not specify the order of elements in the
result of a call of intersection.

INTERSECTION-EQ    See INTERSECTION$.

INTERSECTION-EQUAL    See INTERSECTION$.

INTERSECTP    test whether two lists intersect

     General Forms:
     (set-difference$ l1 l2)
     (set-difference$ l1 l2 :test 'eql)   ; same as above (eql as equality test)
     (set-difference$ l1 l2 :test 'eq)    ; same, but eq is equality test
     (set-difference$ l1 l2 :test 'equal) ; same, but equal is equality test

(Intersectp l1 l2) returns t if l1 and l2 have a member in common, else
it returns nil.  The optional keyword, :TEST, has no effect logically,
but provides the test (default eql) used for comparing members of the
two lists.

The guard for a call of intersectp depends on the test.  In all cases,
both arguments must satisfy true-listp.  If the test is eql, then one
of the arguments must satisfy eqlable-listp.  If the test is eq, then
one of the arguments must satisfy symbol-listp.

See EQUALITY-VARIANTS for a discussion of the relation between
intersectp and its variants:

     (intersectp-eq x lst) is equivalent to (intersectp x lst :test
     'eq);

     (intersectp-equal x lst) is equivalent to (intersectp x lst :test
     'equal).

In particular, reasoning about any of these primitives reduces to
reasoning about the function intersectp-equal.

INTERSECTP-EQ    See INTERSECTP.

INTERSECTP-EQUAL    See INTERSECTP.

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.

To see the ACL2 definition of this function, see PF.

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 !>

To see the ACL2 definition of this function, see PF.

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.

To see the ACL2 definition of this function, see PF.

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).

To see the ACL2 definition of this function, see PF.

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.

To see the ACL2 definition of this function, see PF.

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.)

To see the ACL2 definition of this function, see PF.

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.

To see the ACL2 definition of this function, see PF.

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.

To see the ACL2 definition of this function, see PF.

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.

To see the ACL2 definition of this function, see PF.

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.

To see the ACL2 definition of this function, see PF.

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.

To see the ACL2 definition of this function, see PF.

LOGBITP    the ith bit of an integer

For a nonnegative integer i and an integer j, (logbitp i j) is a
Boolean, which is t if and only if the value of the ith bit is 1 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.

To see the ACL2 definition of this function, see PF.

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.

To see the ACL2 definition of this function, see PF.

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.

To see the ACL2 definition of this function, see PF.

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.

To see the ACL2 definition of this function, see PF.

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.

To see the ACL2 definition of this function, see PF.

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.

To see the ACL2 definition of this function, see PF.

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.

To see the ACL2 definition of this function, see PF.

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.

To see the ACL2 definition of this function, see PF.

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.

To see the ACL2 definition of this function, see PF.

MAKE-CHARACTER-LIST    coerce to a list of characters

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

To see the ACL2 definition of this function, see PF.

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.

To see the ACL2 definition of this function, see PF.

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.

To see the ACL2 definition of this function, see PF.

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 include not only the guard proof
obligations from exec-code, but also, under suitable contextual
assumptions, the term (equal exec-code logic-code).  See
VERIFY-GUARDS (in particular, for discussion of the contextual
assumptions from the :guard and IF-tests) 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) macroexpands in ACL2 to
a form that generates the guard proof obligation (equal logic-code
exec-code).  The c[: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.

MBE1    attach code for execution

The form (mbe1 exec logic) is equivalent to the forms (mbe :logic logic
:exec exec) and (must-be-equal logic exec).  See MBE.

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

     General Forms:
     (member x lst)
     (member x lst :test 'eql)   ; same as above (eql as equality test)
     (member x lst :test 'eq)    ; same, but eq is equality test
     (member x lst :test 'equal) ; same, but equal is equality test

(Member x lst) equals the longest tail of the list lst that begins with
x, or else nil if no such tail exists.  The optional keyword, :TEST,
has no effect logically, but provides the test (default eql) used for
comparing x with successive elements of lst.

The guard for a call of member depends on the test.  In all cases, the
second argument must satisfy true-listp.  If the test is eql, then
either the first argument must be suitable for eql (see
EQLABLEP) or the second argument must satisfy eqlable-listp.  If the
test is eq, then either the first argument must be a symbol or the
second argument must satisfy symbol-listp.

See EQUALITY-VARIANTS for a discussion of the relation between
member and its variants:

     (member-eq x lst) is equivalent to (member x lst :test 'eq);

     (member-equal x lst) is equivalent to (member x lst :test 'equal).

In particular, reasoning about any of these primitives reduces to
reasoning about the function member-equal.

Member is defined by Common Lisp.  See any Common Lisp documentation for
more information.

MEMBER-EQ    See MEMBER.

MEMBER-EQUAL    See MEMBER.

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.

To see the ACL2 definition of this function, see PF.

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.

To see the ACL2 definition of this function, see PF.

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.

To see the ACL2 definition of this function, see PF.

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.

To see the ACL2 definition of this function, see PF.

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.

In essence, the guard for (must-be-equal x y) is (equal x y).  However,
note that must-be-equal is a macro: (must-be-equal logic exec) expands
to (mbe1 exec logic), which expands to a call of return-last.

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.  Also see MV-LIST for a way to convert a multiple
value into an ordinary list.

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.  Also see MV and see
MV-LIST.

MV-LIST    converting multiple-valued result to a single-valued list

     Example Forms:
     ; Returns the list (3 4):
     (mv-list 2 (mv 3 4))

     ; Returns a list containing the three values returned by var-fn-count:
     (mv-list 3 (var-fn-count '(cons (binary-+ x y) z) nil))

     General form:
     (mv-list n term)

Logically, (mv-list n term) is just term; that is, in the logic mv-list
simply returns its second argument.  However, the evaluation of a call
of mv-list on explicit values always results in a single value, which
is a (null-terminated) list.  For evaluation, the term n above (the
first argument to an mv-list call) must "essentially" (see below) be an
integer not less than 2, where that integer is the number of values
returned by the evaluation of term (the second argument to that mv-list
call).

We say "essentially" above because it suffices that the translation of
n to a term (see TRANS) be of the form (quote k), where k is an
integer greater than 1.  So for example, if term above returns three
values, then n can be the expression 3, or (quote 3), or even (mac 3)
if mac is a macro defined by (defmacro mac (x) x).  But n cannot be (+
1 2), because even though that expression evaluates to 3, nevertheless
it translates to (binary-+ '1 '2), not to (quote 3).

Mv-list is the ACL2 analogue of the Common Lisp construct
multiple-value-list.

To see the ACL2 definition of this function, see PF.

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.

Mv-nth is equivalent to the Common Lisp function nth (although without
the guard condition that the list is a true-listp), but is used by ACL2
to access the nth value returned by a multiply valued expression.  For
example, the following are logically equivalent:

     (mv-let (erp val state)
             (read-object ch state)
             (value (list erp val)))

and

     (let ((erp (mv-nth 0 (read-object ch state)))
           (val (mv-nth 1 (read-object ch state)))
           (state (mv-nth 2 (read-object ch state))))
       (value (list erp val)))

To see the ACL2 definition of mv-nth, see PF.

If EXPR is an expression that is multiply valued, then the form (mv-nth
n EXPR) is illegal both in definitions and in forms submitted directly
to the ACL2 loop.  Indeed, EXPR cannot be passed as an argument to any
function (mv-nth or otherwise) in such an evaluation context.  The
reason is that ACL2 code compiled for execution does not actually
create a list for multiple value return; for example, the read-object
call above logically returns a list of length 3, but when evaluated, it
instead stores its three returned values without constructing a list.
In such cases you can use mv-nth to access the corresponding list by
using mv-list, writing (mv-nth n (mv-list k EXPR)) for suitable k,
where mv-list converts a multiple value result into the corresponding
list; see MV-LIST.

MV?    return one or more values

Mv? is designed to work with mv?-let, generalizing how mv works with
mv-let by allowing the binding of a single variable.  For example, the
following form is legal.

     (mv?-let (y)
              (mv? (f x))
              (declare (type integer y))
              (g x y z))

The expression above is equivalent to the following expression, because
(mv? form) expands to form for any expression, form.

     (let ((y (f x)))
       (declare (type integer y))
       (g x y z))

Logically, (mv? x) is the same as x, while (mv? v1 v2 ...) is the same
as (list v1 v2 ...).  Also see MV and see MV?-LET.

MV?-LET    calling possibly multi-valued ACL2 functions

Mv?-let is a macro that extends the macro mv-let by allowing a single
variable to be bound.  Thus, the syntax is the same as that of mv-let
except that mv?-let is permitted to bind a single variable to a form
that produces a single value.  The macros mv?-let and mv?  are provided
to facilitate the writing of macros that traffic in expressions that
could return one or more (multiple) values.

For example, the form

     (mv?-let (y)
              (f x)
              (declare (type integer y))
              (g x y z))

is equivalent to the following form.

     (let ((y (f x)))
       (declare (type integer y))
       (g x y z))

Calls of mv?-let and of mv-let are equivalent when the first argument
contains at least two variables; see MV-LET for documentation.
In the case of binding a single variable, the general form is

     (mv?-let (var)
              term
              (declare ...) ... (declare ...)
              body)

and this is equivalent to the following form (see LET).

     (let ((var term))
       (declare ...) ... (declare ...)
       body)

Also see MV?.

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.

To see the ACL2 definition of this function, see PF.

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.

To see the ACL2 definition of this function, see PF.

NINTH    ninth member of the list

See any Common Lisp documentation for details.

NO-DUPLICATESP    check for duplicates in a list

     General Forms:
     (no-duplicatesp x)
     (no-duplicatesp x :test 'eql)   ; same as above (eql as equality test)
     (no-duplicatesp x :test 'eq)    ; same, but eq is equality test
     (no-duplicatesp x :test 'equal) ; same, but equal is equality test

(no-duplicatesp lst) is true if and only if no member of lst occurs
twice in lst.  The optional keyword, :TEST, has no effect logically,
but provides the test (default eql) used for comparing elements of lst.

The guard for a call of no-duplicatesp depends on the test.  In all
cases, the argument must satisfy true-listp.  If the test is eql, then
the argument must satisfy eqlable-listp.  If the test is eq, then the
argument must satisfy symbol-listp.

See EQUALITY-VARIANTS for a discussion of the relation between
no-duplicatesp and its variants:

     (no-duplicatesp-eq x lst) is equivalent to (no-duplicatesp x lst
     :test 'eq);

     (no-duplicatesp-equal x lst) is equivalent to (no-duplicatesp x
     lst :test 'equal).

In particular, reasoning about any of these primitives reduces to
reasoning about the function no-duplicatesp-equal.

NO-DUPLICATESP-EQ    See NO-DUPLICATESP.

NO-DUPLICATESP-EQUAL    See NO-DUPLICATESP.

NON-EXEC    mark code as non-executable

Non-exec is a macro such that logically, (non-exec x) is equal to x.
However, the argument to a call of non-exec need not obey the usual
syntactic restrictions for executable code, and indeed, evaluation of a
call of non-exec will result in an error.  Moreover, for any form
occurring in the body of a function (see DEFUN) that is a call
of non-exec, no guard proof obligations are generated for that form.

The following example, although rather contrived, illustrates the use of
non-exec.  One can imagine a less contrived example that efficiently
computes return values for a small number of fixed inputs and, for other
inputs, returns something logically "consistent" with those return
values.

     (defun double (x)
       (case x
         (1 2)
         (2 4)
         (3 6)
         (otherwise (non-exec (* 2 x)))))

We can prove that double is compliant with Common Lisp (see
GUARD) and that it always computes (* 2 x).

     (verify-guards double)
     (thm (equal (double x) (* 2 x)))

We can evaluate double on the specified arguments.  But a call of
non-exec results in an error message that reports the form that was
supplied to non-exec.

     ACL2 !>(double 3)
     6
     ACL2 !>(double 10)

     ACL2 Error in TOP-LEVEL:  ACL2 has been instructed to cause an error
     because of an attempt to evaluate the following form (see :DOC non-
     exec):

       (* 2 X).

     To debug see :DOC print-gv, see :DOC trace, and see :DOC wet.

     ACL2 !>

During proofs, the error is silent; it is "caught" by the proof
mechanism and generally results in the introduction of a call of hide
during a proof.

Also see DEFUN-NX for a utility that makes every call of a
function non-executable, rather than a specified form.  The following
examples contrast non-exec with defun-nx, in particular illustratating
the role of non-exec in avoiding guard proof obligations.

     ; Guard verification fails:
     (defun-nx f1 (x)
       (declare (xargs :guard t))
       (car x))

     ; Guard verification succeeds after changing the guard above:
     (defun-nx f1 (x)
       (declare (xargs :guard (consp x)))
       (car x))

     ; Guard verification succeeds:
     (defun f2 (x)
       (declare (xargs :guard t))
       (non-exec (car x)))

     ; Evaluating (g1) prints "Hello" before signaling an error.
     (defun g1 ()
       (f1 (cw "Hello")))

     ; Evaluating (g2) does not print before signaling an error.
     (defun g2 ()
       (non-exec (cw "Hello")))

     ; Evaluating (h1) gives a guard violation for taking reciprocal of 0.
     (defun h1 ()
       (f1 (/ 1 0)))

     ; Evaluating (h2) does not take a reciprocal, hence there is no guard
     ; violation for that; we just get the error expected from using non-exec.
     (defun h2 ()
       (non-exec (/ 0)))

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.

To see the ACL2 definition of this function, see PF.

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.

To see the ACL2 definition of this function, see PF.

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.

To see the ACL2 definition of this function, see PF.

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.

To see the ACL2 definition of this function, see PF.

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.

To see the ACL2 definition of this function, see PF.

NUMERATOR    dividend of a ratio in lowest terms

Completion Axiom (completion-of-numerator):

     (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).

To see the ACL2 definition of this function, see PF.

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.

To see the ACL2 definition of this function, see PF.

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.

To see the ACL2 definition of this function, see PF.

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.

To see the ACL2 definition of this function, see PF.

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.

To see the ACL2 definition of this function, see PF.

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.

To see the ACL2 definition of this function, see PF.

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<.

OBSERVATION    print an observation

Here is a typical application of observation.

     ACL2 !>(let ((ctx 'top-level)
                  (name 'foo))
              (observation ctx
                           "Skipping processing of name ~x0."
                           name))

     ACL2 Observation in TOP-LEVEL:  Skipping processing of name FOO.
     <state>
     ACL2 !>

Observation prints an initial "ACL2 Observation...:  ", and then prints
the indicated message using formatted printing (see FMT).
Notice in the example above that evaluation of a call of observation
returns state.  Indeed, observation is actually a macro whose expansion
takes and returns the ACL2 state.  A similar utility, observation-cw,
is available that does not take or return state; rather, it returns nil
as the suffix "cw" suggests that a "comment window" is the target of
this printing, rather than the state.  For example:

     ACL2 !>(let ((ctx 'top-level)
                  (name 'foo))
              (observation-cw ctx
                              "Skipping processing of name ~x0."
                              name))

     ACL2 Observation in TOP-LEVEL:  Skipping processing of name FOO.
     NIL
     ACL2 !>

Observation-cw takes exactly the same arguments as observation, but
observation-cw does its printing in a so-called "wormhole"; see
WORMHOLE.

     General Forms:
     (observation    ctx fmt-string fmt-arg1 fmt-arg2 ... fmt-argk)
     (observation-cw ctx fmt-string fmt-arg1 fmt-arg2 ... fmt-argk)

where ctx generally evaluates to a symbol (but see below), and
fmt-string together with the fmt-argi are suitable for passing to fmt.
Output begins and ends with a newline.

Recall from the example above that the output from a call of observation
(or observation-cw) begins with "ACL2 Observation" and additional
characters ending in ":  ", for example " in TOP-LEVEL:  ", followed by
formatted output produced from fmt-string with the given fmt-argi.  The
characters printed immediately following the string "ACL2 Observation"
depend on the value of ctx.  If ctx is nil, nothing is printed.  If ctx
is a non-nil symbol, it is printed using fmt directive ~x.  If ctx is a
cons pair whose car is a symbol, formatted printing is applied to the
string "(~x0 ~x1 ...)", where #\0 and #\1 are bound respectively to
that car and cdr.  Otherwise, ctx is printed using fmt directive ~@.

We next discuss situations in which printing is inhibited for
observation and observation-cw.  No printing is done when observation
is among the inhibited output types; see
SET-INHIBIT-OUTPUT-LST.  Moreover, no printing is done by observation
during include-book.  If you want to avoid printing from observation-cw
during include-book, then you need to manage that yourself.

OBSERVATION-CW    See OBSERVATION.

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.

To see the ACL2 definition of this function, see PF.

OPEN-INPUT-CHANNEL    See IO.

OPEN-INPUT-CHANNEL-P    See IO.

OPEN-OUTPUT-CHANNEL    See IO.

OPEN-OUTPUT-CHANNEL-P    See IO.

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.

To see the ACL2 definition of this function, see PF.

PEEK-CHAR$    See IO.

PKG-IMPORTS    list of symbols imported into a given package

Completion Axiom (completion-of-pkg-imports):

     (equal (pkg-imports x)
            (if (stringp x)
                (pkg-imports x)
              nil))

Guard for (pkg-imports x):

     (stringp x)

(Pkg-imports pkg) returns a duplicate-free list of all symbols imported
into pkg, which should be the name of a package known to ACL2.  For
example, suppose "MY-PKG" was created by

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

Then (pkg-imports "MY-PKG") equals the list (ACL2::ABC LISP::CAR).

If pkg is not a string, then (pkg-imports pkg) is nil.  If pkg is a
string but not the name of a package known to ACL2, then the value of
the form (pkg-imports pkg) is unspecified, and it evaluation will fail
to yield a value.  By "the symbols imported into pkg" we mean the
symbols imported into pkg by the defpkg event that introduced pkg.
There are no imports for built-in packages except for the "ACL2"
package, which imports the symbols in the list value of the constant
*common-lisp-symbols-from-main-lisp-package*.  In particular, this is
the case for the "COMMON-LISP" package.  Users familiar with Common
Lisp may find this surprising, since in actual Common Lisp
implementations it is often the case that many symbols in that package
are imported from other packages.  However, ACL2 treats all symbols in
the constant *common-lisp-symbols-from-main-lisp-package* as having a
symbol-package-name of "COMMON-LISP", as though they were not imported.
ACL2 admits a symbol imported into in the "COMMON-LISP" package only if
it belongs to that list: any attempt to read any other symbol imported
into the "COMMON-LISP" package, or to produce such a symbol with
intern$ or intern-in-package-of-symbol, will cause an error.

The following axioms formalize properties of pkg-imports discussed above
(use :pe to view them).

     symbol-package-name-intern-in-package-of-symbol
     intern-in-package-of-symbol-is-identity
     symbol-listp-pkg-imports
     no-duplicatesp-pkg-imports
     completion-of-pkg-imports

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.

To see the ACL2 definition of this function, see PF.

POSITION    position of an item in a string or a list

     General Forms:
     (position x seq)
     (position x seq :test 'eql)   ; same as above (eql as equality test)
     (position x seq :test 'eq)    ; same, but eq is equality test
     (position x seq :test 'equal) ; same, but equal is equality test

(Position x seq) is the least index (zero-based) of the element x in
the string or list seq, if x is an element of seq.  Otherwise (position
x seq) is nil.  The optional keyword, :TEST, has no effect logically,
but provides the test (default eql) used for comparing x with items of
seq.

The guard for a call of position depends on the test.  In all cases,
the second argument must satisfy stringp or true-listp.  If the test is
eql, then either the first argument must be suitable for eql (see
EQLABLEP) or the second argument must satisfy eqlable-listp.  If the
test is eq, then either the first argument must be a symbol or the
second argument must satisfy symbol-listp.

See EQUALITY-VARIANTS for a discussion of the relation between
position and its variants:

     (position-eq x seq) is equivalent to (position x seq :test 'eq);

     (position-equal x seq) is equivalent to (position x seq :test
     'equal).

In particular, reasoning about any of these primitives reduces to
reasoning about the function position-equal.

Position is defined by Common Lisp.  See any Common Lisp documentation
for more information.

POSITION-EQ    See POSITION.

POSITION-EQUAL    See POSITION.

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.

To see the ACL2 definition of this function, see PF.

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)))

PRINC$    print an atom

Use princ$ to do basic printing of atoms (i.e., other than cons pairs).
In particular, princ$ prints a string without the surrounding
double-quotes and without escaping double-quote characters within the
string.  Note that princ is sensitive to the print-base and print-case;
see SET-PRINT-BASE and see SET-PRINT-CASE.  Princ$
returns state.

     Examples:
     ACL2 !>(princ$ "Howdy ho" (standard-co state) state)
     Howdy ho<state>
     ACL2 !>(pprogn (princ$ "Howdy ho" (standard-co state) state)
                    (newline (standard-co state) state))
     Howdy ho
     <state>
     ACL2 !>(princ$ "ab\"cd" *standard-co* state)
     ab"cd<state>
     ACL2 !>
     ACL2 !>(princ$ 17 *standard-co* state)
     17<state>
     ACL2 !>(set-print-base 16 state)
     <state>
     ACL2 !>(princ$ 17 *standard-co* state)
     11<state>
     ACL2 !>(princ$ 'xyz *standard-co* state)
     XYZ<state>
     ACL2 !>(set-print-case :downcase state)
     <state>
     ACL2 !>(princ$ 'xyz *standard-co* state)
     xyz<state>
     ACL2 !>

See FMT for more sophisticated printing routines, and see
IO for general information about input and output.

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$.  Also
see PROGN$ for an extension of prog2$ that handles than two
arguments.

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))))

PROGN$    execute a sequence of forms and return the value of the last one

This macro expands to a corresponding nest of calls of prog2$; see
PROG2$.  The examples below show how this works: the first case
below is typical, but we conclude with two special cases.

     ACL2 !>:trans1 (progn$ (f1 x) (f2 x) (f3 x))
      (PROG2$ (F1 X) (PROG2$ (F2 X) (F3 X)))
     ACL2 !>:trans1 (progn$ (f1 x) (f2 x))
      (PROG2$ (F1 X) (F2 X))
     ACL2 !>:trans1 (progn$ (f1 x))
      (F1 X)
     ACL2 !>:trans1 (progn$)
      NIL
     ACL2 !>

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.

To see the ACL2 definition of this function, see PF.

PSEUDO-TERMP    a predicate for recognizing term-like s-expressions

     Example Forms:
     (pseudo-termp '(car (cons x 'nil)))      ; has value t
     (pseudo-termp '(car x y z))              ; also has value t!
     (pseudo-termp '(delta (h x)))            ; has value t
     (pseudo-termp '(delta (h x) . 7))        ; has value nil (not a true-listp)
     (pseudo-termp '((lambda (x) (car x)) b)) ; has value t
     (pseudo-termp '(if x y 123))             ; has value nil (123 is not quoted)
     (pseudo-termp '(if x y '123))            ; has value t

If x is the quotation of a term, then (pseudo-termp x) is t.  However,
if x is not the quotation of a term it is not necessarily the case that
(pseudo-termp x) is nil.

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

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

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

Metafunctions may use pseudo-termp as a guard.

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

     General Forms:
     (put-assoc name val alist)
     (put-assoc name val alist :test 'eql)   ; same as above (eql as equality test)
     (put-assoc name val alist :test 'eq)    ; same, but eq is equality test
     (put-assoc name val alist :test 'equal) ; same, but equal is equality test

(Put-assoc 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 for a call of put-assoc depends on the test.  In all cases,
the last argument must satisfy alistp.  If the test is eql, then either
the first argument must be suitable for eql (see EQLABLEP) or
the last argument must satisfy eqlable-alistp.  If the test is eq, then
either the first argument must be a symbol or the last argument must
satisfy symbol-alistp.

See EQUALITY-VARIANTS for a discussion of the relation between
put-assoc and its variants:

     (put-assoc-eq name val alist) is equivalent to (put-assoc name val
     alist :test 'eq);

     (put-assoc-equal name val alist) is equivalent to (put-assoc name
     val alist :test 'equal).

In particular, reasoning about any of these primitives reduces to
reasoning about the function put-assoc-equal.

PUT-ASSOC-EQ    See PUT-ASSOC.

PUT-ASSOC-EQL    See PUT-ASSOC.

PUT-ASSOC-EQUAL    See PUT-ASSOC.

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.

To see the ACL2 definition of this function, see PF.

QUOTE    create a constant

The form (quote x) evaluates to x.  See any Common Lisp documentation.

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

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

To see the ACL2 definition of this function, see PF.

R-SYMBOL-ALISTP    recognizer for association lists with symbols as values

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

To see the ACL2 definition of this function, see PF.

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

     General Forms:
     (rassoc x alist)
     (rassoc x alist :test 'eql)   ; same as above (eql as equality test)
     (rassoc x alist :test 'eq)    ; same, but eq is equality test
     (rassoc x alist :test 'equal) ; same, but equal is equality test

(Rassoc x alist) is the first member of alist whose cdr is x, or nil if
no such member exists.  (rassoc x alist) is thus 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 optional keyword, :TEST, has no effect logically, but
provides the test (default eql) used for comparing x with the cdrs of
successive elements of lst.

The guard for a call of rassoc depends on the test.  In all cases, the
second argument must satisfy alistp.  If the test is eql, then either
the first argument must be suitable for eql (see EQLABLEP) or
the second argument must satisfy r-eqlable-alistp.  If the test is eq,
then either the first argument must be a symbol or the second argument
must satisfy r-symbol-alistp.

See EQUALITY-VARIANTS for a discussion of the relation between
rassoc and its variants:

     (rassoc-eq x lst) is equivalent to (rassoc x lst :test 'eq);

     (rassoc-equal x lst) is equivalent to (rassoc x lst :test 'equal).

In particular, reasoning about any of these primitives reduces to
reasoning about the function rassoc-equal.

Rassoc is defined by Common Lisp.  See any Common Lisp documentation for
more information.

RASSOC-EQ    See RASSOC.

RASSOC-EQUAL    See RASSOC.

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.

To see the ACL2 definition of this function, see PF.

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.

READ-RUN-TIME    read elapsed runtime

(Read-run-time state) returns (mv runtime state), where runtime is the
elapsed runtime since the start of the current ACL2 session and state
is the resulting ACL2 state.

The logical definition probably won't concern many users, but for
completeness, we say a word about it here.  That definition uses the
function read-acl2-oracle, which modifies state by popping the returned
runtime value from its acl2-oracle field.

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.

To see the ACL2 definition of this function, see PF.

REALPART    real part of a complex number

Completion Axiom (completion-of-realpart):

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

Guard for (realpart x):

     (acl2-numberp x)

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.

To see the ACL2 definition of this function, see PF.

REMOVE    remove all occurrences

     General Forms:
     (remove x lst)
     (remove x lst :test 'eql)   ; same as above (eql as equality test)
     (remove x lst :test 'eq)    ; same, but eq is equality test
     (remove x lst :test 'equal) ; same, but equal is equality test

(Remove x lst) is equal to lst if x is not a member of lst, else is the
result of removing all occurrences of x from lst.  The optional
keyword, :TEST, has no effect logically, but provides the test (default
eql) used for comparing x with successive elements of lst.

Also see REMOVE1.

The guard for a call of remove depends on the test.  In all cases, the
second argument must satisfy true-listp.  If the test is eql, then
either the first argument must be suitable for eql (see
EQLABLEP) or the second argument must satisfy eqlable-listp.  If the
test is eq, then either the first argument must be a symbol or the
second argument must satisfy symbol-listp.

See EQUALITY-VARIANTS for a discussion of the relation between
remove and its variants:

     (remove-eq x lst) is equivalent to (remove x lst :test 'eq);

     (remove-equal x lst) is equivalent to (remove x lst :test 'equal).

In particular, reasoning about any of these primitives reduces to
reasoning about the function remove-equal.

Remove is defined by Common Lisp.  See any Common Lisp documentation for
more information.

REMOVE-DUPLICATES    remove duplicates from a string or a list

     General Forms:
     (remove-duplicates x)
     (remove-duplicates x :test 'eql)   ; same as above (eql as equality test)
     (remove-duplicates x :test 'eq)    ; same, but eq is equality test
     (remove-duplicates x :test 'equal) ; same, but equal is equality test

(Remove-duplicates x) returns the result of deleting duplicate elements
from the beginning of the list or string x.  For example,
(remove-duplicates '(1 2 3 2 4)) is equal to '(1 3 2 4).  The optional
keyword, :TEST, has no effect logically, but provides the test (default
eql) used for comparing x with successive elements of lst.

The guard for a call of remove-duplicates depends on the test.  In all
cases, the argument must satisfy stringp or true-listp.  If the test is
eql, then the argument must satisfy either stringp or eqlable-listp.
If the test is eq, then the argument must satisfy symbol-listp.

The relation between remove-duplicates and its variants is related to
the usual pattern for equality variants; see EQUALITY-VARIANTS.
However, the possibility of a string argument changes the usual pattern
a bit.  As one might expect:

     (remove-duplicates-eq lst) is equivalent to (remove-duplicates lst
     :test 'eq).

However, remove-duplicates-equal is defined without consideration of
strings, for backward compatibility with versions of ACL2 through
Version_4.2.  The macro remove-duplicates-logic has been introduced to
model the behavior of remove-duplicates even on strings; use :pe if you
wish to see its definition.  So we can say the following.

     (remove-duplicates-logic lst) is equivalent to (remove-duplicates
     lst :test 'equal); and

     (remove-duplicates-logic lst) is equal to (remove-duplicates-equal
     lst) when lst is not a string.

In particular, when the argument is not a string, reasoning about any of
these primitives reduces to reasoning about the function
remove-duplicates-equal.

Remove-duplicates is defined by Common Lisp.  See any Common Lisp
documentation for more information.

REMOVE-DUPLICATES-EQ    See REMOVE-DUPLICATES.

REMOVE-DUPLICATES-EQUAL    See REMOVE-DUPLICATES.

REMOVE-EQ    See REMOVE.

REMOVE-EQUAL    See REMOVE.

REMOVE1    remove first occurrences, testing using eql

     General Forms:
     (remove1 x lst)
     (remove1 x lst :test 'eql)   ; same as above (eql as equality test)
     (remove1 x lst :test 'eq)    ; same, but eq is equality test
     (remove1 x lst :test 'equal) ; same, but equal is equality test

(Remove1 x lst) is equal to lst if x is not a member of lst, else is
the result of removing the first occurrences of x from lst.  The
optional keyword, :TEST, has no effect logically, but provides the test
(default eql) used for comparing x with successive elements of lst.

Also see REMOVE.

The guard for a call of remove1 depends on the test.  In all cases, the
second argument must satisfy true-listp.  If the test is eql, then
either the first argument must be suitable for eql (see
EQLABLEP) or the second argument must satisfy eqlable-listp.  If the
test is eq, then either the first argument must be a symbol or the
second argument must satisfy symbol-listp.

See EQUALITY-VARIANTS for a discussion of the relation between
remove1 and its variants:

     (remove1-eq x lst) is equivalent to (remove1 x lst :test 'eq);

     (remove1-equal x lst) is equivalent to (remove1 x lst :test
     'equal).

In particular, reasoning about any of these primitives reduces to
reasoning about the function remove1-equal.

REMOVE1-EQ    See REMOVE1.

REMOVE1-EQUAL    See REMOVE1.

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.

RETURN-LAST    return the last argument, perhaps with side effects

Return-last is an ACL2 function that returns its last argument.  It is
used to implement common utilities such as prog2$ and time$.  For most
users, this may already be more than one needs to know about
return-last; for example, ACL2 tends to avoid printing calls of
return-last in its output, printing calls of prog2$ or time$ (or other
such utilities) instead.

If you encounter a call of return-last during a proof, then you may find
it most useful to consider return-last simply as a function defined by
the following equation.

     (equal (return-last x y z) z)

It may also be useful to know that unlike other ACL2 functions,
return-last can take a multiple value as its last argument, in which
case this multiple value is returned.  The following contrived
definition illustrates this point.

     ACL2 !>(defun foo (fn x y z)
              (return-last fn x (mv y z)))

     Since FOO is non-recursive, its admission is trivial.  We observe that
     the type of FOO is described by the theorem
     (AND (CONSP (FOO FN X Y Z)) (TRUE-LISTP (FOO FN X Y Z))).  We used
     primitive type reasoning.

     (FOO * * * *) => (MV * *).

     Summary
     Form:  ( DEFUN FOO ...)
     Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL))
     Time:  0.01 seconds (prove: 0.00, print: 0.00, other: 0.01)
      FOO
     ACL2 !>(foo 'bar 3 4 5)
     (4 5)
     ACL2 !>(mv-let (a b)
                    (foo 'bar 3 4 5)
                    (cons b a))
     (5 . 4)
     ACL2 !>

Most readers would be well served to avoid reading the rest of this
documentation of return-last.  For reference, however, below we document
it in some detail.  We include some discussion of its evaluation, in
particular its behavior in raw Lisp, because we expect that most who
read further are working with raw Lisp code (and trust tags).

Return-last is an ACL2 function that can arise from macroexpansion of
certain utilities that return their last argument, which may be a
multiple value.  Consider for example the simplest of these, prog2$:

     ACL2 !>:trans1 (prog2$ (cw "Some CW printing...~%") (+ 3 4))
      (RETURN-LAST 'PROGN
                   (CW "Some CW printing...~%")
                   (+ 3 4))
     ACL2 !>

Notice that a call of prog2$ macroexpands to a call of return-last in
which the first argument is (quote progn).  Although return-last is a
function in the ACL2 world, it is implemented "under the hood" as a
macro in raw Lisp, as the following log (continuing the example above)
illustrates.

     ACL2 !>:q

     Exiting the ACL2 read-eval-print loop.  To re-enter, execute (LP).
     ? [RAW LISP] (macroexpand-1 '(RETURN-LAST 'PROGN
                                                (CW "Some CW printing...~%")
                                                (+ 3 4)))
     (PROGN (LET ((*AOKP* T)) (CW "SOME CW PRINTING...~%")) (+ 3 4))
     T
     ? [RAW LISP]

Thus, the original prog2$ call generates a corresponding call of progn
in raw Lisp, which in turn causes evaluation of each argument and
returns whatever is returned by evaluation of the last (second)
argument.

(Remark for those who use defattach.  The binding of *aokp* to t is
always included for the second argument as shown except when the first
argument is of the form (QUOTE M) where M is a macro, or (less
important) when the first argument is a symbol or a cons whose car is
QUOTE.  This binding allows ACL2 to use attachments in the second
argument of return-last (hence, in the first argument of prog2$), even
in contexts such as proofs in which attachments are normally not
allowed.  Those who use the experimental HONS version of ACL2 (see
HONS-AND-MEMOIZATION) will see an additional binding in the
above single-step macroexpansion, which allows the storing of memoized
results even when that would otherwise be prevented because of the use
of attachments.)

In general, a form (return-last (quote F) X Y) macroexpands to (F X Y),
where F is defined in raw Lisp to return its last argument.  The case
that F is progn is a bit misleading, because it is so simple.  More
commonly, macroexpansion produces a call of a macro defined in raw Lisp
that may produce side effects.  Consider for example the ACL2 utility
with-guard-checking, which is intended to change the guard-checking
mode to the indicated value (see WITH-GUARD-CHECKING).

     ACL2 !>(with-guard-checking :none (car 3)) ; no guard violation
     NIL
     ACL2 !>:trans1 (with-guard-checking :none (car 3))
      (WITH-GUARD-CHECKING1 (CHK-WITH-GUARD-CHECKING-ARG :NONE)
                            (CAR 3))
     ACL2 !>:trans1 (WITH-GUARD-CHECKING1 (CHK-WITH-GUARD-CHECKING-ARG :NONE)
                                          (CAR 3))
      (RETURN-LAST 'WITH-GUARD-CHECKING1-RAW
                   (CHK-WITH-GUARD-CHECKING-ARG :NONE)
                   (CAR 3))
     ACL2 !>:q

     Exiting the ACL2 read-eval-print loop.  To re-enter, execute (LP).
     ? [RAW LISP] (macroexpand-1
                   '(RETURN-LAST 'WITH-GUARD-CHECKING1-RAW
                                  (CHK-WITH-GUARD-CHECKING-ARG :NONE)
                                  (CAR 3)))
     (WITH-GUARD-CHECKING1-RAW (CHK-WITH-GUARD-CHECKING-ARG :NONE) (CAR 3))
     T
     ? [RAW LISP] (pprint
                   (macroexpand-1
                    '(WITH-GUARD-CHECKING1-RAW
                      (CHK-WITH-GUARD-CHECKING-ARG :NONE)
                      (CAR 3))))

     (LET ((ACL2_GLOBAL_ACL2::GUARD-CHECKING-ON
            (CHK-WITH-GUARD-CHECKING-ARG :NONE)))
       (DECLARE (SPECIAL ACL2_GLOBAL_ACL2::GUARD-CHECKING-ON))
       (CAR 3))
     ? [RAW LISP]

The above raw Lisp code binds the state global variable
guard-checking-on to :none, as chk-with-guard-checking-arg is just the
identity function except for causing a hard error for an illegal input.

The intended use of return-last is that the second argument is evaluated
first in a normal manner, and then the third argument is evaluated in an
environment that may depend on the value of the second argument.  (For
example, the macro with-prover-time-limit macroexpands to a call of
return-last with a first argument of 'WITH-PROVER-TIME-LIMIT1-RAW, a
second argument that evaluates to a numeric time limit, and a third
argument that is evaluated in an environment where the theorem prover
is restricted to avoid running longer than that time limit.)  Although
this intended usage model is not strictly enforced, it is useful to
keep in mind in the following description of how calls of return-last
are handled by the ACL2 evaluator.

When a form is submitted in the top-level loop, it is handled by ACL2's
custom evaluator.  That evaluator is specified to respect the semantics
of the expression supplied to it: briefly put, if an expression E
evaluates to a value V, then the equality (equal E (quote V)) should be
a theorem.  Notice that this specification does not discuss the
side-effects that may occur when evaluating a call of return-last, so
we discuss that now.  Suppose that the ACL2 evaluator encounters the
call (return-last 'fn expr1 expr2).  First it evaluates expr1.  If this
evaluation succeeds without error, then it constructs an expression of
the form (fn *x* ev-form), where *x* is a Lisp variable bound to the
result of evaluating expr1 and ev-form is a call of the evaluator for
expr2.  (Those who want implementation details are invited to look at
function ev-rec-return-last in ACL2 source file translate.lisp.)  There
are exceptions if fn is progn, ec-call1-raw, with-guard-checking1-raw,
or mbe1-raw, but the main idea is the same: do a reasonable job
emulating the behavior of a raw-Lisp call of return-last.

The following log shows how a time$ call can generate a call of the
evaluator for the last argument of return-last (arguent expr2, above).
We use :trans1 to show single-step macroexpansions, which indicate how
a call of time$ expands to a call of return-last.  The implementation
actually binds the Lisp variable *RETURN-LAST-ARG3* to expr2 before
calling the ACL2 evaluator, ev-rec.

     ACL2 !>:trans1 (time$ (+ 3 4))
      (TIME$1 (LIST 0 NIL NIL NIL NIL)
              (+ 3 4))
     ACL2 !>:trans1 (TIME$1 (LIST 0 NIL NIL NIL NIL)
                            (+ 3 4))
      (RETURN-LAST 'TIME$1-RAW
                   (LIST 0 NIL NIL NIL NIL)
                   (+ 3 4))
     ACL2 !>(time$ (+ 3 4))
     ; (EV-REC *RETURN-LAST-ARG3* ...) took
     ; 0.00 seconds realtime, 0.00 seconds runtime
     ; (1,120 bytes allocated).
     7
     ACL2 !>

We now show how things can go wrong in other than the "intended use"
case described above.  In the example below, the macro mac-raw is
operating directly on the syntactic representation of its first
argument, which it obtains of course as the second argument of a
return-last call.  Again this "intended use" of return-last requires
that argument to be evaluated and then only its result is relevant; its
syntax is not supposed to matter.  We emphasize that only top-level
evaluation depends on this "intended use"; once evaluation is passed to
Lisp, the issue disappears.  We illustrate below how to use the
top-level utility to avoid this issue; see TOP-LEVEL.  The
example uses the utility defmacro-last to "install" special handling of
the raw-Lisp macro mac-raw by return-last; later below we discuss
defmacro-last.

     ACL2 !>(defttag t)

     TTAG NOTE: Adding ttag :T from the top level loop.
      T
     ACL2 !>(progn!
              (set-raw-mode t)
              (defmacro mac-raw (x y)
                `(progn (print (quote ,(cadr x)))
                        (terpri) ; newline
                        ,y)))

     Summary
     Form:  ( PROGN! (SET-RAW-MODE T) ...)
     Rules: NIL
     Time:  0.01 seconds (prove: 0.00, print: 0.00, other: 0.01)
      NIL
     ACL2 !>(defmacro-last mac)
     [[ ... output omitted ... ]]
      RETURN-LAST-TABLE
     ACL2 !>(return-last 'mac-raw '3 nil)

     ***********************************************
     ************ ABORTING from raw Lisp ***********
     Error:  Fault during read of memory address #x120000300006
     ***********************************************

     If you didn't cause an explicit interrupt (Control-C),
     then the root cause may be call of a :program mode
     function that has the wrong guard specified, or even no
     guard specified (i.e., an implicit guard of t).
     See :DOC guards.

     To enable breaks into the debugger (also see :DOC acl2-customization):
     (SET-DEBUGGER-ENABLE T)
     ACL2 !>(top-level (return-last 'mac-raw '3 nil))

     3
     NIL
     ACL2 !>

We next describe how to extend the behavior of return-last.  This
requires an active trust tag (see DEFTTAG), and is accomplished
by extending a table provided by ACL2, see RETURN-LAST-TABLE.
Rather than using table events directly for this purpose, it is
probably more convenient to use a macro, defmacro-last.  We describe
the distributed book books/misc/profiling.lisp in order to illustrate
how this works.  The events in that book include the following, which
are described below.

     (defttag :profiling)

     (progn!
      (set-raw-mode t)
      (load (concatenate 'string (cbd) "profiling-raw.lsp")))

     (defmacro-last with-profiling)

The first event introduces a trust tag.  The second loads a file into
raw Lisp that defines a macro, with-profiling-raw, which can do
profiling for the form to be evaluated.  The third introduces an ACL2
macro with-profiling, whose calls expand into calls of the form
(return-last (quote with-profiling-raw) & &).  The third event also
extends return-last-table so that these calls will expand in raw Lisp
to calls of with-profiling-raw.

The example above illustrates the following methodology for introducing
a macro that returns its last argument but produces useful side-effects
with raw Lisp code.

     (1) Introduce a trust tag (see DEFTTAG).

     (2) Using progn!, load into raw Lisp a file defining a macro,
     RAW-NAME, that takes two arguments, returning its last (second)
     argument but using the first argument to produce desired side
     effects during evaluation of that last argument.

     (3) Evaluate the form (defmacro-last NAME :raw RAW-NAME).  This
     will introduce NAME as an ACL2 macro that expands to a
     corresponding call of RAW-NAME (see (2) above) in raw Lisp.  The
     specification of keyword value of :raw as RAW-NAME may be omitted
     if RAW-NAME is the result of modifying the symbol NAME by
     suffixing the string "-RAW" to the symbol-name of NAME.

WARNING: Not every use of return-last can be soundly evaluated outside a
function body.  The reason is that ACL2's evaluator, ev-rec, recurs
through terms that are presented in the top-level loop, and handles
return-last calls in a special manner: basically, the call of ev-rec on
the form (return-last 'mac-raw x y) leads to evaluation of a macro call
of the form (mac-raw *return-last-arg2* (ev-rec ...)), where
*return-last-arg2* is a global variable bound to the result of
evaluating x with ev-rec.  Consider the following example.

     (defttag t)
     (set-raw-mode-on state)
     (defmacro mac-raw (str y) ; print message is an atom
      `(let ((result (consp ,y))
             (str ,str))
         (or result
             (prog2$ (fmx ,str ',y)
                     nil))))
     (set-raw-mode-off state)
     (defmacro-last mac)
     ; Horrible error:
     (mac "Not a cons: ~x0~%" 17)
     ; Works, but probably many would consider it awkward to use top-level:
     (top-level (mac "Not a cons: ~x0~%" 17))

In such cases we suggest supplying keyword :top-level-ok nil to the call
of defmacro-last, for example:

     (defmacro-last mac :top-level-ok nil)

Then any attempt to call mac at the top level, as opposed to inside a
function body, will cause a clean error before evaluation begins.

It is useful to explore what is done by defmacro-last.

     ACL2 !>:trans1 (defmacro-last with-profiling)
      (PROGN (DEFMACRO WITH-PROFILING (X Y)
                       (LIST 'RETURN-LAST
                             (LIST 'QUOTE 'WITH-PROFILING-RAW)
                             X Y))
             (TABLE RETURN-LAST-TABLE 'WITH-PROFILING-RAW
                    'WITH-PROFILING))
     ACL2 !>:trans1 (with-profiling '(assoc-eq fgetprop rewrite) (mini-proveall))
      (RETURN-LAST 'WITH-PROFILING-RAW
                   '(ASSOC-EQ FGETPROP REWRITE)
                   (MINI-PROVEALL))
     ACL2 !>:q

     Exiting the ACL2 read-eval-print loop.  To re-enter, execute (LP).
     ? [RAW LISP] (macroexpand-1
                   '(RETURN-LAST 'WITH-PROFILING-RAW
                                  '(ASSOC-EQ FGETPROP REWRITE)
                                  (MINI-PROVEALL)))
     (WITH-PROFILING-RAW '(ASSOC-EQ FGETPROP REWRITE) (MINI-PROVEALL))
     T
     ? [RAW LISP]

To understand the macro with-profiling-raw you could look at the
distributed file loaded above: books/misc/profiling-raw.lsp.  If you
wish to automate certification of such a book with makefiles (see
BOOK-MAKEFILES, perhaps contributing such a book to the ACL2 books
repository (see `http://acl2-books.googlecode.com/'), you may also wish
to look at distributed file books/misc/Makefile, where you'll notice
the following extra `make' dependency:

     profiling.cert: profiling-raw.lsp

We mentioned above that ACL2 tends to print calls of prog2$ or time$
(or other such utilities) instead of calls of return-last.  Here we
elaborate that point.  ACL2's `untranslate' utility treats (return-last
(quote F) X Y) as (G X Y) if F corresponds to the symbol G in
return-last-table.  However, it is generally rare to encounter such a
term during a proof, since calls of return-last are generally expanded
away early during a proof.

Calls of return-last that occur in code -- forms submitted in the
top-level ACL2 loop, and definition bodies other than those marked as
non-executable (see DEFUN-NX) -- have the following
restriction: if the first argument is of the form (quote F), then F
must be an entry in return-last-table.  There are however four
exceptions: the following symbols are considered to be keys of
return-last-table even if they are no longer associated with non-nil
values, say because of a table event with keyword :clear.

     * progn, associated with prog2$
     * mbe1-raw, associated with mbe1, a version of mbe
     * ec-call1-raw, associated with ec-call1 (a variant of ec-call)
     * with-guard-checking1-raw, associated with with-guard-checking1 (a
     variant of with-guard-checking)

Note that because of its special status, it is illegal to trace
return-last.

We conclude by warning that as a user, you take responsibility for not
compromising the soundness or error handling of ACL2 when you define a
macro in raw Lisp and especially when you install it as a key of
return-last-table, either directly or (more likely) using
defmacro-last.  In particular, be sure that you are defining a macro of
two arguments that always returns the value of its last argument,
returning the complete multiple value if that last argument evaluates
to a multiple value.

The following is correct, and illustrates care taken to return multiple
values.

     :q
     (defmacro my-time1-raw (val form)
       (declare (ignore val))
       `(let  ((start-time (get-internal-run-time))
               (result (multiple-value-list ,form))
               (end-time (get-internal-run-time)))
          (format t "Total time: ~s~%"
                  (float (/ (- end-time start-time)
                            internal-time-units-per-second)))
          (values-list result)))
     (lp)
     (defttag t)
     (defmacro-last my-time1)
     (defmacro my-time (form)
       `(my-time1 nil ,form))

Then for example:

     ACL2 !>(my-time (equal (make-list 1000000) (make-list 1000000)))
     Total time: 0.12
     T
     ACL2 !>

But if instead we provide the following more naive implementation, of
the above raw Lisp macro, the above evaluation can produce an error,
for example if the host Lisp is CCL.

     (defmacro my-time1-raw (val form)
         (declare (ignore val))
         `(let  ((start-time (get-internal-run-time))
                 (result ,form)
                 (end-time (get-internal-run-time)))
            (format t "Total time: ~s~%"
                    (float (/ (- end-time start-time)
                              internal-time-units-per-second)))
            result)) ; WRONG -- need multiple values returned!

Here is a second, similar example.  This time we'll start with the
error; can you spot it?

     (defttag t)
     (progn!
      (set-raw-mode t)
      (defmacro foo-raw (x y)
        `(prog1
             ,y
           (cw "Message showing argument 1: ~x0~%" ,x))))
     (defmacro-last foo)

We then can wind up with a hard Lisp error:

     ACL2 !>(foo 3 (mv 4 5))
     Message showing argument 1: 3

     ***********************************************
     ************ ABORTING from raw Lisp ***********
     Error:  value NIL is not of the expected type REAL.
     ***********************************************

     If you didn't cause an explicit interrupt (Control-C),
     then the root cause may be call of a :program mode
     function that has the wrong guard specified, or even no
     guard specified (i.e., an implicit guard of t).
     See :DOC guards.

     To enable breaks into the debugger (also see :DOC acl2-customization):
     (SET-DEBUGGER-ENABLE T)
     ACL2 !>

Here is a corrected version of the above macro.  The point here is that
prog1 returns a single value, while our-multiple-value-prog1 returns
all the values that are returned by its first argument.

     (progn!
      (set-raw-mode t)
      (defmacro foo-raw (x y)
        `(our-multiple-value-prog1 ;; better
          ,y
          (cw "Message showing argument 1: ~x0~%" ,x))))

To see the ACL2 definition of this function, see PF.

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.

To see the ACL2 definition of this function, see PF.

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.

To see the ACL2 definition of this function, see PF.

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.

To see the ACL2 definition of this function, see PF.

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,

To see the ACL2 definition of this function, see PF.

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, which must consist of standard characters (see
     STANDARD-CHAR-P) if the :test is char-equal.

     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$    elements of one list that are not elements of another

     General Forms:
     (set-difference$ l1 l2)
     (set-difference$ l1 l2 :test 'eql)   ; same as above (eql as equality test)
     (set-difference$ l1 l2 :test 'eq)    ; same, but eq is equality test
     (set-difference$ l1 l2 :test 'equal) ; same, but equal is equality test

(Set-difference$ l1 l2) equals a list that contains the members of l1
that are not members of l2.  More precisely, the resulting list is the
same as one gets by deleting the members of l2 from l1, leaving the
remaining elements in the same order as in l1.  The optional keyword,
:TEST, has no effect logically, but provides the test (default eql)
used for comparing members of the two lists.

The guard for a call of set-difference$ depends on the test.  In all
cases, both arguments must satisfy true-listp.  If the test is eql,
then one of the arguments must satisfy eqlable-listp.  If the test is
eq, then one of the arguments must satisfy symbol-listp.

See EQUALITY-VARIANTS for a discussion of the relation between
set-difference$ and its variants:

     (set-difference-eq l1 l2) is equivalent to (set-difference$ l1 l2
     :test 'eq);

     (set-difference-equal l1 l2) is equivalent to (set-difference$ l1
     l2 :test 'equal).

In particular, reasoning about any of these primitives reduces to
reasoning about the function set-difference-equal.

Set-difference$ is similar to the Common Lisp primitive set-difference.
However, Common Lisp does not specify the order of elements in the
result of a call of set-difference.

SET-DIFFERENCE-EQ    See SET-DIFFERENCE$.

SET-DIFFERENCE-EQUAL    See SET-DIFFERENCE$.

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")

It may be surprising that setenv$ returns nil; indeed, it neither takes
nor returns the ACL2 state.  The reason is that getenv$ takes
responsibility for trafficking in state; it is defined in the logic
using the function read-acl2-oracle, which (again, in the logic) does
modify state, by popping an entry from its acl2-oracle field.  getenv$.

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.

To see the ACL2 definition of this function, see PF.

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.

To see the ACL2 definition of this function, see PF.

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.

To see the ACL2 definition of this function, see PF.

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.

To see the ACL2 definition of this function, see PF.

STATE-GLOBAL-LET*    bind state global variables

See PROGRAMMING-WITH-STATE for requisite background on
programming with the ACL2 state.

     Example Forms:
     (state-global-let*
      ((inhibit-output-lst *valid-output-names*))
      (thm (equal x x)))

     (state-global-let*
      ((fmt-hard-right-margin 1000 set-fmt-hard-right-margin)
       (fmt-soft-right-margin 1000 set-fmt-soft-right-margin))
      (mini-proveall))

     General Form:
     (state-global-let* ((var1 form1) ; or (var1 form1 set-var1)
                         ...
                         (vark formk) ; or (vark formk set-vark)
                        )
                        body)

where: each vari is a variable; each formi is an expression whose value
is a single ordinary object (i.e. not multiple values, and not state or
any other stobj); set-vari, if supplied, is a function with signature
((set-vari * state) => state); and body is an expression that evaluates
to an error triple.  Each formi is evaluated in order, starting with
form1, and with each such binding the state global variable vari is
bound to the value of formi, sequentially in the style of let*.  More
precisely, then meaning of this form is to set (in order) the global
values of the indicated state global variables vari to the values of
formi using f-put-global, execute body, restore the vari to their
previous values (but see the discussion of setters below), and return
the triple produced by body (with its state as modified by the
restoration).  The restoration is guaranteed even in the face of
aborts.  The "bound" variables may initially be unbound in state and
restoration means to make them unbound again.

Still referring to the General Form above, let old-vali be the value of
state global variable vari at the time vari is about to be assigned the
value of formi.  If set-vari is not supplied, then as suggested above,
the following form is evaluated at the conclusion of the evaluation of
the state-global-let* form, whether or not an error has occurred:
(f-put-global 'vari 'old-vali state).  However, if set-vari is
supplied, then instead the form evaluated will be (set-vari 'old-vali
state).  This capability is particularly useful if vari is untouchable
(see PUSH-UNTOUCHABLE), since the above call of f-put-global is
illegal.

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.

To see the ACL2 definition of this function, see PF.

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 by 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).

To see the ACL2 definition of this function, see PF.

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.

To see the ACL2 definition of this function, see PF.

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.

To see the ACL2 definition of this function, see PF.

STRING-LISTP    recognizer for a true list of strings

The predicate string-listp tests whether its argument is a true-listp
of strings.

To see the ACL2 definition of this function, see PF.

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.

To see the ACL2 definition of this function, see PF.

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.

To see the ACL2 definition of this function, see PF.

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.

To see the ACL2 definition of this function, see PF.

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.

To see the ACL2 definition of this function, see PF.

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.

To see the ACL2 definition of this function, see PF.

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).

To see the ACL2 definition of this function, see PF.

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.

To see the ACL2 definition of this function, see PF.

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 looked 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.

To see the ACL2 definition of this function, see PF.

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.

To see the ACL2 definition of this function, see PF.

SUBSETP    test if every member of one list is a member of the other

     General Forms:
     (subsetp x y)
     (subsetp x y :test 'eql)   ; same as above (eql as equality test)
     (subsetp x y :test 'eq)    ; same, but eq is equality test
     (subsetp x y :test 'equal) ; same, but equal is equality test

(Subsetp x y) is true if and only if every member of the list x is a
member of the list y.  The optional keyword, :TEST, has no effect
logically, but provides the test (default eql) used for comparing
members of the two lists.

The guard for a call of subsetp depends on the test.  In all cases,
both arguments must satisfy true-listp.  If the test is eql, then one
of the arguments must satisfy eqlable-listp.  If the test is eq, then
one of the arguments must satisfy symbol-listp.

See EQUALITY-VARIANTS for a discussion of the relation between
subsetp and its variants:

     (subsetp-eq x lst) is equivalent to (subsetp x lst :test 'eq);

     (subsetp-equal x lst) is equivalent to (subsetp x lst :test
     'equal).

In particular, reasoning about any of these primitives reduces to
reasoning about the function subsetp-equal.

Subsetp is defined by Common Lisp.  See any Common Lisp documentation
for more information.

SUBSETP-EQ    See SUBSETP.

SUBSETP-EQUAL    See SUBSETP.

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.

To see the ACL2 definition of this function, see PF.

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.

To see the ACL2 definition of this function, see PF.

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.

To see the ACL2 definition of this function, see PF.

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.

To see the ACL2 definition of this function, see PF.

SYMBOL-LISTP    recognizer for a true list of symbols

The predicate symbol-listp tests whether its argument is a true list of
symbols.

To see the ACL2 definition of this function, see PF.

SYMBOL-NAME    the name of a symbol (a string)

Completion Axiom (completion-of-symbol-name):

     (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)

WARNING: While symbol-package-name behaves properly on all ACL2 objects,
it may give surprising results when called in raw Lisp.  More details
see PKG-IMPORTS, in particula the discussion there of the
"COMMON-LISP" package.

Completion Axiom (completion-of-symbol-package-name):

     (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!  We view a use of sys-call as a call to the operating
system that is made outside ACL2.  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 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.

To see the ACL2 definition of this function, see PF.

TENTH    tenth member of the list

See any Common Lisp documentation for details.

TERM-ORDER    the ordering relation on terms used by ACL2

ACL2 must occasionally choose which of two terms is syntactically
smaller.  The need for such a choice arises, for example, when using
equality hypotheses in conjectures (the smaller term is substituted for
the larger elsewhere in the formula), in stopping loops in permutative
rewrite rules (see LOOP-STOPPER), and in choosing the order in
which to try to cancel the addends in linear arithmetic inequalities.
When this notion of syntactic size is needed, ACL2 uses "term order."
Popularly speaking, term order is just a lexicographic ordering on
terms.  But the situation is actually more complicated.

We define term order only with respect to terms in translated form.
See TRANS.  Constants are viewed as built up by
_pseudo-function_ applications, as described at the end of this
documentation.

Term1 comes before term2 in the term order iff

     (a) the number of variable occurrences in term1 is less than that
     in term2, or

     (b) the numbers of variable occurrences in the two terms are equal
     but the number of function applications in term1 is less than that
     in term2, or

     (c) the numbers of variable occurrences in the two terms are
     equal, the numbers of functions applications in the two terms are
     equal, but pseudo-function application count for term1 is less
     than that for term2, or

     (d) the numbers of variable occurrences in the two terms are
     equal, the numbers of functions applications in the two terms are
     equal, the pseudo-function application counts for the two terms
     are equal, and term1 comes before term2 in a lexicographic
     ordering, lexorder, based their structure as Lisp objects: see
     LEXORDER.

The function term-order, when applied to the translations of two ACL2
terms, returns t iff the first is "less than or equal" to the second in
the term order.

By "number of variable occurrences" we do not mean "number of distinct
variables" but "number of times a variable symbol is mentioned."  (Cons
x x) has two variable occurrences, not one.  Thus, perhaps
counterintuitively, a large term that contains only one variable
occurrence, e.g., (standard-char-p (car (reverse x))) comes before
(cons x x) in the term order.

Since constants contain no variable occurrences and non-constant
expressions must contain at least one variable occurrence, constants
come before non-constants in the term order, no matter how large the
constants.  For example, the list constant

     '(monday tuesday wednesday thursday friday)

comes before x in the term order.  Because term order is involved in the
control of permutative rewrite rules and used to shift smaller terms to
the left, a set of permutative rules designed to allow the permutation
of any two tips in a tree representing the nested application of some
function will always move the constants into the left-most tips.  Thus,

     (+ x 3 (car (reverse klst)) (dx i j)) ,

which in translated form is

     (binary-+ x
               (binary-+ '3
                         (binary-+ (dx i j)
                                   (car (reverse klst))))),

will be permuted under the built-in commutativity rules to

     (binary-+ '3
               (binary-+ x
                         (binary-+ (car (reverse klst))
                                   (dx i j))))

or

     (+ 3 x (car (reverse klst)) (dx i j)).

Two terms with the same numbers of variable occurrences and function
applications and the same pseudo-function application count are ordered
by lexicographic means, based on their structures.  See
LEXORDER.  Thus, if two terms (member ...) and (reverse ...) contain
the same numbers of variable occurrences and function applications, and
no quoted constants, then the member term is first in the term order
because member comes before reverse in the term order (which is here
reduced to alphabetic ordering).

It remains to discuss the notion of _pseudo-function application count_.

Clearly, two constants are ordered using cases (c) and (d) of term
order, since they each contain 0 variable occurrences and no function
calls.  This raises the question "How many function applications are in
a constant?"  Because we regard the number of function applications as
a more fundamental measure of the size of a constant than lexicographic
considerations, we decided that for the purposes of term order,
constants would be seen as being built by primitive constructor
functions.  These constructor functions are not actually defined in
ACL2 but merely imagined for the purposes of term order.  We here use
suggestive names for these imagined functions, ignoring entirely the
prior use of these names within ACL2.  The imagined applications of
these functions are what we refer to as _pseudo-function_ applications.

The constant function z constructs 0.  Positive integers are
constructed from (z) by the successor function, s.  Thus 2 is (s (s
(z))) and contains three function applications.  100 contains one
hundred and one applications.  Negative integers are constructed from
their positive counterparts by -.  Thus, -2 is (- (s (s (z)))) and has
four applications.  Ratios are constructed by the dyadic function /.
Thus, -1/2 is

     (/ (- (s (z))) (s (s (z))))

and contains seven applications.  Complex rationals are similarly
constructed from rationals.  All character objects are considered
primitive and are constructed by constant functions of the same name.
Thus #\a and #\b both contain one application.  Strings are built from
the empty string, (o) by the "string-cons" function written cs.  Thus
"AB" is (cs (#\a) (cs (#\b) (o))) and contains five applications.
Symbols are obtained from strings by "packing" the symbol-name with the
unary function p.  Thus 'ab is

     (p (cs (#\a) (cs (#\b) (o))))

and has six applications.  Note that packages are here ignored and thus
'acl2::ab and 'my-package::ab each contain just six applications.
Finally, conses are built with cons, as usual.  So '(1 . 2) is (cons '1
'2) and contains six applications, since '1 contains two and '2
contains three.  This, for better or worse, answers the question "How
many function applications are in a constant?"

Finally, when we refer to the "pseudo-function application count", we
mean the number of pseudo-function applications as described above,
except that we bound this number by the constant
(fn-count-evg-max-val).  (This bound is important for efficiency, so
that constants that are very large cons structures do not cause
significant slowdown as ACL2 attempts to walk through them while
computing their pseudo-function application count.)

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 following remark is for those who verify guards for their functions
(see GUARD and see VERIFY-GUARDS).  We remark that a
call of (the TYPE EXPR) in the body of a function definition generates
a guard proof obligation that the type, TYPE, holds for the value of the
expression, EXPR.  Consider the following example.

     (defun f (x)
       (declare (xargs :guard (p1 x)))
       (if (p2 x)
           (the integer x)
         17))

The guard proof obligation generated for the THE expression above is as
follows.

     (implies (and (p1 x) (p2 x))
              (integerp x))

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.

TIME$    time an evaluation

Semantically, (time$ x ...) equals x.  However, its evaluation may
write timing output to the trace output (which is usually the
terminal), as explained further below.

     Examples:

     ; Basic examples:

     (time$ (foo 3 4))
     (time$ (mini-proveall))
     (defun bar (x) (time$ (f x)))

     ; Custom examples, which use a custom timing message rather than a built-in
     ; message from Lisp:

     ; Report only if real time is at least 1/2 second (two equivalent forms).
     (time$ (foo) :mintime 1/2)
     (time$ (foo) :real-mintime 1/2)

     ; Report only if allocation is at least 1000 bytes (and if the Lisp supports
     ; :minalloc).
     (time$ (foo) :minalloc 1000)

     ; Report only if real time is at least 1/2 second and (if the Lisp supports
     ; :minalloc) allocation is at least 931 bytes.
     (time$ (foo) :real-mintime 1/2 :minalloc 931)

     ; Print "Hello Moon, Goodbye World" instead of any timing data.
     (time$ (foo)
            :msg "Hello ~s0, ~s1 World."
            :args (list "Moon" "Goodbye"))

     ; Print default custom timing message (same as omitting :mintime 0):
     (time$ (foo)
            :mintime 0)

     ; Print supplied custom timing message.
     (let ((bar ...))
       (time$ (foo)
              :msg "The execution of ~xf took ~st seconds of real ~
                    time and ~sc seconds of run time (cpu time), and ~
                    allocated ~sa bytes.  In an unrelated note, bar ~
                    currently has the value ~x0.~%"
              :args (list bar)))

     General Forms:
     (time$ form)
     (time$ form ; arguments below are optional
            :real-mintime  <rational number of seconds>
            :run-mintime   <rational number of seconds>
            :minalloc      <number of bytes>
            :msg           <fmt string>
            :args          <list of arguments for msg>
            )
     ; Note: :real-mintime can be replaced by :mintime

where form is processed as usual except that the host Common Lisp times
its evaluation.

The simplest form is (time$ x), which will call the time utility in the
underlying Lisp, and will print a small default message.  If you want to
see a message printed by the host Lisp, use (time$ x :mintime nil)
instead, which may provide detailed, implementation-specific data such
as the amounts of time spent in user and system mode, the gc time, the
number of page faults encountered, and so on.  Of you can create a
custom message, configured using the :msg and :args parameters.  Time$
can also be made to report timing information only conditionally: the
:real-mintime (or equivalently, :mintime), :run-mintime, and :minalloc
arguments can be used to avoid reporting timing information for
computations that take a small amount of time (perhaps as might be
expected in ordinary cases), but to draw the user's attention to
computations that take longer or allocate more memory than expected.

We next document the keyword arguments in some detail.

     Keyword arguments :real-mintime (or :mintime) and :run-mintime can
     be used to specify a minimum time threshold for time reporting.
     That is, no timing information will be printed if the execution of
     form takes less than the specified number of seconds of real
     (total) time or run (cpu) time, respectively.  Note that rational
     numbers like 1/2 may be used to specify a fractional amount of
     seconds.  It is an error to specify both :real-mintime and its
     synonym, :mintime.

     Keyword argument :minalloc is not supported on all Lisps.  When it
     is not supported, it is ignored.  But on supported Lisps,
     :minalloc can be used to specify a minimum memory allocation
     threshold.  If form results in fewer than this many bytes being
     allocated, then no timing information will be reported.

     Keyword argument :msg, when provided, should be a string accepted
     by the fmt family of functions (see FMT), and it may refer
     to the elements of :args by their positions, just as for cw (see
     CW).

The following directives allow you to report timing information using
the :msg string.  The examples at the top of this documentation topic
illustrate the use of these directives.

     ~xf -- the form that was executed

     ~sa -- the amount of memory allocated, in bytes (in supported
     Lisps)

     ~st -- the real time taken, in seconds

     ~sc -- the run time (cpu time) taken, in seconds

We turn now to an example that illustrates how time$ can be called in
function bodies.  Consider the following definition of the Fibonacci
function, followed by the definition of a function that times k calls of
this function.

     (defun fib (n)
       (if (zp n)
           1
         (if (= n 1)
             1
           (+ (fib (- n 1))
              (fib (- n 2))))))

     (defun time-fib (k)
       (if (zp k)
           nil
         (prog2$
          (time$ (fib k)
                 :mintime 1/2
                 :msg "(fib ~x0) took ~st seconds, ~sa bytes allocated.~%"
                 :args (list k))
          (time-fib (1- k)))))

The following log shows a sample execution of the function defined just
above.

     ACL2 !>(time-fib 36)
     (fib 36) took 3.19 seconds, 1280 bytes allocated.
     (fib 35) took 1.97 seconds, 1280 bytes allocated.
     (fib 34) took 1.21 seconds, 1280 bytes allocated.
     (fib 33) took 0.75 seconds, 1280 bytes allocated.
     NIL
     ACL2 !>

Notes:

(1) Common Lisp specifies that the time utility prints to "trace
output", and time$ follows this convention.  Thus, if you have opened a
trace file (see OPEN-TRACE-FILE), then you can expect to find
the time$ output there.

(2) Unless the :msg argument is supplied, an explicit call of time$ in
the top-level loop will show that the form being timed is a call of the
ACL2 evaluator function ev-rec.  This is normal; the curious are
invited, at their own risk, to see RETURN-LAST for an
explanation.

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.

To see the ACL2 definition of this function, see PF.

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.

To see the ACL2 definition of this function, see PF.

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
     ACL2 !>(truncate 10/4 3/4)
     3

(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,  Also see
NONNEGATIVE-INTEGER-QUOTIENT, which is appropriate for integers
and may simplify reasoning, unless a suitable arithmetic library is
loaded, but be less efficient for evaluation on concrete objects.

To see the ACL2 definition of this function, see PF.

UNARY-    arithmetic negation function

Completion Axiom (completion-of-unary-minus):

     (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 (completion-of-unary-/):

     (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$    elements of one list that are not elements of another

     General Forms:
     (union$ l1 l2 ... lk)
     (union$ l1 l2 ... lk :test 'eql) ; same as above
     (union$ l1 l2 ... lk :test 'eq)    ; same, but eq is equality test
     (union$ l1 l2 ... lk :test 'equal) ; same, but equal is equality test

(Union$ x y) equals a list that contains both 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 optional keyword,
:TEST, has no effect logically, but provides the test (default eql)
used for comparing members of the two lists.

Union$ need not take exactly two arguments: (union$) is nil, (union$ x)
is x, (union$ x y z ... :test test) is (union$ x (union$ y z ... :test
test) :test test), and if :TEST is not supplied, then (union$ x y z
...) is (union$ x (union$ y z ...)).  For the discussion below we
restrict ourselves, then, to the cases (union$ x y) and (union$ x y
:test test).

The guard for a call of union$ (in the two cases just above) depends on
the test.  In all cases, both arguments must satisfy true-listp.  If
the test is eql, then one of the arguments must satisfy eqlable-listp.
If the test is eq, then one of the arguments must satisfy symbol-listp.

See EQUALITY-VARIANTS for a discussion of the relation between
union$ and its variants:

     (union-eq x lst) is equivalent to (union$ x lst :test 'eq);

     (union-equal x lst) is equivalent to (union$ x lst :test 'equal).

In particular, reasoning about any of these primitives reduces to
reasoning about the function union-equal.

Note that union-eq can take any number of arguments, in analogy to
union$; indeed, (union-eq ...) expands to (union$ ... :test 'eq).
However, union-equal is a function, not a macro, and takes exactly two
arguments.

Union$ is similar to the Common Lisp primitive union.  However, Common
Lisp does not specify the order of elements in the result of a call of
union.

UNION-EQ    See UNION$.

UNION-EQUAL    See UNION$.

UNTRANSLATE    See USER-DEFINED-FUNCTIONS-TABLE.

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.

To see the ACL2 definition of this function, see PF.

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.

To see the ACL2 definition of this function, see PF.

WITH-LIVE-STATE    allow a reference to state in raw Lisp

The macro with-live-state is an advanced feature that very few users
will need (basically, only system hackers).  Indeed, it is untouchable;
see REMOVE-UNTOUCHABLE for how to enable calling
with-live-state in the ACL2 loop.

     Example Form:
     (with-live-state (assign y 3))

     General form:
     (with-live-state form)

where form is an arbitrary form with a free reference to the variable
state.

Logically, (with-live-state FORM) macroexpands to FORM.  However, in
raw Lisp it expands to:

     (let ((state *the-live-state*))
       FORM)

If a form that mentions the variable state might be executed in raw
Lisp -- that is, either outside the ACL2 loop or in raw mode (see
SET-RAW-MODE) -- then the surrounding the form with with-live-state
as shown above can avoid potential warnings or (much less likely)
errors.  Note however that if state is lexically bound to a state other
than the usual "live" state, surprising behavior may occur when
evaluating a call of with-live-state in raw Lisp or raw mode (either
directly by evaluation or at compile time), because with-live-state will
override that lexical binding of state by a lexical binding of state to
the usual "live" state.

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).

To see the ACL2 definition of this function, see PF.

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.

To see the ACL2 definition of this function, see PF.

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.

To see the ACL2 definition of this function, see PF.

ACL2-USER    a package the ACL2 user may prefer

This package imports the standard Common Lisp symbols that ACL2
supports and also a few symbols from package "ACL2" that are commonly
used when interacting with ACL2.  You may prefer to select this as your
current package so as to avoid colliding with ACL2 system names.

This package imports the symbols listed in
*common-lisp-symbols-from-main-lisp-package*, which contains hundreds
of CLTL function and macro names including those supported by ACL2 such
as cons, car, and cdr.  It also imports the symbols in *acl2-exports*,
which contains a few symbols that are frequently used while interacting
with the ACL2 system, such as implies, defthm, and rewrite.  It imports
nothing else.

Thus, names such as alistp, member-equal, and type-set, which are
defined in the "ACL2" package are not present here.  If you find
yourself frequently colliding with names that are defined in "ACL2" you
might consider selecting "ACL2-USER" as your current package (see
IN-PACKAGE).  If you select "ACL2-USER" as the current package, you
may then simply type member-equal to refer to acl2-user::member-equal,
which you may define as you see fit.  Of course, should you desire to
refer to the "ACL2" version of member-equal, you will have to use the
"ACL2::" prefix, e.g., acl2::member-equal.

If, while using "ACL2-USER" as the current package, you find that there
are symbols from "ACL2" that you wish we had imported into it (because
they are frequently used in interaction), please bring those symbols to
our attention.  For example, should union-theories and universal-theory
be imported?  Except for stabilizing on the "frequently used" names
from "ACL2", we intend never to define a symbol whose
symbol-package-name is "ACL2-USER".

ARRAYS    an introduction to ACL2 arrays

Below we begin a detailed presentation of ACL2 arrays.  ACL2's
single-threaded objects (see STOBJ) provide a similar
functionality that is generally more efficient when there are updates
(writes), but is also more restrictive.

See ARRAYS-EXAMPLE for a brief introduction illustrating the use
of ACL2 arrays.

ACL2 provides relatively efficient 1- and 2-dimensional arrays.  Arrays
are awkward to provide efficiently in an applicative language because
the programmer rightly expects to be able to "modify" an array object
with the effect of changing the behavior of the element accessing
function on that object.  This, of course, does not make any sense in
an applicative setting.  The element accessing function is, after all,
a function, and its behavior on a given object is immutable.  To
"modify" an array object in an applicative setting we must actually
produce a new array object.  Arranging for this to be done efficiently
is a challenge to the implementors of the language.  In addition, the
programmer accustomed to the von Neumann view of arrays must learn how
to use immutable applicative arrays efficiently.

In this note we explain 1-dimensional arrays.  In particular, we
explain briefly how to create, access, and "modify" them, how they are
implemented, and how to program with them.  2-dimensional arrays are
dealt with by analogy.

_The Logical Description of ACL2 Arrays_

An ACL2 1-dimensional array is an object that associates arbitrary
objects with certain integers, called "indices." Every array has a
dimension, dim, which is a positive integer.  The indices of an array
are the consecutive integers from 0 through dim-1.  To obtain the
object associated with the index i in an array a, one uses (aref1 name
a i).  Name is a symbol that is irrelevant to the semantics of aref1
but affects the speed with which it computes.  We will talk more about
array "names" later.  To produce a new array object that is like a but
which associates val with index i, one uses (aset1 name a i val).

An ACL2 1-dimensional array is actually an alist.  There is no special
ACL2 function for creating arrays; they are generally built with the
standard list processing functions list and cons.  However, there is a
special ACL2 function, called compress1, for speeding up access to the
elements of such an alist.  We discuss compress1 later.

One element of the alist must be the "header" of the array.  The header
of a 1-dimensional array with dimension dim is of the form:

     (:HEADER :DIMENSIONS (dim)
              :MAXIMUM-LENGTH max
              :DEFAULT obj ; optional
              :NAME name   ; optional
              :ORDER order ; optional values are < (the default), >, or :none/nil
              ).

Obj may be any object and is called the "default value" of the array.
Max must be an integer greater than dim.  Name must be a symbol.  The
:default and :name entries are optional; if :default is omitted, the
default value is nil.  The function header, when given a name and a 1-
or 2-dimensional array, returns the header of the array.  The functions
dimensions, maximum-length, and default are similar and return the
corresponding fields of the header of the array.  The role of the
:dimensions field is obvious: it specifies the legal indices into the
array.  The roles played by the :maximum-length and :default fields are
described below.

Aside from the header, the other elements of the alist must each be of
the form (i . val), where i is an integer and 0 <= i < dim, and val is
an arbitrary object.

The :order field of the header is ignored for 2-dimensional arrays.  For
1-dimensional arrays, it specifies the order of keys (i, above) when the
array is compressed as with compress1, as described below.  An :order
of :none or nil specifies no reordering of the alist by compress1, and
an order of > specifies reordering by compress1 so that keys are in
descending order.  Otherwise, the alist is reordered by compress1 so
that keys are in ascending order.

(Aref1 name a i) is guarded so that name must be a symbol, a must be an
array and i must be an index into a.  The value of (aref1 name a i) is
either (cdr (assoc i a)) or else is the default value of a, depending
on whether there is a pair in a whose car is i.  Note that name is
irrelevant to the value of an aref1 expression.  You might :pe aref1 to
see how simple the definition is.

(Aset1 name a i val) is guarded analogously to the aref1 expression.
The value of the aset1 expression is essentially (cons (cons i val) a).
Again, name is irrelevant.  Note (aset1 name a i val) is an array, a',
with the property that (aref1 name a' i) is val and, except for index
i, all other indices into a' produce the same value as in a.  Note also
that if a is viewed as an alist (which it is) the pair "binding" i to
its old value is in a' but "covered up" by the new pair.  Thus, the
length of an array grows by one when aset1 is done.

Because aset1 covers old values with new ones, an array produced by a
sequence of aset1 calls may have many irrelevant pairs in it.  The
function compress1 can remove these irrelevant pairs.  Thus, (compress1
name a) returns an array that is equivalent (vis-a-vis aref1) to a but
which may be shorter.  For technical reasons, the alist returned by
compress1 may also list the pairs in a different order than listed in a.

To prevent arrays from growing excessively long due to repeated aset1
operations, aset1 actually calls compress1 on the new alist whenever
the length of the new alist exceeds the :maximum-length entry, max, in
the header of the array.  See the definition of aset1 (for example by
using :pe).  This is primarily just a mechanism for freeing up cons
space consumed while doing aset1 operations.  Note however that this
compress1 call is replaced by a hard error if the header specifies an
:order of :none or nil.

This completes the logical description of 1-dimensional arrays.
2-dimensional arrays are analogous.  The :dimensions entry of the
header of a 2-dimensional array should be (dim1 dim2).  A pair of
indices, i and j, is legal iff 0 <= i < dim1 and 0 <= j < dim2.  The
:maximum-length must be greater than dim1*dim2.  Aref2, aset2, and
compress2 are like their counterparts but take an additional index
argument.  Finally, the pairs in a 2-dimensional array are of the form
((i . j) . val).

_The Implementation of ACL2 Arrays_

Very informally speaking, the function compress1 "creates" an ACL2
array that provides fast access, while the function aref1 "maintains"
fast access.  We now describe this informal idea more carefully.

Aref1 is essentially assoc.  If aref1 were implemented naively the time
taken to access an array element would be linear in the dimension of
the array and the number of "assignments" to it (the number of aset1
calls done to create the array from the initial alist).  This is
intolerable; arrays are "supposed" to provide constant-time access and
change.

The apparently irrelevant names associated with ACL2 arrays allow us to
provide constant-time access and change when arrays are used in
"conventional" ways.  The implementation of arrays makes it clear what
we mean by "conventional."

Recall that array names are symbols.  Behind the scenes, ACL2
associates two objects with each ACL2 array name.  The first object is
called the "semantic value" of the name and is an alist.  The second
object is called the "raw lisp array" and is a Common Lisp array.

When (compress1 name alist) builds a new alist, a', it sets the
semantic value of name to that new alist.  Furthermore, it creates a
Common Lisp array and writes into it all of the index/value pairs of
a', initializing unassigned indices with the default value.  This array
becomes the raw lisp array of name.  Compress1 then returns a', the
semantic value, as its result, as required by the definition of
compress1.

When (aref1 name a i) is invoked, aref1 first determines whether the
semantic value of name is a (i.e., is eq to the alist a).  If so, aref1
can determine the ith element of a by invoking Common Lisp's aref
function on the raw lisp array associated with name.  Note that no
linear search of the alist a is required; the operation is done in
constant time and involves retrieval of two global variables, an eq
test and jump, and a raw lisp array access.  In fact, an ACL2 array
access of this sort is about 5 times slower than a C array access.  On
the other hand, if name has no semantic value or if it is different
from a, then aref1 determines the answer by linear search of a as
suggested by the assoc-like definition of aref1.  Thus, aref1 always
returns the axiomatically specified result.  It returns in constant
time if the array being accessed is the current semantic value of the
name used.  The ramifications of this are discussed after we deal with
aset1.

When (aset1 name a i val) is invoked, aset1 does two conses to create
the new array.  Call that array a'.  It will be returned as the answer.
(In this discussion we ignore the case in which aset1 does a
compress1.)  However, before returning, aset1 determines if name's
semantic value is a.  If so, it makes the new semantic value of name be
a' and it smashes the raw lisp array of name with val at index i,
before returning a' as the result.  Thus, after doing an aset1 and
obtaining a new semantic value a', all aref1s on that new array will be
fast.  Any aref1s on the old semantic value, a, will be slow.

To understand the performance implications of this design, consider the
chronological sequence in which ACL2 (Common Lisp) evaluates
expressions:  basically inner-most first, left-to-right, call-by-value.
An array use, such as (aref1 name a i), is "fast" (constant-time) if
the alist supplied, a, is the value returned by the most recently
executed compress1 or aset1 on the name supplied.  In the functional
expression of "conventional" array processing, all uses of an array are
fast.

The :name field of the header of an array is completely irrelevant.
Our convention is to store in that field the symbol we mean to use as
the name of the raw lisp array.  But no ACL2 function inspects :name
and its primary value is that it allows the user, by inspecting the
semantic value of the array -- the alist -- to recall the name of the
raw array that probably holds that value.  We say "probably" since
there is no enforcement that the alist was compressed under the name in
the header or that all asets used that name.  Such enforcement would be
inefficient.

_Some Programming Examples_

In the following examples we will use ACL2 "global variables" to hold
several arrays.  See @, and see ASSIGN.

Let the state global variable a be the 1-dimensional compressed array
of dimension 5 constructed below.

     ACL2 !>(assign a (compress1 'demo
                                 '((:header :dimensions (5)
                                            :maximum-length 15
                                            :default uninitialized
                                            :name demo)
                                   (0 . zero))))

Then (aref1 'demo (@ a) 0) is zero and (aref1 'demo (@ a) 1) is
uninitialized.

Now execute

     ACL2 !>(assign b (aset1 'demo (@ a) 1 'one))

Then (aref1 'demo (@ b) 0) is zero and (aref1 'demo (@ b) 1) is one.

All of the aref1s done so far have been "fast."

Note that we now have two array objects, one in the global variable a
and one in the global variable b.  B was obtained by assigning to a.
That assignment does not affect the alist a because this is an
applicative language.  Thus, (aref1 'demo (@ a) 1) must *still* be
uninitialized.  And if you execute that expression in ACL2 you will see
that indeed it is.  However, a rather ugly comment is printed, namely
that this array access is "slow."  The reason it is slow is that the
raw lisp array associated with the name demo is the array we are
calling b.  To access the elements of a, aref1 must now do a linear
search.  Any reference to a as an array is now "unconventional;" in a
conventional language like Ada or Common Lisp it would simply be
impossible to refer to the value of the array before the assignment
that produced our b.

Now let us define a function that counts how many times a given object,
x, occurs in an array.  For simplicity, we will pass in the name and
highest index of the array:

     ACL2 !>(defun cnt (name a i x)
              (declare (xargs :guard
                              (and (array1p name a)
                                   (integerp i)
                                   (>= i -1)
                                   (< i (car (dimensions name a))))
                              :mode :logic
                              :measure (nfix (+ 1 i))))
              (cond ((zp (1+ i)) 0) ; return 0 if i is at most -1
                    ((equal x (aref1 name a i))
                     (1+ (cnt name a (1- i) x)))
                    (t (cnt name a (1- i) x))))

To determine how many times zero appears in (@ b) we can execute:

     ACL2 !>(cnt 'demo (@ b) 4 'zero)

The answer is 1.  How many times does uninitialized appear in (@ b)?

     ACL2 !>(cnt 'demo (@ b) 4 'uninitialized)

The answer is 3, because positions 2, 3 and 4 of the array contain that
default value.

Now imagine that we want to assign 'two to index 2 and then count how
many times the 2nd element of the array occurs in the array.  This
specification is actually ambiguous.  In assigning to b we produce a
new array, which we might call c.  Do we mean to count the occurrences
in c of the 2nd element of b or the 2nd element of c?  That is, do we
count the occurrences of uninitialized or the occurrences of two?  If
we mean the former the correct answer is 2 (positions 3 and 4 are
uninitialized in c); if we mean the latter, the correct answer is 1
(there is only one occurrence of two in c).

Below are ACL2 renderings of the two meanings, which we call [former]
and [latter].  (Warning:  Our description of these examples, and of an
example [fast former] that follows, assumes that only one of these
three examples is actually executed; for example, they are not executed
in sequence.  See "A Word of Warning" below for more about this issue.)

     (cnt 'demo (aset1 'demo (@ b) 2 'two) 4 (aref1 'demo (@ b) 2))  ; [former]

     (let ((c (aset1 'demo (@ b) 2 'two)))                           ; [latter]
       (cnt 'demo c 4 (aref1 'demo c 2)))

Note that in [former] we create c in the second argument of the call to
cnt (although we do not give it a name) and then refer to b in the
fourth argument.  This is unconventional because the second reference
to b in [former] is no longer the semantic value of demo.  While ACL2
computes the correct answer, namely 2, the execution of the aref1
expression in [former] is done slowly.

A conventional rendering with the same meaning is

     (let ((x (aref1 'demo (@ b) 2)))                           ; [fast former]
       (cnt 'demo (aset1 'demo (@ b) 2 'two) 4 x))

which fetches the 2nd element of b before creating c by assignment.  It
is important to understand that [former] and [fast former] mean exactly
the same thing: both count the number of occurrences of uninitialized
in c.  Both are legal ACL2 and both compute the same answer, 2.
Indeed, we can symbolically transform [fast former] into [former]
merely by substituting the binding of x for x in the body of the let.
But [fast former] can be evaluated faster than [former] because all of
the references to demo use the then-current semantic value of demo,
which is b in the first line and c throughout the execution of the cnt
in the second line.  [Fast former] is the preferred form, both because
of its execution speed and its clarity.  If you were writing in a
conventional language you would have to write something like [fast
former] because there is no way to refer to the 2nd element of the old
value of b after smashing b unless it had been saved first.

We turn now to [latter].  It is both clear and efficient.  It creates c
by assignment to b and then it fetches the 2nd element of c, two, and
proceeds to count the number of occurrences in c.  The answer is 1.
[Latter] is a good example of typical ACL2 array manipulation: after
the assignment to b that creates c, c is used throughout.

It takes a while to get used to this because most of us have grown
accustomed to the peculiar semantics of arrays in conventional
languages.  For example, in raw lisp we might have written something
like the following, treating b as a "global variable":

     (cnt 'demo (aset 'demo b 2 'two) 4 (aref 'demo b 2))

which sort of resembles [former] but actually has the semantics of
[latter] because the b from which aref fetches the 2nd element is not
the same b used in the aset!  The array b is destroyed by the aset and
b henceforth refers to the array produced by the aset, as written more
clearly in [latter].

A Word of Warning:  Users must exercise care when experimenting with
[former], [latter] and [fast former].  Suppose you have just created b
with the assignment shown above,

     ACL2 !>(assign b (aset1 'demo (@ a) 1 'one))

If you then evaluate [former] in ACL2 it will complain that the aref1
is slow and compute the answer, as discussed.  Then suppose you
evaluate [latter] in ACL2.  From our discussion you might expect it to
execute fast -- i.e., issue no complaint.  But in fact you will find
that it complains repeatedly.  The problem is that the evaluation of
[former] changed the semantic value of demo so that it is no longer b.
To try the experiment correctly you must make b be the semantic value
of demo again before the next example is evaluated.  One way to do that
is to execute

     ACL2 !>(assign b (compress1 'demo (@ b)))

before each expression.  Because of issues like this it is often hard
to experiment with ACL2 arrays at the top-level.  We find it easier to
write functions that use arrays correctly and efficiently than to so
use them interactively.

This last assignment also illustrates a very common use of compress1.
While it was introduced as a means of removing irrelevant pairs from an
array built up by repeated assignments, it is actually most useful as a
way of insuring fast access to the elements of an array.

Many array processing tasks can be divided into two parts.  During the
first part the array is built.  During the second part the array is
used extensively but not modified.  If your programming task can be so
divided, it might be appropriate to construct the array entirely with
list processing, thereby saving the cost of maintaining the semantic
value of the name while few references are being made.  Once the alist
has stabilized, it might be worthwhile to treat it as an array by
calling compress1, thereby gaining constant time access to it.

ACL2's theorem prover uses this technique in connection with its
implementation of the notion of whether a rune is disabled or not.
Associated with every rune is a unique integer index, called its
"nume."  When each rule is stored, the corresponding nume is stored as
a component of the rule.  Theories are lists of runes and membership in
the "current theory" indicates that the corresponding rule is enabled.
But these lists are very long and membership is a linear-time
operation.  So just before a proof begins we map the list of runes in
the current theory into an alist that pairs the corresponding numes
with t.  Then we compress this alist into an array.  Thus, given a rule
we can obtain its nume (because it is a component) and then determine
in constant time whether it is enabled.  The array is never modified
during the proof, i.e., aset1 is never used in this example.  From the
logical perspective this code looks quite odd:  we have replaced a
linear-time membership test with an apparently linear-time assoc after
going to the trouble of mapping from a list of runes to an alist of
numes.  But because the alist of numes is an array, the "apparently
linear-time assoc" is more apparent than real; the operation is
constant-time.