- ... arithmetic,
^{0.1}
- It should be noted that an extension
of ACL2 supporting the reals through non-standard analysis has been implemented
by Ruben Gamboa.[GAM99]
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.

- ...:
^{1.1}
- The actual ACL2
definition of
*fl* (see `fl`) is given in terms of the
(unfortunately named) built-in function *floor*. The
``definition'' stated here is actually a lemma derived from that
definition. Since all properties of the function that are of interest
to us are consequences of this lemma, we shall treat it as a
definition. Henceforth, we shall not have occasion to refer to the
ACL2 function *floor* and will use that term only in reference to
*fl*.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.

- ... function:
^{1.2}
- ACL2 provides two built-in
``remainder'' functions,
*rem* and *mod*, which agree on positive
arguments but not on negative arguments: *rem* has the oddness property
, whereas *mod* satisfies the desideratum
expressed by Definition 1.2.1. Our theory, therefore, is based on *mod*.
Note that the ``definition'' given here actually corresponds to an ACL2 lemma,
derived from the axioms that characterize the function.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.

- ... Pro.
^{6.1}
- Earlier processors did not conform to the behavior described in
Section 9.4 with respect to the selection between two NaN operands of an x87 instruction.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.

- ... approximation;
^{13.1}
- The first
result is not used in the analysis of the algorithms presented here, each of which involves only two quotient approximations.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.

- ... error:
^{13.2}
- By exhaustive computation, we could establish an error bound slightly less than
, which would reduce the number of special cases to be checked from 1027 to 573, but the bound is sufficient
for the proof of Theorem 13.2.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.