Index

This index lists all documented topics in ACL2, arranged into sections. The first section is devoted to those whose names begin with signs (and digits), such as *STANDARD-CI* and 1+. Thereafter we have one section for each of the 26 letters of the alphabet. The last section is devoted to those topics in the ACL2-PC package. By clicking on the appropriate entry of the line below you can go to the corresponding section of the index. You may use Find to search the Index. We also provide an index based on Major Topics.
Signs A B C D E F G H I J K L M N O P Q R S T U V W X Y Z ACL2-PC:: 



Signs

* -- multiplication macro

*STANDARD-CI* -- an ACL2 character-based analogue of CLTL's *standard-input*

*STANDARD-CO* -- the ACL2 analogue of CLTL's *standard-output*

*STANDARD-OI* -- an ACL2 object-based analogue of CLTL's *standard-input*

*TERMINAL-MARKUP-TABLE* -- a markup table used for printing to the terminal

*UNTROUBLESOME-CHARACTERS* -- some not so weird characters

+ -- addition macro

- -- macro for subtraction and negation

/ -- macro for division and reciprocal

/= -- test inequality of two numbers

1+ -- increment by 1

1- -- decrement by 1

< -- less-than

<= -- less-than-or-equal test

= -- test equality of two numbers

> -- greater-than test

>= -- greater-than-or-equal test

@ -- get the value of a global variable in state



A

A Flying Tour of ACL2 -- A Flying Tour of ACL2

A Sketch of How the Rewriter Works -- A Sketch of How the Rewriter Works

A Tiny Warning Sign -- A Tiny Warning Sign

A Trivial Proof -- A Trivial Proof

A Typical State -- A Typical State

A Walking Tour of ACL2 -- A Walking Tour of ACL2

A! -- to return to the top-level of ACL2's command loop

ABORT! -- to return to the top-level of ACL2's command loop

ABOUT-ACL2 -- about ACL2

ABS -- the absolute value of a real number

ACCUMULATED-PERSISTENCE -- to get statistics on which runes are being tried

ACCUMULATED-PERSISTENCE-SUBTLETIES -- some subtle aspects of the counting done by accumulated-persistence

ACKNOWLEDGMENTS -- some contributors to the well-being of ACL2

ACL2 Characters -- ACL2 Characters

ACL2 Conses or Ordered Pairs -- ACL2 Conses or Ordered Pairs

ACL2 Strings -- ACL2 Strings

ACL2 Symbols -- ACL2 Symbols

ACL2 System Architecture -- ACL2 System Architecture

ACL2 as an Interactive Theorem Prover -- ACL2 as an Interactive Theorem Prover

ACL2 as an Interactive Theorem Prover (cont) -- ACL2 as an Interactive Theorem Prover (cont)

ACL2 is an Untyped Language -- ACL2 is an Untyped Language

ACL2-AS-STANDALONE-PROGRAM -- Calling ACL2 from another program

ACL2-COUNT -- a commonly used measure for justifying recursion

ACL2-CUSTOMIZATION -- file of initial commands for ACL2 to run at startup

ACL2-DEFAULTS-TABLE -- a table specifying certain defaults, e.g., the default defun-mode

ACL2-HELP -- the acl2-help mailing list

ACL2-NUMBERP -- recognizer for numbers

ACL2-SEDAN -- ACL2 Sedan interface

ACL2-TUTORIAL -- tutorial introduction to ACL2

ACL2-USER -- a package the ACL2 user may prefer

ACL2S -- See acl2-sedan.

ACONS -- constructor for association lists

ACTIVE-RUNEP -- check that a rune exists and is enabled

ADD-BINOP -- associate a function name with a macro name

ADD-CUSTOM-KEYWORD-HINT -- add a new custom keyword hint

ADD-DEFAULT-HINTS -- add to the default hints

ADD-DEFAULT-HINTS! -- add to the default hints non-locally

ADD-DIVE-INTO-MACRO -- associate proof-checker diving function with macro name

ADD-INCLUDE-BOOK-DIR -- associate directory to keyword for include-book's :dir argument

ADD-INVISIBLE-FNS -- make some unary functions invisible to the loop-stopper algorithm

ADD-MACRO-ALIAS -- associate a function name with a macro name

ADD-MATCH-FREE-OVERRIDE -- set :match-free value to :once or :all in existing rules

ADD-NTH-ALIAS -- associate one symbol with another for printing of nth/update-nth terms

ADD-OVERRIDE-HINTS -- add to the override-hints

ADD-OVERRIDE-HINTS! -- add non-locally to the override-hints

ADD-RAW-ARITY -- add arity information for raw mode

ADD-TO-SET -- add a symbol to a list

ADD-TO-SET-EQ -- See add-to-set.

ADD-TO-SET-EQL -- See add-to-set.

ADD-TO-SET-EQUAL -- See add-to-set.

ALISTP -- recognizer for association lists

ALLOCATE-FIXNUM-RANGE -- set aside fixnums in GCL

ALPHA-CHAR-P -- recognizer for alphabetic characters

ALPHORDER -- total order on atoms

ALTERNATIVE-INTRODUCTION -- introduction to ACL2

AND -- conjunction

ANNOTATED-ACL2-SCRIPTS -- examples of ACL2 scripts

APPEND -- concatenate zero or more lists

APROPOS -- searching the documentation online

ARCHITECTURE-OF-THE-PROVER -- a simple overview of how the prover works

AREF1 -- access the elements of a 1-dimensional array

AREF2 -- access the elements of a 2-dimensional array

ARGS -- args, guard, type, constraint, etc., of a function symbol

ARRAY1P -- recognize a 1-dimensional array

ARRAY2P -- recognize a 2-dimensional array

ARRAYS -- an introduction to ACL2 arrays

ARRAYS-EXAMPLE -- an example illustrating ACL2 arrays

ASET1 -- set the elements of a 1-dimensional array

ASET2 -- set the elements of a 2-dimensional array

ASH -- arithmetic shift operation

ASSERT$ -- cause a hard error if the given test is false

ASSERT-EVENT -- assert that a given form returns a non-nil value

ASSIGN -- assign to a global variable in state

ASSOC -- look up key in association list

ASSOC-EQ -- See assoc.

ASSOC-EQUAL -- See assoc.

ASSOC-KEYWORD -- look up key in a keyword-value-listp

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

ATOM -- recognizer for atoms

ATOM-LISTP -- recognizer for a true list of atoms

About Models -- About Models

About Types -- About Types

About the ACL2 Home Page -- About the ACL2 Home Page

About the Admission of Recursive Definitions -- About the Admission of Recursive Definitions

About the Prompt -- About the Prompt

An Example Common Lisp Function Definition -- An Example Common Lisp Function Definition

An Example of ACL2 in Use -- An Example of ACL2 in Use

Analyzing Common Lisp Models -- Analyzing Common Lisp Models



B

BACKCHAIN-LIMIT -- limiting the effort expended on relieving hypotheses

BACKCHAIN-LIMIT-RW -- hints keyword :BACKCHAIN-LIMIT-RW

BACKTRACK -- hints keyword :BACKTRACK

BDD -- ordered binary decision diagrams with rewriting

BDD-ALGORITHM -- summary of the BDD algorithm in ACL2

BDD-INTRODUCTION -- examples illustrating the use of BDDs in ACL2

BIBLIOGRAPHY -- reports about ACL2

BINARY-* -- multiplication function

BINARY-+ -- addition function

BINARY-APPEND -- concatenate two lists

BIND-FREE -- to bind free variables of a rewrite or linear rule

BIND-FREE-EXAMPLES -- examples pertaining to bind-free hypotheses

BINOP-TABLE -- associates binary function with the corresponding macro

BOOK-COMPILED-FILE -- creating and loading of compiled and expansion files for books

BOOK-CONTENTS -- restrictions on the forms inside books

BOOK-EXAMPLE -- how to create, certify, and use a simple book

BOOK-MAKEFILES -- makefile support provided with the ACL2 distribution

BOOK-NAME -- conventions associated with book names

BOOKS -- files of ACL2 event forms

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

BOOLEANP -- recognizer for booleans

BREAK$ -- cause an immediate Lisp break

BREAK-LEMMA -- a quick introduction to breaking rewrite rules in ACL2

BREAK-ON-ERROR -- break when encountering a hard or soft error caused by ACL2

BREAK-REWRITE -- the read-eval-print loop entered to monitor rewrite rules

BREAKS -- Common Lisp breaks

BRR -- to enable or disable the breaking of rewrite rules

BRR-COMMANDS -- Break-Rewrite Commands

BRR@ -- to access context sensitive information within break-rewrite

BUILT-IN-CLAUSE -- to build a clause into the simplifier

BUTLAST -- all but a final segment of a list

BY -- hints keyword :BY



C

CAAAAR -- car of the caaar

CAAADR -- car of the caadr

CAAAR -- car of the caar

CAADAR -- car of the cadar

CAADDR -- car of the caddr

CAADR -- car of the cadr

CAAR -- car of the car

CADAAR -- car of the cdaar

CADADR -- car of the cdadr

CADAR -- car of the cdar

CADDAR -- car of the cddar

CADDDR -- car of the cdddr

CADDR -- car of the cddr

CADR -- car of the cdr

CANONICAL-PATHNAME -- the true absolute filename, with soft links resolved

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

CASE -- conditional based on if-then-else using eql

CASE-MATCH -- pattern matching or destructuring

CASE-SPLIT -- like force but immediately splits the top-level goal on the hypothesis

CASE-SPLIT-LIMITATIONS -- a list of two ``numbers'' limiting the number of cases produced at once

CASES -- hints keyword :CASES

CBD -- connected book directory string

CDAAAR -- cdr of the caaar

CDAADR -- cdr of the caadr

CDAAR -- cdr of the caar

CDADAR -- cdr of the cadar

CDADDR -- cdr of the caddr

CDADR -- cdr of the cadr

CDAR -- cdr of the car

CDDAAR -- cdr of the cdaar

CDDADR -- cdr of the cdadr

CDDAR -- cdr of the cdar

CDDDAR -- cdr of the cddar

CDDDDR -- cdr of the cdddr

CDDDR -- cdr of the cddr

CDDR -- cdr of the cdr

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

CEILING -- division returning an integer by truncating toward positive infinity

CERTIFICATE -- how a book is known to be admissible and where its defpkgs reside

CERTIFY-BOOK -- how to produce a certificate for a book

CERTIFY-BOOK! -- a variant of certify-book

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

CHAR-CODE -- the numeric code for a given character

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

CHAR-EQUAL -- character equality without regard to case

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

CHAR< -- less-than test for characters

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

CHAR> -- greater-than test for characters

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

CHARACTER-ALISTP -- recognizer for association lists with characters as keys

CHARACTER-LISTP -- recognizer for a true list of characters

CHARACTERP -- recognizer for characters

CHARACTERS -- characters in ACL2

CHECK-SUM -- assigning ``often unique'' integers to files and objects

CHECKPOINT-FORCED-GOALS -- Cause forcing goals to be checkpointed in proof trees

CLAUSE-IDENTIFIER -- the internal form of a goal-spec

CLAUSE-PROCESSOR -- make or apply a :clause-processor rule (goal-level simplifier)

CLEAR-HASH-TABLES -- deprecated feature

CLEAR-MEMOIZE-STATISTICS -- clears all profiling info displayed by (memoize-summary)

CLEAR-MEMOIZE-TABLE -- forget values remembered for the given function

CLEAR-MEMOIZE-TABLES -- forget values remembered for all the memoized functions

CLOSE-INPUT-CHANNEL -- See io.

CLOSE-OUTPUT-CHANNEL -- See io.

