Proof Obligation 2
Show
INV and (k < b) ==> P3
QED
