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::
* -- 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
+ -- 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 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
ABORT! -- to return to the top-level of ACL2's command loop
ABS -- the absolute value of a real number
ACCUMULATED-PERSISTENCE -- to get statistics on which runes are being tried
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 (continued) -- ACL2 as an Interactive Theorem Prover (continued)
ACL2 is an Untyped Language -- ACL2 is an Untyped Language
ACL2-COUNT -- a commonly used measure for justifying recursion
ACL2-CUSTOMIZATION -- customizing ACL2 for a particular user
ACL2-DEFAULTS-TABLE -- a table specifying certain defaults, e.g., the default defun-mode
ACL2-NUMBERP -- recognizer for numbers
ACL2-TUTORIAL -- tutorial introduction to ACL2
ACL2-USER -- a package the ACL2 user may prefer
ACONS -- constructor for association lists
ADD-BINOP -- associate a binary function name with a macro name
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-RAW-ARITY -- add arity information for raw mode
ADD-TO-SET-EQ -- add a symbol to a list
ADD-TO-SET-EQL -- add an object to a list
ADD-TO-SET-EQUAL -- add an object to a list
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
AND -- conjunction
APPEND -- concatenate two or more lists
APROPOS -- searching :doc and :more-doc text
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
ASSIGN -- assign to a global variable in state
ASSOC -- look up key in association list, using eql as test
ASSOC-EQ -- look up key in association list, using eq as test
ASSOC-EQUAL -- look up key in association list
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
BACKCHAIN-LIMIT -- limiting the effort expended on relieving hypotheses
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-CONTENTS -- restrictions on the forms inside books
BOOK-EXAMPLE -- how to create, certify, and use a simple book
BOOK-NAME -- conventions associated with book names
BOOKS -- files of ACL2 event forms
BOOLEANP -- recognizer for booleans
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-CLAUSES -- to build a clause into the simplifier
BUTLAST -- all but a final segment of a list
BY -- miscellaneous keyword :BY
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
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 -- miscellaneous 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-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
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
COMP -- compile some ACL2 functions
COMP-GCL -- compile some ACL2 functions leaving .c and .h files
COMPILATION -- compiling ACL2 functions
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
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
CURRENT-PACKAGE -- the package used for reading and printing
CURRENT-THEORY -- currently enabled rules as of logical name
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
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
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
DEFAXIOM -- add an axiom
DEFCHOOSE -- define a Skolem (witnessing) function
DEFCONG -- prove that one equivalence relation preserves another in a given
argument position of a given function
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
DEFINITION -- make a rule that acts like a function definition
DEFLABEL -- build a landmark and/or add a documentation topic
DEFMACRO -- define a macro
DEFPKG -- define a new symbol package
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
DEFUN -- define a function symbol
DEFUN-MODE -- determines whether a function definition is a logical act
DEFUN-MODE-CAVEAT -- functions with defun-mode of :program considered unsound
DEFUN-SK -- define a function whose body has an outermost quantifier
DEFUND -- define a function symbol and then disable it
DEFUNS -- an alternative to mutual-recursion
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
DO-NOT -- miscellaneous keyword :DO-NOT
DO-NOT-INDUCT -- miscellaneous 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 at the terminal
E/D -- enable/disable rules
E0-ORD-< -- the old ordering function for ACL2 ordinals
E0-ORDINALP -- the old recognizer for ACL2 ordinals
EIGHTH -- eighth member of the list
ELIM -- make a destructor elimination rule
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
EQUIVALENCE -- mark a relation as an equivalence relation
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
EVENP -- test whether an integer is even
EVENTS -- functions that extend the logic
EVISCERATE-HIDE-TERMS -- to print (hide ...) as <hidden>
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 -- miscellaneous keyword :EXPAND
EXPLODE-NONNEGATIVE-INTEGER -- the list of characters in the decimal form of a number
EXPT -- exponential function
EXTENDED-METAFUNCTIONS -- state and context sensitive metafunctions
Evaluating App on Sample Input -- Evaluating App on Sample Input
FAILED-FORCING -- how to deal with a proof failure in a forcing round
FAILURE -- how to deal with a proof failure
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
FLOOR -- division returning an integer by truncating toward negative infinity
FLUSH-COMPRESS -- flush the under-the-hood array for the given name
FMS -- :(str alist co-channel state evisc) => state
FMS! -- :(str alist co-channel state evisc) => state
FMT -- formatted printing
FMT! -- :(str alist co-channel state evisc) => state
FMT-TO-COMMENT-WINDOW -- print to the comment window
FMT1 -- :(str alist col co-channel state evisc) => (mv col state)
FMT1! -- :(str alist col channel state evisc) => (mv col state)
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
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
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
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
GC$ -- invoke the garbage collector
GENERALIZE -- make a rule to restrict generalizations
GENERALIZED-BOOLEANS -- potential soundness issues related to ACL2 predicates
GOAL-SPEC -- to indicate where a hint is to be used
GOOD-BYE -- quit entirely out of Lisp
GROUND-ZERO -- enabled rules in the startup theory
GUARD -- restricting the domain of a function
GUARD-EXAMPLE -- a brief transcript illustrating guards in ACL2
GUARD-HINTS -- miscellaneous keyword :GUARD-HINTS
GUARD-INTRODUCTION -- introduction to guards in ACL2
GUARD-MISCELLANY -- miscellaneous remarks about guards
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
HANDS-OFF -- miscellaneous 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
HISTORY -- functions that display or change history
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 (continued) -- How To Find Out about ACL2 Functions (continued)
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
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 -- miscellaneous 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
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-THEORIES -- intersect two theories
INTERSECTP-EQ -- test whether two lists of symbols intersect
INTERSECTP-EQUAL -- test whether two lists intersect
INTRODUCTION -- introduction to ACL2
INVISIBLE-FNS-TABLE -- functions that are invisible to the loop-stopper algorithm
IO -- input/output facilities in ACL2
IRRELEVANT-FORMALS -- formals that are used but only insignificantly
J
KEEP -- how we know if include-book read the correct files
KEYWORD-COMMANDS -- how keyword commands are processed
KEYWORD-VALUE-LISTP -- recognizer for true lists whose even-position elements are keywords
KEYWORDP -- recognizer for keywords
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
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
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-LIST -- make a list of a given size
MAKE-ORD -- a constructor for ordinals.
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
MBT -- introduce a test not to be evaluated
MEASURE -- miscellaneous keyword :MEASURE
MEMBER -- membership predicate, using eql as test
MEMBER-EQ -- membership predicate, using eq as test
MEMBER-EQUAL -- membership predicate
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
MODE -- miscellaneous 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-doc's ``(cont'd)''
MORE! -- another response to ``(cont'd)''
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 multiple values
MV-LET -- calling multi-valued ACL2 functions
MV-NTH -- the mv-nth element (zero-based) of a list
Modeling in ACL2 -- Modeling in ACL2
Models in Engineering -- Models in Engineering
Models of Computer Hardware and Software -- Models of Computer Hardware and Software
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 (using eql for equality)
NO-DUPLICATESP-EQUAL -- check for duplicates in a list (using equal for equality)
NON-EXECUTABLE -- miscellaneous keyword :NON-EXECUTABLE
NON-LINEAR-ARITHMETIC -- Non-linear Arithmetic
NONLINEARP -- miscellaneous keyword :NONLINEARP
NONNEGATIVE-INTEGER-QUOTIENT -- natural number division function
NORMALIZE -- miscellaneous keyword :NORMALIZE
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
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
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-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
ODDP -- test whether an integer is odd
OK-IF -- conditional exit from break-rewrite
OOPS -- undo a :u or :ubt
OPEN-TRACE-FILE -- redirect trace output to a file
OR -- disjunction
ORDINALS -- ordinals in ACL2
OTF-FLG -- pushing all the initial subgoals
OTHER -- other commonly used top-level functions
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
PACKAGE-REINCARNATION-IMPORT-RESTRICTIONS -- re-defining undone defpkgs
PAIRLIS -- See pairlis$
PAIRLIS$ -- zipper together two lists
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 event named by a logical name
PE! -- print all the events named by a logical name
PF -- print the formula corresponding to the given name
PKG-WITNESS -- return a specific symbol in the indicated package
PL -- print the rules for the given name or term
PLUSP -- test whether a number is positive
PORTCULLIS -- the gate guarding the entrance to a certified book
POSITION -- position of an item in a string or a list, using eql as test
POSITION-EQ -- position of an item in a string or a list, using eq as test
POSITION-EQUAL -- position of an item in a string or a list
POSP -- a recognizer for the positive integers
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
PRINT-DOC-START-COLUMN -- printing the one-liner
PROG2$ -- execute two forms and return the value of the second one
PROGN -- see the documentation for er-progn
PROGRAM -- to set the default defun-mode to :program
PROGRAMMING -- built-in ACL2 functions
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
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-EQ -- modify an association list by associating a value with a key
PUT-ASSOC-EQL -- modify an association list by associating a value with a key
PUT-ASSOC-EQUAL -- modify an association list by associating a value with a key
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 -- quit ACL2 (type :q) -- reenter with (lp)
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
RASSOC -- look up value in association list, using eql as test
RASSOC-EQ -- look up value in association list, using eq as test
RASSOC-EQUAL -- look up value in association list, using equal as test
RATIONAL-LISTP -- recognizer for a true list of rational numbers
RATIONALP -- recognizer for rational numbers (ratios and integers)
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! -- system hacker's redefinition command
REDEFINED-NAMES -- to collect the names that have been redefined
REDEFINING-PROGRAMS -- an explanation of why we restrict redefinitions
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, testing using eql
REMOVE-BINOP -- remove the association of a binary function name with a macro name
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 (using eql) a list
REMOVE-DUPLICATES-EQUAL -- remove duplicates from a list
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 the association of one symbol with another for printing of nth/update-nth terms
REMOVE-RAW-ARITY -- remove arity information for raw mode
RESET-LD-SPECIALS -- restores initial settings of the ld specials
RESIZE-LIST -- list resizer in support of stobjs
REST -- rest (cdr) of the list
RESTRICT -- miscellaneous keyword :RESTRICT
RETRIEVE -- re-enter a (specified) proof-checker state
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.
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
SAVING-AND-RESTORING -- saving and restoring your logical state
SECOND -- second member of the list
SET-BACKCHAIN-LIMIT -- Sets the backchain-limit used by the rewriter
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-COMPILE-FNS -- have each function compiled as you go along.
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-DIFFERENCE-EQ -- elements of one list that are not elements of another
SET-DIFFERENCE-EQUAL -- elements of one list that are not elements of another
SET-DIFFERENCE-THEORIES -- difference of two theories
SET-GUARD-CHECKING -- control checking guards during execution of top-level forms
SET-IGNORE-OK -- allow unused formals and locals without an ignore declaration
SET-INHIBIT-OUTPUT-LST -- control output
SET-INHIBIT-WARNINGS -- control warnings
SET-INVISIBLE-FNS-TABLE -- set the invisible functions table
SET-IRRELEVANT-FORMALS-OK -- allow irrelevant formals in definitions
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-LINEARP -- to turn on or off non-linear arithmetic reasoning
SET-NU-REWRITER-MODE -- to turn on and off the nu-rewriter
SET-RAW-MODE -- enter or exit ``raw mode,'' a raw Lisp environment
SET-REWRITE-STACK-LIMIT -- Sets the rewrite stack depth used by the rewriter
SET-STATE-OK -- allow the use of STATE as a formal parameter
SET-VERIFY-GUARDS-EAGERNESS -- the eagerness with which guard verification is tried.
SET-WELL-FOUNDED-RELATION -- set the default well-founded relation
SEVENTH -- seventh member of the list
SHOW-BDD -- inspect failed BDD proof attempts
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-ARRAY-WARNING -- a warning issued when arrays are used inefficiently
SOLUTION-TO-SIMPLE-EXAMPLE -- solution to a simple example
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-NUMBERP -- ACL2(r) recognizer for standard numbers
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
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 -- miscellaneous 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
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-EQUAL -- check if all members of one list are members of the other
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
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
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
TIPS -- some hints for using the ACL2 prover
TOGGLE-PC-MACRO -- change an ordinary macro command to an atomic macro, or vice-versa
TRACE -- tracing functions in ACL2
TRACE$ -- trace the indicated functions
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
TTREE -- tag trees
TUTORIAL-EXAMPLES -- examples of ACL2 usage
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-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 -- undo last command, without a query
UBT -- undo the commands back through a command descriptor
UBT! -- undo commands, without a query or an error
UNARY-- -- arithmetic negation function
UNARY-/ -- reciprocal function
UNCERTIFIED-BOOKS -- invalid certificates and uncertified books
UNION-EQ -- union of two lists of symbols
UNION-EQUAL -- union of two lists
UNION-THEORIES -- union two theories
UNIVERSAL-THEORY -- all rules as of logical name
UNMONITOR -- to stop monitoring a rule name
UNSAVE -- remove a proof-checker state
UNTRACE$ -- untrace functions
UPDATE-NTH -- modify a list by putting the given value at the given position
UPPER-CASE-P -- recognizer for upper case characters
USE -- miscellaneous 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
Undocumented Topic -- Undocumented Topic
Using the Associativity of App to Prove a Trivial Consequence -- Using the Associativity of App to Prove a Trivial Consequence
VERBOSE-PSTACK -- seeing what is the prover up to
VERIFY -- enter the interactive proof checker
VERIFY-GUARDS -- verify the guards of a function
VERIFY-TERMINATION -- convert a function from :program mode to :logic mode
VERSION -- ACL2 Version Number
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-ERROR-TRACE -- evaluate a form and print subsequent error trace
WITH-LOCAL-STOBJ -- locally bind a single-threaded object
WITH-OUTPUT -- suppressing or turning on specified output for an event
WORLD -- ACL2 property lists and the ACL2 logical data base
WORMHOLE -- ld without state -- a short-cut to a parallel universe
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) (continued) -- What is a Mechanical Theorem Prover? (continued)
XARGS -- giving hints to defun
You Must Think about the Use of a Formula as a Rule -- You Must Think about the Use of a Formula as a Rule
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::= -- (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::CLAIM -- (atomic macro)
add a new hypothesis
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::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::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::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::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
