From 45a0dbcc34064ba4360518dab8d1814806740dbd Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 12 Feb 2014 09:38:58 -0800 Subject: [PATCH] feat(builtin/num): define fact and exp Signed-off-by: Leonardo de Moura --- src/builtin/num.lean | 31 ++++++++++++++++++++++++++++--- src/builtin/obj/num.olean | Bin 48352 -> 49064 bytes 2 files changed, 28 insertions(+), 3 deletions(-) diff --git a/src/builtin/num.lean b/src/builtin/num.lean index 3279fb13c..76253cfa3 100644 --- a/src/builtin/num.lean +++ b/src/builtin/num.lean @@ -175,7 +175,12 @@ theorem not_lt_zero (n : num) : ¬ (n < zero) add_rewrite not_lt_zero -theorem zero_lt_succ_zero : zero < succ zero +definition one := succ zero + +theorem one_eq_succ_zero : one = succ zero +:= refl one + +theorem zero_lt_one : zero < one := let P : num → Bool := λ x, x = zero in have Ppred : ∀ i, P (succ i) → P i, from take i, assume Ps : P (succ i), @@ -232,7 +237,7 @@ theorem lt_to_lt_succ {m n : num} : m < n → m < succ n theorem n_lt_succ_n (n : num) : n < succ n := induction_on n - zero_lt_succ_zero + (show zero < succ zero, from zero_lt_one) (λ (n : num) (iH : n < succ n), succ_mono_lt iH) @@ -252,7 +257,7 @@ theorem eq_to_not_lt {m n : num} : m = n → ¬ (m < n) theorem zero_lt_succ_n {n : num} : zero < succ n := induction_on n - zero_lt_succ_zero + (show zero < succ zero, from zero_lt_one) (λ (n : num) (iH : zero < succ n), lt_to_lt_succ iH) @@ -681,6 +686,26 @@ theorem strong_induction {P : num → Bool} (H : ∀ n, (∀ m, m < n → P m) show P a, from and_eliml stronger +definition fact (a : num) : num +:= prim_rec one (λ x n, n * x) a + +theorem fact_zero : fact zero = one +:= prim_rec_zero one (λ x n : num, n * x) + +theorem fact_succ (n : num) : fact (succ n) = n * fact n +:= prim_rec_succ one (λ x n : num, n * x) n + +definition exp (a b : num) : num +:= prim_rec one (λ x n, a * x) b + +theorem exp_zero (a : num) : exp a zero = one +:= prim_rec_zero one (λ x n, a * x) + +theorem exp_succ (a b : num) : exp a (succ b) = a * (exp a b) +:= prim_rec_succ one (λ x n, a * x) b + +set_opaque fact true +set_opaque exp true end definition num := num::num diff --git a/src/builtin/obj/num.olean b/src/builtin/obj/num.olean index 9e3e828c5c4572b200003b59149d0b2666a71bae..65c199f0d19d39321406e30161a04114473b36b0 100644 GIT binary patch literal 49064 zcmb7t3z%M2dG6l(|L4EVpJGU(fY1lzmJkaiK|rAA1So+tA_N3MP$xr}kjZ5xnVFCf zb3Cb{Qllusk&6fi6a$I11w`=jc(71FQSs8yT7}xn=}84Wtrm%zQ_lCk@7imvfBk!A z;yh1Q)?Vvd-}=^fUu$3f(KSPZBP)j23}x;wA6~m|bZjD9Jv25lv?g;`=M7Gj)$t8i zOkA^WD4STB)r*l0YqQ~zm4jCdPYhi-Fg$W)c0{f44OxbZE3<4)tr*%gJU%f#FtlcP zZI-o)K~9&W%$vmuUe%AR6@vgj3d2?nEuR>^+R-Jz0$|oTGCDFazG18a0su`E1yHOQ z9vPmv##+h=n#JPbadc;$IVfu=Y<`15rB!TF#TGF#I>EVy*0U+gkHG94&_sfy+!?htY0qGQIE$ftGn>!9iO7>j)Dm7Osy&aT>u6HKwK# zKXxufI4~&9)6(bqfwNGfz7;`c=LLdl#hIg{#z5*kXEr5Xib2`gFtQ_1W9O;3^a}3# z77~D9Gg%&khFPq#Z>DF)dBzEe{Aj>rr#8!(On*1C=^PjsYv-a2`f#4f!*j7!EEZuG z0;tKkSp8#CdIDN=R^Nc?CEfE7yh#a4VF5Fj;IBnBZ=pPxRl>$9OUgN{P7EySO=tIY z_VgK-=3_V=!h*6kC`ERvk5=-B5?V|=>Iyx?b`Y+$8rq)7+mEe1XrJR&v2aAWDPsBjWVu zS#fb@zOsx(Kr7R^(9=#|C_R(gKF2~w-4Ag?%}cuIMH~*v(cbICKDbm9x~EG3e`*co zaaka5^N@4d+m5c)(fOvqD~x;mM=nE)<-$*-fJb730Dny0dMq z;)=2oTjn--D3a&g*nNPL!=Qzdfzo}>ayk0N(6_5vEFM}f5Aa!A!_fK#E<8oGEatOlf6`oq1w8xvtX8ZHCh}zlFh+nUEw(Nn9l2_3 z0WUL7$s#~YIm(qSH$Yq2;FVVnjE!Xoxq}*C1fuv7{ziZYyHC&h8T6nQNO z*k+uttTJBFv(4f{()KL%Y<`!h(Q!A5Q|F=lJc?j4H{nvn15w;BdRYpoeTJ2r?B;Ur+g$j`%t*> zllnz;5zS3D@G`OT9Mdu+@R6H;3&lwSc45d5QOvXVfjEJplU^3iAPr*O~Vr;#P{1<9ZxX3I#mWcWMj^ zLwnw)(kr8XCJBMd%bT35U4?~yh6on!lW(fRLB0~lMC^U4f~258Ug^ZR;5}M4+V^sX zmpuRS{YiYMV&Z&%47iC(@@bAmG0QxJB?3M`lMRt~tw5CR#X!=wm)dkPt|g%vRq!-k z!cz(yV*YL^XH{(_OGPi6kFPr%l%m zBoinkhd7<7iuQu)V8Gj$BIKlC?_6uh4@C1m%~;9Z4?@C9cga55kr-Ke?r}hb#ML{f z0q3JYz;5qof{!AqNqp4)R4npf2dm0OIq`>ykk#u^Rpk1J)$&Db{V1x7kEX1~<#(tl z+X7O;g|#d!*YY6@4Qsh_c=^iFiP5#!m=|RrVI&zHi=8=LC-Lo~iXUVsjHc4-Qnn%a z;hZ}OPO(|61^kC%GVMBNX4JH>HMHK;hbK3{p1(E0M?cv$G0=S+#WsNw|2fLT&v(1X z3o|&v%uH}%Y;Xhuw7*66FCW${=-4pC<{W#Oe03Sn;i>Eoz}X@&G)IP-FALSx(7Wsz z6c&->rUh;-`7#uUY57~Zx`E*)S49hJ#2&%$lt++NIQFS84hEiEJ3sH>Sf4vWWf)jl|dvK z7tQtUa2ZejQNlbQK^k1X8PE&a_|0&QM$$MdO-Vj|{<=Z*X6NK(?I2%!jjx^WYZvBW zTV(bXF1NC~*=ENC!x)9Fh&yPJU7_uAfpGDpT-p78p<&i}qZ5Nn zp$t4P{*VrPK@EfN3;V(~&h9*&Ub3y?Ou)K)3)AJ>aZS~l<&v(YXz_k8|716%d;O*8 z;!rwZ77I!E{lFma_CTmUh^idj=dG6COIU1P@;{%0J}yKI{Vc8>&#abzGUd%)awXyo zU9J}5d2SU*4hX);(4~H=%KTnYuy-dB(`)Mlq>l{{Q$AOdqN+WBFyZ=tp?H+n2cY^@ z6koH#?IPJIAoM&|`t854t6Cm;Zj+vDxJrCpHkK{}jS0sRWlvx>)2>g@^?m?&bC5B` zGeMSv3@4sPLzTpe`+sSz`6mhc7^=^(`Z%iJAs-pO_DxbT(;(|iCr&T*vY!$Z`$=rf ze##@3IU6K%QuGpt`v(;Ngh^;s{)7s`0Fz5|zb^zzWA_MMqc;-CI53WDm;ZYTsJBrS ze_*xzXU*a~H03{2eg$E=xkw&?B)zDL6NzVKj?PRLo0k!7D6sG>)902`03OZOCz`X#O zbV1{5ohot}w2%p{4p@HCDVDCa{1qr5y?ibiiPh$F(KxGv@@;t_7Mq%U?%W#MA;Tvl4;FG9lY%vy6`e3)xg5uR~^(hgG@MIN;D1OiBT=9FIV&vS5xPpjfRGwWr z<-nqybJwhH3bZ~a{R)dE=LF_Qap}!e>HaoE!_ko;0LN*{F0Yc-Y5NDNr5MdAmAg=+ z(C(}_mNaZdeH*Ti^9XprX;Q*0fl$y`9B0a;?TSTMmo-^?eu=g7NHoWlS(yvBW^POt z^G|e&@nMj)nZxsU8yvRG)@bBfBZ>6ck92<*gpxCTUl@yt{%0nR19(#6(%op86ebP9 zv$r@AGjh`|j8a*n+flTrn;+ROld};o!wEsRI2JTr@5o8mb1V$1XkaF?i?B;^N&S#_ z#AR|?x^{GA)a)XpINmn8y@(L_NyVidRF@ZlRu1K-s>-1hOXk=m9ZDdgcoRUn97=hh zO&3`@6hL*mk_%GllbCdq;m%bsoSx%++e25Y#|7iml>8I6U9jw28<$9uK%osC#F@9K z5p-KLQ0;okW5(jGb_QejtkVfJ{j4l_PkBonJ$0Tj*C@2^)wBucGvDB(#7jIg-e{ zY#~|9HB*ZmZW~lwo^VRH1<5IqVSKmfARX3$6+3ZrwA>4=N%yA3dZ1pzj``H71cof3OtxE9rcBG%{YqNCj$O)BqT2Fr!|16j z-@1$QyV3`9gWbXoYL@LKqbTw_OOf9hxXDu~mvO-1D&wG>D$)+G6q2tTDK+CWpsHmB zZA_~tmNM7O$^VF_BPBoMEq34^2k%6g)2UYH7~DFQIR;4hqZ(-VF$yp-O(q^x0s#5C zd{lW~63X-aeXKR1o9OYNLe;)w5O|6u>|Aa2gUp(BavHwJkrS-TR zSsLqH6(gy?$p%EL?O%RWtiPnsgmC5XIPUo>AlgBTGmeT3W+#_`V?ZjS6UjVWOP61- zs>@(roMV?!1_KHUCOP}0#pb*ueU=bhK}{?!LiI7P8O39sELYu*d8vPU?SyeiD=Qwe zP%Tv{sP@Hpw`s&`iy8V1-ZE(dc_VgcEk0KzR9Rm)wBipvA#O)hr&5c{RLYW|^6sRc zF9Xx^7SZAiqj-hu21<4@6EXx$6%=SU6Ijn*c|1%x853(rs%-PYVVS*pr$)aajS z=FZPpZ&4;d?#YBdleG{#7D-LXH}mK~HzKog?-^jAqQ%LH3evmlq)#ds;6Y|Vn`kB> z4wz&p+S`@e07abQUwk(Mjt_%p5@FYIn!?187&(a_#;6zJkWu++ppT^U3^{)j`s9Vr zRTbXE{tCO9Z-<_!ebu%;V?*PkYpx!$E-IK$3_^ldyGXGG;*Rq+Ewl_Ulw%&9^p6j( zU1v8fm)pNJwv014`np!J0wIu;D><-p^G)ot$_n2_HgP#TCe7ahkn5->7g?=#1*;4_ zvsk?Zt;>C21W%mz<&v~dBSJ>og;9Wu&-Z{Uo8?*IPG9Lo!u`nn`Eu148g%8NS8TvC z{i3zPX1qeO&&Y_vE9QpD+g{y@oC%cH{7$s;5H%mLTJ35Akc+z8h4t1p+IG-CTQ>j_ z_(zoV=h-1>a9RRM*k5fU4_|XEMNV5$N>FHdr!I;(YAt?d|``rI9Gb6HKy60I$CPrzqt z>Zl*!oG?;2wAuXS3`U8oeySq{&vX>x-37(62fVIr!C+jw?dl<{qOsif2a5ItijYCM zWDc+(Fut_6DNeUX;rYyX%m}7f5v`x|$XySRCAhnJJO+r`T?${Qeg+M3JkJh75|Uqm zb}h`a=8-TRqL@@M(k`qoyWalQ9zpS?u-*s=Fr=x8nm4Oec2Q+kL!0)=s%&)a24Kvo zcT(4_cJ1u_PpszD^*w0q-MI&gyxT8$8f}y2cAz;q@Ne`10aMshIV;K|YDERK{wupM zSw0Y~b>axp{yub4yQs2^9ZHS4$&?-&T03CwiYPX!m>sY|1G1km?FHlWuQbd3mFf0c znrkr|!YNK7A=?4Z#bCzTv$$;PHpt(i-gUDlqu1I_df#h(we53IlI@(BJ=70MeOJ&5 z%v1ZZ71=^IDjNoGT;!u(aMgRMgx3Lf8>@e6wP=mh_xxBVNMOs5DPewc>ppqvQ49Pi$Q2Pkshfu}v08_?(xCrA78`6=*X92ttG! zxa`lbGXFWC>|w+e_H=51B{OROh(3Cy45?Rb5BYW(TE#*>vY=-OAR~9Y3HCF;ciaSZ znYd~5%(;bV3)O(P;Cc~ew<9#XILS+^Lg%(W%P-5;SEFT z9qXyjfGUK>fTy++1H~z=KVFY^USV9l0}~I|*>j!|c(P>BI*p1J%3H0FCd{@PsmPv# z?zz#FaK`ftJn1~NzU$fTXQ`zhHt-M^xNdu<0uOo*xJQ+(UlNLVLN5dt$DTZg;-x;0 zFz_HmUo7>O!u`6Gm(*ulylEk+pwq1L=s&%oK!4#>nV8`}D5m;6a-TPfd?TESl9ak` zg9i1lwR_dSFl5PdRy^u=>W>>Z#kFJ_w3@539i-KAo>eANH{nV6yLE1mZCw&d+TyYy07hlMguLMQnXr*gMMkuF{D9pEh zYPUok4z5KK1<*O&VyiP$2Hog#nt;b4N1fh*?)}YjjrUlq1wXz*>TXK21;tJjE~)x7 z>N0q)T`K~e^~0n?x+q82XdY!v4^D|-(8^#f77hoC=T)tz0|-(v@%=T2k_&e6j<@ay?(9TpvGb+?OBUhD4$>0DO# z(Z9(NC8T@Q?|E{V-XH0z4u82hv@>XM*j~;EAegim#!__1CL(~+UYG#%2_>P)av5j$ zQZ)vW`~R4>7}P>u4ODyqL6I3WjBWI9r@>e7nRPBpNwfR_AJ2+*6!lvSw0>)KR0=0f z(X&AH<1uxU?^p0vEm=`No&ra(lEUg9dI(6L@e6fR8ekp%F>-zEkrTUz-4rvOp2&pK zFqG79@fKgd#bcJk=m!uV>U3H-+ZtpRw??C^Q8o^XBPI1)i67Q38i|?Kt!qS+Iv>^! zjSfdNvSm=rku>ObEF!?y@9Vzqav2&LB>{W}^l|WP7++jRWl0JZ!NP*N>(Bf$O(h zzc_XmAfI3{1$eh;>z_1u%@Kz4hHAbQn1H?hHKIGvs?wyVP_(XN=O4jjFU+x$+jIFg_P}(c z7F;P0ZR#%o{HIowPyKq@=x(_0C@yVTf6kqcg2kOAZ99emb+O)$A}edmXymV+2N2R} zLWZ-ScUw!<+0UAxwQC3G@ALVO?(6&o@az2NepGed`+(Kl`OkxBMU);|@7{^8-GJWP zj;`5%+I)ul5sqH^xbdeg=Tl$1rFx&}Nz@y&pcZs)Uu*k&69{i#x8EU35x{yb(?1(0sj zM9KLyNcDiQeDI@&zLZZ`EOaY6My$0xk#xs8ECD5=l%k3ztpp09q90Ed8d%x=9fka0 zKXsT@W1--Au&boo=>ygz-14;)faTZTSxm7uOrVTsinYniKx8Cc@wPkGK9X(gps> zx~Uk&dL}NbfO(Pq>s#yDUTz7d98d4vH)&enH5 zU_vb9IK8DM9jfYAl*jJa#r|)hs#fH@wX11*@tuGu5XYI20rO1!Uyq0E7nrHQW6%$69Rk2qlM7Wy-2N6} zg6R9cNuExMR6K-&_kBB}5!bvu%jY!`LOF)i^nH(xcdMW6`&P40eBk;(-}qgt^?i$q z4(3I7?ex}2w8sdUjJx>{j@d5k5$=Y!GO#@?tKYJ z;K7#85-vfnb~#`N8?&2yj_!?29XkOMJ_~5rdtN8hQ<6C4b>WO3mWU27qZ`N~VHrU= zQ%r)j=08N&HWYkpVVBn`rU(smA-c() zX|iVohc;1}4bn3}{flgn8yWRr&bkhtvE=$&tq?qHsL{eDYWbLdw*VT~{c<(gFL421 z->)%hCko{_KSmW1)IV`fV0%{;d7pJf2yo4z_L+<7UOJvxa}2KWyMTrS8naP=>kZq< zx^YmI>}j-ts>V^}&E>`soR9e!V=-Mi?md&`jiVslNHH;i44r_C_~AyHjy<*J9Yjn$ z=b%ZAm}^KPi5Bt)`-)9u>ccJW!*egqdZSE$i|7(Ucd8bgfK1=761rEw6l;- zBqrSmH@l;eoMS=4!`;AnQi-@x3nYM1jgz{~nkU`VJJQiuFpbS>f#6)Qp9n{wi1#wJ zmegk7-EFg7w--R-epcxHXxx!(yee1@b*Rcv8*cz4^7BTezN$O2MvzcH-wJv!eZ{4I z7_O;K6d|Q^HbssNl4Csii4dKU(*d*2?srqGWTHI^W`lB!s`l#XngBs_D09@*kyd;QhV#GJI|xq0{fga5_ucPXR7sr5P!5 z2KSTQ7n~49qm#)OILeG1|2N)Y-l)8DdXRch!W;Lnfp)r+8v3?~j{ueEtL&3lKv#BOSb=&XrlKEiTroy#nL5TaKH$Osi`5z*MDf04K}k&Em) zAafCLe&8rf~k-DM%0pz@beSX^VZIvvxivs-b^S>6wN8<&>X`T!)K z$&TKm_M*t5pCwo~HoTVaS?${^M>VKrZ4>#v2h-{1;;&Fu@{MG?@i^$|yWWc02fUlN ztITc%xpy%_J2>dRrOX$imD_T${%wMn4WxUME3zj)g>5`;Lu_^{@mz+Z)IEUBRx~#r z_q$}hFocPE4qO4=_%VXaF5JbPWz!zQ6+Sm zRoO3oa^ZcLk%Hq3n-W~XMLup%>e^FJ0LU8OvUuNnv|5QBsUjbl>b|8`+XyEpMS!8z zz705%f)TZELr?g0d*df9tL4w&I_%GCcZczJTTksf=+}B_J>d|%mh{_0$_AQ0jRATm zOLGT5!J`+gW&%)wp}XeTrKnD@a-A&ni5P|k8R#GrOO_!Sp{S?g3_pnr-4nV_eqVVu-QoU4%N-b{3d1#>ic zzfRWFjZ?V>5I27>BGHeL>ZWvBH|J>{w(n!$D;QQdW%G5xrbyut#B?AqBb+u5N3Akw z>#UiCCFl0V$$paJWN%qLK)?)z)o~g>vM9SEAzD(ft8h-ANZZ|vf#92mlsMfjdfEnYeT;Fvah`oy|8abE100MU-_|rJ2$ujEjs)c zb+9h{z|1E6A01QRY6psD_cwN5&)n?{1fk-P@Qqy@<3JzAEd3kAu$WofVBF2+Xyxju z(qcO-)If=jj#Jq^z?uX8C0nkBRq{@uWbE*GgH2R*Ie{am4}>LqXu|M*7%X$0`bj<*QLk zKekyM4qdR{6~W(X`&S&9HXNHa%y*x;Ee2>YrYjQz?t4yXx>T}6L|qLpM>to|Z^JZ)6;FspYcXa#8VTPVIc4GW*Z3WAYn&{G_q@Mt$0pJ0y_J?8R6Lb%pX!oNi| zy30nn#so9D|6O1P-TJ)(-X%>9>d64(QM#=gu4z_U`_q^r@;Bd%I1D7;D2se`7^y~F z2ZL;WBaI4gNE=S}Q4c-KN9_x;J|a|EET-nHQD&p?_J`KxES5QSZ3GKu=xI~(}fz#U(&x)ImDxSOnI5f1%nqDO9 zV`~DcC&LuNxf)tmoNk3v+cQG-Ojh?P<}_abEO*esCR+QUQO|3} zI^pS(`b8umKsS?U(mFUXnbiccV!B5ZS_fgKNZc6NdaV_jBXUkq`PM<~vBHTvBqqEY z$b~iej-S?;rVO}&98v~>|H9fb#^UDBQKQ?4oD=z)0-%Uo*5~VzPi#W%!tjZbd4= z;QbIy9NOSa{OnLYht*?hMVJUJ0@ULp+nRl7f#1T)<(gL4tX7=HCmafT7v-1oF=>2V zm^Pf2Hk{>GU2b@zq&ZdL%^-uhJXWUjc6~m-H{4o(>vBNR%k=JY0xs>$s4%NA01Rsl zSg}u=ver8dvT{?#o~}(9Y|bqJlU8lYTKb$&j}Hjs?jVkY+?7DL48=5i$ktT`R81~= z9Jv8IP3$V!AR*64gI*@U$|U_cExxE5~Y_b`1odH_=@F|L_~M7tm=2!>B9 z-s>=Y6vRgHmx4tP=V&g6I5me~U~A0UDsAO`lXK1O;Zm+?4~OZZC6H^krp{(LpkkLw zTvQUjv1?(k+Y?1&R9Fw=0YO{X@wPrW&&tX7#w|Wj60#Q!x&*+->m~C{>2L z*<(d>IgzZgssilYo}AWgXoQAvPWkxOMY#4o#mQV98$r1HMsPrPk4G2fuOc5vT6gG( z`YfxL{6X_=303z?#8t?+!6ijKT)RJl4?6OBOz;Iv5OIYT_7~`R7{y^2sk{Pu*t(6F z?y{;F^7*Ra4*?R&n%xIIZ#{r2ElfC)HStp!^0GSsPP(Xkk>CRm`*~8+dYqUl-TTc! z@F|T{;hW2udIW#7XO_fEnmWm-3c3qtB%e366iWj%foMGQjG>3*p2}1A)_;oM*3Bf7Ksq#U z{W}IRRg8#*0k*lPx)t5(2_%Ir8_`uW_$rK4N(g&u{Rgha724O&!?o4iX>e)`(JjU_ z3D}JBw18t-WA$QGD|a02*@T*0Y^2p$L{K#(AngOK*e7FXA7GG`#=ss<(WrTL1pBMf zvG(jKhy^2^q9w#0W<8ZU)@IMX=vezu;Hc6u_EhRv`%vi^OUec@j3hcb(Ia(JPoSIX zMy2?&!K9I(eS|Qh%j0Z*nZv7evVFJ#w)mt-T3h9puGBG3*XRmdzrVPwO5-XOR)addlNL;zo4B30ULS1qJOgy~7`nJhh3cDKHc(NS*p z6vee1{XFzR9-%3!lk(eW7=lj-VQzL?i7Du`OIt1~dt%F*ba~hKZrbGf#i)O?f~s%Ud+$fp4X1wBAb({&s_M>i>>VWwf5s5&}k` zY4N*>}V=TY4^!g+At8BN_#bCj-KF$0QgcE zVbYKgpR`j{81B-X#5&R48bL9N;xa3G=AnkjSglw5I6asoSv6)om3Fz3YEXUN1(R&e zBh#sxX9fPFEB%abTfdU@Ds*l0qvAb0Wg`O54!Gd&d5YP7w^gRI;r2$1jBFT#+Sj0X zcVarb(YTR4R-`s8MA7zK8VUjMh`!C26NA~b<^@He)Z~-F8NqMiOp^k&(J#pK6_$`| zwci85iA7tI6n9bDH-d3dT#43nR#+3fbQ@1;wQs0e-C5`Xj5u&{!pu#c<~9fui8r7zh{@e7 zpkEYFH#g{zduFFVKW2#9{|(sqniuz-^51Z4?RR0K$YZ`c%?~a~8!oT#snOPN-+Zd> z=7lrS)_aYN=Cv?u-ILtL>J@hFd@9AaZ;mv*e@GwNUItuKIMVd~A^lSG+8`}D(nrAf zV5mIHWihRZe*v6MMz$ZeCe4wA>Gl`cV}&#EG+~7AclQq&2Bx`xn7kgy#k$+_R5hp; zUAnT&M{yaynr@fvhXE-QWze}6mts i&ADR&TN7@`)|*mtg@tO{%!tNMB+Njxyf) z)Ilz^qj@b&@aL?8w4lb)r0zSRZ65A)WtLnI8TqmemvYERWt3#ByiFjJYVg;Q8U(IH zq2POlk1E%G7L-kMYTo8?Pf!jHYJVR%p2f_ma(tIPR`mFPog0yGrY%nsGEh&S5P$|q?ea^Sz4;GQ0|N!5%!PqG_qqCeMO8f${fYU2n@ zYX43Q_QIlvVj^Nl81@iO*Xp+USWA@1ILk17@HFjb z)A+c|$4A_K{;eOhf!-)qDLQ&Ra?x=GC{c90DpXgpI{nSVpqg}RaHH-<1?NGdb{u3- zg|iF@C=n`DLTI}A=m#73Y4gz!P2uLFAM^BV3U*r?Vch1UTanr0Vn;=f;`zJSlj=W3`PGL zgs;?v6TM9O&rIk=4Cp@*#hF$#lZe-UqMuGPan3W*DEC9Y2KN(y>?18TgDRF;(M4)9 zKb_p^2GV~jiNwnKPf3=3dN-4}v*kBF#oh${$q9P6OR+!2 z?45i61%PQle%qTU-CT(1VHd?HHqn_IX=W)rI_xtBHZ(k%=)J zDY?n*8JqHP*7B$2`meE9h5g4jfh>!j#@~x;eyJdCmBm7Fi$|>JzYfI*t+4lwQR*$s ze7k2V-;&hlV#FihbsuOs5F>bu5KqC0>61P}-osJqxG6%*H$U}Ig?46@xb%u9ab4eo z3uw8EiYC_pij^NG4BwULzuv(6dA!Wq3=TDPDgyclfIh~>^In8sOXlA}giPWegf_)r zW4{JH)$_;DeW{*}Z9ZfLH>S0VsQV0QGGFS3s#^fndqiO0u@9*F;gH-hz;;wAU9Fy| zc|axwB|h$}`OQiyWYERp?=T!=`nUG#*#r1KRBAh%i%Dzx<@5fJ0oerIti%euVlAd{ z{>Un|U*VF|-f6lVe-F0*7IcMgqPuItJ59BE(T9fp*;>90i<8D$9=#81-pPKjdt_*H zrHtrYiX||K>=YD;NtBO!e)4^6BtPFDsvodwu>?%XeqjF^E8GtUHC7PQ^XTSpPX%_% zxyBzs@Jiua7qBr#QLk$h%FJ?I*8*ktvWD!3n5qKFAP_m~4np1Da$S!9E1rc%D^+GE zYJ8o%phJ)zk{i`}XyCO~rE2606eel0*k-vjvTlVF30q%UXKx314MrS8_0VyShPzj$iZ z&VE6Ri+J4)FI1Q*ec-aQUpFK%v*^4EI3uY8agNm$y!{wX@rtEkcBlq{`timg5vAv= z{Wl(AT~TBfbx^kyQ~!++kkk>>^Ff8q?mLZ^9i3}5ByrQe)X;XKkT~j zjY>iIf%bLFol7%-{{Q3f#(Il^H(OEd#fX#6RUh6CUaWH*FuoYc&NG{G>xYF?jPZ}) zk|+ELwjK%6#frh+bYPUvPy2UfzOM@du21w@A;eOV=W7^`zUIprOt zXo!@0H;{-rtEG-o!=+GIoeU#dhq%$rH)>hujTQPwj_Nr_;v~ArbLu*Z5=8&T)LcLb z)vmLEGv9@4HC9a8`LEVXwn|_+n@(_0m7M^9GpKTBe&U*7*YU*Ef1;yr_Q^1wYwyWP z7EF?pP)d{gVMEpboE6M~@_U(Z{ZCvg5g`Ncl~4O=cKhori$Z~2_y4UG`Mv0hcS`cx z{ePnn)2)mB;JkY(<3Ln#-TyEO)EW<1A;HOgXzyg0y7JT;0F@@YA7dky;F4YPd%ImK zk5ztm7OpwIOkAv?_>ZG&`0pAkGPwxuLdbn$^xVG_aA`(Z!F)3Q2>>s#qO%NG3Wi>> zcBfryufY#Pmr(W-4d}4km;^!AE;iF$8k_ZL=*}_$fSfLX_rk2!A+MbQM;%DQ1H$T5+Is6qLk)_c9a3@MJiCq_;z&awmm0D*4Y~(7b|hhAHyYto3DXl4@2VvHX~L677^>Bz zw^7M+=nv_3ix1$*EzQn7p5^*gs+3zaOpzbX!=q81FW6MvNpv2@8Y>^*>wFsPp(b{| zkZ=Nr;GIvS04Ddmk*8OFVF!q0RCUvFCW@TPeK=tkgBU?O8k*a9*O*Mt@sC=sV^@Ot z(Mrs8UOY=xY=R%^JXD4GG4yP=BK`Dl=P}QC$&u#29lEO*I)IZsijh%51(NkKf^T@X zYNw*a10%I*R?cy+U3Tsb3tNP1zGxGvDrh93(RV9&-Qj6ul&x$hCLgjXyKGO>#=B@6 z*`L-JR@yQkZuH_aO$^m_zSXL7^7o*o8?s@lPgz?&cdDrX0AWY(HAYA=K5Ht%BU-ra z!5*+NQhew5(deT+l(Q?i*h8SBBUjl$@s%5vPYm0KvQqI z1I^990^rO20TQkjV`;@-p}Lz@qz#?l_>kQxG^;&%nuDoXABx45__Hm@D!abQ6Nc_k>KQvT!wty-hq;zL+ z?C+o~KRbx}FR2`OQbj-TRQ$EoirJ8jB9*?P`4RwrY5!*IhZ>cE8gCiV2wD)bblx$e z-m#hp$hI7XJ_gY(>Du}Zv#uF40AQ;hMv6&deu$QBtp3Pq#Sf?`d(f&MVLgBijGIW! zXE49E^Mon}*3RKlR}tarwtC=S7OK_(n(adW`cs~~re`L+3DtO8%jogLn%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