Thank you, I had forgotten to look at axiom and definition usage. Therefore, I added it back in my mathbox as bj-brrelex12ALT. Benoît
On Wednesday, July 26, 2023 at 12:54:54 PM UTC+2 [email protected] wrote: > Not a bug. The proof of ~brrelex12 uses ax-13, while the proof of ~bj-elbr > doesn't (also ~brrelex12 uses new definitions, so by default I would test > this with `MM-PA> MINIMIZE_WITH * /ALLOW_NEW_AXIOMS * /NO_NEW_AXIOMS_FROM > ax-*` to make sure we are not impeded by them). > > Since the default behaviour of the minimizer is to not introduce any new > $a statements in proofs, then the substitution with ~brrelex12 is rejected. > If you write ` MM-PA> MINIMIZE_WITH * /ALLOW_NEW_AXIOMS * ` then the > minimizer will use ~brrelex12 as a valid shortening. > > Il giorno sabato 22 luglio 2023 alle 20:52:31 UTC+2 Benoit ha scritto: > >> While doing some work, I proved the lemma I needed >> https://us.metamath.org/mpeuni/bj-elbr.html >> It turns out it already existed as >> https://us.metamath.org/mpeuni/brrelex12.html >> >> But when I try to minimize ~bj-elbr, the command `MM-PA> MINIMIZE_WITH *` >> does not find the 1-step proof from ~brrelex12. Is this a bug ? If I do >> `MM-PA> DELETE ALL` and then `MM-PA> IMPROVE ALL` it does find the 1-step >> proof. >> >> Thanks, >> Benoît >> > -- 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/73f1dde5-6520-4ae0-8296-75c3f8e3f893n%40googlegroups.com.
