From fd6f8b1945964cfb0573acf6e0caee540894472c Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 9 Feb 2014 15:03:45 -0800 Subject: [PATCH] refactor(builtin/num): simplify proofs using 'by simp' Signed-off-by: Leonardo de Moura --- src/builtin/num.lean | 41 ++++++++++---------------------------- src/builtin/obj/num.olean | Bin 37655 -> 38268 bytes 2 files changed, 10 insertions(+), 31 deletions(-) diff --git a/src/builtin/num.lean b/src/builtin/num.lean index 5cff6efad..8b73e7ce2 100644 --- a/src/builtin/num.lean +++ b/src/builtin/num.lean @@ -325,8 +325,7 @@ theorem simp_rec_ex {A : (Type U)} (x : A) (f : A → A) (n : num) : ∃ fn, simp_rec_rel fn x f n := induction_on n (let fn : num → A := λ n, x in - have fz : fn zero = x, - from refl (fn zero), + have fz : fn zero = x, by simp, have fs : ∀ m, m < zero → fn (succ m) = f (fn m), from take m, assume Hmn : m < zero, absurd_elim (fn (succ m) = f (fn m)) @@ -335,31 +334,14 @@ theorem simp_rec_ex {A : (Type U)} (x : A) (f : A → A) (n : num) show ∃ fn, simp_rec_rel fn x f zero, from exists_intro fn (and_intro fz fs)) (λ (n : num) (iH : ∃ fn, simp_rec_rel fn x f n), - obtain (fn : num → A) (Hfn : simp_rec_rel fn x f n), - from iH, + obtain (fn : num → A) (Hfn : simp_rec_rel fn x f n), from iH, let fn1 : num → A := λ m, if succ n = m then f (fn n) else fn m in - have f1z : fn1 zero = x, - from calc fn1 zero = if succ n = zero then f (fn n) else fn zero : refl (fn1 zero) - ... = if false then f (fn n) else fn zero : { eqf_intro (succ_nz n) } - ... = fn zero : if_false _ _ - ... = x : and_eliml Hfn, + have fnz : fn zero = x, from and_eliml Hfn, + have f1z : fn1 zero = x, by simp, have f1s : ∀ m, m < succ n → fn1 (succ m) = f (fn1 m), from take m, assume Hlt : m < succ n, or_elim (lt_succ_to_disj Hlt) - (assume Hl : m = n, - have Hrw1 : (succ n = succ m) ↔ true, - from eqt_intro (symm (congr2 succ Hl)), - have Haux1 : (succ n = m) ↔ false, - from eqf_intro (subst (sn_ne_n m) Hl), - have Hrw2 : fn n = fn1 m, - from symm (calc fn1 m = if succ n = m then f (fn n) else fn m : refl (fn1 m) - ... = if false then f (fn n) else fn m : { Haux1 } - ... = fn m : if_false _ _ - ... = fn n : congr2 fn Hl), - calc fn1 (succ m) = if succ n = succ m then f (fn n) else fn (succ m) : refl (fn1 (succ m)) - ... = if true then f (fn n) else fn (succ m) : { Hrw1 } - ... = f (fn n) : if_true _ _ - ... = f (fn1 m) : { Hrw2 }) + (assume Hl : m = n, by simp) (assume Hr : m < n, have Haux1 : fn (succ m) = f (fn m), from (and_elimr Hfn m Hr), @@ -370,12 +352,10 @@ theorem simp_rec_ex {A : (Type U)} (x : A) (f : A → A) (n : num) absurd Hr nLt)), have Haux2 : m < succ n, from lt_to_lt_succ Hr, - have Haux3 : (succ n = m) ↔ false, - from eqf_intro (ne_symm (lt_to_neq Haux2)), + have Haux3 : ¬ (succ n = m), + from ne_symm (lt_to_neq Haux2), have Hrw2 : fn m = fn1 m, - from symm (calc fn1 m = if succ n = m then f (fn n) else fn m : refl (fn1 m) - ... = if false then f (fn n) else fn m : { Haux3 } - ... = fn m : if_false _ _), + by simp, calc fn1 (succ m) = if succ n = succ m then f (fn n) else fn (succ m) : refl (fn1 (succ m)) ... = if false then f (fn n) else fn (succ m) : { Hrw1 } ... = fn (succ m) : if_false _ _ @@ -384,6 +364,7 @@ theorem simp_rec_ex {A : (Type U)} (x : A) (f : A → A) (n : num) show ∃ fn, simp_rec_rel fn x f (succ n), from exists_intro fn1 (and_intro f1z f1s)) + theorem simp_rec_lemma1 {A : (Type U)} (x : A) (f : A → A) (n : num) : simp_rec_fun x f n zero = x ∧ ∀ m, m < n → simp_rec_fun x f n (succ m) = f (simp_rec_fun x f n m) @@ -407,9 +388,7 @@ theorem simp_rec_lemma2 {A : (Type U)} (x : A) (f : A → A) (n m1 m2 : num) from iH H1 H2, have Heq3 : simp_rec_fun x f m2 (succ n) = f (simp_rec_fun x f m2 n), from and_elimr (simp_rec_lemma1 x f m2) n H2, - calc simp_rec_fun x f m1 (succ n) = f (simp_rec_fun x f m1 n) : Heq1 - ... = f (simp_rec_fun x f m2 n) : congr2 f Heq2 - ... = simp_rec_fun x f m2 (succ n) : symm Heq3) + by simp) theorem simp_rec_thm {A : (Type U)} (x : A) (f : A → A) : simp_rec x f zero = x ∧ diff --git a/src/builtin/obj/num.olean b/src/builtin/obj/num.olean index 6f986a4aef140ed6b3e594d196ed3f4b9fe4482c..3038a7c20ff89e10c3fc7f0b33f919b8096f568f 100644 GIT binary patch literal 38268 zcmb7t3$$HTdG31bz1Q9*(r{2A^$CH51m&85C`cQ%90&*@fYzcNJsgsA;OKdTb4~;q zz7Q1fC>IMpXzg`qrAmS?uC4WQ?}e6dP(Z-e){9Epd#|7oLp9bh4BYDdzweuC&biiJ z=h2LjnYrft=Rg0~{QrN>xz^6q_{i|&=-Bv3;{K##6FaA-XOp*$OizxCC+=zM@N8L~ z*>&;kJ9dsFvzI2VY;xB`GB$bX@Wo@ZBRhu1CU+!j^2|3R2_AMN$+|onxngW)c4lZ~ zd~6~~y4f(NOHrmpHp-{g(Rnru@MAFSts~oK$KLMf5?}@}>ztgL9GclR-2efA0!0QC zqhpg}v+uB$a)Kh;GB$(mWW_p^ISQNKU{L91SEyo4Ois;mu93^wl%#7gI|me~k)q6q zF^b96w1ES(gF^J8HegJNcRabC=b=^<+2!~b1Z+|5xd!Z|XX2clo+5({$*fN(=stvyzeUJ31SKyL z`T%SKU1k$bIYSpTN@aZ{xN(k1UQWzCJOt^j1BbGl*{PwxE1<-WpR#Hc<-9d~>p98c zENhCQL7W7{CwiP03{8#<|1B+JS)_sdT zZIjYQ45vfbRMv)N$jEI`M{+kn z;gY+TqEVP$hUyk#S`~4J)=N=v`~XRz9f|K%=nC`~XHM)yO9F1wG*bD@#PIm|$jq#1 zFET5Do>4mSvm?b0qbGS2$ua+Fj8v6}rpQQ&a$y;3lQNt)QIuqu2t;WxengySrAhY2 z#C&BLi-1;3=X_5)eWC13Zu<-i9W6h^4K*+6q8D*EBx}9biG6TsCUj440{kgC%Hxwj z-jyTHWzVh6Tj+fK@Wm!Q{^7XuQPsG!7(>~GVM9BoM|SXu-u=dabY|D~?WTZ9cFv)k zqksrEN3Gw4R!ujW6b-s}Yh?3&w8K@_C)76Si1hRv-Cx^imN&(9DIm=tnFM*HL^0MX>_qg%Jv}ucfsv*hmwhVf{%PrISF;kVRgC1~hqP&<#0>+%BiwL;B8@ zW@+bhwt_9qiW8OlicG4zkAmM=;T@cO2E{2GP<|Cfupx?7-RSrlr#lZ-FN8cB9Uh+< zVP0p;a@VwxQS;o?%PAZr<-7!SC(Gd-JBFsG6NKX7UE>r_vfbOLWxBg8Wu2O&uk?nB z;e!_PHb%jC-kvvw6p zX$oZCtRR0|)9f_%n~z3LO+tS{jU3JiX$wk5_F=}Kpse3oNT3|LBP(a}dOiXn124TzHc7)aXo)0$q1XK83< z6Fe6%;i(0VF$J7A>;`q32GOhCTsIH2rq5rOW5!ca#CZ)Kzs?b#LN#~`vt5X{=3YNo zpSI3Bkj$cx9^x3^6aoe1Trf3q0E71*Yem{aby+h;(#06!;Ifh2O27Oz>xDa6@-a^Qej;S`1E?y7UTd}VM7Cas>MPe$H6YH`6pBFl z=92VltT`fmW)d4OI8vAMP!A_#F#X{k)C$h=AvS7`Yvjskd~>9>F9>lU3%U30s3-G9 zIgw?gThNmJ9#_TvoLFfC5i*(B4T#+?RHbJV=HW(2TK8s!W`xZoJqKkl`T-YH(E3&s zbLZ|ix4^L*`GUpqeyiK4}%ZZ-ill9PhPNBHbnBx9@5_Gp=$Kgu@S_>7?$ z$(7qWQdN}pTLeNOQ1HrE4handTc>7+8UGALnw`qkwkZd~8$+f$Zfg!_K%P#o<8Jmk zz`9_G>CzEAQ&(EC=Bv2;XPG$h;lg)lgC6WynkQnhYw+b`|1eeqAsGoMUv0oMJ-9yA$MUg_F zrgXI?MfDP3RmzL_mA(tbyNUU5RNsl>Jytj%HVOzmSCz~1R^}BR4lX^4AUO^iGJ}@gAzZ9)t0&)^bzZv3X;xA(G!L_{S=B%V-h*QQpmSj z3xr%Q_Z!3h+r&LNJu*5T9HDd^1V`TG3BLr?bF_;4t(M+iWLwdc-mc&XWxBaZz(aVn zLrAAKtGNBA2{+p|iC&X!HfdGO%93U{OH+Cn5a7x&RCi@x^r^A&;r6f-0EdGietDX} z4IL|3a?9_p2uvQorm7tsq5IBtD8aEDDi^>gx)x+;X2O{w*`Obv6?ee$l@-~x2}?eJ z0@_PgQ;^^`rLP=VfvyYFKJsGoUC zh9+hKWGnEbkFLlj&wc|rh$KW?nOF4V##X*uv$`oT{2`fBV3v{-82X8atQU0~yUW`c zk5HVUNtOZMJQ<GRPURBF4~Vjw#zlN0DB*BAXer z{Bh{Yc#}E@Ac+Yz%V`bBa+wmy=P^{WIl$Lx}P*M7mV}W5W20||cP&P;9$iUHC zJF}UXnw&D@ZVdOsNzjlG_-9FHH#PBhK&yc8_o~VXWbJkKNGITO1bfUn0I4{E@>q>- zt#kr_sxJTY>Q-UWnwpLe2&h}Plf`&#x~MAbU7D@sycrr!dZF#Arl$K92}H`QZ$tGU z6f2Lj8`8*DL`nw$1eHn2@=Itmez)*+AUn)9$Ch2y&wDmwr}r$NO3%drC@nhzHKTmn zm@|L_Xjnx}_fQ4HX&W_~61vmXW|TAUn2;Zr5usCHg7O&Vgcbr8s*Qf{lG>2y8-1?lKiQ)sj?#= z0|qr`DtO%QoC4)DVhtHi%d!FQAKWuwX*G5KP^LWyRdEzF*KJpPi)RWL()KfJ)yqlz zE9R4v_?fDUISC&5F6JaK(X%Sqfw{@5%7d{b`za_Y{-RRx7e&&9i*N}A*9wi9Drv|n zs5;uPw7eJW&^|6fEo2s24QTV%H&59^EYrzSp7CBf$d4rKVfi%hH0BhU99#~7d+lVg zmMdhlito%kln65X^+oD~K2l55xJYfY9eBq-1k-X==0C?8R%O>y>9;< z5Ybl5G7noX${iOFWR-lErF)?$$JQ+(SB_4kEW@!Y51TB>KI-k-V6*elmX3<+U_{hR zjcd2^Bd!BH8|fKXQz-jK;4V*tcv~8?T1oAqQ=x#Axgsq&Jp`zlE%{b-Vb<*OemlNZ zc8n$D5@Xr1^H=G!tvO9=`Dgm<*s6IEVoKRDHiMh038GqPuS0LY2P|ZCsW4He5_U-? zhXDsvf`79wuCp@ActBzHC3G#zw#|b{`z)cj^e&idb|{Lgy=7!qd$LsJL5wqhdpBl8 zoMl%BQ{iIBPN-R2WX7269)q78QM~m_+o82k-Isvbn56CqXf$+(?_V(I+EV6RmJF3w zNPa$L=LbpYM)3VN|VU4^vbI#%wRf4n&E|K{Tv_5Or89 zbGN*~-{yHVbm-|y!p5hK7|Xb^((SP_^)eMmb?$H*vbtwi9S)D;vj-@q;Bb^>?EzA* zS9TwO(@CBnbAg`y)|Nd0nJ9_EvvX1=aGy<~^J1oOH*>t~QPI!NesE$=eZ9c9l^Fia~>*u-r9+ih9;fNhlxEQfLE+ zXqAaF@akB9uXQ4FfxLtr#gU(O(3zv5KoPAce2W@3~$!%feiM-+AilSKuHaeorPD{o{M-v|DB=Gw=_J#Rr zbsJi>4$WJw2#dpIrf6%hD{IYP=8Y-Y9}v)@g43Y6I|ExBNY?&FOehiZ1t*E{O_)!n z@dp5~7rDS$^fpBPMq=k}74HicW``tcjhn;Z5sgMCdBs+3Q{fEhl7Krz-iXK0J-Zf^ zQj$?WNalo*>7mV>X*q*Y;;NUfkf|q1cD&=DvG0S-b8>)Zw}FN6mnoZ7?L<6Kv@cK; zGC!{*HwuI7HHYjq_BJnHd#woK0J;OMGXc4J&|Sk_mGLwn@=?VyRNsb%IJhUPyVjDP zjdn5SMe{B{oro;};~8+5LpNAkj?1$AJ%Qf{2xCYSNBaf#25W9wU?W#7Ykgt9Hv(fy zhGe!hD4Fd90A#lGNc}q?u0*cPOFY9%SQ`z=@?kTV6!`6xUm|xA-a5*2ZN&$JNxp|- zmAQkF%iL9O6clIIkcG%`k8l!ePT?sSRmp&5Q0rU3nGlho^ z(kqK{-(_Y#L2A=Spr`cb5P&ip@`YLRKeNJKLC*2dT_`M%N2!Y*IkIumJY}u<_&Sta z`J9+Nkg2R>9up-r5U3{q93D5bQE4{BOh7>=K*SYx8F9XQlA{(_=3#0RF2qV7@eRNO>^0E9b%I!3?N`!+!+0aqK zv(E(LXWlPqYI7!O+B_R8^C06*PsG>*z?FYAkb6*8d=)ym&hr0eHSGsD2W>mM1pT@% z0MUG5H9G{2R6DZf+3Dd)UMD5Vpta`@Mw0*#~&m_x34Ts4K~Y)ZJ1xCI?`Nb*Bdyxh^2hR(dnx#$MJ;!%p7m*BTNICIyLJows9XUm4DE}n||01h8Ak=J?y9DM}q&TbxJ1qcJX}lhAGEsZ^iWdV~52QL9 zgs5Z_9Dfc)$D@rFdUTd58yvL9mcCu!A`S->*$>f0RXvQIV2%Kk(VWBD;B$*t(==~A zV^AySaBmIS12lr`0}}MZjkR>>qUi~b)!{IElg}Q2@U(_#Ndo{vK^pC~DAfFP31L93 z&XWk3RJ#eIl!EJ(&abFZz}GBkp`<8(xM@Z#7Iuru0Nz?baF8AvV;r1K!@CBgMFO(( zXJ`#{fOu}Ls6IO+fuli=|B!(?QO^+z32=s@ez(ndkLhcRv;nv5FEZwCwTTtvl;c_NO!g)IR z@F(ptQppd!_FSWRk!cLc4_b;oyvx3{3b9?sj>_+yGXS=A>o7pauVL})IB?#2(v@A5 zrva)l`bUwu^;|j~t|M+0-JEQ|;#10O8?a3A>mnCLw?1# zhCF6Dj0de>EXxWh11*b-qEQB=rHFOXx`+kwW1)*iV&+2E^G@_kW4h27Q z#Q7-B?a-c%>Q|!L8V%~?`!{M(?z1l%2iWU8Y=%|Q`e403NPWBYi`h#7`C%4|fLB%9 z+F|gTBMiR*T=5p71?;WsfKGR;gLwYWRwNH`<-ZcuL65U_WgzTI-x`^E>$wK6cT!qI zU{Y2@-^OaTF~R`kn5Kp6g4V}sWZj5ve(NH&kXFw{GV7@p7f6g+JQ7bpb!)q)uXQCT ziRjUGf+|gl+N>Wm(E6!NbfBHCU(|$t=hz_uQ>J0RB}g%GY>3 zZA#^jy1t35QG?Tn91Obl;a z_W8~qk?GF>wa$0`995m~eAa62eCJlQ;#hLzGWXeTj-$-{kJje)Px=OQ_Z_aP4}|vj zl}FQ`w!Q_~!1rpe<#4-yh>qf|DLMwWqZ;i_?b>@{6T$g40WgnZpB03?3cZmh-$y-f zMe9EM8yy!Ca(2OP25X)6e;%VHJ7vj~=x%FtvfBdy-RRsNs$XCgOQ!NhEkBV71OpfD zJnZ5pG}0P2dy`2H1Tqf*KCpsNn`~aNn@o}wex{IqIm|JSkvg;fiq%^GiZ!VawuI0y zGF=_!4Aktm9%ZldBtBR@NpAg&BP%CwfgnmEdZ+JTn1P9u=Um5PI+Kq`Z2}sQg~A47 zsgX{evMVP72d$r5k*;o}TU}h^cL0;t_`Ri*(0kJeSaTlN5+q$VzFOWsDN7V?7qvK0P(WQj;sGr1 z{5jeIwQ=j8hhrseF~YGDpWBkT~bh(B!W#fw-AyZz2%#3vMj)XFSagGgFUXhHMQI47Nx@-Fca& zD<^8>z^VNTD=0dby@28z3AdxT%m6+IxbXdvzXhJX6kqHu82%}MwimEnc`y?>*RZ)D zGk{uwLcz=jmN1A;zKu+#p1kO@E80+FzcQr%iIIx^ccH4*yRDX=Oy5^I-j4#YRwsv8 zp-&q`C5b~m)4rJMTX?~wx{QDk*zKkjO&7C5t>6;PPao~WzktGmQIPiXOZOQs6;2kG z8=2s%nMxKgM_X4|Otbu)w2Fvvy>rj~G{;PWEo|lEbLpTtesV6&Fe(Lxq`8Q~TE87C zPXIT5T*OYRD^aiDy0{I!doY&{ENDYSn|II!s>Ww4F_5yNlm*fs`I0CXk*@|SeZhwb z8HerFC$m4|CJPfJCQh zT8-Wj>h?*-Rb?l=i;`N9UA<$bcb52OLK710Z?!ytzJ1f;NF_rUc>ALfjT{*arAjEr zkec=_46|HVob69+p#9*26*?GT<0pXaW*RyV20|=$UyB4?C<16Y5)Na~tsGWb{_EO& zw^(De7pEvtR;Sd%D%e-Q1UVFOMr-HTFIQ%(kIcYT@C{k8k3uSjt<`v z&UJOV9e%mYuMIfg4K(eN=K#l+D)l)kKH&Lp7uFdiykV;eNI zzeBaLkg3_*PWB$*$Q4`$2I*xXOoJGtkx>tpbN+-C`bNL?LR7sOwEw}L+K>6K4`8O% zPply_XV#^?qGb;XrAB{;Dgv*6E1kAu-^DWCN2^-%a;W|6MRP9~>A*Te+5X=|jN1P} z@e35c^y6qQJJ5#E(EhjbUb)S1r|%QF>=_Ag?L2L81{efRF|Y`L@O;tzn@&sHPoZ@; zWf3XF(-H}Z!%@@&5awzBdbubdB&H7?T^ogKa#;wzUh1^S3YHf40iDR{Vzy3N7SZ0r z*$TPvE}=~aAH0`Fwm7^dF8T@14(#o31QNn4ESw`na=Bh)qks&j=9(W8Gji?Z*WR6+ z8JoOhd}P*s+=qWapnjGp`kmOF(_<5Se|&kbQs-wGj{Md1LXQETwp0Ivs(i*jTdl+U zL&os@EWeZhv)R9E7TU>@ek_LHdTB{gWW;b^*$$92c_%ytiHVjlFsqv7WjvN3tM0>!9};go%LihTE}h+3~Z%KL5+OFz!G~? ze**u;=D>|o=QU_ug+i_fHGU|j+`X}%c*Xcn058QoiK<$EYPHUKd$-8$c+r}4Hks$| z-$*uMC&9QNt{x!fr>r$ZG6Y;8*b47GQMe4=|6&YO=mNPVirdEOE{3>LIY>Eue6sl#j=LN;?y(P+R73K#`9dbmuZFv;t{?(e}QAvkD3cbS`VO z^O-=1y$kE|C(N-A1r=A{9py9D)8SHOKZ8_9yr3r{F_;~$$Q?!JNtmPaUf7w0T*ax&3?S~jFCx*8k?Gdyv~JGRdH?dqtg$f+D@wdR z5Y`ka9YJ_gbaX#n z^jZwV2WpBj{8q~v7_B?61FG~OAy|DHRfQ)wALSK%p}X@sJf9&ak2&L5=+lN@S#uLH zZX>iPF=vp1e+Op8N~Fe)nBQ0}N*ySg!_jsQS2rD0h+>gw>#;$;jUNC=pIpizc1X5} zlAS$P)Puff^#56(|ADad)bgjo($js-{~loa1K;+;=tDyLZXFY}zhC}PtbNLOF#ssC;-;E+wXLN9SV-Hmv6I2I+;5fqc{z%Snl<KVxpf%RseTwp z=ey{s|D;IP*U+o|JVRFhdCly3?pOBgE8DWRG9>$@<>Fi0#Vl7wOPVO#-$s?&=*s&e z*4TN9P+&j0+Kg8Laj6IqZxBNdSmBPL*b@Rz?Vzypb3oo_MG~D#QF`2_qMO_H_BWU@ zWfZ?!9%KD_K$Jf-(Rpeqa_J0q*T{W_*}gxT(2pqqa;bC9&eNDL9AdbUMF02b37jxu z0B7a=!k#-%uK{GVz$sFi;O?WjhI#-X(>igFG6GD{f!9~ayA3r)>*&01w_gaQ2a2p@ zaSudsLC&3Tq0DrY$LfnPRlns#qU6fiYf#FkiaMXn+^9rR93MFOu@b2ch$9(MJTjSY zfe@Ho0b}mK`7L$$R4^tYZWgPpNMsOIjS+^ko9!7)=iizjA^(D_pA_8|An{z#O(zu_ zEuIVBnwOOBk(Aj-%+kl!jJ8-CNm`Pv%a_AQ#(K;cUIvg^)|O(i26P2mE-;9>d$GR3 zps7v5)D5~=QzJxNi4e?Dq*l1b8fJ>~Wq?6PB6DtnAs)ealy2XH=V1NC`nqRbU2k|n zWqoX)vY&|aPPA!x82-+Km?cUE6cLWJMi&u|Vs)*R6~`JW&AN)iYG|}1$U(ds016}P z{D!g!7C%_UCno?&FR5+)L|X897~~vDP2O<5Nl-(?eJ0Hw3}JV1 zLTxn7cAa&THfOf--7m0K=bZVoIzdiF_#aJ@iQoU1#Ad2^* zxW+>v3gcg$D*_&G}dkL@fGpdkMbkiwNt<-Is0T zvi20kmjHPmW@_3~u)DISpyOO{Pf^@X-N)g$#yUe+o!qZ4o7}%%oLqD}a%+p{uSv(= z8a3ob5>y0w9uUO42fAJ^zyEF>+=4ktHLkfk{hAY!x=^|1?kwk!Nh>>qM|5(n7!~&7 zkx}_j*JxdoZipeB$AMJGADd8BSUZ8$wN@^aZh0}e-AG+{a6LMDpeZkAq*8btK_vK~ zs6ilwWjoW|VAbfIk$MjPzW@o-Exu<(v;6|b83Z&_+=1t4cR!8XAHN&J8+D3q zPSn{OCIXkmJyx_E_TPnmu%L0RxV=qXYK&?WXv6}g_LImQFn=7{m`XYC=@skpe-MbX zizNfzk1#T%4;)nNJ@Pr8)7wDzIUcEgTvTcU&rWSYTJ!}?(&`==A@RD57fVeUFER989!5ATArsUn zz1Wj{rbap6Pw^ab_u{E~YIJWVKYvy%YSm@0MI zwMZ0-UV5+P9^F$6>9SI#?#Y0>4@A@>09+osU8t#AZueyJ~^kyt0pt zXeJIfMKFrrwT>lY6q32(ZY%mIq#dKXj8PyXJ01;eSujd$^F zz$2)lM=ui6_K8kntdm4B`Xp1KzRT@C&mp<3CACHP4>GVbFl&!4vYM=&*_1PRT05+5 z0c#&d*CN(VjXIMLLL0O}-4QF6XYD%xxv;gPoAczzB==11^K4iV6UJV=7)9T0*(>Uf_*E50yuemG zvQfj@d7Ru(U$9Pnrp#YCa(jy3L2JKruA(XU&U7cB(LMsWE5>2Z1y+A?XU%-Cx5njd z4lrDsgFCI(=MRY;g|lI+6#s%asnraPH5&4@jkGEa@YbyVTt%;y(U3n9i6NMU@^X&C ze9WA>H(6!LWSsMbWSoP#H`>VVO%zzL9rF2O_E^!EjI-y6vb!tu3_*wI-ZZ%G9~+RP zkW)0-aPcH07{k}7q5DK0OLVa%-&!`tvZKc)TOUXFO%PpJi=yU}RLCvXqXl`BH*Wit z?b+$Ei+9b&uGep$n~s{O8tMafSzcRITe;kd@6biRhO@Hz+E8UUSac->j2K(&;PYOq zc0YjPeZaNANinIzVlSz)YH=ruJ(M+dN1H>GTGmqO{uLnav!eSoD;k#yVe0NaKAfhi zFx=%R8>|{_-O*j#h2m}$d#vc2hsFU`IFGF8Lt#l$RQFhK?OQ-=FL18=~K`QPJ^yoQhL7&ddWYu3;EX_kJsuTEpGiS3exoy_dsls|IVh3(g5s zU&BIF4`Ic74W32!evlZJP4V7fDAXE%S&G~U{u`WWL7*=B1^I0PHF<(Ae@Rgy5l1j{Dl=<>O86K#ve3TNB3STU@w7uwfo1us!_D=`$>H;pL#@_cHs!={yvWo+NE z$Ijze*4ZGsbT)ZnXRwuSQ*z>3sYSJcpxlWu(E3Wl7b`!yeywZ;lG}%fqhQo@16(C~B97y_Xz=)_PP3 zp`iC7>!!)|jXkHso*|)O)ct^^T%!g6L=*FJzAub^qTZBIVRr-!uq^!~41j zNH2>3vbVNTk+3aycgQM$`tAW4thWIY-E}k5ts)KVSeCZ}2jVbgTbzK#-l0}FYDh?+ zb}jnjkVeMVStEUA?ZMrZ1ook-W$IMO}?X zCO#CLFbBt`q2DL`Uc=2VHF^*{7gX=Vq@?b0X$x0*o%C)Xe2r+vfUB&B-SvpqyUNe0 z=^(rwe;ZWphbjv0#{ua!?=;L8lUkda{_R6R_yH0L&U(>@Q|c!HL2>sH-U`Lo+H25V zba!v}JSVdlF83<&l7=AJtE=egxcd|fLV{oK{TWc64~y%)$_jlp1HE-`2e!ziUR&{? z;msX?LA2-|!*KOvjaurUyO literal 37655 zcmb7t3z(f%dG3Fiz5hKVU>vLvtyL-{5Vab>3y4Oofp7}}q?U^eL$W6soJ*LQ2->RW zJPP%g9v&|sUJxoGl0@-_rC$2rjggAQ+GDk#z_Cxud7_Ql*mFv}p6`9%wbxqz+W(%3 zJdexuul22OefRHM>;Ly;X0kgrJw7qn&D?+a#MJhg+4=0X-P!5xWageWj?MSFb2~1d zfBp7uHoq+!DyDZ#WfRle#x9?j?`|2LnBI~-vn>2Tmf>MbmaQ&}?$r}>^K+x!$%&~f z>l9<$E=QYJ#Wvt_H%mS}8$gF&ZLT&<2VF+DTSy}DO&D9fLT-MOGbj}#R~j8ROk zW(^#mZ8V}6y%A$dyyMBuJQ=;JDz3u+gMba{{hk4P>6tj^XJ-f@d?Q=B*|;uAg2^GBz+}VtH6BcEs!pWYA9w$%6qc?Crw~hb= zTfz1?42-bLxfNa*8%+{Y`6|Fk7BI&W{3+<>9kfqnm$0$Pl5#E^A_g`?mGk={&a_NQ zYq6XG;rL!}Oor@CAET5HHMD_vG! zfS%S1;%7yQ9m7oaYLa8|(-^5M4?~fWR6WNs)~01Rucj!;FcFB-VEo89hvZptL1wYC zmy3W_u5+HJov~1Mrm%gQrH&!L#4WWb>9QAbI3%ll)QMwo&rBGeUJdw@OSFHK1@hj| zbs>A_s&WXEXO3NN(&K+zcOJT0cLsAPr?6~v`)qd$pBUZW5s=R9*u2>kFwM!GXm?UT zgxg82zZ;|4fWo%`tLr1X6R{u3NHwXF)55;I@{SPF7I_> z&)lg9Me?brjEM(H%ikEh|i@qn2)zowYf=BiWWN@~LAe!r#Zz z>~m;7g{E4D_QD7S*_Ugr4mQ$6Xz)L2qZcGlGZayjpaD(4A?SvjL}8a(?je2WNVBx_ zo#w$-X2pfd*Q-LR`#J@`w#GX+xfRXHYtY_>CfE?gs%cEz&F#)b*9)O6#>Xb-x~%KW zEqBZs8A;@(UQXsBDd!pJJ6Vox*)lpin;{jC?U80+ zF|-@6?u9DMuOK0e1CMjB;U+9}J|b9mP!8LKgK{N~`Pe0!GKZi*UeB}1@LsWv@qOIk zF)zQoAo0r@HqIgR?0Oo>ZCs0H#7a`jjy`Kq3{l8wK$PvnLejR6*7QO=OGC?>;OW4G zrxv)z6magCThwk^#Hel!?Mjw^0KH$)4wU5GacuWwJcO?d~B zc{I{Poa38PprBj`rbhN-@xEiN$%oNBs2wBeVhwT7Z6vo|Tz;+1MPb>;qfr-?&}LKYLd0kPYqs{Aa%e5(Eg@jB}| z*rhZT3vCX|bcTMcU;Nad#7|;%q;3U$#5$*fq;pdAm|@OuLGvMOq5#+v@<(h0LhiZy zJHq+f#63OR9iI$=P&y8RBkziYp8)Eew2E(7FaKCoY{XFhF(pSR)9pAkrLOQis z$DKb-xW%Sv%$jVAY3piNwlu?en$oub0j?ZFX(+qXm&V42JHt)^907*-6=?!D46I0!l1~N1^CNqwZ-1B)+b2oblrG6V5;;AzmGL!H|-}!fwQ~ z!1hbnfye$_0qcbvuqOXDdbP?hLa~6!1?9av(a$(y5_8J%$?w~a*^~(CXMvKTiCF^K z2t4_N%ZllK%8ZVN1bK;{&frQ`&LdEz1KRcd4RcpKvtiZe9H zGT>VvBh>kVDOz=)5wDZVPHwLxkL@ICgX4t^YDRd(1g0!76`L3+@(Y(0a}!oSj=mv2 zr0xWe#Dt#Jv<76gOb^J{FtS?`mY)vLb+OE4KRAc+nCf1eM05s*ysYw{0S!+}!YKPQ zK5TQF$xpQNHlqpPR3Ml%ri~xjeaM+PE%}U~qWnk40>js^5PBhisyQl029DX}&Sq+6 zdd7^qG2M@4K|?~|pCz5$)WkmmtrEijQddEsXsxzK1_4(i*kjQKNG%BTuGJXUdO-kC zb@x9vwF;Bg%xru?K;62NEY|DLMOESK(rhi~&e3r43++@jGuy97AW~($3*7@ytRl{C zNTXO5DIEY1R3RlRE@9C4-N4&{;&3}0TXmJ*_pHN7?+~EM&%pvHtvC`rqkPkZGl2aV zSV2t>qYH-f7J4)#Oy?`jDCb^3r8q7l!lb||dqHAMvP3Y^(MS(qy%I)nv3YO5`EtyI z0b5{1Jt?9GR+z1$QIJ=~0dP?~9nDh{+2{=hBG6JCNyOl^7_laM z08P;6i@EY!1fu*~Hl44m>xi1nTl5y?0>X%8mbDajy5bU ze+}%=KDMG4Dhqi7#{BD>pV&hz)9Ic(uLBciH519Y+c0p6IB}{tE^Y>@}5}+`qomf+g}4BI*M84 zVg91paeyG}`y-XhX-bR%UIj=l1*&9dSKZ`TG}oQJV|TwDhuqGl4Vo##hf z2Y3!LGO(vq_Fdra-3IY(Y0PS^w2N+q0#eqBwB-CSplY_{k6;SB7FYG#@keCGa3NP1 z%Z^>V$`7^SJWuM+{Lt8{`69%WvSnfpZ>pwT;TB;w`~c z=nTaPiN!@`jLp7k@Y7x8TkqNqt)=R|0?gKAX&|7{FdSYpu;$v(tGTQg>b*kp`>8rV zKuXtw?=O>Ypwtv9B1536VZV*$XA@Xojd(mPQJENvuVL*-RJa_#zzPUam$fo?s~h~= zJdcI}Jzq}P__h&inKzcZGghHlmIAr%9d@CrJG35fcokpVPcemnqbh3;kkVf{y&pj* zdyLEldiL2^aX)0DA_~tgNSVNWHHFawjR?s6ej->&C^X!49+gu)i*o#cxM!Q{o7h+t zE507+iR0f$cYN(?+ejZQT=G!79Vunk8Fipov>p`pPR*bqt-2`*)kAWH7J!IWl_(Rh zuJylWQx4vGi`GCn{Vs~>2pmgSL81^8+<=C(@IEYm7IswNc(%F<9A)m^oT)G$$HHC} zq@zRjad``{lS%3Ep1ud(4cUGy#i?AXnUazH4?syp55km5~&KJ7p%pN}0S zPktGOK#Z7S3$1rNdvCG>(QJ2aX7Y7io1%^RiXl*29>MfNjmJ!g(H;iwe%I8MN#06loq*EIaE?{b1l;h&VJaA*hr7tQ|+ON+X0*!ba|3z5SUhw>`my3uXE8AU*}oR z@pV2%cZw|R*=KcoFxD$Cc`S?~kvBZNqG;BEt&S+O+mea#@r+kG8RCA4b7A?))P`29 z#_&dKf^)da6k`o`WuxVDyfJ0_0s>l82pTkZXJCs1$=WZ#h7ut^aFPgLjs0XAe+mHm zkPDneUqh4^5If&i@qNKyc1V(Z+yVx#XtX*jYqn~K3TH@L1MZM{BOb%_{3=jNNk;P^ znHxr?hcOGLy&a4a*WI>Erk<(T@qvTJz85kt$pN0-0T#yJE7`1TH{yY!y@8@o`FSO| zRaj)7ITSCmuX*{|YfTXQF&$`~3&=Ht=>&IO#JQy z%^Ur8BDMmIXTZH2y3WQ*yeuo<9QciZu!b~owRf;r*>IDCb+0}s|H6J30Ao&uWVSRY zne7w+WVVb*{U;!LB0Y1fXLt!~qaj&6Z03>!zkTvc{||7Y5`_dV*kgI4HTErW ziT}F?jTPi*^~OdKX_E4rvC(pJHCnnbH|7k4BXuueql}t{jLQ$Q=}?f_K8BWyT-ekhIq9IGT`^vv#^czbVR%6Ed!3|y6O^jcfOOnGA}jt_Q? z?%RXk*}7hg_yp8%rznsx=XHXhINt?rcEkxvq(4#oyeFp@<(~wQeGWFhwq`95hOA|; z)sOSDW7B-G;*Lx(qw>Q5*?TOypGQ|qpoa1;|NHKOP zb^|)yjI0Ob7p=)2fVpHmUab!}c^nd9I$qK#Ad+Gf@Olfy=yi)dmd^@|u)GG+@=Khl z6H)%HW!LVNwH)+CTG8nSZI|oFP^0eKMvQ=R#}mn08;InTw{mBKi(H- zV1j2Q8Lo67!-Yyyudd@Lw)&lQnv{cs-MWM8Ys&Jwkal`qE)UroFpn4zvq1UJKwtg= zp8X))$fervTN;?X%8VCl%U5|?7{7SYpPvoW+tIbc1tRW!-T;KfNzlAG$z_gyfW*-Z9}C6?vr&a~AQ;;sA2rP@ z^l_Qi*@c8L@4sEfUBO}YzhXTthp~<&1UW2!YE$LUI1eJ|Z*CCqQaeIhu|A#mW=#0( z0pedyP-{wvq};#AqC_pI8+r9n{@gGBPbwc?>1YaqT93j1YfXb!g6Ag$@*YoiIu5J& z-G(kaGTNo?R_KxZmXaP_J`PxVD5>~WLeT%?H1L=AqoFuOKRN#w%tJYn5e0c9#%M6S zK9$HHr?e3y7&OXX;@OdhQGGnXR`6H;lw3j}`EuVawtCeK;iiP*A9|8? zhJG(0h>_O5vqKz|I~x>rRzh7v%RRvw`~?ON@dTH_GPu*wlSGw4WmSDE;$w)J#ccTl z@8({PVnMm@Y;l8DCFQ!+Sf;x~P#ppD@RPSX7=0z6n!|F)EfSkdi02+5(*Oeu%Tfj= zgrmWs5WqQ2F+`)G7lCuW&m6M%nH%vi^dh^$J8M4Ec_I3?Lr zuvZ?i8pf`Ol9$=owy(JzLNfFb)#iryeXP=>zQ2PI?IpRjWLxHR4nQ}0 zA9RC>b)$}vbwkvPf_qa_B7-B*x}xRhQcN^{_|DKd-UG7rcs|dX0TJ_wfv^jboxX`x z{O+M-pwdNWbX%+=;9Uka#N#z=VdziMT$m8V`w4!d$cX9u4v>+cE`Z}GjxjFKdxtK> zs0iR(R3dWMp)K^cmO&MaU)>;jP&KqA;?SP?(p^+;!}PXAz#9ajJ;)@NPXtc28_4Q%eMN7U1WH29^iguzDcG)s!4}FXv)8oay;sCqF+Q8Zr_Mrl33{!^n-_!OG1fu_gt=q6KNG30*+ zgx9UMmS;58j$lO*1g>1@hXvOW63siT={utlUgwAd9h=Xu1(X8oUr-<-$Oen$Ug8v` z>RoM^9@Ki5c~E83p?3*+S zLTTltt4jO798u0iONM*|b-QEd9BodKG@9$NagzZKWCK4`dO1+x;`wTJcn52}=>E@+ z_G>w3?>ncC@Abye$;WZU6NJrp9C%WeSFgDVq$ZhCK zb|0~xyA-({qq@rfXz1R-E?lPeDJ6d!5eSBMaM^7){$Y^PUFS_E+aJi>5BR_e(o)8} zuiLt0noN=vexIK6ov^Mq7O+y6l^?U-&^O?dItni#G_1^529g3b6fCz}Ao0=J5I{pH zU-Ol@YgFHnN-DShoVBku~Z5#eS58 z_tin%Gz}iZ^B-^-8VUx7yS`c|i$F=K2gUDM!#9CBznr8oDuEvfywnXCDn=2{vmmM_ zAl<{qh3w);S=<&!_UR`uOWO)}NyYu%whG!LGPx1~DOJH6Hf;n7s%qu|d_t7<-}vUs z{np9^Edx^`fPqJTl}^hZz?0OZSj!Ep7WHPh2yfV+V678rDdkOW1|lN`EP+&~i{*U^ zFdReA^OTj3d)9SQ!abCle;T&*yQ!FgU8>rNRH7Qln}qB( zMBk?AVyzFHoNh_LLCwjcpzGFQfmod32`C(J&eoyUkk*V$hr5&(4tHAZUjf_-;PC4X z|Bh{b8-5QpFvrrIT3$s~<1nS;P+@XJGlHfYceqy3wJf`KOT%l8^DHBJW0jZ6eHrdV4q3DkMQsGf*%ebJ1gnbuH3I9tYdsX=qR zgpy_$&jUl!Tts0qZx^9c*ad&OVZ-EnEwxmP@w+g)2YcxRO&cQGvW+QFH922PG_*BJ zSs)6Zae5h0(D@CS?Cir5Y!JQ8t>@C#*_fstqZl^;wLuCVIU@6#}Kj9269$T-%is+@eLcfjaeukmiwE;qiS3wI$z*~>ooT*en=%s1KQ5p zjo#(()>s#9;et>b@TipzZd(Qd+{?%)mJfDrhL?Go@|UnS{7OmJOO$tXR$^FCMBuf4 z<9xLWs2;Qbwcd>8t#}OC!)L0$vEle575i-qAhY-Qhyp}<*R|7n`HwNH0|k_jVKBSi zm%|~NabgcAlW*Sz#0SuXTN0^t|woM6Zo*fq^?@{?DFZ`NA6a z{t6F{C7M=HX6wC}p)$ju+r}nZA3?JV9Jk(Qjl}XEuoA#q@2x+(o`wxY6>#lB^BMm=IE=dfqgSugOn;@wtQ-H) z8B|XFBc740{ddB&F8ih8G-je0pnbX2{t!X)EJ+<%ZR=Whb2WPK>=w?-tq1%%8WebL z-H+z)d+$$M_k(2pVvIpTm5NQz+PDD*Wl#)k0w4sERfJ*5xD!%reI28_DGO?hiv~st z@{lGiENOl3U{UNbXqFtUhp=Jm#z+rDgy!Ku=6XCok^nt~K{Vx~YtRK!XGi412aVSE zl4q`b7;7F%#KlPRJdcOoOKI-_-O#q3Mfj?i%BZ?(h=+tU{%a`)Ozg# zyfNdKXLz>;%sT(kP#7mm`tu$9^^IJTGV=uh{O7U$iDN|8i?szqMva%%Y6#sxiZTLAe#^jsqgjn>ScD zN1|~b0gH$b-dLZCEusyQU07|4M1F#m471@6ly#=S>h|$i(>~l9y-AL+VGL{9Cq$d$ zdGR$Y@7gEAfWkM7?dJoB`;DCSTn$)RS6_mK0$rzCk;Kp)xCAw=8v?}*(^Oac1r*}n z>Ef728Zt{pqTn1#{ZtL)n_8jNmbhP#HWF%N;=EsIoG0(KO9omaSo}NH@85=Wc#BZK zVJ#R5XJkncn8hdLo%7G&WRW5h^sIjLO(#!_O-OW& z62dGYPqlQ?DCX?Gi|q@iktsy{coaD$XE!d6o1PVlW*_u}xOS^q$O1^hlTOYphALznA*2v2E{fH|3}J-l@Ll z|5RK413&h!(Qmx$C&k#H^~v7f@U&lntV+QkqDZwHuvPu9uRV+R z1usVuDT?sd*YNXY*u$*Vaqjrdia^H~SYunC9sngxT4Eo@^G@j;sTgL zP;i9Z|C!##ZK8T&SJ+&(4cz)=G*9mQ$Oa!j*l-S^I}!lgem@?o@OSX0b|6)wXYC7tPX?t@DD%#s@2S zQXs*LQ?_B0hR<&fbp0vm(?xhJZSM&rTCe>nJf?r`q39$(lrIiR2M$jMj&OefttfhK zQXCpymH`@;i=RO*X1Ow2(nJeFw2~v$zVNWY_I-o``?WiPpns_dP`Y;dJi6=ce{Ei% zyw`emv1o0Sc#=EC_WhXtfHe+B$aN3e7^i6pt(#ae6$oQ8j@Dqqc`z}8r$_E)^D;t6dP!~X2LnOd zT`s{0P1b2Yu4w!ejM~59V@;5_WRca3zIqyAVh^`9?cW3`(#@m03k2rs zSrL0ODy;ehrk-uhl1vhRV3LcfHC*1rB#jD)`%K!Kn^5qNis+J-5te3~+d|Uj%vQ1c zX*TNg!e4y`IaSZD+1=RO+zkF13zxmU;dP45L=lzkJ0-RtJem#EuGlYw!eIM$#%e@q zXP2u(7b0lL{gKT54%P1imWmG6TD=s5JbE{WGuac(S*wuQ+P5b*d}g#E=X=dk>a9)( zeL=nL+wG}3gUcJ#Tb<4sYoy+&Dq#R6iR}krXQEaDO)$L&(>~!6usQ~7#3tiH(6Qv7 z_`+!*yIEp1PKi`B@UI-I%W%Ff5#A+{@Z=$0XLQ%C0t z_Nxnfh*M{&`1^w>5y>fFj@6}seEJOcln~)}ED5U30BY1uwZ?0Qj_5v<3yB-raSm=h zA?8J8bpoCdIr`R+kjrhNdJU#S3B@%|id5OBF;DPIYpy%l9iJZ^kT;s#*RWJCtLv$~ zkB<5*?!YePq0_~4IC@-JgpDvlQrb6{)+>(UmjHavQM+(RbKNoNz)|VI8qZqqycSi9 zk+qS2o{Qks%7QwtJrB?QsSiNcVyZvCCAf$%DekJb+e-HiJh6}DOi>~83_eqEx^|{G z97JiP;Y?9oOWnt*D5Rn`tFx4f9#X(SaMb0|Ddro5PuO5rJjNbo^X>wyn^I9phQ?jCD& zG)qkv5r(!<-36Fb)C|0UaRvd+RDX%*=txV=V!1m#57z8wu>Ad4o^HfAifL}tzBz0J zE~^h(({%o>J_(`pr#1+{oo!O7>1<>3F$v9{iBScKcFE~Q&B=w2?w7041CFi z_hrx$B|I#uzKZ5PDlnKh<^E;PSkssAh^QSLF&uc-DpeWQ%`Wizn4&Y^A)_; z(a;3Md13z6VC8-jGE)WwzI=be6IJ|8?1bs|&72O~ebdua-D~qogMd`{uHKBEW&o+@ zXrq9MKU$4-1veJ?SYO@8d(#4*(UT8`?@b8OpGJsI#Zfg1#gmvmseRwG5&d&#)gyra z--$rzHxFUvhiEpDEruAOCng+SC5uOzmOqM>UkA)CSa0@EU5Ue^tS6${8v0pQZEUAgu;LYM~Cdl26(j5bF^pR z;U^wx?7HOH*#PLFv@pm``Yhm=5fTLiEP~DTIV^Sg3(W8`Le?iDsZmC;dx?)4C6fzy zZZW)a{e5X^^xSmd_*z<o&im1J1ty%5ihrBVkZEmkT;U(6@9 zN9Rel@}O#u&f$O@SbK2VrJB0sb`F;=#90Ya&q339a<9qkb5!dW$77f{;#*?Kw{xU5 zOXesPbBp9CO!smW_j@h|I5IFxb!Z3!vJ^E$8;nxwdPCV+ZH>EKOq?&t;`~R~c)Qr= zdq^buH`%a7nn*gUBvqSI*(W+M*jZ_f#2C>!SCu5gpYkx7O7OT0KTBw}V+EKV2oVC9c zkb|uq(-eZeY_J}MK=PYPoz9D)mS!Vjh!*3KvS>u7*`k9pqEi8hE9zz=!nC`cPF(X; z84+8SMI#1DY8*+yo-~uJKf}P|YjGdNJ7)+pcJ?^iKTn(?oE$o*8(_7`np}URs%~_g zCL)Dr)%Xm@z%FwYzq_XG(sBI~8zOR%+$-L!{(bFHJP z?o80=9D%`_aoBT(g1WjPh?^F%8IU?Cu0eN?HO+?uEZ5=S2Ee2>JBw7nI2*Q3^?7f| z6m+8@k2TV&GJy8OD3n~yc3vBaffBeGJ2SGjz11;~ccyG&$zq)Qg<_nGI#<}r&J+a} zY=?ZJej!X6Lo3Ww`+L(B%~S9CnAG=sVmp%tm3osE|)vmv+#Z^2Tj{0C|3P;_@By-6-@feN#+*z%F~Q zEhqy&O4F$BWI^(B?#k{fLidl^U1jZ(r)viN>ZL)-m)WY$B|tFXrkHdfy!WWHZgm5i zYZ6y^mkl12t90H0NJRS1JFRJS6~d(9KE9l0a>a62qa@x*YkHqeGp$zFH0?v<04oY+ zaFNblQ5jl zZPqO1!<`ReW#q$H)VT%CZHd>whda1MAmY@Ag(x~u%R(28@j4&k~w-`N8EN zj2HQxyX$IF08m^MP+b}fmYsBWD)eu#`-iQme#V z{U$14f@4Lm+&&wa!A6|n+i|_0qa}P-bP#<;F=`}XP5Z}ik zqdTTubgyqD$^SK{bre1YeNm?Sao*g9t8!JO!Hi`|^_Pd8{vT9l$kNvqG+oQ z#bD>hz2$KRhLsNUmkM!8BV)NuDOU0?X7Y|$FG2ZFQiQs7cp25q0Q<|ZsF7O$4IdIB zyWkTIfZO3itm$Any#*XTMBA~YXM$W6%LqZ8U+U8KWf&#FvM_$0*62sW{0G65JY-f) z1hM|bv?N7&I`kk#xg+8ySOfo&6o=l6N}?sfvcM+z;iC+52b&K6;XrwI_zHyh9ee}% zOrM-i}2M;cP}a-TL6u7h0M_lts|L_se~4iuCl6i&{oRr2UWf}KO8 z>HI3qkL!JY#9QFs`P&qjjL1=T^d{u8_zvf$!j2; zI5=24hHGg+KxH5g=<+FwImzK;7$hIm;bR!r9z1*up8>>8=XAm_6{N9`Gi{{}nwU3P z&bX}7Xs3|K@CF~{T&8KT)8P%I%bNCQ0j^hw5Jl(T(dTsjy_>uBKir| z;7+*d&S98$REsKR-j?!y%jF}g8-tzbO%<}(@TGlOEU1@Ql+XeK#Dn26YnDoA!Uw-G)enmOQNAi;E+@rEz