[Date Prev][Date Next]
[Chronological]
[Thread]
[Top]
RELITERS
Dear Sirs,
I have checked how many errors RELITERS enhancer reports in Mizar
Mathematical Library. RELITERS finds out superfluous steps in iterative
equalities. It only reports errors, does not remove.
The results are as follows:
NAME COUNT
1 ASYMPT_1 479
2 INT_3 370
3 SCMBSORT 363
4 SIN_COS 326
5 QUOFIELD 285
6 SCMISORT 277
7 GCD_1 268
8 SCPQSORT 257
9 BINOM 241
10 LATTICE5 238
11 YONEDA_1 223
12 SCMPDS_7 216
13 RELOC 190
14 BVFUNC_5 185
15 LATTICE8 173
16 GOBOARD6 170
17 SCMP_GCD 170
18 SCMFSA_9 163
19 JORDAN6 163
20 TOPREAL2 157
21 GRAPH_2 150
22 PRALG_3 148
23 SCMPDS_8 142
24 SCMFSA_5 139
25 IDEA_1 138
26 INTEGRA1 138
27 ANPROJ_2 137
28 SCMFSA7B 135
29 SCMFSA9A 135
30 BINARI_2 132
31 SCMPDS_6 118
32 MSSUBLAT 117
33 SCPISORT 116
34 SCMFSA_4 113
35 SCMFSA8C 109
36 GRAPH_4 109
37 SCMFSA6C 108
38 MATRLIN 107
39 JORDAN5C 105
40 JGRAPH_1 103
41 SCM_HALT 100
42 SCMPDS_4 100
43 SCMFSA_7 98
44 IDEAL_1 98
45 MSUALG_5 96
46 SCPINVAR 90
47 SCMPDS_5 88
48 GRSOLV_1 84
49 SCMPDS_2 84
50 JORDAN5B 83
51 SFMASTR3 83
52 POLYNOM1 83
53 FSM_1 82
54 WAYBEL18 81
55 GEOMTRAP 79
56 GOBRD12 78
57 HAHNBAN1 75
58 BVFUNC_4 72
59 SCMPDS_3 72
60 MSUALG_2 71
61 SCMFSA6B 69
62 GOBRD10 67
63 BORSUK_2 67
64 CONLAT_2 66
65 RLVECT_5 65
66 AMI_5 64
67 VECTSP_9 64
68 POLYNOM2 64
69 FUNCTOR1 63
70 POLYEQ_1 58
71 RADIX_1 56
72 TOPREAL1 55
73 WAYBEL_6 55
74 ABIAN 55
75 SCMFSA_2 54
76 TOPREAL6 54
77 SCMFSA_3 53
78 FF_SIEC 52
79 TREAL_1 50
80 RADIX_2 50
81 AXIOMS 48
82 CONLAT_1 48
83 CIRCUIT2 45
84 RFUNCT_3 44
85 PARSP_2 43
86 GOBOARD4 43
87 RLVECT_4 43
88 AUTGROUP 43
89 SCMFSA8B 43
90 MSUALG_4 42
91 SEQ_2 41
92 VECTSP_4 40
93 ANALMETR 39
94 BHSP_1 39
95 RMOD_2 38
96 HILBASIS 38
97 BHSP_4 37
98 SGRAPH1 37
99 GRAPH_3 37
100 YELLOW11 37
101 FDIFF_2 36
102 RFUNCT_4 35
103 CIRCUIT1 34
104 GOBOARD7 34
105 ANPROJ_1 33
106 MSUALG_3 33
107 SCMFSA6A 33
108 WAYBEL_1 33
109 BVFUNC_7 33
110 BVFUNC10 33
111 RLSUB_1 32
112 NORMSP_1 32
113 MSUHOM_1 31
114 SPPOL_2 31
115 COMSEQ_3 31
116 FRECHET 31
117 GROUP_1 30
118 L_HOSPIT 30
119 ORTSP_1 29
120 GROUP_7 29
121 TOPREAL5 28
122 TDGROUP 27
123 GR_CY_1 27
124 WAYBEL17 26
125 BVFUNC_3 26
126 GOBRD14 26
127 FDIFF_1 25
128 PRALG_2 25
129 MSALIMIT 25
130 SCMFSA8A 25
131 INTEGRA2 25
132 WAYBEL29 25
133 SYMSP_1 24
134 NORMFORM 24
135 QC_LANG4 24
136 JORDAN5A 24
137 VECTSP_1 23
138 ENDALG 23
139 FUNCTOR0 23
140 BVFUNC_6 23
141 ALGSTR_3 22
142 WAYBEL_5 22
143 WAYBEL11 22
144 BINARI_3 22
145 SFMASTR1 22
146 SERIES_1 21
147 TWOSCOMP 21
148 SPRECT_2 21
149 ANALOAF 20
150 GR_CY_2 20
151 BINARITH 20
152 PRE_CIRC 20
153 MSAFREE2 20
154 MSSUBFAM 20
155 COMSEQ_2 20
156 NEWTON 19
157 GOBOARD3 19
158 TOPRNS_1 19
159 ALTCAT_1 19
160 FINSEQ_6 19
161 URYSOHN1 19
162 SF_MASTR 19
163 WAYBEL_2 19
164 SFMASTR2 19
165 AMISTD_1 19
166 ALGSTR_2 18
167 HAHNBAN 18
168 COMSEQ_1 18
169 ALTCAT_3 18
170 CLOSURE3 18
171 JORDAN5D 18
172 WAYBEL24 18
173 INTEGRA4 18
174 HILBERT3 18
175 PAPDESAF 17
176 MSUALG_7 17
177 FUNCTOR3 17
178 WAYBEL28 17
179 FUNCSDOM 16
180 ANALORT 16
181 TSEP_1 16
182 TOPREAL3 16
183 FIB_FUSC 16
184 EXTENS_1 16
185 CLOSURE1 16
186 MSUALG_9 16
187 WAYBEL27 16
188 SEQ_1 15
189 RFUNCT_1 15
190 GROUP_4 15
191 MATRIX_3 15
192 ALTCAT_4 15
193 GENEALG1 15
194 RLVECT_2 14
195 VECTSP_2 14
196 MIDSP_2 14
197 FVSUM_1 14
198 KNASTER 14
199 WAYBEL_9 14
200 SUBSTLAT 14
201 WAYBEL20 14
202 AMISTD_2 14
203 ABSVALUE 13
204 FCONT_2 13
205 AFVECT0 13
206 GOBOARD2 13
207 UNIALG_3 13
208 CLOSURE2 13
209 T_1TOPSP 13
210 SCMPDS_1 13
211 WAYBEL25 13
212 METRIC_3 12
213 TSP_2 12
214 BIRKHOFF 12
215 BORSUK_3 12
216 BVFUNC15 12
217 BVFUNC22 12
218 RLSUB_2 11
219 MIDSP_1 11
220 VECTSP_5 11
221 ALG_1 11
222 MSUALG_1 11
223 MSAFREE1 11
224 GOBOARD9 11
225 FRECHET2 11
226 ALGSTR_1 10
227 TOPMETR 10
228 AMI_3 10
229 FUNCTOR2 10
230 NAT_2 10
231 WAYBEL22 10
232 VECTMETR 10
233 JORDAN8 10
234 CFCONT_1 10
235 COMPTRIG 10
236 SETWISEO 9
237 RMOD_3 9
238 RMOD_4 9
239 PRVECT_1 9
240 TSP_1 9
241 GOBOARD5 9
242 MSINST_1 9
243 YELLOW_5 9
244 EQUATION 9
245 WAYBEL15 9
246 CFUNCT_1 9
247 WAYBEL30 9
248 COMPLFLD 9
249 RLVECT_1 8
250 CARD_2 8
251 QC_LANG3 8
252 SETWOP_2 8
253 VECTSP_6 8
254 EUCLMETR 8
255 FDIFF_3 8
256 TMAP_1 8
257 AUTALG_1 8
258 FINSEQ_5 8
259 INDEX_1 8
260 SCMFSA_1 8
261 YELLOW_6 8
262 CARD_FIL 8
263 FINSOP_1 7
264 PROB_2 7
265 FCONT_1 7
266 METRIC_4 7
267 SEQFUNC 7
268 MOD_4 7
269 VFUNCT_1 7
270 PZFMISC1 7
271 WAYBEL16 7
272 REVROT_1 7
273 FINSEQ_1 6
274 VECTSP_7 6
275 SUPINF_2 6
276 MOD_2 6
277 REARRAN1 6
278 LOPCLSET 6
279 QUANTAL1 6
280 CQC_THE3 6
281 FUNCT_7 6
282 ALTCAT_2 6
283 MSUALG_8 6
284 YELLOW_3 6
285 SPRECT_1 6
286 YELLOW_9 6
287 FSCIRC_1 6
288 HILBERT2 6
289 ASYMPT_0 6
290 PENCIL_1 6
291 EXTREAL2 6
292 PRE_TOPC 5
293 TOPS_1 5
294 ROLLE 5
295 RLVECT_3 5
296 VECTSP_3 5
297 EUCLID 5
298 TOPMETR2 5
299 UNIALG_2 5
300 FACIRC_1 5
301 MSSCYC_1 5
302 WAYBEL_8 5
303 CATALG_1 5
304 BINTREE2 5
305 TOPGRP_1 5
306 JORDAN2C 5
307 YELLOW14 5
308 WAYBEL26 5
309 BVFUNC14 5
310 INTEGRA5 5
311 POLYNOM5 5
312 QC_LANG1 4
313 PARSP_1 4
314 FUNCT_4 4
315 METRIC_1 4
316 REAL_LAT 4
317 RPR_1 4
318 BHSP_2 4
319 TBSP_1 4
320 MOD_3 4
321 METRIC_6 4
322 MATRIX_2 4
323 LATTICE3 4
324 MIDSP_3 4
325 JORDAN1 4
326 FIN_TOPO 4
327 TOPS_3 4
328 BOOLMARK 4
329 MSAFREE 4
330 CAT_5 4
331 COHSP_1 4
332 CONNSP_3 4
333 YELLOW_4 4
334 JORDAN3 4
335 YELLOW_8 4
336 WAYBEL13 4
337 PSCOMP_1 4
338 JORDAN2B 4
339 ORDINAL2 3
340 RVSUM_1 3
341 CARD_4 3
342 HEINE 3
343 TSEP_2 3
344 LMOD_7 3
345 RFINSEQ 3
346 PRE_FF 3
347 MBOOLEAN 3
348 LATSUBGR 3
349 MSUALG_6 3
350 MSSCYC_2 3
351 SCMRING1 3
352 LATTICE6 3
353 YELLOW15 3
354 BVFUNC11 3
355 SCMRING3 3
356 POLYNOM4 3
357 SUBSET_1 2
358 ARYTM_1 2
359 FINSET_1 2
360 RECDEF_1 2
361 EQREL_1 2
362 ORDINAL4 2
363 TOLER_1 2
364 SUB_METR 2
365 METRIC_2 2
366 NAT_LAT 2
367 TDLAT_1 2
368 PCOMPS_2 2
369 AMI_2 2
370 MONOID_1 2
371 TRIANG_1 2
372 ORDERS_3 2
373 YELLOW_1 2
374 YELLOW_2 2
375 INSTALG1 2
376 WAYBEL12 2
377 WELLFND1 2
378 YELLOW12 2
379 YELLOW13 2
380 WAYBEL23 2
381 HEYTING2 2
382 JORDAN10 2
383 ALGSPEC1 2
384 BVFUNC20 2
385 WAYBEL31 2
386 WAYBEL32 2
387 FINTOPO2 2
388 ARYTM_2 1
389 FINSUB_1 1
390 CONNSP_1 1
391 ORDERS_2 1
392 FINSEQ_2 1
393 FINSEQ_3 1
394 FINSEQOP 1
395 GROUP_3 1
396 LIMFUNC1 1
397 MEASURE1 1
398 MOD_1 1
399 ALI2 1
400 BHSP_3 1
401 BORSUK_1 1
402 MEASURE3 1
403 TOPREAL4 1
404 AMI_1 1
405 MONOID_0 1
406 MEASURE5 1
407 TEX_1 1
408 DTCONSTR 1
409 FREEALG 1
410 SCM_COMP 1
411 TREES_9 1
412 WAYBEL14 1
413 YELLOW16 1
414 YELLOW17 1
415 ORDERS_4 1
416 JCT_MISC 1
417 CARD_LAR 1
418 EXTREAL1 1
419 MESFUNC2 1
Artur Kornilowicz