A statement that is true upon entering the loop, and after every iteration.

Proving Loop Invariance

Basis

Show that LI holds when entering the loop

Induction Step

We show that LI holds before an iteration and holds after that iteration