Re: Vincent's 5 Oct rad(xx) proof
On 2012-10-19 12:15:16 +0100, John Pryce wrote:
> > If m' = m, then r = b-m < b'-m' ≤ r'. So, let us assume that m' > m.
> Here you need to point out that this implies m' > (a+b)/2 else m' is
> between m and (a+b)/2, which contradicts the first * relation above.
Yes, or said otherwise, assuming m' - (a+b)/2 < 0 immediately yields
(a+b)/2 - m <= (a+b)/2 - m', which contradicts m' > m.
> You write "...seems true for any interval type". That's not the
> point, is it? You've proved it for any *number format*.
Yes, any bounded, non-empty intervals (which are seen at Level 1 here)
and any number format.
--
Vincent Lefèvre <vincent@xxxxxxxxxx> - Web: <http://www.vinc17.net/>
100% accessible validated (X)HTML - Blog: <http://www.vinc17.net/blog/>
Work: CR INRIA - computer arithmetic / AriC project (LIP, ENS-Lyon)