From 43cbe733590047715354d189dbd6d9afad64185e Mon Sep 17 00:00:00 2001 From: Leon Vatthauer Date: Fri, 22 Mar 2024 13:39:29 +0100 Subject: [PATCH] Work on data types chapter --- tex/.vscode/ltex.dictionary.en-US.txt | 5 + .../ltex.hiddenFalsePositives.en-US.txt | 7 + tex/bib.bib | 17 ++ tex/main.pdf | Bin 0 -> 74303 bytes tex/main.tex | 32 +++- tex/sections/01_introduction.tex | 180 +++++++++++++++++- tex/sections/02_datatypes.tex | 1 - 7 files changed, 239 insertions(+), 3 deletions(-) create mode 100644 tex/.vscode/ltex.hiddenFalsePositives.en-US.txt create mode 100644 tex/bib.bib create mode 100644 tex/main.pdf delete mode 100644 tex/sections/02_datatypes.tex diff --git a/tex/.vscode/ltex.dictionary.en-US.txt b/tex/.vscode/ltex.dictionary.en-US.txt index 4619b16..555561b 100644 --- a/tex/.vscode/ltex.dictionary.en-US.txt +++ b/tex/.vscode/ltex.dictionary.en-US.txt @@ -2,3 +2,8 @@ Vatthauer mycase Coalgebras Coalgebra +Milius +FAU +codomain +surjective +haskell diff --git a/tex/.vscode/ltex.hiddenFalsePositives.en-US.txt b/tex/.vscode/ltex.hiddenFalsePositives.en-US.txt new file mode 100644 index 0000000..d1b8528 --- /dev/null +++ b/tex/.vscode/ltex.hiddenFalsePositives.en-US.txt @@ -0,0 +1,7 @@ +{"rule":"MORFOLOGIK_RULE_EN_US","sentence":"^\\QThis is a summary of the course “Algebra of Programming” taught by Prof. Dr. Stefan Milius in the winter term 2023/2024 at the FAU Functions.\\E$"} +{"rule":"MORFOLOGIK_RULE_EN_US","sentence":"^\\QFriedrich-Alexander-Universitity Erlangen-Nürnberg\\E$"} +{"rule":"COMMA_PARENTHESIS_WHITESPACE","sentence":"^\\QThis is a summary of the course “Algebra of Programming” taught by Prof. Dr. Stefan Milius in the winter term 2023/2024 at the FAU .\\E$"} +{"rule":"MORFOLOGIK_RULE_EN_US","sentence":"^\\QThis is a summary of the course “Algebra des Programmierens” taught by Prof. Dr. Stefan Milius in the winter term 2023/2024 at the FAU .\\E$"} +{"rule":"MORFOLOGIK_RULE_EN_US","sentence":"^\\QFriedrich-Alexander-Universität Erlangen-Nürnberg\\E$"} +{"rule":"COMMA_PARENTHESIS_WHITESPACE","sentence":"^\\QThis is a summary of the course “Algebra des Programmierens” taught by Prof. Dr. Stefan Milius in the winter term 2023/2024 at the FAU .\\E$"} +{"rule":"MORFOLOGIK_RULE_EN_US","sentence":"^\\Q\\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q satisfies the following two rules law:natident Identity law:natfusion Fusion Lists.\\E$"} diff --git a/tex/bib.bib b/tex/bib.bib new file mode 100644 index 0000000..51e931b --- /dev/null +++ b/tex/bib.bib @@ -0,0 +1,17 @@ +@article{poll1999algebra, + title = {Algebra of Programming by Richard Bird and Oege de Moor, Prentice Hall, 1996 (dated 1997).}, + author = {Poll, Erik and Thompson, Simon}, + journal = {Journal of Functional Programming}, + volume = {9}, + number = {3}, + pages = {347--354}, + year = {1999}, + publisher = {Cambridge University Press} +} + +@book{adamek1990abstract, + title = {Abstract and concrete categories}, + author = {Ad{\'a}mek, Ji{\v{r}}{\'\i} and Herrlich, Horst and Strecker, George}, + year = {1990}, + publisher = {Wiley-Interscience} +} diff --git a/tex/main.pdf b/tex/main.pdf new file mode 100644 index 0000000000000000000000000000000000000000..b5b59d4252e09241727686cfd01b72439b174db5 GIT binary patch literal 74303 zcma&NLttpx7A+dvwr$%vv8@x^c5-6dwr$(CZQD+M-Tz+W*1OfH-d>&Em}6p$2~zoA zqO^>3tWczfw^y%FjEn>f1hxhiP&_>JqUKgk#t!tNR{BoHzl;rSjg0A~jcrVw%m|n` zS@`&%9Gx7D^{t`Y)|2GhWCsOcuHK-21UmVS6ICf=)k(Mtok9&72$fMjeFAvXXf9pM zj5PR;af5C32s~jl2ui|>`i~~CX3%nerelzCWMPC-XlQV=9peQfqvb^1EI|Jnw!i{|RHt;^ zj^)nzsX?0vE~szd@MnHqWKUpe9FXvXWfZm73LxTSBMzCbvwg&rqv0<0dK_y?_-1&u zd8qr%n%R+2e^l(SaL2NR#|;F&7@JNtjcJI0K?EJ1%)LNY85fGrUS+sH=di3p zzs195WAuLw z_Se^cEX>UMZ%oa|z{K|7w!TX5i{2!F5xDt+`lClNtS5jqm8Ymx)}nHv`c&JnaaH8G zs^rr{CV-SWMiSS29*tF%KNdgA_NpHl=7vas^5bWx$pJMFes?ZU$YsoP00szi2cq`(akDWGMa{bGYZ;5@hQnB`D0UinV-~|r;)pgL;%gw z9VP(M9%ipL;7iI5sQPWy$r%cw_mpEcZ0-U>SVW6kN#;9;MWTp3`K z%*Anb-#TBQ)bF@spFpaiNDR_Z{Kf;_5$56af$9%alpwl#uyOGVtt4#A7D4r+CelF6 z*kR2&V$v*Lax0YaUMJ}F0Rc^o>-MCP7pZMwIH!_dIm3+Z7QuW%nEvKhZ}fMbpa>}e zN>S`v^xz}*bh(=#9NMAdyRD7eaW+Z;XBf&8+rNFV8B6c6f>ki}ZZowv2>%?R$nTV( z)c(rGkTlqyFeecGFi^K2L<}v}dU-ul@~Ch(beC1v@c-kj2$4(bfA-;!jEZzxp>X~cZLX7VU$v1vr&eat=;q@olp-CE65a4=}_eu?14vS>9`(sD^nVTGfSMS0bV(cZ@{K}R%s^9_Oyo|wz4KFm*H4UTNL zFejz!D~TGxMrIuL1#6BKq~O*~1|8ky`G~C>)$CuDVXY^|9T#Hnt9Y3+(~Z=a0Q9VWLY7a#4;TH)#C2d~ z7e&Au{Va>J*DNX}Z~dYsRsZZs=HvR}GZ}_f~7w@JiZwL$cvp=VHfF z;%}WQdG_}hsZv{R%UAH7i!}c)5m; zwK~H5-#o&~{%`UKGaEbmf9H{@-x4u~ZLr-ZYMuP@;lHi~^56jD0Ua_5Z3W?6+IUmW z1|~^;_!ou3JmhAytfNGmu1slBhK`6u+}{ipA_jdd?rPo8MM5Vo;Jt34zrU7sex9x0 zF8Dw53qzU8k2WxKuxLBAy0g9?Xo~I>En<Ka zzMf}9ILRZSIDTV_?*WkMB^ct$r}!;eVnJk25UelMHvh@V!7HPUwy*S&FJ2zu+1lx$ z^`Q|O(M$Q+%jAMW-nutrRE6waS_JQ*|IzuA#VklW4q=U>Ot$+WZ{E_XPHn7NN!4JY zYIGi}6QtYQb{qVfINH$080Q*xAV(0S+$?*7lre1#b9kIE_nqbgH4|ig)E21-E7oNU>k2(!kjtZ znXZ)e_6g)ZRHslqkx;MNl8tJ-5-hs+@-AbRX{ea7Uc6L#(rnsFD+z5$RMwv-sa=|3 zUp@i)Abl^M14b4gLn36Ugf2KCNBek7!WjC_`MWjdXo(PXI%>wLkdwJ$pAU4si-NR) zs$1arhI-5-d92lKuaQ}TgmBF_SDvB3Zr+J^7Z;2W3^{PwMDPi9xd|_C4w-}ZIDXaG zBBM2>xxKmu3O2J$TZPF2{h4xc8xqzMYU@rYCO7a!e+d{X##|1%#x@U-mS{eA`FDG- zS|V&=-_^W)>pcHaT()KnN#9iUDBXqSQ~+_ynTDe>;`BYpXnkz=?6HcJlBRPWb~mj2 zFT#(Y&c-B*Ghy?bE8y_R;6B1bx!<`H3A}(*JMjQd+iU76*-4`G5lrXh%jPVWiqtCB zR=5#0-OooeFivpJ@2;&1J-BYa*9SP5*il)8HR9Io$g4t2&zuT4OP}j1D`=aUi=~xW zEToz#(WoXColX>AexYB9ot{h&=xaJ`=fA{>cPW3e@u_&kZ@2|DepIq;c zon5}-RZ~R{koy&Ag0?25Nw1Mqk7I#cenH8b;Z_Bbll`iMUNN~*U#=f@Q><+1=BF+i zW@bIa)atB>QIOsyfy-GbxRSeIIgF@;vS7ExN>b1ZVeTaC-P*RSV!wmW2Os4`&6f^} z=uZq{o+J{@u~`-{Cy{8+Un$KEd8gq4e6{w%wJwmp6biSYXZ-NxQqOq8| z>HpM-fE3rvLkCcV3yB>*X=M+ELZoO`kx+uU1QiI^tzdoSL8j)M<3xXpw#gPJnW-o|#WU=C4z!8rIAL3~bJH zJxq66FhEcQZMZU0;P@NA@1n3^=T5u7$@Bdb1S?n6#9tBRL13uly_2a~?F!zeayhgb zCBD3{#<1tTEp8F`&l3juxwG0mi^dsp2npmLcsc3RDtO@O-H-R(#r-1-Z)ay6&(I2( zsbJkR_nKVtr|f!a#%+p9x92J`PgKVEAdff zAQsW%c4Q%YE7$cf2$ihra+^*tPG%tn06{0Yfw9z7|C&*^qu)g|6G=SE{TN}6GEAa@ zt0PYDaELGjIHw`M>`o;KN`LiA!&ER&-8)q(FiERSL2t%oh}Z|(II0rsM)pLlJg(Ye zz0cRm%nry^fPl3}hzhF;PTc90B<7;WQF5HqUOc~JH=|?Pbo@|v@2?UbPwzLO$XXw1 zm$PknDd>sRT69zR7|WoZ@B(U*TC6nj@#sE3b^j4E@TELZux4D&7x?ZSU0zY zM|YfI!icVCJ|o(nCkgu*jw~gLZGgxN!wBeW+(9KFIH>=U*R^wXP!l*w#LbGd`L>T^ zr{>F5=Cs69_^hKAlrv;Pukye{-#g0g$JRrVv?-D-)B(&a?ZA`k+PX3kg_bv&Ek-#P z`2E2idhCwvvr=nvZUEx}HRH9VXYnb$mN?T9=X6>RXumpyZd?Hyv2@!3hr$9BXu}F7 zfb}#OZMWAAXyQ(skHxU96uRja|6zbe&Kh3Nn!c_K($LDg!r4DLvz}j1Q2`Jg7ydT5 zMnB-Rj~WX{k>#Zmz99vpeKn2Che2b|79zhpn-D9(ru;%}h(NYk7%ASgpk4j^`7Lvc z%v-vb4x8xeOS#%9hDqy@{nG16Q^hzemO^MAM6NU?IOVi=m6|F%$B00fZyS`?VoopJ zGE2~NX}F8b8ls$FefXfRX>>}^ia3k4`-Wrnmo+NV1Ea#C>Z#l@N)8>-xoKYLwUE^VE6hvMz ziV+inY#X0Ik!Vb*1H-Qj6oN!0=TYt2J@V)L6M?>-*W}tpG7wp(UjX>mP}lG@3kHP6 z#J&ZWGM7T<&=eAP`SzHzr?r^q>0~H%uiO?Pg=juF*!uZEmOs;THdd00Jo2fV7n&_E z5yk5^=oE`Xaa5Vj(58)aKku*+6`&|I@sgpxY6<3jiKl-ukv}|ABRdmQ8tV_E$rNEx zFhgs!tK`KjHr$73B$bQ{TBv|#z>a2!O=_Wk#t|sHV!8?$oWpxZ2?r)YcCcwE{TfEN zhUD;h0I!^(8jL8{^c6VjM#BPlBFbLNVgO@~ye~*=*FqR$0E@wl6lA6|?r;&z;t+A0 z?~RI@Jio4QQ+mU#OBfu)1kRDObE{H*$hJ&=%%xGzbZZ!TrV<%kk>1+^aWIDTa4Ju? zJys>a&>#La&?KNOyMpi zK3#`B(zj#Po5ToBmd)Rt1_tGlX2$O5RO%564nxka2N@1<8poH5v~LWi`z~a5AMz)M6aZhZ3?8AaEpKyHVQQ%6Bukt1Sus$XRQ*Kv)Bj z+SDCQ&C4K5A~(^88bLr=K*pdc3-iBKSC`^36Rfx;!?a8Ivofy295Vs0Jphrp+sCWk z=9ZG~o!PXK%Y_gttmu>%;xHLoT5ze=hbwg&IWOon+P0fxI}V>pe}f@Oyb%}=K24?H3g5#sxK zFY5YAxHOxDz=n0KGh3#JoPz0?ira0Rs>$di5e>fVVR?T&oY_&|$lOiSt+r)H4^Jv@e zNtVKteGjhVb*~s;BdDUcH)xJ>g*>pDvSdq3Irs7ttl~|(lI^zx#ep20S|*My5|W-R ztL%0iH|ke-AC^*ZMbhwv3fF1XY5CA0n!uIHetf$_tDQ(;oXShky~joZNqfqE$OWyv zHqC7H+wYx~P50H6&%g(N-QLlq1AUz=zja*L3K8;JDrhJ&yPhfwskNdrRNRUip#@1W zKt>q#Zu$rijwzvj26zSa*wi$^6=%25dYvHz++?8-Mr)Pn%!GW~YH(Qez?rXQ!>Rji z@B`1JoZ|f@;++O~|2eow`6{aY3&dXWnCc=pHv5fkRCXKOj3%O7nCiA!wQoNTVhR+G zmh2BlKT+lW)!M!G^1g@~!Y|9E#sO3R=tS_Dv%R?184=uZUx1c9giH&}NKb06tjY~{ z6x>zB@hDOVO<%ceN>j`oBp8k;hQkxcQg8UDGpI=q zyN|M96TQ=w)il3AN9XlB;6!mw#LPb_Q(l{PcWpi6HuhMJw3>-Nw|lREzh4MCmmDc~ zG^+^|!`94N;bJi8knfY~a)upXAB`A&zA$tZ98sykyy(0z(LY#CjB^P?c57^BI{3<; zfEjg*o)4;9p-z=$mwXU@yMq&ErlHUaxnvI9)&pmHYM>CTWP0Z(`%Cvk)gK|y9XRtM z|5TNbpG3_r)APq#u=r8#7l<9bWH+zr2Y?Ym5|)=ZGyGtp&5HkaDk7rmk-}A+QB6G7 z@jp^ywSe*)`sVDPM$aJqz$DcJJtR-|je80Q=TAv;hB-AS2)}}_$3w#|g~}3x@HX$B%-l7@A+y*;X`G>Tm@$Jeb2zWnAh0{LKMd=^k(sT z9n)^)KwM3jlqgk_Hq2101U00YFh2T47G5Nzael(a`i-JYr{!jLYWLVbKNY%v-pt>R z)VLw1d0q_OorY9N(^wZuCQgV?#vSPV9620qc>d76?k&1-iBpz=H=7~uD9Qns(C6?; z_hS?X3fm#Z3IL4jr#J#p5EI-<`|e`+iD&ekKk_wZJL(47%i@PBO*p1r>*f^SASY~} zo%wK-JW9JWduJq~!NjI7-kv;uJlY4mzH(5KB}s*1BbEg}K+=5E)`aG>zk;lUA}QdF z-bTNFtj-V(Yi7aO%Nt3b=d*T624J@f(c^C@>v>=bir;>!nQ(ejccY^{GlNPX5f9!l z^bf_r@KduLX9hvgLVToaQQrkhWGiSBp?DNO6MO+ltaGXi%J#48AQ^WB!b`A$ z6Q-&1Nrd#KN@YbNKqHeqgA_w2Kv+n?O1e$i7RZugNQ}TX);i1p9K??xRS@OV7Ls%p z(o10cDxJN+itn3id>j{GrHU6K4SEdGbgn1Ay3fE%B1i#XeqfV6i5C*3x_2C;yrrk^ zM{CA?$em-~k)%8O-K$^BO`^n?Kt@>ExLGD%XIdftrA~`<+^Ix%32KfrR`1pf#Mn4K zNRc&(zZR=wTNZv)LNpb=O$!>uyMn^ftrFEc2}LsxJc2qEPRq5Iay$R7zGoWOp>s&L z>-S!OLqe$*PE@pNNz!J`G*s!Ntwmv^ z5~eUFmPF#=^QJP&ChrRbh9U1J?9)36YG*HwuSw&WI{|RN@sTR(A}m|zO7&LdhZX4W zOu8;PD52aq2^A|E3_rK2O&&PB2g(l<%nV3G<(oa`Lx)T9fYIh38F&fiAC6kWKtvZk zaX+J)bH$pfcDdIOQiN7FA@4A=!AF*!sL(tX=uZrBAj7u9aZ_~1K{)xw7RlD>M@B>< z-W@3=OTK`vtg=+Qy{~#QU8aP?JR$X$%E>Ae=ZtZzZ_Pc-lmyzdTt^I0xy~X@NJ8RF zLu#V?Lh`Pjq394_RR?n9|sw8qf2o8}fBg4%!{IitzwiEirqG!Ywk-W94FP zc~m|7f^|*Y)FWr8?L|>V8>=wSllxEdrEb^E4PpKh3MS(7dz9Rez(bLVw~RWj29dgg zpvnHa?RZt#&Jkw8a`a1yK0#Ddk@b7AXRri&U||rL-FuXT_CQNQE#QwW$OvajqRD8$ zWMNVm?t%=DpH#LfugN$Ha{(BfsY|jw00~r;Gc;WrC$>-*j6j=IA`YSGG#EG^vqW9!lYJ) zidbcvT_&l~@2-rFtF%h}-9xWzHUUy}FLT^?B7vat4^>~uSUpwP@vgQjJW@IpDOjAb zT*)ou6_9*>TrQ#j9zochn@}(^2sGNB)LlG@+?ZG-CBofcNO<$Z2HcCWNoS^72R3Es zlt=6!h(AUq0!AV~n2FB2r&f2xkA>BRgY5?*#^VesNB*1&S#kbf^__dMiTcZ>hq0T! zr**b~C!Pb_mg5B2;(g|&q%e3P$WZ?G4z0qsnoQJq@t(|z(B;y~L;6~=iLZ8uZy-jpDh*uth9p2Krg;H&pUEK(&89{UNt(U_!-Y{X!ad?u2X7Bu0 zu3tzp-~=_e%@L`I_{q+)3nXURLn|WzB~OiQh7}_$Ny)?QYpx*c3dYo+3DwJG>=#m3 zCdTSkWt3!O=4?y8i?NOiomfhM>Y+(;7JHPftv1^3eGqFEbdEa2#PS1){?(BfaNxZ4 zQ-4~KtlKt|$E&hk-6(p+1_KBm97JC_4G=Xq%APlJ@T}b?^eBZ<;mu_%)#iRfnIvO| zeWy8%GnY^}8x5CG>0+~}XkyMkV`6%Ai4jOL(M_bkzv=in4HR*%mHOt(I-7*@Y%isx9D^fVieyN{*(&oy82He@tfMxTQ-g}C z73L4h-^k;N$F$+PH0wsh&8DmZhb{=<(9`2s5%ho&GJ3Iw#Zw7VrOHMbh6Uj0t}OPX z=)!=~Ah_RL?H$=bOI=l`@dAmX;$aOYR~wwK#yPcFkUzO%P4ai&l;<`7bIGokT>fATivv(2$xEL_N5wnSm5$GH!PgW=y6f%1-yGL$tJ>&s-h#CuK(l^|f z)K(yA$mV%ZNg7lBP%X!nyKDHa_6;w}ndoe1Li?b~B^9Z=`!&JA3vdsWsS2@hwfpGx zY?Eb6UILDCx!X9nE0t}4Uouza?@n2gBJhW##I%8b@Qf7H)2UtEA2itcnyo_WW*c+6 zK1I7LqWG~3zbSR)sT2&E$v$T6@XXZmK$|7f@?gTut;U?SaNAJpqcFbd+*lD);4Mxu zP3|XI5i_=(DoMM}B9^!jfD%(*QV}wcbF>eG3{{T{G?-I@b*qKaC^OSDP*L+Ivv_Af zug@;~G0#*QCGANlV;$XeFgvG&J`XwU5ctox3?sG#DuX^G1&%a{@-YkPID~{oFAiK0 z0b^S}OV~jM(~_gN^XSd^sW4`?DMuk?_JBf*^s8K~rT(5Y2JkZYax`n*`7%&QD$PcX zD=9rYia{B&`n5(-G7%5+uml8E95#GEW5iKp6;)pV7Kt~6Ph(bB0W$s#S6wwSge0=d zd>A-ue_G2@=s9WaDjMDzc4wf0>fl1CQ@yJA(s`h>`cj-8jP+$=&0?e>tEO*B6}~h{ zWc&?PeI5~3m_3{ns}uIVu??})@@Y_FSX0Bx>B(F%A$aWxy9${Md2iu0P_!T+W^`l^ zu5F|q(9$vQ>gF<5<*C9s@|zwp{u9l;OcLP9$YDGi5N>&pb8@4gCyjWewU*iv;D=-d zFN^mMtARFOqKkYM&g(Z*QtBIG)L7F`+@C>*@lM7YtA)h*R&tp$uAf75D8?!;>?t1g zbp^#ys`VmK>fZ3oaExd{71^IJE}4~bSD&(Z%n*Sux#Zp5pP$L{ioRj(ZFeP%T$tBm z3IWexi9Rn!7vJ#XUX<}SndJcN-I_Qnh+?(nfU{OGTxjJzhzL(RK{tRS)Y)MimQ4E2 zHX@!JzH;@=w}r2~*e)pcT(cRAbTw&CUelBHbtuVSYv}iX01n0IeoveDnC&@8^x>(Z zL*}ipOKz%%Pj-1$bde5gcQJo^pMVd&wg>lk`dP7kXjRA1LV9N%)uH-&N9W0_@tmt? z7#ue9Vv26O+_b{om!FrA5Sd+1A#>q+vB;^fRIdp^5FlS!H6@PI5X-~cpx4A-?|IDn ztlU32Zz-q;B|EtdTE3JDg)a0d%Dc+F)~UlUoYB5-oDlOjf&t&c1Da&oyv(fDWu zVWEuf_P-4a2JvL5GuyG@*p1@uv>$FmRYx$H7yK65GqdjRw)1>s$E%wo!Yk^tjf?qp z)%u$N6`2tE0sxq$r^U{?#^4ZJ`z~;4KVOVDElcxxGjS4~{$A!>sf`y;PDaSHt#K0@ z=7nwM>08@p&gqCIgM6YaWQ|Uuq#3Rk9SUYGnOoCzm3NH{qOtXO(%LAjNE zvx*TT9XgR&oJ1{NC+XYT?%Mnwj8Ecd<{hl`*_IB^<`;I~? z@B&V#uTYNVw0N8EeBM%o++%hCTRhiBdTv9$p0XAJdfhe0u0R`|$yL{z6MJjP)FAvi zz#$42XLJl(!i_qgYl~VPG=Qh*G@Ta!s4pLJ%Gz%O#l{xI!wGF7{5 z?bx-6@L}*~{zk`IWdb(-#ssW=_$!()AQnhDzJAHa_9wn~gZP-ASN?Jxfyw_>OYHwj zEitjOv;Ox$@9MXd?Ewc;_f5?#K0*pjw_k4vs0sL~mZ5{?Bcbd*AR069qt5e0gS;wZ_L_pvLWs&+Gf5?c=1!nw;Zd zGvfL!uu782vi+pRRxXozq77tvZ?x^st!r}po(|0t%OqHHj@otz%0|6egV#Kj5# z{iT=;i71E(?<50vDUssX5|++BW<4go!h7p)iPAf!Me#c)~1vfoI(yM^mVW1_-A)gzMaO9gfFIGuka*8@g*Ad9z| zx*XBOeSSxc_FA6uWz~x9fjDeHkI1*QJxD2I{1qQZ{_*;;Kx3ilkwU1PX|TmZ8+qWC zV@@|tC$+FV^Lvj){rrP@=<(lf@Q-$#%xdpl$#6@Ozu&@c(|xnHNSG3PNOKYN&*ul+^e%{+iHP+=D4vpP%{ zBm#}2#b(eaZ2U!!$DWjCDEh^#Ezv%HW#fT>{ql5mXA7N8#TRZ^syMC@3TthRUeXMA z5xR4pJ#iXA_Lm?I{?fd7tCEly>Lgg{cQ%%34$7~3#|=p*>O6ztrrO1WU& zy3I& z!4*RYRq{)1VObahMiw!W2o88%6JkKI;|@I6&KmX!O)jj59V>1`YGcsx)mmVPPGCb| zNmMzL0x>>%(L#1ymvx-((Ki{eP8no00i4CVJj62YhsaqJB};uTgc6ls1qKo=(Ebi< zxF5oq+};7YES_ULtRH0mIY47JEonxOtd1Q)qPN?v55S`!i2MLits|2QBO5uaaBH*? za~?X0Ic2oc-ykBjgC(W8A(bN(NLUt9wwogD0C9x7Z%Ro|SlFfoYCel=4F@22R@LA) zHI^0(X*G%5t;^bt(zt&gQmQ|U7`W}vuf?>U5Ds-mF@cD(Hnx)DK=x%>#a(^ORt6o9kc!Xz+9lLHEalHg^S9~yJ z>;b}P)o87yN46$#{i*>n7E4^-q9it%HSv?G;z1f#LNW1@TQ64)K_084+Xgk1b&%Jqipr`y0>&;FBVfW-}{V_@M~tYVqC zVXC6!Ff3`yw!uEQM0Qmqd+DaHy&jqs&To{>e$$0BrC4999;UlbD_YF%;+(w}#z{Ro z+bv~3<}Om#Nlx#gb}eO_J#xaYuFC6%Gh*=wjVL;eDX^m!63slXGSCCOWvahIDfwIT z=&v6uy)B$s9%Xos+ln_1KRo#Ntzt&Dlzz^8qHxexm8*1t-(bFMca+;;d!MDEEG8Q# zoxmqYi2+)iQRrP@RUB^A4=<+?eat%-o5{CTP!>O^70B3GYR&x-#d@g&# zdym5C-oC?I@9Ujj;wxm?&BhU?El64t719uO;i1waG9tU|I~}K(deG`Vy>;k2@x#n8 zKbnWH*p+4;eS-iXG5BZsUNcIN@D~`OzKGUkf4i-L*wMX?re)}1 z5mg4qC16ZP+K-+a<1;o=W02$X)%S}rtUQb^tMKh_&&kd5(}0qCIQ4h?l=`Ske+NFm zIkFdbCMly*MLpVujVNP=hs1V`k_1#JXDQfS?d=ggJl91_g#5Bs8SBDx_>>Ph#a-Ce z3)kQtoNXN@ET4uCX>F~+7-r=E9)$CI2vB0;St|&oB2JoZbV4P#)xhH@_%dLKeFn1=6W;AE&Y6~TT-~qr*A&pQH;N0Q zTt4F69*}D&ji)*OkRt_VoOt_Az2~~8Xwr^Mx?_@n(XYSK(4vOd80-vDAA^&$Nc31+ z!2}{H-EZ|2Ga-hW7Xm~KPh&(IQN{CMet`2XhK_ePdw@_~g^_8ddtNwToLA~Eg6o=u zhs9J$#k)&J_@(UE5K;(btzWI|8ZoXd1)p$cYxlktYc^F!fok8RS>YA3>W??pDf*~Did98DSdm$Q?$#qraVJ*2ev3=?6ZaM#%8p| zJgSOmXje)tEno1cx;S;(=YmRJxSLuE{$zAd!Q+(%z)I^(zh8)wchph}euD3wg7@}yBc zSb_8%qH#F%EqE4IrvK)YRf%;rn+!0) zFMOc7yC`w_6wn-Q6tiffXp35Ngxym0B*MkrexPCZ>M@ff&G0x)@C~KQ)&lwyL z78zk;jh%KRQ?h(#+5n0G9poN$B3J<8u^8KcCZP8xpyn5#OBAI{S^I=d^Qu`+TE|J1 zxW|1k^-%{ZhrskGGcWb3?1FL_67b4E^9;DQZm+eR%{e%GelxDs2%gT`Ls4Wia!wY`4BcD|?w*STC7kJML+jC;~qZtH}NVQ)IR-WeRy?(Xf-o@c$^O>{b4 z0JS4W*87jWU*G>>_*k9H+Lrr)jx~mk<<^^qGoIJ*0-;+lxu*SMAG@G*qEH`rLa_kM z5yBUvM+^!tHK#m#ErV5{cP4dtIb)|{5_I|pN8tQ7j=;>!@!yWnrPN_FzyP!Pf%*wp z;U%63f`JFs2-*(%r0Nuk+$hCtbbgZ(Zgeu|G^&UZ7=-LChG)JC47e_gfSGTS!er$F z#-rs$cN2nmokN7s9+{^1$*>p^0d??PCH9D@fDuRjYYI&Znr3x2Oni)iM81nQZG7P4 z6{zr>hqR#Lmk|h`#`q#c5z<^Sg1xQ;$#i4h7XGaHG;4GjsG4~ioI?!pWuJsBV7H7? z{ey-+IA5&cMKPf6EmXw?8A7bq zp^P#E7`td-5m3eYAQ5m-LKMScum5SH+e%?fZWgE+F4B3qv(kwiiVt`jay6(^&Ua@+ z=>(lF#{83BbG*j~x$Rajj)(>M$=$L#AY(Wz8jO_tGEgs-ao`3$gv@c_W%kE%3S_^UnARw(e`hY^ITy823G@;MzP*f2-VLwphx!05vcBLyPlbjfCv4sk4d$6Vn zA@SXu&l_!4cb12|q(CtpE4LvNNdd|H);fboD}>X?4DMr*?gv-J1}QQ$mV(X$rgo}a z17A&9xl)-Ub~=x0i_r;Ma#eaVA9$UZo_8LC^%mMJpn0$(nc$^lv-}X&H>wf|=~$02 zD~)HJJ1?bWsQSK)<~R;aqeW7HRwQ3lVsuhYorE>Uk2-vQSPV%DdmcIQQ|1Wnt3yc; z+EmAyrU|34*3OJ3OKZ=ou`p9U;Gq~UC^?|HEX93dyLST|vJ7Fg+t_+K1zeI9k}MH! z5O?ol9;vNld^lW5g5+P|oYOVTE@#*c)P%5YQBLp7^kVO=4y4>jn9i zmoGr{C(^N;svX99NAW71GgAx~hKr`T89!tSA1_ypm|#8AKFXVzzOCz9WJj`9zTxf3 zRprGJFQ$V?UaL*Z2w$pbrD5E;RG`)mf2a$h+*H*T7tM_VQTqlq;w~&Jp5DdFAVV-` z)w2N5>MnaLw&Vj13YXs9?FGBSWAFKYV}p^C<=+Gc3lsBy=Pd1nIhz6o1d*LLDE{Vh zs@`E2Vi9pj3Dr59=8mE_0H6dEO2*OHkk2pwn^O3QMDY;J8Qf~qeS@C04i}U={GBDz zsQu0M;f2{PZ<+mHDa#^dC^A|x(tADKD&8pQA>}{XTjGNo12H*1EA%~Z#z(;{?%J*^ z$4{?qQc-57k&`oGazacu>_>(eXU(oBvNS1i2zMjOZWv#}JXPt}zh)jfTz6t^w?uew zBbYiVZ@hhqu-g4JjLq}NBaZqO0!hq5r9lNc2AfBygRK*SDIygLf~A2OAsTu>7jifP?o(Bo3Rd2t znOX2H{`OUmp#-iHn4N$^c!WWwwi2)-+VE!!^>gxHg#&RO0C5HdXT`~c0}-N6mH>}` z1%uTkX63tZM;kuSF}>)hl3vBuvCDt)>kQJGcGAw3gnrxvqCsPtJ}k z=}Om4m2O7{&kFk!cYk|3&R3{}8O5#xd$0eHh|cy0;JOeyt`t%TBRAgRzg;5tO`U-exvB`XRunFP2i=^6 zWP}zYy1yQA&W3;>KOMTiImul#je;)8O@1&)B~#TmCWd=UO^AJ$W}oIAc$Xgy)*<8= z?X1_%(k^WI02<^{X3Dv`|76uz?9M+utDPQmvwxf?cMw|UlHP0x13$3Q)!#G9GN9C} z&_vS?Uy@ehlRxNn7#3K#Y245i11?NNUzIlwW;iUr!vT+majM4aaittWF7=kS0Sp*} zt6tJj>)Ur%4g#%xHqfs#RN4&DvsZLv&|OC(w~t9~gU87w61r2y-^5)BJVqaa|KeQR zj`fG2%x&EjPefFhz72G;3v(!(6%6MgDo0QVicNgWh^qfpNLqLvfR$hqo!Rb)xM zjL9cPVPcpZyq{~YY^ml6In$Gyq*Gw`1Bfh=sq{}c{Hp^GR#wKpWxvF^=zIngft|N- zzG)L?M2g0A3?y(?OP9^HNM?LrdF^;ai2VSco>|9(fmkyKvkBgp=B@^>mTlIjToa#< zW}a5Ttn=dYt){N0A|)}`>I{N#6_u2L*dKa&5%kG>@3}8ZI@u}JkCh$UomVyw^BMC+pallNYYEZT5$XzXO3 ztT%^gxUn}LiL+Dqny`Ws!`;k{x z$xB`<6Oo3f6Y1e1^A0WC%LqG7oH72A<3tWVRSi8&Z^y{DbQwa>ZfFtBPY8%Z9^1xp zS%*>(q(x*{*cSp-k`2xCN2@oG;h|n`Rj)&fr&2(VNGqa4W1i^N;tW_^7>`aHNlQa^ z6yCZ&`#rdzfbcrz}F+2=MD31f> z=YlQs0T^9n6gA zfQ{Nr)n$>GZEv6aEfo#Xi6)c@S5xvZ6gB_nnx13QRpMjgDb>e!_*<}>4li%@yx1m% za(8ugTTp`upnH50#msL@umet)=vfA9Y!%RjeU7X!tE=ZAlucl`oT_O8e}l5b{$7z# zf}4Q4ft89P#!?xk>ieaqtX=0zGW_zzz}R$6D|;0i&w1`p(#?y%`S= z;l{#js@t-W^~2)T%YETwL(N#1ZyOc0aE?6Ez2_yp z7Chx`?+@-{5lcz5RSO;=Hu|y-xF@-s!~*V9jlzee_VRM(*n*e~z>(d>2fg>42|;(u zh9FnC%yM;*rS8(Y>TzXP)lD|;8r91sk9B$y?{Mis*>@$48}rH4wi7rCu|y#VrRaDZ z6G@OVfWjn_9-1b>kw8DVWG|XH>yqOZ?|bf!wl_VIvVjwHl9Nvxj9WJ79x;%&S*<4I zOTZX=pe7F29|}sUp~_w^j;PH3QeA?nr&a)wT72BdaLtvldW}9FCUujfJ+2Cr1|o$p z6VT%+Lq19(O<8J9xdpH;#q_|!t4mg-y~L4DNfP1bq^S@ zXI8!XQm=Y$mp`R-o5Jnu0~AIKEvZqE@d(AEKz@lp3Soge>Ueox07b6s} zU*NeM6xILhLQD({|0eX9|9*R|o$w#xgEF-9h2p-6G1Mc&g^;%}9_Z|2@d0Sn=^_+` zboCeQVIhCi_wT1~<2>=`Y&VZXEze5*sPfd9A52$WN+13%Caq)E);xLztkB}rV3J!? z2{{=e5SD$IHjqFQw7z2$jWPi z9~ZQPh#SO$vxEl$*N24jQ}GMv<&3TdMLL{C5x2A1Mo`@6Kwp=1B8yF{r4pA=M=d0Y zEfGNK??x13djMFa?~3ea>W_g;X0JN&V{)_+bxtc+ojXv&c-QANzUDtq4ir(dilB0%^y=B_pb6O`(G36ns)RES9-89Q!NJDny6Zm#%8J~? zr%Wf2rLH)sDZj3VTJTb6MOCwU9r4jN_rbBK&iG)dzGJoo7xt+0r<* zCud2~Hs#HLT|xBWAP%*J69;-*Sa-2~DM*>5&RBSsJ1NcdNs>Crg-<(rzl-^xZBg=p z4Hv#E&NUgdyOxX}{CFN{x)-`8#CIjr5X6R0H#?D{i1o*%fwnA0$JqEx5x38yn=N2@NOPho zJB#k-gG_ugXNayv$1dlX3jy_yjY*F<19|vpDc|1!X}1mR{{+;(>b)?r{#{DXBn)9`ILCgm*P zVm>&>{0#9&Uqpxtv2A3pm^5&(*QhC=fDo#f7&RJttM|(Xx;DNrqD4mmU1HjwGF+D5 z!-yrJ87ZY~Qv#i&?K4@7%}Q}%QSP`%QBIsC{o{W;XZ*`A*63NIzp|?@Ii}<1^E#m@ zpieR6&$HN~9-Op0%k>%Z+~|7vG}nVI2lA-q0=v}F$)C@%$XTy6q7FNQAqOF$Vl2|%8Rt;pE_fY5f6fIn;#9FKRT`!%CHFo zsuE3JYHD>nxD^bfK$^<M$R_6kCg{^KAM8grZ&>l?{y8vJ5Yw!_jU$qC_)))cnWtQ0AYtVc6W-hf~^fvkY|HCuj4 z%p{1uy~%OEXkabR)_SvdmstsRadCsH$4|h3m#K@7b;T)OL-Sp4{ST$pm--z z%jWi>wze^`B7((uyi`MxxH`wU>QjlcB+B1#>IoQJ3t?)hG8FZ{lfTZgk=DAXeS)$# zwqnY*?7`TX&~f*PW}w`OoE!)f{lSE~;ZhJrg{+CAe?rmHY0mD~Goy0^cS1C_UI_e> zgBP6Mg_e*5w{NwIOCKZHam z!ud`9F1&|{-y+|+X8+drE70vr+uH{}d&gC5!9ELcuj-i4biz)4e4?1d6uYX>3(`la z4?DNMKjm?0vOz!>fj}kEAhn(Eq_e=pR)39~+@4 zH5fHC)0S*(rhxF=!8+Cg=Caoa%%LU~%dMgPXo;#t4B`tjf!mxkE&*GtGaa+PtD86oIRh-uQoLPw|l;i9M2PXrnDCmhw03x%=>It5|YeJ z=(yj9?KU6Der89NX$vVM!aq1ww)aME58~h^8X#uE++L7BSsD4(VPsuU`0VV@wgP4% zNjpY3MI?vO0x37A>b}g-;a$^+@Wj9D(hk))PVU(KQNt)x<_vwG4}4#(>EXiHD%9`` zLsf#x;!QlKGC5sEq^uOY)P9#r@OmCkaxUP#LEatd+_8TDgTnaJSU8oNi0gOvuw?hP zWH+%WX=U(O$)NDW6SW{XNx%_fp99|zo4daPN=;(O;0W0ub&1E=hu}b>gS3=apw@G= zsxUQJVmOhzpi?Y~PBpCZ=#INgF+-gT%kKcgnG-L&iJezidn5AA8(mZQiG)dGZN^W%ck zge>ysve6Mk9(Yp@i;0D*fsfy)4K+tUrcTvxRuBzfSmMOE$@9qBq_G_T0Dt-Y+gO!rTp89#9hb*{bTPhSae4Dze995|Cx}62Qp|NuPN>g{d+M-fKo{#^ zpq$z9uZFtICqNN1!?6B%9lJtgwN;T~X3=L-s}%a_NU%&!%chrLJ0;oM^U!9lBr7vG zyq28MRCBC3f4%^Z;0fxI6#)cpptR3J1`y)X_Ki*>SQSb0l?rIN8Vj)_Z>F5Mb@am^ILfDa_T`9=E7Fh4QN za)FNQn=3UT$f>NbuC&s}EykSeP|c&+IP+X@>Q94YA9DelwM08MQ+IrdAX<NnK`B zl!seUaB97?OKKRh8kn7UHa2E&FoZHJs>x(0WX5X1wKBir}%ie+ToWL zn(cd+^!HrXh6NzjWVepWJZ>018RQO_){=7?qo$dh-capbwuzy>Gr3Wsx9tS$S?WUP z#^qzeZyUk~vZsX`Rr83+v+FL=z9Itp2pPmT(col3^z)yV6ZnrIMXNGO88Pf!GqnrU8; zvocTS>aInE$&J0==lWXsS=%iqVf&YTec=HamR7R8@b4S`watR3yh$^J47?hqLgs|I zC)ewIie0BtMj>q)4qD_)89toPqT!DAA&>}@Q^2B+5+lygE^)ieZZ%@qZ;1fP= z=!SJVO{ASeiwNsv)HG?|QMF#S^T=YU;Xn1s8^;}tzx?B>2jU;Za!xrp_?Ph+vi56N zMJ2uMk*T6OP0G68VqfaL7Dys?@d8bFo* zLpL!j+PEuNq6|X0YeedqrY&5|qa-_oErzrO4r!^>LTX%Pp<=|88(@N{N!4KsY>8H&slpuF8d;O{_k?k}grC;+l=+51EYx zj=IA3Kp)=yeSNnAOvGj+4HT6t<*hN9yDTF}^$NQkY}Dvw^FwBVB`)OLXtG?{;RnB;zezxQlt+G$4me?3szrw!S6XZiOl^0sILhOi&2Fj^cu$%g|J+UzWvC9cf4-I^@g*!0_ke90lGV*l-lBLJo z>CLNv_3vHhb5@&2n!_^3)K&rv-%a*ckWE@Ijeb*8iyt|;zm4M>u_gR-`;Z_Ubk-4J zorFmZ(CbSIEJz#DI+8EsnZ~)Z`T?h?H`QX#VZn4+f^_$|+@jrSX5Qnyk$+?8dtPKl zD3u?|&)L4U7I~&-2Pn#~ktq!3c$N2i=*Iu+d?+R;){SsbNaNnsdnKLt@KDnc^EG97 zQl6@`3>|f->uBYRGbE2xgU7d`T(~~GAMl}uq~#D)W4Xv<$&!B^bQe;|_vW>sCuyp? zsY8kWOo!0=?a1dlcdZuXjb*K}TfQ&6f%`j>MQ-Ao4@H*w0sXu(z0{NZZxRe^X>KYt z-ngC~@!HL3@a|*2Yj*r^hKi8qh>vaX<wvN0b{uhr>VdK zM!JLrVIMZ0?D@|eKF4`+o+}x8Z^@GPB-c+~k7>T;hX#H}EbZS*I7k;p zb?Ov*vhU<1Hy1fX_C#(7!{PY9-^UUIt_b=2o5XVQKASX2#CWm(`ijn6gDxh@NDF8_ z`c*?}`2aHw5Da18DZQ|;%I1ZQN;q(59!@x{daD7Q+=bNwSqisdYiCKTjd)FJHNN}dcwjeiMtX2O1bflze5f{aHgsI+Mp zc}255RKjr*a)hKYZm6nsh}ai`!Lr+rY2@(9PhxkFhlNl!;A9bZHDV~a$4Wgk$Q*sr z!vPIopNe}>pdDchbO~azBi&1ykJ^p~?ipLCS-Os<2ryl-_)EJrU8@+YL2smMpg-0Z z&mc|DdW?T9iYN{9pZbL}&;Egq8AerB5YXqUs1#oQU>YqB4@X+bGV)>E)9-++k+hG0 z?NMaOw+ZPW<_Ksea`d3;xZ0++3(&xE;{A3K!M?^_v6e|evy^Yd7AD1%dq{@ZA*BIqkND9D&2mz3>ym;d9CGxt5#hVPy&D+jPtm~uFnS2tW(jNLGmbE+<$M+% zro=*fLi+BgExRgs*U6D-A6_dNws~T84aRc4r-ZkuQUg9Hx|!=fROqC(er1T7P=bCM zgHW5oYk34wMZAvGNVL-sO{t-@NQ4WX`aUBI?9o*UFmKlmI1L0ChbaUOP-FH=x>+Z- zj6`(`pLIYS)6Iyy8CFDtIOsY+VU^X-7BZA7H6}(p(RipdxlKYvH6MWJdDquyd)BcU zHDpNieK>YktHH4exvPPnF}~y@a_}B+OI(>$Q(^KBUg|;RdZTFWYC% zhbLysmZ{)}z%p#Gh}Tw)f1P|ROu?X62*X03`R59ObERn&SzmkiRsBVV?W7o8miUHG zx^x)>&V8y^MbTz|5?^8}TM{#?^zdLGT`FuPw+Gf0TFH_005k z|5CK*1tVW+3NG+=lUjV>Y(J|{PVBM1DlE| zvZ~sS=`+Enaf(jIrgw7+B|E8xt$Jg{6i6HcTTlAXLkMUT?q&UA!T0D&3t{GqxX;{^ zszsu{0|eUlR1%Ev+q46k9nF=PBr3;@iX@$z2mHfho447-^-#i;v5Bp=0Otjri1qv6 zi__}856CKTLh}o4xzHFFDSu)3TJOz*K3++;NS_d6;e_1#4O44z4iz~2NN49$P^@~d z>lFC<=@}dpfu`P8<+OaqKzs==pHq`Pc@y6N-m2`0OT~owIAIuSsuPVe4y<5C%8TV|lR17sZ6O zJ!}=xA7=x@xGBaASh7IvfRQ(;sqs2vl1IJVLZYqU*h!P=2KBa?>1~0cNs6Go>yrG- zI9M4RG}}-nv#2o9u0Br97>9Uc@eiw8;ur1P<00O)3R6*FgZ9%NEOQhftDqBJ6tSpg zDyhi12ePJj{_B}w_z@wc=l*48Q=em0k)MFvNPWiCWsY14vRnbH-hB-PtfR{?ao3%! z6SjbCKJKWHZSo?ESe(~%xjQ|{c5W?Iu%T+O zU)-Coiq~NuO|-n{t8W~^5`!0a#i1X#MLIUhAM9OU`5p4%V1lZqYgl$6^oL1jtL-4t zX@pJoL_IK^5(jZ;h zC6M4`mqL!0ehs}`XtX_}|UHIk=~Q#V0^_SMW_T-hz9jOiHLi9>Cf zt4*>-&5~&(g6vMqxi&yc*<`^XSt~$%=FkMR&~T@!?xf|h2Pp&zPAWT4`wE7*eON%g ztYFkUu7&S=9d(G4GIjvtpGt8disUR?dgQ7sxGE44W)#BtGSmt$LN{A8&OS^>?&tgmG z$1CPP`(bz9E5!zBW2x(7VWP*a^w%@L9aA9*fN3f9LLDo~9I+HHmKq;k!6s14@)#6# zYSE=sbol<(EX%-nm`<%u&n~3j;3F>Y=S zP8Hh~>+qD>$%GETYJ9wW>T1>?r9nsHe;}nnTf&^-+Jk~&JUtc4a%?1AB*|7>Iw?=8n7Bi~ zzvT=gj$)}&6Ds*TGJ@qKqs_?>F{PNbnAOj(J$DS4fr zTw!d{g*r&0=wXpAZ7_Qgpn&$lJx+!DH*{OZ7q^x+SNt*gA~7@h{K)za<(Q}=wF~o^ z3r{)BdMMy#3qfP@dc_N@3VzTj!A_rfJzmRPD|)I3gH5xpUq`1q54dRIs_YiGapcr~ z1A@casLtn8y4KPSoN$he#w#Upgy*QPz0T^%zsgJ3RJAJ#VodCKe9SYvxP5&kpa)F$ zu*N0ZZ3ipddB(iio$vg)cY%Rj`i0)^#ELAhoIa%Zcxd zSaaXvFKfT5k0l{*jG?O#m~enPju6VQy*FdQ;5ABchAg9MDCo&b7S%Ps`gQ_!DmfBd zB%%g6P~~oLLnMX2i1gzFK@gRwkWg?jQ;k{B(qg)GyD3a zPB&#cXi+_RS?W;WVJcmq7+$OqZc+i6h>Y!oD~L*LL@-IrtQYNpVRgL%-xo89Vry(j zEn&+1__C(bkrGGf8_tdIKN#^-bt2W8se+bzKFRR!hiA-x?DsInd%1RWP-GE%jZrr?~wdQ?B`(GCnBI12m%Ge)Dr@DTKIt(3ED~N zQDc})M!&bQl}q938kD<|Z6%>lcb5~pnZR}ZFuN$TrWxU(k#VvAI9pkh*RTIg8NH?2 zsMvV1S=^fT-3;3UZ*|Z8pbK1b4ul56xNR~3PD-w*ZyhWNHgOK20(e6h+|c@y1yVhV zPA^xyUs()bqt?ZIDKvBQbfOpr95wE;@bP(@n_{s^G#{=X! zr?Wq4YRvhu$?4V1s(~*DUe|F*H5_m1+=~`Y{SE)o(yG zN?q|W&~f(Y29xMugFG-i!K|u>SF~aeQX|I#1TjeH^{_i=S{-ZB*XPNFPL1O52NTI# zHe#Sw#1Z=N))$5keT$8Jrt4O2iz3`}>IrY_RKa(yCgz~uqwh+PAm-i=iqL!a?iR5R zXa8m`XwySv#uImQj4~KFN_y_H+nPyl(g%v?!+=L`Qen~bB9C%6)({Ca&aqc$P3~T8FK2I}t3dpVTpis~UX+3@8_kcCg7U{n=H{wG~{Hr+Q;A%=$cI zqooT_WpPfK>>z8^ zj>^Cd*A8EI3J|_iK^;%P>9D)4`RUq})($^1PLJuT{NCN@lwlw#ZsGoOy}9f&9ognA+Y5~g$pUMV2PneU@+@;n^qbYWo*Wueh#?KS z4~j_bLry7Y30kIOWxJfiti@A8K4{B^cEngDcoW@-+NOQZZ$^NT`CSVXuAgzubS6@O zLGD=jiVigR=ehf8MtpH}9{V~FaPc-cFgbm`=>wZxYnz5ytp-npD_JiF)LA{5F8TFY{K_ zf`>rh29}^iu0qMba+(I(U(t>uQ|5^N6K?&O(CWWc6#qN&_dg_j|EiT;Jv{{@IW^ST zn_kFoC>-EM|1I?YpxOR!ixoyr_Ww{&6eW8qp|9YNm}R!?QJYyZvNE zm6cN=C(#q(kT2Nn=T!?*--L<~N4C>n+v=E*T)ffH=||-C|K~}ni(G*b0Z@ifDfn9$ zwWPSf2DrrUJZx;RNZ?E7^N_hFbUl7Qp8ojg&bjY;dKXrcLk6IR3C71OM!8$CaRIoM zD_V}rrT?5#^CsqeFGQEs=ce6HgYimD&A|y&Qn;lupLGLr;ZZa4h{WSy103GT7@nkp zm_Sl{w5@`#5=6TxpI~s=eqpuZtLRo-Y~Y@e-W2^J^Mt6hE7%Q<6|5S|2DKNFVWHt3 z%EpsB=1ixKKq)DuMgNyS?l5SCePrbgEx6Xlmp??OEK&!d0i6EgjO&4=f6}at(ty^{ zT&g43&Qj?v;D)T0(k7y|Od9u7jwGp#cmZj3IMN$9d*<`U7E2~o!FBaNtHSCI&C&uN z{+drxlUnM>!>?&9R~q*Z;0#wTF>zu_`dAqi4wc6+q(8)Q=|^!gJ-v`P8twMnC|fGd z_a~@Ss1#S~;^7{?c1+~0HR0^ zFY9YEf;Zz&3`DNV)P0k~R;(-go+ywC^`^igrbPSd(BBO6v9B9u3n2pK{KK1cPJ(W? z&W-*xWwP&*+Apaa-1T}@Fj^}_eW1Yl4m0~BVc*}GC(fc7%e;>t98!6Z=yc+u2=T~h z(KKE%ejZI-SKd=hQE|kc$1R3;&ZoUC=KUs~Eqxj=i)p&K&z^W^Ecs>C?$y+D-53-9 z#;%ILm_w#Xzr2$-w|^hbdAreUGk(U2P%^;&_~b@~GoRQjaCN1ZaT*|>YA-uE6O@4N zY~0(naS3!$ps578gN!6DzGWgAUK8?pUK~8JTsqYu8l`1ygUp_m99LAbqebXN-tmHR z&3)6r$?ZJY6PM@e?ZIei{6H}xa!Vw^w#t;jupX>ddCp?pGwWNmHO=k8<&_U$-#SGQ zkJ9linOo#AWLhc&L8UHAD^bz>`y%$5UcFE|^+8TCf^V_!OnkDGwZrntHm;m_bQZVK z?6ejNJQGMM3%sk+qce@}f3B}VF|$U2^lp&S0t-Faa6@(qe1jSwBM$99E(Z)AGlUr* zhkTZDseM8d-=L_X**Ao59+Vk#Aazyk8lGEV2utbee+krO2?iW^z`)@aKxb93WY^cV zwtTSNBz*qrU6OHR6Fl1VO!VQeJVq}C3&D6d3bSI{eV)ZM+ge@bLA4Co-e0FNjm*<#V4l%^tYh3#{8H1Lg4v)=R0`svu}2^jjIF~LSkRBp>0-z^2-OK?wvKPW)cBN7H*_@bJF1v>Q(Fh z*|TLuVW!3iNN^kG8_-oEz3Bnxi1!@k z^ZQ9~T>Wlacw(X3ux9?0@a=T=TA(2M3(3hGw`UxH3S8%*K4#uygH)Py_xF!;@=@E> zd$%SS+#4Lx?L(%nmWcz8ceN_sX0xGMjBk$|W(H>MTz5MOy2ESnuF7UTUGUT? zE{G6rg2g*Y;8-A|>zrF6QobKc3|$Jf94+kfxwYm0+Uapd!Btn2Y0JY-as2&a82(Ne zU{ino%3Onb$An8K8|iv^o~O@p+j`ws#iO%ZoqvIGoqR&G_832$ocz=g*swxmrr^LZ zhIwbSy8c6G<8Y^c!!CS(Wtl~AsGJpMS04=$X@CJS2qyA~Q)LssItS|rz8U2%<7rL+ zFH8&wu8N4Xm20%i<@E|J(HhGfW3vSwQ-3`+@l4jL#87yT@2LUm=7gb@ah4>)$z<@{3s%gnZ)(_!?U^;*yacnM_#0+>GoXL>`GOG_ z!A2{qEmQ!nM8tScBFNU!n1XbL#={=?oJNRx(PU~iibi<>B>^*-ABi!M%)$FJcb8Dd z3kPx<`{xvS{GV=5+@^v9w_DD75b|#Htd{2iV{RnC2#LQhH6C2+_q|#@w*}DAs@R{D zL_7XHs@F1KeLu6K&rC5HT-6;VXgNA1KgugXxO=h=N$ESeD<)pmzc8h;N``{ox-=d} z5^Q%teFc5QHl8}1a9B|Mj^Er4)wO@zu;gM>u_Kgh{0N-}=IiN`V&6PO5pdQ@YEK*l z%roxQL25*bB8IH$EdT!V>B@YlEKI;$6eP*d6_&xlJ$7=d;>pdbOkk@UptQcMd|g#m z{oqkyQC^tvqP;NeQ~u0Om3X-M-ztLtAp`k8OpN*uXV?F)*g%%IGg7kGGlMp^`}Per z7tHOy1ZVmmxXb@-xxvQC_#YaRDvy5}la=+az*u-{1>?vioGby$Dw=S~C6x+=^Xk?W z$h9Z$h)~!-^4LQ%{hbwlWISZ#KJD{v$BL?E3r)?g(yl5=OUs?Ufvy=}uw@V1F7NJZ z&(A=Lo5{>f_nn=8$D8L&SYT~4fDAS4W8S!;Ux;TQ6A-O?bY2608(FWFMGub>Oroix z2lFQZ8d0U6p^RbkXG~+#Ra4WI!|+@1XyZ(s6{W!M`EBH#s@6}idVIQ1cCYkH=!qb9 z>m7hqB{a-j$f+1SNiZr>n6Jbk>INSH%L>Kjglk-kt(ugc)F#A0N}x11e-h6bg#VE%=24=;EYyd|J!RtHc733~hx zk*)QzdG|^=vK*$@e%KS6Q1v~;ZeShmqvsy)8(|-2W*}R?m7VSG{P&2|i_C$@zSsuP zjG1l`*dmdDVPwNF`$4z%F!MntgCDm9x4gIC88cFaCdo6ykiy&ty$rtB z#i~gGiIY($LXQSv4an=l)ubzlmr>6{{|*BB18&GVp>6v^Zphz5zmdd3llX@rlO%=` zk%Uo_1g{EOk?)7P35sMUz{kClyeQvE-DN0gG2EJ>)Q#3VEelr$CK_q1X-YS0*fqQlQb zo>XkF&`14XX3yZ!5Hk2nzK6Tnk;+7AqhD?6T1+gf&Hz#ZwwwNAHSv-Ye%@%Ouo)XU zdyYay0FBgwiLGg~<>IY5-s9CPu}#-gbW{7k!7MYPM668No5;r1jA!=`Kdy*6sldtj zqDLkkKtG(h@Y{ci)DjogfvDF9cE86~^h$854M?YD<;tfu-^w{$*N%06{&3T6Gbu(5 zTtyrzD_uGqr);98{NM+`RU6@2+}fIGda)&18JJAEYNKn^RTVc^<`)xH={ICsZn~58 zWOF*Ko1&hGRj+szs{gcLreHWTbWK<2dSW;;ciLR@_3HMfH2^Ofp9 zAM?gAYh9pvFqdH6qA!YRxzeT+n7ai*+sR|svNtJoLb3Qq1~HlPYWf*W5^go*NR>{z zqb(2Zmi&?3bRK4Yo&^MQdAoHkC8BdIb||!~LN9YgF~>5#?G2^O|?(PlyNK`${Y0 zcA<7jPW(0AjHCk^L40JQF>b2E3XbgppmeXSXN!SSP7L zQkqsb@OgAb@=>)h0aW$ydgXuZP>exa464hAEuW`qKRR~H+?XDFw{PfN{ErweQS9_c z!I}k)gM*=_OvbJ@Zf?QtsV zn3(@^nhL(Qs;aj3$bQDMZ@bAKvuRAVHz}|PDFwR~8aj~{52!&AVbNq!77Q%oqoao4 zw7rQfZR9G^xyvA;^6}ehecXBN(dsgJm zL^q5=GH<}TrLisX3Of74{UR^%h$8bGR4AbX!;B}$7UaHIX>51BS5OD07$f@Ueg4nZ zUlSV?@u}}Y&Uo|X&2>r>#d7RLPzT4l4HW4SR!f;SMHvVuXNa|4N7=z>QidCd?Aa4L z!HxEf+9yE9`{`R(w^YC@Pa!y4x_;%FS+WZke>aIlG=70W<}Kb2B%e51jHl6%m%eKU z6UvBqS>>Qe{VbxtBJos*3_d46CzI?<+&L(XwNG@wR9;YP&+oExVX7cZ6AB;M$Xa?r z)6s=A>Q%Dxjm021^2kgAo~nMN3o#A8kT)!0_ zZIWPD_KG`TXZ@{mXTN7bV&=`%K4F+^65_@~7dQSL;yO|lP08G8T$~=X6DS>S^M?4j z#>-j6&bBQ~D|PN&XukhU6tBUGh{5KN+adIs`qXi<5br-+uShH@6LodFrGjWUS;45; zzt*Qd2**TF?3G~{@8|p$(4la8;UzS8u~K_g;JSif$jHfjh}kXBUN$QjmnUG8c*zsU z;>qa)$EljJGuVekbYf3mOZ?^YeB)!tC_!t2ws3%&f0`PUtuf^*P}_L&n0KC;_uxcmq!IiAL7@Xmnq#tPl8%HKsQ^6 z=B6x#RBosn=0@AsBn5m}3bNbG@1mYm)&SSCH^09I+aK| zo(AXvDF?2%WEWvP`movX71iF#jxOvaz|HflnZx`{1H{a+6kyDYcEOqM`|oP*<7Y+GwevGRVAK*h5p_KwQV&1ta1_Ul1h^ZX0C? zP&^pu$*ee=P@eVrYQQX}t$=Z;v~*>BmG5f6QG0e)p!Uml;56<&2A{9B#Jwkuho%R7 z*^GLnz?|-;wj)G|7iI4WdsHlePz_U}6p#V`!oF&uQw@_E;f1rqIf~sIq?EAL7K(O5 z5qpy&^tr3sR(IP@Y5VB)hb3zB8p+S#83L=vC3LjIzyZ;xuT9Sx(yK;pCD0?zi7#5P z!wIhva81Np7)Bd~RIWBA_0L^sXBxCi!TI-QDPH%L$=z7Awwbanh}y|7py-f3C#&6w z(f5)XbEJn!)C9`4_b8H#aJ*0siY}bF)v8Es=IbSYA08CjpY_L!j8pL*jM(s#wt0B} zQ)8P7Ld5y*MdZHY+738$RV!d9rIxS#+qvJ^{dn; zQ%(jS#<}CfPHeHd@R`RGSGg2@y!tynLm=0@`#wF>x+|_LyN^vb?!m=b9We7Psjz!^ z;B!_z>5H|cjI?Iv>I(;4?ROo;nq?496A9^Kp$t93l`%TuCwiNxopyuxyA)*{2HE+8 zCeFLS@2t*N!4jI|au$y*mG+AFo^PrWCdD9U91DG|l>vdUHVUH4=q%0xwPHxkv)P1oxP=?n|8`o>SKt4+pJP_#MjL zz%f~hsx|DB<35kJA-Cx~`>&puALsW~)~4mFdZ-kgP3}j{O~G3z7oVB!3cT%VZ9FV% zrh70o*ZjmPJ;cb9(r&q_1RN$zG%Agk8FNF(bk#WcJc2p=A=DXb1;3uq*_fbk!L}qg z$Ac-Mr`6ik6T6Pa)2Bfu5iEAT)RzxIP_Q?>hC|0Dj5>ZJ2UM$)Kv1+B$z;e7112B< z_gDV!KNB~z=4itPuh()AkPLSV8?Jj*?i?!$+sY>T1})iJ&Ko2K{^$(5S*ES@SA0Jt z2fdWvnJ_&Bc5(>9(oH?0`w6R*+Z${oo@x;yLp+cApy@35xORkFa?zIF)&hPZDPI{s zUMqSm+OZOt713|eCIp&%#+SyER7(b#gTLs_izn<%!kCU)7=`Mm05c-}(~#@;f#olO z=cp4ofVnV)=ETqrGx~-n8`rSYGfvK_7}$fo_d(w>7npwHt8 z;N-6e8;(hw9^BxHY%2=5cHC-Dm?Uzbdg+-t6xSgG4#I{RRht_=(t%XJ9`Cl**9C0i zX7Ov+Y1s((@Nxt9R#KhSuNTjt51{7dv@>KUJeeiw=qGebnh{+aPlNSk3ccp#pVn)! zg=3F5l}6E8gMg}Wl$stm2aA$L9f&4#6v$AZIC^%_*7hzp^nk5G3%^xbgHlN6n>z<<=T`^A> z)p3R|Q~|-4`;*psN}EaoJFG;8dk86IDGAul9_<hAws`Obiz@RhLque4iRZ;ve9BVU_O;X~(;`G)OpSMf9oc|U6u->3IW zk_xYd)vf(khMsV&n7!Z$Lf`oCVAxbOpO(@%I(IRQMASc$NI2-UaHfVSAjDdkrYC+4 zHkZ#VZLIWIWYo(%*p6Oz-d29B;g1Ut1%8IV#&RKzWk10f6jCZ_-FC#$*h+6pb}#}#B8f0y!$T2y|1#k{8G!@GxUp;XMO znRh2P!5S^vgf?xWxL8eax!yef>qS-1P@i`Tb8kAzgAx3gCl=N|D*&BCJNmLQ=m?~h z$PMi|HtAp}el^q&mQi_;Q5yT*wr$m3I-XM>0PSeIAU=AzE8s*F!y}r_l0C`UXQG6$ zwdVUBTaA@cRcctGy(1cWpu%Qn$Fhuw;YsJ2r(6<9L_iWG^@<{i^<1@sKB1Bj3;B^A zt=v)uE`5P$dx)vfHK0^a({hygwg+O0#whvpI_QWHW1pz|(@)O8R(5Zv5UOk>^ z544eq&`%D|rcrUU51Capewcctc#=TOH|Ewn4q3KsT)idPkcF|8fJ~WY5b<%Srsn0L z5+B(2eVx*=8eJI&kWQOD=x9v&Y5hbMQ7;JY&JvvDg5*!CCDM zr9S;wfNX%kBP6REF?KBIlj7%Lf$&b(y$HQLw|UBj@1?=13b zmDI~qA8o-y0hCy(jRTqvvVmO`23a{#&8;f|L{iEn^Oe_16SwHUirxFnxQ%>LJ4Q0+ z8@_89{g6oDG)kbU<-`Q3Z<`H|Dnf@H(p`TgGaBdmq*^}IlL&ikyb7Bf>M zFB3EUEW2?4K<Hy5iCEbsN|Oj`oNMGCr!tkFpmN^>^DQmu$(p-O^esE_ zu(Zob@j&DwzP(|*j&U67nyL-Qc>QwL-AEZ6==~9q0Oo$}8Jki+44c@I5^QM%&NWMW z0Ne-;abJCs_-b#}9Cx<;2^PD^`#w$R#hsH`Z~o`L@j)o3Hj&m#OreU$)s|$63^9h- zG%t+dYVmU&&bbmzdzeuo{LGa->E?RMfezBUD#q!aJRZ&6{2t@s8 zof%M-r&CNPj1yXIE?``F+9gaHakGpoIJA6f5X@B=8-RjsbgLfR_%8%0yX@kZet901+4>WmmLu7GrPPOnSWG0Ao(s^n~5i&{2bkP`B_t)by7LK_O zBwnkF^LTvJaG_xFXskA6I)~6`;8T13=VkurMMaRUammEvQ4@m!Qv`?jvw@DnGN@lh6vOfW-kA}vSpTY;$1_@K1^zfg zBLYdCOUv4*lrA1d+jN#9^jID-X+1OW^5L;CkcG9wYPmAUXv}>yRs;*{MCDYyT#hAn zcC@+m3;|{Trotm@g7}J2rL~=?>b$&mRvx+SzVlv;3|BoCb6&pb8R(e?rM)&c3@8ZhM5N8y50S*dDfc~5WkXS6_KCd zwB9J}Lbj|=m1+cXUyp=uFUCpw5|bmK6Z=GC6+=hkn&FqmTWhB2h5fWQP{J#tFwxGlG)ym zw#MGnMC{a~nV4z;YU{&>8{V?E!OCKAewdUik###F43LSbKWZj^OFf ze6GI>`Ox}En#^c91wn>$n*FhW`DHUwF2_D>8uT*4A>)k5!y&0FcxfOV#CxQBn4T8= z*eZXdwQa%TN%i3=3#}xUAhO-JaasD$?cN(~j+Cs3tXVeMdd1v1blJR#QpX9^$f5lF zHmeKEg_V3rsa8kB`Pqf56p+_hUT(Cq#%k?|Z=ds5t>56K$JRkIis(aVXva_duxqq=u)n1 z5d>@=I*>fj!&@D5XmGrP1M(bcnSY83U;tyZ@-J>N~HMPSWjy1U<2X{ONc)Gtzx zGK$B>+RQa_!YZn^$2X!0LOkMBMkRUK_;Ugx=rpTJ*P0jj*m%XOOhgu)q0J+hPG2u( z=ymkqJkk>yBUzRn)>>O6n>M$6yamAKD6U$IAPJ3I-!^Vt-hFs|q)`ABZ>bf47W zclGsZU46M?qsTcjP$fRCPBWu$iZ8O7j&il(#w=de~hr4s( zpYLGUIJDU=yMsnF zbNut&EJ{P-FHdSv_nk|>8W%!U$DiDo+6m5j?BA|Y#XR#YJZW%NR!TZTbhqT49;U1b z0VW^NvZ0im*W~{XW#7~!h_bC&wr$(CZQHhOyUVt1+g6ut+f`l0blj(XCia<_`v)@e zAy?#D>r-IutK%of+ns>P^O%kOivbs2f>d;fE)#RKPdcWH&y!cq^>$kbOy|ef%}mpc zTV0!Q><`%A&f@&v-qb$`Y5)E8GX7s&w*Wv;0MIIcf`2>kA9(iv_K|WhvHu6;T%rZ; zqoUe5%dq7j5Fvztrk)N-5J8u3Ae_%63)te#@ij_GN}7pz-p?`{VDrePVix^M(57_T#57YX}OHmn&q%NLCkp zR(@79FDqFmzKJh4kImoN$x2bpNARu({mk;o1!K0PgODXoR6M%Sy#BnRC?oy;YUjS_ zr^<3e{;+KOYp5A=wc?zRuo~JuX-tt3xl9%%I#2T3$Kl}hBe>26m!I2Yx*S1md^nzx za4Vj_;l`ZSu;ydzk~b|mEB;eR$q9}>hdx@0jzVVkcce!9Ud33RRzemzjfA}Hp*W3~ z$$sJ6#RK77VB9dbfWT0Ux0B6dxbuvLLsNOh^3&d!tOzEbP*d_ zY5Hh{BQz7S_+8Km&58Ta2}wjz&Z9=e&*r0u(>B|6tOhRjaQp^3UPjI`22P{z&xpaJ zqX-s0{@e3#{1fyNx^Y?wUyjghrB{cQan4Y9aDF!bKclePr*+a8SSpyVGoVQe4W%MbvfNxcb54Y(q$86dey?JVM@JO-ioM> z$XATiP^vQj?3ZU0C9WZ_nTv}n`$Od5y+pnX3bDJIo9@F?fz2>lQ;xDGD0-TL0|(Eqgm^wKWoW~}h*a(`j9 zrL;x8c#2F$i!zVRu>8hJ=VYPwT50*nX%e56%d^e%HJJ&XPGLB)Z5RBZG4S;Xj%kCN zIc+{wJv}{zWNzmb=B5r&@PHiq^jNlF$?OL~YY~Oznmc#(GFv*xkbz;CnoBYs zKa`h&!E0G7CkNN)7wSdSME^B0=rh<;qXjgQ9cZ zu%Cjb{d;&?t8($YIUm%C6B=W{f&uHU+?pS>Mk_4r%XA<8(+0gd#?ExV zo7(1mg0d#V7|lv|o9F!~-HYL&<8qY`DkGqAbg7?`V9RQ>j?Z8-3_R8mIHH)8}oL0c@*3O)OT0guHb*yDc5oopC zCxbUbN7!LvV0sr`f2pk)HW;OpIBH_tL!Ar$3tK@NmR-_)B0ua@&4LI33 zD<}c(NEvK`DsUgV4#9~-Z0PGb0K2NGo0bmPJ1jAXEa8|DJu|Fvg=c9k!44P@C3*mN z`YZNpQu4e-ws_Png(2fsL)LIapq;=vMMDon#-||smu9&_dmZ^VqR;pI)Sa=8he1y> zp0qcbW|H=JU>}|Ut?~ucOB^qRV6nPoDTK$d0ywGEVr3p+2^J?kR(SZZF#kC8eMgTi zcODPp#ffm8Gx1${^*w78zb{1Q)A_MeMnfGlxa<+I$$3kbYw!@xg1i;6(TBml-NEjW zjIJ|6Gn}*xG%Y!Va;9+@E#NgtQcT+AGbFpAtbq5?7abgWm~gZfxEXs>+_xY)t8y!I zcr370CmF7+>?+V6Ju1$SvIW>=O;E01FouV7V}B_s3!MF+#dWI0ID+_P**(iO zw;Ayxws#2@P-4;epAV_`>+uD@gHR;cN)q=X073GbEo{BQdsV?Z6zEW?k0LySG`~r9 zDxMV#Y96kcxnbpiRRXnzycB_kEe{I-R1Xd{-0p#t*nS=nSsHwK`p4f37-rRSYp`=ig3C%s`pNWW7*&(@MMeqD~1(_TrX%_&2$;zMLvCEun=XI8H(-@rH)A@ zfK>c3vh~Q9+9g2Rr%7mCr~L12e||fO0}i?~<12vGNJ;^f$eQ4(Lyu_x*&y{&Da5GI z{VN%lUr`!<#Y)4Gl7K`D9@nr@!5n~P6E7=4b3MRJ9x-QF$A!SY!>dcPvb4PQ_IAY3HGup%<$H^!S<`vVb^Hj*d1o$AZDIsvkzM%^q|MN(PBe)I} zA~>x;>KK)eFd5Y>I(U;^x($+LoZ+1gp3eCw-|dj14lF)hM!$K;&HP?~d~rdwS=q^R zDglyy?tu)h!j+;IssH1t_OOnoKJ-F z=c>Me!xX>jmL;`!pcH>3C!4;Ij&}bhC?xxe#sw6=EG%In{5Z-dM~Hqo7(o(8VcuS4 zvOPb!tm@ai@^n|SNq8yB!d$oUWnH|S3%eh}?yRn30B{24G=`zmXr^w3WHA+U<{s2* zzq%*fTVHXt9|M<8xIVAOJcRCCGOTr^?5xCB`{AMbi=~;5k>y zK}H7*G)X<&1Kg11n)ajZ*!oH!@`rr<G5%iDHkGzqG8L@>Xyo`H%F;A zsWZMaJ@c=OhPxwX{sT??9S7&3+}>;6iIrXK^=5O2bqUfvq8ln|a)cI`)leRf#CjpS0#}aiQeXG3n20VS9sxFn@kAX~A#8=D^K4Eyuq> zr?z3#qr@$BZ5ncc=(rL)U73c={$3H9j2}zPyD=apbO8O~?wC3rLkH z5L}^MRHjw@KePMJKx8QErZN19p^`y*Fl-_aVWs zxnlHxFv>Fx1g8XswQ(-EDpot>GOc^kYV5-6DhpFpq=;Wb8n866k_r71pBAiB$@uD(LGdl+)AaXkWvAkq=_4 zQ_B%glWmL|uxj;(T`o5N}rr8WKy>S1+pSv5)3Zd*{|F3N7w}= z-(Mc~odwbY=WbGRE2w&X=&Mq%3CQ4mA}hf>@!VT2$5nt#vHOMow)5;ScQJp_wuD*p z>=wLyWZ_#>MI(|4VtCz@S-$&3AcoLC{4C6`?@8nr3Aj<*f@- z1&e$N-CTe%>RjUT6bag#+rv;=VkG-}8X4xEWXsjYnTsQBM7&j(IIf0HZo$G57wm>u>pXt*Xt9i;Isq+zo$> zY6Al2U~O@gOsE7vA^WB4rO70LASqo^Ssf)9-eNQTgm-Yx4-N2{T?-TA)tZ%O>@+C^ z!?7s8U>!sk%Z2#V1u0i4qIhOFi@Tx%It2kH6f06A^nbrv$`V@T`-vm6r%7rEXZ1~6 zRA=5Qu-x{TN=o(8jn3=cIfvO?n6QkK4a;poO_N|_&B2bc8t}o zAc%d$TYX83ZPu$E8I4RmJju*6`)qOIoz?hmB=B$jow_(Pvb52OH!q-NZYk^-4x#b( zLs_<*SZq%IS}#|^M{%dW;X*S#?H63V=)2(^9&qlS@ZgCc%t`t(o6W4g=);0G)HH+ElM#K8cWJiE;&qS@gZ|@L=+oY`JNt`mk@H!g7b11B|hMa zPCO2`L-HF~Je+~eX%ieFcOpFC{QV!Q4aIdE83{s_8a^?}*a7QDV&V60lPgOo<+W!v zwymlOkez(6M3DIWM>M1OJ~w!BFL*?nD|5&kIT^H@9rQvrE|Rqe23FeBKMNWDX(B}( z!1B!MMQl8wOx{4gfBd>?Ivn};2c?)~O{;!E5&E|Svw&W7N?epmeU0&rIM?Ak$a8t= z@&w>xMR<{ag7si5W(PZZr!oGe8;v;`o~JaLp%%0kH5MtYLA`yFXWWa3d||$hJ(pu^ z5d>UFZI8UIk94uallVpFoedzvITchD3m(isA88mt^6p5qkZ(XFW?s(vNRjOlPev8% z^yEWCDRdM~&;D6e2mMG$BskwuTj_AN@rlvH$({+_5*O~elaYpnysv*+7OK_D4NFWH zKLsX@M?^Fve|#(}piZ}oiD=%l_5PbsY#RWuSOEa54(C;)g~d)?$&hpAk`YegC8DM~ z@TDI^0imY>*KuJKI3%Bbe*9RwxPQCY<8JlvKubD1w)@__yKR0e0*E7&L6z-2jhf1J zif5$5dLMj5q+cf?KFc&l*+b?y;p72n0zT3FB(=9aDt(h`m^V^Zl!>CU7&MDE@B z0eYgj2{8CywXYIpAy5$2f&6${)6pbK90SsOC*`Nh6W+*xrMyyDF_bRW_|#_Hcu z0QhrvoC+qS{pZPJW?sUc%N@B`RPq%Ry_GX^Fumn(XcY+kR1^4ZG6$EPj>Q>)RhKec z7J+m#S!g7MZXOywHVG}oGlG>>{j0TPP*&8H={o3J#$W6c&LNVuF01+`xwd#Qzz?H8 zJItWo!)eaaWimSA6q=b3Qff0|k1Qtyh5^@u%ha~|uzG*v7DMB0tnnnG4{s}kLS zTLL~_0l$)K^WO4UuL;^p;njW2kAB6yJP1g$w~@p#%z=5hztDNT4B(G|xGDjGpCnQa zMoM08cGE8b-!{o5Wl4&yOR;@^9A~ax}$*L(!kycC) zzpu3vs@W=Vc)&4e#j0-SB!h9S2Fj|HpHe#{D9c89I|_?YXnhjB{A4%Gi2kZ(Lvf?U zs;X+6N-ARJLX~&ol~r|gH(<`_$sIkCM2!_ekc$_n-so#-CjbB;YDQXJ|Nd0*4EX1d<@8FWJSPsxBS{6Gl1PAUkj#Rb)q6skWwgVvc8-zdfKJ5 zt(j3n>gFU%ODiILo)e|A)i(1h7AwW?B|gC1$hmfD*1m z%wib6CcHe1r{Xby=HC8et%RUO*Tw}#AvyCx=){8wX|RYIct&9JZ}isQ{=7KFY3}6n zOEd{on3i6;JX*dd;7Z2J`NwlK1VCK+Q;ySud$MO@4r#)DJiHWtq*6-H)Cxwixp~{b zg+&`%=Z6I6Tj-1u5#lS7s-2^^*P-0Ou!$KIb8yE`fx5c?G&kH=O%HEx47usReaC?Q z_QmZzO#CpD{6Py2!ExnkA%+=o$uunzO3FBDWQJorP(_RbW-RNWqH9n1j(0}=!{wf~ zmR&GnxRrCqiY!mu$1%$>tBd{U6Er|mwE4#Ud*{JoG~ zZAVYzJIq+o!*~bKdJRQ^V#|))@)sxi_7A~|y&$Esg^78y(vWxgAbZ+^og9Ggl3e(jzz*R2kYtAZ~$C$y2;bf zzf2E+o~(5>&<%RtXum(T*}lH^KxPWg!mhV8BIw392_+P-=*$qj{(k5nUEr0T>U;AA zHd4AITCGVez)ZniFJ3ab2BLn7p#1b%dEH&~KM*fGIPH7S?z+`O?%3OBs6Nl!gZX%O z-XjD@v=B8z`_ID9X1{jzwdK_y1LPA4R!W1QP*qcwSzDG8?mt>KGkh;;b>2(&YmjrU z2I6<~^-2;R(uT=M5L=f$Bv-4NJSyQkwO@7u)FlwFr7gvXvQiWBFq;R~j^ExvK zAr64QY5CGIg-?Un6FzXjTF9!3rj&kN@L`iZ?ZIPMZEV2dW424tS#5}N z4UKYy>0;6UULF?=DTFiW{#*r4*A{$Qj79Y4SSA1C%GS63V0Og*Ajh=aD_puE70J&| zPtGrXL}_=x#txb}uCggny5awz0$_zCQr`52~2ZpOYG6Fd*Q05 z8fOprxCpF;j$_Lzs8b?JEqD6rrxkQITpLiKN}9ycle#DpKPt>17`Uh|295~hXj zH5&6ahMiU2y-i)Ud&|H07L~}6SF4LgPBN^v(NM-QOY8F^s8JCO17~xL>jTZqwZU;V z=eLmOCg>_I-4-)RSu;~l@^rN|c;mYyw|xUUUiI~J?t2UKnTm)>gnM#z46zs$_Bbb9 z61@lZ4|@*bRapYs&g$YT8QN~hQ?`GIi;mF2t>F76zq%-(7L0bQIXM-*=sWVb#PBTA z<1eL2_M~#qN4brl0TXK>)H0uNZ-}9_s0dop2b6`TC^R#sB*_a^(BX|jD@{@r;gYd~ zdX6hwkoh)o&Q-ml9#8xHw%applU^npa+9w*gdC;=7|UB={Q7f%XGaF_`#1264jGX1 z#YKFNN6qQMrn@f>s@}X06?AYYQfFgzQgOTKEx;p-V0Xj1+pgTeFLQY|ypTf&3ea3( zLnN|F=-D1jviIJXwI|1|;Q`}3zQ)WhyuyP=CsAN+o^=scw3DJw@xC33~Nw+u^7QjT% z&U>CHtqZC$^pNj?b%;PNb48ruZ7X)Cy&zq`jNKt-Z5+^$gedmXP9Bmb*}sh8W?$dG z$8gjHVutjDo3{X&V%ZZohYV^yvMB_;9}`-=(t0Y)_#0{k^@(SarJW{*k*h;G-FErx z*1R+gcGW#ry0!x))B0$+@AxuKnC@n?)zx3w8RCwZj2qkIm9)=NSfDCd(@0Fp ztCq9V;+GhyJ{{r+;Sk;MoQ*nD29H<}x~l8mpdx%zB2zx5faZQ{m~m$MN++p4_J&D_NmW1{ zRS<|Jh%13JeBi|1!Jub?JaL6mxNkqxYD*R%s$Bw=b*!9;*zfK10Ui_6rlPxr>i8G* zV-Re=KWT5U-$&-&xq~a#t4;Z%>N1jIhldK_N-ojPi;fR$>~RTzsLNJpiy&1`E1DFh zrISd}#*<$@k!nV6t_)cPs7pfTLg~PDM-IMhT34egM8=M~+4vivn$!1NZP2 zAFh{#=)Oi7Vd97Ob;axp!2yOrxVf6Mp+8e_?c=z(G`GF2>MeCZR$^QGT#xS_@GrWF|n{zc59*R_z4*i6MOmPDsb4ZFZ}TYB@K#6;A|iO zk2HTZE1I`xD7tf%_13!Nl2ERlV@J(*5Vm%c)x^%vqd$PewW|;uNeYmwNl3klpou0M zG6^i{j~X;~OK8xM&=3Zp@-;SYxh-0?s@mb&#t|@=yYu48pl*c-^RP0wWYB^%ls#hX#oOwH;_M5I(B zit4g!7cH0-jG&89pBHfmftV~CttijNmm3?xaTmBK!0Kg8=e3@v9 z=u3wxjnxJuD_f4^0k80K{8b2fXTfo&>gs=ZS!#U;W>mUIjbk=4=Sp>mwAZz7U06f! zIr~wYXTu4>3UVAHdWPeiDlBs3oX9$up*W!kk{|j!s1=g7sIPdP6{HP$f`}3Faxl@; zT#@!ik>2|*l$kh7KmA)lC=8|40faNm|Iy*+PAqNjqkHc|p244B40#$k{c}`)%PVh; zhq+PG%;KjGq2y(Ei^Q3*7CjBTPxJQHRQ@~SJKp~>Xj3S|JJ9fpU`QFEhq4(mpB;W~ zu2g|MH%OCz&l@ts_9F&x({C)mw$1H8M0YsG#wSM&Ofly-Es$VGB@E+KSnfKoh5+%T z5j$t(D~z$2e?VR1IsZI5XAb9YOC2J1(MhD?VOUH!z~@D5%BrC&xRvTTO`ca9+FyL- z@HgE|R==6jDupzKd#;2|MB=s5fwTuBD^ zPCU716Y=*HLY)RsBTSNDj5>_P>|}ELRoi}YVEC)wa`X)uv31d|+#h=1UbJ}qMyp!4 zY1x=QB=3K%{{fpXX{h-Z&I0p4Wb*%=1i|(n0g>AAmHop2ps+A50MW%1W_Ab$AANlf z03l`lk2FCwz z2dMcQ2BB=;$;X%t5wT{p*pa)Ki=3uq18sG^ys@%U(yrz(aKLs2C`14Wm?!{2LJ}Cy z?@a(H4V1u3&}9=PUE|uL+O?M9Rn^LTeeJ~UY|ov;zcrNOEia(GS(bA-opa#nrVtQ(t zYLBPOXr$5{XtgCfWX9?U$gqIIUz3HL?^oJv0@R2P+!y7^iG%V($9cApAeZ_y<@kY9>(wUq z>^cn!ii6%^i6iKnj+_cgc+%{#QzI0V2tAFyo16JC|_~JOT1WF^0 zCz@tVwVVwq}<`=Q?6j%mCs5Dq-W?_*~&!-6_SO zTIe=w2S3SStlL63Pmf)iN>GgVrJi$9_OijYV)$ydj%w@(w}TKUlNxXrpemXAsns;VjZEYWh`zz4-?@5!XN3z8yF@QkwR%cA z=+VI}i}r=fxCf@*-pMELeIvIREQ`sfcOlvabwcl$@YBFnE$s5PmLzpUXscRKG3XT) z8^wFpZYW+xn#0vc$0*5ArC9}O^|+C(Gh9n9MhQHZCrPin-cmGu-18gvTyTsQ(b1DC z_g;iJe6_x1&i!D*8{?zU)P_hxpJGx%&@)z5EvD=PxjZm49OM3Vd!hMF8Gj@kgCEWt z5u7yg{l|#QdTiG8XjXu#mCU8T0A3w2(XvH`UPYSWB$k5rR=MK23zUF}Ttc~Cnbfh7 zb*!x?JlFujD~eBI{)wXY`a$DS`d2$g*ZHV~t30?#LaUiUwKWXh)fxXrT-?glepy60 zXAmwkc+eMqtQV%kifg)4`1$O6s;wgTQp#VXR#wE;qqPxZmmH7Rz4KbWW^97G2bs61 z-ME>mC6*^2bOIoW`$&8vv*(LE@xx64UeU%1v4!QK#9mEp6;L;AcXe zBku6)#Vnq?{1U#nteGLvKkE1h9=a-&meh%?q&@40*Qg9n%Z>FvGluK&=b^VvV!Fi$ zhFsn!sc0F8!pEWYiy;klgHgZu|3=Loa|3^|7PYcD1uVa{PB>?O)&bE7H# zN>gH_j;s523JWr^FsCnG39=Cy44Q@aH?AB2kBjgyY0pNxY=@71!$2ojXCz1d^t>Ww z0JCMa3r}%pNwa6qI+wssga~b1yZS zT4UFNWsAIR$4>M%cGU@86T46%{V3E<)jzbfF}#3S=f(rLdOw8$^=C)WzA>P%7RNaREb*cUOrPXNkhVNP+6@bnu-VaeuDCd^GqHRA<1ARVwghvd4wY&|N2lu|J_#CnBgYl(~4>D8ZX8?Y^ zUNMWTx zT7}dCQ#Jy#0`6(zKsjUs6B%(Y++BWq9$md+Kl%&P_wlO)YCS#K>C`YZw{&*u`W~6S zLTN1;Hhb5zx6@)O@>pqxR)T5hfEm|hoYmTWed63WsGuBCgJNN3eE5iwRPL!!m1uZ5 zUsTX{?kk%a@s<6~8?mFhKY4iL{2cU>6jx8H`xR>-S@1Hs>K7V!Kf*pep_x>*26z>5 zC4)rXEu|VZ2>C)9dr9D%u`+cx$=W{}87{L#2+qQmH2{51SDJpF8`pE_uNGIttG`qt6W%AJ}tR1WQn*lN0yx zyEfWaq8tY^;71wo^RAbIW*sjIIW_5bpkOXYSXk`d$;Lc3{->($EDrk~TlQ*(AN5m1 z-QSwN0XdkDVxF!VDy-tZ!`&#hdukl8BcgV65%4B)4T z_W~Ug&MVoeB<8pObA1j~Cs(;<$q1M*rKZIKmK9@F!-fIbjWk`?O7-%^A5zodDQP1X zAYBL09D@;zYogz-ZEZTG7$B~htlL=E{fE}TBb@=Ml2CbApO(8<_)M@caOYqS*w-4m zSOnX!SIdE=n$mg!U?_Cv0}v5ENlEe$24Q|*!>UMql_IC7%(wS#QUZ5v>n_i>u5 z@+Y7+TbF#V(=vF&^SKLdtIBvXGe?jS&Zd!a_dk-2XydFxiAJ)dmCj3@E?+?co(mdO zHYVEP6+M^bGvV6jYnIWdAAv2SR@SVmNj(mfS~k{_yrIHi*}%m6Ob>j(o!YKrc7=v* zNrw*XUQ2%WL+pMwe3s4_4sI}ib##LQ=wEzv8-s$>+Y;;wS!*vd2FzM8YCwE9_`T|! zOJX@p%+eI(T$2x8a9`tjuzy-wTap%B!3caMGpg&h3gGEVCMeo2Y)sVSD!RJVS6Oih zI{@WAX=7oRB=*YiSLWyFi*mvT`Qv=8x`@4NBgAwc*-(&ky&*Ya|70V%W znU?sYnOU_vHkZmJ+z@^xTE&COD+ecGYNvM^7yWEhB!A9B(&{KST81O6R9fHs4M4MY1d2udZ%p}YU^n!`ScS{*1T zZoKohLo_eVPOIJyK|aal5B**nLf700It#qPE!~A&-C}-zkRnn|=yj#0lWEI3F6L$K z;R07rRX?v9kBr;Je&`4`d?L@&4Y7fl(Q`M$MeRtH+M;VAi}Uk<3H#GEhcRH zC5&oN%Z!e82m}+_cuFPpnVNl%4ug+{&MVjJpo2A`D?&t3%1=tjVH)eWin*FAMr`A} zd2_ob$3wlVxjmG|>JKX1fx|P#)>(ejSKdu(?=kwt4Aa-?_XWc{9ga|pTJT5+=aTD! zPKq>a9l3mR(0*FfLvm90M5 z=Px>XeNv_3Bu_?9Y^3_r8OWJzzK!*DnJZ^_YhHdV^_!S-nDzsqYfX#??^69^c;lDk zHxST+pdh8J(MrP1M;RYTG9HC4 zJ^wbOeN^`s9nS&R=NZuU^Oxy~oW6Q%EPq8ussx2``7c&K0X~=Njkzlf!nlDng{n5Q zIi8p_0ph~@4dDre7zKJogUReu{W!qeu9@cE+mDEPPa1f)8Q>*j0{M{ptL_yap*7Y@ z>;5h;9dho8=uW|T?bkPB;aiu)9CdJmCrhk0T)?S5J_PY${28Fk!?&Ls{SssUYjTC) zkjNhxV>+ zh?mi}Jm1G~G^T83Ub-H3+T9U$?o#m5+1b3#$6)8zH=j>{Ud)I=Fotk26y)U0<8Pd= z%6V7Fu*2&^E=TAL6}W|d7t@EK0s$FNdxF zRc6O{aH;L#IPtn6;>KKg@jazi5pGAk-k8Cmm*wDq)2tbd1G`bM?;xM?xNzFP!)kmQ zkU!b8D2mrt77oL%#;qx0f#CgMJpuyT7`B&N?5fCY){}SsfDJ74rG5Ub?Wk7p$e}${ z)@2(%Q%B-gpO(Va`@gLM{-N^u@5>0L{}}oICo3Ud6>W>L#Aq-mUX%ua&<^D6-wywW z+~a?{XJBIc&$!#rRA?1sb*upLkZFMt3uchb=oy%rph6y>Wvi+ndY?cv#fDKR2@)2G zWDr37011};FbWEa8hAV@LQ7Tj-N}vmmh!7<7-(;lqkSQL-QfMg6r$peC z#y)nq2j$$y$D8c{dAQOdaPK-r*aC`?cfj1P56QFB7nrx@Tk5`o+(2T#A&SvoN(y`` z{!-HC<+qdy3VjrjQjFx-C&d^{)s`z;jE0DahoxDoCuXH3STzUf5fKeVJTH+4%?yrq z3sgy*n?_Q|NlZ$^9fn3S=@`~CWJQ(-4$fieHVkAXb!fk>!#4lHl3-DdR$b)WTF9MWKlt( z1q-%l)>@T=f^Rb`3Cmzs9#T(or`bP`(`yXzUJ0GiLcqr7@}GIiX!vCors-ULVC7tz zZd6ZJQldSG7k6&|L*WElDpc-Z#ljlq6`Ls`s<>FbzQjWn<`o%Lgr<0}0+b>_s%*Jb zl^m%htXc6#3Q5H2oFa!jdnZ}BK+Q(g=P+e&xmJa$jN(@cd3RCwi|4L7Z(U`6@R_Cy zE%FG5@91m0Z;vmu4`Alf19xjGD-sO{PyuZw*Ig(|zGjb4rJ8n9_`|CP`G$58FtW4r zXt;+6j+#AwS0iUxZ9zljp~MWIH>Cc%SdlZldkd#!W&G%L{b8dJkIWcabVy(aI)BOr zccmvA6K+lWY+f<^jbICq9$<8;Ef!{OT1I{48-@Zy=|l1_^%otw_@nT|1E7$}XF5}P zOcQH(G*0#-)I!)1o)y&n?*_rGBgmFpdeo=wH}$@ioRL1v*OtjNHI`BoOH=l4nDCswK-mEGJFV#ttyy;)0Kw@8J)_6oNrTUR;$7j3II1 zP8gz1*9_lxEL%UWf`y9%rSEA%@G7_H=?gCw7Aw-Us~Z~ze#kObiY!6?*R*$CCCShO z>Ro^P`OUqx*7;F-eSGuGsr`N&oc3+ zmb_rk-%nM6%~QVUxQCqrfmdT7kj@IuQE!GX_HuTla&*B~2$mT7%%C5=WaYg@6O#R4qK%k`KSd-KdWD03a71Wb;W!b9sPj_SB*UYE1;;U2bJ%kU6j2=OAx} zaZT*em-ZTt=md{%5enXLi0ZNaQkf9EjgAb$u16Pn^1D~TC*L%^z?SGxKbAz_YFiiA zvePYC$jI2Rxw*5lxZn6Rhhc(nUlAzn2O|M2)!@hK(SHK8Zz@(4U<+M@@mz6+1IRg@o{Li z_+8+OOr_b{GHr&_BnR@Zn~%>0(S6e82IR$IgyoF_{~*H9_y1zQ83e%lP`4N(lrcnW zf+)uxo7et`eXz$nE5A74;$p+93aw;8>C;&akF!alL-2Yiz~=-v854bjQjVEiMdeUX zB*bSorO=u+y@X$=%X7u^kUymhJhF3se{nI~G(ODMT-cyC!`QDBRV+W!7jB(^c z>jC=%C4b;O<_*yI264w7(k&+xopmQWK$kud0Kk_vpx$2q$UKL_lW4+z1{52Hz~b6T z4!=)|1k&2?ng}6dn+YyJd^bjgvya{TW_&{9&vj=H%@xqq1OA$&|SGN&@2xrC*QE34hiT==iW&qiK&W63!pf}^o6^%_PhYFg<-FYZriP~i z;|(hRjtoTg0%~H9SnSA<^Y)5R?ti2>69%K}WbEeaYpjZm_}y4DzeMC5gY`l>-Zy+Q zZY;RuX2y=ayQh31TaxthUQL&!O?W=z9}cJEYCe2>#Lk(sS=p}D+$8qeTnA+1o}Z24 zcgtmbPGtuRC+sm-8Eg%2hp-WCx7qTWkG8eS6WTRlpMu(9J7vbF*J+cjIiranOSK=0 z3>@`_o?5U@^{)%f9bd}%u%%19bpQj1APFWdQN^EKB$~;UEnqGB0c0d^?UjCk>&lI|X<_B)A|^uTqZJX|0m*$khqLGzC_6N1jD`TZ8teD@{K!UWoi z&%t_8JkViK1I=G1QsN~qQh2)@c20=!wFOBw#`g`hta!IQyC=eZA)eCEi?z87a=)k< zJN+%D&qB%Bm)TlX^SE-J-b-OQ$k#uWvM9l3KXU$xf`&s#7faXRbN2T?#?08556m@xcziH@or3bF z%a1=ocDxe{wfM@C`QhWu7+ys+-jRf<`h9pHz^k0tiVKgkbKh26&cG+Gtiy1%Fl;!d0H(~0PlhhX9khdO9dGrsLJIKl}m7aeV*Q$NocQ{Qqc@|06Hse_XQ_WSk_@mFDa7 zL!be$uR+xQk za(tsSgn8uINz1lKs$0^~R@G83I(u_k6kuAEaxB~!{Q0?jXRj;8BtHj8Tn-|eqe){) zlmSF>Y(dEf>KlBf)LEoZ=pX)&UB5~Bk_6UA0p|2&US!%z?P_8?a@oZhd&YNC3I z=;NvRLRDbB&si4<*2L^)pOUvCGk?qV*0PkDS`#i7+K^aW+j{9rc#3nr!dW2n6r)10 zE0WD%cAXtgX1M1;`PHM+Hz)h6Jw3Uvrkv2pfPsaDf$Iv>0X&lX@b)b!GZLdqFe?E} zCU%*+D>9m0x0mfDAsDN!Zfdo5XLmM_xHP%$cJ(BJ=`a?_{rSE^cf;b&#zKO3P|wDR z`z4`6LM@z0;pQ|hFY-0;b`Bh5N35X?BEOg3$q;4PL@QaGt9$ghcKAkk#3x*=TCp&6 zS1fF2G;BzEa6b!Keu+X>CLM9v=ww4k_p9dSTUs4#l+HzOTUJKL$Kk8tT>@K5otKt2DxVU}2Z=q-r%;GXZj2?2b*TlV)BzJGHKVEG6B{om`Ek(G}R%Gt%q z)X)~nW5e3uuMGhh7%%{MFTni2)$#w=ApM`#230?QRqFuaZP0fAb|5PO1A)Df6%-E- zy^N`yxr+rO0V5+LGYkEHzcL#W2g5%vU8Ci#ptI`9f4bAYfiV;BVrpA zgoYrbc$p46~zz6ZAp2zA|IR&F;#Sqh!q7nyN4kpAlYA~QKT)?==L3>5PTRXXSW+&s1U zq~C;wBDnEQA3s}822}U)8=-5G(N=e-tei2QsCzaCYlbJo z=lCu|sWl6KM#kT?OwCW^D=q%9*zeX<3H;4Kl(BW zwNiD=*sq%Li5lnZ;(j5lkGdMa-H#~QL=%(q7%er8`n18cwKWipeT9X6aop+XsS`@_ z7)nJvSZ921a`5+6Ql7}RXHcF$e7_-PJ>7E4B~{z2B;E%eyp=rOdX7Igy)``bD+jgy z)@*>iBw@eYGbB&h8f68#d3frsxh0RWO*Fo7pO&9xheY%&J$g;G{T}wp)=RG|vBf0Z z<^Lh=9b-g``YzA1ZM*80ZQHhO+qP}nwr$&X-Li2DQ!~k=-*@tKXFC1ipOc)N?63Rm zz1I3I*}-d*o^IcFq}d?f-W5;`Nl{`7&t z%z+nDFU8E&A4;d|YqsTuAc-Ot{pFHHv6c`Y38Bha@0kG{Ye&UA2#_E!DNO1DH#){y zqzm`qeFGsW{1^;Hb@;yn;e=r=6an3rQphj6lk$0-HO}A0FI8z~tlTJlny&ItN0NmMTQ>(}qJN*W-mk*%FHX!RQeg z5P~#Q%)E`(7cApwS07y>@g(ttZYIHCIl5RLf0M)mLrctH;EgK6tc!vR;8rB3vNQ}R z;HFk*m@+T;A{+P`u~!ISLu1a^!~I!OUofAOkjECVx!~takp#`BDI#F7s81*!_<-aH z_sHKXCn;~_d$dH%B8gVBu_j8%oGgaHlPsZzRNO>4UO1`n6#Y?~dI7l(zLs6q*S&@qHC@>qf|`WDQ}a?|p2=9b zz#5Gp2tyM<`m{aR;#s=QW26(F-PU@T0q*d>B!)oZ31PIwf#RhpC?praKR)U@R@LzI2B{2j za6Y6ktv(4(wAClDP1H%Aqluyocx#?8=-YNVaA{Fi7j>zrj;E%0XmMi_z@+O(8P*ZR z#@yIY$^tsP{dk$MA<49+W51Z7S%9jxXiW? zW{>7DAMN{Z9U5N##3 zgq4UV_a|5aF&Or^Nyeav!I+r{kBu1RqZz)wH1}ejqQQ?`)W6tnHiP|A(QEuDdgfUJ z`}Kt+0YzdmRpswHLH24r8fvzfz|8PP$3NNNYaWjRm(zcZ<-I#w&#~52uZh(*zng74 z+YdylwAipYJlk6rk?7b@DAZUk$Ol?__9j8IRD)5r_4RxRPwdwal(E za~4{A#q#>3lEY-PEQyUy_Pp0pXl6T;_EPfobY(HgqEe@Ukitl7;y4IE8O73$2O02c z{Li!Qy80Mwk8(pcqyzN%&JohibOmK1M6^NB(8f(6ROGNQ3j^WN+GKItZ6LApiF1L$ zimK6t;B8=LYmGIgY{OpF>q3d~$TbxuiGj2Xwl(!ezDq$q^6P4$sJBKb{j%k>Yu$~G zH1Y1#7LC=#@dKBtL*jS_l??1`4$+x3j?lL`0nH26x3D9-e`cji309*_H;6-*)69*y zzWa>rXRaCFl`xUDb13iC;7xr4OEbXk_!z-5c;R3^tSGYV6GXxUpOy5C*?j(p%)*3# zORyX;(OmH!_AIA@m7^GMq15Y_p9jN)ut&9&Sf%C(-N0{VA0NryjJzyGC*1}X)J2Le zm6?ii9TwGnre2IK5aN{?!zTRUAFqB7{;_++m^nB%0&A;21_{jz|Bfadl%1@W*WmH| zC_#V09g$HFKq#O+&`T(KhdL%8fvPBE8GJv+0YZJ8J;b^kI|vTMo-nO6fF#f%kYtFR zqti73fz!3`;1LKe5jP+%+3yf?1I8@n@Bl12{{h78O!9~P9f`pWQ2j`Ih;%X>pjae0 zK&HStTmCT+JrG=UZ^S2t0dxU)h+YUz!Z)Jx;{B+6jo%k#`A4;=z`1Bl#9(*PkT)Ri zsmZja4%4#*tD5XiWa8{+pm1&WwEK6hsFm=M8SD&pfzF47$Rtl;0%L;i!yu3c3dkhE zQT;o;g13q3kWXXM@$+<91O zT2aD&i1Byd9ptEwdytti4fMOy0)Y+)DJBBScx?_EiD4++IaIEo$)E-;{rC^ULAuzz zJ)bots^4gRjC?;YpWM$tjM!lJWOth5k{a=(h790s65joAhpZxvGxQp!NB!M?^8=_M zaaDI!LfNC~HFHI3Bjcu!tYk~<~&`%tH-@fb8Symk?muOH^~C#S9ERx!0+JRJIO zInZ&gwzhKIj9O^0EX{G!%`0J?@KScMc$*xlc3N#`y%9>>T3Yy(@1KipTG&`veX;E3 zy1ww<-~KA~FX~pj&1$Ly6N((*e!#_xFopz7;@hSuAX6Y)Lzoy&CmR}|b@ixkf~}RA zndVkn*zJ#7R+dkcD$l8JnweXhJ(ZJVX0Am0lvT%}QO{@eRFtrv z6ABA&(A*+Eq?jKmFJf)#4mPfN11SUepCz z-0s_+%`RQrwNvhtsC8{OSzF0Ebvy;-m4hog`1pz)mTgpvSyJ$Ka(kBl1h0?piFqzl z$==SOyvE|>*82Fn#q9kcUb{9%)$93F5%hphS0cL|Te3QKc-w07r@JwEK{@OxvUhOb zS1%ih_`Y-2P_tkKdltM5c=$Z4Wd7cG6+2#tAdVTY?X(-=J~qaxFAtE06v_xV$`@mr zHfeyVnn-|X7DP298m6_)M-g9c_vR0EZ@@6X)4FJBR)I4H|GC`U#sl!|MUiN#B-DT3|BBktOB#jb*T zlir1S>e`Jc%;IZWSz2O~fUI1n3yQygrXZy&b(CGZ3yn3*)Hpl|zycqP#jVY`Fk9p8 z)^jK>AZ~JE$#P#kebg$0Jb~F5)i+l=l@t36BeNgT)K=;CIrP~1{Hu-49f~QvRTZ?$ zna|1rHA+EZKRVJ!N(FojGiHp=*+2v@HE=fO+WE5EOQh_jfz|DHza-PbRti@`C2|^v z|Is5PTRgXkgs3reYskkq5r{uVsY#LgndxhOf?NCZ=Eu$0aNI+FCHX!<7m^_2@)GtX zx?#_Fsu>1B<^Sr%(KG=ZumTN*rbw0vHmi)SW_JDpV@)5T49z!A?ka&nfUxDx29-EP z2t8-JNr6g5MR#O9^ugGpO?Qvd@$h)XsyZq4I86|mvAI=LF~L|U82#am~%|iCEDf6%yEm)%}h2`0z7b0dOy8b<|&9h=gKTX zqN~;B0F3<57WMhb`&ba^eURcETaQhDQe_xE0P~hZ)Rs6l@NE#~MDYs*`;vk3xWP+D zc!v{^z!!%d*JY}L+YU($6qNir?)lcYs2@McH>6_1e?8IAt=@8Ri)tI*C5i+BP1d9` zlxSzjGsmd0|1hnqvV8BI@d3XadY#KV4`;R6IowuXA??Yl>9kYY={NEU#m7(od0ZIi zUGD8s_2vl1C+K~UFYA_Frr68mWN{J8d1%)GEv=}2)5KM%vRpnNOq%0vx{xpLrPY0K z*7FwfBX1sizhYYBQ#t2QJO2DM?<@O+)Jw34<3v2WW#aq1uag#Hf9!}!vo96D6R`?x zOne-A)`$PwxsQ$)id7NgjU2=xwIjfmMtw~1fBv3%K-V!5IFPeab=TrjNZ=e{6e z?53(}t6t>aA&r>cPU$R~h3%YDQ1^0j+BU_O$DAY5xfS|cHN(Ts)( zX_N^c_e9@rAD&B@yt3F^g3*X3QGWM;rBkFj^+n41tUTQPd$hC z`dk|e>#)tN9L-hN^5b$)*WXRx+`~s+HvA~ty-mUgWj2iKRNDbpCI>{bO2->#_jqoJ^Y`)m6*~~a6M|r&#rrNcB?c5!`PVLXLd2LyXUppp*~yN`jwip_(mq#=hpgrxx!w&0vf2{Jd+nPyO2V?5f5n zsaEZ*g8nme1&ywB#svzoam>kX(+6Y|^FeAMl-XZ{wWWRraS%|F4+PO*FXi|~>85@$ zWn*vQ^sU2?HrCpMEqdJxt1-{9&|8XaNLJr(n+En@Rl70(Qs?pp52EcJncwP5{-fcm z3F%U$ifo^kx71W~GqdI|9kqLwy0}MkvtBKy6%{_W=ZdqJm)(!E$GH260AUA5`@P%( zhDHl66cyr!qdO||WeyXu#zOp5cIjNxckS8VxU)^y2qq5D{D_b8wrR)Y2_mFFXFsvkmEdC+jp^pd5O=58+{VbBW0``f6zr(L znAmCSZF~LefLYgUjID*$&Sr;6RMYEXFL0U{-`Dc`N$+FD!1q6;AmCJ9)_??Fg`t;` zZQ664g!DZ%atG`dsZ!fW%m$;sq7xm#bILQ48A^`40;3crB`erHrfecF1Si!J?7p|9 zmuKHAR&@Bgr?xb8E-U}MI{6GbhYLdCSbi+Bh*A4&-$(0J%r1G0<8nIP@U_M+Z~hw1 zu)5mdTeUWHn?JfMoeP`Eu;WEN*=#bR#^stvFh_?5u5h&qgJIEe>Ws*F0paP1h-f%m zua3s{=C8R;>S!w?K_sKBTwDLrB7BSX*Qk16Xod~9?vQA_6#RS&8H6)aYbm$?y2r}9 zm>~bXKGnw!DIO}757KXwltp>(>iF z1*NRj&h#m1MS-1L2PA3SE(%mY*%62ZGw4y2vg1MM2O~Ls`GZSDLR&RLj-*QwABKH(wv>Nvd~rk zhH9d~Z;9=jUFD*xE7hW^cxs`{gqq23#qxM;!8NpczwV-bWUG)7 zgUP~|{qYL?h7Z|sxSXt+TgMGt{0pC!_|#Uoce&IB1lweK&t*OHdfaz+GalH}Z!7v5kY2bQ1^?B$b>jf zOH1vLuGXM)r6U|L40}QP;?OK1*9nF3B?N91a>e2~A^$*L64958IIRI{N=6NMYXF_9 z0q!*zh^pG;xH<~+!UV0Vf%;Pnx~0LU*Q^h&TfNuxs}TILK)W(_ut) zz34*gmi3fXrCuM=w3%xH;Tn-`3R~AmKEZU2o++TRGL^ArvMy`j{pe#-=Nl+x!0u1d zhxKHx0J}zpysdHjm9(u0b=3(>xUGcohEYTVDmyE^>ABAzjcyEuKucttEj!r~D zSiP(6o&E0NMD#?*Pms!ObePkAI<=SP@g~^77GyNZ5zLFkBXISP%F9lIaq8nGMNrlc zh#%+F)qVQoB#ue!tfw-3gZyXwQ9JPoM#{%Bu4EChxf^>;%-9N(rRdHaSW576?dry` zsDXD`(}Ux?$({)vm8l3hW$aXbZX69?tNK-JSZi;n;8151_Ipc@1hFfP#AC&cHSUa_ z3%yf-OBv9Hrluz>N(WLGD@W>9zFhSi;xpj0uM7TO%~djMRp-n>rC$o29!qkZ8R@Fe z5^G80&CL(sPwzR?e-by?{)f2nKbJEY{#ypJ>L(5WK&%(q8c~YZ%LYh^xDdS=FSU)RN+1iQ} zS&Wu^%eO;JqQOomaqTRVcbonA_496b<~$cqPzcp2gZCFR>wNd|v}aZ%`V(Pq`)Nj` z>0*rzTeuK(@9!gYlatbpi5}^qb>ZL1jj6WTpG&z@c!U)={i`r^(}$4#Kd?W7%0G7T zw|)MAKYL!i{L28m*PZlj?ZtEvN9Sb=KbKQ#rH@>_Z9;!6t&hL8eJuvu>%P^_e?WYk zc=^~Kb0+#ag1?E0j&=uIGD321qxrujh8J(I5vq5F>3Bo zFLZU5p7N4fD;Mlkzl7&R42=Gb-8BaN?uQvR-KUARYe^yx3^+bdpKqs{0b( zUh=ItDY$oQ(TnWrZ!+ZaNfJ-Ak>t#fFqLt70#wPvNEscr!t7up=W6PBJbjpmUfz7z zdritKEvu=}CnuqxqOc`Z6_@8mj}kYKVshgpV%dVyCQGm( ziXMx!$!%XgOp+?CZU#7f4_sc7qRK24h=G}D4t94g>694Ol;)>uT_nJwHov;v9^bX#_JQEGBn>lF;{a%f7V7>ZGV1>3HhdL!%yvAw} zu$vkt*Xzzn?4v6EQG>w-!YDgy6*d;LL-7Dos%R$qlLnu8uW8#Eq zh3eI96FwgyO^Z7nXU3$;n#^)CFAU}+5F2GBDg0rrfd*d}e_Ff|SBu&tPpe8z*HZDQ zC_RL5aTz(zxMgfrb&x8nL}nE))IqJ}2x(%|(W9s;b8lQt)vU^n`Z6k5>D(MnFC9Mg zoSmWF`jD-RY7ONmSd1B*KuVRMNtI`xTJ9Ozz70wN#p`0zBi~Yk)2XK-kxQZqsaar+ z9@#!hYpJP-_7D+X-6Fsuqk-&~f(k$&)R^jZbiPvQy&|Ac0~Hy8A#G%$fj*Zp#i6uH zXpN|07bj~P=}DNdLt158T@r3xFD7R!`X_rpAL0nsvU`D6(dW~+R9z20jR-%<#bDQw zyhgnt)UKsn0+FAV+vY+#VF=vMXlk53wdNX11A*!wpJ|S0eS$kN&MUo_JKatAgX_y%t5$yYgFKtO*mWI)^%an7W!4;tj#>FXNOHg6j&SARbku~`gLL6 zR*q{!^j5u1${}404v|fU0>$iuZG^bjjjM>eHH4rgVg|^t=sQx?c=vy-^Fdgy^Y!Y`8;|d{e7Z;9td|ceG1Vuo@&=wT`9k7;MCRwPR}$n(z{5srvRG27NhU3cUErQH+dO5>KH1adSiM zDWu34C>Ym$sfC_vV)wFXlGE4)w}JcfzQNL9)7Bg^Msa8M_ackk7#8InSaP2&y?lfoVhxNRX?sJG)VlU5L^B?qGQY*@8d3 zR8-iVZ?@Lo8cb%)VYAeHL^5(B(%s#Z!!qM^pV1j_U7V>Xme)eP0ck6lgI6h3*7)YK zbPZ;AZL5dQ*vNY^^=Q5|IhZ9oN!0t%b>`mUj63DYy;fg>4zDtO_2`|zK31-ChS4KE z^l=YMG?u2Cep;^jpg!-mi{4-g_`qa+lm)CTS3*Rvs1Y1V;)HR{tPA;_TX)_t_EI|^ ztyK<%Yi@zh8hz@%nj(VROrq?&uQJ`|(8+p!P@$z(S5RYZ76oqq>p)RCHs6f^r*XTz zeYZM9AB51{v6W|6w0;P?uo1uObHyw=PB6#ZI{u%3+~$J`^B8-iMDP~QXiytU%@Hel zGdCE!X&nMAa4{fA5b{f;Jn<2LrEwq!g}=lpJ^KU>SXuheezOn0nE?(tFbT@!=4%Mk z3syXnYp6%y!sWEmIrSq7=NNa$?mkNr0EcdpK<=6`{fHG~y6G&UKadl~G=12B$0>cf ziYuu$4{k|p;y0RP`psvflLBAD_^GZ~K z8}6KDTGKiI>9#!1fupV9+kWP1o3fk)HAg(DEl2!?olu;V`&fYVTOe@8orpbr&BedO zzZ4&7xZ_V-aK;~M1Q$rXfBDJ0XMR87Y_F@n@KSq5`Qia*{Bpw?f8vUFhP>s9hn#{l z9%Q>pfqFKjirJ5>^+^{#EGW`bbW92z6sx5#!UMfm3 zOJyc(Uiz(IhQ$?+Mtp~x1^mN9&*ZvV2JD!WDePWIZOndFvJQkr^Xw9WRPpvnrG# zcn_1Z4l%PFOY|;Tcj(!9`F8FsOa}eb9Tae^MJ~4ocZiYi!Ly?7tA((VGdFwlWfRKc z^O{bs9J!{e`M+2+0oC#nBQY_j{DRuX?X!}6h*TA@!I_%LG9MqWts2##wS~RCu0Qk2 zW-jWX3k_v`eRXqX+dk~6KZi4yVsN2xT3lOmc-a|TinU>~8wo`V+Bd`B4@X92avt0P z#6AI|!a`FS+ev)xEmc+|D7V-5?qDy%dPFZAJsT4v;Fz-YBAm2UofD=j^F&qRGceK|9V~q`yH$0%K0_LT*5dY z+&)?zVzUJO$nwsWMf-iI)!p@pKQ(=}eP7(~{JDMm{Mak7A~2m5yWf4#4FUivre^Xg%Ibn%~`Ejkwix~bnwk{Q`Ips#L{*wiK8fz*1S-qJ5bs>^w5evHs9P_mWtw z)3KH>ds9OHM^4D=+K|`TY>A$xP{z7{=oo3ifvz@BSVN*E5wtm{qh0cqTQ)MX(!ACs z=+G$$?HpCRAd*=E-7HRaU4XYK&xk{GG<@mFZn=vk!Wq4^mJBZ zWP6yah^8BM!fj`(z7d=%!U?|%TXGAe{zyrdb7#Sp4*d4AD1{MG4go{%4ExG^uAl8l zeEyVbzbE5`D!V_+N?qwftUjiUHd}QrN^i8NqVB5l%-G&`==qJIt^9qK!nQV#)}N)6 zErrolxVppHM7k4I9uCUFR7hf`f@7-Ums{FqOs4$Ofw$fz@$?X{!#BxdV2Hn~nU+)b z5CZ!URr^~?vqr@JuL65b>u+S>^YS-2btjN5+XvIWYgc9+fDH{#o5gb(R;|$$nDxQm zbmjLmbvUZ;!b-Z>J)&lNZnM=wAIxj!k4H=J`aCv&=*rdgEa*tCfHzzbu2R*Uz5Mrc zFj!VmRyE4CJ=>O_+_A<$OY{}EJVlr5^|SNoDlaP6r{KvOka`J*l{3682Q2f%*#5ss z<{f?*Eo`y>9G=9;D~!kJ4GSYj=`-b#h@rTghW;+I%W52?;fQh!&Q=We&XU9D@zs(UI-3Z|)>36y)X!3tHi@0B%uZHC8gij0hd5ED zmPBj29jVzr@|AfXe0@3RUOts3=ICt+wb8o@ZP*XBOl%}Y{RCCp?!vDbFqpXt zwds7n{CW>iDD05d?gZ3Vd28IRCyv6^@zXCi3qaa9Uul!P$UKl&@ZlCM zHHvvujIjW3)df3sS$E?}pt_gx0WK1Q^x6X&gcR`uH224Q>^~fES^f`f!i>L7NB`9o zn4$))j;w~33owySL}|2adNth~36CPL-Lkm~zT8%hYOR72gMdUrLI@9t7(t$XOqPD< z8v!T?6eJ)obfPdKX4RtC66M0z_F{F}+FrZ3S?0EGfREf9*Rtd4_TZCrJlpe{{loXe z;Y166|0v|ny_?>$fSpodI1)G?gH$0)tLg=w#)O<I+Mk$^tIPN5~fHs3RyAv zA~V@ovRb@YHB4c_V42f|lPyzPMv1aq2Ps26SC}HHTz$e+vMiyTC0V&M-0GY6yY52|i`8sh zZHR}M=-|FTfRTTQJu^b;4Ay*X!E3?Xr{NM{q7**=^TAt40WH^LdTNq*BYB{UC)HzjQA8sM{&3Y~7$)E&K=N!60Lwn=8og*ncCQPBI420)*{nnqxko z30c1)eg%5p-aQL{Jozu~#V@MIA2Bw+>UBSg&91%Po$S`>K*WT)5?rfTab88FpZp2Q zek_kH_Roll?Z6owa$UmKD=WKIEKBp47U0JI6{YR)oNnSYp<7W_wA6!I>6_SubKReC z`maFWm6o_I+IC6^YDH_C1PNUx=Zb;ryqayMRBZ z<}Upt@V5$d&fE7Uu|gdPu^BI@*!6~4(j|oZEXg^gXHyH8BVnzHL9g28mt3E?Pg#?X z>^Oivc>VXs+D-OayH*yE!jZOVpDf(EihGrWP1pU}#DQG%So*XzM4a0@DmL!_C}P?J ztk*3z;)$S)TQ7C)hId5K=X}6#+Rvt_Ly3b;JoV>+k9N5YJ6OqVn0ieIIM`ulJ9j)f zKD!lmByTvfb88SvaHZ_b>(!RjQd?#W#%A-^8LIELE^sD{nQ$~dG151Q%dBwwft_$| z;RtA6K^$BqZ@L$w6jV!HaAIo5X|BjJ>=dq^Vfli_$%qp;uaDeIhe!Nr^{2QE-~tGma5o_zsCdzJSQu#qj948*FPgEm4tsv%iF zqkc|iFvIf{#rUqh2pUHT>g0616hZGUzu$`DiX>0c&xyc3)e=!sDW1j;>GC;%{lGc! z%X*8zsTN3z{tyXPo%N>dNBAsA2wHOo$ExKc>!ROF_3F1juaAI`jitXCI&$UM z(R6fcyJ!>x*#c=%)&C(o<>g9+g~%C>H68O~Lj@b`zY%jeh9XC53)nPJ8&ueP-sa4?7ggk0KzgK1k0>hxm=aJln6hV$s;o{KIT20`+Fc9S>vQ-T zvMurQ1NAsm{zE?W2n+tmB=RvB-5FVl#5GWBidcXaJWW=QL;~ckaM|2mbva>_GAoI` z3oh79@`U?@ZmW%gFR5Skyp-muTTbb53-_)jz=UI>IbP5OXCABkCOj~IOD5eJago8s z{$<$3Rt0E7WI+AFV6NPXKwDGn4c+TlMJ+0uxepAu`u(_EBiMF1Kv~PI!D%(E86g*hdFYJW z3nU?bj*zhr-H9LjZ0qmPY7)s&lwsQXgf99n&Fqol)c4V>+0`lA9VI-ybJBV+#%V#l zgi>B+pq4M`0b*gHN*I|uQeDarXKate{H`T1@on!fov(-le z5hf|~J-`(J(qe_9QlCGQy++T{_&;UrCX#wE84fx=tB zhR|`Epbn=FAcW-@xETxO>=;{M)_2f+dS+(owJv4KW@7u&$?f*D$9L(X%R8A`;O)>q`{uhuN90ar+LT(5JX}(JWSG(o z{dU!e%+o2dFpSR?@|OX z1C*odkwd*P6uiWJO3swglx(>U<}Xgcrj?vsB5L&9%e(-XbYGvFKCGz$XuXeZEvi*e zegINV$Uf$3DZ^!-0fZvnagoD9P>~p{q&_~^h>96`e@Gzc5$HynP;fxfW-$V_ACX|RtiHVD89aAE+5;q*H|1glO^Q~4iHs`pVx&Z`Nbf52( z=n-DFRWVjhKBAp1D`pnQeHAp!3TYvbyn;t^c^P&ljtstRhI|q5D0jklzi-S0m5y9b z2QIi>P!iZ7pJuJtm-Z6r^-nq9+-uUfnY7z-tzysMTm$E{rCkBLq>!_SW zH%!cWBiY}O&zDD#&*Oia zIguhvZha`XR)JH`ISvJZPEE2(EJ{h679hiRy=q2%3{)h!UyCXT|YmSmd8E}?>2tvD(P@}c$lRJRWoz07z%Y9VA$6zD80!-{=PTgP$308;9>yNKMR-aV0UGzYy=c0S zIs=qs4;^^74cWlajW`lav@R)3Y2s+4L{hR&g>u}`1=E8&g*!p= zRQ{t}Mc}4z**K!QP+dh<@x-{dI=*^gl37!+w!pHoMNgLWkqSjqQO+XS*m-4KxzVtu zI=WgRZGySDR#4RUQdyTbL!!dPxV2EZbaiq(86|Of(%3jeR?UZiMn;WT?zhLP`QaSX zCiCw-p^fG=9VrvrA3jp9%khTnZlj7$PFxLHi*d$`TJ?g(((g9*pRG_~F|0=LjWA<^ zumt3Bw*(~N0A<3KPxJXgq3Cd<17w1|qwB+(VFib(PpQv7C`(X$C@ztI2kpUMHKfzL zxS<_Q-Eq93GW216l)+uaJ*M(?B^EKLb7`Yc3=3*REm=_b!BhQr5W#>BCePGC)V&N$fUEc;*o8mGSZ1+HG$Mry5HWI1z zMXB`Mn4$j$xiP>I&%OK2#_%P7Z_=7}z^YZf{YK&D{ZA^!Zecx2x&DN!2}{*O@Ox9x zWe=Fx|DsfBQ-pRuShw9za;ey*rs1XK{>@8cB-)oRiWWtXnSi7>4dJ&mM2PyIao97=FaRj%wh-lOAyDL3!sU7`m+SNNF zypD_JMV+ey2oK@14_&W%{zOlUj`eI=+pu-Hd1nMxbV@*m-h=7l@**2(00XrLuoVqg zGsMqM-48b3c@8=h{pb9bkN_pTzPHVZFCk5|p;ucfrPJJpCda9)uJ4B^MFcI|p*x%j zW2O8lES}7K)_ZzB+Fld48=J7em3UFgIUj5x5=yS;q?TnDGrisY1-FVzYy|QgEUJ7S zthIsP`VX@-PePUmQ_uh2K&X%(AA^)6UMFeO%ifI0+q1)qTiu6SUs)*+=raMvR~x87*4YqqRAVQn*1V_gj10 zZ4c!1S;P5X9JH(m_DLB?o9F(8&`QA=;M~huE}pl`c*IywwC^`SSKRTxj&lx>p=sf0 zF+J}|{XfrI54@q=><}K_FYxw?A8keOg&#DV6Fxy(?O!=Z^mw`7(A)sX4z_e{YMC{& zRn)_jvmm<}c%gv>9EacMgKyNX*D6N~jZxYBO8nyLOGjFMux$Oe)pr`0+jKqFIpp{w zD?wOp0&AU>u}HThQ2leff1!Y{322#sI&fD&WQ2s0zS?e2WAHysMO=CS>x!R1DV_I( zj#5-VWgoR4JId$O*ayAQy0s&`w3!C9&XX6dsO#j>P59#LqPqvAXO7&+{@unEA*o`4 z5=QqkdG3PSBj@?tNPJqEZyFD{p`v5b8q&l}uOB%+(t4}BK`Ri{lQn=HmXp6Z6_~aE z3q{9e2BT=Iezqp2J#&SCuZDDz>ET1dJ*tJWA=9@JX+lSpx~pI#L<~30c}?eO7H;aj zW{TS0vX@@J0heX-6uGQoNo&cq9cJo)%nE2#P;TrHFsdAs#xn%vmP$W0Fb)XA5$o(_1H{UaDMx%Pc_-{mR--1UD zJ^h||ySZmURj)*%RkK-i`TeABD5z0ZTF^1s&=X z<#teb{O3^;B5k`mz83@w$MZRlhP80qPMQ@f5%&IAl>tW5ul051z0 z%YUN?%xGIVZHcCS_4WbniEbzN`|_14RwmT2uZ~9I@{w)WzXhZcWU(Zc6IMij-M(hq z#)C-kquDSt)fNIe7u`N?Z?$3j7gGuo`XCAs3KbMn8dEpBh9HGF0MUfRu$K=OiChqw zYmqAnM|If{ipYmJhA0Eg^u}wB2nM7!boN&?@1keo1XDMIz*|7cka7CMwzD^5*F&}v zsL?1JjFTUd4*2*$1P=S3=QL4qNrHg7qMpsfywL^^F$1=)o8gE+cieh*ZX-vB!i-OeE>XW@MS zBBr6je!)zm#ZJ?Yduk7M*to*6E@J5aNQRa$CN2RQ4fG@7J^(tOI6np|2R>+v2qk{! zl0X|MPOFKKnvV`_7h6vVLrog}2PR|45~wvHRR@s>m@2nZ0%KQ7%4VLF=Nuywr!)ac z2kI?graQ1X0TOhAUi-5pIT*L zX5!@c>hM!6#V0r!>H9T-7JN9+|DuGf^<35*E%;;x?$0n176e*3qWPa-gZO@jXm+xx zeK3(GAZY;&q#>F~C6Mi+1F?vHSS$jdp8NywU`72;5Euq|ctbFuS~%Qa$CvlOBC)@W zJpl>wEUo}Zr8#9H3J^kkz3?$agnL8;p*=Dz40%rw7(i7pw|oX0___b-u{$BN2ZDby zRA631p~q;eFcHZ)1AUJ(!t5b+Gx=!G;aV%(}lf1YqEn5rGg;2gDB(!970D9J1UT0w0+P9Z+}zRyaBq zYY6)oLw!aEMkb|yULhjOPKohkeCB&HU?I)ixyjtIl)nXhHhJba{WuD$0HdHOGoy*h zT=qEAdD0tZV44EJJSxRB0!l-@G^#Kdpv8FBf+eKIDcolC1_>pZ-c&uPVulQJjdVRm zyC@>IIOX*5Fqm@b2v1GC{zXNS>^?t#7D%kP&bj+sw4@z$|N6WpNTlSWf2(wvGu|=% z6RuI*2B2>6b~4dGY&!TA$r(uYLRaXYT+EbSeQwI34q^Ykk_%MsxbvbW>HDwOud<}7 ziKm(C^KL;!^pVT&rimGx>pA+a6RTlsUchD#N9ScfmYnRqiqoL)swA_owv{rEpC`|! z0?$l%xrYO1cjqU){HK>kn-#v^j*RJlb~n3o9?yo}k8|Hi6HkSia3JQ920tD@%|Ffr zk0T7BJr_Uh9$XiBIMbDn@9vIDlX&cXqay$Yz*(uRCoPLi#GEQbGu&unU9VE5u&sp2 zn+(vGitK`*-LN8%B`U7?-79Ezm{L>rt_{ZOUN)2GJH!vVMtkyjkR`ixC&Mrnh7PVkfVH z+V&2wT_#WgC0`bc2pY}Xc6lA;FHPmOPHj}R_*qotXOq*V@%1!%a2Hj#5~;wGnM)Wg zYJ~EygI-moiyi>!ltBxQIU!V(D2&&^FKgmQBjLK`gZtO8T#{AB3u$?4<9@Iu8ZS(S zlxHfnHj3#f_Y|og&CH&ME_m3MUFP$2p1J$7rB5+*SoVt&VA?0gKI)D&C5o{68_84% z^w@w4{kIRjdBK$K+qNcFQlc4RYk8G#%Zf@6z^0ogO%Tx6$-5IWgpdX+#!?KN89Hmf zAt{E>zpQz2bLP|xg$Fv!Nx_gzHA|RB+}pkW%@J8WZ;s z#I!Ubti>Ginfp(5VLA?^f^tiVj>H5mLfokJBQRVoy^LxlkEu5Wm}oW<8i&*tjkfn# z&Mb$4+8V?^D2&i(IISWc%o)V21oFSP9@hxJn#%lxhRo)uqI9;Jz{@_XamxdKP|fT5RbZOkxMxKmr8a!Nb6dq2y_Fo?MHa znJO)4$-_lvB2_xGhasSWC2kqDEwxmy;GUT_L7Fq zB~A{2^NJJ;#}`X)8jMf`BG0Q>sP|AQ4h~aBrr##q+|zrz9%b<5ZQj7+!gE{vn&86g zRaxRv+dEEcv>6hd()A-J_cx4W}HzHfGC_y2RBxj)XGJ9F+i z_kOgr#E~8GPxb2<*msT*6fNydBKutAx>J_EH0*8x>3`ccVdSj0*--3}S;?qXTc6i# zzjUy-RqbD-rwVg4-?T%Tt>YfH%Ff0zhPuMW(t)Oj$>U%kY{?a0g;NR!$|B!ry+d%T z4#ZZ7eRk7AT`xA;*xDs{`eIy57Oum?o+G$LGNc09o_UHMX;yhad<~29ByXL1rO3O- z`VSqu$335A_LqG8r3t4SSXdVJq=HIoR(^Zd!x7-{WxNC8;-SGh+?3;fe;RWC4cdmm zOzxe#-S+ek<2gVaGZnJ zp#|!Mta7T;>X{L;!b6S)#$hszsL@Wd@~9>&6be@xS;9)xID%-asCeR?{)r!_FUYVG1WE zQ+wG~>%p>m;Kt$FP@DK=92jY3g*tKzxnhyEED3t3vls9@4Rw~Jd5$?)Ud zW}6I0B$B5$KE)*_VbpVSFIwo%1;dw&Jk5`A81Z5aUoa90i!MKa=Z-s}@9G;Dbs1&1 zux~E!9Q=d%V!f4v1Y#>sW@QH9n;a2YE#sJCkq)~PSHSm8&JIge(})`2_^iCf;q8!y zBXAq@rZZqqc^z=c8!UWcXBDnn$s{y+o7LMNFA5HL;+y~RvT2jty2vcMJ=Z7_{;Os& zC;Q{T3j<9}M|(k6(&HwdO|1Kiym2~ zy5v91BzYYBal7?T{vYak%HrR7iZ{utZtp1Q*WC*%%iGP`A9M->s$Cl2$hv+qC(Ked zI?7bu|3<$U*Q{N5cQpS>&lE9%)YBK>KB5~7Aa0J|IQbZjUR1Uc`i!Bi%SjB^;4vyB z6V4xeBd+E7o}BRcn$X`_`hK_^%|;<_4-wHh#QqOok5T#G@@UKTr46^t?oVOZGM!{? zdAw<%25rzDO7r-YV79#haqIs5ZCl-?QCb@Tz1yP-2CD23=lj(Vq^-)8`{&l8YMN>0 zpNmzcXuKecrou7Yse8mLv}ef=h4nDe>PJX zhLS(OhI1}8($Qcbxs5&$^&VUBFKrqv6}xJYrSfw^?e&@ zUyDinN)K$0t&{AwO41U?u?1c5VCxWULal>5Jun^G4z<``*(zFvjhXkVtr7{JO+Zou zL!lu{;>XLh!3_Zj;mFmz@Tl8hyTEMLgozn}0|7-L^+{KW>WYHfPXZ7TA*qj<@k8=W zYO6Uy``UB<*s}>USeT7vXM5#b3Pg;M#Da09T`uU+N(jacB%QQ!Igvk7Sqcxrw@&po z+7|yhglC_MS>Z5lje}6F1`@LFw4Ov5{#NI3PB|y%MlQb$|9lqQVYEHth!}3wF%+u0 z#K$ZE!HQmCdTr4By$g<^oA~$;3}A2+N0E3*=&xs2lNHcY)bO@ph+DUMRU=jjD%iJK z-C8#53MkMb2ftr6>Y{mInN*}@?Qxf@77oQYkT{Z78#PR*lul&ySXz3%8#o)3=3j;; z{~SYd8~Aoi549(HzR41VKGR2@ZIn%w?If)-SY_R$A6!;7AevkCgQe)=9@QL!lz;pR@!)CH(GIgphD3=-b<%g#);QAtI$ybTXPa3L@bTlK>C(w6T_N`Ft7Pmyq>PsS4YsQIRXdkt*pd;cbu zelIm#+;TI3w8&uSRgA$4<Mm@IlZthjyCimBrXuV{v@KmdYK9@;>EkOe70#*DPI;la-&ys3Nt<__{IxzwbklFBGVFJn0{eoAvY%bi#D%@mXB3N+G3;sk->|9Y< z0bCP6B^dPD>q%EL2Rq({Z^}qYs+hq@ArX%yqXq0DLtV&SBb1gSf}evdL~xnWEr zHl=(YF86VSf8?zZ!wVak0^qN0WND@{N{QkiQReOM%p>E}GYxC9F6zeH_8hCU4HWjL z(0hAPrq1r<6Vk5!*t#L_cTTMoT#{T8v^Bd~-@QKLiBCUyxw99HVk2b5?=c{i`J?21 zwDG*;FI}eMgmjahW1i|u=U8DfYC|UaM00Ehr`^;`YXdm)su2GGEgfV*xP8q_Vd}OJbp+!qO>CZ7WUzq+nm9e2n^ozE(my+mr znu5w~I1RtV;X3m9BKMg7+z_G&06INMmCIt^$T?c*MLBRZzD36rr+{Zjp@3)$UJRhf zfT3{s#Fx+7eu6t+hF1ZRSW`l)Zf+eeQ4U#0JmK&9M3O@@V>SbHi9b&-W1iDVHf zwB(O?et5}=w<;9t23Kr;w4vP8V0?*GFGJ4q1(zFxuiVTpzkwN^kEy5G%BrGke`2&%Utwe52!RaCU;W2 zzZgwF27l^!wlW5n2@`K=U9W}!CwJ#A(c?Q@bA7A>4cLqGp40E!;d7X-ZA|$VjGUk> z4CMOaVHr1TX{mBQSF&c^jJZ*_;wRQG44Nwu?mfD{zHMB^tM-7r*f_oxcM4a12nx_K zQ<4EfKzj+|x%Z4OF9Rb`$sAi(!IJkUVrzc4g9%oHbYEPmr4#3==6e%JT2yGTc|wZF z%&vgbMjdxO%fH5JMi1(wOcvAW$iGemk1@5O(I{s2g)n_hO9+!EU!uIX2^3ls+s zfBp6Icf}^bx65d9sp>k)lp?j$l602!yuP?;@`7KH2-yOQ?x%O^=2FP-PjIwma3pHU zS9Mlb-g^grpNu)CDrDw$8a$2&#on}XiL6;AKlmFTJ{As^D1J;=-bE-pphzJ+J?90A zoVF$wPB5r`R1C-RcP~4Q;Ct@p6>xiwks(?VzSo=(E}hi3_3b5ODRzVglDq}$)@Vo@ zFyn9r8W*F1b#~JATU~ha69LK^H#~lN+$?A0#V_Ymhp?Rrvk0BBg_|_3th?MOZ%hH$vVr9c8>}sy3puEtH zR=C2!DnW#FB>_>Iba#0hGvcz?Ke1;Q=vg|=i+F`1Zb-KDv~3rjP-okF!iq#%*e-V` zE;W_efn8C_Xqa|gwtpRhxqC(_!nkVtTRpO#GGK57joD(IxZi7|E5`ngH@BUIHB8@b z0ofZ&uPY$@;mN3I5?XiCp%W1Tngo+_;?C}j%%`?=Q`>nKD}=cs3-yV4mpCTJ29MSz z9gLssNN*t7sk@4@u{#G?^pg73sL={;z=b1oRaZG#^9p((w#kobe;8Dz$k>$QNmjxa z7jS#y*NmS^XJw4^%l`V9wF69mvD{xLJComXbjvkRKKKCZQVhL0Lb5W<9Jth1OAA=v zY17p8%asZ2pqfni;igHExB_?V^3|;2^(&seJZAGy>kiGQ%df(ms$xB=hF0p&wkl`0 zct?pw54|I1V0d-dQXCmn!niIircuR{P1A{`3yv1I!sT=9xR-4E(Z#$S_&tec$wZ&L zKgkSqeqOn!8;QMZE8smRMBX^1!-n~Vb8Bi8H|_&S9t-L`p$w77o?dLb`?bA3haysO z+~C|^uYW)R4b3w;fz_Yw+;Qc|lp==q*u+oBHEg+kb@Nl1=f*>~bDopv*?X15n)d0I zfwH_z!zpxL@HH+lKl%ZBP^!~ks+(@>+ui<+{03R88J&8cF1d|R#FKp>NT{fH|KC{i ze{pR7JGm|M-_*9G?Egha*m+A?B(m%s7u@ytFY>696kv1$mYTyKO)!B*aTIF#vwKe&5#B!a+S zzp!=KM7r{46voYH?JL9pB$yNygXQvc$A1oAIOxmv1wTitmz1yUy$T!7lF~VkC9(U# zTP?MEXjCQB>x$?I%jl&E<&d~h&=p&LMCM%sygEDx^tc$9)&K2v?hmN1d`^By9w-f9NG zS5#gD-az1Wf4hSSonxr!&grPjRdK1=!wBdJc=W^v5J0jdIie)UFp|XZ_#b#Ad3@e{ z8cEDPjcz+MB>}te{|%G>;`;qBOqv)tIEsK&&0pBdI@sITNdase002oxS!r=`QGl(K zt*ofDw1cRam_6|Se_<(N0D<@siT#=B7>Iy89U*N0DGf0YF?0!WU=#lXc4KofHVHOy z%l`xQQlkI1pjqAO$&ZWrB!o`ATx;2eA(8y`l5LrtNA4pzOBX@ccd!whlu zeD-T!RbRC_46t@5KQp#$6%C$5qIV_Mf_K{`_Qu-J-@Wq-SX5muA*$WTXJeMH6|TVkc11HK_QNI{B;a`~~8bXzk9~U_qy#zrM@1p{8rwZi*}vl zQzBIC$)2^~t_|=*FDc?FuN~8e0Wlf8EwRTjVo%e>@XEGKw0hmgdfw1SFL?<#ZcvhZ z7qv(l^^*P2M}we5+VXrDG?ihL-f$!t6q2DSv%%Nte)0)=?giB8$3sxiZMeSgx3Gx8 zcqypc@Gpvy&U#a-+mRggiZ3U$d5at=5wP^!1wA4@Wux6-fAO9>h#GoIpSel%B96BX zN7qgk-0y2r&ecA@$WEzWlYB9!KId%rqN(0x5h3momMJw2g4rW^B9W!|E{7hwinYdR zEFP_9Aji*W0wcPd&Qh)$7+T|%kFvIvaaxx3b@|+zQpj^Yqf#rAJV>iL2$YUSzIxT6 zwf5QoX?tCr7Se_`<4%573aj!I4c7#@y+u1#cI9?f!#glbMwJ4WnoE(G#HKe@_or$% zvx8cnGW>4E_Ku%pVII3RMu97PHBI$~7pqsk&UXr`_m3Ue672qGY54lt`1l3+I5-kX QOZ>SPNyN>qrmIf$ALnatSpWb4 literal 0 HcmV?d00001 diff --git a/tex/main.tex b/tex/main.tex index bd7a373..f01707b 100644 --- a/tex/main.tex +++ b/tex/main.tex @@ -4,8 +4,11 @@ \usepackage[top=2cm,lmargin=1in,rmargin=1in,bottom=3cm,hmarginratio=1:1]{geometry} \usepackage{scrlayer-fancyhdr} \usepackage{extramarks} +\usepackage[ngerman, english]{babel} +\babeltags{german=ngerman} \usepackage{anyfontsize} \usepackage{unicode-math} +\usepackage{amsmath} \usepackage[scale=.85]{noto-mono} % TODO find better unicode mono font \usepackage[final]{hyperref} \pagestyle{fancy} @@ -34,11 +37,26 @@ } %%%% +%%%% Code listings +\usepackage{minted} +\setminted[haskell]{ + linenos=true, + breaklines=true, + encoding=utf8, + fontsize=\small, + autogobble +} +\setmintedinline[haskell]{ + style=bw +} + +%%%% + %%%% Math packages \usepackage{amsthm} \usepackage{thmtools} \usepackage{tikz} -\usetikzlibrary{cd, quotes} +\usetikzlibrary{cd, babel, quotes} \declaretheorem[name=Definition,style=definition,numberwithin=section]{definition} \declaretheorem[name=Example,style=definition,sibling=definition]{example} \declaretheorem[style=definition,numbered=no]{exercise} @@ -52,6 +70,7 @@ \declaretheorem[sibling=lemma]{proposition} %%%% +%%%% href \makeatletter \hypersetup{ pdfauthor={\@author}, @@ -60,6 +79,13 @@ hidelinks, } \makeatother +%%%% + +%%%% Bibliography +\usepackage[style=ieee, sorting=ynt, language=british]{biblatex} % advanced citations, british to make dates DD-MM-YYYY +\usepackage[english=british]{csquotes} % biblatex recommended to load this +\addbibresource{bib.bib} +%%%% %%%% Custom definitions: Commands and environments @@ -114,4 +140,8 @@ \include{sections/02_categories} \include{sections/03_constructions} %% + +\appendix +\emergencystretch=1em +\printbibliography[heading=bibintoc]{} \end{document} \ No newline at end of file diff --git a/tex/sections/01_introduction.tex b/tex/sections/01_introduction.tex index e14a262..77cd775 100644 --- a/tex/sections/01_introduction.tex +++ b/tex/sections/01_introduction.tex @@ -1,4 +1,182 @@ +% chktex-file 46 \section{Introduction} +This is a summary of the course ``Algebra des Programmierens'' taught by Prof.\ Dr.\ Stefan Milius in the winter term 2023/2024 at the FAU~\footnote{Friedrich-Alexander-Universität Erlangen-Nürnberg}. +The course is based on~\cite{poll1999algebra} with~\cite{adamek1990abstract} as a reference for category theory. + +Goal of the course is to develop a mathematical theory for semantics of data types and their accompanying proof principles. The chosen environment is the field of category theory. \subsection{Functions} -\subsection{Data Types} \ No newline at end of file +A function $f : X \rightarrow Y$ is a mapping from the set $X$ (the domain of $f$) to the set $Y$ (the codomain of $f$). +More concretely $f$ is a relation $f \subseteq X \times Y$ which is +\begin{itemize} + \item \emph{left-total}, i.e.\ for all $x \in X$ exists some $y \in Y$ such that $(x,y) \in f$; + \item \emph{right-unique}, i.e.\ any $(x,y),(x,y') \in f$ imply $y = y'$. +\end{itemize} + +Often, one is also interested in the symmetrical properties, a function is called +\begin{itemize} + \item \emph{injective} or \emph{left-unique} if for every $x,x' \in X$ the implication $f(x) = f(x') \rightarrow x = x'$ holds; + \item \emph{surjective} or \emph{right-total} if for every $y \in Y$ there exists an $x \in X$ such that $f(x) = y$; + \item \emph{bijective} if it is injective and surjective. +\end{itemize} + +\begin{example} + \begin{enumerate} + \item The identity function $id_A : A \rightarrow A$, $id_A(x) = x$ + \item The constant function $b! : A \rightarrow B$ for $b \in B$ defined by $b!(x) = b$ + \item The inclusion function $i_A : A \rightarrow B$ for $A \subseteq B$ defined by $i_A(x) = x$ + \item Constants $b : 1 \rightarrow B$, where $1 := {*}$. The function $b$ is in bijection with the set $B$. + \item Composition of function $f : A \rightarrow B, g : B \rightarrow C$ called $g \circ f : A \rightarrow C$ defined by $(g \circ f)(x) = g(f(x))$. + \item The empty function $¡ : \emptyset \rightarrow B$ + \item The singleton function $! : A \rightarrow 1$ + \end{enumerate} +\end{example} + +\subsection{Data Types} + +Programs work with data that should ideally be organized in a useful manner. +A useful representation for data in functional programming is by means of \emph{algebraic data types}. +Some basic data types (written in Haskell notation) are +\begin{minted}{haskell} + data Bool = True | False + data Nat = Zero | Succ Nat +\end{minted} + +These data types are declared by means of constructors, yielding concrete descriptions how inhabitants of these types are created. +\emph{Parametric data types} are additionally parametrized by another data type, e.g.\ +\begin{minted}{haskell} + data Maybe a = Nothing | Just a + data Either a b = Left a | Right b + data List a = Nil | Cons a (List a) +\end{minted} + + +Such data types (parametric or non-parametric) usually come with a principle for defining functions called recursion and in richer type systems (e.g.\ in a dependently typed setting) with a principle for proving facts about recursive functions called induction. +Equivalently, every function defined by recursion can be defined via a \emph{fold}-function which satisfies an identity and fusion law, which replace the induction principle. Let us now consider two examples of data types and illustrate this. + +\subsubsection{Natural Numbers} +The type of natural numbers comes with a fold function $foldn : C \rightarrow (Nat \rightarrow C) \rightarrow Nat \rightarrow C$ for every $C$, defined by +\begin{alignat*}{2} + & foldn\;c\;h\;zero & & = c \\ + & foldn\;c\;h\;(suc\;n) & & = h\;(foldn\;c\;h\;n) +\end{alignat*} + + +\begin{example} Let us now consider some functions defined in terms of $foldn$. + \begin{itemize} + \item $iszero : Nat \rightarrow Bool$ is defined by + \[iszero = foldn\;true\;false!\] + \item $plus : Nat \rightarrow Nat \rightarrow Nat$ is defined by + \[plus = foldn\;id (\lambda f\;n. succ (f\;n)) \] + \end{itemize} +\end{example} + +\begin{proposition} + $foldn$ satisfies the following two rules + \begin{enumerate} + \item \customlabel{law:natident}{\textbf{Identity}}: $foldn\;zero\;succ = id_{Nat}$ + \item \customlabel{law:natfusion}{\textbf{Fusion}}: for all $c : C$, $h, h' : Nat + \rightarrow C$ and $k : C \rightarrow C'$ with $kc = c'$ and $kh = h'k$ follows $k \circ foldn\;c\;h = foldn\;c'\;h'$, or diagrammatically: + % https://q.uiver.app/#q=WzAsNSxbMiwwLCJDIl0sWzQsMCwiQyJdLFsyLDIsIkMnIl0sWzQsMiwiQyciXSxbMCwwLCIxIl0sWzQsMCwiYyJdLFswLDIsImsiXSxbNCwyLCJjJyIsMl0sWzAsMSwiaCIsMl0sWzIsMywiaCciLDJdLFsxLDMsImsiLDFdXQ== + \[ + \begin{tikzcd}[ampersand replacement=\&] + 1 \&\& C \&\& C \\ + \\ + \&\& {C'} \&\& {C'} + \arrow["c", from=1-1, to=1-3] + \arrow["k", from=1-3, to=3-3] + \arrow["{c'}"', from=1-1, to=3-3] + \arrow["h"', from=1-3, to=1-5] + \arrow["{h'}"', from=3-3, to=3-5] + \arrow["k"{description}, from=1-5, to=3-5] + \end{tikzcd} + \] + implies + % https://q.uiver.app/#q=WzAsMyxbMCwwLCJOYXQiXSxbMiwwLCJDIl0sWzIsMiwiQyciXSxbMSwyLCJrIl0sWzAsMSwiZm9sZG5cXDtjXFw7aCJdLFswLDIsImZvbGRuXFw7YydcXDtoJyIsMl1d + \[ + \begin{tikzcd}[ampersand replacement=\&] + Nat \&\& C \\ + \\ + \&\& {C'} + \arrow["k", from=1-3, to=3-3] + \arrow["{foldn\;c\;h}", from=1-1, to=1-3] + \arrow["{foldn\;c'\;h'}"', from=1-1, to=3-3] + \end{tikzcd} + \] + \end{enumerate} +\end{proposition} +\begin{proof} + Both follow by induction over an argument $n : Nat$: + \begin{enumerate} + \item~\ref{law:natident}: + \begin{mycase} + \case{} $n = zero$ + \[foldn\;zero\;succ\;zero = zero = id\;zero\] + \case{} $n = succ\;m$ + \begin{alignat*}{1} + foldn\;zero\;succ\;(succ\;m) & = succ (foldn\;zero\;succ\;m) + \\&= succ\;m \tag{IH} + \\&= id (succ\;m) + \end{alignat*} + \end{mycase} + \item~\ref{law:natfusion}: + \begin{mycase} + \case{} $n = zero$ + \[k(foldn\;c\;h\;zero) = k\;c = c' = foldn\;c'\;h'\;zero\] + \case{} $n = succ\;m$ + \begin{alignat*}{1} + k(foldn\;c\;h\;(succ\;m)) & = k(h(foldn\;c\;h\;m)) + \\&= h'(k(foldn\;c\;h\;m)) + \\&= h'(foldn\;c'\;h'\;m) \tag{IH} + \\&= foldn\;c'\;h'\;(succ\;m) + \end{alignat*} + \end{mycase} + \end{enumerate} +\end{proof} + +\begin{example} + The identity and fusion laws can in turn be used to prove the following induction principle: + + For any predicate $p : Nat \rightarrow Bool$, + \begin{enumerate} + \item $p\;zero = true$ and + \item $p \circ succ = p$ + \end{enumerate} + implies $p = true!$. This follows by % chktex 40 + \begin{alignat*}{1} + & p + \\=\;&p \circ (foldn\;zero\;succ) \tag{\ref{law:natident}} + \\=\;&foldn\;true\;id \tag{\ref{law:natfusion}} + \\=\;&true! \circ (foldn\;zero\;succ) \tag{\ref{law:natfusion}} + \\=\;&true!. \tag{\ref{law:natident}} + \end{alignat*} + + Where the first application of~\ref{law:natfusion} is justified, since the diagram + % https://q.uiver.app/#q=WzAsNSxbMiwwLCJOYXQiXSxbNCwwLCJOYXQiXSxbMiwyLCJCb29sIl0sWzQsMiwiQm9vbCJdLFswLDAsIjEiXSxbNCwwLCJ6ZXJvIl0sWzAsMSwic3VjYyJdLFsxLDMsInAiXSxbMCwyLCJwIl0sWzIsMywiaWQiLDFdLFs0LDIsInRydWUiLDJdXQ== + \[\begin{tikzcd} + 1 && Nat && Nat \\ + \\ + && Bool && Bool + \arrow["zero", from=1-1, to=1-3] + \arrow["succ", from=1-3, to=1-5] + \arrow["p", from=1-5, to=3-5] + \arrow["p", from=1-3, to=3-3] + \arrow["id"{description}, from=3-3, to=3-5] + \arrow["true"', from=1-1, to=3-3] + \end{tikzcd}\] + commutes by the requisite properties of $p$, and the second application of~\ref{law:natfusion} is justified, since the diagram + % https://q.uiver.app/#q=WzAsNSxbMiwwLCJOYXQiXSxbNCwwLCJOYXQiXSxbMiwyLCJCb29sIl0sWzQsMiwiQm9vbCJdLFswLDAsIjEiXSxbNCwwLCJ6ZXJvIl0sWzAsMSwic3VjYyJdLFsxLDMsInRydWUhIl0sWzAsMiwidHJ1ZSEiXSxbMiwzLCJpZCIsMV0sWzQsMiwidHJ1ZSIsMl1d + \[\begin{tikzcd} + 1 && Nat && Nat \\ + \\ + && Bool && Bool + \arrow["zero", from=1-1, to=1-3] + \arrow["succ", from=1-3, to=1-5] + \arrow["{true!}", from=1-5, to=3-5] + \arrow["{true!}", from=1-3, to=3-3] + \arrow["id"{description}, from=3-3, to=3-5] + \arrow["true"', from=1-1, to=3-3] + \end{tikzcd}\] + trivially commutes. +\end{example} +\subsubsection{Lists} \ No newline at end of file diff --git a/tex/sections/02_datatypes.tex b/tex/sections/02_datatypes.tex deleted file mode 100644 index 2241169..0000000 --- a/tex/sections/02_datatypes.tex +++ /dev/null @@ -1 +0,0 @@ -\section{Functions and Data}