PROOF OBLIGATION 1




We must now show that  

    INV and (r >= y)  ==> P2


P2 can be rewritten as

     y <= r and x = q*y + r - y + y


The clause

     INV and (r >= y)


is the same as

     0 <= r  and  y <= r  and  x = q * y + r


So, each clause of P2 is directly a clause 
     of INV and (r >= y)


QED