search

metamath / set.mm

Metamath source file for logic and set theory
Creative Commons Zero v1.0 Universal
238 stars 87 forks source link

rename NaryF to -aryF and switch args #4037

Closed icecream17 closed 1 month ago

icecream17 commented 1 month ago

fixes #4035

also commuted: antecedent of naryfvalel (would lengthen if not for sylan9bb) consequent of naryrcl (prevents extra ancoms) antecedent of naryfvalelwrdf (lengthens proof)

--- explanatory comments there are shortenings but these are either minimize_all or "trivial" (commuting or using i/d/g/etc versions of theorems in ways that are just outside current automation)

proofs of 1aryenef & 2aryenef seem lengthened (0 compressed byte change tho) since ovprc2 is added

I don't think changes-set needs to be changed but here's a convenient copy-paste if it does:

 7-Jun-24 df-naryf  [same]      operands switched
avekens commented 1 month ago

Thank you very much, @icecream17 , for these changes. It is a nice side effect that many of the proofs became shorter, but we should not pay much attention on minimal changes of the lengths here (it does not matter that some proofs became a little bit longer). An entry in changes-set.txt is not necessary, because all changes are within my mathbox.