Your intuition is a great starting point. To formalize this, consider denoting by $F(n)$ the number of times the `col--`

happens, or equivalently, the total time you waste in the `while`

loops.

Notice, that `col`

starts with the value of $n$, and can go down to **up to** $0$ with “jumps” of $1$. Its important that we **never** pass $0$, since it now means the total number of times `col--`

can ever happen is at most $n$. Thus, $F(n)=O(n)$.

Now, consider the rest of the code. You have to account for the `for`

loop, but notice we already counter the `while`

loop that is in it with the value of $F(n)$, so we need to calculate the complexity only for any other operations. But clearly, they don’t cost us more than $O(n)$ total, and hence we can say that the algorithm has $O(n)$ run-time.

I believe this should be formal *enough*. If you want to be even more formal, consider:

- Actually proving that
`col`

never goes lower than $0$ - Writing line numbers in the algorithm, and explaining the total cost of each line (using the same methods as in this proof)