1(*****************************************************************************) 2(* Defines the list of triples ACL2_PACKAGE_ALIST representing the *) 3(* initial ACL2 package structure. *) 4(* *) 5(* Also defines a predicate VALID_PKG_TRIPLES from Matt Kaufmann that *) 6(* abstracts key properties of the package structure and verifies: *) 7(* *) 8(* |- VALID_PKG_TRIPLES ACL2_PACKAGE_ALIST *) 9(* *) 10(* Modified again to split into 4 equal length lists, hence O(n. log n) *) 11(* *) 12(*****************************************************************************) 13 14(*****************************************************************************) 15(* Ignore everything up to "END BOILERPLATE" *) 16(*****************************************************************************) 17 18(*****************************************************************************) 19(* START BOILERPLATE NEEDED FOR COMPILATION *) 20(*****************************************************************************) 21 22(****************************************************************************** 23* Load theories 24******************************************************************************) 25(* The commented out stuff below should be loaded in interactive sessions 26quietdec := true; 27load "stringLib"; 28open stringLib; 29Globals.checking_const_names := false; 30quietdec := false; 31*) 32 33(****************************************************************************** 34* Boilerplate needed for compilation: open HOL4 systems modules. 35******************************************************************************) 36 37open HolKernel Parse boolLib bossLib; 38 39(****************************************************************************** 40* Open theories (including ratTheory from Jens Brandt). 41******************************************************************************) 42 43open listSyntax pairSyntax stringLib listTheory; 44 45(*****************************************************************************) 46(* END BOILERPLATE *) 47(*****************************************************************************) 48 49(*****************************************************************************) 50(* Start new theory "acl2_package" *) 51(*****************************************************************************) 52val _ = new_theory "acl2_package"; 53 54(*****************************************************************************) 55(* ACL2_PACKAGE_ALIST contains a list of triples *) 56(* *) 57(* (symbol-name , known-pkg-name , actual-pkg-name) *) 58(* *) 59(* The idea is that when symbol-name is interned into known-pkg-name, the *) 60(* resulting symbol's package name is actual-pkg-name. That is, the *) 61(* symbol with name symbol-name and package-name actual-pkg-name is *) 62(* imported into package known-pkg-name. *) 63(*****************************************************************************) 64 65 66(*****************************************************************************) 67(* Building a term directly out of a slurped in ACL2 package structure *) 68(* (e.g. kpa-v2-9-3.ml) breaks the HOL compiler. We therefore fold in the *) 69(* abbreviations below (this idea due to Konrad). It is strange that *) 70(* rewriting the big term is no problem, but compiling it breaks. *) 71(*****************************************************************************) 72val ACL2_CL_def = Define `ACL2_CL = ("ACL2", "COMMON-LISP")`; 73val ACL2_USER_def = Define `ACL2_USER = ("ACL2-USER" , "ACL2")`; 74val ACL_USER_CL_def = Define `ACL2_USER_CL = ("ACL2-USER" , "COMMON-LISP")`; 75 76(*****************************************************************************) 77(* Convert imported ACL2 package structure: *) 78(* *) 79(* [ *) 80(* ("&", "ACL2-USER", "ACL2"), *) 81(* ("*ACL2-EXPORTS*", "ACL2-USER", "ACL2"), *) 82(* ... *) 83(* ("VALUES", "ACL2", "COMMON-LISP"), *) 84(* ("ZEROP", "ACL2", "COMMON-LISP") *) 85(* ] *) 86(* *) 87(* to corresponding term, then fold in ACL2_CL_def, ACL2_USER_def and *) 88(* ACL_USER_CL_def using REWRITE_CONV, then extract the simplified term. *) 89(* Used to define ACL2_PACKAGE_ALIST *) 90(*****************************************************************************) 91 92fun make_package_structure_term l = 93 rhs 94 (concl 95 (REWRITE_CONV 96 (map GSYM [ACL2_CL_def,ACL2_USER_def,ACL_USER_CL_def]) 97 (mk_list 98 (map 99 (fn (s1,s2,s3) => 100 mk_pair(fromMLstring s1, mk_pair(fromMLstring s2, fromMLstring s3))) 101 l, 102 ``:string # string # string``)))); 103 104(*****************************************************************************) 105(* The actual triples specifying the initial ACL2 package *) 106(*****************************************************************************) 107 108val ACL2_PACKAGE_ALIST_def = 109 time 110 Define 111 `ACL2_PACKAGE_ALIST = 112 ^(make_package_structure_term 113(* Following List is cut and pasted from ACL2 generated file kpa-v2-9-3.ml *) 114[ 115("&", "ACL2-USER", "ACL2"), 116("*ACL2-EXPORTS*", "ACL2-USER", "ACL2"), 117("*COMMON-LISP-SPECIALS-AND-CONSTANTS*", "ACL2-USER", "ACL2"), 118("*COMMON-LISP-SYMBOLS-FROM-MAIN-LISP-PACKAGE*", "ACL2-USER", "ACL2"), 119("*MAIN-LISP-PACKAGE-NAME*", "ACL2-USER", "ACL2"), 120("*STANDARD-CHARS*", "ACL2-USER", "ACL2"), 121("*STANDARD-CI*", "ACL2-USER", "ACL2"), 122("*STANDARD-CO*", "ACL2-USER", "ACL2"), 123("*STANDARD-OI*", "ACL2-USER", "ACL2"), 124("32-BIT-INTEGER-LISTP", "ACL2-USER", "ACL2"), 125("32-BIT-INTEGER-LISTP-FORWARD-TO-INTEGER-LISTP", "ACL2-USER", "ACL2"), 126("32-BIT-INTEGER-STACK", "ACL2-USER", "ACL2"), 127("32-BIT-INTEGER-STACK-LENGTH", "ACL2-USER", "ACL2"), 128("32-BIT-INTEGER-STACK-LENGTH1", "ACL2-USER", "ACL2"), 129("32-BIT-INTEGERP", "ACL2-USER", "ACL2"), 130("32-BIT-INTEGERP-FORWARD-TO-INTEGERP", "ACL2-USER", "ACL2"), 131("<-ON-OTHERS", "ACL2-USER", "ACL2"), 132("?-FN", "ACL2-USER", "ACL2"), 133("@", "ACL2-USER", "ACL2"), 134("ABORT!", "ACL2-USER", "ACL2"), 135("ACCUMULATED-PERSISTENCE", "ACL2-USER", "ACL2"), 136("ACL2-COUNT", "ACL2-USER", "ACL2"), 137("ACL2-INPUT-CHANNEL-PACKAGE", "ACL2-USER", "ACL2"), 138("ACL2-NUMBERP", "ACL2-USER", "ACL2"), 139("ACL2-OUTPUT-CHANNEL-PACKAGE", "ACL2-USER", "ACL2"), 140("ACL2-PACKAGE", "ACL2-USER", "ACL2"), 141("ADD-DEFAULT-HINTS", "ACL2-USER", "ACL2"), 142("ADD-DEFAULT-HINTS!", "ACL2-USER", "ACL2"), 143("ADD-INVISIBLE-FNS", "ACL2-USER", "ACL2"), 144("ADD-MACRO-ALIAS", "ACL2-USER", "ACL2"), 145("ADD-NTH-ALIAS", "ACL2-USER", "ACL2"), 146("ADD-PAIR", "ACL2-USER", "ACL2"), 147("ADD-PAIR-PRESERVES-ALL-BOUNDP", "ACL2-USER", "ACL2"), 148("ADD-TIMERS", "ACL2-USER", "ACL2"), 149("ADD-TO-SET-EQ", "ACL2-USER", "ACL2"), 150("ADD-TO-SET-EQL", "ACL2-USER", "ACL2"), 151("ADD-TO-SET-EQUAL", "ACL2-USER", "ACL2"), 152("ALISTP", "ACL2-USER", "ACL2"), 153("ALISTP-FORWARD-TO-TRUE-LISTP", "ACL2-USER", "ACL2"), 154("ALL-BOUNDP", "ACL2-USER", "ACL2"), 155("ALL-BOUNDP-PRESERVES-ASSOC", "ACL2-USER", "ACL2"), 156("ALL-VARS", "ACL2-USER", "ACL2"), 157("ALL-VARS1", "ACL2-USER", "ACL2"), 158("ALL-VARS1-LST", "ACL2-USER", "ACL2"), 159("ALPHA-CHAR-P-FORWARD-TO-CHARACTERP", "ACL2-USER", "ACL2"), 160("AND-MACRO", "ACL2-USER", "ACL2"), 161("AREF-32-BIT-INTEGER-STACK", "ACL2-USER", "ACL2"), 162("AREF-T-STACK", "ACL2-USER", "ACL2"), 163("AREF1", "ACL2-USER", "ACL2"), 164("AREF2", "ACL2-USER", "ACL2"), 165("ARGS", "ACL2-USER", "ACL2"), 166("ARRAY1P", "ACL2-USER", "ACL2"), 167("ARRAY1P-CONS", "ACL2-USER", "ACL2"), 168("ARRAY1P-FORWARD", "ACL2-USER", "ACL2"), 169("ARRAY1P-LINEAR", "ACL2-USER", "ACL2"), 170("ARRAY2P", "ACL2-USER", "ACL2"), 171("ARRAY2P-CONS", "ACL2-USER", "ACL2"), 172("ARRAY2P-FORWARD", "ACL2-USER", "ACL2"), 173("ARRAY2P-LINEAR", "ACL2-USER", "ACL2"), 174("ASET-32-BIT-INTEGER-STACK", "ACL2-USER", "ACL2"), 175("ASET-T-STACK", "ACL2-USER", "ACL2"), 176("ASET1", "ACL2-USER", "ACL2"), 177("ASET2", "ACL2-USER", "ACL2"), 178("ASSIGN", "ACL2-USER", "ACL2"), 179("ASSOC-ADD-PAIR", "ACL2-USER", "ACL2"), 180("ASSOC-EQ", "ACL2-USER", "ACL2"), 181("ASSOC-EQ-EQUAL", "ACL2-USER", "ACL2"), 182("ASSOC-EQ-EQUAL-ALISTP", "ACL2-USER", "ACL2"), 183("ASSOC-EQUAL", "ACL2-USER", "ACL2"), 184("ASSOC-KEYWORD", "ACL2-USER", "ACL2"), 185("ASSOC-STRING-EQUAL", "ACL2-USER", "ACL2"), 186("ASSOC2", "ACL2-USER", "ACL2"), 187("ASSOCIATIVITY-OF-*", "ACL2-USER", "ACL2"), 188("ASSOCIATIVITY-OF-+", "ACL2-USER", "ACL2"), 189("ASSUME", "ACL2-USER", "ACL2"), 190("ATOM-LISTP", "ACL2-USER", "ACL2"), 191("ATOM-LISTP-FORWARD-TO-TRUE-LISTP", "ACL2-USER", "ACL2"), 192("BIG-CLOCK-ENTRY", "ACL2-USER", "ACL2"), 193("BIG-CLOCK-NEGATIVE-P", "ACL2-USER", "ACL2"), 194("BINARY-*", "ACL2-USER", "ACL2"), 195("BINARY-+", "ACL2-USER", "ACL2"), 196("BINARY-APPEND", "ACL2-USER", "ACL2"), 197("BIND-FREE", "ACL2-USER", "ACL2"), 198("BINOP-TABLE", "ACL2-USER", "ACL2"), 199("ADD-BINOP", "ACL2-USER", "ACL2"), 200("REMOVE-BINOP", "ACL2-USER", "ACL2"), 201("REMOVE-INVISIBLE-FNS", "ACL2-USER", "ACL2"), 202("BOOLEAN-LISTP", "ACL2-USER", "ACL2"), 203("BOOLEAN-LISTP-CONS", "ACL2-USER", "ACL2"), 204("BOOLEAN-LISTP-FORWARD", "ACL2-USER", "ACL2"), 205("BOOLEAN-LISTP-FORWARD-TO-SYMBOL-LISTP", "ACL2-USER", "ACL2"), 206("BOOLEANP", "ACL2-USER", "ACL2"), 207("BOOLEANP-CHARACTERP", "ACL2-USER", "ACL2"), 208("BOOLEANP-COMPOUND-RECOGNIZER", "ACL2-USER", "ACL2"), 209("BOUNDED-INTEGER-ALISTP", "ACL2-USER", "ACL2"), 210("BOUNDED-INTEGER-ALISTP-FORWARD-TO-EQLABLE-ALISTP", "ACL2-USER", "ACL2"), 211("BOUNDED-INTEGER-ALISTP2", "ACL2-USER", "ACL2"), 212("BOUNDP-GLOBAL", "ACL2-USER", "ACL2"), 213("BOUNDP-GLOBAL1", "ACL2-USER", "ACL2"), 214("BRR", "ACL2-USER", "ACL2"), 215("BRR@", "ACL2-USER", "ACL2"), 216("BUILD-STATE1", "ACL2-USER", "ACL2"), 217("CAR-CDR-ELIM", "ACL2-USER", "ACL2"), 218("CAR-CONS", "ACL2-USER", "ACL2"), 219("CASE-LIST", "ACL2-USER", "ACL2"), 220("CASE-LIST-CHECK", "ACL2-USER", "ACL2"), 221("CASE-MATCH", "ACL2-USER", "ACL2"), 222("CASE-SPLIT", "ACL2-USER", "ACL2"), 223("CASE-TEST", "ACL2-USER", "ACL2"), 224("CBD", "ACL2-USER", "ACL2"), 225("CDR-CONS", "ACL2-USER", "ACL2"), 226("CDRN", "ACL2-USER", "ACL2"), 227("CERTIFY-BOOK", "ACL2-USER", "ACL2"), 228("CERTIFY-BOOK!", "ACL2-USER", "ACL2"), 229("CHAR-CODE-CODE-CHAR-IS-IDENTITY", "ACL2-USER", "ACL2"), 230("CHAR-CODE-LINEAR", "ACL2-USER", "ACL2"), 231("CHARACTER-LISTP", "ACL2-USER", "ACL2"), 232("CHARACTER-LISTP-APPEND", "ACL2-USER", "ACL2"), 233("CHARACTER-LISTP-COERCE", "ACL2-USER", "ACL2"), 234("CHARACTER-LISTP-FORWARD-TO-EQLABLE-LISTP", "ACL2-USER", "ACL2"), 235("CHARACTER-LISTP-REMOVE-DUPLICATES-EQL", "ACL2-USER", "ACL2"), 236("CHARACTER-LISTP-REVAPPEND", "ACL2-USER", "ACL2"), 237("CHARACTER-LISTP-STRING-DOWNCASE-1", "ACL2-USER", "ACL2"), 238("CHARACTER-LISTP-STRING-UPCASE1-1", "ACL2-USER", "ACL2"), 239("CHARACTERP-CHAR-DOWNCASE", "ACL2-USER", "ACL2"), 240("CHARACTERP-CHAR-UPCASE", "ACL2-USER", "ACL2"), 241("CHARACTERP-NTH", "ACL2-USER", "ACL2"), 242("CHARACTERP-PAGE", "ACL2-USER", "ACL2"), 243("CHARACTERP-RUBOUT", "ACL2-USER", "ACL2"), 244("CHARACTERP-TAB", "ACL2-USER", "ACL2"), 245("CHECK-VARS-NOT-FREE", "ACL2-USER", "ACL2"), 246("CHECKPOINT-FORCED-GOALS", "ACL2-USER", "ACL2"), 247("CLAUSE", "ACL2-USER", "ACL2"), 248("CLOSE-INPUT-CHANNEL", "ACL2-USER", "ACL2"), 249("CLOSE-OUTPUT-CHANNEL", "ACL2-USER", "ACL2"), 250("CLOSURE", "ACL2-USER", "ACL2"), 251("CODE-CHAR-CHAR-CODE-IS-IDENTITY", "ACL2-USER", "ACL2"), 252("CODE-CHAR-TYPE", "ACL2-USER", "ACL2"), 253("COERCE-INVERSE-1", "ACL2-USER", "ACL2"), 254("COERCE-INVERSE-2", "ACL2-USER", "ACL2"), 255("COERCE-OBJECT-TO-STATE", "ACL2-USER", "ACL2"), 256("COERCE-STATE-TO-OBJECT", "ACL2-USER", "ACL2"), 257("COMMUTATIVITY-OF-*", "ACL2-USER", "ACL2"), 258("COMMUTATIVITY-OF-+", "ACL2-USER", "ACL2"), 259("COMP", "ACL2-USER", "ACL2"), 260("COMPLETION-OF-*", "ACL2-USER", "ACL2"), 261("COMPLETION-OF-+", "ACL2-USER", "ACL2"), 262("COMPLETION-OF-<", "ACL2-USER", "ACL2"), 263("COMPLETION-OF-CAR", "ACL2-USER", "ACL2"), 264("COMPLETION-OF-CDR", "ACL2-USER", "ACL2"), 265("COMPLETION-OF-CHAR-CODE", "ACL2-USER", "ACL2"), 266("COMPLETION-OF-CODE-CHAR", "ACL2-USER", "ACL2"), 267("COMPLETION-OF-COERCE", "ACL2-USER", "ACL2"), 268("COMPLETION-OF-COMPLEX", "ACL2-USER", "ACL2"), 269("COMPLETION-OF-DENOMINATOR", "ACL2-USER", "ACL2"), 270("COMPLETION-OF-IMAGPART", "ACL2-USER", "ACL2"), 271("COMPLETION-OF-INTERN-IN-PACKAGE-OF-SYMBOL", "ACL2-USER", "ACL2"), 272("COMPLETION-OF-NUMERATOR", "ACL2-USER", "ACL2"), 273("COMPLETION-OF-REALPART", "ACL2-USER", "ACL2"), 274("COMPLETION-OF-SYMBOL-NAME", "ACL2-USER", "ACL2"), 275("COMPLETION-OF-SYMBOL-PACKAGE-NAME", "ACL2-USER", "ACL2"), 276("COMPLETION-OF-UNARY-/", "ACL2-USER", "ACL2"), 277("COMPLETION-OF-UNARY-MINUS", "ACL2-USER", "ACL2"), 278("COMPLEX-0", "ACL2-USER", "ACL2"), 279("COMPLEX-DEFINITION", "ACL2-USER", "ACL2"), 280("COMPLEX-EQUAL", "ACL2-USER", "ACL2"), 281("COMPLEX-IMPLIES1", "ACL2-USER", "ACL2"), 282("COMPLEX-RATIONALP", "ACL2-USER", "ACL2"), 283("COMPRESS1", "ACL2-USER", "ACL2"), 284("COMPRESS11", "ACL2-USER", "ACL2"), 285("COMPRESS2", "ACL2-USER", "ACL2"), 286("COMPRESS21", "ACL2-USER", "ACL2"), 287("COMPRESS211", "ACL2-USER", "ACL2"), 288("COND-CLAUSESP", "ACL2-USER", "ACL2"), 289("COND-MACRO", "ACL2-USER", "ACL2"), 290("CONS-EQUAL", "ACL2-USER", "ACL2"), 291("CONSP-ASSOC", "ACL2-USER", "ACL2"), 292("CONSP-ASSOC-EQ", "ACL2-USER", "ACL2"), 293("CURRENT-PACKAGE", "ACL2-USER", "ACL2"), 294("CURRENT-THEORY", "ACL2-USER", "ACL2"), 295("CW-GSTACK", "ACL2-USER", "ACL2"), 296("CW", "ACL2-USER", "ACL2"), 297("DECREMENT-BIG-CLOCK", "ACL2-USER", "ACL2"), 298("DEFABBREV", "ACL2-USER", "ACL2"), 299("DEFAULT", "ACL2-USER", "ACL2"), 300("DEFAULT-*-1", "ACL2-USER", "ACL2"), 301("DEFAULT-*-2", "ACL2-USER", "ACL2"), 302("DEFAULT-+-1", "ACL2-USER", "ACL2"), 303("DEFAULT-+-2", "ACL2-USER", "ACL2"), 304("DEFAULT-<-1", "ACL2-USER", "ACL2"), 305("DEFAULT-<-2", "ACL2-USER", "ACL2"), 306("DEFAULT-CAR", "ACL2-USER", "ACL2"), 307("DEFAULT-CDR", "ACL2-USER", "ACL2"), 308("DEFAULT-CHAR-CODE", "ACL2-USER", "ACL2"), 309("DEFAULT-COERCE-1", "ACL2-USER", "ACL2"), 310("DEFAULT-COERCE-2", "ACL2-USER", "ACL2"), 311("DEFAULT-COERCE-3", "ACL2-USER", "ACL2"), 312("DEFAULT-COMPILE-FNS", "ACL2-USER", "ACL2"), 313("DEFAULT-COMPLEX-1", "ACL2-USER", "ACL2"), 314("DEFAULT-COMPLEX-2", "ACL2-USER", "ACL2"), 315("DEFAULT-DEFUN-MODE", "ACL2-USER", "ACL2"), 316("DEFAULT-DEFUN-MODE-FROM-STATE", "ACL2-USER", "ACL2"), 317("DEFAULT-DENOMINATOR", "ACL2-USER", "ACL2"), 318("DEFAULT-IMAGPART", "ACL2-USER", "ACL2"), 319("DEFAULT-MEASURE-FUNCTION", "ACL2-USER", "ACL2"), 320("DEFAULT-NUMERATOR", "ACL2-USER", "ACL2"), 321("DEFAULT-REALPART", "ACL2-USER", "ACL2"), 322("DEFAULT-SYMBOL-NAME", "ACL2-USER", "ACL2"), 323("DEFAULT-SYMBOL-PACKAGE-NAME", "ACL2-USER", "ACL2"), 324("DEFAULT-UNARY-/", "ACL2-USER", "ACL2"), 325("DEFAULT-UNARY-MINUS", "ACL2-USER", "ACL2"), 326("DEFAULT-VERIFY-GUARDS-EAGERNESS", "ACL2-USER", "ACL2"), 327("DEFAULT-WELL-FOUNDED-RELATION", "ACL2-USER", "ACL2"), 328("DEFAXIOM", "ACL2-USER", "ACL2"), 329("DEFCHOOSE", "ACL2-USER", "ACL2"), 330("DEFCONG", "ACL2-USER", "ACL2"), 331("DEFCONST", "ACL2-USER", "ACL2"), 332("DEFDOC", "ACL2-USER", "ACL2"), 333("DEFEQUIV", "ACL2-USER", "ACL2"), 334("DEFEVALUATOR", "ACL2-USER", "ACL2"), 335("DEFEXEC", "ACL2-USER", "ACL2"), 336("DEFINE-PC-ATOMIC-MACRO", "ACL2-USER", "ACL2"), 337("DEFINE-PC-HELP", "ACL2-USER", "ACL2"), 338("DEFINE-PC-MACRO", "ACL2-USER", "ACL2"), 339("DEFLABEL", "ACL2-USER", "ACL2"), 340("DEFPKG", "ACL2-USER", "ACL2"), 341("DEFREFINEMENT", "ACL2-USER", "ACL2"), 342("DEFSTOBJ", "ACL2-USER", "ACL2"), 343("DEFSTUB", "ACL2-USER", "ACL2"), 344("DEFTHEORY", "ACL2-USER", "ACL2"), 345("DEFTHM", "ACL2-USER", "ACL2"), 346("DEFTHMD", "ACL2-USER", "ACL2"), 347("DEFUND", "ACL2-USER", "ACL2"), 348("DEFUN-SK", "ACL2-USER", "ACL2"), 349("DEFUNS", "ACL2-USER", "ACL2"), 350("DELETE-PAIR", "ACL2-USER", "ACL2"), 351("DIGIT-TO-CHAR", "ACL2-USER", "ACL2"), 352("DIMENSIONS", "ACL2-USER", "ACL2"), 353("DISABLE", "ACL2-USER", "ACL2"), 354("DISABLE-FORCING", "ACL2-USER", "ACL2"), 355("DISABLEDP", "ACL2-USER", "ACL2"), 356("DISTRIBUTIVITY", "ACL2-USER", "ACL2"), 357("DOC", "ACL2-USER", "ACL2"), 358("DOC!", "ACL2-USER", "ACL2"), 359("DOCS", "ACL2-USER", "ACL2"), 360("DUPLICATES", "ACL2-USER", "ACL2"), 361("E/D", "ACL2-USER", "ACL2"), 362("E0-ORD-<", "ACL2-USER", "ACL2"), 363("E0-ORDINALP", "ACL2-USER", "ACL2"), 364("ELIMINATE-DESTRUCTORS", "ACL2-USER", "ACL2"), 365("ELIMINATE-IRRELEVANCE", "ACL2-USER", "ACL2"), 366("ENABLE", "ACL2-USER", "ACL2"), 367("ENABLE-FORCING", "ACL2-USER", "ACL2"), 368("ENCAPSULATE", "ACL2-USER", "ACL2"), 369("EQLABLE-ALISTP", "ACL2-USER", "ACL2"), 370("EQLABLE-ALISTP-FORWARD-TO-ALISTP", "ACL2-USER", "ACL2"), 371("EQLABLE-LISTP", "ACL2-USER", "ACL2"), 372("EQLABLE-LISTP-FORWARD-TO-ATOM-LISTP", "ACL2-USER", "ACL2"), 373("EQLABLEP", "ACL2-USER", "ACL2"), 374("EQLABLEP-RECOG", "ACL2-USER", "ACL2"), 375("EQUAL-CHAR-CODE", "ACL2-USER", "ACL2"), 376("ER", "ACL2-USER", "ACL2"), 377("ER-PROGN", "ACL2-USER", "ACL2"), 378("ER-PROGN-FN", "ACL2-USER", "ACL2"), 379("EVENS", "ACL2-USER", "ACL2"), 380("EVENT", "ACL2-USER", "ACL2"), 381("EXECUTABLE-COUNTERPART-THEORY", "ACL2-USER", "ACL2"), 382("EXPLODE-ATOM", "ACL2-USER", "ACL2"), 383("EXPLODE-NONNEGATIVE-INTEGER", "ACL2-USER", "ACL2"), 384("EXPT-TYPE-PRESCRIPTION-NON-ZERO-BASE", "ACL2-USER", "ACL2"), 385("EXTEND-32-BIT-INTEGER-STACK", "ACL2-USER", "ACL2"), 386("EXTEND-T-STACK", "ACL2-USER", "ACL2"), 387("EXTEND-WORLD", "ACL2-USER", "ACL2"), 388("FERTILIZE", "ACL2-USER", "ACL2"), 389("FGETPROP", "ACL2-USER", "ACL2"), 390("FILE-CLOCK", "ACL2-USER", "ACL2"), 391("FILE-CLOCK-P", "ACL2-USER", "ACL2"), 392("FILE-CLOCK-P-FORWARD-TO-INTEGERP", "ACL2-USER", "ACL2"), 393("FIRST-N-AC", "ACL2-USER", "ACL2"), 394("FIX", "ACL2-USER", "ACL2"), 395("FIX-TRUE-LIST", "ACL2-USER", "ACL2"), 396("FMS", "ACL2-USER", "ACL2"), 397("FMT", "ACL2-USER", "ACL2"), 398("FMT-TO-COMMENT-WINDOW", "ACL2-USER", "ACL2"), 399("FMT1", "ACL2-USER", "ACL2"), 400("FORCE", "ACL2-USER", "ACL2"), 401("FUNCTION-SYMBOLP", "ACL2-USER", "ACL2"), 402("FUNCTION-THEORY", "ACL2-USER", "ACL2"), 403("GENERALIZE", "ACL2-USER", "ACL2"), 404("GET-GLOBAL", "ACL2-USER", "ACL2"), 405("GET-TIMER", "ACL2-USER", "ACL2"), 406("GETPROP-DEFAULT", "ACL2-USER", "ACL2"), 407("GETPROPS", "ACL2-USER", "ACL2"), 408("GETPROPS1", "ACL2-USER", "ACL2"), 409("GLOBAL-TABLE", "ACL2-USER", "ACL2"), 410("GLOBAL-TABLE-CARS", "ACL2-USER", "ACL2"), 411("GLOBAL-TABLE-CARS1", "ACL2-USER", "ACL2"), 412("GLOBAL-VAL", "ACL2-USER", "ACL2"), 413("GOOD-BYE", "ACL2-USER", "ACL2"), 414("GOOD-DEFUN-MODE-P", "ACL2-USER", "ACL2"), 415("GROUND-ZERO", "ACL2-USER", "ACL2"), 416("HARD-ERROR", "ACL2-USER", "ACL2"), 417("HAS-PROPSP", "ACL2-USER", "ACL2"), 418("HAS-PROPSP1", "ACL2-USER", "ACL2"), 419("HEADER", "ACL2-USER", "ACL2"), 420("HELP", "ACL2-USER", "ACL2"), 421("HIDE", "ACL2-USER", "ACL2"), 422("I-AM-HERE", "ACL2-USER", "ACL2"), 423("ID", "ACL2-USER", "ACL2"), 424("IDATES", "ACL2-USER", "ACL2"), 425("IF*", "ACL2-USER", "ACL2"), 426("IFF", "ACL2-USER", "ACL2"), 427("IFF-IMPLIES-EQUAL-IMPLIES-1", "ACL2-USER", "ACL2"), 428("IFF-IMPLIES-EQUAL-IMPLIES-2", "ACL2-USER", "ACL2"), 429("IFF-IMPLIES-EQUAL-NOT", "ACL2-USER", "ACL2"), 430("IFF-IS-AN-EQUIVALENCE", "ACL2-USER", "ACL2"), 431("IFIX", "ACL2-USER", "ACL2"), 432("ILLEGAL", "ACL2-USER", "ACL2"), 433("IMAGPART-COMPLEX", "ACL2-USER", "ACL2"), 434("IMMEDIATE-FORCE-MODEP", "ACL2-USER", "ACL2"), 435("IMPLIES", "ACL2-USER", "ACL2"), 436("IMPROPER-CONSP", "ACL2-USER", "ACL2"), 437("IN-THEORY", "ACL2-USER", "ACL2"), 438("IN-ARITHMETIC-THEORY", "ACL2-USER", "ACL2"), 439("INCLUDE-BOOK", "ACL2-USER", "ACL2"), 440("INCOMPATIBLE", "ACL2-USER", "ACL2"), 441("INCREMENT-TIMER", "ACL2-USER", "ACL2"), 442("INDUCT", "ACL2-USER", "ACL2"), 443("INT=", "ACL2-USER", "ACL2"), 444("INTEGER-0", "ACL2-USER", "ACL2"), 445("INTEGER-1", "ACL2-USER", "ACL2"), 446("INTEGER-ABS", "ACL2-USER", "ACL2"), 447("INTEGER-IMPLIES-RATIONAL", "ACL2-USER", "ACL2"), 448("INTEGER-LISTP", "ACL2-USER", "ACL2"), 449("INTEGER-LISTP-FORWARD-TO-RATIONAL-LISTP", "ACL2-USER", "ACL2"), 450("INTEGER-STEP", "ACL2-USER", "ACL2"), 451("INTERN$", "ACL2-USER", "ACL2"), 452("INTERN-IN-PACKAGE-OF-SYMBOL", "ACL2-USER", "ACL2"), 453("INTERN-IN-PACKAGE-OF-SYMBOL-SYMBOL-NAME", "ACL2-USER", "ACL2"), 454("INTERSECTION-EQ", "ACL2-USER", "ACL2"), 455("INTERSECTION-THEORIES", "ACL2-USER", "ACL2"), 456("INTERSECTP-EQ", "ACL2-USER", "ACL2"), 457("INTERSECTP-EQUAL", "ACL2-USER", "ACL2"), 458("INVERSE-OF-*", "ACL2-USER", "ACL2"), 459("INVERSE-OF-+", "ACL2-USER", "ACL2"), 460("INVISIBLE-FNS-TABLE", "ACL2-USER", "ACL2"), 461("KEYWORD-PACKAGE", "ACL2-USER", "ACL2"), 462("KEYWORD-VALUE-LISTP", "ACL2-USER", "ACL2"), 463("KEYWORD-VALUE-LISTP-ASSOC-KEYWORD", "ACL2-USER", "ACL2"), 464("KEYWORD-VALUE-LISTP-FORWARD-TO-TRUE-LISTP", "ACL2-USER", "ACL2"), 465("KEYWORDP-FORWARD-TO-SYMBOLP", "ACL2-USER", "ACL2"), 466("KNOWN-PACKAGE-ALIST", "ACL2-USER", "ACL2"), 467("KNOWN-PACKAGE-ALISTP", "ACL2-USER", "ACL2"), 468("KNOWN-PACKAGE-ALISTP-FORWARD-TO-TRUE-LIST-LISTP-AND-ALISTP", "ACL2-USER", 469"ACL2"), 470("LD", "ACL2-USER", "ACL2"), 471("LD-ERROR-ACTION", "ACL2-USER", "ACL2"), 472("LD-ERROR-TRIPLES", "ACL2-USER", "ACL2"), 473("LD-KEYWORD-ALIASES", "ACL2-USER", "ACL2"), 474("LD-POST-EVAL-PRINT", "ACL2-USER", "ACL2"), 475("LD-PRE-EVAL-FILTER", "ACL2-USER", "ACL2"), 476("LD-PRE-EVAL-PRINT", "ACL2-USER", "ACL2"), 477("LD-PROMPT", "ACL2-USER", "ACL2"), 478("LD-QUERY-CONTROL-ALIST", "ACL2-USER", "ACL2"), 479("LD-REDEFINITION-ACTION", "ACL2-USER", "ACL2"), 480("LD-SKIP-PROOFSP", "ACL2-USER", "ACL2"), 481("LD-VERBOSE", "ACL2-USER", "ACL2"), 482("LEGAL-CASE-CLAUSESP", "ACL2-USER", "ACL2"), 483("LEN", "ACL2-USER", "ACL2"), 484("LEN-UPDATE-NTH", "ACL2-USER", "ACL2"), 485("LIST*-MACRO", "ACL2-USER", "ACL2"), 486("LIST-ALL-PACKAGE-NAMES", "ACL2-USER", "ACL2"), 487("LIST-ALL-PACKAGE-NAMES-LST", "ACL2-USER", "ACL2"), 488("LIST-MACRO", "ACL2-USER", "ACL2"), 489("LOCAL", "ACL2-USER", "ACL2"), 490("LOGIC", "ACL2-USER", "ACL2"), 491("LOWER-CASE-P-CHAR-DOWNCASE", "ACL2-USER", "ACL2"), 492("LOWER-CASE-P-FORWARD-TO-ALPHA-CHAR-P", "ACL2-USER", "ACL2"), 493("LOWEST-TERMS", "ACL2-USER", "ACL2"), 494("LP", "ACL2-USER", "ACL2"), 495("MACRO-ALIASES", "ACL2-USER", "ACL2"), 496("NTH-ALIASES", "ACL2-USER", "ACL2"), 497("MAIN-TIMER", "ACL2-USER", "ACL2"), 498("MAIN-TIMER-TYPE-PRESCRIPTION", "ACL2-USER", "ACL2"), 499("MAKE-CHARACTER-LIST", "ACL2-USER", "ACL2"), 500("MAKE-CHARACTER-LIST-MAKE-CHARACTER-LIST", "ACL2-USER", "ACL2"), 501("MAKE-FMT-BINDINGS", "ACL2-USER", "ACL2"), 502("MAKE-INPUT-CHANNEL", "ACL2-USER", "ACL2"), 503("MAKE-LIST-AC", "ACL2-USER", "ACL2"), 504("MAKE-MV-NTHS", "ACL2-USER", "ACL2"), 505("MAKE-ORD", "ACL2-USER", "ACL2"), 506("MAKE-OUTPUT-CHANNEL", "ACL2-USER", "ACL2"), 507("MAKE-VAR-LST", "ACL2-USER", "ACL2"), 508("MAKE-VAR-LST1", "ACL2-USER", "ACL2"), 509("MAKUNBOUND-GLOBAL", "ACL2-USER", "ACL2"), 510("MAXIMUM-LENGTH", "ACL2-USER", "ACL2"), 511("MAY-NEED-SLASHES", "ACL2-USER", "ACL2"), 512("MBE", "ACL2-USER", "ACL2"), 513("MBT", "ACL2-USER", "ACL2"), 514("MEMBER-EQ", "ACL2-USER", "ACL2"), 515("MEMBER-EQUAL", "ACL2-USER", "ACL2"), 516("MEMBER-SYMBOL-NAME", "ACL2-USER", "ACL2"), 517("MFC", "ACL2-USER", "ACL2"), 518("MINIMAL-THEORY", "ACL2-USER", "ACL2"), 519("MONITOR", "ACL2-USER", "ACL2"), 520("MONITORED-RUNES", "ACL2-USER", "ACL2"), 521("MORE", "ACL2-USER", "ACL2"), 522("MORE!", "ACL2-USER", "ACL2"), 523("MORE-DOC", "ACL2-USER", "ACL2"), 524("MUTUAL-RECURSION", "ACL2-USER", "ACL2"), 525("MUTUAL-RECURSION-GUARDP", "ACL2-USER", "ACL2"), 526("MV", "ACL2-USER", "ACL2"), 527("MV-LET", "ACL2-USER", "ACL2"), 528("MV-NTH", "ACL2-USER", "ACL2"), 529("NATP", "ACL2-USER", "ACL2"), 530("NEWLINE", "ACL2-USER", "ACL2"), 531("NFIX", "ACL2-USER", "ACL2"), 532("NIL-IS-NOT-CIRCULAR", "ACL2-USER", "ACL2"), 533("NO-DUPLICATESP", "ACL2-USER", "ACL2"), 534("NO-DUPLICATESP-EQUAL", "ACL2-USER", "ACL2"), 535("NONNEGATIVE-INTEGER-QUOTIENT", "ACL2-USER", "ACL2"), 536("NONNEGATIVE-PRODUCT", "ACL2-USER", "ACL2"), 537("NONZERO-IMAGPART", "ACL2-USER", "ACL2"), 538("NQTHM-TO-ACL2", "ACL2-USER", "ACL2"), 539("NTH-0-CONS", "ACL2-USER", "ACL2"), 540("NTH-0-READ-RUN-TIME-TYPE-PRESCRIPTION", "ACL2-USER", "ACL2"), 541("NTH-ADD1", "ACL2-USER", "ACL2"), 542("NTH-UPDATE-NTH", "ACL2-USER", "ACL2"), 543("O<", "ACL2-USER", "ACL2"), 544("O<=", "ACL2-USER", "ACL2"), 545("O>", "ACL2-USER", "ACL2"), 546("O>=", "ACL2-USER", "ACL2"), 547("O-FINP", "ACL2-USER", "ACL2"), 548("O-FIRST-COEFF", "ACL2-USER", "ACL2"), 549("O-FIRST-EXPT", "ACL2-USER", "ACL2"), 550("O-INFP", "ACL2-USER", "ACL2"), 551("O-P", "ACL2-USER", "ACL2"), 552("O-RST", "ACL2-USER", "ACL2"), 553("OBSERVATION", "ACL2-USER", "ACL2"), 554("ODDS", "ACL2-USER", "ACL2"), 555("OK-IF", "ACL2-USER", "ACL2"), 556("OOPS", "ACL2-USER", "ACL2"), 557("OPEN-CHANNEL-LISTP", "ACL2-USER", "ACL2"), 558("OPEN-CHANNEL1", "ACL2-USER", "ACL2"), 559("OPEN-CHANNEL1-FORWARD-TO-TRUE-LISTP-AND-CONSP", "ACL2-USER", "ACL2"), 560("OPEN-CHANNELS-P", "ACL2-USER", "ACL2"), 561("OPEN-CHANNELS-P-FORWARD", "ACL2-USER", "ACL2"), 562("OPEN-INPUT-CHANNEL", "ACL2-USER", "ACL2"), 563("OPEN-INPUT-CHANNEL-ANY-P", "ACL2-USER", "ACL2"), 564("OPEN-INPUT-CHANNEL-ANY-P1", "ACL2-USER", "ACL2"), 565("OPEN-INPUT-CHANNEL-P", "ACL2-USER", "ACL2"), 566("OPEN-INPUT-CHANNEL-P1", "ACL2-USER", "ACL2"), 567("OPEN-INPUT-CHANNELS", "ACL2-USER", "ACL2"), 568("OPEN-OUTPUT-CHANNEL", "ACL2-USER", "ACL2"), 569("OPEN-OUTPUT-CHANNEL-ANY-P", "ACL2-USER", "ACL2"), 570("OPEN-OUTPUT-CHANNEL-ANY-P1", "ACL2-USER", "ACL2"), 571("OPEN-OUTPUT-CHANNEL-P", "ACL2-USER", "ACL2"), 572("OPEN-OUTPUT-CHANNEL-P1", "ACL2-USER", "ACL2"), 573("OPEN-OUTPUT-CHANNELS", "ACL2-USER", "ACL2"), 574("OR-MACRO", "ACL2-USER", "ACL2"), 575("ORDERED-SYMBOL-ALISTP", "ACL2-USER", "ACL2"), 576("ORDERED-SYMBOL-ALISTP-ADD-PAIR", "ACL2-USER", "ACL2"), 577("ORDERED-SYMBOL-ALISTP-ADD-PAIR-FORWARD", "ACL2-USER", "ACL2"), 578("ORDERED-SYMBOL-ALISTP-FORWARD-TO-SYMBOL-ALISTP", "ACL2-USER", "ACL2"), 579("ORDERED-SYMBOL-ALISTP-GETPROPS", "ACL2-USER", "ACL2"), 580("ORDERED-SYMBOL-ALISTP-REMOVE-FIRST-PAIR", "ACL2-USER", "ACL2"), 581("OUR-DIGIT-CHAR-P", "ACL2-USER", "ACL2"), 582("PAIRLIS$", "ACL2-USER", "ACL2"), 583("PAIRLIS2", "ACL2-USER", "ACL2"), 584("PBT", "ACL2-USER", "ACL2"), 585("PC", "ACL2-USER", "ACL2"), 586("PCB", "ACL2-USER", "ACL2"), 587("PCB!", "ACL2-USER", "ACL2"), 588("PCS", "ACL2-USER", "ACL2"), 589("PE", "ACL2-USER", "ACL2"), 590("PE!", "ACL2-USER", "ACL2"), 591("PEEK-CHAR$", "ACL2-USER", "ACL2"), 592("PF", "ACL2-USER", "ACL2"), 593("PL", "ACL2-USER", "ACL2"), 594("POP-TIMER", "ACL2-USER", "ACL2"), 595("POSITION-AC", "ACL2-USER", "ACL2"), 596("POSITION-EQ", "ACL2-USER", "ACL2"), 597("POSITION-EQ-AC", "ACL2-USER", "ACL2"), 598("POSITION-EQUAL", "ACL2-USER", "ACL2"), 599("POSITION-EQUAL-AC", "ACL2-USER", "ACL2"), 600("POSITIVE", "ACL2-USER", "ACL2"), 601("POSP", "ACL2-USER", "ACL2"), 602("POWER-EVAL", "ACL2-USER", "ACL2"), 603("PPROGN", "ACL2-USER", "ACL2"), 604("PR", "ACL2-USER", "ACL2"), 605("PR!", "ACL2-USER", "ACL2"), 606("PREPROCESS", "ACL2-USER", "ACL2"), 607("PRIN1$", "ACL2-USER", "ACL2"), 608("PRIN1-WITH-SLASHES", "ACL2-USER", "ACL2"), 609("PRIN1-WITH-SLASHES1", "ACL2-USER", "ACL2"), 610("PRINC$", "ACL2-USER", "ACL2"), 611("PRINT-OBJECT$", "ACL2-USER", "ACL2"), 612("PRINT-RATIONAL-AS-DECIMAL", "ACL2-USER", "ACL2"), 613("PRINT-TIMER", "ACL2-USER", "ACL2"), 614("PROG2$", "ACL2-USER", "ACL2"), 615("PROGRAM", "ACL2-USER", "ACL2"), 616("PROOF-TREE", "ACL2-USER", "ACL2"), 617("PROOFS-CO", "ACL2-USER", "ACL2"), 618("PROPER-CONSP", "ACL2-USER", "ACL2"), 619("PROPS", "ACL2-USER", "ACL2"), 620("PROVE", "ACL2-USER", "ACL2"), 621("PSEUDO-TERM-LISTP", "ACL2-USER", "ACL2"), 622("PSEUDO-TERM-LISTP-FORWARD-TO-TRUE-LISTP", "ACL2-USER", "ACL2"), 623("PSEUDO-TERMP", "ACL2-USER", "ACL2"), 624("PSTACK", "ACL2-USER", "ACL2"), 625("PUFF", "ACL2-USER", "ACL2"), 626("PUFF*", "ACL2-USER", "ACL2"), 627("PUSH-TIMER", "ACL2-USER", "ACL2"), 628("PUSH-UNTOUCHABLE", "ACL2-USER", "ACL2"), 629("PUT-ASSOC-EQ", "ACL2-USER", "ACL2"), 630("PUT-ASSOC-EQUAL", "ACL2-USER", "ACL2"), 631("PUT-GLOBAL", "ACL2-USER", "ACL2"), 632("PUTPROP", "ACL2-USER", "ACL2"), 633("QUOTEP", "ACL2-USER", "ACL2"), 634("R-EQLABLE-ALISTP", "ACL2-USER", "ACL2"), 635("RASSOC-EQ", "ACL2-USER", "ACL2"), 636("RASSOC-EQUAL", "ACL2-USER", "ACL2"), 637("RATIONAL-IMPLIES1", "ACL2-USER", "ACL2"), 638("RATIONAL-IMPLIES2", "ACL2-USER", "ACL2"), 639("RATIONAL-LISTP", "ACL2-USER", "ACL2"), 640("RATIONAL-LISTP-FORWARD-TO-TRUE-LISTP", "ACL2-USER", "ACL2"), 641("RATIONALP-*", "ACL2-USER", "ACL2"), 642("RATIONALP-+", "ACL2-USER", "ACL2"), 643("RATIONALP-EXPT-TYPE-PRESCRIPTION", "ACL2-USER", "ACL2"), 644("RATIONALP-IMPLIES-ACL2-NUMBERP", "ACL2-USER", "ACL2"), 645("RATIONALP-UNARY--", "ACL2-USER", "ACL2"), 646("RATIONALP-UNARY-/", "ACL2-USER", "ACL2"), 647("READ-BYTE$", "ACL2-USER", "ACL2"), 648("READ-CHAR$", "ACL2-USER", "ACL2"), 649("READ-FILE-LISTP", "ACL2-USER", "ACL2"), 650("READ-FILE-LISTP-FORWARD-TO-TRUE-LIST-LISTP", "ACL2-USER", "ACL2"), 651("READ-FILE-LISTP1", "ACL2-USER", "ACL2"), 652("READ-FILE-LISTP1-FORWARD-TO-TRUE-LISTP-AND-CONSP", "ACL2-USER", "ACL2"), 653("READ-FILES", "ACL2-USER", "ACL2"), 654("READ-FILES-P", "ACL2-USER", "ACL2"), 655("READ-FILES-P-FORWARD-TO-READ-FILE-LISTP", "ACL2-USER", "ACL2"), 656("READ-IDATE", "ACL2-USER", "ACL2"), 657("READ-OBJECT", "ACL2-USER", "ACL2"), 658("READ-RUN-TIME", "ACL2-USER", "ACL2"), 659("READ-RUN-TIME-PRESERVES-STATE-P1", "ACL2-USER", "ACL2"), 660("READABLE-FILE", "ACL2-USER", "ACL2"), 661("READABLE-FILE-FORWARD-TO-TRUE-LISTP-AND-CONSP", "ACL2-USER", "ACL2"), 662("READABLE-FILES", "ACL2-USER", "ACL2"), 663("READABLE-FILES-LISTP", "ACL2-USER", "ACL2"), 664("READABLE-FILES-LISTP-FORWARD-TO-TRUE-LIST-LISTP-AND-ALISTP", "ACL2-USER", 665"ACL2"), 666("READABLE-FILES-P", "ACL2-USER", "ACL2"), 667("READABLE-FILES-P-FORWARD-TO-READABLE-FILES-LISTP", "ACL2-USER", "ACL2"), 668("REAL/RATIONALP", "ACL2-USER", "ACL2"), 669("REALFIX", "ACL2-USER", "ACL2"), 670("REALPART-COMPLEX", "ACL2-USER", "ACL2"), 671("REALPART-IMAGPART-ELIM", "ACL2-USER", "ACL2"), 672("REBUILD", "ACL2-USER", "ACL2"), 673("REDEF", "ACL2-USER", "ACL2"), 674("REDEF!", "ACL2-USER", "ACL2"), 675("REMOVE-DEFAULT-HINTS", "ACL2-USER", "ACL2"), 676("REMOVE-DEFAULT-HINTS!", "ACL2-USER", "ACL2"), 677("REMOVE-DUPLICATES-EQL", "ACL2-USER", "ACL2"), 678("REMOVE-DUPLICATES-EQUAL", "ACL2-USER", "ACL2"), 679("REMOVE-FIRST-PAIR", "ACL2-USER", "ACL2"), 680("REMOVE-MACRO-ALIAS", "ACL2-USER", "ACL2"), 681("REMOVE-NTH-ALIAS", "ACL2-USER", "ACL2"), 682("RESET-LD-SPECIALS", "ACL2-USER", "ACL2"), 683("RETRACT-WORLD", "ACL2-USER", "ACL2"), 684("RETRIEVE", "ACL2-USER", "ACL2"), 685("RFIX", "ACL2-USER", "ACL2"), 686("RUN-TIMES", "ACL2-USER", "ACL2"), 687("SET-BOGUS-MUTUAL-RECURSION-OK", "ACL2-USER", "ACL2"), 688("SET-CBD", "ACL2-USER", "ACL2"), 689("SET-CASE-SPLIT-LIMITATIONS", "ACL2-USER", "ACL2"), 690("SET-COMPILE-FNS", "ACL2-USER", "ACL2"), 691("SET-DEFAULT-HINTS", "ACL2-USER", "ACL2"), 692("SET-DEFAULT-HINTS!", "ACL2-USER", "ACL2"), 693("SET-DIFFERENCE-EQ", "ACL2-USER", "ACL2"), 694("SET-DIFFERENCE-EQUAL", "ACL2-USER", "ACL2"), 695("SET-DIFFERENCE-THEORIES", "ACL2-USER", "ACL2"), 696("SET-ENFORCE-REDUNDANCY", "ACL2-USER", "ACL2"), 697("SET-EQUALP-EQUAL", "ACL2-USER", "ACL2"), 698("SET-GUARD-CHECKING", "ACL2-USER", "ACL2"), 699("SET-IGNORE-OK", "ACL2-USER", "ACL2"), 700("SET-INHIBIT-OUTPUT-LST", "ACL2-USER", "ACL2"), 701("SET-INHIBIT-WARNINGS", "ACL2-USER", "ACL2"), 702("SET-INVISIBLE-FNS-TABLE", "ACL2-USER", "ACL2"), 703("SET-IRRELEVANT-FORMALS-OK", "ACL2-USER", "ACL2"), 704("SET-MEASURE-FUNCTION", "ACL2-USER", "ACL2"), 705("SET-NON-LINEARP", "ACL2-USER", "ACL2"), 706("SET-STATE-OK", "ACL2-USER", "ACL2"), 707("SET-TIMER", "ACL2-USER", "ACL2"), 708("SET-VERIFY-GUARDS-EAGERNESS", "ACL2-USER", "ACL2"), 709("SET-W", "ACL2-USER", "ACL2"), 710("SET-WELL-FOUNDED-RELATION", "ACL2-USER", "ACL2"), 711("SGETPROP", "ACL2-USER", "ACL2"), 712("SHOW-BDD", "ACL2-USER", "ACL2"), 713("SHOW-ACCUMULATED-PERSISTENCE", "ACL2-USER", "ACL2"), 714("SHRINK-32-BIT-INTEGER-STACK", "ACL2-USER", "ACL2"), 715("SHRINK-T-STACK", "ACL2-USER", "ACL2"), 716("SIMPLIFY", "ACL2-USER", "ACL2"), 717("SKIP-PROOFS", "ACL2-USER", "ACL2"), 718("SOME-SLASHABLE", "ACL2-USER", "ACL2"), 719("STABLE-UNDER-SIMPLIFICATIONP", "ACL2-USER", "ACL2"), 720("STANDARD-CHAR-LISTP", "ACL2-USER", "ACL2"), 721("STANDARD-CHAR-LISTP-APPEND", "ACL2-USER", "ACL2"), 722("STANDARD-CHAR-LISTP-FORWARD-TO-CHARACTER-LISTP", "ACL2-USER", "ACL2"), 723("STANDARD-CHAR-P-NTH", "ACL2-USER", "ACL2"), 724("STANDARD-CO", "ACL2-USER", "ACL2"), 725("STANDARD-OI", "ACL2-USER", "ACL2"), 726("START-PROOF-TREE", "ACL2-USER", "ACL2"), 727("STATE", "ACL2-USER", "ACL2"), 728("STATE-GLOBAL-LET*-CLEANUP", "ACL2-USER", "ACL2"), 729("STATE-GLOBAL-LET*-GET-GLOBALS", "ACL2-USER", "ACL2"), 730("STATE-GLOBAL-LET*-PUT-GLOBALS", "ACL2-USER", "ACL2"), 731("STATE-P", "ACL2-USER", "ACL2"), 732("STATE-P-IMPLIES-AND-FORWARD-TO-STATE-P1", "ACL2-USER", "ACL2"), 733("STATE-P1", "ACL2-USER", "ACL2"), 734("STATE-P1-FORWARD", "ACL2-USER", "ACL2"), 735("STATE-P1-UPDATE-MAIN-TIMER", "ACL2-USER", "ACL2"), 736("STATE-P1-UPDATE-NTH-2-WORLD", "ACL2-USER", "ACL2"), 737("STOP-PROOF-TREE", "ACL2-USER", "ACL2"), 738("STANDARD-STRING-ALISTP", "ACL2-USER", "ACL2"), 739("STANDARD-STRING-ALISTP-FORWARD-TO-ALISTP", "ACL2-USER", "ACL2"), 740("STRING-APPEND", "ACL2-USER", "ACL2"), 741("STRING-APPEND-LST", "ACL2-USER", "ACL2"), 742("STRING-DOWNCASE1", "ACL2-USER", "ACL2"), 743("STRING-EQUAL1", "ACL2-USER", "ACL2"), 744("STRING-IS-NOT-CIRCULAR", "ACL2-USER", "ACL2"), 745("STRING-LISTP", "ACL2-USER", "ACL2"), 746("STRING-UPCASE1", "ACL2-USER", "ACL2"), 747("STRING<-IRREFLEXIVE", "ACL2-USER", "ACL2"), 748("STRING<-L", "ACL2-USER", "ACL2"), 749("STRING<-L-ASYMMETRIC", "ACL2-USER", "ACL2"), 750("STRING<-L-IRREFLEXIVE", "ACL2-USER", "ACL2"), 751("STRING<-L-TRANSITIVE", "ACL2-USER", "ACL2"), 752("STRING<-L-TRICHOTOMY", "ACL2-USER", "ACL2"), 753("STRINGP-SYMBOL-PACKAGE-NAME", "ACL2-USER", "ACL2"), 754("STRIP-CARS", "ACL2-USER", "ACL2"), 755("STRIP-CDRS", "ACL2-USER", "ACL2"), 756("SUBSEQ-LIST", "ACL2-USER", "ACL2"), 757("SUBSETP-EQUAL", "ACL2-USER", "ACL2"), 758("SUBSTITUTE-AC", "ACL2-USER", "ACL2"), 759("SUMMARY", "ACL2-USER", "ACL2"), 760("SYMBOL-<", "ACL2-USER", "ACL2"), 761("SYMBOL-<-ASYMMETRIC", "ACL2-USER", "ACL2"), 762("SYMBOL-<-IRREFLEXIVE", "ACL2-USER", "ACL2"), 763("SYMBOL-<-TRANSITIVE", "ACL2-USER", "ACL2"), 764("SYMBOL-<-TRICHOTOMY", "ACL2-USER", "ACL2"), 765("SYMBOL-ALISTP", "ACL2-USER", "ACL2"), 766("SYMBOL-ALISTP-FORWARD-TO-EQLABLE-ALISTP", "ACL2-USER", "ACL2"), 767("SYMBOL-DOUBLET-LISTP", "ACL2-USER", "ACL2"), 768("SYMBOL-EQUALITY", "ACL2-USER", "ACL2"), 769("SYMBOL-LISTP", "ACL2-USER", "ACL2"), 770("SYMBOL-LISTP-FORWARD-TO-TRUE-LISTP", "ACL2-USER", "ACL2"), 771("SYMBOL-NAME-INTERN-IN-PACKAGE-OF-SYMBOL", "ACL2-USER", "ACL2"), 772("SYMBOL-PACKAGE-NAME", "ACL2-USER", "ACL2"), 773("SYMBOLP-INTERN-IN-PACKAGE-OF-SYMBOL", "ACL2-USER", "ACL2"), 774("SYNP", "ACL2-USER", "ACL2"), 775("SYNTAXP", "ACL2-USER", "ACL2"), 776("SYS-CALL", "ACL2-USER", "ACL2"), 777("SYS-CALL-STATUS", "ACL2-USER", "ACL2"), 778("T-STACK", "ACL2-USER", "ACL2"), 779("T-STACK-LENGTH", "ACL2-USER", "ACL2"), 780("T-STACK-LENGTH1", "ACL2-USER", "ACL2"), 781("TABLE", "ACL2-USER", "ACL2"), 782("TABLE-ALIST", "ACL2-USER", "ACL2"), 783("TAKE", "ACL2-USER", "ACL2"), 784("THE-ERROR", "ACL2-USER", "ACL2"), 785("THE-FIXNUM", "ACL2-USER", "ACL2"), 786("THE-FIXNUM!", "ACL2-USER", "ACL2"), 787("THEORY", "ACL2-USER", "ACL2"), 788("THEORY-INVARIANT", "ACL2-USER", "ACL2"), 789("THM", "ACL2-USER", "ACL2"), 790("TIMER-ALISTP", "ACL2-USER", "ACL2"), 791("TIMER-ALISTP-FORWARD-TO-TRUE-LIST-LISTP-AND-SYMBOL-ALISTP", "ACL2-USER", 792"ACL2"), 793("TOGGLE-PC-MACRO", "ACL2-USER", "ACL2"), 794("TRACE$", "ACL2-USER", "ACL2"), 795("TRANS", "ACL2-USER", "ACL2"), 796("TRANS1", "ACL2-USER", "ACL2"), 797("TRICHOTOMY", "ACL2-USER", "ACL2"), 798("TRUE-LISTP", "ACL2-USER", "ACL2"), 799("TRUE-LIST-LISTP", "ACL2-USER", "ACL2"), 800("TRUE-LIST-LISTP-FORWARD-TO-TRUE-LISTP", "ACL2-USER", "ACL2"), 801("TRUE-LIST-LISTP-FORWARD-TO-TRUE-LISTP-ASSOC-EQ", "ACL2-USER", "ACL2"), 802("TRUE-LISTP-CADR-ASSOC-EQ-FOR-OPEN-CHANNELS-P", "ACL2-USER", "ACL2"), 803("TRUE-LISTP-UPDATE-NTH", "ACL2-USER", "ACL2"), 804("TYPED-IO-LISTP", "ACL2-USER", "ACL2"), 805("TYPED-IO-LISTP-FORWARD-TO-TRUE-LISTP", "ACL2-USER", "ACL2"), 806("U", "ACL2-USER", "ACL2"), 807("UBT", "ACL2-USER", "ACL2"), 808("UBT!", "ACL2-USER", "ACL2"), 809("UNARY--", "ACL2-USER", "ACL2"), 810("UNARY-/", "ACL2-USER", "ACL2"), 811("UNARY-FUNCTION-SYMBOL-LISTP", "ACL2-USER", "ACL2"), 812("UNICITY-OF-0", "ACL2-USER", "ACL2"), 813("UNICITY-OF-1", "ACL2-USER", "ACL2"), 814("UNION-EQ", "ACL2-USER", "ACL2"), 815("UNION-EQUAL", "ACL2-USER", "ACL2"), 816("UNION-THEORIES", "ACL2-USER", "ACL2"), 817("UNIVERSAL-THEORY", "ACL2-USER", "ACL2"), 818("UNMONITOR", "ACL2-USER", "ACL2"), 819("UNSAVE", "ACL2-USER", "ACL2"), 820("UNTRACE$", "ACL2-USER", "ACL2"), 821("UPDATE-32-BIT-INTEGER-STACK", "ACL2-USER", "ACL2"), 822("UPDATE-BIG-CLOCK-ENTRY", "ACL2-USER", "ACL2"), 823("UPDATE-FILE-CLOCK", "ACL2-USER", "ACL2"), 824("UPDATE-GLOBAL-TABLE", "ACL2-USER", "ACL2"), 825("UPDATE-IDATES", "ACL2-USER", "ACL2"), 826("UPDATE-LIST-ALL-PACKAGE-NAMES-LST", "ACL2-USER", "ACL2"), 827("UPDATE-NTH", "ACL2-USER", "ACL2"), 828("UPDATE-OPEN-INPUT-CHANNELS", "ACL2-USER", "ACL2"), 829("UPDATE-OPEN-OUTPUT-CHANNELS", "ACL2-USER", "ACL2"), 830("UPDATE-READ-FILES", "ACL2-USER", "ACL2"), 831("UPDATE-RUN-TIMES", "ACL2-USER", "ACL2"), 832("UPDATE-RUN-TIMES-PRESERVES-STATE-P1", "ACL2-USER", "ACL2"), 833("UPDATE-T-STACK", "ACL2-USER", "ACL2"), 834("UPDATE-USER-STOBJ-ALIST", "ACL2-USER", "ACL2"), 835("UPDATE-USER-STOBJ-ALIST1", "ACL2-USER", "ACL2"), 836("UPDATE-WRITTEN-FILES", "ACL2-USER", "ACL2"), 837("UPPER-CASE-P-CHAR-UPCASE", "ACL2-USER", "ACL2"), 838("UPPER-CASE-P-FORWARD-TO-ALPHA-CHAR-P", "ACL2-USER", "ACL2"), 839("USER-STOBJ-ALIST", "ACL2-USER", "ACL2"), 840("USER-STOBJ-ALIST1", "ACL2-USER", "ACL2"), 841("VERBOSE-PSTACK", "ACL2-USER", "ACL2"), 842("VERIFY", "ACL2-USER", "ACL2"), 843("VERIFY-GUARDS", "ACL2-USER", "ACL2"), 844("VERIFY-TERMINATION", "ACL2-USER", "ACL2"), 845("W", "ACL2-USER", "ACL2"), 846("WARNING!", "ACL2-USER", "ACL2"), 847("WET", "ACL2-USER", "ACL2"), 848("WITH-OUTPUT", "ACL2-USER", "ACL2"), 849("WORLD", "ACL2-USER", "ACL2"), 850("WORLDP", "ACL2-USER", "ACL2"), 851("WORLDP-FORWARD-TO-ASSOC-EQ-EQUAL-ALISTP", "ACL2-USER", "ACL2"), 852("WORMHOLE", "ACL2-USER", "ACL2"), 853("WORMHOLE1", "ACL2-USER", "ACL2"), 854("WRITABLE-FILE-LISTP", "ACL2-USER", "ACL2"), 855("WRITABLE-FILE-LISTP-FORWARD-TO-TRUE-LIST-LISTP", "ACL2-USER", "ACL2"), 856("WRITABLE-FILE-LISTP1", "ACL2-USER", "ACL2"), 857("WRITABLE-FILE-LISTP1-FORWARD-TO-TRUE-LISTP-AND-CONSP", "ACL2-USER", 858"ACL2"), 859("WRITE-BYTE$", "ACL2-USER", "ACL2"), 860("WRITEABLE-FILES", "ACL2-USER", "ACL2"), 861("WRITEABLE-FILES-P", "ACL2-USER", "ACL2"), 862("WRITEABLE-FILES-P-FORWARD-TO-WRITABLE-FILE-LISTP", "ACL2-USER", "ACL2"), 863("WRITTEN-FILE", "ACL2-USER", "ACL2"), 864("WRITTEN-FILE-FORWARD-TO-TRUE-LISTP-AND-CONSP", "ACL2-USER", "ACL2"), 865("WRITTEN-FILE-LISTP", "ACL2-USER", "ACL2"), 866("WRITTEN-FILE-LISTP-FORWARD-TO-TRUE-LIST-LISTP-AND-ALISTP", "ACL2-USER", 867"ACL2"), 868("WRITTEN-FILES", "ACL2-USER", "ACL2"), 869("WRITTEN-FILES-P", "ACL2-USER", "ACL2"), 870("WRITTEN-FILES-P-FORWARD-TO-WRITTEN-FILE-LISTP", "ACL2-USER", "ACL2"), 871("XARGS", "ACL2-USER", "ACL2"), 872("XXXJOIN", "ACL2-USER", "ACL2"), 873("ZERO", "ACL2-USER", "ACL2"), 874("ZIP", "ACL2-USER", "ACL2"), 875("ZP", "ACL2-USER", "ACL2"), 876("&ALLOW-OTHER-KEYS", "ACL2-USER", "COMMON-LISP"), 877("*PRINT-MISER-WIDTH*", "ACL2-USER", "COMMON-LISP"), 878("&AUX", "ACL2-USER", "COMMON-LISP"), 879("*PRINT-PPRINT-DISPATCH*", "ACL2-USER", "COMMON-LISP"), 880("&BODY", "ACL2-USER", "COMMON-LISP"), 881("*PRINT-PRETTY*", "ACL2-USER", "COMMON-LISP"), 882("&ENVIRONMENT", "ACL2-USER", "COMMON-LISP"), 883("*PRINT-RADIX*", "ACL2-USER", "COMMON-LISP"), 884("&KEY", "ACL2-USER", "COMMON-LISP"), 885("*PRINT-READABLY*", "ACL2-USER", "COMMON-LISP"), 886("&OPTIONAL", "ACL2-USER", "COMMON-LISP"), 887("*PRINT-RIGHT-MARGIN*", "ACL2-USER", "COMMON-LISP"), 888("&REST", "ACL2-USER", "COMMON-LISP"), 889("*QUERY-IO*", "ACL2-USER", "COMMON-LISP"), 890("&WHOLE", "ACL2-USER", "COMMON-LISP"), 891("*RANDOM-STATE*", "ACL2-USER", "COMMON-LISP"), 892("*", "ACL2-USER", "COMMON-LISP"), 893("*READ-BASE*", "ACL2-USER", "COMMON-LISP"), 894("**", "ACL2-USER", "COMMON-LISP"), 895("*READ-DEFAULT-FLOAT-FORMAT*", "ACL2-USER", "COMMON-LISP"), 896("***", "ACL2-USER", "COMMON-LISP"), 897("*READ-EVAL*", "ACL2-USER", "COMMON-LISP"), 898("*BREAK-ON-SIGNALS*", "ACL2-USER", "COMMON-LISP"), 899("*READ-SUPPRESS*", "ACL2-USER", "COMMON-LISP"), 900("*COMPILE-FILE-PATHNAME*", "ACL2-USER", "COMMON-LISP"), 901("*READTABLE*", "ACL2-USER", "COMMON-LISP"), 902("*COMPILE-FILE-TRUENAME*", "ACL2-USER", "COMMON-LISP"), 903("*STANDARD-INPUT*", "ACL2-USER", "COMMON-LISP"), 904("*COMPILE-PRINT*", "ACL2-USER", "COMMON-LISP"), 905("*STANDARD-OUTPUT*", "ACL2-USER", "COMMON-LISP"), 906("*COMPILE-VERBOSE*", "ACL2-USER", "COMMON-LISP"), 907("*TERMINAL-IO*", "ACL2-USER", "COMMON-LISP"), 908("*DEBUG-IO*", "ACL2-USER", "COMMON-LISP"), 909("*TRACE-OUTPUT*", "ACL2-USER", "COMMON-LISP"), 910("*DEBUGGER-HOOK*", "ACL2-USER", "COMMON-LISP"), 911("+", "ACL2-USER", "COMMON-LISP"), 912("*DEFAULT-PATHNAME-DEFAULTS*", "ACL2-USER", "COMMON-LISP"), 913("++", "ACL2-USER", "COMMON-LISP"), 914("*ERROR-OUTPUT*", "ACL2-USER", "COMMON-LISP"), 915("+++", "ACL2-USER", "COMMON-LISP"), 916("*FEATURES*", "ACL2-USER", "COMMON-LISP"), 917("-", "ACL2-USER", "COMMON-LISP"), 918("*GENSYM-COUNTER*", "ACL2-USER", "COMMON-LISP"), 919("/", "ACL2-USER", "COMMON-LISP"), 920("*LOAD-PATHNAME*", "ACL2-USER", "COMMON-LISP"), 921("//", "ACL2-USER", "COMMON-LISP"), 922("*LOAD-PRINT*", "ACL2-USER", "COMMON-LISP"), 923("///", "ACL2-USER", "COMMON-LISP"), 924("*LOAD-TRUENAME*", "ACL2-USER", "COMMON-LISP"), 925("/=", "ACL2-USER", "COMMON-LISP"), 926("*LOAD-VERBOSE*", "ACL2-USER", "COMMON-LISP"), 927("1+", "ACL2-USER", "COMMON-LISP"), 928("*MACROEXPAND-HOOK*", "ACL2-USER", "COMMON-LISP"), 929("1-", "ACL2-USER", "COMMON-LISP"), 930("*MODULES*", "ACL2-USER", "COMMON-LISP"), 931("<", "ACL2-USER", "COMMON-LISP"), 932("*PACKAGE*", "ACL2-USER", "COMMON-LISP"), 933("<=", "ACL2-USER", "COMMON-LISP"), 934("*PRINT-ARRAY*", "ACL2-USER", "COMMON-LISP"), 935("=", "ACL2-USER", "COMMON-LISP"), 936("*PRINT-BASE*", "ACL2-USER", "COMMON-LISP"), 937(">", "ACL2-USER", "COMMON-LISP"), 938("*PRINT-CASE*", "ACL2-USER", "COMMON-LISP"), 939(">=", "ACL2-USER", "COMMON-LISP"), 940("*PRINT-CIRCLE*", "ACL2-USER", "COMMON-LISP"), 941("ABORT", "ACL2-USER", "COMMON-LISP"), 942("*PRINT-ESCAPE*", "ACL2-USER", "COMMON-LISP"), 943("ABS", "ACL2-USER", "COMMON-LISP"), 944("*PRINT-GENSYM*", "ACL2-USER", "COMMON-LISP"), 945("ACONS", "ACL2-USER", "COMMON-LISP"), 946("*PRINT-LENGTH*", "ACL2-USER", "COMMON-LISP"), 947("ACOS", "ACL2-USER", "COMMON-LISP"), 948("*PRINT-LEVEL*", "ACL2-USER", "COMMON-LISP"), 949("ACOSH", "ACL2-USER", "COMMON-LISP"), 950("*PRINT-LINES*", "ACL2-USER", "COMMON-LISP"), 951("ADD-METHOD", "ACL2-USER", "COMMON-LISP"), 952("ADJOIN", "ACL2-USER", "COMMON-LISP"), 953("ATOM", "ACL2-USER", "COMMON-LISP"), 954("BOUNDP", "ACL2-USER", "COMMON-LISP"), 955("ADJUST-ARRAY", "ACL2-USER", "COMMON-LISP"), 956("BASE-CHAR", "ACL2-USER", "COMMON-LISP"), 957("BREAK", "ACL2-USER", "COMMON-LISP"), 958("ADJUSTABLE-ARRAY-P", "ACL2-USER", "COMMON-LISP"), 959("BASE-STRING", "ACL2-USER", "COMMON-LISP"), 960("BROADCAST-STREAM", "ACL2-USER", "COMMON-LISP"), 961("ALLOCATE-INSTANCE", "ACL2-USER", "COMMON-LISP"), 962("BIGNUM", "ACL2-USER", "COMMON-LISP"), 963("BROADCAST-STREAM-STREAMS", "ACL2-USER", "COMMON-LISP"), 964("ALPHA-CHAR-P", "ACL2-USER", "COMMON-LISP"), 965("BIT", "ACL2-USER", "COMMON-LISP"), 966("BUILT-IN-CLASS", "ACL2-USER", "COMMON-LISP"), 967("ALPHANUMERICP", "ACL2-USER", "COMMON-LISP"), 968("BIT-AND", "ACL2-USER", "COMMON-LISP"), 969("BUTLAST", "ACL2-USER", "COMMON-LISP"), 970("AND", "ACL2-USER", "COMMON-LISP"), 971("BIT-ANDC1", "ACL2-USER", "COMMON-LISP"), 972("BYTE", "ACL2-USER", "COMMON-LISP"), 973("APPEND", "ACL2-USER", "COMMON-LISP"), 974("BIT-ANDC2", "ACL2-USER", "COMMON-LISP"), 975("BYTE-POSITION", "ACL2-USER", "COMMON-LISP"), 976("APPLY", "ACL2-USER", "COMMON-LISP"), 977("BIT-EQV", "ACL2-USER", "COMMON-LISP"), 978("BYTE-SIZE", "ACL2-USER", "COMMON-LISP"), 979("APROPOS", "ACL2-USER", "COMMON-LISP"), 980("BIT-IOR", "ACL2-USER", "COMMON-LISP"), 981("CAAAAR", "ACL2-USER", "COMMON-LISP"), 982("APROPOS-LIST", "ACL2-USER", "COMMON-LISP"), 983("BIT-NAND", "ACL2-USER", "COMMON-LISP"), 984("CAAADR", "ACL2-USER", "COMMON-LISP"), 985("AREF", "ACL2-USER", "COMMON-LISP"), 986("BIT-NOR", "ACL2-USER", "COMMON-LISP"), 987("CAAAR", "ACL2-USER", "COMMON-LISP"), 988("ARITHMETIC-ERROR", "ACL2-USER", "COMMON-LISP"), 989("BIT-NOT", "ACL2-USER", "COMMON-LISP"), 990("CAADAR", "ACL2-USER", "COMMON-LISP"), 991("ARITHMETIC-ERROR-OPERANDS", "ACL2-USER", "COMMON-LISP"), 992("BIT-ORC1", "ACL2-USER", "COMMON-LISP"), 993("CAADDR", "ACL2-USER", "COMMON-LISP"), 994("ARITHMETIC-ERROR-OPERATION", "ACL2-USER", "COMMON-LISP"), 995("BIT-ORC2", "ACL2-USER", "COMMON-LISP"), 996("CAADR", "ACL2-USER", "COMMON-LISP"), 997("ARRAY", "ACL2-USER", "COMMON-LISP"), 998("BIT-VECTOR", "ACL2-USER", "COMMON-LISP"), 999("CAAR", "ACL2-USER", "COMMON-LISP"), 1000("ARRAY-DIMENSION", "ACL2-USER", "COMMON-LISP"), 1001("BIT-VECTOR-P", "ACL2-USER", "COMMON-LISP"), 1002("CADAAR", "ACL2-USER", "COMMON-LISP"), 1003("ARRAY-DIMENSION-LIMIT", "ACL2-USER", "COMMON-LISP"), 1004("BIT-XOR", "ACL2-USER", "COMMON-LISP"), 1005("CADADR", "ACL2-USER", "COMMON-LISP"), 1006("ARRAY-DIMENSIONS", "ACL2-USER", "COMMON-LISP"), 1007("BLOCK", "ACL2-USER", "COMMON-LISP"), 1008("CADAR", "ACL2-USER", "COMMON-LISP"), 1009("ARRAY-DISPLACEMENT", "ACL2-USER", "COMMON-LISP"), 1010("BOOLE", "ACL2-USER", "COMMON-LISP"), 1011("CADDAR", "ACL2-USER", "COMMON-LISP"), 1012("ARRAY-ELEMENT-TYPE", "ACL2-USER", "COMMON-LISP"), 1013("BOOLE-1", "ACL2-USER", "COMMON-LISP"), 1014("CADDDR", "ACL2-USER", "COMMON-LISP"), 1015("ARRAY-HAS-FILL-POINTER-P", "ACL2-USER", "COMMON-LISP"), 1016("BOOLE-2", "ACL2-USER", "COMMON-LISP"), 1017("CADDR", "ACL2-USER", "COMMON-LISP"), 1018("ARRAY-IN-BOUNDS-P", "ACL2-USER", "COMMON-LISP"), 1019("BOOLE-AND", "ACL2-USER", "COMMON-LISP"), 1020("CADR", "ACL2-USER", "COMMON-LISP"), 1021("ARRAY-RANK", "ACL2-USER", "COMMON-LISP"), 1022("BOOLE-ANDC1", "ACL2-USER", "COMMON-LISP"), 1023("CALL-ARGUMENTS-LIMIT", "ACL2-USER", "COMMON-LISP"), 1024("ARRAY-RANK-LIMIT", "ACL2-USER", "COMMON-LISP"), 1025("BOOLE-ANDC2", "ACL2-USER", "COMMON-LISP"), 1026("CALL-METHOD", "ACL2-USER", "COMMON-LISP"), 1027("ARRAY-ROW-MAJOR-INDEX", "ACL2-USER", "COMMON-LISP"), 1028("BOOLE-C1", "ACL2-USER", "COMMON-LISP"), 1029("CALL-NEXT-METHOD", "ACL2-USER", "COMMON-LISP"), 1030("ARRAY-TOTAL-SIZE", "ACL2-USER", "COMMON-LISP"), 1031("BOOLE-C2", "ACL2-USER", "COMMON-LISP"), 1032("CAR", "ACL2-USER", "COMMON-LISP"), 1033("ARRAY-TOTAL-SIZE-LIMIT", "ACL2-USER", "COMMON-LISP"), 1034("BOOLE-CLR", "ACL2-USER", "COMMON-LISP"), 1035("CASE", "ACL2-USER", "COMMON-LISP"), 1036("ARRAYP", "ACL2-USER", "COMMON-LISP"), 1037("BOOLE-EQV", "ACL2-USER", "COMMON-LISP"), 1038("CATCH", "ACL2-USER", "COMMON-LISP"), 1039("ASH", "ACL2-USER", "COMMON-LISP"), 1040("BOOLE-IOR", "ACL2-USER", "COMMON-LISP"), 1041("CCASE", "ACL2-USER", "COMMON-LISP"), 1042("ASIN", "ACL2-USER", "COMMON-LISP"), 1043("BOOLE-NAND", "ACL2-USER", "COMMON-LISP"), 1044("CDAAAR", "ACL2-USER", "COMMON-LISP"), 1045("ASINH", "ACL2-USER", "COMMON-LISP"), 1046("BOOLE-NOR", "ACL2-USER", "COMMON-LISP"), 1047("CDAADR", "ACL2-USER", "COMMON-LISP"), 1048("ASSERT", "ACL2-USER", "COMMON-LISP"), 1049("BOOLE-ORC1", "ACL2-USER", "COMMON-LISP"), 1050("CDAAR", "ACL2-USER", "COMMON-LISP"), 1051("ASSOC", "ACL2-USER", "COMMON-LISP"), 1052("BOOLE-ORC2", "ACL2-USER", "COMMON-LISP"), 1053("CDADAR", "ACL2-USER", "COMMON-LISP"), 1054("ASSOC-IF", "ACL2-USER", "COMMON-LISP"), 1055("BOOLE-SET", "ACL2-USER", "COMMON-LISP"), 1056("CDADDR", "ACL2-USER", "COMMON-LISP"), 1057("ASSOC-IF-NOT", "ACL2-USER", "COMMON-LISP"), 1058("BOOLE-XOR", "ACL2-USER", "COMMON-LISP"), 1059("CDADR", "ACL2-USER", "COMMON-LISP"), 1060("ATAN", "ACL2-USER", "COMMON-LISP"), 1061("BOOLEAN", "ACL2-USER", "COMMON-LISP"), 1062("CDAR", "ACL2-USER", "COMMON-LISP"), 1063("ATANH", "ACL2-USER", "COMMON-LISP"), 1064("BOTH-CASE-P", "ACL2-USER", "COMMON-LISP"), 1065("CDDAAR", "ACL2-USER", "COMMON-LISP"), 1066("CDDADR", "ACL2-USER", "COMMON-LISP"), 1067("CLEAR-INPUT", "ACL2-USER", "COMMON-LISP"), 1068("COPY-TREE", "ACL2-USER", "COMMON-LISP"), 1069("CDDAR", "ACL2-USER", "COMMON-LISP"), 1070("CLEAR-OUTPUT", "ACL2-USER", "COMMON-LISP"), 1071("COS", "ACL2-USER", "COMMON-LISP"), 1072("CDDDAR", "ACL2-USER", "COMMON-LISP"), 1073("CLOSE", "ACL2-USER", "COMMON-LISP"), 1074("COSH", "ACL2-USER", "COMMON-LISP"), 1075("CDDDDR", "ACL2-USER", "COMMON-LISP"), 1076("CLRHASH", "ACL2-USER", "COMMON-LISP"), 1077("COUNT", "ACL2-USER", "COMMON-LISP"), 1078("CDDDR", "ACL2-USER", "COMMON-LISP"), 1079("CODE-CHAR", "ACL2-USER", "COMMON-LISP"), 1080("COUNT-IF", "ACL2-USER", "COMMON-LISP"), 1081("CDDR", "ACL2-USER", "COMMON-LISP"), 1082("COERCE", "ACL2-USER", "COMMON-LISP"), 1083("COUNT-IF-NOT", "ACL2-USER", "COMMON-LISP"), 1084("CDR", "ACL2-USER", "COMMON-LISP"), 1085("COMPILATION-SPEED", "ACL2-USER", "COMMON-LISP"), 1086("CTYPECASE", "ACL2-USER", "COMMON-LISP"), 1087("CEILING", "ACL2-USER", "COMMON-LISP"), 1088("COMPILE", "ACL2-USER", "COMMON-LISP"), 1089("DEBUG", "ACL2-USER", "COMMON-LISP"), 1090("CELL-ERROR", "ACL2-USER", "COMMON-LISP"), 1091("COMPILE-FILE", "ACL2-USER", "COMMON-LISP"), 1092("DECF", "ACL2-USER", "COMMON-LISP"), 1093("CELL-ERROR-NAME", "ACL2-USER", "COMMON-LISP"), 1094("COMPILE-FILE-PATHNAME", "ACL2-USER", "COMMON-LISP"), 1095("DECLAIM", "ACL2-USER", "COMMON-LISP"), 1096("CERROR", "ACL2-USER", "COMMON-LISP"), 1097("COMPILED-FUNCTION", "ACL2-USER", "COMMON-LISP"), 1098("DECLARATION", "ACL2-USER", "COMMON-LISP"), 1099("CHANGE-CLASS", "ACL2-USER", "COMMON-LISP"), 1100("COMPILED-FUNCTION-P", "ACL2-USER", "COMMON-LISP"), 1101("DECLARE", "ACL2-USER", "COMMON-LISP"), 1102("CHAR", "ACL2-USER", "COMMON-LISP"), 1103("COMPILER-MACRO", "ACL2-USER", "COMMON-LISP"), 1104("DECODE-FLOAT", "ACL2-USER", "COMMON-LISP"), 1105("CHAR-CODE", "ACL2-USER", "COMMON-LISP"), 1106("COMPILER-MACRO-FUNCTION", "ACL2-USER", "COMMON-LISP"), 1107("DECODE-UNIVERSAL-TIME", "ACL2-USER", "COMMON-LISP"), 1108("CHAR-CODE-LIMIT", "ACL2-USER", "COMMON-LISP"), 1109("COMPLEMENT", "ACL2-USER", "COMMON-LISP"), 1110("DEFCLASS", "ACL2-USER", "COMMON-LISP"), 1111("CHAR-DOWNCASE", "ACL2-USER", "COMMON-LISP"), 1112("COMPLEX", "ACL2-USER", "COMMON-LISP"), 1113("DEFCONSTANT", "ACL2-USER", "COMMON-LISP"), 1114("CHAR-EQUAL", "ACL2-USER", "COMMON-LISP"), 1115("COMPLEXP", "ACL2-USER", "COMMON-LISP"), 1116("DEFGENERIC", "ACL2-USER", "COMMON-LISP"), 1117("CHAR-GREATERP", "ACL2-USER", "COMMON-LISP"), 1118("COMPUTE-APPLICABLE-METHODS", "ACL2-USER", "COMMON-LISP"), 1119("DEFINE-COMPILER-MACRO", "ACL2-USER", "COMMON-LISP"), 1120("CHAR-INT", "ACL2-USER", "COMMON-LISP"), 1121("COMPUTE-RESTARTS", "ACL2-USER", "COMMON-LISP"), 1122("DEFINE-CONDITION", "ACL2-USER", "COMMON-LISP"), 1123("CHAR-LESSP", "ACL2-USER", "COMMON-LISP"), 1124("CONCATENATE", "ACL2-USER", "COMMON-LISP"), 1125("DEFINE-METHOD-COMBINATION", "ACL2-USER", "COMMON-LISP"), 1126("CHAR-NAME", "ACL2-USER", "COMMON-LISP"), 1127("CONCATENATED-STREAM", "ACL2-USER", "COMMON-LISP"), 1128("DEFINE-MODIFY-MACRO", "ACL2-USER", "COMMON-LISP"), 1129("CHAR-NOT-EQUAL", "ACL2-USER", "COMMON-LISP"), 1130("CONCATENATED-STREAM-STREAMS", "ACL2-USER", "COMMON-LISP"), 1131("DEFINE-SETF-EXPANDER", "ACL2-USER", "COMMON-LISP"), 1132("CHAR-NOT-GREATERP", "ACL2-USER", "COMMON-LISP"), 1133("COND", "ACL2-USER", "COMMON-LISP"), 1134("DEFINE-SYMBOL-MACRO", "ACL2-USER", "COMMON-LISP"), 1135("CHAR-NOT-LESSP", "ACL2-USER", "COMMON-LISP"), 1136("CONDITION", "ACL2-USER", "COMMON-LISP"), 1137("DEFMACRO", "ACL2-USER", "COMMON-LISP"), 1138("CHAR-UPCASE", "ACL2-USER", "COMMON-LISP"), 1139("CONJUGATE", "ACL2-USER", "COMMON-LISP"), 1140("DEFMETHOD", "ACL2-USER", "COMMON-LISP"), 1141("CHAR/=", "ACL2-USER", "COMMON-LISP"), 1142("CONS", "ACL2-USER", "COMMON-LISP"), 1143("DEFPACKAGE", "ACL2-USER", "COMMON-LISP"), 1144("CHAR<", "ACL2-USER", "COMMON-LISP"), 1145("CONSP", "ACL2-USER", "COMMON-LISP"), 1146("DEFPARAMETER", "ACL2-USER", "COMMON-LISP"), 1147("CHAR<=", "ACL2-USER", "COMMON-LISP"), 1148("CONSTANTLY", "ACL2-USER", "COMMON-LISP"), 1149("DEFSETF", "ACL2-USER", "COMMON-LISP"), 1150("CHAR=", "ACL2-USER", "COMMON-LISP"), 1151("CONSTANTP", "ACL2-USER", "COMMON-LISP"), 1152("DEFSTRUCT", "ACL2-USER", "COMMON-LISP"), 1153("CHAR>", "ACL2-USER", "COMMON-LISP"), 1154("CONTINUE", "ACL2-USER", "COMMON-LISP"), 1155("DEFTYPE", "ACL2-USER", "COMMON-LISP"), 1156("CHAR>=", "ACL2-USER", "COMMON-LISP"), 1157("CONTROL-ERROR", "ACL2-USER", "COMMON-LISP"), 1158("DEFUN", "ACL2-USER", "COMMON-LISP"), 1159("CHARACTER", "ACL2-USER", "COMMON-LISP"), 1160("COPY-ALIST", "ACL2-USER", "COMMON-LISP"), 1161("DEFVAR", "ACL2-USER", "COMMON-LISP"), 1162("CHARACTERP", "ACL2-USER", "COMMON-LISP"), 1163("COPY-LIST", "ACL2-USER", "COMMON-LISP"), 1164("DELETE", "ACL2-USER", "COMMON-LISP"), 1165("CHECK-TYPE", "ACL2-USER", "COMMON-LISP"), 1166("COPY-PPRINT-DISPATCH", "ACL2-USER", "COMMON-LISP"), 1167("DELETE-DUPLICATES", "ACL2-USER", "COMMON-LISP"), 1168("CIS", "ACL2-USER", "COMMON-LISP"), 1169("COPY-READTABLE", "ACL2-USER", "COMMON-LISP"), 1170("DELETE-FILE", "ACL2-USER", "COMMON-LISP"), 1171("CLASS", "ACL2-USER", "COMMON-LISP"), 1172("COPY-SEQ", "ACL2-USER", "COMMON-LISP"), 1173("DELETE-IF", "ACL2-USER", "COMMON-LISP"), 1174("CLASS-NAME", "ACL2-USER", "COMMON-LISP"), 1175("COPY-STRUCTURE", "ACL2-USER", "COMMON-LISP"), 1176("DELETE-IF-NOT", "ACL2-USER", "COMMON-LISP"), 1177("CLASS-OF", "ACL2-USER", "COMMON-LISP"), 1178("COPY-SYMBOL", "ACL2-USER", "COMMON-LISP"), 1179("DELETE-PACKAGE", "ACL2-USER", "COMMON-LISP"), 1180("DENOMINATOR", "ACL2-USER", "COMMON-LISP"), 1181("EQ", "ACL2-USER", "COMMON-LISP"), 1182("DEPOSIT-FIELD", "ACL2-USER", "COMMON-LISP"), 1183("EQL", "ACL2-USER", "COMMON-LISP"), 1184("DESCRIBE", "ACL2-USER", "COMMON-LISP"), 1185("EQUAL", "ACL2-USER", "COMMON-LISP"), 1186("DESCRIBE-OBJECT", "ACL2-USER", "COMMON-LISP"), 1187("EQUALP", "ACL2-USER", "COMMON-LISP"), 1188("DESTRUCTURING-BIND", "ACL2-USER", "COMMON-LISP"), 1189("ERROR", "ACL2-USER", "COMMON-LISP"), 1190("DIGIT-CHAR", "ACL2-USER", "COMMON-LISP"), 1191("ETYPECASE", "ACL2-USER", "COMMON-LISP"), 1192("DIGIT-CHAR-P", "ACL2-USER", "COMMON-LISP"), 1193("EVAL", "ACL2-USER", "COMMON-LISP"), 1194("DIRECTORY", "ACL2-USER", "COMMON-LISP"), 1195("EVAL-WHEN", "ACL2-USER", "COMMON-LISP"), 1196("DIRECTORY-NAMESTRING", "ACL2-USER", "COMMON-LISP"), 1197("EVENP", "ACL2-USER", "COMMON-LISP"), 1198("DISASSEMBLE", "ACL2-USER", "COMMON-LISP"), 1199("EVERY", "ACL2-USER", "COMMON-LISP"), 1200("DIVISION-BY-ZERO", "ACL2-USER", "COMMON-LISP"), 1201("EXP", "ACL2-USER", "COMMON-LISP"), 1202("DO", "ACL2-USER", "COMMON-LISP"), 1203("EXPORT", "ACL2-USER", "COMMON-LISP"), 1204("DO*", "ACL2-USER", "COMMON-LISP"), 1205("EXPT", "ACL2-USER", "COMMON-LISP"), 1206("DO-ALL-SYMBOLS", "ACL2-USER", "COMMON-LISP"), 1207("EXTENDED-CHAR", "ACL2-USER", "COMMON-LISP"), 1208("DO-EXTERNAL-SYMBOLS", "ACL2-USER", "COMMON-LISP"), 1209("FBOUNDP", "ACL2-USER", "COMMON-LISP"), 1210("DO-SYMBOLS", "ACL2-USER", "COMMON-LISP"), 1211("FCEILING", "ACL2-USER", "COMMON-LISP"), 1212("DOCUMENTATION", "ACL2-USER", "COMMON-LISP"), 1213("FDEFINITION", "ACL2-USER", "COMMON-LISP"), 1214("DOLIST", "ACL2-USER", "COMMON-LISP"), 1215("FFLOOR", "ACL2-USER", "COMMON-LISP"), 1216("DOTIMES", "ACL2-USER", "COMMON-LISP"), 1217("FIFTH", "ACL2-USER", "COMMON-LISP"), 1218("DOUBLE-FLOAT", "ACL2-USER", "COMMON-LISP"), 1219("FILE-AUTHOR", "ACL2-USER", "COMMON-LISP"), 1220("DOUBLE-FLOAT-EPSILON", "ACL2-USER", "COMMON-LISP"), 1221("FILE-ERROR", "ACL2-USER", "COMMON-LISP"), 1222("DOUBLE-FLOAT-NEGATIVE-EPSILON", "ACL2-USER", "COMMON-LISP"), 1223("FILE-ERROR-PATHNAME", "ACL2-USER", "COMMON-LISP"), 1224("DPB", "ACL2-USER", "COMMON-LISP"), 1225("FILE-LENGTH", "ACL2-USER", "COMMON-LISP"), 1226("DRIBBLE", "ACL2-USER", "COMMON-LISP"), 1227("FILE-NAMESTRING", "ACL2-USER", "COMMON-LISP"), 1228("DYNAMIC-EXTENT", "ACL2-USER", "COMMON-LISP"), 1229("FILE-POSITION", "ACL2-USER", "COMMON-LISP"), 1230("ECASE", "ACL2-USER", "COMMON-LISP"), 1231("FILE-STREAM", "ACL2-USER", "COMMON-LISP"), 1232("ECHO-STREAM", "ACL2-USER", "COMMON-LISP"), 1233("FILE-STRING-LENGTH", "ACL2-USER", "COMMON-LISP"), 1234("ECHO-STREAM-INPUT-STREAM", "ACL2-USER", "COMMON-LISP"), 1235("FILE-WRITE-DATE", "ACL2-USER", "COMMON-LISP"), 1236("ECHO-STREAM-OUTPUT-STREAM", "ACL2-USER", "COMMON-LISP"), 1237("FILL", "ACL2-USER", "COMMON-LISP"), 1238("ED", "ACL2-USER", "COMMON-LISP"), 1239("FILL-POINTER", "ACL2-USER", "COMMON-LISP"), 1240("EIGHTH", "ACL2-USER", "COMMON-LISP"), 1241("FIND", "ACL2-USER", "COMMON-LISP"), 1242("ELT", "ACL2-USER", "COMMON-LISP"), 1243("FIND-ALL-SYMBOLS", "ACL2-USER", "COMMON-LISP"), 1244("ENCODE-UNIVERSAL-TIME", "ACL2-USER", "COMMON-LISP"), 1245("FIND-CLASS", "ACL2-USER", "COMMON-LISP"), 1246("END-OF-FILE", "ACL2-USER", "COMMON-LISP"), 1247("FIND-IF", "ACL2-USER", "COMMON-LISP"), 1248("ENDP", "ACL2-USER", "COMMON-LISP"), 1249("FIND-IF-NOT", "ACL2-USER", "COMMON-LISP"), 1250("ENOUGH-NAMESTRING", "ACL2-USER", "COMMON-LISP"), 1251("FIND-METHOD", "ACL2-USER", "COMMON-LISP"), 1252("ENSURE-DIRECTORIES-EXIST", "ACL2-USER", "COMMON-LISP"), 1253("FIND-PACKAGE", "ACL2-USER", "COMMON-LISP"), 1254("ENSURE-GENERIC-FUNCTION", "ACL2-USER", "COMMON-LISP"), 1255("FIND-RESTART", "ACL2-USER", "COMMON-LISP"), 1256("FIND-SYMBOL", "ACL2-USER", "COMMON-LISP"), 1257("GET-INTERNAL-RUN-TIME", "ACL2-USER", "COMMON-LISP"), 1258("FINISH-OUTPUT", "ACL2-USER", "COMMON-LISP"), 1259("GET-MACRO-CHARACTER", "ACL2-USER", "COMMON-LISP"), 1260("FIRST", "ACL2-USER", "COMMON-LISP"), 1261("GET-OUTPUT-STREAM-STRING", "ACL2-USER", "COMMON-LISP"), 1262("FIXNUM", "ACL2-USER", "COMMON-LISP"), 1263("GET-PROPERTIES", "ACL2-USER", "COMMON-LISP"), 1264("FLET", "ACL2-USER", "COMMON-LISP"), 1265("GET-SETF-EXPANSION", "ACL2-USER", "COMMON-LISP"), 1266("FLOAT", "ACL2-USER", "COMMON-LISP"), 1267("GET-UNIVERSAL-TIME", "ACL2-USER", "COMMON-LISP"), 1268("FLOAT-DIGITS", "ACL2-USER", "COMMON-LISP"), 1269("GETF", "ACL2-USER", "COMMON-LISP"), 1270("FLOAT-PRECISION", "ACL2-USER", "COMMON-LISP"), 1271("GETHASH", "ACL2-USER", "COMMON-LISP"), 1272("FLOAT-RADIX", "ACL2-USER", "COMMON-LISP"), 1273("GO", "ACL2-USER", "COMMON-LISP"), 1274("FLOAT-SIGN", "ACL2-USER", "COMMON-LISP"), 1275("GRAPHIC-CHAR-P", "ACL2-USER", "COMMON-LISP"), 1276("FLOATING-POINT-INEXACT", "ACL2-USER", "COMMON-LISP"), 1277("HANDLER-BIND", "ACL2-USER", "COMMON-LISP"), 1278("FLOATING-POINT-INVALID-OPERATION", "ACL2-USER", "COMMON-LISP"), 1279("HANDLER-CASE", "ACL2-USER", "COMMON-LISP"), 1280("FLOATING-POINT-OVERFLOW", "ACL2-USER", "COMMON-LISP"), 1281("HASH-TABLE", "ACL2-USER", "COMMON-LISP"), 1282("FLOATING-POINT-UNDERFLOW", "ACL2-USER", "COMMON-LISP"), 1283("HASH-TABLE-COUNT", "ACL2-USER", "COMMON-LISP"), 1284("FLOATP", "ACL2-USER", "COMMON-LISP"), 1285("HASH-TABLE-P", "ACL2-USER", "COMMON-LISP"), 1286("FLOOR", "ACL2-USER", "COMMON-LISP"), 1287("HASH-TABLE-REHASH-SIZE", "ACL2-USER", "COMMON-LISP"), 1288("FMAKUNBOUND", "ACL2-USER", "COMMON-LISP"), 1289("HASH-TABLE-REHASH-THRESHOLD", "ACL2-USER", "COMMON-LISP"), 1290("FORCE-OUTPUT", "ACL2-USER", "COMMON-LISP"), 1291("HASH-TABLE-SIZE", "ACL2-USER", "COMMON-LISP"), 1292("FORMAT", "ACL2-USER", "COMMON-LISP"), 1293("HASH-TABLE-TEST", "ACL2-USER", "COMMON-LISP"), 1294("FORMATTER", "ACL2-USER", "COMMON-LISP"), 1295("HOST-NAMESTRING", "ACL2-USER", "COMMON-LISP"), 1296("FOURTH", "ACL2-USER", "COMMON-LISP"), 1297("IDENTITY", "ACL2-USER", "COMMON-LISP"), 1298("FRESH-LINE", "ACL2-USER", "COMMON-LISP"), 1299("IF", "ACL2-USER", "COMMON-LISP"), 1300("FROUND", "ACL2-USER", "COMMON-LISP"), 1301("IGNORABLE", "ACL2-USER", "COMMON-LISP"), 1302("FTRUNCATE", "ACL2-USER", "COMMON-LISP"), 1303("IGNORE", "ACL2-USER", "COMMON-LISP"), 1304("FTYPE", "ACL2-USER", "COMMON-LISP"), 1305("IGNORE-ERRORS", "ACL2-USER", "COMMON-LISP"), 1306("FUNCALL", "ACL2-USER", "COMMON-LISP"), 1307("IMAGPART", "ACL2-USER", "COMMON-LISP"), 1308("FUNCTION", "ACL2-USER", "COMMON-LISP"), 1309("IMPORT", "ACL2-USER", "COMMON-LISP"), 1310("FUNCTION-KEYWORDS", "ACL2-USER", "COMMON-LISP"), 1311("IN-PACKAGE", "ACL2-USER", "COMMON-LISP"), 1312("FUNCTION-LAMBDA-EXPRESSION", "ACL2-USER", "COMMON-LISP"), 1313("INCF", "ACL2-USER", "COMMON-LISP"), 1314("FUNCTIONP", "ACL2-USER", "COMMON-LISP"), 1315("INITIALIZE-INSTANCE", "ACL2-USER", "COMMON-LISP"), 1316("GCD", "ACL2-USER", "COMMON-LISP"), 1317("INLINE", "ACL2-USER", "COMMON-LISP"), 1318("GENERIC-FUNCTION", "ACL2-USER", "COMMON-LISP"), 1319("INPUT-STREAM-P", "ACL2-USER", "COMMON-LISP"), 1320("GENSYM", "ACL2-USER", "COMMON-LISP"), 1321("INSPECT", "ACL2-USER", "COMMON-LISP"), 1322("GENTEMP", "ACL2-USER", "COMMON-LISP"), 1323("INTEGER", "ACL2-USER", "COMMON-LISP"), 1324("GET", "ACL2-USER", "COMMON-LISP"), 1325("INTEGER-DECODE-FLOAT", "ACL2-USER", "COMMON-LISP"), 1326("GET-DECODED-TIME", "ACL2-USER", "COMMON-LISP"), 1327("INTEGER-LENGTH", "ACL2-USER", "COMMON-LISP"), 1328("GET-DISPATCH-MACRO-CHARACTER", "ACL2-USER", "COMMON-LISP"), 1329("INTEGERP", "ACL2-USER", "COMMON-LISP"), 1330("GET-INTERNAL-REAL-TIME", "ACL2-USER", "COMMON-LISP"), 1331("INTERACTIVE-STREAM-P", "ACL2-USER", "COMMON-LISP"), 1332("INTERN", "ACL2-USER", "COMMON-LISP"), 1333("LISP-IMPLEMENTATION-TYPE", "ACL2-USER", "COMMON-LISP"), 1334("INTERNAL-TIME-UNITS-PER-SECOND", "ACL2-USER", "COMMON-LISP"), 1335("LISP-IMPLEMENTATION-VERSION", "ACL2-USER", "COMMON-LISP"), 1336("INTERSECTION", "ACL2-USER", "COMMON-LISP"), 1337("LIST", "ACL2-USER", "COMMON-LISP"), 1338("INVALID-METHOD-ERROR", "ACL2-USER", "COMMON-LISP"), 1339("LIST*", "ACL2-USER", "COMMON-LISP"), 1340("INVOKE-DEBUGGER", "ACL2-USER", "COMMON-LISP"), 1341("LIST-ALL-PACKAGES", "ACL2-USER", "COMMON-LISP"), 1342("INVOKE-RESTART", "ACL2-USER", "COMMON-LISP"), 1343("LIST-LENGTH", "ACL2-USER", "COMMON-LISP"), 1344("INVOKE-RESTART-INTERACTIVELY", "ACL2-USER", "COMMON-LISP"), 1345("LISTEN", "ACL2-USER", "COMMON-LISP"), 1346("ISQRT", "ACL2-USER", "COMMON-LISP"), 1347("LISTP", "ACL2-USER", "COMMON-LISP"), 1348("KEYWORD", "ACL2-USER", "COMMON-LISP"), 1349("LOAD", "ACL2-USER", "COMMON-LISP"), 1350("KEYWORDP", "ACL2-USER", "COMMON-LISP"), 1351("LOAD-LOGICAL-PATHNAME-TRANSLATIONS", "ACL2-USER", "COMMON-LISP"), 1352("LABELS", "ACL2-USER", "COMMON-LISP"), 1353("LOAD-TIME-VALUE", "ACL2-USER", "COMMON-LISP"), 1354("LAMBDA", "ACL2-USER", "COMMON-LISP"), 1355("LOCALLY", "ACL2-USER", "COMMON-LISP"), 1356("LAMBDA-LIST-KEYWORDS", "ACL2-USER", "COMMON-LISP"), 1357("LOG", "ACL2-USER", "COMMON-LISP"), 1358("LAMBDA-PARAMETERS-LIMIT", "ACL2-USER", "COMMON-LISP"), 1359("LOGAND", "ACL2-USER", "COMMON-LISP"), 1360("LAST", "ACL2-USER", "COMMON-LISP"), 1361("LOGANDC1", "ACL2-USER", "COMMON-LISP"), 1362("LCM", "ACL2-USER", "COMMON-LISP"), 1363("LOGANDC2", "ACL2-USER", "COMMON-LISP"), 1364("LDB", "ACL2-USER", "COMMON-LISP"), 1365("LOGBITP", "ACL2-USER", "COMMON-LISP"), 1366("LDB-TEST", "ACL2-USER", "COMMON-LISP"), 1367("LOGCOUNT", "ACL2-USER", "COMMON-LISP"), 1368("LDIFF", "ACL2-USER", "COMMON-LISP"), 1369("LOGEQV", "ACL2-USER", "COMMON-LISP"), 1370("LEAST-NEGATIVE-DOUBLE-FLOAT", "ACL2-USER", "COMMON-LISP"), 1371("LOGICAL-PATHNAME", "ACL2-USER", "COMMON-LISP"), 1372("LEAST-NEGATIVE-LONG-FLOAT", "ACL2-USER", "COMMON-LISP"), 1373("LOGICAL-PATHNAME-TRANSLATIONS", "ACL2-USER", "COMMON-LISP"), 1374("LEAST-NEGATIVE-NORMALIZED-DOUBLE-FLOAT", "ACL2-USER", "COMMON-LISP"), 1375("LOGIOR", "ACL2-USER", "COMMON-LISP"), 1376("LEAST-NEGATIVE-NORMALIZED-LONG-FLOAT", "ACL2-USER", "COMMON-LISP"), 1377("LOGNAND", "ACL2-USER", "COMMON-LISP"), 1378("LEAST-NEGATIVE-NORMALIZED-SHORT-FLOAT", "ACL2-USER", "COMMON-LISP"), 1379("LOGNOR", "ACL2-USER", "COMMON-LISP"), 1380("LEAST-NEGATIVE-NORMALIZED-SINGLE-FLOAT", "ACL2-USER", "COMMON-LISP"), 1381("LOGNOT", "ACL2-USER", "COMMON-LISP"), 1382("LEAST-NEGATIVE-SHORT-FLOAT", "ACL2-USER", "COMMON-LISP"), 1383("LOGORC1", "ACL2-USER", "COMMON-LISP"), 1384("LEAST-NEGATIVE-SINGLE-FLOAT", "ACL2-USER", "COMMON-LISP"), 1385("LOGORC2", "ACL2-USER", "COMMON-LISP"), 1386("LEAST-POSITIVE-DOUBLE-FLOAT", "ACL2-USER", "COMMON-LISP"), 1387("LOGTEST", "ACL2-USER", "COMMON-LISP"), 1388("LEAST-POSITIVE-LONG-FLOAT", "ACL2-USER", "COMMON-LISP"), 1389("LOGXOR", "ACL2-USER", "COMMON-LISP"), 1390("LEAST-POSITIVE-NORMALIZED-DOUBLE-FLOAT", "ACL2-USER", "COMMON-LISP"), 1391("LONG-FLOAT", "ACL2-USER", "COMMON-LISP"), 1392("LEAST-POSITIVE-NORMALIZED-LONG-FLOAT", "ACL2-USER", "COMMON-LISP"), 1393("LONG-FLOAT-EPSILON", "ACL2-USER", "COMMON-LISP"), 1394("LEAST-POSITIVE-NORMALIZED-SHORT-FLOAT", "ACL2-USER", "COMMON-LISP"), 1395("LONG-FLOAT-NEGATIVE-EPSILON", "ACL2-USER", "COMMON-LISP"), 1396("LEAST-POSITIVE-NORMALIZED-SINGLE-FLOAT", "ACL2-USER", "COMMON-LISP"), 1397("LONG-SITE-NAME", "ACL2-USER", "COMMON-LISP"), 1398("LEAST-POSITIVE-SHORT-FLOAT", "ACL2-USER", "COMMON-LISP"), 1399("LOOP", "ACL2-USER", "COMMON-LISP"), 1400("LEAST-POSITIVE-SINGLE-FLOAT", "ACL2-USER", "COMMON-LISP"), 1401("LOOP-FINISH", "ACL2-USER", "COMMON-LISP"), 1402("LENGTH", "ACL2-USER", "COMMON-LISP"), 1403("LOWER-CASE-P", "ACL2-USER", "COMMON-LISP"), 1404("LET", "ACL2-USER", "COMMON-LISP"), 1405("MACHINE-INSTANCE", "ACL2-USER", "COMMON-LISP"), 1406("LET*", "ACL2-USER", "COMMON-LISP"), 1407("MACHINE-TYPE", "ACL2-USER", "COMMON-LISP"), 1408("MACHINE-VERSION", "ACL2-USER", "COMMON-LISP"), 1409("MASK-FIELD", "ACL2-USER", "COMMON-LISP"), 1410("MACRO-FUNCTION", "ACL2-USER", "COMMON-LISP"), 1411("MAX", "ACL2-USER", "COMMON-LISP"), 1412("MACROEXPAND", "ACL2-USER", "COMMON-LISP"), 1413("MEMBER", "ACL2-USER", "COMMON-LISP"), 1414("MACROEXPAND-1", "ACL2-USER", "COMMON-LISP"), 1415("MEMBER-IF", "ACL2-USER", "COMMON-LISP"), 1416("MACROLET", "ACL2-USER", "COMMON-LISP"), 1417("MEMBER-IF-NOT", "ACL2-USER", "COMMON-LISP"), 1418("MAKE-ARRAY", "ACL2-USER", "COMMON-LISP"), 1419("MERGE", "ACL2-USER", "COMMON-LISP"), 1420("MAKE-BROADCAST-STREAM", "ACL2-USER", "COMMON-LISP"), 1421("MERGE-PATHNAMES", "ACL2-USER", "COMMON-LISP"), 1422("MAKE-CONCATENATED-STREAM", "ACL2-USER", "COMMON-LISP"), 1423("METHOD", "ACL2-USER", "COMMON-LISP"), 1424("MAKE-CONDITION", "ACL2-USER", "COMMON-LISP"), 1425("METHOD-COMBINATION", "ACL2-USER", "COMMON-LISP"), 1426("MAKE-DISPATCH-MACRO-CHARACTER", "ACL2-USER", "COMMON-LISP"), 1427("METHOD-COMBINATION-ERROR", "ACL2-USER", "COMMON-LISP"), 1428("MAKE-ECHO-STREAM", "ACL2-USER", "COMMON-LISP"), 1429("METHOD-QUALIFIERS", "ACL2-USER", "COMMON-LISP"), 1430("MAKE-HASH-TABLE", "ACL2-USER", "COMMON-LISP"), 1431("MIN", "ACL2-USER", "COMMON-LISP"), 1432("MAKE-INSTANCE", "ACL2-USER", "COMMON-LISP"), 1433("MINUSP", "ACL2-USER", "COMMON-LISP"), 1434("MAKE-INSTANCES-OBSOLETE", "ACL2-USER", "COMMON-LISP"), 1435("MISMATCH", "ACL2-USER", "COMMON-LISP"), 1436("MAKE-LIST", "ACL2-USER", "COMMON-LISP"), 1437("MOD", "ACL2-USER", "COMMON-LISP"), 1438("MAKE-LOAD-FORM", "ACL2-USER", "COMMON-LISP"), 1439("MOST-NEGATIVE-DOUBLE-FLOAT", "ACL2-USER", "COMMON-LISP"), 1440("MAKE-LOAD-FORM-SAVING-SLOTS", "ACL2-USER", "COMMON-LISP"), 1441("MOST-NEGATIVE-FIXNUM", "ACL2-USER", "COMMON-LISP"), 1442("MAKE-METHOD", "ACL2-USER", "COMMON-LISP"), 1443("MOST-NEGATIVE-LONG-FLOAT", "ACL2-USER", "COMMON-LISP"), 1444("MAKE-PACKAGE", "ACL2-USER", "COMMON-LISP"), 1445("MOST-NEGATIVE-SHORT-FLOAT", "ACL2-USER", "COMMON-LISP"), 1446("MAKE-PATHNAME", "ACL2-USER", "COMMON-LISP"), 1447("MOST-NEGATIVE-SINGLE-FLOAT", "ACL2-USER", "COMMON-LISP"), 1448("MAKE-RANDOM-STATE", "ACL2-USER", "COMMON-LISP"), 1449("MOST-POSITIVE-DOUBLE-FLOAT", "ACL2-USER", "COMMON-LISP"), 1450("MAKE-SEQUENCE", "ACL2-USER", "COMMON-LISP"), 1451("MOST-POSITIVE-FIXNUM", "ACL2-USER", "COMMON-LISP"), 1452("MAKE-STRING", "ACL2-USER", "COMMON-LISP"), 1453("MOST-POSITIVE-LONG-FLOAT", "ACL2-USER", "COMMON-LISP"), 1454("MAKE-STRING-INPUT-STREAM", "ACL2-USER", "COMMON-LISP"), 1455("MOST-POSITIVE-SHORT-FLOAT", "ACL2-USER", "COMMON-LISP"), 1456("MAKE-STRING-OUTPUT-STREAM", "ACL2-USER", "COMMON-LISP"), 1457("MOST-POSITIVE-SINGLE-FLOAT", "ACL2-USER", "COMMON-LISP"), 1458("MAKE-SYMBOL", "ACL2-USER", "COMMON-LISP"), 1459("MUFFLE-WARNING", "ACL2-USER", "COMMON-LISP"), 1460("MAKE-SYNONYM-STREAM", "ACL2-USER", "COMMON-LISP"), 1461("MULTIPLE-VALUE-BIND", "ACL2-USER", "COMMON-LISP"), 1462("MAKE-TWO-WAY-STREAM", "ACL2-USER", "COMMON-LISP"), 1463("MULTIPLE-VALUE-CALL", "ACL2-USER", "COMMON-LISP"), 1464("MAKUNBOUND", "ACL2-USER", "COMMON-LISP"), 1465("MULTIPLE-VALUE-LIST", "ACL2-USER", "COMMON-LISP"), 1466("MAP", "ACL2-USER", "COMMON-LISP"), 1467("MULTIPLE-VALUE-PROG1", "ACL2-USER", "COMMON-LISP"), 1468("MAP-INTO", "ACL2-USER", "COMMON-LISP"), 1469("MULTIPLE-VALUE-SETQ", "ACL2-USER", "COMMON-LISP"), 1470("MAPC", "ACL2-USER", "COMMON-LISP"), 1471("MULTIPLE-VALUES-LIMIT", "ACL2-USER", "COMMON-LISP"), 1472("MAPCAN", "ACL2-USER", "COMMON-LISP"), 1473("NAME-CHAR", "ACL2-USER", "COMMON-LISP"), 1474("MAPCAR", "ACL2-USER", "COMMON-LISP"), 1475("NAMESTRING", "ACL2-USER", "COMMON-LISP"), 1476("MAPCON", "ACL2-USER", "COMMON-LISP"), 1477("NBUTLAST", "ACL2-USER", "COMMON-LISP"), 1478("MAPHASH", "ACL2-USER", "COMMON-LISP"), 1479("NCONC", "ACL2-USER", "COMMON-LISP"), 1480("MAPL", "ACL2-USER", "COMMON-LISP"), 1481("NEXT-METHOD-P", "ACL2-USER", "COMMON-LISP"), 1482("MAPLIST", "ACL2-USER", "COMMON-LISP"), 1483("NIL", "ACL2-USER", "COMMON-LISP"), 1484("NINTERSECTION", "ACL2-USER", "COMMON-LISP"), 1485("PACKAGE-ERROR", "ACL2-USER", "COMMON-LISP"), 1486("NINTH", "ACL2-USER", "COMMON-LISP"), 1487("PACKAGE-ERROR-PACKAGE", "ACL2-USER", "COMMON-LISP"), 1488("NO-APPLICABLE-METHOD", "ACL2-USER", "COMMON-LISP"), 1489("PACKAGE-NAME", "ACL2-USER", "COMMON-LISP"), 1490("NO-NEXT-METHOD", "ACL2-USER", "COMMON-LISP"), 1491("PACKAGE-NICKNAMES", "ACL2-USER", "COMMON-LISP"), 1492("NOT", "ACL2-USER", "COMMON-LISP"), 1493("PACKAGE-SHADOWING-SYMBOLS", "ACL2-USER", "COMMON-LISP"), 1494("NOTANY", "ACL2-USER", "COMMON-LISP"), 1495("PACKAGE-USE-LIST", "ACL2-USER", "COMMON-LISP"), 1496("NOTEVERY", "ACL2-USER", "COMMON-LISP"), 1497("PACKAGE-USED-BY-LIST", "ACL2-USER", "COMMON-LISP"), 1498("NOTINLINE", "ACL2-USER", "COMMON-LISP"), 1499("PACKAGEP", "ACL2-USER", "COMMON-LISP"), 1500("NRECONC", "ACL2-USER", "COMMON-LISP"), 1501("PAIRLIS", "ACL2-USER", "COMMON-LISP"), 1502("NREVERSE", "ACL2-USER", "COMMON-LISP"), 1503("PARSE-ERROR", "ACL2-USER", "COMMON-LISP"), 1504("NSET-DIFFERENCE", "ACL2-USER", "COMMON-LISP"), 1505("PARSE-INTEGER", "ACL2-USER", "COMMON-LISP"), 1506("NSET-EXCLUSIVE-OR", "ACL2-USER", "COMMON-LISP"), 1507("PARSE-NAMESTRING", "ACL2-USER", "COMMON-LISP"), 1508("NSTRING-CAPITALIZE", "ACL2-USER", "COMMON-LISP"), 1509("PATHNAME", "ACL2-USER", "COMMON-LISP"), 1510("NSTRING-DOWNCASE", "ACL2-USER", "COMMON-LISP"), 1511("PATHNAME-DEVICE", "ACL2-USER", "COMMON-LISP"), 1512("NSTRING-UPCASE", "ACL2-USER", "COMMON-LISP"), 1513("PATHNAME-DIRECTORY", "ACL2-USER", "COMMON-LISP"), 1514("NSUBLIS", "ACL2-USER", "COMMON-LISP"), 1515("PATHNAME-HOST", "ACL2-USER", "COMMON-LISP"), 1516("NSUBST", "ACL2-USER", "COMMON-LISP"), 1517("PATHNAME-MATCH-P", "ACL2-USER", "COMMON-LISP"), 1518("NSUBST-IF", "ACL2-USER", "COMMON-LISP"), 1519("PATHNAME-NAME", "ACL2-USER", "COMMON-LISP"), 1520("NSUBST-IF-NOT", "ACL2-USER", "COMMON-LISP"), 1521("PATHNAME-TYPE", "ACL2-USER", "COMMON-LISP"), 1522("NSUBSTITUTE", "ACL2-USER", "COMMON-LISP"), 1523("PATHNAME-VERSION", "ACL2-USER", "COMMON-LISP"), 1524("NSUBSTITUTE-IF", "ACL2-USER", "COMMON-LISP"), 1525("PATHNAMEP", "ACL2-USER", "COMMON-LISP"), 1526("NSUBSTITUTE-IF-NOT", "ACL2-USER", "COMMON-LISP"), 1527("PEEK-CHAR", "ACL2-USER", "COMMON-LISP"), 1528("NTH", "ACL2-USER", "COMMON-LISP"), 1529("PHASE", "ACL2-USER", "COMMON-LISP"), 1530("NTH-VALUE", "ACL2-USER", "COMMON-LISP"), 1531("PI", "ACL2-USER", "COMMON-LISP"), 1532("NTHCDR", "ACL2-USER", "COMMON-LISP"), 1533("PLUSP", "ACL2-USER", "COMMON-LISP"), 1534("NULL", "ACL2-USER", "COMMON-LISP"), 1535("POP", "ACL2-USER", "COMMON-LISP"), 1536("NUMBER", "ACL2-USER", "COMMON-LISP"), 1537("POSITION", "ACL2-USER", "COMMON-LISP"), 1538("NUMBERP", "ACL2-USER", "COMMON-LISP"), 1539("POSITION-IF", "ACL2-USER", "COMMON-LISP"), 1540("NUMERATOR", "ACL2-USER", "COMMON-LISP"), 1541("POSITION-IF-NOT", "ACL2-USER", "COMMON-LISP"), 1542("NUNION", "ACL2-USER", "COMMON-LISP"), 1543("PPRINT", "ACL2-USER", "COMMON-LISP"), 1544("ODDP", "ACL2-USER", "COMMON-LISP"), 1545("PPRINT-DISPATCH", "ACL2-USER", "COMMON-LISP"), 1546("OPEN", "ACL2-USER", "COMMON-LISP"), 1547("PPRINT-EXIT-IF-LIST-EXHAUSTED", "ACL2-USER", "COMMON-LISP"), 1548("OPEN-STREAM-P", "ACL2-USER", "COMMON-LISP"), 1549("PPRINT-FILL", "ACL2-USER", "COMMON-LISP"), 1550("OPTIMIZE", "ACL2-USER", "COMMON-LISP"), 1551("PPRINT-INDENT", "ACL2-USER", "COMMON-LISP"), 1552("OR", "ACL2-USER", "COMMON-LISP"), 1553("PPRINT-LINEAR", "ACL2-USER", "COMMON-LISP"), 1554("OTHERWISE", "ACL2-USER", "COMMON-LISP"), 1555("PPRINT-LOGICAL-BLOCK", "ACL2-USER", "COMMON-LISP"), 1556("OUTPUT-STREAM-P", "ACL2-USER", "COMMON-LISP"), 1557("PPRINT-NEWLINE", "ACL2-USER", "COMMON-LISP"), 1558("PACKAGE", "ACL2-USER", "COMMON-LISP"), 1559("PPRINT-POP", "ACL2-USER", "COMMON-LISP"), 1560("PPRINT-TAB", "ACL2-USER", "COMMON-LISP"), 1561("READ-CHAR", "ACL2-USER", "COMMON-LISP"), 1562("PPRINT-TABULAR", "ACL2-USER", "COMMON-LISP"), 1563("READ-CHAR-NO-HANG", "ACL2-USER", "COMMON-LISP"), 1564("PRIN1", "ACL2-USER", "COMMON-LISP"), 1565("READ-DELIMITED-LIST", "ACL2-USER", "COMMON-LISP"), 1566("PRIN1-TO-STRING", "ACL2-USER", "COMMON-LISP"), 1567("READ-FROM-STRING", "ACL2-USER", "COMMON-LISP"), 1568("PRINC", "ACL2-USER", "COMMON-LISP"), 1569("READ-LINE", "ACL2-USER", "COMMON-LISP"), 1570("PRINC-TO-STRING", "ACL2-USER", "COMMON-LISP"), 1571("READ-PRESERVING-WHITESPACE", "ACL2-USER", "COMMON-LISP"), 1572("PRINT", "ACL2-USER", "COMMON-LISP"), 1573("READ-SEQUENCE", "ACL2-USER", "COMMON-LISP"), 1574("PRINT-NOT-READABLE", "ACL2-USER", "COMMON-LISP"), 1575("READER-ERROR", "ACL2-USER", "COMMON-LISP"), 1576("PRINT-NOT-READABLE-OBJECT", "ACL2-USER", "COMMON-LISP"), 1577("READTABLE", "ACL2-USER", "COMMON-LISP"), 1578("PRINT-OBJECT", "ACL2-USER", "COMMON-LISP"), 1579("READTABLE-CASE", "ACL2-USER", "COMMON-LISP"), 1580("PRINT-UNREADABLE-OBJECT", "ACL2-USER", "COMMON-LISP"), 1581("READTABLEP", "ACL2-USER", "COMMON-LISP"), 1582("PROBE-FILE", "ACL2-USER", "COMMON-LISP"), 1583("REAL", "ACL2-USER", "COMMON-LISP"), 1584("PROCLAIM", "ACL2-USER", "COMMON-LISP"), 1585("REALP", "ACL2-USER", "COMMON-LISP"), 1586("PROG", "ACL2-USER", "COMMON-LISP"), 1587("REALPART", "ACL2-USER", "COMMON-LISP"), 1588("PROG*", "ACL2-USER", "COMMON-LISP"), 1589("REDUCE", "ACL2-USER", "COMMON-LISP"), 1590("PROG1", "ACL2-USER", "COMMON-LISP"), 1591("REINITIALIZE-INSTANCE", "ACL2-USER", "COMMON-LISP"), 1592("PROG2", "ACL2-USER", "COMMON-LISP"), 1593("REM", "ACL2-USER", "COMMON-LISP"), 1594("PROGN", "ACL2-USER", "COMMON-LISP"), 1595("REMF", "ACL2-USER", "COMMON-LISP"), 1596("PROGRAM-ERROR", "ACL2-USER", "COMMON-LISP"), 1597("REMHASH", "ACL2-USER", "COMMON-LISP"), 1598("PROGV", "ACL2-USER", "COMMON-LISP"), 1599("REMOVE", "ACL2-USER", "COMMON-LISP"), 1600("PROVIDE", "ACL2-USER", "COMMON-LISP"), 1601("REMOVE-DUPLICATES", "ACL2-USER", "COMMON-LISP"), 1602("PSETF", "ACL2-USER", "COMMON-LISP"), 1603("REMOVE-IF", "ACL2-USER", "COMMON-LISP"), 1604("PSETQ", "ACL2-USER", "COMMON-LISP"), 1605("REMOVE-IF-NOT", "ACL2-USER", "COMMON-LISP"), 1606("PUSH", "ACL2-USER", "COMMON-LISP"), 1607("REMOVE-METHOD", "ACL2-USER", "COMMON-LISP"), 1608("PUSHNEW", "ACL2-USER", "COMMON-LISP"), 1609("REMPROP", "ACL2-USER", "COMMON-LISP"), 1610("QUOTE", "ACL2-USER", "COMMON-LISP"), 1611("RENAME-FILE", "ACL2-USER", "COMMON-LISP"), 1612("RANDOM", "ACL2-USER", "COMMON-LISP"), 1613("RENAME-PACKAGE", "ACL2-USER", "COMMON-LISP"), 1614("RANDOM-STATE", "ACL2-USER", "COMMON-LISP"), 1615("REPLACE", "ACL2-USER", "COMMON-LISP"), 1616("RANDOM-STATE-P", "ACL2-USER", "COMMON-LISP"), 1617("REQUIRE", "ACL2-USER", "COMMON-LISP"), 1618("RASSOC", "ACL2-USER", "COMMON-LISP"), 1619("REST", "ACL2-USER", "COMMON-LISP"), 1620("RASSOC-IF", "ACL2-USER", "COMMON-LISP"), 1621("RESTART", "ACL2-USER", "COMMON-LISP"), 1622("RASSOC-IF-NOT", "ACL2-USER", "COMMON-LISP"), 1623("RESTART-BIND", "ACL2-USER", "COMMON-LISP"), 1624("RATIO", "ACL2-USER", "COMMON-LISP"), 1625("RESTART-CASE", "ACL2-USER", "COMMON-LISP"), 1626("RATIONAL", "ACL2-USER", "COMMON-LISP"), 1627("RESTART-NAME", "ACL2-USER", "COMMON-LISP"), 1628("RATIONALIZE", "ACL2-USER", "COMMON-LISP"), 1629("RETURN", "ACL2-USER", "COMMON-LISP"), 1630("RATIONALP", "ACL2-USER", "COMMON-LISP"), 1631("RETURN-FROM", "ACL2-USER", "COMMON-LISP"), 1632("READ", "ACL2-USER", "COMMON-LISP"), 1633("REVAPPEND", "ACL2-USER", "COMMON-LISP"), 1634("READ-BYTE", "ACL2-USER", "COMMON-LISP"), 1635("REVERSE", "ACL2-USER", "COMMON-LISP"), 1636("ROOM", "ACL2-USER", "COMMON-LISP"), 1637("SIMPLE-BIT-VECTOR", "ACL2-USER", "COMMON-LISP"), 1638("ROTATEF", "ACL2-USER", "COMMON-LISP"), 1639("SIMPLE-BIT-VECTOR-P", "ACL2-USER", "COMMON-LISP"), 1640("ROUND", "ACL2-USER", "COMMON-LISP"), 1641("SIMPLE-CONDITION", "ACL2-USER", "COMMON-LISP"), 1642("ROW-MAJOR-AREF", "ACL2-USER", "COMMON-LISP"), 1643("SIMPLE-CONDITION-FORMAT-ARGUMENTS", "ACL2-USER", "COMMON-LISP"), 1644("RPLACA", "ACL2-USER", "COMMON-LISP"), 1645("SIMPLE-CONDITION-FORMAT-CONTROL", "ACL2-USER", "COMMON-LISP"), 1646("RPLACD", "ACL2-USER", "COMMON-LISP"), 1647("SIMPLE-ERROR", "ACL2-USER", "COMMON-LISP"), 1648("SAFETY", "ACL2-USER", "COMMON-LISP"), 1649("SIMPLE-STRING", "ACL2-USER", "COMMON-LISP"), 1650("SATISFIES", "ACL2-USER", "COMMON-LISP"), 1651("SIMPLE-STRING-P", "ACL2-USER", "COMMON-LISP"), 1652("SBIT", "ACL2-USER", "COMMON-LISP"), 1653("SIMPLE-TYPE-ERROR", "ACL2-USER", "COMMON-LISP"), 1654("SCALE-FLOAT", "ACL2-USER", "COMMON-LISP"), 1655("SIMPLE-VECTOR", "ACL2-USER", "COMMON-LISP"), 1656("SCHAR", "ACL2-USER", "COMMON-LISP"), 1657("SIMPLE-VECTOR-P", "ACL2-USER", "COMMON-LISP"), 1658("SEARCH", "ACL2-USER", "COMMON-LISP"), 1659("SIMPLE-WARNING", "ACL2-USER", "COMMON-LISP"), 1660("SECOND", "ACL2-USER", "COMMON-LISP"), 1661("SIN", "ACL2-USER", "COMMON-LISP"), 1662("SEQUENCE", "ACL2-USER", "COMMON-LISP"), 1663("SINGLE-FLOAT", "ACL2-USER", "COMMON-LISP"), 1664("SERIOUS-CONDITION", "ACL2-USER", "COMMON-LISP"), 1665("SINGLE-FLOAT-EPSILON", "ACL2-USER", "COMMON-LISP"), 1666("SET", "ACL2-USER", "COMMON-LISP"), 1667("SINGLE-FLOAT-NEGATIVE-EPSILON", "ACL2-USER", "COMMON-LISP"), 1668("SET-DIFFERENCE", "ACL2-USER", "COMMON-LISP"), 1669("SINH", "ACL2-USER", "COMMON-LISP"), 1670("SET-DISPATCH-MACRO-CHARACTER", "ACL2-USER", "COMMON-LISP"), 1671("SIXTH", "ACL2-USER", "COMMON-LISP"), 1672("SET-EXCLUSIVE-OR", "ACL2-USER", "COMMON-LISP"), 1673("SLEEP", "ACL2-USER", "COMMON-LISP"), 1674("SET-MACRO-CHARACTER", "ACL2-USER", "COMMON-LISP"), 1675("SLOT-BOUNDP", "ACL2-USER", "COMMON-LISP"), 1676("SET-PPRINT-DISPATCH", "ACL2-USER", "COMMON-LISP"), 1677("SLOT-EXISTS-P", "ACL2-USER", "COMMON-LISP"), 1678("SET-SYNTAX-FROM-CHAR", "ACL2-USER", "COMMON-LISP"), 1679("SLOT-MAKUNBOUND", "ACL2-USER", "COMMON-LISP"), 1680("SETF", "ACL2-USER", "COMMON-LISP"), 1681("SLOT-MISSING", "ACL2-USER", "COMMON-LISP"), 1682("SETQ", "ACL2-USER", "COMMON-LISP"), 1683("SLOT-UNBOUND", "ACL2-USER", "COMMON-LISP"), 1684("SEVENTH", "ACL2-USER", "COMMON-LISP"), 1685("SLOT-VALUE", "ACL2-USER", "COMMON-LISP"), 1686("SHADOW", "ACL2-USER", "COMMON-LISP"), 1687("SOFTWARE-TYPE", "ACL2-USER", "COMMON-LISP"), 1688("SHADOWING-IMPORT", "ACL2-USER", "COMMON-LISP"), 1689("SOFTWARE-VERSION", "ACL2-USER", "COMMON-LISP"), 1690("SHARED-INITIALIZE", "ACL2-USER", "COMMON-LISP"), 1691("SOME", "ACL2-USER", "COMMON-LISP"), 1692("SHIFTF", "ACL2-USER", "COMMON-LISP"), 1693("SORT", "ACL2-USER", "COMMON-LISP"), 1694("SHORT-FLOAT", "ACL2-USER", "COMMON-LISP"), 1695("SPACE", "ACL2-USER", "COMMON-LISP"), 1696("SHORT-FLOAT-EPSILON", "ACL2-USER", "COMMON-LISP"), 1697("SPECIAL", "ACL2-USER", "COMMON-LISP"), 1698("SHORT-FLOAT-NEGATIVE-EPSILON", "ACL2-USER", "COMMON-LISP"), 1699("SPECIAL-OPERATOR-P", "ACL2-USER", "COMMON-LISP"), 1700("SHORT-SITE-NAME", "ACL2-USER", "COMMON-LISP"), 1701("SPEED", "ACL2-USER", "COMMON-LISP"), 1702("SIGNAL", "ACL2-USER", "COMMON-LISP"), 1703("SQRT", "ACL2-USER", "COMMON-LISP"), 1704("SIGNED-BYTE", "ACL2-USER", "COMMON-LISP"), 1705("STABLE-SORT", "ACL2-USER", "COMMON-LISP"), 1706("SIGNUM", "ACL2-USER", "COMMON-LISP"), 1707("STANDARD", "ACL2-USER", "COMMON-LISP"), 1708("SIMPLE-ARRAY", "ACL2-USER", "COMMON-LISP"), 1709("STANDARD-CHAR", "ACL2-USER", "COMMON-LISP"), 1710("SIMPLE-BASE-STRING", "ACL2-USER", "COMMON-LISP"), 1711("STANDARD-CHAR-P", "ACL2-USER", "COMMON-LISP"), 1712("STANDARD-CLASS", "ACL2-USER", "COMMON-LISP"), 1713("SUBLIS", "ACL2-USER", "COMMON-LISP"), 1714("STANDARD-GENERIC-FUNCTION", "ACL2-USER", "COMMON-LISP"), 1715("SUBSEQ", "ACL2-USER", "COMMON-LISP"), 1716("STANDARD-METHOD", "ACL2-USER", "COMMON-LISP"), 1717("SUBSETP", "ACL2-USER", "COMMON-LISP"), 1718("STANDARD-OBJECT", "ACL2-USER", "COMMON-LISP"), 1719("SUBST", "ACL2-USER", "COMMON-LISP"), 1720("STEP", "ACL2-USER", "COMMON-LISP"), 1721("SUBST-IF", "ACL2-USER", "COMMON-LISP"), 1722("STORAGE-CONDITION", "ACL2-USER", "COMMON-LISP"), 1723("SUBST-IF-NOT", "ACL2-USER", "COMMON-LISP"), 1724("STORE-VALUE", "ACL2-USER", "COMMON-LISP"), 1725("SUBSTITUTE", "ACL2-USER", "COMMON-LISP"), 1726("STREAM", "ACL2-USER", "COMMON-LISP"), 1727("SUBSTITUTE-IF", "ACL2-USER", "COMMON-LISP"), 1728("STREAM-ELEMENT-TYPE", "ACL2-USER", "COMMON-LISP"), 1729("SUBSTITUTE-IF-NOT", "ACL2-USER", "COMMON-LISP"), 1730("STREAM-ERROR", "ACL2-USER", "COMMON-LISP"), 1731("SUBTYPEP", "ACL2-USER", "COMMON-LISP"), 1732("STREAM-ERROR-STREAM", "ACL2-USER", "COMMON-LISP"), 1733("SVREF", "ACL2-USER", "COMMON-LISP"), 1734("STREAM-EXTERNAL-FORMAT", "ACL2-USER", "COMMON-LISP"), 1735("SXHASH", "ACL2-USER", "COMMON-LISP"), 1736("STREAMP", "ACL2-USER", "COMMON-LISP"), 1737("SYMBOL", "ACL2-USER", "COMMON-LISP"), 1738("STRING", "ACL2-USER", "COMMON-LISP"), 1739("SYMBOL-FUNCTION", "ACL2-USER", "COMMON-LISP"), 1740("STRING-CAPITALIZE", "ACL2-USER", "COMMON-LISP"), 1741("SYMBOL-MACROLET", "ACL2-USER", "COMMON-LISP"), 1742("STRING-DOWNCASE", "ACL2-USER", "COMMON-LISP"), 1743("SYMBOL-NAME", "ACL2-USER", "COMMON-LISP"), 1744("STRING-EQUAL", "ACL2-USER", "COMMON-LISP"), 1745("SYMBOL-PACKAGE", "ACL2-USER", "COMMON-LISP"), 1746("STRING-GREATERP", "ACL2-USER", "COMMON-LISP"), 1747("SYMBOL-PLIST", "ACL2-USER", "COMMON-LISP"), 1748("STRING-LEFT-TRIM", "ACL2-USER", "COMMON-LISP"), 1749("SYMBOL-VALUE", "ACL2-USER", "COMMON-LISP"), 1750("STRING-LESSP", "ACL2-USER", "COMMON-LISP"), 1751("SYMBOLP", "ACL2-USER", "COMMON-LISP"), 1752("STRING-NOT-EQUAL", "ACL2-USER", "COMMON-LISP"), 1753("SYNONYM-STREAM", "ACL2-USER", "COMMON-LISP"), 1754("STRING-NOT-GREATERP", "ACL2-USER", "COMMON-LISP"), 1755("SYNONYM-STREAM-SYMBOL", "ACL2-USER", "COMMON-LISP"), 1756("STRING-NOT-LESSP", "ACL2-USER", "COMMON-LISP"), 1757("T", "ACL2-USER", "COMMON-LISP"), 1758("STRING-RIGHT-TRIM", "ACL2-USER", "COMMON-LISP"), 1759("TAGBODY", "ACL2-USER", "COMMON-LISP"), 1760("STRING-STREAM", "ACL2-USER", "COMMON-LISP"), 1761("TAILP", "ACL2-USER", "COMMON-LISP"), 1762("STRING-TRIM", "ACL2-USER", "COMMON-LISP"), 1763("TAN", "ACL2-USER", "COMMON-LISP"), 1764("STRING-UPCASE", "ACL2-USER", "COMMON-LISP"), 1765("TANH", "ACL2-USER", "COMMON-LISP"), 1766("STRING/=", "ACL2-USER", "COMMON-LISP"), 1767("TENTH", "ACL2-USER", "COMMON-LISP"), 1768("STRING<", "ACL2-USER", "COMMON-LISP"), 1769("TERPRI", "ACL2-USER", "COMMON-LISP"), 1770("STRING<=", "ACL2-USER", "COMMON-LISP"), 1771("THE", "ACL2-USER", "COMMON-LISP"), 1772("STRING=", "ACL2-USER", "COMMON-LISP"), 1773("THIRD", "ACL2-USER", "COMMON-LISP"), 1774("STRING>", "ACL2-USER", "COMMON-LISP"), 1775("THROW", "ACL2-USER", "COMMON-LISP"), 1776("STRING>=", "ACL2-USER", "COMMON-LISP"), 1777("TIME", "ACL2-USER", "COMMON-LISP"), 1778("STRINGP", "ACL2-USER", "COMMON-LISP"), 1779("TRACE", "ACL2-USER", "COMMON-LISP"), 1780("STRUCTURE", "ACL2-USER", "COMMON-LISP"), 1781("TRANSLATE-LOGICAL-PATHNAME", "ACL2-USER", "COMMON-LISP"), 1782("STRUCTURE-CLASS", "ACL2-USER", "COMMON-LISP"), 1783("TRANSLATE-PATHNAME", "ACL2-USER", "COMMON-LISP"), 1784("STRUCTURE-OBJECT", "ACL2-USER", "COMMON-LISP"), 1785("TREE-EQUAL", "ACL2-USER", "COMMON-LISP"), 1786("STYLE-WARNING", "ACL2-USER", "COMMON-LISP"), 1787("TRUENAME", "ACL2-USER", "COMMON-LISP"), 1788("TRUNCATE", "ACL2-USER", "COMMON-LISP"), 1789("VALUES-LIST", "ACL2-USER", "COMMON-LISP"), 1790("TWO-WAY-STREAM", "ACL2-USER", "COMMON-LISP"), 1791("VARIABLE", "ACL2-USER", "COMMON-LISP"), 1792("TWO-WAY-STREAM-INPUT-STREAM", "ACL2-USER", "COMMON-LISP"), 1793("VECTOR", "ACL2-USER", "COMMON-LISP"), 1794("TWO-WAY-STREAM-OUTPUT-STREAM", "ACL2-USER", "COMMON-LISP"), 1795("VECTOR-POP", "ACL2-USER", "COMMON-LISP"), 1796("TYPE", "ACL2-USER", "COMMON-LISP"), 1797("VECTOR-PUSH", "ACL2-USER", "COMMON-LISP"), 1798("TYPE-ERROR", "ACL2-USER", "COMMON-LISP"), 1799("VECTOR-PUSH-EXTEND", "ACL2-USER", "COMMON-LISP"), 1800("TYPE-ERROR-DATUM", "ACL2-USER", "COMMON-LISP"), 1801("VECTORP", "ACL2-USER", "COMMON-LISP"), 1802("TYPE-ERROR-EXPECTED-TYPE", "ACL2-USER", "COMMON-LISP"), 1803("WARN", "ACL2-USER", "COMMON-LISP"), 1804("TYPE-OF", "ACL2-USER", "COMMON-LISP"), 1805("WARNING", "ACL2-USER", "COMMON-LISP"), 1806("TYPECASE", "ACL2-USER", "COMMON-LISP"), 1807("WHEN", "ACL2-USER", "COMMON-LISP"), 1808("TYPEP", "ACL2-USER", "COMMON-LISP"), 1809("WILD-PATHNAME-P", "ACL2-USER", "COMMON-LISP"), 1810("UNBOUND-SLOT", "ACL2-USER", "COMMON-LISP"), 1811("WITH-ACCESSORS", "ACL2-USER", "COMMON-LISP"), 1812("UNBOUND-SLOT-INSTANCE", "ACL2-USER", "COMMON-LISP"), 1813("WITH-COMPILATION-UNIT", "ACL2-USER", "COMMON-LISP"), 1814("UNBOUND-VARIABLE", "ACL2-USER", "COMMON-LISP"), 1815("WITH-CONDITION-RESTARTS", "ACL2-USER", "COMMON-LISP"), 1816("UNDEFINED-FUNCTION", "ACL2-USER", "COMMON-LISP"), 1817("WITH-HASH-TABLE-ITERATOR", "ACL2-USER", "COMMON-LISP"), 1818("UNEXPORT", "ACL2-USER", "COMMON-LISP"), 1819("WITH-INPUT-FROM-STRING", "ACL2-USER", "COMMON-LISP"), 1820("UNINTERN", "ACL2-USER", "COMMON-LISP"), 1821("WITH-OPEN-FILE", "ACL2-USER", "COMMON-LISP"), 1822("UNION", "ACL2-USER", "COMMON-LISP"), 1823("WITH-OPEN-STREAM", "ACL2-USER", "COMMON-LISP"), 1824("UNLESS", "ACL2-USER", "COMMON-LISP"), 1825("WITH-OUTPUT-TO-STRING", "ACL2-USER", "COMMON-LISP"), 1826("UNREAD-CHAR", "ACL2-USER", "COMMON-LISP"), 1827("WITH-PACKAGE-ITERATOR", "ACL2-USER", "COMMON-LISP"), 1828("UNSIGNED-BYTE", "ACL2-USER", "COMMON-LISP"), 1829("WITH-SIMPLE-RESTART", "ACL2-USER", "COMMON-LISP"), 1830("UNTRACE", "ACL2-USER", "COMMON-LISP"), 1831("WITH-SLOTS", "ACL2-USER", "COMMON-LISP"), 1832("UNUSE-PACKAGE", "ACL2-USER", "COMMON-LISP"), 1833("WITH-STANDARD-IO-SYNTAX", "ACL2-USER", "COMMON-LISP"), 1834("UNWIND-PROTECT", "ACL2-USER", "COMMON-LISP"), 1835("WRITE", "ACL2-USER", "COMMON-LISP"), 1836("UPDATE-INSTANCE-FOR-DIFFERENT-CLASS", "ACL2-USER", "COMMON-LISP"), 1837("WRITE-BYTE", "ACL2-USER", "COMMON-LISP"), 1838("UPDATE-INSTANCE-FOR-REDEFINED-CLASS", "ACL2-USER", "COMMON-LISP"), 1839("WRITE-CHAR", "ACL2-USER", "COMMON-LISP"), 1840("UPGRADED-ARRAY-ELEMENT-TYPE", "ACL2-USER", "COMMON-LISP"), 1841("WRITE-LINE", "ACL2-USER", "COMMON-LISP"), 1842("UPGRADED-COMPLEX-PART-TYPE", "ACL2-USER", "COMMON-LISP"), 1843("WRITE-SEQUENCE", "ACL2-USER", "COMMON-LISP"), 1844("UPPER-CASE-P", "ACL2-USER", "COMMON-LISP"), 1845("WRITE-STRING", "ACL2-USER", "COMMON-LISP"), 1846("USE-PACKAGE", "ACL2-USER", "COMMON-LISP"), 1847("WRITE-TO-STRING", "ACL2-USER", "COMMON-LISP"), 1848("USE-VALUE", "ACL2-USER", "COMMON-LISP"), 1849("Y-OR-N-P", "ACL2-USER", "COMMON-LISP"), 1850("USER-HOMEDIR-PATHNAME", "ACL2-USER", "COMMON-LISP"), 1851("YES-OR-NO-P", "ACL2-USER", "COMMON-LISP"), 1852("VALUES", "ACL2-USER", "COMMON-LISP"), 1853("ZEROP", "ACL2-USER", "COMMON-LISP"), 1854("&ALLOW-OTHER-KEYS", "ACL2", "COMMON-LISP"), 1855("*PRINT-MISER-WIDTH*", "ACL2", "COMMON-LISP"), 1856("&AUX", "ACL2", "COMMON-LISP"), 1857("*PRINT-PPRINT-DISPATCH*", "ACL2", "COMMON-LISP"), 1858("&BODY", "ACL2", "COMMON-LISP"), 1859("*PRINT-PRETTY*", "ACL2", "COMMON-LISP"), 1860("&ENVIRONMENT", "ACL2", "COMMON-LISP"), 1861("*PRINT-RADIX*", "ACL2", "COMMON-LISP"), 1862("&KEY", "ACL2", "COMMON-LISP"), 1863("*PRINT-READABLY*", "ACL2", "COMMON-LISP"), 1864("&OPTIONAL", "ACL2", "COMMON-LISP"), 1865("*PRINT-RIGHT-MARGIN*", "ACL2", "COMMON-LISP"), 1866("&REST", "ACL2", "COMMON-LISP"), 1867("*QUERY-IO*", "ACL2", "COMMON-LISP"), 1868("&WHOLE", "ACL2", "COMMON-LISP"), 1869("*RANDOM-STATE*", "ACL2", "COMMON-LISP"), 1870("*", "ACL2", "COMMON-LISP"), 1871("*READ-BASE*", "ACL2", "COMMON-LISP"), 1872("**", "ACL2", "COMMON-LISP"), 1873("*READ-DEFAULT-FLOAT-FORMAT*", "ACL2", "COMMON-LISP"), 1874("***", "ACL2", "COMMON-LISP"), 1875("*READ-EVAL*", "ACL2", "COMMON-LISP"), 1876("*BREAK-ON-SIGNALS*", "ACL2", "COMMON-LISP"), 1877("*READ-SUPPRESS*", "ACL2", "COMMON-LISP"), 1878("*COMPILE-FILE-PATHNAME*", "ACL2", "COMMON-LISP"), 1879("*READTABLE*", "ACL2", "COMMON-LISP"), 1880("*COMPILE-FILE-TRUENAME*", "ACL2", "COMMON-LISP"), 1881("*STANDARD-INPUT*", "ACL2", "COMMON-LISP"), 1882("*COMPILE-PRINT*", "ACL2", "COMMON-LISP"), 1883("*STANDARD-OUTPUT*", "ACL2", "COMMON-LISP"), 1884("*COMPILE-VERBOSE*", "ACL2", "COMMON-LISP"), 1885("*TERMINAL-IO*", "ACL2", "COMMON-LISP"), 1886("*DEBUG-IO*", "ACL2", "COMMON-LISP"), 1887("*TRACE-OUTPUT*", "ACL2", "COMMON-LISP"), 1888("*DEBUGGER-HOOK*", "ACL2", "COMMON-LISP"), 1889("+", "ACL2", "COMMON-LISP"), 1890("*DEFAULT-PATHNAME-DEFAULTS*", "ACL2", "COMMON-LISP"), 1891("++", "ACL2", "COMMON-LISP"), 1892("*ERROR-OUTPUT*", "ACL2", "COMMON-LISP"), 1893("+++", "ACL2", "COMMON-LISP"), 1894("*FEATURES*", "ACL2", "COMMON-LISP"), 1895("-", "ACL2", "COMMON-LISP"), 1896("*GENSYM-COUNTER*", "ACL2", "COMMON-LISP"), 1897("/", "ACL2", "COMMON-LISP"), 1898("*LOAD-PATHNAME*", "ACL2", "COMMON-LISP"), 1899("//", "ACL2", "COMMON-LISP"), 1900("*LOAD-PRINT*", "ACL2", "COMMON-LISP"), 1901("///", "ACL2", "COMMON-LISP"), 1902("*LOAD-TRUENAME*", "ACL2", "COMMON-LISP"), 1903("/=", "ACL2", "COMMON-LISP"), 1904("*LOAD-VERBOSE*", "ACL2", "COMMON-LISP"), 1905("1+", "ACL2", "COMMON-LISP"), 1906("*MACROEXPAND-HOOK*", "ACL2", "COMMON-LISP"), 1907("1-", "ACL2", "COMMON-LISP"), 1908("*MODULES*", "ACL2", "COMMON-LISP"), 1909("<", "ACL2", "COMMON-LISP"), 1910("*PACKAGE*", "ACL2", "COMMON-LISP"), 1911("<=", "ACL2", "COMMON-LISP"), 1912("*PRINT-ARRAY*", "ACL2", "COMMON-LISP"), 1913("=", "ACL2", "COMMON-LISP"), 1914("*PRINT-BASE*", "ACL2", "COMMON-LISP"), 1915(">", "ACL2", "COMMON-LISP"), 1916("*PRINT-CASE*", "ACL2", "COMMON-LISP"), 1917(">=", "ACL2", "COMMON-LISP"), 1918("*PRINT-CIRCLE*", "ACL2", "COMMON-LISP"), 1919("ABORT", "ACL2", "COMMON-LISP"), 1920("*PRINT-ESCAPE*", "ACL2", "COMMON-LISP"), 1921("ABS", "ACL2", "COMMON-LISP"), 1922("*PRINT-GENSYM*", "ACL2", "COMMON-LISP"), 1923("ACONS", "ACL2", "COMMON-LISP"), 1924("*PRINT-LENGTH*", "ACL2", "COMMON-LISP"), 1925("ACOS", "ACL2", "COMMON-LISP"), 1926("*PRINT-LEVEL*", "ACL2", "COMMON-LISP"), 1927("ACOSH", "ACL2", "COMMON-LISP"), 1928("*PRINT-LINES*", "ACL2", "COMMON-LISP"), 1929("ADD-METHOD", "ACL2", "COMMON-LISP"), 1930("ADJOIN", "ACL2", "COMMON-LISP"), 1931("ATOM", "ACL2", "COMMON-LISP"), 1932("BOUNDP", "ACL2", "COMMON-LISP"), 1933("ADJUST-ARRAY", "ACL2", "COMMON-LISP"), 1934("BASE-CHAR", "ACL2", "COMMON-LISP"), 1935("BREAK", "ACL2", "COMMON-LISP"), 1936("ADJUSTABLE-ARRAY-P", "ACL2", "COMMON-LISP"), 1937("BASE-STRING", "ACL2", "COMMON-LISP"), 1938("BROADCAST-STREAM", "ACL2", "COMMON-LISP"), 1939("ALLOCATE-INSTANCE", "ACL2", "COMMON-LISP"), 1940("BIGNUM", "ACL2", "COMMON-LISP"), 1941("BROADCAST-STREAM-STREAMS", "ACL2", "COMMON-LISP"), 1942("ALPHA-CHAR-P", "ACL2", "COMMON-LISP"), 1943("BIT", "ACL2", "COMMON-LISP"), 1944("BUILT-IN-CLASS", "ACL2", "COMMON-LISP"), 1945("ALPHANUMERICP", "ACL2", "COMMON-LISP"), 1946("BIT-AND", "ACL2", "COMMON-LISP"), 1947("BUTLAST", "ACL2", "COMMON-LISP"), 1948("AND", "ACL2", "COMMON-LISP"), 1949("BIT-ANDC1", "ACL2", "COMMON-LISP"), 1950("BYTE", "ACL2", "COMMON-LISP"), 1951("APPEND", "ACL2", "COMMON-LISP"), 1952("BIT-ANDC2", "ACL2", "COMMON-LISP"), 1953("BYTE-POSITION", "ACL2", "COMMON-LISP"), 1954("APPLY", "ACL2", "COMMON-LISP"), 1955("BIT-EQV", "ACL2", "COMMON-LISP"), 1956("BYTE-SIZE", "ACL2", "COMMON-LISP"), 1957("APROPOS", "ACL2", "COMMON-LISP"), 1958("BIT-IOR", "ACL2", "COMMON-LISP"), 1959("CAAAAR", "ACL2", "COMMON-LISP"), 1960("APROPOS-LIST", "ACL2", "COMMON-LISP"), 1961("BIT-NAND", "ACL2", "COMMON-LISP"), 1962("CAAADR", "ACL2", "COMMON-LISP"), 1963("AREF", "ACL2", "COMMON-LISP"), 1964("BIT-NOR", "ACL2", "COMMON-LISP"), 1965("CAAAR", "ACL2", "COMMON-LISP"), 1966("ARITHMETIC-ERROR", "ACL2", "COMMON-LISP"), 1967("BIT-NOT", "ACL2", "COMMON-LISP"), 1968("CAADAR", "ACL2", "COMMON-LISP"), 1969("ARITHMETIC-ERROR-OPERANDS", "ACL2", "COMMON-LISP"), 1970("BIT-ORC1", "ACL2", "COMMON-LISP"), 1971("CAADDR", "ACL2", "COMMON-LISP"), 1972("ARITHMETIC-ERROR-OPERATION", "ACL2", "COMMON-LISP"), 1973("BIT-ORC2", "ACL2", "COMMON-LISP"), 1974("CAADR", "ACL2", "COMMON-LISP"), 1975("ARRAY", "ACL2", "COMMON-LISP"), 1976("BIT-VECTOR", "ACL2", "COMMON-LISP"), 1977("CAAR", "ACL2", "COMMON-LISP"), 1978("ARRAY-DIMENSION", "ACL2", "COMMON-LISP"), 1979("BIT-VECTOR-P", "ACL2", "COMMON-LISP"), 1980("CADAAR", "ACL2", "COMMON-LISP"), 1981("ARRAY-DIMENSION-LIMIT", "ACL2", "COMMON-LISP"), 1982("BIT-XOR", "ACL2", "COMMON-LISP"), 1983("CADADR", "ACL2", "COMMON-LISP"), 1984("ARRAY-DIMENSIONS", "ACL2", "COMMON-LISP"), 1985("BLOCK", "ACL2", "COMMON-LISP"), 1986("CADAR", "ACL2", "COMMON-LISP"), 1987("ARRAY-DISPLACEMENT", "ACL2", "COMMON-LISP"), 1988("BOOLE", "ACL2", "COMMON-LISP"), 1989("CADDAR", "ACL2", "COMMON-LISP"), 1990("ARRAY-ELEMENT-TYPE", "ACL2", "COMMON-LISP"), 1991("BOOLE-1", "ACL2", "COMMON-LISP"), 1992("CADDDR", "ACL2", "COMMON-LISP"), 1993("ARRAY-HAS-FILL-POINTER-P", "ACL2", "COMMON-LISP"), 1994("BOOLE-2", "ACL2", "COMMON-LISP"), 1995("CADDR", "ACL2", "COMMON-LISP"), 1996("ARRAY-IN-BOUNDS-P", "ACL2", "COMMON-LISP"), 1997("BOOLE-AND", "ACL2", "COMMON-LISP"), 1998("CADR", "ACL2", "COMMON-LISP"), 1999("ARRAY-RANK", "ACL2", "COMMON-LISP"), 2000("BOOLE-ANDC1", "ACL2", "COMMON-LISP"), 2001("CALL-ARGUMENTS-LIMIT", "ACL2", "COMMON-LISP"), 2002("ARRAY-RANK-LIMIT", "ACL2", "COMMON-LISP"), 2003("BOOLE-ANDC2", "ACL2", "COMMON-LISP"), 2004("CALL-METHOD", "ACL2", "COMMON-LISP"), 2005("ARRAY-ROW-MAJOR-INDEX", "ACL2", "COMMON-LISP"), 2006("BOOLE-C1", "ACL2", "COMMON-LISP"), 2007("CALL-NEXT-METHOD", "ACL2", "COMMON-LISP"), 2008("ARRAY-TOTAL-SIZE", "ACL2", "COMMON-LISP"), 2009("BOOLE-C2", "ACL2", "COMMON-LISP"), 2010("CAR", "ACL2", "COMMON-LISP"), 2011("ARRAY-TOTAL-SIZE-LIMIT", "ACL2", "COMMON-LISP"), 2012("BOOLE-CLR", "ACL2", "COMMON-LISP"), 2013("CASE", "ACL2", "COMMON-LISP"), 2014("ARRAYP", "ACL2", "COMMON-LISP"), 2015("BOOLE-EQV", "ACL2", "COMMON-LISP"), 2016("CATCH", "ACL2", "COMMON-LISP"), 2017("ASH", "ACL2", "COMMON-LISP"), 2018("BOOLE-IOR", "ACL2", "COMMON-LISP"), 2019("CCASE", "ACL2", "COMMON-LISP"), 2020("ASIN", "ACL2", "COMMON-LISP"), 2021("BOOLE-NAND", "ACL2", "COMMON-LISP"), 2022("CDAAAR", "ACL2", "COMMON-LISP"), 2023("ASINH", "ACL2", "COMMON-LISP"), 2024("BOOLE-NOR", "ACL2", "COMMON-LISP"), 2025("CDAADR", "ACL2", "COMMON-LISP"), 2026("ASSERT", "ACL2", "COMMON-LISP"), 2027("BOOLE-ORC1", "ACL2", "COMMON-LISP"), 2028("CDAAR", "ACL2", "COMMON-LISP"), 2029("ASSOC", "ACL2", "COMMON-LISP"), 2030("BOOLE-ORC2", "ACL2", "COMMON-LISP"), 2031("CDADAR", "ACL2", "COMMON-LISP"), 2032("ASSOC-IF", "ACL2", "COMMON-LISP"), 2033("BOOLE-SET", "ACL2", "COMMON-LISP"), 2034("CDADDR", "ACL2", "COMMON-LISP"), 2035("ASSOC-IF-NOT", "ACL2", "COMMON-LISP"), 2036("BOOLE-XOR", "ACL2", "COMMON-LISP"), 2037("CDADR", "ACL2", "COMMON-LISP"), 2038("ATAN", "ACL2", "COMMON-LISP"), 2039("BOOLEAN", "ACL2", "COMMON-LISP"), 2040("CDAR", "ACL2", "COMMON-LISP"), 2041("ATANH", "ACL2", "COMMON-LISP"), 2042("BOTH-CASE-P", "ACL2", "COMMON-LISP"), 2043("CDDAAR", "ACL2", "COMMON-LISP"), 2044("CDDADR", "ACL2", "COMMON-LISP"), 2045("CLEAR-INPUT", "ACL2", "COMMON-LISP"), 2046("COPY-TREE", "ACL2", "COMMON-LISP"), 2047("CDDAR", "ACL2", "COMMON-LISP"), 2048("CLEAR-OUTPUT", "ACL2", "COMMON-LISP"), 2049("COS", "ACL2", "COMMON-LISP"), 2050("CDDDAR", "ACL2", "COMMON-LISP"), 2051("CLOSE", "ACL2", "COMMON-LISP"), 2052("COSH", "ACL2", "COMMON-LISP"), 2053("CDDDDR", "ACL2", "COMMON-LISP"), 2054("CLRHASH", "ACL2", "COMMON-LISP"), 2055("COUNT", "ACL2", "COMMON-LISP"), 2056("CDDDR", "ACL2", "COMMON-LISP"), 2057("CODE-CHAR", "ACL2", "COMMON-LISP"), 2058("COUNT-IF", "ACL2", "COMMON-LISP"), 2059("CDDR", "ACL2", "COMMON-LISP"), 2060("COERCE", "ACL2", "COMMON-LISP"), 2061("COUNT-IF-NOT", "ACL2", "COMMON-LISP"), 2062("CDR", "ACL2", "COMMON-LISP"), 2063("COMPILATION-SPEED", "ACL2", "COMMON-LISP"), 2064("CTYPECASE", "ACL2", "COMMON-LISP"), 2065("CEILING", "ACL2", "COMMON-LISP"), 2066("COMPILE", "ACL2", "COMMON-LISP"), 2067("DEBUG", "ACL2", "COMMON-LISP"), 2068("CELL-ERROR", "ACL2", "COMMON-LISP"), 2069("COMPILE-FILE", "ACL2", "COMMON-LISP"), 2070("DECF", "ACL2", "COMMON-LISP"), 2071("CELL-ERROR-NAME", "ACL2", "COMMON-LISP"), 2072("COMPILE-FILE-PATHNAME", "ACL2", "COMMON-LISP"), 2073("DECLAIM", "ACL2", "COMMON-LISP"), 2074("CERROR", "ACL2", "COMMON-LISP"), 2075("COMPILED-FUNCTION", "ACL2", "COMMON-LISP"), 2076("DECLARATION", "ACL2", "COMMON-LISP"), 2077("CHANGE-CLASS", "ACL2", "COMMON-LISP"), 2078("COMPILED-FUNCTION-P", "ACL2", "COMMON-LISP"), 2079("DECLARE", "ACL2", "COMMON-LISP"), 2080("CHAR", "ACL2", "COMMON-LISP"), 2081("COMPILER-MACRO", "ACL2", "COMMON-LISP"), 2082("DECODE-FLOAT", "ACL2", "COMMON-LISP"), 2083("CHAR-CODE", "ACL2", "COMMON-LISP"), 2084("COMPILER-MACRO-FUNCTION", "ACL2", "COMMON-LISP"), 2085("DECODE-UNIVERSAL-TIME", "ACL2", "COMMON-LISP"), 2086("CHAR-CODE-LIMIT", "ACL2", "COMMON-LISP"), 2087("COMPLEMENT", "ACL2", "COMMON-LISP"), 2088("DEFCLASS", "ACL2", "COMMON-LISP"), 2089("CHAR-DOWNCASE", "ACL2", "COMMON-LISP"), 2090("COMPLEX", "ACL2", "COMMON-LISP"), 2091("DEFCONSTANT", "ACL2", "COMMON-LISP"), 2092("CHAR-EQUAL", "ACL2", "COMMON-LISP"), 2093("COMPLEXP", "ACL2", "COMMON-LISP"), 2094("DEFGENERIC", "ACL2", "COMMON-LISP"), 2095("CHAR-GREATERP", "ACL2", "COMMON-LISP"), 2096("COMPUTE-APPLICABLE-METHODS", "ACL2", "COMMON-LISP"), 2097("DEFINE-COMPILER-MACRO", "ACL2", "COMMON-LISP"), 2098("CHAR-INT", "ACL2", "COMMON-LISP"), 2099("COMPUTE-RESTARTS", "ACL2", "COMMON-LISP"), 2100("DEFINE-CONDITION", "ACL2", "COMMON-LISP"), 2101("CHAR-LESSP", "ACL2", "COMMON-LISP"), 2102("CONCATENATE", "ACL2", "COMMON-LISP"), 2103("DEFINE-METHOD-COMBINATION", "ACL2", "COMMON-LISP"), 2104("CHAR-NAME", "ACL2", "COMMON-LISP"), 2105("CONCATENATED-STREAM", "ACL2", "COMMON-LISP"), 2106("DEFINE-MODIFY-MACRO", "ACL2", "COMMON-LISP"), 2107("CHAR-NOT-EQUAL", "ACL2", "COMMON-LISP"), 2108("CONCATENATED-STREAM-STREAMS", "ACL2", "COMMON-LISP"), 2109("DEFINE-SETF-EXPANDER", "ACL2", "COMMON-LISP"), 2110("CHAR-NOT-GREATERP", "ACL2", "COMMON-LISP"), 2111("COND", "ACL2", "COMMON-LISP"), 2112("DEFINE-SYMBOL-MACRO", "ACL2", "COMMON-LISP"), 2113("CHAR-NOT-LESSP", "ACL2", "COMMON-LISP"), 2114("CONDITION", "ACL2", "COMMON-LISP"), 2115("DEFMACRO", "ACL2", "COMMON-LISP"), 2116("CHAR-UPCASE", "ACL2", "COMMON-LISP"), 2117("CONJUGATE", "ACL2", "COMMON-LISP"), 2118("DEFMETHOD", "ACL2", "COMMON-LISP"), 2119("CHAR/=", "ACL2", "COMMON-LISP"), 2120("CONS", "ACL2", "COMMON-LISP"), 2121("DEFPACKAGE", "ACL2", "COMMON-LISP"), 2122("CHAR<", "ACL2", "COMMON-LISP"), 2123("CONSP", "ACL2", "COMMON-LISP"), 2124("DEFPARAMETER", "ACL2", "COMMON-LISP"), 2125("CHAR<=", "ACL2", "COMMON-LISP"), 2126("CONSTANTLY", "ACL2", "COMMON-LISP"), 2127("DEFSETF", "ACL2", "COMMON-LISP"), 2128("CHAR=", "ACL2", "COMMON-LISP"), 2129("CONSTANTP", "ACL2", "COMMON-LISP"), 2130("DEFSTRUCT", "ACL2", "COMMON-LISP"), 2131("CHAR>", "ACL2", "COMMON-LISP"), 2132("CONTINUE", "ACL2", "COMMON-LISP"), 2133("DEFTYPE", "ACL2", "COMMON-LISP"), 2134("CHAR>=", "ACL2", "COMMON-LISP"), 2135("CONTROL-ERROR", "ACL2", "COMMON-LISP"), 2136("DEFUN", "ACL2", "COMMON-LISP"), 2137("CHARACTER", "ACL2", "COMMON-LISP"), 2138("COPY-ALIST", "ACL2", "COMMON-LISP"), 2139("DEFVAR", "ACL2", "COMMON-LISP"), 2140("CHARACTERP", "ACL2", "COMMON-LISP"), 2141("COPY-LIST", "ACL2", "COMMON-LISP"), 2142("DELETE", "ACL2", "COMMON-LISP"), 2143("CHECK-TYPE", "ACL2", "COMMON-LISP"), 2144("COPY-PPRINT-DISPATCH", "ACL2", "COMMON-LISP"), 2145("DELETE-DUPLICATES", "ACL2", "COMMON-LISP"), 2146("CIS", "ACL2", "COMMON-LISP"), 2147("COPY-READTABLE", "ACL2", "COMMON-LISP"), 2148("DELETE-FILE", "ACL2", "COMMON-LISP"), 2149("CLASS", "ACL2", "COMMON-LISP"), 2150("COPY-SEQ", "ACL2", "COMMON-LISP"), 2151("DELETE-IF", "ACL2", "COMMON-LISP"), 2152("CLASS-NAME", "ACL2", "COMMON-LISP"), 2153("COPY-STRUCTURE", "ACL2", "COMMON-LISP"), 2154("DELETE-IF-NOT", "ACL2", "COMMON-LISP"), 2155("CLASS-OF", "ACL2", "COMMON-LISP"), 2156("COPY-SYMBOL", "ACL2", "COMMON-LISP"), 2157("DELETE-PACKAGE", "ACL2", "COMMON-LISP"), 2158("DENOMINATOR", "ACL2", "COMMON-LISP"), 2159("EQ", "ACL2", "COMMON-LISP"), 2160("DEPOSIT-FIELD", "ACL2", "COMMON-LISP"), 2161("EQL", "ACL2", "COMMON-LISP"), 2162("DESCRIBE", "ACL2", "COMMON-LISP"), 2163("EQUAL", "ACL2", "COMMON-LISP"), 2164("DESCRIBE-OBJECT", "ACL2", "COMMON-LISP"), 2165("EQUALP", "ACL2", "COMMON-LISP"), 2166("DESTRUCTURING-BIND", "ACL2", "COMMON-LISP"), 2167("ERROR", "ACL2", "COMMON-LISP"), 2168("DIGIT-CHAR", "ACL2", "COMMON-LISP"), 2169("ETYPECASE", "ACL2", "COMMON-LISP"), 2170("DIGIT-CHAR-P", "ACL2", "COMMON-LISP"), 2171("EVAL", "ACL2", "COMMON-LISP"), 2172("DIRECTORY", "ACL2", "COMMON-LISP"), 2173("EVAL-WHEN", "ACL2", "COMMON-LISP"), 2174("DIRECTORY-NAMESTRING", "ACL2", "COMMON-LISP"), 2175("EVENP", "ACL2", "COMMON-LISP"), 2176("DISASSEMBLE", "ACL2", "COMMON-LISP"), 2177("EVERY", "ACL2", "COMMON-LISP"), 2178("DIVISION-BY-ZERO", "ACL2", "COMMON-LISP"), 2179("EXP", "ACL2", "COMMON-LISP"), 2180("DO", "ACL2", "COMMON-LISP"), 2181("EXPORT", "ACL2", "COMMON-LISP"), 2182("DO*", "ACL2", "COMMON-LISP"), 2183("EXPT", "ACL2", "COMMON-LISP"), 2184("DO-ALL-SYMBOLS", "ACL2", "COMMON-LISP"), 2185("EXTENDED-CHAR", "ACL2", "COMMON-LISP"), 2186("DO-EXTERNAL-SYMBOLS", "ACL2", "COMMON-LISP"), 2187("FBOUNDP", "ACL2", "COMMON-LISP"), 2188("DO-SYMBOLS", "ACL2", "COMMON-LISP"), 2189("FCEILING", "ACL2", "COMMON-LISP"), 2190("DOCUMENTATION", "ACL2", "COMMON-LISP"), 2191("FDEFINITION", "ACL2", "COMMON-LISP"), 2192("DOLIST", "ACL2", "COMMON-LISP"), 2193("FFLOOR", "ACL2", "COMMON-LISP"), 2194("DOTIMES", "ACL2", "COMMON-LISP"), 2195("FIFTH", "ACL2", "COMMON-LISP"), 2196("DOUBLE-FLOAT", "ACL2", "COMMON-LISP"), 2197("FILE-AUTHOR", "ACL2", "COMMON-LISP"), 2198("DOUBLE-FLOAT-EPSILON", "ACL2", "COMMON-LISP"), 2199("FILE-ERROR", "ACL2", "COMMON-LISP"), 2200("DOUBLE-FLOAT-NEGATIVE-EPSILON", "ACL2", "COMMON-LISP"), 2201("FILE-ERROR-PATHNAME", "ACL2", "COMMON-LISP"), 2202("DPB", "ACL2", "COMMON-LISP"), 2203("FILE-LENGTH", "ACL2", "COMMON-LISP"), 2204("DRIBBLE", "ACL2", "COMMON-LISP"), 2205("FILE-NAMESTRING", "ACL2", "COMMON-LISP"), 2206("DYNAMIC-EXTENT", "ACL2", "COMMON-LISP"), 2207("FILE-POSITION", "ACL2", "COMMON-LISP"), 2208("ECASE", "ACL2", "COMMON-LISP"), 2209("FILE-STREAM", "ACL2", "COMMON-LISP"), 2210("ECHO-STREAM", "ACL2", "COMMON-LISP"), 2211("FILE-STRING-LENGTH", "ACL2", "COMMON-LISP"), 2212("ECHO-STREAM-INPUT-STREAM", "ACL2", "COMMON-LISP"), 2213("FILE-WRITE-DATE", "ACL2", "COMMON-LISP"), 2214("ECHO-STREAM-OUTPUT-STREAM", "ACL2", "COMMON-LISP"), 2215("FILL", "ACL2", "COMMON-LISP"), 2216("ED", "ACL2", "COMMON-LISP"), 2217("FILL-POINTER", "ACL2", "COMMON-LISP"), 2218("EIGHTH", "ACL2", "COMMON-LISP"), 2219("FIND", "ACL2", "COMMON-LISP"), 2220("ELT", "ACL2", "COMMON-LISP"), 2221("FIND-ALL-SYMBOLS", "ACL2", "COMMON-LISP"), 2222("ENCODE-UNIVERSAL-TIME", "ACL2", "COMMON-LISP"), 2223("FIND-CLASS", "ACL2", "COMMON-LISP"), 2224("END-OF-FILE", "ACL2", "COMMON-LISP"), 2225("FIND-IF", "ACL2", "COMMON-LISP"), 2226("ENDP", "ACL2", "COMMON-LISP"), 2227("FIND-IF-NOT", "ACL2", "COMMON-LISP"), 2228("ENOUGH-NAMESTRING", "ACL2", "COMMON-LISP"), 2229("FIND-METHOD", "ACL2", "COMMON-LISP"), 2230("ENSURE-DIRECTORIES-EXIST", "ACL2", "COMMON-LISP"), 2231("FIND-PACKAGE", "ACL2", "COMMON-LISP"), 2232("ENSURE-GENERIC-FUNCTION", "ACL2", "COMMON-LISP"), 2233("FIND-RESTART", "ACL2", "COMMON-LISP"), 2234("FIND-SYMBOL", "ACL2", "COMMON-LISP"), 2235("GET-INTERNAL-RUN-TIME", "ACL2", "COMMON-LISP"), 2236("FINISH-OUTPUT", "ACL2", "COMMON-LISP"), 2237("GET-MACRO-CHARACTER", "ACL2", "COMMON-LISP"), 2238("FIRST", "ACL2", "COMMON-LISP"), 2239("GET-OUTPUT-STREAM-STRING", "ACL2", "COMMON-LISP"), 2240("FIXNUM", "ACL2", "COMMON-LISP"), 2241("GET-PROPERTIES", "ACL2", "COMMON-LISP"), 2242("FLET", "ACL2", "COMMON-LISP"), 2243("GET-SETF-EXPANSION", "ACL2", "COMMON-LISP"), 2244("FLOAT", "ACL2", "COMMON-LISP"), 2245("GET-UNIVERSAL-TIME", "ACL2", "COMMON-LISP"), 2246("FLOAT-DIGITS", "ACL2", "COMMON-LISP"), 2247("GETF", "ACL2", "COMMON-LISP"), 2248("FLOAT-PRECISION", "ACL2", "COMMON-LISP"), 2249("GETHASH", "ACL2", "COMMON-LISP"), 2250("FLOAT-RADIX", "ACL2", "COMMON-LISP"), 2251("GO", "ACL2", "COMMON-LISP"), 2252("FLOAT-SIGN", "ACL2", "COMMON-LISP"), 2253("GRAPHIC-CHAR-P", "ACL2", "COMMON-LISP"), 2254("FLOATING-POINT-INEXACT", "ACL2", "COMMON-LISP"), 2255("HANDLER-BIND", "ACL2", "COMMON-LISP"), 2256("FLOATING-POINT-INVALID-OPERATION", "ACL2", "COMMON-LISP"), 2257("HANDLER-CASE", "ACL2", "COMMON-LISP"), 2258("FLOATING-POINT-OVERFLOW", "ACL2", "COMMON-LISP"), 2259("HASH-TABLE", "ACL2", "COMMON-LISP"), 2260("FLOATING-POINT-UNDERFLOW", "ACL2", "COMMON-LISP"), 2261("HASH-TABLE-COUNT", "ACL2", "COMMON-LISP"), 2262("FLOATP", "ACL2", "COMMON-LISP"), 2263("HASH-TABLE-P", "ACL2", "COMMON-LISP"), 2264("FLOOR", "ACL2", "COMMON-LISP"), 2265("HASH-TABLE-REHASH-SIZE", "ACL2", "COMMON-LISP"), 2266("FMAKUNBOUND", "ACL2", "COMMON-LISP"), 2267("HASH-TABLE-REHASH-THRESHOLD", "ACL2", "COMMON-LISP"), 2268("FORCE-OUTPUT", "ACL2", "COMMON-LISP"), 2269("HASH-TABLE-SIZE", "ACL2", "COMMON-LISP"), 2270("FORMAT", "ACL2", "COMMON-LISP"), 2271("HASH-TABLE-TEST", "ACL2", "COMMON-LISP"), 2272("FORMATTER", "ACL2", "COMMON-LISP"), 2273("HOST-NAMESTRING", "ACL2", "COMMON-LISP"), 2274("FOURTH", "ACL2", "COMMON-LISP"), 2275("IDENTITY", "ACL2", "COMMON-LISP"), 2276("FRESH-LINE", "ACL2", "COMMON-LISP"), 2277("IF", "ACL2", "COMMON-LISP"), 2278("FROUND", "ACL2", "COMMON-LISP"), 2279("IGNORABLE", "ACL2", "COMMON-LISP"), 2280("FTRUNCATE", "ACL2", "COMMON-LISP"), 2281("IGNORE", "ACL2", "COMMON-LISP"), 2282("FTYPE", "ACL2", "COMMON-LISP"), 2283("IGNORE-ERRORS", "ACL2", "COMMON-LISP"), 2284("FUNCALL", "ACL2", "COMMON-LISP"), 2285("IMAGPART", "ACL2", "COMMON-LISP"), 2286("FUNCTION", "ACL2", "COMMON-LISP"), 2287("IMPORT", "ACL2", "COMMON-LISP"), 2288("FUNCTION-KEYWORDS", "ACL2", "COMMON-LISP"), 2289("IN-PACKAGE", "ACL2", "COMMON-LISP"), 2290("FUNCTION-LAMBDA-EXPRESSION", "ACL2", "COMMON-LISP"), 2291("INCF", "ACL2", "COMMON-LISP"), 2292("FUNCTIONP", "ACL2", "COMMON-LISP"), 2293("INITIALIZE-INSTANCE", "ACL2", "COMMON-LISP"), 2294("GCD", "ACL2", "COMMON-LISP"), 2295("INLINE", "ACL2", "COMMON-LISP"), 2296("GENERIC-FUNCTION", "ACL2", "COMMON-LISP"), 2297("INPUT-STREAM-P", "ACL2", "COMMON-LISP"), 2298("GENSYM", "ACL2", "COMMON-LISP"), 2299("INSPECT", "ACL2", "COMMON-LISP"), 2300("GENTEMP", "ACL2", "COMMON-LISP"), 2301("INTEGER", "ACL2", "COMMON-LISP"), 2302("GET", "ACL2", "COMMON-LISP"), 2303("INTEGER-DECODE-FLOAT", "ACL2", "COMMON-LISP"), 2304("GET-DECODED-TIME", "ACL2", "COMMON-LISP"), 2305("INTEGER-LENGTH", "ACL2", "COMMON-LISP"), 2306("GET-DISPATCH-MACRO-CHARACTER", "ACL2", "COMMON-LISP"), 2307("INTEGERP", "ACL2", "COMMON-LISP"), 2308("GET-INTERNAL-REAL-TIME", "ACL2", "COMMON-LISP"), 2309("INTERACTIVE-STREAM-P", "ACL2", "COMMON-LISP"), 2310("INTERN", "ACL2", "COMMON-LISP"), 2311("LISP-IMPLEMENTATION-TYPE", "ACL2", "COMMON-LISP"), 2312("INTERNAL-TIME-UNITS-PER-SECOND", "ACL2", "COMMON-LISP"), 2313("LISP-IMPLEMENTATION-VERSION", "ACL2", "COMMON-LISP"), 2314("INTERSECTION", "ACL2", "COMMON-LISP"), 2315("LIST", "ACL2", "COMMON-LISP"), 2316("INVALID-METHOD-ERROR", "ACL2", "COMMON-LISP"), 2317("LIST*", "ACL2", "COMMON-LISP"), 2318("INVOKE-DEBUGGER", "ACL2", "COMMON-LISP"), 2319("LIST-ALL-PACKAGES", "ACL2", "COMMON-LISP"), 2320("INVOKE-RESTART", "ACL2", "COMMON-LISP"), 2321("LIST-LENGTH", "ACL2", "COMMON-LISP"), 2322("INVOKE-RESTART-INTERACTIVELY", "ACL2", "COMMON-LISP"), 2323("LISTEN", "ACL2", "COMMON-LISP"), 2324("ISQRT", "ACL2", "COMMON-LISP"), 2325("LISTP", "ACL2", "COMMON-LISP"), 2326("KEYWORD", "ACL2", "COMMON-LISP"), 2327("LOAD", "ACL2", "COMMON-LISP"), 2328("KEYWORDP", "ACL2", "COMMON-LISP"), 2329("LOAD-LOGICAL-PATHNAME-TRANSLATIONS", "ACL2", "COMMON-LISP"), 2330("LABELS", "ACL2", "COMMON-LISP"), 2331("LOAD-TIME-VALUE", "ACL2", "COMMON-LISP"), 2332("LAMBDA", "ACL2", "COMMON-LISP"), 2333("LOCALLY", "ACL2", "COMMON-LISP"), 2334("LAMBDA-LIST-KEYWORDS", "ACL2", "COMMON-LISP"), 2335("LOG", "ACL2", "COMMON-LISP"), 2336("LAMBDA-PARAMETERS-LIMIT", "ACL2", "COMMON-LISP"), 2337("LOGAND", "ACL2", "COMMON-LISP"), 2338("LAST", "ACL2", "COMMON-LISP"), 2339("LOGANDC1", "ACL2", "COMMON-LISP"), 2340("LCM", "ACL2", "COMMON-LISP"), 2341("LOGANDC2", "ACL2", "COMMON-LISP"), 2342("LDB", "ACL2", "COMMON-LISP"), 2343("LOGBITP", "ACL2", "COMMON-LISP"), 2344("LDB-TEST", "ACL2", "COMMON-LISP"), 2345("LOGCOUNT", "ACL2", "COMMON-LISP"), 2346("LDIFF", "ACL2", "COMMON-LISP"), 2347("LOGEQV", "ACL2", "COMMON-LISP"), 2348("LEAST-NEGATIVE-DOUBLE-FLOAT", "ACL2", "COMMON-LISP"), 2349("LOGICAL-PATHNAME", "ACL2", "COMMON-LISP"), 2350("LEAST-NEGATIVE-LONG-FLOAT", "ACL2", "COMMON-LISP"), 2351("LOGICAL-PATHNAME-TRANSLATIONS", "ACL2", "COMMON-LISP"), 2352("LEAST-NEGATIVE-NORMALIZED-DOUBLE-FLOAT", "ACL2", "COMMON-LISP"), 2353("LOGIOR", "ACL2", "COMMON-LISP"), 2354("LEAST-NEGATIVE-NORMALIZED-LONG-FLOAT", "ACL2", "COMMON-LISP"), 2355("LOGNAND", "ACL2", "COMMON-LISP"), 2356("LEAST-NEGATIVE-NORMALIZED-SHORT-FLOAT", "ACL2", "COMMON-LISP"), 2357("LOGNOR", "ACL2", "COMMON-LISP"), 2358("LEAST-NEGATIVE-NORMALIZED-SINGLE-FLOAT", "ACL2", "COMMON-LISP"), 2359("LOGNOT", "ACL2", "COMMON-LISP"), 2360("LEAST-NEGATIVE-SHORT-FLOAT", "ACL2", "COMMON-LISP"), 2361("LOGORC1", "ACL2", "COMMON-LISP"), 2362("LEAST-NEGATIVE-SINGLE-FLOAT", "ACL2", "COMMON-LISP"), 2363("LOGORC2", "ACL2", "COMMON-LISP"), 2364("LEAST-POSITIVE-DOUBLE-FLOAT", "ACL2", "COMMON-LISP"), 2365("LOGTEST", "ACL2", "COMMON-LISP"), 2366("LEAST-POSITIVE-LONG-FLOAT", "ACL2", "COMMON-LISP"), 2367("LOGXOR", "ACL2", "COMMON-LISP"), 2368("LEAST-POSITIVE-NORMALIZED-DOUBLE-FLOAT", "ACL2", "COMMON-LISP"), 2369("LONG-FLOAT", "ACL2", "COMMON-LISP"), 2370("LEAST-POSITIVE-NORMALIZED-LONG-FLOAT", "ACL2", "COMMON-LISP"), 2371("LONG-FLOAT-EPSILON", "ACL2", "COMMON-LISP"), 2372("LEAST-POSITIVE-NORMALIZED-SHORT-FLOAT", "ACL2", "COMMON-LISP"), 2373("LONG-FLOAT-NEGATIVE-EPSILON", "ACL2", "COMMON-LISP"), 2374("LEAST-POSITIVE-NORMALIZED-SINGLE-FLOAT", "ACL2", "COMMON-LISP"), 2375("LONG-SITE-NAME", "ACL2", "COMMON-LISP"), 2376("LEAST-POSITIVE-SHORT-FLOAT", "ACL2", "COMMON-LISP"), 2377("LOOP", "ACL2", "COMMON-LISP"), 2378("LEAST-POSITIVE-SINGLE-FLOAT", "ACL2", "COMMON-LISP"), 2379("LOOP-FINISH", "ACL2", "COMMON-LISP"), 2380("LENGTH", "ACL2", "COMMON-LISP"), 2381("LOWER-CASE-P", "ACL2", "COMMON-LISP"), 2382("LET", "ACL2", "COMMON-LISP"), 2383("MACHINE-INSTANCE", "ACL2", "COMMON-LISP"), 2384("LET*", "ACL2", "COMMON-LISP"), 2385("MACHINE-TYPE", "ACL2", "COMMON-LISP"), 2386("MACHINE-VERSION", "ACL2", "COMMON-LISP"), 2387("MASK-FIELD", "ACL2", "COMMON-LISP"), 2388("MACRO-FUNCTION", "ACL2", "COMMON-LISP"), 2389("MAX", "ACL2", "COMMON-LISP"), 2390("MACROEXPAND", "ACL2", "COMMON-LISP"), 2391("MEMBER", "ACL2", "COMMON-LISP"), 2392("MACROEXPAND-1", "ACL2", "COMMON-LISP"), 2393("MEMBER-IF", "ACL2", "COMMON-LISP"), 2394("MACROLET", "ACL2", "COMMON-LISP"), 2395("MEMBER-IF-NOT", "ACL2", "COMMON-LISP"), 2396("MAKE-ARRAY", "ACL2", "COMMON-LISP"), 2397("MERGE", "ACL2", "COMMON-LISP"), 2398("MAKE-BROADCAST-STREAM", "ACL2", "COMMON-LISP"), 2399("MERGE-PATHNAMES", "ACL2", "COMMON-LISP"), 2400("MAKE-CONCATENATED-STREAM", "ACL2", "COMMON-LISP"), 2401("METHOD", "ACL2", "COMMON-LISP"), 2402("MAKE-CONDITION", "ACL2", "COMMON-LISP"), 2403("METHOD-COMBINATION", "ACL2", "COMMON-LISP"), 2404("MAKE-DISPATCH-MACRO-CHARACTER", "ACL2", "COMMON-LISP"), 2405("METHOD-COMBINATION-ERROR", "ACL2", "COMMON-LISP"), 2406("MAKE-ECHO-STREAM", "ACL2", "COMMON-LISP"), 2407("METHOD-QUALIFIERS", "ACL2", "COMMON-LISP"), 2408("MAKE-HASH-TABLE", "ACL2", "COMMON-LISP"), 2409("MIN", "ACL2", "COMMON-LISP"), 2410("MAKE-INSTANCE", "ACL2", "COMMON-LISP"), 2411("MINUSP", "ACL2", "COMMON-LISP"), 2412("MAKE-INSTANCES-OBSOLETE", "ACL2", "COMMON-LISP"), 2413("MISMATCH", "ACL2", "COMMON-LISP"), 2414("MAKE-LIST", "ACL2", "COMMON-LISP"), 2415("MOD", "ACL2", "COMMON-LISP"), 2416("MAKE-LOAD-FORM", "ACL2", "COMMON-LISP"), 2417("MOST-NEGATIVE-DOUBLE-FLOAT", "ACL2", "COMMON-LISP"), 2418("MAKE-LOAD-FORM-SAVING-SLOTS", "ACL2", "COMMON-LISP"), 2419("MOST-NEGATIVE-FIXNUM", "ACL2", "COMMON-LISP"), 2420("MAKE-METHOD", "ACL2", "COMMON-LISP"), 2421("MOST-NEGATIVE-LONG-FLOAT", "ACL2", "COMMON-LISP"), 2422("MAKE-PACKAGE", "ACL2", "COMMON-LISP"), 2423("MOST-NEGATIVE-SHORT-FLOAT", "ACL2", "COMMON-LISP"), 2424("MAKE-PATHNAME", "ACL2", "COMMON-LISP"), 2425("MOST-NEGATIVE-SINGLE-FLOAT", "ACL2", "COMMON-LISP"), 2426("MAKE-RANDOM-STATE", "ACL2", "COMMON-LISP"), 2427("MOST-POSITIVE-DOUBLE-FLOAT", "ACL2", "COMMON-LISP"), 2428("MAKE-SEQUENCE", "ACL2", "COMMON-LISP"), 2429("MOST-POSITIVE-FIXNUM", "ACL2", "COMMON-LISP"), 2430("MAKE-STRING", "ACL2", "COMMON-LISP"), 2431("MOST-POSITIVE-LONG-FLOAT", "ACL2", "COMMON-LISP"), 2432("MAKE-STRING-INPUT-STREAM", "ACL2", "COMMON-LISP"), 2433("MOST-POSITIVE-SHORT-FLOAT", "ACL2", "COMMON-LISP"), 2434("MAKE-STRING-OUTPUT-STREAM", "ACL2", "COMMON-LISP"), 2435("MOST-POSITIVE-SINGLE-FLOAT", "ACL2", "COMMON-LISP"), 2436("MAKE-SYMBOL", "ACL2", "COMMON-LISP"), 2437("MUFFLE-WARNING", "ACL2", "COMMON-LISP"), 2438("MAKE-SYNONYM-STREAM", "ACL2", "COMMON-LISP"), 2439("MULTIPLE-VALUE-BIND", "ACL2", "COMMON-LISP"), 2440("MAKE-TWO-WAY-STREAM", "ACL2", "COMMON-LISP"), 2441("MULTIPLE-VALUE-CALL", "ACL2", "COMMON-LISP"), 2442("MAKUNBOUND", "ACL2", "COMMON-LISP"), 2443("MULTIPLE-VALUE-LIST", "ACL2", "COMMON-LISP"), 2444("MAP", "ACL2", "COMMON-LISP"), 2445("MULTIPLE-VALUE-PROG1", "ACL2", "COMMON-LISP"), 2446("MAP-INTO", "ACL2", "COMMON-LISP"), 2447("MULTIPLE-VALUE-SETQ", "ACL2", "COMMON-LISP"), 2448("MAPC", "ACL2", "COMMON-LISP"), 2449("MULTIPLE-VALUES-LIMIT", "ACL2", "COMMON-LISP"), 2450("MAPCAN", "ACL2", "COMMON-LISP"), 2451("NAME-CHAR", "ACL2", "COMMON-LISP"), 2452("MAPCAR", "ACL2", "COMMON-LISP"), 2453("NAMESTRING", "ACL2", "COMMON-LISP"), 2454("MAPCON", "ACL2", "COMMON-LISP"), 2455("NBUTLAST", "ACL2", "COMMON-LISP"), 2456("MAPHASH", "ACL2", "COMMON-LISP"), 2457("NCONC", "ACL2", "COMMON-LISP"), 2458("MAPL", "ACL2", "COMMON-LISP"), 2459("NEXT-METHOD-P", "ACL2", "COMMON-LISP"), 2460("MAPLIST", "ACL2", "COMMON-LISP"), 2461("NIL", "ACL2", "COMMON-LISP"), 2462("NINTERSECTION", "ACL2", "COMMON-LISP"), 2463("PACKAGE-ERROR", "ACL2", "COMMON-LISP"), 2464("NINTH", "ACL2", "COMMON-LISP"), 2465("PACKAGE-ERROR-PACKAGE", "ACL2", "COMMON-LISP"), 2466("NO-APPLICABLE-METHOD", "ACL2", "COMMON-LISP"), 2467("PACKAGE-NAME", "ACL2", "COMMON-LISP"), 2468("NO-NEXT-METHOD", "ACL2", "COMMON-LISP"), 2469("PACKAGE-NICKNAMES", "ACL2", "COMMON-LISP"), 2470("NOT", "ACL2", "COMMON-LISP"), 2471("PACKAGE-SHADOWING-SYMBOLS", "ACL2", "COMMON-LISP"), 2472("NOTANY", "ACL2", "COMMON-LISP"), 2473("PACKAGE-USE-LIST", "ACL2", "COMMON-LISP"), 2474("NOTEVERY", "ACL2", "COMMON-LISP"), 2475("PACKAGE-USED-BY-LIST", "ACL2", "COMMON-LISP"), 2476("NOTINLINE", "ACL2", "COMMON-LISP"), 2477("PACKAGEP", "ACL2", "COMMON-LISP"), 2478("NRECONC", "ACL2", "COMMON-LISP"), 2479("PAIRLIS", "ACL2", "COMMON-LISP"), 2480("NREVERSE", "ACL2", "COMMON-LISP"), 2481("PARSE-ERROR", "ACL2", "COMMON-LISP"), 2482("NSET-DIFFERENCE", "ACL2", "COMMON-LISP"), 2483("PARSE-INTEGER", "ACL2", "COMMON-LISP"), 2484("NSET-EXCLUSIVE-OR", "ACL2", "COMMON-LISP"), 2485("PARSE-NAMESTRING", "ACL2", "COMMON-LISP"), 2486("NSTRING-CAPITALIZE", "ACL2", "COMMON-LISP"), 2487("PATHNAME", "ACL2", "COMMON-LISP"), 2488("NSTRING-DOWNCASE", "ACL2", "COMMON-LISP"), 2489("PATHNAME-DEVICE", "ACL2", "COMMON-LISP"), 2490("NSTRING-UPCASE", "ACL2", "COMMON-LISP"), 2491("PATHNAME-DIRECTORY", "ACL2", "COMMON-LISP"), 2492("NSUBLIS", "ACL2", "COMMON-LISP"), 2493("PATHNAME-HOST", "ACL2", "COMMON-LISP"), 2494("NSUBST", "ACL2", "COMMON-LISP"), 2495("PATHNAME-MATCH-P", "ACL2", "COMMON-LISP"), 2496("NSUBST-IF", "ACL2", "COMMON-LISP"), 2497("PATHNAME-NAME", "ACL2", "COMMON-LISP"), 2498("NSUBST-IF-NOT", "ACL2", "COMMON-LISP"), 2499("PATHNAME-TYPE", "ACL2", "COMMON-LISP"), 2500("NSUBSTITUTE", "ACL2", "COMMON-LISP"), 2501("PATHNAME-VERSION", "ACL2", "COMMON-LISP"), 2502("NSUBSTITUTE-IF", "ACL2", "COMMON-LISP"), 2503("PATHNAMEP", "ACL2", "COMMON-LISP"), 2504("NSUBSTITUTE-IF-NOT", "ACL2", "COMMON-LISP"), 2505("PEEK-CHAR", "ACL2", "COMMON-LISP"), 2506("NTH", "ACL2", "COMMON-LISP"), 2507("PHASE", "ACL2", "COMMON-LISP"), 2508("NTH-VALUE", "ACL2", "COMMON-LISP"), 2509("PI", "ACL2", "COMMON-LISP"), 2510("NTHCDR", "ACL2", "COMMON-LISP"), 2511("PLUSP", "ACL2", "COMMON-LISP"), 2512("NULL", "ACL2", "COMMON-LISP"), 2513("POP", "ACL2", "COMMON-LISP"), 2514("NUMBER", "ACL2", "COMMON-LISP"), 2515("POSITION", "ACL2", "COMMON-LISP"), 2516("NUMBERP", "ACL2", "COMMON-LISP"), 2517("POSITION-IF", "ACL2", "COMMON-LISP"), 2518("NUMERATOR", "ACL2", "COMMON-LISP"), 2519("POSITION-IF-NOT", "ACL2", "COMMON-LISP"), 2520("NUNION", "ACL2", "COMMON-LISP"), 2521("PPRINT", "ACL2", "COMMON-LISP"), 2522("ODDP", "ACL2", "COMMON-LISP"), 2523("PPRINT-DISPATCH", "ACL2", "COMMON-LISP"), 2524("OPEN", "ACL2", "COMMON-LISP"), 2525("PPRINT-EXIT-IF-LIST-EXHAUSTED", "ACL2", "COMMON-LISP"), 2526("OPEN-STREAM-P", "ACL2", "COMMON-LISP"), 2527("PPRINT-FILL", "ACL2", "COMMON-LISP"), 2528("OPTIMIZE", "ACL2", "COMMON-LISP"), 2529("PPRINT-INDENT", "ACL2", "COMMON-LISP"), 2530("OR", "ACL2", "COMMON-LISP"), 2531("PPRINT-LINEAR", "ACL2", "COMMON-LISP"), 2532("OTHERWISE", "ACL2", "COMMON-LISP"), 2533("PPRINT-LOGICAL-BLOCK", "ACL2", "COMMON-LISP"), 2534("OUTPUT-STREAM-P", "ACL2", "COMMON-LISP"), 2535("PPRINT-NEWLINE", "ACL2", "COMMON-LISP"), 2536("PACKAGE", "ACL2", "COMMON-LISP"), 2537("PPRINT-POP", "ACL2", "COMMON-LISP"), 2538("PPRINT-TAB", "ACL2", "COMMON-LISP"), 2539("READ-CHAR", "ACL2", "COMMON-LISP"), 2540("PPRINT-TABULAR", "ACL2", "COMMON-LISP"), 2541("READ-CHAR-NO-HANG", "ACL2", "COMMON-LISP"), 2542("PRIN1", "ACL2", "COMMON-LISP"), 2543("READ-DELIMITED-LIST", "ACL2", "COMMON-LISP"), 2544("PRIN1-TO-STRING", "ACL2", "COMMON-LISP"), 2545("READ-FROM-STRING", "ACL2", "COMMON-LISP"), 2546("PRINC", "ACL2", "COMMON-LISP"), 2547("READ-LINE", "ACL2", "COMMON-LISP"), 2548("PRINC-TO-STRING", "ACL2", "COMMON-LISP"), 2549("READ-PRESERVING-WHITESPACE", "ACL2", "COMMON-LISP"), 2550("PRINT", "ACL2", "COMMON-LISP"), 2551("READ-SEQUENCE", "ACL2", "COMMON-LISP"), 2552("PRINT-NOT-READABLE", "ACL2", "COMMON-LISP"), 2553("READER-ERROR", "ACL2", "COMMON-LISP"), 2554("PRINT-NOT-READABLE-OBJECT", "ACL2", "COMMON-LISP"), 2555("READTABLE", "ACL2", "COMMON-LISP"), 2556("PRINT-OBJECT", "ACL2", "COMMON-LISP"), 2557("READTABLE-CASE", "ACL2", "COMMON-LISP"), 2558("PRINT-UNREADABLE-OBJECT", "ACL2", "COMMON-LISP"), 2559("READTABLEP", "ACL2", "COMMON-LISP"), 2560("PROBE-FILE", "ACL2", "COMMON-LISP"), 2561("REAL", "ACL2", "COMMON-LISP"), 2562("PROCLAIM", "ACL2", "COMMON-LISP"), 2563("REALP", "ACL2", "COMMON-LISP"), 2564("PROG", "ACL2", "COMMON-LISP"), 2565("REALPART", "ACL2", "COMMON-LISP"), 2566("PROG*", "ACL2", "COMMON-LISP"), 2567("REDUCE", "ACL2", "COMMON-LISP"), 2568("PROG1", "ACL2", "COMMON-LISP"), 2569("REINITIALIZE-INSTANCE", "ACL2", "COMMON-LISP"), 2570("PROG2", "ACL2", "COMMON-LISP"), 2571("REM", "ACL2", "COMMON-LISP"), 2572("PROGN", "ACL2", "COMMON-LISP"), 2573("REMF", "ACL2", "COMMON-LISP"), 2574("PROGRAM-ERROR", "ACL2", "COMMON-LISP"), 2575("REMHASH", "ACL2", "COMMON-LISP"), 2576("PROGV", "ACL2", "COMMON-LISP"), 2577("REMOVE", "ACL2", "COMMON-LISP"), 2578("PROVIDE", "ACL2", "COMMON-LISP"), 2579("REMOVE-DUPLICATES", "ACL2", "COMMON-LISP"), 2580("PSETF", "ACL2", "COMMON-LISP"), 2581("REMOVE-IF", "ACL2", "COMMON-LISP"), 2582("PSETQ", "ACL2", "COMMON-LISP"), 2583("REMOVE-IF-NOT", "ACL2", "COMMON-LISP"), 2584("PUSH", "ACL2", "COMMON-LISP"), 2585("REMOVE-METHOD", "ACL2", "COMMON-LISP"), 2586("PUSHNEW", "ACL2", "COMMON-LISP"), 2587("REMPROP", "ACL2", "COMMON-LISP"), 2588("QUOTE", "ACL2", "COMMON-LISP"), 2589("RENAME-FILE", "ACL2", "COMMON-LISP"), 2590("RANDOM", "ACL2", "COMMON-LISP"), 2591("RENAME-PACKAGE", "ACL2", "COMMON-LISP"), 2592("RANDOM-STATE", "ACL2", "COMMON-LISP"), 2593("REPLACE", "ACL2", "COMMON-LISP"), 2594("RANDOM-STATE-P", "ACL2", "COMMON-LISP"), 2595("REQUIRE", "ACL2", "COMMON-LISP"), 2596("RASSOC", "ACL2", "COMMON-LISP"), 2597("REST", "ACL2", "COMMON-LISP"), 2598("RASSOC-IF", "ACL2", "COMMON-LISP"), 2599("RESTART", "ACL2", "COMMON-LISP"), 2600("RASSOC-IF-NOT", "ACL2", "COMMON-LISP"), 2601("RESTART-BIND", "ACL2", "COMMON-LISP"), 2602("RATIO", "ACL2", "COMMON-LISP"), 2603("RESTART-CASE", "ACL2", "COMMON-LISP"), 2604("RATIONAL", "ACL2", "COMMON-LISP"), 2605("RESTART-NAME", "ACL2", "COMMON-LISP"), 2606("RATIONALIZE", "ACL2", "COMMON-LISP"), 2607("RETURN", "ACL2", "COMMON-LISP"), 2608("RATIONALP", "ACL2", "COMMON-LISP"), 2609("RETURN-FROM", "ACL2", "COMMON-LISP"), 2610("READ", "ACL2", "COMMON-LISP"), 2611("REVAPPEND", "ACL2", "COMMON-LISP"), 2612("READ-BYTE", "ACL2", "COMMON-LISP"), 2613("REVERSE", "ACL2", "COMMON-LISP"), 2614("ROOM", "ACL2", "COMMON-LISP"), 2615("SIMPLE-BIT-VECTOR", "ACL2", "COMMON-LISP"), 2616("ROTATEF", "ACL2", "COMMON-LISP"), 2617("SIMPLE-BIT-VECTOR-P", "ACL2", "COMMON-LISP"), 2618("ROUND", "ACL2", "COMMON-LISP"), 2619("SIMPLE-CONDITION", "ACL2", "COMMON-LISP"), 2620("ROW-MAJOR-AREF", "ACL2", "COMMON-LISP"), 2621("SIMPLE-CONDITION-FORMAT-ARGUMENTS", "ACL2", "COMMON-LISP"), 2622("RPLACA", "ACL2", "COMMON-LISP"), 2623("SIMPLE-CONDITION-FORMAT-CONTROL", "ACL2", "COMMON-LISP"), 2624("RPLACD", "ACL2", "COMMON-LISP"), 2625("SIMPLE-ERROR", "ACL2", "COMMON-LISP"), 2626("SAFETY", "ACL2", "COMMON-LISP"), 2627("SIMPLE-STRING", "ACL2", "COMMON-LISP"), 2628("SATISFIES", "ACL2", "COMMON-LISP"), 2629("SIMPLE-STRING-P", "ACL2", "COMMON-LISP"), 2630("SBIT", "ACL2", "COMMON-LISP"), 2631("SIMPLE-TYPE-ERROR", "ACL2", "COMMON-LISP"), 2632("SCALE-FLOAT", "ACL2", "COMMON-LISP"), 2633("SIMPLE-VECTOR", "ACL2", "COMMON-LISP"), 2634("SCHAR", "ACL2", "COMMON-LISP"), 2635("SIMPLE-VECTOR-P", "ACL2", "COMMON-LISP"), 2636("SEARCH", "ACL2", "COMMON-LISP"), 2637("SIMPLE-WARNING", "ACL2", "COMMON-LISP"), 2638("SECOND", "ACL2", "COMMON-LISP"), 2639("SIN", "ACL2", "COMMON-LISP"), 2640("SEQUENCE", "ACL2", "COMMON-LISP"), 2641("SINGLE-FLOAT", "ACL2", "COMMON-LISP"), 2642("SERIOUS-CONDITION", "ACL2", "COMMON-LISP"), 2643("SINGLE-FLOAT-EPSILON", "ACL2", "COMMON-LISP"), 2644("SET", "ACL2", "COMMON-LISP"), 2645("SINGLE-FLOAT-NEGATIVE-EPSILON", "ACL2", "COMMON-LISP"), 2646("SET-DIFFERENCE", "ACL2", "COMMON-LISP"), 2647("SINH", "ACL2", "COMMON-LISP"), 2648("SET-DISPATCH-MACRO-CHARACTER", "ACL2", "COMMON-LISP"), 2649("SIXTH", "ACL2", "COMMON-LISP"), 2650("SET-EXCLUSIVE-OR", "ACL2", "COMMON-LISP"), 2651("SLEEP", "ACL2", "COMMON-LISP"), 2652("SET-MACRO-CHARACTER", "ACL2", "COMMON-LISP"), 2653("SLOT-BOUNDP", "ACL2", "COMMON-LISP"), 2654("SET-PPRINT-DISPATCH", "ACL2", "COMMON-LISP"), 2655("SLOT-EXISTS-P", "ACL2", "COMMON-LISP"), 2656("SET-SYNTAX-FROM-CHAR", "ACL2", "COMMON-LISP"), 2657("SLOT-MAKUNBOUND", "ACL2", "COMMON-LISP"), 2658("SETF", "ACL2", "COMMON-LISP"), 2659("SLOT-MISSING", "ACL2", "COMMON-LISP"), 2660("SETQ", "ACL2", "COMMON-LISP"), 2661("SLOT-UNBOUND", "ACL2", "COMMON-LISP"), 2662("SEVENTH", "ACL2", "COMMON-LISP"), 2663("SLOT-VALUE", "ACL2", "COMMON-LISP"), 2664("SHADOW", "ACL2", "COMMON-LISP"), 2665("SOFTWARE-TYPE", "ACL2", "COMMON-LISP"), 2666("SHADOWING-IMPORT", "ACL2", "COMMON-LISP"), 2667("SOFTWARE-VERSION", "ACL2", "COMMON-LISP"), 2668("SHARED-INITIALIZE", "ACL2", "COMMON-LISP"), 2669("SOME", "ACL2", "COMMON-LISP"), 2670("SHIFTF", "ACL2", "COMMON-LISP"), 2671("SORT", "ACL2", "COMMON-LISP"), 2672("SHORT-FLOAT", "ACL2", "COMMON-LISP"), 2673("SPACE", "ACL2", "COMMON-LISP"), 2674("SHORT-FLOAT-EPSILON", "ACL2", "COMMON-LISP"), 2675("SPECIAL", "ACL2", "COMMON-LISP"), 2676("SHORT-FLOAT-NEGATIVE-EPSILON", "ACL2", "COMMON-LISP"), 2677("SPECIAL-OPERATOR-P", "ACL2", "COMMON-LISP"), 2678("SHORT-SITE-NAME", "ACL2", "COMMON-LISP"), 2679("SPEED", "ACL2", "COMMON-LISP"), 2680("SIGNAL", "ACL2", "COMMON-LISP"), 2681("SQRT", "ACL2", "COMMON-LISP"), 2682("SIGNED-BYTE", "ACL2", "COMMON-LISP"), 2683("STABLE-SORT", "ACL2", "COMMON-LISP"), 2684("SIGNUM", "ACL2", "COMMON-LISP"), 2685("STANDARD", "ACL2", "COMMON-LISP"), 2686("SIMPLE-ARRAY", "ACL2", "COMMON-LISP"), 2687("STANDARD-CHAR", "ACL2", "COMMON-LISP"), 2688("SIMPLE-BASE-STRING", "ACL2", "COMMON-LISP"), 2689("STANDARD-CHAR-P", "ACL2", "COMMON-LISP"), 2690("STANDARD-CLASS", "ACL2", "COMMON-LISP"), 2691("SUBLIS", "ACL2", "COMMON-LISP"), 2692("STANDARD-GENERIC-FUNCTION", "ACL2", "COMMON-LISP"), 2693("SUBSEQ", "ACL2", "COMMON-LISP"), 2694("STANDARD-METHOD", "ACL2", "COMMON-LISP"), 2695("SUBSETP", "ACL2", "COMMON-LISP"), 2696("STANDARD-OBJECT", "ACL2", "COMMON-LISP"), 2697("SUBST", "ACL2", "COMMON-LISP"), 2698("STEP", "ACL2", "COMMON-LISP"), 2699("SUBST-IF", "ACL2", "COMMON-LISP"), 2700("STORAGE-CONDITION", "ACL2", "COMMON-LISP"), 2701("SUBST-IF-NOT", "ACL2", "COMMON-LISP"), 2702("STORE-VALUE", "ACL2", "COMMON-LISP"), 2703("SUBSTITUTE", "ACL2", "COMMON-LISP"), 2704("STREAM", "ACL2", "COMMON-LISP"), 2705("SUBSTITUTE-IF", "ACL2", "COMMON-LISP"), 2706("STREAM-ELEMENT-TYPE", "ACL2", "COMMON-LISP"), 2707("SUBSTITUTE-IF-NOT", "ACL2", "COMMON-LISP"), 2708("STREAM-ERROR", "ACL2", "COMMON-LISP"), 2709("SUBTYPEP", "ACL2", "COMMON-LISP"), 2710("STREAM-ERROR-STREAM", "ACL2", "COMMON-LISP"), 2711("SVREF", "ACL2", "COMMON-LISP"), 2712("STREAM-EXTERNAL-FORMAT", "ACL2", "COMMON-LISP"), 2713("SXHASH", "ACL2", "COMMON-LISP"), 2714("STREAMP", "ACL2", "COMMON-LISP"), 2715("SYMBOL", "ACL2", "COMMON-LISP"), 2716("STRING", "ACL2", "COMMON-LISP"), 2717("SYMBOL-FUNCTION", "ACL2", "COMMON-LISP"), 2718("STRING-CAPITALIZE", "ACL2", "COMMON-LISP"), 2719("SYMBOL-MACROLET", "ACL2", "COMMON-LISP"), 2720("STRING-DOWNCASE", "ACL2", "COMMON-LISP"), 2721("SYMBOL-NAME", "ACL2", "COMMON-LISP"), 2722("STRING-EQUAL", "ACL2", "COMMON-LISP"), 2723("SYMBOL-PACKAGE", "ACL2", "COMMON-LISP"), 2724("STRING-GREATERP", "ACL2", "COMMON-LISP"), 2725("SYMBOL-PLIST", "ACL2", "COMMON-LISP"), 2726("STRING-LEFT-TRIM", "ACL2", "COMMON-LISP"), 2727("SYMBOL-VALUE", "ACL2", "COMMON-LISP"), 2728("STRING-LESSP", "ACL2", "COMMON-LISP"), 2729("SYMBOLP", "ACL2", "COMMON-LISP"), 2730("STRING-NOT-EQUAL", "ACL2", "COMMON-LISP"), 2731("SYNONYM-STREAM", "ACL2", "COMMON-LISP"), 2732("STRING-NOT-GREATERP", "ACL2", "COMMON-LISP"), 2733("SYNONYM-STREAM-SYMBOL", "ACL2", "COMMON-LISP"), 2734("STRING-NOT-LESSP", "ACL2", "COMMON-LISP"), 2735("T", "ACL2", "COMMON-LISP"), 2736("STRING-RIGHT-TRIM", "ACL2", "COMMON-LISP"), 2737("TAGBODY", "ACL2", "COMMON-LISP"), 2738("STRING-STREAM", "ACL2", "COMMON-LISP"), 2739("TAILP", "ACL2", "COMMON-LISP"), 2740("STRING-TRIM", "ACL2", "COMMON-LISP"), 2741("TAN", "ACL2", "COMMON-LISP"), 2742("STRING-UPCASE", "ACL2", "COMMON-LISP"), 2743("TANH", "ACL2", "COMMON-LISP"), 2744("STRING/=", "ACL2", "COMMON-LISP"), 2745("TENTH", "ACL2", "COMMON-LISP"), 2746("STRING<", "ACL2", "COMMON-LISP"), 2747("TERPRI", "ACL2", "COMMON-LISP"), 2748("STRING<=", "ACL2", "COMMON-LISP"), 2749("THE", "ACL2", "COMMON-LISP"), 2750("STRING=", "ACL2", "COMMON-LISP"), 2751("THIRD", "ACL2", "COMMON-LISP"), 2752("STRING>", "ACL2", "COMMON-LISP"), 2753("THROW", "ACL2", "COMMON-LISP"), 2754("STRING>=", "ACL2", "COMMON-LISP"), 2755("TIME", "ACL2", "COMMON-LISP"), 2756("STRINGP", "ACL2", "COMMON-LISP"), 2757("TRACE", "ACL2", "COMMON-LISP"), 2758("STRUCTURE", "ACL2", "COMMON-LISP"), 2759("TRANSLATE-LOGICAL-PATHNAME", "ACL2", "COMMON-LISP"), 2760("STRUCTURE-CLASS", "ACL2", "COMMON-LISP"), 2761("TRANSLATE-PATHNAME", "ACL2", "COMMON-LISP"), 2762("STRUCTURE-OBJECT", "ACL2", "COMMON-LISP"), 2763("TREE-EQUAL", "ACL2", "COMMON-LISP"), 2764("STYLE-WARNING", "ACL2", "COMMON-LISP"), 2765("TRUENAME", "ACL2", "COMMON-LISP"), 2766("TRUNCATE", "ACL2", "COMMON-LISP"), 2767("VALUES-LIST", "ACL2", "COMMON-LISP"), 2768("TWO-WAY-STREAM", "ACL2", "COMMON-LISP"), 2769("VARIABLE", "ACL2", "COMMON-LISP"), 2770("TWO-WAY-STREAM-INPUT-STREAM", "ACL2", "COMMON-LISP"), 2771("VECTOR", "ACL2", "COMMON-LISP"), 2772("TWO-WAY-STREAM-OUTPUT-STREAM", "ACL2", "COMMON-LISP"), 2773("VECTOR-POP", "ACL2", "COMMON-LISP"), 2774("TYPE", "ACL2", "COMMON-LISP"), 2775("VECTOR-PUSH", "ACL2", "COMMON-LISP"), 2776("TYPE-ERROR", "ACL2", "COMMON-LISP"), 2777("VECTOR-PUSH-EXTEND", "ACL2", "COMMON-LISP"), 2778("TYPE-ERROR-DATUM", "ACL2", "COMMON-LISP"), 2779("VECTORP", "ACL2", "COMMON-LISP"), 2780("TYPE-ERROR-EXPECTED-TYPE", "ACL2", "COMMON-LISP"), 2781("WARN", "ACL2", "COMMON-LISP"), 2782("TYPE-OF", "ACL2", "COMMON-LISP"), 2783("WARNING", "ACL2", "COMMON-LISP"), 2784("TYPECASE", "ACL2", "COMMON-LISP"), 2785("WHEN", "ACL2", "COMMON-LISP"), 2786("TYPEP", "ACL2", "COMMON-LISP"), 2787("WILD-PATHNAME-P", "ACL2", "COMMON-LISP"), 2788("UNBOUND-SLOT", "ACL2", "COMMON-LISP"), 2789("WITH-ACCESSORS", "ACL2", "COMMON-LISP"), 2790("UNBOUND-SLOT-INSTANCE", "ACL2", "COMMON-LISP"), 2791("WITH-COMPILATION-UNIT", "ACL2", "COMMON-LISP"), 2792("UNBOUND-VARIABLE", "ACL2", "COMMON-LISP"), 2793("WITH-CONDITION-RESTARTS", "ACL2", "COMMON-LISP"), 2794("UNDEFINED-FUNCTION", "ACL2", "COMMON-LISP"), 2795("WITH-HASH-TABLE-ITERATOR", "ACL2", "COMMON-LISP"), 2796("UNEXPORT", "ACL2", "COMMON-LISP"), 2797("WITH-INPUT-FROM-STRING", "ACL2", "COMMON-LISP"), 2798("UNINTERN", "ACL2", "COMMON-LISP"), 2799("WITH-OPEN-FILE", "ACL2", "COMMON-LISP"), 2800("UNION", "ACL2", "COMMON-LISP"), 2801("WITH-OPEN-STREAM", "ACL2", "COMMON-LISP"), 2802("UNLESS", "ACL2", "COMMON-LISP"), 2803("WITH-OUTPUT-TO-STRING", "ACL2", "COMMON-LISP"), 2804("UNREAD-CHAR", "ACL2", "COMMON-LISP"), 2805("WITH-PACKAGE-ITERATOR", "ACL2", "COMMON-LISP"), 2806("UNSIGNED-BYTE", "ACL2", "COMMON-LISP"), 2807("WITH-SIMPLE-RESTART", "ACL2", "COMMON-LISP"), 2808("UNTRACE", "ACL2", "COMMON-LISP"), 2809("WITH-SLOTS", "ACL2", "COMMON-LISP"), 2810("UNUSE-PACKAGE", "ACL2", "COMMON-LISP"), 2811("WITH-STANDARD-IO-SYNTAX", "ACL2", "COMMON-LISP"), 2812("UNWIND-PROTECT", "ACL2", "COMMON-LISP"), 2813("WRITE", "ACL2", "COMMON-LISP"), 2814("UPDATE-INSTANCE-FOR-DIFFERENT-CLASS", "ACL2", "COMMON-LISP"), 2815("WRITE-BYTE", "ACL2", "COMMON-LISP"), 2816("UPDATE-INSTANCE-FOR-REDEFINED-CLASS", "ACL2", "COMMON-LISP"), 2817("WRITE-CHAR", "ACL2", "COMMON-LISP"), 2818("UPGRADED-ARRAY-ELEMENT-TYPE", "ACL2", "COMMON-LISP"), 2819("WRITE-LINE", "ACL2", "COMMON-LISP"), 2820("UPGRADED-COMPLEX-PART-TYPE", "ACL2", "COMMON-LISP"), 2821("WRITE-SEQUENCE", "ACL2", "COMMON-LISP"), 2822("UPPER-CASE-P", "ACL2", "COMMON-LISP"), 2823("WRITE-STRING", "ACL2", "COMMON-LISP"), 2824("USE-PACKAGE", "ACL2", "COMMON-LISP"), 2825("WRITE-TO-STRING", "ACL2", "COMMON-LISP"), 2826("USE-VALUE", "ACL2", "COMMON-LISP"), 2827("Y-OR-N-P", "ACL2", "COMMON-LISP"), 2828("USER-HOMEDIR-PATHNAME", "ACL2", "COMMON-LISP"), 2829("YES-OR-NO-P", "ACL2", "COMMON-LISP"), 2830("VALUES", "ACL2", "COMMON-LISP"), 2831("ZEROP", "ACL2", "COMMON-LISP") 2832] 2833)`; 2834 2835(*****************************************************************************) 2836(* Verification that the actual ACL2 triples are well-formed. *) 2837(*****************************************************************************) 2838 2839(*****************************************************************************) 2840(* (defun lookup (pkg-name triples sym-name) *) 2841(* *) 2842(* ; Triples is a list of "package triples" of the form (sym-name *) 2843(* ; pkg-name orig-pkg-name) representing that the symbol-package-name of *) 2844(* ; pkg-name::sym-anme is orig-pkg-name. Lookup returns the *) 2845(* ; symbol-package-name of pkg-name::sym-name. *) 2846(* *) 2847(* (cond ((endp triples) *) 2848(* pkg-name) *) 2849(* ((and (equal pkg-name (nth 1 (car triples))) *) 2850(* (equal sym-name (nth 0 (car triples)))) *) 2851(* (nth 2 (car triples))) *) 2852(* (t (lookup pkg-name (cdr triples) sym-name)))) *) 2853(* *) 2854(* LOOKUP pkg_name [(x1,y1,z1);...;(xn,yn,zn)] sym_name = zi *) 2855(* if for some i: sym_name=xi and pkg_name=yi (scanning from left) *) 2856(* *) 2857(* LOOKUP pkg_name [(x1,y1,z1);...;(xn,yn,zn)] sym_name = pkg_name *) 2858(* if for all i: ~(sym_name=xi and pkg_name=yi) *) 2859(* *) 2860(*****************************************************************************) 2861val LOOKUP_def = 2862 Define 2863 `(LOOKUP pkg_name [] _ = pkg_name) 2864 /\ 2865 (LOOKUP pkg_name ((x1,y1,z1)::a) sym_name = 2866 if (sym_name=x1) /\ (pkg_name=y1) 2867 then z1 2868 else LOOKUP pkg_name a sym_name)`; 2869 2870(*****************************************************************************) 2871(* (defun valid-pkg-triples-aux (tail triples) *) 2872(* *) 2873(* ; We recognize whether tail, a tail of triples, is a legal list of *) 2874(* ; package triples with respect to the full list, triples. The idea is *) 2875(* ; that for any symbol s imported from package p1 to package p2, s *) 2876(* ; cannot be imported from some other package p0 into p1. That is, *) 2877(* ; lookup is idempotent. *) 2878(* *) 2879(* (if (endp tail) *) 2880(* t *) 2881(* (let* ((trip (car tail)) *) 2882(* (sym-name (nth 0 trip)) *) 2883(* (p2 (nth 2 trip))) *) 2884(* (and (equal (lookup p2 triples sym-name) *) 2885(* p2) *) 2886(* (not (equal sym-name "ACL2-PKG-WITNESS")) *) 2887(* (not (equal p2 "")) *) 2888(* (valid-pkg-triples-aux (cdr tail) triples))))) *) 2889(*****************************************************************************) 2890val VALID_PKG_TRIPLES_AUX_def = 2891 Define 2892 `(VALID_PKG_TRIPLES_AUX [] triples = T) 2893 /\ 2894 (VALID_PKG_TRIPLES_AUX ((sym_name,_,p2)::tail) triples = 2895 (LOOKUP p2 triples sym_name = p2) /\ 2896 ~(sym_name = "ACL2-PKG-WITNESS") /\ 2897 ~(p2 = "") /\ 2898 (VALID_PKG_TRIPLES_AUX tail triples))`; 2899 2900val VALID_PKG_TRIPLES_def = 2901 Define 2902 `VALID_PKG_TRIPLES triples = VALID_PKG_TRIPLES_AUX triples triples`; 2903 2904(*****************************************************************************) 2905(* Optimisation: Use a quicksort like algorithm to split the list *) 2906(* *) 2907(*****************************************************************************) 2908 2909val LOOKUP_AUX_def = 2910 Define 2911 `(LOOKUP_AUX [] _ = T) 2912 /\ 2913 (LOOKUP_AUX ((x1,y1,z1)::a) (sym_name:string,q:string,pkg_name:string) = 2914 if (sym_name=x1) /\ (pkg_name=y1) 2915 then (z1 = pkg_name) 2916 else LOOKUP_AUX a (sym_name,q,pkg_name))`; 2917 2918val ELOOKUP_def = 2919 Define `ELOOKUP l1 = EVERY (LOOKUP_AUX l1) l1`; 2920 2921val elookup_empty = 2922 prove(``ELOOKUP [] = T``,RW_TAC std_ss [ELOOKUP_def,EVERY_DEF]); 2923 2924val lookup_fast = 2925 prove(``!l. (LOOKUP pkg_name l sym_name = pkg_name) = 2926 LOOKUP_AUX l (sym_name,q,pkg_name)``, 2927 Induct THEN TRY (Cases THEN Cases_on `r`) THEN 2928 RW_TAC std_ss [LOOKUP_def,LOOKUP_AUX_def]); 2929 2930val separate_lemma = prove(``!l1 l2. VALID_PKG_TRIPLES_AUX l1 l2 = 2931 (EVERY (\ (x,y,z). ~(z = "")) l1) /\ 2932 (EVERY (\ (x,y,z). ~(x = "ACL2-PKG-WITNESS")) l1) /\ 2933 (EVERY (LOOKUP_AUX l2) l1)``, 2934 Induct THEN TRY (Cases THEN Cases_on `r`) THEN 2935 RW_TAC std_ss [VALID_PKG_TRIPLES_AUX_def,EVERY_DEF,GSYM lookup_fast] THEN 2936 METIS_TAC []); 2937 2938val separate_proof = prove(``!l1. VALID_PKG_TRIPLES l1 = 2939 (EVERY (\ (x,y,z). ~(z = "")) l1) /\ 2940 (EVERY (\ (x,y,z). ~(x = "ACL2-PKG-WITNESS")) l1) /\ 2941 (ELOOKUP l1)``, 2942 RW_TAC std_ss [VALID_PKG_TRIPLES_def,ELOOKUP_def,separate_lemma]); 2943 2944val every_split = 2945 prove(``!l. (!x. A x = B x /\ C x) ==> (EVERY A l = EVERY B l /\ EVERY C l)``, 2946 Induct THEN RW_TAC std_ss [EVERY_DEF] THEN METIS_TAC []); 2947 2948val leq_def = 2949 Define ` 2950 (leq "" "" = T) /\ 2951 (leq "" (STRING a b) = T) /\ 2952 (leq (STRING a b) "" = F) /\ 2953 (leq (STRING a b) (STRING c d) = 2954 if ORD a < ORD c then T else (ORD a = ORD c) /\ leq b d)`; 2955 2956val LEQ_def = 2957 Define 2958 `LEQ s1 (s2,x:string # string) = leq s1 s2`; 2959 2960val leq_only = prove(``!s a x y. LEQ s (a,x) = LEQ s (a,y)``, 2961 Cases THEN Cases THEN RW_TAC std_ss [LEQ_def]); 2962 2963val leq_t_imp = prove(``!l s x v0 v1. LEQ s (x,v0) ==> LOOKUP_AUX (FILTER ($~ o LEQ s) l) (x,v1)``, 2964 Induct THEN TRY (Cases THEN Cases_on `r`) THEN 2965 RW_TAC std_ss [FILTER] THEN Cases_on `v1` THEN RW_TAC std_ss [LOOKUP_AUX_def] THEN 2966 METIS_TAC [leq_only]); 2967 2968val leq_f_imp = prove(``!l s x v0 v1. ~LEQ s (x,v0) ==> LOOKUP_AUX (FILTER (LEQ s) l) (x,v1)``, 2969 Induct THEN TRY (Cases THEN Cases_on `r`) THEN 2970 RW_TAC std_ss [FILTER] THEN Cases_on `v1` THEN RW_TAC std_ss [LOOKUP_AUX_def] THEN 2971 METIS_TAC [leq_only]); 2972 2973val lookup_split_leq = 2974 prove(``!l1 x. LOOKUP_AUX l1 x = LOOKUP_AUX (FILTER (LEQ s) l1) x /\ LOOKUP_AUX (FILTER ($~ o LEQ s) l1) x``, 2975 Induct THEN TRY (Cases THEN Cases_on `r` THEN Cases_on `x` THEN Cases_on `r`) THEN 2976 RW_TAC std_ss [LOOKUP_AUX_def,FILTER] THEN 2977 METIS_TAC [leq_t_imp,leq_f_imp]); 2978 2979val every_lookup_split_leq = 2980 prove(``!s l1 l2. 2981 EVERY (LOOKUP_AUX l1) l2 = 2982 EVERY (LOOKUP_AUX (FILTER (LEQ s) l1)) (FILTER (LEQ s) l2) /\ 2983 EVERY (LOOKUP_AUX (FILTER ($~ o LEQ s) l1)) (FILTER ($~ o LEQ s) l2)``, 2984 CONV_TAC (STRIP_QUANT_CONV (LAND_CONV (REWR_CONV (MATCH_MP every_split (Q.SPEC `l1` lookup_split_leq))))) THEN 2985 GEN_TAC THEN GEN_TAC THEN Induct THEN TRY (Cases THEN Cases_on `r`) THEN 2986 RW_TAC std_ss [EVERY_DEF,LOOKUP_AUX_def,FILTER] THEN 2987 METIS_TAC [leq_t_imp,leq_f_imp]); 2988 2989val EVERY_FILTER = 2990 prove(``!l. EVERY P l = EVERY P (FILTER Q l) /\ EVERY P (FILTER ($~ o Q) l)``, 2991 Induct THEN RW_TAC arith_ss [EVERY_DEF,FILTER] THEN PROVE_TAC []); 2992 2993val PLACE_def = 2994 Define 2995 `PLACE s1 s2 s3 a (A,B,C,D) = 2996 if LEQ s2 a 2997 then if LEQ s1 a then (a::A,B,C,D) else (A,a::B,C,D) 2998 else if LEQ s3 a then (A,B,a::C,D) else (A,B,C,a::D)`; 2999 3000val (PARTITION_def,PARTIION_ind) = 3001 Defn.tprove(Defn.Hol_defn "PARTITION" 3002 `(PARTITION s1 s2 s3 (A,B,C,D) [] = (A,B,C,D)) /\ 3003 (PARTITION s1 s2 s3 (A,B,C,D) (a::bs) = 3004 PARTITION s1 s2 s3 (PLACE s1 s2 s3 a (A,B,C,D)) bs)`, 3005 Q.EXISTS_TAC `measure (LENGTH o SND o SND o SND o SND)` THEN 3006 REWRITE_TAC [prim_recTheory.WF_measure] THEN 3007 REWRITE_TAC [prim_recTheory.measure_thm] THEN 3008 RW_TAC std_ss [LENGTH]); 3009 3010val RFILTER_def = 3011 Define 3012 `(RFILTER P [] A = A) /\ 3013 (RFILTER P (a::b) A = RFILTER P b (if P a then a::A else A))`; 3014 3015val partition_lem = prove(``!l A B C D. PARTITION s1 s2 s3 (A,B,C,D) l = 3016 (RFILTER (\x. LEQ s1 x /\ LEQ s2 x) l A, 3017 RFILTER (\x. ~LEQ s1 x /\ LEQ s2 x) l B, 3018 RFILTER (\x. LEQ s3 x /\ ~LEQ s2 x) l C, 3019 RFILTER (\x. ~LEQ s3 x /\ ~LEQ s2 x) l D)``, 3020 Induct THEN RW_TAC arith_ss [PLACE_def,PARTITION_def,RFILTER_def] THEN 3021 FULL_SIMP_TAC std_ss []); 3022 3023val EPARTITION_def = 3024 Define 3025 `EPARTITION s1 s2 s3 (A,B,C,D) L = 3026 (\ (A,B,C,D). VALID_PKG_TRIPLES (REVERSE A) /\ 3027 VALID_PKG_TRIPLES (REVERSE B) /\ 3028 VALID_PKG_TRIPLES (REVERSE C) /\ 3029 VALID_PKG_TRIPLES (REVERSE D)) 3030 (PARTITION s1 s2 s3 (A,B,C,D) L)`; 3031 3032val RPARTITION_def = 3033 Define 3034 `RPARTITION s1 s2 s3 (A,B,C,D) L = 3035 (\ (A,B,C,D). VALID_PKG_TRIPLES A /\ 3036 VALID_PKG_TRIPLES B /\ 3037 VALID_PKG_TRIPLES C /\ 3038 VALID_PKG_TRIPLES D) 3039 (PARTITION s1 s2 s3 (A,B,C,D) L)`; 3040 3041val RFILTER_thm = 3042 prove(``!A B P. RFILTER P A B = REVERSE (FILTER P A) ++ B``, 3043 Induct THEN RW_TAC arith_ss 3044 [RFILTER_def,FILTER,REVERSE_DEF,APPEND,GSYM APPEND_ASSOC]); 3045 3046val FILTER_SPLIT = 3047 prove(``!l P Q. FILTER (\x. P x /\ Q x) l = FILTER P (FILTER Q l)``, 3048 Induct THEN RW_TAC arith_ss [FILTER] THEN FULL_SIMP_TAC arith_ss []); 3049 3050val FILTER_REVERSE = 3051 prove(``!l. REVERSE (FILTER P l) = FILTER P (REVERSE l)``, 3052 Induct THEN 3053 RW_TAC arith_ss [FILTER,REVERSE_DEF,FILTER_APPEND_DISTRIB,APPEND_NIL]); 3054 3055val elookup_split = 3056prove(``!s1 s2 s3 l. VALID_PKG_TRIPLES l = EPARTITION s1 s2 s3 ([],[],[],[]) l``, 3057 RW_TAC arith_ss [EPARTITION_def,separate_proof,ELOOKUP_def, 3058 partition_lem,RFILTER_thm,REVERSE_REVERSE, 3059 APPEND_NIL,FILTER_SPLIT] THEN 3060 METIS_TAC [every_lookup_split_leq,EVERY_FILTER]); 3061 3062val rlookup_split = prove(``!s1 s2 s3 l. VALID_PKG_TRIPLES (REVERSE l) = RPARTITION s1 s2 s3 ([],[],[],[]) l``, 3063 RW_TAC arith_ss [RPARTITION_def,separate_proof,ELOOKUP_def,partition_lem,RFILTER_thm, 3064 APPEND_NIL,FILTER_SPLIT,FILTER_REVERSE] THEN 3065 METIS_TAC [every_lookup_split_leq,EVERY_FILTER]); 3066 3067val RPARTITION = prove(`` 3068 (RPARTITION s1 s2 s3 (A,B,C,D) [] = 3069 ((VALID_PKG_TRIPLES A /\ VALID_PKG_TRIPLES B) /\ (VALID_PKG_TRIPLES C /\ VALID_PKG_TRIPLES D))) /\ 3070 (RPARTITION s1 s2 s3 X [a] = RPARTITION s1 s2 s3 (PLACE s1 s2 s3 a X) []) /\ 3071 (RPARTITION s1 s2 s3 X (a::b::c) = 3072 RPARTITION s1 s2 s3 (PLACE s1 s2 s3 b (PLACE s1 s2 s3 a X)) c)``, 3073 Cases_on `X` THEN Cases_on `r` THEN Cases_on `r'` THEN 3074 RW_TAC arith_ss [PLACE_def,PARTITION_def,RPARTITION_def] THEN 3075 RW_TAC arith_ss [RPARTITION_def] THEN METIS_TAC []); 3076 3077val EPARTITION = prove(`` 3078 (EPARTITION s1 s2 s3 (A,B,C,D) [] = 3079 ((VALID_PKG_TRIPLES (REVERSE A) /\ VALID_PKG_TRIPLES (REVERSE B)) /\ 3080 (VALID_PKG_TRIPLES (REVERSE C) /\ VALID_PKG_TRIPLES (REVERSE D)))) /\ 3081 (EPARTITION s1 s2 s3 X [a] = EPARTITION s1 s2 s3 (PLACE s1 s2 s3 a X) []) /\ 3082 (EPARTITION s1 s2 s3 X (a::b::c) = 3083 EPARTITION s1 s2 s3 (PLACE s1 s2 s3 b (PLACE s1 s2 s3 a X)) c)``, 3084 Cases_on `X` THEN Cases_on `r` THEN Cases_on `r'` THEN 3085 RW_TAC arith_ss [PLACE_def,PARTITION_def,EPARTITION_def] THEN 3086 RW_TAC arith_ss [EPARTITION_def] THEN METIS_TAC []); 3087 3088val LLEQ_def = Define ` 3089 (LLEQ [] "" = T) /\ 3090 (LLEQ [] (STRING a b) = T) /\ 3091 (LLEQ (x::y) "" = F) /\ 3092 (LLEQ (x::y) (STRING a b) = if x < ORD a then T else (if (x = ORD a) then LLEQ y b else F))`; 3093 3094val LPLACE_def = Define ` 3095 LPLACE l1 l2 l3 a (A,B,C,D) = 3096 if LLEQ l2 (FST a) then 3097 if LLEQ l1 (FST a) then (a::A,B,C,D) else (A,a::B,C,D) 3098 else 3099 if LLEQ l3 (FST a) then (A,B,a::C,D) else (A,B,C,a::D)`; 3100 3101val LLEQ_THM = prove(``!s1 s2 x. LLEQ (MAP ORD (EXPLODE s1)) s2 = LEQ s1 (s2,x)``, 3102 completeInduct_on `STRLEN s1 + STRLEN s2` THEN 3103 Cases THEN Cases THEN RW_TAC arith_ss [LLEQ_def,LEQ_def,stringTheory.EXPLODE_EQNS,MAP,leq_def] THEN 3104 RULE_ASSUM_TAC (CONV_RULE (REPEATC (STRIP_QUANT_CONV RIGHT_IMP_FORALL_CONV) THENC 3105 REWRITE_CONV [AND_IMP_INTRO])) THEN 3106 REPEAT AP_TERM_TAC THEN 3107 REWRITE_TAC [GSYM LEQ_def] THEN 3108 POP_ASSUM MATCH_MP_TAC THEN 3109 RW_TAC arith_ss [stringTheory.STRLEN_DEF]); 3110 3111val LPLACE_THM = prove(``!s1 s2 s3. PLACE s1 s2 s3 = 3112 LPLACE (MAP ORD (EXPLODE s1)) (MAP ORD (EXPLODE s2)) (MAP ORD (EXPLODE s3))``, 3113 REPEAT GEN_TAC THEN REWRITE_TAC [FUN_EQ_THM] THEN 3114 GEN_TAC THEN Cases THEN Cases_on `r` THEN Cases_on `r'` THEN 3115 RW_TAC arith_ss [PLACE_def,LPLACE_def,LLEQ_THM] THEN 3116 Cases_on `x` THEN FULL_SIMP_TAC arith_ss [GSYM LLEQ_THM]); 3117 3118val AL_def = Define `AL (a:string # string # string) (A,B,C,D) = (a::A,B,C,D)`; 3119val BL_def = Define `BL (a:string # string # string) (A,B,C,D) = (A,a::B,C,D)`; 3120val CL_def = Define `CL (a:string # string # string) (A,B,C,D) = (A,B,a::C,D)`; 3121val DL_def = Define `DL (a:string # string # string) (A,B,C,D) = (A,B,C,a::D)`; 3122 3123val L_defs = LIST_CONJ [AL_def,BL_def,CL_def,DL_def]; 3124 3125val LPLACE_RWR = prove(``LPLACE l1 l2 l3 a = 3126 if LLEQ l2 (FST a) then 3127 if LLEQ l1 (FST a) then AL a else BL a 3128 else 3129 if LLEQ l3 (FST a) then CL a else DL a``, 3130 REWRITE_TAC [FUN_EQ_THM] THEN Cases THEN Cases_on `r` THEN Cases_on `r'` THEN 3131 RW_TAC arith_ss [LPLACE_def,L_defs]); 3132 3133val LOOKUP_AUX_RWR = prove(`` 3134 (LOOKUP_AUX [] v = T) /\ 3135 (LOOKUP_AUX ((name1,ACL2_CL)::a) (name2,ACL2_CL) = LOOKUP_AUX a (name2,ACL2_CL)) /\ 3136 (LOOKUP_AUX ((name1,ACL2_CL)::a) (name2,ACL2_USER_CL) = LOOKUP_AUX a (name2,ACL2_USER_CL)) /\ 3137 (LOOKUP_AUX ((name1,ACL2_CL)::a) (name2,ACL2_USER) = ~(name1 = name2) /\ LOOKUP_AUX a (name2,ACL2_USER)) /\ 3138 (LOOKUP_AUX ((name1,ACL2_USER_CL)::a) (name2,ACL2_CL) = LOOKUP_AUX a (name2,ACL2_CL)) /\ 3139 (LOOKUP_AUX ((name1,ACL2_USER_CL)::a) (name2,ACL2_USER_CL) = LOOKUP_AUX a (name2,ACL2_USER_CL)) /\ 3140 (LOOKUP_AUX ((name1,ACL2_USER_CL)::a) (name2,ACL2_USER) = LOOKUP_AUX a (name2,ACL2_USER)) /\ 3141 (LOOKUP_AUX ((name1,ACL2_USER)::a) (name2,ACL2_CL) = LOOKUP_AUX a (name2,ACL2_CL)) /\ 3142 (LOOKUP_AUX ((name1,ACL2_USER)::a) (name2,ACL2_USER_CL) = LOOKUP_AUX a (name2,ACL2_USER_CL)) /\ 3143 (LOOKUP_AUX ((name1,ACL2_USER)::a) (name2,ACL2_USER) = LOOKUP_AUX a (name2,ACL2_USER))``, 3144 RW_TAC arith_ss [LOOKUP_AUX_def,ACL2_CL_def,ACL2_USER_def,ACL_USER_CL_def] THEN 3145 METIS_TAC []); 3146 3147val CHECK_def = Define `CHECK (x,y,z) = ~(z = "") /\ ~(x = "ACL2-PKG-WITNESS")`; 3148 3149val VALID_PKG_TRIPLES_RWR = prove(``!l1. 3150 VALID_PKG_TRIPLES l1 = EVERY CHECK l1 /\ ELOOKUP l1``, 3151 STRIP_TAC THEN REWRITE_TAC [separate_proof] THEN 3152 MATCH_MP_TAC (DECIDE ``(A = B /\ C) /\ (D = E) ==> (B /\ C /\ E = A /\ D)``) THEN 3153 Induct_on `l1` THEN RW_TAC arith_ss [EVERY_DEF] THEN 3154 Cases_on `h` THEN Cases_on `r` THEN RW_TAC arith_ss [CHECK_def] THEN 3155 PROVE_TAC []); 3156 3157val PRE_EVAL_RWR = prove(`` 3158 (CHECK (x,ACL2_CL) = ~(x = "ACL2-PKG-WITNESS")) /\ 3159 (CHECK (x,ACL2_USER_CL) = ~(x = "ACL2-PKG-WITNESS")) /\ 3160 (CHECK (x,ACL2_USER) = ~(x = "ACL2-PKG-WITNESS"))``, 3161 RW_TAC arith_ss [CHECK_def,ACL2_CL_def,ACL2_USER_def,ACL_USER_CL_def]); 3162 3163fun ABBREV_CONV conv term = 3164let val (a,right) = dest_comb term 3165 val (left,lterm) = dest_comb a 3166 val var = genvar (type_of lterm) 3167in INST [var |-> lterm] (conv (mk_comb(mk_comb(left,var),right))) 3168end; 3169 3170local 3171 val (thm1,p1) = CONJ_PAIR RPARTITION 3172 val (thm2,thm3) = CONJ_PAIR p1 3173in 3174fun RPART_CONV n compset term = 3175let val x = (rator o rator) term 3176 val (k,s3) = dest_comb x 3177 val (l,s2) = dest_comb k 3178 val s1 = rand l 3179 val place_thm = RIGHT_CONV_RULE EVAL (SPECL [s1,s2,s3] LPLACE_THM); 3180 val inst = INST [``s1:string`` |-> s1,``s2:string`` |-> s2,``s3:string`` |-> s3]; 3181 val thm3' = REWRITE_RULE [place_thm] (inst thm3) 3182 val thm2' = REWRITE_RULE [place_thm] (inst thm2); 3183 fun RPART_CONV_x n term = 3184 (if n mod 50 = 0 then (print "R[" ; print (int_to_string n) ; print "]") else () 3185 ; ABBREV_CONV (FIRST_CONV 3186 [REWR_CONV thm3' THENC 3187 RATOR_CONV (RAND_CONV (computeLib.CBV_CONV compset)) THENC 3188 RPART_CONV_x (n - 2) 3189 ,REWR_CONV thm2' THENC 3190 RATOR_CONV (RAND_CONV (computeLib.CBV_CONV compset)) THENC 3191 RPART_CONV_x (n - 1) 3192 ,ALL_CONV]) term) 3193in 3194 (RPART_CONV_x n THENC 3195 DEPTH_CONV (FIRST_CONV (map REWR_CONV (CONJUNCTS L_defs))) THENC 3196 REWR_CONV thm1) term 3197end 3198end; 3199 3200local 3201 val (thm1,p1) = CONJ_PAIR EPARTITION 3202 val (thm2,thm3) = CONJ_PAIR p1 3203in 3204fun EPART_CONV n compset term = 3205let val x = (rator o rator) term 3206 val (k,s3) = dest_comb x 3207 val (l,s2) = dest_comb k 3208 val s1 = rand l 3209 val place_thm = RIGHT_CONV_RULE EVAL (SPECL [s1,s2,s3] LPLACE_THM); 3210 val inst = INST [``s1:string`` |-> s1,``s2:string`` |-> s2,``s3:string`` |-> s3]; 3211 val thm3' = REWRITE_RULE [place_thm] (inst thm3) 3212 val thm2' = REWRITE_RULE [place_thm] (inst thm2); 3213 fun EPART_CONV_x n term = 3214 (if n mod 50 = 0 then (print "E[" ; print (int_to_string n) ; print "]") else () 3215 ; ABBREV_CONV (FIRST_CONV 3216 [REWR_CONV thm3' THENC 3217 RATOR_CONV (RAND_CONV (computeLib.CBV_CONV compset)) THENC 3218 EPART_CONV_x (n - 2) 3219 ,REWR_CONV thm2' THENC 3220 RATOR_CONV (RAND_CONV (computeLib.CBV_CONV compset)) THENC 3221 EPART_CONV_x (n - 1) 3222 ,ALL_CONV]) term) 3223in 3224 (EPART_CONV_x n THENC 3225 DEPTH_CONV (FIRST_CONV (map REWR_CONV (CONJUNCTS L_defs))) THENC 3226 REWR_CONV thm1) term 3227end 3228end; 3229 3230local 3231 open computeLib 3232 val compset_part = reduceLib.num_compset(); 3233 val _ = set_skip compset_part ``COND`` (SOME 1); 3234 val _ = add_thms [LLEQ_def,LPLACE_RWR,pairTheory.FST] compset_part; 3235 val _ = add_conv (``$ORD``,1,stringLib.ORD_CHR_CONV) compset_part 3236 3237 val full_compset = new_compset [VALID_PKG_TRIPLES_RWR,PRE_EVAL_RWR, 3238 REVERSE_REV,REV_DEF,ELOOKUP_def,EVERY_DEF,LOOKUP_AUX_RWR,NOT_CLAUSES,AND_CLAUSES]; 3239 val _ = add_conv (``($=):string -> string -> bool``,2,stringLib.string_EQ_CONV) full_compset; 3240in 3241fun split_term_leq list term = 3242let val x = length list 3243 val _ = (print "\n" ; print (int_to_string (length list)) ; print ":") 3244 val (listl,listr) = (split_after (length list div 2) list handle e => ([],[])) 3245 val (list1,list2) = (split_after (length listl div 2) listl handle e => ([],[])) 3246 val (list3,list4) = (split_after (length listr div 2) listr handle e => ([],[])) 3247in 3248 if x <= 12 orelse all (curry op= (hd list)) list then 3249 (CBV_CONV full_compset THENC EVAL) term 3250 else split4 x (list1,list2,list3,list4) term 3251end 3252and split4 n (list1,list2,list3,list4) term = 3253let val spec = map fromMLstring [hd list4,hd list3,hd list2] 3254in 3255 (FIRST_CONV 3256 [REWR_CONV (SPECL spec rlookup_split) THENC RPART_CONV n compset_part 3257 ,REWR_CONV (SPECL spec elookup_split) THENC EPART_CONV n compset_part] THENC 3258 FORK_CONV ( 3259 FORK_CONV (split_term_leq list4,split_term_leq list3), 3260 FORK_CONV (split_term_leq list2,split_term_leq list1)) THENC 3261 REWRITE_CONV []) term 3262end 3263end; 3264 3265fun prove_valid_pkg_leq thm = 3266let val list = 3267 sort (fn a => fn b => a <= b) 3268 ((map (fromHOLstring o hd o strip_pair) o fst o dest_list o rhs o concl) thm); 3269in 3270 (RIGHT_CONV_RULE (split_term_leq list) (AP_TERM ``VALID_PKG_TRIPLES`` thm)) 3271 before (print "\n") 3272end; 3273 3274(*****************************************************************************) 3275(* Warning: *) 3276(* runtime: 1356.715s, gctime: 156.740s, systime: 1.650s *) 3277(*****************************************************************************) 3278 3279val pkg_valid_thm = time prove_valid_pkg_leq ACL2_PACKAGE_ALIST_def; 3280 3281val _ = save_thm("VALID_ACL2_PACKAGE_ALIST",pkg_valid_thm); 3282 3283(* 3284 3285val VALID_ACL2_PACKAGE_ALIST = 3286 save_thm 3287 ("VALID_ACL2_PACKAGE_ALIST", 3288 Count.apply (time EVAL) ``VALID_PKG_TRIPLES ACL2_PACKAGE_ALIST``); 3289 3290This causes an overflow: 3291 3292 OverflowUncaught exception: 3293 Overflow 3294 3295*) 3296 3297val _ = export_theory(); 3298