-
Notifications
You must be signed in to change notification settings - Fork 0
/
.Lists.aux
323 lines (323 loc) · 10.2 KB
/
.Lists.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
COQAUX1 4e6d77dde0206b938144d4d948b7670b /Users/antonio/Desktop/tmp/coc/Lists.v
0 0 VernacProof "tac:no using:no"
3211 3215 proof_build_time "0.003"
0 0 surjective_pairing' "0.003"
3197 3209 context_used ""
3211 3215 proof_check_time "0.001"
0 0 VernacProof "tac:no using:no"
3432 3438 proof_build_time "0.001"
3432 3438 proof_check_time "0.000"
0 0 VernacProof "tac:no using:no"
3743 3747 proof_build_time "0.003"
0 0 surjective_pairing "0.003"
3729 3741 context_used ""
3743 3747 proof_check_time "0.001"
0 0 VernacProof "tac:no using:no"
4158 4162 proof_build_time "0.002"
0 0 snd_fst_is_swap "0.002"
4145 4157 context_used ""
4158 4162 proof_check_time "0.001"
0 0 VernacProof "tac:no using:no"
4361 4365 proof_build_time "0.001"
0 0 fst_swap_is_snd "0.001"
4348 4360 context_used ""
4361 4365 proof_check_time "0.000"
0 0 VernacProof "tac:no using:no"
7926 7930 proof_build_time "0.002"
0 0 test_app1 "0.002"
7913 7925 context_used ""
7926 7930 proof_check_time "0.002"
0 0 VernacProof "tac:no using:no"
8002 8006 proof_build_time "0.001"
0 0 test_app2 "0.001"
7989 8001 context_used ""
8002 8006 proof_check_time "0.001"
0 0 VernacProof "tac:no using:no"
8082 8086 proof_build_time "0.001"
0 0 test_app3 "0.001"
8069 8081 context_used ""
8082 8086 proof_check_time "0.001"
0 0 VernacProof "tac:no using:no"
8774 8778 proof_build_time "0.001"
0 0 test_hd1 "0.001"
8761 8773 context_used ""
8774 8778 proof_check_time "0.001"
0 0 VernacProof "tac:no using:no"
8841 8845 proof_build_time "0.001"
0 0 test_hd2 "0.001"
8828 8840 context_used ""
8841 8845 proof_check_time "0.000"
0 0 VernacProof "tac:no using:no"
8915 8919 proof_build_time "0.001"
0 0 test_tl "0.001"
8902 8914 context_used ""
8915 8919 proof_check_time "0.001"
0 0 VernacProof "tac:no using:no"
9813 9817 proof_build_time "0.002"
0 0 test_nonzeros "0.002"
9800 9812 context_used ""
9813 9817 proof_check_time "0.001"
0 0 VernacProof "tac:no using:no"
9907 9911 proof_build_time "0.002"
0 0 test_nonzeros' "0.002"
9894 9906 context_used ""
9907 9911 proof_check_time "0.001"
0 0 VernacProof "tac:no using:no"
10270 10274 proof_build_time "0.002"
0 0 test_oddmembers "0.002"
10257 10269 context_used ""
10270 10274 proof_check_time "0.001"
0 0 VernacProof "tac:no using:no"
10549 10553 proof_build_time "0.001"
0 0 test_countoddmembers1 "0.001"
10536 10548 context_used ""
10549 10553 proof_check_time "0.001"
0 0 VernacProof "tac:no using:no"
10644 10648 proof_build_time "0.001"
0 0 test_countoddmembers2 "0.001"
10631 10643 context_used ""
10644 10648 proof_check_time "0.001"
0 0 VernacProof "tac:no using:no"
10735 10739 proof_build_time "0.001"
0 0 test_countoddmembers3 "0.001"
10722 10734 context_used ""
10735 10739 proof_check_time "0.000"
0 0 VernacProof "tac:no using:no"
11726 11730 proof_build_time "0.002"
0 0 test_alternate1 "0.002"
11713 11725 context_used ""
11726 11730 proof_check_time "0.003"
0 0 VernacProof "tac:no using:no"
11820 11824 proof_build_time "0.002"
0 0 test_alternate2 "0.002"
11807 11819 context_used ""
11820 11824 proof_check_time "0.002"
0 0 VernacProof "tac:no using:no"
11914 11918 proof_build_time "0.001"
0 0 test_alternate3 "0.001"
11901 11913 context_used ""
11914 11918 proof_check_time "0.001"
0 0 VernacProof "tac:no using:no"
12005 12009 proof_build_time "0.002"
0 0 test_alternate4 "0.002"
11992 12004 context_used ""
12005 12009 proof_check_time "0.003"
0 0 VernacProof "tac:no using:no"
12756 12760 proof_build_time "0.003"
0 0 test_count1 "0.003"
12743 12755 context_used ""
12756 12760 proof_check_time "0.001"
0 0 VernacProof "tac:no using:no"
12838 12842 proof_build_time "0.003"
0 0 test_count2 "0.003"
12825 12837 context_used ""
12838 12842 proof_check_time "0.001"
0 0 VernacProof "tac:no using:no"
12991 12995 proof_build_time "0.004"
0 0 test_sum1 "0.004"
12978 12990 context_used ""
12991 12995 proof_check_time "0.001"
0 0 VernacProof "tac:no using:no"
13145 13149 proof_build_time "0.002"
0 0 test_add1 "0.002"
13132 13144 context_used ""
13145 13149 proof_check_time "0.001"
0 0 VernacProof "tac:no using:no"
13240 13244 proof_build_time "0.002"
0 0 test_add2 "0.002"
13227 13239 context_used ""
13240 13244 proof_check_time "0.001"
0 0 VernacProof "tac:no using:no"
13433 13437 proof_build_time "0.001"
0 0 test_member1 "0.001"
13420 13432 context_used ""
13433 13437 proof_check_time "0.001"
0 0 VernacProof "tac:no using:no"
13525 13529 proof_build_time "0.001"
0 0 test_member2 "0.001"
13512 13524 context_used ""
13525 13529 proof_check_time "0.001"
0 0 VernacProof "tac:no using:no"
13613 13617 proof_build_time "0.001"
0 0 test_member3 "0.001"
13600 13612 context_used ""
13613 13617 proof_check_time "0.000"
0 0 VernacProof "tac:no using:no"
14300 14304 proof_build_time "0.003"
0 0 test_remove_one1 "0.003"
14287 14299 context_used ""
14300 14304 proof_check_time "0.001"
0 0 VernacProof "tac:no using:no"
14394 14398 proof_build_time "0.002"
0 0 test_remove_one2 "0.002"
14381 14393 context_used ""
14394 14398 proof_check_time "0.001"
0 0 VernacProof "tac:no using:no"
14494 14498 proof_build_time "0.003"
0 0 test_remove_one3 "0.003"
14481 14493 context_used ""
14494 14498 proof_check_time "0.002"
0 0 VernacProof "tac:no using:no"
14596 14600 proof_build_time "0.004"
0 0 test_remove_one4 "0.004"
14583 14595 context_used ""
14596 14600 proof_check_time "0.001"
0 0 VernacProof "tac:no using:no"
14873 14877 proof_build_time "0.004"
0 0 test_remove_all1 "0.004"
14860 14872 context_used ""
14873 14877 proof_check_time "0.001"
0 0 VernacProof "tac:no using:no"
14963 14967 proof_build_time "0.001"
0 0 test_remove_all2 "0.001"
14950 14962 context_used ""
14963 14967 proof_check_time "0.001"
0 0 VernacProof "tac:no using:no"
15057 15061 proof_build_time "0.001"
0 0 test_remove_all3 "0.001"
15044 15056 context_used ""
15057 15061 proof_check_time "0.001"
0 0 VernacProof "tac:no using:no"
15166 15170 proof_build_time "0.007"
0 0 test_remove_all4 "0.007"
15153 15165 context_used ""
15166 15170 proof_check_time "0.002"
0 0 VernacProof "tac:no using:no"
15423 15427 proof_build_time "0.002"
0 0 test_subset1 "0.002"
15410 15422 context_used ""
15423 15427 proof_check_time "0.001"
0 0 VernacProof "tac:no using:no"
15524 15528 proof_build_time "0.004"
0 0 test_subset2 "0.004"
15511 15523 context_used ""
15524 15528 proof_check_time "0.001"
0 0 VernacProof "tac:no using:no"
15943 15947 proof_build_time "0.001"
0 0 nil_app "0.001"
15930 15942 context_used ""
15943 15947 proof_check_time "0.000"
0 0 VernacProof "tac:no using:no"
16534 16538 proof_build_time "0.003"
0 0 tl_length_pred "0.003"
16521 16533 context_used ""
16534 16538 proof_check_time "0.001"
0 0 VernacProof "tac:no using:no"
19256 19260 proof_build_time "0.004"
0 0 app_assoc "0.004"
19243 19255 context_used ""
19256 19260 proof_check_time "0.001"
0 0 VernacProof "tac:no using:no"
21249 21253 proof_build_time "0.002"
0 0 test_rev1 "0.002"
21236 21248 context_used ""
21249 21253 proof_check_time "0.001"
0 0 VernacProof "tac:no using:no"
21320 21324 proof_build_time "0.001"
0 0 test_rev2 "0.001"
21307 21319 context_used ""
21320 21324 proof_check_time "0.001"
0 0 VernacProof "tac:no using:no"
22166 22172 proof_build_time "0.005"
22166 22172 proof_check_time "0.000"
0 0 VernacProof "tac:no using:no"
22618 22622 proof_build_time "0.005"
0 0 app_length "0.005"
22605 22617 context_used ""
22618 22622 proof_check_time "0.002"
0 0 VernacProof "tac:no using:no"
23321 23325 proof_build_time "0.008"
0 0 rev_length "0.008"
23308 23320 context_used ""
23321 23325 proof_check_time "0.002"
0 0 VernacProof "tac:no using:no"
25263 25267 proof_build_time "0.002"
0 0 app_nil_r "0.002"
25250 25262 context_used ""
25263 25267 proof_check_time "0.001"
0 0 VernacProof "tac:no using:no"
25614 25618 proof_build_time "0.004"
0 0 rev_app_assoc "0.004"
25601 25613 context_used ""
25614 25618 proof_check_time "0.001"
0 0 VernacProof "tac:no using:no"
25888 25892 proof_build_time "0.004"
0 0 rev_involutive "0.004"
25875 25887 context_used ""
25888 25892 proof_check_time "0.001"
0 0 VernacProof "tac:no using:no"
26109 26113 proof_build_time "0.004"
0 0 app_assoc4 "0.004"
26096 26108 context_used ""
26109 26113 proof_check_time "0.001"
0 0 VernacProof "tac:no using:no"
26506 26510 proof_build_time "0.007"
0 0 nonzeros_app "0.007"
26504 26505 context_used ""
26506 26510 proof_check_time "0.001"
0 0 VernacProof "tac:no using:no"
27053 27057 proof_build_time "0.001"
0 0 test_eqblist1 "0.001"
27040 27052 context_used ""
27053 27057 proof_check_time "0.000"
0 0 VernacProof "tac:no using:no"
27141 27145 proof_build_time "0.001"
0 0 test_eqblist2 "0.001"
27128 27140 context_used ""
27141 27145 proof_check_time "0.000"
0 0 VernacProof "tac:no using:no"
27230 27234 proof_build_time "0.001"
0 0 test_eqblist3 "0.001"
27217 27229 context_used ""
27230 27234 proof_check_time "0.001"
0 0 VernacProof "tac:no using:no"
27522 27526 proof_build_time "0.003"
0 0 eqblist_refl "0.003"
27509 27521 context_used ""
27522 27526 proof_check_time "0.001"
0 0 VernacProof "tac:no using:no"
27882 27886 proof_build_time "0.002"
0 0 rev_injective "0.002"
27869 27881 context_used ""
27882 27886 proof_check_time "0.000"
0 0 VernacProof "tac:no using:no"
29423 29427 proof_build_time "0.001"
0 0 test_nth_error1 "0.001"
29410 29422 context_used ""
29423 29427 proof_check_time "0.001"
0 0 VernacProof "tac:no using:no"
29506 29510 proof_build_time "0.001"
0 0 test_nth_error2 "0.001"
29493 29505 context_used ""
29506 29510 proof_check_time "0.001"
0 0 VernacProof "tac:no using:no"
29587 29591 proof_build_time "0.001"
0 0 test_nth_error3 "0.001"
29574 29586 context_used ""
29587 29591 proof_check_time "0.001"
0 0 VernacProof "tac:no using:no"
30777 30781 proof_build_time "0.001"
0 0 test_hd_error1 "0.001"
30764 30776 context_used ""
30777 30781 proof_check_time "0.000"
0 0 VernacProof "tac:no using:no"
30850 30854 proof_build_time "0.001"
0 0 test_hd_error2 "0.001"
30837 30849 context_used ""
30850 30854 proof_check_time "0.001"
0 0 VernacProof "tac:no using:no"
30932 30936 proof_build_time "0.001"
0 0 test_hd_error3 "0.001"
30919 30931 context_used ""
30932 30936 proof_check_time "0.001"
0 0 VernacProof "tac:no using:no"
31956 31960 proof_build_time "0.008"
0 0 eqb_id_refl "0.008"
31943 31955 context_used ""
31956 31960 proof_check_time "0.000"
0 0 VernacProof "tac:no using:no"
33523 33527 proof_build_time "0.002"
0 0 update_eq "0.002"
33510 33522 context_used ""
33523 33527 proof_check_time "0.000"
0 0 vo_compile_time "2.084"