Under Rule 2.6 and nearest rounding, \forall x, y \in \mathbb D, the following formulas achieve EFT z + zz = x + y:
\begin{align}
z & = fl( x + y); \\
w & = fl( z - x); \\
z1 & = fl( y - w); \\
v & = fl( w - z); \\
z2 & = fl( x + v); \\
zz & = fl( z1 + z2).
\end{align}
Proof.
The case when x and y admit representations with e(x) \geq e(y) has already been covered by the proof of Theorem 3.1 since it is easy to show that z2 = 0 following w = z - x in this case.
Therefore, we limit our discussion below to the complementary case, i.e., when x and y do not admit representations such that e(x) \geq e(y).
In this scenario, aside from the obvious condition d = e(x) - e(y) < 0, we also have that y cannot admit a representation with the exponent E_{\min} since, otherwise, any representation of x would lead to e(x) \geq e(y) for this representation of y.
Consequently, y admits a normal representation in \mathbb D.
We work with this normal representation of y in the following.
In other words, when writing y = m(y) \times \beta^{e(y)} below, the conditions e(y) > E_{\min} and \beta^{t-1} \leq \vert m(y) \vert < \beta^t are implied.
These conditions appear in Lemma ?, ? and Lemma ?, ? invoked in this proof.
The proof below consists of three parts: first, we show that z1=y-w under the above conditions; second, we show that w-z2 = z-x by invoking Theorem 3.1; third, we show that zz = z1 + z2.
We proceed to show that z1=y-w still holds
by separating the discussion into four cases based on the signs of f and g, similar to that in the proof of Theorem 3.1.
We assume that overflow does not happen when forming z for the four cases below.
The special scenario of overflow is addressed immediately after the discussion of these cases.
Adjustwidth. 1.5em
kwdcolorCase 1: if f \geq 0 and g > 0, we again have \zeta \in \mathbb Z as in Case 1 of Theorem 3.1, where \zeta is defined in (?), and thus, z = x + y. This leads to w = z - x = y
and z1 = fl(y - w) = 0 = y - w as desired.
Additionally, we also have v = -x, z2 = 0, and zz = 0 following w = z - x.
kwdcolorCase 2: if f \geq 0 and g \leq 0, we have d = f - g \geq 0, which contradicts the assumption d < 0. Thus, this is a null case.
kwdcolorCase 3: if f < 0 and g \geq 0, recall that z = m(z) \times \beta^{e(z)} = round(\zeta) \times \beta^{e(z)}, where \zeta is defined in (?),
we have
\begin{align}
z - x
& = \left( m(z) - m(x) \cdot \beta^f \right) \times \beta^{e(z)}
\\
& = \left( m(z) - m(x) \cdot \beta^f - m(y) \cdot \beta^g + m(y) \cdot \beta^g \right) \times \beta^{e(z)}
\\
& = y + \left( m(z) - m(x) \cdot \beta^f - m(y) \cdot \beta^g \right) \times \beta^{e(z)}
\\
& \in \left[ y - \tfrac{1}{2} \times \beta^{e(z)} , y + \tfrac{1}{2} \times \beta^{e(z)} \right]
\subseteq \left[ y - \tfrac{1}{2} \times \beta^{e(y)} , y + \tfrac{1}{2} \times \beta^{e(y)} \right]
.
\end{align}
From Lemma ?, ? presented after this theorem, we know
that y - fl(z-x) = y-w can only take values \pm 1 \times \beta^{e(y)-1}, 0, or \pm 1 \times \beta^{e(y)}, all of which are in \mathbb D.
Therefore, we have z1 = y-w as desired.
kwdcolorCase 4: if f < 0 and g < 0, we have that z admits a representation with e(z) \leq e(y) + 1 following Lemma 2.12.
Working with a representation of z such that e(z) \leq e(y) + 1 holds, the condition that g < 0 further
implies that e(z) = e(y) + 1.
Similar to (?), we have in this case
z - x
\in \left[ y - \tfrac{1}{2} \times \beta^{e(z)} , y + \tfrac{1}{2} \times \beta^{e(z)} \right]
= \left[ y - 1 \times \beta^{e(y)} , y + 1 \times \beta^{e(y)} \right],
where \beta = 2 is used for the last equality.
When t > 1, we can invoke Lemma ?, ? presented after this theorem to arrive at the desired result z1 = y - w as in Case 3.
The special situation t = 1 is addressed in Remark 6 following this theorem.
We now address the special scenario of kwdcoloroverflow when forming z.
Notice that overflow cannot possibly happen in Cases 1 and 2 above because we have e(z) < e(y) under the combination of assumptions d < 0 and f \geq 0.
Therefore, we need only to concentrate on Cases 3 and 4 above, where f < 0.
Moreover, since x and y must have the same sign for z to overflow,
it is sufficient to address only the case where both x and y are positive.
Because overflow leads to clipping in Dekker’s system, we have z = \big(\beta^t - 1\big) \times \beta^{E_{\max}} and, therefore,
z - x
= \left( \big(\beta^t-1\big) - m(x) \cdot \beta^{f} \right) \times \beta^{E_{\max}}
\geq \left( \big(\beta^t-1\big) - \big(\beta^t-1\big) \cdot \beta^{-1} \right) \times \beta^{E_{\max}}
= \big(\beta^t-1\big) \times \beta^{E_{\max}-1},
where f \leq -1 is used for the inequality and \beta = 2 is used for the last equality.
Moreover, because of overflow, we also have x+y>z, i.e., z-x<y.
Thus, by monotonicity, we have
\big(\beta^t-1\big) \times \beta^{E_{\max}-1} \leq w \leq y.
Because of (?), we can write
\begin{align}
y & = \tilde{m}(y) \times \beta^{E_{\max}-1} ; \\
w & = \tilde{m}(w) \times \beta^{E_{\max}-1} ,
\end{align}
where \tilde{m}(y)\in\mathbb Z and \tilde{m}(w)\in\mathbb Z.
Notice that we have used \tilde{m}(\cdot) instead of m(\cdot) for the mantissas in (?) and (?) because they are not necessarily valid representations in \mathbb D.
Moreover, since \tilde{m}(y) \leq \big(\beta^t - 1\big) \cdot \beta and \tilde{m}(w) \geq \big(\beta^t-1\big), we can write
y - w = \big(\tilde{m}(y) - \tilde{m}(w)\big) \times \beta^{E_{\max}-1},
where \tilde{m}(y) - \tilde{m}(w) \in \mathbb Z and 0 \leq \tilde{m}(y) - \tilde{m}(w) \leq \beta^t - 1.
Thus, y-w \in \mathbb D with (?) being a valid representation, which leads to z1 = y - w as desired.
This concludes the discussion for the special scenario of kwdcoloroverflow when forming z.
Now that we completed the demonstration of z1 = y - w, we proceed to show that w-z2 = z-x.
When f \geq 0, from the discussion above, Case 1 is the only nontrivial case under the conditions of the theorem,
for which w-z2 = z-x holds because w = z - x and z2 = 0.
When f<0, i.e., e(x) < e(z), following Theorem (3.1), operations (3.2), (3.2), and (3.2) form a 3op EFT over addition (after adjusting for the signs), which leads to w - z2 = z - x.
Combined with z1 = y - w obtained earlier, this leads to
z + z1 + z2 = x + y.
It remains to show that zz = z1 + z2, i.e., (3.2) also commits no rounding error.
For all non-empty cases discussed above, including the special scenario of overflow when forming z and the special systems with t=1, we have that z1 = y - w admits a representation in \mathbb D with an exponent no less than e(y) - 1.
Since d = e(x) - e(y) < 0, it follows that z1 can be expressed as \tilde{m}(z1) \times \beta^{e(x)} where \tilde{m}(z1) \in \mathbb Z.
Moreover, from the proof of Theorem (3.1), we have that z2 can be expressed as m(z2) \times \beta^{e(x)} where m(z2) \in \mathbb Z and \vert m(z2) \vert < M.
Therefore, z1+z2 can be expressed as an integer times \beta^{e(x)} as well, i.e., z1+z2 = \Big(\tilde{m}(z1) + m(z2)\Big) \times \beta^{e(x)}.
From (?), we have
\vert z1 + z2 \vert = \vert x + y - z \vert \leq \vert x + y - y \vert = \vert x \vert
following the nearest rounding property,
which leads to \vert \tilde{m}(z1) + m(z2) \vert \leq \vert m(x) \vert < M.
Therefore, z1+z2 \in \mathbb D and
zz = z1 + z2 follows.
End of proof for Theorem 3.2.