1,295
edits
| Line 69: | Line 69: | ||
If F1' = F2' then there is nothing to draw and requirement 8 is not relevant. So assume F1' < F2'. We must show that the ranges [I1, I2] and [S.F1' + T, S.F2' + T] have non-empty intersection. | If F1' = F2' then there is nothing to draw and requirement 8 is not relevant. So assume F1' < F2'. We must show that the ranges [I1, I2] and [S.F1' + T, S.F2' + T] have non-empty intersection. | ||
Let C = P' - (D1 + P/S). Then -0.5 < C <= 0.5. | Let C = P' - (D1 + P/S). Then -0.5 < C <= 0.5, by the definition of 'round'. | ||
Since F1' < F2' and they're both integers, we must have F2' - 0.5 > F1 (otherwise F1 would have rounded up to F2'). Therefore F2' - C > F1. Therefore S.(F2' - C - D1) > S.(F1 - D1). Therefore S.(F2' - C - D1) > I1. | Since F1' < F2' and they're both integers, we must have F2' - 0.5 > F1 (otherwise F1 would have rounded up to F2'). Therefore F2' - C > F1. Therefore S.(F2' - C - D1) > S.(F1 - D1). Therefore S.(F2' - C - D1) > I1. Now S.(F2' - C - D1) = S.(F2' - P' + D1 + P/S - D1) = S.F2' - S.P' + P = S.F2' + T. So S.F2' + T > I1. | ||
edits