"df-plus" should be named "df-add"

[David A. Wheeler]

While trying to document the conventions, I noticed an inconsistency.
I suggest renaming "df-plus" to "df-add" to make the names more consistent.

Usually the label abbreviation uses whatever is after "df-". E.G., "an" for "df-an", etc.
However, "df-plus" doesn't follow this convention. Instead, "add" is consistently used
in label names (e.g., "addcl", "addcom"). What's more, the "df-plus" name isn't even
consistent with its comment, which says "Define addition over complex numbers."
All-constant theorems like 3p2e5 don't follow the "plus" convention either
(all-constant theorems appear to uniformly use "p" not "plus"), so there's
no reason to call it "df-plus". It's odd to have something this basic be inconsistent.

I am *NOT* suggesting we rename "df-plusg"; "plusg" *is* consistently used in labels.
What's more, "plusg" emphasizes a generic symbol (which is sensible), while
"df-plus" isn't (df-plus refers to a specific operation: addition).
I don't think "df-plusf" should change either.

--- David A. Wheeler

[Norman Megill]

On Wednesday, July 19, 2017 at 1:14:40 PM UTC-4, David A. Wheeler wrote:

While trying to document the conventions, I noticed an inconsistency.
I suggest renaming "df-plus" to "df-add" to make the names more consistent.

This is fine with me.  Remember to put the label change at the top of set.mm.  There are some others ones with similar mismatch, such as df-ring for the definition but *rng* for theorems.
 

Usually the label abbreviation uses whatever is after "df-".  E.G., "an" for "df-an", etc.
However, "df-plus" doesn't follow this convention.  Instead, "add" is consistently used
in label names (e.g., "addcl", "addcom").  What's more, the "df-plus" name isn't even
consistent with its comment, which says "Define addition over complex numbers."
All-constant theorems like 3p2e5 don't follow the "plus" convention either
(all-constant theorems appear to uniformly use "p" not "plus"), so there's
no reason to call it "df-plus".  It's odd to have something this basic be inconsistent.

It is rare to use it directly (2 theorems), so it probably wasn't noticed too often.
 

I am *NOT* suggesting we rename "df-plusg"; "plusg" *is* consistently used in labels.
What's more, "plusg" emphasizes a generic symbol (which is sensible), while
"df-plus" isn't (df-plus refers to a specific operation: addition).
I don't think "df-plusf" should change either.

--- David A. Wheeler

Norm

[David A. Wheeler]

On Wed, 19 Jul 2017 10:32:09 -0700 (PDT), Norman Megill <n...@alum.mit.edu> wrote:
> ... There are some others ones with similar mismatch, such as df-ring

> for the definition but *rng* for theorems.

If that's going to continue for rings, I suggest adding a comment to "df-ring".
Something like this:

> Use the abbreviation "rng" in labels when representing this definition.

I don't mind the occasional "longer name" in a definition, but it should
be *obvious* to readers when labels do something different.

--- David A. Wheeler

[Mario Carneiro]

I don't think it is worth keeping these few exceptions. For uniformity, I support both these renames.

Mario 

--
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 metamath+unsubscribe@googlegroups.com.
To post to this group, send email to meta...@googlegroups.com.
Visit this group at https://groups.google.com/group/metamath.
For more options, visit https://groups.google.com/d/optout.

[Norman Megill]

On Wednesday, July 19, 2017 at 3:47:12 PM UTC-4, David A. Wheeler wrote:

On Wed, 19 Jul 2017 10:32:09 -0700 (PDT), Norman Megill wrote:
> ... There are some others ones with similar mismatch, such as df-ring
> for the definition but *rng* for theorems.

If that's going to continue for rings, I suggest adding a comment to "df-ring".

What I meant to say was that df-ring should be changed to df-rng, and there may be other cases like that that also should be changed.  Note that we use df-grp rather than df-group, and df-rng would be consistent with this.
 

Something like this:

> Use the abbreviation "rng" in labels when representing this definition.

I don't think that label convention explanations should appear in statements' comments.  There is no easy way to locate and update them with future label changes, if they are scattered about.  The conventions section where you have them now is fine.

Norm

[David A. Wheeler]

On Wed, 19 Jul 2017 13:14:56 -0700 (PDT), Norman Megill <n...@alum.mit.edu> wrote:
> What I meant to say was that df-ring should be changed to df-rng, and there
> may be other cases like that that also should be changed. Note that we use
> df-grp rather than df-group, and df-rng would be consistent with this.

Oh, *that*'s what you meant! In that case, forget about adding comments.
Being consistent is easier than explaining why you aren't consistent :-).

> I don't think that label convention explanations should appear in
> statements' comments. There is no easy way to locate and update them with
> future label changes, if they are scattered about.

I don't think that's true for definitions.
*Definitions* are easily found by searching for "df-".
If you're going to update a label that corresponds to a definition,
updating its corresponding definition is not hard.
Not everything in a label corresponds to a definition, though.

In any case, it's better to try to be consistent first. If we decide
that we *won't* be consistent, then we can figure out how to document that.
But if we can keep inconsistencies to a dull roar that'd help.

> The conventions section where you have them now is fine.

Sounds good. I plan to merge the first cut soon, since I haven't seen objections and
their purpose is to merely document what is *already* being done.

There's an interesting side-effect of alphabetizing
abbreviations in one place: it suddenly becomes obvious
when there is a potential inconsistency. There are several cases where
there are multiple abbreviations for something
(just look for "," in the abbreviations).
They may indicate an inconsistency, or that the rule is more
complex than the documentation indicates, but those are at
least places to think about.

For example, the empty set is sometimes identified as "z" ( ~ snnz , ~ prnz )
and other times is identified with "0" ( ~ n0i , ~ vn0 ), even though it is "df-nul".
I only noticed this when I alphabetized things.

--- David A. Wheeler

[Mario Carneiro]

Currently, zero is labeled a bit oddly. df-0 is the complex number, but its corresponding syntax axiom is cc0 instead of c0 by the usual rule because c0 is taken for the empty set. This is also inconsistent with its definition df-nul. Unfortunately, both these have the same label fragment "0" in theorems (luckily the context usually puts these in complementary distribution), so there is no way to have them both as df-0. (We can't use "z" uniquely for the empty set since that would overlap with df-z "ZZ".) I don't really want to replace 0 with nul in all the nullset theorems, so I think we should just note this as a slight inconsistency in order to reuse the "0" label fragment in the set theory section.

To make the syntax axioms more consistent, I propose the replacements cc0 -> c0 (class 0), c0 -> cnl (class (/) ), cnl -> cnul (class null). Since cc0 is used 4543 times and c0 is used only 3494 times, the length swap here will decrease overall size. df-nlfn ("null") is an outdated definition about the null space of a linear functional in the Hilbert space section, so we can afford to give it a longer name. (This rename also has the advantage that now all the digits are formed as "c" + digit, which is important for the arithmetic prover. The current version has to special-case zero because of the naming inconsistency.)

Mario

[Mario Carneiro]

Regarding "nz" for nonzero, I suggest collecting a list of all of these and renaming to "n0" for consistency.

[David A. Wheeler]

On Wed, 19 Jul 2017 23:18:21 +0100, Mario Carneiro <di....@gmail.com> wrote:
> Currently, zero is labeled a bit oddly. df-0 is the complex number, but its
> corresponding syntax axiom is cc0 instead of c0 by the usual rule because
> c0 is taken for the empty set. This is also inconsistent with its
> definition df-nul. Unfortunately, both these have the same label fragment
> "0" in theorems (luckily the context usually puts these in complementary
> distribution), so there is no way to have them both as df-0. (We can't use
> "z" uniquely for the empty set since that would overlap with df-z "ZZ".)

The empty set is sometimes notated as "0" ( ~ n0i , ~ vn0 )
and other times as "z" ( ~ snnz , ~ prnz ).
It would make sense to consistently use "z" for the empty set
and "0" for zero. The problem, as you noted, is that
"df-z" already used for ZZ. Indeed,
"z" is *also* used in many places to represent ZZ ( ~ elz , ~ zcn ).

Perhaps "df-z" should be renamed to "df-zz", since the ASCII symbol is "ZZ" anyway.
Then we could consistently use "zz" instead of "z" in labels to mean integer,
and consistently use "z" to mean the empty set. Then the empty set
definition could be renamed to "df-z", with labels always using "z" to refer to it.

--- David A. Wheeler

[Norman Megill]

On Wednesday, July 19, 2017 at 6:23:09 PM UTC-4, Mario Carneiro wrote:

Regarding "nz" for nonzero, I suggest collecting a list of all of these and renaming to "n0" for consistency

This seems ok.  There seem to be only 5 of them:  snnz, prnz, tpnz, opnz, xpnz.

There is an informal sub-convention that "n0" means =/= (/) and "ne0" means =/= 0.  "n0" has occasional conflict with operators ending with "n" evaluated at 0 e.g. rn0 although offhand I don't notice any obvious ambiguities (since e.g. we know we're working with "rn" in this case).  Anyway we shouldn't become too obsessed with occasional ambiguities; the purpose is to have short names and patterns that are easier for humans to remember.

In the r19.* theorems, a "z" suffix is used to indicate that a non-empty condition is required e.g. r19.27z.  I added the z a long time ago to remind me that going from 19.27 to r19.27z requires the extra non-empty condition, unlike most of the 19.* to r19.* generalizations.  I suppose we could change those to "n0", although in general it seems "n0" is used for showing something isn't (/) rather than requiring that something not be (/).  Alternately we could just take off the "z" and let the theorem itself  tell us what's needed.

As an aside, over the years we have slowly been changing the *19.* to more meaningful patterns when we can think of good ones, such as *19.21a* becoming *alrim* (add for|al|l to the |r|ight side of an |im|plication).  Such renames can increase confusion if not chosen carefully, and we'd probably want to discuss them first.

Norm

[David A. Wheeler]

>Anyway we shouldn't become too obsessed with occasional ambiguities;
>the
>purpose is to have short names and patterns that are easier for humans
>to remember.

Agreed. If they are consistent they are easier to find. That said, avoiding lots of ambiguities also makes the names more consistent, since you then don't need to disambiguate.

One way that many ambiguities could be avoided would be to avoid having definitions followed by a single letter. E.g., df-z => df-zz. With just 2 symbols, each a lowercase letter or digit, you have over a thousand possibilities... which reduces the likelihood of overlap.


--- David A.Wheeler

[David A. Wheeler]

On Wed, 19 Jul 2017 16:48:03 -0700 (PDT), Norman Megill <n...@alum.mit.edu> wrote:
> There is an informal sub-convention that "n0" means =/= (/) and "ne0" means
> =/= 0.

There's nothing wrong with sub-conventions, we should just document them.

That said, "n0" seems unfortunate.
There's already the widely-used set N0, so that's confusing.
Also, using "0" for both zero and the empty set makes it hard to tell the
difference between the empty set and 0 via the name,
and that is more likely to lead to collisions.

It'd be better if the empty set and zero used *different* label fragments,
since both show up often. It'd be even better if the definition
of empty set and its label fragment matched.
The empty set's conventions seem odd no matter what: df-nul for the definition,
nul in some places, 0 in others, z in still others.

It'd be a nontrivial change, but you could use "df-es" to define the empty set,
and then use "es" everywhere for the empty set.

In general, we should change things so that when "df-NAME" is used,
NAME is what's used in the labels.

On a somewhat related note...

