Hi Alexander, Thanks a lot for looking into this!
The test.shortening/train.shortening is a quite arbitrary split (shortenings coming from the training set vs the test set we use), both are to be considered. Best, -stan On Mon, Jul 6, 2020 at 12:40 PM 'Alexander van der Vekens' via Metamath <[email protected]> wrote: > > Hi Stan, > very interesing results. I had a look at the theorems I contributed in > test.shortening: > > ~reuan: Additional distinct variable condition! This shortening must not be > performed. > ~elmod2: This shortening is great! It should be done in set.mm > ~el2fzo: To be investigated if this theorem is still useful (or if its single > usage can be replaced by elfzolt3b found by the shortening). > > I had only a quick glance at train.shortening (what is it good for?) - it > seems to be a lot of good shortenings in there, too. > For ~suppss2f, however, the shortening is not allowed, because an OLD theorem > (suppss2OLD) is used for it. And the shortening of ~ subdir2d shows that it > is a duplicate of ~subdid. > > Regards, > Alexander > > > -- > 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/9f2536d7-d120-41e3-ba3d-9802270a9f69o%40googlegroups.com. -- 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/CACZd_0xhXcZDWbxmR2Fc1%2BqTPDV5TWriHbzWtrCH2afQ%3DACk9g%40mail.gmail.com.
