Proving the correctness of an algorithm, which computes the connectivity of a directed graph
Suppose that the algorithm is incorrect. We can slightly modify the algorithm by moving lines 8,12 just after the inner loop. If the algorithm returns $k$ incorrectly at the end of step $i$, then there must exist vertices $v_s,v_t$, for $s,t&gt;i$, and a set $S$ of size $k-1$ not containing $v_s,v_t$, such that after removing $S$ there is no path from $v_s$ to $v_t$. I claim that $v_1,\ldots,v_i \in S$: if $v_j \notin S$ for some $j \leq i$, then since $S$ does not disconnect $v_j$ from any other vertex, we would have a path $v_s \to v_j \to v_t$. Since $v_1,\ldots,v_i \in S$, in particular $|S| \geq i$. Stated differently, $k-1 \geq i$. So if $i &gt; k-1$, this is impossible.

My proof, if correct, shows that you can actually use the weaker condition $i &gt; k-1$ in lines 8,12.