CLOSE-TRACE-FILE -- stop redirecting trace output to a file

CODE-CHAR -- the character corresponding to a given numeric code

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

COMMAND -- forms you type at the top-level, but...

COMMAND-DESCRIPTOR -- an object describing a particular command typed by the user

COMMON-LISP -- relation to Common Lisp, including deviations from the spec

COMP -- compile some ACL2 functions

COMP-GCL -- compile some ACL2 functions leaving .c and .h files

COMPILATION -- compiling ACL2 functions

COMPILING-ACL2P -- compiling ACL2(p)

COMPLEX -- create an ACL2 number

COMPLEX-RATIONALP -- recognizes complex rational numbers

COMPLEX/COMPLEX-RATIONALP -- recognizer for complex numbers

COMPOUND-RECOGNIZER -- make a rule used by the typing mechanism

COMPRESS1 -- remove irrelevant pairs from a 1-dimensional array

COMPRESS2 -- remove irrelevant pairs from a 2-dimensional array

COMPUTED-HINTS -- computing advice to the theorem proving process

CONCATENATE -- concatenate lists or strings together

COND -- conditional based on if-then-else

CONGRUENCE -- the relations to maintain while simplifying arguments

CONJUGATE -- complex number conjugate

CONS -- pair and list constructor

CONS-SUBTREES -- (cons-subtrees x nil) builds a fast alist that associates each subtree
of X with T, without duplication.


CONSERVATIVITY-OF-DEFCHOOSE -- proof of conservativity of defchoose

CONSP -- recognizer for cons pairs

CONSTRAINT -- restrictions on certain functions introduced in encapsulate events

COPYRIGHT -- ACL2 copyright, license, sponsorship

COROLLARY -- the corollary formula of a rune

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

CPU-CORE-COUNT -- the number of cpu cores

CURRENT-PACKAGE -- the package used for reading and printing

CURRENT-THEORY -- currently enabled rules as of logical name

CUSTOM-KEYWORD-HINTS -- user-defined hints

CW -- print to the comment window

CW! -- print to the comment window

CW-GSTACK -- debug a rewriting loop or stack overflow

Common Lisp -- Common Lisp

Common Lisp as a Modeling Language -- Common Lisp as a Modeling Language

Conversion -- Conversion to Uppercase

Corroborating Models -- Corroborating Models



D

DEALING-WITH-KEY-COMBINATIONS-OF-FUNCTION-SYMBOLS -- how to get rid of key combinations of function symbols

DECLARE -- declarations

DECLARE-STOBJS -- declaring a formal parameter name to be a single-threaded object

DEFABBREV -- a convenient form of macro definition for simple expansions

DEFATTACH -- execute constrained functions using corresponding attached functions

DEFAULT -- return the :default from the header of a 1- or 2-dimensional array

DEFAULT-BACKCHAIN-LIMIT -- specifying the backchain limit for a rule

DEFAULT-DEFUN-MODE -- the default defun-mode of defun'd functions

DEFAULT-HINTS -- a list of hints added to every proof attempt

DEFAULT-HINTS-TABLE -- a table used to provide hints for proofs

DEFAULT-PRINT-PROMPT -- the default prompt printed by ld

DEFAULT-RULER-EXTENDERS -- the default ruler-extenders for defun'd functions

DEFAULT-VERIFY-GUARDS-EAGERNESS -- See set-verify-guards-eagerness.

DEFAXIOM -- add an axiom

DEFCHOOSE -- define a Skolem (witnessing) function

DEFCONG -- prove congruence rule

DEFCONST -- define a constant

DEFDOC -- add a documentation topic

DEFEQUIV -- prove that a function is an equivalence relation

DEFEVALUATOR -- introduce an evaluator function

DEFEXEC -- attach a terminating executable function to a definition

DEFINE-PC-HELP -- define a macro command whose purpose is to print something

DEFINE-PC-MACRO -- define a proof-checker macro command

DEFINE-PC-META -- define a proof-checker meta command

DEFINE-TRUSTED-CLAUSE-PROCESSOR -- define a trusted (unverified) goal-level simplifier

DEFINITION -- make a rule that acts like a function definition

DEFLABEL -- build a landmark and/or add a documentation topic

DEFMACRO -- define a macro

DEFMACRO-LAST -- define a macro that returns its last argument, but with side effects

DEFN -- definition with guard t

DEFPKG -- define a new symbol package

DEFPROXY -- define a non-executable :program-mode function for attachment

DEFPUN -- define a tail-recursive function symbol

DEFREFINEMENT -- prove that equiv1 refines equiv2

DEFSTOBJ -- define a new single-threaded object

DEFSTUB -- stub-out a function symbol

DEFTHEORY -- define a theory (to enable or disable a set of rules)

DEFTHM -- prove and name a theorem

DEFTHMD -- prove and name a theorem and then disable it

DEFTTAG -- introduce a trust tag (ttag)

DEFUN -- define a function symbol

DEFUN-MODE -- determines whether a function definition is a logical act

DEFUN-MODE-CAVEAT -- potential soundness issue for functions with defun-mode :program

DEFUN-NX -- define a non-executable function symbol

DEFUN-SK -- define a function whose body has an outermost quantifier

DEFUN-SK-EXAMPLE -- a simple example using defun-sk

DEFUND -- define a function symbol and then disable it

DEFUNS -- an alternative to mutual-recursion

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

DELETE-ASSOC-EQ -- See delete-assoc.

DELETE-ASSOC-EQUAL -- See delete-assoc.

DELETE-INCLUDE-BOOK-DIR -- remove association of keyword for include-book's :dir argument

DENOMINATOR -- divisor of a ratio in lowest terms

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

DIGIT-TO-CHAR -- map a digit to a character

DIMENSIONS -- return the :dimensions from the header of a 1- or 2-dimensional array

DISABLE -- deletes names from current theory

DISABLE-FORCING -- to disallow forced case-splits

DISABLE-IMMEDIATE-FORCE-MODEP -- forced hypotheses are not attacked immediately

DISABLEDP -- determine whether a given name or rune is disabled

DIVE-INTO-MACROS-TABLE -- right-associated function information for the proof-checker

DMR -- dynamically monitor rewrites and other prover activity

DO-NOT -- hints keyword :DO-NOT

DO-NOT-INDUCT -- hints keyword :DO-NOT-INDUCT

DOC -- brief documentation (type :doc name)

DOC! -- all the documentation for a name (type :doc! name)

DOC-STRING -- formatted documentation strings

DOCS -- available documentation topics (by section)

DOCUMENTATION -- functions that display documentation

DOUBLE-REWRITE -- cause a term to be rewritten twice

DYNAMICALLY-MONITOR-REWRITES -- See dmr.



E

E/D -- enable/disable rules

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

E0-ORDINALP -- the old recognizer for ACL2 ordinals

EARLY-TERMINATION -- early termination for pand and por.

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

EIGHTH -- eighth member of the list

ELIM -- make a destructor elimination rule

EMACS -- emacs support for ACL2

EMBEDDED-EVENT-FORM -- forms that may be embedded in other events

ENABLE -- adds names to current theory

ENABLE-FORCING -- to allow forced splits

ENABLE-IMMEDIATE-FORCE-MODEP -- forced hypotheses are attacked immediately

ENCAPSULATE -- constrain some functions and/or hide some events

ENDP -- recognizer for empty lists

ENTER-BOOT-STRAP-MODE -- The first millisecond of the Big Bang

EQ -- equality of symbols

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

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

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

EQLABLEP -- the guard for the function eql

EQUAL -- true equality

EQUALITY-VARIANTS -- versions of a function using different equality tests

EQUALITY-VARIANTS-DETAILS -- details about equality-variants

EQUIVALENCE -- mark a relation as an equivalence relation

EQUIVALENT-FORMULAS-DIFFERENT-REWRITE-RULES -- logically equivalent formulas can generate radically different rules

ER -- print an error message and ``cause an error''

ER-PROGN -- perform a sequence of state-changing ``error triples''

ERROR1 -- print an error message and cause a ``soft error''

ESCAPE-TO-COMMON-LISP -- escaping to Common Lisp

EVALUATOR-RESTRICTIONS -- some restrictions on the use of evaluators in meta-level rules

EVENP -- test whether an integer is even

EVENTS -- functions that extend the logic

EVISC-TABLE -- support for abbreviated output

EVISC-TUPLE -- control suppression of details when printing

EVISCERATE-HIDE-TERMS -- to print (hide ...) as <hidden>

EXAMPLE-INDUCTION-SCHEME-BINARY-TREES -- induction on binary trees

EXAMPLE-INDUCTION-SCHEME-DOWN-BY-2 -- induction downwards 2 steps at a time

EXAMPLE-INDUCTION-SCHEME-NAT-RECURSION -- induction on natural numbers

EXAMPLE-INDUCTION-SCHEME-ON-LISTS -- induction on lists

EXAMPLE-INDUCTION-SCHEME-ON-SEVERAL-VARIABLES -- induction on several variables

EXAMPLE-INDUCTION-SCHEME-UPWARDS -- induction upwards

EXAMPLE-INDUCTION-SCHEME-WITH-ACCUMULATORS -- induction scheme with accumulators

EXAMPLE-INDUCTION-SCHEME-WITH-MULTIPLE-INDUCTION-STEPS -- induction scheme with more than one induction step

EXAMPLE-INDUCTIONS -- some examples of induction schemes in ACL2

EXECUTABLE-COUNTERPART -- a rule for computing the value of a function

EXECUTABLE-COUNTERPART-THEORY -- executable counterpart rules as of logical name

EXISTS -- existential quantifier

EXIT -- quit entirely out of Lisp

EXIT-BOOT-STRAP-MODE -- the end of pre-history

EXPAND -- hints keyword :EXPAND

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

EXPT -- exponential function

EXTENDED-METAFUNCTIONS -- state and context sensitive metafunctions

EXTRA-INFO -- generate markers to indicate sources of guard proof obligations

Evaluating App on Sample Input -- Evaluating App on Sample Input



F

FAILED-FORCING -- how to deal with a proof failure in a forcing round

FAILURE -- how to deal with a proof failure

FAST-ALIST-FREE -- (fast-alist-free alist) throws away the hash table associated with a fast
alist.


FAST-ALIST-LEN -- (fast-alist-len alist) counts the number of unique keys in a fast alist.

FAST-ALIST-SUMMARY -- (fast-alist-summary) prints some basic statistics about any current fast
alists.


FAST-ALISTS -- alists with hidden hash tables for faster execution

FC-REPORT -- to report on the forward chaining activity in the most recent proof

FIFTH -- fifth member of the list

FILE-READING-EXAMPLE -- example of reading files in ACL2

FIND-RULES-OF-RUNE -- find the rules named rune

FIRST -- first member of the list

FIX -- coerce to a number

FIX-TRUE-LIST -- coerce to a true list

FLET -- local binding of function symbols

FLOOR -- division returning an integer by truncating toward negative infinity

FLUSH-COMPRESS -- flush the under-the-hood array for the given name

FLUSH-HONS-GET-HASH-TABLE-LINK -- deprecated feature

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

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

FMS!-TO-STRING -- See printing-to-strings.

FMS-TO-STRING -- See printing-to-strings.

FMT -- formatted printing

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

FMT!-TO-STRING -- See printing-to-strings.

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

FMT-TO-STRING -- See printing-to-strings.

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

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

FMT1!-TO-STRING -- See printing-to-strings.

FMT1-TO-STRING -- See printing-to-strings.

FORALL -- universal quantifier

FORCE -- identity function used to force a hypothesis

FORCING-ROUND -- a section of a proof dealing with forced assumptions

