forked from ahja-itu/ITU-PV22-mini-project
-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathADTTest.glob
804 lines (804 loc) · 34.4 KB
/
ADTTest.glob
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
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
DIGEST ba79af41dcfb9e783c3dc62767a6aea1
FVFA.ADTTest
R70:75 Coq.Strings.String <> <> lib
R102:104 VFA.ADT <> <> lib
ax 118:124 <> MISSING
mod 141:145 <> Check
R211:217 VFA.ADTTest <> MISSING defax
R211:217 VFA.ADTTest <> MISSING defax
R410:413 Coq.Init.Datatypes <> Some constr
R410:413 Coq.Init.Datatypes <> Some constr
R593:596 Coq.Init.Datatypes <> None constr
R593:596 Coq.Init.Datatypes <> None constr
R678:682 VFA.ADTTest Check <> mod
R710:712 VFA.ADT <> <> lib
R722:726 VFA.ADTTest Check <> mod
def 730:738 <> Unnamed_thm
R735:738 Coq.Init.Logic <> True ind
R932:990 VFA.ADT StringListsTableExamples.StringListsTable get_empty_default prfax
R1006:1050 VFA.ADT StringListsTableExamples.StringListsTable key def
binder 1002:1002 <> k:2
R1152:1155 Coq.Init.Logic <> ::type_scope:x_'='_x not
R1054:1098 VFA.ADT StringListsTableExamples.StringListsTable get prfax
R1100:1100 VFA.ADTTest <> k:2 var
R1105:1151 VFA.ADT StringListsTableExamples.StringListsTable empty def
R1156:1204 VFA.ADT StringListsTableExamples.StringListsTable default def
R932:990 VFA.ADT StringListsTableExamples.StringListsTable get_empty_default prfax
R1006:1050 VFA.ADT StringListsTableExamples.StringListsTable key def
binder 1002:1002 <> k:3
R1152:1155 Coq.Init.Logic <> ::type_scope:x_'='_x not
R1054:1098 VFA.ADT StringListsTableExamples.StringListsTable get prfax
R1100:1100 VFA.ADTTest <> k:3 var
R1105:1151 VFA.ADT StringListsTableExamples.StringListsTable empty def
R1156:1204 VFA.ADT StringListsTableExamples.StringListsTable default def
R1256:1314 VFA.ADT StringListsTableExamples.StringListsTable get_empty_default prfax
def 1317:1325 <> Unnamed_thm
R1322:1325 Coq.Init.Logic <> True ind
R1449:1502 VFA.ADT StringListsTableExamples.StringListsTable get_set_same prfax
R1519:1563 VFA.ADT StringListsTableExamples.StringListsTable key def
binder 1515:1515 <> k:4
R1574:1616 VFA.ADT StringListsTableExamples.StringListsTable V def
binder 1570:1570 <> v:5
R1627:1673 VFA.ADT StringListsTableExamples.StringListsTable table def
binder 1623:1623 <> t:6
R1782:1784 Coq.Init.Logic <> ::type_scope:x_'='_x not
R1678:1722 VFA.ADT StringListsTableExamples.StringListsTable get prfax
R1724:1724 VFA.ADTTest <> k:4 var
R1730:1774 VFA.ADT StringListsTableExamples.StringListsTable set prfax
R1776:1776 VFA.ADTTest <> k:4 var
R1778:1778 VFA.ADTTest <> v:5 var
R1780:1780 VFA.ADTTest <> t:6 var
R1785:1785 VFA.ADTTest <> v:5 var
R1449:1502 VFA.ADT StringListsTableExamples.StringListsTable get_set_same prfax
R1519:1563 VFA.ADT StringListsTableExamples.StringListsTable key def
binder 1515:1515 <> k:7
R1574:1616 VFA.ADT StringListsTableExamples.StringListsTable V def
binder 1570:1570 <> v:8
R1627:1673 VFA.ADT StringListsTableExamples.StringListsTable table def
binder 1623:1623 <> t:9
R1782:1784 Coq.Init.Logic <> ::type_scope:x_'='_x not
R1678:1722 VFA.ADT StringListsTableExamples.StringListsTable get prfax
R1724:1724 VFA.ADTTest <> k:7 var
R1730:1774 VFA.ADT StringListsTableExamples.StringListsTable set prfax
R1776:1776 VFA.ADTTest <> k:7 var
R1778:1778 VFA.ADTTest <> v:8 var
R1780:1780 VFA.ADTTest <> t:9 var
R1785:1785 VFA.ADTTest <> v:8 var
R1837:1890 VFA.ADT StringListsTableExamples.StringListsTable get_set_same prfax
def 1893:1901 <> Unnamed_thm
R1898:1901 Coq.Init.Logic <> True ind
R2026:2080 VFA.ADT StringListsTableExamples.StringListsTable get_set_other prfax
R2100:2144 VFA.ADT StringListsTableExamples.StringListsTable key def
binder 2093:2093 <> k:10
binder 2095:2096 <> k':11
R2155:2197 VFA.ADT StringListsTableExamples.StringListsTable V def
binder 2151:2151 <> v:12
R2208:2254 VFA.ADT StringListsTableExamples.StringListsTable table def
binder 2204:2204 <> t:13
R2266:2270 Coq.Init.Logic <> ::type_scope:x_'->'_x not
R2260:2263 Coq.Init.Logic <> ::type_scope:x_'<>'_x not
R2259:2259 VFA.ADTTest <> k:10 var
R2264:2265 VFA.ADTTest <> k':11 var
R2376:2379 Coq.Init.Logic <> ::type_scope:x_'='_x not
R2271:2315 VFA.ADT StringListsTableExamples.StringListsTable get prfax
R2317:2318 VFA.ADTTest <> k':11 var
R2324:2368 VFA.ADT StringListsTableExamples.StringListsTable set prfax
R2370:2370 VFA.ADTTest <> k:10 var
R2372:2372 VFA.ADTTest <> v:12 var
R2374:2374 VFA.ADTTest <> t:13 var
R2380:2424 VFA.ADT StringListsTableExamples.StringListsTable get prfax
R2426:2427 VFA.ADTTest <> k':11 var
R2429:2429 VFA.ADTTest <> t:13 var
R2026:2080 VFA.ADT StringListsTableExamples.StringListsTable get_set_other prfax
R2100:2144 VFA.ADT StringListsTableExamples.StringListsTable key def
binder 2093:2093 <> k:14
binder 2095:2096 <> k':15
R2155:2197 VFA.ADT StringListsTableExamples.StringListsTable V def
binder 2151:2151 <> v:16
R2208:2254 VFA.ADT StringListsTableExamples.StringListsTable table def
binder 2204:2204 <> t:17
R2266:2270 Coq.Init.Logic <> ::type_scope:x_'->'_x not
R2260:2263 Coq.Init.Logic <> ::type_scope:x_'<>'_x not
R2259:2259 VFA.ADTTest <> k:14 var
R2264:2265 VFA.ADTTest <> k':15 var
R2376:2379 Coq.Init.Logic <> ::type_scope:x_'='_x not
R2271:2315 VFA.ADT StringListsTableExamples.StringListsTable get prfax
R2317:2318 VFA.ADTTest <> k':15 var
R2324:2368 VFA.ADT StringListsTableExamples.StringListsTable set prfax
R2370:2370 VFA.ADTTest <> k:14 var
R2372:2372 VFA.ADTTest <> v:16 var
R2374:2374 VFA.ADTTest <> t:17 var
R2380:2424 VFA.ADT StringListsTableExamples.StringListsTable get prfax
R2426:2427 VFA.ADTTest <> k':15 var
R2429:2429 VFA.ADTTest <> t:17 var
R2481:2535 VFA.ADT StringListsTableExamples.StringListsTable get_set_other prfax
def 2538:2546 <> Unnamed_thm
R2543:2546 Coq.Init.Logic <> True ind
R2644:2671 VFA.ADT StringListsTableExamples ex1 prfax
R2774:2776 Coq.Init.Logic <> ::type_scope:x_'='_x not
R2676:2720 VFA.ADT StringListsTableExamples.StringListsTable get prfax
R2727:2773 VFA.ADT StringListsTableExamples.StringListsTable empty def
R2777:2794 Coq.Strings.String <> EmptyString constr
R2644:2671 VFA.ADT StringListsTableExamples ex1 prfax
R2774:2776 Coq.Init.Logic <> ::type_scope:x_'='_x not
R2676:2720 VFA.ADT StringListsTableExamples.StringListsTable get prfax
R2727:2773 VFA.ADT StringListsTableExamples.StringListsTable empty def
R2777:2794 Coq.Strings.String <> EmptyString constr
R2846:2873 VFA.ADT StringListsTableExamples ex1 prfax
def 2876:2884 <> Unnamed_thm
R2881:2884 Coq.Init.Logic <> True ind
R2982:3009 VFA.ADT StringListsTableExamples ex2 prfax
R3281:3284 Coq.Init.Logic <> ::type_scope:x_'='_x not
R3014:3058 VFA.ADT StringListsTableExamples.StringListsTable get prfax
R3066:3110 VFA.ADT StringListsTableExamples.StringListsTable set prfax
R3121:3133 Coq.Strings.String <> String constr
R3145:3155 Coq.Strings.Ascii <> Ascii constr
R3157:3160 Coq.Init.Datatypes <> true constr
R3162:3166 Coq.Init.Datatypes <> false constr
R3168:3172 Coq.Init.Datatypes <> false constr
R3174:3178 Coq.Init.Datatypes <> false constr
R3180:3184 Coq.Init.Datatypes <> false constr
R3186:3190 Coq.Init.Datatypes <> false constr
R3192:3195 Coq.Init.Datatypes <> true constr
R3197:3201 Coq.Init.Datatypes <> false constr
R3213:3230 Coq.Strings.String <> EmptyString constr
R3233:3279 VFA.ADT StringListsTableExamples.StringListsTable empty def
R3285:3297 Coq.Strings.String <> String constr
R3300:3310 Coq.Strings.Ascii <> Ascii constr
R3312:3315 Coq.Init.Datatypes <> true constr
R3317:3321 Coq.Init.Datatypes <> false constr
R3323:3327 Coq.Init.Datatypes <> false constr
R3329:3333 Coq.Init.Datatypes <> false constr
R3335:3339 Coq.Init.Datatypes <> false constr
R3341:3345 Coq.Init.Datatypes <> false constr
R3347:3350 Coq.Init.Datatypes <> true constr
R3352:3356 Coq.Init.Datatypes <> false constr
R3362:3379 Coq.Strings.String <> EmptyString constr
R2982:3009 VFA.ADT StringListsTableExamples ex2 prfax
R3281:3284 Coq.Init.Logic <> ::type_scope:x_'='_x not
R3014:3058 VFA.ADT StringListsTableExamples.StringListsTable get prfax
R3066:3110 VFA.ADT StringListsTableExamples.StringListsTable set prfax
R3121:3133 Coq.Strings.String <> String constr
R3145:3155 Coq.Strings.Ascii <> Ascii constr
R3157:3160 Coq.Init.Datatypes <> true constr
R3162:3166 Coq.Init.Datatypes <> false constr
R3168:3172 Coq.Init.Datatypes <> false constr
R3174:3178 Coq.Init.Datatypes <> false constr
R3180:3184 Coq.Init.Datatypes <> false constr
R3186:3190 Coq.Init.Datatypes <> false constr
R3192:3195 Coq.Init.Datatypes <> true constr
R3197:3201 Coq.Init.Datatypes <> false constr
R3213:3230 Coq.Strings.String <> EmptyString constr
R3233:3279 VFA.ADT StringListsTableExamples.StringListsTable empty def
R3285:3297 Coq.Strings.String <> String constr
R3300:3310 Coq.Strings.Ascii <> Ascii constr
R3312:3315 Coq.Init.Datatypes <> true constr
R3317:3321 Coq.Init.Datatypes <> false constr
R3323:3327 Coq.Init.Datatypes <> false constr
R3329:3333 Coq.Init.Datatypes <> false constr
R3335:3339 Coq.Init.Datatypes <> false constr
R3341:3345 Coq.Init.Datatypes <> false constr
R3347:3350 Coq.Init.Datatypes <> true constr
R3352:3356 Coq.Init.Datatypes <> false constr
R3362:3379 Coq.Strings.String <> EmptyString constr
R3431:3458 VFA.ADT StringListsTableExamples ex2 prfax
def 3461:3469 <> Unnamed_thm
R3466:3469 Coq.Init.Logic <> True ind
R3567:3594 VFA.ADT StringListsTableExamples ex3 prfax
R3866:3869 Coq.Init.Logic <> ::type_scope:x_'='_x not
R3599:3643 VFA.ADT StringListsTableExamples.StringListsTable get prfax
R3651:3695 VFA.ADT StringListsTableExamples.StringListsTable set prfax
R3706:3718 Coq.Strings.String <> String constr
R3730:3740 Coq.Strings.Ascii <> Ascii constr
R3742:3745 Coq.Init.Datatypes <> true constr
R3747:3751 Coq.Init.Datatypes <> false constr
R3753:3757 Coq.Init.Datatypes <> false constr
R3759:3763 Coq.Init.Datatypes <> false constr
R3765:3769 Coq.Init.Datatypes <> false constr
R3771:3775 Coq.Init.Datatypes <> false constr
R3777:3780 Coq.Init.Datatypes <> true constr
R3782:3786 Coq.Init.Datatypes <> false constr
R3798:3815 Coq.Strings.String <> EmptyString constr
R3818:3864 VFA.ADT StringListsTableExamples.StringListsTable empty def
R3870:3887 Coq.Strings.String <> EmptyString constr
R3567:3594 VFA.ADT StringListsTableExamples ex3 prfax
R3866:3869 Coq.Init.Logic <> ::type_scope:x_'='_x not
R3599:3643 VFA.ADT StringListsTableExamples.StringListsTable get prfax
R3651:3695 VFA.ADT StringListsTableExamples.StringListsTable set prfax
R3706:3718 Coq.Strings.String <> String constr
R3730:3740 Coq.Strings.Ascii <> Ascii constr
R3742:3745 Coq.Init.Datatypes <> true constr
R3747:3751 Coq.Init.Datatypes <> false constr
R3753:3757 Coq.Init.Datatypes <> false constr
R3759:3763 Coq.Init.Datatypes <> false constr
R3765:3769 Coq.Init.Datatypes <> false constr
R3771:3775 Coq.Init.Datatypes <> false constr
R3777:3780 Coq.Init.Datatypes <> true constr
R3782:3786 Coq.Init.Datatypes <> false constr
R3798:3815 Coq.Strings.String <> EmptyString constr
R3818:3864 VFA.ADT StringListsTableExamples.StringListsTable empty def
R3870:3887 Coq.Strings.String <> EmptyString constr
R3939:3966 VFA.ADT StringListsTableExamples ex3 prfax
def 3969:3977 <> Unnamed_thm
R3974:3977 Coq.Init.Logic <> True ind
R4155:4182 VFA.ADT StringListETableAbs empty_ok prfax
R4187:4212 VFA.ADT StringListETableAbs rep_ok prfax
R4214:4238 VFA.ADT StringListETableAbs empty prfax
R4155:4182 VFA.ADT StringListETableAbs empty_ok prfax
R4187:4212 VFA.ADT StringListETableAbs rep_ok prfax
R4214:4238 VFA.ADT StringListETableAbs empty prfax
R4290:4317 VFA.ADT StringListETableAbs empty_ok prfax
def 4320:4328 <> Unnamed_thm
R4325:4328 Coq.Init.Logic <> True ind
R4424:4449 VFA.ADT StringListETableAbs set_ok prfax
R4466:4488 VFA.ADT StringListETableAbs key def
binder 4462:4462 <> k:18
R4496:4516 VFA.ADT StringListETableAbs V def
binder 4492:4492 <> v:19
R4527:4551 VFA.ADT StringListETableAbs table def
binder 4523:4523 <> t:20
R4584:4588 Coq.Init.Logic <> ::type_scope:x_'->'_x not
R4556:4581 VFA.ADT StringListETableAbs rep_ok prfax
R4583:4583 VFA.ADTTest <> t:20 var
R4589:4614 VFA.ADT StringListETableAbs rep_ok prfax
R4617:4639 VFA.ADT StringListETableAbs set prfax
R4641:4641 VFA.ADTTest <> k:18 var
R4643:4643 VFA.ADTTest <> v:19 var
R4645:4645 VFA.ADTTest <> t:20 var
R4424:4449 VFA.ADT StringListETableAbs set_ok prfax
R4466:4488 VFA.ADT StringListETableAbs key def
binder 4462:4462 <> k:21
R4496:4516 VFA.ADT StringListETableAbs V def
binder 4492:4492 <> v:22
R4527:4551 VFA.ADT StringListETableAbs table def
binder 4523:4523 <> t:23
R4584:4588 Coq.Init.Logic <> ::type_scope:x_'->'_x not
R4556:4581 VFA.ADT StringListETableAbs rep_ok prfax
R4583:4583 VFA.ADTTest <> t:23 var
R4589:4614 VFA.ADT StringListETableAbs rep_ok prfax
R4617:4639 VFA.ADT StringListETableAbs set prfax
R4641:4641 VFA.ADTTest <> k:21 var
R4643:4643 VFA.ADTTest <> v:22 var
R4645:4645 VFA.ADTTest <> t:23 var
R4698:4723 VFA.ADT StringListETableAbs set_ok prfax
def 4726:4734 <> Unnamed_thm
R4731:4734 Coq.Init.Logic <> True ind
R4836:4867 VFA.ADT StringListETableAbs empty_relate prfax
R4921:4924 Coq.Init.Logic <> ::type_scope:x_'='_x not
R4872:4894 VFA.ADT StringListETableAbs Abs prfax
R4896:4920 VFA.ADT StringListETableAbs empty prfax
R4926:4934 VFA.ADT <> empty_map def
R4936:4956 VFA.ADT StringListETableAbs V def
R4836:4867 VFA.ADT StringListETableAbs empty_relate prfax
R4921:4924 Coq.Init.Logic <> ::type_scope:x_'='_x not
R4872:4894 VFA.ADT StringListETableAbs Abs prfax
R4896:4920 VFA.ADT StringListETableAbs empty prfax
R4926:4934 VFA.ADT <> empty_map def
R4936:4956 VFA.ADT StringListETableAbs V def
R5008:5039 VFA.ADT StringListETableAbs empty_relate prfax
def 5042:5050 <> Unnamed_thm
R5047:5050 Coq.Init.Logic <> True ind
R5152:5183 VFA.ADT StringListETableAbs bound_relate prfax
R5200:5224 VFA.ADT StringListETableAbs table def
binder 5196:5196 <> t:24
R5232:5254 VFA.ADT StringListETableAbs key def
binder 5228:5228 <> k:25
R5287:5291 Coq.Init.Logic <> ::type_scope:x_'->'_x not
R5259:5284 VFA.ADT StringListETableAbs rep_ok prfax
R5286:5286 VFA.ADTTest <> t:24 var
R5365:5368 Coq.Init.Logic <> ::type_scope:x_'='_x not
R5293:5312 VFA.SearchTree <> map_bound def
R5314:5334 VFA.ADT StringListETableAbs V def
R5336:5336 VFA.ADTTest <> k:25 var
R5339:5361 VFA.ADT StringListETableAbs Abs prfax
R5363:5363 VFA.ADTTest <> t:24 var
R5369:5393 VFA.ADT StringListETableAbs bound prfax
R5395:5395 VFA.ADTTest <> k:25 var
R5397:5397 VFA.ADTTest <> t:24 var
R5152:5183 VFA.ADT StringListETableAbs bound_relate prfax
R5200:5224 VFA.ADT StringListETableAbs table def
binder 5196:5196 <> t:26
R5232:5254 VFA.ADT StringListETableAbs key def
binder 5228:5228 <> k:27
R5287:5291 Coq.Init.Logic <> ::type_scope:x_'->'_x not
R5259:5284 VFA.ADT StringListETableAbs rep_ok prfax
R5286:5286 VFA.ADTTest <> t:26 var
R5365:5368 Coq.Init.Logic <> ::type_scope:x_'='_x not
R5293:5312 VFA.SearchTree <> map_bound def
R5314:5334 VFA.ADT StringListETableAbs V def
R5336:5336 VFA.ADTTest <> k:27 var
R5339:5361 VFA.ADT StringListETableAbs Abs prfax
R5363:5363 VFA.ADTTest <> t:26 var
R5369:5393 VFA.ADT StringListETableAbs bound prfax
R5395:5395 VFA.ADTTest <> k:27 var
R5397:5397 VFA.ADTTest <> t:26 var
R5449:5480 VFA.ADT StringListETableAbs bound_relate prfax
def 5483:5491 <> Unnamed_thm
R5488:5491 Coq.Init.Logic <> True ind
R5594:5626 VFA.ADT StringListETableAbs lookup_relate prfax
R5643:5667 VFA.ADT StringListETableAbs table def
binder 5639:5639 <> t:28
R5675:5697 VFA.ADT StringListETableAbs key def
binder 5671:5671 <> k:29
R5730:5734 Coq.Init.Logic <> ::type_scope:x_'->'_x not
R5702:5727 VFA.ADT StringListETableAbs rep_ok prfax
R5729:5729 VFA.ADTTest <> t:28 var
R5817:5819 Coq.Init.Logic <> ::type_scope:x_'='_x not
R5736:5743 VFA.ADT <> map_find def
R5745:5755 VFA.ADT StringVal V def
R5757:5783 VFA.ADT StringListETableAbs default def
R5785:5785 VFA.ADTTest <> k:29 var
R5791:5813 VFA.ADT StringListETableAbs Abs prfax
R5815:5815 VFA.ADTTest <> t:28 var
R5820:5842 VFA.ADT StringListETableAbs get prfax
R5844:5844 VFA.ADTTest <> k:29 var
R5846:5846 VFA.ADTTest <> t:28 var
R5594:5626 VFA.ADT StringListETableAbs lookup_relate prfax
R5643:5667 VFA.ADT StringListETableAbs table def
binder 5639:5639 <> t:30
R5675:5697 VFA.ADT StringListETableAbs key def
binder 5671:5671 <> k:31
R5730:5734 Coq.Init.Logic <> ::type_scope:x_'->'_x not
R5702:5727 VFA.ADT StringListETableAbs rep_ok prfax
R5729:5729 VFA.ADTTest <> t:30 var
R5817:5819 Coq.Init.Logic <> ::type_scope:x_'='_x not
R5736:5743 VFA.ADT <> map_find def
R5745:5755 VFA.ADT StringVal V def
R5757:5783 VFA.ADT StringListETableAbs default def
R5785:5785 VFA.ADTTest <> k:31 var
R5791:5813 VFA.ADT StringListETableAbs Abs prfax
R5815:5815 VFA.ADTTest <> t:30 var
R5820:5842 VFA.ADT StringListETableAbs get prfax
R5844:5844 VFA.ADTTest <> k:31 var
R5846:5846 VFA.ADTTest <> t:30 var
R5898:5930 VFA.ADT StringListETableAbs lookup_relate prfax
def 5933:5941 <> Unnamed_thm
R5938:5941 Coq.Init.Logic <> True ind
R6044:6076 VFA.ADT StringListETableAbs insert_relate prfax
R6093:6117 VFA.ADT StringListETableAbs table def
binder 6089:6089 <> t:32
R6125:6147 VFA.ADT StringListETableAbs key def
binder 6121:6121 <> k:33
R6158:6178 VFA.ADT StringListETableAbs V def
binder 6154:6154 <> v:34
R6211:6215 Coq.Init.Logic <> ::type_scope:x_'->'_x not
R6183:6208 VFA.ADT StringListETableAbs rep_ok prfax
R6210:6210 VFA.ADTTest <> t:32 var
R6281:6284 Coq.Init.Logic <> ::type_scope:x_'='_x not
R6217:6226 VFA.ADT <> map_update def
R6228:6248 VFA.ADT StringListETableAbs V def
R6250:6250 VFA.ADTTest <> k:33 var
R6252:6252 VFA.ADTTest <> v:34 var
R6255:6277 VFA.ADT StringListETableAbs Abs prfax
R6279:6279 VFA.ADTTest <> t:32 var
R6285:6307 VFA.ADT StringListETableAbs Abs prfax
R6310:6332 VFA.ADT StringListETableAbs set prfax
R6334:6334 VFA.ADTTest <> k:33 var
R6336:6336 VFA.ADTTest <> v:34 var
R6338:6338 VFA.ADTTest <> t:32 var
R6044:6076 VFA.ADT StringListETableAbs insert_relate prfax
R6093:6117 VFA.ADT StringListETableAbs table def
binder 6089:6089 <> t:35
R6125:6147 VFA.ADT StringListETableAbs key def
binder 6121:6121 <> k:36
R6158:6178 VFA.ADT StringListETableAbs V def
binder 6154:6154 <> v:37
R6211:6215 Coq.Init.Logic <> ::type_scope:x_'->'_x not
R6183:6208 VFA.ADT StringListETableAbs rep_ok prfax
R6210:6210 VFA.ADTTest <> t:35 var
R6281:6284 Coq.Init.Logic <> ::type_scope:x_'='_x not
R6217:6226 VFA.ADT <> map_update def
R6228:6248 VFA.ADT StringListETableAbs V def
R6250:6250 VFA.ADTTest <> k:36 var
R6252:6252 VFA.ADTTest <> v:37 var
R6255:6277 VFA.ADT StringListETableAbs Abs prfax
R6279:6279 VFA.ADTTest <> t:35 var
R6285:6307 VFA.ADT StringListETableAbs Abs prfax
R6310:6332 VFA.ADT StringListETableAbs set prfax
R6334:6334 VFA.ADTTest <> k:36 var
R6336:6336 VFA.ADTTest <> v:37 var
R6338:6338 VFA.ADTTest <> t:35 var
R6391:6423 VFA.ADT StringListETableAbs insert_relate prfax
def 6426:6434 <> Unnamed_thm
R6431:6434 Coq.Init.Logic <> True ind
R6537:6571 VFA.ADT StringListETableAbs elements_relate prfax
R6587:6611 VFA.ADT StringListETableAbs table def
binder 6583:6583 <> t:38
R6643:6647 Coq.Init.Logic <> ::type_scope:x_'->'_x not
R6615:6640 VFA.ADT StringListETableAbs rep_ok prfax
R6642:6642 VFA.ADTTest <> t:38 var
R6673:6676 Coq.Init.Logic <> ::type_scope:x_'='_x not
R6648:6670 VFA.ADT StringListETableAbs Abs prfax
R6672:6672 VFA.ADTTest <> t:38 var
R6678:6699 VFA.SearchTree <> map_of_list def
R6701:6721 VFA.ADT StringListETableAbs V def
R6727:6754 VFA.ADT StringListETableAbs elements prfax
R6756:6756 VFA.ADTTest <> t:38 var
R6537:6571 VFA.ADT StringListETableAbs elements_relate prfax
R6587:6611 VFA.ADT StringListETableAbs table def
binder 6583:6583 <> t:39
R6643:6647 Coq.Init.Logic <> ::type_scope:x_'->'_x not
R6615:6640 VFA.ADT StringListETableAbs rep_ok prfax
R6642:6642 VFA.ADTTest <> t:39 var
R6673:6676 Coq.Init.Logic <> ::type_scope:x_'='_x not
R6648:6670 VFA.ADT StringListETableAbs Abs prfax
R6672:6672 VFA.ADTTest <> t:39 var
R6678:6699 VFA.SearchTree <> map_of_list def
R6701:6721 VFA.ADT StringListETableAbs V def
R6727:6754 VFA.ADT StringListETableAbs elements prfax
R6756:6756 VFA.ADTTest <> t:39 var
R6809:6843 VFA.ADT StringListETableAbs elements_relate prfax
def 6846:6854 <> Unnamed_thm
R6851:6854 Coq.Init.Logic <> True ind
R7023:7046 VFA.ADT ListQueue is_empty_empty prfax
R7084:7086 Coq.Init.Logic <> ::type_scope:x_'='_x not
R7050:7067 VFA.ADT ListQueue is_empty prfax
R7069:7083 VFA.ADT ListQueue empty prfax
R7087:7090 Coq.Init.Datatypes <> true constr
R7023:7046 VFA.ADT ListQueue is_empty_empty prfax
R7084:7086 Coq.Init.Logic <> ::type_scope:x_'='_x not
R7050:7067 VFA.ADT ListQueue is_empty prfax
R7069:7083 VFA.ADT ListQueue empty prfax
R7087:7090 Coq.Init.Datatypes <> true constr
R7142:7165 VFA.ADT ListQueue is_empty_empty prfax
def 7168:7176 <> Unnamed_thm
R7173:7176 Coq.Init.Logic <> True ind
R7273:7299 VFA.ADT ListQueue is_empty_nonempty prfax
R7316:7330 VFA.ADT ListQueue queue def
binder 7312:7312 <> q:40
R7338:7348 VFA.ADT ListQueue V def
binder 7334:7334 <> v:41
R7391:7393 Coq.Init.Logic <> ::type_scope:x_'='_x not
R7353:7370 VFA.ADT ListQueue is_empty prfax
R7373:7385 VFA.ADT ListQueue enq prfax
R7387:7387 VFA.ADTTest <> q:40 var
R7389:7389 VFA.ADTTest <> v:41 var
R7394:7398 Coq.Init.Datatypes <> false constr
R7273:7299 VFA.ADT ListQueue is_empty_nonempty prfax
R7316:7330 VFA.ADT ListQueue queue def
binder 7312:7312 <> q:42
R7338:7348 VFA.ADT ListQueue V def
binder 7334:7334 <> v:43
R7391:7393 Coq.Init.Logic <> ::type_scope:x_'='_x not
R7353:7370 VFA.ADT ListQueue is_empty prfax
R7373:7385 VFA.ADT ListQueue enq prfax
R7387:7387 VFA.ADTTest <> q:42 var
R7389:7389 VFA.ADTTest <> v:43 var
R7394:7398 Coq.Init.Datatypes <> false constr
R7450:7476 VFA.ADT ListQueue is_empty_nonempty prfax
def 7479:7487 <> Unnamed_thm
R7484:7487 Coq.Init.Logic <> True ind
R7577:7596 VFA.ADT ListQueue peek_empty prfax
R7612:7622 VFA.ADT ListQueue V def
binder 7608:7608 <> d:44
R7657:7659 Coq.Init.Logic <> ::type_scope:x_'='_x not
R7625:7638 VFA.ADT ListQueue peek prfax
R7640:7640 VFA.ADTTest <> d:44 var
R7642:7656 VFA.ADT ListQueue empty prfax
R7660:7660 VFA.ADTTest <> d:44 var
R7577:7596 VFA.ADT ListQueue peek_empty prfax
R7612:7622 VFA.ADT ListQueue V def
binder 7608:7608 <> d:45
R7657:7659 Coq.Init.Logic <> ::type_scope:x_'='_x not
R7625:7638 VFA.ADT ListQueue peek prfax
R7640:7640 VFA.ADTTest <> d:45 var
R7642:7656 VFA.ADT ListQueue empty prfax
R7660:7660 VFA.ADTTest <> d:45 var
R7712:7731 VFA.ADT ListQueue peek_empty prfax
def 7734:7742 <> Unnamed_thm
R7739:7742 Coq.Init.Logic <> True ind
R7835:7857 VFA.ADT ListQueue peek_nonempty prfax
R7874:7884 VFA.ADT ListQueue V def
binder 7870:7870 <> d:46
R7892:7906 VFA.ADT ListQueue queue def
binder 7888:7888 <> q:47
R7914:7924 VFA.ADT ListQueue V def
binder 7910:7910 <> v:48
R7965:7967 Coq.Init.Logic <> ::type_scope:x_'='_x not
R7929:7942 VFA.ADT ListQueue peek prfax
R7944:7944 VFA.ADTTest <> d:46 var
R7947:7959 VFA.ADT ListQueue enq prfax
R7961:7961 VFA.ADTTest <> q:47 var
R7963:7963 VFA.ADTTest <> v:48 var
R7968:7981 VFA.ADT ListQueue peek prfax
R7983:7983 VFA.ADTTest <> v:48 var
R7985:7985 VFA.ADTTest <> q:47 var
R7835:7857 VFA.ADT ListQueue peek_nonempty prfax
R7874:7884 VFA.ADT ListQueue V def
binder 7870:7870 <> d:49
R7892:7906 VFA.ADT ListQueue queue def
binder 7888:7888 <> q:50
R7914:7924 VFA.ADT ListQueue V def
binder 7910:7910 <> v:51
R7965:7967 Coq.Init.Logic <> ::type_scope:x_'='_x not
R7929:7942 VFA.ADT ListQueue peek prfax
R7944:7944 VFA.ADTTest <> d:49 var
R7947:7959 VFA.ADT ListQueue enq prfax
R7961:7961 VFA.ADTTest <> q:50 var
R7963:7963 VFA.ADTTest <> v:51 var
R7968:7981 VFA.ADT ListQueue peek prfax
R7983:7983 VFA.ADTTest <> v:51 var
R7985:7985 VFA.ADTTest <> q:50 var
R8037:8059 VFA.ADT ListQueue peek_nonempty prfax
def 8062:8070 <> Unnamed_thm
R8067:8070 Coq.Init.Logic <> True ind
R8159:8177 VFA.ADT ListQueue deq_empty prfax
R8210:8212 Coq.Init.Logic <> ::type_scope:x_'='_x not
R8181:8193 VFA.ADT ListQueue deq prfax
R8195:8209 VFA.ADT ListQueue empty prfax
R8213:8227 VFA.ADT ListQueue empty prfax
R8159:8177 VFA.ADT ListQueue deq_empty prfax
R8210:8212 Coq.Init.Logic <> ::type_scope:x_'='_x not
R8181:8193 VFA.ADT ListQueue deq prfax
R8195:8209 VFA.ADT ListQueue empty prfax
R8213:8227 VFA.ADT ListQueue empty prfax
R8279:8297 VFA.ADT ListQueue deq_empty prfax
def 8300:8308 <> Unnamed_thm
R8305:8308 Coq.Init.Logic <> True ind
R8400:8421 VFA.ADT ListQueue deq_nonempty prfax
R8438:8452 VFA.ADT ListQueue queue def
binder 8434:8434 <> q:52
R8460:8470 VFA.ADT ListQueue V def
binder 8456:8456 <> v:53
R8508:8512 Coq.Init.Logic <> ::type_scope:x_'='_x not
R8582:8582 Coq.Init.Logic <> ::type_scope:x_'='_x not
R8475:8487 VFA.ADT ListQueue deq prfax
R8490:8502 VFA.ADT ListQueue enq prfax
R8504:8504 VFA.ADTTest <> q:52 var
R8506:8506 VFA.ADTTest <> v:53 var
R8516:8533 VFA.ADT ListQueue is_empty prfax
R8535:8535 VFA.ADTTest <> q:52 var
R8549:8561 VFA.ADT ListQueue enq prfax
R8564:8576 VFA.ADT ListQueue deq prfax
R8578:8578 VFA.ADTTest <> q:52 var
R8581:8581 VFA.ADTTest <> v:53 var
R8542:8542 VFA.ADTTest <> q:52 var
R8400:8421 VFA.ADT ListQueue deq_nonempty prfax
R8438:8452 VFA.ADT ListQueue queue def
binder 8434:8434 <> q:54
R8460:8470 VFA.ADT ListQueue V def
binder 8456:8456 <> v:55
R8508:8512 Coq.Init.Logic <> ::type_scope:x_'='_x not
R8582:8582 Coq.Init.Logic <> ::type_scope:x_'='_x not
R8475:8487 VFA.ADT ListQueue deq prfax
R8490:8502 VFA.ADT ListQueue enq prfax
R8504:8504 VFA.ADTTest <> q:54 var
R8506:8506 VFA.ADTTest <> v:55 var
R8516:8533 VFA.ADT ListQueue is_empty prfax
R8535:8535 VFA.ADTTest <> q:54 var
R8549:8561 VFA.ADT ListQueue enq prfax
R8564:8576 VFA.ADT ListQueue deq prfax
R8578:8578 VFA.ADTTest <> q:54 var
R8581:8581 VFA.ADTTest <> v:55 var
R8542:8542 VFA.ADTTest <> q:54 var
R8634:8655 VFA.ADT ListQueue deq_nonempty prfax
def 8658:8666 <> Unnamed_thm
R8663:8666 Coq.Init.Logic <> True ind
R8843:8870 VFA.ADT TwoListQueueAbs empty_relate prfax
R8916:8918 Coq.Init.Logic <> ::type_scope:x_'='_x not
R8875:8893 VFA.ADT TwoListQueueAbs Abs def
R8895:8915 VFA.ADT TwoListQueueAbs empty def
R8920:8922 Coq.Init.Datatypes <> nil constr
R8924:8940 VFA.ADT TwoListQueueAbs V def
R8843:8870 VFA.ADT TwoListQueueAbs empty_relate prfax
R8916:8918 Coq.Init.Logic <> ::type_scope:x_'='_x not
R8875:8893 VFA.ADT TwoListQueueAbs Abs def
R8895:8915 VFA.ADT TwoListQueueAbs empty def
R8920:8922 Coq.Init.Datatypes <> nil constr
R8924:8940 VFA.ADT TwoListQueueAbs V def
R8992:9019 VFA.ADT TwoListQueueAbs empty_relate prfax
def 9022:9030 <> Unnamed_thm
R9027:9030 Coq.Init.Logic <> True ind
R9126:9151 VFA.ADT TwoListQueueAbs enq_relate prfax
R9168:9188 VFA.ADT TwoListQueueAbs queue def
binder 9164:9164 <> q:56
R9196:9212 VFA.ADT TwoListQueueAbs V def
binder 9192:9192 <> v:57
R9262:9265 Coq.Init.Logic <> ::type_scope:x_'='_x not
R9217:9235 VFA.ADT TwoListQueueAbs Abs def
R9238:9256 VFA.ADT TwoListQueueAbs enq def
R9258:9258 VFA.ADTTest <> q:56 var
R9260:9260 VFA.ADTTest <> v:57 var
R9288:9291 Coq.Init.Datatypes <> ::list_scope:x_'++'_x not
R9267:9285 VFA.ADT TwoListQueueAbs Abs def
R9287:9287 VFA.ADTTest <> q:56 var
R9293:9296 Coq.Init.Datatypes <> ::list_scope:x_'::'_x not
R9292:9292 VFA.ADTTest <> v:57 var
R9298:9300 Coq.Init.Datatypes <> nil constr
R9302:9318 VFA.ADT TwoListQueueAbs V def
R9126:9151 VFA.ADT TwoListQueueAbs enq_relate prfax
R9168:9188 VFA.ADT TwoListQueueAbs queue def
binder 9164:9164 <> q:58
R9196:9212 VFA.ADT TwoListQueueAbs V def
binder 9192:9192 <> v:59
R9262:9265 Coq.Init.Logic <> ::type_scope:x_'='_x not
R9217:9235 VFA.ADT TwoListQueueAbs Abs def
R9238:9256 VFA.ADT TwoListQueueAbs enq def
R9258:9258 VFA.ADTTest <> q:58 var
R9260:9260 VFA.ADTTest <> v:59 var
R9288:9291 Coq.Init.Datatypes <> ::list_scope:x_'++'_x not
R9267:9285 VFA.ADT TwoListQueueAbs Abs def
R9287:9287 VFA.ADTTest <> q:58 var
R9293:9296 Coq.Init.Datatypes <> ::list_scope:x_'::'_x not
R9292:9292 VFA.ADTTest <> v:59 var
R9298:9300 Coq.Init.Datatypes <> nil constr
R9302:9318 VFA.ADT TwoListQueueAbs V def
R9376:9401 VFA.ADT TwoListQueueAbs enq_relate prfax
def 9404:9412 <> Unnamed_thm
R9409:9412 Coq.Init.Logic <> True ind
R9507:9533 VFA.ADT TwoListQueueAbs peek_relate prfax
R9550:9566 VFA.ADT TwoListQueueAbs V def
binder 9546:9546 <> d:60
R9574:9594 VFA.ADT TwoListQueueAbs queue def
binder 9570:9570 <> q:61
R9623:9626 Coq.Init.Logic <> ::type_scope:x_'='_x not
R9599:9618 VFA.ADT TwoListQueueAbs peek def
R9620:9620 VFA.ADTTest <> d:60 var
R9622:9622 VFA.ADTTest <> q:61 var
R9628:9634 Coq.Lists.List <> hd def
R9636:9652 VFA.ADT TwoListQueueAbs V def
R9654:9654 VFA.ADTTest <> d:60 var
R9657:9675 VFA.ADT TwoListQueueAbs Abs def
R9677:9677 VFA.ADTTest <> q:61 var
R9507:9533 VFA.ADT TwoListQueueAbs peek_relate prfax
R9550:9566 VFA.ADT TwoListQueueAbs V def
binder 9546:9546 <> d:62
R9574:9594 VFA.ADT TwoListQueueAbs queue def
binder 9570:9570 <> q:63
R9623:9626 Coq.Init.Logic <> ::type_scope:x_'='_x not
R9599:9618 VFA.ADT TwoListQueueAbs peek def
R9620:9620 VFA.ADTTest <> d:62 var
R9622:9622 VFA.ADTTest <> q:63 var
R9628:9634 Coq.Lists.List <> hd def
R9636:9652 VFA.ADT TwoListQueueAbs V def
R9654:9654 VFA.ADTTest <> d:62 var
R9657:9675 VFA.ADT TwoListQueueAbs Abs def
R9677:9677 VFA.ADTTest <> q:63 var
R9730:9756 VFA.ADT TwoListQueueAbs peek_relate prfax
def 9759:9767 <> Unnamed_thm
R9764:9767 Coq.Init.Logic <> True ind
R9861:9886 VFA.ADT TwoListQueueAbs deq_relate prfax
R9902:9922 VFA.ADT TwoListQueueAbs queue def
binder 9898:9898 <> q:64
R9969:9972 Coq.Init.Logic <> ::type_scope:x_'='_x not
R9926:9944 VFA.ADT TwoListQueueAbs Abs def
R9947:9965 VFA.ADT TwoListQueueAbs deq def
R9967:9967 VFA.ADTTest <> q:64 var
R9974:9980 Coq.Lists.List <> tl def
R9982:9998 VFA.ADT TwoListQueueAbs V def
R10001:10019 VFA.ADT TwoListQueueAbs Abs def
R10021:10021 VFA.ADTTest <> q:64 var
R9861:9886 VFA.ADT TwoListQueueAbs deq_relate prfax
R9902:9922 VFA.ADT TwoListQueueAbs queue def
binder 9898:9898 <> q:65
R9969:9972 Coq.Init.Logic <> ::type_scope:x_'='_x not
R9926:9944 VFA.ADT TwoListQueueAbs Abs def
R9947:9965 VFA.ADT TwoListQueueAbs deq def
R9967:9967 VFA.ADTTest <> q:65 var
R9974:9980 Coq.Lists.List <> tl def
R9982:9998 VFA.ADT TwoListQueueAbs V def
R10001:10019 VFA.ADT TwoListQueueAbs Abs def
R10021:10021 VFA.ADTTest <> q:65 var
R10074:10099 VFA.ADT TwoListQueueAbs deq_relate prfax
def 10102:10110 <> Unnamed_thm
R10107:10110 Coq.Init.Logic <> True ind
R10259:10266 VFA.ADT <> a_vector prfax
R10270:10275 VFA.ADT <> vector def
R10277:10279 Coq.Init.Datatypes <> nat ind
R10259:10266 VFA.ADT <> a_vector prfax
R10270:10275 VFA.ADT <> vector def
R10277:10279 Coq.Init.Datatypes <> nat ind
R10331:10338 VFA.ADT <> a_vector prfax
def 10341:10349 <> Unnamed_thm
R10346:10349 Coq.Init.Logic <> True ind
R10520:10538 VFA.ADT <> vector_cons_correct prfax
binder 10551:10551 <> X:66
R10566:10566 VFA.ADTTest <> X:66 var
binder 10562:10562 <> x:67
R10574:10579 VFA.ADT <> vector def
R10581:10581 VFA.ADTTest <> X:66 var
binder 10570:10570 <> v:68
R10624:10626 Coq.Init.Logic <> ::type_scope:x_'='_x not
R10587:10600 VFA.ADT <> list_of_vector def
R10602:10602 VFA.ADTTest <> X:66 var
R10606:10616 VFA.ADT <> vector_cons prfax
R10618:10618 VFA.ADTTest <> X:66 var
R10620:10620 VFA.ADTTest <> x:67 var
R10622:10622 VFA.ADTTest <> v:68 var
R10629:10632 Coq.Init.Datatypes <> ::list_scope:x_'::'_x not
R10628:10628 VFA.ADTTest <> x:67 var
R10634:10647 VFA.ADT <> list_of_vector def
R10649:10649 VFA.ADTTest <> X:66 var
R10651:10651 VFA.ADTTest <> v:68 var
R10520:10538 VFA.ADT <> vector_cons_correct prfax
binder 10551:10551 <> X:69
R10566:10566 VFA.ADTTest <> X:69 var
binder 10562:10562 <> x:70
R10574:10579 VFA.ADT <> vector def
R10581:10581 VFA.ADTTest <> X:69 var
binder 10570:10570 <> v:71
R10624:10626 Coq.Init.Logic <> ::type_scope:x_'='_x not
R10587:10600 VFA.ADT <> list_of_vector def
R10602:10602 VFA.ADTTest <> X:69 var
R10606:10616 VFA.ADT <> vector_cons prfax
R10618:10618 VFA.ADTTest <> X:69 var
R10620:10620 VFA.ADTTest <> x:70 var
R10622:10622 VFA.ADTTest <> v:71 var
R10629:10632 Coq.Init.Datatypes <> ::list_scope:x_'::'_x not
R10628:10628 VFA.ADTTest <> x:70 var
R10634:10647 VFA.ADT <> list_of_vector def
R10649:10649 VFA.ADTTest <> X:69 var
R10651:10651 VFA.ADTTest <> v:71 var
R10709:10727 VFA.ADT <> vector_cons_correct prfax
def 10730:10738 <> Unnamed_thm
R10735:10738 Coq.Init.Logic <> True ind
R10907:10924 VFA.ADT <> vector_app_correct prfax
binder 10937:10937 <> X:72
R10956:10961 VFA.ADT <> vector def
R10963:10963 VFA.ADTTest <> X:72 var
binder 10948:10949 <> v1:73
binder 10951:10952 <> v2:74
R11007:11010 Coq.Init.Logic <> ::type_scope:x_'='_x not
R10969:10982 VFA.ADT <> list_of_vector def
R10984:10984 VFA.ADTTest <> X:72 var
R10988:10997 VFA.ADT <> vector_app prfax
R10999:10999 VFA.ADTTest <> X:72 var
R11001:11002 VFA.ADTTest <> v1:73 var
R11004:11005 VFA.ADTTest <> v2:74 var
R11032:11035 Coq.Init.Datatypes <> ::list_scope:x_'++'_x not
R11013:11026 VFA.ADT <> list_of_vector def
R11028:11028 VFA.ADTTest <> X:72 var
R11030:11031 VFA.ADTTest <> v1:73 var
R11037:11050 VFA.ADT <> list_of_vector def
R11052:11052 VFA.ADTTest <> X:72 var
R11054:11055 VFA.ADTTest <> v2:74 var
R10907:10924 VFA.ADT <> vector_app_correct prfax
binder 10937:10937 <> X:75
R10956:10961 VFA.ADT <> vector def
R10963:10963 VFA.ADTTest <> X:75 var
binder 10948:10949 <> v1:76
binder 10951:10952 <> v2:77
R11007:11010 Coq.Init.Logic <> ::type_scope:x_'='_x not
R10969:10982 VFA.ADT <> list_of_vector def
R10984:10984 VFA.ADTTest <> X:75 var
R10988:10997 VFA.ADT <> vector_app prfax
R10999:10999 VFA.ADTTest <> X:75 var
R11001:11002 VFA.ADTTest <> v1:76 var
R11004:11005 VFA.ADTTest <> v2:77 var
R11032:11035 Coq.Init.Datatypes <> ::list_scope:x_'++'_x not
R11013:11026 VFA.ADT <> list_of_vector def
R11028:11028 VFA.ADTTest <> X:75 var
R11030:11031 VFA.ADTTest <> v1:76 var
R11037:11050 VFA.ADT <> list_of_vector def
R11052:11052 VFA.ADTTest <> X:75 var
R11054:11055 VFA.ADTTest <> v2:77 var
R11113:11130 VFA.ADT <> vector_app_correct prfax
def 11133:11141 <> Unnamed_thm
R11138:11141 Coq.Init.Logic <> True ind
R11338:11365 VFA.ADT <> manual_grade_for_ListsETable def
R12564:12622 VFA.ADT StringListsTableExamples.StringListsTable get_empty_default prfax
R12728:12781 VFA.ADT StringListsTableExamples.StringListsTable get_set_same prfax
R12888:12942 VFA.ADT StringListsTableExamples.StringListsTable get_set_other prfax
R13022:13049 VFA.ADT StringListsTableExamples ex1 prfax
R13129:13156 VFA.ADT StringListsTableExamples ex2 prfax
R13236:13263 VFA.ADT StringListsTableExamples ex3 prfax
R13343:13370 VFA.ADT StringListETableAbs empty_ok prfax
R13448:13473 VFA.ADT StringListETableAbs set_ok prfax
R13557:13588 VFA.ADT StringListETableAbs empty_relate prfax
R13672:13703 VFA.ADT StringListETableAbs bound_relate prfax
R13788:13820 VFA.ADT StringListETableAbs lookup_relate prfax
R13905:13937 VFA.ADT StringListETableAbs insert_relate prfax
R14024:14058 VFA.ADT StringListETableAbs elements_relate prfax
R14134:14157 VFA.ADT ListQueue is_empty_empty prfax
R14236:14262 VFA.ADT ListQueue is_empty_nonempty prfax
R14334:14353 VFA.ADT ListQueue peek_empty prfax
R14428:14450 VFA.ADT ListQueue peek_nonempty prfax
R14521:14539 VFA.ADT ListQueue deq_empty prfax
R14613:14634 VFA.ADT ListQueue deq_nonempty prfax
R14714:14741 VFA.ADT TwoListQueueAbs empty_relate prfax
R14819:14844 VFA.ADT TwoListQueueAbs enq_relate prfax
R14923:14949 VFA.ADT TwoListQueueAbs peek_relate prfax
R15027:15052 VFA.ADT TwoListQueueAbs deq_relate prfax
R15112:15119 VFA.ADT <> a_vector prfax
R15190:15208 VFA.ADT <> vector_cons_correct prfax
R15278:15295 VFA.ADT <> vector_app_correct prfax