From c2711f4acab84d2d5f05b566b26a0ed7fc4cbe66 Mon Sep 17 00:00:00 2001
From: Michael Leuschel <leuschel@uni-duesseldorf.de>
Date: Fri, 17 Apr 2020 09:14:47 +0200
Subject: [PATCH] add slides about proof and laws

---
 info4/kapitel-0/Mengentheorie.ipynb | 144 +++++++++++++++++++++++++++-
 info4/kapitel-0/img/Venn.pdf        | Bin 0 -> 11740 bytes
 2 files changed, 143 insertions(+), 1 deletion(-)
 create mode 100644 info4/kapitel-0/img/Venn.pdf

diff --git a/info4/kapitel-0/Mengentheorie.ipynb b/info4/kapitel-0/Mengentheorie.ipynb
index 9676745..3e5d2a5 100644
--- a/info4/kapitel-0/Mengentheorie.ipynb
+++ b/info4/kapitel-0/Mengentheorie.ipynb
@@ -545,7 +545,7 @@
    "cell_type": "markdown",
    "metadata": {},
    "source": [
-    "# Ein Theorem\n",
+    "# Ein Theorem (Distributivgesetz 1)\n",
     "\n",
     "Für alle Mengen $x$, $y$, $z$ gilt:\n",
     "* $x \\cup (y \\cap z) = (x\\cup y) \\cap (x\\cup z)$\n",
@@ -599,6 +599,148 @@
     "({2,3,55}∪{2,44,77})∩({2,3,55}∪{2,44,66})"
    ]
   },
