Proof Obligation 1
Show
INV and k!=0 and ~odd(k) ==> P1
We can do this by examining each clause of P1 and seeing if it is implied by the information on the left of the implication...
k/2 >= 0 is implied by k>=0 in INV...
x!=0 is a direct component of INV...
z*z != 0 is implied by z!=0 in INV...
rewrite x^n = y*(z*z)^(k/2) so we have:
x^n = y*z^(2*k/2)
since even(k), we know 2*k/2 = k, and so:
x^n = y*z^k, a direct component of INV.
QED
