On Saturday, September 5, 2020 at 6:19:34 PM UTC-4 di.... gmail.com wrote: > The Metamath -> MM0 importer already contains a feature for selecting > which target theorems you want, so it has the same effect as using /extract > on the source database first and then importing it. I've been using numbers > for example theorems like dirith or pnt in my talks. I wonder what is the > maximum fraction of set.mm you can get by /extracting a single theorem...? >
I did this for all theorems in set.mm, and below are the 63 requiring > 8000 $p's. It looks like dirith uses the most in terms of $p count. I didn't save the extracted .mms, but re-running it on 3 of them, dirith.mm has 6994793 bytes, fouriersw.mm has 7026106 bytes, and pnt.mm has 5665034 bytes. For comparison, the current set.mm has 36616 $p, 2587 $a, and 39486525 bytes. BTW $a includes both |- and syntax statements, so the number of axioms and definitions is about half the $a count. 8019 $p 557 $a pntlemp 8024 $p 557 $a pntleml 8030 $p 620 $a dchrisum0flblem2 8032 $p 620 $a dchrisum0flb 8033 $p 559 $a areacirc 8041 $p 622 $a dchrmusum2 8049 $p 557 $a pnt3 8049 $p 596 $a meascnbl 8049 $p 600 $a coinflippvt 8051 $p 557 $a pnt2 8053 $p 557 $a pnt 8075 $p 596 $a omssubadd 8076 $p 560 $a etransclem23 8077 $p 616 $a dchrisum0lem2a 8080 $p 616 $a dchrisum0lem2 8114 $p 608 $a dstfrvclim1 8145 $p 624 $a dchrvmasumlem3 8149 $p 624 $a dchrvmasumiflem1 8172 $p 628 $a dchrisum0fno1 8187 $p 554 $a fourierdlem111 8237 $p 620 $a dchrisum0lem3 8244 $p 568 $a etransclem46 8248 $p 604 $a omsmeas 8271 $p 620 $a rpvmasumlem 8278 $p 552 $a fourierdlem103 8278 $p 552 $a fourierdlem104 8313 $p 562 $a stirling 8334 $p 564 $a stirlingr 8417 $p 554 $a fourierdlem112 8431 $p 630 $a dchrvmasumiflem2 8447 $p 640 $a dchrpt 8455 $p 574 $a etransclem47 8465 $p 554 $a fourierdlem113 8480 $p 554 $a fourierdlem114 8481 $p 554 $a fourierdlem115 8482 $p 554 $a fourierclimd 8482 $p 554 $a fourierd 8483 $p 554 $a fourier 8483 $p 554 $a fourierclim 8483 $p 554 $a fouriercnp 8484 $p 554 $a fouriercn 8486 $p 554 $a fourier2 8498 $p 632 $a dchrvmasumif 8517 $p 574 $a etransclem48 8542 $p 576 $a etransc 8563 $p 556 $a fouriersw 8595 $p 654 $a sumdchr2 8603 $p 654 $a dchrhash 8604 $p 654 $a sumdchr 8641 $p 658 $a sum2dchr 8653 $p 684 $a sitgaddlemb 9313 $p 678 $a rpvmasum2 9331 $p 678 $a dchrisum0re 9428 $p 682 $a dchrisum0 9429 $p 682 $a dchrisumn0 9429 $p 682 $a rpvmasum 9430 $p 682 $a dchrmusumlem 9430 $p 682 $a dchrvmasumlem 9431 $p 682 $a dchrmusum 9431 $p 682 $a dchrvmasum 9502 $p 684 $a rplogsum 9505 $p 684 $a dirith2 9506 $p 684 $a dirith Norm -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to metamath+unsubscr...@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/97201ab7-e740-46c4-8cac-e11e699f4a62n%40googlegroups.com.
