On Saturday, February 15, 2020 at 12:28:58 AM UTC+1, David Starner wrote: > > On Fri, Feb 14, 2020 at 3:12 PM Norman Megill <[email protected] > <javascript:>> wrote: > > A simple way to fix this is to add "(Proof modification is > discouraged.)" to dral1ALT, etc. as they should have anyway. Then the > final 'minimize' run will skip them. There are also a number of > "suspicious" minimizations on non-ALT/OLD theorems as can be seen with > "grep 'to [12]. bytes' job*.log" e.g.: > > > > job102.log:Proof of "bj-abf" decreased from 45 to 12 bytes using "abf". > > job103.log:Proof of "hashssle" decreased from 370 to 19 bytes using > "hashss". > > > > When everything is done, we will need to analyze these and decide what > to do. > > That seems correct for hashssle; it takes a hypothesis in hashss 𝐴 ∈ > 𝑉 and turns it into 𝐴 ∈ Fin. > > Yes, ~hashssle is a specialization of ~hashss and could be replaced (and removed afterwards). ~hashssle (and ~bj-abf), however, are in mathboxes. In my opinion, the owners of the mathboxes should be responsible for cleaning up such cases. But it would be great if a list of such cases was created and provided after the global minimize action (to be used by the mathbox owners).
-- 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/b6ba0e3e-0f90-4ae3-9627-5d4cf9303727%40googlegroups.com.
