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