This would be less ambiguous, and greatly reduce collisions, if "df-"
was almost never followed by a single letter. I looked into what that
would entail. I searched for all cases of df-[a-z]; here they are:
df-v $a |- _V = { x | x = x } $.
df-f $a |- ( F : A --> B <-> ( F Fn A /\ ran F C_ B ) ) $.
df-c $a |- CC = ( R. X. R. ) $.
df-i $a |- _i = <. 0R , 1R >. $.
df-r $a |- RR = ( R. X. { 0R } ) $.
df-n $a |- NN = ( rec ( ( x e. _V |-> ( x + 1 ) ) , 1 ) " om ) $.
df-z $a |- ZZ = { n e. RR | ( n = 0 \/ n e. NN \/ -u n e. NN ) } $.
df-q $a |- QQ = ( / " ( ZZ X. NN ) ) $.
df-e $a |- _e = ( exp ` 1 ) $.

All the doubled-letter ones could be renamed like this without
renaming any other $a (the doubled ones aren't used, and it
would make *sense* to use doubled letters for them!):
CC: df-c => df-cc
RR: df-r => df-rr
NN: df-n => df-nn
ZZ: df-z => df-zz
QQ: df-q => df-qq
Labels that use them would then be adjusted.
That would eliminate a lot of
ambiguity & greatly reduce the likelihood of collisions.

Labels are allowed to have underscores, so we could easily do this:
_V : df-v => df-_v
_i : df-i => df-_i
_e : df-e => df-_e

I'm not sure what to do with df-f. Maybe "df-fd"?

--- David A. Wheeler

[Mario Carneiro]

On Thu, Jul 20, 2017 at 4:18 PM, David A. Wheeler <dwhe...@dwheeler.com> wrote:

On Wed, 19 Jul 2017 16:48:03 -0700 (PDT), Norman Megill <n...@alum.mit.edu> wrote:
> There is an informal sub-convention that "n0" means =/= (/) and "ne0" means
> =/= 0.

There's nothing wrong with sub-conventions, we should just document them.

That said, "n0" seems unfortunate.
There's already the widely-used set N0, so that's confusing.
Also, using "0" for both zero and the empty set makes it hard to tell the
difference between the empty set and 0 via the name,
and that is more likely to lead to collisions.

It'd be better if the empty set and zero used *different* label fragments,
since both show up often. It'd be even better if the definition
of empty set and its label fragment matched.
The empty set's conventions seem odd no matter what: df-nul for the definition,
nul in some places, 0 in others, z in still others.

It'd be a nontrivial change, but you could use "df-es" to define the empty set,
and then use "es" everywhere for the empty set.

Sorry, but this is getting into "don't rock the boat" territory for me. If you introduce too many name changes, it will require a lot of re-learning. The two uses of 0 are not colliding in any specific cases under consideration, so this seems gratuitous.
 

In general, we should change things so that when "df-NAME" is used,
NAME is what's used in the labels.

On a somewhat related note...

This would be less ambiguous, and greatly reduce collisions, if "df-"
was almost never followed by a single letter.  I looked into what that
would entail. I searched for all cases of df-[a-z]; here they are:
  df-v $a |- _V = { x | x = x } $.
  df-f $a |- ( F : A --> B <-> ( F Fn A /\ ran F C_ B ) ) $.
  df-c $a |- CC = ( R. X. R. ) $.
  df-i $a |- _i = <. 0R , 1R >. $.
  df-r $a |- RR = ( R. X. { 0R } ) $.
  df-n $a |- NN = ( rec ( ( x e. _V |-> ( x + 1 ) ) , 1 ) " om ) $.
  df-z $a |- ZZ = { n e. RR | ( n = 0 \/ n e. NN \/ -u n e. NN ) } $.
  df-q $a |- QQ = ( / " ( ZZ X. NN ) ) $.
  df-e $a |- _e = ( exp ` 1 ) $.

I don't see why it is necessary to avoid single letter fragments. If anything I would like to fill the space of possibilities, as long as ambiguous combinations are unlikely to crop up.

That said, there are a few inconsistencies in this list. df-c has label fragment "cn" in theorems (although we can't do anything about it since "cn" is doing double duty for continuous functions), df-r has label fragment "re" (again, this overlaps with the real part function), and df-n has label fragment "nn" (this one is open, though).

 

All the doubled-letter ones could be renamed like this without
renaming any other $a (the doubled ones aren't used, and it
would make *sense* to use doubled letters for them!):
 CC: df-c => df-cc
 RR: df-r => df-rr
 NN: df-n => df-nn
 ZZ: df-z => df-zz
 QQ: df-q => df-qq
Labels that use them would then be adjusted.
That would eliminate a lot of
ambiguity & greatly reduce the likelihood of collisions.

This is a fair point, when possible the symbol should at least somewhat resemble the label fragment, and as you say the doubled letter fragments are as yet unused here. So how about just these five renames? Even this will affect quite a lot of theorems and a few axioms, so it's a nontrivial change.

Mario

[David A. Wheeler]

On Thu, Jul 20, 2017 at 4:18 PM, David A. Wheeler <dwhe...@dwheeler.com> wrote:
> > It'd be a nontrivial change, but you could use "df-es" to define the empty
> > set, and then use "es" everywhere for the empty set.

On Thu, 20 Jul 2017 17:18:43 +0100, Mario Carneiro <di....@gmail.com> wrote:
> Sorry, but this is getting into "don't rock the boat" territory for me. If
> you introduce too many name changes, it will require a lot of re-learning.

I agree that we don't want too many definition name changes.
I don't expect many, because label names and df-NAME normally match.
Also, changes made to improve consistency should quickly provide some
dividends; better consistency will make new learning much easier
(there will be much less to remember).

Sadly, the empty set notation is *not* an example of stellar consistency :-).

> The two uses of 0 are not colliding in any specific cases under
> consideration, so this seems gratuitous.

It's not gratuitous. The current setup is inconsistent with the claimed
naming scheme, and this inconsistency involves something widely used.
If "0" is normally used in labels to represent the empty set,
then "df-0" should define the empty set... and that isn't true in what's proposed.

Currently the empty set (defined in "df-nul") is represented by nul, z, and 0.
Obviously that's inconsistent, and it should be made consistent.
It's a commonly-used symbol, so I understand why the longer "nul" is
often not used in labels (I think the empty set should NOT be a 3-letter label name
because it's too common).

If the current "df-z" (ZZ) is renamed to "df-zz", as discussed below below,
then we could use "df-z" ("slashed zero') to instead define the empty set.
Then we could *uniformly* use "z" in labels to represent the empty set.
We *already* use "z" in several labels to represent the empty set!

Using "z" would not be rocking the boat, it'd be consistently selecting
one of the existing boats :-).

> > All the doubled-letter ones could be renamed like this without
> > renaming any other $a (the doubled ones aren't used, and it
> > would make *sense* to use doubled letters for them!):
> > CC: df-c => df-cc

...

> This is a fair point, when possible the symbol should at least somewhat
> resemble the label fragment, and as you say the doubled letter fragments
> are as yet unused here. So how about just these five renames? Even this
> will affect quite a lot of theorems and a few axioms, so it's a nontrivial
> change.

Sure. It should be easy to heuristically detect & perform many of those
renames; we can then fix the stragglers.

I would suggest doing them one at a time. If we do ZZ first,
that would make it possible to do df-nul => df-z.

Most of the short label forms for the number sets aren't consistent
with their df-NAME *currently*. So if we want the short names
to be consistent with the label names, some renaming would
be needed no matter what. We currently have:
Symbol Defined-in label-form Consistent?
NN df-n nn No (switching df-n to df-nn would *make* them consistent!)
ZZ df-z z Yes (note: Some labels, like zzngim , already use "zz" for ZZ)
RR df-r re No (and "df-re" means something different!!)
CC df-c cn No (and "df-cn" means something different!!)
QQ df-q q Yes (so "q" would change to "qq" in labels)

Note that RR* is defined in "df-xr", and "xr" seems to consistently
used in labels, so I see no reason to change that.

--- David A. Wheeler

[Mario Carneiro]

On Thu, Jul 20, 2017 at 7:18 PM, David A. Wheeler <dwhe...@dwheeler.com> wrote:

On Thu, Jul 20, 2017 at 4:18 PM, David A. Wheeler <dwhe...@dwheeler.com> wrote:
> > It'd be a nontrivial change, but you could use "df-es" to define the empty
> > set, and then use "es" everywhere for the empty set.

On Thu, 20 Jul 2017 17:18:43 +0100, Mario Carneiro <di....@gmail.com> wrote:
> Sorry, but this is getting into "don't rock the boat" territory for me. If
> you introduce too many name changes, it will require a lot of re-learning.

I agree that we don't want too many definition name changes.
I don't expect many, because label names and df-NAME normally match.
Also, changes made to improve consistency should quickly provide some
dividends; better consistency will make new learning much easier
(there will be much less to remember).

Sadly, the empty set notation is *not* an example of stellar consistency :-).

> The two uses of 0 are not colliding in any specific cases under
> consideration, so this seems gratuitous.

It's not gratuitous.  The current setup is inconsistent with the claimed
naming scheme, and this inconsistency involves something widely used.
If "0" is normally used in labels to represent the empty set,
then "df-0" should define the empty set... and that isn't true in what's proposed.

Currently the empty set (defined in "df-nul") is represented by nul, z, and 0.
Obviously that's inconsistent, and it should be made consistent.

I've already stated that I support renaming "z" to "0" (or more precisely, "nz" to "n0" since I think it always occurs in that context). The "nul" label fragment occurs to my knowledge *only* in the definition df-nul, and that is simply because we can't have df-0 twice. The label fragment convention that 0 maps to the number 0 and also the empty set is otherwise followed consistently, and I do not wish to diverge from this convention.

 

It's a commonly-used symbol, so I understand why the longer "nul" is
often not used in labels (I think the empty set should NOT be a 3-letter label name
because it's too common).

If the current "df-z" (ZZ) is renamed to "df-zz", as discussed below below,
then we could use "df-z" ("slashed zero') to instead define the empty set.
Then we could *uniformly* use "z" in labels to represent the empty set.
We *already* use "z" in several labels to represent the empty set!

Using "z" would not be rocking the boat, it'd be consistently selecting
one of the existing boats :-).

Hm, okay I'm seeing the benefit here.
 

> > All the doubled-letter ones could be renamed like this without
> > renaming any other $a (the doubled ones aren't used, and it
> > would make *sense* to use doubled letters for them!):
> >  CC: df-c => df-cc
...

> This is a fair point, when possible the symbol should at least somewhat
> resemble the label fragment, and as you say the doubled letter fragments
> are as yet unused here. So how about just these five renames? Even this
> will affect quite a lot of theorems and a few axioms, so it's a nontrivial
> change.

Sure.  It should be easy to heuristically detect & perform many of those
renames; we can then fix the stragglers.

I would suggest doing them one at a time.  If we do ZZ first,
that would make it possible to do df-nul => df-z.

I don't see the purpose of doing this "slowly" if slowly means over the course of a few days. That's not enough to get full community feedback, so you may as well minimize the pain of intermediate states by doing the renames in bulk. The best way to do this if you want transparency is to construct a full list of renames for review (such as might go in the rename list at the top of set.mm), and then apply them in bulk once you are getting a green light. Drizzling them out one piece at a time just makes review harder.

 

Mario

[David A. Wheeler]

On Thu, 20 Jul 2017 21:43:39 +0100, Mario Carneiro <di....@gmail.com> wrote:
> The "nul"
> label fragment occurs to my knowledge *only* in the definition df-nul, and

> that is simply because we can't have df-0 twice...

On a quick search I found these examples where "nul" (or "null")
appears to be used for (/):

df-nul $a |- (/) = ( _V \ _V ) $.
dfnul2 $p |- (/) = { x | -. x = x } $=
dfnul3 $p |- (/) = { x e. A | -. x e. A } $=
nnullss $p |- ( A =/= (/) -> E. x ( x C_ A /\ x =/= (/) ) ) $=
iotanul $p |- ( -. E! x ph -> ( iota x ph ) = (/) ) $=
sumnul $p |- ( ph -> sum_ k e. Z A = (/) ) $=
chocnul $p |- ( _|_ ` (/) ) = ~H $=

I found these examples where "z" may be
used for (/), NOT including all the r19.z* labels. In some cases
"z" may stand for something else, but I was trying to do a
quick search, and I think this list is long enough to show
that set.mm labels do *not* consistently
use "0" for the empty set:

snnzg $p |- ( A e. V -> { A } =/= (/) ) $=
snnz $p |- { A } =/= (/) $=
prnz $p |- { A , B } =/= (/) $=
prnzg $p |- ( A e. V -> { A , B } =/= (/) ) $=
tpnz $p |- { A , B , C } =/= (/) $=
opnz $p |- ( <. A , B >. =/= (/) <-> ( A e. _V /\ B e. _V ) ) $=
opnzi $p |- <. A , B >. =/= (/) $=
unizlim $p |- ( Ord A -> ( A = U. A <-> ( A = (/) \/ Lim A ) ) ) $=
xpnz $p |- ( ( A =/= (/) /\ B =/= (/) ) <-> ( A X. B ) =/= (/) ) $=
zfreg $p |- ( A =/= (/) -> E. x e. A ( x i^i A ) = (/) ) $=
zfreg2 $p |- ( A =/= (/) -> E. x e. A ( A i^i x ) = (/) ) $=
zfinf2 $p |- E. x ( (/) e. x /\ A. y e. x suc y e. x ) $=
zfregs $p |- ( A =/= (/) -> E. x e. A ( x i^i A ) = (/) ) $=
zfregs2 $p |- ( A =/= (/) -> -. A. x e. A E. y ( y e. A /\ y e. x ) ) $=
suprzcl $p |- ( ( A C_ ZZ /\ A =/= (/) /\ E. x e. RR A. y e. A y <_ x ) ->
uzwo $p |- ( ( S C_ ( ZZ>= ` M ) /\ S =/= (/) ) ->
uzwoOLD $p |- ( ( S C_ ( ZZ>= ` M ) /\ -. S = (/) ) ->
uzwo2 $p |- ( ( S C_ ( ZZ>= ` M ) /\ S =/= (/) ) ->
infmssuzcl $p |- ( ( S C_ ( ZZ>= ` M ) /\ S =/= (/) ) ->
zsupss $p |- ( ( A C_ ZZ /\ A =/= (/) /\ E. x e. ZZ A. y e. A y <_ x ) ->
suprzcl2 $p |- ( ( A C_ ZZ /\ A =/= (/) /\ E. x e. ZZ A. y e. A y <_ x ) ->
uzwo3 $p |- ( ( B e. RR /\ ( A C_ { z e. ZZ | B <_ z } /\ A =/= (/) ) )
fzn $p |- ( ( M e. ZZ /\ N e. ZZ ) -> ( N < M <-> ( M ... N ) = (/) ) ) $=
om2uz0i $p |- ( G ` (/) ) = C $=
s1nz $p |- <" A "> =/= (/) $=

> I don't see the purpose of doing this "slowly" if slowly means over the
> course of a few days. That's not enough to get full community feedback, so
> you may as well minimize the pain of intermediate states by doing the
> renames in bulk. The best way to do this if you want transparency is to
> construct a full list of renames for review (such as might go in the rename
> list at the top of set.mm), and then apply them in bulk once you are
> getting a green light. Drizzling them out one piece at a time just makes
> review harder.

I meant "rename one df-... & its corresponding labels at a time", to simplify review.
For a given definition, it's *definitely* best to do it in bulk.

I did a quick check on renaming "df-z" to "df-zz" along with its
corresponding labels. This is perhaps the most challenging, because
labels use "z" for other things. However, I created simple
script "rename-proposals" below to create an automated list of
proposed renames, and then ran it like this:
./rename-proposals 'z' 'zz' 'ZZ'

Basically, it ONLY does a rename if the same line has a sample of the
relevant symbol. This seems to do a decent job of picking the right ones.
Each line produced by the script describes a proposed rename in the form:
> Old-name New-name First-part-of-expression

That output should make it easy to focus on the proposal. I looked over the
list, and quickly removed "df-za" as a spurious result.
I could then run a separate program to actually make those proposed
changes to set.mm, verify it, and create a PR as you noted above.

--- David A. Wheeler


== File "rename-proposals" (used to create the list below)
#!/bin/sh

# Create a first-cut list of rename proposals
# (the result can then be edited, including deleting irrelevant lines)
# We create a list of labels to rename, but *ONLY* if there's a relevant
# symbol on the same line (a reasonable heuristic)

# Use like this:
# ./rename-proposals 'cn' 'cc' 'CC'

old_label_fragment="$1"
new_label_fragment="$2"
symbol="$3"

# Use "read -r" to disable backslash interpretation.

grep "${old_label_fragment}.* \$[ap] .* ${symbol} " set.mm |
while read -r oldlabel info
do
newlabel=`printf %s "$oldlabel" |
sed -e "s/${old_label_fragment}/${new_label_fragment}/g" -`
printf '%s\n' "$oldlabel $newlabel $info"
done


== Proposals generated from: ./rename-proposals 'z' 'zz' 'ZZ'

cz czz $a class ZZ $.
df-z df-zz $a |- ZZ = { n e. RR | ( n = 0 \/ n e. NN \/ -u n e. NN ) } $.
elz elzz $p |- ( N e. ZZ <->
nnnegz nnnegzz $p |- ( N e. NN -> -u N e. ZZ ) $=
zre zzre $p |- ( N e. ZZ -> N e. RR ) $=
zcn zzcn $p |- ( N e. ZZ -> N e. CC ) $=
zssre zzssre $p |- ZZ C_ RR $=
zsscn zzsscn $p |- ZZ C_ CC $=
zex zzex $p |- ZZ e. _V $=
elnnz elnnzz $p |- ( N e. NN <-> ( N e. ZZ /\ 0 < N ) ) $=
0z 0zz $p |- 0 e. ZZ $=
elnn0z elnn0zz $p |- ( N e. NN0 <-> ( N e. ZZ /\ 0 <_ N ) ) $=
elznn0nn elzznn0nn $p |- ( N e. ZZ <-> ( N e. NN0 \/ ( N e. RR /\ -u N e. NN ) ) ) $=
elznn0 elzznn0 $p |- ( N e. ZZ <-> ( N e. RR /\ ( N e. NN0 \/ -u N e. NN0 ) ) ) $=
elznn elzznn $p |- ( N e. ZZ <-> ( N e. RR /\ ( N e. NN \/ -u N e. NN0 ) ) ) $=
elz2 elzz2 $p |- ( N e. ZZ <-> E. x e. NN E. y e. NN N = ( x - y ) ) $=
dfz2 dfzz2 $p |- ZZ = ( - " ( NN X. NN ) ) $=
zexALT zzexALT $p |- ZZ e. _V $=
nnssz nnsszz $p |- NN C_ ZZ $=
nn0ssz nn0sszz $p |- NN0 C_ ZZ $=
nnz nnzz $p |- ( N e. NN -> N e. ZZ ) $=
nn0z nn0zz $p |- ( N e. NN0 -> N e. ZZ ) $=
nnzi nnzzi $p |- N e. ZZ $=
nn0zi nn0zzi $p |- N e. ZZ $=
elnnz1 elnnzz1 $p |- ( N e. NN <-> ( N e. ZZ /\ 1 <_ N ) ) $=
znnnlt1 zznnnlt1 $p |- ( N e. ZZ -> ( -. N e. NN <-> N < 1 ) ) $=
nnzrab nnzzrab $p |- NN = { x e. ZZ | 1 <_ x } $=
nn0zrab nn0zzrab $p |- NN0 = { x e. ZZ | 0 <_ x } $=
1z 1zz $p |- 1 e. ZZ $=
2z 2zz $p |- 2 e. ZZ $=
znegcl zznegcl $p |- ( N e. ZZ -> -u N e. ZZ ) $=
znegclb zznegclb $p |- ( A e. CC -> ( A e. ZZ <-> -u A e. ZZ ) ) $=
nn0negz nn0negzz $p |- ( N e. NN0 -> -u N e. ZZ ) $=
nn0negzi nn0negzzi $p |- -u N e. ZZ $=
zaddcl zzaddcl $p |- ( ( M e. ZZ /\ N e. ZZ ) -> ( M + N ) e. ZZ ) $=
peano2z peano2zz $p |- ( N e. ZZ -> ( N + 1 ) e. ZZ ) $=
zsubcl zzsubcl $p |- ( ( M e. ZZ /\ N e. ZZ ) -> ( M - N ) e. ZZ ) $=
peano2zm peano2zzm $p |- ( N e. ZZ -> ( N - 1 ) e. ZZ ) $=
zrevaddcl zzrevaddcl $p |- ( N e. ZZ ->
znnsub zznnsub $p |- ( ( M e. ZZ /\ N e. ZZ ) -> ( M < N <-> ( N - M ) e. NN ) ) $=
znn0sub zznn0sub $p |- ( ( M e. ZZ /\ N e. ZZ ) ->
zmulcl zzmulcl $p |- ( ( M e. ZZ /\ N e. ZZ ) -> ( M x. N ) e. ZZ ) $=
zltp1le zzltp1le $p |- ( ( M e. ZZ /\ N e. ZZ ) -> ( M < N <-> ( M + 1 ) <_ N ) ) $=
zleltp1 zzleltp1 $p |- ( ( M e. ZZ /\ N e. ZZ ) -> ( M <_ N <-> M < ( N + 1 ) ) ) $=
zlem1lt zzlem1lt $p |- ( ( M e. ZZ /\ N e. ZZ ) -> ( M <_ N <-> ( M - 1 ) < N ) ) $=
zltlem1 zzltlem1 $p |- ( ( M e. ZZ /\ N e. ZZ ) -> ( M < N <-> M <_ ( N - 1 ) ) ) $=
zdiv zzdiv $p |- ( ( M e. NN /\ N e. ZZ )
zdivadd zzdivadd $p |- ( ( ( D e. NN /\ A e. ZZ /\ B e. ZZ ) /\
zdivmul zzdivmul $p |- ( ( ( D e. NN /\ A e. ZZ /\ B e. ZZ ) /\
zextle zzextle $p |- ( ( M e. ZZ /\ N e. ZZ /\ A. k e. ZZ ( k <_ M <-> k <_ N ) )
zextlt zzextlt $p |- ( ( M e. ZZ /\ N e. ZZ /\ A. k e. ZZ ( k < M <-> k < N ) )
recnz recnzz $p |- ( ( A e. RR /\ 1 < A ) -> -. ( 1 / A ) e. ZZ ) $=
btwnnz btwnnzz $p |- ( ( A e. ZZ /\ A < B /\ B < ( A + 1 ) ) -> -. B e. ZZ ) $=
halfnz halfnzz $p |- -. ( 1 / 2 ) e. ZZ $=
suprzcl suprzzcl $p |- ( ( A C_ ZZ /\ A =/= (/) /\ E. x e. RR A. y e. A y <_ x ) ->
msqznn msqzznn $p |- ( ( A e. ZZ /\ A =/= 0 ) -> ( A x. A ) e. NN ) $=
zneo zzneo $p |- ( ( A e. ZZ /\ B e. ZZ ) ->
zeo zzeo $p |- ( N e. ZZ -> ( ( N / 2 ) e. ZZ \/ ( ( N + 1 ) / 2 ) e. ZZ ) ) $=
zeo2 zzeo2 $p |- ( N e. ZZ ->
peano2uz2 peano2uzz2 $p |- ( ( A e. ZZ /\ B e. { x e. ZZ | A <_ x } ) ->
peano5uzti peano5uzzti $p |- ( N e. ZZ -> ( ( N e. A /\ A. x e. A ( x + 1 ) e. A )
dfuzi dfuzzi $p |- { z e. ZZ | N <_ z } =
uzind uzzind $p |- ( ( M e. ZZ /\ N e. ZZ /\ M <_ N ) -> ta ) $=
uzind2 uzzind2 $p |- ( ( M e. ZZ /\ N e. ZZ /\ M < N ) -> ta ) $=
uzind3 uzzind3 $p |- ( ( M e. ZZ /\ N e. { k e. ZZ | M <_ k } ) -> ta ) $=
uzindOLD uzzindOLD $p |- ( ( ( A e. ZZ /\ B e. ZZ ) /\ B <_ A ) -> ta ) $=
uzind3OLD uzzind3OLD $p |- ( ( B e. ZZ /\ A e. { z e. ZZ | B <_ z } ) -> ta ) $=
fzind fzzind $p |- ( ( ( M e. ZZ /\ N e. ZZ ) /\
zindd zzindd $p |- ( ze -> ( A e. ZZ -> et ) ) $=
btwnz btwnzz $p |- ( A e. RR -> ( E. x e. ZZ x < A /\ E. y e. ZZ A < y ) ) $=
nn0zd nn0zzd $p |- ( ph -> A e. ZZ ) $=
nnzd nnzzd $p |- ( ph -> A e. ZZ ) $=
znegcld zznegcld $p |- ( ph -> -u A e. ZZ ) $=
peano2zd peano2zzd $p |- ( ph -> ( A + 1 ) e. ZZ ) $=
zaddcld zzaddcld $p |- ( ph -> ( A + B ) e. ZZ ) $=
zsubcld zzsubcld $p |- ( ph -> ( A - B ) e. ZZ ) $=
zmulcld zzmulcld $p |- ( ph -> ( A x. B ) e. ZZ ) $=
df-uz df-uzz $a |- ZZ>= = ( j e. ZZ |-> { k e. ZZ | j <_ k } ) $.
uzval uzzval $p |- ( N e. ZZ -> ( ZZ>= ` N ) = { k e. ZZ | N <_ k } ) $=
uzf uzzf $p |- ZZ>= : ZZ --> ~P ZZ $=
eluz1 eluzz1 $p |- ( M e. ZZ ->
eluzel2 eluzzel2 $p |- ( N e. ( ZZ>= ` M ) -> M e. ZZ ) $=
eluz2 eluzz2 $p |- ( N e. ( ZZ>= ` M ) <-> ( M e. ZZ /\ N e. ZZ /\ M <_ N ) ) $=
eluz1i eluzz1i $p |- ( N e. ( ZZ>= ` M ) <-> ( N e. ZZ /\ M <_ N ) ) $=
eluzelz eluzzelzz $p |- ( N e. ( ZZ>= ` M ) -> N e. ZZ ) $=
eluz eluzz $p |- ( ( M e. ZZ /\ N e. ZZ ) ->
uzid uzzid $p |- ( M e. ZZ -> M e. ( ZZ>= ` M ) ) $=
uzssz uzzsszz $p |- ( ZZ>= ` M ) C_ ZZ $=
uztric uzztric $p |- ( ( M e. ZZ /\ N e. ZZ ) ->
uz11 uzz11 $p |- ( M e. ZZ ->
eluzp1m1 eluzzp1m1 $p |- ( ( M e. ZZ /\
eluzp1l eluzzp1l $p |- ( ( M e. ZZ /\
eluzadd eluzzadd $p |- ( ( N e. ( ZZ>= ` M ) /\ K e. ZZ ) ->
eluzsub eluzzsub $p |- ( ( M e. ZZ /\ K e. ZZ /\ N e. ( ZZ>= ` ( M + K ) ) )
uzin uzzin $p |- ( ( M e. ZZ /\ N e. ZZ ) ->
raluz raluzz $p |- ( M e. ZZ -> ( A. n e. ( ZZ>= ` M ) ph <->
rexuz rexuzz $p |- ( M e. ZZ -> ( E. n e. ( ZZ>= ` M ) ph <->
peano2uzr peano2uzzr $p |- ( ( M e. ZZ /\
eluz2b1 eluzz2b1 $p |- ( N e. ( ZZ>= ` 2 ) <-> ( N e. ZZ /\ 1 < N ) ) $=
eqreznegel eqrezznegel $p |- ( A C_ ZZ ->
zsupss zzsupss $p |- ( ( A C_ ZZ /\ A =/= (/) /\ E. x e. ZZ A. y e. A y <_ x ) ->
suprzcl2 suprzzcl2 $p |- ( ( A C_ ZZ /\ A =/= (/) /\ E. x e. ZZ A. y e. A y <_ x ) ->
suprzub suprzzub $p |- ( ( A C_ ZZ /\ E. x e. ZZ A. y e. A y <_ x /\ B e. A ) ->
uzsupss uzzsupss $p |- ( ( M e. ZZ /\ A C_ Z /\ E. x e. ZZ A. y e. A y <_ x ) ->
uzwo3 uzzwo3 $p |- ( ( B e. RR /\ ( A C_ { z e. ZZ | B <_ z } /\ A =/= (/) ) )
zbtwnre zzbtwnre $p |- ( A e. RR -> E! x e. ZZ ( A <_ x /\ x < ( A + 1 ) ) ) $=
rebtwnz rebtwnzz $p |- ( A e. RR -> E! x e. ZZ ( x <_ A /\ A < ( x + 1 ) ) ) $=
qmulz qmulzz $p |- ( A e. QQ -> E. x e. NN ( A x. x ) e. ZZ ) $=
znq zznq $p |- ( ( A e. ZZ /\ B e. NN ) -> ( A / B ) e. QQ ) $=
zq zzq $p |- ( A e. ZZ -> A e. QQ ) $=
zssq zzssq $p |- ZZ C_ QQ $=
z2ge zz2ge $p |- ( ( M e. ZZ /\ N e. ZZ ) ->
df-fz df-fzz $a |- ... = ( m e. ZZ , n e. ZZ |->
fzval fzzval $p |- ( ( M e. ZZ /\ N e. ZZ ) -> ( M ... N ) =
fzval2 fzzval2 $p |- ( ( M e. ZZ /\ N e. ZZ ) ->
fzf fzzf $p |- ... : ( ZZ X. ZZ ) --> ~P ZZ $=
elfz1 elfzz1 $p |- ( ( M e. ZZ /\ N e. ZZ ) -> ( K e. ( M ... N ) <->
elfz elfzz $p |- ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( K e. ( M ... N ) <->
elfz5 elfzz5 $p |- ( ( K e. ( ZZ>= ` M ) /\ N e. ZZ ) ->
elfz4 elfzz4 $p |- ( ( ( M e. ZZ /\ N e. ZZ /\ K e. ZZ ) /\ ( M <_ K /\ K <_ N ) )
elfzel2 elfzzel2 $p |- ( K e. ( M ... N ) -> N e. ZZ ) $=
elfzel1 elfzzel1 $p |- ( K e. ( M ... N ) -> M e. ZZ ) $=
elfzelz elfzzelzz $p |- ( K e. ( M ... N ) -> K e. ZZ ) $=
elfz3 elfzz3 $p |- ( N e. ZZ -> N e. ( N ... N ) ) $=
fzn fzzn $p |- ( ( M e. ZZ /\ N e. ZZ ) -> ( N < M <-> ( M ... N ) = (/) ) ) $=
fzen fzzen $p |- ( ( M e. ZZ /\ N e. ZZ /\ K e. ZZ ) ->
fz01en fzz01en $p |- ( N e. ZZ -> ( 0 ... ( N - 1 ) ) ~~ ( 1 ... N ) ) $=
fzaddel fzzaddel $p |- ( ( ( M e. ZZ /\ N e. ZZ ) /\ ( J e. ZZ /\ K e. ZZ ) ) ->
fzsubel fzzsubel $p |- ( ( ( M e. ZZ /\ N e. ZZ ) /\ ( J e. ZZ /\ K e. ZZ ) ) ->
fzsn fzzsn $p |- ( M e. ZZ -> ( M ... M ) = { M } ) $=
fzp1ss fzzp1ss $p |- ( M e. ZZ -> ( ( M + 1 ) ... N ) C_ ( M ... N ) ) $=
fzpr fzzpr $p |- ( M e. ZZ -> ( M ... ( M + 1 ) ) = { M , ( M + 1 ) } ) $=
fztp fzztp $p |- ( M e. ZZ -> ( M ... ( M + 2 ) )
fzsuc2 fzzsuc2 $p |- ( ( M e. ZZ /\ N e. ( ZZ>= ` ( M - 1 ) ) ) ->
fzrev fzzrev $p |- ( ( ( M e. ZZ /\ N e. ZZ ) /\ ( J e. ZZ /\ K e. ZZ ) ) ->
fzrev2 fzzrev2 $p |- ( ( ( M e. ZZ /\ N e. ZZ ) /\ ( J e. ZZ /\ K e. ZZ ) ) ->
fzrev2i fzzrev2i $p |- ( ( J e. ZZ /\ K e. ( M ... N ) )
fzrev3 fzzrev3 $p |- ( K e. ZZ -> ( K e. ( M ... N )
elfzm11 elfzzm11 $p |- ( ( M e. ZZ /\ N e. ZZ ) -> ( K e. ( M ... ( N - 1 ) ) <->
elfzm1b elfzzm1b $p |- ( ( K e. ZZ /\ N e. ZZ ) ->
fzneuz fzzneuzz $p |- ( ( N e. ( ZZ>= ` M ) /\ K e. ZZ )
fzrevral fzzrevral $p |- ( ( M e. ZZ /\ N e. ZZ /\ K e. ZZ )
fzrevral2 fzzrevral2 $p |- ( ( M e. ZZ /\ N e. ZZ /\ K e. ZZ )
fzrevral3 fzzrevral3 $p |- ( ( M e. ZZ /\ N e. ZZ ) -> ( A. j e. ( M ... N ) ph
fzshftral fzzshftral $p |- ( ( M e. ZZ /\ N e. ZZ /\ K e. ZZ )
df-fzo df-fzzo $a |- ..^ = ( m e. ZZ , n e. ZZ |-> ( m ... ( n - 1 ) ) ) $.
fzof fzzof $p |- ..^ : ( ZZ X. ZZ ) --> ~P ZZ $=
elfzoel1 elfzzoel1 $p |- ( A e. ( B ..^ C ) -> B e. ZZ ) $=
elfzoel2 elfzzoel2 $p |- ( A e. ( B ..^ C ) -> C e. ZZ ) $=
elfzoelz elfzzoelzz $p |- ( A e. ( B ..^ C ) -> A e. ZZ ) $=
fzoval fzzoval $p |- ( N e. ZZ -> ( M ..^ N ) = ( M ... ( N - 1 ) ) ) $=
elfzo elfzzo $p |- ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( K e. ( M ..^ N ) <->
fzolb fzzolb $p |- ( M e. ( M ..^ N ) <-> ( M e. ZZ /\ N e. ZZ /\ M < N ) ) $=
fzolb2 fzzolb2 $p |- ( ( M e. ZZ /\ N e. ZZ ) -> ( M e. ( M ..^ N ) <-> M < N ) ) $=
fzospliti fzzospliti $p |- ( ( A e. ( B ..^ C ) /\ D e. ZZ ) ->
fzoaddel fzzoaddel $p |- ( ( A e. ( B ..^ C ) /\ D e. ZZ ) ->
fzoaddel2 fzzoaddel2 $p |- ( ( A e. ( 0 ..^ ( B - C ) ) /\ B e. ZZ /\ C e. ZZ ) ->
fzosubel fzzosubel $p |- ( ( A e. ( B ..^ C ) /\ D e. ZZ ) ->
fzosubel2 fzzosubel2 $p |- ( ( A e. ( ( B + C ) ..^ ( B + D ) ) /\ ( B e. ZZ /\
fzosubel3 fzzosubel3 $p |- ( ( A e. ( B ..^ ( B + D ) ) /\ D e. ZZ ) ->
fzval3 fzzval3 $p |- ( N e. ZZ -> ( M ... N ) = ( M ..^ ( N + 1 ) ) ) $=
fzosn fzzosn $p |- ( A e. ZZ -> ( A ..^ ( A + 1 ) ) = { A } ) $=
elfzom1b elfzzom1b $p |- ( ( K e. ZZ /\ N e. ZZ ) ->
flidz flidzz $p |- ( A e. RR -> ( ( |_ ` A ) = A <-> A e. ZZ ) ) $=
fladdz fladdzz $p |- ( ( A e. RR /\ N e. ZZ ) -> ( |_ ` ( A + N ) ) =
flzadd flzzadd $p |- ( ( N e. ZZ /\ A e. RR ) -> ( |_ ` ( N + A ) ) =
btwnzge0 btwnzzge0 $p |- ( ( ( A e. RR /\ N e. ZZ ) /\ ( N <_ A /\ A < ( N + 1 ) ) )
quoremz quoremzz $p |- ( ( A e. ZZ /\ B e. NN ) -> ( ( Q e. ZZ /\ R e. NN0 )
uzsup uzzsup $p |- ( M e. ZZ -> sup ( Z , RR* , < ) = +oo ) $=
zmod10 zzmod10 $p |- ( N e. ZZ -> ( N mod 1 ) = 0 ) $=
zmodcl zzmodcl $p |- ( ( A e. ZZ /\ B e. NN ) -> ( A mod B ) e. NN0 ) $=
zmodfz zzmodfzz $p |- ( ( A e. ZZ /\ B e. NN ) ->
zmodfzo zzmodfzzo $p |- ( ( A e. ZZ /\ B e. NN ) -> ( A mod B ) e. ( 0 ..^ B ) ) $=
uzenom uzzenom $p |- ( M e. ZZ -> Z ~~ om ) $=
uzinf uzzinf $p |- ( M e. ZZ -> -. Z e. Fin ) $=
zexpcl zzexpcl $p |- ( ( A e. ZZ /\ N e. NN0 ) -> ( A ^ N ) e. ZZ ) $=
reexpclz reexpclzz $p |- ( ( A e. RR /\ A =/= 0 /\ N e. ZZ ) ->
qexpclz qexpclzz $p |- ( ( A e. QQ /\ A =/= 0 /\ N e. ZZ ) -> ( A ^ N ) e. QQ ) $=
expclzlem expclzzlem $p |- ( ( A e. CC /\ A =/= 0 /\ N e. ZZ ) ->
expclz expclzz $p |- ( ( A e. CC /\ A =/= 0 /\ N e. ZZ ) -> ( A ^ N ) e. CC ) $=
expnegz expnegzz $p |- ( ( A e. CC /\ A =/= 0 /\ N e. ZZ ) ->
expaddz expaddzz $p |- ( ( ( A e. CC /\ A =/= 0 ) /\ ( M e. ZZ /\ N e. ZZ ) ) ->
expmulz expmulzz $p |- ( ( ( A e. CC /\ A =/= 0 ) /\ ( M e. ZZ /\ N e. ZZ ) ) ->
expp1z expp1zz $p |- ( ( A e. CC /\ A =/= 0 /\ N e. ZZ ) -> ( A ^ ( N + 1 ) ) =
zsqcl zzsqcl $p |- ( A e. ZZ -> ( A ^ 2 ) e. ZZ ) $=
zsqcl2 zzsqcl2 $p |- ( A e. ZZ -> ( A ^ 2 ) e. NN0 ) $=
zesq zzesq $p |- ( N e. ZZ ->
fzsdom2 fzzsdom2 $p |- ( ( ( B e. ( ZZ>= ` A ) /\ C e. ZZ ) /\ B < C ) ->
shftuz shftuzz $p |- ( ( A e. ZZ /\ B e. ZZ ) ->
absexpz absexpzz $p |- ( ( A e. CC /\ A =/= 0 /\ N e. ZZ ) ->
absz abszz $p |- ( A e. RR -> ( A e. ZZ <-> ( abs ` A ) e. ZZ ) ) $=
rexanuz rexanuzz $p |- ( E. j e. ZZ A. k e. ( ZZ>= ` j ) ( ph /\ ps ) <->
rexuz3 rexuzz3 $p |- ( M e. ZZ -> ( E. j e. Z A. k e. ( ZZ>= ` j ) ph <->
rexuzre rexuzzre $p |- ( M e. ZZ -> ( E. j e. Z A. k e. ( ZZ>= ` j ) ph <->
climz climzz $p |- ( ZZ X. { 0 } ) ~~> 0 $=
fsumzcl fsumzzcl $p |- ( ph -> sum_ k e. A B e. ZZ ) $=
efzval efzzval $p |- ( N e. ZZ -> ( exp ` N ) = ( _e ^ N ) ) $=
znnenlem zznnenlem $p |- ( ( ( 0 <_ x /\ -. 0 <_ y ) /\ ( x e. ZZ /\ y e. ZZ ) ) ->
znnen zznnen $p |- ZZ ~~ NN $=
nthruz nthruzz $p |- ( NN C. NN0 /\ NN0 C. ZZ ) $=
dvdszrcl dvdszzrcl $p |- ( X || Y -> ( X e. ZZ /\ Y e. ZZ ) ) $=
alzdvds alzzdvds $p |- ( N e. ZZ -> ( A. x e. ZZ x || N <-> N = 0 ) ) $=
bitsfzo bitsfzzo $p |- ( ( N e. ZZ /\ M e. NN0 ) ->
bitsuz bitsuzz $p |- ( ( A e. ZZ /\ N e. NN0 ) ->
bezout bezzout $p |- ( ( A e. ZZ /\ B e. ZZ ) ->
gcdmultiplez gcdmultiplezz $p |- ( ( M e. NN /\ N e. ZZ ) ->
prmz prmzz $p |- ( P e. Prime -> P e. ZZ ) $=
zgcdsq zzgcdsq $p |- ( ( A e. ZZ /\ B e. ZZ ) -> ( ( A gcd B ) ^ 2 ) = ( ( A ^ 2 )
qden1elz qden1elzz $p |- ( A e. QQ -> ( ( denom ` A ) = 1 <-> A e. ZZ ) ) $=
zsqrelqelz zzsqrelqelzz $p |- ( ( A e. ZZ /\ ( sqr ` A ) e. QQ )
df-odz df-odzz $a |- odZ = ( n e. NN |-> ( x e. { x e. ZZ | ( x gcd n ) = 1 } |->
odzval odzzval $p |- ( ( N e. NN /\ A e. ZZ /\ ( A gcd N ) = 1 ) ->
odzcllem odzzcllem $p |- ( ( N e. NN /\ A e. ZZ /\ ( A gcd N ) = 1 ) ->
odzcl odzzcl $p |- ( ( N e. NN /\ A e. ZZ /\ ( A gcd N ) = 1 ) ->
odzid odzzid $p |- ( ( N e. NN /\ A e. ZZ /\ ( A gcd N ) = 1 ) ->
odzdvds odzzdvds $p |- ( ( ( N e. NN /\ A e. ZZ /\ ( A gcd N ) = 1 ) /\ K e. NN0 )
odzphi odzzphi $p |- ( ( N e. NN /\ A e. ZZ /\ ( A gcd N ) = 1 ) ->
pczpre pczzpre $p |- ( ( P e. Prime /\ ( N e. ZZ /\ N =/= 0 ) ) ->
pczcl pczzcl $p |- ( ( P e. Prime /\ ( N e. ZZ /\ N =/= 0 ) ) ->
pczdvds pczzdvds $p |- ( ( P e. Prime /\ ( N e. ZZ /\ N =/= 0 ) ) ->
pczndvds pczzndvds $p |- ( ( P e. Prime /\ ( N e. ZZ /\ N =/= 0 ) ) ->
pczndvds2 pczzndvds2 $p |- ( ( P e. Prime /\ ( N e. ZZ /\ N =/= 0 ) ) ->
pcz pczz $p |- ( A e. QQ -> ( A e. ZZ <-> A. p e. Prime 0 <_ ( p pCnt A ) ) ) $=
qexpz qexpzz $p |- ( ( A e. QQ /\ N e. NN /\ ( A ^ N ) e. ZZ ) ->
df-gz df-gzz $a |- Z[i] = { x e. CC | ( ( Re ` x ) e. ZZ /\ ( Im ` x ) e. ZZ ) } $.
zgz zzgzz $p |- ( A e. ZZ -> A e. Z[i] ) $=
gzreim gzzreim $p |- ( ( A e. ZZ /\ B e. ZZ ) -> ( A + ( _i x. B ) ) e. Z[i] ) $=
mulgz mulgzz $p |- ( ( G e. Grp /\ N e. ZZ ) -> ( N .x. .0. ) = .0. ) $=
odbezout odbezzout $p |- ( ( ( G e. Grp /\ A e. X /\ N e. ZZ ) /\
zsubrg zzsubrg $p |- ZZ e. ( SubRing ` CCfld ) $=
zsssubrg zzsssubrg $p |- ( R e. ( SubRing ` CCfld ) -> ZZ C_ R ) $=
zrngunit zzrngunit $p |- ( A e. ( Unit ` Z ) <-> ( A e. ZZ /\ ( abs ` A ) = 1 ) ) $=
df-zrh df-zzrh $a |- ZRHom = ( r e. _V |-> U. ( ( CCfld |`s ZZ ) RingHom r ) ) $.
df-zn df-zzn $a |- Z/nZ = ( n e. NN0 |-> [_ ( CCfld |`s ZZ ) / z ]_
zrhval2 zzrhval2 $p |- ( R e. Ring -> L = ( n e. ZZ |-> ( n .x. .1. ) ) ) $=
zrhmulg zzrhmulg $p |- ( ( R e. Ring /\ N e. ZZ ) ->
znlidl zznlidl $p |- ( N e. ZZ -> ( S ` { N } ) e. ( LIdeal ` Z ) ) $=
zncrng2 zzncrng2 $p |- ( N e. ZZ -> U e. CRing ) $=
znbas zznbas $p |- ( N e. NN0 -> ( ZZ /. R ) = ( Base ` Y ) ) $=
znzrh2 zznzzrh2 $p |- ( N e. NN0 -> L = ( x e. ZZ |-> [ x ] .~ ) ) $=
znzrhval zznzzrhval $p |- ( ( N e. NN0 /\ A e. ZZ ) -> ( L ` A ) = [ A ] .~ ) $=
znzrhfo zznzzrhfo $p |- ( N e. NN0 -> L : ZZ -onto-> B ) $=
zndvds zzndvds $p |- ( ( N e. NN0 /\ A e. ZZ /\ B e. ZZ ) ->
zndvds0 zzndvds0 $p |- ( ( N e. NN0 /\ A e. ZZ ) ->
zzngim zzzzngim $p |- L e. ( ( CCfld |`s ZZ ) GrpIso Y ) $=
znunit zznunit $p |- ( ( N e. NN0 /\ A e. ZZ ) ->
cygznlem1 cygzznlem1 $p |- ( ( ph /\ ( K e. ZZ /\ M e. ZZ ) ) ->
cygznlem2 cygzznlem2 $p |- ( ( ph /\ M e. ZZ ) ->
zfbas zzfbas $p |- ran ZZ>= e. ( fBas ` ZZ ) $=
uzrest uzzrest $p |- ( M e. ZZ -> ( ran ZZ>= |`t Z ) = ( ZZ>= " Z ) ) $=
uzfbas uzzfbas $p |- ( M e. ZZ -> ( ZZ>= " Z ) e. ( fBas ` Z ) ) $=
zcld zzcld $p |- ZZ e. ( Clsd ` J ) $=
zcld2 zzcld2 $p |- ZZ e. ( Clsd ` J ) $=
zdis zzdis $p |- ( J |`t ZZ ) = ~P ZZ $=
clmzss clmzzss $p |- ( W e. CMod -> ZZ C_ K ) $=
clmzlmvsca clmzzlmvsca $p |- ( ( G e. CMod /\ ( A e. ZZ /\ B e. X ) ) ->
cxpexpz cxpexpzz $p |- ( ( A e. CC /\ A =/= 0 /\ B e. ZZ ) ->
cxpmul2z cxpmul2zz $p |- ( ( ( A e. CC /\ A =/= 0 ) /\ ( B e. CC /\ C e. ZZ ) ) ->
zaddsubgo zzaddsubgo $p |- ( + |` ( ZZ X. ZZ ) ) e. ( SubGrpOp ` + ) $=
ballotlemfelz ballotlemfelzz $p |- ( ph -> ( ( F ` C ) ` J ) e. ZZ ) $=
zmodid2 zzmodid2 $p |- ( ( M e. ZZ /\ N e. NN ) -> ( ( M mod N ) = M <->
elfzp1b elfzzp1b $p |- ( ( K e. ZZ /\ N e. ZZ ) ->
supfz supfzz $p |- ( N e. ( ZZ>= ` M ) -> sup ( ( M ... N ) , ZZ , < ) = N ) $=
inffz inffzz $p |- ( N e. ( ZZ>= ` M ) -> sup ( ( M ... N ) , ZZ , `' < ) = M ) $=
eluzaddOLD eluzzaddOLD $p |- ( ( N e. ( ZZ>= ` M ) /\ K e. ZZ ) ->
eluzsubOLD eluzzsubOLD $p |- ( ( M e. ZZ /\ K e. ZZ /\ N e. ( ZZ>= ` ( M + K ) ) )
fzmul fzzmul $p |- ( ( M e. ZZ /\ N e. ZZ /\ K e. NN ) -> ( J e. ( M ... N ) ->
fzadd2 fzzadd2 $p |- ( ( ( M e. ZZ /\ N e. ZZ ) /\ ( O e. ZZ /\ P e. ZZ ) ) ->
abszOLD abszzOLD $p |- ( A e. RR -> ( A e. ZZ <-> ( abs ` A ) e. ZZ ) ) $=
df-mzpcl df-mzzpcl $a |- mzPolyCld = ( v e. _V |-> { p e. ~P ( ZZ ^m ( ZZ ^m v ) ) |
mzpclall mzzpclall $p |- ( V e. _V -> ( ZZ ^m ( ZZ ^m V ) ) e. ( mzPolyCld ` V ) ) $=
mzpcl1 mzzpcl1 $p |- ( ( P e. ( mzPolyCld ` V ) /\ F e. ZZ ) ->
mzpconst mzzpconst $p |- ( ( V e. _V /\ C e. ZZ ) ->
mzpf mzzpf $p |- ( F e. ( mzPoly ` V ) -> F : ( ZZ ^m V ) --> ZZ ) $=
mzpproj mzzpproj $p |- ( ( V e. _V /\ X e. V ) -> ( g e. ( ZZ ^m V ) |-> ( g ` X ) )
mzpconstmpt mzzpconstmpt $p |- ( ( V e. _V /\ C e. ZZ ) ->
mzpaddmpt mzzpaddmpt $p |- ( ( ( x e. ( ZZ ^m V ) |-> A ) e. ( mzPoly ` V ) /\ ( x e.
mzpmulmpt mzzpmulmpt $p |- ( ( ( x e. ( ZZ ^m V ) |-> A ) e. ( mzPoly ` V ) /\
mzpsubmpt mzzpsubmpt $p |- ( ( ( x e. ( ZZ ^m V ) |-> A ) e. ( mzPoly ` V ) /\
mzpnegmpt mzzpnegmpt $p |- ( ( x e. ( ZZ ^m V ) |-> A ) e. ( mzPoly ` V ) ->
mzpexpmpt mzzpexpmpt $p |- ( ( ( x e. ( ZZ ^m V ) |-> A ) e. ( mzPoly ` V ) /\
mzpmfp mzzpmfp $p |- ( mzPoly ` I ) = ran ( I eval ( CCfld |`s ZZ ) ) $=
ellz1 ellzz1 $p |- ( B e. ZZ -> ( A e. ( ZZ \ ( ZZ>= ` ( B + 1 ) ) ) <-> ( A e. ZZ
lzunuz lzzunuzz $p |- ( ( A e. ZZ /\ B e. ZZ /\ B <_ ( A + 1 ) ) -> ( ( ZZ \ ( ZZ>=
fz1eqin fzz1eqin $p |- ( N e. NN0 -> ( 1 ... N ) = ( ( ZZ \ ( ZZ>= ` ( N + 1 ) ) )
lzenom lzzenom $p |- ( N e. ZZ -> ( ZZ \ ( ZZ>= ` ( N + 1 ) ) ) ~~ om ) $=
rexzrexnn0 rexzzrexnn0 $p |- ( E. x e. ZZ ph <-> E. y e. NN0 ( ps \/ ch ) ) $=
eluzrabdioph eluzzrabdioph $p |- ( ( N e. NN0 /\ M e. ZZ /\ ( t e. ( ZZ ^m ( 1 ... N ) )
monotoddzzfi monotoddzzzzfi $p |- ( ( ph /\ A e. ZZ /\ B e. ZZ ) -> ( A < B <-> ( F ` A )
monotoddzz monotoddzzzz $p |- ( ( ph /\ A e. ZZ /\ B e. ZZ ) -> ( A < B <-> C < D ) ) $=
oddcomabszz oddcomabszzzz $p |- ( ( ph /\ D e. ZZ ) -> ( abs ` E ) = F ) $=
zindbi zzindbi $p |- ( A e. ZZ -> ( th <-> ta ) ) $=
mzpcong mzzpcong $p |- ( ( F e. ( mzPoly ` V ) /\ ( X e. ( ZZ ^m V ) /\ Y e. ( ZZ ^m
fzmaxdif fzzmaxdif $p |- ( ( ( C e. ZZ /\ A e. ( B ... C ) ) /\ ( F e. ZZ /\ D e. ( E
fzneg fzzneg $p |- ( ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) -> ( A e. ( B ... C ) <-> -u
bezoutr bezzoutr $p |- ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( X e. ZZ /\ Y e. ZZ ) ) -> ( A
bezoutr1 bezzoutr1 $p |- ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( X e. ZZ /\ Y e. ZZ ) ) -> ( (
zabscl zzabscl $p |- ( A e. ZZ -> ( abs ` A ) e. ZZ ) $=

[Mario Carneiro]

Before I forget: "df-divides" is inconsistent with the label fragment "dvds" (it is also used on a few of the definitional theorems).

Here is the list of all the ones that should NOT be renamed out of that list:

peano2uz2 peano2uzz2 $p |- ( ( A e. ZZ /\ B e. { x e. ZZ | A <_ x } ) ->
peano5uzti peano5uzzti $p |- ( N e. ZZ -> ( ( N e. A /\ A. x e. A ( x + 1 ) e. A )
dfuzi dfuzzi $p |- { z e. ZZ | N <_ z } =
uzind uzzind $p |- ( ( M e. ZZ /\ N e. ZZ /\ M <_ N ) -> ta ) $=
uzind2 uzzind2 $p |- ( ( M e. ZZ /\ N e. ZZ /\ M < N ) -> ta ) $=
uzind3 uzzind3 $p |- ( ( M e. ZZ /\ N e. { k e. ZZ | M <_ k } ) -> ta ) $=
uzindOLD uzzindOLD $p |- ( ( ( A e. ZZ /\ B e. ZZ ) /\ B <_ A ) -> ta ) $=
uzind3OLD uzzind3OLD $p |- ( ( B e. ZZ /\ A e. { z e. ZZ | B <_ z } ) -> ta ) $=
fzind fzzind $p |- ( ( ( M e. ZZ /\ N e. ZZ ) /\

 

df-uz df-uzz $a |- ZZ>= = ( j e. ZZ |-> { k e. ZZ | j <_ k } ) $.

uzval uzzval $p |- ( N e. ZZ -> ( ZZ>= ` N ) = { k e. ZZ | N <_ k } ) $=
uzf uzzf $p |- ZZ>= : ZZ --> ~P ZZ $=
eluz1 eluzz1 $p |- ( M e. ZZ ->
eluzel2 eluzzel2 $p |- ( N e. ( ZZ>= ` M ) -> M e. ZZ ) $=
eluz2 eluzz2 $p |- ( N e. ( ZZ>= ` M ) <-> ( M e. ZZ /\ N e. ZZ /\ M <_ N ) ) $=
eluz1i eluzz1i $p |- ( N e. ( ZZ>= ` M ) <-> ( N e. ZZ /\ M <_ N ) ) $=
eluzelz eluzzelzz $p |- ( N e. ( ZZ>= ` M ) -> N e. ZZ ) $=
eluz eluzz $p |- ( ( M e. ZZ /\ N e. ZZ ) ->
uzid uzzid $p |- ( M e. ZZ -> M e. ( ZZ>= ` M ) ) $=
uzssz uzzsszz $p |- ( ZZ>= ` M ) C_ ZZ $=
uztric uzztric $p |- ( ( M e. ZZ /\ N e. ZZ ) ->
uz11 uzz11 $p |- ( M e. ZZ ->
eluzp1m1 eluzzp1m1 $p |- ( ( M e. ZZ /\
eluzp1l eluzzp1l $p |- ( ( M e. ZZ /\
eluzadd eluzzadd $p |- ( ( N e. ( ZZ>= ` M ) /\ K e. ZZ ) ->
eluzsub eluzzsub $p |- ( ( M e. ZZ /\ K e. ZZ /\ N e. ( ZZ>= ` ( M + K ) ) )
uzin uzzin $p |- ( ( M e. ZZ /\ N e. ZZ ) ->
raluz raluzz $p |- ( M e. ZZ -> ( A. n e. ( ZZ>= ` M ) ph <->
rexuz rexuzz $p |- ( M e. ZZ -> ( E. n e. ( ZZ>= ` M ) ph <->
peano2uzr peano2uzzr $p |- ( ( M e. ZZ /\
eluz2b1 eluzz2b1 $p |- ( N e. ( ZZ>= ` 2 ) <-> ( N e. ZZ /\ 1 < N ) ) $=

 

uzsupss uzzsupss $p |- ( ( M e. ZZ /\ A C_ Z /\ E. x e. ZZ A. y e. A y <_ x ) ->

uzwo3 uzzwo3 $p |- ( ( B e. RR /\ ( A C_ { z e. ZZ | B <_ z } /\ A =/= (/) ) )

 

df-fz df-fzz $a |- ... = ( m e. ZZ , n e. ZZ |->

 

uzsup uzzsup $p |- ( M e. ZZ -> sup ( Z , RR* , < ) = +oo ) $=

 

uzenom uzzenom $p |- ( M e. ZZ -> Z ~~ om ) $=

uzinf uzzinf $p |- ( M e. ZZ -> -. Z e. Fin ) $=

 

fzsdom2 fzzsdom2 $p |- ( ( ( B e. ( ZZ>= ` A ) /\ C e. ZZ ) /\ B < C ) ->

shftuz shftuzz $p |- ( ( A e. ZZ /\ B e. ZZ ) ->

 

rexanuz rexanuzz $p |- ( E. j e. ZZ A. k e. ( ZZ>= ` j ) ( ph /\ ps ) <->

rexuz3 rexuzz3 $p |- ( M e. ZZ -> ( E. j e. Z A. k e. ( ZZ>= ` j ) ph <->
rexuzre rexuzzre $p |- ( M e. ZZ -> ( E. j e. Z A. k e. ( ZZ>= ` j ) ph <->

 

bitsfzo bitsfzzo $p |- ( ( N e. ZZ /\ M e. NN0 ) ->

bitsuz bitsuzz $p |- ( ( A e. ZZ /\ N e. NN0 ) ->
bezout bezzout $p |- ( ( A e. ZZ /\ B e. ZZ ) ->

 

df-odz df-odzz $a |- odZ = ( n e. NN |-> ( x e. { x e. ZZ | ( x gcd n ) = 1 } |->

odzval odzzval $p |- ( ( N e. NN /\ A e. ZZ /\ ( A gcd N ) = 1 ) ->
odzcllem odzzcllem $p |- ( ( N e. NN /\ A e. ZZ /\ ( A gcd N ) = 1 ) ->
odzcl odzzcl $p |- ( ( N e. NN /\ A e. ZZ /\ ( A gcd N ) = 1 ) ->
odzid odzzid $p |- ( ( N e. NN /\ A e. ZZ /\ ( A gcd N ) = 1 ) ->
odzdvds odzzdvds $p |- ( ( ( N e. NN /\ A e. ZZ /\ ( A gcd N ) = 1 ) /\ K e. NN0 )
odzphi odzzphi $p |- ( ( N e. NN /\ A e. ZZ /\ ( A gcd N ) = 1 ) ->

 

df-gz df-gzz $a |- Z[i] = { x e. CC | ( ( Re ` x ) e. ZZ /\ ( Im ` x ) e. ZZ ) } $.

zgz zzgzz $p |- ( A e. ZZ -> A e. Z[i] ) $=

This one should be zzgz

 

gzreim gzzreim $p |- ( ( A e. ZZ /\ B e. ZZ ) -> ( A + ( _i x. B ) ) e. Z[i] ) $=
mulgz mulgzz $p |- ( ( G e. Grp /\ N e. ZZ ) -> ( N .x. .0. ) = .0. ) $= 

odbezout odbezzout $p |- ( ( ( G e. Grp /\ A e. X /\ N e. ZZ ) /\

 

df-zrh df-zzrh $a |- ZRHom = ( r e. _V |-> U. ( ( CCfld |`s ZZ ) RingHom r ) ) $.

df-zn df-zzn $a |- Z/nZ = ( n e. NN0 |-> [_ ( CCfld |`s ZZ ) / z ]_
zrhval2 zzrhval2 $p |- ( R e. Ring -> L = ( n e. ZZ |-> ( n .x. .1. ) ) ) $=
zrhmulg zzrhmulg $p |- ( ( R e. Ring /\ N e. ZZ ) ->
znlidl zznlidl $p |- ( N e. ZZ -> ( S ` { N } ) e. ( LIdeal ` Z ) ) $=
zncrng2 zzncrng2 $p |- ( N e. ZZ -> U e. CRing ) $=
znbas zznbas $p |- ( N e. NN0 -> ( ZZ /. R ) = ( Base ` Y ) ) $=
znzrh2 zznzzrh2 $p |- ( N e. NN0 -> L = ( x e. ZZ |-> [ x ] .~ ) ) $=
znzrhval zznzzrhval $p |- ( ( N e. NN0 /\ A e. ZZ ) -> ( L ` A ) = [ A ] .~ ) $=
znzrhfo zznzzrhfo $p |- ( N e. NN0 -> L : ZZ -onto-> B ) $=
zndvds zzndvds $p |- ( ( N e. NN0 /\ A e. ZZ /\ B e. ZZ ) ->
zndvds0 zzndvds0 $p |- ( ( N e. NN0 /\ A e. ZZ ) ->
zzngim zzzzngim $p |- L e. ( ( CCfld |`s ZZ ) GrpIso Y ) $=
znunit zznunit $p |- ( ( N e. NN0 /\ A e. ZZ ) ->
cygznlem1 cygzznlem1 $p |- ( ( ph /\ ( K e. ZZ /\ M e. ZZ ) ) ->
cygznlem2 cygzznlem2 $p |- ( ( ph /\ M e. ZZ ) ->

 

uzrest uzzrest $p |- ( M e. ZZ -> ( ran ZZ>= |`t Z ) = ( ZZ>= " Z ) ) $=

uzfbas uzzfbas $p |- ( M e. ZZ -> ( ZZ>= " Z ) e. ( fBas ` Z ) ) $=

 

elfzp1b elfzzp1b $p |- ( ( K e. ZZ /\ N e. ZZ ) ->

supfz supfzz $p |- ( N e. ( ZZ>= ` M ) -> sup ( ( M ... N ) , ZZ , < ) = N ) $=
inffz inffzz $p |- ( N e. ( ZZ>= ` M ) -> sup ( ( M ... N ) , ZZ , `' < ) = M ) $=

 

eluzaddOLD eluzzaddOLD $p |- ( ( N e. ( ZZ>= ` M ) /\ K e. ZZ ) ->
eluzsubOLD eluzzsubOLD $p |- ( ( M e. ZZ /\ K e. ZZ /\ N e. ( ZZ>= ` ( M + K ) ) )
fzmul fzzmul $p |- ( ( M e. ZZ /\ N e. ZZ /\ K e. NN ) -> ( J e. ( M ... N ) ->
fzadd2 fzzadd2 $p |- ( ( ( M e. ZZ /\ N e. ZZ ) /\ ( O e. ZZ /\ P e. ZZ ) ) ->

 

df-mzpcl df-mzzpcl $a |- mzPolyCld = ( v e. _V |-> { p e. ~P ( ZZ ^m ( ZZ ^m v ) ) |

mzpclall mzzpclall $p |- ( V e. _V -> ( ZZ ^m ( ZZ ^m V ) ) e. ( mzPolyCld ` V ) ) $=
mzpcl1 mzzpcl1 $p |- ( ( P e. ( mzPolyCld ` V ) /\ F e. ZZ ) ->
mzpconst mzzpconst $p |- ( ( V e. _V /\ C e. ZZ ) ->
mzpf mzzpf $p |- ( F e. ( mzPoly ` V ) -> F : ( ZZ ^m V ) --> ZZ ) $=
mzpproj mzzpproj $p |- ( ( V e. _V /\ X e. V ) -> ( g e. ( ZZ ^m V ) |-> ( g ` X ) )
mzpconstmpt mzzpconstmpt $p |- ( ( V e. _V /\ C e. ZZ ) ->
mzpaddmpt mzzpaddmpt $p |- ( ( ( x e. ( ZZ ^m V ) |-> A ) e. ( mzPoly ` V ) /\ ( x e.
mzpmulmpt mzzpmulmpt $p |- ( ( ( x e. ( ZZ ^m V ) |-> A ) e. ( mzPoly ` V ) /\
mzpsubmpt mzzpsubmpt $p |- ( ( ( x e. ( ZZ ^m V ) |-> A ) e. ( mzPoly ` V ) /\
mzpnegmpt mzzpnegmpt $p |- ( ( x e. ( ZZ ^m V ) |-> A ) e. ( mzPoly ` V ) ->
mzpexpmpt mzzpexpmpt $p |- ( ( ( x e. ( ZZ ^m V ) |-> A ) e. ( mzPoly ` V ) /\
mzpmfp mzzpmfp $p |- ( mzPoly ` I ) = ran ( I eval ( CCfld |`s ZZ ) ) $=
ellz1 ellzz1 $p |- ( B e. ZZ -> ( A e. ( ZZ \ ( ZZ>= ` ( B + 1 ) ) ) <-> ( A e. ZZ
lzunuz lzzunuzz $p |- ( ( A e. ZZ /\ B e. ZZ /\ B <_ ( A + 1 ) ) -> ( ( ZZ \ ( ZZ>=
fz1eqin fzz1eqin $p |- ( N e. NN0 -> ( 1 ... N ) = ( ( ZZ \ ( ZZ>= ` ( N + 1 ) ) )
lzenom lzzenom $p |- ( N e. ZZ -> ( ZZ \ ( ZZ>= ` ( N + 1 ) ) ) ~~ om ) $=

 

eluzrabdioph eluzzrabdioph $p |- ( ( N e. NN0 /\ M e. ZZ /\ ( t e. ( ZZ ^m ( 1 ... N ) )

monotoddzzfi monotoddzzzzfi $p |- ( ( ph /\ A e. ZZ /\ B e. ZZ ) -> ( A < B <-> ( F ` A )
monotoddzz monotoddzzzz $p |- ( ( ph /\ A e. ZZ /\ B e. ZZ ) -> ( A < B <-> C < D ) ) $=
oddcomabszz oddcomabszzzz $p |- ( ( ph /\ D e. ZZ ) -> ( abs ` E ) = F ) $=

 

mzpcong mzzpcong $p |- ( ( F e. ( mzPoly ` V ) /\ ( X e. ( ZZ ^m V ) /\ Y e. ( ZZ ^m

[Norman Megill]

To me, "0" is natural to abbreviate the empty set, whereas "es" seems weird.  There is no essential confusion because theorems about (/) and the number 0 are in different sections, and (/) isn't common in complex number theorems.  Books often use 0 to denote both.

I have mixed feelings about using "z" for (/).  While the symbol 0 is used books to denote the empty set, I think it is rare for word "zero" to be used to describe the empty set outside of the context of ordinal numbers.

But even if we adopt z for (/) in basic set theory, the "z" meaning integer is in a different section.  It seems you are trying to impose a context-free universal label convention on all of set.mm, which is not necessarily a positive thing if it leads to longer labels.  Our CC subsets are now abbreviated cn (complex numbers), re (reals), nn (natural numbers), nn0 (natural numbers including 0), z (integers [zahlen]), q (rationals [quotient]).  cn, re, and nn use 2 letters since c, r, n are often used for other things. "zz" doesn't mean anything (zahlen zahlen?) unless it's to mimic the ZZ we use for blackboard bold; but if that's the pattern, then we should also use cc, rr, qq to be consistent.  But the double-letter ASCII token is not shown on the web page, so it would not necessarily be meaningful to someone not familiar with the source file.

The goal with labels is to represent patterns that are easy to remember and easy to type.  Obviously that is very subjective, but imposing longer names to be able to reverse-engineer the theorem from the label isn't our goal.

Norm

[Mario Carneiro]

On Fri, Jul 21, 2017 at 12:53 AM, Norman Megill <n...@alum.mit.edu> wrote:

To me, "0" is natural to abbreviate the empty set, whereas "es" seems weird.  There is no essential confusion because theorems about (/) and the number 0 are in different sections, and (/) isn't common in complex number theorems.  Books often use 0 to denote both.

I have mixed feelings about using "z" for (/).  While the symbol 0 is used books to denote the empty set, I think it is rare for word "zero" to be used to describe the empty set outside of the context of ordinal numbers.

But even if we adopt z for (/) in basic set theory, the "z" meaning integer is in a different section.  It seems you are trying to impose a context-free universal label convention on all of set.mm, which is not necessarily a positive thing if it leads to longer labels.

I have to second this. The label convention system is not 100% consistent, and is not unambiguous. But as long as there are reasonably good reasons for the inconsistencies that exist, I don't think it is a bad thing.

 

  Our CC subsets are now abbreviated cn (complex numbers), re (reals), nn (natural numbers), nn0 (natural numbers including 0), z (integers [zahlen]), q (rationals [quotient]).  cn, re, and nn use 2 letters since c, r, n are often used for other things. "zz" doesn't mean anything (zahlen zahlen?) unless it's to mimic the ZZ we use for blackboard bold; but if that's the pattern, then we should also use cc, rr, qq to be consistent.

I think that's David's plan, although he wants to do it one letter at a time for some reason.
 

  But the double-letter ASCII token is not shown on the web page, so it would not necessarily be meaningful to someone not familiar with the source file.

I don't think this is necessarily a problem; label fragments have always had their own internal consistency which is somewhat separate from the symbol used. Even without reading the source, with enough examples people would make the connection "integers = zz" even if it's not so clear why that particular fragment is used.
 

The goal with labels is to represent patterns that are easy to remember and easy to type.  Obviously that is very subjective, but imposing longer names to be able to reverse-engineer the theorem from the label isn't our goal.

I think you would acknowledge that the goal of labels is to be able to reverse-engineer the label from the statement (with practice), and a uniform label convention assists in this effort. It is worth noting, though, that as long as we are going from statement -> label, there is no need for delimiters between label fragments or unique label fragments. In particular, this model of the recall process justifies inconsistencies whenever the inconsistency is sufficiently strongly associated to the statement or pattern. (Case study: syl instead of imtri)

Mario

[David A. Wheeler]

> On Fri, Jul 21, 2017 at 12:53 AM, Norman Megill <n...@alum.mit.edu> wrote:
> > To me, "0" is natural to abbreviate the empty set, whereas "es" seems

> > weird....
> > I have mixed feelings about using "z" for (/)....

> > But even if we adopt z for (/) in basic set theory, the "z" meaning
> > integer is in a different section. It seems you are trying to impose a
> > context-free universal label convention on all of set.mm, which is not
> > necessarily a positive thing if it leads to longer labels.

On Fri, 21 Jul 2017 01:22:58 +0100, Mario Carneiro <di....@gmail.com> wrote:
> I have to second this. The label convention system is not 100% consistent,
> and is not unambiguous. But as long as there are reasonably good reasons
> for the inconsistencies that exist, I don't think it is a bad thing.

I'm *fine* with inconsistencies, but they need to:
1. actually have reasonably good reasons,
2. be *documented* (if there's a different rule), and
3. have only a limited number
(if everything is an exception it's a nightmare).

In particular: if there's a df-NAME that consistently uses a fragment
other than NAME, then I think there is an *obligation* to document that,
and we should strive to limit those situations.

So: if (/) is defined in "df-nul", but is consistently marked as "0" in labels,
that needs to be *documented*. I personally think that
"z" would be better (so you can use "df-z" and be totally consistent),
but if not, let's agree that it should be *documented*.

I currently have a "Syntax?" column in the naming table. I think I
should change that column to "Match df?". It would then be "yes" if
the conventional fragment matches the text after its "df-...", else no.
That would make exceptions much more obvious, and would mean that
I would no longer have to decide if a structure was "syntax".
Any objections to that?

If I switch to "Match df?", I think we should strive to (eventually) list in the
table *every* case where a fragment is normally *not* the same as
what's after df-. That way people can find, in one place, all the
other conventions.

> > ... "zz" doesn't mean anything (zahlen

> > zahlen?) unless it's to mimic the ZZ we use for blackboard bold; but if
> > that's the pattern, then we should also use cc, rr, qq to be consistent.
> I think that's David's plan, although he wants to do it one letter at a
> time for some reason.

Yes, that is my plan. It turns out that df-cc, df-rr, df-qq are all unused,
so it's quite plausible to switch to that convention.
The reason I'd rather do it one letter at a time is simply
because I find it harder to review "all the changes at once".

I could do it all at once if that's important to someone.

> > But the double-letter ASCII token is not shown on the web page, so it
> > would not necessarily be meaningful to someone not familiar with the source
> > file.

I think "doubled letter for blackboard bold" is a pretty clear convention,
even if you only saw the blackboard bold letters.

> I don't think this is necessarily a problem; label fragments have always
> had their own internal consistency which is somewhat separate from the
> symbol used. Even without reading the source, with enough examples people
> would make the connection "integers = zz" even if it's not so clear why
> that particular fragment is used.

More importantly, we've now (for the first time) documented that when there's
a definition df-NAME, the label fragment is normally NAME. So if "df-zz" is
the definition for ZZ, then they'll know that the label fragment is probably "zz".

> I think you would acknowledge that the goal of labels is to be able to
> reverse-engineer the label from the statement (with practice), and a
> uniform label convention assists in this effort. It is worth noting,
> though, that as long as we are going from statement -> label, there is no
> need for delimiters between label fragments or unique label fragments. In
> particular, this model of the recall process justifies inconsistencies
> whenever the inconsistency is sufficiently strongly associated to the
> statement or pattern. (Case study: syl instead of imtri)

Agreed. I'm not trying to make it possible to uniquely map a
label to a statement; that would require much longer labels.
But it'd be nice to be able to easily guess, from just a statement, what
the label *probably* is, just by knowing the names of the definitions
and without memorizing a long list of exceptions
(CC uses "cn" even though it's defined in df-c, (/) uses "z" even though it's
defined in df-nul, etc.). There are some advantages in making it relatively
easy to guess the other direction (label to some plausible statements);
more consistency would help that way too.

--- David A. Wheeler

[David A. Wheeler]

On Thu, 20 Jul 2017 23:16:09 +0100, Mario Carneiro <di....@gmail.com> wrote:
> Before I forget: "df-divides" is inconsistent with the label fragment
> "dvds" (it is also used on a few of the definitional theorems).

Good info. I've added it to the name table so it won't be forgotten.

> Here is the list of all the ones that should NOT be renamed out of that

> list:..

Thanks so much!!
I hand-edited the list to remove the ones you noted.
Whew, next time I'll run a script to do that!

Below is what I think is the final list of changes to change "df-z" to "df-zz"
and change all matching labels to use "zz" for consistency's sake.
It's a surprisingly short list for such a broad change.

ZZ and QQ are the only cases where labels get *longer*, and since
there are relatively few theorems involving QQ, the list below is
practically *all* of the impact. I don't think we significantly
increase the uncompressed file size to create this consistency.
The potential consistency gains are at least:
* All blackboard-font set names are doubled letters (consistently)
* All blackboard-font label fragments match their definition name
(no need to explain the exceptions)
* Given a label, it's somewhat easier to guess what it probably refers to
(by reducing the number of one-letter fragments). There would
still be ambiguities, I'm not trying to eliminate that.
That's not a primary reason, but it's nice to have.

After this, I'd do the others. For example:
NN: df-n => df-nn, almost nothing else changes.
CC: df-c => df-cc, fragments "cn" become "cc".
RR: df-r => df-rr, fragments "re" become "rr"
QQ: df-q => df-qq, fragments "q" become "qq"

I expect the others to be easier to do (two-character matches are less
likely to mismatch, are there are few that involve QQ).

So for example, "zzcc" would represent ` ( N e. ZZ -> N e. CC ) `
instead of the current name "zcn".

So... thoughts? Should we proceed in this direction?
I think we should, but I thought it'd be easier to *show* a little of
what the changes would look like so we can reasonably discuss them.

--- David A. Wheeler

============================================

zeo2 zzeo2 $p |- ( N e. ZZ ->

zindd zzindd $p |- ( ze -> ( A e. ZZ -> et ) ) $=
btwnz btwnzz $p |- ( A e. RR -> ( E. x e. ZZ x < A /\ E. y e. ZZ A < y ) ) $=
nn0zd nn0zzd $p |- ( ph -> A e. ZZ ) $=
nnzd nnzzd $p |- ( ph -> A e. ZZ ) $=
znegcld zznegcld $p |- ( ph -> -u A e. ZZ ) $=
peano2zd peano2zzd $p |- ( ph -> ( A + 1 ) e. ZZ ) $=
zaddcld zzaddcld $p |- ( ph -> ( A + B ) e. ZZ ) $=
zsubcld zzsubcld $p |- ( ph -> ( A - B ) e. ZZ ) $=

zmulcld zzmulcld $p |- ( ph -> ( A x. B ) e. ZZ ) $=

eqreznegel eqrezznegel $p |- ( A C_ ZZ ->
zsupss zzsupss $p |- ( ( A C_ ZZ /\ A =/= (/) /\ E. x e. ZZ A. y e. A y <_ x ) ->
suprzcl2 suprzzcl2 $p |- ( ( A C_ ZZ /\ A =/= (/) /\ E. x e. ZZ A. y e. A y <_ x ) ->
suprzub suprzzub $p |- ( ( A C_ ZZ /\ E. x e. ZZ A. y e. A y <_ x /\ B e. A ) ->

zbtwnre zzbtwnre $p |- ( A e. RR -> E! x e. ZZ ( A <_ x /\ x < ( A + 1 ) ) ) $=
rebtwnz rebtwnzz $p |- ( A e. RR -> E! x e. ZZ ( x <_ A /\ A < ( x + 1 ) ) ) $=
qmulz qmulzz $p |- ( A e. QQ -> E. x e. NN ( A x. x ) e. ZZ ) $=
znq zznq $p |- ( ( A e. ZZ /\ B e. NN ) -> ( A / B ) e. QQ ) $=
zq zzq $p |- ( A e. ZZ -> A e. QQ ) $=
zssq zzssq $p |- ZZ C_ QQ $=

z2ge zz2ge $p |- ( ( M e. ZZ /\ N e. ZZ ) ->

flidz flidzz $p |- ( A e. RR -> ( ( |_ ` A ) = A <-> A e. ZZ ) ) $=
fladdz fladdzz $p |- ( ( A e. RR /\ N e. ZZ ) -> ( |_ ` ( A + N ) ) =
flzadd flzzadd $p |- ( ( N e. ZZ /\ A e. RR ) -> ( |_ ` ( N + A ) ) =
btwnzge0 btwnzzge0 $p |- ( ( ( A e. RR /\ N e. ZZ ) /\ ( N <_ A /\ A < ( N + 1 ) ) )
quoremz quoremzz $p |- ( ( A e. ZZ /\ B e. NN ) -> ( ( Q e. ZZ /\ R e. NN0 )

zmod10 zzmod10 $p |- ( N e. ZZ -> ( N mod 1 ) = 0 ) $=
zmodcl zzmodcl $p |- ( ( A e. ZZ /\ B e. NN ) -> ( A mod B ) e. NN0 ) $=
zmodfz zzmodfzz $p |- ( ( A e. ZZ /\ B e. NN ) ->
zmodfzo zzmodfzzo $p |- ( ( A e. ZZ /\ B e. NN ) -> ( A mod B ) e. ( 0 ..^ B ) ) $=

zexpcl zzexpcl $p |- ( ( A e. ZZ /\ N e. NN0 ) -> ( A ^ N ) e. ZZ ) $=
reexpclz reexpclzz $p |- ( ( A e. RR /\ A =/= 0 /\ N e. ZZ ) ->
qexpclz qexpclzz $p |- ( ( A e. QQ /\ A =/= 0 /\ N e. ZZ ) -> ( A ^ N ) e. QQ ) $=
expclzlem expclzzlem $p |- ( ( A e. CC /\ A =/= 0 /\ N e. ZZ ) ->
expclz expclzz $p |- ( ( A e. CC /\ A =/= 0 /\ N e. ZZ ) -> ( A ^ N ) e. CC ) $=
expnegz expnegzz $p |- ( ( A e. CC /\ A =/= 0 /\ N e. ZZ ) ->
expaddz expaddzz $p |- ( ( ( A e. CC /\ A =/= 0 ) /\ ( M e. ZZ /\ N e. ZZ ) ) ->
expmulz expmulzz $p |- ( ( ( A e. CC /\ A =/= 0 ) /\ ( M e. ZZ /\ N e. ZZ ) ) ->
expp1z expp1zz $p |- ( ( A e. CC /\ A =/= 0 /\ N e. ZZ ) -> ( A ^ ( N + 1 ) ) =
zsqcl zzsqcl $p |- ( A e. ZZ -> ( A ^ 2 ) e. ZZ ) $=
zsqcl2 zzsqcl2 $p |- ( A e. ZZ -> ( A ^ 2 ) e. NN0 ) $=

zesq zzesq $p |- ( N e. ZZ ->
absexpz absexpzz $p |- ( ( A e. CC /\ A =/= 0 /\ N e. ZZ ) ->
absz abszz $p |- ( A e. RR -> ( A e. ZZ <-> ( abs ` A ) e. ZZ ) ) $=

climz climzz $p |- ( ZZ X. { 0 } ) ~~> 0 $=
fsumzcl fsumzzcl $p |- ( ph -> sum_ k e. A B e. ZZ ) $=
efzval efzzval $p |- ( N e. ZZ -> ( exp ` N ) = ( _e ^ N ) ) $=
znnenlem zznnenlem $p |- ( ( ( 0 <_ x /\ -. 0 <_ y ) /\ ( x e. ZZ /\ y e. ZZ ) ) ->
znnen zznnen $p |- ZZ ~~ NN $=
nthruz nthruzz $p |- ( NN C. NN0 /\ NN0 C. ZZ ) $=
dvdszrcl dvdszzrcl $p |- ( X || Y -> ( X e. ZZ /\ Y e. ZZ ) ) $=
alzdvds alzzdvds $p |- ( N e. ZZ -> ( A. x e. ZZ x || N <-> N = 0 ) ) $=

gcdmultiplez gcdmultiplezz $p |- ( ( M e. NN /\ N e. ZZ ) ->
prmz prmzz $p |- ( P e. Prime -> P e. ZZ ) $=
zgcdsq zzgcdsq $p |- ( ( A e. ZZ /\ B e. ZZ ) -> ( ( A gcd B ) ^ 2 ) = ( ( A ^ 2 )
qden1elz qden1elzz $p |- ( A e. QQ -> ( ( denom ` A ) = 1 <-> A e. ZZ ) ) $=
zsqrelqelz zzsqrelqelzz $p |- ( ( A e. ZZ /\ ( sqr ` A ) e. QQ )

pczpre pczzpre $p |- ( ( P e. Prime /\ ( N e. ZZ /\ N =/= 0 ) ) ->
pczcl pczzcl $p |- ( ( P e. Prime /\ ( N e. ZZ /\ N =/= 0 ) ) ->
pczdvds pczzdvds $p |- ( ( P e. Prime /\ ( N e. ZZ /\ N =/= 0 ) ) ->
pczndvds pczzndvds $p |- ( ( P e. Prime /\ ( N e. ZZ /\ N =/= 0 ) ) ->
pczndvds2 pczzndvds2 $p |- ( ( P e. Prime /\ ( N e. ZZ /\ N =/= 0 ) ) ->
pcz pczz $p |- ( A e. QQ -> ( A e. ZZ <-> A. p e. Prime 0 <_ ( p pCnt A ) ) ) $=
qexpz qexpzz $p |- ( ( A e. QQ /\ N e. NN /\ ( A ^ N ) e. ZZ ) ->

zgz zzgz $p |- ( A e. ZZ -> A e. Z[i] ) $=

zsubrg zzsubrg $p |- ZZ e. ( SubRing ` CCfld ) $=
zsssubrg zzsssubrg $p |- ( R e. ( SubRing ` CCfld ) -> ZZ C_ R ) $=
zrngunit zzrngunit $p |- ( A e. ( Unit ` Z ) <-> ( A e. ZZ /\ ( abs ` A ) = 1 ) ) $=

zfbas zzfbas $p |- ran ZZ>= e. ( fBas ` ZZ ) $=

zcld zzcld $p |- ZZ e. ( Clsd ` J ) $=
zcld2 zzcld2 $p |- ZZ e. ( Clsd ` J ) $=
zdis zzdis $p |- ( J |`t ZZ ) = ~P ZZ $=
clmzss clmzzss $p |- ( W e. CMod -> ZZ C_ K ) $=
clmzlmvsca clmzzlmvsca $p |- ( ( G e. CMod /\ ( A e. ZZ /\ B e. X ) ) ->
cxpexpz cxpexpzz $p |- ( ( A e. CC /\ A =/= 0 /\ B e. ZZ ) ->
cxpmul2z cxpmul2zz $p |- ( ( ( A e. CC /\ A =/= 0 ) /\ ( B e. CC /\ C e. ZZ ) ) ->
zaddsubgo zzaddsubgo $p |- ( + |` ( ZZ X. ZZ ) ) e. ( SubGrpOp ` + ) $=
ballotlemfelz ballotlemfelzz $p |- ( ph -> ( ( F ` C ) ` J ) e. ZZ ) $=
zmodid2 zzmodid2 $p |- ( ( M e. ZZ /\ N e. NN ) -> ( ( M mod N ) = M <->

abszOLD abszzOLD $p |- ( A e. RR -> ( A e. ZZ <-> ( abs ` A ) e. ZZ ) ) $=

rexzrexnn0 rexzzrexnn0 $p |- ( E. x e. ZZ ph <-> E. y e. NN0 ( ps \/ ch ) ) $=

[Mario Carneiro]

On Fri, Jul 21, 2017 at 3:04 AM, David A. Wheeler <dwhe...@dwheeler.com> wrote:

> On Fri, Jul 21, 2017 at 12:53 AM, Norman Megill <n...@alum.mit.edu> wrote:
> > To me, "0" is natural to abbreviate the empty set, whereas "es" seems
> > weird....
> > I have mixed feelings about using "z" for (/)....
> > But even if we adopt z for (/) in basic set theory, the "z" meaning
> > integer is in a different section.  It seems you are trying to impose a
> > context-free universal label convention on all of set.mm, which is not
> > necessarily a positive thing if it leads to longer labels.

On Fri, 21 Jul 2017 01:22:58 +0100, Mario Carneiro <di....@gmail.com> wrote:
> I have to second this. The label convention system is not 100% consistent,
> and is not unambiguous. But as long as there are reasonably good reasons
> for the inconsistencies that exist, I don't think it is a bad thing.

I'm *fine* with inconsistencies, but they need to:
1. actually have reasonably good reasons,
2. be *documented* (if there's a different rule), and
3. have only a limited number
   (if everything is an exception it's a nightmare).

In particular: if there's a df-NAME that consistently uses a fragment
other than NAME, then I think there is an *obligation* to document that,
and we should strive to limit those situations.

So: if (/) is defined in "df-nul", but is consistently marked as "0" in labels,
that needs to be *documented*.  I personally think that
"z" would be better (so you can use "df-z" and be totally consistent),
but if not, let's agree that it should be *documented*.

Agreed. But this is not so hard and has much less impact.
 

I currently have a "Syntax?" column in the naming table.  I think I
should change that column to "Match df?".  It would then be "yes" if
the conventional fragment matches the text after its "df-...", else no.
That would make exceptions much more obvious, and would mean that
I would no longer have to decide if a structure was "syntax".
Any objections to that?

I think it should be a "comment" instead in the table (like "definition is df-nul"). I want people to associate the label fragment with the definition. The thing after df-NAME is not actually that important, since it is usually rarely used. Contrary to Norm's suggestion, in this case (definitions that don't match their label fragments) I would recommend adding a note to the definition, such as "Note: In theorems, this definition is referred to with the label fragment '0', not 'nul'." These are already not on the naming scheme, so they will need to be visited anyway if we do a wholesale naming change later.

 

If I switch to "Match df?", I think we should strive to (eventually) list in the
table *every* case where a fragment is normally *not* the same as
what's after df-.  That way people can find, in one place, all the
other conventions.

I think this is fine, although again I think a "comment" column for documenting exceptions to the table is a better way to go.
 

Agreed.  I'm not trying to make it possible to uniquely map a

label to a statement; that would require much longer labels.
But it'd be nice to be able to easily guess, from just a statement, what
the label *probably* is, just by knowing the names of the definitions
and without memorizing a long list of exceptions
(CC uses "cn" even though it's defined in df-c, (/) uses "z" even though it's
defined in df-nul, etc.).

I don't like this way of thinking. Don't memorize the list of definition names + exceptions, memorize the label fragments and forget the exceptions. No one cares that df-c is not df-cn, because it's never used. (I had to look it up to confirm.)

 

On Fri, Jul 21, 2017 at 3:52 AM, David A. Wheeler <dwhe...@dwheeler.com> wrote:

On Thu, 20 Jul 2017 23:16:09 +0100, Mario Carneiro <di....@gmail.com> wrote:
> Before I forget: "df-divides" is inconsistent with the label fragment
> "dvds" (it is also used on a few of the definitional theorems).

Good info.  I've added it to the name table so it won't be forgotten.

Actually, I think it should just be renamed. I am thinking: df-divides -> df-dvds, divides[1-3] -> dvdsval[1-3].
 

> Here is the list of all the ones that should NOT be renamed out of that
> list:..

Thanks so much!!
I hand-edited the list to remove the ones you noted.
Whew, next time I'll run a script to do that!

Below is what I think is the final list of changes to change "df-z" to "df-zz"
and change all matching labels to use "zz" for consistency's sake.
It's a surprisingly short list for such a broad change.

ZZ and QQ are the only cases where labels get *longer*, and since
there are relatively few theorems involving QQ, the list below is
practically *all* of the impact. I don't think we significantly
increase the uncompressed file size to create this consistency.
The potential consistency gains are at least:
* All blackboard-font set names are doubled letters (consistently)

By the way, df-aa is also a blackboard bold notation, but it has always been written doubled. df-prime is another exception - it is notated with a blackboard P, but the syntax is "Prime", defined by "cprime" and "df-prime", and the label fragment is usually "prm". I don't know if we should use "pp" instead, "prm" is more mnemonic.

* All blackboard-font label fragments match their definition name
   (no need to explain the exceptions)
* Given a label, it's somewhat easier to guess what it probably refers to
   (by reducing the number of one-letter fragments).  There would
   still be ambiguities, I'm not trying to eliminate that.
   That's not a primary reason, but it's nice to have.

After this, I'd do the others.  For example:
NN: df-n => df-nn, almost nothing else changes.
CC: df-c => df-cc, fragments "cn" become "cc".
RR: df-r => df-rr, fragments "re" become "rr"
QQ: df-q => df-qq, fragments "q" become "qq"

I expect the others to be easier to do (two-character matches are less
likely to mismatch, are there are few that involve QQ).

So for example, "zzcc" would represent ` ( N e. ZZ -> N e. CC ) `
instead of the current name "zcn".

So... thoughts?  Should we proceed in this direction?
I think we should, but I thought it'd be easier to *show* a little of
what the changes would look like so we can reasonably discuss them.

--- David A. Wheeler

============================================

Okay, one more pass:

 

cz czz $a class ZZ $.

Not this one. Brevity is more important than consistency for syntax axioms, and the label fragment in syntax axioms is often an abbreviated version of the label fragment.

 

zmodfz zzmodfzz $p |- ( ( A e. ZZ /\ B e. NN ) ->
zmodfzo zzmodfzzo $p |- ( ( A e. ZZ /\ B e. NN ) -> ( A mod B ) e. ( 0 ..^ B ) ) $=

oops, missed these: zmodfz -> zzmodfz, zmodfzo -> zzmodfzo

 

nthruz nthruzz $p |- ( NN C. NN0 /\ NN0 C. ZZ ) $=

This should be nnthruzz (mentioning now since I doubt you are listing uses of "n" for "NN" since it is rare)

Mario

[David A. Wheeler]

On Fri, 21 Jul 2017 09:40:53 +0100, Mario Carneiro <di....@gmail.com> wrote:
> > ... That would make exceptions much more obvious, and would mean that

> > I would no longer have to decide if a structure was "syntax".
> > Any objections to that?

> I think it should be a "comment" instead in the table (like "definition is
> df-nul"). I want people to associate the label fragment with the
> definition. The thing after df-NAME is not actually that important, since
> it is usually rarely used. Contrary to Norm's suggestion, in this case
> (definitions that don't match their label fragments) I would recommend
> adding a note to the definition, such as "Note: In theorems, this
> definition is referred to with the label fragment '0', not 'nul'." These
> are already not on the naming scheme, so they will need to be visited
> anyway if we do a wholesale naming change later.

I'd be fine with that. Indeed, I think it should be documented
in both places (the table maps fragment=>definition, the definitions
map definition=>fragment).

However, Norm strongly objected to including this information in
individual comments of the definitions. I think the
most important issue is that it be documented *somehow*.
If the exceptions are documented in the "conventions" table,
it's still an improvement over "not written anywhere".

> ... I don't like this way of thinking. Don't memorize the list of definition

> names + exceptions, memorize the label fragments and forget the exceptions.
> No one cares that df-c is not df-cn, because it's never used. (I had to
> look it up to confirm.)

The goal is to make it easy to find the conventional abbreviation for "CC".
If the usual rule is "look up its df-NAME and use NAME", then we only need
to document the exceptions... but we need to document them somewhere.
Ideally there wouldn't be too many exceptions, but that's a different issue.

> Actually, I think it should just be renamed. I am thinking: df-divides ->
> df-dvds, divides[1-3] -> dvdsval[1-3].

Even better. One less exception.

> By the way, df-aa is also a blackboard bold notation, but it has always
> been written doubled.

Interesting; so it's already done in at least one case.

> df-prime is another exception - it is notated with a
> blackboard P, but the syntax is "Prime", defined by "cprime" and
> "df-prime", and the label fragment is usually "prm". I don't know if we
> should use "pp" instead, "prm" is more mnemonic.

We could rename it to "pp", but I don't think we should.
Prime is different than the others. While it's often *presented*
as blackboard P, the ASCII syntax is "Prime" not "PP".
That makes it different in set.mm from NN, ZZ, CC, QQ, AA, and so on.
Since its underlying syntactic term is different,
it makes sense that its label fragment is also different.
And I agree that "prm" is more mnemonic.

I think we should just rename just "df-prime" into "df-prm".
I don't think any other labels/theorems would change, because
I think all the labels use "prm" already.
Just that one change would eliminate yet another inconsistency.

> Okay, one more pass:
>
> > cz czz $a class ZZ $.
> >
>
> Not this one. Brevity is more important than consistency for syntax axioms,
> and the label fragment in syntax axioms is often an abbreviated version of
> the label fragment.

Interesting. That strikes me as odd somehow, but I can't see a real
problem doing that. The tools automatically load the relevant syntax axioms,
so their names aren't as important. Okay, sure.

> > zmodfz zzmodfzz $p |- ( ( A e. ZZ /\ B e. NN ) ->
> > zmodfzo zzmodfzzo $p |- ( ( A e. ZZ /\ B e. NN ) -> ( A mod B ) e. ( 0 ..^
> > B ) ) $=
> >
> oops, missed these: zmodfz -> zzmodfz, zmodfzo -> zzmodfzo

> > nthruz nthruzz $p |- ( NN C. NN0 /\ NN0 C. ZZ ) $=
> >
>
> This should be nnthruzz (mentioning now since I doubt you are listing uses
> of "n" for "NN" since it is rare)

You're right. Normally NN is already represented as nn.

--- David A. Wheeler

[David A. Wheeler]

> On Fri, 21 Jul 2017 09:40:53 +0100, Mario Carneiro <di....@gmail.com> wrote:
> > Actually, I think it should just be renamed. I am thinking: df-divides ->
> > df-dvds, divides[1-3] -> dvdsval[1-3].

I plan to do that this weekend unless someone objects.
Mario & I both agree on it, and I haven't heard a disagreement.

Most of the labels already use "dvds", so changing "df-divides" to "df-dvds"
(along with those stragglers) simply makes the definition consistent
with the rest of set.mm.

> > df-prime is another exception - it is notated with a
> > blackboard P, but the syntax is "Prime", defined by "cprime" and
> > "df-prime", and the label fragment is usually "prm". I don't know if we
> > should use "pp" instead, "prm" is more mnemonic.

Since almost everything uses "prm" for ` Prime ` , let's just rename
"df-prime" to "df-prm". Then the definition will be consistent with most
of its actual uses. You & I both seem to think that's reasonable.

There are a two theorems that use "prime"
when referring to ` Prime `, but those are easy renames
(same format as before: oldname newname firstline):

dvdsprime dvdsprm $p |- ( ( P e. Prime /\ M e. NN ) ->
dfprime2 dfprm2 $p |- Prime = ( NN i^i I ) $=

Again, I intend to do this rename this weekend unless someone speaks up.

These are small changes, and simply rename "df-NAME" to match
the actual fragment in use (which *is* the convention).
I'll add these to the list of renames, of course.

--- David A. Wheeler

[Alexander van der Vekens]

Hi David,
do you want to hear a fourth opinion?

I strongly agree with using (almost) always the same label fragment for the same mathematical concept in the labels for theorems, but exceptions should be possible if there are good and, again only if necessary, documented reasons for such exceptions.
So I would vote for renaming "dvdsprime" in "dvdsprm".

However, I do not like that such great and important mathematical concepts like "Primes" and "divides" are mutilated even in a label. In my opinion, df-prime and df-divides should not be changed.

I also do not in general agree with the rule to always use the fragment of the definition label as fragment in the labels for theorems. A definition is really something special, and its label should reflect the meaning of the definiendum, more than a label fragment in a theorem must reflect the usage of a concept. From my point of view, it is also useful to "see" if a prove uses a definition and not only theorems, so with a more prominent name the usage of a definition becomes more visible, for example:

dvdsrz $p |- || = ( ||r ` Z ) $=
      ( vx vy vz cv cz wcel wa cmul co wceq copab cfv simpl cc ccnfld ax-mp cvv
      wrex cdivides anim1i zmulcl ancoms eleq1 syl5ibcom rexlimdva simpr impbii
      cdsr imp jca31 opabbii df-divides wss cbs cnfldbas ressbas2 eqid cnfldmul
      zsscn cmulr zex ressmulr dvdsrval 3eqtr4i ) ...

Finally, definition labels are rarely used, mainly in basic theorems (as for df-prime), so they can be longer than labels for theorems.

By these arguments I would prefer, in contrast to the conventions discussed in this thread, even longer definition labels in many other cases. Examples:

df-f => df-funmap
df-fv => df-funval
df-ov => df-opval

With this opinion, I support at least the avoidance of one letter fragments ;-).
However, also for this approach there cannot be strict rules (I also do not want to rename df-f in df-functionmapping or df-fv in df-functionvalue which would really be too long). The corresponding label fragments for theorems would still be "f" (not "fm", since this is already used for "FilMap"...), "fv", "ov"...

To comment the argumentation that consistent label fragments for definitions and theorems can improve the understandability:

1. It is a common way to abbreviate words by removing the vowels, so that "prime" becomes "prm" as label fragment in theorems should be obvious.
2. It is not necessary to document the deviation of the convention explicitely ("In labels for theorems using ... the fragment ... will be used.") in the comment
of a definition, but to provide references to important/useful theorems using this definition, e.g.:

    $( Definition of a monoid.  A monoid is a set equipped with an everywhere
       defined internal operation (so, a magma, see ~ mndcl ), whose operation
       is associative (so, a semigroup, see ~ mndass ) and has a two-sided
       neutral element (see ~ mndid ).  (Contributed by Mario Carneiro,
       6-Jan-2015.) $)
    df-mnd $a |- Mnd = { g | [. ( Base ` g ) / b ]. [. ( +g ` g ) / p ].

(In this example I wouldn't have any objection to use the label df-monoid...).

This should be done anyway to provide evidence for the existence of this definition.

Since, as always in discussions about naming conventions, there is no absolute truth, and its important to get an agreement quickly before wasting to much time.
Therefore I would propose a quick voting with a deadline this evening 6 pm:

If you three (involved in this discussion so far) vote for David's proposal, I will not disagree, and the changes can be made. However, if there are comments from other people with other opinions until then, the new score must be considered...

Best regards,
Alexander

[Alexander van der Vekens]

 ... I forgot to comment on "dfprime2 vs. dfprm2": such an alternative definition is something special, something between definition and theorem. So special conventions should hold (hold already?) for the labels for alternative definitions: removal of the hyphen and adding a number. So if df-prime is not changed, dfprime2 should not be changed either.

Alexander

[David A. Wheeler]

On July 22, 2017 4:01:46 AM EDT, 'Alexander van der Vekens' via Metamath <meta...@googlegroups.com> wrote:
>I also do not in general agree with the rule to always use the fragment of
>the definition label as fragment in the labels for theorems. A
>definition
>is really something special, and its label should reflect the meaning of
>the definiendum, more than a label fragment in a theorem must reflect
>the usage of a concept.

I don't agree.

If the label fragment is different than what happens after df-..., then there needs to be some other way to easily and consistently find out what the label fragment is. A few exceptions are fine, but if everything is an exception then the whole system is excessively hard to use.

>1. It is a common way to abbreviate words by removing the vowels, so
>that
>"prime" becomes "prm" as label fragment in theorems should be obvious.

No. "and" would then become "nd", for example. The whole point of a naming convention is to let people think of something else other than naming.

>2. It is not necessary to document the deviation of the convention
>explicitely ("In labels for theorems using ... the fragment ... will be
>used.") in the comment
>of a definition, but to provide references to important/useful theorems
>using this definition

I think that is inadequate. That requires too much analysis to figure out what should be trivial. Formal mathematics is challenging enough without requiring everyone to figure out a name guessing game.

In addition, this is not a change to the approach in set.mm. Almost all of set.mm already follows this convention. The challenge, from my viewpoint, is that there were just enough exceptions that the convention was not obvious. By eliminating some of the exceptions, and documenting the others, the naming convention is much easier to understand.



--- David A.Wheeler

[David A. Wheeler]

>I also do not in general agree with the rule to always use the fragment of
>the definition label as fragment in the labels for theorems.

But this is normally what is done. Let me illustrate with a few examples. Groups are defined in df-grp (not df-group), "and" is defined in df-an (not df-and). I just switched rings from df-ring to df-rng, because that was one of the few stragglers.

These consistent shortenings make things easier to deal with. It doesn't interfere with finding the full name, those are already in the comments of the definitions.


--- David A.Wheeler

[Mario Carneiro]

On Sat, Jul 22, 2017 at 9:01 AM, 'Alexander van der Vekens' via Metamath <meta...@googlegroups.com> wrote:

Hi David,
do you want to hear a fourth opinion?

I strongly agree with using (almost) always the same label fragment for the same mathematical concept in the labels for theorems, but exceptions should be possible if there are good and, again only if necessary, documented reasons for such exceptions.
So I would vote for renaming "dvdsprime" in "dvdsprm".

However, I do not like that such great and important mathematical concepts like "Primes" and "divides" are mutilated even in a label. In my opinion, df-prime and df-divides should not be changed.

I also do not in general agree with the rule to always use the fragment of the definition label as fragment in the labels for theorems. A definition is really something special, and its label should reflect the meaning of the definiendum, more than a label fragment in a theorem must reflect the usage of a concept. From my point of view, it is also useful to "see" if a prove uses a definition and not only theorems, so with a more prominent name the usage of a definition becomes more visible, for example:

dvdsrz $p |- || = ( ||r ` Z ) $=
      ( vx vy vz cv cz wcel wa cmul co wceq copab cfv simpl cc ccnfld ax-mp cvv
      wrex cdivides anim1i zmulcl ancoms eleq1 syl5ibcom rexlimdva simpr impbii
      cdsr imp jca31 opabbii df-divides wss cbs cnfldbas ressbas2 eqid cnfldmul
      zsscn cmulr zex ressmulr dvdsrval 3eqtr4i ) ...

This heuristic is flawed. Only very few theorems actually use the definition directly. As a matter of fact, I do the same thing (glance at the label list in a compressed proof to get a hint of what concepts are involved), but I key off the *label fragments*, which are much more reliably associated to a definition than the df-NAME statement itself. So, for example, I can look at that label list and see "cnfld" and "ress" in the statements to get a clue that structure restriction of the complex numbers is involved in the proof.

 

Finally, definition labels are rarely used, mainly in basic theorems (as for df-prime), so they can be longer than labels for theorems.

By these arguments I would prefer, in contrast to the conventions discussed in this thread, even longer definition labels in many other cases. Examples:

df-f => df-funmap
df-fv => df-funval
df-ov => df-opval

...

Since, as always in discussions about naming conventions, there is no absolute truth, and its important to get an agreement quickly before wasting to much time.
Therefore I would propose a quick voting with a deadline this evening 6 pm:

You should be careful about times on an international message board. I don't even know what timezone you are in, so I don't know when 6pm is.

But if you want a vote, I'll vote against, for much the same reasons as David. The label fragment "funmap" never occurs - or worse, it occurs in unrelated contexts (in this case, df-fun + df-map, which isn't what you want). So this is just promoting a useless association of names for readers. As David says, the full names of the concepts involved can be elaborated in comments, where we are not nearly as pressed for space and can explain things properly.

Mario

[Alexander van der Vekens]

Since, as always in discussions about naming conventions, there is no absolute truth, and its important to get an agreement quickly before wasting to much time.
Therefore I would propose a quick voting with a deadline this evening 6 pm:

You should be careful about times on an international message board. I don't even know what timezone you are in, so I don't know when 6pm is.

But if you want a vote, I'll vote against, for much the same reasons as David. The label fragment "funmap" never occurs - or worse, it occurs in unrelated contexts (in this case, df-fun + df-map, which isn't what you want). So this is just promoting a useless association of names for readers. As David says, the full names of the concepts involved can be elaborated in comments, where we are not nearly as pressed for space and can explain things properly.

 
Hi Mario,
I did'n want to propose a voting about my proposals (these were only examples), but about David's proposals concerning df-prime and df-divides. And I intentionally did not specify a time zone to let David decide when for him the voting ends, so that he can start its changes.

And I do not want to stop any improvements on set.mm, just give my opinion on this topic. I think the main argument for performing David's changes is the (until now unspoken) convention/rule to use the label fragments to be used for theorems already for definitions. Therefore I withdraw my objection, and fully support David's proposal.

Alexander

[David A. Wheeler]

On Fri, 21 Jul 2017 09:40:53 +0100, Mario Carneiro <di....@gmail.com> wrote:
> Actually, I think it should just be renamed. I am thinking: df-divides ->
> df-dvds, divides[1-3] -> dvdsval[1-3].

Okay. Below in ",rename1" is the set of renames I plan to run to turn
"df-divides" into "df-dvds", as well as turn "df-prime" into "df-prm".
Since most theorem labels already follow these conventions, there aren't
many renames.

After that is a script I wrote that does all the renames and then
verifies that the result passes. This set already passes without problems.
I intend to run this soon, and post the results to "develop".

--- David A. Wheeler



=== ,rename1 ===
df-divides df-dvds $a |- || = { <. x , y >. | ( ( x e. ZZ /\ y e. ZZ ) /\
divides dvdsval1 $p |- ( ( M e. ZZ /\ N e. ZZ ) ->
divides2 dvdsval2 $p |- ( ( M e. ZZ /\ M =/= 0 /\ N e. ZZ ) ->
divides3 dvdsval3 $p |- ( ( M e. NN /\ N e. ZZ ) ->
nndivdivides nndivdvds $p |- ( ( A e. NN /\ B e. NN ) ->
df-prime df-prm $a |- Prime = { p e. NN | { n e. NN | n || p } ~~ 2o } $.


=== mass-rename ===
#!/bin/sh

# Requires $1: name of file listing what to change
# The file is formatted as lines of:
# old-name new-name other-info

# This changes *all* cases of old-name after the list of "past renames";
# beware if "old-name" is an ordinary English word.

if [ "$#" -ne 0 ] ; then
echo 'Requires 0 arguments (stdin must be the list of renames)' >&2
exit 1
fi

mmfile='set.mm'

# Skip the list of "past renames" so we don't accidentally
# change any historical info.
range='/^ *[a-zA-Z0-9._-]+ \$[apef] /,$'

while read old new rest
do
echo "$old $new"
sed -E -e "${range}s/ $old( |$)/ $new /g" -e 's/ $//' < "$mmfile" \
> "$mmfile.tmp"
mv "$mmfile.tmp" "$mmfile"
done

echo
metamath "read $mmfile" 'verify proof *' 'verify markup *' quit

[Norman Megill]

Don't forget to check the 7 mm*.html files in the set.mm github directory.  For example, df-plus is referenced in mmset.html.  I suppose it is possible to automate, but since this isn't a frequent activity, I just grep for all of the old names and check the result by hand to see which ones are real matches that need to be changed.

Also, I trust you are keeping the the label change list at the top of set.mm updated.

Norm

On Saturday, July 22, 2017 at 3:52:24 PM UTC-4, David A. Wheeler wrote:

[David A. Wheeler]

On Sat, 22 Jul 2017 13:48:02 -0700 (PDT), Norman Megill <n...@alum.mit.edu> wrote:
> Don't forget to check the 7 mm*.html files in the set.mm github directory.
> For example, df-plus is referenced in mmset.html.

Too late, I *did* forget them :-). Working it now.

> I suppose it is possible
> to automate, but since this isn't a frequent activity, I just grep for all
> of the old names and check the result by hand to see which ones are real
> matches that need to be changed.

The change for set.mm is already automated, per the script I posted.
I'll tweak the script.

> Also, I trust you are keeping the the label change list at the top of
> set.mm updated.

Yes, absolutely! The script doesn't add them, but it prints the change list
so I can easily do it in one step.

--- David A. Wheeler

[David A. Wheeler]

In case anyone else wants to use it...

Below is my updated "mass-rename" program,
it should work on any POSIX system (including Windows with Cygwin).
You can give it a list of renames, and off it goes.
It even tries to do renames in the mm*.html files.

Should we put scripts like this into the git repository, say in
a "scripts/" subdirectory? Automation can be a good thing.
They wouldn't take much space, and when you need them
they can be very useful.

--- David A. Wheeler


====================================
#!/bin/sh

# Mass rename of set.mm file. Standard input has form:
# old-name new-name other-info

# Beware if "old-name" is an ordinary English word!

if [ "$#" -ne 0 ] ; then
echo 'Requires 0 arguments (stdin must be the list of renames)' >&2
exit 1
fi

mmfile='set.mm'

# Skip the list of "past renames" so we don't accidentally
# change any historical info.
range='/^ *[a-zA-Z0-9._-]+ \$[apef] /,$'

while read old new rest
do
echo "$old $new"
sed -E -e "${range}s/ $old( |$)/ $new /g" -e 's/ $//' < "$mmfile" \
> "$mmfile.tmp"
mv "$mmfile.tmp" "$mmfile"

for f in $(git ls-files | grep '^mm.*\.html')
do
sed -E -e "s/ $old( |$)/ $new /g" -e 's/ $//' \
-e "s/<A HREF=\"${old}.html\">${old}<\/A>/<A HREF=\"${new}.html\">${new}<\/A>/ig" \
< "$f" > "$f.tmp"
mv "$f.tmp" "$f"
done

[Norman Megill]

In the match to "<A HREF", sometimes there is a newline instead of a space after the A.  That can happen if I wrapped the HTML in a text editor.

Also, the 2+2=4 path is of the form e.g.
<A HREF="con2d.html" TITLE="A contraposition deduction.">con2d</A>

I can't think of any other cases right now.

Norm

[Mario Carneiro]

On Sat, Jul 22, 2017 at 10:41 PM, David A. Wheeler <dwhe...@dwheeler.com> wrote:

In case anyone else wants to use it...

Below is my updated "mass-rename" program,
it should work on any POSIX system (including Windows with Cygwin).
You can give it a list of renames, and off it goes.
It even tries to do renames in the mm*.html files.

Should we put scripts like this into the git repository, say in
a "scripts/" subdirectory?  Automation can be a good thing.
They wouldn't take much space, and when you need them
they can be very useful.

--- David A. Wheeler


====================================
#!/bin/sh

# Mass rename of set.mm file.  Standard input has form:
# old-name new-name other-info

# Beware if "old-name" is an ordinary English word!

if [ "$#" -ne 0 ] ; then
  echo 'Requires 0 arguments (stdin must be the list of renames)' >&2
  exit 1
fi

mmfile='set.mm'

# Skip the list of "past renames" so we don't accidentally
# change any historical info.
range='/^ *[a-zA-Z0-9._-]+ \$[apef] /,$'

If I'm reading this right, you are only replacing labels before $p etc. You also have to replace names in label lists in proofs, or else everything will break.

[David A. Wheeler]

My script:

>> # Skip the list of "past renames" so we don't accidentally
>> # change any historical info.
>> range='/^ *[a-zA-Z0-9._-]+ \$[apef] /,$'

Mario:

>If I'm reading this right, you are only replacing labels before $p etc.
>You also have to replace names in label lists in proofs, or else everything
>will break.

No, you are not reading it right. What the range statement does is require that substitutions only begin after the first legitimate dollar statement. Without this range value, the global substitution would not only change the normal contents, but it would also change the historical information about past renames. We don't want to do that.


--- David A.Wheeler

[David A. Wheeler]

I have not made these renames:

dvdsprime dvdsprm $p |- ( ( P e. Prime /\ M e. NN ) ->
dfprime2 dfprm2 $p |- Prime = ( NN i^i I ) $=

When I tried to do this set, verification immediately failed
because of the first line.
It turns out that there is an existing "dvdsprm", so I obviously
can't rename "dvdsprime" into "dvdsprm". For the moment
I've left them as-is.

Any suggestions on better names for dvdsprime and dvdsprm?

--- David A. Wheeler

==================================

${
$d M m $. $d P m $.
$( If ` M ` divides a prime, then ` M ` is either the prime or one.
(Contributed by Scott Fenton, 8-Apr-2014.) $)
dvdsprime $p |- ( ( P e. Prime /\ M e. NN ) ->
( M || P <-> ( M = P \/ M = 1 ) ) ) $=
( vm cprime wcel cn wa cdivides wbr wceq c1 wo c2 cuz wi breq1 syl adantr
eqeq1 syl5ibrcom cfv cv wral isprm2 orbi12d orcom syl6bb imbi12d rcla4cva
adantll sylanb cz prmz iddvds 1dvds jaod impbid ) ADEZBFEZGZBAHIZBAJZBKJZ
LZURAMNUAEZCUBZAHIZVFKJZVFAJZLZOZCFUCZGUSVAVDOZCAUDVLUSVMVEVKVMCBFVFBJZVG
VAVJVDVFBAHPVNVJVCVBLVDVNVHVCVIVBVFBKSVFBASUEVCVBUFUGUHUIUJUKUTVBVAVCUTVA
VBAAHIZURVOUSURAULEZVOAUMZAUNQRBAAHPTUTVAVCKAHIZURVRUSURVPVRVQAUOQRBKAHPT
UPUQ $.
$}

${
$d N z $. $d P z $.
$( An integer greater than or equal to 2 divides a prime number iff it is
equal to it. (Contributed by Paul Chapman, 26-Oct-2012.) $)
dvdsprm $p |- ( ( N e. ( ZZ>= ` 2 ) /\ P e. Prime ) ->
( N || P <-> N = P ) ) $=
( vz c2 cuz cfv wcel cprime wa cdivides wbr wceq wi cv wral simprbi breq1
isprm4 eqeq1 imbi12d rcla4v mpan9 ancoms cz iddvds breq2 syl5ibcom adantr
eluzelz syl impbid ) BDEFZGZAHGZIBAJKZBALZUNUMUOUPMZUNCNZAJKZURALZMZCULOZ
UMUQUNAULGVBCARPVAUQCBULURBLUSUOUTUPURBAJQURBASTUAUBUCUMUPUOMZUNUMBUDGZVC
DBUIVDBBJKUPUOBUEBABJUFUGUJUHUK $.
$}

[Norman Megill]

Your script is fine, but if anyone is interested, here is how I do this.

The 'tools' command in metamath.exe was actually a program I wrote a long time ago for non-technical employees to do simple file manipulations, after seeing them struggle with regex, special character escapes, and so on.

Below I commented the script I use, called rename.cmd, which is run inside of metamath.exe with 'submit rename.cmd' at the MM> prompt.  It isn't as sophisticated as yours since does not attempt to update the mm*.html files (as I mentioned, I manually inspect a grep output for possible changes to be done by hand).  It should produce a set.mm identical to yours if you want to double-check your script.  Note that the 'renames' file must have only two fields per line, since that's the way I use it, but it's easy to modify for you 3 fields if we want.

Norm


!--- start of rename.cmd ---!
tools
! This script applies a set of label renames, from a file called "renames", to set.mm.
!
! It does not prepend the label change list in set.mm.  That should be
! done by hand.
!
! The file "renames" format s.b. "<old-label> <new-label>" (2 fields per line)
!
! Make temporary copies
copy set.mm s.tmp
copy renames r.tmp
!
! Part 1: split off the list of historical label changes at the top of set.mm
!
! Tag historical set.mm label change list with string "@@@@" (that doesn't
! occur in set.mm), from start of set.mm file to the first line
! containing "How to use"
tag s.tmp "@@@@" "" "" 1 "How to use" 1
! Split set.mm into t.tmp (historical label change list) and s.tmp (main body)
copy s.tmp t.tmp
match t.tmp "@@@@" y
substitute t.tmp "@@@@" "" "" ""
match s.tmp "@@@@" n
!
! Part 2: do the renaming
!
! Clean up any beginning, multiple, ending spaces in 'renames' file
clean r.tmp ber
! Put a space after each set.mm line, so we can match "<space><label><space>"
add s.tmp "" " "
! Note that r.tmp lines should be of the form "old new"
! Turn them into "old ' ' new"
substitute r.tmp " " " ' ' " all ""
! Turn them into "subsitute s.tmp ' old ' ' new ' all ''"
add r.tmp "substitute s.tmp ' " " ' all ''"
! Run the rename commands as a script
submit r.tmp
!
! Cleanup
!
! Remove space after each set.mm line
clean s.tmp e
! Concatenate historical label change list t.tmp with body s.tmp
copy t.tmp,s.tmp set.mm
exit
!--- end of rename.cmd ---!

[David A. Wheeler]

On Thu, 20 Jul 2017 22:52:28 -0400 (EDT), "David A. Wheeler" <dwhe...@dwheeler.com> wrote:

This primarily a question for Norm, but other comments are welcome too.

Basically: Should we rename the definitions and labels for ZZ, NN, CC, RR, and QQ?

I've already posted a list of label renames to support renaming
"df-z" to "df-zz"; Mario has adjusted that list.
I think it's doable.
I propose that we apply that set of changes, and then follow with:

> NN: df-n => df-nn, almost nothing else changes.
> CC: df-c => df-cc, fragments "cn" become "cc".
> RR: df-r => df-rr, fragments "re" become "rr"
> QQ: df-q => df-qq, fragments "q" become "qq"

AA is already this way.

This change would eliminate a major inconsistency between labels and df-NAMEs.
In the case of ZZ and QQ, it would also make overlaps with other
label fragments less likely.

However, it's obviously a nontrivial change, and it renames
a number of often-used labels. I've created a few scripts to
help automate the change. However, I don't want to do work
that won't be used. If we do *not* do these renamings, then
at the very least the inconsistency should be documented.

So... should this happen?

--- David A. Wheeler

[Stefan O'Rear]

I would prefer no renamings. They bloat the repository, cause
unproductive bikeshed discussions, and discourage contribution (if I
start working on something, I want my personal branch to stay
mergable). No compelling reason has been presented (making it easier
to memorize the names of df-* statements is not a reason to rename
anything else).

-s

[Dan Connolly]

What happens to incoming web links when theorems are renamed?

--
Dan Connolly
http://www.madmode.com

On Jul 20, 2017 10:18 AM, "David A. Wheeler" <dwhe...@dwheeler.com> wrote:

On Wed, 19 Jul 2017 16:48:03 -0700 (PDT), Norman Megill <n...@alum.mit.edu> wrote:
> There is an informal sub-convention that "n0" means =/= (/) and "ne0" means
> =/= 0.

There's nothing wrong with sub-conventions, we should just document them.

[Norman Megill]

If there is a great demand for this, I could go along with it.  Otherwise I think we shouldn't make this change or should at least postpone it.  Here are some considerations.

1. cn, re, nn stand for "complex number", "real number", "natural number".  Although logically real number should have been "rn", it conflicted with "rn" for range, which at the time I felt was too great a conflict.  As for z and q, we don't say "zahlen number" or "quotient number" but just "z" and "q", and that's why they have only one letter.

2. Having repeated letters cc and rr could create ambiguity where none existed before.  Does "ccc" mean "cnc" or "ccn"?  Does "rrr" mean "rre" or "rer"?  Maybe this is a strawman - there don't see to be many such cases at present - but in any case cc and rr don't decrease potential ambiguity..

3. Most theorems about z and q almost always have the letter in front:  zaddcl, qnegcl.  So even though these letters are commonly used (such as in all theorems with "eq"), labels starting with q or z  that aren't about rationals or integers are not very common.

4. Adding another letter to z and q makes those names longer.  I know that's a relatively small complaint, but it is a checkpoint on the negative side.

5. As Dan pointed out, renames could break links to us from an external site.  So that is an argument in favor of not changing a name without a good reason.  (There is a page http://us.metamath.org/missing.html that 404's used to redirect to - I just checked, it's still there! - with a list of page name changes.  I looked for 404's in the web logs to determine what obsolete pages sites were linking to and added them to this page.  It became too much of a pain to maintain, and I stopped doing so in 2004.)

6. AFAIK only you are requesting this change, motivated in part by wanting to make your conventions table more uniform.  While better uniformity is a valid point in favor, I would like to see more people on board with it before going ahead.  There is no urgency, and I have no problem postponing it until there is more interest.

Norm

On Saturday, July 22, 2017 at 10:58:32 PM UTC-4, David A. Wheeler wrote:

[David A. Wheeler]

On Sat, 22 Jul 2017 22:01:07 -0700 (PDT), Norman Megill <n...@alum.mit.edu> wrote:
> If there is a great demand for this, I could go along with it. Otherwise I

> think we shouldn't make this change or should at least postpone it...

Okay. In that case, here's what I plan to do:
1. *Document* in "conventions" these exceptions. E.g., that
cn stands for "complex number" and "re" stands for "real number".
2. I'll define "reserved placeholders" in my mathbox for "df-cc", "df-rr", etc.
That way people won't accidentally use them. That will make it easier
to make this change later if we choose to. I'll mark them as
"(New usage is discouraged.)", of course.

I have some requests:
1. Can we at least rename "df-n" to "df-nn"? The placeholder is already "nn",
there's no "df-nn", and the placeholder "n" is already often used for "not".
We already have other number definitions with multiple letters, such as
df-xr (for RR*) and df-rp (for RR+).
2. Can we please include, the *definition comments*, when the label fragment
of df-NAME is not NAME (in addition to the "conventions" table)?
Both Mario & I think this would be appropriate.

> 5. As Dan pointed out, renames could break links to us from an external site.

I use a script to generate the renames. That script could easily be modified
to create redirection links or redirection pages.

> 6. AFAIK only you are requesting this change, motivated in part by
> wanting to make your conventions table more uniform

It's not that I want the *table* to be more uniform; it's that I want to
maximize making the *naming convention* uniform. I think exceptions
must be documented, and it's better to minimize the exceptions.

I also want to minimize the number of different possible interpretations of
a label, so that when you see a label, you're more likely to correctly guess
its meaning. Minimizing the number of single-letter label fragments helps
minimize the number of possible interpretations.

So let's document things as they are, and I hope I can talk you into the
two requests above :-).

--- David A. Wheeler

[Norman Megill]

On Sunday, July 23, 2017 at 3:10:10 PM UTC-4, David A. Wheeler wrote:

On Sat, 22 Jul 2017 22:01:07 -0700 (PDT), Norman Megill wrote:
> If there is a great demand for this, I could go along with it.  Otherwise I
> think we shouldn't make this change or should at least postpone it...

Okay.  In that case, here's what I plan to do:
1. *Document* in "conventions" these exceptions. E.g., that
    cn stands for "complex number" and "re" stands for "real number".
2. I'll define "reserved placeholders" in my mathbox for "df-cc", "df-rr", etc.
    That way people won't accidentally use them.  That will make it easier
    to make this change later if we choose to.  I'll mark them as
    "(New usage is discouraged.)", of course.

How are you going to reserve them?  Dummy theorems starting with df-?  That would be confusing, and I doubt it's worth the trouble.  If someone steals df-rr for something else, we can always change it when the day comes to use it for reals.
 

I have some requests:
1. Can we at least rename "df-n" to "df-nn"?  The placeholder is already "nn",
    there's no "df-nn", and the placeholder "n" is already often used for "not".
    We already have other number definitions with multiple letters, such as
    df-xr (for RR*) and df-rp (for RR+).

Sure, I have no problem with that.  Go ahead.
 

2. Can we please include, the *definition comments*, when the label fragment
    of df-NAME is not NAME (in addition to the "conventions" table)?
    Both Mario & I think this would be appropriate.

I don't want to put label fragments that won't automatically update when we run your or my script to change labels.  It is one more thing to maintain.

Outside of a very rare case like df-nul, I see no reason to ever use df-NAME where NAME is not the abbreviation used elsewhere.

In a case where df-NAME would conflict by doing that, rename the thing it conflicts with. If _that_ is a problem, then show the convention by example, such as giving a couple of examples that use the definition as part of the normal comment text e.g. ~ abcval and ~ elabc (will be renamed automatically with a script and checked automatically with 'verify markup') rather than *abc* (needs to be maintained by hand).  The reader should get the hint from the examples.  I see no need to be overly pedantic about it.  The only reason we never changed df-plus to df-add in a couple of decades is that no one ever complained that it was confusing or even brought it up at all.
 

> 5. As Dan pointed out, renames could break links to us from an external site.

I use a script to generate the renames.  That script could easily be modified
to create redirection links or redirection pages.

I have no control over .htaccess or other server directive on the mirrors.  So we'd have to have a dummy redirect page for every rename, of which there have been around 10,000 so far.  And we'd need logic to make sure that an old name to be redirected isn't currently used for another purpose.

I brought this up to indicate a small potential problem, but it is very small and I don't think it is worth worrying about.  Over the past 15 years Metamath has been more stable than probably 95% of the sites out there.  People can use archive.org for the occasional broken link.

Practically all external links I know of are to the home page or MPE home page, along with 2p2e4, equid, and a handful of prop calc theorems like peirce and id1.  Maybe someone with google/bing expertise could collect them?

Norm

[David A. Wheeler]

> On Sunday, July 23, 2017 at 3:10:10 PM UTC-4, David A. Wheeler wrote:
> > 2. I'll define "reserved placeholders" in my mathbox for "df-cc", "df-rr",
> > etc.
> > That way people won't accidentally use them. That will make it easier
> > to make this change later if we choose to. I'll mark them as
> > "(New usage is discouraged.)", of course.

On Sun, 23 Jul 2017 13:57:10 -0700 (PDT), Norman Megill <n...@alum.mit.edu> wrote:
> How are you going to reserve them? Dummy theorems starting with df-? That

> would be confusing...

Yes, and I don't think it'll be confusing at all.
The comments would clearly indicate that they
are merely reserving a name, and since they'd be marked with
"(New usage is discouraged.)" the tools will generally skip it.
If it's not clear, fix the comment until it's clear.

> and I doubt it's worth the trouble.
> If someone steals
> df-rr for something else, we can always change it when the day comes to use
> it for reals.

I think that error-checking should be automated *unless* it's too difficult/expensive
to automate it. Especially for larger datasets like set.mm.

Humans are bad at being perfect. Indeed, a
reason for math formalization is to use computers to check that
claims are correct. In this case, there's a claim that a name is reserved -
we should automate detection of using a reserved name.
It's odd that we're using tools to check consistency, yet not using the
tools to check what we (easily) can.

> > I have some requests:
> > 1. Can we at least rename "df-n" to "df-nn"? ...

> Sure, I have no problem with that. Go ahead.

Great!

> > 2. Can we please include, the *definition comments*, when the label
> > fragment
> > of df-NAME is not NAME (in addition to the "conventions" table)?
> > Both Mario & I think this would be appropriate.
> >
>
> I don't want to put label fragments that won't automatically update when we
> run your or my script to change labels. It is one more thing to maintain.
> Outside of a very rare case like df-nul, I see no reason to ever use
> df-NAME where NAME is not the abbreviation used elsewhere.

I think we're talking past each other.
I recommend that we do *NOT* put any comments on a definition df-NAME
if the label fragment is NAME.

However, if the label fragment is not NAME, *then* we should document it.
Yes, it's one more thing to maintain on a name change, but it should overall
*reduce* the number of changes necessary because people will more easily
learn about the exceptions. There should be very few, e.g.,
df-c (cn), df-r (re), and df-nul (0). So I'm just suggesting adding
comments to perhaps 10 definitions, where they do NOT follow the conventions.

> In a case where df-NAME would conflict by doing that, rename the thing it
> conflicts with. If _that_ is a problem, then show the convention by
> example, such as giving a couple of examples that use the definition as
> part of the normal comment text e.g. ~ abcval and ~ elabc (will be renamed
> automatically with a script and checked automatically with 'verify markup')
> rather than *abc* (needs to be maintained by hand). The reader should get
> the hint from the examples. I see no need to be overly pedantic about it.
> The only reason we never changed df-plus to df-add in a couple of decades
> is that no one ever complained that it was confusing or even brought it up
> at all.

It's not about pedantry, it's about clarity, especially for new readers/users.

In my experience many users do not "get hints".
I've been using metamath for years and only in the last month finally
(mostly) understood the naming scheme. You & Mario have been doing
metamath for a long time, and to both of you a lot of these conventions
are "obvious", but they're not obvious to everyone else.
The fix is straightforward - document things.

--- David A. Wheeler

P.S. Here's a draft to reserve the names:

$(
=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
+ Reserved definition names
+=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
+
+ In the future we may want to rename the definition of the
+ complex numbers into df-cc, reals to df-rr, etc., and rename
+ the corresponding labels to match. This would provide naming consistency,
+ however, it'd be a big name change.
+
+ Reserve those definition names so that they aren't accidentally used,
+ so that we'll retain the ability to more easily make that change.
+$)
+
+ $( Reserve df-cc. (Contributed by David A. Wheeler, 23-Feb-2017.)
+ (New usage is discouraged.) $)
+ df-cc $a |- CC = ( R. X. R. ) $.
+
+ $( Reserve df-qq. (Contributed by David A. Wheeler, 23-Feb-2017.)
+ (New usage is discouraged.) $)
+ df-qq $a |- QQ = ( / " ( ZZ X. NN ) ) $.
+
+ $( Reserve df-zz. (Contributed by David A. Wheeler, 23-Feb-2017.)
+ (New usage is discouraged.) $)
+ df-zz $a |- ZZ = { n e. RR | ( n = 0 \/ n e. NN \/ -u n e. NN ) } $.
+
+ $( Reserve df-rr. (Contributed by David A. Wheeler, 23-Feb-2017.)
+ (New usage is discouraged.) $)
+ df-rr $a |- RR = ( R. X. { 0R } ) $.
+

[Mario Carneiro]

On Sun, Jul 23, 2017 at 11:40 PM, David A. Wheeler <dwhe...@dwheeler.com> wrote:

> On Sunday, July 23, 2017 at 3:10:10 PM UTC-4, David A. Wheeler wrote:
> > 2. I'll define "reserved placeholders" in my mathbox for "df-cc", "df-rr",
> > etc.
> >     That way people won't accidentally use them.  That will make it easier
> >     to make this change later if we choose to.  I'll mark them as
> >     "(New usage is discouraged.)", of course.

On Sun, 23 Jul 2017 13:57:10 -0700 (PDT), Norman Megill <n...@alum.mit.edu> wrote:
> How are you going to reserve them?  Dummy theorems starting with df-?  That
> would be confusing...

Yes, and I don't think it'll be confusing at all.
The comments would clearly indicate that they
are merely reserving a name, and since they'd be marked with
"(New usage is discouraged.)" the tools will generally skip it.
If it's not clear, fix the comment until it's clear.

I concur with Norm. This is not the usual approach to reserved names - usually we just maintain the reservation manually (because it doesn't matter if it is violated), and if/when we get around to using the name properly, any squatters are kicked out. I don't like the idea of additional definitions/axioms with no semantic purpose.

Mario

[Norman Megill]

On Sunday, July 23, 2017 at 6:40:54 PM UTC-4, David A. Wheeler wrote:

...

However, if the label fragment is not NAME, *then* we should document it.
Yes, it's one more thing to maintain on a name change, but it should overall
*reduce* the number of changes necessary because people will more easily
learn about the exceptions.  There should be very few, e.g.,
df-c (cn), df-r (re), and df-nul (0).  So I'm just suggesting adding
comments to perhaps 10 definitions, where they do NOT follow the conventions.

It doesn't matter if it was even 1 definition. It sets a precedent, creating one more thing maintainers have remember to check whenever labels are changed, presumably into perpetuity.

Instead, how about just linking to the conventions for these 10 definitions?
...

 +  $( Reserve df-cc.  (Contributed by David A. Wheeler, 23-Feb-2017.) 

+     (New usage is discouraged.) $)
+  df-cc $a |- CC = ( R. X. R. ) $.

This will fail the mmj2 definition check since it attempts to define CC twice..
 
Norm

[David A. Wheeler]

On Sun, 23 Jul 2017 17:33:51 -0700 (PDT), Norman Megill <n...@alum.mit.edu> wrote:
> It doesn't matter if it was even 1 definition. It sets a precedent,
> creating one more thing maintainers have remember to check whenever labels
> are changed, presumably into perpetuity.
> Instead, how about just linking to the conventions for these 10 definitions?

Okay. That at least gives a hint to people who are creating their
first metamath proofs that there's somewhere they should look
(without committing to a particular value, or even that it's an exception).
I'd add that text where there are currently naming exceptions,
such as df-c, df-r, and df-nul.

How about this as text?:

> For more about label naming conventions, see ~ conventions .

Mario:

> This is not the usual approach to reserved names -
> usually we just maintain the reservation manually (because it doesn't
> matter if it is violated), and if/when we get around to using the name
> properly, any squatters are kicked out. I don't like the idea of additional
> definitions/axioms with no semantic purpose.

Okay. If we're going to continue to track them manually, then
I propose adding this to section "1. Recent label changes"
in the PROPOSED list:

Date Old New Notes
proposed df-c df-cc
proposed df-q df-q
proposed df-z df-zz
proposed df-q df-qq

--- David A. Wheeler