I had a look at Anthony's filtered list (218 entries), and I removed the theorems with the following name patterns (because they are definitive in mathboxes): wl-*, bj-*, rp-*, bnj*, *RP, frege* , axfrege* . Then 103 entries remain. In general, theorems of mathboxes should not be considered.
There are, however, duplicates in the mathboxes (mainly from GS): * fdmfifsupp, fidmfisupp (fidmfisupp in GS's mathbox, can be removed) * le2addd, leadd12dd (leadd12dd in GS's mathbox, can be removed) * fz0ssnn0, fzssnn0 (fzssnn0 in GS's mathbox, can be removed) * tendopl2, tendospdi2 (both in NM's mathbox, tendospdi2 could be removed) * mapss2, mapssbi (both in GS's mathbox, mapss2 could be removed) * fnfvimad, fnfvima2 (both in GS's mathbox, fnfvima2 could be removed) * climd, clim2d (both in GS's mathbox, clim2d could be removed) * volicorecl, volicore (both in GS's mathbox, volicore could be removed) Attached my reduced list, containing some comments (including the above listed comments). @Glauco: Maybe you can have a look at this list and find additional duplicates. Could you remove these, please? On Tuesday, August 30, 2022 at 3:55:23 PM UTC+2 [email protected] wrote: > On Tue, Aug 30, 2022 at 12:10 AM Benoit <[email protected]> wrote: > > That's a nice work. > > Thanks :-) > > > As for the big list, it would be interesting to have it. > > Please find the original unfiltered alt-mm output here > https://github.com/Antony74/alt-mm/blob/1cef09bc1976bd673d10ae76bdc872ff476b2fa1/set-mm-output.txt > And with the label filtering suggested by David here > https://github.com/Antony74/alt-mm/blob/master/set-mm-output.txt > > I don't know why I didn't think of committing the output to the git > repository before. If I make further improvements I should be able to keep > that output file in sync. > > Note: you wrote on the first line of your first post "proofs that are >> identical", but the proofs can differ: what you mean is that the statements >> are identical (more precisely, as you wrote later: the $f, $d, $e and $p >> statements of the associated frame). >> > > I think it's the bit where I said axioms, definitions, and proofs were > assertions, that I went wrong. A proof does contain an assertion but it > contains more than just that. We're only concerned here with the assertion > part. The concept of an assertion is just something I've picked up from > the checkmm source code, sorry if it's not proper terminology. > > > And probably not up to variable renaming ? > > No. Savask has got further with this question than me by considering > which sets of variables can be used interchangeably. Sounds like a > challenging problem to resolve programmatically (though easily guessed when > looking at an .mm file). After solving that I would probably just > re-assign variables alphabetically in order of appearance - imposing a > consistent ordering makes a test for equality trivial - except I think > that falls apart here because the hypotheses in which variables may appear > are themselves unordered. > > Best regards, > > Antony > -- 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 [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/cc08f9ee-7a44-464e-acc9-3539a2c8ba15n%40googlegroups.com.
a1ii, dummylink ax-mp, nic-stdmp, re1axmp, e0a ax-1, minimp-ax1, luklem5, tbw-ax2, retbwax2, re1tbw2, tb-ax2 ax-2, minimp-ax2, re1ax2 ax-3, con4, ax3h mp2, e00 id, id1 pm2.43, minimp-pm2.43, merlem11, luklem6, merco1lem9 imim2, luklem8 imim1, luk-1, nic-luk1, tbw-ax1, re1luk1, retbwax1, re1tbw1, re2luk1, tb-ax1, ax-luk1 pm2.04, luklem7, tbwlem1, re1ax2lem jarr, minimp-syllsimp, merco1lem4 pm2.21, axin2 pm2.24, luk-3, nic-luk3, re1luk3, re2luk3, ax-luk3 pm2.18, luk-2, nic-luk2, re1luk2, re2luk2, ax-luk2 pm2.01, axin1 peirce, tbw-ax3, retbwax3, re1tbw3, tb-ax3 pm3.2, axia3 simpl, axia1 simpr, axia2 intnanr, notatnand adantl3r, ad5ant1345, adantlllr jaob, axio nanbi1, nabi1 nanbi2, nabi2 falim, tbw-ax4, retbwax4, re1tbw4 nic-ax, renicax ax-4, alim, ax4fromc4 nfbiit, nfbii2 ax-6, ax6fromc10 equid, equid1 nfequid, nfequid-o alcomiw, ax11w ax6dgen, ax-9d1 nfa1, nfa1-o axc4, axc5c4c711toc4 axc7, axc5c7toc7, axc711toc7, axc5c711toc7, axc5c4c711toc7 axc16g, axc16g-o axc16, axc16b axc11n, axi10, axc11n11, axc11n11r, aecom-o, axc11nfromc11 aecoms, aecoms-o naecoms, naecoms-o hbnae, hbnae-o dral2, dral2-o dral1, dral1-o ax-ext, zfcndext eqid, eqid1 eqtrd, int-eqtransd ralimdaa, ralimda keepel, ifcli ax-rep, zfcndrep ax-pow, zfcndpow, grothpw vpwex, grothpwex zfpair, zfpair2 suctr, suctrALTcf fdmfifsupp, fidmfisupp (fidmfisupp in GS's mathbox, can be removed) hartogs, ondomon ax-reg, zfcndreg dominf, dominfac ax-ac, zfcndac cardeqv, grothac axcnex, cnex axaddcl, addcl axaddrcl, readdcl axmulcl, mulcl axmulrcl, remulcl axmulcom, mulcom axaddass, addass, cnncvsaddassdemo axmulass, mulass, cnncvsmulassdemo axdistr, adddi axlttrn, lttr addcom, cnaddcom le2addd, leadd12dd (leadd12dd in GS's mathbox, can be removed) 1div0, 1div0apr 1p1e2, 1p1e2apr1 nn0ind, nn0ind-raph fz0ssnn0, fzssnn0 (fzssnn0 in GS's mathbox, can be removed) absneg, cnncvsabsnegdemo 3lcm2e6woprm, 3lcm2e6 prmgap, prmgaplcm, prmgapprmo iblabslem, iblabsnclem cniccibl, cnicciblnc ftc2, ftc2nc (ftc2nc in BL's mathbox, should be renamed ftc2ALT) ex-natded5.13, ex-natded5.13-2 ex-natded9.20, ex-natded9.20-2 ex-natded9.26, ex-natded9.26-2 omlsi, pjomli pjpj0i, pjpji chjassi, qlax3i pjcompi, pjvi abrexdomjm, abrexdom abrexdom2jm, abrexdom2 tgoldbachgt, ax-tgoldbachgt (in TA's and AV's mathboxs) axc11n-16, axc11next (both in ATS's mathbox) tendopl2, tendospdi2 (both in NM's mathbox, tendospdi2 could be removed) rntrclfvOAI, rntrclfv (in OpenAI's and RP's mathboxs) sspwimp, sspwimpcf (both in AS's mathbox) restuni3, restuni6 (both in GS's mathbox, restuni6 has a much shorter proof) mapss2, mapssbi (both in GS's mathbox, mapss2 could be removed) fnfvimad, fnfvima2 (both in GS's mathbox, fnfvima2 could be removed) climd, clim2d (both in GS's mathbox, clim2d could be removed) volicorecl, volicore (both in GS's mathbox, volicore could be removed) atbiffatnnb, atbiffatnnbalt (both in JU's mathbox, atbiffatnnbalt should be renamed atbiffatnnbALT)
