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/fe9384b2-392a-4950-b106-d56f90139b01n%40googlegroups.com.
