Proving correctness of search algorithms
The idea of the algorithm is to maintain the following invariant:


  If $x$ is in the matrix, then it is in the submatrix whose top right corner is $e$.


The invariant clearly holds in the beginning, since $e$ is the top right corner of the original matrix.

If $e &gt; x$ then all elements below $e$ are also larger than $x$, and so $x$ cannot be contained in that column. Therefore the invariant continues to hold with $e$ replaced with its left neighbor (if $e$ has no left neightbor, we can deduce that $x$ is not found in the matrix).

If $e &lt; x$ then all elements to the left of $e$ are also smaller than $x$, and so $x$ cannot be contained in that row. Therefore the invariant continues to hold with $e$ replaced with its neighbor below (if any).

On an $n \times m$ matrix, this process terminates in at most $n+m$ steps, either finding $x$ or determining that it does not appear in the matrix.