On Thu, 13 Feb 2020 06:25:42 -0800 (PST), Benoit <[email protected]> wrote: > Actually, most *OLD and *ALT should probably have both discouragement tags > as well, it seems ?
I looked at the .log files I have so far. Once I "cd" into metamathjobs/ ... I have no proposed minimizations involving "OLD": grep 'decreased' *.log | grep OLD But I do have some proposed minimizations involving "ALT": grep 'decreased' *.log | grep ALT | uniq The list: job129.log:Proof of "dral1ALT" decreased from 81 to 16 bytes using "dral1". job129.log:Proof of "dveeq2ALT" decreased from 41 to 15 bytes using "dveeq2". job132.log:Proof of "ax16nfALT" decreased from 45 to 16 bytes using "ax16nf". I don't think we want to apply these minimizations :-). As a first cut, we might just skip anything involving ALT or OLD, then look more carefully. At the least, we shouldn't use THEOREMT to prove THEOREMTALT. --- David A. Wheeler -- 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/E1j2iJW-0006oo-UE%40rmmprod07.runbox.
