= Linear search correctness
The <loop invariant> just before inspecting index $i$ is: $0\leq i\leq n$, and no entry at an index $k<i$ matches $x$. Initially $i=0$, so there are no earlier entries. A failed <equality test> extends the excluded region by one position and preserves the <loop invariant>. A successful <equality test> at index $i$ establishes a match; the <loop invariant> establishes that it is the first one. At exhaustion, $i=n$ and every entry has failed, so the absent result is correct. The number $n-i$ of remaining entries decreases after each failed <equality test>, proving termination for a finite <sequence>. Together these establish <algorithm correctness> under the assumptions that the <input> is stable and each <equality test> terminates. No step of the argument compares the relative order of values.
Back to article page