FORWARD-CHAINING -- make a rule to forward chain when a certain trigger arises

FORWARD-CHAINING-REPORTS -- to see reports about the forward chaining process

FOURTH -- fourth member of the list

FREE-VARIABLES -- free variables in rules

FREE-VARIABLES-EXAMPLES -- examples pertaining to free variables in rules

FREE-VARIABLES-EXAMPLES-FORWARD-CHAINING -- examples pertaining to free variables in forward-chaining rules

FREE-VARIABLES-EXAMPLES-REWRITE -- examples pertaining to free variables in rewrite rules

FREE-VARIABLES-TYPE-PRESCRIPTION -- matching for free variable in type-prescription rules

FREQUENTLY-ASKED-QUESTIONS-BY-NEWCOMERS -- some questions newcomers frequently ask

FULL-BOOK-NAME -- book naming conventions assumed by ACL2

FUNCTION-THEORY -- function symbol rules as of logical name

FUNCTIONAL-INSTANTIATION-EXAMPLE -- a small proof demonstrating functional instantiation

FURTHER-INFORMATION-ON-REWRITING -- a grab bag of advice and information on rewriting

Flawed Induction Candidates in App Example -- Flawed Induction Candidates in App Example

Free Variables in Top-Level Input -- Free Variables in Top-Level Input

Functions for Manipulating these Objects -- Functions for Manipulating these Objects



G

GAG-MODE -- verbosity of proof output

GC$ -- invoke the garbage collector

GCL -- tips on building and using ACL2 based on Gnu Common Lisp

GENERALIZE -- make a rule to restrict generalizations

GENERALIZED-BOOLEANS -- potential soundness issues related to ACL2 predicates

GENERALIZING-KEY-CHECKPOINTS -- getting rid of unnecessary specificity

GET-OUTPUT-STREAM-STRING$ -- See io.

GET-WORMHOLE-STATUS -- make a wormhole's status visible outside the wormhole

GETENV$ -- read an environment variable

GETPROP -- access fast property lists

GOAL-SPEC -- to indicate where a hint is to be used

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

GOOD-BYE -- quit entirely out of Lisp

GRANULARITY -- limit the amount of parallelism

GROUND-ZERO -- enabled rules in the startup theory

GUARD -- restricting the domain of a function

GUARD-DEBUG -- generate markers to indicate sources of guard proof obligations

GUARD-EVALUATION-EXAMPLES-LOG -- log showing combinations of defun-modes and guard-checking

GUARD-EVALUATION-EXAMPLES-SCRIPT -- a script to show combinations of defun-modes and guard-checking

GUARD-EVALUATION-TABLE -- a table that shows combinations of defun-modes and guard-checking

GUARD-EXAMPLE -- a brief transcript illustrating guards in ACL2

GUARD-HINTS -- xargs keyword :GUARD-HINTS

GUARD-INTRODUCTION -- introduction to guards in ACL2

GUARD-MISCELLANY -- miscellaneous remarks about guards

GUARD-OBLIGATION -- the guard proof obligation

GUARD-QUICK-REFERENCE -- brief summary of guard checking and guard verification

GUARDS-AND-EVALUATION -- the relationship between guards and evaluation

GUARDS-FOR-SPECIFICATION -- guards as a specification device

Guards -- Guards

Guessing the Type of a Newly Admitted Function -- Guessing the Type of a Newly Admitted Function

Guiding the ACL2 Theorem Prover -- Guiding the ACL2 Theorem Prover



H

HANDS-OFF -- hints keyword :HANDS-OFF

HARD-ERROR -- print an error message and stop execution

HEADER -- return the header of a 1- or 2-dimensional array

HELP -- brief survey of ACL2 features

HIDDEN-DEATH-PACKAGE -- handling defpkg events that are local

HIDDEN-DEFPKG -- handling defpkg events that are local

HIDE -- hide a term from the rewriter

HINTS -- advice to the theorem proving process

HINTS-AND-THE-WATERFALL -- how hints fit into the ACL2 proof waterfall

HISTORY -- functions that display or change history

HONS -- (hons x y) returns a normed object equal to (cons x y).

HONS-ACONS -- (hons-acons key val alist) is the main way to create or extend
fast-alists.


HONS-ACONS! -- (hons-acons! key val alist) is an alternative to hons-acons that
produces normed, fast alists.


HONS-AND-MEMOIZATION -- hash cons, function memoization, and applicative hash tables

HONS-ASSOC-EQUAL -- (hons-assoc-equal key alist) is not fast; it serves as the logical
definition for hons-get.


HONS-CLEAR -- (hons-clear gc) is a drastic garbage collection mechanism that clears out
the underlying Hons Space.


HONS-COPY -- (hons-copy x) returns a normed object that is equal to X.

HONS-COPY-PERSISTENT -- (hons-copy-persistent x) returns a normed object that is equal to X
and which will be re-normed after any calls to hons-clear.


HONS-EQUAL -- (hons-equal x y) is a recursive equality check that optimizes when parts of
its arguments are normed.


HONS-EQUAL-LITE -- (hons-equal-lite x y) is a non-recursive equality check that optimizes if
its arguments are normed.


HONS-GET -- (hons-get key alist) is the efficient lookup operation for
fast-alists.


HONS-RESIZE -- (hons-resize ...) can be used to manually adjust the sizes of the hash
tables that govern which ACL2 Objects are considered normed.


HONS-SHRINK-ALIST -- (hons-shrink-alist alist ans) can be used to eliminate "shadowed pairs"
from an alist or to copy fast-alists.


HONS-SHRINK-ALIST! -- (hons-shrink-alist! alist ans) is an alternative to hons-shrink-alist
that produces a normed result.


HONS-SUMMARY -- (hons-summary) prints basic information about the sizes of the tables in
the current Hons Space.


HONS-WASH -- (hons-wash) is like gc$ but can also garbage collect normed
objects (CCL Only).


Hey Wait! Is ACL2 Typed or Untyped(Q) -- Hey Wait! Is ACL2 Typed or Untyped?

How Long Does It Take to Become an Effective User(Q) -- How Long Does It Take to Become an Effective User?

How To Find Out about ACL2 Functions -- How To Find Out about ACL2 Functions

How To Find Out about ACL2 Functions (cont) -- How To Find Out about ACL2 Functions (cont)



I

I-AM-HERE -- a convenient marker for use with rebuild

I-CLOSE -- ACL2(r) test for whether two numbers are infinitesimally close

I-LARGE -- ACL2(r) recognizer for infinitely large numbers

I-LIMITED -- ACL2(r) recognizer for limited numbers

I-SMALL -- ACL2(r) recognizer for infinitesimal numbers

IDENTITY -- the identity function

IF -- if-then-else function

IF* -- for conditional rewriting with BDDs

IFF -- logical ``if and only if''

IFIX -- coerce to an integer

IGNORABLE -- See declare.

IGNORE -- See declare.

ILLEGAL -- print an error message and stop execution

IMAGPART -- imaginary part of a complex number

IMMEDIATE-FORCE-MODEP -- when executable counterpart is enabled,
forced hypotheses are attacked immediately


IMPLIES -- logical implication

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

IN-ARITHMETIC-THEORY -- designate ``current'' theory for some rewriting done in linear arithmetic

IN-PACKAGE -- select current package

IN-THEORY -- designate ``current'' theory (enabling its rules)

INCLUDE-BOOK -- load the events in a file

INCOMPATIBLE -- declaring that two rules should not both be enabled

INDUCT -- hints keyword :INDUCT

INDUCTION -- make a rule that suggests a certain induction

INSTRUCTIONS -- instructions to the proof checker

INT= -- test equality of two integers

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

INTEGER-LISTP -- recognizer for a true list of integers

INTEGERP -- recognizer for whole numbers

INTERESTING-APPLICATIONS -- some industrial examples of ACL2 use

INTERN -- create a new symbol in a given package

INTERN$ -- create a new symbol in a given package

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

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

INTERSECTION-EQ -- See intersection$.

INTERSECTION-EQUAL -- See intersection$.

INTERSECTION-THEORIES -- intersect two theories

INTERSECTP -- test whether two lists intersect

INTERSECTP-EQ -- See intersectp.

INTERSECTP-EQUAL -- See intersectp.

INTRODUCTION-TO-A-FEW-SYSTEM-CONSIDERATIONS -- the mechanics of interaction with the theorem prover

INTRODUCTION-TO-HINTS -- how to provide hints to the theorem prover

INTRODUCTION-TO-KEY-CHECKPOINTS -- What questions to ask at key checkpoints

INTRODUCTION-TO-REWRITE-RULES-PART-1 -- introduction to ACL2's notion of rewrite rules

INTRODUCTION-TO-REWRITE-RULES-PART-2 -- how to arrange rewrite rules

INTRODUCTION-TO-THE-DATABASE -- how to update the database

INTRODUCTION-TO-THE-THEOREM-PROVER -- how the theorem prover works -- level 0

INTRODUCTORY-CHALLENGE-PROBLEM-1 -- challenge problem 1 for the new user of ACL2

INTRODUCTORY-CHALLENGE-PROBLEM-1-ANSWER -- answer to challenge problem 1 for the new user of ACL2

INTRODUCTORY-CHALLENGE-PROBLEM-2 -- challenge problem 2 for the new user of ACL2

INTRODUCTORY-CHALLENGE-PROBLEM-2-ANSWER -- answer to challenge problem 2 for the new user of ACL2

INTRODUCTORY-CHALLENGE-PROBLEM-3 -- challenge problem 3 for the new user of ACL2

INTRODUCTORY-CHALLENGE-PROBLEM-3-ANSWER -- answer to challenge problem 3 for the new user of ACL2

INTRODUCTORY-CHALLENGE-PROBLEM-4 -- challenge problem 4 for the new user of ACL2

INTRODUCTORY-CHALLENGE-PROBLEM-4-ANSWER -- answer to challenge problem 4 for the new user of ACL2

INTRODUCTORY-CHALLENGES -- challenge problems for the new ACL2 user

INVISIBLE-FNS-TABLE -- functions that are invisible to the loop-stopper algorithm

IO -- input/output facilities in ACL2

IPRINT -- See set-iprint.

IPRINTING -- See set-iprint.

IRRELEVANT-FORMALS -- formals that are used but only insignificantly



J



K

KEEP -- how we know if include-book read the correct files

KEYWORD -- See keywordp.

KEYWORD-COMMANDS -- how keyword commands are processed

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

KEYWORDP -- recognizer for keywords

KWOTE -- quote an arbitrary object

KWOTE-LST -- quote an arbitrary true list of objects



L

LAMBDA -- See term.

LAST -- the last cons (not element) of a list

LD -- the ACL2 read-eval-print loop, file loader, and command processor

LD-ERROR-ACTION -- determines ld's response to an error

LD-ERROR-TRIPLES -- determines whether a form caused an error during ld

LD-EVISC-TUPLE -- determines whether ld suppresses details when printing

LD-KEYWORD-ALIASES -- allows the abbreviation of some keyword commands

LD-POST-EVAL-PRINT -- determines whether and how ld prints the result of evaluation

LD-PRE-EVAL-FILTER -- determines which forms ld evaluates

LD-PRE-EVAL-PRINT -- determines whether ld prints the forms to be eval'd

LD-PROMPT -- determines the prompt printed by ld

LD-QUERY-CONTROL-ALIST -- how to default answers to queries

LD-REDEFINITION-ACTION -- to allow redefinition without undoing

LD-SKIP-PROOFSP -- how carefully ACL2 processes your commands

LD-VERBOSE -- determines whether ld prints ``ACL2 Loading ...''

