The first step toward the definition of *qsqrt* is the following recursive function, the name of which is motivated by the
(unproven) observation that for
,

PROOF: If , then and the claim is trivial. Proceeding by induction, let , , and , and assume that . If , the claim follows trivially; otherwise, and

PROOF: The claim is trivial for . Let , , and , and assume that is -exact, i.e., . Then either and or

PROOF: The claim is trivial for . Let , , and assume that . If and , the claim is trivial. Otherwise, , , and

Accordoing to the next lemma, is uniquelt determined by the above properties.

PROOF: Let . If , then by Lemmas4.2.16,

We have the following variation of Lemma 6.1.15.

PROOF: The case follows from Lemmas 6.1.10 and 7.1.3. We proceed by induction on . Let and assume that . Then by Lemma 6.1.15,

David Russinoff 2017-07-06