PROOF OBLIGATION 1
![]()
We must now show that
INV and (r >= y) ==> P2P2 can be rewritten asy <= r and x = q*y + r - y + yThe clauseINV and (r >= y)is the same as0 <= r and y <= r and x = q * y + rSo, each clause of P2 is directly a clause of INV and (r >= y)QED