acl2-source 7.2dfsg-3 / usr / share / acl2-7.2dfsg / acl2-proclaims.lisp

(COMMON-LISP::IN-PACKAGE "COMMON-LISP-USER") 
(COMMON-LISP::PROCLAIM
    '(COMMON-LISP::FTYPE
         (COMMON-LISP::FUNCTION (COMMON-LISP::STRING) COMMON-LISP::T)
         ACL2::PKG-WITNESS ACL2::PKG-IMPORTS)) 
(COMMON-LISP::PROCLAIM
    '(COMMON-LISP::FTYPE
         (COMMON-LISP::FUNCTION (COMMON-LISP::T COMMON-LISP::T)
             COMMON-LISP::FIXNUM)
         ACL2::SER-DECODE-AND-LOAD-RATS ACL2::SER-DECODE-AND-LOAD-CHARS
         ACL2::TYPE-SET-BINARY-+-ALIST-ENTRY
         ACL2::SER-DECODE-AND-LOAD-COMPLEXES
         ACL2::SER-DECODE-AND-LOAD-NATS ACL2::TYPE-SET-<-ALIST-ENTRY
         ACL2::TYPE-SET-BINARY-*-ALIST-ENTRY)) 
(COMMON-LISP::PROCLAIM
    '(COMMON-LISP::FTYPE
         (COMMON-LISP::FUNCTION
             (COMMON-LISP::FIXNUM COMMON-LISP::FIXNUM)
             COMMON-LISP::FIXNUM)
         ACL2::TIMES-MOD-M31 ACL2::PLUS-MOD-M31 ACL2::MIN-FIXNUM)) 
(COMMON-LISP::PROCLAIM
    '(COMMON-LISP::FTYPE
         (COMMON-LISP::FUNCTION (COMMON-LISP::FIXNUM COMMON-LISP::T)
             COMMON-LISP::T)
         ACL2::AREF-32-BIT-INTEGER-STACK ACL2::AREF-T-STACK
         ACL2::CHECK-SUM-INC)) 
(COMMON-LISP::PROCLAIM
    '(COMMON-LISP::FTYPE
         (COMMON-LISP::FUNCTION (COMMON-LISP::INTEGER COMMON-LISP::T)
             COMMON-LISP::T)
         ACL2::SHRINK-32-BIT-INTEGER-STACK ACL2::SHRINK-T-STACK
         ACL2::CHECK-SUM-NATURAL)) 
(COMMON-LISP::PROCLAIM
    '(COMMON-LISP::FTYPE
         (COMMON-LISP::FUNCTION
             (COMMON-LISP::INTEGER COMMON-LISP::FIXNUM)
             COMMON-LISP::FIXNUM)
         ACL2::FCHECKSUM-NATURAL-AUX)) 
(COMMON-LISP::PROCLAIM
    '(COMMON-LISP::FTYPE
         (COMMON-LISP::FUNCTION COMMON-LISP::NIL COMMON-LISP::T)
         ACL2::WHAT-IS-THE-GLOBAL-STATE ACL2::DMR-STRING ACL2::BIG-N
         ACL2::LENGTH-MEMOIZED-FUNCTIONS ACL2::UNMEMOIZE-ALL
         ACL2::MEMOIZE-INIT ACL2::ACL2H-INIT-MEMOIZATIONS
         ACL2::HCOMP-TRANSFER-TO-HASH-TABLES ACL2::OUR-UNAME
         ACL2::GET-INTERNAL-TIME ACL2::HONS-SUMMARY
         ACL2::LOWER-OVERHEAD ACL2::PRINT-CALL-STACK
         ACL2::CHECK-STATE-GLOBALS-INITIALIZED
         ACL2::INSTALL-OLD-RAW-PROMPT
         ACL2::INITIALIZE-FC-WORMHOLE-SITES ACL2::SETUP-STANDARD-IO
         ACL2::PRIMITIVE-EVENT-MACROS ACL2::BREAK$
         ACL2::MEMOIZED-FUNCTIONS ACL2::CREATE-STATE
         ACL2::INITIALIZE-DMR-INTERVAL-USED
         ACL2::HL-MAYBE-INITIALIZE-DEFAULT-HS
         ACL2::INSTALL-NEW-RAW-PROMPT ACL2::ILLEGAL-MSG
         ACL2::INCREMENT-TRACE-LEVEL ACL2::SET-INITIAL-CBD
         ACL2::UNMEMOIZE-PROFILED ACL2::ACL2H-INIT ACL2::DMR-DISPLAY
         ACL2::DMR-STOP-FN-RAW ACL2::CHECK-BUILT-IN-CONSTANTS
         ACL2::LATEST-RELEASE-NOTE-STRING ACL2::FAST-ALIST-SUMMARY
         ACL2::HL-HSPACE-FALTABLE-WRAPPER ACL2::MEMOIZE-SUMMARY-SORT
         ACL2::PONS-SUMMARY ACL2::HONS-WASH
         ACL2::SAVED-BUILD-DATE-STRING
         ACL2::HL-MAYBE-INITIALIZE-DEFAULT-HS-WRAPPER
         ACL2::RESTORE-FC-REPORT-SETTINGS ACL2::TRACE-EVISC-TUPLE
         ACL2::INITIAL-MEMOIZE-INFO-HT ACL2::10-DAYS
         ACL2::CLEAR-MEMOIZE-CALL-ARRAY
         ACL2::MEMOIZE-SUMMARY-AFTER-COMPUTE-CALLS-AND-TIMES
         ACL2::CHECK-ACL2-INITIALIZATION ACL2::NIL-FN
         ACL2::CLEAR-MEMOIZE-STATISTICS ACL2::RESET-FC-REPORTING
         ACL2::HONS-WASH! ACL2::INITIALIZE-ACCUMULATED-WARNINGS
         ACL2::PRINT-NOT-CALLED ACL2::CLEAR-MEMOIZE-TABLES
         ACL2::MEMOIZE-SUMMARY ACL2::INITIALIZE-NEVER-MEMOIZE-HT
         ACL2::FLOAT-TICKS/SECOND-INIT ACL2::SHOW-FC-CRITERIA
         ACL2::CW-GSTACK-SHORT ACL2::SAVE-FC-REPORT-SETTINGS
         ACL2::DEFAULT-TOTAL-PARALLELISM-WORK-LIMIT ACL2::ABORT!
         ACL2::DMR-PREFIX ACL2::CLEAR-MEMO-TABLES ACL2::HCOMP-INIT
         ACL2::COMPUTE-CALLS-AND-TIMES ACL2::IDATE
         ACL2::PRINT-MEMO-MAX-SIZES ACL2::PROFILED-FUNCTIONS
         ACL2::HL-SYSTEM-GC ACL2::DMR-FILE-NAME ACL2::P!
         ACL2::IMMEDIATE-FORCE-MODEP ACL2::PRINT-CALL-HISTORY
         ACL2::INCREMENT-*FILE-CLOCK* ACL2::EXIT-BOOT-STRAP-MODE)) 
(COMMON-LISP::PROCLAIM
    '(COMMON-LISP::FTYPE
         (COMMON-LISP::FUNCTION (COMMON-LISP::INTEGER COMMON-LISP::T)
             COMMON-LISP::*)
         ACL2::RANDOM$)) 
(COMMON-LISP::PROCLAIM
    '(COMMON-LISP::FTYPE
         (COMMON-LISP::FUNCTION (COMMON-LISP::FIXNUM COMMON-LISP::T)
             COMMON-LISP::*)
         ACL2::COMBINE-OP-CSTS1 ACL2::COMBINE-IF-CSTS1)) 
(COMMON-LISP::PROCLAIM
    '(COMMON-LISP::FTYPE
         (COMMON-LISP::FUNCTION COMMON-LISP::NIL COMMON-LISP::*)
         ACL2::CHECK-INVARIANT-RISK-STATE-P
         ACL2::ENTER-BOOT-STRAP-PASS-2 ACL2::HCOMP-ALISTS-FROM-HTS
         ACL2::INITIAL-CUSTOMIZATION-FILENAME)) 
(COMMON-LISP::PROCLAIM
    '(COMMON-LISP::FTYPE
         (COMMON-LISP::FUNCTION (COMMON-LISP::T) COMMON-LISP::LIST)
         ACL2::SER-ENCODER-COMPLEXES ACL2::SER-ENCODER-SYMBOL-AL
         ACL2::SER-ENCODER-NATURALS ACL2::SER-ENCODER-CHARS
         ACL2::SER-ENCODER-STRINGS ACL2::SER-ENCODER-RATIONALS)) 
(COMMON-LISP::PROCLAIM
    '(COMMON-LISP::FTYPE
         (COMMON-LISP::FUNCTION (COMMON-LISP::T)
             (COMMON-LISP::SIMPLE-ARRAY COMMON-LISP::BIT
                 (COMMON-LISP::*)))
         ACL2::HL-HSPACE-SBITS)) 
(COMMON-LISP::PROCLAIM
    '(COMMON-LISP::FTYPE
         (COMMON-LISP::FUNCTION
             (COMMON-LISP::STRING COMMON-LISP::T COMMON-LISP::FIXNUM
                 COMMON-LISP::FIXNUM COMMON-LISP::FIXNUM COMMON-LISP::T
                 COMMON-LISP::T COMMON-LISP::T)
             COMMON-LISP::*)
         ACL2::FMT0)) 
(COMMON-LISP::PROCLAIM
    '(COMMON-LISP::FTYPE
         (COMMON-LISP::FUNCTION
             (COMMON-LISP::STRING COMMON-LISP::INTEGER
                 COMMON-LISP::INTEGER COMMON-LISP::FIXNUM)
             COMMON-LISP::FIXNUM)
         ACL2::FCHECKSUM-STRING2)) 
(COMMON-LISP::PROCLAIM
    '(COMMON-LISP::FTYPE
         (COMMON-LISP::FUNCTION
             (COMMON-LISP::STRING COMMON-LISP::FIXNUM
                 COMMON-LISP::FIXNUM COMMON-LISP::FIXNUM)
             COMMON-LISP::FIXNUM)
         ACL2::FCHECKSUM-STRING1)) 
(COMMON-LISP::PROCLAIM
    '(COMMON-LISP::FTYPE
         (COMMON-LISP::FUNCTION
             (COMMON-LISP::STRING COMMON-LISP::T COMMON-LISP::FIXNUM
                 COMMON-LISP::FIXNUM)
             COMMON-LISP::T)
         ACL2::FMT-VAR)) 
(COMMON-LISP::PROCLAIM
    '(COMMON-LISP::FTYPE
         (COMMON-LISP::FUNCTION
             (COMMON-LISP::STRING COMMON-LISP::FIXNUM
                 COMMON-LISP::FIXNUM)
             COMMON-LISP::FIXNUM)
         ACL2::FIND-ALTERNATIVE-SKIP ACL2::SCAN-PAST-WHITESPACE
         ACL2::FIND-ALTERNATIVE-STOP)) 
(COMMON-LISP::PROCLAIM
    '(COMMON-LISP::FTYPE
         (COMMON-LISP::FUNCTION
             (COMMON-LISP::STRING COMMON-LISP::T COMMON-LISP::T
                 COMMON-LISP::T)
             COMMON-LISP::T)
         ACL2::CHECK-SUM-STRING2)) 
(COMMON-LISP::PROCLAIM
    '(COMMON-LISP::FTYPE
         (COMMON-LISP::FUNCTION
             (COMMON-LISP::STRING COMMON-LISP::T COMMON-LISP::T)
             COMMON-LISP::T)
         ACL2::SER-ENCODE-PACKAGE)) 
(COMMON-LISP::PROCLAIM
    '(COMMON-LISP::FTYPE
         (COMMON-LISP::FUNCTION
             (COMMON-LISP::FIXNUM COMMON-LISP::STRING
                 COMMON-LISP::FIXNUM COMMON-LISP::FIXNUM)
             COMMON-LISP::FIXNUM)
         ACL2::FIND-ALTERNATIVE-START1)) 
(COMMON-LISP::PROCLAIM
    '(COMMON-LISP::FTYPE
         (COMMON-LISP::FUNCTION (COMMON-LISP::T COMMON-LISP::T)
             COMMON-LISP::T)
         ACL2_*1*_COMMON-LISP::COMPLEX ACL2::HITP ACL2::CONJOIN2
         ACL2::TOO-MANY-IFS-POST-REWRITE-BUILTIN
         ACL2::GET-NORMALIZED-BODIES ACL2::SET-DIFFERENCE-EQL-EXEC
         ACL2::DESTRUCTORS-LST ACL2::DEFAXIOM-SUPPORTER-MSG-LIST
         ACL2::PT-OCCUR ACL2::MFC-FORCE-FLG
         ACL2::CONVERT-RETURNED-VARS-TO-TERM-LST
         ACL2::SET-RW-CACHE-STATE-IN-PSPV ACL2::TABLE-ALIST
         ACL2::NONNEGATIVE-INTEGER-QUOTIENT ACL2::SYMBOL-CLASS
         ACL2::INITIALIZE-TAU-PRED ACL2::CDRP ACL2::CANCEL2
         ACL2::TERM-ORDER ACL2::DELETE-NAMES-FROM-KPA
         ACL2::MEMBER-EQUAL-MOD-COMMUTING-LST ACL2::FFNNAMES-SUBSETP
         ACL2::SUBLIS-VAR-LST ACL2::ALL-INSTANTIABLEP
         ACL2::RELATIVE-TO-ABSOLUTE-COMMAND-NUMBER
         ACL2::SYSFILE-TO-FILENAME-INCLUDE-BOOK-ENTRY
         ACL2_*1*_COMMON-LISP::COERCE ACL2::XXXJOIN
         ACL2::CHECK-VARS-NOT-FREE-TEST ACL2::SIMPLE-SIGNATUREP
         ACL2::SOME-CONGRUENCE-RULE-DISABLEDP
         ACL2::ATTACHMENT-COMPONENT-OWNER ACL2::MERGE-SYMBOL-ALISTP
         ACL2::FROMTO ACL2::SET-DIFFERENCE-EQ-EXEC$GUARD-CHECK
         ACL2::EVAL-TAU-INTERVAL1 ACL2::GET-LEVEL-NO
         ACL2::UNIVERSAL-THEORY-FN ACL2::CHECKPOINT-WORLD
         ACL2::FIND-RUNED-LINEAR-LEMMA
         ACL2::MAKE-LET-PAIRS-FROM-FORMALS ACL2::INDUCTION-COMPLEXITY1
         ACL2::POWER-REP ACL2::RECOVER-DEFS-LST
         ACL2::SET-GC-THRESHOLD$-FN ACL2::TYPESPEC-CHECK
         ACL2::BAD-ATOM<= ACL2::MAKE-POSNS
         ACL2::HYPS-THAT-INSTANTIATE-FREE-VARS
         ACL2::TAU-VISIT-FUNCTION-INTRODUCTIONS
         ACL2::OLD-DEFSTOBJ-REDUNDANCY-BUNDLE ACL2::ASSOC-EQ-EXEC
         ACL2::TAU-PAIRS-INTERSECTIONP ACL2::PAIRLIS-X1
         ACL2::CURRENT-IMMEDIATE-DEPS
         ACL2::ADD-TYPE-ALIST-RUNES-TO-TTREE1 ACL2::SLOW-ARRAY-WARNING
         ACL2::MEMBER-EQ-EXEC$GUARD-CHECK ACL2::READ-FILE-INTO-STRING2
         ACL2::NEGATIVE-UPPER-BOUNDP ACL2::UPDATE-CURRENT-THEORY
         ACL2::PATHNAME-UNIX-TO-OS ACL2::SUBLIS-VAR-LSTP
         ACL2::PROCESS-ASSUMPTIONS-TTREE ACL2::MAYBE-FINISH-OUTPUT$
         ACL2::TERMINATION-THEOREM ACL2::MF-PRINT-ALIST
         ACL2::GAG-START-MSG ACL2::FREE-VARSP-LST
         ACL2::EQUAL-MODULO-HIDDEN-DEFPKGS ACL2::O< ACL2::CONS-SUBTREES
         ACL2::DECODE-LOGICAL-NAME ACL2::SUBSETP-EQUAL
         ACL2::INTRO-UDF-LST2 ACL2::FIND-DUPLICATE-GENERALIZE-ENTRIES
         ACL2::PRINT-GAG-INFO ACL2::SUBLIS-EQUAL ACL2::ASSOC-RW-CACHE
         ACL2::CONJOIN-CLAUSE-SETS ACL2::BIG-M-LITTLE-M-CLIQUE
         ACL2::MAKE-CONTROLLER-ALIST ACL2::CLOSE-CHANNELS
         ACL2::INDUCT-VARS ACL2::COLLECT-LOGICALS ACL2::CHANGE-LAST
         ACL2::COLLECT-NON-X ACL2::UPDATE-BIG-CLOCK-ENTRY
         ACL2::MAXIMIZE-FERTILIZE-COMPLEXITY ACL2::SET-PRINT-LENGTH
         ACL2::PART-OF1 ACL2::STRIP-NON-NIL-BASE-SYMBOLS
         ACL2::SUBBAGP-EQ ACL2::DECODE-CST-ALIST ACL2::PAIRLIS$
         ACL2::REMOVE-INVISIBLE-FNCALLS ACL2::WORLD-TO-NEXT-COMMAND
         ACL2::NON-TERM-LISTP-MSG ACL2::ASSOC-EQUAL-CADR
         ACL2::FORMAL-VALUE-TRIPLE ACL2::HL-MAYBE-RESIZE-HT
         ACL2::RETRACT-WORLD ACL2::FILTER-GENEQV-LST
         ACL2::NON-PRIMITIVE-INSTRUCTIONS ACL2::PRINT-TYPE-ALIST
         ACL2::PUT-TTREE-INTO-PSPV ACL2::FORBIDDEN-FNS
         ACL2::ASSOC-PROOF-SUPPORTERS-ALIST ACL2::COLLECT-ASSUMPTIONS
         ACL2::INTERSECTION-EQUAL ACL2::IF-INTERP-ASSUMED-VALUE
         ACL2::COLLECT-NON-TRIVIAL-BINDINGS ACL2::ENABLED-LMI-NAMES1
         ACL2::SOME-BDD-CONSTRUCTORP
         ACL2::FILENAME-TO-SYSFILE-TTAG-ALIST-VAL ACL2::SUBLIS-VAR
         ACL2::ALIST-KEYS-SUBSETP ACL2::EQUAL-MOD-COMMUTING-LST
         ACL2::ALL-FNNAMES-WORLD ACL2::PRUNE-POLY-LST
         ACL2::COMPONENT-PATH-EXTENSION ACL2::TAGGED-OBJECT
         ACL2::SOME-POOL-MEMBER-SUBSUMES ACL2::BINARY-APPEND
         ACL2::ALL-RUNES-IN-TTREE-FIND-EQUATIONAL-POLY-LST
         ACL2::TRUNCATE-CLASSES ACL2::TS<
         ACL2::PRETTYIFY-FC-DERIVATIONS
         ACL2::MIS-ORDERED-COMMUTATIVE-ARGS ACL2::PT-INTERSECTP
         ACL2::DELETE-EXPANSION-FILE ACL2::IN-ENCAPSULATEP
         ACL2::COLLECT-TAU-BIG-SWITCHES ACL2::IO?-NIL-OUTPUT
         ACL2::THEORY-FN ACL2::HL-HSPACE-NUMBER-SUBTREES
         ACL2::BOUNDP-GLOBAL ACL2::CONTROLLER-VARIABLES1
         ACL2::ALL-VARS1-LST-LST ACL2::FCOMPLEMENTARY-MULTIPLEP
         ACL2::FIND-RULES-OF-RUNE ACL2::SET-COMPILER-ENABLED
         ACL2::UPDATE-FILE-CLOCK ACL2::UPDATE-READ-FILES
         ACL2::BOUNDP-GLOBAL1 ACL2::FREE-VARSP-MEMBER-LST
         ACL2::CHECK-DCL-GUARDIAN ACL2::EQUAL-MOD-ELIDE-LOCALS-LST
         ACL2::SUBLIS-EXPR-NON-QUOTEPS ACL2::POP-ACCP-FN
         ACL2::FIRST-NON-MEMBER-EQ ACL2::SET-PRINT-ESCAPE
         ACL2::QUICK-AND-DIRTY-SRS-BUILTIN
         ACL2::ALL-RUNES-IN-TTREE-FC-DERIVATION-LST ACL2::PAIRLIS2
         ACL2::MERGE-RUNES ACL2::TILDE-@-ASSUMNOTES-PHRASE-LST
         ACL2::FIND-SUBJECT-BOUNDER-LINK-TERM ACL2::NORMALIZE-POLY1
         ACL2::RELEVANT-GROUND-LEMMAS ACL2::CHECK-OUT-INSTANTIABLEP1
         ACL2::PE-EVENT-FORM ACL2::OUTPUT-IGNORED-P
         ACL2::PUSH-MV-NTH-DOWN ACL2::MAKE-INITIAL-MEMOIZE-HASH-TABLE
         ACL2::TILDE-*-MEASURE-PHRASE ACL2::POP-ACCP-FN-ITERATE
         ACL2::SHOW-RETRIEVED-GOAL ACL2::REC-FNNAMES-LST
         ACL2::MEMOIZE-LOOK-UP-DEF-RAW ACL2::SET-CL-IDS-OF-ASSUMPTIONS
         ACL2::TRACE$-VALUE-MSGP ACL2::COLLECT-NON-LOGIC-MODE
         ACL2::COLLECT-POSP-INDICES-TO-HEADER ACL2::DUMB-OCCUR-LST
         ACL2::SCAN-PAST-DEEPER-EVENT-LANDMARKS
         ACL2::DEFSTOBJ-AXIOMATIC-INIT-FIELDS
         ACL2::MERGE-ARITH-TERM-ORDER ACL2::MERGE-TERM-ORDER
         ACL2::IF-INTERP-ASSUMED-VALUE0
         ACL2::SET-TOTAL-PARALLELISM-WORK-LIMIT-ERROR-FN
         ACL2::M&M-OVER-POWERSET ACL2::DUMB-OCCUR-IN-TYPE-ALIST
         ACL2::NAME-INTRODUCED ACL2::TAU-INTERVAL-EQUAL-DECIDER
         ACL2::SATISFYING-FC-DERIVATION1P ACL2::UNMEASURED-VARIABLES2
         ACL2::ALMOST-LEXORDER-SINGLETONS ACL2::PROGRAM-TERM-LISTP
         ACL2::CLAUSE-SET-DIFFICULTY ACL2::STOBJ-RECOGNIZER-P
         ACL2::BEING-OPENEDP-REC ACL2::MAKE-RECORD-MAKER-CONS
         ACL2::GET-EVG ACL2::EARLIER-ACL2-VERSIONP
         ACL2::POLYS-WITH-VAR1 ACL2::OCCUR-LST
         ACL2::HL-ALIST-LONGEST-NORMED-TAIL ACL2::NEWLINE
         ACL2::MULTIPLE-ASSOC-TERMINAL-SUBSTRINGP
         ACL2::LISP-BOOK-SYNTAXP1 ACL2::MEASURED-VARIABLES
         ACL2::PUFFABLE-COMMAND-NUMBERP ACL2::MERGE-CAND1-INTO-CAND2
         ACL2::UPDATE-32-BIT-INTEGER-STACK ACL2::UPDATE-IPRINT-ALIST
         ACL2::COLLECT-TAU-RELEVANT-TRIPLES ACL2::READ-FILE-INTO-STRING
         ACL2::NEW-DEFPKG-P ACL2::CHECK-SUM-STRING
         ACL2::DELETE-ASSUMPTIONS ACL2::THROW-OR-ATTACH-CALL
         ACL2::ORIGINAL-DEF-BODY ACL2::SER-ENCODE-CHARS ACL2::MIN-VAR
         ACL2::ACCEPTABLE-TAU-RULEP ACL2::IMPLIES
         ACL2::TYPE-ALIST-SEGMENTS ACL2::CLEAN-BRR-STACK1
         ACL2::OPEN-OUTPUT-CHANNEL-ANY-P1 ACL2::NON-TERM-LIST-LISTP-MSG
         ACL2::HONS-EQUAL ACL2::BOUNDER-SUBSUMEDP-BY-SOME
         ACL2::SYSFILE-TO-FILENAME-TTAG-ALIST-VAL ACL2::NO-NEW-NAMESP
         ACL2::EXTEND-SORTED-SYMBOL-ALIST
         ACL2::SET-TOTAL-PARALLELISM-WORK-LIMIT-FN ACL2::OCCUR
         ACL2::TAU-PAIRS-SUBSETP ACL2::BINARY-+
         ACL2::DELETE-NAMES-FROM-KPA-REC ACL2::TMP-FILENAME
         ACL2::EVG-OCCUR ACL2::PARTITION-ACCORDING-TO-ASSUMPTION-TERM
         ACL2::FILENAME-TO-SYSFILE-TTAG-ALISTP
         ACL2::INDUCTION-HYP-CLAUSE-SEGMENTS ACL2::SET-IPRINT-AR
         ACL2::ARRAY2P ACL2::RESTORE-RW-CACHE-ANY-TAG
         ACL2::RECORD-GAG-STATE ACL2::SER-ENCODE-PACKAGES
         ACL2::TAU-LIKE-SUBJECT-CRITERION
         ACL2::TILDE-*-ELIM-PHRASE/ALIST1
         ACL2::OPEN-INPUT-CHANNEL-ANY-P1 ACL2::DECODE-TAU-ALIST
         ACL2::ASSOC-EQ-EXEC$GUARD-CHECK ACL2::OUR-IMPORT
         ACL2::GENERATE-VARIABLE-LST-SIMPLE
         ACL2::ALL-RUNES-IN-VAR-TO-RUNES-ALIST-LST
         ACL2::REMOVE-TAG-FROM-TAG-TREE!
         ACL2::ENFORCE-REDUNDANCY-ER-ARGS ACL2::AUGMENT-THEORY
         ACL2::STOBJ-FIELD-FN-OF-STOBJ-TYPE-P
         ACL2::CHK-ASSUMPTION-FREE-TTREE-1 ACL2::MERGE-CAR-<
         ACL2::CONS-SUBSET-TREE ACL2::ALL-DUMB-OCCUR-IN-TYPE-ALIST
         ACL2::SUBLIS-EXPR-LST ACL2::INTERSECTP-EQ-EXEC$GUARD-CHECK
         ACL2::PART-OF ACL2::TREE-OCCUR ACL2::CHECK-NONE-IDEAL
         ACL2::DEFUN-NX-FN ACL2::NAMEDP-PREFIX
         ACL2::EXTEND-RULE-CLASSES ACL2::M&M
         ACL2::SYMBOL-NAME-TREE-OCCUR ACL2::FFNNAMEP-MOD-MBE-LST
         ACL2::GET-STOBJ-RECOGNIZER ACL2::CDR-ASSOC-QUERY-ID
         ACL2::THEORYP! ACL2::RULER-EXTENDERS-MSG-AUX
         ACL2::SOME-GENEQV-DISABLEDP ACL2::NORMALIZED-EVALUATOR-CL-SET
         ACL2::TILDE-*-CONJUNCTION-PHRASE1 ACL2::FNSTACK-TERM-MEMBER
         ACL2::BUILT-IN-CLAUSE-DISCRIMINATOR-FN ACL2::ARITH-TERM-ORDER
         ACL2::REMOVE-LISP-SUFFIX ACL2::ALL-RUNES-IN-TTREE-LST
         ACL2::PAIRWISE-SUBSETP-EQ ACL2::CONTROLLER-UNIFY-SUBST2
         ACL2::APPROVED-FC-DERIVATIONP
         ACL2::CONTEXT-FOR-ENCAPSULATE-PASS-2 ACL2::GET-GUARDSP
         ACL2::ALL-VARS-LST-BOUNDP ACL2::EVISCERATION-STOBJ-MARKS1
         ACL2::SETENV$ ACL2::DUPLICITOUS-SORT-CAR
         ACL2::UNRELATIVIZE-BOOK-PATH
         ACL2::FIX-FREE-FAILURE-REASON-ALIST
         ACL2::TILDE-@-WELL-FOUNDED-RELATION-PHRASE
         ACL2::MEMOIZE-USE-ATTACHMENT-WARNING ACL2::RET-STACK
         ACL2::CLEAN-UP-ALIST ACL2::MEMOIZE-FN-SUFFIX
         ACL2::MERGE-LENGTH ACL2::HOW-MANY-TO-BE-PROVED ACL2::CAR/CDR^N
         ACL2::FIRST-ASSOC-EQ ACL2::POSITION-EQUAL
         ACL2::SET-PRINT-LEVEL ACL2::UNENCUMBER-ASSUMPTION
         ACL2::DISJOIN-INTERVALS ACL2::TILDE-*-GEN-PHRASE/ALIST
         ACL2::DUMB-TYPE-ALIST-IMPLICATIONP ACL2::REMOVE-KEYWORD
         ACL2::ALL-RUNES-IN-VAR-TO-RUNES-ALIST ACL2::ORIGINAL-DEF-BODY1
         ACL2::PUT-CURRENT-FC-CALL-ALIST ACL2::EQUAL-X-CONSTANT
         ACL2::SHOW-ACCUMULATED-PERSISTENCE-LIST ACL2::RUNIC-THEORYP
         ACL2::NORMALIZE-STRING ACL2::COLLECT-WHEN-CADR-EQ
         ACL2::QUICK-BLOCK-INFO1 ACL2::DEFATTACH-LOOP-ERROR-MSG
         ACL2::UNIFY-SUBST-SUBSETP ACL2::PRINT-TYPE-ALIST-SEGMENTS
         ACL2::MAKE-DEFTHM-FORMS-FOR-BYES ACL2::BOUNDER-SUBSUMEDP
         ACL2::CANONICAL-SIBLING ACL2::PUSH-WARNING
         ACL2::SER-ENCODE-COMPLEXES ACL2::CORRESPONDING-ENCAPS
         ACL2::INSTALL-GLOBAL-ENABLED-STRUCTURE
         ACL2::ASSOC-STRING-EQUAL
         ACL2::NO-DUPLICATESP-CHECKS-FOR-STOBJ-LET-ACTUALS
         ACL2::SET-EQUALP-EQ ACL2::INCLUDE-BOOK-ALIST-ENTRY-P
         ACL2::SET-WORMHOLE-DATA ACL2::EQUAL-MOD-ELIDE-LOCALS
         ACL2::DECODE-TAU ACL2::RUNEP ACL2::MERGE-CAR-TERM-ORDER
         ACL2::SIGNATE ACL2::UPDATE-USER-STOBJ-ALIST ACL2::FIND-GOAL
         ACL2::FNUME ACL2::QUICK-BLOCK-INFO2
         ACL2::MEMBER-REWRITE-RULE-RUNE ACL2::EXTEND-EACH-VALUE-SET
         ACL2::POSITION-EQL-EXEC$GUARD-CHECK
         ACL2::CROSS-TESTS-AND-CALLS1 ACL2::SET-DIFFERENCE-ASSOC-EQUAL
         ACL2::FAST-ALIST-FORK! ACL2::NEEDS-SLASHES ACL2::TAU-DATA-FN
         ACL2::CONJOIN-INTERVALS ACL2::FETCH-DCL-FIELD ACL2::HEADER
         ACL2::UPDATE-T-STACK ACL2::REMOVE-EQL-EXEC
         ACL2::EQUIVALENCE-RUNE ACL2::BINARY-LOGIOR
         ACL2::EXPAND-ANY-FINAL-IMPLIES1 ACL2::STORE-IN-KILL-RING
         ACL2::SET-EQUALP-EQUAL ACL2::FLUSH-CAND1-DOWN-CAND2
         ACL2::COMPRESS1 ACL2::SET-ABSSTOBJ-DEBUG-FN
         ACL2::ONE-WAY-UNIFY-P ACL2::DECODE-TAU1 ACL2::LOGICAL-<=
         ACL2::RESTRICT-ALIST ACL2::FILTER-GENEQV1 ACL2::BINARY-LOGAND
         ACL2::CLOAKED-SET-W! ACL2::TERM-DIFFICULTY
         ACL2::ACCESS-X-RULE-RUNE
         ACL2::ELIDE-LOCALS-FROM-EXPANSION-ALIST
         ACL2::FIND-EQUIVALENCE-RUNE ACL2::DELETE-ASSOC-EQL-EXEC
         ACL2::HL-HSPACE-PERSISTENT-NORM ACL2::LOGICAL-<
         ACL2::CONTAINS-CONSTRAINED-CONSTANTP
         ACL2::SYSTEM-VERIFY-GUARDS-FN-1 ACL2::DEFABSSTOBJ-MISSING-MSG
         ACL2_*1*_COMMON-LISP::EQUAL ACL2::TAU-INTERVAL-<-DECIDER
         ACL2::TERMP ACL2::MEMBER-EQUAL-+- ACL2::INSTANTIABLEP
         ACL2::EXTEND-VALUE-SET ACL2::STRING-APPEND
         ACL2::DEFSTOBJ-SUPPORTERP ACL2::INSERT-TAU-PAIR
         ACL2::BIND-FREE-VARS-TO-UNBOUND-FREE-VARS
         ACL2::UPDATE-OPEN-INPUT-CHANNELS ACL2::GET-UNNORMALIZED-BODIES
         ACL2::SYMBOL-IN-CURRENT-PACKAGE-P ACL2::TRUNCATE-CLASS-ALIST
         ACL2::CORRESPONDING-INLINE-FN ACL2::HONS-COPY-WITH-STATE
         ACL2::INTERSECTP-EQ/UNION-EQUAL ACL2::HL-FALTABLE-SLOT-LOOKUP
         ACL2::MEMBER-STRING-EQUAL
         ACL2::SHOW-ACCUMULATED-PERSISTENCE-PHRASE
         ACL2::HL-HSPACE-HONSP ACL2::DEFAULT ACL2::HONS-EQUAL-LITE
         ACL2::FUNCTION-THEORY-FN ACL2::METHOD-EXEC
         ACL2::PRINT-PC-DEFTHM ACL2::KNOWN-PACKAGE-ALIST-INCLUDED-P
         ACL2::EQUAL-INSIG ACL2::CASE-LIST ACL2::SORT-APPROVED1-RATING
         ACL2::ALL-ARGS-OCCUR-IN-TOP-CLAUSEP
         ACL2::COLLECT-RUNE-TRIGGER-PAIRS-FROM-FC-DERIVATIONS
         ACL2::ALREADY-USED-BY-FIND-EQUATIONAL-POLYP
         ACL2::REMOVE1-EQ-EXEC$GUARD-CHECK ACL2::SORT-APPROVED1
         ACL2::MAKE-HIDDEN-DEFPKG
         ACL2::CONTAINS-CONSTRAINED-CONSTANTP-LST
         ACL2::INSERT-CDR-TERM-ORDER ACL2::GLOBAL-VAL
         ACL2::PROVED-FUNCTIONAL-INSTANCES-FROM-TAGGED-OBJECTS
         ACL2::RELEVANT-POSNS-LAMBDAS-LST ACL2::PACK2
         ACL2::PC-FREE-INSTR-P ACL2::UPDATE-RNCST-FOR-FORCEP
         ACL2::SATISFYING-FC-ACTIVATIONP ACL2::MAKE-RUNIC-MAPPING-PAIRS
         ACL2::SUBSETP-EQL-EXEC ACL2::APPEND-STRIP-CDRS
         ACL2::REMOVE-EQL-EXEC$GUARD-CHECK ACL2::ABSSTOBJ-NAME
         ACL2::COLLECT-CADRS-WHEN-CAR-EQ ACL2::CROSS-TESTS-AND-CALLS2
         ACL2::MEMBER-NEG-EVGS
         ACL2_*1*_ACL2::INTERN-IN-PACKAGE-OF-SYMBOL
         ACL2::SET-PRINT-BASE ACL2::START-PROOF-TREE-FN
         ACL2_*1*_ACL2::BINARY-* ACL2::FETCH-FROM-ZAP-TABLE
         ACL2::ALL-SIMPLE-SIGNATURESP ACL2::ASSOC-TS-SUBSETP
         ACL2::OP-SEARCH-BUCKET-QUOTE ACL2::POS-EVG-NEAR-SUBSETP
         ACL2::PRINT-NUMBER-BASE-16-UPCASE-DIGITS
         ACL2::SET-PROOFS-CO-STATE ACL2::DEFUN-MODE
         ACL2::STATE-GLOBAL-LET*-CLEANUP ACL2::ACL2-SYSTEM-NAMEP-STATE
         ACL2::EXTEND-WORLD ACL2::TAU-LST-WITH-ACCEPTABLE-DOMAINSP
         ACL2::MAKE-STACK-FROM-ALIST ACL2::THE-NAMEX-SYMBOL-CLASS
         ACL2::DEREF-MACRO-NAME-LST ACL2::SET-PRINT-CASE
         ACL2::RELATIVIZE-BOOK-PATH-LST ACL2::DECODE-TYPE-SET1
         ACL2::ADD-TO-ZAP-TABLE ACL2::HL-FALTABLE-MAPHASH
         ACL2::BOUNDED-INTEGER-ALISTP
         ACL2::CERT-INCLUDE-EXPANSION-ALIST ACL2::ARRAY1P
         ACL2::MSWINDOWS-DRIVE ACL2::UPDATE-IPRINT-AR
         ACL2::MEMBER-EQL-EXEC ACL2::OPEN-OUTPUT-CHANNEL-ANY-P
         ACL2::SYSTEM-EVENTS-FN ACL2::TILDE-*-CONJUNCTION-PHRASE
         ACL2::MAKE-RECORD-CAR-CDRS ACL2::CROSS-PROD
         ACL2::COLLECT-NEVER-UNTOUCHABLE-FNS-ENTRIES
         ACL2::ASSOC-EQL-EXEC ACL2::DIMENSIONS
         ACL2::ADD-SEGMENTS-TO-CLAUSE ACL2::FETCH-DCL-FIELDS1
         ACL2::SER-GATHER-ATOMS ACL2::ADD-SUFFIX-TO-FN
         ACL2::PRIMORDIAL-EVENT-MACROS-AND-FNS ACL2::UNION-EQL-EXEC
         ACL2::FILTER-GENEQV-LST1 ACL2::UNTRANSLATE-HYPS
         ACL2::TILDE-@-ASSUMNOTES-PHRASE-LST-GAG-MODE ACL2::COUNT-OFF
         ACL2::UPDATE-USER-STOBJ-ALIST1 ACL2::DEF-BODY
         ACL2::FILTER-ATOMS ACL2::FLUSH-CANDIDATES
         ACL2::DELETE-ASSOC-EQUAL ACL2::STOBJS-IN
         ACL2::INFECT-TYPE-ALIST-ENTRY ACL2::SHOW-GENEQV
         ACL2::TAU-INTERVAL-DOMAINP ACL2::HONS ACL2::MARRY-PARENTS
         ACL2::PUSH-LEMMA? ACL2::COLLECT-PARENTS0
         ACL2::ALL-RUNES-IN-ELIM-SEQUENCE ACL2::COLLECT-NON-IDEALS
         ACL2::LEN2 ACL2::DELETE-ASSOC-EQUAL-LST ACL2::INSERT-NEG-EVGS
         ACL2::SUPER-DEFSTOBJ-WART-STOBJS-IN ACL2::CHECK-SUM-OBJ1
         ACL2::SUBLIS-VARP ACL2::REPLACE-LAST-CDR
         ACL2::HONS-ASSOC-EQUAL ACL2::SYSFILE-TO-FILENAME-TTAG-ALISTP
         ACL2::UNION-EQ-EXEC ACL2::CLOSE-INPUT-CHANNEL
         ACL2::SET-TEMP-TOUCHABLE-VARS
         ACL2::TAU-BOOLEAN-SIGNATURE-FORMP ACL2::MAXIMUM-LENGTH
         ACL2::HL-HSPACE-FAST-ALIST-FREE
         ACL2::RASSOC-EQ-EXEC$GUARD-CHECK ACL2::>=-LEN ACL2::SOME->
         ACL2::HONS-GET ACL2::TRIVIAL-CLAUSE-P ACL2::FCD-RUNEP-LST
         ACL2::SIMPLE-ARRAY-TYPE
         ACL2::INCLUDE-BOOK-ALIST-EQUAL-MODULO-LOCAL
         ACL2::FREE-VARSP-MEMBER ACL2::DISABLEDP-FN-LST
         ACL2::REMOVE-EQ-EXEC ACL2::VAR-COUNTS ACL2::MAP-CONS-TAG-TREES
         ACL2::GOAL-DEPENDENT-P ACL2::EXPAND-ANY-FINAL-IMPLIES1-LST
         ACL2::SORT-XRUNE-ALIST-BY-RUNE
         ACL2::EXECUTABLE-COUNTERPART-THEORY-FN
         ACL2::DELETE-SOME-SUBSUMED-BOUNDERS ACL2::IMPLICATE
         ACL2::ARG1-ALMOST-SUBSUMES-ARG2 ACL2::NON-FUNCTION-SYMBOLS
         ACL2::SUBLIS-EXPR ACL2::REMOVE1-EQ-EXEC
         ACL2::UPDATE-GUARD-POST ACL2::WARNING-OFF-P
         ACL2::EVISCERATION-STOBJ-MARKS ACL2::FC-REPORT1
         ACL2::LOGIOR-LST ACL2::CONS-TERM-BINARY-*-CONSTANT
         ACL2::ALL-FNNAMES-SUBSUMER ACL2::SET-CBD-STATE
         ACL2::ALL-FNNAMES-LST-LST1 ACL2_*1*_COMMON-LISP::APPLY
         ACL2::FIND-RUNED-LEMMA ACL2::STORE-SUPER-DEFUN-WARTS-STOBJS-IN
         ACL2::SET-PRINT-READABLY ACL2::MEMBER-COMPLEMENT-TERM1
         ACL2::INSTRUCTIONS-OF-STATE-STACK ACL2::COROLLARY
         ACL2::COLLECT-REDEFINED ACL2::DEFAULT-BACKCHAIN-LIMIT
         ACL2::FILTER-> ACL2::UNPRETTYIFY/ADD-HYPS-TO-PAIRS
         ACL2::TILDE-*-ASSUMNOTES-COLUMN-PHRASE
         ACL2::UNION-EQUAL-TO-END ACL2::UNMEASURED-VARIABLES3
         ACL2::PUTPROP-PRIMITIVE-RECURSIVE-DEFUNP-LST
         ACL2::UNTRANSLATE-OR ACL2::RESTORE-HINT-SETTINGS-IN-PSPV
         ACL2::CURRENT-THEORY-FN ACL2::TAUTOLOGYP
         ACL2::MARK-LOCAL-INCLUDED-BOOKS ACL2::POSITIVE-LOWER-BOUNDP
         ACL2::MAKE-INITIAL-MEMOIZE-PONS-TABLE
         ACL2::EXPANSION-ALIST-PKG-NAMES ACL2::ROTATE-KILL-RING1
         ACL2::RASSOC-EQL-EXEC$GUARD-CHECK
         ACL2::PRINT-CERTIFY-BOOK-STEP-5 ACL2::COMPRESS2
         ACL2::SHOW-TTAG-NOTES1 ACL2::FORMALS ACL2::FRUNIC-MAPPING-PAIR
         ACL2::THEORY-NAMEP ACL2::REBUILD-EXPANSION ACL2::BINARY-PAND
         ACL2::CONDITIONALLY-MEMOIZED-FNS
         ACL2::REPLACE-DUPLICATE-VARS-WITH-ANONYMOUS-VAR-1-LST
         ACL2::DUMB-TYPE-ALIST-IMPLICATIONP2
         ACL2::ENCAPSULATE-FIX-KNOWN-PACKAGE-ALIST
         ACL2::UNION-COLLECT-NON-X ACL2::CONS-TAG-TREES-RW-CACHE
         ACL2_*1*_COMMON-LISP::< ACL2::IMMEDIATE-FORCEP
         ACL2::DISJOIN-CLAUSE-SEGMENT-TO-CLAUSE-SET
         ACL2::LOGICALLY-EQUIVALENT-STATES ACL2::DEFSTUB-IGNORES
         ACL2::THE-FN ACL2::CONSTANT-CONTROLLER-POCKETP1
         ACL2::COLLECT-RUNE-TRIGGER-PAIRS-FROM-FC-ACTIVATIONS
         ACL2::SET-GC-STRATEGY-FN ACL2::SET-TERM-EVISC-TUPLE-STATE
         ACL2::SUBSETP-EQL-EXEC$GUARD-CHECK ACL2::RASSOC-EQL-EXEC
         ACL2::DELETE-ASSOC-EQ-EXEC ACL2::PUTPROP-COARSENINGS
         ACL2::ENABLED-ARITH-NUMEP ACL2::RESTORE-RW-CACHE-STATE-IN-PSPV
         ACL2::EXT-ANC-ATTACHMENT-MISSING
         ACL2::UPDATE-LIST-ALL-PACKAGE-NAMES-LST
         ACL2::SET-FMT-HARD-RIGHT-MARGIN ACL2::CROSS-TESTS-AND-CALLS3
         ACL2::REMOVE-DUPLICATES-EQUAL-FROM-END
         ACL2::TESTS-AND-ALISTS-LST-FROM-FN ACL2::CHK-LIVE-STATE-P
         ACL2::PRINT-GAG-STATE1 ACL2::TAU-GET-ALL-SIG-FNS
         ACL2::PAIR-CONGRUENCE-RULES-WITH-COARSENINGS
         ACL2::EXPUNGE-FC-DERIVATIONS-LST ACL2::MEMOIZE-OFF-TRACE-ERROR
         ACL2::PEEK-CHAR$ ACL2::TILDE-@-POOL-NAME-PHRASE-LST
         ACL2::SYMBOL-PACKAGE-NAME-SET ACL2::SER-ENCODE-NATS
         ACL2::MERGE-CADR-< ACL2::SHOW-ACCUMULATED-PERSISTENCE-PHRASE0
         ACL2::CDRN ACL2::REMOVE-EQUAL ACL2::FIND-EVFN-LST-IN-CLAUSE
         ACL2::ADD-BOUNDER-TO-BOUNDERS ACL2::FFNNAMES-SUBSETP-LISTP
         ACL2::CONS-TAG-TREES-RW-CACHE-FIRST ACL2::REV-UNION-EQUAL
         ACL2::RESTRICT-EXPANSION-ALIST ACL2::NO-RUNE-BASED-ON
         ACL2::IPRINT-AR-AREF1 ACL2::PAIR-CL-ID-WITH-HINT-SETTING
         ACL2::ADD-TO-SET-EQUAL
         ACL2::ALREADY-USED-BY-FIND-EQUATIONAL-POLYP-LST
         ACL2::FREE-VARSP ACL2::PRINT-COMMANDS ACL2::TAU-SUBINTERVALP
         ACL2::REPLACE-STOBJS1 ACL2::SIBLINGS
         ACL2::SOME-ELEMENT-DUMB-OCCUR-LST ACL2::OPEN-TRACE-FILE-FN
         ACL2::MUTUALLY-EXCLUSIVE-TESTS ACL2::RASSOC-EQ-AS-CAR
         ACL2::FARGN1 ACL2::ENUMERATE-ELEMENTS ACL2::BINARY-LOGEQV
         ACL2::COLLECT-WHEN-FFNNAMESP ACL2::STOBJS-IN-MATCHP
         ACL2::FERTILIZE-COMPLEXITY ACL2::FORBIDDEN-FNS-IN-TERM
         ACL2::LD-PRINT-RESULTS ACL2::INCLUDE-BOOK-ALIST-SUBSETP
         ACL2::CONS-TERM1 ACL2::CLAUSE-DIFFICULTY ACL2::MAKE-RUNES
         ACL2::DISJOIN-CLAUSES ACL2::RESTRICT-ALIST-TO-ALL-VARS
         ACL2::SHARP-ATSIGN-ALIST ACL2::SYS-CALL
         ACL2::SET-DIFFERENCE-CURRENT-THEORY-FN ACL2::BOUNDER-ARGS
         ACL2::INTERSECTION-EQL-EXEC ACL2::FILENAME-TO-SYSFILE
         ACL2::MAKE-RECORD-CAR-CDRS1 ACL2::NORMALIZE-CHAR
         ACL2::ALL-DUMB-OCCUR-LST ACL2::NO-AUGMENTED-RUNE-BASED-ON
         ACL2::EXTRA-INFO ACL2::VIRGINP ACL2::FIND-MAPPING-PAIRS-TAIL1
         ACL2::RULER-EXTENDERS-LST ACL2::EVALUATOR-CLAUSE
         ACL2::ASSOC-EQ-BUTLAST-2 ACL2::SUBSETP-EQUAL/SMALLER
         ACL2::DUMB-OCCUR-VAR-LST ACL2::MAKE-NEW-GOALS-FROM-ASSUMPTIONS
         ACL2::REMOVE1-EQL-EXEC ACL2::TTAG-ALISTP
         ACL2::HL-CHECK-ALIST-FOR-SERIALIZE-RESTORE
         ACL2::SHOW-ACCUMULATED-PERSISTENCE-REMOVE-USELESS
         ACL2::XD-NAME ACL2::SORT->-ABSOLUTE-EVENT-NUMBER
         ACL2::BIG-M-LITTLE-M-NAME ACL2::BINARY-POR
         ACL2::NON-TRIVIAL-STOBJ-BINDING
         ACL2::CHK-EMBEDDED-EVENT-FORM-ORIG-FORM-MSG ACL2::MAX-LEVEL-NO
         ACL2::MERGE-USING-DOT-DOT ACL2::DISJOIN-CLAUSES1
         ACL2::REPLACE-GOAL-SPEC-IN-NAME-TREE ACL2::ALPHORDER
         ACL2::IRRECONCILABLE-ALISTSP ACL2::TRACE$-WHEN-GCOND
         ACL2::ALWAYS-BIGGERP ACL2::ADD-TEST-SMART
         ACL2::BIG-M-LITTLE-M-EVENT ACL2_*1*_COMMON-LISP::CONS
         ACL2::DEREF-MACRO-NAME ACL2::ACL2-UNWIND ACL2::POLYS-WITH-VAR
         ACL2::MAYBE-UNTRACE$-FN ACL2::ADD-TO-SET-EQ-EXEC
         ACL2::RESET-LD-SPECIALS-FN ACL2::CURRENT-ALL-DEPS
         ACL2::MEMBER-EQ-ALL ACL2::MAKE-RECORD-EXPANSION
         ACL2::GET-EVENT-DATA ACL2::STRIP-DCLS
         ACL2::GET-COEFF-FOR-CANCEL1 ACL2::CASE-TEST
         ACL2::SOME-ELEMENT-MEMBER-COMPLEMENT-TERM ACL2::SET-W!
         ACL2::SET-LD-EVISC-TUPLE-STATE ACL2::CERT-ANNOTATIONSP
         ACL2::REMOVE1-EQL-EXEC$GUARD-CHECK ACL2::MEMBER-NEG-EVGS1
         ACL2::REC-FNNAMES ACL2::STOBJ-RECOGNIZER-TERMS
         ACL2::TAU-BIG-SWITCH-EQUATIONP ACL2::BOUND-VARS-LST
         ACL2::SET-SERIALIZE-CHARACTER ACL2::DEFSTOBJ-DEFCONSTS
         ACL2::SET-ABBREV-EVISC-TUPLE-STATE ACL2::ASSOC-EQ-TRACE-ALIST
         ACL2_*1*_ACL2::BINARY-+
         ACL2::COLLECT-DISAGREEING-ARITY-ASSUMPTIONS ACL2::INTRO-UDF
         ACL2::CONVERT-NAME-TREE-TO-NEW-NAME ACL2::GET-CLIQUE
         ACL2::REMOVE-ONE-+- ACL2::ASSOC-EQL-EXEC$GUARD-CHECK
         ACL2::MAKE-LET-OR-LET* ACL2::ALL-PROGRAMP ACL2::ALL-VARS-BAG
         ACL2::KEYWORD-PARAM-VALUEP ACL2::TRANSLATE-UNBOUND
         ACL2::SET-PRINT-PRETTY
         ACL2::ANTAGONISTIC-TESTS-AND-ALISTS-LSTP ACL2::INDUCT-VARS1
         ACL2::CDR-NEST ACL2::TRANSLATE-GENERALIZE-ALIST-2
         ACL2::SAME-GOAL ACL2::INTERSECTION-EQ-EXEC
         ACL2::CONGRUENT-STOBJ-REP ACL2::IFF
         ACL2::SUBSETP-EQUAL-MOD-EXTRA-INFO-LITS ACL2::TAU-PAIR-MEMBER1
         ACL2::POLY-MEMBER ACL2::UPDATE-HINT-SETTINGS
         ACL2::BACKCHAIN-LIMIT-REACHEDP ACL2::LET-MBE-GUARD-FORM
         ACL2::HELPFUL-LITTLE-ECNT-MSG ACL2::TRANSLATE-ABBREV-RUNE
         ACL2::HL-RESTORE-FAL-FOR-SERIALIZE ACL2::SAVED-OUTPUT-TOKEN-P
         ACL2::RECORD-ERROR ACL2::CLTL-DEF-FROM-NAME
         ACL2::ADD-TO-SET-EQL-EXEC ACL2::UNION-EQUAL
         ACL2::STOBJ-PRINT-SYMBOL ACL2::SET-TEMP-TOUCHABLE-FNS
         ACL2::TYPED-IO-LISTP ACL2::ACCESSOR-ARRAY ACL2::REPLACE-STOBJS
         ACL2::SET-MEMO-TABLE-EVENTS ACL2::ATTACHMENT-ALIST
         ACL2::GENEQV-REFINEMENTP1 ACL2::DROP-FROM-END
         ACL2::PRINT-RULES-AND-HINT-EVENTS-SUMMARY
         ACL2::MCONS-TERM-SMART ACL2::ASSOC-EQUAL
         ACL2::SUPPLY-NAME-FOR-PROVED-FUNCTIONAL-INSTANCES-ALIST-ENTRY
         ACL2::MERGE-CANDIDATES ACL2::PRINT-STEPS-SUMMARY
         ACL2::GET-SUBVERSIVES ACL2::STOBJS-OUT
         ACL2::MAKE-PEQUIV-PATTERN
         ACL2::INTERSECTP-EQL-EXEC$GUARD-CHECK
         ACL2::TERM-ALISTP-FAILURE-MSG ACL2::SET-PRINT-RADIX
         ACL2::MAKUNBOUND-GLOBAL ACL2::MAKE-IDENTITY-INTERVAL
         ACL2::OR-SUBSET-TREES ACL2_*1*_ACL2::BAD-ATOM<=
         ACL2::GUESS-EVFN-LST-FOR-EVFN ACL2::SIMPLIFIABLE-MV-NTHP
         ACL2::ASSOC-EQUAL-CDR ACL2::RETURN-LAST-LOOKUP
         ACL2::ATTACHMENT-CLTL-CMD
         ACL2::COLLECT-NON-COMMON-LISP-COMPLIANTS
         ACL2::DEFINED-CONSTANT ACL2::PUTPROP-LEVEL-NO-LST
         ACL2::SET-PRINT-LINES
         ACL2::PRINT-ENCAPSULATE-MSG3/EXPORTED-NAMES
         ACL2::INTERSECTION-EQL-EXEC$GUARD-CHECK ACL2::SET-GAG-MODE-FN
         ACL2::STORE-CLAUSE ACL2::F-PUT-LD-SPECIALS
         ACL2::SET-STANDARD-CO-STATE ACL2::DEFCONST-VAL-RAW
         ACL2::PROPER-DUMB-OCCUR-AS-OUTPUT ACL2::FIX-STOBJ-ARRAY-TYPE
         ACL2::QUICK-AND-DIRTY-SUBSUMPTION-REPLACEMENT-STEP
         ACL2::COLLECT-BAD-FN-ARITY-PAIRS ACL2::TILDE-*-ELIM-PHRASE
         ACL2::SYSFILE-TO-FILENAME-CERT-ANNOTATIONS
         ACL2::UPDATE-WORLD-INDEX ACL2::DEF-BASIC-TYPE-SETS1
         ACL2::MEMBER-SYMBOL-NAME ACL2::INSERT-ARITH-TERM-ORDER
         ACL2::ILLEGAL-STOBJ-LET-MSG ACL2::REMOVE1-EQUAL ACL2::XOR
         ACL2::LOOKUP-BRR-STACK ACL2::FREE-VARS-IN-HYPS-SIMPLE
         ACL2::TILDE-@-BOOK-STACK-MSG ACL2::FREE-VAR-RUNES
         ACL2::SOME-CONGRUENCE-RULE-SAME ACL2::COMPATIBLE-ARITY-ALISTSP
         ACL2::ILLEGAL-FNP-LIST ACL2::HL-FALTABLE-REMOVE ACL2::ARITY
         ACL2::THE-FN-FOR-*1* ACL2::COMPUTED-HINT-TUPLE-LISTP
         ACL2::TILDE-*-ELIM-PHRASE/ALIST ACL2::GET-TIMER
         ACL2::WALKABOUT=-FN ACL2::INITIALIZE-TAU-PREDS
         ACL2::TRANSLATE-DCL-LST ACL2::TOO-MANY-IFS-PRE-REWRITE-BUILTIN
         ACL2::ILLEGAL-FNP ACL2::CW-GSTACK-FN
         ACL2::NORMALIZE-LINEAR-SUM-P ACL2::DEFCONST-NAME-ALIST
         ACL2::TS-BUILDER-MACRO ACL2::UPDATE-CBD
         ACL2::MEMBER-EQL-EXEC$GUARD-CHECK ACL2::SUBSETP-EQ-EXEC
         ACL2::BOOL-FLG ACL2::TILDE-@-HYP-PHRASE
         ACL2::MONITORABLE-RUNES-FROM-MAPPING-PAIRS
         ACL2::ALL-ARGS-OCCUR-AFTER-STRIP-NOT ACL2::EXTEND-WORLD1
         ACL2::SET-CL-IDS-OF-ASSUMPTIONS1 ACL2::SER-ENCODE-STRS
         ACL2::HL-HSPACE-MAKE-FAST-ALIST
         ACL2::DUPLICITOUS-REVAPPEND-CAR ACL2::CLEANSE-TYPE-ALIST
         ACL2::RETRACT-WORLD1 ACL2::REMOVE-TRIVIAL-CLAUSES
         ACL2::LOOKUP-BDDNOTE ACL2::SET-ATTACHMENT-SYMBOL-FORM
         ACL2::ZIP-VARIABLE-TYPE-ALIST ACL2::WEAK-CONS-OCCUR
         ACL2::FORMALIZED-VARLISTP ACL2::ADD-SUFFIX
         ACL2::IO?-WORMHOLE-BINDINGS ACL2::CONGRUENT-STOBJ-FIELDS
         ACL2::SUM-LEVEL-NOS
         ACL2::DUMB-KEEP-ASSUMPTIONS-WITH-WEAKEST-TYPE-ALISTS
         ACL2::DEFABSSTOBJ-RAW-INIT ACL2::MERGE-INTO-EXPANSION-ALIST
         ACL2::DUMB-OCCUR-VAR
         ACL2::SUBST-NIL-INTO-TYPE-PRESCRIPTION-DISJUNCT
         ACL2::COLLECT-KEYS-EQ ACL2::GET-EVENT
         ACL2::DELETE-ASSOC-EQUAL?-LST
         ACL2::ADD-TO-SET-EQL-EXEC$GUARD-CHECK ACL2::BINARY-*
         ACL2::NO-ELEMENT-ALWAYS-BIGGERP ACL2::SET-DIFFERENCE-EQUAL
         ACL2::HIDDEN-DEFPKG-EVENTS-SIMPLE ACL2::TAKE
         ACL2::SUBSETP-EQ-EXEC$GUARD-CHECK ACL2::WORMHOLE-ER
         ACL2::FCOMPLEMENTARY-MULTIPLEP1 ACL2::MAKE-CONTROLLER-ALIST1
         ACL2::ACL2X-ALISTP-DOMAINS-SUBSETP ACL2::ARITIES-OKP
         ACL2::REWRITE-CLAUSE-ACTION ACL2::FIND-CLAUSES
         ACL2::CD-FORM-MATCHP ACL2::SET-GAG-MODE-EVISC-TUPLE-STATE
         ACL2::DEFABSSTOBJ-RAW-DEFS ACL2::BACKCHAIN-LIMIT
         ACL2::UNKNOWN-PKG-ERROR-MSG ACL2::IN-TAU-INTERVALP
         ACL2::CST=-LST ACL2::MAP-MULTIPLY-CAR
         ACL2::IDENTITY-WITH-STATE ACL2::MAKE-IMPLICATION
         ACL2::FMT-CONTROL-BINDINGS1 ACL2::SMART-MEMBER-EQUAL-+-
         ACL2::COLLECT-PROGRAMS ACL2::FIND-FN-IN-CLAUSE
         ACL2::FIND-POSSIBLE-PUT ACL2::COMPUTE-VETOES
         ACL2::PRINT-UNPROVED-GOALS-MESSAGE ACL2::COLLECT-OLD-NAMEPS
         ACL2::ALL-VARS1-LST ACL2::UPDATE-OPEN-OUTPUT-CHANNELS
         ACL2::HL-HSPACE-NUMBER-SUBTREES-AUX ACL2::POP-ACCP
         ACL2::DUMB-OCCUR ACL2::SURROUNDING-FNS ACL2::COLLECT-PARENTS1
         ACL2::ALL-FUNCTION-SYMBOLPS
         ACL2::PRIMORDIAL-EVENT-MACRO-AND-FN ACL2::REDEFINED-NAMES1
         ACL2::SET-WORMHOLE-ENTRY-CODE
         ACL2::MAKE-RECORD-CHANGER-LET-BINDINGS ACL2::RUNIC-THEORY
         ACL2::CONVERT-BOOK-NAME-TO-CERT-NAME ACL2::ALL-BOUNDP
         ACL2::HL-HSPACE-HONS-CLEAR ACL2::TREE-OCCUR-EQ
         ACL2::PRODUCT-ALREADY-TRIEDP ACL2::TO-BE-IGNOREDP1
         ACL2::TILDE-@-POOL-NAME-PHRASE ACL2::GEN-NEW-NAME
         ACL2::CAR-CADR-CADDR-ETC ACL2::EVISC-INDEXED-INSTRS-1
         ACL2::GET-SKIPPED-PROOFS-P ACL2::IF-INTERP-ASSUMED-VALUE-X
         ACL2::RUN-INSTR-ON-GOALS-GUTS ACL2::SUBLIS-FN-LST-SIMPLE
         ACL2::UNION-CURRENT-THEORY-FN ACL2::POLY-EQUAL
         ACL2::PUFFABLE-COMMAND-BLOCKP ACL2::PUTPROP-TAU-PAIR
         ACL2::PRETTYIFY-CLAUSE2
         ACL2::RECOMPRESS-GLOBAL-ENABLED-STRUCTURE
         ACL2::SER-ENCODE-RATS ACL2::INTERSECTION1-EQ
         ACL2::EVISCERATION-STOBJ-MARK
         ACL2::TILDE-*-RAW-PREPROCESS-PHRASE ACL2::LOGICAL-NAMEP
         ACL2::TO-BE-IGNOREDP ACL2::OUR-DIGIT-CHAR-P ACL2::CASE-LENGTH
         ACL2::GLOBAL-SET-LST ACL2::ENABLED-NUMEP
         ACL2::CANONICAL-ANCESTORS-LST ACL2::EVALUATOR-CLAUSES1
         ACL2::ABSORB-FRAME ACL2::PRINT-ALL-CONCS
         ACL2::MEMOIZE-EVAL-COMPILE ACL2::HITP-LST
         ACL2::SET-PPR-FLAT-RIGHT-MARGIN ACL2::SCAN-TO-INCLUDE-BOOK
         ACL2::MEMBER-EQUAL ACL2::DUPLICITOUS-CONS-CAR
         ACL2_*1*_ACL2::MV-LIST ACL2::PROGRAM-TERMP
         ACL2::DUPLICATE-KEYS-ACTION
         ACL2::SHOW-ACCUMULATED-PERSISTENCE-PHRASE2-NOT-MERGE
         ACL2::PUTPROP-INITIAL-TYPE-PRESCRIPTIONS
         ACL2::ALL-RUNES-IN-TTREE ACL2::GOAL-TREE-WITH-CL-ID
         ACL2::CONVERT-CLAUSE-TO-ASSUMPTIONS
         ACL2::ATTACHMENT-RECORDS-FAL ACL2::PUSH-ACCP
         ACL2::FALSIFYING-ASSIGNMENT ACL2::UPDATE-WRITTEN-FILES
         ACL2::ATTACHED-FNS ACL2::AUGMENT-RUNIC-THEORY ACL2::LOGAND-LST
         ACL2::REPLACE-VARS-BY-BINDINGS
         ACL2::DELETE-ASSOC-EQL-EXEC$GUARD-CHECK ACL2::HL-NAT-COMBINE*
         ACL2::ACTIVE-BOOK-NAME ACL2::SET-DEBUGGER-ENABLE-FN
         ACL2::MERGE-ALPHA-< ACL2::FUNCTION-SYMBOLP ACL2::RENEW-LEMMAS
         ACL2::REMOVE-EQ-EXEC$GUARD-CHECK ACL2::ACL2-SYSTEM-NAMEP
         ACL2::HL-FALTABLE-EJECT ACL2::FFNNAMESP-EQ-LST
         ACL2::MAKE-VAR-LST ACL2::POLY-ALIST-EQUAL ACL2::MERGE-CAR->
         ACL2::GET-TYPE-DECLS ACL2::INTERSECTP-EQ-EXEC
         ACL2::DEFSTOBJ-FUNCTIONSP ACL2::REVERSE-STRIP-CDRS
         ACL2::SWEEP-CLAUSES1 ACL2::MARK-MISSING-AS-HIDDEN-P
         ACL2::PUT-CL-ID-OF-CUSTOM-KEYWORD-HINT-IN-COMPUTED-HINT-FORM
         ACL2::COLLECT-WORLD-GLOBALS ACL2::BIG-C-LITTLE-C-EVENT
         ACL2::BOOKDATA-ALIST ACL2::RECOMPRESS-STOBJ-ACCESSOR-ARRAYS
         ACL2::FORBIDDEN-FNS-IN-TERM-LIST ACL2::INTERSECTION-DOMAINS
         ACL2::FIND-LONGEST-COMMON-RETRACTION1
         ACL2::RECOVER-FORCED-RUNES1 ACL2::RASSOC-EQUAL
         ACL2::ALIST-DIFFERENCE-EQ ACL2::DELETE-ASSOC-EQ-ASSOC-EQ
         ACL2::TAU-MV-NTH-SYNONYM-FORMP ACL2::RELEVANT-POSNS-LAMBDAS
         ACL2::HL-HSPACE-TRULY-STATIC-HONSP ACL2::LENGTH-EXCEEDSP
         ACL2::MACRO-ARGLIST-KEYSP ACL2::HL-HSPACE-NORM-EXPENSIVE
         ACL2::INCLUDE-BOOK-DIR-ALISTP ACL2::ALIST-TO-KEYWORD-ALIST
         ACL2::UPDATE-WRLD-STRUCTURES ACL2::PRINT-CERTIFY-BOOK-STEP-3
         ACL2::NON-MEMOIZABLE-STOBJS ACL2::MATCH-CLAUSE-LIST
         ACL2::UNION-EQ1-REV ACL2::LOOP-STOPPER ACL2::COLLECT-EXT-ANC
         ACL2::SATISFYING-FC-DERIVATIONP ACL2::WELL-FORMED-TYPE-DECLS-P
         ACL2::INTERSECTION-EQ-EXEC$GUARD-CHECK
         ACL2::SYSFILE-TO-FILENAME ACL2::STOBJ-CREATORP
         ACL2::WORLD-EVISCERATION-ALIST ACL2::GET-BRR-LOCAL
         ACL2::DUMB-ASSUMPTION-SUBSUMPTION1
         ACL2::UNARY-FUNCTION-SYMBOL-LISTP
         ACL2::FILENAME-TO-SYSFILE-CERT-ANNOTATIONS
         ACL2::PUT-ASSOC-EQ-ALIST ACL2::SHOW-POLY2
         ACL2::HONS-UNION-ORDERED-STRING-LISTS ACL2::ALL-VARS1
         ACL2::COMPLEMENTARYP ACL2::FFNNAMESP ACL2::VARIFY!-LST1
         ACL2::LINKED-VARIABLES ACL2::BACKCHAIN-LIMIT-REACHEDP1
         ACL2::FFNNAMESP-LST ACL2::FFNNAMEP-LST
         ACL2::FIND-NONTRIVIAL-RULERS ACL2::NORMALIZE-LINEAR-SUM-P1
         ACL2::BDD-CONSTRUCTOR-TRM-P ACL2::VAR-IN-POT-LST-P
         ACL2::TAU-GET-ALL-PREDS ACL2::UNKNOWN-CONSTRAINT-SUPPORTERS
         ACL2::BOUND-VARS ACL2::CONS-TERM-BINARY-+-CONSTANT
         ACL2::HL-FALTABLE-GENERAL-LOOKUP
         ACL2::ADD-TYPE-ALIST-RUNES-TO-TTREE ACL2::INTERSECTP-EQL-EXEC
         ACL2::CONVERT-THEORY-TO-UNORDERED-MAPPING-PAIRS
         ACL2::QUICK-AND-DIRTY-SUBSUMPTION-REPLACEMENT-STEP1
         ACL2::PUT-DEFSTOBJ-INVARIANT-RISK
         ACL2::NEW-DEPENDENT-CLAUSE-PROCESSORS ACL2::DISJOIN2
         ACL2::DELETE-ASSOC-EQUAL? ACL2::FILTER-GENEQV
         ACL2::LD-FN-ALIST ACL2::PRINT-ALL-GOALS
         ACL2::CLEAR-MEMO-TABLE-EVENTS ACL2::DEFABSSTOBJ-AXIOMATIC-DEFS
         ACL2::UNION-VALUES ACL2::COLLECT-CDRS-WHEN-CAR-EQ
         ACL2::ONCEP-TP-BUILTIN
         ACL2::FILENAME-TO-SYSFILE-INCLUDE-BOOK-ENTRY
         ACL2::ENCAPSULATE-CTX ACL2::DMR-INTERP-FRESH-REWRITE-P
         ACL2::ATTACHMENT-RECORD-PAIRS
         ACL2::FIND-LONGEST-COMMON-RETRACTION1-EVENT
         ACL2::EV-LST-FROM-EV ACL2::MF-SHORTEN ACL2::CLEAN-BRR-STACK
         ACL2::EQUIVALENCE-RUNE1 ACL2::TRANSLATE-DEREF
         ACL2::ILLEGAL-RULER-EXTENDERS-VALUES ACL2::TERM-EVISC-TUPLE
         ACL2::PRETTYIFY-FC-DERIVATION ACL2::MAX-LEVEL-NO-LST
         ACL2::GUARD-RAW ACL2::CONTROLLER-VARIABLES
         ACL2::RECORD-ACCESSOR-FUNCTION-NAME ACL2::VECTOR-TS-UNION
         ACL2::SET-DIFFERENCE-ASSOC-EQ ACL2::SATISFYING-FC-ACTIVATION1P
         ACL2::UNSAVE-FN ACL2::NEW-NAMEP
         ACL2::SUBST-NIL-INTO-TYPE-PRESCRIPTION-CONCL
         ACL2::MAKE-CONTROLLER-POCKET ACL2::EVGS-OR-T
         ACL2::ALL-VARS-BOUNDP ACL2::SORT-APPROVED ACL2::CONCRETE-STOBJ
         ACL2::CONVERT-BOOK-NAME-TO-COMPILED-NAME
         ACL2::EVAL-TAU-INTERVAL ACL2::MAX-WIDTH ACL2::SUBLIS-FN-SIMPLE
         ACL2::FIRST-ASSOC-KEYWORD ACL2::TILDE-*-GEN-PHRASE/ALIST1
         ACL2::PRETTYIFY-CLAUSE1 ACL2::SKIP-META-TERMP-CHECKS
         ACL2::EXPLODE-ATOM ACL2::FIND-RUNED-TYPE-PRESCRIPTION
         ACL2::CROSS-PROD1 ACL2::UNION-EQ-EXEC$GUARD-CHECK
         ACL2::EXPAND-ANY-FINAL-IMPLIES ACL2::SUBSEQUENCEP
         ACL2::COMPUTE-VETOES2 ACL2::STUFF-STANDARD-OI
         ACL2::OUR-MERGE-PATHNAMES ACL2::MERGE-ACCUMULATED-PERSISTENCE
         ACL2::ALL-VARS-BAG-LST ACL2::ABBREVIATE ACL2::TERM-LIST-LISTP
         ACL2::EQUAL/UNION-EQUAL ACL2::LEXORDER ACL2::DEGREE-OF-MATCH
         ACL2::LOOP-STOPPER-VALUE-OF-VAR ACL2::MEMBER-COMPLEMENT-TERM
         ACL2::REPLACE-DUPLICATE-VARS-WITH-ANONYMOUS-VAR-1
         ACL2::SUBSUMED-CLAUSE-IDS-FROM-POP-HISTORY
         ACL2::SOME-SYMBOL-NAME-TREE-OCCUR
         ACL2::OPEN-INPUT-CHANNEL-ANY-P ACL2::PAIRLIS-X2
         ACL2::MAKE-SPACES-ARRAY-REC ACL2::INDUCTION-FORMULA
         ACL2::MACRO-ARGS ACL2::CONS-TAG-TREES
         ACL2::EVAL-EVENT-LST-ENVIRONMENT ACL2::RASSOC-EQ-EXEC
         ACL2::NOT-TO-BE-REWRITTENP1
         ACL2::CONJOIN-CLAUSE-SETS-EXTRA-INFO
         ACL2::REMOVE-TAG-FROM-TAG-TREE ACL2::RW-CACHE-EXIT-CONTEXT
         ACL2::RUNES-TO-CLASS-ALIST1 ACL2::STOBJ-EVISCERATION-ALIST
         ACL2::DEF-BODY-LEMMAS ACL2::SCAN-TO-DEFPKG
         ACL2::TAU-VISIT-FUNCTION-INTRODUCTION
         ACL2::SET-DIFFERENCE-EQL-EXEC$GUARD-CHECK
         ACL2::STRIP-KEYWORD-LIST ACL2::EXTEND-UNIFY-SUBST
         ACL2::TRACE-MULTIPLICITY ACL2::HL-HSPACE-NORM-ATOM
         ACL2::EXT-ANCESTORS-ATTACHMENTS ACL2::SELECT-X-CL-SET
         ACL2::HL-HSPACE-FAST-ALIST-LEN ACL2::POSITION-EQ-EXEC
         ACL2::GOVERNORS ACL2::IF-INTERP-ASSUMED-VALUE1
         ACL2::SUBLIS-VAR-LST-LST ACL2::FIX-TRACE-UNTRACE
         ACL2::CONJOIN-CLAUSE-TO-CLAUSE-SET ACL2::RULER-EXTENDERS-MSG
         ACL2::BUILD-PC-ENABLED-STRUCTURE-FROM-ENS
         ACL2::EXPANDED-NEW-VARS-IN-POT-LST
         ACL2::SUBLIS-EXPR-NON-QUOTEPS-LST ACL2::PSEUDO-VARIANTP
         ACL2::PRETTYIFY-FC-ACTIVATION
         ACL2::ABSOLUTE-TO-RELATIVE-COMMAND-NUMBER ACL2::TERM-LISTP
         ACL2::FETCH-TERM ACL2::HL-HSPACE-NORMEDP ACL2::DESTRUCTORS
         ACL2::SET-TRACE-EVISC-TUPLE ACL2::ALL-PICKS
         ACL2::INIT-IPRINT-AR ACL2::UPDATE-IDATES
         ACL2::PUT-BRR-LOCAL-LST ACL2::WORSE-THAN-BUILTIN
         ACL2::MEMBER-TERM ACL2::PRINT-RE-ENTERING-PROOF-CHECKER
         ACL2::WALKABOUT-IP ACL2::EVERY-CONCL-MEMBER-EQUALP
         ACL2::GET-STOBJ-CREATOR ACL2::NOTE-FNS-IN-FORM
         ACL2::OBVIOUSLY-IFF-EQUIV-TERMS ACL2::ACCEPTABLE-TAU-RULES
         ACL2::TILDE-*-MEASURE-PHRASE1 ACL2::UNMEASURED-VARIABLES1
         ACL2::GC-VERBOSE-FN ACL2::SET-PRINT-CIRCLE
         ACL2::SPONTANEOUS-DECERTIFICATIONP ACL2::INTERSECTP-EQUAL
         ACL2::CHECK-ACL2-WORLD-INVARIANT ACL2::CLOSE-TRACE-FILE-FN
         ACL2::FAST-ALIST-FORK ACL2::HL-MAKE-FAST-ALIST-PUT-PAIRS
         ACL2::ALL-DIGITS-P ACL2::SER-HASHTABLE-INIT
         ACL2::RIGHT-ASSOCIATED-ARGS ACL2::BINARY-LOGXOR
         ACL2::WORSE-THAN-OR-EQUAL-BUILTIN ACL2::PARSE-INFIX-FILE
         ACL2::CONSTANT-CONTROLLER-POCKETP
         ACL2::SET-FMT-SOFT-RIGHT-MARGIN ACL2::IF-INTERP-ASSUMED-VALUE3
         ACL2::NON-TAUTOLOGICAL-CLASSES ACL2::FFNNAMESP-EQ
         ACL2::ENTER-BOOT-STRAP-MODE ACL2::RUNE-<
         ACL2::RELEVANT-POSNS-MERGE ACL2::PRETTYIFY-FC-ACTIVATIONS
         ACL2::SEQUENTIAL-SUBST-VAR-TERM ACL2::CONS-ALL-TO-LST
         ACL2::SET-PRINT-RIGHT-MARGIN ACL2::FIND-LIKELY-NEAR-MISSES
         ACL2::MEMBER-EQ-EXEC ACL2::SYMBOL-< ACL2::ALL->=-LEN
         ACL2::CHK-MAKE-ARRAY$ ACL2::INCREMENT-TIMER
         ACL2::RELATIVIZE-BOOK-PATH
         ACL2::ADD-TO-SET-EQ-EXEC$GUARD-CHECK ACL2::THEORYP
         ACL2::CD-SOME-EVENT-MATCHP ACL2::INDUCTION-FORMULA-SIZE
         ACL2::MERGE-ACCUMULATED-PERSISTENCE-REC
         ACL2::REMOVE-ONE-COMPLEMENT ACL2::MAKE-UDF-INSIGS
         ACL2::CONJOIN-CLAUSE-TO-CLAUSE-SET-EXTRA-INFO
         ACL2::HL-HSPACE-NORM ACL2::MV-NTH ACL2::SUBLIS-TESTS-REV
         ACL2::FFNNAMEP ACL2::DELETE-ASSOC-EQ-LST ACL2::AND-ORP
         ACL2::KNOWN-ASSUMPTIONS ACL2::PRIMITIVE-INSTRUCTIONP
         ACL2::POSITION-EQL-EXEC ACL2::ALL-NILS-OR-X ACL2::LISTLIS
         ACL2::UPDATE-ACL2-ORACLE ACL2::UNSIGNED-BYTE-P
         ACL2::UPDATE-GLOBAL-TABLE ACL2::POSITION-EQ-EXEC$GUARD-CHECK
         ACL2::TAU-PAIR-MEMBER ACL2::CHK-MACRO-ARGLIST-KEYS
         ACL2::ATTACHMENT-PAIR ACL2::PACKN-POS ACL2::CHECK-PRINT-BASE
         ACL2::DEFUND-NAME-LIST
         ACL2::REMOVE-IRRELEVANT-LOOP-STOPPER-PAIRS
         ACL2::TYPE-PRESCRIPTION-CONCLP
         ACL2::REMOVE-SMALLER-KEYS-FROM-SORTED-ALIST
         ACL2::ASSOC-KEYWORD ACL2::DESTRUCTIVE-POP-ASSOC
         ACL2::POWER-EVAL ACL2::OBSERVE-RAW-MODE-SETTING
         ACL2::CHK-PACKAGE-REINCARNATION-IMPORT-RESTRICTIONS2
         ACL2::EQUAL-X-CONS-X-YP ACL2::SOME-CDR-EQUALP
         ACL2::CONGRUENCE-RULE-LISTP ACL2::STRIP-DCLS1
         ACL2::MAKE-FMT-BINDINGS ACL2::SET-PORT-FILE-ENABLED
         ACL2::IRRELEVANT-LOOP-STOPPER-PAIRS ACL2::SIGNED-BYTE-P
         ACL2::THROW-NONEXEC-ERROR ACL2::EXTRA-RULES-FOR-BDDS
         ACL2::UNION-EQL-EXEC$GUARD-CHECK
         ACL2::CONJOIN2-UNTRANSLATED-TERMS ACL2::DECODE-TAU-LST
         ACL2::ALL-FFN-SYMBS ACL2::FIND-DOT-DOT
         ACL2::SIBLING-ATTACHMENTS ACL2::PRINT-CURRENT-IDATE
         ACL2::FMT-DOC-EXAMPLE1
         ACL2::CHK-PACKAGE-REINCARNATION-IMPORT-RESTRICTIONS
         ACL2::REMOVE-STOBJS-IN-BY-POSITION
         ACL2::FORBIDDEN-FNS-IN-TERM-LIST-LIST ACL2::MEASURE-ALIST?
         ACL2::TYPE-PRESCRIPTION-DISJUNCTP ACL2::ALPHA-<
         ACL2::REVERSE-STRIP-CARS ACL2::IGNORE-POLYP
         ACL2::DELETE-ASSOC-EQ-EXEC$GUARD-CHECK
         ACL2::UNMEASURED-VARIABLES ACL2::CHECK-NULL-OR-NATP
         ACL2::INTRO-UDF-LST1 ACL2::SYMBOL-NAME-EQUAL
         ACL2::ALL-RUNES-IN-ELIM-SEQUENCE-LST
         ACL2::IPRINT-AR-ILLEGAL-INDEX ACL2::*1*DEFP
         ACL2::ALL-FFN-SYMBS-LST ACL2::IF-INTERP-ASSUMED-VALUE4
         ACL2::FETCH-DCL-FIELDS ACL2::CONS-TERM
         ACL2::ACCUMULATE-POST-ALIST ACL2::PSEUDO-VARIANTP-LIST
         ACL2::SET-DIFFERENCE-EQ-EXEC ACL2::NOT-IN-DOMAIN-EQ
         ACL2::SET-PRINT-BASE-RADIX ACL2::GUESS-FN-ARGS-LST-FOR-EVFN
         ACL2::FFNNAMEP-MOD-MBE ACL2::EXTRA-INFO-LITS)) 
(COMMON-LISP::PROCLAIM
    '(COMMON-LISP::FTYPE
         (COMMON-LISP::FUNCTION
             (COMMON-LISP::STRING COMMON-LISP::STRING) COMMON-LISP::T)
         ACL2::STRING-PREFIXP)) 
(COMMON-LISP::PROCLAIM
    '(COMMON-LISP::FTYPE
         (COMMON-LISP::FUNCTION (COMMON-LISP::T COMMON-LISP::FIXNUM)
             COMMON-LISP::FIXNUM)
         ACL2::LEN1 ACL2::MAX-FORM-COUNT-LST
         ACL2::CONS-COUNT-BOUNDED-AC)) 
(COMMON-LISP::PROCLAIM
    '(COMMON-LISP::FTYPE
         (COMMON-LISP::FUNCTION
             (COMMON-LISP::FIXNUM COMMON-LISP::FIXNUM) COMMON-LISP::T)
         ACL2::ALLOCATE-FIXNUM-RANGE)) 
(COMMON-LISP::PROCLAIM
    '(COMMON-LISP::FTYPE
         (COMMON-LISP::FUNCTION (COMMON-LISP::STRING)
             COMMON-LISP::FIXNUM)
         ACL2::FCHECKSUM-STRING)) 
(COMMON-LISP::PROCLAIM
    '(COMMON-LISP::FTYPE
         (COMMON-LISP::FUNCTION COMMON-LISP::NIL COMMON-LISP::FIXNUM)
         ACL2::SYNC-MEMOIZE-CALL-ARRAY ACL2::OUTSIDE-CALLER-COL-BASE)) 
(COMMON-LISP::PROCLAIM
    '(COMMON-LISP::FTYPE
         (COMMON-LISP::FUNCTION (COMMON-LISP::T COMMON-LISP::T)
             COMMON-LISP::*)
         ACL2::POP-CLAUSE1 ACL2-PC::GOALS ACL2-PC::=
         ACL2::SET-LD-PRE-EVAL-FILTER ACL2::TOO-MANY-IFS-PRE-REWRITE
         ACL2-PC::SEQUENCE-NO-RESTORE
         ACL2::SWEEP-GLOBAL-STATE-FOR-LISP-OBJECTS
         ACL2::CLOSE-OUTPUT-CHANNEL ACL2-PC::GENERALIZE
         ACL2::DECODE-CST-ALIST1 ACL2::PROPS-FN ACL2-PC::FORWARDCHAIN
         ACL2-PC::NX ACL2-PC::FINISH-ERROR ACL2-PC::SUCCEED ACL2-PC::AL
         ACL2-PC::PUT ACL2-PC::TYPE-ALIST ACL2-PC::ACL2-WRAP
         ACL2::CANCEL ACL2-PC::SLS ACL2::COLLECT-DCLS
         ACL2-PC::DROP-CONC ACL2::TRANS!-FN ACL2-PC::R ACL2::DOC-FN
         ACL2::FMT-DOC-EXAMPLE
         ACL2::PRINT-DEFUN-MSG/COLLECT-TYPE-PRESCRIPTIONS ACL2-PC::TH
         ACL2-PC::RUNES ACL2-PC::CL-PROC ACL2-PC::REPEAT-REC
         ACL2::SET-LD-PRE-EVAL-PRINT ACL2::SET-LD-SKIP-PROOFSP
         ACL2::SET-LD-QUERY-CONTROL-ALIST ACL2-PC::THEN
         ACL2-PC::RESTORE ACL2::SKIP-WHEN-LOGIC ACL2::BRR-PROMPT
         ACL2::PC-FN ACL2::CERTIFICATE-FILE ACL2-PC::S-PROP
         ACL2::TAU-BOUNDER-FORMP ACL2-PC::ADD-ABBREVIATION
         ACL2-PC::RUN-INSTR-ON-GOAL ACL2-PC::SAVE ACL2-PC::PSO!
         ACL2::SET-LD-MISSING-INPUT-OK ACL2::DEFATTACH-MERGE
         ACL2::VERIFY-TERMINATION-FN ACL2::DEFAULT-PRINT-PROMPT
         ACL2-PC::PR ACL2::COMBINE-FREE-FAILURE-ALISTS ACL2::PUFF-FN1
         ACL2::SET-WRITE-ACL2X ACL2-PC::SHOW-REWRITES ACL2::TRANS1-FN
         ACL2::WORSE-THAN-OR-EQUAL ACL2-PC::PSO ACL2-PC::USE
         ACL2::PROGN-FN ACL2::SER-ENCODE-RAT ACL2::EXTRACT-GOAL
         ACL2::HL-CACHE-GET ACL2::CHECK-&OPTIONAL-AND-&REST
         ACL2::DELETE-CONSECUTIVE-INTEGERS-UPWARD ACL2::GET-BRR-GLOBAL
         ACL2-PC::SHOW-TYPE-PRESCRIPTIONS ACL2::TRANSLATE-FC-CRITERIA
         ACL2-PC::EXPAND ACL2-PC::WRAP ACL2-PC::REWRITE ACL2::PCB!-FN
         ACL2::OUR-ABORT ACL2::ONCEP-TP ACL2::TOO-MANY-IFS-POST-REWRITE
         ACL2-PC::INDUCT ACL2::MAYBE-INSTALL-ACL2-DEFAULTS-TABLE
         ACL2::SET-LD-POST-EVAL-PRINT ACL2-PC::COMMANDS
         ACL2::MAKE-PC-ENS ACL2-PC::CONTRADICT ACL2-PC::WRAP1
         ACL2::DECODE-CST-LST ACL2::PR!-FN ACL2-PC::NIL ACL2-PC::DOC
         ACL2::SER-ENCODE-CONSES ACL2::COMBINE-RW-CACHE-LISTS
         ACL2-PC::PRO ACL2-PC::PROTECT ACL2-PC::REMOVE-ABBREVIATIONS
         ACL2::SET-DIFFERENCE-EQUAL-CHANGEDP ACL2-PC::DEMOTE
         ACL2-PC::BK ACL2-PC::HYPS ACL2::REGENERATE-TAU-DATABASE-FN
         ACL2::WORMHOLE-PROMPT ACL2::WALKABOUT ACL2::LD-FILTER-COMMAND
         ACL2::WORSE-THAN ACL2::SUBTERM-ONE-WAY-UNIFY-LST
         ACL2::PARTITION-REST-AND-KEYWORD-ARGS ACL2-PC::S
         ACL2::SET-STANDARD-CO ACL2-PC::DO-ALL ACL2::CHK-MEMO-QUOTEP
         ACL2-PC::ILLEGAL ACL2::CUSTOM-KEYWORD-HINT
         ACL2::SET-IPRINT-FN1 ACL2-PC::IF-NOT-PROVED ACL2-PC::PRINT
         ACL2-PC::WRAP-INDUCT ACL2-PC::PRINT-ALL-CONCS ACL2::READ-CHAR$
         ACL2::MERGE-LEXORDER-FAST ACL2::REMOVE-GUARD-HOLDERS1
         ACL2::CONSTRAINT-INFO ACL2::CHK-LEGAL-DEFSTOBJ-NAME
         ACL2::SUBLIS-VAR1 ACL2::SET-IPRINT-FN
         ACL2::DELETE-ASSUMPTIONS-1 ACL2::MAKE-REVERSED-AD-LIST
         ACL2::SPLIT-INITIAL-EXTRA-INFO-LITS ACL2::PUFF-FN
         ACL2-PC::GENEQV ACL2::SET-CHECK-INVARIANT-RISK-FN ACL2-PC::ST
         ACL2::SET-STANDARD-OI ACL2::PSTACK-FN ACL2-PC::COMM
         ACL2-PC::CLAIM ACL2::TRANS-FN
         ACL2::FIND-FIRST-CUSTOM-KEYWORD-HINT ACL2-PC::UNDO
         ACL2::TAU-INTERVAL-NEAR-SUBSETP ACL2-PC::PRINT-ALL-GOALS
         ACL2::LD-READ-KEYWORD-COMMAND ACL2::MAXIMAL-MULTIPLES
         ACL2::NQTHM-TO-ACL2-FN ACL2-PC::FAIL ACL2::SER-ENCODE-COMPLEX
         ACL2::READ-BYTE$ ACL2::EMPTY-ENCAPSULATE ACL2-PC::PP
         ACL2::PAIR-KEYWORDS ACL2-PC::SR ACL2-PC::TOP?
         ACL2::QUICK-AND-DIRTY-SRS ACL2-PC::IN-THEORY
         ACL2::SET-LD-ERROR-TRIPLES ACL2::IN-PACKAGE-FN ACL2-PC::NOISE
         ACL2::RECOVER-METAFUNCTION-OR-CLAUSE-PROCESSOR-SIGNATURES
         ACL2::PC-SINGLE-STEP-PRIMITIVE ACL2::OLD-CHECK-SUM-OBJ
         ACL2::ACCUMULATE-TTREE-IN-PC-STATE ACL2::NOTE-FNS-IN-FILE
         ACL2::CHECK-CARS-ARE-VARIABLES ACL2::CHK-ACCEPTABLE-LD-FN
         ACL2-PC::EQUIV ACL2-PC::CONTRAPOSE ACL2::COMBINE-RW-CACHES
         ACL2::SUBTERM-ONE-WAY-UNIFY ACL2::ELIDE-LOCALS-REC
         ACL2::META-EXTRACT-FORMULA ACL2::SUBLIS-VAR1-LST ACL2-PC::BDD
         ACL2::BRR-FN ACL2::GET-OUTPUT-STREAM-STRING$-FN
         ACL2::SET-LD-EVISC-TUPLE ACL2::ARGS-FN
         ACL2::INITIAL-STEP-LIMIT ACL2::DECODE-CST ACL2::GETENV!
         ACL2::SET-LD-ERROR-ACTION ACL2::HCOMP-BUILD-FROM-STATE-RAW
         ACL2-PC::UNSAVE ACL2-PC::FAIL-PRIMITIVE ACL2::OP-ALIST-INFO
         ACL2-PC::RETAIN ACL2-PC::DROP-LAST ACL2-PC::DROP
         ACL2::SET-GAG-MODE-EVISC-TUPLE ACL2::MERGE-RW-CACHES
         ACL2::SET-LD-REDEFINITION-ACTION ACL2-PC::DO-ALL-NO-PROMPT
         ACL2-PC::BOOKMARK ACL2::SET-PROOFS-CO
         ACL2::FIND-SUBSUMER-REPLACEMENT ACL2-PC::EX
         ACL2::CHECK-FOR-NO-OVERRIDE-HINTS ACL2::RW-CACHED-FAILURE-PAIR
         ACL2-PC::SKIP ACL2::READ-FILE ACL2::SET-ABBREV-EVISC-TUPLE
         ACL2-PC::REDUCE-BY-INDUCTION ACL2::ROTATE-KILL-RING
         ACL2::DELETE-CONSECUTIVE-INTEGERS-DOWNWARD
         ACL2::GET-COEFFICIENT ACL2::PR-FN ACL2-PC::CHECK-PROVED-GOAL
         ACL2::TILDE-*-SIMP-PHRASE1 ACL2::PC-MACROEXPAND ACL2::FIRST-IF
         ACL2::TERM-AND-TYP-TO-LOOKUP ACL2::PF-FN ACL2-PC::REPLAY
         ACL2-PC::CHANGE-GOAL ACL2::SIMPLIFIABLE-MV-NTH
         ACL2::POP-WARNING-FRAME ACL2::CHK-DECLARE ACL2::PE-FN
         ACL2::SPLIT-KEYWORD-ALIST
         ACL2::CERT-ANNOTATIONS-AND-CHECKSUM-FROM-CERT-FILE ACL2::PL-FN
         ACL2-PC::DO-STRICT ACL2-PC::SL ACL2-PC::TOP
         ACL2::ONE-WAY-UNIFY1-QUOTEP-SUBPROBLEMS
         ACL2::DELETE-ASSOC-EQ-ASSOC-EQ-1 ACL2::CHK-ABSSTOBJ-INVARIANTS
         ACL2::CHK-NO-DUPLICATE-DEFUNS-CMP ACL2::TRANSLATE-FC-CRITERION
         ACL2-PC::SHOW-ABBREVIATIONS ACL2::EXPANSION-ALIST-CONFLICT
         ACL2::LD-SIMPLE ACL2-PC::CG ACL2::READ-OBJECT
         ACL2-PC::SHOW-LINEARS ACL2::GETENV$
         ACL2::ACL2X-EXPANSION-ALIST
         ACL2::SET-CHECKPOINT-SUMMARY-LIMIT-FN
         ACL2::SET-DEFERRED-TTAG-NOTES ACL2::GET-WORMHOLE-STATUS
         ACL2::FILTER-POLYS ACL2::DCLS-GUARD-RAW-FROM-DEF
         ACL2::PC-SINGLE-STEP ACL2::REPLACE-GOAL-SPEC-IN-NAME-TREE1
         ACL2::COMMAND-BLOCK-NAMES ACL2::RETRIEVE-FN
         ACL2::SET-CURRENT-PACKAGE ACL2::WALKABOUT-NTH ACL2-PC::P
         ACL2::SET-FC-CRITERIA-FN ACL2-PC::SET-SUCCESS
         ACL2-PC::CONTRAPOSE-LAST ACL2-PC::PL ACL2::UNTRACE$-FN
         ACL2::ER-CMP-FN ACL2-PC::ELIM ACL2-PC::CLAUSE-PROCESSOR
         ACL2::STRIP-NON-REWRITTENP-ASSUMPTIONS1 ACL2-PC::NEGATE
         ACL2::REMOVE-META-EXTRACT-GLOBAL-HYPS ACL2-PC::PROVE
         ACL2-PC::COMMENT ACL2-PC::X-DUMB
         ACL2::RESTRICT-ALIST-TO-ALL-VARS1 ACL2::MSG-TO-CMP
         ACL2-PC::DIVE ACL2::GENERALIZING-RELATIONP ACL2-PC::PROMOTE
         ACL2::SPLIT-PSORTED-LIST1 ACL2::VERIFY-TERMINATION1
         ACL2-PC::EXIT ACL2-PC::SEQUENCE ACL2-PC::CHECK-PROVED
         ACL2::DEFATTACH-ERASE-COMPONENTS ACL2-PC::BASH
         ACL2::SET-LD-PROMPT ACL2::SET-LD-VERBOSE ACL2-PC::LEMMAS-USED
         ACL2::FIND-EQUATIONAL-POLY ACL2::PCB-FN
         ACL2-PC::RUN-INSTR-ON-NEW-GOALS ACL2-PC::LISP
         ACL2::REBUILD-FN-READ-FILTER ACL2-PC::FREE ACL2-PC::DV
         ACL2::FILE-WRITE-DATE$ ACL2::NORMALIZE-ABSOLUTE-COMMAND-NUMBER
         ACL2::MERGE-FREE-FAILURE-ALISTS-NIL-TAG ACL2::WITHOUT-EVISC-FN
         ACL2::ELIDE-LOCALS-LST ACL2::OK-IF-FN
         ACL2::COMBINE-SORTED-RW-CACHE-LISTS1 ACL2-PC::CASESPLIT
         ACL2::PUFF*-FN ACL2::RESET-KILL-RING ACL2-PC::QUIET
         ACL2-PC::REPEAT ACL2-PC::X ACL2-PC::PRINT-MAIN
         ACL2::ACL2-RAW-EVAL ACL2::RATIONAL-TO-DECIMAL-STRING
         ACL2::CHECK-SUM ACL2-PC::FINISH ACL2-PC::APPLY-LINEAR
         ACL2::HL-HSPACE-GROW-SBITS ACL2::PSTK-BINDINGS-AND-ARGS
         ACL2::ONE-WAY-UNIFY ACL2-PC::UP ACL2::READ-OBJECT-SUPPRESS
         ACL2-PC::REDUCE ACL2::CHK-LEGAL-DEFCONST-NAME
         ACL2::FIND-FIRST-ACCEPTABLE-DOMAIN ACL2::PC-SINGLE-STEP-1
         ACL2::LD-READ-KEYWORD-COMMAND1 ACL2-PC::P-TOP
         ACL2::NORMALIZE-LINEAR-SUM-1 ACL2-PC::RETRIEVE ACL2-PC::ORELSE
         ACL2-PC::SPLIT ACL2-PC::PSOG ACL2::SET-TERM-EVISC-TUPLE
         ACL2-PC::HELP ACL2::SET-CBD-FN ACL2::INCLUDE-BOOK-DIR
         ACL2::VARIANTP)) 
(COMMON-LISP::PROCLAIM
    '(COMMON-LISP::FTYPE
         (COMMON-LISP::FUNCTION (COMMON-LISP::T COMMON-LISP::*)
             COMMON-LISP::T)
         ACL2::MF-MULTIPROCESSING ACL2::COMPILE-UNCOMPILED-DEFUNS
         ACL2::PROFILE-FN ACL2::PROTECT-MV
         ACL2::CHECK-AGAINST-READ-FILE-ALIST ACL2::TT-START
         ACL2::COMPILE-UNCOMPILED-*1*-DEFUNS ACL2::MAYBE-UNTRACE!)) 
(COMMON-LISP::PROCLAIM
    '(COMMON-LISP::FTYPE
         (COMMON-LISP::FUNCTION (COMMON-LISP::T)
             COMMON-LISP::HASH-TABLE)
         ACL2::SER-ENCODER-SEEN-CONS ACL2::SER-ENCODER-SEEN-EQL
         ACL2::HL-FALTABLE-TABLE ACL2::HL-HSPACE-ADDR-HT
         ACL2::SER-ENCODER-SEEN-SYM ACL2::HL-HSPACE-PERSIST-HT
         ACL2::SER-ENCODER-SEEN-STR ACL2::HL-HSPACE-STR-HT
         ACL2::SER-ENCODER-SYMBOL-HT ACL2::HL-HSPACE-OTHER-HT)) 
(COMMON-LISP::PROCLAIM
    '(COMMON-LISP::FTYPE
         (COMMON-LISP::FUNCTION (COMMON-LISP::T)
             COMMON-LISP::SIMPLE-VECTOR)
         ACL2::HL-CACHE-KEYDATA ACL2::HL-CACHE-VALDATA
         ACL2::SER-DECODER-ARRAY)) 
(COMMON-LISP::PROCLAIM
    '(COMMON-LISP::FTYPE
         (COMMON-LISP::FUNCTION (COMMON-LISP::T)
             (COMMON-LISP::VALUES COMMON-LISP::T COMMON-LISP::T))
         ACL2::CAR-CDR-ABBREV-NAME ACL2::ADD-@PAR-SUFFIX
         ACL2::INTERN-IN-KEYWORD-PACKAGE ACL2::MAKE-PRETTY-PC-COMMAND
         ACL2::ST-LST)) 
(COMMON-LISP::PROCLAIM
    '(COMMON-LISP::FTYPE
         (COMMON-LISP::FUNCTION
             (COMMON-LISP::STRING COMMON-LISP::FIXNUM
                 COMMON-LISP::FIXNUM COMMON-LISP::FIXNUM COMMON-LISP::T
                 COMMON-LISP::T)
             COMMON-LISP::*)
         ACL2::FMT-TILDE-S1)) 
(COMMON-LISP::PROCLAIM
    '(COMMON-LISP::FTYPE
         (COMMON-LISP::FUNCTION
             (COMMON-LISP::BIT-VECTOR COMMON-LISP::T COMMON-LISP::T
                 COMMON-LISP::T)
             COMMON-LISP::T)
         ACL2::HL-REBUILD-ADDR-HT)) 
(COMMON-LISP::PROCLAIM
    '(COMMON-LISP::FTYPE
         (COMMON-LISP::FUNCTION
             (COMMON-LISP::STRING COMMON-LISP::FIXNUM
                 COMMON-LISP::STRING)
             COMMON-LISP::T)
         ACL2::STRING-PREFIXP-1)) 
(COMMON-LISP::PROCLAIM
    '(COMMON-LISP::FTYPE
         (COMMON-LISP::FUNCTION (COMMON-LISP::T)
             COMMON-LISP::CHARACTER)
         ACL2::SER-ENCODE-MAGIC)) 
(COMMON-LISP::PROCLAIM
    '(COMMON-LISP::FTYPE
         (COMMON-LISP::FUNCTION
             (COMMON-LISP::T COMMON-LISP::STRING COMMON-LISP::FIXNUM
                 COMMON-LISP::FIXNUM)
             COMMON-LISP::FIXNUM)
         ACL2::FIND-ALTERNATIVE-START)) 
(COMMON-LISP::PROCLAIM
    '(COMMON-LISP::FTYPE
         (COMMON-LISP::FUNCTION
             (COMMON-LISP::STRING COMMON-LISP::FIXNUM
                 COMMON-LISP::FIXNUM COMMON-LISP::T)
             COMMON-LISP::T)
         ACL2::CHECK-SUM-STRING1)) 
(COMMON-LISP::PROCLAIM
    '(COMMON-LISP::FTYPE
         (COMMON-LISP::FUNCTION
             (COMMON-LISP::STRING COMMON-LISP::FIXNUM
                 COMMON-LISP::FIXNUM COMMON-LISP::FIXNUM
                 COMMON-LISP::T)
             COMMON-LISP::T)
         ACL2::FMT-CHAR)) 
(COMMON-LISP::MAPC
    (COMMON-LISP::LAMBDA (COMPILER::X)
      (COMMON-LISP::SETF
          (COMMON-LISP::GET COMPILER::X 'COMPILER::PROCLAIMED-CLOSURE)
          COMMON-LISP::T))
    '(ACL2::HCOMP-RESTORE-DEFS ACL2::ACL2-COMPILE-FILE
         ACL2::WRITE-EXPANSION-FILE ACL2::MEMOIZE-FN
         ACL2::PHYSICAL-MEMORY ACL2::INSTALL-FOR-ADD-TRIP-INCLUDE-BOOK
         ACL2::UNTRACE$-FN1 ACL2::UNMEMOIZE-FN)) 
(COMMON-LISP::PROCLAIM
    '(COMMON-LISP::FTYPE
         (COMMON-LISP::FUNCTION (COMMON-LISP::INTEGER) COMMON-LISP::T)
         ACL2::ZP)) 
(COMMON-LISP::PROCLAIM
    '(COMMON-LISP::FTYPE
         (COMMON-LISP::FUNCTION (COMMON-LISP::T) COMMON-LISP::FIXNUM)
         ACL2::FCHECKSUM-OBJ ACL2::HL-HSPACE-ADDR-LIMIT
         ACL2::OP-HASH-INDEX-EVG ACL2::HL-MAKE-ADDR-LIMIT-NEXT
         ACL2::SER-DECODER-FREE ACL2::HL-MAKE-ADDR-LIMIT-CURRENT
         ACL2::NUMBER-OF-CALLS ACL2::CONS-COUNT-BOUNDED
         ACL2::NUMBER-OF-MHT-CALLS ACL2::ZERO-ONE-OR-MORE
         ACL2::SER-MAKE-ATOM-MAP ACL2::PONS-CALLS
         ACL2::PRINT-LDD-FORMULA-COLUMN ACL2::NUMBER-OF-HITS
         ACL2::COUNT-ASSUMPTIONS ACL2::SER-ENCODER-FREE-INDEX
         ACL2::FCHECKSUM-ATOM ACL2::CHECK-SUM-OBJ)) 
(COMMON-LISP::PROCLAIM
    '(COMMON-LISP::FTYPE
         (COMMON-LISP::FUNCTION (COMMON-LISP::FIXNUM) COMMON-LISP::T)
         ACL2::ZPF)) 
(COMMON-LISP::PROCLAIM
    '(COMMON-LISP::FTYPE
         (COMMON-LISP::FUNCTION (COMMON-LISP::STRING COMMON-LISP::T)
             COMMON-LISP::T)
         ACL2::INTERN-IN-PACKAGE-OF-SYMBOL ACL2::SER-ENCODE-STR
         ACL2::MAY-NEED-SLASHES-FN)) 
(COMMON-LISP::PROCLAIM
    '(COMMON-LISP::FTYPE
         (COMMON-LISP::FUNCTION (COMMON-LISP::T)
             (COMMON-LISP::SATISFIES ACL2::RATIONAL-LISTP))
         ACL2::TIME-TRACKER-TIMES)) 
(COMMON-LISP::PROCLAIM
    '(COMMON-LISP::FTYPE
         (COMMON-LISP::FUNCTION (COMMON-LISP::T)
             (COMMON-LISP::OR COMMON-LISP::NULL COMMON-LISP::RATIONAL))
         ACL2::TIME-TRACKER-INTERVAL ACL2::TIME-TRACKER-LATEST)) 
(COMMON-LISP::PROCLAIM
    '(COMMON-LISP::FTYPE
         (COMMON-LISP::FUNCTION (COMMON-LISP::BIT-VECTOR)
             (COMMON-LISP::INTEGER -9223372036854775808
                 9223372036854775807))
         ACL2::HL-FIX-SBITS-AFTER-GC)) 
(COMMON-LISP::PROCLAIM
    '(COMMON-LISP::FTYPE
         (COMMON-LISP::FUNCTION
             (COMMON-LISP::T COMMON-LISP::FIXNUM COMMON-LISP::FIXNUM
                 COMMON-LISP::T COMMON-LISP::T COMMON-LISP::T
                 COMMON-LISP::T COMMON-LISP::T COMMON-LISP::T
                 COMMON-LISP::T COMMON-LISP::T COMMON-LISP::T
                 COMMON-LISP::T COMMON-LISP::T COMMON-LISP::T
                 COMMON-LISP::T)
             COMMON-LISP::*)
         ACL2::REWRITE-WITH-LINEAR ACL2::REWRITE-SOLIDIFY-PLUS
         ACL2::REWRITE-WITH-LEMMAS)) 
(COMMON-LISP::PROCLAIM
    '(COMMON-LISP::FTYPE
         (COMMON-LISP::FUNCTION
             (COMMON-LISP::FIXNUM COMMON-LISP::T COMMON-LISP::T
                 COMMON-LISP::T)
             COMMON-LISP::*)
         ACL2::CHK-MEMO)) 
(COMMON-LISP::PROCLAIM
    '(COMMON-LISP::FTYPE
         (COMMON-LISP::FUNCTION
             (COMMON-LISP::FIXNUM COMMON-LISP::T COMMON-LISP::T
                 COMMON-LISP::T COMMON-LISP::T COMMON-LISP::T
                 COMMON-LISP::T COMMON-LISP::T COMMON-LISP::T
                 COMMON-LISP::T)
             COMMON-LISP::*)
         ACL2::REWRITE-SOLIDIFY-REC)) 
(COMMON-LISP::PROCLAIM
    '(COMMON-LISP::FTYPE
         (COMMON-LISP::FUNCTION
             (COMMON-LISP::T COMMON-LISP::FIXNUM COMMON-LISP::T
                 COMMON-LISP::T)
             COMMON-LISP::*)
         ACL2::FMT-TILDE-S ACL2::FMT-CTX ACL2::FMT-IN-CTX)) 
(COMMON-LISP::PROCLAIM
    '(COMMON-LISP::FTYPE
         (COMMON-LISP::FUNCTION
             (COMMON-LISP::FIXNUM COMMON-LISP::T COMMON-LISP::T
                 COMMON-LISP::T COMMON-LISP::T)
             COMMON-LISP::*)
         ACL2::ONE-WAY-UNIFY1-CST ACL2::ONE-WAY-UNIFY1-CST-LST
         ACL2::CHK-MEMO-2)) 
(COMMON-LISP::PROCLAIM
    '(COMMON-LISP::FTYPE
         (COMMON-LISP::FUNCTION
             (COMMON-LISP::FIXNUM COMMON-LISP::T COMMON-LISP::FIXNUM
                 COMMON-LISP::T COMMON-LISP::T COMMON-LISP::T
                 COMMON-LISP::T COMMON-LISP::T COMMON-LISP::T
                 COMMON-LISP::T COMMON-LISP::T COMMON-LISP::T)
             COMMON-LISP::*)
         ACL2::COMBINE-OP-CSTS)) 
(COMMON-LISP::PROCLAIM
    '(COMMON-LISP::FTYPE
         (COMMON-LISP::FUNCTION
             (COMMON-LISP::FIXNUM COMMON-LISP::T COMMON-LISP::T
                 COMMON-LISP::T COMMON-LISP::T COMMON-LISP::T
                 COMMON-LISP::T)
             COMMON-LISP::*)
         ACL2::MAKE-IF-NO-MEMO ACL2::ONE-WAY-UNIFY1-CST-EQUAL)) 
(COMMON-LISP::PROCLAIM
    '(COMMON-LISP::FTYPE
         (COMMON-LISP::FUNCTION
             (COMMON-LISP::T COMMON-LISP::FIXNUM COMMON-LISP::FIXNUM
                 COMMON-LISP::T COMMON-LISP::T)
             COMMON-LISP::*)
         ACL2::PRINT-STRING-REPEAT)) 
(COMMON-LISP::PROCLAIM
    '(COMMON-LISP::FTYPE
         (COMMON-LISP::FUNCTION
             (COMMON-LISP::FIXNUM COMMON-LISP::T COMMON-LISP::FIXNUM
                 COMMON-LISP::T COMMON-LISP::FIXNUM COMMON-LISP::T
                 COMMON-LISP::T COMMON-LISP::T COMMON-LISP::T
                 COMMON-LISP::T COMMON-LISP::T COMMON-LISP::T
                 COMMON-LISP::T COMMON-LISP::T)
             COMMON-LISP::*)
         ACL2::COMBINE-OP-CSTS-GUTS)) 
(COMMON-LISP::PROCLAIM
    '(COMMON-LISP::FTYPE
         (COMMON-LISP::FUNCTION (COMMON-LISP::T) ACL2::HL-FALSLOT)
         ACL2::HL-FALTABLE-SLOT1 ACL2::HL-FALTABLE-SLOT2)) 
(COMMON-LISP::PROCLAIM
    '(COMMON-LISP::FTYPE
         (COMMON-LISP::FUNCTION (COMMON-LISP::T) COMMON-LISP::RATIONAL)
         ACL2::TIME-TRACKER-INIT ACL2::TIME-TRACKER-ELAPSED)) 
(COMMON-LISP::PROCLAIM
    '(COMMON-LISP::FTYPE
         (COMMON-LISP::FUNCTION
             (COMMON-LISP::FIXNUM COMMON-LISP::T COMMON-LISP::T
                 COMMON-LISP::FIXNUM COMMON-LISP::T COMMON-LISP::T
                 COMMON-LISP::T COMMON-LISP::T COMMON-LISP::T
                 COMMON-LISP::T COMMON-LISP::T COMMON-LISP::T
                 COMMON-LISP::T COMMON-LISP::T COMMON-LISP::T)
             COMMON-LISP::*)
         ACL2::COMBINE-OP-CSTS-COMM)) 
(COMMON-LISP::PROCLAIM
    '(COMMON-LISP::FTYPE
         (COMMON-LISP::FUNCTION
             (COMMON-LISP::FIXNUM COMMON-LISP::T COMMON-LISP::T
                 COMMON-LISP::T COMMON-LISP::T COMMON-LISP::T
                 COMMON-LISP::FIXNUM COMMON-LISP::T COMMON-LISP::T)
             COMMON-LISP::*)
         ACL2::COMBINE-OP-CSTS-SIMPLE)) 
(COMMON-LISP::PROCLAIM
    '(COMMON-LISP::FTYPE
         (COMMON-LISP::FUNCTION
             (COMMON-LISP::T COMMON-LISP::T COMMON-LISP::T
                 COMMON-LISP::T)
             COMMON-LISP::FIXNUM)
         ACL2::CHECK-SUM-CERT-OBJ)) 
(COMMON-LISP::PROCLAIM
    '(COMMON-LISP::FTYPE
         (COMMON-LISP::FUNCTION
             (COMMON-LISP::T COMMON-LISP::T COMMON-LISP::T
                 COMMON-LISP::T COMMON-LISP::T)
             COMMON-LISP::FIXNUM)
         ACL2::STEP-LIMIT-ERROR1 ACL2::DEGREE-OF-MATCH2)) 
(COMMON-LISP::PROCLAIM
    '(COMMON-LISP::FTYPE
         (COMMON-LISP::FUNCTION
             (COMMON-LISP::FIXNUM COMMON-LISP::T COMMON-LISP::T
                 COMMON-LISP::T)
             COMMON-LISP::T)
         ACL2::SUBSUMES-REC)) 
(COMMON-LISP::PROCLAIM
    '(COMMON-LISP::FTYPE
         (COMMON-LISP::FUNCTION
             (COMMON-LISP::INTEGER COMMON-LISP::T COMMON-LISP::T)
             COMMON-LISP::T)
         ACL2::EXTEND-T-STACK ACL2::FIRST-N-AC ACL2::UPDATE-NTH)) 
(COMMON-LISP::PROCLAIM
    '(COMMON-LISP::FTYPE
         (COMMON-LISP::FUNCTION
             (COMMON-LISP::T COMMON-LISP::T COMMON-LISP::T)
             COMMON-LISP::FIXNUM)
         ACL2::SER-DECODE-AND-LOAD-CONSES ACL2::CHECK-SUM-CERT
         ACL2::SER-DECODE-AND-LOAD-PACKAGE
         ACL2::SER-DECODE-AND-LOAD-STRS)) 
(COMMON-LISP::PROCLAIM
    '(COMMON-LISP::FTYPE
         (COMMON-LISP::FUNCTION
             (COMMON-LISP::FIXNUM COMMON-LISP::T COMMON-LISP::T
                 COMMON-LISP::T COMMON-LISP::T COMMON-LISP::T)
             COMMON-LISP::T)
         ACL2::SUBSUMES1)) 
(COMMON-LISP::PROCLAIM
    '(COMMON-LISP::FTYPE
         (COMMON-LISP::FUNCTION
             (COMMON-LISP::T COMMON-LISP::T COMMON-LISP::FIXNUM
                 COMMON-LISP::FIXNUM COMMON-LISP::FIXNUM)
             COMMON-LISP::FIXNUM)
         ACL2::OCCUR-CNT-BOUNDED ACL2::OCCUR-CNT-BOUNDED-LST)) 
(COMMON-LISP::PROCLAIM
    '(COMMON-LISP::FTYPE
         (COMMON-LISP::FUNCTION
             (COMMON-LISP::FIXNUM COMMON-LISP::FIXNUM COMMON-LISP::T)
             COMMON-LISP::FIXNUM)
         ACL2::OP-HASH-INDEX-STRING)) 
(COMMON-LISP::PROCLAIM
    '(COMMON-LISP::FTYPE
         (COMMON-LISP::FUNCTION (COMMON-LISP::FIXNUM COMMON-LISP::T)
             COMMON-LISP::CHARACTER)
         ACL2::SER-ENCODE-NAT-FIXNUM)) 
(COMMON-LISP::PROCLAIM
    '(COMMON-LISP::FTYPE
         (COMMON-LISP::FUNCTION (COMMON-LISP::INTEGER COMMON-LISP::T)
             COMMON-LISP::CHARACTER)
         ACL2::SER-ENCODE-NAT-LARGE)) 
(COMMON-LISP::PROCLAIM
    '(COMMON-LISP::FTYPE
         (COMMON-LISP::FUNCTION
             (COMMON-LISP::FIXNUM COMMON-LISP::T COMMON-LISP::T)
             COMMON-LISP::T)
         ACL2::ASET-T-STACK ACL2::FIRST-N-AC-REV)) 
(COMMON-LISP::PROCLAIM
    '(COMMON-LISP::FTYPE
         (COMMON-LISP::FUNCTION
             (COMMON-LISP::T COMMON-LISP::FIXNUM COMMON-LISP::T
                 COMMON-LISP::FIXNUM COMMON-LISP::FIXNUM COMMON-LISP::T
                 COMMON-LISP::T)
             COMMON-LISP::T)
         ACL2::PPR1-LST ACL2::PPR1)) 
(COMMON-LISP::PROCLAIM
    '(COMMON-LISP::FTYPE
         (COMMON-LISP::FUNCTION
             (COMMON-LISP::T COMMON-LISP::T COMMON-LISP::*)
             COMMON-LISP::FIXNUM)
         ACL2::METER-MAID)) 
(COMMON-LISP::PROCLAIM
    '(COMMON-LISP::FTYPE
         (COMMON-LISP::FUNCTION
             (COMMON-LISP::T COMMON-LISP::FIXNUM COMMON-LISP::T
                 COMMON-LISP::T COMMON-LISP::T)
             COMMON-LISP::T)
         ACL2::PPR)) 
(COMMON-LISP::PROCLAIM
    '(COMMON-LISP::FTYPE
         (COMMON-LISP::FUNCTION
             (COMMON-LISP::INTEGER COMMON-LISP::INTEGER COMMON-LISP::T)
             COMMON-LISP::INTEGER)
         ACL2::SER-DECODE-NAT-LARGE)) 
(COMMON-LISP::PROCLAIM
    '(COMMON-LISP::FTYPE
         (COMMON-LISP::FUNCTION
             (COMMON-LISP::T COMMON-LISP::FIXNUM COMMON-LISP::FIXNUM)
             COMMON-LISP::T)
         ACL2::OP-HASH-INDEX1)) 
(COMMON-LISP::PROCLAIM
    '(COMMON-LISP::FTYPE
         (COMMON-LISP::FUNCTION (COMMON-LISP::T) COMMON-LISP::T)
         ACL2::ABBREVIATION-RAW-TERM-P ACL2::DIGIT-TO-CHAR
         ACL2::SHALLOW-CLAUSIFY ACL2::DEFABSSTOBJ-LOGIC-SUBST
         ACL2::TILDE-*-PROPS-FN-PHRASE ACL2::GET-IGNORES
         ACL2::ENS-FROM-PSPV ACL2::SET-FC-REPORT-ON-THE-FLY
         ACL2::WRITABLE-FILE-LISTP ACL2::DCL-FIELDS1 ACL2::ARGLISTP
         ACL2::NEVER-MEMOIZE-FN ACL2::EVENS ACL2::GET-IGNORABLES
         ACL2::ALL-QUOTEPS ACL2::MAYBE-UNMEMOIZE ACL2::SCAN-TO-EVENT
         ACL2::STOBJ-UPDATER-GUESS-FROM-ACCESSOR
         ACL2::INITIAL-GLOBAL-ENABLED-STRUCTURE
         ACL2::STRICT-MERGE-SORT-SYMBOL-<-CDRS ACL2::TS-UNION0-FN
         ACL2::ACCESS-LDD-STATUS ACL2::GET-HINTS
         ACL2::DECODE-TYPE-ALIST ACL2::LISP-BOOK-SYNTAXP
         ACL2::HL-HSPACE-HONS-WASH ACL2::OPEN-CHANNEL-LISTP
         ACL2::POSSIBLE-TRIVIAL-CLAUSE-P ACL2::NAME-DROPPER
         ACL2::BOOLEAN-TERM-VAR ACL2::ALWAYS-BIGGERP-DATA
         ACL2::POS-LISTP ACL2::TS-UNION-FN ACL2::ALL-VARIABLEP
         ACL2::ALIST-TO-DOUBLETS ACL2::MF-LEN-INPUTS
         ACL2::COLLECT-COARSENINGS ACL2::WEAK-FC-ACTIVATION-P
         ACL2::IPRINT-LAST-INDEX ACL2::CLOAKING-DEVICE-OBJ
         ACL2::NON-CONS-CDR ACL2::RECORD-MAKER-RECOGNIZER-NAME
         ACL2::STANDARD-CHAR-LISTP ACL2::READ-FILES-P
         ACL2::TERM-LIST-IGNORE-OKP ACL2::END-PREHISTORIC-WORLD
         ACL2::STRIP-NON-HIDDEN-PACKAGE-NAMES ACL2::WORLD-TO-NEXT-EVENT
         ACL2::STRIP-FFN-SYMBS ACL2::MUTUAL-RECURSION-GUARDP
         ACL2::BOOLEANP ACL2::DEFEVALUATOR-FORM/FNS-CLAUSES
         ACL2::IPRINT-ENABLEDP ACL2::SCRUNCH-EQ ACL2::FIX-TRUE-LIST
         ACL2::WEAK-PROVE-SPEC-VAR-P ACL2::GLOBAL-TABLE-CARS1
         ACL2::USE-NAMES-IN-TTREE ACL2::POP-BRR-STACK-FRAME
         ACL2::NO-DUPLICATESP-EQ-EXEC ACL2::DMR-STOP-FN
         ACL2::PRINT-LDD-FULL-OR-SKETCH/ENCAPSULATE
         ACL2::PROOF-CHECKER-CLAUSE-LIST
         ACL2::ASSUMNOTE-LIST-TO-CLAUSE-ID-LIST ACL2::REPLACED-STOBJ
         ACL2::SPLIT-ON-CONJOINED-DISJUNCTIONS
         ACL2::REPLACE-DEFUN@PAR-WITH-DEFUN ACL2::WORMHOLE-ENTRY-CODE
         ACL2::MF-LEN-OUTPUTS ACL2::RW-CACHEABLE-NIL-TAG
         ACL2::HL-HSPACE-FAST-ALIST-SUMMARY
         ACL2::COLLECT-NON-LEGAL-VARIABLEPS ACL2::READABLE-FILES-LISTP
         ACL2::CL-PROC-NAMES-IN-TTREE ACL2::CLASSES-THEOREMS
         ACL2::CONGRUENT-STOBJ-REP-RAW ACL2::ACCESS-EVENT-TUPLE-NAMEX
         ACL2::STRIP-LAST-ELEMENTS
         ACL2::CONVERT-NON-NIL-SYMBOLS-TO-KEYWORDS
         ACL2::STOP-PROOF-TREE-FN ACL2::LD-EVISC-TUPLE
         ACL2::PUFFABLE-ENCAPSULATE-P ACL2::PRINT-RULES-SUMMARY
         ACL2::PUSH-BRR-STACK-FRAME ACL2::STRING-DOWNCASE1
         ACL2::NO-DUPLICATESP-EQL-EXEC$GUARD-CHECK
         ACL2::WEAK-ACCP-INFO-P ACL2::PRINT-WARNINGS-SUMMARY
         ACL2::NON-TRIVIAL-ENCAPSULATE-EE-ENTRIES ACL2::GOOD-BYE-FN
         ACL2::PUFFERT ACL2::ASSUMNOTE-LIST-TO-TOKEN-LIST
         ACL2::EVAL-TYPE-SET-LST ACL2::WEAK-LINEAR-LEMMA-P
         ACL2::TYPE-SET-QUOTE ACL2::ERASE-RW-CACHE-FROM-PSPV
         ACL2::SER-DECODE-NAT ACL2::WEAK-GOAL-P ACL2::ALL-SYMBOLS-LIST
         ACL2::IFIX ACL2::TS-COMPLEMENT-FN
         ACL2::REMOVE-ADJACENT-DUPLICATES-EQ ACL2::WEAK-PEQUIV-P
         ACL2::CLOAKING-DEVICE-P ACL2::MAYBE-SET-RW-CACHE-STATE-ENABLED
         ACL2::GET-NAMES ACL2::SYMBOL-NAME-ORDER
         ACL2::DEFAULT-DEFUN-MODE-FROM-STATE ACL2::SPLICE-INSTRS
         ACL2::STANDARD-THEORIES ACL2::BOOLEAN-LISTP
         ACL2::TILDE-*-PROPS-FN-PHRASE1 ACL2::ACCESS-COMMAND-TUPLE-FORM
         ACL2::TAU-INTERVAL-LO ACL2::COUNT-IFS
         ACL2::CLAUSE-PROCESSOR-FNS ACL2::WEAK-ENABLED-STRUCTURE-P
         ACL2::PRINT-PROOF-TREE ACL2::RECORD-CHANGER-FUNCTION-NAME
         ACL2::TILDE-*-ASSUMNOTES-COLUMN-PHRASE-GAG-MODE
         ACL2::LET*-ABSTRACTIONP ACL2::DEFABSSTOBJ-RAW-DEFS-REC
         ACL2::SYSFILE-OR-STRING-LISTP ACL2::MAGIC-EV-FNCALL-CL-PROC
         ACL2::O-P ACL2::LIST*-MACRO ACL2::ENABLED-STRUCTUREP
         ACL2::REMOVE-LAMBDAS-LST ACL2::GET-GUARD-HINTS1
         ACL2::STRIP-TOP-LEVEL-NOTS-AND-FORCES
         ACL2::WEAK-ABSSTOBJ-INFO-P ACL2::ACL2-ORACLE
         ACL2::LEGAL-CONSTANTP1 ACL2::ADD-LINEAR-TERMS-FN
         ACL2::CONFLICTING-IMPORTS ACL2::WEAK-REWRITE-RULE-P
         ACL2::EVISC-INDEXED-INSTRS-REC ACL2::SYSTEM-INCLUDE-BOOK-FORMS
         ACL2::TYPE-ALIST-ENTRYP ACL2::WEAK-PC-STATE-P
         ACL2::DUMB-NEGATE-LIT ACL2::WEAK-DISC-TREE
         ACL2::INITIAL-MEMOIZE-CALL-ARRAY ACL2::TAU-INTERVAL-HI
         ACL2::UNPARSE-SIGNATURE ACL2::HONS-CLEAR!
         ACL2::CHK-BAD-LISP-OBJECT ACL2::FMAKUNBOUND!
         ACL2::PROGRAM-DECLARED-P1
         ACL2::LEGAL-VARIABLE-OR-CONSTANT-NAMEP ACL2::WEAK-ACCP-ENTRY-P
         ACL2::LD-FIX-COMMAND ACL2::CHARACTER-ALISTP
         ACL2::CONVERT-BOOK-NAME-TO-PORT-NAME ACL2::MSWINDOWS-DRIVE1
         ACL2_*1*_COMMON-LISP::IMAGPART ACL2::ALL-TYPE-REASONING-TAGS-P
         ACL2::ALWAYS-BOUNDP-GLOBAL ACL2::RELEVANT-POSNS-LAMBDAS-TOP
         ACL2::STATE-GLOBAL-BINDINGS ACL2_*1*_COMMON-LISP::CONSP
         ACL2::LOCK-SYMBOL-NAME-P ACL2::UNPROVED-GOALS
         ACL2::BACKCHAIN-LIMIT-LISTP ACL2::MERGE-SORT-LENGTH
         ACL2::PLIST-WORLDP ACL2::BAD-LISP-OBJECTP
         ACL2::MAKE-CHARACTER-LIST ACL2::ORDERED-SYMBOL-ALISTP
         ACL2::EVENT-NAME-AND-TYPES-AND-RAW-TERM ACL2::PRIMORDIAL-WORLD
         ACL2::SHOW-POLY-LST ACL2::ALL-VARS-IN-HYPS
         ACL2::MAKE-ABSSTOBJ-LOGIC-EXEC-PAIRS
         ACL2::WEAK-TYPE-PRESCRIPTION-P
         ACL2::DECODE-TAU-CONJUNCTIVE-RULES
         ACL2::PREVIOUS-PROCESS-WAS-SPECIOUSP
         ACL2::WEAK-BUILT-IN-CLAUSE-P ACL2::LMI-NAME-OR-RUNE
         ACL2::STRIP-FORCE-AND-CASE-SPLIT
         ACL2::PLIST-WORLDP-WITH-FORMALS
         ACL2::SUPER-DEFUN-WART-BINDINGS ACL2::LD-QUERY-CONTROL-ALISTP
         ACL2::FIX-TRACE ACL2::COLLECT-LAMBDA-KEYWORDPS
         ACL2::ADD-EACH-LITERAL ACL2::SER-DECODE-RAT ACL2::TIME/CALL
         ACL2::RW-CACHE-ALIST-NIL-TAG-P ACL2::MFC-UNIFY-SUBST
         ACL2::WEAK-CONGRUENCE-RULE-P ACL2::MSGP ACL2::GEN-VAR-MARKER
         ACL2::STATE-GLOBAL-LET*-GET-GLOBALS ACL2::ONE-BIT-TYPE-SETP
         ACL2::CHECK-OUT-INSTANTIABLEP ACL2::ACCESS-EVENT-TUPLE-DEPTH
         ACL2::IGNORED-ATTACHMENT-MSG ACL2::QUOTEP
         ACL2::WEAK-COMMAND-NUMBER-BASELINE-INFO-P
         ACL2::INSIDE-DEFABSSTOBJ ACL2::DEBUGGER-ENABLEDP
         ACL2::COERCE-TO-PROCESS-NAME-LST ACL2::GOOD-ATOM-LISTP
         ACL2::HL-FALSLOT-VAL ACL2::OK-TO-FORCE ACL2::READ-FILE-LISTP
         ACL2::MAX-FORM-COUNT ACL2::DECODE-TAU-CONJUNCTIVE-RULE
         ACL2::DECODE-IDATE ACL2::WEAK-THEORY-INVARIANT-RECORD-P
         ACL2::WEAK-GAG-STATE-P ACL2::REDEFINED-NAMES
         ACL2_*1*_COMMON-LISP::RATIONALP ACL2::ERASE-RW-CACHE
         ACL2::WEAK-FC-DERIVATION-P ACL2::UNARY-/
         ACL2_*1*_COMMON-LISP::REALPART ACL2::MERGE-SORT-CAR->
         ACL2::PROGRAM-DECLARED-P ACL2::HL-HSPACE-NORMEDP-WRAPPER
         ACL2::LEAF-CST-LIST-ARRAY ACL2::MONITORABLE-RUNES
         ACL2::TAU-AUTO-MODEP ACL2::CHARS-FOR-TILDE-@-CLAUSE-ID-PHRASE
         ACL2::CLEAN-TYPE-ALIST ACL2::TAU-INTERVAL-LO-REL
         ACL2::TILDE-*-ELIM-PHRASE3 ACL2::FLATTEN-ANDS-IN-LIT-LST
         ACL2::ALMOST-QUOTEP ACL2::PROBABLY-NOT-VALIDP ACL2::ZIP
         ACL2::CST-NONNILP ACL2::SORT-SYMBOL-LISTP
         ACL2::MAKE-PRETTY-PC-INSTR ACL2::SAVE-BRR-GLOBALS
         ACL2::SORT-TYPE-ALIST-SEGMENTS ACL2::FC-PAIR-LST
         ACL2::DEFAULT-MEASURE-FUNCTION ACL2::TILDE-*-PREPROCESS-PHRASE
         ACL2::INITIALIZE-TAU-GLOBALS ACL2::MACROEXPAND1!
         ACL2::WEAK-INDUCTION-RULE-P ACL2::OR-MACRO
         ACL2::NON-MEMOIZABLE-STOBJ-RAW ACL2::CST-QUOTE-LISTP
         ACL2::STRIP-CARS ACL2::LAMBDA-NEST-HIDEP ACL2::NFIX
         ACL2::COUNT-NON-NILS ACL2::CST-LIST-TO-EVG-LIST
         ACL2::STRICT-MERGE-SORT-SYMBOL-< ACL2::EQLABLE-LISTP
         ACL2::WEAK-SATISFIES-TYPE-SPEC-P ACL2::COND-CLAUSESP
         ACL2::FILTER-REDUNDANT-APPROVED-FC-DERIVATION
         ACL2::HL-FALSLOT-P ACL2::CHARACTER-LISTP
         ACL2::SER-DECODE-COMPLEX ACL2_*1*_COMMON-LISP::CHARACTERP
         ACL2::FILE-CLOCK-P ACL2::WEAK-RECOGNIZER-TUPLE-P
         ACL2::CONTAINS-ASSUMPTIONP ACL2::MAX-NUME-EXCEEDED-ERROR
         ACL2::REMOVE-GUARD-HOLDERS-LST ACL2::VARIFY!-LST
         ACL2::TOTAL-TIME ACL2::ACL2-VERSION-R-P ACL2::MEMOIZEDP-RAW
         ACL2::ALMOST-QUOTEP1 ACL2::TRACE-EVISCERATION-ALIST
         ACL2::EXECUTION-ORDER ACL2::OOPS-WARNING ACL2::HL-HSPACE-P
         ACL2::WEAK-BDD-RULE-P ACL2::PROGRAM-DECLARED-P2
         ACL2::ACCESS-EVENT-TUPLE-SYMBOL-CLASS ACL2::GET-HINTS1
         ACL2::TILDE-*-OR-HIT-SUMMARY-PHRASE
         ACL2::REPLACE-DUPLICATE-VARS-WITH-ANONYMOUS-VAR
         ACL2::HONS-COPY-PERSISTENT ACL2::HL-FALSLOT-KEY
         ACL2::DEFAULT-COMPILE-FNS ACL2::DUPLICATES
         ACL2::COLLECT-PROBLEMATIC-PRE-EQUIVALENCE-RULE-NAMES
         ACL2::COLLECT-PARENTS ACL2::MERGE-SORT-LEXORDER
         ACL2::THROW-RAW-EV-FNCALL ACL2::DISJOIN-LST
         ACL2::WEAK-PEQUIV-INFO-P ACL2::MEMOIZE-INFO
         ACL2::WEAK-DEFSTOBJ-TEMPLATE-P ACL2::CLEAR-EVENT-DATA
         ACL2::BOGUS-FALSIFYING-ASSIGNMENT-VAR ACL2::GET-SIG-FNS
         ACL2::MATCH-FREE-OVERRIDE
         ACL2::CHARS-FOR-TILDE-@-CLAUSE-ID-PHRASE/PRIMES
         ACL2::REMOVE-STOBJ-INLINE-DECLARE ACL2::RW-CACHE-STATE
         ACL2::EXPAND-INEQUALITY-FNCALL1
         ACL2::LET-FORM-FOR-PC-STATE-VARS ACL2::PRINT-BASE-P
         ACL2::GC$-FN ACL2::ERASE-GAG-STATE
         ACL2::STRIP-FORCE-AND-CASE-SPLIT-IN-HYPS-OF-PAIRS
         ACL2::REWRITE-RULE-TERM ACL2::RESTORE-BRR-GLOBALS
         ACL2::TAU-SUM-LST ACL2::CDR-SORT-RW-CACHE ACL2::WEAK-GFRAME-P
         ACL2::ACCESS-COMMAND-TUPLE-LAST-MAKE-EVENT-EXPANSION
         ACL2::DUMB-ASSUMPTION-SUBSUMPTION ACL2::FORCED-HYPS
         ACL2::WEAK-ASSUMNOTE-P ACL2::MATCH-FREE-DEFAULT
         ACL2::MEMOIZE-CONDITION ACL2::BINARY-*-LEAVES
         ACL2::REFLEXIVITY ACL2::NORMALIZE-ALLEGED-EVALUATOR-CLAUSE-SET
         ACL2::REMOVE-STRINGS ACL2::INSTR-NAME ACL2::TAU-SIZE ACL2::OS
         ACL2::MORE-THAN-SIMPLIFIEDP ACL2::PUNCTP ACL2::TIMER-ALISTP
         ACL2::HIDE-LAMBDAS1 ACL2::DUMB-FN-COUNT
         ACL2::USER-STOBJ-ALIST1 ACL2::OR-LIST
         ACL2::LOGICAL-NAME-TYPE-STRING
         ACL2::TAG-TREE-OCCUR-ASSUMPTION-NIL ACL2::HL-GET-FINAL-CDR
         ACL2::GET-GUARD-HINTS ACL2::NORMALIZE-POLY
         ACL2::DEFSTOBJ-REDUNDANCY-BUNDLE ACL2::FIX-FREE-FAILURE-REASON
         ACL2::ALL-VARS ACL2::BOOLEAN-FN ACL2::FLUSH-COMPRESS
         ACL2::BY-NAMES-IN-TTREE ACL2::OUTPUT-IN-INFIXP
         ACL2::CURRENT-FC-CALL-ALIST ACL2::CONJOIN-UNTRANSLATED-TERMS
         ACL2::GLOBAL-TABLE ACL2::INSTR-LISTP
         ACL2::MAX-ABSOLUTE-COMMAND-NUMBER
         ACL2::REMOVE-REDUNDANT-NO-OPS ACL2::CHK-LEGAL-INIT-MSG
         ACL2::PC-STATE-VARS ACL2::INSIST
         ACL2::EQUIVALENCE-RELATION-CONDITION
         ACL2::TYPE-ALIST-EQUALITY-LOOP-EXIT ACL2::WEAK-TAU-P
         ACL2::IMPROPER-CONSP ACL2::PLAUSIBLE-DCLSP ACL2::D-POS-LISTP
         ACL2::WRITTEN-FILES ACL2::THEORY-FN-TRANSLATED-CALLP
         ACL2::WEAK-PEQUIVS-PROPERTY-P
         ACL2::POSSIBLY-ADD-LISP-EXTENSION ACL2::OVERRIDE-HINTS
         ACL2::MARK-UNFINISHED-INSTRS ACL2::WEAK-TESTS-AND-ALISTS-P
         ACL2::PRIMORDIAL-EVENT-MACRO-AND-FN1 ACL2::PARSE-CLAUSE-ID
         ACL2::REVERSE-INTO-DMR-ARRAY
         ACL2::FILTER-ALL-SATISFYING-FC-DERIVATIONS
         ACL2::PREPROCESS-HYP ACL2::DCL-GUARDIAN
         ACL2::UNPROVED-PC-PROVE-CLAUSES ACL2::REALFIX
         ACL2::RECURSIVE-FN-ON-FNSTACKP ACL2::REMOVE-GUARD-HOLDERS
         ACL2::STEP-LIMIT-FROM-TABLE ACL2::ALISTP ACL2::PLIST-TO-ALIST
         ACL2::FIRST-KNOWN-PACKAGE-ALIST ACL2::SIMPLIFY-TESTS-AND-CALLS
         ACL2::ACCESS-COMMAND-TUPLE-DEFUN-MODE
         ACL2::STRIP-ACCESSOR-NAMES ACL2::TIME-LIMIT5-REACHED-P
         ACL2::GOALS-TO-CLAUSE-LIST ACL2::WEAK-JUSTIFICATION-P
         ACL2::WEAK-CERTIFY-BOOK-INFO-P ACL2::BIG-CLOCK-NEGATIVE-P
         ACL2::WEAK-METAFUNCTION-CONTEXT-P ACL2::UNION-EQ-CARS
         ACL2::REMOVE-DUPLICATES-EQ-EXEC$GUARD-CHECK
         ACL2::PSEUDO-TERM-LIST-LISTP ACL2_*1*_COMMON-LISP::INTEGERP
         ACL2::NO-DUPLICATESP-EQUAL ACL2::GEN-FORMALS-FROM-PRETTY-FLAGS
         ACL2::DEFABSSTOBJ-RAW-DEF ACL2::PSEUDO-TERMP
         ACL2::MERGE-SORT-TERM-ORDER ACL2::RECOVER-FORCED-RUNES
         ACL2::INTEGER-LISTP ACL2::PRINT-SUMMARY-ON-ERROR
         ACL2::IGNORE-VARS ACL2::TILDE-*-IRRELEVANT-FORMALS-MSG1
         ACL2::TTAG ACL2::WEAK-EXPAND-HINT-P ACL2::DECLS-AND-DOC
         ACL2::PACKN ACL2_*1*_COMMON-LISP::CODE-CHAR
         ACL2::ALL-TAU-EMPTYP ACL2::PRETTYIFY-SUBST
         ACL2::WEAK-DEFERRED-TTAG-NOTE-P ACL2::F-GET-LD-SPECIALS
         ACL2::LD-KEYWORD-ALIASES ACL2::MFC-ANCESTORS
         ACL2::NUMBER-OF-MEMOIZED-ENTRIES ACL2::VERBOSE-PSTACK
         ACL2::WRITEABLE-FILES ACL2::MF-NUM-TO-STRING ACL2::DISJOIN
         ACL2::WEAK-TESTS-AND-CALL-P
         ACL2::NO-DUPLICATESP-CHECKS-FOR-STOBJ-LET-ACTUALS/ALIST
         ACL2::NO-DUPLICATESP-EQL-EXEC ACL2::FLUSH-UNDO-STACK
         ACL2::ARGLISTP1 ACL2::DMR-START-FN ACL2::RFIX
         ACL2::MAKE-NON-NIL-TTREE ACL2::WEAK-SIGNATURE-RULE-P
         ACL2::TAU-INTERVAL-HI-REL ACL2::FOUND-HIT-REWRITE-HIST-ENTRY
         ACL2::GET-REWRITE-AND-DEFN-RUNES-FROM-RUNIC-MAPPING-PAIRS
         ACL2::ERROR-TRACE-SUGGESTION ACL2::MERGE-SORT-SYMBOL-<
         ACL2::TRUE-POLYP ACL2::INVISIBLE-FNS-TABLE
         ACL2::TILDE-*-BAD-INSIGS-PHRASE
         ACL2::FIND-CANDIDATE-EQUIVALENCE-RELATION
         ACL2::WRITEABLE-FILES-P ACL2::PRINT-GAG-STATE
         ACL2::DEFCONST-NAME ACL2::READABLE-FILES ACL2::REWRITE-EQUIV
         ACL2::MERGE-SORT-CAR-< ACL2::ZERO-FACTOR-P
         ACL2::WEAK-MEMOIZE-INFO-HT-ENTRY-P ACL2::OPEN-CHANNELS-P
         ACL2::TAU-DATABASE ACL2::TRUE-LIST-LISTP
         ACL2::SYMBOL-TO-FIXNUM-CREATE ACL2::ACL2-MAGIC-MFC
         ACL2::EQUAL-MOD-ELIDE-LOCALS1 ACL2::EQLABLE-ALISTP
         ACL2::REMOVE-DUPLICATES-EQL-EXEC$GUARD-CHECK
         ACL2::PRINT-ALL-GOALS-PROVED-MESSAGE ACL2::LAMBDA-NEST-UNHIDE
         ACL2::LIST-ALL-PACKAGE-NAMES-LST ACL2::HONS-ENABLEDP
         ACL2::WEAK-IO-RECORD-P ACL2_*1*_ACL2::ACL2-NUMBERP
         ACL2::REMOVE-LAMBDAS ACL2::MF-DCLS
         ACL2::DEFAULT-VERIFY-GUARDS-EAGERNESS ACL2::ACCESS-LDD-N
         ACL2::ERASE-RW-CACHE-ANY-TAG-FROM-PSPV ACL2::GC-OFF1
         ACL2::CHK-NO-DUPLICATESP
         ACL2::TILDE-*-CONJUNCTION-OF-POSSIBLY-FORCED-NAMES-PHRASE1
         ACL2::WEAK-ATTACHMENT-P ACL2::STRIP-CADDRS ACL2::TILDE-@P
         ACL2::COUNT-TAU-SIGS-BY-SLOT ACL2::ACL2-COUNT
         ACL2::TS-BUILDER-CASE-LISTP ACL2::PTS-TO-TTREE-LST
         ACL2::WEAK-DEFSTOBJ-FIELD-TEMPLATE-P
         ACL2::ACCUMULATED-PERSISTENCE-MAKE-FAILURES
         ACL2::PRINT-DEFERRED-TTAG-NOTES-SUMMARY
         ACL2::WEAK-ABSSTOBJ-METHOD-P ACL2::GAG-MODE-EVISC-TUPLE
         ACL2::REPLACE-BAD-LISP-OBJECT ACL2::WEAK-BDDSPV-P
         ACL2::COLLECT-RATIONAL-POLY-P-LST ACL2::STRIP-FCD-CONCLS
         ACL2::REWRITE-STACK-LIMIT ACL2::ARRAY-ETYPE-IS-FIXNUM-TYPE
         ACL2::ALL-VARS-GOALS ACL2::LIVE-STATE-SYMBOLP ACL2::KWOTE
         ACL2::BOOLEAN-HYPS-VARS ACL2::TS-INTERSECTION-FN
         ACL2::DUPLICATE-KEYSP-EQ ACL2::WORMHOLE-DATA ACL2::HONS-COPY
         ACL2::QUICK-BLOCK-INITIAL-SETTINGS ACL2::WEAK-HISTORY-ENTRY-P
         ACL2::PUSH-WARNING-FRAME ACL2::GET-SLOW-ALIST-ACTION
         ACL2::WEAK-TAU-INTERVAL-P ACL2::FIND-FIRST-FNSYMB-LST
         ACL2::STOBJ-LET-FN-RAW ACL2::MERGE-SORT-CAR-TERM-ORDER
         ACL2::SKIPPED-PROOFSP-IN-POST-ALIST
         ACL2::SIMPLIFY-TESTS-AND-CALLS-LST ACL2::BINARY-*-TREE
         ACL2::LAMBDA-KEYWORDP ACL2::TRANSITIVITY ACL2::LISTIFY
         ACL2::ASCII-CODE! ACL2::LIST-OF-THE-TYPE-SET
         ACL2::DELETE-SOMETHING ACL2::CONJOIN ACL2::IDATES
         ACL2::SER-DECODER-P ACL2::LEN ACL2::DELETE-CERT-FILES
         ACL2::32-BIT-INTEGER-STACK ACL2::AND-MACRO ACL2::RCNSTP
         ACL2::ARGLISTS-TO-NILS ACL2::TAU-INTERVAL-DOM
         ACL2::LMI-SEED-LST ACL2::GET-STRING
         ACL2::HL-FALTABLE-GET-FREE-SLOT
         ACL2::STATE-GLOBAL-LET*-PUT-GLOBALS ACL2::COMPLEX-RATIONALP
         ACL2::UPDATE-MUTUAL-RECURSION-FOR-DEFUN-NX
         ACL2::SER-ENCODE-ATOMS ACL2::ALL-TYPE-REASONING-TAGS-P1
         ACL2::FAST-ALIST-CLEAN! ACL2::LEGAL-CONSTANTP
         ACL2::CHK-WITH-GUARD-CHECKING-ARG ACL2::NULL-POOL
         ACL2::COERCE-TO-ACL2-PACKAGE-LST ACL2::HL-CACHE-CLEAR
         ACL2::THE-LIVE-VAR
         ACL2::SPLIT-ON-CONJOINED-DISJUNCTIONS-IN-HYPS-OF-PAIRS
         ACL2::ANCESTOR-LISTP ACL2::DOUBLETON-LIST-P
         ACL2::STRIP-ANCESTOR-LITERALS ACL2::ACCESS-EVENT-TUPLE-TYPE
         ACL2::HL-ADDR-HT-FULLNESS ACL2::VARIFY!
         ACL2::DECODE-TYPE-SET-LST ACL2::HIDE ACL2::WEAK-DEF-BODY-P
         ACL2::IF-TAUTOLOGYP ACL2::ALL-NILS
         ACL2::EXPUNGE-FC-DERIVATIONS ACL2::MFC-WORLD
         ACL2::DEFINE-GLOBAL-NAME ACL2::CLAUSES-RESULT
         ACL2::STRICT-SYMBOL-<-SORTEDP
         ACL2::EXPAND-TAU-LIKE-PROPOSITION ACL2::WRITTEN-FILE-LISTP
         ACL2::MAYBE-POP-UNDO-STACK ACL2::SYMBOL-ALISTP
         ACL2::BIG-CLOCK-ENTRY ACL2::NORMALIZE-ADDEND ACL2::MFC-CLAUSE
         ACL2::REMOVE-DUPLICATES-EQUAL ACL2::EQLABLEP
         ACL2::FIRST-TRACE-PRINTING-COLUMN ACL2::LAST-PROVER-STEPS
         ACL2::R-SYMBOL-ALISTP ACL2::PRINT-PROOF-TREE-FINISH
         ACL2::CONJOIN-CLAUSES ACL2::TRACE-HIDE-WORLD-AND-STATE
         ACL2::EXPANSION-ALIST-PKG-NAMES-MEMOIZE
         ACL2::NORMALIZE-POLY-LST
         ACL2::TILDE-*-CONJUNCTION-OF-POSSIBLY-FORCED-NAMES-PHRASE
         ACL2::HL-SLOW-ALIST-WARNING ACL2::ALL-CARS-NIL
         ACL2::FAST-ALIST-LEN ACL2::ALWAYS-BIGGERP-DATA-LST
         ACL2::GET-DOCS ACL2::32-BIT-INTEGER-STACK-LENGTH
         ACL2::THE-MAYBE-LIVE-VAR-BINDINGS
         ACL2::REMOVE-ASSUMPTION-ENTRIES-FROM-TYPE-ALIST
         ACL2::DECREMENT-BIG-CLOCK ACL2::MAKE-PRETTY-START-INSTR
         ACL2::OPEN-CHANNEL1 ACL2::VAR-WITH-DIVISIONP
         ACL2::FILTER-SATISFYING-FC-ACTIVATIONS ACL2::USER-STOBJSP
         ACL2::REASON-FOR-NON-KEYWORD-VALUE-LISTP
         ACL2::WEAK-BOUNDER-CORRECTNESS-P ACL2::HITS/CALLS
         ACL2::TILDE-@-ABBREVIATE-OBJECT-PHRASE ACL2::STATE-P
         ACL2::HL-INITIALIZE-FALTABLE-TABLE ACL2::GOAL-NAMES
         ACL2::LIST-MACRO ACL2::ACCESS-EVENT-TUPLE-NUMBER
         ACL2::COERCE-STATE-TO-OBJECT ACL2::PRINT-TIME-SUMMARY
         ACL2::MAKE-EVENT-CTX
         ACL2::CUSTOM-KEYWORD-HINT-IN-COMPUTED-HINT-FORM
         ACL2::FIND-?-FN ACL2::REPLACE-BAD-LISP-OBJECT-LIST
         ACL2::EXPAND-INEQUALITY-FNCALL ACL2::WEAK-ELIM-RULE-P
         ACL2::OPEN-OUTPUT-CHANNELS ACL2::MERGE-SORT-RUNES
         ACL2::STOBJ-LET-FN ACL2_*1*_ACL2::COMPLEX-RATIONALP
         ACL2_*1*_COMMON-LISP::CDR
         ACL2::INITIALIZE-SUMMARY-ACCUMULATORS
         ACL2::CHK-MACRO-ARGLIST-OPTIONAL ACL2::LEGAL-INITP
         ACL2::MAX-ABSOLUTE-EVENT-NUMBER ACL2::READ-FILES
         ACL2::WEAK-REWRITE-CONSTANT-P ACL2::ATOM-LISTP
         ACL2::PRINT-LDD-FULL-OR-SKETCH/MUTUAL-RECURSION
         ACL2::MAKE-SHARP-ATSIGN ACL2::PRETTYIFY-CLAUSE-SIMPLE
         ACL2::SER-ENCODER-STREAM ACL2::CONS-TERM-UNARY--
         ACL2::DUPLICATE-KEY-IN-KEYWORD-VALUE-LISTP
         ACL2::DIVE-INTO-MACROS-TABLE ACL2::SYMBOL-LIST-LISTP
         ACL2::DISTRIBUTE-OTHER-HINTS-INTO-OR
         ACL2::ADD-EACH-LITERAL-LST ACL2::LMI-SEED
         ACL2::DOUBLET-STYLE-SYMBOL-TO-SYMBOL-ALISTP ACL2::HL-CACHE-P
         ACL2::PRETTYIFY-XRUNE ACL2::HIDE-LAMBDAS
         ACL2::COLLECT-UNCERTIFIED-BOOKS ACL2::ALL-BUT-LAST
         ACL2::NTH-ALIASES ACL2::DISC-TREE
         ACL2::WEAK-CLAUSE-PROCESSOR-HINT-P ACL2::DEFAULT-HINTS
         ACL2::ER-PROGN-FN-CMP ACL2::EVISC-INDEXED-INSTRS ACL2::NATP
         ACL2::ALMOST-QUOTEP1-LISTP
         ACL2::ACL2-DEFAULTS-TABLE-LOCAL-CTX-P
         ACL2::REMOVE-BYES-FROM-TAG-TREE ACL2::CERT-OP
         ACL2::PAIR-VARS-WITH-LITS ACL2::SOME-SLASHABLE
         ACL2::REMOVE-ALL-NO-OPS ACL2::GUARD-CHECK-FN
         ACL2::WEAK-PROVED-FUNCTIONAL-INSTANCES-ALIST-ENTRY-P
         ACL2::ASSUMPTION-FREE-TTREEP ACL2::FAST-ALIST-FREE
         ACL2::CONTAINS-ASSUMPTIONP-FC-DERIVATIONS
         ACL2::OPEN-INPUT-CHANNELS ACL2::NONNEGATIVE-LOWER-BOUNDP
         ACL2::PAIRS-TO-MACRO-ALIAS-MSGS ACL2::GET-SIG-FNS1
         ACL2::GOOD-COEFFICIENT ACL2::IMPOSSIBLE-POLYP
         ACL2::ACCESS-LDD-MARKP ACL2::MAKE-FC-ACTIVITY-REPORT
         ACL2::PACKN1 ACL2::SHALLOW-CLAUSIFY1
         ACL2_*1*_COMMON-LISP::DENOMINATOR ACL2::WEAK-BDDNOTE-P
         ACL2::SAME-NAME-TWICE ACL2::COLLECT-ALL-VARS
         ACL2::COERCE-OBJECT-TO-STATE ACL2::TIME-TRACKER-MSG
         ACL2::MAKE-TRUE-LIST-CONS-NEST ACL2::BRR-RESULT
         ACL2::STOBJ-OUT ACL2::WEAK-ASSUMPTION-P ACL2::FILE-CLOCK
         ACL2::BINDS-TO-CONSTANTS-P ACL2::STEP-LIMIT-STRICTP
         ACL2::TERM-IGNORE-OKP ACL2::PREPROCESS-HYPS ACL2::FC-REPORT
         ACL2::GAG-MODE-JPPL-FLG ACL2::NON-GEN-VAR-MARKERS
         ACL2::UNTRANSLATE-CAR-CDR-NEST ACL2::MFC-RDEPTH
         ACL2::CLOSE-VALUE-SETS ACL2::HL-ALIST-STOLEN-WARNING
         ACL2::DEFUN-FOR-STATE-NAME ACL2::TILDE-@-BDDNOTE-PHRASE
         ACL2::FIND-?-MEASURE ACL2_*1*_COMMON-LISP::SYMBOLP
         ACL2::LEGAL-VARIABLEP ACL2::SYSFILE-P ACL2::ACCESS-LDD-FULLP
         ACL2::ARITY-ALISTP ACL2::LMI-TECHS
         ACL2::INVERT-ABBREVIATIONS-ALIST ACL2::IF-INTERP-SWITCH
         ACL2::CHK-STATE-OK-MSG ACL2::KWOTE-LST
         ACL2::HL-FALTABLE-CLEAR-CACHE ACL2::PRIMORDIAL-WORLD-GLOBALS
         ACL2::SYMMETRY ACL2::WEAK-BIG-SWITCH-RULE-P
         ACL2::MAKE-INITIAL-GOAL ACL2::TT-STOP
         ACL2::WARN-FOR-GUARD-BODY ACL2::UNARY--
         ACL2::EXPAND-EQ-AND-ATOM-TERM-LST ACL2::PLAUSIBLE-DCLSP1
         ACL2::GET-DECLARED-STOBJS ACL2::TAU-EMPTY-INTERVALP
         ACL2::WEAK-HCOMP-BOOK-HT-ENTRY-P
         ACL2::MAYBE-SET-RW-CACHE-STATE-DISABLED ACL2::ASSIGN-LOCK
         ACL2::DIRECTORY-OF-ABSOLUTE-PATHNAME
         ACL2::SOME-SLOT-HAS-MULTIPLE-TAU-SIGS
         ACL2::EVALUATE-GROUND-POLY ACL2::DEFSTUB-BODY
         ACL2::IRRELEVANT-LITS
         ACL2::ASSUMNOTE-LIST-LIST-TO-CLAUSE-ID-LIST-LIST
         ACL2::STRING-FOR-TILDE-@-CLAUSE-ID-PHRASE
         ACL2::INDEX-OF-NON-NUMBER ACL2::SWEEP-CLAUSES ACL2::O-FINP
         ACL2::TYPE-ALISTP ACL2::NAT-LISTP ACL2::EXPAND-ASSUMPTIONS-1
         ACL2::TT-END ACL2::MACRO-ARGLIST-OPTIONALP
         ACL2::KEYWORD-VALUE-LISTP ACL2::ACCESS-COMMAND-TUPLE-CBD
         ACL2_*1*_ACL2::PKG-IMPORTS ACL2::WRITABLE-FILE-LISTP1
         ACL2::FIND-PKG-WITNESS ACL2::LEAF-CST-LIST-TO-ALIST
         ACL2::ACCESS-COMMAND-TUPLE-NUMBER ACL2::ALIST-TO-BINDINGS
         ACL2::WEAK-GENERALIZE-RULE-P
         ACL2::TRANSLATED-ACL2-UNWIND-PROTECTP
         ACL2::WEAK-TYPE-SET-INVERTER-RULE-P ACL2::GET-BODIES
         ACL2::SYMBOL-DOUBLET-LISTP ACL2::SUBST-EXPR-ERROR
         ACL2::REMOVE-DUPLICATES-EQ-EXEC
         ACL2::PRINT-CLAUSE-ID-OKP-BUILTIN ACL2::IPRINT-LAST-INDEX*
         ACL2::DELETE-AUXILIARY-BOOK-FILES ACL2::ER-PROGN-FN
         ACL2::NUMBER-SUBTREES ACL2::RAW-INCLUDE-BOOK-DIR-P
         ACL2::MACRO-VARS ACL2::POOL-LST ACL2::DUPLICATE-KEYSP
         ACL2::FIRST-KEYWORD ACL2::HL-HSPACE-HONS-SUMMARY
         ACL2::CURRENT-FC-CALL-NUMBER ACL2::WEAK-TESTS-AND-CALLS-P
         ACL2::T-STACK-LENGTH1 ACL2::TILDE-*-OR-HIT-SUMMARY-PHRASE1
         ACL2::GET-STOBJS-OUT-FOR-DECLARE-FORM
         ACL2_*1*_COMMON-LISP::CAR ACL2::SPLICED-INSTR-LISTP
         ACL2::ACCESS-LDD-FORM ACL2::NO-OP-HISTP
         ACL2::GET-PARENT-DIRECTORY ACL2::FLATTEN-ANDS-IN-LIT
         ACL2::FLUSH-HONS-GET-HASH-TABLE-LINK ACL2::ACCESS-LDD-CLASS
         ACL2::NEXT-ABSOLUTE-EVENT-NUMBER ACL2::KNOWN-PACKAGE-ALISTP
         ACL2::TERMIFY-CLAUSE-SET ACL2::LAMBDA-SUBTERMP
         ACL2::IDENTITY-INTERVALP ACL2::READ-FILE-LISTP1
         ACL2::RECORD-MAKER-FUNCTION-NAME ACL2::MACRO-VARS-AFTER-REST
         ACL2::STANDARD-STRING-ALISTP
         ACL2::RESTORE-IPRINT-AR-FROM-WORMHOLE ACL2::LARGE-CONSP
         ACL2::IMPOSSIBLE-POLY ACL2::FORMAL-BINDINGS
         ACL2::ALL-VARS-IN-POLY-LST ACL2::MERGE-SORT-CADR-<
         ACL2::LAMBDA-SUBTERMP-LST ACL2::POSP
         ACL2::SCAN-TO-CLTL-COMMAND ACL2::MAYBE-ADD-SEPARATOR
         ACL2::ABBREVIATE-HYPHENATED-STRING ACL2::HONS-GENTEMP
         ACL2::COERCE-INDEX ACL2::IPRINT-VIRGINP
         ACL2::SET-WATERFALL-PARALLELISM-HACKS-ENABLED-GUARD
         ACL2::TAG-TREE-OCCUR-ASSUMPTION-NIL-1
         ACL2::HL-HSPACE-HONSP-WRAPPER
         ACL2::32-BIT-INTEGER-STACK-LENGTH1 ACL2::GETPROPS1
         ACL2::MEMBER-NIL-NEG-EVGS ACL2::NEW-VERIFY-GUARDS-FNS
         ACL2_*1*_COMMON-LISP::STRINGP ACL2::WEAK-POLY-P
         ACL2::ACL2-RAW-EVAL-FORM-TO-EVAL ACL2::WEAK-PEQUIV-PATTERN-P
         ACL2::WEAK-LINEAR-POT-P ACL2::RW-CACHE-ENTER-CONTEXT
         ACL2::COLLECT-IDEAL-USER-DEFUNS ACL2::DEFAULT-DEFUN-MODE
         ACL2::MERGE-SORT-LEXORDER-FAST ACL2::PRETTYIFY-STOBJS-OUT
         ACL2::MAKE-RECORD-FIELD-LST ACL2::DUMB-NEGATE-LIT-LST
         ACL2::FMT-CONTROL-BINDINGS ACL2::DECODE-TYPE-SET
         ACL2::APPEND-LST ACL2::WORMHOLE-STATUSP ACL2::ACL2-NUMBERP
         ACL2::CLEAR-ONE-MEMO-AND-PONS-HASH ACL2::SYSFILE-FILENAME
         ACL2::TILDE-*-BAD-INSIGS-PHRASE1 ACL2::NEW-NUMES
         ACL2::CASE-LIST-CHECK ACL2::READABLE-FILE
         ACL2::SCAN-TO-COMMAND ACL2::SYMBOL-LISTP
         ACL2::PUSH-INHIBIT-OUTPUT-LST-STACK ACL2::WEAK-POOL-ELEMENT-P
         ACL2::RAW-SOURCE-NAME-P ACL2::ALL-ATTACHMENTS
         ACL2::ACL2-NUMBER-LISTP ACL2::NEXT-TAG ACL2::TRUE-LISTP
         ACL2::HONS-CLEAR ACL2::SORT-RW-CACHE-LIST
         ACL2::STRIP-ASSUMPTION-TERMS ACL2::MAYBE-PRINT-CALL-HISTORY
         ACL2::WEAK-STATE-VARS-P ACL2_*1*_ACL2::UNARY--
         ACL2::FIND-FIRST-VAR ACL2::FORCE ACL2::HL-FALTABLE-P
         ACL2::UNTRANS-TABLE ACL2::PRETTYIFY-STOBJ-FLAGS
         ACL2::REDUNDANT-PREDEFINED-ERROR-MSG ACL2::SIGNATURE-FNS
         ACL2::DUPLICATE-VARS ACL2::SILLY-POLYP
         ACL2::COLLECT-ABBREVIATION-SUBCLASS
         ACL2::FIND-EQUATIONAL-POLY-RHS ACL2::WEAK-LDD-STATUS-P
         ACL2::TRACE$-ER-MSG ACL2::TAU-SYSTEM
         ACL2::MACRO-ARGLIST-AFTER-RESTP ACL2::STRIP-CADRS
         ACL2::COND-MACRO ACL2::STEP-LIMIT-START
         ACL2::ALIST-TO-THE-FOR-*1*-LST ACL2::ODDS ACL2::MACRO-VARS-KEY
         ACL2::NORMALIZE-RW-ANY-CACHE ACL2::FIND-FIRST-NON-NIL
         ACL2::FN-SYMB ACL2::WEAK-SAR-P ACL2::WITH-GUARD-CHECKING-GATE
         ACL2::CONVERT-BOOK-NAME-TO-ACL2X-NAME ACL2::SER-DECODE-MAGIC
         ACL2::CHK-MACRO-ARGLIST-AFTER-REST ACL2::HL-ADDR-LIMIT-ACTION
         ACL2::STRIP-CDDRS ACL2::TTAGS-FROM-DEFERRED-TTAG-NOTES1
         ACL2::UNTRANSLATE-PREPROCESS-FN ACL2::CHAR-LIST-FRACTION
         ACL2::CASE-SPLIT-LIMITATIONS ACL2::TAU-BIG-SWITCH-VAR
         ACL2::MAKE-OFFICIAL-PC-INSTR ACL2::EV-FNCALL-CREATOR-ER-MSG
         ACL2::DEFSTOBJ-RAW-INIT ACL2::ULTIMATE-EXPANSION
         ACL2::SORT-ARITH-TERM-ORDER ACL2::RUNES-TO-CLASS-ALIST
         ACL2::CLEAR-MEMOIZE-TABLE ACL2::ACL2-MAGIC-CANONICAL-PATHNAME
         ACL2::QUOTE-LISTP ACL2::O-RST ACL2::BDD-CONSTRUCTORS
         ACL2::GC-OFF ACL2::CLOAKING-DEVICE-HINT ACL2::ALL-KEYWORDS-P
         ACL2::KNOWN-PACKAGE-ALIST ACL2::WEAK-GOAL-TREE-P
         ACL2::DOUBLE-REWRITE ACL2::SER-ENCODER-P ACL2::FIX
         ACL2::WEAK-MEMO-MAX-SIZES-ENTRY-P
         ACL2::WEAK-ATTACHMENT-COMPONENT-P
         ACL2_*1*_COMMON-LISP::NUMERATOR
         ACL2::TTAGS-FROM-DEFERRED-TTAG-NOTES
         ACL2::SET-FORMS-FROM-BINDINGS ACL2::SOME-PROGRAM-DECLARED-P
         ACL2::ACCESS-EVENT-TUPLE-FORM ACL2::TILDE-*-SIMP-PHRASE
         ACL2::LMI-TECHS-LST ACL2::RW-CACHEABLE-FAILURE-REASON-BUILTIN
         ACL2::CHARS-FOR-TILDE-@-CLAUSE-ID-PHRASE/PERIODS
         ACL2::DEFUN-MODE-STRING ACL2::STRIP-CDRS
         ACL2::OUTSIDE-CALLER-P ACL2::MERGE-SORT-ALPHA-<
         ACL2::NORMALIZE-LINEAR-SUM-2
         ACL2::NO-DUPLICATESP-EQ-EXEC$GUARD-CHECK
         ACL2::REMOVE-ANCESTOR-LITERALS-FROM-PAIRS
         ACL2::WEAK-STEP-LIMIT-RECORD-P ACL2::REWRITE-RULE-TO-BDD-RULE
         ACL2::GOOD-POT-VARP ACL2::FIND-FIRST-VAR-LST
         ACL2::WEAK-ANCESTOR-P ACL2::STRING-LISTP ACL2::GOOD-POLYP
         ACL2::ACCESS-EVENT-TUPLE-SKIPPED-PROOFS-P
         ACL2::THE-LIVE-VAR-BINDINGS ACL2::FREE-VARS-DISPLAY-LIMIT
         ACL2::TILDE-@-CLAUSE-ID-PHRASE ACL2::WEAK-CERT-OBJ-P
         ACL2::EVG-TYPE ACL2::MACRO-ALIASES
         ACL2::WEAK-CURRENT-LITERAL-P ACL2::DEFAULT-RULER-EXTENDERS
         ACL2::SKIP-PROOF-TREE-TIME ACL2::SHOW-POLY
         ACL2_*1*_COMMON-LISP::CHAR-CODE ACL2::PONS-ADDR-OF-ARGUMENT
         ACL2::MAKE-IDENTITY-FOR-@PAR-MAPPINGS ACL2::STRING-APPEND-LST
         ACL2::CASE-SPLIT ACL2::DUMB-NEGATE-LIT-LST-LST
         ACL2::INITIALIZE-INVARIANT-RISK ACL2::WEAK-CANDIDATE-P
         ACL2::GET-NEXT-NUME ACL2::MAKE-FAST-ALIST ACL2::DEFABBREV1
         ACL2::ALL-SYMBOLS ACL2::OPTIMIZE-ALISTP
         ACL2::REMOVE-CURRENT-ACL2-WORLD-KEY
         ACL2::MERGE-SORT-SYMBOL-ALISTP
         ACL2::NORMALIZE-ALLEGED-EVALUATOR-CLAUSE
         ACL2::LEGAL-CASE-CLAUSESP ACL2::REMOVE-GUARD-HOLDERS-LST-LST
         ACL2::CL-SET-TO-IMPLICATIONS ACL2::SYMBOL-NAME-LST
         ACL2::TIME-TRACKER-P ACL2::NEXT-ABSOLUTE-COMMAND-NUMBER
         ACL2::SER-DECODER-VERSION ACL2_*1*_COMMON-LISP::SYMBOL-NAME
         ACL2::THEORY-FN-CALLP ACL2::FAST-ALIST-CLEAN
         ACL2::ALL-PICKS-SIZE ACL2::PROVER-STEPS
         ACL2::ABBREV-EVISC-TUPLE ACL2::EXPORTED-FUNCTION-NAMES
         ACL2::WEAK-COMMAND-TUPLE-P ACL2::CLEAR-TEMP-TOUCHABLE-VARS
         ACL2::WRITTEN-FILE ACL2::MEMOIZE-FLUSH1
         ACL2::FIND-FIRST-FNSYMB ACL2::OK-TO-FORCE-ENS
         ACL2::BOOT-TRANSLATE ACL2::GET-SHARP-ATSIGN
         ACL2::WEAK-RW-CACHE-ENTRY-P ACL2::TAU-GET-STATS
         ACL2::T-STACK-LENGTH ACL2::O-FIRST-EXPT
         ACL2::UPDATE-MUTUAL-RECURSION-FOR-DEFUN-NX-1
         ACL2::PARSE-INFIX-FROM-TERMINAL ACL2::TIME-FOR-NON-HITS/CALL
         ACL2::ARRAY-ORDER ACL2::DMR-START-FN-RAW
         ACL2::DEFSTOBJ-RAW-INIT-FIELDS ACL2::T-STACK
         ACL2::SINGLE-VALUED-SYMBOLP-ALISTP ACL2_*1*_ACL2::UNARY-/
         ACL2::CREATE-LIVE-USER-STOBJP-TEST ACL2::IGNORABLE-VARS
         ACL2::ALL-UNRESTRICTED-SIGNATURE-RULESP ACL2::RW-CACHE
         ACL2::STOBJ-PRINT-NAME ACL2::USER-STOBJ-ALIST
         ACL2::CAAR-IS-DECLAREP ACL2::DECLARE-GRANULARITY-P
         ACL2::STRING-UPCASE1 ACL2::UNPRETTYIFY
         ACL2::FIND-EQUATIONAL-POLY-RHS1 ACL2::BAD-ATOM
         ACL2::TILDE-@-ILLEGAL-VARIABLE-OR-CONSTANT-NAME-PHRASE
         ACL2::ASSOC-EQ-EQUAL-ALISTP ACL2::PROPER-CONSP
         ACL2::CLAUSE-ID-P ACL2::NON-LINEARP ACL2::SHOW-TTAG-NOTES-FN
         ACL2::STATE-GLOBAL-LET*-BINDINGS-P ACL2::CONS-TERM1-CASES
         ACL2::INITIALIZE-TIMERS ACL2::STANDARD-EVISC-TUPLEP
         ACL2::MACRO-VARS-OPTIONAL ACL2::CHK-MACRO-ARGLIST1
         ACL2::WEAK-FORWARD-CHAINING-RULE-P ACL2::COUNT-IFS-LST
         ACL2::WEAK-CLAUSE-ID-P ACL2::GLOBAL-TABLE-CARS
         ACL2::MACRO-ARGS-STRUCTUREP ACL2::GENERATE-@PAR-MAPPINGS
         ACL2::REMOVE-DUPLICATES-EQL-EXEC ACL2::EVG-FN-SYMB
         ACL2::POP-INHIBIT-OUTPUT-LST-STACK ACL2::DCL-FIELDS
         ACL2::READABLE-FILES-P ACL2::O<G ACL2::MACRO-MINIMAL-ARITY1
         ACL2::FIXNUM-TO-SYMBOL ACL2::INTEGER-ABS ACL2::WEAK-GAG-INFO-P
         ACL2::GET-CHECK-INVARIANT-RISK
         ACL2::SAFE-ACCESS-COMMAND-TUPLE-FORM ACL2::MAKE-SPACES-ARRAY
         ACL2::CLEAR-TEMP-TOUCHABLE-FNS ACL2::GOAL-TERMS
         ACL2::CHK-WITH-PROVER-TIME-LIMIT-ARG ACL2::DUMB-EVAL
         ACL2::EVAL-TYPE-SET ACL2::CBD-FN ACL2::COND-LENGTH
         ACL2::VARIFY ACL2::STRIP-NUMERIC-POSTFIX
         ACL2::32-BIT-INTEGER-LISTP
         ACL2::MINIMALLY-WELL-FORMED-OR-HINTP ACL2::EXPAND-ASSUMPTIONS
         ACL2::CANCEL-DOT-DOTS ACL2::SYMBOL-TO-FIXNUM
         ACL2::O-FIRST-COEFF ACL2::PRINT-LIST-WITHOUT-STOBJ-ARRAYS
         ACL2::DEFAULT-WELL-FOUNDED-RELATION ACL2::STATE-P1
         ACL2::WATERFALL-PRINTING-VALUE-FOR-PARALLELISM-VALUE
         ACL2::PROCESS-DEFABBREV-DECLARES ACL2::NUMBER-OF-STRINGS
         ACL2::COMPILED-FUNCTION-P! ACL2::ABBREVIATIONS-ALIST
         ACL2::R-EQLABLE-ALISTP ACL2::WRITTEN-FILES-P ACL2::AND-LIST
         ACL2::SYMBOL-CLASS-CHAR ACL2::UNPRETTYIFY-STOBJ-FLAGS
         ACL2::MOVE-CURRENT-ACL2-WORLD-KEY-TO-FRONT
         ACL2::DEFUN-MODE-PROMPT-STRING ACL2::EXTRA-INFO-LIT-P
         ACL2::TAU-INTERVALP ACL2::ABBREVIATIONS-ALIST-?
         ACL2::GET-DIRECTORY-OF-FILE
         ACL2::UNMARK-AND-DELETE-LOCAL-INCLUDED-BOOKS ACL2::INVERT-VAR
         ACL2::PSEUDO-TERM-LISTP ACL2::INITIALIZE-BRR-STACK
         ACL2::32-BIT-INTEGERP ACL2::DUMB-EVAL-YIELDS-QUOTEP
         ACL2::MAKE-RECORD-RECOGNIZER-BODY ACL2::MFC-TYPE-ALIST
         ACL2::SYMBOL-LIST-TO-PACKAGE-ALIST
         ACL2::TILDE-*-IRRELEVANT-FORMALS-MSG
         ACL2::INFO-FOR-WELL-FOUNDED-RELATION-RULES
         ACL2::MACRO-ARGLIST1P ACL2::RATIONAL-LISTP)) 
(COMMON-LISP::PROCLAIM
    '(COMMON-LISP::FTYPE
         (COMMON-LISP::FUNCTION (COMMON-LISP::*) COMMON-LISP::*)
         ACL2::REMEMOIZE-ALL ACL2::LP)) 
(COMMON-LISP::PROCLAIM
    '(COMMON-LISP::FTYPE
         (COMMON-LISP::FUNCTION (COMMON-LISP::FIXNUM)
             COMMON-LISP::FIXNUM)
         ACL2::DOUBLE-MOD-M31 ACL2::TIMES-EXPT-2-16-MOD-M31)) 
(COMMON-LISP::PROCLAIM
    '(COMMON-LISP::FTYPE
         (COMMON-LISP::FUNCTION (COMMON-LISP::INTEGER)
             COMMON-LISP::FIXNUM)
         ACL2::FCHECKSUM-NATURAL)) 
(COMMON-LISP::PROCLAIM
    '(COMMON-LISP::FTYPE
         (COMMON-LISP::FUNCTION (COMMON-LISP::T) ACL2::HL-CACHE)
         ACL2::HL-HSPACE-NORM-CACHE)) 
(COMMON-LISP::PROCLAIM
    '(COMMON-LISP::FTYPE
         (COMMON-LISP::FUNCTION (COMMON-LISP::T) COMMON-LISP::BOOLEAN)
         ACL2::HL-FALTABLE-EJECT1 ACL2::HL-FALSLOT-UNIQUEP)) 
(COMMON-LISP::PROCLAIM
    '(COMMON-LISP::FTYPE
         (COMMON-LISP::FUNCTION (COMMON-LISP::T) COMMON-LISP::*)
         ACL2::KEEP-TMP-FILES ACL2::PC-PRINT-MACROEXPANSION-FLG-FN
         ACL2::WORMHOLE-P ACL2::EXTRACT-BOUNDS
         ACL2::TERM-EQUATED-TO-CONSTANT ACL2::READ-RUN-TIME
         ACL2::DESTRUCTURE-WELL-FOUNDED-RELATION-RULE
         ACL2::DESTRUCTURE-COMPOUND-RECOGNIZER ACL2::ATTACHMENT-SYMBOL
         ACL2::INITIALIZE-PC-ACL2 ACL2::MONITORED-RUNES-FN
         ACL2::LD-ERROR-TRIPLES ACL2::UNPRETTYIFY-TP
         ACL2::WALKABOUT-HUH ACL2::LD-LOOP ACL2::W ACL2::READ-IDATE
         ACL2::STANDARD-CO ACL2::DESTRUCTURE-CLAUSE-PROCESSOR-RULE
         ACL2::LD-PRE-EVAL-FILTER ACL2::PC-PROMPT-FN
         ACL2::EXIT-BRR-WORMHOLE ACL2::WRITE-FOR-READ
         ACL2::FNS-DIFFERENT-WRT-ACL2-LOOP-ONLY
         ACL2::HCOMP-BUILD-FROM-STATE ACL2::LD-MISSING-INPUT-OK
         ACL2::REMOVE-GUARD-HOLDERS1-LST-LST ACL2::IF-HT-MAX-LENGTH
         ACL2::PC-PROMPT-DEPTH-PREFIX-FN ACL2::*1*-SYMBOL?
         ACL2::LD-REDEFINITION-ACTION ACL2::DEBUGGER-ENABLE
         ACL2::REMOVE-TYPE-DCLS ACL2::INTERPRET-TERM-AS-META-RULE
         ACL2::LD-READ-EVAL-PRINT ACL2::PARSE-VERSION ACL2::OOPS-FN
         ACL2::DISABLE-IPRINT-AR ACL2::PRINT-CLAUSE-ID-OKP
         ACL2::FMT-HARD-RIGHT-MARGIN
         ACL2::STRIP-NON-REWRITTENP-ASSUMPTIONS ACL2::SET-RAW-MODE-ON
         ACL2::LD-READ-EVAL-PRINT-SIMPLE ACL2::EXIT-BRR
         ACL2::RAW-MODE-P ACL2::UBT-PREHISTORY-FN
         ACL2_*1*_ACL2::SYMBOL-PACKAGE-NAME ACL2::LD-ERROR-ACTION
         ACL2::PARSE-WITH-LOCAL-STOBJ ACL2::SILENT-ERROR
         ACL2::CHK-DEFMACRO-WIDTH ACL2::LD-LOOP-SIMPLE
         ACL2::TERM-EQUATED-TO-CONSTANT-IN-TERMLIST
         ACL2::LD-POST-EVAL-PRINT ACL2::ENS
         ACL2::DESTRUCTURE-FORWARD-CHAINING-TERM ACL2::OP-HT-MAX-LENGTH
         ACL2::SPLIT-AT-FIRST-KEYWORD ACL2::STANDARD-OI
         ACL2::W-OF-ANY-STATE ACL2::REMOVE-GUARD-HOLDERS1-LST
         ACL2::FMT-SOFT-RIGHT-MARGIN ACL2::LD-PRINT-PROMPT
         ACL2::PC-PRINT-PROMPT-AND-INSTR-FLG-FN ACL2::NEVER-MEMOIZE-P
         ACL2::LD-RETURN-ERROR ACL2::GC-STRATEGY
         ACL2::DESTRUCTURE-EXPANSION
         ACL2::TRANSLATED-ACL2-UNWIND-PROTECTP4 ACL2::CPU-CORE-COUNT
         ACL2::REPLAY-QUERY ACL2::PARTITION-REST-AND-KEYWORD-ARGS1
         ACL2::NORMALIZE-LINEAR-SUM ACL2::RW-CACHEABLE-FAILURE-REASON
         ACL2::*1*-SYMBOL ACL2::LD-SKIP-PROOFSP ACL2::SYS-CALL-STATUS
         ACL2::STRIP-FINAL-DIGITS ACL2::ENS-MAYBE-BRR
         ACL2::CURRENT-PACKAGE ACL2::PRINT-PC-PROMPT
         ACL2::IPRINT-HARD-BOUND ACL2::LD-PROMPT
         ACL2::MAYBE-ADD-EVENT-LANDMARK ACL2::SPLIT-IMPLIES
         ACL2::READ-ACL2-ORACLE@PAR
         ACL2::CHECK-AND-PARSE-FOR-GRANULARITY-FORM
         ACL2::LD-READ-COMMAND ACL2::LIST-ALL-PACKAGE-NAMES
         ACL2::GET-DECLAIM-LIST ACL2::STRIP-FINAL-DIGITS1
         ACL2::FIND-FIRST-BAD-ARG ACL2::SER-ENCODE-FALS
         ACL2::PARSE-STOBJ-LET ACL2::SPLIT-PSORTED-LIST
         ACL2::MAIN-TIMER ACL2::LD-PRE-EVAL-PRINT
         ACL2_*1*_ACL2::PKG-WITNESS ACL2::IPRINT-SOFT-BOUND
         ACL2::EXIT-LD ACL2::GET-SERIALIZE-CHARACTER
         ACL2::LD-QUERY-CONTROL-ALIST ACL2::READ-ACL2-ORACLE
         ACL2::LD-VERBOSE ACL2::SET-RAW-MODE-OFF ACL2::READ-STANDARD-OI
         ACL2::?-FN ACL2::ENABLE-IPRINT-AR ACL2::PROOFS-CO)) 
(COMMON-LISP::PROCLAIM
    '(COMMON-LISP::FTYPE
         (COMMON-LISP::FUNCTION (COMMON-LISP::*) COMMON-LISP::T)
         ACL2::HL-FALTABLE-INIT ACL2::MAKE-CLOAKING-DEVICE
         ACL2::INTERFACE-ER ACL2::HL-FALTABLE-INIT-RAW ACL2::MEMINFO
         ACL2::HL-HSPACE-INIT ACL2::MEMOIZED-VALUES
         ACL2::MAKE-SER-ENCODER ACL2::DMR-FLUSH ACL2::MAKE-HL-CACHE
         ACL2::DMR-FLUSH1 ACL2::HL-MHT-FN ACL2::INITIALIZE-ACL2
         ACL2::HL-HSPACE-INIT-RAW ACL2::MAKE-TIME-TRACKER
         ACL2::MAKE-HL-FALSLOT ACL2::MEMSTAT ACL2::MAKE-SER-DECODER
         ACL2::MEMOIZE-CALL-ARRAY-GROW)) 
(COMMON-LISP::PROCLAIM
    '(COMMON-LISP::FTYPE
         (COMMON-LISP::FUNCTION (COMMON-LISP::T) ACL2::HL-FALTABLE)
         ACL2::HL-HSPACE-FALTABLE)) 
(COMMON-LISP::PROCLAIM
    '(COMMON-LISP::FTYPE
         (COMMON-LISP::FUNCTION (COMMON-LISP::T COMMON-LISP::T)
             (COMMON-LISP::VALUES COMMON-LISP::T COMMON-LISP::T))
         ACL2::MAKE-INPUT-CHANNEL ACL2::MAKE-OUTPUT-CHANNEL
         ACL2::SYMBOL-CONSTANT-FN)) 
(COMMON-LISP::PROCLAIM
    '(COMMON-LISP::FTYPE
         (COMMON-LISP::FUNCTION
             (COMMON-LISP::T COMMON-LISP::T COMMON-LISP::T
                 COMMON-LISP::T)
             COMMON-LISP::*)
         ACL2::HIDDEN-DEFPKG-EVENTS ACL2::BAD-SYNP-HYP-MSG1
         ACL2::CHECK-CERTIFICATE-FILE-EXISTS ACL2::UBT-UBU-FN1
         ACL2::GET-STOBJS-IN-LST ACL2::CHEAP-TYPE-ALIST-AND-POT-LST
         ACL2::REMOVE-UNTOUCHABLE-FN ACL2::EXPAND-PERMISSION-RESULT1
         ACL2::ONE-WAY-UNIFY1-TERM-ALIST ACL2::CHK-XARGS-KEYWORDS
         ACL2::TYPE-SET-RECOGNIZER ACL2::PC-PROCESS-ASSUMPTIONS
         ACL2::CHK-EVALUATOR ACL2::APPLY-CASES-HINT-CLAUSE
         ACL2::TRANSLATE-ABB ACL2::WRAP1-AUX1
         ACL2::TRANSLATE-GENERALIZE-ALIST-1 ACL2::FILTER-ABSSTOBJS
         ACL2::CRUNCH-CLAUSE-SEGMENTS2 ACL2::MACROEXPAND1-CMP
         ACL2::CHK-DEFABSSTOBJ-GUARD ACL2::SUBLIS-FN-REC
         ACL2::M&M-SEARCH ACL2::MAYBE-RESET-DEFAULTS-TABLE1
         ACL2::FN-AND-MAXIMAL-LEVEL-NO ACL2::CHK-ARGLIST-FOR-DEFCHOOSE
         ACL2::TYPE-SET-EQUAL ACL2::GUARD-OBLIGATION ACL2::ERROR1
         ACL2::MACROEXPAND1* ACL2::ENCAPSULATE-CONSTRAINT
         ACL2::WRITE-ACL2X-FILE ACL2::PARSE-NATURAL
         ACL2::COMMENT-ON-NEW-RECOG-TUPLE1 ACL2::MAXIMAL-MULTIPLES1
         ACL2::MACROEXPAND1*-CMP ACL2::TAU-VISIT-DEFUNS ACL2::TOUCH?
         ACL2::EVAL-THEORY-EXPR ACL2::EXTEND-ATTACHMENT-RECORD
         ACL2::TRANSLATE-NONLINEARP-HINT
         ACL2::CHK-ACCEPTABLE-VERIFY-GUARDS ACL2::PROCESS-ASSUMPTIONS
         ACL2::DEFATTACH-UNKNOWN-CONSTRAINTS-ERROR ACL2::POP-CLAUSE
         ACL2::LD-FN1 ACL2::ACL2-QUERY1 ACL2::TRANSLATE-RESTRICT-HINT
         ACL2::CHK-THEORY-INVARIANT ACL2::CHK-CERTIFY-BOOK-STEP-3
         ACL2::TAU-NEAR-SUBSETP ACL2::WRITE-PORT-FILE ACL2::PC-MAIN1
         ACL2::SUPERIOR-COMMAND-WORLD ACL2::CHK-ARGLIST-CMP
         ACL2::CHECK-TRANSLATED-OVERRIDE-HINT
         ACL2::UPDATE-ATTACHMENT-RECORDS1
         ACL2::APPLY-CONJUNCTIVE-TAU-RULE ACL2::CHK-MUTUAL-RECURSION
         ACL2::GAG-STATE-EXITING-CL-ID ACL2::TRANSLATE-MEASURES
         ACL2::PRINT-DEFUN-MSG/TYPE-PRESCRIPTIONS1 ACL2::DEFSTOBJ-FN
         ACL2::REMOVE-?S ACL2::TYPE-SET-AND-RETURNED-FORMALS-LST
         ACL2::THM-FN ACL2::UNHIDDEN-LIT-INFO
         ACL2::CHK-ACCEPTABLE-DEFUNS0 ACL2::GET-MEASURES1
         ACL2::GET-DECLARED-STOBJ-NAMES ACL2::EVAL-BREAK-CONDITION
         ACL2::TRANSLATE-HANDS-OFF-HINT
         ACL2::CANCEL-POLY-AGAINST-ALL-POLYS ACL2::UNTRANSLATE-CONS1
         ACL2::MONITOR1 ACL2::CHK-NON-EXECUTABLEP
         ACL2::SERIALIZE-READ-FN ACL2::TRANSLATE-NO-OP-HINT
         ACL2::CHK-BOOK-NAME ACL2::PUFF-INCLUDE-BOOK
         ACL2::CHK-FLET-DECLARATIONS
         ACL2::TRANSLATE-CASE-SPLIT-LIMITATIONS-HINT
         ACL2::CHK-ACCEPTABLE-DEFUNS ACL2::APPLY-CONJUNCTIVE-TAU-RULES
         ACL2::EXTEND-CURRENT-THEORY ACL2::PR-BODY ACL2::CHK-SIGNATURE
         ACL2::APPROVE-FC-DERIVATIONS
         ACL2::SWEEP-SYMBOL-BINDING-FOR-BAD-SYMBOL
         ACL2::TRANSLATE-ERROR-HINT
         ACL2::CHK-ACCEPTABLE-DEFUNS-VERIFY-GUARDS-ER
         ACL2::CHK-WELL-FORMED-TTAGS ACL2::COMP-FN
         ACL2::TRANSLATE-EXPAND-HINT ACL2::ADD-CUSTOM-KEYWORD-HINT-FN
         ACL2::TRANSLATE-FUNCTIONAL-SUBSTITUTION ACL2::MFC-TS-RAW
         ACL2::ADJUST-LOWER-BOUND-WITH-NEG-EVGS
         ACL2::ONE-WAY-UNIFY1-TERM-ALIST-LST
         ACL2::TYPE-ALIST-EQUALITY-LOOP ACL2::COMPILE-FOR-INCLUDE-BOOK
         ACL2::CHK-ALL-BUT-NEW-NAME-CMP ACL2::PARSE-NATURAL1
         ACL2::TRANSLATE-DO-NOT-INDUCT-HINT ACL2::APPLY-REORDER-HINT
         ACL2::CHK-ACCEPTABLE-VERIFY-TERMINATION ACL2::PROGN-FN1
         ACL2::FILTER-WITH-AND-WITHOUT ACL2::GET-NORMALIZEPS
         ACL2::MODIFIED-ERROR-TRIPLE-FOR-SEQUENCE
         ACL2::TRANSLATE-HANDS-OFF-HINT1 ACL2::CHANGE-INCLUDE-BOOK-DIR
         ACL2::TYPE-ALIST-EQUALITY-LOOP1 ACL2::DEFEXEC-EXTRACT-KEY
         ACL2::DEFATTACH-ERASE ACL2::MFC-TS-TTREE
         ACL2::CHK-STOBJS-OUT-BOUND ACL2::TRANSLATE-NO-THANKS-HINT
         ACL2::GENERALIZE-RULE-SEGMENT ACL2::TABLE-FN
         ACL2::ENCAPSULATE-FN ACL2::ER-DECODE-LOGICAL-NAME
         ACL2::POST-ALIST-FROM-CHANNEL
         ACL2::ELIDE-LOCALS-AND-SPLIT-EXPANSION-ALIST
         ACL2::TRANSLATE-CLAUSE-PROCESSOR-HINT
         ACL2_*1*_ACL2::MFC-TS-TTREE
         ACL2::TRANSLATE-RW-CACHE-STATE-HINT ACL2::CHK-MACRO-ARGLIST
         ACL2::CHK-BOOT-STRAP-REDEFINEABLE-NAMEP
         ACL2::TAU-VISIT-DEFUNS1 ACL2::COPY-PCERT0-TO-PCERT1
         ACL2::INTERPRET-TERM-AS-REWRITE-RULE1 ACL2::DEFCONST-FN1
         ACL2::GET-RULER-EXTENDERS-LST
         ACL2::MAYBE-RESET-DEFAULTS-TABLE2 ACL2::HYPS-TYPE-ALIST
         ACL2::CRUNCH-CLAUSE-SEGMENTS1 ACL2::EV-SYNP
         ACL2::TYPE-SET-COMPLEX ACL2::TRANS-EVAL ACL2::GET-NORMALIZEP
         ACL2::PL2-FN ACL2::TRANSLATE-SIMPLE-OR-ERROR-TRIPLE
         ACL2::REVERT-GOAL-TREE-LST ACL2::TRANSLATE-INDUCT-HINT
         ACL2::EXPAND-PERMISSION-RESULT ACL2::TRANSLATE-REORDER-HINT
         ACL2::CHK-DEFUNS-TUPLES-CMP ACL2::DEFTHEORY-FN
         ACL2::TRANSLATE-SUBSTITUTION ACL2::TRANSLATE-GENERALIZE-ALIST
         ACL2::TRACE-PPR ACL2::GET-MEASURES ACL2::ASSOC-EQUIV+
         ACL2::ER-DECODE-CD ACL2::MAYBE-WRITE-BOOKDATA
         ACL2::PUSH-UNTOUCHABLE-FN ACL2::ACL2-QUERY
         ACL2::SELECT-FORWARD-CHAINED-CONCLS-AND-TTREES
         ACL2::TYPE-SET-BINARY-* ACL2::GET-BOOL-VARS
         ACL2::READ-FILE-INTO-STRING1 ACL2::FN-AND-MAXIMAL-LEVEL-NO-LST
         ACL2::POST-ALIST-FROM-PCERT1 ACL2::SET-BODY-FN
         ACL2::CHK-DO-NOT-EXPR-VALUE ACL2::RELEVANT-CONSTRAINTS
         ACL2::DECONSTRUCT-CONJUNCTION ACL2::MATCH-TESTS-AND-BINDINGS
         ACL2::ADJUST-UPPER-BOUND-WITH-NEG-EVGS ACL2::TYPE-SET-<-1
         ACL2::CHK-SIGNATURES ACL2::TRANSLATE-BOOK-NAMES
         ACL2::FN-COUNT-1 ACL2::CHK-XARGS-KEYWORDS1
         ACL2::TRANSLATE-SUBSTITUTION-LST
         ACL2::CHK-ACCEPTABLE-DEFUNS-REDUNDANCY ACL2::ERROR1-SAFE
         ACL2::PROCEED-FROM-BRKPT1 ACL2::CHK-MEMO-IF
         ACL2::SORT-APPROVED1-RATING1-LST ACL2::TRANSLATE-USE-HINT
         ACL2::TRANSLATE-EXPAND-TERM ACL2::LEAF-CST-LIST
         ACL2::TRANSLATE-BDD-HINT
         ACL2::TRANSLATE-BACKCHAIN-LIMIT-RW-HINT
         ACL2::SPLIT-XRUNE-ALIST ACL2::BIND-MACRO-ARGS
         ACL2::PUFFED-COMMAND-SEQUENCE ACL2::TRANS-EVAL-LST
         ACL2::SORT-APPROVED1-RATING1 ACL2::TRANSLATE-CASES-HINT
         ACL2::PE-FN-MAIN ACL2::EV-FNCALL-NULL-BODY-ER ACL2::PCS-FN
         ACL2::PRINT-GV-FN ACL2::SUBLIS-FN-REC-LST
         ACL2::TAU-VISIT-DEFUN
         ACL2::CHK-UNRESTRICTED-GUARDS-FOR-USER-FNS
         ACL2::TRANSLATE-USE-HINT1
         ACL2::REMOVE-META-EXTRACT-CONTEXTUAL-HYPS)) 
(COMMON-LISP::PROCLAIM
    '(COMMON-LISP::FTYPE
         (COMMON-LISP::FUNCTION
             (COMMON-LISP::T COMMON-LISP::T COMMON-LISP::T)
             COMMON-LISP::*)
         ACL2::PRINT-RULE-STORAGE-DEPENDENCIES ACL2::DUPLICATE-VARS-1
         ACL2::CHK-FLET-DECLARE-FORM ACL2::CHK-LD-QUERY-CONTROL-ALIST
         ACL2::OPEN-OUTPUT-CHANNEL! ACL2::ANCESTORS-CHECK-BUILTIN
         ACL2::REMOVE-POOL-LST-FROM-GAG-STATE ACL2::CLAUSIFY-ASSUMPTION
         ACL2::DEFATTACH-MERGE-LST-LST ACL2::RESET-PREHISTORY-FN
         ACL2::CHK-LD-ERROR-TRIPLES ACL2::LD-FN-BODY ACL2::PROGN!-FN
         ACL2::SET-QUERY-VAL ACL2::DEFATTACH-CLOSE
         ACL2::TAU-BOUNDER-DOMS-EXTRACTION ACL2::UNMONITOR1
         ACL2::CHK-LD-PRE-EVAL-PRINT ACL2::MOD-EXPT
         ACL2::READ-FILE-ITERATE ACL2::CHK-NO-DUPLICATE-DEFUNS
         ACL2::CHK-LD-MISSING-INPUT-OK ACL2::COMPILE-FUNCTION
         ACL2::PROCESS-DEFATTACH-ARGS ACL2::DEFUNS-FN
         ACL2::OPEN-INPUT-OBJECT-FILE ACL2::ONE-WAY-UNIFY-RESTRICTIONS1
         ACL2::OPEN-INPUT-CHANNEL ACL2::PRINT-PROMPT
         ACL2::CHK-LD-PRE-EVAL-FILTER ACL2::PCB-PCB!-FN
         ACL2::CHK-LEGAL-INIT ACL2::UPDATE-MEMO-ENTRY-FOR-ATTACHMENTS
         ACL2::TRANSLATE-BREAK-CONDITION ACL2::ADD-PC-COMMAND-1
         ACL2::GOAL-TREE-CHOOSE-DISJUNCT-REC ACL2::PRUNE-GOAL-TREE
         ACL2::INTERPRET-TERM-AS-CONGRUENCE-RULE
         ACL2::TILDE-*-BOOK-CHECK-SUMS-PHRASE1 ACL2::CONS-TERM1-MV2
         ACL2::CHK-LD-ERROR-ACTION ACL2::CERTIFY-BOOK-FINISH-COMPLETE
         ACL2::CHK-LENGTH-AND-KEYS ACL2::UNMONITOR-FN ACL2::CHK-?S
         ACL2::CHK-PROOFS-CO ACL2::FINALIZE-EVENT-USER
         ACL2::TYPE-SET-CONS ACL2::STOBJ-UPDATES-LISTP
         ACL2::REVERT-GOAL-TREE-REC ACL2::CHK-?S-LST
         ACL2::MAYBE-RESET-DEFAULTS-TABLE
         ACL2::CONVERT-NAME-TREE-TO-NEW-NAME1 ACL2::CHK-STANDARD-OI
         ACL2::EXPANDED-NEW-VARS-IN-POT-LST2 ACL2::ALWAYS
         ACL2::SWEEP-GLOBAL-LST ACL2::OR-ADDR
         ACL2::ELIMINATE-MACRO-ALIASES ACL2::TRANSLATE-SUBST-ABB1
         ACL2::EVAL-PORT-FILE ACL2::CONVERT-TYPE-PRESCRIPTION-TO-TERM
         ACL2::GET-COMMAND-SEQUENCE-FN ACL2::TYPE-SET-UNARY--
         ACL2::LIMIT-FAILURE-REASON ACL2::TRANSLATE-SUBST-ABB
         ACL2::CHK-PRIMITIVE-INSTRUCTION-LISTP ACL2::ONE-WAY-UNIFY1
         ACL2::TRANSLATE-DO-NOT-HINT ACL2::GENERALIZE-RULE-SEGMENT1
         ACL2::DEFMACRO-FN ACL2::LIMIT-FAILURE-REASON-ALIST
         ACL2::CHK-DEFUN-MODE ACL2::DUPLICATE-VARS-1-LST
         ACL2::VERIFY-TERMINATION-BOOT-STRAP-FN ACL2::TRACE$-FN-GENERAL
         ACL2::PARSE-PRIMES ACL2::CHK-INHIBIT-OUTPUT-LST
         ACL2::ONE-WAY-UNIFY1-LST ACL2::MAKE-EVENT-DEBUG-PRE
         ACL2::TYPE-SET-CAR ACL2::DEFCHOOSE-FN
         ACL2::SET-PARALLEL-EXECUTION-FN
         ACL2::GOAL-TREE-CHOOSE-DISJUNCT-LST ACL2::TRACE$-LST
         ACL2::FIX-LOOP-STOPPER-ALIST
         ACL2::TILDE-*-BOOK-CHECK-SUMS-PHRASE ACL2::CHK-EVISC-TUPLE
         ACL2::CHK-LD-REDEFINITION-ACTION ACL2::IN-THEORY-FN
         ACL2::PRINT-CLAUSE-PROCESSOR-RULES1
         ACL2::EXISTS-ASSUMPTION-WITH-WEAKER-TYPE-ALIST
         ACL2::DEFATTACH-MERGE-LST
         ACL2::TAU-INTERVAL-ENDPOINT-TO-SIGN-K-TOKEN
         ACL2::INCLUDE-BOOK-ALIST-UNCERTIFIED-BOOKS ACL2::DEFUN-FN
         ACL2::SET-IPRINT-SOFT-BOUND ACL2::MAPDO ACL2::STOBJ-UPDATES-P
         ACL2::MONADIC-BOOLEAN-FNP ACL2::CHK-STANDARD-CO
         ACL2::FIND-EQUATIONAL-POLY1 ACL2::CONVERT-TERM-TO-PAIRS
         ACL2::CHK-FLET-DECLARE-FORM-LIST ACL2::LD-FN0
         ACL2::DEFLABEL-FN ACL2::THANKS-FOR-THE-HINT ACL2::SYS-CALL+
         ACL2::SWEEP-ACL2-ORACLE ACL2::BAD-SYNP-HYP-MSG-FOR-LINEAR
         ACL2::EV-FNCALL-META ACL2::TOGGLE-PC-MACRO-FN
         ACL2::DEFATTACH-FN ACL2::SWEEP-T-STACK ACL2::GET-MEASURES2
         ACL2::CERTIFICATE-FILE-AND-INPUT-CHANNEL
         ACL2::PRINT-LDD-FULL-OR-SKETCH ACL2::REDUCE-GENEQV-FOR-EQUIV
         ACL2::TYPE-SET-NUMERATOR ACL2::CHK-LD-SKIP-PROOFSP
         ACL2::SPLIT-AT-POSITION ACL2::SET-IPRINT-HARD-BOUND
         ACL2::TYPE-SET-CDR ACL2::CHECK-FIELD-NAMES ACL2::TRACE$-FN
         ACL2::ORACLE-APPLY ACL2::LOOK-IN-TYPE-ALIST ACL2::UBT-UBU-FN
         ACL2::SIMPLIFY-CLAUSE-FOR-TERM-EQUAL-CONST-1
         ACL2::STOP-REDUNDANT-EVENT-FN ACL2::CHK-LD-PROMPT
         ACL2::ACCUMULATE-TTREE-AND-STEP-LIMIT-INTO-STATE
         ACL2::READ-OBJECT-FILE1 ACL2::FIRST-BOOLEAN-TYPE-PRESCRIPTION
         ACL2::SIMPLIFY-TESTS ACL2::TYPE-SET-REALPART
         ACL2::MACRO-GUARD-ER-MSG ACL2::APPLY-GENERALIZE-RULE
         ACL2::FIND-EQUATIONAL-POLY3 ACL2::CHK-EXTENSIBLE-RULE-CLASSES
         ACL2::INITIALIZE-EVENT-USER ACL2::MACROEXPAND1
         ACL2::CHK-LD-POST-EVAL-PRINT
         ACL2::FIND-SUBSUMER-REPLACEMENT-REC ACL2::BINDING-HYP-P
         ACL2::CHK-INPUT-OBJECT-FILE ACL2::ANCESTORS-CHECK
         ACL2::IN-ARITHMETIC-THEORY-FN ACL2::DEFATTACH-LOOP-ERROR
         ACL2::PRINT-DOC-DWIM ACL2::RUNES-TO-MONITOR ACL2::CHK-STATE-OK
         ACL2::PRUNE-GOAL-TREE-LST ACL2::UBT!-UBU!-FN
         ACL2::META-EXTRACT-GLOBAL-FACT+ ACL2::MONITOR-FN
         ACL2::FIND-EQUATIONAL-POLY2 ACL2::FETCH-TERM-AND-CL
         ACL2::UPDATE-PROOF-SUPPORTERS-ALIST ACL2::TYPE-SET-IMAGPART
         ACL2::TYPE-SET-NOT ACL2::FALSIFYING-ASSIGNMENT1
         ACL2::SUBLIS-FN ACL2::UNTRACE$-REC ACL2::PUFF*-FN1
         ACL2::DEFATTACH-ERASE-P ACL2::ONE-WAY-UNIFY-RESTRICTIONS
         ACL2::SIMPLIFIABLE-MV-NTH1
         ACL2::INTERPRET-TERM-AS-WELL-FORMEDNESS-GUARANTEE-THM
         ACL2::UBT?-UBU?-FN ACL2::AND-ADDR ACL2::ORACLE-APPLY-RAW
         ACL2::READ-OBJECT-FILE ACL2::TAU-LIKE-TERM
         ACL2::HARD-ERROR-IS-ERROR ACL2::LD-FN
         ACL2::SET-WATERFALL-PRINTING-FN ACL2::PRINT-INFO-FOR-RULES
         ACL2::CHK-LD-VERBOSE ACL2::MAPCAR$
         ACL2::COUNT-FORMS-IN-CHANNEL ACL2::TYPE-SET-UNARY-/
         ACL2::CANONICAL-REPRESENTATIVE
         ACL2::CERTIFICATE-FILE-AND-INPUT-CHANNEL1 ACL2::THEREIS
         ACL2::CHK-CURRENT-PACKAGE ACL2::COMMAND-BLOCK-NAMES1
         ACL2::TYPE-SET-LENGTH ACL2::PRINT-SAVED-OUTPUT
         ACL2::OPEN-OUTPUT-CHANNEL ACL2::SET-WATERFALL-PARALLELISM-FN
         ACL2::CHK-ASSUMPTION-FREE-TTREE ACL2::TRACE$-FN-SIMPLE
         ACL2::TYPE-SET-CHAR-CODE ACL2::SKIP-FORMS-IN-CHANNEL
         ACL2::PICK-BEST-PSPV-FOR-WATERFALL0-OR-HIT
         ACL2::PROOF-CHECKER-CL-PROC ACL2::ASSOC-TYPE-ALIST)) 
(COMMON-LISP::PROCLAIM
    '(COMMON-LISP::FTYPE
         (COMMON-LISP::FUNCTION
             (COMMON-LISP::T COMMON-LISP::T COMMON-LISP::T
                 COMMON-LISP::T COMMON-LISP::T COMMON-LISP::T
                 COMMON-LISP::T)
             COMMON-LISP::*)
         ACL2::EV-LST-RESPECTING-ENS ACL2::BIND-MACRO-ARGS-KEYS1
         ACL2::KNOWN-WHETHER-NIL ACL2::FIX-PORTCULLIS-CMDS
         ACL2::SPLAT-ATOM ACL2::CLAUSIFY-INPUT
         ACL2_*1*_ACL2::MFC-RW+-FN ACL2::EVISCERATE ACL2::PROOF-CHECKER
         ACL2::CHK-ACCEPTABLE-DEFPKG ACL2::TRANSLATE
         ACL2::TRANSLATE-RULE-CLASS ACL2::DEFPKG-ITEMS-REC
         ACL2::CHK-ACCEPTABLE-TTAG1
         ACL2::CHK-COMMON-LISP-COMPLIANT-SUBFUNCTIONS
         ACL2::CHK-JUST-NEW-NAME ACL2::REWRITE-CLAUSE-TYPE-ALIST
         ACL2::TAU-CLAUSEP-LST ACL2::MFC-RW+-FN ACL2::SPLAT1
         ACL2::CHK-ACCEPTABLE-TYPE-SET-INVERTER-RULE
         ACL2::TRANSLATE-TERM-LST ACL2::PROVE-COROLLARIES
         ACL2::CHK-JUST-NEW-NAMES-REC ACL2::SET-PRINT-GV-DEFAULTS-FN
         ACL2::PARSE-STOBJ-LET1 ACL2::TRANSLATE-CMP ACL2::ADD-POLYS1
         ACL2::TRANSLATE-HINTS1 ACL2::TAU-REWRITE ACL2::TRACE$-INSTALL
         ACL2::EXPAND-ADDRESS ACL2::SPLAT ACL2::RECONSIDER-TYPE-ALIST
         ACL2::MAKE-INCLUDE-BOOKS-ABSOLUTE-LST
         ACL2::UNCOVERED-EQUIVS-ALIST-LST
         ACL2::INDUCTION-MACHINE-FOR-FN1-LST
         ACL2::TRANSLATE-RULE-CLASSES1 ACL2::MAKE-EVENT-FN2
         ACL2::DEFPKG-FN ACL2::PUTPROP-TYPE-PRESCRIPTION-LST
         ACL2::INDUCTION-MACHINE-FOR-FN1 ACL2::XTRANS-EVAL
         ACL2::TRANSLATE-RULE-CLASSES ACL2::UPDATE-ATTACHMENT-RECORDS
         ACL2::TRANSLATE-X-HINT-VALUE ACL2::SEARCH-GROUND-UNITS
         ACL2::EVISCERATE-TOP ACL2::CRUNCH-CLAUSE-SEGMENTS
         ACL2::VAR-FN-COUNT-1 ACL2::TRANSLATE1
         ACL2::EVAL-CLAUSE-PROCESSOR ACL2::POP-CLAUSE-MSG1
         ACL2::EV-RESPECTING-ENS ACL2::PROVE-LOOP
         ACL2::ANCESTORS-CHECK1 ACL2::CHK-ACCEPTABLE-TTAGS1
         ACL2::ADD-INVERSE-POLYS ACL2::MAKE-EVENT-FN1
         ACL2::DEFCHOOSE-CONSTRAINT-BASIC ACL2::PC-TOP
         ACL2::BDD-RULES-ALIST1 ACL2::CHK-REDEFINEABLE-NAMEP
         ACL2::MAKE-INCLUDE-BOOKS-ABSOLUTE-1 ACL2::OBJ-TABLE
         ACL2::MV-ATF ACL2::CERT-OBJ-FOR-CONVERT
         ACL2::FIND-TRIVIAL-EQUIVALENCE1 ACL2::CHK-ACCEPTABLE-META-RULE
         ACL2::RAW-EV-FNCALL ACL2::MAKE-EVENT-FN2-LST
         ACL2::TRANSLATE1-CMP ACL2::WATERFALL-UPDATE-GAG-STATE
         ACL2::CLAUSIFY-INPUT1-LST ACL2::GUESS-MEASURE-ALIST
         ACL2::SETUP-SIMPLIFY-CLAUSE-POT-LST1 ACL2::TAU-CLAUSE1P
         ACL2::CHK-CERT-ANNOTATIONS ACL2::PROVE-LOOP0
         ACL2::CHK-TRACE-OPTIONS ACL2::REGENERATE-TAU-DATABASE-FN0
         ACL2::FC-EXIT ACL2::LOAD-HINT-SETTINGS-INTO-PSPV
         ACL2::TAU-TERM ACL2::APPLY-TOP-HINTS-CLAUSE1
         ACL2::STATE-STACK-FROM-INSTRUCTIONS ACL2::PROVE
         ACL2::TAU-CLAUSEP-LST-REC ACL2::CHK-ACCEPTABLE-TTAGS2
         ACL2::INCLUDE-BOOK-ER
         ACL2::GUESS-AND-PUTPROP-TYPE-PRESCRIPTION-LST-FOR-CLIQUE-STEP
         ACL2::RELEVANT-CONSTRAINTS1-AXIOMS ACL2::CHK-RAISE-PORTCULLIS2
         ACL2::ADD-POLYS-FROM-TYPE-SET ACL2::CHK-LOGIC-SUBFUNCTIONS
         ACL2::TRANSLATE-WELL-FORMEDNESS-GUARANTEE
         ACL2::TRANSLATE-HINTS2 ACL2::CHK-CERTIFICATE-FILE
         ACL2::ENCAPSULATE-PASS-2)) 
(COMMON-LISP::PROCLAIM
    '(COMMON-LISP::FTYPE
         (COMMON-LISP::FUNCTION
             (COMMON-LISP::T COMMON-LISP::T COMMON-LISP::T
                 COMMON-LISP::T COMMON-LISP::T COMMON-LISP::T
                 COMMON-LISP::T COMMON-LISP::T COMMON-LISP::T
                 COMMON-LISP::T COMMON-LISP::T COMMON-LISP::T
                 COMMON-LISP::T COMMON-LISP::T COMMON-LISP::T
                 COMMON-LISP::T COMMON-LISP::T COMMON-LISP::T
                 COMMON-LISP::T)
             COMMON-LISP::*)
         ACL2::DEFUNS-FN1 ACL2::TYPE-SET-RELIEVE-HYPS1)) 
(COMMON-LISP::PROCLAIM
    '(COMMON-LISP::FTYPE
         (COMMON-LISP::FUNCTION
             (COMMON-LISP::T COMMON-LISP::T COMMON-LISP::T
                 COMMON-LISP::T COMMON-LISP::T)
             COMMON-LISP::*)
         ACL2::ONE-WAY-UNIFY1-EQUAL ACL2::CHK-DEFATTACH-LOOP
         ACL2::STOBJS-IN-OUT ACL2::GUESS-TYPE-PRESCRIPTION-FOR-FN-STEP
         ACL2::CERTIFICATE-POST-ALIST ACL2::PUFF-COMMAND-BLOCK
         ACL2::GENERATE-VARIABLE-ROOT
         ACL2::SMALLEST-COMMON-SUBTERMS1-LST
         ACL2::EVAL-GROUND-SUBEXPRESSIONS ACL2::PUSH-CLAUSE
         ACL2::RW-CACHE-DEBUG-ACTION ACL2::EXPAND-AND-OR-SIMPLE
         ACL2::COLLECT-DECLARATIONS ACL2::FIND-AND-OR-LEMMA
         ACL2::CHK-THEORY-EXPR-VALUE ACL2::PEQUIVS-FOR-REWRITE-ARGS
         ACL2::PC-MAIN-LOOP ACL2::TYPE-SET-INTERN-IN-PACKAGE-OF-SYMBOL
         ACL2::CHK-ACCEPTABLE-TTAG ACL2::TRANSLATE-INSTRUCTIONS
         ACL2::ATTACHMENT-RECORDS ACL2::DESTRUCTURE-TYPE-PRESCRIPTION
         ACL2_*1*_ACL2::MAGIC-EV-FNCALL ACL2::TAU-CLAUSEP
         ACL2::TRANSLATE-BDD-HINT1 ACL2::TRANSLATE-HINTS
         ACL2::COLLECT-DECLARATIONS-CMP ACL2::DEFPKG-ITEMS
         ACL2::DELETE-BAD-VALS1 ACL2::DEPOSIT-TERM-IN-GOAL
         ACL2::EXPAND-RECOGNIZER ACL2::UPDATE-PROOF-SUPPORTERS-ALIST-1
         ACL2::TRANSLATE-BY-HINT
         ACL2::GET-BOOLEAN-UNAMBIGUOUS-XARGS-FLG-LST
         ACL2::ELIMINATE-DESTRUCTORS-CLAUSE
         ACL2::GET-UNAMBIGUOUS-XARGS-FLG-LST
         ACL2::TRANSLATE-OVERRIDE-HINTS ACL2::PROVER-CALL
         ACL2::ADD-POLY ACL2::PRINT-GV1 ACL2::SETTLED-DOWN-CLAUSE
         ACL2::APPLY-CONJUNCTIVE-TAU-RULES2
         ACL2::CHK-ACCEPTABLE-EQUIVALENCE-RULE
         ACL2::FIND-REWRITING-EQUIVALENCE
         ACL2::GET-CMDS-FROM-PORTCULLIS1 ACL2::CHK-MUTUAL-RECURSION1
         ACL2::EV-FNCALL! ACL2::GET-RULER-EXTENDERS2
         ACL2::CHK-DEFUNS-TUPLES ACL2::FIRST-FERTILIZE-LIT
         ACL2::CHK-ACCEPTABLE-TAU-RULE ACL2::TRANSLATE-EXPAND-HINT1
         ACL2::EVAL-GROUND-SUBEXPRESSIONS-LST-LST
         ACL2::EVAL-GROUND-SUBEXPRESSIONS-LST ACL2::SUBLIS-VAR!-LST
         ACL2::RW-CACHE-DEBUG ACL2::POP-CLAUSE-UPDATE-GAG-STATE-POP
         ACL2::CHK-ACCEPTABLE-CONGRUENCE-RULE
         ACL2::TAU-RULES-FROM-TYPE-PRESCRIPTIONS
         ACL2::TAU-PUT*-INTERVAL-ENDPOINTS ACL2::FILTER-FOR-ATTACHMENT
         ACL2::LOOKUP-HYP ACL2::CHK-ALL-BUT-NEW-NAME
         ACL2::M&M-OVER-POWERSET1 ACL2::WRAP1-AUX2
         ACL2::DELETE-BAD-VALS ACL2::TRANSLATE-DEFATTACH-HELPERS
         ACL2::RELIEVE-HYP-FAILURE-ENTRY-SKIP-P
         ACL2::MAYBE-ADD-COMMAND-LANDMARK
         ACL2::GET-UNAMBIGUOUS-XARGS-FLG
         ACL2::PARTITION-SIGNATURE-HYPS-INTO-TAU-ALIST-AND-OTHERS
         ACL2::CERTIFY-BOOK-FINISH-CONVERT
         ACL2::CHK-ACCEPTABLE-BUILT-IN-CLAUSE-RULE
         ACL2::FIND-ABBREVIATION-LEMMA ACL2::FMT!-TO-STRING-FN
         ACL2::FMT! ACL2::PUFF*-FN11 ACL2::PUFF-REPORT
         ACL2::MAGIC-EV-FNCALL ACL2::TRANSLATE-CUSTOM-KEYWORD-HINT
         ACL2::TAU-VISIT-DEFTHM ACL2::MAKE-IF-CST ACL2::DEFCONST-FN
         ACL2::SHOW-BDD-FN ACL2::FREE-VARIABLE-ERROR? ACL2::CHK-ARGLIST
         ACL2::ADD-POLYS0 ACL2::CHK-ACCEPTABLE-TTAGS
         ACL2::CHK-ACCEPTABLE-DEFATTACH
         ACL2::TYPE-SET-AND-RETURNED-FORMALS ACL2::CHK-IN-PACKAGE
         ACL2::ADD-LITERAL-AND-PT ACL2::PARSE-BOOK-NAME
         ACL2::PEGATE-LIT ACL2::PUFF-COMMAND-BLOCK1
         ACL2::SMALLEST-COMMON-SUBTERMS1
         ACL2::CHK-ACCEPTABLE-ENCAPSULATE2 ACL2::DESTRUCTURE-DEFINITION
         ACL2::GET-UNAMBIGUOUS-XARGS-FLG1 ACL2::CHK-TABLE-GUARDS
         ACL2::TAU-PUT*-TAU ACL2::INTERPRET-TERM-AS-REWRITE-RULE
         ACL2::CHK-DESTRUCTURE-DEFINITION ACL2::TAU-VISIT-DEFTHM1
         ACL2::TILDE-@-CERT-POST-ALIST-PHRASE
         ACL2::SET-OVERRIDE-HINTS-FN ACL2::GENERALIZE-CLAUSE
         ACL2::COMMENT-ON-NEW-RECOG-TUPLE ACL2::NEGATE-LIT
         ACL2::COLLECT-TERMS-AND-ACTIVATIONS-FROM-FCD-LST
         ACL2::FIND-EQUIVALENCE-HYP-TERM-NO-TARGET
         ACL2::CHK-LEGAL-LINEAR-TRIGGER-TERMS1
         ACL2::CHK-ACCEPTABLE-VERIFY-GUARDS-FORMULA
         ACL2::CHK-ACCEPTABLE-REFINEMENT-RULE
         ACL2::CHK-ACCEPTABLE-INDUCTION-RULE ACL2::APPLY-TAU-BOUNDERS
         ACL2::GET-AND-CHK-LAST-MAKE-EVENT-EXPANSION
         ACL2::CLEAN-UP-CLAUSE-SET ACL2::EXTEND-ATTACHMENT-COMPONENTS
         ACL2::POP-CLAUSE-MSG
         ACL2::CHK-ACCEPTABLE-CLAUSE-PROCESSOR-RULE
         ACL2::SET-EVISC-TUPLE-LST ACL2::CHK-ACCEPTABLE-ELIM-RULE
         ACL2::CHK-TABLE-NIL-ARGS ACL2::EXPAND-CLAUSE
         ACL2::DEFATTACH-CONSTRAINT ACL2::PE-FN2
         ACL2::CHK-ACCEPTABLE-ENCAPSULATE1
         ACL2::ELIMINATE-IRRELEVANCE-CLAUSE
         ACL2::META-RULE-HYPOTHESIS-FUNCTIONS ACL2::FMT
         ACL2::CHK-ACCEPTABLE-DEFSTOBJ ACL2::LD-STANDARD-OI-MISSING
         ACL2::DEFAXIOM-FN ACL2::FIND-TRIVIAL-EQUIVALENCE
         ACL2::REBUILD-FN ACL2::GUARD-OBLIGATION-CLAUSES
         ACL2::SWEEP-STACK-ENTRY-FOR-BAD-SYMBOL
         ACL2::CHK-ACCEPTABLE-BUILT-IN-CLAUSE-RULE1
         ACL2::CHK-ACCEPTABLE-WELL-FOUNDED-RELATION-RULE
         ACL2::CHK-DCL-LST ACL2::NOT-IDENT
         ACL2::TRANSLATE-BACKTRACK-HINT ACL2::ONE-WAY-UNIFY1-EQUAL1
         ACL2::CHK-ACCEPTABLE-GENERALIZE-RULE
         ACL2::CLAUSIFY-ASSUMPTIONS
         ACL2::MAYBE-TRUNCATE-CURRENT-ADDRESS ACL2::DEFCONST-VAL
         ACL2::GENERATE-VARIABLE-ROOT1 ACL2::TRANSLATE-LMI
         ACL2::CHK-LEGAL-LINEAR-TRIGGER-TERMS
         ACL2::CONVERT-TYPE-SET-TO-TERM-LST ACL2::REWRITE-IF11
         ACL2::CHK-ALL-STOBJ-NAMES ACL2::BDD-RULES-ALIST
         ACL2::ADD-TAU-RULE ACL2::UPDATE-PROOF-SUPPORTERS-ALIST-3
         ACL2::CHK-NEW-STRINGP-NAME ACL2::TRANSLATE-IN-THEORY-HINT
         ACL2::CHECK-FORMALS-LENGTH ACL2::TYPE-SET-BINARY-+
         ACL2::PRINT-DEFUN-MSG/TYPE-PRESCRIPTIONS
         ACL2::CHK-DEFABSSTOBJ-GUARDS ACL2::CONVERT-TYPE-SET-TO-TERM
         ACL2::PROTECTED-EVAL ACL2::SUBLIS-VAR!
         ACL2::PARSE-DOTTED-NATURALS ACL2::DEFAXIOM-SUPPORTERS
         ACL2::DEFATTACH-ERASE1 ACL2::FMT-TO-STRING-FN)) 
(COMMON-LISP::PROCLAIM
    '(COMMON-LISP::FTYPE
         (COMMON-LISP::FUNCTION
             (COMMON-LISP::T COMMON-LISP::T COMMON-LISP::T
                 COMMON-LISP::T COMMON-LISP::T COMMON-LISP::T)
             COMMON-LISP::*)
         ACL2::EXTRACT-AND-CLAUSIFY-ASSUMPTIONS ACL2::PREPROCESS-CLAUSE
         ACL2::FIX-TTAGS ACL2::CHK-ACCEPTABLE-DEFSTOBJ-RENAMING
         ACL2::SEARCH-TYPE-ALIST ACL2::BIND-MACRO-ARGS1 ACL2::TAU-PUT*
         ACL2::NORMALIZE ACL2::BDD-CLAUSE ACL2::CHK-TRACE-OPTIONS-AUX
         ACL2::TRANS-EVAL1 ACL2::UNKNOWN-BINDING-MSG-ER
         ACL2::BUILT-IN-CLAUSEP ACL2::FMT1-TO-STRING-FN
         ACL2::CHK-TABLE-GUARDS-REC
         ACL2::CHK-ACCEPTABLE-VERIFY-TERMINATION1 ACL2::WALKABOUT1
         ACL2::TRANSLATE-HINT-EXPRESSION ACL2::INCLUDE-BOOK-ER1
         ACL2::NORMALIZE-LST ACL2::VERIFY-GUARDS-FN
         ACL2::TRANSLATE-HINT ACL2::INCLUDE-BOOK-RAW ACL2::TAU-PUT
         ACL2::NORMALIZE-WITH-TYPE-SET
         ACL2::TYPE-SET-AND-RETURNED-FORMALS-WITH-RULE
         ACL2::REMOVE-BUILT-IN-CLAUSES ACL2::TYPE-SET-FINISH
         ACL2::GUESS-CONTROLLER-ALIST-FOR-DEFINITION-RULE
         ACL2::STOBJS-IN-OUT1 ACL2::COLLECT-TERMS-AND-ACTIVATIONS-LST
         ACL2::VERIFY-GUARDS-FN1 ACL2::PRINT-INDENTED-LIST
         ACL2::FERTILIZE-CLAUSE ACL2::TRANSLATE-HINTS+
         ACL2::CHK-ACCEPTABLE-LD-FN1-PAIR ACL2::CHK-ACCEPTABLE-X-RULE
         ACL2::ADD-TAU-RULE1 ACL2::GET-PORTCULLIS-CMDS
         ACL2::TYPE-ALIST-FCD-LST ACL2::VERIFY-FN
         ACL2::CHK-RAISE-PORTCULLIS1 ACL2::EV-FNCALL
         ACL2::APPLY-INSTANTIATED-ELIM-RULE
         ACL2::CHK-NON-EXECUTABLE-BODIES ACL2::FC-PAIR-LST-TYPE-ALIST
         ACL2::DEFEVALUATOR-CHECK ACL2::DEFMACRO-FN1
         ACL2::TYPE-RESTRICTION-SEGMENT ACL2::BIND-MACRO-ARGS-KEYS
         ACL2::TRANSLATE-HINTS+1 ACL2::SIMPLE-TRANSLATE-ABSSTOBJ-FIELDS
         ACL2::CHK-DECLARED-IGNORES ACL2::EV-FNCALL-GUARD-ER
         ACL2::PREPROCESS-CLAUSE? ACL2::TYPE-ALIST-CLAUSE-FINISH1
         ACL2::CHK-RULE-FN-GUARD ACL2::GUARD-CLAUSES-LST
         ACL2::GUARD-CLAUSES ACL2::TRANSLATE-EXPAND-TERM1
         ACL2::MAKE-EVENT-FN ACL2::CHK-ACCEPTABLE-BUILT-IN-CLAUSE-RULE2
         ACL2::SET-EVISC-TUPLE-FN1 ACL2::TRANSLATE-HINT-SETTINGS
         ACL2::CHK-INCLUDE-BOOK-INPUTS ACL2::MFC-RW-TTREE
         ACL2::CHK-FREE-VARS ACL2::CHK-ACCEPTABLE-RULES
         ACL2::CHK-CERT-ANNOTATIONS-POST-ALIST
         ACL2::CHK-ACCEPTABLE-COMPOUND-RECOGNIZER-RULE
         ACL2::SET-EVISC-TUPLE-FN ACL2::LOAD-HINT-SETTINGS-INTO-RCNST
         ACL2::TRANSLATE-OR-HINT ACL2::GET-UNAMBIGUOUS-XARGS-FLG1/EDCLS
         ACL2::TAU-PUT*-RECOGS ACL2::READ-ACL2X-FILE ACL2::ADD-TO-TAU!
         ACL2::CHK-ACCEPTABLE-ELIM-RULE1
         ACL2::BIND-MACRO-ARGS-AFTER-REST ACL2::TYPE-SET-COERCE
         ACL2::APPLY-USE-HINT-CLAUSES ACL2::CLAUSIFY-TYPE-ALIST
         ACL2::PROVE-GUARD-CLAUSES-MSG ACL2::PROVE-DEFATTACH-GUARDS
         ACL2::CONVERT-TYPE-SET-TO-TERM1
         ACL2::TRANSLATE-HINT-EXPRESSIONS ACL2::CHK-THEORY-INVARIANT1
         ACL2::TILDE-*-RAW-SIMP-PHRASE1 ACL2::EV-LST
         ACL2::PARSE-ARGS-AND-TEST ACL2::EV-FOR-TRANS-EVAL
         ACL2::SEARCH-TYPE-ALIST-WITH-REST
         ACL2::GET-CMDS-FROM-PORTCULLIS ACL2::CHK-JUST-NEW-NAMES
         ACL2::REMOVE-TRIVIAL-LITS ACL2::FMT1!
         ACL2::CHK-STOBJ-FIELD-DESCRIPTOR
         ACL2::COLLECT-TERMS-AND-ACTIVATIONS
         ACL2::REGENERATE-TAU-DATABASE-FN1 ACL2::FMT1!-TO-STRING-FN
         ACL2::GUARD-CLAUSES-FOR-CLIQUE
         ACL2::PICK-BEST-PSPV-FOR-WATERFALL0-OR-HIT1
         ACL2::ELIMINATE-DESTRUCTORS-CLAUSE1 ACL2::GENERALIZE1
         ACL2::CHK-TABLE-GUARD ACL2::FMT-ABBREV1
         ACL2::NORMALIZE-OR-DISTRIBUTE-FIRST-IF
         ACL2::GUARD-CLAUSES-FOR-FN ACL2::CHK-ACCEPTABLE-X-RULES
         ACL2::SIMPLIFY-CLAUSE1 ACL2::SCONS-TERM
         ACL2::TAU-EXPAND-BIG-SWITCH ACL2::TYPE-SET-FINISH-1
         ACL2_*1*_ACL2::MFC-RW-TTREE ACL2::SEARCH-TYPE-ALIST-REC
         ACL2::EV ACL2::CHK-EQUAL-ARITIES ACL2::SEARCH-TYPE-ALIST+
         ACL2::POST-ALIST-FROM-PCERT1-1 ACL2::TYPE-SET-IMPLIED-BY-TERM
         ACL2::CHK-THEORY-EXPR-VALUE1 ACL2::HIDDEN-DEFPKG-EVENTS1
         ACL2::GET-RULER-EXTENDERS1 ACL2::DISTRIBUTE-FIRST-IF
         ACL2::BIND-MACRO-ARGS-OPTIONAL ACL2::INTRO-UDF-GUARDS
         ACL2::INCLUDE-BOOK-RAW-TOP ACL2::SIMPLIFY-CLAUSE)) 
(COMMON-LISP::PROCLAIM
    '(COMMON-LISP::FTYPE
         (COMMON-LISP::FUNCTION
             (COMMON-LISP::T COMMON-LISP::T COMMON-LISP::T
                 COMMON-LISP::T COMMON-LISP::T COMMON-LISP::T
                 COMMON-LISP::T COMMON-LISP::T COMMON-LISP::T
                 COMMON-LISP::T COMMON-LISP::T COMMON-LISP::T)
             COMMON-LISP::*)
         ACL2::PC-RELIEVE-HYPS1-ITER
         ACL2::PROPER/IMPROPER-CONS-TS-TUPLE ACL2::FERTILIZE-CLAUSE1
         ACL2::EV-REC-RETURN-LAST ACL2::APPLY-OVERRIDE-HINTS
         ACL2::WATERFALL1 ACL2::ASSUME-TRUE-FALSE-REC ACL2::REWRITE-ATM
         ACL2::DEFABSSTOBJ-FN1 ACL2::FORWARD-CHAIN1
         ACL2::APPLY-OVERRIDE-HINT ACL2::ASSUME-TRUE-FALSE-IF
         ACL2::CERTIFY-BOOK-FN ACL2::APPLY-OVERRIDE-HINT1
         ACL2::WATERFALL-STEP-CLEANUP
         ACL2::SUBST-EQUIV-AND-MAYBE-DELETE-LIT
         ACL2::PUT-INDUCTION-INFO-RECURSIVE ACL2::ASSUME-TRUE-FALSE1
         ACL2::TRANSLATE11-CALL ACL2::TYPE-SET-WITH-RULE)) 
(COMMON-LISP::PROCLAIM
    '(COMMON-LISP::FTYPE
         (COMMON-LISP::FUNCTION
             (COMMON-LISP::T COMMON-LISP::T COMMON-LISP::T
                 COMMON-LISP::T COMMON-LISP::T COMMON-LISP::T
                 COMMON-LISP::T COMMON-LISP::T COMMON-LISP::T
                 COMMON-LISP::T)
             COMMON-LISP::*)
         ACL2::PROVE-LOOP2 ACL2::ADVANCE-FC-ACTIVATIONS
         ACL2::CHK-ACCEPTABLE-DEFUNS1 ACL2::PROVE-DEFATTACH-GUARDS1
         ACL2::PUTPROP-BODY-LST ACL2::CHK-IRRELEVANT-FORMALS
         ACL2::CHK-DEFABSSTOBJ-METHOD ACL2::ASSUME-TRUE-FALSE
         ACL2::SIMPLE-TRANSLATE-AND-EVAL-CMP
         ACL2::TRANSLATE-RULE-CLASS-ALIST ACL2::TRANSLATE11-LST
         ACL2::WATERFALL ACL2::ADD-TYPE-SET-POLYS
         ACL2::PROVE-COROLLARIES1 ACL2::CHK-EMBEDDED-EVENT-FORM
         ACL2::INCLUDE-BOOK-FN ACL2::CHK-FREE-AND-IGNORED-VARS-LSTS
         ACL2::EV-REC-ACL2-UNWIND-PROTECT ACL2::EV-REC-LST ACL2::EV-REC
         ACL2::LINEARIZE-LST1 ACL2::NEXT-PEQUIVS
         ACL2::APPLY-SIGNATURE-TAU-RULES1 ACL2::EV-FNCALL-REC
         ACL2::APPLY-SIGNATURE-TAU-RULES ACL2::CHK-TRIGGERS
         ACL2::EV-FNCALL-REC-LOGICAL ACL2::PRINT-GV-CONJUNCT
         ACL2::CHK-FREE-AND-IGNORED-VARS
         ACL2::EXPAND-ABBREVIATIONS-WITH-LEMMA
         ACL2::INSTALL-EVENT-DEFUNS
         ACL2::GENEQV-AND-PEQUIV-INFO-FOR-REWRITE ACL2::TRANSLATE11-LET
         ACL2::SIMPLE-TRANSLATE-AND-EVAL-ERROR-DOUBLE
         ACL2::PROCESS-EMBEDDED-EVENTS ACL2::INSTALL-EVENT
         ACL2::ADVANCE-FC-ACTIVATION ACL2::CHK-ACCEPTABLE-DEFSTOBJ1
         ACL2::TRANSLATE11-LET*)) 
(COMMON-LISP::PROCLAIM
    '(COMMON-LISP::FTYPE
         (COMMON-LISP::FUNCTION
             (COMMON-LISP::T COMMON-LISP::T COMMON-LISP::T
                 COMMON-LISP::T COMMON-LISP::T COMMON-LISP::T
                 COMMON-LISP::T COMMON-LISP::T COMMON-LISP::T
                 COMMON-LISP::T COMMON-LISP::T)
             COMMON-LISP::*)
         ACL2::EXPAND-ABBREVIATIONS ACL2::TYPE-SET-PRIMITIVE
         ACL2::PC-RELIEVE-HYPS1 ACL2::ADD-LINEAR-LEMMA-FINISH
         ACL2::DEFABSSTOBJ-FN ACL2::NEXT-PEQUIVS-ALIST
         ACL2::FIND-APPLICABLE-HINT-SETTINGS1 ACL2::WATERFALL0
         ACL2::TRANSLATE11-MV-LET ACL2::CUSTOM-KEYWORD-HINT-INTERPRETER
         ACL2::PROVE-TERMINATION-NON-RECURSIVE ACL2::TYPE-SET-REC)) 
(COMMON-LISP::PROCLAIM
    '(COMMON-LISP::FTYPE
         (COMMON-LISP::FUNCTION
             (COMMON-LISP::T COMMON-LISP::T COMMON-LISP::T
                 COMMON-LISP::T COMMON-LISP::T COMMON-LISP::T
                 COMMON-LISP::T COMMON-LISP::T COMMON-LISP::T)
             COMMON-LISP::*)
         ACL2::CHK-RAISE-PORTCULLIS ACL2::PROVE-LOOP1 ACL2::REWRITE-IF1
         ACL2::TYPE-SET-AND-RETURNED-FORMALS-WITH-RULE1
         ACL2::SUBST-EQUIV-EXPR1-LST ACL2::TRANSLATE11
         ACL2::UNRELIEVED-HYPS ACL2::MULT-LOOKUP-HYP
         ACL2::TRANSLATE11-FLET-ALIST ACL2::TRANSLATE-LMI/INSTANCE
         ACL2::MAKE-CERTIFICATE-FILE1 ACL2::MAKE-CERTIFICATE-FILE
         ACL2::CHK-ACCEPTABLE-REWRITE-RULE2
         ACL2::OK-TO-FIRE-SIGNATURE-RULEP
         ACL2::TAU-GET-STATS-ON-SIGNATURES1 ACL2::BDD-CLAUSE1
         ACL2::PROCESS-DEFATTACH-ARGS1 ACL2::FORWARD-CHAIN-TOP
         ACL2::DEFCHOOSE-CONSTRAINT ACL2::WATERFALL-MSG
         ACL2::PC-RELIEVE-HYPS ACL2::MV-ATF-2
         ACL2::CHK-ACCEPTABLE-LINEAR-RULE2 ACL2::REWRITE-RECOGNIZER
         ACL2::TYPE-SET-< ACL2::SUBST-EQUIV-EXPR1
         ACL2::CHK-ACCEPTABLE-DEFINITION-RULE
         ACL2::CHK-EVALUATOR-USE-IN-RULE ACL2::PROCESS-BACKTRACK-HINT
         ACL2::DEFUNS-FN-SHORT-CUT ACL2::REWRITE-SOLIDIFY
         ACL2::FIND-APPLICABLE-HINT-SETTINGS ACL2::PRINT-GV-FORM
         ACL2::RELIEVE-DEPENDENT-HYPS
         ACL2::LOAD-THEORY-INTO-ENABLED-STRUCTURE ACL2::WATERFALL-STEP
         ACL2::TYPE-SET ACL2::TRANSLATE-STOBJ-CALLS
         ACL2::RESUME-SUSPENDED-ASSUMPTION-REWRITING1
         ACL2::CHK-CERTIFICATE-FILE1 ACL2::MAKE-CERTIFICATE-FILES
         ACL2::REMOVE-TRIVIAL-EQUIVALENCES
         ACL2::ADD-DEFINITION-RULE-WITH-TTREE
         ACL2::TRANSLATE-LMI/FUNCTIONAL-INSTANCE ACL2::PC-MAIN
         ACL2::TRANSLATE11-FLET-ALIST1 ACL2::SUBST-EQUIV-EXPR
         ACL2::EVISCERATE1-LST
         ACL2::CHK-ACCEPTABLE-DEFINITION-INSTALL-BODY
         ACL2::MULT-SEARCH-TYPE-ALIST ACL2::TRANSLATE-ABSSTOBJ-FIELD
         ACL2::TYPE-SET-AND-RETURNED-FORMALS-WITH-RULES ACL2::TABLE-FN1
         ACL2::APPLY-SIGNATURE-TAU-RULE)) 
(COMMON-LISP::PROCLAIM
    '(COMMON-LISP::FTYPE
         (COMMON-LISP::FUNCTION
             (COMMON-LISP::FIXNUM COMMON-LISP::FIXNUM COMMON-LISP::T
                 COMMON-LISP::T)
             COMMON-LISP::*)
         ACL2::CHECK-SUM1)) 
(COMMON-LISP::PROCLAIM
    '(COMMON-LISP::FTYPE
         (COMMON-LISP::FUNCTION
             (COMMON-LISP::T COMMON-LISP::T COMMON-LISP::T
                 COMMON-LISP::T COMMON-LISP::T COMMON-LISP::T
                 COMMON-LISP::T COMMON-LISP::T)
             COMMON-LISP::*)
         ACL2::EV-W-LST ACL2::CHK-ACCEPTABLE-LINEAR-RULE
         ACL2::GUESS-AND-PUTPROP-TYPE-PRESCRIPTION-LST-FOR-CLIQUE
         ACL2::PROVE-DEFATTACH-CONSTRAINT ACL2::LINEARIZE-LST
         ACL2::DEFTHM-FN1 ACL2::TRY-TYPE-SET-AND-CLAUSE
         ACL2::CHK-ACCEPTABLE-FORWARD-CHAINING-RULE
         ACL2::REDEFINITION-RENEWAL-MODE ACL2::DEFTHM-FN
         ACL2::GUARD-CLAUSES+ ACL2::TRANSLATE-BODIES1
         ACL2::FORWARD-CHAIN ACL2::SEARCH-GROUND-UNITS1
         ACL2::GUARD-CLAUSES-FOR-BODY ACL2::TRANSLATE-BODIES
         ACL2::DEFATTACH-MERGE-INTO-COMPONENT
         ACL2::TYPE-ALIST-CLAUSE-FINISH ACL2::MAKE-RECOGNIZER-TUPLE
         ACL2::PROCESS-EQUATIONAL-POLYS ACL2::EVISCERATE1
         ACL2::RELEVANT-CONSTRAINTS1 ACL2::TAU-ASSUME-BASIC
         ACL2::UNCOVERED-EQUIVS-ALIST ACL2::DEFATTACH-MERGE-COMPONENTS
         ACL2::EV-W ACL2::MFC-RELIEVE-HYP-FN
         ACL2::CLEANSE-TYPE-PRESCRIPTIONS ACL2::MFC-RELIEVE-HYP-RAW
         ACL2::CHK-ACCEPTABLE-LINEAR-RULE1 ACL2::TRANSLATE-RULE-CLASS1
         ACL2::ADD-POLYS ACL2::CHK-META-FUNCTION ACL2::PC-PROVE
         ACL2::RESUME-SUSPENDED-ASSUMPTION-REWRITING ACL2::INDUCT
         ACL2::TAU-BOUNDER-HYP-EXTRACTION
         ACL2_*1*_ACL2::MFC-RELIEVE-HYP-FN ACL2::EVISCERATE-STOBJS
         ACL2::SETUP-SIMPLIFY-CLAUSE-POT-LST ACL2::TRANSLATE11-FLET
         ACL2::GUESS-MEASURE ACL2::DEFATTACH-CONSTRAINT-REC
         ACL2::EVISCERATE-STOBJS1 ACL2::CHK-DEFABSSTOBJ-METHOD-LEMMAS
         ACL2::CHK-ACCEPTABLE-TYPE-PRESCRIPTION-RULE
         ACL2::UBT-UBU-QUERY ACL2::PC-RELIEVE-HYP
         ACL2::PROVE-GUARD-CLAUSES ACL2::ADD-LINEAR-ASSUMPTION
         ACL2::EV-FNCALL-W ACL2::TAU-TERM-LST
         ACL2::APPLY-TOP-HINTS-CLAUSE ACL2::CHK-ACCEPTABLE-CERTIFY-BOOK
         ACL2::TRANSLATE11-WORMHOLE-EVAL
         ACL2::CHK-ACCEPTABLE-REWRITE-RULE1 ACL2::CLAUSIFY-INPUT1
         ACL2::MFC-RW-RAW ACL2::ADD-POLYNOMIAL-INEQUALITIES
         ACL2::SIMPLE-TRANSLATE-AND-EVAL ACL2::WATERFALL-STEP1
         ACL2::TYPE-ALIST-CLAUSE ACL2::FORCE-ASSUMPTION
         ACL2::TAU-ASSUME ACL2::CHK-ACCEPTABLE-REWRITE-RULE
         ACL2::EVISCERATE-STOBJS-TOP ACL2::CHK-REWRITE-RULE-WARNINGS
         ACL2::CHK-ACCEPTABLE-LD-FN1 ACL2::TAU-VISIT-EVENT
         ACL2::EXPAND-AND-OR)) 
(COMMON-LISP::PROCLAIM
    '(COMMON-LISP::FTYPE
         (COMMON-LISP::FUNCTION
             (COMMON-LISP::T COMMON-LISP::T COMMON-LISP::T
                 COMMON-LISP::T COMMON-LISP::T COMMON-LISP::T
                 COMMON-LISP::T COMMON-LISP::T COMMON-LISP::T
                 COMMON-LISP::T COMMON-LISP::T COMMON-LISP::T
                 COMMON-LISP::T COMMON-LISP::T COMMON-LISP::T)
             COMMON-LISP::*)
         ACL2::PC-REWRITE*-1 ACL2::PUT-INDUCTION-INFO
         ACL2::RELIEVE-HYP-SYNP ACL2::PC-REWRITE*)) 
(COMMON-LISP::PROCLAIM
    '(COMMON-LISP::FTYPE
         (COMMON-LISP::FUNCTION
             (COMMON-LISP::T COMMON-LISP::T COMMON-LISP::T
                 COMMON-LISP::T COMMON-LISP::FIXNUM COMMON-LISP::T
                 COMMON-LISP::T COMMON-LISP::T)
             COMMON-LISP::*)
         ACL2::BDD ACL2::BDD-LIST)) 
(COMMON-LISP::PROCLAIM
    '(COMMON-LISP::FTYPE
         (COMMON-LISP::FUNCTION
             (COMMON-LISP::T COMMON-LISP::T COMMON-LISP::FIXNUM
                 COMMON-LISP::FIXNUM COMMON-LISP::T COMMON-LISP::T
                 COMMON-LISP::T COMMON-LISP::T COMMON-LISP::T
                 COMMON-LISP::T COMMON-LISP::T COMMON-LISP::T
                 COMMON-LISP::T COMMON-LISP::T COMMON-LISP::T
                 COMMON-LISP::T COMMON-LISP::T)
             COMMON-LISP::*)
         ACL2::ADD-LINEAR-LEMMA ACL2::REWRITE-LINEAR-TERM-LST
         ACL2::MULTIPLY-POTS-SUPER-FILTER ACL2::REWRITE-PRIMITIVE
         ACL2::MULTIPLY-POTS-FILTER ACL2::ADD-LINEAR-LEMMAS
         ACL2::ADD-POLYS-AND-LEMMAS ACL2::ADD-POLYS-AND-LEMMAS2-NL
         ACL2::MULTIPLY-POLYS ACL2::REWRITE-WITH-LEMMA
         ACL2::ADD-POLYS-AND-LEMMAS1-NL ACL2::REWRITE-WITH-LEMMAS1
         ACL2::REWRITE-FNCALL ACL2::REWRITE-LINEAR-TERM
         ACL2::MULTIPLY-POTS ACL2::ADD-POLYS-AND-LEMMAS1
         ACL2::ADD-DISJUNCT-POLYS-AND-LEMMAS)) 
(COMMON-LISP::PROCLAIM
    '(COMMON-LISP::FTYPE
         (COMMON-LISP::FUNCTION
             (COMMON-LISP::T COMMON-LISP::T COMMON-LISP::T
                 COMMON-LISP::T COMMON-LISP::T COMMON-LISP::T
                 COMMON-LISP::T COMMON-LISP::T COMMON-LISP::T
                 COMMON-LISP::T COMMON-LISP::T COMMON-LISP::T
                 COMMON-LISP::T COMMON-LISP::T)
             COMMON-LISP::*)
         ACL2::CHK-ACCEPTABLE-DEFABSSTOBJ1
         ACL2::PROVE-TERMINATION-RECURSIVE ACL2::INCLUDE-BOOK-FN1
         ACL2::EVAL-AND-TRANSLATE-HINT-EXPRESSION
         ACL2::PROVE-TERMINATION ACL2::ADVANCE-FC-ACTIVATION1
         ACL2::CHK-ACCEPTABLE-DEFABSSTOBJ)) 
(COMMON-LISP::PROCLAIM
    '(COMMON-LISP::FTYPE
         (COMMON-LISP::FUNCTION
             (COMMON-LISP::T COMMON-LISP::T COMMON-LISP::T
                 COMMON-LISP::FIXNUM COMMON-LISP::T)
             COMMON-LISP::*)
         ACL2::SOME-ONE-WAY-UNIFY-CST-LST)) 
(COMMON-LISP::PROCLAIM
    '(COMMON-LISP::FTYPE
         (COMMON-LISP::FUNCTION
             (COMMON-LISP::T COMMON-LISP::T COMMON-LISP::T
                 COMMON-LISP::T COMMON-LISP::T COMMON-LISP::T
                 COMMON-LISP::T COMMON-LISP::T COMMON-LISP::T
                 COMMON-LISP::T COMMON-LISP::T COMMON-LISP::T
                 COMMON-LISP::T)
             COMMON-LISP::*)
         ACL2::EVAL-EVENT-LST ACL2::ADVANCE-FC-ACTIVATION3
         ACL2::CUSTOM-KEYWORD-HINT-INTERPRETER1
         ACL2::CHK-ACCEPTABLE-CERTIFY-BOOK1 ACL2::WATERFALL1-LST
         ACL2::WATERFALL0-WITH-HINT-SETTINGS
         ACL2::ADVANCE-FC-ACTIVATION2 ACL2::TYPE-SET-WITH-RULE1
         ACL2::TYPE-SET-WITH-RULES)) 
(COMMON-LISP::PROCLAIM
    '(COMMON-LISP::FTYPE
         (COMMON-LISP::FUNCTION
             (COMMON-LISP::T COMMON-LISP::T COMMON-LISP::T
                 COMMON-LISP::T COMMON-LISP::T COMMON-LISP::FIXNUM
                 COMMON-LISP::T COMMON-LISP::T COMMON-LISP::T)
             COMMON-LISP::*)
         ACL2::BDD-ALIST)) 
(COMMON-LISP::PROCLAIM
    '(COMMON-LISP::FTYPE
         (COMMON-LISP::FUNCTION
             (COMMON-LISP::T COMMON-LISP::T COMMON-LISP::T
                 COMMON-LISP::T COMMON-LISP::T COMMON-LISP::T
                 COMMON-LISP::T COMMON-LISP::T COMMON-LISP::T
                 COMMON-LISP::T COMMON-LISP::T COMMON-LISP::T
                 COMMON-LISP::T COMMON-LISP::T COMMON-LISP::T
                 COMMON-LISP::T COMMON-LISP::T COMMON-LISP::FIXNUM
                 COMMON-LISP::FIXNUM COMMON-LISP::T COMMON-LISP::T
                 COMMON-LISP::T COMMON-LISP::T COMMON-LISP::T
                 COMMON-LISP::T COMMON-LISP::T COMMON-LISP::T
                 COMMON-LISP::T COMMON-LISP::T COMMON-LISP::T
                 COMMON-LISP::T COMMON-LISP::T)
             COMMON-LISP::*)
         ACL2::RELIEVE-HYPS1-FREE-2)) 
(COMMON-LISP::PROCLAIM
    '(COMMON-LISP::FTYPE
         (COMMON-LISP::FUNCTION
             (COMMON-LISP::FIXNUM COMMON-LISP::FIXNUM COMMON-LISP::T
                 COMMON-LISP::T COMMON-LISP::T COMMON-LISP::T
                 COMMON-LISP::T COMMON-LISP::T COMMON-LISP::T
                 COMMON-LISP::T)
             COMMON-LISP::*)
         ACL2::MAKE-IF ACL2::MAKE-IF-FOR-OP)) 
(COMMON-LISP::PROCLAIM
    '(COMMON-LISP::FTYPE
         (COMMON-LISP::FUNCTION
             (COMMON-LISP::T COMMON-LISP::T COMMON-LISP::T
                 COMMON-LISP::T COMMON-LISP::T COMMON-LISP::T
                 COMMON-LISP::T COMMON-LISP::T COMMON-LISP::T
                 COMMON-LISP::T COMMON-LISP::T COMMON-LISP::T
                 COMMON-LISP::T COMMON-LISP::T COMMON-LISP::T
                 COMMON-LISP::T COMMON-LISP::T COMMON-LISP::T
                 COMMON-LISP::T COMMON-LISP::T)
             COMMON-LISP::*)
         ACL2::TYPE-SET-RELIEVE-HYPS-FREE)) 
(COMMON-LISP::PROCLAIM
    '(COMMON-LISP::FTYPE
         (COMMON-LISP::FUNCTION
             (COMMON-LISP::T COMMON-LISP::T COMMON-LISP::T
                 COMMON-LISP::T COMMON-LISP::T COMMON-LISP::T
                 COMMON-LISP::T COMMON-LISP::T COMMON-LISP::T
                 COMMON-LISP::T COMMON-LISP::T COMMON-LISP::T
                 COMMON-LISP::T COMMON-LISP::T COMMON-LISP::T
                 COMMON-LISP::T COMMON-LISP::T)
             COMMON-LISP::*)
         ACL2::TYPE-SET-RELIEVE-HYPS ACL2::REWRITE-CLAUSE
         ACL2::PARSE-DEFEXEC-DCLS-1 ACL2::PARSE-DEFEXEC-DCLS)) 
(COMMON-LISP::PROCLAIM
    '(COMMON-LISP::FTYPE
         (COMMON-LISP::FUNCTION
             (COMMON-LISP::T COMMON-LISP::T COMMON-LISP::FIXNUM)
             COMMON-LISP::*)
         ACL2::BDD-QUOTEP)) 
(COMMON-LISP::PROCLAIM
    '(COMMON-LISP::FTYPE
         (COMMON-LISP::FUNCTION
             (COMMON-LISP::T COMMON-LISP::T COMMON-LISP::T
                 COMMON-LISP::T COMMON-LISP::T COMMON-LISP::FIXNUM
                 COMMON-LISP::T)
             COMMON-LISP::*)
         ACL2::COMBINE-IF-CSTS)) 
(COMMON-LISP::PROCLAIM
    '(COMMON-LISP::FTYPE
         (COMMON-LISP::FUNCTION
             (COMMON-LISP::FIXNUM COMMON-LISP::FIXNUM COMMON-LISP::T
                 COMMON-LISP::T COMMON-LISP::T COMMON-LISP::T
                 COMMON-LISP::T COMMON-LISP::T COMMON-LISP::T
                 COMMON-LISP::T COMMON-LISP::T)
             COMMON-LISP::*)
         ACL2::BDD-EV-FNCALL)) 
(COMMON-LISP::PROCLAIM
    '(COMMON-LISP::FTYPE
         (COMMON-LISP::FUNCTION
             (COMMON-LISP::T COMMON-LISP::T COMMON-LISP::T
                 COMMON-LISP::FIXNUM COMMON-LISP::T COMMON-LISP::T
                 COMMON-LISP::T)
             COMMON-LISP::*)
         ACL2::FMT0&V)) 
(COMMON-LISP::PROCLAIM
    '(COMMON-LISP::FTYPE
         (COMMON-LISP::FUNCTION
             (COMMON-LISP::T COMMON-LISP::T COMMON-LISP::T
                 COMMON-LISP::FIXNUM COMMON-LISP::FIXNUM COMMON-LISP::T
                 COMMON-LISP::T COMMON-LISP::T COMMON-LISP::T
                 COMMON-LISP::T COMMON-LISP::T COMMON-LISP::T
                 COMMON-LISP::T COMMON-LISP::T COMMON-LISP::T
                 COMMON-LISP::T COMMON-LISP::T COMMON-LISP::T)
             COMMON-LISP::*)
         ACL2::ADD-DISJUNCTS-POLYS-AND-LEMMAS
         ACL2::NON-LINEAR-ARITHMETIC ACL2::ADD-MULTIPLIED-POLYS-FILTER
         ACL2::MULTIPLY-POTS1 ACL2::MULTIPLY-POTS2 ACL2::REWRITE
         ACL2::MULTIPLY-ALISTS ACL2::MULTIPLY-ALISTS2
         ACL2::ADD-MULTIPLIED-POLYS ACL2::NON-LINEAR-ARITHMETIC1
         ACL2::ADD-TERMS-AND-LEMMAS ACL2::MULTIPLY-ALISTS1)) 
(COMMON-LISP::PROCLAIM
    '(COMMON-LISP::FTYPE
         (COMMON-LISP::FUNCTION
             (COMMON-LISP::T COMMON-LISP::T COMMON-LISP::T
                 COMMON-LISP::T COMMON-LISP::T COMMON-LISP::T
                 COMMON-LISP::FIXNUM COMMON-LISP::FIXNUM COMMON-LISP::T
                 COMMON-LISP::T COMMON-LISP::T COMMON-LISP::T
                 COMMON-LISP::T COMMON-LISP::T COMMON-LISP::T
                 COMMON-LISP::T COMMON-LISP::T COMMON-LISP::T
                 COMMON-LISP::T COMMON-LISP::T COMMON-LISP::T)
             COMMON-LISP::*)
         ACL2::RELIEVE-HYPS ACL2::RELIEVE-HYP)) 
(COMMON-LISP::PROCLAIM
    '(COMMON-LISP::FTYPE
         (COMMON-LISP::FUNCTION
             (COMMON-LISP::T COMMON-LISP::T COMMON-LISP::T
                 COMMON-LISP::T COMMON-LISP::T COMMON-LISP::T
                 COMMON-LISP::T COMMON-LISP::FIXNUM COMMON-LISP::FIXNUM
                 COMMON-LISP::T COMMON-LISP::T COMMON-LISP::T
                 COMMON-LISP::T COMMON-LISP::T COMMON-LISP::T
                 COMMON-LISP::T COMMON-LISP::T COMMON-LISP::T
                 COMMON-LISP::T COMMON-LISP::T COMMON-LISP::T
                 COMMON-LISP::T)
             COMMON-LISP::*)
         ACL2::MULTIPLY-POLYS1)) 
(COMMON-LISP::PROCLAIM
    '(COMMON-LISP::FTYPE
         (COMMON-LISP::FUNCTION
             (COMMON-LISP::T COMMON-LISP::T COMMON-LISP::FIXNUM
                 COMMON-LISP::T COMMON-LISP::T COMMON-LISP::T)
             COMMON-LISP::*)
         ACL2::SPELL-NUMBER ACL2::FMT1)) 
(COMMON-LISP::PROCLAIM
    '(COMMON-LISP::FTYPE
         (COMMON-LISP::FUNCTION
             (COMMON-LISP::STRING COMMON-LISP::STRING
                 COMMON-LISP::STRING COMMON-LISP::STRING COMMON-LISP::T
                 COMMON-LISP::T COMMON-LISP::FIXNUM COMMON-LISP::T
                 COMMON-LISP::T COMMON-LISP::T)
             COMMON-LISP::*)
         ACL2::FMT0*)) 
(COMMON-LISP::PROCLAIM
    '(COMMON-LISP::FTYPE
         (COMMON-LISP::FUNCTION
             (COMMON-LISP::T COMMON-LISP::T COMMON-LISP::FIXNUM
                 COMMON-LISP::T COMMON-LISP::T)
             COMMON-LISP::*)
         ACL2::LEFT-PAD-WITH-BLANKS)) 
(COMMON-LISP::PROCLAIM
    '(COMMON-LISP::FTYPE
         (COMMON-LISP::FUNCTION
             (COMMON-LISP::T COMMON-LISP::T COMMON-LISP::T
                 COMMON-LISP::T COMMON-LISP::T COMMON-LISP::T
                 COMMON-LISP::T COMMON-LISP::T COMMON-LISP::T
                 COMMON-LISP::T COMMON-LISP::T COMMON-LISP::T
                 COMMON-LISP::T COMMON-LISP::T COMMON-LISP::T
                 COMMON-LISP::T)
             COMMON-LISP::*)
         ACL2::WATERFALL0-OR-HIT ACL2::EXPAND-ABBREVIATIONS-LST)) 
(COMMON-LISP::PROCLAIM
    '(COMMON-LISP::FTYPE
         (COMMON-LISP::FUNCTION
             (COMMON-LISP::T COMMON-LISP::T COMMON-LISP::T
                 COMMON-LISP::T COMMON-LISP::T COMMON-LISP::FIXNUM
                 COMMON-LISP::FIXNUM COMMON-LISP::T COMMON-LISP::T
                 COMMON-LISP::T COMMON-LISP::T COMMON-LISP::T
                 COMMON-LISP::T COMMON-LISP::T COMMON-LISP::T
                 COMMON-LISP::T COMMON-LISP::T COMMON-LISP::T
                 COMMON-LISP::T COMMON-LISP::T)
             COMMON-LISP::*)
         ACL2::DEAL-WITH-DIVISION ACL2::DEAL-WITH-PRODUCT1
         ACL2::REWRITE-IF)) 
(COMMON-LISP::PROCLAIM
    '(COMMON-LISP::FTYPE
         (COMMON-LISP::FUNCTION
             (COMMON-LISP::T COMMON-LISP::T COMMON-LISP::T
                 COMMON-LISP::T COMMON-LISP::T COMMON-LISP::T
                 COMMON-LISP::T COMMON-LISP::T COMMON-LISP::T
                 COMMON-LISP::T COMMON-LISP::T COMMON-LISP::T
                 COMMON-LISP::T COMMON-LISP::T COMMON-LISP::T
                 COMMON-LISP::T COMMON-LISP::T COMMON-LISP::T)
             COMMON-LISP::*)
         ACL2::REWRITE-CLAUSE-LST)) 
(COMMON-LISP::PROCLAIM
    '(COMMON-LISP::FTYPE
         (COMMON-LISP::FUNCTION
             (COMMON-LISP::T COMMON-LISP::T COMMON-LISP::T
                 COMMON-LISP::T COMMON-LISP::T COMMON-LISP::T
                 COMMON-LISP::T COMMON-LISP::T COMMON-LISP::T
                 COMMON-LISP::T COMMON-LISP::T COMMON-LISP::T
                 COMMON-LISP::T COMMON-LISP::T COMMON-LISP::T
                 COMMON-LISP::T COMMON-LISP::T COMMON-LISP::T
                 COMMON-LISP::T COMMON-LISP::T COMMON-LISP::T
                 COMMON-LISP::T COMMON-LISP::T COMMON-LISP::T
                 COMMON-LISP::T COMMON-LISP::T COMMON-LISP::T)
             COMMON-LISP::*)
         ACL2::RELIEVE-HYPS1-ITER)) 
(COMMON-LISP::PROCLAIM
    '(COMMON-LISP::FTYPE
         (COMMON-LISP::FUNCTION
             (COMMON-LISP::T COMMON-LISP::T COMMON-LISP::T
                 COMMON-LISP::T COMMON-LISP::FIXNUM COMMON-LISP::FIXNUM
                 COMMON-LISP::T COMMON-LISP::T COMMON-LISP::T
                 COMMON-LISP::T COMMON-LISP::T COMMON-LISP::T
                 COMMON-LISP::T COMMON-LISP::T COMMON-LISP::T
                 COMMON-LISP::T COMMON-LISP::T COMMON-LISP::T
                 COMMON-LISP::T)
             COMMON-LISP::*)
         ACL2::DEAL-WITH-PRODUCT ACL2::DEAL-WITH-FACTOR
         ACL2::REWRITE-EQUAL)) 
(COMMON-LISP::PROCLAIM
    '(COMMON-LISP::FTYPE
         (COMMON-LISP::FUNCTION
             (COMMON-LISP::T COMMON-LISP::T COMMON-LISP::T
                 COMMON-LISP::T COMMON-LISP::T COMMON-LISP::T
                 COMMON-LISP::T COMMON-LISP::T COMMON-LISP::T
                 COMMON-LISP::T COMMON-LISP::T COMMON-LISP::T
                 COMMON-LISP::T COMMON-LISP::T COMMON-LISP::T
                 COMMON-LISP::T COMMON-LISP::T COMMON-LISP::T
                 COMMON-LISP::T COMMON-LISP::T COMMON-LISP::T
                 COMMON-LISP::T COMMON-LISP::T)
             COMMON-LISP::*)
         ACL2::DEFUNS-FN0)) 
(COMMON-LISP::PROCLAIM
    '(COMMON-LISP::FTYPE
         (COMMON-LISP::FUNCTION
             (COMMON-LISP::T COMMON-LISP::T COMMON-LISP::T
                 COMMON-LISP::T COMMON-LISP::T COMMON-LISP::T
                 COMMON-LISP::T COMMON-LISP::T COMMON-LISP::FIXNUM
                 COMMON-LISP::FIXNUM COMMON-LISP::T COMMON-LISP::T
                 COMMON-LISP::T COMMON-LISP::T COMMON-LISP::T
                 COMMON-LISP::T COMMON-LISP::T COMMON-LISP::T
                 COMMON-LISP::T COMMON-LISP::T COMMON-LISP::T
                 COMMON-LISP::T COMMON-LISP::T)
             COMMON-LISP::*)
         ACL2::REWRITE-ARGS)) 
(COMMON-LISP::PROCLAIM
    '(COMMON-LISP::FTYPE
         (COMMON-LISP::FUNCTION
             ((COMMON-LISP::VECTOR COMMON-LISP::T)
              (COMMON-LISP::VECTOR COMMON-LISP::T) COMMON-LISP::FIXNUM
              COMMON-LISP::FIXNUM)
             (COMMON-LISP::VECTOR COMMON-LISP::T))
         ACL2::STOBJ-COPY-ARRAY-SVREF)) 
(COMMON-LISP::PROCLAIM
    '(COMMON-LISP::FTYPE
         (COMMON-LISP::FUNCTION
             ((COMMON-LISP::VECTOR COMMON-LISP::FIXNUM)
              (COMMON-LISP::VECTOR COMMON-LISP::FIXNUM)
              COMMON-LISP::FIXNUM COMMON-LISP::FIXNUM)
             (COMMON-LISP::VECTOR COMMON-LISP::FIXNUM))
         ACL2::STOBJ-COPY-ARRAY-FIX-AREF)) 
(COMMON-LISP::PROCLAIM
    '(COMMON-LISP::FTYPE
         (COMMON-LISP::FUNCTION (COMMON-LISP::T COMMON-LISP::T)
             COMMON-LISP::CHARACTER)
         ACL2::SER-ENCODE-TO-STREAM)) 
(COMMON-LISP::PROCLAIM
    '(COMMON-LISP::FTYPE
         (COMMON-LISP::FUNCTION
             (COMMON-LISP::T COMMON-LISP::T COMMON-LISP::T
                 COMMON-LISP::T COMMON-LISP::T COMMON-LISP::T
                 COMMON-LISP::T COMMON-LISP::T COMMON-LISP::T
                 COMMON-LISP::T COMMON-LISP::T COMMON-LISP::T
                 COMMON-LISP::T COMMON-LISP::T COMMON-LISP::T
                 COMMON-LISP::T COMMON-LISP::T COMMON-LISP::T
                 COMMON-LISP::FIXNUM COMMON-LISP::FIXNUM COMMON-LISP::T
                 COMMON-LISP::T COMMON-LISP::T COMMON-LISP::T
                 COMMON-LISP::T COMMON-LISP::T COMMON-LISP::T
                 COMMON-LISP::T COMMON-LISP::T COMMON-LISP::T
                 COMMON-LISP::T COMMON-LISP::T COMMON-LISP::T)
             COMMON-LISP::*)
         ACL2::RELIEVE-HYPS1-FREE-1)) 
(COMMON-LISP::PROCLAIM
    '(COMMON-LISP::FTYPE
         (COMMON-LISP::FUNCTION
             (COMMON-LISP::T COMMON-LISP::T COMMON-LISP::T
                 COMMON-LISP::T COMMON-LISP::T COMMON-LISP::T
                 COMMON-LISP::T COMMON-LISP::T COMMON-LISP::T
                 COMMON-LISP::T COMMON-LISP::T COMMON-LISP::FIXNUM
                 COMMON-LISP::FIXNUM COMMON-LISP::T COMMON-LISP::T
                 COMMON-LISP::T COMMON-LISP::T COMMON-LISP::T
                 COMMON-LISP::T COMMON-LISP::T COMMON-LISP::T
                 COMMON-LISP::T COMMON-LISP::T COMMON-LISP::T
                 COMMON-LISP::T COMMON-LISP::T)
             COMMON-LISP::*)
         ACL2::RELIEVE-HYPS1)) 
(COMMON-LISP::PROCLAIM
    '(COMMON-LISP::FTYPE
         (COMMON-LISP::FUNCTION
             (COMMON-LISP::FIXNUM COMMON-LISP::INTEGER
                 COMMON-LISP::INTEGER)
             COMMON-LISP::T)
         ACL2::BOOLE$)) 
(COMMON-LISP::PROCLAIM
    '(COMMON-LISP::FTYPE
         (COMMON-LISP::FUNCTION
             (COMMON-LISP::T COMMON-LISP::T COMMON-LISP::T)
             COMMON-LISP::T)
         ACL2::OPEN-OUTPUT-CHANNEL-P ACL2::INTEGER-RANGE-P
         ACL2::CURRENT-THEORY1 ACL2::TRANSLATE-STOBJ-TYPE-TO-GUARD
         ACL2::IMMEDIATE-INSTANTIABLE-ANCESTORS ACL2::GUARD
         ACL2::SUBST-TYPE-ALIST1-CHECK ACL2::GETPROPS
         ACL2::INDUCTION-HYP-CLAUSE-SEGMENTS2 ACL2::FORMULA
         ACL2::EQUAL-EXCEPT-ON-NON-STOBJS ACL2::FSUBCOR-VAR-LST
         ACL2::STRONG-COMPOUND-RECOGNIZER-P ACL2::COLLECT-INSTANTIABLEP
         ACL2::SUBSTITUTE1 ACL2::FIND-NONTRIVIAL-RULERS-LST
         ACL2::REVAPPEND-DELETE-RUNES-BASED-ON-SYMBOLS1
         ACL2::MAKE-WORMHOLE-STATUS ACL2::PRINT-HYPS-TOP
         ACL2::SCAN-TO-LANDMARK-NUMBER ACL2::BIG-D-LITTLE-D-NAME1
         ACL2::ALWAYS-TESTED-AND-CHANGEDP ACL2::CONS-ASSOC-EQ-REC
         ACL2::TAKE-BY-INDICES ACL2::MAYBE-PRINT-NIL-GOAL-GENERATED
         ACL2::COUNT-LISTP ACL2::<? ACL2::PRETTYIFY-CLAUSE
         ACL2::PRINT-INDENTED-LIST-MSG ACL2::INDUCTION-MACHINES
         ACL2::UNION-GENEQV ACL2::ENABLED-RUNEP-STRING
         ACL2::GETPROP-X-LST ACL2::TILDE-*-ANCESTORS-STACK-MSG
         ACL2::ADD-LITERAL ACL2::DUMB-OCCUR-LST-EXCEPT
         ACL2::WARNED-NON-REC-FNS-TP-HYPS ACL2::HL-ADDR-OF-UNUSUAL-ATOM
         ACL2::WARNING-OFF-P1 ACL2::APPLY-INVERSE-SYMBOL-ALIST
         ACL2::HL-CACHE-SET ACL2::TAU-LIKE-PROPOSITIONP
         ACL2::EQUAL-MOD-ALIST ACL2::PUT-GLOBAL ACL2::LD-ALIST-RAW
         ACL2::PRIN1$ ACL2_*1*_ACL2::RETURN-LAST
         ACL2::RAW-INDEXED-INSTRS ACL2::CONGRUENT-STOBJSP
         ACL2::DISVAR-TYPE-ALIST ACL2::UNIFORM-DEFUN-MODES
         ACL2::DEFSTOBJ-FIELD-TEMPLATES ACL2::ASSOC2
         ACL2::POSITION-AC-EQ-EXEC$GUARD-CHECK
         ACL2::NEW-VERIFY-GUARDS-FNS1 ACL2::COLLECT-FFNNAMES-LST
         ACL2::PRUNE-PROOF-TREE ACL2::ABBREVIATIONP1-LST
         ACL2::PRETTYIFY-BLOCKED-FC-INST-HYP ACL2::DECODE-RECOG
         ACL2::EXPAND-SOME-NON-REC-FNS-IN-CLAUSES ACL2::UNTRANSLATE-AND
         ACL2::TRANSLATE-LMI/INSTANCE-FIX-ALIST
         ACL2::MERGE-ALIST1-LST-INTO-ALIST2
         ACL2::TILDE-*-RAW-SIMP-PHRASE ACL2::PRINT-ENCAPSULATE-MSG2
         ACL2::INFECT-NEW-POLYS ACL2::LD-KEYWORD-ALIASESP
         ACL2::EXPLODE-NONNEGATIVE-INTEGER
         ACL2::MARK-ATTACHMENT-DISALLOWED1 ACL2::COMMANDS-BACK-TO
         ACL2::ADD-LITERAL-SMART ACL2::TAU-SIMPLE-FORMP
         ACL2::TILDE-@-FREE-VARS-PHRASE ACL2::SUBST-FOR-NTH-ARG
         ACL2::SATISFYING-VIRTUAL-FC-ACTIVATIONP ACL2::INFORM-SIMPLIFY2
         ACL2::POSITION-AC-EQ-EXEC ACL2::TAG-TREE-OCCUR
         ACL2::ACCESSOR-ROOT ACL2::MEMBER-CHAR-STRINGP
         ACL2::TYPE-SET-BINARY-+-ALIST1 ACL2::MAY-NEED-SLASHES1
         ACL2::RENEW-NAME/OVERWRITE
         ACL2::ALREADY-USED-BY-FERTILIZE-CLAUSEP ACL2::ADD-TO-TAG-TREE!
         ACL2::ROLLOVER-IPRINT-AR ACL2::ARITY-MISMATCH-MSG
         ACL2::DEGREE-OF-MATCH1 ACL2::ADD-SPLITTERS-TO-TTREE1
         ACL2::ASET1-LST ACL2::SER-DECODE-AND-LOAD-PACKAGES
         ACL2::EXTEND-32-BIT-INTEGER-STACK
         ACL2::CURRENT-THEORY1-AUGMENTED ACL2::MERGE-EXTRA-INFO-LITS
         ACL2::SUBSEQ-LIST ACL2::MAKE-RECORD-CHANGER
         ACL2::MAKE-REWRITE-INSTR ACL2::INSERT-NEG-EVGS1 ACL2::PRINC$
         ACL2::PUT-MATCH-FREE-VALUE ACL2::DELETE-FROM-TTREE
         ACL2::PUT-DEFABSSTOBJ-INVARIANT-RISK
         ACL2::PRETTYIFY-CLAUSE-LST
         ACL2::EVENT-RESPONSIBLE-FOR-PROVED-CONSTRAINT
         ACL2::MEMBER-CLASS-NAME-RUNES ACL2::ALL-PICKS2R
         ACL2::COLLECT-<?-K-X ACL2::MAXIMAL-TERMS ACL2::PUT-BRR-LOCAL
         ACL2::PRINT-LDD ACL2::SUBCOR-VAR-LST
         ACL2::COLLECT-FC-STATUS-SITE-1 ACL2::THROW-NONEXEC-ERROR-P
         ACL2::TERM-DIFFICULTY1 ACL2::MAXIMAL-MULTIPLE-LST
         ACL2::HONS-ACONS! ACL2::PUT-STOBJS-IN-AND-OUTS1
         ACL2::HL-HSPACE-RESTORE-FAL-FOR-SERIALIZE
         ACL2::UNION-AUGMENTED-THEORIES-FN1 ACL2::VAR-COUNTS1-LST
         ACL2::ACL2X-ALISTP ACL2::SUBCOR-VAR1 ACL2::FN-STOBJ-UPDATES-P
         ACL2::DEPOSIT-TERM ACL2::GLOBAL-SET ACL2::CONJOIN-CLAUSE-SETS+
         ACL2::FIND-RULES-OF-RUNE1 ACL2::TS-BUILDER-MACRO1
         ACL2::POSITION-EQUAL-AC ACL2::FLUSH-TRIP
         ACL2::MAYBE-COERCE-OVERWRITE-TO-ERASE
         ACL2::TRANSLATE-DECLARATION-TO-GUARD1 ACL2::KEY-LESSEQP
         ACL2::INFORM-SIMPLIFY3 ACL2::STRICT-MERGE-SYMBOL-<
         ACL2::CONS-TAG-TREES1 ACL2::MERGE-TESTS-AND-ALISTS-LSTS
         ACL2::ALL-CALLS-TEST-ALIST ACL2::FIND-CLAUSES1
         ACL2::EXT-ANCESTORS-ATTACHMENTS4 ACL2::MAKE-ACCESS-BINDINGS
         ACL2::SATISFYING-VIRTUAL-FC-ACTIVATION1P
         ACL2::INSTALL-FOR-ADD-TRIP ACL2::SUBST-EXPR ACL2::PAIR-INDICES
         ACL2::GEN-NEW-NAME-IN-PACKAGE-OF-SYMBOL ACL2::POOL-LST1
         ACL2::CANCEL1 ACL2::EXTRACT-AND-CLASSIFY-LEMMAS
         ACL2::MF-NOTE-ARITY ACL2::EXPANDED-NEW-VARS-IN-POT-LST1
         ACL2::UPDATE-FOR-REDO-FLAT ACL2::EV-FNCALL-MSG
         ACL2::ADD-META-RULE1 ACL2::OPEN-OUTPUT-CHANNEL-P1
         ACL2::PUT-CLTL-COMMAND ACL2::MAYBE-SUBSUMES ACL2::E/D-FN
         ACL2::BIG-D-LITTLE-D-CLIQUE ACL2::HL-MAKE-FAST-NORM-KEYS
         ACL2::MERGE-ACCUMULATED-PERSISTENCE-AUX
         ACL2::SET-DIFFERENCE-AUGMENTED-THEORIES-FN1
         ACL2::ASSUME-TRUE-FALSE-ERROR
         ACL2::INSTALL-FOR-ADD-TRIP-HCOMP-BUILD
         ACL2::DELETE-BY-POSITION
         ACL2::REVAPPEND-DELETE-AUGMENTED-RUNES-BASED-ON-SYMBOLS
         ACL2::TYPE-SET-<-ALIST1 ACL2::PRINT-OBJECTS
         ACL2::ACTUAL-STOBJS-OUT1 ACL2::INVISIBLE-FNS
         ACL2::SHORTEST-POLYS-WITH-VAR1 ACL2::TILDE-*-ALIST-PHRASE
         ACL2::MERGE-SYMBOL-< ACL2::PRINT-PROOF-TREE1
         ACL2::UPDATE-BDDNOTE-WITH-TERM ACL2::TILDE-@-LMI-PHRASE
         ACL2::TRANSLATE-DECLARATION-TO-GUARD-VAR-LST
         ACL2::INTERSECTION-THEORIES-FN ACL2::SET-W
         ACL2::INCREMENT-PROOF-TREE-POP-CLAUSE
         ACL2::SYSFILE-TO-FILENAME-INCLUDE-BOOK-ALIST
         ACL2::GUARD-OR-TERMINATION-THEOREM-MSG
         ACL2::INFECT-NEW-TYPE-ALIST-ENTRIES
         ACL2::ADD-ASSUMPTION-WITH-WEAK-TYPE-ALIST
         ACL2::UNTRANSLATE-LST ACL2::ABBREVIATIONP1
         ACL2_*1*_ACL2::WORMHOLE-EVAL
         ACL2::GEN-FORMALS-FROM-PRETTY-FLAGS1 ACL2::DISVAR-TYPE-ALIST1
         ACL2::MEMOIZE-FN-INIT ACL2::REPLACE-REWRITE-RULE-RUNE
         ACL2::TRANSLATE-DECLARATION-TO-GUARD/INTEGER ACL2::THE-CHECK
         ACL2::REPLACE-CLAUSE ACL2::LATEST-BODY
         ACL2::COLLECT-PEQUIVS-OF-RUNE ACL2::PUT-ASSOC-RW-CACHE1
         ACL2::VALUE-TRIPLE-FN ACL2::ENABLED-LMI-NAMES
         ACL2::INSTANTIABLE-ANCESTORS ACL2::PRINT-TERMS
         ACL2::ELIDE-LOCALS ACL2::PROJECT-OUT-COLUMNS-I-AND-J
         ACL2::CHANGE-OR-HIT-HISTORY-ENTRY ACL2::DMR-INTERP
         ACL2::DO-NOT-INDUCT-MSG ACL2::ENABLED-XFNP ACL2::STOBJP
         ACL2::ALL-PICKS2 ACL2::MV-NTH-LIST ACL2::COLLECT-<?-X-K
         ACL2::RENEW-NAME ACL2::MAXIMAL-ELEMENTS-APPLY
         ACL2::EXPANSION-ALIST-PKG-NAMES0 ACL2::EQUAL-MOD-ALIST-LST
         ACL2::DEFEVALUATOR-FORM/DEFTHM-HINTS ACL2::TOO-MANY-POLYSP
         ACL2::CONTROLLER-COMPLEXITY ACL2::STRIP-BRANCHES
         ACL2::CHANGE-BY-POSITION ACL2::COLLECTABLE-FNP
         ACL2::REMOVE-BY-INDICES ACL2::MAXIMAL-ELEMENTS
         ACL2::CANONICAL-ANCESTORS ACL2::PUSH-ANCESTOR
         ACL2::SUBSUMES-BUT-FOR-ONE-NEGATION
         ACL2::BIG-C-LITTLE-C-COMMAND-BLOCK
         ACL2::TRANSLATE-DECLARATION-TO-GUARD ACL2::TILDE-*-&V-STRINGS
         ACL2::FNCALL-TERM ACL2::DUMB-FN-COUNT-1
         ACL2::CANONICAL-DIRNAME! ACL2::RENEW-NAMES
         ACL2::ALL-CALLS-ALIST ACL2::FREE-VARS-IN-FC-HYPS
         ACL2::PUT-ASSOC-EQ-EXEC$GUARD-CHECK ACL2::IF-COMPILE-FORMAL
         ACL2::PRINT-LDDS ACL2::REMOVE1-BY-POSITION
         ACL2::UPDATE-MEMO-ENTRIES-FOR-ATTACHMENTS
         ACL2::THE-NAMEX-SYMBOL-CLASS1
         ACL2::FILTER-DISABLED-EXPAND-TERMS
         ACL2::OPTIMIZE-STOBJ-RECOGNIZERS1 ACL2::TAU-SIGNATURE-FORMP
         ACL2::PRINT-ENCAPSULATE-MSG1 ACL2::MAYBE-EXTEND-TAG-TREE
         ACL2::PUT-INVARIANT-RISK1 ACL2::UPDATE-MEMO-MAX-SIZES
         ACL2::OPTIMIZE-STOBJ-RECOGNIZERS ACL2::COMPILE-CERTIFIED-FILE
         ACL2::POSN-FIRST-NON-EVENT ACL2::GUARD-THEOREM
         ACL2::MEMBER-EQUAL-MOD-ALIST ACL2::MAXIMAL-TERMS1
         ACL2::INCLUDE-BOOK-ER-WARNING-SUMMARY
         ACL2::MAYBE-ONE-WAY-UNIFY-LST ACL2::MAKE-DISJUNCTIVE-CLAUSE-ID
         ACL2::FALSIFYING-PAIR-P ACL2::CHECKPOINT-WORLD1
         ACL2::PUT-STOBJS-IN-AND-OUTS ACL2::RULE-NAME-DESIGNATORP
         ACL2::TRY-CLAUSE ACL2::DISCOVER-TAU-PRED ACL2::CHK-ARGLIST-MSG
         ACL2::ALL-FNNAMES1-EXEC ACL2::PUTPROP-RECURSIVEP-LST
         ACL2::ILLEGAL ACL2::RECOVER-WORLD1 ACL2::TAU-SIMPLE-IMPLICANTS
         ACL2::MAP-RETURNED-FORMALS-VIA-FORMALS
         ACL2::NON-RECURSIVE-FNNAMES-LST ACL2::DEFUN-CTX
         ACL2::MERGE-INTO-ALIST ACL2::INVISIBLE-FNS-ENTRYP
         ACL2::RESIZE-LIST ACL2::STORE-STOBJS-OUT
         ACL2::TILDE-*-UNTRANSLATE-LST-PHRASE
         ACL2::UNION-LASTN-PC-TAG-TREES ACL2::MATCH-CLAUSE
         ACL2::CONJOIN-BOUNDING-INTERVALS
         ACL2::COLLECT-FC-STATUS-SITE-4
         ACL2::ANTAGONISTIC-TESTS-AND-ALISTS-LSTSP
         ACL2::PRIMITIVE-RECURSIVE-CALLP ACL2::OWNED-VARS
         ACL2::TT-PRINT-MSG ACL2::GET-COMMAND-SEQUENCE-FN1
         ACL2::ANCESTRAL-FFN-SYMBS-LST ACL2::CHK-RETURN-LAST-ENTRY
         ACL2::PRINT-CERTIFY-BOOK-STEP-4 ACL2::NEW-DEFPKG-LIST
         ACL2::ORACLE-APPLY-GUARD ACL2::GOOD-BOUNDS-IN-POT
         ACL2::CONJOIN-INTO-ALIST ACL2::TAU-DATA-FNS
         ACL2::RESTORE-BRR-GLOBALS1 ACL2::PRIMITIVE-RECURSIVE-ARGP
         ACL2::NAMES-OF-SYMBOLS-IN-PACKAGE
         ACL2::DESTRUCTOR-APPLIED-TO-VARSP
         ACL2::DEFSTOBJ-AXIOMATIC-DEFS ACL2::CORRESPONDING-ENCAP-EVENTS
         ACL2::POLY-SET ACL2::INFORM-SIMPLIFY1
         ACL2::MERGE-INTO-EXPANSION-ALIST1
         ACL2::WATERFALL-PRINT-CLAUSE-BODY
         ACL2::DECORATE-FORCED-GOALS-1-LST
         ACL2::EV-FNCALL-NULL-BODY-ER-MSG ACL2::GUARD-LST
         ACL2::REDUNDANT-DEFCHOOSEP ACL2::LATCH-STOBJS
         ACL2::ACCUMULATE-RW-CACHE? ACL2::PUTPROP-QUICK-BLOCK-INFO-LST
         ACL2::DEFATTACH-COMPONENT-HAS-OWNER ACL2::TYPE-SET-<-ALIST
         ACL2::TERM-ORDER1 ACL2::PRINT-VERIFY-GUARDS-MSG
         ACL2::REDUNDANT-DEFABSSTOBJP
         ACL2::TILDE-@-ILLEGAL-CLAUSE-PROCESSOR-SIG-MSG
         ACL2::MERGE-LST1-INTO-ALIST2-LST ACL2::CHK-STOBJ-LET/UPDATERS1
         ACL2::INSTALL-DISJUNCT-INTO-PROOF-TREE ACL2::ADD-REWRITE-ARGS
         ACL2::SPLICE-INSTRS1 ACL2::UNCOVERED-EQUIVS
         ACL2::ATTACHMENT-PAIRS ACL2::VAR-COUNTS1
         ACL2::BIG-D-LITTLE-D-NAME ACL2::RW-CACHE-LIST-LOOKUP
         ACL2::BOUNDS-POLYS-WITH-VAR ACL2::EXTEND-PATHNAME
         ACL2::MULTIPLY-ALIST-AND-CONST ACL2::SYSTEM-VERIFY-GUARDS-FN
         ACL2::OPEN-INPUT-CHANNEL-P ACL2::PUT-ASSOC-EQL-EXEC
         ACL2::COMMUTATIVE-P ACL2::ADD-PAIR
         ACL2::OPTIMIZE-STOBJ-RECOGNIZERS1-LST
         ACL2::HIDE-IGNORED-ACTUALS ACL2::ABSOLUTE-PATHNAME-STRING-P
         ACL2::USER-STOBJ-ALIST-SAFE ACL2::PUT-CDR-ASSOC-QUERY-ID
         ACL2::TYPE-SET-BINARY-*-ALIST ACL2::IF*
         ACL2::<?-NUMBER-V-RATIONAL ACL2::EXPLODE-ATOM+
         ACL2::SUBSUMPTION-REPLACEMENT-LOOP ACL2::WRITE-BYTE$
         ACL2::BOOL-MASK1 ACL2::CONTROLLER-COMPLEXITY1
         ACL2::ENABLED-RUNEP ACL2::TRANSLATE-DECLARATION-TO-GUARD-LST
         ACL2::MAYBE-ONE-WAY-UNIFY ACL2::TAU-LIKE-TERM-LISTP
         ACL2::PUT-ASSOC-EQUAL-FAST ACL2::EVALUATOR-CLAUSES
         ACL2::MAKE-NEW-GOALS ACL2::SER-DECODE-AND-RESTORE-FALS
         ACL2::APPLY-USER-STOBJ-ALIST-OR-KWOTE
         ACL2::REDUNDANT-DEFSTOBJP ACL2::CHK-MACRO-ARGLIST-MSG
         ACL2::PRINT-ABBREVIATIONS ACL2::ADD-NEW-NEVER-UNTOUCHABLE-FNS
         ACL2::CONS-ABSOLUTE-EVENT-NUMBERS ACL2::MERGE-LEXORDER
         ACL2::LOOKUP-WORLD-INDEX ACL2::SHOW-POLY1 ACL2::POLY-WEAKERP
         ACL2::NEW-AND-UGLY-LINEAR-VARSP
         ACL2::HL-HSPACE-HONS-EQUAL-LITE ACL2::REFINEMENTP
         ACL2::FREE-VARS-IN-HYPS-CONSIDERING-BIND-FREE
         ACL2::SET-BODY-FN1 ACL2::SPLIT-ON-ASSUMPTIONS
         ACL2::FIRST-NOMINATION ACL2::THEORY-WARNING-FNS
         ACL2::MAKE-DISJUNCTIVE-GOAL-SPEC
         ACL2::ADD-CONGRUENCE-RULE-TO-CONGRUENCE
         ACL2::INCLUDE-BOOK-DIR-ALIST-ENTRY-P ACL2::PRINT-IDATE
         ACL2::INDUCTION-MACHINE-FOR-FN ACL2::COLLECT-MONADIC-BOOLEANS
         ACL2::MERGE-LST1-INTO-ALIST2
         ACL2::PUTPROP-HEREDITARILY-CONSTRAINED-FNNAMES-LST
         ACL2::DEFSTOBJ-TEMPLATE ACL2::SWITCH-VARP
         ACL2::TILDE-*-ALIST-PHRASE1 ACL2::TERM-ORDER+
         ACL2::PUT-ABSSTOBJS-IN-AND-OUTS
         ACL2::COLLECT-CONGRUENCE-RULES-OF-RUNE-IN-GENEQV-LST
         ACL2::SECOND-NOMINATION ACL2::GOAL-TREE-CHOOSE-DISJUNCT
         ACL2::INSTALL-PROOF-SUPPORTERS-ALIST ACL2::NEW-VARS-IN-POT-LST
         ACL2::MAKE-VERIFY-TERMINATION-DEF ACL2::SUBCOR-VAR
         ACL2::CONTAINS-AFFINITY ACL2::MAKE-LIST-AC
         ACL2::COLLECT-SATISFYING-FC-ACTIVATIONS ACL2::SELECT-STOBJ
         ACL2::PRINT-OBJECT$ ACL2::MEMBER-ONE-WAY-UNIFY1
         ACL2::TYPE-SET-BINARY-*-ALIST1 ACL2::STOBJ-FIELD-ACCESSOR-P
         ACL2::REDUNDANT-LABELP ACL2::NUMBER-OF-DIGITS
         ACL2::COLLECT-SATISFYING-FC-DERIVATIONS
         ACL2::INSTALL-PROOF-SUPPORTERS ACL2::MAXIMAL-MULTIPLE
         ACL2::POP-TIMER ACL2::UNPROTECTED-EXPORT-P ACL2::NULL-BODY-ER
         ACL2::PRINT-RUNES-SUMMARY ACL2::ACCUMULATE-RW-CACHE
         ACL2::FFNNAMEP-HIDE-LST ACL2::FFNNAMEP-HIDE
         ACL2::COLLECT-FFNNAMES ACL2::TT-PRINT?
         ACL2::REMOVE-ANCESTOR-LITERALS-FROM-PAIRS1
         ACL2::SET-DIFFERENCE-EQ-SORTED
         ACL2::SOME-CONTROLLER-POCKET-CONSTANT-AND-NON-CONTROLLER-SIMPLERP
         ACL2::PUT-ASSOC-RW-CACHE ACL2::PRINT-GOVERNORS-TOP
         ACL2::STORE-STOBJS-INS ACL2::CHANGED-POT-VARS
         ACL2::MAYBE-PRINT-MACROEXPANSION ACL2::OPEN-INPUT-CHANNEL-P1
         ACL2::UNIVERSAL-THEORY-FN1
         ACL2::POSITION-AC-EQL-EXEC$GUARD-CHECK
         ACL2::TAU-BIG-SWITCH-FORMP ACL2::CLEANUP-IF-EXPR
         ACL2::POSITION-AC-EQL-EXEC
         ACL2::CONVERT-NORMALIZED-TERM-TO-PAIRS
         ACL2::PRINT-PROOF-TREE-CTX ACL2::SHORTEST-POLYS-WITH-VAR
         ACL2::PRETTYIFY-CLAUSE-SET ACL2::COMMUTATIVE-P1
         ACL2::POLYS-WITH-POTS ACL2::LOOP-STOPPERP
         ACL2::HL-HSPACE-NORM-AUX ACL2::DISABLEDP-FN
         ACL2::NEWLY-DEFINED-TOP-LEVEL-FNS ACL2::PROGRAM-ONLY-ER-MSG
         ACL2::CONSTRAINTS-INTRODUCED1 ACL2::HARD-ERROR
         ACL2::REDEFINED-WARNING ACL2::TAU-CONJUNCTIVE-FORMP
         ACL2::SHOW-ACCUMULATED-PERSISTENCE-PHRASE2 ACL2::SUBST-EXPR1
         ACL2::ADD-LINEAR-TERM ACL2::ACCEPTABLE-DOMAINS-FOR-BOUNDER
         ACL2::PRINT-FAILURE ACL2::UNIX-TRUENAME-PATHNAME
         ACL2::FIND-MAPPING-PAIRS-TAIL ACL2::CONTROLLER-UNIFY-SUBST1
         ACL2_*1*_COMMON-LISP::IF ACL2::MOST-RECENT-ENABLED-RECOG-TUPLE
         ACL2::MUTUALLY-EXCLUSIVE-SUBSUMPTIONP ACL2::ACTUAL-PROPS
         ACL2::MAKE-EVENT-DEBUG-POST ACL2::GETPROP-DEFAULT
         ACL2::ADD-TO-TYPE-ALIST-SEGMENTS ACL2::CONSTRAINTS-INTRODUCED
         ACL2::MERGE-ALIST1-INTO-ALIST2 ACL2::WITH-PROVER-STEP-LIMIT-FN
         ACL2::TS-BOOLEANP ACL2::COMPUTE-STOBJ-FLAGS
         ACL2::PATHNAME-OS-TO-UNIX ACL2::SYNP
         ACL2::TILDE-@-BKPTR-STRING ACL2::MODIFY-LINEAR-POT
         ACL2::PRINT-RATIONAL-AS-DECIMAL ACL2::MAKE-LAMBDA-APPLICATION
         ACL2::PUSH-TIMER ACL2::PUTPROP-DEFUN-RUNIC-MAPPING-PAIRS
         ACL2::MACRO-MINIMAL-ARITY ACL2::MEMBER-EQUAL-MOD-COMMUTING
         ACL2::BODY ACL2::LOGICAL-NAME-TYPE
         ACL2::INCLUDE-BOOK-ALIST-SUBSETP-FAILURE-WITNESSES
         ACL2::EQUAL-MOD-COMMUTING ACL2::CNF-DNF
         ACL2::SPONTANEOUS-DECERTIFICATIONP1 ACL2::OUR-UPDATE-HT
         ACL2::PRINT-DEFUN-MSG/SIGNATURES1 ACL2::STRING<-L
         ACL2::PRIMITIVE-RECURSIVE-MACHINEP ACL2::GENEQV-REFINEMENTP
         ACL2::MAKE-MV-NTHS ACL2::PCD2 ACL2::CONTROLLER-POCKET-SIMPLERP
         ACL2::MAKE-FREE-MAX-TERMS-MSG1 ACL2::SQUEEZE-K
         ACL2::PUSH-WORMHOLE-UNDO-FORMI ACL2::ADD-LINEAR-VARIABLE
         ACL2::ASSOC-EQ-EQUAL-BUTLAST-2 ACL2::XXXJOIN-FIXNUM
         ACL2::COLLECT-ASSUMPTIONS1 ACL2::ACCEPTABLE-TAU-RULESP
         ACL2::PUT-ASSOC-EQL-EXEC$GUARD-CHECK ACL2::MAKE-RECORD-MAKER
         ACL2::DISTRIBUTE-OTHER-HINTS-INTO-OR1 ACL2::PUT-ASSOC-EQ-EXEC
         ACL2::MEMOIZE-TABLE-CHK ACL2::PUT-ASSOC-EQUAL
         ACL2::TILDE-@-CASE-SPLIT-LIMITATIONS-PHRASE
         ACL2::REVERT-GOAL-TREE ACL2::LONGEST-COMMON-TAIL-LENGTH
         ACL2::SET-TAU-RUNES ACL2::SUBST-BY-POSITION
         ACL2::INTERSECTION-AUGMENTED-THEORIES-FN1
         ACL2::PAIRLIS$-TAILREC ACL2::HL-HSPACE-HONS-GET
         ACL2::M&M-APPLY ACL2::DUMB-TYPE-ALIST-IMPLICATIONP1
         ACL2::EXTEND-PEQUIV-LST ACL2::ALL-FNNAMES1
         ACL2::MAKE-VERIFY-TERMINATION-DEFS-LST
         ACL2::ACCUMULATE-RW-CACHE-INTO-PSPV
         ACL2::EXT-ANC-ATTACHMENTS-VALID-P-1 ACL2::PIGEON-HOLEP-APPLY
         ACL2::APPLY-SYMBOL-ALIST ACL2::TERM-STOBJS-OUT
         ACL2::FIND-TYPE-PRESCRIPTION-PAT ACL2::FORMAL-POSITION
         ACL2::INDUCTION-HYP-CLAUSE-SEGMENTS1 ACL2::EVERY-ALIST1-MATEDP
         ACL2::QUICK-BLOCK-INFO ACL2::INFECT-NEW-TYPE-ALIST-ENTRIES2
         ACL2::OR-HIT-MSG ACL2::SOME-CONGRUENCE-RULE-HAS-REFINEMENT
         ACL2::INFORM-SIMPLIFY
         ACL2::SHOW-ACCUMULATED-PERSISTENCE-PHRASE-KEY
         ACL2::NON-RECURSIVE-FNNAMES ACL2::EXPANSION-FILENAME
         ACL2::ASSIGN-EVENT-NAME-AND-RULE-CLASSES ACL2::ADD-TIMERS
         ACL2::CHECK-PROPOSED-IMPORTS ACL2::COLLECT-INSTANTIABLEP1
         ACL2::CLEANUP-IF-EXPR-LST ACL2::PUSH-IO-RECORD
         ACL2::INTRO-UDF-LST ACL2::LENGTH-OF-SHORTEST-POLYS-WITH-VAR
         ACL2::COLLECT-NAMES-IN-DEFUN-MODES
         ACL2_*1*_ACL2::CANONICAL-PATHNAME ACL2::UNENCUMBER-ASSUMPTIONS
         ACL2::VAR-ADDRESS ACL2::DECODE-RECOG-LST
         ACL2::BIG-D-LITTLE-D-EVENT ACL2::SAVE-FN
         ACL2::NON-BOUNDED-NUMS ACL2::<?-RATIONAL-V-NUMBER
         ACL2::PAIR-FNS-WITH-MEASURED-SUBSETS
         ACL2::SIMPLIFY-CLAUSE-FOR-TERM-EQUAL-CONST
         ACL2::UPDATE-PROOF-SUPPORTERS-ALIST-2
         ACL2::SER-DECODE-FROM-STREAM
         ACL2::META-EXTRACT-CONTEXTUAL-FACT
         ACL2::EXPAND-SOME-NON-REC-FNS ACL2::TERMINATION-MACHINE1
         ACL2::FILTER-HITPS ACL2::NON-STOBJPS ACL2::DECODE-TAU-INTERVAL
         ACL2::CANONICAL-PATHNAME ACL2::UNTRANSLATE
         ACL2::PAIRWISE-UNION-GENEQV ACL2::TAU-PAIRS-NEAR-SUBSETP
         ACL2::DECIMAL-STRING-TO-NUMBER
         ACL2::BIG-M-LITTLE-M-COMMAND-BLOCK ACL2::CONTROLLER-ALISTP
         ACL2::FILENAME-TO-SYSFILE-INCLUDE-BOOK-ALIST
         ACL2::HL-HSPACE-HONS-EQUAL-1 ACL2::TILDE-@-BKPTR-PHRASE
         ACL2::TYPE-SET-IMPLIED-BY-TERM1
         ACL2::MARK-ATTACHMENT-DISALLOWED2 ACL2::BOUNDS-POLY-WITH-VAR
         ACL2::ABBREVIATIONP ACL2::SET-TIMER ACL2::UNION-GENEQV1
         ACL2::FNS-USED-IN-AXIOMS ACL2::CANONICAL-UNIX-PATHNAME
         ACL2::MAYBE-ONE-WAY-UNIFY-WITH-SOME ACL2::DISCOVER-TAU-PREDS
         ACL2::ADD-TO-TAG-TREE ACL2::BOUNDED-INTEGER-LISTP
         ACL2::TAU-BOOLEAN-FORMP ACL2::SYMBOL-LIST-TO-PACKAGE-ALIST1
         ACL2::NOTE-FNS-IN-FILES ACL2::MAKE-LINEAR-INSTR
         ACL2::COLLECT-HEREDITARILY-CONSTRAINED-FNNAMES
         ACL2::CHK-VIRGIN2 ACL2::HL-FALTABLE-LOAD-EMPTY-SLOT
         ACL2::PRINT-DEFUN-MSG/SIGNATURES
         ACL2::INTRO-UDF-NON-CLASSICALP ACL2::OP-SEARCH-BUCKET
         ACL2::BOUNDED-INTEGER-ALISTP2 ACL2::PUT-EVENT-DATA
         ACL2::LOOP-STOPPERP-REC ACL2::MAKE-RUNES1
         ACL2::ADD-BINDING-TO-TAG-TREE ACL2::TERMINATION-MACHINES
         ACL2::FOCCURRENCES-LST ACL2::UPDATE-PCERT-BOOKS
         ACL2::TYPE-SET-BINARY-+-ALIST ACL2::MAP-TYPE-SETS-VIA-FORMALS
         ACL2::COLLECT-BY-POSITION ACL2::RUNIC-THEORYP1
         ACL2::COLLECT-IDEALS ACL2::SUBSUMES!-REC ACL2::COMPUTE-VETOES1
         ACL2::UNTRANSLATE-SUBST-ABB ACL2::LOOP-STOPPER1
         ACL2::TERM-ID-IFF ACL2::MULTIPLE-ASSOC-TERMINAL-SUBSTRINGP1
         ACL2::CONTROLLER-UNIFY-SUBST
         ACL2::CLASSIFY-AND-STORE-BUILT-IN-CLAUSE-RULES
         ACL2::EXT-ANCESTORS-ATTACHMENTS3 ACL2::SUBST-VAR-LST
         ACL2::MAKE-LEAF-CST ACL2::FREE-VARS-IN-HYPS
         ACL2::DECORATE-FORCED-GOALS-1 ACL2::COLLECT-BOUNDER-ARGS
         ACL2::NOT-TO-BE-REWRITTENP ACL2::PRINT-HINT-EVENTS-SUMMARY
         ACL2::FOCCURRENCES ACL2::TERM-DIFFICULTY1-LST
         ACL2::GEN-NEW-NAME1 ACL2::MAKE-RECORD-CHANGER-CONS
         ACL2::LATCH-STOBJS1 ACL2::RENEW-NAME/ERASE
         ACL2::INDUCTION-FORMULA-SIZE1 ACL2::POOL-DIFFICULTY
         ACL2::ALL-INTEGERS-IN-RANGE-EXCLUDEDP1
         ACL2::TRUSTED-CLAUSE-PROCESSOR-TABLE-GUARD
         ACL2::EVALUATOR-CLAUSE/ARGLIST
         ACL2::PARTITION-REST-AND-KEYWORD-ARGS2 ACL2::TRUNCATED-CLASS
         ACL2::ADD-TRIP ACL2::SUBST-EXPR1-LST ACL2::FSUBCOR-VAR
         ACL2::BOUNDING-INTERVAL ACL2::QUICK-BLOCK-SETTINGS
         ACL2::REVAPPEND-DELETE-RUNES-BASED-ON-SYMBOLS
         ACL2::GENERALIZABLE-TERMS ACL2::PRINT-REDEFINITION-WARNING
         ACL2::IF-INTERP-ASSUMED-VALUE2-EQUAL-CONSTANT
         ACL2::HAS-PROPSP1 ACL2::MERGE-LST1-INTO-LST2 ACL2::MAKE-ORD
         ACL2::THEORYP1 ACL2::CANONICAL-CDRS
         ACL2::EXPAND-SOME-NON-REC-FNS-LST ACL2::STORE-CLAUSE1
         ACL2::REVAPPEND-DELETE-AUGMENTED-RUNES-BASED-ON-SYMBOLS1
         ACL2::BIG-M-LITTLE-M-CLIQUE1 ACL2::PRINT-TIMER
         ACL2::GET-GUARDS1 ACL2::UNDO-TRIP
         ACL2::CONVERT-ASSUMPTIONS-TO-CLAUSE-SEGMENT
         ACL2::DEFINITION-RUNES ACL2::SPLICE-KEYWORD-ALIST
         ACL2::ALISTS-AGREEP ACL2::INFECT-POLYS
         ACL2::IF-INTERP-ASSUME-TRUE ACL2::HL-HSPACE-FAST-ALIST-CLEAN
         ACL2::CHK-VIRGIN ACL2::CONSTRAINED-FUNCTIONS
         ACL2::FETCH-DCL-FIELDS2 ACL2::REPRETTYIFY ACL2::SER-DECODE-STR
         ACL2::SUBSUMES-REWRITE-RULE
         ACL2::PRINT-SET-WATERFALL-PARALLELISM-NOTICE
         ACL2::FIND-NAMED-LEMMA ACL2::CONS-ASSOC-EQ
         ACL2::SHOW-ACCUMULATED-PERSISTENCE-PHRASE2-MERGE
         ACL2::CHK-MUTUAL-RECURSION-BAD-NAMES
         ACL2::HL-HSPACE-HONS-EQUAL ACL2::PC-COMMAND-TABLE-GUARD
         ACL2::NEW-BACKCHAIN-LIMIT ACL2::ASSOC-EQ-EQUAL
         ACL2::AUGMENT-IGNORE-VARS ACL2::COLLECT-IDEAL-USER-DEFUNS1
         ACL2::ASSOC-EQ-EQ ACL2::REFINEMENTP1
         ACL2::ADD-LINEAR-VARIABLE1 ACL2::CLAUSE-SET-SUBSUMES
         ACL2::DEFSTOBJ-CREATOR-FN ACL2::TAU-EVAL-FORMP ACL2::SUBST-VAR
         ACL2::FIND-LONGEST-COMMON-RETRACTION ACL2::PONS
         ACL2::PRIMITIVE-RECURSIVE-CALLSP ACL2::HONS-ACONS
         ACL2::COLLECT-CONGRUENCE-RULES-OF-RUNE)) 
(COMMON-LISP::PROCLAIM
    '(COMMON-LISP::FTYPE
         (COMMON-LISP::FUNCTION
             (COMMON-LISP::T COMMON-LISP::T COMMON-LISP::T
                 COMMON-LISP::T COMMON-LISP::T COMMON-LISP::T)
             COMMON-LISP::T)
         ACL2::REDUNDANT-OR-RECLASSIFYING-DEFUNSP0 ACL2::MFC-RW-FN
         ACL2::EVISCERATE-SIMPLE ACL2::STATE-FROM-INSTRUCTIONS
         ACL2::ADD-EVENT-LANDMARK ACL2::INFO-FOR-X-RULES
         ACL2::WARNING1-CW ACL2::MAYBE-WARN-ABOUT-THEORY-FROM-RCNSTS
         ACL2::REPLACE-FREE-RW-CACHE-ENTRY ACL2::MAKE-EVENT-LDD
         ACL2::PARSE-MATCH ACL2::MV-LET-FOR-WITH-LOCAL-STOBJ
         ACL2::NOTE-RELIEVE-HYP-FAILURE ACL2::INTERVAL-DECIDER
         ACL2_*1*_ACL2::MFC-RW-FN ACL2::DEFEVALUATOR-FORM/DEFTHM
         ACL2::ADD-FORWARD-CHAINING-RULE ACL2::GUARD-ER-MESSAGE-CODA
         ACL2::SHOW-TYPE-PRESCRIPTION-RULES
         ACL2::DEFEVALUATOR-FORM/DEFTHM-NAME
         ACL2::REDUNDANT-ENCAPSULATE-TUPLEP ACL2::PROMOTE-GUTS
         ACL2::MAKE-LDD ACL2::ADD-TYPE-SET-INVERTER-RULE
         ACL2::PRINT-CERTIFY-BOOK-GUARDS-WARNING ACL2::TAU-SUBRS
         ACL2::REDUNDANT-OR-RECLASSIFYING-DEFUNSP1 ACL2::TRANSLATABLE-P
         ACL2::WATERFALL-OR-HIT-MSG-C ACL2::FLSZ
         ACL2::MEASURE-CLAUSE-FOR-BRANCH
         ACL2::MAKE-GOALS-FROM-ASSUMPTIONS ACL2::CROSS-FERTILIZEP
         ACL2::TRACE$-DEF ACL2::DEFEVALUATOR-FORM/DEFTHMS
         ACL2::ADD-X-RULE ACL2::TAU-INTERVAL-ENDPOINT-IMPLICATION
         ACL2::WATERFALL-OR-HIT-MSG-A ACL2::SGETPROP1 ACL2::IF-INTERP
         ACL2::SHOW-META-LEMMAS1 ACL2::NON-ACCEPTABLE-DEFUN-SK-P
         ACL2::INITIALIZE-PROOF-TREE1
         ACL2::SOUND-INDUCTION-PRINCIPLE-MASK1 ACL2::FMT-ABBREV
         ACL2::EVERY-OCCURRENCE-EQUIV-HITTABLEP
         ACL2::UNTRANSLATE-INTO-CASE-CLAUSES
         ACL2::ADD-ACCUMULATED-PERSISTENCE-F ACL2::GENEQV-AT-SUBTERM
         ACL2::ADD-ACCUMULATED-PERSISTENCE-S ACL2::TABLE-CLTL-CMD
         ACL2::SUBST-TYPE-ALIST1
         ACL2::SHOW-DOUBLE-REWRITE-OPPORTUNITIES
         ACL2::RELEVANT-POSNS-TERM-LST ACL2::FORMAT-PROOF-TREE
         ACL2::PUSH-CLAUSE-MSG1 ACL2::NOTE-RW-CACHE-FREE-NIL-TAG
         ACL2::STRING-MATCHP ACL2::ERROR-FMS-CHANNEL
         ACL2::REDUNDANT-OR-RECLASSIFYING-DEFUNP0
         ACL2::REWRITE-FNCALLP-LISTP ACL2::FERTILIZE-FEASIBLE
         ACL2::PPR2-COLUMN ACL2::SOME-OCCURRENCE-EQUIV-HITTABLEP1
         ACL2::REWRITE-FNCALLP ACL2::MAKE-LDDS-COMMAND-SEQUENCE
         ACL2::SOME-OCCURRENCE-EQUIV-HITTABLEP ACL2::COMPRESS21
         ACL2::GET-INDUCTION-CANDS-FROM-CL-SET1
         ACL2::PRINT-GAG-STACK-REV ACL2::COMPRESS211
         ACL2::SOME-OCCURRENCE-EQUIV-HITTABLEP1-LISTP
         ACL2::RELEVANT-POSNS-TERM ACL2::MEASURE-CLAUSES-FOR-FN1
         ACL2::EXTRACT-AND-CLASSIFY-LEMMAS1
         ACL2::MAKE-FC-ACTIVITY-REPORT1 ACL2::ADD-TAU-SIGNATURE-RULE)) 
(COMMON-LISP::PROCLAIM
    '(COMMON-LISP::FTYPE
         (COMMON-LISP::FUNCTION
             (COMMON-LISP::T COMMON-LISP::T COMMON-LISP::T
                 COMMON-LISP::T COMMON-LISP::T COMMON-LISP::T
                 COMMON-LISP::T COMMON-LISP::T COMMON-LISP::T)
             COMMON-LISP::T)
         ACL2::HONS-RESIZE-FN ACL2::ASSUME-TRUE-FALSE-<
         ACL2::MEMOIZE-FN-OUTER-BODY ACL2::WATERFALL-MSG1
         ACL2::TAU-GET-STATS-ON-SIGNATURES ACL2::ADD-LINEAR-RULE
         ACL2::BRKPT1 ACL2::ADD-LINEAR-RULE1 ACL2::ADD-LINEAR-RULE3
         ACL2::RUNES-TO-MONITOR-WARNINGS
         ACL2::INTRINSIC-SUGGESTED-INDUCTION-CAND
         ACL2::ADD-REWRITE-RULE2 ACL2::ADD-ELIM-RULE1)) 
(COMMON-LISP::PROCLAIM
    '(COMMON-LISP::FTYPE
         (COMMON-LISP::FUNCTION
             (COMMON-LISP::T COMMON-LISP::FIXNUM COMMON-LISP::T
                 COMMON-LISP::FIXNUM COMMON-LISP::FIXNUM COMMON-LISP::T
                 COMMON-LISP::T)
             COMMON-LISP::FIXNUM)
         ACL2::FLSZ1)) 
(COMMON-LISP::PROCLAIM
    '(COMMON-LISP::FTYPE
         (COMMON-LISP::FUNCTION
             (COMMON-LISP::T COMMON-LISP::T COMMON-LISP::T
                 COMMON-LISP::T COMMON-LISP::T)
             COMMON-LISP::T)
         ACL2::PRINT-TTAG-NOTE ACL2::SGETPROP ACL2::PPR?
         ACL2::UPDATE-ENABLED-STRUCTURE-ARRAY ACL2::FMS
         ACL2::BAD-VAL-OR-UNKNOWNS ACL2::SUSPEND-FC-ACTIVATION
         ACL2::TILDE-@-FAILURE-REASON-FREE-PHRASE
         ACL2::META-EXTRACT-RW+-TERM ACL2::ADD-RULES1
         ACL2::CANONICAL-FFN-SYMBS-LST
         ACL2::ALL-INTEGERS-IN-RANGE-EXCLUDEDP ACL2::CHANGEABLES
         ACL2::ALL-EVAL-VALP ACL2::ERROR-FMS
         ACL2::EXT-ANCESTORS-ATTACHMENTS1 ACL2::SUBSUMES!1 ACL2::PPR2
         ACL2::GET-INDUCTION-CANDS-LST ACL2::PUTPROP-CONSTRAINTS
         ACL2::INITIAL-STATE-STACK
         ACL2::CONJOIN-CLAUSE-TO-CLAUSE-SET-EXTRA-INFO1
         ACL2::APPLY-CONJUNCTIVE-TAU-RULES1 ACL2::MAXIMAL-ELEMENTS1
         ACL2::ADD-RECOGS-TO-TAU1 ACL2::PUTPROP-INDUCTION-MACHINE-LST
         ACL2::ACCUMULATE-SHALLOW-PEQUIV-ALIST
         ACL2::ADD-TAU-SIMPLE-RULE ACL2::SEARCH-FROM-END
         ACL2::EXTEND-TYPE-ALIST ACL2::DEFEVALUATOR-CHECK-MSG
         ACL2::MAKE-FC-ACTIVATIONS ACL2::ADD-TAU-CONJUNCTIVE-RULE
         ACL2::BASE-POLY0 ACL2::SETTLED-DOWN-CLAUSE-MSG1
         ACL2::DEFSTOBJ-FIELD-FNS-AXIOMATIC-DEFS
         ACL2::HL-FAST-ALIST-FORK-AUX-SLOW ACL2::MEMOIZE-FN-INIT-2
         ACL2::PC-PRIMITIVE-DEFUN-FORM
         ACL2::FIND-FIRST-NON-LOCAL-NAME-LST
         ACL2::RW-CACHE-DEBUG-ACTION-BUILTIN
         ACL2::HL-FAST-ALIST-CLEAN-AUX ACL2::FORMAT-FORCED-SUBGOALS
         ACL2::M&M1 ACL2::PRINT-DEFUN-MSG ACL2::LOAD-COMPILED-BOOK
         ACL2::RECOVER-WORLD ACL2::GENERATE-VARIABLE-LST
         ACL2::PRINT-SPLITTER-RULES-SUMMARY ACL2::UNTRANSLATE1-LST
         ACL2::FIND-RULES-OF-RUNE2 ACL2::UNTRANSLATE-INTO-COND-CLAUSES
         ACL2::EXT-ANCESTORS-ATTACHMENTS2
         ACL2::ALLEGRO-ALLOCATE-SLOWLY-FN ACL2::LET*-MACRO
         ACL2::EXISTS-BAD-VALP ACL2::CROSS-FERTILIZEP/D
         ACL2::HAS-PROPSP ACL2::ADD-TAU-BOUNDER-RULE ACL2::ADD-TO-TAU1
         ACL2::ACL2-QUERY-SIMULATE-INTERACTION
         ACL2::GENERALIZABLE-TERMS-ACROSS-LITERALS1
         ACL2::MEMOIZE-TABLE-CHK-COMMUTATIVE ACL2::ADD-TO-TAU
         ACL2::ELIMINATE-IRRELEVANCE-CLAUSE-MSG1
         ACL2::COMBINE-POS/NEG-PAIRS-FROM-TAU ACL2::WARNING1
         ACL2::RELEVANT-POSNS-CLIQUE1 ACL2::FMS!
         ACL2::RETURN-TYPE-ALIST ACL2::FMS-TO-STRING-FN
         ACL2::SMALLEST-COMMON-SUBTERMS ACL2::CONS-PPR1 ACL2::OP-ALIST
         ACL2::REDUNDANT-DEFMACROP ACL2::INSTALL-DEFS-FOR-ADD-TRIP
         ACL2::PUTPROP-X-LST2-UNLESS ACL2::MAKE-TAU-INTERVAL
         ACL2::MAKE-COMMAND-TUPLE ACL2::SELECT-INSTANTIATED-ELIM-RULE
         ACL2::EVERY-OCCURRENCE-EQUIV-HITTABLEP-IN-CLAUSEP
         ACL2::UNION-THEORIES-FN1 ACL2::MAYBE-ADD-SPLITTERS-TO-TTREE
         ACL2::REDUCE-SIGN/RECOG ACL2::REDUNDANT-THEOREMP
         ACL2::CHK-DEFABSSTOBJ-GUARDS1 ACL2::PE-FN1
         ACL2::REDUNDANT-OR-RECLASSIFYING-DEFUNP
         ACL2::CANONICAL-FFN-SYMBS ACL2::MAYBE-WARN-FOR-USE-HINT
         ACL2::COLLECT-RULES-WITH-DEPENDENT-HYPS
         ACL2::TILDE-@-FAILURE-REASON-PHRASE
         ACL2::PC-META-OR-MACRO-DEFUN ACL2::MISSING-COMPILED-BOOK
         ACL2::TILDE-@-FAILURE-REASON-PHRASE1
         ACL2::RW-CACHE-DEBUG-BUILTIN ACL2::ADD-ACCUMULATED-PERSISTENCE
         ACL2::PREPROCESS-CLAUSE-MSG1 ACL2::NEW-DEFPKG-LIST1
         ACL2::FORMALS-PRETTY-FLAGS-MISMATCH-MSG ACL2::COMPRESS11
         ACL2::ADD-EQUIVALENCE-RULE ACL2::SET-DIFFERENCE-THEORIES-FN1
         ACL2::HL-FAST-ALIST-FORK-AUX-FAST ACL2::GENERATE-VARIABLE
         ACL2::TILDE-*-ELIM-PHRASE2 ACL2::FIND-EQUIVALENCE-HYP-TERM
         ACL2::GENERALIZE-CLAUSE-MSG1 ACL2::MAKE-LDDS-COMMAND-BLOCK
         ACL2::FIND-STOBJ-OUT-AND-CALL ACL2::FERTILIZE-CLAUSE-MSG1
         ACL2::TERMINATION-MACHINE ACL2::WARNING1-BODY
         ACL2::PARSE-CLAUSE-ID2
         ACL2::COLLECT-RULES-WITH-DEPENDENT-HYPS-ACROSS-MV
         ACL2::DEFUN-INLINE-FORM ACL2::APPLICABLE-LINEAR-RULES1
         ACL2::FILTER-SATISFYING-VIRTUAL-FC-ACTIVATION
         ACL2::PUTPROP-UNLESS ACL2::COLLECT-FC-STATUS-SITES-2-3-5
         ACL2::IRRELEVANT-NON-LAMBDA-SLOTS-CLIQUE2
         ACL2::GET-INDUCTION-CANDS
         ACL2::ELIMINATE-DESTRUCTORS-CLAUSE-MSG1
         ACL2::TILDE-*-GEN-PHRASE
         ACL2::COROLLARIES-AND-RUNES-OF-ENABLED-RULES
         ACL2::UNCHANGEABLES ACL2::ADD-TO-POP-HISTORY
         ACL2::MAYBE-WARN-ABOUT-THEORY-SIMPLE ACL2::FMS!-TO-STRING-FN
         ACL2::PUTPROP-DEFUN-RUNIC-MAPPING-PAIRS1
         ACL2::TERMINATION-MACHINE-FOR-LIST
         ACL2::PRINT-CERTIFY-BOOK-STEP-2 ACL2::ADD-COMMAND-LANDMARK
         ACL2::DEFSTOBJ-FIELD-FNS-RAW-DEFS
         ACL2::INTERPRET-TERM-AS-REWRITE-RULE2
         ACL2::EARLIER-ANCESTOR-BIGGERP ACL2::FLPR
         ACL2::MAKE-COMMAND-LDD ACL2::CALL-STACK ACL2::UNTRANSLATE-IF
         ACL2::SUBST-TYPE-ALIST ACL2::MAKE-PEQUIV ACL2::INVERSE-POLYS
         ACL2::MATCH-FREE-FC-VALUE ACL2::UNTRANSLATE1
         ACL2::PROCESS-ASSUMPTIONS-MSG ACL2::OBSERVATION1
         ACL2::ADD-COMPOUND-RECOGNIZER-RULE
         ACL2::WARNED-NON-REC-FNS-TP-HYPS1
         ACL2::RELIEVE-HYP-FAILURE-ENTRY ACL2::GET-GUARDS2
         ACL2::MAKE-RECORD-CHANGER-LET
         ACL2::RELIEVE-HYP-FAILURE-ENTRY-SKIP-P-BUILTIN
         ACL2::CROSS-FERTILIZEP/C)) 
(COMMON-LISP::PROCLAIM
    '(COMMON-LISP::FTYPE
         (COMMON-LISP::FUNCTION
             (COMMON-LISP::T COMMON-LISP::T COMMON-LISP::T
                 COMMON-LISP::T)
             COMMON-LISP::T)
         ACL2::ADD-ONLY-SIMPLE-AND-CONJUNCTIVE-TAU-RULES
         ACL2::PUT-INVARIANT-RISK ACL2::SUBST-BY-POSITION1
         ACL2::INFO-FOR-GENERALIZE-RULES
         ACL2::EXISTS-FCD-WORSE-THAN-OR-EQUAL
         ACL2::DECORATE-FORCED-GOALS ACL2::EVISCERATE1P-LST
         ACL2::ACCUMULATE-RW-CACHE1
         ACL2::GENERALIZABLE-TERMS-ACROSS-LITERALS ACL2::THEORYP!1
         ACL2::DECODE-TAU-SIGNATURE-RULES1
         ACL2::CONTAINS-REWRITEABLE-CALLP ACL2::GENEQV-LST
         ACL2::GEN-NEW-NAME-IN-PACKAGE-OF-SYMBOL1
         ACL2::CHK-USER-STOBJ-ALIST ACL2::MAKE-FREE-MAX-TERMS-MSG
         ACL2::SERIALIZE-WRITE-FN ACL2::ADD-TAU-BIG-SWITCH-RULE
         ACL2::BUILT-IN-CLAUSEP2 ACL2::SELECTED-ALL-FNNAMES-LST
         ACL2::DECODE-TAU-SIGNATURE-RULE ACL2::ADD-CONGRUENCE-RULE
         ACL2::REPLACE-FREE-RW-CACHE-ENTRY1
         ACL2::BOGUS-EXPORTED-COMPLIANTS
         ACL2::EXPAND-TILDE-TO-USER-HOME-DIR ACL2::CLAUSIFY
         ACL2::OP-SEARCH-BUCKET-IF ACL2::PRINT-OBJECT$-SER
         ACL2::TILDE-*-ELIM-PHRASE1 ACL2::SINGLETON-TAU-INTERVALP
         ACL2::GENERALIZABLE-TERMS-ACROSS-RELATIONS
         ACL2::INSERT-INTO-GOAL-TREE-LST
         ACL2::MAYBE-PRINT-PROVED-GOAL-MESSAGE
         ACL2::BAD-SIGNATURE-ALIST ACL2::COVERED-GENEQV-ALIST
         ACL2::HL-HSPACE-FAST-ALIST-FORK ACL2::FMT-TO-COMMENT-WINDOW
         ACL2::BASE-POLY ACL2::GENVAR ACL2::UNTRANS0-LST-FN
         ACL2::DEFCHOOSE-CONSTRAINT-EXTRA
         ACL2::STORE-ABSOLUTE-EVENT-NUMBER ACL2::TERMINAL-SUBSTRINGP
         ACL2::OCCURS-NOWHERE-ELSE ACL2::ADD-BUILT-IN-CLAUSE-RULE
         ACL2::TILDE-*-ANCESTORS-STACK-MSG1 ACL2::FGETPROP
         ACL2::UNION-THEORIES-FN ACL2::SER-DECODE-AND-LOAD-ATOMS
         ACL2::TESTS-AND-ALISTS
         ACL2::INFO-FOR-COMPOUND-RECOGNIZER-RULES
         ACL2::INFO-FOR-FORWARD-CHAINING-RULES ACL2::SUBVERSIVE-CLIQUEP
         ACL2::EVERY-NEG-EVG-IN-TAU-P ACL2::QUICK-BLOCK-DOWN-T-MACHINE
         ACL2::ADD-TO-CR-AND-COARSENINGS ACL2::INFO-FOR-RULES
         ACL2::INFO-FOR-INDUCTION-RULES ACL2::SUBSUMES
         ACL2::ADD-TAU-EVAL-RULE ACL2::TAU-IMPLIES ACL2::SHOW-BDD-TERM
         ACL2::RULE-BACKCHAIN-LIMIT-LST
         ACL2::CONVERT-TAU-LIKE-TERMS-TO-TAU ACL2::ERROR-FMS-CW
         ACL2::BOOL-MASK ACL2::TERM-STOBJS-OUT-ALIST
         ACL2::FIND-SUBSUMED-RULE-NAMES ACL2::WATERFALL-OR-HIT-MSG-B
         ACL2::MAKE-BUILT-IN-CLAUSE-RULES1
         ACL2::PICK-HIGHEST-SUM-LEVEL-NOS
         ACL2::INFO-FOR-ELIMINATE-DESTRUCTORS-RULE
         ACL2::WATERFALL-PRINT-CLAUSE
         ACL2::CONVERT-THEORY-TO-UNORDERED-MAPPING-PAIRS1
         ACL2::COUNT-FN ACL2::TESTS-AND-ALISTS/ALIST
         ACL2::IF-COMPILE-LST ACL2::UNTRANSLATE-CONS
         ACL2::IDENTICAL-DEFP ACL2::MFC-AP-RAW
         ACL2::ADD-TAU-BOOLEAN-RULE ACL2::UPPER-BOUND->=
         ACL2::INSERT-INTO-GOAL-TREE-REC
         ACL2::INFO-FOR-TYPE-SET-INVERTER-RULES
         ACL2::PUSH-CLAUSE-MSG1-ABORT
         ACL2::ADD-WELL-FOUNDED-RELATION-RULE
         ACL2::COLLECT-CANONICAL-SIBLINGS ACL2::STRING-EQUAL1
         ACL2::NON-IDENTICAL-DEFP ACL2::LD-PRINT-COMMAND
         ACL2::SET-DIFFERENCE-AUGMENTED-THEORIES-FN1+
         ACL2::ANNOTATE-CLAUSE-WITH-KEY-NUMBERS ACL2::ACTUAL-STOBJS-OUT
         ACL2::MAKE-RECORD-RECOGNIZER ACL2::COVERED-GENEQV-ALIST-LST
         ACL2::SUBSTITUTE1-AC ACL2::CHK-STOBJ-LET/UPDATERS
         ACL2::GET-GUARDS ACL2::TILDE-*-SUBSTITUTION-PHRASE
         ACL2::SORT-XRUNE-ALIST-BY-RUNE1 ACL2::UPDATE-NTH-ARRAY
         ACL2::SURROUNDING-FNS1 ACL2::IF-INTERP-ASSUMED-VALUE2
         ACL2::PRETTY-PARSE-AD-LIST ACL2::LEGAL-LET*-P
         ACL2::NEW-DEFPKG-LIST2 ACL2::AUGMENT-RUNIC-THEORY1
         ACL2::APPLY-REORDER-HINT-FRONT ACL2::DESTRUCTIVE-PUSH-ASSOC
         ACL2::SOME-OCCUR-AFFINITY ACL2::DEFSTOBJ-FNNAME
         ACL2::INFECT-NEW-TYPE-ALIST-ENTRIES1 ACL2::CLTL-DEF-FROM-NAME2
         ACL2::ADD-GENERALIZE-RULE
         ACL2::COPY-OBJECT-CHANNEL-UNTIL-MARKER ACL2::NOTIFY-ON-DEFTTAG
         ACL2::PRINT-INFO-FOR-RULES-ENTRY ACL2::INFO-FOR-LEMMAS
         ACL2::BAD-SYNP-HYP-MSG ACL2::CW-GSTACK1
         ACL2::BIG-D-LITTLE-D-COMMAND-BLOCK
         ACL2::INFO-FOR-BUILT-IN-CLAUSE-RULES1 ACL2::SUBVERSIVEP
         ACL2::TERMINAL-SUBSTRINGP1 ACL2::SUBSTITUTE-AC
         ACL2::OK-TO-FIRE-SIGNATURE-RULEP1 ACL2::FMS-TO-STANDARD-CO
         ACL2::UPPER-BOUND-< ACL2::THROW-NONEXEC-ERROR-P1
         ACL2::ADD-CLAUSE-PROCESSOR-RULE ACL2::FUNCTION-THEORY-FN1
         ACL2::VAR-ADDRESS-LST ACL2::P-BODY
         ACL2::CHK-STOBJ-LET/BINDINGS ACL2::UNENCUMBER-TYPE-ALIST
         ACL2::SET-LOOP-STOPPER-VALUES ACL2::CROSS-TESTS-AND-CALLS
         ACL2::SET-TAU-POS-EVG ACL2::PUTPROP-IF-DIFFERENT
         ACL2::BAD-SYNP-ALIST1-LST ACL2::BIG-D-LITTLE-D-CLIQUE1
         ACL2_*1*_ACL2::MFC-TS-FN ACL2::THE-CHECK-FOR-*1*
         ACL2::WARN-ON-DUPLICATE-HINT-GOAL-SPECS
         ACL2::MAKE-RECORD-MAKER-LET ACL2::ADD-ASSUMPTIONS-TO-TOP-GOAL
         ACL2::ADD-SPLITTERS-TO-TTREE
         ACL2::REPLACE-STRING-PREFIX-IN-TREE
         ACL2::CORRESPONDING-ARGS-EQ-EXCEPT ACL2::ADD-ELIM-RULE
         ACL2::INFO-FOR-CONGRUENCES
         ACL2::DEFSTOBJ-COMPONENT-RECOGNIZER-CALLS ACL2::COMBINE-TAU
         ACL2::DEPOSIT-TERM-LST ACL2::CLTL-DEF-FROM-NAME1
         ACL2::RW-CACHE-ADD-FAILURE-REASON ACL2::BAD-SYNP-ALIST1
         ACL2::TESTS-AND-ALISTS/ALISTS ACL2::SET-DIFFERENCE-THEORIES-FN
         ACL2::ABBREVIATE-HYPHENATED-STRING1 ACL2::INDUCT-MSG/LOSE
         ACL2::UNKNOWN-BINDING-MSG ACL2::WARNED-NON-REC-FNS-FOR-TP
         ACL2::INDUCTION-FORMULA3 ACL2::REPLACE-INITIAL-SUBSTRING
         ACL2::INSTANTIABLE-FFN-SYMBS ACL2::DEFEVALUATOR-CHECK-FORM
         ACL2::DEFEVALUATOR-FORM
         ACL2::SYSFILE-TO-FILENAME-INCLUDE-BOOK-ALIST1
         ACL2::PRINT-SUMMARY ACL2::MISSING-KNOWN-STOBJS
         ACL2::INDUCTION-FORMULA1 ACL2::EXTEND-GENEQV-ALIST
         ACL2::GENEQV-LST1 ACL2::DECODE-TAU-SIGNATURE-RULES2
         ACL2::SOME-HYP-PROBABLY-NILP ACL2::ASSOC-EQUIV
         ACL2::NEWLY-DEFINED-TOP-LEVEL-FNS-REC
         ACL2::UNION-AUGMENTED-THEORIES-FN1+ ACL2::PRINT-FLAT-INFIX
         ACL2::MATCH-FREE-VALUE ACL2::TAU-GET-STATS-ON-IMPLICANT-SIZES
         ACL2::ONEIFY ACL2::RECOGNIZER-RUNE ACL2::META-FN-ARGS
         ACL2::HL-HSPACE-HONS-ACONS
         ACL2::AUGMENT-POS/NEG-PAIRS-WITH-IMPLICIT-NUMERIC-RECOGS
         ACL2::SEARCH-FROM-START ACL2::TTAG-ALLOWED-P ACL2::AFFINITY
         ACL2::SAVE-EV-FNCALL-GUARD-ER ACL2::CONSTRAINTS-LIST
         ACL2::ALL-CALLS-LST ACL2::FLPR1 ACL2::ADD-LITERAL-AND-PT1
         ACL2::PUSH-RW-CACHE-ENTRY ACL2::DEFPKG-RAW1
         ACL2::REPLACE-CLAUSE1 ACL2::ALL-FNNAMES-WORLD1
         ACL2::IF-COMPILE ACL2::EXTEND-RW-CACHE-ALIST-FREE
         ACL2::INITIALIZE-PROOF-TREE
         ACL2::DECORATE-FORCED-GOALS-IN-PROOF-TREE
         ACL2::MAKE-RECORD-ACCESSORS
         ACL2::ABSSTOBJ-CORRESPONDENCE-CONCL-LST ACL2::ONEIFY-LST
         ACL2::CONTAINS-REWRITEABLE-CALLP-LST
         ACL2::MEMBER-COMPLEMENT-TERM2 ACL2::TESTS-AND-ALISTS-LST
         ACL2::BIND-FREE-INFO ACL2::EXT-ANC-ATTACHMENTS-VALID-P
         ACL2::LOWER-BOUND-<= ACL2::PRINT-HYPS
         ACL2::DUPLICITOUS-MERGE-CAR ACL2::INFECT-FIRST-N-POLYS
         ACL2::SHOW-FALSIFYING-ASSIGNMENT ACL2::RECORD-MACROS
         ACL2_*1*_ACL2::MFC-AP-FN ACL2::NORMALIZE-STRING1
         ACL2::EXTERNAL-LINEARIZE
         ACL2::EXTEND-PROOF-TREE-FOR-FORCING-ROUND
         ACL2::CANONICAL-ANCESTORS-REC
         ACL2::WARN-ON-INAPPROPRIATE-DEFUN-MODE ACL2::MAYBE-PUTPROP-LST
         ACL2::SHOW-META-LEMMAS ACL2::INFO-FOR-PEQUIVS
         ACL2::TILDE-*-SUBSTITUTION-PHRASE1 ACL2::PUT-BRR-LOCAL1
         ACL2::COUNT-STRINGP ACL2::ONCEP ACL2::MAKE-FC-ACTIVATION
         ACL2::SOUND-INDUCTION-PRINCIPLE-MASK ACL2::LOWER-BOUND->
         ACL2::PROCESS-ASSUMPTIONS-MSG1
         ACL2::IMMEDIATE-CANONICAL-ANCESTORS ACL2::MAKE-VAR-LST1
         ACL2::SURROUNDING-FNS-LST ACL2::ALL-OCCUR-AFFINITY
         ACL2::FMT-TO-COMMENT-WINDOW! ACL2::GENEQV-AT-SUBTERM-TOP
         ACL2::DEFSTOBJ-COMPONENT-RECOGNIZER-AXIOMATIC-DEFS
         ACL2::SHOW-BDD-BACKTRACE ACL2::PRINT-BOOK-PATH
         ACL2::PRINT-ENCAPSULATE-MSG3/CONSTRAINTS
         ACL2::FCD-WORSE-THAN-OR-EQUAL-LST ACL2::EVISCERATE1P
         ACL2::CW-GFRAME ACL2::GENVAR1 ACL2::COMM-EQUAL
         ACL2::MAKE-LDD-FLAGS ACL2::DEFINE-PC-META-OR-MACRO-FN
         ACL2::NON-FREE-VAR-RUNES ACL2::PUT-ASSOC-EQUAL-TS
         ACL2::PARSE-CLAUSE-ID1 ACL2::INSTANTIABLE-FFN-SYMBS-LST
         ACL2::LOOKUP-WORLD-INDEX1 ACL2::DECODE-TAU-SIGNATURE-RULES
         ACL2::DECODED-TYPE-SET-FROM-TP-RULE ACL2::VETOEDP
         ACL2::INFO-FOR-LINEAR-LEMMAS ACL2::MFC-TS-FN
         ACL2::PUTPROP-X-LST1 ACL2::LINKED-VARIABLES1
         ACL2::OBSERVATION1-CW ACL2::PUTPROP
         ACL2::CHANGED/UNCHANGED-VARS ACL2::CLAUSE-SET-SUBSUMES-1
         ACL2::PPR2-FLAT ACL2::FIND-FIRST-NON-LOCAL-NAME
         ACL2::SHOW-BDD-GOAL ACL2::MEMBER-AFFINITY ACL2::TAU-UNION
         ACL2::FLPR11 ACL2::HL-HSPACE-HONS-ACONS!
         ACL2::INFO-FOR-BUILT-IN-CLAUSE-RULES
         ACL2::NON-IDENTICAL-DEFP-CHK-MEASURES
         ACL2::APPLY-REORDER-HINT-BACK
         ACL2::RELEVANT-POSNS-CLIQUE-RECUR
         ACL2::IRRELEVANT-NON-LAMBDA-SLOTS-CLIQUE1
         ACL2::GET-UNAMBIGUOUS-XARGS-FLG1/EDCLS1
         ACL2::ADD-STRING-VAL-PAIR-TO-STRING-VAL-ALIST
         ACL2::NEXT-PEQUIV ACL2::PIGEON-HOLEP ACL2::CD-SEARCH
         ACL2::BUILT-IN-CLAUSEP1 ACL2::INFO-FOR-TYPE-PRESCRIPTIONS
         ACL2::CHK-INITIAL-BUILT-IN-CLAUSES ACL2::FORMAT-PROCESSOR
         ACL2::EMPTY-TAU-INTERVALP ACL2::MEMBER-TERM2
         ACL2::DEFSTOBJ-RAW-DEFS ACL2::GLOBAL-SET? ACL2::MFC-AP-FN
         ACL2::INITIAL-RCNST-FROM-ENS ACL2::EXPAND-PERMISSION-P
         ACL2::PRINT-ON-SEPARATE-LINES ACL2::MAKE-BUILT-IN-CLAUSE-RULES
         ACL2::PRINT-NO-CHANGE-FN ACL2::PUTPROP-X-LST2 ACL2::WORMHOLE1
         ACL2::APPLICABLE-LINEAR-RULES ACL2::OP-SEARCH-BUCKET-2
         ACL2::EQUAL-MOD-ALIST2-LST ACL2::MARK-ATTACHMENT-DISALLOWED
         ACL2::COLLECT-X-RULES-OF-RUNE ACL2::SET-SITE-EVISC-TUPLE
         ACL2::ALL-PICKS1 ACL2::EV-FNCALL-W-GUARD ACL2::ALL-CALLS
         ACL2::SHOW-ACCUMULATED-PERSISTENCE-PHRASE1 ACL2::EVISC-TUPLE
         ACL2::TT-INIT ACL2::FIND-SUBSUMING-RULE-NAMES
         ACL2::NEW-DISABLES ACL2::ONEIFY-FLET-BINDINGS
         ACL2::INDUCTION-FORMULA2 ACL2::EQUAL-MOD-ALIST2
         ACL2::FN-RUNE-NUME ACL2::PRIN1-WITH-SLASHES
         ACL2::TAU-GET-STATS-NEW-MAX-BLOCK
         ACL2::GET-INDUCTION-CANDS-FROM-CL-SET
         ACL2::FILENAME-TO-SYSFILE-INCLUDE-BOOK-ALIST1 ACL2::NEW-TRIPS
         ACL2::MAKE-NEW-GOALS-FIXED-HYPS ACL2::INSERT-INTO-GOAL-TREE
         ACL2::INFO-FOR-COARSENINGS ACL2::EXTEND-TYPE-ALIST-SIMPLE
         ACL2::EV-FNCALL-W-TAU-RECOG ACL2::SOME-MEMBER-SUBSUMES
         ACL2::REDUNDANT-ENCAPSULATEP
         ACL2::HL-FAST-ALIST-FORK-AUX-REALLY-SLOW
         ACL2::MAYBE-ADD-EXTRA-INFO-LIT ACL2::HL-HSPACE-HONS-NORMED
         ACL2::PRIN1-WITH-SLASHES1 ACL2::OCCUR-AFFINITY
         ACL2::IF-INTERP-ADD-CLAUSE ACL2::ADD-TAU-MV-NTH-SYNONYM-RULE
         ACL2::ADD-REFINEMENT-RULE ACL2::IF-SEARCH-BUCKET
         ACL2::CONTROLLERS)) 
(COMMON-LISP::PROCLAIM
    '(COMMON-LISP::FTYPE
         (COMMON-LISP::FUNCTION
             (COMMON-LISP::T COMMON-LISP::T COMMON-LISP::FIXNUM
                 COMMON-LISP::FIXNUM)
             COMMON-LISP::T)
         ACL2::STOBJ-COPY-ARRAY-AREF ACL2::AREF2
         ACL2::LONGEST-COMMON-TAIL-LENGTH-REC)) 
(COMMON-LISP::PROCLAIM
    '(COMMON-LISP::FTYPE
         (COMMON-LISP::FUNCTION
             (COMMON-LISP::T COMMON-LISP::T COMMON-LISP::T
                 COMMON-LISP::T COMMON-LISP::T COMMON-LISP::T
                 COMMON-LISP::T)
             COMMON-LISP::T)
         ACL2::CHK-STOBJ-LET ACL2::ADD-META-RULE
         ACL2::MEASURE-CLAUSES-FOR-FN ACL2::PEQUIV-INFO-FOR-REWRITE
         ACL2::FORCE-ASSUMPTION1 ACL2::EXTRACT-AND-CLASSIFY-LEMMAS2
         ACL2::EVERY-OCCURRENCE-EQUIV-HITTABLEP1 ACL2::ONEIFY-FAIL-FORM
         ACL2::SUBSUMES!1-EQUALITY-WITH-CONST ACL2::FORMAT-GOAL-TREE
         ACL2::EVERY-NEG-EVG-IN-TAU-P1 ACL2::ADD-INDUCTION-RULE
         ACL2::PIGEON-HOLEP1 ACL2::PRINT-SPLITTER-RULES-SUMMARY-1
         ACL2::FIX-PORTCULLIS-CMDS1
         ACL2::SHOW-DOUBLE-REWRITE-OPPORTUNITIES-LINEAR
         ACL2::APPLY-TOP-HINTS-CLAUSE-MSG1
         ACL2::UPDATE-ENABLED-STRUCTURE ACL2::MFC-RW+-TTREE
         ACL2::APPLICABLE-REWRITE-RULES ACL2::INITIAL-PSPV
         ACL2::EV-FNCALL-GUARD-ER-MSG
         ACL2::DOUBLE-REWRITE-OPPORTUNITIES ACL2::MAKE-EVENT-TUPLE
         ACL2::EQUIV-HITTABLE-IN-SOME-OTHER-LIT
         ACL2::SUGGESTED-INDUCTION-CANDS
         ACL2::MAKE-INCLUDE-BOOKS-ABSOLUTE ACL2::PRINT-INFIX
         ACL2::BDD-TOP ACL2::FLESH-OUT-INDUCTION-PRINCIPLE
         ACL2::PUTPROP-JUSTIFICATION-LST ACL2::MAYBE-WARN-ABOUT-THEORY
         ACL2::TERMINATION-THEOREM-CLAUSES ACL2::ADD-RULES
         ACL2_*1*_ACL2::MFC-RW+-TTREE ACL2::SIMPLIFY-CLAUSE-MSG1
         ACL2::REDUNDANT-OR-RECLASSIFYING-DEFUNSP10
         ACL2::SHOW-TYPE-PRESCRIPTION-RULE
         ACL2::APPLICABLE-REWRITE-RULES1 ACL2::COLLECT-FC-STATUS
         ACL2::NOMINATE-DESTRUCTOR-CANDIDATES ACL2::SAVE-EXEC-FN
         ACL2::PUTPROP-FORWARD-CHAINING-RULES-LST
         ACL2::MEASURE-CLAUSES-FOR-CLIQUE
         ACL2::NOMINATE-DESTRUCTOR-CANDIDATES-LST
         ACL2::POLYS-FROM-TYPE-SET
         ACL2::EVERY-OCCURRENCE-EQUIV-HITTABLEP1-LISTP
         ACL2::COMBINE-POS/NEG-PAIRS-FROM-TAU1 ACL2::TIGHTEN-BOUND
         ACL2::TIME-TRACKER-FN)) 
(COMMON-LISP::PROCLAIM
    '(COMMON-LISP::FTYPE
         (COMMON-LISP::FUNCTION
             (COMMON-LISP::T COMMON-LISP::T COMMON-LISP::FIXNUM)
             COMMON-LISP::T)
         ACL2::BASIC-WORSE-THAN ACL2::SOME-SUBTERM-WORSE-THAN-OR-EQUAL
         ACL2::AREF1 ACL2::WORSE-THAN-OR-EQUAL-BUILTIN-CLOCKED
         ACL2::BASIC-WORSE-THAN-LST1
         ACL2::SOME-SUBTERM-WORSE-THAN-OR-EQUAL-LST
         ACL2::WORSE-THAN-LST ACL2::WORSE-THAN-BUILTIN-CLOCKED
         ACL2::BASIC-WORSE-THAN-LST2)) 
(COMMON-LISP::PROCLAIM
    '(COMMON-LISP::FTYPE
         (COMMON-LISP::FUNCTION
             (COMMON-LISP::T COMMON-LISP::T COMMON-LISP::T
                 COMMON-LISP::T COMMON-LISP::T COMMON-LISP::T
                 COMMON-LISP::T COMMON-LISP::T)
             COMMON-LISP::T)
         ACL2::ABSSTOBJ-CORRESPONDENCE-FORMULA ACL2::ADD-REWRITE-RULE1
         ACL2::RELEVANT-POSNS-CLIQUE-INIT
         ACL2::IRRELEVANT-NON-LAMBDA-SLOTS-CLIQUE
         ACL2::NOTE-RELIEVE-HYPS-FAILURE-FREE ACL2::BRKPT2
         ACL2::RELEVANT-POSNS-CALL ACL2::ADD-TYPE-PRESCRIPTION-RULE
         ACL2::ADD-REWRITE-RULE ACL2::GENEQV-FOR-REWRITE
         ACL2::APPLY-INDUCTION-RULE ACL2::LINEARIZE ACL2::NEW-FC-CALL
         ACL2::LINEARIZE1 ACL2::RELEVANT-POSNS-CLIQUE
         ACL2::ABSSTOBJ-PRESERVED-FORMULA ACL2::NEG-EVGS-NEAR-SUBSETP
         ACL2::FORMAT-GOAL-TREE-LST
         ACL2::SHOW-DOUBLE-REWRITE-OPPORTUNITIES1
         ACL2::SUGGESTED-INDUCTION-CANDS1
         ACL2::NOMINATE-DESTRUCTOR-CANDIDATE
         ACL2::SUBSUMES1-EQUALITY-WITH-CONST ACL2::ADD-DEFINITION-RULE
         ACL2::TILDE-@-DEFPKG-ERROR-PHRASE
         ACL2::SHOW-TYPE-PRESCRIPTION-RULES1 ACL2::FLATSIZE-INFIX
         ACL2_*1*_ACL2::MFC-RELIEVE-HYP-TTREE
         ACL2::MFC-RELIEVE-HYP-TTREE ACL2::INCREMENT-PROOF-TREE
         ACL2::MAKE-LDDS-COMMAND-BLOCK1)) 
(COMMON-LISP::PROCLAIM
    '(COMMON-LISP::FTYPE
         (COMMON-LISP::FUNCTION
             (COMMON-LISP::T COMMON-LISP::T COMMON-LISP::T
                 COMMON-LISP::T COMMON-LISP::T COMMON-LISP::T
                 COMMON-LISP::T COMMON-LISP::T COMMON-LISP::T
                 COMMON-LISP::T)
             COMMON-LISP::T)
         ACL2::MEMOIZE-FN-DEF ACL2::SEARCH-FN ACL2::HL-HSPACE-RESIZE
         ACL2::ADD-FC-DERIVATIONS ACL2::TYPE-SET-LST
         ACL2::SEARCH-FN-GUARD ACL2::PRINT-ENCAPSULATE-MSG3
         ACL2::CREATE-REWRITE-RULE ACL2::ADD-LINEAR-RULE2)) 
(COMMON-LISP::PROCLAIM
    '(COMMON-LISP::FTYPE
         (COMMON-LISP::FUNCTION
             (COMMON-LISP::T COMMON-LISP::T COMMON-LISP::T
                 COMMON-LISP::T COMMON-LISP::T COMMON-LISP::T
                 COMMON-LISP::T COMMON-LISP::T COMMON-LISP::T
                 COMMON-LISP::T COMMON-LISP::T)
             COMMON-LISP::T)
         ACL2::SHOW-REWRITES-LINEARS-FN ACL2::LABELS-FORM-FOR-*1*
         ACL2::EXTEND-TYPE-ALIST1 ACL2::SHOW-REWRITES-LINEARS
         ACL2::REDUNDANT-OR-RECLASSIFYING-DEFUNSP
         ACL2::EXTEND-TYPE-ALIST-WITH-BINDINGS ACL2::FIX-EXEC-XARGS)) 
(COMMON-LISP::PROCLAIM
    '(COMMON-LISP::FTYPE
         (COMMON-LISP::FUNCTION
             (COMMON-LISP::FIXNUM COMMON-LISP::FIXNUM COMMON-LISP::T)
             COMMON-LISP::T)
         ACL2::SAFE-INCF-AUX-ERROR ACL2::ASET-32-BIT-INTEGER-STACK)) 
(COMMON-LISP::PROCLAIM
    '(COMMON-LISP::FTYPE
         (COMMON-LISP::FUNCTION
             (COMMON-LISP::T COMMON-LISP::T COMMON-LISP::T
                 COMMON-LISP::T COMMON-LISP::T COMMON-LISP::T
                 COMMON-LISP::T COMMON-LISP::T COMMON-LISP::T
                 COMMON-LISP::T COMMON-LISP::T COMMON-LISP::T
                 COMMON-LISP::T)
             COMMON-LISP::T)
         ACL2::EXTEND-WITH-PROPER/IMPROPER-CONS-TS-TUPLE
         ACL2::MEMOIZE-FORM)) 
(COMMON-LISP::PROCLAIM
    '(COMMON-LISP::FTYPE
         (COMMON-LISP::FUNCTION
             (COMMON-LISP::T COMMON-LISP::T COMMON-LISP::T
                 COMMON-LISP::T COMMON-LISP::*)
             COMMON-LISP::T)
         ACL2::MEMOIZE-LOOK-UP-DEF ACL2::ONEIFY-CLTL-CODE)) 
(COMMON-LISP::PROCLAIM
    '(COMMON-LISP::FTYPE
         (COMMON-LISP::FUNCTION
             (COMMON-LISP::T COMMON-LISP::FIXNUM COMMON-LISP::FIXNUM)
             COMMON-LISP::FIXNUM)
         ACL2::FLSZ-INTEGER ACL2::FN-COUNT-EVG-REC)) 
(COMMON-LISP::PROCLAIM
    '(COMMON-LISP::FTYPE
         (COMMON-LISP::FUNCTION
             (COMMON-LISP::T COMMON-LISP::T COMMON-LISP::*)
             COMMON-LISP::T)
         ACL2::CUSTOM-TRACE-PPR ACL2::MF-LOOKING-AT ACL2::ONEIFIED-DEF
         ACL2::MAYBE-PUSH-UNDO-STACK)) 
(COMMON-LISP::PROCLAIM
    '(COMMON-LISP::FTYPE
         (COMMON-LISP::FUNCTION
             (COMMON-LISP::FIXNUM COMMON-LISP::FIXNUM COMMON-LISP::T
                 COMMON-LISP::T)
             COMMON-LISP::T)
         ACL2::SPACES)) 
(COMMON-LISP::PROCLAIM
    '(COMMON-LISP::FTYPE
         (COMMON-LISP::FUNCTION
             (COMMON-LISP::T COMMON-LISP::T COMMON-LISP::T
                 COMMON-LISP::*)
             COMMON-LISP::T)
         ACL2::MEMOIZE-FN-FORMALS)) 
(COMMON-LISP::PROCLAIM
    '(COMMON-LISP::FTYPE
         (COMMON-LISP::FUNCTION
             (COMMON-LISP::T COMMON-LISP::T COMMON-LISP::T
                 COMMON-LISP::T COMMON-LISP::T COMMON-LISP::T
                 COMMON-LISP::T COMMON-LISP::T COMMON-LISP::T
                 COMMON-LISP::T COMMON-LISP::T COMMON-LISP::T
                 COMMON-LISP::T COMMON-LISP::T COMMON-LISP::T
                 COMMON-LISP::T)
             COMMON-LISP::T)
         ACL2::MEMOIZE-FN-INNER-BODY)) 
(COMMON-LISP::PROCLAIM
    '(COMMON-LISP::FTYPE
         (COMMON-LISP::FUNCTION
             (COMMON-LISP::T COMMON-LISP::T COMMON-LISP::FIXNUM
                 COMMON-LISP::FIXNUM COMMON-LISP::T)
             COMMON-LISP::T)
         ACL2::TOO-MANY-IFS1 ACL2::ASET2)) 
(COMMON-LISP::PROCLAIM
    '(COMMON-LISP::FTYPE
         (COMMON-LISP::FUNCTION
             (COMMON-LISP::T COMMON-LISP::T COMMON-LISP::BIT-VECTOR
                 COMMON-LISP::T COMMON-LISP::T)
             COMMON-LISP::T)
         ACL2::HL-HSPACE-STATIC-RESTORE)) 
(COMMON-LISP::PROCLAIM
    '(COMMON-LISP::FTYPE
         (COMMON-LISP::FUNCTION
             (COMMON-LISP::T COMMON-LISP::T COMMON-LISP::FIXNUM
                 COMMON-LISP::T)
             COMMON-LISP::T)
         ACL2::TOO-MANY-IFS0 ACL2::ASET1)) 
(COMMON-LISP::PROCLAIM
    '(COMMON-LISP::FTYPE
         (COMMON-LISP::FUNCTION
             (COMMON-LISP::T COMMON-LISP::T COMMON-LISP::T
                 COMMON-LISP::FIXNUM COMMON-LISP::T COMMON-LISP::T
                 COMMON-LISP::T COMMON-LISP::T)
             COMMON-LISP::T)
         ACL2::THEORY-WARNING-FNS-AUX)) 
(COMMON-LISP::PROCLAIM
    '(COMMON-LISP::FTYPE
         (COMMON-LISP::FUNCTION
             (COMMON-LISP::T COMMON-LISP::FIXNUM COMMON-LISP::T
                 COMMON-LISP::FIXNUM COMMON-LISP::T)
             COMMON-LISP::FIXNUM)
         ACL2::FLSZ-ATOM)) 
(COMMON-LISP::PROCLAIM
    '(COMMON-LISP::FTYPE
         (COMMON-LISP::FUNCTION
             (COMMON-LISP::T COMMON-LISP::T COMMON-LISP::T
                 COMMON-LISP::T COMMON-LISP::T COMMON-LISP::T
                 COMMON-LISP::T COMMON-LISP::T COMMON-LISP::T
                 COMMON-LISP::T COMMON-LISP::T COMMON-LISP::T
                 COMMON-LISP::T COMMON-LISP::T COMMON-LISP::T
                 COMMON-LISP::T COMMON-LISP::T COMMON-LISP::T
                 COMMON-LISP::T COMMON-LISP::T)
             COMMON-LISP::T)
         ACL2::BOOKDATA-ALIST1 ACL2::SHOW-REWRITE-LINEAR)) 
(COMMON-LISP::PROCLAIM
    '(COMMON-LISP::FTYPE
         (COMMON-LISP::FUNCTION
             (COMMON-LISP::T COMMON-LISP::T COMMON-LISP::T
                 COMMON-LISP::T COMMON-LISP::T COMMON-LISP::T
                 COMMON-LISP::T COMMON-LISP::T COMMON-LISP::T
                 COMMON-LISP::T COMMON-LISP::T COMMON-LISP::T
                 COMMON-LISP::T COMMON-LISP::T COMMON-LISP::T)
             COMMON-LISP::T)
         ACL2::INDUCT-MSG/CONTINUE ACL2::BUILD-STATE1)) 
(COMMON-LISP::PROCLAIM
    '(COMMON-LISP::FTYPE
         (COMMON-LISP::FUNCTION
             (COMMON-LISP::FIXNUM COMMON-LISP::FIXNUM
                 COMMON-LISP::FIXNUM COMMON-LISP::T COMMON-LISP::T)
             COMMON-LISP::T)
         ACL2::SPACES1)) 
(COMMON-LISP::PROCLAIM
    '(COMMON-LISP::FTYPE
         (COMMON-LISP::FUNCTION
             (COMMON-LISP::T COMMON-LISP::T COMMON-LISP::T
                 COMMON-LISP::T COMMON-LISP::FIXNUM COMMON-LISP::T
                 COMMON-LISP::T COMMON-LISP::T)
             COMMON-LISP::T)
         ACL2::FMT-PPR)) 
(COMMON-LISP::PROCLAIM
    '(COMMON-LISP::FTYPE
         (COMMON-LISP::FUNCTION
             (COMMON-LISP::T COMMON-LISP::T COMMON-LISP::T
                 COMMON-LISP::T COMMON-LISP::T COMMON-LISP::T
                 COMMON-LISP::T COMMON-LISP::T COMMON-LISP::T
                 COMMON-LISP::T COMMON-LISP::T COMMON-LISP::T)
             COMMON-LISP::T)
         ACL2::WITH-OUTPUT-FN))