From: Christoph Fuerst <ch.fuerst@gmx.at>
Date: Sun, 2 Apr 2017 18:56:39 +0000 (+0200)
Subject: Added reasoning for z
X-Git-Url: http://git.risc.jku.at/gitweb/?a=commitdiff_plain;h=ec17721e12a6245911eb991d00b7a56f87b14ad9;p=cfuerst%2Fformal-numbers.git

Added reasoning for z
---

diff --git a/report/formal.pdf b/report/formal.pdf
index a3781aa..8974510 100644
Binary files a/report/formal.pdf and b/report/formal.pdf differ
diff --git a/report/formal.tex b/report/formal.tex
index de6e576..ab315e5 100644
--- a/report/formal.tex
+++ b/report/formal.tex
@@ -347,10 +347,10 @@ $y = \pm \sqrt{x}$.\\
 Computing the \emph{integer-square-root} amounts to the following: Given a non-negative integer $a\in\mathbb{N}^+$,
 usually its square root is either an integer or irrational. The integer-square-root is defined as the non-negative
 integer $x\in\mathbb{N}^+$ that fulfills $x\leq \sqrt{a}<x+1$. Reformulated we immediately see that this is equivalent
-to $x := \lfloor \sqrt{a}\rfloor$. The integer-square-root is needed in the Baby-Step Giant-Step algorithm 
+to $x := \lfloor \sqrt{a}\rfloor$. The integer-square-root is needed in the Baby-Step Giant-Step algorithm
 (recall that $\lceil x\rceil + \lfloor -x\rfloor = 0$), but also
-in algorithms for prime-factorization of integers, because the largest prime-factor of $n\in\mathbb{N}$ 
-does noet exceed the integer-square-root of $n$. 
+in algorithms for prime-factorization of integers, because the largest prime-factor of $n\in\mathbb{N}$
+does noet exceed the integer-square-root of $n$.
 We present an algorithm that computes the integer-square-root, and analyze it afterwards.
 \begin{algorithm}[H]
 \begin{algorithmic}[1]
@@ -368,23 +368,29 @@ We present an algorithm that computes the integer-square-root, and analyze it af
         \label{alg:2}
 \end{algorithm}
 The first step of Algorithm \ref{alg:2} is the initialization of the result $x$ and two
-temporary variables $y$ and $z$. As for the While-Loop, we observe that initially 
+temporary variables $y$ and $z$. As for the While-Loop, we observe that initially
 \begin{align}
 x = x^2 &\leq a\quad  &\wedge& \quad y = x^2 + z \quad &\wedge& \quad z = 2x+1\label{eq:inv}\\
 0 &\leq a\quad &\wedge& \quad 1 = 0+1 \quad &\wedge& \quad 1 = 2\cdot 0 +1.\nonumber
 \end{align}
 We claim, that \eqref{eq:inv} is an invariant that is kept at each step of the loop. This is
-seen as follows: The tuple $(x,y,z)$ is updated to $(x',y',z')$, where 
+seen as follows: The tuple $(x,y,z)$ is updated to $(x',y',z')$, where
 $$
 (x',y',z') \leftarrow (x+1,y+z+2,z+2).
 $$
-Indeed, 
+Indeed,
 \begin{align*}
 y' = (x')^2 + z' &\Leftrightarrow y+z+2 = (x+1)^2 + z+2 = x^2 + 2x + 3 + z\\
 &\Leftrightarrow y = x^2 + 2x + 1 = x^2+z.
 \end{align*}
-as claimed. After finitely many iterations, we have $y > a$ and we terminate the algorithm with
-$x^2\leq a$ (as it holds in each step of the loop), and we conclude 
+as claimed. Similar, reasoning for $z'$ we obtain
+$$
+z' = 2\cdot x' + 1 \Leftrightarrow z+2 = 2\cdot (x+1) + 1 = (2x + 1) + 2
+\Leftrightarrow z = 2x + 1.
+$$
+
+After finitely many iterations, we have $y > a$ and we terminate the algorithm with
+$x^2\leq a$ (as it holds in each step of the loop), and we conclude
 $$
 y > a \Leftrightarrow (x^2+z) > a \Leftrightarrow x^2+2x+1 > a \Leftrightarrow (x+1)^2 > a,
 $$
@@ -417,7 +423,7 @@ hence we have shown $x^2\leq a < (x+1)^2$, and taking square roots shows the cla
 %   stepnumber=1,                  % the step between two line-numbers. If it's 1, each line will be numbered
 %   tabsize=2,	                   % sets default tabsize to 2 spaces
 % }
-% 
+%
 % {\tiny \lstinputlisting{../src/primefactors.cpp}}
 
 \begin{thebibliography}{9}