I define numerals to be non-empty sequencs of digits and specify how, for a given base, each numeral denotes a specific natural. It remains to show that, for any given base:

- for every natural, there is at least one numeral to represent it;
- among the numerals representing a given natural, there is a unique shortest and all others are just this one prefixed with various numbers of zero digits;
- every numeral does in fact represent a unique natural;
- the successor operation (described following the specification) on numerals does in fact transform a numeral representing one natural into another numeral representing that natural's successor; and
- the natural denoted by a numeral is equal to a particular sum (that I'll explain in more detail below) of powers of the base, each scaled by the natural represented by a digit in the numeral.

The specification requires a choice of natural n > 1 (i.e. with 1 as a member of n) for use as base and a choice of denotations, the digits, for the members of this natural n (i.e. for each natural in n, notably including 1 and 0). We can encode those choices by a monic list ({digits}: b |n), whose collection of inputs is our base, n; each index into b is a natural i in n that b maps to an entry that's our representation's digit (a text) representing this i. That b is monic just means we don't try to use the same digit to represent two distinct naturals. The specification then defines a partial order on numerals, that equates numerals that only differ by the addition or removal of a prefix consisting entirely of the zero digit. The specification ends by saying that each numeral denotes the natural that is the number of distinct, modulo this zero-prefix equivalence, numerals less than it.

Since we have 0 in 1 in n, we have 0 in unite(n), hence unite(n) isn't empty = 0; this shall be important when we come to study the successor operation on numerals, which treats the digit representing unite(n) specially – because unite(n) +1 is n (so, given enough arithmetic, you can think of unite(n) as n −1).

For a given choice ({digits}: b |n) of representation, refer to numerals understood with respect to that representation as b-numerals. Our mapping b enables us to transform numerals, and hence the specification, into an equivalent representation using lists (n: :). Define a mapping

- digit = (: (: (n: digit(b, K, i) ←i :) ←K :{b-numerals}) ←({digits}: b |n) :{monic mappings})

for which digit(b, K, i) is the natural represented by the digit in K
that has i digits to its right. For each b-numeral K, digit(b, K) is thus a
list whose entries are in n; the length of this list is the number of digits in
K. (Note that I write lists left to right, with a list f expressed as [f(0),
f(1), …] so digit(b, K)'s representation as [digit(b, K, 0), digit(b, K,
1), …] reverses the digits of K; its right-most digit gives us digit(b,
K, 0) and each successive digit(b, K, i) comes from the next
digit *leftwards* in K. Using the usual form of base ten, with b as its
encoding, digit(b, 3210) = [0, 1, 2, 3], for example.)

For any monic ({digits}: b |n) with n > 1, digits(b) provides a
one-to-one correspondence between b-numerals and non-empty lists (n: :). It
thus enables us to discuss our specification in terms of an equivalent
specification for lists (n: :) in place of numerals. Because we now have lists
of naturals, we can do arithmetic without having to go via the
indirection of representation, encoded by b, all the time. We can also
use list concatenation, denoted by the
binary operator &, to be read as and then

; when h = f&g, f is
described as a prefix of h and g as a suffix.

The mapping digit(:b|n) transforms any b-numeral K into a list; any prefix in K of zero-digits, b(0), becomes a suffix of digit(b, K) whose entries are all 0; and our comparison ignores these. So let's define a mapping ({lists (n: :)}: trim |{non-empty lists (n: :)}) by

- trim(n: h |m) = (: h :unite({1+i in m: h(i) > 0}))

For a given list (n: h |m), consider p = unite({1+i in m: h(i) > 0}), for which trim(h) = (: h :p). If all entries in h are 0, no h(i) is > 0 so p is unite({}) = {}, which is 0, making trim(h) = (: h :{}) = []. So trim maps the all-zero lists to [], the empty list. (For these purposes, [] itself is an all-zero list and h([]) = [], too.) Any other list has an entry > 0; each index i of a non-zero entry contributes i+1 to the union we take to produce p; and i is a member of i+1, which p subsumes, so i is in p; thus every index at which h has a non-zero entry is in p. Furthermore, any union of naturals is one of those naturals (that is ≥ all of the others) so p is in fact i+1 for some i for which h(i) > 0, so the last entry in trim(h) = (:h:p) is non-zero. To include also the p = 0 case, we can assert that trim(h) doesn't have 0 as its last entry (true for [] simply because it doesn't have a last entry at all). Since all non-zero entries in h are at indices of trim(h), i.e. indices < p, every index i of h that isn't an index of trim(h) has h(i) = 0 and we have h = trim(h)&({0}: |k) for some natural k; h is equal to trim(h) precisely if k is 0, precisely if h doesn't have 0 as last entry.

