-
Notifications
You must be signed in to change notification settings - Fork 0
/
.IndProp.aux
629 lines (629 loc) · 20.4 KB
/
.IndProp.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
COQAUX1 76001e5755071e267b364df10e18ea47 C:\Users\fang\Desktop\If\IndProp.v
2958 3049 context_used ""
4812 4818 VernacProof "tac:no using:no"
4857 4861 proof_build_time "0.000"
0 0 ev_4 "0.000"
4857 4861 context_used ""
4857 4861 proof_check_time "0.000"
4940 4946 VernacProof "tac:no using:no"
4979 4983 proof_build_time "0.000"
0 0 ev_4' "0.000"
4979 4983 context_used ""
4979 4983 proof_check_time "0.000"
5106 5112 VernacProof "tac:no using:no"
5181 5185 proof_build_time "0.000"
0 0 ev_plus4 "0.000"
5181 5185 context_used ""
5181 5185 proof_check_time "0.000"
5353 5359 VernacProof "tac:no using:no"
5455 5459 proof_build_time "0.000"
0 0 ev_double "0.000"
5455 5459 context_used ""
5455 5459 proof_check_time "0.000"
7878 7884 VernacProof "tac:no using:no"
8009 8013 proof_build_time "0.016"
0 0 ev_minus2 "0.016"
8009 8013 context_used ""
8009 8013 proof_check_time "0.000"
8757 8763 VernacProof "tac:no using:no"
8887 8891 proof_build_time "0.000"
0 0 ev_minus2' "0.000"
8887 8891 context_used ""
8887 8891 proof_check_time "0.000"
9756 9762 VernacProof "tac:no using:no"
9886 9892 proof_build_time "0.000"
9886 9892 proof_check_time "0.000"
10611 10617 VernacProof "tac:no using:no"
10722 10726 proof_build_time "0.000"
0 0 evSS_ev "0.000"
10722 10726 context_used ""
10722 10726 proof_check_time "0.000"
10927 10933 VernacProof "tac:no using:no"
10959 10963 proof_build_time "0.000"
0 0 one_not_even "0.000"
10959 10963 context_used ""
10959 10963 proof_check_time "0.000"
11129 11135 VernacProof "tac:no using:no"
11194 11198 proof_build_time "0.000"
0 0 SSSSev__even "0.000"
11194 11198 context_used ""
11194 11198 proof_check_time "0.000"
11357 11363 VernacProof "tac:no using:no"
11423 11427 proof_build_time "0.000"
0 0 even5_nonsense "0.000"
11423 11427 context_used ""
11423 11427 proof_check_time "0.000"
12948 12954 VernacProof "tac:no using:no"
14488 14497 proof_build_time "0.000"
0 0 ev_even_firsttry "0.000"
14488 14497 proof_check_time "0.000"
15259 15265 VernacProof "tac:no using:no"
15499 15503 proof_build_time "0.016"
0 0 ev_even "0.016"
15499 15503 context_used ""
15499 15503 proof_check_time "0.000"
15928 15934 VernacProof "tac:no using:no"
16039 16043 proof_build_time "0.001"
0 0 ev_even_iff "0.001"
16039 16043 context_used ""
16039 16043 proof_check_time "0.000"
16517 16523 VernacProof "tac:no using:no"
16646 16650 proof_build_time "0.002"
0 0 ev_sum "0.002"
16646 16650 context_used ""
16646 16650 proof_check_time "0.001"
16879 16996 context_used ""
17208 17214 VernacProof "tac:no using:no"
17528 17532 proof_build_time "0.004"
0 0 ev'_ev "0.004"
17528 17532 context_used ""
17528 17532 proof_check_time "0.001"
17743 17749 VernacProof "tac:no using:no"
17895 17899 proof_build_time "0.003"
0 0 ev_ev__ev "0.003"
17895 17899 context_used ""
17895 17899 proof_check_time "0.000"
18202 18208 VernacProof "tac:no using:no"
18763 18767 proof_build_time "0.292"
0 0 ev_plus_plus "0.292"
18763 18767 context_used ""
18763 18767 proof_check_time "0.001"
19664 19777 context_used ""
20621 20627 VernacProof "tac:no using:no"
20667 20671 proof_build_time "0.000"
0 0 test_le1 "0.000"
20667 20671 context_used ""
20667 20671 proof_check_time "0.000"
20702 20708 VernacProof "tac:no using:no"
20784 20788 proof_build_time "0.002"
0 0 test_le2 "0.002"
20784 20788 context_used ""
20784 20788 proof_check_time "0.000"
20834 20840 VernacProof "tac:no using:no"
20905 20909 proof_build_time "0.008"
0 0 test_le3 "0.008"
20905 20909 context_used ""
20905 20909 proof_check_time "0.002"
21019 21057 context_used ""
21147 21234 context_used ""
21236 21319 context_used ""
21321 21475 context_used ""
21650 21947 context_used ""
22486 22492 VernacProof "tac:no using:no"
22699 22703 proof_build_time "0.002"
0 0 le_trans "0.002"
22699 22703 context_used ""
22699 22703 proof_check_time "0.001"
22742 22748 VernacProof "tac:no using:no"
22842 22846 proof_build_time "0.001"
0 0 O_le_n "0.001"
22842 22846 context_used ""
22842 22846 proof_check_time "0.000"
22911 22917 VernacProof "tac:no using:no"
23013 23017 proof_build_time "0.001"
0 0 n_le_m__Sn_le_Sm "0.001"
23013 23017 context_used ""
23013 23017 proof_check_time "0.000"
23083 23089 VernacProof "tac:no using:no"
23322 23326 proof_build_time "0.006"
0 0 Sn_le_Sm__n_le_m "0.006"
23322 23326 context_used ""
23322 23326 proof_check_time "0.001"
23374 23380 VernacProof "tac:no using:no"
23510 23514 proof_build_time "0.001"
0 0 le_plus_l "0.001"
23510 23514 context_used ""
23510 23514 proof_check_time "0.000"
23785 23791 VernacProof "tac:no using:no"
24043 24047 proof_build_time "0.003"
0 0 plus_lt "0.003"
24043 24047 context_used ""
24043 24047 proof_check_time "0.000"
24099 24105 VernacProof "tac:no using:no"
24150 24154 proof_build_time "0.000"
0 0 lt_S "0.000"
24150 24154 context_used ""
24150 24154 proof_check_time "0.000"
24219 24225 VernacProof "tac:no using:no"
24417 24421 proof_build_time "0.002"
0 0 leb_complete "0.002"
24417 24421 context_used ""
24417 24421 proof_check_time "0.000"
24543 24549 VernacProof "tac:no using:no"
24620 24624 proof_build_time "0.001"
0 0 leb_gep_O "0.001"
24620 24624 context_used ""
24620 24624 proof_check_time "0.001"
24690 24696 VernacProof "tac:no using:no"
24924 24928 proof_build_time "0.003"
0 0 leb_correct "0.003"
24924 24928 context_used ""
24924 24928 proof_check_time "0.001"
25062 25068 VernacProof "tac:no using:no"
25126 25130 proof_build_time "0.001"
0 0 leb_eq_le "0.001"
25126 25130 context_used ""
25126 25130 proof_check_time "0.000"
25224 25230 VernacProof "tac:no using:no"
25346 25350 proof_build_time "0.015"
0 0 leb_true_trans "0.015"
25346 25350 context_used ""
25346 25350 proof_check_time "0.001"
25475 25481 VernacProof "tac:no using:no"
25502 25506 proof_build_time "0.001"
0 0 leb_iff "0.001"
25502 25506 context_used ""
25502 25506 proof_check_time "0.000"
25772 26037 context_used ""
26840 26882 context_used ""
26943 26949 VernacProof "tac:no using:no"
27872 27876 proof_build_time "0.099"
0 0 R_equiv_fR "0.099"
27872 27876 context_used ""
27872 27876 proof_check_time "0.002"
29076 29272 context_used ""
29317 29323 VernacProof "tac:no using:no"
29413 29417 proof_build_time "0.001"
0 0 subseq_refl "0.001"
29413 29417 context_used ""
29413 29417 proof_check_time "0.000"
29494 29500 VernacProof "tac:no using:no"
29776 29780 proof_build_time "0.013"
0 0 subseq_app "0.013"
29776 29780 context_used ""
29776 29780 proof_check_time "0.003"
29867 29873 VernacProof "tac:no using:no"
30308 30312 proof_build_time "0.023"
0 0 subseq_trans "0.023"
30308 30312 context_used ""
30308 30312 proof_check_time "0.006"
30722 30884 context_used ""
30919 30925 VernacProof "tac:no using:no"
31008 31012 proof_build_time "0.002"
0 0 test_R_1 "0.002"
31008 31012 context_used ""
31008 31012 proof_check_time "0.001"
31766 31975 context_used ""
31766 31975 context_used ""
31766 31975 context_used ""
33435 34117 context_used ""
36541 36547 VernacProof "tac:no using:no"
36563 36567 proof_build_time "0.000"
0 0 reg_exp_ex1 "0.000"
36563 36567 context_used ""
36563 36567 proof_check_time "0.000"
36624 36630 VernacProof "tac:no using:no"
36691 36695 proof_build_time "0.001"
0 0 reg_exp_ex2 "0.001"
36691 36695 context_used ""
36691 36695 proof_check_time "0.001"
37080 37086 VernacProof "tac:no using:no"
37112 37116 proof_build_time "0.006"
0 0 reg_exp_ex3 "0.006"
37112 37116 context_used ""
37112 37116 proof_check_time "0.003"
37333 37467 context_used ""
37531 37537 VernacProof "tac:no using:no"
37678 37682 proof_build_time "0.002"
0 0 reg_exp_ex4 "0.002"
37678 37682 context_used ""
37678 37682 proof_check_time "0.000"
37937 37943 VernacProof "tac:no using:no"
38052 38056 proof_build_time "0.001"
0 0 MStar1 "0.001"
38052 38056 context_used ""
38052 38056 proof_check_time "0.000"
38465 38471 VernacProof "tac:no using:no"
38513 38517 proof_build_time "0.006"
0 0 empty_is_empty "0.006"
38513 38517 context_used ""
38513 38517 proof_check_time "0.002"
38629 38635 VernacProof "tac:no using:no"
38744 38748 proof_build_time "0.002"
0 0 MUnion' "0.002"
38744 38748 context_used ""
38744 38748 proof_check_time "0.000"
39122 39128 VernacProof "tac:no using:no"
39621 39625 proof_build_time "0.009"
0 0 MStar' "0.009"
39621 39625 context_used ""
39621 39625 proof_check_time "0.002"
39852 39858 VernacProof "tac:no using:no"
40037 40041 proof_build_time "0.004"
0 0 plus_nil_l "0.004"
40037 40041 context_used ""
40037 40041 proof_check_time "0.001"
40141 40147 VernacProof "tac:no using:no"
40771 40775 proof_build_time "0.140"
0 0 reg_exp_of_list_spec "0.140"
40771 40775 context_used ""
40771 40775 proof_check_time "0.000"
41327 41579 context_used ""
41747 41753 VernacProof "tac:no using:no"
43124 43128 proof_build_time "0.018"
0 0 in_re_match "0.018"
43124 43128 context_used ""
43124 43128 proof_check_time "0.001"
43332 43634 context_used ""
43716 43722 VernacProof "tac:no using:no"
43780 43784 proof_build_time "0.001"
0 0 true_or_l "0.001"
43780 43784 context_used ""
43780 43784 proof_check_time "0.000"
43831 43837 VernacProof "tac:no using:no"
43956 43960 proof_build_time "0.002"
0 0 a_or_b "0.002"
43956 43960 context_used ""
43956 43960 proof_check_time "0.000"
44069 44075 VernacProof "tac:no using:no"
45060 45064 proof_build_time "0.096"
0 0 re_not_empty_correct "0.096"
45060 45064 context_used ""
45060 45064 proof_check_time "0.000"
45626 45632 VernacProof "tac:no using:no"
46745 46751 proof_build_time "0.017"
46745 46751 proof_check_time "0.000"
47800 47806 proof_build_time "0.000"
47800 47806 proof_check_time "0.000"
48170 48176 VernacProof "tac:no using:no"
49277 49281 proof_build_time "0.005"
0 0 star_app "0.005"
49277 49281 context_used ""
49277 49281 proof_check_time "0.000"
49710 49716 VernacProof "tac:no using:no"
50326 50330 proof_build_time "0.031"
0 0 MStar'' "0.031"
50326 50330 context_used ""
50326 50330 proof_check_time "0.000"
51035 51322 context_used ""
51454 51567 context_used ""
51662 51668 VernacProof "tac:no using:no"
51779 51783 proof_build_time "0.016"
0 0 napp_plus "0.016"
51779 51783 context_used ""
51779 51783 proof_check_time "0.000"
51863 51869 VernacProof "tac:no using:no"
52022 52026 proof_build_time "0.000"
0 0 napp_star "0.000"
52022 52026 context_used ""
52022 52026 proof_check_time "0.000"
52758 52764 VernacProof "tac:no using:no"
52846 52852 proof_build_time "0.000"
52846 52852 proof_check_time "0.000"
52929 52935 VernacProof "tac:no using:no"
53474 53478 proof_build_time "0.504"
0 0 a_b_c_d "0.504"
53474 53478 context_used ""
53474 53478 proof_check_time "0.000"
53546 53552 VernacProof "tac:no using:no"
53694 53698 proof_build_time "0.000"
0 0 S_le_a_b "0.000"
53694 53698 context_used ""
53694 53698 proof_check_time "0.000"
54387 54393 VernacProof "tac:no using:no"
57149 57153 proof_build_time "0.455"
57149 57153 context_used ""
57149 57153 proof_check_time "0.024"
57649 57655 VernacProof "tac:no using:no"
58014 58018 proof_build_time "0.004"
0 0 filter_not_empty_In "0.004"
58014 58018 context_used ""
58014 58018 proof_check_time "0.001"
58659 58775 context_used ""
59652 59658 VernacProof "tac:no using:no"
59811 59815 proof_build_time "0.004"
0 0 iff_reflect "0.004"
59811 59815 context_used ""
59811 59815 proof_check_time "0.001"
59942 59948 VernacProof "tac:no using:no"
60136 60140 proof_build_time "0.005"
0 0 reflect_iff "0.005"
60136 60140 context_used ""
60136 60140 proof_check_time "0.001"
60547 60553 VernacProof "tac:no using:no"
60626 60630 proof_build_time "0.001"
0 0 beq_natP "0.001"
60626 60630 context_used ""
60626 60630 proof_check_time "0.000"
61085 61091 VernacProof "tac:no using:no"
61393 61397 proof_build_time "0.004"
0 0 filter_not_empty_In' "0.004"
61393 61397 context_used ""
61393 61397 proof_check_time "0.001"
61519 61633 context_used ""
61705 61711 VernacProof "tac:no using:no"
62023 62027 proof_build_time "0.005"
0 0 beq_natP_practice "0.005"
62023 62027 context_used ""
62023 62027 proof_check_time "0.001"
63452 63629 context_used ""
64270 64276 VernacProof "tac:no using:no"
64330 64334 proof_build_time "0.004"
0 0 test_nostutter_1 "0.004"
64330 64334 context_used ""
64330 64334 proof_check_time "0.000"
64412 64418 VernacProof "tac:no using:no"
64472 64476 proof_build_time "0.000"
0 0 test_nostutter_2 "0.000"
64472 64476 context_used ""
64472 64476 proof_check_time "0.000"
64524 64530 VernacProof "tac:no using:no"
64578 64582 proof_build_time "0.000"
0 0 test_nostutter_3 "0.000"
64578 64582 context_used ""
64578 64582 proof_check_time "0.000"
64645 64651 VernacProof "tac:no using:no"
64772 64776 proof_build_time "0.016"
0 0 test_nostutter_4 "0.016"
64772 64776 context_used ""
64772 64776 proof_check_time "0.000"
65833 66112 context_used ""
66235 66241 VernacProof "tac:no using:no"
66319 66323 proof_build_time "0.016"
0 0 test_merge "0.016"
66319 66323 context_used ""
66319 66323 proof_check_time "0.000"
66442 66448 VernacProof "tac:no using:no"
66599 66603 proof_build_time "0.016"
0 0 mergelist_nil_l "0.016"
66599 66603 context_used ""
66599 66603 proof_check_time "0.000"
66680 66686 VernacProof "tac:no using:no"
66835 66839 proof_build_time "0.000"
0 0 mergelist_nil_r "0.000"
66835 66839 context_used ""
66835 66839 proof_check_time "0.016"
67216 67222 VernacProof "tac:no using:no"
68305 68309 proof_build_time "0.361"
0 0 filter_challenge "0.361"
68305 68309 context_used ""
68305 68309 proof_check_time "0.011"
69334 69464 context_used ""
69526 69532 VernacProof "tac:no using:no"
69640 69644 proof_build_time "0.000"
0 0 pal_app_rev "0.000"
69640 69644 context_used ""
69640 69644 proof_check_time "0.000"
69704 69710 VernacProof "tac:no using:no"
69856 69860 proof_build_time "0.106"
0 0 pal_rev "0.106"
69856 69860 context_used ""
69856 69860 proof_check_time "0.000"
70471 70573 context_used ""
70575 70673 context_used ""
70675 70740 context_used ""
70741 70801 context_used ""
70866 70872 VernacProof "tac:no using:no"
70888 70892 proof_build_time "0.000"
0 0 test_tail "0.000"
70888 70892 context_used ""
70888 70892 proof_check_time "0.000"
70976 70982 VernacProof "tac:no using:no"
71208 71212 proof_build_time "0.117"
0 0 liat_snoc "0.117"
71208 71212 context_used ""
71208 71212 proof_check_time "0.001"
71312 71318 VernacProof "tac:no using:no"
71449 71453 proof_build_time "0.004"
0 0 tail_htt "0.004"
71449 71453 context_used ""
71449 71453 proof_check_time "0.001"
71538 71544 VernacProof "tac:no using:no"
71775 71779 proof_build_time "0.006"
0 0 liat_htt "0.006"
71775 71779 context_used ""
71775 71779 proof_check_time "0.000"
71894 71900 VernacProof "tac:no using:no"
72062 72066 proof_build_time "0.000"
0 0 lemma "0.000"
72062 72066 context_used ""
72062 72066 proof_check_time "0.000"
72137 72143 VernacProof "tac:no using:no"
72216 72220 proof_build_time "0.127"
0 0 tail_rev "0.127"
72216 72220 context_used ""
72216 72220 proof_check_time "0.000"
72290 72296 VernacProof "tac:no using:no"
72378 72382 proof_build_time "0.000"
0 0 liat_rev "0.000"
72378 72382 context_used ""
72378 72382 proof_check_time "0.000"
72455 72461 VernacProof "tac:no using:no"
72686 72692 proof_build_time "0.000"
72686 72692 proof_check_time "0.000"
73289 73531 context_used ""
73920 74065 context_used ""
74779 74785 VernacProof "tac:no using:no"
75090 75094 proof_build_time "0.016"
0 0 in_split "0.016"
75090 75094 context_used ""
75090 75094 proof_check_time "0.000"
76002 76008 VernacProof "tac:no using:no"
76156 76160 proof_build_time "0.000"
0 0 In_x_x'_l "0.000"
76156 76160 context_used ""
76156 76160 proof_check_time "0.000"
76162 76327 context_used ""
76460 76466 VernacProof "tac:no using:no"
76717 76721 proof_build_time "0.019"
0 0 appears_in_app "0.019"
76717 76721 context_used ""
76717 76721 proof_check_time "0.001"
76855 76861 VernacProof "tac:no using:no"
77159 77163 proof_build_time "0.008"
0 0 app_appears_in "0.008"
77159 77163 context_used ""
77159 77163 proof_check_time "0.001"
77291 77297 VernacProof "tac:no using:no"
77561 77565 proof_build_time "0.009"
0 0 appears_in_app_split "0.009"
77561 77565 context_used ""
77561 77565 proof_check_time "0.003"
77663 77669 VernacProof "tac:no using:no"
77758 77762 proof_build_time "0.001"
0 0 ai_comm "0.001"
77758 77762 context_used ""
77758 77762 proof_check_time "0.001"
77764 77945 context_used ""
77989 77995 VernacProof "tac:no using:no"
78043 78047 proof_build_time "0.001"
0 0 test_repeats1 "0.001"
78043 78047 context_used ""
78043 78047 proof_check_time "0.000"
78157 78163 VernacProof "tac:no using:no"
78269 78273 proof_build_time "0.004"
0 0 ai_later' "0.004"
78269 78273 context_used ""
78269 78273 proof_check_time "0.001"
78457 78463 VernacProof "tac:no using:no"
79291 79295 proof_build_time "0.106"
0 0 pigeonhole_principle "0.106"
79291 79295 context_used ""
79291 79295 proof_check_time "0.000"
80795 80827 context_used ""
82055 82061 VernacProof "tac:no using:no"
82129 82133 proof_build_time "0.000"
0 0 provable_equiv_true "0.000"
82129 82133 context_used ""
82129 82133 proof_check_time "0.000"
82271 82277 VernacProof "tac:no using:no"
82336 82340 proof_build_time "0.000"
0 0 not_equiv_false "0.000"
82336 82340 context_used ""
82336 82340 proof_check_time "0.000"
82453 82459 VernacProof "tac:no using:no"
82531 82535 proof_build_time "0.000"
0 0 null_matches_none "0.000"
82531 82535 context_used ""
82531 82535 proof_check_time "0.000"
82660 82666 VernacProof "tac:no using:no"
82751 82755 proof_build_time "0.016"
0 0 empty_matches_eps "0.016"
82751 82755 context_used ""
82751 82755 proof_check_time "0.000"
82883 82889 VernacProof "tac:no using:no"
82960 82964 proof_build_time "0.016"
0 0 empty_nomatch_ne "0.016"
82960 82964 context_used ""
82960 82964 proof_check_time "0.000"
83130 83136 VernacProof "tac:no using:no"
83238 83242 proof_build_time "0.000"
0 0 char_nomatch_char "0.000"
83238 83242 context_used ""
83238 83242 proof_check_time "0.016"
83401 83407 VernacProof "tac:no using:no"
83491 83495 proof_build_time "0.000"
0 0 char_eps_suffix "0.000"
83491 83495 context_used ""
83491 83495 proof_check_time "0.000"
83741 83747 VernacProof "tac:no using:no"
83971 83975 proof_build_time "0.016"
0 0 app_exists "0.016"
83971 83975 context_used ""
83971 83975 proof_check_time "0.000"
84613 84619 VernacProof "tac:no using:no"
85158 85162 proof_build_time "0.031"
0 0 app_ne "0.031"
85158 85162 context_used ""
85158 85162 proof_check_time "0.000"
85340 85346 VernacProof "tac:no using:no"
85517 85521 proof_build_time "0.011"
0 0 union_disj "0.011"
85517 85521 context_used ""
85517 85521 proof_check_time "0.003"
86433 86439 VernacProof "tac:no using:no"
87089 87093 proof_build_time "0.020"
0 0 star_ne "0.020"
87089 87093 context_used ""
87089 87093 proof_check_time "0.008"
87364 87454 context_used ""
87657 87922 context_used ""
88239 88245 VernacProof "tac:no using:no"
88324 88328 proof_build_time "0.000"
0 0 plus_nil_r "0.000"
88324 88328 context_used ""
88324 88328 proof_check_time "0.000"
88380 88386 VernacProof "tac:no using:no"
89752 89756 proof_build_time "0.283"
0 0 match_eps_refl "0.283"
89752 89756 context_used ""
89752 89756 proof_check_time "0.016"
90351 90429 context_used ""
90608 90666 context_used ""
90917 90970 context_used ""
90989 91649 context_used ""
91965 91994 context_used ""
91995 92025 context_used ""
92179 92185 VernacProof "tac:no using:no"
92201 92205 proof_build_time "0.000"
0 0 test_der0 "0.000"
92201 92205 context_used ""
92201 92205 proof_check_time "0.000"
92287 92293 VernacProof "tac:no using:no"
92309 92313 proof_build_time "0.016"
0 0 test_der1 "0.016"
92309 92313 context_used ""
92309 92313 proof_check_time "0.001"
92396 92402 VernacProof "tac:no using:no"
92418 92422 proof_build_time "0.001"
0 0 test_der2 "0.001"
92418 92422 context_used ""
92418 92422 proof_check_time "0.001"
92534 92540 VernacProof "tac:no using:no"
92556 92560 proof_build_time "0.001"
0 0 test_der3 "0.001"
92556 92560 context_used ""
92556 92560 proof_check_time "0.001"
92672 92678 VernacProof "tac:no using:no"
92694 92698 proof_build_time "0.001"
0 0 test_der4 "0.001"
92694 92698 context_used ""
92694 92698 proof_check_time "0.001"
92787 92793 VernacProof "tac:no using:no"
92809 92813 proof_build_time "0.003"
0 0 test_der5 "0.003"
92809 92813 context_used ""
92809 92813 proof_check_time "0.001"
92939 92945 VernacProof "tac:no using:no"
92961 92965 proof_build_time "0.003"
0 0 test_der6 "0.003"
92961 92965 context_used ""
92961 92965 proof_check_time "0.002"
93092 93098 VernacProof "tac:no using:no"
93114 93118 proof_build_time "0.001"
0 0 test_der7 "0.001"
93114 93118 context_used ""
93114 93118 proof_check_time "0.001"
94180 94186 VernacProof "tac:no using:no"
94209 94218 proof_build_time "0.000"
0 0 derive_corr "0.000"
94209 94218 proof_check_time "0.000"
94611 94701 context_used ""
94958 94967 proof_build_time "0.000"
0 0 regex_match "0.000"
94958 94967 proof_check_time "0.000"
95652 95658 VernacProof "tac:no using:no"
95680 95689 proof_build_time "0.000"
0 0 regex_refl "0.000"
95680 95689 proof_check_time "0.000"
0 0 vo_compile_time "6.447"