Index

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



Signs

* -- multiplication macro

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

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

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

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

+ -- 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

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



B

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



C

CAAAAR -- car of the caaar

CAAADR -- car of the caadr

CAAAR -- car of the caar

CAADAR -- car of the cadar

CAADDR -- car of the caddr

CAADR -- car of the cadr

CAAR -- car of the car

CADAAR -- car of the cdaar

CADADR -- car of the cdadr

CADAR -- car of the cdar

CADDAR -- car of the cddar

CADDDR -- car of the cdddr

CADDR -- car of the cddr

CADR -- car of the cdr

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



D

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



E

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



F

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



G

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



H

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

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



K

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



L

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



M

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

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

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

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

MAKE-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



N

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



O

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



P

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

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



R

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



S

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



T

TABLE -- user-managed tables

TAKE -- initial segment of a list

TENTH -- tenth member of the list

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

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

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

THE -- run-time type check

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

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



V

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



W

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)



X

XARGS -- giving hints to defun



Y

You Must Think about the Use of a Formula as a Rule -- You Must Think about the Use of a Formula as a Rule



Z

ZERO-TEST-IDIOMS -- how to test for 0

ZEROP -- test an acl2-number against 0

ZIP -- testing an ``integer'' against 0

ZP -- testing a ``natural'' against 0



ACL2-PC::

ACL2-PC::= -- (atomic macro)
attempt an equality (or equivalence) substitution


ACL2-PC::ACL2-WRAP -- (macro)
same as (lisp x)


ACL2-PC::ADD-ABBREVIATION -- (primitive)
add an abbreviation


ACL2-PC::BASH -- (atomic macro)
call the ACL2 theorem prover's simplifier


ACL2-PC::BDD -- (atomic macro)
prove the current goal using bdds


ACL2-PC::BK -- (atomic macro)
move backward one argument in the enclosing term


ACL2-PC::BOOKMARK -- (macro)
insert matching ``bookends'' comments


ACL2-PC::CASESPLIT -- (primitive)
split into two cases


ACL2-PC::CG -- (macro)
change to another goal.


ACL2-PC::CHANGE-GOAL -- (primitive)
change to another goal.


ACL2-PC::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