Proof Obligation 3

Show

    INV and k!=0 ==> P3

which in this case is trivial, due to our if-then-else construction.

QED