LEMMA-INSTANCE -- an object denoting an instance of a theorem

LEN -- length of a list

LENGTH -- length of a string or proper list

LET -- binding of lexically scoped (local) variables

LET* -- binding of lexically scoped (local) variables

LEXORDER -- total order on ACL2 objects

LINEAR -- make some arithmetic inequality rules

LINEAR-ARITHMETIC -- A description of the linear arithmetic decision procedure

LIST -- build a list

LIST* -- build a list

LISTP -- recognizer for (not necessarily proper) lists

LOCAL -- hiding an event in an encapsulation or book

LOCAL-INCOMPATIBILITY -- when non-local events won't replay in isolation

LOGAND -- bitwise logical `and' of zero or more integers

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

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

LOGBITP -- the ith bit of an integer

LOGCOUNT -- number of ``on'' bits in a two's complement number

LOGEQV -- bitwise logical equivalence of zero or more integers

LOGIC -- to set the default defun-mode to :logic

LOGIC-KNOWLEDGE-TAKEN-FOR-GRANTED -- background knowledge in ACL2 logic for theorem prover tutorial

LOGIC-KNOWLEDGE-TAKEN-FOR-GRANTED-BASE-CASE -- a brief explanation of base cases

LOGIC-KNOWLEDGE-TAKEN-FOR-GRANTED-EQUALS-FOR-EQUALS -- substitution of equals for equals

LOGIC-KNOWLEDGE-TAKEN-FOR-GRANTED-EVALUATION -- evaluation during proofs

LOGIC-KNOWLEDGE-TAKEN-FOR-GRANTED-INDUCTIVE-PROOF -- a brief explanation of induction

LOGIC-KNOWLEDGE-TAKEN-FOR-GRANTED-INSTANCE -- a brief explanation of substitution instances

LOGIC-KNOWLEDGE-TAKEN-FOR-GRANTED-PROPOSITIONAL-CALCULUS -- a brief explanation of propositional calculus

LOGIC-KNOWLEDGE-TAKEN-FOR-GRANTED-Q1-ANSWER -- the inductive step of the rev-rev proof -- Answer to Question 1

LOGIC-KNOWLEDGE-TAKEN-FOR-GRANTED-Q2-ANSWER -- the inductive step of the rev-rev proof -- Answer to Question 2

LOGIC-KNOWLEDGE-TAKEN-FOR-GRANTED-Q3-ANSWER -- the inductive step of the rev-rev proof -- Answer to Question 2

LOGIC-KNOWLEDGE-TAKEN-FOR-GRANTED-REWRITING -- a brief explanation of rewriting from the logical perspective

LOGIC-KNOWLEDGE-TAKEN-FOR-GRANTED-REWRITING-REPEATEDLY -- further information on expanding definitions via rewriting

LOGICAL-NAME -- a name created by a logical event

LOGIOR -- bitwise logical inclusive or of zero or more integers

LOGNAND -- bitwise logical `nand' of two integers

LOGNOR -- bitwise logical `nor' of two integers

LOGNOT -- bitwise not of a two's complement number

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

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

LOGTEST -- test if two integers share a `1' bit

LOGXOR -- bitwise logical exclusive or of zero or more integers

LOOP-STOPPER -- limit application of permutative rewrite rules

LOWER-CASE-P -- recognizer for lower case characters

LP -- the Common Lisp entry to ACL2



M

MACRO-ALIASES-TABLE -- a table used to associate function names with macro names

MACRO-ARGS -- the formals list of a macro definition

MACRO-COMMAND -- compound command for the proof-checker

MAKE-CHARACTER-LIST -- coerce to a list of characters

MAKE-EVENT -- evaluate (expand) a given form and then evaluate the result

MAKE-EVENT-DETAILS -- details on make-event expansion

MAKE-LIST -- make a list of a given size

MAKE-ORD -- a constructor for ordinals.

MAKE-WORMHOLE-STATUS -- creates a wormhole status object from given status, entry code, and data

MAKEFILES -- See book-makefiles.

MANAGING-ACL2-PACKAGES -- user-contributed documentation on packages

MARKUP -- the markup language for ACL2 documentation strings

MAX -- the larger of two numbers

MAXIMUM-LENGTH -- return the :maximum-length from the header of an array

MBE -- attach code for execution

MBE1 -- attach code for execution

MBT -- introduce a test not to be evaluated

MEASURE -- xargs keyword :MEASURE

MEMBER -- membership predicate

MEMBER-EQ -- See member.

MEMBER-EQUAL -- See member.

MEMOIZE -- turn on memoization for one function

MEMOIZE-SUMMARY -- display all collected profiling and memoization table info

MEMSUM -- display all collected profiling and memoization info

META -- make a :meta rule (a hand-written simplifier)

MIN -- the smaller of two numbers

MINIMAL-THEORY -- a minimal theory to enable

MINUSP -- test whether a number is negative

MISCELLANEOUS -- a miscellany of documented functions and concepts
(often cited in more accessible documentation)


MOD -- remainder using floor

MOD-EXPT -- exponential function

MODE -- xargs keyword :MODE

MONITOR -- to monitor the attempted application of a rule name

MONITORED-RUNES -- print the monitored runes and their break conditions

MORE -- your response to :doc or :more's ``(type :more...)''

MORE! -- another response to ``(type :more for more, :more! for the rest)''

MORE-DOC -- a continuation of the :doc documentation

MUST-BE-EQUAL -- attach code for execution

MUTUAL-RECURSION -- define some mutually recursive functions

MUTUAL-RECURSION-PROOF-EXAMPLE -- a small proof about mutually recursive functions

MV -- returning a multiple value

MV-LET -- calling multi-valued ACL2 functions

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

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

MV? -- returning a single value

MV?-LET -- calling possibly multi-valued ACL2 functions

Modeling in ACL2 -- Modeling in ACL2

Models in Engineering -- Models in Engineering

Models of Computer Hardware and Software -- Models of Computer Hardware and Software



N

NAME -- syntactic rules on logical names

NATP -- a recognizer for the natural numbers

NFIX -- coerce to a natural number

NINTH -- ninth member of the list

NO-DUPLICATESP -- check for duplicates in a list

NO-DUPLICATESP-EQ -- See no-duplicatesp.

NO-DUPLICATESP-EQUAL -- See no-duplicatesp.

NO-THANKS -- hints keyword :NO-THANKS

NON-EXECUTABLE -- xargs keyword :NON-EXECUTABLE

NON-LINEAR-ARITHMETIC -- Non-linear Arithmetic

NONLINEARP -- hints keyword :NONLINEARP

NONNEGATIVE-INTEGER-QUOTIENT -- natural number division function

NORMALIZE -- xargs keyword :NORMALIZE

NORMED -- Normed objects are ACL2 Objects that are "canonical" or "unique" in a
certain sense.


NOT -- logical negation

NOTE-2-0 -- ACL2 Version 2.0 (July, 1997) Notes

NOTE-2-1 -- ACL2 Version 2.1 (December, 1997) Notes

NOTE-2-2 -- ACL2 Version 2.2 (August, 1998) Notes

NOTE-2-3 -- ACL2 Version 2.3 (October, 1998) Notes

NOTE-2-4 -- ACL2 Version 2.4 (August, 1999) Notes

NOTE-2-5 -- ACL2 Version 2.5 (June, 2000) Notes

NOTE-2-5(R) -- ACL2 Version 2.5(r) (June, 2000) Notes

NOTE-2-6 -- ACL2 Version 2.6 (November, 2001) Notes

NOTE-2-6(R) -- ACL2 Version 2.6(r) (November, 2001) Notes

NOTE-2-6-GUARDS -- ACL2 Version 2.6 Notes on Guard-related Changes

NOTE-2-6-NEW-FUNCTIONALITY -- ACL2 Version 2.6 Notes on New Functionality

NOTE-2-6-OTHER -- ACL2 Version 2.6 Notes on Other (Minor) Changes

NOTE-2-6-PROOF-CHECKER -- ACL2 Version 2.6 Notes on Proof-checker Changes

NOTE-2-6-PROOFS -- ACL2 Version 2.6 Notes on Changes in Proof Engine

NOTE-2-6-RULES -- ACL2 Version 2.6 Notes on Changes in Rules and Constants

NOTE-2-6-SYSTEM -- ACL2 Version 2.6 Notes on System-level Changes

NOTE-2-7 -- ACL2 Version 2.7 (November, 2002) Notes

NOTE-2-7(R) -- ACL2 Version 2.7(r) (November, 2002) Notes

NOTE-2-7-BUG-FIXES -- ACL2 Version 2.7 Notes on Bug Fixes

NOTE-2-7-GUARDS -- ACL2 Version 2.7 Notes on Guard-related Changes

NOTE-2-7-NEW-FUNCTIONALITY -- ACL2 Version 2.7 Notes on New Functionality

NOTE-2-7-OTHER -- ACL2 Version 2.7 Notes on Miscellaneous Changes

NOTE-2-7-PROOF-CHECKER -- ACL2 Version 2.7 Notes on Proof-checker Changes

NOTE-2-7-PROOFS -- ACL2 Version 2.7 Notes on Changes in Proof Engine

NOTE-2-7-RULES -- ACL2 Version 2.7 Notes on Changes in Rules and Constants

NOTE-2-7-SYSTEM -- ACL2 Version 2.7 Notes on System-level Changes

NOTE-2-8 -- ACL2 Version 2.8 (March, 2004) Notes

NOTE-2-8(R) -- ACL2 Version 2.8(r) (March, 2003) Notes

NOTE-2-8-BUG-FIXES -- ACL2 Version 2.8 Notes on Bug Fixes

NOTE-2-8-GUARDS -- ACL2 Version 2.8 Notes on Guard-related Changes

NOTE-2-8-NEW-FUNCTIONALITY -- ACL2 Version 2.8 Notes on New Functionality

NOTE-2-8-ORDINALS -- ACL2 Version 2.8 Notes on Changes to the Ordinals

NOTE-2-8-OTHER -- ACL2 Version 2.8 Notes on Miscellaneous Changes

NOTE-2-8-PROOF-CHECKER -- ACL2 Version 2.8 Notes on Proof-checker Changes

NOTE-2-8-PROOFS -- ACL2 Version 2.8 Notes on Changes in Proof Engine

NOTE-2-8-RULES -- ACL2 Version 2.8 Notes on Changes in Rules, Definitions, and Constants

NOTE-2-8-SYSTEM -- ACL2 Version 2.8 Notes on System-level Changes

NOTE-2-9 -- ACL2 Version 2.9 (October, 2004) Notes

NOTE-2-9(R) -- ACL2 Version 2.9(r) (October, 2004) Notes

NOTE-2-9-1 -- ACL2 Version 2.9.1 (December, 2004) Notes

NOTE-2-9-2 -- ACL2 Version 2.9.2 (April, 2005) Notes

NOTE-2-9-3 -- ACL2 Version 2.9.3 (August, 2005) Notes

NOTE-2-9-3-PPR-CHANGE -- change in pretty-printing for ACL2 Version_2.9.3

NOTE-2-9-4 -- ACL2 Version 2.9.4 (February, 2006) Notes

NOTE-2-9-5 -- Changes in Version 3.0 since Version 2.9.4

NOTE-3-0 -- ACL2 Version 3.0 (June, 2006) Notes

NOTE-3-0(R) -- ACL2 Version 3.0(r) (June, 2006) Notes

NOTE-3-0-1 -- ACL2 Version 3.0.1 (August, 2006) Notes

NOTE-3-0-1(R) -- ACL2 Version 3.0.1(r) (August, 2006) Notes

NOTE-3-0-2 -- ACL2 Version 3.0.2 (December, 2006) Notes

