Minimize ax-13 usage 27 #3873
Minimize ax-13 usage 27 #3873
Conversation
There was a problem hiding this comment.
In limsuppnfd (in a mathbox) I noticed that the proof became shorter. The reason was that two instances of cbvralv were substituted with one of cbvral2vw. I consider this as acceptable. But it is easier for me to review such massive changes when there is a direct mapping between old and new versions of theorems in proofs. A separate minimizing sweep could then improve on proof structure.
|
Because of the way the script is designed, these "special shorter proofs" can happen, although they should be so rare to not constitute a problem (and they are further improvements, so I didn't consider them an issue). Trying to avoid these cases on purpose is a bit difficult. Best thing I can do at the moment is to look for them manually and report them in the PR description. |
Part of groups.google.com/g/metamath/c/OB2_9sYgDfA.
Continuation of #3796.
This PR drops ax-13 from 167 theorems. Full axiom usage here: 8ea714f
Affected mathboxes:
@tirix mathbox (just the leftover reuxfrdf).
@glacode mathbox.