On Wednesday, September 8, 2021 at 7:58:31 AM UTC-4 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..
That was a rough and probably outdated rule of thumb I sometimes used decades ago, especially early in set.mm development when I thought that 5 to 10 uses was an indication that the convenience theorem might be used more widely in the future. But as far as achieving a net shortening of set.mm, it depends on how many steps the new theorem saves in each proof. If it replaces a large section in the target proofs, as few as 2 or 3 uses could pay off. A convenience theorem saving one a1i step like this one may require dozens of uses. It is probably reasonable to expect that 447 uses would shorten set.mm. The only accurate way to find out is to do trial minimizations then keep or abandon the convenience theorem based whether there is a net size reduction. Since much of it can be done with scripts, it's usually not too time-consuming to do that, and I've done it quite often myself. 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/274eb227-98fe-48f7-a8aa-e0bfc30087e9n%40googlegroups.com.