NOTE-3-1 -- ACL2 Version 3.1 (December, 2006) Notes

NOTE-3-1(R) -- ACL2 Version 3.1(r) (December, 2006) Notes

NOTE-3-2 -- ACL2 Version 3.2 (April, 2007) Notes

NOTE-3-2(R) -- ACL2 Version 3.2(r) (April, 2007) Notes

NOTE-3-2-1 -- ACL2 Version 3.2.1 (June, 2007) Notes

NOTE-3-2-1(R) -- ACL2 Version 3.2.1(r) (June, 2007) Notes

NOTE-3-3 -- ACL2 Version 3.3 (November, 2007) Notes

NOTE-3-3(R) -- ACL2 Version 3.3(r) (November, 2007) Notes

NOTE-3-4 -- ACL2 Version 3.4 (August, 2008) Notes

NOTE-3-4(R) -- ACL2 Version 3.4(r) (August, 2008) Notes

NOTE-3-5 -- ACL2 Version 3.5 (May, 2009) Notes

NOTE-3-5(R) -- ACL2 Version 3.5(r) (May, 2009) Notes

NOTE-3-6 -- ACL2 Version 3.6 (August, 2009) Notes

NOTE-3-6(R) -- ACL2 Version 3.6(r) (August, 2009) Notes

NOTE-3-6-1 -- ACL2 Version 3.6.1 (September, 2009) Notes

NOTE-4-0 -- ACL2 Version 4.0 (July, 2010) Notes

NOTE-4-0(R) -- ACL2 Version 4.0(r) (July, 2010) Notes

NOTE-4-0-WORMHOLE-CHANGES -- how to convert calls of wormhole for Version 4.0

NOTE-4-1 -- ACL2 Version 4.1 (September, 2010) Notes

NOTE-4-1(R) -- ACL2 Version 4.1(r) (September, 2010) Notes

NOTE-4-2 -- ACL2 Version 4.2 (January, 2011) Notes

NOTE-4-2(R) -- ACL2 Version 4.2(r) (January, 2011) Notes

NOTE-4-3 -- ACL2 Version 4.3 (July, 2011) Notes

NOTE-4-3(R) -- ACL2 Version 4.3(r) (July, 2011) Notes

NOTE1 -- Acl2 Version 1.1 Notes

NOTE2 -- Acl2 Version 1.2 Notes

NOTE3 -- Acl2 Version 1.3 Notes

NOTE4 -- Acl2 Version 1.4 Notes

NOTE5 -- Acl2 Version 1.5 Notes

NOTE6 -- Acl2 Version 1.6 Notes

NOTE7 -- ACL2 Version 1.7 (released October 1994) Notes

NOTE8 -- ACL2 Version 1.8 (May, 1995) Notes

NOTE8-UPDATE -- ACL2 Version 1.8 (Summer, 1995) Notes

NOTE9 -- ACL2 Version 1.9 (Fall, 1996) Notes

NQTHM-TO-ACL2 -- ACL2 analogues of Nqthm functions and commands

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

NTH-ALIASES-TABLE -- a table used to associate names for nth/update-nth printing

NTHCDR -- final segment of a list

NU-REWRITER -- rewriting NTH/UPDATE-NTH expressions

NULL -- recognizer for the empty list

NUMBER-SUBTREES -- (number-subtrees x) returns the number of distinct subtrees of X, in the
sense of equal


NUMERATOR -- dividend of a ratio in lowest terms

Name the Formula Above -- Name the Formula Above

Nontautological Subgoals -- Prover output omits some details

Numbers in ACL2 -- Numbers in ACL2



O

O-FINP -- recognizes if an ordinal is finite

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

O-FIRST-EXPT -- the first exponent of an ordinal

O-INFP -- recognizes if an ordinal is infinite

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

O-RST -- returns the rest of an infinite ordinal

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

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

O> -- the greater-than relation for the ordinals

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

OBDD -- ordered binary decision diagrams with rewriting

OBSERVATION -- print an observation

OBSERVATION-CW -- See observation.

ODDP -- test whether an integer is odd

OK-IF -- conditional exit from break-rewrite

OOPS -- undo a :u or :ubt

OPEN-INPUT-CHANNEL -- See io.

OPEN-INPUT-CHANNEL-P -- See io.

OPEN-OUTPUT-CHANNEL -- See io.

OPEN-OUTPUT-CHANNEL! -- when trust tags are needed to open output channels

OPEN-OUTPUT-CHANNEL-P -- See io.

OPEN-TRACE-FILE -- redirect trace output to a file

OPTIMIZE -- See declare.

OR -- disjunction

ORDINALS -- ordinals in ACL2

OTF-FLG -- pushing all the initial subgoals

OTHER -- other commonly used top-level functions

OVERRIDE-HINTS -- a list of hints given priority in every proof attempt

On the Naming of Subgoals -- On the Naming of Subgoals

Other Requirements -- Other Requirements

Overview of the Expansion of ENDP in the Base Case -- Overview of the Expansion of ENDP in the Base Case

Overview of the Expansion of ENDP in the Induction Step -- Overview of the Expansion of ENDP in the Induction Step

Overview of the Final Simplification in the Base Case -- Overview of the Final Simplification in the Base Case

Overview of the Proof of a Trivial Consequence -- Overview of the Proof of a Trivial Consequence

Overview of the Simplification of the Base Case to T -- Overview of the Simplification of the Base Case to T

Overview of the Simplification of the Induction Conclusion -- Overview of the Simplification of the Induction Conclusion

Overview of the Simplification of the Induction Step to T -- Overview of the Simplification of the Induction Step to T



P

P! -- to pop up (at least) one level of ACL2's command loop

PACKAGE-REINCARNATION-IMPORT-RESTRICTIONS -- re-defining undone defpkgs

PAIRLIS -- See pairlis$

PAIRLIS$ -- zipper together two lists

PAND -- parallel, Boolean version of and

PARALLEL -- evaluating forms in parallel

PARALLEL-PUSHING-OF-SUBGOALS-FOR-INDUCTION -- consequences of how parallelized proofs of subgoals are pushed for induction

PARALLELISM -- experimental extension for evaluating forms in parallel

PARALLELISM-AT-THE-TOP-LEVEL -- parallel evaluation in the ACL2 top-level loop

PARALLELISM-BUILD -- building an ACL2 executable with parallel evaluation enabled

PARALLELISM-PERFORMANCE -- performance issues for parallel evaluation

PARALLELISM-TUTORIAL -- a tutorial on how to use the parallelism library.

PARGS -- parallel evaluation of arguments in a function call

PATHNAME -- introduction to filename conventions in ACL2

PBT -- print the commands back through a command descriptor

PC -- print the command described by a command descriptor

PCB -- print the command block described by a command descriptor

PCB! -- print in full the command block described by a command descriptor

PCS -- print the sequence of commands between two command descriptors

PE -- print the events named by a logical name

PE! -- deprecated (see pe)

PEEK-CHAR$ -- See io.

PF -- print the formula corresponding to the given name

PKG-IMPORTS -- list of symbols imported into a given package

PKG-WITNESS -- return a specific symbol in the indicated package

PL -- print the rules for the given name or term

PL2 -- print rule(s) for the given form

PLET -- parallel version of let

PLUSP -- test whether a number is positive

POR -- parallel, Boolean version of or

PORTCULLIS -- the gate guarding the entrance to a certified book

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

POSITION-EQ -- See position.

POSITION-EQUAL -- See position.

POSP -- a recognizer for the positive integers

POST-INDUCTION-KEY-CHECKPOINTS -- reading post-induction key checkpoints

PPROGN -- evaluate a sequence of forms that return state

PR -- print the rules stored by the event with the given name

PR! -- print rules stored by the command with a given command descriptor

PRACTICE-FORMULATING-STRONG-RULES -- a few simple checkpoints suggesting strong rules

PRACTICE-FORMULATING-STRONG-RULES-1 -- rules suggested by (TRUE-LISTP (APPEND (FOO A) (BAR B)))

PRACTICE-FORMULATING-STRONG-RULES-2 -- rules suggested by (TRUE-LISTP (REV (FOO A)))

PRACTICE-FORMULATING-STRONG-RULES-3 -- rules suggested by (MEMBER (FOO A) (APPEND (BAR B) (MUM C)))

PRACTICE-FORMULATING-STRONG-RULES-4 -- rules suggested by (SUBSETP (APPEND (FOO A) (BAR B)) (MUM C))

PRACTICE-FORMULATING-STRONG-RULES-5 -- rules suggested by (SUBSETP (FOO A) (APPEND (BAR B) (MUM C)))

PRACTICE-FORMULATING-STRONG-RULES-6 -- rules suggested by (MEMBER (FOO A) (NATS-BELOW (BAR B)))

PRINC$ -- print a string

PRINT-CONTROL -- advanced controls of ACL2 printing

PRINT-DOC-START-COLUMN -- printing the one-liner

PRINT-GV -- print a form whose evaluation caused a guard violation

PRINT-OBJECT$ -- See io.

PRINTING-TO-STRINGS -- printing to strings instead of files or standard output

PROFILE -- turn on profiling for one function

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

PROGN -- evaluate some events

PROGN! -- evaluate some forms, not necessarily events

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

PROGRAM -- to set the default defun-mode to :program

PROGRAMMING -- built-in ACL2 functions

PROGRAMMING-KNOWLEDGE-TAKEN-FOR-GRANTED -- background knowledge in ACL2 programming for theorem prover tutorial

PROMPT -- the prompt printed by ld

PROOF-CHECKER -- support for low-level interaction

PROOF-CHECKER-COMMANDS -- list of commands for the proof-checker

PROOF-OF-WELL-FOUNDEDNESS -- a proof that o< is well-founded on o-ps

PROOF-TREE -- proof tree displays

PROOF-TREE-BINDINGS -- using emacs with proof trees

PROOF-TREE-DETAILS -- proof tree details not covered elsewhere

PROOF-TREE-EMACS -- using emacs with proof trees

PROOF-TREE-EXAMPLES -- proof tree example

PROOFS-CO -- the proofs character output channel

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

PROPS -- print the ACL2 properties on a symbol

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

PSO -- show the most recently saved output

PSO! -- show the most recently saved output, including proof-tree output

PSOG -- show the most recently saved output in gag-mode

PSTACK -- seeing what is the prover up to

PUFF -- replace a compound command by its immediate subevents

PUFF* -- replace a compound command by its subevents

PUSH-UNTOUCHABLE -- add name or list of names to the list of untouchable symbols

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

PUT-ASSOC-EQ -- See put-assoc.

PUT-ASSOC-EQL -- See put-assoc.

PUT-ASSOC-EQUAL -- See put-assoc.

PUTPROP -- update fast property lists

Pages Written Especially for the Tours -- Pages Written Especially for the Tours

Perhaps -- Perhaps

Popping out of an Inductive Proof -- Popping out of an Inductive Proof

Proving Theorems about Models -- Proving Theorems about Models



Q

Q -- quit ACL2 (type :q) -- reenter with (lp)

QUANTIFIER-TUTORIAL -- A Beginner's Guide to Reasoning about Quantification in ACL2

QUANTIFIERS -- issues about quantification in ACL2

QUANTIFIERS-USING-DEFUN-SK -- quantification example

QUANTIFIERS-USING-DEFUN-SK-EXTENDED -- quantification example with details

QUANTIFIERS-USING-RECURSION -- recursion for implementing quantification

QUIT -- quit entirely out of Lisp

QUOTE -- create a constant



R

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

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

RANDOM$ -- obtain a random value

RASSOC -- look up value in association list

RASSOC-EQ -- See rassoc.

