Minor nitpick: Around 2:35 the argument is made that one needs to ensure a minimum decrease for the loop termination expression; however this is not the case.  Rather, it is sufficient and necessary that the sequence of values either diverges, or converges to a value less than zero.  For instance, both these loops will provably terminate, for any positive values of x and n:

 

/* decreases x - 1 */
while (x > 1)
{
  x = x / 2;
}

 

/* decreases x */
while (x > 0)
{
  x = x - (1 / n);
  n = n + 1;
}