... 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.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.