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, symbols, or characters)
> -- 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 rational number
ACCUMULATED-PERSISTENCE -- to get statistics on which runes are being tried
ACKNOWLEDGEMENTS -- 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-MACRO-ALIAS -- associate a function name with a macro name
ADD-TO-SET-EQ -- add a symbol to a list
ALISTP -- recognizer for association lists
ALPHA-CHAR-P -- recognizer for alphabetic characters
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.
ASET1 -- set the elements of a 1-dimensional array
ASET2 -- set the elements of a 2-dimensional array
ASH -- arithmetic shift operation
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
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
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-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 and measure and guard generating
BUTLAST -- all but a final segment of a list
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
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
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
COMPILATION -- compiling ACL2 functions
COMPLEX -- create an ACL2 number
COMPLEX-RATIONALP -- recognizes complex rational 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
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
DEFAULT -- return the :default from the header of a 1- or 2-dimensional array
DEFAULT-DEFUN-MODE -- the default defun-mode of defun'd functions
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
DEFINE-PC-HELP -- define a macro command whose purpose is to print something
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
DEFSTUB -- stub-out a function symbol
DEFTHEORY -- define a theory (to enable or disable a set of rules)
DEFTHM -- prove and name a theorem
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
DEFUNS -- an alternative to mutual-recursion
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
DISABLEDP -- determine whether a given name or rune is disabled
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
E0-ORD-< -- the well-founded less-than relation on ordinals up to epsilon-0
E0-ORDINALP -- a recognizer for the ordinals up to epsilon-0
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 case splits
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-PROGN -- perform a sequence of state-changing ``error triples''
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-BOOT-STRAP-MODE -- the end of pre-history
EXPLODE-NONNEGATIVE-INTEGER -- the list of characters in the decimal form of a number
EXPT -- exponential function
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
FMS -- :(str alist co-channel state evisc) => state
FMT -- formatted printing
FMT1 -- :(str alist col co-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
FULL-BOOK-NAME -- book naming conventions assumed by ACL2
FUNCTION-THEORY -- function symbol rules as of logical name
Flawed Induction Candidates in App Example -- Flawed Induction Candidates in App Example
Functions for Manipulating these Objects -- Functions for Manipulating these Objects
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-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
HEADER -- return the header of a 1- or 2-dimensional array
HELP -- brief survey of ACL2 features
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
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 -- cause a hard error
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-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
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-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-ALIST -- 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
LENGTH -- length of a string or proper list
LET -- binding of lexically scoped (local) variables
LET* -- binding of lexically scoped (local) variables
LINEAR -- make some arithmetic inequality rules
LINEAR-ALIAS -- make a rule to extend the applicability of linear arithmetic
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 two 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 two 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 two 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 two 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
MARKUP -- the markup language for ACL2 documentation strings
MAX -- the larger of two rational numbers
MAXIMUM-LENGTH -- return the :maximum-length from the header of an array
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 rational numbers
MINUSP -- test whether a rational number is negative
MISCELLANEOUS -- a miscellany of documented functions and concepts
(often cited in more accessible documentation)
MOD -- remainder using floor
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
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
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)
NONNEGATIVE-INTEGER-QUOTIENT -- natural number division function
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
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
NTHCDR -- final segment of a list
NULL -- recognizer for the empty list
NUMERATOR -- dividend of a ratio in lowest terms
Name the Formula Above -- Name the Formula Above
Numbers in ACL2 -- Numbers in ACL2
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
OR -- conjunction
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
PL -- print the rules whose top function symbol is the given name
PLUSP -- test whether a rational 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
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
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-OF-WELL-FOUNDEDNESS -- a proof that e0-ord-< is well-founded on e0-ordinalps
PROOF-TREE -- proof tree displays
PROOF-TREE-DETAILS -- proof tree details not covered elsewhere
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
PUFF -- replace a compound command by its immediate subevents
PUFF* -- replace a compound command by its subevents
PUT-ASSOC-EQ -- 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)
RASSOC -- look up value in association list, using eql as test
RATIONAL-LISTP -- recognizer for a true list of rational numbers
RATIONALP -- recognizer for whole numbers
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-DUPLICATES -- remove duplicates from a string or (using eql) a list
REMOVE-DUPLICATES-EQUAL -- remove duplicates from a list
REMOVE-MACRO-ALIAS -- remove the association of a function name with a macro name
RESET-LD-SPECIALS -- restores initial settings of the ld specials
REST -- rest (cdr) of the list
RETRIEVE -- re-enter a (specified) proof-checker state
REVAPPEND -- concatentate the reverse of one list to another
REVERSE -- reverse a list
REWRITE -- make some :rewrite rules (possibly conditional ones)
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-CBD -- to set the connected book directory
SET-COMPILE-FNS -- have each function compiled as you go along.
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-ALIST -- set the invisible functions alist
SET-IRRELEVANT-FORMALS-OK -- allow irrelevant formals in definitions
SET-MEASURE-FUNCTION -- set the default measure function symbol
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 an event -- 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 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''
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
STATE is the Only Variable in Top-Level Forms -- STATE is the Only Variable in Top-Level Forms
STOP-PROOF-TREE -- stop displaying proof trees during proofs
STRING -- coerce to a string
STRING-ALISTP -- recognizer for association lists with strings as keys
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
SUBVERSIVE-INDUCTIONS -- 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 -- to attach a heuristic filter on a :rewrite rule
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
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
TRANS -- print the macroexpansion of a form
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
UPDATE-NTH -- modify a list by putting the given value at the given position
UPPER-CASE-P -- recognizer for upper case characters
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 -- 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
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
WHY-BRR -- an explanation of why ACL2 has an explicit brr mode
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
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::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-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 toxae THEN
ACL2-PC::RUN-INSTR-ON-NEW-GOALS -- (macro)
auxiliary to then
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::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
