1
2val _ = current_package :=
3 implode(map chr (cons 65 (cons 67 (cons 76 (cons 50 nil)))));
4
5val _ = sexp.acl2_list_ref := [
6
7(mkpair (mksym "ACL2" "INCLUDE-BOOK") (mkpair (mk_chars_str (chars_to_string (
8cons 116 (cons 111 (cons 116 (cons 97 (cons 108 (cons 45 (cons 111 (cons 114 (
9cons 100 (cons 101 (cons 114 nil))))))))))))) (mksym "COMMON-LISP" "NIL")))
10,
11
12(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" "MEMBERP") (
13mkpair (mkpair (mksym "ACL2" "A") (mkpair (mksym "ACL2" "X") (mksym 
14"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (
15mkpair (mksym "COMMON-LISP" "CONSP") (mkpair (mksym "ACL2" "X") (mksym 
16"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (
17mkpair (mksym "COMMON-LISP" "EQUAL") (mkpair (mksym "ACL2" "A") (mkpair (
18mkpair (mksym "COMMON-LISP" "CAR") (mkpair (mksym "ACL2" "X") (mksym 
19"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym 
20"COMMON-LISP" "EQUAL") (mkpair (mksym "ACL2" "A") (mkpair (mkpair (mksym 
21"COMMON-LISP" "CAR") (mkpair (mksym "ACL2" "X") (mksym "COMMON-LISP" "NIL"))) (
22mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "ACL2" "MEMBERP") (
23mkpair (mksym "ACL2" "A") (mkpair (mkpair (mksym "COMMON-LISP" "CDR") (mkpair (
24mksym "ACL2" "X") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) (
25mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (
26mkpair (mksym "COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) (mksym 
27"COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL")))))
28,
29
30(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" "DROP") (mkpair (
31mkpair (mksym "ACL2" "A") (mkpair (mksym "ACL2" "X") (mksym "COMMON-LISP" 
32"NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym 
33"COMMON-LISP" "ENDP") (mkpair (mksym "ACL2" "X") (mksym "COMMON-LISP" "NIL"))) (
34mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" 
35"NIL") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" 
36"IF") (mkpair (mkpair (mksym "COMMON-LISP" "EQUAL") (mkpair (mksym "ACL2" "A") (
37mkpair (mkpair (mksym "COMMON-LISP" "CAR") (mkpair (mksym "ACL2" "X") (mksym 
38"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym 
39"ACL2" "DROP") (mkpair (mksym "ACL2" "A") (mkpair (mkpair (mksym 
40"COMMON-LISP" "CDR") (mkpair (mksym "ACL2" "X") (mksym "COMMON-LISP" "NIL"))) (
41mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" "CONS") (
42mkpair (mkpair (mksym "COMMON-LISP" "CAR") (mkpair (mksym "ACL2" "X") (mksym 
43"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "ACL2" "DROP") (mkpair (mksym 
44"ACL2" "A") (mkpair (mkpair (mksym "COMMON-LISP" "CDR") (mkpair (mksym "ACL2" 
45"X") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) (mksym 
46"COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" 
47"NIL"))))) (mksym "COMMON-LISP" "NIL")))))
48,
49
50(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" "INSERT") (mkpair (
51mkpair (mksym "ACL2" "A") (mkpair (mksym "ACL2" "X") (mksym "COMMON-LISP" 
52"NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym 
53"COMMON-LISP" "ENDP") (mkpair (mksym "ACL2" "X") (mksym "COMMON-LISP" "NIL"))) (
54mkpair (mkpair (mksym "COMMON-LISP" "CONS") (mkpair (mksym "ACL2" "A") (
55mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" 
56"NIL") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) (mkpair (
57mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "COMMON-LISP" 
58"EQUAL") (mkpair (mksym "ACL2" "A") (mkpair (mkpair (mksym "COMMON-LISP" 
59"CAR") (mkpair (mksym "ACL2" "X") (mksym "COMMON-LISP" "NIL"))) (mksym 
60"COMMON-LISP" "NIL")))) (mkpair (mksym "ACL2" "X") (mkpair (mkpair (mksym 
61"COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2" "<<") (mkpair (mksym "ACL2" 
62"A") (mkpair (mkpair (mksym "COMMON-LISP" "CAR") (mkpair (mksym "ACL2" "X") (
63mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (
64mksym "COMMON-LISP" "CONS") (mkpair (mksym "ACL2" "A") (mkpair (mksym "ACL2" 
65"X") (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" 
66"CONS") (mkpair (mkpair (mksym "COMMON-LISP" "CAR") (mkpair (mksym "ACL2" "X") (
67mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "ACL2" "INSERT") (mkpair (
68mksym "ACL2" "A") (mkpair (mkpair (mksym "COMMON-LISP" "CDR") (mkpair (mksym 
69"ACL2" "X") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) (
70mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL"))))) (mksym 
71"COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" 
72"NIL")))))
73,
74
75(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" "ORDEREDP") (
76mkpair (mkpair (mksym "ACL2" "X") (mksym "COMMON-LISP" "NIL")) (mkpair (
77mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "COMMON-LISP" "ENDP") (
78mkpair (mkpair (mksym "COMMON-LISP" "CDR") (mkpair (mksym "ACL2" "X") (mksym 
79"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym 
80"COMMON-LISP" "ENDP") (mkpair (mkpair (mksym "COMMON-LISP" "CDR") (mkpair (
81mksym "ACL2" "X") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))) (
82mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2" "<<") (
83mkpair (mkpair (mksym "COMMON-LISP" "CAR") (mkpair (mksym "ACL2" "X") (mksym 
84"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "CAR") (mkpair (
85mkpair (mksym "COMMON-LISP" "CDR") (mkpair (mksym "ACL2" "X") (mksym 
86"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" 
87"NIL")))) (mkpair (mkpair (mksym "ACL2" "ORDEREDP") (mkpair (mkpair (mksym 
88"COMMON-LISP" "CDR") (mkpair (mksym "ACL2" "X") (mksym "COMMON-LISP" "NIL"))) (
89mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (
90mkpair (mksym "COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) (mksym 
91"COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" 
92"NIL")))))
93,
94
95(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" "UNIQUEP") (
96mkpair (mkpair (mksym "ACL2" "X") (mksym "COMMON-LISP" "NIL")) (mkpair (
97mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "COMMON-LISP" "ENDP") (
98mkpair (mksym "ACL2" "X") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (
99mksym "COMMON-LISP" "ENDP") (mkpair (mksym "ACL2" "X") (mksym "COMMON-LISP" 
100"NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym 
101"COMMON-LISP" "NOT") (mkpair (mkpair (mksym "ACL2" "MEMBERP") (mkpair (mkpair (
102mksym "COMMON-LISP" "CAR") (mkpair (mksym "ACL2" "X") (mksym "COMMON-LISP" 
103"NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "CDR") (mkpair (mksym "ACL2" 
104"X") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) (mksym 
105"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "ACL2" "UNIQUEP") (mkpair (
106mkpair (mksym "COMMON-LISP" "CDR") (mkpair (mksym "ACL2" "X") (mksym 
107"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym 
108"COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym 
109"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" 
110"NIL"))))) (mksym "COMMON-LISP" "NIL")))))
111,
112
113(mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "ACL2" "MEMBERP-INSERT-SAME") (
114mkpair (mkpair (mksym "COMMON-LISP" "EQUAL") (mkpair (mkpair (mksym "ACL2" 
115"MEMBERP") (mkpair (mksym "ACL2" "A") (mkpair (mkpair (mksym "ACL2" "INSERT") (
116mkpair (mksym "ACL2" "A") (mkpair (mksym "ACL2" "X") (mksym "COMMON-LISP" 
117"NIL")))) (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" 
118"QUOTE") (mkpair (mksym "COMMON-LISP" "T") (mksym "COMMON-LISP" "NIL"))) (
119mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL"))))
120,
121
122(mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "ACL2" "MEMBERP-INSERT-DIFF") (
123mkpair (mkpair (mksym "ACL2" "IMPLIES") (mkpair (mkpair (mksym "COMMON-LISP" 
124"NOT") (mkpair (mkpair (mksym "COMMON-LISP" "EQUAL") (mkpair (mksym "ACL2" 
125"A") (mkpair (mksym "ACL2" "B") (mksym "COMMON-LISP" "NIL")))) (mksym 
126"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "EQUAL") (mkpair (
127mkpair (mksym "ACL2" "MEMBERP") (mkpair (mksym "ACL2" "A") (mkpair (mkpair (
128mksym "ACL2" "INSERT") (mkpair (mksym "ACL2" "B") (mkpair (mksym "ACL2" "X") (
129mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (
130mksym "ACL2" "MEMBERP") (mkpair (mksym "ACL2" "A") (mkpair (mksym "ACL2" "X") (
131mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) (mksym 
132"COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL"))))
133,
134
135(mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "ACL2" "MEMBERP-DROP-SAME") (
136mkpair (mkpair (mksym "COMMON-LISP" "EQUAL") (mkpair (mkpair (mksym "ACL2" 
137"MEMBERP") (mkpair (mksym "ACL2" "A") (mkpair (mkpair (mksym "ACL2" "DROP") (
138mkpair (mksym "ACL2" "A") (mkpair (mksym "ACL2" "X") (mksym "COMMON-LISP" 
139"NIL")))) (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" 
140"QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) (
141mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL"))))
142,
143
144(mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "ACL2" "MEMBERP-DROP-DIFF") (
145mkpair (mkpair (mksym "ACL2" "IMPLIES") (mkpair (mkpair (mksym "COMMON-LISP" 
146"NOT") (mkpair (mkpair (mksym "COMMON-LISP" "EQUAL") (mkpair (mksym "ACL2" 
147"A") (mkpair (mksym "ACL2" "B") (mksym "COMMON-LISP" "NIL")))) (mksym 
148"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "EQUAL") (mkpair (
149mkpair (mksym "ACL2" "MEMBERP") (mkpair (mksym "ACL2" "A") (mkpair (mkpair (
150mksym "ACL2" "DROP") (mkpair (mksym "ACL2" "B") (mkpair (mksym "ACL2" "X") (
151mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (
152mksym "ACL2" "MEMBERP") (mkpair (mksym "ACL2" "A") (mkpair (mksym "ACL2" "X") (
153mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) (mksym 
154"COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL"))))
155,
156
157(mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "ACL2" 
158"ORDERED-IMPLIES-UNIQUE") (mkpair (mkpair (mksym "ACL2" "IMPLIES") (mkpair (
159mkpair (mksym "ACL2" "ORDEREDP") (mkpair (mksym "ACL2" "X") (mksym 
160"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "ACL2" "UNIQUEP") (mkpair (
161mksym "ACL2" "X") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) (
162mksym "COMMON-LISP" "NIL"))))
163,
164
165(mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "ACL2" 
166"MEMBERP-YES-REDUCE-INSERT") (mkpair (mkpair (mksym "ACL2" "IMPLIES") (mkpair (
167mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2" "ORDEREDP") (
168mkpair (mksym "ACL2" "X") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (
169mksym "ACL2" "MEMBERP") (mkpair (mksym "ACL2" "A") (mkpair (mksym "ACL2" "X") (
170mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (
171mkpair (mksym "COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) (mksym 
172"COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym "COMMON-LISP" "EQUAL") (
173mkpair (mkpair (mksym "ACL2" "INSERT") (mkpair (mksym "ACL2" "A") (mkpair (
174mksym "ACL2" "X") (mksym "COMMON-LISP" "NIL")))) (mkpair (mksym "ACL2" "X") (
175mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) (mksym 
176"COMMON-LISP" "NIL"))))
177,
178
179(mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "ACL2" 
180"MEMBERP-NO-REDUCE-DROP") (mkpair (mkpair (mksym "ACL2" "IMPLIES") (mkpair (
181mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2" "TRUE-LISTP") (
182mkpair (mksym "ACL2" "X") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (
183mksym "COMMON-LISP" "NOT") (mkpair (mkpair (mksym "ACL2" "MEMBERP") (mkpair (
184mksym "ACL2" "A") (mkpair (mksym "ACL2" "X") (mksym "COMMON-LISP" "NIL")))) (
185mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (
186mkpair (mksym "COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) (mksym 
187"COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym "COMMON-LISP" "EQUAL") (
188mkpair (mkpair (mksym "ACL2" "DROP") (mkpair (mksym "ACL2" "A") (mkpair (
189mksym "ACL2" "X") (mksym "COMMON-LISP" "NIL")))) (mkpair (mksym "ACL2" "X") (
190mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) (mksym 
191"COMMON-LISP" "NIL"))))
192,
193
194(mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "ACL2" 
195"DROP-PRESERVES-ORDEREDP") (mkpair (mkpair (mksym "ACL2" "IMPLIES") (mkpair (
196mkpair (mksym "ACL2" "ORDEREDP") (mkpair (mksym "ACL2" "X") (mksym 
197"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "ACL2" "ORDEREDP") (mkpair (
198mkpair (mksym "ACL2" "DROP") (mkpair (mksym "ACL2" "A") (mkpair (mksym "ACL2" 
199"X") (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL"))) (mksym 
200"COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL"))))
201,
202
203(mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "ACL2" 
204"INSERT-PRESERVES-ORDEREDP") (mkpair (mkpair (mksym "ACL2" "IMPLIES") (mkpair (
205mkpair (mksym "ACL2" "ORDEREDP") (mkpair (mksym "ACL2" "X") (mksym 
206"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "ACL2" "ORDEREDP") (mkpair (
207mkpair (mksym "ACL2" "INSERT") (mkpair (mksym "ACL2" "A") (mkpair (mksym 
208"ACL2" "X") (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL"))) (
209mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL"))))
210,
211
212(mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "ACL2" 
213"DROP-OF-INSERT-IS-SAME") (mkpair (mkpair (mksym "ACL2" "IMPLIES") (mkpair (
214mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2" "TRUE-LISTP") (
215mkpair (mksym "ACL2" "X") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (
216mksym "COMMON-LISP" "NOT") (mkpair (mkpair (mksym "ACL2" "MEMBERP") (mkpair (
217mksym "ACL2" "A") (mkpair (mksym "ACL2" "X") (mksym "COMMON-LISP" "NIL")))) (
218mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (
219mkpair (mksym "COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) (mksym 
220"COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym "COMMON-LISP" "EQUAL") (
221mkpair (mkpair (mksym "ACL2" "DROP") (mkpair (mksym "ACL2" "A") (mkpair (
222mkpair (mksym "ACL2" "INSERT") (mkpair (mksym "ACL2" "A") (mkpair (mksym 
223"ACL2" "X") (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) (
224mkpair (mksym "ACL2" "X") (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" 
225"NIL")))) (mksym "COMMON-LISP" "NIL"))))
226,
227
228(mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "ACL2" 
229"INSERT-OF-DROP-IS-SAME") (mkpair (mkpair (mksym "ACL2" "IMPLIES") (mkpair (
230mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2" "ORDEREDP") (
231mkpair (mksym "ACL2" "X") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (
232mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2" "TRUE-LISTP") (mkpair (
233mksym "ACL2" "X") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "ACL2" 
234"MEMBERP") (mkpair (mksym "ACL2" "A") (mkpair (mksym "ACL2" "X") (mksym 
235"COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (
236mksym "COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" 
237"NIL"))))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym 
238"COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (
239mkpair (mkpair (mksym "COMMON-LISP" "EQUAL") (mkpair (mkpair (mksym "ACL2" 
240"INSERT") (mkpair (mksym "ACL2" "A") (mkpair (mkpair (mksym "ACL2" "DROP") (
241mkpair (mksym "ACL2" "A") (mkpair (mksym "ACL2" "X") (mksym "COMMON-LISP" 
242"NIL")))) (mksym "COMMON-LISP" "NIL")))) (mkpair (mksym "ACL2" "X") (mksym 
243"COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" 
244"NIL"))))
245,
246
247(mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "ACL2" 
248"INSERT-RETURNS-TRUE-LISTS") (mkpair (mkpair (mksym "ACL2" "IMPLIES") (mkpair (
249mkpair (mksym "ACL2" "TRUE-LISTP") (mkpair (mksym "ACL2" "X") (mksym 
250"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "ACL2" "TRUE-LISTP") (mkpair (
251mkpair (mksym "ACL2" "INSERT") (mkpair (mksym "ACL2" "A") (mkpair (mksym 
252"ACL2" "X") (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL"))) (
253mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL"))))
254
255];
256