Now, the specification of numerals deems two b-numerals equivalent precisely if each is a (possibly empty) sequence of zero digits to the left of a (possibly empty) sequence, the same in each numeral, of further digits; the lengths of the zero-sequences to the left may differ between the numerals. Such numerals become, under digits(b), t&({0}: |p) for some fixed list (n: t :) and diverse naturals p; trim maps each of these to trim(t). So digits(b) maps equivalent numerals to lists that are (: trim |)-equivalent. Conversely, (: trim |)-equivalent lists are diverse h = trim(h)&({0}: |k) with equal trim(h), i.e. lists are (: trim |)-equivalent precisely if they are t&({0}: |k) for diverse naturals k; but, in that case, any b-numerals they encode via digit(b) are equivalent. Thus (: trim |) encodes our equivalence on b-numerals (while extending it to identify [] with the all-zero lists).

So, for given ({digits}: b |n), we can use digit(b) as a one-to-one correspondence between b-numerals and non-empty lists (n: :); and we can use (: trim |) to encode our equivalence on these lists. When we come to encode our ordering on lists, we can use trim to encode ignoring a numeral's leading zero-digits, which digit(b) turns into trailing 0 entries in our lists; since trim's outputs include [], which isn't an output of digit(b), it'll be convenient to define this ordering in such a way that it applies to all lists (n: :), not just the non-empty ones to which digit(b) maps b-numerals; as it'll deem (: trim |)-equivalent lists equal, it'll treat [] as just another all-0 list, equivalent to [0].

Let's look at our ordering on lists (n: :) and refer
to the length of trim(f) as the trimmed
length

of f; this is the unique natural m for which trim(f) = (: trim(f)
|m); the definition of trim ensures that trim(f) = (:f|m), also. If two lists
have distinct trimmed lengths, the one with the greater trimmed length is
greater than the other. Othewise, the two lists are (before trimming) h = (: h
|j)&({0}: |p) and k = (: k |j)&({0}: |q) for some naturals j (their
trimmed length), p and q. In particular, there exist naturals m, p, q and a
list t for which h = (: h |m)&t&({0}: |p) and k = (: k
|m)&t&({0}: |q); namely, m = j, t = [] and the previously found p,
q. Let m be the least m for which such p, q and t exist; that is, the
intersection of all such m (we know m = j is one candidate, so this isn't an
empty intersection). If m is 0, then (:h:j) = trim(h) and (:k:j) = trim(k) are
equal and our lists are equivalent; otherwise, m is 1+i for some natural i and
we have h = (: h |i)&[h(i)]&t&({0}: |p) and k = (: k
|i)&[k(i)]&t&({0}: |q). By minimality of m, this tells us
[h(i)]&t and [k(i)]&t are
distinct; we can cancel t from this
leaving [h(i)] and [k(i)] distinct; since they have only one right value, 0,
these can only differ in the left value each relates to it, so h(i) and k(i)
must be distinct; the list with greater entry at index i is then greater than
the other.

By the structure of this definition, comparison of lists h and k gives the same answer as comparison of trim(h) and trim(k), so trim respects the orddering. The transformed specification also ensures that distinct outputs of trim are distinguished by the comparison; they either have different length or have an index at which their entries differ. Consequently, the number of distinct lists, modulo our equivalence, less than any given list h is just the number of trimmed lists less than trim(h); and this is just the natural encoded by the list h, in base n.

Having re-cast our specification in terms of the lists digit({digits}: b |n)
identifies b-numerals with, we can restate the expected properties of numerals,
above, in terms of non-empty lists (n: :); if our transformed specification has
these properties, the original specification must likewise have the properties
stated above. In particular, I only roughly stated the sum of scaled
powers

property above; in the lists (n: :) representation, it is finally
easy to state it concisely and precisely. The properties are then: for lists
(n: :) understood base n,

- each natural is represented by at least one list;
- the lists representing any given natural all have a common prefix, which is a list representing the given natural, and their entries after this prefix (if any) are all 0;
- each list represents a unique natural;
- for each natural m there is a list representing it of form ({unite(n)}: |k)&[i]&t with k natural (it may be zero), i in unite(n) and t a list (n: :), for which ({0}: |k)&[i+1]&t represents the successor of m; and
- the natural represented by a list (n: h :) is sum(: h(i).power(i, n) ←i :(:h|)).

Note that replacing h with trim(h) in the sum only discards various
0.power(i, n) for i with h(i) = 0; since these sum to 0, they don't change the
sum. In the case of an all-zero list, we get sum([]) and do depend on knowing
we're summing an empty list *of naturals* to get the answer 0 as the sum
(rather than the identity of some other addition).

So, now that we can talk about our numerals via a proxy representation that's equivalent but directly amenable to arithmetic, and we have trim to simplify our discussion of that representation, let's see what we can do about establishing our claimed properties of lists representing numerals. As it turns out, the last property (the sum of powers) is a good place to start; so let's begin by defining a mapping ({naturals}: S |{lists (n: :)}) to encode our sum of scaled powers, for base n as

- S(h) = sum(: h(i).power(i, n) ←i :(:h|))

