The modulus 0 < M < 2WM occupies a register of WM-bits width:
 ←WM→ M

We will use ↜curly arrows↝ to refer to the widths of hypothetical zero and nonzero segments of registers, for the purpose of min/max width analysis of the intermediate results in our computation.

0 ≤ JM < WM is one less than the measure of M:
 0 M ↜JM↝

Lemma 1: For any integers A ≥ 0, B > 0, C = ⌊A / B⌋, Measure(C) ≤ Measure(A) - Measure(B) + 1.

Therefore, Measure of BM will be less than or equal to:

2WM - Measure(M) + 1 = 2WM - JM

 0 < BM < 2KM ←2WM→ 0 BM ↜JM↝ ↜2WM - JM↝

0 ≤ X < 2KM is the integer to be reduced modulo M, and occupies a register of twice the bitness of the register containing M:

 X ←2WM→

1: Xs = X >> JM

 0 XS ↜JM↝ ↜2WM - JM↝

Lemma 2: For any integers A ≥ 0, B ≥ 0, C = A × B, Measure(C) ≤ Measure(A) + Measure(B).

2: Z  := Xs × BM

 0 XS × 0 BM ←4WM→ = 0 Z ↜2JM↝ ↜4WM - 2JM↝

3: Zs := Z >> 2WM - JM

 ←4WM→ 0 ZS ↜2WM - JM↝

 ←2WM→ 0 ZS ↜2WM - JM↝

4: Q := Zs × M

 0 ZS × 0 M ←3WM→ = 0 Q ←2WM→