RASSOC-EQUAL -- See rassoc.

RATIONAL-LISTP -- recognizer for a true list of rational numbers

RATIONALP -- recognizer for rational numbers (ratios and integers)

READ-BYTE$ -- See io.

READ-CHAR$ -- See io.

READ-OBJECT -- See io.

REAL -- ACL2(r) support for real numbers

REAL-LISTP -- ACL2(r) recognizer for a true list of real numbers

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

REALFIX -- coerce to a real number

REALPART -- real part of a complex number

REBUILD -- a convenient way to reconstruct your old state

REDEF -- a common way to set ld-redefinition-action

REDEF! -- a common way to set ld-redefinition-action

REDEF+ -- system hacker's redefinition command

REDEF- -- turn off system hacker's redefinition command

REDEFINED-NAMES -- to collect the names that have been redefined

REDEFINING-PROGRAMS -- an explanation of why we restrict redefinitions

REDO-FLAT -- redo on failure of a progn, encapsulate, or certify-book

REDUNDANT-EVENTS -- allowing a name to be introduced ``twice''

REFINEMENT -- record that one equivalence relation refines another

RELEASE-NOTES -- pointers to what has changed

REM -- remainder using truncate

REMOVE -- remove all occurrences

REMOVE-BINOP -- remove the association of a binary function name with a macro name

REMOVE-CUSTOM-KEYWORD-HINT -- remove a custom keyword hint

REMOVE-DEFAULT-HINTS -- remove from the default hints

REMOVE-DEFAULT-HINTS! -- remove from the default hints non-locally

REMOVE-DIVE-INTO-MACRO -- removes association of proof-checker diving function with macro name

REMOVE-DUPLICATES -- remove duplicates from a string or a list

REMOVE-DUPLICATES-EQ -- See remove-duplicates.

REMOVE-DUPLICATES-EQUAL -- See remove-duplicates.

REMOVE-EQ -- See remove.

REMOVE-EQUAL -- See remove.

REMOVE-INVISIBLE-FNS -- make some unary functions no longer invisible

REMOVE-MACRO-ALIAS -- remove the association of a function name with a macro name

REMOVE-NTH-ALIAS -- remove a symbol alias for printing of nth/update-nth terms

REMOVE-OVERRIDE-HINTS -- delete from the list of override-hints

REMOVE-OVERRIDE-HINTS! -- delete non-locally from the list of override-hints

REMOVE-RAW-ARITY -- remove arity information for raw mode

REMOVE-UNTOUCHABLE -- remove names from lists of untouchable symbols

REMOVE1 -- remove first occurrences, testing using eql

REMOVE1-EQ -- See remove1.

REMOVE1-EQUAL -- See remove1.

REORDER -- hints keyword :REORDER

RESET-FC-REPORTING -- reset the forward-chaining tracking state to its initial configuration

RESET-KILL-RING -- save memory by resetting and perhaps resizing the kill ring used by oops

RESET-LD-SPECIALS -- restores initial settings of the ld specials

RESET-PREHISTORY -- reset the prehistory

RESET-PRINT-CONTROL -- See print-control.

RESIZE-LIST -- list resizer in support of stobjs

REST -- rest (cdr) of the list

RESTRICT -- hints keyword :RESTRICT

RETRIEVE -- re-enter a (specified) proof-checker state

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

RETURN-LAST-TABLE -- install special raw Lisp behavior

REVAPPEND -- concatentate the reverse of one list to another

REVERSE -- reverse a list or string

REWRITE -- make some :rewrite rules (possibly conditional ones)

REWRITE-STACK-LIMIT -- limiting the stack depth of the ACL2 rewriter

RFIX -- coerce to a rational number

ROUND -- division returning an integer by rounding off

RULE-CLASSES -- adding rules to the data base

RULE-NAMES -- How rules are named.

RULER-EXTENDERS -- control for ACL2's termination and induction analyses

RUNE -- a rule name

Revisiting the Admission of App -- Revisiting the Admission of App

Rewrite Rules are Generated from DEFTHM Events -- Rewrite Rules are Generated from DEFTHM Events

Running Models -- Running Models



S

SAVE-EXEC -- save an executable image and (for most Common Lisps) a wrapper script

SAVING-AND-RESTORING -- saving and restoring your logical state

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

SECOND -- second member of the list

SET-BACKCHAIN-LIMIT -- sets the backchain-limit used by the type-set and rewriting mechanisms

SET-BODY -- set the definition body

SET-BOGUS-DEFUN-HINTS-OK -- allow unnecessary ``mutual recursion''

SET-BOGUS-MUTUAL-RECURSION-OK -- allow unnecessary ``mutual recursion''

SET-CASE-SPLIT-LIMITATIONS -- set the case-split-limitations

SET-CBD -- to set the connected book directory

SET-CHECKPOINT-SUMMARY-LIMIT -- control printing of key checkpoints upon a proof's failure

SET-COMPILE-FNS -- have each function compiled as you go along.

SET-COMPILER-ENABLED -- See compilation.

SET-DEBUGGER-ENABLE -- control whether Lisp errors and breaks invoke the Lisp debugger

SET-DEFAULT-BACKCHAIN-LIMIT -- sets the default backchain-limit used when admitting a rule

SET-DEFAULT-HINTS -- set the default hints

SET-DEFAULT-HINTS! -- set the default hints non-locally

SET-DEFERRED-TTAG-NOTES -- modify the verbosity of TTAG NOTE printing

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

SET-DIFFERENCE-EQ -- See set-difference$.

SET-DIFFERENCE-EQUAL -- See set-difference$.

SET-DIFFERENCE-THEORIES -- difference of two theories

SET-ENFORCE-REDUNDANCY -- require most events to be redundant

SET-EVISC-TUPLE -- control suppression of details when printing

SET-FC-CRITERIA -- to set the tracking criteria for forward chaining reports

SET-FC-REPORT-ON-THE-FLY -- to determine when forward-chaining reports are printed

SET-FMT-HARD-RIGHT-MARGIN -- set the right margin for formatted output

SET-FMT-SOFT-RIGHT-MARGIN -- set the soft right margin for formatted output

SET-GAG-MODE -- modify the nature of proof output

SET-GUARD-CHECKING -- control checking guards during execution of top-level forms

SET-IGNORE-DOC-STRING-ERROR -- allow ill-formed documentation strings

SET-IGNORE-OK -- allow unused formals and locals without an ignore or ignorable declaration

SET-INHIBIT-OUTPUT-LST -- control output

SET-INHIBIT-WARNINGS -- control warnings

SET-INHIBITED-SUMMARY-TYPES -- control which parts of the summary are printed

SET-INVISIBLE-FNS-TABLE -- set the invisible functions table

SET-IPRINT -- control whether abbreviated output can be read back in

SET-IRRELEVANT-FORMALS-OK -- allow irrelevant formals in definitions

SET-LD-KEYWORD-ALIASES -- See ld-keyword-aliases.

SET-LD-REDEFINITION-ACTION -- See ld-redefinition-action.

SET-LD-SKIP-PROOFS -- See set-ld-skip-proofsp.

SET-LD-SKIP-PROOFSP -- See ld-skip-proofsp.

SET-LET*-ABSTRACTION -- See set-let*-abstractionp.

SET-LET*-ABSTRACTIONP -- to shorten many prettyprinted clauses

SET-MATCH-FREE-DEFAULT -- provide default for :match-free in future rules

SET-MATCH-FREE-ERROR -- control error vs. warning when :match-free is missing

SET-MEASURE-FUNCTION -- set the default measure function symbol

SET-NON-LINEAR -- See set-non-linearp.

SET-NON-LINEARP -- to turn on or off non-linear arithmetic reasoning

SET-NU-REWRITER-MODE -- to turn on and off the nu-rewriter

SET-OVERRIDE-HINTS -- set the override-hints

SET-OVERRIDE-HINTS! -- set the override-hints non-locally

SET-PARALLEL-EVALUATION -- enabling parallel evaluation for four of the parallelism primitives

SET-PRINT-BASE -- control radix in which number are printed

SET-PRINT-CASE -- control whether symbols are printed in upper case or in lower case

SET-PRINT-CIRCLE -- See print-control.

SET-PRINT-CLAUSE-IDS -- cause subgoal numbers to be printed when 'prove output is inhibited

SET-PRINT-ESCAPE -- See print-control.

SET-PRINT-LENGTH -- See print-control.

SET-PRINT-LEVEL -- See print-control.

SET-PRINT-LINES -- See print-control.

SET-PRINT-RADIX -- See print-control.

SET-PRINT-READABLY -- See print-control.

SET-PRINT-RIGHT-MARGIN -- See print-control.

SET-PROVER-STEP-LIMIT -- sets the step-limit used by the ACL2 prover at the top level only

SET-RAW-MODE -- enter or exit ``raw mode,'' a raw Lisp environment

SET-RAW-MODE-ON! -- enter ``raw mode,'' a raw Lisp environment

SET-RAW-PROOF-FORMAT -- print runes as lists in proof output from simplification

SET-REWRITE-STACK-LIMIT -- Sets the rewrite stack depth used by the rewriter

SET-RULER-EXTENDERS -- See ruler-extenders.

SET-RW-CACHE-STATE -- set the default rw-cache-state

SET-RW-CACHE-STATE! -- set the default rw-cache-state non-locally

SET-SAVED-OUTPUT -- save proof output for later display with :pso or :pso!

SET-STATE-OK -- allow the use of STATE as a formal parameter

SET-TAINTED-OK -- See set-tainted-okp.

SET-TAINTED-OKP -- control output

SET-TRACE-EVISC-TUPLE -- set the trace evisc tuple

SET-VERIFY-GUARDS-EAGERNESS -- the eagerness with which guard verification is tried.

SET-WATERFALL-PARALLELISM -- for ACL2(p): configuring the parallel execution of the waterfall

SET-WATERFALL-PRINTING -- for ACL2(p): configuring the printing that occurs within the parallelized waterfall

SET-WELL-FOUNDED-RELATION -- set the default well-founded relation

SET-WORMHOLE-DATA -- sets the wormhole data object in a wormhole status object

SET-WORMHOLE-ENTRY-CODE -- sets the wormhole entry code in a wormhole status object

SET-WRITE-ACL2X -- cause certify-book to write out a .acl2x file

SETENV$ -- set an environment variable

SEVENTH -- seventh member of the list

SHARP-BANG-READER -- package prefix that is not restricted to symbols

SHARP-COMMA-READER -- DEPRECATED read-time evaluation of constants

SHARP-DOT-READER -- read-time evaluation of constants

SHOW-ACCUMULATED-PERSISTENCE -- See accumulated-persistence.

SHOW-BDD -- inspect failed BDD proof attempts

SHOW-BODIES -- show the potential definition bodies

SHOW-CUSTOM-KEYWORD-HINT-EXPANSION -- print out custom keyword hints when they are expanded

SHOW-FC-CRITERIA -- print the forward-chaining tracking criteria

SIGNATURE -- how to specify the arity of a constrained function

SIGNUM -- indicator for positive, negative, or zero

SIMPLE -- :definition and :rewrite rules used in preprocessing

SIXTH -- sixth member of the list

SKIP-PROOFS -- skip proofs for a given form -- a quick way to introduce unsoundness

SLOW-ALIST-WARNING -- warnings issued when fast-alists are used inefficiently

SLOW-ARRAY-WARNING -- a warning or error issued when arrays are used inefficiently

SOLUTION-TO-SIMPLE-EXAMPLE -- solution to a simple example

SPEC-MV-LET -- modification of mv-let supporting speculative and parallel execution

