Proving the Assertions (4)
Induction Step: Assume it is true
for an
arbitrary time; show it is true the next
time (if there is a next time).
Assume the assertion is true
now.
Suppose there is a next time the
program gets
to that point.
What happened
in between?
(("k <
i) a[k] != v ô i <
a.length)