Binary search: elaborate on correctness

jxu · web-flow · commit 995370cb96a8 · 2023-10-15T17:21:41.000-04:00
diff --git a/src/num_methods/binary_search.md b/src/num_methods/binary_search.md
@@ -83,7 +83,7 @@ The binary search, the way it is described above, finds the partition of the arr
 It is possible to use arbitrary monotonous predicate instead of $k < A_M$. It is particularly useful when the computation of $f(k)$ is requires too much time to actually compute it for every possible value.
 In other words, binary search finds the unique index $L$ such that $f(L) = 0$ and $f(R)=f(L+1)=1$ if such a _transition point_ exists, or gives us $L = n-1$ if $f(0) = \dots = f(n-1) = 0$ or $L = -1$ if $f(0) = \dots = f(n-1) = 1$.
 
-Proof of correctness supposing a transition point exists, that is $f(0)=0$ and $f(n-1)=1$: The implementation maintaints the _loop invariant_ $f(l)=0, f(r)=1$ and terminates when $r - l = 1$, giving us our desired transition point.
+Proof of correctness supposing a transition point exists, that is $f(0)=0$ and $f(n-1)=1$: The implementation maintaints the _loop invariant_ $f(l)=0, f(r)=1$. When $r - l > 1$, the choice of $m$ means $r-l$ will always decrease. The loop terminates when $r - l = 1$, giving us our desired transition point.
 
 ```cpp
 ... // f(i) is a boolean function such that f(0) <= ... <= f(n-1)
