This is documentation for ACL2 Version 3.4
Copyright (C) 2008  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.

MEMBER-EQUAL    membership predicate

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

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

MIN    the smaller of two numbers

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

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

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

MINUSP    test whether a number is negative

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

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

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

MOD    remainder using floor

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

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

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

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

MOD-EXPT    exponential function

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

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

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

MUST-BE-EQUAL    attach code for execution

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

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

MV    returning a multiple value

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

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

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

MV-LET    calling multi-valued ACL2 functions

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

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

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

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

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

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

     (defun count-and-collect (x)

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

       (cond ((atom x)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

NATP    a recognizer for the natural numbers

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

NFIX    coerce to a natural number

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

Nfix has a guard of t.

NINTH    ninth member of the list

See any Common Lisp documentation for details.

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

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

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

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

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

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

NONNEGATIVE-INTEGER-QUOTIENT    natural number division function

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

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

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

NOT    logical negation

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

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

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

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

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

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

NTHCDR    final segment of a list

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

The following is a theorem.

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

For related functions, see TAKE and see BUTLAST.

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

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

NULL    recognizer for the empty list

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

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

NUMERATOR    dividend of a ratio in lowest terms

Completion Axiom:

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

Guard for (numerator x):

     (rationalp x)

O-FINP    recognizes if an ordinal is finite

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

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

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

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

O-FIRST-EXPT    the first exponent of an ordinal

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

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

O-INFP    recognizes if an ordinal is infinite

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

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

Using the nonnegative integers and lists we can represent the ordinals
up to epsilon-0. The ordinal representation used in ACL2 has changed as
of Version_2.8 from that of Nqthm-1992, courtesy of Pete 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.

OPEN-INPUT-CHANNEL    See IO.

OPEN-INPUT-CHANNEL-P    See IO.

OPEN-OUTPUT-CHANNEL    See IO.

OPEN-OUTPUT-CHANNEL-P    See IO.

OPTIMIZE    See DECLARE.

OR    disjunction

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

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

PAIRLIS    See PAIRLIS$

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

PAIRLIS$    zipper together two lists

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

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

PEEK-CHAR$    See IO.

PKG-WITNESS    return a specific symbol in the indicated package

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

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

PLUSP    test whether a number is positive

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

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

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

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

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

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

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

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

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

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

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

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

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

POSP    a recognizer for the positive integers

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

PPROGN    evaluate a sequence of forms that return state

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

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

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

General Form:

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

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

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

PRINT-OBJECT$    See IO.

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

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

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

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

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

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

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

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

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

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

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

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

PROOFS-CO    the proofs character output channel

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

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

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

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

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

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

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

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

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

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

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

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

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

PUTPROP    update fast property lists

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

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

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

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

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

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

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

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

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

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

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

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

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

RATIONAL-LISTP    recognizer for a true list of rational numbers

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

RATIONALP    recognizer for rational numbers (ratios and integers)

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

READ-BYTE$    See IO.

READ-CHAR$    See IO.

READ-OBJECT    See IO.

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

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

REALFIX    coerce to a real number

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

Realfix has a guard of t.

REALPART    real part of a complex number

Completion Axiom:

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

Guard for (realpart x):

     (acl2-numberp x)