This is documentation for ACL2 Version 3.0
Copyright (C) 2006  University of Texas at Austin

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

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

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

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

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.

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

LEXORDER    total order on ACL2 objects

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

Lexorder has a guard of t.

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

LIST    build a list

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

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

LIST*    build a list

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

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

LISTP    recognizer for (not necessarily proper) lists

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

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

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

LOGAND    bitwise logical `and' of zero or more integers

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

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

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

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

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

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

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

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

LOGBITP    the ith bit of an integer

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

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

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

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

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

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

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

LOGEQV    bitwise logical equivalence of zero or more integers

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

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

LOGIOR    bitwise logical inclusive or of zero or more integers

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

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

LOGNAND    bitwise logical `nand' of two integers

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

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

LOGNOR    bitwise logical `nor' of two integers

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

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

LOGNOT    bitwise not of a two's complement number

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

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

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

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

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

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

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

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

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

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

LOGTEST    test if two integers share a `1' bit

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

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

LOGXOR    bitwise logical exclusive or of zero or more integers

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

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

LOWER-CASE-P    recognizer for lower case characters

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

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

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

MAKE-CHARACTER-LIST    coerce to a list of characters

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

MAKE-LIST    make a list of a given size

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

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

MAKE-ORD    a constructor for ordinals.

Make-ord is the ordinal constructor.  Its use is recommended instead of
using cons to make ordinals.

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

     (make-ord 1 1 0)

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

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

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

MAX    the larger of two numbers

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

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

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

MBE    attach code for execution

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

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

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

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

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, and generation of constraints for functional instantiation also
treat the above mbe call as if were replaced by logic-code.

MBT    introduce a test not to be evaluated

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

     (verify-guards recurX2)

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

MEMBER    membership predicate, using eql as test

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

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

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

MEMBER-EQ    membership predicate, using eq as test

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

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

MEMBER-EQUAL    membership predicate

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

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

MIN    the smaller of two numbers

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

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

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

MINUSP    test whether a number is negative

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

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

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

MOD    remainder using floor

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

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

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

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

MUST-BE-EQUAL    attach code for execution

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

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

MV    returning a multiple value

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

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

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

MV-LET    calling multi-valued ACL2 functions

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

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

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

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

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

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

     (defun count-and-collect (x)

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

       (cond ((atom x)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

NATP    a recognizer for the natural numbers

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

NFIX    coerce to a natural number

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

Nfix has a guard of t.

NINTH    ninth member of the list

See any Common Lisp documentation for details.

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

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

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

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

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

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

NONNEGATIVE-INTEGER-QUOTIENT    natural number division function

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

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

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

NOT    logical negation

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

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

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

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

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

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

NTHCDR    final segment of a list

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

The following is a theorem.

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

For related functions, see TAKE and see BUTLAST.

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

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

NULL    recognizer for the empty list

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

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

NUMERATOR    dividend of a ratio in lowest terms

Completion Axiom:

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

Guard for (numerator x):

     (rationalp x)

O-FINP    recognizes if an ordinal is finite

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

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

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

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

O-FIRST-EXPT    the first exponent of an ordinal

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

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

O-INFP    recognizes if an ordinal is infinite

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

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

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

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

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

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

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

     w             |||||...,

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

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

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

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

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

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

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

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

            .
           .
          .
         w
        w
       w
      w
     w

That is epsilon-0.

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

       ordinal            ACL2 representation

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

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

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

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

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

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

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

       ...                ...

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

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

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

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

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

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

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

O-RST    returns the rest of an infinite ordinal

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

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

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

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

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

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

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

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

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

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

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

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

O>    the greater-than relation for the ordinals

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

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

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

ODDP    test whether an integer is odd

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

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

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

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.

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.

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) evaluates to a symbol in that package whose
symbol-name is the value of constant *pkg-witness-name*.

(Pkg-witness pkg) has a guard of (stringp pkg).  However, if pkg-witness
is called on an argument that is not the name of a package known to
ACL2, a hard Lisp error will result.