From c5674d4ddad07f10a2d00988a0f4f3af240ba382 Mon Sep 17 00:00:00 2001
From: dgelessus <dgelessus@users.noreply.github.com>
Date: Fri, 4 Jun 2021 14:32:51 +0200
Subject: [PATCH] Add initial version of ABZ 2021 slides
---
notebooks/presentations/ABZ 2021.ipynb | 1563 +++++++++++++++++++++
notebooks/presentations/img/prob_logo.png | Bin 0 -> 44553 bytes
2 files changed, 1563 insertions(+)
create mode 100644 notebooks/presentations/ABZ 2021.ipynb
create mode 100644 notebooks/presentations/img/prob_logo.png
diff --git a/notebooks/presentations/ABZ 2021.ipynb b/notebooks/presentations/ABZ 2021.ipynb
new file mode 100644
index 0000000..558d784
--- /dev/null
+++ b/notebooks/presentations/ABZ 2021.ipynb
@@ -0,0 +1,1563 @@
+{
+ "cells": [
+ {
+ "cell_type": "markdown",
+ "metadata": {
+ "slideshow": {
+ "slide_type": "slide"
+ }
+ },
+ "source": [
+ "# ProB and Jupyter for Logic, Set Theory, Theoretical Computer Science and Formal Methods\n",
+ "\n",
+ "### David Geleßus, Michael Leuschel\n",
+ "### ABZ 2021\n",
+ "\n",
+ "### https://gitlab.cs.uni-duesseldorf.de/general/stups/prob2-jupyter-kernel\n",
+ "\n",
+ ""
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {
+ "slideshow": {
+ "slide_type": "slide"
+ }
+ },
+ "source": [
+ "# Intro: Notebooks, Jupyter"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {
+ "slideshow": {
+ "slide_type": "subslide"
+ }
+ },
+ "source": [
+ "## What is a Notebook?\n",
+ "\n",
+ "* Document containing text and executable code blocks\n",
+ "* Code can be executed interactively\n",
+ "* Results are shown in the notebook below the corresponding code\n",
+ "* Similar to a REPL (read-eval-print-loop), with some differences:\n",
+ " * Code blocks can be edited and executed out-of-order\n",
+ " * Results can contain rich text and graphics\n",
+ " * Notebooks are saved as a file\n",
+ " * Code can be re-executed later\n",
+ " * Can be shared with other users\n",
+ "* Implementations: Mathematica, Maple, Jupyter, others"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {
+ "slideshow": {
+ "slide_type": "subslide"
+ }
+ },
+ "source": [
+ "## Jupyter Notebook\n",
+ "\n",
+ "* Browser-based notebook interface\n",
+ "* Open-source and cross-platform\n",
+ "* Originated in the Python community, implemented in Python\n",
+ "* Jupyter notebooks can also use languages other than Python\n",
+ "* Strict separation between frontend and kernel:\n",
+ " * The generic **frontend** implements e.g. the user interface and file format\n",
+ " * A language-specific **kernel** allows the frontend to use the language\n",
+ "* Language-neutral interface between frontend and kernel\n",
+ " * Kernels can be implemented in (nearly) any language - no Python code necessary"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {
+ "slideshow": {
+ "slide_type": "subslide"
+ }
+ },
+ "source": [
+ "## ProB (https://prob.hhu.de/w/)\n",
+ "\n",
+ "* Animation, verification and visualisation tool for formal specifications\n",
+ "* Based on a solver for predicate logic, set theory with relations, functions, and arithmetic\n",
+ "* Supports mainly B specifications (classical B, Event-B)\n",
+ "* Also understands some other formalisms, e.g. TLA<sup>+</sup> and Z\n",
+ "* Core of ProB implemented in SICStus Prolog\n",
+ "* High-level Java API available\n",
+ "* Jupyter kernel written in Java based on this API"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {
+ "slideshow": {
+ "slide_type": "slide"
+ }
+ },
+ "source": [
+ "# Features"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {
+ "slideshow": {
+ "slide_type": "subslide"
+ }
+ },
+ "source": [
+ "## Evaluating Formulas\n",
+ "\n",
+ "Evaluating B expressions and solving predicates:"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 1,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$3$"
+ ],
+ "text/plain": [
+ "3"
+ ]
+ },
+ "execution_count": 1,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "1 + 2"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 2,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\mathit{TRUE}$\n",
+ "\n",
+ "**Solution:**\n",
+ "* $\\mathit{x} = 2$"
+ ],
+ "text/plain": [
+ "TRUE\n",
+ "\n",
+ "Solution:\n",
+ "\tx = 2"
+ ]
+ },
+ "execution_count": 2,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "1 + x = 3"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 3,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\{1,2,3,4,5,10,11,12,13,14,15\\}$"
+ ],
+ "text/plain": [
+ "{1,2,3,4,5,10,11,12,13,14,15}"
+ ]
+ },
+ "execution_count": 3,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "1..5 \\/ 10..15"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "Example: Set of all prime numbers < 500"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 4,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\{2,3,5,7,11,13,17,19,23,29,31,37,41,43,47,53,59,61,67,71,73,79,83,89,97,101,103,107,109,113,127,131,137,139,149,151,157,163,167,173,179,181,191,193,197,199,211,223,227,229,233,239,241,251,257,263,269,271,277,281,283,293,307,311,313,317,331,337,347,349,353,359,367,373,379,383,389,397,401,409,419,421,431,433,439,443,449,457,461,463,467,479,487,491,499\\}$"
+ ],
+ "text/plain": [
+ "{2,3,5,7,11,13,17,19,23,29,31,37,41,43,47,53,59,61,67,71,73,79,83,89,97,101,103,107,109,113,127,131,137,139,149,151,157,163,167,173,179,181,191,193,197,199,211,223,227,229,233,239,241,251,257,263,269,271,277,281,283,293,307,311,313,317,331,337,347,349,353,359,367,373,379,383,389,397,401,409,419,421,431,433,439,443,449,457,461,463,467,479,487,491,499}"
+ ]
+ },
+ "execution_count": 4,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "{x | x > 1 & x < 500 & not(#y.(y > 1 & y < x & x mod y = 0))}"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "Outputs are rendered as $\\LaTeX$ formulas:"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 5,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/latex": [
+ "$\\mathit{x} > 1 \\wedge \\mathit{x} < 500 \\wedge \\neg (\\exists \\mathit{y}\\cdot (\\mathit{y} > 1 \\wedge \\mathit{y} < \\mathit{x} \\wedge \\mathit{x} \\mod \\mathit{y} = 0))$"
+ ],
+ "text/plain": [
+ "x > 1 ∧ x < 500 ∧ ¬(∃y·(y > 1 ∧ y < x ∧ x mod y = 0))"
+ ]
+ },
+ "execution_count": 5,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":prettyprint x > 1 & x < 500 & not(#y.(y > 1 & y < x & x mod y = 0))"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {
+ "slideshow": {
+ "slide_type": "subslide"
+ }
+ },
+ "source": [
+ "Unicode symbols can also be used in inputs:"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 6,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\{2,3,5,7,11,13,17,19,23,29,31,37,41,43,47,53,59,61,67,71,73,79,83,89,97,101,103,107,109,113,127,131,137,139,149,151,157,163,167,173,179,181,191,193,197,199,211,223,227,229,233,239,241,251,257,263,269,271,277,281,283,293,307,311,313,317,331,337,347,349,353,359,367,373,379,383,389,397,401,409,419,421,431,433,439,443,449,457,461,463,467,479,487,491,499\\}$"
+ ],
+ "text/plain": [
+ "{2,3,5,7,11,13,17,19,23,29,31,37,41,43,47,53,59,61,67,71,73,79,83,89,97,101,103,107,109,113,127,131,137,139,149,151,157,163,167,173,179,181,191,193,197,199,211,223,227,229,233,239,241,251,257,263,269,271,277,281,283,293,307,311,313,317,331,337,347,349,353,359,367,373,379,383,389,397,401,409,419,421,431,433,439,443,449,457,461,463,467,479,487,491,499}"
+ ]
+ },
+ "execution_count": 6,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "{x | x>1 ∧ x<500 ∧ ¬(∃y.(y>1 ∧ y<x ∧ x mod y=0))}"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {
+ "slideshow": {
+ "slide_type": "subslide"
+ }
+ },
+ "source": [
+ "Convenient multiline input, with syntax highlighting and code completion"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 7,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\mathit{TRUE}$\n",
+ "\n",
+ "**Solution:**\n",
+ "* $\\mathit{R} = 8$\n",
+ "* $\\mathit{S} = 9$\n",
+ "* $\\mathit{D} = 7$\n",
+ "* $\\mathit{E} = 5$\n",
+ "* $\\mathit{Y} = 2$\n",
+ "* $\\mathit{M} = 1$\n",
+ "* $\\mathit{N} = 6$\n",
+ "* $\\mathit{O} = 0$"
+ ],
+ "text/plain": [
+ "TRUE\n",
+ "\n",
+ "Solution:\n",
+ "\tR = 8\n",
+ "\tS = 9\n",
+ "\tD = 7\n",
+ "\tE = 5\n",
+ "\tY = 2\n",
+ "\tM = 1\n",
+ "\tN = 6\n",
+ "\tO = 0"
+ ]
+ },
+ "execution_count": 7,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "{S, E, N, D, M, O, R, Y} <: 0..9\n",
+ "& S > 0 & M > 0\n",
+ "& card({S, E, N, D, M, O, R, Y}) = 8\n",
+ "&\n",
+ " S*1000 + E*100 + N*10 + D\n",
+ "+ M*1000 + O*100 + R*10 + E\n",
+ "= M*10000 + O*1000 + N*100 + E*10 + Y"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {
+ "slideshow": {
+ "slide_type": "subslide"
+ }
+ },
+ "source": [
+ "Finding all solutions as a set and displaying them as a table using the `:table` command:"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 8,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "|S|E|N|D|M|O|R|Y|\n",
+ "|---|---|---|---|---|---|---|---|\n",
+ "|$9$|$5$|$6$|$7$|$1$|$0$|$8$|$2$|\n"
+ ],
+ "text/plain": [
+ "S\tE\tN\tD\tM\tO\tR\tY\n",
+ "9\t5\t6\t7\t1\t0\t8\t2\n"
+ ]
+ },
+ "execution_count": 8,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":table {S,E,N,D,M,O,R,Y |\n",
+ "\n",
+ "{S, E, N, D, M, O, R, Y} <: 0..9\n",
+ "& S > 0 & M > 0 // <--\n",
+ "& card({S, E, N, D, M, O, R, Y}) = 8\n",
+ "&\n",
+ " S*1000 + E*100 + N*10 + D\n",
+ "+ M*1000 + O*100 + R*10 + E\n",
+ "= M*10000 + O*1000 + N*100 + E*10 + Y\n",
+ "\n",
+ "}"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {
+ "slideshow": {
+ "slide_type": "subslide"
+ }
+ },
+ "source": [
+ "## Visualisation\n",
+ "\n",
+ "In B, sequences are also functions, functions are relations, and relations are sets.\n",
+ "Relations can be displayed visually:"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 9,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\{(2\\mapsto 1),(3\\mapsto 1),(3\\mapsto 2),(4\\mapsto 1),(4\\mapsto 2),(4\\mapsto 3),(5\\mapsto 1),(5\\mapsto 2),(5\\mapsto 3),(5\\mapsto 4)\\}$"
+ ],
+ "text/plain": [
+ "{(2↦1),(3↦1),(3↦2),(4↦1),(4↦2),(4↦3),(5↦1),(5↦2),(5↦3),(5↦4)}"
+ ]
+ },
+ "execution_count": 9,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "{x,y|x:1..5 & y:1..5 & x>y}"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 10,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Preference changed: DOT_ENGINE = circo\n"
+ ]
+ },
+ "execution_count": 10,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":pref DOT_ENGINE=circo"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 11,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "image/svg+xml": [
+ "<?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n",
+ "<!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\"\n",
+ " \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\n",
+ "<!-- Generated by graphviz version 2.40.1 (20161225.0304)\n",
+ " -->\n",
+ "<!-- Title: state Pages: 1 -->\n",
+ "<svg width=\"243pt\" height=\"235pt\"\n",
+ " viewBox=\"0.00 0.00 243.39 234.72\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
+ "<g id=\"graph0\" class=\"graph\" transform=\"scale(1 1) rotate(0) translate(4 230.7203)\">\n",
+ "<title>state</title>\n",
+ "<polygon fill=\"#ffffff\" stroke=\"transparent\" points=\"-4,4 -4,-230.7203 239.3858,-230.7203 239.3858,4 -4,4\"/>\n",
+ "<!-- 5 -->\n",
+ "<g id=\"node1\" class=\"node\">\n",
+ "<title>5</title>\n",
+ "<polygon fill=\"#cdba96\" stroke=\"#cdba96\" points=\"166.1026,-36 112.1026,-36 112.1026,0 166.1026,0 166.1026,-36\"/>\n",
+ "<text text-anchor=\"middle\" x=\"139.1026\" y=\"-14.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">5</text>\n",
+ "</g>\n",
+ "<!-- 4 -->\n",
+ "<g id=\"node2\" class=\"node\">\n",
+ "<title>4</title>\n",
+ "<polygon fill=\"#cdba96\" stroke=\"#cdba96\" points=\"235.3858,-131.3602 181.3858,-131.3602 181.3858,-95.3602 235.3858,-95.3602 235.3858,-131.3602\"/>\n",
+ "<text text-anchor=\"middle\" x=\"208.3858\" y=\"-109.6602\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">4</text>\n",
+ "</g>\n",
+ "<!-- 5->4 -->\n",
+ "<g id=\"edge1\" class=\"edge\">\n",
+ "<title>5->4</title>\n",
+ "<path fill=\"none\" stroke=\"#b22222\" d=\"M152.4611,-36.3864C162.879,-50.7254 177.4897,-70.8353 189.1646,-86.9044\"/>\n",
+ "<polygon fill=\"#b22222\" stroke=\"#b22222\" points=\"186.5938,-89.3207 195.3033,-95.3536 192.257,-85.2062 186.5938,-89.3207\"/>\n",
+ "<text text-anchor=\"middle\" x=\"161.8128\" y=\"-65.4454\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">K5</text>\n",
+ "</g>\n",
+ "<!-- 3 -->\n",
+ "<g id=\"node3\" class=\"node\">\n",
+ "<title>3</title>\n",
+ "<polygon fill=\"#cdba96\" stroke=\"#cdba96\" points=\"54,-190.296 0,-190.296 0,-154.296 54,-154.296 54,-190.296\"/>\n",
+ "<text text-anchor=\"middle\" x=\"27\" y=\"-168.596\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">3</text>\n",
+ "</g>\n",
+ "<!-- 5->3 -->\n",
+ "<g id=\"edge2\" class=\"edge\">\n",
+ "<title>5->3</title>\n",
+ "<path fill=\"none\" stroke=\"#b22222\" d=\"M126.0236,-36.0017C106.3845,-63.0326 69.1556,-114.2737 46.3626,-145.6457\"/>\n",
+ "<polygon fill=\"#b22222\" stroke=\"#b22222\" points=\"43.3895,-143.7832 40.3432,-153.9307 49.0526,-147.8978 43.3895,-143.7832\"/>\n",
+ "<text text-anchor=\"middle\" x=\"77.1931\" y=\"-94.6237\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">K5</text>\n",
+ "</g>\n",
+ "<!-- 2 -->\n",
+ "<g id=\"node4\" class=\"node\">\n",
+ "<title>2</title>\n",
+ "<polygon fill=\"#cdba96\" stroke=\"#cdba96\" points=\"166.1026,-226.7203 112.1026,-226.7203 112.1026,-190.7203 166.1026,-190.7203 166.1026,-226.7203\"/>\n",
+ "<text text-anchor=\"middle\" x=\"139.1026\" y=\"-205.0203\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">2</text>\n",
+ "</g>\n",
+ "<!-- 5->2 -->\n",
+ "<g id=\"edge3\" class=\"edge\">\n",
+ "<title>5->2</title>\n",
+ "<path fill=\"none\" stroke=\"#b22222\" d=\"M139.1026,-36.2871C139.1026,-69.6799 139.1026,-140.734 139.1026,-180.4178\"/>\n",
+ "<polygon fill=\"#b22222\" stroke=\"#b22222\" points=\"135.6027,-180.4886 139.1026,-190.4886 142.6027,-180.4887 135.6027,-180.4886\"/>\n",
+ "<text text-anchor=\"middle\" x=\"130.1026\" y=\"-112.1524\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">K5</text>\n",
+ "</g>\n",
+ "<!-- 1 -->\n",
+ "<g id=\"node5\" class=\"node\">\n",
+ "<title>1</title>\n",
+ "<polygon fill=\"#cdba96\" stroke=\"#cdba96\" points=\"54,-72.4243 0,-72.4243 0,-36.4243 54,-36.4243 54,-72.4243\"/>\n",
+ "<text text-anchor=\"middle\" x=\"27\" y=\"-50.7243\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">1</text>\n",
+ "</g>\n",
+ "<!-- 5->1 -->\n",
+ "<g id=\"edge4\" class=\"edge\">\n",
+ "<title>5->1</title>\n",
+ "<path fill=\"none\" stroke=\"#b22222\" d=\"M111.9657,-26.8173C97.6137,-31.4806 79.779,-37.2754 64.1603,-42.3502\"/>\n",
+ "<polygon fill=\"#b22222\" stroke=\"#b22222\" points=\"62.7045,-39.143 54.2756,-45.562 64.8677,-45.8004 62.7045,-39.143\"/>\n",
+ "<text text-anchor=\"middle\" x=\"79.063\" y=\"-38.3838\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">K5</text>\n",
+ "</g>\n",
+ "<!-- 4->3 -->\n",
+ "<g id=\"edge5\" class=\"edge\">\n",
+ "<title>4->3</title>\n",
+ "<path fill=\"none\" stroke=\"#b22222\" d=\"M181.2305,-122.1835C150.0179,-132.3251 98.6277,-149.0227 63.8291,-160.3295\"/>\n",
+ "<polygon fill=\"#b22222\" stroke=\"#b22222\" points=\"62.4733,-157.0898 54.0443,-163.5088 64.6364,-163.7472 62.4733,-157.0898\"/>\n",
+ "<text text-anchor=\"middle\" x=\"113.5298\" y=\"-145.0565\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">K5</text>\n",
+ "</g>\n",
+ "<!-- 4->2 -->\n",
+ "<g id=\"edge6\" class=\"edge\">\n",
+ "<title>4->2</title>\n",
+ "<path fill=\"none\" stroke=\"#b22222\" d=\"M195.0273,-131.7466C184.6094,-146.0856 169.9987,-166.1955 158.3238,-182.2646\"/>\n",
+ "<polygon fill=\"#b22222\" stroke=\"#b22222\" points=\"155.2315,-180.5663 152.1851,-190.7138 160.8946,-184.6809 155.2315,-180.5663\"/>\n",
+ "<text text-anchor=\"middle\" x=\"167.6756\" y=\"-160.8056\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">K5</text>\n",
+ "</g>\n",
+ "<!-- 4->1 -->\n",
+ "<g id=\"edge7\" class=\"edge\">\n",
+ "<title>4->1</title>\n",
+ "<path fill=\"none\" stroke=\"#b22222\" d=\"M181.2305,-104.5369C150.0179,-94.3953 98.6277,-77.6976 63.8291,-66.3908\"/>\n",
+ "<polygon fill=\"#b22222\" stroke=\"#b22222\" points=\"64.6364,-62.9731 54.0443,-63.2116 62.4733,-69.6305 64.6364,-62.9731\"/>\n",
+ "<text text-anchor=\"middle\" x=\"113.5298\" y=\"-89.2639\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">K5</text>\n",
+ "</g>\n",
+ "<!-- 3->2 -->\n",
+ "<g id=\"edge8\" class=\"edge\">\n",
+ "<title>3->2</title>\n",
+ "<path fill=\"none\" stroke=\"#b22222\" d=\"M54.1369,-181.1133C68.4889,-185.7765 86.3236,-191.5714 101.9423,-196.6462\"/>\n",
+ "<polygon fill=\"#b22222\" stroke=\"#b22222\" points=\"101.2349,-200.0964 111.827,-199.858 103.3981,-193.439 101.2349,-200.0964\"/>\n",
+ "<text text-anchor=\"middle\" x=\"69.0396\" y=\"-192.6798\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">K5</text>\n",
+ "</g>\n",
+ "<!-- 3->1 -->\n",
+ "<g id=\"edge9\" class=\"edge\">\n",
+ "<title>3->1</title>\n",
+ "<path fill=\"none\" stroke=\"#b22222\" d=\"M27,-154.1369C27,-135.157 27,-105.1104 27,-82.9567\"/>\n",
+ "<polygon fill=\"#b22222\" stroke=\"#b22222\" points=\"30.5001,-82.7983 27,-72.7983 23.5001,-82.7983 30.5001,-82.7983\"/>\n",
+ "<text text-anchor=\"middle\" x=\"18\" y=\"-122.3468\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">K5</text>\n",
+ "</g>\n",
+ "<!-- 2->1 -->\n",
+ "<g id=\"edge10\" class=\"edge\">\n",
+ "<title>2->1</title>\n",
+ "<path fill=\"none\" stroke=\"#b22222\" d=\"M126.0236,-190.7187C106.3845,-163.6878 69.1556,-112.4466 46.3626,-81.0746\"/>\n",
+ "<polygon fill=\"#b22222\" stroke=\"#b22222\" points=\"49.0526,-78.8226 40.3432,-72.7896 43.3895,-82.9371 49.0526,-78.8226\"/>\n",
+ "<text text-anchor=\"middle\" x=\"77.1931\" y=\"-139.6966\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">K5</text>\n",
+ "</g>\n",
+ "</g>\n",
+ "</svg>\n"
+ ],
+ "text/plain": [
+ "<Dot visualization: expr_as_graph [(\"K5\",{x,y|x:1..5 & y:1..5 & x>y})]>"
+ ]
+ },
+ "execution_count": 11,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":dot expr_as_graph (\"K5\", {x,y|x:1..5 & y:1..5 & x>y})"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "## Working with Machines"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 12,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Loaded machine: Lift"
+ ]
+ },
+ "execution_count": 12,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "MACHINE Lift\n",
+ "VARIABLES curfloor\n",
+ "INVARIANT curfloor : 1..5\n",
+ "INITIALISATION curfloor := 5\n",
+ "OPERATIONS\n",
+ " up = PRE curfloor < 5 THEN curfloor := curfloor + 1 END;\n",
+ " down = BEGIN curfloor := curfloor - 1 END\n",
+ "END"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 13,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Executed operation: INITIALISATION()"
+ ]
+ },
+ "execution_count": 13,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":init"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "Expressions are evaluated in the current state of the machine."
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 14,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$5$"
+ ],
+ "text/plain": [
+ "5"
+ ]
+ },
+ "execution_count": 14,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "curfloor"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 15,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Executed operation: down()"
+ ]
+ },
+ "execution_count": 15,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":exec down"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 16,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$4$"
+ ],
+ "text/plain": [
+ "4"
+ ]
+ },
+ "execution_count": 16,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "curfloor"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 17,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "0.093 sec, 7 of 8 states processed, 12 transitions"
+ ]
+ },
+ "metadata": {},
+ "output_type": "display_data"
+ },
+ {
+ "data": {
+ "text/plain": [
+ "Model check uncovered an error: Invariant violation found.\n",
+ "Use :trace to view the trace to the error state."
+ ]
+ },
+ "execution_count": 17,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":modelcheck"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 18,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "* -1: Root state\n",
+ "* 0: `INITIALISATION()`\n",
+ "* 1: `down()`\n",
+ "* 2: `down()`\n",
+ "* 3: `down()`\n",
+ "* 4: `down()`\n",
+ "* 5: `down()` **(current)**"
+ ],
+ "text/plain": [
+ "-1: Root state\n",
+ "0: INITIALISATION()\n",
+ "1: down()\n",
+ "2: down()\n",
+ "3: down()\n",
+ "4: down()\n",
+ "5: down() (current)"
+ ]
+ },
+ "execution_count": 18,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":trace"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 19,
+ "metadata": {
+ "scrolled": true
+ },
+ "outputs": [
+ {
+ "data": {
+ "image/svg+xml": [
+ "<?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n",
+ "<!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\"\n",
+ " \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\n",
+ "<!-- Generated by graphviz version 2.40.1 (20161225.0304)\n",
+ " -->\n",
+ "<!-- Title: visited_states Pages: 1 -->\n",
+ "<svg width=\"1148pt\" height=\"90pt\"\n",
+ " viewBox=\"0.00 0.00 1147.93 89.89\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
+ "<g id=\"graph0\" class=\"graph\" transform=\"scale(1 1) rotate(0) translate(4 85.8853)\">\n",
+ "<title>visited_states</title>\n",
+ "<polygon fill=\"#ffffff\" stroke=\"transparent\" points=\"-4,4 -4,-85.8853 1143.9253,-85.8853 1143.9253,4 -4,4\"/>\n",
+ "<!-- root -->\n",
+ "<g id=\"node1\" class=\"node\">\n",
+ "<title>root</title>\n",
+ "<polygon fill=\"none\" stroke=\"#99bf38\" stroke-width=\"2\" points=\"44.3223,-19.9205 88.4675,-51.4205 .177,-51.4205 44.3223,-19.9205\"/>\n",
+ "<text text-anchor=\"middle\" x=\"44.3223\" y=\"-37.8205\" font-family=\"Times,serif\" font-size=\"12.00\" fill=\"#000000\">root</text>\n",
+ "</g>\n",
+ "<!-- 0 -->\n",
+ "<g id=\"node2\" class=\"node\">\n",
+ "<title>0</title>\n",
+ "<polygon fill=\"none\" stroke=\"#99bf38\" stroke-width=\"2\" points=\"233.6445,-58.9205 160.6445,-58.9205 160.6445,-22.9205 233.6445,-22.9205 233.6445,-58.9205\"/>\n",
+ "<text text-anchor=\"middle\" x=\"197.1445\" y=\"-37.8205\" font-family=\"Times,serif\" font-size=\"12.00\" fill=\"#000000\">curfloor = 5</text>\n",
+ "</g>\n",
+ "<!-- root->0 -->\n",
+ "<g id=\"edge1\" class=\"edge\">\n",
+ "<title>root->0</title>\n",
+ "<path fill=\"none\" stroke=\"#000000\" stroke-dasharray=\"1,5\" d=\"M73.7879,-40.9205C95.5141,-40.9205 125.5073,-40.9205 150.4784,-40.9205\"/>\n",
+ "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"150.4791,-44.4206 160.479,-40.9205 150.479,-37.4206 150.4791,-44.4206\"/>\n",
+ "<text text-anchor=\"middle\" x=\"135.1332\" y=\"-31.3205\" font-family=\"Times,serif\" font-size=\"12.00\" fill=\"#000000\">INITIALISATION</text>\n",
+ "</g>\n",
+ "<!-- 1 -->\n",
+ "<g id=\"node3\" class=\"node\">\n",
+ "<title>1</title>\n",
+ "<polygon fill=\"none\" stroke=\"#99bf38\" stroke-width=\"2\" points=\"378.6445,-58.9205 305.6445,-58.9205 305.6445,-22.9205 378.6445,-22.9205 378.6445,-58.9205\"/>\n",
+ "<text text-anchor=\"middle\" x=\"342.1445\" y=\"-37.8205\" font-family=\"Times,serif\" font-size=\"12.00\" fill=\"#000000\">curfloor = 4</text>\n",
+ "</g>\n",
+ "<!-- 0->1 -->\n",
+ "<g id=\"edge2\" class=\"edge\">\n",
+ "<title>0->1</title>\n",
+ "<path fill=\"none\" stroke=\"#006391\" d=\"M203.7517,-59.1114C225.8314,-86.2861 297.3874,-88.6347 328.0192,-66.1572\"/>\n",
+ "<polygon fill=\"#006391\" stroke=\"#006391\" points=\"330.5878,-68.5471 335.4986,-59.1591 325.8052,-63.4356 330.5878,-68.5471\"/>\n",
+ "<text text-anchor=\"middle\" x=\"252.3854\" y=\"-66.0343\" font-family=\"Times,serif\" font-size=\"12.00\" fill=\"#000000\">down</text>\n",
+ "</g>\n",
+ "<!-- 1->0 -->\n",
+ "<g id=\"edge3\" class=\"edge\">\n",
+ "<title>1->0</title>\n",
+ "<path fill=\"none\" stroke=\"#006391\" d=\"M335.5374,-22.7296C313.4576,4.4451 241.9017,6.7937 211.2699,-15.6838\"/>\n",
+ "<polygon fill=\"#006391\" stroke=\"#006391\" points=\"208.7013,-13.2939 203.7905,-22.682 213.4839,-18.4054 208.7013,-13.2939\"/>\n",
+ "<text text-anchor=\"middle\" x=\"266.9036\" y=\"-22.6067\" font-family=\"Times,serif\" font-size=\"12.00\" fill=\"#000000\">up</text>\n",
+ "</g>\n",
+ "<!-- 2 -->\n",
+ "<g id=\"node4\" class=\"node\">\n",
+ "<title>2</title>\n",
+ "<polygon fill=\"none\" stroke=\"#99bf38\" stroke-width=\"2\" points=\"523.6445,-58.9205 450.6445,-58.9205 450.6445,-22.9205 523.6445,-22.9205 523.6445,-58.9205\"/>\n",
+ "<text text-anchor=\"middle\" x=\"487.1445\" y=\"-37.8205\" font-family=\"Times,serif\" font-size=\"12.00\" fill=\"#000000\">curfloor = 3</text>\n",
+ "</g>\n",
+ "<!-- 1->2 -->\n",
+ "<g id=\"edge4\" class=\"edge\">\n",
+ "<title>1->2</title>\n",
+ "<path fill=\"none\" stroke=\"#006391\" d=\"M348.7517,-59.1114C370.8314,-86.2861 442.3874,-88.6347 473.0192,-66.1572\"/>\n",
+ "<polygon fill=\"#006391\" stroke=\"#006391\" points=\"475.5878,-68.5471 480.4986,-59.1591 470.8052,-63.4356 475.5878,-68.5471\"/>\n",
+ "<text text-anchor=\"middle\" x=\"397.3854\" y=\"-66.0343\" font-family=\"Times,serif\" font-size=\"12.00\" fill=\"#000000\">down</text>\n",
+ "</g>\n",
+ "<!-- 2->1 -->\n",
+ "<g id=\"edge5\" class=\"edge\">\n",
+ "<title>2->1</title>\n",
+ "<path fill=\"none\" stroke=\"#006391\" d=\"M480.5374,-22.7296C458.4576,4.4451 386.9017,6.7937 356.2699,-15.6838\"/>\n",
+ "<polygon fill=\"#006391\" stroke=\"#006391\" points=\"353.7013,-13.2939 348.7905,-22.682 358.4839,-18.4054 353.7013,-13.2939\"/>\n",
+ "<text text-anchor=\"middle\" x=\"411.9036\" y=\"-22.6067\" font-family=\"Times,serif\" font-size=\"12.00\" fill=\"#000000\">up</text>\n",
+ "</g>\n",
+ "<!-- 3 -->\n",
+ "<g id=\"node5\" class=\"node\">\n",
+ "<title>3</title>\n",
+ "<polygon fill=\"none\" stroke=\"#99bf38\" stroke-width=\"2\" points=\"668.6445,-58.9205 595.6445,-58.9205 595.6445,-22.9205 668.6445,-22.9205 668.6445,-58.9205\"/>\n",
+ "<text text-anchor=\"middle\" x=\"632.1445\" y=\"-37.8205\" font-family=\"Times,serif\" font-size=\"12.00\" fill=\"#000000\">curfloor = 2</text>\n",
+ "</g>\n",
+ "<!-- 2->3 -->\n",
+ "<g id=\"edge6\" class=\"edge\">\n",
+ "<title>2->3</title>\n",
+ "<path fill=\"none\" stroke=\"#006391\" d=\"M493.7517,-59.1114C515.8314,-86.2861 587.3874,-88.6347 618.0192,-66.1572\"/>\n",
+ "<polygon fill=\"#006391\" stroke=\"#006391\" points=\"620.5878,-68.5471 625.4986,-59.1591 615.8052,-63.4356 620.5878,-68.5471\"/>\n",
+ "<text text-anchor=\"middle\" x=\"542.3854\" y=\"-66.0343\" font-family=\"Times,serif\" font-size=\"12.00\" fill=\"#000000\">down</text>\n",
+ "</g>\n",
+ "<!-- 3->2 -->\n",
+ "<g id=\"edge7\" class=\"edge\">\n",
+ "<title>3->2</title>\n",
+ "<path fill=\"none\" stroke=\"#006391\" d=\"M625.5374,-22.7296C603.4576,4.4451 531.9017,6.7937 501.2699,-15.6838\"/>\n",
+ "<polygon fill=\"#006391\" stroke=\"#006391\" points=\"498.7013,-13.2939 493.7905,-22.682 503.4839,-18.4054 498.7013,-13.2939\"/>\n",
+ "<text text-anchor=\"middle\" x=\"556.9036\" y=\"-22.6067\" font-family=\"Times,serif\" font-size=\"12.00\" fill=\"#000000\">up</text>\n",
+ "</g>\n",
+ "<!-- 4 -->\n",
+ "<g id=\"node6\" class=\"node\">\n",
+ "<title>4</title>\n",
+ "<polygon fill=\"none\" stroke=\"#99bf38\" stroke-width=\"2\" points=\"813.6445,-58.9205 740.6445,-58.9205 740.6445,-22.9205 813.6445,-22.9205 813.6445,-58.9205\"/>\n",
+ "<text text-anchor=\"middle\" x=\"777.1445\" y=\"-37.8205\" font-family=\"Times,serif\" font-size=\"12.00\" fill=\"#000000\">curfloor = 1</text>\n",
+ "</g>\n",
+ "<!-- 3->4 -->\n",
+ "<g id=\"edge8\" class=\"edge\">\n",
+ "<title>3->4</title>\n",
+ "<path fill=\"none\" stroke=\"#006391\" d=\"M638.7517,-59.1114C660.8314,-86.2861 732.3874,-88.6347 763.0192,-66.1572\"/>\n",
+ "<polygon fill=\"#006391\" stroke=\"#006391\" points=\"765.5878,-68.5471 770.4986,-59.1591 760.8052,-63.4356 765.5878,-68.5471\"/>\n",
+ "<text text-anchor=\"middle\" x=\"687.3854\" y=\"-66.0343\" font-family=\"Times,serif\" font-size=\"12.00\" fill=\"#000000\">down</text>\n",
+ "</g>\n",
+ "<!-- 4->3 -->\n",
+ "<g id=\"edge9\" class=\"edge\">\n",
+ "<title>4->3</title>\n",
+ "<path fill=\"none\" stroke=\"#006391\" d=\"M770.5374,-22.7296C748.4576,4.4451 676.9017,6.7937 646.2699,-15.6838\"/>\n",
+ "<polygon fill=\"#006391\" stroke=\"#006391\" points=\"643.7013,-13.2939 638.7905,-22.682 648.4839,-18.4054 643.7013,-13.2939\"/>\n",
+ "<text text-anchor=\"middle\" x=\"701.9036\" y=\"-22.6067\" font-family=\"Times,serif\" font-size=\"12.00\" fill=\"#000000\">up</text>\n",
+ "</g>\n",
+ "<!-- 5 -->\n",
+ "<g id=\"node7\" class=\"node\">\n",
+ "<title>5</title>\n",
+ "<polygon fill=\"#ff3800\" stroke=\"#ff3800\" stroke-width=\"2\" points=\"987.0554,-33.4647 987.0554,-48.3764 958.4863,-58.9205 918.0835,-58.9205 889.5145,-48.3764 889.5145,-33.4647 918.0835,-22.9205 958.4863,-22.9205 987.0554,-33.4647\"/>\n",
+ "<polygon fill=\"none\" stroke=\"#ff3800\" stroke-width=\"2\" points=\"991.066,-30.6798 991.066,-51.1612 959.2046,-62.9205 917.3652,-62.9205 885.5038,-51.1612 885.5038,-30.6798 917.3652,-18.9205 959.2046,-18.9205 991.066,-30.6798\"/>\n",
+ "<text text-anchor=\"middle\" x=\"938.2849\" y=\"-37.8205\" font-family=\"Times,serif\" font-size=\"12.00\" fill=\"#000000\">curfloor = 0</text>\n",
+ "</g>\n",
+ "<!-- 4->5 -->\n",
+ "<g id=\"edge10\" class=\"edge\">\n",
+ "<title>4->5</title>\n",
+ "<path fill=\"none\" stroke=\"#006391\" d=\"M784.4871,-59.1114C807.9991,-85.1504 881.9947,-88.395 918.088,-68.8454\"/>\n",
+ "<polygon fill=\"#006391\" stroke=\"#006391\" points=\"920.403,-71.5093 926.793,-63.0584 916.5276,-65.6799 920.403,-71.5093\"/>\n",
+ "<text text-anchor=\"middle\" x=\"837.7876\" y=\"-67.3784\" font-family=\"Times,serif\" font-size=\"12.00\" fill=\"#000000\">down</text>\n",
+ "</g>\n",
+ "<!-- 5->4 -->\n",
+ "<g id=\"edge11\" class=\"edge\">\n",
+ "<title>5->4</title>\n",
+ "<path fill=\"none\" stroke=\"#006391\" d=\"M926.9538,-18.9161C898.5346,4.7749 824.2191,5.7065 792.1902,-16.1212\"/>\n",
+ "<polygon fill=\"#006391\" stroke=\"#006391\" points=\"789.6384,-13.7 784.351,-22.8812 794.2098,-19.0012 789.6384,-13.7\"/>\n",
+ "<text text-anchor=\"middle\" x=\"853.072\" y=\"-20.9186\" font-family=\"Times,serif\" font-size=\"12.00\" fill=\"#000000\">up</text>\n",
+ "</g>\n",
+ "<!-- 6 -->\n",
+ "<g id=\"node8\" class=\"node\">\n",
+ "<title>6</title>\n",
+ "<polygon fill=\"none\" stroke=\"#f4e3c1\" stroke-width=\"2\" points=\"1139.9253,-58.9205 1062.9253,-58.9205 1062.9253,-22.9205 1139.9253,-22.9205 1139.9253,-58.9205\"/>\n",
+ "<text text-anchor=\"middle\" x=\"1101.4253\" y=\"-37.8205\" font-family=\"Times,serif\" font-size=\"12.00\" fill=\"#000000\">curfloor = -1</text>\n",
+ "</g>\n",
+ "<!-- 5->6 -->\n",
+ "<g id=\"edge12\" class=\"edge\">\n",
+ "<title>5->6</title>\n",
+ "<path fill=\"none\" stroke=\"#006391\" d=\"M991.2519,-40.9205C1010.9682,-40.9205 1033.2372,-40.9205 1052.5683,-40.9205\"/>\n",
+ "<polygon fill=\"#006391\" stroke=\"#006391\" points=\"1052.6745,-44.4206 1062.6744,-40.9205 1052.6744,-37.4206 1052.6745,-44.4206\"/>\n",
+ "<text text-anchor=\"middle\" x=\"1008.4101\" y=\"-44.3205\" font-family=\"Times,serif\" font-size=\"12.00\" fill=\"#000000\">down</text>\n",
+ "</g>\n",
+ "</g>\n",
+ "</svg>\n"
+ ],
+ "text/plain": [
+ "<Dot visualization: state_space []>"
+ ]
+ },
+ "execution_count": 19,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":dot state_space"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {
+ "slideshow": {
+ "slide_type": "slide"
+ }
+ },
+ "source": [
+ "# Applications"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {
+ "slideshow": {
+ "slide_type": "subslide"
+ }
+ },
+ "source": [
+ "## Interactive Usage as a REPL\n",
+ "\n",
+ "* Jupyter Notebook can be used like a REPL\n",
+ "* Advantages: easy multi-line input, rich text output, advanced editor features, saveable"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {
+ "slideshow": {
+ "slide_type": "subslide"
+ }
+ },
+ "source": [
+ "## Interactive Editing of Models\n",
+ "\n",
+ "* Any part of a notebook can be edited and re-executed\n",
+ "* Simplifies testing changes to the code, e.g.:\n",
+ " * Changing the values of constants and preferences\n",
+ " * Adding/removing invariants/guards\n",
+ " * Changing the order of operations\n",
+ "* Notebooks created by other users can be easily edited\n",
+ " * Notebook files are never \"read-only\"\n",
+ " * The same interface is used for viewing and editing notebooks"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {
+ "slideshow": {
+ "slide_type": "subslide"
+ }
+ },
+ "source": [
+ "## Documentation of Models\n",
+ "\n",
+ "* Notebooks can be used to document an existing model\n",
+ "* Animation steps can be used to demonstrate behavior of model in specific cases\n",
+ "* Similar to trace files, but with ability to add inline explanations\n",
+ "* Visualisation features make states easier to understand"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {
+ "slideshow": {
+ "slide_type": "subslide"
+ }
+ },
+ "source": [
+ "## Example: Documentation of ProB Standard Libraries"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "# External Functions\n",
+ "## LibraryStrings\n",
+ "\n",
+ "In pure B there are only two built-in operators on strings: equality $=$ and inequality $\\neq$.\n",
+ "This library provides several string manipulation functions, and assumes that STRINGS are\n",
+ " sequences of unicode characters (in UTF-8 encoding).\n",
+ "You can obtain the definitions below by putting the following into your DEFINITIONS clause:\n",
+ "\n",
+ "`DEFINITIONS \"LibraryStrings.def\"`\n",
+ "\n",
+ "The file `LibraryStrings.def` is bundled with ProB and can be found in the `stdlib` folder.\n",
+ "You can also include the machine `LibraryStrings.mch` instead of the definition file;\n",
+ " the machine defines some of the functions below as proper B functions (i.e., functions\n",
+ " for which you can compute the domain and use constructs such as\n",
+ " relational image)."
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 20,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Loaded machine: Jupyter_LibraryStrings"
+ ]
+ },
+ "execution_count": 20,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "MACHINE Jupyter_LibraryStrings\n",
+ "DEFINITIONS \"LibraryStrings.def\"\n",
+ "END"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "### STRING_LENGTH\n",
+ "\n",
+ "This external function takes a string and returns the length.\n",
+ "\n",
+ "Type: $STRING \\rightarrow INTEGER$."
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 21,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$3$"
+ ],
+ "text/plain": [
+ "3"
+ ]
+ },
+ "execution_count": 21,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "STRING_LENGTH(\"abc\")"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 22,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$0$"
+ ],
+ "text/plain": [
+ "0"
+ ]
+ },
+ "execution_count": 22,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "STRING_LENGTH(\"\")"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "### STRING_SPLIT\n",
+ "\n",
+ "This external function takes two strings and separates the first string\n",
+ " according to the separator specified by the second string.\n",
+ "\n",
+ "Type: $STRING \\times STRING \\rightarrow \\mathit{seq}(STRING) $."
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 23,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\{(1\\mapsto\\text{\"filename\"}),(2\\mapsto\\text{\"ext\"})\\}$"
+ ],
+ "text/plain": [
+ "{(1↦\"filename\"),(2↦\"ext\")}"
+ ]
+ },
+ "execution_count": 23,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "STRING_SPLIT(\"filename.ext\",\".\")"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 24,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\{(1\\mapsto\\text{\"filename.ext\"})\\}$"
+ ],
+ "text/plain": [
+ "{(1↦\"filename.ext\")}"
+ ]
+ },
+ "execution_count": 24,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "STRING_SPLIT(\"filename.ext\",\"/\")"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 25,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\{(1\\mapsto\\text{\"usr\"}),(2\\mapsto\\text{\"local\"}),(3\\mapsto\\text{\"lib\"})\\}$"
+ ],
+ "text/plain": [
+ "{(1↦\"usr\"),(2↦\"local\"),(3↦\"lib\")}"
+ ]
+ },
+ "execution_count": 25,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "STRING_SPLIT(\"usr/local/lib\",\"/\")"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 26,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\{(1\\mapsto\\text{\"\"})\\}$"
+ ],
+ "text/plain": [
+ "{(1↦\"\")}"
+ ]
+ },
+ "execution_count": 26,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "STRING_SPLIT(\"\",\".\")"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {
+ "slideshow": {
+ "slide_type": "subslide"
+ }
+ },
+ "source": [
+ "## Use in Teaching\n",
+ "\n",
+ "* Course materials/lecture notes as notebooks\n",
+ " * Students can execute examples themselves and experiment with the code\n",
+ " * Visualisation of concepts like relations, finite automata\n",
+ " * `nbconvert` renders notebooks to standard formats (HTML, PDF)\n",
+ "* Exercise sheets as notebooks\n",
+ " * An incomplete notebook with exercises is provided\n",
+ " * Students solve the exercises and turn in the finished notebook\n",
+ " * `nbgrader` assists with creating and grading exercises\n",
+ " * Automatic grading sometimes possible"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {
+ "slideshow": {
+ "slide_type": "subslide"
+ }
+ },
+ "source": [
+ "## Example: Course Notes for Theoretical CS"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 27,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Loaded machine: BaseTypes"
+ ]
+ },
+ "execution_count": 27,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "MACHINE BaseTypes\n",
+ "SETS PERSONS = {peter,paul,mary}; COLOURS = {red,green,blue}\n",
+ "END"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {
+ "slideshow": {
+ "slide_type": "subslide"
+ }
+ },
+ "source": [
+ "In mathematics a binary relation over the sets $A$ and $B$ is defined to be\n",
+ " a subset of $A\\times B$.\n",
+ "The Cartesian product $A \\times B$ in turn is defined to be the set of pairs\n",
+ " $a \\mapsto b$ such that $a\\in A$ and $b\\in B$.\n",
+ " For example, we have:"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 28,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\{(\\mathit{peter}\\mapsto\\mathit{red}),(\\mathit{peter}\\mapsto\\mathit{green}),(\\mathit{peter}\\mapsto\\mathit{blue}),(\\mathit{paul}\\mapsto\\mathit{red}),(\\mathit{paul}\\mapsto\\mathit{green}),(\\mathit{paul}\\mapsto\\mathit{blue}),(\\mathit{mary}\\mapsto\\mathit{red}),(\\mathit{mary}\\mapsto\\mathit{green}),(\\mathit{mary}\\mapsto\\mathit{blue})\\}$"
+ ],
+ "text/plain": [
+ "{(peter↦red),(peter↦green),(peter↦blue),(paul↦red),(paul↦green),(paul↦blue),(mary↦red),(mary↦green),(mary↦blue)}"
+ ]
+ },
+ "execution_count": 28,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "PERSONS × COLOURS"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {
+ "slideshow": {
+ "slide_type": "subslide"
+ }
+ },
+ "source": [
+ "A particular relation could be the following one, which is a subset of PERSONS × COLOURS:"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 29,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\{(\\mathit{peter}\\mapsto\\mathit{green}),(\\mathit{peter}\\mapsto\\mathit{blue}),(\\mathit{mary}\\mapsto\\mathit{blue})\\}$"
+ ],
+ "text/plain": [
+ "{(peter↦green),(peter↦blue),(mary↦blue)}"
+ ]
+ },
+ "execution_count": 29,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "{peter|->green,peter|->blue,mary|->blue}"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {
+ "slideshow": {
+ "slide_type": "subslide"
+ }
+ },
+ "source": [
+ "We can visualize this relation graphically as follows:"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 30,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "image/svg+xml": [
+ "<?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n",
+ "<!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\"\n",
+ " \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\n",
+ "<!-- Generated by graphviz version 2.40.1 (20161225.0304)\n",
+ " -->\n",
+ "<!-- Title: state Pages: 1 -->\n",
+ "<svg width=\"440pt\" height=\"44pt\"\n",
+ " viewBox=\"0.00 0.00 440.00 44.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
+ "<g id=\"graph0\" class=\"graph\" transform=\"scale(1 1) rotate(0) translate(4 40)\">\n",
+ "<title>state</title>\n",
+ "<polygon fill=\"#ffffff\" stroke=\"transparent\" points=\"-4,4 -4,-40 436,-40 436,4 -4,4\"/>\n",
+ "<!-- mary -->\n",
+ "<g id=\"node1\" class=\"node\">\n",
+ "<title>mary</title>\n",
+ "<polygon fill=\"#efdf84\" stroke=\"#efdf84\" points=\"54,-36 0,-36 0,0 54,0 54,-36\"/>\n",
+ "<text text-anchor=\"middle\" x=\"27\" y=\"-14.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">mary</text>\n",
+ "</g>\n",
+ "<!-- blue -->\n",
+ "<g id=\"node2\" class=\"node\">\n",
+ "<title>blue</title>\n",
+ "<polygon fill=\"#bdef6b\" stroke=\"#bdef6b\" points=\"180,-36 126,-36 126,0 180,0 180,-36\"/>\n",
+ "<text text-anchor=\"middle\" x=\"153\" y=\"-14.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">blue</text>\n",
+ "</g>\n",
+ "<!-- mary->blue -->\n",
+ "<g id=\"edge1\" class=\"edge\">\n",
+ "<title>mary->blue</title>\n",
+ "<path fill=\"none\" stroke=\"#b22222\" d=\"M54.0302,-18C71.9281,-18 95.6509,-18 115.3839,-18\"/>\n",
+ "<polygon fill=\"#b22222\" stroke=\"#b22222\" points=\"115.5798,-21.5001 125.5798,-18 115.5797,-14.5001 115.5798,-21.5001\"/>\n",
+ "<text text-anchor=\"middle\" x=\"78.707\" y=\"-21.8\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">r1</text>\n",
+ "</g>\n",
+ "<!-- peter -->\n",
+ "<g id=\"node3\" class=\"node\">\n",
+ "<title>peter</title>\n",
+ "<polygon fill=\"#efdf84\" stroke=\"#efdf84\" points=\"306,-36 252,-36 252,0 306,0 306,-36\"/>\n",
+ "<text text-anchor=\"middle\" x=\"279\" y=\"-14.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">peter</text>\n",
+ "</g>\n",
+ "<!-- peter->blue -->\n",
+ "<g id=\"edge2\" class=\"edge\">\n",
+ "<title>peter->blue</title>\n",
+ "<path fill=\"none\" stroke=\"#b22222\" d=\"M251.9698,-18C234.0719,-18 210.3491,-18 190.6161,-18\"/>\n",
+ "<polygon fill=\"#b22222\" stroke=\"#b22222\" points=\"190.4203,-14.5001 180.4202,-18 190.4202,-21.5001 190.4203,-14.5001\"/>\n",
+ "<text text-anchor=\"middle\" x=\"215.293\" y=\"-21.8\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">r1</text>\n",
+ "</g>\n",
+ "<!-- green -->\n",
+ "<g id=\"node4\" class=\"node\">\n",
+ "<title>green</title>\n",
+ "<polygon fill=\"#bdef6b\" stroke=\"#bdef6b\" points=\"432,-36 378,-36 378,0 432,0 432,-36\"/>\n",
+ "<text text-anchor=\"middle\" x=\"405\" y=\"-14.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">green</text>\n",
+ "</g>\n",
+ "<!-- peter->green -->\n",
+ "<g id=\"edge3\" class=\"edge\">\n",
+ "<title>peter->green</title>\n",
+ "<path fill=\"none\" stroke=\"#b22222\" d=\"M306.0302,-18C323.9281,-18 347.6509,-18 367.3839,-18\"/>\n",
+ "<polygon fill=\"#b22222\" stroke=\"#b22222\" points=\"367.5798,-21.5001 377.5798,-18 367.5797,-14.5001 367.5798,-21.5001\"/>\n",
+ "<text text-anchor=\"middle\" x=\"330.707\" y=\"-21.8\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">r1</text>\n",
+ "</g>\n",
+ "</g>\n",
+ "</svg>\n"
+ ],
+ "text/plain": [
+ "<Dot visualization: expr_as_graph [(\"r1\",{(peter,green),(peter,blue),(mary,blue)})]>"
+ ]
+ },
+ "execution_count": 30,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":dot expr_as_graph (\"r1\",{peter|->green,peter|->blue,mary|->blue})"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 31,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "|prj1|prj2|\n",
+ "|---|---|\n",
+ "|$\\mathit{peter}$|$\\mathit{green}$|\n",
+ "|$\\mathit{peter}$|$\\mathit{blue}$|\n",
+ "|$\\mathit{mary}$|$\\mathit{blue}$|\n"
+ ],
+ "text/plain": [
+ "prj1\tprj2\n",
+ "peter\tgreen\n",
+ "peter\tblue\n",
+ "mary\tblue\n"
+ ]
+ },
+ "execution_count": 31,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":table {peter|->green,peter|->blue,mary|->blue}"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {
+ "slideshow": {
+ "slide_type": "subslide"
+ }
+ },
+ "source": [
+ "As in B a relation is a set of pairs, all set operators can be applied to relations.\n",
+ "For example,"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 32,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\{(\\mathit{peter}\\mapsto\\mathit{green}),(\\mathit{peter}\\mapsto\\mathit{blue})\\}$"
+ ],
+ "text/plain": [
+ "{(peter↦green),(peter↦blue)}"
+ ]
+ },
+ "execution_count": 32,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "{peter|->green,peter|->blue,mary|->blue} - {mary|->blue}"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 33,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\{(\\mathit{mary}\\mapsto\\mathit{blue})\\}$"
+ ],
+ "text/plain": [
+ "{(mary↦blue)}"
+ ]
+ },
+ "execution_count": 33,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "{peter|->green,peter|->blue,mary|->blue} /\\ {mary}*COLOURS"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {
+ "slideshow": {
+ "slide_type": "slide"
+ }
+ },
+ "source": [
+ "# Conclusion\n",
+ "\n",
+ "* the B language relatively close to the mathematical notation used when teaching theoretical computer science\n",
+ "* the B language supports functional programming, constraint programming, logical inference and proving\n",
+ "* ProB can be used to evaluate, animate, and visualize B (and other formalisms)\n",
+ "* the new Jupyter kernel allows creating interactive, executable documents\n",
+ "* Jupyter Notebook makes it easy to integrate new languages/tools in notebooks\n",
+ "* the Jupyter ecosystem provides a standard file format and useful tools (`nbconvert`, `nbgrader`, ...)"
+ ]
+ }
+ ],
+ "metadata": {
+ "kernelspec": {
+ "display_name": "ProB 2",
+ "language": "prob",
+ "name": "prob2"
+ },
+ "language_info": {
+ "codemirror_mode": "prob2_jupyter_repl",
+ "file_extension": ".prob",
+ "mimetype": "text/x-prob2-jupyter-repl",
+ "name": "prob"
+ }
+ },
+ "nbformat": 4,
+ "nbformat_minor": 2
+}
diff --git a/notebooks/presentations/img/prob_logo.png b/notebooks/presentations/img/prob_logo.png
new file mode 100644
index 0000000000000000000000000000000000000000..a836e0edd4cc8701cf957306ed2aad433e0657fd
GIT binary patch
literal 44553
zcmeAS@N?(olHy`uVBq!ia0y~yV60$ZU})lCV_;zLd3-sSfq{XsILO_JVcj{ImkbOH
zoCO|{#S9F**Fl)kNn>^e0|Vpf%#etZ2wxwo<osN{#FYG`RK1Ga0tOJUsj#ZZEyztR
zNmQuF&B-gas<2f8tFX!|wgL(3D=C1Llw{i~Mfe6NIOi9oDwyh-=ou*4aVaP$*c7Ft
zSp~VcLA4j9q}eKEl#~=$>Fbx5m+O@q>*W`v>l<2HTIw4Z=^Gj87Nw-=7FXt#Bv$C=
z6)QswftllyTAW;zSx}OhpQivaH!&%{w8U0P31pE13_#tPTL8BxuNdm9<osOyio^na
zLp=k1Y??|k(-6)>(FKx$XaoBSVwX)tZh@6^QEFmIeo;t%evTc;N11uq#mR{UsUUyZ
z=%cGZxYPz@q?LbBW@=tZBFIN}hBo>bVo>!q`XKKjc^~Wwh-i?Dn;n;pJ~$RYF=EFh
zaXK`Dfx&^n)5S5Qg7Hl)dqZsK%>Un)eV^p1w%5^#V`2NfYQZI%9ULpTzlDC^|L9ec
z;<VE1#~x|zUeVE=;CM&W)xl*JQ_zxfCdDO_=biCccK%QO{`Yf=-|zf>_xHWp$qRQD
zPpbSrW&PZ5bKg&?UUy=Kw07f0AqiR%`%em;=v4{t7Sq+5e3)O~TIR&-Yip(DIC~A}
zT-0q$SMxb>@@_f*!n`)O$)7%aD0t@`|10R{!*+Q+cbUQ?0)G~J{?qk%J&9$e`$8X?
z$oW%xce}(aI`Q>-{QTJsyVCYszh1LB;`(7urrh)^1$h!7f!CEU@!vjK!*f@=(OYk4
zipBD+6RLS%-As1TxBjhP|MT>xh%XTzd_$PlD9bi%k6*TN*S&v6HD@(@(&|%oOZrx=
zuYC5O-!NhC980FV(G$1!MEu+t(<gTL!Snqe?^~N~3z3Zv4>py3xUH+JD`wpqp8u|o
zo+V2vJu0;GUm)UhK54$huftAJtugatK5__XJkIFcSaiZGG{Ww<p`V8eyE4ZWhcinp
zBa{<UEZTzjo|HWh(`RB|5aYn#xarP^3jzvl#e4TQ|2=J<cc;qy)r-0%JewU49FpdF
zG3~)a1x9!7!VkgsfBpO6`FPfSyNz2b^GZvf9(lEDR#uqlNnU<_#x*?0<XYt1L{j-T
zz3~$8tW&+k!<%W>d}dY2tS9LbCly7FT>c%@7hApK7xNDeeeurpDZ)w)u1}X8aFbZN
zwqT0mY%9(whV#Efr2oCxzU<<wt!IxjzMi~bS%im#o`QIV&mQ064;n$u4IEFhGX(wz
z+^_u+ySK3TIrH?IKYRD5%jWvWS|79PjeH*+@_FOpviwuLJU#1IWv^PZMq<&Apt!h1
z<AjaBWVcoBN?7{k@%+NtnjH<jlfCrU`76eF{hDmjuzbm{kKR%RPenx!|CRKV=&@V5
zdVRRllueg}y1FwG&gR$0@BdQzm2p@6sqE8-jWk+PI0Lq5{aV}e?4iJ9*6T&@&ht(U
z=i?6xnNn)=?@(LsisyNgHhw*#CUojxi-@?^G!X_j{V0=|Z5e@iFW$<>gp|M7_jzAn
zZ0OH&Utiy?zP(?A!edoA7Ju5x%Mx<q#>*x?@fP2l53i4G;m}+0vhF~jQ;bej@QLHT
zNj_B^FAlG^7txzCfpc5ARK@RZ_j5&8B>pj+`|)-9q9~60$w|x{`t_DeC8qc^<Rs-x
zwUDfx)RuXmTj9mW0EdkAf0-{`ys2nwTf05?#-5+T|En&x&pW&zrg1-`*QBe33diSX
z&0GKfgZO;8`!V$wk9^~No4fXG)cI72qot=fmg(g`S^tz@?U;X_nrL(Dv7LuPb<{TU
z=x$i-Eb`U(UQmDp?@bBr$A=|tnkT<6pVE_a>foi015)S0!rBkdGC%NZOVJLC%SJJ~
z4j&A5RTTNK_Wq(-HoF@%S(x8lV5-w|;?$6x#yVv;4-e0xb-R~r&b~c4de`rNg%{oL
ze?IPd_{HL54BRWyza&_)O-gcz|FTy8{hdqKKAgODYn5=+Z0Y0I!$LzHcPpPvY5BR3
z`_!Qhv9_7do{QIUFXBALpY-!+lc7FS&JUIor%X<@3$#TZP?_L;S-`h&YMbZ6x&`ag
zqve0`@;GrAWt<Li{Fs~&ldY=Qqbiyj6zLp&<4L@-ZhpLruzW|eLQrYJHIdKBsUMP<
z)=vs)`Xecq7Q48fzwG;$_3x!6_9S1vcJB24PyFxeJp?mE7M){yBGRv3Xw>rh!}I^2
zzuzjmU3h41Zti2TXKn1MHQtvUij(geL@`J=Ok4cA=h;iE_GccKV_P!{XJ_=5v*w@T
zSs9iStSct)=;uo@7fET0Q~3#*Hmd{II2cxmU3?fJaCXnJi7mnol~F8Th0i2L*-!2~
zobcjf#*YsT0Tq8XoRN`#v{@}DBJ*Xxkm(j)r9azF=?KW@tjS<+atnwHjGTLWPv+@u
zymMub|39s+zvKA!Gdx?H_G_^!?yG#NU$^h@8Od~W^APXa+_MU4W`~)Zo2@21IC+Zq
ziTR>iHM1CmJdYlAJ+07VZtyGnW0O%}j`Ojt{D%SscP3p9d0;us%e~&G=ijX(0&JUh
zu-GVnoW}4tM>AV4_NsxnBO{~R!zpbi<;B-ISE;zAC!M(bYtC_hzA1ronijk7Tb21x
z(yey!y3<S6ELyXCyT4ify-x?b?Tg;=d#}lU`u^AV{ePZsm6yJL=fm8YmzPhwem%^S
zx7Td$IjO?fg~#WgnKC&t_3Nnv2R9vvwTs|8rg-j`sc7BjEmh18YIhl4<}*CjU~y>M
zcf4JIvHtw|9rNDV`QF~PHoR=UwX53J?JpL1+NQ~HOP=|VaKGxs$)y)QJ=Nep_sqve
z@{+$u#n<rpJ=Zt<HWWNF+xvSEk9>fk1)o{Vg?+s*Vj^2}?rm~4D=n$}`B~oXyAZeF
zrgDvq>WoG^>;L}q&!1~hcc?J*>EYVRw{L4nzsf3VZg#$O^|JEayL+P?&REZ_yuonz
zRqt`D0~yD1J5r_u*yIS!5V^#^*N#8sET>D*Jf1aE6<(ak2#l-|e?CJpFh^rr$AY6=
z3!5$6EGupoNcMC*OSBGf*A(J=7!tzW{8T8nVvAebgp>dFF`iLAt-ZahBsXH)qpP<2
zcfSzUj!`d5xjfI$vF2^p{JP@hmYemZ!sGA8$HzzCyL>x(Tc-E&oVRz>_Rd(h>Eg_3
zvVsQvIVz^M0wRL!md|uGjQW*cM_<m7Im!C)z~hB(KPp><_AGg`Yla$gIQt!z8w#>=
z{kc+0dd(00c%{(v`sAxhWfRW$uzAh%G^clU6@`BL%iPTTW3_}s?V9^LzP@mkxBt%<
z-Y)oLN<;JC>DqO_PQDCQkG*y)Ks#5r_isc|>fGnM7BFnxcUMUCv}-1-oOIF*A-Aff
zZHIT6SUB#Ka#FObl}djov90w<Y4Wi{ttV!sMa)*QH*I^d;YN7T3-j2ydp~V+7CZ4o
zQ`k{R_-?@AXe|Yv#m~aG+o;Ty@Yw0~Fk=Oe*#UQrCh?U*GdJ{JmFVwKO#UpX!ZhPk
z;kGr+I)|8>53hLr@6@STQIR{V&R)0w{_wM1H{&tg+0s{9?l)zB2;i|g`u|Y*daLal
zSN_~lB>8Io9lL#8Vsp#Bl}ekP7AvXJ<9`vvDA6LxyL033BXeJFFuP|L!6E1&eo)<8
zHHgv9m6bzj(Lx2Q^NaUvVtSrfEjaJOvFtiw&)*vuI1&Wjt4cm{OiBt6yb-bT$!aaF
zEsw)PriFiVI%#fhzSZ~5+y6oa`Um{>EYRbfI3<3`^g`S3^7}qE+Zx*b4^dvWWb4+e
zqS4#Ro`tQytr2at>%xgMm*!8LynkOq<)!5XULE)NuCQdOof1FGeCmvraDtjb|L?M@
zh0RsP%@IZ#;yUvR64sxX%F7#)q_}I_vQN<q_L;vH@aLKq#N^gyeBPwmM7;j-s=c$N
zv-Go9u3lEu-fIxEGwm+h%?&G^cU33sa6C9M$l*+y<-Fo$#~<@7zxbOs<;0=W>|ufi
zdsa34G3>nI)RfreBztHQ@3g%ono0uGKUf}Q(6YUue&f<jURHi%1;28YnSGZ(R9LN_
zxwg>Z_@{tW*4I+^J}sQLPA@Yz>)#o1{ofzoHtamhdx=l~pU#R03nkcAN@$(dx*r}K
zs`xhdY-(x1y9n+{qS@D0PI_KqxHWBWkIMAs-m~5%9Uoc5<<GlqD^S{6k<t@#!0^Kn
zh9t*H-O;lR1(vAuR<<Y!YX>Zf*(bnuAjfIZ!f*TwFNb@GN-^_n=-PKLuFe1dkL&*)
zZ_eO&eWCE9#+J159q*X^@^Y=xk8RQ1d8}>LzjL{^Q%_%CGyUv}{JDL%7_XTW#fzz1
z&!6Xgrg{3iJzl36(p?Kzbe?B&aauXKM$S}4TuYbPQz{|t+60@F``(E<GK<&du)6R}
zuwA3jw|UFLx<3yidw(5ch`)IIx_L-!=-%u0wZBg--v4nWcmDCr?oF?I7x901G>>(^
zP4SN^j*C}<KEGTUtmd3~#c?`+_?ot&c<#e%`Q2t02S!d_QZylQ{*o6L9Sv5lvE^{S
zA>5Mr=kzO)P(df1tFdbY?uJWsX;rW$+aEn6VZ|qXCqeXX`k7O=4_H2Q{-;<MG^_D)
zYM?~e)sRo3GMBX3P8B^(-CBBeKI^~S^m&!b-c4`avS?okYrg0qcm4f)7H(RU)c<Q%
zR%Xr${nxjyDQn++xxJ)ulBk*IGYxs>m!AZeL>>tdd>p)wA@Dcn#>*k89GSIG=BlMP
znoLhAjh2gald$xel>BgBC&vMgvzvsC+zyDu3aKkI&c2_(Z=Sj#J3i8{uw7eAJ9_o$
zEPkg;`R8{1tJ>z*q-rU%)@G9Jt~L9XJ$ul0D=X^t(>E_<&fGk(RmNkEo`#69&)?P^
z8*@~etrRZ!zIxHN@M*Vu1eaWr(bJrb8~<2H%6x6$c=$=?R)&m$h`<FsLI3BjIZB%I
z%@~4s8MP{}vA!q_IR0_#!dItGZJKuL)?dd*->&)2=DKRip3V2oS^m$N{ifHiUz58V
z5X|~|%bptEw5;rFxj|3gZ7=uFnR-Fe;A2I6%`aceV+&&vg%2$g)#W*K=&0w+8#nUj
z%*fr%$0Zre@#o3a+073pvp)EDApAFjk&CnXyGJsQU*0^F8M5Ji)4$^fS4g!OESUa1
z(Je4EuJAzmzR!~-R~%1m?b#l}dOk<vwC|-T)2*BKE!-EDd@cW$mh{%k%U5emU)a#r
zed3qT>1>|)2{}14Wex->3JdoLG-?RW@Njs^Rxq>WV}p@`kjfK@Up88=WD}+?_*86p
zS3&wwR90nbo{+G(&1au?Rjpn>5*NEB?|U)Ze&yPgYv;A>TesY#K!pEve%`BBAD2$A
zmrU`0Fipy}^+Dms2RUn|OXSwZHMNUY^)6T^!`<oY)q2T!mZn|%9HpR%PbRE*ByPZB
z5%Qdk<(Lc??|~KeIybgVJTT>|_0j_KCvUlZ4*Nd7on~fwW$P!A81ZixujSoPy0azp
zs2dmOsWSl@|4!GqwG>G9ACq!o=sB=#Vz`2{hJtu|>Eg{#-#_^AWS5z!>U61<E7%Q$
zrCcO5zwz^1`AaNYApY{DsvKXRIOk>Cf+Ted=F|r-{EIG%<tm&>IFh_;&c=;#tF$)w
zv1k@OeOlUFTU*VL7peGIH}v3cH-@0nsW)yuTxYec$tw1_q3&aiqFD#nlst2~=lm*=
z-7E0)(VXCu;(i-^zJ}U4%<|IgIdtVujo74p5i2F@CfbOpiF2ILl;w{|c-Chxv*mzi
zw}Ro($3J{z?e}ilRwZ$KQQOk&=<;>ar)``wVs4$eaG*!`iJ)eLh1&zCq~9-EAK3H-
z=BKGVQ(WUcKYz*sPS@8)#=^}pEfp<MDic&VAIa>s(0LSjz4=A=otmZ393%Q;-f!}L
zxc&6}d#U0}!@?ttH!fQy^<2SqTUoBK&dHUBlK)z7YYge&aOJ3tOJR`uI6>gxXAZXo
zn;2L)W}b-5NabhA33~M9Ov4q&{;k_hJed8s3WbHM#V7QdzGGqCVD2H%=AHPL*(U7e
zriTfCeQvtge45+*`0~%s3;#$sAG^lP6!M|=hW-WL@Sfls<;gmHU%KaX?l%F2WBZv^
zhE0q-l5dZ`*td2$zw~L12@1-stZEU79EUX(o*$I9u~(hawJ*cHXPIiN(i9~|hslzU
zYZ7B)=0rHz_$Rt7e$3+}rt*Aq=VbFlWuB?44vD!3m`wAO_xV{=7PM!w;RXKO`4@Y$
z*J+=hntS+m@PbCMyZw(R9PE^w%H$Nl7w-2nQs<DS3r8(mYl?ANprFWpkrt&%tS7?^
z?0mwuPwrgQFSXUd=lMd@uBjCfpKLxn%v58a@MX)b1=|+N-QFy^>(1u2yVc!U7kLY~
zZhpg9aZe>oYC7XFv1+YO14U*-?w+UIb9+j@^PE^R&FyAwzot?0tBQB3uR0~B_XYA6
z_%Y45tCHVRRU12%Z&`(^!|CJg98Wj>IN7NfvFiMD|H)eOFEE5f6bebLnxXzIh|^W5
zOY6tMgN&bVDJ?hKAhzPp*(woZ>4m9Ge&<@27-(@`ls0y9_@Sfo^3rT~dwr#*w@f*|
zmhy4%nSYI(P^ww!^XS2cyT)vj56xy~imRA%kjo@0m-S|GY$WGXzOrAR*fS5j;xxZF
zalxV`2Fofos+e6`@g-4%P3m+^)P;nP=GE&iWh_0KKIKf4Xy{5V_srfaKd*dFzNFH9
zyjXHxZ6SyL_f6{-=ifQDaPJ1wpJ%jnZY((7Qj_2izh+~V>Kb)^?VGQUsB`^E3uLU5
z_H#ScfA-u(!!yeTk2FY3RhTaR@l>D8mfJa&1rK8~GgcWZWZXV^N_)WqIleN>IT2a8
zYnaz6?vXz5X<KBlVa>|g`YC=AS}N8bn1$l@D|!j^i*LTM{HJ`;jO|aIUwQ6Z#5K=j
z31`)<8DHLNrO71v^R%q_5GJwxNMp;HJ{zyXw#BI)F4|5?y!>kvVpw(xI5IS)33hOp
zvbjw=Ze#RP@PdVN#pXF)^X}Y9in4MtY3+@g%69G9iaXBT=kyO~_z85S_8r{v=^*FU
zj&4@v%tVD_3O)_zgB~<5N>hFjSP&N6RwKl{NF&A2j?waQ;iJ|b<^}_<eMu>tKCdS&
zw=O6WdjEz$ZGEo!{O6pGSIl2a{EbS_GYdc1T=QbmQj^Sy@mu!iG{>>5ZgD8|%;+i4
zm7efYc-GSw%+F5GkyX?Fn;2KvFo}2VSDl>VOFfN^Umc&Wsy(zw^?IO>9s81t8%^f#
zZSKCjO@r<3m)v#B0@V3GabydIhaCJI$MXA>j<n+kaWSFDU@Ps;uPgUtSXjAhDY>jX
zxlYHaZ<<qFOXvCSbKM<Y4_;)?JLDk3p~zRvI_dKR?_PzsN{ie)iVmE0EarQ}q+sT@
zZt1JcZjO+u1<amX4?NywZT(MS{)*zs-s+y6mVV6TPYz7xI>^0@yJJepjxSSe1V1Uo
z#4fwcaeGHU&yNRZ=Qbs=zg;50KHq8K!ZQaq-f6qg{5GO*^Bq0a+r<t){&i`UuTB5<
zK7-SE{h8#RxBwP2+Y_>{C#{{J$Izvy{Nm#0JwFRL4L!ZZ8E0%d(p~?8x&8gt#WI`D
z+pIi#I{NUp6U#3~7Vgw&Jk73Yxxdv}J|p+pRGl4(>|9r8FuwUYF-PE{Rrm8Ih54HO
zh6?ldeGZ=cN`bj6>Up1gV|pNKe`~q%sl|!~OVouoyD+cfSyAjSeMC89fz_PjMzT$;
z`wj`{buZh{^wj96UXP@~i5HyG8DcCNhjkL<dc36nRcJ1LoXT!+N^-W-3VGXo(M*|J
z114x{m0dGl-t=ZuB5(UXr<7)$G)8rwhJcQ&jaxK~RXL|*<OH$2+_kGDqNlh|L`L*`
ziB``;78!l51`eCPb=5)^OI|0Py{s(a%MiYJ&PJyGsz(dtm^H*&7+>gA%-y<i-$(r^
z$4*R9cT`yQdB^he0)>?wdbXwq8CC2;*Qtc@-C`>EUwA$?&2i`ThqBA;B=)p!TR2DO
zooCXq^~_AaF6@|Am6^L@qNw!tN3z0lOAC26+sQUPeYm-6Vu5F4maEmqpU1ZrT@!YG
zb6t|B;?4P#f?aCdyVePA2wbtbKSjvS$I)TEqiS&1v7}y0p}>Z+kDpjn!<Y1BFjn!U
zu=pQ$UD<BGa!QxCV;A440P}0SeWw=+X2d2I=-PF1yRKNdR$A`W4K7*#n#(_5ez$DB
zaB`oA-D1&H!8vEtGFBX3-*It^3SVDc&@6d(uR!Mm{<=@}^_Vv<-rV=dV&Wo=X`B;+
zCwx%%Pnc}~Zu^El!KAsxCVB^_PM!KXcS+R!HO0oWvR4;bF5);B-%}E1F+ZtF%vAN%
zBp#tf%nD12-_~mP)#M$Sy+im`w5jKG$;KI1<b0%VdvPUB$xjWPdS=!oHT`w>G<cte
z-r7Ft^DLR!PL=|<D`MVnz3Ax?QFYa{;tIzRp_sshJa@aIdls-6YyL<KSbRt!(CEQ4
z>C?)V)_!+X%3L4K&=m4L71Q9=;53KXK_^_I-fBzoi-S);ZZqgCN{wD*xZ-7y$hrI(
z@?Tj~nD{UB-v9ea^o^qIy{|<}1Pt7?<Vw6v)+DdZ|9wV#lEot4$$?=vCb(Sm;&RCK
zWqEjL-VVh8hN#waVbfVxsHp4|>I`+%k#Ohvw6fsjfu5y7k9@Kx%neMBS*rQNan3Bm
zuQF2kC+|EG>N9vFcwLEIQva0lEP3f8H+Fq$U|zp)=HaVM%$wx6>g2w}N2>NYzG5t!
z!n;=N{=z#&sekscuK0Ya>44?S8BDS4Ga@gmb^IyaDCcltY7fJ<4eD7OB2A{2JsuKW
ziCkRX>+?>Uc7OHDa}}-8*E3qidS155kGb?!pTX2FNqa8Nx0h->1&=Fy7Vf@gv4~~s
zNr!#KFMeuXoMG`ZL(93)jpO*@8pURlsucnee{aStc_gxQLrLdK&WUc5R)|<}Y%Y?B
zeI&)(+q7Vw;q&k2QxDAv5;$zx<2-{)z30Re?-N0VHtizficKe7<Qx96q&xcLsx47>
zQ4KC~ifmEHSkRonw0ENG%$@z`HeArJ>}or;OQe1GsV(;HU(bG%xumgcuLFaA^1ST}
zB%TC_nDIIs<xc%_By?8JZ{Dp_i;g#+Kh5nOKlNtt?UYL`VlyvXQ_=PPx+~`KryK2!
z2}fV?R^31IXJ@eRuYIB-wHa1AKgu5D-?+ARb4!z?%vu-y*<M14oBf;e*8Y3+`ST*K
zc`eM@d~@gXcFoSudVhp<gJkku7wL9(kM-QQ(xYOdihe1qXg2n}Em*kGZp%kuB`tTm
z9{I;QiS~LTW>T}|<lBuCb%kfAsOagGD~V2jdc@^;ySjGCFSgp~N4wr!<1=>Vel>Ha
zPtvPLcP?|W>~Z-ZQW?o~kx?;Bjc1apj@5&SQ=WY^dSNKJx8%9$ZI`1DWonAllAWxI
zDt6_x{4ku)8ZbpdvNgo@6-V2Sh~5jo9#sjlKT`aA!e>U@8TYRT{=NCP<I3Y{IwI!t
zQ+rexbbKz_95Yzy7!=F2k?BHZ%8g~)9?YHlRe$|N_PB`7-CIsA*}Bh7ZM&%l_qC^m
zS2xYezJKSU?&)i}6UFYV|LQNk&C}LA#WG@-Ph(#fQ}ND)8^g+GTYKj1`fr)JX8k#v
z8DhGJB90{;RLEaq{AOB4!2LImk6x{2<Cd!yS@v-O<I2<y_4CtSDWx2+d(~NXD<kSz
zfRo>0jr})j>X}O84~sLX=IS0{5vrTge0fKJg1pM&{SyrIbUPU@=h*By_WZ$2cE8(a
z<=<xh(>_{gaGi0ktbDKSrH9^%Qy8ah`h7Jy>wuDxw_fzO%uiXL-@UMw;6LklWRi^A
zy~zcF5$+27mt0iT-8GgZEOV(|k>}+v*JHNl!RG`I*Jh6=)tXs350`EWy8d9NmY_!Y
z74zTaJ-m^k1$?`v{OnhLUJ!eu+DP-3!JZ>C%y$}Xx%1_kZ_K5mOWXKjiuYz7tvai`
z^yw<G_5atlZQZ|cwfi)kXzkr^cQL#B#QhLTW@>EMaQmF`lYaia9b5CibxWM^Xzt^S
zY-r;?b~4lEUU|a(Ck!lt3PSty!fvE)dhm6}oU)45Paa-Z((u}6@VUZJtc9&0bJeNW
zGMO#Rj1MF|<BT4$<Xn34;n8B1#R~;^K2BRvDbQzk+3~c&VW}e->yN8!=J~9c82aMP
zmt7{w^Sz}1U0C|`#Gxgs?JQTqvubDQv{m*`<ZhC@$^PNk<3v$`o`5q;<E0Fpq)G}L
z6*x0m3K?^I*f!h>&Aj-k==J8vlWeosguHpDA9Q}nld0YZZuFZiO*C~1yC(S{Y3hT|
zVL962POdEr%q}*4(yM({U22vo5H1jqX#epJm&S*gFN_)bE?!|23H$%$WbUTtb54Gm
z{(RbNQTC(P9_dD(E)bEMF!`7?>yzS;a|a)@WeFH7w@24Mzr3N7d#$TrzsW<LoxP$t
zMhhQpYzt+}K5{B#M((BuX;RZCOcR)@RhW2eWkwy-?Zt&{64J8!rgUX<C8S=c(?7~`
zT<>*)Xjyc?{Tt;6fAiPeJXx}3#foW~@@5B*+;9kceY!L5iDb$~jyY<~7R#i%l3Y{#
zoA_87)T0DEFZ?W&EMzkKDWYVkvb=spdRYH9SDBgxA7>ubjc8ciRQSc|{K3N#4;u2)
zp4%}NEpVClVczwAHUHX;hHU44H0dR`)oxSV`{ag!?S1htq6;3``RbZ?1%yVb`S01{
z)py*r>+#1T5xdwl5nIm)vo~&*J$&r?bCmgQHp_fG$8qZUVTo{&#wnVWr3EKLk~T7!
z9h)wBrEt9ikAnS+W1IhoNH-^cs1iA?S-DxU`Akq}MTA?O)>IMk*IzmdG+Q5Ni20>y
zP2IK9qJ8msmozRpMsGfsiF0|>%w~x_uwGyy=JGj#Y0sV)A`0H&!51$q;+uP~EaHCC
zer>KP61Tc;R8=Q&9e@8tPAaObvd<=Y(a%+iFGTqa*}R|Z(O{4MFq2W+@s5+q&93f6
z5!)mcK1Z|)wcD|NYI?H%;G!m%lfvy?k>0_*8#1b*Uc6jhDQq*nJm>zg6AO;bzP5GZ
zu_vZ_6V$gn=jAfs^HZ~nv6;c*Kj(m;q=V~2o~BJ*AGtjyPV#4G+`VI|{HKWP7nSvO
zB3W7c7f;>AmTRbMyY)?Ag7vvsJ*)ZCPQ2~k+q1QzIK}8eU_-eHKSM}j4U765dGP=<
zxiu#~uqfxXyWMArDf}DvN5oh1eoCuFh*Ze^XFfL4qH_hi_Ol+@l%U7lHRIo8hZC+#
zgB4o5m(DSK&T(W>tU$SyM849T#n~1t3O#8DRDairKbKIkmEAY}*<^!@t(-F}r?@-p
ztvSdkpLR^hSJFIr(-x-wmaX@$esYgpe%~T6!lYkmk72|+-Xn{gejGSs6d1T8L&K%(
zSCdtj+wBSSXZ6Op+;Gy6%Y4pz&^dlmL}l(Z_M#(yEPmX~Gvr%b^YNS7ujdS}Y`dd3
zJdoV_V5Q=gcxRJWW#4k2UFE6z@Wk?1<)H(oZJSG$AK8;~tw!_Q%b6xJr-UYJ`WG&H
zXe2lNQzG-U@@qLSUrlvSoGHKIy5GfMqqu)PqVam}@;kb1etapq^W<b14+HyS(cW&Y
zBX|9|1D)qDyS*TccY11xz%@}*jh}&0&DZ_bzqSvUckR&Sx))EKrnl8}cK=Ae$+3`m
z*0IC)LvAo=I~W;mOi*N6BFoNyVwL(S+l&Q0d`x1>T(cT-AKqDPkjx(H;K233@anxb
zzZPzl_JXvq_FX%A6tB9>pUHG-5%acxi4qTUe69POKUUn*I49O+>7<e7c%i9NvAagF
zX_Cishb0DAf9$a^%bGsNWxvBLu45&CK2B^{r|{CgufnRuyHIGhq|}>ojURKO9=5qH
z6pxqT{q9n}?X>ZV{6(AR$ucuNO+E4<VNz3@qubNn9#+f~Ia*|mk9WLOJGb<SFt3Bs
zCs&Q)2gNGFoFC?WH@eyN{+!>jkH;_jMJiOkwUQ3kug+g(RpTA;n~|;AGg$3Jru!Q;
z`#m2O_dJbSoc-g}A@Kv>kN>pZWhU*zchGr$|FVr4^J6ASA5(RiQ`>t=%7*VE%iOzb
zF3;>+?_3@uCOXI7=R=Vow>5`7bL*c@t5fRo&gZ;8eNBjYCXrXSA*H3EWxamW37h_j
z+f?+-nk#20IJx?qo}0gUm8#g)GnIE93%<LjXq;-^Wmhk$JmuQdt;Y-mDjrSojd*=Y
zQMK76DcI3jP-Nc0kQ)t2GMZv(txGMI9a$i(;JhNC?CGLQp4xMjPIB%!bBTvNv9u!1
z<N<Tk7KWcrb0W)JV_z%nTYB7GaADWY>x_$c9G}{GY<EzpznfIO;J3n68#nmtPis-w
zKYL?g@OGK4&wVPNbN=>x{UfbRF2|?f?%^Uo<whgxl>I+HJ$W?s(}nKrg1H4t_2ycb
zbj1ghc~9?eDlptw$#pHKb7OqkVVzxU{&E(R6PFcbxa`{3-L&9f+S3rjDRbR+M0_s^
zI(ArZ--XE`wR<XV95<EJV|nO&`F(KT^2{3(zDx?5RTAhV*J-mpb<%Nd{tFyD7VNW*
zOcVMP^`WRF%&)^(=Q3+gMW|zax_W%fwU<`X!mq6#?NQk4H;scw+FdbR<z}Gj+eHid
z_#1?I8K=+taAvZt=6b&ln+GgS`?mB=JFGoH@VHWEQqUabqaQOSY%clm$l_e@N0lF2
zEb0nw>F!L57W~S$`MP>w&n*7g$6HRAeZJV<yKQ1+MPkdhZ4wbW5=_Ty0x#yCu*=w4
zUiR(e&g1VC)#Y}I-z(Fdo+z{UNXS($nWNu4C)@kUd!&}O&iT9T@6)C7ca&uJ{@vAg
z{wi;p-t5Hm70;w?URo|GiD^5WnzcfE&r>JwbsgHP9-L;=GC0*9wrBRP<Gpi(tixT_
zU9pM$*_^{Nk7F0-j4dfaCpU7sEDAI%TQX_JdBI8jCuARsimLEz^p`AiDd?Gd-{$L!
zI|}cXIR2Ght#d^G#bLeGdT(x|TFCYL-bwk|p)!sA=z`)$GXtVRn#9UkY>sr8w{FmG
z<H#v$5a}um^kLA9QGB3MD6^+pt>fSlmMbhLo@jh?)DkT#{;Zarl&hj_eC=EIxijr-
zY#UE8*TlzZ&k3$}QS`rC@Z_@R`a0jI{e?$Zb=L*HwrG%_bj{GCa)x8)fu7BQJclwl
z{5P9OoC%uY6d|Nid;I>dirP)ZdlGbbS{K+z@6QXKzUT3TpGB7ne+O-x8Enj|uTmUx
zcJfd6N>A%P-?|rToS($kmCU|!Eqqnp1?!)4f3UFUxb$ggPQJ>~&@aOpw(mwXvtx+4
zc}(~0d{@yw7ZSufw$4bEDycZf5&2-3+|o@;I79?*am*4BJ$q22g(*|%Ow$b}nGOdF
z{)xONxve{Fl;pbRPZN6E%<@l1C`e@KNw;SEuH)+x=cNTYsJhwfE??#LSoa<ali-7!
zUB6Ogi?vSJ2Vc)wa;jy4<FX!gj$bJ;8=t0fnbhtG`pdZ4=1^4WtTRhmo=ljkJc;GW
zC8vz%-u{IG_k<5rUXh&W&~mYILts#x#;d1%7RL%pW2U6um+4gItl3e$qetq}rORbY
zf60}y*@dhU^?24D8oMFl_r`-B`|HdmyydC;SD4xVw(kSa_s8qSH`G>q@=pHMvS4q+
zOUFAEch24Dcsj}J!`efW-!5LAAMmk*+h|7WjF>=^BP!1(XZ{kkX719TrRe`F{TJ77
z@7mCvdp2whKNn#Td#~<`lY>(HgyzgfWqs)@jVz4zHxIt#owp;tZu-y7Pn6$V1nm2{
z+5WM2;Ma)$<#{Y3FIL>pv1Xeo_&jG0x6}cJC35~syuz~|i}RYD%Zb^Woz&<%eG%8b
zoCR{J2mH>TN?xAsyvT^roNLyU>Y}SLn!iu<XFA5EC9j;A5Oi)a!^D6+0ZN^jjSMGG
zKAFd-$kT2&J#GHRmJEXg0cWFwhgK?bUFW&!w(a4+9=n_`8!k^>{ARVm-Zh8Km2YbO
zJj5pZbMdw{q2Vz{ttGcP9h}bp`IuGo{T1nZn>(b#*6B5!vD7K@DPWxA+ubhf#Wb@;
zgFW`k%wuXUJ&rCjj$U$7IWO+W(RGyZNKkCa4;?lKK^qC>iM>2WjODb{{>~C^+7*<%
zbIoD)YtC&i_sN;e;L9<3)T+LBPWIDTy|?zS{PN@Lwzw^u<L)fI$J`ptd-&tWbh8eV
z(32;3Z(VG<z}89rgICs%FCzT2Jr<m}5uwTY{?{SP;<z8FEt?iSblj7gZT)oS)459C
z8*X1e{rcU7Hg&TupVd=$_J(d^jSqTt>9UrZyqL9N@Ujpep_{u6=9>yUyvlc>Zd?4m
zUyCm<UAgsSoT|*?jOI7-sWsYNT%u0}C0R~1ecBxFa8kbL0aN7eyv=(af8Ias@wa&g
z_?HzO5UJr8)DN4wxc^aS-Ky(ii_dv<Z;vZ-D0+Hy`RB<tKiT;TN<!W?M^qnoSo60i
zMCV7`_eGQEZhKwCTk5vqPx6#5uMKzYx0SqIY*MsTabw}fipUxLmv*GKf78<H3-L*D
zJ^Qll!l|=&Cv5d8n|n)X@-3;QZ1M^Zz88kCe?MV)SZ)}1MpCk=j(oD?2J6CG>xy?;
z+-G{Ixaa2azS9R|@&!XBAM`)W_<8gZ7wh96CwLAB&Ys^;k<2EtX#3yHlsO@cbv9F{
zw_aqwEX2C)kp%aa1v!~7>TD_`*Y#}=<a+bm@8SxT045u8UfC8udyU!{_j3=#B4<pW
zw(f28=8ewBwr@R=d_M8;hnY(~7*nt8waYYenzVB3(@%G5XFr*=US9k8-p?9)E?V9b
zX%^*oP%b)i{@OXYn;UjI+yA(G^`h$PxLEz|_8*%5JZn_l^kdyrC1a_S<FZnTZ~0em
zI)CO8bBft4gWwkt+kETF|Nc(-_eb`lpuj!h_l!4XHry@Vx@^s+sIc`lp-~?;_D9`G
z7Ownx@~PO1D~Bz4+S2#@Rrnd1-#@4L+SE%M&R6j4N!`S2^!eY9Dv5N{i0{i6rSD&R
z_*bp1-LF{g{d`Ov>)ZBoF*o@wx^TX<vy(MNbiY<T%g*qod!6+bn&w%@Rc=n0AeeWe
zK;+?zLyHoPC1TSxH(i)gpee)Sw#sH>inHW?Ms9wE4)3L5DhpYd5>_WKJwES<XJcSa
zv$omy6OruiRgTMUaY#$J+t2Izym3W)T*Mde@O6`Czpo6c`}{yi=I0?-4~J*JcHZN*
zkNLAk=cncKS2JI4`r)%&t9tsj+VefBLQ|X{+_c+Pd803HmQ4@;<)%iRp01#hClcMC
zf}S7G+|yZ>sV2Gq&wBnp4l8F!wbxyh6gd@la-rOUgC7M;Y}eazq&l7El@Gq2UAWWb
zQva6R9}>mt`-9obugCt;eRoED?u5va=Ug04N1eT|r%rvlV(qS&X?L~;?kl_L`RROp
zy_kN1<Ks{3uj!s!F5nU!J#|ZOJ|o8|2ku0Vb2YyoetP;f+8{YX>H7Uo4S!zTt{0sd
zr(68o<kYV?o)m$e3z4#)x9zER_;zQnFP~*Xc#42}`;Be6KPU0A`$gSN4V_W6;QgKd
z2ZW0rw1%I0I^V*{uIk~+S$-AQroZoSkFuDe_ulTaMCM=T#dChFlkYyWYJ%n3tDD$D
z52eo5-Lq5JJGyzt1E2GoHW!?fKV{$U*uWehyXMcVS6ZR}dL<YvBtjnSO186P`0!3f
zbhC^&|4g>W-IHGE?{ab0iJi5vJa)yT^tKrejF0ug7(PB(lsNnSrIP_OR2p^M*QZU&
z6hEM=Wy0toYBHswr#aIzP>bPW#_?;mx+1#Ai$eaLT5J1>fB9SW_ck9HF7LXrQ%2`g
zNOzk-{XL(V_UW^Ha`w8f`|)?N(c-0H=J$VW^wV28_1Ol7_G72qR$q3}u09}iWX^t*
zU6Ko#A2q7W3Z`bLO)9(*@pE#Mo8USB?#E9zdxffsU9~x*|JvuI@`{)n(kCx&vvt}S
zv$gs4r|SmSmTr8~<{0I_#i24dvbcA4`K;p1mc)B?9@!gaFSBw_xYBRc^KWXzzZHjz
zH!y8BzsIxUo!)PqZwnS4n0~Y8p;^PMqbz)GGBWc*7yLf8%`VfvXiv<KcaInJY^Z4u
zzr8ZU?KE%lPu7`6xm-mX*6b)T<ZL^$<mB6;FN)Qt+V9o&)O??1f5P;BrN=RO3%{t1
z)AsGl_t5&YN=G3;{>8bx6;qDa?GMWP_qaLW$Z^Ms!ZUwfkaDUEJZHQ2)1Pkr(`(D^
zbmsqiBER(QfvBH1*z0wJ4U;XuK5^bCbNJKQ^i^K-n)x#36ue>lbYt$?qJQ@By8d@I
zc|DW0^)pKfc;#kpQq8i?SHercmv<B6mDk4@c^EX_H}ZC**j`TTTrPKNKV#*xtM_jO
z=$<XT8Wb4HT-a6qZV{K9xv0cxS)S7Evb{b2xtqh-L{(mV`^lPcDS7|O1RVw`(VMYq
z5!05Gu3RJAP%E@pK}T3NGE3??zwNXjBhlVc&%(3?*KZnYe7-gN$&<t1S#nF9)_i|j
zTgOxJE7B<9>vEZ`=Ie}W8DD?-Yo+?+0FSf&?!%h14su=FyfS&-g@otl%k|E2zISw4
zB$049eb@X3j@4gm&XlZA7H>}2;&1BX=NQo7lxf(+_3B{r%$M`n{H6+KCVBZT?-EK~
z_dnuWz?oy8+P*G3CEX=edik#RQ`-fb*XOO?^Oc2L)IwH7dn)6x?+;G?6^p7g*xJ0$
z{p5xJp%-}%{93|#>Yr8-%fEMr;sx6evR*y?f0;z2`j?3YTD`O9HLtFEx}^M#POff*
zIQyRrt#YsDZ1$oDvW5Tjz4}nFU$5}Z?gH_hMF;tcjumo0{c=7|{nB3FvKjXjRwqoo
zY^DEf#@w^DH`H&ekF=|~sk`ZVUhxva>umdX<xS2x{P*3T=)U!)cRyc9`uYC7E$a)%
znWYu0OBP$D$z4-hzW1;Crw7iDQ|{N6xyC=9=W6FaonP<on~le9cD`LzKjnSwSL>gr
zp8wO>w88b6N%-liFX`vHuHJ0toKdyTDbAz)O6;~P3Jh<=w#@Xk{kw@ty}_cHkxhC|
z-;3+szx1*LS^XJTXjnWozh-S7eRi4i!*l*;E<6?Iy!1(_H_QCu36{@-jh!q`k5qqn
zG^Q*rxy*S(Z#w@1mrsi)tNO6(U9M&5N?umgk|LcTy@=KKwXd$-6^q9|m)qzl_b!(3
zSU$->o&QGm*@l>|I(5lUOBz=+TmFeU{^YdFdC6}pmnJK&ogno|^TPY(l`W6&g&62=
zwAuOSMcs|*2m1Lt8o~`EE}pM{a$a6xbIzG%#=lvn`z9nhzvOk0{P@}<<W}t64f_P2
zU5YfnwB0eYxT}xJR3~s_$hB2_Ub6RBeYq;L{QitZmjnGix5roIMEo{Y-ebY1+jG4t
z_ymuAw+zqJ6*E_U<k*uZW%X!Q`4efiTG46j9`U*Xr*8*#*lgXPWa!GI;m^T;Nh2xx
zn%Lo%+?~!Viy}X5*)FT5|IWtS?%UJsr`M##PS0swyGh1d!KN|z%-3d5WwsN3S1vCU
z|I^Ob_FC@nvOM)~+dc#;p9yy<TQzxRyZK5T>4ehk-i2{m-&RljYxl`Hvgod>QFVLf
z$=RF37*6>%udcmh@$-`XUUxq0gvOXZ@Apq^ulwG$Mb^acR+e^(aK?Az`|~cGlYbE+
z&M1+#UZ~{sg$#?;Nw;4<-O6fv*g`Du#!{^xu5$DAE;<BXSoHX!w-&=bwYMi9I6kk|
zOi;>+ThiIFqL;%*MZn-xz<#l7laEv~KRJ-xa<$~NKEGLl>_>|Y9w|BrQpWu)iIZ6x
z^)#5|WRs6>Vh(*BHD~3ttOGV%v%3Ghy2k!wPcZ+~Pp`7Vn4WN-Zk%oOG&R(yVddvi
zb9)VMvyziJ`|Qq6X8-YkT{KYB@Aa%+{`xPkcgC3*9-riF5Ub&+_^S05hen0#yI{^m
zZy!8gZfUQ{UZ7|6^ks_bo<}$2MYbP{V7{Z_IXj(iT8xz;m&`PAwp)2E+Y^7boQf8;
zc-1?*-iD7OMKx~SSHY+UTUR*OiR!g$n#ranMq1635MQZiuc+HTWp=^8%PDP7yo$8A
zQ~NzqJPH(q=GbH&WM5wTOk$$$skYqK_>NPrR&aQ3mbq{J)S*k0Z`!e5%R?sj1^w8Y
z4$9^1@S8qA_E+G~GcDOqPUYL{6!*!fYcF`RS?BtJj_GPTnO_&=Mb0-CzqVN3Y?bS|
z!<;s2H}AYJvH6L=rd7c9$pz_ux^(w`I_F;(pSSaq{F1$URVy!F<?`j8Z!GZa@r=da
zrnXj}nJS&P&;Q@M>g^}ntgm&wxxGleWn1EhJ8bh}#I!F3he(7?HZ)4mUy#qUBr9K=
zLr&76>gp_R-3qaWw=t|*F_A8>HJ?OXaX;jFV%oy%3>>0ejPVjD9xn>AW?_Fmuh2z$
zeUOEO)*OpDkDX@9%<1m7jqDW7S);MPJ?`y<v<SCqzpN?So>|>>e1Gsu?b~O1l?A2j
zZ#oliX2$4VyPW;x_5R9;xX8Vn-ln@x_Zh1_nw)Z#akXE~nuL$q*-zT6<tN{_+vStS
zIPduF8xOvU@Z78F?hG_Ip}FMTl?$91M}rx6^juv1G;o3wXXm~Yg*O@P7eBNzs^&b=
zJagEDKU7*lDyr?4WzM_;$xTrYVw?<TPusA=karnVy6py@ozHw(&zXyFRk%=CDK@8z
zpTG7~i%Z{fc?BU?)B1&Xcvjz9q~2ZJ8o+a{*?6v;k?7&hrQa1|x|vLkZXa17d)sbb
zZp5mMA2X)p)v2ABec!hB*Uafp=bVq#wcZl)x<^%h(pT@#4Q)O%uO!%3zB&?iv;LsT
zOy<=U&n+)6T`76m;m&L4o5!a+YKYktEc8}+e9ZLZcKiQvbJojG$*%jh<V@5Bo%KmS
zo2RW!Q=8^5p7Jx{rCfYPlWNbUTRdmI;wm>ynpv8Y-!lF9uBSIHr@d-h{#Jxf<>N~>
z&8W|7A4@&``+Tm(arvDAd3#?c?))SE{nTM|UE!Hg%3qCNrD(0Qda$WG_*>f2BNM)+
zCf^K{6ZQYRic53i{_Zmi9t5UE%rlhEuej8||4|mRP{w0U?$d_4-%KRxu04`Cqxxu)
zLrjfQbX3#<Z=dc@1qz-zizcWY(advXcd|LXZ>RKZjf@rltFAF_5|}RSJO9cu>*v$B
z`ntcK+7$Zw={<Mx(@*OwypBDNI4qMh>))@1s-NV)>r7j`%=ENKwa+H$<0|0~W;~G(
z&pY~NQ%qXW&cjL??oT%uKQt;|9OLmv@9@G4`K7*h3*5h}?VaBudtHN1EaJr?#be6%
zb4n}uKK_|MWeR(DhttvLmp2rw<KNYHBz?mjhhTQ2mr@pMa-*`d8l5Y5f6dR!dn9AA
z#*!za<+*&uX5-&ndnRVz3wTiC#<N&JG9lu$vf=-(PqY3{*qT{2Wm$-5{^tcQHYK{r
ze>P0$URyswmusDP^P^z%Jxcz%ISpb<17;mKlH$I3E3?@DQ@I}NCpn*=rz>A~{9w_e
zK<<SCiHf&*eZ$Z9ajdP>I=k!{+s|X^_mul}e)ieyt(m+fS$L}SMb_IBRhg7!*LBp0
zE!w**Ca$h(b<Mlg?We^5-M<;s%j=guH@b*bKI`n_zlAgA8?BAKSO4zzlPkh}Q{3lA
z=xo39bw*6-@8VB~-mX`YHQvKox?}xrr)9~K%h`-8&$0DxOkMKSqWMMQEs^M|_EcAM
zsY1{~n(wbeS?8>Cb~&+f^Tj`L^9~#nP2jPJOO{)<O}j;QSyfC5Lp#Uq3Z@+jy3aZv
ziiMaN-jG<zbC4xd##iOyr`tVWZ^~}S{PmQ7u7>rQc}W?Y5}MCVIK1<=Rc7W~-QD^#
zRN3E~y8rvRKX2mN8!<C4MKs&*S+jAe`?S0p%e*>y7w`q2b5^^O?fhb4r4#$U4EA47
zQiGOS#I`X@u9MzeSeTVl<?HlsN<o#)X=__kHBrW&>^ChfESGcL={9cW)0N!fY2x-S
z@WT?$e*Q~R@0ST3-^{NbP$l5by=Q)EPfdYk_w1sO2RUsu*Oc{^uU1d{=y`R!=q&!T
z`-I)*FU*<v!d&OTw_v5ut_{!StLy`B{t1{B^{R5oC#8l74@zq5xZ?Z{r9BGE2#{N@
z_ax%DsPMw`Wyjdf6b{UvAFo|+_xbpy+bhdYf7iG3=DU;MnD@%)EbpVfdBLA1tNBh?
zz3)ff&HDNI-j63<-E}{(D$!!q&+}C}>-TP28O~=}v8m?O;pNUduO}2dbZozLt6_4z
zM7zq1V-J}hxXW+dFH`y=?$dv}4UTa&m8~}4z6AX|z1aK7%cZZMt~|bR)4pld%y*2Q
zFL-;!<hS|##G_Vk*L?fLY8`U6M#^wg9^<1)=25b02ZLhPzkHMNa?7Kg*N%Pl3=4Ru
zW%A_H!c7T`*QX}R?eJ#cxg@cO_3=@uV}E)dJ}bW_VDd#ZXw%7Q3yfStq%;ohF_|W+
z-XvY!{^ZnmdG4onvb?OqDF-%uvJJ?66Vsh?=N<R6Q|agKsvWQY>}I)WZ`}1)+J-gZ
z4|R-0r@Wle<ZBzWeUoPX6+zB|z4K13WpO`zYR%r@#zXxEuP+4kpI9|<--l`bN;;P$
z<Qt;<?Q$dwbmvrFYGjq;)7x?=w9$FyXN`r{b|=)$EqBhl#jd(;d4NN_sD+inZ-s5T
zh3ll<JtO0Oxc{r<k|~^(P$yA!+G3jQXP4AdQRiZ=b~EJ6-KHoYc})6DS>Q3%hn##b
zV*DH{IZwt#OkE)~$F9*vWX%F*hJ@`*jXx#&`_s3`8b{8H*%rum>wk37*{{z}?o5|i
zxH-VbW$WJGPfB9<?GOKUyE^^nt@6If-S(BM&m61zW0jN8*S6TF)L{Bflh5n#TRTVH
zj@o*DQvRKdJX_x?U2Z*fYU#(NntFmo3uajDm93xr^n>%aN&Sf*Zfsc^{KKtKJ?_`5
z!_Pj6&6)lF&b7t0o4E4VTu+QFPpW=>Ay|Kn-v0yD>*u;eij}Q7Wh*0os?AuV;_|~g
zQ|6vFmI-}%C@+5{E5BHO@yh_drVEvC74;7}s;j8DSiU%MSzLRP0Pm9Kn<B^0+b({g
z_GD?GWd5Ov>;7)sv+1(Wm6Htj7A1FkBplH&W6^!Qu<j;j{DhnP*Yaf_X08f1ji0Ue
z;=uITt7X1?cq(4E@BHK?3d?d1+Q;@izSLJ1bb-<S@<-m87KXP)oDQ)t<S!4Hd*8;_
z);NDxCR@bb^(<oM(*t&hoeO`wbLL53pQz_|8s4?)%n1}|4>RY{o+3Zh;!i^OdUtkh
zA8DmrZQl9s{A=|NF592i-%=%~dvBKN((_#BJxT>1d}v?fwsFHAkE0PEKDfkcriO8?
zIo_HPqxHCRhG&KJ?x!!LEZ?8ePJOW}(enSA#UF$OS<mXbJleQ^&+8}6Papl?<39b)
z4!-kKXT2@8soq!Oy1eGcqP<TVYM(W0+^;#SpRld|9M8?ZoryZle+_yzoOj?>J{p+z
zC;WL|^Q1CXKQ7-4d39m6N4|+?^&4;8k8P7!w%;y1`Zvow?``#+ZIfBjw_f&IRG0X?
zoJq;@*&GACSr5OQv04!{UwM&)xNc)+Vx}-hia<;60y*~w^9~++wW>5a<=B_bUxzrP
z8>O$-2CiU;eD?Ilo~UMPy?;%rGY@ZgxaxVlr_NPL?a=9NMK@woV;4S5EkC>BcB$LW
z#f!e0c|J|Ac$O+E81m%Ve&3_bT+ZKf4$L^M@h6E-w{ZEHuRIoyN-9}jZaMJ#1b^kS
zOV8Lg20nP^sXgbk#*?R41aI%u<~+NQJ79)MxPm6{Q(xJBn|%LiS{suVoRTe_6JFD!
z@Udp@v^bTJEG>b0rmmT-PkOqShgBuaJ!4-sYtQ%C>nHduLJCeW?tZzeIwo^d?*XF;
zvI!=!fBw}z&Hn#QedfOK?wmuPV$7Bwde&&PjWhqly2v}4>W>nfT}`K_eLBB?bN{r1
ztKxR2HUGJMy-rPhPU#GpP5;+*92Vrf>+Eptvgp!Jrl;<mI#}gU=Ob?ZRQ&jIzI6wV
zI@s>DxfMBi4x_%itL~4rO^YiZxV}EAS!LI&^-;rhj|0Q&4PDOhEIMKwOL=PzCtO#J
z;QGE~&Q7b+k__hXLvLcb&o|Y6f4=?nQF#l`sOXPXX7_3?3tkosWLaUjXYZkU?eMh|
z^Z$SGo7v9wbZ6vU9-RoLHi6e|>-`?PpA>gVTqG<aX7ftSZTHITNeQa6QUbOXWHoL!
zRO%J8o4Wm;)(Q1PF;)vz&n=I7xWN5qX6s~@wL07R-icJHE<ZeNa-bE*Aw&0H$K}6%
zw0x$d+E66xd9%RPLMNIf=CEqvm5F@!G~GBHKgo#hQJSRncd7NKBY%?uE-ly?KKak(
zRPz(M;b*3#-Qk>EBG1FyX|(5R<r~M{C$F2`S1f&zKD+eds*-zr&2Njfr&m2QIlX76
zu>fym(#=Hq2RlpD{(e}#{nXX_wGQk4onQWBQTO-B+~+Obo;}>NPi>L^lt(>>)ZKa(
zsxE4l5|`h)=B6X}?nPX6ciVaoN3TBJelu`oLQmHAX(F!!XL~RS`+9fycN9f(20Fzv
z?Km|-WWE$TTVMO32{kH*j{A6N=<sjsbX^+C`gw9!fB520Pq~hLPGQTxJG(tt&whV>
zr%wIX=bsK<=9^&q?EI9l8a<!obqxzQJz4g`D&j4_?Z-(mzgF*maCU31(awcl{co3^
z_TlW|QOmY@n!?ty?}JP)qt=(*M^%a}`%2GR2War0zaq`br!Aehja5#$M9d<7-6ckj
ziXZE_Y&INFG`YQK<Dp*5AKRB7n0(7;VUympw5*L1Q#{r4zlV42%-s+f9}<>%cgDw=
z#qL%sTX^>C?0<5-(agNQX6>J+yN(v!XFY$S^SB&`<;FO9;bRdynk}*{U0*S7GhGck
z3xIFFg7@xUg*(F~`91|qn`pVuXG>c0`aO>~NE%6R&b_xcS!DIX<;`60pB%ieUsu{*
z^Ka4a6uC5+7i^!_YX8@||Lfo3Pj}bLsHe{@nz6-yfuea)q}#M+0qxj>`bG}f+e`V^
zM(lQ-HG9@l@yktHUl*oZhzRQMU-{sf=&dPYMxP#7<t==Z@wZ~CON73JSJ;K{4rYP9
zDekwsxiohlF*x?*Aoug?&L`fv*IIY}{FxO#-)2AG?)wqmvrX5z-72gUp86+P_V1;g
zj32LBT4n?_>r|F@%lus$e|qBP=+y6#!YQ|oq^&#}vR>F-WBU4=D*Sqp>ilb8OlY0_
zDn-d`e#M;r*zFP4g_8p9YL>D771Ld(!kpBdbHk)X^gLH&=h7w5r>_lO-FfP^W<lCq
zF6#{k0;|{j&vMyyZh2}h_Z_<}N1T2NbJ^`*@c&!#A+GMHTRnbS*svC>$|z4%>{!iv
z!ObB0@cf03K9`DiScGqM%@n%7JWxcDwV^GLZ@arwTjbZG$Fcq=KDxh=jW}aB>6Ki@
zHP76$MSu2metKO!-K#j7ciP{Y6_@_-zSy5V|CYk?KcC+P9WD3UkmF=G=VsB&6>GZO
zRewKSm7PC{`+oV}Gj^+Fm)r6lerX|k<n62e`WJ3LPx-%}-oF0t6rb6B+AW5QLnFO~
zQ+F@CEV{>iRyFsXn73_B@%wfLS1stM@SA*^FT`ihw@rucRp;c{7|*>o!60nz=hsV|
zZl60L-IUZPV|!+1?%_n1nuTIU7oSXKc)lo-t;Y24ztFoy?+(5EH1%`Yw3`<1Z}FVo
z!>3=oA+Y2@>XNh3Rt2iBxpsa#m;Q92X}|~L*(tW`y#89A+rIv3$pmX>jmsw^e$VbP
zf6h0zPdjMgjY_Aszo+MzZkTjy&+Egbc4Z-Ik2BMvoOddoxO)3^vEk7<iZ_CTt@rFp
zep|qo-64~+t0A5>N9#)#Pr{$$d~dEWuC#hov+BO9L7~YU!CVuKy_T6hCiMrB0~c4m
zjQt?BKr~>I^LO=$9Zlt;8LwtN+44-X#Iwhz=$6=K1~o-xJ%?8I|J66uZ)HE(r#|iE
zwZ2>nyE`*>_&EP8HZV(fo_Ok+_|i?XCyvNACX4O(<YYdZU8!it+|m{N$E@BJU-!Mj
zSo!Ov_|sSM_cZVS`Sf?w<BP(+|F>Gqz7St2IZJ27^v(RURE5<aM6Z`<2%2jB;Y=g*
zDet|V@z<A!c1@YzbMy3q2ZiEBV)21(r*^PO%C-e1AAS@o{pZ)I1owWqQ|k|T9N2nA
zs;A-VjgTdqmOpwv|8{`MrrVbix&s}*9{;}V$thRs8u4Ssie8**N2@bj_quIyG0@w)
z=J?HTY8s#H^{kxv?p3R=T)BGdp@6$qDO`bS>~F2(?|t3&_eq<*osxK5@%lISqm(xn
zW+fa~3*Odp?WthJkFeQR3pTAOmEx^h!+xmX^CW4#KgrAwjkwNNe>UNYUw@oc(<mTJ
zaqpb#hwhp_%$($3=)<I}bMeETeUWhwD+}|g3)v4^d@fNuW*A?0!_Dxe?&}%Lw|698
ze0{7VSKI2mwrg2TQ`=3c+tXh@;4Jmzow(G4<FK-CO<E&+#G=myHw)AsyY4?8|MJMg
zma~_P_|l&(Ue>4D7-{n5(v~uf%Txab?KJMFC=vR(#AOqUnZxo>`5RjCKfX&p+3m}_
z>2}^{gAHF!83(+%{{LIt&r9O(glA5gEZZlkpZ$StZQ{}RVh;!Qj^)))@5syRO*P$d
z(=@Sp+MCj6EvvMj&ps4Y!LecYEI$7UA=6WN6pGkb{WnJb57A3xUa;}N#5Q%gk{gaf
ztj{<(<z6nH|8dT#;LHn`o?iF0VEC|jd&s|38HN|nMHmaB0)7;VIUmq{_wfls`C|s*
zhMg8Ro8^VROki5?CDKyE@A@oyaj3=1Pu<?<rtP#o=fe2q<(1x|9eXTfqGfjc-W925
z@mnG@J9on6{gs>Fn6H$ZW@PTXb7Q98q!$-m+A3oNr*W9;?UXxbANBlC^3O{i7u}Lh
zH+Rjf`6(EC$FI3DqB<sMqs7Kg^Ay&aIB%U7$L6ATTw#CZm3vi!`D^#=kTtv_*|jT$
zS<WKIYR<%$d4jk4!<L0fdpE5s_$w{J{ygEXv5#zLf8`=aPF=0r28%-?g|s|=i&>=@
z+nqVcbHTt+waL9}aSP`X6TbDUJ&dQkyZfW*>bvK4{{OyfFF#$Zziv{ueJT6BphG?n
zKZt$N+f%~vH1E`%r{dKG8i$ug|9Wzw+-G9!v$G8nKfR52U1?68SN*;+V&C`6yPsT9
z7CT`Q(|_m69hJ+=d!|1-W_7i{Rj2ay)8Ha;xAdS7XSSNLd=}P}$YuMLJd3IIlHi$a
z9T|x`Khv6mG+V=z+zdka-rGG7e*bHOSNz(#?7&Iu*45wq{5WdKx|o|BXa5_de`r-=
zX_)wB5#uxQbN@>PYbu}pn_eh*L)@>eXg=fJd%SfUDh`@FaC4Dfpi|<!f$vm7{Qr{?
z!8ZT-`%n1i)yFMMI=f-Am)xI_gH6hjo9}cy%b3(QX`{^--J;$tM@}+SypgbQSbQwj
za{qzYE0qdu8!siUnLf!&mD@+_(`=oGYbT3)bp6lKuQBW?ny$0k+SOMn!(xx`C7$bR
zM7#w(mtK;csFNaDyyWo0_Ar&-4vy_c1@qTj*(1VY*6ArS_sv{`duqOGf)~H;3H~3Q
z;<WXQRhEpmr*6%(h)WHpc%yFKP~R<Y9-5V1!8Gx-abV(#;}voL*6p`Z-oNLO;vZXP
z2A+h;(oZJTMyGDr6ZG$Kar#NS9cq#5nbh}`c6DDa@3;NUl{9NBo3!-ufH^MHeGf8+
z>Q+n&$UJ!AqmRPcz(0isU2NX-e#}$m_{wSip@J_;Uusj~nuzp?tN54=pH21+nE&Hq
ziHec!BlRhVnj~xwHs9cp*r(R8VXEnjg$h3Z+^%N|bN_k6-IKZA>8sri&hnF6v=}FS
zc*Uq_aroAcxBA*0Vph}Fmd!Ped~(Ts>7x}<TaU%w`*ANd?seck!Jr9;thioTnjNw$
z3v*HLc;INI|4~<EPv0C}U2c)54-MSE&-9IY>UrV1^OB2a6B4sjQ|7mDoJ-}|=2?7K
zGTFOiMNaPJ1%m186HB~rw;BnlU3(G2BhFFzc#+S_X>Qqb)lV)uB|q~<&(fqC=KLk6
z-%tEg__Wb$-t{l%EYl|K%h}Eu-uNN@#Us_W?eUdQKTpctbpM_4#<cjA##QwNN%tRJ
zy%4)&*$;nyeL>5Dt}}<jZ`^pf>)?CQJLfn5Ij4H*Z~uwzYaFMIo-F?HVn&3D`=3?3
zQ=aPmTe4%vIbRlK?!_NoG;{xS{i|mB^?H)~WykI(D|{j<V?qqR2yWou>-X1_eesWz
z>+n%w)enb-fBdar%H-O4@n?YAu|IBCXEk3lVTsvceSDGh1oipxYQNuZX81MZw@AQR
zPu&a3>)qFEa6j1ls#>l(GUdEg?cICs-c!yPe#>aR_rzuCOb?wSJ-=_{Y*{x`KvA0W
z$i;gzKFkhSV!lXWi^Pr3-lZ9bOxUipC{C<UPKj7Mt%p_iL3)e6ioQp{$#qAUPxv<b
zrq1NbI}_XzCNb;uzt=nd(qv|2=j3b#t`twF6JqYZ4#G3r6}FU^Mz?-WyYWawdP>C_
zX3gMvIj5(Fp8CsguU)_Ao#>j!{s+?k{+epXKH1Ih^z($7ZRXiVX4CkMSFfM2)3~rE
zc-~s|i^?C$#s5u;DP%q0xP-H3hV$IFyLmpXyy>^ddeM%Cs0W29GXCpNO!#PUt-su&
z(#0pyFiNmCr#*Q-=L$QP$>vEW^IO*Mi}}$TooYTO{eFIaOka!sg@lDNViQvzMMPBX
zI&x%g#gh2H_T{JY>%TRfxwYSQd5zuQx8El(EQ?MF{T|Uhp`>Y+l<DRvN*c*0^JfWN
zc;@OlA=Ok*$yBs^qul3Ro3e#21RKf<FBISuIR4jF$W3g;L$>>?ZHr!L?)GNZt<d<9
z!rbL9!T$8=(;eA+Io&7UY;eCg)ydcXozm1zeDQHcpW2!NET<pbal5TLP4D+d`Gh;B
z5BRFiEYRVoUM02u#}tw4FRy-l`0CJ+2iJAoA3pPY$&)nMMkdY3LPSAAa`w&jj?e4Y
z&Ohp!V(IcfW9E^67Z^?Y&O6l??unS8damohYyP0Pc)j2I-?x979RJAZKkp7!zF?Pq
zk;j!oQ>T98m)5eeK5bM}`7$f=%iH)9?f1(UpSiQ%b-%9Ux2}si?%`=x>P3xB=U++f
zv0I^L!;+e)G(WjM|C!N;Rhv_u^4($7QCzTZ>nYnH!Tbw+N*gs9_pb?ZFmjumt32I$
z+SgN^?eE&Q?>;;6vBfUE)rX?u8o77nRpmAJWFPs+wA}E1!?)A?g(q6Lbi^M@rOYkd
z;B#T_f;*)JhaR2M&)X4Q_x*Et%D0L;hD)XHPLclVEITbPHFbJPNkCz+Z8qzK7OU81
z`B&#{e?Q7<DZg{%#O|QC-`6b9$e6fmzl8JCU-fU?S2Nr1QOJ}zw`W?v_Tjyf*H2Cn
zemBj3-k$b1n-kiun3{O_@=B|o+f@Gj)Un>^C;Z>-_3!^R-S>0HqUbW4Rjy&lucpWT
z?OQNmajvp3Bj2NCtK1vrbRL!nIH`Jo?RmJnjZf1p4ew=ZIM(Dl&v&VLF6^81>hQ6@
zg;5{B9D2w$XIphy?RJ^McYd4R&$D)n{AA)~*B7}-W4ieCH6k&$RNfx<oicUDjq@TN
zc7L*E5A)_{YD_;Hz5DCie7&m@Px;RMSa;y-{(ath7XRy0zFibfvAtjaF(!a_1<xz)
zV9k#{hi}NqoZ9>0lhl&!!W_(}SoW7@O!=+3&m~#$?yfaKO#V@aE`~k#_{VD#TX<8a
zh<SQ`*0sm)N@Y&-_GuNlJe&Jwk9g9b&bOObrv94Qo!9*AcwdF&xx?qz9pN+TILLJ|
z_LJ;~v{zrMR?dyk&0cXQ_O4~!?dTFM{d%3mZylR1b<UP{b~e%qdzrG$+<fW7+d9+R
zOoCoqpE^^}=v>g@9}g#gJ(GU2^oXidOb_eQ5RR!!;{DwtZxwVTo;@6$da-_w|Nbu`
z_P&pvJT#Se-f`pgH2cE^vpO$lnA~>{5$k*O%{H^uIr7EnUeT)&eM^@;sn(p)c<0OS
z-%r*U7c|~76yB(ly<BqRp}VKLE6Q@G-M{y-CGPwI?WU`blvJ+-uiI2qarV^KqPw>G
zUUwNc|Jr^xKH^>v*F0}2M)`n}pq=T7YWX`uX6s(NYOyEsRCUU<yd!Bx7XSIhvz9qT
z=Gw0%+yWNwmJ}LiE#;bj{}%IXHJj!4dLK`y+9{S1`nKnH+6B(a{cUyaf>TcyJg~_Z
zFc0F-d^!KKfw-zg_<60#|0Gh*M>B0TykK6;X>m7EbWi4_ZHsO`e7RKg(e|rOKMOZ_
zEsEH^xhCmLhpBXYdex_Ap`Y%`&sA)f-=MuK{FA%cmmQ|}oGU*befsJBbvwPwWf@0u
zrz~-pncNb;T;co$?sb}#pIWbe`W^jWiQDk^1JMK9@Bf@Ir{+<As@lDpyG^C#x88aF
z=Da(h-mK3%?(5v;Pu}0(9rEo~_VXKoCu82d`#n!0?)UT3qAR=8PRrh2{b1wPM#B#G
zm1nN}<<;JKePz>$Hs2QcJ_&y9M@Q2)th+aR@?`({y2opC*1g&ESY_q9l@q;8boBP~
zJn-x4oxSbUUjIEx`*%HOt^89y!|LsQjm-sLGMPoJzIO`k|NUdvljRZWr^OGQxe{?b
zt?!xhhVvh;L}{lPZJpsHyiJ9@U|T(3&72zr3QuBfZ>f7LnXu(}HJCm!nOU8tFFi{u
zqV>8J=gXT`p-cH@@uY=*5WKeZq_f!`l^mNj_to>`bmRBFaryb7y3ct{Za1gV3pS-+
z4@&p{?oKfF)=GPL$I9>Wo{4?a=WMLMvwfYrpUuPeO}{%QKh0%7H+A)gpT3qWT(95x
zS=+qjQsVy${~AjFNat4ve7jY<PHg`-_dV5{OD~J<{Pe5(<HL7pm6@_;Mcq4m#P)PK
zv*u?>t6V;!edw+3gfnf&9(!H2aQXKrclOgo>tz()TYgoTx&Lv<%40{Js|<HOJ6y)1
z+ns3n^at}(WBC^os{j9*Q}c3_^^=Leubp`Fvv=1yzp7=+_sFq2#I39IdVE?|dW)_0
zs>O~od1bY}vqfZTPhXh0x8wBX65)=Qkusdke9NvFv0C$=&8R9BHCilKE}3ZD8ytKt
zZ&7>v<QKn+RG0pb@7kOyl@b{mC!qCgrGZo&d-3J%p8EIqhN=4PGWoT7;f?48BJ*!w
zQC@#<XQ<x)kCLAj7WW;kWR(!q{J!HwVX{nG#gC28pLC1=k1Vs;5qWKAYX2XdJ$Z&U
zx7`;nW%bq;?whaV|6uJk^>x2iZ#kPY!R*O$Y387ac?-{rPpD1&v`)9^<kkAApU>NP
zrM(n?Q1!Lq>EV9;Y1ZrNJ)g-~i=MVQ`St1LQ%fG)d~CT%;%{E3)y=NYAAatA`S(|u
zhE~SeUv)blPW$|1O7gd(e0E)&;ccHDGdbIEy$luPZk>9n^oLnZ_Qxs0e3P0BpP#wD
z{>R#y&zsm&ug%M;s9Abb^v3H@7Ud`G!Hr&Wt_v)=m!5T0f1dL7SKQAp)#9h}tbH%@
z>#F-2JI}dr+^{cPx8&jPP3s?V-0U))o%-`s@2BO*Kdd{(ZDF{<d+wQ8G0V9VW?wkq
z9UQ7S|G%)^{;a#PGChwc&Jdb=ZS%hj?Y_k37Xtr;);yP35Sf>;a*|k#O+={UYHPm6
z4W}|r1aADS@qlg5yZvnLiq~!Ks{Wp9>izHS?dK;avcErfgz1#*ao&$Y7mxAIe)@j@
zzwDSdN8fLZdbGaU{`7fu?@3`lR$Cmtf9$kGdCtK?kK(0fm%A(<z2Xi&|K&t(xvi48
zPww^Ne|zW3emZ^suDa1`xBl=TRncNe(LJ%v;k^8lv=-}Lc=SnZ@<Ab=EJ4Wtcfpp(
z%wwC*1m(Q@bKdm%gV)d5owdKVWhZ33n7Fn0sjOJT&ufnuL~1w3d^%Zv>Q--T(bu&*
zx)`qi%X4MjpLeeF$vjEP)vWvxTc0JZKbUnh;n$vDC-p3!vR6OWwys_*oD|<ARvDJQ
zr891d8}}OV`wMC+k6P7~R7}0o;JbA7`bx3a_LeiPS3Bw#p7JUyc`)O!`99uh)5K4`
z2`}O-O_Ve|?k73BwfT?H2g@ZVkN598A-wv@M)eA_=#|SFt6ttXZMDJkoNZp;oS$p=
zKHczF{J}AgJA2wq%VQ^bNJNy}m7Vs1;oa_E&-nAE{C*#yXnm;T(bD)08@s|2r=1a*
zuxE<OG^Xh}Kkl;ZYI&1UbLsr*6Zdy0A3G^t_a}Yl$8+jm`Sk0KefoCv^%6#T^W}CA
zd6v&Oz2w2x_)WL7_bzOyxE9QvW#XM}k|}z+tf-3jOxMyK?vIXKE}t;D?*@06wI09o
zvafG4jl5K*UDNr`R=BpP)_HHuhuHR$SEt*lmIiNJ-S@Qp&pKg8`J)Zm-ge#QO%}<|
zB41m17<~Ehj^QP5R`c8A|BUXjT!<585c|4eV(|o>!<F~Bbk4r9s^9i+Zp|0FPyFv=
z_3rQfR`&Cvx!m-~<6B;(P5GVS6?kYdQ^F@pttD~dN;!d3ZvLHm?uu?#=Ix&J`45$z
zS47U2c$w-|y*j4$?(d~iU!ztm-5eXrxNPM@Ht%^`jd-VLpFQ9jEqb-)A(uYqw~x1%
zFOxr7ytsDa^COAcv1M0%Kjn+xSN`lLp?~^=Zuq;IE6e(yEBdJvS6typefENRlJ)nM
zZH3Bjde0yFvZ%IW-JK?9dD|Q5D;|hwG@oAbAhKYMgc;MnziX}H{%g<vxbXE%;SHT#
ziyW72)^q%knl$C!f}X{uoAR4W5<1(y9yEPpzB#+K;B>_K44*acue@BcO}EVHzzn%{
zH;wY|i=I<?d1+>TV{%%D<CNZ2OxI4#+kJN8|6iX<EK45Re%jan&u!WJiwbiilq3o~
z*h=4&Pw{HdUwJ+0!m>vuveDXR3)X$@FWKMM?DG1e3D1u`ydVE;?(0++=eYbKA-SQn
zd#Uwz-peM<j<=Q5y7wG@S{;60Ykq9W_BS<$SSnQm-ld36oo|?5dR%nVH?=b*4<h_y
zE#hLm^t!bwdR9mACMtih-uHIxsefz#A68y*Lw4fx>FW-EcVYjqNa&ozlAKQ>r*uVS
z_pdy4+4NJubQ8JuyT!KlU&A!?Z^gIfZ1^(gHM?NfIf)3iABVfOqqcFp{H`k5TD`e)
z>6hyBR#C^cnw-*1kJH}#JzFHFJ>q+qhP`^W=G_Yqr~E3h`SB!v<z`czM^2d=^842u
zbFPe>9-+af-1Q@5{)Lu?8!{?fyh<vrKZ|yxe(Zcc?PR)r-R=*v!gc*k>S1P!AE%jQ
zbbEY_Qs3O?m3{aQ|Kp3EYvcQh8kyH#jA(xU)Y8*T?n2nF6+E#E7p_t5Rc(<^eg3>$
z#N+eXE0K>^J^j8vR?B?u#}#`XFL5q-t9R{z;QX}6A30kWFPL!ZW0SLboaw)RrS*rr
zxvySw?T%pFdZA{@#jlh17&W=;zE)5&mj7NT-kk8Xw7+3l?}wF2Z$GMwot|a-y5w83
z)dqfsi3yEUA8NHvo2E9i`Sc{I4_CGQ#M=@WUv1*ORCzg#@B6F$e|P+Sa!PyK1LkA<
zCt4ogev4mQ<wNf#4VhbhUk)9)e<0*pwoB#e3wCGgWMA<KeX^Ri`9bo<k9V>zYdCf!
zaoPICf8V#ktX{!x)#j?N)1UsD{cgH{%~w8&lvJbiq_t}fN!3iey2Rq7xrWW6uAs=X
za-4f~awchJ%}Zx^XwrAC=VRQ_*)N**PdON}C(~hRqPR+~kb7KM=Ml~OX*qFQ-riDp
z|L4sAQ|mXT6u;W|`&HlGd5ao9aq0<u*2t)Qtj_-0xIJ3!`r6wX|I3c{ewzGx-qc9$
zSzmsHb$VZw`zo~8ai)U#m+1j7uG)UhaDIJtQShFIX%iPJXg>KreaHQO+4KKNHWcy}
zEvj_n7G7JlJjya-e%a3hn!itE9)G)fev<T|-z;yAy!jy`Q?%j3dCRW?KmXphZ~x9c
z?NmxlL*)G+lSMs$vp6?2B~1-+I{BpNY2e<zP3F98{$XZ^C8gIXhHPkk;wfgNu0MJ5
zqAq!l$!fim`{N6Q;+k%`+SR_~{nRcUKdq8GI>q$^W1me}y|UniL+iSXo~?Kxu|VHy
z;k^jSsOM4QFFFj_^m@hbT~D^%%2%uwci{f|%iMEx-EH2dK6q+nV|0am^^J!|JofrI
z7WG@p<u?^M9-i0pn#IrlXZol9Zn4ulZP@M8S6z7^QxkdaCMVzhDHir;b~DPW>}P-e
zVE>QB)=y8mUpw`N^~T-fvm&n*e^_TD^K?ha%|q+bKD}OH@y{*zyhig1p0;HRU%Z$+
z>%F+-{g`&;Z0l2pEYHrcE8eU9>I@Hiu-}#cwfgx}exLg{HKy>K@~7_gd)?E{&gl_9
z<fQ7qdf&Ene*gZxIs7#Ies$cd{^Lh|m;?S9o?Ij&(RFId{C~fW?XarN-61u*&ob@q
zlwA(VDNdcc&b^(!PTMV}bYazg54MWqmdnyz7c4rN$epVB&_Ca<+2(?DN#?0}@*9@j
zu06<C^mnQJ1aI*>I`O}*+`Und8|)n??EdAjk9+jLjuTTlp6uAA)W3MP*^!Vb5+-{l
zUPwH;aPh-MT=yDhyB+X4@!l!r#O|maa@%%nj=yH#y7l?i8#b#Cd@vB!(Ku}s;wAr#
z`SHd?gY|yT%tAQNTZ>n%KK-#ScizdPC*6*p4cK?g`1_5ponMakpIZ9==ZZNcpL{IK
z{##y%7hd=xd#TX#f}gQh>h3fz%->|U&u884@2-(`pRM+6yr!`Enc2zJjYa8vlYaiJ
zEEah8a{1Ip=0BDO-}F#h<MaB?&DtQYm92K{&*#+`hlV9Cm~GYZddlVN$(bU3$J>vp
z&ov2@tEkv2^MB>)r}wn&bRK_{W9*-`Df#p3hzmb9eb2K#;rM=DBV%H-&x+M9)rEK5
z{yn*U)TY$YGNjWXXJ5k8dmD6Hjl7$`RFqdb@E5+(*Wr`m$?^a3e_2VI=ea%4g+h0P
z#h6OYJe_j9=2?M4;?YxIi=Nl|KWgE*U(lvKC2_*zP3g(8rqf<a8R|{(w%wO%lbf`9
zi^<iQ!lo(=i#=Z+cavEDV`uthmLJ}BANgjs^heh}`E&o|p2x>uo^CyPDXr7@e74w|
ziHAfUy}IP{*WgJ~SMljJ4<eJJ(sgqF8k?RtX3f`C>wLap&Hm)gXRLE4&H2BsHYNVf
ziW?Uq^siPu<h%Fn{oCVw70YeDd@0)b>|6TNo6=$4KNWk8c5ZVrbGo>BvPh1|(a%O&
z0wT?_Q~S88p50;FyZ-gE<6$R#ukUH;DLBsGEE1=B?PzJtHUF;)*4I4pihAFa9I|*g
zJ^shTxU<5Xdlk=J@n5;-=E5)h9UrD$n6jyO(WA#dA52f=(V1~s#sB|#uAeVCzn@aq
zx8Za-b6`QO)U=pn=e2W+PQ>hd&#%3tF46Sdx!WZUo8ErpJz=FGsy8=t>%;cR?Y<is
z+e&Y7?5GOiieDFbyS3`^?EV?P8P(6kcV(TLDyKeo8|M+DqY-M4qz`{EYb-aNXVbiQ
zAvYV3+20V2q>Y~@-s|{gyL4Mj|DKP$uC+fWu<o`!*ELc7=?R~Tw`E(nJ*U+_)OQjL
zlr#|FYLmb0b}HrSt+N)c#k@%y)-Uo9bYY+OVae70{Xef(MDK|cduQT#uk3@(&HVG0
zn;x$@xhvneXQu4Wtl1wlUbrUT*?;if+4l3+e9hjiF$L#%H#|9h^3?u=Po;DN_syTQ
zH6t)=rl?KkuCkMkbFays&-}D+T59(0rD;LUf8L*6enRl~d!@Cy6*n25n}1e4dD5``
zy{>%a`HMy0+viQ~kExrzCSqS`TEgTMTdUjB3k7Zl{#;ceJL9r_!#&^C-9ML3J)VDr
z?~$c+_JODFS2cOo^2^;#u78v}>9EK1O~L#o=cKZethAXG*6&aDFQ`Ab<)_by!rH>f
zhEr9`CSBimrb$89>buFpC-Gs69?#_wJo4$u;jEaqw_5ro>i=HvKVi9Cre(JOY-a5^
z^X(Ti#m~*}^S{gg;;;Fty^f8i_A>4XTX!htwdA?&YkJn~JUR8!p5o?fidVKvDV#a~
zY5Ip_Z-mb16sn)NSbS^4w|M^3g5SR^wlmLvH)VSKU9E2GUrYIxbcmPhba|c8skr>m
zi06&8+(DmGW2OF#Y01w`y^U|x)~>a@w2e3aO&;sn=<u==pZBv1=!u_wds(5lV4|44
z*kM&K^};#+%Qh%EE7@(0d!ZS7_%pZjnpYeCyy)N6lzTI+Y5Dw=_nw=cPm!|ynwa7C
z@`vK4CktjXE3iM0`?5RT{QHT`+x4eq>(|Dl^t=81v$Oi-&*ic@#m{{%3tR1Cl+SLy
zv;AVlg&(^&_fI;PYy0UW{~t!LeWKfo_-9-;on=4&x5kg$eU~*wSv}l!XB={3ZkWc*
ze*BQ$<finWAO4nx&6*}UKjDz-%+%Mrp8lv^c9MTz#kMmu>^M0$q!h$tb%dt`32`|u
z?^qGC<>0huY<pCz7U<l`b^rMyyk61#U+PSs-1S#)i}8NQ{(pM<tc<^b2Xi92qm||_
zn$&Pu_MH(Y>+x&fwLUp`_a8dHeqvEgMY&(?(t8o^t?%ZXoyEOx>HIU^6Xr*x8%Y+6
zT3Ov(veiaV?A;^#+)3io)?J+az3t<n?nK|X!$JKs7d-f67FU{(R58`pFYMv1mhO9d
z+uzvbYw1)M$5&V``<-oGc0zo8y~KSjsc9!G3{yUy4tNt#H~;T}eMN5^Kc^nsQnqEg
z*k3)psp6tG>r?-Jc0PYP@%jJlJ_lDnn5`(Wh}qq8<&8>{d_$3MJGO5<eSKeD!<*f=
zbM~w;c3kF@5#)VI(|ImyBHN}k=XRa=t#NX-RV!nD-9Dc3G5=bEL-rBfrJ`9^a{hnZ
z_jWD6hDS-x*{nVLB;D*g+}T^5`gN5}Ijq=HxzqN}PD&MT>}Q?x<xSq>Ks8ZQ(Mu&s
zwmnM~f4<s(Uq62DE5V)5wDTu#_O}x-e;3B0zOKedr})$P#0|erRQF9?9v`J`|6~60
zlxuI?=6Z@xxv%~u?8D{*d&(kxo}A&jXHq7zXxg-mWxFlJ+eE+o)!*Yi^>;#kznr>?
z&%KRK;ghHIGc%ZZEqmD4dRpJkJ8#beu01?g)TeG(^7GlF?57?xvzNYEp`ZI|>Q;V-
zjq+E!F3VV-a-2U~ar3fmo~rj&tUmV3YV*nPm%l%Ty*d?cezMkIZ@RQxjMn-4o8;!-
zS~byfa@JL$>e~BTYSwzGE$P;u-^yGm@psnG2=%ElU#+W`?C#$F_##)Tj+Vo19+4W^
z??oGIn2$Pk_nz7&DIXR2HDdanzn^TMY-koc^yJt-K5gFRGs4zHY0v+8b+OUb8V|Ai
z`(5q+b?$w#_`PLN*}X)rWvM$B&;PbFO(f1L@72Se(q!c`IjO699xj(j+h)Le+FW0+
zy(YJ`=<WJ@ipOQQ?e>xAf8X+InKf6hiO8J?5>`!hhK|3F9sGU%_{s&%Prq@`o3wdf
z_3oV5U7^n&RYlw0dwxT6dr)1C%l-Lt*_MVrU8Aw&;gj=z$<+$7=GQdS&&`N`sL)n9
zGyU7UvlhOlD$n<Rp8n}ac=(Cu_GMaWo?lm4f4Q;b_zbIbj%FuSo-OC=zo`5?$h`hU
z)tN<E2Adz`y!^lF^pXd6YeKs_?K9YQUnJ<?-RAl4wY&PMGm?`(O!DfVQmk&<oSZu4
zaEao%FE53kvcI<tu&a3YKE-{_+_lZD4`gObyO+t>UD@Y-?aKcgju(Eame&e(D~g!@
zUYZ;I<U_gdbpM)<3YHAnwZg~Ey)CCyt%#|)G$qO7oL#EJK918LE~dv#oB!vT<IkJr
z^Co|EH+w0%d{0}#Z(YOr&%gcB-26LvWopT<-m)iRPrY?EuYCO2YF3@h-@bP5^79rk
zMK^9dwY=HJKT$gBNV%4fwOq~W8|#v1i*UCcObAHtdUlKD)%Q(aI`a=!%xL-gP4#>J
z)c^ZFg;>7d;`}9g#+@zFPu%vq&#v3HvgnGTZe?ykPe{7io#jPsA8&|RzQ6nV>FN0v
ztm<_Z!AIL?lnM)Mw&7ap`hZ8_QVO?glUAMaZVB^sf#+&|FWe-PzVrXn{dtqL|Gh4}
z$$9_D(~tXdWG{M5{r}oaHTwVOkIb*{hAy1HqR!n~Us17X1E1a01g5w;k&Qo(Dodqs
zZ;<@IHs3}?`+E7wr|}irxAYzUB>n1!#B4>qUaz=PgW6jvJAXdfe)@Lb&rY9XLA?H(
zELS?c_%p-ct?wIdv%Q;7#&3yzIeU$T*3n?LHynL+rq`p`t5csxJ`R++IYU)E+OKTZ
zy*8DeZ5JlJSz?oQvxToqRODvYsmR{Uj|S}(N47V-ui(+!)7{urD(#l5CMwiebe$<*
zI!)$vLH?Jm_V%%UwrTQrS(be|c1ND~SWLkb{}UxqQ9N(oo-O)wr1nV%v)GB<el;<E
zv0tJy*mRg5+=@PR=-><9;&nWCid&jyES!8fR_Ma~OBx$_?!>$KT(gW-eRaoTGUs&B
z&^;?srs=;nTGHR3G`noEtX!g$RQA6uu64gQUw%60GQYF+QHF+@5~2>4`D{;n6cw1H
z0<Q6_mhcD?<0zOLKlQhA^pi*aZ`J4jKC$wLNb=f!h2C*)2N$gI;MXsZoOQ%)&g{+y
zr|h?vz0q4d+pM%H=G)Hl<e4ix_kGxDf7-9z@#N!Yj%6z+$$s{?`8Tn&)9<u!1)HfJ
z!=V=+3SDRQy3PqR(~<8Iv3RC;l<nIe=i?{O*Z*2$a`ms*X}!0)#cR1^>I>f}?mpc*
z|E}}8Js&M~7VbSa{qN729-pQMnM|~DZP>BKq*hI^|Cng#2R4~24#97&QfC~FOk3i!
zVygRxr<0WVmh*;nUD+q#{OL${wt?!3wyt)eqgHnwt*zbkE-)t{m)ZEvQ=`>;-L7X=
z*8S>S`*)M1xl~eK_jZ@;)K@7ro}99`VorMR`f2&xP1C%1mlgZddGdS1`R>WbcODe9
z>HBueJ}2Eb??mFh81}Wtq8?}-msjZbpRG_`^CxS~Qa&$Zx5efqS}%^Iw8g|;cwM5_
zy{x17xXR7CGh1X?LM}%?`nBO7hpzr!mb$i<#o>LAm)E>LRJ?Ajqh<1A=T*1<)mPtV
zOb;)-TYK-@ve4MCZ4+9!CcQYz;bQ12l5AkXcw4b>L$b8Y?LRr{8~<)pv$rmEnj@iZ
z$XE8~s6?}7pReFD4j03{$}YmIRwysLJ9XRpeeeI<7oV>!e!qMD+OU?IdlSFitxi8T
z$Flg`Oyk;RLen!QS{yQ%cl7I{1MBy0_Fng|{b-S)+KUP!MgMhA-X)3kY`eC1Q{8F3
z%!89Zdp))IkfY=G-=^SJMC`Aw$l{~khmHCke_wt3N%8zhmHWRARW9H!fAcCaB7$p$
zNdr^NntNC8DXw1|segO>+eveEtGB8fusL%k7fe3Chgsb#*Y+EG1D{pw&&GxOvt*h-
zhR?TUpWGDtX|KGkI(w3{OnC0pWBVfhd3Ue*^1(e-_KEtTpj1Qc)k<>@v2Sp7*Xo(Q
zH(5@@?EQ<0pB}%r(`P>~qdz^qitWXzcgKxy)|s$X#NJESvy$7rFx=~_$O+EU9jO}&
zx|mxNUimByc;>x8#l@9dx+X)?-Kh0>1owBI%GnuR>h~t7{aNXFB%8bE?GD%8qNnwC
zy59aVD#dC3?Vrjsa_8r02x=DG(skj~T)k@Q_Ivjf;{TkSZ1j1C;HNb0plXrlPVqL8
zdV6y=%Ggv->X9;yaa+9M%ELJ?<$N}6efM@sdHJ?SJTK>Ndh<R1L}~fHgQkT>-sL^t
zGPCVcTqfMp5P7t{et&e{zK2Yv?=siSS6#p98E4M{8UJV9^*Ixl{<hk9F=^SI@~f3a
zw_43T9zX1@I-kV3==8)>36;TVKNc_5y41^bC+*M9JnKiZoG$X$&&+RoT5#>?=SR;P
zLh^5^d|Q)}*xZw=#9Cp_%E#q>JkF<K|4r4a#;;3Sec9sY@YN(|q==|}w6Fi@$#rbc
zhn_iCv&~M|-~T@6&b~*bm9KQyWL0uoU1*E(b<ms{r(0ilsKoTsr4UtJ1A#Zb>+Uk|
zjWTds_v_HkpytYkI*Bx?j7L|dDZQwX$lkyH?^ESZudB@;2#LhK%rIg6z9q`?_ZQ7i
zOZ|1G1@~E7T#=Raa#+8Gsdwi3+GjeIIakAe{(V)RdT4`IZ12>Q@$bx+J@Q%a?SFcX
zaL_xCj{+u_E=gQUGWpA^UCb}I+jpVOBaS`!hcsm7yS#Y#;XqflYSW6v6YH1n^?#<5
zJ4xH_cY{pz3!RvDbMCh$U(O_b$=vC7KJ((8%uk*6v$gkEyvTjia!m5ot*iZyWdE$s
zxwZMS2Ai67nA^Rh$MtVCtry#}N+Cs5T*C9HU*d_jxlv+FcQmxcYd)v#{Q9c@^d8I0
z54xF7De`m7sQ0_o7qOiAK%-%3S>pYQ?7cBx*3LHk*Sl%sQsLdM8#iYB{P}6&;q=oR
z9>(~e*5dln(O&P-H$6+H!LWYUQj4T-+Vz`!^M1U2{Av6B>L@kYOA0cHPuoO`?=*Zh
z+f~v2_|+QYK*2;cw~r#LT6F3zT|UZc_=0O*!4nzF=S`AD>eo*8ANT6#liT&h{*{Ju
zn9GT@4?5Fiwmpcv;QUUI-Tnhl-5&M7kN6s1oSa}E_QENq@WO-LjE9Y07v6s>Ki5R`
z`GJ0B|GPU)c*<)0PEUJlvr?|4@N;n2_nVK5jm|h_9D2<DC;w2y_Dg3%%_BmKZ{PJl
z(OO?B&R$yR<22XjSlaGgA8%}DC^%=nWkJ)=lY3WhOnSvDX}mUW`hT-Ufg9d_G~4;E
zT>RvY!o`Vqb~YT?dMA?Y#;^b1rR67_{{N+1>G+k?XKsECYL(t&vBvrMLoqXtcTqci
z-&s9O|Md5@|786-uI(ZV+YhicNmYhOEOzUikiBn5NZ;QR^<IA!w_aK)s$%%$fy^FG
zr=2U-oam|hG>3b7@e##cGJQu+iHa9B*O%NA?zR41l=!o**5kiz{G3aNzD+pzS?kFy
z>F^U@i<c$Uu~|)=kelbU=Frty^1nYg>Fllvl{&x5{rtI`OD_e<#AH0}(#mQOmy0^~
zVdey0{lZg>yxs>c9|{ov__|enznIB~Tbav*Ue-(Tg;#hg^Ix20wa6_j_pb71{l6<?
z{!dpwC8@46fzwyH<dTt0`;{$%j7ti?o)LRfwfp<Vsh?iT+co7GYH=(4I&-u5$?fnt
z+K&TgSkxTyoMJL9CavP&k3QBAFROKq^IMf!*8Tg$T6E*!<)@49?_f49oq8-W_3Vz&
zH7&PxKfMt7xa6#{`rbJY3oO`vtuAStpyhK;&MJM<ot;UGuk;-1spUMHxFGZRV@>N5
zA}Ld&XGT7_9KfK(`0CLlnaaigKcv*~<<1n?a`lv#xTnip@0O1ix7YMCTsvFPGyh0_
z*uN=fC3u?meD+yh^NziHtHY-o5zWsx^E)e@o*&(AdhP3~{1~>C6`5}wy~Q*?Ty0}r
zBPK1h|IgXSMJL_!r$&0ad%tR^y4m}1i{FIPif%!^vrcaaPdL?5HTS~p-f5=2zoTzk
zJ-HmNGvVlp1CbMVGr3kAVfy2rU+K~Nd(r1(ud=lCc(1%u{^`1$Ytp2X8uH0@QTp*a
z-_)%+uy)G%+D{?JgBvu?-OIC-68;<i^N-@EztJ1E<Z~VCzPZ@*%*@Ye^E&5!R{d-8
zX5kvI?3jYY4b$E?q&*6eJT%|W|L2ou6BP8%nV(;8_G3ZuhKM+0MgNvdO*8W2R@tT(
zHUIf@eEsRC;_D|X^V@1jm?dW%(>%E#iBWp)jK?>6_p-;VWnI0<A@GIIp1;4@-hTX|
zyrfZI;l{qdM(#x?y-&^f{OzyK<qNrH3l0Sbe-enja3I;R@Pd@{ryuLxn8Tc>a&_FE
zaN|khRgJ97oo`luPu%<C@h9=)vI^=tv%0()HdwJv55D|0QK<NHpID_x^so9aKddH(
zM?XE_Tv(`c?3$l_Nz<RZ;pg15mj#AfPGR+W-Lm9jv;1+U`}a#{2N&IY>3;fb1ovO}
z_?^yaXLGM43rv}5!t#P^``e={CnV%;^89dF<EyN$gU-jte;3{P;IeOzyq>n`GH-v0
z3aRgPHQCxy@0VJvozlrQHQn-YkYcmV%Eses{Uk$8&h$x{av0o*c^4&nLrVP7gCBk&
zcO0%YObgd8v)}*YcKK6xbDg8PcEzQ0ZvAk-dC?*N)(+>oKR2o*`)h@4Pe?x&cDsD(
z)Uluq>Yi?l4fpo$C|Vm+^z*LK|2u`7xOMmEi4+|xb(N`L`sA5qUDvU@>GrdmT6b=!
zPoGoUqBnc1x5f(lREgsHXRYQ>H|gKi=RPN`K6~TFvl}%IxZPsfQ&Yn9UhR+0pBEKB
zZTfb`w)jRLf9T~d9rb|4X#M=(KW4f=h~ViFZ!Q<jFg0FV)0ZjGWZP)+FD5l+)*9J=
z4b!`rmpU6e-+5yCA<?n<q>8+)RNK87VebwIUU|>Dn1_XdIW@v0UXS1I=PsF@8OuH?
z^torc<rkd#F|p|2BF>`U#j{f`6};(jI6Y6#zWnhGw)fGc;igAcGp(#B_$9q(b<oB0
zm01~5H^XKw5cjqV7diN}iEW;<T(4FR*BrNI-NOsq8Wke7%N~0Ew{-8Da(9Ntu6O&)
zpYD1cCzv?DzG%V`>kOlhZk>`>jpW=v^;u+1**4?JPP3h#Ry{6VGxzn2?$|6&pI0FV
zC)RPT{a5T~<>F`ilC?77tKZC+_=T^RU1UEXc);}2>gC%`gudQ>`p(VZfX))j$EhA{
zA4;bG3p<&Xll1f8<JT!~c39=^jrPuG&`=JXb3!?8V*ea2F3F2ORyH}CS*1&K&ivne
ztf_Bm^E1{xyj#v_hSvsNEWNUzc*)~iyEh!QEM_$N5Sb?7r_i(XR2I+lgw6-K<@GUo
z7H>JCo*oD=D*fxS#b_tLt!?COJ>>%3+kSpdM)kAYGpd>Y3CSc@6)ril|Nb9|FZ|Ej
znEmy`PHi}(w3NfI<jb>`Khg`{ZwTI~U3@P@AZhlxn8(XjFAo0q^q9MATIk}!#}hJ-
zy36_;@Zy@8rhVLmf9>S={~rZfmfSO0d9*5*@AHZ|200e;pM96tS9IO^{cN|9WN)in
zi{&~sg;w#)NfxO`+FFf2uyz;oNVa(~FN)07=4&;GRJc&m`R~*oi7p1YAjfvDsf;f)
znf19s13V+TJ}U2A)00{?SEo8_ZOp$;zm@BkKUC9CmT+)a)%tb#x$m^w)AJ`tg>c0(
z20xxPx&ON1n&vMnWtjEsVqg8ro_Qd+)Y<lDbH2@$dk<qzr`ZT|PI-E*BhBG4zj(G|
z#;mSMi<rLf*c4`Y3!eX;aQG&ZRYJ_(D}FM^?(JHq5g_r#^`$d+Px6(!0&dy~*&c?+
zbk!f4NwjEvY|*{C(`l01!j)4NKlh!)9(P0S>Wa117nUnNjmlh7^<@6P*NQ(6#@F*)
ze_6Ovx}E99UR_<&7d$+I#{w?ydQxz?Kd*|#I?g(kW!E*C(@Pn;N`ETI9xqP*^tf%q
zhbIEPWw#S=UiDx<HCZ~?<Oq+3s8=sL?{q`X*6^$k>Gu;u+<AY-mlZ75k%;cE)`;Y)
zoj%EG3)||ALQfBzT>RvS^RmQ@M-DR`ZWi0_l(cp!oSMGXuP5%?<mD;9njX%$(k|o7
z%$usN8!_L{s`h!*k<d@KX1{*&tNPlBJ1f6l@ZO@aaQZFn4~@e2UK`p>KE}1SzwU{H
zWar7KzL&=TuU)Ep+H3mhwDt9qf0_#gIkjZgT@I^z;OV@2Ye>U&jpUkprW+D`=HA(t
zvpDAG$*)Ck1d9`=+_~htO>5=k=d~Hr?(9yQY;xwXUlfmO<R2Cz)1D&ryjL5IKX^{4
z{1foY)NaF4gEuaBuPWN{ZDiQ_X~x>3XWH_HK1~mAHMQT{u$+};VcavtL<PqupRerF
zs!Xvh<IJ!1e|Bcp5yhs44jwo4&0LWti#d-+K3LIh`81~Isf_Up%Z%V7uFlGizaKWA
zVLs2)r@4Bf`_hB8D|jqi9!Gu9xt+0x_n3rD@nUDSDGEYMm4510*l%CbdUV#^OXq$>
zm`l7it7mAa_^|x(V+*bY>}``ILzZ6Rd05QQ_c8k0g4B+;=PvkNSn2ul#@jg`zka&>
zG<)f~Z+t(GrTa}U+~FKlZk)B*xIW2*$4z>wU1*%{+O^eB;`1v4_I>USFYvfzV0*_)
z{esO|jVYr1CfyA7d43ijCY+lx*|m!`ggfg%a;lTqw>xs{>Y6qg+I?E(7C5<4UXn|B
z?u!G*?RP(L{&cdq|Jn{u1Do|N7MVGBj~Rs=kl0o1cIxR;{tAg}mo~Zodv@QT@nrrx
zJJ;5SJ%XuTzZ|&Rx>rowSFGcC`jokO(Ms`0O1>pmPdXnv{ahmM^uw9Ce~ZpEtxV9_
zeym*6eyaYBzrTKqU)z+rXsSj|(y;}T)s&tK*FTy4{snt+UtCVB&6hK`s|s69*+RAl
z#PH8E6>M82qodZ}Vb!JF#4pdIYX3WPM&tbVOD*{3DM`71Rfs;eT~R7rOmx2FkC+bU
zX^&V-g57V(U3s`BV$PkNos43?ST6F;k&d{lX<fdZ(Q5zOjEn<DR}0r|ciO$U#NhFd
z;7`Io-V_&Ic%e5%e`#9@qkzfBh3j95n%oHybTm(0Tdn^|`Rv`M?G<xc6@&gAm!CSR
z$v-Hmd(!KZ7W*C_J#Az2>f`hK(_BCE7o0lQbM(O<3(xoGG(t}Q`WpQ-UOry`a-o65
z@oe9RH{U+Hw7oL8{Ura!s7DXY%T9c^+Z)m6%spxPe>a(>nJKS?&n$WLs)x-i?4jR@
z^tejrbw8g97hS(RJJqg__1VQ8Hm~nRPUP9<)RlPBz|HPPz|BJ(jgyXvOfK-U(>70O
z@@i0;t+--^`61(VkLTw<m^$C$nd0=CtczCbkIwwLQ+9=N<AU4wn-|1oJY01yEcEob
zxw@a$*2k)Cx7+IZ%(p~%@hxs;1=%moqB4*FRutDA)PMQz=&LEm!}0`YJ_=hp#nH?#
z%=OU?cJBS>^3Sa}oVE7hhqPkV0)=(buRqGy2#OwWvC2L2!m&6@mhth$V-ly7FJ*Ez
z`^d^2xHqvq{+3GoyBAFBb7r&|{wjzux-{oz!_r9+$9uo*NVdLdczs>#nziLi9-ms`
zo?mn%C;kQ3#=v9|_Q^e49vn;#TXxjK^uxMI4-9<o9Nn1Wd?Z<=e)9IHdmAhkvu|3q
z?^)TM*A1(9PRCz#xnN^8x2$jqo0gnxhTkC<`}_3^O0uPn{!{3`QoPvna(j%1?sWbS
z3piq24_sl;oZ;chC*e{z;pERK3D+gMH_BDm7k>TybH45B?0e#mRlLf!?l^MtssHAw
z;-Z-v?STp1@2%})`;-%YFOhPaZ5?xSX?e(J5r;Lu9ILq15@#E$C7-u>>9+IHZuisQ
z*V~AnYI2w?HD!u3%b#a$oP7u19aDMbmeUuxwW|BhuMg6nZnv8+oDhEc53|%#)|Z7r
zfnP1%*8R_XQJkvg`7?CizO2etw?g3ty$|I^iM2gS-psvCk#aoiEe{;puk)twyUvFx
z8-Fi*vvtAd*428}?lM^m*3W;>VDV|g43+51PF9-RE^RFP`E&a96W7;A>+!F-rTAGr
z`n<>N&5B9Sf_ZH+PkQmNGE|u5<sLj@{_YCzi!`fN8EK~76WeFr_-Vm+x^QPs<Hsus
z3k)|s-n;kHqi1Gs@>t_8IlO6`?$7>a(nf~!6$XDAZcVwfy;NUJCSl^iFB@m2pJge@
zGZItPIhZw1y==?rly81TeTR2%Iq80CmUGd$1LCI=b>^I&>RY%{e@Zi#!Hb;}zd7mt
zU|5<q{VA{hk;yBw8YUF=sh;(}tiqji>FADte;)nL)va@~XYA<eTFf71%674%+pqrP
zy2CjtHx3C;;Ggo2C8Tw4%`Xr2)Ry`w)q=%qTD2Ls<%?>5&`b`UdFS^&sfuUo*jqly
zT@hZlD?0CQlC+wac+woPm4`NLs$RFJO^D6R=d{4%)~3b@_apXt?)y8L{pqrF^V0`?
zEjsyHOIVIIXI`<qcRpWdLBP_-mKS%Mm7SXY|DD9oTT8tQzKI-**_an!xM*4Zv!kY;
z;=k|F=+!u~`<7K|d3O7rty_KP-EX+NIrm1O<;F0vb4Pn!58OWHb>!>Psq1Q1xv@T)
z|9;a0(F2Yz^^IgZg*mKK+7z2FoK$C<?7wcq?xtgT#h!kb8@O2Ant#M>`f!<vKUsRI
zmdpDpE5WYA8$Pg}_;LQ>0b${u>cS)1<xTfKUReEU`}Vbm);;5zX}^&1G;3t#u8p4?
zIHnsFP7phBZn-P3;iud8ZtA{IntaLQjRl)=g2yHc*-4N0Z*biw%D!#B-KH=%(?<_B
zDtzt|*UZ1a)!i&%QRcrHUUSv`vX(A-vQo!sPhaJhBVMl!^d{WzJ6rYsZDXUn{0VMH
zg^AWnjz9RYPfuq5TBDZqm?}N>Ckw1Yl$5hWp7|_t5uc{KT4e@9M%uiq22JzXCd-=&
zv9IS`9jPkS%MkO-v99gkFR7m&Kfh8?KKPLRa=_1IMOJ-o%_qMMT-u`qQbl(i@Cts~
z6`^v$zoSA_a$ZH}`IQDITD1dyJihGfFQ3Y>rC)!Vo^-BC-_PR?>5gk!qd#oeDlk(?
zHHm9(uai-vWT-*s9fngb4<1RXu=i?A=idK$LCvR)+n-EM*O}5<tj4{)x|nCGu*0#c
z^kssYH++^#N6J;W=KXrVwdfOPa;mepxS5F4g54WVP3Qi4JmEw_g{qnMG;d|E10@pg
z*2foanp60v=B{VP_4<!?q4PNZ9j%Yo^WWDctlYlP)srbu;dtVm%7aU+Zg{OZ+7|fS
zg}2m&n_;uNg<X^V-vj&(pR9UCkCYzRD8a+c<;oHmkzf<wAZ5|Ip4GmhD&S}Q##fr6
zTe>>CEw<=bIK?h(TBEbSFeUfJ%N@zpl8V#B3)-DC?;707y)o~8+ro8WIj`#<uFd^)
z!CU(2Jn@6Y8)^=U_*_tWB^Pqa?9J1t(~><=2UfmVqWaF^M_im;^HiJOE3!44uZHzp
zmgAnq$othoYL=+-qD(&%D>04-94s#nRAotsZmSXIwGj@gI~v3y`)7IOA(c?^{`d}y
zZ)^o@!fMeo^`!YMicOgg_WSh3Dy{n{I_30|lFbGwHd{VS);khx*SI`I+jzlLsVDqS
zCOX2}=cRcyO8XR+ZJ(7d-kxc&amQT`CF{xl;@77ud@PvZ<d!VGOfLUnyVZ{~`Uy81
zn(ZbmPrb0(<Co8z63M+{f^}Zv^Lg3>9x1SdN^}d`)ZY3WDAqmg`{hf4mC1XT+?sdj
z+uj21c`IM3Xa@zTHWX?)Gxe!Y%Za=7i7lvo%XHS3_6I+%NXOmPGq>5oBkb2(bZ3p>
zrVkBjGcR3fm|b||?y*l#-mbmDW8~&%leJB%vgk+fa~Zw+<}pu>FfeHE_jGX#Ia2n7
zJ^n!7@t3@xIM-CiZYtPxW{#1U#lcG*$qCtph2f0N0o}^{6^6{^KDRnc<_J8J_}%Qk
zPto6Qo3o$gKF@6ro!Dg;I!bg)_8;|3&Y6-F{(F_v@*BmwUEZ;LG?}*EkmcIP7_}!4
zRra)1)_s%mZdl;5GB&p+!~9%Acdb!zhqvn~vkx527tfUWY>BC>d%n5o=UM#|k3N=O
zYVEopv)MVwa^KmhZrK~YGbTqzl(jD0KQW@*ZjqN*BD?0#v)0v|{?04@il0(*5V4zT
zr@@z*xJ;R++0Jp{u7lov$&<xXxC+IJY#vVev7=J=<ky21JEke{uxhRDSm@Cu@Okqm
zXUk%VONFY;M+(-tESjqNzI2C*u*|1}dm{2T=B(N?(ci<TdD?^W)_tPC9v)GC;jrt-
z!JS;klkXp3UjAtZgWe&7eUcSLHs`)D^h^2dQ5J1I$>i;E>ggHQfc4)U{Esa*w`CMR
zvf-lmg1#dqb(ua#7Jct+<Nn^h<Uok8JyR#Yvjf`?mYMb|ww^lwEVRa8QSqL~(Z_z4
zTsD_eXP){0>_fN3O)d>;uZ}NR)4cxTVy+8CjE_Y8-Y6z*i<yxxHThtHPIHNj^8EV|
z%3EJ3edapwzoJaoq||nHvB5Ksp3ZBE%^8pGmY)rpBVit|{(6~@l(K)#Uz5t(w`P$=
zPjv3Q?KmwH;Zd42g;i5w3d?8vusj8U7cqylSk_FC=zJ{L7iSYU?eUsP%^Rl9O@1A7
z&9imU&cesVOH3X!T{4#YH=B)3!1GL(@x=#|C#e1WnfdVUg`HeCH60^0|9%VHt#Y;R
zl)o%*d-hffGeP+d2i43PZid6|`n^@$@1EqonQAt7El;zIo6B?7C!a5DUFXKXGD#|I
z+5w5rbIRA{E<32QJ~XN#Ynrbmlc12`<?DJ@nVvdf3`vP@GS?q5#w}I&{CFX^t!e$0
z{1bD3O?)A+?3h4-s$|6iWjEag)0VfeloU&5K9GOOpYZ6*rTM(d*PHks2uJ<l^mN&i
z!!*@~S6fu!`JL`dUW<D-IQc1Zc<<u$sXZ^MdxV|g-*fW^oO0*Y125h$pQBwV%e%q*
zS?}R<rDvut=ux}qVK4V`PZ6_J-HVgojr<p^U(l_dA=r~=_c2{`N~5^5bt3P)jLDB8
zivAh<NLBi0GE4t-=s&WP`=iIcwQD~J@GhEmdB<bUZw?IsL0rsoQywN*y|R64@wQS|
ztwC(T*4WO^%ilDmOqcQFKBDq6^SYf@_Hwh6C4Vj^$QPgBv3#~+rUH9F&fMzs(%(F(
zdYh&+&UEa4vm}{+((l6QZ)*GZ>&gFKpT1<xV)pceoy-d&R&YNv_u<elOqeQ=Q9Sd+
zhTeZ-`f}46wO*Y~S#*rC>&zkfR}O&^Q>^{2Ik?%JX`7T+6a093j}Nc%JB78EH|B?}
z;pF=vaY#<E_3aIpnFg}Qxl`Le9#Z97%3Yvo>*%Pedu(?^(5))=HBxVP=rFuq$enET
zSIVI0x>*``*HcbbF6UYumUW+um7GN?<4v?p3=TXz*0=bh=dyS54pvzjdmmJo^}4qx
z-?d6VbSSc`IN3z;eJ!)UZD{fewtEj%EeoxbPBMm-_Rr(A=|6C*{p582XUZMvFDrC5
zNCcf<x=Y&n$(m%oE8KQDD|0y#^bZ{0y&yhjuXC34YJ(@COB%QT_@-iLr|4$9bK#mo
zhHH;cx$gcc9cA}e==0={4^2Ejv`y8Mo^>VL_`O}spS>Fzp9iwq+-{k9us-|+d)|Y|
zMwu=vnOGTWmTxToJimhTkL4UAsne$oZs_f={9*d@lKRF@#=h+?7dKqCY%O<lw(a`!
zaKhOQZCN`X^c;Sgdxo**<^5@==VsrZ?7UFMX4MQ)ftOtt!eucF=ei^bHZ=U?_%x~Y
z%pYY=k^cu(JljO8w3=7X>OR_dYs&LgO%Ae)0#gr7zx4D^Oz*_*fFGAnC^TjFt1gjt
zDebp0TJ-GqnKBm#M!|NGAPK7&5e1&fMY|TYv8`X1bWWkmS$my=UZEL-`g6fe(a$r>
z8*SF*Y+;(lD=ake$0IF+B^)w04?E;Ie0lxHQCF>>b2XcppztUE`ZUo3Ep4gmG8=a8
ziG5fubCK(4g`fVTwA3S~j#bR(7W~V3c&E{kK&wYj5B9&F)N?X?qJ>Rcf0Rgv-{J@D
zm(u(F3*^o|I?T_K!tmhn@!jhVAHVtk_4b_U@#`}$wn@F8pjT$6*4D?l+n()*XWJge
z22KTz@LA0nbs~!vY%cizw2rs+XQYjqbM4|acjLr)F7h0+s#up**7b5;SVBybo7<O}
zE;}404t{%U|M=sigvzF;vurK)Kl@PlY2#%6vcDk;nqHiLj|koCbe{ezvG_F4oScfk
z;nPpe|9jY|vaDEJ?0m?Jt~myCcQC0Nu~;T8`!RjW%!)SQ46UQ5Jsudazr6C!oL4dC
zo!^}KOl=uK5|@_<8QRU~ImUl~i|HC?le#%)c7IaK_;}Im&1UaM{m;0+9GI~~)XCF<
zr>M=Xy(YqdDd|y?K|R~#e-ksT-yC?kIM-r9o=Ly3!%@Ec9b0-1oSId*V|&Bo12Kip
z%0XSqx+X?@elIALFuVUF`M5{(>EfM%`6|47F3p#&cbF8$bgfF=+pAQ|SRq+1H2#N*
zkljjaE&s14yQ37nat|6$TDWb^t?g_NnoSzM|9Lv$3dfhac}HY-+yA~3xZ_iCh(*7c
z`nd}>`(Me<5x%Hxs+?V*vj28vj_1+GB7c3K^sUJdS+1eybAMvcgc%o;&s*?5lXso5
z(s+j4RoyA3+!2DG^zJkrm#B&4I=yWILx1aarsji=svVtdm0vl#h2OVl+MHi3ki#P9
z^H`~WZARkV&o3V<K2VbpZ<yP5EQ0^NL;TeZjPmDKOSX5<-2eS~ck03ak!ryQ0zMh%
zY(2`d;-#dliq*W09&T)2vHvQ3=6M~MHeZXWCG1SlDgo`ViwO$_Qn-`(Qle%W3shXa
z!p<6Jd&q;a!HyxLwZ?#F&wRF@;vc3M1<icECdXs9@dvKgl1Ymee!gJI|JCQD!G-@4
z(>!yJ&-#9Gap9W{Rt|@M_(|MVaPL_;J#>dvo`rc0<N9{1hO>VkY-FnrNSt%2MY(%+
z!)!6`DLbY`&dhP1m7mC$Y|^f9<989)^p1efj*-lMpHKXWdM1>dQXN+Cp7E3G-ojr^
zMZPizR!?D6fBMp9^JDi~fr(Ye?OC40B#QJ-`I)q2M{v>!#dWhD+U`mH^yFRM&l`cl
zPm`DH2Hkob_``Q*!O6Vn?A>>Me7J2?Dr3IqVE@m?<e<8uGp`%w^dE5-xUhC*M$#Wg
ztvDyKtMlR}BpKB^dr!F{tUKA@$d&&|r^*tU<1cHj%;V}k#IJVHqEI|QM7@ROXI<f;
z-h}F3WeWs!winoU-=4S5rf!yw702yeg;!oBNR=<{^q>3Ykgm<=biWDta|~kledg#>
zb3MJ<JKSDErRda|sJ6d6Gv+t$<M&_AqLZ%iM&oTw(TyD<?Gbv`4#(EMHb`{*`OMsC
zDXX2NGOzCq-|wumdE$2IS9aNpRZJHXUYLI6;&HQ`E9;(YI3#v?-WiScWk*!!ZQ}M$
zn<!~2mL;ChlbyZl>4}@ZMc=J+i$vNuS8|^zGVDv3v!$MUZ}aDLvy%ooM@=4cNq5Ig
zIr(jF?k6d|^_G0*GYU;7ZkoXPL4O*%uh_3;hmAR|-xEtu^)5O0LQ(#T_=V-k4}AD4
zR@fiqzo@|UDEg?BS&P>ab(ZvP&2Lr|y03pG>$67AU{Bb(pLaZW<Ox6bO!P2a`DZuR
z=AgR&k6ssj&))rH#>vuMdm<}E)FxDRuFiTH!&4Bb@$tmMCWV0P1coDt0=<DR-$=3t
znl|ulP`c(d<*C7jdq1n5xANAgi)@tfzI7m1H^M}2$&tkes#86VOiWOo#n_slJTX~b
zX7-bfHR}4aTITj!sJrCf__*=7(woQ2WerOI99-cuZLhAW?~Dd#wxVZ=|0f28_?_Wf
zp|trzvCW*WfGv+DY>XQ1W%swQsb%)x^Yhq)t1sAE@A#Xk@9$cs&GjN`&4N}o4fgYy
z84^>@A8_BeOMh<&i|*0u*WVvHYAnf|w`)ViLlHrlq_F0D%%zR%0{(fhCrY?mUE1_y
z!pSO;B6~6R33i+2<o!*%W5Rm)oaqnEZEId;Hr9O7H~1peRz7($pXXGitVeB&1+NzI
z#y;FI`JwvWtOqCE7ds|D`Q;dMiPuJ?`=Q|rCmSP+>Zq`j^95gQv){EjSgdE&)cEAB
zcT999p9}rAbt<>@$9vVepU&@()!aNQtK_84&lXpcNWFunZ*FJU6tb)MWwM4llR@C=
z1Toih%6`+E7EfH5Dy>_gdpqr6@q-2Bj?Da@`BHAxg|qF965v#LKCN=8xyO+|P3PCR
z&-tL!U?aDxV8PO9t4)fEjQE=v**@-aD7d!Oui#|a8becuHNO?5W_a)1k!Srfb@zrX
zLH#*F56<ZAx;e#~TX!i}OxA<Xq7?!MoctC)P<_3(&1$p$&gFKyPPuiSb!+|5C{-b+
zZ_7Nr#AZv;>X@Rm=~n{2-70c2x)HlK<D83S;W3WPgMXRsd^mDg@=sgwq<_sa2}jv<
zu5cXp%RcgP>k5?$9w!IO&xaoOhVR+rs+O=O;(XvHsY?PvoU*A5%at}Vt^dQpqs=`1
zK|bq0F3TKukB!F<**tLkxofeeM!A&m2l0{&RY{fk+)F1dFKU0|S-fU~!LI&8o1Q*S
zw)nf1={WoI+g2Oze7jg~RdD=>%g<*^<qw_Qytqi}yMTDd&X@P5KiyZlw&>1}sJ%i#
zpT!s?WDBLv*dJ*Yk1u~I-~agVvl{i{nmUcm3}=_`{r!-$LxfetS6l1D%wK0GS99-d
zVw-pRL8ba?!?~OX)RP|kb(u8dN&EZLyX6*iiR!N3ds#_+;Reb4Z>;J2cJS5j-?LTn
z`7D!=A}^lIO9!5IfBn}Y$r+`f<5>~puTi6A!oA`qC$nc=RYZZAN#X8kGoo!%+2&bI
z;9uCre(Je&#p0=%zgg29T3s_gYe_5l7BHKBh*31&xX&jq=B`rw{T;z#GA5kPjO&)3
zRn~QTY;|CNj8*u#{qH0#C3ojV7m7`MW_qIMlimXNom~8<mIyw6b=v&h)Z2Eu17>X~
zyFKmO%L1mV#jguCo;)9aTa!IGQm>lr$sQ|biJDoTEM;99)%SlqSk!raQp~DVT$_%q
z(u_#ay?-HJ?Qr?G>z&b0Wka-nPHYa4kjV>pe8uTboT0Smxj!@I|Al6%Hrp0hbp5o9
z*;paK$G7JxxBKax>gTR5URJ#IPUr2fn^rw}xcvSk{XfrmE#;p7dNDI(LFbo<D7W_7
z+m|D99@a$7`1$enpGgmR^<KaHd_l?R@UtGqDGjaB67zWcE+1g_w?F<sarU8SdppEz
zE*H4*u2d2<{Sd(IdqMfZ--@Sht;!b;?fm(&{K@0x=iC!lU(Y>p>yShW(;Xx2vajDx
z`TFNgIb4wGaZy^8ZKjw%ugGTo{~i){H>xhhiLpG1+Ie(^V_Sk)UT=S+zm_2PF3Ae5
z>3kOhe(c;L(0WHpY`&lO!R6E6f1AsaUHHg<v7xiKNRx%-!k5#GFTG-{=H%Sb>t|c^
z|MKgUgKsz$d%bk0J<_wS+g9^&>e(XQcd{0u%bkmYr%S!kkd*4*^6A?u_Iqz9=*w7p
zo{Opp*f8gM(K{vEFK?_ekG>5Ejak1|yL{0@IYFs|l8M`1Xy{*G^f}j~XUY-(FTOGB
zWln5ua!^fdo3M4yH0=j&T%8|{=N*d)6aS&zbhmBd(;m?%@hsN3&>gbHA}^#)-n`s)
z^7^@%>hg9{<!lea)btv!8Ge_UxkYiy_3->@-RtYU`i}ezv*?ie%yprD$wIB!iWVQw
zW^7vi^i;#y`~ScFee{8C`qvbde?JACm;@&XoJ)|ZNbina+PC&+<ch~~tcn#6-RmXQ
zqGsyVT{$rMq(WcGp8M+<br*{6-u0yI{@N+}e?MN#YWdRCF~RY--$beJ4ioDt-+M*&
z9iBhUA<?Q-_s_qRr82Aae^>NzoG$1VKE%c-shYs8BWHcyyzN2coR>b=^kjcD?vF}*
zqWPhRxp9Thja8*Hik3fbzrEY`u#Kuq_$>|jxAP);7z{dAto5(hc}m_u%b(?$v&@1A
z0w*~aXFrwh&zVx(H(zygL5!PySYD>NeDdR~7Jd(A&$kLIE4Nd#kKY<REn&{|$Jh6?
zcCHP#+O$Zh&gSh0Mj5@blXDD<t}Z?9#rtTJ`T?62^Aer!xB2dVGOPXC$&bl*Dh!Wb
z=AL*mW;0XqrnK(9PZyVX|5jZ1D(2?0#^sCGYrlT8QL2Yc^`F6CwK?}9!<#?9xoDx`
zvR`rKF#{jjw$8T4O#PgTUq9Wz>~?C+%EhVAt{58CSWKUkv_a!W<-98sl=sT`X{}y0
z>FSM>|Bl;NxXfzU%=KCJj?dcHjvo7;9yH2ec~Tj*?x)YG{#I$Oy4mqUdk(hxGxOOt
zi7&n?z$Cf%%7NzdPfWj7UuerXwV}(+(_PDD-K>xhzDHBu-!?ZsX?j9^@rT-<jip9R
zvnTy~vZnRnTd!06$>$g*C29BE)OwtvH%rm{&fiHf|8|?slJj4pv+Tjq$*R6PW9-C!
zeVp{*PeFCKDuY3*fAX5HfJv?DOOLo6e#m8UIqc7efSb=HKQG+4@M7w(AM-B@#xJz_
zdGYZEH|fids;31<&7Bys_<+;ehBF}yvhGsOhm_@xP5pYZ|9y??zki$6Us$?j#s+aL
z=4HNXvdpor;-`@1t9esDnH!v2TfMvRkIlKO3tbzt+Y|3MIKS6Q{POSVn#fNpjm1x#
z5G;Loihq*JtsUq7rJs&F+G=Q_C-M4S=~S^llQ%t`e4@bIZ{EaEyLrD050{&~-;vq2
zBjb$a!8f<<Wt*4lX}&)cF;V=f{;6X=cP@SXbk%$EQ^8KbzYiw(@t%qn{kOvWsoDOv
z#m<MC8H$&z7gecjeL7En-7Ssje}8a(d2!cs(_NkQCnS!_ES$fCXa4+~8j+FlPbOOK
zQ(x&X)AnIse2~oHnLkXd8e7&|xiCw<?9F`=nzUp^`av<9gTYTkjz9d^?{p#PQLx-m
z%N_C4PC7`eiLdzber3knKQHs|PwBP(c53<gI0fP3{SLc08X7b!RQU@(Ph82vt}{R6
zipUfm%PDJbM?bNDU+22-;|uFqeCwl)AIlvV|KFExH$UL-j@Ab?5z8jBtoLeQ$iDi~
zb60oi)auulS60oreE5jKbZ5~pwvOmj{{0&ojtFEsI#spu*es5$d-L-7@jpDa`<3ga
zh>AL@&y;v{ylkTfbFDM;`#r{6jQ6FUJJh6ZSac)d+Xtzi%cqx}Sa>@8q^h_0Aql7O
z565ekZOmLI$lIeIQ_(V~@(fR9<yW)H%)5CvJC&DpmYL`+iZ{q@(V1n+w>B`w`^1x`
z)LOkrhJyxw%?r%!H%9t3+ZAu$@-nh#$r}IZ+2$_JkA3PMyx5?#qef2DV&7)}4cXKG
znw^raw|M5#{&PzC71=*8PtN)&py+J#s>0^_H~u3N6@3Kkp9tEYeB6=v?L!b-$-7%;
z>~>Zk%`SSUA9v`|RU^sPr>nE>tlZrY*k@7D%e>^>$@qPrFY}*oc~)zz^Q~vGLA|`^
z9+hK{TQ+c-tUUK|)7u99D6#Gh_govUFleeL&9LDX%jP@2XTpMmRff;lnR*taO8n7%
zZ}Mq*@}JN4^X_VW-?PtqoyAiI%a0dU8VTyIHoEt~X=P!fVWDcFP)A7PhHKJ0FBuDN
z%gLSUUXXl#zwHjUu;jhAAIldknf_8Gq-E9zWzJHG4)IIbdh$9CyINK4<ga~T*KwN3
z6ZKweb<(TK!wu@Z@gFXT%@tZE^QmW5Q_BB<pG}4px7vc{s0q7teAb*7eoFU^ufb(Q
zcX=r<5Bu8(q;($OjBnaE@sHk?Jo_Hcef|p+4P~aEm{WTwXU>xbHkN-g_QieSc{<B5
z*W}-^6FUw3sv>zVyZ$n9SXGnpG5V+g-~XxMr<ncs>54!8^E-GVTYmK=r*4TQ_lrcI
zvo>8ZoZ~Betnd%RQOEa+44QuwD);CL_pQ0`MfTAF;kDT@^*eLR)lUWKdC6#;maJA@
zYOV6(Uv^0Pfk_)94)?lOPkz8V``+aF_x1*@tE&;Nx+&r1wk6K&SW_G4=0$z_f4b8f
zXD++^fkA=qu>#jWwi%yJolW4Gsg^BY;Wnv{adODK)$3EG<!=>e?%~*Ez%t$Q+osk9
zTlW}$h<aSz!u!JXjKhaV;znnAH)Z>KH{Ab`zm2&#$cW$jR#m_Qy?<Y&i>`dyT6FG@
znq}U*h?yqa0@WVQNYq<dGC3fz$?EpGLpM81zs$aOS9$ift*3<7=TF}q_HKfD!Ms00
zGV!|wDsIL;yODK4-at#~JkPZm4N3v;nm4e?3#ReiV0r&1&f%PASon+BgZiuFpC^V|
zDj%P-<jryU<CQOe1TZr+KgxJsVSKO2=&aX-o!Jf#le`5In9GhS+r>snhDf!^OWPG>
zJ<dop4dLUzrL<J^;-=^ia+ehHXIbw1ZN*`*>}cxb<%voE=gf|qDs9M9d{MKwAV^b3
zxp!O8@oRfFPx4valYRH41M~4d+3*$42i$iheEEIx*K<p+`nuoQn|553RBLspIXhpe
zz`oE-h+p>MjD1orx<8&&+H7k|`)hKzy}snu?Z*bZtjFxzBMw_6R$08*{rl<L9g7*Q
zt9PzoT-{c*)H#an^vsx_SH4WyzHZ~DTz6@;1J_U4-`Ve0R{rq8!9t69Qcq`2)kvJm
z)i3gRCb!1|gC)`vCHn6h#(H#2y?%Pq_H++tfzy9#RlXSi*QsFnvf0opn&;P#D~o5;
zuyDR#bNI8h-sCq-PO^&>i$n_kOnuW+blPc7W8pHX%e6~;pU(PqVx5Wq&uFV{e!J7m
z?e_cb`}#v{X8+@i=lts@eKfd|T)^_tV2<kHkNe`byt-{wpy-mle49^L;_J`axwb~T
zm-#Ha5~?Am<;_2p^@Gk##g`{adRjQ7Ii4RjG7ztk(QC?BAn($}GPkjPBV+R^Z7mtj
zpWAj<zP#vRdF^t-3`6&Q4_31B)|p!Qbv>@D44C+AhUbpLD|Ro~em+~z`~AZ7KUp<g
zo0fg_oG(>yA?R%GUx}=OEe1Pe(*J#4Cck`fB-=a%7cobP3L(S)Om|Ht*!`H>>G|#a
zy{%DkM-0v^KR-j6-B*@1x$jZ)#-z2k4=_nd=;Vh#4`4mk=Eg2wA^hzvul3Wm-}k4i
zo_||yd2+hR*Xb`aoez1QQaqr4x!?L(S3;lJH<bg~pJM(`N;+bgvM*BCFt+@UPG-tY
zw!Hp6s}JR>=idGQX}kJ~zI~mAn(;*bki5<#sR8c~&pzGE$KBld=lHw|_Pm!-n=`lD
z?9J-_^QN=>$;H^YMMhFdkF#T(dy0Z1)t9_6Irvdm(c+cs!HbrRk66!q_^~jN`3L6)
zwxZK+2@k~%<$n&YeB8{wH1lW6nHbgR9p!O14k#<8$_QO>Ss4)0(lnD#X~H9wgybdi
zX+B^7O5B&>?67n`>^!G};VR?d)2Y`uwl7N5)|(b_{Z^ay@2Emgqv^>Hjgnm+lukD_
zU@)DrcYcT73zIqTjvJWVFzobp3D9<y@xDCesJb&NL%+(jBa41tWcxq2vyp@A{?<jA
z8M?}@D&}kkwr8ptxGi@pJuAA_f5~24^y%sBvXy)#g}ghM7OQgJD82ptlp{xazdLV%
zpyxEEq!dHXZF=d>dF$6y`)g^NFEDqDGFZdAGw=S{&66E0Uml;l_Ls^{i&i#PF%OoK
z2lKP6AI)@3^{(SA3$oi#wf)btcK?&97H{4iVHGymX~A^Z{Hm4CfrZSUPFpIpIu)K+
zwpDa{&)&_^`b_^h+eCsh9OfKNl(d<-L+@oumtzRObHi!dGxPobO|*J;UhPWe8t+2U
z7rsk&II*T|c*wTU@)a-dJe_dv0Kvb?ZH^UxpB|OB^H5u$YG06kVzS`}7vHccx-WF!
zHprAeytY16y6p7i{I`>=&9|NO)9H<DlD>8BNTuBq`O|Cf?sLuir8jR<?d{1M5@o8|
z<SWb*Cn!g~U}lhS<6wKBQ(Jv3aMu2X&&*G1Y9E%cNl8iF-EmljoBv|M7hblBmL;xt
zx%hs}dfTJ<(c#zS^YiL_g1zMDKm7Qx>3hX9-Xn`PpUF_>;)-tndi<+}>;*#&;mKSs
z5|fTp#LQf*!rZdcWYVJ@Z>|5CocY$%zCZr{vA8D+0US1`wPzk>Iv05FX8g_gur@Q*
zWQLhxZ*;yS@a?^jclp$Z`QbSeroWF}zSjQNO6CLYuTH1xOxxZ1_>9;#`FTF&Y-X&n
zzfV|yy7c$8v+~J@GheRQk$(N)jkIZjJB*|*9Ngm~v-!L|x4~a-9^2376JDKk(Gt1y
z-<A8%Z2#QJOLurAecMqr({5YbG5+<_*uKa~)atkKZCm(sH(xiyy(6l(zwf=RDID0t
z=W>41Lz8Jw)?eL!M85pl@#PcK42~R}X3iWj^Hpg{RtHDnqDIlWOB)VvoKzsXNSk|_
znen-}V@eV~Uk6(LO?$e#=*E#M9cP!<6J1&xx|W@ouQ2JTs+?6#c~kz|AGdEd-s8J=
zWdFYH?rIM6E?+FL5UOVJNawFOuDWv7{3nS5(_iqY?&Z<F|MHK)^T&Uj>i1a0)O<{u
zeDl=@lgAI*r8hC!*}myI=xupqg{b8-C(o{Lw=T>$I>SX`-s`0bF21IIlU+JpPqsfb
zSyrUOk)n~xSXtLLRgvSnrm31_vqzwc&1{#`J6eA{c$V&e$mq_a4|o5Gs0qzXyTd5G
zC%aQC<y!y26xNypHYbwiK55R05QuoOTI&yAd0kWc_p4vtuY2LK{L7)@_U4Kk`Re=~
z^ONQ^P5aEa<432?*Pq8qkJmDINadZFU-WXJ+v$`GMzU@5LIpCHBtJbnd(jk!Tl#yV
zBo3SE*EA-}Ii<5*vT>g4%JAuE#hQp2&zTd?q(83JpS7cZUGCJ~_wMM<HaK}h=t>1|
zhmj;N&%DK#8VY|-Haz0I<;ldb2FIt5FSkCJqsQld=|<IC_wMaH$F|A5K5%zSk)KE;
z<BPisBc>;QT|Ud}s^p)H*1QAL^m_j|o-kH7oPT@E^koW%E?exWeO{|o<bBXF=<W*p
zt3PHpDqg;M$FXnAmiAut@1iTt&CC(d?NXe)=;!Co6_Mu-{bdMd)Us}0y-6u*SIsNy
z&QFGKe(%2cR9#-J_1em5xjg*Kv{rL1n{)d>d}(OZtl3NVtY6;lEWhWx!QJzL))JKl
z^ZzT|@MILxdwhbS=4VJ6)7@x>q<eKapFhucdAi$TkNms+zYG6-PfDoy!T-zp^JRYF
zE7y;&{W_y%<(fkiShvr8(DONTHCI~s**TJXldr9PcP#Q`gyN;vrasQCBI+xR7lj%=
zZl5l<DtIRQ3dZMrRvabw6TV$G_VPBVwtATz_l-sN-s+&E`JcJJp0w%7Q%k9D?928S
ztjpN&+Ui|l#eC-t3VekZ4KB`D-FV2nx{uG7A@#sCKTZD!uMTIf`YUn$`NsWICz$eW
z;oKa+v#RUWt$qLGa*|S(wsbjpn{q5+>{V7;Y4R!OY5$?B|4!?+tYN&>EwJH6=#?J@
z_m^}h6*S0IC<d9_X@6dAQ_u1#@lEt(=Y~VSCo)-?h$+7^XQ+`-y6L{$<RiP!3-?N&
z<-ZHgC56tKUOPqH@bs+P2ei|C;;)8n`BKiY>dmXDc_$AZ(hpGUySZ^&_Y?IqB_`qf
z%318Vmhq%jOehg4=b1L2ZMwjh_Lr=xFIs!5s;e%Gie6o*b>-7k(WllYdzOVif114a
z)9an*<t`Q<+n!fFU3g0E-MKGKcsQo@I9z+PF*V}Ubsi&qhJUvn^)sa??d#7^<KR+#
z8T@{~`Y~nU8aEb)C#=2mkBjJAJ+_F|ou;N=bng1Rb$T)G?2mamX5C_ws92Nf|NX(I
zi-*=(GBmEt(AHo7>h)tkH<No23yX~`R>vF<NK29D{$N)taY>^5nfRfPM=PXRUa432
zv&pz`;=g}%!I#7@vi8r!FZoJ2F$td1>sUSUTjQ=bD{5=^UTU`1Qdm$@>Z|*$EHuf|
zk&D%2|LNQZig_-+cRzmZ-!ixO>s<ZtYkbx__wQc3fB*8`d)6?m-Mz}{Nw=Hbq)=bo
z+v?6Nk|7#*7WB^iX8XnGS;NOI(yjY87wdmn9sf$YZQ-)@IWM(WS2b?T+xyhX>|)W*
zFO!}<>k>VCcJI@tQ}vxH{a(J!Xl{IeaMC_M&DCvdE_N?A7OA<lo9%~vNCoc`f4j`z
z6aPKG*L$d<?$Le4*2I7JmcNnIPqg^4e);Zbt8d#p`So_MT(@rOuPPpnugRWiR$oOj
zbE-<)Q#DmAKV7O3Jv4jicBQRLjY79tPhFS$>TScl2Wp#*w(#sUHc7vy+_9%WNr@%o
z=YoH`+j)Npw|q!+_*pF4xo^K+k4UxKr9l5bJd5fCRKLfTl$XDVSCxv{TFNU^chrk1
z^7NPdx%;)|K0f#M&*CrMv*fknFV+O*ySn~7`*iA7_3vd@zItDu_vzm{KGSzkr`}+h
zx?#4#yvkFm@7xb@S$988{=wj})8OHIW|uZ|nez9pZ}08f&f2;^c-5-a)za?0tB-8-
zKmG2<v&iV#vuB^46?}tj`teBa{cCo;3je#eHaslEe9HHdcfQ|C%NOjw*Pq(4RpZYb
zg_PfV9@f7&HXMJlm{qjF@V$lRzLv*{zklDhn5jMYNP+SVp1^e{njgLAv2IV^rTP4u
z*&XTIefJ`lnwa#wSiM$0?%w_Dn^%?P9p_Rjf4x@x=~UAv)5GRw{Cn|k^SXVHFMfIz
z`26sW?}-`fmF`|%D7^pa0bl2%^&<09r~jy(e)@hp=Y8d#l8VCydt90hGyI5Zu={y9
z#6IGj$C&_D`KqjjR;jz+<~E+&Bk4Z(%<rn|rJHNlZz<p6BxA9C`M!nw^KNt$y?kBy
zZTo$z>b1wR^Ui6$x6!ST(Y#wT$xl-ERo$=U`ll~WzuGHRopO9#Nx6S{b*TSyxhp!h
zGwvKz(c#(`+{QC=qWOh0oZNk`X)#Y0FDPeAc%l1*A*$rfuF}IR%1gFnck`Lny#FvU
zSz9~kuk4B$``;$4KeX7gXWAF0#TTyMnWLBe@AVa9`JeALy<UCXXUCf4>(k!N>-*-#
zbA8E;S<m?r%O39ZYJa|9HuqK0I6qzE)JX<&=Beyyew?qit~ymB@sEJ(u@~|Z;?In`
zm0F(gooUj$$-L&l9j|=<?NSwCFIF5`y06Sdp3COht%9PY@L#jH$CU)$Z{2<;=v?|j
zlepT_c|kEVz5WUu=6W7}g-_di`+LvtUrQdY6Ld-6>6UHSJ8$;2#L6QJi@050-4Lib
z(ovu+-r~XW{m1jY#|%CQFZ{_U^k`3g+{q=Xzn?AE;+6ce;7n=hw#DK1`tC(Wy?WKQ
z^tH6q<<J=c@87=sulQJeQu)CtTQ8U||E2$9H+z~#<o&L$Q?oSR?%uvou>bLts_Kgi
z4zID^{XXMnYBw*d`G=BYcWYZ%?|I&NI@xhS8~>qKR}-a}l-+of8U9~!wL9~f|DET;
z#W!2K#3tWQs4oqT&HAxo<5QXbqaTID?|l1eTp#PfsN_?;-FC_P9c7VUmwnq*t(Dz2
z_sYdhu~k;LtAFp>9ea>JW!a~Y${7JM+WnLJOZ+z8X*bgsaQu5F%3_1VGC%(v&t_fz
z@la&`vZn@;KiFTsd>&Z5XTFE3c<EKCX|6?Yt4ecgcWv7?FSb;~eGU8jJH=Pu##_J5
z(q4V^(}@S?f1lfwz3P?J`kefm_paaVYm4ST_GBfu<4r!5=P9YIRu`BriS5bSG-c~4
zf7gEb+EvTtl-D?PID`p?EidCtt~kuWCHd1cW&NvQmN(7cCoVZYP4aPnpl|(;jY8><
zdsi>HFx%_;)ob6cUo~GQ?PeBQ@-}zp!|V06$Cih<z0=9>p8Iu6$|k0oer|o2)eO3O
zxcBd`5xV9X%br|kw)<7i(eFu%+D+|xdr!F;FBUqyTziMkmtX6Sd_I%Wwz_}wGanz#
z!jE&-Fsn99&-;-!;n?HJ=ML`rZoeh|iEP)|`Z)qe*X+7-jsI|G%?ttG@9U4u6b--g
z?JECzgPl_k$zCtbf46_bPca4AkNz7@*9S(%MqljycrWgY$PVe?@HUB{spfW0KT|@w
zgwi&2$@<q>Tkh`LzmUU8B<x~@1KZS}H45|ld=}Sy=nV5bd}CU2%^t3`U$xG32E5xF
z`!@RErTsszhWr1Nlt|{3R&@Q)^*1a0*17-hHr4B`U-fqqAM@MH#x>R#>YPtDFD!JG
z%J_K5C5CB=ZdGh!!&Q04#Osa!qzr|dSw4E#FNj!kVe6;x9zN~n&z8OOIVM=E2>xk)
zFmrLyqX3@&JG_>yS``*Bb9q)fulv)u&UsP4^@A>#$FJJEWr5=~eQnp`qvm4bv77&}
zoOmKrqWtXJ*Kb#r{;oQ`K;pnt&d{e%Tb^aT;*tE4dZ?!8`-<X+-E~Dv!fP3pc;Ay*
z#qf>)hv2mvH<X%9&#bwteM)Qh#ZA%es=fR?@^*jB|2JMWP~Cbb`HhLP|NH*`kN2`C
zKYUyH^52!j2@>m+k`BJRJhe3N>B1vS)1AZes%MH8ZRg^yw!QeXV|T!>j}8BA?;D(G
zeje~3kmH0QhirS>mwe~uSAji??)>|F+W)TPiSC&52Y=d3sc?JLv_HO#@7$6<To+_`
zHLtI#b>p7YYyLKn{f4ffonTk|<rbcXb1#G&*;xM-8vR-Eaf8x+-KQEBHItbaCH!xW
zk9<;jY+mB7%HG2Z-?)12lKxaLH}&n-?KN+=%=Xw8@Af%WS$l5Hfvzd9A3G~gZfp};
z5_JDx8B2VzK+bud614@E=?X>%x3tB`@ip9iSmDN&6W>$a!TM>>hegq+ZxnO?ZHu!j
zkdY9HOm5?ODo~%NH1F_6iPE{T)BLV4oH$SOvZcwvJ>2X2zTXHJ+91AuO87FzNB8=-
zcr85L{&hzC+bqY9&qpqp-*%b%!g&3^t5cWnTiLi~!b_o?4Zrx0@lWN_&e582CgFkf
zp^fil7WnAxQRU_36iK)rsKwTIdDR-<jclCn1!grCC)A&8v0_=(cIwLk*Uj<CY@akW
zdk+dcOL(Bs`9kr54&R=5TiH`p0#?@|zwlRzJUj4PHTmto{Z{AKZqoF*CUE56vjcxZ
zSMOM3YSp%Pzp(5f`y-8td_08-9n8)$5|0iDu(w$lP$2X_-{Ql62K6ue22y<Hu?!3h
N44$rjF6*2UngHq^v*7>$
literal 0
HcmV?d00001
--
GitLab