udiv_qr_3by2 vs divappr

[paul zimmermann]

       Dear Niels,

it works with r = (u_0 - q d_1 - p_1 - 1) \bmod \beta line 6 in all
cases, assuming it works with -1 replaced by - [p_0 > 0].

We only need to check the case p_0 = 0.

p_0 = 0 means that q d_0 is divisible by \beta, i.e., R' is multiple of \beta.

Let still <r_1, r_0> be the two low words from R'. We have r_0 = 0.

We have r = r_1 - 1 in the algorithm, instead of r = r_1.

For the first adjustment, the only case that differs from the original
algorithm is when r_1 = q_0 thus r = q_0 - 1 and the first adjustment
no longer applies. Since R' > q_0 \beta - \beta^2 [*], then necessarily
R' = q_0 \beta.

If the second adjustment does not apply, then r <= d_1 - 2, which means
q_0 <= d_1 - 1, thus 0 <= R' <= (d_1-1) \beta and we are done.

If the second adjustment applies, then r >= d_1 - 1, which means
q_0 >= d_1, thus after the adjustment, R = q_0 \beta - d > -\beta.
(For the upper bound, R < \beta^2 - d <= d.)

[*] the proof of Theorem 3 from [4] says "The lower bounds ... and
\tilde{r} > q_0 \beta - \beta^2 follow in the same way as in the proof of
Theorem 2".

For the second adjustment, assume r = d_1 - 2, in which case the second
adjustment would have been made with r = r_1.

If the first adjustment did not apply, then we have r_1 - 1 = d_1 - 2 < q_0,
thus r_1 = d_1 - 1 < q_0 + 1. Thus r_1 <= q_0. But since
R' > q_0 \beta - \beta^2, then R' = <r_1, 0> = <d_1 - 1, 0> which is ok.

If the first adjustment did apply, then we have r = r_1 + d_1 mod \beta,
which with r = d_1 - 2 implies r_1 = \beta - 2. If R' < 0, then
R' = r_1 \beta - \beta^2 = -2 \beta which is ok. If R' >= 0, then
R' = \beta^2 - 2 \beta. But this is not possible with the upper bound
R' < max(\beta^2 - d, q_0 \beta) - \beta, since \beta^2 - d <= \beta^2/2,
and since the first adjustment did apply, r >= q_0 thus r_1 - 1 >= q_0,
thus q_0 <= \beta - 3.

Surely this can be simplified...

Paul