Hi all, Here are my remarks to the results of the minimizations:
> job115.log:Proof of "signswbase" decreased from 257 to 86 bytes using > "grpbase". Ok > job104.log:Proof of "gsumsn2" decreased from 351 to 45 bytes using "gsumsnd". It looks like my version was anterior to Alexander, but Alexander’s is more powerful. Anyway only one version shall be kept, as they are identical, so I suggest to remove gsumsn2. > job106.log:Proof of "gsumsndf" decreased from 351 to 29 bytes using > "gsumsnfd". The ‘f’ version replaces distinct variable restriction. Is the shortening legit? (Does it not reintroduce the distinct variables?) > job102.log:Proof of "ncolne2" decreased from 304 to 53 bytes using "ncolcom". I probably have proved ~ncolne2 when ~ncolcom did not exist yet. The minimization is legit, and maybe ~ncolne2 could be simplified out. > job102.log:Proof of "ifeq123d" decreased from 174 to 25 bytes using > "ifbieq12d". There is already a note from AV noting that ifeq123d shall be replaced by ifbieq12d > job107.log:Proof of "perpdrag" decreased from 420 to 36 bytes using > "perpdragALT". I think even though longer, the proof for perpdragALT was interesting (it does not require the extra set variable ‘x’) and I wanted to keep it. It shall have been marked “Proof modification discouraged” and “New usage discouraged”, though. BR, _ Thierry -- 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/F47AFC04-64C6-452F-A16A-917F299E40C6%40gmx.net.
