Representations of Integers

Existence. Just before each test of the guard on line 3, the invariant $𝑃(𝑡)$ is the conjunction of three clauses.

1. Expansion. $𝑛={\sum }_{𝑖=0}^{𝑡-1}{𝑎}_{𝑖}{𝑏}^{𝑖}+{𝑞}_{𝑡}{𝑏}^{𝑡}$. The sum is empty, hence $0$, when $𝑡=0$.
2. Digits. $0\leq {𝑎}_{𝑖}<𝑏$ for every $𝑖<𝑡$.
3. Bound. ${𝑞}_{𝑡}\geq 0$.

The variant is ${𝑞}_{𝑡}$. Initialization and maintenance keep $𝑃(𝑡)$ true at every test of the guard. Termination shows that the guard fails. Exit reads the expansion off $𝑃(𝑡)$ at that test.

Initialization. After lines 1 and 2, and before the guard is tested, the expansion says $𝑛={𝑞}_{0}$. The digit clause is vacuous. The bound holds because ${𝑞}_{0}=𝑛>0$.

Maintenance. Assume $𝑃(𝑡)$ and the guard on line 3, and execute lines 4 and 5 once. The new digit satisfies $0\leq {𝑎}_{𝑡}<𝑏$, and the earlier digits are unchanged, so the digit clause holds at $𝑡+1$. The new quotient meets the bound. If ${𝑞}_{𝑡+1}\leq -1$, then

$${𝑞}_{𝑡}=𝑏{𝑞}_{𝑡+1}+{𝑎}_{𝑡}\leq -𝑏+(𝑏-1)=-1<0,$$

contradicting ${𝑞}_{𝑡}>0$. The expansion carries to the next test of the guard:

$$\begin{aligned}𝑛 & =\sum _{𝑖=0}^{𝑡-1}{𝑎}_{𝑖}{𝑏}^{𝑖}+{𝑞}_{𝑡}{𝑏}^{𝑡} \\ & =\sum _{𝑖=0}^{𝑡-1}{𝑎}_{𝑖}{𝑏}^{𝑖}+(𝑏{𝑞}_{𝑡+1}+{𝑎}_{𝑡}){𝑏}^{𝑡} \\ & =\sum _{𝑖=0}^{𝑡-1}{𝑎}_{𝑖}{𝑏}^{𝑖}+{𝑎}_{𝑡}{𝑏}^{𝑡}+{𝑞}_{𝑡+1}{𝑏}^{𝑡+1} \\ & =\sum _{𝑖=0}^{𝑡}{𝑎}_{𝑖}{𝑏}^{𝑖}+{𝑞}_{𝑡+1}{𝑏}^{𝑡+1}.\end{aligned}$$

Thus $𝑃(𝑡+1)$ holds.

Termination. The bound clause says the variant ${𝑞}_{𝑡}$ is a nonnegative integer. Whenever the guard holds, the body replaces it by a strictly smaller one. Maintenance has already given ${𝑞}_{𝑡+1}\geq 0$, and

$${𝑞}_{𝑡}-{𝑞}_{𝑡+1}=(𝑏-1){𝑞}_{𝑡+1}+{𝑎}_{𝑡}.$$

If ${𝑞}_{𝑡+1}\geq 1$, the right-hand side is at least $𝑏-1\geq 1$. If ${𝑞}_{𝑡+1}=0$, it equals ${𝑎}_{𝑡}={𝑞}_{𝑡}\geq 1$. Thus ${𝑞}_{𝑡+1}<{𝑞}_{𝑡}$. If the guard never failed, the successive values of the variant would be a strictly decreasing sequence of nonnegative integers, whose set of values would have no least element, contradicting Proposition 1.1. So the guard fails after finitely many iterations.

Exit. The guard on line 3 has failed, so ${𝑞}_{𝑡}=0$, and $𝑃(𝑡)$ still holds. The expansion collapses to

$$𝑛=\sum _{𝑖=0}^{𝑡-1}{𝑎}_{𝑖}{𝑏}^{𝑖},$$

and the digit clause gives $0\leq {𝑎}_{𝑖}<𝑏$. Here $𝑡\geq 1$: the case $𝑡=0$ would mean ${𝑞}_{0}=𝑛=0$. Line 6 sets $𝑘=𝑡-1$. The last pass through line 4 began under the guard ${𝑞}_{𝑘}>0$ and produced ${𝑞}_{𝑘+1}=0$, so ${𝑞}_{𝑘}={𝑎}_{𝑘}$ and ${𝑎}_{𝑘}\neq 0$.

Uniqueness. Suppose ${\sum }_{𝑖=0}^{𝑘}{𝑎}_{𝑖}{𝑏}^{𝑖}$ and ${\sum }_{𝑖=0}^{𝑚}{𝑐}_{𝑖}{𝑏}^{𝑖}$ are two such expansions. Set ${𝑎}_{𝑖}=0$ for $𝑖>𝑘$ and ${𝑐}_{𝑖}=0$ for $𝑖>𝑚$, and let $𝑁=\max (𝑘,𝑚)$. Then

$$\sum _{𝑖=0}^{𝑁}({𝑎}_{𝑖}-{𝑐}_{𝑖}){𝑏}^{𝑖}=0.$$

Assume, on the contrary, that ${𝑎}_{𝑖}\neq {𝑐}_{𝑖}$ for some $𝑖$, and let $𝑟$ be the least such index. The powers below ${𝑏}^{𝑟}$ cancel, so

$${𝑎}_{𝑟}-{𝑐}_{𝑟}=-\sum _{𝑗=1}^{𝑁-𝑟}({𝑎}_{𝑟+𝑗}-{𝑐}_{𝑟+𝑗}){𝑏}^{𝑗}.$$

The sum is empty when $𝑟=𝑁$, and in every case the right-hand side is a multiple of $𝑏$. Thus $𝑏∣({𝑎}_{𝑟}-{𝑐}_{𝑟})$. But $1\leq |{𝑎}_{𝑟}-{𝑐}_{𝑟}|\leq 𝑏-1$, so $𝑏∤({𝑎}_{𝑟}-{𝑐}_{𝑟})$. This is a contradiction. Therefore ${𝑎}_{𝑖}={𝑐}_{𝑖}$ for every $𝑖$. In particular ${𝑐}_{𝑘}={𝑎}_{𝑘}\neq 0$ and ${𝑎}_{𝑚}={𝑐}_{𝑚}\neq 0$, so $𝑘=𝑚$.