... 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 $ rem(-x,y) = -rem(x,y)$, 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 $ 1.5 \cdot 2^{-23}$, which would reduce the number of special cases to be checked from 1027 to 573, but the bound $ 2^{-22}$ is sufficient for the proof of Theorem 13.2.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.