(("+" "+" "+.html" "" "+") ("1+" "1+" "1+.html" "" "1+") ("1-" "1-" "1-.html" "" "1-") ("=" "=" "=.html" "" "=") ("abs" "abs" "ABS.html" "" "abs") ("accumulated-persistence" "accumulated-persistence" "ACCUMULATED-PERSISTENCE.html" "" "accumulated-persistence") ("acknowledgments" "acknowledgments" "ACKNOWLEDGMENTS.html" "" "acknowledgments") ("acl2-count" "acl2-count" "ACL2-COUNT.html" "" "acl2-count") ("acl2-customization" "acl2-customization" "ACL2-CUSTOMIZATION.html" "" "acl2-customization") ("acl2-defaults-table" "acl2-defaults-table" "ACL2-DEFAULTS-TABLE.html" "" "acl2-defaults-table") ("acl2-help" "acl2-help" "ACL2-HELP.html" "" "acl2-help") ("acl2-numberp" "acl2-numberp" "ACL2-NUMBERP.html" "" "acl2-numberp") ("acl2-tutorial" "acl2-tutorial" "ACL2-TUTORIAL.html" "" "acl2-tutorial") ("acl2-user" "acl2-user" "ACL2-USER.html" "" "acl2-user") ("acons" "acons" "ACONS.html" "" "acons") ("active-runep" "active-runep" "ACTIVE-RUNEP.html" "" "active-runep") ("add-binop" "add-binop" "ADD-BINOP.html" "" "add-binop") ("add-default-hints" "add-default-hints" "ADD-DEFAULT-HINTS.html" "" "add-default-hints") ("add-dive-into-macro" "add-dive-into-macro" "ADD-DIVE-INTO-MACRO.html" "" "add-dive-into-macro") ("add-include-book-dir" "add-include-book-dir" "ADD-INCLUDE-BOOK-DIR.html" "" "add-include-book-dir") ("add-invisible-fns" "add-invisible-fns" "ADD-INVISIBLE-FNS.html" "" "add-invisible-fns") ("add-macro-alias" "add-macro-alias" "ADD-MACRO-ALIAS.html" "" "add-macro-alias") ("add-match-free-override" "add-match-free-override" "ADD-MATCH-FREE-OVERRIDE.html" "" "add-match-free-override") ("add-nth-alias" "add-nth-alias" "ADD-NTH-ALIAS.html" "" "add-nth-alias") ("add-raw-arity" "add-raw-arity" "ADD-RAW-ARITY.html" "" "add-raw-arity") ("add-to-set-eq" "add-to-set-eq" "ADD-TO-SET-EQ.html" "" "add-to-set-eq") ("add-to-set-eql" "add-to-set-eql" "ADD-TO-SET-EQL.html" "" "add-to-set-eql") ("add-to-set-equal" "add-to-set-equal" "ADD-TO-SET-EQUAL.html" "" "add-to-set-equal") ("alistp" "alistp" "ALISTP.html" "" "alistp") ("allocate-fixnum-range" "allocate-fixnum-range" "ALLOCATE-FIXNUM-RANGE.html" "" "allocate-fixnum-range") ("alpha-char-p" "alpha-char-p" "ALPHA-CHAR-P.html" "" "alpha-char-p") ("alphorder" "alphorder" "ALPHORDER.html" "" "alphorder") ("and" "and" "AND.html" "" "and") ("append" "append" "APPEND.html" "" "append") ("apropos" "apropos" "APROPOS.html" "" "apropos") ("aref1" "aref1" "AREF1.html" "" "aref1") ("aref2" "aref2" "AREF2.html" "" "aref2") ("args" "args" "ARGS.html" "" "args") ("array1p" "array1p" "ARRAY1P.html" "" "array1p") ("array2p" "array2p" "ARRAY2P.html" "" "array2p") ("arrays-example" "arrays-example" "ARRAYS-EXAMPLE.html" "" "arrays-example") ("arrays" "arrays" "ARRAYS.html" "" "arrays") ("aset1" "aset1" "ASET1.html" "" "aset1") ("aset2" "aset2" "ASET2.html" "" "aset2") ("ash" "ash" "ASH.html" "" "ash") ("assert$" "assert$" "ASSERT$.html" "" "assert$") ("assert-event" "assert-event" "ASSERT-EVENT.html" "" "assert-event") ("assign" "assign" "ASSIGN.html" "" "assign") ("assoc-eq" "assoc-eq" "ASSOC-EQ.html" "" "assoc-eq") ("assoc-equal" "assoc-equal" "ASSOC-EQUAL.html" "" "assoc-equal") ("assoc-keyword" "assoc-keyword" "ASSOC-KEYWORD.html" "" "assoc-keyword") ("assoc-string-equal" "assoc-string-equal" "ASSOC-STRING-EQUAL.html" "" "assoc-string-equal") ("assoc" "assoc" "ASSOC.html" "" "assoc") ("atom-listp" "atom-listp" "ATOM-LISTP.html" "" "atom-listp") ("atom" "atom" "ATOM.html" "" "atom") ("backchain-limit" "backchain-limit" "BACKCHAIN-LIMIT.html" "" "backchain-limit") ("bdd-algorithm" "bdd-algorithm" "BDD-ALGORITHM.html" "" "bdd-algorithm") ("bdd-introduction" "bdd-introduction" "BDD-INTRODUCTION.html" "" "bdd-introduction") ("bdd" "bdd" "BDD.html" "" "bdd") ("bibliography" "bibliography" "BIBLIOGRAPHY.html" "" "bibliography") ("binary-+" "binary-+" "BINARY-+.html" "" "binary-+") ("binary-append" "binary-append" "BINARY-APPEND.html" "" "binary-append") ("bind-free-examples" "bind-free-examples" "BIND-FREE-EXAMPLES.html" "" "bind-free-examples") ("bind-free" "bind-free" "BIND-FREE.html" "" "bind-free") ("binop-table" "binop-table" "BINOP-TABLE.html" "" "binop-table") ("book-contents" "book-contents" "BOOK-CONTENTS.html" "" "book-contents") ("book-example" "book-example" "BOOK-EXAMPLE.html" "" "book-example") ("book-makefiles" "book-makefiles" "BOOK-MAKEFILES.html" "" "book-makefiles") ("book-name" "book-name" "BOOK-NAME.html" "" "book-name") ("books" "books" "BOOKS.html" "" "books") ("booleanp" "booleanp" "BOOLEANP.html" "" "booleanp") ("break-lemma" "break-lemma" "BREAK-LEMMA.html" "" "break-lemma") ("break-on-error" "break-on-error" "BREAK-ON-ERROR.html" "" "break-on-error") ("break-rewrite" "break-rewrite" "BREAK-REWRITE.html" "" "break-rewrite") ("breaks" "breaks" "BREAKS.html" "" "breaks") ("brr-commands" "brr-commands" "BRR-COMMANDS.html" "" "brr-commands") ("brr" "brr" "BRR.html" "" "brr") ("built-in-clauses" "built-in-clauses" "BUILT-IN-CLAUSES.html" "" "built-in-clauses") ("butlast" "butlast" "BUTLAST.html" "" "butlast") ("by" "by" "BY.html" "" "by") ("caaaar" "caaaar" "CAAAAR.html" "" "caaaar") ("caaadr" "caaadr" "CAAADR.html" "" "caaadr") ("caaar" "caaar" "CAAAR.html" "" "caaar") ("caadar" "caadar" "CAADAR.html" "" "caadar") ("caaddr" "caaddr" "CAADDR.html" "" "caaddr") ("caadr" "caadr" "CAADR.html" "" "caadr") ("caar" "caar" "CAAR.html" "" "caar") ("cadaar" "cadaar" "CADAAR.html" "" "cadaar") ("cadadr" "cadadr" "CADADR.html" "" "cadadr") ("cadar" "cadar" "CADAR.html" "" "cadar") ("caddar" "caddar" "CADDAR.html" "" "caddar") ("cadddr" "cadddr" "CADDDR.html" "" "cadddr") ("caddr" "caddr" "CADDR.html" "" "caddr") ("cadr" "cadr" "CADR.html" "" "cadr") ("car" "car" "CAR.html" "" "car") ("case-match" "case-match" "CASE-MATCH.html" "" "case-match") ("case-split-limitations" "case-split-limitations" "CASE-SPLIT-LIMITATIONS.html" "" "case-split-limitations") ("case-split" "case-split" "CASE-SPLIT.html" "" "case-split") ("case" "case" "CASE.html" "" "case") ("cases" "cases" "CASES.html" "" "cases") ("cbd" "cbd" "CBD.html" "" "cbd") ("cdaaar" "cdaaar" "CDAAAR.html" "" "cdaaar") ("cdaadr" "cdaadr" "CDAADR.html" "" "cdaadr") ("cdaar" "cdaar" "CDAAR.html" "" "cdaar") ("cdadar" "cdadar" "CDADAR.html" "" "cdadar") ("cdaddr" "cdaddr" "CDADDR.html" "" "cdaddr") ("cdadr" "cdadr" "CDADR.html" "" "cdadr") ("cdar" "cdar" "CDAR.html" "" "cdar") ("cddaar" "cddaar" "CDDAAR.html" "" "cddaar") ("cddadr" "cddadr" "CDDADR.html" "" "cddadr") ("cddar" "cddar" "CDDAR.html" "" "cddar") ("cdddar" "cdddar" "CDDDAR.html" "" "cdddar") ("cddddr" "cddddr" "CDDDDR.html" "" "cddddr") ("cdddr" "cdddr" "CDDDR.html" "" "cdddr") ("cddr" "cddr" "CDDR.html" "" "cddr") ("cdr" "cdr" "CDR.html" "" "cdr") ("ceiling" "ceiling" "CEILING.html" "" "ceiling") ("certificate" "certificate" "CERTIFICATE.html" "" "certificate") ("certify-book" "certify-book" "CERTIFY-BOOK.html" "" "certify-book") ("char-code" "char-code" "CHAR-CODE.html" "" "char-code") ("char-downcase" "char-downcase" "CHAR-DOWNCASE.html" "" "char-downcase") ("char-equal" "char-equal" "CHAR-EQUAL.html" "" "char-equal") ("char-upcase" "char-upcase" "CHAR-UPCASE.html" "" "char-upcase") ("char" "char" "CHAR.html" "" "char") ("character-listp" "character-listp" "CHARACTER-LISTP.html" "" "character-listp") ("characterp" "characterp" "CHARACTERP.html" "" "characterp") ("characters" "characters" "CHARACTERS.html" "" "characters") ("check-sum" "check-sum" "CHECK-SUM.html" "" "check-sum") ("checkpoint-forced-goals" "checkpoint-forced-goals" "CHECKPOINT-FORCED-GOALS.html" "" "checkpoint-forced-goals") ("clause-identifier" "clause-identifier" "CLAUSE-IDENTIFIER.html" "" "clause-identifier") ("close-input-channel" "close-input-channel" "CLOSE-INPUT-CHANNEL.html" "" "close-input-channel") ("close-output-channel" "close-output-channel" "CLOSE-OUTPUT-CHANNEL.html" "" "close-output-channel") ("close-trace-file" "close-trace-file" "CLOSE-TRACE-FILE.html" "" "close-trace-file") ("code-char" "code-char" "CODE-CHAR.html" "" "code-char") ("coerce" "coerce" "COERCE.html" "" "coerce") ("command-descriptor" "command-descriptor" "COMMAND-DESCRIPTOR.html" "" "command-descriptor") ("command" "command" "COMMAND.html" "" "command") ("comp-gcl" "comp-gcl" "COMP-GCL.html" "" "comp-gcl") ("comp" "comp" "COMP.html" "" "comp") ("compilation" "compilation" "COMPILATION.html" "" "compilation") ("complex-rationalp" "complex-rationalp" "COMPLEX-RATIONALP.html" "" "complex-rationalp") ("complex" "complex" "COMPLEX.html" "" "complex") ("compound-recognizer" "compound-recognizer" "COMPOUND-RECOGNIZER.html" "" "compound-recognizer") ("compress1" "compress1" "COMPRESS1.html" "" "compress1") ("compress2" "compress2" "COMPRESS2.html" "" "compress2") ("computed-hints" "computed-hints" "COMPUTED-HINTS.html" "" "computed-hints") ("concatenate" "concatenate" "CONCATENATE.html" "" "concatenate") ("cond" "cond" "COND.html" "" "cond") ("congruence" "congruence" "CONGRUENCE.html" "" "congruence") ("conjugate" "conjugate" "CONJUGATE.html" "" "conjugate") ("cons" "cons" "CONS.html" "" "cons") ("conservativity-of-defchoose" "conservativity-of-defchoose" "CONSERVATIVITY-OF-DEFCHOOSE.html" "" "conservativity-of-defchoose") ("consp" "consp" "CONSP.html" "" "consp") ("constraint" "constraint" "CONSTRAINT.html" "" "constraint") ("copyright" "copyright" "COPYRIGHT.html" "" "copyright") ("corollary" "corollary" "COROLLARY.html" "" "corollary") ("current-package" "current-package" "CURRENT-PACKAGE.html" "" "current-package") ("current-theory" "current-theory" "CURRENT-THEORY.html" "" "current-theory") ("cw-gstack" "cw-gstack" "CW-GSTACK.html" "" "cw-gstack") ("cw" "cw" "CW.html" "" "cw") ("declare-stobjs" "declare-stobjs" "DECLARE-STOBJS.html" "" "declare-stobjs") ("declare" "declare" "DECLARE.html" "" "declare") ("defabbrev" "defabbrev" "DEFABBREV.html" "" "defabbrev") ("default-backchain-limit" "default-backchain-limit" "DEFAULT-BACKCHAIN-LIMIT.html" "" "default-backchain-limit") ("default-defun-mode" "default-defun-mode" "DEFAULT-DEFUN-MODE.html" "" "default-defun-mode") ("default-hints-table" "default-hints-table" "DEFAULT-HINTS-TABLE.html" "" "default-hints-table") ("default-hints" "default-hints" "DEFAULT-HINTS.html" "" "default-hints") ("default-print-prompt" "default-print-prompt" "DEFAULT-PRINT-PROMPT.html" "" "default-print-prompt") ("default" "default" "DEFAULT.html" "" "default") ("defaxiom" "defaxiom" "DEFAXIOM.html" "" "defaxiom") ("defchoose" "defchoose" "DEFCHOOSE.html" "" "defchoose") ("defcong" "defcong" "DEFCONG.html" "" "defcong") ("defconst" "defconst" "DEFCONST.html" "" "defconst") ("defdoc" "defdoc" "DEFDOC.html" "" "defdoc") ("defequiv" "defequiv" "DEFEQUIV.html" "" "defequiv") ("defevaluator" "defevaluator" "DEFEVALUATOR.html" "" "defevaluator") ("defexec" "defexec" "DEFEXEC.html" "" "defexec") ("define-pc-help" "define-pc-help" "DEFINE-PC-HELP.html" "" "define-pc-help") ("define-pc-macro" "define-pc-macro" "DEFINE-PC-MACRO.html" "" "define-pc-macro") ("define-pc-meta" "define-pc-meta" "DEFINE-PC-META.html" "" "define-pc-meta") ("definition" "definition" "DEFINITION.html" "" "definition") ("deflabel" "deflabel" "DEFLABEL.html" "" "deflabel") ("defmacro" "defmacro" "DEFMACRO.html" "" "defmacro") ("defpkg" "defpkg" "DEFPKG.html" "" "defpkg") ("defrefinement" "defrefinement" "DEFREFINEMENT.html" "" "defrefinement") ("defstobj" "defstobj" "DEFSTOBJ.html" "" "defstobj") ("defstub" "defstub" "DEFSTUB.html" "" "defstub") ("deftheory" "deftheory" "DEFTHEORY.html" "" "deftheory") ("defthm" "defthm" "DEFTHM.html" "" "defthm") ("defthmd" "defthmd" "DEFTHMD.html" "" "defthmd") ("defttag" "defttag" "DEFTTAG.html" "" "defttag") ("defun-mode-caveat" "defun-mode-caveat" "DEFUN-MODE-CAVEAT.html" "" "defun-mode-caveat") ("defun-mode" "defun-mode" "DEFUN-MODE.html" "" "defun-mode") ("defun-sk-example" "defun-sk-example" "DEFUN-SK-EXAMPLE.html" "" "defun-sk-example") ("defun-sk" "defun-sk" "DEFUN-SK.html" "" "defun-sk") ("defun" "defun" "DEFUN.html" "" "defun") ("defund" "defund" "DEFUND.html" "" "defund") ("defuns" "defuns" "DEFUNS.html" "" "defuns") ("delete-include-book-dir" "delete-include-book-dir" "DELETE-INCLUDE-BOOK-DIR.html" "" "delete-include-book-dir") ("denominator" "denominator" "DENOMINATOR.html" "" "denominator") ("digit-char-p" "digit-char-p" "DIGIT-CHAR-P.html" "" "digit-char-p") ("digit-to-char" "digit-to-char" "DIGIT-TO-CHAR.html" "" "digit-to-char") ("dimensions" "dimensions" "DIMENSIONS.html" "" "dimensions") ("disable-forcing" "disable-forcing" "DISABLE-FORCING.html" "" "disable-forcing") ("disable-immediate-force-modep" "disable-immediate-force-modep" "DISABLE-IMMEDIATE-FORCE-MODEP.html" "" "disable-immediate-force-modep") ("disable" "disable" "DISABLE.html" "" "disable") ("disabledp" "disabledp" "DISABLEDP.html" "" "disabledp") ("dive-into-macros-table" "dive-into-macros-table" "DIVE-INTO-MACROS-TABLE.html" "" "dive-into-macros-table") ("do-not-induct" "do-not-induct" "DO-NOT-INDUCT.html" "" "do-not-induct") ("do-not" "do-not" "DO-NOT.html" "" "do-not") ("doc-string" "doc-string" "DOC-STRING.html" "" "doc-string") ("doc" "doc" "DOC.html" "" "doc") ("docs" "docs" "DOCS.html" "" "docs") ("documentation" "documentation" "DOCUMENTATION.html" "" "documentation") ("double-rewrite" "double-rewrite" "DOUBLE-REWRITE.html" "" "double-rewrite") ("e0-ordinalp" "e0-ordinalp" "E0-ORDINALP.html" "" "e0-ordinalp") ("eighth" "eighth" "EIGHTH.html" "" "eighth") ("elim" "elim" "ELIM.html" "" "elim") ("embedded-event-form" "embedded-event-form" "EMBEDDED-EVENT-FORM.html" "" "embedded-event-form") ("enable-forcing" "enable-forcing" "ENABLE-FORCING.html" "" "enable-forcing") ("enable-immediate-force-modep" "enable-immediate-force-modep" "ENABLE-IMMEDIATE-FORCE-MODEP.html" "" "enable-immediate-force-modep") ("enable" "enable" "ENABLE.html" "" "enable") ("encapsulate" "encapsulate" "ENCAPSULATE.html" "" "encapsulate") ("endp" "endp" "ENDP.html" "" "endp") ("enter-boot-strap-mode" "enter-boot-strap-mode" "ENTER-BOOT-STRAP-MODE.html" "" "enter-boot-strap-mode") ("eq" "eq" "EQ.html" "" "eq") ("eql" "eql" "EQL.html" "" "eql") ("eqlable-alistp" "eqlable-alistp" "EQLABLE-ALISTP.html" "" "eqlable-alistp") ("eqlable-listp" "eqlable-listp" "EQLABLE-LISTP.html" "" "eqlable-listp") ("eqlablep" "eqlablep" "EQLABLEP.html" "" "eqlablep") ("equal" "equal" "EQUAL.html" "" "equal") ("equivalence" "equivalence" "EQUIVALENCE.html" "" "equivalence") ("er-progn" "er-progn" "ER-PROGN.html" "" "er-progn") ("er" "er" "ER.html" "" "er") ("error1" "error1" "ERROR1.html" "" "error1") ("escape-to-common-lisp" "escape-to-common-lisp" "ESCAPE-TO-COMMON-LISP.html" "" "escape-to-common-lisp") ("evenp" "evenp" "EVENP.html" "" "evenp") ("events" "events" "EVENTS.html" "" "events") ("eviscerate-hide-terms" "eviscerate-hide-terms" "EVISCERATE-HIDE-TERMS.html" "" "eviscerate-hide-terms") ("executable-counterpart-theory" "executable-counterpart-theory" "EXECUTABLE-COUNTERPART-THEORY.html" "" "executable-counterpart-theory") ("executable-counterpart" "executable-counterpart" "EXECUTABLE-COUNTERPART.html" "" "executable-counterpart") ("exists" "exists" "EXISTS.html" "" "exists") ("exit-boot-strap-mode" "exit-boot-strap-mode" "EXIT-BOOT-STRAP-MODE.html" "" "exit-boot-strap-mode") ("exit" "exit" "EXIT.html" "" "exit") ("expand" "expand" "EXPAND.html" "" "expand") ("explode-nonnegative-integer" "explode-nonnegative-integer" "EXPLODE-NONNEGATIVE-INTEGER.html" "" "explode-nonnegative-integer") ("expt" "expt" "EXPT.html" "" "expt") ("extended-metafunctions" "extended-metafunctions" "EXTENDED-METAFUNCTIONS.html" "" "extended-metafunctions") ("failed-forcing" "failed-forcing" "FAILED-FORCING.html" "" "failed-forcing") ("failure" "failure" "FAILURE.html" "" "failure") ("fifth" "fifth" "FIFTH.html" "" "fifth") ("file-reading-example" "file-reading-example" "FILE-READING-EXAMPLE.html" "" "file-reading-example") ("find-rules-of-rune" "find-rules-of-rune" "FIND-RULES-OF-RUNE.html" "" "find-rules-of-rune") ("first" "first" "FIRST.html" "" "first") ("fix-true-list" "fix-true-list" "FIX-TRUE-LIST.html" "" "fix-true-list") ("fix" "fix" "FIX.html" "" "fix") ("floor" "floor" "FLOOR.html" "" "floor") ("flush-compress" "flush-compress" "FLUSH-COMPRESS.html" "" "flush-compress") ("fms" "fms" "FMS.html" "" "fms") ("fmt-to-comment-window" "fmt-to-comment-window" "FMT-TO-COMMENT-WINDOW.html" "" "fmt-to-comment-window") ("fmt" "fmt" "FMT.html" "" "fmt") ("fmt1" "fmt1" "FMT1.html" "" "fmt1") ("forall" "forall" "FORALL.html" "" "forall") ("force" "force" "FORCE.html" "" "force") ("forcing-round" "forcing-round" "FORCING-ROUND.html" "" "forcing-round") ("forward-chaining" "forward-chaining" "FORWARD-CHAINING.html" "" "forward-chaining") ("fourth" "fourth" "FOURTH.html" "" "fourth") ("free-variables-examples-forward-chaining" "free-variables-examples-forward-chaining" "FREE-VARIABLES-EXAMPLES-FORWARD-CHAINING.html" "" "free-variables-examples-forward-chaining") ("free-variables-examples-rewrite" "free-variables-examples-rewrite" "FREE-VARIABLES-EXAMPLES-REWRITE.html" "" "free-variables-examples-rewrite") ("free-variables-examples" "free-variables-examples" "FREE-VARIABLES-EXAMPLES.html" "" "free-variables-examples") ("free-variables" "free-variables" "FREE-VARIABLES.html" "" "free-variables") ("full-book-name" "full-book-name" "FULL-BOOK-NAME.html" "" "full-book-name") ("function-theory" "function-theory" "FUNCTION-THEORY.html" "" "function-theory") ("functional-instantiation-example" "functional-instantiation-example" "FUNCTIONAL-INSTANTIATION-EXAMPLE.html" "" "functional-instantiation-example") ("gc$" "gc$" "GC$.html" "" "gc$") ("gcl" "gcl" "GCL.html" "" "gcl") ("generalize" "generalize" "GENERALIZE.html" "" "generalize") ("generalized-booleans" "generalized-booleans" "GENERALIZED-BOOLEANS.html" "" "generalized-booleans") ("getenv$" "getenv$" "GETENV$.html" "" "getenv$") ("goal-spec" "goal-spec" "GOAL-SPEC.html" "" "goal-spec") ("good-bye" "good-bye" "GOOD-BYE.html" "" "good-bye") ("ground-zero" "ground-zero" "GROUND-ZERO.html" "" "ground-zero") ("guard-evaluation-examples-log" "guard-evaluation-examples-log" "GUARD-EVALUATION-EXAMPLES-LOG.html" "" "guard-evaluation-examples-log") ("guard-evaluation-examples-script" "guard-evaluation-examples-script" "GUARD-EVALUATION-EXAMPLES-SCRIPT.html" "" "guard-evaluation-examples-script") ("guard-evaluation-table" "guard-evaluation-table" "GUARD-EVALUATION-TABLE.html" "" "guard-evaluation-table") ("guard-example" "guard-example" "GUARD-EXAMPLE.html" "" "guard-example") ("guard-hints" "guard-hints" "GUARD-HINTS.html" "" "guard-hints") ("guard-introduction" "guard-introduction" "GUARD-INTRODUCTION.html" "" "guard-introduction") ("guard-miscellany" "guard-miscellany" "GUARD-MISCELLANY.html" "" "guard-miscellany") ("guard-quick-reference" "guard-quick-reference" "GUARD-QUICK-REFERENCE.html" "" "guard-quick-reference") ("guard" "guard" "GUARD.html" "" "guard") ("guards-and-evaluation" "guards-and-evaluation" "GUARDS-AND-EVALUATION.html" "" "guards-and-evaluation") ("guards-for-specification" "guards-for-specification" "GUARDS-FOR-SPECIFICATION.html" "" "guards-for-specification") ("hands-off" "hands-off" "HANDS-OFF.html" "" "hands-off") ("hard-error" "hard-error" "HARD-ERROR.html" "" "hard-error") ("header" "header" "HEADER.html" "" "header") ("help" "help" "HELP.html" "" "help") ("hidden-death-package" "hidden-death-package" "HIDDEN-DEATH-PACKAGE.html" "" "hidden-death-package") ("hidden-defpkg" "hidden-defpkg" "HIDDEN-DEFPKG.html" "" "hidden-defpkg") ("hide" "hide" "HIDE.html" "" "hide") ("hints" "hints" "HINTS.html" "" "hints") ("history" "history" "HISTORY.html" "" "history") ("i-am-here" "i-am-here" "I-AM-HERE.html" "" "i-am-here") ("i-close" "i-close" "I-CLOSE.html" "" "i-close") ("i-large" "i-large" "I-LARGE.html" "" "i-large") ("i-limited" "i-limited" "I-LIMITED.html" "" "i-limited") ("i-small" "i-small" "I-SMALL.html" "" "i-small") ("identity" "identity" "IDENTITY.html" "" "identity") ("if" "if" "IF.html" "" "if") ("iff" "iff" "IFF.html" "" "iff") ("ifix" "ifix" "IFIX.html" "" "ifix") ("illegal" "illegal" "ILLEGAL.html" "" "illegal") ("imagpart" "imagpart" "IMAGPART.html" "" "imagpart") ("immediate-force-modep" "immediate-force-modep" "IMMEDIATE-FORCE-MODEP.html" "" "immediate-force-modep") ("implies" "implies" "IMPLIES.html" "" "implies") ("improper-consp" "improper-consp" "IMPROPER-CONSP.html" "" "improper-consp") ("in-arithmetic-theory" "in-arithmetic-theory" "IN-ARITHMETIC-THEORY.html" "" "in-arithmetic-theory") ("in-package" "in-package" "IN-PACKAGE.html" "" "in-package") ("in-theory" "in-theory" "IN-THEORY.html" "" "in-theory") ("include-book" "include-book" "INCLUDE-BOOK.html" "" "include-book") ("incompatible" "incompatible" "INCOMPATIBLE.html" "" "incompatible") ("induct" "induct" "INDUCT.html" "" "induct") ("induction" "induction" "INDUCTION.html" "" "induction") ("instructions" "instructions" "INSTRUCTIONS.html" "" "instructions") ("int=" "int=" "INT=.html" "" "int=") ("integer-length" "integer-length" "INTEGER-LENGTH.html" "" "integer-length") ("integer-listp" "integer-listp" "INTEGER-LISTP.html" "" "integer-listp") ("integerp" "integerp" "INTEGERP.html" "" "integerp") ("intern$" "intern$" "INTERN$.html" "" "intern$") ("intern-in-package-of-symbol" "intern-in-package-of-symbol" "INTERN-IN-PACKAGE-OF-SYMBOL.html" "" "intern-in-package-of-symbol") ("intern" "intern" "INTERN.html" "" "intern") ("intersection-theories" "intersection-theories" "INTERSECTION-THEORIES.html" "" "intersection-theories") ("intersectp-eq" "intersectp-eq" "INTERSECTP-EQ.html" "" "intersectp-eq") ("intersectp-equal" "intersectp-equal" "INTERSECTP-EQUAL.html" "" "intersectp-equal") ("introduction" "introduction" "INTRODUCTION.html" "" "introduction") ("invisible-fns-table" "invisible-fns-table" "INVISIBLE-FNS-TABLE.html" "" "invisible-fns-table") ("io" "io" "IO.html" "" "io") ("irrelevant-formals" "irrelevant-formals" "IRRELEVANT-FORMALS.html" "" "irrelevant-formals") ("keep" "keep" "KEEP.html" "" "keep") ("keyword-commands" "keyword-commands" "KEYWORD-COMMANDS.html" "" "keyword-commands") ("keyword-value-listp" "keyword-value-listp" "KEYWORD-VALUE-LISTP.html" "" "keyword-value-listp") ("keywordp" "keywordp" "KEYWORDP.html" "" "keywordp") ("lambda" "lambda" "LAMBDA.html" "" "lambda") ("last" "last" "LAST.html" "" "last") ("ld-error-action" "ld-error-action" "LD-ERROR-ACTION.html" "" "ld-error-action") ("ld-error-triples" "ld-error-triples" "LD-ERROR-TRIPLES.html" "" "ld-error-triples") ("ld-evisc-tuple" "ld-evisc-tuple" "LD-EVISC-TUPLE.html" "" "ld-evisc-tuple") ("ld-keyword-aliases" "ld-keyword-aliases" "LD-KEYWORD-ALIASES.html" "" "ld-keyword-aliases") ("ld-post-eval-print" "ld-post-eval-print" "LD-POST-EVAL-PRINT.html" "" "ld-post-eval-print") ("ld-pre-eval-filter" "ld-pre-eval-filter" "LD-PRE-EVAL-FILTER.html" "" "ld-pre-eval-filter") ("ld-pre-eval-print" "ld-pre-eval-print" "LD-PRE-EVAL-PRINT.html" "" "ld-pre-eval-print") ("ld-prompt" "ld-prompt" "LD-PROMPT.html" "" "ld-prompt") ("ld-query-control-alist" "ld-query-control-alist" "LD-QUERY-CONTROL-ALIST.html" "" "ld-query-control-alist") ("ld-redefinition-action" "ld-redefinition-action" "LD-REDEFINITION-ACTION.html" "" "ld-redefinition-action") ("ld-skip-proofsp" "ld-skip-proofsp" "LD-SKIP-PROOFSP.html" "" "ld-skip-proofsp") ("ld-verbose" "ld-verbose" "LD-VERBOSE.html" "" "ld-verbose") ("ld" "ld" "LD.html" "" "ld") ("lemma-instance" "lemma-instance" "LEMMA-INSTANCE.html" "" "lemma-instance") ("len" "len" "LEN.html" "" "len") ("length" "length" "LENGTH.html" "" "length") ("let" "let" "LET.html" "" "let") ("lexorder" "lexorder" "LEXORDER.html" "" "lexorder") ("linear-arithmetic" "linear-arithmetic" "LINEAR-ARITHMETIC.html" "" "linear-arithmetic") ("linear" "linear" "LINEAR.html" "" "linear") ("list" "list" "LIST.html" "" "list") ("listp" "listp" "LISTP.html" "" "listp") ("local-incompatibility" "local-incompatibility" "LOCAL-INCOMPATIBILITY.html" "" "local-incompatibility") ("local" "local" "LOCAL.html" "" "local") ("logand" "logand" "LOGAND.html" "" "logand") ("logandc1" "logandc1" "LOGANDC1.html" "" "logandc1") ("logandc2" "logandc2" "LOGANDC2.html" "" "logandc2") ("logbitp" "logbitp" "LOGBITP.html" "" "logbitp") ("logcount" "logcount" "LOGCOUNT.html" "" "logcount") ("logeqv" "logeqv" "LOGEQV.html" "" "logeqv") ("logic" "logic" "LOGIC.html" "" "logic") ("logical-name" "logical-name" "LOGICAL-NAME.html" "" "logical-name") ("logior" "logior" "LOGIOR.html" "" "logior") ("lognand" "lognand" "LOGNAND.html" "" "lognand") ("lognor" "lognor" "LOGNOR.html" "" "lognor") ("lognot" "lognot" "LOGNOT.html" "" "lognot") ("logorc1" "logorc1" "LOGORC1.html" "" "logorc1") ("logorc2" "logorc2" "LOGORC2.html" "" "logorc2") ("logtest" "logtest" "LOGTEST.html" "" "logtest") ("logxor" "logxor" "LOGXOR.html" "" "logxor") ("loop-stopper" "loop-stopper" "LOOP-STOPPER.html" "" "loop-stopper") ("lower-case-p" "lower-case-p" "LOWER-CASE-P.html" "" "lower-case-p") ("lp" "lp" "LP.html" "" "lp") ("macro-aliases-table" "macro-aliases-table" "MACRO-ALIASES-TABLE.html" "" "macro-aliases-table") ("macro-args" "macro-args" "MACRO-ARGS.html" "" "macro-args") ("macro-command" "macro-command" "MACRO-COMMAND.html" "" "macro-command") ("make-character-list" "make-character-list" "MAKE-CHARACTER-LIST.html" "" "make-character-list") ("make-event-details" "make-event-details" "MAKE-EVENT-DETAILS.html" "" "make-event-details") ("make-event" "make-event" "MAKE-EVENT.html" "" "make-event") ("make-list" "make-list" "MAKE-LIST.html" "" "make-list") ("make-ord" "make-ord" "MAKE-ORD.html" "" "make-ord") ("makefiles" "makefiles" "MAKEFILES.html" "" "makefiles") ("markup" "markup" "MARKUP.html" "" "markup") ("max" "max" "MAX.html" "" "max") ("maximum-length" "maximum-length" "MAXIMUM-LENGTH.html" "" "maximum-length") ("mbe" "mbe" "MBE.html" "" "mbe") ("mbt" "mbt" "MBT.html" "" "mbt") ("measure" "measure" "MEASURE.html" "" "measure") ("member-eq" "member-eq" "MEMBER-EQ.html" "" "member-eq") ("member-equal" "member-equal" "MEMBER-EQUAL.html" "" "member-equal") ("member" "member" "MEMBER.html" "" "member") ("meta" "meta" "META.html" "" "meta") ("min" "min" "MIN.html" "" "min") ("minimal-theory" "minimal-theory" "MINIMAL-THEORY.html" "" "minimal-theory") ("minusp" "minusp" "MINUSP.html" "" "minusp") ("miscellaneous" "miscellaneous" "MISCELLANEOUS.html" "" "miscellaneous") ("mod-expt" "mod-expt" "MOD-EXPT.html" "" "mod-expt") ("mod" "mod" "MOD.html" "" "mod") ("mode" "mode" "MODE.html" "" "mode") ("monitor" "monitor" "MONITOR.html" "" "monitor") ("monitored-runes" "monitored-runes" "MONITORED-RUNES.html" "" "monitored-runes") ("more-doc" "more-doc" "MORE-DOC.html" "" "more-doc") ("more" "more" "MORE.html" "" "more") ("must-be-equal" "must-be-equal" "MUST-BE-EQUAL.html" "" "must-be-equal") ("mutual-recursion-proof-example" "mutual-recursion-proof-example" "MUTUAL-RECURSION-PROOF-EXAMPLE.html" "" "mutual-recursion-proof-example") ("mutual-recursion" "mutual-recursion" "MUTUAL-RECURSION.html" "" "mutual-recursion") ("mv-let" "mv-let" "MV-LET.html" "" "mv-let") ("mv-nth" "mv-nth" "MV-NTH.html" "" "mv-nth") ("mv" "mv" "MV.html" "" "mv") ("name" "name" "NAME.html" "" "name") ("natp" "natp" "NATP.html" "" "natp") ("nfix" "nfix" "NFIX.html" "" "nfix") ("ninth" "ninth" "NINTH.html" "" "ninth") ("no-duplicatesp-equal" "no-duplicatesp-equal" "NO-DUPLICATESP-EQUAL.html" "" "no-duplicatesp-equal") ("no-duplicatesp" "no-duplicatesp" "NO-DUPLICATESP.html" "" "no-duplicatesp") ("non-executable" "non-executable" "NON-EXECUTABLE.html" "" "non-executable") ("non-linear-arithmetic" "non-linear-arithmetic" "NON-LINEAR-ARITHMETIC.html" "" "non-linear-arithmetic") ("nonlinearp" "nonlinearp" "NONLINEARP.html" "" "nonlinearp") ("nonnegative-integer-quotient" "nonnegative-integer-quotient" "NONNEGATIVE-INTEGER-QUOTIENT.html" "" "nonnegative-integer-quotient") ("normalize" "normalize" "NORMALIZE.html" "" "normalize") ("not" "not" "NOT.html" "" "not") ("note-2-0" "note-2-0" "NOTE-2-0.html" "" "note-2-0") ("note-2-1" "note-2-1" "NOTE-2-1.html" "" "note-2-1") ("note-2-2" "note-2-2" "NOTE-2-2.html" "" "note-2-2") ("note-2-3" "note-2-3" "NOTE-2-3.html" "" "note-2-3") ("note-2-4" "note-2-4" "NOTE-2-4.html" "" "note-2-4") ("note-2-5" "note-2-5" "NOTE-2-5.html" "" "note-2-5") ("note-2-6-guards" "note-2-6-guards" "NOTE-2-6-GUARDS.html" "" "note-2-6-guards") ("note-2-6-new-functionality" "note-2-6-new-functionality" "NOTE-2-6-NEW-FUNCTIONALITY.html" "" "note-2-6-new-functionality") ("note-2-6-other" "note-2-6-other" "NOTE-2-6-OTHER.html" "" "note-2-6-other") ("note-2-6-proof-checker" "note-2-6-proof-checker" "NOTE-2-6-PROOF-CHECKER.html" "" "note-2-6-proof-checker") ("note-2-6-proofs" "note-2-6-proofs" "NOTE-2-6-PROOFS.html" "" "note-2-6-proofs") ("note-2-6-rules" "note-2-6-rules" "NOTE-2-6-RULES.html" "" "note-2-6-rules") ("note-2-6-system" "note-2-6-system" "NOTE-2-6-SYSTEM.html" "" "note-2-6-system") ("note-2-6" "note-2-6" "NOTE-2-6.html" "" "note-2-6") ("note-2-7-bug-fixes" "note-2-7-bug-fixes" "NOTE-2-7-BUG-FIXES.html" "" "note-2-7-bug-fixes") ("note-2-7-guards" "note-2-7-guards" "NOTE-2-7-GUARDS.html" "" "note-2-7-guards") ("note-2-7-new-functionality" "note-2-7-new-functionality" "NOTE-2-7-NEW-FUNCTIONALITY.html" "" "note-2-7-new-functionality") ("note-2-7-other" "note-2-7-other" "NOTE-2-7-OTHER.html" "" "note-2-7-other") ("note-2-7-proof-checker" "note-2-7-proof-checker" "NOTE-2-7-PROOF-CHECKER.html" "" "note-2-7-proof-checker") ("note-2-7-proofs" "note-2-7-proofs" "NOTE-2-7-PROOFS.html" "" "note-2-7-proofs") ("note-2-7-rules" "note-2-7-rules" "NOTE-2-7-RULES.html" "" "note-2-7-rules") ("note-2-7-system" "note-2-7-system" "NOTE-2-7-SYSTEM.html" "" "note-2-7-system") ("note-2-7" "note-2-7" "NOTE-2-7.html" "" "note-2-7") ("note-2-8-bug-fixes" "note-2-8-bug-fixes" "NOTE-2-8-BUG-FIXES.html" "" "note-2-8-bug-fixes") ("note-2-8-guards" "note-2-8-guards" "NOTE-2-8-GUARDS.html" "" "note-2-8-guards") ("note-2-8-new-functionality" "note-2-8-new-functionality" "NOTE-2-8-NEW-FUNCTIONALITY.html" "" "note-2-8-new-functionality") ("note-2-8-ordinals" "note-2-8-ordinals" "NOTE-2-8-ORDINALS.html" "" "note-2-8-ordinals") ("note-2-8-other" "note-2-8-other" "NOTE-2-8-OTHER.html" "" "note-2-8-other") ("note-2-8-proof-checker" "note-2-8-proof-checker" "NOTE-2-8-PROOF-CHECKER.html" "" "note-2-8-proof-checker") ("note-2-8-proofs" "note-2-8-proofs" "NOTE-2-8-PROOFS.html" "" "note-2-8-proofs") ("note-2-8-rules" "note-2-8-rules" "NOTE-2-8-RULES.html" "" "note-2-8-rules") ("note-2-8-system" "note-2-8-system" "NOTE-2-8-SYSTEM.html" "" "note-2-8-system") ("note-2-8" "note-2-8" "NOTE-2-8.html" "" "note-2-8") ("note-2-9-1" "note-2-9-1" "NOTE-2-9-1.html" "" "note-2-9-1") ("note-2-9-2" "note-2-9-2" "NOTE-2-9-2.html" "" "note-2-9-2") ("note-2-9-3-ppr-change" "note-2-9-3-ppr-change" "NOTE-2-9-3-PPR-CHANGE.html" "" "note-2-9-3-ppr-change") ("note-2-9-3" "note-2-9-3" "NOTE-2-9-3.html" "" "note-2-9-3") ("note-2-9-4" "note-2-9-4" "NOTE-2-9-4.html" "" "note-2-9-4") ("note-2-9-5" "note-2-9-5" "NOTE-2-9-5.html" "" "note-2-9-5") ("note-2-9" "note-2-9" "NOTE-2-9.html" "" "note-2-9") ("note-3-0-1" "note-3-0-1" "NOTE-3-0-1.html" "" "note-3-0-1") ("note-3-0-2" "note-3-0-2" "NOTE-3-0-2.html" "" "note-3-0-2") ("note-3-0" "note-3-0" "NOTE-3-0.html" "" "note-3-0") ("note-3-1" "note-3-1" "NOTE-3-1.html" "" "note-3-1") ("note1" "note1" "NOTE1.html" "" "note1") ("note2" "note2" "NOTE2.html" "" "note2") ("note3" "note3" "NOTE3.html" "" "note3") ("note4" "note4" "NOTE4.html" "" "note4") ("note5" "note5" "NOTE5.html" "" "note5") ("note6" "note6" "NOTE6.html" "" "note6") ("note7" "note7" "NOTE7.html" "" "note7") ("note8-update" "note8-update" "NOTE8-UPDATE.html" "" "note8-update") ("note8" "note8" "NOTE8.html" "" "note8") ("note9" "note9" "NOTE9.html" "" "note9") ("nqthm-to-acl2" "nqthm-to-acl2" "NQTHM-TO-ACL2.html" "" "nqthm-to-acl2") ("nth-aliases-table" "nth-aliases-table" "NTH-ALIASES-TABLE.html" "" "nth-aliases-table") ("nth" "nth" "NTH.html" "" "nth") ("nthcdr" "nthcdr" "NTHCDR.html" "" "nthcdr") ("nu-rewriter" "nu-rewriter" "NU-REWRITER.html" "" "nu-rewriter") ("null" "null" "NULL.html" "" "null") ("numerator" "numerator" "NUMERATOR.html" "" "numerator") ("o-finp" "o-finp" "O-FINP.html" "" "o-finp") ("o-first-coeff" "o-first-coeff" "O-FIRST-COEFF.html" "" "o-first-coeff") ("o-first-expt" "o-first-expt" "O-FIRST-EXPT.html" "" "o-first-expt") ("o-infp" "o-infp" "O-INFP.html" "" "o-infp") ("o-p" "o-p" "O-P.html" "" "o-p") ("o-rst" "o-rst" "O-RST.html" "" "o-rst") ("obdd" "obdd" "OBDD.html" "" "obdd") ("oddp" "oddp" "ODDP.html" "" "oddp") ("ok-if" "ok-if" "OK-IF.html" "" "ok-if") ("oops" "oops" "OOPS.html" "" "oops") ("open-input-channel-p" "open-input-channel-p" "OPEN-INPUT-CHANNEL-P.html" "" "open-input-channel-p") ("open-input-channel" "open-input-channel" "OPEN-INPUT-CHANNEL.html" "" "open-input-channel") ("open-output-channel-p" "open-output-channel-p" "OPEN-OUTPUT-CHANNEL-P.html" "" "open-output-channel-p") ("open-output-channel" "open-output-channel" "OPEN-OUTPUT-CHANNEL.html" "" "open-output-channel") ("open-trace-file" "open-trace-file" "OPEN-TRACE-FILE.html" "" "open-trace-file") ("or" "or" "OR.html" "" "or") ("ordinals" "ordinals" "ORDINALS.html" "" "ordinals") ("otf-flg" "otf-flg" "OTF-FLG.html" "" "otf-flg") ("other" "other" "OTHER.html" "" "other") ("package-reincarnation-import-restrictions" "package-reincarnation-import-restrictions" "PACKAGE-REINCARNATION-IMPORT-RESTRICTIONS.html" "" "package-reincarnation-import-restrictions") ("pairlis$" "pairlis$" "PAIRLIS$.html" "" "pairlis$") ("pairlis" "pairlis" "PAIRLIS.html" "" "pairlis") ("pathname" "pathname" "PATHNAME.html" "" "pathname") ("pbt" "pbt" "PBT.html" "" "pbt") ("pc" "pc" "PC.html" "" "pc") ("pcb" "pcb" "PCB.html" "" "pcb") ("pcs" "pcs" "PCS.html" "" "pcs") ("pe" "pe" "PE.html" "" "pe") ("peek-char$" "peek-char$" "PEEK-CHAR$.html" "" "peek-char$") ("pf" "pf" "PF.html" "" "pf") ("pkg-witness" "pkg-witness" "PKG-WITNESS.html" "" "pkg-witness") ("pl" "pl" "PL.html" "" "pl") ("plusp" "plusp" "PLUSP.html" "" "plusp") ("portcullis" "portcullis" "PORTCULLIS.html" "" "portcullis") ("position-eq" "position-eq" "POSITION-EQ.html" "" "position-eq") ("position-equal" "position-equal" "POSITION-EQUAL.html" "" "position-equal") ("position" "position" "POSITION.html" "" "position") ("posp" "posp" "POSP.html" "" "posp") ("pprogn" "pprogn" "PPROGN.html" "" "pprogn") ("pr" "pr" "PR.html" "" "pr") ("princ$" "princ$" "PRINC$.html" "" "princ$") ("print-doc-start-column" "print-doc-start-column" "PRINT-DOC-START-COLUMN.html" "" "print-doc-start-column") ("print-object$" "print-object$" "PRINT-OBJECT$.html" "" "print-object$") ("prog2$" "prog2$" "PROG2$.html" "" "prog2$") ("progn" "progn" "PROGN.html" "" "progn") ("program" "program" "PROGRAM.html" "" "program") ("programming" "programming" "PROGRAMMING.html" "" "programming") ("prompt" "prompt" "PROMPT.html" "" "prompt") ("proof-checker-commands" "proof-checker-commands" "PROOF-CHECKER-COMMANDS.html" "" "proof-checker-commands") ("proof-checker" "proof-checker" "PROOF-CHECKER.html" "" "proof-checker") ("proof-of-well-foundedness" "proof-of-well-foundedness" "PROOF-OF-WELL-FOUNDEDNESS.html" "" "proof-of-well-foundedness") ("proof-tree-bindings" "proof-tree-bindings" "PROOF-TREE-BINDINGS.html" "" "proof-tree-bindings") ("proof-tree-details" "proof-tree-details" "PROOF-TREE-DETAILS.html" "" "proof-tree-details") ("proof-tree-emacs" "proof-tree-emacs" "PROOF-TREE-EMACS.html" "" "proof-tree-emacs") ("proof-tree-examples" "proof-tree-examples" "PROOF-TREE-EXAMPLES.html" "" "proof-tree-examples") ("proof-tree" "proof-tree" "PROOF-TREE.html" "" "proof-tree") ("proofs-co" "proofs-co" "PROOFS-CO.html" "" "proofs-co") ("proper-consp" "proper-consp" "PROPER-CONSP.html" "" "proper-consp") ("props" "props" "PROPS.html" "" "props") ("pseudo-termp" "pseudo-termp" "PSEUDO-TERMP.html" "" "pseudo-termp") ("pso" "pso" "PSO.html" "" "pso") ("pstack" "pstack" "PSTACK.html" "" "pstack") ("puff" "puff" "PUFF.html" "" "puff") ("push-untouchable" "push-untouchable" "PUSH-UNTOUCHABLE.html" "" "push-untouchable") ("put-assoc-eq" "put-assoc-eq" "PUT-ASSOC-EQ.html" "" "put-assoc-eq") ("put-assoc-eql" "put-assoc-eql" "PUT-ASSOC-EQL.html" "" "put-assoc-eql") ("put-assoc-equal" "put-assoc-equal" "PUT-ASSOC-EQUAL.html" "" "put-assoc-equal") ("q" "q" "Q.html" "" "q") ("quantifiers-using-defun-sk-extended" "quantifiers-using-defun-sk-extended" "QUANTIFIERS-USING-DEFUN-SK-EXTENDED.html" "" "quantifiers-using-defun-sk-extended") ("quantifiers-using-defun-sk" "quantifiers-using-defun-sk" "QUANTIFIERS-USING-DEFUN-SK.html" "" "quantifiers-using-defun-sk") ("quantifiers-using-recursion" "quantifiers-using-recursion" "QUANTIFIERS-USING-RECURSION.html" "" "quantifiers-using-recursion") ("quantifiers" "quantifiers" "QUANTIFIERS.html" "" "quantifiers") ("quit" "quit" "QUIT.html" "" "quit") ("rassoc-eq" "rassoc-eq" "RASSOC-EQ.html" "" "rassoc-eq") ("rassoc-equal" "rassoc-equal" "RASSOC-EQUAL.html" "" "rassoc-equal") ("rassoc" "rassoc" "RASSOC.html" "" "rassoc") ("rational-listp" "rational-listp" "RATIONAL-LISTP.html" "" "rational-listp") ("rationalp" "rationalp" "RATIONALP.html" "" "rationalp") ("read-byte$" "read-byte$" "READ-BYTE$.html" "" "read-byte$") ("read-char$" "read-char$" "READ-CHAR$.html" "" "read-char$") ("read-object" "read-object" "READ-OBJECT.html" "" "read-object") ("real-listp" "real-listp" "REAL-LISTP.html" "" "real-listp") ("real" "real" "REAL.html" "" "real") ("realfix" "realfix" "REALFIX.html" "" "realfix") ("realpart" "realpart" "REALPART.html" "" "realpart") ("rebuild" "rebuild" "REBUILD.html" "" "rebuild") ("redef" "redef" "REDEF.html" "" "redef") ("redefined-names" "redefined-names" "REDEFINED-NAMES.html" "" "redefined-names") ("redefining-programs" "redefining-programs" "REDEFINING-PROGRAMS.html" "" "redefining-programs") ("redo-flat" "redo-flat" "REDO-FLAT.html" "" "redo-flat") ("redundant-events" "redundant-events" "REDUNDANT-EVENTS.html" "" "redundant-events") ("refinement" "refinement" "REFINEMENT.html" "" "refinement") ("release-notes" "release-notes" "RELEASE-NOTES.html" "" "release-notes") ("rem" "rem" "REM.html" "" "rem") ("remove-binop" "remove-binop" "REMOVE-BINOP.html" "" "remove-binop") ("remove-default-hints" "remove-default-hints" "REMOVE-DEFAULT-HINTS.html" "" "remove-default-hints") ("remove-dive-into-macro" "remove-dive-into-macro" "REMOVE-DIVE-INTO-MACRO.html" "" "remove-dive-into-macro") ("remove-duplicates-equal" "remove-duplicates-equal" "REMOVE-DUPLICATES-EQUAL.html" "" "remove-duplicates-equal") ("remove-duplicates" "remove-duplicates" "REMOVE-DUPLICATES.html" "" "remove-duplicates") ("remove-eq" "remove-eq" "REMOVE-EQ.html" "" "remove-eq") ("remove-equal" "remove-equal" "REMOVE-EQUAL.html" "" "remove-equal") ("remove-invisible-fns" "remove-invisible-fns" "REMOVE-INVISIBLE-FNS.html" "" "remove-invisible-fns") ("remove-macro-alias" "remove-macro-alias" "REMOVE-MACRO-ALIAS.html" "" "remove-macro-alias") ("remove-nth-alias" "remove-nth-alias" "REMOVE-NTH-ALIAS.html" "" "remove-nth-alias") ("remove-raw-arity" "remove-raw-arity" "REMOVE-RAW-ARITY.html" "" "remove-raw-arity") ("remove-untouchable" "remove-untouchable" "REMOVE-UNTOUCHABLE.html" "" "remove-untouchable") ("remove" "remove" "REMOVE.html" "" "remove") ("remove1-eq" "remove1-eq" "REMOVE1-EQ.html" "" "remove1-eq") ("remove1-equal" "remove1-equal" "REMOVE1-EQUAL.html" "" "remove1-equal") ("remove1" "remove1" "REMOVE1.html" "" "remove1") ("reset-kill-ring" "reset-kill-ring" "RESET-KILL-RING.html" "" "reset-kill-ring") ("reset-ld-specials" "reset-ld-specials" "RESET-LD-SPECIALS.html" "" "reset-ld-specials") ("reset-prehistory" "reset-prehistory" "RESET-PREHISTORY.html" "" "reset-prehistory") ("resize-list" "resize-list" "RESIZE-LIST.html" "" "resize-list") ("rest" "rest" "REST.html" "" "rest") ("restrict" "restrict" "RESTRICT.html" "" "restrict") ("retrieve" "retrieve" "RETRIEVE.html" "" "retrieve") ("revappend" "revappend" "REVAPPEND.html" "" "revappend") ("reverse" "reverse" "REVERSE.html" "" "reverse") ("rewrite-stack-limit" "rewrite-stack-limit" "REWRITE-STACK-LIMIT.html" "" "rewrite-stack-limit") ("rewrite" "rewrite" "REWRITE.html" "" "rewrite") ("rfix" "rfix" "RFIX.html" "" "rfix") ("round" "round" "ROUND.html" "" "round") ("rule-classes" "rule-classes" "RULE-CLASSES.html" "" "rule-classes") ("rule-names" "rule-names" "RULE-NAMES.html" "" "rule-names") ("rune" "rune" "RUNE.html" "" "rune") ("save-exec" "save-exec" "SAVE-EXEC.html" "" "save-exec") ("saving-and-restoring" "saving-and-restoring" "SAVING-AND-RESTORING.html" "" "saving-and-restoring") ("second" "second" "SECOND.html" "" "second") ("set-acl2-print-base" "set-acl2-print-base" "SET-ACL2-PRINT-BASE.html" "" "set-acl2-print-base") ("set-acl2-print-case" "set-acl2-print-case" "SET-ACL2-PRINT-CASE.html" "" "set-acl2-print-case") ("set-backchain-limit" "set-backchain-limit" "SET-BACKCHAIN-LIMIT.html" "" "set-backchain-limit") ("set-body" "set-body" "SET-BODY.html" "" "set-body") ("set-bogus-mutual-recursion-ok" "set-bogus-mutual-recursion-ok" "SET-BOGUS-MUTUAL-RECURSION-OK.html" "" "set-bogus-mutual-recursion-ok") ("set-brr-term-evisc-tuple" "set-brr-term-evisc-tuple" "SET-BRR-TERM-EVISC-TUPLE.html" "" "set-brr-term-evisc-tuple") ("set-case-split-limitations" "set-case-split-limitations" "SET-CASE-SPLIT-LIMITATIONS.html" "" "set-case-split-limitations") ("set-cbd" "set-cbd" "SET-CBD.html" "" "set-cbd") ("set-compile-fns" "set-compile-fns" "SET-COMPILE-FNS.html" "" "set-compile-fns") ("set-default-backchain-limit" "set-default-backchain-limit" "SET-DEFAULT-BACKCHAIN-LIMIT.html" "" "set-default-backchain-limit") ("set-default-hints" "set-default-hints" "SET-DEFAULT-HINTS.html" "" "set-default-hints") ("set-difference-eq" "set-difference-eq" "SET-DIFFERENCE-EQ.html" "" "set-difference-eq") ("set-difference-equal" "set-difference-equal" "SET-DIFFERENCE-EQUAL.html" "" "set-difference-equal") ("set-difference-theories" "set-difference-theories" "SET-DIFFERENCE-THEORIES.html" "" "set-difference-theories") ("set-enforce-redundancy" "set-enforce-redundancy" "SET-ENFORCE-REDUNDANCY.html" "" "set-enforce-redundancy") ("set-guard-checking" "set-guard-checking" "SET-GUARD-CHECKING.html" "" "set-guard-checking") ("set-ignore-ok" "set-ignore-ok" "SET-IGNORE-OK.html" "" "set-ignore-ok") ("set-inhibit-output-lst" "set-inhibit-output-lst" "SET-INHIBIT-OUTPUT-LST.html" "" "set-inhibit-output-lst") ("set-inhibit-warnings" "set-inhibit-warnings" "SET-INHIBIT-WARNINGS.html" "" "set-inhibit-warnings") ("set-invisible-fns-table" "set-invisible-fns-table" "SET-INVISIBLE-FNS-TABLE.html" "" "set-invisible-fns-table") ("set-irrelevant-formals-ok" "set-irrelevant-formals-ok" "SET-IRRELEVANT-FORMALS-OK.html" "" "set-irrelevant-formals-ok") ("set-ld-redefinition-action" "set-ld-redefinition-action" "SET-LD-REDEFINITION-ACTION.html" "" "set-ld-redefinition-action") ("set-ld-skip-proofsp" "set-ld-skip-proofsp" "SET-LD-SKIP-PROOFSP.html" "" "set-ld-skip-proofsp") ("set-match-free-default" "set-match-free-default" "SET-MATCH-FREE-DEFAULT.html" "" "set-match-free-default") ("set-match-free-error" "set-match-free-error" "SET-MATCH-FREE-ERROR.html" "" "set-match-free-error") ("set-measure-function" "set-measure-function" "SET-MEASURE-FUNCTION.html" "" "set-measure-function") ("set-non-linearp" "set-non-linearp" "SET-NON-LINEARP.html" "" "set-non-linearp") ("set-nu-rewriter-mode" "set-nu-rewriter-mode" "SET-NU-REWRITER-MODE.html" "" "set-nu-rewriter-mode") ("set-print-clause-ids" "set-print-clause-ids" "SET-PRINT-CLAUSE-IDS.html" "" "set-print-clause-ids") ("set-raw-mode" "set-raw-mode" "SET-RAW-MODE.html" "" "set-raw-mode") ("set-rewrite-stack-limit" "set-rewrite-stack-limit" "SET-REWRITE-STACK-LIMIT.html" "" "set-rewrite-stack-limit") ("set-saved-output" "set-saved-output" "SET-SAVED-OUTPUT.html" "" "set-saved-output") ("set-state-ok" "set-state-ok" "SET-STATE-OK.html" "" "set-state-ok") ("set-tainted-okp" "set-tainted-okp" "SET-TAINTED-OKP.html" "" "set-tainted-okp") ("set-verify-guards-eagerness" "set-verify-guards-eagerness" "SET-VERIFY-GUARDS-EAGERNESS.html" "" "set-verify-guards-eagerness") ("set-well-founded-relation" "set-well-founded-relation" "SET-WELL-FOUNDED-RELATION.html" "" "set-well-founded-relation") ("setenv$" "setenv$" "SETENV$.html" "" "setenv$") ("seventh" "seventh" "SEVENTH.html" "" "seventh") ("show-bdd" "show-bdd" "SHOW-BDD.html" "" "show-bdd") ("show-bodies" "show-bodies" "SHOW-BODIES.html" "" "show-bodies") ("signature" "signature" "SIGNATURE.html" "" "signature") ("signum" "signum" "SIGNUM.html" "" "signum") ("simple" "simple" "SIMPLE.html" "" "simple") ("sixth" "sixth" "SIXTH.html" "" "sixth") ("skip-proofs" "skip-proofs" "SKIP-PROOFS.html" "" "skip-proofs") ("slow-array-warning" "slow-array-warning" "SLOW-ARRAY-WARNING.html" "" "slow-array-warning") ("solution-to-simple-example" "solution-to-simple-example" "SOLUTION-TO-SIMPLE-EXAMPLE.html" "" "solution-to-simple-example") ("specious-simplification" "specious-simplification" "SPECIOUS-SIMPLIFICATION.html" "" "specious-simplification") ("standard-char-listp" "standard-char-listp" "STANDARD-CHAR-LISTP.html" "" "standard-char-listp") ("standard-char-p" "standard-char-p" "STANDARD-CHAR-P.html" "" "standard-char-p") ("standard-co" "standard-co" "STANDARD-CO.html" "" "standard-co") ("standard-numberp" "standard-numberp" "STANDARD-NUMBERP.html" "" "standard-numberp") ("standard-oi" "standard-oi" "STANDARD-OI.html" "" "standard-oi") ("standard-part" "standard-part" "STANDARD-PART.html" "" "standard-part") ("standard-string-alistp" "standard-string-alistp" "STANDARD-STRING-ALISTP.html" "" "standard-string-alistp") ("start-proof-tree" "start-proof-tree" "START-PROOF-TREE.html" "" "start-proof-tree") ("startup" "startup" "STARTUP.html" "" "startup") ("state" "state" "STATE.html" "" "state") ("stobj-example-1-defuns" "stobj-example-1-defuns" "STOBJ-EXAMPLE-1-DEFUNS.html" "" "stobj-example-1-defuns") ("stobj-example-1-implementation" "stobj-example-1-implementation" "STOBJ-EXAMPLE-1-IMPLEMENTATION.html" "" "stobj-example-1-implementation") ("stobj-example-1-proofs" "stobj-example-1-proofs" "STOBJ-EXAMPLE-1-PROOFS.html" "" "stobj-example-1-proofs") ("stobj-example-1" "stobj-example-1" "STOBJ-EXAMPLE-1.html" "" "stobj-example-1") ("stobj-example-2" "stobj-example-2" "STOBJ-EXAMPLE-2.html" "" "stobj-example-2") ("stobj-example-3" "stobj-example-3" "STOBJ-EXAMPLE-3.html" "" "stobj-example-3") ("stobj" "stobj" "STOBJ.html" "" "stobj") ("stobjs" "stobjs" "STOBJS.html" "" "stobjs") ("stop-proof-tree" "stop-proof-tree" "STOP-PROOF-TREE.html" "" "stop-proof-tree") ("string-append" "string-append" "STRING-APPEND.html" "" "string-append") ("string-downcase" "string-downcase" "STRING-DOWNCASE.html" "" "string-downcase") ("string-equal" "string-equal" "STRING-EQUAL.html" "" "string-equal") ("string-listp" "string-listp" "STRING-LISTP.html" "" "string-listp") ("string-upcase" "string-upcase" "STRING-UPCASE.html" "" "string-upcase") ("string" "string" "STRING.html" "" "string") ("stringp" "stringp" "STRINGP.html" "" "stringp") ("strip-cars" "strip-cars" "STRIP-CARS.html" "" "strip-cars") ("strip-cdrs" "strip-cdrs" "STRIP-CDRS.html" "" "strip-cdrs") ("sublis" "sublis" "SUBLIS.html" "" "sublis") ("subseq" "subseq" "SUBSEQ.html" "" "subseq") ("subsetp-equal" "subsetp-equal" "SUBSETP-EQUAL.html" "" "subsetp-equal") ("subsetp" "subsetp" "SUBSETP.html" "" "subsetp") ("subst" "subst" "SUBST.html" "" "subst") ("substitute" "substitute" "SUBSTITUTE.html" "" "substitute") ("subversive-inductions" "subversive-inductions" "SUBVERSIVE-INDUCTIONS.html" "" "subversive-inductions") ("subversive-recursions" "subversive-recursions" "SUBVERSIVE-RECURSIONS.html" "" "subversive-recursions") ("symbol-alistp" "symbol-alistp" "SYMBOL-ALISTP.html" "" "symbol-alistp") ("symbol-listp" "symbol-listp" "SYMBOL-LISTP.html" "" "symbol-listp") ("symbol-name" "symbol-name" "SYMBOL-NAME.html" "" "symbol-name") ("symbol-package-name" "symbol-package-name" "SYMBOL-PACKAGE-NAME.html" "" "symbol-package-name") ("symbolp" "symbolp" "SYMBOLP.html" "" "symbolp") ("syntax" "syntax" "SYNTAX.html" "" "syntax") ("syntaxp-examples" "syntaxp-examples" "SYNTAXP-EXAMPLES.html" "" "syntaxp-examples") ("syntaxp" "syntaxp" "SYNTAXP.html" "" "syntaxp") ("sys-call-status" "sys-call-status" "SYS-CALL-STATUS.html" "" "sys-call-status") ("sys-call" "sys-call" "SYS-CALL.html" "" "sys-call") ("table" "table" "TABLE.html" "" "table") ("take" "take" "TAKE.html" "" "take") ("tenth" "tenth" "TENTH.html" "" "tenth") ("term-order" "term-order" "TERM-ORDER.html" "" "term-order") ("term-table" "term-table" "TERM-TABLE.html" "" "term-table") ("term" "term" "TERM.html" "" "term") ("the-method" "the-method" "THE-METHOD.html" "" "the-method") ("the" "the" "THE.html" "" "the") ("theories" "theories" "THEORIES.html" "" "theories") ("theory-functions" "theory-functions" "THEORY-FUNCTIONS.html" "" "theory-functions") ("theory-invariant" "theory-invariant" "THEORY-INVARIANT.html" "" "theory-invariant") ("theory" "theory" "THEORY.html" "" "theory") ("third" "third" "THIRD.html" "" "third") ("thm" "thm" "THM.html" "" "thm") ("tidbits" "tidbits" "TIDBITS.html" "" "tidbits") ("time$" "time$" "TIME$.html" "" "time$") ("tips" "tips" "TIPS.html" "" "tips") ("toggle-pc-macro" "toggle-pc-macro" "TOGGLE-PC-MACRO.html" "" "toggle-pc-macro") ("trace$" "trace$" "TRACE$.html" "" "trace$") ("trace" "trace" "TRACE.html" "" "trace") ("trans" "trans" "TRANS.html" "" "trans") ("trans1" "trans1" "TRANS1.html" "" "trans1") ("true-list-listp" "true-list-listp" "TRUE-LIST-LISTP.html" "" "true-list-listp") ("true-listp" "true-listp" "TRUE-LISTP.html" "" "true-listp") ("truncate" "truncate" "TRUNCATE.html" "" "truncate") ("ttags-seen" "ttags-seen" "TTAGS-SEEN.html" "" "ttags-seen") ("ttree" "ttree" "TTREE.html" "" "ttree") ("tutorial-examples" "tutorial-examples" "TUTORIAL-EXAMPLES.html" "" "tutorial-examples") ("tutorial1-towers-of-hanoi" "tutorial1-towers-of-hanoi" "TUTORIAL1-TOWERS-OF-HANOI.html" "" "tutorial1-towers-of-hanoi") ("tutorial2-eights-problem" "tutorial2-eights-problem" "TUTORIAL2-EIGHTS-PROBLEM.html" "" "tutorial2-eights-problem") ("tutorial3-phonebook-example" "tutorial3-phonebook-example" "TUTORIAL3-PHONEBOOK-EXAMPLE.html" "" "tutorial3-phonebook-example") ("tutorial4-defun-sk-example" "tutorial4-defun-sk-example" "TUTORIAL4-DEFUN-SK-EXAMPLE.html" "" "tutorial4-defun-sk-example") ("tutorial5-miscellaneous-examples" "tutorial5-miscellaneous-examples" "TUTORIAL5-MISCELLANEOUS-EXAMPLES.html" "" "tutorial5-miscellaneous-examples") ("type-prescription" "type-prescription" "TYPE-PRESCRIPTION.html" "" "type-prescription") ("type-set-inverter" "type-set-inverter" "TYPE-SET-INVERTER.html" "" "type-set-inverter") ("type-set" "type-set" "TYPE-SET.html" "" "type-set") ("type-spec" "type-spec" "TYPE-SPEC.html" "" "type-spec") ("u" "u" "U.html" "" "u") ("ubt-prehistory" "ubt-prehistory" "UBT-PREHISTORY.html" "" "ubt-prehistory") ("ubt" "ubt" "UBT.html" "" "ubt") ("ubu" "ubu" "UBU.html" "" "ubu") ("unary--" "unary--" "UNARY--.html" "" "unary--") ("uncertified-books" "uncertified-books" "UNCERTIFIED-BOOKS.html" "" "uncertified-books") ("union-eq" "union-eq" "UNION-EQ.html" "" "union-eq") ("union-equal" "union-equal" "UNION-EQUAL.html" "" "union-equal") ("union-theories" "union-theories" "UNION-THEORIES.html" "" "union-theories") ("universal-theory" "universal-theory" "UNIVERSAL-THEORY.html" "" "universal-theory") ("unmonitor" "unmonitor" "UNMONITOR.html" "" "unmonitor") ("unsave" "unsave" "UNSAVE.html" "" "unsave") ("untrace$" "untrace$" "UNTRACE$.html" "" "untrace$") ("untranslate" "untranslate" "UNTRANSLATE.html" "" "untranslate") ("update-nth" "update-nth" "UPDATE-NTH.html" "" "update-nth") ("upper-case-p" "upper-case-p" "UPPER-CASE-P.html" "" "upper-case-p") ("use" "use" "USE.html" "" "use") ("user-defined-functions-table" "user-defined-functions-table" "USER-DEFINED-FUNCTIONS-TABLE.html" "" "user-defined-functions-table") ("using-computed-hints-1" "using-computed-hints-1" "USING-COMPUTED-HINTS-1.html" "" "using-computed-hints-1") ("using-computed-hints-2" "using-computed-hints-2" "USING-COMPUTED-HINTS-2.html" "" "using-computed-hints-2") ("using-computed-hints-3" "using-computed-hints-3" "USING-COMPUTED-HINTS-3.html" "" "using-computed-hints-3") ("using-computed-hints-4" "using-computed-hints-4" "USING-COMPUTED-HINTS-4.html" "" "using-computed-hints-4") ("using-computed-hints-5" "using-computed-hints-5" "USING-COMPUTED-HINTS-5.html" "" "using-computed-hints-5") ("using-computed-hints-6" "using-computed-hints-6" "USING-COMPUTED-HINTS-6.html" "" "using-computed-hints-6") ("using-computed-hints-7" "using-computed-hints-7" "USING-COMPUTED-HINTS-7.html" "" "using-computed-hints-7") ("using-computed-hints-8" "using-computed-hints-8" "USING-COMPUTED-HINTS-8.html" "" "using-computed-hints-8") ("using-computed-hints" "using-computed-hints" "USING-COMPUTED-HINTS.html" "" "using-computed-hints") ("verbose-pstack" "verbose-pstack" "VERBOSE-PSTACK.html" "" "verbose-pstack") ("verify-guards" "verify-guards" "VERIFY-GUARDS.html" "" "verify-guards") ("verify-termination" "verify-termination" "VERIFY-TERMINATION.html" "" "verify-termination") ("verify" "verify" "VERIFY.html" "" "verify") ("version" "version" "VERSION.html" "" "version") ("well-founded-relation" "well-founded-relation" "WELL-FOUNDED-RELATION.html" "" "well-founded-relation") ("wet" "wet" "WET.html" "" "wet") ("why-brr" "why-brr" "WHY-BRR.html" "" "why-brr") ("with-error-trace" "with-error-trace" "WITH-ERROR-TRACE.html" "" "with-error-trace") ("with-local-stobj" "with-local-stobj" "WITH-LOCAL-STOBJ.html" "" "with-local-stobj") ("with-output" "with-output" "WITH-OUTPUT.html" "" "with-output") ("with-prover-time-limit" "with-prover-time-limit" "WITH-PROVER-TIME-LIMIT.html" "" "with-prover-time-limit") ("world" "world" "WORLD.html" "" "world") ("wormhole-p" "wormhole-p" "WORMHOLE-P.html" "" "wormhole-p") ("wormhole" "wormhole" "WORMHOLE.html" "" "wormhole") ("write-byte$" "write-byte$" "WRITE-BYTE$.html" "" "write-byte$") ("xargs" "xargs" "XARGS.html" "" "xargs") ("zero-test-idioms" "zero-test-idioms" "ZERO-TEST-IDIOMS.html" "" "zero-test-idioms") ("zerop" "zerop" "ZEROP.html" "" "zerop") ("zip" "zip" "ZIP.html" "" "zip") ("zp" "zp" "ZP.html" "" "zp") ("zpf" "zpf" "ZPF.html" "" "zpf"))