From 11a2b3016f2f8d45e8fedaf695940ac9e347d566 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 10 Feb 2014 14:05:51 -0800 Subject: [PATCH] fix(builtin/num): remove hacks for making the elaborator happy Signed-off-by: Leonardo de Moura --- src/builtin/num.lean | 4 ++-- src/builtin/obj/num.olean | Bin 48291 -> 48352 bytes 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/src/builtin/num.lean b/src/builtin/num.lean index 3c4bc8e5b..958986543 100644 --- a/src/builtin/num.lean +++ b/src/builtin/num.lean @@ -296,7 +296,7 @@ theorem disj_to_lt_succ {m n : num} : m = n ∨ m < n → m < succ n have H1 : n < succ n, from n_lt_succ_n n, show m < succ n, - from substp (λ x, x < succ n) H1 (symm Hl)) -- TODO, improve elaborator to catch this case + from subst H1 (symm Hl)) (λ Hr : m < n, lt_to_lt_succ Hr) theorem lt_succ_ne_to_lt {m n : num} : m < succ n → m ≠ n → m < n @@ -480,7 +480,7 @@ theorem prim_rec_thm {A : (Type U)} (x : A) (f : A → num → A) have Heq2 : simp_rec (λ n, x) faux (succ m) = faux (simp_rec (λ n, x) faux m), from and_elimr (simp_rec_thm (λ n, x) faux) m, calc prim_rec x f (succ m) = prim_rec_fun x f (succ m) (pre (succ m)) : refl _ - ... = prim_rec_fun x f (succ m) m : congr2 (prim_rec_fun x f (succ m)) Heq1 + ... = prim_rec_fun x f (succ m) m : { Heq1 } ... = simp_rec (λ n, x) faux (succ m) m : refl _ ... = faux (simp_rec (λ n, x) faux m) m : congr1 Heq2 m ... = f (prim_rec x f m) m : refl _, diff --git a/src/builtin/obj/num.olean b/src/builtin/obj/num.olean index 7c21f7b23a72a52ca6d506c3e91916bfbf2838f0..9e3e828c5c4572b200003b59149d0b2666a71bae 100644 GIT binary patch literal 48352 zcmb7t3z%M2dG6l(|L4CVhBPV{L0W`_M34lqirNV01fr%8Zqk4<8IlPM$;^bA3AZ9d zZ50V}tOW1^7E>%F0l9cPK5{@oMe7Ybjn$qLdU|{+p%;6qg+?3e`QG49x{(dTnfuE}MmLU6Ol9kbC&q?1WbW$Bp{cSux#^Or zYc>vNQ)e7H`Ww=WetVRZ!oB|imO#ICdS66IM?tMY|8SZFgph{Q6oi#5n~jS zs|f=KXaj}lMQyGzCEju6dR~rNvsqk)|3ScV)m~=6UV0|Zsflqy2;bbb!|Sp-8_s1} zx9NvBilGb_VeIhL@o)}00ApT);(&nYLR@D#DStJql8MQzPblaH!+!Ac!NO8LW7!CqxTO*MYp z0;+IuNR}to7x;m5QKP*TL1$+Mf@;NS&87si<;390-Tz+|U1%bCo6uVvF2a4^T+V56LE*u%TRFqT#`aN65n&s73goib#x!iGs+;oB2w%Sda?^hj>S)7q*r-pij1ULI+n3ECd0Xaq9nsaAWDPrW5wy@S#f@5 zv9er?fL5+^j;EcmPm z*ABaoz2%r%9i49y2bLr$;-yCDu+12F#HY_K_0e9q5;;IWuHR9X`8(?+M;4o7(#cprBz%~ zR$|ZGq6kIuTo~I9I0X!PCSl*D-;3lHy(zsSmGAQ$oI97By14r zwuO=6&AcuL&Y0P)xO@b~HW7P1>e*6?=kut}MbYdQCe%S&ZnQdUa(YKHEnVc{qbb5y zVrcdy6c3|lc2Ta1P>_AO*8E^2RfGorlQzmAft;a;q67`d7#*CrszN_VY1XX+6@k+mYt7}nGjY6K>%o(t?rAXyknPL zFEJ1oyh{IdD;7rVDBCEvgJ=zu`5soU1kCfSUWMvEHeCp~saqJoJ}AE$odYP`@{`6z zbP>%~8+f5ad4^dT68I?0pG$R;fL$2!zfjDvA?Iqy3O{4BI9plUa?{>MQy#Yn%4fD$ z%{~{Xw!RwM2NL>AYU350kanQFYcIfliNa#Q@{JaKh`5!aKZk@MSDkurU*GH*tftM@`KU5Uo%!p_a|j;7C@2095wdy}Jo7M7VZ2d5*%a5V1CKY#RDO&fH1R_Wh0#<-UFtR@Kb&(X z!KpS|YXN_AOr~Au%#510Yz<#w=EIX4V9(!?;A5QZnHcD9N3lhq#D9kJ@Uz@5@|+BT zFf$jNniv{`0_|^^{mVx*3pzFpvpL6JCSPAJ=!jJI2jFZO1ezm5%~yx&de~j|eH6AL zDNGC8TJqH>u%_kjAa{c!Ywg1RC`Yi9UuI`O;}e6RKEo{b<4F25GgOWF9HaE(UNI5$m6?m27Y5PGvS^0Ib_uf5#Y&hoW$^02M4 z%+7lha46p(nZb2}PWO~s**$EtV}cQk!dAo`w8*c}c9B5HJSkUpe_&{sd*=Am5K|}v z&xSs|^p!=NF^7{yj%}f5^eDskK3G{wkJDFK6zblo^K1wB$4MVON z@iMmxGzSD<;?kvln#$sSRj_v_5i@G*1Z02>P*c7@lcK6UfH2|uaTH(S^(#<)48>Qi zaJxu03J5(BQ-Ue(_U-5CHL9GQbEmOaq51@ZR!2nAKxDO!HGBi2r zOp$ERL#D(Xu>7K1tQ@uc6)2#+d;tXsZu13boZCgYDi6eBQbTbF%eSx5Vz8T;$@EelnAZx6cval4tF+J9NsO)R-8u;B9YN}cIlJ@OuOK& zS=|(9-7WhH%u;d!^P|XmGc~#&d86YAq_aH9GT_@qMrZ`PO!L}X*mCGn9GfG*z}k6! znd8b_!mW+w8_ewTPjrjP5!-_dUd!S6^`Ol5LDpy~i#3u7pQ^}EIdRThduc3F28%h^ zyYpDX<)*}-d@2y^Wl=1_jND-hqwLG*b`&im!B`&E!#V=eY=b5A9W8-GIAqnx;+w12-;MF0~?4Uyb9%$wA|DdW|zBqlp zUDD+P5ycq*>2dk;$eBT`ba_DaI{VqF%1KPR4R9wP7*5|l%XYcdHgWbO%_IMWCG?g* zYikjy4=A+dg3;wIs8fN3E~I@)c@S8fW2Yo`S2;c7T#D^QhggwIQVzv=sF~TV9FbzR zOPvD^YL^Pt=kowHhZ0t3LgVXEEHI;+yk=B^S#|P< z^5)jE8140eVw40UCKsdT4rfo6=l_vEa7@O4W>#|!_$sF85-XD_&i3pV=dlVi!6BZ- zFcc7n5oT>yapbcAqJ}76TRw1oFd(2NDl?xKsfkDr1Q3*!?eofaplA#-zdD(uI1k)Y z{LW5rxzBkzC3CMe6gZJA&L)R&dUtKLywd5*b?bS+_GX86PkZLY9z#y|Gs~6f`T2l# z$@6nYo^r7-Dm|Zj@tHgy6TQ7>fw$P#tL$KA***%2D*r^O@=pY5^4!Sf1oRG?G4)iD z78Yl+W7v za=N-ds1+INbP1vov1Dz{U+ULZ)3Iq9PYzUV1crd8IGy72>z|9-AXu@5K|X&OV5e8L zxBu(`0RCqbE{&21A6XP~_mvucEYYwFRJ~5AF?%WLD6NB27Hpi0%&S-h`ryP`Dr6we zQ}W-k=2)wiH9&sM^QISJ_LOH|32}Y|@Jn#7QWbaeP|Ke37HqHzTKRqAFPIAh@6ulW zoGC{91$Z{nu*50oDGtSS<=I|-IGUm$(35sW2R8vJ^ElZoX|A?e>@Jur7mxH??6b63 zI*UtMWwE8aL8rg#1w`x7a8zu+yvJusSUWO_o3L8{?Bv5aM@7Q2lPus|j>hOzLPbj@ z$D+&I@^ka;DoR*DVX+4w`(?!ztE7FFP+UPvv~1O?kExGUPge1m7qT;SJMtSAXT@W- z6vl(4y0_}joj}2>0^-k>2+Hzc#KV<_%>7ljPVc^3GUY$8DFEc00dCJ>` z0Rx1Vw}=*p3dOI;H&ABMxMdlJfSG~T)oTg-ie5^XVR8v9evPqnLvo^1_&JmuQhm9D z(TnJoVjA3!0L*PIZpE=(Vg~0X{#-EPjb|B7A zwZg^n(^M^%w^(~D!g6<0KrtPmYXkw7ZCF?B51sgUZcrY!&OU1d?(k2X>HsH8ERdo$sQU z$PUjf^RoeRBh3Wcj~Z`i>&1RygiKuYB}>|t5g}LGrO^TxAGiTmHrI>7 z9fvZCgd2qUv*of1o2+Dd-6pWDwBKmV}XAV}aJQ8J!quSA2h5@^EyY7;ySm8&yo%gqG^h`A-V7urP? zx6^P6pn%NdLkSN&vH2A=8U!-or+_+H4mb`=KW+U-tZ z@@1BWu2p%UXm6kh8I%J96bOtj?e&JY*t6+;h&vVpQ>=*A?H;-70kQ;luZ&@BS?x|O zU#NZx4dn^7tg>Y-`D(O_F)y0WhUu`1$#Wy?0)N>p_OFK9d9}|6ej^~jkftVT-mNaP ziz>GozIwmB%0}022FCo|RycFjkuY0t0D$7yW&reWdV)vVVRLB`qt^2%W1~b;4vBI9Bui?KRq3F5$k}+y+ zBfamjzS_1RBu>m8+6T41D_8}NUut~(Z7Ca-4MR3=<)dAY>wPrB_gk0U4hO&otcZA| zz2~QcM>)=QR&z-LYUa;ck8D4vn<%xXKxYQ7YM=EQp2ehjXey5PcZ^QcLp-r@WjuKv zred2ckg(nB#L^;r*$K3n0|X_)3|#i-xy*kKD0@0^ojooZU@45+ZuBuKWtLxMwO>$f ze}Gnra8*z?bmUGmA%5ofPMV-DlQeCf#Xa*7<1*{dbyq1^upOyW?|*{PbgtUZtmd{8 zG=DM#6VMwPB)YiEF7va{2({fTy+w10^Z(AM>M~R~T1sKoH?N+YQ$IgG@uX z$XgWA9afbk%(EJ)$acf_+-Pbz<9P-iJs!TI=V9s}(n>#M;9*_R*1CyAaowPMcG&tU z_*f=1OoTZ0?GT{P{0keGJovldQhu|kjH2e;sLeX(~7U1L!FL=-1`yQtM^4z~p) z=toScpA7owWwkos=^_rZxBHr22?~C4wn6f)3~A&BESiqKL>xLM0(AWZPmR_?E{a$l z76Wf2xc53yBpjRwhVMiJPtl-7-n$%<-fM-a z(%WoQ{?T46^+hlfh^mhH^Ysw0Bg(VK=Mw90^s1*w*wkL!uV-AfvEEhh(J4zC^Vu?L0g*aSSt+Ea~Q z5KUn~ih&8r88iy_t)JYhQHO)PNTUEctygXJcl2KO1Wmx7fr8P2;eEM6kf3HoDJ-PvXR-F6VVVk*<(96ddQxSr3`VG-h=+eIm_U4?7J z4BhL}ZFAhTch~6F8(hy)!uO&9>8cKYxjD2mXh_)JmIxr2wBRmVhioDOgY69lK%ZC= zny~vW!0fYB&(7MC+x?ifc$XM~6huhD5ujn>D*w6|Vg(-}CmTwd6$jDOH=GtH-Q>F#sSwW$CPNo;AoVwnn3@Q9l0XRv{(zt;7#+7mdWsAgk+p z(DUb*E;KqE(a4td=ZO3obO)FS@b!CouX{oUha&RVZw*-PfHrCNm_N$2>bC-wJc3dX0qrp>DpsIc|9DU*-+NJm@}|9HR^tHssD~|9;QFz& zKS&*7k;Lu<tnbgY8z@gP zea5%OroPPJ^(adHRxl|mVr*lz7>zIhIW_PttJMD@A?s`C=Ic&U3u*OSWK*7Maq&NZ z<8e=Q{SHrG{WG8>qDT7?sx)gRvp$AdlT(|5xxAv@VVHqWrPY5r->Nm7#woV32d*Qt zAg37)ZR$TovB!$?Fb!HW)wJK;=OL%2?IxGH2k<$7OLm_}RkHhn z)tv0Uh*sU_`R}3nC05}wJrBV0rKmtKw3FE_2)i8=8Yx}9pMmut&pnyias^hVIDFdf zpfKH$dNjHZSxF*@szqDLxq;wNVgS0x=j-$=d&PX z!tP>lte?OvY%4lOtkpe{497Yw0VSf8s){D91PZF+LXa>TMA`dcgZwZ*b(mFSVc?Np zCEd;*z>{z*4pRY^Uwbp0fj3N`jAsVkqLYTwo;1RHkff;6|vmxJ2_;0R@NYBhPs0 z;e?B0rQ9g$=l~XC9k@F%-Ye#aak=7V11IqV+fc(+K0eb94D+i4qJXPXU`U#aC`|h8 zKpMMROUVrRhN+%auSvhyj$XbPtOJWCuhCUwR0UNVrh3*u+6<*Ekp7h~3%N+VcKZpr z4(B|Ail0LWxg6LScnG9Wk5TxY2DOJ*MmCc*c`Ax=Zgto0eVOd(@Lmd~%@*iQC^Y&O@*RPf@1RB9#nb-~-=^Xyi!mSP7vVLuv-T%fP$Y zzzH+(J*(L_H*kHhZ$!u%_$CegciHGYO)rT=x(Jz!yZHxq(QQ4LX#MzPzVBLNv=~tVR)T7z;e4 zA-o>=6)__XQU5N=|NH)WkJSc#g-hM>6=awWVj1{VBD?j37vXT>%zd)rZ8}T^@dLl{ zpH(98LMwR#Ph`+GB5kZD5HLoKn#S4&erZLcMyj|nfU4|vuoi)@POf{tZDF9iNu}v; z$K`4i>*3iEk_o%aA|XLOk|bhNqo6ohkcO@HOp`q$ID9pY*&yMdk@l9^<$y*;J(#op zaw~LNUq2gF;)4%0C{iv76aL)-SX}Sh&J@4Y1$+bW5!tD7oM&;371Td*PGEZl#5{o(q!vWRvT;wN$GM!4B6;yIFY9GA!t#@j%qO6&vw zfo_pN^)2poYo2tAVi7Zo&x%2?5&S2@5h&ulO!1QX?Df4q+jDyXbhkk zMwO#BUJJ&Tn~a$5U^SOchcfr&8rt0Fv^fxVc1UlytzX zv->@fidn^YA>GRPf6D6!3fC|(m*hq8=n2Q=njaFj2x3RR_E6>I$k?SDhNtX1PW%Ib z`Xp8QF_`?X(>L&T`zXWLm#}pDofuAMN#GlRkXY$PS~(E_$~zDt2vIdUnS7oA=H&Rl z@dp--$~&irs0SsYabGy1pYEiEo|i~Ss<$zX)q0!{x7*6B04mQILG2m2>R2`hAlyA@ zW4Z;TXWIhFl4=QZ{{oN4BPCYkCqUIVJqz_}i6uknLvT;ZUD z3w;AAXd@f|s4?7&(Dfn$SrKOg%j`OfLIRY#!uNE$>U`+v7Uk48h} zDqf=Okck3>b_?C-*9MM2UBe-Y!eKI$8&m{>|6In%yA_T1P_vscnzMa?*O8{xYTb?Z z1i~nn5BAd001_5X)09Oew?#ZAOHYE`*!WD|iL=Lj5>D0L4SKfoRW~($dFSK&{ys+_J>lXOy0shA*HYW@vYYN9S__|ZDY%V0i zriCPsN%6h6SJ1LIDx41%Mk`n%KKG8dw=&sQBp-;+`Gi#l{sWf^V6a|gfeba3YuO(e zOydR=m1~*0Vc7YSp~<-bT_aZNYY-jTCzCXf}4_dtn_bIWTj ze|#oecZpz-K^0l_I{_OfMn?Ib)&9M5RD)U8CMow9fm8>K|AwlPZ>Ic@gC6c`Ywz_z z2{23jgW91Tytt1W^IH_kZON>^qx^z_^loxR_VlN)jmK?>&5nUIJyH4_yB4JdYK_PJ zE?F-OVWQ}WGHkdTUn@7U7 zVdIB@=2{-c@onmir&*Q#k|)ZdhT#-PQAd@ED+a9Ac-)@UwWprYnl-*@>wW*xY9)3O zj7O$=Z>iNL5CmliaI_i@D`dwQQTrC`gip6O{;p-U{JXdg$0xPB!uY$ar}l01Q%*WQ z(dpd>(UtUDc4)0RC#*$thd9Bb7jZ+U3Ig3V--e3n1S|Pup)bO48N%qs&oHL(v=v#3 z4Q&|H_~&SHT+cja01nppf5Fu`&%Y3d4=@DEc2T=&fZ;1+B8kg*pbOLtycj61=%$t$ zKc^7?S~qGp+bA;U7zrzDIK@iUfSIHK<$vKVCCT_e^ zM^n2&I1lW5?`YPx1@qb#$0@E4@-Q7Dha>yiHlX61G#FZ7bl}~CvlkSyXf`YDoL_^M z#o3D_E_pX_o(s#MWbl!sw*%dQ0HR{~_+#TA?6Qxv#V6$H^496mGtzLK z)K`_OkSL5rcUUk-^X0HJ#~ZFa$;vf=xOs3yq8}sEP3g35&eJ?>|HojZ<+8#lo39K$ zMGB7~rh|bQD`oR=)G8Nkoi&rNS4YaRT3hWf?tJm z`dY8H-OU&%zWE9ar$I*dsfg~-F1n^U$*%M@m}oZDvZCPF5Q=q@%|XFxoMm!p3*j{F zCvD+4yLqCaZ@wNgg%z({=?g5&RjaG}df%xSh8MxFW~F@OimQF&N0_M~QY~-41t2YN z^Q_ijUZVBpN4Vb2MS^qotif)nFAg%GDq`GuGeaYy{tj~WkGhbPLJTt%0 z*Vg#j3%>U2=!JbdTEPU3cKP*vJ2$ulEjs)cb?`3y;)|3Qjw#T*14Xmaat(Yz3s&F~F`(M=oBvL7O~4=tx6 zO$edl6X`CbbWf*rj}FqcX=jt}CQ^!m(q;Nl;NVe;Xj1W%?d+5-^@7L5`zv@-Ai;}M zmZ6oZ=Sf^~0_j3Sv6xl3TXQ|DD8NFKJGk`gm&K9Efno7GX~Uwl;kE9&v&EsMn-oWf zCrAJd%f&Y>X0lw0l|0CT5HjURJx^qU@*B~m1Jd|pCFq~HRB)YR&WdQzyxEF;H45G_ zntrd}gf0hujp5NwdXHVPhaw#K4<=j1kpOabVU>J>Z2Sotag>Pvn>T{Go?8eBxeNw7 z5^`^gyboxoeiZ4MP&0)TI)iN9PMl$dO%64h`T+=ksF9I|l;^FO9XQh)3(c)`^(YEZ z?j&>vU+OA;2V*53-sp~SL�OgUSI|@fE^$Ksq{}5YH4JO_oj;ZqLHL;6jmo%^bTZ z8EB|^DLv$Mn3VVO3T-FgEIl?CDZwjEnVfq<#kVRQlogZWYWpM!x(6Exj*RkTDBL<~ zei4M;4vJ*3ms^!5!Ron#-3zUZ4%Si)e-1z&L-7SGsuc_vr(h_wc?+*$I;pxok2a|* zK;pW&4aGeb#{bClvM5dhI&C>3Sul8~-te_Z5vkR20IB$f;p-Dt|4`5h(B?N$JT;35 zzX}e*!Kns4$>E8N_Mq{r?6IQHUA~$SF8)dQH)%$9+9=nUV5YNt2be*3beA;M&=Ud1 zqf{Qm?3->S-oJq$uST z9=f#95LDH-uyw!IoaRpfOCJtC(Q2bn`{3A^JzX+Crb`;N%ix>qAk5(Tt(Pa}v5r81 z3Gd@;?~tr6t$CO!Qa47nUS@^nh=LPLzBP|MRycKs#AFMMjU+bt;(@45QwF$UNErnF zGi$T=K2iJ=3Wkj+I8pvtPeRtxK}5C0V5}0UXka#?D%Y9lya&G3njZGTq) z-Yxb{-&)Y)^c#lPO-;8TRXIN9?s{=4P(MT$|1Z|%T>QU=Dr_X%a%`;#6QMn$hx`9j2 zHb#5g5Mf)x-ZSGTAUO)2*&60}D-`ya)N{we2&;)fPaYmyEDtjxqw?!#rFBudVPR_C zfH}4MUxBI?$lqrbfo;Z38D!-)WvK+Y+L8km=$}UGQh16Wl77(EGQ-mPW1w1%Vzy=S zy#_RZ0N45>EBb`K2R(o(jTqPO#C5a_qJdzzJA)uGRe`tlJ`BGc{n7eM#iECEG%tn; zXb#U{3)rd-Fj||ZmzvwdrBc%#4%0;}P-M-3r|AWYvXN<__zDFhH6Hg>GFK8Bvw zrJ;w)3x5AeiLdN$QCXxRa_s=beqp|wm@3WSE{KF8ZQY)*L;QDvCe)f2C*<&*c#XWx z`n9YAQZc@DmepFmr#Ok+u@OM-8^M9QyFGVN{wnf;r1dc!QJ-e@NOG;)5~}W(imQ-u zgG-8}xkzgFNAST$9>ly4CsLt@?L^NbDEOi7CUOyno|v#jmp~q@8vc;=(gL&Xu=Caf zCAh!(=JUbh}B$O5!tEKfFPhJ*&d?Rv}DBN+8>7BD9QVwXAmGcmECfBjRq2GBMX_oU7c-C|6W05}6T8_px>4CkV; za>vnrDdDGA8-?IJBA6P~*2Z1(d^L($b{uU4iArZ+52vu(KnB!;ID-FG*;xCfGZ2fA z=L{_&7GJKaw6QjO_Q%HBhXO~Hjj^ZF#@dI<##mA}kOfI}bfQP*rk+4I%&mO{=KO*c zsUfzH5N33FoXsyJZW1;t?ZXYQ#V19g@Q!tiJ=%c#)7^q^>ool$O&v8K#bl7Nv&%GU zpOrS8(_^{&cU*l#kQL*(j;r5+skN86fYq7yG6vAPK0%}X3mSXk6F}dGVmJt%*8O@w zu0}E2rUb*aDH*m}^`-w7}>Thf3K?Fzj8F)L`F zW|Yjz9OnzEJqNWR%l2uQIWna^cGda_d#vb7?a|YEvg~esEzr%d`Xto_V%w)$;V2|f zWrV#A5@a6KJ~bhPx!G+cCgn=BB&ID)xZE7QG>EO!G4M1{6TDK?yqya1=U?q`5@f$Y zGBq)B$)>5{C^GwPd)4U|xurfJ%kmaYZ>zH7>lwjuy5r3MqELM&t222*zz8(0Hm@n= zlkK{_7zn00_9k_^tiPnrsyxwXogd^zSGm-B_RCe;a1gpmd!5xPU4<~|k`SM?Gc01b zOLG=lHQJlfnntXxbvcUjt>~MF79wZ0URlu_gG*9Wu)0dWTmu>Q#E>9lxMb_-AY_WR zNlDUMlQZx3rWw4Ijw=Lmi!cr1Jx?*)*MOE;0#thfBO@Qip!O7sYZBMlgT@K=Sdsd$ z5JlT_Stxkm5q~M8^Hzon55DBCrMFP!19=K=VE{p+=*doHFyk6Y~C{l}*g_*8ILAh2ARRF~kH0@hb z%MBrozv?cY5T)CbC~mIePNCSk1-&wn_@t+qgvn@b?p2clfTRKHv!%V#V6g0)oeKRB z=)xmpt*1HW0bDbFlddZ&f>hM=uwhPwUPXhKYNLs`t~ z;tzwq;Nl$FeuTpltJ!0X?T6W8g>&)LvB;?IA2N8&a{q8s-~(nsX5DRhni{vUyR1i9 z=9f{6Uro2m_9K)q{RohbcOp)y0}usRy~R4;x|Oe{=W*z1(!||HnxKT$olhO)!cdww z&>R1WRgf0USeDd#C$!DOo$6Jg`Ewf{-3e{WDL0{2(I$wGX7K&U41!dmrQo|Zk|x)F z#%i+~2akJ#ad1%kd%*DwW=?XrHlB_lOke!hxe*D6fAjGd;fP{g0Ma8ij08GJNfil9 zP2JvPl~2+{e_6ykZ%<8w04O9L_XgO z^5Iu|v*K|KeZ-Bz|MY`4 zup8-3tE0Cgw>qx1ez!UfhbnXR{a76-8={1L=$1ESp$wQt!yN}3D}rS}KsoLrmfps6 z^U*odfc9(i(K*5(x%ue43Wyn!qF}Sf+6dz|AH9am9=CQ>^k_Z5l0B)NLL!~RX{QuU zIx+mdgVPx;TAKi=g@{tXYSjKJiYJnZ!G;@%o`@INs@wX6d4a9{q!k^Av}$kD;jNk( z6@zU9UBxYEFNzu|w^MF7iBQ+(#+KO1ugBB?)?jONl?l?1Os;k2-YtN!a#t zAcTUT!6zZL^SYi08XhLvzsD6Z&2I(zKz~aoG&pi_q4V-kUC-*VR<=N*0A_ev=>~&o ze}$@A19&aB6jR?@CTr5g;WE#f{i3UN&UhH*_|5MFH~elpA5?C&5pVP=sg7I6L58Xu zRn<+Q{JvxCvgdIUp`v)aOT^D{Cd)!Tm<}L-OUW=7G^jwW6oG*S`_0-}R`kaS7#Vr# zTmZRpR30iiaQU!v);wyBr!Iy~A9> zcO^O>w9C#%$k&}#b*K}dn*j7755$jA$SVAsp9rz>uNj-+Z?Ip3p6U5x*uMC;vCW69 z;KsCe7HuE)SK-?0y5DxsRC(9+Wo|42oxUzvhWiWH2#i68)?yCYX1sIPWy2~5`Pc2b1S;S zH__cS;hm*gou7lq4q|Khk|;Q><V~>I_LPL#8nN#xh zUZCt{YuJ8>scIqN`I4jV5F2LXm%)S7y_9X3T|P~d*@;HJPF~!|evnhZZ7S~N!Vc}P zHcScZ&m4@coP)FJHXDxyWxKLKnUZ1dJgE!c9&C;+>rSJe7+MAF$*TY@O!_OQmy7UIsLO zA4#13Wii`r?9TI)t#suvM>z=??>t|k>q|D#<2*c&M9zpPBg@g;`QIUw;F|FRA7ttIhBS4_j~f+70!r7Y zHRq$Op_s*_8J>0maNqu#s6IWcF&MbqJB<;&1}$CtiOA(^@FS>p(cwKr@BJ&d)octI z#3dP1!?0uEXA?RfOcoou)?VPXFE_7^+Y7q*SeZuhI-Hhd zd%GC53ew7UQy0(nYJ?v~%3J8?XHV)MwpwUZ3c?SxZ(QR-ngMkFufrSLEe76ZMfE2H z^aZA!)~ye3hbY!P)*3s{MY{9CrrtVx&<{1nKY~k{EUMHXU7i~2iHC-uy9kB8x#`1S z_xN6sbYBA?6n#dTLLNtSDAJczl84{Aizq1{C`CgQ%D|(e&T46()bOwn$}u87B#mCV z(aO3fLaxz7fTTqAoFj2M_rP!-$LTtH(~sy+Ooh!w67JBA9*t3B#iZRg01{%A%W)=o zLcl>&b_xJF!IZnNNkS70BA%Ge%h|QgmO04>46ZLHSu#ydLM=_7Dj2HHkF4N2pWnyq zwtK&8np6Au2kRnPXvAeF~*-@@NH=x}_QxEMh3&&Sm89}{+k z2=1sTeF!Du3 zh1*s=ga+~VaHvANt`+;=?kbo>mlh@Sh9kJ}Nils2*Kz7-mtC~UyCjK{^ariEZ|gBJ zG&WhG6n{(EpN#klo%3GIL6cKX{&`%BpD%>!7ga?9Wq;;1?kl+Yee=-(#o3@4lYd&* zP5@%I?#)srwBY8aVC-`^_M@u!Gjz*U?cN$sVqL|f1c=-WtS}79k~s|%GA8|MoT3i6 zx{(&gbYVY0N_3cy)$T{l`G#z%tegPrFyHad7a&50n>^h+Jr!EWk#$Z7g2t&n9dK;DQjF>{YT@Dz)lUthIyS>Q! zJ}E)`T53O?=roM#(!HspM+h`(Q)?Fz9!Kr|Dfpo!cGLGqa0uST@h?J|(EM4?}gGZ?-Cpr+YVQdV(%Y zg@hzuFw;~3Kq!jdYmAUGp=oM`$7-Qpl*#y`xbbdDF%STLwf~%5^eis+5a{^WrFKxf zcGH@v5&N)wt5}H<*&dwEw94-@Vp;LuXmx8$ZP>u_M*)11Ym&z-2W!QX=-9*R*R0lk z(J$HELbKYFr~LiGYyhCkEAeO7VKMDHvDc7;Du?K|T5U_T#&WC_qL_!duJfP5wROR= z0{biGVWQ$hD{6m@HQKK=?;w|wULkpHjop*G9)3uri$gVpYeOyGZOL-eO%(@OBD&u|x zDJCiSF@}hkzqVTOmmo%~n0|!y6>MO1L27;gWn||GRRXM?MphsVeBO?6lFPZoSmPts z#Y&R-QUD<|F|=g+IL(1}dBCA4IBoGSyf!`9PnfW}z)Jn#0)|Rx@fRwAg};6zsqx4y zoY7M`8f2neJ~o_@6zpwcQsB&r%I+8ImZKpWEM-XZqPSO{)1@bioK<7F$0_dY&!}+5`_8mY7*>|l*Ejt@WkN52->_Q)oF2*)V SFE;{U%d)Yxr;ltH&i+4UfVces literal 48291 zcmb7t3z%L-dH*@*`}Vt13~MYPQ01BsiJE{nw2hZ0M2!$GiimczNj9(~*@WE<1f&|V z$|V(0BZw3csDB`VrXX$QUxkPl6cqYzjV(_BZMB-xKBd;8u}$^={(iqXGxN=Nb~nxQ zFwB{G=bd-n`^=f|?1ptC!((ek*NtTEUp~5iE@C{jpht*j&r&f$?9-Ww+7#dkOx<1QV z#W1JKQRdBJ4WH`A)QVw%AB$lZjI5d*y~xoezye^_IksVJXkycN1q1+^C<>rhGdeap zd5N`@6EusZqZ8=Px^qz0P}uwigG#H|tcopSY{Mky8o7{7S$;HT=YS?^q^K}rjAE{8 z+`s|aKp}cj8?;4f?RauMzlmD2SzL_&gMg)~y~uz)_l%vB;~NMee1oe;)?{@yoXN6o z(~oS_f-*dWu_K$~;T&`T#{33~0|KJ=;5o}l`7x}DC&sfrrl9*kLcV~IM-!B55z_~u z6X-IXaKafnvyv;vM~qv?5!ow=xs8Xwy*XH+G-qrcYuTqrrCisr$BnPuh z1Vx2-H4vZVah^FeHZt@cQ`b?n8=Fioyh5O59$9dxmVYE+BE`b<%Tc_ZU@tMIrV^h& zmm(Y*mgZ^cbN#?U)TnPoklCq$pjz?f4I7Ms)OpTqO1vC{vL!IGqfuk$$$0b%?)w%I zfMBy&9*>4WR@pbpGvid_ghYNEV6u~&QZ8w6|D}f=cC~GL6Sl}(z<7%E70G3>-vpo$*|fyk3>GPet6xwk%>u@ zUZhq4J*9Nw%Ob%JqbEC?rtE2Pn!z+z@{Ks);psI0iV+>^%h7D~TA6d;OdiU!B(uqy0R+#|C*tr$u zRx*fiTPgKVqE!=+`Q~6X{rHF^>pB6(vD-YOfL(L@DTsoU-bmngVc6Dgaq7^R1wuTq z^V8)d%ZI9_=@v_eCeGh*aXG{hhT%7$2>h@hi3Vt2mfebi(>8l)w4h>K7)E!twNbc-=Pc)RZg3*`aswl$1gxX=a2$o3UTl4TI- zZSx|*n|fUUobh6};qg8cw~5$yqMj`xd;Sd7K@`nyVN4yeaHHs~$!Q(Qv^0@>k0lEa z$I$En6!)TNc2S-aq2TgmT62PqR1q5NPtquz1agKV@)A@aTj(Ran5Ye|Kxe%3va2W&q;^c*J7sstsf3jW6V5 z#wl3@XemdzvQ-9XD;r+DdT4w+L&zQ8v`*H$s#h1sE)7ei;G!tQDRxjCr%935gMh8Z z3Ck+u6@9N+oI%>YM?G86BWiTqhT`OTDDOuROlBJ%)s5O;aJth`^)jy&YlhcN7&nn@ zt+a&McpL;kRQCb?WDb%pz7%z*I*tu!Sc_tvXMrX4n=CuuFlJ0x9vA_j#TMNcM0v+< zdtPWD&Uuyg>mn9LY%kl$w}Yq+-A3g7<3MxaN#HQ zi|8VnZ8q>dV&y5OWk}#7H-9F@Ndk6b$ls%wWkb%?kY#?xW^uZ*wxuS$jV3&95tPr| zRWPu_y-3Ls%l<12owXdDjX=****;ZTqNAufek_vDP9JuI8dZbnz_+F9f!2K9oEm0)1By6>!{Y-SaSN)!Q<(08y-6gwI-NFMJCIDG zkR0N4rYhPCs*3^VFh$5o!M?fHkRO8P{hG0oyH`WPN_WXV+L0JpdhQ88gv8Z5s3GU0 zK)@dFXo8O-swsTbK~yaAU^}bIMLF@uh>+E5P*vo*)@u1;wqA$o(&H$r3Hcpr%GQ9C zaA7Tr%C-C&p)i_CuS?m6-u7?WwwIWwcCg{_ebO?`NB1MK;`5`6TNJre`n^(eLql=x3k9)6nJMV^tt z5oTtBljFl<5TN~AZ2#q>ngt!3M%bKVFO#n=13EmF{R42e7!1vkq2?<>buIKRdjf?; zB)MsUTT8wI1!7wMF0O89bhSO$Kk^aF$oF!-*pFI?yB&eQ27+bZ4+SeI{My8I42Q?&+N(zP5d-tXl%_fopgKZ-66 zr2}TMh=kt@4DxRGh3Xejm7}}gYWban#pWg7IR|}Qh!}b|o*mDumfxK6W*@l{@rEu} z3-LU+3M2;v4={A8pQ^H;Uli=!LB#ahIsqAA1H_ci)ugCu4kreC?m4Vx~dXnNFOZ?`JEw9~l4>|fReHw8b5(9Z zsVjTLdvRNbJMnSh-meD+8&*S4g(W%jW3-d0{uQV-C#Epn?T}%Xsf8km zVh`1YjX><&K5M0!J#J6&@dNhM#xkC~c}|hE1H<&hxSJ)!ZO02%^h7>jeG$5Pb{i3j z-RRt{0Qd;%8C#5nls?$4w4ivATYXA|B0O0IB8nrN&J{;=i?L;AaRm{}s64xM%7H~Y z=dM}Z6li@~`V|&S&I!zq;?kR`(*2!RI-Wo}%@Z#JzTI31m0-6?UV94*hc3mjIr6iu zo#&T1p3Ed%Y&6?oW|!a8Eha{74>EKqhvy#vWwsBpMoU?&k&E!DiWHR-=ghSi#XP06 zn1#JNk2PFwN({=U0>Pda#X`);9kwt^zl?52(PA!m3!t{5u%(U}@zU}TA&dFemtPb3 zU%VVDUozVYwzWz81w?Q@V*u*2^(VPoPH{!9(W!5>nf;)=Zv1r1+Cw zFZ09DZ?e!?WpQR8iOkCuk;QbT)FOx51{Hcm60qvU9XUn9ak^msTZ*eAC3fQVWw~3i z48E7&+*%gvdu^atPlDl-i}hv>r%#mU|B*d#Oh$)hT5|^0RZP+(mM2r3?w4Pj#VXVU zhj`}0P=Fmqn6+KZkEpa3Wcp&K1Jw-Luv5N~161);|NbH#@X<+S3Pn3|Zo5mMPQn z^8xFU<>&M~Ww0+QEuVYw=`0@;y}c*EoA2utc2Kiy9~niF-&BhHroc^}8@Zf-)CLm=VC!HnD)jEsa1(W6CzJ85; zh8jy_aY?H*w&XYH^l!a@Xe}C!j`f%C_)G|^MBrH3)1f0uJ8J$Qd zXo=)_ba`F=$sBu%5*AQc>;cGrX|ee#NuMPIS5OlzTea$g>SNWDRXpgK>=fOO{6@60 z;z0{VQk8;gUu@_#jaY4gcEI4rMif)M5j(UNj;r#gY=9^|wDvl5e2C!HnbXoTbF!SL zd|enYfN6P)XmO}e{1?{^l$j)MS%x8CW}vuwDS;2}rGyzKLtybg7&{n}6P?1(BIl6m z%N&eec(){nR~R@9uvvU0h-YN*`C)GVQ>$@)h5Om0`7R`Hzmb?8@{n3RGChDQliFdm z5Fqj#P9}T4cUgROQ>$|j6Q!`%v=yH2GbS6E>t$PlfQ!$?J(AYKEc6nS$c}pBCED|r zR?jk#x3Dp{l{U3XcKnvu!O}Zp$%83Mz6JBbdlqLAXaP&F2M!edTdeRqT1qX++8JGx z`S1YIJp*BWi4`^2W$idDmyy}^qZ_8>;uLC>i;v707CSmP4tVkD^BqwLY>#045){`1 zasDPNoG*W~s>M?LzjiW7BP|Ge`JGl2WxnIC3fv=WA@(~kin6(sd-n<9xF6x+9 zM=b`_)|M;0%)yw@+q=CE@gaVs!mRdy%-x{#$3upnS6{Tg4hgK~k>#z|OM8 zXREC7U1SrN!=uamOw4^HHRUX;)qamvMxQ}e&qnKzkB#7obHH4Zc4kD#fV(J)aq*cO zaAkv@74AfojwHMz%%3SED|SPbi(az{%k+!Z3Y+l?sV7E86k#zptloC#R^;zPRcrn| zRC%zO4_U1?P5^RIZ=kT=+JtQY{e8C~kidULNtd1-js~YCkc9oKP4GZ8$5Q0CW$A)K z+hDoc_u50%YNuGKLD$Cp0)dHJ?tBfZTGx4~YF+1B&8=$`ty@JF<}67@jcnV2nm3{m zdx%mluXxbKY8lvoh%)NRH&`Bu9vo=Zem~WqS#!{Qg%y1^fVK*)vew!fuS(gzfPnfG zTn3fhsn_&C()G2NPz>aDS`0*H;}}T6GLg(4L+i(g_5B#eBmJqDK~l(LOUvY4H9D*H zSgmauoceq=;O4TLm?c_U=$?en)YMTwz&T;0aA>pn%NdLkSG}bx1uaU zYTm3au!kzM8ri&GR%N4W9|OkxgH||o-GZvr^+Q&3>Uud^`}aM;B0uXFJcG7LbGy)- z9QY@EK)@7sQ)W$h60N9!R&Ml_@eT!RojjVfe*_TJE~+f8T(I0{N{`IQ1rZj$>_Ci zC%qrGzS`|`P}1BvF?*;Vl=|+V6}JQMDJ!x?Y*a!F-nhs|z2K_%Q3{eEU+KfYn0(!22cqEHM3`~6I(*PN2z@ibY@sp?S3!e8C06*rdsj-j?sa7@FzB|^e4|k zRcxOH671@N+xA*oWWRR;ZDs&Lh)@HU{rOeq{{bkwAh^bEj0RXTqsC1;y;6qMtM;Gd z+j}rVEaWu;2^%tU2by3%Q+&rwP?w3DHqU~dd5Ceb_2+uA6g1dQ)hYK+Vl<7b_MFw+ zj)LmX1USI z$vlg$N5s!_*ND;QXyYE+O<|4Plh%{QfTy+^1H~z=KVFYEUokS6czDj9_Kd)7k74UH zDoEdrR+T2qwi>C(o`$I0Xi7Mv*5dZ@$b~)kslP{|e$2o_T;RIxo&zpl54r2Z)-MS~ zJfRnYi*vGq;-x;0Fn5&bi)G$YxMi2}lKSj2Z(2wy=rrrcVAVzP3W5H@sWLIce^9;Z z#{qo}X}$wO%_k}K<4H|We>(^0Q~$z7BzK>9xUb(Rk?LZLw*)dRzm(5Bw5Y>~Go2R( zgLsu+c69Vm!#QC6)mG$d=b_rQLbvgQS@5~O5QJ05^^8IFlTf_c>qSlKdV{q(BApPKFmDQaE@t`P&MFm*L3K^rn z3#ny54T{a4RyL~VMC+k`<+D9Kt|wx5FKLvuj2wtLymo}g9t5tF6Rbhno=WuH(G&(G zADEz=Mxrp^`m1{->Tqx^k|==Q(kr(5*}cy_P80A;QP4X)joMq~8b5D!{?x>dFWqZs zwxHO7!X;IIjJgb-YuAcEXZ>(1f=FsdfDX#hHJV2ox2CK<&ra+N zVvxnEIT)ZrStwcrrl5Nmh{&f-6rvzrSH^__dZq5X5F6+{=b}sby-_%Ru@Q(hWZy_s zs zdflZr=id&`=+=+8o*{?n{r91tZ_>Frv}0&+*nTh(Krm@Bf~Dw?O+?tEo%j*@#FEft zx$gtaK1=oNtSx!tk7e~#o z{;BGy6i%F?YsB>vFm;o^dEm=gvZ8(hBa-eHSigH~9s<&BexYtk&I`!k`q(2Ub}PFn zW;#8Q38i5usc-WZU*G02%V7)vh!-uL7S6T?nZ>7~QPwCMhfM3AVnO_{cF{=8bh3K> zJbLcHbfMAVh(@-oKZobnpig5F0lxnE-sc{d!J+W{^=$#mry)%UypH*!OsmcxmdGO5 zh18<1<$y>!2@#=2>L;AN8b3v%A)@-HA-&=(6w6Sp-xS2jpT4Mp5ZT^n9ALlfVGA7U z)*njy1J^%o{o>fofP9$6G~ieUqaH%~Jvt}~uLzuO^T8KV7wNWlFuXh+`$gj1c z&R3z_p3Aqf2c{#n;7WODQ~wFTbv}XRyBA(CQ@R`OJBqVfc>XN7iXViITWCnOx0O)4T!zIP5#U4b!s?Z4$?509y5)=l_Q4U$P3F>A3^T-$ez2p&gmMg0R;?p^+S1FCYQU2&Nqu$!vE+k3@JISd5_XfNtb8zWFs7J=#+@Bqc{_(Qs#&kkanZ4mUQlnobD ze1?uMVpRo@UeiR$`3y*@%gzVy0$K9GUkQtaZbiq4wYn#g?wBz^*&~FkBtDw75-5m@ zBa?*&R`!0|AV17c9cI;7D0pO7Nw?DntVy`#YbgNBue};hvo=hijAxp)$;?1xB!C%^ z#yh567+Ea<-I{@M*Oz!M)R*8HX||G#v#eI`qNWE50!ZbfH2{&W_(nT`69P^@Cpql` z|5V*n;bJ}0EuZHPjC!`0TY_oF(|Zr#^dvfx(iS5eN%48$JPMk;0-YQ*a6W6Gfrlsc z6QHg64OTcLRvS1E1y4+Lf^veV*|Zy0E9 zOt?jHnF0J6;3^WC$@AAw7yiir-RA)t?Cl6MkrCA6L<5g}J7Sj?u$wXM^HR~P)`6?h z8e$>CtA05p9jfYAl>atHD)xT|Rkc2Dwc0pMFMbn{E%MS&2;}b-9F-&v`OLr#6yGkZ zRvSz)KP)85ROo*FYJ^(BC7QnqC>Ts1dA63GmGBjHCEv*E=l~Xk4BQ$P?g^t-L<^TG zZoz6f=62Mum5u$-?1_3!D8GIy%ijj;z@mvp zqOH-Zf~s|sJu#3vLoN%XKk{WE7l~uHpOA4_XW8*Rgx)Yea4$%q93%HT1!{v7yfU)s zw8>LZoa9-YM^Tt#AMykWE#7ZKm?qE)|6j4y#rZPs)wli*kWHy9hdxcwr? zp2cY_OZg8Sf_wpQwN&==j$rmYhW{gqpI|s`nXK>^EgrMx_*#|S3=5us!WQ5i^clcDFVb|~fA~0Q)d=h9BDEP65=MD98B$s`foPT+t7^3;TdWd4(iG08kFK`y1|pNzzMe8=PZs4X;cM zIO)bqQP@t_jf1N2!d&Ae=r|HDtI^bW2{AGsqx~vSmv4R=M?$)KrASV&2!P3}Q5}0~ z&D)7Ml8L9KY7I#wA=?`-+g}u567zt@%Q4|}*3DBj$`iR_gRg#dJhK?jC-xH8csUwT zL^})VL}Jp7@UmOPb0p{Bk8C3zLU|htOT+`e28%@kxZ7CRYt}sJrrtSXX0TZ;5X%Vm z6X6IH@m;3YlG-d^jm5)*7LZFFP|S&*2F2ZAIaG}*Lv6egkn>R-Sf#J(hCVwxg&^y1 zw}ReFUsmC%w@9W4$>TRux{3E*=qBC+jVAk3Fo=C*3#yV<9a*T??q~?Q)xg;-w z2V^)d*Zklxuc6>l<;3XNdFw_d?Nd(t2Lkm~s`Ps>`BUkS@V@W841d9d(CK$#IGrW! zuLDA21?ybolq-Nxvb#{qASoK1O#TbH%HJq=XE$tD`td5L<@l1%63FZ(*&BEl^;=6fQkT;ZUDfxfX8FyR0|jbnlI#q2MOI2%Au7P$^WuBAp%Y8u&V zZuv%F(wyXpAORG4F803ykR&YfH=L8X$)#bUtp=&!0=YH7)&}pF=psj;!+EAu7{Ui6 z`c4|Ma_RpE1bQqQB2)1kWrtK0Akh^cG9heC7G%lxP zw^&tVU&-f4(xl-^f(F7Ck*J$Eu0S{F%I@N9K}J_ZOhrH3xMGafGS43CT{HrboMDIujSr)d9vJ?o z@lg~X;uK*)Nlf9G#_ItjGRdC~MiQF>Ng$KmAMRzej@&V?UU)|lEMcGfnYY(6=~l#_ zJwW1hc;MG~lmmnIDhs5msf=YGF_^{{6qT_|-B9eD>7QgBwBipi^6e--82CX(W7Sko z?ynmY_NcSgC=!PEzY-4RK(SG!3F%alDjg!DM1;*NM@lvL21}7K_Q+Ehu?@|iCxTwl z$c(jj=#>^a9oeFv^U()fCLC=5l84uw4jr#%#I?BX)} z4~1zK$)Tnk?v#hZjlZp+kw2);c$!t&FMg680~pSeVSPKLUt33+DBn2aCk5a>#FaNk@4fzx34>nT!Y#9Gp3<#Sj z9iQm*?rL-;{dP&&TJy)OaKFjY+`;|v=tZlcQ877^Lz-iQM0J9d>tvyi!qDMhbmKXU zY5YGcvJ@NIFsAYE(d2lZe#`)LvGLPj>YV34h{HP=0%g0&($^S##5^6i8VNPhY#y3d_7ic> z$vKtKCT<*|qp9zMa30wAzR|4R9@Ojh*iSJ&=(URuk;9RF?RKDovZ|jN7#(=`;Oqqj zFPgfVpX&McKu9=^~c7)T4NuHLG5_(D=q@F)~Uci{}c%_ zK~KZb&u4fLT7^VzEPBI&IhqGU&ty%#IF)Mvar4lKL_bEVo6>3BoTqvC{*O7@#xSgK z%BF7NZUH7z_!3}>G8Z=f7TOp?r>27+F3h(8l4C?tu#0fco=D5ROo8BuiWqmEI4v>HkQfR_vGPzu=7@PQCJ(6tS#vPjeni%zh*+Nm)~2yRte2KC zs?(H1Boc2CC7W*s($FK;mkY(@{;QYy8Rhpc^Y{ANh_C&^*M1%S;NFf#FhQeJen8(2 z5mur_hxgJp=8^VCTQ;jBcA4%IBE8?OeHnAFHz9}=hllUh;ur?{FmCDFuuw4(&|U(L zsCh1$xq7O!bO2^-d?h-F)*es*ta-LS$^mu=IKuA#97yFfWTo8eU14%Dm`cD=Jm4-U zYJCyA0Mi`_0B)X*$7cA3!TL=&=-3~Y+P9KZmL`Ny@XcQC&Lel1kR5XZcWv64xI0ct zQINY#9}1lGNo$)!tfH8ivPGWpn0S8~PYTFlnn07kWo(94ik>HF`ZA-qeU-vH$VUl&BZq`z6#a; z-zcO1Bk0lrXM8de@Bqp>{BY<>jP^}GT|$VH&fwqw4C+)qT-hklA5MS7;wOd*BNAe)~g z&JbafLy6|cK}fiXE*jD`b1}e~z8GkJoGvEv0%Sf3-Oe9n6~r(0@I`fm8_uYC1Lo%d zy|}^Sb_~+-g4T@Z@N2HfC8&&9BBm|H_PpeGK z-7xX3O6Ms4>GYE%xR1bwv0P}Xu=iuaPg>C@arSIu_dF}>%zWtGQwiS-AiTzGe!+@r z0Rx5s$&}h^O(LQ?rsBE}kP=sb#B=i&6t`9=|4vG;(pHO;fKFS6NQvmYQ)~E2B#2b& zIDk}q)$sK(tA8kH1!(i@D84oW3wf717>Ne$;_xaL@nDI#&s_B7w6IdGpM-y%s&JzX zb&UyT8q2qU8FcGjQ?m-@p#bAix~&(UX;xbMSLqur0J_B(^tFh?cz(Dn^0i^48u1(q zviWct6;4VUUgM)4dRA?)Z@&77P-U^0dKKvpnT^8R8?4J&>~FJ*@YZwhK3T>+2^wsm zDgp=^??Z7z!j>PSQARj}p4^9-f}YS$oP$dwwFfvc8)10X+x(*92~9#ntE}lqWPNN+ zK=n{q<91+;PFpD2e@}RVM5~FS&sJhcnOOU)6G8YRTu{s5iHQyP(||5h z@p{=RR$)ZEMcFEb2ewnI1_4FiuY??p%~cFEZ$y^@4YyIMzL~AlX|SK6`9r{R2OYBg zRs)UN2gf=QMlrrdBq2aISAm%!(`dagQ4cJ)iDITJ2CaiIQzUK-YJm-!BN2D&Aof_{ z#2pfotw*B^#@@WaS9P~7Lc%!aQwD+mi;c10ZK8M<1>HvEoXG#|?p-U91Rz+ffb`0_QjX72CKPFE`;?=+f+3O| z@g~Ia{g-H@UGs1(QUF+O>t!g&b!YYf#~89yCJ+Wxr$ePKi0#cRX z8?F{VFCdkmuHQowUu<2@#FvEXDXbn}E5bx*5ukg?)f_+z{8o+%UDK+X)r!~ihC)H_ zqWn@mCXKI)(uUWk4ZrJGU2b@zq&ZdLagf1Wo(Y{cyl+Qi<)*B4Cc36bdIK))%o6iC z+eYRqP|UC?YrV^WDmP{9>DiRcH_#b2Wvw%*7JXhbkjqG#q~xs?hIjwS9Wuyja?#_+ z4a|VhTSGE2mVuDL5sHmSs2Wtpv&-ZJAGjG%y5Y+5T(W26Y# z7k4c5u$ma%(Y3?!Fe6ebA3rO#i`)%?sd*XZ)b9UOR23jkV|B&=30}EPS;|404z*at zG*XwqQv?zBgS24lt;;d%3KZe9Gdf~RHesy~8qmP6tZ046iaw_AK@VV@RzN(hbMPGP zf~X)EKBIWI7*Ojx5F2?;xZKtjv`MgG4!^+G1=d@2fYIXj8T;cU*zWdlDc7`z!*tOS z$hD8B>OdW1rsiBKaRIm6w^*fxy>4F=jZtAeilP8*ak-zGXVt0q#;t2GQ^;O4=sFHh zxJLTG*ZF*@@y1 zlFhsV+T8jCpKr9P7;<;j@OuCW4b1L>p10^z2JtK$$(pVUtN~<;bftn1KCk1+>)fja#FBHK)jgvN(gFeF4u}TR%Y8G)Y$U3%oRI`H_v>zpUkl z23ei8pvT3hM2UYWv9KJk0gPe0^<%5CDD#$gpwFcb364G1F=Jpu23Q@~&{GCBP*A)L z4Q?u{FtqWpGQRx)v`-P=<^vIRGL2-vu#U>(*%o`CLNgt}w|)*F8hoU@U-6GfTBzhWXyd^9jW8=moa3yND) zV~AccRv81|Ogf98F}xEZ*lRXWx_U}_yBBQ-n{8;QjW^-3LUvuA&FtbH(WROuLdDs`-Vuyl+i92G+zNpy4u zbsMzaVt!yU)UAD(710}qkPWmC6K3lVIGbPK@G6~bpf3D-|cVlYpWzJ!>&$UOEU;wT6CukO7 zRKKDFbPI}=f$>zBS6So!ZAvg)o064QtKO6V#_73LT35i)6YBPFM{EcRqEx}_AM=kkI5Ojoi}Qulo`c$WchF9cl=hH3_E^!E+A~?&Rd%<& z64*_*%6qERzxMAKkfV@5RodM81idA;Jni2BRHD;NyND_1w9*#lR&I`78nmpp03}a? z6$D_FqGl=h8M2smxPf4QMr3k)bmgYWk;pUqZF|+}S5Qt!p?pQt+e+1Fy`SdzUQi+R ze_yEn9;?$?Lcj<#tp=aTwT1TF=G}`aj=iZZj8x$T5>GT*X9T{{R8||R{W6s{41}iA zUS+jPQz1+m65^9~xl23HQ>%_br}e3Nn-|VRTkkhAnwQa$at|p-%4n@B+(|`(oLVOgIemXfAKGSmGL0kE z>+6Ul_@(A$L0XILx&5cngzPVi8BP38!0BM(JOys=u4$iS1gHr0~K)}H2Ef#u| zucqg5=xI{L-3tJ`G;x&i&8H5Fp(xGEXoAnO+N;LWq~157Z65AaM}_8dm?ZM#GD*A$ZgVQRUi?TWv<=;Bik-4i0KR1{{x9DaW_iV@03;*SQf1hkf(< zi*Q7O3_!YKLr?J6)R0t=z|_?1O;&l6Ch_0oo-W#?Y6iYGA0i<^&ESIQ#G6l`My|EL zY&Azsud25HS`20x7WOcQTG4)-m{*t2&4-im{OYuv_IFAk$C7llP}}xX!LxrSVLtu& zQvd>{^h~k+R28MlOyPan-_hwW~zIZs;tG0^g86)pb=w9qw$d~z{hj(nbC zht{9)=P^-DOunixM5?KQk@iIJKP#ti|L4?e*cjIEv#K>PaspEyKO-xIiZXX={|q#0 zp;V+OVPnAC>(}6x4{#3B!7efJa*24NxB#F>F;b0M7>t|;wPdkl34o%2`FI*1SNQmd z7lr@pi#E`35w1`aG+xmWd9&MQAbWPz^I4sFn?c?XB{dIj)V*8qjoNXLK^4w2ARr$Z zF%m-4%}3`5nVum!hbC>~f^U*onYJHo6J=R7TxA~yXT>wZ(o;@yhRP=D4(VSpU zYWG-t=f%`h@_~oSiI?l(bVfmI9FPh`Jl0UZ75B%b7EK?^+7|&2~VGkHFaL&;a^Ai zN?n-mWzyl_35^7Y7|@xI;$$nDNyO{uR1VW=CeC>>Xps9MUxWJzK=zT9nn4vStjMy6 z)P!GL+G`D@vyen`s_08P>hEO|cNU$6KwNc`mfh`l`!#2i7%m?x_9mQtMS>pgQtXcy z1wz{1xp&@*$6rC?+CQ>_E39;>ofCUJXt+$Yf7cZabw`^&>MiJZCp2p@t#%XZLRIoV z9$+9*0Mp!7Le|^q2bJq7OlaVwyT;P{xf05NXr#*~v>&@>3xB1t+cu~34 zfWIlgS+^P-6u2taTweam@9c{RLPha;lhB!~68j`9d3M)VPgoB-$5OPW@Y@#6}rE_h<~GMa%gmHa(n~&G`Zce zDOT~(7&5vPwa$h1Gh_epOdyNjvhTz5VA?8+h2j=pu%fdC#pPD?e3n1I!!wn?lFa$J z7x4&q-3L||DW+OdrLIw-H+Ykd$``+|H~Lmwuv2Tp#Vjg~_>#iYC_p z$sOtvz6;U$C@8v?>%waWhdKee0zg-Lpy)f!<>CmcmEi=FV(ZL z&3mk%iPe@<_i*Js0^X|3pCts*mzoh1 zWxd6<0O`BP!I;5mNfv*;%s(k2h2?ftUuj_o?$1+&KrYrM===!NByY$%KZ!Wb{<4_q z;%w)~T!v)jF-JMc9&7CUxJ1{NY@)|mIL-b7Kth~CEN{-`Lm(Y)CL-*F{3nb-ck4XV zxH;mcQpal?xEVd-kYYEVQCP^LCPMvO$a*rk5TY@eKkj8FvC)BG)6Sdr}HZ#brt@Isdabw4$)ixvIQ8^SZNR| zv*>%A;3K15=c7rmp*Pu!Zu|1`viQ5p6jOm?%rz&L{YbZq=@NBh zzEEg8L)+t@eoBC-u2RptfP&kT=8dR|gbKvnj_>AeMP*_-?)k@)qst5zVGnHdW(TKSW)f8^f~n% z)~yd`2QSuz&UJni$qra)`;=SfpU@96#(%^X&t3k_vM9F_6KL|v=90StlvsCOmams6rk9i@iL9b$DdjA$L=Mlau} zW!+a&f=}2WWetENM_ob>C3WV3;q;t(j-mw7zfw`ePa-Xb!glAekqS&7Sf%vcR|68f zmB8eq1@3WBm7M^9GpKU+_{24lrf6bX4$&#jmO05)hNdqkSvW;bf;qFPQw8hnFdQMy z=XW9*Dn4h0OSo=T)xN#88MW@aqflVaoxidozY|^YPRaT0Clq3Ob+PkdKuZ#bpi1%W zv`}M1)T&6 z0N=fdQb}VT979(>=C}Z$i}C!~h`yuIdRH%2o_uvbXB~Y(uz#pQ5wv?7YPZg_vfi~q z5ho3WTxvL~)}Wg)^0p*a?Li~S2jaekiW@hjAl{P5x~8r7w$Qbs$m#^_tFOhTz0-9N&5R84GRRBuAVhcW;62hM&JU2~;5F4}F^td$ww)qQrw2U6GQc! zZ?P&(s|%}fcO}A9H(6Ugce<$nfGt7vyT%A9#%E1Mcti`gJ>Va;jogHD`~)t8%b(j* zPjInIpc}@{vxDN*n^sMZ+K1s=#d3_u_TY4;Rel^DVWsDD@4&Ohiu_9eKGz>0;b|$B zR(u`RJ*oGZ}ub1KK* z0Aeev-?dsX8!E0yrLSN<4}hQBe+M*BqcTwAE%6*f3qqF8JG%S2Ruci)WyhkALG-e8 zZ3Bl}*8z0^*y=}-Vv>TtM~jGg%4)@T=?(UxRewbFU^eVS1D1BcL8#ezLKOpRZ{bq7 zVYScOVRuSe9UE(JnQPC*a*`R2ow&4poaR95Kj2^#WJ>WaO z{8?yV;a@Kj*LdU>&gi)U4Kh|P9UI9=%Ij>9qMb;gz+ARg!!&OLKr~pwkmN}>_*Lld zWpat+fcwis0HDDZpCQM;4_xB-4=|HX)@cj31@bioKnJ@hc?yt!$xAr@5|KTQJ|V*{ kky3U#jvk-Mf6X5B;pbv(ljL$G0Jbh3TfJm--AMNT0Sk4mrvLx|