Info file: acl2-doc-emacs.info, -*-Text-*- produced by `texinfo-format-buffer' from file `acl2-doc-emacs.texinfo' using `texinfmt.el' version 2.32 of 19 November 1993. This is documentation for ACL2 Version 1.9 Copyright (C) 1997 Computational Logic, Inc. This program is free software; you can redistribute it and/or modify it under the terms of the GNU General Public License as published by the Free Software Foundation; either version 2 of the License, or (at your option) any later version. This program is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License for more details. You should have received a copy of the GNU General Public License along with this program; if not, write to the Free Software Foundation, Inc., 675 Mass Ave, Cambridge, MA 02139, USA. Written by: Matt Kaufmann and J Strother Moore Computational Logic, Inc. 1717 West Sixth Street, Suite 290 Austin, TX 78703-4776 U.S.A.  File: acl2-doc-emacs.info, Node: CURRENT-THEORY, Next: DISABLE, Prev: THEORIES, Up: THEORIES CURRENT-THEORY currently enabled rules as of logical name Examples: (current-theory :here) (current-theory 'lemma3) See *Note LOGICAL-NAME::. General Form: (current-theory logical-name) Returns the current theory as it existed immediately after the introduction of logical-name provided it is evaluated in an environment in which the variable symbol WORLD is bound to the current ACL2 logical world, (w state). Thus, ACL2 !>(current-theory :here) will cause an (unbound variable) error while ACL2 !>(let ((world (w state))) (current-theory :here)) will return the current theory in world. See *Note THEORIES:: and see *Note LOGICAL-NAME:: for a discussion of theories in general and why the commonly used "theory functions" such as current-theory are really macros that expand into terms involving the variable world. The theory returned by current-theory is in fact the theory selected by the in-theory event most recently preceding logical name, extended by the rules introduced up through logical-name. You may experience a fencepost problem in deciding which logical name to use. Deflabel can always be used to mark unambiguously for future reference a particular point in the development of your theory. The order of events in the vicinity of an encapsulate is confusing. See *Note ENCAPSULATE::. This "function" is actually a macro that expands to a term mentioning the single free variable world. When theory expressions are evaluated by in-theory or the :in-theory hint, world is bound to the current ACL2 world.  File: acl2-doc-emacs.info, Node: DISABLE, Next: ENABLE, Prev: CURRENT-THEORY, Up: THEORIES DISABLE deletes names from current theory Example: (disable fact (fact) associativity-of-app) General Form: (disable name1 name2 ... namek) where each namei is a runic designator; see *Note THEORIES::. The result is the theory that contains all the names in the current theory except those listed. Note that this is merely a function that returns a theory. The result is generally a very long list of runes and you will probably regret printing it. The standard way to "disable" a fixed set of names, is: (in-theory (disable name1 name2 ... namek)) ; globally :in-theory (disable name1 name2 ... namek) ; locally Note that all the names are implicitly quoted. If you wish to disable a computed list of names, lst, use the theory expression (set-difference-theories (current-theory :here) lst).  File: acl2-doc-emacs.info, Node: ENABLE, Next: EXECUTABLE-COUNTERPART-THEORY, Prev: DISABLE, Up: THEORIES ENABLE adds names to current theory Example: (enable fact (fact) associativity-of-app) General Form: (enable name1 name2 ... namek) where each namei is a runic designator; see *Note THEORIES::. The result is the theory that contains all the names in the current theory plus those listed. Note that this is merely a function that returns a theory. The result is generally a very long list of runes and you will probably regret printing it. The standard way to "enable" a fixed set of names, is (in-theory (enable name1 name2 ... namek)) ; globally :in-theory (enable name1 name2 ... namek) ; locally Note that all the names are implicitly quoted. If you wish to enable a computed list of names, lst, use the theory expression (union-theories (current-theory :here) lst).  File: acl2-doc-emacs.info, Node: EXECUTABLE-COUNTERPART-THEORY, Next: FUNCTION-THEORY, Prev: ENABLE, Up: THEORIES EXECUTABLE-COUNTERPART-THEORY executable counterpart rules as of logical name Examples: (executable-counterpart-theory :here) (executable-counterpart-theory 'lemma3) See *Note LOGICAL-NAME::. General Form: (executable-counterpart-theory logical-name) Returns the theory containing all the :executable-counterpart runes, whether enabled or not, that existed immediately after logical-name was introduced. See the documentation for theories, logical-name, executable-counterpart and function-theory. You may experience a fencepost problem in deciding which logical name to use. Deflabel can always be used to mark unambiguously for future reference a particular point in the development of your theory. The order of events in the vicinity of an encapsulate is confusing. See *Note ENCAPSULATE::. This "function" is actually a macro that expands to a term mentioning the single free variable world. When theory expressions are evaluated by in-theory or the :in-theory hint, world is bound to the current ACL2 world.  File: acl2-doc-emacs.info, Node: FUNCTION-THEORY, Next: GROUND-ZERO, Prev: EXECUTABLE-COUNTERPART-THEORY, Up: THEORIES FUNCTION-THEORY function symbol rules as of logical name Examples: (function-theory :here) (function-theory 'lemma3) See *Note LOGICAL-NAME::. General Form: (function-theory logical-name) Returns the theory containing all the :definition runes, whether enabled or not, that existed immediately after logical-name was introduced. See the documentation for theories, logical-name and executable-counterpart-theory. You may experience a fencepost problem in deciding which logical name to use. Deflabel can always be used to mark unambiguously for future reference a particular point in the development of your theory. The order of events in the vicinity of an encapsulate is confusing. See *Note ENCAPSULATE::. This "function" is actually a macro that expands to a term mentioning the single free variable world. When theory expressions are evaluated by in-theory or the :in-theory hint, world is bound to the current ACL2 world.  File: acl2-doc-emacs.info, Node: GROUND-ZERO, Next: INCOMPATIBLE, Prev: FUNCTION-THEORY, Up: THEORIES GROUND-ZERO enabled rules in the startup theory ACL2 concludes its initialization (boot-strapping) procedure by defining the theory ground-zero; see *Note THEORIES::. In fact, this theory is just the theory defined by (current-theory :here) at the conclusion of initialization; see *Note CURRENT-THEORY::. Note that by executing the event (in-theory (current-theory 'ground-zero)) you can restore the current theory to its value at the time you started up ACL2.  File: acl2-doc-emacs.info, Node: INCOMPATIBLE, Next: INTERSECTION-THEORIES, Prev: GROUND-ZERO, Up: THEORIES INCOMPATIBLE declaring that two rules should not both be enabled Example: (theory-invariant (incompatible (:rewrite left-to-right) (:rewrite right-to-left))) General Form: (incompatible rune1 rune2) where rune1 and rune2 are two specific runes. The arguments are not evaluated. Invariant is just a macro that expands into a term that checks that theory does not contain both runes. See *Note THEORY-INVARIANT::.  File: acl2-doc-emacs.info, Node: INTERSECTION-THEORIES, Next: RULE-NAMES, Prev: INCOMPATIBLE, Up: THEORIES INTERSECTION-THEORIES intersect two theories Example: (intersection-theories (current-theory :here) (theory 'arith-patch)) General Form: (intersection-theories th1 th2) where th1 and th2 are theories (see *Note THEORIES::). To each of the arguments there corresponds a runic theory. This function returns the intersection of those two runic theories, represented as a list and ordered chronologically. This "function" is actually a macro that expands to a term mentioning the single free variable world. When theory expressions are evaluated by in-theory or the :in-theory hint, world is bound to the current ACL2 world.  File: acl2-doc-emacs.info, Node: RULE-NAMES, Next: RUNE, Prev: INTERSECTION-THEORIES, Up: THEORIES RULE-NAMES How rules are named. Examples: (:rewrite assoc-of-app) (:linear delta-aref . 2) (:definition length) (:executable-counterpart length) See *Note RUNE::.  File: acl2-doc-emacs.info, Node: RUNE, Next: SET-DIFFERENCE-THEORIES, Prev: RULE-NAMES, Up: THEORIES RUNE a rule name Examples: (:rewrite assoc-of-app) (:linear delta-aref . 2) (:definition length) (:executable-counterpart length) Background: The theorem prover is driven from a data base of rules. The most common rules are :rewrite rules, which cause the simplifier to replace one term with another. Events introduce rules into the data base. For example, a defun event may introduce as many as four rules: one for symbolically replacing a function call by its instantiated body, one for evaluating the function on constants, and two for determining the type of a call of the function (one of which is deduced before guard verification and the other of which is deduced after guard verification). Defthm may introduce several rules, one for each of the rule classes specified. Every rule in the system has a name. Each name is a structured object called a "rune," which is short for "rule name". Runes are always of the form (:token symbol . x), where :token is some keyword symbol indicating what kind of rule is named, symbol is the event name that created the rule (and is called the "base symbol" of the rune), and x is either nil or a natural number that makes the rule name unique. For example, an event of the form (defthm name thm :rule-classes ((:REWRITE :COROLLARY term1) (:REWRITE :COROLLARY term2) (:ELIM :COROLLARY term3))) creates three rules, each with a unique rune. The runes are (:REWRITE name . 1), (:REWRITE name . 2), and (:ELIM name). The function corollary will return the corollary term associated with a given rune in a given world. Example: (corollary '(:TYPE-PRESCRIPTION DIGIT-TO-CHAR) (w state)) However, the preferred way to see the corollary term associated with a rune or a name is to use :pf; see *Note PF::. The defun event creates as many as four rules. (:definition fn) is the rune given to the equality axiom defining the function, fn. (:executable-counterpart fn) is the rune given to the rule for computing fn on known arguments. A type prescription rule may be created under the name (:type-prescription fn), and an induction rule may be created under the name (:induction fn). Runes may be individually enabled and disabled, according to whether they are included in the current theory. See *Note THEORIES::. Thus, it is permitted to disable (:elim name), say, while enabling the other rules derived from name. Similarly, (:definition fn) may be disabled while (:executable-counterpart fn) and the type prescriptions for fn are enabled. Associated with most runes is the formula justifying the rule named. This is called the "corollary formula" of the rune and may be obtained via the function corollary, which takes as its argument a rune and a property list world. Also see *Note PF::. The corollary formula for (:rewrite name . 1) after the defthm event above is term1. The corollary formulas for (:definition fn) and (:executable-counterpart fn) are always identical: the defining axiom. Some runes, e.g., (:definition car), do not have corollary formulas. Corollary returns nil on such runes. In any case, the corollary formula of a rune, when it is non-nil, is a theorem and may be used in the :use and :by hints. Note: The system has many built in rules that, for regularity, ought to have names but don't because they can never be disabled. One such rule is that implemented by the linear arithmetic package. Because many of our subroutines are required by their calling conventions to return the justifying rune, we have invented the notion of "fake runes." Fake runes always have the base symbol nil, use a keyword token that includes the phrase "fake-rune", and are always enabled. For example, (:fake-rune-for-linear nil) is a fake rune. Occasionally the system will print a fake rune where a rune is expected. For example, when the linear arithmetic fake rune is reported among the rules used in a proof, it is an indication that the linear arithmetic package was used. However, fake runes are not allowed in theories, they cannot be enabled or disabled, and they do not have associated corollary formulas. In short, despite the fact that the user may sometimes see fake runes printed, they should never be typed.  File: acl2-doc-emacs.info, Node: SET-DIFFERENCE-THEORIES, Next: THEORY, Prev: RUNE, Up: THEORIES SET-DIFFERENCE-THEORIES difference of two theories Example: (set-difference-theories (current-theory :here) '(fact (fact))) General Form: (set-difference-theories th1 th2) where th1 and th2 are theories (see *Note THEORIES::). To each of the arguments there corresponds a runic theory. This function returns the set-difference of those two runic theories, represented as a list and ordered chronologically. That is, a rune is in the result iff it is in the first runic theory but not in the second. The standard way to "disable" a theory, lst, is: (in-theory (set-difference-theories (current-theory :here) lst)). This "function" is actually a macro that expands to a term mentioning the single free variable world. When theory expressions are evaluated by in-theory or the :in-theory hint, world is bound to the current ACL2 world.  File: acl2-doc-emacs.info, Node: THEORY, Next: THEORY-FUNCTIONS, Prev: SET-DIFFERENCE-THEORIES, Up: THEORIES THEORY retrieve named theory Example: (theory 'my-theory) General Form: (theory name) where name is the name of a previously executed deftheory event. Returns the named theory. See *Note THEORIES::. This "function" is actually a macro that expands to a term mentioning the single free variable world. When theory expressions are evaluated by in-theory or the :in-theory hint, world is bound to the current ACL2 world.  File: acl2-doc-emacs.info, Node: THEORY-FUNCTIONS, Next: UNION-THEORIES, Prev: THEORY, Up: THEORIES THEORY-FUNCTIONS functions for obtaining or producing theories Example Calls of Theory Functions: (universal-theory :here) (union-theories th1 th2) (set-difference-theories th1 th2) The theory functions are documented individually: * Menu: Related topics other than immediate subtopics: * CURRENT-THEORY:: currently enabled rules as of logical name * DISABLE:: deletes names from current theory * ENABLE:: adds names to current theory * EXECUTABLE-COUNTERPART-THEORY:: executable counterpart rules as of logical name * FUNCTION-THEORY:: function symbol rules as of logical name * INTERSECTION-THEORIES:: intersect two theories * SET-DIFFERENCE-THEORIES:: difference of two theories * THEORY:: retrieve named theory * UNION-THEORIES:: union two theories * UNIVERSAL-THEORY:: all rules as of logical name The functions (actually, macros) mentioned above are convenient ways to produce theories. (See *Note THEORIES::.) Some, like universal-theory, take a logical name (see *Note LOGICAL-NAME::) as an argument and return the relevant theory as of the time that name was introduced. Others, like union-theories, take two theories and produce a new one. See *Note REDUNDANT-EVENTS:: for a caution about the use of logical names in theory expressions. Theory expressions are generally composed of applications of theory functions. Formally, theory expressions are expressions that involve, at most, the free variable world and that when evaluated with world bound to the current ACL2 world (see *Note WORLD::) return theories. The "theory functions" are actually macros that expand into forms that involve the free variable world. Thus, for example (universal-theory :here) actually expands to (universal-theory-fn :here world) and when that form is evaluated with world bound to the current ACL2 world, universal-theory-fn scans the ACL2 property lists and computes the current universal theory. Because the theory functions all implicitly use world, the variable does not generally appear in anything the user types.  File: acl2-doc-emacs.info, Node: UNION-THEORIES, Next: UNIVERSAL-THEORY, Prev: THEORY-FUNCTIONS, Up: THEORIES UNION-THEORIES union two theories Example: (union-theories (current-theory 'lemma3) (theory 'arith-patch)) General Form: (union-theories th1 th2) where th1 and th2 are theories (see *Note THEORIES::). To each of the arguments there corresponds a runic theory. This function returns the union of those two runic theories, represented as a list and ordered chronologically. This "function" is actually a macro that expands to a term mentioning the single free variable world. When theory expressions are evaluated by in-theory or the :in-theory hint, world is bound to the current ACL2 world.  File: acl2-doc-emacs.info, Node: UNIVERSAL-THEORY, Prev: UNION-THEORIES, Up: THEORIES UNIVERSAL-THEORY all rules as of logical name Examples: (universal-theory :here) (universal-theory 'lemma3) See *Note LOGICAL-NAME::. General Form: (universal-theory logical-name) Returns the theory consisting of all the runes that existed immediately after logical-name was introduced. See *Note THEORIES::and see *Note LOGICAL-NAME::. The theory includes logical-name itself (if there is a rule by that name). (Note that since some events do not introduce rules (e.g., defmacro, defconst or defthm with :rule-classes nil), the universal-theory does not necessarily include a rune for every event name.) The universal-theory is very long and you will probably regret printing it. You may experience a fencepost problem in deciding which logical-name to use. Deflabel can always be used to mark unambiguously for future reference a particular point in the development of your theory. This is convenient because deflabel does not introduce any rules and hence it doesn't matter if you count it as being in the interval or not. The order of events in the vicinity of an encapsulate is confusing. See *Note ENCAPSULATE::. This "function" is actually a macro that expands to a term mentioning the single free variable world. When theory expressions are evaluated by in-theory or the :in-theory hint, world is bound to the current ACL2 world.  File: acl2-doc-emacs.info, Node: Index, Up: Top Index ***** * Menu: * *: *. 2. * +: +. 2. * -: -. 2. * /: /. 2. * <: <. 2. * =: =. 2. * >: >. 2. * /=: /=. 2. * <=: <=. 2. * >=: >=. 2. * @: atsign. 2. * 1+: 1+. 2. * 1-: 1-. 2. * A Flying Tour of ACL2: A Flying Tour of ACL2. 2. * A Sketch of How the Rewriter Works: A Sketch of How the Rewriter Works. 2. * A Tiny Warning Sign: A Tiny Warning Sign. 2. * A Trivial Proof: A Trivial Proof. 2. * A Typical State: A Typical State. 2. * A Walking Tour of ACL2: A Walking Tour of ACL2. 2. * About Models: About Models. 2. * About the ACL2 Home Page: About the ACL2 Home Page. 2. * About the Admission of Recursive Definitions: About the Admission of Recursive Definitions. 2. * About the Prompt: About the Prompt. 2. * About Types: About Types. 2. * ABS: ABS. 2. * ACCUMULATED-PERSISTENCE: ACCUMULATED-PERSISTENCE. 2. * ACKNOWLEDGEMENTS: ACKNOWLEDGEMENTS. 2. * ACL2 as an Interactive Theorem Prover: ACL2 as an Interactive Theorem Prover. 2. * ACL2 as an Interactive Theorem Prover (continued): ACL2 as an Interactive Theorem Prover (continued). 2. * ACL2 Characters: ACL2 Characters. 2. * ACL2 Conses or Ordered Pairs: ACL2 Conses or Ordered Pairs. 2. * ACL2 is an Untyped Language: ACL2 is an Untyped Language. 2. * ACL2 Strings: ACL2 Strings. 2. * ACL2 Symbols: ACL2 Symbols. 2. * ACL2 System Architecture: ACL2 System Architecture. 2. * ACL2-COMPLEX-RATIONALP: ACL2-COMPLEX-RATIONALP. 2. * ACL2-COUNT: ACL2-COUNT. 2. * ACL2-CUSTOMIZATION: ACL2-CUSTOMIZATION. 2. * ACL2-DEFAULTS-TABLE: ACL2-DEFAULTS-TABLE. 2. * ACL2-NUMBERP: ACL2-NUMBERP. 2. * ACL2-PC||=: ACL2-PC||=. 2. * ACL2-PC||ACL2-WRAP: ACL2-PC||ACL2-WRAP. 2. * ACL2-PC||ADD-ABBREVIATION: ACL2-PC||ADD-ABBREVIATION. 2. * ACL2-PC||BASH: ACL2-PC||BASH. 2. * ACL2-PC||BDD: ACL2-PC||BDD. 2. * ACL2-PC||BK: ACL2-PC||BK. 2. * ACL2-PC||BOOKMARK: ACL2-PC||BOOKMARK. 2. * ACL2-PC||CASESPLIT: ACL2-PC||CASESPLIT. 2. * ACL2-PC||CG: ACL2-PC||CG. 2. * ACL2-PC||CHANGE-GOAL: ACL2-PC||CHANGE-GOAL. 2. * ACL2-PC||CLAIM: ACL2-PC||CLAIM. 2. * ACL2-PC||COMM: ACL2-PC||COMM. 2. * ACL2-PC||COMMANDS: ACL2-PC||COMMANDS. 2. * ACL2-PC||COMMENT: ACL2-PC||COMMENT. 2. * ACL2-PC||CONTRADICT: ACL2-PC||CONTRADICT. 2. * ACL2-PC||CONTRAPOSE: ACL2-PC||CONTRAPOSE. 2. * ACL2-PC||DEMOTE: ACL2-PC||DEMOTE. 2. * ACL2-PC||DIVE: ACL2-PC||DIVE. 2. * ACL2-PC||DO-ALL: ACL2-PC||DO-ALL. 2. * ACL2-PC||DO-ALL-NO-PROMPT: ACL2-PC||DO-ALL-NO-PROMPT. 2. * ACL2-PC||DO-STRICT: ACL2-PC||DO-STRICT. 2. * ACL2-PC||DROP: ACL2-PC||DROP. 2. * ACL2-PC||DV: ACL2-PC||DV. 2. * ACL2-PC||ELIM: ACL2-PC||ELIM. 2. * ACL2-PC||EQUIV: ACL2-PC||EQUIV. 2. * ACL2-PC||EX: ACL2-PC||EX. 2. * ACL2-PC||EXIT: ACL2-PC||EXIT. 2. * ACL2-PC||EXPAND: ACL2-PC||EXPAND. 2. * ACL2-PC||FAIL: ACL2-PC||FAIL. 2. * ACL2-PC||FORWARDCHAIN: ACL2-PC||FORWARDCHAIN. 2. * ACL2-PC||FREE: ACL2-PC||FREE. 2. * ACL2-PC||GENERALIZE: ACL2-PC||GENERALIZE. 2. * ACL2-PC||GOALS: ACL2-PC||GOALS. 2. * ACL2-PC||HELP: ACL2-PC||HELP. 2. * ACL2-PC||HELP!: ACL2-PC||HELP!. 2. * ACL2-PC||HELP-LONG: ACL2-PC||HELP-LONG. 2. * ACL2-PC||HYPS: ACL2-PC||HYPS. 2. * ACL2-PC||ILLEGAL: ACL2-PC||ILLEGAL. 2. * ACL2-PC||INDUCT: ACL2-PC||INDUCT. 2. * ACL2-PC||IN-THEORY: ACL2-PC||IN-THEORY. 2. * ACL2-PC||LISP: ACL2-PC||LISP. 2. * ACL2-PC||MORE: ACL2-PC||MORE. 2. * ACL2-PC||MORE!: ACL2-PC||MORE!. 2. * ACL2-PC||NEGATE: ACL2-PC||NEGATE. 2. * ACL2-PC||NIL: ACL2-PC||NIL. 2. * ACL2-PC||NOISE: ACL2-PC||NOISE. 2. * ACL2-PC||NX: ACL2-PC||NX. 2. * ACL2-PC||ORELSE: ACL2-PC||ORELSE. 2. * ACL2-PC||P: ACL2-PC||P. 2. * ACL2-PC||PP: ACL2-PC||PP. 2. * ACL2-PC||PRINT: ACL2-PC||PRINT. 2. * ACL2-PC||PRINT-ALL-GOALS: ACL2-PC||PRINT-ALL-GOALS. 2. * ACL2-PC||PRINT-MAIN: ACL2-PC||PRINT-MAIN. 2. * ACL2-PC||PRO: ACL2-PC||PRO. 2. * ACL2-PC||PROMOTE: ACL2-PC||PROMOTE. 2. * ACL2-PC||PROTECT: ACL2-PC||PROTECT. 2. * ACL2-PC||PROVE: ACL2-PC||PROVE. 2. * ACL2-PC||P-TOP: ACL2-PC||P-TOP. 2. * ACL2-PC||PUT: ACL2-PC||PUT. 2. * ACL2-PC||QUIET: ACL2-PC||QUIET. 2. * ACL2-PC||R: ACL2-PC||R. 2. * ACL2-PC||REDUCE: ACL2-PC||REDUCE. 2. * ACL2-PC||REDUCE-BY-INDUCTION: ACL2-PC||REDUCE-BY-INDUCTION. 2. * ACL2-PC||REMOVE-ABBREVIATIONS: ACL2-PC||REMOVE-ABBREVIATIONS. 2. * ACL2-PC||REPEAT: ACL2-PC||REPEAT. 2. * ACL2-PC||REPEAT-REC: ACL2-PC||REPEAT-REC. 2. * ACL2-PC||REPLAY: ACL2-PC||REPLAY. 2. * ACL2-PC||RESTORE: ACL2-PC||RESTORE. 2. * ACL2-PC||RETAIN: ACL2-PC||RETAIN. 2. * ACL2-PC||RETRIEVE: ACL2-PC||RETRIEVE. 2. * ACL2-PC||REWRITE: ACL2-PC||REWRITE. 2. * ACL2-PC||RUN-INSTR-ON-GOAL: ACL2-PC||RUN-INSTR-ON-GOAL. 2. * ACL2-PC||RUN-INSTR-ON-NEW-GOALS: ACL2-PC||RUN-INSTR-ON-NEW-GOALS. 2. * ACL2-PC||S: ACL2-PC||S. 2. * ACL2-PC||SAVE: ACL2-PC||SAVE. 2. * ACL2-PC||SEQUENCE: ACL2-PC||SEQUENCE. 2. * ACL2-PC||SHOW-ABBREVIATIONS: ACL2-PC||SHOW-ABBREVIATIONS. 2. * ACL2-PC||SHOW-REWRITES: ACL2-PC||SHOW-REWRITES. 2. * ACL2-PC||SKIP: ACL2-PC||SKIP. 2. * ACL2-PC||SL: ACL2-PC||SL. 2. * ACL2-PC||SPLIT: ACL2-PC||SPLIT. 2. * ACL2-PC||S-PROP: ACL2-PC||S-PROP. 2. * ACL2-PC||SR: ACL2-PC||SR. 2. * ACL2-PC||SUCCEED: ACL2-PC||SUCCEED. 2. * ACL2-PC||TH: ACL2-PC||TH. 2. * ACL2-PC||THEN: ACL2-PC||THEN. 2. * ACL2-PC||TOP: ACL2-PC||TOP. 2. * ACL2-PC||TYPE-ALIST: ACL2-PC||TYPE-ALIST. 2. * ACL2-PC||UNDO: ACL2-PC||UNDO. 2. * ACL2-PC||UNSAVE: ACL2-PC||UNSAVE. 2. * ACL2-PC||UP: ACL2-PC||UP. 2. * ACL2-PC||USE: ACL2-PC||USE. 2. * ACL2-PC||X: ACL2-PC||X. 2. * ACL2-PC||X-DUMB: ACL2-PC||X-DUMB. 2. * ACL2-TUTORIAL: ACL2-TUTORIAL. 2. * ACL2-USER: ACL2-USER. 2. * ACONS: ACONS. 2. * ADD-MACRO-ALIAS: ADD-MACRO-ALIAS. 2. * ADD-TO-SET-EQ: ADD-TO-SET-EQ. 2. * ALISTP: ALISTP. 2. * ALPHA-CHAR-P: ALPHA-CHAR-P. 2. * An Example Common Lisp Function Definition: An Example Common Lisp Function Definition. 2. * An Example of ACL2 in Use: An Example of ACL2 in Use. 2. * Analyzing Common Lisp Models: Analyzing Common Lisp Models. 2. * AND: AND. 2. * APPEND: APPEND. 2. * APROPOS: APROPOS. 2. * AREF1: AREF1. 2. * AREF2: AREF2. 2. * ARGS: ARGS. 2. * ARRAY1P: ARRAY1P. 2. * ARRAY2P: ARRAY2P. 2. * ARRAYS: ARRAYS. 2. * ASET1: ASET1. 2. * ASET2: ASET2. 2. * ASH: ASH. 2. * ASSIGN: ASSIGN. 2. * ASSOC: ASSOC. 2. * ASSOC-EQ: ASSOC-EQ. 2. * ASSOC-EQUAL: ASSOC-EQUAL. 2. * ASSOC-KEYWORD: ASSOC-KEYWORD. 2. * ASSOC-STRING-EQUAL: ASSOC-STRING-EQUAL. 2. * ATOM: ATOM. 2. * ATOM-LISTP: ATOM-LISTP. 2. * BDD: BDD. 2. * BDD-ALGORITHM: BDD-ALGORITHM. 2. * BDD-INTRODUCTION: BDD-INTRODUCTION. 2. * BIBLIOGRAPHY: BIBLIOGRAPHY. 2. * BINARY-*: BINARY-*. 2. * BINARY-+: BINARY-+. 2. * BINARY-APPEND: BINARY-APPEND. 2. * BOOK-CONTENTS: BOOK-CONTENTS. 2. * BOOK-EXAMPLE: BOOK-EXAMPLE. 2. * BOOK-NAME: BOOK-NAME. 2. * BOOKS: BOOKS. 2. * BOOLEANP: BOOLEANP. 2. * BREAK-LEMMA: BREAK-LEMMA. 2. * BREAK-REWRITE: BREAK-REWRITE. 2. * BREAKS: BREAKS. 2. * BRR: BRR. 2. * BRR@: BRRatsign. 2. * BRR-COMMANDS: BRR-COMMANDS. 2. * BUILT-IN-CLAUSES: BUILT-IN-CLAUSES. 2. * BUTLAST: BUTLAST. 2. * CAAAAR: CAAAAR. 2. * CAAADR: CAAADR. 2. * CAAAR: CAAAR. 2. * CAADAR: CAADAR. 2. * CAADDR: CAADDR. 2. * CAADR: CAADR. 2. * CAAR: CAAR. 2. * CADAAR: CADAAR. 2. * CADADR: CADADR. 2. * CADAR: CADAR. 2. * CADDAR: CADDAR. 2. * CADDDR: CADDDR. 2. * CADDR: CADDR. 2. * CADR: CADR. 2. * CAR: CAR. 2. * CASE: CASE. 2. * CASE-MATCH: CASE-MATCH. 2. * CBD: CBD. 2. * CDAAAR: CDAAAR. 2. * CDAADR: CDAADR. 2. * CDAAR: CDAAR. 2. * CDADAR: CDADAR. 2. * CDADDR: CDADDR. 2. * CDADR: CDADR. 2. * CDAR: CDAR. 2. * CDDAAR: CDDAAR. 2. * CDDADR: CDDADR. 2. * CDDAR: CDDAR. 2. * CDDDAR: CDDDAR. 2. * CDDDDR: CDDDDR. 2. * CDDDR: CDDDR. 2. * CDDR: CDDR. 2. * CDR: CDR. 2. * CEILING: CEILING. 2. * CERTIFICATE: CERTIFICATE. 2. * CERTIFY-BOOK: CERTIFY-BOOK. 2. * CERTIFY-BOOK!: CERTIFY-BOOK!. 2. * CHAR: CHAR. 2. * CHAR<: CHAR<. 2. * CHAR>: CHAR>. 2. * CHAR<=: CHAR<=. 2. * CHAR>=: CHAR>=. 2. * CHARACTER-LISTP: CHARACTER-LISTP. 2. * CHARACTERP: CHARACTERP. 2. * CHARACTERS: CHARACTERS. 2. * CHAR-CODE: CHAR-CODE. 2. * CHAR-DOWNCASE: CHAR-DOWNCASE. 2. * CHAR-EQUAL: CHAR-EQUAL. 2. * CHAR-UPCASE: CHAR-UPCASE. 2. * CHECKPOINT-FORCED-GOALS: CHECKPOINT-FORCED-GOALS. 2. * CHECK-SUM: CHECK-SUM. 2. * CLAUSE-IDENTIFIER: CLAUSE-IDENTIFIER. 2. * CODE-CHAR: CODE-CHAR. 2. * COERCE: COERCE. 2. * COMMAND: COMMAND. 2. * COMMAND-DESCRIPTOR: COMMAND-DESCRIPTOR. 2. * Common Lisp: Common Lisp. 2. * Common Lisp as a Modeling Language: Common Lisp as a Modeling Language. 2. * COMP: COMP. 2. * COMPILATION: COMPILATION. 2. * COMPLEX: COMPLEX. 2. * COMPLEX-RATIONALP: COMPLEX-RATIONALP. 2. * COMPOUND-RECOGNIZER: COMPOUND-RECOGNIZER. 2. * COMPRESS1: COMPRESS1. 2. * COMPRESS2: COMPRESS2. 2. * COMPUTED-HINTS: COMPUTED-HINTS. 2. * CONCATENATE: CONCATENATE. 2. * COND: COND. 2. * CONGRUENCE: CONGRUENCE. 2. * CONJUGATE: CONJUGATE. 2. * CONS: CONS. 2. * CONSP: CONSP. 2. * CONSTRAINT: CONSTRAINT. 2. * Conversion: Conversion. 2. * COPYRIGHT: COPYRIGHT. 2. * COROLLARY: COROLLARY. 2. * Corroborating Models: Corroborating Models. 2. * CURRENT-PACKAGE: CURRENT-PACKAGE. 2. * CURRENT-THEORY: CURRENT-THEORY. 2. * DECLARE: DECLARE. 2. * DEFAULT: DEFAULT. 2. * DEFAULT-DEFUN-MODE: DEFAULT-DEFUN-MODE. 2. * DEFAULT-PRINT-PROMPT: DEFAULT-PRINT-PROMPT. 2. * DEFAXIOM: DEFAXIOM. 2. * DEFCHOOSE: DEFCHOOSE. 2. * DEFCONG: DEFCONG. 2. * DEFCONST: DEFCONST. 2. * DEFDOC: DEFDOC. 2. * DEFEQUIV: DEFEQUIV. 2. * DEFEVALUATOR: DEFEVALUATOR. 2. * DEFINE-PC-HELP: DEFINE-PC-HELP. 2. * DEFINITION: DEFINITION. 2. * DEFLABEL: DEFLABEL. 2. * DEFMACRO: DEFMACRO. 2. * DEFPKG: DEFPKG. 2. * DEFREFINEMENT: DEFREFINEMENT. 2. * DEFSTUB: DEFSTUB. 2. * DEFTHEORY: DEFTHEORY. 2. * DEFTHM: DEFTHM. 2. * DEFUN: DEFUN. 2. * DEFUN-MODE: DEFUN-MODE. 2. * DEFUN-MODE-CAVEAT: DEFUN-MODE-CAVEAT. 2. * DEFUNS: DEFUNS. 2. * DEFUN-SK: DEFUN-SK. 2. * DENOMINATOR: DENOMINATOR. 2. * DIGIT-CHAR-P: DIGIT-CHAR-P. 2. * DIGIT-TO-CHAR: DIGIT-TO-CHAR. 2. * DIMENSIONS: DIMENSIONS. 2. * DISABLE: DISABLE. 2. * DISABLEDP: DISABLEDP. 2. * DISABLE-FORCING: DISABLE-FORCING. 2. * DOC: DOC. 2. * DOC!: DOC!. 2. * DOCS: DOCS. 2. * DOC-STRING: DOC-STRING. 2. * DOCUMENTATION: DOCUMENTATION. 2. * E0-ORD-<: E0-ORD-<. 2. * E0-ORDINALP: E0-ORDINALP. 2. * EIGHTH: EIGHTH. 2. * ELIM: ELIM. 2. * EMBEDDED-EVENT-FORM: EMBEDDED-EVENT-FORM. 2. * ENABLE: ENABLE. 2. * ENABLE-FORCING: ENABLE-FORCING. 2. * ENCAPSULATE: ENCAPSULATE. 2. * ENDP: ENDP. 2. * ENTER-BOOT-STRAP-MODE: ENTER-BOOT-STRAP-MODE. 2. * EQ: EQ. 2. * EQL: EQL. 2. * EQLABLE-ALISTP: EQLABLE-ALISTP. 2. * EQLABLE-LISTP: EQLABLE-LISTP. 2. * EQLABLEP: EQLABLEP. 2. * EQUAL: EQUAL. 2. * EQUIVALENCE: EQUIVALENCE. 2. * ER-PROGN: ER-PROGN. 2. * ESCAPE-TO-COMMON-LISP: ESCAPE-TO-COMMON-LISP. 2. * Evaluating App on Sample Input: Evaluating App on Sample Input. 2. * EVENP: EVENP. 2. * EVENTS: EVENTS. 2. * EVISCERATE-HIDE-TERMS: EVISCERATE-HIDE-TERMS. 2. * EXECUTABLE-COUNTERPART: EXECUTABLE-COUNTERPART. 2. * EXECUTABLE-COUNTERPART-THEORY: EXECUTABLE-COUNTERPART-THEORY. 2. * EXISTS: EXISTS. 2. * EXIT-BOOT-STRAP-MODE: EXIT-BOOT-STRAP-MODE. 2. * EXPLODE-NONNEGATIVE-INTEGER: EXPLODE-NONNEGATIVE-INTEGER. 2. * EXPT: EXPT. 2. * FAILED-FORCING: FAILED-FORCING. 2. * FAILURE: FAILURE. 2. * FIFTH: FIFTH. 2. * FILE-READING-EXAMPLE: FILE-READING-EXAMPLE. 2. * FIND-RULES-OF-RUNE: FIND-RULES-OF-RUNE. 2. * FIRST: FIRST. 2. * FIX: FIX. 2. * FIX-TRUE-LIST: FIX-TRUE-LIST. 2. * Flawed Induction Candidates in App Example: Flawed Induction Candidates in App Example. 2. * FLOOR: FLOOR. 2. * FMS: FMS. 2. * FMT: FMT. 2. * FMT1: FMT1. 2. * FORALL: FORALL. 2. * FORCE: FORCE. 2. * FORCING-ROUND: FORCING-ROUND. 2. * FORWARD-CHAINING: FORWARD-CHAINING. 2. * FOURTH: FOURTH. 2. * FULL-BOOK-NAME: FULL-BOOK-NAME. 2. * Functions for Manipulating these Objects: Functions for Manipulating these Objects. 2. * FUNCTION-THEORY: FUNCTION-THEORY. 2. * GENERALIZE: GENERALIZE. 2. * GENERALIZED-BOOLEANS: GENERALIZED-BOOLEANS. 2. * GOAL-SPEC: GOAL-SPEC. 2. * GOOD-BYE: GOOD-BYE. 2. * GROUND-ZERO: GROUND-ZERO. 2. * GUARD: GUARD. 2. * GUARD-EXAMPLE: GUARD-EXAMPLE. 2. * GUARD-INTRODUCTION: GUARD-INTRODUCTION. 2. * GUARD-MISCELLANY: GUARD-MISCELLANY. 2. * GUARD-QUICK-REFERENCE: GUARD-QUICK-REFERENCE. 2. * Guards: Guards. 2. * GUARDS-AND-EVALUATION: GUARDS-AND-EVALUATION. 2. * GUARDS-FOR-SPECIFICATION: GUARDS-FOR-SPECIFICATION. 2. * Guessing the Type of a Newly Admitted Function: Guessing the Type of a Newly Admitted Function. 2. * Guiding the ACL2 Theorem Prover: Guiding the ACL2 Theorem Prover. 2. * HEADER: HEADER. 2. * HELP: HELP. 2. * Hey Wait! Is ACL2 Typed or Untyped(Q): Hey Wait! Is ACL2 Typed or Untyped(Q). 2. * HIDE: HIDE. 2. * HINTS: HINTS. 2. * HISTORY: HISTORY. 2. * How Long Does It Take to Become an Effective User(Q): How Long Does It Take to Become an Effective User(Q). 2. * How To Find Out about ACL2 Functions (continued): How To Find Out about ACL2 Functions (continued). 2. * How To Find Out about ACL2 Functions: How To Find Out about ACL2 Functions. 2. * I-AM-HERE: I-AM-HERE. 2. * IDENTITY: IDENTITY. 2. * IF: IF. 2. * IF*: IF*. 2. * IFF: IFF. 2. * IFIX: IFIX. 2. * ILLEGAL: ILLEGAL. 2. * IMAGPART: IMAGPART. 2. * IMMEDIATE-FORCE-MODEP: IMMEDIATE-FORCE-MODEP. 2. * IMPLIES: IMPLIES. 2. * IMPROPER-CONSP: IMPROPER-CONSP. 2. * INCLUDE-BOOK: INCLUDE-BOOK. 2. * INCOMPATIBLE: INCOMPATIBLE. 2. * INDUCTION: INDUCTION. 2. * IN-PACKAGE: IN-PACKAGE. 2. * INSTRUCTIONS: INSTRUCTIONS. 2. * INT=: INT=. 2. * INTEGER-LENGTH: INTEGER-LENGTH. 2. * INTEGER-LISTP: INTEGER-LISTP. 2. * INTEGERP: INTEGERP. 2. * INTERN: INTERN. 2. * INTERN-IN-PACKAGE-OF-SYMBOL: INTERN-IN-PACKAGE-OF-SYMBOL. 2. * INTERSECTION-THEORIES: INTERSECTION-THEORIES. 2. * INTERSECTP-EQ: INTERSECTP-EQ. 2. * INTERSECTP-EQUAL: INTERSECTP-EQUAL. 2. * IN-THEORY: IN-THEORY. 2. * INTRODUCTION: INTRODUCTION. 2. * INVISIBLE-FNS-ALIST: INVISIBLE-FNS-ALIST. 2. * IO: IO. 2. * IRRELEVANT-FORMALS: IRRELEVANT-FORMALS. 2. * KEEP: KEEP. 2. * KEYWORD-COMMANDS: KEYWORD-COMMANDS. 2. * KEYWORDP: KEYWORDP. 2. * KEYWORD-VALUE-LISTP: KEYWORD-VALUE-LISTP. 2. * LAST: LAST. 2. * LD: LD. 2. * LD-ERROR-ACTION: LD-ERROR-ACTION. 2. * LD-ERROR-TRIPLES: LD-ERROR-TRIPLES. 2. * LD-EVISC-TUPLE: LD-EVISC-TUPLE. 2. * LD-KEYWORD-ALIASES: LD-KEYWORD-ALIASES. 2. * LD-POST-EVAL-PRINT: LD-POST-EVAL-PRINT. 2. * LD-PRE-EVAL-FILTER: LD-PRE-EVAL-FILTER. 2. * LD-PRE-EVAL-PRINT: LD-PRE-EVAL-PRINT. 2. * LD-PROMPT: LD-PROMPT. 2. * LD-QUERY-CONTROL-ALIST: LD-QUERY-CONTROL-ALIST. 2. * LD-REDEFINITION-ACTION: LD-REDEFINITION-ACTION. 2. * LD-SKIP-PROOFSP: LD-SKIP-PROOFSP. 2. * LD-VERBOSE: LD-VERBOSE. 2. * LEMMA-INSTANCE: LEMMA-INSTANCE. 2. * LENGTH: LENGTH. 2. * LET: LET. 2. * LET*: LET*. 2. * LINEAR: LINEAR. 2. * LINEAR-ALIAS: LINEAR-ALIAS. 2. * LIST: LIST. 2. * LIST*: LIST*. 2. * LISTP: LISTP. 2. * LOCAL: LOCAL. 2. * LOCAL-INCOMPATIBILITY: LOCAL-INCOMPATIBILITY. 2. * LOGAND: LOGAND. 2. * LOGANDC1: LOGANDC1. 2. * LOGANDC2: LOGANDC2. 2. * LOGBITP: LOGBITP. 2. * LOGCOUNT: LOGCOUNT. 2. * LOGEQV: LOGEQV. 2. * LOGIC: LOGIC. 2. * LOGICAL-NAME: LOGICAL-NAME. 2. * LOGIOR: LOGIOR. 2. * LOGNAND: LOGNAND. 2. * LOGNOR: LOGNOR. 2. * LOGNOT: LOGNOT. 2. * LOGORC1: LOGORC1. 2. * LOGORC2: LOGORC2. 2. * LOGTEST: LOGTEST. 2. * LOGXOR: LOGXOR. 2. * LOOP-STOPPER: LOOP-STOPPER. 2. * LOWER-CASE-P: LOWER-CASE-P. 2. * LP: LP. 2. * MACRO-ALIASES-TABLE: MACRO-ALIASES-TABLE. 2. * MACRO-ARGS: MACRO-ARGS. 2. * MACRO-COMMAND: MACRO-COMMAND. 2. * MAKE-CHARACTER-LIST: MAKE-CHARACTER-LIST. 2. * MAKE-LIST: MAKE-LIST. 2. * MARKUP: MARKUP. 2. * MAX: MAX. 2. * MAXIMUM-LENGTH: MAXIMUM-LENGTH. 2. * MEMBER: MEMBER. 2. * MEMBER-EQ: MEMBER-EQ. 2. * MEMBER-EQUAL: MEMBER-EQUAL. 2. * META: META. 2. * MIN: MIN. 2. * MINUSP: MINUSP. 2. * MISCELLANEOUS: MISCELLANEOUS. 2. * MOD: MOD. 2. * Modeling in ACL2: Modeling in ACL2. 2. * Models in Engineering: Models in Engineering. 2. * Models of Computer Hardware and Software: Models of Computer Hardware and Software. 2. * MONITOR: MONITOR. 2. * MONITORED-RUNES: MONITORED-RUNES. 2. * MORE: MORE. 2. * MORE!: MORE!. 2. * MORE-DOC: MORE-DOC. 2. * MUTUAL-RECURSION: MUTUAL-RECURSION. 2. * MUTUAL-RECURSION-PROOF-EXAMPLE: MUTUAL-RECURSION-PROOF-EXAMPLE. 2. * MV: MV. 2. * MV-LET: MV-LET. 2. * MV-NTH: MV-NTH. 2. * NAME: NAME. 2. * Name the Formula Above: Name the Formula Above. 2. * NFIX: NFIX. 2. * NINTH: NINTH. 2. * NO-DUPLICATESP: NO-DUPLICATESP. 2. * NO-DUPLICATESP-EQUAL: NO-DUPLICATESP-EQUAL. 2. * NONNEGATIVE-INTEGER-QUOTIENT: NONNEGATIVE-INTEGER-QUOTIENT. 2. * NOT: NOT. 2. * NOTE1: NOTE1. 2. * NOTE2: NOTE2. 2. * NOTE3: NOTE3. 2. * NOTE4: NOTE4. 2. * NOTE5: NOTE5. 2. * NOTE6: NOTE6. 2. * NOTE7: NOTE7. 2. * NOTE8: NOTE8. 2. * NOTE8-UPDATE: NOTE8-UPDATE. 2. * NOTE9: NOTE9. 2. * NQTHM-TO-ACL2: NQTHM-TO-ACL2. 2. * NTH: NTH. 2. * NTHCDR: NTHCDR. 2. * NULL: NULL. 2. * Numbers in ACL2: Numbers in ACL2. 2. * NUMERATOR: NUMERATOR. 2. * OBDD: OBDD. 2. * ODDP: ODDP. 2. * OK-IF: OK-IF. 2. * On the Naming of Subgoals: On the Naming of Subgoals. 2. * OOPS: OOPS. 2. * OR: OR. 2. * OTF-FLG: OTF-FLG. 2. * OTHER: OTHER. 2. * Other Requirements: Other Requirements. 2. * Overview of the Expansion of ENDP in the Base Case: Overview of the Expansion of ENDP in the Base Case. 2. * Overview of the Expansion of ENDP in the Induction Step: Overview of the Expansion of ENDP in the Induction Step. 2. * Overview of the Final Simplification in the Base Case: Overview of the Final Simplification in the Base Case. 2. * Overview of the Proof of a Trivial Consequence: Overview of the Proof of a Trivial Consequence. 2. * Overview of the Simplification of the Base Case to T: Overview of the Simplification of the Base Case to T. 2. * Overview of the Simplification of the Induction Conclusion: Overview of the Simplification of the Induction Conclusion. 2. * Overview of the Simplification of the Induction Step to T: Overview of the Simplification of the Induction Step to T. 2. * PACKAGE-REINCARNATION-IMPORT-RESTRICTIONS: PACKAGE-REINCARNATION-IMPORT-RESTRICTIONS. 2. * Pages Written Especially for the Tours: Pages Written Especially for the Tours. 2. * PAIRLIS: PAIRLIS. 2. * PAIRLIS$: PAIRLIS$. 2. * PATHNAME: PATHNAME. 2. * PBT: PBT. 2. * PC: PC. 2. * PCB: PCB. 2. * PCB!: PCB!. 2. * PCS: PCS. 2. * PE: PE. 2. * PE!: PE!. 2. * Perhaps: Perhaps. 2. * PF: PF. 2. * PL: PL. 2. * PLUSP: PLUSP. 2. * Popping out of an Inductive Proof: Popping out of an Inductive Proof. 2. * PORTCULLIS: PORTCULLIS. 2. * POSITION: POSITION. 2. * POSITION-EQ: POSITION-EQ. 2. * POSITION-EQUAL: POSITION-EQUAL. 2. * PPROGN: PPROGN. 2. * PR: PR. 2. * PR!: PR!. 2. * PRINT-DOC-START-COLUMN: PRINT-DOC-START-COLUMN. 2. * PROGN: PROGN. 2. * PROGRAM: PROGRAM. 2. * PROGRAMMING: PROGRAMMING. 2. * PROMPT: PROMPT. 2. * PROOF-CHECKER: PROOF-CHECKER. 2. * PROOF-OF-WELL-FOUNDEDNESS: PROOF-OF-WELL-FOUNDEDNESS. 2. * PROOFS-CO: PROOFS-CO. 2. * PROOF-TREE: PROOF-TREE. 2. * PROOF-TREE-DETAILS: PROOF-TREE-DETAILS. 2. * PROOF-TREE-EXAMPLES: PROOF-TREE-EXAMPLES. 2. * PROPER-CONSP: PROPER-CONSP. 2. * PROPS: PROPS. 2. * Proving Theorems about Models: Proving Theorems about Models. 2. * PSEUDO-TERMP: PSEUDO-TERMP. 2. * PUFF: PUFF. 2. * PUFF*: PUFF*. 2. * PUT-ASSOC-EQ: PUT-ASSOC-EQ. 2. * PUT-ASSOC-EQUAL: PUT-ASSOC-EQUAL. 2. * Q: Q. 2. * RASSOC: RASSOC. 2. * RATIONAL-LISTP: RATIONAL-LISTP. 2. * RATIONALP: RATIONALP. 2. * REALPART: REALPART. 2. * REBUILD: REBUILD. 2. * REDEF: REDEF. 2. * REDEF!: REDEF!. 2. * REDEFINED-NAMES: REDEFINED-NAMES. 2. * REDEFINING-PROGRAMS: REDEFINING-PROGRAMS. 2. * REDUNDANT-EVENTS: REDUNDANT-EVENTS. 2. * REFINEMENT: REFINEMENT. 2. * RELEASE-NOTES: RELEASE-NOTES. 2. * REM: REM. 2. * REMOVE: REMOVE. 2. * REMOVE-DUPLICATES: REMOVE-DUPLICATES. 2. * REMOVE-DUPLICATES-EQUAL: REMOVE-DUPLICATES-EQUAL. 2. * REMOVE-MACRO-ALIAS: REMOVE-MACRO-ALIAS. 2. * RESET-LD-SPECIALS: RESET-LD-SPECIALS. 2. * REST: REST. 2. * RETRIEVE: RETRIEVE. 2. * REVAPPEND: REVAPPEND. 2. * REVERSE: REVERSE. 2. * Revisiting the Admission of App: Revisiting the Admission of App. 2. * REWRITE: REWRITE. 2. * Rewrite Rules are Generated from DEFTHM Events: Rewrite Rules are Generated from DEFTHM Events. 2. * RFIX: RFIX. 2. * ROUND: ROUND. 2. * RULE-CLASSES: RULE-CLASSES. 2. * RULE-NAMES: RULE-NAMES. 2. * RUNE: RUNE. 2. * Running Models: Running Models. 2. * SAVING-AND-RESTORING: SAVING-AND-RESTORING. 2. * SECOND: SECOND. 2. * SET-CBD: SET-CBD. 2. * SET-COMPILE-FNS: SET-COMPILE-FNS. 2. * SET-DIFFERENCE-EQUAL: SET-DIFFERENCE-EQUAL. 2. * SET-DIFFERENCE-THEORIES: SET-DIFFERENCE-THEORIES. 2. * SET-GUARD-CHECKING: SET-GUARD-CHECKING. 2. * SET-IGNORE-OK: SET-IGNORE-OK. 2. * SET-INHIBIT-OUTPUT-LST: SET-INHIBIT-OUTPUT-LST. 2. * SET-INHIBIT-WARNINGS: SET-INHIBIT-WARNINGS. 2. * SET-INVISIBLE-FNS-ALIST: SET-INVISIBLE-FNS-ALIST. 2. * SET-IRRELEVANT-FORMALS-OK: SET-IRRELEVANT-FORMALS-OK. 2. * SET-MEASURE-FUNCTION: SET-MEASURE-FUNCTION. 2. * SET-STATE-OK: SET-STATE-OK. 2. * SET-VERIFY-GUARDS-EAGERNESS: SET-VERIFY-GUARDS-EAGERNESS. 2. * SET-WELL-FOUNDED-RELATION: SET-WELL-FOUNDED-RELATION. 2. * SEVENTH: SEVENTH. 2. * SHOW-BDD: SHOW-BDD. 2. * SIGNATURE: SIGNATURE. 2. * SIGNUM: SIGNUM. 2. * SIMPLE: SIMPLE. 2. * SIXTH: SIXTH. 2. * SKIP-PROOFS: SKIP-PROOFS. 2. * SLOW-ARRAY-WARNING: SLOW-ARRAY-WARNING. 2. * SOLUTION-TO-SIMPLE-EXAMPLE: SOLUTION-TO-SIMPLE-EXAMPLE. 2. * SPECIOUS-SIMPLIFICATION: SPECIOUS-SIMPLIFICATION. 2. * STANDARD-CHAR-LISTP: STANDARD-CHAR-LISTP. 2. * STANDARD-CHAR-P: STANDARD-CHAR-P. 2. * *STANDARD-CI*: *STANDARD-CI*. 2. * STANDARD-CO: STANDARD-CO. 2. * *STANDARD-CO*: *STANDARD-CO*. 2. * STANDARD-OI: STANDARD-OI. 2. * *STANDARD-OI*: *STANDARD-OI*. 2. * START-PROOF-TREE: START-PROOF-TREE. 2. * STARTUP: STARTUP. 2. * STATE: STATE. 2. * STATE is the Only Variable in Top-Level Forms: STATE is the Only Variable in Top-Level Forms. 2. * STOP-PROOF-TREE: STOP-PROOF-TREE. 2. * STRING: STRING. 2. * STRING<: STRING<. 2. * STRING>: STRING>. 2. * STRING<=: STRING<=. 2. * STRING>=: STRING>=. 2. * STRING-ALISTP: STRING-ALISTP. 2. * STRING-APPEND: STRING-APPEND. 2. * STRING-DOWNCASE: STRING-DOWNCASE. 2. * STRING-EQUAL: STRING-EQUAL. 2. * STRING-LISTP: STRING-LISTP. 2. * STRINGP: STRINGP. 2. * STRING-UPCASE: STRING-UPCASE. 2. * STRIP-CARS: STRIP-CARS. 2. * STRIP-CDRS: STRIP-CDRS. 2. * SUBLIS: SUBLIS. 2. * SUBSEQ: SUBSEQ. 2. * SUBSETP: SUBSETP. 2. * SUBSETP-EQUAL: SUBSETP-EQUAL. 2. * SUBST: SUBST. 2. * Subsumption of Induction Candidates in App Example: Subsumption of Induction Candidates in App Example. 2. * SUBVERSIVE-INDUCTIONS: SUBVERSIVE-INDUCTIONS. 2. * Suggested Inductions in the Associativity of App Example: Suggested Inductions in the Associativity of App Example. 2. * SYMBOL-<: SYMBOL-<. 2. * SYMBOL-ALISTP: SYMBOL-ALISTP. 2. * Symbolic Execution of Models: Symbolic Execution of Models. 2. * SYMBOL-LISTP: SYMBOL-LISTP. 2. * SYMBOL-NAME: SYMBOL-NAME. 2. * SYMBOLP: SYMBOLP. 2. * SYMBOL-PACKAGE-NAME: SYMBOL-PACKAGE-NAME. 2. * SYNTAX: SYNTAX. 2. * SYNTAXP: SYNTAXP. 2. * TABLE: TABLE. 2. * TAKE: TAKE. 2. * TENTH: TENTH. 2. * TERM: TERM. 2. * *TERMINAL-MARKUP-TABLE*: *TERMINAL-MARKUP-TABLE*. 2. * TERM-ORDER: TERM-ORDER. 2. * TERM-TABLE: TERM-TABLE. 2. * THE: THE. 2. * The Admission of App: The Admission of App. 2. * The Associativity of App: The Associativity of App. 2. * The Base Case in the App Example: The Base Case in the App Example. 2. * The End of the Flying Tour: The End of the Flying Tour. 2. * The End of the Proof of the Associativity of App: The End of the Proof of the Associativity of App. 2. * The End of the Walking Tour: The End of the Walking Tour. 2. * The Event Summary: The Event Summary. 2. * The Expansion of ENDP in the Induction Step (Step 0): The Expansion of ENDP in the Induction Step (Step 0). 2. * The Expansion of ENDP in the Induction Step (Step 1): The Expansion of ENDP in the Induction Step (Step 1). 2. * The Expansion of ENDP in the Induction Step (Step 2): The Expansion of ENDP in the Induction Step (Step 2). 2. * The Falling Body Model: The Falling Body Model. 2. * The Final Simplification in the Base Case (Step 0): The Final Simplification in the Base Case (Step 0). 2. * The Final Simplification in the Base Case (Step 1): The Final Simplification in the Base Case (Step 1). 2. * The Final Simplification in the Base Case (Step 2): The Final Simplification in the Base Case (Step 2). 2. * The Final Simplification in the Base Case (Step 3): The Final Simplification in the Base Case (Step 3). 2. * The First Application of the Associativity Rule: The First Application of the Associativity Rule. 2. * The Induction Scheme Selected for the App Example: The Induction Scheme Selected for the App Example. 2. * The Induction Step in the App Example: The Induction Step in the App Example. 2. * The Instantiation of the Induction Scheme: The Instantiation of the Induction Scheme. 2. * The Justification of the Induction Scheme: The Justification of the Induction Scheme. 2. * The Proof of the Associativity of App: The Proof of the Associativity of App. 2. * The Q.E.D. Message: The Q.E.D. Message. 2. * The Rules used in the Associativity of App Proof: The Rules used in the Associativity of App Proof. 2. * The Simplification of the Induction Conclusion (Step 0): The Simplification of the Induction Conclusion (Step 0). 2. * The Simplification of the Induction Conclusion (Step 1): The Simplification of the Induction Conclusion (Step 1). 2. * The Simplification of the Induction Conclusion (Step 10): The Simplification of the Induction Conclusion (Step 10). 2. * The Simplification of the Induction Conclusion (Step 11): The Simplification of the Induction Conclusion (Step 11). 2. * The Simplification of the Induction Conclusion (Step 12): The Simplification of the Induction Conclusion (Step 12). 2. * The Simplification of the Induction Conclusion (Step 2): The Simplification of the Induction Conclusion (Step 2). 2. * The Simplification of the Induction Conclusion (Step 3): The Simplification of the Induction Conclusion (Step 3). 2. * The Simplification of the Induction Conclusion (Step 4): The Simplification of the Induction Conclusion (Step 4). 2. * The Simplification of the Induction Conclusion (Step 5): The Simplification of the Induction Conclusion (Step 5). 2. * The Simplification of the Induction Conclusion (Step 6): The Simplification of the Induction Conclusion (Step 6). 2. * The Simplification of the Induction Conclusion (Step 7): The Simplification of the Induction Conclusion (Step 7). 2. * The Simplification of the Induction Conclusion (Step 8): The Simplification of the Induction Conclusion (Step 8). 2. * The Simplification of the Induction Conclusion (Step 9): The Simplification of the Induction Conclusion (Step 9). 2. * The Summary of the Proof of the Trivial Consequence: The Summary of the Proof of the Trivial Consequence. 2. * The Theorem that App is Associative: The Theorem that App is Associative. 2. * The Time Taken to do the Associativity of App Proof: The Time Taken to do the Associativity of App Proof. 2. * The Tours: The Tours. 2. * The WARNING about the Trivial Consequence: The WARNING about the Trivial Consequence. 2. * THEORIES: THEORIES. 2. * THEORY: THEORY. 2. * THEORY-FUNCTIONS: THEORY-FUNCTIONS. 2. * THEORY-INVARIANT: THEORY-INVARIANT. 2. * THIRD: THIRD. 2. * THM: THM. 2. * TIDBITS: TIDBITS. 2. * TIPS: TIPS. 2. * TOGGLE-PC-MACRO: TOGGLE-PC-MACRO. 2. * TRANS: TRANS. 2. * TRANS1: TRANS1. 2. * TRUE-LIST-LISTP: TRUE-LIST-LISTP. 2. * TRUE-LISTP: TRUE-LISTP. 2. * TRUNCATE: TRUNCATE. 2. * TTREE: TTREE. 2. * TUTORIAL1-TOWERS-OF-HANOI: TUTORIAL1-TOWERS-OF-HANOI. 2. * TUTORIAL2-EIGHTS-PROBLEM: TUTORIAL2-EIGHTS-PROBLEM. 2. * TUTORIAL3-PHONEBOOK-EXAMPLE: TUTORIAL3-PHONEBOOK-EXAMPLE. 2. * TUTORIAL4-DEFUN-SK-EXAMPLE: TUTORIAL4-DEFUN-SK-EXAMPLE. 2. * TUTORIAL5-MISCELLANEOUS-EXAMPLES: TUTORIAL5-MISCELLANEOUS-EXAMPLES. 2. * TUTORIAL-EXAMPLES: TUTORIAL-EXAMPLES. 2. * TYPE-PRESCRIPTION: TYPE-PRESCRIPTION. 2. * TYPE-SET: TYPE-SET. 2. * TYPE-SET-INVERTER: TYPE-SET-INVERTER. 2. * TYPE-SPEC: TYPE-SPEC. 2. * U: U. 2. * UBT: UBT. 2. * UBT!: UBT!. 2. * UNARY--: UNARY--. 2. * UNARY-/: UNARY-/. 2. * UNCERTIFIED-BOOKS: UNCERTIFIED-BOOKS. 2. * Undocumented Topic: Undocumented Topic. 2. * UNION-EQ: UNION-EQ. 2. * UNION-EQUAL: UNION-EQUAL. 2. * UNION-THEORIES: UNION-THEORIES. 2. * UNIVERSAL-THEORY: UNIVERSAL-THEORY. 2. * UNMONITOR: UNMONITOR. 2. * UNSAVE: UNSAVE. 2. * UPDATE-NTH: UPDATE-NTH. 2. * UPPER-CASE-P: UPPER-CASE-P. 2. * Using the Associativity of App to Prove a Trivial Consequence: Using the Associativity of App to Prove a Trivial Consequence. 2. * USING-COMPUTED-HINTS: USING-COMPUTED-HINTS. 2. * USING-COMPUTED-HINTS-1: USING-COMPUTED-HINTS-1. 2. * USING-COMPUTED-HINTS-2: USING-COMPUTED-HINTS-2. 2. * USING-COMPUTED-HINTS-3: USING-COMPUTED-HINTS-3. 2. * USING-COMPUTED-HINTS-4: USING-COMPUTED-HINTS-4. 2. * USING-COMPUTED-HINTS-5: USING-COMPUTED-HINTS-5. 2. * USING-COMPUTED-HINTS-6: USING-COMPUTED-HINTS-6. 2. * VERIFY: VERIFY. 2. * VERIFY-GUARDS: VERIFY-GUARDS. 2. * VERIFY-TERMINATION: VERIFY-TERMINATION. 2. * VERSION: VERSION. 2. * WELL-FOUNDED-RELATION: WELL-FOUNDED-RELATION. 2. * What is a Mathematical Logic(Q): What is a Mathematical Logic(Q). 2. * What is a Mechanical Theorem Prover(Q) (continued): What is a Mechanical Theorem Prover(Q) (continued). 2. * What is a Mechanical Theorem Prover(Q): What is a Mechanical Theorem Prover(Q). 2. * What Is ACL2(Q): What Is ACL2(Q). 2. * What is Required of the User(Q): What is Required of the User(Q). 2. * WHY-BRR: WHY-BRR. 2. * WORLD: WORLD. 2. * WORMHOLE: WORMHOLE. 2. * XARGS: XARGS. 2. * You Must Think about the Use of a Formula as a Rule: You Must Think about the Use of a Formula as a Rule. 2. * ZEROP: ZEROP. 2. * ZERO-TEST-IDIOMS: ZERO-TEST-IDIOMS. 2. * ZIP: ZIP. 2. * ZP: ZP. 2.