On Friday, February 14, 2020 at 6:28:58 PM UTC-5, David Starner wrote: > > On Fri, Feb 14, 2020 at 3:12 PM Norman Megill 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, it is correct, but we normally don't have 1-step proofs for substitution instances because it wastes set.mm file space. This is telling us we should delete hashssle and use hashss instead. > > > Unfortunately these jobs will have to be rerun. The theorems in > job133.cmd through job160.cmd were not changed so those runs shou OK. > > Does that mean that 125-132 are open again? Since 155 hasn't started > running backwards yet, I might as well load up the rest of those > cores. > Let's see what David W. wants to do. Also, this might affect anyone who used the script, so there might be other jobs to be redone. 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/1d9ed0d9-012e-4894-9d27-4d74fd1eddaf%40googlegroups.com.
