-
Notifications
You must be signed in to change notification settings - Fork 0
/
.Basics.aux
284 lines (284 loc) · 8.89 KB
/
.Basics.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
COQAUX1 3d2cfd7ed27ef1b132dde0a8fac82cde /Users/antonio/Desktop/tmp/coc/Basics.v
0 0 VernacProof "tac:no using:no"
933 937 proof_build_time "0.003"
0 0 test_next_weekday "0.003"
919 931 context_used ""
933 937 proof_check_time "0.001"
0 0 VernacProof "tac:no using:no"
2361 2365 proof_build_time "0.001"
0 0 test_orb1 "0.001"
2347 2359 context_used ""
2361 2365 proof_check_time "0.000"
0 0 VernacProof "tac:no using:no"
2441 2445 proof_build_time "0.001"
0 0 test_orb2 "0.001"
2427 2439 context_used ""
2441 2445 proof_check_time "0.000"
0 0 VernacProof "tac:no using:no"
2520 2524 proof_build_time "0.001"
0 0 test_orb3 "0.001"
2506 2518 context_used ""
2520 2524 proof_check_time "0.000"
0 0 VernacProof "tac:no using:no"
2599 2603 proof_build_time "0.001"
0 0 test_orb4 "0.001"
2585 2597 context_used ""
2599 2603 proof_check_time "0.000"
0 0 VernacProof "tac:no using:no"
2950 2954 proof_build_time "0.001"
0 0 test_orb5 "0.001"
2937 2949 context_used ""
2950 2954 proof_check_time "0.000"
0 0 VernacProof "tac:no using:no"
4096 4100 proof_build_time "0.001"
0 0 test_nandb1 "0.001"
4083 4095 context_used ""
4096 4100 proof_check_time "0.001"
0 0 VernacProof "tac:no using:no"
4191 4195 proof_build_time "0.002"
0 0 test_nandb2 "0.002"
4178 4190 context_used ""
4191 4195 proof_check_time "0.000"
0 0 VernacProof "tac:no using:no"
4285 4289 proof_build_time "0.001"
0 0 test_nandb3 "0.001"
4272 4284 context_used ""
4285 4289 proof_check_time "0.000"
0 0 VernacProof "tac:no using:no"
4379 4383 proof_build_time "0.001"
0 0 test_nandb4 "0.001"
4366 4378 context_used ""
4379 4383 proof_check_time "0.000"
0 0 VernacProof "tac:no using:no"
4712 4716 proof_build_time "0.001"
0 0 test_andb31 "0.001"
4699 4711 context_used ""
4712 4716 proof_check_time "0.000"
0 0 VernacProof "tac:no using:no"
4814 4818 proof_build_time "0.001"
0 0 test_andb32 "0.001"
4801 4813 context_used ""
4814 4818 proof_check_time "0.000"
0 0 VernacProof "tac:no using:no"
4916 4920 proof_build_time "0.001"
0 0 test_andb33 "0.001"
4903 4915 context_used ""
4916 4920 proof_check_time "0.001"
0 0 VernacProof "tac:no using:no"
5018 5022 proof_build_time "0.001"
0 0 test_andb34 "0.001"
5005 5017 context_used ""
5018 5022 proof_check_time "0.000"
0 0 VernacProof "tac:no using:no"
8370 8374 proof_build_time "0.001"
0 0 test_monochrome "0.001"
8357 8369 context_used ""
8370 8374 proof_check_time "0.000"
0 0 VernacProof "tac:no using:no"
11888 11892 proof_build_time "0.002"
0 0 test_oddb1 "0.002"
11875 11887 context_used ""
11888 11892 proof_check_time "0.001"
0 0 VernacProof "tac:no using:no"
11956 11960 proof_build_time "0.002"
0 0 test_oddb2 "0.002"
11943 11955 context_used ""
11956 11960 proof_check_time "0.001"
0 0 VernacProof "tac:no using:no"
12785 12789 proof_build_time "0.002"
0 0 test_mult1 "0.002"
12772 12784 context_used ""
12785 12789 proof_check_time "0.001"
0 0 VernacProof "tac:no using:no"
13195 13199 proof_build_time "0.013"
0 0 test_exp1 "0.013"
13182 13194 context_used ""
13195 13199 proof_check_time "0.001"
0 0 VernacProof "tac:no using:no"
13594 13598 proof_build_time "0.004"
0 0 test_factorial1 "0.004"
13581 13593 context_used ""
13594 13598 proof_check_time "0.001"
0 0 VernacProof "tac:no using:no"
13672 13676 proof_build_time "0.072"
0 0 test_factorial2 "0.072"
13659 13671 context_used ""
13672 13676 proof_check_time "0.005"
0 0 VernacProof "tac:no using:no"
13752 13756 proof_build_time "0.004"
0 0 test_factorial3 "0.004"
13739 13751 context_used ""
13752 13756 proof_check_time "0.005"
0 0 VernacProof "tac:no using:no"
14739 14743 proof_build_time "0.001"
0 0 test_eqb1 "0.001"
14726 14738 context_used ""
14739 14743 proof_check_time "0.001"
0 0 VernacProof "tac:no using:no"
14809 14813 proof_build_time "0.001"
0 0 test_eqb2 "0.001"
14796 14808 context_used ""
14809 14813 proof_check_time "0.001"
0 0 VernacProof "tac:no using:no"
15159 15163 proof_build_time "0.001"
0 0 test_leb1 "0.001"
15146 15158 context_used ""
15159 15163 proof_check_time "0.000"
0 0 VernacProof "tac:no using:no"
15228 15232 proof_build_time "0.001"
0 0 test_leb2 "0.001"
15215 15227 context_used ""
15228 15232 proof_check_time "0.000"
0 0 VernacProof "tac:no using:no"
15310 15314 proof_build_time "0.001"
0 0 test_leb3 "0.001"
15297 15309 context_used ""
15310 15314 proof_check_time "0.001"
0 0 VernacProof "tac:no using:no"
15393 15397 proof_build_time "0.001"
0 0 test_leb4 "0.001"
15380 15392 context_used ""
15393 15397 proof_check_time "0.001"
0 0 VernacProof "tac:no using:no"
15675 15679 proof_build_time "0.001"
0 0 test_leb5 "0.001"
15662 15674 context_used ""
15675 15679 proof_check_time "0.000"
0 0 VernacProof "tac:no using:no"
16551 16555 proof_build_time "0.001"
0 0 test_ltb1 "0.001"
16538 16550 context_used ""
16551 16555 proof_check_time "0.000"
0 0 VernacProof "tac:no using:no"
16620 16624 proof_build_time "0.001"
0 0 test_ltb2 "0.001"
16607 16619 context_used ""
16620 16624 proof_check_time "0.001"
0 0 VernacProof "tac:no using:no"
16689 16693 proof_build_time "0.003"
0 0 test_ltb3 "0.003"
16676 16688 context_used ""
16689 16693 proof_check_time "0.001"
0 0 VernacProof "tac:no using:no"
16883 16887 proof_build_time "0.004"
0 0 plus_0_n "0.004"
16870 16882 context_used ""
16883 16887 proof_check_time "0.001"
0 0 VernacProof "tac:no using:no"
17226 17230 proof_build_time "0.002"
0 0 plus_O_n' "0.002"
17213 17225 context_used ""
17226 17230 proof_check_time "0.001"
0 0 VernacProof "tac:no using:no"
18614 18618 proof_build_time "0.001"
0 0 plus_O_n'' "0.001"
18601 18613 context_used ""
18614 18618 proof_check_time "0.000"
0 0 VernacProof "tac:no using:no"
19093 19097 proof_build_time "0.002"
0 0 plus_1_1 "0.002"
19080 19092 context_used ""
19093 19097 proof_check_time "0.000"
0 0 VernacProof "tac:no using:no"
19180 19184 proof_build_time "0.001"
0 0 mult_O_1 "0.001"
19167 19179 context_used ""
19180 19184 proof_check_time "0.000"
0 0 VernacProof "tac:no using:no"
20863 20867 proof_build_time "0.003"
0 0 plus_id_example "0.003"
20850 20862 context_used ""
20863 20867 proof_check_time "0.001"
0 0 VernacProof "tac:no using:no"
21934 21938 proof_build_time "0.003"
0 0 plus_id_exercise "0.003"
21921 21933 context_used ""
21934 21938 proof_check_time "0.001"
0 0 VernacProof "tac:no using:no"
22267 22271 proof_build_time "0.003"
0 0 mult_n_0_m_0 "0.003"
22254 22266 context_used ""
22267 22271 proof_check_time "0.001"
0 0 VernacProof "tac:no using:no"
22518 22527 proof_build_time "0.000"
0 0 mult_n_1 "0.000"
22518 22527 proof_check_time "0.000"
0 0 VernacProof "tac:no using:no"
22651 22655 proof_build_time "0.002"
0 0 mult_0_plus "0.002"
22636 22648 context_used ""
22651 22655 proof_check_time "0.000"
0 0 VernacProof "tac:no using:no"
22863 22867 proof_build_time "0.002"
0 0 mult_S_1 "0.002"
22850 22862 context_used ""
22863 22867 proof_check_time "0.002"
0 0 VernacProof "tac:no using:no"
23478 23484 proof_build_time "0.001"
23478 23484 proof_check_time "0.000"
0 0 VernacProof "tac:no using:no"
24512 24516 proof_build_time "0.004"
0 0 plus_1_neq_0 "0.004"
24499 24511 context_used ""
24512 24516 proof_check_time "0.001"
0 0 VernacProof "tac:no using:no"
28009 28013 proof_build_time "0.005"
0 0 negb_involutive "0.005"
27996 28008 context_used ""
28009 28013 proof_check_time "0.001"
0 0 VernacProof "tac:no using:no"
28903 28907 proof_build_time "0.009"
0 0 andb_commutative "0.009"
28890 28902 context_used ""
28903 28907 proof_check_time "0.001"
0 0 VernacProof "tac:no using:no"
29500 29504 proof_build_time "0.016"
0 0 andb_commutative' "0.016"
29498 29499 context_used ""
29500 29504 proof_check_time "0.002"
0 0 VernacProof "tac:no using:no"
30001 30005 proof_build_time "0.019"
0 0 andb3_exchange "0.019"
29999 30000 context_used ""
30001 30005 proof_check_time "0.005"
0 0 VernacProof "tac:no using:no"
30278 30282 proof_build_time "0.011"
0 0 andb_commutative'' "0.011"
30265 30277 context_used ""
30278 30282 proof_check_time "0.005"
0 0 VernacProof "tac:no using:no"
30429 30433 proof_build_time "0.006"
0 0 zero_neq_plus_1 "0.006"
30416 30428 context_used ""
30429 30433 proof_check_time "0.001"
0 0 VernacProof "tac:no using:no"
34097 34101 proof_build_time "0.003"
0 0 identity_fn_applied_twice "0.003"
34084 34096 context_used ""
34097 34101 proof_check_time "0.001"
0 0 VernacProof "tac:no using:no"
34544 34548 proof_build_time "0.004"
0 0 negation_fn_applied_twice "0.004"
34531 34543 context_used ""
34544 34548 proof_check_time "0.001"
0 0 VernacProof "tac:no using:no"
35080 35084 proof_build_time "0.006"
0 0 andb_eq_orb "0.006"
35067 35079 context_used ""
35080 35084 proof_check_time "0.002"
0 0 VernacProof "tac:no using:no"
36695 36699 proof_build_time "0.001"
0 0 test_bin_incr1 "0.001"
36682 36694 context_used ""
36695 36699 proof_check_time "0.000"
0 0 VernacProof "tac:no using:no"
36785 36789 proof_build_time "0.001"
0 0 test_bin_incr2 "0.001"
36772 36784 context_used ""
36785 36789 proof_check_time "0.000"
0 0 VernacProof "tac:no using:no"
36880 36884 proof_build_time "0.001"
0 0 test_bin_incr3 "0.001"
36867 36879 context_used ""
36880 36884 proof_check_time "0.000"
0 0 vo_compile_time "1.018"