Hi Norm, I had a look at the first two blocks. See my remarks/recommendations below.
Alexander On Friday, February 21, 2020 at 4:28:24 AM UTC+1, Norman Megill wrote: > > > $ grep '[0-9]... to [1-3].. bytes' job*.log | uniq > job128.log:Proof of "fprodshft" decreased from 1054 to 209 bytes using > "mptfzshft". > ~frprodshft (contributed in Jan 2018, used 2 times) is in SF's mathbox, ~mptfzshft (contributed in Aug 2019) is in main set. I think both should be kept, shortening proof of frprodshft (will still have 13 essential lines) should be OK. > $ grep '[2-9].. to [4-9]. bytes' job*.log | uniq > job102.log:Proof of "ncolne2" decreased from 304 to 53 bytes using > "ncolcom". > Both contibuted by TA, he should decide (From my point of view shortening is OK) job104.log:Proof of "gsumsn2" decreased from 351 to 45 bytes using > "gsumsnd". > ~gsumsn2 (contributed in Jan 2017, used only once) is in TA's mathbox, ~gsumsnd (contributed in Jan 2019) is in main set. I think ~gsumsn2 could be deleted, replaced by ~gsumsnd in proof of ~esumsn. Maybe the tags for ~gsumsnd could be changed to "(Contributed by TA, 30-Jan-2017.) (Proof shortened by AV, 11-Dec-2019.) $)" after the deletion of ~gsumsn. job109.log:Proof of "fz0hash" decreased from 207 to 98 bytes using > "hashfz0". > ~fz0hash(contributed in Jun 2018, used 3 times) and ~hashfz0 (contributed in Jul 2018) both in main set. I think both should be kept, shortening proof of ~fz0hash is OK. job115.log:Proof of "signswbase" decreased from 257 to 86 bytes using > "grpbase". > ~signswbase (contributed in Sep 2018, used 6 times) is in TA's mathbox, ~grpbase (contributed in Aug 2013) is in main set. I think both should be kept, shortening proof of ~signswbase is OK. > job132.log:Proof of "euhash1" decreased from 514 to 93 bytes using > "hashen1". > ~euhash1 (contributed in Feb 2018, used only once) and ~hashen1 (contributed in Apr 2019) both in main set. I think both should be kept, shortening proof of ~euhash1 is OK. job154.log:Proof of "fourierdlem45" decreased from 5709 to 53 bytes using > "ioodvbdlimc1lem > ~fourierdlem45 (contributed in Dec 2019, not used!), ~ioodvbdlimc1lem does not exist (cut off at the end?), only ~ioodvbdlimc1lem1 and ~ioodvbdlimc1lem2 all in GS's mathbox. I think ~fourierdlem45 ciuld be deleted (but GS has to decide). -- 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/a30c379b-6884-4586-872d-512d826573a3%40googlegroups.com.
