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