From ec17721e12a6245911eb991d00b7a56f87b14ad9 Mon Sep 17 00:00:00 2001 From: Christoph Fuerst Date: Sun, 2 Apr 2017 20:56:39 +0200 Subject: [PATCH] Added reasoning for z --- report/formal.pdf | Bin 297554 -> 297700 bytes report/formal.tex | 24 +++++++++++++++--------- 2 files changed, 15 insertions(+), 9 deletions(-) diff --git a/report/formal.pdf b/report/formal.pdf index a3781aa42e03167d2f86b82137b4d2825acae24d..8974510c74c08f21e578031fb17aeded6f2d6a7a 100644 GIT binary patch delta 2699 zcmV;63Uu|-loI5X60m()0x~d@@lPp#&05=z+%^(@pRdrP8XnQ&owPRr9Ka3|EEd>! zfIMWgfIO{n3+c;P>WMw`^;;x$qnc7n65duYS0HxqA5y z{%fQK5z)i3(UU%tblcb}w)G7W<5EkEs7 zM8(JaV_qijKRsk+p8RrHC2;O=G&f(py$KmW2$B*H4WL?$8judWGGP!VNO0!#`z8PM zP?Y&At4nk5%XftLZe$X1Ng9iPGG{YUy%h?jlr;-#r_jC#jab_H+3No%CCsdeaEdrQA5@dVUAjLFJR(wmqy&j%3R@}J zRN!$$gz)pm)3XzmBB6B?GzpO^{)hRIt@6aX4YAI=7qF0!7zf;k6)3=)g@@8P&4lrv zE6(F=o4b_TJ_ej9Ae1>BI+2Vy@wbeQCJV5Vg~Gy%oe)-lj;WdhSr8tK&D&TBuH%D^ zWebdb3K%PqqH2k;PeEge;sayJn6Z4Gu|gw?eOvhgTW5sld0QWYwz4h}Uj!tWqoKDv zFL1zk9CpI+H{cY1$&6P3IyH3?#Ddf=^W#Ig4?!`M13C=of!0E|af-Z026?Igo~oEw z!c%QE^8*JkW>>($^@E3y^}6 z%noI=N*H7Do668G7T-1e%lgk8{AvnI^3S@*xxaR2t^K*X=kTG*%Rk!_HQ}{K^$rE8 zTSBpgu>`_@MPs>;!Hrj^F99C!@_-?Xsn-k)P?bQmCcRZls-e%*B$Bwz%>RaD0NF|T z6lQtAcVV-M&$<-#%$^I7Lz8(Iyys00m!w`@`_8o(BqWI=rqv}XITHx?%L`9|HTURg zUnV2~ltRKFsa^fI_oTr{lI&TOYDN%|QIBHhu-b2bsWaNQ-IEXSOx3gHhcbx3zKG85 z6bFg3R&6$imGn@WAWU0dz6xw%LV-j`Xww~#D7W(0m7)%haD2PXirsaCO;A}JJP~id z?TMmtzuCV2Z(Gk6xAzA6k4|U?Ywt?6h zl5aMDPB3mCQ02L$0pJafVr7-H?e4GzAt2*(^~%WLuIgH|AMV@spuZcMA<6lSmXBYo z<@1MYcED1vDQY_&Tsd85$9!F@e+U5=v`l!J?)3saz)0F3@r0xRztqAT@w8qzl?atz z=s6O3Na9maBGW;MWK!aY&pnqk^?Z|;q4-FDFfmgQ<|o(J_}Z&S6Q1dAFD#h1Pr!+CS~rdA`05v2%!CHCX)^406JV4IwrjLfjJhq_?Urt0NHrPNJu??r?5@ zv00JJP9nF@9NmSpdoL<13^z&2s2#M(0Y|WhXFl~SrHl)0*?cxkEL(sA~YtG zXgtvsV$;XsKwHSi+QMhoH*WJN02z2pFVYd=i_Or_waFCPWI~tp$zQ_@Ww4@ubbU8< zDJ%QsD+C8z+30&#{pvq0=n;iv2Q|;!3PttY*^#_FnI0KUP5>1sr6(&uGjoW_%xjAdW14n*iF)9GdRCJ>~FUZ>yh`kY&a}8n~Is)RFl4;5u$m$#`Q3-F4BH~{y*o;WbEz5 zNb~1?NbtSGf{=TFM02KR!_MEEc7-sYU*Hz|;hRh;GoAr8z6jLnudxCf2V2V*ebRG@##9Fk z_20W7CbVa$kBbb5>>qtCVqMv9E!~>3`QWnhH>UD%mpS&1g74~$12q-qi$jWJt%43N zeS35DKgi~#B!jMDhpu4(hpu4)hpu4*x2|CXUJwK|H8nVw5OM?`1T{4^IJYx$1V9#2 zHbO-*L^(q_Gc`9eGB!alLPa(>MKL%+IW;ynH!?UuJ|H|cLPat}IYT)!H8(RdHbF2# zMK(A^F*rgwH8wXlGB`m#T?#KuWo~D5Xdp8&G$50a1t@vQ5^>3ULtw@!#s(IkH3CqzDqc z(?go9kz#-1fkZF$;3XxH*uIW&QbtN4iF@5Gl0D)OA0+jmhXhHI3Q`U^$m^ksR6>rj zI{L{ZsU|g~mQ0a4GDGUgENLK(Bu1J@GYODs(n5lym9&v|5+WTWOd^ouYyCziuU0QmxYFu_<%G2QVP!hrwFY24N3;fEdrq{5U>`ne4a0u* zYK_4D3}}tQ{(jLKgUQ9U#$obFtqGDLS(wwbz}!5@KPWgXc$X=P1Re`FF*7g=Z4j6@9Ym!vI_0!h)LDA06) zKJ)@8Yi%slYi}gE$?n&8C{nU0)3&sA&_3CgMx&YG@XVQ^aq=O-$#+-Se}23o@QD+W z5JHe7JW)&{DnxQ~clFyJI9bBY9}h%{dp zZp*D7B0-dp%7Tr9NRI{a>qwM+JiWyGHpU!rkU1SP!EpTsF4=^ioS|yvFqE%k;FD9GMY};uy-g( z?L#|`E|(#Qf(351JdDtnr!X^Itxv0RT|^wA1`xG3^dXM*dnoUJP-dhh+#^0S18X!A zx_`}bd(u}4J074R@RglJdH@qa=nSmnv9t(sCx#VZBi2(O3(|x0X$z|$bYirye1@}+ z5oZx6LRAXcnhm7pRKt*`DWpihGyja~0J4L{Da;Ch z@4{}=kacMmxIGmh$1aO~@}74&UXliN?Q7R!(3mEHxY3uW$EH45BYaYDI%zuVTc$L)=U{>CZoKyLrgUo8aQ`>WmEBHzyfs4sZ-d0VLL6%VvDU3U=cA^Cdc z6qEjc1$9xhGytLzP^`RmzTIxupagV$s$W_i!d2bY?cIIf9t>B*aHNEo(DI3kwS3`l ztsSs>NJTWc6FO3XFJbe@nHA3Z=W{O4; z)A$(G$W2ruJ*n|X%!810^?X%SvHZvgwNns(9&WCG6YHQJorugp>TIl^sxcmG5z|Lc z>N_#eAae&AQv*A(+=WGF)VKz59gTwYzBWuI1QYwq^EN%kZ5q_WPU9f-BAhB}a=LC% z$)GhKrS|umWl=1j$JjY!uO3N1M3bCy+NKacoC}82co`11H06mx1@*u5;%;?xA1}1~)>|K0h zf!h4mUvP!aZ)NXu1aCE>R8MP6W*R>cMW#lVb^J3n9zcYWQymW=0d7zA0I{G(ntzd& z|7EXt;gFKcJG8+ltnbh)CVS%C#@kQC zR5t*-*=}yuyJZobdTF4nYD^DuBSa_fs3Vsltvu8j5$C4C(C9`%C^z=AK^7>3Zd+B(XCU14NUNX{aVoqnaNW$XTf7|5g!MI9OUS>umlK4AVp$ z4F{-*Ljyi^Gz3PTHu+zGv?TrDe%9@urkqUG{d1}g7p4w?m%B2IqK9r4Hh{*4ni#0# z+LsU$m3?!4^$$1=w335FVuwUx0f$6l0*6Fm1GhwC1YQsXGd40cm!@(A9|SWtGBvl! zas)sYQZh6)FhoH%Fhxa1G(%EwVxuiH8`7d#QJ) z$To3E9wdCDi%qhBObSRoBzmEXB2oy6?dx%ll#pUb;#Oy~WS97e7m|F{MS^UQGExdT zIMzi4DTf?B>(M1+#7`Q!nT2a93*Xjf!8Lckh?o+E9miJ0Ns|QvpuGI_c;aaN?w)6ib z{jk#ktpV7%Gp#|`Z&|G&*k2*7VVLy2)(Fheqt+-%kv*7`CxOYj@(V1>EghG;iUb}D OHaR#j3MC~)PeuxvBf4P# 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} 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} -- 2.1.4