PROOF OBLIGATION 3 We must show that P5 ==> POST I5 can be rewritten as 0 <= r < y and x = q * y + r Both clauses of POST are direct parts of P5 QED
We must show that
P5 ==> POST
0 <= r < y and x = q * y + r
QED