From 82558bb67ef0c3babb06e5d0878c26c61d8a4dd8 Mon Sep 17 00:00:00 2001 From: Chris Martens Date: Sun, 3 Jun 2012 14:55:08 -0400 Subject: [PATCH] added abstract to readme. corrected url in paper. --- README.md | 23 ++++++++++++++++++++--- lfinlf.pdf | Bin 251867 -> 251482 bytes 2 files changed, 20 insertions(+), 3 deletions(-) diff --git a/README.md b/README.md index 9846656..5368dbe 100644 --- a/README.md +++ b/README.md @@ -1,4 +1,21 @@ -lfinlf -====== +This repository comprises the public LFinLF development, including +soundness and completeness of translation to canonical forms, family-level +lambdas, and constants. + +The paper draft documenting the proof structure is lfinlf.pdf. + +All code by Chris Martens, 2008 - present. + +Paper abstract: + +We present a mechanized proof of the metatheory of LF, i.e. the decidability of +typechecking and the existence and uniqueness of canonical forms. We use a +syntactic approach in which we define a translation from LF to its canonical +forms presentation (in which only beta-short, eta-long terms are well-formed) +and prove soundness and completeness of the translation, establishing that +definitional equivalence in LF corresponds to syntactic equivalence in +canonical forms. Much recent work is based on the system of canonical +forms and hereditary substitution presented herein; our proof also serves +to reconcile that presentation with the traditional version based on +definitional equivalence. -Mechanized metatheory of LF in Twelf. \ No newline at end of file diff --git a/lfinlf.pdf b/lfinlf.pdf index 4f075fcc8e7cf73aaabc0ff8e3df6273ec8e2f62..a2d3244d7a8698fb0084bbd2a098b8d029446753 100644 GIT binary patch delta 17723 zcmajGWmH_J$}s1PG0VsCVzKMrRz2VuAOlTa867NSq(fM9Ccy_4I^aBv z+b{OyH4rXD6RV6Wg8gdaKa`h~Sc+?5oHST5pKG0T;1E$4K4!W*;}K7!1XE4fcIQNa zjdy=BO<%$uft>g`v10>TE>ZLLvLn)F%HNXe|J@d*oQ2Q8&) z{JpE(J{2G(y2e4mM1v-wLSg0?)I(+Q2~56$m@YBL?_y!f=*yC-(x?a7lyhtm3z@U_ zwHkMI9C7wpZb7~y?x3Kf!ulP~!%El0DTYGS-aO0gK()w%Bq4vUgaa~uL()QWY1BYE z0Y_M6%D(IMG|ar!)c(8|!LbqGqF#KNtmJH{UV1jqh|p= zh4fkd1GtkSeAU2DRBykFm1j!D;&n>MiJIA3O$v0U#}9`H4|lcTJT2hiul;~a%m zDA)sX(deLXOP>`j&s2n;0|7KcNKo==(qUz-cmCelGRqdE0irpu^>}qpa}y#|zrYlK z6a{&3|9nOJDJrOaFA(;*EXKQA7r$0h$ZN0UpAO@{S(M@xrb_V3ZQjuIZ@ zW$NZe>t+EJSAV~w-;Yuqj1TPvn+DCgR4|D^E|d0>Kg&n|ye&AWG_xa%c07yu54^4- zG`{B4g~*zlbj-Vj3yyEMGw?mdIK^y;eIcL1=C818;+$xtmC-KO}iFNaTtK67C%5OnRNEfRI z(iii5ZAo(^QWpKI-x-!X!A5=_-0^2Z8M4wW+EJ0=Y-S$7%oT>^jtv z;WojKW{Ygl^B9*u7FrIcA^w|oz?{@JnUGE|(z(u~T+cIYr7|K~9 zEE7@)Rl*+AM+PghD-%%(c|~Vlv=Pz2E|@DdOemzZPT?022|0-`6^>-z@B#G3a_j|o z`lJ1&5n|Uq*_vN-qu6|6!@QXAN$ra7X>~iq^m%)H#&|~Tn|{n;S9_rnveID4g!LKb zd+L_#p%B?Chli77Z|=2gf<9EdHzouUO60=VhuSBP>LV2-k>?W(&DI!#9Z~YuX?+#U z5FT2;-@RQ9b8-L^sNVcw zOWULRVuG@R!?ESBZM8FZimh<9Vj zZ!V!5m*pZ-U6aG{m+dwN0 zEff1d%K&`oa+t637r_)BQcXx*+*UTip(Ut;pyNQ)wQd!(cc|Psv)+I0s0_of7D#+o zJcWynxzGCt0Y}0cADo>c5a+aNETm^xS-@A~CNphWAc7LQn9#&PXq^rdo1|54W-Ebm zA)ZaZ-)&QWvoPzlLes#}_Y;$>23Ny^8QaK<>mD#Ej;a3Mj$c%KGeg-5r+icHk8k2` zY`U1n-6g^KL#pRCFS|qR+pe&t2#y#2!yPY0eD=T)r@?G}(>jIvPUH$H9{01$oI|QB zU|tmW?KpW*qnnn;8=bp`ZK&w&rXwN``?L;W7Vh;IwA?UchE0Nj{(ctft;WhVf&BOrD>fD)A>{~ zMwy@A+s0pfYDVUUzeSN5oZq(-{kbX!bjpg#U~SbQh@oH~nMm!P&JqKGj;pFIDGy$}yFxuBI| z&#z^VQ~QGPCNy2e0lXHV-W`jjYdFKmZODmWw8oAsm1q&wN5V&fN%}#TGJaoO@P8@Jb_k!Z|sA1C12C zpuFs5RluIXpl(rvo*@3Hm+*EApc&OpLTlDq7_~B>=RPjQwUEl*d5hx_!)02SbQnM)N_Q7bcQz& z0zLSo+YhsuBHSlNYuE^5Z~Y7DzYKTXYE533g&8#ZkCvm1zabmT^hi3O1C&o=GT2(D zt6Vyi3q>h$*p~*An9A&z3K(yT#l%WUHj011pvYivtuhhlgf(`8WXU9CzBl-FfsvsJ zOFLIb=Qc0oB`kt=_%U!yeyXL0hE?5&CJGY`n`_G?!xYe<^hRczKKu#zy)WF|>O7_# z`>s>numEtUZboJgpH=$#9YFqVT~oll3UQ(+4oZAWITPNGELc8_M@vwXxbsWZ>w4ob z4h&ck^O!E3r^aR`n`IEfapI1}s?Z+smA!W@A-o*Gq9<2a@~<~+Ye?hld&`}$vKfdG z9d_dr$Z{&+TKUf1WZ&nh2W||@yXP32&IIzu9RSS_ucJ^XJ**`)B-nbWbQ*n9MW0aKPCJK_tl78Fn2Eb@&b}7! z%Y!KrZGGd9Dt~%`I`q}WesjwFs2-t4g6Gbu)JD&8)rP}4SUUt^tHqHyYFwezX;Uxw zZFJKRNcQq^vs_`WGzxFgOWl7Jkqe6du}UF&%Z(_8o4rHSAAl96T&cNQ*_YD>_8Pb^ za(fuUZRS<*azgloIL(d#Kj&Rh&-608#^ZVRIso_n8 z{w<`9NGGIpdbb1rC@gG#7*PB3_D92nuaVQXU1%(*RlBN66;{6l- z%fKZ3%oI0Fbv!-y->I+B_%c^0`4joH`dB+X&6OF|>ZeX`nhnRNMRwgi-8f>bW1Drd zn>a=#%90|W^$L*tekP%Zw-%(YVvn*Xq=C3{ZUna?6oD~YqbIsf>`OZgnTPAOQ+;3V znnoy^98Y7H+uVgVw$xtZ9=GT&juk0rlm7I6H~q!w>nQFz3+_wfzo+cRPsuvp#9eZk zXwm~wp00QowhuePlQhFU;Dz`R=5Q>|Xt<$y2HA+c?nbhHh-WhtyMcw2L8|9=goG;* ziGH4VXn-&(^MzJ%z5T=G+Py%sv}ErMcRuu*T;olrOdFyodK5=n!q3#)4f%kZlhuJR z7(=2%`&?~*SuD8??wix4LhJW9|<3p6TDBmpCPUZbN8yLtL$kI;9qhz#sPtMpsS zAjYBSEg2+pc6L>C%gt!C znM+fU>U|u%zNi(bV?xP)7_{pc-58vRG|ly zlIp);?>KYXBK*sm6M5<}`s6wSx5#<&K<#IDR$8t5D=k|VFJO0rqA&LdUH?zyc9dmZ ztFKst9DP}ndAz&5YAsq}_*zRjkpZ6D*b3(m;xIPudVwI=m*M+gSp&+12b6}eWeO2c zX^H*=liiI`<>`8c-N{^F>cnx(^`fKlg|Tbf8j+$*>=`u)=~*s2NLH=zB%Kl!fwh%o zh7|WcGlsJF7_9W>$^3w;f-HJt1rq-2GXjp3681bdsAPgOVdCd_+4@Y+yP0QHd}!P$ ze?#_QLw4voLv|QNBOG2{FbezoPqyaH7F<-E92{WIgfR|iJa|q{E*?;*t{mVO<{LT(9=6&2#zK+X>1b)&?*z!HHsKuMb)c!C zK$%VCeaPx#C_6}hzG#0DI}(1D>R`0mK00C<>R8>}?8b0*Gzo5;59O|aX>JFOT%kTk zllD#FnxfxGaEOxcz}=}53m}k-&R`r|W zk<+R91#u&tnV0WnKo|S9dBUz3Z{MXHl^uwDYmZ*;7iDHHh~>swgAJO6v1yN_@(XHy z+tgGizzl^{@$?33X9pp06IKZLVknbI$Fg$W{{_l}i4_Wq{)FAbR=w2F+zsLiDPO0= z;d{#b;-ZCN%nIw`2qU(*#PP(N!7__)3UA$n*_#2`hx+0v_V5G)HvCpIOi5ELl*)HO zWk`q_9dlqn&4Jq^0@jHZ@QaF#RgDftg>r=UYc4t9eaf7*a&)9C|J7}T3pnUSJt0wO-)Gkc$nTXk7)}3@Md)}c9S*p4O4meU({qL(y;kN~ zQo|wS6d^XKZOV+c=cL~~gCr;p7q<)#*N=`n`-Ow=T8wX1PnU%)Eejy+Q4y5wJ;R-_ zE9;vGC#c9UFi$BPcDKOu_osy-WVmM+o)O^Y2NhV^?@tDbVaa_I%4l2A*VD2GHfjRps{8U;@TpDp={fHSGyZvD<@xx_h7cJ!&_oQ}Ka1FA;?9n3 zmqE=^dDVBui=(6Hp!Yook@!97nu4N1vz@y@i`w;sCvJ8m>ua z?vWzlSr;aJ2^$UCQhcc$Xy$rKMauCsjq`~ zAvhbs=+n!xfGkuy^aH7bLuaZegqh=@I&wM_$by3=i+`pf%9vXIhPhSsmH&6w<1oxb zpV1?GAN&f`BdQ}Tugz1?1BdB-?>$OW#Ph8CEfkrn@Q7jh*D;mMyZ zRz-YgiPN6G=$88d-yJ$a`JYuWww!~6lCfl>Bkn~2_0qOt0OJ}M5-bnm^Vc0FvkJdrj`5MnzA|DPduR?W=d}NUE2kg&szWwvnQcCIG&@;5iK=?Bs?pz@_8d z084#x-yi{5b>*D&X@*zJqyG2DhUdR-v&D~y&%R?~RCdw$J=;v6HhGLehI1-wZu3LEp8^JkF`@AlpWL`P>NfwUWa=PW^YK%0hQO`!-?`2XbS3 zt=9mD(s=sZevf84y{CxUokEdE0L&wNO6f-Hb9Pvp?>AUu2JZ|my`N#hRFP(!t0gn# zU)|1Sr}j4XyM;;~J$>BLph$tr;mI+{~5T*^04&@hJ=uL(0c$ZEa;4XtlWCVO>qfC z-bYQyCP%1?=X(|xmbHR{9ED}nKkqdOTacNLMU#{h98L~Zx$yC!}67fY!`;yAMQ`XVR7vNAZ3+ghcBg&`?AECW^bb86Z{D=#C8nQn;-E3GhC zJ%LN|?&waFqE-=F9p8#i?7b(HS$-w(@MSK?SfAhn<7ZBoIDPrVRJ9^9r$c|fEEwtW zsdI;q)>p~4EirsQ3m5j|Dif0O?!QjX67xfowTIU&A#Ba;dAuSws(~;Ro-Atnhk1j8bq1|6|0Qu;z z@iPk=)6#Uol*faKh|UC^^Y9u>Id0Z=ESEps;f^#KBy6FR7I4qjM<*p}*HJ}L@n0QE zs|n5?n=DA}_(;xu8}$v+o5M8Q$a&BevEy4CMHf}MexeUyr6|3%jRQ&^+imA3hd)(S9rvZm>?uj(>f7)qS67oHF<;TQp{Ca6 zI#Y?Qp$&kUIprXaAIHQg2Rltj@BPi6`vybq5eh~AYVm_LEV+n?8MJvhfR0>g3iEvq zo_Pu9rEs{T_wN*KLOrBCl3S+x_AiU4m~fPkp0cQJPk;4Dxv~j*;WO3oejll4NH(3iuvx1O((}{_)9Iyjitx5#i%xko3AE)Xd$bikfmD8%X^g1jguR?IozWt)7 zyuVaN&RG>K`V+W>fyqc?UG-b!2FZJYRoW*ZI)Au4f5D$*iJUWnQTAYdeEYyg{{&gWGEGItZ*ymuUR@{#w` zV-YS51(MJpF1I~fl<}N{?t3CX7O4-XvjpnRc<$_irTF4pRC7hdyo0U>)O<6H_j=0# ziwgN%S{wa3aBto>l$xP5MRxE}!#hBETvtt7<>*Q{jnS zc}b3b_P?#LDivDFR!}%%kUYi=?&W9XD`2iD?cKL-!5`(#knB1mmm+Zu{)#$f_M_`3 zR8prp37T{MHR&+&Qi7VCrP=TGQP9J^;OubgP{BH-yKeNRrH6A=b=U`X6q0@n2+Y|C zR>beHV^^2F!!;UbHY4^a&M&s3BPsDRmRtet9$IXfun$b`ajy0)g_bXmo|(thYryM$ z$B7JOJ+4d~;l_Z&<=L~53rj*YK)qwLv%wpmxN*{*7T>0uH-2Y# zCj$%|cj7mPerblwuNZ*AAOEQ{m(|TT;XgHMO47@7oxkcNfdC`u-G*_uy)=ul+Sycz z{b?OF79a4voDFPaq-j~?qKJ94qJhBzHEUO$(4?%t&kUzft>jLVuuz6v&i#bHaVoQ| z6M1m-ZBCjMCs+9dbq2Pi&r|6$a!|i zQMHcQb#UtQ)5Nv*dWeK>@Woqa?tFC0fOwSNdNRO1TDo2HW41VbqH!wUj@lB4YAWlJ zPrB*z-MKw%p7_Yaey?r$RyH3;BZD z65>m2*K*{L7e!>ok!4M3wfIjc4^H+v@~?sEY$#c<7k^D{d$4AfD}9~$Z|*|mf~@`k zBfmXLH))crdd97syyWc%RXzSKrfA1^6oIz|zTp>ropp_Ay-PSniD^FQBrS`5$+Q~Z zGSj0+LOUG5^3(wgcs_mJWvn_o1`l8VHtbRu33;VNst}3rd48E{(%2i_DCH!)c zNXnLG%Wxj{V14e*?xEmH+9?wPwbe*58XZo;lxgbuOwSVAQc`0}SJW^-$7FL@J}c2r z^^6kdJ1iim&lJhne7+(L_CHkeu=HSBEM7ZSY_&$ zGcR*(t^c65ZczX_^XYPWR8t_gjLRj{S&{VbN{EoTr+}C}J2j2TtcQo^;N8uoaSF`klRhIbl_32r){S3=Wfj6C?lqd+-&JKHdq_7=udueTrgRP>DeIbfk^t(FJU zI!DuV;u1Pk&ZU6_Ez=Qh)zX3My2Z>KT#+|EzGKN_igNMmC)BUHugoV!Tu=BBZ)%O4 zkM-45kt=%X)9U0lbfZl>-Tbps^0dB65ZVXvm`jwlF`rfwa5o6B zQhi2FpNg_t8}j_ByU8GTH08(k+8tYHk(#UZZ5bn9vZ__=&gqTiLKsW5{fQ}#kS1-UdqdOgX7M=hxu2*>ZwVP-lRE!LMiY zWQk;km38db?=I4X0xB)63i$g!y|m0aP3T{m-JPy(YzDAxKRBjyxq}$ij6VbAHGu?$ zSx*P+gAkJqf6*Y8%&LQ4@FuE%8(s5^OAKS$c#OkqiQ!&{1Jl z0BxZBV`!Phhpls1!A>hoH-lPO#9Mnf3`5{siY&oGM&tKE?=Vmi#s2nHCXBKydhA&h?h^Qh{ zeiSPs_kxsZF-vM=hBleVR8YYr_MWxA94OUe>SUuz5~;^y62h0q{vf~kr(bS5l8@m_ zQVyB>al__ZN}+81$)*Rq8?nw}L9TNuSBeyv zjtQE)yN(HC`f+4J6WW3DKc(4goPfk)TtS5r?|UT4kzA)jHm7DO>zX!i`C$AAf!l-7 zc&qYMwK`e!Kmjv3X_H5>Hl&YK@viq`h+>8d*|fC7g4ATaqXL8ip98NnZ*s@@>JzL5 zD+f3UClI{~hKCIHh1&|mT;2{8MWs7yW5*0t2L%bMar#2`>=0>)X|#HeFoBydvDwZG zxnP$N^#|%lKGn6*ulI+|Rvsb|a~^ z5>*;Wu-wLRp6Ea%ogw9Eguo0n+wqm@`e)wWw8a2g#-Q`6;VRs#G^$Vnfe$ZkxKXT{ z)5{?Wv#w!k-#G5xwKp(PI{Zu(>pA#Kt3rb7mM^Ux=h`)Lw#I+;k)qydbgCwI7+)cQ z(6M?i*=#H0jd;m%t0&l1w=K70iq$Wc6G8CuR^wvjhu3hB{Vgh%E?_1*G5lzCZ-pzT zCT^olDr2(LHXM}~SOj;_kTmQS!A;ZK$~ylm7ICD7w2w-+&zMHn&~mspH7A8a%<~iV z*Ys#?)m|C$LKwBF-4SJj%=fLe6V(fGLOPZciUTx8`{-r+v=e+HivX_gAJ#7vj{2>2 z%0+M7qa^Vq^x``Bg#oDmV*NwDT*Zg1exg(IcH?kq68!oM!M-|K&<$7mTjdTd_V0D@0+a3=^Q);|`rntzrY=Kodj90g8Qq?~g19P_p?_lxFf z7luwFHV*r={cBBvF6}Ai?usY+dDNV@LgMg3iZXu7Te=I)@DC!0Xm}!Ex{&(RXG!Ld!bEPK;={35}99AdW^cdB9zp@X{|W^mckkYvJTVKbc2saD0{R?8zFNQ@^6HFadj zP+;S#2rH0{%LdecyB`$aiHg|&YFcJ7mHN8sLhBX_BDUVQRT^PK91B4npj^A!u~n z_8dnrDQvRNk}qC1c3N+qyZzx0`=qtnEyhi^W^7`whzn#G1*z9{z6-NMMSs@Eb$ID+RQ6FP0*99@k=L3; zFnTjEwMo?1;a0^ZmMUkgw^Cg>t*Sm=tlkaDY1hNHU+5p*dMw*u&K}Q|7w*?AtGaR4 z#$+y5$AQ}oe7YkSp$$8KZt<^Y zpFz{CJS3=t;F2wN0oC%o_l|0b?7UneYs+;jQ!bgGTB;OmaJU)?HZK;o5xZqJ%LliIf!z!nWzOW2GK)%ZB_Q~H_1_8r)^a(rU$f%E)xQmfC9c^aSUGoKZ z$S0U(y4%rLP>MbFcsW(SPfClzoyZBXS4BHJ77wWDdZ(?FhYlA_%4hB=vWO*-v-w@} zm5Ez2XIMoNDkx(JaK|Od{O?PmC5O8HsxLLK`;jJ~dfa|y{vD{^>+yvwO}CEnGMvb- zy8}4NqM^ISj&;ls5rV#!`Fz_o7Tqnws%2bQSY(M3Bqhryf>R{jo&Ea&;}D#D(7Pf3 z)}-VJRt%!zqV@D%XVvqvI@AxYBOpqMf(e>Vl&5-0gFI-tIK3cjyrN)aDe&m-L_^SX z$ATxgQII1m^*em7+q)m6NG6x1Yu80-mGXdx<0$n9E!2zPV&%?H`t6@!2V*|I+u7^w zESz&|PSKHIW{OUowwhpDBtD7?P#ExeT5j4)w?ph6t;>(0V*&irBtN#x_~jMTWbOv6{=YZ3~)R zpE|OK3$Cp>uMI62f#)F^Gak~MMo?rAPDoW%Oz_}nH-;{MG1jjt*7g33>)KcVd%|+S z(SPS;)TN8&d!6N!w}CnfjeG20(hisI=&+#yG``P47d7U@M?Qw0Z&Y)y%%Tw@uOHKt zm@!igw>dM6Npsv*L+aCQKJq%s5%YX^3&&C z6djyPe%j6{z8<^5*@pSlU9PANAOP-6;XZ$AZN~VmX)@yFf|Ac{u$2SWQ0SRTz&YK` zzG^_7$AJ27kp!{gh41?aneYqR5u7uBX295)CS9gouVov(yyH=i=ot zBOCdisy+poujtGa#PPzH5?9t&)GyrMmo3a(SK-2*3=AyhQWVq2D$P{k0c+^hqH_W^ z)r;N>d10CP?9MD_wT=ezYe-%h2^?<{Rf;wc=pKsPXR^&aM=dR^XzA1z58FcYfWYZ< zR@SGceR=G+Lj(43&>RiC+FyU#!)F|%eRx(Fl=M8q(hHqZJ=3dgg$v3wgkHC>79Yyx zHX3TEP4uJmrPGfx-AF@;2V~N0(>4z^j*gXd7x3|n)`s~Q<7Or zc^EyanvnRKKn7E*8h@$4gk+$t^0=f;ap=YvBDUDuD3%Pr$H1ts3?;&s@C#Z50zyTs z-ubC(=b*29_~c}l2PBL7qybN>koZvedcL+A%fyoW{GWrpJScInY^R~xGS$(YS0KxDN}C!NUk}^np)#E(=cb&xo!_<$g_YkP>D=wW zE232eOgc7|jvXsy^MdNpeyT>NR&@eWO!7t-5p_&xd%hY2#}S$ks@TpJxe_rw@RE#@ zxmAK4Q)J4)yF;N(`lU!~O~!YtD%MYqCfl2{rk^+*?6iyX{KI|r`K2TOuCjM-kx7hK zq`#{)3ecfet%d`%Wqbq3omQxsEjwj>sjY+s^N-ILG0b4Mzl$Lp<2d%q^bn)ux3sJO zWb>E3*^(-;e@2F5J7 zCHF(?MHqfMs%F;LrTNrOwvfi<%$sktn~@%Nby(bT8MCm!{CO|>j2b<+9%Vg@Roe8t zngsKLXfu65u2)*ro5!0|NhLl{#4DnfvCxLxsMKIaDQ`*t3IzTd^mQXyLC>U{xUcHL zhUSF$2iMhJL4SXa&GqS8v5N`}ZNHgjAe<85LCKrgw)d8t{?MCzS;1w%A|Gk+MW=sl zxWZ$$>*v^Cz{89-pPCgv5+nX(_Hya~T?3!OA=kv}FWD#C+GYPkD}K2Z0${Fx`m`Js za&<;)_^rAk(YBfbP%&kPKAL&hx&IPw$5|nsc0}9w^@4|{l4*`%Q9h_C-7^pbFRrIZ zRQW7weu@^7jFe@#*=zsE_x0HY>jJ@nV7nAzWsX({WGC_PN5SV;6xwFPnKC~VvQ4T?~#ku z=MpG3TTpbq3$jWY3U(vV{z@QaH|dIql|gC655hF5byA^t*K&ed7ZuNb2Ue}B8P~^4 z3!X5vH6MsHBEU~UG0k0ybhZySBPO!kol^Hq0}{Dnw+w#;-zRk{Y9s z+x!r#Ic*c85H(r#XP09+SS@Ne=QD$2(IrA*Pv)*Po!Vu1Ia`A(_Y9TZ?=ESI?Hgg2 zFCoaFZ%VrN{4mNh`mAt%2C4YZlY8Fd?;?btr_F)}LsSU-x1-PXoHmgnBFvJ_hj0E= z9sRpm`*c7IJIC?kKrbstx0PSoGL4j; zs^&NiQBD;}QUNW2ojfmLC%01;4yaVl9=N~lB3rh?+Q%-s!ss6HMx;FLj#+c~wyFd@ zy{hEQ&Xvm`AG9DV^rsmNvO@x?nU0iJTP^EoEQCR4SLU+fFT3-ul*Cj;UR{65ok)k^ z2BuILV4a3Xai=nLm^;yJQ7_rV<0bT%0;|BnNWHT`aE&cXlGfS2oL1C5mH*EzU_6=W zu%tf_D{z=qW6A%)T;@F#d*i_q)8C`ZH#DQ?57<@?pR*{|)WKHOW{201fzLsfZMvl< zbTK0?BB-GYiaFukjA{`$2F828PF+0KKePCXJ>spr`@9c<*tm8{2b9P(SZHWUMUGRZ zCI+tQ=8dgGJ@|?7jBIX&epQ+H25blD;yx8(L09d~FKiGaj@N(f*t^>J8_?w|f6?)K zX4czlkB0xk7Bz4udy>$OQX(CHU1aNhOp9EnR5p0p7H^JXl|7yG^f|sT)zK$v;miDLzStJ<$Us6(7=a9imOa^*ODEZQ9+IaCmx-`a!xs15j1@U~xTk zS`2Ue&OVv3<34Ok;V|J+_ve*4M2p4POnfE8ZGGbcj$7-LlY{fH6S)V9Hp6 zVk!HfuM2HmaC_wj=YT2NjAYcz@L8+YW9usDC}O7j)U;AwkiUg^ofmi^TnDuTh zoeiGP^2?P}pIYpM?3JTOhr+v?b#&+s;SMFne(i5n;(;4!DXuY8n9GEJ0!kqYQcM|~ z*hslyAF5+%s}^&h{DGL&Eaba>o_hM8DaDU<-GW_4n7_O~bPW)yuB0L9$Vo2xP5(w{ zC@NGXV-3#P+k&LlJO}jzHH&tJP|DkFZ z_2(>Nrk39%ceg7aik@ZC`P(0D9%WKRIf5f20nZkdXM7Bn(NX}-7K&rgk;BFNk?RcB z4YWOs*2VbQ)BE^KloMUorSMkg2Mfk^59_tarIQhECA+`4k{$78)W6fe8oVVhqrZjl zrz$TypH&4HePZexchr#QD7s|XCuGGBEu&wlPm5ct`8bm+&v{@mNJ!FZCoH==a^5Mr zU(TK007Ni{CykZeLOMO?6f5YTQ5#j7Z za6VGyPa+n0yl3a@)*AN`=s2CX55L4=1SgDaiwdd~Q=AHcg!+f&wZ!YJV*ewGu))jf zmL36DTDLyUa{1KvAKtvX=uJZ!@9nSF4H9!Z59h!u57-yMkG|F7>+O zej_Wk)UWdJW3{USOv&{5@S>!*TAh}ghq%(Y_~-#$Zx+WdFb>Phv-^O_Q%XJBcfz`3Ln@Or#1G22ujM$ zUaYh9zd}K$iUBG6^Nee{nqGryS>~%#g$3+8-A)wq>n4;&`}$~m*%<;pA z(M&ynzfiL3*td3Z-6+emgUwa~?b^)CuKU}`2*r;V0PM*7Jo1vKruz}f4@mM}3;nGY za1pqFeRm3YIG-}RCY|Gz86C7-@_ndO+M+)8pm8xv_QR>>aKSTa$+EMARi}Nc>g>NU zt={D~OWyFuKZefy4t6pb;(o+7c@lWo&X1xOeiM3dC+=lZ7zG+_g|+*!%3tr=w*h>M zmb{tq0(^EmCq_mt3sM~Uvr<}og%D-3@2PlA-;p9l_?~%88tT+`F=MFOAJPTRCMgTM zMq6iG_2zIPbaOW2pUwy1h%KARB*PiobQd;A#ajr6SD|T|n8>cu6MTVzi>E}nW07%= zp6VYGhK?CmwhyM+tjFR&4VlF|eS4@XvrN%!4O9a)2VRILs%~6v8~VE9-R1;i zav^)B`PDgtgre=W3ZE%xv3%aV`Or64e#ZecT=C-#YSigv5af#D@HGniMG%daY)pi9 zC_~#H!VKx%w=8BrqlqL@xxBw-SXWtL8at(b)XZ2Rz@j~`@ z0VZ5kiqFc?kvt2-4zivj`tud**sVK+yEex|m5A)n-z6(S4Kp2KL<-}sHzH=vmj%WL zn5h}+rbKb&6}xUrOJh2Dw(q&qS+@-@cMVCY>;C%SYA)m!wJGv%?7}@gddQCk<_(?MlE#GzPXP5m|vz;q` zZ~yRXj2++8MhqD{$K3ASvd?Uv8H*~Pi}jV~2L&yS^z#(q=z6tCdyJMp?qcP?*g&1Q z{e^a^`FSQbzOH!We)v{ws)gE{28TJ$cy6<1fcw%PGJDdY%~Q3@ni8?p9AV#@QowAW zC6!=!zU;3LY88TKgh3L7Abg$xGNzb1xZxhShdqqic*%7r*+xR}iRE+Zu6@|MQpyTC z)&lGd!o%ePlo0A6(h;#gB@LfJLmLfI`VZps)g<>H>ebyd{`eHiHcu1#*i!D7Yu2!t z+bI7)ksd(eOiFZdoh$f3dE_Jyl?Q~p{jM%DUG+Xeim8oAe!HuPP=Zt%g;n0FNHqsY za;k&*?h!Pu5R2~x(K z0#Mq~OUwz>3oy6|o~Vy2Elc0Fm-ipur|p5`KLOje%Lqg zupll_g3<^q)qi|(9D%(6AbdPLR2=_$sBEcF{`JYl!^_1BevLu6c|or+FdvxjHO9-y z$^8$E2lS5~5HR>(>x}-bF_?$*9}B@?KF)t^24XDmt6m&78uO+ z&vjtl|G2yVTWT-_#Pe#HmtQ(S{_EI*{|XllFocim)qUmw^K$>Q$xDw{8*;oP!9UCe z=7WG=6M?+A=HHF^qW_C8L9eBOygdIXeo_B*V_pd7KV*H01*8R^{D;FPx^A)?7Yr_3HXkHSI_q7*Zuzw`n zzc3JY0{;xGnBmJCL`+PalS>jT%_+vs1Cf@L;^2~exijKok{mDg6{ZsW|6QU-B`l2M ckZ z-1n={;Uxi%xe686LwnY|A!kER+LaDQ$M@Dbc@Ls$MDUwijl~K&*Yo zTT?3_U?u^ii2zk78GTqB5wEDW)Wr&6t}>(Pjenvl+Hp7wLnO9DIucZ6nrMe6(KbkA z`?fI@desXyrU_6lPiA0*Rt){%2g{UNfJdwZW$&PzcSZ-!P=R$fnHlQ4RzN7E<{+Dk zx77!bt^Jh!tct$M979h`?{FZfQezp4LuedvXnEewk?ax*Jc+N6!dMV>7Bt>YWd4TK zth@Aa-Y!V-!P!NCC7)j2(6sWX+hzDw_S5M|9G*9F4R4vNKUUG6$Kp|9V%ewiu3l)v zJy*DRpONOCNdh)TQZ5lX-*L_Uk6%o0+j{^MdMBgo)D`iU9D-U-8khr)ojhOV>~GRr zi?E>&8G-rq1_?=J`GwXa#p!_B!Mi?~s;>`g@k|!060;iPq1Xl4R|Y?ywou-l#H|Bu zc*RBVI&hZ_-UtwgAn9@)-bur~;LyP^SvXNx5km%2TA@k?R2N za9i&7X;01HqTheBN1dkjt$V`MC>$1kQ?6BMEW@UB;37as2C zI({v6IqykBQSs}C{lMMkmjA;8&_EC5II;eHchsTp<)5QJ<1}D~@+-4U_63=&$sILT z8d*e#TU{ku}Mk#f=eD%2dy{0(EU0dRp&}%&yaGA*8ON0#? z6uRq_A0gt|Dx92ojm-I0S>zj~^fLcu)=t11NbxORvm;6i#i#{!jrOX)-@{TEkbFsH zRCw^BxK(Y(g+IhdMis}{0?1*auAay7v31fRCF6~EI4ytgW%tL7cdYM4@Nw;4|G1#j z<((6O8o-*QQkb3VRkrDy?=>Ci=);Nt) z8Uo^ZyPqhOL3j*S;tekJ``vx+&And~9kk9P%Vrb+EW9Qb7kTD&epqVu8iTRbAgq%> zaVE#_OSYE{Rr{S{4u;tuN%$>jDkjx(yYIf-0Ryg7<`i8FDw>y-LILlxFAU)s`qBCZ z8$C=zf{kdy!ox1U!@-mNc=mbye4=`ByyL17NzXpuWw>(|>7kLs=Vzlh`eEtoK-KbV zTd`VhyCt(ecHG4U=jd#+LTO1n67giKhK+8r+$ubKJTr58yf!TjO-(?`!o7>m(y&65 zAW(EUkCYRyYdg+!HUF45)gJs~T6W!vvJ6$~`Pq7Vi?}sPZm}HPqd3*<{N6@8%kM*= zZ#}3@g~2IR;;kWE;Lg@dM7aT+uFZ%-Ut>6gXIao z=XIjP8`lgF!8Fg?KA)ss6jV0Zya$j`J&M1x^qVem5T75Ca#3Ot&YyFS-P0XZJU&6w ztlc8yaZ{^B?7)GxUDX>-@)hi-)Oqgx3363>-9*-q3M3ib4-8uz>^X{)zDsJ0UDcQ2BV1W|=Kr?snVFcb$Oz0B+i6aT z!B-45owVa|lD^eC;Sy#Gi}LgxMsQXKYtSj?hH~{jei+G#cyq_e8r&K@i%eEde>x%) zF7FWi=$nf1e2_~))#&UwR(4J6J0(X@M>2sJypCuJ<}~!VO?qp!f+FnqqTI(P)pG>8L109Ee*>E9ce|{rL$(OLiI; z4PoLTau%r{&KC#YJLe*4VGizB`YzlV26;kyb-tP!8 zbrF+xEbzeuvS+eufJp7IL5ZXRyPY@A?d$P&(%B|^ncoe91c#X(wFmG{rFFM3tn$`M zmsN#+GPqaz-ri)GL5GW8O3+dvx)hFwp}?nGF~H6Bd*6KSnJo&&z@*|AX3{EI(aykQ z+Xn|{p4Vx#RI=ts|6UCMLl9J61h ze`4buk?0}VbR*H;DVqUb{4TVZj$|Ij(&0Pm!dPE)&*}t;aKL0;rhOV(MB!N1k8r+z@Z&UUo_7U2?*{n~hf!Vxv9MF) z&Uf4L{G>0t%XBQZ6*>=ZYjsBJ+H_kOdxuA&!&hZHTusgj()4C+HI`I*IIwuI^e)DV zE_=jj5v4S;c$(m&uFbz{RH-MCTT4-zc68vV%rDL1HZd?pMGt*79IWbmhpcth+Xod? zSIb=bt(~6A!8rx!#0-K6>TrD($vbd(x8F=f$I~jNf&S9)e*akj{hX%DAi5xibW*F8zeLekHu-*L}|-+=7j(|1CK%)8ZealeW7? zuomb>>^^3Nd>|?-{C>>J;705gIm*?$?W8P*tdE8buyOqEjC9R{A6W!AaBp|uM%`bf z70xETOtP%!U z^h-vSi-v(EK^s()(O#obhJz{4V4`pwZpyoCP3NJ-85f)aECK<;wwgoVl9W`Sr4hoW z7iJd7Gq}*y$eA$e3*4#1-PoAoAm{DR;z2=EpY9_Od=h}La1D8EL*8Sg(kJf?Mpf6t zg6JvQFjq~q@@6q%98eXp7_V1%MPK)T2E&Me$j=o{GP$=9Dkx#aoU{Bhu0)9Qbc?@H0;NZ;XkLuSsO*P+ra9ZEnoInd^QD? zyySNvCY&yr`voGdPj8y8E%k@1v>rEtyOPY^+XcNRi3PbY_&^_9O9tG1pDb+Jvu*JR zB-<;SK7~o#M~)2jLwC#!m{PTJQNy}kof!MZkm`ayxhr6Wd$fd$vbUbY@65>btQ{KK zWpeK#!-NenM4H9KJ_mDm%4g3ig}(zv38oXB;0TrjgD-lY8tO31J#iE~&6oK!{c)bU z&}QeJ?N3waQtfsQMrEp8(&@a{bMLKF(IdR9hZCE9nNA|;2@jJUbA8)AuRc{sgv*jYa6 z%eo38rcUFBc!JB)9prgscAHRSlBhJfXNcT#KZQu0?xKsMf zq0&Fvy*OWUYy$5;M=(9k{8Dj8&z=$j|U#(3Y&DcmmtQ>4yNswWXSg;@vn2j@OYZ;0Lh^U2C!8#&f zmT{q&W+f%#aioZyUK8kq_&AF8(S?q5tsvjWk&B#ajSdAvX&M2_-L&O?$s_Cf&2p{9 zq&&rK-Fy8Z8K1+cG5?!^ngJ{x)_C8@7zJFk>dYKA?8U`}!}Z0*7AyO)=%(CeM=$s2 zlL40t0y6y_3$!K|D?(&6Fyy<5z{iP)m3^`Wv$+RCG6y0TX)A zm!Av_!D;QohK%SuV3-)#^w21Ba*e%)v@=|bNSTO&4*`NT zskv82*oEU?f%>raC<{XfO{GovlC?`hjg zhd`VCh59i%jt_YYK)r$yNf%Z_@ZU)Ahd`Xxfn%WG&D*aryF zTyh_uxA#|E!0VgB8`B(&$Zz_H{VZ201#LXx8+o{p`PbmUeSPW6n@WE}=oc3_Cp@FL zE}z0T#&)_W(kRaDu=_W+SD@wP?b|Df;%}Ri3S8kqHHKEt?x3?mZaWtB&4rH{j z6G({_2J0;lP}ttonSA-7TLrvf_5Pl3u2 zAjl`=493@w)9@@>NRI#lmj!j=?Er1Tobj&(`5^8)p4(86SCwHM^-*0jc zK{LaNUU$81yQny4(I)od>By_oX37WrJoLe1*rm9}1WIfp={C0}k$&jV<6>cba`s2E z+#XH>A7lA0!}NG!plLQ~6W=njF5&c7Pt(sW0-3X(C8VgOj1jeF8DgjCaD-AS&4+i9 zybJn3$FWE@Zi|gEI5}&ug>2wo3!N^=o;oZz+)xu?&|@b{J<-3BLBkDDv*ErNMC@>{-9YH@BXHW8BqunEg- zELVEqhK|^-auL*5m+e-=b{(-v+Mdx1`NWSi#%y3qXW2$YJ4) zfV0fVqwdL;)@bH+rEwJDZ%ZwLT%O z?J&PERSZD8PA$e_-pm>ohs#|!(wq&Ly}MRYndwTe7zB)J+m?&$0$yb8Hy z&X`iK5lU74y1npeNJG$@<8`SpLzuO28{HH)+)gQ()4no-Xh)-+RtKtl9`A8s)H~Ga zS#v2l;d2>bTtWB1x3W46gVQt;>xHBNBJ@%&0h6vFBQ|y1B0i}fGQNkgHKDL5@LiZO zhGVdH_)$Vp{LT2I_$NldqTuJ!#e#K0nDtgMp zo`KJaar_euu0q?)k7=>v4qs6dgg!7c*mbLoUmVXnIW(RSX|b712~rz|jx7*{YiZt3 zV7V%9z{xF7@hD|q!hB7^B`8dZNCN-ty|`ZKOTRoPcICPDl6b}g_Q^5h@;C^><)d=2HYe8uUp2pZ&`or+K%0e@G#}i)`YB?iv$HkxXXB=@{%WJJK zV1+vaz4&nFx03C^h22&6CHR`rf+Dh?_RHgx7&2zvH$6Wyr$&yOn@ZV7176FqW|5!7 ze3ap|+01E?Ub8)vF(OyAJva^<8+l%;Dfoh$6rPQ`K1=9t;%QD24VdgD0!A2Lrzd!O znc!V5oUl$Uk3mNcbJch6;`~NL_qx34E|@xBFP)4G#YSX+J@&~N$Bo(Ah5B}6dE)OB z{OS<`yz?>PF8H?|x4XgifUD{{zpXC$45@$(YWD-wqJ-P(4L;OjJ2ai$mrV;2vXT!^PlfZc~*Xs~*CVDlGRPjTK#IzPYKUzvqs1P?RQSBT$m zDq;at>qa&}FO7ZE{hEqoLyY3${HSXkQ&`G~;M{O^?77zzs#4@oXrb&T#Kh=m{MP-1 z=&j51qjUy4pc)$M5}er{!(mGox%;rqL9&6O>nb*3lcfIi=^<|Mry7FT{k8a5r+EcM z)INKiJd#z;!R z(=Z-Bt17=6b%1=8OP5-G%+A33XZaw$#4Yin&~(>ezs`3%J}uoxg{P4H!p2=~n#_F4cOz^CDh^eKY$$KcsMgozbWYm>QAi~pSQtj~=%&D3 zrcPo2m!$@Hco^N4)2onwAPG0nHTIPi&GwPj-usIYZ-W#&0%9~%KVSW3FwPotu z{LLbdu4Yo+i#O<^?_(e1g%rfwa&fDIc{iMx#0=}AZjd_iTk%I-AACSno}ZS17Rq1u zc@I+_-KDGb>Pm9oQHWBk_76SCF9}rZ#bC#QAcgS*_vY}JTSw0^#&|h|-Tm$86fz`{ zqpH!21`^dE(o^9;riho|!MYMu``L>KfekmsgAn<485muFg!CCH9oj>ilp5o7pB10X zG;;(>xy!*O5gurcYgdBo6NZen0S$K-u;mbHV!$rN3G79Eu?*&Lp^0%2ZHDIe?6?CS zIv%YTq{C18Z@I%X!s*XT2f$Zif_r;Gl9j9K%62{hTXWwFaOaTa`E_TbW80RHr6QVB zCUB{Jgf^~Bu3uSjt7UNz@wL)XnZre<&ebwU+Z5^rg}c>U9b`>!aBv8H=BP3h`Q_ZX zYBc?Lx}EXf3}}R0KN^*Pi?a@%t#<+J(nid4gyVG)u4!%;!NrU2jsm3xyQ#ZvykzFF25AEem99d-J!5F5h<@0+ zU{g%KyfM43#AI-Fad~bMT*lKkpNz|^R{R@{p^~y!wE$@57%5uj3%d_vR$&94p0$a% zg86c1*;nC(R6zUs-c5s93qyvf;%V=B0&)}~KJ(+JG-ZFhc>X?gmp@8_%0j@Irk>O@ z3M(@^Efb|J+8-(%T}e-YdGA>kAR6Y50oVTLDP6oFYos#+hC2lOxQt?N`u;8*dZiu) zYw)n4=6f#E_jRU9%>2(t8!%9mU-m=o9NK>qX+mQh}{fWYQ=$Ssr{-f=1Uc&vCgDn%^ z^2mG&L*~DegMq*<-A_qTAcra9!JBscJT}`7WUsK8`s}u^;F^|i*6ot zhftm9gc~m}XF6^QjO>MXAFP@4MU7^T&BO(q7}{Jn!T zRWcfw2R9f%_S!HIh!06!$MCDh6l*bVUmtF{S{S&*cR%+=N4ZRzYf`3l+?24mIu7|Ei(t?%8ONx*8HMnJhUc6n2} z^|?fNtQt#hhR_SC*GMgtZHC#Y!|rT}bnSW0kDf*}WO+un9#Ufyy|fpTPQ9zA%^)T8 zJarKa;K0~4R=*J#?y+y3V^zkcMX5CRs*<^ZP7D<){xnE2Q!kwCyX4&eS8jt8;)ePz9Bl&NQ*w(aRD9b67+WBzRWgGS<2wyn( zEW|rw(D>Ofkso6Y+9Xj!qD=Q4Y?7?cZ!XQ^2l206@G21i9@$_w@A5Tk_N)@V&l%+` zpLZ;S`%Z*VuUJ$ci`=9sNm0Tnc~L9&*cLwkaZkUvEuRQO-JXspcD_+DPjx^3UgRG; z5>^_<`s`{SJ6$}L#KiSv4~0^v)deDN(BDI@v{G<5?FZBNxA8!C^K`HX2{I2VDFh6= zOmmvzPY;2B^>MW1Juy-tZcx=`oE4+1vpt~z5(3#!Y29>-a_;2i$cJrAy;%N_UP4|0 zp@pPzr+DrC-<4Z&kzE6ai3S(B@En^^CIsfQFZQ+<+9|@8DbF9^NGqJEEaJA$TM9{Ptg|};sI`)b+?m1iw|7`}7bEn zG_jobCclg#J$<|pOPL*iAM(nhV$Eb3US1vok;s}XrFYpj-a3~N?e9G*uww@!Kgk{O zV6!qDjGVVtB|E);aa7gP)sK;0G7!OYLSL*CdhEW#3VrEQ)HJFVmZIHn8D4;o?elZt z8hw;5H(9x|!OHuV^KqnWy;8`0hU3q3nJVmbO+8dVRii^{N4oD+hrDBA0F6qAyBJC; z;EnzhQ{=KPc(ReP_HQkMw$M}oHI+p7`?97zp(ewubH|S@V(i5MWP?bRn)PT zkL#D0E)=WHwF6>_0^5@qiddDU`k1rfLN$IyF?)-Hd{ z98}=D{M11|!7y;;ePk22;v1$oiGGa$j21uP_>*L05=(DJhHde0Ih*o}7_uOa!Xc-)lV5S@+NC zatKG1ezz~W*6#VrGK*HlUQx9ohc9r@t4#WlEK)pp}MRQ^ru{@_Fw2QYU=cN&p5!lliJl|yY40KDpQA4Q$Bnt{;(wPDw(NT0%=dm=$ zZII~#mdrJg8Mdrqaz38xaF(tBE2$$)nI?-&?b&LEc4wCU4G(uG8|qr5NnN(MjIdIk zu-_Yv0;^n!-h;pUM!Js9!idrmwlT|k2YIClGHhBllN ztRBrL$WQDPBk#7AI&K&eYx}IYfUM=$(|HqvD7Q~wPu#$LRU*V;B%Dy+u9l_1Ss(N7 zGlb7|{p$-WLayDx-^+yL7e4eC3Q{0TSTxH7yc2V-E`K&3%2&Zl<=2cmRo-?%cz)OZ z`8!MreBQ76LwpPeEFvXxU`)IHDRmGpLN4Fj$i2ZAYrdZ8+ag@ZP`iQ)GJZdD` z_Rd!U`U5zVA(D3vpV1Yx!Q=J__XpGCxu(csP)PRBNRP3ISe<+zU}{Wi3D?hxSG6}N z>rh}WkFe8_X9(SYk!?m*cU(|F(F>>b8tUTtcg;@gd5zp5zn*!A?Srb0onwQwI<=7` zy@ZD>L$oQcr~Gzoy4kQ^3P`){ql4Q|j~Y>y7pSn*a?EyB`H_Pwz(andSbaQz`!y!W?T)Dc^>AX9c)>X|Fx0Qu&53#LYZN%S%mvpb z`7#$lfQ=pBZ;ZoAIEvE45;d!*^-@uHir^@;KnBgh(Q16|#jv_$PhHx2O0H%evO z05UhlpjxxJa#~|AJ>F-|WWKL7yPIqk+&cTUnhe)fV=PX0>0@Aj<2Njcyn=ci^7p=+ zj7q5mp9pEyqGvzY;N?`nMb}uAXxAUQ4lW9sYVlM`{vA0gtm?xuDNu)a{7t) zUPn(;Lx0+_AjVW_furH!1GFD_JUg{Cvhn594OU!A8n+(hYj3=~Rv;W8@1(#*Ue1 z7~e4eQk2OTx=5ldVqL1i3n|ziB{P{7f)YuN-zv>Jm|U7?^D~kqyKc!^OA@5^J%M|t z2fY?7XJF9na$F}Sa*&9?i{qmv@BT%v@#=;B#5*VZR9?*4_da`QdC1geT*VT$neF?M z9||JW34gUi*2E~!26qnZ8g&LunyU5}Y;S4?S_|FMxOvYEK=vqg3vxMg=i}eS^Nyjz zx)LVZ?ih*lI}Z=&*L~4cSq1T@2bm_M)x3lT-~bAwmNM2cSJ#L^&dxg|^P2p@@Yqc8 z!(mHD@M@}cbl{~Oi{iAYI`@+xKh)KIJ}W$CXDqN>Y~VCTo9sbMQ!`>6JP;t3dW1w-yi6yrwQiLTDgZ>EEo*FKaUA)#Vc z5i!2x6MV6aId|I}^%7Det$9H=dwnU-(nvxv{&^E+f;bUM$UX+4IjZc8BO`Hccsb%Z zV33oLGy}8#(U5lZo5RDeAW!8Ikh967B-bqNpL^T!xv_-7K8w5cjRpr!O}R|Dr#(RF zJTrKC4O=F40yh>_(BK|>j5^|h~&eq=Yx(bl-D4tg>K zs5>bo!4w9=wAIaM)Xf%+c{ErHcr2xctA9<+>-L5m#iMAqBrUP%8b0|cU4+Tmp166r znkZ@2p3kljBZIm;FU0{JiXkcEISV9hmZ(5$r#x4};x;ScdVe`#&%)C+up=M4-iUG$ z`sx3YIvs13`}SG171#s&*F)QaMRE)NnCh(T#XDn;USeaEAI8J$ z$df;i{;N*G*$4Vk+?(pH0rKBo+n$~!jmj4imK=5tL$TH8M8f%okI^*2gaCSl3@@|8 z?BZ-Q2}phj(pA`69ozg7q|>aMQ|sDYGrS$+uQvi>;;}yrt(Mf9cQdO(BlsbH*b{ch zB9o?JZ!DQ~L#=h{L4JmDWG{;EY&3UNTmX4VercRRJOmj?%2@U-52xqjaTfBUx$Dio z?bHhMHdU0IiTKz$7&ZMfF5rls@(pp1U>dKjv@yeezl{8MxpSHd3?=7W#j+HsHyPix zVmpRi@MOU8xrb@25K$@M0Zww@|wiy&!71&lF609W<+NG8qIvMRV&QUdUH>_^FU5=IU z&S>{Ld&h5^L`ss?7yzVM4=v(4QR2%8y_v<&ec?~t`K`uQuZBNqzwX|ieWN^tgsu0v zkq$+-96tH|2vei>@O&(2o+qg0+u)qUTLAu&tCFbcdm*km8|brr02ApJ=muBC9C}%3 z9YK`o|1RF;^lC6Jtg$d_vQYBmm7RF8%4(`a&8IFsu@iS(~ky1a$hOPKfkS;^w-EMKK!erzHiWwQ=y`9m8(3oorug#0)+uTQm zjpO`!G7kISX&1XJRWy+B-Q3~Yj5kaJ(-_4s8$O(~?{TI^%x)$ml1?4Eh?H|k_1jNH zpo%rs-llp2)#CvM&2SSHvF{nYZu`@4RuJQuyp z4kG`U=aaD9!S`Jn&wIO~m-%(V|ny1yKwCpb}!4nz6Mhch0lGEO2> zhto8)crLx@|`{onm&+z5eu%O2{E35u?bPuD{S9DXORMu=ha>ZGvig8;cGYi>7q)iurz|? zpC5vc*{#5&mcbii7%O16?y=7}r>}$v_g>p5Bs&@x$&gat_@;87J}UhR33N=kcqr?d zU}D53@YA)TRpNjxr?H0Zw-ziV6#8}YTmlCV5Y|!-r4SZRn5d|++=8dJRbVL6FElgj z&{}BtlNP>lAPiiY=(?46|BmUJJvT5BC~GJfspB$G{v~1*Vb7jbbSFwkQd9Cpsg;lxtMya1^rT9w^>5ZDND?7>u zHNR#Fn_?BZKSZC9({vkLF^|>L{OSzo_Mz`5#{8vkp8m9N%6z(njpw^+rchy1d;A<> zM=_L}FsscX>tyj>yp60*Y2S1WKNv=v8femhS8V>(Cxu#-&O(7n4&+XzABre)T=?hD zihyRy=Y8v`M$7LbaLn|vHmaX=+?|aW64m6;E?3hABkF5W{(L#$>O#7U2S5?jI@c@L zjXHfDOwVTzDZz6O>N+N_5oGgMeS}_WJmYZKXsKw030Z&@Aj#Ei4=SLobZ$K#1Yq&l zXKU|^LztF-j3iq2{p2d1&cJLFSQ)MD7udh!lQrDAn&Fcg7CUXeH~wPD4wR>)NID%P znca*EQ%$sS8f(c!4GRC7(zwp|j%q7R7?^sH*Pp9St;A!c=Y-ABAEe(u9~A%j9QjH1 z#{e<3K7NuUN>p~CC7g^5SoKAN0FYJaC>3)fo$?fH{}_>%oH~CQ_M)i!)#O%M@?e+T zfmaONvpXe5Vfe%V#kCt)$2?m(kY>L}`@`hb3|3Z+pTPmTii#2oyXnkFF+JR5r8Ub} z@l}N$(~36K*aO|Yx}P!NvB1NB4?eZ>rOaeif5jVBH&iSo(G`E>n>-FoEI`$G-d&g* z^RAt7mW3}a(N``wzOS-;Q*_e2x}qjrekA@B6NTz$b8v5LLWlbxjcrqT+D_~~4ks#$ z92ZJqmF`uxQSjFOqilo`m6G`{RQczGrnsOMl>BifpONEo(%~pr*+oS1@7CmbmUN*W z<^5bliuikM7g9?bQQ7lJl)yC|<>bf?CK`%?mT9442-f7AS3!> zv+VfnCaSMR>lX5DM0MTbT%n5uKOK%H2CRfduoTFMyS?H=W~^QNdDqe)XJ|DZVS0_jNXvn!?HQO_TcXwhE%8k;8|ocP;!N+B^IX-@%^&E_;^1g72a3~ z^Z0p~tQU#y0FV~RxLIg=cy3opQ~SB>SQ@Vb$gIqbs?4X?jvm=R;m%SsMhcIFQ`s1_L$r|0aRo^u#R^A7}6Xcq4@4RL{7&t zSlfTGRRLvbj1n$Q)wF3_#iZsSXbh*mB`lYgRf}nC2v?ilORH0Va~YmrEZS@7PC=63 zB8KW5hDa0cx|H_a>e`Qy#N{K9U1Jej^0zg= zb7VGZVj$T^Z-s=q=?Iay{oSGC%E8QmqCUEyROvyKYj=vu5A)H$j@Hi1j9I%6wDJe- zAOU=7yO~&`9i!7wQx@~XnIzWdu)8S%LD}d;bB1L$47jwI2>CBfYUl6HB;$09CTnU^ z*jGlcY=#$vo&Ci|XzTXZv>G%5g0`J^S1o3GJ^=@xsopQdMzFMIWvwaWUQEnKq7X>+ zp#@Re$VI1wXvH9zHDR8Ar?fw!oT#@CTn1>A(9f(Wj`7j!x;n$=tv=KAFX9P4B3CKq z_VQY0doR*kk9z?WpG9t9g;2VY5r&G=8`cCFTR^ZJ!H3wygr2S(_P)+1^SBY0ubms} zguqZ#_=6e$2QNp@jXO!@>BPq(U$5-3g~6d939YrY`s$d` zEp~Wc{jj;iK}iTkaf2vd1f?gF6pbwQhFs-@Bt9>o zz{rdpYean=@-?q<$4FB^98TNdeO}5!I16qIs3EwTrQ5Bw^`Bn*&5(> zoBjK-A~bsS)4U6t|3mu*`+6k&Oq&pc`ybe9keqxwEw*0RyXKy53}28Uk#ad3jI1vitT<0zqe(@?P^A z8De3!M$fPJ@qDdnD~sDjQ->Y|C2XOuvnpicJB^;%+dcr}b`er|ceEV40uzulE?INK zOvn%)PPUk;9magzM+wPj+@e3g;ym{Ceu-%5n>8MgdUxL<;5FOod38n+k3{nDN??gn zP!wne;UXUdwwFqY^vBh&xPYmkXk{QpU$Pr#bi4W{ z$JmYsa>94sRCzOGno9S~qvvu!vo&^JzPBMY#wDAtd{d2Okp<)i&B zSdl-JciF9|I>#e3Mh6J2Gsx79k{Ps3ssU@L_DL1lg=sz*Yk%qYxMG{Wl ztkhP7XezJ50Jh34g^s0#gtrzTgYnUZ*^w~QlHEsL<{}?HQ38l6i3iU5AKJ&JvcY>b zpLz>MoiixY%_|R-i$b{~Ey6%ORxjLx;I08j(TCHqu&HgOq9+N8A;vj(>h`rO)otJ0 zz2z9HSaFXlA$NLS1O+lsB#nLy=$^7w`}@2_Ev=(2k;H)Dx%jH7AkL$cCC}kP{jHs4 zF1vG#POowLA+X%9WSIJN8$IJyKS<`k*lBo|HgmQ zM-;#fcH&EZPXRRh&|gYpWbESk6Xgf}{A$e)`Kp3-^mXYrH}|HZB({Vu)qX_EVAQkowX zN$6{*<6rwT#Bo6K)!b~QM?6_8U%sf()B(+C?!3hAY4@U1b*^)->q!a}ouItM-Q8fn zc_4Ddm@))A0yeIQEG#glDNS2#Wx9pI-+*vPrww0&W;bc69BR|aa+#V=$jj$qrF;}+ z@IcQFNruR~|KQqiKBp-_{N@C+up?Bm(NAndQzbJhF?O-4-wVuk!Cp05Pf>*%Hak_g z#$LE^^OTI@wLMD_*#4@xpAU~T^e{f13zR5SE-)HKg;@ukS}n;AA=eMn(0pCR!fU6V zI&$Th#7XPYPfMe1lm!=CpRh0J!*h5c9M z;U(z)_6Es!lO>yU)Cwg8CnX^!uBej4(gszOG}i`Y2*u(a3~q;N0JlS1z5BnT4MhXc z6tK|jTpUT`qtK-P`EWT3eFJc_v+Wd0#mWW#n~;YU#P;9VAAk)EN~#)%#)JeX^^HSQ z0X(e#5(4J=w-7E49`?VvxVbp~je*(z;`_5E2gkp(fx(>r*#q#u9pwVE|K%tv8z(#a zUz7h}Y;1qWfw*}%{^dM3i2H9b>}>4p|6BCCe{#wGhmSkyasnDt;D3+(C(B??&|e&E z99(Rmzv5WgdAQlwlSC%}Q2Z7Chn`p2;U z*9EL#RxX~us+$$e!S#1B{=vBaJ(q)tnDg(-`E#25%Sf(2&Cij9KJ$m-@9;nU_;mOn4NrwMW{FUNA1K|H^k3Xpffw)<@|4REGjQtNq)jt$}dGW_L@Za45V*iuC|S4Kc!u0N;Pf7b;F z{AY82&*kFzKeNCH1PcRTFrewRFgJvSZ9Ocl0!2*FQ;rePndlK?1dIf8w9?rKCgFmZD+HZ?SMH8e3ab8Y@Mu