1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
|
(NO-DUPLICATESP-OF-MEMBER
(360 21 (:DEFINITION NO-DUPLICATESP-EQUAL))
(106 53 (:REWRITE SUBSETP-MEMBER . 3))
(79 79 (:REWRITE DEFAULT-CDR))
(63 63 (:REWRITE DEFAULT-CAR))
(58 58 (:REWRITE SUBSETP-MEMBER . 2))
(58 58 (:REWRITE SUBSETP-MEMBER . 1))
(53 53 (:REWRITE SUBSETP-MEMBER . 4))
(50 2 (:DEFINITION SUBSETP-EQUAL))
(12 12 (:REWRITE FLATTEN-WHEN-NOT-CONSP))
(7 7 (:TYPE-PRESCRIPTION SUBSETP-EQUAL))
(4 4 (:REWRITE SUBSETP-TRANS2))
(4 4 (:REWRITE SUBSETP-TRANS))
)
(LEN-OF-FLATTEN-OF-UPDATE-NTH
(273 151 (:REWRITE DEFAULT-+-2))
(189 151 (:REWRITE DEFAULT-+-1))
(141 35 (:REWRITE ZP-OPEN))
(114 16 (:REWRITE NFIX-WHEN-ZP))
(82 67 (:REWRITE DEFAULT-<-2))
(67 67 (:REWRITE DEFAULT-<-1))
(52 52 (:LINEAR POSITION-WHEN-MEMBER))
(52 52 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
(49 25 (:REWRITE FOLD-CONSTS-IN-+))
(45 5 (:REWRITE CONSP-OF-NTH-WHEN-ALISTP))
(30 5 (:DEFINITION ALISTP))
(25 25 (:TYPE-PRESCRIPTION ALISTP))
(20 10 (:REWRITE DEFAULT-UNARY-MINUS))
(18 6 (:DEFINITION NFIX))
(18 6 (:DEFINITION NATP))
(16 9 (:TYPE-PRESCRIPTION TRUE-LISTP-UPDATE-NTH))
(16 4 (:REWRITE APPEND-ATOM-UNDER-LIST-EQUIV))
(14 2 (:DEFINITION BINARY-APPEND))
(7 7 (:TYPE-PRESCRIPTION TRUE-LISTP))
(6 6 (:TYPE-PRESCRIPTION NATP))
)
(NOT-INTERSECTP-LIST
(18 2 (:REWRITE TRUE-LISTP-WHEN-STRING-LIST))
(12 2 (:DEFINITION STRING-LISTP))
(11 1 (:DEFINITION TRUE-LISTP))
(10 10 (:TYPE-PRESCRIPTION STRING-LISTP))
(4 4 (:REWRITE DEFAULT-CDR))
(4 4 (:REWRITE DEFAULT-CAR))
)
(LIST-EQUIV-IMPLIES-EQUAL-NOT-INTERSECTP-LIST-1
(2294 124 (:REWRITE NO-DUPLICATESP-OF-MEMBER))
(1922 124 (:DEFINITION NO-DUPLICATESP-EQUAL))
(793 793 (:REWRITE DEFAULT-CDR))
(774 655 (:REWRITE SUBSETP-MEMBER . 1))
(740 740 (:REWRITE DEFAULT-CAR))
(655 655 (:REWRITE SUBSETP-MEMBER . 2))
(620 620 (:TYPE-PRESCRIPTION NO-DUPLICATESP-EQUAL))
(509 107 (:REWRITE INTERSECT-WITH-SUBSET . 8))
(491 107 (:REWRITE INTERSECT-WITH-SUBSET . 2))
(398 398 (:REWRITE SUBSETP-TRANS2))
(398 398 (:REWRITE SUBSETP-TRANS))
(363 107 (:REWRITE INTERSECT-WITH-SUBSET . 12))
(322 124 (:REWRITE SUBSETP-MEMBER . 3))
(315 107 (:REWRITE INTERSECT-WITH-SUBSET . 5))
(243 107 (:REWRITE INTERSECT-WITH-SUBSET . 11))
(171 107 (:REWRITE INTERSECT-WITH-SUBSET . 6))
(124 124 (:REWRITE SUBSETP-MEMBER . 4))
(123 107 (:REWRITE INTERSECT-WITH-SUBSET . 9))
(123 107 (:REWRITE INTERSECT-WITH-SUBSET . 3))
(107 107 (:REWRITE INTERSECT-WITH-SUBSET . 10))
(107 107 (:REWRITE INTERSECT-WITH-SUBSET . 7))
(107 107 (:REWRITE INTERSECT-WITH-SUBSET . 4))
(107 107 (:REWRITE INTERSECT-WITH-SUBSET . 1))
(18 18 (:REWRITE LIST-EQUIV-WHEN-ATOM-RIGHT))
(18 18 (:REWRITE LIST-EQUIV-WHEN-ATOM-LEFT))
)
(NOT-INTERSECTP-LIST-CORRECTNESS-1
(3992 356 (:DEFINITION MEMBER-EQUAL))
(2109 114 (:REWRITE NO-DUPLICATESP-OF-MEMBER))
(1767 114 (:DEFINITION NO-DUPLICATESP-EQUAL))
(1109 118 (:REWRITE INTERSECT-WITH-SUBSET . 5))
(878 878 (:REWRITE DEFAULT-CDR))
(865 754 (:REWRITE SUBSETP-MEMBER . 2))
(783 783 (:REWRITE DEFAULT-CAR))
(754 754 (:REWRITE SUBSETP-MEMBER . 1))
(733 477 (:REWRITE SUBSETP-TRANS2))
(692 7 (:REWRITE SUBSETP-APPEND1))
(620 620 (:TYPE-PRESCRIPTION TRUE-LISTP-OF-FLATTEN))
(570 570 (:TYPE-PRESCRIPTION NO-DUPLICATESP-EQUAL))
(477 477 (:REWRITE SUBSETP-TRANS))
(329 118 (:REWRITE INTERSECT-WITH-SUBSET . 3))
(319 118 (:REWRITE INTERSECT-WITH-SUBSET . 11))
(278 118 (:REWRITE INTERSECT-WITH-SUBSET . 8))
(246 118 (:REWRITE INTERSECT-WITH-SUBSET . 9))
(158 118 (:REWRITE INTERSECT-WITH-SUBSET . 2))
(118 118 (:REWRITE INTERSECT-WITH-SUBSET . 10))
(118 118 (:REWRITE INTERSECT-WITH-SUBSET . 7))
(118 118 (:REWRITE INTERSECT-WITH-SUBSET . 6))
(118 118 (:REWRITE INTERSECT-WITH-SUBSET . 4))
(118 118 (:REWRITE INTERSECT-WITH-SUBSET . 1))
(114 114 (:REWRITE SUBSETP-MEMBER . 4))
(114 114 (:REWRITE SUBSETP-MEMBER . 3))
(56 2 (:REWRITE MEMBER-OF-BINARY-APPEND))
(3 1 (:DEFINITION BINARY-APPEND))
)
(NOT-INTERSECTP-LIST-CORRECTNESS-2
(454 23 (:DEFINITION SUBSETP-EQUAL))
(355 19 (:REWRITE NO-DUPLICATESP-OF-MEMBER))
(350 14 (:REWRITE INTERSECTP-WHEN-SUBSETP))
(298 19 (:DEFINITION NO-DUPLICATESP-EQUAL))
(126 14 (:REWRITE INTERSECT-WITH-SUBSET . 5))
(113 113 (:REWRITE DEFAULT-CDR))
(112 112 (:TYPE-PRESCRIPTION SUBSETP-EQUAL))
(101 101 (:REWRITE DEFAULT-CAR))
(95 95 (:TYPE-PRESCRIPTION NO-DUPLICATESP-EQUAL))
(93 93 (:REWRITE SUBSETP-MEMBER . 2))
(93 93 (:REWRITE SUBSETP-MEMBER . 1))
(72 19 (:REWRITE SUBSETP-MEMBER . 3))
(54 14 (:REWRITE INTERSECT-WITH-SUBSET . 2))
(46 46 (:REWRITE SUBSETP-TRANS2))
(46 46 (:REWRITE SUBSETP-TRANS))
(19 19 (:REWRITE SUBSETP-MEMBER . 4))
(14 14 (:REWRITE INTERSECT-WITH-SUBSET . 12))
(14 14 (:REWRITE INTERSECT-WITH-SUBSET . 11))
(14 14 (:REWRITE INTERSECT-WITH-SUBSET . 10))
(14 14 (:REWRITE INTERSECT-WITH-SUBSET . 9))
(14 14 (:REWRITE INTERSECT-WITH-SUBSET . 8))
(14 14 (:REWRITE INTERSECT-WITH-SUBSET . 7))
(14 14 (:REWRITE INTERSECT-WITH-SUBSET . 6))
(14 14 (:REWRITE INTERSECT-WITH-SUBSET . 4))
(14 14 (:REWRITE INTERSECT-WITH-SUBSET . 3))
(14 14 (:REWRITE INTERSECT-WITH-SUBSET . 1))
)
(NOT-INTERSECTP-LIST-OF-APPEND-1
(1681 80 (:DEFINITION SUBSETP-EQUAL))
(1648 138 (:DEFINITION MEMBER-EQUAL))
(1618 58 (:REWRITE INTERSECTP-WHEN-SUBSETP))
(1073 58 (:REWRITE NO-DUPLICATESP-OF-MEMBER))
(899 58 (:DEFINITION NO-DUPLICATESP-EQUAL))
(435 380 (:REWRITE DEFAULT-CDR))
(402 344 (:REWRITE DEFAULT-CAR))
(400 400 (:TYPE-PRESCRIPTION SUBSETP-EQUAL))
(293 293 (:REWRITE SUBSETP-MEMBER . 2))
(293 293 (:REWRITE SUBSETP-MEMBER . 1))
(290 290 (:TYPE-PRESCRIPTION NO-DUPLICATESP-EQUAL))
(232 116 (:TYPE-PRESCRIPTION TRUE-LISTP-APPEND))
(227 58 (:REWRITE INTERSECT-WITH-SUBSET . 12))
(218 58 (:REWRITE INTERSECT-WITH-SUBSET . 8))
(160 160 (:REWRITE SUBSETP-TRANS2))
(160 160 (:REWRITE SUBSETP-TRANS))
(138 58 (:REWRITE INTERSECT-WITH-SUBSET . 2))
(116 116 (:TYPE-PRESCRIPTION TRUE-LISTP))
(116 116 (:TYPE-PRESCRIPTION BINARY-APPEND))
(90 58 (:REWRITE INTERSECT-WITH-SUBSET . 5))
(58 58 (:REWRITE SUBSETP-MEMBER . 4))
(58 58 (:REWRITE SUBSETP-MEMBER . 3))
(58 58 (:REWRITE INTERSECT-WITH-SUBSET . 11))
(58 58 (:REWRITE INTERSECT-WITH-SUBSET . 10))
(58 58 (:REWRITE INTERSECT-WITH-SUBSET . 9))
(58 58 (:REWRITE INTERSECT-WITH-SUBSET . 7))
(58 58 (:REWRITE INTERSECT-WITH-SUBSET . 6))
(58 58 (:REWRITE INTERSECT-WITH-SUBSET . 4))
(58 58 (:REWRITE INTERSECT-WITH-SUBSET . 3))
(58 58 (:REWRITE INTERSECT-WITH-SUBSET . 1))
(21 21 (:REWRITE CONSP-OF-APPEND))
)
(NOT-INTERSECTP-LIST-WHEN-ATOM
(5 5 (:REWRITE SUBSETP-TRANS2))
(5 5 (:REWRITE SUBSETP-TRANS))
(5 5 (:REWRITE DEFAULT-CAR))
(2 2 (:REWRITE DEFAULT-CDR))
)
(NOT-INTERSECTP-LIST-WHEN-SUBSETP-1
(1702 22 (:DEFINITION INTERSECTP-EQUAL))
(1321 56 (:DEFINITION SUBSETP-EQUAL))
(1190 47 (:REWRITE INTERSECTP-WHEN-SUBSETP))
(1029 96 (:DEFINITION MEMBER-EQUAL))
(984 29 (:REWRITE INTERSECT-WITH-SUBSET . 7))
(666 36 (:REWRITE NO-DUPLICATESP-OF-MEMBER))
(558 36 (:DEFINITION NO-DUPLICATESP-EQUAL))
(533 45 (:REWRITE INTERSECT-WITH-SUBSET . 1))
(477 477 (:TYPE-PRESCRIPTION MEMBER-EQUAL))
(291 115 (:REWRITE SUBSETP-TRANS))
(249 249 (:REWRITE DEFAULT-CDR))
(221 221 (:REWRITE DEFAULT-CAR))
(209 209 (:REWRITE SUBSETP-MEMBER . 2))
(209 209 (:REWRITE SUBSETP-MEMBER . 1))
(180 180 (:TYPE-PRESCRIPTION NO-DUPLICATESP-EQUAL))
(115 115 (:REWRITE SUBSETP-TRANS2))
(65 8 (:REWRITE INTERSECT-WITH-SUBSET . 16))
(46 46 (:REWRITE INTERSECT-WITH-SUBSET . 6))
(46 46 (:REWRITE INTERSECT-WITH-SUBSET . 5))
(46 46 (:REWRITE INTERSECT-WITH-SUBSET . 4))
(46 46 (:REWRITE INTERSECT-WITH-SUBSET . 3))
(46 30 (:REWRITE INTERSECT-WITH-SUBSET . 12))
(44 1 (:REWRITE INTERSECTP-IS-COMMUTATIVE))
(36 36 (:REWRITE SUBSETP-MEMBER . 4))
(36 36 (:REWRITE SUBSETP-MEMBER . 3))
(30 30 (:REWRITE INTERSECT-WITH-SUBSET . 11))
(30 30 (:REWRITE INTERSECT-WITH-SUBSET . 10))
(30 30 (:REWRITE INTERSECT-WITH-SUBSET . 9))
(14 14 (:REWRITE NOT-INTERSECTP-LIST-WHEN-ATOM))
(8 8 (:REWRITE INTERSECT-WITH-SUBSET . 15))
(8 8 (:REWRITE INTERSECT-WITH-SUBSET . 14))
(8 8 (:REWRITE INTERSECT-WITH-SUBSET . 13))
)
(NOT-INTERSECTP-LIST-WHEN-SUBSETP-2
(2175 117 (:REWRITE NO-DUPLICATESP-OF-MEMBER))
(1900 76 (:REWRITE INTERSECTP-WHEN-SUBSETP))
(1824 117 (:DEFINITION NO-DUPLICATESP-EQUAL))
(619 619 (:REWRITE DEFAULT-CDR))
(585 585 (:TYPE-PRESCRIPTION NO-DUPLICATESP-EQUAL))
(530 530 (:REWRITE DEFAULT-CAR))
(504 504 (:REWRITE SUBSETP-MEMBER . 1))
(292 76 (:REWRITE INTERSECT-WITH-SUBSET . 6))
(220 220 (:REWRITE SUBSETP-TRANS2))
(220 220 (:REWRITE SUBSETP-TRANS))
(180 76 (:REWRITE INTERSECT-WITH-SUBSET . 5))
(170 117 (:REWRITE SUBSETP-MEMBER . 3))
(156 76 (:REWRITE INTERSECT-WITH-SUBSET . 2))
(140 76 (:REWRITE INTERSECT-WITH-SUBSET . 12))
(117 117 (:REWRITE SUBSETP-MEMBER . 4))
(116 76 (:REWRITE INTERSECT-WITH-SUBSET . 8))
(76 76 (:REWRITE INTERSECT-WITH-SUBSET . 11))
(76 76 (:REWRITE INTERSECT-WITH-SUBSET . 10))
(76 76 (:REWRITE INTERSECT-WITH-SUBSET . 9))
(76 76 (:REWRITE INTERSECT-WITH-SUBSET . 7))
(76 76 (:REWRITE INTERSECT-WITH-SUBSET . 4))
(76 76 (:REWRITE INTERSECT-WITH-SUBSET . 3))
(76 76 (:REWRITE INTERSECT-WITH-SUBSET . 1))
(40 40 (:REWRITE NOT-INTERSECTP-LIST-WHEN-SUBSETP-1))
(40 40 (:REWRITE NOT-INTERSECTP-LIST-WHEN-ATOM))
(18 18 (:REWRITE INTERSECT-WITH-SUBSET . 16))
(18 18 (:REWRITE INTERSECT-WITH-SUBSET . 15))
(18 18 (:REWRITE INTERSECT-WITH-SUBSET . 14))
(18 18 (:REWRITE INTERSECT-WITH-SUBSET . 13))
)
(NOT-INTERSECTP-LIST-OF-TRUE-LIST-FIX
(636 35 (:DEFINITION SUBSETP-EQUAL))
(562 57 (:DEFINITION MEMBER-EQUAL))
(550 22 (:REWRITE INTERSECTP-WHEN-SUBSETP))
(407 22 (:REWRITE NO-DUPLICATESP-OF-MEMBER))
(341 22 (:DEFINITION NO-DUPLICATESP-EQUAL))
(301 21 (:DEFINITION TRUE-LISTP))
(298 41 (:REWRITE TRUE-LISTP-WHEN-STRING-LIST))
(270 10 (:REWRITE LIST-FIX-WHEN-TRUE-LISTP))
(212 212 (:REWRITE DEFAULT-CDR))
(195 33 (:DEFINITION STRING-LISTP))
(185 9 (:REWRITE TRUE-LIST-FIX-WHEN-TRUE-LISTP))
(175 175 (:TYPE-PRESCRIPTION SUBSETP-EQUAL))
(169 169 (:REWRITE DEFAULT-CAR))
(158 158 (:TYPE-PRESCRIPTION STRING-LISTP))
(117 117 (:REWRITE SUBSETP-MEMBER . 2))
(117 117 (:REWRITE SUBSETP-MEMBER . 1))
(110 110 (:TYPE-PRESCRIPTION NO-DUPLICATESP-EQUAL))
(102 22 (:REWRITE INTERSECT-WITH-SUBSET . 8))
(102 22 (:REWRITE INTERSECT-WITH-SUBSET . 2))
(95 95 (:TYPE-PRESCRIPTION TRUE-LISTP))
(78 22 (:REWRITE INTERSECT-WITH-SUBSET . 12))
(70 70 (:REWRITE SUBSETP-TRANS2))
(70 70 (:REWRITE SUBSETP-TRANS))
(54 22 (:REWRITE INTERSECT-WITH-SUBSET . 5))
(22 22 (:REWRITE SUBSETP-MEMBER . 4))
(22 22 (:REWRITE SUBSETP-MEMBER . 3))
(22 22 (:REWRITE INTERSECT-WITH-SUBSET . 11))
(22 22 (:REWRITE INTERSECT-WITH-SUBSET . 10))
(22 22 (:REWRITE INTERSECT-WITH-SUBSET . 9))
(22 22 (:REWRITE INTERSECT-WITH-SUBSET . 7))
(22 22 (:REWRITE INTERSECT-WITH-SUBSET . 6))
(22 22 (:REWRITE INTERSECT-WITH-SUBSET . 4))
(22 22 (:REWRITE INTERSECT-WITH-SUBSET . 3))
(22 22 (:REWRITE INTERSECT-WITH-SUBSET . 1))
(22 11 (:REWRITE DEFAULT-+-2))
(17 17 (:REWRITE NOT-INTERSECTP-LIST-WHEN-SUBSETP-2))
(17 17 (:REWRITE NOT-INTERSECTP-LIST-WHEN-SUBSETP-1))
(17 17 (:REWRITE NOT-INTERSECTP-LIST-WHEN-ATOM))
(11 11 (:REWRITE DEFAULT-+-1))
(9 9 (:REWRITE LIST-FIX-WHEN-NOT-CONSP))
(8 8 (:LINEAR POSITION-WHEN-MEMBER))
(8 8 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
)
(FLATTEN-SUBSET-NO-DUPLICATESP-LEMMA-1
(4338 237 (:DEFINITION NO-DUPLICATESP-EQUAL))
(3813 311 (:REWRITE NO-DUPLICATESP-OF-MEMBER))
(3370 173 (:DEFINITION SUBSETP-EQUAL))
(2650 106 (:REWRITE INTERSECTP-WHEN-SUBSETP))
(1154 1154 (:REWRITE DEFAULT-CDR))
(974 974 (:REWRITE DEFAULT-CAR))
(938 916 (:REWRITE SUBSETP-MEMBER . 1))
(916 916 (:REWRITE SUBSETP-MEMBER . 2))
(850 850 (:TYPE-PRESCRIPTION SUBSETP-EQUAL))
(602 106 (:REWRITE INTERSECT-WITH-SUBSET . 6))
(564 311 (:REWRITE SUBSETP-MEMBER . 3))
(426 106 (:REWRITE INTERSECT-WITH-SUBSET . 9))
(346 346 (:REWRITE SUBSETP-TRANS2))
(346 346 (:REWRITE SUBSETP-TRANS))
(311 311 (:REWRITE SUBSETP-MEMBER . 4))
(266 106 (:REWRITE INTERSECT-WITH-SUBSET . 3))
(234 106 (:REWRITE INTERSECT-WITH-SUBSET . 12))
(186 106 (:REWRITE INTERSECT-WITH-SUBSET . 8))
(138 106 (:REWRITE INTERSECT-WITH-SUBSET . 11))
(106 106 (:REWRITE INTERSECT-WITH-SUBSET . 10))
(106 106 (:REWRITE INTERSECT-WITH-SUBSET . 7))
(106 106 (:REWRITE INTERSECT-WITH-SUBSET . 5))
(106 106 (:REWRITE INTERSECT-WITH-SUBSET . 4))
(106 106 (:REWRITE INTERSECT-WITH-SUBSET . 2))
(106 106 (:REWRITE INTERSECT-WITH-SUBSET . 1))
(47 47 (:REWRITE FLATTEN-WHEN-NOT-CONSP))
(24 24 (:REWRITE NOT-INTERSECTP-LIST-WHEN-SUBSETP-2))
(24 24 (:REWRITE NOT-INTERSECTP-LIST-WHEN-SUBSETP-1))
(24 24 (:REWRITE NOT-INTERSECTP-LIST-WHEN-ATOM))
)
(FLATTEN-SUBSET-NO-DUPLICATESP-LEMMA-3
(927 57 (:REWRITE NO-DUPLICATESP-OF-MEMBER))
(876 52 (:DEFINITION NO-DUPLICATESP-EQUAL))
(684 6 (:DEFINITION INTERSECTP-EQUAL))
(471 231 (:REWRITE SUBSETP-MEMBER . 1))
(328 57 (:REWRITE SUBSETP-MEMBER . 3))
(321 237 (:REWRITE SUBSETP-MEMBER . 2))
(300 12 (:REWRITE INTERSECTP-WHEN-SUBSETP))
(249 249 (:REWRITE DEFAULT-CDR))
(221 221 (:REWRITE DEFAULT-CAR))
(120 7 (:REWRITE NOT-INTERSECTP-LIST-WHEN-SUBSETP-2))
(116 90 (:REWRITE SUBSETP-TRANS))
(90 90 (:REWRITE SUBSETP-TRANS2))
(57 57 (:REWRITE SUBSETP-MEMBER . 4))
(12 12 (:REWRITE INTERSECT-WITH-SUBSET . 12))
(12 12 (:REWRITE INTERSECT-WITH-SUBSET . 11))
(12 12 (:REWRITE INTERSECT-WITH-SUBSET . 10))
(12 12 (:REWRITE INTERSECT-WITH-SUBSET . 9))
(12 12 (:REWRITE INTERSECT-WITH-SUBSET . 8))
(12 12 (:REWRITE INTERSECT-WITH-SUBSET . 7))
(12 12 (:REWRITE INTERSECT-WITH-SUBSET . 6))
(12 12 (:REWRITE INTERSECT-WITH-SUBSET . 5))
(12 12 (:REWRITE INTERSECT-WITH-SUBSET . 4))
(12 12 (:REWRITE INTERSECT-WITH-SUBSET . 3))
(12 12 (:REWRITE INTERSECT-WITH-SUBSET . 2))
(12 12 (:REWRITE INTERSECT-WITH-SUBSET . 1))
(10 10 (:TYPE-PRESCRIPTION TRUE-LISTP-OF-FLATTEN))
(8 8 (:REWRITE INTERSECT-WITH-SUBSET . 16))
(8 8 (:REWRITE INTERSECT-WITH-SUBSET . 15))
(8 8 (:REWRITE INTERSECT-WITH-SUBSET . 14))
(8 8 (:REWRITE INTERSECT-WITH-SUBSET . 13))
(7 7 (:REWRITE NOT-INTERSECTP-LIST-WHEN-SUBSETP-1))
(7 7 (:REWRITE NOT-INTERSECTP-LIST-WHEN-ATOM))
(5 5 (:REWRITE FLATTEN-WHEN-NOT-CONSP))
)
(FLATTEN-SUBSET-NO-DUPLICATESP
(501 197 (:REWRITE SUBSETP-MEMBER . 1))
(363 96 (:REWRITE SUBSETP-MEMBER . 3))
(259 259 (:REWRITE DEFAULT-CDR))
(209 197 (:REWRITE SUBSETP-MEMBER . 2))
(197 197 (:REWRITE DEFAULT-CAR))
(158 77 (:REWRITE SUBSETP-TRANS))
(96 96 (:REWRITE SUBSETP-MEMBER . 4))
(77 77 (:REWRITE SUBSETP-TRANS2))
(29 1 (:REWRITE FLATTEN-SUBSET-NO-DUPLICATESP-LEMMA-1))
(19 19 (:REWRITE FLATTEN-WHEN-NOT-CONSP))
(14 14 (:REWRITE INTERSECT-WITH-SUBSET . 16))
(14 14 (:REWRITE INTERSECT-WITH-SUBSET . 15))
(14 14 (:REWRITE INTERSECT-WITH-SUBSET . 14))
(14 14 (:REWRITE INTERSECT-WITH-SUBSET . 13))
(8 2 (:REWRITE APPEND-ATOM-UNDER-LIST-EQUIV))
(7 1 (:DEFINITION BINARY-APPEND))
)
|
