(************** Content-type: application/mathematica ************** CreatedBy='Mathematica 5.0' Mathematica-Compatible Notebook This notebook can be used with any Mathematica-compatible application, such as Mathematica, MathReader or Publicon. The data for the notebook starts with the line containing stars above. To get the notebook into a Mathematica-compatible application, do one of the following: * Save the data starting with the line of stars above into a file with a name ending in .nb, then open the file inside the application; * Copy the data starting with the line of stars above to the clipboard, then use the Paste menu command inside the application. Data for notebooks contains only printable 7-bit ASCII and can be sent directly in email or through ftp in text mode. Newlines can be CR, LF or CRLF (Unix, Macintosh or MS-DOS style). NOTE: If you modify the data for this notebook not in a Mathematica- compatible application, you must delete the line below containing the word CacheID, otherwise Mathematica-compatible applications may try to use invalid cache data. For more information on notebooks and Mathematica-compatible applications, contact Wolfram Research: web: http://www.wolfram.com email: info@wolfram.com phone: +1-217-398-0700 (U.S.) Notebook reader applications are available free of charge from Wolfram Research. *******************************************************************) (*CacheID: 232*) (*NotebookFileLineBreakTest NotebookFileLineBreakTest*) (*NotebookOptionsPosition[ 226751, 5175]*) (*NotebookOutlinePosition[ 232875, 5390]*) (* CellTagsIndexPosition[ 232058, 5355]*) (*WindowFrame->Normal*) Notebook[{ Cell["\[Copyright] 2003 K. Sutner ", "SmallText"], Cell[CellGroupData[{ Cell["Induction", "Title", Evaluatable->False, AspectRatioFixed->True, CellTags->"c:1"], Cell[CellGroupData[{ Cell["Induction on Integers", "Section", Evaluatable->False, AspectRatioFixed->True, CellTags->"c:2"], Cell["\<\ In this section we take a closer look at induction on the \ non-negative integers; we wil generalize induction to other sets and data \ structures later (induction on list, on trees). \ \>", "Text"], Cell[CellGroupData[{ Cell[" The Principle of Induction", "Subsection", Evaluatable->False, AspectRatioFixed->True, CellTags->"c:3"], Cell[CellGroupData[{ Cell[" Plain Induction", "Subsubsection", Evaluatable->False, AspectRatioFixed->True, CellTags->"c:4"], Cell[TextData[{ "Suppose we have some property ", Cell[BoxData[ \(TraditionalForm\`\(\(P(n)\)\(\ \)\)\)]], " that may or may not hold for a natural number ", Cell[BoxData[ \(TraditionalForm\`n\)]], ". To demonstrate that ", Cell[BoxData[ \(TraditionalForm\`P(n)\)]], " is true for all ", Cell[BoxData[ \(TraditionalForm\`n\)]], " is a little problematic: there are infinitely many cases to consider. \ Even if we can provide proofs for ", Cell[BoxData[ \(TraditionalForm\`P(0), \ P(1), \ \(\(...\)\(,\)\(\ \)\(P(s)\)\)\)]], " where ", Cell[BoxData[ \(TraditionalForm\`s\)]], " is some large number, we have accomplished nothing (well, very little), \ since there are infinitely many other values left unchecked. However, there \ is a general method, the ", StyleBox["Principle of Mathematical Induction", FontColor->RGBColor[0, 0, 1]], ", that allows us to show that assertions hold for all natural numbers, by \ establishing only two facts.\n\n", StyleBox["Principle of Induction\n", FontColor->RGBColor[0, 0, 1]], "In order to show that ", Cell[BoxData[ \(TraditionalForm\`\[ForAll] \ n\ \(P(n)\)\)]], " holds, it suffices to establish the following two properties.\n\t (I1) \ ", StyleBox["Base case", FontColor->RGBColor[0, 0, 1]], ": Show that ", Cell[BoxData[ \(TraditionalForm\`P(0)\)]], " holds. \n\t (I2) ", StyleBox[" Induction step", FontColor->RGBColor[0, 0, 1]], ": Assume that ", Cell[BoxData[ \(TraditionalForm\`P(n)\)]], " holds, and show that ", Cell[BoxData[ \(TraditionalForm\`P(n + 1)\)]], " also holds. \nIn the induction step, the assumption that ", Cell[BoxData[ \(TraditionalForm\`P(n)\)]], " holds is called the ", StyleBox["Induction Hypothesis", FontColor->RGBColor[0, 0, 1]], " (IH). Note that the argument given there has to be perfectly general, it \ must hold for all ", Cell[BoxData[ \(TraditionalForm\`n\)]], ", not a just a few convenient values such as 1,2 or 3. \nIn more formal \ notation, we have to show\n\t", Cell[BoxData[ \(TraditionalForm\`P(0)\ \ \ \[And] \ \ \ \[ForAll] \ x\ \((\ \ \(P(x)\)\ \[DoubleLongRightArrow]\ \ \(P(x + 1)\))\)\)]], ".\nThis is method of proof is called ", StyleBox["Proof by (mathematical) Induction", FontColor->RGBColor[0, 0, 1]], ". " }], "Text", Evaluatable->False, AspectRatioFixed->True], Cell[TextData[{ "You can think of induction as a kind of ", StyleBox["recursive proof", FontColor->RGBColor[0, 0, 1]], ". We are supposed to come up with a proof for ", Cell[BoxData[ \(TraditionalForm\`P(n)\)]], ", for all ", Cell[BoxData[ \(TraditionalForm\`n\)]], ". Instead of attacking this problem directly, we only explain how to get \ a proof for ", Cell[BoxData[ \(TraditionalForm\`P(n)\)]], " out of a proof for ", Cell[BoxData[ \(TraditionalForm\`P(n - 1)\)]], ". And, we have a direct argument for ", Cell[BoxData[ \(TraditionalForm\`P(0)\)]], ". But that's really enough: we reduce ", Cell[BoxData[ \(TraditionalForm\`\(\(P(n)\)\(\ \)\)\)]], "to ", Cell[BoxData[ \(TraditionalForm\`P(n - 1)\)]], ", which reduces to ", Cell[BoxData[ \(TraditionalForm\`P(n - 2)\)]], ", and so forth, until we reach ", Cell[BoxData[ \(TraditionalForm\`P(0)\)]], ". " }], "Text", Evaluatable->False, AspectRatioFixed->True] }, Closed]], Cell[CellGroupData[{ Cell[" Soundness of Induction", "Subsubsection", Evaluatable->False, AspectRatioFixed->True, CellTags->"c:5"], Cell[TextData[{ "How do we know that this really works? How do we know that the principle \ of induction cannot be used to demonstrate false assertions? Here is an \ argument that may convince you that is in fact sufficient to establish (I1) \ and (I2) in order to demonstrate that a property ", Cell[BoxData[ \(TraditionalForm\`P(n)\)]], " holds for all n. \n\nFor the sake of a contradiction, suppose our method \ is not sound. So, for some assertion ", Cell[BoxData[ \(TraditionalForm\`P(n)\)]], ", we can establish the base case, and the induction step, but nonetheless \ it is not true that ", Cell[BoxData[ \(TraditionalForm\`P(n)\)]], " holds for all ", Cell[BoxData[ \(TraditionalForm\`n\)]], ". So, for some values of ", Cell[BoxData[ \(TraditionalForm\`n\)]], ", ", Cell[BoxData[ \(TraditionalForm\`P(n)\)]], " is false. Let ", Cell[BoxData[ \(TraditionalForm\`n\_0\)]], " be the least such ", Cell[BoxData[ \(TraditionalForm\`n\)]], ". Certainly, ", Cell[BoxData[ \(TraditionalForm\`n\_0\)]], " cannot be 0 by (I1). But if ", Cell[BoxData[ \(TraditionalForm\`n\_0\)]], " is larger than 0 it must have the form ", Cell[BoxData[ \(TraditionalForm\`n\_\(\(0\)\(\ \)\) = \ n\_1 + \ 1\)]], ", where ", Cell[BoxData[ \(TraditionalForm\`n\_1\ < \ n\_0\)]], ". Now, by our choice of ", Cell[BoxData[ \(TraditionalForm\`n\_0\)]], ", this means that ", Cell[BoxData[ \(TraditionalForm\`P(n\_1)\)]], " holds. But then by (I2), ", Cell[BoxData[ \(TraditionalForm\`P(n\_1 + \ 1)\)]], " also holds. But that is the same same as ", Cell[BoxData[ \(TraditionalForm\`P(n\_0)\)]], ", and we have a contradiction. \nThus, proof by induction works. " }], "Text", Evaluatable->False, AspectRatioFixed->True], Cell[TextData[{ "The perplexed reader may note that there is one crucial assumption in the \ last argument: if ", Cell[BoxData[ \(TraditionalForm\`P(n)\)]], " fails to hold for all ", Cell[BoxData[ \(TraditionalForm\`n\)]], ", then we can pick ", Cell[BoxData[ \(TraditionalForm\`n\_0\)]], " to be the least ", Cell[BoxData[ \(TraditionalForm\`n\)]], " where ", Cell[BoxData[ \(TraditionalForm\`P(n)\)]], " fails. This is called the ", StyleBox["Least Element Principle (LEP)", FontColor->RGBColor[0, 0, 1]], ", and may be no more obvious than Induction in the first place. Put \ differently, the LEP can be stated like so: \n\tEvery non-empty subset of the \ natural numbers must contain a least element. \nSo, we can either assume \ induction as a basic priciple, an axiom, or LEP. The latter implies the \ former. As we will see, induction can also be used to establish LEP, so the \ two axioms are equivaletn. Pick whichever one you prefer. " }], "Text", Evaluatable->False, AspectRatioFixed->True] }, Closed]], Cell[CellGroupData[{ Cell[" Some Comments", "Subsubsection", Evaluatable->False, AspectRatioFixed->True, CellTags->"c:6"], Cell[TextData[{ StyleBox["Comment 1:", FontWeight->"Bold"], " \nWe have chosen to describe the induction step as moving from ", Cell[BoxData[ \(TraditionalForm\`n\)]], " to ", Cell[BoxData[ \(TraditionalForm\`n + 1\)]], ", where ", Cell[BoxData[ \(TraditionalForm\`n\ \[GreaterEqual] \ 0\)]], ". There is the obvious alternative to change the induction step from ", Cell[BoxData[ \(TraditionalForm\`n - 1\)]], " to ", Cell[BoxData[ \(TraditionalForm\`n\)]], ", where ", Cell[BoxData[ \(TraditionalForm\`n\ > \ 0\)]], ". There is no difference whatsoever between the two methods, on occasion \ one yields slightly shorter expressions than the other, so it is a little \ easier to follow the argument. That's all. Of course, you can't mix and \ match, and move from ", Cell[BoxData[ \(TraditionalForm\`n - 1\)]], " to ", Cell[BoxData[ \(TraditionalForm\`n + 1\)]], ". \n\n", StyleBox["Comment 2:", FontWeight->"Bold"], " \nThere is nothing sacred about the base case ", Cell[BoxData[ \(TraditionalForm\`n = 0\)]], ", we could just as well start at ", Cell[BoxData[ \(TraditionalForm\`n\ = \ 17\)]], ". However, we would then only prove that assertion ", Cell[BoxData[ \(TraditionalForm\`P(n)\)]], " holds for all ", Cell[BoxData[ \(TraditionalForm\`n\ \[GreaterEqual] \ 17\)]], ". This makes no difference, since we can consider the property ", Cell[BoxData[ \(TraditionalForm\`\(Q(n)\)\ \ \[DoubleLongLeftRightArrow]\ \ \(P( n + 17)\)\)]], " and establish ", Cell[BoxData[ \(TraditionalForm\`\[ForAll] \ n\ \ \(Q(n)\)\)]], " by ordinary induction. That is the same as showing that ", Cell[BoxData[ \(TraditionalForm\`\[ForAll] \ n\ \[GreaterEqual] \ \ 17\ \(P(n)\)\)]], ". You will probably never have to start an induction at 17, but 0, 1, and \ even 2 are very popular starting points. \n\n", StyleBox["Comment 3:", FontWeight->"Bold"], " \nIt is often tempting to make additional assumptions about n when one \ tries to show that ", Cell[BoxData[ \(TraditionalForm\`P(n + 1)\)]], " holds, give ", Cell[BoxData[ \(TraditionalForm\`P(n)\)]], ". For example, the argumen might become easier for even ", Cell[BoxData[ \(TraditionalForm\`n\)]], ". Needless to say, this is not allowed. If you have a simple argument for \ even ", Cell[BoxData[ \(TraditionalForm\`n\)]], ", you have nonetheless to produce an argument for odd ", Cell[BoxData[ \(TraditionalForm\`n\)]], ", easy or not. \n\n", StyleBox["Comment 4", FontWeight->"Bold"], ": \nWe have already seen that the non-negative integers ", Cell[BoxData[ \(TraditionalForm\`\[DoubleStruckCapitalN]\ = \ {0, \ 1, \ \(\(...\)\(,\)\(\ \)\(n\)\), \ ... }\)]], " can be viewed as a recursively defined data structure: 0 is in ", Cell[BoxData[ \(TraditionalForm\`\[DoubleStruckCapitalN]\)]], ", and whenever n belongs to ", Cell[BoxData[ \(TraditionalForm\`\[DoubleStruckCapitalN]\)]], ", so does its successor ", Cell[BoxData[ \(TraditionalForm\`S(n)\)]], ", usually written ", Cell[BoxData[ \(TraditionalForm\`n + 1\)]], ". Correspondingly, we can define functions ", Cell[BoxData[ \(TraditionalForm\`f\)]], " by recursion on ", Cell[BoxData[ \(TraditionalForm\`\[DoubleStruckCapitalN]\)]], " as follows: \n\t(1) define ", Cell[BoxData[ \(TraditionalForm\`f(0)\)]], ",\n\t(2) define ", Cell[BoxData[ \(TraditionalForm\`f(n + 1)\)]], ", assuming that ", Cell[BoxData[ \(TraditionalForm\`f(n)\)]], " is already defined. \nThis is usually done in by specifying two \ equations such as \n\t", Cell[BoxData[ \(TraditionalForm\`f(0, x)\ = \ g(x)\)]], ",\n\t", Cell[BoxData[ \(TraditionalForm\`f(n + 1, x)\ = \ F(\ n, \ f(n, x), x)\)]], ".\nHere ", Cell[BoxData[ \(TraditionalForm\`g\ : \ \ \[DoubleStruckCapitalN]\ \[LongRightArrow]\ \ \[DoubleStruckCapitalN]\)]], " and ", Cell[BoxData[ \(TraditionalForm\`F\ : \ \[DoubleStruckCapitalN]\ \[Cross]\ \ \[DoubleStruckCapitalN]\ \[LongRightArrow]\ \[DoubleStruckCapitalN]\)]], " are given functions. \nProof by induction follows precisely this \ pattern, except that instead of defining a function value we establish an \ assertion. Indeed, one can show by induction that the two given equations \ uniquely define the function ", Cell[BoxData[ \(TraditionalForm\`f\)]], ". " }], "Text", Evaluatable->False, AspectRatioFixed->True] }, Closed]] }, Closed]], Cell[CellGroupData[{ Cell[" Little Gauss", "Subsection", Evaluatable->False, AspectRatioFixed->True, CellTags->"c:7"], Cell[TextData[{ "While ", StyleBox["C. F. Gauss (1777-1855)", FontColor->RGBColor[0, 0, 1]], " was attending grammar school, his math teacher decided that it was \ preferable to read the newspaper, rather than teach arithmetic. So, he posed \ the following problem to the students: \n Sum up the integers from 1 \ to 5000, and submit the result. \nPaper was too expensive in those days, so \ the kids had little slate boards to write on. According to one version of \ the story, no sooner had the teacher setteld down into a comfortable position \ that young Gauss got up and tossed his slate board on the teacher's desk, \ contemptuously announcing: \"There it is.\" \nHow did he do it? Think \ average. " }], "Text", Evaluatable->False, AspectRatioFixed->True], Cell[TextData[{ "Summing the first ", Cell[BoxData[ \(TraditionalForm\`n\)]], " integers is inevitably the first example for a proof by induction. We \ want to show that \n\n ", Cell[BoxData[ \(TraditionalForm\`\(\(\ \)\(\[Sum]\_\(i = 1\)\%n\ i\ = \ \(\(1\ + \ 2\ + \ ... \)\ + \ \((n - 1)\)\ + \ n\ = \ \(n\ \((n\ + \ 1)\)\)\/2\)\)\)\)]], StyleBox[",\n ", FontWeight->"Bold"], "\nfor all ", Cell[BoxData[ \(TraditionalForm\`\(\(\ \)\(n\ \[GreaterEqual] \ 0\)\)\)]], ". This looks reasonable, since there are ", Cell[BoxData[ \(TraditionalForm\`n\)]], " terms, and the average is clearly (!) ", Cell[BoxData[ \(TraditionalForm\`\(n + 1\)\/2\)]], ". So, in this case, our assertion ", Cell[BoxData[ \(TraditionalForm\`P(n)\)]], " is precisely this equation, one of the many summation formulae in \ arithmetic. \n\nJust to reassure ourselves, let us use ", StyleBox["Mathematica", FontSlant->"Italic"], " to determine the sum." }], "Text", Evaluatable->False, AspectRatioFixed->True], Cell[BoxData[ \(\[Sum]\+\(i = 1\)\%n i\)], "Input"], Cell[TextData[{ "Looks good, now for the proof. \n\n", StyleBox["Lemma", FontWeight->"Bold"], ": ", StyleBox[" ", FontWeight->"Bold"], Cell[BoxData[ \(TraditionalForm\`\[Sum]\_\(i = 1\)\%n\ i\ \ = \ \(n\ \((n\ + \ 1)\)\)\/2\)]], "\nProof: \nWe can prove this summation formula by induction on n. \nBase \ case: ", Cell[BoxData[ \(TraditionalForm\`P(0)\)]], " holds, since both the left and the right side evaluate to 0: \n", Cell[BoxData[ \(TraditionalForm\`\[Sum]\_\(i = 1\)\%0\ i\ \ = \(0\ = \ \ \(0\ \((0 + \ 1)\)\)\/2\)\)]], ". \nInduction step: Suppose ", Cell[BoxData[ \(TraditionalForm\`P(n)\)]], " holds, so ", Cell[BoxData[ \(TraditionalForm\`\[Sum]\_\(i = 1\)\%n\ i\ \ = \ \(n\ \((n\ + \ 1)\)\)\/2\)]], ". \nThen \n\t", Cell[BoxData[ \(TraditionalForm\`\(\(\[Sum]\_\(i = 1\)\%\(n + 1\)\ i\)\(\ \ \)\(=\)\(\ \)\(\[Sum]\_\(i = 1\)\%n\ i\ \ + \ \((n + 1)\)\ = \ \(\(n\ \((n\ + \ 1)\)\)\/2\ + \ \((n + 1)\)\ = \ \ \(\((n\ \ + \ 2)\)\ \((n\ + \ \ 1)\)\)\/2\)\)\(\ \)\)\)]], " \n\[EmptySquare] \n\nAs you can see in this argument, it is a good \ idea to indicate exactly where the IH was used. The reader is expected to \ figure out the other manipulations on her own." }], "Text", Evaluatable->False, AspectRatioFixed->True], Cell[TextData[{ "Note that the only properties of summation we needed are:\n\t ", Cell[BoxData[ \(TraditionalForm\`\[Sum]\_\(i = 1\)\%0 f(i)\ \ = \ 0\)]], ",\n\t ", Cell[BoxData[ \(TraditionalForm\`\[Sum]\_\(i = 1\)\%\(n + 1\)\ f(i)\ \ = \ \[Sum]\_\(i = 1\)\%n\ f(i)\ + \ f(n + 1)\)]], "." }], "Text", Evaluatable->False, AspectRatioFixed->True] }, Closed]], Cell[CellGroupData[{ Cell[" Summing the first n squares", "Subsection", Evaluatable->False, AspectRatioFixed->True, CellTags->"c:8"], Cell[TextData[{ "To get ahead of little Gauss, here is a slightly more complicated example \ for a proof by induction. We want to show that \n\n \ ", Cell[BoxData[ \(TraditionalForm\`\(1\^2\ + \ 2\^2\ + \ ... \)\ + \ n\^2\ = \ \(n(n\ + \ 1)\) \((2 n + 1)\)/6\)]], StyleBox[",\n ", FontWeight->"Bold"], "\nfor all ", Cell[BoxData[ \(TraditionalForm\`n\ \[GreaterEqual] \ 0\)]], ". The right hand side is more complicated, and it is more difficult to \ come up with the right guess, but once we know what we are trying to prove, \ the argument is almost verbatim the same as in the first example. \n\n", StyleBox["Lemma", FontWeight->"Bold"], ": For all ", Cell[BoxData[ \(TraditionalForm\`n\ \[GreaterEqual] \ 0\)]], ": ", StyleBox[" ", FontWeight->"Bold"], Cell[BoxData[ \(TraditionalForm\`\(\(\ \ \)\(\[Sum]\_\(i = 1\)\%n\ i\^2\ = \ \(n(n + 1)\) \((2 n + 1)\)/6\)\)\)]], ". \n\nProof: \nWe can prove this summation formula by induction on ", Cell[BoxData[ \(TraditionalForm\`n\)]], ". \nBase case: ", Cell[BoxData[ \(TraditionalForm\`P(0)\)]], " holds, since both the left and the right side evaluate to 0: \n\t", Cell[BoxData[ \(TraditionalForm\`\[Sum]\_\(i = 1\)\%0\ i\^2\ = \ \(0\ = \ 0 \((0 + 1)\) \((2\[CenterDot]0 + 1)\)/6\)\)]], "\nInduction step: Suppose ", Cell[BoxData[ \(TraditionalForm\`P(n)\)]], " holds, so ", Cell[BoxData[ \(TraditionalForm\`\[Sum]\_\(i = 1\)\%n\ i\^2\ = \ \(n(n + 1)\) \((2 n + 1)\)/6\)]], ". Then \n\t", Cell[BoxData[ \(TraditionalForm\`\(\(\[Sum]\_\(i = 1\)\%\(n + 1\)\ i\^2\)\(\ \)\(=\)\(\(\[Sum]\_\(i = 1\)\%n\ i\^2\ + \ \((n + 1)\)\^\(\(2\)\(\ \)\)\)\(=\)\)\(\ \)\)\)]], "\n\t", Cell[BoxData[ \(TraditionalForm\`\(\(\(n(n + 1)\) \((2 n + 1)\)/ 6\ + \ \((n + 1)\)\^2\)\(=\)\)\)]], "\n\t", Cell[BoxData[ \(TraditionalForm\`\(\(\((n + 1)\) \((\ \(n(2 n + 1)\)/ 6\ + \ \((n + 1)\)\ )\)\)\(\ \)\(=\)\)\)]], "\n\t", Cell[BoxData[ \(TraditionalForm\`\(\(\ \)\(\((n + 1)\) \((n + 2)\) \((2 \((n + 1)\) + 1)\)/6\)\)\)]], ",\nand we are done.\n\[EmptySquare]\n\nNeedless to say, this is just the \ tip of an iceberg: we can produce similar arguments for ", Cell[BoxData[ \(TraditionalForm\`\(\(\ \)\(\[Sum]\_\(i = 1\)\%n\ i\^\(\(\(\ \)\(k\)\)\(\ \)\)\)\)\)]], " for any integer exponent ", Cell[BoxData[ \(TraditionalForm\`\(\(\ \)\(k\ \[GreaterEqual] \ 0\)\)\)]], ". Summation of this form are encountered in the analysis of algorithms \ when one tries to determine the running time of programs containing nested \ loops. \nOf course, the hard part is to figure out what to prove. For \ example, it is far from clear what ", Cell[BoxData[ \(TraditionalForm\`\[Sum]\_\(i = 1\)\%n\ i\^\(\(\ \)\(5\)\)\)]], " would be. But once the right expression for the right hand side has \ been found, the argument always follows the pattern of the case ", Cell[BoxData[ \(TraditionalForm\`k = 1\)]], " and ", Cell[BoxData[ \(TraditionalForm\`k = 2\)]], ", and is essentially no more complicated. " }], "Text", Evaluatable->False, AspectRatioFixed->True] }, Closed]], Cell[CellGroupData[{ Cell[" Using Mathematica to help with the proof", "Subsection", Evaluatable->False, AspectRatioFixed->True, CellTags->"c:9"], Cell["\<\ In fact, in the presence of a computer algebra system we can \ mechanize the proof of summation formulae and other similar problems almost \ completely. More precisely, the induction arguments for the fist two \ summation formulae \[Bullet] both follow precisely the same logical pattern, and \[Bullet] involve a little bit of arithmetic, some manipulation of sums and \ some simplifications. Therefore, it is perhaps not too surprising that one can abuse Mathematica to \ do all the arithmetic, and basically take care of the whole proof. Make sure \ you understand what is going on. \ \>", "Text", Evaluatable->False, AspectRatioFixed->True], Cell[CellGroupData[{ Cell[" Sums of Integers, again", "Subsubsection", Evaluatable->False, AspectRatioFixed->True, CellTags->"c:10"], Cell["\<\ Here is a semi-automatic proof of our first summation formula. \ \>", "Text", Evaluatable->False, AspectRatioFixed->True], Cell[TextData[{ StyleBox["Lemma: ", FontFamily->"Times", FontWeight->"Bold"], StyleBox[" ", FontWeight->"Bold"], Cell[BoxData[ \(TraditionalForm\`\[Sum]\_\(i = 1\)\%n\ i\ \ = \ \(n\ \((n\ + \ 1)\)\)\/2\)]], StyleBox[" . ", FontFamily->"Times", FontWeight->"Bold"] }], "Text", Evaluatable->False, AspectRatioFixed->True], Cell[TextData[{ "Proof:\nFirst, we introduce functions ", Cell[BoxData[ \(TraditionalForm\`L\)]], " and ", Cell[BoxData[ \(TraditionalForm\`R\)]], " for the left and right hand side. " }], "Text", Evaluatable->False, AspectRatioFixed->True], Cell[BoxData[{ \(Clear[L, R, n]\), "\n", \(\(L[n_] := \[Sum]\+\(i = 1\)\%n i;\)\), "\n", \(\(R[n_] := 1\/2\ n\ \((n + 1)\);\)\)}], "Input", AspectRatioFixed->True], Cell[TextData[{ "So, we have to show that ", Cell[BoxData[ \(TraditionalForm\`L(n)\ = \ R(n)\)]], " for all ", Cell[BoxData[ \(TraditionalForm\`n\ \[GreaterEqual] \ 0\)]], ". \n\nBase Case: \nWe have to make sure that ", Cell[BoxData[ FormBox[ RowBox[{" ", FormBox[\(L(0)\ = \ R(0)\), "TraditionalForm"], " "}], TraditionalForm]]], ". Mathematica can check this equation:" }], "Text", Evaluatable->False, AspectRatioFixed->True], Cell[BoxData[ \(L[0] == R[0]\)], "Input", AspectRatioFixed->True], Cell[TextData[{ "Induction Step:\nFor the induction step we have to show \n\t", Cell[BoxData[ \(TraditionalForm\`L(n + 1)\ = \ R(n + 1)\)]], " assuming that already ", Cell[BoxData[ \(TraditionalForm\`L(n)\ = \ R(n)\)]], ". \nSince ", Cell[BoxData[ \(TraditionalForm\`L\)]], " is a sum, we have ", Cell[BoxData[ \(TraditionalForm\`L(n + 1)\ = \ L(n)\ + \ n + 1\)]], ". Hence, b", StyleBox["y", FontWeight->"Bold"], " the Induction Hypothesis ", Cell[BoxData[ \(TraditionalForm\`L(n + 1)\ = \ R(n)\ + \ n + 1\)]], ". Therefore, we only have to show that\n\t\t ", Cell[BoxData[ \(TraditionalForm\`R(n + 1)\ = \ R(n)\ + \ n + 1\)]], ",\nor, equivalently, \n\t\t ", Cell[BoxData[ \(TraditionalForm\`R(n + 1)\ - \ R(n)\ = \ n + 1\)]], ".\nThe latter form is often easier to digest for a computer algebra \ system. Here we go:\n" }], "Text", Evaluatable->False, AspectRatioFixed->True], Cell[BoxData[{ \(R[n + 1] - R[n]\), "\n", \(Simplify[%]\)}], "Input", AspectRatioFixed->True], Cell[TextData[{ "Done. Note that it is crucial here that ", Cell[BoxData[ \(TraditionalForm\`n\)]], " is a free variable. If ", Cell[BoxData[ \(TraditionalForm\`n\)]], " were bound to a value, the argument would be totally useless. \n\ \[EmptySquare]" }], "Text", Evaluatable->False, AspectRatioFixed->True], Cell[TextData[{ "If we were dealing with a more general sum of the form ", Cell[BoxData[ \(TraditionalForm\`L( n)\ \ = \ \(\(\[Sum]\_\(i\ \[LessEqual] \ n\)\)\(\ \)\(f( i)\)\(\ \)\)\)]], " we would have to veryify that \t\t \t", Cell[BoxData[ \(TraditionalForm\`R(n + 1)\ - \ R(n)\ = \ f(n + 1)\)]], ".\nFor example, here is the same process for sums of squares. " }], "Text"], Cell[BoxData[{ \(Clear[f, L, R, n]\), "\n", \(\(f[n_]\ := \ n\^2;\)\), "\n", \(\(L[n_] := \[Sum]\+\(i = 1\)\%n f[i];\)\), "\n", \(\(R[n_] := 1\/6\ n\ \((n + 1)\)\ \((2\ n + 1)\);\)\)}], "Input", AspectRatioFixed->True], Cell["Base:", "Text"], Cell[BoxData[ \(L[0] == R[0]\)], "Input", AspectRatioFixed->True], Cell["Induction Step:", "Text", Evaluatable->False, AspectRatioFixed->True], Cell[BoxData[{ \(R[n + 1] - R[n]\), "\n", \(Simplify[%]\)}], "Input", AspectRatioFixed->True], Cell[TextData[{ "\nPiece of cake! We can prove any of these power sum formulae, provided \ someone is kind enough to figure out the right hand side. As it turns out, ", StyleBox["Mathematica", FontSlant->"Italic"], " is able to produce closed form descriptions:" }], "Text", Evaluatable->False, AspectRatioFixed->True], Cell[BoxData[ \(\[Sum]\_\(i = 1\)\%n i\^5\)], "Input"], Cell[TextData[{ "We can verify by induction that the answer is correct (assuming that the \ arithmetic simplification routines in ", StyleBox["Mathematica", FontSlant->"Italic"], " work properly)." }], "Text"], Cell[BoxData[{ \(\(R[n_]\ := \ Evaluate[%];\)\), "\n", \(\(L[n_]\ := \ \[Sum]\_\(i = 1\)\%n i\^5;\)\)}], "Input"], Cell[BoxData[ \(R[n + 1]\ - \ R[n]\ // \ Simplify\)], "Input"] }, Closed]] }, Closed]], Cell[CellGroupData[{ Cell[" Summation Formulae: Numerical Estimates", "Subsection", Evaluatable->False, AspectRatioFixed->True, CellTags->"c:11"], Cell[TextData[{ "In practice, the hard part is often to figure out what to prove in the \ first place. In the sum-of-squares and sum-of-cubes example, where do the \ right hand sides come from when one does not have access to the complicated \ algorithms in a computer algebra system? \nFor simple summation problems, the \ following section shows how to derive the right formula as a conjecture, and \ then to prove the conjecture by induction (by hand, or using Mathematica). \n\ As in our automatic proofs, define a function ", Cell[BoxData[ \(TraditionalForm\`L\)]], " for the left hand side. Let's look at some values of ", Cell[BoxData[ \(TraditionalForm\`L\)]], "." }], "Text", Evaluatable->False, AspectRatioFixed->True], Cell[BoxData[{ \(Clear[f, ff, g, i]\), "\n", \(L[n_Integer] := \[Sum]\+\(i = 1\)\%n i\), "\n", \(\(tab = L /@ Range[100];\)\)}], "Input", AspectRatioFixed->True], Cell[BoxData[ \(\(ListPlot[tab, PlotStyle -> Blue];\)\)], "Input", AspectRatioFixed->True], Cell["\<\ Looks vaguely like a parabola. So, as a very first approach, let us \ try to fit a quadratic curve to the data points. Fitting curves to given \ data is one of the most standard things to do in empirical sciences, so of \ course it's built in. \ \>", "Text", Evaluatable->False, AspectRatioFixed->True], Cell[BoxData[ \(Information[Fit, LongForm \[Rule] False]\)], "Input", AspectRatioFixed->True], Cell[TextData[{ "Let's use 10 data points, and the functions ", Cell[BoxData[ \(TraditionalForm\`{1, \ x, \ x\^2}\)]], " to fit the curve. " }], "Text", Evaluatable->False, AspectRatioFixed->True], Cell[BoxData[ \(data = Take[tab, 10]\)], "Input", AspectRatioFixed->True], Cell[BoxData[ \(Fit[data, {1, x, x\^2}, x]\)], "Input", AspectRatioFixed->True], Cell[TextData[{ "Note that ", StyleBox["Fit", "SmallText"], " automatically uses approximate reals to do the curve fitting. Clearly, \ the first term should be 0, and the others are just 1/2. " }], "Text", Evaluatable->False, AspectRatioFixed->True], Cell[BoxData[ \(Chop[%]\)], "Input", AspectRatioFixed->True], Cell[TextData[{ "To see that the correct solution is in fact ", Cell[BoxData[ \(TraditionalForm\`\(n(n + 1)\)/2\)]], " in precise rational numbers, we set up a system of equations and solve \ it (symbolically, no round-off error here). " }], "Text", Evaluatable->False, AspectRatioFixed->True], Cell[BoxData[ \(\(coeffs = {c\_0, c\_1, c\_2};\)\)], "Input", AspectRatioFixed->True], Cell[BoxData[{ \(Clear[LL]\), "\n", \(\(LL[x_] := c\_2\ x\^2 + c\_1\ x + \ c\_0;\)\)}], "Input", AspectRatioFixed->True], Cell[TextData[{ "The equations are of the form ", Cell[BoxData[ \(TraditionalForm\`L(n)\ = \ LL(n)\)]], ", and we can choose ", Cell[BoxData[ \(TraditionalForm\`n\)]], " any which way we like. For example, for ", Cell[BoxData[ \(TraditionalForm\`\(\(n\ = \ 1\)\(,\)\(\ \)\(10\)\(,\)\(\ \)\(15\)\(\ \)\)\)]], "we get:" }], "Text", Evaluatable->False, AspectRatioFixed->True], Cell[BoxData[{ \(\(eqn = {L[1] == LL[1], L[10] == LL[10], L[15] == LL[15]};\)\), "\n", \(TableForm[eqn]\)}], "Input", AspectRatioFixed->True], Cell["Now we can solve:", "Text", Evaluatable->False, AspectRatioFixed->True], Cell[BoxData[ \(sol = Solve[eqn, coeffs]\)], "Input", AspectRatioFixed->True], Cell[TextData[{ StyleBox["Mathematica", FontSlant->"Italic"], " returns the solution as a set of rules: variable -> value. Since \ the solution is unique in this case there is only one triple of rules. If we \ apply these rules to the variables we get the values." }], "Text", Evaluatable->False, AspectRatioFixed->True], Cell[BoxData[ \(coeffs /. sol\[LeftDoubleBracket]1\[RightDoubleBracket]\)], "Input", AspectRatioFixed->True], Cell["So we get the right hand side:", "Text", Evaluatable->False, AspectRatioFixed->True], Cell[BoxData[{ \(LL[n] /. sol\[LeftDoubleBracket]1\[RightDoubleBracket]\), "\n", \(Factor[%]\)}], "Input", AspectRatioFixed->True], Cell["Exactly the right expression for the proof. ", "Text", Evaluatable->False, AspectRatioFixed->True] }, Closed]], Cell[CellGroupData[{ Cell[" An ATM Machine", "Subsection", Evaluatable->False, AspectRatioFixed->True, CellTags->"c:12"], Cell[TextData[{ "Suppose an ATM machine has only two dollar and five dollar bills. You can \ type in the amount you want, and it will figure out how to divide things up \ into the proper number of two's and five's. \n\n", StyleBox["Claim", FontWeight->"Bold"], ": The ATM can generate any output amount ", Cell[BoxData[ \(TraditionalForm\`n\ \[GreaterEqual] \ 4\)]], ". \n\nProof:\nBy induction on ", Cell[BoxData[ \(TraditionalForm\`n\)]], ". \nBase case: ", Cell[BoxData[ \(TraditionalForm\`n = 4\)]], ". 2 two's, done.\n\nInduction step: suppose the machine can already \ handle ", Cell[BoxData[ \(TraditionalForm\`n \[GreaterEqual] 4\)]], " dollars. \nTo produce ", Cell[BoxData[ \(TraditionalForm\`n + 1\)]], " dollars, we proceed as follows.\n\nCase 1: The ", Cell[BoxData[ \(TraditionalForm\`n\)]], " dollar output contains a five. \nThen we can replace the five by 3 two's \ to get ", Cell[BoxData[ \(TraditionalForm\`n + 1\)]], " dollars.\n\nCase 2: The ", Cell[BoxData[ \(TraditionalForm\`n\)]], " dollar output contains only two's. \nSince ", Cell[BoxData[ \(TraditionalForm\`n \[GreaterEqual] 4\)]], ", there must be at least 2 two's. Remove 2, and replace them by 1 five. \ Done. \nQED\n\nNote that the proof actually produces an algorithm, you can \ write a program that on input n will determine how many two's and five's the \ machine is supposed to emit. \n\nHere is the algorithm that is implicit in \ the proof. We return ", Cell[BoxData[ \(TraditionalForm\`{p, q}\)]], " to indicate that the machine will output ", Cell[BoxData[ \(TraditionalForm\`p\)]], " two's and ", Cell[BoxData[ \(TraditionalForm\`q\)]], " five's. \n" }], "Text", Evaluatable->False, AspectRatioFixed->True], Cell[BoxData[{ \(atm[4] = {2, 0}; \), "\n", \(\(atm[ n_Integer] := \[IndentingNewLine]Module[{p, q}, \[IndentingNewLine]{p, q} = atm[n - 1]; \[IndentingNewLine]If[ q > 0, {p + 3, q - 1}, {p - 2, q + 1}]\[IndentingNewLine]];\)\)}], "Input", AspectRatioFixed->True], Cell["\<\ TableForm[ ({#,atm[#]}&) /@ Range[4,20], TableDepth\[Rule]2 ]\ \>", \ "Input", AspectRatioFixed->True], Cell["\<\ Can you see a pattern in this output? Use it to give a direct \ proof of the claim, without induction. Then try to come up with a similar argument for a machine that has three's \ (three dollar bills, to be introduced by President Dole to wipe out the \ deficit and fight crime) and five's. \ \>", "Text", Evaluatable->False, AspectRatioFixed->True] }, Closed]], Cell[CellGroupData[{ Cell[" Some Inequalities", "Subsection", Evaluatable->False, AspectRatioFixed->True, CellTags->"c:13"], Cell["\<\ So far, we have only established equations by induction. Here are \ two inequalities that can be proven by induction. Note, though, that automating a proof that deals with inequalities rather \ than equations is quite a bit harder. Mathematica is of little or no use \ here, you have to argue by hand. \ \>", "Text", Evaluatable->False, AspectRatioFixed->True], Cell[CellGroupData[{ Cell[TextData[{ " A Lower Bound for ", Cell[BoxData[ \(TraditionalForm\`\((1 + x)\)\^\(\(\ \)\(n\)\)\)]] }], "Subsubsection", Evaluatable->False, AspectRatioFixed->True, CellTags->"c:14"], Cell[TextData[{ "The following is a type of lower bound that one finds frequently in \ calculus. \n\n", StyleBox["Claim:", FontWeight->"Bold"], " For all positive integers ", Cell[BoxData[ \(TraditionalForm\`n\)]], " and all positive reals ", Cell[BoxData[ \(TraditionalForm\`x\)]], StyleBox[": ", FontWeight->"Bold"], Cell[BoxData[ \(TraditionalForm\`1\ + \ n\ x\ \[LessEqual] \ \((1 + x)\)\^\(\(\ \)\(n\)\)\)]], ".", StyleBox["\n", FontWeight->"Bold"], "\nLet's look at plots for some values of ", Cell[BoxData[ \(TraditionalForm\`n\)]], " first to get some evidence that the claim is actually correct. " }], "Text", Evaluatable->False, AspectRatioFixed->True], Cell[BoxData[{ \(Clear[f, g, n, x]\), "\n", \(\(f[x_] := \((1 + x)\)\^n;\)\), "\n", \(\(g[x_] := 1 + n\ x;\)\)}], "Input", AspectRatioFixed->True], Cell["\<\ Execute the next cell and click on the bracket. Then press alt-Y \ and the sequence of plots will be animated. You can use the control buttons \ in the lower left hand corner to manipulate the movie. \ \>", "Text", Evaluatable->False, AspectRatioFixed->True], Cell[BoxData[ \(Do[Plot[{f[x], g[x]}, {x, \(- .9\), 4}, PlotRange \[Rule] {{\(-1\), 5}, {\(-10\), 100}}, PlotStyle \[Rule] {Red, Blue}], {n, 5}]\)], "Input", AspectRatioFixed->True], Cell[TextData[{ "It appears that ", Cell[BoxData[ \(TraditionalForm\`f\)]], " is always larger than ", Cell[BoxData[ \(TraditionalForm\`g\)]], ". Of course, these pictures prove nothing. Here is the real argument. \n\n\ Proof:\nWe proceed by induction on ", Cell[BoxData[ \(TraditionalForm\`n\)]], ". \n\nBase case: ", Cell[BoxData[ \(TraditionalForm\`n = 0\)]], " yields ", Cell[BoxData[ \(TraditionalForm\`1\ + \ 0\ x\ = \ \(1\ = \ \((1\ + \ x)\)\^0\)\)]], ", so for ", Cell[BoxData[ \(TraditionalForm\`n = 0\)]], " we even have equality. \n\nInduction step: \nSuppose ", Cell[BoxData[ \(TraditionalForm\`1\ + \ n\ x\ \[LessEqual] \ \((1 + x)\)\^\(\(\ \)\(n\)\)\)]], ". Then \n", Cell[BoxData[ \(TraditionalForm\`1\ + \ \((n + 1)\)\ x\ = \ \(1\ + \ n\ x\ + \ x\ \[LessEqual] \ \((1 + x)\)\^\(\(\ \)\(n\)\)\ + \ x\ \[LessEqual] \ \((1 + x)\)\^\(\(\ \)\(n\)\) + \ x\ \((1 + x)\)\^\(\(\ \)\(n\)\(\ \)\) = \ \((1 + x)\)\^\(\(\ \)\ \(n + 1\)\)\)\)]], ".\nQED " }], "Text", Evaluatable->False, AspectRatioFixed->True] }, Closed]], Cell[CellGroupData[{ Cell[" Pinning Down Fibonacci Numbers", "Subsubsection", Evaluatable->False, AspectRatioFixed->True, CellTags->"c:15"], Cell[TextData[{ "Fibonacci numbers clearly grow very rapidly. A crude upper bound for ", Cell[BoxData[ \(TraditionalForm\`F\_n\)]], " would be ", Cell[BoxData[ \(TraditionalForm\`2\^\(\(\ \)\(n\)\)\)]], " (strightforward by induction). Here is a better bound. Let ", StyleBox[" ", FontWeight->"Bold"], Cell[BoxData[ \(TraditionalForm\`\[CurlyPhi]\)]], " denote the ", StyleBox["Golden Ratio", FontColor->RGBColor[0, 0, 1]], ", the number ", Cell[BoxData[ \(TraditionalForm\`\((1\ + \ \@5)\)/2\)]], ". This number is the positive root of the equation ", Cell[BoxData[ \(TraditionalForm\`\(\(\ \)\(x\^2\ = \ x\ + \ 1\)\)\)]], " and was considered to represent particularly harmonious proportions (a \ rectangle with sides 1 and Golden Ratio has the same proportions as the \ rectangle obtained from it by removing a unit square, see the fabulous \ graphics below). The Golden Ratio is a built-in constant in Mathematica. " }], "Text", Evaluatable->False, AspectRatioFixed->True], Cell[BoxData[{ \(N[GoldenRatio]\), "\n", \(N[1\/\(GoldenRatio - 1\)]\)}], "Input", AspectRatioFixed->True], Cell[TextData[{ "And ", StyleBox["Mathematica", FontSlant->"Italic"], " can even figure out the basic relation between these symbolic terms, with \ a bit of effort." }], "Text"], Cell[BoxData[ \(GoldenRatio\ == \ 1/\((GoldenRatio - 1)\)\ // \ FullSimplify\)], "Input"], Cell[BoxData[ \(Solve[x\^2 == x + 1, x]\)], "Input", AspectRatioFixed->True], Cell[BoxData[ \(\(Show[ Graphics[{{Gold, Rectangle[{0, 0}, {GoldenRatio, 1}]}, {Cyan, Rectangle[{0, 0}, {1, 1}]}, {Red, Rectangle[{1, 0}, {GoldenRatio, GoldenRatio - 1}]}, Line[{{0, 0}, {GoldenRatio, 1}}]}], AspectRatio \[Rule] Automatic, Frame \[Rule] True, FrameTicks \[Rule] None];\)\)], "Input", AspectRatioFixed->True], Cell["\<\ And, the inverse of GoldenRatio is used as the default aspect ratio \ in plotting commands. \ \>", "Text", Evaluatable->False, AspectRatioFixed->True], Cell[BoxData[ \(First[Options[Plot]]\)], "Input", AspectRatioFixed->True], Cell[TextData[{ "At any rate, here is a connection between the Golden Ratio and Fibonacci \ numbers. \n\n", StyleBox["Claim:", FontWeight->"Bold"], " For all integers ", Cell[BoxData[ \(TraditionalForm\`n\ \[GreaterEqual] \ 2\)]], ": ", Cell[BoxData[ \(TraditionalForm\`\[CurlyPhi]\^\(\(\ \)\(n - 2\)\) \[LessEqual] \ F\_n \[LessEqual] \ \[CurlyPhi]\^\(\(\ \)\(n\)\)\)]], ".", StyleBox["\n", FontWeight->"Bold"], "\nThus, the sequence ", Cell[BoxData[ \(TraditionalForm\`F\_n\)]], " grows essentially just like the exponential function ", Cell[BoxData[ \(TraditionalForm\`\[CurlyPhi]\^\(\(\ \)\(n\)\)\)]], ". Here is a computational check for the upper bound, and a lovely \ Mathematica hack to compare lists pointwise. Make sure to also check the \ lower bound. " }], "Text", Evaluatable->False, AspectRatioFixed->True], Cell[BoxData[{ \(Fibonacci[Range[20]]\), "\n", \(N[GoldenRatio]\^Range[20]\), "\n", \(Thread[%% < %]\)}], "Input", AspectRatioFixed->True], Cell[TextData[{ "\nProof: \nWe only prove the upper bound, the argument for the lower \ bound is almost verbatim the same. The upper bound actually holds for all ", Cell[BoxData[ \(TraditionalForm\`n\ \[GreaterEqual] \ 0\)]], ". Since we need two previous values to compute the next Fibonacci number, \ we need a slightly stronger base case than usual. More precisely, we will \ establish the property \n\t", Cell[BoxData[ \(TraditionalForm\`P(n)\)]], ": ", Cell[BoxData[ \(TraditionalForm\`F\_n \[LessEqual] \ \[CurlyPhi]\^\(\(\ \ \)\(n\)\)\)]], " and ", Cell[BoxData[ \(TraditionalForm\`F\_\(n + 1\) \[LessEqual] \ \[CurlyPhi]\^\(n + \ 1\)\)]], ". \n for all ", Cell[BoxData[ \(TraditionalForm\`n\ \[GreaterEqual] \ 0\)]], ", rather than the more obvious ", Cell[BoxData[ \(TraditionalForm\`P(n)\)]], ": ", Cell[BoxData[ \(TraditionalForm\`F\_n \[LessEqual] \ \[CurlyPhi]\^\(\(\ \ \)\(n\)\)\)]], " .\nBase case: ", Cell[BoxData[ \(TraditionalForm\`n = 0\)]], ". \nWe have ", Cell[BoxData[ \(TraditionalForm\`F\_0 = \ \(0\ < \ 1\ = \ \[CurlyPhi]\^0\)\)]], " and ", Cell[BoxData[ \(TraditionalForm\`F\_1 = \ \(1\ < \ \[CurlyPhi]\ = \ \ \[CurlyPhi]\^1\)\)]], ".\nInduction step: Assume ", Cell[BoxData[ \(TraditionalForm\`P(n)\)]], " holds, ", Cell[BoxData[ \(TraditionalForm\`n \[GreaterEqual] 0\)]], ". To establish ", Cell[BoxData[ \(TraditionalForm\`P(n + 1)\)]], " we only have to show that ", Cell[BoxData[ \(TraditionalForm\`F\_\(n + 2\)\ \[LessEqual] \ \[CurlyPhi]\^\(\(\ \ \)\(n + 2\)\)\)]], " (why?). \n\t", Cell[BoxData[ \(TraditionalForm\`F\_\(n + 2\) = \ \(F\_\(n + 1\) + \ F\_n\ \[LessEqual] \ \[CurlyPhi]\^\(\(\ \)\(n + 1\)\) + \ \ \[CurlyPhi]\^\(\(\ \)\(n\)\) = \ \(\(\[CurlyPhi]\^\(\(\ \)\(n\)\)\)(\ 1\ + \ \[CurlyPhi])\ = \ \(\(\[CurlyPhi]\^\(\(\ \)\(n\)\)\) \ \[CurlyPhi]\^\(\(\ \)\(2\)\) = \ \[CurlyPhi]\^\(\(\ \)\(n + 2\)\)\)\)\)\)]], ". \nQED " }], "Text", Evaluatable->False, AspectRatioFixed->True], Cell[TextData[{ "Make sure you understand why the simple version of ", Cell[BoxData[ \(TraditionalForm\`P(n)\)]], " would not work in the last proof. " }], "Text", Evaluatable->False, AspectRatioFixed->True] }, Closed]] }, Closed]] }, Closed]], Cell[CellGroupData[{ Cell["Strong Induction", "Section", Evaluatable->False, AspectRatioFixed->True, CellTags->"c:16"], Cell[CellGroupData[{ Cell[" The Strong Induction Principle", "Subsection", Evaluatable->False, AspectRatioFixed->True, CellTags->"c:17"], Cell[TextData[{ "As the last example involving Fibonacci numbers indicates, sometimes one \ would like to have not just ", Cell[BoxData[ \(TraditionalForm\`P(n - 1)\)]], " as induction hypothesis, but also ", Cell[BoxData[ \(TraditionalForm\`P(n - 2)\)]], ". In fact, sometimes it is preferable to have all of ", Cell[BoxData[ \(TraditionalForm\`P(0), \[Ellipsis], P(n - 1)\)]], " available as an assumption. There is a slightly different form of \ induction that does exactly this. Again, suppose we have some property ", Cell[BoxData[ \(TraditionalForm\`P(n)\)]], " that may or may not hold of a number ", Cell[BoxData[ \(TraditionalForm\`n\)]], ". \n\n", StyleBox["Strong Induction Principle", FontColor->RGBColor[0, 0, 1]], "\nIn order to show that ", Cell[BoxData[ \(TraditionalForm\`P(n)\)]], " holds for all ", Cell[BoxData[ \(TraditionalForm\`n\)]], ", it suffices to establish the following:\n\n\t", StyleBox["Strong Induction Property", FontColor->RGBColor[0, 0, 1]], ": \n\tFor any ", Cell[BoxData[ \(TraditionalForm\`n\)]], " the following holds: ", Cell[BoxData[ \(TraditionalForm\`\[ForAll] m\ < \ n\ \(P(m)\)\)]], " implies ", Cell[BoxData[ \(TraditionalForm\`P(n)\)]], ".\n\t \nIn other words, we may assume that ", Cell[BoxData[ \(TraditionalForm\`P(m)\)]], " holds for all ", Cell[BoxData[ \(TraditionalForm\`m < n\)]], ", and have to show that ", Cell[BoxData[ \(TraditionalForm\`P(n)\)]], " also holds. " }], "Text", Evaluatable->False, AspectRatioFixed->True], Cell[TextData[{ "It is not surprising that the stronger hypothesis sometimes makes it \ easier to establish the conclusion ", Cell[BoxData[ \(TraditionalForm\`P(n)\)]], ". \nNote that there actually is a base case here, but it is a little \ hidden. For ", Cell[BoxData[ \(TraditionalForm\`n = 0\)]], " we are supposed to demonstrate ", Cell[BoxData[ \(TraditionalForm\`P(0)\)]], ", assuming ", Cell[BoxData[ \(TraditionalForm\`P(m)\)]], " for all ", Cell[BoxData[ \(TraditionalForm\`m < 0\)]], ". But since we are only dealing with non-neagtive integers here, there is \ no such ", Cell[BoxData[ \(TraditionalForm\`m\)]], ", and therefore there are no assumptions. In other words, we have to prove \ ", Cell[BoxData[ \(TraditionalForm\`P(0)\)]], " from scratch, just as in ordinary induction. There is no such thing as a \ free lunch. " }], "Text", Evaluatable->False, AspectRatioFixed->True], Cell[CellGroupData[{ Cell[" Ordinary versus Strong Induction", "Subsubsection", Evaluatable->False, AspectRatioFixed->True, CellTags->"c:18"], Cell[TextData[{ "Perhaps surprisingly, the principle of strong induction can be proven from \ ordinary induction: there is no more proof power in strong induction than in \ ordinary induction, however, the argument can be greatly facilitated. So, \ it's only a matter of convenience. \n\n", StyleBox["Theorem", FontWeight->"Bold"], ": If we can establish the strong induction property for an assertion ", Cell[BoxData[ \(TraditionalForm\`P\)]], ", then ", Cell[BoxData[ \(TraditionalForm\`P(n)\)]], " holds for all ", Cell[BoxData[ \(TraditionalForm\`n\)]], ". \n\nProof. \nLet ", Cell[BoxData[ \(TraditionalForm\`Q(n)\)]], " be the assertion \n\t", Cell[BoxData[ \(TraditionalForm\`P(0)\ \[And] \ P(1)\ \[And] \ \[Ellipsis]\ \[And] \ P(n - 1)\)]], "\nUsing quantifiers, this could be written as ", Cell[BoxData[ \(TraditionalForm\`\[ForAll] \ m < n\ \(P(m)\)\)]], ". So, ", Cell[BoxData[ \(TraditionalForm\`Q(n)\)]], " is precisely the assumption we can make in strong induction when we are \ trying to prove ", Cell[BoxData[ \(TraditionalForm\`P(n)\)]], ". We will show by ordinary induction that ", Cell[BoxData[ \(TraditionalForm\`Q(n)\)]], " holds for all ", Cell[BoxData[ \(TraditionalForm\`n\)]], ". \n\nBase step: ", Cell[BoxData[ \(TraditionalForm\`Q(0)\)]], " is the empty assertion, which is vacuously true. Yes?\nThis is just like \ ", Cell[BoxData[ \(TraditionalForm\`Plus[]\ == \ 0\)]], " or ", Cell[BoxData[ \(TraditionalForm\`Times[]\ == \ 1\)]], ". In fact, even Mathematica knows this:" }], "Text", Evaluatable->False, AspectRatioFixed->True], Cell[BoxData[{ \(And[]\), "\n", \(Or[]\)}], "Input", AspectRatioFixed->True], Cell[TextData[{ "Induction step: assume ", Cell[BoxData[ \(TraditionalForm\`Q(n)\)]], ", and show that ", Cell[BoxData[ \(TraditionalForm\`Q(n + 1)\)]], " holds. \nSince ", Cell[BoxData[ \(TraditionalForm\`Q(n)\)]], " is precisely the hypothesis in strong induction, and since the theorem \ assumes that we have established the strong induction property for ", Cell[BoxData[ \(TraditionalForm\`P\)]], ", we may conclude that ", Cell[BoxData[ \(TraditionalForm\`P(n)\)]], " holds. But then ", Cell[BoxData[ \(TraditionalForm\`P(0)\ \[And] \ P(1)\ \[And] \ \[Ellipsis]\ \[And] \ P(n - 1)\)]], " and ", Cell[BoxData[ \(TraditionalForm\`P(n)\)]], " holds, and therefore ", Cell[BoxData[ \(TraditionalForm\`Q(n + 1)\ \ = \ P(0)\ \[And] \ P(1)\ \[And] \ \[Ellipsis]\ \[And] \ P(n - 1)\ \[And] \ P(n)\)]], " also holds. \n\[EmptySquare]\n" }], "Text", Evaluatable->False, AspectRatioFixed->True] }, Closed]] }, Closed]], Cell[CellGroupData[{ Cell[" Examples", "Subsection", Evaluatable->False, AspectRatioFixed->True, CellTags->"c:19"], Cell[CellGroupData[{ Cell[" The Prime Example", "Subsubsection", Evaluatable->False, AspectRatioFixed->True, CellTags->"c:20"], Cell[TextData[{ "Here is the typical example for strong induction. \n\n", StyleBox["Lemma", FontWeight->"Bold"], ": Every positive integer ", Cell[BoxData[ \(TraditionalForm\`n\)]], " can be written as a product of primes. \n\nProof: \nWe use strong \ induction on ", Cell[BoxData[ \(TraditionalForm\`n\)]], ". The property ", Cell[BoxData[ \(TraditionalForm\`P(n)\)]], " here is: \n ", Cell[BoxData[ \(TraditionalForm\`n\ = \ 0\)]], " ", StyleBox["\[Or] ", FontWeight->"Bold"], " ", Cell[BoxData[ \(TraditionalForm\`n\)]], " can be written as a product of primes. \nLet ", Cell[BoxData[ \(TraditionalForm\`n\ \[GreaterEqual] \ 0\)]], " be arbitrary. We have to show that ", Cell[BoxData[ \(TraditionalForm\`P(n)\)]], " holds, assuming that ", Cell[BoxData[ \(TraditionalForm\`P(m)\)]], " already holds for all ", Cell[BoxData[ \(TraditionalForm\`m\ < \ n\)]], ". \n", Cell[BoxData[ \(TraditionalForm\`P(0)\)]], " is obvious, and a moment's thought reveals that ", Cell[BoxData[ \(TraditionalForm\`P(1)\)]], " also holds: 1 is the empty product of primes. So we only have to deal \ with ", Cell[BoxData[ \(TraditionalForm\`n\ \[GreaterEqual] \ 2\)]], ". We want to show that ", Cell[BoxData[ \(TraditionalForm\`n\)]], " is a product of primes. \n\nThere are two possibilities: \n", StyleBox["Case 1", FontWeight->"Bold"], ": ", Cell[BoxData[ \(TraditionalForm\`n\)]], " is prime. Then we are done. \n", StyleBox["Case 2", FontWeight->"Bold"], ": ", Cell[BoxData[ \(TraditionalForm\`n\)]], " is composite, say ", Cell[BoxData[ \(TraditionalForm\`n\ = \ p\ \[CenterDot]q\)]], " where ", Cell[BoxData[ \(TraditionalForm\`1\ < \ p, q\ < \ n\)]], ". \nBut then by IH, ", Cell[BoxData[ \(TraditionalForm\`p\)]], " and ", Cell[BoxData[ \(TraditionalForm\`q\)]], " are already products of primes, and ", Cell[BoxData[ \(TraditionalForm\`n\)]], " is simply the product of all the primes occurring in these two products. \ \n\[EmptySquare]" }], "Text", Evaluatable->False, AspectRatioFixed->True], Cell[TextData[{ "\n", StyleBox["Comments:", FontWeight->"Bold"], "\n(1) The reason we have to use strong induction here is that the factors \ ", Cell[BoxData[ \(TraditionalForm\`p\)]], " and ", Cell[BoxData[ \(TraditionalForm\`q\)]], " can lie anywhere between 1 and ", Cell[BoxData[ \(TraditionalForm\`n\)]], ", so we need to assume that ", Cell[BoxData[ \(TraditionalForm\`P\)]], " already holds for all these numbers. \n\n(2) Also note that defining ", Cell[BoxData[ \(TraditionalForm\`P(n)\)]], " as we did is really a little too fastidious. A more sloppy approach, \ which can be justified by doing what we just did, is to say that we prove the \ claim by strong induction for all positive integers (without the pesky 0). \n\ \n(3) Even if you don't care about primes (and you should, RSA is based on \ number theory), similar problems occur in many places in CS. For example, a \ compiler has to break up large expressions into smaller ones, and recursively \ digest the smaller pieces. There is no way to predict the size of the smaller \ pieces, so one needs some tool like strong induction to show that the \ compiler works properly. " }], "Text", Evaluatable->False, AspectRatioFixed->True] }, Closed]], Cell[CellGroupData[{ Cell[" Binary Lists", "Subsubsection", Evaluatable->False, AspectRatioFixed->True, CellTags->"c:21"], Cell[TextData[{ "A binary list is a list of 0's and 1's. There are ", Cell[BoxData[ \(TraditionalForm\`2\^n\)]], " such lists of length ", Cell[BoxData[ \(TraditionalForm\`n\)]], ". How many of them have no adjacent 0's? \n\nThis type of question is best \ attacked by a little experimentation, followed by a clever conjecture, and a \ proof. \nFirst, a devious function that computes all the binary lists of \ length ", Cell[BoxData[ \(TraditionalForm\`n\)]], ". Recursion could be used, but this solution introduces you to another \ important, and seemingly incomprehensible, command in Mathematica. " }], "Text", Evaluatable->False, AspectRatioFixed->True], Cell[BoxData[ \(binList[n_Integer] := Distribute[Table[{0, 1}, {n}], List]\)], "Input", AspectRatioFixed->True], Cell[BoxData[{ \(binList[5]\), "\n", \(Length[%]\)}], "Input", AspectRatioFixed->True], Cell[TextData[{ "Works, for whatever reason. Make sure to look up the documentation for ", StyleBox["Distribute", FontFamily->"Courier"], ". If you understand what exactly the command is supposed to do, let me \ know. \nHow do we extract the lists that do not have adjacent 0's? We could \ use a loop to test things by hand, but there is an easier way using pattern \ matching." }], "Text", Evaluatable->False, AspectRatioFixed->True], Cell[BoxData[ \(bin00free[n_Integer]\ := \ DeleteCases[\ binList[n], {___, 0, 0, ___}\ ]\)], "Input", AspectRatioFixed->True], Cell[BoxData[{ \(bin00free[1]\), "\n", \(bin00free[2]\), "\n", \(bin00free[3]\), "\n", \(bin00free[4]\), "\n", \(bin00free[5]\)}], "Input", AspectRatioFixed->True], Cell[TextData[{ "So, we can simply compute the length of the output of ", StyleBox["bin00free", FontFamily->"Courier"], ". " }], "Text", Evaluatable->False, AspectRatioFixed->True], Cell[BoxData[{ \(\(cnt[n_Integer] := Length[bin00free[n]];\)\), "\n", \(cnt /@ Range[10]\)}], "Input", AspectRatioFixed->True], Cell[TextData[{ "Lo and behold, the Fibonacci numbers, except that we start at 2 and 3 this \ time. \n\n", StyleBox["Conjecture", FontWeight->"Bold"], ": \nThe number of 00-free binary lists of length n is ", Cell[BoxData[ \(TraditionalForm\`F\_\(n + 2\)\)]], ", the ", Cell[BoxData[ \(TraditionalForm\`\((n + 2)\)\^nd\)]], " Fibonacci number. \n\nProof: \nWrite ", Cell[BoxData[ \(TraditionalForm\`\[Sigma]\_n\)]], " for the number of 00-free binary lists of length ", Cell[BoxData[ \(TraditionalForm\`n\)]], ". We will show by strong induction on ", Cell[BoxData[ \(TraditionalForm\`n\)]], " that ", Cell[BoxData[ \(TraditionalForm\`\[Sigma]\_n = \ F\_\(n + 2\)\)]], ". Clearly ", Cell[BoxData[ \(TraditionalForm\`\[Sigma]\_0\ = \ 1\)]], " and ", Cell[BoxData[ \(TraditionalForm\`\[Sigma]\_1 = \ 2\)]], ", so we may safely assume ", Cell[BoxData[ \(TraditionalForm\`n\ \[GreaterEqual] \ 2\)]], ". The 00-free lists ", Cell[BoxData[ \(TraditionalForm\`L\)]], " of length ", Cell[BoxData[ \(TraditionalForm\`n\)]], " break up into two groups as follows. \n\nCase 1: ", Cell[BoxData[ \(TraditionalForm\`L\)]], " ends in 1.\nIn this case ", Cell[BoxData[ \(TraditionalForm\`L\ = \ app(K, 1)\)]], " where ", Cell[BoxData[ \(TraditionalForm\`K\)]], " is an arbitrary 00-free lists of length", Cell[BoxData[ \(TraditionalForm\`\(\(\ \ \)\(n - 1\)\)\)]], ". \n\nCase 2: ", Cell[BoxData[ \(TraditionalForm\`L\)]], " ends in 0.\nTo avoid a double 0, and since the length of ", Cell[BoxData[ \(TraditionalForm\`L\)]], " is at least 2, ", Cell[BoxData[ \(TraditionalForm\`L\)]], " must actually end in 10. So, ", Cell[BoxData[ \(TraditionalForm\`L\ = \ K\ \[CirclePlus]\ 10\)]], " where K is an arbitrary 00-free list of length ", Cell[BoxData[ \(TraditionalForm\`n - 2\)]], ". \n\nBut then ", Cell[BoxData[ \(TraditionalForm\`\[Sigma]\_n = \ \[Sigma]\_\(n - 1\)\ + \ \[Sigma]\_\ \(n - 2\)\)]], ". By IH, ", Cell[BoxData[ \(TraditionalForm\`\[Sigma]\_n = \ \(F\_\(n + 1\)\ + \ F\_n\ = \ F\_\(n + 2\)\)\)]], ", and we are done. \n\[EmptySquare]" }], "Text", Evaluatable->False, AspectRatioFixed->True] }, Closed]], Cell[CellGroupData[{ Cell[" Back to foo and bag", "Subsubsection", Evaluatable->False, AspectRatioFixed->True, CellTags->"c:22"], Cell["\<\ Recall the recursive function foo from the notebook on recursion. \ \ \>", "Text", Evaluatable->False, AspectRatioFixed->True], Cell[BoxData[{ \(\(foo[1] = 0;\)\), "\n", \(\(foo[n_] := foo[Floor[n\/2]] + 1;\)\)}], "Input", AspectRatioFixed->True], Cell[TextData[{ StyleBox["Lemma", FontWeight->"Bold"], ": For all positive ", Cell[BoxData[ \(TraditionalForm\`n\)]], ": ", StyleBox[" ", FontWeight->"Bold"], Cell[BoxData[ \(TraditionalForm\`\(\(foo( n)\)\(\ \)\(=\)\(\ \)\(\[LeftFloor]\ \(log\_2\) n\[RightFloor]\)\(\ \)\)\)]], ". \nProof: \nFirst, we need one little fact about the logarithm function: \ it is strictly increasing, meaning that, for ", Cell[BoxData[ \(TraditionalForm\`\(\(\ \)\(0\ < \ x\ < \ y\)\)\)]], " we have ", Cell[BoxData[ \(TraditionalForm\`\(\(\ \)\(\(log\_2\) x\ < \ \ \(log\_2\) y\)\)\)]], ". Also, by its very definition, ", Cell[BoxData[ \(TraditionalForm\`2\^\(\(log\_2\) x\)\ = \ x\)]], ". " }], "Text", Evaluatable->False, AspectRatioFixed->True], Cell[BoxData[ \(\(Plot[\ Log[2, x], {x, 1, 512}, PlotStyle \[Rule] Blue];\)\)], "Input",\ AspectRatioFixed->True], Cell[TextData[{ "But then it follows that for all positive real ", Cell[BoxData[ \(TraditionalForm\`x\)]], ": \n\t", Cell[BoxData[ \(TraditionalForm\`2\^k\ \[LessEqual] \ x\ < \ 2\^\(k + 1\)\ \ iff\ \ \ k\ \[LessEqual] \ \(log\_2\) x\ < \ k\ + \ 1. \)]], "\nFrom the definition of the floor function, \n\t", Cell[BoxData[ \(TraditionalForm\`2\^k\ \[LessEqual] \ x\ < \ 2\^\(k + 1\)\ \ iff\ \ \ \[LeftFloor]\ \(log\_2\) x\ \[RightFloor]\ = \ \ \(\(k\)\(.\)\)\)]], "\nIn particular, this is true for integers ", Cell[BoxData[ \(TraditionalForm\`x\)]], ". We can now use strong induction on ", Cell[BoxData[ \(TraditionalForm\`n\ > \ 0\)]], " to show that \n\t", Cell[BoxData[ \(TraditionalForm\`2\^k\ \[LessEqual] \ x\ < \ 2\^\(k + 1\)\ \ iff\ \ \ \(foo(n)\) = \ \ \(\(k\)\(.\)\)\)]], "\n\nConsider ", Cell[BoxData[ \(TraditionalForm\`n\ \[GreaterEqual] \ 1\)]], ", assuming that this claim is already true for all ", Cell[BoxData[ \(TraditionalForm\`0\ < \ i\ < \ n\)]], ". \n\[EmptyCircle] If ", Cell[BoxData[ \(TraditionalForm\`n\ = \ 2 m\)]], " is even, we have ", Cell[BoxData[ \(TraditionalForm\`foo(n)\ = \ foo(m)\ + \ 1\)]], ", so that \n", Cell[BoxData[ \(TraditionalForm\`foo(n)\ = \ \(k\ \ \ iff\ \ \(foo(m)\)\ = \ k - 1\ \ iff\ \ 2\^\(k - 1\)\ \[LessEqual] \ m\ < \ 2\^k\ \ \ iff\ \ 2\^k\ \[LessEqual] \ n\ < \ 2\^\(k + 1\)\)\)]], ".\n\[EmptyCircle] If ", Cell[BoxData[ \(TraditionalForm\`n\ = \ 2 m\ + \ 1\ > \ 1\)]], " is odd, we have ", Cell[BoxData[ \(TraditionalForm\`foo(n)\ = \ \(foo(n - 1)\ = \ foo(m)\)\)]], ", and the same argument works. The case ", Cell[BoxData[ \(TraditionalForm\`n = 1\)]], " is obvious. \n\[EmptySquare]\n" }], "Text", Evaluatable->False, AspectRatioFixed->True], Cell[TextData[{ StyleBox["Exercise", FontWeight->"Bold"], ":\nPerform a similar argument for the ", Cell[BoxData[ FormBox[ StyleBox["bag", "SmallText"], TraditionalForm]]], " function. " }], "Text", Evaluatable->False, AspectRatioFixed->True] }, Closed]], Cell[CellGroupData[{ Cell[" The Least Element Principle", "Subsubsection", Evaluatable->False, AspectRatioFixed->True, CellTags->"c:23"], Cell[TextData[{ "In our initial discussion of induction, we showed that the Least Element \ Principle can be used to motivate induction. We will now show that induction \ suffices to prove the LEP, so the two principles are equally powerful. \ However, one may be easier to use in a specific proof than the other. \n\n", StyleBox["Least Element Principle", FontColor->RGBColor[0, 0, 1]], "\nEvery non-empty set of natural numbers has a least element.\n\nProof: \n\ We proof the contrapositive: if a set ", Cell[BoxData[ \(TraditionalForm\`T\)]], " has no least element, then ", Cell[BoxData[ \(TraditionalForm\`T\)]], " is empty. \nSuppose ", Cell[BoxData[ \(TraditionalForm\`T\ \[SubsetEqual] \ \[DoubleStruckCapitalN]\)]], " is some set of natural numbers that has no least element. We will show \ by strong induction that the complement of ", Cell[BoxData[ \(TraditionalForm\`T\)]], " comprises all natural numbers. For let ", Cell[BoxData[ \(TraditionalForm\`S\ = \ \[DoubleStruckCapitalN]\ - \ T\)]], " be the complement of ", Cell[BoxData[ \(TraditionalForm\`T\)]], ". Assume that all numbers ", Cell[BoxData[ \(TraditionalForm\`m\ < \ n\)]], " are in ", Cell[BoxData[ \(TraditionalForm\`S\)]], ", for some natural number ", Cell[BoxData[ \(TraditionalForm\`n\)]], ". Then ", Cell[BoxData[ \(TraditionalForm\`n\)]], " must also be in ", Cell[BoxData[ \(TraditionalForm\`S\)]], ", for otherwise ", Cell[BoxData[ \(TraditionalForm\`n\)]], " would be in ", Cell[BoxData[ \(TraditionalForm\`T\)]], ", and ", Cell[BoxData[ \(TraditionalForm\`T\)]], " would have a least element. So, ", Cell[BoxData[ \(TraditionalForm\`S\ = \ \[DoubleStruckCapitalN]\)]], ", and therefore ", Cell[BoxData[ \(TraditionalForm\`T\)]], " is the empty set, as required. \n\[EmptySquare]" }], "Text", Evaluatable->False, AspectRatioFixed->True], Cell["\<\ So, we have closed the circle: \tLEP \[DoubleLongRightArrow] induction \[DoubleLongRightArrow] strong \ induction \[DoubleLongRightArrow] LEP. All three principles are equivalent, they all have the same proof power. \ There are much stronger proof principles in mathematics, but we will hardly \ ever need any of them. \ \>", "Text", Evaluatable->False, AspectRatioFixed->True] }, Closed]] }, Closed]] }, Closed]], Cell[CellGroupData[{ Cell["Induction in Geometry", "Section", Evaluatable->False, AspectRatioFixed->True, CellTags->"c:24"], Cell[CellGroupData[{ Cell["Triominos", "Subsection", Evaluatable->False, AspectRatioFixed->True, CellTags->"c:25"], Cell[TextData[{ "All our examples so far deal with numbers or lists. Here is a completely \ different problem taken from plane geometry. Suppose we have an ", Cell[BoxData[ \(TraditionalForm\`n\ \[Cross]\ n\)]], " square, where ", Cell[BoxData[ \(TraditionalForm\`n\)]], " is a power of 2. Show that the square can be tiled with triominos, so \ that exactly one square remains uncovered. A triomino here is simple an \ L-shaped object consisting of three unit squares. Tiling means that the \ pieces are not allowed to overlap, and there must be no gaps between them. " }], "Text"], Cell[TextData[{ "In other words, for each ", Cell[BoxData[ \(TraditionalForm\`n\ \[Cross]\ n\)]], " square, where ", Cell[BoxData[ \(TraditionalForm\`n\ = \ 2\^k\)]], ", we have to prove that it can be tiled after some square ", Cell[BoxData[ \(TraditionalForm\`\((i, j)\)\)]], ", ", Cell[BoxData[ \(TraditionalForm\`1\ \[LessEqual] \ i, j\ \[LessEqual] \ n\)]], " has been omitted. It is absolutely not clear that this is true, so here a \ few examples. Actually, if you study the pictures carefully, a proof will \ materialize. \n" }], "Text"], Cell[CellGroupData[{ Cell[" Code -- don't look, just execute", "Subsubsection", CellTags->"c:26"], Cell[BoxData[{ \(Clear["\", rules, "\", tiling, makeTiling]\), "\n", \(\(ellSW[x_, y_] := Line[\(({x, y} + #1 &)\) /@ {{0, 0}, {0, 2}, {1, 2}, {1, 1}, {2, 1}, {2, 0}, {0, 0}}];\)\), "\n", \(\(ellSE[x_, y_] := Line[\(({x, y} + #1 &)\) /@ {{0, 0}, {0, 1}, {1, 1}, {1, 2}, {2, 2}, {2, 0}, {0, 0}}];\)\), "\n", \(\(ellNE[x_, y_] := Line[\(({x, y} + #1 &)\) /@ {{0, 1}, {0, 2}, {2, 2}, {2, 0}, {1, 0}, {1, 1}, {0, 1}}];\)\), "\n", \(\(ellNW[x_, y_] := Line[\(({x, y} + #1 &)\) /@ {{0, 0}, {0, 2}, {2, 2}, {2, 1}, {1, 1}, {1, 0}, {0, 0}}];\)\), "\n", \(\(rules = {tr[0, x_, y_] \[RuleDelayed] ellSW[x, y], tr[1, x_, y_] \[RuleDelayed] ellSE[x, y], tr[2, x_, y_] \[RuleDelayed] ellNE[x, y], tr[3, x_, y_] \[RuleDelayed] ellNW[x, y]};\)\), "\n", \(\(shiftRight[t_tr, nn_] := ReplacePart[t, t\[LeftDoubleBracket]2\[RightDoubleBracket] + 2\^nn, 2];\)\), "\n", \(shiftRight[LL_List, nn_] := \((shiftRight[#1, nn] &)\) /@ LL\), "\n", \(\(shiftUp[t_tr, nn_] := ReplacePart[t, t\[LeftDoubleBracket]3\[RightDoubleBracket] + 2\^nn, 3];\)\), "\n", \(shiftUp[LL_List, nn_] := \((shiftUp[#1, nn] &)\) /@ LL\), "\n", \(\(shiftDiag[xx_, nn_] := shiftUp[shiftRight[xx, nn], nn];\)\), "\n", \(\(tiling[1, 1, 1] := {tr[2, 0, 0]};\)\), "\n", \(\(tiling[1, 1, 2] := {tr[1, 0, 0]};\)\), "\n", \(\(tiling[1, 2, 1] := {tr[3, 0, 0]};\)\), "\n", \(\(tiling[1, 2, 2] := {tr[0, 0, 0]};\)\), "\n", \(\(tiling[k_, i_, j_] := Module[{nn, LL}, nn = 2\^\(k - 1\); If[i \[LessEqual] nn && j \[LessEqual] nn, \(LL = Join[tiling[k - 1, i, j], shiftRight[tiling[k - 1, 1, nn], k - 1], shiftUp[tiling[k - 1, nn, 1], k - 1], shiftDiag[tiling[k - 1, 1, 1], k - 1], {tr[2, nn - 1, nn - 1]}];\)]; If[i \[LessEqual] nn && j > nn, \(LL = Join[tiling[k - 1, nn, nn], shiftRight[tiling[k - 1, 1, nn], k - 1], shiftUp[tiling[k - 1, i, j - nn], k - 1], shiftDiag[tiling[k - 1, 1, 1], k - 1], {tr[1, nn - 1, nn - 1]}];\)]; If[i > nn && j \[LessEqual] nn, \(LL = Join[tiling[k - 1, nn, nn], shiftRight[tiling[k - 1, i - nn, j], k - 1], shiftUp[tiling[k - 1, nn, 1], k - 1], shiftDiag[tiling[k - 1, 1, 1], k - 1], {tr[3, nn - 1, nn - 1]}];\)]; If[i > nn && j > nn, \(LL = Join[tiling[k - 1, nn, nn], shiftRight[tiling[k - 1, 1, nn], k - 1], shiftUp[tiling[k - 1, nn, 1], k - 1], shiftDiag[tiling[k - 1, i - nn, j - nn], k - 1], {tr[0, nn - 1, nn - 1]}];\)]; LL];\)\), "\n", \(\(square[x_, y_] := {Blue, Polygon[{{x - 1, y - 1}, {x, y - 1}, {x, y}, {x - 1, y}, {x - 1, y - 1}}]};\)\), "\n", \(\(makeTiling[kk_, ii_, jj_Integer, opts___?OptionQ] := Show[Graphics[Join[tiling[kk, ii, jj] /. rules, square[ii, jj]]], AspectRatio \[Rule] 1, opts];\)\)}], "Input"] }, Closed]], Cell[CellGroupData[{ Cell[" Pictures", "Subsubsection", CellTags->"c:27"], Cell[TextData[{ "The last code cell defines a function ", StyleBox[" makeTiling[k, i, j] ", "SmallText"], "where ", Cell[BoxData[ \(TraditionalForm\`k\)]], " controls the size of the square (", Cell[BoxData[ \(TraditionalForm\`2\^k\[Cross]\ 2\^k\)]], "), and ", Cell[BoxData[ \(TraditionalForm\`i\)]], " and ", Cell[BoxData[ \(TraditionalForm\`j\)]], " indicate the subsquare that is supposed to be left uncovered (we need ", Cell[BoxData[ \(TraditionalForm\`1\ \[LessEqual] \ i, j\ \[LessEqual] \ n\)]], "). \n\nHere are some examples. " }], "Text"], Cell[BoxData[ \(\(makeTiling[3, 1, 1];\)\)], "Input"], Cell[BoxData[ \(\(makeTiling[3, 5, 5];\)\)], "Input"], Cell[BoxData[ \(\(makeTiling[3, 5, 6];\)\)], "Input"], Cell[BoxData[ \(\(makeTiling[5, 10, 20];\)\)], "Input"], Cell[BoxData[{ \(\(tb = Table[makeTiling[2, i, j, DisplayFunction \[Rule] Identity], {i, 4}, {j, 4}];\)\), "\n", \(\(Show[GraphicsArray[tb]];\)\)}], "Input"], Cell["\<\ Can you see how the tiling works in general? Can you turn this into real proof by induction? \ \>", "Text"] }, Closed]] }, Closed]], Cell[CellGroupData[{ Cell["Smith/Sierpinski", "Subsection", Evaluatable->False, AspectRatioFixed->True, CellTags->"c:28"], Cell[TextData[{ "Just as a reminder, the countless images of fractals that one can now see \ everywhere, are often generated by recursive procedures. Establishing \ properties of these objects often involves induction arguments. One \ interesting fact to remember is that these geometric objects have non-integer \ dimensions. \n\nFor example, the following example of a recursive pattern, \ which is usually attributed to Sierpinski (a famous Polish topologist, though \ Henry J.S. Smith at Oxford found it a number of years earlier), has \ dimension ", Cell[BoxData[ \(TraditionalForm\`log\_3\)]], " 8." }], "Text"], Cell[BoxData[ \(N[Log[3, 8]]\)], "Input"], Cell["\<\ Fractal objects arise rather frequently in nature: clouds, \ coastlines, ferns, sponges, mountain ranges. Old-fashioned Euclidean geometry \ is really not appropriate to describe many common objects. No, we will not \ do a crash course in fractal geometry, it's too hard. But we will see more \ fractals when we deal with cellular automata. \ \>", "Text"], Cell[CellGroupData[{ Cell[" Code", "Subsubsection", CellTags->"c:29"], Cell["\<\ It is actually quite amazing that the following little piece of \ code generates rather complicated geometric structures. We use simple \ substitutions of matrix elements by matrices.\ \>", "Text"], Cell[BoxData[{ \(\(<< LinearAlgebra`MatrixManipulation`;\)\), "\n", \(Clear[next, makeMatrix]\), "\n", \(\(\(next[rules_List]\)[L_?MatrixQ]\ := \ BlockMatrix[L\ /. \ rules];\)\), "\n", \(\(makeMatrix[rules_List, n_Integer, init_: {{1}}]\ := \ \[IndentingNewLine]\t\tNest[\ next[rules], \ init, \ n\ ];\)\)}], "Input"] }, Closed]], Cell[CellGroupData[{ Cell["Pictures", "Subsubsection", CellTags->"c:30"], Cell["\<\ Here are the pictures. First, make a list of rectangles by \ iterating the next function, and applying toSquare to its output. Then, make \ a Graphics object, and display it. \ \>", "Text"], Cell[BoxData[{ \(\(rules\ = \ {\[IndentingNewLine]0 \[Rule] {{0, 0, 0}, {0, 0, 0}, {0, 0, 0}}, \[IndentingNewLine]1 \[Rule] \ {{1, 1, 1}, {1, 0, 1}, {1, 1, 1}}\[IndentingNewLine]};\)\), "\n", \(\(mat\ = \ makeMatrix[\ rules, 4];\)\), "\n", \(\(PlotMatrix[mat];\)\)}], "Input"], Cell[BoxData[{ \(\(rules\ = \ {\[IndentingNewLine]0 \[Rule] {{0, 0, 0}, {0, 0, 0}, {0, 0, 0}}, \[IndentingNewLine]1 \[Rule] \ {{0, 1, 0}, {1, 1, 1}, {1, 1, 1}}\[IndentingNewLine]};\)\), "\n", \(\(mat\ = \ makeMatrix[\ rules, 4];\)\), "\n", \(\(PlotMatrix[mat];\)\)}], "Input"], Cell[TextData[{ "The last structure is thinner, it has fractal dimension ", Cell[BoxData[ \(TraditionalForm\`\(log\_3\) 7\ \[TildeTilde] \ 1.77\)]], ", less than the Sierpinski gadget. " }], "Text"], Cell[BoxData[{ \(\(rules\ = \ {\[IndentingNewLine]0 \[Rule] {{0, 0, 0}, {0, 0, 0}, {0, 0, 0}}, \[IndentingNewLine]1 \[Rule] \ {{0, 1, 0}, {1, 1, 1}, {1, 1, 1}}\[IndentingNewLine]};\)\), "\n", \(\(mat\ = \ makeMatrix[\ rules, 4];\)\), "\n", \(\(PlotMatrix[mat];\)\)}], "Input"], Cell["Another classic, a ", "Text"], Cell[BoxData[{ \(\(rules\ = \ {\[IndentingNewLine]0 \[Rule] {{0, 0}, {0, 0}}, \[IndentingNewLine]1 \[Rule] \ {{0, 1}, {1, 1}}\[IndentingNewLine]};\)\), "\n", \(\(mat\ = \ makeMatrix[\ rules, 6];\)\), "\n", \(\(PlotMatrix[mat];\)\)}], "Input"], Cell[TextData[{ "The last fractal is quite thin, its dimension is only ", Cell[BoxData[ \(TraditionalForm\`\(log\_2\) 3\ \[TildeTilde] \ 1.58\)]], ". Here is the sequence of intermediate pictures (computed in a rather \ inefficent way). One can see nicely how a fractal is produced in the limit \ (as with all fractals, the real object is only obtained in the limit, all we \ can do is to represent a few early stages in the development). " }], "Text"], Cell[BoxData[{ \(\(Table[\ PlotMatrix[\ makeMatrix[\ rules, k], DisplayFunction \[Rule] Identity], \ {k, 6}];\)\), "\n", \(\(ShowArray[\ %, \ DisplayFunction \[Rule] $DisplayFunction\ ];\)\)}], "Input"], Cell["Another example of somewhat surprising structure.", "Text"], Cell[BoxData[{ \(\(rules\ = \ {\[IndentingNewLine]0 \[Rule] {{1, 1, 1}, {1, 1, 1}, {1, 1, 1}}, \[IndentingNewLine]1 \[Rule] \ {{0, 1, 0}, {1, 0, 1}, {0, 1, 0}}\[IndentingNewLine]};\)\), "\[IndentingNewLine]", \(\(mat\ = \ makeMatrix[\ rules, 5];\)\), "\n", \(\(PlotMatrix[mat];\)\)}], "Input"], Cell["\<\ Of course, we can play similar games with more than 2 colors.\ \>", \ "Text"], Cell[BoxData[{ \(\(rules\ = \ {\[IndentingNewLine]0 \[Rule] {{1, 1, 1}, {1, 1, 1}, {1, 1, 1}}, \[IndentingNewLine]1 \[Rule] \ {{0, 1, 0}, {1, 2, 1}, {0, 1, 0}}, \[IndentingNewLine]2 \[Rule] \ {{0, 2, 0}, {2, 0, 2}, {0, 2, 0}}\[IndentingNewLine]};\)\), "\[IndentingNewLine]", \(\(mat\ = \ makeMatrix[\ rules, 4];\)\), "\n", \(\(PlotMatrix[\ mat\ /. \ 2 \[Rule] 5];\)\)}], "Input"], Cell[BoxData[{ \(\(rules\ = \ {\[IndentingNewLine]0 \[Rule] {{0, 0, 0}, {0, 0, 0}, {0, 0, 0}}, \[IndentingNewLine]1 \[Rule] \ {{1, 1, 1}, {1, 2, 1}, {1, 1, 1}}, \[IndentingNewLine]2 \[Rule] \ {{0, 2, 0}, {2, 1, 2}, {0, 2, 0}}\[IndentingNewLine]};\)\), "\[IndentingNewLine]", \(\(mat\ = \ makeMatrix[\ rules, 5];\)\), "\n", \(\(PlotMatrix[\ mat\ /. \ 2 \[Rule] 3];\)\)}], "Input"], Cell[BoxData[{ \(\(rules\ = \ {\[IndentingNewLine]0 \[Rule] {{1, 1, 1}, {1, 0, 1}, {1, 1, 1}}, \[IndentingNewLine]1 \[Rule] \ {{2, 2, 2}, {2, 1, 2}, {2, 2, 2}}, \[IndentingNewLine]2 \[Rule] \ {{0, 1, 0}, {1, 0, 1}, {0, 1, 0}}\[IndentingNewLine]};\)\), "\[IndentingNewLine]", \(\(mat\ = \ makeMatrix[\ rules, 4];\)\), "\n", \(\(PlotMatrix[mat\ /. \ 2 \[Rule] 3];\)\)}], "Input"], Cell[BoxData[{ \(\(rules\ = \ {\[IndentingNewLine]0 \[Rule] {{0, 1, 2}, {1, 2, 0}, {2, 0, 1}}, \[IndentingNewLine]1 \[Rule] \ {{2, 2, 2}, {2, 1, 2}, {2, 2, 2}}, \[IndentingNewLine]2 \[Rule] \ {{1, 0, 1}, {0, 1, 0}, {1, 0, 1}}\[IndentingNewLine]};\)\), "\[IndentingNewLine]", \(\(mat\ = \ makeMatrix[\ rules, 4];\)\), "\n", \(\(PlotMatrix[mat];\)\)}], "Input"], Cell[BoxData[{ \(\(rules\ = \ {\[IndentingNewLine]0 \[Rule] {{0, 0, 2}, {1, 2, 1}, {2, 0, 0}}, \[IndentingNewLine]1 \[Rule] \ {{1, 0, 1}, {0, 1, 0}, {1, 0, 1}} + 1, \[IndentingNewLine]2 \[Rule] \ {{1, 0, 1}, {0, 1, 0}, {1, 0, 1}}\[IndentingNewLine]};\)\), "\[IndentingNewLine]", \(\(mat\ = \ makeMatrix[\ rules, 4];\)\), "\n", \(\(PlotMatrix[mat];\)\)}], "Input"], Cell[BoxData[{ \(\(rules\ = \ {\[IndentingNewLine]0 \[Rule] {{0, 0, 2}, {0, 2, 0}, {2, 0, 0}}, \[IndentingNewLine]1 \[Rule] \ {{0, 1, 0}, {1, 1, 1}, {0, 1, 0}}, \[IndentingNewLine]2 \[Rule] \ {{1, 0, 1}, {0, 1, 0}, {1, 0, 1}}\[IndentingNewLine]};\)\), "\[IndentingNewLine]", \(\(mat\ = \ makeMatrix[\ rules, 5];\)\), "\n", \(\(PlotMatrix[mat];\)\)}], "Input"], Cell[BoxData[ \({0 \[Rule] {{0, 2, 1}, {1, 2, 1}, {1, 0, 2}}, 1 \[Rule] {{2, 2, 1}, {1, 2, 0}, {1, 0, 0}}, 2 \[Rule] {{0, 2, 2}, {2, 1, 1}, {2, 1, 0}}}\)], "Input"], Cell[BoxData[ \({0 \[Rule] {{2, 0, 1}, {0, 2, 1}, {0, 0, 1}}, 1 \[Rule] {{0, 2, 0}, {0, 0, 2}, {0, 0, 2}}, 2 \[Rule] {{1, 1, 2}, {0, 1, 0}, {1, 2, 2}}}\)], "Input"], Cell[BoxData[ \({0 \[Rule] {{2, 1, 0}, {0, 0, 0}, {1, 1, 0}}, 1 \[Rule] {{0, 0, 0}, {1, 2, 1}, {1, 0, 2}}, 2 \[Rule] {{1, 1, 2}, {2, 2, 1}, {0, 0, 1}}}\)], "Input"], Cell[BoxData[{ \(\(rules\ = \ {\[IndentingNewLine]0 \[Rule] {{0, 1, 2}, {1, 2, 0}, {2, 0, 1}}, \[IndentingNewLine]1 \[Rule] \ {{0, 1, 2}, {1, 2, 0}, {2, 0, 1}}, \[IndentingNewLine]2 \[Rule] \ {{0, 1, 2}, {2, 0, 1}, {1, 2, 0}}\[IndentingNewLine]};\)\), "\[IndentingNewLine]", \(\(mat\ = \ makeMatrix[\ rules, 5];\)\), "\n", \(\(PlotMatrix[mat];\)\)}], "Input"], Cell[BoxData[{ \(\(rules\ = \ {\[IndentingNewLine]0 \[Rule] IdentityMatrix[3], \[IndentingNewLine]1 \[Rule] \ 2\ IdentityMatrix[3], \[IndentingNewLine]2 \[Rule] \ RotateRight /@ {{0, 1, 2}, {1, 2, 0}, {2, 0, 1}}\[IndentingNewLine]};\)\), "\[IndentingNewLine]", \(\(mat\ = \ makeMatrix[\ rules, 5];\)\), "\n", \(\(PlotMatrix[mat];\)\)}], "Input"] }, Closed]] }, Closed]] }, Closed]], Cell[CellGroupData[{ Cell["Structural Induction on Lists", "Section", Evaluatable->False, AspectRatioFixed->True, CellTags->"c:2"], Cell[TextData[{ "Our examples of induction so far are all limited to natural numbers. In \ computer science, where one often deals with other data types, such as lists, \ trees, graphs, and so forth, it is convenient to have induction principles \ that directly apply to these data types. These principles are referred to as \ ", StyleBox["structural induction", FontColor->RGBColor[0, 0, 1]], ". Everything boils down to ordinary induction in the end, but the \ arguments are often quite a bit easier if one used the other induction \ principles. We will here focus our attention on lists. " }], "Text", Evaluatable->False, AspectRatioFixed->True], Cell[TextData[{ "\n", StyleBox["WARNING", FontColor->RGBColor[1, 0, 0]], "\nThe proofs in this section tend to be extremely tedious, every single \ step is a trivial manipulation of the previous term, but it is very easy to \ get lost in the chain of steps. Make sure you understand the basic strategy, \ the single steps are then very easy to reproduce. Needless to say, this type \ of mechanical reasoning is ideall suited for machines." }], "Text", Evaluatable->False, AspectRatioFixed->True], Cell[CellGroupData[{ Cell[" Structural Induction", "Subsection", Evaluatable->False, AspectRatioFixed->True, CellTags->"c:3"], Cell[CellGroupData[{ Cell[" Induction on Length", "Subsubsection", Evaluatable->False, AspectRatioFixed->True, CellTags->"c:4"], Cell[TextData[{ "Recall our axioms for lists. \n\t(1) ", Cell[BoxData[ \(TraditionalForm\`\(\({}\)\(\ \ \)\)\)]], "is a list (the empty list ),\n\t(2) for any list ", Cell[BoxData[ \(TraditionalForm\`L\)]], ", and any element ", Cell[BoxData[ \(TraditionalForm\`a\)]], ", ", Cell[BoxData[ \(TraditionalForm\`app(L, a)\)]], " is a list.\nUsing these axioms, we saw how to define a recursive \ functions ", Cell[BoxData[ \(TraditionalForm\`f\)]], " on lists by \n\t(1) specifying ", Cell[BoxData[ \(TraditionalForm\`f({})\)]], "\n\t(2) specifying ", Cell[BoxData[ \(TraditionalForm\`f(app(L, a))\)]], ", using a recursive call to ", Cell[BoxData[ \(TraditionalForm\`f(L)\)]], "." }], "Text", Evaluatable->False, AspectRatioFixed->True], Cell[TextData[{ "Now consider the problem of proving assertions about lists, say, some \ assertion ", Cell[BoxData[ \(TraditionalForm\`P(L)\)]], ". \n\n", StyleBox["Structural Induction Principle (Length)", FontColor->RGBColor[0, 0, 1]], "\nIn order to establish ", Cell[BoxData[ \(TraditionalForm\`P(L)\)]], " for all lists ", Cell[BoxData[ \(TraditionalForm\`L\)]], " is suffices to show that\n(SIP1) ", Cell[BoxData[ \(TraditionalForm\`P({})\)]], " holds,\n(SIP2) ", Cell[BoxData[ \(TraditionalForm\`P(\ app(L, a)\ )\)]], " holds for all elements ", Cell[BoxData[ \(TraditionalForm\`a\)]], ", assuming that ", Cell[BoxData[ \(TraditionalForm\`P(L)\)]], " holds. \n\nThis is completely analogous to induction on the natural \ numbers, and referred to as ", StyleBox["structural induction", FontColor->RGBColor[0, 0, 1]], " (on lists). (SIP1) is the base case, and (SIP2) is the induction step. \ Instead of adding 1 to a number, we append another element to a list. We can \ use ordinary induction to show this proof principle is sound.\n\n", StyleBox["Theorem", FontWeight->"Bold"], ": Let ", Cell[BoxData[ \(TraditionalForm\`\(\(P\)\(\ \)\)\)]], "be an assertion about lists, and assume that (SIP1) and (SIP2) hold. Then \ ", Cell[BoxData[ \(TraditionalForm\`P(L)\)]], " holds for all lists ", Cell[BoxData[ \(TraditionalForm\`L\)]], ". \n\nProof:\nWe show by induction on ", Cell[BoxData[ \(TraditionalForm\`n\ = \ \(\(|\)\(\(L\)\(|\)\)\)\)]], " that ", Cell[BoxData[ \(TraditionalForm\`P(L)\)]], " holds for all lists of length ", Cell[BoxData[ \(TraditionalForm\`n\)]], ". \nBase case: ", Cell[BoxData[ \(TraditionalForm\`n\ = \ 0\)]], ", so that ", Cell[BoxData[ \(TraditionalForm\`L\ = \ {}\)]], ". This is taken care of by (SIP1). \nInduction step: ", Cell[BoxData[ \(TraditionalForm\`n\ > \ 0\)]], ". Then we can write ", Cell[BoxData[ \(TraditionalForm\`L = \ app(K, a)\)]], " where ", Cell[BoxData[ \(TraditionalForm\`\(\(|\)\(K\)\(|\)\)\ = \ n - 1\ < \ n\)]], ". Hence, by IH, ", Cell[BoxData[ \(TraditionalForm\`P(K)\)]], " holds. But then by (SIP2) it follows that ", Cell[BoxData[ \(TraditionalForm\`P(L)\)]], " also holds. \n\[EmptySquare]\n\nAs the proof shows, structural induction \ really boils down to induction on the length of the list. However, it is \ often less cumbersome to use structural induction directly. " }], "Text", Evaluatable->False, AspectRatioFixed->True] }, Closed]], Cell[CellGroupData[{ Cell[" Induction on Depth", "Subsubsection", Evaluatable->False, AspectRatioFixed->True, CellTags->"c:5"], Cell[TextData[{ "Another variation of structural induction on lists that is often useful is \ based on depth rather than length. Suppose we can show that \n\n", StyleBox["Structural Induction Principle (Depth)\n", FontColor->RGBColor[0, 0, 1]], "In order to establish ", Cell[BoxData[ \(TraditionalForm\`P(L)\)]], " for all lists ", Cell[BoxData[ \(TraditionalForm\`L\)]], " is suffices to show that\n\t(SIP D) Let ", Cell[BoxData[ \(TraditionalForm\`L\)]], " be a list of depth ", Cell[BoxData[ \(TraditionalForm\`d\)]], ". Then ", Cell[BoxData[ \(TraditionalForm\`P(L)\)]], " holds, \n\t\tassuming ", Cell[BoxData[ \(TraditionalForm\`P(K)\)]], " already holds for all lists ", Cell[BoxData[ \(TraditionalForm\`K\)]], " of depth less than ", Cell[BoxData[ \(TraditionalForm\`d\)]], ". \n\nSo, we first have to show that ", Cell[BoxData[ \(TraditionalForm\`P({a\_1, \[Ellipsis], a\_n})\)]], " holds for all atoms ", Cell[BoxData[ \(TraditionalForm\`a\_i\)]], ", then we show that ", Cell[BoxData[ \(TraditionalForm\`P\)]], " holds for all lists containing atoms and such flat lists of atoms, and so \ forth. Note that the length of the lists here is completely irrelevant, only \ the depth counts. \nIt is a good idea to concoct a proof of this induction \ principle, assuming only ordinary induction on integers. " }], "Text", Evaluatable->False, AspectRatioFixed->True] }, Closed]] }, Closed]], Cell[CellGroupData[{ Cell[" Joining Lists", "Subsection", Evaluatable->False, AspectRatioFixed->True, CellTags->"c:6"], Cell["\<\ Recall the definitions for the recursive implementation of the join \ function. \ \>", "Text", Evaluatable->False, AspectRatioFixed->True], Cell["\<\ join[{xx___},{}] := {xx}; join[{xx___},{yy___,y_}] := Append[join[{xx},{yy}],y];\ \>", "Input", AspectRatioFixed->True], Cell[TextData[{ "We will now formally prove the following basic facts about join. To keep \ notation halfway under control, we will write ", Cell[BoxData[ \(TraditionalForm\`K\ \[CirclePlus]\ L\)]], " for the join of lists ", Cell[BoxData[ \(TraditionalForm\`K\)]], " and ", Cell[BoxData[ \(TraditionalForm\`L\)]], ", and we abbreviate the append operation to ", Cell[BoxData[ \(TraditionalForm\`app(L, x)\)]], ". First, let us rewrite the code for join into axioms, so we can pin down \ the crucial properties of the operation.\n\n", StyleBox["Axioms", FontWeight->"Bold"], " ", StyleBox["for Join", FontWeight->"Bold"], " (using append)\n\t", Cell[BoxData[ \(TraditionalForm\`L\ \[CirclePlus]\ {}\ \ = \ L\)]], ",\n\t", Cell[BoxData[ \(TraditionalForm\`L\ \[CirclePlus]\ app(K, a)\ = \ app(L\ \[CirclePlus]\ K, \ a\ \ )\)]], ".\n\nHad we chosen prepend as the fundamental operation, the second axiom \ would have to be rewritten correspondingly.\n" }], "Text", Evaluatable->False, AspectRatioFixed->True], Cell[TextData[{ StyleBox["Main Lemma:", FontWeight->"Bold"], " For any lists ", Cell[BoxData[ \(TraditionalForm\`L\)]], ", ", Cell[BoxData[ \(TraditionalForm\`K\)]], " and ", Cell[BoxData[ \(TraditionalForm\`M\)]], " we have:\n(1) ", Cell[BoxData[ FormBox[ RowBox[{\(L\ \[CirclePlus]\ {}\), " ", "=", " ", RowBox[{"L", " ", "=", " ", FormBox[ RowBox[{\({}\), " ", "\[CirclePlus]", " ", FormBox[\(\(L\)\(\ \)\), "TraditionalForm"]}], "TraditionalForm"]}]}], TraditionalForm]]], "\n(2) ", Cell[BoxData[ \(TraditionalForm\`L\ \[CirclePlus]\ \((\ K\[CirclePlus]\ M\ )\)\ = \ \((\ L\ \[CirclePlus]K\ )\)\ \[CirclePlus]\ M\)]] }], "Text"], Cell[TextData[{ "Proof: \nThe first equation is obvious from the definition, but even the \ second equation already requires an induction argument. The induction is \ here on the list B. \nBase Case: ", Cell[BoxData[ \(TraditionalForm\`L\ = \ {}\)]], ". \nThen, by the definition of join, ", Cell[BoxData[ \(TraditionalForm\`{}\ \[CirclePlus]\ L\ = \ \ \({}\ \[CirclePlus]\ {}\ = \ \ \({}\ \ = \ L\)\)\)]], ". \nInduction Step: ", Cell[BoxData[ \(TraditionalForm\`L\ = \ app(A, a)\)]], " \nSo, ", Cell[BoxData[ \(TraditionalForm\`a\)]], " is the last element in ", Cell[BoxData[ \(TraditionalForm\`L\)]], ". Then, by the definition of join and the IH\n\t", Cell[BoxData[ \(TraditionalForm\`{}\ \[CirclePlus]\ L\ = \ \({}\ \[CirclePlus]\ app(A, a)\ \( = \_IH\)\ \(app(\ {}\ \[CirclePlus]\ A, \ a)\ = \ \(app(A, a)\ = \ L\)\)\)\)]], ". \nThe second step is by Induction Hypothesis. Done with claim (1). " }], "Text", Evaluatable->False, AspectRatioFixed->True], Cell[TextData[{ "\nHow about part (2) of the lemma? Ugly, but induction on list ", Cell[BoxData[ \(TraditionalForm\`M\)]], " still works.\nBase Case: ", Cell[BoxData[ \(TraditionalForm\`M = {}\)]], ". Then \n", Cell[BoxData[ \(TraditionalForm\`\((\ K\ \[CirclePlus]\ L)\)\ \[CirclePlus]\ {}\ = \ \ \(K\ \[CirclePlus]L\ = \ K\ \[CirclePlus]\ \((\ L\ \[CirclePlus]\ {}\ )\)\)\)]], ".\nInduction Step: ", Cell[BoxData[ \(TraditionalForm\`M\ = \ app(A, a)\)]], ".\n", Cell[BoxData[ \(TraditionalForm\`\(\(\((K\ \[CirclePlus]\ L\ )\)\ \[CirclePlus]\ M\)\(\ \)\(=\)\)\)]], "\n", Cell[BoxData[ \(TraditionalForm\`\(\(\((\ K\ \[CirclePlus]\ L)\)\ \[CirclePlus]\ app(A, a)\)\(\ \)\(=\)\(\ \ \)\(app(\ \((K\ \[CirclePlus]L)\)\ \ \[CirclePlus]\ A, \ a)\ \( = \_IH\)\ \(\(app(\ K\ \[CirclePlus]\ \((L\ \[CirclePlus]\ A)\), \ a\ )\)\(\ \)\(=\)\)\)\(\ \ \)\)\)]], "\n", Cell[BoxData[ \(TraditionalForm\`\(\(K\ \[CirclePlus]\ app(\ L\[CirclePlus]\ A, a)\)\(\ \)\(=\)\(\ \)\(\(K\ \[CirclePlus]\ \((L\ \[CirclePlus]\ app(A, a))\)\)\(\ \ \)\(=\)\)\(\ \)\)\)]], "\n", Cell[BoxData[ \(TraditionalForm\`\(\(\ \)\(\((\ L\ \[CirclePlus]K\ )\)\ \[CirclePlus]\ M\)\)\)]], ".\nMake sure to check all the steps in the last argument. \nQED" }], "Text", Evaluatable->False, AspectRatioFixed->True] }, Closed]], Cell[CellGroupData[{ Cell[" Powers and Periods of Lists", "Subsection", Evaluatable->False, AspectRatioFixed->True, CellTags->"c:7"], Cell[CellGroupData[{ Cell["Powers, Periods, Roots", "Subsubsection", CellTags->"c:8"], Cell[TextData[{ "We can generate the so-called powers of a list by joining a list \ repeatedly to itself. More formally, we define ", Cell[BoxData[ \(TraditionalForm\`L\^n\)]], " as follows." }], "Text", Evaluatable->False, AspectRatioFixed->True], Cell[TextData[{ "Axioms for powers of lists\n\t", Cell[BoxData[ \(TraditionalForm\`L\^\(\(0\)\(\ \)\) = \ {}\)]], "\n\t", Cell[BoxData[ \(TraditionalForm\`L\^\(n + 1\)\ = \ \ L\^\(\(n\)\(\ \)\)\[CirclePlus]\ \ L\)]] }], "Text"], Cell[TextData[{ "Main Lemma\nFor any list ", Cell[BoxData[ \(TraditionalForm\`L\)]], " and natural numbers ", Cell[BoxData[ \(TraditionalForm\`n\)]], " and ", Cell[BoxData[ \(TraditionalForm\`m\)]], " we have: ", Cell[BoxData[ \(TraditionalForm\`L\^n\ \[CirclePlus]L\^m\ = \(L\^\(n + m\) = L\^m\[CirclePlus]\ L\^n\)\)]], ".\nProof: By induction on ", Cell[BoxData[ \(TraditionalForm\`m\)]], ". \[EmptySquare]\n" }], "Text"], Cell[TextData[{ "Definition\nLet ", Cell[BoxData[ \(TraditionalForm\`\(\(L\)\(\ \)\)\)]], " be a list, and ", Cell[BoxData[ \(TraditionalForm\`\(\(p\)\(\ \)\)\)]], "a positive integer. ", Cell[BoxData[ \(TraditionalForm\`\(\(p\)\(\ \)\)\)]], " is a ", StyleBox["period", FontColor->RGBColor[0, 0, 1]], " of L iff there is a list ", Cell[BoxData[ \(TraditionalForm\`K\)]], " of length ", Cell[BoxData[ \(TraditionalForm\`\(\(p\)\(\ \)\)\)]], "such that ", Cell[BoxData[ \(TraditionalForm\`\(\(\ \)\(L\ = \ K\^s\)\)\)]], " for some ", Cell[BoxData[ \(TraditionalForm\`s\)]], ". The least such ", Cell[BoxData[ \(TraditionalForm\`p\)]], " is ", StyleBox["the (least) period", FontColor->RGBColor[0, 0, 1]], " of ", Cell[BoxData[ \(TraditionalForm\`L\)]], ". The list ", Cell[BoxData[ \(TraditionalForm\`K\)]], " corresponding to the least period is the ", StyleBox["root", FontColor->RGBColor[0, 0, 1]], " of ", Cell[BoxData[ \(TraditionalForm\`L\)]], ". A list that is its own root is called ", StyleBox["primitive", FontColor->RGBColor[0, 0, 1]], ", and ", StyleBox["periodic", FontColor->RGBColor[0, 0, 1]], " otherwise. " }], "Text"], Cell[TextData[{ "If one thinks of a periodic list as a 0-indexed sequence ", Cell[BoxData[ \(TraditionalForm\`a\_0, \ a\_1, \ \[Ellipsis], \ a\_\(n - 1\)\)]], ", then a period ", Cell[BoxData[ \(TraditionalForm\`p > \ 0\)]], " is any number with the property ", Cell[BoxData[ \(TraditionalForm\`a\_i\ = \ a\_\(i + p\)\)]], ", where ", Cell[BoxData[ \(TraditionalForm\`0\ \[LessEqual] \ i\ < \ n - p\)]], ", or, equivalently, ", Cell[BoxData[ \(TraditionalForm\`a\_i = \ a\_\(i\ mod\ p\)\)]], ".\n\nSo, for example, the list ", Cell[BoxData[ \(TraditionalForm\`{\ a, \ b, \ b, \ b\ }\)]], " is primitive, but ", Cell[BoxData[ \(TraditionalForm\`{a, \ b, \ a, \ b, \ a, ... , \ a, \ b}\)]], " is not. In fact, the second list has root ", Cell[BoxData[ \(TraditionalForm\`{a, \ b}\)]], ". " }], "Text"], Cell[TextData[{ "If two lists ", Cell[BoxData[ \(TraditionalForm\`K\)]], " and ", Cell[BoxData[ \(TraditionalForm\`\(\(L\)\(\ \)\)\)]], " have the same root, then ", Cell[BoxData[ \(TraditionalForm\`L\ \[CirclePlus]\ K\)]], " must be the same as ", Cell[BoxData[ \(TraditionalForm\`K\[CirclePlus]\ L\)]], ". One says that ", Cell[BoxData[ \(TraditionalForm\`K\)]], " and ", Cell[BoxData[ \(TraditionalForm\`L\)]], " ", StyleBox["commute", FontColor->RGBColor[0, 0, 1]], " with respect to join. The next theorem shows that this is the only case \ in which lists commute. \n\nTheorem\n", Cell[BoxData[ \(TraditionalForm\`L\ \[CirclePlus]K\ = K\[CirclePlus]\ L\)]], " implies ", Cell[BoxData[ \(TraditionalForm\`root(L)\ = \ root(K)\)]], ".\nProof.\nThe proof is by strong induction on ", Cell[BoxData[ \(TraditionalForm\`n\ = \ \(\(\(|\)\(L\)\(|\)\(\ \)\(+\ \ \(\(|\)\(K\)\(|\)\)\)\)\ = \ \(\(|\)\(L\ \[CirclePlus]\ K\)\(|\)\)\)\)]], ". Suppose the claim holds for all ", Cell[BoxData[ \(TraditionalForm\`m\ < \ n\)]], " and consider two lists with total length ", Cell[BoxData[ \(TraditionalForm\`n\)]], ".\nIt is an absolute must to draw a picture of ", Cell[BoxData[ \(TraditionalForm\`L\ \[CirclePlus]\ K\)]], " and ", Cell[BoxData[ \(TraditionalForm\`K\[CirclePlus]\ L\)]], ". Don't ask how long it took to get the picture below to look right. " }], "Text"], Cell[GraphicsData["PostScript", "\<\ %! %%Creator: Mathematica %%AspectRatio: .33333 MathPictureStart /Mabs { Mgmatrix idtransform Mtmatrix dtransform } bind def /Mabsadd { Mabs 3 -1 roll add 3 1 roll add exch } bind def %% Graphics /Courier findfont 10 scalefont setfont % Scaling calculations 0.0238095 0.31746 0.166667 0.15873 [ [ 0 0 0 0 ] [ 1 .33333 0 0 ] ] MathScale % Start of Graphics 1 setlinecap 1 setlinejoin newpath 0 0 m 1 0 L 1 .33333 L 0 .33333 L closepath clip newpath 1 1 0 r .02381 .16667 m .02381 .3254 L .65873 .3254 L .65873 .16667 L F .34127 .00794 m .34127 .16667 L .97619 .16667 L .97619 .00794 L F .678 .847 .902 r .65873 .16667 m .65873 .3254 L .97619 .3254 L .97619 .16667 L F .02381 .00794 m .02381 .16667 L .34127 .16667 L .34127 .00794 L F 0 g .5 Mabswid [ ] 0 setdash .02381 .00794 m .02381 .3254 L .97619 .3254 L .97619 .00794 L .02381 .00794 L s .65873 .16667 m .65873 .3254 L s .02381 .16667 m .97619 .16667 L s .34127 .00794 m .34127 .16667 L s gsave .34127 .24603 -70.5 -13.5 Mabsadd m 1 1 Mabs scale currentpoint translate 0 27 translate 1 -1 scale 63.000000 19.000000 moveto /Courier findfont 24.000000 scalefont [1 0 0 -1 0 0 ] makefont setfont 0.000000 0.000000 0.000000 setrgbcolor 0.000000 0.000000 rmoveto 63.000000 19.000000 moveto /Courier findfont 24.000000 scalefont [1 0 0 -1 0 0 ] makefont setfont 0.000000 0.000000 0.000000 setrgbcolor (L) show 78.000000 19.000000 moveto /Courier findfont 24.000000 scalefont [1 0 0 -1 0 0 ] makefont setfont 0.000000 0.000000 0.000000 setrgbcolor 0.000000 0.000000 rmoveto 1.000000 setlinewidth grestore gsave .81746 .24603 -70.5 -13.5 Mabsadd m 1 1 Mabs scale currentpoint translate 0 27 translate 1 -1 scale 63.000000 19.000000 moveto /Courier findfont 24.000000 scalefont [1 0 0 -1 0 0 ] makefont setfont 0.000000 0.000000 0.000000 setrgbcolor 0.000000 0.000000 rmoveto 63.000000 19.000000 moveto /Courier findfont 24.000000 scalefont [1 0 0 -1 0 0 ] makefont setfont 0.000000 0.000000 0.000000 setrgbcolor (K) show 78.000000 19.000000 moveto /Courier findfont 24.000000 scalefont [1 0 0 -1 0 0 ] makefont setfont 0.000000 0.000000 0.000000 setrgbcolor 0.000000 0.000000 rmoveto 1.000000 setlinewidth grestore gsave .65873 .0873 -70.5 -13.5 Mabsadd m 1 1 Mabs scale currentpoint translate 0 27 translate 1 -1 scale 63.000000 19.000000 moveto /Courier findfont 24.000000 scalefont [1 0 0 -1 0 0 ] makefont setfont 0.000000 0.000000 0.000000 setrgbcolor 0.000000 0.000000 rmoveto 63.000000 19.000000 moveto /Courier findfont 24.000000 scalefont [1 0 0 -1 0 0 ] makefont setfont 0.000000 0.000000 0.000000 setrgbcolor (L) show 78.000000 19.000000 moveto /Courier findfont 24.000000 scalefont [1 0 0 -1 0 0 ] makefont setfont 0.000000 0.000000 0.000000 setrgbcolor 0.000000 0.000000 rmoveto 1.000000 setlinewidth grestore gsave .18254 .0873 -70.5 -13.5 Mabsadd m 1 1 Mabs scale currentpoint translate 0 27 translate 1 -1 scale 63.000000 19.000000 moveto /Courier findfont 24.000000 scalefont [1 0 0 -1 0 0 ] makefont setfont 0.000000 0.000000 0.000000 setrgbcolor 0.000000 0.000000 rmoveto 63.000000 19.000000 moveto /Courier findfont 24.000000 scalefont [1 0 0 -1 0 0 ] makefont setfont 0.000000 0.000000 0.000000 setrgbcolor (K) show 78.000000 19.000000 moveto /Courier findfont 24.000000 scalefont [1 0 0 -1 0 0 ] makefont setfont 0.000000 0.000000 0.000000 setrgbcolor 0.000000 0.000000 rmoveto 1.000000 setlinewidth grestore % End of Graphics MathPictureEnd \ \>"], "Graphics", ImageSize->{288, 95.875}, ImageMargins->{{56.25, 0}, {0, 0}}, ImageRegion->{{0, 1}, {0, 1}}, ImageCache->GraphicsData["Bitmap", "\<\ CF5dJ6E]HGAYHf4PAg9QL6QYHgo`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0 cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0 U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0 cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0 U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0 cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0 U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0 cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0 U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0000003o0?oo 0100ool000<000000?ooo`3oool02P3oool000/0oooo08T000000o`2Db/d0cLko09C:c@3=c_l0 U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0 cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0 U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0 cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0 U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0 cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0 U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0 cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0 U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0000003o0?oo0100ool000<000000?ooo`3oool02P3o ool000/0oooo08T000000o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0 U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0 cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0 U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0 cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0 U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0 cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0 U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0 cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0 U<[=0000003o0?oo0100ool000<000000?ooo`3oool02P3oool000/0oooo08T000000o`2Db/d0 cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0 U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0 cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0 U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0 cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0 U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0 cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0 U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0 cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0000003o0?oo0100ool000<00000 0?ooo`3oool02P3oool000/0oooo08T000000o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0 cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0 U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0 cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0 U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0 cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0 U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0 cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0 U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0 cLko09C:c@3=c_l0U<[=0000003o0?oo0100ool000<000000?ooo`3oool02P3oool000/0oooo08T0 00000o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0 cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0 U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0 cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0 U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0 cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0 U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0 cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0 U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0000003o0?oo 0100ool000<000000?ooo`3oool02P3oool000/0oooo08T000000o`2Db/d0cLko09C:c@3=c_l0 U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0 cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0 U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0 cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0 U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0 cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0 U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0 cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0 U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0000003o0?oo0100ool000<000000?ooo`3oool02P3o ool000/0oooo08T000000o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0 U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0 cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0 U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0 cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0 U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0 cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0 U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0 cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0 U<[=0000003o0?oo0100ool000<000000?ooo`3oool02P3oool000/0oooo08T000000o`2Db/d0 cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0 U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0 cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0 U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0 cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0 U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0 cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0 U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0 cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0000003o0?oo0100ool000<00000 0?ooo`3oool02P3oool000/0oooo08T000000o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0 cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0 U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0 cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0 U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0 cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0 U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0 cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0 U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0 cLko09C:c@3=c_l0U<[=0000003o0?oo0100ool000<000000?ooo`3oool02P3oool000/0oooo08T0 00000o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0 cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0 U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0 cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0 U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0 cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0 U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0 cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0 U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0000003o0?oo 0100ool000<000000?ooo`3oool02P3oool000/0oooo08T000000o`2Db/d0cLko09C:c@3=c_l0 U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0 cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0 U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0 cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0 U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0 cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0 U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0 cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0 U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0000003o0?oo0100ool000<000000?ooo`3oool02P3o ool000/0oooo08T000000o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0 U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0 cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0 U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0 cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0 U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0 cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0 U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0 cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0 U<[=0000003o0?oo0100ool000<000000?ooo`3oool02P3oool000/0oooo03/000000o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0 cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0 U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0 cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0 200000001`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d01@000000>P2Db/d0cLko09C:c@3=c_l0 U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0 cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0 U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0 cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@00001n0?oo01<00000OP3oo`000`000000oooo 0?ooo`0:0?ooo`002`3oool0?P000000cOoo09c:c@3=ool0W<[=0o`2Db/d0cLko09C:c@3=c_l0U<[= 0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko 09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[= 0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko 09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@80000000T0cLko09C:c@3=c_l0U<[=0o`2Db/d0 cLko09C:c@3=c_l00P000000?P2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0 U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0 cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0 U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0 cLko09C:c@3=c_l0U<[=0o`2Db/d00000PP3oo`02000000/0ool00P00001n0?oo00030000003o ool0oooo00X0oooo000;0?ooo`0n0000003=ool0W<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2D b/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3= c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2D b/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3= c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0P000000203=c_l0U<[=0o`2Db/d0cLko09C: c@3=c_l0U<[=0P000000?`3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko 09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[= 0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko 09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[= 0o`2Db/d0cLko09C:c@3=c_l0U<[=000000220?oo008000002`3oo`02000007h0ool000<00000 0?ooo`3oool02P3oool000/0oooo03h000000o`2Db/d0cLko 09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[= 0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko 09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[= 0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d2000000060o`2Db/d0cLko09C:c@3=c_l0 U<[=0`000000@02Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2D b/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3= c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2D b/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3= c_l0U<[=0o`2Db/d0cLko09C:c@0000220?oo008000002`3oo`02000007h0ool000<000000?oo o`3oool02P3oool000/0oooo03h000000o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C: c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0 o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C: c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0 o`2Db/d0cLko09C:c@3=c_l0U<[=100000000`3=c_l0U<[=000000020000001209C:c@3=c_l0U<[= 0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko 09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[= 0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko 09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[= 0o`2Db/d00000PP3oo`02000008/0ool000<000000?ooo`3oool02P3oool000/0oooo03h00000 0o`2Db/d0cLko 09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[= 0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko 09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[= 0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d2000000190o`00000000000000003=c_l0 U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0 cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0 U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0 cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0 U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=000000220?oo00800000R`3oo`000`000000oooo0?oo o`0:0?ooo`002`3oool0?P000000cOoo09c:c@3=ool0W<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0 U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0 cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0 U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0 cLko09C:c@3=c_l0U<[=0P000000103=c_l0U<[=0o`2Db/d2000000130o`2Db/d0cLko09C: c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0 o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C: c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0 o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C: c@3=c_l0U<[=000000220?oo00800000R`3oo`000`000000oooo0?ooo`0:0?ooo`002`3oool0?P00 0000cOoo09c:c@3=ool0W<[=0 o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C: c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0 o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C: c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0P00 00001P3=c_l0U<[=0o`2Db/d0cLko09C:c@<000000400U<[=0o`2Db/d0cLko09C:c@3=c_l0 U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0 cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0 U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0 cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d00000PP3oo`020000 08/0ool000<000000?ooo`3oool02P3oool000/0oooo03h000000o`2Db/d0cLko09C:c@3=c_l0 U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0 cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0 U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0 cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@80000000P0cLko09C:c@3=c_l0U<[=0o`2D b/d0cLko09C:c@<0000003h0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C: c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0 o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C: c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0 o`2Db/d0cLko09C:c@3=c_l0U<[=00000880ool00P00002;0?oo00030000003oool0oooo00X0oooo 000;0?ooo`0n0000003=ool0W<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C: c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0 o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C: c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l020000000 102Db/d0cLko09C:c@3=c_l70000000k0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko 09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[= 0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko 09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[= 0o`2Db/d0cLko09C:c@000000OP3oo`0:000008L0ool000<000000?ooo`3oool02P3oool000/0 oooo03/000000o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C: c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0 o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C: c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0 o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C: c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0 o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C: c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0 o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C: c@3=c_l0U<[=0o`2Db/d000000?l0ool0403oo`000`000000oooo0?ooo`0:0?ooo`002`3oool0 R@000000cOoo09c:c@3=ool0W<[=0 o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C: c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0 o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C: c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0 o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C: c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0 o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C: c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0 o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d000000?l0 ool0403oo`000`000000oooo0?ooo`0:0?ooo`002`3oool0R@000000cOoo09c:c@3=ool0W<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0 o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C: c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0 o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C: c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0 o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C: c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0 o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C: c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0 o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d000000?l0ool0403oo`000`000000oooo0?ooo`0: 0?ooo`002`3oool0R@000000cOoo09c:c@3=ool0W<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0 o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C: c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0 o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C: c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0 o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C: c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0 o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C: c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0 o`2Db/d000000?l0ool0403oo`000`000000oooo0?ooo`0:0?ooo`002`3oool0R@000000cOoo09c: c@3=ool0W<[=0o`2Db/d0cLko09C: c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0 o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C: c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0 o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C: c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0 o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C: c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0 o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C: c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d000000?l0ool0403oo`000`00 0000oooo0?ooo`0:0?ooo`002`3oool0R@000000cOoo09c:c@3=ool0W<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C: c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0 o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C: c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0 o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C: c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0 o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C: c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0 o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C: c@3=c_l0U<[=0o`2Db/d000000?l0ool0403oo`000`000000oooo0?ooo`0:0?ooo`002`3oool0 R@000000cOoo09c:c@3=ool0W<[=0 o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C: c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0 o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C: c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0 o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C: c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0 o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C: c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0 o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d000000?l0 ool0403oo`000`000000oooo0?ooo`0:0?ooo`002`3oool0R@000000cOoo09c:c@3=ool0W<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0 o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C: c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0 o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C: c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0 o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C: c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0 o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C: c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0 o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d000000?l0ool0403oo`000`000000oooo0?ooo`0: 0?ooo`002`3oool0R@000000cOoo09c:c@3=ool0W<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0 o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C: c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0 o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C: c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0 o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C: c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0 o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C: c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0 o`2Db/d000000?l0ool0403oo`000`000000oooo0?ooo`0:0?ooo`002`3oool0R@000000cOoo09c: c@3=ool0W<[=0o`2Db/d0cLko09C: c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0 o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C: c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0 o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C: c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0 o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C: c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0 o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C: c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d000000?l0ool0403oo`000`00 0000oooo0?ooo`0:0?ooo`002`3oool0R@000000cOoo09c:c@3=ool0W<[=00?oo0029 0000003=ool0W<[=00?oo00290000002Db/d0cLko 09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[= 0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko 09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[= 0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko 09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[= 0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko 09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[= 0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko 09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@000000303o ool000/0oooo00<000000?oo003oo`00o`3oo`0>0?oo00290000003=ool0W<[=00?oo00290000002Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko 09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[= 0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko 09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[= 0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko 09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[= 0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko 09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[= 0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko 09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@000000303oool000/0oooo00<000000?oo003oo`00 o`3oo`0>0?oo00290000003=ool0W<[=00?oo0029 0000002Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko 09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[= 0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko 09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[= 0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko 09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[= 0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko 09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[= 0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko 09C:c@000000303oool000/0oooo00<000000?oo003oo`00o`3oo`0>0?oo00290000003=ool0W<[= 00?oo00290000002Db/d0cLko09C:c@3=c_l0U<[= 0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko 09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[= 0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko 09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[= 0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko 09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[= 0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko 09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[= 0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@000000303oool000/0oooo00<0 00000?oo003oo`00o`3oo`0>0?oo00290000003=ool0W<[=00?oo00290000002Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[= 0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko 09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[= 0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko 09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[= 0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko 09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[= 0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko 09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[= 0o`2Db/d0cLko09C:c@000000303oool000/0oooo00<000000?oo003oo`00o`3oo`0>0?oo0029 0000003=ool0W<[=00?oo00290000002Db/d0cLko 09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[= 0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko 09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[= 0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko 09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[= 0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko 09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[= 0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko 09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@000000303o ool000/0oooo00<000000?oo003oo`00o`3oo`0>0?oo00290000003=ool0W<[=00?oo00290000002Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko 09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[= 0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko 09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[= 0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko 09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[= 0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko 09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[= 0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko 09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@000000303oool000/0oooo00<000000?oo003oo`00 o`3oo`0>0?oo00290000003=ool0W<[=00?oo0029 0000002Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko 09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[= 0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko 09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[= 0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko 09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[= 0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko 09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[= 0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko 09C:c@000000303oool000/0oooo00<000000?oo003oo`00o`3oo`0>0?oo00290000003=ool0W<[= 00?oo00290000002Db/d0cLko09C:c@3=c_l0U<[= 0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko 09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[= 0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko 09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[= 0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko 09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[= 0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko 09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[= 0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@000000303oool000/0oooo00<0 00000?oo003oo`00o`3oo`0>0?oo00290000003=ool0W<[=00?oo00290000002Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[= 0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko 09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[= 0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko 09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[= 0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko 09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[= 0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko 09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[= 0o`2Db/d0cLko09C:c@000000303oool000/0oooo00<000000?oo003oo`00o`3oo`0>0?oo0029 0000003=ool0W<[=00?oo00290000002Db/d0cLko 09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[= 0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko 09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[= 0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko 09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[= 0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko 09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[= 0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko 09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@000000303o ool000/0oooo00<000000?oo003oo`00o`3oo`0>0?oo00290000003=ool0W<[=00?oo00290000002Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko 09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[= 0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko 09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[= 0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko 09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[= 0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko 09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[= 0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko 09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@000000303oool000/0oooo00<000000?oo003oo`00 o`3oo`0>0?oo00290000003=ool0W<[=00?oo0029 0000002Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko 09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[= 0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko 09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[= 0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko 09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[= 0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko 09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[= 0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko 09C:c@000000303oool000/0oooo00<000000?oo003oo`00O03oo`0C000007h0ool003/000000o`2Db/d0cLko09C:c@3=c_l0U<[=0 o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C: c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0 o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C: c@3=c_l0200000001`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d01@000000>P2Db/d0cLko09C: c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0 o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C: c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0 o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@00000<0?ooo`002`3oool00`000000 ool00?oo00200?oo008000002P3oo`03000007h0ool003h000000o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko 09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[= 0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko 09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d2000000090o`2Db/d0 cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko0080000003h0U<[=0o`2Db/d0cLko09C:c@3=c_l0 U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0 cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0 U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0 cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=000000`0oooo000;0?ooo`030000 003oo`00ool00800ool00P00000;0?oo00800000OP3oo`00?P000000cOoo09c:c@3=ool0W<[=0o`2D b/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3= c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2D b/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3= c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@80000000P0cLko09C: c@3=c_l0U<[=0o`2Db/d0cLko09C:c@80000003l0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko 09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[= 0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko 09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[= 0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@000000303oool000/0oooo00<0 00000?oo003oo`00P03oo`02000000/0ool00P00001n0?oo000n0000003=ool0W<[=0o`2Db/d0cLko 09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[= 0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko 09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[= 0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0P0000001P3=c_l0 U<[=0o`2Db/d0cLko09C:c@<000000400U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2D b/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3= c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2D b/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3= c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d00000303oool000/0oooo00<00000 0?oo003oo`00P03oo`02000000/0ool00P00001n0?oo000n0000003=ool0W<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0 cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0 U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0 cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0 U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=100000000`3=c_l0U<[=000000020000001209C:c@3= c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2D b/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3= c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2D b/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3= c_l0U<[=0o`2Db/d00000303oool000/0oooo00<000000?oo003oo`00P03oo`02000008/0ool0 03h000000o`2D b/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3= c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2D b/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3= c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d2000000190o`00000000000000 003=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0 o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C: c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0 o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C: c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0000000<0?ooo`002`3oool00`000000ool0 0?oo00200?oo00800000R`3oo`00?P000000cOoo09c:c@3=ool0W<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C: c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0 o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C: c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0 o`2Db/d0cLko09C:c@3=c_l0U<[=0P000000103=c_l0U<[=0o`2Db/d2000000130o`2Db/d0 cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0 U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0 cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0 U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0 cLko09C:c@3=c_l0U<[=0000000<0?ooo`002`3oool00`000000ool00?oo00200?oo00800000R`3o o`00?P000000cOoo09c:c@3=ool0W<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0 cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0 U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0 cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0 U<[=0P0000001P3=c_l0U<[=0o`2Db/d0cLko09C:c@<000000400U<[=0o`2Db/d0cLko09C: c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0 o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C: c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0 o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d00000303o ool000/0oooo00<000000?oo003oo`00P03oo`02000008/0ool003h000000o`2Db/d0cLko09C: c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0 o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C: c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0 o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@80000000P0cLko09C:c@3=c_l0U<[= 0o`2Db/d0cLko09C:c@<0000003h0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0 cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0 U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0 cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0 U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=000000`0oooo000;0?ooo`030000003oo`00ool00800 ool00P00002;0?oo000n0000003=ool0W<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0 cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0 U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0 cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0 20000000102Db/d0cLko09C:c@3=c_l70000000k0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2D b/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3= c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2D b/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3= c_l0U<[=0o`2Db/d0cLko09C:c@000000303oool000/0oooo00<000000?oo003oo`00O03oo`0: 000008L0ool003/000000o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2D b/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3= c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2D b/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3= c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2D b/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3= c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2D b/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3= c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2D b/d0cLko09C:c@3=c_l0U<[=0000000<0?ooo`002`3oool00`000000ool00?oo003o0?oo00h0ool0 08T000000o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2D b/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3= c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2D b/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3= c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2D b/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3= c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2D b/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3= c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0000000< 0?ooo`002`3oool00`000000ool00?oo003o0?oo00h0ool008T000000o`2Db/d0cLko09C:c@3= c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2D b/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3= c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2D b/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3= c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2D b/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3= c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2D b/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3= c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0000000<0?ooo`002`3oool00`000000ool00?oo 003o0?oo00h0ool008T000000o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3= c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2D b/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3= c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2D b/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3= c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2D b/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3= c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2D b/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3= c_l0U<[=0000000<0?ooo`002`3oool00`000000ool00?oo003o0?oo00h0ool008T000000o`2D b/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3= c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2D b/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3= c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2D b/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3= c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2D b/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3= c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2D b/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0000000<0?ooo`002`3oool0 0`000000ool00?oo003o0?oo00h0ool008T000000o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2D b/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3= c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2D b/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3= c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2D b/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3= c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2D b/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3= c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2D b/d0cLko09C:c@3=c_l0U<[=0000000<0?ooo`002`3oool00`000000ool00?oo003o0?oo00h0ool0 08T000000o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2D b/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3= c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2D b/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3= c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2D b/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3= c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2D b/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3= c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0000000< 0?ooo`002`3oool00`000000ool00?oo003o0?oo00h0ool008T000000o`2Db/d0cLko09C:c@3= c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2D b/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3= c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2D b/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3= c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2D b/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3= c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2D b/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3= c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0000000<0?ooo`002`3oool00`000000ool00?oo 003o0?oo00h0ool008T000000o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3= c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2D b/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3= c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2D b/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3= c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2D b/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3= c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2D b/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3= c_l0U<[=0000000<0?ooo`002`3oool00`000000ool00?oo003o0?oo00h0ool008T000000o`2D b/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3= c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2D b/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3= c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2D b/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3= c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2D b/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3= c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0o`2D b/d0cLko09C:c@3=c_l0U<[=0o`2Db/d0cLko09C:c@3=c_l0U<[=0000000<0?ooo`002`3oool0 0`000000ool00?oo003o0?oo00h0ool008T000000"], ImageRangeCache->{{{0, 431}, {142.812, 0}} -> {0, -1, 0, 0}}], Cell[TextData[{ "In the picture, ", Cell[BoxData[ \(TraditionalForm\`L\)]], " is longer than ", Cell[BoxData[ \(TraditionalForm\`K\)]], ", but one may easily convince oneself that our argument works fine in the \ other cases. Since the join on top is supposed to be the same as the join at \ the bottom, it follows that ", Cell[BoxData[ \(TraditionalForm\`L\ = \ K\ \[CirclePlus]\ L\_0\)]], ". But then ", Cell[BoxData[ \(TraditionalForm\`L\_0\ \[CirclePlus]K\ = K\[CirclePlus]\ L\_0\)]], " and ", Cell[BoxData[ \(TraditionalForm\`\(\(|\)\(K\[CirclePlus]\ L\_0\)\(|\)\(\ \)\(\(<\)\(\ \)\(n\)\)\)\)]], ". Therfore, ", Cell[BoxData[ \(TraditionalForm\`K\)]], " and ", Cell[BoxData[ \(TraditionalForm\`L\_0\)]], " ", " have a common root, say, ", Cell[BoxData[ \(TraditionalForm\`M\)]], ". But then ", Cell[BoxData[ \(TraditionalForm\`M\)]], " is also the root of ", Cell[BoxData[ \(TraditionalForm\`L\)]], ", and we are done. \n\[EmptySquare]" }], "Text"], Cell[TextData[{ StyleBox["Corollary:", FontWeight->"Bold"], " For all ", Cell[BoxData[ \(TraditionalForm\`n, m\ > \ 0\)]], ": ", Cell[BoxData[ \(TraditionalForm\`L\^n\ = \ K\^m\)]], " implies ", Cell[BoxData[ \(TraditionalForm\`root(L)\ = \ root(K)\)]], "." }], "Text"], Cell[TextData[{ StyleBox["Lemma", FontWeight->"Bold"], " : If ", Cell[BoxData[ \(TraditionalForm\`p\)]], " and ", Cell[BoxData[ \(TraditionalForm\`q\)]], " are both periods of ", Cell[BoxData[ \(TraditionalForm\`L\)]], ", then ", Cell[BoxData[ \(TraditionalForm\`gcd(p, q)\)]], " is also a period of ", Cell[BoxData[ \(TraditionalForm\`L\)]], "." }], "Text"] }, Closed]], Cell[CellGroupData[{ Cell["Counting Primitive Lists", "Subsubsection", CellTags->"c:9"], Cell[TextData[{ "Suppose we consider lists over some fixed, finite set of possible \ elements, say, ", Cell[BoxData[ \(TraditionalForm\`A\ = \ {0, 1, \[Ellipsis], k - 1}\)]], ". How many primitive lists of length ", Cell[BoxData[ \(TraditionalForm\`n\)]], " are there? Is there an easy way to generate them? \n\nNote that a list of \ length ", Cell[BoxData[ \(TraditionalForm\`n\)]], " that fails to be primitive must have a root of length ", Cell[BoxData[ \(TraditionalForm\`d\ < \ n\)]], ", and the root itself is primitive. Moreover, we must have ", Cell[BoxData[ \(TraditionalForm\`d\ | \ n\)]], ". Also, for any proper divisor ", Cell[BoxData[ \(TraditionalForm\`d\)]], " of ", Cell[BoxData[ \(TraditionalForm\`n\)]], " and any primitive list ", Cell[BoxData[ \(TraditionalForm\`K\)]], " of length ", Cell[BoxData[ \(TraditionalForm\`d\)]], " we can construct exactly one list of length ", Cell[BoxData[ \(TraditionalForm\`n\)]], " that fails to be primitive: ", Cell[BoxData[ \(TraditionalForm\`L\ = \ K\^\(n\/d\)\)]], ". It follows that for ", Cell[BoxData[ \(TraditionalForm\`n\)]], " prime there are ", Cell[BoxData[ \(TraditionalForm\`k\^n - \ k\)]], " primitive lists of length ", Cell[BoxData[ \(TraditionalForm\`n\)]], ". In general, the number ", Cell[BoxData[ \(TraditionalForm\`p\_n\)]], " of primitive lists of length ", Cell[BoxData[ \(TraditionalForm\`n\)]], " satisfies the following equation:\n\t\t", Cell[BoxData[ \(TraditionalForm\`p\_n\ = \ k\^n\ - \ \ \[Sum]\_\(\(d | n\ &\)\ d < n\)\ p\_d\)]], ".\nNote that the summation is over all proper divisors of ", Cell[BoxData[ \(TraditionalForm\`n\)]], ". In other words, \n \t\t", Cell[BoxData[ FormBox[ RowBox[{" ", FormBox[\(k\^n = \ \ \[Sum]\_\(\(d\)\(|\)\(n\)\(\ \)\)\ p\_d\), "TraditionalForm"]}], TraditionalForm]]], "\n where the summation is now over all divisors, including ", Cell[BoxData[ \(TraditionalForm\`n\)]], ". The second equation may seem not particularly helpful, but it actually \ provides an immediate solution to our first question. There is a general \ result, called M\[ODoubleDot]bius inversion, that allows one to solve \ equations of the form \n \t\t", Cell[BoxData[ FormBox[ RowBox[{" ", FormBox[\(f(n) = \ \ \[Sum]\_\(\(d\)\(|\)\(n\)\(\ \)\)\ g(d)\), "TraditionalForm"]}], TraditionalForm]]], "\n in the sense that one can express ", Cell[BoxData[ \(TraditionalForm\`g\)]], " in terms of ", Cell[BoxData[ \(TraditionalForm\`f\)]], ". More precisely, \n \t\t", Cell[BoxData[ FormBox[ RowBox[{" ", FormBox[\(g( n) = \ \ \[Sum]\_\(\(d\)\(|\)\(n\)\(\ \)\)\ \(\[Mu]( n\/d)\)\ \ \(f(d)\)\), "TraditionalForm"]}], TraditionalForm]]], "\n where ", Cell[BoxData[ \(TraditionalForm\`\[Mu]\)]], " is the M\[ODoubleDot]bius function, which is defined as follows:\n \t\t\ ", Cell[BoxData[ \(TraditionalForm\`\[Mu](n)\ = \ 0\)]], " \t\tif ", Cell[BoxData[ \(TraditionalForm\`n\)]], " contains a square,\n \t\t", Cell[BoxData[ \(TraditionalForm\`\[Mu](n)\ = \ \((\(-1\))\)\^m\)]], " \t\tif ", Cell[BoxData[ \(TraditionalForm\`n\)]], " is square-free, and has ", Cell[BoxData[ \(TraditionalForm\`m\)]], " distinct prime factors.\nWe will forgoe the opportunity to prove the \ correctness of M\[ODoubleDot]bius inversion. At any rate, the \ M\[ODoubleDot]bius function is very important in number theory and \ combinatorics, and is therefore built-in. " }], "Text"], Cell[BoxData[ \(\({Range[20], MoebiusMu[\ Range[20]]}\ \ // \ Thread\)\ // \ TableForm\)], "Input"], Cell[TextData[{ "Coming back to primitive lists, it follows that \n\n\t", Cell[BoxData[ \(TraditionalForm\`p\_n\ \ = \ \ \[Sum]\_\(d | n\)\ \(\[Mu]( n\/d)\)\ k\^d\)]], ".\n\t\nWe can easily compute some values:" }], "Text"], Cell[BoxData[ \(\(prim[n_, k_]\ := \ With[\ {D\ = \ Divisors[n]}, \n\t\t\t\tMoebiusMu[ n/D]\ . \ \((k^D)\)\ ];\)\)], "Input"], Cell[BoxData[{ \(\(prim[\ #, \ 2\ ] &\)\ /@ \ Range[10]\), "\n", \(prim[\ 20, \ 2]/2\^20\ // \ N\)}], "Input"], Cell[TextData[{ "Note that out of the ", Cell[BoxData[ \(TraditionalForm\`\(\(2\^10\)\(=\)\(\ \)\(1024\)\(\ \)\)\)]], " binary lists of length 10, a whole 990 are primitive, and for lists of \ length 20 less then one promille is periodic. \n\nGenerating primitive lists \ by recursion is easy keeping the equation above in mind. Note that the number \ of all lists grows exponentially, so the following must not be used for large \ values of ", Cell[BoxData[ \(TraditionalForm\`n\)]], " and ", Cell[BoxData[ \(TraditionalForm\`k\)]], ". " }], "Text"], Cell[BoxData[{ \(primL[1, k_]\ := \ Table[{i}, {i, 0, k - 1}]\), "\n", \(primL[n_, k_]\ := \ \n Module[\ {pp}, \n\t\t\tpp\ = Flatten[\ \(primL[#, k] &\)\ /@ \ Drop[Divisors[n], \(-1\)], \ 1]; \n\t\tpower[LL_List]\ := \ Join @@ Table[ LL, {n/Length[LL]}]; \n\t\tComplement[\ \ KPermutationsR[k, n], \ power\ /@ \ pp]\n]\)}], "Input"], Cell[BoxData[{ \(prim[4, 2]\), "\n", \(primL[4, \ 2\ ]\ \), "\n", \(%\ // \ Length\)}], "Input"] }, Closed]], Cell[CellGroupData[{ Cell["Weak Periods", "Subsubsection", CellTags->"c:10"], Cell[TextData[{ "Definition\nLet ", Cell[BoxData[ \(TraditionalForm\`\(\(L\)\(\ \)\)\)]], " be a list, and ", Cell[BoxData[ \(TraditionalForm\`\(\(p\)\(\ \)\)\)]], "a positive integer. ", Cell[BoxData[ \(TraditionalForm\`\(\(p\)\(\ \)\)\)]], " is a weak period of L iff there is a list ", Cell[BoxData[ \(TraditionalForm\`K\)]], " of length ", Cell[BoxData[ \(TraditionalForm\`\(\(p\)\(\ \)\)\)]], " such that ", Cell[BoxData[ \(TraditionalForm\`\(\(\ \)\(L\ = \ K\^\(\(s\)\(\ \)\)\[CirclePlus]\ M\)\)\)]], " for some ", Cell[BoxData[ \(TraditionalForm\`s\)]], " and ", Cell[BoxData[ \(TraditionalForm\`M\)]], " has length at most ", Cell[BoxData[ \(TraditionalForm\`p\)]], ". The least such ", Cell[BoxData[ \(TraditionalForm\`p\)]], " is the (least) weak period of ", Cell[BoxData[ \(TraditionalForm\`L\)]], ". " }], "Text"], Cell[TextData[{ StyleBox["Lemma:", FontWeight->"Bold"], "\nIf ", Cell[BoxData[ \(TraditionalForm\`p\)]], " and ", Cell[BoxData[ \(TraditionalForm\`q\)]], " are both weak periods of ", Cell[BoxData[ \(TraditionalForm\`L\)]], ", and ", Cell[BoxData[ \(TraditionalForm\`\(\(p\ + \ q\)\(\ \)\(\[LessEqual]\)\)\ | L | \(+\ \(gcd(p, q)\)\)\)]], ", then ", Cell[BoxData[ \(TraditionalForm\`gcd(p, q)\)]], " is also a weak period of ", Cell[BoxData[ \(TraditionalForm\`L\)]], ".\n" }], "Text"] }, Closed]] }, Closed]], Cell[CellGroupData[{ Cell[" Reversing Lists", "Subsection", Evaluatable->False, AspectRatioFixed->True, CellTags->"c:11"], Cell[TextData[{ "Recall the definitions for reversal (from right to left), and left \ reversal. We have written the definitions here without the patterns, but you \ can check that this is really the same as our original definitions. We will \ write ", Cell[BoxData[ \(TraditionalForm\`pre(L, x)\)]], " for the prepend operation. " }], "Text", Evaluatable->False, AspectRatioFixed->True], Cell[TextData[{ "\n", StyleBox["Axioms for Reversal", FontWeight->"Bold"], " (from right)\n\t", Cell[BoxData[ \(TraditionalForm\`rev(\ {}\ )\ = \ {}\)]], "\n\t", Cell[BoxData[ \(TraditionalForm\`rev(\ app(L, x)\ )\ = \ pre(\ rev(L), \ x\ )\)]], "\n\nAlternatively, we could remove the first element an attach it to the \ end of the reversed remainder of the list. \n", StyleBox["Axioms for Reversal", FontWeight->"Bold"], " (from left)\n\t", Cell[BoxData[ \(TraditionalForm\`ver(\ {}\ )\ = \ {}\)]], "\n\t", Cell[BoxData[ \(TraditionalForm\`ver(\ pre(L, x)\ )\ = \ app(\ ver(L), \ x\ )\)]], "\n" }], "Text", Evaluatable->False, AspectRatioFixed->True], Cell[TextData[{ "We will now prove that for any list these two opearations produce the same \ output. First, a little auxiliary lemma that shows that rev satisfies the \ axioms for ver.\nWe will need the following\n", StyleBox["Fact", FontWeight->"Bold"], ": ", Cell[BoxData[ \(TraditionalForm\`app(\ pre(X, a), b\ )\ = \ pre(\ app(X, b), a\ )\)]], ". \nThis is really an axiom for the prepend operation, the other axiom \ being ", Cell[BoxData[ \(TraditionalForm\`pre({}, a) = \ app({}, a)\)]], ". Recall that we have chosen append as the fundamental operation, so \ prepend can be expressed in terms of append. \n\n", StyleBox["Lemma 1", FontWeight->"Bold"], ": For any list ", Cell[BoxData[ \(TraditionalForm\`A\)]], " and any element ", Cell[BoxData[ \(TraditionalForm\`a\)]], ": ", Cell[BoxData[ \(TraditionalForm\`rev(\ pre(A, a))\ = \ app(rev(A), a)\)]], ".\t \nProof: \nBy induction on the list ", Cell[BoxData[ \(TraditionalForm\`A\)]], ". \nBases case: ", Cell[BoxData[ \(TraditionalForm\`A\ = \ {}\)]], ". \n", Cell[BoxData[ \(TraditionalForm\`rev( pre({}, a))\ = \ \(rev({a})\ = \ \(rev( app({}, a))\ = \ \(\(pre(rev({}), a)\)\(\ \)\(=\)\)\)\)\)]], "\n", Cell[BoxData[ \(TraditionalForm\`\(\(\ \)\(pre({}, a)\ = \ \({a}\ = \ \(app({}, a)\ = \ app(rev({}), a)\)\)\)\)\)]], ".\n\nInduction step: ", Cell[BoxData[ \(TraditionalForm\`A\ = \ app(X, b)\)]], ". \n", Cell[BoxData[ \(TraditionalForm\`rev( pre(A, a))\ = \ \(rev( pre(app(X, b), a))\ = \ \(\(rev( app(pre(X, a), b))\)\(\ \)\(=\)\)\)\)]], "\n", Cell[BoxData[ \(TraditionalForm\`pre(\ rev(\ \(pre(X, a)\)\(,\)), b)\ = \ \(\(pre\)\((\)\(\ \)\(app(\ rev(X), a, \ b)\ = \ \(\(app(\ pre(\ rev(X), \ b), \ a\ )\)\(\ \)\(=\)\)\)\)\)]], "\n", Cell[BoxData[ \(TraditionalForm\`app(\ rev(\ app(\ X, b)), \ a\ )\ = \ app(\ rev(A), \ a\ )\)]], ".\nIs anyone still breathing? If so, figure out where the induction \ hypothesis and the fact were used. \nQED\n" }], "Text", Evaluatable->False, AspectRatioFixed->True], Cell[TextData[{ "Now the main lemma. \n", StyleBox["Lemma 2", FontWeight->"Bold"], ": For any list ", Cell[BoxData[ \(TraditionalForm\`L\)]], ": ", StyleBox[" ", FontWeight->"Bold"], Cell[BoxData[ \(TraditionalForm\`rev(L)\ = \ ver(L)\)]], ".\n\t \nProof: \nBy induction on ", Cell[BoxData[ \(TraditionalForm\`n\ = \ \(\(|\)\(\(L\)\(|\)\)\)\)]], ". \nBase case: ", Cell[BoxData[ \(TraditionalForm\`n\ = \ 0\)]], ", so that ", Cell[BoxData[ \(TraditionalForm\`L\ = \ {}\)]], ". Then ", Cell[BoxData[ \(TraditionalForm\`rev({})\ = \ \({}\ = \ ver({})\)\)]], ".\nInduction step: ", Cell[BoxData[ \(TraditionalForm\`\(\(\ \)\(n\ > \ 0\)\)\)]], ". Then ", Cell[BoxData[ \(TraditionalForm\`L\ = \ pre(A, a)\)]], " where ", Cell[BoxData[ \(TraditionalForm\`A\)]], " and ", Cell[BoxData[ \(TraditionalForm\`a\)]], " are uniquely determined, and ", Cell[BoxData[ \(TraditionalForm\`\(\(|\)\(\(A\)\(|\)\)\) = \ n - 1\)]], ". \n", Cell[BoxData[ \(TraditionalForm\`rev( L)\ = \ \(rev(\ pre(A, a))\ = \ \(app(\ rev(A), \ a\ )\ = \ \(app(\ ver(A), \ a)\ = \ \(ver(\ pre(A, a))\ = \ ver(L)\)\)\)\)\)]], ".\nQED " }], "Text", Evaluatable->False, AspectRatioFixed->True] }, Closed]], Cell[CellGroupData[{ Cell[" Join and Reverse", "Subsection", Evaluatable->False, AspectRatioFixed->True, CellTags->"c:12"], Cell[TextData[{ "Here is one more property of join and reversal that is fairly obvious \ intuitively, and takes a little effort to establish formally. We will use \ this property later on in a C++ program, so make sure you understand what is \ going on. \n\n", StyleBox["Theorem", FontWeight->"Bold"], ": Let ", Cell[BoxData[ \(TraditionalForm\`A\)]], " and ", Cell[BoxData[ \(TraditionalForm\`B\)]], " be two lists. Then ", Cell[BoxData[ \(TraditionalForm\`rev(\ A\ \[CirclePlus]\ B\ )\ = \ rev(B)\ \[CirclePlus]\ rev(A)\)]], ".\nProof: \nBy structural induction on ", Cell[BoxData[ \(TraditionalForm\`B\)]], ". \n\nBases case: ", Cell[BoxData[ \(TraditionalForm\`B = {}\)]], ". Then using our previous results, \n", Cell[BoxData[ \(TraditionalForm\`rev(\ A\ \[CirclePlus]\ {})\ = \ \(rev( A)\ = \ \({}\ \[CirclePlus]\ rev(A)\ = \ rev({})\ \[CirclePlus]\ rev(A)\)\)\)]], ". \nInduction step: ", Cell[BoxData[ \(TraditionalForm\`B\ = \ app(BB, b)\)]], ". Then\n", Cell[BoxData[ \(TraditionalForm\`rev(\ A\ \[CirclePlus]\ app(BB, b))\ = \ \(rev(\ app(\ A\ \[CirclePlus]\ BB, \ b)\ )\ = \ \(\(pre(\ rev(\ A\ \[CirclePlus]\ BB), \ b\ )\)\(\ \)\(=\)\)\)\)]], "\n", Cell[BoxData[ \(TraditionalForm\`pre(\ rev(BB)\ \[CirclePlus]\ rev(A), \ b\ )\ = \ \(pre(\ rev(BB), \ b\ )\ \[CirclePlus]\ rev(A)\ = \ \(\(rev\)\((\)\(\ \)\(app(BB, b)\ \[CirclePlus]\ rev(A)\ = \ rev(B)\ \[CirclePlus]\ rev(A)\)\)\)\)]], ". \n\nThe second to the last step actually requires a little auxiliary \ lemma, namely that \n\t", Cell[BoxData[ \(TraditionalForm\`pre(\ X\ \[CirclePlus]\ Y, \ z\ )\ = \ pre(\ X, \ z)\ \[CirclePlus]\ Y\)]], ". \nThis is left as an exercise. \nQED\n\nThe only thing to remember here \ is that ", Cell[BoxData[ \(TraditionalForm\`A\)]], " and ", Cell[BoxData[ \(TraditionalForm\`B\)]], " on the right hand side are interchanged. " }], "Text", Evaluatable->False, AspectRatioFixed->True] }, Closed]], Cell[CellGroupData[{ Cell[" ToInteger with MSD", "Subsection", Evaluatable->False, AspectRatioFixed->True, CellTags->"c:13"], Cell[TextData[{ "Let us return to the conversion function toint that takes as input a \ list of digits (in some given base) and returns the corresponding number as \ output. The basic laws for toint are the following. \n\n ", Cell[BoxData[ \(TraditionalForm\`toint(\ {}, \ b\ )\ = \ 0\)]], ",\n ", Cell[BoxData[ \(TraditionalForm\`toint(\ app(L, d), \ b\ )\ = \ \(toint(\ L, \ b)\)\ \[CenterDot]\ b\ + \ d\)]], ".\n \nNote that from a practical point of view an empty list \ of digits may seem a degenerate case that should be ignored, but it actually \ makes the laws much easier to state if we allow this special case: every \ possible digit list can be built from the empty list using a sequence of \ Append operations. So, the two equations cover all possible situations, and \ in fact we pretty much have a written down a program to compute ToInteger. \n\ \nThe equations as stated correspond to our approach of dealing with the LSD \ first: d is the LSD and is peeled off first. Of course, we could also \ implement a different version of toint that removes the MSD first. For that \ version of toint, the second law would read (the first remains the same):\n \n\ \t", Cell[BoxData[ \(TraditionalForm\`toint2(\ pre(L, d), \ b\ )\ = \ d\ \[CenterDot]\ b\^\(\(|\)\(L\)\(|\)\)\ + \ toint2(L, b)\)]], ".\n \t\nWe can prove that the original toint also satisfies this equation, \ despite the fact that the recursion is going in the opposite direction. \n\n\ ", StyleBox["Lemma", FontWeight->"Bold"], ": For all digit lists ", Cell[BoxData[ \(TraditionalForm\`L\)]], ", any digit ", Cell[BoxData[ \(TraditionalForm\`d\)]], ", and any base ", Cell[BoxData[ \(TraditionalForm\`b\)]], ", ", Cell[BoxData[ \(TraditionalForm\`0\ \[LessEqual] \ d\ < \ b\)]], ", we have \n", Cell[BoxData[ \(TraditionalForm\`toint(\ pre(L, d), \ b\ )\ = \ d\ \[CenterDot]\ b\^\(\(|\)\(\(L\)\(|\)\)\)\ + \ toint(L, b)\)]], ".\n\nProof:\nWe proceed by structural induction on ", Cell[BoxData[ \(TraditionalForm\`L\)]], " (length type). Since the base ", Cell[BoxData[ \(TraditionalForm\`b\)]], " and the digit ", Cell[BoxData[ \(TraditionalForm\`d\)]], " can be considered fixed, we are really dealing with an assertion about \ lists here (rather than about a list together with two numbers).\n\nBase \ case: ", Cell[BoxData[ \(TraditionalForm\`L\ = \ {}\)]], ". Then \n", Cell[BoxData[ \(TraditionalForm\`toint(\ pre(\ {}, d), b)\ = \ \(toint(\ app({}, d), b)\ = \ \(\(toint({}, b)\)\ b\ + \ d\ = \ d\ b\^0 + \ toint({}, b)\)\)\)]], ". \n\nInduction step: suppose ", Cell[BoxData[ \(TraditionalForm\`L\ = \ app(K, s)\)]], ". Then \n", Cell[BoxData[ \(TraditionalForm\`\(\(toint(\ pre(L, d), b)\)\(\ \)\(=\)\(\ \)\(toint(\ pre(app(K, s), d), b)\ = \ \(\(toint(\ app(pre(K, d), s), b)\)\(\ \)\(=\)\)\)\(\ \)\)\)]], "\n", Cell[BoxData[ \(TraditionalForm\`\(toint(\ pre(K, d), b)\)\ \[CenterDot]\ b\ + \ s\ = \ \(\(\((d\ \[CenterDot]\ b\^\(\(|\)\(K\)\(|\)\)\ + \ toint(K, b))\)\ b\ + \ s\)\(\ \)\(=\)\)\)]], "\n", Cell[BoxData[ \(TraditionalForm\`d\ \[CenterDot]\ b\^\(\(|\)\(L\)\(|\)\)\ + \ \(toint(K, b)\)\ b\ + \ s\ = \(d\ \[CenterDot]\ b\^\(\(|\)\(L\)\(|\)\)\ + \ toint(app(K, s), b)\ = \ d\ \[CenterDot]\ b\^\(\(|\)\(L\)\(|\)\)\ + \ toint(L, b)\)\)]], ".\nQED\n" }], "Text", Evaluatable->False, AspectRatioFixed->True] }, Closed]] }, Closed]] }, Open ]] }, FrontEndVersion->"5.0 for X", ScreenRectangle->{{0, 1280}, {0, 1024}}, AutoGeneratedPackage->None, WindowToolbars->{}, CellGrouping->Automatic, WindowSize->{1152, 814}, WindowMargins->{{0, Automatic}, {Automatic, 0}}, PrintingStartingPageNumber->263, PrivateNotebookOptions->{"ColorPalette"->{RGBColor, 256}}, ShowCellLabel->True, ShowCellTags->False, RenderingOptions->{"ObjectDithering"->True, "RasterDithering"->False}, CharacterEncoding->Automatic, Magnification->1.5, StyleDefinitions -> "Classic.nb" ] (******************************************************************* Cached data follows. If you edit this Notebook file directly, not using Mathematica, you must remove the line containing CacheID at the top of the file. The cache data will then be recreated when you save this file from within Mathematica. *******************************************************************) (*CellTagsOutline CellTagsIndex->{ "c:1"->{ Cell[1828, 55, 93, 3, 110, "Title", Evaluatable->False, CellTags->"c:1"]}, "c:2"->{ Cell[1946, 62, 107, 3, 88, "Section", Evaluatable->False, CellTags->"c:2"], Cell[79612, 2484, 115, 3, 47, "Section", Evaluatable->False, CellTags->"c:2"]}, "c:3"->{ Cell[2289, 75, 116, 3, 42, "Subsection", Evaluatable->False, CellTags->"c:3"], Cell[80931, 2519, 111, 3, 42, "Subsection", Evaluatable->False, CellTags->"c:3"]}, "c:4"->{ Cell[2430, 82, 108, 3, 42, "Subsubsection", Evaluatable->False, CellTags->"c:4"], Cell[81067, 2526, 112, 3, 70, "Subsubsection", Evaluatable->False, CellTags->"c:4"]}, "c:5"->{ Cell[6089, 198, 115, 3, 42, "Subsubsection", Evaluatable->False, CellTags->"c:5"], Cell[84709, 2647, 111, 3, 70, "Subsubsection", Evaluatable->False, CellTags->"c:5"]}, "c:6"->{ Cell[9190, 295, 106, 3, 42, "Subsubsection", Evaluatable->False, CellTags->"c:6"], Cell[86378, 2702, 104, 3, 28, "Subsection", Evaluatable->False, CellTags->"c:6"]}, "c:7"->{ Cell[14018, 441, 103, 3, 42, "Subsection", Evaluatable->False, CellTags->"c:7"], Cell[91348, 2859, 118, 3, 28, "Subsection", Evaluatable->False, CellTags->"c:7"]}, "c:8"->{ Cell[17968, 555, 118, 3, 42, "Subsection", Evaluatable->False, CellTags->"c:8"], Cell[91491, 2866, 66, 1, 70, "Subsubsection", CellTags->"c:8"]}, "c:9"->{ Cell[21528, 650, 131, 3, 28, "Subsection", Evaluatable->False, CellTags->"c:9"], Cell[208230, 4598, 68, 1, 70, "Subsubsection", CellTags->"c:9"]}, "c:10"->{ Cell[22355, 674, 118, 3, 69, "Subsubsection", Evaluatable->False, CellTags->"c:10"], Cell[213935, 4773, 57, 1, 70, "Subsubsection", CellTags->"c:10"]}, "c:11"->{ Cell[27270, 857, 131, 3, 28, "Subsection", Evaluatable->False, CellTags->"c:11"], Cell[215568, 4843, 107, 3, 28, "Subsection", Evaluatable->False, CellTags->"c:11"]}, "c:12"->{ Cell[31718, 1011, 106, 3, 28, "Subsection", Evaluatable->False, CellTags->"c:12"], Cell[220537, 5007, 108, 3, 28, "Subsection", Evaluatable->False, CellTags->"c:12"]}, "c:13"->{ Cell[34518, 1100, 109, 3, 28, "Subsection", Evaluatable->False, CellTags->"c:13"], Cell[222855, 5076, 110, 3, 28, "Subsection", Evaluatable->False, CellTags->"c:13"]}, "c:14"->{ Cell[35033, 1118, 204, 7, 42, "Subsubsection", Evaluatable->False, CellTags->"c:14"]}, "c:15"->{ Cell[37864, 1214, 125, 3, 42, "Subsubsection", Evaluatable->False, CellTags->"c:15"]}, "c:16"->{ Cell[43714, 1402, 103, 3, 47, "Section", Evaluatable->False, CellTags->"c:16"]}, "c:17"->{ Cell[43842, 1409, 121, 3, 42, "Subsection", Evaluatable->False, CellTags->"c:17"]}, "c:18"->{ Cell[46628, 1501, 126, 3, 42, "Subsubsection", Evaluatable->False, CellTags->"c:18"]}, "c:19"->{ Cell[49637, 1603, 99, 3, 42, "Subsection", Evaluatable->False, CellTags->"c:19"]}, "c:20"->{ Cell[49761, 1610, 111, 3, 42, "Subsubsection", Evaluatable->False, CellTags->"c:20"]}, "c:21"->{ Cell[53434, 1732, 106, 3, 28, "Subsubsection", Evaluatable->False, CellTags->"c:21"]}, "c:22"->{ Cell[57977, 1885, 113, 3, 42, "Subsubsection", Evaluatable->False, CellTags->"c:22"]}, "c:23"->{ Cell[61632, 2007, 121, 3, 42, "Subsubsection", Evaluatable->False, CellTags->"c:23"]}, "c:24"->{ Cell[64233, 2090, 108, 3, 47, "Section", Evaluatable->False, CellTags->"c:24"]}, "c:25"->{ Cell[64366, 2097, 99, 3, 42, "Subsection", Evaluatable->False, CellTags->"c:25"]}, "c:26"->{ Cell[65694, 2136, 78, 1, 42, "Subsubsection", CellTags->"c:26"]}, "c:27"->{ Cell[69237, 2210, 54, 1, 42, "Subsubsection", CellTags->"c:27"]}, "c:28"->{ Cell[70507, 2261, 106, 3, 42, "Subsection", Evaluatable->False, CellTags->"c:28"]}, "c:29"->{ Cell[71690, 2293, 50, 1, 42, "Subsubsection", CellTags->"c:29"]}, "c:30"->{ Cell[72360, 2314, 53, 1, 42, "Subsubsection", CellTags->"c:30"]} } *) (*CellTagsIndex CellTagsIndex->{ {"c:1", 227686, 5202}, {"c:2", 227788, 5206}, {"c:3", 227987, 5213}, {"c:4", 228192, 5220}, {"c:5", 228403, 5227}, {"c:6", 228615, 5234}, {"c:7", 228824, 5241}, {"c:8", 229031, 5248}, {"c:9", 229214, 5254}, {"c:10", 229399, 5260}, {"c:11", 229589, 5266}, {"c:12", 229800, 5273}, {"c:13", 230012, 5280}, {"c:14", 230224, 5287}, {"c:15", 230339, 5291}, {"c:16", 230454, 5295}, {"c:17", 230563, 5299}, {"c:18", 230675, 5303}, {"c:19", 230790, 5307}, {"c:20", 230901, 5311}, {"c:21", 231016, 5315}, {"c:22", 231131, 5319}, {"c:23", 231246, 5323}, {"c:24", 231361, 5327}, {"c:25", 231470, 5331}, {"c:26", 231581, 5335}, {"c:27", 231669, 5338}, {"c:28", 231757, 5341}, {"c:29", 231869, 5345}, {"c:30", 231957, 5348} } *) (*NotebookFileOutline Notebook[{ Cell[1754, 51, 49, 0, 40, "SmallText"], Cell[CellGroupData[{ Cell[1828, 55, 93, 3, 110, "Title", Evaluatable->False, CellTags->"c:1"], Cell[CellGroupData[{ Cell[1946, 62, 107, 3, 88, "Section", Evaluatable->False, CellTags->"c:2"], Cell[2056, 67, 208, 4, 68, "Text"], Cell[CellGroupData[{ Cell[2289, 75, 116, 3, 42, "Subsection", Evaluatable->False, CellTags->"c:3"], Cell[CellGroupData[{ Cell[2430, 82, 108, 3, 42, "Subsubsection", Evaluatable->False, CellTags->"c:4"], Cell[2541, 87, 2480, 69, 393, "Text", Evaluatable->False], Cell[5024, 158, 1028, 35, 118, "Text", Evaluatable->False] }, Closed]], Cell[CellGroupData[{ Cell[6089, 198, 115, 3, 42, "Subsubsection", Evaluatable->False, CellTags->"c:5"], Cell[6207, 203, 1875, 57, 268, "Text", Evaluatable->False], Cell[8085, 262, 1068, 28, 168, "Text", Evaluatable->False] }, Closed]], Cell[CellGroupData[{ Cell[9190, 295, 106, 3, 42, "Subsubsection", Evaluatable->False, CellTags->"c:6"], Cell[9299, 300, 4670, 135, 743, "Text", Evaluatable->False] }, Closed]] }, Closed]], Cell[CellGroupData[{ Cell[14018, 441, 103, 3, 42, "Subsection", Evaluatable->False, CellTags->"c:7"], Cell[14124, 446, 787, 15, 193, "Text", Evaluatable->False], Cell[14914, 463, 1143, 31, 228, "Text", Evaluatable->False], Cell[16060, 496, 55, 1, 89, "Input"], Cell[16118, 499, 1425, 38, 388, "Text", Evaluatable->False], Cell[17546, 539, 385, 11, 93, "Text", Evaluatable->False] }, Closed]], Cell[CellGroupData[{ Cell[17968, 555, 118, 3, 42, "Subsection", Evaluatable->False, CellTags->"c:8"], Cell[18089, 560, 3402, 85, 69, "Text", Evaluatable->False] }, Closed]], Cell[CellGroupData[{ Cell[21528, 650, 131, 3, 28, "Subsection", Evaluatable->False, CellTags->"c:9"], Cell[21662, 655, 668, 15, 69, "Text", Evaluatable->False], Cell[CellGroupData[{ Cell[22355, 674, 118, 3, 69, "Subsubsection", Evaluatable->False, CellTags->"c:10"], Cell[22476, 679, 136, 5, 69, "Text", Evaluatable->False], Cell[22615, 686, 371, 14, 69, "Text", Evaluatable->False], Cell[22989, 702, 266, 10, 69, "Text", Evaluatable->False], Cell[23258, 714, 179, 4, 69, "Input"], Cell[23440, 720, 501, 16, 69, "Text", Evaluatable->False], Cell[23944, 738, 71, 2, 69, "Input"], Cell[24018, 742, 982, 29, 69, "Text", Evaluatable->False], Cell[25003, 773, 104, 3, 69, "Input"], Cell[25110, 778, 333, 11, 69, "Text", Evaluatable->False], Cell[25446, 791, 428, 10, 69, "Text"], Cell[25877, 803, 240, 5, 69, "Input"], Cell[26120, 810, 21, 0, 69, "Text"], Cell[26144, 812, 71, 2, 69, "Input"], Cell[26218, 816, 79, 2, 69, "Text", Evaluatable->False], Cell[26300, 820, 104, 3, 69, "Input"], Cell[26407, 825, 333, 8, 69, "Text", Evaluatable->False], Cell[26743, 835, 58, 1, 69, "Input"], Cell[26804, 838, 219, 6, 69, "Text"], Cell[27026, 846, 124, 2, 69, "Input"], Cell[27153, 850, 68, 1, 69, "Input"] }, Closed]] }, Closed]], Cell[CellGroupData[{ Cell[27270, 857, 131, 3, 28, "Subsection", Evaluatable->False, CellTags->"c:11"], Cell[27404, 862, 755, 16, 69, "Text", Evaluatable->False], Cell[28162, 880, 177, 4, 69, "Input"], Cell[28342, 886, 96, 2, 69, "Input"], Cell[28441, 890, 317, 7, 69, "Text", Evaluatable->False], Cell[28761, 899, 99, 2, 69, "Input"], Cell[28863, 903, 213, 7, 69, "Text", Evaluatable->False], Cell[29079, 912, 79, 2, 69, "Input"], Cell[29161, 916, 85, 2, 69, "Input"], Cell[29249, 920, 259, 7, 69, "Text", Evaluatable->False], Cell[29511, 929, 66, 2, 69, "Input"], Cell[29580, 933, 311, 8, 69, "Text", Evaluatable->False], Cell[29894, 943, 91, 2, 69, "Input"], Cell[29988, 947, 131, 3, 69, "Input"], Cell[30122, 952, 424, 14, 69, "Text", Evaluatable->False], Cell[30549, 968, 152, 3, 69, "Input"], Cell[30704, 973, 81, 2, 69, "Text", Evaluatable->False], Cell[30788, 977, 83, 2, 69, "Input"], Cell[30874, 981, 338, 8, 69, "Text", Evaluatable->False], Cell[31215, 991, 114, 2, 69, "Input"], Cell[31332, 995, 94, 2, 69, "Text", Evaluatable->False], Cell[31429, 999, 141, 3, 69, "Input"], Cell[31573, 1004, 108, 2, 69, "Text", Evaluatable->False] }, Closed]], Cell[CellGroupData[{ Cell[31718, 1011, 106, 3, 28, "Subsection", Evaluatable->False, CellTags->"c:12"], Cell[31827, 1016, 1839, 51, 618, "Text", Evaluatable->False], Cell[33669, 1069, 324, 7, 166, "Input"], Cell[33996, 1078, 114, 4, 50, "Input"], Cell[34113, 1084, 368, 11, 168, "Text", Evaluatable->False] }, Closed]], Cell[CellGroupData[{ Cell[34518, 1100, 109, 3, 28, "Subsection", Evaluatable->False, CellTags->"c:13"], Cell[34630, 1105, 378, 9, 118, "Text", Evaluatable->False], Cell[CellGroupData[{ Cell[35033, 1118, 204, 7, 42, "Subsubsection", Evaluatable->False, CellTags->"c:14"], Cell[35240, 1127, 743, 25, 143, "Text", Evaluatable->False], Cell[35986, 1154, 162, 4, 98, "Input"], Cell[36151, 1160, 275, 6, 68, "Text", Evaluatable->False], Cell[36429, 1168, 205, 4, 74, "Input"], Cell[36637, 1174, 1190, 35, 293, "Text", Evaluatable->False] }, Closed]], Cell[CellGroupData[{ Cell[37864, 1214, 125, 3, 42, "Subsubsection", Evaluatable->False, CellTags->"c:15"], Cell[37992, 1219, 1053, 27, 143, "Text", Evaluatable->False], Cell[39048, 1248, 117, 3, 106, "Input"], Cell[39168, 1253, 187, 6, 43, "Text"], Cell[39358, 1261, 102, 2, 51, "Input"], Cell[39463, 1265, 82, 2, 59, "Input"], Cell[39548, 1269, 398, 8, 143, "Input"], Cell[39949, 1279, 165, 5, 43, "Text", Evaluatable->False], Cell[40117, 1286, 79, 2, 51, "Input"], Cell[40199, 1290, 901, 26, 168, "Text", Evaluatable->False], Cell[41103, 1318, 154, 4, 101, "Input"], Cell[41260, 1324, 2167, 62, 318, "Text", Evaluatable->False], Cell[43430, 1388, 223, 7, 43, "Text", Evaluatable->False] }, Closed]] }, Closed]] }, Closed]], Cell[CellGroupData[{ Cell[43714, 1402, 103, 3, 47, "Section", Evaluatable->False, CellTags->"c:16"], Cell[CellGroupData[{ Cell[43842, 1409, 121, 3, 42, "Subsection", Evaluatable->False, CellTags->"c:17"], Cell[43966, 1414, 1662, 51, 318, "Text", Evaluatable->False], Cell[45631, 1467, 972, 30, 143, "Text", Evaluatable->False], Cell[CellGroupData[{ Cell[46628, 1501, 126, 3, 42, "Subsubsection", Evaluatable->False, CellTags->"c:18"], Cell[46757, 1506, 1724, 52, 343, "Text", Evaluatable->False], Cell[48484, 1560, 87, 3, 74, "Input"], Cell[48574, 1565, 1014, 32, 168, "Text", Evaluatable->False] }, Closed]] }, Closed]], Cell[CellGroupData[{ Cell[49637, 1603, 99, 3, 42, "Subsection", Evaluatable->False, CellTags->"c:19"], Cell[CellGroupData[{ Cell[49761, 1610, 111, 3, 42, "Subsubsection", Evaluatable->False, CellTags->"c:20"], Cell[49875, 1615, 2254, 79, 69, "Text", Evaluatable->False], Cell[52132, 1696, 1265, 31, 69, "Text", Evaluatable->False] }, Closed]], Cell[CellGroupData[{ Cell[53434, 1732, 106, 3, 28, "Subsubsection", Evaluatable->False, CellTags->"c:21"], Cell[53543, 1737, 695, 17, 143, "Text", Evaluatable->False], Cell[54241, 1756, 117, 2, 51, "Input"], Cell[54361, 1760, 97, 3, 74, "Input"], Cell[54461, 1765, 448, 10, 118, "Text", Evaluatable->False], Cell[54912, 1777, 139, 3, 51, "Input"], Cell[55054, 1782, 189, 6, 143, "Input"], Cell[55246, 1790, 194, 7, 43, "Text", Evaluatable->False], Cell[55443, 1799, 137, 3, 74, "Input"], Cell[55583, 1804, 2357, 76, 468, "Text", Evaluatable->False] }, Closed]], Cell[CellGroupData[{ Cell[57977, 1885, 113, 3, 42, "Subsubsection", Evaluatable->False, CellTags->"c:22"], Cell[58093, 1890, 140, 5, 43, "Text", Evaluatable->False], Cell[58236, 1897, 129, 3, 103, "Input"], Cell[58368, 1902, 829, 26, 118, "Text", Evaluatable->False], Cell[59200, 1930, 120, 3, 51, "Input"], Cell[59323, 1935, 1987, 54, 343, "Text", Evaluatable->False], Cell[61313, 1991, 282, 11, 68, "Text", Evaluatable->False] }, Closed]], Cell[CellGroupData[{ Cell[61632, 2007, 121, 3, 42, "Subsubsection", Evaluatable->False, CellTags->"c:23"], Cell[61756, 2012, 2013, 60, 69, "Text", Evaluatable->False], Cell[63772, 2074, 400, 9, 69, "Text", Evaluatable->False] }, Closed]] }, Closed]] }, Closed]], Cell[CellGroupData[{ Cell[64233, 2090, 108, 3, 47, "Section", Evaluatable->False, CellTags->"c:24"], Cell[CellGroupData[{ Cell[64366, 2097, 99, 3, 42, "Subsection", Evaluatable->False, CellTags->"c:25"], Cell[64468, 2102, 606, 12, 118, "Text"], Cell[65077, 2116, 592, 16, 118, "Text"], Cell[CellGroupData[{ Cell[65694, 2136, 78, 1, 42, "Subsubsection", CellTags->"c:26"], Cell[65775, 2139, 3425, 66, 1030, "Input"] }, Closed]], Cell[CellGroupData[{ Cell[69237, 2210, 54, 1, 42, "Subsubsection", CellTags->"c:27"], Cell[69294, 2213, 610, 19, 118, "Text"], Cell[69907, 2234, 57, 1, 51, "Input"], Cell[69967, 2237, 57, 1, 51, "Input"], Cell[70027, 2240, 57, 1, 51, "Input"], Cell[70087, 2243, 59, 1, 51, "Input"], Cell[70149, 2246, 188, 4, 74, "Input"], Cell[70340, 2252, 118, 3, 68, "Text"] }, Closed]] }, Closed]], Cell[CellGroupData[{ Cell[70507, 2261, 106, 3, 42, "Subsection", Evaluatable->False, CellTags->"c:28"], Cell[70616, 2266, 631, 12, 168, "Text"], Cell[71250, 2280, 45, 1, 51, "Input"], Cell[71298, 2283, 367, 6, 93, "Text"], Cell[CellGroupData[{ Cell[71690, 2293, 50, 1, 42, "Subsubsection", CellTags->"c:29"], Cell[71743, 2296, 207, 4, 68, "Text"], Cell[71953, 2302, 370, 7, 143, "Input"] }, Closed]], Cell[CellGroupData[{ Cell[72360, 2314, 53, 1, 42, "Subsubsection", CellTags->"c:30"], Cell[72416, 2317, 201, 4, 68, "Text"], Cell[72620, 2323, 326, 5, 166, "Input"], Cell[72949, 2330, 326, 5, 166, "Input"], Cell[73278, 2337, 212, 5, 43, "Text"], Cell[73493, 2344, 326, 5, 166, "Input"], Cell[73822, 2351, 35, 0, 43, "Text"], Cell[73860, 2353, 292, 5, 166, "Input"], Cell[74155, 2360, 468, 8, 93, "Text"], Cell[74626, 2370, 240, 5, 74, "Input"], Cell[74869, 2377, 65, 0, 43, "Text"], Cell[74937, 2379, 360, 6, 166, "Input"], Cell[75300, 2387, 87, 3, 43, "Text"], Cell[75390, 2392, 464, 7, 189, "Input"], Cell[75857, 2401, 464, 7, 189, "Input"], Cell[76324, 2410, 462, 7, 189, "Input"], Cell[76789, 2419, 443, 7, 189, "Input"], Cell[77235, 2428, 447, 7, 189, "Input"], Cell[77685, 2437, 443, 7, 189, "Input"], Cell[78131, 2446, 182, 3, 74, "Input"], Cell[78316, 2451, 182, 3, 74, "Input"], Cell[78501, 2456, 182, 3, 74, "Input"], Cell[78686, 2461, 443, 7, 189, "Input"], Cell[79132, 2470, 419, 7, 189, "Input"] }, Closed]] }, Closed]] }, Closed]], Cell[CellGroupData[{ Cell[79612, 2484, 115, 3, 47, "Section", Evaluatable->False, CellTags->"c:2"], Cell[79730, 2489, 663, 13, 118, "Text", Evaluatable->False], Cell[80396, 2504, 510, 11, 143, "Text", Evaluatable->False], Cell[CellGroupData[{ Cell[80931, 2519, 111, 3, 42, "Subsection", Evaluatable->False, CellTags->"c:3"], Cell[CellGroupData[{ Cell[81067, 2526, 112, 3, 70, "Subsubsection", Evaluatable->False, CellTags->"c:4"], Cell[81182, 2531, 834, 29, 70, "Text", Evaluatable->False], Cell[82019, 2562, 2653, 80, 70, "Text", Evaluatable->False] }, Closed]], Cell[CellGroupData[{ Cell[84709, 2647, 111, 3, 70, "Subsubsection", Evaluatable->False, CellTags->"c:5"], Cell[84823, 2652, 1506, 44, 70, "Text", Evaluatable->False] }, Closed]] }, Closed]], Cell[CellGroupData[{ Cell[86378, 2702, 104, 3, 28, "Subsection", Evaluatable->False, CellTags->"c:6"], Cell[86485, 2707, 152, 5, 70, "Text", Evaluatable->False], Cell[86640, 2714, 131, 4, 70, "Input"], Cell[86774, 2720, 1102, 32, 70, "Text", Evaluatable->False], Cell[87879, 2754, 815, 27, 70, "Text"], Cell[88697, 2783, 1091, 28, 70, "Text", Evaluatable->False], Cell[89791, 2813, 1520, 41, 70, "Text", Evaluatable->False] }, Closed]], Cell[CellGroupData[{ Cell[91348, 2859, 118, 3, 28, "Subsection", Evaluatable->False, CellTags->"c:7"], Cell[CellGroupData[{ Cell[91491, 2866, 66, 1, 70, "Subsubsection", CellTags->"c:8"], Cell[91560, 2869, 263, 8, 70, "Text", Evaluatable->False], Cell[91826, 2879, 248, 8, 70, "Text"], Cell[92077, 2889, 490, 18, 70, "Text"], Cell[92570, 2909, 1292, 50, 70, "Text"], Cell[93865, 2961, 892, 26, 70, "Text"], Cell[94760, 2989, 1518, 46, 70, "Text"], Cell[96281, 3037, 110091, 1482, 70, 3469, 162, "GraphicsData", "PostScript", \ "Graphics"], Cell[206375, 4521, 1075, 36, 70, "Text"], Cell[207453, 4559, 316, 13, 70, "Text"], Cell[207772, 4574, 421, 19, 70, "Text"] }, Closed]], Cell[CellGroupData[{ Cell[208230, 4598, 68, 1, 70, "Subsubsection", CellTags->"c:9"], Cell[208301, 4601, 3830, 114, 70, "Text"], Cell[212134, 4717, 112, 2, 70, "Input"], Cell[212249, 4721, 250, 6, 70, "Text"], Cell[212502, 4729, 155, 3, 70, "Input"], Cell[212660, 4734, 121, 2, 70, "Input"], Cell[212784, 4738, 582, 15, 70, "Text"], Cell[213369, 4755, 415, 8, 70, "Input"], Cell[213787, 4765, 111, 3, 70, "Input"] }, Closed]], Cell[CellGroupData[{ Cell[213935, 4773, 57, 1, 70, "Subsubsection", CellTags->"c:10"], Cell[213995, 4776, 953, 36, 70, "Text"], Cell[214951, 4814, 568, 23, 70, "Text"] }, Closed]] }, Closed]], Cell[CellGroupData[{ Cell[215568, 4843, 107, 3, 28, "Subsection", Evaluatable->False, CellTags->"c:11"], Cell[215678, 4848, 402, 10, 70, "Text", Evaluatable->False], Cell[216083, 4860, 717, 23, 70, "Text", Evaluatable->False], Cell[216803, 4885, 2304, 66, 70, "Text", Evaluatable->False], Cell[219110, 4953, 1390, 49, 70, "Text", Evaluatable->False] }, Closed]], Cell[CellGroupData[{ Cell[220537, 5007, 108, 3, 28, "Subsection", Evaluatable->False, CellTags->"c:12"], Cell[220648, 5012, 2170, 59, 558, "Text", Evaluatable->False] }, Closed]], Cell[CellGroupData[{ Cell[222855, 5076, 110, 3, 28, "Subsection", Evaluatable->False, CellTags->"c:13"], Cell[222968, 5081, 3743, 89, 1059, "Text", Evaluatable->False] }, Closed]] }, Closed]] }, Open ]] } ] *) (******************************************************************* End of Mathematica Notebook file. *******************************************************************)