-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy path.BVList.aux
1307 lines (1307 loc) · 42.7 KB
/
.BVList.aux
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
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
COQAUX1 25453fbf55a225cb7dbf666ad4d44259 /home/sec/Desktop/bitvectors/BVList.v
1494 1559 context_used ""
1614 1620 VernacProof "tac:no using:no"
1634 1638 proof_build_time "0.096"
0 0 inj "0.096"
1634 1638 context_used ""
1634 1638 proof_check_time "0.014"
1642 1881 context_used ""
1909 1941 context_used ""
1944 2001 context_used ""
2004 2085 context_used ""
2088 2147 context_used ""
2169 2213 context_used ""
2232 2299 context_used ""
2327 2409 context_used ""
2412 2486 context_used ""
2489 2563 context_used ""
2566 2640 context_used ""
2643 2717 context_used ""
2720 2794 context_used ""
2797 2871 context_used ""
2874 2941 context_used ""
2944 3011 context_used ""
3015 3082 context_used ""
3085 3152 context_used ""
3156 3230 context_used ""
3233 3307 context_used ""
3336 3399 context_used ""
3402 3465 context_used ""
3468 3541 context_used ""
3655 3727 context_used ""
3730 3802 context_used ""
3929 4013 context_used ""
4016 4093 context_used ""
4096 4161 context_used ""
4165 4249 context_used ""
4252 4336 context_used ""
4339 4417 context_used ""
4420 4498 context_used ""
4501 4573 context_used ""
4576 4648 context_used ""
4652 4741 context_used ""
4744 4831 context_used ""
4834 4923 context_used ""
4928 5042 context_used ""
5045 5155 context_used ""
5158 5272 context_used ""
5275 5389 context_used ""
5392 5479 context_used ""
5483 5548 context_used ""
5593 5621 context_used ""
5622 5660 context_used ""
5661 5707 context_used ""
5708 5754 context_used ""
5755 5806 context_used ""
5807 5855 context_used ""
5873 5911 context_used ""
5926 5980 context_used ""
6004 6063 context_used ""
6064 6123 context_used ""
6124 6183 context_used ""
6184 6243 context_used ""
6244 6303 context_used ""
6304 6363 context_used ""
6364 6423 context_used ""
6424 6478 context_used ""
6479 6533 context_used ""
6535 6589 context_used ""
6590 6644 context_used ""
6646 6705 context_used ""
6706 6765 context_used ""
6788 6834 context_used ""
6835 6881 context_used ""
6882 6949 context_used ""
7048 7111 context_used ""
7112 7175 context_used ""
7223 7300 context_used ""
7301 7378 context_used ""
7379 7439 context_used ""
7440 7492 context_used ""
7493 7589 context_used ""
7590 7677 context_used ""
7678 7764 context_used ""
7765 7852 context_used ""
7853 7940 context_used ""
7941 8029 context_used ""
8030 8118 context_used ""
8119 8188 context_used ""
8189 8258 context_used ""
8259 8346 context_used ""
8347 8434 context_used ""
8436 8523 context_used ""
8660 8752 context_used ""
8753 8845 context_used ""
8867 8929 context_used ""
8930 8980 context_used ""
8983 9046 context_used ""
9047 9110 context_used ""
9111 9168 context_used ""
9169 9226 context_used ""
9227 9296 context_used ""
9297 9366 context_used ""
9369 9458 context_used ""
9459 9546 context_used ""
9547 9636 context_used ""
9638 9806 context_used ""
9807 9971 context_used ""
9972 10140 context_used ""
10141 10309 context_used ""
10310 10367 context_used ""
10443 10555 context_used ""
10443 10555 context_used ""
10558 10593 context_used ""
10597 10645 context_used ""
10723 10729 VernacProof "tac:no using:no"
10771 10775 proof_build_time "0.003"
0 0 of_bits_size "0.003"
10771 10775 context_used ""
10771 10775 proof_check_time "0.001"
10835 10841 VernacProof "tac:no using:no"
10871 10875 proof_build_time "0.001"
0 0 _of_bits_size "0.001"
10871 10875 context_used ""
10871 10875 proof_check_time "0.014"
10880 11005 context_used ""
11009 11122 context_used ""
11126 11187 context_used ""
11191 11279 context_used ""
11283 11343 context_used ""
11347 11411 context_used ""
11415 11479 context_used ""
11483 11614 context_used ""
11618 11746 context_used ""
11750 11881 context_used ""
11885 12019 context_used ""
12023 12157 context_used ""
12161 12292 context_used ""
12296 12365 context_used ""
12369 12438 context_used ""
12442 12557 context_used ""
12561 12676 context_used ""
12680 12849 context_used ""
12853 13007 context_used ""
13217 13372 context_used ""
13376 13531 context_used ""
13535 13666 context_used ""
13670 13801 context_used ""
13880 13886 VernacProof "tac:no using:no"
13929 13933 proof_build_time "0.016"
0 0 bits_size "0.016"
13929 13933 context_used ""
13929 13933 proof_check_time "0.001"
14081 14087 VernacProof "tac:no using:no"
14348 14352 proof_build_time "0.100"
0 0 bv_eq_reflect "0.100"
14348 14352 context_used ""
14348 14352 proof_check_time "0.015"
14415 14421 VernacProof "tac:no using:no"
14471 14475 proof_build_time "0.003"
0 0 bv_eq_refl "0.003"
14471 14475 context_used ""
14471 14475 proof_check_time "0.003"
14555 14561 VernacProof "tac:no using:no"
14735 14739 proof_build_time "0.023"
0 0 bv_ult_not_eqP "0.023"
14735 14739 context_used ""
14735 14739 proof_check_time "0.012"
14819 14825 VernacProof "tac:no using:no"
14999 15003 proof_build_time "0.050"
0 0 bv_slt_not_eqP "0.050"
14999 15003 context_used ""
14999 15003 proof_check_time "0.001"
15088 15094 VernacProof "tac:no using:no"
15258 15262 proof_build_time "0.025"
0 0 bv_ult_not_eq "0.025"
15258 15262 context_used ""
15258 15262 proof_check_time "0.019"
15347 15353 VernacProof "tac:no using:no"
15517 15521 proof_build_time "0.021"
0 0 bv_slt_not_eq "0.021"
15517 15521 context_used ""
15517 15521 proof_check_time "0.002"
15609 15615 VernacProof "tac:no using:no"
15702 15706 proof_build_time "0.431"
0 0 bv_ult_B2P "0.431"
15702 15706 context_used ""
15702 15706 proof_check_time "0.001"
15795 15801 VernacProof "tac:no using:no"
15888 15892 proof_build_time "0.003"
0 0 bv_slt_B2P "0.003"
15888 15892 context_used ""
15888 15892 proof_check_time "0.001"
15978 15984 VernacProof "tac:no using:no"
16072 16076 proof_build_time "0.006"
0 0 bv_and_comm "0.006"
16072 16076 context_used ""
16072 16076 proof_check_time "0.001"
16159 16165 VernacProof "tac:no using:no"
16252 16256 proof_build_time "0.004"
0 0 bv_or_comm "0.004"
16252 16256 context_used ""
16252 16256 proof_check_time "0.001"
16342 16348 VernacProof "tac:no using:no"
16436 16440 proof_build_time "0.004"
0 0 bv_add_comm "0.004"
16436 16440 context_used ""
16436 16440 proof_check_time "0.001"
16560 16566 VernacProof "tac:no using:no"
16696 16700 proof_build_time "0.006"
0 0 bv_and_assoc "0.006"
16696 16700 context_used ""
16696 16700 proof_check_time "0.001"
16815 16821 VernacProof "tac:no using:no"
16950 16954 proof_build_time "0.005"
0 0 bv_or_assoc "0.005"
16950 16954 context_used ""
16950 16954 proof_check_time "0.002"
17074 17080 VernacProof "tac:no using:no"
17210 17214 proof_build_time "0.006"
0 0 bv_xor_assoc "0.006"
17210 17214 context_used ""
17210 17214 proof_check_time "0.001"
17334 17340 VernacProof "tac:no using:no"
17470 17474 proof_build_time "0.006"
0 0 bv_add_assoc "0.006"
17470 17474 context_used ""
17470 17474 proof_check_time "0.002"
17568 17574 VernacProof "tac:no using:no"
17705 17709 proof_build_time "0.003"
0 0 bv_not_involutive "0.003"
17705 17709 context_used ""
17705 17709 proof_check_time "0.001"
17775 17809 context_used ""
17810 17857 context_used ""
17858 17916 context_used ""
17917 17967 context_used ""
18034 18040 VernacProof "tac:no using:no"
18082 18086 proof_build_time "0.002"
0 0 bits_size "0.002"
18082 18086 context_used ""
18082 18086 proof_check_time "0.000"
18156 18162 VernacProof "tac:no using:no"
18207 18211 proof_build_time "0.002"
0 0 of_bits_size "0.002"
18207 18211 context_used ""
18207 18211 proof_check_time "0.000"
18213 18391 context_used ""
18393 18506 context_used ""
18508 18681 context_used ""
18737 18743 VernacProof "tac:no using:no"
19248 19252 proof_build_time "0.019"
0 0 bv_mk_eq "0.019"
19248 19252 context_used ""
19248 19252 proof_check_time "0.010"
19253 19313 context_used ""
19991 19997 VernacProof "tac:no using:no"
20218 20222 proof_build_time "0.006"
0 0 foo "0.006"
20218 20222 context_used ""
20218 20222 proof_check_time "0.003"
20872 20936 context_used ""
20938 21093 context_used ""
21095 21248 context_used ""
21250 21405 context_used ""
21407 21474 context_used ""
21519 21854 context_used ""
21914 22161 context_used ""
22163 22227 context_used ""
22229 22367 context_used ""
22389 22482 context_used ""
22486 22554 context_used ""
22556 22617 context_used ""
22619 22784 context_used ""
22786 23194 context_used ""
23196 23454 context_used ""
23456 23526 context_used ""
23528 23687 context_used ""
23706 23993 context_used ""
23995 24085 context_used ""
24088 24375 context_used ""
24377 24465 context_used ""
24468 24567 context_used ""
24570 24669 context_used ""
24671 24751 context_used ""
24753 24833 context_used ""
24835 24936 context_used ""
24938 25039 context_used ""
25064 25331 context_used ""
25333 25629 context_used ""
25633 25788 context_used ""
25790 26254 context_used ""
26256 26445 context_used ""
26447 26789 context_used ""
26791 27000 context_used ""
27002 27057 context_used ""
27059 27185 context_used ""
27271 27277 VernacProof "tac:no using:no"
27386 27390 proof_build_time "0.003"
0 0 length_mk_list_false "0.003"
27386 27390 context_used ""
27386 27390 proof_check_time "0.001"
27392 27487 context_used ""
27541 27547 VernacProof "tac:no using:no"
27761 27765 proof_build_time "0.007"
0 0 _of_bits_size "0.007"
27761 27765 context_used ""
27761 27765 proof_check_time "0.002"
27833 27839 VernacProof "tac:no using:no"
27948 27952 proof_build_time "0.003"
0 0 length_mk_list_true "0.003"
27948 27952 context_used ""
27948 27952 proof_check_time "0.001"
28001 28007 VernacProof "tac:no using:no"
28072 28076 proof_build_time "0.002"
0 0 zeros_size "0.002"
28072 28076 context_used ""
28072 28076 proof_check_time "0.000"
28151 28157 VernacProof "tac:no using:no"
28491 28495 proof_build_time "0.024"
0 0 List_eq "0.024"
28491 28495 context_used ""
28491 28495 proof_check_time "0.008"
28565 28571 VernacProof "tac:no using:no"
28847 28851 proof_build_time "0.062"
0 0 List_eqP "0.062"
28847 28851 context_used ""
28847 28851 proof_check_time "0.006"
28918 28924 VernacProof "tac:no using:no"
29048 29052 proof_build_time "0.004"
0 0 List_eq_refl "0.004"
29048 29052 context_used ""
29048 29052 proof_check_time "0.001"
29125 29131 VernacProof "tac:no using:no"
29249 29253 proof_build_time "0.008"
0 0 List_eqP_refl "0.008"
29249 29253 context_used ""
29249 29253 proof_check_time "0.002"
29329 29335 VernacProof "tac:no using:no"
29942 29946 proof_build_time "0.082"
0 0 List_neq "0.082"
29942 29946 context_used ""
29942 29946 proof_check_time "0.010"
30017 30023 VernacProof "tac:no using:no"
30340 30344 proof_build_time "0.076"
0 0 List_neqP "0.076"
30340 30344 context_used ""
30340 30344 proof_check_time "0.006"
30400 30406 VernacProof "tac:no using:no"
30574 30578 proof_build_time "0.008"
0 0 bv_eq_reflect "0.008"
30574 30578 context_used ""
30574 30578 proof_check_time "0.002"
30618 30624 VernacProof "tac:no using:no"
30681 30685 proof_build_time "0.003"
0 0 bv_eq_refl "0.003"
30681 30685 context_used ""
30681 30685 proof_check_time "0.001"
30780 30786 VernacProof "tac:no using:no"
30896 30900 proof_build_time "0.004"
0 0 bv_concat_size "0.004"
30896 30900 context_used ""
30896 30900 proof_check_time "0.002"
31016 31022 VernacProof "tac:no using:no"
31330 31334 proof_build_time "0.010"
0 0 map2_and_comm "0.010"
31330 31334 context_used ""
31330 31334 proof_check_time "0.003"
31448 31454 VernacProof "tac:no using:no"
31760 31764 proof_build_time "0.013"
0 0 map2_and_assoc "0.013"
31760 31764 context_used ""
31760 31764 proof_check_time "0.004"
31863 31869 VernacProof "tac:no using:no"
32219 32223 proof_build_time "0.013"
0 0 map2_and_idem1 "0.013"
32219 32223 context_used ""
32219 32223 proof_check_time "0.004"
32326 32332 VernacProof "tac:no using:no"
32413 32417 proof_build_time "0.003"
0 0 map2_and_idem_comm "0.003"
32413 32417 context_used ""
32413 32417 proof_check_time "0.001"
32516 32522 VernacProof "tac:no using:no"
32872 32876 proof_build_time "0.013"
0 0 map2_and_idem2 "0.013"
32872 32876 context_used ""
32872 32876 proof_check_time "0.003"
32980 32986 VernacProof "tac:no using:no"
33067 33071 proof_build_time "0.044"
0 0 map2_and_idem_comm2 "0.044"
33067 33071 context_used ""
33067 33071 proof_check_time "0.007"
33149 33155 VernacProof "tac:no using:no"
33211 33215 proof_build_time "0.002"
0 0 map2_and_empty_empty1 "0.002"
33211 33215 context_used ""
33211 33215 proof_check_time "0.005"
33293 33299 VernacProof "tac:no using:no"
33362 33366 proof_build_time "0.002"
0 0 map2_and_empty_empty2 "0.002"
33362 33366 context_used ""
33362 33366 proof_check_time "0.005"
33438 33444 VernacProof "tac:no using:no"
33500 33504 proof_build_time "0.002"
0 0 map2_nth_empty_false "0.002"
33500 33504 context_used ""
33500 33504 proof_check_time "0.001"
33607 33613 VernacProof "tac:no using:no"
33753 33757 proof_build_time "0.011"
0 0 mk_list_true_equiv "0.011"
33753 33757 context_used ""
33753 33757 proof_check_time "0.006"
33863 33869 VernacProof "tac:no using:no"
34010 34014 proof_build_time "0.015"
0 0 mk_list_false_equiv "0.015"
34010 34014 context_used ""
34010 34014 proof_check_time "0.005"
34086 34092 VernacProof "tac:no using:no"
34113 34117 proof_build_time "0.001"
0 0 len_mk_list_true_empty "0.001"
34113 34117 context_used ""
34113 34117 proof_check_time "0.000"
34213 34219 VernacProof "tac:no using:no"
34336 34340 proof_build_time "0.045"
0 0 add_mk_list_true "0.045"
34336 34340 context_used ""
34336 34340 proof_check_time "0.011"
34599 34605 VernacProof "tac:no using:no"
35274 35278 proof_build_time "0.247"
0 0 map2_and_nth_bitOf "0.247"
35274 35278 context_used ""
35274 35278 proof_check_time "0.023"
35358 35364 VernacProof "tac:no using:no"
35414 35418 proof_build_time "0.004"
0 0 length_mk_list_true_full "0.004"
35414 35418 context_used ""
35414 35418 proof_check_time "0.001"
35508 35514 VernacProof "tac:no using:no"
35822 35826 proof_build_time "0.011"
0 0 mk_list_app "0.011"
35822 35826 context_used ""
35822 35826 proof_check_time "0.003"
35914 35920 VernacProof "tac:no using:no"
35963 35967 proof_build_time "0.003"
0 0 mk_list_ltrue "0.003"
35963 35967 context_used ""
35963 35967 proof_check_time "0.001"
36063 36069 VernacProof "tac:no using:no"
36212 36216 proof_build_time "0.007"
0 0 map2_and_1_neutral "0.007"
36212 36216 context_used ""
36212 36216 proof_check_time "0.001"
36337 36343 VernacProof "tac:no using:no"
36488 36492 proof_build_time "0.005"
0 0 map2_and_0_absorb "0.005"
36488 36492 context_used ""
36488 36492 proof_check_time "0.002"
36600 36606 VernacProof "tac:no using:no"
36801 36805 proof_build_time "0.010"
0 0 map2_and_length "0.010"
36801 36805 context_used ""
36801 36805 proof_check_time "0.003"
36914 36920 VernacProof "tac:no using:no"
37130 37134 proof_build_time "0.009"
0 0 bv_and_size "0.009"
37130 37134 context_used ""
37130 37134 proof_check_time "0.003"
37215 37221 VernacProof "tac:no using:no"
37348 37352 proof_build_time "0.014"
0 0 bv_and_comm "0.014"
37348 37352 context_used ""
37348 37352 proof_check_time "0.006"
37518 37524 VernacProof "tac:no using:no"
38016 38020 proof_build_time "0.059"
0 0 bv_and_assoc "0.059"
38016 38020 context_used ""
38016 38020 proof_check_time "0.096"
38125 38131 VernacProof "tac:no using:no"
38463 38467 proof_build_time "0.026"
0 0 bv_and_idem1 "0.026"
38463 38467 context_used ""
38463 38467 proof_check_time "0.010"
38572 38578 VernacProof "tac:no using:no"
38909 38913 proof_build_time "0.017"
0 0 bv_and_idem2 "0.017"
38909 38913 context_used ""
38909 38913 proof_check_time "0.009"
38915 38953 context_used ""
39024 39030 VernacProof "tac:no using:no"
39409 39413 proof_build_time "0.011"
0 0 bv_and_empty_empty1 "0.011"
39409 39413 context_used ""
39409 39413 proof_check_time "0.004"
39691 39697 VernacProof "tac:no using:no"
39948 39952 proof_build_time "0.009"
0 0 bv_and_nth_bitOf "0.009"
39948 39952 context_used ""
39948 39952 proof_check_time "0.004"
40023 40029 VernacProof "tac:no using:no"
40107 40111 proof_build_time "0.003"
0 0 bv_and_empty_empty2 "0.003"
40107 40111 context_used ""
40107 40111 proof_check_time "0.001"
40196 40202 VernacProof "tac:no using:no"
40384 40388 proof_build_time "0.006"
0 0 bv_and_1_neutral "0.006"
40384 40388 context_used ""
40384 40388 proof_check_time "0.002"
40505 40511 VernacProof "tac:no using:no"
40694 40698 proof_build_time "0.006"
0 0 bv_and_0_absorb "0.006"
40694 40698 context_used ""
40694 40698 proof_check_time "0.002"
40813 40819 VernacProof "tac:no using:no"
41126 41130 proof_build_time "0.010"
0 0 map2_or_comm "0.010"
41126 41130 context_used ""
41126 41130 proof_check_time "0.003"
41239 41245 VernacProof "tac:no using:no"
41550 41554 proof_build_time "0.012"
0 0 map2_or_assoc "0.012"
41550 41554 context_used ""
41550 41554 proof_check_time "0.004"
41660 41666 VernacProof "tac:no using:no"
41861 41865 proof_build_time "0.009"
0 0 map2_or_length "0.009"
41861 41865 context_used ""
41861 41865 proof_check_time "0.003"
41941 41947 VernacProof "tac:no using:no"
42003 42007 proof_build_time "0.002"
0 0 map2_or_empty_empty1 "0.002"
42003 42007 context_used ""
42003 42007 proof_check_time "0.001"
42083 42089 VernacProof "tac:no using:no"
42150 42154 proof_build_time "0.004"
0 0 map2_or_empty_empty2 "0.004"
42150 42154 context_used ""
42150 42154 proof_check_time "0.001"
42411 42417 VernacProof "tac:no using:no"
43184 43188 proof_build_time "0.278"
0 0 map2_or_nth_bitOf "0.278"
43184 43188 context_used ""
43184 43188 proof_check_time "0.097"
43283 43289 VernacProof "tac:no using:no"
43432 43436 proof_build_time "0.005"
0 0 map2_or_0_neutral "0.005"
43432 43436 context_used ""
43432 43436 proof_check_time "0.001"
43551 43557 VernacProof "tac:no using:no"
43700 43704 proof_build_time "0.007"
0 0 map2_or_1_true "0.007"
43700 43704 context_used ""
43700 43704 proof_check_time "0.002"
43810 43816 VernacProof "tac:no using:no"
44024 44028 proof_build_time "0.009"
0 0 bv_or_size "0.009"
44024 44028 context_used ""
44024 44028 proof_check_time "0.004"
44117 44123 VernacProof "tac:no using:no"
44270 44274 proof_build_time "0.006"
0 0 bv_or_comm "0.006"
44270 44274 context_used ""
44270 44274 proof_check_time "0.002"
44442 44448 VernacProof "tac:no using:no"
44996 45000 proof_build_time "0.036"
0 0 bv_or_assoc "0.036"
44996 45000 context_used ""
44996 45000 proof_check_time "0.017"
45069 45075 VernacProof "tac:no using:no"
45462 45466 proof_build_time "0.012"
0 0 bv_or_empty_empty1 "0.012"
45462 45466 context_used ""
45462 45466 proof_check_time "0.004"
45742 45748 VernacProof "tac:no using:no"
45997 46001 proof_build_time "0.009"
0 0 bv_or_nth_bitOf "0.009"
45997 46001 context_used ""
45997 46001 proof_check_time "0.004"
46085 46091 VernacProof "tac:no using:no"
46272 46276 proof_build_time "0.006"
0 0 bv_or_0_neutral "0.006"
46272 46276 context_used ""
46272 46276 proof_check_time "0.007"
46387 46393 VernacProof "tac:no using:no"
46571 46575 proof_build_time "0.011"
0 0 bv_or_1_true "0.011"
46571 46575 context_used ""
46571 46575 proof_check_time "0.002"
46694 46700 VernacProof "tac:no using:no"
47012 47016 proof_build_time "0.022"
0 0 map2_xor_comm "0.022"
47012 47016 context_used ""
47012 47016 proof_check_time "0.003"
47130 47136 VernacProof "tac:no using:no"
47479 47483 proof_build_time "0.033"
0 0 map2_xor_assoc "0.033"
47479 47483 context_used ""
47479 47483 proof_check_time "0.008"
47591 47597 VernacProof "tac:no using:no"
47792 47796 proof_build_time "0.019"
0 0 map2_xor_length "0.019"
47792 47796 context_used ""
47792 47796 proof_check_time "0.007"
47874 47880 VernacProof "tac:no using:no"
47936 47940 proof_build_time "0.006"
0 0 map2_xor_empty_empty1 "0.006"
47936 47940 context_used ""
47936 47940 proof_check_time "0.001"
48018 48024 VernacProof "tac:no using:no"
48087 48091 proof_build_time "0.006"
0 0 map2_xor_empty_empty2 "0.006"
48087 48091 context_used ""
48087 48091 proof_check_time "0.000"
48352 48358 VernacProof "tac:no using:no"
49128 49132 proof_build_time "0.435"
0 0 map2_xor_nth_bitOf "0.435"
49128 49132 context_used ""
49128 49132 proof_check_time "0.078"
49229 49235 VernacProof "tac:no using:no"
49379 49383 proof_build_time "0.009"
0 0 map2_xor_0_neutral "0.009"
49379 49383 context_used ""
49379 49383 proof_check_time "0.001"
49485 49491 VernacProof "tac:no using:no"
49652 49656 proof_build_time "0.006"
0 0 map2_xor_1_true "0.006"
49652 49656 context_used ""
49652 49656 proof_check_time "0.007"
49764 49770 VernacProof "tac:no using:no"
49980 49984 proof_build_time "0.020"
0 0 bv_xor_size "0.020"
49980 49984 context_used ""
49980 49984 proof_check_time "0.010"
50076 50082 VernacProof "tac:no using:no"
50231 50235 proof_build_time "0.008"
0 0 bv_xor_comm "0.008"
50231 50235 context_used ""
50231 50235 proof_check_time "0.002"
50408 50414 VernacProof "tac:no using:no"
50966 50970 proof_build_time "0.035"
0 0 bv_xor_assoc "0.035"
50966 50970 context_used ""
50966 50970 proof_check_time "0.016"
51041 51047 VernacProof "tac:no using:no"
51436 51440 proof_build_time "0.012"
0 0 bv_xor_empty_empty1 "0.012"
51436 51440 context_used ""
51436 51440 proof_check_time "0.005"
51720 51726 VernacProof "tac:no using:no"
51977 51981 proof_build_time "0.009"
0 0 bv_xor_nth_bitOf "0.009"
51977 51981 context_used ""
51977 51981 proof_check_time "0.003"
52067 52073 VernacProof "tac:no using:no"
52256 52260 proof_build_time "0.006"
0 0 bv_xor_0_neutral "0.006"
52256 52260 context_used ""
52256 52260 proof_check_time "0.002"
52351 52357 VernacProof "tac:no using:no"
52537 52541 proof_build_time "0.006"
0 0 bv_xor_1_true "0.006"
52537 52541 context_used ""
52537 52541 proof_check_time "0.002"
52636 52642 VernacProof "tac:no using:no"
52749 52753 proof_build_time "0.003"
0 0 not_list_length "0.003"
52749 52753 context_used ""
52749 52753 proof_check_time "0.001"
52821 52827 VernacProof "tac:no using:no"
52947 52951 proof_build_time "0.005"
0 0 not_list_involutative "0.005"
52947 52951 context_used ""
52947 52951 proof_check_time "0.002"
53035 53041 VernacProof "tac:no using:no"
53142 53146 proof_build_time "0.003"
0 0 not_list_false_true "0.003"
53142 53146 context_used ""
53142 53146 proof_check_time "0.001"
53230 53236 VernacProof "tac:no using:no"
53337 53341 proof_build_time "0.003"
0 0 not_list_true_false "0.003"
53337 53341 context_used ""
53337 53341 proof_check_time "0.001"
53441 53447 VernacProof "tac:no using:no"
53618 53622 proof_build_time "0.008"
0 0 not_list_and_or "0.008"
53618 53622 context_used ""
53618 53622 proof_check_time "0.003"
53722 53728 VernacProof "tac:no using:no"
53898 53902 proof_build_time "0.008"
0 0 not_list_or_and "0.008"
53898 53902 context_used ""
53898 53902 proof_check_time "0.003"
54002 54008 VernacProof "tac:no using:no"
54106 54110 proof_build_time "0.011"
0 0 bv_not_size "0.011"
54106 54110 context_used ""
54106 54110 proof_check_time "0.001"
54170 54176 VernacProof "tac:no using:no"
54271 54275 proof_build_time "0.002"
0 0 bv_not_involutive "0.002"
54271 54275 context_used ""
54271 54275 proof_check_time "0.001"
54357 54363 VernacProof "tac:no using:no"
54457 54461 proof_build_time "0.003"
0 0 bv_not_false_true "0.003"
54457 54461 context_used ""
54457 54461 proof_check_time "0.001"
54543 54549 VernacProof "tac:no using:no"
54643 54647 proof_build_time "0.002"
0 0 bv_not_true_false "0.002"
54643 54647 context_used ""
54643 54647 proof_check_time "0.001"
54767 54773 VernacProof "tac:no using:no"
55118 55122 proof_build_time "0.027"
0 0 bv_not_and_or "0.027"
55118 55122 context_used ""
55118 55122 proof_check_time "0.009"
55242 55248 VernacProof "tac:no using:no"
55605 55609 proof_build_time "0.054"
0 0 bv_not_or_and "0.054"
55605 55609 context_used ""
55605 55609 proof_check_time "0.005"
55713 55719 VernacProof "tac:no using:no"
55758 55762 proof_build_time "0.002"
0 0 add_carry_ff "0.002"
55758 55762 context_used ""
55758 55762 proof_check_time "0.001"
55841 55847 VernacProof "tac:no using:no"
55886 55890 proof_build_time "0.002"
0 0 add_carry_neg_f "0.002"
55886 55890 context_used ""
55886 55890 proof_check_time "0.001"
55971 55977 VernacProof "tac:no using:no"
56016 56020 proof_build_time "0.002"
0 0 add_carry_neg_f_r "0.002"
56016 56020 context_used ""
56016 56020 proof_check_time "0.001"
56098 56104 VernacProof "tac:no using:no"
56143 56147 proof_build_time "0.002"
0 0 add_carry_neg_t "0.002"
56143 56147 context_used ""
56143 56147 proof_check_time "0.001"
56214 56220 VernacProof "tac:no using:no"
56244 56248 proof_build_time "0.002"
0 0 add_carry_tt "0.002"
56244 56248 context_used ""
56244 56248 proof_check_time "0.000"
56319 56325 VernacProof "tac:no using:no"
56437 56441 proof_build_time "0.003"
0 0 add_list_empty_l "0.003"
56437 56441 context_used ""
56437 56441 proof_check_time "0.001"
56512 56518 VernacProof "tac:no using:no"
56596 56600 proof_build_time "0.002"
0 0 add_list_empty_r "0.002"
56596 56600 context_used ""
56596 56600 proof_check_time "0.001"
56687 56693 VernacProof "tac:no using:no"
56771 56775 proof_build_time "0.005"
0 0 add_list_ingr_l "0.005"
56771 56775 context_used ""
56771 56775 proof_check_time "0.002"
56862 56868 VernacProof "tac:no using:no"
56946 56950 proof_build_time "0.005"
0 0 add_list_ingr_r "0.005"
56946 56950 context_used ""
56946 56950 proof_check_time "0.002"
57058 57064 VernacProof "tac:no using:no"
57446 57450 proof_build_time "0.025"
0 0 add_list_carry_comm "0.025"
57446 57450 context_used ""
57446 57450 proof_check_time "0.004"
57531 57537 VernacProof "tac:no using:no"
57606 57610 proof_build_time "0.001"
0 0 add_list_comm "0.001"
57606 57610 context_used ""
57606 57610 proof_check_time "0.000"
57884 57890 VernacProof "tac:no using:no"
58651 58655 proof_build_time "11.507"
0 0 add_list_carry_assoc "11.507"
58651 58655 context_used ""
58651 58655 proof_check_time "4.347"
58780 58786 VernacProof "tac:no using:no"
59072 59076 proof_build_time "0.026"
0 0 add_list_carry_length_eq "0.026"
59072 59076 context_used ""
59072 59076 proof_check_time "0.008"
59208 59214 VernacProof "tac:no using:no"
59491 59495 proof_build_time "0.085"
0 0 add_list_carry_length_ge "0.085"
59491 59495 context_used ""
59491 59495 proof_check_time "0.009"
59627 59633 VernacProof "tac:no using:no"
59931 59935 proof_build_time "0.051"
0 0 add_list_carry_length_le "0.051"
59931 59935 context_used ""
59931 59935 proof_check_time "0.009"
60005 60011 VernacProof "tac:no using:no"
60311 60315 proof_build_time "0.007"
0 0 bv_neg_size "0.007"
60311 60315 context_used ""
60311 60315 proof_check_time "0.002"
60425 60431 VernacProof "tac:no using:no"
60517 60521 proof_build_time "0.002"
0 0 length_add_list_eq "0.002"
60517 60521 context_used ""
60517 60521 proof_check_time "0.000"
60638 60644 VernacProof "tac:no using:no"
60730 60734 proof_build_time "0.001"
0 0 length_add_list_ge "0.001"
60730 60734 context_used ""
60730 60734 proof_check_time "0.000"
60851 60857 VernacProof "tac:no using:no"
60943 60947 proof_build_time "0.001"
0 0 length_add_list_le "0.001"
60943 60947 context_used ""
60943 60947 proof_check_time "0.000"
61057 61063 VernacProof "tac:no using:no"
61190 61194 proof_build_time "0.002"
0 0 add_list_assoc "0.002"
61190 61194 context_used ""
61190 61194 proof_check_time "0.001"
61333 61339 VernacProof "tac:no using:no"
61588 61592 proof_build_time "0.064"
0 0 add_list_carry_empty_neutral_n_l "0.064"
61588 61592 context_used ""
61588 61592 proof_check_time "0.021"
61731 61737 VernacProof "tac:no using:no"
61986 61990 proof_build_time "0.106"
0 0 add_list_carry_empty_neutral_n_r "0.106"
61986 61990 context_used ""
61986 61990 proof_check_time "0.009"
62109 62115 VernacProof "tac:no using:no"
62180 62184 proof_build_time "0.002"
0 0 add_list_carry_empty_neutral_l "0.002"
62180 62184 context_used ""
62180 62184 proof_check_time "0.000"
62303 62309 VernacProof "tac:no using:no"
62374 62378 proof_build_time "0.002"
0 0 add_list_carry_empty_neutral_r "0.002"
62374 62378 context_used ""
62374 62378 proof_check_time "0.001"
62500 62506 VernacProof "tac:no using:no"
62586 62590 proof_build_time "0.001"
0 0 add_list_empty_neutral_n_l "0.001"
62586 62590 context_used ""
62586 62590 proof_check_time "0.000"
62712 62718 VernacProof "tac:no using:no"
62798 62802 proof_build_time "0.001"
0 0 add_list_empty_neutral_n_r "0.001"
62798 62802 context_used ""
62798 62802 proof_check_time "0.000"
62904 62910 VernacProof "tac:no using:no"
62988 62992 proof_build_time "0.002"
0 0 add_list_empty_neutral_r "0.002"
62988 62992 context_used ""
62988 62992 proof_check_time "0.000"
63094 63100 VernacProof "tac:no using:no"
63178 63182 proof_build_time "0.001"
0 0 add_list_empty_neutral_l "0.001"
63178 63182 context_used ""
63178 63182 proof_check_time "0.000"
63276 63282 VernacProof "tac:no using:no"
63518 63522 proof_build_time "0.010"
0 0 add_list_carry_unit_t "0.010"
63518 63522 context_used ""
63518 63522 proof_check_time "0.004"
63607 63613 VernacProof "tac:no using:no"
64244 64248 proof_build_time "0.027"
0 0 add_list_carry_twice "0.027"
64244 64248 context_used ""
64244 64248 proof_check_time "0.012"
64322 64328 VernacProof "tac:no using:no"
64406 64410 proof_build_time "0.002"
0 0 add_list_twice "0.002"
64406 64410 context_used ""
64406 64410 proof_check_time "0.001"
64531 64537 VernacProof "tac:no using:no"
64759 64763 proof_build_time "0.008"
0 0 bv_add_size "0.008"
64759 64763 context_used ""
64759 64763 proof_check_time "0.002"
64855 64861 VernacProof "tac:no using:no"
65034 65038 proof_build_time "0.006"
0 0 bv_add_comm "0.006"
65034 65038 context_used ""
65034 65038 proof_check_time "0.002"
65211 65217 VernacProof "tac:no using:no"
65758 65762 proof_build_time "0.043"
0 0 bv_add_assoc "0.043"
65758 65762 context_used ""
65758 65762 proof_check_time "0.025"
65854 65860 VernacProof "tac:no using:no"
66036 66040 proof_build_time "0.013"
0 0 bv_add_empty_neutral_l "0.013"
66036 66040 context_used ""
66036 66040 proof_check_time "0.007"
66132 66138 VernacProof "tac:no using:no"
66313 66317 proof_build_time "0.010"
0 0 bv_add_empty_neutral_r "0.010"
66313 66317 context_used ""
66313 66317 proof_check_time "0.002"
66387 66393 VernacProof "tac:no using:no"
66528 66532 proof_build_time "0.008"
0 0 bv_add_twice "0.008"
66528 66532 context_used ""
66528 66532 proof_check_time "0.001"
66632 66638 VernacProof "tac:no using:no"
66673 66677 proof_build_time "0.006"
0 0 subst_list_empty_empty_l "0.006"
66673 66677 context_used ""
66673 66677 proof_check_time "0.000"
66745 66751 VernacProof "tac:no using:no"
66849 66853 proof_build_time "0.006"
0 0 subst_list_empty_empty_r "0.006"
66849 66853 context_used ""
66849 66853 proof_check_time "0.001"
66923 66929 VernacProof "tac:no using:no"
67070 67074 proof_build_time "0.014"
0 0 subst_list'_empty_empty_r "0.014"
67070 67074 context_used ""
67070 67074 proof_check_time "0.002"
67204 67210 VernacProof "tac:no using:no"
67505 67509 proof_build_time "0.037"
0 0 subst_list_borrow_length "0.037"
67505 67509 context_used ""
67505 67509 proof_check_time "0.004"
67603 67609 VernacProof "tac:no using:no"
67987 67991 proof_build_time "0.012"
0 0 length_twos_complement "0.012"
67987 67991 context_used ""
67987 67991 proof_check_time "0.003"
68103 68109 VernacProof "tac:no using:no"
68197 68201 proof_build_time "0.002"
0 0 subst_list_length "0.002"
68197 68201 context_used ""
68197 68201 proof_check_time "0.000"
68314 68320 VernacProof "tac:no using:no"
68498 68502 proof_build_time "0.017"
0 0 subst_list'_length "0.017"
68498 68502 context_used ""
68498 68502 proof_check_time "0.001"
68626 68632 VernacProof "tac:no using:no"
68881 68885 proof_build_time "0.007"
0 0 subst_list_borrow_empty_neutral "0.007"
68881 68885 context_used ""
68881 68885 proof_check_time "0.002"
68989 68995 VernacProof "tac:no using:no"
69076 69080 proof_build_time "0.001"
0 0 subst_list_empty_neutral "0.001"
69076 69080 context_used ""
69076 69080 proof_check_time "0.000"
69185 69191 VernacProof "tac:no using:no"
69283 69287 proof_build_time "0.005"
0 0 twos_complement_cons_false "0.005"
69283 69287 context_used ""
69283 69287 proof_check_time "0.002"
69387 69393 VernacProof "tac:no using:no"
69542 69546 proof_build_time "0.006"
0 0 twos_complement_false_false "0.006"
69542 69546 context_used ""
69542 69546 proof_check_time "0.001"
69652 69658 VernacProof "tac:no using:no"
69801 69805 proof_build_time "0.003"
0 0 subst_list'_empty_neutral "0.003"
69801 69805 context_used ""
69801 69805 proof_check_time "0.001"
70007 70013 VernacProof "tac:no using:no"
71418 71422 proof_build_time "0.513"
0 0 ult_list_big_endian_trans "0.513"
71418 71422 context_used ""
71418 71422 proof_check_time "0.089"
71537 71543 VernacProof "tac:no using:no"
71608 71612 proof_build_time "0.001"
0 0 ult_list_trans "0.001"
71608 71612 context_used ""
71608 71612 proof_check_time "0.001"
71707 71713 VernacProof "tac:no using:no"
72181 72185 proof_build_time "0.268"
0 0 ult_list_big_endian_not_eq "0.268"
72181 72185 context_used ""
72181 72185 proof_check_time "0.021"
72256 72262 VernacProof "tac:no using:no"
72358 72362 proof_build_time "0.003"
0 0 ult_list_not_eq "0.003"
72358 72362 context_used ""
72358 72362 proof_check_time "0.001"
72457 72463 VernacProof "tac:no using:no"
72945 72949 proof_build_time "0.250"
0 0 slt_list_big_endian_not_eq "0.250"
72945 72949 context_used ""
72945 72949 proof_check_time "0.051"
73020 73026 VernacProof "tac:no using:no"
73122 73126 proof_build_time "0.007"
0 0 slt_list_not_eq "0.007"
73122 73126 context_used ""
73122 73126 proof_check_time "0.001"
73191 73197 VernacProof "tac:no using:no"
73418 73422 proof_build_time "0.016"