-
Notifications
You must be signed in to change notification settings - Fork 0
/
.c2.aux
219 lines (219 loc) · 6.61 KB
/
.c2.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
COQAUX1 535dad38bb5b55770ddfcbf821f86cce /usr/gaodc/coq_learn/c2.v
0 0 VernacProof "tac:no using:no"
227 231 proof_build_time "0.001"
0 0 add_0_r_firsttry "0.001"
214 226 context_used ""
227 231 proof_check_time "0.000"
0 0 VernacProof "tac:no using:no"
463 467 proof_build_time "0.001"
0 0 minus_n_n "0.001"
450 462 context_used ""
463 467 proof_check_time "0.000"
0 0 VernacProof "tac:no using:no"
629 633 proof_build_time "0.001"
0 0 mul_0_r "0.001"
616 628 context_used ""
629 633 proof_check_time "0.000"
0 0 VernacProof "tac:no using:no"
816 820 proof_build_time "0.001"
0 0 plus_n_Sm "0.001"
803 815 context_used ""
816 820 proof_check_time "0.000"
0 0 VernacProof "tac:no using:no"
1093 1097 proof_build_time "0.002"
0 0 add_comm "0.002"
1080 1092 context_used ""
1093 1097 proof_check_time "0.000"
0 0 VernacProof "tac:no using:no"
1285 1289 proof_build_time "0.001"
0 0 add_assoc "0.001"
1283 1284 context_used ""
1285 1289 proof_check_time "0.000"
0 0 VernacProof "tac:no using:no"
1582 1586 proof_build_time "0.001"
0 0 double_plus "0.001"
1580 1581 context_used ""
1582 1586 proof_check_time "0.000"
0 0 VernacProof "tac:no using:no"
1770 1774 proof_build_time "0.001"
0 0 eqb_refl "0.001"
1768 1769 context_used ""
1770 1774 proof_check_time "0.000"
0 0 VernacProof "tac:no using:no"
1911 1915 proof_build_time "0.001"
0 0 negbb "0.001"
1898 1910 context_used ""
1911 1915 proof_check_time "0.000"
0 0 VernacProof "tac:no using:no"
2110 2114 proof_build_time "0.001"
0 0 even_S "0.001"
2108 2109 context_used ""
2110 2114 proof_check_time "0.000"
0 0 VernacProof "tac:no using:no"
2326 2330 proof_build_time "0.001"
0 0 mult_0_plus' "0.001"
2313 2325 context_used ""
2326 2330 proof_check_time "0.000"
0 0 VernacProof "tac:no using:no"
2629 2635 proof_build_time "0.000"
2629 2635 proof_check_time "0.000"
0 0 VernacProof "tac:no using:no"
2878 2882 proof_build_time "0.001"
0 0 add_shuffle3 "0.001"
2865 2877 context_used ""
2878 2882 proof_check_time "0.000"
0 0 VernacProof "tac:no using:no"
3086 3090 proof_build_time "0.001"
0 0 mul_n_m_1 "0.001"
3073 3085 context_used ""
3086 3090 proof_check_time "0.000"
0 0 VernacProof "tac:no using:no"
3301 3305 proof_build_time "0.001"
0 0 mul_comm "0.001"
3288 3300 context_used ""
3301 3305 proof_check_time "0.000"
0 0 VernacProof "tac:no using:no"
3566 3570 proof_build_time "0.001"
0 0 plus_leb_compat_l "0.001"
3553 3565 context_used ""
3566 3570 proof_check_time "0.000"
0 0 VernacProof "tac:no using:no"
3778 3782 proof_build_time "0.001"
0 0 leb_refl "0.001"
3763 3775 context_used ""
3778 3782 proof_check_time "0.000"
0 0 VernacProof "tac:no using:no"
3935 3939 proof_build_time "0.000"
0 0 zero_neqb_S "0.000"
3922 3934 context_used ""
3935 3939 proof_check_time "0.000"
0 0 VernacProof "tac:no using:no"
4125 4129 proof_build_time "0.001"
0 0 zero_neqb_S' "0.001"
4111 4123 context_used ""
4125 4129 proof_check_time "0.000"
0 0 VernacProof "tac:no using:no"
4346 4350 proof_build_time "0.001"
0 0 zero_neqb_S'' "0.001"
4332 4344 context_used ""
4346 4350 proof_check_time "0.000"
0 0 VernacProof "tac:no using:no"
4537 4541 proof_build_time "0.000"
0 0 andb_false_r "0.000"
4524 4536 context_used ""
4537 4541 proof_check_time "0.000"
0 0 VernacProof "tac:no using:no"
4662 4666 proof_build_time "0.000"
0 0 S_neqb_0 "0.000"
4649 4661 context_used ""
4662 4666 proof_check_time "0.000"
0 0 VernacProof "tac:no using:no"
4824 4828 proof_build_time "0.000"
0 0 S_neqb_0' "0.000"
4811 4823 context_used ""
4824 4828 proof_check_time "0.000"
0 0 VernacProof "tac:no using:no"
5013 5017 proof_build_time "0.001"
0 0 S_neqb_0'' "0.001"
5000 5012 context_used ""
5013 5017 proof_check_time "0.000"
0 0 VernacProof "tac:no using:no"
5150 5154 proof_build_time "0.001"
0 0 mult_1_l "0.001"
5137 5149 context_used ""
5150 5154 proof_check_time "0.000"
0 0 VernacProof "tac:no using:no"
5328 5332 proof_build_time "0.001"
0 0 mult_1_l' "0.001"
5315 5327 context_used ""
5328 5332 proof_check_time "0.000"
0 0 VernacProof "tac:no using:no"
5544 5548 proof_build_time "0.001"
0 0 mult_1_l'' "0.001"
5531 5543 context_used ""
5544 5548 proof_check_time "0.000"
0 0 VernacProof "tac:no using:no"
5776 5780 proof_build_time "0.001"
0 0 all3_spec "0.001"
5763 5775 context_used ""
5776 5780 proof_check_time "0.000"
0 0 VernacProof "tac:no using:no"
6030 6034 proof_build_time "0.001"
0 0 mult_plus_distr_r "0.001"
6028 6029 context_used ""
6030 6034 proof_check_time "0.000"
0 0 VernacProof "tac:no using:no"
6260 6264 proof_build_time "0.001"
0 0 mult_assoc "0.001"
6247 6259 context_used ""
6260 6264 proof_check_time "0.000"
0 0 VernacProof "tac:no using:no"
6508 6512 proof_build_time "0.001"
0 0 add_shuffle3' "0.001"
6495 6507 context_used ""
6508 6512 proof_check_time "0.000"
0 0 VernacProof "tac:no using:no"
7215 7219 proof_build_time "0.002"
0 0 bin_to_nat_pres_incr "0.002"
7202 7214 context_used ""
7215 7219 proof_check_time "0.001"
0 0 VernacProof "tac:no using:no"
7568 7572 proof_build_time "0.001"
0 0 nat_bin_nat "0.001"
7555 7567 context_used ""
7568 7572 proof_check_time "0.000"
0 0 VernacProof "tac:no using:no"
7750 7754 proof_build_time "0.001"
0 0 double_incr "0.001"
7737 7749 context_used ""
7750 7754 proof_check_time "0.000"
0 0 VernacProof "tac:no using:no"
8112 8116 proof_build_time "0.001"
0 0 double_incr_bin "0.001"
8099 8111 context_used ""
8112 8116 proof_check_time "0.000"
0 0 VernacProof "tac:no using:no"
8361 8365 proof_build_time "0.000"
0 0 normalize_1 "0.000"
8348 8360 context_used ""
8361 8365 proof_check_time "0.000"
0 0 VernacProof "tac:no using:no"
8454 8458 proof_build_time "0.000"
0 0 normalize_2 "0.000"
8441 8453 context_used ""
8454 8458 proof_check_time "0.000"
0 0 VernacProof "tac:no using:no"
8646 8650 proof_build_time "0.001"
0 0 B1_incr "0.001"
8633 8645 context_used ""
8646 8650 proof_check_time "0.000"
0 0 VernacProof "tac:no using:no"
9141 9145 proof_build_time "0.004"
0 0 nat_twice_plus_one "0.004"
9137 9138 context_used ""
9141 9145 proof_check_time "0.001"
0 0 VernacProof "tac:no using:no"
9483 9487 proof_build_time "0.002"
0 0 nat_twice_plus_one' "0.002"
9469 9481 context_used ""
9483 9487 proof_check_time "0.000"
0 0 VernacProof "tac:no using:no"
9579 9588 proof_build_time "0.000"
0 0 normalize_incr "0.000"
9579 9588 proof_check_time "0.000"
0 0 VernacProof "tac:no using:no"
9894 9898 proof_build_time "0.002"
0 0 L1 "0.002"
9881 9893 context_used ""
9894 9898 proof_check_time "0.000"
0 0 VernacProof "tac:no using:no"
10156 10160 proof_build_time "0.001"
0 0 L2 "0.001"
10143 10155 context_used ""
10156 10160 proof_check_time "0.000"
0 0 VernacProof "tac:no using:no"
10516 10520 proof_build_time "0.003"
0 0 bin_nat_bin "0.003"
10503 10515 context_used ""
10516 10520 proof_check_time "0.000"
0 0 vo_compile_time "0.069"