+  {
+   "cell_type": "markdown",
+   "metadata": {},
+   "source": [
+    "## Beweis von  $x \\cup (y \\cap z) = (x\\cup y) \\cap (x\\cup z)$\n",
+    "\n",
+    "Lemmata:\n",
+    "1.  $x \\cup y = \\{a \\mid a\\in x \\vee a\\in y\\}$\n",
+    "2.  $x \\cap y = \\{a \\mid a\\in x \\wedge a\\in y\\}$\n",
+    "3.  $a \\in \\{b \\mid P(b)\\} \\equiv P(a)$\n",
+    "4.  $\\phi \\vee (\\psi \\wedge \\rho) \\equiv (\\phi \\vee \\psi) \\wedge (\\phi \\vee \\rho)$\n",
+    "\n",
+    "Äquivalenzbeweis \n",
+    "1.  $x \\cup (y \\cap z)$\n",
+    "2. (Lemma 1) $\\Longleftrightarrow$ $\\{a \\mid a\\in x \\vee a\\in (y \\cap z)\\}$ \n",
+    "3. (Lemma 2) $\\Longleftrightarrow$ $\\{a \\mid a\\in x \\vee a\\in \\{b \\mid b\\in y \\wedge b\\in z\\} \\}$ \n",
+    "4. (Lemma 3) $\\Longleftrightarrow$ $\\{a \\mid a\\in x \\vee (a\\in y \\wedge a\\in z) \\}$\n",
+    "5. (Lemma 4) $\\Longleftrightarrow$ $\\{a \\mid (a\\in x \\vee a\\in y) \\wedge (a\\in x \\vee a\\in z) \\}$\n",
+    "6. (Lemma 3, $\\Leftarrow$) $\\Longleftrightarrow$ $\\{a \\mid a\\in \\{b \\mid b\\in x \\vee b\\in y\\}  \\wedge a\\in \\{b \\mid b\\in x \\vee b\\in z\\} \\}$\n",
+    "7. (Lemma 1, $\\Leftarrow$) $\\Longleftrightarrow$ $\\{a \\mid a\\in x \\cup y \\wedge a\\in x \\cup z) \\}$\n",
+    "8. (Lemma 2, $\\Leftarrow$) $(x\\cup y) \\cap (x\\cup z)$"
+   ]
+  },
+  {
+   "cell_type": "markdown",
+   "metadata": {},
+   "source": [
+    "# Gesetze\n",
+    "\n",
+    "Für alle Mengen $x$, $y$, $z$ gilt:\n",
+    "* $x \\cup y = y \\cup x$  (Kommutativ 1)\n",
+    "* $x \\cap y = y \\cap x$  (Kommutativ 2)\n",
+    "* $x \\cup (y \\cup z) = (x\\cup y) \\cup z$  (Assoziativ 1)\n",
+    "* $x \\cap (y \\cap z) = (x\\cap y) \\cap z$  (Assoziativ 2)\n",
+    "* $x \\cup (y \\cap z) = (x\\cup y) \\cap (x\\cup z)$  (Distributiv 1, siehe oben)\n",
+    "* $x \\cap (y \\cup z) = (x\\cap y) \\cup (x\\cap z)$  (Distributiv 2)\n",
+    "* $z \\setminus (x \\cup y) = (z\\setminus x) \\cap (z\\setminus y)$  (De Morgan 1)\n",
+    "* $z \\setminus (x \\cap y) = (z\\setminus x) \\cup (z\\setminus y)$  (De Morgan 2)\n",
+    "* $x \\cup \\emptyset = x$  (Leere Menge 1)\n",
+    "* $x \\cap \\emptyset = \\emptyset$  (Leere Menge 2)\n",
+    "* $x \\cap (z \\setminus x) = \\emptyset$  (Leere Menge 3)"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 31,
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "text/markdown": [
+       "$\\{1,3,7,9\\}$"
+      ],
+      "text/plain": [
+       "{1,3,7,9}"
+      ]
+     },
+     "execution_count": 31,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    "(1..10) \\ ({2,4,6,8} ∪ {5,10})  // De Morgan 1 - linke Seite"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 28,
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "text/markdown": [
+       "$\\{1,3,5,7,9,10\\}$"
+      ],
+      "text/plain": [
+       "{1,3,5,7,9,10}"
+      ]
+     },
+     "execution_count": 28,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    "(1..10) \\ {2,4,6,8}"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 29,
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "text/markdown": [
+       "$\\{1,2,3,4,6,7,8,9\\}$"
+      ],
+      "text/plain": [
+       "{1,2,3,4,6,7,8,9}"
+      ]
+     },
+     "execution_count": 29,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    "(1..10) \\ {5,10}"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 32,
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "text/markdown": [
+       "$\\{1,3,7,9\\}$"
+      ],
+      "text/plain": [
+       "{1,3,7,9}"
+      ]
+     },
+     "execution_count": 32,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    "((1..10) \\ {2,4,6,8}) ∩ ((1..10) \\ {5,10})  // De Morgan 1 - rechte Seite"
+   ]
+  },
+  {
+   "cell_type": "markdown",
+   "metadata": {},
+   "source": [
+    "Gesetze von De Morgan:  $Op1(  x  ~ Op2 ~   y)$  wird umgewandelt nach $Op1(x) ~ Op2' ~ Op1(y)$, wo Op2' der duale Operator von Op2 ist."
+   ]
+  },
   {
    "cell_type": "code",
    "execution_count": null,
diff --git a/info4/kapitel-0/img/Venn.pdf b/info4/kapitel-0/img/Venn.pdf
new file mode 100644
index 0000000000000000000000000000000000000000..a95d99be94cc8c7f2aba5852085a15e7f688d7d9
GIT binary patch
literal 11740
zcmY!laB<T$)HCK%J@WL^)7Q&CFSu~z7?+8HfkJ*#7MG2Ug1%2`UV2G}f~kUmLXd*K
zTV_s4YLSAzTTWt0s!M8eeoCr>ogG(kNl|KIE>{I(ZRqJfVMBpEzqNmHw4d2^d;Q0$
z9Eyd}sVa5}E)J_%G@mfl*gg$Ezkz>BY;Wk}tm&&y&y%*j)T>iB(YAHYi|66Loa|pb
ztVoY~f21US{(k%E+b`WKnxDw^eO0JlY0Ar>o#Max(q|W{SubS>t6i|8*r;%pGTTPJ
zGgJ5Y27fb~<YHafSLu9XspgqJ^SCFOV&CS4O%k~Mg?V>W1F!Y<XWA}`rHA?|A8b?l
zW-NAN!NNlt#TiFu?P^GWx2T=VHSS&EQe&GRJ^z<Kd-gG8?WPi|Mamo4_cK4%U#!nJ
zdw0-;G=aiAYmK(s+g41x^4(IPXy@#OHuHB~)&6;*mv>+E+a;3OA`>snSt{EfJSV3?
zZSA@aEeV^&Ru`Yf&5c+h8o=7M;+*XJmIkHVa|+$tQVO5*ra#emo^-aob%_Pr`42WM
zUXwevPRrbR>F}m0GxXA{zW=t>^?&yG(yD7bw>8;kCv$kD@XZP8k>IR)9;ByjS92)v
zN7?d*ZQmA@Nv~Ji_1rexrFfx@FaMkQyZ=fVJ^rwZEn0EXPV<E0BDbX%d=-^^X@2VR
zorR2x_srA1x}ZZ#)+RV<S8>h!V=XM9)+~ZL>;jo{RKF-s_?5<%wCAmL*gW?sS&dVZ
zKE1ue=CV%ikI{-ejYq*NPS22CFS0iC%B!vu0R|Nu9@lp+n!0vZqRh%D2T_ehR^@vp
z9xM8O)kH};Xj7qaRg!J`5~DqnyzI~BKmFu?QZ-Z0`_^w>%XOY>o}BWMd%ks-SWI4X
zk)cQNS@-L;G990{{mPi4E@<VodqU@tT&wdtZz|N~ZPPxq!}!&ggU)INe-D^U&kVUQ
z5W2wTYUk_9kmJXfaha`3P+0%wy}e}5yxHvS0rM2AYHWm#KXY3Zy}i=eqP%{J#>U+p
z0Y@&}DcHCAbKERxW<~MG1<sX|cFtUWRaBCz=TnHro9mz0@35(U-IIAkVd|=ok_T@U
z^5*j$7n|>Ur%-?W@y_ikv+DCt#77Is|7Y?PS@fMNH7^C4+*9*XK)D2zH9)kvi2+Cw
z#56+6Kp~X{sS5f5iRoanC^fG{!5EU6f>Mj~ON)|Iixtcu0?zq)C8>EO#R{Md7^I-@
zo0^iD=#*cf5N)7fpkQWbqF`!i9?PX4lwXoqlB!?;%6d>ofJ^|{49c<rMfu6WsU-^0
z3i<&qZVLJ#sTCy(u?qUm`8oMT!3BxQsR|%v&c%ib=1_}^jT9_kOk)L05R=Q!PC?(b
zqQpHIY#B(0d$FN{p&>|8LEpXDNWl=~&ma)nSiunDDUc?&{Javd4Iv?h3Wgx32Z0Q;
zvx5Z>*bJC!A>o6tNIyAI!9dT@(98tMdtjUJ=`ciA3~~xS#RhtY<|gLIIzRyq(*Z5<
z3_<Z4q@eGoV5p$)2rBmSK!L9Bl3JFToa$bbSV_1zYz>XgkO>vB+g+T_EW|Fqg;#e=
zvwbe-OQX&(;qI-seRp{ZZ-1Q@JX`BjNtv1T*_5<7Gw-S`^k4d5wiwIH)eG#7HF0dy
zGSmOIbm`GaUZ(t9f>AvR8nr<mtc`D{lsOt5p8NCN&gb*0&y~O1Ieo?J{JWpuZ1FOA
z-cq-4&TKo&TCcaed^3Yq%>MAg?ZH#8rJTq5UeEZGUoUrWsfhQxH|f!DlcT>qStTiP
zVOQI;Fy`bwjirLAS#8hTU1Fyz$lFL)_2e_#TSjX>Z@k_x^;(QW)v5%mW%-g>2d|4?
zne_gej`hpeVUKf?Pp6;D+pzx68@JbdY3j#6zHdD*?vtJ+R3ZOi(!zd&cg*{4Z}AgJ
zp5s^jaAMJ#`RB~imKW*%JUOerWR>dvfcze#b3#j}i@ly|-Y}mbuGCMwfBTo~>30ja
zU3OOaD&hD~<iq9zQFmn?+pIhwdS7?5-RZ-tENz(n7=2LHmRZekc;6T23v*H|H!L_>
zHSh0{D5YvQ`!J?^Y&9pgaPJX&)6pe9?Zz{O4||fuD|L_P>CJW&(N7Y$Z~b~IV~zfD
z=lzF@=c`Tner3(#<O2^}<ktRPtkZ5^^y22ldsTuJC-bLRezQH0y~{p`q3!IM<j~p~
zm35324Sq{Xj7~1S{6p%=h5a4o3f;2=Kb<%p!CO0<>q5bWnlC&Vq75Zc3|gvNe7;1e
z&s!WMYCAP;QKVzbjZ=SD<OkGUUw)-wi{I-B*Bav%$19z*`Ri5u;<;jOLe8?od2(?U
zTR8Y{2ygqjAoa57?N+sU?$#P=N3@dycqVGaiMAhAG~{_X!9wC}=U)F`=j!ZkZ1|#g
z&G*+n9zLfv>4%Nk*A$pA+WcUDea>wb=Qh1}8E-!C>Az?Het)v$cDo;&d-pQ@GF0Dx
za1nR5n(DJS`|rN~hn!1YYrbBa`|kDg7Zpa{f%jI;jhuA-$?s2G`@TQ9x`g*<dZp<5
zz1w1JPjUaByz{K0oAso#j^}J<2W}}mCVfD0$4b}YZ`&h%Hoe@Iv?bxB)0DZZcl<xi
z`T4NT_KiWsdhb5$*>0a~cJ_N0e|O0~|J`fWX3x*C&#KSRzIEJTzqh<syw`oN@FlA+
z@dho;zO?Df+%J2-?EGR{74NW1C-&tH&%!s-yV>iGRbR_^YmnBqSw!ITp<8FTyyZWZ
zvn9{|X}s`i9P`}W^~t(VJ2nMZx=DtWX`j~=_F7-$V7VqIobAG|se!5bZe@8JQj%@Y
zHMG`GO7C8#yzY_B#_-Y&&kuXczF!s}bNE`D=?za?zIiuqE#q4+7`|ULG<lD8>>M^L
zU&W;Eb4o?>R&(UlSN%J8GiI`dX;A*7DI1RHUDQ7oWjaHcJ)re*?pKQwp|d1U@}w6n
zNvkq;p84;L;jzFq7k^H=*?m#5#$D*1@oB^VvrUhrOT3qTwt_QfaeK73$@9Ydf=^@f
z4{lF;wa{uorv6IHnDxu7o=M!a3*DY;D#aCYpT}o^X4vK<<>u#=f4%<t!p|>vccRIk
zG@ZpEuhcHqZ||RM0xC*Tt08cC1uDY~4Gqme(jYddd<W6d3i_VT&Q6KNsVNGEpu#Rl
zAr_{_5V`Jv6@DO%;KI)sOW_yf?nJokn>(#MB>1LS`}w`*doKtnDX4yts^V0*WbGl!
z64>e45Wv*dqE_a@>Lwzn8I}@qfYH5ODcMzoySXXpI_D>WfMW*(U0k2u?aAhRzt;5g
zy;*;cN8Z2reEapA>F;Z=?_vn})5LP9B!aQQWMPEJyVnO}goIBY`OYLEz{nTDc;I1L
z8jJf67p5zJ_S(*zxx(Yv=5O!x8d7%O*4ZDRR($P${X`{mXB9REF4wDOHg#&^Pno6!
zZ$2t%^q=L_m#LaYZH7i-3pp39QF?r2ea^S#&$M@+oH1SP$wH~fbCP>Z=Jo6jxHn7n
z;o=^ag)uW!AEYm?VNcx~;yH`q>35CGmw(LhVK5Mx8Gq)v+QOVpBUcg0cb%V@7&xXJ
zvD{O{*ZtEnV;)1rvh*iiES;W7%LK2_$b9<ZMB1;9n}dHQ8EQ{C?EA2z!sq;#Ej)b&
z;tlKbr@1n!M&{1UnD}<B%-gq-*Pdnk+<)`FTwU;A+Y?p4LqDp$IX};_XI|v}oHuLq
z_lhxmQ;C`_yLsQ#P=+nJYz|K!uJM1b!0?HcVavTapXJ(e;wBw=#G}sL{pL+hG2{Gf
zJ?$6fzvnmQpW5GM`F-Z;cfZ4|mx<dqDtn3=r@B5}wtShl%b7DgeACaT{QWNQ|M3CK
z%(EvC>&%&dK>TCti_pLqQ#e~XGj_MyG)7F&OW|s%zxuFV!c3iAvTkm+NJeQqLv5>N
zzz$FL6Zy6b&dSUxdG=LIwXdTE47pD1+mo?&;`-u#qpE+;f5~&lbmcwtaa0O^_Kl}M
zrAT#=j^yI|Ejb67geI_;EZ{O})H7hxN#K=fFfL%er@+wC;32>~jakowDbs;vlcU`Y
z1};a#8;oVmSp^JN8mlg__%)dou*I;1AK)$E=4o(u;A%VQZNPZ1F_WX|gMjEF$5j)=
zmhjJXx+WkU#Zl?(7+@j7eAKyfg1{t)pBL0tNN6>$TId{L`$f4#Y8OXr^RET$7Zgm`
z{xa6K2+m--oXC5FVOzt^4c0Oo?uSl4aH$ZT!!CZ{_Cv27Vs?Dn4~ajN{=lHq8h>aq
zhr<aD=8J9-9MT_MoF+u5FbXPWPgGjMw9<9f1imHGJ9|AQ7CvESYhRc+LqhDB<m2|p
zo`*?ciPw_646e>do)P9F{>&^*z_{^e)6%4?8<$0>udy%VG!vZNt9v9Yp+6yd!}N{J
zHxl1i%kUjPAo)n9pl*jmj8UHHI+pGH*L!w1ygtnPQ0-&I9<6&K@0<7!7Jo>pQQXH>
zFH<jfzhC~?e)S2QQ7qX_{EE{QRB}{81f)2gbNp=)JY*8sxWd0gsZF5rNKBIE#=aYl
zdpu>-{3eTdwyB5*sc6pJ(iq~Ir4*}XtF~8h@=2={_acc%hdBRrD)SZMRrx2`2TajW
z6Y=+wado=sXX&-mq0*t!d1(;uio7ckt7hz)8|A;(rPixf-+i+2^v}~DpIke6^~CI{
zucue5`cJt&y?lDS-hB0V#d@!Q%l_<O3Owj=Ft~B?hOmWh54Rk$ZS{1WwP<QmN7AgM
z&ZOo?rbh!+_e^S>v|Y%5rNhe&msFQ3N;zF#T6t;57T+yaw^DBz$hw;^`F(lv%cEc9
zU+n$DnW~x^{Z!+r%u}hSn@<I?9WqGxVH_m6v}bb9?w<b7CeL=Be|-M7+4{`5|9dp2
z{?y9Ts+p=ZHEk;6)c#dIq4`%uuFhSRyUPEHL6%xpV%E*9-&gfk_nu#VzI@*Kx$!3d
zpZsZmwP9Ch)sA0TUk|^seKlEXmef8eNvTk&=_bcaC1>T$Iyvj<tmh`jw`4?dZ)J&k
z8uff@oWazY@6Lpzsc!DJT)1}K+vU0!?UvkKZM!yk#pa0g#eSR53CB*-i#B)M9<x2T
z+{xctKSDo#ec=0rc7gNP&R??MeSdWQsRI`jZY6X(&OW$eVb{X_iSrT{KTK9$HF5Pt
zt;JD`t&dqGZ!7HjX!kf;ZA0f=&q<!WCw+r&T)7vLu<QJm^E}zlGSo~~o9;foXv3Yz
z$Te=)7FZs(IZ?B?a`sPcZrkpN?zv)j#o~3|>ICb)){&3YjAV_--STR~ufw;F%*u{U
zu07tC^*DL+xn*~sZC$%k_kP*_x3$)@VmI6s+wHge{5QUDO25^98?xKBSG4ct`+lRO
zOk;OT?N!0oFCOkV_p#?OyLz?y#><||@6U}qr+JR|++uDX@ekrxbR~)|7Czh|Q#4U8
zMXx8mqF~{b(A!fVN4@@a#`k*f^RgqkNABLRz4>>?Z*6{W{)z70$EPfx{9NihcU;Hx
z_2Co4*KeQnJ?VYc`{j04cAa*;cEbD0_N}hf|B?8Y>2KMuyPvOrc>e49Z+{jGmNlF&
zxR$WEv4pYPaT{?8v6iwNKFD}*cayySrFfN?D`HGef1Jx&Z8%MNVnu%yOX%sCtWkSY
zxg)fquA-bpH_6q-`N(dM{u7r@xOex8d5e|1ope9ydez<6wc2&MtM~K>oyg5k+<KyV
z6qebF$xDk?tCSV3{C?@Kcl+ZvkGLMc(=(2lw)xGiqODI?o<6^BLj1wVLM=IIdD;5{
z|2u^bt$gaU?o0g6@~14<C+}|mJ?Z%|?dQE8V}GRnnaDD|WmC&Vm+41hJCi-vd5U^I
zX7YF3`k-`E{HMkzE2m7DvRKo2<;9g}Gh4R&*mBuPHL+`hcC4|j`d<CRCW{T6cb&?-
z`Yu#>k;BD_J{rZ5X}f3i{qy<i(W5e3wK<Y|bJnJN>F%lXPX(S4eD>wZtS5P=Wlw%S
z`Mb_E&9uBUeP7wXwm%0=-(~ZyZN0WG=Jrm%^4NpB9)8{Tx<6MT*W>1g({87GQ>E|c
zb=|uXxFB%DzJ!d;@1GrW+UXSdaIfyUXuh1IIifjl@1|{Dn{|7-QryL_Nv9umJ@Qw*
zGwJpH$lCCqch7uldAoP%x23<!ACz&F-?{s8*XM|tNs)0kFRXhIyY}gsPm4Zn-yQyD
zUsz&vVFG_<e@g!rqZOO>daciLzq<U@l2?sV{j;9!eO0~v?c7_(Z(rYkKezreV=wbj
zb~`x{nLYI<z6WHlb<91Qc<14o!{=WwdbMkRdVPGo%Uh3+6VJQ1x-UI`sK4~8^_A=9
zE6k^u9qOHQY~$m?<N1Fde08oCUi~t_c=663EEbBEA0Hk6A^(0JkIl`>uG&>E)&I`_
zw(UYxSJc95cdm7ATVj@3?NfdKWy9sUvgc%V?Pve5`O@=k=B&-9(!I}5JSRG5w&nct
zx=&8WT0eGoinm*Zm)Pyv^5oLobsN^*JKZ>aecZ>LMJsRb{rx9&`s(y`ma*2gb8Gj$
zZTs7MO>XzRY4LCBGGA_epS$;E!REiy9<S}&$6EXRSL|>7d*61|KJEKISDLw-?bkcK
zebxWt?%2Mpz4!Mb`%3;e`!iJ*e>46jzj?e!oy%Wq-YWaGf3N<yp0;xDmp2QpC!F8h
zk>207!&(3T)Sv7953`<Md0yLXi`y&rweIJ8e)in0+W6(@htoaNFF$VGulaA=_o)|G
z&#x>0y*EAS<dF~A7hlh`_qw-YpXIM>-*TU)ym)fCJoEjs<z4qy@3a5b_;=y&<S)l3
zzI@~V!++}hUi<PI&Oe_j)N<3F-T&V5`8TLRiq@tDHA6w|S0gh+Bak$R4H~Eb(I{<N
zP#YGxO$$>58n%G7X~Dx9ly&HrhO<XZzAk0=-{X+ijbOJMCyW-nk(|kx!tWT8B;+BX
z$kx=bL*ppdHC;X#QQfYfEm49RdRHDT$P0MABfy(=so3fr8>-H8F1YY*=XbmFXaCFm
z`(Be?^V;@)J%dB+iK!l&3K<;wEaIhvPW#Q9Ip@%lyUbh;;wzZk7o2+f)bqy0i-HAQ
z0?)fxU)X;9zKJ`*qv$Z>Thqcf`@d<_ILh&#vto@FwC|tJ%<zntVQs(q#AnP4G8mse
z<Nl<|(eAWns;Im)L!lM}m)7F!g%UGbIF2x_>^ROdv8a27;+;7%dY5lroGGb$)>l0B
zfAiIhi~m2LJ~>Ts_r>!pW>fd9*-`MLtmWJEk2@PVc01S1IL_N8eYBt3rE{XdZ{~*C
zo}ZQ<camZIXcHO6B%M^<@%r-8gPa1toob>rxLqrx7+U-`8rX3rC3hS?@>yxI!nc-)
z6Q{X78gH;Yl3Li%{D~#mEk@*N@gv2yUmeRY-H9-{FUD|bwmt`s)WpdzBX>SL!Dg)S
zUvIqv-^r(D;@r#=<_3u0oO+VCyX^+oBk`s;0w(hBoDC;DabIkkIA2KPT%SwTU&VDo
zPfq@At@R4uXCU|Vj3mRV$bBYqYg@MkKECXFP^P0<QBTCnd7{iOZ(GHa(?0VYYx(7;
z)$O{^Sw8b1Qz28A;-jNM>r6CQk|eaFv^|dOa9}7pX!Bz_`;i6g299z9jZBuO7-A+c
zOAALO@JDmZQEl_(N`KO*qjA1r$M?q;uNI4D^s@9lX)3WWmR=`4*@#hooqS~bw-c?r
zUoY&d{Zw1I_?OJWeGHG+H}dpxA7qdbcQRovIj!1yVV}$m{)Qk)nbQpwd&JUDD5neP
zZZAE;X41FiOMlkMR_z}}vC6L}Ojq8<>M;B00*OAw+fU|A-lft#hikUDq~os%Iy=oY
z=LE9IJSocGnd9?X{rtrIzw%qpwQuYDURSf{SW=DDF>U#Gb9ik<`j4seM}6kIHP>|4
zuV9m>Qr9I;<fu$q6>2!ga%)ld#P?@{Ud9N%KlSS1{|Q_DZ%SQ$XP}rL__$Iro$G)8
zo`zi-*EPd6`8CWLh4<AjED8Fhu*-WV`+RHpx1Dmw*+r_4$O!(?ZnEn$OlXO;*~#)$
zN!m_Bzkd7Y;B#)@exBx&P`uu4aeCVOCW&dx(x=uq%)2hIVm|lhiR_DYn{8b06g2cm
z&fhJl``FK++H<vBLfKlIQbvQ<S7)6+z4gT6yPjrC?*(M)dy20&oZ#{7$}}EsmHBRg
zaxABn<K3Eqs;?<tW60)TJ@4zBuMaNsT+_XlzsB#Hp2eq@2!9#XKH;-2+!q;VY`E?;
zM{U;A74tG$&u^E%?wj)CgypOg1xL*9X)K=D|8wyisq=pe<xV{|71K4T*9o4vSiRKd
zdqB-`W46>c^_w$l+|<KbCcZi0FMD{-!y^j}b0qb6%$SpB96CPpA^$|n!##orFSIUR
z$dm1+kbLQQMbDhV6n3lk9f`@M4}(R$+ZHGLIQ-*O<X`e>)=}B7-`Cq2saJGr&C2+*
z^3aP9DSa7ID>;*`jz7{$KhZLIDuZd~0j7+0kz=BB%M913p5ZJGP<0FCFcO-rdj6sP
z9F|KnN|Y=&7`Za4om7kU_#fD_YN~lnz*?!5_xP5`%Y0R3_AC!Meyp0IT)tC$RmT6E
zzdt4`E~pAxyV5Zv`{%u)_bVE&1Y{W`1kIf=$EsC|Z6o`vsrni%<@^jxMXIhrfo%r!
zPquBBVVtb|%<`7;+(^F<uiM`FWbiSZPkvIa=(D_8eX>~336C#}7*s3fUt;?8VRaVY
z{%d>}w9Ox|?w{%Sflq+-k)zQJ=Dz}me7q7<ybl-!@M#^C+8~(2YJE^HfL-c9Vgb*V
zrppi53pis~=RVN;Gw(~2dV;_nmctTl7Y(eIb-qkio1vQ4ZkhaUhQ3&fYr@6|qiJoa
z2}wR}QxoPVPQ783qrHuL_2GR-XKlQEgY}J68T;#lzc$)$*ly9d`a#qV!Ms-ggLezf
z<ob?3-u#iL#xAaB`oq;9&Q|co^_xFh{?WTa{a&yA!FCP@4PmPm&4&&<gc)5#CORz<
z4oWf%bPN$Rbzxq^`1T0zqS+D(_a=k{O-`A_XVASch3Ta7^U2*Or#=ZQlE3LOPc?sn
z?GuHc^PHAT1ijIiC&HJirrNxzA;@p#qANjtLFW!~-Sw{YTpCoGP<JQc-lUZ?ue4s7
zdgbkv<}1NhvahsXQIzUk=D&II&kKt(VxsKU&e_%)=5Ot}+wb+#y<q`i27v`(9AO@T
z0@_owLNwomTP!SyeK_&ZhDEa$EnT!cX^K+(Mvua+kK~Su9o6pI+jZFMmDe>dJFkyk
zGrdkvG1E5Hm>axn`Inf;$eTVloh{uWm+T3t-26%L>E~0nr}9HgLUKZxLV`k5v{r|F
zTQw(W=i*Ou{FX;w{QFY#OU*B>D%rn0e;NOpI!}Ih;(@`B9@U;KH|57xk5{f*v}&nV
zbZKAK#;mEY1g~nZV$SNy3d>^5irIQJ>uT27tnF9Yu9#k(du8#J;w#~+-iPmBaBsQe
z<qelOE<MPelKJME#o~_vlP{QD=eh7Cvu@c=_s?_E){BLnj_O`Kb!F(vuf5k&*E;6%
zzRkSVd8_r-)mz86?k?q!)t2q^+jcH%?qRD~tNha5lAF7j?uzc>-F3Y*{-y7w&)0=t
zgualy^7=~k>ho9lFP*;>zq;P%|31ddglvK24F?k14_Y=idPYs&qxMlP)W^!^rMmN-
z3)c*;6)b$1cbM<6qH^+L0p-q%VvCL4n2%W<`*&>SG3g$EiSM&BX8oAe;bS&qj!EU2
zD`}f%-aK>m%;qzW!OoWhf@i+eyL@`t;k0XMoM}tb*w4P3tvz%1?B%ob4f2iUw-{`k
zkr<d%c;Jz`x2t!#_rj-Yr^`-<hg}Qv3_HEHFY;^T>&W6Y-D~+H?r&ar`^U{Q+gEPf
zX*tvCW^K{6CvPXOzx8OF-ZrP(S+}*zcFbKp_e9?AyQbA$d)xQk*mvyTwB|16+Y1jo
zY;f*h+?U*vyz;T(@#Vof%a-^=S}(0VRXvScTe|M<JF85KR?DeYTP^-R%z1sLcwN~(
z%c*vz6|W|(^bMZxyLq<SjBUxca>ae8OX{7Dy%qDXq_lYIF0&oqc1P}5x-++U_tSMx
z<=*bQ^mh;Y(d1pnh5Ez#&F8I~_j6vmZT<J652rredVlqK?pxgt_a6VfaQsaB>&>T^
z-=6+*_Ostp^S94mDSv(avG?iq#r6B@*Zx=jmQtp+d*0s?tL$ARzb?L9&t$_a#yW>f
zg~^#on@OKNlSP#!m$ynFM{JH@jY5UN5!IB$6DtF}GAdr&x)3d+%-0`$T#~1lJ6fd7
zEJoEvuO|D)dBJUhmpZ0N{^;2t`8xeh_m&<Jce!q+z&R_v27X_>cJXufdU@yG&c2m>
zKTWS`Zd2K2>t~#ocjw=Z=^rmY4nKb1cZ25y)h(*4)Rw7TQ{Csq<r6jiif!?!Gp@$^
zs?sXmlV%5HXm)CD)pXw6l$JZ^>g-pOqUPN)y<JuI@C|n{&$E>CmUiK#dgbpXns`M8
z-TJqs{EkK*Z+V7X`n_$H&3hQ`sofLaXJ5~}KmLJognGr4ca!(&?bSc5o?Pp;|AK#n
zs*C_@$F{C{scmWR&eTj5ox0WhwR2g}w}UdRbGFP$+t_B|U1N6LV!OfjSx5YW^j^+;
zZ(0BNk7MSJEoS_uXV1MpWj*WvgKs9>JYhHetH=+r5b-^66LviCSXi}i$A-lxwq>|p
zT>R+4qxIsGxGTADd--@zoBBm3N&nVXiD;Yr!rMZhRa3pIrnl+b-R_ead2N%tcjVI7
zUhy^4zC?P@47_=1Q~Uh(nz{vZ0`+wFZ@rWK^PK((eV6!{IK$GT(?s8E{}2_|j+`1g
z^?lf<u(&^$UY<T1Ul%cT->Xkq*RNV%3%K5Ky=3jz=-v5qf9-ly%76WQ#QhzOI~OJ$
z?(Qu%k6SS-Y-{o4OKLZly*n#7d-k@7oXE{j?}k0RcJ9^7tL)n)^P)Gty;}C~+iUAT
z<tA@TZbk0={5E{i`n>mCH?Kw{hX!w*y=!;E_x066-?!Ai{Z|^h)-gBr?fmMa)w{nR
zeP<p0JS=?s{eu6mn13+dZ2b4@%CFV;S?Vrdd2nIF>jmcyo^pOL;mw7|`Iq;-wUVjZ
z@wVgl#J2Z3`)`+pe9mxHz7}!CqQa+Q&2G(|FQbYhile*3PhWg5yZ`>}tXomFF~5Jj
z682I*<yT`7SyS|4%9ASxUiMt(zx{06U0dVNXU=XmOxK^!ZD0Pc{ek?sEt_xq&--q9
zzv|#;r_Zk6yN~PbjLUjc@Y3Sf;?w=^`n%)u_B<+E`f}CrtJAXYUH6OmzPs+1+k;;D
zyrR6gS3Pg`T$_5K^mo{+weN2Kxm{bn>AlVGl@FFb-0l5Pb>E|XxBjkTZ{yGUXZkaq
zeRu5c{_iZ`O8&@v|9rQ7PrHBJ$=^?7^KY*I62Dq*rp>C?#qYA;^1s{vtK!<@d+L+a
z4>LdAzw-aKw=2(HeqZ<f|K8++X9@3(UvB2FUsJR0f6e>uO#NGJi`wP(oT;?@v+B{-
zf3Iuv@7&+A-?!>_M#VwvTf5KJ`~BPewD!mEYWX6&njhx6u^(hW9W}Im9H{FB>a!Ue
zo0)^8L2Q^9N<R+NZwo@qO<>OC1|+7Z7GqA08!4Du8iD7yOY=%VGq&EDDa8uW3XmD<
zSfsgLBhZ92$bL}Q5Hk7foLG{Wlb;Tmr7wm}&xfTJ6=&w>Dd-#Op-e?%>IYAF>j#%6
zm4N5^LyAgMAqImcTp*He9{ye-p4uL%Ic2FOnaPQMsimn3`XD)%)Z*l#%z~2qA}%B7
z+`4OCa(+r?Ub=$5Z(?##er{qOLc}ezsJO&ABe6)q(8xeR-zO2yGg8nG&rB)FC{~E(
zGBvbNFf}kxFtIRDK=C}t22{_Zx&h)Qzr<XS>#(~yCo#QP!Pp3*(#a{mf-73r($r8v
z*Tlk5!O+seT*1)5+&or6-?Jn!Co|bGFFgmeRzcsfI2p9~!P3-7K_BF45J%U@&{#p=
zIkCVaH8VY<gv;E}P(eSqBsDio0pz*VL~t+|St#g7KvaNNLFoG?R)D>#U}R)u3UP>A
zW=^V+f)OOX5laog0x%Cl2Lg;hsVWGzw8>Dx$j}_*8v;w4)`t1|$fQct?f-c*zC|{n
z(a0fP=HI2*%@=f4ReALa#TU*F6PffbWMfXkPs1GVS5bx+Q*5`i+s>%k!1nmA-11|S
zTD?1MZ-mUAG2_b>iGI1Bj}4ven|{<7KW5W0J5rK%zjFWg=hge4SEoIjs~c0P?`|5R
zGEr#r&o^8*+y97%9Dj4Q>Di4pVkM{loN~Iib$iE>d#z9TpUK|7?5X0>z4OhS<jcY@
zCU+NDm{~L4-8n;ljn%e4+9er3Kdq7ezU2Vllg+E&{rV!YtxR+FdCQ;sG+*4CdiuRs
z%x-b3T}7(TpKa!Ov)Qkw!?66wRu}V={@oXv-o9lBN;qC8>8B#R^vc(p-KER_r*xet
zy!cDoIOd{%`uerDlIvx@-kZ#p@arzuH<^ulq!*gq&ppz8uewaNy03cTsVfqRvu7v<
z1h?EhT6EaNL(s~L*CVt0LafWVH|4oZOI)&+`1p9&Zn-i^CzydPP0;jH{4BkM6>s<g
z1179=t8m~tbg^XSAK{s|duo%W-F&yTXwoh7hOj+9zIkhiUfpsf=u(ogL5qgW@sge+
zE6lPwV;ASA@C0jTF8#Q3lG!TVwC6f2PhaDB;+5vJIm2jk%j*!g?Ly0<WS{vIbCjyY
zu?J6xGYWhtyPavv+pf0?o_)(qz2D3`v1i`KF3+o8D!!rDw@%q=I&tH+NvrZ^o%j?o
zk;(A>zUG_UXXYh${GOvVc}1g8+R7u@hlF;OX0Hwj^1jje*6@pw^7Y2KpJX;_ho*IQ
z^6;zj#6IP7HZOT#FnPt>{$=XMnhF;!Cmjf$5>&*$^q^M2lWPod7nXf#eeRO^Hc?}(
zwaC(iT9<04XdRGwH07GS&&rQHPOEv;`4V=#Fo>~fc-U6UV{SM5VS%W*gBfG)jkFy<
zEe-D!NwoFLbUnPLb*YwT^?^I5B=c4q%?Z$5Ww#|^$B*^y)Bb&y{I`F~_V)|t<Oaul
zm>_@ac-=y^FM`Ye3+~$A?zAEN?L3VKuVj)#7R;A?Ka1(;#gKY|cgoL}%Dm65kWGGJ
zD-h4|{(1j|8*D;Hb1R&sUnJK&srSjSSjqFt#pmg{0~=mirM#Qq`G}8GcmtQ(35kX2
zdEdVp$6k~ciA~I&+O8wFUWX(8O^w=`w{wK{F&EiCc)x(1Z6&*Q1*0-UqJZYM%=d>^
zUzvZ)MNZl7)$4qL$IWL83om^5CUL)hcfn(~fB&w3mam_YzVMWMzud-W_ut=fT$jIn
z{@=D;z9n<tf0F;g#lCvN`YyXOvJY+f%B|-mPS)3&+~jKRuy%v(qK3^<S#4h&*c8`0
zopTmbc<)?uS=lJ|_yaYU8TVXPmur3bdV1@kk4fd{9oW0&?SC2xKjyWF+_3I$$Cj(5
zSJ-YduWh?uVextAhnKA(-#PdCO*((_p7Pn}tP7Jit^W~wY;PL>26g+DN9+xIT<+Lu
zZsClvtA4}#^(%kdSH`)#FB125)&@tWFV~(P@%)6xEYbE$e<}<1&D-)@RrdL_;C7bt
zv%iS>-WGKG8qqE<_wS{YZ1vkSS1M9;w%3@3N6b1q@ASiX_P@N0lJBcQH6?0A3NE@p
z#hIa@i6KZD#5Mv==z|y<VX1j}ns8yz0w%DqZ(_27f3QM?f}w$)p^=`kLSSiPQAw3T
zfQuV=$yr4SLKA2p6{0CKIU_MON5Lnxv^Y5<H3y*tHYls%pPQHIUX+-YmXoSru4klY
zgir&j$HB(9SQ!}@nj07!ni(3HnwnTf85pP=7^uTlqEtwkB{``IVDAJe=sT8{WaJkq
z7=c_Aq@W*Al%G<XoLZz{1oBsqg1&Q6YGMgU0mwZterA52OJYeXml4PTpe1zqDImTA
zl#i$wDvDCmxC|7GEV&HeK*7w^)Yw!ZO#vciXkcMsqyUyx$b*U*7+9E^qKjErn3<r9
z85n@79*|~ay~bu3>MYGH(Z!5RLC!_hYiev@fUeHM0#lu(0cdp{s$N4w6AXVC8d_qC
z85x_S+hJ&AfgxsOYJf!yGYm|P%rX3CYK$2M78aQ1Sy-B2*kNge83vXnCWdHkHZ(9Z
zNB5hdftjT-hB|XY^!P9|Fvo}wLjwx~^!PP2urNW2kCLLq%$(FB@QUf+%&JrcBTEJS
zp#1z21#ojSNI~B-FD+jIl-NOR7lmjAo8&|zGZPa-bAzNba}$HK<YXg*H1jlLa}XoN
h+$_zGi?9+%<F2?Qv8V)`pbZTT42-x`RbBnvxBv>5g#G{k

literal 0
HcmV?d00001

-- 
GitLab