scripts/min.cmd is due to Norm. My modifications were very minor. Indeed it is very useful. Benoît
On Thursday, September 9, 2021 at 7:30:17 PM UTC+2 Alexander van der Vekens wrote: > Using Benoît's Minimize-Script scripts/min.cmd, I checked all 2743 proofs > using fvex, and 447 of them can be minimized (by 2-10 bytes) by using > fvexd. Therefore, Glauco's assumption that many proofs become shorter is > true. > > On Wednesday, September 8, 2021 at 1:58:31 PM UTC+2 ookami wrote: > >> Norm once told me (several years ago!) that the threshold value is 7 >> theorems: If the introduction of a convenience theorem affects this many or >> more theorems, its value outperforms the downside of having more theorems.. >> >> Wolf Lammen >> [email protected] schrieb am Montag, 6. September 2021 um 01:12:20 UTC+2: >> >>> As with things like 1cnd I think it is a matter of whether the >>> convenience theorem would get used enough times to justify having it. >>> On 9/5/21 7:22 AM, Glauco wrote: >>> >>> A theorem like >>> >>> |- ( ph -> ( F ` A ) e. _V ) >>> >>> would clearly be "redundant". >>> >>> But it would save a LOT of a1i (and shorten many proofs, I guess) >>> >>> And the autocomplete feature of mmj2 would take advantage of it (as far >>> as I can tell, the current version doesn't add an a1i automagically). >>> >>> Comments? >>> >>> >>> >>> -- >>> 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/756da4ff-316a-4861-bbaf-b100e108cdc8n%40googlegroups.com >>> >>> <https://groups.google.com/d/msgid/metamath/756da4ff-316a-4861-bbaf-b100e108cdc8n%40googlegroups.com?utm_medium=email&utm_source=footer> >>> . >>> >>> -- 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/a1d38ee4-f896-474b-993d-25385f80152cn%40googlegroups.com.
