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-08-01