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/25cfa8fa-a786-45b3-a5e1-3a49ed1a058en%40googlegroups.com.
