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.

REDEFINING-PROGRAMS    an explanation of why we restrict redefinitions

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

REM    remainder using truncate

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

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

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

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

REMOVE    remove all occurrences, testing using eql

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

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

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

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

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

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

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

is equal to '(1 3 2 4).

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

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

REMOVE-DUPLICATES-EQUAL    remove duplicates from a list

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

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

REMOVE-EQ    remove all occurrences, testing using eq

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

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

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

REMOVE-EQUAL    remove all occurrences, testing using equal

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

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

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

REMOVE1    remove first occurrences, testing using eql

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

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

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

REMOVE1-EQ    remove first occurrences, testing using eq

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

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

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

REMOVE1-EQUAL    remove first occurrences, testing using equal

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

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

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

REST    rest (cdr) of the list

In the logic, rest is just a macro for cdr.

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

REVAPPEND    concatentate the reverse of one list to another

(Revappend x y) concatenates the reverse of the list x to y, which is
also typically a list.

The following theorem characterizes this English description.

     (equal (revappend x y)
            (append (reverse x) y))

Hint:  This lemma follows immediately from the definition of reverse
and the following lemma.

     (defthm revappend-append
       (equal (append (revappend x y) z)
              (revappend x (append y z))))

The guard for (revappend x y) requires that x is a true list.

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

REVERSE    reverse a list or string

(Reverse x) is the result of reversing the order of the elements of the
list or string x.

The guard for reverse requires that its argument is a true list or a
string.

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

RFIX    coerce to a rational number

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

Rfix has a guard of t.

ROUND    division returning an integer by rounding off

     Example Forms:
     ACL2 !>(round 14 3)
     5
     ACL2 !>(round -14 3)
     -5
     ACL2 !>(round 14 -3)
     -5
     ACL2 !>(round -14 -3)
     5
     ACL2 !>(round 13 3)
     4
     ACL2 !>(round -13 3)
     -4
     ACL2 !>(round 13 -3)
     -4
     ACL2 !>(round -13 -3)
     4
     ACL2 !>(round -15 -3)
     5
     ACL2 !>(round 15 -2)
     -8

(Round i j) is the result of taking the quotient of i and j and
rounding off to the nearest integer.  When the quotient is exactly
halfway between consecutive integers, it rounds to the even one.

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

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

