I think I have to prove that the invariant is true for I(0) which is the basis which is easy, and then assume the ith works, and prove i+1 works, and then prove that it terminates correctly and then I'll have the full proof.
It's easy to just figure out the values like you suggest and say yes, 1=1 so it is correct, but that's not a formal enough proof, it just tells us that it should be correct.
Well the question as asked does not ask for a proof of the invariant, but
You can show the base cae is true, now suppose the invariant holds for some , if is odd then on the -st trip around the loop at the top of the loop .
Now at the end of the loop:
and:
(note in the last line the value of used is that produced by the previous line not what it was at the top of the loop)
So the invariant holds in this case.
Now if is even, at the top of the look after the k-th itteration:
and at the end of the loop:
and:
so the invariant holds in this case also, and so the given loop invariant is indeed a loop invariant for this loop.
RonL