Thanks, Alexander now I'm working on tooling, but as soon as I get back to set.mm with new proofs, I will certainly look into this list.
BR Glauco Il giorno domenica 4 dicembre 2022 alle 11:34:26 UTC+1 Alexander van der Vekens ha scritto: > 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/c6751e4e-98de-4d88-a479-8494716c16a6n%40googlegroups.com.