SEARCH    search for a string or list in another string or list

     Example Forms:
     (search "cd" "Cdabcdefcde")                   ; = 4, index of first match
     (search "cd" "Cdabcdefcde" :test 'equal)      ; same as above
     (search "cd" "Cdabcdefcde" :from-end t)       ; = 8, index of last match
     (search "cd" "Cdabcdefcde" :start1 1)         ; = 1
     (search "cd" "Cdabcdefcde" :start2 5)         ; = 8
     (search "cd" "Cdabcdefcde" :test 'char-equal) ; = 0 (case-insensitive)
     (search "ac" "Cdabcdefcde")                   ; = nil
     (search '(a b) '(9 8 a b 7 6))                    ; = 2

     General Form:
     (search seq1 seq2 &key from-end test start1 start2 end1 end2)

Search indicates whether one string or list occurs as a (contiguous)
subsequence of another string or list, respectively.  It returns nil if
no such match is found; otherwise it returns the (zero-based) index of
the first match by default, but a non-nil value of keyword argument
:from-end causes it to return the last match.  The :test is equal by
default.  The other legal value for :test is char-equal, which can be
given only for two strings, in which case the match is case-insensitive.
Finally, values of :start1 and :end1 for the first sequence, and of
:start2 and [:end2] for the second sequence, bound the portion of the
respective sequence used for deciding on a match, though the index
returned is always an index into the second sequence as a whole.

The guard for calls of search is given by a function, search-fn-guard,
which has the following requirements.

     o The two arguments much both satisfy true-listp or else must both
     be strings consisting of standard characters (see
     STANDARD-CHAR-P).

     o The :test must evaluate to one of the symbols equal or
     char-equal, where the latter is only allowed if the (first) two
     arguments are strings.

     o The values of :start1, :start2, :end1, and :end2 must all be
     natural numbers, where if omitted they default to 0, 0, the length
     len1 of the first argument, and the length len2 of the second
     argument, respectively.

     o If start1 is the value of :start1, defaulting as described just
     above, and similarly for the other start and end keywords and for
     lengths len1 and len2 as described just above, then: start1 <=
     end1 <= len1 and start2 <= end2 <= len2.

Search is a Common Lisp function (actually, a macro in ACL2).  See any
Common Lisp documentation for more information.

SECOND    second member of the list

See any Common Lisp documentation for details.

SET-DIFFERENCE-EQ    elements of one list that are not elements of another

(Set-difference-eq x y) is logically equivalent to
set-difference-equal, except that the guard requires not only that the
two arguments are true-listps but also that at least one is a
symbol-listp.  Also see SET-DIFFERENCE-EQUAL.

SET-DIFFERENCE-EQUAL    elements of one list that are not elements of another

(Set-difference-equal x y) equals a list whose members (see
MEMBER-EQUAL) contains the members of x that are not members of y.
More precisely, the resulting list is the same as one gets by deleting
the members of y from x, leaving the remaining elements in the same
order as they had in x.

The guard for set-difference-equal requires both arguments to be true
lists.  Essentially, set-difference-equal has the same functionality as
the Common Lisp function set-difference, except that it uses the equal
function to test membership rather than eql.  However, we do not
include the function set-difference in ACL2, because the Common Lisp
language does not specify the order of the elements in the list that it
returns.

Also see SET-DIFFERENCE-EQ for a semantically equivalent
function that executes more efficiently on lists of symbols.

SETENV$    set an environment variable

(Setenv$ str val), where str and val are strings, sets the environment
variable str to have value val, for subsequent read by getenv$ (see
GETENV$), and returns nil.  Or, if this operation is not
implemented for the host Common Lisp, an error will occur.

     Example:
     (setenv$ "FOO" "BAR")

SEVENTH    seventh member of the list

See any Common Lisp documentation for details.

SIGNUM    indicator for positive, negative, or zero

(Signum x) is 0 if x is 0, -1 if x is negative, and is 1 otherwise.

The guard for signum requires its argument to be rational (real, in
ACL2(r)) number.

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

From "Common Lisp the Language" page 206, we see a definition of signum
in terms of abs.  As explained elsewhere (see ABS), the guard
for abs requires its argument to be a rational (real, in ACL2(r))
number; hence, we make the same restriction for signum.

SIXTH    sixth member of the list

See any Common Lisp documentation for details.

STANDARD-CHAR-LISTP    recognizer for a true list of standard characters

(standard-char-listp x) is true if and only if x is a null-terminated
list all of whose members are standard characters.  See
STANDARD-CHAR-P.

Standard-char-listp has a guard of t.

STANDARD-CHAR-P    recognizer for standard characters

(Standard-char-p x) is true if and only if x is a "standard" character,
i.e., a member of the list *standard-chars*.  This list includes
#Newline and #Space characters, as well as the usual punctuation and
alphanumeric characters.

Standard-char-p has a guard requiring its argument to be a character.

Standard-char-p is a Common Lisp function.  See any Common Lisp
documentation for more information.

STANDARD-CO    the character output channel to which ld prints

Standard-co is an ld special (see LD).  The accessor is
(standard-co state) and the updater is (set-standard-co val state).
Standard-co must be an open character output channel.  It is to this
channel that ld prints the prompt, the form to be evaluated, and the
results.  The event commands such as defun, defthm, etc., which print
extensive commentary do not print to standard-co but rather to a
different channel, proofs-co, so that you may redirect this commentary
while still interacting via standard-co.  See PROOFS-CO.

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

STANDARD-OI    the standard object input ``channel''

Standard-oi is an ld special (see LD).  The accessor is
(standard-oi state) and the updater is (set-standard-oi val state).
Standard-oi must be an open object input channel, a true list of
objects, or a list of objects whose last cdr is an open object input
channel.  It is from this source that ld takes the input forms to
process.  When ld is called, if the value specified for standard-oi is
a string or a list of objects whose last cdr is a string, then ld
treats the string as a file name and opens an object input channel from
that file, where the connected book directory (see CBD) is used
to resolve relative pathnames.  The channel opened by ld is closed by
ld upon termination.

"Standard-oi" stands for "standard object input." The read-eval-print
loop in ld reads the objects in standard-oi and treats them as forms to
be evaluated.  The initial value of standard-oi is the same as the
value of *standard-oi* (see *STANDARD-OI*).

STANDARD-STRING-ALISTP    recognizer for association lists with standard strings as keys

(Standard-string-alistp x) is true if and only if x is a list of pairs
of the form (cons key val) where key is a string all of whose
characters are standard (see STANDARD-CHAR-P).

Standard-string-alistp has a guard of t.

STRING    coerce to a string

(String x) coerces x to a string.  If x is already a string, then it is
returned unchanged; if x is a symbol, then its symbol-name is returned;
and if x is a character, the corresponding one-character string is
returned.

The guard for string requires its argument to be a string, a symbol, or
a character.

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

STRING-APPEND    concatenate two strings

NOTE:  It is probably more efficient to use the Common Lisp function
concatenate in place of string-append.  That is,

     (string-append str1 str2)

is equal to

     (concatenate 'string str1 str2).

At any rate, string-append takes two arguments, which are both strings
(if the guard is to be met), and returns a string obtained
concatenating together the characters in the first string followed by
those in the second.  See CONCATENATE.

STRING-DOWNCASE    in a given string, turn upper-case characters into lower-case

For a string x, (string-downcase x) is the result of applying
char-downcase to each character in x.

The guard for string-downcase requires its argument to be a string
containing only standard characters.

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

STRING-EQUAL    string equality without regard to case

For strings str1 and str2, (string-equal str1 str2) is true if and only
str1 and str2 are the same except perhaps for the cases of their
characters.

The guard on string-equal requires that its arguments are strings
consisting of standard characters (see STANDARD-CHAR-LISTP).

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

STRING-LISTP    recognizer for a true list of strings

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

STRING-UPCASE    in a given string, turn lower-case characters into upper-case

For a string x, (string-upcase x) is the result of applying char-upcase
to each character in x.

The guard for string-upcase requires its argument to be a string
containing only standard characters.

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

STRING<    less-than test for strings

(String< str1 str2) is non-nil if and only if the string str1 precedes
the string str2 lexicographically, where character inequalities are
tested using char<.  When non-nil, (string< str1 str2) is the first
position (zero-based) at which the strings differ.  Here are some
examples.

     ACL2 !>(string< "abcd" "abu")
     2
     ACL2 !>(string< "abcd" "Abu")
     NIL
     ACL2 !>(string< "abc" "abcde")
     3
     ACL2 !>(string< "abcde" "abc")
     NIL

The guard for string< specifies that its arguments are strings.

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

STRING<=    less-than-or-equal test for strings

(String<= str1 str2) is non-nil if and only if the string str1 precedes
the string str2 lexicographically or the strings are equal.  When
non-nil, (string<= str1 str2) is the first position (zero-based) at
which the strings differ, if they differ, and otherwise is their common
length.  See STRING<.

The guard for string<= specifies that its arguments are strings.

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

STRING>    greater-than test for strings

(String> str1 str2) is non-nil if and only if str2 precedes str1
lexicographically.  When non-nil, (string> str1 str2) is the first
position (zero-based) at which the strings differ.  See STRING<.

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

STRING>=    less-than-or-equal test for strings

(String>= str1 str2) is non-nil if and only if the string str2 precedes
the string str1 lexicographically or the strings are equal.  When
non-nil, (string>= str1 str2) is the first position (zero-based) at
which the strings differ, if they differ, and otherwise is their common
length.  See STRING>.

The guard for string>= specifies that its arguments are strings.

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

STRINGP    recognizer for strings

(stringp x) is true if and only if x is a string.

STRIP-CARS    collect up all first components of pairs in a list

(strip-cars x) is the list obtained by walking through the list x and
collecting up all first components (cars).  This function is
implemented in a tail-recursive way, despite its logical definition.

(strip-cars x) has a guard of (alistp x).

STRIP-CDRS    collect up all second components of pairs in a list

(strip-cdrs x) has a guard of (alistp x), and returns the list obtained
by walking through the list x and collecting up all second components
(cdrs).  This function is implemented in a tail-recursive way, despite
its logical definition.

SUBLIS    substitute an alist into a tree

(Sublis alist tree) is obtained by replacing every leaf of tree with
the result of looking that leaf up in the association list alist.
However, a leaf is left unchanged if it is not found as a key in alist.

Leaves are lookup up using the function assoc.  The guard for (sublis
alist tree) requires (eqlable-alistp alist).  This guard ensures that
the guard for assoc will be met for each lookup generated by sublis.

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

SUBSEQ    subsequence of a string or list

For any natural numbers start and end, where start <= end <= (length
seq), (subseq seq start end) is the subsequence of seq from index start
up to, but not including, index end.  End may be nil, which which case
it is treated as though it is (length seq), i.e., we obtain the
subsequence of seq from index start all the way to the end.

The guard for (subseq seq start end) is that seq is a true list or a
string, start and end are integers (except, end may be nil, in which
case it is treated as (length seq) for the rest of this discussion),
and 0 <= start <= end <= (length seq).

Subseq is a Common Lisp function.  See any Common Lisp documentation
for more information.  Note:  In Common Lisp the third argument of
subseq is optional, but in ACL2 it is required, though it may be nil as
explained above.

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

(Subsetp x y) is true if and only if every member of the list x is a
member of the list y.

Membership is tested using the function member.  Thus, the guard for
subsetp requires that its arguments are true lists, and moreover, at
least one satisfies eqlable-listp.  This guard ensures that the guard
for member will be met for each call generated by subsetp.

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

SUBSETP-EQUAL    check if all members of one list are members of the other

(Subsetp-equal x y) returns t if every member of x is a member of y,
where membership is tested using member-equal.

The guard for subsetp-equal requires both arguments to be true lists.
Subsetp-equal has the same functionality as the Common Lisp function
subsetp, except that it uses the equal function to test membership
rather than eql.

SUBST    a single substitution into a tree

(Subst new old tree) is obtained by substituting new for every
occurence of old in the given tree.

Equality to old is determined using the function eql.  The guard for
(subst new old tree) requires (eqlablep old), which ensures that the
guard for eql will be met for each comparison generated by subst.

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

SUBSTITUTE    substitute into a string or a list, using eql as test

(Substitute new old seq) is the result of replacing each occurrence of
old in seq, which is a list or a string, with new.

The guard for substitute requires that either seq is a string and new
is a character, or else:  seq is a true-listp such that either all of
its members are eqlablep or old is eqlablep.

Substitute is a Common Lisp function.  See any Common Lisp
documentation for more information.  Since ACL2 functions cannot take
keyword arguments (though macros can), the test used in substitute is
eql.

SYMBOL-<    less-than test for symbols

(symbol-< x y) is non-nil if and only if either the symbol-name of the
symbol x lexicographially precedes the symbol-name of the symbol y (in
the sense of string<) or else the symbol-names are equal and the
symbol-package-name of x lexicographically precedes that of y (in the
same sense).  So for example, (symbol-< 'abcd 'abce) and (symbol-<
'acl2::abcd 'foo::abce) are true.

The guard for symbol specifies that its arguments are symbols.

SYMBOL-ALISTP    recognizer for association lists with symbols as keys

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

SYMBOL-LISTP    recognizer for a true list of symbols

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

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

Completion Axiom:

     (equal (symbol-name x)
            (if (symbolp x)
                (symbol-name x)
              ""))

Guard for (symbol-name x):

     (symbolp x)

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

Completion Axiom:

     (equal (symbol-package-name x)
            (if (symbolp x)
                (symbol-package-name x)
              ""))

Guard for (symbol-package-name x):

     (symbolp x)

Note:  If the ACL2 image is built on GCL, then symbol-package-name
diverges from the name of the symbol's package in raw Lisp, in the case
that this package is the main Lisp package.  For example,
(symbol-package-name 'car) evaluates to "COMMON-LISP" regardless of of
the underlying Lisp implementation, even though the name of the main
Lisp package in GCL is "LISP".

SYMBOLP    recognizer for symbols

(symbolp x) is true if and only if x is a symbol.

SYS-CALL    make a system call to the host operating system

     Example Forms:
     (sys-call "cp" '("foo.lisp" "foo-copied.lisp"))
     (prog2$ (sys-call "cp" '("foo.lisp" "foo-copied.lisp"))
             (sys-call-status state))

The first argument of sys-call is a command for the host operating
system, and the second argument is a list of strings that are the
arguments for that command.  In GCL and perhaps other lisps, you can
put the arguments with the command; but this is not the case, for
example, in Allegro CL running on Linux.

The use of prog2$ above is optional, but illustrates a typical sort of
use when one wishes to get the return status.  See
SYS-CALL-STATUS.

     General Form:
     (sys-call cmd args)

This function logically returns nil.  However, it makes the indicated
call to the host operating system, as described above, using a function
supplied "under the hood" by the underlying Lisp system.  On occasions
where one wishes to obtain the numeric status returned by the host
operating system (or more precisely, by the Lisp function under the
hood that passes the system call to the host operating system), one may
do so;  see SYS-CALL-STATUS.  The status value is the value
returned by that Lisp function, which may well be the same numeric
value returned by the host operating system for the underlying system
call.

Note that sys-call does not touch the ACL2 state; however,
sys-call-status updates the file-clock field of the state.  One may
view that update as modifying the fileclock to be at least as recent as
the time of the most recent sys-call.

Be careful if you use sys-call!  It can be used for example to overwrite
files, or worse!  The following example from Bob Boyer shows how to use
sys-call to execute, in effect, arbitrary Lisp forms.  ACL2 provides a
"trust tag" mechanism that requires execution of a defttag form before
you can use sys-call; see DEFTTAG.  (Note: The setting of the
raw Lisp variable *features* below is just to illustrate that any such
mischief is possible.  Normally *features* is a list with more than a
few elements.)

     % cat foo
     print *0x85d2064=0x838E920
     detach
     q
     % acl2
     ... boilerplate deleted
     ACL2 !>(sys-call "gdb -p $PPID -w < foo >& /dev/null " nil)
     NIL
     ACL2 !>:q

     Exiting the ACL2 read-eval-print loop.  To re-enter, execute (LP).
     ACL2>*features*

     (:AKCL-SET-MV)

     ACL2>

Finally, we make a comment about output redirection, which also applies
to other related features that one may expect of a shell.  Sys-call
does not directly support output redirection.  If you want to run a
program, P, and redirect its output, we suggest that you create a
wrapper script, W to call instead.  Thus W might be a shell script
containing the line:

     P $* >& foo.out

If this sort of solution proves inadequate, please contact the ACL2
implementors and perhaps we can come up with a solution.

SYS-CALL-STATUS    exit status from the preceding system call

This function returns two values, (mv status state).  The first is the
status returned by the most recent invocation of function sys-call; see
SYS-CALL.  The second is the ACL2 state object, which is also
the input to this function.

The function sys-call makes a system call to the host operating system
using a function supplied "under the hood" by the underlying Lisp
system.  The status value is the value returned by that Lisp function,
which may well be the same numeric value returned by the host operating
system for the underlying system call.  For more information, see
SYS-CALL.

TAKE    initial segment of a list

For any natural number n not exceeding the length of l, (take n l)
collects the first n elements of the list l.

The following is a theorem (though it takes some effort, including
lemmas, to get ACL2 to prove it):

     (equal (length (take n l)) (nfix n))

If n is is an integer greater than the length of l, then take pads the
list with the appropriate number of nil elements.  Thus, the following
is also a theorem.

     (implies (and (integerp n)
                   (true-listp l)
                   (<= (length l) n))
              (equal (take n l)
                     (append l (make-list (- n (length l))))))

For related functions, see NTHCDR and see BUTLAST.

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

TENTH    tenth member of the list

See any Common Lisp documentation for details.

THE    run-time type check

(The typ val) checks that val satisfies the type specification typ (see
TYPE-SPEC).  An error is caused if the check fails, and
otherwise, val is the value of this expression.  Here are some examples.

     (the integer 3)       ; returns 3
     (the (integer 0 6) 3) ; returns 3
     (the (integer 0 6) 7) ; causes an error

See TYPE-SPEC for a discussion of the legal type specifications.

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

THIRD    third member of the list

See any Common Lisp documentation for details.

TRUE-LIST-LISTP    recognizer for true (proper) lists of true lists

True-list-listp is the function that checks whether its argument is a
list that ends in, or equals, nil, and furthermore, all of its elements
have that property.  Also see TRUE-LISTP.

TRUE-LISTP    recognizer for proper (null-terminated) lists

True-listp is the function that checks whether its argument is a list
that ends in, or equals, nil.

TRUNCATE    division returning an integer by truncating toward 0

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

(Truncate i j) is the result of taking the quotient of i and j and
dropping the fraction.  For example, the quotient of -14 by 3 is -4
2/3, so dropping the fraction 2/3, we obtain a result for (truncate -14
3) of -4.

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

Truncate is a Common Lisp function.  However, note that unlike Common
Lisp, the ACL2 truncate function returns only a single value,

TYPE    See DECLARE.

TYPE-SPEC    type specifiers in declarations

     Examples:
     The symbol INTEGER in (declare (type INTEGER i j k)) is a type-spec.  Other
     type-specs supported by ACL2 include RATIONAL, COMPLEX, (INTEGER 0 127),
     (RATIONAL 1 *), CHARACTER, and ATOM.

The type-specs and their meanings (when applied to the variable x as in
(declare (type type-spec x)) are given below.

     type-spec              meaning
     (AND type1 ... typek)  (AND (p1 X) ... (pk X))
                            where (pj x) is the meaning for type-spec typej
     ATOM                   (ATOM X)
     BIT                    (OR (EQUAL X 1) (EQUAL X 0))
     CHARACTER              (CHARACTERP X)
     COMPLEX,               (AND (COMPLEX-RATIONALP X)
     (COMPLEX RATIONAL)          (RATIONALP (REALPART X))
                                 (RATIONALP (IMAGPART X)))
     (COMPLEX type)         (AND (COMPLEX-RATIONALP X)
                                 (p (REALPART X))
                                 (p (IMAGPART X)))
                            where (p x) is the meaning for type-spec type
     CONS                   (CONSP X)
     INTEGER                (INTEGERP X)
     (INTEGER i j)          (AND (INTEGERP X)   ; See notes below
                                 (<= i X)
                                 (<= X j))
     (MEMBER x1 ... xn)     (MEMBER X '(x1 ... xn))
     (MOD i)                same as (INTEGER 0 i-1)
     NIL                    NIL
     (NOT type)             (NOT (p X))
                            where (p x) is the meaning for type-spec type
     NULL                   (EQ X NIL)
     (OR type1 ... typek)   (OR (p1 X) ... (pk X))
                            where (pj x) is the meaning for type-spec typej
     RATIO                  (AND (RATIONALP X) (NOT (INTEGERP X)))
     RATIONAL               (RATIONALP X)
     (RATIONAL i j)         (AND (RATIONALP X)  ; See notes below
                                 (<= i X)
                                 (<= X j))
     REAL                   (RATIONALP X)       ; (REALP X) in ACL2(r)
     (REAL i j)             (AND (RATIONALP X)  ; See notes below
                                 (<= i X)
                                 (<= X j))
     (SATISFIES pred)       (pred X) ; Lisp requires a unary function, not a macro
     SIGNED-BYTE            (INTEGERP X)
     (SIGNED-BYTE i)        same as (INTEGER -2**i-1 (2**i-1)-1)
     STANDARD-CHAR          (STANDARD-CHARP X)
     STRING                 (STRINGP X)
     (STRING max)           (AND (STRINGP X) (EQUAL (LENGTH X) max))
     SYMBOL                 (SYMBOLP X)
     T                      T
     UNSIGNED-BYTE          same as (INTEGER 0 *)
     (UNSIGNED-BYTE i)      same as (INTEGER 0 (2**i)-1)

_Notes:_

In general, (integer i j) means

          (AND (INTEGERP X)
               (<= i X)
               (<= X j)).

But if i is the symbol *, the first inequality is omitted.  If j is the
symbol *, the second inequality is omitted.  If instead of being an
integer, the second element of the type specification is a list
containing an integer, (i), then the first inequality is made strict.
An analogous remark holds for the (j) case.  The RATIONAL and REAL type
specifiers are similarly generalized.

UNARY--    arithmetic negation function

Completion Axiom:

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

Guard for (unary- x):

     (acl2-numberp x)

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

Calls of the macro - on one argument expand to calls of unary-; see
-.

UNARY-/    reciprocal function

Completion Axiom:

     (equal (unary-/ x)
            (if (and (acl2-numberp x)
                     (not (equal x 0)))
                (unary-/ x)
              0))

Guard for (unary-/ x):

     (and (acl2-numberp x)
          (not (equal x 0)))

Notice that like all arithmetic functions, unary-/ treats non-numeric
inputs as 0.

Calls of the macro / on one argument expand to calls of unary-/; see
/.

UNION-EQ    union of two lists of symbols

(Union-eq x y) equals a list whose members (see MEMBER-EQ)
contains the members of x and the members of y.  More precisely, the
resulting list is the same as one would get by first deleting the
members of y from x, and then concatenating the result to the front of
y.

The guard for union-eq requires both arguments to be true lists, but in
fact further requires the first list to contain only symbols, as the
function member-eq is used to test membership (with eq).  See
UNION-EQUAL.

UNION-EQUAL    union of two lists

(Union-equal x y) equals a list whose members (see
MEMBER-EQUAL) contains the members of x and the members of y.  More
precisely, the resulting list is the same as one would get by first
deleting the members of y from x, and then concatenating the result to
the front of y.

The guard for union-equal requires both arguments to be true lists.
Essentially, union-equal has the same functionality as the Common Lisp
function union, except that it uses the equal function to test
membership rather than eql.  However, we do not include the function
union in ACL2, because the Common Lisp language does not specify the
order of the elements in the list that it returns.