SPECIAL-CASES-FOR-REWRITE-RULES -- convenient short forms for rewrite rule formulas

SPECIFIC-KINDS-OF-FORMULAS-AS-REWRITE-RULES -- advice about how to handle commonly occurring formulas as rewrite rules

SPECIOUS-SIMPLIFICATION -- nonproductive proof steps

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

STANDARD-CHAR-P -- recognizer for standard characters

STANDARD-CO -- the character output channel to which ld prints

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

STANDARD-PART -- ACL2(r) function mapping limited numbers to standard numbers

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

STANDARDP -- ACL2(r) recognizer for standard objects

START-PROOF-TREE -- start displaying proof trees during proofs

STARTUP -- How to start using ACL2; the ACL2 command loop

STATE -- the von Neumannesque ACL2 state object

STOBJ -- single-threaded objects or ``von Neumann bottlenecks''

STOBJ-EXAMPLE-1 -- an example of the use of single-threaded objects

STOBJ-EXAMPLE-1-DEFUNS -- the defuns created by the counters stobj

STOBJ-EXAMPLE-1-IMPLEMENTATION -- the implementation of the counters stobj

STOBJ-EXAMPLE-1-PROOFS -- some proofs involving the counters stobj

STOBJ-EXAMPLE-2 -- an example of the use of arrays in single-threaded objects

STOBJ-EXAMPLE-3 -- another example of a single-threaded object

STOBJS -- xargs keyword :STOBJS

STOP-PROOF-TREE -- stop displaying proof trees during proofs

STRING -- coerce to a string

STRING-APPEND -- concatenate two strings

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

STRING-EQUAL -- string equality without regard to case

STRING-LISTP -- recognizer for a true list of strings

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

STRING< -- less-than test for strings

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

STRING> -- greater-than test for strings

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

STRINGP -- recognizer for strings

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

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

STRONG-REWRITE-RULES -- formulating good rewrite rules

SUBLIS -- substitute an alist into a tree

SUBSEQ -- subsequence of a string or list

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

SUBSETP-EQ -- See subsetp.

SUBSETP-EQUAL -- See subsetp.

SUBST -- a single substitution into a tree

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

SUBVERSIVE-INDUCTIONS -- why we restrict encapsulated recursive functions

SUBVERSIVE-RECURSIONS -- why we restrict encapsulated recursive functions

SWITCHES-PARAMETERS-AND-MODES -- a variety of ways to modify the ACL2 environment

SYMBOL-< -- less-than test for symbols

SYMBOL-ALISTP -- recognizer for association lists with symbols as keys

SYMBOL-LISTP -- recognizer for a true list of symbols

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

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

SYMBOLP -- recognizer for symbols

SYNTAX -- the syntax of ACL2 is that of Common Lisp

SYNTAXP -- attach a heuristic filter on a :rewrite, :meta, or :linear rule

SYNTAXP-EXAMPLES -- examples pertaining to syntaxp hypotheses

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

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

Subsumption of Induction Candidates in App Example -- Subsumption of Induction Candidates in App Example

Suggested Inductions in the Associativity of App Example -- Suggested Inductions in the Associativity of App Example

Symbolic Execution of Models -- Symbolic Execution of Models



T

TABLE -- user-managed tables

TAKE -- initial segment of a list

TENTH -- tenth member of the list

TERM -- the three senses of well-formed ACL2 expressions or formulas

TERM-ORDER -- the ordering relation on terms used by ACL2

TERM-TABLE -- a table used to validate meta rules

THE -- run-time type check

THE-METHOD -- how to find proofs

THEORIES -- sets of runes to enable/disable in concert

THEORY -- retrieve named theory

THEORY-FUNCTIONS -- functions for obtaining or producing theories

THEORY-INVARIANT -- user-specified invariants on theories

THIRD -- third member of the list

THM -- prove a theorem

TIDBITS -- some basic hints for using ACL2

TIME$ -- time an evaluation

TIPS -- some hints for using the ACL2 prover

TOGGLE-PC-MACRO -- change an ordinary macro command to an atomic macro, or vice-versa

TOP-LEVEL -- evaluate a top-level form as a function body

TRACE -- tracing functions in ACL2

TRACE! -- trace the indicated functions after creating an active trust tag

TRACE$ -- trace function evaluations

TRANS -- print the macroexpansion of a form

TRANS! -- print the macroexpansion of a form without single-threadedness concerns

TRANS1 -- print the one-step macroexpansion of a form

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

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

TRUNCATE -- division returning an integer by truncating toward 0

TTAGS-SEEN -- list some declared trust tags (ttags)

TTREE -- tag-trees

TUTORIAL1-TOWERS-OF-HANOI -- The Towers of Hanoi Example

TUTORIAL2-EIGHTS-PROBLEM -- The Eights Problem Example

TUTORIAL3-PHONEBOOK-EXAMPLE -- A Phonebook Specification

TUTORIAL4-DEFUN-SK-EXAMPLE -- example of quantified notions

TUTORIAL5-MISCELLANEOUS-EXAMPLES -- miscellaneous ACL2 examples

TYPE -- See declare.

TYPE-PRESCRIPTION -- make a rule that specifies the type of a term

TYPE-SET -- how type information is encoded in ACL2

TYPE-SET-INVERTER -- exhibit a new decoding for an ACL2 type-set

TYPE-SPEC -- type specifiers in declarations

The Admission of App -- The Admission of App

The Associativity of App -- The Associativity of App

The Base Case in the App Example -- The Base Case in the App Example

The End of the Flying Tour -- The End of the Flying Tour

The End of the Proof of the Associativity of App -- The End of the Proof of the Associativity of App

The End of the Walking Tour -- The End of the Walking Tour

The Event Summary -- The Event Summary

The Expansion of ENDP in the Induction Step (Step 0) -- The Expansion of ENDP in the Induction Step (Step 0)

The Expansion of ENDP in the Induction Step (Step 1) -- The Expansion of ENDP in the Induction Step (Step 1)

The Expansion of ENDP in the Induction Step (Step 2) -- The Expansion of ENDP in the Induction Step (Step 2)

The Falling Body Model -- The Falling Body Model

The Final Simplification in the Base Case (Step 0) -- the Final Simplification in the Base Case (Step 0)

The Final Simplification in the Base Case (Step 1) -- the Final Simplification in the Base Case (Step 1)

The Final Simplification in the Base Case (Step 2) -- the Final Simplification in the Base Case (Step 2)

The Final Simplification in the Base Case (Step 3) -- the Final Simplification in the Base Case (Step 3)

The First Application of the Associativity Rule -- The First Application of the Associativity Rule

The Induction Scheme Selected for the App Example -- The Induction Scheme Selected for the App Example

The Induction Step in the App Example -- The Induction Step in the App Example

The Instantiation of the Induction Scheme -- The Instantiation of the Induction Scheme

The Justification of the Induction Scheme -- The Justification of the Induction Scheme

The Proof of the Associativity of App -- The Proof of the Associativity of App

The Q.E.D. Message -- The Q.E.D. Message

The Rules used in the Associativity of App Proof -- The Rules used in the Associativity of App Proof

The Simplification of the Induction Conclusion (Step 0) -- the Simplification of the Induction Conclusion (Step 0)

The Simplification of the Induction Conclusion (Step 1) -- the Simplification of the Induction Conclusion (Step 1)

The Simplification of the Induction Conclusion (Step 10) -- the Simplification of the Induction Conclusion (Step 10)

The Simplification of the Induction Conclusion (Step 11) -- the Simplification of the Induction Conclusion (Step 11)

The Simplification of the Induction Conclusion (Step 12) -- the Simplification of the Induction Conclusion (Step 12)

The Simplification of the Induction Conclusion (Step 2) -- the Simplification of the Induction Conclusion (Step 2)

The Simplification of the Induction Conclusion (Step 3) -- the Simplification of the Induction Conclusion (Step 3)

The Simplification of the Induction Conclusion (Step 4) -- the Simplification of the Induction Conclusion (Step 4)

The Simplification of the Induction Conclusion (Step 5) -- the Simplification of the Induction Conclusion (Step 5)

The Simplification of the Induction Conclusion (Step 6) -- the Simplification of the Induction Conclusion (Step 6)

The Simplification of the Induction Conclusion (Step 7) -- the Simplification of the Induction Conclusion (Step 7)

The Simplification of the Induction Conclusion (Step 8) -- the Simplification of the Induction Conclusion (Step 8)

The Simplification of the Induction Conclusion (Step 9) -- the Simplification of the Induction Conclusion (Step 9)

The Summary of the Proof of the Trivial Consequence -- The Summary of the Proof of the Trivial Consequence

The Theorem that App is Associative -- The Theorem that App is Associative

The Time Taken to do the Associativity of App Proof -- The Time Taken to do the Associativity of App Proof

The Tours -- The Tours

The WARNING about the Trivial Consequence -- The WARNING about the Trivial Consequence



U

U -- undo last command, without a query

UBT -- undo the commands back through a command descriptor

UBT! -- undo commands, without a query or an error

UBT-PREHISTORY -- undo the commands back through the last reset-prehistory event

UBU -- undo the commands back up to (not including) a command descriptor

UBU! -- undo commands, without a query or an error

UNARY-- -- arithmetic negation function

UNARY-/ -- reciprocal function

UNCERTIFIED-BOOKS -- invalid certificates and uncertified books

UNION$ -- elements of one list that are not elements of another

UNION-EQ -- See union$.

UNION-EQUAL -- See union$.

UNION-THEORIES -- union two theories

UNIVERSAL-THEORY -- all rules as of logical name

UNMEMOIZE -- turn off memoization for the specified function

UNMONITOR -- to stop monitoring a rule name

UNSAVE -- remove a proof-checker state

UNSUPPORTED-WATERFALL-PARALLELISM-FEATURES -- proof features not supported with waterfall-parallelism enabled

UNTRACE$ -- untrace functions

UNTRANSLATE -- See user-defined-functions-table.

UPDATE-NTH -- modify a list by putting the given value at the given position

UPPER-CASE-P -- recognizer for upper case characters

USE -- hints keyword :USE

USER-DEFINED-FUNCTIONS-TABLE -- an advanced table used to replace certain system functions

USING-COMPUTED-HINTS -- how to use computed hints

USING-COMPUTED-HINTS-1 -- Driving Home the Basics

USING-COMPUTED-HINTS-2 -- One Hint to Every Top-Level Goal in a Forcing Round

USING-COMPUTED-HINTS-3 -- Hints as a Function of the Goal (not its Name)

USING-COMPUTED-HINTS-4 -- Computing the Hints

USING-COMPUTED-HINTS-5 -- Debugging Computed Hints

USING-COMPUTED-HINTS-6 -- Using the computed-hint-replacement feature

USING-COMPUTED-HINTS-7 -- Using the stable-under-simplificationp flag

USING-COMPUTED-HINTS-8 -- Some Final Comments

USING-TABLES-EFFICIENTLY -- Notes on how to use tables efficiently

Undocumented Topic -- Undocumented Topic

Using the Associativity of App to Prove a Trivial Consequence -- Using the Associativity of App to Prove a Trivial Consequence



V

VALUE-TRIPLE -- compute a value, optionally checking that it is not nil

VERBOSE-PSTACK -- seeing what is the prover up to (for advanced users)

VERIFY -- enter the interactive proof checker

VERIFY-GUARDS -- verify the guards of a function

VERIFY-GUARDS-EAGERNESS -- See set-verify-guards-eagerness.

VERIFY-GUARDS-FORMULA -- view the guard proof obligation, without proving it

VERIFY-TERMINATION -- convert a function from :program mode to :logic mode

VERSION -- ACL2 Version Number



W

