On Wednesday, February 12, 2020 at 10:00:42 AM UTC+1, David Starner wrote: > > There might be an error in the minimize command; it found that axdc > has a much shorter proof using ax-dc, which is obviously true yet > defeats the purpose of the axdc theorem ( > http://us.metamath.org/mpegif/axdc.html ) and uses new axioms for that > theorem. > > I think ~axdc must be tagged with "(Proof modification is discouraged.)", so that minimize will not touch its proof. This is not an error of the minimize command.
-- 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/e6d93a99-24bc-4361-b502-ca99f146b726%40googlegroups.com.
