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
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
|
(VL2014::VL-PARSE-LVALUE-FN
(237 7 (:REWRITE PREFIXP-WHEN-EQUAL-LENGTHS))
(191 26 (:REWRITE LEN-WHEN-ATOM))
(160 7 (:REWRITE PREFIXP-WHEN-PREFIXP))
(93 6 (:REWRITE LEN-WHEN-PREFIXP))
(66 33 (:TYPE-PRESCRIPTION VL2014::VL-IS-TOKEN?-FN-WHEN-ATOM-OF-TOKENS))
(62 62 (:REWRITE CONSP-WHEN-MEMBER-EQUAL-OF-CONS-LISTP))
(62 31 (:REWRITE CONSP-UNDER-IFF-WHEN-TRUE-LISTP))
(54 54 (:REWRITE CONSP-WHEN-MEMBER-EQUAL-OF-ATOM-LISTP))
(40 4 (:REWRITE VL2014::VL-MATCH-UNDER-IFF))
(38 5 (:REWRITE PREFIXP-WHEN-NOT-CONSP-RIGHT))
(38 5 (:REWRITE PREFIXP-WHEN-NOT-CONSP-LEFT))
(31 31 (:TYPE-PRESCRIPTION TRUE-LISTP))
(31 31 (:REWRITE VL2014::CONSP-WHEN-MEMBER-EQUAL-OF-VL-USERTYPES-P . 2))
(31 31 (:REWRITE VL2014::CONSP-WHEN-MEMBER-EQUAL-OF-VL-USERTYPES-P . 1))
(31 31 (:REWRITE VL2014::CONSP-WHEN-MEMBER-EQUAL-OF-VL-ATTS-P . 2))
(31 31 (:REWRITE VL2014::CONSP-WHEN-MEMBER-EQUAL-OF-VL-ATTS-P . 1))
(31 31 (:REWRITE CONSP-BY-LEN))
(24 2 (:REWRITE SUBLISTP-WHEN-ATOM-RIGHT))
(24 2 (:REWRITE SUBLISTP-WHEN-ATOM-LEFT))
(16 16 (:REWRITE VL2014::PREFIXP-WHEN-MEMBER-EQUAL-OF-PREFIX-OF-EACHP))
(13 2 (:REWRITE LIST-EQUIV-WHEN-ATOM-RIGHT))
(13 2 (:REWRITE LIST-EQUIV-WHEN-ATOM-LEFT))
(12 6 (:REWRITE DEFAULT-<-1))
(10 10 (:LINEAR LOWER-BOUND-OF-LEN-WHEN-SUBLISTP))
(10 10 (:LINEAR LISTPOS-UPPER-BOUND-STRONG-2))
(10 10 (:LINEAR LEN-WHEN-PREFIXP))
(9 6 (:REWRITE DEFAULT-<-2))
(8 8 (:REWRITE VL2014::TRANSITIVITY-OF-PREFIXP))
(8 8 (:META CANCEL_PLUS-LESSP-CORRECT))
(8 8 (:LINEAR LEQ-POSITION-EQUAL-LEN))
(8 8 (:LINEAR INDEX-OF-<-LEN))
(7 7 (:REWRITE PREFIXP-TRANSITIVE . 2))
(7 7 (:REWRITE PREFIXP-TRANSITIVE . 1))
(7 7 (:REWRITE PREFIXP-ONE-WAY-OR-ANOTHER . 2))
(7 7 (:REWRITE PREFIXP-ONE-WAY-OR-ANOTHER . 1))
(6 3 (:REWRITE VL2014::O<-WHEN-NATPS))
(5 5 (:LINEAR STR::COUNT-LEADING-CHARSET-LEN))
(3 3 (:TYPE-PRESCRIPTION TWO-NATS-MEASURE))
(3 3 (:REWRITE SUBLISTP-COMPLETE))
(2 2 (:TYPE-PRESCRIPTION LIST-EQUIV))
(1 1 (:REWRITE SET::DOUBLE-CONTAINMENT))
(1 1 (:META CANCEL_TIMES-EQUAL-CORRECT))
(1 1 (:META CANCEL_PLUS-EQUAL-CORRECT))
)
(VL2014::PARSE-LVALUES-FLAG
(237 7 (:REWRITE PREFIXP-WHEN-EQUAL-LENGTHS))
(215 28 (:REWRITE LEN-WHEN-ATOM))
(160 7 (:REWRITE PREFIXP-WHEN-PREFIXP))
(93 6 (:REWRITE LEN-WHEN-PREFIXP))
(66 66 (:REWRITE CONSP-WHEN-MEMBER-EQUAL-OF-CONS-LISTP))
(66 33 (:REWRITE CONSP-UNDER-IFF-WHEN-TRUE-LISTP))
(58 58 (:REWRITE CONSP-WHEN-MEMBER-EQUAL-OF-ATOM-LISTP))
(44 24 (:TYPE-PRESCRIPTION VL2014::VL-IS-TOKEN?-FN-WHEN-ATOM-OF-TOKENS))
(40 4 (:REWRITE VL2014::VL-MATCH-UNDER-IFF))
(38 5 (:REWRITE PREFIXP-WHEN-NOT-CONSP-RIGHT))
(38 5 (:REWRITE PREFIXP-WHEN-NOT-CONSP-LEFT))
(33 33 (:TYPE-PRESCRIPTION TRUE-LISTP))
(33 33 (:REWRITE VL2014::CONSP-WHEN-MEMBER-EQUAL-OF-VL-USERTYPES-P . 2))
(33 33 (:REWRITE VL2014::CONSP-WHEN-MEMBER-EQUAL-OF-VL-USERTYPES-P . 1))
(33 33 (:REWRITE VL2014::CONSP-WHEN-MEMBER-EQUAL-OF-VL-ATTS-P . 2))
(33 33 (:REWRITE VL2014::CONSP-WHEN-MEMBER-EQUAL-OF-VL-ATTS-P . 1))
(33 33 (:REWRITE CONSP-BY-LEN))
(25 4 (:REWRITE SET::DOUBLE-CONTAINMENT))
(24 2 (:REWRITE SUBLISTP-WHEN-ATOM-RIGHT))
(24 2 (:REWRITE SUBLISTP-WHEN-ATOM-LEFT))
(16 16 (:REWRITE VL2014::PREFIXP-WHEN-MEMBER-EQUAL-OF-PREFIX-OF-EACHP))
(13 2 (:REWRITE LIST-EQUIV-WHEN-ATOM-RIGHT))
(13 2 (:REWRITE LIST-EQUIV-WHEN-ATOM-LEFT))
(12 6 (:REWRITE DEFAULT-<-1))
(10 10 (:LINEAR LOWER-BOUND-OF-LEN-WHEN-SUBLISTP))
(10 10 (:LINEAR LISTPOS-UPPER-BOUND-STRONG-2))
(10 10 (:LINEAR LEN-WHEN-PREFIXP))
(9 6 (:REWRITE DEFAULT-<-2))
(8 8 (:REWRITE VL2014::TRANSITIVITY-OF-PREFIXP))
(8 8 (:META CANCEL_PLUS-LESSP-CORRECT))
(8 8 (:LINEAR LEQ-POSITION-EQUAL-LEN))
(8 8 (:LINEAR INDEX-OF-<-LEN))
(7 7 (:REWRITE PREFIXP-TRANSITIVE . 2))
(7 7 (:REWRITE PREFIXP-TRANSITIVE . 1))
(7 7 (:REWRITE PREFIXP-ONE-WAY-OR-ANOTHER . 2))
(7 7 (:REWRITE PREFIXP-ONE-WAY-OR-ANOTHER . 1))
(6 6 (:TYPE-PRESCRIPTION SET::SETP-TYPE))
(6 3 (:REWRITE OMAP::SETP-WHEN-MAPP))
(6 3 (:REWRITE VL2014::O<-WHEN-NATPS))
(6 3 (:REWRITE SET::NONEMPTY-MEANS-SET))
(5 5 (:TYPE-PRESCRIPTION TWO-NATS-MEASURE))
(5 5 (:LINEAR STR::COUNT-LEADING-CHARSET-LEN))
(4 4 (:META CANCEL_TIMES-EQUAL-CORRECT))
(4 4 (:META CANCEL_PLUS-EQUAL-CORRECT))
(3 3 (:TYPE-PRESCRIPTION OMAP::MAPP))
(3 3 (:TYPE-PRESCRIPTION SET::EMPTY-TYPE))
(3 3 (:REWRITE SUBLISTP-COMPLETE))
(3 3 (:REWRITE SET::IN-SET))
(3 1 (:REWRITE VL2014::O-P-WHEN-NATP))
(2 2 (:TYPE-PRESCRIPTION LIST-EQUIV))
)
(FLAG::FLAG-EQUIV-LEMMA)
(VL2014::PARSE-LVALUES-FLAG-EQUIVALENCES)
(VL2014::FLAG-LEMMA-FOR-COUNT-STRONG
(20275 342 (:REWRITE LOWER-BOUND-OF-LEN-WHEN-SUBLISTP))
(16355 140 (:REWRITE SUBLISTP-WHEN-PREFIXP))
(8112 519 (:REWRITE PREFIXP-WHEN-EQUAL-LENGTHS))
(8105 519 (:REWRITE PREFIXP-WHEN-PREFIXP))
(4330 766 (:REWRITE LEN-WHEN-ATOM))
(3746 342 (:REWRITE LEN-WHEN-PREFIXP))
(2974 444 (:REWRITE PREFIXP-WHEN-NOT-CONSP-RIGHT))
(2974 444 (:REWRITE PREFIXP-WHEN-NOT-CONSP-LEFT))
(2464 2464 (:REWRITE CONSP-WHEN-MEMBER-EQUAL-OF-CONS-LISTP))
(2464 1232 (:REWRITE CONSP-UNDER-IFF-WHEN-TRUE-LISTP))
(2454 2454 (:REWRITE CONSP-WHEN-MEMBER-EQUAL-OF-ATOM-LISTP))
(1680 140 (:REWRITE SUBLISTP-WHEN-ATOM-RIGHT))
(1680 140 (:REWRITE SUBLISTP-WHEN-ATOM-LEFT))
(1526 763 (:TYPE-PRESCRIPTION VL2014::VL-IS-TOKEN?-FN-WHEN-ATOM-OF-TOKENS))
(1295 1295 (:TYPE-PRESCRIPTION PREFIXP))
(1232 1232 (:TYPE-PRESCRIPTION TRUE-LISTP))
(1232 1232 (:REWRITE VL2014::CONSP-WHEN-MEMBER-EQUAL-OF-VL-USERTYPES-P . 2))
(1232 1232 (:REWRITE VL2014::CONSP-WHEN-MEMBER-EQUAL-OF-VL-USERTYPES-P . 1))
(1232 1232 (:REWRITE VL2014::CONSP-WHEN-MEMBER-EQUAL-OF-VL-ATTS-P . 2))
(1232 1232 (:REWRITE VL2014::CONSP-WHEN-MEMBER-EQUAL-OF-VL-ATTS-P . 1))
(1232 1232 (:REWRITE CONSP-BY-LEN))
(1128 94 (:REWRITE DEFAULT-CAR))
(1038 1038 (:REWRITE VL2014::PREFIXP-WHEN-MEMBER-EQUAL-OF-PREFIX-OF-EACHP))
(608 342 (:REWRITE DEFAULT-<-1))
(542 342 (:REWRITE DEFAULT-<-2))
(519 519 (:REWRITE VL2014::TRANSITIVITY-OF-PREFIXP))
(519 519 (:REWRITE PREFIXP-TRANSITIVE . 2))
(519 519 (:REWRITE PREFIXP-TRANSITIVE . 1))
(519 519 (:REWRITE PREFIXP-ONE-WAY-OR-ANOTHER . 2))
(519 519 (:REWRITE PREFIXP-ONE-WAY-OR-ANOTHER . 1))
(482 482 (:TYPE-PRESCRIPTION SUBLISTP))
(449 75 (:REWRITE LIST-EQUIV-WHEN-ATOM-RIGHT))
(449 75 (:REWRITE LIST-EQUIV-WHEN-ATOM-LEFT))
(432 432 (:LINEAR LOWER-BOUND-OF-LEN-WHEN-SUBLISTP))
(432 432 (:LINEAR LISTPOS-UPPER-BOUND-STRONG-2))
(432 432 (:LINEAR LEN-WHEN-PREFIXP))
(344 344 (:META CANCEL_PLUS-LESSP-CORRECT))
(226 226 (:LINEAR LEQ-POSITION-EQUAL-LEN))
(226 226 (:LINEAR INDEX-OF-<-LEN))
(216 216 (:LINEAR STR::COUNT-LEADING-CHARSET-LEN))
(176 176 (:REWRITE-QUOTED-CONSTANT SYMBOL-FIX-UNDER-SYMBOL-EQUIV))
(158 158 (:REWRITE-QUOTED-CONSTANT VL2014::VL-OP-FIX-UNDER-VL-OP-EQUIV))
(158 158 (:REWRITE-QUOTED-CONSTANT VL2014::VL-MAYBE-EXPRTYPE-FIX-UNDER-VL-MAYBE-EXPRTYPE-EQUIV))
(158 158 (:REWRITE-QUOTED-CONSTANT VL2014::VL-ATTS-FIX-UNDER-VL-ATTS-EQUIV))
(158 158 (:REWRITE-QUOTED-CONSTANT MAYBE-NATP-FIX-UNDER-MAYBE-NAT-EQUIV))
(140 140 (:REWRITE SUBLISTP-COMPLETE))
(94 94 (:REWRITE CAR-WHEN-ALL-EQUALP))
(75 75 (:TYPE-PRESCRIPTION LIST-EQUIV))
(50 5 (:REWRITE VL2014::VL-MATCH-UNDER-IFF))
(40 5 (:REWRITE SET::DOUBLE-CONTAINMENT))
(12 1 (:REWRITE VL2014::VL-PARSE-EXPRESSION-EOF-VL-PARSE-INDEXED-ID))
(10 10 (:TYPE-PRESCRIPTION SET::SETP-TYPE))
(10 5 (:REWRITE OMAP::SETP-WHEN-MAPP))
(10 5 (:REWRITE SET::NONEMPTY-MEANS-SET))
(5 5 (:TYPE-PRESCRIPTION OMAP::MAPP))
(5 5 (:TYPE-PRESCRIPTION SET::EMPTY-TYPE))
(5 5 (:REWRITE SET::IN-SET))
(5 5 (:META CANCEL_TIMES-EQUAL-CORRECT))
(5 5 (:META CANCEL_PLUS-EQUAL-CORRECT))
)
(VL2014::COUNT-STRONG-VL-PARSE-LVALUE)
(VL2014::COUNT-STRONG-VL-PARSE-1+-LVALUES-SEPARATED-BY-COMMAS)
(VL2014::FLAG-LEMMA-FOR-FAILS-GRACEFULLY
(3768 314 (:REWRITE LEN-WHEN-ATOM))
(2040 1020 (:TYPE-PRESCRIPTION VL2014::VL-IS-TOKEN?-FN-WHEN-ATOM-OF-TOKENS))
(1704 142 (:REWRITE DEFAULT-CAR))
(918 918 (:REWRITE CONSP-WHEN-MEMBER-EQUAL-OF-CONS-LISTP))
(918 918 (:REWRITE CONSP-WHEN-MEMBER-EQUAL-OF-ATOM-LISTP))
(918 459 (:REWRITE CONSP-UNDER-IFF-WHEN-TRUE-LISTP))
(459 459 (:TYPE-PRESCRIPTION TRUE-LISTP))
(459 459 (:REWRITE VL2014::CONSP-WHEN-MEMBER-EQUAL-OF-VL-USERTYPES-P . 2))
(459 459 (:REWRITE VL2014::CONSP-WHEN-MEMBER-EQUAL-OF-VL-USERTYPES-P . 1))
(459 459 (:REWRITE VL2014::CONSP-WHEN-MEMBER-EQUAL-OF-VL-ATTS-P . 2))
(459 459 (:REWRITE VL2014::CONSP-WHEN-MEMBER-EQUAL-OF-VL-ATTS-P . 1))
(459 459 (:REWRITE CONSP-BY-LEN))
(232 232 (:REWRITE-QUOTED-CONSTANT VL2014::VL-OP-FIX-UNDER-VL-OP-EQUIV))
(232 232 (:REWRITE-QUOTED-CONSTANT VL2014::VL-MAYBE-EXPRTYPE-FIX-UNDER-VL-MAYBE-EXPRTYPE-EQUIV))
(232 232 (:REWRITE-QUOTED-CONSTANT VL2014::VL-ATTS-FIX-UNDER-VL-ATTS-EQUIV))
(232 232 (:REWRITE-QUOTED-CONSTANT MAYBE-NATP-FIX-UNDER-MAYBE-NAT-EQUIV))
(142 142 (:REWRITE CAR-WHEN-ALL-EQUALP))
(48 6 (:REWRITE SET::DOUBLE-CONTAINMENT))
(37 4 (:REWRITE VL2014::VL-PARSE-EXPRESSION-EOF-VL-PARSE-INDEXED-ID))
(24 24 (:REWRITE VL2014::VL-WARNING-P-WHEN-MEMBER-EQUAL-OF-VL-WARNINGLIST-P))
(12 12 (:TYPE-PRESCRIPTION SET::SETP-TYPE))
(12 6 (:REWRITE OMAP::SETP-WHEN-MAPP))
(12 6 (:REWRITE SET::NONEMPTY-MEANS-SET))
(8 8 (:LINEAR LOWER-BOUND-OF-LEN-WHEN-SUBLISTP))
(8 8 (:LINEAR LISTPOS-UPPER-BOUND-STRONG-2))
(8 8 (:LINEAR LEN-WHEN-PREFIXP))
(6 6 (:TYPE-PRESCRIPTION OMAP::MAPP))
(6 6 (:TYPE-PRESCRIPTION SET::EMPTY-TYPE))
(6 6 (:REWRITE SET::IN-SET))
(6 6 (:META CANCEL_TIMES-EQUAL-CORRECT))
(6 6 (:META CANCEL_PLUS-EQUAL-CORRECT))
(4 4 (:LINEAR LEQ-POSITION-EQUAL-LEN))
(4 4 (:LINEAR INDEX-OF-<-LEN))
(4 4 (:LINEAR STR::COUNT-LEADING-CHARSET-LEN))
)
(VL2014::FAILS-GRACEFULLY-VL-PARSE-LVALUE)
(VL2014::FAILS-GRACEFULLY-VL-PARSE-1+-LVALUES-SEPARATED-BY-COMMAS)
(VL2014::FLAG-LEMMA-FOR-RESULT
(1551 132 (:REWRITE LEN-WHEN-ATOM))
(1034 517 (:TYPE-PRESCRIPTION VL2014::VL-IS-TOKEN?-FN-WHEN-ATOM-OF-TOKENS))
(663 58 (:REWRITE DEFAULT-CAR))
(394 394 (:REWRITE CONSP-WHEN-MEMBER-EQUAL-OF-CONS-LISTP))
(394 394 (:REWRITE CONSP-WHEN-MEMBER-EQUAL-OF-ATOM-LISTP))
(394 197 (:REWRITE CONSP-UNDER-IFF-WHEN-TRUE-LISTP))
(230 230 (:TYPE-PRESCRIPTION TRUE-LISTP))
(197 197 (:REWRITE VL2014::CONSP-WHEN-MEMBER-EQUAL-OF-VL-USERTYPES-P . 2))
(197 197 (:REWRITE VL2014::CONSP-WHEN-MEMBER-EQUAL-OF-VL-USERTYPES-P . 1))
(197 197 (:REWRITE VL2014::CONSP-WHEN-MEMBER-EQUAL-OF-VL-ATTS-P . 2))
(197 197 (:REWRITE VL2014::CONSP-WHEN-MEMBER-EQUAL-OF-VL-ATTS-P . 1))
(197 197 (:REWRITE CONSP-BY-LEN))
(99 11 (:REWRITE VL2014::VL-EXPRLIST-P-WHEN-NOT-CONSP))
(95 30 (:REWRITE VL2014::VL-EXPR-P-WHEN-MEMBER-EQUAL-OF-VL-EXPRLIST-P))
(93 3 (:REWRITE SUBSETP-OF-CONS))
(86 86 (:REWRITE-QUOTED-CONSTANT VL2014::VL-OP-FIX-UNDER-VL-OP-EQUIV))
(86 86 (:REWRITE-QUOTED-CONSTANT VL2014::VL-MAYBE-EXPRTYPE-FIX-UNDER-VL-MAYBE-EXPRTYPE-EQUIV))
(86 86 (:REWRITE-QUOTED-CONSTANT VL2014::VL-ATTS-FIX-UNDER-VL-ATTS-EQUIV))
(86 86 (:REWRITE-QUOTED-CONSTANT MAYBE-NATP-FIX-UNDER-MAYBE-NAT-EQUIV))
(66 33 (:TYPE-PRESCRIPTION TRUE-LISTP-MEMBER-EQUAL))
(65 11 (:REWRITE VL2014::MEMBER-EQUAL-WHEN-MEMBER-EQUAL-OF-CDR-UNDER-IFF))
(59 7 (:REWRITE SET::DOUBLE-CONTAINMENT))
(58 58 (:REWRITE CAR-WHEN-ALL-EQUALP))
(38 5 (:REWRITE VL2014::VL-PARSE-EXPRESSION-EOF-VL-PARSE-INDEXED-ID))
(33 33 (:TYPE-PRESCRIPTION CONSP-MEMBER-EQUAL))
(24 24 (:REWRITE VL2014::VL-EXPRLIST-P-WHEN-MEMBER-EQUAL-OF-VL-EXPRLISTLIST-P))
(14 14 (:TYPE-PRESCRIPTION SET::SETP-TYPE))
(14 7 (:REWRITE OMAP::SETP-WHEN-MAPP))
(14 7 (:REWRITE SET::NONEMPTY-MEANS-SET))
(12 1 (:REWRITE SUBSETP-WHEN-ATOM-RIGHT))
(12 1 (:REWRITE SUBSETP-WHEN-ATOM-LEFT))
(11 11 (:REWRITE SUBSETP-MEMBER . 2))
(11 11 (:REWRITE SUBSETP-MEMBER . 1))
(11 11 (:REWRITE MEMBER-EQUAL-WHEN-ALL-EQUALP))
(8 8 (:REWRITE SUBSETP-TRANS2))
(8 8 (:REWRITE SUBSETP-TRANS))
(8 8 (:LINEAR LOWER-BOUND-OF-LEN-WHEN-SUBLISTP))
(8 8 (:LINEAR LISTPOS-UPPER-BOUND-STRONG-2))
(8 8 (:LINEAR LEN-WHEN-PREFIXP))
(7 7 (:TYPE-PRESCRIPTION OMAP::MAPP))
(7 7 (:TYPE-PRESCRIPTION SET::EMPTY-TYPE))
(7 7 (:REWRITE SET::IN-SET))
(7 7 (:META CANCEL_TIMES-EQUAL-CORRECT))
(7 7 (:META CANCEL_PLUS-EQUAL-CORRECT))
(4 4 (:LINEAR LEQ-POSITION-EQUAL-LEN))
(4 4 (:LINEAR INDEX-OF-<-LEN))
(4 4 (:LINEAR STR::COUNT-LEADING-CHARSET-LEN))
(3 3 (:REWRITE DEFAULT-CDR))
(2 2 (:REWRITE SUBSETP-NIL))
)
(VL2014::RESULT-VL-PARSE-LVALUE)
(VL2014::RESULT-VL-PARSE-1+-LVALUES-SEPARATED-BY-COMMAS)
(VL2014::FLAG-LEMMA-FOR-PARSE-LVALUES-TRUE-LISTP
(850 50 (:DEFINITION VL2014::VL-PARSE-LVALUE-FN))
(735 64 (:REWRITE LEN-WHEN-ATOM))
(400 100 (:REWRITE VL2014::VL-MATCH-TOKEN-FAILS-GRACEFULLY))
(378 189 (:TYPE-PRESCRIPTION VL2014::VL-IS-TOKEN?-FN-WHEN-ATOM-OF-TOKENS))
(255 24 (:REWRITE DEFAULT-CAR))
(189 189 (:TYPE-PRESCRIPTION ATOM))
(170 170 (:REWRITE CONSP-WHEN-MEMBER-EQUAL-OF-CONS-LISTP))
(170 170 (:REWRITE CONSP-WHEN-MEMBER-EQUAL-OF-ATOM-LISTP))
(170 85 (:REWRITE CONSP-UNDER-IFF-WHEN-TRUE-LISTP))
(85 85 (:REWRITE VL2014::CONSP-WHEN-MEMBER-EQUAL-OF-VL-USERTYPES-P . 2))
(85 85 (:REWRITE VL2014::CONSP-WHEN-MEMBER-EQUAL-OF-VL-USERTYPES-P . 1))
(85 85 (:REWRITE VL2014::CONSP-WHEN-MEMBER-EQUAL-OF-VL-ATTS-P . 2))
(85 85 (:REWRITE VL2014::CONSP-WHEN-MEMBER-EQUAL-OF-VL-ATTS-P . 1))
(85 85 (:REWRITE CONSP-BY-LEN))
(51 3 (:REWRITE TRUE-LISTP-WHEN-SYMBOL-LISTP-REWRITE))
(50 50 (:REWRITE-QUOTED-CONSTANT VL2014::VL-OP-FIX-UNDER-VL-OP-EQUIV))
(50 50 (:REWRITE-QUOTED-CONSTANT VL2014::VL-MAYBE-EXPRTYPE-FIX-UNDER-VL-MAYBE-EXPRTYPE-EQUIV))
(50 50 (:REWRITE-QUOTED-CONSTANT VL2014::VL-ATTS-FIX-UNDER-VL-ATTS-EQUIV))
(50 50 (:REWRITE-QUOTED-CONSTANT MAYBE-NATP-FIX-UNDER-MAYBE-NAT-EQUIV))
(42 3 (:REWRITE TRUE-LISTP-WHEN-STRING-LISTP-REWRITE))
(36 3 (:REWRITE TRUE-LISTP-WHEN-CHARACTER-LISTP-REWRITE))
(36 3 (:REWRITE TRUE-LISTP-WHEN-ATOM))
(24 24 (:REWRITE CAR-WHEN-ALL-EQUALP))
(24 3 (:REWRITE SET::SETS-ARE-TRUE-LISTS-CHEAP))
(24 3 (:REWRITE SET::DOUBLE-CONTAINMENT))
(12 12 (:TYPE-PRESCRIPTION SET::SETP-TYPE))
(12 6 (:REWRITE SYMBOL-LISTP-WHEN-SUBSETP-EQUAL))
(12 6 (:REWRITE OMAP::SETP-WHEN-MAPP))
(12 6 (:REWRITE SET::NONEMPTY-MEANS-SET))
(12 3 (:REWRITE VL2014::STRING-LISTP-WHEN-NO-NILS-IN-VL-MAYBE-STRING-LISTP))
(9 3 (:REWRITE VL2014::SYMBOL-LISTP-WHEN-SUBSETP-EQUAL-OF-SYMBOL-LISTP . 1))
(8 8 (:LINEAR LOWER-BOUND-OF-LEN-WHEN-SUBLISTP))
(8 8 (:LINEAR LISTPOS-UPPER-BOUND-STRONG-2))
(8 8 (:LINEAR LEN-WHEN-PREFIXP))
(6 6 (:TYPE-PRESCRIPTION SYMBOL-LISTP))
(6 6 (:TYPE-PRESCRIPTION SUBSETP-EQUAL))
(6 6 (:TYPE-PRESCRIPTION STRING-LISTP))
(6 6 (:TYPE-PRESCRIPTION OMAP::MAPP))
(6 6 (:TYPE-PRESCRIPTION SET::EMPTY-TYPE))
(6 6 (:TYPE-PRESCRIPTION CHARACTER-LISTP))
(6 6 (:REWRITE VL2014::TRUE-LISTP-WHEN-MEMBER-EQUAL-OF-TRUE-LIST-LISTP))
(6 6 (:REWRITE VL2014::SYMBOL-LISTP-WHEN-MEMBER-EQUAL-OF-SYMBOL-LIST-LISTP))
(6 6 (:REWRITE VL2014::SYMBOL-LISTP-OF-ALIST-VALS-OF-VL-FULL-KEYWORD-TABLE))
(6 6 (:REWRITE STRING-LISTP-WHEN-SUBSETP-EQUAL))
(6 6 (:REWRITE VL2014::STRING-LISTP-WHEN-MEMBER-EQUAL-OF-STRING-LIST-LISTP))
(6 6 (:REWRITE SET::IN-SET))
(6 6 (:REWRITE CHARACTER-LISTP-WHEN-SUBSETP-EQUAL))
(6 3 (:TYPE-PRESCRIPTION TRUE-LISTP-MEMBER-EQUAL))
(6 3 (:REWRITE SYMBOL-LISTP-WHEN-BOOLEAN-LISTP))
(6 3 (:REWRITE STR::CHARACTER-LISTP-WHEN-OCT-DIGIT-CHAR-LISTP))
(6 3 (:REWRITE STR::CHARACTER-LISTP-WHEN-HEX-DIGIT-CHAR-LISTP))
(6 3 (:REWRITE STR::CHARACTER-LISTP-WHEN-DEC-DIGIT-CHAR-LISTP))
(4 4 (:LINEAR LEQ-POSITION-EQUAL-LEN))
(4 4 (:LINEAR INDEX-OF-<-LEN))
(4 4 (:LINEAR STR::COUNT-LEADING-CHARSET-LEN))
(3 3 (:TYPE-PRESCRIPTION STR::OCT-DIGIT-CHAR-LISTP))
(3 3 (:TYPE-PRESCRIPTION STR::HEX-DIGIT-CHAR-LISTP))
(3 3 (:TYPE-PRESCRIPTION STR::DEC-DIGIT-CHAR-LISTP))
(3 3 (:TYPE-PRESCRIPTION CONSP-MEMBER-EQUAL))
(3 3 (:TYPE-PRESCRIPTION BOOLEAN-LISTP))
(3 3 (:REWRITE TRUE-LISTP-WHEN-UNSIGNED-BYTE-LISTP))
(3 3 (:REWRITE TRUE-LISTP-WHEN-SIGNED-BYTE-LISTP))
(3 3 (:REWRITE VL2014::SYMBOL-LISTP-WHEN-SUBSETP-EQUAL-OF-SYMBOL-LISTP . 2))
(3 3 (:REWRITE SYMBOL-LISTP-WHEN-NOT-CONSP))
(3 3 (:REWRITE VL2014::STRING-LISTP-WHEN-SUBSETP-EQUAL-OF-STRING-LISTP . 2))
(3 3 (:REWRITE VL2014::STRING-LISTP-WHEN-SUBSETP-EQUAL-OF-STRING-LISTP . 1))
(3 3 (:REWRITE STRING-LISTP-WHEN-NOT-CONSP))
(3 3 (:REWRITE FN-CHECK-DEF-FORMALS))
(3 3 (:REWRITE CHARACTER-LISTP-WHEN-NOT-CONSP))
(3 3 (:META CANCEL_TIMES-EQUAL-CORRECT))
(3 3 (:META CANCEL_PLUS-EQUAL-CORRECT))
)
(VL2014::PARSE-LVALUES-TRUE-LISTP-VL-PARSE-LVALUE)
(VL2014::PARSE-LVALUES-TRUE-LISTP-VL-PARSE-1+-LVALUES-SEPARATED-BY-COMMAS)
(VL2014::VL-PARSE-LVALUE-FN
(271 7 (:DEFINITION VL2014::VL-PARSE-1+-LVALUES-SEPARATED-BY-COMMAS-FN))
(265 35 (:REWRITE LEN-WHEN-ATOM))
(181 3 (:REWRITE VL2014::VL-TOKENLIST-P-WHEN-NOT-CONSP))
(133 3 (:REWRITE CONSP-OF-CAR-WHEN-ALISTP))
(122 122 (:REWRITE CONSP-WHEN-MEMBER-EQUAL-OF-CONS-LISTP))
(122 122 (:REWRITE CONSP-WHEN-MEMBER-EQUAL-OF-ATOM-LISTP))
(112 6 (:REWRITE VL2014::NTH-WHEN-TOO-BIG))
(102 6 (:DEFINITION VL2014::VL-PARSE-LVALUE-FN))
(96 13 (:REWRITE DEFAULT-CAR))
(60 16 (:REWRITE VL2014::FAILS-GRACEFULLY-VL-PARSE-1+-LVALUES-SEPARATED-BY-COMMAS))
(51 3 (:REWRITE TRUE-LISTP-WHEN-SYMBOL-LISTP-REWRITE))
(48 12 (:REWRITE VL2014::VL-MATCH-TOKEN-FAILS-GRACEFULLY))
(42 3 (:REWRITE TRUE-LISTP-WHEN-STRING-LISTP-REWRITE))
(39 3 (:REWRITE OMAP::ALISTP-WHEN-MAPP))
(36 3 (:REWRITE TRUE-LISTP-WHEN-CHARACTER-LISTP-REWRITE))
(32 3 (:REWRITE TRUE-LISTP-WHEN-ATOM))
(28 28 (:REWRITE CONSP-BY-LEN))
(28 3 (:REWRITE VL2014::VL-TOKENLIST-P-OF-CAR-WHEN-VL-TOKENLISTLIST-P))
(28 3 (:REWRITE VL2014::ALISTP-WHEN-VL-ATTS-P-REWRITE))
(27 27 (:REWRITE VL2014::CONSP-WHEN-MEMBER-EQUAL-OF-VL-USERTYPES-P . 2))
(27 27 (:REWRITE VL2014::CONSP-WHEN-MEMBER-EQUAL-OF-VL-USERTYPES-P . 1))
(27 27 (:REWRITE VL2014::CONSP-WHEN-MEMBER-EQUAL-OF-VL-ATTS-P . 2))
(27 27 (:REWRITE VL2014::CONSP-WHEN-MEMBER-EQUAL-OF-VL-ATTS-P . 1))
(24 3 (:REWRITE SET::SETS-ARE-TRUE-LISTS-CHEAP))
(24 2 (:LINEAR VL2014::LEN-OF-CDR-STRONG))
(22 3 (:REWRITE ALISTP-WHEN-HONS-DUPLICITY-ALIST-P))
(22 3 (:REWRITE VL2014::ALISTP-WHEN-ALL-HAVE-LEN))
(15 15 (:TYPE-PRESCRIPTION OMAP::MAPP))
(15 3 (:REWRITE OMAP::MFIX-IMPLIES-MAPP))
(15 3 (:REWRITE OMAP::MAPP-WHEN-NOT-EMPTY))
(14 14 (:REWRITE DEFAULT-CDR))
(14 2 (:REWRITE |(< 0 (len x))|))
(13 13 (:REWRITE CAR-WHEN-ALL-EQUALP))
(13 3 (:REWRITE VL2014::VL-TOKENLISTLIST-P-WHEN-NOT-CONSP))
(13 3 (:REWRITE VL2014::VL-ATTS-P-WHEN-NOT-CONSP))
(13 3 (:REWRITE HONS-DUPLICITY-ALIST-P-WHEN-NOT-CONSP))
(13 3 (:REWRITE VL2014::ALL-HAVE-LEN-WHEN-NOT-CONSP))
(13 3 (:REWRITE ALISTP-WHEN-ATOM))
(12 6 (:REWRITE SYMBOL-LISTP-WHEN-SUBSETP-EQUAL))
(12 3 (:REWRITE VL2014::STRING-LISTP-WHEN-NO-NILS-IN-VL-MAYBE-STRING-LISTP))
(12 2 (:REWRITE NTH-WHEN-ATOM))
(12 2 (:REWRITE VL2014::NTH-OF-ATOM))
(9 3 (:REWRITE VL2014::SYMBOL-LISTP-WHEN-SUBSETP-EQUAL-OF-SYMBOL-LISTP . 1))
(7 7 (:REWRITE-QUOTED-CONSTANT VL2014::VL-OP-FIX-UNDER-VL-OP-EQUIV))
(7 7 (:REWRITE VL2014::FAILS-GRACEFULLY-VL-PARSE-LVALUE))
(6 6 (:TYPE-PRESCRIPTION SUBSETP-EQUAL))
(6 6 (:TYPE-PRESCRIPTION SET::SETP-TYPE))
(6 6 (:TYPE-PRESCRIPTION OMAP::MFIX))
(6 6 (:TYPE-PRESCRIPTION HONS-DUPLICITY-ALIST-P))
(6 6 (:TYPE-PRESCRIPTION OMAP::EMPTY))
(6 6 (:TYPE-PRESCRIPTION VL2014::ALL-HAVE-LEN))
(6 6 (:TYPE-PRESCRIPTION ALISTP))
(6 6 (:REWRITE-QUOTED-CONSTANT VL2014::VL-MAYBE-EXPRTYPE-FIX-UNDER-VL-MAYBE-EXPRTYPE-EQUIV))
(6 6 (:REWRITE-QUOTED-CONSTANT VL2014::VL-ATTS-FIX-UNDER-VL-ATTS-EQUIV))
(6 6 (:REWRITE-QUOTED-CONSTANT MAYBE-NATP-FIX-UNDER-MAYBE-NAT-EQUIV))
(6 6 (:REWRITE VL2014::VL-TOKENLISTLIST-P-WHEN-SUBSETP-EQUAL))
(6 6 (:REWRITE VL2014::VL-TOKENLIST-P-WHEN-SUBSETP-EQUAL))
(6 6 (:REWRITE VL2014::VL-TOKENLIST-P-WHEN-MEMBER-EQUAL-OF-VL-TOKENLISTLIST-P))
(6 6 (:REWRITE VL2014::VL-ATTS-P-WHEN-SUBSETP-EQUAL))
(6 6 (:REWRITE VL2014::TRUE-LISTP-WHEN-MEMBER-EQUAL-OF-TRUE-LIST-LISTP))
(6 6 (:REWRITE VL2014::SYMBOL-LISTP-WHEN-MEMBER-EQUAL-OF-SYMBOL-LIST-LISTP))
(6 6 (:REWRITE VL2014::SYMBOL-LISTP-OF-ALIST-VALS-OF-VL-FULL-KEYWORD-TABLE))
(6 6 (:REWRITE STRING-LISTP-WHEN-SUBSETP-EQUAL))
(6 6 (:REWRITE VL2014::STRING-LISTP-WHEN-MEMBER-EQUAL-OF-STRING-LIST-LISTP))
(6 6 (:REWRITE CHARACTER-LISTP-WHEN-SUBSETP-EQUAL))
(6 6 (:LINEAR LOWER-BOUND-OF-LEN-WHEN-SUBLISTP))
(6 6 (:LINEAR LISTPOS-UPPER-BOUND-STRONG-2))
(6 6 (:LINEAR LEN-WHEN-PREFIXP))
(6 3 (:TYPE-PRESCRIPTION TRUE-LISTP-MEMBER-EQUAL))
(6 3 (:REWRITE SYMBOL-LISTP-WHEN-BOOLEAN-LISTP))
(6 3 (:REWRITE OMAP::SETP-WHEN-MAPP))
(6 3 (:REWRITE SET::NONEMPTY-MEANS-SET))
(6 3 (:REWRITE OMAP::MFIX-WHEN-MAPP))
(6 3 (:REWRITE OMAP::MAPP-NON-NIL-IMPLIES-NON-EMPTY))
(6 3 (:REWRITE SET::DOUBLE-CONTAINMENT))
(6 3 (:REWRITE CONSP-OF-CAR-WHEN-CONS-LISTP))
(6 3 (:REWRITE CONSP-OF-CAR-WHEN-ATOM-LISTP))
(6 3 (:REWRITE STR::CHARACTER-LISTP-WHEN-OCT-DIGIT-CHAR-LISTP))
(6 3 (:REWRITE STR::CHARACTER-LISTP-WHEN-HEX-DIGIT-CHAR-LISTP))
(6 3 (:REWRITE STR::CHARACTER-LISTP-WHEN-DEC-DIGIT-CHAR-LISTP))
(6 2 (:REWRITE NTH-WITH-LARGE-INDEX))
(6 2 (:REWRITE NTH-WHEN-TOO-LARGE-CHEAP))
(3 3 (:TYPE-PRESCRIPTION SET::EMPTY-TYPE))
(3 3 (:TYPE-PRESCRIPTION CONSP-MEMBER-EQUAL))
(3 3 (:REWRITE TRUE-LISTP-WHEN-UNSIGNED-BYTE-LISTP))
(3 3 (:REWRITE TRUE-LISTP-WHEN-SIGNED-BYTE-LISTP))
(3 3 (:REWRITE VL2014::SYMBOL-LISTP-WHEN-SUBSETP-EQUAL-OF-SYMBOL-LISTP . 2))
(3 3 (:REWRITE SYMBOL-LISTP-WHEN-NOT-CONSP))
(3 3 (:REWRITE VL2014::STRING-LISTP-WHEN-SUBSETP-EQUAL-OF-STRING-LISTP . 2))
(3 3 (:REWRITE VL2014::STRING-LISTP-WHEN-SUBSETP-EQUAL-OF-STRING-LISTP . 1))
(3 3 (:REWRITE STRING-LISTP-WHEN-NOT-CONSP))
(3 3 (:REWRITE SET::IN-SET))
(3 3 (:REWRITE FN-CHECK-DEF-FORMALS))
(3 3 (:REWRITE CHARACTER-LISTP-WHEN-NOT-CONSP))
(3 3 (:META CANCEL_TIMES-EQUAL-CORRECT))
(3 3 (:META CANCEL_PLUS-EQUAL-CORRECT))
(3 3 (:LINEAR LEQ-POSITION-EQUAL-LEN))
(3 3 (:LINEAR INDEX-OF-<-LEN))
(3 3 (:LINEAR STR::COUNT-LEADING-CHARSET-LEN))
(2 2 (:REWRITE NTH-WHEN-ZP))
(2 2 (:REWRITE NTH-WHEN-PREFIXP))
)
(VL2014::VL-PARSE-ASSIGNMENT-FN)
(VL2014::VL-PARSE-ASSIGNMENT-FAILS-GRACEFULLY
(70 35 (:TYPE-PRESCRIPTION VL2014::VL-IS-TOKEN?-FN-WHEN-ATOM-OF-TOKENS))
(36 3 (:REWRITE VL2014::VL-PARSE-EXPRESSION-EOF-VL-PARSE-EXPRESSION))
(21 3 (:REWRITE VL2014::VL-MATCH-TOKEN-FAILS-GRACEFULLY))
(6 6 (:REWRITE CONSP-WHEN-MEMBER-EQUAL-OF-CONS-LISTP))
(6 6 (:REWRITE CONSP-WHEN-MEMBER-EQUAL-OF-ATOM-LISTP))
(6 3 (:REWRITE CONSP-UNDER-IFF-WHEN-TRUE-LISTP))
(3 3 (:TYPE-PRESCRIPTION TRUE-LISTP))
(3 3 (:REWRITE VL2014::CONSP-WHEN-MEMBER-EQUAL-OF-VL-USERTYPES-P . 2))
(3 3 (:REWRITE VL2014::CONSP-WHEN-MEMBER-EQUAL-OF-VL-USERTYPES-P . 1))
(3 3 (:REWRITE VL2014::CONSP-WHEN-MEMBER-EQUAL-OF-VL-ATTS-P . 2))
(3 3 (:REWRITE VL2014::CONSP-WHEN-MEMBER-EQUAL-OF-VL-ATTS-P . 1))
(3 3 (:REWRITE CONSP-BY-LEN))
)
(VL2014::VL-WARNING-P-OF-VL-PARSE-ASSIGNMENT
(39 3 (:REWRITE VL2014::VL-PARSE-EXPRESSION-VAL-WHEN-ERROR-VL-PARSE-EXPRESSION))
(36 3 (:REWRITE VL2014::VL-PARSE-EXPRESSION-EOF-VL-PARSE-EXPRESSION))
(21 3 (:REWRITE VL2014::VL-MATCH-TOKEN-FAILS-GRACEFULLY))
(12 6 (:TYPE-PRESCRIPTION VL2014::VL-IS-TOKEN?-FN-WHEN-ATOM-OF-TOKENS))
(6 6 (:TYPE-PRESCRIPTION VL2014::VL-IS-TOKEN?$INLINE))
(6 6 (:TYPE-PRESCRIPTION ATOM))
(6 6 (:REWRITE CONSP-WHEN-MEMBER-EQUAL-OF-CONS-LISTP))
(6 6 (:REWRITE CONSP-WHEN-MEMBER-EQUAL-OF-ATOM-LISTP))
(6 3 (:REWRITE CONSP-UNDER-IFF-WHEN-TRUE-LISTP))
(3 3 (:TYPE-PRESCRIPTION TRUE-LISTP))
(3 3 (:REWRITE VL2014::CONSP-WHEN-MEMBER-EQUAL-OF-VL-USERTYPES-P . 2))
(3 3 (:REWRITE VL2014::CONSP-WHEN-MEMBER-EQUAL-OF-VL-USERTYPES-P . 1))
(3 3 (:REWRITE VL2014::CONSP-WHEN-MEMBER-EQUAL-OF-VL-ATTS-P . 2))
(3 3 (:REWRITE VL2014::CONSP-WHEN-MEMBER-EQUAL-OF-VL-ATTS-P . 1))
(3 3 (:REWRITE CONSP-BY-LEN))
(2 2 (:REWRITE VL2014::VL-WARNING-P-WHEN-MEMBER-EQUAL-OF-VL-WARNINGLIST-P))
)
(VL2014::VL-PARSE-ASSIGNMENT-RESULT
(16 4 (:REWRITE VL2014::VL-PARSE-EXPRESSION-VAL-WHEN-ERROR-VL-PARSE-EXPRESSION))
(16 4 (:REWRITE VL2014::VL-MATCH-TOKEN-FAILS-GRACEFULLY))
(12 1 (:REWRITE VL2014::VL-PARSE-EXPRESSION-EOF-VL-PARSE-EXPRESSION))
(8 4 (:TYPE-PRESCRIPTION VL2014::VL-IS-TOKEN?-FN-WHEN-ATOM-OF-TOKENS))
(4 4 (:TYPE-PRESCRIPTION VL2014::VL-IS-TOKEN?$INLINE))
(4 4 (:TYPE-PRESCRIPTION ATOM))
(4 4 (:REWRITE VL2014::FAILS-GRACEFULLY-VL-PARSE-LVALUE))
(2 2 (:REWRITE CONSP-WHEN-MEMBER-EQUAL-OF-CONS-LISTP))
(2 2 (:REWRITE CONSP-WHEN-MEMBER-EQUAL-OF-ATOM-LISTP))
(2 1 (:REWRITE CONSP-UNDER-IFF-WHEN-TRUE-LISTP))
(1 1 (:TYPE-PRESCRIPTION TRUE-LISTP))
(1 1 (:REWRITE DEFAULT-CDR))
(1 1 (:REWRITE DEFAULT-CAR))
(1 1 (:REWRITE VL2014::CONSP-WHEN-MEMBER-EQUAL-OF-VL-USERTYPES-P . 2))
(1 1 (:REWRITE VL2014::CONSP-WHEN-MEMBER-EQUAL-OF-VL-USERTYPES-P . 1))
(1 1 (:REWRITE VL2014::CONSP-WHEN-MEMBER-EQUAL-OF-VL-ATTS-P . 2))
(1 1 (:REWRITE VL2014::CONSP-WHEN-MEMBER-EQUAL-OF-VL-ATTS-P . 1))
(1 1 (:REWRITE CONSP-BY-LEN))
(1 1 (:REWRITE CAR-WHEN-ALL-EQUALP))
)
(VL2014::VL-PARSE-ASSIGNMENT-COUNT-STRONG
(620 5 (:REWRITE LOWER-BOUND-OF-LEN-WHEN-SUBLISTP))
(596 7 (:REWRITE PREFIXP-WHEN-EQUAL-LENGTHS))
(586 58 (:REWRITE LEN-WHEN-ATOM))
(564 2 (:REWRITE SUBLISTP-WHEN-PREFIXP))
(306 7 (:REWRITE PREFIXP-WHEN-PREFIXP))
(189 5 (:REWRITE LEN-WHEN-PREFIXP))
(126 126 (:REWRITE CONSP-WHEN-MEMBER-EQUAL-OF-CONS-LISTP))
(126 126 (:REWRITE CONSP-WHEN-MEMBER-EQUAL-OF-ATOM-LISTP))
(126 63 (:REWRITE CONSP-UNDER-IFF-WHEN-TRUE-LISTP))
(63 63 (:TYPE-PRESCRIPTION TRUE-LISTP))
(63 63 (:REWRITE VL2014::CONSP-WHEN-MEMBER-EQUAL-OF-VL-USERTYPES-P . 2))
(63 63 (:REWRITE VL2014::CONSP-WHEN-MEMBER-EQUAL-OF-VL-USERTYPES-P . 1))
(63 63 (:REWRITE VL2014::CONSP-WHEN-MEMBER-EQUAL-OF-VL-ATTS-P . 2))
(63 63 (:REWRITE VL2014::CONSP-WHEN-MEMBER-EQUAL-OF-VL-ATTS-P . 1))
(63 63 (:REWRITE CONSP-BY-LEN))
(38 5 (:REWRITE PREFIXP-WHEN-NOT-CONSP-RIGHT))
(38 5 (:REWRITE PREFIXP-WHEN-NOT-CONSP-LEFT))
(36 36 (:LINEAR LOWER-BOUND-OF-LEN-WHEN-SUBLISTP))
(36 36 (:LINEAR LISTPOS-UPPER-BOUND-STRONG-2))
(36 36 (:LINEAR LEN-WHEN-PREFIXP))
(36 3 (:REWRITE VL2014::VL-PARSE-EXPRESSION-EOF-VL-PARSE-EXPRESSION))
(27 3 (:REWRITE VL2014::VL-PARSE-EXPRESSION-VAL-WHEN-ERROR-VL-PARSE-EXPRESSION))
(24 12 (:TYPE-PRESCRIPTION VL2014::VL-IS-TOKEN?-FN-WHEN-ATOM-OF-TOKENS))
(24 6 (:REWRITE VL2014::VL-MATCH-TOKEN-UNDER-IFF))
(24 2 (:REWRITE SUBLISTP-WHEN-ATOM-RIGHT))
(24 2 (:REWRITE SUBLISTP-WHEN-ATOM-LEFT))
(21 3 (:REWRITE VL2014::VL-MATCH-TOKEN-FAILS-GRACEFULLY))
(18 18 (:LINEAR LEQ-POSITION-EQUAL-LEN))
(18 18 (:LINEAR INDEX-OF-<-LEN))
(18 18 (:LINEAR STR::COUNT-LEADING-CHARSET-LEN))
(17 17 (:TYPE-PRESCRIPTION PREFIXP))
(14 14 (:REWRITE VL2014::PREFIXP-WHEN-MEMBER-EQUAL-OF-PREFIX-OF-EACHP))
(13 2 (:REWRITE LIST-EQUIV-WHEN-ATOM-RIGHT))
(13 2 (:REWRITE LIST-EQUIV-WHEN-ATOM-LEFT))
(12 12 (:TYPE-PRESCRIPTION VL2014::VL-IS-TOKEN?$INLINE))
(12 12 (:TYPE-PRESCRIPTION ATOM))
(10 5 (:REWRITE DEFAULT-<-2))
(10 5 (:REWRITE DEFAULT-<-1))
(7 7 (:TYPE-PRESCRIPTION SUBLISTP))
(7 7 (:REWRITE VL2014::TRANSITIVITY-OF-PREFIXP))
(7 7 (:REWRITE PREFIXP-TRANSITIVE . 2))
(7 7 (:REWRITE PREFIXP-TRANSITIVE . 1))
(7 7 (:REWRITE PREFIXP-ONE-WAY-OR-ANOTHER . 2))
(7 7 (:REWRITE PREFIXP-ONE-WAY-OR-ANOTHER . 1))
(5 5 (:META CANCEL_PLUS-LESSP-CORRECT))
(3 3 (:REWRITE VL2014::FAILS-GRACEFULLY-VL-PARSE-LVALUE))
(2 2 (:TYPE-PRESCRIPTION LIST-EQUIV))
(2 2 (:REWRITE SUBLISTP-COMPLETE))
)
|
