Info file: acl2-doc-lemacs.info, -*-Text-*- produced by `texinfo-format-buffer' from file `acl2-doc-lemacs.texinfo' using `texinfmt.el' version 2.32 of 19 November 1993. This is documentation for ACL2 Version 1.8 Copyright (C) 1989-95 Computational Logic, Inc. (CLI). All rights reserved.  File: acl2-doc-lemacs.info, Node: REFINEMENT, Next: REWRITE, Prev: META, Up: RULE-CLASSES REFINEMENT record that one equivalence relation refines another *Note RULE-CLASSES:: for a general discussion of rule classes and how they are used to build rules from formulas. An example :corollary formula from which a :refinement rule might be built is: Example: (implies (bag-equal x y) (set-equal y x)). Also *Note DEFREFINEMENT::. General Form: (implies (equiv1 x y) (equiv2 x y)) Equiv1 and equiv2 must be known equivalence relations. The effect of such a rule is to record that equiv1 is a refinement of equiv2. This means that equiv1 :rewrite rules may be used while trying to maintain equiv2. *Note EQUIVALENCE:: for a general discussion of the issues. The macro form (defrefinement equiv1 equiv2) is an abbreviation for a defthm of rule-class :refinement that establishes that equiv1 is a refinement of equiv2. *Note DEFREFINEMENT::. Suppose we have the :rewrite rule (bag-equal (append a b) (append b a)) which states that append is commutative modulo bag-equality. Suppose further we have established that bag-equality refines set-equality. Then when we are simplifying append expressions while maintaining set-equality we use append's commutativity property, even though it was proved for bag-equality. Equality is known to be a refinement of all equivalence relations. The transitive closure of the refinement relation is maintained, so if set-equality, say, is shown to be a refinement of some third sense of equivalence, then bag-equality will automatially be known as a refinement of that third equivalence. :refinement lemmas cannot be disabled. That is, once one equivalence relation has been shown to be a refinement of another, there is no way to prevent the system from using that information. Of course, individual :rewrite rules can be disabled. More will be written about this as we develop the techniques.  File: acl2-doc-lemacs.info, Node: REWRITE, Next: TYPE-PRESCRIPTION, Prev: REFINEMENT, Up: RULE-CLASSES REWRITE make some :rewrite rules (possibly conditional ones) *Note RULE-CLASSES:: for a general discussion of rule classes and how they are used to build rules from formulas. Example :corollary formulas from which :rewrite rules might be built are: Example: (equal (+ x y) (+ y x)) replace (+ a b) by (+ b a) provided certain heuristics approve the permutation. (implies (true-listp x) replace (append a nil) by a, if (equal (append x nil) x)) (true-listp a) rewrites to t (implies replace (member a (append b c)) by (and (eqlablep e) (member a (append c b)) in contexts (true-listp x) in which propositional equivalence (true-listp y)) is sufficient, provided (eqlablep a) (iff (member e (append x y)) (true-listp b) and (true-listp c) (member e (append y x)))) rewrite to t and the permutative heuristics approve General Form: (and ... (implies (and ...hi...) (implies (and ...hk...) (and ... (equiv lhs rhs) ...))) ...) Note: One :rewrite rule class object might create many rewrite rules from the :corollary formula. To create the rules, we first translate the formula (expanding all macros; also *Note TRANS::). Next, we eliminate all lambdas; one may think of this step as simply substituting away every let, let*, and mv-let in the formula. We then flatten the and and implies structure of the formula, transforming it into a conjunction of formulas, each of the form (implies (and h1 ... hn) concl) where no hypothesis is a conjunction and concl is neither a conjunction nor an implication. If necessary, the hypothesis of such a conjunct may be vacuous. We then further coerce each concl into the form (equiv lhs rhs), where equiv is a known equivalence relation, by replacing any concl not of that form by (iff concl t). A concl of the form (not term) is considered to be of the form (iff term nil). By these steps we reduce the given :corollary to a sequence of conjuncts, each of which is of the form (implies (and h1 ... hn) (equiv lhs rhs)) where equiv is a known equivalence relation. *Note EQUIVALENCE::for a general discussion of the introduction of new equivalence relations. We create a :rewrite rule for each such conjunct, if possible, and otherwise cause an error. It is possible to create a rewrite rule from such a conjunct provided lhs is not a variable, a quoted constant, a let-expression, a lambda application, or an if-expression. A :rewrite rule is used when any instance of the lhs occurs in a context in which the equivalence relation is operative. First, we find a substitution that makes lhs equal to the target term. Then we attempt to relieve the instantiated hypotheses of the rule. Hypotheses that are fully instantiated are relieved by recursive rewriting. Hypotheses that contain "free variables" (variables not assigned by the unifying substitution) are relieved by attempting to guess a suitable instance so as to make the hypothesis equal to some known assumption in the context of the target. If the hypotheses are relieved, and certain restrictions that prevent some forms of infinite regress are met (*Note LOOP-STOPPER::), the target is replaced by the instantiated rhs, which is then recursively rewritten. At the moment, the best description of how ACL2 :rewrite rules are used may be found in the discussion of "Replacement Rules" pp 234 of A Computational Logic Handbook.  File: acl2-doc-lemacs.info, Node: TYPE-PRESCRIPTION, Next: TYPE-SET-INVERTER, Prev: REWRITE, Up: RULE-CLASSES TYPE-PRESCRIPTION make a rule that specifies the type of a term *Note RULE-CLASSES:: for a general discussion of rule classes and how they are used to build rules from formulas. Some example :corollary formulas from which :type-prescription rules might be built are: Examples: (implies (nth n lst) is of type characterp (and (character-listp lst) provided the two hypotheses can (< n (length lst))) be established by type reasoning (characterp (nth n lst))). (implies (demodulize a lst 'value ans) is (and (atom a) either a nonnegative integer or (true-listp lst) of the same type as ans, provided (member-equal a lst)) the hyps can be established by type (or (and reasoning (integerp (demodulize a lst 'value ans)) (>= (demodulize a lst 'value ans) 0)) (equal (demodulize a lst 'value ans) ans))). To specify the term whose type (*Note TYPE-SET::) is described by the rule, provide that term as the value of the :typed-term field of the rule class object. General Form: (implies hyps (or type-restriction1-on-pat ... type-restrictionk-on-pat (equal pat var1) ... (equal pat varj))) where pat is the application of some function symbol to some arguments, each type-restrictioni-on-pat is a term involving pat and containing no variables outside of the occurrences of pat, and each vari is one of the variables of pat. Generally speaking, the type-restriction terms ought to be terms that inform us as to the type of pat. Ideally, they should be "primitive recognizing expressions" about pat; *Note COMPOUND-RECOGNIZER::. If the :typed-term is not provided in the rule class object, it is computed heuristically by looking for a term in the conclusion whose type is being restricted. An error is caused if no such term is found. Roughly speaking, the effect of adding such a rule is to inform the ACL2 typing mechanism that pat has the type described by the conclusion, when the hypotheses are true. In particular, the type of pat is within the union of the types described by the several disjuncts. The "type described by" (equal pat vari) is the type of vari. More operationally, when asked to determine the type of a term that is an instance of pat, ACL2 will first attempt to establish the hypotheses. *This is done by type reasoning alone, not rewriting!* Of course, if some hypothesis is to be forced, it is so treated; *Note FORCE::. Provided the hypotheses are established by type reasoning, ACL2 then unions the types described by the type-restrictioni-on-pat terms together with the types of those subexpressions of pat identified by the vari. The final type computed for a term is the intersection of the types implied by each applicable rule. Type prescription rules may be disabled. Because only type reasoning is used to establish the hypotheses of :type-prescription rules, some care must be taken with the hypotheses. Suppose, for example, that the non-recursive function my-statep is defined as (defun my-statep (x) (and (true-listp x) (equal (length x) 2))) and suppose (my-statep s) occurs as a hypothesis of a :type-prescription rule that is being considered for use in the proof attempt for a conjecture with the hypothesis (my-statep s). Since the hypothesis in the conjecture is rewritten, it will become the conjunction of (true-listp s) and (equal (length s) 2). Those two terms will be assumed to have type t in the context in which the :type-prescription rule is tried. But type reasoning will be unable to deduce that (my-statep s) has type t in this context. Thus, either my-statep should be disabled (*Note DISABLE::) during the proof attempt or else the occurrence of (my-statep s) in the :type-prescription rule should be replaced by the conjunction into which it rewrites. While this example makes it clear how non-recursive predicates can cause problems, non-recursive functions in general can cause problems. For example, if (mitigate x) is defined to be (if (rationalp x) (1- x) x) then the hypothesis (pred (mitigate s)) in the conjecture will rewrite, opening mitigate and splitting the conjecture into two subgoals, one in which (rationalp s) and (pred (1- x)) are assumed and the other in which (not (rationalp s)) and (pred x) are assumed. But (pred (mitigate s)) will not be typed as t in either of these contexts. The moral is: beware of non-recursive functions occuring in the hypotheses of :type-prescription rules. Because of the freedom one has in forming the conclusion of a type-prescription, we have to use heuristics to recover the pattern, pat, whose type is being specified. In some cases our heuristics may not identify the intended term and the :type-prescription rule will be rejected as illegal because the conclusion is not of the correct form. When this happens you may wish to specify the pat directly. This may be done by using a suitable rule class token. In particular, when the token :type-prescription is used it means ACL2 is to compute pat with its heuristics; otherwise the token should be of the form (:type-prescription :typed-term pat), where pat is the term whose type is being specified. The defun event may generate a :type-prescription rule. Suppose fn is the name of the function concerned. Then (:type-prescription fn) is the rune given to the type-prescription, if any, generated for fn by defun. (The trivial rule, saying fn has unknown type, is not stored, but defun still allocates the rune and the corollary of this rune is known to be t.)  File: acl2-doc-lemacs.info, Node: TYPE-SET-INVERTER, Next: WELL-FOUNDED-RELATION, Prev: TYPE-PRESCRIPTION, Up: RULE-CLASSES TYPE-SET-INVERTER exhibit a new decoding for an ACL2 type-set *Note RULE-CLASSES:: for a general discussion of rule classes and how they are used to build rules from formulas. Example Rule Class: (:type-set-inverter :corollary (equal (and (counting-number x) (not (equal x 0))) (and (integerp x) (< x 0))) :type-set 2) General Forms of Rule Class: :type-set-inverter, or (:type-set-inverter :type-set n) General Form of Theorem or Corollary: (EQUAL new-expr old-expr) where n is a type-set (*Note TYPE-SET::) and old-expr is the term containing x as a free variable that ACL2 currently uses to recognize type-set n. For a given n, the exact form of old-expr is generated by (convert-type-set-to-term 'x n (ens state) (w state) nil)]. If the :type-set field of the rule-class is omitted, we attempt to compute it from the right-hand side, old-expr, of the corollary. That computation is done by type-set-implied-by-term (*Note TYPE-SET::). However, it is possible that the type-set we compute from lhs does not have the required property that when inverted with convert-type-set-to-term the result is lhs. If you omit :type-set and an error is caused because lhs has the incorrect form, you should manually specify both :type-set and the lhs generated by convert-type-set-to-term. The rule generated will henceforth make new-expr be the term used by ACL2 to recognize type-set n. If this rule is created by a defthm event named name then the rune of the rule is (:type-set-inverter name) and by disabling that rune you can prevent its being used to decode type-sets. Type-sets are inverted when forced assumptions are turned into formulas to be proved. In their internal form, assumptions are essentially pairs consisting of a context and a goal term, which was forced. Abstractly a context is just a list of hypotheses which may be assumed while proving the goal term. But actually contexts are alists which pair terms with type-sets, encoding the current hypotheses. For example, if the original conjecture contained the hypothesis (integerp x) then the context used while working on that conjecture will include the assignment to x of the type-set *ts-integer*.  File: acl2-doc-lemacs.info, Node: WELL-FOUNDED-RELATION, Prev: TYPE-SET-INVERTER, Up: RULE-CLASSES WELL-FOUNDED-RELATION show that a relation is well-founded on a set *Note RULE-CLASSES:: for a general discussion of rule classes and how they are used to build rules from formulas. An example :corollary formula from which a :well-founded-relation rule might be built is as follows. (Of course, the functions pairp, lex2p, and ordinate would have to be defined first.) Example: (and (implies (pairp x) (e0-ordinalp (ordinate x))) (implies (and (pairp x) (pairp y) (lex2p x y)) (e0-ord-< (ordinate x) (ordinate y)))) The above example establishes that lex2p is a well-founded relation on pairps. We explain and give details below. Exactly two general forms are recognized: General Forms (AND (IMPLIES (mp x) (E0-ORDINALP (fn x))) ; Property 1 (IMPLIES (AND (mp x) ; Property 2 (mp y) (rel x y)) (E0-ORD-< (fn x) (fn y)))), or (AND (E0-ORDINALP (fn x)) ; Property 1 (IMPLIES (rel x y) ; Property 2 (E0-ORD-< (fn x) (fn y)))) where mp, fn, and rel are function symbols, x and y are distinct variable symbols, and no other :well-founded-relation theorem about fn has been proved. When the second general form is used, we act as though the first form were used with mp being the function that ignores its argument and returns t. The discussion below therefore considers only the first general form. Note: We are very rigid when checking that the submitted formula is of one of these forms. For example, in the first form, we insist that all the conjuncts appear in the order shown above. Thus, interchanging the two properties in the top-level conjunct or rearranging the hyptheses in the second conjunct both produce unrecognized forms. The requirement that each fn be proved well-founded at most once insures that for each well-founded relation, fn, there is a unique mp that recognizes the domain on which rel is well-founded. We impose this requirement simply so that rel can be used as a short-hand when specifying the well-founded relations to be used in definitions; otherwise the specification would have to indicate which mp was to be used. Mp is a predicate that recognizes the objects that are supposedly ordered in a well-founded way by rel. We call such an object an "mp-measure" or simply a "measure" when mp is understood. Property 1 tells us that every measure can be mapped into an ACL2 ordinal. (*Note E0-ORDINALP::.) This mapping is performed by fn. Property 2 tells us that if the measure x is smaller than the measure y according to rel then the image of x under fn is a smaller than that of y, according to the well-founded relation e0-ord-<. (*Note E0-ORD-<::.) Thus, the general form of a :well-founded-relation formula establishes that there exists a rel-order preserving embedding (namely via fn) of the mp-measures into the ordinals. We can thus conclude that rel is well-founded on mp-measures. Such well-founded relations are used in the admissibility test for recursive functions, in particular, to show that the recursion terminates. To illustrate how such information may be used, consider a generic function definition (defun g (x) (if (test x) (g (step x)) (base x))). If rel has been shown to be well-founded on mp-measures, then g's termination can be insured by finding a measure, (m x), with the property that m produces a measure: (mp (m x)), ; Defun-goal-1 and that the argument to g gets smaller (when measured by m and compared by rel) in the recursion, (implies (test x) (rel (m (step x)) (m x))). ; Defun-goal-2 If rel is selected as the :well-founded-relation to be used in the definition of g, the definitional principal will generate and attempt to prove defun-goal-1 and defun-goal-2 to justify g. We show later why these two goals are sufficient to establish the termination of g. Observe that neither the ordinals nor the embedding, fn, of the mp-measures into the ordinals is involved in the goals generated by the definitional principal. Suppose now that a :well-founded-relation theorem has been proved for mp and rel. How can rel be "selected as the :well-founded-relation" by defun? There are two ways. First, an xargs keyword to the defun event allows the specification of a :well-founded-relation. Thus, the definition of g above might be written (defun g (x) (declare (xargs :well-founded-relation (mp . rel))) (if (test x) (g (step x)) (base x))) Alternatively, rel may be specified as the :default-well-founded-relation in acl2-defaults-table by executing the event (set-default-well-founded-relation rel). When a defun event does not explicitly specify the relation in its xargs the default relation is used. When ACL2 is initialized, the default relation is e0-ord-<. Finally, though it is probably obvious, we now show that defun-goal-1 and defun-goal-2 are sufficient to insure the termination of g provided property-1 and property-2 of mp and rel have been proved. To this end, assume we have proved defun-goal-1 and defun-goal-2 as well as property-1 and property-2 and we show how to admit g under the primitive ACL2 definitional principal (i.e., using only the ordinals). In particular, consider the definition event (defun g (x) (declare (xargs :well-founded-relation e0-ord-< :measure (fn (m x)))) (if (test x) (g (step x)) (base x))) Proof that g is admissible: To admit the definition of g above we must prove (e0-ordinalp (fn (m x))) ; *1 and (implies (test x) ; *2 (e0-ord-< (fn (m (step x))) (fn (m x)))). But *1 can be proved by instantiating property-1 to get (implies (mp (m x)) (e0-ordinalp (fn (m x)))), and then relieving the hypothesis with defun-goal-1, (mp (m x)). Similarly, *2 can be proved by instantiating property-2 to get (implies (and (mp (m (step x))) (mp (m x)) (rel (m (step x)) (m x))) (e0-ord-< (fn (m (step x))) (fn (m x)))) and relieving the first two hypotheses by appealing to two instances of defun-goal-1, thus obtaining (implies (rel (m (step x)) (m x)) (e0-ord-< (fn (m (step x))) (fn (m x)))). By chaining this together with defun-goal-2, (implies (test x) (rel (m (step x)) (m x))) we obtain *2. Q.E.D.  File: acl2-doc-lemacs.info, Node: THEORIES, Prev: RULE-CLASSES, Up: Top THEORIES sets of runes to enable/disable in concert Example: '((:definition app) (:executable-counterpart app) rv (rv) assoc-of-app) See: * Menu: * 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 * GROUND-ZERO:: enabled rules in the startup theory * INCOMPATIBLE:: declaring that two rules should not both be enabled * INTERSECTION-THEORIES:: intersect two theories * RULE-NAMES:: How rules are named. * RUNE:: a rule name * SET-DIFFERENCE-THEORIES:: difference of two theories * THEORY:: retrieve named theory * THEORY-FUNCTIONS:: functions for obtaining or producing theories * UNION-THEORIES:: union two theories * UNIVERSAL-THEORY:: all rules as of logical name A theory is a list of "runic designators" as described below. Each runic designator denotes a set of "runes" (*Note RUNE::) and by unioning together the runes denoted by each member of a theory we define the set of runes corresponding to a theory. Theories are used to control which rules are "enabled," i.e., available for automatic application by the theorem prover. There is always a "current" theory. A rule is enabled precisely if its rune is an element of the set of runes corresponding to the current theory. At the top-level, the current theory is the theory selected by the most recent in-theory event, extended with the rule names introduced since then. Inside the theorem prover, the :in-theory hint (*Note HINTS::) can be used to select a particular theory as current during the proof attempt for a particular goal. Theories are generally constructed by "theory expressions." Formally, a theory expression is any term, containing at most the single free variable world, that when evaluated with world bound to the current ACL2 world (*Note WORLD::) produces a theory. ACL2 provides various functions for the convenient construction and manipulation of theories. These are called "theory functions" (*Note THEORY-FUNCTIONS::). For example, the theory function union-theories takes two theories and produces their union. The theory function universal-theory returns the theory containing all known rule names as of the introduction of a given logical name. But a theory expression can contain constants, e.g., '(assoc (assoc) (:rewrite car-cons) car-cdr-elim) and user-defined functions. The only important criterion is that a theory expression mention no variable freely except world and evaluate to a theory. More often than not, theory expressions typed by the user do not mention the variable world. This is because user-typed theory expressions are generally composed of applications of ACL2's theory functions. These "functions" are actually macros that expand into terms in which world is used freely and appropriately. Thus, the technical definition of "theory expression" should not mislead you into thinking that interestng theory expressions must mention world; they probably do and you just didn't know it! One aspect of this arrangement is that theory expressions cannot generally be evaluated at the top-level of ACL2, because world is not bound. To see the value of a theory expression, expr, at the top-level, type ACL2 !>(LET ((WORLD (W STATE))) expr). However, because the built-in theories are quite long, you may be sorry you printed the value of a theory expression! A theory is a true list of runic designators and to each theory there corresponds a set of runes, obtained by unioning together the sets of runes denoted by each runic designator. For example, the theory constant '(assoc (assoc) (:rewrite car-cons) car-cdr-elim) corresponds to the set of runes {(:definition assoc) (:executable-counterpart assoc) (:rewrite car-cons) (:rewrite car-cdr-elim) (:elim car-cdr-elim)} . Observe that the theory contains four elements but its runic correspondent contains five. That is because some designators denote sets of several runes. If the above theory were selected as current then the five rules named in its runic counterpart would be enabled and all other rules would be disabled. We now precisely define the runic designators and the set of runes denoted by each. o A rune is a runic designator and denotes the singleton set containing that rune. o If symb is a function symbol introduced with a defun (or defuns) event, then symb is a runic designator and denotes the singleton set containing the rune (:definition symb). o If symb is a function symbol introduced with a defun (or defuns) event, then (symb) is a runic designator and denotes the singleton set containing the rune (:executable-counterpart symb). o If symb is the name of a defthm (or defaxiom) event that introduced at least one rule, then symb is a runic designator and denotes the set of the names of all rules introduced by the named event. o If str is the string naming some defpkg event and symb is the symbol returned by (intern str "ACL2"), then symb is a runic designator and denotes the singleton set containing (:rewrite symb), which is the name of the rule stating the conditions under which the symbol-package-name of (intern x str) is str. o If symb is the name of a deftheory event, then symb is a runic designator and denotes the runic theory corresponding to symb. These conventions attempt to implement the Nqthm-1992 treatment of theories. For example, including a function name, e.g., assoc, in the current theory enables that function but does not enable the executable counterpart. Similarly, including (assoc) enables the executable counterpart (Nqthm's *1*assoc) but not the symbolic definition. And including the name of a proved lemma enables all of the rules added by the event. These conventions are entirely consistent with Nqthm usage. Of course, in ACL2 one can include explicitly the runes naming the rules in question and so can avoid entirely the use of non-runic elements in theories. Because a rune is a runic designator denoting the set containing that rune, a list of runes is a theory and denotes itself. We call such theories "runic theories." To every theory there corresponds a runic theory obtained by unioning together the sets denoted by each designator in the theory. When a theory is selected as "current" it is actually its runic correspondent that is effectively used. That is, a rune is enabled iff it is a member of the runic correspondent of the current theory. The value of a theory defined with deftheory is the runic correspondent of the theory computed by the defining theory expression. The theory manipulation functions, e.g., union-theories, actually convert their theory arguments to their runic correspondents before performing the required set operation. The manipulation functions always return runic theories. Thus, it is sometimes convenient to think of (non-runic) theories as merely abbreviations for their runic correspondents, abbreviations which are "expanded" at the first opportunity by theory manipulation functions and the "theory consumer" functions such as in-theory and deftheory.  File: acl2-doc-lemacs.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) *Note LOGICAL-NAME::. General Form: (current-theory logical-name) Returns the current theory as it existed immediately after the introduction of logical-name. *Note THEORIES:: and *Note LOGICAL-NAME::. This 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. *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-lemacs.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; *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-lemacs.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; *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-lemacs.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) *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. *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-lemacs.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) *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. *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-lemacs.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; *Note THEORIES::. In fact, this theory is just the theory defined by (current-theory :here) at the conclusion of initialization; *Note CURRENT-THEORY::. Note that by executing the event (in-theory 'ground-zero), you can restore the current theory to its value at the time you started up ACL2.  File: acl2-doc-lemacs.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. *Note THEORY-INVARIANT::.  File: acl2-doc-lemacs.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 (*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-lemacs.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) *Note RUNE::.  File: acl2-doc-lemacs.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; *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. *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 *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-lemacs.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 (*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-lemacs.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. *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-lemacs.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. (*Note THEORIES::.) Some, like universal-theory, take a logical name (*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. *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 (*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-lemacs.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 (*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-lemacs.info, Node: UNIVERSAL-THEORY, Prev: UNION-THEORIES, Up: THEORIES UNIVERSAL-THEORY all rules as of logical name Examples: (universal-theory :here) (universal-theory 'lemma3) *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. *Note THEORIES::and *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. *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-lemacs.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. * ABS: ABS. 2. * ACCUMULATED-PERSISTENCE: ACCUMULATED-PERSISTENCE. 2. * ACKNOWLEDGEMENTS: ACKNOWLEDGEMENTS. 2. * ACL2-CHARACTERP: ACL2-CHARACTERP. 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. * 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. * 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. * CODE-CHAR: CODE-CHAR. 2. * COERCE: COERCE. 2. * COMMAND: COMMAND. 2. * COMMAND-DESCRIPTOR: COMMAND-DESCRIPTOR. 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. * CONCATENATE: CONCATENATE. 2. * COND: COND. 2. * CONGRUENCE: CONGRUENCE. 2. * CONJUGATE: CONJUGATE. 2. * CONS: CONS. 2. * CONSP: CONSP. 2. * CONSTRAINT: CONSTRAINT. 2. * COPYRIGHT: COPYRIGHT. 2. * COROLLARY: COROLLARY. 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. * 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. * 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. * 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-AND-EVALUATION: GUARDS-AND-EVALUATION. 2. * GUARDS-FOR-SPECIFICATION: GUARDS-FOR-SPECIFICATION. 2. * HEADER: HEADER. 2. * HELP: HELP. 2. * HIDE: HIDE. 2. * HINTS: HINTS. 2. * HISTORY: HISTORY. 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. * 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. * NFIX: NFIX. 2. * NINTH: NINTH. 2. * NO-DUPLICATESP: NO-DUPLICATESP. 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. * NQTHM-TO-ACL2: NQTHM-TO-ACL2. 2. * NTH: NTH. 2. * NTHCDR: NTHCDR. 2. * NULL: NULL. 2. * NUMERATOR: NUMERATOR. 2. * OBDD: OBDD. 2. * ODDP: ODDP. 2. * OK-IF: OK-IF. 2. * OOPS: OOPS. 2. * OR: OR. 2. * OTF-FLG: OTF-FLG. 2. * OTHER: OTHER. 2. * PACKAGE-REINCARNATION-IMPORT-RESTRICTIONS: PACKAGE-REINCARNATION-IMPORT-RESTRICTIONS. 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. * PF: PF. 2. * PL: PL. 2. * PLUSP: PLUSP. 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. * 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. * REWRITE: REWRITE. 2. * RFIX: RFIX. 2. * ROUND: ROUND. 2. * RULE-CLASSES: RULE-CLASSES. 2. * RULE-NAMES: RULE-NAMES. 2. * RUNE: RUNE. 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-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. * 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. * SUBVERSIVE-INDUCTIONS: SUBVERSIVE-INDUCTIONS. 2. * SYMBOL-<: SYMBOL-<. 2. * SYMBOL-ALISTP: SYMBOL-ALISTP. 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. * 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. * 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. * 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. * VERIFY: VERIFY. 2. * VERIFY-GUARDS: VERIFY-GUARDS. 2. * VERIFY-TERMINATION: VERIFY-TERMINATION. 2. * WELL-FOUNDED-RELATION: WELL-FOUNDED-RELATION. 2. * WHY-BRR: WHY-BRR. 2. * WORLD: WORLD. 2. * WORMHOLE: WORMHOLE. 2. * XARGS: XARGS. 2. * ZEROP: ZEROP. 2. * ZERO-TEST-IDIOMS: ZERO-TEST-IDIOMS. 2. * ZIP: ZIP. 2. * ZP: ZP. 2.