It may minimize with the statement, then later minimize the statement away. I wouldn't be worried unless "idi" appears in the minimized proof.
On Fri, Feb 14, 2020 at 6:27 PM David A. Wheeler <dwhee...@dwheeler.com> wrote: > I just took a quick look at job144.log as posted on: > https://dwheeler.com/temp/job144.log > > I noticed these... oddities: > Proof of "fourierdlem48" decreased from 18892 to 18864 bytes using > "dummylink". > Proof of "fourierdlem48" decreased from 18864 to 18848 bytes using "idi". > > I didn't expect that. This is using Metamath Version 0.181 12-Feb-2020. > Is this expected behavior (and if so, why)? > > --- 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 metamath+unsubscr...@googlegroups.com. > To view this discussion on the web visit > https://groups.google.com/d/msgid/metamath/E1j2nAt-0005ZC-6n%40rmmprod07.runbox > . > -- 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 metamath+unsubscr...@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/CAFXXJSuq_ii-gN9bcYyFJMBBPSDN1H6W1DZO3dqPrwJorfdS3g%40mail.gmail.com.
