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" "SUBSET") (mkpair (
9mkpair (mksym "ACL2" "X") (mkpair (mksym "ACL2" "Y") (mksym "COMMON-LISP"
10"NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym
11"COMMON-LISP" "ENDP") (mkpair (mksym "ACL2" "X") (mksym "COMMON-LISP" "NIL"))) (
12mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "T") (
13mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") (
14mkpair (mkpair (mksym "ACL2" "MEMBERP") (mkpair (mkpair (mksym "COMMON-LISP"
15"CAR") (mkpair (mksym "ACL2" "X") (mksym "COMMON-LISP" "NIL"))) (mkpair (
16mksym "ACL2" "Y") (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym
17"ACL2" "SUBSET") (mkpair (mkpair (mksym "COMMON-LISP" "CDR") (mkpair (mksym
18"ACL2" "X") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "Y") (mksym
19"COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (
20mksym "COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP"
21"NIL"))))) (mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL")))))
22,
23
24(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" "SET-INTERSECT") (
25mkpair (mkpair (mksym "ACL2" "X") (mkpair (mksym "ACL2" "Y") (mksym
26"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (
27mkpair (mksym "COMMON-LISP" "ENDP") (mkpair (mksym "ACL2" "X") (mksym
28"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (
29mksym "COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (
30mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2" "MEMBERP") (mkpair (
31mkpair (mksym "COMMON-LISP" "CAR") (mkpair (mksym "ACL2" "X") (mksym
32"COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "Y") (mksym "COMMON-LISP" "NIL")))) (
33mkpair (mkpair (mksym "COMMON-LISP" "CONS") (mkpair (mkpair (mksym
34"COMMON-LISP" "CAR") (mkpair (mksym "ACL2" "X") (mksym "COMMON-LISP" "NIL"))) (
35mkpair (mkpair (mksym "ACL2" "SET-INTERSECT") (mkpair (mkpair (mksym
36"COMMON-LISP" "CDR") (mkpair (mksym "ACL2" "X") (mksym "COMMON-LISP" "NIL"))) (
37mkpair (mksym "ACL2" "Y") (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP"
38"NIL")))) (mkpair (mkpair (mksym "ACL2" "SET-INTERSECT") (mkpair (mkpair (
39mksym "COMMON-LISP" "CDR") (mkpair (mksym "ACL2" "X") (mksym "COMMON-LISP"
40"NIL"))) (mkpair (mksym "ACL2" "Y") (mksym "COMMON-LISP" "NIL")))) (mksym
41"COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP"
42"NIL")))))
43,
44
45(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" "SET-UNION") (
46mkpair (mkpair (mksym "ACL2" "X") (mkpair (mksym "ACL2" "Y") (mksym
47"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (
48mkpair (mksym "COMMON-LISP" "ENDP") (mkpair (mksym "ACL2" "X") (mksym
49"COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "Y") (mkpair (mkpair (mksym
50"COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2" "MEMBERP") (mkpair (mkpair (
51mksym "COMMON-LISP" "CAR") (mkpair (mksym "ACL2" "X") (mksym "COMMON-LISP"
52"NIL"))) (mkpair (mksym "ACL2" "Y") (mksym "COMMON-LISP" "NIL")))) (mkpair (
53mkpair (mksym "ACL2" "SET-UNION") (mkpair (mkpair (mksym "COMMON-LISP" "CDR") (
54mkpair (mksym "ACL2" "X") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2"
55"Y") (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "COMMON-LISP"
56"CONS") (mkpair (mkpair (mksym "COMMON-LISP" "CAR") (mkpair (mksym "ACL2" "X") (
57mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "ACL2" "SET-UNION") (
58mkpair (mkpair (mksym "COMMON-LISP" "CDR") (mkpair (mksym "ACL2" "X") (mksym
59"COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "Y") (mksym "COMMON-LISP" "NIL")))) (
60mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL"))))) (mksym
61"COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL")))))
62,
63
64(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" "SET-EQUAL") (
65mkpair (mkpair (mksym "ACL2" "X") (mkpair (mksym "ACL2" "Y") (mksym
66"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (
67mkpair (mksym "ACL2" "SUBSET") (mkpair (mksym "ACL2" "X") (mkpair (mksym
68"ACL2" "Y") (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "ACL2"
69"SUBSET") (mkpair (mksym "ACL2" "Y") (mkpair (mksym "ACL2" "X") (mksym
70"COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (
71mksym "COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP"
72"NIL"))))) (mksym "COMMON-LISP" "NIL")))))
73,
74
75(mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "ACL2" "SUBSET-IS-REFLEXIVE") (
76mkpair (mkpair (mksym "ACL2" "SUBSET") (mkpair (mksym "ACL2" "X") (mkpair (
77mksym "ACL2" "X") (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL"))))
78,
79
80(mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "ACL2" "SUBSET-IS-TRANSITIVE") (
81mkpair (mkpair (mksym "ACL2" "IMPLIES") (mkpair (mkpair (mksym "COMMON-LISP"
82"IF") (mkpair (mkpair (mksym "ACL2" "SUBSET") (mkpair (mksym "ACL2" "X") (
83mkpair (mksym "ACL2" "Y") (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (
84mksym "ACL2" "SUBSET") (mkpair (mksym "ACL2" "Y") (mkpair (mksym "ACL2" "Z") (
85mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (
86mkpair (mksym "COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) (mksym
87"COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym "ACL2" "SUBSET") (mkpair (
88mksym "ACL2" "X") (mkpair (mksym "ACL2" "Z") (mksym "COMMON-LISP" "NIL")))) (
89mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL"))))
90,
91
92(mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "ACL2"
93"SUBSET-OF-EMPTY-IS-EMPTY") (mkpair (mkpair (mksym "ACL2" "IMPLIES") (mkpair (
94mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "COMMON-LISP" "NOT") (
95mkpair (mkpair (mksym "COMMON-LISP" "CONSP") (mkpair (mksym "ACL2" "X") (
96mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (
97mksym "ACL2" "SUBSET") (mkpair (mksym "ACL2" "Y") (mkpair (mksym "ACL2" "X") (
98mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (
99mkpair (mksym "COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) (mksym
100"COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym "COMMON-LISP" "NOT") (mkpair (
101mkpair (mksym "COMMON-LISP" "CONSP") (mkpair (mksym "ACL2" "Y") (mksym
102"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP"
103"NIL")))) (mksym "COMMON-LISP" "NIL"))))
104,
105
106(mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "ACL2"
107"SET-EQUAL-IS-AN-EQUIVALENCE") (mkpair (mkpair (mksym "COMMON-LISP" "IF") (
108mkpair (mkpair (mksym "ACL2" "BOOLEANP") (mkpair (mkpair (mksym "ACL2"
109"SET-EQUAL") (mkpair (mksym "ACL2" "X") (mkpair (mksym "ACL2" "Y") (mksym
110"COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym
111"COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2" "SET-EQUAL") (mkpair (mksym
112"ACL2" "X") (mkpair (mksym "ACL2" "X") (mksym "COMMON-LISP" "NIL")))) (mkpair (
113mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2" "IMPLIES") (
114mkpair (mkpair (mksym "ACL2" "SET-EQUAL") (mkpair (mksym "ACL2" "X") (mkpair (
115mksym "ACL2" "Y") (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym
116"ACL2" "SET-EQUAL") (mkpair (mksym "ACL2" "Y") (mkpair (mksym "ACL2" "X") (
117mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (
118mksym "ACL2" "IMPLIES") (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (
119mkpair (mksym "ACL2" "SET-EQUAL") (mkpair (mksym "ACL2" "X") (mkpair (mksym
120"ACL2" "Y") (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "ACL2"
121"SET-EQUAL") (mkpair (mksym "ACL2" "Y") (mkpair (mksym "ACL2" "Z") (mksym
122"COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (
123mksym "COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP"
124"NIL"))))) (mkpair (mkpair (mksym "ACL2" "SET-EQUAL") (mkpair (mksym "ACL2"
125"X") (mkpair (mksym "ACL2" "Z") (mksym "COMMON-LISP" "NIL")))) (mksym
126"COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (
127mksym "COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP"
128"NIL"))))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym
129"COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (
130mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP"
131"NIL") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mksym
132"COMMON-LISP" "NIL"))))
133,
134
135(mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "ACL2"
136"SUBSET-IS-ANTISYMMETRIC") (mkpair (mkpair (mksym "ACL2" "IMPLIES") (mkpair (
137mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2" "SUBSET") (
138mkpair (mksym "ACL2" "X") (mkpair (mksym "ACL2" "Y") (mksym "COMMON-LISP"
139"NIL")))) (mkpair (mkpair (mksym "ACL2" "SUBSET") (mkpair (mksym "ACL2" "Y") (
140mkpair (mksym "ACL2" "X") (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (
141mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym
142"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym
143"ACL2" "SET-EQUAL") (mkpair (mksym "ACL2" "X") (mkpair (mksym "ACL2" "Y") (
144mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) (mksym
145"COMMON-LISP" "NIL"))))
146,
147
148(mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "ACL2"
149"INTERSECT-IS-A-SUBSET-1") (mkpair (mkpair (mksym "ACL2" "SUBSET") (mkpair (
150mkpair (mksym "ACL2" "SET-INTERSECT") (mkpair (mksym "ACL2" "X") (mkpair (
151mksym "ACL2" "Y") (mksym "COMMON-LISP" "NIL")))) (mkpair (mksym "ACL2" "X") (
152mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL"))))
153,
154
155(mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "ACL2"
156"INTERSECT-IS-A-SUBSET-2") (mkpair (mkpair (mksym "ACL2" "SUBSET") (mkpair (
157mkpair (mksym "ACL2" "SET-INTERSECT") (mkpair (mksym "ACL2" "X") (mkpair (
158mksym "ACL2" "Y") (mksym "COMMON-LISP" "NIL")))) (mkpair (mksym "ACL2" "Y") (
159mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL"))))
160,
161
162(mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "ACL2" "UNION-IS-A-SUBSET-1") (
163mkpair (mkpair (mksym "ACL2" "SUBSET") (mkpair (mksym "ACL2" "X") (mkpair (
164mkpair (mksym "ACL2" "SET-UNION") (mkpair (mksym "ACL2" "X") (mkpair (mksym
165"ACL2" "Y") (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) (
166mksym "COMMON-LISP" "NIL"))))
167,
168
169(mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "ACL2" "UNION-IS-A-SUBSET-2") (
170mkpair (mkpair (mksym "ACL2" "SUBSET") (mkpair (mksym "ACL2" "Y") (mkpair (
171mkpair (mksym "ACL2" "SET-UNION") (mkpair (mksym "ACL2" "X") (mkpair (mksym
172"ACL2" "Y") (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) (
173mksym "COMMON-LISP" "NIL"))))
174,
175
176(mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "ACL2"
177"SUPERSET-CONTAINS-EVERYTHING") (mkpair (mkpair (mksym "ACL2" "IMPLIES") (
178mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2"
179"MEMBERP") (mkpair (mksym "ACL2" "E") (mkpair (mksym "ACL2" "X") (mksym
180"COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "ACL2" "SUBSET") (mkpair (
181mksym "ACL2" "X") (mkpair (mksym "ACL2" "Y") (mksym "COMMON-LISP" "NIL")))) (
182mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP"
183"NIL") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mkpair (
184mkpair (mksym "ACL2" "MEMBERP") (mkpair (mksym "ACL2" "E") (mkpair (mksym
185"ACL2" "Y") (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) (
186mksym "COMMON-LISP" "NIL"))))
187,
188
189(mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "ACL2" "SUBSET-OF-NIL-IS-NIL") (
190mkpair (mkpair (mksym "ACL2" "IMPLIES") (mkpair (mkpair (mksym "COMMON-LISP"
191"IF") (mkpair (mkpair (mksym "COMMON-LISP" "NOT") (mkpair (mkpair (mksym
192"COMMON-LISP" "CONSP") (mkpair (mksym "ACL2" "Y") (mksym "COMMON-LISP" "NIL"))) (
193mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "ACL2" "SUBSET") (mkpair (
194mksym "ACL2" "X") (mkpair (mksym "ACL2" "Y") (mksym "COMMON-LISP" "NIL")))) (
195mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP"
196"NIL") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mkpair (
197mkpair (mksym "COMMON-LISP" "NOT") (mkpair (mkpair (mksym "COMMON-LISP"
198"CONSP") (mkpair (mksym "ACL2" "X") (mksym "COMMON-LISP" "NIL"))) (mksym
199"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP"
200"NIL"))))
201,
202
203(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" "PROPER-SUBSET") (
204mkpair (mkpair (mksym "ACL2" "X") (mkpair (mksym "ACL2" "Y") (mksym
205"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (
206mkpair (mksym "ACL2" "SUBSET") (mkpair (mksym "ACL2" "X") (mkpair (mksym
207"ACL2" "Y") (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym
208"COMMON-LISP" "NOT") (mkpair (mkpair (mksym "ACL2" "SUBSET") (mkpair (mksym
209"ACL2" "Y") (mkpair (mksym "ACL2" "X") (mksym "COMMON-LISP" "NIL")))) (mksym
210"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (
211mksym "COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP"
212"NIL"))))) (mksym "COMMON-LISP" "NIL")))))
213,
214
215(mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "ACL2"
216"PROPER-SUBSET-IS-IRREFLEXIVE") (mkpair (mkpair (mksym "COMMON-LISP" "NOT") (
217mkpair (mkpair (mksym "ACL2" "PROPER-SUBSET") (mkpair (mksym "ACL2" "X") (
218mkpair (mksym "ACL2" "X") (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP"
219"NIL"))) (mksym "COMMON-LISP" "NIL"))))
220,
221
222(mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "ACL2"
223"PROPER-SUBSET-IS-TRANSITIVE") (mkpair (mkpair (mksym "ACL2" "IMPLIES") (
224mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2"
225"PROPER-SUBSET") (mkpair (mksym "ACL2" "X") (mkpair (mksym "ACL2" "Y") (mksym
226"COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "ACL2" "PROPER-SUBSET") (
227mkpair (mksym "ACL2" "Y") (mkpair (mksym "ACL2" "Z") (mksym "COMMON-LISP"
228"NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym
229"COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (
230mkpair (mkpair (mksym "ACL2" "PROPER-SUBSET") (mkpair (mksym "ACL2" "X") (
231mkpair (mksym "ACL2" "Z") (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP"
232"NIL")))) (mksym "COMMON-LISP" "NIL"))))
233,
234
235(mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "ACL2"
236"PROPER-SUBSET-IS-STRONGER-THAN-SUBSET") (mkpair (mkpair (mksym "ACL2"
237"IMPLIES") (mkpair (mkpair (mksym "ACL2" "PROPER-SUBSET") (mkpair (mksym
238"ACL2" "X") (mkpair (mksym "ACL2" "Y") (mksym "COMMON-LISP" "NIL")))) (mkpair (
239mkpair (mksym "ACL2" "SUBSET") (mkpair (mksym "ACL2" "X") (mkpair (mksym
240"ACL2" "Y") (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) (
241mksym "COMMON-LISP" "NIL"))))
242
243];
244