Problem set 5   --- Solutions
                                      
(i) Without understanding the connection between y and x it's hard to
say what's ahppening in this loop. Playing around with some small number it 
seems that y=x*x is a plausible invariant. Indeed, if we start, say, at x = 5, 
we get y=25, and then x=4, y=16; x=3, y=9 and so on. So we try to prove the
following LI. 
P(i): if there are at least i iterations then y_i = x_i^2. Also x_i>=0
P(0) holds because of the initial setting y = x*x
If we know P(i), we get y_{i+1} = y_i - 2*x_{i+1} - 1 # (why? bc we
modiy y using the "old" y and the x that was just changed)
 = x_i ^ 2 - 2*(x_i-1) - 1 = x_i^2-2x+1 = (x_i-1)^2 = x_{i+1)^2 
To show that x_{i+1} >=0 it's enough to show that x_i>=1. This is indeed the 
case (asuming there are at least i+1 itertions which we may): by the
induction hypothesis, we know that x_i>=0, and also that y_i=x_i^2. But since 
the loop continued beyond the i'th iteration, it must be that y_i>0, hence 
x_i>0 and we are done.


(ii) if y = y-2*x is the used instead of y = y -2*x-1 the loop 
will run forever: take for example x=1, then y is initially 1, and
in the firt iteration x will become 0 and y remain 1. Then x will become -1 
and so next y will become 3. It is easy to see that x will continue to 
decrease and become more and more negative and y increase and will never be 0. Therefore the loop will run forever. In fact, any value of x will result in 
an infinite loop with this code.

(iii) Here are some examples of L such that L = L o L. 
   L = {epsilon}
   L = S* where S is any subset of Signma. 
It is not hard to hard to show that the example L = {epsilon} is the only
example in which L is nonempty and finite (try to see why!).