WALKABOUT -- explore an ACL2 cons tree

WATERFALL -- See hints-and-the-waterfall.

WATERFALL-PARALLELISM -- for ACL2(p): configuring the parallel execution of the waterfall

WATERFALL-PRINTING -- for ACL2(p): configuring the printing within the parallelized waterfall

WELL-FOUNDED-RELATION -- show that a relation is well-founded on a set

WET -- evaluate a form and print subsequent error trace

WHY-BRR -- an explanation of why ACL2 has an explicit brr mode

WITH-GUARD-CHECKING -- suppressing or enable guard-checking for a form

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

WITH-LOCAL-STATE -- locally bind state

WITH-LOCAL-STOBJ -- locally bind a single-threaded object

WITH-OUTPUT -- suppressing or turning on specified output for an event

WITH-PROVER-STEP-LIMIT -- limit the number of steps for proofs

WITH-PROVER-TIME-LIMIT -- limit the time for proofs

WITHOUT-EVISC -- print output in full

WORLD -- ACL2 property lists and the ACL2 logical data base

WORMHOLE -- ld without state -- a short-cut to a parallel universe

WORMHOLE-DATA -- determines the wormhole data object from a wormhole status object

WORMHOLE-ENTRY-CODE -- determines the wormhole entry code from a wormhole status object

WORMHOLE-EVAL -- state-saving without state -- a short-cut to a parallel universe

WORMHOLE-IMPLEMENTATION -- notes on how wormholes are implemented

WORMHOLE-P -- predicate to determine if you are inside a wormhole

WORMHOLE-STATUSP -- predicate recognizing well-formed wormhole status object

WRITE-BYTE$ -- See io.

What Is ACL2(Q) -- What Is ACL2?

What is Required of the User(Q) -- What is Required of the User?

What is a Mathematical Logic(Q) -- What is a Mathematical Logic?

What is a Mechanical Theorem Prover(Q) -- What is a Mechanical Theorem Prover?

What is a Mechanical Theorem Prover(Q) (cont) -- What is a Mechanical Theorem Prover? (cont)



X

XARGS -- giving hints to defun

XOR -- logical ``exclusive or''



Y

You Must Think about the Use of a Formula as a Rule -- You Must Think about the Use of a Formula as a Rule



Z

ZERO-TEST-IDIOMS -- how to test for 0

ZEROP -- test an acl2-number against 0

ZIP -- testing an ``integer'' against 0

ZP -- testing a ``natural'' against 0

ZPF -- testing a nonnegative fixnum against 0



ACL2-PC::

ACL2-PC::= -- (atomic macro)
attempt an equality (or equivalence) substitution


ACL2-PC::ACL2-WRAP -- (macro)
same as (lisp x)


ACL2-PC::ADD-ABBREVIATION -- (primitive)
add an abbreviation


ACL2-PC::BASH -- (atomic macro)
call the ACL2 theorem prover's simplifier


ACL2-PC::BDD -- (atomic macro)
prove the current goal using bdds


ACL2-PC::BK -- (atomic macro)
move backward one argument in the enclosing term


ACL2-PC::BOOKMARK -- (macro)
insert matching ``bookends'' comments


ACL2-PC::CASESPLIT -- (primitive)
split into two cases


ACL2-PC::CG -- (macro)
change to another goal.


ACL2-PC::CHANGE-GOAL -- (primitive)
change to another goal.


ACL2-PC::CL-PROC -- (macro)
same as clause-processor


ACL2-PC::CLAIM -- (atomic macro)
add a new hypothesis


ACL2-PC::CLAUSE-PROCESSOR -- (atomic macro)
use a clause-processor


ACL2-PC::COMM -- (macro)
display instructions from the current interactive session


ACL2-PC::COMMANDS -- (macro)
display instructions from the current interactive session


ACL2-PC::COMMENT -- (primitive)
insert a comment


ACL2-PC::CONTRADICT -- (macro)
same as contrapose


ACL2-PC::CONTRAPOSE -- (primitive)
switch a hypothesis with the conclusion, negating both


ACL2-PC::DEMOTE -- (primitive)
move top-level hypotheses to the conclusion


ACL2-PC::DIVE -- (primitive)
move to the indicated subterm


ACL2-PC::DO-ALL -- (macro)
run the given instructions


ACL2-PC::DO-ALL-NO-PROMPT -- (macro)
run the given instructions, halting once there is a ``failure''


ACL2-PC::DO-STRICT -- (macro)
run the given instructions, halting once there is a ``failure''


ACL2-PC::DROP -- (primitive)
drop top-level hypotheses


ACL2-PC::DV -- (atomic macro)
move to the indicated subterm


ACL2-PC::ELIM -- (atomic macro)
call the ACL2 theorem prover's elimination process


ACL2-PC::EQUIV -- (primitive)
attempt an equality (or congruence-based) substitution


ACL2-PC::EX -- (macro)
exit after possibly saving the state


ACL2-PC::EXIT -- (meta)
exit the interactive proof-checker


ACL2-PC::EXPAND -- (primitive)
expand the current function call without simplification


ACL2-PC::FAIL -- (macro)
cause a failure


ACL2-PC::FINISH -- (macro)
require completion of instructions; save error if inside :hints


ACL2-PC::FORWARDCHAIN -- (atomic macro)
forward chain from an implication in the hyps


ACL2-PC::FREE -- (atomic macro)
create a ``free variable''


ACL2-PC::GENERALIZE -- (primitive)
perform a generalization


ACL2-PC::GOALS -- (macro)
list the names of goals on the stack


ACL2-PC::HELP -- (macro)
proof-checker help facility


ACL2-PC::HELP! -- (macro)
proof-checker help facility


ACL2-PC::HELP-LONG -- (macro)
same as help!


ACL2-PC::HYPS -- (macro)
print the hypotheses


ACL2-PC::ILLEGAL -- (macro)
illegal instruction


ACL2-PC::IN-THEORY -- (primitive)
set the current proof-checker theory


ACL2-PC::INDUCT -- (atomic macro)
generate subgoals using induction


ACL2-PC::LEMMAS-USED -- (macro)
print the runes (definitions, lemmas, ...) used


ACL2-PC::LISP -- (meta)
evaluate the given form in Lisp


ACL2-PC::MORE -- (macro)
proof-checker help facility


ACL2-PC::MORE! -- (macro)
proof-checker help facility


ACL2-PC::NEGATE -- (macro)
run the given instructions, and ``succeed'' if and only if they ``fail''


ACL2-PC::NIL -- (macro)
used for interpreting control-d


ACL2-PC::NOISE -- (meta)
run instructions with output


ACL2-PC::NX -- (atomic macro)
move forward one argument in the enclosing term


ACL2-PC::ORELSE -- (macro)
run the first instruction; if (and only if) it ``fails'', run the
second


ACL2-PC::P -- (macro)
prettyprint the current term


ACL2-PC::P-TOP -- (macro)
prettyprint the conclusion, highlighting the current term


ACL2-PC::PP -- (macro)
prettyprint the current term


ACL2-PC::PRINT -- (macro)
print the result of evaluating the given form


ACL2-PC::PRINT-ALL-CONCS -- (macro)
print all the conclusions of (as yet unproved) goals


ACL2-PC::PRINT-ALL-GOALS -- (macro)
print all the (as yet unproved) goals


ACL2-PC::PRINT-MAIN -- (macro)
print the original goal


ACL2-PC::PRO -- (atomic macro)
repeatedly apply promote


ACL2-PC::PROMOTE -- (primitive)
move antecedents of conclusion's implies term to top-level
hypotheses


ACL2-PC::PROTECT -- (macro)
run the given instructions, reverting to existing state upon
failure


ACL2-PC::PROVE -- (primitive)
call the ACL2 theorem prover to prove the current goal


ACL2-PC::PSO -- (macro)
print the most recent proof attempt from inside the proof-checker


ACL2-PC::PSO! -- (macro)
print the most recent proof attempt from inside the proof-checker


ACL2-PC::PSOG -- (macro)
print the most recent proof attempt from inside the proof-checker


ACL2-PC::PUT -- (macro)
substitute for a ``free variable''


ACL2-PC::QUIET -- (meta)
run instructions without output


ACL2-PC::R -- (macro)
same as rewrite


ACL2-PC::REDUCE -- (atomic macro)
call the ACL2 theorem prover's simplifier


ACL2-PC::REDUCE-BY-INDUCTION -- (macro)
call the ACL2 prover without induction, after going into
induction


ACL2-PC::REMOVE-ABBREVIATIONS -- (primitive)
remove one or more abbreviations


ACL2-PC::REPEAT -- (macro)
repeat the given instruction until it ``fails''


ACL2-PC::REPEAT-REC -- (macro)
auxiliary to repeat


ACL2-PC::REPLAY -- (macro)
replay one or more instructions


ACL2-PC::RESTORE -- (meta)
remove the effect of an UNDO command


ACL2-PC::RETAIN -- (atomic macro)
drop all but the indicated top-level hypotheses


ACL2-PC::RETRIEVE -- (macro)
re-enter the proof-checker


ACL2-PC::REWRITE -- (primitive)
apply a rewrite rule


ACL2-PC::RUN-INSTR-ON-GOAL -- (macro)
auxiliary to THEN


ACL2-PC::RUN-INSTR-ON-NEW-GOALS -- (macro)
auxiliary to then


ACL2-PC::RUNES -- (macro)
print the runes (definitions, lemmas, ...) used


ACL2-PC::S -- (primitive)
simplify the current subterm


ACL2-PC::S-PROP -- (atomic macro)
simplify propositionally


ACL2-PC::SAVE -- (macro)
save the proof-checker state (state-stack)


ACL2-PC::SEQUENCE -- (meta)
run the given list of instructions according to a multitude of
options


ACL2-PC::SHOW-ABBREVIATIONS -- (macro)
display the current abbreviations


ACL2-PC::SHOW-REWRITES -- (macro)
display the applicable rewrite rules


ACL2-PC::SHOW-TYPE-PRESCRIPTIONS -- (macro)
display the applicable type-prescription rules


ACL2-PC::SKIP -- (macro)
``succeed'' without doing anything


ACL2-PC::SL -- (atomic macro)
simplify with lemmas


ACL2-PC::SPLIT -- (atomic macro)
split the current goal into cases


ACL2-PC::SR -- (macro)
same as SHOW-REWRITES


ACL2-PC::ST -- (macro)
same as SHOW-TYPE-PRESCRIPTIONS


ACL2-PC::SUCCEED -- (macro)
run the given instructions, and ``succeed''


ACL2-PC::TH -- (macro)
print the top-level hypotheses and the current subterm


ACL2-PC::THEN -- (macro)
apply one instruction to current goal and another to new subgoals


ACL2-PC::TOP -- (atomic macro)
move to the top of the goal


ACL2-PC::TYPE-ALIST -- (macro)
display the type-alist from the current context


ACL2-PC::UNDO -- (meta)
undo some instructions


ACL2-PC::UNSAVE -- (macro)
remove a proof-checker state


ACL2-PC::UP -- (primitive)
move to the parent (or some ancestor) of the current subterm


ACL2-PC::USE -- (atomic macro)
use a lemma instance


ACL2-PC::WRAP -- (atomic macro)
execute the indicated instructions and combine all the new goals


ACL2-PC::WRAP-INDUCT -- (atomic macro)
same as induct, but create a single goal


ACL2-PC::WRAP1 -- (primitive)
combine goals into a single goal


ACL2-PC::X -- (atomic macro)
expand and (maybe) simplify function call at the current subterm


ACL2-PC::X-DUMB -- (atomic macro)
expand function call at the current subterm, without simplifying