From 273f78d1cbb817ccc98a7a92a45bb69d900f3a7f Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 9 Feb 2014 20:28:55 -0800 Subject: [PATCH] feat(builtin/num): prove strong induction and other theorems for num Signed-off-by: Leonardo de Moura --- src/builtin/num.lean | 150 +++++++++++++++++++++++++++++++++++--- src/builtin/obj/num.olean | Bin 38268 -> 48176 bytes 2 files changed, 140 insertions(+), 10 deletions(-) diff --git a/src/builtin/num.lean b/src/builtin/num.lean index 79e6d4216..3c4bc8e5b 100644 --- a/src/builtin/num.lean +++ b/src/builtin/num.lean @@ -67,6 +67,13 @@ theorem succ_inj {a b : num} : succ a = succ b → a = b show a = b, from rep_inj rep_eq +theorem succ_inj_rw {a b : num} : succ a = succ b ↔ a = b +:= iff_intro + (assume Hl, succ_inj Hl) + (assume Hr, congr2 succ Hr) + +add_rewrite succ_inj_rw + theorem succ_nz (a : num) : ¬ (succ a = zero) := not_intro (assume R : succ a = zero, have Heq1 : S (rep a) = Z, @@ -103,6 +110,12 @@ theorem induction {P : num → Bool} (H1 : P zero) (H2 : ∀ n, P n → P (succ theorem induction_on {P : num → Bool} (a : num) (H1 : P zero) (H2 : ∀ n, P n → P (succ n)) : P a := induction H1 H2 a +theorem dichotomy (m : num) : m = zero ∨ (∃ n, m = succ n) +:= induction_on m + (by simp) + (λ n iH, or_intror _ + (@exists_intro _ (λ x, succ n = succ x) n (refl (succ n)))) + theorem sn_ne_n (n : num) : succ n ≠ n := induction_on n (succ_nz zero) @@ -192,12 +205,12 @@ theorem succ_mono_lt {m n : num} : m < n → succ m < succ n (assume Hl : succ i = succ m, have Him : i = m, from succ_inj Hl, have Pi : P i, from subst Pm (symm Him), - or_intror (i = succ m) Pi) + or_intror _ Pi) (assume Hr : P (succ i), have Pi : P i, from Ppred i Hr, - or_intror (i = succ m) Pi), + or_intror _ Pi), have Qsm : Q (succ m), - from or_introl (refl (succ m)) (P (succ m)), + from or_introl (refl (succ m)) _, have nQsn : ¬ Q (succ n), from not_intro (assume R : Q (succ n), @@ -252,7 +265,7 @@ theorem lt_succ_to_disj {m n : num} : m < succ n → m = n ∨ m < n lt_elim H (λ (P : num → Bool) (Ppred : ∀ i, P (succ i) → P i) (Pm : P m) (nPsn : ¬ P (succ n)), or_elim (em (m = n)) - (assume Heq : m = n, or_introl Heq (m < n)) + (assume Heq : m = n, or_introl Heq _) (assume Hne : m ≠ n, let Q : num → Bool := λ x, x ≠ n ∧ P x in have Qpred : ∀ i, Q (succ i) → Q i, @@ -274,7 +287,7 @@ theorem lt_succ_to_disj {m n : num} : m < succ n → m = n ∨ m < n (assume N : n ≠ n ∧ P n, absurd (refl n) (and_eliml N)), show m = n ∨ m < n, - from or_intror (m = n) (lt_intro Qpred Qm nQn))) + from or_intror _ (lt_intro Qpred Qm nQn))) theorem disj_to_lt_succ {m n : num} : m = n ∨ m < n → m < succ n := assume H : m = n ∨ m < n, @@ -388,7 +401,8 @@ 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, - by simp) + show simp_rec_fun x f m1 (succ n) = simp_rec_fun x f m2 (succ n), + by simp) theorem simp_rec_thm {A : (Type U)} (x : A) (f : A → A) : simp_rec x f zero = x ∧ @@ -417,19 +431,31 @@ theorem simp_rec_thm {A : (Type U)} (x : A) (f : A → A) definition pre (m : num) := if m = zero then zero else ε inhab (λ n, succ n = m) -set_option simplifier::unfold true - theorem pre_zero : pre zero = zero -:= by simp +:= by (Then (unfold num::pre) simp) theorem pre_succ (m : num) : pre (succ m) = m := have Heq : (λ n, succ n = succ m) = (λ n, n = m), from funext (λ n, iff_intro (assume Hl, succ_inj Hl) (assume Hr, congr2 succ Hr)), - calc pre (succ m) = ε inhab (λ n, succ n = succ m) : by simp + calc pre (succ m) = ε inhab (λ n, succ n = succ m) : by (Then (unfold num::pre) simp) ... = ε inhab (λ n, n = m) : { Heq } ... = m : eps_singleton inhab m +add_rewrite pre_zero pre_succ + +theorem succ_pre (m : num) : m ≠ zero → succ (pre m) = m +:= assume H : m ≠ zero, + have H1 : ∃ n, m = succ n, + from resolve1 (dichotomy m) H, + obtain (w : num) (H2 : m = succ w), from H1, + have H3 : (λ n, succ n = m) = (λ n, n = w), + from funext (λ n, by simp), + calc succ (pre m) = succ (if m = zero then zero else ε inhab (λ n, succ n = m)) : refl _ + ... = succ (ε inhab (λ n, n = w)) : by simp + ... = succ w : { eps_singleton inhab w } + ... = m : symm H2 + definition prim_rec_fun {A : (Type U)} (x : A) (f : A → num → A) := simp_rec (λ n : num, x) (λ fn n, f (fn (pre n)) n) @@ -553,6 +579,110 @@ theorem mul_left_comm (a b c : num) : a * (b * c) = b * (a * c) := left_comm mul_comm mul_assoc a b c add_rewrite mul_assoc mul_left_comm + +theorem lt_addr {a b : num} (c : num) : a < b → a + c < b + c +:= assume H : a < b, + induction_on c + (by simp) + (λ (c : num) (iH : a + c < b + c), + have H1 : succ (a + c) < succ (b + c), + from succ_mono_lt iH, + show a + succ c < b + succ c, + from subst (subst H1 (symm (add_succr a c))) (symm (add_succr b c))) + +theorem addl_lt {a b c : num} : a + c < b → a < b +:= induction_on c + (assume H : a + zero < b, subst H (add_zeror a)) + (λ (c : num) (iH : a + c < b → a < b), + assume H : a + (succ c) < b, + have H1 : succ (a + c) < b, + from subst H (add_succr a c), + have H2 : a + c < b, + from lt_succ H1, + show a < b, from iH H2) + +theorem lt_to_nez {a b : num} (H : a < b) : b ≠ zero +:= not_intro (assume N : b = zero, + absurd (subst H N) (not_lt_zero a)) + +theorem lt_ex1 {a b : num} : a < b → ∃ c, a + (succ c) = b +:= induction_on a + (assume H : zero < b, + have H1 : b ≠ zero, from lt_to_nez H, + have H2 : succ (pre b) = b, from succ_pre b H1, + show ∃ c, zero + (succ c) = b, + from exists_intro (pre b) (by simp)) + (λ (a : num) (iH : a < b → ∃ c, a + (succ c) = b), + assume H : succ a < b, + have H1 : a < b, from lt_succ H, + obtain (c : num) (Hc : a + (succ c) = b), from iH H1, + have Hcnz : c ≠ zero, + from not_intro (assume L1 : c = zero, + have Hb : b = a + (succ c), from symm Hc, + have L2 : succ a = b, by simp, + show false, from absurd L2 (lt_to_neq H)), + have Hspc : succ (pre c) = c, + from succ_pre c Hcnz, + show ∃ c, (succ a) + (succ c) = b, + from exists_intro (pre c) (calc (succ a) + (succ (pre c)) = succ (a + c) : by simp + ... = a + (succ c) : symm (add_succr _ _) + ... = b : Hc )) + +theorem lt_ex2 {a b : num} : (∃ c, a + (succ c) = b) → a < b +:= assume Hex : ∃ c, a + (succ c) = b, + obtain (c : num) (Hc : a + (succ c) = b), from Hex, + have H1 : succ (a + c) = b, + from subst Hc (add_succr a c), + have H2 : a + c < b, + from subst (n_lt_succ_n (a + c)) H1, + show a < b, + from addl_lt H2 + +theorem lt_ex (a b : num) : a < b ↔ ∃ c, a + (succ c) = b +:= iff_intro (assume Hl, lt_ex1 Hl) (assume Hr, lt_ex2 Hr) + +theorem lt_to_ex {a b : num} (H : a < b) : ∃ c, a + (succ c) = b +:= lt_ex1 H + +theorem ex_to_lt {a b c : num} (H : a + succ c = b) : a < b +:= lt_ex2 (exists_intro c H) + +theorem lt_trans {a b c : num} : a < b → b < c → a < c +:= assume H1 H2, + obtain (w1 : num) (Hw1 : a + succ w1 = b), from lt_to_ex H1, + obtain (w2 : num) (Hw2 : b + succ w2 = c), from lt_to_ex H2, + have Hac : a + succ (succ (w1 + w2)) = c, + from calc a + succ (succ (w1 + w2)) = (a + succ w1) + succ w2 : by simp_no_assump + ... = b + succ w2 : { Hw1 } + ... = c : { Hw2 }, + ex_to_lt Hac + +theorem strong_induction {P : num → Bool} (H : ∀ n, (∀ m, m < n → P m) → P n) : ∀ a, P a +:= take a : num, + have stronger : P a ∧ ∀ m, m < a → P m, + from induction_on a -- we prove a stronger result by regular induction on a + (have c2 : ∀ m, m < zero → P m, + from λ (m : num) (Hlt : m < zero), absurd_elim (P m) Hlt (not_lt_zero m), + have c1 : P zero, + from H zero c2, + show P zero ∧ ∀ m, m < zero → P m, + from and_intro c1 c2) + (λ (n : num) (iH : P n ∧ ∀ m, m < n → P m), + have iH1 : P n, + from and_eliml iH, + have iH2 : ∀ m, m < n → P m, + from and_elimr iH, + have c2 : ∀ m, m < succ n → P m, + from take m : num, assume Hlt : m < succ n, + or_elim (em (m = n)) + (assume Heq : m = n, subst iH1 (symm Heq)) + (assume Hne : m ≠ n, iH2 m (lt_succ_ne_to_lt Hlt Hne)), + have c1 : P (succ n), + from H (succ n) c2, + and_intro c1 c2), + show P a, + from and_eliml stronger + end definition num := num::num diff --git a/src/builtin/obj/num.olean b/src/builtin/obj/num.olean index d774427e4d3b1f6bb24c927b52f3b2fcea966c07..d904b9b9a9096fff76675e39288366388408b978 100644 GIT binary patch literal 48176 zcmb7t3z%M2dG6l(|L4CVhBOGsr9hAgQD})&MB4_@K-3sQuyVNQFi9qpfn+93CJ>Nf z5v^cAg9H)!P#z_sNwlJ(f>JIOg;VMM39VGnr=HW3O0hldL1P>0`QG>lsW}V{`<3pP^PgXzxpoyXYinU|o zV^ddKOF2QaSUR=|-C1`KWetVRZ!oB|iY=J(Y|8Tan4JTfsF9+=h%t(} zs!0O}Xaj}lMQyGvN^8fJ>vf5Wcx05XQU$#X$klMYzs#Qhoxf;)(IBk16Orn2@g|?>{W_#-UQ!Coa8W; ziJ+(uZvf)cJkIln#z%%OGIbq8yRpgi!Yc$?7Lo-=X!*wxCQ>Y1pMv7e1p8HEYAW%Q z7f^&l!_qu0eSsf17d7fz5oESJ5L7G9nwT&KQs+6dDe(#n%Fc$7%}0%$Z^ETlaNoC> z00f)E@+36OWtDw%JTsOXCnWL{0h7I{S{K7EgE>rxcNO88M+a&>db zT(0hQXcVTCQC&(*bE4IubsY+hpG#7xM_TtBbOrjGZ{M&HEg4pu=aI-aZ5Up^eq_^> zNiR|>fSyx2@nw-8$j$(-%t5HnihVqmw zkax|9bJ<%@tku!^&f!(YJ^pdrN>nxO9gLyu!my!@lOt<*Men{XAl74|A4~A{+7R!gmEfC^@ zou4WvSus>KO}AJ&v}xVMRpk&z7>3`0BJjh4BpRT7S@vlZoVM9ZqXiY?!Z5nCt*v5J zS&1!kt2`9Rb8c)W;N&o9p=6+RpR-(yelheCRg0w~SI7f=!PYQx#Ud9VBimOXNtQvR zpII0Q-qh`&4todj}*BJvVcAY16r_nIYs3Z(c9!UEQmTNi_Wjpd}XFPmS`9 zJ$AjwK%Da`?bk&tjM!DSk#C1k8_4s$tX>J2e`572RR6i@T);=Wg{{{+A#izllXJDJu+YyC!Qun*O;tF^SK^q8y-!t;6corSofsFqPs>L8e$Mcc z=U;vZiSJfSoF9S#+o>cwI2OfR^AMH@_yA2dMBcRmQMMlgN!xyE)9JXDgbu2Lr|}Y= zQs5X9zDT@d?dpJd?5gP)In5p_@DV`0wORU9N-m@}oO3t9DHMyOfWKMJ zkLn79`2}cgT2LCf!jyyOGQgg%Oz_bQ_Dqa{pG2`$pu~TUvg~u+9&u#`Hir zMX{2r8yW+C`y(H*oP3R)@Jvh&fdVBH`5Mno+mtK?bbf)wO#@3#=ofJ9cxJWy&XhO%$(4vV^srip=eboNIUx8N1C#ox zDyQ~~g1x(mSZ+3&6k^I3Xi`)^3#{7yF~Rv38XqR+!%+Puia)l(0kKg)=y|mC+xOd5 zEss36Nl!LhB|a}3ONN2QgkxzisiGduvFq3C`d|ROE6AAQnIg*{MVG|$Sg1aZs<{6r zR?D?V|2C@MVn2!1@zOw$M=Wy+NHQlyFM+t{ zQ2fve7a>a~KVmIla%t{6!&#KEdz`M(8;N8b7{|5C|2+lNTd5V_w_5&_X0aSi`A?KR zL6~lCiUaiEK;DVXD()=Cm|Lu%yEWbx<5tzIEUAW5RHf%_JXhrwl)ADfy%)E2xbqwr z?)`dTuwgayR9KQTKSn$0!e4?~b7BfpzZeA2izw(|X#hI_GVOvkZE&i{WiV(>X?4Kz zFWq9r2Fp%?0@BMDkdatz&cHjji>?dvK%@VI7VTEyUGHJ zSGvWfL@1z>Ga#Zk%&Ay$ShpBo_HM2q;t+LZkB%&`Xy?l{tD6F?&q=NW}dMTtS_Qy|#$qIez9 zaJwvw(l4XiQS??W_*y`1MPW-FH{zw#As`lm)|Y=Y@V{694KJ9xg6RZME>8(cd#xi& z4ktHEj8B;6hMdD|Z?9Pkfft8Zvx@@#3DC;IUr<#RUYtoPVc}uJSG)z6Jr-V`AJb=* z77nOh+deN9If+TLes_$4;o5OiOxU01@-lp;#KQaZ5 z$>__*T^?VI(;D8{E5~A)Uw&~et8n(kGApt&kUBYD!I94cNPNe_a@tss4JDY*qYcFS z6pkYQ*|p!x-3`Eef%B8eRK>aA0fpdH1eg1rsgpnVT0^lB#WJoF+U2gTR&DiVrt(jK z?ac=54)x5z9YfCaGs~7~`uTu$$@KGvsxz7XtpJ(H^sT#C(i70l`SprCC|kCljH2K_ zSqlD>ftw8AE(f5EP?;%`ibR0=KsAj#DfQ!SP(6hLShRX#DU*S`Zp|@I$4h?3o8G`b z4&IG2C&ubDKzURRQ$BB}#c6oorH~A9x`a>zlHi)Z(g#gp@6YaD!=T z%sz5DHBFs_vTH69u;P3mfU}K~KQG%~vF2E|mOOxqO!uZ|WcH+Ig3{pp7~mKCepOZ6 zp+hZu((AFo>c&dGLwX#PhE6zHrBldgl>wfOR4=U*^c0j~d7_seji$&I^kiSraZNzV zbWWN}nyWSUSu6^(7GLbw+h?h_G#Qt>N^hNiV$kq+vViDv`$=8%cV_+<{3QNhP0sl0;0k$}zOgFsxvx93Ne+n`^P z3Wff8qnnO444p_VKAHxovZ~!y3t=M9b$pO87&%RidZHAM2NE(>W4O%QlO!jU|M1w*T?1jh*@_x?Tst1iIG=M*vCfj#5rKfe~Mm* z2pMn}M=>rwX#=iou4jci2c;tkHv;o#ODjP5t6cQj%~+;iv{u-RS4cfEGNK5JxwoR= ziEsX1RJG>!p~~aTe8_6GajuzM)O{zcw>Dv$LH`Wf5J=!3QPQPnN1?%K2_#{EwFw@B z^1hnO$;kvk0b*{s+Dq)BYPHj>6v)T@0)c4`$zF@9)-{T%*0s)RZe3$&-72y$XGt<@ zWZQ1kyb+DqMU--R#e*(Z%fJRilu=i{%kl{HOrW?r)u1_pXuiRUJ{v$=g;rT>ZIxH0 zY=1yNeF`pv%I?%_W+3VM<(Nmr(Xt1A&;?} zCU%X^YCTqKTL-5;cLm&BRui*CYYW{|@R^!A>IXO{j1&%SHh(#TQR1q9(3OH`4APl* z7gX_m;B}3taqYILN3m*!-|q*C_63TNM7ewpu)q>u+FJ`}+9T(DHalhnPckA}@AJrA z50E9edwDzwh}xZsV5t5f8sd)^GW-M0YUAeUeU@0%Z-He*wET> za!*9DQAKof9U74RgfR$=&mU}-TP)M<4K&x{UbR*8bcIdpN#^|Nahz zrR*qm+l3Dz)b1g@@K3dS22s-7IWc>vAC&r@pcVH3kQf)UQ3)}4<02pRf~($7CA`tP z?15VV++;I#*zMo_Uc$4eG|y1A;sYI{ zbM@d)Y+UJ2{t>ET`z(-fpO=ZHMfMI8Xfp!{DnZ**_UBib{}fR6(BE2n3N*ly88vR& z>6J31UbTNE-!8%kv5*fBNZ623rejU8pDDiMCaBBAO`GS`o_UDzt=6CG{!-9jJ65OM zZ^LLBSM3F>xg7=79}6n(Mn6yZNp$fkG%iIW#GX@@`C42rv46FfJwM!Ti9jg$AWn|h ztxe<-+AnnpRMvE~=&yyD5ANhG_XM{aNNC`Zm)DR5XaF7ByKymYFB}$gyY*+fs|C&H zUD(>CP;Cc~ek9}dx)oB{e4%?Z7=5B$c*Br7bhOUbB|>AsQ@a!c#VM^nUXM0kVO+fi z#)RwaIV{aT!8D8u;|R(-t&k?nvl^+$o`deW(UfpTPlP9mN3Q63M*10QDanG!5p3n;cv6C_sFZFSRxwk}LoEA#%!8|Bcq>)E`tA?0Jd_Rp*cgl2-bO8u1N8iVS; zj$)D5i&{o?xWif<5{@Jg=yT`*PZJ?f{S>eFwPbV0`!g&^V=+lge!2{tAr74sVFOt| zxwo4z+Gm3{dz8uknh6DGL=;#zAH+*%q{rZ7qLQku1-#M5)E80ia9yHkl#QGSw&qv^ zOVJ=cpb#Sgf5WxhRB3J2mEYBirM>`a0{PT2f6m)wZoFR}ePR8LUgI-xOr`>Ez&#ze%^(&v}>2W;~yL(BatYzdt%;B{o zJa&>#96_Se_Ee(pj-~)@^rZ>P86*nxO(p7Za4nK3fEee4*y`u^im}IO0{(3%=p9JX z61m3DS}R{4vExg3ADS&FcB61f)eh9@C1WOmhxNm)5PP*uFGtsC9%vGS>nBeKCII^NC85c3abRR`4d5-_q2%sArY-D=U;8ir6@ZbDf+Ik~GHF!%~SEY4*p zX_g}{e)53Yy0Iu0Oqfuy}Q9`D5 z9NpG$C4N}DXe4G@yRJWto_jG}XmmKDkuB?Ij-)|+qa(oAKaE9&>mHZEq450mZ2`-6 zND~6DWBw@9s&4}-Sp>Tf&g)tZh@_Jc5o)A~)4Ctc- zz6&7U>g6pHk@Yyb`4*GJLR$SQvMEosz`qF`4|}TXdeercz{gr6dbA&*NbO|_8yC&` zEzFvn+7!cR%$OS-i5c>bTT$n&P;Sp7D~9PvEx1x1+SGpx@c(Uvj_tB&dk*;8rB)Q@ zwyex~YNTD|JtXa3YbBS8Q7;FwvbK6Y1^_|+EPxOtv_tS`Ki64H)!EPbkqsM$Pd(uC zpHFbn_XEFs0z)4_WHYtoe`MyB| z*LmkYt0@p8wrDL=({^)}x(D!efQxtEKvleZ&}xo%5201}d7#OzN^R^vQRB-`fnZ1{ zvs(~$J18`gyLvGLMv&*8Ozy*?!^|lTpSC*)jPDoZkAyjRpro_xM-9oqvEDIdvoMWk z5)1sC5jAA2j;pBeVP8g|f#a~41wDs!fgo}sJlU7G{0s`_IhG0`>OmKs)dx~5f#ym> zp@V%#z&wRlP6Vt2$6JvvsH9t6wDHFb%AFiNZnfesy6{oJAlC7Fef?9iHp%NCH!H87>ZHoe041_FR_0EBcAQ$mSD#5^xgxbHZnSr z(iS5eN%4AMH3dyxfe;QFSi>5wc_2|=0HX3ctZ+!IHn1AS=zJ?P4F|mT5yYg_BdB2& z9|EB|Yje{XB2kC5dH`%7>s z%STX;lMq}gnEAlsrJ|f|;P(L&Vj;t;-j|XNRrM>%V|VOg|DU0%R@@7!jnnkvI|12Z zFa3nT0v(P@5{G6;PUj-BlrjI;ZOV3Ie94q-o zR!0Z0AY|a~uy9WpwIW)$Oc7fbielg%)UcJ0&$PpW`7r@ez^D`!(k)BdGW} zgx)Ye@I}l|IY#bx8q@|Ucx7ZWX_Kd-IK{JgnuNuJ<}ZVmS<;pPX2+3cRjvn!#4&$r zV=dF?wF3`eM0ngINqcofHfLcCNZ?)!70NI-wGv1Ks#poP6y3g}@+4_v{xX+8ZCWXw z=t(9%xlo0~?QiKHA(Vk9W=1L=Lcs^V8_~#--mnrvIfm2>{3#tT42v)W-?N&1N(0x2 z`^NuiwSn(Y(Qz;k-L=y@BatkWjeu}>^AF}y+-?OEkNRtq`Ti6=VJ|Ksp6a62-5ig+ z`1EE?$1=rf{|00AP!(Liy&YtwIE`f~|Di*WFW^%xmHkbO%wDp81J9%QF)nG#WQE^s zgJ=ITy$H zOLTk4|GxkxUhlQaz|V21JHCPp(*bDU=Lzpd2`|E7!kPP4#XEQcLgEMZ`>!Pt*x$g@ zwA78-3+TcO{KSN$5jAQW>mK--6^)EkjagMVK8dA8;Fl!V;iT4H`!`VDq;f-XDgME- zBP4vhB4QHw!!ZNY!C#V{EXcm?_DqvKBRH~!%50F(%1C-k?9z>ldN5}lXQVo9N?Sm85 zy`VmuJ7`6tiz=vX9E9R16thV6Jf_I*u-HE;o)O!OX{KzjW!i_dJOajiVu5 z-BJW@(G&m~@xzTYo$zbTyQGMI(6mO(H6)Ql3sIgHiPbMB;xZ-xlb8oI76N)E>%Io? zl;_D-Y4FxBgBMM>@oT-98!!+S(au6lNKCpBZgz`!j^rE*6COf&8>f_r2mTY?B7x!y z_qH_=?k|X95i^U;YJpfr?FEda*aD6~5$|QHJGEKf8jFXA6)Z874cLO-h6dsWvp-o5 zRinyK8?OW8Nhms1`l@c|g0oWyvVM*gI=|(y9Z$VQGDS#+{5D0-a69E(|E5Q=erF9Tvh;)Yuj(rR{JvUaQbhdgavT!(m!1V zgj~ZSR2r*n5%GDAeK};Bd3FPSKgOH{s#3?fjy--bl`Gupl$RIvI25z zV1L%oeO+2opu>5lRGWm)MrHc;8TkODjcWw@8uUe`;yKC=sVG32C?Na%%CMps5ki;q zMafXm;F7unoeeAI-HOI_l#zL15@ zYfsFZ#)u6ne<_8;juv+6`(8FDA?E~H^0mg0xxpy%_JJ#a9Sub;WMC{0iNL-~^=zFtpltf!Hsx zriaLIqTKk0mX-Nmpg$a+)b0x7@3NlSQ|Kq3(nIiC(r*tb8)*JL45&qO2S3517p;ay z6&Si_&<2U>1S{9cLSKbh3-lP>cmZP?e^y>cD&)sB{yCa__Avwh4wx5%sdJv65{Gv% z1j_UUtJJ~pl`)aTFdkM3k_P@gP+ZYXDK-9uO#Fdv)WREUv06xotl<*ovmNBXaA5DW3>yb@0e;Y`{NU^?LC?@ycy3ALWU%kvP@wE|O z`?;_EGJ4_Ojz%y+qfveo-wqL0p+$%H(l#d0_CqWZUN~j|*e(>!-mlfZmbuqk5JZZj z!q;kX3iI}!lgJRg_M@C}0vn{ldeAS|^nB&RG* z2%+E;?k*&E&n7zt19xrO*|^I96Syn8I|anjVKgsh6~*k7E%uDZ#0ScFQXs}_r7S}$ ziQ`FHv53S_5U*zyGH9-06$KQec^PWycPxwJlLNovgtX!0wBc0u!Pw%c(oBlMkn95* znu~8z%%r(eTGB+qe*@M2Cn`bn^@PImdrn5g74#983dE^!9@YFXE-yhb%AOE-lD&HK zLk2YP9{`HN++Mq452qOTPbNzRo*0ZK&H1s2>{c|E$C=IRXCs%+U{^x!$0F+kI*K1f zdZyD%A%)H$n;)NLp|^lCXW^)khIGxhu*Zt@#z6BHx|qldknbdP7hlRMh+i_{jp_(D zoKf>O;O2mxs8Nr1VUUg&v}Ur8n>%?_Z$i*7m{6o&Gy5)iT}*T-7440fRIW znw8f6D5i+C?Xif%*3*2XEbIkKKT?gj&b>i4A4#LaX=%ghJtn()!oL6NBSMwMV(KB% zA2J(-x8JlbXR*J<>P!|3G?8LaJC!JM1+jqw6x!XqEn&+)pixFRi=O-ukOn=Woj3=V zNOLc6dRyXIZ}S1glhc4hL#wRmN0o$sE3k_0B|2?cf~o#F5$!rOqUf`g7*g6=f;NAO z+KaRBfRqFtXwVB7$&;8!Tgd}zD-ieDiq~VI_}&5oibm5OsEk;Kvj>Ho)6pO&#gB(b zZ%D8|=_Bn0T@5SSS(zxB#QJ%$JbnD9P* zWpru10y9P8#>m#eR%nh$V0+Q?3iepx#2qrQtxz^Dta+QS>e;pk32p#~ltJMC$J+Ew zf#yG=Mz;|;C-T2HA!~I(c6Cf@LRrO9@tN6(s*E$yc@1olpMOXGLme zJ%hZN5tN@WY#l$dnYE7Y<+}#`DyEwc*+wiQ-;ZXG6{(rEj@Im+aC!x1GQuP+fwgH) z@f;Q_Al-7Vl;aCtj(xUIIm#;-BH`qHDXMbwB{Z(%9LZ`($e{I*SEbnl9Ag~Uu^1Y? z7{9>oNNEBWtIIrU^(@hHto9bYX%kXoEBHvqSY9R!^!GVIs89oSGNZ ztX904k0BI`+0IgqBn_gA(}p*v4R7;HD|fX~W}NEjIOc;ta0drm#5-_Zx$|nhi=bp? zpRWnHh%iZHTj$x(1KN4DRv2XE&Wk-gJFk;Lj~0MQt9D+kcg;pF!(~eDML>5T8^zXz z23bumdK|gX;mD3Il=iR;e51(4JcTiy7;1TX#CI()(g5CT6}J;5?ke+Z@mIU#x46E@ zC&2t#SRc^~2GZA~ophryUwf45K(||58MzyxPm`xMI-H_5Y3H>ZQ}^p!mA<;2SIR*e z4OgII2B}NnDT0XmL0T~A*0okRU07(<>33SKtF3$BKQQL~R%9vD_o4?dPAlLYTRa1c zwmK9qhR-VAYcPBm#HNBpj}vT|!!NM4#(FDl<*Mnq<~C|6*R)Z?bkP#Xwf`~*LF;{?2k0Zazg_Gr`&+kIO*B*jv0s?)Af`$y=NAsh($+12N|j+d zCc#Y23lehp0SAq|83Umqgw*4MEyS>v?W zvwFn2*3Ai;dnMv3WZcD)qCT$O8^H%1xexPxKH&;2>@(=uiDDi{zGPL0p4YeInhd$G zYWU}@ml~Mugp+FRD8U_$WKACp)WQ3-NEeka;$Hw_KaXQtUnizY!QX^+N_;7ebniEn zGxZ7nCQpvU3;S!`hej%IbXXASfJ~i0R1B;kwtBMl>mGA#>Rhwa0Zg)kLs4+%R0F;p zAqlb!#u8~bC;b!P{Ep{_o0$@&1aBrjN|f{Q$W!Sd{7vg)=#SFFkEKb~+tY?+JpplI zoS$5Fo5rf3rB~w=nNZ@_ldA%rHMX8b7b9l>_JmGn5CD5v1T~}2ecl=mENgkrAgi+$ z^tkvGu#?UFOi}6mY5+SIMe9dpk?m35vJB0A6cWcjSjVh^ZG{0<2R8JSfejQCZ%2ch z$|?+PysV6G&r;BpsjGXn64=s6_J6Id@(i}co^9+-%rrTJZT%~NJ^`RedH32Cd)&!u z!ta0eX22v<_X~HSvGrphq6$RBlEMFO9Zi^uTSlelKxSIaV4t%#`Agode%?9ihcY4~5>2-_}bcz;a4a;rAPgUxedJaU#+J^u~m5#BeQpehdNXJ;hxiI9B zL`P>(H;`Bi2D+hc?L)1IZYzXn);?62tv}#weu=}Ybh16q09*XRUSuJNW9%Ug<&9LC zL1L#%2VIm=^J}Of);PUPz4nT0DTW_g+;fJlXbdQ0FHDADKe^{q1PW&Q_R`?a|j zO>1+4M*9~u_IQ1}ZZXflBru)|^J{?A26drTXV{crxHcu)?*UQ7;=OjoDV(0;@_N|1 zY#-dM)bo=oX;o%HO@bh@rGrU{2-wK(U99y+{Y9#W^v!88K z9?;A3J`4rsTa_Jera4~BSy`o$$r5l#F|#EEj2PQ0culUo&aT_!+%#v~qyr(aqz(u$ zd23nV8%+iKu>&%dHipww+9bVd|4x`RB*e$*bc-17(wxLP8Kf_@?iSL;7E`5k9%_h; z6?n*xMZqM=sx{VAX_ps)hdn+dFc~JXRuZpt`2LZ<^dOV5{lE_ z2wG;b;r19tMmCH=?aNVYOiX7l8ewlloZ7Gul?kdrNke%AkD|R169uzr9TOCVQj<@{ zYIttnhKh-XD6Rz{_6zbVVyf~4ZGJyMG8|8q!{|1JNib9J1QL-v0eV`;Kn|^QtkBks zyd}1Xu*)d`ibei35(`^73jU#QO<|}U=nVk+aH_e%rM)3k;icP`p}3)Hb#lelEe@QM zaQre)bDNHfB;L>~Cf$h$ zvBH^nYFJ#TZW5w8+fBm6Qn*-m?;Uhewdm57Wj+9u&9HW=(oR6iL>Y8&j_nwfQbz{@ z23BveOqjVmqdcG^nvOsrPngn}<8qQ6atE z*_Kg~u}CcXqC)&3N9DIq=`)o}Q*j)$9dy>mi1qW(dJ_ z;?3`&My|ELVKqlhuS&F^7K2%ag+0QdRoK?>Fw;B)7Crcp5l618U z7taLG{$#>@MyqE^OzD|o`i!r$)%{ygEUMB)^9diWR1>DxagP~{pf3u}0>Y7LB>z|_aj$O@sN z+}E~W1dUoK6)AcWfnMt0{2JWy0nR}>*d-M3aN%%h%i8R^8Z`wmWLIB|0vkP1ZP0@&Do5QV-^Ey36|m*ECt;>dAASKZbp%nNL7 z?7%xmT2ZyP>C7$|WYaVi_xui5#1#9oz!oGkorO?v7j-Dua9dCBoG73L1hAFP$yUr3 z&^il%F9b9W>YT*k2_yER5p9G?1DX&q>FB&x$`@3SE1hdYX_}qrn=#<78#=C)0SfS) zQ&9t>JFh1@Ds^Gd%cOH!LN9e;5aUm?qM1azj!xweNHi1YJPkC+{fK5>pWOqLEmm|G zveq6_lli%{MHu=z63MAv%cTUpThz-W?kqa517aq1i5{}Mz0$8ao5FDUSg|)je^P=T z?o#YeF?;9Uc`H!zm#Ny%Th%ET8dm~aaH*Y>dpu}(V(7r0NiBNc|JasT@wYtjfX=IOWJR<+Ik_JxW(fOd%0VP~VPBl!N@{U%r#z~HbaT+_?Z zDJqMk_t;>VYslpLodGl{$67j<`zmMcklPH|k*4e=q!on8dH1{d5nf}ss*Cw+Q&U4@ z<5QF5g(kN*{mKVZ%O82`jCK8obA&95wl4dDm){JCTViRpOwfdPH=Xe$s#X!X_TQ#dh=?r>C7T%24^ z>^jQvbV3Oi$AWLs);^WDFUkj0oppfMULRU0 z1JLS;`dUA$6jB+uSZ&}Px(C1)e}&-~)7jXsXPk2!Nr+O5pcpqYUKj;>fa4)BtJhCsvov$aVFT2ec%2y-sgV8r|~{wg6l7i ziZmO5R3swpF$#3iF3B7QA|3(M{u(`V%GX%I)mZUtStIt7NLA5-=ShybBY?!5=xY2w z&AX&jnce7L%yp9Y(!-lLs!|WFr?!e5IFLEGc+SDu^nM2)*PsV=M<4QNhPm^g(gf;~ zI>j03i9s~h@)3mmC!kQg?fsDuG;0yJuu8$`NGqr@GkcQ77m@knAX3<8;al{*6&|wo z?-FPS?&U6n?O>Oh-UjRZFq)SAW#OKE3wc@cAVKGO@>T?U%xO4bjscGLWt8Y~7EV1} z3mjX~NW|fQOA+gG07cjd`5fASowqQeXT>BD^mH~72DFCUhGP)2sEJU&v84d({8exz zxTgQWr%`&o=1f)LXNHPb14`GZH3w1FP|TvzG$_hdKaP0-DyokFYYb*s>W#*TrulS! zW~8ph&yiYp=RwM+wEksGxEt>?h*eqmZok~gKEPj>1RF#oeZ#`Op}Z{qf-(mcXIppq z+oKr&UqOsZc%5h#CegQ&M`wm4W)_`aCQ=9DoSyaUUhON+4mhD21nS&iH6lt6Q9C!l zdZNgzg~HlWOr0ArlhhGQ;L`}*T0$7+DFCOp7|1om56F7H5vRUF+Jce=FV;N<7=IASE)0TxbztEXWBhZpV0QP|N(s{B zDX|`Z$N?yh4^u&xy7PNk(mf81DAGrN`yh`eIus`m=d_Npdn`HS9i?c9T-jbAIkrTX zI!X^CM6tHWhVgO4658c4q6i>%dqQsV!9U2PG9VEt&d<> zZ>lw7KO$J2lVDE%ymYniw$9F<0R(YA-@!!W4{@y+evhj56|F6(byq~8z^*$_S&{ER zSG-ele)~y*uMbC+;`^Lc*wbKe(sq*E*WSr6_2jA7V`Q4_GHc<_Or@Eg z@>u0}Z^l#{UnVZrP`q$r4gVpHb-NVqsK|XVC1kpH+eIJuE0|Ble;2@KTG3rW)_&fq zj+eYc ziFFkZ6Cg4(EQM}R!H&}~A!E|7M*cWh_oEm}THK-w`zcWTaXwbNx0vw_Td1s@AUD|N z<5t8!+ey{B)l;EB4#S=f$b%{i;t2)dySGs)@dL$Zy%ojn@W|oBsQbx?zWLS_`E_FD z$yfJN7?fmc6+;b*pxwJryK|wH(?0>&N>K`$`5hl)JCvh!Ual2O%77evnGelB4bgBU>_yI!*Kt}zh= z$HQAWb|skauf+UW!h1mo^Jl9t)6Lz1*^`g(cE9QwFFCFQ&O4yHdTRr|%}JmFF<;qj zJ_71w;JIfJsnIiz$~mCw-A{#uEy4Ajk(J;YG_r`kK;asJIm%Y_hLjK4lwGzD?%GA$ z2(#80R@wrpmr-2l8+ihyYkjYdB7p|D2O`2$w_)UhnWh2&Tv7D$VuTdqv!)_EqJ`TY z@aJhGH{l#Vfy?0XfL-+j7kkokVtmvNiq~vjJvC;ZcyAReFe2NFQ^HpHr9^}k|Fu*X zV`>Pz`GWwy*fnXRx)e(*zKxE(tUh72?h8I-cMHvGkC#&3*#JP7R^rdDMONAK7!z2o zA%|2B(XXc3mT0x*SSdttFh*bNKT3-Pg|VVI7!wsITT%Nf!k_^8wZAb`cD8`(rJS7k z>mIxAIq()uKZA1UD0C~Ue~s&dq2h{E`kp0C`DfPH{Vyvxk2KyA&vCRMWa+%4`~SLD z69L(^R7(cYYtyw2K*hQYf42HDq?n`trwjTOvEo^)6@N)@un(>JIn=}0z=2rWL2Y(b zGqARpO940RS@!Y+x}J?S-mfU$8Cee@QS9e55Wqp$XB~79u8S9WZ3yhgL|9#5rMoSF z8ZLQyqfIbR*upMDJ%lmNEgc_8e^LMr$bCthIf(lz@H@~P4JH_L#`sJ!!JhnOh?^AX zT*v)nkmo>gI~k1quVXNe#dH`+)xVo-JQo0(g0(J6Zu;{Fy+HE^iR@|gNp-N3p-`Pl hqsMQX{=_cy#pYssGn3EkMgVMGGQQ^QvGpU_{|C@tiZTEI literal 38268 zcmb7t3$$HTdG31bz1Q9*(r^$V^}!>Mkf2->5Cv%imXLrD0!S&)(ZeA*2acXcIOjx= zp&|kT9_3=e2d%vhtyD?y#kI9w?!C|w4hR^qwe_OX_TDRK#85rfF$~=5{lD*jwJ4B^T1SD zo!oKx)VsG2CR0}?jcjbkXfix@<-p~`Q-j<3hsU-hEAq@YBnck2CCREh8@y(Ca%!@F zaAbHiN!r-}r%O?$MK;8z#!-1T0Pv$R>>Yz!r-t9<=n`NCFzXx}AM2moF;N2nfC5DZ z6hp&f!&C3JmU4n3+cZ3h?qta-lsO8U-(XN_XV<7=OpJ|BajwCu*p#FzFgphnsF9+~ zh%t)E)r5fqw1q!t)6xr4I7X)ll?O+4;(lc>RO^g#l`1-aD4kZmX zT)?tn(+_SJLkS+j*uiV!;T*ISV_uG8X+U%do|BZ6AH}L)J|59~vY_Lc>mZ4LzG*;~iQO@Op{&TK}!1%r|^u*g=R#?F)R=ndTW zttSA%ma$xohCWu=x6BJ;vq?fKUkRAxY1eUc(kUho`C8_-SZH-1qVkP_)cqDgy z6fU`Y9U6t{^{8$lrezU#XuT2z$M=yG+L8EPhOR(=apvfDv?Sm*O(T_0jt-2B3{Fm& z_9C+a=*H5CpB*W706ob?B**-xG19F(G(|>IlncvP86-1bHb9SuLk4K*+6q8D*EBrCnwiG6TsCUj310siD1<#9S26gWLE-?|yqgI=N%(R#U(jJEu`j zQ$U29rq=I3t0tiE&B1E=i9u=BbpniI@AQHKcFpalAPQ1?7lD5t!={&HoBPKs5aNNI zpDZWY(qA{tl5A7|td67gnZm7$4=u@zXYZ+w zLT3|&^T}0bfi9xC(*|B5ac(sChpaa8eHT!r^!A1n@oe- zO@Yjt73A-!o1Mmf=TXS1N$5|gkwZ8kZ9&P%Ud;Ft6t*xnZMP*!#O*3dj_X;SRVd)$ zYNge%FtnSmDP0x%myrxb6$RFM&g&$Oq@dK$(=Nk&v7h@K1)e0I{K(ZF+?t>22rvP14-LHTGN~GEDbHK zgXaP!Jhi|vrhxMX+@Mz7AbPbstLA~$^i`{J%y z62?C5{Yr32L^X#?I*?S8<(;f5ALGO~5h1G|L{%~LW~-$qu=N&H-?Wmd0dcmbPz2J~ zm!#il%@OI7W7v4Xk-D6RdN>J#=?{0IR&b6Fvr%*0C|5?~nc!vLLV8CK$&binE{|jHv1@*NH$zRV#LebD$pDdTur~De%jI6URAJn7ZGa}MGAqM z(&d^I)hmEiDKFwz`d$?8Bj!U;eGiK3tZ+bV6cBo@FPG&f>?u#9g=yMTR#2xtuN%vC zfX0+#Sq`b99WArxRxoRL>Me{udZ4^?W{5zksTwk0qF1N?0t!^dqdoNYmRW z$J?yxU>DLXq)5;?$9$ah-{ zgj_E7+r$3b#631KI5ZL*p>!MsN8aTLzYNsVw2H^9mfl-ro6(fstKbM_y17Zf9z5D1 zq*I$!-2T&qn{63GugNwWv#MrgNi&?HDLn}YaOD`Py0S0%)Y$lNd)QHc!@&^0JWb$+ zjukAq<@Z+vCXZiN)sBwPeg7(y;8+fo3t$Lcb22nJ>P(Sr(2q}vJ7D?hl5ESUB_BWm z?WM~pNN}6dSN1JI*Trcdb}##m$>iz|mVd zvl$&98#m*w4fg{{(2x-LXGv!#HSu>qtAOzLs>%su%~keDC*X1fd(2t@>2d<)u^Qc4 z=>!1Pz5LIsT7^k#d?G#|pl;nx7UQ+)qN=cWskfH%CTTe7#kQ*&pXgO25Gk|12i5&h ztUS(6NF!SkDIEY1R3;_MFQL)+-Ne&@>>%45TXt1F?^%zX-phb0Jr@I@wCqsSjPfnR z&H!f7u#B4SpbCc5CTcV#bf?SBC@0@NDnBkGLZ`qAyC5+pnIf3zXr%iwUI8O4u_p0dSEWhT>Hf+2{rXa&+XFR?O|ox^;{|A!X*@3D>P=Rq$aDN z>S)8#@@}w0`?vzNkXdLopv_<3ykHNpOvg%j#(U`?Ka#ME<%_^mn^RVBzBBVsBFOO96RG$6NG(m{BDHQ8!QF4xr1(xERVZXdB=y&9Wc4?y&ZTOt0>FF` z#eYQM(kO}WUQ2FyU#a06DjKGelJ(t7Q)Bj$+McBeccN^gZ>7~T9^Ny`K;Ihbb^Gst zh_+&udDwbU?l^}ayUBN1x)+LaY~3Pq<>*ApG90_|u*s6_W8SU}Haj0}>5#Y%Mnuh2 zxOOW);yS>yk)DAyg|dGH?(#Hp?0b?EJPfrX4N6(;Ib!Y--g zAmD&X@Nf2|RaQnB4=BvOjIKr5ws|mVpCuHRJ^*vg4n%Q-w~XutPnN1Yh;im`@5T&@ zv+RaoDqIZN@fC}U%ovkBWbk8yino4gJG2(6dlE1klT;l6jfU>b)|zJXF*$cPMqvW8h}P0t~)-Wu_En4&T;X1g)AFG^hYqhT3@sKZ*B zyX6i3HqWD>Lr<3yHa=~{SjLT|ZjY6zm#ILibBBA7)xEsi;qWLvdz@kl4o6wmE+FN4 zW%n$cPVyX?3-s)>w(N1pL`f8$os%+w`)mrW`)d)9`B@@ZPAC+dbqbkNcNAs&esRyT zs&8UrRxJOzzZA!_q&q%#wP~aeCN616-VT+ryBT$$7_2MqiXF;M66nqQ?Y2kTTdMsv?<9MB_avXW;mpMaW zI)s5`7No61@e74F}bCk4Iv6LQ7(n8*%KPSfAvXma+uR?UxQ z^;ER>u?qb8N*@~`6X$@*l6GxGID@YBQH+Z>^T3t#c~Q7SRyvY!iIje-+B!sFz0BWSsW+-*XYXQezJ$xmYI+t8{bAn==?Y@0*>Qcyog z;2+sECBih#SqU`3Q9NT!!HUb#DFi{Gt*_+v411{Kb`DMrIzP!X2u#aJ_7+sd*LkRl zuk)?u___eC(;^FV_E_C6w3X>4w}p`>@`i^iih3Q`=!h~qEg2pfN_eD`!0+eS7v`r| zZD`plG;g*dEDo2MqOHcRtTlhVH>PA?KtPKMPJ`y|3~YWNS^I^UP$J|DP7>iom`|qh z2LP}axxiWUHbj0QvGcZy_XTsaLz1+{&0+9}Mx&Fw%T{eu;SA}DfICFqh{w=9wGxz4 zl2JcM=7f>yq0O9WIfGH+s#h+NsV7QyyyKv;?}f~Ba)4*IfrasxDVtU8L_AQmH&7HZ zKd&S=3WMx5hwM~)o0qS>b_rq@-GSE0fLuN3uHf#L@dP09A;mIO--(7exF^fo){>r$ zb}{Bf^Ikulh%Er)8E}_Fw^>_`%d-5sz;6VEF{Fv3{Q`TtHPLt2kcl7#-7x7(pI;aHsSpERzb~;)m!VN*$&{4v( z&jjLU-Y;otb0%rpJZrn=LB^Y&fU&c{m47UdyI)p(JvzD0^8aQv?FTpqZ9BUH{kksz z(R^VwI{=MTJF@1fiGeX*Cnd=SYtNsECIKMEC9{CrF_44qAtH8&tkHtI^hyKaO^8*xa~d(E2U3a)(Fm6786|&Y`ZXAN{&mqeK3* zJ?6*4)*U?h_u%onsELy`ju^B!28cHd$#E2ve;0BHjR8-7EC$Y!!lzK};zwJwFfRW` zst($bwDxcyuaWGX%mK6;1}jqXbSP>~D@aAM2TRUjqso(Q)?jz+aBgu%kUYZ0c_w;g zZdMWBxDpv2>US@m0)T3YWI__}DtnSySYp-b0Y0P_5o*eRN$J1VstyP>Tjef+`4uS+>%mS7Kvf#A2b@e)UcTbRfYt-4 z&Ne`3G7OGCheG7hMgu)MOO+vRu*ZhJUEm@P2Nc;4(M6>_iJf4M0F=?D!`k3;gICkE zaXn*DBj<2$7un-9hg$;@^uvucbm*e#36CY>Fnhbt9*6L>kZ4nV075|;?X@V>{B#Ln zK&{S`2$*zt6GkZo7cHG%QK5jZS<+TXQT}Azj94-37L@_Kv4r3tJv2HToJb?v)~}TU ziu0Ff2=sk;ZY=43&Yui?Y~auj8Bx4O(g7DXD5@MKlHa;SYOI&aIUr z3Er(0hl9lUkqy3%6jawZvRf5N?D&B65EMW!bcf2lK|kE^*g>Vcs%8s{T_{|p1pb|; zgGD-yNayqR9I51oUXQNPyvPIw=ld;1AJ}1ET7}rIV@Kup&KUsPs#O@E>*azsD?x@r3n@WmzF*pk;AcG|Hf~D6vi&m$C4xT{IFiSG%6K184%%g+_-X8p&0H zrK>?(!9;*>Z0~;Vav2;7@6hNEShhl&xS(oa{wP~&^b-|V1iK*khS(vIa1tUyjRe2T zH(o}fDbB6Xo{s95qS_b=>g4-3YEbU8HyQ`nTRd!rRnhoRwLeIGtMyA_R|4`QEan04 zR&8UO!E25%{5EjKTZjg*H*Nts-LY=K^MAG?*~69pCR8_goQ-P(Vb}WB$kZDL8@%30 zY4n3hSrL63tJ&HJ1CUb#xGrdXyh7IP=;pUBIn_d1Jr~K8r&?SfF>3HgJOR~>t)9Nd zwV))TM|%qDIVmc$e#k(pr!vujcDfV<^S$N9eXFd>J$JN#@DPU zU*q+(DXBk}gW6W6D$rWbGWKL z5Zc>U9!-D7`sQQ<->aR*;dcKJ9mQKybPQ}qHQJrpwfE>cg7a$vU>?GbD+qfTdLvK1 zmwMie*1h&OIxZyS)STT6);jI~0!B-A%91J3o!01Nw+jHe(YZHNzsM?-+Op+CTrjULm%rS$JI41Bb_{DS55>D8b7xpU0zGKy12&g117EU|7x}DPlJ}`CYV}Uh+qQoot?&un4~J! zo&&jt9q@0OTpQU9Y|^fBtTnPGou}EUCth0!;-+cv1S|akhoPWg?4<*<#t4*@MWA{H zJV5bTb4a&SzCg;XJUOa66`Wfm9R_PWu`MdnqvOV46)SOB8MwH9t^LKvh5D z0W9$RIobi_FL|6{PD zH`h_o*bV3zgPO;qIFU5qxG{f;CVy)Q#LYx=9f6QvaATRjWNVOMutgH; z&dW4iIZ+b_PR%!3LD9MF1r+B23n(lY1!*t8bg%K! z#mU@qBNKczQ^^A6XzB`!X_lXpRuM6-cka2L=9n?Cg{^#iE*&(-PtK(oMy0@zG#61= z>9<4WQQ*dpi`Z#(SJW%GF783^F3hC^3)&FT<}GxAs*$O#7)V)B$^z+)d`Xmx$X5fE zzTm@zjKlWo6I+8eBT(yUz6agZW8{A4K<(k7lTR-<=>x`L8%b+eN`KuOKXuHG@zJ4<{sp$>`mw^|-R-@Idfq>>>Fy!o++Mve@I z(oHDGkecRQ46|HVob69+p#9*26*?GT<0pabP8vE720|=$UyB4?C<16Y5)Na~)f`q@ z{_DzocUfb!7pE;XKd}U@?#4Uv;&U%+I+iKA#D_6fuTR1G+4n(KQqs`|jt)V-fN!nT z_7@nLJcr?5M8W0Jhc=4Bzew>vtR;Sd%D%e-Q1Wr_OMr+6TgkN5(&y2uT@C{k8k0MH zjt<`v&UJOp9e%mYuuA{JyDS3N0B)WSemD}FQ4hZ}8EBphH<~LFNZ7A4-xtiZ3 z>{*m}`YpCZ!}OZO`3cVb@Td8=-IC^oQ6y3eEsN&=Gd zf*zm(_B265^E=cS3t5@H=wz=D4qn3*V31xGLbm~fG&1VJO3t6NLZ9b1UW2MEz$(pu zz#|B0KI6YWfSGoGV(s;2=Z4U#*(?6+LZQ^??@&eH^>3xqfb6?i#`|bhYjO^?pS`H> zAK&0jAT1%$-(p`~l1a7`{V!PiTz23f)S z;y$1iIbF=wO3NbJdpLt37v3c_>EMI+(#QsfSHwkU!P$Ym`Dh>^yu!jcQbZ2gSF1r? z;euDQ@9{mNaQ+4C5J7Tb1@e&HVYiMJ-%QWvT)-*6t&4{Twl>)K=J&18L?EvDgRpjJ z8j;KNOSOgN(6YZt^IuT%9xZ19oM07wAdkA5g2HST+qE~uDOF(W1=Z; z7<_|3XI9xDQC-1GK3VW9cx?+Xy7dPb(*l#adylZ84P#mtN0Z}u{xMA4T9+JUkor`K z^IQrX?n6wgx$Lg6DzDoj;pya6B++9BEH?`FILke+^j-|OPArWFE_~ekY zSJi--q&1RgKPNHY5rMQ(p+=S+S$?ITh`Y`SXoO(#XG(042%6c^Jmd4*d}Jk{aH5ot z#C}RU6RJ>K=5Rofj~I08Dl4=CX@Sx9z6)nJC~e@XT05T%gxI^Va@h3Odod9eSKS@u zlfcfU%6{Zk0|0=RB>O7C&YMD0smNC0-v4Yl^e+;ywR+VD>_9-Hb=R znmsoi4F6i3L?n{Jx(KHV6>YhrBQB=vF%gY8I#naO8<(JKj(vCST7iir+IP>Q8eFON z-5eCO?ko%9km_suwZLFG+eb{nC2iP=aB{vDVV zE0G#IVt!+_D0QG{4nf;FT-|g~LG+PmtFb}8O;&cQA*l9Cwuq9gUFZ%`MWQdI{{O7c z|3FxJO8HY^=^4J}e-AMIfp7a^^dX^rw~h&#-!FeC);?vt94&f*ora;+VZYcdCbnV|fyA8iGichM)MuH}bHD2}|DwFf6iDZKzwj(Ms-V(zJmL!ZlFFB&gON zPynp;px@~NI}{vYFJEbobTWMuMsXU7QttJhN~`95nSp9&t}pTJ)e37!A#_IqP_!Pj zA}PX;EspL$tXPal?dK({BCQZY#aE=ehSEKQ(p?&)Ytt?yUF?Y>>CQlc*+FQegj$cX zieh2P)_cKY;>8M{6iD#mlx1k8>iI@PhK1#%e<-V1ZY{=isvic@`Yw8^KPi&+G;}II z&yZDrUNd{8`;|TW%C@X64eqS8TzqRgpXJJENfTxJ+o*CI-Sz&6HMS6zw2zCfHse)5 zTq;7u+km07R=5Kx_JqJwIVf!X9FUI?D1s@-e`ccf z0<<+BxpW3QE9Ab!Y~LSE=*JWQxzIUh>qX2L4lxp8u5iL&0d!qQ7xvtGaRr7)Yn#%f z_3b>0%clbXF|BMV;D(L0;P4gg?m>+r;m>bHCx1KrLMS~@WF_-^Ac_k}Ti-&N={%3s z*J8e2%ZWs(^|pNJk{!0wFNF0><2e^IPcfsbEY* z+$@$`QL8q>&=kx74W{*Pb&ya(!PQTS?g@~1F6gF{E*mWlp4&!skEF~#VwOI(VzkA| zNYavQRlXcXGFBTc3(90gw=EYK#N54DU9&!^O~O>Ix>!*mL|lmw%u%FPxW)=*iu3h= zK}RB+u7e>S!FZHz--G91{l)64XI)-xcy-tM*g9@M5$By~-SRN}ttT)`lnf{$9AS+v zA{@!;N-Mh@Yos*mDh{fk(UKqsmE%_$S?f2HMX>k{-T34QAn66Qt)EB>J`aPOH>t=Q z-Z+?e^HDs$RxX)~$Nr-zOn8?SWgdoVx6%JzEl)=U_PNZXvkNZh^CI?SRED^PTZH0# zD;8vu_=9`qpkfP$*D(od2-9QI?7yYm!F~xLH0!Fu2BeYttTkFV8d5MN@jmqEU4abNFb=U^@KeY+c~_VAlmRa zd#rHkeafn`*l8FSNo@VbS9QA`?Y?ow7XmK9i?;!XeBoK>re6p;mi#MgVH9N7M>`s) zL@J3fma9s49-U!ug?u0qo>oY(3K&H3eiS!i!tgSfn69K^#dY1%N3j<`{`d@WP1S@5muACuh_^%?J0^c1F~*U!Je)?1%2lHdy3*- z>OKy~71ouZ2FvEc{Klfm{p&f&MUNvlVCTB|Ym%_LLI}B$@DzMr2?X)(fnJvw{=0Q> z_mxP{wae{(zuX*DST$U3_m}8p$g%;9Dc}raxpo;9_TrII`A}DDU6gK!A+2YDS;rsi zP*qqvp4F9B&XsO?S-IUvRf2Fm+CPzv`HWNwuOf(~AGAeVfMq+=U1Qbg#gVEH{$GH6 z1cZFgiXNdei~+`31x0-yo}=9X)r;W^s+Z^&G)1PS0jMZ*$Uym^ys1lQse_k z@dD3Hv(;8F<%8zuyV11Msts`4Asc`Zk)q;->ZoXPAu!N(14XMM74Y7+zeyVopm-NX zGHsw;70>e-TUQFCtv6x9y5aC9#_R*kJ+R((hAP*MNbIJr*c+(B5+Gew79t?_^GKro z3Sz2N{ExvW<2%Wc+C27 zQK=0)JGBLA(H8(|j|ChNA@RD57fVGMhZ~YM4(2MGdFDSDU0aTkRwb?aK6pCJYucS)tlMU&jQl<7u zfUHZE*yEy1MVBW@4Pq(>1LvY>pHdddjIxilXm&|J1;_7N$AaMrd0bH&p3qZ#4uarYFIwT^e;_IBXo;>~j6T0qly7sB zuZgj~l*H*7kKsSaz|O#|J-W!Mvvy`v&g5zBu(mm@ou?l2SUZ*JOg>1CdKomNi?jA^ zfULE4^vGU#)=No*1y+~pv%HBN_o@tr4N8-iSs(Q5iJXAzP*R7p!BgYpAW( zkZ-P~Rk?t-X8q?XdRK>r{Lx676y$Eh?}9r=`K+gXhjlENjB~z_jB`-?b{pBgqhdvr z;*Z&5MNcx$oT%y)oAOE?&1Ly52Dy*MbA96 z5U|2|WJMniOOm2`$a-tn<<}s?c>;_MC580%pi#!_$}w?U-w^#4D2d)LiFVP{jWhFr zi)$E$(|!!JEO3I{u6*^wLG6b*ys~t#hTGtrFx53IMAbM}yx-tiv>yYBVc8V#4~9am z@t38@jo=^UOmhOY(J#nv6R6G;wE3Hg5|KVZ2)P{t+a62;OoUp1G;oJc}A#iWOb#L z3m#KeuiWTE+xG&&JdRZNQ%s~~|L{w#XM?stS10@&rS1@(C6E;hE%AB7!NL+ta7C@}2R>jH>~UAqumGACU9CbIUs2(k z1WH^mrjr9wOO!!Jyc2Piy4}DD0oHGy(Bm9?H(eal`T@JO6@ClqqD+^C_u(0a(s~w4 zkXtQfq`{13N!^!+9lr5i9~G*XhwX48>AX!KlV))E(V(Il6+$TJK!7y4&XHDI&^TTL z(S{t3gF1&zgWcIJ~cmfY?u$(^*-oNZ6LUJ7o2k z3OS6^TgsWLW~N(38rU%`?>0#8Oeogkcsx>Sodd1rs0p&B*{#ILIHZxWRUB$X=SX7a zF`IfSkEM6^ii8nO$@|3(tyVLa&Zeduwqqhhk?aiOKwPCx@~UpvC`spkN@P6d=Y9!ffZD z%EVy94Xl_xY}IXj!o0xNc?F6cR@CinIy|VFS26ekMLt&Xh#aA@9bH#3irv@~#e#Z? zrHX)F>}Er?U_ko-Fhv0kgE}{$xVa(-1~lw)JAmm?DiO(h+$8EMG(zrNAP#c~a~k@6 z!tVwYc`3moAJF!HnwAw SBX2=Dy