Problem set 4   --- Solutions
                                      
The LI we will be using is "t is the number of occurances of x in A[f...i-1]
We will therefore try to prove the predicate 
P(n) : "if there are at least n iterations then at the end of the 
n'th iteration we have that t_n = # of occurance of x in A[f...i_n-1]"
(notice that t_n,i_n stand for the values of t,i at the end of the n'th 
iteration.

* We first prove the LI predicate. 
   P(0) holds since t_0 = 0 = # of occurance is A[f...i_0-1] (notice that i_0=f
so the range above is an empty one, from f to f-1).
   Assume P(n) holds. We show P(n+1) holds too. i_{n+1} = i_n + 1.
   So the range A[f...i_{n+1}-1] = A[f...i_n]. Now, t_n is the # of occurances
   of x in A[f...i_n -1] and so # of occurances of x in A[f...i_{n+1}-1] is
   t_n is A[i_n] != x and t_{n+1} = t_n + 1 if A[i_n] == x. But notice that 
   the code is doing this precisely (a subtle point is that at the n+1 th 
   iteration, the value of t is updated according to i_n, as i changes its
   value at the end of the iteration.) Hence 
   t_[n+1] = number of occurances of x in A[f...i_{n+1}-1], and the LI is proven.

   To show termination notice that T_n = l - i_n is decreasing, and that it is
   at least 0 as the long as the loop is iterated, simply by the condition 
   'while i<= l '. Hence termination is guaranteeed.

   At exit, the value of i must be l+1 is this is the first time the condition
   for entering the loop is violated. Using the LI we can conclude that
   t is the number of occurances of x in A[f...i-1], but since i+l+1 this is
   the number of occurances of x in A[f...l] as required.