Before we get into the detail, we need an important simple result from the study of polynomials: the particular case to which we need to apply it is with u = unite(n), giving us sum(: power(j, u +1) ←j :i).u +1 = power(i, u +1) for any natural i; this ensures that power(i, n) > unite(n).sum(: power(j, n) ←j |i). The right hand side of this is an upper bound on S(n: f :i), since this sum only has terms f(j).power(j, n) with j in i and each f(j) ≤ unite(n), the largest member of n.

In particular, if we have lists h, k with trim(h) longer than (: trim(k) |m), there is some i ≥ m for which natural h(i) > 0 so h(i) ≥ 1 gives S(h) a term h(i).power(i, n) ≥ power(i, n) > S(n: k :i) = S(k). The last step, S(:k:i) = S(k), follows from the terms dropped from the sum, by restricting k, all being of form k(j).power(j, n) with j ≥ m hence k(j) = 0.

For two lists h, k with equal trimmed length, if they're (: trim |)-equivalent then their sums of scaled powers have exactly the same terms with non-zero scalings so are equal; otherwise, there is some index at which they have distinct entries; all such indices are less than their trimmed length, so there is a maximal such index (their union), i. Every natural j > i for which either h(j) or k(j) is non-zero has, in fact, both h(j) and k(j) non-zero, with h(j) = k(j) so S(h) and S(k) have the same multiplier for power(j, n). Let T be the sum of all such terms. Then S(h) = T +h(i).power(i, n) +S(:h:i) and S(k) = T +k(i).power(i, n) +S(:k:i); as h(i) and k(i) are distinct, one of them is greater than the other; when this is h(i) > k(i), with both natural, we have h(i) ≥ 1 +k(i) and S(:h:i) ≥ 0, hence S(h) ≥ T +k(i).power(i, n) +power(i, n) > T +k(i).power(i, n) +S(:k:i) = S(k). Thus the list that has the higher entry at the highest index at which the lists differ, i.e. the list that's greater in our ordering of lists, also has the greater sum of scaled powers. So S maps greater lists to greater naturals and equivalent lists to the same natural; it is a homomorphism from the ordering on lists to the one on naturals.

Now let's consider the successor operation we've defined on lists; every list is equivalent to some list ({unite(n)}: |j)&[i]&t with i in unite(n); the successor of this is ({0}: |j)&[i+1]&t. The change in S between them gets no contribution from t (same contribution to each), with the latter getting i+1 instead of i as multiplier of power(j, n), contributing just power(j, n) = 1 +unite(n).sum(: power(p, n) ←p |j) more to the successor; at lower powers, the successor gets nothing while its predecessor gets unite(n).sum(: power(p, n) ←p |j); the difference is thus 1. Thus, for every list (n: h :), there is a successor list k for which S(k) = 1 +S(h); and that's the end of the messy formulae.

S preserves order, so it respects (: trim |)-equivalence and is monic on (| trim :), since distinct (as lists) outputs of trim are indeed distinguished by our order on lists. The all-zero lists are all equivalent, S maps them to 0; and 0 is the natural they represent, since no list is < any all-zero list. Every output of S is S(t) for some list t whose successor gives us S(t) +1, so (| S :) is closed under the naturals' successor mapping; since it includes 0 = S([0]) it is thus {naturals} and we have ({naturals}| S |{lists (n: :)}); as every list t is (: trim |)-equivalent to trim(t), we have ({naturals}| S |trim) and we know S is monic on trim's outputs; consequently, it is iso ({naturals}| S |trim) and every natural is S(t) for at least some list t; in particular, every natural is S(t) for exactly one output of trim, t (and for every list in ({t}: trim |) as these are (: trim |)-equivalent to t). For any list h, every trim-output t less than h has S(t) < S(h) and every trim-output with S(t) < S(h) is in fact t < h; since every natural is S(t) for some trim-output t, there are in fact S(h) outputs t of trim with t < h and h represents the natural S(h).

So we've proved that every list does indeed represent a unique natural, the natural represented by a list h is S(h) and that every natural is represented by at least one list. Furthermore, as S and trim both perserve our ordering on lists, any list h representing a natural has trim(h) representing the same natural; trim(h) is a prefix of h and all entries in h after this prefix are 0. So all that remains is some fine detail in the successor condition.

For every natural m there is indeed a list representing it; specifically, some output of trim; and appending any number of 0 entries to that gives a list representing the same natural, m. If the output of trim has any entry that isn't unite(n), then it is indeed of form ({unite(n)}: |k)&[i]&t for some natural k, some i in unite(n) and some list (n: t :). Otherwise, the output of trim is ({unite(n)}: |k) for some k and appending a 0 gives us ({unite(n)}: |k)&[0]&[] which, with i = 0 and t = [], is of the required form; since we merely appended a 0, this list is equivalent to our output of trim so represents the same natural m. In either case, ({0}: |k)&[1+i]&t does indeed represent m's successor, 1+m.

Written by Eddy.