On Saturday, February 22, 2020 at 9:27:56 PM UTC+1, Norman Megill wrote: > > Thank you, Alexander and Glauco. I'd like to hear from Benoit and Wolf > who have a number of theorems in these lists. After that I'll organize it > into the final list of actions we'll take. (I will probably do the > necessary editing of set.mm myself to prevent confusion or conflict.) > > Here are some more ALT cases (with duplicates removed): > > $ grep 'using ".*ALT"' j*g > job116.log:Proof of "climf" decreased from 873 to 872 bytes using > "rexbidvALT". <- use rexbidv instead >
"rexbidvALT" is only used in the backward scan, but the result of the forward scan is used. Therefore, I think that there is nothing to to here. job147.log:Proof of "fourierdlem65" decreased from 9585 to 9567 bytes using > "rexbidvALT". <- use rexbidv instead > > $ grep 'Proof of "ALT" decr' j*g > job119.log:Proof of "ismgmALT" decreased from 199 to 151 bytes using > "elab2g". <- Alexander: I assume this is ok to do? > Yes, it's OK to minimize the prove using elab2g. And no tags are required. -- 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/9c7129e0-02b0-462d-a5e2-134c8a48427c%40googlegroups.com.
