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.
