From c526e5ec0032e89355b75f521c5edf49cc7e7e55 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 15 Feb 2014 14:26:13 -0800 Subject: [PATCH] feat(builtin/kernel): prove false_elim without using case Signed-off-by: Leonardo de Moura --- src/builtin/kernel.lean | 33 +++++++++++++++++---------------- src/builtin/obj/kernel.olean | Bin 51330 -> 51309 bytes src/kernel/kernel_decls.cpp | 6 +++--- src/kernel/kernel_decls.h | 18 +++++++++--------- 4 files changed, 29 insertions(+), 28 deletions(-) diff --git a/src/builtin/kernel.lean b/src/builtin/kernel.lean index 1d8447b44..be3379248 100644 --- a/src/builtin/kernel.lean +++ b/src/builtin/kernel.lean @@ -37,7 +37,6 @@ set_opaque true true definition false : Bool := ∀ x : Bool, x -set_opaque false true alias ⊤ : true alias ⊥ : false @@ -89,10 +88,10 @@ definition Exists (A : (Type U)) (P : A → Bool) definition exists_unique {A : (Type U)} (p : A → Bool) := ∃ x, p x ∧ ∀ y, y ≠ x → ¬ p y -axiom case (P : Bool → Bool) (H1 : P true) (H2 : P false) (a : Bool) : P a - theorem false_elim (a : Bool) (H : false) : a -:= case (λ x, x) trivial H a +:= H a + +set_opaque false true theorem mt {a b : Bool} (H1 : a → b) (H2 : ¬ b) : ¬ a := assume Ha : a, absurd (H1 Ha) H2 @@ -110,18 +109,6 @@ theorem or_introl {a : Bool} (H : a) (b : Bool) : a ∨ b theorem or_intror {b : Bool} (a : Bool) (H : b) : a ∨ b := assume H1 : ¬ a, H -theorem boolcomplete (a : Bool) : a = true ∨ a = false -:= case (λ x, x = true ∨ x = false) - (or_introl (refl true) (true = false)) - (or_intror (false = true) (refl false)) - a - -theorem boolcomplete_swapped (a : Bool) : a = false ∨ a = true -:= case (λ x, x = false ∨ x = true) - (or_intror (true = false) (refl true)) - (or_introl (refl false) (false = true)) - a - theorem resolve1 {a b : Bool} (H1 : a ∨ b) (H2 : ¬ a) : b := H1 H2 @@ -208,6 +195,20 @@ theorem eqf_elim {a : Bool} (H : a = false) : ¬ a theorem heqt_elim {a : Bool} (H : a == true) : a := eqt_elim (to_eq H) +axiom case (P : Bool → Bool) (H1 : P true) (H2 : P false) (a : Bool) : P a + +theorem boolcomplete (a : Bool) : a = true ∨ a = false +:= case (λ x, x = true ∨ x = false) + (or_introl (refl true) (true = false)) + (or_intror (false = true) (refl false)) + a + +theorem boolcomplete_swapped (a : Bool) : a = false ∨ a = true +:= case (λ x, x = false ∨ x = true) + (or_intror (true = false) (refl true)) + (or_introl (refl false) (false = true)) + a + theorem not_true : (¬ true) = false := let aux : ¬ (¬ true) = true := assume H : (¬ true) = true, diff --git a/src/builtin/obj/kernel.olean b/src/builtin/obj/kernel.olean index 816c3407a6aac538ab39cfe3b52909fa92253a27..6dd8a2e9359661c94647c10e32757c41a33e6950 100644 GIT binary patch literal 51309 zcmcJ237DNlmG-yX+jr?^L^{J{; z=bSp{)T!mG@4FN0Mux{n$JUKx?q9xPd~D;$sZ)gOig}Sz&0y8`e!{8;2*e;_!)yb%sr}e0Wn{uKvFU}>eTi4o7L@qo|EgyX`xAuCiqu2i&bo!mtvDOP~1Y26Qo=v!G4rB$b|XQ zGid@lKXzhzczSGN99Vhr!VCf*Olg|g^xCZG5;{uo4B+pHL_`6J-(vtu3f7lTCpC1* zBYO${3Ya;#tQ|RRaMqr(VPpuovjOFyKq^sEFnt{ACBWkWO02yAHY5x9W|`=CSsrU8 zPUX{+8%Bg7Ce31#vPhfcu@6Bc?A+7Qhv~_&jbp>>RI+#Wbksft$y_8)f5mzkZ*SRk zba0th@50XQ~p75ALqI z_3TTMI{NzX_!=N)2ZcTbIV6McBIQ`zO>f>jlAB98=2zr+=1Hmq^`+hIZasTjQb#$) zPF=rlY-9?^y=3WD;Yx)HTy@;CLmvS9iG10AOou^vRScw5Og1*Y9o0Jaf%1Vk$ zcT^`1Lus>7tQZ&WF~kCa@rmidvGM82iAbketUz^k0FuR&@+AN@tX~R{RUt|qVI_)D z!>gt?Os?r7wFLMG$15mWwisC{{78VJN{*8CD3mUi!T|;?zsxc|;%^$8nx0C{d|Y5k z%~8Q3{c;eISyuu)S<3Md#rYfyWf9FO6(3FM45W-f-PRpX5q$ZH*kofBXiuj2UJPF`3BAg6xu{oIp>^y_rgVl@# zsd3b((|+ijV3js>;EJm!%nygxPbjFo$wvosTPLNFCb4C3WR)$RM{=NIOps_~0t)^) zXc@;t4mv}VRW&rI2FlD)M51%p%Mp;48aU7el68X!Yk{y;v*>F8XLD%wGXV+@P>^no zWu$8Y5sG_ zoRhtHZHN+V1h~!ED*S9kcF6Y@u4bNrrRUU!RZ|!mhXEmrt2p0zbBP#Zs52WrCJ&v2 zQrHMLCbadQh0&;iPzT8zBC%1&v)*LowcP%}^~qd8<#S1xk+$RX*f0_B?^8jGmxqph zS_>EJi6PX1wH-;v$D|#Uf#OhFsw_C+TMf1J!klqx?-^8Pz}NugY+rR1Ajy)VJb+qO z%smJ7^2fIW)F62WzSZ1yhz zzaLdXvJ!>$TTs74Y+>U*=8^QU=Ra9-@UFEMSv!*$QNg(n55tR%&D}?>1U_j(A{lBH z9W7HXK$d;p49iP^CJI?Y39mwy?JQ79&D(`I7d6p(MBGfw_n<~<`d5Irv-Es`cM!Y~ z;4Xp}0lbUg`v7j2v%fWwQ2tG&u}dA`&1n>C@i+TjA`Njg>ryb1Jt4Z)-Dsd5`N4Xg zl>~M6(k7Zvi2!U8HQhNqP;>CGRC5;tjS@1U1Xaxeh4Ljjdp`=Lvkye@g8-M2$cGHd zh45j3^1Y7$!RZWLF+U>q7J?z^0HVCC4TI|6t+>1Q2V3_NUqZVOF>TB!P*|rqL*|8# z7~hu_fWDoMK|Wd=5Y(X9MtUr`B!V9Ur~&kGfWrNRL3u&kOHrx;^jm=G0CKMFh7W5g z0DDUnQm3#^f;PorK4R{)_y^?e55c7j(LlxvOtS%3$`sFW~?I?@+~!9p~Wocx|nqxa$#9_hRQY_Yy40+A*gYq&%>%$DHITS|{ zwg(*4sR5O;C@PErYaS>sv?&vR^A)jINiC|hczXiCti=56mW|jf@#F&zEe=3&WC23f z{1~!56M0nSM*|`q5YSrQpM*pzUM{WLi9T|g9d>y)>9JZr3e;uDFM)>^KVOdER{$Or z)(CSdJ&yXP^OwL5OR_Io#@0ra{pn_|FV+zCi`DJvd;eaw)-pd4dP4`2BNRUhv~mKs zqv-5_Xj^&WHOQ+k*GBLg0FNTtHvu-N+Y6a4wI$%reZ%6Pu5&W)!&Ro|E^n0Zw8gBOP{VhZB zOBsl1ryGw}(u(^lh=8*M{=R`u;2R_Og9!f6Kqv5z08X1HNlV+K@}&VZqLzdFH&}_6 z-(-Junw|!`wIuixkd|6^M)0Q*{F#9i?O>Fdyg^6~uEb9;I^9YQP;iJJBjdx!#KWAj zV(jDJ01_?TZULxqcq>57y1xL}U>|M+I3S&|T`)yJjXyI97Q$nRF=@va=LY zll=YQE|+@%pbYvy0A@Jd^w=}s|)al zTS<~-pR}0Sf*LLSsNS8(!|gQM%IM=!AT|#(;U5e)EdER(NhE%RI*FYoWm(uyCK=*z z{l);S}s#MlFL@6o#M2w<3`ews)o2pWbIx>eGT<`l$2Z!d+A6?Lf&qIte2_=x{w zk^dd}vscDnVdQ4uNQ;RUyaFC$bvm9}J#3G{a0G>abIo2QWa+sK7hRW}u*i=H3;^mLa{P_`VQIwjj#*)JlIsiL8kBi8s zkT4P&d4*bxS6fiY3pp;NCbVE-l?)5H98UW%ICc8)`t>8pvj%d<5+KJ!lHbO@JP~A@ zkff-0_2hA2UBIpdy=(=b77Nj^fI*ADLIT%`t9LH{yT#6r0mj1qVtB)*ET`Rh4w=6>J-fvXY zpC6B=^L8gPG5nsSnBOg`+S4)`Q#_+Exgg7aNaiD%C#fJ|rY7a^nl*M200oR1`ID;! zPlLB&pM?Kh=Qv+Ylr9~E2DPOiN&ELQ^^ygpJ$S|%pZ}VnH5KJlQR$yd3Qx$kAZaGt zEn7SXg~xO|eDR#p3iBtcV^5=Xi$j2zu!LG=poJBdGRf>LUkFN7mMAO^Me;mU&rt8& zpv~Pc8QGJSQ8PFJ$o7RWImP6(oNFku^Z+0v*4OOa}tUj$HM90X8CUkp$)<1-B^Udl0ZV(bVvHdI_ljHsDq?L!mf1p=h;^5m%T}ccC-A}S)t}@__0&w3nEAtUuE*R<#$gZfi8Lc z)cJfXaiZ9riJ8y1C8v~2;iTf&m7Z7}nfq4--WY5#6 z?kusZJH5d`;pC?y+Z~q8G>mqR4Xv)?uqeJHwN}`X(ssy{tP0s)OD*&v;{(u~JAL8@gAF^<)jnC9;wwnf zJ_NHCS6BFvXu@v}P{og;&|Tp#zANNcQ3u=4t`1fQmmh?1@+F)e&A5&f!oZ3i-o%bD z7$uH$icxfqv@U|D0+b_-8o-HV6=;%`6-$!FJf!)0 z)XS4k1E@vvEdU*sA8SNE+BD1P#_d2jj?X6yUpm5Gcos4AZ)%Ek}h!dlNt{ z?Z`FJ&~jAyT}ZZEn@LWBF8ZS$;|hN>CmQAFIY(UPQ4_)A&M;)J%)v2iB4-!$v7jtd zz6GEJeJeoS+ofr;?6K?{x4+%Y-i$^(JfL@1x2!9pPN-=n;`jGp!W%zjWdouWSaKn; z2~_U+a8EetQdo@$nIokJWU=^1fON$CZGebXk{Yr0=Ca*L&U&v>qthQc=U2w=+yH_y z@fLv6+}Qw2s3_kGP?Od<$X}_|D#I+#nX_QAv#j1vi@4}HJrOsERonT;OpPE)&i%}x zWcm&;l_>uNP@-^#Q-g4VkzeUu`|ZH9y+L(T^X6*7-&G6V4*jhg8J)J7y!%?sE2Cxn zOisVC)r&*j1o5yig}d5dj4_6DKso~0(`2+7#i^-@)y6_ZjHrlongxej=I&>J@D8@# zu9TdRP#8H413Bjb9UH64(>9W#Z4b9aJ9*5$lTHjm?y?xI?A4yPpD@=$ls8tXVx8H@}w%4Kn0pRMpYaKImbI{jU2audj1JEAb4p6KS?ksu$;7f zIpzB|ss2TJ6p=*b5$ppBE4?l^Ma^&wD{c@S`EnEZLe1(LV}jJYgEf(*nj5BEqyrbB zI?FSG$q}!X#H63VK+=%x*KdeoN#9r zw}8Y2$U{Q@y&(37iiinF6jv~D$XbWW4#XpuhVx_IJV}lhsOIRlT2p9gPPx7S{)t>1 z@jymVqle$P^*X!0?S>d(K)3% zq;_0!lD`{eU@%G}S}1)D`9v9?LEazfm&oN5XVDY#%=omVybMTcsjhw%1;H7ohc`?oFL+45KsXkO_uOZG1a|-yygVUC1#-ITUyJ-l(Hwi~Y|5G?8qx z|K(+D@Nwjmxn;&F_y?=2vX55_{;xVTy4m^ z1!K1y<)0u-V&GnUQ>0zM4+^Udc-7Ayt)nAA6gM^91~588Z68%>Ua0L8g`{3wLpN(w z9YM85AU`^lruUphX+jGp&7G8{d+w+`)e4LkT)#nh?rZyV z*8UmrdlEgv_*P zgQUeho?Gw1gk}dIIR?B6c22JzJ_V&sB*%1-m?1GxCXrAdMIB%q55CI9J|I@~ala=& zb1UVQL9wU|@o13;+?OYqwRL{L5OIcs{l04HKUE5fqFPX^7Bsz->8Aq1K?+9_k6f1# zM9|Taj@HxNB90{9HA?lf%rI+{z5~k`#N!#t)<|wEXzGRmSL@gb%h1UNl>?dQ{zF!s zKJV8yg;mrNnu8*FJ392@{ZL9gO_M0(y3)PeyNLBH9Rdg+sl6FcXRal>{?I|56ALap z@J*`T>tNvJ7f1cEmplM0_C}qQwoe3~zy?rLeke;rB5{$Wi2g{q*vm@%lO4V7T|MJI z4vn&to5kS-@YL14fI5l-5$00ed!(I(QhR!TjJ@Tf&0=3P;8`XwY-J~NTs;w`>dKQ0 zs=bS)PX_pIP0l9(1E(9WB;c-Scy@Z}jorGBO=+YZFhceZNbW;|htBw$-A8>=Dqw5J zNXWlbQ=m`&oL%p>hi6TPp$VSl1hvRL8otj%Bu~|lhkDLJ^_-KQdQK6!J1FLZEZh=r zC~iU~^{A^fQ^JKZQ3XVy{Vj@u{-sAOyfxP2>i}qUvfPQJ7DZVb{s5Uohk&^XU~wQo zNlq1?4DWI`x(up)R+NCX8p$fs3;|O0^7~Z?6H&GqPg8Nz{ zB$=KCP}*E#Q0=qOY3}Ym#qP-p2LYK5yBWA&rFRt!@#!4wj)@DbCA!DPhVjvfb!)m_ zA`L=!`$6qmGC!Ew(HM!+*zuV&G0T?Hx-W)sI%)vKHdoOEhaj)+J_n$>`&@u>9<04; z*Um5P4}I61Bya#0PD*NA;o78lI!btg2ZdQB4Vv5};4vTFfH8{!qo$*Hb%#Rg6qSC? z_b7{HAf~4%Nr!f#6oRR1_dy>#P^s-SXV=$IYCQNa7`}CpAbI>x0#rtFlU*<1McR~B zk7+28(UyWGc9ci&-BBKNvv#`)F+QS;p)>$WHL&98ZtWhR-Zqc=MF;exqsApZ-^D2J zh$c(~HpHA}B13+zEy=K~qT|%A$55;N8if{IB?DbUdO-Dyc6S^xpj+=lVenuCboz3=9R-2%Yj*%oJBnQuyFdl< zM6Tb%Gzi=GGRf{NLg`jo!`ii$)af+^@=m?n2T8rhqLg=Hv<`L++#=&zc^2Hl2B!V5 z@hF9|LW3x-XF{Tr&Oq`J3nxVW6FlQ*SN@jRQ^0J=Y0E_ zQ=cN8w#miupz7k#s{zWlUIUQA`zVg?d%Ld@mRvd-Da zUb=~Ek$8kS2UMvvIWl(vlIBFTJp^^dNx+g8PDbf-=36Sq?6C0`AaszxtwhkqSPYwj z=yTWmK467X=Jp02c1f`pn`SC6%om#E{v&ovbJQv@mDH;N%7NAxRQr!8D*9TxCK`}! zwdJH5D0&zwSk6l7%@o^>S&(OMIch_1!>cEJLBfrS*eSb2-oe`wAyUZ}w_^bmJ9CF$ zopJJ(-86YKHmQSSkbs{&DBfsL{kVpu#VIIdFsq%9(&HP&vGLAt{rLW3YDt!ZRhBGZ z>_OTl6lEl;{u}1OSgWxj=K{j6(YPE46i?Eq;;BJ?AlOqQIsGhXBrA>5vokkfyhAhA z*aUJ0TGfY;vc-0pscHFQ%94C3Sh<;pJ)E|D9VS(Sg@C-V>T80r?A3&+L#(HTRfAfl zX^&EZd3LvVzm8?P!`CD~iWO``XR9C5EY_o4*TdRT6vRmcIdUi|Dmy1@y~%3aAUYFR z?(G;@F00eMFy7ZGJKz5JQRNH+A=72n%rP|w7$7nUz`fy7U~IV&sVR;UgIfJ>0}W{2 z&qW3n+;h>d$+onzaE*-eDB_GxOb)MGH~5IOWfbaMe@Qd{2$Isw+fb$Oau!Ot!>?nF z=^J>xJO^^t{~kz*Izlf{j!l5;zvYT)Z{vTkoC}k748vVxa{L!|+u<2hv!I9JM#GB1 zVcddQG3Y)Rr47`c;6}fqo^WA!a22MD6@#l$MO)P`;0zjY^95F+Z%q_$2a-bRJ0kc` z5qxI^|JlI$g$+xKa{*oiI>qIdxUXPvbV88&`!HPe&<%6^AS0rExdWwY0IZ7>xqPhQ zpxEhi>=h|~7-ZBZk>QHk6vLT}BQsy>o9!^_Dq296!UfAqQWOr|`p2p$hNqg3S8Gyk z8u#;nl3a47_&mgMhlgnw4YPQ!C3SdzeYA=Eg+A{t#e`i~{Sr(Ky1_=O?j@DqTd8#p zPM8k?2ATTD0nLNf>sJ8WQIQMi*-qGQ7P&4U0+M-@>->;!Kn{J~QmndJ>pnQj>dBHH znEs|Xz%5A9yMNtGq>;~8IDHI_HpB4aw0!;I1y&F@uF;wdzqI-cgM$X8`-TDaE4ziS zqtNtLT3XZq%SjW9iu7(Y_dc{D)=qYcc@WIBbBPxHMmKZqlXwPRJ{9=r0Ar^cGG5t=ozi|k{g>Q#s%u1|38=&!&PRD!&O5ZgWYul>So+i z4II9H8LOi`018rEA2loBbJ-kxg97}G{iV_;1?qJ#Rz`MK(|)?GC^3ZZwbH$ zEz$WAA{;MVcFnid$1Y)L>9NaZGzy1KpSR46zCY?&!#&4h#Qm+CCX8?$2V8y6XXi1j zU5~#W!K)*9O$4tsuejC!r#NUY^Mvg1JK7t&hssCQ6Zo(up{nv{64n{>V9p?WayDo*<*Cij-e#|J; zFG~FOBKa-TrC>&v#V9J?#Qxz7*7fAZ2>u{~KaAjy46I+oX8(s^)i6yfEzUy&u%TZU zZ$WlZaCX&j%yv+-m4>!0N+~mT@NT=s$-e3kL?TIU`hr8;U<76= z^-&E72z6hwR$2q0c%D)JodJDgRLM_KC{N)941qVrQqDmtz1d3L(&!cg``%L3BnsDC zlB(}`%lA}YvRZl=t!V3_`M&5-&)iH&&(vP<#+}A(rsDphq4Y*7=nlxQ{_l$5oe{h% zf_EF(Ybt;>6DM}(9d0U64DFr@Za4JM3p^&Yan+*_8YaO9-EB(_Pafmxvc`Xdxq86U zPIu{|X-A3nuQ&@SrtH2CIf?o{3d3p%OS!7I3qZVfx?#(P{ET34bWROhJ-TLLJ|@a8 zh@)H6BlD15bK}N&2I?B5>MiR|;{ahIO^q#rKbc5kF^r>s6>r(_`LW0XaQ?^h=QcwPJU83a{JE9hTs9?rk83>BQ;& z3=R?vD@=cr#W@{sYs=}r;|=k>sQtw0NEZ&oYci?Rp@aMmg}cX0%wV_j6jUd6<9wVt zsa5x39wE&x&$Pnw%;28R9bxw5g(MoVw6ZQw3_j}`p&pi^JK}HOcaUYfnJ=aQ0RxfP z8d}-`%iCB3G3as$2aE;Rf#{r_h`!6f6x}=9?!K@fU&A`0kKbD<+n`5-mi-YN0K&H` zzQ(tX`fiY~{RzlDe64I*apG%sR=^(+nYn0JlmoUdRM61WD&t%ES70E?9z&3hbO=F9 zl2!#CbMYHNeGgQTf}+bkykcJq#MBihE?JU3x+f?!k+3_*0OCd2avy;4 zVqjx$RViFI_NLt~M;VR5kb^-}eA-5V22CT50!EUuVoQY=kf1;mAc+(@P2!m2%$9fo z0}-36CDk(oO6*D`OxZ98q0V1ou5>)gubb6_cpbc_#-uk;sw(SAC~WfFwWOkSnGUzq zp?_ZHR4-Q=Voq_YADW7~cdp&jOz5iEFPv*ogMkW##q;2WqOdp=Vu~Z=gusqvV65mXSwX{&RnTad zmSKYsozy0_BunXtBWZs~n|SeykoOMJco7=v8yel7!izgPEK^0~FU9U&0QO!{k+LKL z90>uAaUR(?k^?zsB=4S~6uxwjE)gnMT+6+y1y8INR6pWYKBbEB)M~-gss;O13!VX0 zV0f7IVn_)`J2C}aljjTRT~WpeKB+7ZK)vRQ0|_EDXjMQ9Vk|WN#**@yFsU+pxZ`xu zk7nnH*OMI#uxu+5eX%g+8)OnDq{eGKX5)3$nx6D&O0Hj$P(<6L!y$<-K?}uCs{}jX zt?OY=0ob(v6sU0oWQhzKuSYhyOfhrDi)tWMidmWb8Ye0??FV96uW;IU9ec6`^(hPF zxtgm8n{5T3dM4ZOo zTA>|ZAf2J|DksRJkXW_qn`KqHT-Bx~GKE>Vc*K~mmjtmY&-h8p7d%X}qpX15~F@?=H( zIh03f#UU_@R&9I~dEWFZ4+ltz%Oe2FBVPhAG2YiL+rX1(lsCQ}l~OTY<5D1?aE8s; zYv~X;Ja0)2)v&_GWnS;wdATg-v9sQVpsr*kv^Q%?7?Y}MDrfI#DmJ6N8rF=aYRDGg zs%vj20K%min#x&{LX$J?3_hKR-HD1zgQnnyI)}Q- zAo;%CopO3)EqF`ulFF;ws5`VsT|}6_%Xf=P!}+F+K|SjQRrcyvl^S=TR32;PQmlJ< zq+79gN-%pUlVX{U8XcUpNY+Hhb5N1!SZlEgI&r9XE^4HA#A7!+P6C+d9mime2fd2^ zcfMt-7x*X@t=d6jT`*@}!cl?{qJ#rP8z-mZFCCsxGpDBSK%u_5#I}44S`MRh2a>y^ zkrM|-Q{D9gQnL@3-2Rrk04A8eHxDMgF^r}rVzPvk%_6!Bbla?1(nIPjxjrjVhk&>v z>P1qcumLHPqujCXt}sMt9t;B#qqoa%x@N%CYi1jdv$_rAfd&C_kmt4a#vdDybFC$A zXfjA>Xuc7p(M6j3S+=>qQ)+X+M5*3MJAt|zcOlQW2WC@jbN&J&tu4s|U^=FDOlc;& zYocL54c`YrAUKS);`AkevIn5yA{h%iEnm9>c96FyZ&|1JNIkwUg4+8)QxTL_ZaD@0*J#Af}nA8|IiiJ<;aGsxtRw%c z68^wjZi(Z>X^6%ZJ0C5f6zBE!fjzy0=)de3!X)Plyo7i>2xcvN#Ao9{9--L7ooC|V z$U6g25!?eP2)-F4y-ag^GS(>n@|W0wig5*+FS4k>8*H$UA544*NQ^#8Y$_VEGJXz}Y4@mAn*+To@T<=E{w=lKy zBiT3~8eZ)yUGD}olkXAV>De8UAoR6h}1l9$Q!<>Eys<=CRU91U1#q1eQ+w0sBP zUGpuePK+qJ6txf@OKI7}rb4}UQM(keNe{$e2)g$A8B{^$qC1(xfYrpN5Y=c8LU_fnNVR{>wS*a ztI_BmunMQ94+50YKLoIPnQ;$yZP@ zWdEC=hTk>+%@XPSRlW>Lq>%0v57I=>C&PUmgQP#2l z>~pqI3dJ~9vECsJON1Gr2mwN`W$j>WC|<>;JCH)E%>PJpd5LBG^R0F6Bj;ga4t+ZU zZ7LHpgWjGfZzAD{9I6!FX%)7sv$VV%NQwhoX~@ApjZ#g~R~Xd12{z&sow>H|<(e#n zd>)Qy+G9k&3M9ncBJw11aU+=^6OZ$C^bXAl2?ZYpK4nz=9JzjS;*CqfmmDg}u{Yy} zvsOA84&ea5h4x>7Eb#v<`CZ{y1N&;NN0ab_I6CLr&U>NR9Q{!o{XDRxKbnzm)|C*w zc`p_GMS#B{_$7e%EwD8EeB?*9Q)QHiWO-!Td@!1Ahj@1MCpptZ>*nu3GHhu+XPI!P z2U716njxtJwmz3Pk_)u!rP)khEwe&OOojw$pmiR|n`U+ra z>8la^nt?4%JXZsh!(9WgKhYBTQAw_v3mMVfbxfL8RY!oI)L(rZv%Ax0PsOer1I1W z$YF1*Y3+l+lJ6nBTFIpv{qKJc^%{XCRdAvQ~{hfSMkf{Q#hp_d|eE-j4v@!7nY8 z;3M8O_=#`awJYJIvl)2)mScINWh|U-9G-qO^{4<4TRkCK!K`1bMb zbz{R*S@GQ~Gd+#?aaISV&Tv+eFaD>@1YI3~$~5CZyj0#3yY!B$29N1vmfQ3DB0(>_j#+zbux! z9-@LoTI8-lh_VoNZnunI&YH+mW8)qB&9{m1RPvx4CwX**L?3Q|dz(fa_Mrq*c0@iy zXH-Z2+iLVmX!&bm^?Ref!G3^fILlF({N6h0HRM>(xHkobjaRf$>^cnFYXv|z5V#8rO9pXufUehztTKJ%8P>;^z3olicqDE90RvqR6YasTws;Ygb^}U*m8`2vpYROonlc$ z4xJ$gTI)j#+L8MlIa{r1g{||5fRm%vd*@lIbG$o|ztEeQGlXox&m>7L{BjPLE?hs= zxUn2U!wdFVP{CvRc@+xnCXil&pYSUy~_DH=06_V|hj znmQro8x}VajbAwl8^7`r>Oh-wfh3IGxyqVJPZpX->6joO7j6A#FjD?p=N9>M*_aE` zVEG*V%KWFRYLBxFG`(hIG%M_zC28nd4NN$ni(3Bf3-#Bbf9wwosctTjSxUBCyzrx{ zX^?^(t>YR6cLMq?p)9=rjmlbhiCia2dx9*x0McPjuI*=;?q7#5i!tlN^xBben~>K{ zjo61moMm`xyv3ym`wR8D(M^aQJqVz>zZf9rqMD8w z7g%1$CuraLAxOKp1^pfr3BO$JnewfqEQFolToMf z^*j`6)IA@dN)H8?Tz!Mfv>%gzBy@ zK_S-Eu9~AlL#HDA6DR^aTmu50);jqBq+ET&w~`Uj-W$G^1^o6tmTU3LhLsV~=0wG? z%dhyzH7nzxy$|TuUIdyPkFbTvwXkO9uj^_Yu$trGP=3$9_FSvyNMOzXK(5wr*<1r~ zm%&EM5*fE$LjjG;!-jUt=jm3N-xk!CS$S~&VO~f-45+w2wVFVjQxnruj5y&y<&uv= z%E?JbuFoY9k4pmt9UZ*?rs=JNDs)Q&jnBuD8i?g;2*LjG zf}a}pz8A{lJyGKH5*a0vD{I(8ilEgkqY}{D%i&(Spv-#x0yyJ~mRe3Uzgb-z-BazO zR>?jFlm_}irB!ZMtc=Kt!80}z%|6*O7Zr%${%4^I1L^F-4nEsHF=)4aqTz@nVr<55z|!`t(X00I z0;sHZB#`9DD*(!okBZ>Y0C`AJdpSU@H&+7W1H{@f0C^RpcC10g)uj6h1KYeISwn1Y z>zk<<75Ww!`$cKmL+B^Jk&!Po_t9&!`BFI$y4;SvI~7@UQ61UYUBl2LRYsq0qfMgZ z_;`mk?QyGSoAyNT*;wPgO;D}r!PiMd*>;akVIq3_G@wW4cP6AqZ$XWFjbv!lFk(4IoEb2bW4E$SH&5xOXZUDORd@yuV;9;RD&!|aq!3Y_*tg+PWFPyj zt3>&buW3&hq+gJV=+2tm($dcL(HR;7rHZt2iRw@Y8qznGwAqUqnm~^!7+0iDIiUV# zIH z#%#fH#X^VP?GYL*$-R*DVKay(B9f=%tkgh7?i4-PEDF-s4)LLV1u(;2<<*w)hfQ`w z08{b!;9*QaMaM!7~y=X)jt^GwmauDLZ zDTddtw^y%bx!rNNA)3;XbshYABh*M<1` z)Y@vY0BUVb1V;eM-jG3u1*0|Rcq#2RXW>5*H`AN^>7UrE~00l5hd@dNB$76eGkw%1aLIt@<0`HuHSYkm_A^WJMF182C<9dD zYAPy$Abo9%`C24o8>=RblprH#a3`qc+ILscfiq_R`;*@-Vvq0a=^G3MR3k^yShP(O zlsKG#)5Zq7eIJq=A`bf2-?BuHZ62Zh$a7Zv^|xt1tP7-7Ne4AV`}I>g-ZWNRL>GJ8 zkK7)a{ebGMWKh4pT^t;XJlo&*ArDc?KQFZ(&Q1ef*V_uK4bS3?pKuyJzS&Mt`@ZCH zeKLJ2$VTIbz?S%PGP@>3)DldSW9e9^M;5Y}SJWw1r}dP*Xx^o#t{am74|?i{$JnQjE!mAqC{=nL2#x6VB~pIQ z!KsAHeW_%cSVZ7{T`HmFxG3v?77*BXDa1c5O6D&PT!a9z>sHTcR-EUrSU-&V?C1bJ zDL_vP(EI=`_E2p<4`ogFFlhXZBde#!Hg-J{I-JyPmK`Oq45>QE;|O`en@}q7On}Sm z;norWnK|pGg9+LEJnU{0A&+6~rdk?-p1}Tg_i~fr*=XU@s_}{O!Kn?CUP`O!U)k{Y zO&Wz0)jtDV#(+t&?Rkq1Pizo@ps{CATNGJC9$i}t%fz=>iLvJ8kuiN7Dl2gLV{CkM zY{S`Vi%{_1UyvYia~$<@Yv*R_jhRR z?h8pvDr#-sZ#0{Kwj&;DzV$Tq(%*`sk`a*IRO^S^Rx5FF2?7k_YLtCCA$>k54aaLy zL4D2N)XCG5);@rKV@amr@os=}j(-8Dhpp!s)V$ZOXN;U?AD9n>aLFzq0rb;;5WximK;c;UT+5^yopIRLtxtS-c6dH0VA!m}U))VzrJ^yj zXF7mrMtZFw>+3xExzc0kHkV!X)##6Q$-wVFhxzR&gyj9_G%T%MfV|9fAwZewB7h3) z?*phP_HPE&u4l7B_Z!r|mEZ>q%+H-+-F&I6>x4<<#Bg-`eupCYdZMuFjf%-N z=Wh=U>Z72^-MX=*S5(=uvfeQ?`|u0}a9$9Iv`+*Po|9!I)D{=A{g+UUJFSpWy#Ep` zZ~FhvlJ<#E0v9!G+P@7oA4BqSRInDqKf22Kmg$QJ2rdF}49*;Y7L7Tzw!-4T`wJY$ zURQkvXotB~*F?>^EFN^%wDtyKLxui6D0`%Cv4_+T9YtraA4VHF%10vjQ3G|SvxeR} zN4X?|?EdG_^%|7W|M{S<^mFG4b0A%X_6@#cklhYA+tJ5A!F!_$FSd$$ID%Qbdlgy? zqY4p8HGu{d;&Sj3FzNpsRfZT)QPd_>)8T5AYI{Xd{Ge6slR%Q9xKY!H`ji#wN@(qJ zAZSFfKiYJD+6w!ns4D<|FHw}`^|BH0`@e6Ab0#0eFSQaWfz#IN;i>81KL#k^7@$6* zYkBV5UTHZCSD1m&Zg6c9{L{883@^(DJdrsAv`-Dq{hR`*hnIiOiXDfwQyW(8RyOlj zhCoEcju5=rO#{I`}1_tn=f) z1GvLtU#_rJmq{5a>&ROtyzmP&L{@RRq)#a7VGhE05tor0oa_2l%s48p!@BAxzcH~ju|h;o2iOR+X^MD zZB2<@JM3cEOYZ6(TS2RI?ag30Wd9W;>W@dBlWBb~fSgS0dmA*chB|u!N_P>2xOnGC ztKxyt0}v%NZ)!Gxn=}tV(r1Z_y)nGzD2y+`2R+%HyPzliFjg2^{K2c*W%>~;mL6y{ z^5-rhYlHx;BDVn zx4T-q!X5HuU@hB{4b&DQX#H`PNmf#J`qCXkgLMtyxahHS;TC2-$l_$)EvUBo8KwW& zWJu87q00kp2vetkvNsJQkgYhc*5Rm{R_bKK8AeCM9a7+g!tF>MrtUv>fu-?L%fLD0 z%NWtInt?Xzd43xg`N^xxxqjG^tLi43?gT#C59lC(2Ywuh=b$FJX+lgek-#&KJK5;K zsE6bYCRUw?rhclg?{Ar8udvqEX%z#_jNRtyKAMHmXm)WEnL%1>0iZS$quJ!9gM|EC zV?6M7Dt8eiQm{HGf{P>g%m_XUplq@vf(J+N*%3U%Ko{elV_=Uxq+%U3JaArEGtl?t z^>ifrB0zP`P;oeCW9l5Ej{|Sud_ZAmnKZHD0gUK@a{^DYi(?AkTX{r0cY>$dRqYH8 zm8~dB=mS?6Fz}uQmL@)Y1?8uEq2B}Vv4mD}_sD#-2H~b(gJAxfK4U$;-w8)S6FgW` zz)pv>e4=6YCk}WG@GXJ*3)zOA@S+I57@$Vy@(7Z_Kv0_&uNn+OnxVGXsYWFzbF_wm z@B(We<{)lax_czCYavKQd-9QB|1R+7+{Ogmae8CVUW&Zp&dUJSSb8MD2BMFqUNjxJ z*%J2?dNpivW|H-mc!|~NP@4jGFVs^j96>TxvSOHa;BtJ`YLo(0+)d7kI}k}-qLwJ9cx=H+)2p$WB?f!&_ zuJubR8Mp`C7`UCaNYo9K-4hOcVo!tTM?Cde6spyvV81P?Rn9J>>cYTmomX`v6E#aU z(2dB-(Se+Qv?QC;PvY@ZG2=5oDm)>|CzLEqqR9>rh~{KXwsSTSlZI6}qm!a$50Kr1 zzrZa!qtFre)l_2@hw>7UBnG%iqg~_+e36bHIMR|rs0G*&i{Uj4S`146#GgZ8{f2d2 z&vO)q?11L*`5-Z{#y@-5<-Oi!DO=jXXZT8L!!Bj4Smk#A*y3b-zQ(SnDPNOKOxwFRTw)Hbso#lYO4! z)~8_r4Pcqg{VFN*8D{NgsHRuXsIGc-zHGkX_M2rk*wUh?m_>1S04e(X zz?qiKm!S}zWWV~2{O^&Va1Xfr9tQ@;XJKr^>e_9@u_S9ils)Q}M8rJ~v@CHd6XGka z9A3!BEt3=WmfqOpZ~~7taT%= z%KCi;8}%bC*1mpd{rbtQFtp(fV^i4~!|Su+@QH~r!zNljyfG`*tRGoDmNkpRSY*I( zRsbACQZhMe?K=FQ)$K3O+3U#Zp-GM=_*XWI6>OWA>LzQTxP>GqNWMyf11N2<6Xr|b zNfX%lF%wh6Q==2(z{-mkWng$QxoKuoYqFw)>Bzyefxj~n5e20F{tBSDV12nasbNSS z*>kWHFmv>>X5{ptX-CS2u|x2k4Jr=-Qi$S$=~GcJ2A&2`Y|RGP5HILA%S6ZX@)Rp^ zBA;5nVMG|}q*-iK7HN}x>`D*`2e&uIFtvX4jM3pSmF$x3joLks%tf;IvFoI~U8L95 z!((P>_}A>9UwXVb`S952uvyi;Z@HRy^Fsau>SK=Va@-6Q|K>KFc^E-wCn#Rnso`5b zio$FG`F@5dOsuChqMSmR%P~HS`G%Pq0TAU#79mTFMkncW&m~`bko2BeXXVNJs}hYD zcUIl|rfZTqTK(|&Dj;V2hA{;`#DgCq`Pi?M-n@AvHi zb>w4o?Ygnikx3x;;-!O&23w4q8ROqT!#R5Hhfw+6V%bkPLhUf8M z%M{K>Mpv&!T`!@?X;4XH5)+-0K4jk)Q_{PWuNPKSbnoW3s}?kt!L>#(R@rou+(BGf zNp@+D8pL5JZ8nOf#h99AJ?0%Piw#|HjeDsmWB$ z$AwNQISN>$UjZUg>oS0+NH{*WIGbakG@{vsJq+2zce;ytLy6sLGCF1NvKSF3Ae=QC zE*>_h3Rp$9yjh%u|Fb#JlPnN%nOrhS8E6AD4ER{fKoN%o z=25nB01Jafu#7ZI=$et$JBTwHuk3}O+@JtX1}NE`0&w9xcJpe$ndXVz2(!2W%4?^B z_$|hUxM*zR-;$_&azw*yv#%l4tFPq|ByUTIKwA5m<%-|-v)L(3AwsOLZdwAW1BGo_nkYm2!xHQrvwgldxvi&q*P_a&s$lU=2qhDni*N3dWOR!Zj zG@_m;0TP|VQJx0U62t2wI0jHUSqpHBg#S9g*&N!^1pvt+=>+aZtylt>STFy^0;{5P zu9iR`2_2FqiA}JIAnjf5$smqUBHeD0tk7S|h{$+-U=7vD4d&G#p9)*@9!3jxE)j7m zmxwl?FM($OG{1A)Ft`N&fzH+K3R`lnoUkctWD0)dI#j@<9JwH4(4ZyF>s6?rMQ?7- zL%-*Ee`mvw%QVO3&wu3Ny^dbDA!&P4+m0N4L2~naTx7+iXXC83y_Z1pIK&}P z$#&Nu0djn#C~tc^3N>k70#LsH4uA?s?*zE}0;G2%k$?cH{$du!4mb+Rw;f#}HVT0Y ziuL2Lz&+kE$vZ(Nx?G8FFt?ftV`q`BVs5M<8`NMU7E-3Fp$IMmO%48XfExT205!NP z0ZLHs0{9S{y&K@eQ6wZQR#;DwY*)81tUllqiE<%Mki(@`7wl?{&0_8K@TFkZhX==E zV>9&CRe#pRVo6P*8gv0IZDaxY_yg7|x4gSw}Nw^_SBQi#^Ck3<0 zxv|%XynDRIXasTgk|sNW5b@6zEG9cQO;B>MuvBs%0~$GGLJn*?m4Q0R0fmA~WcFbc zN@gF4;70*2A(87)zZb#l0q#xk1|T?@VJK!dESE_!kED%+{IWI})3sLIIr_ymyu_B! zF2qXn83hU(H066^77b~K*h6fRcad{4R?1%?#VkJ&DeKyRI5ZC5VZq!|EY^_> z`V?d#}G zq466LydB_CMtCuRY))moQQ91D37oLl-D(+I167U_&gD8{6;ZcVPZQqxM%7x&{A{dW zFo5L5%iFwGNa*b-nl>PcPj>emdA5%qXXqZF+mi$=Gz|`=or2yfzzw!R$Bn>U*7n0!5Kw4tGFM{_+@BstK8jale4NT4jQer1DZcr4# zApXnHJgZX^k8?Z@-^af}BwDCF2v9-wR{*uX`!&D@$M73~gOVBB1yy7ZX^-|4U`#vT z{?h6a2JH+#oou9%u=$S5ach;|Kn8vX>f-SC0L9@$0L9_M0C$gCMOA(S^KU>E3@GQS zfi*XwEXeP-$he?u$CW&|=r|tG^bfb!K5ZGAlQHAjX zih>N>{K1O7dpl;Pi9sNcb3QwV%=`%j;()V}z(O z?4RhXF9FSDNU@NEC6k=eb0A8gIbkX^FHlN_<`nE*#`OUx%kE2jfePJ*Qg%hsL3)o_ zvDc-!t#R+8&S7W~S9Phqtz?yUO#mNapp4wd&a_M7I1_Kg!16w{q>ai@H6%tZ4XFhL z4Zj~CosWz2{3i=ga5oZ?<(RZ|xtN8K7it#Lk++r6#v?;)?q|ZhZn$BoX97tg@e`Cu z?46XQVLzE<@V)$A%3v1wk_>hNC>i_}K*?ZdfRX`1MlKmV6{SyXr%2IL1{^L0fv$r$ z=Lk??xFe@eb)7>h{@sX1Vrn)(I!nF_z#F5J0&*dkW+!!`kTvZ7TsP%$k*=lN$mxnA z>FP(_GV<^tLcSZws9Q?(CLL!Ufnwv#PXoyWKs2teI)}WgHBiSET6+zcL7U8KKvdRW zqaXGE41{6rl1Ae*{tKYD+q^VHLXq1nk<-&ntc*DjlpNq_* zUKsOiw5TlpTF>IXnk_(<4#CdRuZU@B%Y4v?YQ&rP#tE2FL-KTy+=vn(a!nl8vdK9K zSzZUkc{8z048Ptj7Idvyvq2bQd$FJ zQ`);xDV`5fN3+X4079t6^I=W-Gc~Y1sojDb(xgiWP6}FB=~610zRMR|%dRd_SR8`n z1*q;4@7y5GnU^CR$+9RJuHJVCGdbB*xT9A}+WVlp2K6hG&-}yNd_G#`RlUwnIPuYH zhRD1W^oy4vRrp*4P;BfAP;BVzpM36bg~iM0GiS$vU?t?%Z)7aX+9*+U2jnN!{5i8i8>}i%| zZPar~x2k8sBbIG9>XY}-#VDv`< zNfrnxq5qkbbs@-TxXS>lCkA1G$5>%;Ap}^ofzVL@3{G;o&i>&Ou77)G>8^1EcMCeA zk>F}j$3rAJF_&l^BF7q+BbJ%BA+P*6up=g48NuTt`1b}Dml5{_fR__|wSoEEI3Rl_ zLvd$`Ufsz69EFpgj>)vfrT6@c)u?b=@T(mtn?gcO28|qx5*LP6oHe9J*{eoZ@>ZH3 zCUU75QBOrv&qUW! zHZ0o|HCb&B1DCE?jV8sHCDuxJq_hn@C96UbrF!=k`!vScKq5W_lY#WGBV8SnRTsA) zNyiY>THIRck3^IH=EVNUN{Rlka`!`Fe-&}C{q*8sbujrMFeh8W$wb%9q!0#{_OK=n zguy5=q}PK-Sr1oo0@tEchBR(aeh!z>IlA{|2uK3;5&ASMam-=c(Z$?SG|9?}CP`x+ zQmrq=!0AMVEfn_xbXXm(cdkhmO9{963LD%BE0K(_@0x~&vYU@zY7i(t&)Y6Vy1#KfJp+iyS zcOluKI)~#VsLrJ;V;y*zV~za31O=KQ0145vdX|-VVGfPrjs&Oo zbQ4N-nKy@Ovg|2r!ree;XXjgGV%^mn8Ovfu(X3EomrbB@&xgyy z$&kWoL>C$9DK#Lgi+=)0>EzTnvC0+-iM0!t?MBkg%~d)1#|8dCGrx;Gv73iLMJm1! zpd|MufF(qfzZsyG6K_HOF0ED>W;3=9F=DgT`)Lt(KJ5rNY!IjADX@~?g`Qr>PX8I8 zSmC@ZR{j;Gx`ad(LZ10u-d--U9D1*AYR<0~{6n?iBFJxSWc8HIDv zT4b?m(VQdO{u~P9a8a!}M<>#sLUlB9zZ5T*#}2}Xi_3r!g+`>|hXLRR(0} z=}0~my40dtlAyV8JQ4@^h=Z!wY{`j*Q!uXI_MYY`OA1E`4dG_c<;f+Nh2`bQLo59M z@;Dv}A|@bFe1eHXcI!~;K~e(=-qtprc&i~fT;iCc*(#;`d_6KFUkjaok+0;~p~{z7QsB~Z$W|9gQobY;SE#CyB?A+5RO5jezpR1YfXU1%(bMr380r)x{Q%4 z#wnu`3)w3A6wTs2Nb_%iqNa`8Blt~%3o(QoQZAd3qD^h_;R)2mTJMR)q<~83%(A6cbB9Whvi=?L^mC7<)Icv#iJUX zVBLYdB=?;N-U(213nSHjoJICRsU|w)c?G9DD=I`)$jf%x0iUW0%kFPmxmzyad~lle zLNF*D{bk&s(Hyn7|1PMD^Y0NPkN1N1g_e{*b&gY9s2%yCK+*zqjt&s9Ug}V>ijS-o zJ3{48(L;HEY=rr$d;ob4P?G=)e^Dufj(B3+JA%itae#`HKLm{=IQ#+m5W)XY>4zNn zT0JxqtE^Bh33yhX%mUcSE+m>p5Lj)N7yb0nIvN64aZ~1h0gQ%F+f7xP7izmjVNouwp_?^$?2#CPYC+)K zl$+jj7P*NnWR@IMW$vi$X#^c#nkcz9)|BHW%AcZBg?)I!4C{s{1WwZ0?9-zXA-F0h z1isUfxFTzVH@G95Xs;BMaJ&>|STB$tVPgp5=hpzMVmQ#sYT^u?)#d_8Ej5My90gGb z)wdkUp%zb32uGudI{hucLuTld*vcOUuL>57ZUP@+Da2M{su05Tvo^zhP4eZEdZt=t)q;m0(otSQ?Xhz6XE&S;=zv;J{SU=~0xs%nCm`?Fi^|3I zBCvj$cGKnLz8m&HJCTbs&Lw8{I&|Z`srEWrHCaPvTC^csJm`Dt?M$Gu4-(!KFGxWz z4Dz(0$*K+#T^s|2`%B8Bs3RX4^;ItR5wTMqk9hLkTPZILvPEI2j~4rY`SJv_w$?ig z5xbU!f2?Zy(Mmy4R10d=f~My({c1osNKudgS4#*k2Izd*pkfyC^rT`Zg27(0C6=#E z`T;CiVA&#`p=^odwxFSI7~BL9J7Fn0*`U&qH=!EGG9AzRxlLgerG)0dW8aPrx#E(N zc$y|rsH@%WxoEHm$tIR^M-CgQ5n{crKeU0w{RB>L`A$ynbujSqTcZ3pN?sEvc0rwl zwrd1;V*`jOKbfT=5xdBeMZdN!W?PAWvZEKjt7qKDp;2~9vpAdpp1Qi17+0e}gt=7r z7HMapl%AgKa_PFCVi~r^j2N-PX{& z;k(o8Qy5l0n@yhur0q~b_AmCAV~qBCh?vS}Q=a4s*xE4?@~>wU7?VF|*K6+KS<_)? zf=47lEHV!}pw^g|lRQPkJ~VO`YUE^IBPWa89Tf9H7G{Ze-8LfQUh<~8rZi%jn5Y7Q zO#53D1uC5;`B0$8hXT;(6q%E(HS*f<2goG49GEKr7S91F&dJItur7C_%b?n4qTR0q z>I%{f0aEp{`xOWik+-g=DM6%^WbHFv5PJKRy>BK@`=cZA^jv_FCJs?+pMgwsclRj{ zPg>X)$TZl^!2JrBeg#8(ItROB;sPFGZubvoN)$uxFV7k)|YF}gLizyxXNaV(j z&zy=`b}+U35-`WzYYB*Lra0W^A+O;c1W?0$K0p}{)?T%*%||=huGvoL0a#P0|1Kb# z6wk!}Ji*hcvpaYs4?ClZYZ974jA^yIli`p_oubmtx0A~yY+D`B4wQ00XqC@~Jb0i| zyW5OiA4aL&&CWlCI(PC2Ba2T8B#h*iv|i4+lo=oBNv-Tj8pUp!vx|!~=)P8CCjQ9M@`=biU6}86^zXnL`&_Bg44z!Y9 zc7@ZB8RLs|0D?)BvAIgdq%&UFLbe8pUJIl=+Lo>TC)IQ)s$@*;OUA_5E@L{v>gzeZ z98+!W4kUM>u&@Lcr1P2D9rIB0TNGMw6%QQp0E#F9AalB}-8J9JYCIx{$W>#Z@F^=W zoDZ;`0|4DR_>UHhfKFSk4@5>F{M!A%(~jbSie5;9Omfx?(;#%;OC>XDgxoDdhhMX# zE}0_l#LIn<#Cr@%c_&8eVAnuXM(t~|ESQBkrv26a6ObS7Qe^76kZ7b`NIqiWgvfm; zW^{bb@QTr?k>t5P=xE8nc{GpWH9bjx6#hIe=Y0F_sZWtk+vMVvpz7k#s{l$4uLcP9 zhv^K%$;akeT09e#CwZn%Kn1@d5P0sI8qDO-vd&4sUg(Hxk$8kii=)tF$gf2&;szUn z`a!5GPDZJua0*JFKi^UrW}A&K20|MN%*vgVrD0P6ls0#VAHzw8S>{=F6dSvR7v>A9 zwf5;aEX`3X(5bjy2~Y;K%Ane(BdZu|?Y5{uw$+xCVj$}#e({Rstf0-&Rg!QDhe$^2 zUvuC~-OekbYU~nu8=n#hk&3#=`>+5CgUM|@Bs1aUExl>-UW3jwz)?Vbka}^NCG}Sl ze7%8sU{$*erN=jlV@R1x*ZT1T#pD55j;^vrQ39jhghA9Dd;7vr}Mz$a(;FC|p`vz_*-7YKkMrpjJOW(17IqTx4Kzz9n6EwY|8&tRl|piS@%{ zV?$3!TGpt}MVBP=Pv}9Cxd2rPFPl-y9e({hl)469F3$&_^?w9XB91T$lw%X%#&5Y| zgJ&9zT$r?D815RACum`}9iBlo3j_^g#vF5K7`I@S4!O@fX#=%0Ymw0Z?RL!4p%s`e zmJY2%DRou9oHJ;^&5yE*d~UT!BvE_25{~AF&&#GU+W^V&{VnsrB>sKdy`B(#|$aeS~M@5PsFp;`3i42#~CKx&` zJu^SiH^U-CMMtqq;aXw++7yMZTmNts1sqVvAF0-)y~*z@@7w5dG!Jpy;bA&Nqg%Wa zT+r~_P2?~4`Rb*u`n3p*y1_=FxR+G^Xr(qdFsK_lAXEPcO6Ni9^-loY4%U;)w?NN! zKzGydg)r^7CtsI_e1icx>;~%}>FnAyGW7aQl}^caGDoE^A9Z#jiF~fo(}%&sW+;A~ z)?B|D9mI`m)F#6(wce$0(4aQA8c_dKC-Zd_n%qiDiyB}VX(Bn1o2(_c z8eQj|1Kdj`?0Xd1TW8V(5Vl&PE>jIzp%ed1x)W=3rb=Uur2b>0Qm@)H#l?pdy@zuP z8ezLq|0)v3sQT9pq{-HAN8xvUXnu?3!i%V*J~}6d!H*N2UDVZrshxN|`h&mY{$mW{ zt5A~dSHa_m7#!XOgDb8AlA`m~5&S>|KN!Ie8CZXq&1eCSP~OyEJYA!SrO|miv?``4 zUPWiHkZl6NYvx+2K#nm2r8B%X^V<75F-&zGx_(Yrs z`gTLv?G+({IWklK4yy0$)MFe#-!7dERWp5H?JGbI&lUUXmSq03CB^$K(;akd`6iD{ zFVw6=Lo5VkJ$^-KW%Y-Uyc_Z>K5mH%7+eM@cED&|>8B$2X#?vILChAr0AI=Xs|rLy ze})H$_TrzW)UQU-934{}TJ{JA~|FPIjaGW(2<#!T4~#xWh_2?Dq-{6DsMpUn}Z6 z5EVgn->^*JU6;b_JB3ebKV}r_S0;9QrRc}UAn_{=?zSbOvo00rvc|8G*9d+?aGs^by-hnx1aKizOxb-`nXw|%_aPYm47UsR zv+CML!b^958gF5ZUUFO{ib>}g+{Ux38tHl zBOK0Zo2*97;dnD$Yk&uXjt$z<;5e+}dX$i8dznDSnmZ5(1xl8;FX8UAP-Ue+DSl9wXRcbiA!Cqx+Uu#GO(4bOv2% zA>A#YP&GOb%&xLOcaNEvn@|Y!atu(SH_peYky>>hCJ!2Nhh$y3>n?y1mnAcBKH_-4h{_|{S1Hrd*vK<;5{+z}?WW@iQbEs^d; zyP}*Cv9Fha78OmYGQO2Np-`Ot6+s%(K?E&HS{0|F@M!z%`|m1JFzDJO>i>lLxa-Q6 zSkA6Mq3~iP=^0#Tn(u|G>SuuT&6NV8^45TH^!*Nbx(we2tW1L9)eLwe(A;AR4xQG6 zcEym_q!Zrbs56m-6vF#cS}&bG#fqIy?MGPb zOLUmJ;>0CQ(niB6x|{(z(M8#ESAg+iV1s%8%6DVe7$v9-$`4Lcd^|W!BYJ_R)ru|^ zUeFC0qCAsGq0=NfQT5}i3`A_MmK4t$K&go&5+-kOV-)-Qxs`!O{&@jzcnBXm=qWMD z4V1`hBCKbiu*q}Rau>k5Oov09MEzF@Uto$TwRvw(*^w@|pa(9^&fLeD?b)5&H|EU1f6}3e$6_o@^?9vVCNe z_HhW9ZUNJfxk$w-h`@k_vxH;Bed(2y4n zJEweU0wcyzh1>D1w5kpEiPL?X5bMD8|yP}G*R12+EbH#Ij zs)pf=cCD%-XgE|L|Xy9>XN4M25FThSJkQ;M(-|+mhOO8L|d%s6m8=? z!_;2Cu^AjxwMw?0m{uu~4b;LOAl0BF?kF zO)+KZcVYbP99@tPApgDm{?zqHw*LN16obqoi(GCmWJQx?MZfal$*0>(^ZND_$ zMy5F7ZbQWs67<9EAOAN#9S@ODu+z9ciXyPbW>B2uxMCP9sy9wdnv#~d0(|`15ct+-uP-1 zN=12%>wtj5E}ey~u(ZMRmQ+y?TH|^z_ief$^=*)of+$aE31y~DF=Jd+Rps;@RmEo1 z7nbc*RYSUUMdnS%QH7ucs4preCCVE^@l{uXAGkXc-+iwEnS&Muv z^HwgkaHB>xZ<{PB}TU_5njlJOekYPy*@>El_u8%>Tj<3qs>(yQK^a!o8^s%8g$mp)oaYq1JCaVYoK0+ife2T<;D zGQdRcI9F>t>P7Uw^DSGwz!y1aqp>cSi=)VJ2vNcTqWQ_0_@4$(s98kG>zhmDo{vGx zVW4iezkDDnIWb@~)m=XzaWwwAx8)VIWa@r2k0zr*lUl+q^6|)se&4KvPB+(Ca(z~; zE(fAM9Yr~aYZUUfcXE_F+BuXa{6Z5@a7cJ>huw6{fT`6?=Z|q%c048%j}cSTL!1YB zZN0&JUF8~ZBNL(IM5w;Ec%bbZiX355;M)V!3AVXlfuZoA zGT+UhY*g*ycgAvCIuaaYK%SfJZbJq6ye0*YzSw5hh+w zd|79ZYk@Bx;pEDLNQS&%posW%t2})bqJe(cT6f9Nx^|x>dLd2+MwmOaBgQnJ?`D)Z z@@75Z%S(qoh_0J{XU|@FO;gZRr?i`lbLt5~q;g$%K3YO3&g$(0dwK`af7vmFNzNB| z36Zl!*0M)@<`1cbbLY9)Xt}_Myi))LaUQB<;oJ_$!g-9}RIH9E4QKR@g6pwE1!##L>a!eDko+rqO1^eK@RDwJ zvuwUAh8MSyU446;G~QluY9Hyfsm-waSncniQ& zByRUqjum_u&^+CH6SpumeGF?gn#90nnVS9HO7d<%^Gt?-3#=w@`R*B#iZbAl>PKK|ZB>6zMny$Q&QR~n^P_$5}{ z`2s=bnk6pWdu_jD1u@P=9kJ|Sbh;c#TqiaVKHc*Da)7dmD*$SJawWjl0!!j4QWHaL zJZec(UpNa7JXE7K442*d&Kbwrgp3;h;|+pL=u;QVt-`+60%ez6JEyV%??QvD8auqK zF0)+6G(BoJKA+sWxtFN?A?Idvdxy($`P}52Z{>Tf!inj90HyTz1FVYaqwD~Iy!lp3 zDD38S6ASS>a|;}AywP_IP9+ZZsg|x`UsLwcF4SuqZZ@KmP_Vs zz`{SnfJWs3R1&$i{yz** zilqQ=N8fx6%5Zgeq50PNDElEW!NrPy|l&TGn>PhT;S^#qvt$ zLTzvF*I0>vzBT4Pavmn;Ft#JuymMk^(AyamO(ah907IeQ)md4218O9P8v#lVHv!ZX z{c(eu_drLSqJ3NUa!m~RJRHe6yT;X$dbfzY9t7h?G9q)yswGskf#f$;MZt>&8$Uls zu3JBG+5zE94xPfmn{mTgE1e9N;{d;f_Fn)m@Ruz4h1ysH{c0iI0K{#IWVfx4&NN5= z=@{g*z>)m8*y=;0^7EE7e@F0(0Dn*LO90&uF~$C{z|(-qQ#@*HJ{onoU46FoUvj32 z*3Cayl7%hJ&6WvwdLX66(?|)&dXUmEn#%y~n9fP*-%&=6@RE|=*4~+1v!;z|CKy^O zrFI_*vN`%sQu;TPNJ@-e0>5H~Em_%D0rD4n%Ub~sB5r1P$NsnsW>S$-%l%d_@VBW? z$3Y?`Fxt{8&YRMgttd!o%}ipFF&TREckUrj^Y;)5N**4xl$2XLK@jEFP^{r?1tfd; zx`ECfz5!77a67>G!(2_wu@ZS|1ngl~t7+|qz?AWIenlbZy)vxZtcb(H&y%m-Fs|Q6 z==P4)AcZ$ZAsRCT49G9;br{KT!9CArpezr@$TJwnrK=(n5)TB%>Ne+Hj3Kb|sv2#ItAbF2l8OddBd2``OWT9l!ET zJ>o6R<3O1aBJ&?5DSu!k_VMkp(c#Ig_|_*gJ&pK5Ru)6Hyfz6Nu_60E8EuuGUt*XS z$qvA-tEL)4zxPH&q|UVuMMqO2Q(>$R8m?9$Vev7v%DgQdD`#oGqK#rVVCY^e0Ga_ow<38M3}_(m zYiInA7}%PC<5Q1Vk!-Y#sS$FKz+~(GBjn7@^OpaRVL7ctR(o-Z$-t>6Fsa|(Ea_z8 zj5`Q{h*tH3B4_r~s$HB(l|VewGlcCzk#Pm*4j%BMs+~R=44e$E&k)pLNuCpAB*80$xdaNNYW2-d{Y+XVGtl?Uh&a;#! zZ(R1ZuJ9`63?W_cGf5H)znr7}J?4!XcazIO=zXyvnBb>9wa99{&+_3qdaaIH_aj7; zueYD~SzC#H!K-K^txGucW!9>7X_SIFiKJlilN1;UHD@JKcpCba6lMeBd{f&6)Goo$ z>*oQy6v++lSi)pd7KaX3bZQuijy=92f~Jm%`G&Yhwir!Ku8>h;czi3 zIaz34O~V8MnP}_gsHE38v&dh=#@j)x?J4HZ2jo9pReP#sAn8>jtFywsS(1jXmB57Y zxv1suzRW>!oA$96K#6WHK%O7yh@Xp>8pC!Hq`*h(m5qWsflT^1*!O_S+TA|4iEVcV zSq=dmhB>+REX#EM@_1Q{+8CzRjEviaJT^I!!HV{U6b%^<*+<NQO%&^@n^hI}s0h zy${Jfku?U62P#OIQd^u?`DS5$s^uk8ebABJvy=PSY0Q(duBoCv`;Ps&K51;iME62M zJt?<-2FxFUoRc`9yXPZ)ktJIE)D9qsgp8{ZHK>}(!2XNu9c<_=+9NEYwSAw`elEpc zKmr*Nvgb4aiTINUqD||ksF55_28fP%GST{p0it^_mzVjYsA}o$-h%*>$)6&v9fVHP3 z$Mj?7Vd5->YNQ8LJf{EY>@;{xKVNXIc#P}QXto|i#}!}c-yJm&N$XdMgCLKEw5z69 z9AbIhzKW-m{qbCxw{vN8tyA|w``-c|_L_J^|E{ntItTIlce7mU)W{g|fz!V$5E*t4 zj;2}hhyLAwUwg4fr7lFS_1{*=Uq6!{&|M+Q;*drijW7|G_9wpoh(1~mAvskJct7gc zR?6*1D=C+U4gLK--=gvRZ9#2`l?US==7sdbfQq&CN&<0CO;k??L#K#(HKsA9zatV+P=du1` z)F3a+g!eZCHCW2XAszK8@Qnr#4m0Iym5mq>ik=w@u#uszPqxej9Yk>dvrvVBE#!qAY_|X8Al-gUXCk?Sn4L9x)m~Nr!Pkxik_>q% zKpFB;5qvp7UI(td0-)BLSmNseV(n;v+ez#ggNj=T9&2DfZ%Ec&36PORw;T8^FkRL@ z5mmz&C%=)ApJ?Wz*Jkq*Wk48me;mU&vKXQUvZJ#`QHsKeHs6mniIBGi%VbUegjG|Z z{p)(vxNj3wYkKtSI3jN|qm!A4-oGB`(fFMTAx7=qoGU{Vyxc%n?#G@kj!j=QiZzT_ zuA|_}$$;CPeM&y_y81*Pd}JIcM+@T+`p>A4pA3;gM0sN04>Mx-aooB}#K#O`43oHi zK`Nrl)Ty&5A?mqKOYD$P4{l`=Rab!Q6w_5x8NxcKH$MMx!U6R+z(CD40guhBWv&Yy z`#?XviVh<1#QwMSsv%=twpy_}M94&-J9-f6pF|g!68g_Zb(Erp#UOhgs?Vq5_B1e6 z9K9DVl=QPa$VZBMn^o&Traz$fRvdbJf{FvGK2!sT?tgPdN0sN4$zZm)Q=i()tX;$Q z)cEHDJ67l1nflGGh4k*&zLZv@8M6sCIOWkfO3USQ8RA}z8pX@kL=Yj(m7Zi!zg>m( z?{s1WdijUm7Z-0?vI<~-3ecd$p1Dz(0UhelGzj$mPXzUF)z|+?R%5oHUuh}WMq%|m zHxf$jg(QmzzEYHkM5v?;FsXrv+$nm{S!AS-pS0ylqW=@X43qY&EaMNG?1%uW;_<=b zsLERPU+-}?SK{VRF^vEQIOS*fIglY zmqrTdQTqH)ZC0%>L7&3X9&-=m1Lu8xv404s|3OqI?~lcwG<6?ut=!id(EsG=%5Q(da z&K4Ny8?czKMMAczs!|XYCE#TjTBJ?o~iFsIiadwXK~1FF*! z23B;cihcI`pLVVxO8Mud_QTm}!0UKhVWr_&obmCk;p3a_1hwx=9@i(+Cneu2uyw@| zDk>qOmgqD&mX3wgRBa6P3W;k0Dh^`V=AOWDm!oYQm)UK8?1`gxW}$v5BOYYME@V%B zZg{=X)OyNZH1Cj8#|_E<2RU(*lgp&bVk`l&S<4LeYGKo@&ge!l^jQe$o zgqma6A2{ ztmz&Gjh{BMa%%L9jz>aa-d)XZmLSytc^si(pN&$1=Kx${54SkH%#3y8ViaXIKM%Xx zM9f;^rrL12pp|^*C^s6Oc?+LbjZcgZO>S84xwM)Ad*9q0oiyBc>T~ym&HVrp*|z5` zIy^Ba0zu=3L2Xg&nqg%#s=_ky4VJO4d3j`XoC|=gz~zt8@ztZ_qf=+;?f%sm7?f1I z0L=$Zbqov)(Zmnd`4zhzz@m_eU7TVQ^q~@04EpPaN7qkxe}~%cypVK2MXb$7jArvO zJK~|_ThG!c{jE3{mEKBFDE034W-E7b2@DM3YLtCCA$>kbV@R$=1@Se1UuU0|v~a%L z{Jka4JuU_)lq`b+XvjS}(vd+~8t_W#MBaWZ$13 z?Bhc~VzqWcu&=$t60Ry*2-B^d*mSmm1Mth%PI%&-9~@a|K1v4ufXZ2xxa(O8V-S+O zmiGV#HX#cZ(q|T4qHnX}RH9vneVy{;9f0|u1-HR8!Mn*TR5WV(OdW`^K^n9gV&^wV zj$znbcGXv5Jn}8z4_w4NBM&$qxTs+%@4Y%TU2b`&rYj6|f&EH=iem3FsCEaNy&I*Y z1m9!Oz*`8u*TDRSF74(gO1qAkgipAm+xI&Z@z)cDL$^ylW;;>k?o+d&L7gtn-MV#4 ztEhI%%K94X+O7P|sNZ&|&2!RJiY&via zYCeqQBdB04+&>FX5H7V$Upzo?5r96}<$%})acXVZWe-JvZ!a($d)MjNpdIE`T@$s? zXYru3rnM^&8!GhoK{+A~iz93UhlcWb>h@~n<6Q#@yfPU1jSXOUQ&^uK4z%Sqp)YwmC)J^AR|HD2yio{bCW?% zP#*`#&z8}yXyUc|fl7zv*X@{3jyF08JZJZtS*qpc-GI!4(<%7YsCW+pg)rjzDM80@A>-k~NAT2Ie=={0Wf@$(e(?gQx_*6Tv$pnBdY%C9LlPLE!fc z%5NZr?-N{TDZ7bBu}+oK2!)}7k^zW;zVfA0deix#Uum7T=;2@LGpxyW4`$~@H@}geO8nTYTanM=zKh`l9Bt)jT6^7 z)IYeNg$Qv4KHa0 zk9hA@I^Y|yVYs%`^218T>ntG~)Ld#@@x(Qk*gFdcadE}ITw!Tlvl&4oiX`FC%O!QJRtArqXQ}&fQshNe>r{x>g+54uJ2t&FYca+t#Q>QKep|p|J^l@X z=D=+Lb*YJ7hET)zS4(fzbYB0~55WRFbM5|j3`gr#s^{pUPn)YU( zEC(8cMEz;Vb26>Z2E<)NeHQ}H8iqs^8vnAsrvB@woO2;g|&8tIpimyYXw@O zk|{rz)Sqf~$x6yjUpix`*RILihff3MgJjsb5KvJ&EU4b%XOw|s6PKXA!;l9Dz)YPC zO5dFK1hN$mRq8NQ%_V$$-hm5H+9m}|DB6zH_W^h;>f*Dl!Hd{0#KC!HaDZ*^wrpJF zC$BE&CstXeYoPsLP8Rn7DY)+7MSvQCULt5tetMLg9CxzOq9}*t4JKAy0(wC`ds!yg zE3C0~T17$KvD+B)(JXkQ>BT9{pcUu>hcqjyO0&sL2MIaWtAqbc;VvRN!F?mRUj+A$ z;Bx^=CtOzxTpUXejNtPObTRHA1AFWtql5=932O%0zFdihWM2e00Yps;F4`sMcTEV| z>6kKykJ9l5F9Q^ImWjfxco1VAyeRa^?xIiG2%lJ=J7V`$J)?)pRum<)flnAP_zu`q zV#A*x|1?C5dyr=x(2DLH1e0N`^J@^ye^Y0z!}mL3D8Pm%Yj2Rcv}~eb`X>(h8su97 z^%t=X)&JrMz67AW^Uw&ggTWv+EneHGSKRFuTO3p)u6c8`ptpum9bzS64&s)jb3|gh z7J^jNCm#t8JOGkpLYyE=TPQiQze8Se=Vbu-#zg%{fP5;XsTWNLe}Y2&gkBAsoNlsi z6;gkx)oBSrhC3JPsTPhP87o;jOg(Tpu3KIJhgqGR74zYph7@9&_*9|%0Z8&OY5$0RmPlmAVB-u-}%{DhKL!VPLw!t2&a2lBE!7M(oPb0iVR4 zGXUcLJjvjU&-}=BLX=M^S(ro<3OuS)VQt5BEG7-Bd_qn#Qq;_XN@tak4hkJ{UrjMq zamX(bMZ%DsUMK{;NT)ZkIMWH0jzsOrrMv^cDg6_Fy1=>(V;#?P7>C@#(QpSxlJ%mj z-exIV+QDYrXTgxy?w?y6_a&j74Iw{zzNM1zuwP+f;O@IT2FY|{M9`WYrpjPY(?b34 zkykLl%;MIcuQJfBKVOYft|#kQ^t%b~M1y9{hW*x00=P?DH_pO}wRZg?O9$6mqE!NT z<7aF1F(t>j70%LG9S|v1CKW5JLp~{D44bF5OSQgI0tTk&< zFjy82hBmCO{fs!4WDT$~tIv{%I1ADxPGv$o-pXNxeB82r!rsywUB7+=b|@3Gy@?J1 zGkaA?%O6T8+uhsospv?1NqbV#i-4xjNC^`uS3ROM2#MEMTB2=;Z!=)`>M(5A~9P;Bs9AUDYwkpo0T_rPde$$U&lH5*xa06v*bTsWC1 zmO;E~v7KxnhHB5k(1;-ko$*UiSXxJos>ud>!0CM~kK