1open HolKernel Parse boolLib bossLib intSyntax pairSyntax listSyntax stringLib numLib sexp;
2
3val package =
4 implode(map chr (cons 65 (cons 67 (cons 76 (cons 50 nil)))));
5
6val events = [
7
8(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" "RCDP") (mkpair (
9mkpair (mksym "ACL2" "X") (mksym "COMMON-LISP" "NIL")) (mkpair (mkpair (mksym
10"COMMON-LISP" "IF") (mkpair (mkpair (mksym "COMMON-LISP" "NULL") (mkpair (
11mksym "ACL2" "X") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym
12"COMMON-LISP" "NULL") (mkpair (mksym "ACL2" "X") (mksym "COMMON-LISP" "NIL"))) (
13mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym
14"COMMON-LISP" "CONSP") (mkpair (mksym "ACL2" "X") (mksym "COMMON-LISP" "NIL"))) (
15mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym
16"COMMON-LISP" "CONSP") (mkpair (mkpair (mksym "COMMON-LISP" "CAR") (mkpair (
17mksym "ACL2" "X") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))) (
18mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2"
19"RCDP") (mkpair (mkpair (mksym "COMMON-LISP" "CDR") (mkpair (mksym "ACL2" "X") (
20mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (
21mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "COMMON-LISP" "CDR") (mkpair (
22mkpair (mksym "COMMON-LISP" "CAR") (mkpair (mksym "ACL2" "X") (mksym
23"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym
24"COMMON-LISP" "IF") (mkpair (mkpair (mksym "COMMON-LISP" "NULL") (mkpair (
25mkpair (mksym "COMMON-LISP" "CDR") (mkpair (mksym "ACL2" "X") (mksym
26"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym
27"COMMON-LISP" "NULL") (mkpair (mkpair (mksym "COMMON-LISP" "CDR") (mkpair (
28mksym "ACL2" "X") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))) (
29mkpair (mkpair (mksym "ACL2" "<<") (mkpair (mkpair (mksym "COMMON-LISP" "CAR") (
30mkpair (mkpair (mksym "COMMON-LISP" "CAR") (mkpair (mksym "ACL2" "X") (mksym
31"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym
32"COMMON-LISP" "CAR") (mkpair (mkpair (mksym "COMMON-LISP" "CAR") (mkpair (
33mkpair (mksym "COMMON-LISP" "CDR") (mkpair (mksym "ACL2" "X") (mksym
34"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP"
35"NIL"))) (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL"))))) (
36mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP"
37"NIL") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mkpair (
38mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (
39mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (
40mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym
41"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym
42"COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym
43"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP"
44"NIL"))))) (mksym "COMMON-LISP" "NIL")))))
45,
46
47(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" "IFRP") (mkpair (
48mkpair (mksym "ACL2" "X") (mksym "COMMON-LISP" "NIL")) (mkpair (mkpair (mksym
49"COMMON-LISP" "IF") (mkpair (mkpair (mksym "COMMON-LISP" "NOT") (mkpair (
50mkpair (mksym "ACL2" "RCDP") (mkpair (mksym "ACL2" "X") (mksym "COMMON-LISP"
51"NIL"))) (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP"
52"NOT") (mkpair (mkpair (mksym "ACL2" "RCDP") (mkpair (mksym "ACL2" "X") (
53mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (
54mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "COMMON-LISP" "CONSP") (
55mkpair (mksym "ACL2" "X") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (
56mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "COMMON-LISP" "NULL") (
57mkpair (mkpair (mksym "COMMON-LISP" "CDR") (mkpair (mksym "ACL2" "X") (mksym
58"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym
59"COMMON-LISP" "IF") (mkpair (mkpair (mksym "COMMON-LISP" "CONSP") (mkpair (
60mkpair (mksym "COMMON-LISP" "CAR") (mkpair (mksym "ACL2" "X") (mksym
61"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym
62"COMMON-LISP" "IF") (mkpair (mkpair (mksym "COMMON-LISP" "NULL") (mkpair (
63mkpair (mksym "COMMON-LISP" "CAR") (mkpair (mkpair (mksym "COMMON-LISP" "CAR") (
64mkpair (mksym "ACL2" "X") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP"
65"NIL"))) (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "ACL2" "IFRP") (
66mkpair (mkpair (mksym "COMMON-LISP" "CDR") (mkpair (mkpair (mksym
67"COMMON-LISP" "CAR") (mkpair (mksym "ACL2" "X") (mksym "COMMON-LISP" "NIL"))) (
68mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (
69mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym
70"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym
71"COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym
72"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym
73"COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym
74"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym
75"COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym
76"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP"
77"NIL"))))) (mksym "COMMON-LISP" "NIL")))))
78,
79
80(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" "ACL2->RCD") (
81mkpair (mkpair (mksym "ACL2" "X") (mksym "COMMON-LISP" "NIL")) (mkpair (
82mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2" "IFRP") (
83mkpair (mksym "ACL2" "X") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (
84mksym "COMMON-LISP" "CONS") (mkpair (mkpair (mksym "COMMON-LISP" "CONS") (
85mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP"
86"NIL") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "X") (mksym
87"COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (
88mksym "COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP"
89"NIL")))) (mkpair (mksym "ACL2" "X") (mksym "COMMON-LISP" "NIL"))))) (mksym
90"COMMON-LISP" "NIL")))))
91,
92
93(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" "RCD->ACL2") (
94mkpair (mkpair (mksym "ACL2" "X") (mksym "COMMON-LISP" "NIL")) (mkpair (
95mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2" "IFRP") (
96mkpair (mksym "ACL2" "X") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (
97mksym "COMMON-LISP" "CDR") (mkpair (mkpair (mksym "COMMON-LISP" "CAR") (
98mkpair (mksym "ACL2" "X") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP"
99"NIL"))) (mkpair (mksym "ACL2" "X") (mksym "COMMON-LISP" "NIL"))))) (mksym
100"COMMON-LISP" "NIL")))))
101,
102
103(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" "G-AUX") (mkpair (
104mkpair (mksym "ACL2" "A") (mkpair (mksym "ACL2" "X") (mksym "COMMON-LISP"
105"NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym
106"COMMON-LISP" "IF") (mkpair (mkpair (mksym "COMMON-LISP" "ENDP") (mkpair (
107mksym "ACL2" "X") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym
108"COMMON-LISP" "ENDP") (mkpair (mksym "ACL2" "X") (mksym "COMMON-LISP" "NIL"))) (
109mkpair (mkpair (mksym "ACL2" "<<") (mkpair (mksym "ACL2" "A") (mkpair (mkpair (
110mksym "COMMON-LISP" "CAR") (mkpair (mkpair (mksym "COMMON-LISP" "CAR") (
111mkpair (mksym "ACL2" "X") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP"
112"NIL"))) (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL"))))) (
113mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP"
114"NIL") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP"
115"IF") (mkpair (mkpair (mksym "COMMON-LISP" "EQUAL") (mkpair (mksym "ACL2" "A") (
116mkpair (mkpair (mksym "COMMON-LISP" "CAR") (mkpair (mkpair (mksym
117"COMMON-LISP" "CAR") (mkpair (mksym "ACL2" "X") (mksym "COMMON-LISP" "NIL"))) (
118mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (
119mksym "COMMON-LISP" "CDR") (mkpair (mkpair (mksym "COMMON-LISP" "CAR") (
120mkpair (mksym "ACL2" "X") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP"
121"NIL"))) (mkpair (mkpair (mksym "ACL2" "G-AUX") (mkpair (mksym "ACL2" "A") (
122mkpair (mkpair (mksym "COMMON-LISP" "CDR") (mkpair (mksym "ACL2" "X") (mksym
123"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP"
124"NIL"))))) (mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL")))))
125,
126
127(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" "G") (mkpair (
128mkpair (mksym "ACL2" "A") (mkpair (mksym "ACL2" "X") (mksym "COMMON-LISP"
129"NIL"))) (mkpair (mkpair (mksym "ACL2" "G-AUX") (mkpair (mksym "ACL2" "A") (
130mkpair (mkpair (mksym "ACL2" "ACL2->RCD") (mkpair (mksym "ACL2" "X") (mksym
131"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP"
132"NIL")))))
133,
134
135(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" "S-AUX") (mkpair (
136mkpair (mksym "ACL2" "A") (mkpair (mksym "ACL2" "V") (mkpair (mksym "ACL2"
137"R") (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") (
138mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym
139"COMMON-LISP" "ENDP") (mkpair (mksym "ACL2" "R") (mksym "COMMON-LISP" "NIL"))) (
140mkpair (mkpair (mksym "COMMON-LISP" "ENDP") (mkpair (mksym "ACL2" "R") (mksym
141"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "ACL2" "<<") (mkpair (mksym
142"ACL2" "A") (mkpair (mkpair (mksym "COMMON-LISP" "CAR") (mkpair (mkpair (
143mksym "COMMON-LISP" "CAR") (mkpair (mksym "ACL2" "R") (mksym "COMMON-LISP"
144"NIL"))) (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) (mksym
145"COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (
146mksym "ACL2" "V") (mkpair (mkpair (mksym "COMMON-LISP" "CONS") (mkpair (
147mkpair (mksym "COMMON-LISP" "CONS") (mkpair (mksym "ACL2" "A") (mkpair (mksym
148"ACL2" "V") (mksym "COMMON-LISP" "NIL")))) (mkpair (mksym "ACL2" "R") (mksym
149"COMMON-LISP" "NIL")))) (mkpair (mksym "ACL2" "R") (mksym "COMMON-LISP" "NIL"))))) (
150mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym
151"COMMON-LISP" "EQUAL") (mkpair (mksym "ACL2" "A") (mkpair (mkpair (mksym
152"COMMON-LISP" "CAR") (mkpair (mkpair (mksym "COMMON-LISP" "CAR") (mkpair (
153mksym "ACL2" "R") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))) (
154mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") (
155mkpair (mksym "ACL2" "V") (mkpair (mkpair (mksym "COMMON-LISP" "CONS") (
156mkpair (mkpair (mksym "COMMON-LISP" "CONS") (mkpair (mksym "ACL2" "A") (
157mkpair (mksym "ACL2" "V") (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (
158mksym "COMMON-LISP" "CDR") (mkpair (mksym "ACL2" "R") (mksym "COMMON-LISP"
159"NIL"))) (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "COMMON-LISP"
160"CDR") (mkpair (mksym "ACL2" "R") (mksym "COMMON-LISP" "NIL"))) (mksym
161"COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym "COMMON-LISP" "CONS") (mkpair (
162mkpair (mksym "COMMON-LISP" "CAR") (mkpair (mksym "ACL2" "R") (mksym
163"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "ACL2" "S-AUX") (mkpair (mksym
164"ACL2" "A") (mkpair (mksym "ACL2" "V") (mkpair (mkpair (mksym "COMMON-LISP"
165"CDR") (mkpair (mksym "ACL2" "R") (mksym "COMMON-LISP" "NIL"))) (mksym
166"COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP"
167"NIL"))))) (mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL")))))
168,
169
170(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" "S") (mkpair (
171mkpair (mksym "ACL2" "A") (mkpair (mksym "ACL2" "V") (mkpair (mksym "ACL2"
172"X") (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "ACL2" "RCD->ACL2") (
173mkpair (mkpair (mksym "ACL2" "S-AUX") (mkpair (mksym "ACL2" "A") (mkpair (
174mksym "ACL2" "V") (mkpair (mkpair (mksym "ACL2" "ACL2->RCD") (mkpair (mksym
175"ACL2" "X") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (
176mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))))
177,
178
179(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" "KEYS-AUX") (
180mkpair (mkpair (mksym "ACL2" "X") (mksym "COMMON-LISP" "NIL")) (mkpair (
181mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "COMMON-LISP" "ENDP") (
182mkpair (mksym "ACL2" "X") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (
183mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym
184"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "CONS") (mkpair (
185mkpair (mksym "COMMON-LISP" "CAR") (mkpair (mkpair (mksym "COMMON-LISP" "CAR") (
186mkpair (mksym "ACL2" "X") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP"
187"NIL"))) (mkpair (mkpair (mksym "ACL2" "KEYS-AUX") (mkpair (mkpair (mksym
188"COMMON-LISP" "CDR") (mkpair (mksym "ACL2" "X") (mksym "COMMON-LISP" "NIL"))) (
189mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) (mksym
190"COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL")))))
191,
192
193(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" "KEYS") (mkpair (
194mkpair (mksym "ACL2" "X") (mksym "COMMON-LISP" "NIL")) (mkpair (mkpair (mksym
195"ACL2" "KEYS-AUX") (mkpair (mkpair (mksym "ACL2" "ACL2->RCD") (mkpair (mksym
196"ACL2" "X") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))) (
197mksym "COMMON-LISP" "NIL")))))
198,
199
200(mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "ACL2" "G-SAME-S") (mkpair (
201mkpair (mksym "COMMON-LISP" "EQUAL") (mkpair (mkpair (mksym "ACL2" "G") (
202mkpair (mksym "ACL2" "A") (mkpair (mkpair (mksym "ACL2" "S") (mkpair (mksym
203"ACL2" "A") (mkpair (mksym "ACL2" "V") (mkpair (mksym "ACL2" "R") (mksym
204"COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL")))) (mkpair (mksym "ACL2"
205"V") (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL"))))
206,
207
208(mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "ACL2" "G-DIFF-S") (mkpair (
209mkpair (mksym "ACL2" "IMPLIES") (mkpair (mkpair (mksym "COMMON-LISP" "NOT") (
210mkpair (mkpair (mksym "COMMON-LISP" "EQUAL") (mkpair (mksym "ACL2" "A") (
211mkpair (mksym "ACL2" "B") (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP"
212"NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "EQUAL") (mkpair (mkpair (mksym
213"ACL2" "G") (mkpair (mksym "ACL2" "A") (mkpair (mkpair (mksym "ACL2" "S") (
214mkpair (mksym "ACL2" "B") (mkpair (mksym "ACL2" "V") (mkpair (mksym "ACL2"
215"R") (mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL")))) (mkpair (
216mkpair (mksym "ACL2" "G") (mkpair (mksym "ACL2" "A") (mkpair (mksym "ACL2"
217"R") (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) (mksym
218"COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL"))))
219,
220
221(mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "ACL2" "G-OF-S-REDUX") (mkpair (
222mkpair (mksym "COMMON-LISP" "EQUAL") (mkpair (mkpair (mksym "ACL2" "G") (
223mkpair (mksym "ACL2" "A") (mkpair (mkpair (mksym "ACL2" "S") (mkpair (mksym
224"ACL2" "B") (mkpair (mksym "ACL2" "V") (mkpair (mksym "ACL2" "R") (mksym
225"COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (
226mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "COMMON-LISP" "EQUAL") (
227mkpair (mksym "ACL2" "A") (mkpair (mksym "ACL2" "B") (mksym "COMMON-LISP"
228"NIL")))) (mkpair (mksym "ACL2" "V") (mkpair (mkpair (mksym "ACL2" "G") (
229mkpair (mksym "ACL2" "A") (mkpair (mksym "ACL2" "R") (mksym "COMMON-LISP"
230"NIL")))) (mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL")))) (
231mksym "COMMON-LISP" "NIL"))))
232,
233
234(mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "ACL2" "S-SAME-G") (mkpair (
235mkpair (mksym "COMMON-LISP" "EQUAL") (mkpair (mkpair (mksym "ACL2" "S") (
236mkpair (mksym "ACL2" "A") (mkpair (mkpair (mksym "ACL2" "G") (mkpair (mksym
237"ACL2" "A") (mkpair (mksym "ACL2" "R") (mksym "COMMON-LISP" "NIL")))) (mkpair (
238mksym "ACL2" "R") (mksym "COMMON-LISP" "NIL"))))) (mkpair (mksym "ACL2" "R") (
239mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL"))))
240,
241
242(mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "ACL2" "S-SAME-S") (mkpair (
243mkpair (mksym "COMMON-LISP" "EQUAL") (mkpair (mkpair (mksym "ACL2" "S") (
244mkpair (mksym "ACL2" "A") (mkpair (mksym "ACL2" "Y") (mkpair (mkpair (mksym
245"ACL2" "S") (mkpair (mksym "ACL2" "A") (mkpair (mksym "ACL2" "X") (mkpair (
246mksym "ACL2" "R") (mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL"))))) (
247mkpair (mkpair (mksym "ACL2" "S") (mkpair (mksym "ACL2" "A") (mkpair (mksym
248"ACL2" "Y") (mkpair (mksym "ACL2" "R") (mksym "COMMON-LISP" "NIL"))))) (mksym
249"COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL"))))
250,
251
252(mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "ACL2" "S-DIFF-S") (mkpair (
253mkpair (mksym "ACL2" "IMPLIES") (mkpair (mkpair (mksym "COMMON-LISP" "NOT") (
254mkpair (mkpair (mksym "COMMON-LISP" "EQUAL") (mkpair (mksym "ACL2" "A") (
255mkpair (mksym "ACL2" "B") (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP"
256"NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "EQUAL") (mkpair (mkpair (mksym
257"ACL2" "S") (mkpair (mksym "ACL2" "B") (mkpair (mksym "ACL2" "Y") (mkpair (
258mkpair (mksym "ACL2" "S") (mkpair (mksym "ACL2" "A") (mkpair (mksym "ACL2"
259"X") (mkpair (mksym "ACL2" "R") (mksym "COMMON-LISP" "NIL"))))) (mksym
260"COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym "ACL2" "S") (mkpair (mksym
261"ACL2" "A") (mkpair (mksym "ACL2" "X") (mkpair (mkpair (mksym "ACL2" "S") (
262mkpair (mksym "ACL2" "B") (mkpair (mksym "ACL2" "Y") (mkpair (mksym "ACL2"
263"R") (mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL"))))) (mksym
264"COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP"
265"NIL"))))
266,
267
268(mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "ACL2" "G-KEYS-RELATIONSHIP") (
269mkpair (mkpair (mksym "ACL2" "IFF") (mkpair (mkpair (mksym "ACL2" "MEMBERP") (
270mkpair (mksym "ACL2" "A") (mkpair (mkpair (mksym "ACL2" "KEYS") (mkpair (
271mksym "ACL2" "R") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) (
272mkpair (mkpair (mksym "ACL2" "G") (mkpair (mksym "ACL2" "A") (mkpair (mksym
273"ACL2" "R") (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) (
274mksym "COMMON-LISP" "NIL"))))
275,
276
277(mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "ACL2" "S-KEYS-REDUCTION") (
278mkpair (mkpair (mksym "COMMON-LISP" "EQUAL") (mkpair (mkpair (mksym "ACL2"
279"KEYS") (mkpair (mkpair (mksym "ACL2" "S") (mkpair (mksym "ACL2" "A") (mkpair (
280mksym "ACL2" "V") (mkpair (mksym "ACL2" "R") (mksym "COMMON-LISP" "NIL"))))) (
281mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") (
282mkpair (mksym "ACL2" "V") (mkpair (mkpair (mksym "ACL2" "INSERT") (mkpair (
283mksym "ACL2" "A") (mkpair (mkpair (mksym "ACL2" "KEYS") (mkpair (mksym "ACL2"
284"R") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) (mkpair (
285mkpair (mksym "ACL2" "DROP") (mkpair (mksym "ACL2" "A") (mkpair (mkpair (
286mksym "ACL2" "KEYS") (mkpair (mksym "ACL2" "R") (mksym "COMMON-LISP" "NIL"))) (
287mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL"))))) (mksym
288"COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL"))))
289,
290
291(mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "ACL2" "KEYS-ARE-ORDERED") (
292mkpair (mkpair (mksym "ACL2" "ORDEREDP") (mkpair (mkpair (mksym "ACL2" "KEYS") (
293mkpair (mksym "ACL2" "R") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP"
294"NIL"))) (mksym "COMMON-LISP" "NIL"))))
295,
296
297(mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "ACL2" "G-OF-NIL-IS-NIL") (
298mkpair (mkpair (mksym "COMMON-LISP" "NOT") (mkpair (mkpair (mksym "ACL2" "G") (
299mkpair (mksym "ACL2" "A") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (
300mkpair (mksym "COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) (mksym
301"COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP"
302"NIL"))))
303,
304
305(mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "ACL2"
306"S-NON-NIL-CANNOT-BE-NIL") (mkpair (mkpair (mksym "ACL2" "IMPLIES") (mkpair (
307mksym "ACL2" "V") (mkpair (mkpair (mksym "ACL2" "S") (mkpair (mksym "ACL2"
308"A") (mkpair (mksym "ACL2" "V") (mkpair (mksym "ACL2" "R") (mksym
309"COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP"
310"NIL"))))
311,
312
313(mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "ACL2" "NON-NIL-IF-G-NON-NIL") (
314mkpair (mkpair (mksym "ACL2" "IMPLIES") (mkpair (mkpair (mksym "ACL2" "G") (
315mkpair (mksym "ACL2" "A") (mkpair (mksym "ACL2" "R") (mksym "COMMON-LISP"
316"NIL")))) (mkpair (mksym "ACL2" "R") (mksym "COMMON-LISP" "NIL")))) (mksym
317"COMMON-LISP" "NIL"))))
318,
319
320(mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "ACL2"
321"S-SAME-G-BACK-CHAINING") (mkpair (mkpair (mksym "ACL2" "IMPLIES") (mkpair (
322mkpair (mksym "COMMON-LISP" "EQUAL") (mkpair (mksym "ACL2" "V") (mkpair (
323mkpair (mksym "ACL2" "G") (mkpair (mksym "ACL2" "A") (mkpair (mksym "ACL2"
324"R") (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) (mkpair (
325mkpair (mksym "COMMON-LISP" "EQUAL") (mkpair (mkpair (mksym "ACL2" "S") (
326mkpair (mksym "ACL2" "A") (mkpair (mksym "ACL2" "V") (mkpair (mksym "ACL2"
327"R") (mksym "COMMON-LISP" "NIL"))))) (mkpair (mksym "ACL2" "R") (mksym
328"COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP"
329"NIL"))))
330,
331
332(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" "UPDATE-MACRO") (
333mkpair (mkpair (mksym "ACL2" "UPDS") (mkpair (mksym "ACL2" "RESULT") (mksym
334"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (
335mkpair (mksym "COMMON-LISP" "ENDP") (mkpair (mksym "ACL2" "UPDS") (mksym
336"COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "RESULT") (mkpair (mkpair (mksym
337"ACL2" "UPDATE-MACRO") (mkpair (mkpair (mksym "COMMON-LISP" "CDR") (mkpair (
338mkpair (mksym "COMMON-LISP" "CDR") (mkpair (mksym "ACL2" "UPDS") (mksym
339"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym
340"COMMON-LISP" "CONS") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (
341mksym "ACL2" "S") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym
342"COMMON-LISP" "CONS") (mkpair (mkpair (mksym "COMMON-LISP" "CAR") (mkpair (
343mksym "ACL2" "UPDS") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym
344"COMMON-LISP" "CONS") (mkpair (mkpair (mksym "COMMON-LISP" "CAR") (mkpair (
345mkpair (mksym "COMMON-LISP" "CDR") (mkpair (mksym "ACL2" "UPDS") (mksym
346"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym
347"COMMON-LISP" "CONS") (mkpair (mksym "ACL2" "RESULT") (mkpair (mkpair (mksym
348"COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym
349"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP"
350"NIL")))) (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) (
351mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL"))))) (mksym
352"COMMON-LISP" "NIL")))))
353
354];
355