-
Notifications
You must be signed in to change notification settings - Fork 0
/
.c3.aux
347 lines (347 loc) · 10.7 KB
/
.c3.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
COQAUX1 88ebd3f3c3e429eff1dd28733db3b604 /usr/gaodc/coq_learn/c3.v
0 0 VernacProof "tac:no using:no"
707 711 proof_build_time "0.000"
0 0 surjective_pairing' "0.000"
694 706 context_used ""
707 711 proof_check_time "0.000"
0 0 VernacProof "tac:no using:no"
860 864 proof_build_time "0.000"
0 0 surjective_pairing_stuck "0.000"
847 859 context_used ""
860 864 proof_check_time "0.000"
0 0 VernacProof "tac:no using:no"
1013 1017 proof_build_time "0.001"
0 0 snd_fst_is_swap "0.001"
1000 1012 context_used ""
1013 1017 proof_check_time "0.000"
0 0 VernacProof "tac:no using:no"
1162 1166 proof_build_time "0.000"
0 0 fst_swap_is_snd "0.000"
1149 1161 context_used ""
1162 1166 proof_check_time "0.000"
0 0 VernacProof "tac:no using:no"
1967 1971 proof_build_time "0.000"
0 0 test_app1 "0.000"
1954 1966 context_used ""
1967 1971 proof_check_time "0.000"
0 0 VernacProof "tac:no using:no"
2033 2037 proof_build_time "0.000"
0 0 test_app2 "0.000"
2020 2032 context_used ""
2033 2037 proof_check_time "0.000"
0 0 VernacProof "tac:no using:no"
2103 2107 proof_build_time "0.000"
0 0 test_app3 "0.000"
2090 2102 context_used ""
2103 2107 proof_check_time "0.000"
0 0 VernacProof "tac:no using:no"
2385 2389 proof_build_time "0.000"
0 0 test_hd1 "0.000"
2372 2384 context_used ""
2385 2389 proof_check_time "0.000"
0 0 VernacProof "tac:no using:no"
2441 2445 proof_build_time "0.000"
0 0 test_hd2 "0.000"
2428 2440 context_used ""
2441 2445 proof_check_time "0.000"
0 0 VernacProof "tac:no using:no"
2503 2507 proof_build_time "0.000"
0 0 test_tl "0.000"
2490 2502 context_used ""
2503 2507 proof_check_time "0.000"
0 0 VernacProof "tac:no using:no"
2737 2741 proof_build_time "0.000"
0 0 test_nonzeros "0.000"
2724 2736 context_used ""
2737 2741 proof_check_time "0.000"
0 0 VernacProof "tac:no using:no"
3010 3014 proof_build_time "0.000"
0 0 test_oddmembers "0.000"
2997 3009 context_used ""
3010 3014 proof_check_time "0.000"
0 0 VernacProof "tac:no using:no"
3189 3193 proof_build_time "0.000"
0 0 test_countoddmembers1 "0.000"
3176 3188 context_used ""
3189 3193 proof_check_time "0.000"
0 0 VernacProof "tac:no using:no"
3281 3285 proof_build_time "0.000"
0 0 test_countoddmembers2 "0.000"
3268 3280 context_used ""
3281 3285 proof_check_time "0.000"
0 0 VernacProof "tac:no using:no"
3369 3373 proof_build_time "0.000"
0 0 test_countoddmembers3 "0.000"
3356 3368 context_used ""
3369 3373 proof_check_time "0.000"
0 0 VernacProof "tac:no using:no"
3636 3640 proof_build_time "0.000"
0 0 test_alternate1 "0.000"
3623 3635 context_used ""
3636 3640 proof_check_time "0.000"
0 0 VernacProof "tac:no using:no"
3728 3732 proof_build_time "0.000"
0 0 test_alternate2 "0.000"
3715 3727 context_used ""
3728 3732 proof_check_time "0.000"
0 0 VernacProof "tac:no using:no"
3820 3824 proof_build_time "0.000"
0 0 test_alternate3 "0.000"
3807 3819 context_used ""
3820 3824 proof_check_time "0.000"
0 0 VernacProof "tac:no using:no"
3909 3913 proof_build_time "0.000"
0 0 test_alternate4 "0.000"
3896 3908 context_used ""
3909 3913 proof_check_time "0.000"
0 0 VernacProof "tac:no using:no"
4181 4185 proof_build_time "0.001"
0 0 test_count1 "0.001"
4168 4180 context_used ""
4181 4185 proof_check_time "0.000"
0 0 VernacProof "tac:no using:no"
4261 4265 proof_build_time "0.001"
0 0 test_count2 "0.001"
4248 4260 context_used ""
4261 4265 proof_check_time "0.000"
0 0 VernacProof "tac:no using:no"
4390 4394 proof_build_time "0.001"
0 0 test_sum1 "0.001"
4377 4389 context_used ""
4390 4394 proof_check_time "0.000"
0 0 VernacProof "tac:no using:no"
4519 4523 proof_build_time "0.000"
0 0 test_add1 "0.000"
4506 4518 context_used ""
4519 4523 proof_check_time "0.000"
0 0 VernacProof "tac:no using:no"
4599 4603 proof_build_time "0.000"
0 0 test_add2 "0.000"
4586 4598 context_used ""
4599 4603 proof_check_time "0.000"
0 0 VernacProof "tac:no using:no"
4838 4842 proof_build_time "0.000"
0 0 test_member1 "0.000"
4825 4837 context_used ""
4838 4842 proof_check_time "0.000"
0 0 VernacProof "tac:no using:no"
4922 4926 proof_build_time "0.000"
0 0 test_member2 "0.000"
4909 4921 context_used ""
4922 4926 proof_check_time "0.000"
0 0 VernacProof "tac:no using:no"
5191 5195 proof_build_time "0.001"
0 0 test_remove_one1 "0.001"
5178 5190 context_used ""
5191 5195 proof_check_time "0.000"
0 0 VernacProof "tac:no using:no"
5288 5292 proof_build_time "0.001"
0 0 test_remove_one2 "0.001"
5275 5287 context_used ""
5288 5292 proof_check_time "0.000"
0 0 VernacProof "tac:no using:no"
5389 5393 proof_build_time "0.001"
0 0 test_remove_one3 "0.001"
5376 5388 context_used ""
5389 5393 proof_check_time "0.000"
0 0 VernacProof "tac:no using:no"
5492 5496 proof_build_time "0.000"
0 0 test_remove_one4 "0.000"
5479 5491 context_used ""
5492 5496 proof_check_time "0.000"
0 0 VernacProof "tac:no using:no"
5772 5776 proof_build_time "0.001"
0 0 test_remove_all1 "0.001"
5759 5771 context_used ""
5772 5776 proof_check_time "0.000"
0 0 VernacProof "tac:no using:no"
5868 5872 proof_build_time "0.001"
0 0 test_remove_all2 "0.001"
5855 5867 context_used ""
5868 5872 proof_check_time "0.000"
0 0 VernacProof "tac:no using:no"
5968 5972 proof_build_time "0.001"
0 0 test_remove_all3 "0.001"
5955 5967 context_used ""
5968 5972 proof_check_time "0.000"
0 0 VernacProof "tac:no using:no"
6076 6080 proof_build_time "0.001"
0 0 test_remove_all4 "0.001"
6063 6075 context_used ""
6076 6080 proof_check_time "0.000"
0 0 VernacProof "tac:no using:no"
6354 6358 proof_build_time "0.000"
0 0 test_subset1 "0.000"
6341 6353 context_used ""
6354 6358 proof_check_time "0.000"
0 0 VernacProof "tac:no using:no"
6444 6448 proof_build_time "0.000"
0 0 test_subset2 "0.000"
6431 6443 context_used ""
6444 6448 proof_check_time "0.000"
0 0 VernacProof "tac:no using:no"
6677 6681 proof_build_time "0.001"
0 0 add_inc_count "0.001"
6664 6676 context_used ""
6677 6681 proof_check_time "0.000"
0 0 VernacProof "tac:no using:no"
6756 6760 proof_build_time "0.000"
0 0 nil_app "0.000"
6743 6755 context_used ""
6756 6760 proof_check_time "0.000"
0 0 VernacProof "tac:no using:no"
6955 6959 proof_build_time "0.000"
0 0 tl_length_pred "0.000"
6942 6954 context_used ""
6955 6959 proof_check_time "0.000"
0 0 VernacProof "tac:no using:no"
7179 7183 proof_build_time "0.001"
0 0 app_assoc "0.001"
7166 7178 context_used ""
7179 7183 proof_check_time "0.000"
0 0 VernacProof "tac:no using:no"
7349 7353 proof_build_time "0.000"
0 0 test_rev1 "0.000"
7336 7348 context_used ""
7349 7353 proof_check_time "0.000"
0 0 VernacProof "tac:no using:no"
7408 7412 proof_build_time "0.000"
0 0 test_rev2 "0.000"
7395 7407 context_used ""
7408 7412 proof_check_time "0.000"
0 0 VernacProof "tac:no using:no"
7635 7639 proof_build_time "0.001"
0 0 app_length "0.001"
7622 7634 context_used ""
7635 7639 proof_check_time "0.000"
0 0 VernacProof "tac:no using:no"
7912 7916 proof_build_time "0.002"
0 0 add_comm "0.002"
7899 7911 context_used ""
7912 7916 proof_check_time "0.000"
0 0 VernacProof "tac:no using:no"
8178 8182 proof_build_time "0.001"
0 0 rev_length_firsttry "0.001"
8165 8177 context_used ""
8178 8182 proof_check_time "0.000"
0 0 VernacProof "tac:no using:no"
8398 8402 proof_build_time "0.001"
0 0 app_nil_r "0.001"
8385 8397 context_used ""
8398 8402 proof_check_time "0.000"
0 0 VernacProof "tac:no using:no"
8814 8818 proof_build_time "0.004"
0 0 rev_app_distr "0.004"
8801 8813 context_used ""
8814 8818 proof_check_time "0.001"
0 0 VernacProof "tac:no using:no"
9040 9044 proof_build_time "0.001"
0 0 rev_involutive "0.001"
9027 9039 context_used ""
9040 9044 proof_check_time "0.000"
0 0 VernacProof "tac:no using:no"
9260 9264 proof_build_time "0.001"
0 0 app_assoc4 "0.001"
9247 9259 context_used ""
9260 9264 proof_check_time "0.000"
0 0 VernacProof "tac:no using:no"
9575 9579 proof_build_time "0.002"
0 0 nonzeros_app "0.002"
9562 9574 context_used ""
9575 9579 proof_check_time "0.000"
0 0 VernacProof "tac:no using:no"
9835 9839 proof_build_time "0.000"
0 0 test_eqblist1 "0.000"
9822 9834 context_used ""
9835 9839 proof_check_time "0.000"
0 0 VernacProof "tac:no using:no"
9920 9924 proof_build_time "0.000"
0 0 test_eqblist2 "0.000"
9907 9919 context_used ""
9920 9924 proof_check_time "0.000"
0 0 VernacProof "tac:no using:no"
10006 10010 proof_build_time "0.000"
0 0 test_eqblist3 "0.000"
9993 10005 context_used ""
10006 10010 proof_check_time "0.000"
0 0 VernacProof "tac:no using:no"
10358 10362 proof_build_time "0.002"
0 0 eqblist_refl "0.002"
10345 10357 context_used ""
10358 10362 proof_check_time "0.000"
0 0 VernacProof "tac:no using:no"
10493 10497 proof_build_time "0.000"
0 0 count_member_nonzero "0.000"
10480 10492 context_used ""
10493 10497 proof_check_time "0.000"
0 0 VernacProof "tac:no using:no"
10663 10667 proof_build_time "0.001"
0 0 leb_n_Sn "0.001"
10650 10662 context_used ""
10663 10667 proof_check_time "0.000"
0 0 VernacProof "tac:no using:no"
10985 10989 proof_build_time "0.002"
0 0 remove_does_not_increase_count "0.002"
10972 10984 context_used ""
10985 10989 proof_check_time "0.000"
0 0 VernacProof "tac:no using:no"
11232 11236 proof_build_time "0.001"
0 0 involution_injective "0.001"
11219 11231 context_used ""
11232 11236 proof_check_time "0.000"
0 0 VernacProof "tac:no using:no"
11438 11442 proof_build_time "0.001"
0 0 rev_injective "0.001"
11425 11437 context_used ""
11438 11442 proof_check_time "0.000"
0 0 VernacProof "tac:no using:no"
11813 11817 proof_build_time "0.000"
0 0 test_nth_error1 "0.000"
11800 11812 context_used ""
11813 11817 proof_check_time "0.000"
0 0 VernacProof "tac:no using:no"
11896 11900 proof_build_time "0.000"
0 0 test_nth_error2 "0.000"
11883 11895 context_used ""
11896 11900 proof_check_time "0.000"
0 0 VernacProof "tac:no using:no"
11977 11981 proof_build_time "0.000"
0 0 test_nth_error3 "0.000"
11964 11976 context_used ""
11977 11981 proof_check_time "0.000"
0 0 VernacProof "tac:no using:no"
12288 12292 proof_build_time "0.000"
0 0 test_hd_error1 "0.000"
12275 12287 context_used ""
12288 12292 proof_check_time "0.000"
0 0 VernacProof "tac:no using:no"
12362 12366 proof_build_time "0.000"
0 0 test_hd_error2 "0.000"
12349 12361 context_used ""
12362 12366 proof_check_time "0.000"
0 0 VernacProof "tac:no using:no"
12438 12442 proof_build_time "0.000"
0 0 test_hd_error3 "0.000"
12425 12437 context_used ""
12438 12442 proof_check_time "0.000"
0 0 VernacProof "tac:no using:no"
12659 12663 proof_build_time "0.001"
0 0 option_elim_hd "0.001"
12646 12658 context_used ""
12659 12663 proof_check_time "0.000"
0 0 VernacProof "tac:no using:no"
12986 12990 proof_build_time "0.001"
0 0 beq_id_refl "0.001"
12973 12985 context_used ""
12986 12990 proof_check_time "0.000"
0 0 VernacProof "tac:no using:no"
13603 13607 proof_build_time "0.001"
0 0 update_eq "0.001"
13589 13601 context_used ""
13603 13607 proof_check_time "0.000"
0 0 VernacProof "tac:no using:no"
13802 13806 proof_build_time "0.000"
0 0 update_neq "0.000"
13789 13801 context_used ""
13802 13806 proof_check_time "0.000"
0 0 vo_compile_time "0.198"