I would suggest that you run the minimizations on your pieces (calling them say job160a, job160b, job160c for mideulem). Before my final minimize run I will use your logs from these 3 new jobs to extract the minimizations, after you do a PR for the break down. Since all other jobs are using a fixed set.mm, there should be no conflict with them. (I would still like to see the run times for the original 159 (David W.) and 160 (Mario) if they ever complete.)
Norm On Sunday, February 16, 2020 at 5:30:51 AM UTC-5, Thierry Arnoux wrote: > > Hi Norm, > > How do I best submit the change to break down those theorems/lemma? > I may be able to provide something for ~mideulem soon, breaking it into 3. > > BR, > _ > Thierry > > -- 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/a8a1dc2a-5d86-413b-838f-1f98b48cd9d5%40googlegroups.com.
