Finite real interval operations enclose their exact values

For intervals $X=[a,b]$ and $Y=[c,d]$, addition and subtraction have exact endpoint ranges $[a+c,b+d]$ and $[a-d,b-c]$. For multiplication, the function $xy$ is affine in either variable with the other fixed, so its extrema on the rectangle $X\times Y$ occur at one of the four corners. If $0\mathrm{\notin }Y$, reciprocal is monotone on $Y$, and division is multiplication by the exact reciprocal interval; squaring has lower endpoint $0$ when $0\in X$ and otherwise its endpoint minimum, with endpoint maximum in both cases.

Each exact lower and upper endpoint in step 1.1 is expanded outward by the downward and upward roundings in [F1]; [F2] puts the exact endpoint between those rounded values. Thus every finite interval-operation result contains its exact operation range. If an endpoint overflows or a domain restriction fails, the operation reports a non-finite status and the Statement asserts no finite enclosure.

Order the nodes of the finite acyclic graph topologically. Input and constant values lie in their supplied intervals by the enclosure hypotheses. Inductively, if an operation node has predecessor values in their computed intervals, step 2.1 shows that its exact output belongs to the computed output interval. Shared nodes reuse the same value by [F3], so the induction applies also to correlated intermediate values. It reaches every node and therefore the root, for every admissible assignment.