{ "cells": [ { "cell_type": "markdown", "metadata": {}, "source": [ "# Week 4: Non-regular languages" ] }, { "cell_type": "code", "execution_count": 1, "metadata": {}, "outputs": [], "source": [ "from tock import *\n", "from tock.syntax import String\n", "import itertools" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "# Tuesday\n", "\n", "

Read Section 1.4, focusing on pages 77-79.

Watch W4E1: Prelude to the Pumping Lemma.

\n", "\n", "## Non-regular languages\n", "\n", "We've seen that three computational models (DFA, NFA, regular expression) turn out to recognize the same class of languages, the regular languages. Are there languages that aren't regular? Definitely -- the two classic examples are\n", "\n", "$$ B = \\{\\mathtt{0}^n \\mathtt{1}^n \\mid n \\geq 0\\} $$\n", "$$ G = \\{w w^R \\mid w \\in \\{\\mathtt{0}, \\mathtt{1}\\}^\\ast \\} $$\n", "\n", "The intuitive reason why is: If I give you two strings $u, v$, what information would you need about $u$ to decide whether $uv$ is in the language? Let's say that $L$ is the language of natural base-10 numbers that are divisible by 3. Recall that a number is divisible by 3 iff its digits sum to a multiple of 3. So the only information that you need about $u$ is the sum of its digits, _modulo 3_. That's a finite amount of information, so the language is regular.\n", "\n", "Now consider $B$. If I give you $u=\\mathtt{000001}$, the only $v$ that matches up with it is $v=\\mathtt{1111}$. The information that you need about $u$ is how many $\\mathtt{0}$'s it contains -- which can be unbounded. So, intuitively, this is not a regular language.\n", "\n", "## The pumping lemma\n", "\n", "But how do we really prove that $B$ is not regular? To do this, we entertain the possibility that it *is* regular. If there were a DFA $M$ that recognizes $B$, we try to \"break\" it by finding a string that is *not* in $B$ but *is* accepted by $M$. If we show that we can break *all* possible DFAs in this way, then that means we've shown that there is *no* DFA that recognizes $B$. So $B$ is not regular.\n", "\n", "The way that we are going to find the string that breaks $M$ involves a back-and-forth that is best thought of as a dialogue. Below, we imagine a dialogue between two people named Alice and Bill. Bill proposes $M$. Alice gives Bill a \"test\" string $s$ that $M$ is supposed to accept. But then, she uses the information that Bill reveals to concoct another string, and this is the one that breaks $M$.\n", "\n", "## A dialogue\n", "\n", "Alice. The language $B = \\{\\texttt{0}^n \\texttt{1}^n \\mid n \\geq 0\\}$ is not regular.\n", "\n", "Bill. Yes it is!\n", "\n", "Alice. Oh really, then show me a DFA that generates it.\n", "\n", "Bill. Here's one:" ] }, { "cell_type": "code", "execution_count": 2, "metadata": {}, "outputs": [ { "data": { "image/svg+xml": [ "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "q1\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "0\n", "\n", "\n", "\n", "\n", "\n", "\n", "q2\n", "\n", "\n", "\n", "\n", "\n", "\n", "1\n", "\n", "\n", "\n", "\n", "\n", "\n", "1\n", "\n", "\n", "" ], "text/plain": [ "" ] }, "metadata": {}, "output_type": "display_data" } ], "source": [ "m = read_csv(\"pumping1.csv\")\n", "m" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "Alice. How many states does it have?\n", "\n", "Bill. Let me see..." ] }, { "cell_type": "code", "execution_count": 3, "metadata": {}, "outputs": [ { "data": { "text/plain": [ "2" ] }, "execution_count": 3, "metadata": {}, "output_type": "execute_result" } ], "source": [ "p = len(m.states)\n", "p" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "Alice. Does your automaton accept the string $s = \\texttt{0}^p \\texttt{1}^p$?" ] }, { "cell_type": "code", "execution_count": 4, "metadata": {}, "outputs": [ { "data": { "text/html": [ "0 0 1 1" ], "text/plain": [ "String(values=('0', '0', '1', '1'))" ] }, "execution_count": 4, "metadata": {}, "output_type": "execute_result" } ], "source": [ "s = String(['0']*p + ['1']*p)\n", "s" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "Bill. Let me see..." ] }, { "cell_type": "code", "execution_count": 5, "metadata": {}, "outputs": [ { "data": { "image/svg+xml": [ "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "q1\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "q1\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "q1\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "q2\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "q2\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "1\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "1\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "0\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "0\n", "\n", "\n", "" ], "text/plain": [ "" ] }, "metadata": {}, "output_type": "display_data" }, { "name": "stdout", "output_type": "stream", "text": [ "Yes.\n" ] } ], "source": [ "graph = run(m, s)\n", "display(graph)\n", "path = graph.only_path()\n", "if path.accept:\n", " print('Yes.')\n", "else:\n", " print('No, I lose.')" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "Alice. Does this run use a state twice while reading in the first half of the string?\n", "\n", "Bill. Let me see..." ] }, { "cell_type": "code", "execution_count": 6, "metadata": {}, "outputs": [ { "name": "stdout", "output_type": "stream", "text": [ "Yes, the state is q1.\n" ] } ], "source": [ "if path.accept:\n", " for i, j in itertools.combinations(range(p+1), 2):\n", " if path[i][0] == path[j][0]:\n", " print(f'Yes, the state is {path[i][0]}.')\n", " break\n", " else:\n", " print(f'No.')\n", "else:\n", " print(\"I've lost already.\")" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "Alice. What are the strings that it reads up to the first visit, between the first and second visits, and after the second visit?" ] }, { "cell_type": "code", "execution_count": 7, "metadata": {}, "outputs": [ { "name": "stdout", "output_type": "stream", "text": [ "ε, 0, and 0 1 1\n" ] } ], "source": [ "if path.accept:\n", " x = String(s[:i])\n", " y = String(s[i:j])\n", " z = String(s[j:])\n", " print(f'{x}, {y}, and {z}')\n", "else:\n", " print(\"I've lost already.\")\n", " x = y = z = []" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "Alice. So, does your automaton accept this string?" ] }, { "cell_type": "code", "execution_count": 8, "metadata": {}, "outputs": [ { "data": { "text/html": [ "0 0 0 1 1" ], "text/plain": [ "String(values=('0', '0', '0', '1', '1'))" ] }, "execution_count": 8, "metadata": {}, "output_type": "execute_result" } ], "source": [ "s2 = x + 2 * y + z\n", "s2" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "Bill. Let me see..." ] }, { "cell_type": "code", "execution_count": 9, "metadata": {}, "outputs": [ { "name": "stdout", "output_type": "stream", "text": [ "Yes, I lose.\n" ] } ], "source": [ "if path.accept:\n", " p2 = run(m, s2).only_path()\n", " if p2.accept:\n", " print('Yes, I lose.')\n", " else:\n", " print('No.')\n", "else:\n", " print(\"I've lost already.\")" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "Try loading some other automata (`pumping2.csv`, `pumping3.csv`) to see how Bill always fails." ] }, { "attachments": { "image.png": { "image/png": "iVBORw0KGgoAAAANSUhEUgAAA1oAAAFoCAYAAABOj4oRAAAAAXNSR0IArs4c6QAAAJBlWElmTU0AKgAAAAgABgEGAAMAAAABAAIAAAESAAMAAAABAAEAAAEaAAUAAAABAAAAVgEbAAUAAAABAAAAXgEoAAMAAAABAAIAAIdpAAQAAAABAAAAZgAAAAAAAACQAAAAAQAAAJAAAAABAAOgAQADAAAAAQABAACgAgAEAAAAAQAAA1qgAwAEAAAAAQAAAWgAAAAA6R8yJwAAAAlwSFlzAAAWJQAAFiUBSVIk8AAAAgtpVFh0WE1MOmNvbS5hZG9iZS54bXAAAAAAADx4OnhtcG1ldGEgeG1sbnM6eD0iYWRvYmU6bnM6bWV0YS8iIHg6eG1wdGs9IlhNUCBDb3JlIDUuNC4wIj4KICAgPHJkZjpSREYgeG1sbnM6cmRmPSJodHRwOi8vd3d3LnczLm9yZy8xOTk5LzAyLzIyLXJkZi1zeW50YXgtbnMjIj4KICAgICAgPHJkZjpEZXNjcmlwdGlvbiByZGY6YWJvdXQ9IiIKICAgICAgICAgICAgeG1sbnM6dGlmZj0iaHR0cDovL25zLmFkb2JlLmNvbS90aWZmLzEuMC8iPgogICAgICAgICA8dGlmZjpPcmllbnRhdGlvbj4xPC90aWZmOk9yaWVudGF0aW9uPgogICAgICAgICA8dGlmZjpQaG90b21ldHJpY0ludGVycHJldGF0aW9uPjI8L3RpZmY6UGhvdG9tZXRyaWNJbnRlcnByZXRhdGlvbj4KICAgICAgICAgPHRpZmY6UmVzb2x1dGlvblVuaXQ+MjwvdGlmZjpSZXNvbHV0aW9uVW5pdD4KICAgICAgICAgPHRpZmY6Q29tcHJlc3Npb24+NTwvdGlmZjpDb21wcmVzc2lvbj4KICAgICAgPC9yZGY6RGVzY3JpcHRpb24+CiAgIDwvcmRmOlJERj4KPC94OnhtcG1ldGE+Cs+OiooAAEAASURBVHgB7Z0HvB1F2f9PGklIQkIoIYEUIKFI7yAlqFSpgoCBVxQpAqIvRUAREAu8gKAgYkE6/OmoVAkgoUUgdOmhBULoENJDyt3/77fePew95d5z7j1l95zv8/k8d/fMzs4+853duTs7M89kMggEIAABCEAAAhCAAAQgAAEIQAACEIAABCAAAQhAAAIQgAAEIAABCEAAAhCAAAQgAAEIQAACEIAABCAAAQhAAAIQgAAEIAABCEAAAhCAAAQgAAEIQAACEIAABCAAAQhAAAIQgAAEIAABCEAAAhCAAAQgAAEIQAACEIAABCAAAQhAAAIQgAAEIAABCEAAAhCAAAQgAAEIQAACEIAABCAAAQhAAAIQgAAEIAABCEAAAhCAAAQgAAEIQAACEIAABCAAAQhAAAIQgAAEIAABCEAAAhCAAAQgAAEIQAACEIAABCAAAQhAAAIQgAAEIAABCEAAAhCAAAQgAAEIQAACEIAABCAAAQhAAAIQgAAEIAABCEAAAhCAAAQgAAEIQAACEIAABCAAAQhAAAIQgAAEIAABCEAAAhCAAAQgAAEIQAACEIAABCAAAQhAAAIQgAAEIAABCEAAAhCAAAQgAAEIQAACEIAABCAAAQhAAAIQgAAEIAABCEAAAhCAAAQgAAEIQAACEIAABCAAAQhAAAIQgAAEIAABCEAAAhCAAAQgAAEIQAACEIAABCAAAQhAAAIQgAAEIAABCEAAAhCAAAQgAAEIQAACEIAABCAAAQhAAAIQgAAEIAABCEAAAhCAAAQgAAEIQAACEIAABCAAAQhAAAIQgAAEIAABCEAAAhCAAAQgAAEIQAACEIAABCAAAQhAAAIQgAAEIAABCEAAAhCAAAQgAAEIQAAC5RHoVl50YkMAAhCAAAQagsA3lYt+sZxM1f59sd+l7G6hSKvlRPyPfj+dE8ZPCEAAAhCAAAQgAAEIQAACDU9gPeUwyNFJZea6v+J/mJOG03QDDoEABCAAAQhAAAIQgAAEINB0BJZUjhdL442t6WVSODXnfKf1cJlpEB0CEIAABCAAAQhAAAIQgEBDEZis3MQbWt5frsQcLqN4M3LOb9HvTUs8n2gQgAAEIAABCEAAAhCAAAQaksDNylVuQ+vLJeb0nALnXlXiuUSDAAQgAAEIQAACEIAABCDQsAROU85yG1rfKSG3KynOvJxz5+q3wxEIQAACEIBAlkD37B47EIAABCAAgeYh8FyBrOZ6ECwQJeO5WX1yDvxGv9/JCeMnBCAAAQhAAAIQgAAEIACBpiPgRlVuj9YNHVDwOQtzzpum33E38R0kwWEIQAACEIAABCAAAQhAAAKNS6CHsuYhf/HGVkfrX12XE9/nfleKQAACEIAABCAAAQhAAAIQgEArgSe0jTe0ZrVDZgMds2fBePwn9btbO+dwCAIQgAAEIAABCEAAAhCAQNMRuEw5jjecvD+sCIV/Foi7TZG4BEMAAhCAAAQgAAEIQAACEGhaAscq57kNrbEFaLhBlRvP7uERCEAAAhCAAAQgAAEIQAACEMghsL1+5zagDs2J458Tc+J9rt+r+gACAQhAAAIQgAAEIAABCEAAAm0JrKCfuQ2ts9tGyexaII7duSMQgAAEIAABCEAAAhCAAAQgUITARwqPN7b+HovntSafzTn+oX4PjMVhFwIQgAAEIAABCEAAAhCAAARyCNyn3/GG1gux4/vnHHO8I2LH2YUABCAAAQhAAAIQgAAEIACBAgTOV1i8oTVPv92T1Uv6Ws6x5/Xb628hEIAABCAAgQ4J9OwwBhEgAAEIQAACjUvguZys9dHv4dKvS3MdXhynsMVSBAIQgAAEIAABCEAAAhCAAATaIbCZjsV7tLy/h/TdnPA79RuBAAQgAAEIQAACEIAABCAAgRII9FecFmm8sfVWzu+F+r2mFIEABCAAAQhAAAIQgAAEIACBEgm8rnjxhlbu/h9KTIdoEIAABCAAAQhAAAIQgAAEINBK4B/a5jauot/TdWxZSEEAAhCAAATKJWDPSggEIAABCECgmQnkOsSIs/iVfnwcD2AfAhCAAAQgAAEIQAACEIAABDomsK+iRD1Y8e2rCl+i49OJAQEIQAACEIAABCAAAQhAAAK5BOzoIt7Aiva/kRuR3xCAAAQgAAEIQAACEIAABCBQGoGBihY1rqLthNJOJRYEIAABCEAAAhCAAAQgAAEIFCJwtgKjBpa3XpR4g0IRCYMABCAAAQhAAAIQgAAEIACBjgmsrSheJyve0Lq049OIAQEIQAACEIAABCAAAQhAAAKFCHRT4IPSeCNrln4PLRSZMAhAAAIQgAAEIAABCEAAAhDomMBhihJvZHn/5I5PIwYEIAABCEAAAhCAAAQgAAEIFCKwmQLnS+MNrVf0u0+hyIRBAAIQgAAEIAABCEAAAhCAQFsC2+vn11qDltL2f6TvSuONLDvA2FyKQAACEIAABCAAAQhAAAIQgEAJBO5THDeqpktzHV9Eja3TdAyBAAQgAAEIQAACEIAABCAAgRIIdFccO7iIGlSFtpeXkA5RIAABCEAAAhCAAAQgAAEIQKCVwDraFmpcOWyR9LfSnlIEAhCAAAQgAAEIQAACEIAABEokMFzxrpe+L22RzpU+Ib1Muq4UgQAEIAABCEAAAhCAAAQgAIEuEHDPldfOQiAAAQhAAAIQgAAEIAABCEAAAhCAAAQgAAEIQAACEIAABCAAAQhAAAIQgECTE2AIRZPfAGQfAhCAAATaEBioX8tJ/f/Rc7rsMMMu4b21fi6dI0UgAAEIQAAC7RKgodUuHg5CAAIQgEDKCCwve8dIvS2kXrD4V9J/SHNlhAJekfbJPZDz+zT9/kVOmH/alfzxUp//TqtObd3O1BaBAAQgAIEmIoBL2yYqbLIKAQhAoMEJjFb+npf27iCfG+p4oYaWFzR+TLqi1O7f3XDy/8lerdvof+an+l1IvqTAMwsdUJgbWu9I35a6kfaoFIEABCAAgQYmQI9WAxcuWYMABCCQcgJu4HgdrI2lG7Vu19T2/6TulcoVD/u7Udpf+mERfVfhL0urJd9Qwm7IrdSqdi/v/X7SSLx213HRj9jW/5O3l74vdYPRQxcRCEAAAhCAAAQgAAEIQAACXSawo1L4k/RxqedD5S427HlSP5KmTZaWwW40jpUuWcT4nRQe5fcz7d8lPVn6FWmxc3QIgQAEIAABCEAAAhCAAAQgUJyAe7DckIoaG4u1/5L0KunR0q2k8Z4h/WwoGaTcXCR9QxoxiLZ2yOHGp3vzaHQJAgIBCEAAAhCAAAQgAAEIfEHAQwDX++Jn3t5+CjlGuo10QN7R5gkYpqzuIz1P6gaWG1pRo2sX7SMQgAAEIAABCEAAAhCAQJMT8JC506WvSd1Y8JDAPlKkdALuyfuqdJzUTjoKyWAF2nMiAgEIQAACEIAABCAAAQg0KIExytcp0hekUU+Mt9OkJ0mRyhN4Qkma8cPSg6XN3COo7CMQgAAEIAABCEAAAhBoHAIjlZVJ0njj6iP9toOLsdJivTE6hHSRwI91vt3IR+xna/9yqbnjZVgQEAhAAAIQgAAEIAABCKSVwK4y3C/69pp3mdReBKP1p7SLVJmAHWUcKJ0gbZG6LKyvS+3BsLcUgQAEIAABCEAAAhCAAARSSMDDBnmhr3/BrSITfil9Sxo1uP63/mZhAQQgAAEIQAACEIAABCCQS6CHAr4r/Y0UN+OCkALxcM3tpW50DUmBvZgIAQhAAAIQgAAEIACBpiHgOT52vf6yNOodWbdpck9GIQABCEAAAhCAAAQgAAEIVJiA5109I40aWJO1/80KX4Pk6kdgGV36Tem90vXrZwZXhgAEIAABCEAAAhCAQHMQ+Kqy+Yg0amC9rf1DpDi3EIQGEq+/9Y7U5bxYerGUIYaCgEAAAhCAAAQgAAEIQKDSBE5XglED633t24kCDi4qTTk56Q2UKedKvZi0y91u4n8ipcwFAYEABCAAAQhAAAIQgEClCJyphN6V/lTar1KJkk7iCYyWhf+QRo3sN7W/T+KtxkAIQAACEIAABCAAAQhAAAIpIOBho89KowbXqSmwGRMhAAEIQAACEIAABCAAAQgknkB3WXio9HnpwYm3FgMhAAEIQAACEIAABCCQEALbyY4/S3F8kJACwQwIQAACEIAABCAAAQhAIL0E3FPxS6k9zHlo2M5SBAIQgAAEIAABCEAAAhCAAAQ6SWAFnXef1A2sRdKfSREIdIbAijrp+1KcpXSGHudAAAIQgAAEIAABCDQMga8oJ+9J3ciyR8FtpQgEOkvgNzrR95IXsx7Z2UQ4DwIQgAAEIAABCEAAAmkl4KGCp0ijoYL3ap95WWktzeTY7cbVy1I3tj6Ubi1FIAABCEAAAhCAAAQg0DQErlZO/TLshtZpUje8EAhUgoAXOr5T6vtrgdReChEIQAACEIAABCAAAQg0BYGJyqWHCtrLIAKBShPooQTPkbqxZb1A2lOKQAACEIAABCAAAQhAoKEJ+KXXL8MIBKpJ4EAlPl/qxpaHp7q3C4EABCAAAQhAAAIQgAAEIACBLhLYXOdHDld+1MW0OB0CEIAABCAAAQhAAAIQgAAEWgkM0/ZEqZcSQCAAAQhAAAIQgAAEIJB6AlsoB3h+S30xkgEIQAACEIAABCAAAQhAICkEviFDvADxR0kxCDsgAAEIQAACEIAABCAAAQikmcDXZHzkhOCkNGcE2yEAAQhAAAIQgAAEIAABCCSBwCYyYpbUnt7OS4JB2ACBIgR2Vvj10hWLHCcYAhCAAAQgAAEIQAACiSDwJVnxsdSNrCuk3aQIBJJK4HwZ5nv1KWm/pBqJXRCAAAQgAAEIQAACzU1gpLL/jtQvrrdIWSBWEJBEExgs616R+p69VdpdikAAAhCAAAQgAAEIQCAxBPzCOlnqF9YJ0j5SBAJpIDBaRka9sAx1TUOJYSMEIAABCEAAAhBoIgK7K69uZD0hHdBE+SarjUFgK2Ujct7yg8bIErmAAAQgAAEIQAACEGgEAh4muIu0fyNkhjw0JYEDlGt/LPCSBHaSgUAAAhCAAAQgAAEIQAACEIBABQj8XGm4sTVTuloF0iMJCEAAAhCAAAQgAAEIQAACEBCBq6RubH0bGhCAAAQgAAEIQAACEIAABCBQGQJekmADaY/KJEcqEIAABCAAAQhAAAIQKJ3Ayoraq/ToxIQABCAAAQhAAAIQgAAEIACB9ggcqIMeWnVae5E4BgEIQAACEIAABCAAAQhAAAKlEVhB0T6VuqH1zdJOIRYEIAABCEAAAhCAAAQgAAEItEfgZh10I+v29iJxDAINSMBLGCAQgAAEIAABCEAAAhCoOIG9laIbWTOkK1U8dRKEQHIJXCDTPpaukVwTsQwCEIAABCAAAQhAII0ElpbR70nd0Do8jRnAZgh0gcC5Otf3/t1dSINTIQABCEAAAhCAAAQgkEfgMoX4RfN+qd1fIxBoJgLLKLOfSP0M7NVMGSevEIAABCAAAQhAAALVI7C9kvYL5jzpmOpdhpQhkGgC7sn1czBF2leKQAACEIAABCAAAQhAoEsELtbZfsE8oUupcDIE0k2gu8x/Uupn4ZfpzgrWQwACEIAABCAAAQgkgcBwGbGvlCGDSSgNbKgngS108Rape3dXqachXBsCEIAABCAAAQhAAAIQgEAjEbhcmXGv1q2NlCnyAgEIQAACEIAABCAAAQhAoJ4EhujiXuLAja2162kI14YABCBQLoEe5Z5AfAhAAAIQgAAEIFAjAnN0nZekfl+5Wvq5FIEABCAAAQhAAAIQgAAEIAABCEAAAhCAAAQgAAEIQKDWBPrpgkdKl6r1hbkeBCAAAQhAAAIQgAAEIACBRiVwgTLm+Sc/bNQMki8IQAACEIAABCAAAQhAAAK1JDBIF5stdUNrrVpemGtBAAIQgAAEIAABCEAAAhBoVALHK2NuZI1v1AySLwhUgcBySrNXFdIlSQhAAAIQgAAEIACBBiDQU3l4W+qG1k4NkB+yAIFaEBipi8yX2gMhAgEIQAACEIAABCAAgTwC+ynEjawXpd3yjhIAAQgUIrCMAu3ifZF0xUIRCIMABCAAAQhAAAIQaG4Cjyj7bmh9v7kxkHsIlE3gOp3hZ+fnZZ/JCRCAAAQgAAEIQAACDU1gc+XOL4ofS/s2dE7JHAQqT+ArStLPj4fedq988qQIAQhAAAIQgAAEIJBWAn+S4X5RPD2tGcBuCNSRgIfaTpb6GdqljnZwaQhAAALtEujR7lEOQgACEIBANQj0VqLWn0jnVeMCpAmBBifg52cH6QDptQ2eV7IHAQhAAAIQgAAEIAABCECgJgTs4j1yirFSTa7IRSAAAQiUSYAerTKBER0CEIAABCAAgboTmCsL1pauI50hfUCKQAACEEgUASaRJqo4MAYCEIAABCAAgRIJnK94i6WDS4xPNAhAAAIQgAAEIAABCEAAAhAogcAIxVmihHhEgQAEIAABCEAAAhCAAAQgAAEIQAACEIAABCAAAQhAoBQCSyrSz6UjS4lMHAhAAAIQgAAEIAABCEAAAhDomMAJiuJ1f37dcVRiQAACEIAABCCQdgI4w0h7CWI/BCCQFgI7txr6TFoMxk4IQAACEIAABCAAAQhAAAJJJtBfxi2QLpIOSrKh2AaBlBLwh2OWrElp4WE2BCAAAQhAAAIQ6CyB3XSihw1O7GwCnAcBCLRL4Eod/VC6TLuxOAgBCECghgQYOlhD2FwKAhBoWgI7teZ8fNMSIOMQqC6BZZX8ctLtqnsZUocABCBQOgEaWqWzIiYEIACBzhLYsfXEuzqbAOdBAALtEniw9ejYdmNxEAIQgAAEIAABCECgYQisqpx42ODHUj5uNUyxkpGEEdhC9vg5eyFhdmEOBCAAAQhAAAIQgECVCBypdP0CeG2V0idZCEAgk+klCLOlftY8hBCBAAQgUHcCfF2texFgAAQg0OAEpit/LdIrGjyfZA8C9SSwUBf/d6sBY+tpCNeGAAQgAAEIQAACEKgdgSVqdymuBIGmJfAz5dw9Whc0LQEyDgEIQAACEIAABCAAAQhAoMIEtlJ6bmj9p8LpkhwEIAABCEAAAhCAAAQgAIGmJeCe4znSxdKeTUuBjEMAAokhQEWUmKLAEAhAAAIQgAAEukBggc79rnRF6SIpAgEIQAACEIAABCAAAQhAAAIQgAAEIAABCEAAAhCAQCkEupUSiTgQgAAEIAABCDQegR6NlyVyBAEIQCARBJaRFa9Jh0nvToRFGAEBCEAAAhCAQM0IsI5WzVBzIQhAoMkIfFn5HSr9UpPlm+xCAAIQgAAEICACNLS4DSAAAQhUh8Bqrcm+Wp3kSRUCEIAABCAAgSQToKGV5NLBNghAIM0EoobWK2nOBLZDIIUEesvmvaT9Umg7JkMAAhCAAAQgAAEIdEDgfh334qnbdxCPwxCAQGUJHKLk/OydVNlkSQ0CEIBAeQTo0SqPF7EhAAEIlEqAHq1SSREPApUlsKA1ubUqmyypQQACECiPAA2t8ngRGwIQgEApBAYokh1hzJNOLeUE4kAAAhUjMKU1pVEVS5GEIAABCHSCAA2tTkDjFAhAAAIdEIh6s+ze3UOYEAhAoHYEprRealTtLsmVIAABCOQToKGVz4QQCEAAAl0lsEprAjjC6CpJzodA+QSm6ZRFUvcqL1H+6ZwBAQhAAAIQgAAEIJBUAqNk2H3S7ZJqIHZBoMEJvKn8uTd5dIPnk+xBAAIQgAAEIAABCEAAAhCoGYEJupIbWnzsqBlyLgQBCOQSYOhgLhF+QwACEIAABCCQdgJvtWZgZNozgv0QgEB6CdDQSm/ZYTkEIAABCEAAAoUJvNwabA+gCAQgAAEIQAACEIAABCAAAQhUgMBApXGkdOkKpEUSEIAABCAAAQhAAAIQgAAEIAABCEAAAhCAAAQgAIHGJODhSj0aM2vkCgIQgAAEIAABCEAAAhCAQO0JLKVLTpf+o/aX5ooQgAAEIAABCCSFAM4wklIS2AEBCDQKAXs5GyRdtVEyRD4gAAEIQAACECifAA2t8plxBgQgAIH2CPRrPTi7vUgcgwAEIAABCECgsQnQ0Grs8iV3EIBA7QlEDa05tb80V4QABGIENtD+trHf7EIAAhCoKYGeNb0aF4MABCDQ+ARoaDV+GZPDdBC4UWauJF1GyoePdJQZVkKgoQjQo9VQxUlmIACBBBCgoZWAQsAECIiAn8XeUhYt5naAAATqQoCGVl2wc1EIQKCBCdDQauDCJWupIrCg1dolUmU1xkIAAg1DgIZWwxQlGYEABBJCoH+rHQxVSkiBYEbTEljYmvNeTUuAjEMAAnUlQEOrrvi5OAQg0IAE+rbmaVYD5o0sQSBNBOjRSlNpYSsEGpAAzjAasFDJEgQgUFcCt+nq20o9ER+BAATqRyDq0WLoYP3KgCtDAAIQgAAEIAABCEAAAg1G4HHlJ5Bu3GD5IjsQgEBKCDB0MCUFhZkQgAAEIAABCJRFgKGDZeEiMgQgUGkCNLQqTZT0IAABCEAAAhBIAoFonmTU4EqCTdgAAQhAAAIQgAAEIAABCEAg1QTWl/VHS7ulOhcYDwEIQAACEIAABCAAAQhAAAIQgAAEIAABCEAAAhCoBoHeSnRX6ZLVSJw0IQABCEAAAhCAAAQgAAEINCOBQ5Vpezo7vhkzT54hAAEIQAACEPgvAZxhcCdAAAIQqCyBPq3JDa9ssqQGAQhAAAIQgECaCNDQSlNpYSsEIJAGArNbjRyQBmOxEQIQgAAEIACB6hCgoVUdrqQKAQg0L4HIpXT/5kVAziGQCALryorNEmEJRkAAAk1JoGdT5ppMQwACEKgeAXq0qseWlCFQDoG7FHkp6UDp4nJOJC4EIACBShCgR6sSFEkDAhCAwBcEoh4thg5+wYQ9CNSagL1/DpX2ktLIqjV9rgcBCIQEaGhxI0AAAhCoLIGoocXQwcpyJTUIlENgmdbIn5RzEnEhAAEIVJIADa1K0iQtCEAAApkMQwe5CyBQfwI0tOpfBlgAgaYnQEOr6W8BAEAAAhUmMF3ptUi7VThdkoMABEonQEOrdFbEhAAEqkQAZxhVAkuyEIBA0xJwQ+sg6UdNS4CMQ6D+BGho1b8MsAACTU+AhlbT3wIAgAAEqkDgyiqkSZIQgEDpBGholc6KmBCAQJUIMHSwSmBJFgIQgAAEIACBuhGgoVU39FwYAhCICNDQikiwhQAEIAABCECgUQjYrbvl3f9u+AsBCEAAAhCAAAQgAAEIQAACXSWwghL4sdQLFiMQgAAEIAABCEAAAhCAAAQgAAEIQAACEIAABCAAAQgUI7C5DgwudpBwCEAAAhCAAAQgAAEIQAACECiPwFqKHkhvLO80YkMAAhCAAAQg0CgEcIbRKCVJPiAAgSQR+LzVmM2SZBS2QAACEIAABCAAAQhAAAIQSDOBHjJ+vrRF2i/NGcF2CEAAAhCAAAQ6R4Aerc5x4ywIQAAC7RFYrIOvSrtJV28vIscgAIGKE1hWKX5P2rfiKZMgBCAAAQhAAAIQgEDdCXh+ludp7V93SzAAAs1F4HfKLs9ec5U5uYVAIgnQo5XIYsEoCECgAQi81JqHNRsgL2QBAmkiEM2N/CBNRmMrBCDQeARoaDVemZIjCEAgGQRebjVjjWSYgxUQaAoCHq67TmtOn2mKHJNJCEAAAhCAAAQg0GQENlR+PXzpuSbLN9mFQD0JjNHF/dxNracRXBsCEICACdCjxX0AAQhAoDoEXlGyC6XLVyd5UoUABAoQWL81jN6sAnAIggAEakugZ20vx9UgAAEINA2BOcrpXlK7eEcgAIHaEKChVRvOXAUCEIAABCAAAQhAAAIQaCICdyivHjq4dxPlmaxCAAIQgAAEIAABCEAAAhCoKoF3lLobWqtW9SokDgEIQAACEIAABCAAAQhAoIkIzFBe35Pa+yACAQhAoK4EmKNVV/xcHAIQgAAEIACBChL4stL6XOpeLQQCEIAABCAAAQhAAAIQgAAEIAABCECgkQj0aKTMkBcIQAACCSTgkQNHSmdJP06gfZgEAQhAAAIQgAAEIAABCEAgdQQ2lsUexvRw6izHYAhAAAIQgAAEIAABCEAAAgkl0E92zZculi6TUBsxCwIQgAAEIACBChPoXuH0SA4CEIAABNoS8MLFD0pd3+7Y9hC/IAABCEAAAhBoVAI0tBq1ZMkXBCCQJAJ3thrz9SQZhS0QaCACFyovVgQCEIAABCAAAQhAoIkIrKa8ep7WR1I+cDVRwZPVmhBYS1fx8zWtJlfjIhCAAARKJMA//BJBEQ0CEIBAFwhM1rmvS5eVbtqFdDgVAhDIJ7B3a1DUc5wfgxAIQAACdSBAQ6sO0LkkBCDQlASil0CGDzZl8ZPpKhKIGlo3V/EaJA0BCEAAAhCAAAQgkFACO8kuD2+alFD7MAsCaSQwWkb7uZou7ZXGDGAzBCDQuATo0WrcsiVnEIBAsgjcL3OmSL1wMQIBCFSGQNSbdZuSW1iZJEkFAhCAAAQgAAEIQCBtBPzFna/uaSs17E0yAfcQu0drjyQbiW0QgAAEIAABCEAAAhCAAATSQmCEDHUjy73EfdJiNHZCAALNQ4Chg81T1uQUAhCAAAQg0EgEvtKaGTuamd9IGSMvEIAABCAAAQhAAAIQgAAE6kVglC58rXTNehnAdSEAAQhAAAIQgAAEIAABCEAAAhCAAAQgAAEIQAACDU9gbeWwX8PnkgxCAAIQgAAEIAABCEAAAhCoEYG1dJ0W6T9qdD0uAwEIQAACEKgHgW66qD8q9pd6v6mk6TLcVKVLZiEAgaQSWFqGTZX6n8860uelCAQgAAEIQCAtBOxQb7h0TI6uqN9uVA1o3fr/XNTesJfQOdLZMZ2m/Vdz9G399sdIBAIQgAAEINApAufrLP/TubxTZ3MSBCAAAQhAoHYE3HjaQfpr6UPSeVL/D6uG2ovoROkZ0p2kbrSlUqIWZiqNx2gIQAACKSawsmz3V7zFUu+/K0UgAIH2CXhu4+nSE6SvtB+VoxCAQBcJbKjz95F+Ver9ntKCsuSSS2ZWXXXVzKhRozIDBgwItX///plIu3Xrlpk1a1Zm9uzZWZ05c2bmrbfeyrz22muZuXPnFky3NdD/J5+WTpDeKH1cmgqhoZWKYirJyB6K5e7ZBVLWEykJGZEgUHcC18uCfaVnSX9Sd2swICLgITGuT/3Pvd3//tEJbGtGwF/St5IeJL1cikAAApUlsJqSG9eqq+cm3b1798x6662X2XrrrTNrrbVWZsyYMaGuuOKKGTemOivTpk3LvPrqq2Gj64UXXsg89NBDmWeeeSazeLGr4Tx5TSFe2uEa6ct5RxMU0HkiCcpEg5viBtQI6ZgcHa7f7saNxsH20X4ki7QTH//6sX77poyPgfVvx0EgAIH6EdhEl54k/UzqZ5pnUhCqKP6f5/kDrk9Ht269P0oazSfwdklpJJ4nEK9Pp+v369J4fep9hyPVJfA1JX+v1P/TVpbyvAgCAoEKEOirNL4rPVi6kTQrblhtvPHGmbFjx4a61VZbZQYOHJg9Xs0d93hNnDgx88ADD4Q6adKkTEtL3tStZ2TDJdJLpXwYq2aBNEjavZWPraQ/k46XzpJ2OP61R48ewVJLLRX06dOnw7it6flO/Y/0D1J3Cw+RIhCAQO0JPKBL+rk9uvaXbvgr+kOVXxqOkdrD4yfSDutIvVgEGvoSaChMh3Fj6fnjlf/Rf0fqRgBSeQIPKUmXCb2/lWdLis1JwI6ZTpZ+KG1T32200UbBOeecE7zzzjtBUuTdd98Nfve73wWbbrppG1tbbfcHmNOky0gTI90SY0lzG7K8su/hQ3tJt5DGe6cyw4cPz3bNuot29OjRmVGjRmXUsArHvnosrBpYOu2/smjRouz4V4+Fff/998PuWHfJRt2ykydPDhYsWJBb/h7vfpfUXbH+yo5AAALVJ7CbLnGrdLI0b5hG9S/fcFdwj9Q3pP6AtI10KWlWll9++cxqq63Wpk5dZZVVwi+0nkvg+tRzDSLx19P4nIKPP/64TX0a1auOkyNT9fseqYe3TJAuliKdJ+A5Iv+SurE8SpoHXGEIBCBQGoHhiuYPUIdKPTIqFNeFBx54YGbcuHFhPRmFJ3H7+uuvZ6699trMFVdcEQ43jNnoXi33cJ0rfSsWXpfd3BftuhjRpBf1P3+/DOwv/ZrUX14twbrrrtttm222CbtovfWLQaVFjazM448/HnbFPvjgg2HXbM6Lwuu6pl8QrC9W+vqkBwEIZAm4Hr699dcu2VB2yiHQW5G/LnV9uqs0++XJH6bi9ak/UlVa3Bh79tlns/Wp5xa4QRaTD7Tv+XiuTx+NhbNbOoEHFXVr6UnS/yv9NGJCAAIxAp576hFTx0pdb4ay4YYbZk488cTM3nvvndEIqSi4rK3nUr399tvhhyjXf7mOL9QrlucgY9lllw0/eo0cObLT13X9+/e//z1z9tlnZzy0MCYLtX+e9FdSjw5DmoTAmsqnh5dk3WL26tWrZffddw/UMg8+/fTTuvTQqhcseOSRR4Jjjz020ITG3C7Zx2XvftLOPX06EYEABCBQBQIrKs3fSD+ThvWWJmO3bLvttsFf/vKXQJOr61Kf6h9/8NxzzwWnnXZasPrqq+fWp6/K1iOkfaVIaQTcm2WObr1mv76XdiqxIACBVgJ+j5sqzdZJ2223XXDPPfeUXU9+9tlnwe233x6ocRbstttuwRprrBEsscQS2XTj1yhlX+/BgUYaBLvssktwwgknBLfeemswffr0su2aMGFCsNNOO+XaYY++/yNFGpyAhwR6joDnRgV+GfjKV74S/PWvf61b46rYHayvEoFv1kMPPTRYeumlQ3tts9S9XH5ByH4t1j4CAQhAoNYE1tAFPTTkc2n4T9XzCc4999xEzSeI6tgnn3wyOO6444KVVlop/gLwoWz33AjPkUDaJ/CADpvdT9uPxlEIQKAAgXUUNkGarX8233zz4LHHHouqqA63n3/+eXDbbbcFRx99dLDBBhsEnscaT6+9fb3vBv369Qs0NNvvviWf52vIu2Hwox/9KPjHP/4RzJ8/v0M7owiuc+W0I/daD8vO9aVIgxHYVvl5SBoWuOZStRx55JGBxpZG90Oit76xL7rookBzw+I37AfKjycj0+ASBAQCEKgZgbV1pewHK/0jbtlvv/2Cp556KtH1aGScP2LddNNNuRO5PaTFcwlocBW+jexqf47UDdMBhaMQCgEIFCDgZ8cfcxZJw3e4IUOGBJdddlngXveOxPXVv/71r+CQQw7xR/f4O2B2v2fPnsHaa68dfOMb3wh7otx5cP/99wf2A/Dee+8FGj7Y5lq+rsN8TPNbA3kTDC655JLgJz/5SaBhi546EzjNyN74Vp4Og4MOOii4++67A4/CKkWuvvrqYOjQofH0FivNX0oZoSUIaZeVlIHrpGEBDxo0qOXkk08OPvzww1LujcTFiV4QNtlkk/gN6x6u3dNeUNgPAQgknoB9CZ8v9Zh7e1dN1QerQhW6Rw3kDHH5SHk7TOqXI6QtgfX0c5W2QfyCAATaITBUx+6Thu9sbrwcc8wxwYwZMwpVR23C7GXQw/dyGihhOh4e6J6ik046KRg/fnzYaGpzcgV+yF9AOJzR78yaXxv07t07/t4Z7rvB6FECmhPW4RXdsDv++OMDD0+MeGj7oNTv6UgKCXhyoSfr2iNS0Ldv35Zf//rXVbkZO7y7qhTh3nvvDb86OH+t+k9tV5MiEIAABCpJwI5Cvid1L7qHq7T88Ic/TO0Hq0JV8tNPPx189atfjepSb5+Qbi5FIAABCHSGwM46yT3AYb2y5pprBnLWU6j6aRP20ksvhT1GuXOt/HuPPfYIrr/++mDOnDltzqnFj7lz54YjAfbaa6+8JYzceJKXxHBObEe2aBHkYJ111onXtZ+IEZ0FnbnD6njONrq2JzqHBbnvvvsGU6dO7ajsU3nc3bYXXHBB4J661vx6rsQvpT2lCAQg0HkCfXXqm9JbpG5oNKt4HtZj0rA+1WKZwX/+859U1pelGH3jjTcGI0aMiF4CXK96DhpD5QQBgQAESiLg4XB2DhS9lwUHH3xwh40jD712Qyp3/pR7ky6++OJOOaUopc7rTBz3yHnoo30cKJ9Zte12pCGvg+0mO2/evOCII47InteahkdL9JIiCSbQXbadKg3HwXq8qoeFNIN89NFH4fhd3eTRg/1vcRiZ4LLCNAgknYA/Vrwn9T+Do5JubJXsO0jphqMC7EDCHlmbQfy12MNl9AU5qk8ni8OGVWJMshCAQOMQ8Ac6r8cYNiK0zmqH9aZcsAeHH354G8cWdkDhuVIdNViSUB+7geg5unJHn204ucHlxmVH03Q8V1YdBdnzxM1ryPaTIgkkMEw2TZCGngT9T3LhwoVJuAdraoPWjQm0sHJ0004Xj70SWFaYBIG0ENhDhvp5cmNjlbQYXQE73YNztTSsSzwkxOPrm01efvnlYP3114/qU48W+N8KsCUJCECgMQkMVrYmSsM6w14BX3vttaLVpufc//GPfwwGDx4c1TGha/bDDjssdGJR9MSEHrBzOfdSxedyuRF1/vnnt+s0Y8qUKbmOibwI13KNeYukN1dfl+mewBxOGrR3lmaWTz75JNhzzz2zD664XCjNLoinfQQCECidwP9TVD9PE6TNMITQPTfh0Gu5Am658sorm7k6DV0Zez5a6z3grb9W+4Wq0WUpZfBa6cGNnlHyB4EKEBiuNF6UhnXFDjvs0O7Hqeeffz50zx7F99ZOeV555ZXU17duXHpNr3jePCfrmWeeKZo3jyLYdddd4+d4FMHKUiQBBDykx24ig5133rnDbsqipdyABzx3Kzb05X4xGihFIACB8gj4pfp9qf8J/KC8U1MXexdZbBfe4UtAI/zTr1TV7vVjYusZvixGI1NXuuUZ7EaW7/kbyzuN2BBoOgJrKcdTpWFDYf/99w8WLFhQtOqx63U5aAvj+pxVVlkluOWWW4rGT+uBO++8s82SRPJSG1x44YVFs+NRaHYbH3HU1gscrydF6kjg17q2C6Xl9NNPb7NGQNGSbLID9qS14oorRvMMnhUrD7FEIACB8gh8Q9Fd13itpUb9yub5WKHbdo+tL2dRymapVu3C2MOBWu+FadquK21E8b3gfM6Ujm7EDJInCFSIwBilk/UsaNftxdbGsgMJz2VS/FA9p8nTXOwYolHFCyz/8pe/bLMml9f6+vTTT4tm+ac//WmWkVjZI+GaUqTGBOzR5WKpJ9+1XHHFFUULjANBuL6B3Yqal3SKdHUpAgEIlEcg+sL/L53WrbxTEx/bC5+HdcQpp5xCtdkOgZkzZ8bdwH8mbmMTX7rlGeglQkIHKNp+u7xTiQ2BpiKwgnL7hjSsO88666yiNYc/ervnKoqrD+DhgsJFT2iwAxMnTox7cw33H3/88aK59LyuiJW2b0tZa0sQaiV9dCGPkQ/XxnLXJNIxAc/b2mKLLaIb9yPx26RWBcZ1INAgBJZRPj6Q+jlap0Hy5AajXeqGToQ8MRvpmIC/0nrZEHOTzpe6x7MRZAll4kmp83VVI2SIPECgSgQ8h/FpaVgPnHbaaUUrDvsNsPfBKK7nItnTYLOJe7HcmxVx0Bzg4J///GdRDGeeeWY2rs55Xrq0FKkyAfdk/UNqLy0tjz76aNEC4kA+AS82F5ts+Kk4elwxkj4Cfg7GSb8TU395LrWXZWzsvCiNAxWGdExgQ0U5SeqlJBpBfqNMhHM57WYXKZ2APYbFnGQsEMedGuCG+K3vB+lrUnueRDKZLQUhqie7ut0DoA1BoLdycZ/Uz0romr1YzeHFhaOFh+2y/ZxzzikWtWnCf//732ddwXuh46uuuqpo3o8++uiQcSvrh7W1+3ykigQuUtrhhGSvLI2UT8CTDb02gzlK35EOlyLpIuDelKgM49vtS8jGWMXxS2H8PO/fUsK5RGksAscpO4H+0bXcfffd5VcmnBESOPHEE6NnycPt0jxSwA1Fz+d1/ZDmfMj8ispDSi0q465uH6yoZSRWLwI3RPfEXnvtFfijSyGxQzI3rhzXLs9vuOGGQtGaMszOhewcw2y85tZvfvObghw8323cuHHx587vKqV+VFZUpBwCv1TkcLjgI488UrBACCyNgCe5jx07Nrpx7Y7UXtWQdBG4W+ZGZRht3dvbnozSQQ8bjeJH20cVtqQUaR4CByirfqluaZZFiEurHTsXK+Ypy8+X5zilUVwPuE44IY3GV8lm91xH89Wi+rIr23OqZCfJ1o7AMbpUeA/4PaqY06Azzjgje5942OB9993Xucqlgc/yuq/y5JrldOqppxbMrYdqb7fddtl44v/T2hV381zpSN/Ydnxx++23FywIAssj8NlnnwXrrrtudOP+W3x50U7X8/QVPxM5uki/i/VQ9tOxZ3Pi+/zJ0mWlSPMQ2FFZDXs1zzvvvPIqDmIXJOCRArvsskv0PL4pvkNTeDvtJZtPkvK1+IvC+5J2o3KtxHbfL5JmL4UENpLNXrg8dGzh96hCcvHFF2fvlRVWWCGwIwykMAGvJ2bHIGZq/cMf/lAwop0Qrb766lE8e8fdQopUiMAOSmexNLjssssKFgCBnSPw7rvvBqNGjYpu3BsqVF4kUzsCj/i5yFEveZArfnG6WZob144dVsmNzO9OEfC8uTTI6jLSLuoDD3lDKkfAC27GHA49IcZ2LIGkm4A/XN0vdW9fqZpbz0a/fb4/eCHpJOA5i5676OHWwaRJkwpWHl4Py27bHW/ZZZcNXn755YLxCPyCwOuvvx4MGTIkZOahljfeeOMXB2N7XvDYQzDNVjpFOkiKdJGAXWeGXr5+8YtfxHCzWykCXpB0wIABHkLkG/f7XSwvTq8tgd11uajSibbvK6xXjhmnFYjn4TAb58TjZ+cInKjTZkhdHkmW3jLuGWngBTWRyhOwd9dVV101ehbPS/LNgG1VIeCv7OGHDG2j+8BbP3dLS5H0ErhGpodlWsyhxcMPP5xdiNge9R577LHKVzINmuJTTz3ld9GQrxtTxYZauscrKgdt/QEZ6QIBf4W/RxqOzSw22bBB77maZsteccxZOk+6thRJBwE/I89Lo/KLtt+Kmb+39qOGdHTc3e47x+Kw2zUCR+h0s7Wb71IcknTtap0/+0KdGqy22mrBrFmzalrHNNPFvDaMHYyYtXS3zhcXZ6aMwPqyd7o0qmej7UsKWz5lecHctgS+q59hee68884FFyR+7bXXsvONevbsGbD0UPm1vt3gRx4aPa/tpZdeKphI3EW8yuXwtkXFr3II/FSRg+WXXz547733CsImsHIEDj300Oifwgviznytcu7U+sb9Hz8nORp5tlpP4e65yj3+PYUhlSXg3gtzniPdqrJJVyS1byiV0I078wUqV28WS+ncc8+NnrmPxX2lipRgZRNZUcn1rWySTZ3aGsr9h9Ko3KPtGwozayS9BOws7BNpMGzYsODDDz/Me+ztrGHjjTcOy9we9K688sq8OASURsAf/iNPjfYjMG/evLwTvR7XiBEjomfsM5XNkPTeXvWz3N3v/ureMn78+DzIBFSegNfYWmuttaIb9+L6FT1XLpNAT8V/UxqVXbT9qsKmFAg/VWFI5Qm4d/GvUvP3MEJPmk6KjJAhXjcv8PolSPUJ2CVxzDnGA2LfPSk3g+zwxxn/f701QTal2ZSVZbyXSonq3mjrMB9D0k3gTzI/LFO7JC8kxxxzTFTmwY9//ONCUQgrg8DJJ5+c5XnEEUcUPPOuu+7KxlH5XJbuW6z21vvF0S7Hmaxd8PaqXqC9v2hdg2jIi1/UkXQQOFJmxiudYvsXpSM7qbXSL9PROH73ZCRlGK5fqIM99tijepUHKecR+Oijj4KhQ4dG9amf0STIwTIidC6l7Y+SYFDKbXBv1RvS3DrXvVvu5ULSTWADmR8+LzvuuGPeM+4Ae8J2L5biBZtuummwYMGCgvEILJ3AokWLgq222ir7TN18880FT/b/NHOXup7dXIqUSOBYxQvnEbg7FqktgdjaD57740YvknwCfWTi+9Ko0im0vV3H0+IZL/nEi1voZ+YWqcvgPeloaT3Fc/FChzfvv/9+bSsTrhb8/e9/j55FDz1app43gq79A2nU8GOtrK4XxnJKwvOvojKOtu499rBtJN0EPErhYWk4b8iOw3Jl2rRpoWdBxxk4cGDwxhtv5EbhdycJvP3228HgwYPDZ2rQoEHBW2+9lZeSeUeLHqsMHpcmaeSAzEmmeJylh90E//znP/OgElB9Am7cjh49OvqHcXQybxOsKkDgJ35uiuhjCl+ywDkEVYeAvfvdLXV5uIFbL7F78cnS4He/+131Kw+uUJDADjvsED2Xf67XjaDrHuf7QOqG1g+lSNcIDNLpT0ujso22sxS2WdeS5uyEEPi27AjL9YQTTij4bO+7775RuQeeW4RUloCHakZlsPvuuxdM3IscR3G0PVSKdEDgch0PigEtSJnAihO44447ohvXkwzxltTBTZuQwx6mFpVbfPuOwv3lFaktATdsz5fuXdvLtrla2Pj+0pe+FHhBXaQ+BLyOjryQuYHjIUgbtimhrv0otW4+WZdxnWAbeBHpGnOf3V/6b2m8nvX+XOm2UiT9BDz64w1p6ACjkJfWCRMmZMt/3Lhx9alcmuCqBx10UJZzoQ4Y+xcYOXJkFMfvO7nL26T/bqxgDjy+skX+81u8eBlSXwK77rprdONeWsEyJqnqEPDXVQ/1jMosvn2kOpck1YQTGCb7ZksDu8xF6kvAE+RdFtKJ0krISCXyrnStDhI7Ucd93UXSAzuIy+GOCXiY9r+kUXlG288V5mG6SGMQ+JayEZbtn/70p7zKwx+u1l577fB4//79g3feeScvDgGVIfDBBx+EwzJdHl6apNCUossuuyx6Dr39rhQpQuAuhQc/+9nPKlM6pNIlAl4TonUtGP+DXqVImRFcfwIeHjZBGq9ocve/Wn8zsaDGBM7zPbH33nt3qR7g5MoQmDlzZjBkyBD3KPnZ3LGL94J7S6Nha37pb08czx4G920vEsdKIuAv5bdJc+tX/4/cq6QUiJQWAuHzpWe2oHvx888/P3sPnHnmmZWpJEilKIHzzjsvy/uss87Ki2cHJCuttFIU50XdZJ5fh+QQWE+/A62k3WL/+EgyCMS6bC/MKS9+JoOAK5P/J40qmGLbB5JhLlbUiMBgXSfszXr22WeTUZlgRXD22WdHz+d9XbwPrtP5UVretjc8dQUdr7dDli5mNxGneyjZ9dI4d++78ey5PEjjENhBWQnL+fTTT8+ruaZPn57tYRkzZkzBHpa8kwjoEgH3IEbLD7kHsdBaZrG1C112uzfO7Vi5nIQvi8cee2yXCoOTK0vAq3KriP2PxGPPmedTufu9UimdqYTCfwix7evaLzSMcGylLko6XSLgr+JPSf8htfOfasgpSjTYeeedK1shkFqXCMyYMSNYaqmlol6tTTpZ8D912UqjdLw/RdpXilSHgD9oXSrNrWv9+/DqXJJU60jAvcT21Bq4UZUrbnz5uNWu3ZHaELj33nuz3E855ZS8i3oe3dJLLx3FmVjH+yeRlx4lqxZ5svDUqVPz4BFQXwKxdQp+lci7p3mNOkJZjyqVaGuPnV+S7lHg2H0KQ+pPwC/Eb0tdZu9Lt5dWUpz+h9Lg/vvvr2/lwdXzCJx44onRs3pjJwp9F52zWBpvZEXp/bwT6XFKaQR+r2gR5/j2uNJOJ1aKCISjq1zexx13XN7zO2/ePA8BDu+B9ddfP+84AdUlsPnmm4fs7fZ99uzZeRfz1COXXavi/TP24F1gKN/5znfyoBFQfwL//ve/o5vWa4PY2xJSfwLuFve8gKhsvPUL2Nellu7SV6Xx497fSorUn4CHc90rdZn4pfkMaU9pJeQHSiTYbLPN6l95YEEegffee89r8rjM/byOKaPA11DccOkTbXOfa/9eIGW4jCBUWE5XeoV4/7zC1yG5ZBD4jcvbCxAXWrfJjjF83HrttdfmPd8EVJdAbF3CgkuWuH7t0aNHVEZuWyAi0Eca/vN4/vnnq1tCpN5pAltuuWV0436Xu7buBDaVBXOkUZlE29yvq0cViHNP3a3HgIiAG8M/k0YNZg91GBEd7ML2WZ0b3HTTTZ1+3jmxugQOPvjg6Jk9s8RyHqh4r7hcO9CpJaZHtNII/KQIb7+MI41HwENEw9EGY8eOzasEFi9enF1jdOWVVw4WLVqUF4eA6hJoaWkJVl999bAeHDFiRMFlS3bccceonvSIEc+tbHqxp55g4403rm7pkHqXCPz1r3+NbtzxTX/H1hfAqrr8B35mcvTSAmb1U9j0nHg+78sF4hJUPwLuZYyGErrXeM8umOJho4GHVdgLE5JMAg8//HD0/E5Refnlrj1xg/xOaXROsa17yXzsq1Kk6wQKfagy3z91PWlSSCiBbWRX+Hz9+c9/zqs8br311uyz94c//CHvOAG1IXDxxRdny+GGG27Iu+jll1+ePa7ytGOTppebRCD47W9/mweLgOQQsCfImKv35Zv+rq0PgGV12cl+XnL0If22i/dCcpYCc+N7GQUkWQTsJfAWqcuq3CFl8Zz82mkcdthhyak8sCSPgL/K+mtsa3lvGS/AAvvu9XLcqCEVnVds+5ziVmoYagFzmiLou8plId6TFL6mdI0y1UOFkeQTcCPa7zrBxx9/nPfcfutb3wqfOXu9mzNnTt5xAmpDYP78+cGgQYPCsthzzz3zLmqnQ3369Inqx8uSf9tV18KllPw8jYVtmTZtWh4sApJFYPfdd49uXH/pQ2pLwA4O/i2NyiDaTlFYe94gV9LxhQXOY5KooCRQjpBNV0oHdNK213ReMGHChGRVHliTRyDmFOMP7ZT1OJentNBLf1QHFNr+sJ00OdQ+gXV1OBrOW4htZ8LaK+P2reForQj448TH0mCXXXbJe17teGHJJZcMy/6AAw7IO05AbQlEw6979+5d0DOk1490WUo9Nam3NBQPD2g2+YYy3GfbbbftNmzYsGbLe+ryu//++0c2Z3eiALZVJeC64WrpFjlXma3fu0k/ygmP/3xHP26MB7Tun1ogjKD6E/AX1QOlszphihvPq6644oqZbbbZphOnc0otCYwb5zZUKPvqb6EeqA0Vfsl/o3Q4vLA1WnbzS+25Bxwpn4B7GCs9r+P58s3gjBoT+LKut4yvGXs2sybccsstmblz54a/Y+9C2ePs1JZAVAaff/555m9/+1vexWNl6A6dsVGEZm1oFbypIyhsk0Ngt912y7R+0fEL/5DkWNbwlvxOOfRcxrj4S80BUg8T6kh8fq7YO+HGuYH8TjWBcG7Xvvvum+nevRn/naSr7NZbb73Mmmt6FFrYI507fNDDs73OmnuyOyODdJK95SHlE1iv/FM6POOZDmMQod4Esi/jO+yQP61HHgZD+5ZZZpnM9ttvX29bm/766qDJDB06NOQQlU0cynbbbRf/P5gt22b7z+gJwFsbTKGbOg6M/WQQUCMrs/XWW0cTt/lkXpti8QvYjwpc6iSF3VogvFDQ4wp8uMCB/QqEEZRcAlfItKnS46SFXsDDfybyuJTcHGBZGwKx/33ZFwFF6CX13OXhbSLn/wjyg8IQ93Q/KvXx7JCZ8Ah/SiHQ3lDsUs7PjdOigFI+iOWex+/aEgjfafzxY7nl2t4C7skaP358aM0+++yT0Ryu2lrG1fII+GPifvv99xVGQ+UzmpfVJs7AgQMz/pjVKtn31WZraK0tAINHjhyZsSLpIBAbkhR/MUiH8em0cqLMduM2Vz1BvhzxR43cNI4vJwHi1p3AfFngOXfnSN+Q/q+0j9SypHRj/fMJvvxlj4BB0kBALqQjM7MvAgq4QBp+hGw96AZTIVkNU3uwAAAmjklEQVSowP9Ir5H6w4uHEa8s9VAZjzo4XPq5FCmPwN6KnltXduW3hyHOKc8EYteYgFtOfmYysWcya8IjjzySWbjQj1sms/POO2fD2akvgags5HY/I0+uecbEynJTHQz/VzZbQyv8DxN7cc+DREDyCMRu3PiLQfIMxSIINB6B7ytL/i9vz2f2Ynae9HXpUVI/j7022mijbgMGdNaPhlJAakpAIwR8PTek/JLnlz2XsTUuPm4nJx5K+CupP+OuJe0n9SfbA6T/J71dOkVarGGmQwgEIFCAwEYK8/NUcH7rAw88EJ4ix20e1RPu86f+BPxRsWfP/05vjcooblWsfWGvzJv7WKHJsPFzGm0/fFGPvbg3Wv4aMj+bbLJJpm/fvpl58+aFPZLK5KcNmVEyBYFkErhLZll3kf5C6hcE94CE4yZi/1gUhCSdwLLLLptZa621ur3wwgvukTxYeqJ0vNTOE55r3b6o7TwpAgEIVIdA9sNxoTr0wQcfDK+6zjrrZJZeeunqWECqZROQm/3MhhtumJk0aVImKqN4Im4Uu3Esf4gOdhnf32w9WuFngUI3dRwU+8kisMQSS2Q23zz8MOChFFslyzqsgUDTELhDObUzkz2lz0oHSjNjxozxBkkRgdj/QL/BrSzdSfpj6RXSJ6U0sgQBgUAVCazrtIcPH56x19a42KvdY489FgbRMRAnk4z9qEyefPLJjNY2a2OUP2SNHj06CgvLuJkaWoOU8xXcGuXFILoH0rPdYIMNImPXjHbYQgACdSFwi67qB/IzXz0as+59JB0E/EW2VVaPdthCAAI1JRB+oVpttdXyLvrss89mtEBuGM6wwTw8dQ+IymTRokUZN7ZyJVamYRk3U0MrzDCNrNxbIh2/Y+XG5/N0FBlWNjaB/sreIA/p9RdZJF0EqE/TVV5Y25AEir6TTp48OZvhtdf2jAkkSQTiZRIvq8jGWP3qrq1uTdfQinXpRUzYpoBA7MaloZWC8sLEhicQPoeuTz0eHUkXgVh9mh3jkq4cYC0EUk1gGVnvYbsFR1i9+uqrYebsTnzVVVcN9/mTHAL2Wu4pLZaorOLWxepXz4MdluSG1pYysHfc+C7uF/160MV0Ob0GBGI3Lg2tGvDmEg1HwHOr7IK7UkJ9WimSdUhn2LBhXgjeV/YixZW8L+qQGy4JgaoSsLfNIRW+QvY9JvZuk71E9PI+YsSI7At99iA7dSfgBvAqq6wS2hGVVdyonDIdk+SG1u9k+HvSC6WbxDPRyX1eDDoJLgmneXhSnz7hkgRDZU/oEjUJdmEDBFJC4Eey833p1dLtpF2t+6lPBTHNEhvdkX3pS3N+sB0CVSKwh9J9R3qbdG/pf7sytNMFyfYk57yUh0lGL++FjnXhmpxaQQJR2URlFU86OtYaNrqr/2zjaVdj312rR0onSV+QHi/1i3ZnJHTrwkLFnUFX/3M8PCk2F6Sti576m4cFEEgDgb4y8gDpPdIp0l9LO/uSTX0qeGmW2P9C6tM0FyS214JAT11kV+lNUncAXCDdSNpZWSY6cYUVVoh2s9s333wz3I99DMkeYycZBKKyicoqbtWQIW06QAcnvaEVt/1L+nG2dKr0Duk+0nKGFnrydoaFNU0hnRIru7As05kLrIZAIgjYg8XPpJ51/bD0EGk5Q8ioTwUszUJ9mubSw/Y6Ehisax8lfUL6nPQ4aZs3a/3uSLLvMPaEnSszZswIgwYP9qWQJBKIysbu3RcvXtzGRDuJ6tGjRxQ2IE0Nrcho2/x16Q3ScoYWhndzoZs6SphtsgnEyi6/Zkq26VgHgaQS8KqKW0r/Ki1naCH1aVJLtES7Yg2tASWeQjQIQKAtgbX18xzpO9LbpHtLSxlaGNafvXv3zvTs6c6yL8RraNltuCX2zvNFBPYSQSBeNrNnz86zKXa8fxobWnEXV+UMLQz/mcT+ueSBISDZBOI3brItxToIpIZAvD71JMgDpPdIp0h/LS02tJCGluCkWahP01x62J4wAu6+2FV6k/Rd6QXSjaTFpGj9GX9pjz2jxdIhvE4E4mUTL7PInNjxVDa0onzkbjsaWlj0xs5NiN/JJBBrJPMFNplFhFXpJhBvdHU0tJAPV+ku6/jX8vB/Y8qzg/kQqCeBeN25jAw5SvqE9DnpcdLcoYVF30fjL+2xl3UlgSSJQLxs4mUW2Rg7nm1oHaGDC6QeRpIU3SQyuMxtsaGFSzqdVpe2ZSZJ9CQQeP99j2wK5Tr9LXaffqxj6/w3Wt7fbylknrTYuQ7nfPg16v2T90CUEOBnotDQQurTEuAlOcpHH30UmXeadorViXN0bNcoYs52c/2eLi12rsM5H35pv39Wz7nvy/m5tiKfI80dWhh6Tu7XL9+Bsuf8RFLoeHSMbX0JxNsS8TKLrIqVXb80Dh2M8lHu9nOf4PGvSDoJLFy4MJ2GYzUEGo/AfGdp/vxw03i5a4IcUZ82QSGTxaQSKFp/ti5jE9pN/ZrU4mvbloiXWWRxrOwS/U9ykgxu70tZsWOeRXiHdB9p3Cuhx80G7777boCkk8Buu+0WlfluKksEAhAoncCViho9P+VuH9a5h0jjXgnvc3r33XdfOisTrA5OOOGE6D44XmWJQAAChQmcpODoWSl3W2zo4B+d5vLLL59XE33wwQfZa/zxj3/MO05AMghceuml2XJ666238ozSYtPR8Ut7Fr6vUhn6oqy+XHq11N4IcyV0C1JoLGVuRH4nk0Cs7PJdvCTTZKyCQJoI+B9DNNfAy2i4cXaF9FVprlCf5hJJ2e9Zs2ZFFlOfRiTYQqBzBOJ15ydK4lrp5dInpYWkaP0Zm9uTib3zFEqDsDoSiJdNvMwik2LHZ6exoRW/oT0+PLqhH48yWGRb9MYuEp/ghBGI37gJMw1zIJBWAvH61EMc/ia9XOoeqxZpMaE+LUYmJeHUpykpKMxMAwEvpHSX9HLpbVL7PGhPwq8cc+fOzbS0tGS6d/9iFo/n/vi3w2MfQ9pLi2N1IBAvm5ijtqwlseOz0tjQ8j//8dLLpbdKS510xYuBYKVZeDFIc+lhe0IJuAdrovRy6Q3SmdJShPq0FEoJjkN9muDCwbS0EHhehl4u9UiqD6SlSlh/OrKfw6WWio/K/u/6WTNnzsxYkWQSiMpmiSWWyPTq1auNkQsWLMjE5sCmqkero6GBbTJa4EfoYklztAocIigNBGJl92Ea7MVGCCSYQEdDAzsyPXwGY89kR/E5njACsbIL/zcmzDzMgUBSCXwqw66RXi4tNjRQh9qVGdHRTz/9NK+hNXz48MwLL7yQefPNN6NobBNGICobl1WuuExjMiPpPVrlDA2M5avgbjjP4NVXC003KBifwAQRsCviGTPCuukzmeUx0AgEIFAeAS9tUOrQwI5Sfs0RqE87wpTc47Gy459icosJy5JBwE7Wyhka2JHV2RbUa6+9lhk1alSb+GPGjAkbWrFntM1xftSfQFQ2LqtccZnG5M0kN7SOkaFPSEsdGhjLV8FdGloFsaQjMLqpZS0vBekoMqxMFoHfy5yjpJUai0J9mqzyLcua6dOnZ1q/unquSDlDnsq6DpEh0AAEblEeLpFW8jnJvsf43Wa77bZrgyl6eX/jjTfy5nC1iciPuhGIGlNRWcUNib2vOvjVL2bgxWMlY3+izKhUI8s5Cm/sCE4ysogVpRKI3bjZCqrUc4kHAQiEH60q1cgyThpaKb6pqE9TXHiYXmsCL+iClWxk2f5pUo8wKDgqIHp597qvb7/9tqMhCSLw/vvvZx2VRGUVNy9Wv7ondEqSG1pxuyuxz4tBJSjWKY3YjUtDq05lwGUhECPgOVoz3TPyySeM5I1xScUu9WkqigkjG5eAvb0WHX4df3l/+eWXG5dCSnMWL5N4WUXZidWvHiK6qJkaWl5ba5bn+mhBuIgH25QQeP55O/cJ5ZVohy0EIFBXAuGzGHs262oMFy+dQKzMJpd+FjEhAIEKEij68X/99dfPunyfONGDu5AkEYiXyQYbbJBnWqyhFZZxMzW0DONR/3nooYe8QVJCQEtuZx5++OHI2keiHbYQgEBdCYTPIvVpXcugUxd/8MEHo/OoTyMSbCFQWwIv+XJ+KY9chUeXHzRoUGbdddcNfz7wwANRMNuEEIjKZI011sgMGTKkjVXz5s3LvPiinaSHEpZxszW0wjs2ghSRYJtsAnZz2jo8yS6ppyTbWqyDQNMQCN/WqU/TVd5+EZg0aZKHLnmR1ewXrHTlAmshkHoC4Rd/L0wc+5CczdQ222wT7utZzcyf77XkkSQQWLRoUebf//53aEpURnG7HnnkkfgaWmEZN1tDK3wxiH3Ni/NhP6EEYuXFp52ElhFmNSWBsD7N+cfSlCDSlGmXl14WusnmZ6T2OohAAAK1J+C3dX/syMTecbJWjB07Nty3Q4zHHnssG85OfQk8+eSTmTlz5oRGRGUUtyhWlv6Y1ZQNrUnK+Pz//Oc/gSdxI+kgEPtiHr7YpcNqrIRAwxPwQrcv+Z+O//kg6SAQq0/5cJWOIsPKxiTgjxxPOWuxZzKb06233jq7f++992b32akvgXhZFOrRipWlHQuEKxc3W4+W3cX700C3CRMm1Le0uHpJBNytfv/990dxeTGISLCFQDIIhM/kfffdlwxrsKJDArGyoj7tkBYRIFBVAuHHY3+omjt3bpsLLbfccplNN900DLvuuuvaHONH/QhEZeE5dCuttFIbQxYsWJB59NHQFYTDsx0DzdbQcubv8J8bbrjBGyThBNzI+vBDe5IOXaHiISvh5YV5TUcgrE+vv/76pst4GjM8bdo0zwfxkBav4cPXxjQWIjY3EoHwY8fChQsLDh8cN25cmFev//r44483Ur5TmZfnnnsuE3lsjcomnhHP3YrNp8t+yGrGhpY/DQS33nprMHv27Dgj9hNI4Nprr42syu5EAWwhAIG6ExgvCz7VcOy4p6W6G4UBhQm0fo3tpqO3S5mfVRgToRCoFQG/jIeeLgp9/N9vv/2ybt5j70K1so3r5BCIyqBbt26ZQg2tWBku1KnZYR7N2NCy57qH5Xmp2y233JKDkZ9JIuBu2Jtvvjky6Zpohy0EIJAYAv6HcpOtueYaHtHElEoRQ6IXBR3mw1URRgRDoIYEZupad/p6f/vb3zJ2fBGXoUOHZrbddtswyKMGPJUCqR+BqP7cYostMiNHjmxjiL0R3njjjVHYPdr5JPrRjA0t5z18I+DFILoNkrm96667Mq1OS+wdi+XRk1lMWAWB8KU9+icEjmQSmDx5cuS0ZIYsDF/ukmkpVkGgqQiE76MzZszI3Hln/mO5//77hzDefffdzO23uyMaqQeBu+++OzNlypTw0lGZxO245557Mh9//HEU1OarY7M2tPwFdtH48eOD1vk/ERy2CSJw9dVXR9a0uWmjQLYQgEAiCDwoK6a98cYbGbsOR5JJIFaf/k0Wtv10nkyTsQoCzUDA81zds1VwVICHD3oBY8tZZ50VbvlTewIR+/79+2cOOOCAPANiHTdzdZDhcq2E/q5tcPLJJwdI8gi8+eabQffu3d1PvkC6YmuZsYEABJJJ4AyZFXzzm99MXmWCRYE8mgXyYmYnGNZtknkLYRUEmpbA5cp50KdPn2DmzJl5NdZJJ50UPbuBndkgtSUgRyRZ/scdd1zexV2/qgEWxcFFZOwx3sI39tJLLx3MmjUrDxwB9SVw1FFHRTetKyAEAhBINoEVZN58TRJu0RC1+lYeXD2PwB/+8IeoPs36Hk727YR1EGgqAjsot+Ezet555+U9vx988EHYCHOc3XbbLe84AdUlsM8++4Rl06tXr2Dq1Kl5F/vzn/8c1a/e7t5Ud24JmfWQl+C3v/1tHjgC6kfgo48+Cvr27eveLOtaJZQjUSAAgfoTuEgmBIcddlj9Kg+unEdAk7SDlVdeOXoR2Kv+twkWQAACOQTsCdTz0IMRI0YEcvee9xwffvjh4TOsj1mB3IznHSegOgReeeUVj64K2X/3u9/Nu8jixYuD0aNHR/XrGyrDHjll2/Q/d/WNPXz48EAe7vIAElAfAqeeemp0097a9HcoACCQHgKrydTFSyyxRMt7771Xn8qDq+YRkJOSqD59ReXTrPOy0/MUYWmzEjhYGQ+f1SuvvDLvOdZaWkGPHj3C49ttt13ecQKqQ2DXXXcNmbuB+8ILL+RdRC7do/rV2x80683bXr79FeF5aXDJJZfkASSg9gTkeScYPHiwe7J8024lRSAAgfQQ8HoMwfHHH1/7yoMr5hHw19Z11103ehE4JD23EZZCoOkILKEcT5MGa6+9diBX7nnPc2xKRaClb/KOE1BZAnfccUdUdwaHHHJIwcQ32mijKM6HKru+TXfXlpjhcb6xV1hhhYKTEAuSJbBqBI455pjopr2/xPIjGgQgkBwCG8mUFvdqvfrqq1WrJ0i4NAJ/+ctfovr0LZVL7+TcJlgCAQgUIHC8wsJnVq7c8x7yTz/9NFh22WXD41rHKXRykxeJgIoQ0Jpm2SGB8vpoD+V56d57771R/ertKQXKk6AYgYe1HxTyJpJHloCqEXC3rLrG3Zu1SLperHzYhQAE0kPgEpka7LLLLlWrK0i4YwLxlzKVxzfTc/tgKQSalsBSyvln0mDjjTcO3COdKxdddFH25d7TLJDqEDjjjDOynH//+98XvMiWW24ZxZmtMhvctHdtiRnfQPEW9+zZs+XFF18sCJTA6hP42te+Ft20F5ZYbkSDAASSR2B5mTRdGtx2223Vrzi4QkECP/jBD6L69F/Ju0WwCAIQKELgNIWHz+5f//rXvGfbjS83whynd+/ewdNPP50Xh4CuEfBHfzlkCxmvs846gR0K5cpVV10V1a/enilFSiDwJ8UJtt9++1ye/K4BgRtvvDG6ab209tIllBdRIACB5BL4kUwLVl111WD+/Pk1qEG4RJzAM888E61DuFDl8KXk3iZYBgEI5BDwPJ8p0nCY4PTp0+OPdrg/adKkQB0D4TvT6quvHsyePTsvDgGdI+A1sTxHzvztbbDQumVe62zo0KHRO6vn1fWXIiUQcLffJ9LALVWkdgQ8xGXFFVeMHGAcVkJZEQUCEEg2gZ4y7zlp8LOf/ax2lQlXCl1Db7bZZtFLwG+TfZtgHQQgUIDA3goLn2E7wCgk//d//xc948GBBx5YKAphnSDg5Uki9j//+c8LpvDjH/84G0dxDyhQfgS1Q+AgHfMKz0zkLnh7VSdwzz33jG7aieKP++F2blAOQSBFBOw1dJEXMf7Xv/5VncqDVPMInHjiiVF9agcYnvOBQAAC6SNwj0wOXbo/++yzec+5vRJ6BJbjWAu5hM87iYB2CcRdtW+zzTYFhwy+9NJLgRcubuX+kLZIJwhcq3MCu2y01xGkugQuuOCC6Ib1nI6RnSgvToEABJJL4OcyLRxmUchrU3Vrl+ZLffz48a5PPTrAQwa/LEUgAIF0ElhTZvs5DtxDXWgR4/fffz8YMmRI+A6lDoLgqaeear5Kr0I59iLQAwcODFkus8wywTvvvJOXsudqbb311mEclYudtq0vRTpBwF8AX5MGRx99dB5oAipHwJM47QbarKV7SREIQKCxCLiH+n5psPPOOxdcG6ZyNUpzpxR/6RLvk6QIBCCQbgJny/zwxf6EE04oWMHdfffd4Vwix3OjywsbI+UReOuttzx9JeTshYmLOXGyl8eoPLT9vRTpAoGNde4CaXDrrbeWV2LELomAJxOuttpq0U2Ll8Eu3KycCoGEExgm+z6SBmeffXZJ9QORyiNgT2TbbbddVJ96yBFDsBP+UGAeBEog4EWMn5QGbgDcddddBSuGCy+8MHr2QwdEH3zwQcF4BOYT+Pjjj4M11lgjy+/cc8/Nj6SQCRMmZBu0Ko//SPtIkS4SOFbnB/369Wt54oknCoInsHMEFixYEB9b/Kw4c8N28WbldAgknMAusq/F87VuvvnmzlUcnFWUwOGHHx69KHwgzisk/F7APAhAoHQCoxV1pjRYfvnlg/fee69gPXDKKadEdUCw4YYbBv6YjbRPYM6cOcHmm2+e5Xb88ccXPOGjjz4Khg0bFsWbo7LAk2vp92+7Mbvp6BXSYLnllsM5RsHbr/xAT+AcN25cdMO+J74rt1sKHIQABBqFgIezhcOFH3jggfIrD84oSOC0006L6tO54rtlo9ws5AMCEMgSOEB74XPunutCCxm7cjjkkEOiuiDYaqutgkKu4QtWIk0Y6IboV7/61Syvb3/72wWHtvuddZdddsnGUzkcnC0VdipCwC6K75QGq6yyStEvCU14j3Y6y573Zp7SGVImEgoCAoEmIuBx7cFSSy3VUsiTVqcrliY98c9//nNUn3pi9m5NdB+RVQg0G4HLlOHwef/f//3fgjWenTXsscceUZ0QrgdVyKlDwZObKNDzWTfYYIMsp5122qmgsxEjiXlxdXw7y0OqQKCf0nxUGqy//vrBjBkzmuh2rGxWzzrrrOjGni+eX6lCWZEkBCCQbAKeO3S91J4IW6ZMmVLZSqaJUvvb3/7meRuRMyG+sib7vsc6CHSVgN9Fw7UJtQ3OPPPMgrWdvWXvu+++0btWMGLEiMAuyZH/Enj11VfDjhMztHp5oXnz5hXEc95552U5Ku7LUpbLEIRqyTJK2JCDTTbZJPB4TaQ8ArHF9RaL4z7VKijShQAEEk/AE7z/JQ1GjhwZvPzyy+VVJsQOrr/+eq/lEjWyfpb4EsdACECgEgRWUiJvS8MGwGWXXVawNvTQwh/+8IfZRoLdlU+cOLFg3GYKnDRpUjjPLeLnxYndC1hIrrnmmtABSWvcd7UdJUWqTGCk0g/dvttb3ptvvlmobAjLIeDxrT/60Y+iB96NrEOrXE4kDwEIJJ/AAJnoBcoDvQS0PPbYYzk1Bz+LEfj9738f78my+2cEAhBoHgJeX+sTadCzZ8/g9ttvL1ZVBKeffnr07hUusmuvr34na0Zx75SWE8rysKv2YnLPPffE434m1us2z+1V/5wOkQlPScMFOJljUOw2/W+4u7D322+/6Mb2cMG961+EWAABCCSEQF/ZcZs0WHLJJVv++c9/tl+hcDQ46aSTovrUvVnHJ6QcMQMCEKgtgS10OXu/c90Z3H///UVrx0svvTTeaAh23HHHoJncv9t9+2677RbVm2GD03Nbi4l7/gYMGBDF93vr2NoWLVczAX+JvVcaTui2b30kn4Dnsn3ta1+LblZ/EdhWikAAAhCIE+ihH5dIgx49erRcccUV+ZUJIeFE7e9973tRfbpQvA6MQ2QfAhBoOgK7KseuC4LevXsH7S2b8eSTTwZjxoyJ6o9ghRVWCLzQcaOL38+jhYjNaeWVVw7aGz3hhYr79u0bcfIIrL2kSJ0IeI7BddLw5eCMM84o6m6z0W/kQvl7/PHHw0XzzEfqsa3rSREIQAACxQicoQPhPzivCVVscnKh+qbRwzxMPbbWy2xx2rkYRMIhAIGmIrCfcrtAGi6m+6c//alodThr1qzgf/7nf6JGRLj91re+FTSiV0KvNWZ37V7k2WysdhDy2WefFeXjnj8PxWyNz8csgUiCdJMRfjkIJyR7bYNiC8kVLdkGO+Cxv7/97W/jk7SfFJ9RUgQCEIBARwQOU4R50mCdddYJXnzxxQarIcvPzo033hgMHDgwcnoxRWw2kSIQgAAEIgLba2eWNGwk/PznP2+3orn88suD/v37Rw2KoF+/foGdlXmqR9plwYIFwTnnnBMf+hcOrbzooovazZo7SyJ+2npI5telSIII7CBb3peGCxuPHz++3QJt1IP2xJizqNt5YrJEgsoJUyAAgeQTcO936OFVQzhaLrnkkkatMtvNl3v0vv/978f/+d8sLoOSX3xYCAEI1IHARrrmB9KwzvDCxfPnzy9ax0ydOjU+fz48x0MLr7766qLrSRVNLAEH7DnwuuuuC9ZYY414nRnsvffeQXtLiLhhduSRR8bP+VgMN69D+XHJEgisoDj3SF1gLXYZ6Ql4zSJXXXVVMGTIkOirq2/U3aQIBCAAgc4Q8Hoxl0nDf4C777578MYbbzRLdRrY41XshcE9fEd2BiLnQAACTUVgtHL7ujSsN73u6yuvvNJuvWknGh49EJ3jrZfcsGfTOXPmtHtuEg7OnTs3+OMf/9hmXSznYc011wzr0fZsfP3118PlmmJ5f0v7a0iRBBPwUMKfSsPxsoMGDWq58MILi/rob+8GSMuxp59+Othyyy3jD+n9yr/XeUAgAAEIdJXAAUpghtSTvVtOOeWUwP9YG1X85XWvvfaK16cvKO+4Fe7qXcT5EGgeAvaM/W9pWI94iGBHDobcG+SGlR1kROd567W3XOd6gd+kiRtJp512Wps1sWzz8ssvH05fcU9Ve3LttdfamV08v5N0/opSJCUEVpedd0nDQlxvvfWCBx98sL0yT92xTz75JDjiiCPia7m8p/zaC5YbmwgEIACBShHwaIErpGGP+YgRI4KbbropdXVmewZ7mOAvfvGLoE+fPtGoAM+3OEHaS4pAAAIQKIdAT0U+QxrVJ8GBBx4Y2BlGe+Khhp7LFPdOqDTC99hNNtkkbMBMmzatvSSqesw+EM4///xgs802izeQwv1VVlkl7NnqyImSe+k8rDLKVyujc7SlrhWENMqeMvoNaViodpbhISFpFnun+fGPf+yJlNED7N4736RLSREIQAAC1SLgdWPsXCesTzfccMNwTL6/xqZVpk+fHngStoZdx//xX608DqsWRNKFAASahsB2ymnoP0DbYNSoUcHf//73DqvLxYsXhx+zCjVounfvHo5i8np+9kfQUeOtw4u1E2H27NnhO/PJJ58cbL311vbwHa8nw/2NN9645P8DXth59OjR8TQ+FBecXjTA49BHeThVGg5/0TZI4wuCvX8ddNBBcW+CvlnvlHqFcgQCEIBALQh010UOk7oHPfyHGX3JTNOQwgIfrJyXx6VbSREIQAAClSLgoYTjpdkGxg477BC8/PLL7TRxvjjkePZiWKiXy2naHfqmm24a/OAHPwjOO++84I477ggmT55clkONhQsXhsMT77zzzrDH6qijjgqXs4i5Ws/a7muuuuqqgRtfL7zwwheGtrPnoY85jtqc3n1SPmgJQiPJQGXmJ9I2LwgeY9rRZMV27p+qHvKXCnug2XnnnX1TRj1Yi7R/nXQDKQIBCECgHgR666KHSidLw3/Cyy67bMuxxx4beA2/JIrnDNx6662B163p1atXVJ/a9rulX5MiEIAABKpBwFM6vi+1o7KwvlQdFBx//PHBzJkzS64un3jiiXBE0wYbbBCu2RWlVWjrRtLQoUPDBprjb7PNNsHXv/71UL3vDofVVlstjFOsQRWl6140T8Fx/d7eYsO5GXGPmHvevJhzlJa2n0qPkvqjHdKgBPyC4C+y2RcE7QcbbbRRcO6559Z94Tivo3DLLbeEbj/tWtm2tepcbS+UriJFIAABCCSBgP9Z7i31ROaorgr/uZ966qklf7XN/Qddqd8egjNhwoTg0EMPDQYPHpy1T7ZGH6w21D4CAQhAoBYEBusif5Qulob10XLLLRf86le/Cjzvvhzxwr8einfCCScEW2yxRa5jiXhdV/b+gAEDwnlYnqbij1MeYl2OFBmS7Tz/VbqstOaC84KaIw8v6BcEf8UcJ91L6h4vS7Duuut2U4s/M3bs2Iy38qLy3yNV+KuvrBl9Ac488MADGTnsyDz88MN26RndE35AHpZeI71R+okUgQAEIJBEApvKqP2l+0qHRgZqTH62LnWdKtfF0aGKb7Vge+bZZ5/N1qeuU/UCE7/Os/pxrdR16tT4AfYhAAEI1IjA+rrOBdLsUGXNu8/ISURGvUaZ4cOHd8qMDz/8MKNheqG+9tprGa2tmlGvUqgaIRVunbCvFVc19jKupzU8MVTNWe3U9eWoI6Phi5m//OUvGV8vJo9p371YT8TCarobvVTX9KJcrA0B93J5Qp5fEnaR9pVmReupZNTjlb0Jo5tR7uOzcTra0RjYzJtvvpl9CPwwaN5V5tFHH/Widrn3wNNKzy8DHiLIy0BHcDkOAQgkiYA/Yn1FGn3EWjpunLwWZjTJO68+LeeDlhtUb7/9dpv6VHMZMo888khmxgxPx20jr+mX61I3rl5qc4QfEIAABOpH4Ju6tKe0bBSZoCGFGQ1vznzve98LP/Rr2F50KJFb9XS5gyBz6aWXZq655pqMOw9i4g9bZ0qvl7rjoG6S+5JdN0O4cEjAja5NpGOl20i/LO0vzZOBAwdmtA5A9suAulsz/fr1y2j4X/YrQvQ1wYsn6+WgUFn75vNaLQ+06oPafiBFIAABCKSdQA9lwF9vXZe6Tt1a6uEzeeIvrK5Toy+trk+9L6+GefXpp59+mvsPPZ7e6/rhetR1qrdvShEIQAACSSVg74QnSLePGzhs2LCw0TVu3LiMvPvFD9V9X2u4ZrQWVua6667LTJ2a1x8wQQaeJbUTkERIoZfvRBiGESGBnvq7gXQt6ZiYjtZ+wQaYwguJx6e+LX01ppO177kNbca26DcCAQhAoBEJ+P+d61IvAhyvT73fpudLv9sTf6B6VxqvT73/uHSaFIEABCCQNgKeM3q81NNZlogb75FUe+65ZzgMe6uttgo/SsWPV3tfTjsyEydODIdly49AxiMIcmShft8iPVvqejhRQkMrUcVRljEeOzhA6gaX1fv9pJ9LZ+fodP32jYhAAAIQgEA+AdefXg8wXp96344rcuvTzxQ2X4pAAAIQaDQC/uhkJ0OezuKRAN2lWfFwQnkBDIcW2o/AWmutlVl55ZUzSyzRpm2WjV/uTjTVRe7bMw899FDoP+CZZ57JyLlQblL+4OVRA57qcpM0sZ0GNLRUOggEIAABCEAAAhCAAAQgkCUwTHv7SfeRelqLR1nliRYTDh0NRT4E7HQod2qLh2Jboikt0da9VW+99VZ2zuuUKVMKNaqia7q19YT0RqnnXr0jTbzQ0Ep8EWEgBCAAAQhAAAIQgAAE6kbALSX7DYjmvNrTa2W6sYpnaYEOuWH1gNS9VxOlbVwK6nfihYZW4osIAyEAAQhAAAIQgAAEIJAYAn1kiZ0NrSaNz3m1DwEPwy5H3Hiyh9bcea/2gj2vnISSGJeGVhJLBZsgAAEIQAACEIAABCCQPgJx/wHuCYt+Oye5c17dyEpdL5UzUqr8f6NYRrZvwvMvAAAAAElFTkSuQmCC" } }, "cell_type": "markdown", "metadata": {}, "source": [ "## The dialogue explained\n", "\n", "

Watch W4E2: The Pumping Lemma.

\n", "\n", "Alice first chooses $s = \\texttt{0}^p \\texttt{1}^p$, which she knows belongs to $B$. Hopefully it will become clear soon why she chooses this particular string.\n", "\n", "Alice knows that Bill's DFA $M$, which supposedly recognizes $B$, has $p$ states. And on reading the first $p$ symbols, this automaton must make $(p+1)$ visits to states: first the start state, then one for each symbol. By the [pigeonhole principle](https://en.wikipedia.org/wiki/Pigeonhole_principle), two of these visits must be to the same state. So when she asks Bill whether this happens, she knows that the answer must be yes.\n", "\n", "Now let $x$ be the part of the string read before the first visit, let $y$ be the part of the string read between the two visits, and let $z$ be the part of the string read after the second visit. Alice knows that $y$ is nonempty because $M$ is a DFA, and $|xy| \\leq p$ because the repeat must occur within the first $p$ symbols. Her choice of $s$, then, guarantees that $y$ consists of one or more $\\texttt{0}$'s and no $\\texttt{1}$'s.\n", "\n", "Here's what the accepting path for $s$ looks like:\n", "![image.png](attachment:image.png)\n", "The dashed line stands for one or more transitions. By going around the loop zero times, we get an accepting path for $xz$; by going around the loop two times, we get accepting path for $xyyz$; and in general, by going around the loop $i$ times, we get an accepting path for $xy^iz$. So all of these strings must be accepted by $M$.\n", "\n", "Alice chooses one of these strings. In this case, the choice doesn't matter too much; she chooses $i=2$. But because $y$ consists of one or more $\\texttt{0}$'s and no $\\texttt{1}$'s, $xyyz$ has more $\\texttt{0}$'s than $\\texttt{1}$'s and therefore does not belong to $B$. \n", "\n", "Since $M$ accepts $xyyz$ but $xyyz \\not\\in B$, $M$ does not recognize $B$." ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "## The dialogue becomes a proof\n", "\n", "Now we distill the dialogue into a proof.\n", "\n", "Claim: The language $B = \\{\\texttt{0}^n \\texttt{1}^n \\mid n \\geq 0\\}$ is not regular.\n", "\n", "Proof: Suppose, for the sake of contradiction, that there is a DFA $M$ that recognizes $B$. Let $p$ be the number of states in $M$. Let $s = \\texttt{0}^p \\texttt{1}^p$, which belongs to $B$, so is accepted by $M$. On reading the first $p$ symbols of $s$, $M$ makes $(p+1)$ visits to states (the start state plus one for each symbol). But $M$ has only $p$ states, so by the pigeonhole principle, it must visit the same state $q$ twice while reading the first $p$ symbols. \n", "\n", "Let $x$ be the string read before the first visit to $q$, let $y$ be the string read between the first two visits to $q$, and let $z$ be the rest of the string. We know that $y$ must be nonempty because $M$ is a DFA, and $y$ must contain only $\\texttt{0}$s, because the repeat visit to $q$ occurred within the first $p$ symbols of $s$.\n", "\n", "So $xyyz$ has more $\\texttt{0}$'s than $\\texttt{1}$'s, so it does not belong to $B$. But $M$ must accept $xyyz$. This contradicts the assumption that $M$ recognizes $B$." ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "## The pumping lemma\n", "\n", "If you were to write more and more of these proofs, however, you would find yourself making the same argument over and over. The pumping lemma is like a boilerplate non-regularity proof that you can use to simplify your proofs.\n", "\n", "The lemma itself goes like this:\n", "\n", "1. For all regular languages $A$,\n", "2. there exists a $p \\geq 1$ such that\n", "3. for all $s \\in A$ such that $|s| \\geq p$,\n", "4. there exist $x, y, z$ such that $s = xyz$, $|y| > 0$, $|xy| \\leq p$ and\n", "5. for all $i \\geq 0$, $x y^i z \\in A$.\n", "\n", "And here is how you use it:\n", "\n", "Claim: The language $B = \\{\\texttt{0}^n \\texttt{1}^n \\mid n \\geq 0\\}$ is not regular.\n", "\n", "Proof: Suppose, for the sake of contradiction, that $B$ is regular. By the pumping lemma for regular languages, there is a $p \\geq 1$ such that any $s \\in B$ such that $|s| \\geq p$ can be written as $s = xyz$, where $|y| > 0$, $|xy| \\leq p$, and for all $i$, $x y^i z \\in B$.\n", "\n", "Let $s = \\texttt{0}^p \\texttt{1}^p$ (line 3). Then the pumping lemma writes $s$ as $xyz$, where $|y| > 0$ and $|xy| \\leq p$ (line 4), which means that $y$ consists of one or more $\\texttt{0}$'s. Let $i=2$. The pumping lemma says (line 5) that $xy^iz \\in B$, but $xy^iz$ contains more $\\texttt{0}$s than $\\texttt{1}$s, which is a contradiction.\n", "\n", "The advantage is that this proof is shorter and doesn't need to make reference to an actual automaton. If you prefer to use the longer form, it's fine with me. But, regardless, you need to understand the argument, and it's critical that you remember which variables you get to choose and which variables you don't get to choose. Your job, as Alice, is to choose $s$ (line 3) and $i$ (line 5), and to produce a contradiction, namely, that $xy^iz$ does not belong to the language. Bill chooses $p$ (line 2) and $xyz$ (line 4); since you don't get to choose them, you must write your argument to work for any values of $p$ and $xyz$." ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "## More practice with the pumping lemma\n", "\n", "**Question.** Prove that $G = \\{ ww^R \\mid w \\in \\{\\mathtt{0},\\mathtt{1}\\}^\\ast\\}$ is not regular.\n", "\n", "**Question.** Prove that $C = \\{w \\in \\{\\mathtt{0}, \\mathtt{1}\\}^\\ast \\mid \\text{$w$ contains an equal number of $\\mathtt{0}$'s and $\\mathtt{1}$'s}\\}$ is not regular." ] }, { "attachments": { "image.png": { "image/png": "iVBORw0KGgoAAAANSUhEUgAAAnIAAABSCAYAAADQHTmKAAAAAXNSR0IArs4c6QAAAJBlWElmTU0AKgAAAAgABgEGAAMAAAABAAIAAAESAAMAAAABAAEAAAEaAAUAAAABAAAAVgEbAAUAAAABAAAAXgEoAAMAAAABAAIAAIdpAAQAAAABAAAAZgAAAAAAAACQAAAAAQAAAJAAAAABAAOgAQADAAAAAQABAACgAgAEAAAAAQAAAnKgAwAEAAAAAQAAAFIAAAAA7jOKIAAAAAlwSFlzAAAWJQAAFiUBSVIk8AAAAgtpVFh0WE1MOmNvbS5hZG9iZS54bXAAAAAAADx4OnhtcG1ldGEgeG1sbnM6eD0iYWRvYmU6bnM6bWV0YS8iIHg6eG1wdGs9IlhNUCBDb3JlIDUuNC4wIj4KICAgPHJkZjpSREYgeG1sbnM6cmRmPSJodHRwOi8vd3d3LnczLm9yZy8xOTk5LzAyLzIyLXJkZi1zeW50YXgtbnMjIj4KICAgICAgPHJkZjpEZXNjcmlwdGlvbiByZGY6YWJvdXQ9IiIKICAgICAgICAgICAgeG1sbnM6dGlmZj0iaHR0cDovL25zLmFkb2JlLmNvbS90aWZmLzEuMC8iPgogICAgICAgICA8dGlmZjpPcmllbnRhdGlvbj4xPC90aWZmOk9yaWVudGF0aW9uPgogICAgICAgICA8dGlmZjpQaG90b21ldHJpY0ludGVycHJldGF0aW9uPjI8L3RpZmY6UGhvdG9tZXRyaWNJbnRlcnByZXRhdGlvbj4KICAgICAgICAgPHRpZmY6UmVzb2x1dGlvblVuaXQ+MjwvdGlmZjpSZXNvbHV0aW9uVW5pdD4KICAgICAgICAgPHRpZmY6Q29tcHJlc3Npb24+NTwvdGlmZjpDb21wcmVzc2lvbj4KICAgICAgPC9yZGY6RGVzY3JpcHRpb24+CiAgIDwvcmRmOlJERj4KPC94OnhtcG1ldGE+Cs+OiooAADFwSURBVHgB7V0J/BVTG542pZKktGpTKYlCaFP25aOP9KEFfSgqpAilT1GWLCURkSSEJCEipM2uCKWNFi2WlKi03vM9z3HP3+l2t7l35t65///7/n7PnbkzZ87yvHPOvGd3HBFhQBgQBoQBYUAYEAaEAWFAGBAGhAFhQBgQBoQBYUAYEAaEAWFAGBAGhAFhQBgQBoQBYUAYEAaEAWFAGBAGhAFhQBgQBoQBYUAYEAaEAWFAGBAGhAFhQBgQBoQBYUAYEAaEAWFAGBAGhAFhQBgQBoQBYUAYEAaEAWFAGBAGhAFhQBgQBoQBYUAYEAaEAWFAGBAGhAFhQBgQBoQBYUAYEAaEAWFAGBAGhAFhQBgQBoQBYUAYEAaEAWFAGBAGhAFhQBgQBoQBYUAYEAaEAWFAGBAGhAFhQBgQBoQBYUAYEAaEAWFAGBAGhAFhQBgQBgoqAych4f2Bx4EhwH4ApQfwNXAZ/7iQcXDL545w8Yw49YYB0aU3PIovwoAwIAyQASlT5T0IPAMDEENl4XecFwJqAVuBP4AKgBtpC8f0c7qbh8Rt2gyILtOmUDwQBoQBYSCPASlT86iQk6AyUB0R2wPQ6FoGPAjcCFCmAbzOFzkV+QQP8fl/p/KwPOOaAdGla8rkAWFAGBAGYjIgZWpMauRGkBi4BZGhsbUZOMSK2LHh61twLG1dd3NKA45+z3PzkLhNmQHRZcrUyYPCgDAgDOzDgJSp+1AiF4LIwDuIFI2tCRGRGxe+/lzEdTd/Oc7ut7A/rdw8KG5TYkB0mRJt8pAwIAwIA1EZkDI1Ki1yMQgMlEMkXg1jG4405BaH/w/E8UBgO8DrZwOR0hwXXgT4DFvsfgHY6sYu2JKALaPxh/68ZF+Uc88YEF16RqV4JAwIA8KAI2WqvAQ5wcDpiCWNq2gYievnWfcOwrkt/8OfaM+ZazNtxzi/POyeXbdFI+7J3/QZEF2mz6H4IAwIA8KAYUDKVMNEjhz9NixKgIe6YdTGsSzA8WbFAbaE/QlsADjJgFgB0CDyW75HAF2BM4H2AFvfrgMonwJdeAKh8bVJn/39cw4Od4b/z8LxAWAJUBG4FfgX0BqoD7C1jsI0UcoATYGP+SfHhANe6wF1AKaVOiR2AmyRJE9MJ3W4FKBuMyWiy+SYZiszdcj8WAPg+0gdFgGoQ2ItsBygDtcDIsKAMOA9A5XgpcmLVXB+AMC8uAdgPuR3cRVgylOuopBJkTI1MdvsebNtG5av1CGHU3GlC+rxZ8DYNtRnTkkzxPYuYA6wA1AusBFuXwN6AzUBv+VRBMD4fRgREP/z+lcR118OX2c3arGIe5XD9/gcW/SM0AgyHPQ1FwN+ZFp6AEwvX0YT/2SOu+CexvB9wMlAYSATIrrcm2W+n+cCbGFeAISAZPRn3LDgeRboAhwEiAgDwkBqDPAjfznwDLASMHksmSPz7TfAIwCXtKKhkCmRMvUfpgvhtDUwFGBjDL9zyejPuPkF7icB1wI03j0Vr1rkqiJW3YGOQC0Tw0KFCqnDDz/cqVu3rlOnTh3n4IMPdkqXLu0UL17c2bZtm/Pnn38669evd5YtW+YsWbLEWbt2LT8YfFmJBwESxpd/PMBWM6/lxLCHNDxsYY2JsuLvQ94vX2waN4sAKtIW4xevrbVurME53fLD6rkCrXDSPeW7cAnwX6ANkGeAVaxY0alfv77WY9WqVbUOqcedO3c6W7ZscTZt2uR8//33Wo/fffddkT179hyP5wkarusAjiccBbCm55cY/gu6LhuDYBrh7YE8Awx5Th1xxBFah7Vq1XLKli2r9VikSBGtQ+bF1atXGx1Sp6yAdA5jJ45vA2OAqQALJxFhQBiIzQA//GcDVwHnAMUBLcx7DRo00HmxevXqTpkyZXReRLmp8+LmzZudH374IS8vbt++/Ug8SPQE2Dr3CsDydD7gp0iZ+rc9w/K0A0A7RwvKTWW+iYcddphTrlw5rcP99tvP2bp1q7Zt1q1bp3W4ePFi56effqqABy8MYwSOs4GngReASFsClzIrdRHcU0Bey1u1atVUnz591Jtvvql+//135UZWrVqlxo8frzp27KhKlixptyD8jDBuAw4AvJL94REJ5Efp4ghP2bTN68MirvNvGeB0gJnqXuA54AuAzeJ85i8gstbE7ireex4ImrD7uxewCmAcFV7GULt27dSYMWMUjGw3KlQw7NT06dNVv379FIx37V/Y3904vgQcBXgtosu/V16nsZXH+dFHH60GDx6s5syZo3bs2JG0HkOhkPrmm2/UI488os444wxVuHBhOy8uRBiXA3mGvtfKFP+EgRxmgPmCFSC2oum8yPxz2mmnqYcfflgtWLBAMX8lK8y3c+fOVUOGDFFNmjTJy9thv9/F8WTADynoZSoN5wkAv1ua99q1a6tbbrlFvfPOOwoV32RVqN0tX75cjR07VrVv316hUm2Xpz/C/z4A+c64lEaIQwFtwPFFvfjii9WsWbNcvaTxmIBVq55//nnVtGlT++Vl686lHqW2Jfwxfte0/GRNyhBN49EIDZ7RQJ5icW6et4+0tCOF3cx0My3yRpb/t0X4bCXT8W/YsKE23twa4PH0+Nlnn6krrrhCFStWzHBKg/cxgDOjvJKCrMvqIJGtxFqHpUqVCrEitWjRonhqcXUPtUk1bNgwhdYD+z2fjzBbeKVA8UcYyAcMsAWLlXqdT9iocf/99yv0OrnKb/Eco3VH3XTTTeqAAw4w5SnDehWoCXgpBbVMZS/GSEB/54sWLRrq0qWL+vjjj+OpxdW9P/74Qxt1jRo1ssvTlQizHZAxOQUhsbtQoes0dOWVVyp0q7lKiFvHM2bMUM2bN7cTPRPhVwPSkZvwMP38OYonv4XvsfnaCGs/Jg4LcP4A0BU4DWBcvgR4/24gUpbgAu+xizEIcjAi8Rqg03PUUUep119/3TMjPJp+0W2ubrjhBsWMEQ53A45evbgFVZdsFd5KPmnA3XnnnQpdotHo9+Tarl27dIt5zZo1TT7gkZWbrNQmEa6IMBAEBljJfxTQZduhhx6qnn76aYWhJ57ku2iesLJ91113KQxxMeUpe4LYs+KVFMQylQ0bvwIKXaeh6667Tv3444/R6PfsGnsuI1paOXSF3bC+SRH4PATQXYgnnHCC+uKLLzxLUCKP2BzNbleM1zIvLo0tEp+qmFaM16N4sAjX+JEyLWgk1oR7RxT37GI29zkewha28G0H6B8t/WzLSYiANsQPPPDA0MiRI9Xu3bsT0e/ZfYyhU+xmQBwMWACyIExHCpouWWucDGgOO3TooNasWeOZjhJ5hPGtauDAgXYXwbeIS8N0FCjPCgM5ykB9xJsVez0k5bbbblPsTcqUYByW6ty5sylLeeT3jBX1dKUglakcvzgC0DyefPLJ6ttvv82UChXGRqrHHntMHXTQQcaGYM8jG8w8l5Lw8U1Aj5e54447dOAZS6kV0K+//qr+9a9/mReXCb85xdSyb5r+2N2nxivT+vZd+ML5Ybd0X8k4Ch9pqHHsG+/RyC0L2FIVf0x8+9k3wufFcFwK9Ixyz+tL/4WHuwDVsmVLhcHtFrOZPaUBybF4jAvwIVAOSFWyrUtOYnkaYAVgGcABrCzg/ZCa8FS38NIQnzRpUmYVZ4XGcXSYQGHe7T8RrzP8SLD4KQwElAF+bP8AOKlPffXVV1buyOzplClTbENgOeJ0WJqcZbtM5aQtfh86p5mORI/zez0L0MN/hg8fnlnFWaGx16pNmzamPN2NOHVLFHk392ndfwyo8uXLh2bPnm0Fnb1Tjj1g1y7jBQwDaFAlK/zwGsLYNRop/8MF3mdzNf1tFv7Pa/cA+wEUGmn8aBu/+PJHSktcMPdbR9wshf+Phe+zKdtPoRGp43HrrbdmtBUu1lvy5Zdfqho1ahhuFiJ+h6ZAQLZ1ydYxds9vA0aHwfdmI1Ad8FKOhmesrenm+JUrV8aiNmPX2fpgtQjsRNw6eZlg8UsYCCgDFyFeOwB1ySWX6EleGct0MQJixdwaU84y6ZgUuct2mcpodwX4bfCzpZ/p/JrhYDxjKJM9jDFUqBvIBgwYYL6JPN4OpC2cJTofUFiyQC1dujRW+Fm5PnHiRHsQPZtGk5V2cEiSaAgeGOUhDlo1ZFbGOVsk9Qc0fH0Ljswoxg0/2jxnixxbLgsDRlij4D12rxYPX6QhyOZ4fvyNH34actqIo+E7atSorOgqVqCshViDPpeDj4qAG8m2LgcgstThBVak24avsULglTSAR3rs5qmnnqo4YDZIwtlciB/BPHUJICIM5FcGLkTCWNbrFRrczEL1O89y1YAzzzzT5MVNiOORKSgh22Uqo8xKMb+z9reU172S8vBoCaB7FfweC+dW708++aS9WsDAdBJNY+M9JrRevXqezrxxm6h47t999127i+7WJBN8J9MFsCssmhTBRWO4mY9SM1zTisfRZJTfcf4wUBfYGr5ON7Y8jj90P826WBTn94XxKI6875chx+5U3Xr54osvxqMya/c4cNeqSc5DfFmBSFayrcsJiOivgN0iTIOdOh0PeCFs+V0FqLZt27paSiSTSr333ntNvtiBuEZr6faCC/FDGMgmA60R+HZAcXJREIWTLC688EKTFzke2m3PQLbLVOqX34HZPAkLW0B57SFzIY0je8I+BXTPxsaNG4OoRvXKK6/Yxly3VNP7FBNaqVKl0IoVKwKZUBMpjhOyullZW/JCTEvLVMszGniHAycBkZmjNK61AioARmgM/wYwU7GVJpqwBYr3/TDkGM9d9D9oLXFGd+bIsY+sMIS5IOe2YYS/aYmfujwVMWMN1pbj8YdpGWxfTPGcE0G+BPS4xr/++stQFsgjl0ZgXIE/AFZwRISB/MJAbSSElXd1/fXXBzL/mUhhEWHFQfuMK/ANsD/gpfhZprIizMrgsHCEr8WRLaCvA+wdS1cmwwPFdeG4tFKQhS1zjCuwG+C3xpV0hGu1//77h7I5gNMNwQ899JBJMJuTa7pKbXTH5XGZY51oCB0S3UnCq+xuY7x+AArHcO2XIcexjayNKY6JywVhhQErZIcYZ6AP4JVkSpeMLw35rwC+N15MeNAttjRy/VxaxKv3g91MXFMSaSfmA2Y4AU5FhIGcZaAYYv4ZoC644AJfl2ryKi9ihwh7MtKTHjPvZ5nalDwDtENYGeb5aKAIkK7QKFTYXSPkdrF7r/Ti1p/bb7/dlKfrEfekbZFacMzatF4c1m2g2XTPDMZ4Ax8BsQwn3Epa2P1J/4Yn/cQ/DtmixKZgPt8FiCV+GXKvIUDdipPJ5UXS1f8bb7xhdLgT8W8Si7QUrmdCl60RrxUAa49XpBDHyEfYiquHDnBiSK4Ix+9Zu3qYWnVk2uS/MJBLDNyLyCquoejlgul+52nOLC9RooSpHLf3mHC/ytTu5BqYGT5OwNELaQRPdLc4uy1zRbg8idW6+layRGgD4KKLLsqVdObFk33dXIwRCSW6JZvgOO4OwD1awVR+9Tjuot26BBcZj/ej3bSu+WHIaQOAy1Nkc4mRPMW4PGG3RZi7T3D0qovVT12ytv4AwAJzFXAykK6UhAf0S40YMcIlg9l3zhlgXFQT8WeXwNGAiDCQqwxw5uQu7mD0ySefZD9zuYwB1yhD/Im1AIcAeSV+lalPIYKM7zbgN+ALwAuZDU/UNddc45LB7DvneoFWb1VCg/wsJpTbfwS97zgWtRwvxzQAG4ByQLpyPjyYDvzXpUf3hJ+rk+A5rw25Egjve0BxrbZcFO5jV6VKFVOL7JKAPze3/dAlW34nA3znHgM4kNYL0V0Kxx57bNbWbEz33endu7fJiyxARYSBXGWAlXHVs2fPdLNEVp7ncIcTTzzR5MWhHivBjzJ1AeL4O9ASGAIw7o2AdEQPFzvkkENC7HLORRk9erTRISv4rOjHFBKoHnzwwVxMZ16cuTwD0wGwOTzo4rUhdwMSrLjtVi51qeYpL3wyYcIEo0OO89svwEq8nHwDN3oYR46D+AsIebnHXyTHfv9ngcmCE+kgP+cBIsJArjFwJiKsDj744FBQZzcmk4/ZQh6eEMhJBFUCrAROyuD4YjMkowHOWX6Y/zh1LUXxxEpAjRs3Lhm6AumGXays2DMdQF8gqpyNq6pq1aq+7hGXCYa4UTvTAtCqLwMEWbw05PjCrgYUx5p5JRzz9Nxzz2ls2LDBK28T+kNjlGkB3LaG4pGMyYcIieP5rgKuiMDx+J+KDMFD6vzzz0/IUbIOsqVDaxLS3FSIkGeEgSwzMAPhq/vuuy/ZrKbdZSu/xYskh0sxLQDHtgVVmiFijGMHK4Lzcf4zwCEsqUgnPKQaNGiQE5NU4unw7bffNjpchzRFbeD4gIl94IEH4vmTM/eswYE3paL5DD7jpSHXmTps2LChpy/sW2+9ZV6ejE7XpvHI9ACLMqgPN0EVguOtgIln5PF+N56F3bJrdiP99LI1Lls65AKl1h6CzVPgQx4RBrLFwHEIWJUpU8Z1d1y28lu8DzRb5ZgeYDMQ1AaO7uE41sHRCHs7GO9zzQWXR93TOHbs2Hj05My9xo0bGz2y4WAvqYl/qlSpUiHWJPKDTJ061SR24V4pzd9/9FiOMWPGeKrCQYMGaS6rV6/uqb+JPNu1a5duIea7CZyYv1WXlzo9lqNZs2aJ6HF1P1s6ZCT79etn8uITeamUE2Eg+Aw8giiqG2+80VVeo+Ns5rd4kW3durXJi12CT78nMTyGOqxYsWJgF1KPp69o98aPH290OMcwVDh8opsx0ZVTCBMdzL2cPmKbEqdChQpMwxHAUTmdmOQiXxnO2mAjetW+fcJJLcn5GHb1+eef67Pjj0+1p9BVcHmOixYt6mAfQ/Pfbmo31/LjUacT+5d6mrZs6ZCJuPTSS01a+GJG7Q4wDuQoDASEgaKIx0WMi/X+Jh21bOa3eJG0ypUCVZ6iW9nBtzEeNTlzr127dg7W+KUx1wKobkd8Hv4otmLlJ+nRo4exXDkDML9LTyRQQcmeqJArg3NdPo7TKl26tOaRLXL8n8np2/PmzTM65NT5/C6sRe3ksh3c6SJdCYoOmY6jjz7a6JEz40WEgaAzcAoiqMdVJZsPg5TfYsWZEzaKFSvGCUhcFuigoCvBg/itgB+eDlOJxW0mr6OBw5SnvQ1HZXGyB9ZqiC9ifpI333zTJDavCdIkOsvHegi/msdxeBn+ebaIM9dLon/RwE2ZMynYJs7Eg7wFRdia3RrgODmvRC//07x5c0/oDZIO+/fvb3Q41CuyxB9hIMwAeyMaeMyGXv6HW84lK0HKb/Hi3KZNG5MX23rMWbrenQQP2BLqldSER5xx7OmY8XjcZuqe1b36Gsnix6glj1hnplDx4sV5Ld9IixYtHEy55kvLPkGurxYUYW2Pa8FMBzgman8gXWEmcDAGIl1/9PM1atRwsM+bg82X9X8shulgHRt9beDAgZ6EkawnJ52kk0bneSfJPuujuyLweybANftISE0gXdHKs9Kbln9B0qH1XgZJh2nxKw8HhgFW8Dgh6lOgO+BFS5Pr8jRI+Q0cxBSrfPHmYxEzJNc3nsYT7HkZBngxHErrsFWrVrQDXEcmyA9Y5WkrxFMn7g6c6AHJflmTc+bMUX369FEYY8XFhvWxe/fuas2aNerTTz/V3XXssvNjooXVpXNCgBRzDTm3sBnnHAjeHEhFauAhPaDTax1Sb/T7yCOP9NrrpP3jzgaMAzAaCIpwKryJF48h4APgcoAzT1OR9/CQ50McgqBDLvKMtJGjHQCNYBFhwCsGWsMjvl8G3InnJeBsIJV3jR9GPRs9lbXjgpDf4hWu06dPNzzNRjqDJKwUm7jxOB+4HigPpCJ6ssr9998fj4607y1cuFDbMP/5z390yx/XqqOtg52VFLtA/ZJq1aoZruqSnAmAYlOdH8LlTNCaYwLc60jjgDOCGD5nlfgh1gbenZnYgEikIWfzsgRx7A+46Xo9De4VrHTPKWzZsqWO2xVXXOG538l6aBU8HwREf4xGNEPO6PFP3H8aaA24qQqugnu1fPnyZKlJyl0QdMiIWtvn1UI6RYQBrxhgPjN5j0dWGMz/dTgfCjQAkpWqcJjyNyko+S1W4cBtG5k+YH2yhGTInW3I2TrcifAnA20BN12v78C95xXjSF5HjRql+aQ9M2DAAMOtPvq5ucLpp59uwjqHXavamqtbVx/w1zu5/fbbHYwxcLBFiINNtB0squhgsV5nxowZTtu2bZ1vv/3WQUJ1gE2bNvUuYMsnK13eJ9AKx8NTdhPcBfCjPh3oCOwPxBNfdIidIZz581kpQt90hmes2om1dFjHvh6wc9tg436GXYCZQLJdr+z6PxQzdbkxN069kaDokKlhGRCWXMmLJr5yzC0G7LxYGVG/GXDT9ZpyeRqk/BZLZWjJ4axH3q4EsKwKitAwMWLrkMbbBQDHg60FhgFHAYkkZT0m8ti+b2Yof/fdd86QIUMcLOPmYEKgc/fddzv//ve/baeenlvfxbokiAvSOtjRwdNAYPVrw42eNmnSxHnnnXfMciA6HAy4dE455RRn5syZ+v8JJ/jT82mlS6dTB5YbP3yRTw/jDxxfAsYBHwGRcggvWGmNvJ/Sfxra27Zt089m05Cz0pVrOiR3tYBBwEBgFjAOmASw68YWrpVTCBM7HMxata+ndR4UHTIR/ICEJRf1aOIux9xkgEbC8WEMx5FGwTiAleU9gC36/bTKHfte3PMg5bdYEeV4scqVKzs//PADnTCtW2K5Dch126jjt653GF/iOA6YAGwAIsWX72JkIMaQwxZazmmnnea88MILTvnyqfYGR/oe+7/1fh7CFjltkWOJidhPpHDnzjvvdHbs2KHXbnnttdf2MuLoHV8ma40w31p8rHXxvE1gCpy4fMR+ecvg2a7Ah0C0rle9+J+VVpdBRXfO1lNKiRIlnEaNGkV3lIGrmC7vhCfiFENwuTwjpw3iPw74CXgaaA0YPev3M7/qEOl0rDIm1/Iioy+S2wyYfMZU7AdcBLwF/AgMBRoARvT7ab2v5nrCY1DKzEQRtcqZXM2LNMybACOAdcBkoC3AxikKbZuSnOxYsmTc/eW141R/tm7d6ixatEg/Xr9+fWfy5MkZMeIYoKXDA3wz5LAnmE7c5Zdf7mBsjD6P/LEX6POraxVLqphg9X5r+MMXINt4zEQqhWM9PHMXsAowXa809HSTLo9eiSmU2KLKxXmzKRiXYIKnQrOtP4a/00QoyaP9IWHh2QWYCZiu1zo4z9c6xNp4TCJlFLAZaMk/UeRMXGMrAXkWd/8QJLz8w4V95nZcjp0Xo3W9snXcrnjYYcU9D1KZGS+imzZtMre/wkkQylPG4TATqSSOtg75cboAeA1YCwwD+E4UQjcnbDnbKa56KBx6xKFjlP/973+2ceVhKNG9YhduWErRkNMfpJ073X6XjB/7HjH71Fm7lnxic7Rzz93XQfjKihUr9Bn7erEfY0x36dzgmIUCIJ7rkJyZQikZI7tXr14Od9PwS0xm8cv/APirX1RsS+ZpVBLpkN0B9957r4O163SFC3sUOy+/zCUJvZcCkhe9J058zDQDOhOm8k1MlN+YkHr16qU8dorlA59/9NFH0+KE+T6fS8o6dMOL6VblmEOzVJeb59Nxa72fO2nJsuZbCptbe9YasGzZsrz41apVK+888mTatGn6kp/jr9gtF5axOF5p/mT5yFmrqbbKLcWzzwDjgTUApSF/qEMvZfHixdq73377zWHG53g5qzlX32NL2aRJk5wnnnjCt+5XhgEjgDU2ShHAnOsLWfrhi+Wm9sM4m6ohFTUJGAfMBnivNuBgmQ4ePJNEOmSL+fPPP6+N8A4dOjivvPKKw+1snnrqKQczlT2LBz3CwpzGv6tw8pT5E+XI2WbJdPmIuyjk4VJB4+Xz6DTEvGrnxfVw9SwwDvgOoFzKn1TK00T57ffff3cwK93p2LEjg3Al7Mbj5EF+X//66y9Xz0Y6tspxdin/XdBHOsr8/+UIMtlWOVuHrARPBcYB7C43rTe7YOwUo/Fr2QG47Z0YQw57Y5vhP955nsAn6/3cUhhu2XXhWE2tCR5PfNt6SRzLatzrQdZcvvjiC33NT0POShcnDOSS8EU1wrg/CbQADgfuBowRh1NHp81KK6+lLVgHR/vBDz3HqJ111ll7+XnDDTfoQbP88Ftd2Hu58eLP5s36FaURRCvH5sUL7zPpx0wE1gWoBPwXmAWY9GRch/zoTJgwwaEBx6EQnFWOLdEcLAXkPPTQQ4iat2K9n1qh3vouvgkDcRkw+YyOWAGbCJwDHArcAhgjDqepfxMTlZnMX6yYHnfccQwnKeE3FOuh6nHmjz/+eFLPJHJk5cVc+y6apPF7wMkOvYAqQDvgdcAYcThNXY98OBkxhhw2VEjGuaduLB1upiG3gr6zluCV1KxZ0+FOABROdIgURqBr1655l/005L7//nsTjp6iY/7kwJEFz7tAJ4Af/m7AR0A00Wmz0hrNjetr99xzj2MKJrbIsTCxhf8vu+wyp2/fvnpGol9jEax06XfVjkMOnDPOg4DawMnAM8BWIFI24MKfzBtWBo104/p/PB1yujw/KlddxQayv6Vs2bJ64pHdqm7upXu0yphc1GO6yZfns8sAP/ycvdUD4Li4i4FpwB4gUvT7ab2vkfdj/o+X3/iQabwww1VWrlypV2/gCg6//PJLVH/5LeWwlWuvvdbB/uFR3bi5yJacn3/+mY9sB9giGXRRVgRJ0nCAH6NjgIcBlp3RROvR+n5Ec5PyNSwW7Ri//Vp1I17kTNhwo9M5Eidq2LBhKNO9k3POOYfkc8aImjhxol7xmN1js2fPVki0vsf7aPJUfu7xiunAJqyzEV5QhF2rJl6RxyW41x+o5iKyjemfH7svoFlarV+/XoP6iyXY9kWvZh3rfjrXMZ3bcOTP4C0XRFtOi5FzCxzxav6z5fBpoDXAD0iyMh8O9W4n6fAV+WwsHeJDpcaOHavs1evptnbt2urwww+P9Cat/xjjqMsCpg/Qk3OSJUXcCQMJGGA+43tlYOfFdbg+FGAXYrKyPxyG8G0KoQLr+r2Pld/oUfv27RVX5KcsWLBAYRkQhWUk1Ndff62vJfr56aefdBrT2a3gyy+/NDx9mywhGXLHVhcTN1uHbEGdDLQFigLJyvNwqJ555plEtKZ0H0uqmbjq72NKnqTx0DHHHGPCP56k6LmzZuHXZBlK5G7w4MHOe++9p8dVseuNLTtsseEYAVvYquPXHq/gyMFLa4JbaE4CePwDcXoJGAfEanXDrZiyFHd2o4WlCMZRcKZOTIdub3C2Ktc2y6awOyIsf8/zNv+Cd5yJKI0DJgHRWt1wOa7wHW3C9HrZSh1Lh4cddphDGGF+Yesq15diy4KXsmTJErMm4Vr4y/ddRBjwiwF++NkVNA6YDkRrdcPlmPIX7qyEQVaL68IdddRRMR1GuxErv9EtW+TYrYoGDb0oPtcC47CGWCs7RPM/3WtWeRrkbyIrwPx4jwMmALFa3XArpujvBdPLniOvxXSrVq9ePePfSA5lwrtpDLnF7P+cwwTOmjXL03TCWnQ+/PBDp0GDvytCHOdEI46LgsJCdho3ZiOSvzsGYA80hwP1IavD4HlQhDWOZLtOE8V5GxzMR+2x0Mcff5zIbc7dt95N/a4GLAErEJ9BQKKu02SirdPHQj7Twq4WrkLOsXHY99jB1nmeRiHgOvQ0reJZ1hj4DCGz7zFR12kyEfT8u7hhwwaHXalc0YFdpRyAP3fu3DwjDttk6nGqHKtq4MdMb6t8CWJ56qbrNJEePdehHSBaUfXfbHSrco4Bxk7S2GUkdMWYf2jter7Ho2k1hDGl8MKqNWvW6EtoNVKotWhrkhvM+iXWZuvPIn1BknqIjJuu02Tifj8cqX79+vlFZ1x//epahfGvsNMBjV7Wsr1rakyG0fhuWAlqDTD/eCX14ZFCC6geihCXcA9vTpkyRWElcoV1HRW2mFGpdCclio615zGHFYgIA14yQMPNTddpMmFfAUfqggsuSPRqJ30fLW+mBUV3r6KHSmGcU97zGJ+ad59hY5Z33j1z4kXXqrXnsbumxmRYS8/NSXjcTddpotCKw8F28ByCEW0ozBfHgQMHmndlhE3Cc/ijsDdYRhI5Z84cEwmFVZF9C7NFixYmnA52YvPp+cnUIfaz9I3PeB77ZchxDBfTBbyXT/UWmawfmF5sXRePbs/uoRVAYTC14ngLtGB75q/tEStuGCtLY5yoCYgIA0FnoCoiuAfDfkJYF9V+nVM+ZyUJfiosHKu++uqrvHPjIRs8bLASGynpGnIfffSRKU9/RFy8rIQGVZ9vkXPM9o2kMqf/o6fT6PFMm/hzmFg/BstHY+vBBx/UkShTpoxvLQ+rVq1iGPxwcM2uILXkIDq+CFuIOP5Iodk1Gu2+XvPLkLMmq7CGXBDkLiRSXX311b7qi56jO1VhqSDVunVrhXWpfAvPmqzyYUFQoKQx3zDwAfOiV4PlMWQhb6IDM1vDhg0Vxle5agFP15C77rrrjAHAHpyCIJ2RSF3G+VbAZdhjUwlAutgNXYRK5MefwrFaGziwExa7vuDnz6effqq956BPv5asGD16NMNgjYODXlMZeM7nc0lotL7ICHu11lC2E8/p/++//z4Lnh0AZy0VBOHAXq7vprhDip/CzZ25ADEnHHE9ObR+5oELA3sl4bxI73TavPJX/BEGfGZAv6/W+5tWcJzoYJYdoUedOnVyVq9e7cyYMSMtf5N9mAsKP/vssyxPKQUlL05BWrdhjK7ickv5QazvOydI7jOR505cVG3btvXdvuzevbs6/fTTfWvuxMdJYbwBDRu+tJlfqQ+BZkkOQ7i7OW0eA2p916MdAFvksCiifSnt827dupna4xNZ4jNbwb6PgNXQoUPT5jCeB5jJZfjd58hxNF4IKm3G701I0wHZIlTCFQZSYKAkntHjxzkcKB3BPsM6H9jDlzDxQXGcHPNhspJOi9zw4cNNXpyTAhe5/MgjiLzq0qVLsjQH1h17Udjdj/QQh0dTSgVc5OzHENe3yWXB3pHmhZ0VLaH5/BqtdIVdF3JZherHH3/k4Hu+rKxx1MvnOotM3hm4wEkPISzemdN6ZMWQaQHujkyk/BcGcoCBQYijwq42OZ0Psb2i7tZlWoBzgYIktZDY3ZhgGcL+7jmtx5tvvtmUp6/GU+Bw3Mzp/mQuXlu6dGnTGndavMTm03tHI117+NKiKTlnX1prluML+VRPiZL1CRxkbRayFy/O9OnTTaHDPuKKiRIs94WBADJwMOLExU/V1KlTvcgWWfHDmuU4H2kpCJMcIl+lZ6hDL2chZ1qR2G2HGyiY1rhjIxNo/y+LPxxApzhAORelc+fO5uMR12K1E50Pzx+jDjlRIBcFY0aMDjm28dB8qJ9kknQ8HIXYKrl06dKcU+OOHTtU/fr1jR5vSibB4kYYCCgDvRAvvSKAn5OC/MrkWODbdMcxP7YIKMd+R4tL1LBCqbgjQy6K2S0LaXgqGbI4O1AddNBBIXZv5ZK8/PLL5sPBlbnZnFpQhbVIPbZj5MiRuaRChX1GVY0aNYwe+xdUBYbTzQyrtz7D4o85pcfevXsbHXKEcbECrkdJfm4zwLXNvgFUz549cyofcruw5s2bm7z4bG6rIe3Ys0KpqlSpknPrymHCjdHhJqThkGSZeIMJbtWqlYq3v2aQ3mj2fWMbMNOl2iPZhOZjd+2oQ7bocG+9XJF27dqZF5Zdi14uDpmLqj4QkV5BPd500025okLdBcU4A1zEuSkgIgzkOgNNkABuMq8mT56cM3mxf//+pjxdjbiXy3UlpBl/LtXBiR7qvPPOyxkdciuuEiVKGNvmEjcclIfjNUzwNddcE/gEc+HERo0amRfWu3UT3DAWTLejqEO2cGV6FmsqL82gQYOMDjkmpWYwKc14rDjrehcQ8mo9q1R0k+wz33zzjV2hujHjbEmAwoB/DFwHr7n2Yk5UjsPrN9IA2A209I+WnPKZQ3V+AxSN3KALZyljP2zzXXwyFaab4yHOYlV33HFHYNPLMQtc+oLxBBYCHOcn8jcDJXDgIqwKGz+raCuFB0WxXHmb8QRY6BS0WVVIclzpibt6q7K33norKCrbJx5chLty5cqm5jgRcS6Ig6rjKlJu5jwDzyMFqmLFiiF7e619MkOWL7z77rtmYDzL1N45z7q3CeBuCKwcqyAPPeKOIk2aNDHfRS6+y+VwUpK2eIofVjV48OAsv5r7Bs/14rgeHeMH/AgU1IHxSHpMYXM6DVyFxSgV1zMKmtCI4354jCNwJSCyLwN34ZJuYg/i7DnOqKpdu7bJizMQ1+L7JkGuCAM5zwDHe04HdE/H4sWLg1acKu7pGt4Sj/mxoOzg4PbFugwPhPjdCaIxx63amjVrZsrTJYgre0nTki54WhtzPXr0cLWdiJ9vOBfGO/bYY01C1yOOR6SVyvz9MA3c5YCqV6+eCtJaOlZ3KnXZN3+rIe3U6a7yIkWKhLgHbVAEK9arChUqGEOcNccyaadUPBAGgstAaURN93RgY/sQF70OinDnBi49hfixPB0DSKs4SIghN+C65uq2224LigoVdvtQ1l6qKxDHmjHi7/ry+XiCM0HVKaecotatW5fVRM+ePVtVrVrVvKzLEK/arlNU8B6oiCTPA1S5cuVCb7zxRlZ1yNmp1sQGVhSkJS65d1LvwEI9cgbd9u3bs6rHJ5980h6IOw3xKgj7GienKXGVnxnYH4nTkwK50v6oUaOymg+53A8XgUecDO7Jz+R7mLbL4JfuZuXi5WwJy6ZMmzZNlS9f3tg2CxA3LpviqbSEbz8BOqApU6ZkPL38aHFhw8KFC5uEzkV8kp6K6ykbuenZAYj2VEBn9uuvv16xezrTwnXiavyzxAgnNsiYOHfvUzc41zPosE+q4ibKmZZffvlFXXTRReajweMTQEGfZexOi+I61xkoggQ8Cuh8wIopB6dnWjjB6JhjjjF5kTPFOaZWJHkGzoLTjYBuIOL4wkwL9sFVffr0oQ6NbfM2zrlqgS/CVp13AP3SnH322WrJkiUZSTPHBdWpU8e8rHsQhyEAM5KIOwbY1N4HYIbXa+pwg/ZMCNcltHZsoC65xEhNQMQ9A1wOgWMndMWGrXMbN270XY1cl2rEiBH2zNQ/EIcO7qMvTwgD+YaB/yAlrJDqGa3Dhg1TzCd+Cyev9erVS0+CYtgAh88cB4i4Z6A6HmHDkLYxLrzwQsXJW5mQl156SXFv63DYbB28BfC9S5wBXAtwYTr9EnXq1En5sT9rKBRSr776qj3oj4nlwownASLpMUBDgIaUfoE4q/W5557zpQDiQPhu3bqZvVMZ3lagPyAtOCAhDeFYneGA7hrgsgjci8+PoQ/cq/GRRx5RtWrVMgUOj28CMqwBJIgUeAZqgIHXAJ0/2OPw8MMPK7a0eC1s9evXr59dmeLQlIcBGZsKEtIQfo9oRP0J6Fm/V111lfJjQgvX5+XyMNasVL43nwMZN8QrINDRgP6I4KhatmypOFaA3S7pyMKFC9WAAQPsWXBM5K9AL0A+/iDBI6FR3gVYA+gCCGMP1Y033qjmzZuXjgr1UicckM9ZxdaMVLakvgDI7GKQ4KE0hF95LeXcj497Ck6cOFHRAEtV9uzZo2bNmqWuvvpqvdMLwtDvCI6LAekOBwkiwkAEA2fj/0JA55WyZcuGunbtqj744IO0Jgpyma1JkyYpthRxkXfjP47vAY0AEe8YqAqvngX4vdLfr1NPPVWNGTNG7zyUannK57g4f9++fe0WOL4n64CrgMJASuJF8x0/yuyqY0TYQuDgw60wdqcQ1ndzsOSFU7duXQfdog4G2fMenWiBVepgk3sHLTYOumidjz76yMGHw0EXnHHC40pgGPAUwHXtRLxnYD942QnoCzQw3leqVMmhDlu0aOFgFo3WIww9B4aCceLg3XQ2b97sYE0lrUcYgFqH8+fPZ8FllL0DD4wHHgCW5j0sJ14zwNrczUA7QA87QKGvTjzxRJ0XGzdurHWIVjUHrXd7hY3B0g5mS2kdoiLlzJ0715kzZ46DSSm2O85IHQqw5YEfExFhQBjYlwGWe20B5sXm5jaMOgeNHQ52THIaNmyo82L16tUdrNpvnOjjli1bHOyPqvPi119/rcvTTz75RCGPmvKUeW8KwLz4mX5IfvxgoA48vQm4HNBKwvh8jkfU5elxxx2ndYgFex3q1rZt0LXuoGdE6xAtero8xSRNbe9YEV2Cc34TaTTyGxkIKYVYdASmAnogNo6mBm+OoVKlSnHWJGe6mWvRjmx9ewJoA6RspeJZEfcMnIhHRgBrgWi64QbMWoelS5fmfbt2aLvfiXusLV4JlAVEMsdAJQTF1uuPAV2rxNHWDcfVqTJlyrCljV0Ie92LcLsM/+8CjgREhAFhwB0DXBZrMLAUiJrPmP+YD5kfsbRQVDd4luUsK1K9gSqASOYYOBBBdQGmA/yuRdNRiN9D2jb8PsZww+vrgZFAc8AzMRa+Zx6GPSqO4wnASQA/AHWB2gAJscNk3/4GgB8LgstjzAZM0zRORbLIQD2ETR02BXhOPXKWcDHACF/OLcAPAHW4CJgD0IjYCohklwEa0S3DqI8jdVgDYMXLFhZQbOKnDpcCHD/JvLgaEBEGhIH0GagGL1oDrCyb8rQKzvm9tGUb/qwCmBcXAx8CLFP3ah7Hf5HMM8DdFZoBrQAOaWGrHW0bdnFE2jY/4xp1SHwBsDylPj0XO2DPPY/iIcMjEXxx+bJuB0RyjwHqj4YAP/401mjMieQWA4UR3dJAEYCG+C5ARBgQBjLPACvGzItsPWd5yqNIbjFA24bfxP0A6jAwXaWIi4gwIAwIA8KAMCAMCAPCQFAZ+D/qqJWJSxd5AAAAAABJRU5ErkJggg==" } }, "cell_type": "markdown", "metadata": {}, "source": [ "# Thursday\n", "\n", "

Reread Section 1.4, paying closer attention this time to pages 80-82.

\n", "

Watch W4E3: Proving Nonregularity Using Closure Properties

\n", "\n", "Today we look at non-regularity proofs that use closure properties. We've learned a number of closure properties: union, concatenation, Kleene star, reversal. But the two closure properties that are especially useful are intersection and string homomorphism.\n", "\n", "## Intersection\n", "\n", "Example 1.74 mentions an alternative proof strategy that involves the fact that regular languages are closed under intersection (footnote 3 of this chapter). This is an extremely common technique that lets you filter out strings that you don't want to deal with.\n", "\n", "To show: Prove that $C = \\{w \\in \\{\\mathtt{0}, \\mathtt{1}\\}^\\ast \\mid \\text{$w$ contains an equal number of $\\mathtt{0}$'s and $\\mathtt{1}$'s}\\}$ is not regular.\n", "\n", "Proof: Suppose that $C$ is regular. Because regular languages are closed under intersection, we can form the language $C \\cap \\texttt{0}^\\ast \\texttt{1}^\\ast$, which must also be regular. But this language is none other than $B$, which we know is not regular. This is a contradiction.\n", "\n", "As another example, let's prove that C (the programming language) is not regular. This is a big, messy language. The idea is to focus on one aspect of it, like curly braces. Suppose that C is regular. Then intersect C with the regular expression\n", "$$\\texttt{void main(void)}\\texttt{\\{}^\\ast\\texttt{\\}}^\\ast$$\n", "The only valid C programs that match this are of the form\n", "$$\\texttt{void main(void)}\\texttt{\\{}^n\\texttt{\\}}^n$$\n", "for $n \\geq 1$. So now our job is to show that this simpler language (call it $C'$) is not regular. This is much easier -- but the $\\texttt{void main(void)}$ is a nuisance. The proof goes like this:\n", "\n", "The pumping lemma for regular languages says that there is a $p \\geq 1$ such that any $s$ where $|s| \\geq p$ can be written as $s = xyz$ where $|y| > 0$, $|xy| \\leq p$ and $xy^iz \\in C'$ for all $i$. \n", "Let $$s = \\texttt{void main(void)}\\texttt{\\{}^p\\texttt{\\}}^p$$\n", "Note that because $|xy| \\leq p$, $y$ cannot contain any $\\texttt{\\}}$ symbols.\n", "- Case 1: $y$ consists of only $\\{$ symbols. Then let $i=2$. But $xyyz$ must have more $\\{$ symbols than $\\}$ symbols, so it does not belong to $C'$, which is a contradiction.\n", "- Case 2: $y$ contains something other than $\\{$. Then let $i=0$. But $xz$ does not belong to $C'$ because -- because obviously, right?\n", "\n", "You might be able to get away with that Case 2, but a much cleaner way of dealing with this is to use the next closure property.\n", "\n", "## String homomorphisms\n", "\n", "Another commonly used property is closure under string homomorphisms (Exercise 1.66). Remember that we defined a string homomorphism in HW1 to be a mapping from strings to strings with the properties\n", "\\begin{align*}\n", "f(\\varepsilon) &= \\epsilon \\\\\n", "f(uv) &= f(u) f(v).\n", "\\end{align*}\n", "and we showed that we can think of a string homomorphism in terms of what it does to individual symbols. For example, if $\\Sigma = \\{\\mathtt{a}, \\mathtt{b}\\}$ we can define a string homomorphism $f(\\mathtt{a}) = \\mathtt{a}, f(\\mathtt{b}) = \\varepsilon$. Extended to strings, what $f$ does is to delete all the $\\mathtt{b}$'s from a string. \n", "\n", "Regular languages are closed under string homomorphisms. That is, if $L$ is a regular language and $f$ is a string homomorphism, then\n", "$$f(L) = \\{f(w) \\mid w \\in L\\}$$\n", "is also a regular language.\n", "\n", "Proof: Let $\\alpha$ be a regular expression that describes $L$. Extend $f$ to regular expressions as follows:\n", "\\begin{align*}\n", "f(\\emptyset) &= \\emptyset \\\\\n", "f(\\alpha \\cup \\beta) &= f(\\alpha) \\cup f(\\beta) \\\\\n", "f(\\alpha^\\ast) &= f(\\alpha)^\\ast\n", "\\end{align*}\n", "Then $f(\\alpha)$ is a regular expression that describes $f(L)$.\n", "\n", "Another proof: Let $N$ be a NFA that recognizes $L$. We construct a new NFA $N'$ as follows. For each transition $q \\xrightarrow{a} r$, let $k = |f(a)|$. If $k=0$, replace this transition with $q \\xrightarrow{\\varepsilon} r$. Otherwise, replace it with a chain of $k$ transitions:\n", "![image.png](attachment:image.png)\n", "where $t_1, \\ldots, t_{k-1}$ are fresh states that aren't used anywhere else. Then $N'$ recognizes $f(L)$.\n", "\n", "This closure property lets you filter out symbols that you don't want to deal with. It also lets you conflate symbols that you don't need to distinguish. For our C-language example above, we could prove that $C'$ is not regular as follows:\n", "\n", "Define a string homomorphism\n", "\\begin{align*}\n", "f(\\texttt{\\{}) &= \\texttt{0} \\\\\n", "f(\\texttt{\\}}) &= \\texttt{1} \\\\\n", "f(a) &= \\varepsilon \\qquad a \\not\\in \\{ \\texttt{0}, \\texttt{1} \\}\n", "\\end{align*}\n", "\n", "Then $f(C') = \\{ \\texttt{0}^n \\texttt{1}^n \\mid n \\geq 1 \\}$. But this is just $B$ (or close enough), which we know is not regular. This is a contradiction." ] } ], "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 }