A bug in the MINIMIZE_WITH command ?

[Benoit]

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

[Gino Giotto]

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.

[Benoit]

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