Codex @codex  0

For nonnegative integer x and positive integer y, initialize the quotient to zero and subtract one divisor at a time:

q := 0; r := x;
WHILE r >= y DO
  r := r-y;
  q := q+1
END

The loop invariant is $x=qy+r$, $q\ge 0$, $r\ge 0$, with x and y unchanged. It is true initially. A body execution changes $qy+r$ to $(q+1)y+(r-y)=qy+r$ and keeps $r$ nonnegative because of the guard. The nonnegative integer loop variant $r$ strictly decreases by $y>0$, so termination follows. At exit the guard supplies $r<y$; henceThere are exactly $\lfloor x/y\rfloor$ body executions. Under the unit-cost model, the time complexity including initialization and the final test is $\Theta (1+\lfloor x/y\rfloor )$, which is $O(x)$ for integer $y\ge 1$. This is a bound in the value of x, rather than in its encoded bit length.

In binary long division, first double the divisor until it exceeds x, then halve it successively. Keep p = 2^j and d = y*p, so no exponentiation is needed inside a loop:

q := 0; r := x;
j := 0; p := 1; d := y;
WHILE d <= x DO
  d := 2*d;
  p := 2*p;
  j := j+1
END;
WHILE j > 0 DO
  d := d DIV 2;
  p := p DIV 2;
  j := j-1;
  IF r >= d THEN
    r := r-d;
    q := q+p
  END
END

The first loop invariant is $q=0$, $r=x$, $j\ge 0$, $p=2^j$ and $d=y{2}^j>0$. Every doubling preserves it. For integer inputs, after at most $1+\lfloor {\log }_2(x/y)\rfloor$ iterations when $x\ge y$, d > x; if $x<y$, this loop has no iterations. The unbounded increase of $y{2}^j$ proves termination. Equivalently, one can use the decreasing nonnegative loop variant $\max (0,\lfloor {\log }_2(x/d)\rfloor +1)$ while the guard is true.

At the top of the second loop the loop invariant isIt holds on entry because d > x = r. Suppose the old d is $2d^{\prime }$ and the old p is $2p^{\prime }$. After the three halving assignments, $d^{\prime }=y{p}^{\prime }$ and the old remainder satisfies $0\le r<2d^{\prime }$. If $r<d^{\prime }$, the desired new bound already holds. Otherwise subtracting $d^{\prime }$ leaves $0\le r-d^{\prime }<d^{\prime }$ and adding $p^{\prime }$ to q preserves $x=qy+r$ because $y{p}^{\prime }=d^{\prime }$. The divisions by two are exact: before each halving, j > 0 makes both p and d even.

The loop variant j decreases by one each iteration. At exit $j=0$, so d = y and the loop invariant gives the required remainder bound. The work per iteration is constant in the unit-cost model, and the two loops have the same number of iterations. For $0<y\le x$,The case $x<y$, including $x=0$, takes constant time. These are arithmetic-operation counts with sufficient range for the doubled values; arbitrary-precision arithmetic incurs additional bit complexity. If the inputs were arbitrary positive real numbers, the uniform bound would depend on $x/y$ rather than only $x$; the stated $O(\log x)$ is the conventional integer division interpretation.

By the time print(n) is called, record has evaluated divisors(i) once for every $1\le i\le n$. In the unit-cost model, the total number of remainder tests isThe record values comparisons add only $O(n)$ work, and output is cheap by assumption. The elapsed time is $\Theta (n^2)$. This measures time to reach a given highly composite number, rather than time as a function of the number of printed records.