IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

Counting Indirectly - integer ranges.

Counting the number of members of a class A is often accomplished indirectly by finding another class B that we already know how to count, and showing that A ~ B. This is an alternative to explicitly describing a function that counts a class directly according to Introduction to Counting.
Then counting B, establishing for some k that B ~ k, justifies the inference that A ~ k, since Thm* (A ~ B) (B ~ C) (A ~ C).

Thus developing the skill of counting abstractly specified classes depends partly on developing a few basic forms that one knows how to count, and partly on developing the skill of "translating" new descriptions of classes into these forms one already knows how to count.

If you take a finite range of consecutive integers and add the same number to them all then you get a new collection with the same size as the old one.We will normally indicate such consecutive integer collections either with

The notation {i..j}, which mentions the least member and the number
after the largest member, turns out often to be more convenient to use than the more natural notation {i...j} which mentions both ends. (With both notations there are infinitely many ways of specifying the empty class, by picking ends in the "wrong" order, e.g., {4...3}, {1...-2}, {0..0}, or {0..(-3)}.)

We shall also adopt {0..k} as our "standard" finite class having k members, rather than the more every-day counting set {1...k}.
We tend to use this standard when precisely expressing facts about class size.
We shall abbreviate {0..k} as k, connoting "the first k members of ".