{ "cells": [ { "cell_type": "markdown", "metadata": {}, "source": [ "# Week 1: Introduction and background" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "## About these notes\n", "\n", "These notes are _not_ a replacement for the (excellent) textbook. They correspond roughly to the content of my lectures, but also include pointers to readings in the textbook, which usually go into a lot more detail. Unless marked optional, you're responsible for both the notes as well as any readings/videos that they point to.\n", "\n", "There is one notebook for each week of the course. Please read the section titled \"Tuesday\" **before** Tuesday's class, and the section \"Thursday\" **before** Thursday's class. In class, I will take questions about the readings and then we will often jump right in to doing example problems." ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "# Tuesday\n", "\n", "
\n", "

Read 0.1, which is an overview of the whole course.

\n", "

Watch W1E1: Welcome

\n", "
\n", "\n", "Welcome to *Theory of Computing*! \n", "\n", "I'd like to introduce the course with a game called Poco. Please visit [https://bit.ly/playpoco](https://bit.ly/playpoco) and play a few levels. Then, think about: how would you make a computer play this game perfectly? If a puzzle has a solution, the computer must find it, but if a puzzle has no solution, the computer must click the \"give up\" button.\n", "\n", "If you tried to write a program to do this, you would find that it's extremely difficult (particularly, how to make the computer decide to give up). You might suspect that it's impossible, but how would you know for sure? And maybe it's not possible now, but might it be possible in a more powerful programming language, or on more powerful hardware, perhaps hardware that hasn't been invented yet?\n", "\n", "To give a definite answer to this question, we need three ingredients. These ingredients will be part of everything we do in this course. \n", "\n", "First, we need a **model of computation**, a definition of what a computer is and does.\n", "\n", "Second, we need to define our **computational problem**, in this case, \"playing Poco perfectly,\" in a precise way.\n", "\n", "Third, we need to **prove a relationship** between models of computation and/or computational problems: in this case, that it's either possible or impossible to make a computer play Poco perfectly." ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "## Computation\n", "\n", "
\n", " Watch W1E2: What is a Computer?\n", "
\n", " \n", "What is a computer? Most of you are juniors in computer science, and by the end of this year, we hope you'll understand, from bottom to top, how a C/C++/Python program running on Linux running on x86/ARM/MIPS works. But we want your computer science degree to be good for a lifetime. In 50 years, what kinds of computers will you be programming, building, or even inventing? In this course, we want to teach you what we believe to be true, not just about a particular kind of computer, but about all computers, past, present, and future.\n", "\n", "To do this, we need to look to the beginning. Historically, the answer to this question came from a totally different direction, from people asking not \"what is a computer,\" but \"what does it mean to compute?\" For in 1936, everyone knew what a computer was. A printer is a person who prints; a dishwasher is a person who washes dishes; and a computer is a person who computes. For example, when you do arithmetic or solve a system of linear equations or find a derivative, you're computing -- you're following an algorithm that you learned in school. But some math requires more ingenuity, like writing proofs. In the early 20th century, mathematicians were starting to wonder whether there was an \"effective procedure\" (we would say, an algorithm) for writing proofs too.\n", "\n", "In 1936, Turing published the paper that many consider to be the founding document of computer science. His answer to the question about what was meant by an \"effective procedure\" was not the first, but it was the most convincing. He imagined a computing person with access to an unlimited supply of paper, argued convincingly for various simplifying assumptions about how he/she computes, and finally imagined a machine (which he called an a-machine, but which we now call a Turing machine) that would do the same thing automatically. \n", "\n", "Although Turing machines were invented just as a mathematical construct, they are important for computer science because all current computers (under some reasonable assumptions) can be emulated by a Turing machine. We will further argue that even computers of the future can be emulated by Turing machines. If you accept these arguments, then Turing machines serve as our definition of what a computer is: if something can be done on a computer, it can be done on a Turing machine; if something cannot be done on a Turing machine, it cannot be done on any other computer.\n", "\n", "Under this definition, we'll be able to prove that there are problems that *no* Turing machine can solve, and therefore that no program written for any current or future computer can solve. Automatically solving \"Poco\" (more commonly known as the [Post Correspondence Problem]) is one of these.\n", "\n", "[Post Correspondence Problem]: https://en.wikipedia.org/wiki/Post_correspondence_problem\n", "\n", "Before we get there in Unit III, we will study several simpler models of computation in Units I and II. You're probably familiar with two of them already: deterministic finite automata (also known as finite state machines) and regular expressions. And in Unit IV, we will continue to study Turing machines, but we'll restrict them to use only a polynomial amount of time." ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "## Problems\n", "\n", "
Watch W1E3: Strings and Languages
\n", "\n", "The second ingredient is that we need a way of talking about computational problems. It would seem that there are so many different kinds of things that computers could do, that we have to study each kind separately. But maybe we can reduce them all to one kind of problem, and focus our study on that one kind of problem. Namely, we want to treat every kind of object as a **string of symbols** (e.g., bits), and we want to treat every kind of computational problem as a **yes/no question about strings**.\n", "\n", "People are fairly comfortable these days with the idea that any kind of object we might want to compute about can be represented as a string. We deal every day with messages, music, pictures, movies, books, etc., in digital form, with the awareness that these are just strings of 0’s and 1’s.\n", "\n", "Less obvious, perhaps, is that it makes sense to reduce all kinds of computations down to yes/no questions about strings. There are a number of objections that could be raised and which we can discuss in class, but to me the most glaring one is that the output from a computer program is much more than just a \"yes\" or \"no\" answer. For example, suppose we want a program that looks at a chess board `b` and outputs the best next move -- that's not a yes/no question. But suppose further that we can write a function `is_best_move` that takes a chess board, a possible next move `m`, and returns \"yes\" if `m` is the best move and \"no\" otherwise. Then we can write a function\n", "\n", " def find_best_move(board):\n", " for all possible moves m:\n", " if is_best_move(board, m):\n", " return m\n", "\n", "Since it's possible to implement any function as a wrapper around a function that returns yes/no, it's sufficient, for pretty much the rest of the course, to only think about computations that result in a yes/no answer. (Caveat: Implementing a function this way can be *much slower* than implementing it directly, but for the first three units of the course, we don't care about efficiency. In Unit IV, we will talk about how to improve the efficiency of this trick.)\n", "\n", "Next, I'd like to introduce the concepts and notation for strings and sets of strings that we'll use for the rest of the course.\n", "\n", "
\n", "

Skim Section 0.2, which covers mathematical preliminaries that you should have gotten in Discrete Math. If anything seems unfamiliar to you, study it a little more carefully. The subsection \"Strings and Languages\" is especially important and surprisingly short; the notes below expand on it considerably.

\n", "
" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "### Symbols and alphabets\n", "\n", "An *alphabet* is a nonempty finite set of *symbols*. We use $\\Sigma$ (uppercase sigma) or sometimes $\\Gamma$ (uppercase gamma) to stand for an alphabet. For example, some alphabets we will use frequently in this class are\n", "\\begin{align}\n", "\\Sigma &= \\{ \\texttt{0}, \\texttt{1} \\} \\\\\n", "\\Sigma &= \\{ \\texttt{a}, \\texttt{b} \\}.\n", "\\end{align}\n", "When possible, we write symbols using typewriter font. When we want a variable to range over symbols, we usually use $\\sigma$ (lowercase sigma) or $a, b$, etc. Note that $\\texttt{a}$ is an actual symbol, whereas $a$ is a variable that ranges over symbols (analogous to the distinction between the character constant `'a'` and the variable `a` in C)." ] }, { "attachments": { "image.png": { "image/png": "iVBORw0KGgoAAAANSUhEUgAAAsIAAAF+CAYAAACI8nxKAAAAAXNSR0IArs4c6QAAAJBlWElmTU0AKgAAAAgABgEGAAMAAAABAAIAAAESAAMAAAABAAEAAAEaAAUAAAABAAAAVgEbAAUAAAABAAAAXgEoAAMAAAABAAIAAIdpAAQAAAABAAAAZgAAAAAAAACQAAAAAQAAAJAAAAABAAOgAQADAAAAAQABAACgAgAEAAAAAQAAAsKgAwAEAAAAAQAAAX4AAAAAoiD77wAAAAlwSFlzAAAWJQAAFiUBSVIk8AAAAgtpVFh0WE1MOmNvbS5hZG9iZS54bXAAAAAAADx4OnhtcG1ldGEgeG1sbnM6eD0iYWRvYmU6bnM6bWV0YS8iIHg6eG1wdGs9IlhNUCBDb3JlIDUuNC4wIj4KICAgPHJkZjpSREYgeG1sbnM6cmRmPSJodHRwOi8vd3d3LnczLm9yZy8xOTk5LzAyLzIyLXJkZi1zeW50YXgtbnMjIj4KICAgICAgPHJkZjpEZXNjcmlwdGlvbiByZGY6YWJvdXQ9IiIKICAgICAgICAgICAgeG1sbnM6dGlmZj0iaHR0cDovL25zLmFkb2JlLmNvbS90aWZmLzEuMC8iPgogICAgICAgICA8dGlmZjpPcmllbnRhdGlvbj4xPC90aWZmOk9yaWVudGF0aW9uPgogICAgICAgICA8dGlmZjpQaG90b21ldHJpY0ludGVycHJldGF0aW9uPjI8L3RpZmY6UGhvdG9tZXRyaWNJbnRlcnByZXRhdGlvbj4KICAgICAgICAgPHRpZmY6UmVzb2x1dGlvblVuaXQ+MjwvdGlmZjpSZXNvbHV0aW9uVW5pdD4KICAgICAgICAgPHRpZmY6Q29tcHJlc3Npb24+NTwvdGlmZjpDb21wcmVzc2lvbj4KICAgICAgPC9yZGY6RGVzY3JpcHRpb24+CiAgIDwvcmRmOlJERj4KPC94OnhtcG1ldGE+Cs+OiooAAEAASURBVHgB7J0HmBTF08Z7OXKQqGQ4kiKIEiQoUZQgAqKYMCBmEDMmRD8xK38DqChmEAVFVAQjSRAQASWIIJIkiCCSo6AwX73t9Tp7t3u3ezezO7vz1vPUTe7w677d2p7qaqUoJEACJEACJEACJEACJOBDAgEf1plVJgES8DeB/FL9UqIlRYuJFhEtmo1md72QPIf00mwayzHuhfwjeiRD7fs4F83xIbnvQAQ9GOG8uR/X94vuFt0livwoJEACJOALAjSEfdHMrCQJpBwBGLClMxRGLfaj3RaXeymRCeyTSztFYRTHssW9MKgpJEACJJA0BGgIJ01TsaAkkPIEYNxWEC1vU/uxfR/35krS0tJUqVKltBYtWlSF0yJFioQ9b+411wsXLqyQXv78+fUW+7Ec4znIP//8o44cORLcYj+W47/++ksdOHBAHTx4UG+xH06zu75r1y4FRb55EBjCf2Tolgj7uI5rNJoFAoUESCCxBGgIJ5Y/cycBPxCA+0AV0Wo2rST7MHhzZdzCEC1TpowqXbq0Nmhj2ZYoUUKypUQisHfvXrVz505tFMey3bFjhzbEI6Ub5nw4o/l3uW+DTX+Tfbh9UEiABEjAFQI0hF3BykRJwFcEyklt7Uaufb+6XIPBm+NnDUZby5cvH9QKFSoE93Hefkxj1pv9C0b0H3/8oXXLli3BfZzLfIwR6yjEknswgrxe1G4g2/e3RZEObyEBEiCBsARy/HIK+xRPkgAJ+IkAJovVFq2Todi3G7uYaBZR8Pq/cuXKqnr16qpatWpacWw3bGHo0riNiDAlL9iNZmMob9q0SW3YsEHr+vXrFY7hNpKDwKK2G8ar5XhVhmIfkwEpJEACJBCWAA3hsFh4kgR8R6Cg1Lim6PGixuA1W7g1RPysgL8tDFy7oWsMXmwrVaqk8uXLJ0lQSCA2AkePHlW///570Dg2RjK2MJSxhV9zNoIRZbhXGMPYbFfKubWih0UpJEACPiYQ8cvNx0xYdRJIVQL4f08XrSsKI9du9MKFIay1WrBgQVWjRg1Vp06doKanpwdHdzmSK+QoCSOAkWVjIK9bt06tWrUqqL/++qs6fDiirXtUCr1e1G4cY3+F6DpRGNEUEiCBFCeAL0YKCZBA6hE4Tqp0kmgD27a+7IcNHYZIBzBu7cbu8ccfr48x0ovrFBJINgKIgIGRYxjHK1euDBrIOIbRnE2EDISQWya6VPQn23ar7FNIgARSiAAN4RRqTFbFlwQQAgEGbmaj99hwNCpWrKjq16+vDVxj6ML4xYhvgQIFwj3CcySQkgT+/vtvhRFjM4JsDOVly5apzZs3R6rzn3Ihs3EMg3lvpAd4ngRIwNsEaAh7u31YOhIwBPC/Wkv0VNGTRY3hC5eGLP/HJUuWVCeddJJq0KCB3pp9hByjkAAJZE8AoeCWLl2qfvrpJ61mf/duLL6XReBCsV7UGMg/yv73omtE6V4hECgk4GUCWb5AvVxYlo0EfEQgXeoKo9doE9nHymkhggUdTjzxxBBjF0Zv1apVQ+7jAQmQQN4JbNy4McQwhqH8888/KyxoEkYwi+8HURjFRtfJPoUESMBDBGgIe6gxWBTfEkBUBmPwmm3ZzDTg1nDqqaeqxo0bB0d7a9euTf/dzKB4TAJxJAA/49WrVwdHkBcuXKi+//77SO4V26Voxig2W0S1oJAACSSIAA3hBIFntr4lgElszUSNwYstFpwIkeOOO041adJEG74wfps2bapgCFNIgASSgwDCvsEgNvrDDz+orVvDzrXDgiHGKMZ2vmjYG5Oj5iwlCSQXARrCydVeLG3yEThBitxStFWGImxZiMBvF8Yu1Bi/iL9LIQESSC0CCPMGwxhGsTGQ4Y8cRhDGbXaGzpHtL2Hu4SkSIAEHCNAQdgAikyCBDAIIu9BY1Bi9MIBDojcUK1bMat68ecAYvtgiYgOFBEjAnwQQucIYxdjOmzfP2r9/f+bvZkSrgEFsjOOFsv+3P4mx1iTgLIHM/2zOps7USCC1CRwj1Ttd1Iz4Npd9LEccFLgztGzZUrVq1Uprw4YN6dMbpMMdEiCBzATgc7x48WI1e/ZsrXPmzAnnb4xlo+eJwjCGgfyt6B5RCgmQQIwEaAjHCIy3+5oAYo+1F20nilFfLFZhX43NkggOAWP0YluzZk25hUICJEACuSewdu3aoGEMA1kiVSAsm/37G6vkIXwbDOMZotNFw/pcyHkKCZCAjYD9H8l2mrskQAJCoLAoRns7iJ4l2kg0aPjKAhSWTGILGr4Y+WWcXiFEIQEScJUA/IoxUmxGjRcsWGDJAiH273MYxotEp4pOEcWocdgYb3KeQgK+JmD/x/E1CFaeBIQAjFwYuzB6oRj1hTGspVChQpaM8gbOPPNM1bp1az25DXF8KSRAAiSQSAKIYwz/4lmzZqlp06bBQLYOHTpk/36HEYzRYhjGUBjJMJYpJOB7AvZ/FN/DIABfEoDvghnxbS/7cH/QEggErEaNGgXOOussBYXxS8PX0OGWBEjAqwRgGMMonjp1qtZFixZZIvbve7hNwH3CjBiv9WpdWC4ScJuA/R/D7byYPgl4gUBJKURHUWP81rAXCj69xvBt3769Kls2y7oW9tu57zMCeCUdIRZsrknAnQZxoykk4BaB7du3q+nTpwcNY/gcZ5Jf5dgYxZNlP+xa0pme4SEJpAQBGsIp0YysRA4Easn1bqJdRduIFhDVAkMXBi+M3w4dOjCUmQHDbVgCMrKml9QNezGXJ9PT09XppyP4SHj5888/1Xfffafy58+vI4+UKFEi/I08SwJREkDItilTpmjDGAYyDGWbICzbN6Kfik4SXSNKIYGUJUBDOGWb1tcVS5PanyYK4xd6oqiWtLQ07efbpUsXbfyK64MSFwhzmVsSyJbAwYMHtQ/mnj1ZI1VVqlQpbGg8eSWtDh8+rPCsxIdVR48eDckjJ0MYRrAZwUN/lcgkIc/zgATyQgD9Ez/w4Ebx+eefa/9iCeFm/1D8WdKHQQydK3pElEICKUPA3tlTplKsiC8JIKZvJ1EYvl1Egz4NpUuXVp07d1bdunXTWxxTSCC3BGDQwmjYu3dvSBIwhNu0aaPy5cOcy/AiM/vV+vXr9aiyeT4nQ3j+/Plq9erVOkEswHL88ceHT5xnScABAjt37lRffvmlmjRpkt7i2CYYOv5cFEbxV6JZfxHKSQoJJBMBGsLJ1Fosa2YCmOhmRn1DXB5gLHTt2lUbv4jni9fKFBJwikAkY7h69erazSGntwwYGf7qq68UJjXZDeFffvlFrVixQvsMS2g+3W/xGnvuXAzEiW+P9OljjjlGwV0CBjIMa9xXuXJlp6rGdEggSOCff/7RIdpgFH/66adq5cqVwWuyY1woYBRDszge22/mPgl4lQANYa+2DMsViUA9uXCR6IWi2NdiXB4w6gvlqJkhw61bBA4cOKDdJMzIrsmndu3aqlmzZuYw4nbjxo16Zr/dEP7oo4+0cYyHypUrp9q1a6fdKiZOnKgkbrW68MILFSbsYUQaRgoEI9G4j0ICbhOAIQyjGIoQbZlcKJZJ/uNFx4kud7ssTJ8EnCJAQ9gpkkzHTQJ1JXEYv9D6JqOSJUta4usbwCjZ2WefrejyYMhwGy8CMIZhlO7bty8ky3r16iksp52dYDR3/Pjxyowi416EvIKBbAR9um3bttrwkP6uDeyvv/5aSYxYc4tq0KCB1uAJ7pBAHAjAZeKLL77QI8XiW2zt3r3bbk/AKIZBDF0Rh+IwCxLINQF7x811InyQBFwgUEfShOF7sWgDkz6iPJx33nnq4osv1qNgdHkwZLhNFIFIxvApp5yi6tcP/m4LWzwYEujTZgQZE+k2bNig1q1bp7Zs2aIn1hUsWFCPCiMB+B/jniJFiqiKFStqt4oKFSqETZsnSSBeBPB2YsaMGer9999XH3/8ceYoFEulHO+LwiheFa8yMR8SiJYADeFoSfG+eBBAmDMz8hscTsOoGIzfiy66SGFVNxq/8WgK5hELAfj8YmQYW7vAf7dOHfymi11gXGB02PgHIwUYxVjYpXz58rEnyCdIIA4E0G+xut24ceO0UZxpst1iKYIZKWZYtji0B7PImQAN4ZwZ8Q53CdSQ5OHvi5HfxiarUqVKqR49emjjFzF+4R9JIQEvE4hkDCNGMPyAoxWEs0Jc182bN+vRYXnlHPIoRoCrVq2qjWFMnKOQgFcJwP0HPxBhFE+YMEHt2rXLXtSFcoCR4g9EsaAHhQQSQoCGcEKw+z5TxC/rJXqlaDNDQxYKsMT4DWDkt2PHjnr0y1zjlgSSgQB8hfHFD3cJI4gggbBq0UR22LRpk/rhhx9CfI6rVKmiDYhChQopLKYBtwkj8Btu3ry5nlhnznFLAl4kgFjakydPNkaxJZNM7fbHfCnzKNGxoiHx2rxYF5YptQjYO2Jq1Yy18RoBLHLRSbSPaHfRQqKqePHi1rnnnquN306dOil82VNIIJkJhDOG4dt7xhln5OjSgJBq9lW+4GN80kknqQ8++ED7BXfv3l2HTVuz5r+3yjCwMaGOQgLJQgCTPdHXMVL8ySefWPI/Y2wRzAKdKDpSFHGKuXiHQKC4SyBy5Hd382Xq/iFQT6r6lCimwn8meqGMkBXEiO+YMWMQDzXwzjvvKHzB0wgWOpSkJyA/7vSqhUWLFg3WBRPcZs6cGQyNFryQzQ78izHhDq+T8TxcLyRclZ5YV7MmQmj/K/Z8zDluScDLBPBZj898fPbjOwDfBfhOwHeDlBuucviuwHcGvjvwHUIhAdcImF9hrmXAhH1JAK4Pl4j2EQ26PpxwwgnqyiuvVL17947qNbE8SyGBpCWAkV2MehlBmLTTTjst25XnsMAGfIMRScL4/y5dulRBIZgoB/9g+BH//vvvOowajulDbyhzm8wE4Br09ttvq1GjRiksLmMTuE6MFH1PlK4TAoHiHAEaws6x9HtKaQKgo2gf0XNFtY8DfBgR6qxPnz7aCJDzFBJIeQLwEUa8XzPRDT8CGzdujBGvmOuOsFQweiHRxCeOOQM+QAIeJIBoKSNHjtQh2cz/kRQTrhOfiI4UnSxK1wmBQMkbgdg/lfOWH59OPQK1pUrXiV4hWhHVky97S15zBTD6i7BnhQsXxmkKCfiCwJ49e9T06dODE+aiiSecHZjvv/8+uLRtrBEoskuX10ggGQjgLQliE2OUWCbbycsQy9gtm6X8o0VfE12dDHVhGb1JwHQob5aOpfIqAfiWnyPaXxSjwLof0fVBSFB8TQDuEBjBxWQgjP4iooPdnzc3cBCCCpEisIgGJsblZlQ5N/nyGRLwGoEIrhOWlBOjw8NF4Vt8VJRCAlEToCEcNSreKATKiV4r2le0uihGe61LL700cO2119L1AUAoviUA314skYwFBdLS0lSrVq3oC+/b3sCKu00ArhOvv/46Jl1bMmpsbJn1ku8I0ddFt7ldBqafGgRM50mN2rAWbhFoLglj9Bervmnf39q1a6t+/fqpq666SmHlNwoJ+JkARmzxxYxJbFj9DeHMjj322ByRYDllvPo9/vjjc7yXN5AACWQlgJXr3nrrLfXyyy+r1auDHhLwJR4nilHieVmf4hkS+I8ADeH/WHAvlEAROewleqNoE1yC7+8555wT6N+/v0LMX76iBRWK3wlgdjsWwYAglBniBWOSaDSCkGoHDx5UnTt3juZ23kMCJBCBAH6EIkrL8OHD1WeffWb3JcY/50uiY0UPRnicp31MgIawjxs/QtVryfl+oleL6qHecuXKqWuuuUb17dtXpaeny2kKCZAACCxZskQtW7ZMw0C4s/bt22tjOBo6+OKeNGmSHkGmIRwNMd5DAtERwBuaESNGqDfeeENt2xb0kEDYtTdFXxb9b0Wa6JLkXSlMgIZwCjdujFXrIPffIdpJVPcLTPTB6C+WPOZiFzHS5O0pTQALXCCag3kVCyO4Xbt2US8Ljsl0q1atUitWrFBlypThiHBK9xZWLlEE8H+G1eswSjxvXtBDApPrvhJ9VnRKosrGfL1DgIawd9oiESVJk0wvFL1btBEKYCa/3XjjjapJE+0RgdMUEiCBDAJY3W3OnDnqt99+c4QJDWFHMDIREsiWANyXXnrppcyT6xbJQ0NEPxBlTOJsCabuRRrCqdu22dWsqFy8SvRO0XRRVaFCBXXbbbep66+/npPfAIRCAmEIIJQZ/Hq3bt0a5mruTtEQzh03PkUCuSGAyXWvvPKKGjZsmNqyZYtJYp3sPC36lugBUYqPCNAQ9lFjS1XLit6UoQiFphD7984771RXXHEF3R8AhEIC2RCwr/KWzW0xXaIhHBMu3kwCjhCA28To0aPV008/bV/OGQ7FL2bodkcyYiKeJ4CFESipTyBdqvi86AbRwaLlWrRooT766CO1fPlyhRjA9AEWKhQSyIEAYgQ7Lfnz53c6SaZHAiSQAwF85+G7D9+B+C7Ed6IIBogGi+K7Et+Z6aKUFCfAEeHUbuCGUj34/14kCn9gHf7s7rvvVm3atJFDCgmQAAmQAAmQAAh88803asiQITr8mhzCPoLf8DhR+BEvFqWkIAEawinYqFKlM0TvFcXyx0pGnKzLLrsscNddd6n69evjFIUESIAESIAESCAMAYREhEGMVevkLZCxk7CM85OiX4d5hKeSmIBp4CSuAotuI9Ba9h8RbYtzxYoVs2644YbA7bffrqpUqYJTFBIgARIgARIggSgIIDLMc889h8l11v79+429NFMefUB0VhRJ8JYkIGAaNgmKyiJmQwBLIMMARixgRH2wBgwYoFeAK1WqFE5RSIAESIAESIAEckFg165dOhbxM888Y0nUCWM3IQYxDOJggOJcJM1HPEDANKgHisIi5IJAY3nmYdFz8KwE9dcGMMKgIcA/hQRIgARIgARIwBkCe/bsUUOHDlUwiGXf2E+fSer/J7rQmVyYSrwJmIaMd77ML28EGsjjD4n2EA3ABUKM34CMAjMGcN648mkSIAESIAESyJYAYhGLMQyj2LhMYLW6CaIPii7N9mFe9BwBGsKea5JsC1RXrg4WRRSIQJEiRaybbropgCgQ5crpsMBymkICJEACJEACJOA2gW3btulJdS+++KJ18OBB2FMwiBFlYrDoClFKEhCgIZwEjSRFrCWKX5qXiqYVLFjQ6tevX2DgwIGqfPnycopCAiRAAiRAAiSQCAJ//PGHeuKJJ9TLL79sHT58GHYVwq6NEX1IdI0oxcMEaAh7uHGkaBVF4QPcRzR/gQIFLAkAHhg0aJCqXLmynKKQAAmQAAmQAAl4gcCmTZvUY489pl577TUTdg0r8IwUhQ/xZlGKBwnQEPZgo0iRiogOEEUs4GJpaWlWnz59Ag888ICqXr26nKKQAAmQAAmQAAl4kcD69evVI488okaOHGkdOXIEdtY+0adEnxE9KErxEAEawh5qDCkK2qOXKIJ2VxVV5513nvZBql27Ng4pJEACJEACJEACSUBg9erVCnN4Pv74Y1PajbKDAa6xovAnpniAAA1hDzRCRhFOk+1zoogJrBo3bqyeffZZ1bZtWxxSSIAESIAESIAEkpDAzJkz1R133KEWLgxGWEPs4dtF5yZhdVKuyPlSrkbJV6FqUmT8OvxWtHnFihXVm2++qRYsWEAjOPnakiUmARIgARIggRACGNDCdzq+2/EdL4IBL3zn47sfNgAlgQTSEpi337MuLgAQCQIzSxsWLlzYuvfeewPjxo1TzZo1U4EAB+v93kFYfxIgARIggdQggO/0Ro0aqb59+6p8+fKp+fPnY0Id1gToJ1pUdL7oYVFKnAnQ2oozcMkOo/BXiT4qWkHUuuyyywIIvVK1qnYLllMUEiABEiABEiCBVCWwceNGhRCo7777LnyFYYttEb1f9C3Ro6KUOBGgIRwn0BnZtJbt86INcXz66aer5557To8A45hCAiRAAiRAAiTgHwIyMqxuv/129e238JTQslj+3iI6699D/nWbAH2E3Sb8b/qlZfOa6EzRhgiB9t5776k5c+bQCP6XD/+SAAmQAAmQgO8IwBUStgBsgozwqBgog60AmwG2A8VlAvQRdhmwJI9waJ+KtpYV4ZTEAg6gwzdsqAeF3c+dOZAACZAACZAACXiawEknnaT9h2XhLD06LPGHm0iBrxLdJPqTpwuf5IWja4R7DVhTkn5ZtCOyaNeunRoxYoQ64YQTcEghARIgARIgARIggSwEfvnlF20Uz5gxw1ybLDuYVLfWnODWOQJ0jXCOpUmpgOwgYDZ+wXUsU6aMhZApX3/9NY1gQ4hbEiABEiABEiCBsAQwYAabAbYDbAi5CQNqsClgW8DGoDhIgCPCDsKUpLAoxiuiCImirrjiCr0oRrly5XBIIQESIAESIAESIIGoCWzbtk0vxjF69GjzzFLZuUF0rjnBbd4I0BDOGz/zdEnZeUK0r2igTp062g2iffv25jq3JEACJEACJEACJJArAtOmTVP9+vVTq1atwvMYJR4hOlB0tyglDwQ4WS4P8DIevVC2n4qeASf3++67LzB27FgFY5hCAiRAAiRAAiRAAnklULNmTXXdddfpxbbmzp2rjh492lTSvFJ0g+jyvKbv5+c5Ipz71i8jj+IXGQxh1bp1a/XKK6+oE088EYcUEiABEiABEiABEnCcwM8//6xuuOEGNWtWMNTwOMkEk+l2OJ6ZDxLkZLncNXIneQx+OhcWL17cevXVV9XMmTNpBOeOJZ8iARIgARIgARKIkgAG3GBzwPaADSKPXSQKmwS2CSVGAhwRjg1YEbl9iGh/0QBGgd9++22Vnp4uhxQSSAyBAwcOqNWrV2vfMfiPrV+/Xu3du1ft27cvRO3nUFL5ANVaokSJ4L79HIK7w8UHWrt2bVW0aNHEVJC5kgAJkAAJhCWwbt061bt3bzM6DKN4uOjdogfDPsCTWQjQEM6CJOKJU+UKpm3WFV9g65FHHgncddddKl8+DqpHJMYLjhLYuXOnXoFo+fLlIYbvpk2It+6uBAIBValSpRDDuF69eqply5aqdGkufuQufaZOAiRAApEJiL+w+t///ocFu6y///4bdt0K0StEv4/8FK8YAjSEDYnIW0wovE/0/0TzY/WXd955R51yyimRn+AVEnCAwNatW9U333yjFa/Bli5dqiwLP/hDpVChQqpWrVp61Bajt5hUUbJkyZBR3syjvkjBPmJsHy3G+d27d6u1a9fqUWaMNq9Zs0YdOnQoNGM5goHcoEED1bZtW9WmTRutxx13XJb7eIIESIAESMBdAkuWLFGXX365+uknhBxW/4g+LPq46BFRSgQCNIQjgMk4XVu2GAVuIWoNGDAg8NhjjykYHhQScJoARny//PJL7fsFw3fFCvyo/08KFy6smjdvrho3bhwcmYXhW7VqVdffTGDEYePGjUH3C7hgLFy4UM2bN0/99ddf/xVS9urWrasNYxjHnTt35ohxCB0ekAAJkIB7BDBgMWjQIPXMM89g1AQ23neiGB1eLUoJQ4CGcBgoGadukO0zosWqVaumRo0apZdJjnw7r5BA7ATg3ztx4kSFkHswgg8fPhxMpFixYur000/Xo6wwKps1a+a5H2H40J0/f7423jF6/e2336r9+/cH61CwYEFtDPfq1Ut1796dfsZBMtwhARIgAfcIYHnmK6+8Um3YgOhqCh/KA0Sx4BclEwEawpmAyGFZ0VGi5+ASVod74YUX9KtmHFNIIK8ExIdLTZ48WY0ZM0Z98sknQcMxLS1NYRGWs846S4+oNmnSROXPnz+v2cX1+X/++Uf98MMP2jCeOnWqmj59ujpy5N+3cjDszz33XHXppZeqjh07KsTdppAACZAACbhDAC5uN998s7KtSveZ5HSl6HZ3ckzOVGkIh7ZbUzkcL1oN63tLaJJAz549Q+/gEQnkkgBGTrF2/Pjx49X27f9+DsHH9rTTTlMYMb3oootUqvnXws953LhxesQbQeCNj3PZsmXVBRdcoK6++mo90p1LpHyMBEiABEggBwIffvihuv76660dO3bA5sMQ8QWiC3J4zDeXaQj/19RYHnmYaEEYJh988IGqXLnyf1e5RwK5JPD555+rIUOG6FFSkwQmmGFk9JJLLlHp6enmdEpvEebnvffe0yPhmPhnBG4fd999t+rSpYs5xS0JkAAJkICDBBBd6MILL1QYkBCBD96toiNw4HehIawUgqOiM8CZXN1yyy3q6aef5mtbwKDkmgBcBGD0wQA2Rl+pUqX0akBwt6lfv36u006FB5ctW6Zf12E1xl27dukq4ccBDGL8OEg2l5BUaBPWgQRIILUJwC3vzjvvVM8//7ypKIIBYBDwgDnhx63fDeE60ugfijYQ/0XrjTfeCFx88cV+7Aess0MEMFFM+hFm7JpJCvrNwu23345XUwphzCj/EUDYNqyO9NxzzykTDxmTUyVCi7rmmmsU/IopJEACJEACzhF4//338flqyfcVbEC8noMP6CrnckiulPxsCJ8nTTVS9BgsVwgfGmwpJJAbAoie8Oyzz2oD2Pj/YsEJLLpy2WWX8Q1DDlAxUvHuu+/qEfSff/5Z3w0/YhjEd9xxh+eiZeRQHV4mARIgAU8TwOcs5kBlfN7ukcL2Ef3Y04V2qXB+NIQxDf8J0TvBFK9hX3vtNb34AI4pJBArgU8//VTddtttetEJPIuQZ/fcc4/q1q2bXnAi1vT8fD8m002aNEk99dRTOhQbWGCxkKFDh6quXbv6GQ3rTgIkQAKOEsDiSdddd51248tI+GnZDhTFYhy+Eb8ZwhWkZd8XbSM+iJaM4AUQWoRCArkhgBXXbr31VoXJcBD4uMJgQwg0St4JIPQafmAYH2tMphs2bJheQS/vqTMFEiABEiABEECIWHnzZsncFtiE34jCR3SLqC/ET4YwQqN9IlqxSpUqOipEixYtfNHIrKSzBOAHjBUG4QeMBTAwCe6hhx5S/fv3V4gFTHGOAGIQDx8+XD344IN6Uh0W6IC7BFZOov+wc5yZEgmQgL8JfPfddzqqxG+//QYQm0XPFfVFiDW/GMI9pEHfFS165pln6pimxx57rBxSSCA2AogEgVm3mNiFGMCIg/vEE08o9qfYOMZ6959//qkGDhyo4zDDfQKhDRHdBa5NFBIgARIggbwTwOcsYtpPmzYNiSGSxGWiE3CQyuIHQ/g2acBnRPPBF+all15iaKZU7tEu1U0CkWujFyvBQbDc8YsvvqiaNsWLBkq8CCxYsEDddNNNelln5ImV6rBIiSyAE68iMB8SIAESSFkCCP3Zr18/9frrr6OOR0UHiA7FQapKKr/HRd1eEH0Ajffkk08GMAEnX758OKSQQNQEZs+erTp06KCNr9KlS+tX9XhdzwVXokbo2I1gfu211yqEWJs1a5ZavHixfsODHyQ4RyEBEiABEsg9AdhI3bt3V0WKFFFTp05FQp1F8Qr9K1FLNOUkVQ3h4tJSiA98WaFChayxY8cGEMOVQgKxEDh69Kj2Be7Tp4/2T0U0CHwwtGvXjtEgYgHp8L1wSWnUqJF+hYdlq7E4x9tvv61/5LZq1Ypt4zBvJkcCJOA/AvgslYWfAhMnTrRkrkYzIdBEdKIoVqVLKUlF14hK0kKfijaC36Y0ouKkuJTqs3GpzObNm9Xll1+uELkAv5DvvfdePSGOK57FBX/UmeA1HibSyRsfhR8uiNjxzjvvqIoVK0adBm8kARIgARIITwCT6DBCDP9hkUWiiGP5Ow5SRVLNED5ZGuYz0Sp169ZVn332mapZs2aqtBXrEScCX3zxhbryyiv1P36FChX0UsBnnXVWnHJnNrkhgJF6LF29ZcsWPXFx1KhR6uyzz85NUnyGBEiABEjARmDt2rXqnHPOUStWrMBZhJU4R/RHHKSCpJLDLPxYZotWwavrb7/9lkZwKvTQONfh/vvv1//w+PXbqVMntWTJEkUjOM6NkIvs0EZoK7QZ2g4f2mhLCgmQAAmQQN4IYEARNhVsK5EqorC1YHOlhKTKiHAfaQ1McUzDSB5WiitQoEBKNBArER8CeMWOSVgYSYT7A+IEY3lk+KMmgyCqxdatWx0tKiIxHHfccY6m6XZiCK32v//9T8cZRpvi8wCzn+nS4jZ5pk8CJJDqBP7++2+9Eh2+J0WOiF4rOlI0qSU5vuWzR9xXLr8kGhg8eLD2F8z+dl4lgVACBw4c0IHEsUJc8eLF1Ycffqg6duwYepPHjxYtWmTWjHespOnp6Xq5aMcSjGNCkydPVj179lRYQhQr0n3wwQeqaNGicSwBsyIBEiCB1CSABaRgb4kgikQ/0VdwkKyS7FEjbhXwL4oGnnvuOT2hKVkbguVODIHt27fr1+kzZszQvqVTpkxRrVu3Tkxh8pArVrf7/fff1aFDh7KkUqlSJb36XcmSJZVdjznmGFW4cGE9GRCjpxhNtQvSrFq1qv1U0uzXqlVL/5iZMGGCdplAgPjzzjuPxnDStCALSgIk4FUCcJHA98NXX32FwVRMntslOs+r5c2pXMk8InyvVO4JUevll18O9O2LgWEKCURPYMOGDdoIxgSAGjVq4J9a1alTJ/oEPHbnwYMHdXi3vXv3hpQMhnCbNm2yjaGNV17r16/Xo8rm+WQeETYAVq1apdv4119/VZhAizZmvGFDh1sSIAESyD2BESNGYPENjKDAloRN9lTuU0vck8k6IjxYkD0i/pvWyJEjA/DtpJBALASWLl2qzjjjDAUDqWHDhurrr79W1atXjyUJz90Lv3gYeVj++fDh/0I9wrCFYnQ3ks9zWlqaXp2tSpUq2iDGCHEyjwibxilbtqy6+OKL9ZKhP/30kxo3bpweKS5fvry5hVsSIAESIIFcEDj11FMxiBSQFVdhDHcQhUE8QzSpJBmjRuAXx4Pyxa0XysBkGAoJxEIAs18xQgpXAhjDM2fOVAiTlgqC1YDOPPNMVaJEiZDqYLQXyxPnJMWKFUu5ZaPRtmhjtDXaHG2PPkAhARIgARLIGwHYYGPGjAnAJpOUHhR9Mm8pxv/pZDOEhwmiu2Xkyxo/fnwAIz0UEoiFAEYFEVpr165deoIcYgbDVzaVBJPCYAxj4p9dVq9erZcktp8Ltw/DMdLIcbj7k+Ec2hhtfeGFF+q2Rx9AX6CQAAmQAAnkjcAll1yiYJPBNpOU7hGFrZY0kiyGMIbbMSvxFiyZLMPwgR49eiQNZBbUGwSMT7Axgt977z0l/ckbhXO4FDCGEVs3szG8fPlyvSRxdtnBxQJuEakWcgxtjTY3xjBiDqNPUEiABEiABPJGADYZbDPYaJLSLaKw2ZJiHloyFBJlfEP0KvlytyZNmhTAMqoUEoiFAKJDYO10TIzDK3KMDqaqEWznsn//fj2BDlu7NG3aNKknBtrrEus+Imtg1Tn4hWMC3ezZsxV8iSkkQAIkQAJ5IzB9+nTVrVs3S8KSwnZ7S/QaURjHnpVkMISfFXq3y8iW9eWXXwZatmzpWZgsmDcJIE4wfjzNmzdPT4yDv2iquUNkRz6SMXz66acrRIbwo+zZs0e1bdtWu4o0b95c4cObcYb92BNYZxIgAacJzJkzR3Xu3NmSOO6wMZ8TvcPpPJxMz+uuEQOlsrcXLFhQu0PQCHay6f2RFqIf4FU4jGCZ3apHgv1kBKOVMQEOPsOZDb25c+fqCBP+6AmhtTQ+w+gT6BvoI+grFBIgARIggbwRgK0GNwnYbpLS7aKw5TwrXg6fhphowxAi7f333w9gcguFBGIlcPXVV8OJXy+WkQoh0mKtv7lfPpAUQqNt3LhRIWawERwfe+yxWXyJzfVU3sJ/GqvOwW94yZIl2l+Ycw9SucVZNxIggXgRwCBDvXr1ArKqJ4zhs0Q3iS6MV/6x5ONVQ/g8qcTbovleffXVwOWXXx5LnXgvCWgCgwYNUi+++KI28rBiXIMGDXxNJpwxjNXkYAxjJbZUmxwXTWPDNxg+42PHjtXh5TAqzDkI0ZDjPSRAAiSQPQExhJUs6BSQuV24EaOZS0VX4MBL4kVDuJ0AmiBa4PHHH1e33opVlCkkEBsBTIaTFW+0cSevaJJy2eTYahzd3TCGMQK8Zs2a4ANYaAO+wqkWMi1YwRx2sPIeAsNjZPibb75RzZo18+1EwhxQ8TIJkAAJxESgSZMmemK6LHMPV1yE+5otuk7UM+I1Q7iRkPlKtNjtt9+uHn30Uc+AYkGSh8DmzZv1srqYJPbEE0+o3r17J0/hXS4pJg4iSgIiJ0BOOOEEbfjly+f16QLugsGIeOHChRXeHEyePFnhLVTmRUncLQFTJwESIIHUJNC6dWuFCcrfffddfqnh+aKw87Z4pbZeihpRR6Dgl8JxMFxk6WTfjlB5pXMkYzmOHj2qOnTooKMAIE4sRob9OtKZuf3wQYToCDCGIaeccoqqX79+5tt8eww3EYRV++qrr7R7BIxiv/9A8G1nYMVJgAQcJYDP1z59+qi334bXq9oq2kp0FQ4SLV4ZEa4oIGaIVu7atSuW61OyXF+i2TD/JCTw2GOPqTfffFMvmYyRvcwLSiRhlRwpMuIowwj+66+/9A+DFi1a6NFgRxJPkUTwg6ljx47qnXfeUUuXLlVYWATLMVNIgARIgATyRgCfrxJfWC1atEitXLmymKTWTXSc6L68pZz3p70wIoylvb4RbYbhc4zGFClSJO81Ywq+I4BX/u3atVP45Yl+hJXVKErBVWTWrFk6PBh+YGJhkcqVKxNNBAJTp07VrjX44J4xY4bmFeFWniYBEiABEoiBwMGDB/XnK76TROaLYrThX189nEmAeMExcITUu1nNmjXVhAkTaAQnoBOkQpY7duxQl156qTpy5Ii69957aQRnNOq6deu0MYdoCJgoh4gI0RjBWHpYfrWnQteIuQ74AYU+hL6EPoW+RSEBEiABEsg7AQx0wtaDzSfSTBQ2YEIl0YYw1qPuIwH/sWCGKlOmTEJhMPPkJYB4wQgDhtXSHnrooeStiIMl/+WXX9S3336rR8ixmAZ8pxExIhr59ddf1dq1a6O5NSXvQR9CX0KfQt+ikAAJkAAJOEMAth5sPth+kmIfUdiCCZNEuka0k1pPEU378MMPA+efj4mEFBKInQDCXvXq1UuVLl1aL5lbrVq12BNJsSewQMSyZct0rbCKGkaCM68sF6nKcC1B3EeMIMsymZFuS/nzGBVv2LCh2rlzp44zfMkll6R8nVlBEnCDwOrVq5WEz1KHDx/WySNCC77zEceb4l8CH330kerZsyeM4SOiHURniMZdEjUjrbrUdKpo8QceeCBw4403xr3izDA1CCBEWvfu3dXevXvV8OHDtY9watQsd7VA1IwFCxYojAZDYATDbxoTv/CqPydFRAkY0L///rt2U6pdu3buCpICT5UsWVKPoE+cOBFhf9QNN9ygfxykQNVYBRKIK4FGjRqpd999V0fxQSQf/NAuX768Ou200+JaDmbmLQInnniiku+sgMRvh3dCV1FMntsd71Iiplu8BTPhPhYthxmEfI0db/yplR9iTW/atEnHwr3qqqtSq3Ix1gZG7pw5c9Rvv/0WfBIh02DIUXJHAH3qlVdeUfPnz9dxzRGXmkICJBA9AbxhgmYW+1Lvma/x2D8EYAMuXrwYP47KSa1hG7YUPRhPAonwEX5DKtiobt26OkwRY7zGs7lTK69Vq1apZ599VocDw1LKfu5L+FL5+uuvQ4zg1GrtxNQGfcr0LfQ19DkKCZBA9ATwP/TZZ5+pF154QWHJXQoJ2AmgfyBkJWxCESyqBhsxrhJvQ/guqV0veV2rJ8fhtS2FBHJL4LbbbtM+Z5jM1LRp09wmkxLPYSR469atKVEXr1UCfQt9DP6N6HMUEiCB2Ag0aNBA3XTTTaplSwz2UUgglABsQUyeg20oV3qJwlaMm8TTED5DavWEWP+WTG4KHH/88XGrJDNKPQKffvqp+vzzz1WpUqX0MsqpV8PYaoTwaE5L/vyJ8JxyuhbOpAeXCPQ19Dn0PQoJkAAJkIBzBGATjh07VkzEAIxh+KDBZoyLxOubrpTU5m3RNPiDYBlTCgnklsChQ4eCI3PoT9GGBMttfsnwHBcPcbeV0MfQ12699Vbd9xCKrlAhrAVEcYIAJrtCSpQo4URyOg030nSscEmeENkmeQN6tPhdunRRgwcPDjz44IMI5DBK9GTRXW4XN14jwi9JRaogLud9993ndp2YfooTgK/mmjVrFF639e/fP8Vry+p5hQD6Gvoc+h76ICV3BNavX68nHmI56+OOO05HNMGrUSh+cOB7YujQoXolxGhzcCPNaPNO9fvcZouBjR9++EG99tprChGkrr32WvX888+rmTNnqt274x5AINWb0/P1GzRokP4MkIJWFYXtmBICfw+rePHiRyVAv0wepZBA7gns27fPktiTeHViTZ8+PfcJ8UkSyAUBiYWq+x76IPoiJTYCI0aMsGQkXTPE/3B2Kj86LIkIk2MGbqSZY6Y+ucFpttddd12wzZ988klLJvhaFSpUCJ7L3B/kDYH16quv+oQ2q2kIyGCDthkz+gNsyKQWWPQ7Ra233nrL1JFbEsg1gWHDhukPTRk1ynUafJAE8kIAfQ+faeiLlNgISOzYsEaPLIZjwegBV7tedNFFOWbgRpo5ZuqTG5xmazeEy5UrZ6WlpYW0t73t7fuysI+1bds2n1BnNUEANmNGH4ANCVvSNXHTNSIgpYaPRymsINOnTx/XKsGE/UEAE8KeeeYZXdl77rnHH5VmLT1HwPQ99EU3Jil6rsIOFujkk+HyJ5NF0tJU165ddYzm5cuXqx07dijEvP7+++/VqaeeGsxx3LhxauHChcHjcDtupBkuHz+ec5OtGLZ6gR9wxcI9cD1CiDXxEdWLJOXL95958uWXX6q+ffv6sQl8W2fYjBkrDmOO2UhR2JRJJ3dIia2KFSvylxx/4DlCYPTo0foXosSitGQ1GkfSZCIkECsB9D1ZEUn3RfRJSvQEDh48aE2dOtX6448/Ij4EdwhxpTOjQdbrr78e8V5ccCPNbDP00UWn2dpHhGEfiLFryQ9L66+//spCVUJCWnXq1An2A9wvP4yy3McTqUsAbwFgQ6LtRWFTuiL//eRyNvkGktzjotbIkSO5nrizbH2b2pAhQ3Td77rrLl8vnuHbDuCRiiMA/N13361LY/qkR4rm+WIULlxYnXnmmXqSnCmsfI3rSVFmpbFKlSrpe8z1nBYxcSNNk7fft26zveWWW5T4CoeNwIJJk5MnT1byoyjYDLif4h8CMhdDiYsEKgxDGDYlbEvHxQ1DGDGF3hEtdPPNNwcwM5hCAnklgPitS5cuVZUrV1aXXXZZXpPj8ySQJwLog+iL6JPom5ToCWzevFlhZnibNm1UzZo1FYwtxGguWLCgDp8G14hvvvkmmOCWLVuC+5F23EgzUl5+O+8W2ypVqqjHHnssW5zp6enq4YcfDt6DvrBu3brgMXdSn0CnTp0UbEmpadC2TIZaD5ZCWnh9jdcqFBJwgkDbtm3165Gnn37aieSYBgnkmQD6Ij7r0DcpOROQEV/r+uuvt8Tg1dzALhrt3bt3xMTdSDNiZj674AZbu2vEpZdeGhXRlStXhvQTWYEsqud4U+oQgC0JmzLj82KwbB0VpxfUqCGlwywmhDwJ4Jc+hQTySmDevHk6piRGjeSLNK/J8XkScIQA+uKjjz6q++b8+fNVs2bNHEk3VRNBjFjEirUL/qfr1q2rJISWnkCHET9MjpMvPvttEffdSDNiZj674DbbE044ISqitWrVUljl0kxMXbZsmZ5MF9XDvCklCMCWFJtStWrVCsYwbMxRor86VTmnXSOGScEKX3nllQGuKe5UEzGdN998U0O44YYbHF15imRJIC8EsAoa+iTkjTfeyEtSKf/shAkTQoxgRAn44IMPFAzfuXPnqo8//liNHz9ezZ49W+3atSvINTswbqSZXX5+uhYPttu3b48KKaKJGCMYDzi5+mBUBeBNniAAmxK2pRQGI6ywNR0TJw3hc6RU3UqWLGlxAolj7eP7hDCBBl+QkCuuuML3PAjAWwRMn/zwww8V+iolPAGsEmYEfp8weC+44IKwk6TgKyxxhc3tESfGupFmMFOf78SD7eLFi6Oi/OOPP4bc17Bhw5BjHviHAGxLWYESo8LdRGFzOiJOGcJwYtYWurwqDGDZTAoJOEHgq6++0jFGEc+yfv36TiTJNEjAMQLok+ibGN1CX6WEJwDXESOIDSoLNZjDsNsvvvgieF48HYP79h030rSn7+f9eLDFhEgJpZcjZsQVNoKILaeccoo55NZnBGBbwsbMqDZsTtieeRanDGHEEqqFDtqvX788F4oJkIAhMHbsWL3bq1fSr7JoqsRtihEwfdP01RSrnuPV+fPPPyOmefjwYXX11VerJUuWBO+B8ZOTuJFmTnn65bqbbGXyXLZRIBBaTZZhDqKWFeboGhGk4c8d+K5n/BiqJQRge+ZZnDCE06UUA0Wtl156SU94yHOpmAAJCIEDBw4omSGsX40aY4NgSMBrBNA3Yayhr6LPUrISsI/iySIk6vHHH1e//fZb8MZDhw4pxJxv3LixiRsavBZpRNiNNIOZ+nwnXmwRCq1BgwZ6RbkNGzZo6pgoiQnSCJs1cCBMi39F3C71hClzzK0/CWBVStiaInhVhA6SLppw+VhKYIkTc+rE6mBNPEFARtjQ0S0JrO6J8rAQJBCJAPoo+ir6LCUrAVkYQfMBI7uKEWSJe4lVpEiRkPP2eyRigCUxZ61GjRpZElEimLgbaQYT9/mO02zldbYlvr0W2tLetuH2sdpcuPOjRo3yeauw+nYCsDkz+gls0IRKZ8ndkl9qR7NbMtNeeO6TQLQEunXrpjv6iy++GO0jvI8EEkIAfRSfheizlPAEJCi++eLKdnvGGWdYw4cPD3vPnXfeGZK4G2mGZODjAyfZZkxwCmnT5s2bWzLqG3IO/0OZVfzJLYli4eOWYNXDEYDNCdszo7/AFk2IwHEL0z6tYcOGhSsnz5FArgns2LFDB96X1yAWf2TlGiMfjBMB9FH0VSwWgb5LyUrgyJEj1ssvv2zJsqlZjB2MAiJgviynqh8UVwlL4jKH3CdLL1viLxqSsBtphmTg4wMn2crcIatAgQIh7dm/f38Li3YMGDDAknB6lrgXhVyvWrWqJf7i1rZt23zcCqx6dgSGDh1q+swisUVznkwQwVTO9YOS3nmiH2GZxNWrV4cNgxMhT54mgRwJjBkzRi+l3KFDB73efI4P8AYSSDABLCc/ZcoUhb5Ln/bIjQE/aiyK8Msvv6j9+/drH1GExCpatGjkh3K44kaaOWTpm8vxYov40YsWwZ5RejJUmTJlfMOYFc0dAcwtQEzyjPkG50squXKTyO3KcjCg/w9Fv++++2gEAwTFUQIIrQOBIUwhgWQggL4KQxgxWGkIR24xGLxNmzbVGvmu2K64kWZsJUjdu+PFFqsMiltM6oJkzRwnUKhQIW2DIpKECGzSCaIYJY5Jchs1oofk0lBeXahrrrkmpgx5MwlEQ8AEdG/Tpk00t/MeEkg4AdNXTd9NeIFYABIgARJIcQKwQWGLimClFdimMUtuDOGQ0WCsAkQhAScJbN26Va1YsUIVK1ZMNWnSxMmkmRYJuEYAfRV9Fn0XfZhCAiRAAiTgLgHYoPBMyBCMCsfs8psbQ1iPBlerVk0HPje5c0sCThEwbhESkkpJuB2nkmU6JOAqAfRV9FmI6cOuZsjESYAESIAEtC0Km1QkV6PCsRrCHA1mp3OdgDEi2rZt63pezIAEnCRg+qzpw06mzbRIgARIgASyEsjrqHCshnBwNPiqq67KWhqeIQEHCBgfS+Nz6UCSTIIE4kLA9FnTh+OSKTMhARIgAZ8TgE2a21HhWA1h+F+oQYMGKfoG+7zXuVT9nTt3qqVLl6rChQsriSPqUi5MlgTcIYA+i76LPoy+TCEBEiABEnCfAGxS2KYZom1Vc5DTNhZDuLUk1lCCmiuOBueElddzS2DOnDlKAmgrWXWIYflyC5HPJYwAwvmg76IPoy9TSIAESIAE4kMAtilsVBH4CsNmjUpiMYT7IsVrr71WyQoxUSXOm0ggVgLLly/XjzRu3DjWR3k/CXiCgOm7pi97olAsBAmQAAmkOAHYpraQvtpmjabK0RrC5SSxnlgGE4YwhQTcIrBq1SqddJ06ddzKgumSgKsETN81fdnVzJg4CZAACZBAkMB1112nYKvKiZ6isF1zlGgN4T6SUqGuXbsGMgIX55gwbyCB3BAwxoMxJnKTBp8hgUQSMH0XS89TSIAESIAE4kcANipsVcmxkGifaHKOxhBGgjcgsb59ox5pjiZv3kMCWQgY48EYE1lu4AkS8DgB03fNjzqPF5fFIwESIIGUImCzVWG7wobNVnK8QZ4+S3RKenq6WrNmDYacs02QF0kgtwQOHDigihcvriOSYJ99Lbck+VwiCRw9elQVLVpUHT58WO3bt0/vJ7I8zJsESIAE/EQAn8G1atVS69atQ7U7iE7FTiSJxqrVw8DXX389DZNIFHneEQIYDcZse3RgGsGOIGUiCSCAvos+jL5s3nAkoBjMkgRIgAR8SQCfwbBZMyRHV4acDOEKktC5snSodfXVV5tEuSUBVwiYV8nm1bIrmTBREogDgdq1a+tcTJ+OQ5bMggRIgARIIIMAbFbYrnJ4rihs2YiSkyEM6zf/+eefHyhfvnzERHiBBJwgYIwGY0Q4kSbTIIFEEDA/5kyfTkQZmCcJkAAJ+JUAbFbYrlL//KLZjuTmZAhfCIhcQAMUKG4TWL9+vc6iZs2abmfF9EnAVQKmD5s+7WpmTJwESIAESCALgT59+phz2pY1B5m32RnC1eXmhiVKlLDat2+f+Tkek4DjBPbu3avTLFmypONpM0ESiCcB04dNn45n3syLBEiABEhAqTPPPFPBhhUWWGkONm1Yyc4Q7oEnzjnnnADWcKaQgNsEMMMegsgRFBJIZgKmD5s+ncx1YdlJgARIIBkJwHaFDZtRdm3ThqtHjoZwjx4Rnw2XHs+RQK4JGKPBGBG5TogPkkCCCZg+bPp0govD7EmABEjAlwRsNmxEYzaSIVxWiLWGNd2lSxdfwmOl40/AvEaWVxnxz5w5koCDBEwfNn3awaSZFAmQAAmQQJQEYMNmeDW0lkdg22aRSIZwV7kzLcO/IstDPEECbhAwo2dmNM2NPJgmCcSDgOnDpk/HI0/mQQIkQAIkEEoAgxKwZUXSRGHbZpFIhvB5uNM2pJzlQZ4gAacJGKPBGBFOp8/0SCBeBEwfNn06XvkyHxIgARIggVACNls2rHtEOEO4qCTRMRAIWN27dw9NjUck4CIBYzQYI8LFrJg0CbhKwPRh06ddzYyJkwAJkAAJRCQAWxY2rdzQURQ2boiEM4SxLnOR0047LVChQraLcYQkxAMSyCsBYzQYIyKv6fF5EkgUAdOHTZ9OVDmYLwmQAAn4nQBsWdi0wgFG8FmZeYQzhNvgpo4dYThTSIAESIAESIAESIAESCB5Cdhs2raZaxHOED4NN4n1nPleHpOAqwQ4iuYqXiYeRwJmJNj06ThmzaxIgARIgAQyEbDZtFmM28yGMFbOaAxfiubNm2dKhock4C4BYzQYI8Ld3Jg6CbhHwPRh06fdy4kpkwAJkAAJ5EQANm2Gn3BjuTdklbjMhnAjuaFQvXr1AmaJ0JwS53UScIqAMRqMEeFUukyHBOJNwPRhE0843vkzPxIgARIggf8IwKaFbStnConC1g1K/uDevzt6yPj000/PdJqHJOA+AWM0cBEC91kncw6rV69W06ZNU4cPH9bVKFy4sDr//PNV2bJhY6UnpKqmD5sfdwkpBDMlARIgARIIEoBtu2zZMhzD1p1nLoQ1hG2+FOY+bknAdQLGaDDxVdfWAABAAElEQVSjaa5nyAySkgCCo2/YsCGk7DA877jjjpBziTwwfdj06USWhXmTAAmQAAn8O/fttddeAwoYwkMNk8yuEXpEmIawwcNtPAkYo8EYEfHMm3klBwHLshQ0s/z999+ZTyX02PRh06cTWhhmTgIkQAIkYA8CoW1dg8RuCFeWk1VLly6tTjjhBHOdWxKIGwFjNBgjIm4ZM6OkISCTHdRnn32mXnjhBfh7ebbcpg+bPu3ZgrJgJEACJOATArBtYeOKVBWFzavFbgi3wJkWLVpgZt2/V/mXBOJIwPgI7969O465MqtkI9CgQQN10003qZYtW3q26KYPmz7t2YKyYCRAAiTgEwKwbWHjZkhwx24In4iLJ598srmJWxKIK4Hq1avr/NauXRvXfJkZCThNwPRh06edTp/pkQAJkAAJxE7AZuNqmxcp2CfL1cSJmjX1Bru+loMHD6pJkyaphQsXqo0bN6p//vlHv4o96aSTFEakatWqpdLS0nzNyOnK16lTRyeJqABeExMFgCN8XmsZb5Zn1apVumCmT3uzlCwVCZAACfiLgM3GDRq7NITD9IEhQ4aoRx99VBnjB78g4Ov34YcfqiNHjugnsHb1yJEjVadOncKkwFO5IWCMBmNE5CYNJ55Zv369Gj16tPrmm2/U4sWL1c6dO/UPIaRdrlw5hXJedNFF+vV8/vz2fyEncmcaeSFw6NAh9dNPP+kfsIsWLdIh1vD/e8opp6iGDRuqeMVHNz/mTJ/OS534LAmQAAmQgDMEojKEMdLpZxk4cKB68skngwhefPFF1b9/f338+++/q2bNmqlNmzapLVu2qG7duultmTJlgvdzJ/cEateurf3T16xZo44ePary5bN77uQ+3ViefOWVV9Stt96qYFCFk23btino3Llz1Ztvvqm+/PJLValSpXC38lycCcyYMUP16tVL/0+Gyxqj+c8884y67rrrwl127Bz6Lvow/NHQpykkQAIkQALeIGCzcYMjwmZWHJabOyijW/ngEuDXUa79+/froPzGCGrSpIn6/vvvQ1pvypQpqmPHjsFz48ePVz179gwecydvBKpUqaJ/aKxbt04lwr8SI/1//PFHlkpgpincY8xbAnMDRobff/99c8htHAlcf/31KiMmpB6px8i9eWOTXTE6d+6s3nnnHdcW4MAbhfT0dFW5cmX122+/ZVcUXiMBEiABEogjAXyPFylSBN/nRyXbIqKHzZBbuhzkq1atmm+NYKm/mjp1ashIYLgV9jp06KDuu+8+PVpZqFAh1bgxlq2mOEXAvEpOlHuEcaSH/3fXrl0VRoiXL1+uduzYofbs2aN/GJ166qnB6o4bN06/hg+e4E5CCGCU3hjBGIXFWxyEWBs8eLDq3r17yNsFjOL37dvXtXKavmv6smsZMWESIAESIIGYCGCgF7auCOzfdOwYB0c9RGzzncA13wlGw+0C4yecPPbYY+raa69VpUqVMjHpwt3Gc7kgACMGr7hhTJx11lm5SCFvj0ycOFHNmTNHT4g87rjjsiSGtwSffPKJjrVtYsXCF5U/iLKgivsJuNLcdddd6qGHHlL4kWqXb7/9VvXp00f3K5zHm5wPPvhAXXjhhfbbHNmnIewIRiZCAiRAAq4QgK2bEdkHtu9KMyJMQ1honHHGGXrI3JD/4osvgqNM5pzZ1qhRg0awgeHg1oyiGWPCwaSjSqpw4cIKS/jajWCsZIa4sGb1MvgE4x4jiSqryZ/bfwnccsst2r8/sxGMq3i7M3nyZD3p1fDC/W6I6Q/0D3aDLtMkARIggbwRsA36atuXhrCNZ/ny5XVkCIz0QjAifOeddyqMFOPXw4gRI9Q555yj7r//fttT3HWSgFktDGHrEiWbN29WgwYNUm3atNHhBGEco08ULFhQYcIVXCMQUcIIJk5SEksAvuV4U5OdwG/34YcfDt6CdoMvutNi+q7py06nz/RIgARIgARyT8BmCNdAKsYQLosDGIJ+l7PPPltP1kL4NMjQoUNV0aJFddzgfv36qc8//1x/4W7YsMHvqFypP1YLw2z7efPmhfhru5JZpkThRH/DDTfoiU6PP/64mjVrlvr11191CC5zK9whfvjhBx1SzZzDiDElsQTwowX/pzkJ/L7t8uOPP9oP87yPibbou+jDXl75Ls8VZQIkQAIkkKQEbLZuOVTB+AgXxwFi5fpdMPqLEd9hw4ZpFBgJRGQAvBaH7yoMI7hFMGSWOz0F0RmwYAkMlPnz56vWrVu7k1GYVG+88cZgFAJzGe1ft25dhWgSmECHUUSM+GX2Jzf3c5sYAlhDPhpB6BxMlsCPHsiyZcv0ZLpono3mHvTZv/76S6/QmbGmfTSP8R4SIAESIIE4EbDZutroNYZwMeRfrJjexKko3ssGI3uXX365+uijj3ThsHgCvthg+BpBaC2c56pyhojz27Zt22pDGO4H8TKEJ0yYEGIEw7/ziSee0LGiM/ucHj58WMG/FBElKN4gsH379qgKgsgfxgjGA06vFDhz5kxdDvRhCgmQAAmQgPcI2GxdbfQa1wgawtJWMIaMEYymg3+w3QjGOQyp0wgGCfcEr7khxqhwL6f/UrbnBV/S2bNnqwsuuCBL9AE8AV9h+2gfXoNTEksAKwBGI5ldIbDanJNifMdNH3YybaZFAiRAAiSQdwKRDGG6Rghb+ITapX79+vZD7seJgDEiEPLKPnrnZvYY+Tdy/vnn5+gvj4giRugjbEgkbgsDFHHAcxLEFTaCHzBYetkpQV9Fn4WYPuxU2kyHBEiABEjAGQKZXSM4ImzjumvXLtuRUlhSOTsZM2aMateuXdiVyLJ7jteyJ4DQZfDLxUp/mJgWb/nzzz8jZgm3iKuvvlotWbIkeA9HhIMoErqDpZOziwKBpdO//vrrYBmxwpyTrhHoq+iz6Lv28HvBDLlDAiRAAg4TQHSrp556SoeIRAx1+8qo+HEOOwXhPrES59KlS0NynzZtml4ZF4M/WDXXL5J5RNjUe6PsWBs3bpTBLf/Kq6++iun/QRU/v4gwxNfQklfolviSWjJTPOJ9vJA7AhK9QbfDkCFDcpdAjE9JRJBgu6MPSCiukP8HmQBlvfXWW5a8JQi5D/f27t07xtx4uxMExPDN0hbyS996/vnnLVnmWGdx4MAB67vvvrNkWfSQe0uWLBnSvk6UR76MdB7ouxQSIAESiAeBXr16hXy2yUJUwWxlHkvINXzuyY91fV2M4pBr+C77/vvvg8+m8g5s3QxbD7ZvUHbKnrVz585UrnuOdZOIEJaEYDKA9PbBBx+0ZOnWkGdlxNCSSVz6+qRJk0Ku8cAZAu+++67mK0taO5NgDqnIYgsh7Y7/B6hEsNDGr6xNHvY67pEoBJbEsbUaNWpkSUSJHHLi5bwSkNCGlvj2au6mnSJtZbW5sO02atSovBYjy/PoqyiHjMBkucYTJEACJOA0AYleZMlk7iyfcbLugc7K2Cn2z8eRI0fqa/fdd1+W5/zyIx62bgYT2L7BOMKcLCcwZIRXiWGrsICCEbxqaNGihRo4cKBetQpLK2MCHZbhHT58uMocl9Q8x23eCCCeMyalTZ8+XW3dujVviUXxtBgx6uabb85yJ14lIcSWPVwaViBE2xvB66fffvtNYallvIaiuEtA3hIoTI6z+483b95cderUKUvGR48eDTmHya6YFCuj+CHn83qAPoq+ij4LlwsKCZAACbhNAG55meOnI8rRMccco7O2uQAEi3LsscfmeC14c4ru2Lho29dU87Ds8BV/xs81MXz06+4CBQqYXw0hW4z8iG+N0z/umF4mAt27d9fcX3jhhUxX3DnEyP/LL79slS1bNqS98b+BkUVZKUy7RyB3uMM0a9Ys5D6JLW2JD6o7hWOqQQJwY8n8v9m/f39LYn1bAwYM0O5K8gUR0jZVq1a1xLfb2rZtWzAdJ3fQR9FP0GcpJEACJBAvAvfcc0/IZx1cxozIAmCWRLkKXj/++OODb7hlBVULrmT43ILibbgsFGYeTektvr8z6g3bV5m4TxgeLgWna3tYKNzgZ9m7d69as2aNXkQDo09YxhVL89lWJfEzHtfr/t577ynxf9KTADACHy8Rv1I9CvzLL7/oyU9Y4ANhtjL/8o5XeZhP7AQw8RUj9BBEhihTpkzsicTwBFaRQ8SIsWPHqksuuSSGJ3krCZAACeSNwIIFC/TbbJkLoVq1ahWSmPjDqnfeeUfbLuedd55+a2Vu2L17txI3RCVWr15DQXyIzaWU3oprhPlOgO1bxhjCcBiuAmAw9igk4AUCMEgx+x5b8XnSriteKBfLQAJ2AohUgR/I+KEEFwn+YLLT4T4JkAAJeIsAXBnlLSEK9ZtoVRM+bT/OIPQPhQS8QgAGxbnnnqt/rWJ0mEICXiSAvokRFfRVGsFebCGWiQRIgAT+I7Bv3z5zoI3eEEPYdtHcxC0JJJTApZdeqvPnJLSENgMzz4aA6Zumr2ZzKy+RAAmQAAkkmIBt0DfEENbmse1igovJ7EngXwLweZLJazoQOKI3UEjASwTQJxFZBH0UfZVCAiRAAiTgbQI2W1fbviEjwraL3q4FS+cbAhIdQF1wwQW6vqNHj/ZNvVnR5CDw9ttv64Kij6KvUkiABEiABLxNwGbrhowI6wO6Rni78fxaOixpDJFVchQieVBIwAsE0BdlNUpdFNNHvVAuloEESIAESCAyAZutG2II0zUiMjNeSTABiderZLlrhZBYxvBIcJGYPQnovog+ib6JPkohARIgARLwPgHbiHCIa8R2FP2PP/7wfg1YQl8SuPvuu3W9n3vuOSULJ/iSASvtHQLog+iLENM3vVM6loQESIAESCASAZutuw33GB/htThArFYKCXiRQJcuXRQWtti0aZMOAO7FMrJM/iGAIPToi+iT6JsUEiABEiCB5CBgs3V/RYlpCCdHu7GUQsCMvP3vf//TcVsJhQQSQQAxg9EHIaZPJqIczJMESIAESCB2AjZDWI/+0hCOnSGfSBABLF1brVo1tXz5cr2cZIKKwWx9TmDSpEm6D6Ivcjlln3cGVp8ESCDpCEQyhNdJTY5u2LBB/fPPP0lXKRbYHwTy58+vBgwYoCv71FNP+aPSrKXnCJi+h76IPkkhARIgARJIDgKwcWHrihwVXYedAP5kCK5UXbNmjapZs6Y5xy0JeIoAZntWr15dbd++XU2bNk21b9/eU+VjYVKbwPTp09WZZ56pF9BYv369KlasWGpXmLUjARIggRQigNHgWrVqoUYbRathJx/+ZIj2lbANGZvz3JKAZwjA8DCjwrfeeqs6cuSIZ8rGgqQ2AfQ19DkI+iCN4NRub9aOBEgg9QjYbFxt86KGNIRTr51TvkZ33HGH/kX3008/qeHDh6d8fVlBbxBAX0Ofw2gC+iCFBEiABEgguQjQEE6u9mJpIxAoVKiQGjp0qL764IMPqj///DPCnTxNAs4QQB9DX4Og76EPUkiABEiABJKLQE6G8M+ozo8//phctWJpfUmga9euOn4rVvYaOHCgLxmw0vEjgD6GvoaYweh7FBIgARIggeQjYLNxtc2LGtgny1WW499Kly6tJyIFAvZLyVdZljj1CaxatUqddNJJeqW5efPmqaZNm6Z+pVnDuBNYsGCBat68uSpQoIBatmyZql27dtzLwAxJgARIgATyRgAx4MuWLat27tyJhKqIbsKO3UcYJzbihl9++QXXKCTgaQJ16tTRk5bQuW+66SYusuHp1krOwtn7FibI0QhOznZkqUmABEgAtm2GEYyIEdoIBhW7IYzjufrPXL3BLoUEPE1g0KBBqnLlymr+/Pnqrbfe8nRZWbjkI4A+hb6FPoa+RiEBEiABEkhOAnP/s21DjFwawsnZnix1BgGEsHr66af10Z133mkCZZMPCeSZAIKuo09B0McYLi3PSJkACZAACSSMwLfffmvyztkQtt1sHuKWBDxLAMvcnnvuufqVR69evbg6omdbKnkKhtWH0JfwGg19i0spJ0/bsaQkQAIkEI5ApBHhzDPiCsrDe2SiXEH5AgiULFkyXFo8RwKeI7Bjxw7VsGFDtXHjRnXfffepxx57zHNlZIGShwDcIB5//HFVtWpVtXjxYlWmTJnkKTxLSgIkQAIkEEJg9+7dSoJByLQP67BcOEYUWy2ZXSNw4Qe5MYBZ+BQSSBYCMFTGjBmj0tLS1JNPPqmmTp2aLEVnOT1GAH0HfQh9CX2KRrDHGojFIQESIIEYCcCmhW0rj/0gGjSCkUxmQxjnvsMf2xAyDikk4HkCrVq1UoMHD1ZHjx5VV1xxhdq6davny8wCeosA+gz6DvoQ+hL6FIUESIAESCC5CdhsWm3j2msTzhCeiRu++uor+33cJ4GkIAC3iPbt26stW7ao3r17M6RaUrSaNwopowW6z6DvoA+hL1FIgARIgASSn4DNptU2rr1GmX2Eca2I6DbxEy7y+++/BypUqGC/n/sk4HkCmzdvVqeccopeevmpp55Sd999t+fLzAImnsCQIUPUPffco4499li1ZMkSVbFixcQXiiUgARIgARLIEwEMblSqVEnGOqyDklA5UWyDEm5EGDdMhi/FxIkTgzdyhwSShQAMmFGjRimsjohJT5MnT06WorOcCSKAPoK+gj6DvkMjOEENwWxJgARIwGECsGVh00qyMAZCjGBkFc4QxvkJ+PPxxx9jQyGBpCNw9tln61fbCIPVs2dP9f333yddHVjg+BBA30AfQV+BOwT6DoUESIAESCA1CNhsWW3bZq5VONcI3FNW9I+CBQum/fnnn+qYYxBpgkICyUegT58+eoQPr7vnzJmjsCwzhQQMgVWrVqmWLVtqN5orr7xSjRw50lzi1iECq1evVtOmTVOHD/87Ubtw4cLq/PPPV2XL4muG4jUCbrSXG2l6jRvL400Ce/bs0e5u8vlzREpYXnR75pLmz3wi4xg3zpIH233xxRfq4osvjnAbT5OAtwm8/vrr2sj5/PPPVadOnRQWi6Hfu7fbLF6lg98Y+gR+7Hfp0kWhr1CcJ3DmmWdmWfFx79696o477nA+M6aYZwJutJcbaea5okzAFwRgw2b8CJ8lFc5iBANCJNcIXKN7BChQkppA/vz51QcffKCaN2+ufv31V/3aG78QKf4mgD4AFwj0CfQN9BH0FYqzBMQvL2zklr///tvZjJiaIwTcaC830nSkskzEFwRycosAhBwNYRlJs8wrLV9QYyVTjkDRokXVZ599purWratXCevRo4c6dOhQytWTFYqOANoefQArxqFPoG+gj1CcJ4DJh+D7wgsvqHr16jmfAVN0lIAb7eVGmo5WmomlLAHYrrBhMyoY1j8Y17IzhNfL9cXyCisA/y4KCSQzAfgjfvnllwihor7++uvgognJXCeWPXYCZrEV9AH0BcSWpK9q7BxjeaJBgwbqpptu0r7YsTzHexNDwI32ciPNxNBhrslEALYrbFgp82JR2LRhJTtDGA98gD+cQAIKlGQnUL16dW0MlypVSr8Kv+SSSzgynOyNGkP5MRKMNocbBPoAfhhVq1YthhR4KwmQAAmQQLIQsNmu47Irc06G8Jvy8D8fffSR9ccff2SXDq+RQFIQwMgEXtUaYxh+ovQZToqmy1MhjU+wMYLRB9AXKKlLABPyoBQSIAH/EYDNCttVav6P6FvZEchpdsgWeXiCxNe84M0331QDBw7MLi1eI4GkIHD66aerWbNm6YgBeEXetm1bhZmljCaRFM0XcyERHQI/eOATbNwhTjrppJjT4QPOE8Ao/U8//aQWLlyoFi1apGd3n3zyyXplyIYNG6qSJUtGlen69evV6NGj1TfffKPbeefOnTouNB4uV66cDpt40UUXaRcNToqMCmnYm5xqL3vibqRpT5/7/iQAm1VsV7hFwDcYtmye5Cx52kpPT7eOHDkiE0ApJJAaBOTL05LJUvjFaNWoUcNauXJlalSMtQgSQJuibdHGaGu0OSUxBK677jrdDmiLJ5980pIfoZb8+Ayew3m7lihRwnr11VdzLOyIESOsQoUKhTxrT8e+L28BrE2bNuWYJm+wLDfay4002VYkkJkAbFXYrBn/+7Bh8yywqFeJWvI6MXN+PCaBpCawbds2S8Jn6X8YWXTDWrBgQVLXh4X/jwDaEm2Kzy60MdqakjgCdiNIRmmttLQ080WV7bZz587Ztl358uXDPl+6dGkLxjTa364yMpw4CEmUsxvt5UaaSYSURY0TAdiqGf/zsF1hw2YrOfkI42Ek+Ap25Jc3NhQSSBkCiBgwffp0vaACFlY444wz1OTJWI6ckswE0IZoS7NYBtqY0SG806Lyo0TJqI0uUO3atVX//v11iLXBgwer7t27q3z5/vtqwqTGvn37Riw8XCkgYlirrl27qldeeUUtX75c7dixQ/v/YwntU089Nfj8uHHjtCtG8AR3ciTgZHuZzNxI06TNrb8J2GxV2K6wYR2RcpLKX/LhdHTDhg1xsumZDQnEj4AE+LdkiV39K1J8CK2nnnrKklBb8SsAc3KEANoMbYc2lM8s3aZoW0riCdhHA9E28n1i3XPPPdZff/2VpXCyHLoly6HrNsS9UDFgs9yHEwcPHrSmTp2KCd1hr+Mk3CGKFy8eTE9WEYx4Ly/8S8CN9nIjTbYXCdgJwEaFrSqfGX+JwnZ1VN6V1KwHHnjAnif3SSClCAwaNMiSAPD6C1OW3832yzWlKp4ClYEhhDbD5xTaEG1J8Q6BzEbQbbfdlm3hZNW/EOMV/sTRCn4Q7dq1C4tBBR8599xzg4YwDHBK9gTcaC830sy+FrzqNwKwUfEdIAqbNSr57/1Tzrdrvwj5Ja24PGbOsHhHchJ49NFHdXg18S3Viy2ccsopSkabkrMyPio12ghthQUy0HYIj4a2pHiTQJUqVdRjjz2WbeFksot6+OGHg/cg+se6deuCx/adzZs3K/nho9q0aaNq1qypChcurEMkFixYUImfsHaNQEQJI0iLEj0Bp9sLObuRZvQ14p2pSAC2KWzUDInalzcWQ3iWJL4YHzgIS0EhgVQlgFBbS5YsUe3bt1f4wpRRRv0lK6FYUrXKSVsvtAkMILQR2gpthrZDG1K8SwAGazTLWsPn1y4//vij/VCHSLvhhhsUjObHH39ch0WUkWQdhs3cuG/fPvXDDz8ohFQzIqNkZpfbKAg41V72rNxI054+9/1HALYpbFQRrCQHmzUqicUQRoIP4Q8+cLCGM4UEUpVAxYoV1ZQpU9Qjjzyi5DW77vOINyz+R6la5aSrF9oCbYLPI7QR2gpthrajeJvACSecEFUBa9Wqpexxf5ctWxby3I033qgkxFrI9xEWy2nRooXq0aOH6tmzp17auUiRIiHP8SA2Ak61lz1XN9K0p899fxGATYrvggzRtqo5yGkbqyH8iSS4GF9AHBXOCS2vJzsBzFy///771YwZM1TVqlXVt99+qxDkH32fI0qJa12wRxugLdAmaBu0EdoKbUbxPoHt27dHVUisCGh/EwM3ByMTJkxQr732mjlUiD6BlQPxZmDu3Lnq448/VuPHj1ezZ89W4i+sMHJMyR0BJ9orc85upJk5Dx77hwC+EzIGqjAaDFs1aon1WwPvk7Sl/cQTT4T8Co86R95IAklGoFWrVnq1Kplso1+vXnPNNXrESeLUJllNkr+4YI7RPrQBXnWjTbBiHNqIkjwE0GbRSGZXCPz4MTJz5kyzq10jYPBecMEFShbXCJ43O/AVlrjC5lC/QQgecCdHAk60V+ZM3Egzcx489geBMKPBMfk+xWoIg2pwVPiNN97wB2XW0vcEypQpozACNXbsWFW5cmU1f/58JYs0qGuvvVbHqvU9IJcBIB4wWIM52KMN0BZoE7QNJbkIYOJaNJNQEVfYCNxfMCHSCPqBkfPPP1/JwhrmMOwWy6gb4RsdQyK6rRPtlTknN9LMnAeP/UEAtujGjRtR2ZhHg/FQbgxhjgqDHMWXBC655BL1yy+/qHvvvVcVKFBA4R/w+OOPV88//3xwgQBfgnGp0lh0AWzBGKzBHOzRBmgLSvISkFBaEaNAoFayDLOSZZiDFZQV5nQEiOAJ2w5+KEUSjBZdffXVehKluQdGNSU2Ak62l8nZjTRN2tz6gwD+v+GhkCHwWIhpNNg8mJstPkUWIcPhw4fLj2sKCfiPwMqVK60uXbrgn05rgwYNLFnBzH8gXKrxtGnTLDA1fMEazCnJSSBzDFm0Kxa5kB861vr163WlDhw4YH333XdWx44dg+2O+0qWLGnJiE9Ixfv16xdyj4RjC7kHC3W89dZbVv369UPuQ3q9e/cOSYsHWQk43V7IwY00s5acZ/xEADZoxncEbNK4/8LtgcwlFmDYlYH81BCsq78JTJo0yZLZ7eaf0Tr99NOtTz75hCvT5aJbYCEEsAPDjA83zRaMKclJQOI5W+LbG1ztz7RruC1Wmwt3ftSoUVkqL8toh70XP55g/EqkiLDXkT5WHsR3V6NGjayFCxdmSdvPJ9xoLzfS9HMbse7/EsCPXfwfZ3xmwCaNuwRHhYcOHcp2IQFfE8A/pIRuscqWLWv+Ka169erpESl5deNrNtFUHowwenfiiScG+YElmIZbgjeaNHmPNwgcc8wxwTaVbym9L77ewVUAzblwW/H7tcQPPGJFbr755ixph0vnjDPO0G8vw1278847I6bvxwtutJcbafqxbVjnUAKwPTP+pxMyGix5a+ksf/Ha6mh267yHFp1HJJC6BCR4vzVs2DCrWrVq5h/Ukold1tNPP21JKKjUrXguawYmYANG+CyBgh0YgiUl+QnAhUF8u4Ptizbu37+/JatAWQMGDLAk7FlwWXPTByQkniV+vda2bduyBSA+5NbLL78c8gPUpIHRZfNjFIkcOnTIatasWUg5KlWqZIkfcrZ5+O2iG+3lRpp+axfWN5QAbE7Ynhn/77BFcy1O+FN8LLn3uPLKK9XIkSNzXRA+SAKpRACxT9977z01ZMgQtXTpUl01BPpHLNMrrrhCyavbVKpuzHXBwgijR49Wr7zyio7xigTklba6++679SQ4+yIKMSfOB5KOAOL8LlqEQR2lI0PEGglEfIsV+hQmUe7fv1/3JYRai2b1uqSD5YEC57W9wlXBjTTD5cNzqUGgT58+SlymUJkJouflpVZOGMLpUoDlooXnzJkTEN++vJSHz5JAyhH4/PPPtUFsj3t68sknq169emmtXr16ytU5XIVkQpQOeYawZ/b4sFgdDgawTIYL9xjPkQAJkAAJkECQABZSatmyJd7u/CVaT3SdaK7FCUMYmT8g+jBiPGJN97S0tFwXiA+SQKoSmDdvnl4RDatd7dixQ1cTYZxOO+00demll6oLL7xQHXfccSlV/a1bt+rVvsaMGaNX+5KXW7p+GPHD4gdYGENeV6dUnVkZEiABEiABdwggpGaTJk1MOMT/k1weyWtOThnCWMoHi8DXQsxPmcCQ13LxeRJIWQLiG6lkxruCcSgREvSrXFQWPyDbt2+vOnTooNq0aaP/2ZPNRQAuIfgxjGD5U6ZMURJOLhhfuVixYnolOBj9Eh5LxwRO2UZmxUiABEiABBwn8MILL6hbbrkF6a4RhY/hIRzkRZwyhFGGc0Q/RbxHifUZSLWRrbxA5rMkEIkAfBsnTpyojeKvvvoqZNlyGI5wNYLrAAxjjJyGWz42UtrxOC8TkPRKbzB84fqBV1bw0TSCpW07deqkR7y7d+9On00DhlsSIAESIIGYCOANY506dTDxHLZrV9HPYkogws1OGsLIYqJoN06ci0Cbp0kgGwI7d+5UWAbWGJUrVqwIubtw4cJ6ieHGjRvjwyCoMsNeyQz5kHudPpD4vnoJy1WrVimjEn9Vwd1DwpuFZFe3bl1tvMOAx2pgpUuXDrnOAxIgARIgARKIlYBtgtwkebZ7rM9Hut9pQ7iGZISJc4Vmz54dEGfmSPnyPAmQQA4E8OsXRrExjBF9wvjY2h/FKLEs6KENYwlFpWrWrKnkzYySVbu0lihRIrhvzuF5CU8Wonv37g0e7969W61du1atXr1aG75r1qxRGP3NLPBxRrQHM2qNkWu+DcpMicckQAIkQAJ5ISDBGFSrVq0wyQRfRJgg92te0rM/67QhjLQHiz4o8Ru1ryBGsSgkQAJ5J4ARY3wYLF++PDgqC0N106ZNeU88hxRg8ErMVQVD24xG438cP3Y54psDPF4mARIgARLINQG8dcQEOXz3iTwkOhg7TokbhjAmzs0XPRmT5jB5jkICJOAeAfgZm5FbuC0gTJl9dNe+b0aBURozOmy29pFj7COsmzF6YQAzJqt7bciUSYAESIAEwhPA5DhMkhP5URRhhrK+nsTVXIobhjCK0kB0gWhBmQAUwAxxCgmQAAmQAAmQAAmQAAlESwARlmTCNVwiDos2Ff13hapoE4jiPrcMYWR9h+gzFStW1CtrlS1bNori8BYSIAESIAESIAESIAG/E9i+fbueg7J582agGCD6rBtM3Jxq/pwUeDoqcP3117tRdqZJAiRAAiRAAiRAAiSQggRgO2YYwdOlerApXRG3l4D7Wkp91c8//1w4PT1dYe13CgmQAAmQAAmQAAmQAAlEIjBy5Ej15JNP4vIu0U6iu3HghrjpGmHK20t2xsiEHOvHH38M1KhRw5znlgRIgARIgARIgARIgASCBH799Vd18sknWzK5GzbqpaJjgxdd2HHTNcIUFxUYiwpdfvnlweVWzUVuSYAESIAESIAESIAESODIkSMKtmKGEaztR7epuO0aYco/TXYu27hxY8m0tDQdfN9c4JYESIAESIAESIAESIAEHn30UTV69GiA2CiKZZRDly7FFYclHq4RpshnyM4UCcyf79NPPw106dLFnOeWBEiABEiABEiABEjAxwQ+//xz1bVrV1lA1ToqGDqIYp6Z6xJPQxiVuUt0yDHHHGMtWLAgcPzxx7teQWZAAiRAAiRAAiRAAiTgXQIrV65UTZs2tfbs2QO79G7R/8WrtPE2hFGvMaK96tatq+bNm6fEKI5XXZkPCZAACZAACZAACZCAhwiI8auaN2+uVqxYgVLBLxgT5OIm8Zgsl7ky18iJRagwHKJlCDzzdR6TAAmQAAmQAAmQAAmkOAHYgLAFM4zgRVJd2IhxlbS45vZvZv/I5kvRy2UovChmCLZv3z4BxWCWJEACJEACJEACJEACiSLwf//3f+r1119H9ttEz8zY4jhukgjXCFO5drIzRTRt/PjxgZ49e5rz3JIACZAACZAACZAACaQwgQ8//FBdcMEFcAs4IorJcTNE4y6JNIRR2VtEhxUrVsz67rvvAieddFLcATBDEiABEiABEiABEiCB+BH46aefVIsWLaz9+/fDDr1V9Pn45R6aU6INYZTmLdE+NWvWVBJJQpUpUya0hDwiARIgARIgARIgARJICQI7duxAhAi1du1a1Gek6FXYSZQkYrJc5rr2lRPzAaRHjx7q4MGDma/zmARIgARIgARIgARIIMkJwMaDrZdhBM+X6sAGTKh4wRA+JAR6iK6bNWuWuvjii9U//2A+HYUESIAESIAESIAESCAVCMC2g40HW09knShsP9iACRUvGMIAsFm0o+jWSZMmqWuuuYZh1UCFQgIkQAIkQAIkQAJJTgBh0mDbwcYT2SoKmw+2X8IlEeHTIlV6h1yYLtpryZIlhfbu3as6deoU6V6eJwESIAESIAESIAESSAICd955pxoxYgRKukcUESKW4cAL4iVDGDzw6+A70V5z587NX6hQIdW6dWucp5AACZAACZAACZAACSQZgSeeeEI9+uijKDXcILqKzsWBV8RrhjC4rBPFL4ULpk2blq9y5cqqSZMmckghARIgARIgARIgARJIFgKvvfaauu2221BcxAq+WBQLqnlKvGgIAxAWnP5dtPunn35qSXzhQL169XCeQgIkQAIkQAIkQAIk4HECWDCjd+/eWDADoXpvEB3jxSJ71RAGq4Wih0XPmjBhgtWyZctAjRo1cJ5CAiRAAiRAAiRAAiTgUQLTp09X559/vnXkyBEYwfeJJmzBjJwQoYBel2elgLcXL17c+vLLLwNiEHu9vCwfCZAACZAACZAACfiSwJw5c1Tnzp2tffv2wcZ8TvQOL4NIBkMYZXxD9KqiRYtaEnoj0L59ey8zZdlIgARIgARIgARIwHcEMBLcrVs368CBA7DdsHLwNaJwj/CseCWOcHaAABAgXwXYLl26WF988UV29/MaCZAACZAACZAACZBAHAnANoONlmEEvypZe94IBh4v+whnbr5P5UQZ8TdpMW7cOKtBgwaBunXrZr6HxyRAAiRAAiRAAiRAAnEkIHO5VM+ePa3Dhw9jJBj+wP3jmH2eskomQxgVRdiNokePHm01fvx464QTTghIRIk8AeDDJEACJEACJEACJEACuSPw3nvvqUsuucSSJZRhBA8RHZC7lBLzVLIZwqA0VTQgy/W1k9AcVnp6eqBhw4aJocdcSYAESIAESIAESMCnBEaNGqVDpMkAJYzgh0TvTzYUyWgIg/EMUaxQokOrVahQIXDqqafKIYUESIAESIAESIAESMBtAlgy+brrrjNxggdKfnr5OLfzdTr9ZDWEwWG26C7Rs/+/vTOBsqK61vC5dDO0gIBiECGAhEEUREUGBQJLECGI4nJ6OIHKE1HzDBqcsswL0ZgAGuRFBRSe4BADmigqIgouFAcQCeGBzEIzDxIGARkaqLf/outSXG7T3dDDHb691m+dOlW3hq9u238fdu0zadIkV7VqVdemTRv1ExCAAAQgAAEIQAACxUTg2Wefdb/85S91dI0Ea+q4Z7SSjJHMRli8Z5k2mrpPmTIlYuE6duxoqwQEIAABCEAAAhCAQFETGDRokHv0UQ0A+2XR+tvy+aI+R0keL9mNsFjNMa0y9Zg+fXqZ7Oxs1717d5eRkQq3ptsjIAABCEAAAhCAQOkSyMnJcXfccYcbPny4LuSg6Q6T5nlI6tCQdqpEV7uRCabKGhX+xz/+4apVq5Yq98Z9QAACEIAABCAAgVIhsG3bNk2Z7GzAUeffabrBpEpeSR+pZIT1MM43TTLVVo1h5Q7Xr19f/QQEIAABCEAAAhCAQCEJrFixwv+X9sWLF+uTa03dTf+nlVSIMqlwE6F70INpbZqrB6aX52bOnBnaTBMCEIAABCAAAQhAoCAE5KHkpXJN8Fz7jDxWyphgMUg1I6x7Wm/6uWnS999/r5fnvDfffFP9BAQgAAEIQAACEIBAAQjIO8lDyUtZ6F/b5a3ksVIqUvWNsv32lMabTrcpmVvZw/SysrIi7dq1S6mHx81AAAIQgAAEIACBoiYwePBg169fP888lFJoVRWit0nzN6RcpKoR1oNSkecPTD+YukydOjWyfv16161bN1emTCoOhNtdEhCAAAQgAAEIQOAECdg0yTLAbsgQzZTs+yhNl/zb3Lb6Ui5S7WW5vB5QT9vwuumUTp06uTfeeMOdccYZee1LPwQgAAEIQAACEEgrAkqB6NWrl5s2bZru+0fTzaZ3tJLKkS5GWM+wpWmiqWbt2rWdcl+YiU5YCAhAAAIQgAAE0pmAXoq7/vrr3dq1KgrhNpiuNs3WSqpHOuUI6IFeZPpMD7p9+/beX/7yl1R/vtwfBCAAAQhAAAIQyJOAvJA8Ua4J/sx2lFdKCxMsKKmcI6z7i41d1vGa6ZRDhw61nTx5sluyZInr2rWrK1euXOy+rEMAAhCAAAQgAIGUJLBr1y7Xu3dvN3ToUGeeSBkCT5tuM+ndqrSJdEqNiH2o11jHWNOpTZo0cX//+9+dlgQEIAABCEAAAhBIZQKLFi1y1157rdPSQsa3j+ltU9pFOqVGxD5cPfCLTfP1RWjZsqU3frwqrhEQgAAEIAABCEAgNQnI68jz5Jrg+XaX8kJpaYL1hNMtNUL3HI6ttjLOVCcnJ6f5W2+95TSfdufOnV1GRrqjCWOiDQEIQAACEIBAMhMwn+MeeOABN3DgQGdtZQS8alJVrU3JfF8ne+3pnBoRy+5u6xhuKnfJJZf4VSVq1aoVuw/rEIAABCAAAQhAIKkIrFu3zq8K8dVXX+m6NenY/aaRWkn3SOfUiNhnry+Epp5brS/K+eef7ylvmIAABCAAAQhAAALJSkBeRp4m1wSvtvuQ18EE5z5QjPDR3+ygxNqkrVu3Rq677jr/jcodO3YcvRdrEIAABCAAAQhAIIEJyLvcdtttTl5GnsYudZIprUqjFeTxkBqRN6V+tukZU8U6deq4cePGuY4dO+a9N1sgAAEIQAACEIBAAhCYPn26P5C3erUGgN1uk6ZKHqUV4mgCvBF2NI/w2hxbmWBqZX9V1TYj7FnNvUiHDh1cZmZmeD/aEIAABCAAAQhAoNQJ7Nu3zz3yyCOuX79+nnkXDXbONF1h+rjULy5BL4AR4fwfjP5YeMz0W1Nm06ZN3WuvveaaN2+e/yfZAwIQgAAEIAABCJQAgXnz5rlbbrnFLViwQGc7YPq96SnTQRORBwFGhPMAE+r2rP2ZabKpw+bNm6uPGTPGK1++fETVJSIR/pYIsaIJAQhAAAIQgEAJErBZ4fzZ4Xr16uVt3LhRpmSJqbvpbyZ5GOI4BHBxx4ETZ1OW9Q013WOK2Nzc7pVXXnH16tWzVQICEIAABCAAAQiUHIHs7Gz/hbgZM2bopDK9L5gGmvaYiAIQKFOAfdjlCAF9se4zdTOt1xevWbNm3ksvveQ8jz+6jmCiBQEIQAACEIBAcRGQ55D3kAfJNcHr7VxdTfIomOBCgGdEuBCwYnY9zdZVh+969Wt0eNSoUa5JkyZaJSAAAQhAAAIQgECRE9DUyPYynMs1wDr+myZNCqbZcolCEiBHuJDAQrvrLy59+Raa2lmJksovvviit3///sill15KZYkQKJoQgAAEIAABCJwcgb1797pBgwbphThv5cqVGsjcYLrTNMjEKLBBOJFgRPhEqB37mSrW9SeTag9HGjZs6EaMGOE6dep07J70QAACEIAABCAAgUIQmDZtmuvfv79btmyZPqVcTNUEfsTEjF8G4WSCHOGToXfks/oi9je1NS3QF7Vz585+MestW7Yc2YsWBCAAAQhAAAIQKCABeYjevXv7niLXBKs2mryGPAcmuIAcj7cbqRHHo1P4bWvtI6NNP5raWk2/siq1VqNGjcgFF1xQ+KPxCQhAAAIQgAAE0pLA2LFjXY8ePbyZM2fqX++V+qD5DPqYVpmIIiJAakQRgYxzmPrWN8LURds0PfPIkSNd48aNtUpAAAIQgAAEIACBYwgsWbLE3X333U7TJOfGR7bUCPCKoINl0RFgRLjoWMYeaZt1vGZSQk97q/VXUS/TWeHrSJs2bXiZLpYW6xCAAAQgAIE0JqCX4f7whz+4m266yfvuu+80ULnZdJfpYZM8BVEMBDDCxQA15pDzbX2M6fSDBw9eZH/hRTRFc82aNZ2mayYgAAEIQAACEEhvAuPHj3c9e/Z0EydOdOYVBEO+4WrTbK0QxUeA1IjiYxvvyO2t839MfsKwyqwNGzbMtWrVKt6+9EEAAhCAAAQgkMIEvv76azdgwAD35ZdfBnf5L2v8l2lG0MGyeAlQNaJ4+cYeXV/sFqa+po364rdu3dqzmoBuzZo1sfuyDgEIQAACEIBAChLQ73z97pcHyDXBG+025Q3kETDBJfjMM0rwXJzqMAHV/5trUg1ARav58+dnWt1hfzIOjQ6XK1fu8Bb+CwEIQAACEIBAyhDYvXu3e/LJJ12vXr28uXPn6l/l95mGmG4wzTLJIxAlSIDUiBKEncep6lj/YNN/aLtyh5966il32223uTJlGLAXEwICEIAABCCQzATsRXn3yiuvuMcee8xt2KAJ4fz4m/1XL8KtPrzKf0uDAEa4NKjHP+cl1j3M1FqbL7roIvfnP//ZdejQQasEBCAAAQhAAAJJSODTTz91DzzwgPvnP/8ZXL1GfgeYvgo6WJYeAYYcS4997Jn1AyEzfLNpjX5gVHv42muvdcuXL4/dl3UIQAACEIAABBKYgH5363e4fpfnmmC9DKTf8fpdjwlOkGfHiHCCPIiYy8iy9QdN+ieTShkZGV6fPn0ijz/+uKtbt27MrqxCAAIQgAAEIJAoBFatWuWeeOIJZzPDeVYKTT5rl0kpkM+Y9piIBCKAEU6ghxHnUmpa3+9NfUyZZcuW9fr27Rv5zW9+42rVqmVdBAQgAAEIQAACiUBg3bp1/oQYo0eP9nJycuSvDpjGmjQ1cjQx2NpEAhHACCfQwzjOpfzMtv23Sf+kUqZ8+fKeTb8YefTRR12NGjWO8zE2QQACEIAABCBQnAQ2bdrk/vjHP7qRI0d6+/btk686ZHrdNMj0nYlIYAIY4QR+OHEu7Rzr+51JZVYiWVlZ3n333Rd56KGHXPXq1a2LgAAEIAABCECgJAhs2bLFDRkyxD333HPenj175KdU+myC6XemxSYiCQhghJPgIcW5xGbWp780r9G2ihUrer/61a8iDz74oKtWrZq6CAhAAAIQgAAEioHAtm3b3DPPPOOeffZZz+oCBz7qbTuV/uV2fjGckkMWI4HgARbjKTh0MRK4yI6tHOLuOsepp57qmRmOmClWW10EBCAAAQhAAAJFQOCHH36Q+ZUJ9qwd+KdJdmjlAEdroxXBqThECRIIHmQJnpJTFQOBNnZMGeLLdWwbFfZ+/etfR+655x5XtWpVdREQgAAEIAABCJwAge3bt7sXXnjBPf30056NBge+6WM71OMm1QQmkphA8ECT+Ba49BCB9tZ+wtRBfUqZ6NevX2TAgAGudu3a6iIgAAEIQAACECgAgbVr17phw4a5UaNGhVMgPrWPygDPKMAh2CUJCGCEk+AhncAlXmafecTkjxBnZmZ6N998c2TgwIHuvPPOO4HD8REIQAACEIBAehD49ttv3dChQ93rr7/uHThwIPBJGgH+k+mT9KCQPncZPOD0ueP0utML7HYfMqnKRIbJu/LKK/0qE+3ba/CYgAAEIAABCEBABGbMmOFXgXj//fdV/UH+6KBJVSCGmP5lIlKQAEY4BR9qnFuqZ32aqe4O0ykm16ZNG/fwww+7q666ypUpU0ZdBAQgAAEIQCCtCBw6dMi9++67bvDgwW7mzJnBvf9ojf81aSa4bBORwgQwwin8cOPcmooN32e61+QXHm7cuLGzF+vcrbfe6myijjgfoQsCEIAABCCQWgRs4gv36quv6gU4t2TJkuDmtljjedNzJrWJNCCAEU6DhxznFjUqrNFhjRLXM7maNWu6+++/3911113UIhYQAgIQgAAEUo6AagC/+OKLbvjw4W7Dhuisx9l2oxr91SiwRoOJNCKAEU6jhx3nVpU3rPzhh0zKJ3YVKlTwbrrpJr/0WosWLdRFQAACEIAABJKawJw5c/wSaH/961+9vXv3Bt5Heb/K/51gUj4wkYYEgi9DGt46txxDoIutDzBdYfK/F61bt3b33nuvu+GGG0ibiIHFKgQgAAEIJDYBpT9MmDDBPf/8827WrGi5X70IN8U0zPRRYt8BV1cSBDDCJUE5uc7xM7vce0y3m/z5mqtXr+7uvPNO179/f1e3bt3kuhuuFgIQgAAE0opAdna2GzlypBszZozbsiWa6rvNILxsesH0XVoB4WaPSwAjfFw8ab0xy+6+l0kv1mkqZxeJRPzyaxol7tKli9bVTUAAAhCAAARKlYDnee6jjz7yR39V/swi+AWlqY/1Atwbpj2lepGcPCEJBF+UhLw4LiphCGgKZ40SK5+4vK6qQYMG/gjx7bffzst1AkJAAAIQgECJE9DLby+//LIbMWKEW758eXD+fdZQ3q9Gf6M10YKNLCEQJoARDtOgnR8BlVzra7rb5OdI6OU6zVrXt29fvzZxfgdgOwQgAAEIQOBkCajm7+jRo/3Z30Ivv62y4440jTZFcyJO9lx8PrUJYIRT+/kW191pBo7uJqVN6CU7/3ukmsR9+vTxaxLXqlXLugkIQAACEIBA0RBYt26dX/t37Nix4dq/evlNL70p/WGS6ZCJgECBCWCEC4yKHfMg0MD6/9N0q6mm9lEuseUQR2SKe/bsqZJs6iYgAAEIQAAChSJgo73unXfecTK/lgMczv3dYAd61fSSKZoTUaiDszMEjABGmK9BURHIsANpdLiP6WqTn0tctWpVd+ONN/ojxZrWmYAABCAAAQjkR0CpDzK/48ePd9u3bw92V+7vRNNYk0aBqf1rEIiTI4ARPjl+fDo+AZVdU8WJPqaWJj/OOecc17t3b1InAiAsIQABCEAgSiBIfRg3bpxbvHhxtN8as01jTar8oDJoBASKjABGuMhQcqA8CJxr/X1Mt5hInTAIBAQgAAEIHCaQT+rDa7bXWNPCw3vzXwgUPQGMcNEz5YjxCSh14gpTH9NVJj91olKlSt7VV18d0ex1V1xxBTPYGRgCAhCAQCoT0IxvU6ZM8Wd9mzhxordr167Aiyj14V3TWNMUE6kPBoEoXgLBl694z8LRIXA0gSB1ord1two2Va5c2bOX63xTrAk7ypUrF2xiCQEIQAACSUxg//79/oQXmvLYXn7zdu7cGfYfX9utjTOR+pDEzzhZLz38RUzWe+C6k5vA2Xb5mqhD8mew0+3oJTtVnNBIcefOnV3ZsmXVTUAAAhCAQJIQyMnJcVOnTvVHflX5IfTSm+5AM75p0gtppYmAQKkQwAiXCnZOmgeBn1n/jSaZ4ubBPtWqVXPXXHONb4o7derkMjMzg00sIQABCEAggQgcOHDATZs2zTe/b7/9ttPMb6GYZ20Z3/Gm70L9NCFQagQwwqWGnhPnQ6CRbQ9GipsF+55++um+KVZJto4dO2KKAzAsIQABCJQSAZnf6dOn+6XOZH7//e9/h69kvq0EI79LwxtoQyARCGCEE+EpcA35ETjHdghM8XnBzlWqVPF+8YtfRHr06OG6du3qNHJMQAACEIBA8RPQSO+HH37o3nvvPffBBx94O3bsCPuJb+0KAvN7VB204r8yzgCBwhEIf3EL90n2hkDpEDjXTqv0ietMavuRkZHhtW/f3jfFV155pWvUSAPKBAQgAAEIFBWBpUuXuvfff983vzNmzPAOHjwY9hAL7TxvmZT2oDYBgaQgEP4SJ8UFc5EQCBGob+0eufq5LaNv1MkIa6RYatu2LSkUIWg0IQABCBSEgFIevvjiC9/4auRXRjgUOdb+zPRerlaEttGEQNIQwAgnzaPiQvMhcKpt72qSMe5mOt3kh1ImlDohU9ytWze/IkWwjSUEIAABCBwhoMoOkydP9s2vUh9iXnZT8u9kk8zvh6YfTAQEkpoARjipHx8XnwcBTd5xiSkYLW4S7BekUMgQqyzbhRde6CIRfgwCPiwhAIH0IuB5nps7d65f5kwGOE7KwyIjEoz6fmVtJrlIr69Iyt8tDiDlHzE3aARUli0wxe2tHU2hUBWKyy67zF1++eW+MT777LMBBgEIQCClCaxcudI3vh9//LH75JNPYqs8KOVhhikwv5Q5S+lvAzeHEeY7kG4EqtgNd8lVZ1vWM0Wjfv36viHWaLEMsowyAQEIQCCZCaicmQyvJreQVqw4Jp032+5vqumjXO2wJQGBtCCAEU6Lx8xNHoeARotliKXLTKeZ/LCUCc9SJyIyxRoxbteunatQoUKwmSUEIACBhCSwd+9e9/nnnzuN+Mr4WuqDZUB44d/3W+3CPzHJ/EqM+hoEIj0JhH8w0pMAdw2BIwTKWFPTPAfGuK21o863fPnynpnhiGa3s1JtrmXLls76jnyaFgQgAIFSILBv3z43e/Zs5ff6s7qZCfasL/z7fa9d1hemwPhqeuNDpXCpnBICCUcg/IOScBfHBUGglAnIBLczBcb4QmvLLPtRrlw5z8xwRCPF0qWXXupOOy06oBzsxhICXIiqmQAABoNJREFUEIBAkRLYunWr+/LLL/1RX438mgn29u/fH/59LpM71xQY38+tLTNMQAACMQTCPzgxm1iFAARiCChhWOkTHUwyyM1MUWNsbe/cc8+NGmOZY16+MyoEBCBwUgT0cpsMb6CFCxd6dsDw728Z3/kmGd5PTUp7UKkzAgIQyIdA+Acpn13ZDAEIxBDQi3cq0yZTLLUyZZmicdZZZ/kTegSjxs2bN3dWwi26nQYEIACBMAGbrc3Nmzcvano1ocX69evDu6i9x/S1ScZXUlkzXnAzCAQECksAI1xYYuwPgbwJqCybcowDY6wc4zPCu1esWNFr3bp1RPnFF198sa969eqFd6ENAQikEYHs7Gz3zTff+FKe76xZs7zdu3fH/m7+3pAoxzcwvsrxVZkzAgIQOEkCsT9sJ3k4Pg4BCMQQaGzrgTHWskHMdr9EW2CKW7Ro4Zvjn/70p7G7sQ4BCCQ5gTVr1viGd86cOVHzq9JmcWK59QWmV8slcfahCwIQKAICGOEigMghIFAIAjVs35ami0NS31Hxk5/8JDpiHJjkmjVrHrUPKxCAQOIS2LBhQ9TsBiO+mzdvjnfBm6zzm5BmW1t9BAQgUAIEMMIlAJlTQCAfArVte9gYq33MTB7KN5Yp1rTQzZo1c02bNnUNGjQg5zgfuGyGQHESUE7v8uXL3YIFC9z8+fP96YplfOPk9eoyNPwbNr1qr9UGAgIQKB0CGOHS4c5ZIZAfgXq2Q9gct7D1qrEf0gQfTZo08U1xYI61rF1b3pqAAASKksDatWt9sxuYXi0XLVrkNIFFnNhufXNMYeObHWc/uiAAgVIkgBEuRficGgKFIKCfVc2CJ3Pc3NTU1MxUx3TMz3HVqlV9c6xRYykwydQ5NloEBPIhoDq9YbOrtrR9u7ztMaFSZqtNKl+2wDTPJPOr2dq0jYAABBKYwDG/QBP4Wrk0CEDgWAKVres8k0xxYI61PKpaha37ofQKq3XsGjVq5Kthw4ZOUuWKsmVV9IKAQHoQyMnJcarYsGzZMl9Lly51ktXozSutQWBUvUFmNzC9Wn5r2mkiIACBJCSAEU7Ch8YlQ6AABPQCXtgYyyifa6oU77OZmZm+GQ6MsZYyy1rWqVOHPOR40OhLeALK3129enXU6AamV0uZ4AMHDuR1D7tsw0JT2PDKAPMSW17E6IdAkhLACCfpg+OyIXACBPTzXs/UxNQwRnVtPTxLnq0eDptK2tWvX983xYFRrlu3rm+QZZIrV9agNAGB0iGwc+dO3+zK8K5atSo6wiuzu2LFCmdTD+d1YZqNbZVpWYwW2Xq2ibQGg0BAINUJYIRT/QlzfxAoGIFytptykMMGuVHuei1b5vn/imrVqkVNsYxxWDLMKvtWpkxcj22HJSCQN4FDhw45lSGTwZXRjadt27blfYDDZnad7SCzuzR3GRhf5fDm6ZJtGwEBCKQBgTx/uaXBvXOLEIBAwQhk2W6aCEQmWeZYhlkjyHpRTzN/nGLKM5R2oSoWYYNcq1Ytd+aZZ7oaNWr4UrtSpbhZG3kelw3JTWDXrl1u48aNbtOmTb7UXrdu3VFmV1UajpO+EAD40RprTHphTSO8MriB6dXEFHtMBAQgAIG4BDDCcbHQCQEIFIJAddtXplgKDHKwrqXylfP9f80pp5xylDEOTLKWYdOsddIxjGgChtIUAmOrZdjoxq7/+KP8a76h9ATl5crkhiXDG6xvsTYBAQhA4IQI5PvL6YSOyocgAAEIHCFQ3poqbBw2ymfZugyydGbu8rgjy7ZPNLKysvypqVUmTqkZhVlioqMY4zZkZlUmTCkHhVlqquA9ewo1+ConLJO7MXep9npTMLKrpSab2GciIAABCBQLAYxwsWDloBCAwAkQUG5E2BjHGuXweoFNc+x1KFWjSpUqvnnWKHRektnOa5v6tV0Tmuh4GRkZ0aXahVnX9am6gVIAtAxU0HXtpwkdZEI1ypqX8tsu07tjx46CpCLEIg2vy9yGjW2s0Q2vqzIDAQEIQKBUCWCESxU/J4cABE6QQEX73GmmaibNuFeYpT5L5E1gt23SG2iaPaIwy622vz5LQAACEEgaAhjhpHlUXCgEIFBEBDLtODLOp5pkijW6LGWF2kFfeBlvewX7TEaudNygrWVB121Xd9CkorZaBirouvZT+oBGY8NSnkJ4PbYd3i4D+4NJxlfHIyAAAQhAAAIQgAAEIAABCEAAAhBIVQL/D+sDHtLCNsVZAAAAAElFTkSuQmCC" } }, "cell_type": "markdown", "metadata": {}, "source": [ "### Strings\n", "\n", "A *string* over $\\Sigma$ is a finite sequence of symbols from $\\Sigma$. For example, if $\\Sigma = \\{ \\texttt{a}, \\texttt{b} \\}$, some strings over $\\Sigma$ are $\\texttt{a}$ and $\\texttt{bab}$. The set of all strings over $\\Sigma$ is written $\\Sigma^\\ast$ (sigma star). We usually use $w$ for a variable that stands for a string and $u,v$ or $x,y,z$ when we need more variables. \n", "\n", "We don't distinguish between symbols and length-1 strings. (This is unlike C, which distinguishes between `'a'` and `\"a\"`, but like Python, where they are the same thing.)\n", "\n", "Please pay careful attention to this: We write the *empty string* (that is, the string of length 0) as $\\varepsilon$ (epsilon). Although $\\varepsilon$ may look like a symbol, it is not.\n", "\n", "Maybe this Venn diagram will help, assuming $\\Sigma = \\{\\texttt{a}, \\texttt{b}\\}$:\n", "![image.png](attachment:image.png)\n", "\n", "**Question.** (This question and all questions below are not for credit; they will be discussed in class.) True or false:\n", "- $\\Sigma \\subseteq \\Sigma^\\ast$\n", "- $\\varepsilon \\in \\Sigma$\n", "- $\\varepsilon \\in \\Sigma^\\ast$\n", "- $\\texttt{a} = \\texttt{aa}$\n", "- $\\texttt{ab} = \\texttt{ba}$\n", "\n", "If $w$ is a string, we write $w_i$ for the $i$-th symbol of $w$ and $|w|$ for the length of $w$. If we ever have to number some strings, we'll write them as $w^{(1)}, w^{(2)},$ etc. The parentheses are there to make it clear that the numbers aren't exponents.\n", "\n", "If $x$ and $y$ are strings, we write $xy$ (or occasionally $x \\circ y$) for the *concatenation* of $u$ and $v$. Also, we write $w^2 = ww$, $w^3 = www$, etc. Concatenation is associative: $(xy)z = x(yz) = xyz$. And concatenating the empty string does nothing: $w \\varepsilon = \\varepsilon w = w$.\n", "\n", "We say that $x$ is a *prefix* of $w$ if there is a string $y$ such that $w = xy$, and we say that $y$ is a *suffix* of $w$ if there is a string $x$ such that $w = xy$. We say that $y$ is a *substring* of $w$ if there are strings $x, z$ such that $w = xyz$.\n", "\n", "**Question.**\n", "- List all the prefixes of $\\texttt{abc}$.\n", "- What is $|\\varepsilon\\varepsilon\\varepsilon|$?\n", "- Give an example of when $xz$ isn't a substring of $xyz$. Give an example of when it is." ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "### Languages\n", "\n", "Above, we said that we treat every computational problem as a yes/no question about strings. Another way of saying this is that we treat every computational problem as a set of strings, which we call a *language*. For example, the problem of testing whether a number is prime could be treated as the language $$\\{w \\in \\{\\texttt{0}, \\ldots, \\texttt{9}\\}^\\ast \\mid \\text{the number with decimal representation $w$ is prime}\\}.$$\n", "\n", "We've already met one language, $\\Sigma^\\ast$. We write $\\emptyset$ (empty set) for the empty language.\n", "\n", "**Question.** True or false?\n", "\\begin{align}\n", "\\varepsilon &\\in \\{\\mathtt{abc}\\} \\\\\n", "\\varepsilon &\\in \\Sigma^\\ast \\\\\n", "\\{\\texttt{abc}\\} \\cup \\emptyset &= \\{\\texttt{abc}\\} \\\\\n", "\\{\\texttt{abc}\\} \\cup \\{\\varepsilon\\} &= \\{\\texttt{abc}\\}\n", "\\end{align}\n", "\n", "**Question.** Is there such a thing (according to the definitions above) as \n", "- an infinite alphabet?\n", "- an infinite string?\n", "- an infinite language?\n", "\n", "Operations on strings often induce analogous operations on languages. For example, if $w$ is a string, define $w^R$ to be the *reversal* of $w$, that is, the string with the same symbols as $w$ but in reverse order. Then there is a natural definition for the reversal of a language:\n", "\\begin{equation}\n", "L^R = \\{ w^R \\mid w \\in L \\}.\n", "\\end{equation}\n", "\n", "If $A$ and $B$ are languages,\n", "\\begin{align}\n", "A \\circ B = AB &= \\{ xy \\mid x \\in A, y \\in B\\}.\n", "\\end{align}\n", "\n", "For example, if $A = \\{\\texttt{c}, \\texttt{d}\\}$ and $B = \\{\\texttt{at}, \\texttt{og}\\}$, then $A \\circ B = \\{\\texttt{cat}, \\texttt{cog}, \\texttt{dat}, \\texttt{dog}\\}$.\n", "\n", "**Question.** According to the above definition, what is\n", "- $\\emptyset \\circ \\{\\texttt{a}\\}$\n", "- $\\{\\varepsilon\\} \\circ \\{\\texttt{a}\\}$\n", "\n", "The $\\ast$ operator that we saw above, known as the Kleene star, can be applied to any language. If $L$ is a language, then $L^\\ast$ is the set of strings made out of zero or more strings in $L$. More formally:\n", "\\begin{equation}\n", "L^\\ast = \\{ w^{(1)} \\cdots w^{(k)} \\mid k \\geq 0, w^{(i)} \\in L \\}.\n", "\\end{equation}\n", "\n", "For example, if $L = \\{\\texttt{aa}, \\texttt{bb}\\}$, then $L^\\ast = \\{\\varepsilon, \\texttt{aa}, \\texttt{bb}, \\texttt{aaaa}, \\texttt{aabb}, \\texttt{bbaa}, \\texttt{bbbb}, \\texttt{aaaaaa}, \\ldots\\}$.\n", "\n", "**Question.** According to the above definition, what is \n", "- $\\emptyset^\\ast$?\n", "- $\\{\\varepsilon\\}^\\ast$?" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "# Thursday" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "## Proofs\n", "\n", "Most of the work that you will do in this class involves writing proofs. Because students in this class probably have a wide range of backgrounds in proof-writing, I'd like to say a little about it here.\n", "\n", "

Read Sections 0.3–0.4, unless you feel very comfortable with writing proofs.

\n", "

Read W1E4: Writing Proofs I

\n", "
" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "My mantra is that writing proofs is actually a lot like writing programs (in fact, there is a [deep connection between the two](https://en.wikipedia.org/wiki/Curry–Howard_correspondence)). Much of my advice below applies equally well to programming, and I firmly believe that if you work to make your proofs better, you'll also become a better programmer.\n", "\n", "### Before you write\n", "\n", "Many students feel that when they are asked to write a proof, they feel that they don't know how to begin. As a running example, imagine that you need to prove: $L^\\ast = \\{\\varepsilon\\} \\cup L \\circ L^\\ast$ for any language $L$.\n", "\n", "1. **Understand the requirements.** What are the givens: the premise or \"if\" part of the statement to be proven, the definitions of all terms in the statement, and any facts that you're allowed to use? What is the conclusion or \"then\" part of the statement to be proven? You may want to rewrite the statement in a more explicit way. For example, you might rewrite the above statement as: If $L$ is a language over an alphabet $\\Sigma$, then $L^\\ast = \\{\\varepsilon\\} \\cup (L \\circ L^\\ast)$. You might also review the definitions of union ($\\cup$), concatenation ($\\circ$), and Kleene star ($\\ast$).\n", "\n", "2. **Develop an intuition.** Sometimes it's obvious, but more often, it is not obvious, or it may even feel obviously false! One way to convince yourself is to try examples. If, for example, the statement says \"for all strings,\" try a few strings and see whether the thing to be proved is true for them. Choosing good examples (like choosing good test cases) means trying to find examples that falsify the thing to be proved. Seeing how such examples fail is a great way to develop an intuition for why the thing must be true.\n", "\n", "3. **Divide and conquer.** Once you understand what you are given and what you must prove, and have some intuition for why one implies the other, you need to solidify this intuition into a rigorous proof. See if you can break it down into smaller, easier-to-prove pieces. It's okay, and often easier, to work backwards from the conclusion. In our example, we most likely want to break it down into $L^\\ast \\subseteq \\{\\varepsilon\\} \\cup L \\circ L^\\ast$ and $L^\\ast \\supseteq \\{\\varepsilon\\} \\cup L \\circ L^\\ast$." ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "### Paragraph proofs\n", "\n", "If your high-school geometry class was like mine, you were taught to write \"two-column\" or \"statement-reason\" proofs. These consist of a sequence of logical statements, each accompanied by a reason. Each statement should be a consequence of zero or more *previous* statements or givens.\n", "\n", "These are the \"best\" kind of proof because their logical structure is completely explicit. But a proof written this way could be hundreds of pages! You don't want to write that, and your TAs don't want to read that. Instead, most proofs are \"paragraph proofs,\" that is, they are written in English and convince the reader that they *could* write a \"statement-reason\" proof if they really wanted to.\n", "\n", "Here's an example proof for our example above (that $L^\\ast = \\{\\varepsilon\\} \\cup L L^\\ast$): \n", "\n", "> To show that $L^\\ast = \\{\\varepsilon\\} \\cup L L^\\ast$, we need to show that $L^\\ast \\subseteq \\{\\varepsilon\\} \\cup L L^\\ast$ and $L^\\ast \\supseteq \\{\\varepsilon\\} \\cup L L^\\ast$.\n", ">\n", "> ($\\subseteq$) If $w \\in L^\\ast$, it can be written as $w^{(1)} \\cdots w^{(k)}$, where $w^{(i)} \\in L$, for some $k \\geq 0$. If $k=0$, then $w = \\varepsilon$. Otherwise, we have $w^{(1)} \\in L$ and $w^{(2)} \\cdots w^{(k)} \\in L^\\ast$, so $w \\in L L^\\ast$. Either way, we have $w \\in \\{\\varepsilon\\} \\cup L L^\\ast$.\n", ">\n", "> ($\\supseteq$) If $w \\in \\{\\varepsilon\\} \\cup L L^\\ast$, then either $w = \\varepsilon$ or $w \\in L L^\\ast$. If $w = \\varepsilon$, then $w \\in L^\\ast$. If $w \\in L L^\\ast$, it can be written as $u v$ where $u \\in L$ and $v \\in L^\\ast$. And $v$, in turn, can be written as $v^{(1)} \\cdots v^{(k)}$ where $v^{(i)} \\in L$. So $w$ can be written as $u v^{(1)} \\cdots v^{(k)}$ where $u, v^{(i)} \\in L$, so $w \\in L^\\ast$.\n", "\n", "**Exercise** (this exercise and the ones below are not for credit). Suppose you are told, \"Prove that if $y$ is a substring of $w$, then $y^R$ is a substring of $w^R$. You may use the fact that, for any string $u, v$, $(uv)^R = v^R u^R$.\" Below is a statement-reason proof of this fact; rewrite it as a paragraph proof.\n", "\n", "| Statement | Reason |\n", "|:---------------------------------|:--------------------------|\n", "| 1. $y$ is a substring of $w$ | Given |\n", "| 2. $w = xyz$ for some $x, z$ | Def. of substring |\n", "| 3. $w^R = (xyz)^R$ | Reflexivity, substitution |\n", "| 4. $w^R = (yz)^R x^R$ | Fact given above |\n", "| 5. $w^R = z^R y^R x^R$ | Fact given above |\n", "| 6. $y^R$ is a substring of $w^R$ | Def. of substring |\n", "\n", "Paragraph proofs fundamentally have the same structure as statement-reason proofs, but are meant to be more natural to read and write. The next few sections explain the similarities and differences more." ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "
\n", " Watch W1E5: Writing Proofs II\n", "
\n", "\n", "### Order\n", "\n", "A paragraph proof, like a statement-reason proof, should start from the givens and reason to the conclusion. It shouldn't start with the conclusion and reason backwards to the givens; still less should it assume the conclusion and reason in a circle back to the conclusion.\n", "\n", "However, just as it's good programming practice to preface a function with a comment that says what the function will do, it's also good proof-writing to sometimes preface a piece of your proof with a \"comment\" stating what it will prove. Be sure to clearly distinguish these \"comments\" with verbiage like \"we need to show...\" so that your reader doesn't think you've skipped a bunch of steps.\n", "\n", "In our example proof above, we start with two such \"comments,\" introduced by \"to show that...\" and \"we need to show...\". I was lazy and didn't bother to restate them at the end of the proof.\n", "\n", "**Exercise**. Look at the proof of Theorem 0.20 and number the statements in logical order. If two statements are equivalent, give them the same number. " ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "### Generality\n", "\n", "If you have to prove a statement \"There exists X such that Y,\" then it's fine to come up with an example X and prove that it makes Y true; similarly, if you have to *disprove* a statement \"For all X, Y,\" then it's fine to come up with a counterexample X and prove that it makes Y false.\n", "\n", "But if you have to prove \"For all X, Y,\" although it may be very helpful to think about examples for X (as we encouraged you to do above), examples don't constitute proofs. An example might sometimes be helpful to make a general statement more clear, but I'd encourage you to try to make the general statement clear on its own." ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "### Detail\n", "\n", "A statement-reason proof leaves no gaps in reasoning, but a paragraph proof leaves out details for the sake of brevity and clarity. How much detail? Just as pseudocode should have enough detail that someone else could implement it, a paragraph proof should have enough detail that someone (one of your classmates) can be convinced that a statement-reason proof could be written. But this rule is admittedly difficult to put in to practice. Here are a few examples.\n", "\n", "There are places in the example proof above where more detail could be given, but isn't expected. For example, it uses the fact that if $w \\in A \\cup B$, then $w \\in A$ or $w \\in B$. In principle, you might need to prove this, but we don't expect it because set theory isn't the focus of this class.\n", "\n", "Another missing detail is in the statement \"If $w = \\varepsilon$, then $w \\in L^\\ast$.\" In my opinion, this is fine, but since this is a fact about formal languages, which *is* the focus of this class, it would also be okay to add more justification: \"If $w = \\varepsilon$, then $w \\in L^\\ast$, because $\\varepsilon$ is of the form $w^{(1)} \\cdots w^{(k)}$ where $k=0$.\"\n", "\n", "On the other hand, if the other case just said, \"If $w \\in LL^\\ast$, then obviously $w \\in L^\\ast$,\" that would be too big of a jump for the first homework, where our focus is on strings and languages and writing good proofs. (It would be fine in later homeworks, after our focus has moved on to other topics.)\n", "\n", "If you're in doubt about how much detail to include, ask a TA or me, and if you ever lose points for omitting a detail that you thought was obvious, feel free to ask me to reconsider it." ] } ], "metadata": { "kernelspec": { "display_name": "Python 3", "language": "python", "name": "python3" }, "language_info": { "codemirror_mode": { "name": "ipython", "version": 3 }, "file_extension": ".py", "mimetype": "text/x-python", "name": "python", "nbconvert_exporter": "python", "pygments_lexer": "ipython3", "version": "3.8.1" } }, "nbformat": 4, "nbformat_minor": 4 }