Remove same-alphabet requirement from ccatval1 #3788
Conversation
* ccats1val1: remove antecedent of sethood of S * ccat2s1p1: remove antecedent of sethood of Y * ccat2s1p2: remove antecedent of sethood of X
| 17-Jan-24 mteqand [same] moved from SN's mathbox to main set.mm | ||
| 15-Jan-24 sseqtr4d sseqtrrd | ||
| 14-Jan-24 sseqtr4i sseqtrri | ||
| 14-Jan-24 ccat2s1len [same] revised - eliminated unnecessary antecedents | ||
| 14-Jan-24 wlklenvclwlk [same] revised - eliminated unnecessary antecedent |
There was a problem hiding this comment.
Our convention is not to add revised theorems to the changes-set, but to append an OLD to the former version and to add "(Proof modification is discouraged.)" and "(New usage is discouraged.)" to it. Furthermore, the comment should contain a hint that this version is obsolete.
See, for example, ~pm2.18OLD:
$( Obsolete version of ~ pm2.18 as of 17-Nov-2023. (Contributed by NM,
29-Dec-1992.) (Proof modification is discouraged.)
(New usage is discouraged.) $)
pm2.18OLD $p |- ( ( -. ph -> ph ) -> ph ) $=
TThese OLD theorems will be deleted after about a year.
There was a problem hiding this comment.
~ccat2s1len and ~wlklenvclwlk were revised in a previous PR? Then the corresponding OLD theorems should be added belatedly.
There was a problem hiding this comment.
Our convention is not to add revised theorems to the changes-set, ....
OK, there are no exact conventions when and how to add entries to changes-set.txt. I had a look at older entries, and actually there are many about revisions. Therefore, I do not insist in removing this entries anymore.
set.mm
Outdated
| @@ -150291,11 +150293,12 @@ computer programs (as last() or lastChar()), the terminology used for | |||
| UPRABUCUMUDUMUEUFUG $. | |||
|
|
|||
| $( Value of a symbol in the left half of a word concatenated with a single | |||
| symbol. (Contributed by Alexander van der Vekens, 5-Aug-2018.) $) | |||
| ccats1val1 $p |- ( ( W e. Word V /\ S e. V /\ I e. ( 0 ..^ ( # ` W ) ) ) | |||
There was a problem hiding this comment.
As explained above, this versin should be kept as ccats1val1OLD.
set.mm
Outdated
|
|
||
| $( Extract the first of two concatenated singleton words. (Contributed by | ||
| Alexander van der Vekens, 22-Sep-2018.) $) | ||
| ccat2s1p1 $p |- ( ( X e. V /\ Y e. V ) |
set.mm
Outdated
|
|
||
| $( Extract the second of two concatenated singleton words. (Contributed by | ||
| Alexander van der Vekens, 22-Sep-2018.) $) | ||
| ccat2s1p2 $p |- ( ( X e. V /\ Y e. V ) | ||
| -> ( ( <" X "> ++ <" Y "> ) ` 1 ) = Y ) $= |
set.mm
Outdated
| @@ -150424,15 +150421,15 @@ computer programs (as last() or lastChar()), the terminology used for | |||
| ccat2s1fvw $p |- ( ( ( W e. Word V /\ I e. NN0 /\ I < ( # ` W ) ) | |||
| /\ ( X e. V /\ Y e. V ) ) | |||
There was a problem hiding this comment.
I think ( X e. V /\ Y e. V ) is also unnecessary here.
set.mm
Outdated
| @@ -150391,21 +150388,21 @@ computer programs (as last() or lastChar()), the terminology used for | |||
| wrdsymb1 syldan cfzo simpl s1cld cn cn0 lencl elnnnn0c biimpri sylan lbfzo0 | |||
| sylibr ccatval1 syl3anc eqtr4d ) ABCZDZEAFGZHIZJZAKAGZLZMNZOGZUSKVAGZUOUQUS | |||
| BDVBUSPBARZUSBAQSURUOUTUNDKKUPTNDZVCUSPUOUQUAURUSBVDUBURUPUCDZVEUOUPUDDZUQV | |||
| FBAUEVFVGUQJUPUFUGUHUPUIUJBAUTKUKULUM $. | |||
| FBAUEVFVGUQJUPUFUGUHUPUIUJBBAUTKUKULUM $. | |||
|
|
|||
| $( Extract the symbol of the first singleton word of a word concatenated with | |||
| this singleton word and another singleton word. (Contributed by Alexander | |||
| van der Vekens, 22-Sep-2018.) (Proof shortened by AV, 1-May-2020.) $) | |||
| ccatw2s1p1 $p |- ( ( ( W e. Word V /\ ( # ` W ) = N ) | |||
| /\ ( X e. V /\ Y e. V ) ) | |||
There was a problem hiding this comment.
I think Y e. V is also unnecessary here.
|
To not block this PR any longer, I will solve the merge conflicts and approve this PR, so that it can be merged. I will incorporate my review remarks in a separate PR afterwards. @benjub do you agree? |
| 17-Jan-24 mteqand [same] moved from SN's mathbox to main set.mm | ||
| 15-Jan-24 sseqtr4d sseqtrrd | ||
| 14-Jan-24 sseqtr4i sseqtrri | ||
| 14-Jan-24 ccat2s1len [same] revised - eliminated unnecessary antecedents | ||
| 14-Jan-24 wlklenvclwlk [same] revised - eliminated unnecessary antecedent |
There was a problem hiding this comment.
Our convention is not to add revised theorems to the changes-set, ....
OK, there are no exact conventions when and how to add entries to changes-set.txt. I had a look at older entries, and actually there are many about revisions. Therefore, I do not insist in removing this entries anymore.
Agreed. And then, the antecedents you noticed are unnecessary can be removed in a later PR. |
|
While working on the removal of the unnecessary antecedents, I detected more such cases (and maybe there will be even more...). I try to revise all this cases with my announced PR (may take a little bit longer as expected now). |
Follow up of PR metamath#3788: * reconstructed OLD theorems: catlenOLD, ccatval1OLD, ccat2s1lenOLD, ccats1val1OLD, ccat2s1p1OLD, ccat2s1p2OLD, wlklenvclwlkOLD, * some unnecessary antecedents removed: ccatw2s1ass, ccatw2s1p1, ccat2s1fvw, ccat2s1fst, ccatw2s1ccatws2, ccat2s1fvwALT
Follow up of PR #3788: * reconstructed OLD theorems: catlenOLD, ccatval1OLD, ccat2s1lenOLD, ccats1val1OLD, ccat2s1p1OLD, ccat2s1p2OLD, wlklenvclwlkOLD, * some unnecessary antecedents removed: ccatw2s1ass, ccatw2s1p1, ccat2s1fvw, ccat2s1fst, ccatw2s1ccatws2, ccat2s1fvwALT
Other changes:
$d x A $.for the new variableAs before, I have looked for opportunities to shrink each proof a little, to counteract the small size growth due to introducing a new variable. I have done many of these proofs already in previous rounds of removing same-alphabet requirements, so there are quite a few instances of single-digit growth.