IEEE-Compliant Square Root

  • David M. Russinoff


Many of the preceding results are propositions pertaining to real variables, which are formalized by ACL2 events in which these variables are restricted to the rational domain. Many of the lemmas of this chapter similarly apply to arbitrary real numbers, but in light of our present focus, these results are formulated to correspond more closely with their formal versions. Apart from the informal discussion immediately below, the lemmas themselves contain no references to the real numbers or the square root function.

Copyright information

© Springer Nature Switzerland AG 2019

Authors and Affiliations

  • David M. Russinoff
    • 1
  1. 1.Arm HoldingsAustinUSA

Personalised recommendations