From 3683448ace9efb97a00dc879ce4b435219c0d863 Mon Sep 17 00:00:00 2001 From: djvelleman <110697570+djvelleman@users.noreply.github.com> Date: Tue, 17 Dec 2024 12:30:06 -0500 Subject: [PATCH] Update instructions for toggling infoview --- IntroLean.qmd | 2 +- docs/How-To-Prove-It-With-Lean.pdf | Bin 2295536 -> 2295515 bytes docs/IntroLean.html | 2 +- docs/search.json | 2 +- 4 files changed, 3 insertions(+), 3 deletions(-) diff --git a/IntroLean.qmd b/IntroLean.qmd index 1e98a2e..6c5b62a 100644 --- a/IntroLean.qmd +++ b/IntroLean.qmd @@ -58,7 +58,7 @@ We can learn something else from this example by changing it slightly. If you c theorem extremely_easy (P : Prop) (h : P) : P := **f:: ``` -This indicates that Lean has detected an error in the proof. Lean always indicates errors by putting a red squiggle under the offending text. Lean also puts a message in the Lean Infoview pane explaining what the error is. (If you don't see the Infoview pane, choose "Command Palette ..." in the "View" menu, and then type "Lean" in the text box that appears. You will see a list of commands that start with "Lean". Click on "Lean 4: Infoview: Toggle" to make the Infoview pane appear.) In this case, the message is `unknown identifier 'f'`. The message is introduced by a heading, in red, that identifies the file, the line number, and the character position on that line where the error appears. If you change `f` back to `h`, the red squiggle and error message go away. +This indicates that Lean has detected an error in the proof. Lean always indicates errors by putting a red squiggle under the offending text. Lean also puts a message in the Lean Infoview pane explaining what the error is. (If you don't see the Infoview pane on the right side of the window, click on the "$\forall$" icon near the top of the window and select "Infoview: Toggle Infoview" from the popup menu to make the Infoview pane appear.) In this case, the message is `unknown identifier 'f'`. The message is introduced by a heading, in red, that identifies the file, the line number, and the character position on that line where the error appears. If you change `f` back to `h`, the red squiggle and error message go away. Let's try a slightly less trivial example. You can type the next theorem below the previous one, leaving a blank line between them to keep them visually separate. To type the `→` symbol in the next example, type `\to` and then hit either the space bar or the tab key; when you type either space or tab, the `\to` will change to `→`. Alternatively, you can type `\r` (short for "right arrow") or `\imp` (short for "implies"), again followed by either space or tab. Or, you can type `->`, and Lean will interpret it as `→`. (There is a list in the appendix showing how to type all of the symbols used in this book.) diff --git a/docs/How-To-Prove-It-With-Lean.pdf b/docs/How-To-Prove-It-With-Lean.pdf index f58159445d65ea1bb2d37ea1c99b161eb9fbd6fa..5216efea2db616eb6c536505dc3c885754925fd7 100644 GIT binary patch delta 39602 zcmY(~LvWx?w*cUYZQHi(iEZ1-#O51kV%xUuiEVpg+noFT%UjjY?yOFAS9KlS#zcc` z{-=Hj6krz=gmrOsHaE6|_1w79owUE;MBaX(djzu>-@AnX*Fm>}b6q9vDum;U?K&^~ z`X~N|t5Qt9IZ-5UAL0Wh+bBNc7<=r*jr&bF^yf>61^f2j+wEhT(8v0}uQ!W4A%4W& zf8>yV)fr!mj9qrz%95>rH zyuul5?w23qXDy*E_CL>0^Vd5kdF1|#0|hwBaN~GcN_@RQs(r&vI_n zH6%}cVh(~I@J$2nA0<`!;ICjw84B^3$W{8w3-TjZp#}TDicZZSCNW-Z!tmhC5nBA}&H$yV zB&yNzfdN04@Uk0p;CR1Lpy|83uCyTy_GX0#xxZCN%Sa~KC8sK=3fp8sYBp3jV>E>h zriFJj`ZfI>S3it|#L3SYN3gbqNaCYRR1fMR2r&J{+3G0X(!aT)uFL(|Nt=kPXSfYY z4*7=EE%j+KpJH6FKh21_W4^&Tu?7VkZ8{BLYqsNIJ)#q=ta30~C!&Ueuu3zZ8*bD()q7!lhb zqSYdiz%CERu7*aeztF=sz6Fp9A_F-P(uNy|Y9fNU-u6adS!PnTbLG0uFOHn9ATUGNUR!Lx)(BgJwYyb(5U-5vNBAOTPy~%`(()5R2r?3+)3Cz14){@D1s#l+>y)Eq7fqCLS9JFrVb4R)hcsjxoP8Co- zY3>|b;BhNKolf?XL<1(j*|a@89t=EfQgQOqtfDr>$#Jiht!1L=#SbZbkh*lpwreT; zGO~W!QA$@kRcmprCRtG|N+^nYS5jr=Poa75sWd$|<8>_|t9YV*|KO>e5ivK*cMw_nOjW~OGh-lMWWguPxg@hnb*k(_{VRHTBGVv&heeyfvAGdU-_ z9MM*E**B!o^$66DbnGy)Btssvh+sFVnMetYJePmG*6>Y4yOW~6jjU|ko9@|a+rqh6 zrA@#y`TwH#q!ExDH{n~2y;Dr1cZckT=@Q58?0;X9J9zA$-|2CY5uH`sX(HuUI*xB! ziQTK5s%}VE3K)M`XroT@K9e()s3NQc7!5wvM#p6Tgacx8+8F23#at}Z4lxllDtMa2 zndL8nsr_1&JN#~D37-C<3O5w|a-EceAFF*|*+}0cP^6_7cCK4GyjB(1OkYWR7)ivX zG&j<=e7N4DG<`e-7hlTroLzg1FO^^~L`zT(e6HD@G^&$jR)WmIK{j(aR?z*Wlb~32RaIz3$w!cVX=!o6T+?Him((=D zIS_u~ZT)^&z4?YXB&pO(BLT%l3%-E~zkvby59oiu{saCWi2p$T2kJl2|M_1G?0?|? z1OFd{{~-Pc=|9MAH!vs)yI^e0JZW{|s2IShsdKtc4^h7nGWc(V*VgeJc%ss_vKLe+ zC+D%7a8mIIm5NSFPE$USdP0vhnL_GF2W7wavtmWq?=w~Q+dN*sZ=Ef1YyfB-Qy#yBc4($knX#HxnNHE+0{s=3xn%ROI^#mdVi6df~H@|HPvBE((= z!<$;b$-6HShB1c6-qb=-N01g9L;*U3XURd*Qd>2OPzj?8FzH8M z!O#m8ieT;d7AnS_m4$%sR{ytA86A*q25e-_lU6f?oB5wSTTdnSA`uy`qYVnT)=ko@ z(#7cO={LWy`IPJf{=ExU1aK^XbQ7!+O)5X zEgdDNmT4{wlKp1>7~?))gA#MZ`u^=bAQZGMDJW|VIKw&a)I*MR(&$Qlx!G3FFbjON zG-sN{C=;nnT37oWjS8U5Y|;u%)-;LO69^&<{lR=h4vV36*w2+~0Zb>rJXfGs8XL4L z4p98E_874B(~1u{xB?w*6btOzd)$|qjAjN*dW?`4oZ(fmy*K7%thbbQ%@T*W!p@zg z)B{(%%p1RRDNe)aTF_yZhc_1N;_H2KDnEd6^BoYlFqJS;YLnIhAm3 z!y}JOx_<9&PYMn&{5!|D5eVnPJN>qf1)cQ@c7b_)v<4V&8Eugoe&{GZsZ?892hXWh zNM0F}udTfwE|`a|ZnyaK(d7UAt;Mo^3Y{D(bW*2XA4~X59v5KTN?Z^14tsg0o1ycF zyWx{XGxMVb3)_Pg@rEoDs50D1?)wo8#ay&by1Bug>0b}Lz{fc??e(XE4U$3C?+Pqr1G{6E)9bI149 zk21QiDZOl&Ed~THAyj`+jkb9?Ylj`tQEe78xDj>TUQb+XqTjxa>pbIg9j!PR!&VPm`e*Cqnuzc5T7>|!nVb! zk>@UR_$MZzsnX|*puI(0*DmEZebiozx?GBQ?fdQr_EHPN#3MVmSqB)yEp*Nw`on%u zpGA0ZPp%w=H$mECU3E<$mY(41$i*=;ws|sjO-H<5i}xhLT9;X3mcNlK&zagDuaaou z=KyN5P;fotqTGf_(QC|d@;NmjNGlajo3HuIUc*#Zt@{fd38F*BIdJfWn`#Rfo@`oh z1U;BoYI0)9AWz{HR(~z}VT^cA}z!5=_nIr2n%%P{_A87vm{^xNMsj z9Kv7g8$4dhUavW2q{D299B3`uNzr2ph`6Agm4{O`;nm(a*W++&HF>!T5KWYhX{d-b z>yJ8dR?rtxOa7)I>YiUfMGo@=X-Y6SlQ#NOKJE8bUljDG0`i8~n z9P%;ZJLuY8$&+6=`#3&v*U|++%;v(C>lw1aOOEYl$!LrUDL@?Ob899Hb;g5#Sxk3#SpL_!vt+_q@D_}YnvDGi zq33eUVUlfZVEGGi6|^^cSQ*rpC);s72=?|iN?3OXBbH?N81RJKm#VYf%5?QTjTrzl4?jYac%A%e#%G^pO@S8y%*y#Wn!5M6JhlZ$fp zN4}l+{h{lfWzr)|FsdmWU_i(lOSv)-meCdt*6g6Ou%64e%7&5gJjOXAXUXMvnXg5^ z>K(tLRcIH`FPHdni`;x&A;@klBCj18{A8Xlk`0RRrw9|~wvE8U_~H%+%01%ZpmI6! zhjP+oPR&|Tq$o?l`!RpmPmRlv**Jl@bKBe)BObnLv?kL<88IbZK(|9&GBxMj{hJ!z zW>f;RV9BYeiQP!;sb9v~Wvlw$gF#r?5X~zhPnghDYkeW=vBWSTwY&$40Qeh^c(UUa z8Rm^&zfW0DO*`Cn;XYJ@y_eehOS#%V8~rTciRG+l-SytX%|egja|ctD=%OQ^i)aUR zxq%Kod2I_{LvlJ4aA0m)X^OXMa($Y>>w2I^Qt8Vy)hp$mHrHe<)}fblcn_ z1&)d68pbITDo*TwwpjV})y{dc#6xK49z}!aU`D_TyM3!B`4`JaL@X1Yl&kiWGi~}F zw~Q7W!Dei;Y!i19BOMCJtfd8(&{{gB+y$mA?nT~9O3oaTg}E`>kp1UTp;?Z)RzS&# zhcs6~p^N>2QqYO5JLfL zJ{rPOe{OU@SV&56Xaq=)M7mC(WBnQ+MeGc)ij8JLltj+k`u=TKUVAr__WxoD_4=4O zDcX;EQHC@$bloHNo;fZ*Cv9KNX%$iIyN9h`9?ne!F8U9y=kRnhmuu@gzI)!F`h~9Z z9Wx~&sA*qGd|#Rzus>@82yE9^y^3Rn&rzK3mfG1LZK2x?2ZWQaQ;F2{;2AXtw_TFB zNrZQcyUb6EZ^F9Nf2)r&;L|l#^;7*eN4Wea0~^iFLhu@o6b#bjOzwqXIwxJzDU_DQVKE2`FU z4H=NUQn0KW3Kq=rnsLS&=GN(WdXzcyTdi~$=PRljjn1n53lwj4avqNOZso=a4Po=wPj84rB$OSP0_z(J-P=)ALR9y4B_rLhfZ?2< z+n!$36o?c0)?6{$W;GN4E)QdI}%Cmam@zkYuU zL|d96pc8xyU{XZU)!zlxoMcujJ{5@+AOk>Y) zaOq8-x4DE(v#xwyRac!|8yIh%dHD8Jl$Dxp+RFWgoW%U5eD|`c8}p*UwCKv`Wqz!- zHm)X0`(IJ173DD-d=?FIc{rLki{ZM)Z`ah$FY#Z|20e4ZSKNk1dJ|02a!x^_Zkn17Inn_qpaQn0!kKim{}>~fAK+ZR6SkJ zNTl?LJwaWSOIUQ;I{kzM+O2MmPuUleQ#R_b7%f}zB}ns_ zpjPQz>+%Qm=I(d!5}l|uXt<5d{NuekT#k?*7H}LP`E&SX`KfU52%&p;j{l z2VJbiX?vnu#D1FlU;L_39V~P7lQFmiud2h;GCZ9A*rQ4bGKe3-DZt{{5uKfiKyzrT zUVhb%=St)2lPCgOiap@7qKxo^p0XC?*}9kT8ISX;TB0Iq2wFYqs*uNfH&%9+&leM8 zoN&OV*)*LYdcG5~-jiT*5#e%~MGK38{JXFu3_TF-t2(YYQAHiK9BwtcaSTMaqh{(Wtw+C?rl;!Yo5@Wq#=_)PnRQz-Q>;+~@$S9zQ1a(%oK?%# zBm9rZ{fnx(JaS(X^~UEsFyY#^*+KjrcPx%apNMY8k6IN*`Gx%s}b8je=;Oxvi zoN524aIn)*-chgtKxmjWie69$H^$Nqyx*HXV%h>DYIt8W?s||3$_x2ck+3`H-_YKX z!m-|omm5^g=bR6u&WpaD^6 zy1dv4vEWY8!T%~9Z-vTdq&tpFI%&EpFQ1d1B(z0e@;*f}IOI>q;cy0hw4uq9(I;JN($v*{9mlOx& z=aQ{Jwxtt*R6*S2r04*fWOn!9vk8A8{amIeg;BFgZQ+UCM5lL1=$`o0CR2T%d0t+& z4#R25f_!4%lqfv|K~d6F?p$@HcpB`K)UTVbrP6bP3`?BmOV~Sf_GjNIF|r~3&iu#p zPXyY60)|wMr9V7!J`L`->g!6Yh+eACKk?D6D?(8Lv8wURl+_;;1|P@jA`;4}m8V7H zd9Qr;J6BleH_pxr0j1*u)rm~*9AsVn*R`F$7qE&`0_$wFg|Z=>^KqeC1m;>2b}0i( z>3kurOWQSy-L=!-EF8|K-HPH17jC78RhisyeUxllSVCi35}9*1a5DRT?UW8Ltf(PzYrv4q!34#~5=V z7$56Xg6sXroEUPf|N8Lfeid%>|CS#$Li)#3eEgZW_VZ1@*N;&%)@$lMkj$?Z^A&SA ziz{*vDVzuhii6ww`0oRB)aRK|}kgs5ShoHB6nq+c4K^^-?DEj{7MsrB8Bkvv2d znDG%|E}+$@M%V`rT-F2T;`_OOvUh_#2qM_|XTU?BJ{f0>xpV#q&+_CG;F;!vRsUAo zn`mcZE9}@~(Y4ID8R>O=SwxwGiA4s6ZNOKuT3ob2z)lu+oKz%xz*2;UL_eE+y^yXs ziEXz#;NOy0D?Nxh*|sC@9NoZ~?wa|NxRezXsBqBxmCps94yXJWA>>B9zZOQ8z|GWL zP=5qLivO8CBJ0WCZYV;bi;+=gUWMMfZV5a&M&US3_>(@3EzU_CW|cpam;V6Jvq}H? z6>s3e>gq&#uO}M#1y4uxU@wJTrWK9TE8_|_gV2Pc_3K9^H@r$NZk+El+i6Jy?_Y|O z6#9ka<%TTS5h0@S(>-SpXkyU zZr!f^qjb23xWk3Tg#DO-O|(p)GnoS8FA98p%4>}MG?RWNCXufEjkX3+=>unxc~l}s z>UG(bxfJO9ZuUj~DYtWx7@0}C2p5_0Y=>QiYo@R21z>U>>f{C zsAh3OP+R?KRKDtMV_>$&u!ur`rJRW059=q0j6_m;lFk`{hUgP5&3V!P^^bbKL61A; z4cvIJ%?RGE3+3jmJwlkJ$UWI-Z(=^L*Ia2YlqsLoPmH_%e*d7fvT9eH4D&E$D`=76 z30#WXEw6%!+WJ-qHN+A?2__w7GlYn-_lZ*Cu>GT_ce(z|IAPEV<_U{&OgOvV;AUxK zocmUG!*BUqPTEesf|MoMXK~a(lT4Y$!rP~fSu{w-I&^0gvCsY|&c*2>ify*tuv+W~ zQCWnurFoLA+MCw!g-kc=B%#+3nR0Tj<-UuCa_4=%23iIqemfbEJ!RIU#G!>nt6PY@ z{>Q|1o0QfOsi&@s0!r{G34^{dyPXx4t7=@+N*X$C30a#;|AaFyTfTH!!Nil=EZ?%p z8z13yTe<4)w3}TUmjKV@>a}`n?+ABar(Ux&{%*Rj(!IfoNl0}=U<(zM1v4D!5`BzB zaKrQ0Zxj5ag-bc0%qXJBsTL~QQH-0T=H!zSVtmkxw4M))Qo04;_Jm|#_tg%u2NUSR z$&K;}Bdp`MIW=$eH)v5;qS#OKFM48b9JYZ&VH6;Z3U{GopoUb`jIqWI*XnoVDun>iw75=Fbh8G3@3wEH7b!`a3z<+uC=*K;v^VZ4e+LeLdy}-(VR9Mj2 ze3(K$Gf-5u>`uJ(cPo~!Ae+E*(ywe@wp8@3-jUAglXr)dE%BqiB^_cemB)=MSeff& zUyEA1`=VLJON$jg!*?_Pm!0!Yg^is4xde3DLPw5YH(dn*U2~g!mB!k5LX!=@gG1+> z>u4623q&Fy)%k)wInww&)H;h8)fL8NNH_-HNPeYj3OQE?(`}4S9cV)cfeR87dQb&| zTjteV*ucrd?iNPz-Z1ET;-u9wp}v(2PaBMB@i33@?nu^G(vR~SEw&{gbabV#eg=uB zyMBu4-F$?xK3;OhIW!XjE@x0pHyz3*aJxO$NYx~h4KvAy&fJS* z5kpzAb`p-6|C=cF%=OhizAV{J_X#bOO!pj}zt1wZ&z-kD)3vlXOWRxI@=<+%bAG9c z^Ir!Rt(HEpPw)YK2hJX8GD)wQ^}|-OjOQz`c?~B7=I2|1j6_|%PTdqaDO)qI5dk7%lGz0oQ?yYt>jYiXql`KE% z9z(<%tY=HCh9MkW&?YL%E*AtVy3*C%0@(qLw_9e~ibd~WYq|rbb6IGnM-I3+yZa*0 z-Hk9pg%=DC8=VwAHzfj9T01Rp&t`8^1h5X#@i!Vtr#ULjuO^z`!Sg~gL|z#Jt~oZj z_8)R_t<~*S9M05m(fnO&EF$$$& zeVG;el4fn?ztcjv+~Mm4G=<>axUL3`F@9ZPVG@%GT}3s}FXF zx1rodZkBaVVfnD6<*wB0M;)iSR_H!R5ivR zr=mDd6xKal+)VzI7%#&s^ZaGMUWFc2rIL{i4o{)DwVbdT;=nF;g0)U#ygNZV3E=5T0bQxCp70 zEUkrV`0uRer3{^?+hf@d20w1xGq<&>9#1pxsnYUx)jdC})WT~;8ryn|-iJ(wr@9da znT8fgdLDY6vhMcqv&)}L5O$6+{r5jkYB=Kb+D+9t;!s-VY)SX@2ZBh0WKl*2qTB2O zRd6F_5tltXl6*KvX(;6fV5k$nKnd*nN2V!QXC_o>lXkqS=^`uFT{eE;T!PUkER#-e zS{LzlJXPR)9vAyqeN@3QDNX-e0!J>TZ!8+p%F@8vce3GiAcqJS<&$M?RjC4<;+h~Q z64w|ke&h{o*U^B;1!}yYF%CVe8A21(5uL03(@C2h>M;aE!*_qExH>c^B(_ak-CVHX zFKfJYjf{D_G!2bCppwBWAW=wMoHnThl64e8T*_6XwofVyXkG`Za2DMB8TR+rUq+oV z-&K?G*i=&qBWpdd@FJ)7)%qp3z5)I`o}mXvS}tx-OYVvb09`bQ9xhzuhM=;aT~`m3 z9Pny|1q5x*VubBgtQ&Oq>GEJH^>W8!TeNMetLk4ePKugUpioNjaO9*<*v0W2EsVC* zCg^bxc81j{73%A4ktSh5=}-2sJ6mnHRUFR7H`0=e0<}h+xDTD+IS)a8-gR!jdyzP# zA=oGCr5!wcfiPS#VR{w;E?wkJ$84K>`9xHuRInpFo?|ie;Pt2aNb^&3{m$IRK&cp7 zcbn|M6CI5i>7xd7>?zYDuHiEx;%e)-UH^`49Eyj4Z*|G7pwKBx6VYJjMd%6KW>Y{J(rrd0O ztfZm)El!b8n0Bx{i;LmojLV?D2G=#WZxq!!KBblp8%@-7CX>{q5Lwj%=5QPo=x0t4 z7@9c3K#Qi!WK^21{gaHxmK6R27Irh#i>am+nxbEQUGGc*>qa&UOQ+A%yGpE0TO^mR zxZgv-++s$}K0)-FPz;fMn03TJ`y^Z}u2^Qz9`PbI-`!YN-17yEVDZt{=;LZ_2;_z2 zoKD2HR0$#cU@%j;lsSvReOr{3&&*lI1ujPWrSBE#r#!+C%Kt+y#J_1&&uf+kk)$s90z&*7Y170u%FU?yG1ul?v7 zk3LmqbOjG7aFjv#*R4@K>NX9%Ac28wK&s>URfcTfE0X{F*OyD&qYsbBSp?QCo2ejMiFSX`}C!R@EKS-}<6>xjnLCv%;-MP=^|* zor!g;1RQ18DT&r=zMtyz(PW-3mbpRjzvAZJ_byH zKpd3;=FmzH8&qf;e*gA`@9(>V`{_Ipru-FoyL#Vl zM&zl=YJ<6IiH@U#qdG+yoc!HMHpur&&UbYgZBN01GSF_7ejxNa_dz!J&fLavK_`u} z!P}qJfJWZ!uS?~_;OI@NkRQL<9py#q0lvm zvz1)8?}OzKMfD0eQ3Y-nXoVPt_iEDuVRCOGxBF%;`sr+m_9*1xD8EA*F35>YVM$JhPwCz4T7JQarm($^tlbVhw5+XPzLR>lC9 zv#N+C@Z#QkID2eS;Na$Huqt1K z^y~}w)B%K}D`oALHuC8#FDSmBfsWwx{S&%99 zn)au@nky?K&JVMg?xI8sHc1rh5fnu|16V0Jj>?e-G+3>4nL_PX zMLB_WMLRBntgZ98PFCGq!zKYcuOS5`AfvVup-Mnp;`oL4s^u%UlNC;x=gP;&vu072d%Xp#B_B z@4ev#{#-21p2DS{QE}cH`P$*X9l`CN^eo6t`(b3WP%DBoxLP&Pbd=J+|J;pc(>lsa7qde8g9J*_^T&g9YI09CQv|0b;+_+iKHqFc--^4b3%e!025Z_qvu5rR< z(Rc!lQs!egQ1+Ma#ggRtoIzI$(EeAQcjb5E?72Xwx#pPNw{6fz-~HENCSnLneq5DB zYo0}Lm32Cb=G6%qEifDb;j{JurbSHb0Czh;q5O5-b)qoW*0D4bXE6OE5X8>f9B!|r zm3c@c9;?!9JcYp`T}1pIUfo#xE4X|ZyF6|lv($cMP>!kM(FyI=2D^|QpeH=Klp{}C z*6zttR8*@xzNMXI4*em4>&IZ?ja8=_q$97zL**-Wy7I#wrk;MTaMPpCHtyPux$`SkR3z|g`UT?NK>ajEiV;&=e9QG)9%gx&5?{eOrmC_ z-AnG*Dv|PP*2O!SYk6yf&^&21EZ6$L!p`PjKg0@(PP;=usS6Sw7BriX%X&?ttAEyO zhrH7_P78o%{3v&-KfbbL3aY4c-G8)2{lMaNaW7qw-`q^fRBcUf~oT8^Z*L$-Pui6<3RS^U@5fCr!REL}p8l`M_w*-ekBK@hP z3b_{DO)=DO?{!hwK|3*?r|CEf|W(gG!Kr zmHo>w=Ey>>hb`<&ed0?tP)i=--L`10j*S#zWI?oe5Pi571mVkp7#0G#k#=ODv(zi1 zpmG+V5<1QY?V&04g_BrRzSEWLlQiQZIqH(a9Dp4zV`240+bEvBTT_^uOk7gifNA}t zMYV>orm-fqJCFLA2woyL`ujzGJEn<@>eOHhEZ~j6Xc;WmdPse7EXi5f6kNxolt+x* zi#1pDn&Nx~l~(1m5nO8#)_bOp0(0n!@hcFR;m?2?qwv(JH*`wIF*R%@G@o!G3ud6# zLBqfmJHQcF@W2*p;lUb;k+y83SzkR4XeLWuLea}HgRNt&%AZACkC}Ccwo=RovtE@C zDh4Yhf3E)ha7;y`P~o9i-8o!n0|&%{3xuo*48D`sdrt_S$F_NYx2rW3l&TL=M1 z+)V#P92vhs)A&5sGm(1}Mm=C^!^(~{B~^?4zCSEMmZzfJY1FcdzmE6HGV5jG7@>W+ zBlEN1QMMHvZ~*#-I4;DF;{j9a97eGTM!y>xWY)*r)X>@&du?oPN0g{1 z{3Z7K>efUCO~nBD$%%>Zl5H3R?~R-%?5?6K$`gTMcghvemFj{DgEddfT{Mt`?~RZC zHifSI$Yvj3L!V|gm&fB3nwB=GZ#kbfA@7{xVK3FVyN}@Zl?LqWbx;c~6>(tNOQ1d9 zRI^bi!=EjSS*^_G)Cw`$6*kX(W!aZ*fwu;nRAcqMM9E>j)VVL*SMVtqpKHJ_!*BZA{UpLKO6PU z9vzxbvUzXc#dh>|rR}c%1UFYGW|pCK8hf;r>>_(twAu&x>q)ae^FXFEA;GF0Pa}sP z{v|_-@ifx5`Aa}=NZBFo@SDc4J~d}V2~z0E*_KB7tnnv`|4 z&h4yoOz1j}FGbH2UuuzZ2$p%R5Vd`TuiY&GjuuC-gv*pA*bJxy2aRgl1n(uJWR|;E zneAL0>_uZ2fqpb^R)^R=Fz^U3ny+k-%(^xIR~6>q6`xLl&$k(j%4+5Ekh&{gd?U=q z+!5a?8XiQsx|}o7ojNwPX{|8~qsk^^986Tz{Wvh!di06>xS2lH#y?uvH}uAGm|IK_ zK=HtGtMd4Z^8jq(1#>?Z*&dp>j}tHa&VI~#2dQYI!H_n_VrN;b9f_Bcxfpczx!a>- zEI#sFPA*GY=D@^elTxvWl+h;Z_`J8~thcxjX~;QAg>vezsnDkM!y0az6gZm5luy(A zAh__{wY=yyQ4&jZ^e|?-talDr-I9W>M3{38#(kjM!UFX0ofF6Dk)f}avp=Vvu@w=R zqtZ(kwo#M3&uX7m5_tcLv`qc$H0GA&xW?#mVarH!fZAK0YC zwH)BhP(W}@S3sa%tT3*WSE}nWfy~wG3uDRw>>|OYAx0*d( zc0Oqu6N(oeu&2NYpKo?8d)`Yi<{tD@k~W@Ac$w{VbR&QKd5Kh&j$T1kX#2Ce$g`8Z zlZkpog~y%Yst#W`HWO7{T>SGcN0q{1_ZUul7UxYrgS16*hd)&yh=D7oMs6}vEZJe2 zvKJ8I$c(|{X>-pj?89f(y4(>}=auBu^1f~DVaWr1npU9h zsd-!-Yt1&TE<5r8z2bcr%TG_Nk6Wh?=PLYzCOa{)i{_}L|F+y9S(PjHYIa?p_qhH+ z;GU(V^;6-Xg;GPFCG*ZPn8hgsWs zUy~tM!<6>_ULoTV*^k8{2_^rL#J0H)juWHvy{)%%zm0wYW)O0DME~}(8cqc}1j}~7 zi;&w81O*a? zu7@=7zlO>92zP=gEyO~EIF^(}dIhEm2O`G8^lOq{_jXwV7(mrMMLLkLAj2x%N7qF&jNYw)g#E zj|u2Mroz>P=LY^iLWf`zGA64De3Gxc+wW0rfY?Uusof*B#~dZm(e}#ikp`_heR|GA z^AmAj&uFynpPKg!(yn5oaN6F|prK|Vhq@)&294FCo3g1K0V!$pw%`Oz+AGn;-N+Rw z>OSL*oE>C)yT#H5tRe&%6mZkOL%q*LC+|&&p=w1{67A)sj$^Ch=|xr7d^&jXwEK4V zfDPctCraI^1Vz4YCAQvTjbsYfH^l*NAC}?a2SS;8IhIq&jd7+WGgN(QwCf3<&04{W zNOq)TUc5}bM){z1J+86{AGFx+UuxHC{XWzI)}LogNz9Dxv3=bI{Ji@{m}Mw6r>nGe za3dvV9{gZr}Z(7nU0PNlMV-h|H`BBpz!&sGR^VBNEe*%u@{6q}BW@}%=eb-lKH%(=mS9fQ-SW&^# z1?$=T+T6B>U6?h01Me&gmM#9de?0H+*Z?2Mx$;TbE^Jl<0pxO;%|=0h><U`p3+% zm5cK~&yGG^(!(2u-u3D>-+u`GfQ3g~+OB?a!4=~zg@Wc>hfm{rU*CqH-qzQ9)^PB$ z;^y$q!%@<5&i1HgS6mO94q*0X@6n|D-IfKFHN2X4C8SU2ph=a72lW0-MTPOJXc!LRnXZCa_=0%W_n}bjAo(#XY9WrnBL9^sg~o z9ywNfjcrOwzI*J?jN&m{K#ev&4ezAXUDdu@OKpPoWyt8LTWOcD}8 zzmA>APwcQtT)#*ZP#Cf4p=sP1SKo-+ zB5&zDd&ABwp^eX;QxoFZJCz8@IZ%z)R88T3H<7}jit8oQC5_{%U9&IXp@Yjx-4hi4^-$ zhM(ozLuOidY|`@=h_ZP}gdy6e^w2RklO?Q^Ln+A(ZIJN_iuSr!D~pBrMUw6VmT#Gy z3-AB#sU<1Q*X``wGgV5iLK@JOy`|flaN`K!kg*ItUdly-E1j0dJ1(P%u|bibY?vY{ zViv{0DVH}9%O5^S)3&t9|8sbaF7A4AWHO$iL%GV^png)N@n6)I%FE6%s2YWBfI{YS-@P#peZqTr>mAy{Hi4$f62Cd zd*lkKF?Z*!CI45;=E2>L@%z5r)?Zp$wB>EY9Op{)jFX{AeTgf6p7Uex7Mo#-*tL&G zrEr!d8Q*sW$_Oe(atif?#Vj>^^-~y+itlg_Xx;xK>>Z;k`GS7onb@{%+nU%mCbrFv zZJkW4iS0}@v6BfW&cwETbMNzhc>bT>)#tZX_vv%iUfor@w5w`&05PKOyPOzf-fNF4 zc8j@S8)~s-KfDpsuFG~X^iJ*79PJY@Mz6aZ=hTQep-nWZ%N7keCM%A_`MA8342Kn{ zN36z~R&y;X&(v2rMFfw{B?;UXS`eRVTJXr5EAzT#J-yewuWcqD&g9?(?4#7=o{w_0 zrgn0*3T+ft>XO7Bfc-3b=jZeh?Rw`wEANQ1zjP1RTTgd(-v-$nz%gm8cQ{Tt5RT_@ z=f>M(U+k}ER$etdH*DGEDfc)z@`nhy{hDN@h1^Cc%EBk-@HGfM^Tk+KsGwa-85fE( z8~g*C6-fFF%N?dpay<3-<-b6pP}oNoAp2Wx3~sDS?;h?|1IdxFUSy2ikSEf-w;RT) zJt2`1Nsqh2;VzE{3R@3yrtzBNcUPnPlrxW`TlYsX!~0I`bVYEe<-};Jf0<8|Q=L;J z_RdCK{C#MMUD^U%Y&+WBe;L#ur&B|>4y^JrE9$N)g$MPtXv%=W2DjeXc?6a-OIHu14o!ez_Qp$I1xuX_+M!`v?R)fHuMFrHi{;lTWukbGNUP=Y?-w zXU7^4?rmU|MM*h}1V*bO-|ZS!+TYRg*AWC%q%92_9hL@fF-R1I77oXnf1=Naw zmF5HNdMvPZpXe>V>ll1GT{kAaPL;2&Iwu@sn;9jvDLguitr5&xWA0oha|VhYZ9Teq zHHz2?M(cbAOojC^Dp{#(b;ovb{M^E^J{u09`brI^(E_3pxImj1zJ zVpq{Z%3jiSa|}Y{is1a>H2KfQngC@J{6cH@sX(FR!#93ueGjZW96FHt9vVzzOJ_mL zEw;h6uPfZYjt>VeJ;_=o!Wu-OjO;tIV9xq`avKT4@niYA^Ys?4%nh-~Zx3xgN_1Ps zz+HGc*SM{3Yv-fnq53oy=gc_0a0E3WZe4wME8j~(Ud!gjCQ~cD^UB@XS(A3H&QrbQ z!{4T z+Gp2!xDq9jk-UCpef-!<=Cp<|N*6yhfsd$Sn7_gQpgY}f9Y{N>Y8G%kK{dSz#B9>{c%ysx>h@UtS@>_=bPZ-6Vwl^0$u0&22 z!%r5gSdQCb2Wto5uBF84q|bVXlbKxS+lE62oaGM)o2#kbjbKxp5jVV<;YE0NZ@BcR%ODdOP>zC`&l)0{0VmpTPeF!6yhmLG%gYR-{0ZWDvmmzul`G9no~k za>TV43~w+5F|lnt!#Kfd?u>(+iwl^5ze)kgX>QW>_=#mdrVF_}b9D5!!JpCwuf zPyF#4NVNM>y=_f(McN0#yt2&MLHcx-$D~{Xbr^~&1kJI7EVkNq(La7~r>_>6R~LC%6Kq)o6EZf)OT1yVyd5b&z8+up zBZk$gk8=-(0Lk`w29kT`Ptj`KT)dD&&{48?TzWzBupnN*t}|+Ob*h+NUlQG4(H^fI zJ{SsQdKMD*2~h=Ir%-n>@I{g`HUUIYLWkXCym=s>mQf(b+3d1*_S-GC-!%A^Qfw#_ zS3C|%8v@>1r!u+M%?j<_Tej=kP8j!*LzHgTw_DcQ zN1Y@JY46tz@276nmS1Sc|FSm3xi8V6iy_vekeTLufMtp)e9u%RLR5*sfX2JD3Hu%E z45km1z|~3|s1qPshVS7uX~C_})BGe))!K6aH&+}7w}2uT{jGEP3~u$+aimS`H$GcF zmK$MxI7QGl{|dj#xA z*t|CB#y`k2(JYiCHNVII;A~K&mmF#%jj@RWwn~B-unadL$&319i}J~x!enb@3Yv6( zHWsLaaD(xkjK~isjLl;VAds6Vd}<_FS`U0f+c91fg)-4vW5Unj2=Es`f4?O1sm?n$ z9lNigshS|VE^)KHSrVX*DRM>keseO2Q;Z~Yx5eH_wmfHaMVj3hc5t>TF(T-&E-?a7 zpkgCIfksU%Dc~C-r#Kp?C1F3R0vo^rvqPZ3zi3Q7{rMue@Ks8d-m!*+xOxi5IS0+D z&s`P^hCspnF-(=7{H+fE8x-x72?YImIeA#2vp5Tksx)-%)${R>?!tMg_iM>wu2|{J z-+C_xI<>1M=@C9&b7au@w2(LfP++a60&HBIbJk=T-H zoXEKG8)9&6Tc0Qo8fXz6K`IMWOS=keN|GhSu&#pmEO8eFmkkNe>XGive%|3L=iY*$s`HBRMGH>BY_1z_qrRhs7m@wBw2yCFO2<$kB6TkOC!tw zN2dFgA+yc~f?x&;6Nb|)9~MfN(5g_9(5f%JTI@_IOz!$Bq37dj8Ysx5EYp0y-Vy$I zJE;Xe&XmwbO9@Uh5V?wH$e++a z;E0?e;n_tnH!U}jxo6j1X!FEp8}`t5)p7b>gXvj%F7&&fL0nWQ!Ydc!PngeK5>{WGgyMuFda5sDbFcZm7zDAs_L7hB4U2~z zxh?hl+r1q|w>@q;`WHG6A1Ex3kAo3>hNj=fLoCPG?J}!73(C_{xOb`Q#~F`7UD(q3 zfz-alo$haj%e`fra9S-uR;X*0gMb+mB8oYvi;b(mu#%j5> z;tV>}W$WX2IhI}(0_^Qf>JNt+7(2VAR~~Ve>@sI@<_6pLNz`qAroX58Qpj`RQTZCP zWIfPiM&T(`wo~Sz;fZ0dCR{Hsg1u&rp!{lt@FVF(F4tsPajo!yKqmDVL-zJ{w4v&+ zMm354*UpvG#ea6zep8fQbsw|iHd6kAfDJFs=C|vN{X4=LxuVK{QHIa_H-J+)YQ9w< zouh*9Yx@xujPA2)Eu*(!6#Iuz{f2{+0!G>of)1h8k21K{>jN0K)!s+0$p)cjvoK|E z$GVXAQF3&zsE%KrfWsdyBAZ|QzsHIh?>u2T8Sg3|)Te6-2B*1sY%|80V%}zi*F907 zs12taxtjgB(=KmRoLj$0mA#8Jdoh$O=0z4-C#OuR5MtLv?_T?FMo3-hE2j%oz$CX^ z=y6MUx_i7&a*680;SsgYK~gYR|18qaxnHH47=MahFthA>0MbT8QqR@^XQzi$r5Z>4 z)GBeE<7L##knNP`UtNnrVYN@LXf=~3)DWxtTi!(Wc`fFJ=0zvX4Xlu1IBVH)}&s5an`x7Ju7?3)`vBDU5&qMNkI@EECWBj zG^dT@KE+0s1J;vIAIpU+W}?7ajkLUucDjS;Op}c~za1E9Opv}>7L$$#V$%Jv4HW#@ z0oJuzf0(CI7C)O_246`@J+u6>+xhBWPmYsyof_RumEOMFtsCr&No<%+KkwVru&#kXto8sd#&{_Eu_Axe)8NF%fsAUDLc6X{x zaMu=QDFxE(qAxIob%W&|#1z}DFm4J|jD?Slm(0&cti3+9N^u!mT5%Kj-<+Wf%J$d? zIru`ny%BBS(~>=vI${R&WIY77UTiC(M9T z4vk)%Q^{zuy&~x!i`975Em~lT;qza}b_+fN{<*G3kW$VD*>3Lm+B17ZycO6>HhU5M zs<|iw}9I2NH1kS-y~^OHOgXmx23u#9)J?b$wNAU z#%7jb&W6NJEk4QS5lPvBPUbs=RBz@fw#$CotIGb3n{k=_+486ay>D=Yp$%tLDviw} z=%*}_i-{x@wS}3d2^B@!cWj>LgR+|bi5Y9^m)K0+qv*FKY`*M9ip5?HN7m_(pp8cK zmVzF>R&l0&=X6(o;?pOtXQIy7id7c*zu(##`UcrIQ58;v9hx`%~1Ms*am z&#_V>j=V{g6AM~UC&+0~u_AErk2EXOuH%d=dgxP97WxHhUxM0`ng(;;uhiT zXtZ?R=!aY`e5I2N8$G40u#L#Y;x*JRRYqzbYPv|c!md(ATGPVaf7V%##-Q@GrKyXE zbrYNhkM~Za=+*^Z5=^0ciza7-_t&pl8nItNDkh|upczwAYJmMeb17}cVTA=F{K7k0 z-y@SwnqZZLlmdpOzS>q}1zI}9SejD&E7SA6-0PdoPYJN2Mt{HekH-OAtgO8fA;Xj{ zHQ$<+t<2MeyBb8$O?9={H5SsaPol->xwe7CRS#d<)XBVSjO49p;)L3s-0lw` zz)L7^jE`_#IHLco%kIL+Xt7+*!+81_lt4xC!>e&EK)+_Isr=!mR#2YWb!?{+WG_T_g0=R#KJ6>~7!JOM9hBJnaV zdg+QZgNg!uPCc<}mY`kH(1`3`Zj_O(WCVNgFj9)4McHusJT7G3${yY*&PcofkqZGY zYJ6Cc-4xO9%r^N`|wN!UlRWyymol0q>N2#i?BnxCV_%*&0%E6O4B zx%r^-F%l8*bxE&(6C~tAq(1v&eTYq+v+H`;bQ@FT+X=HEiK}d147reAW-$PAmOom$yIPA@c%r@NJG*Umvt=*G&!4tl>J+! zzwLy&8RTZKts}x)%nKh!3azmHvtqTe$MEH%@4&L)SF^pR%y5EK=R5jK*0XlR^o5+O z!*ki=3v{EoyZQfc=MRfd?)=X>n?dTTO^66e_=SITmmTfk&Uq6`s5m-`k9;OH%Lx_c zF&(~ZQfuwGaIrFJkfSHk#{^Hfgob7dp~T~sPZxU;PfLsQ{+dxX*Y+ zbkPx=@9CfkDh#Sa>C(ZB!Qgts5%PY3kgsQ)bG2YphkyMIb;mf%YsS=)inwU*ixcbo zQ8(*B!Q#-uy;-mXhhV$5T?sXEto{4C9Bga93h>u~D?uy88^hfBy!^6QLRAHq`}&J#|&&D2LssKpP;Szc3;Wa=Ga`!t^+ zcnWPmH&?VOj26708)0l74#FI_VlrQz)p?o+oZeInG>-?7LwhY_rGk&rRGbk#pl${c z%x02Y26HEKD9=NcN;yJZ5Qd^wfF3GCZw9i?s21}u5yOZwq<72BP_`dSA4znPSC`Ac zaTbzK;Q^ zD1!3Fg#0?O3(yb=ogd#mdue90dV32d%-c`aV^^k8hYJ5_KA15aB(r@6U!SzCZ6RIF zOwsnMl515p4Bv|2V=IE`5;!Zsw6_R;n9bEA)E!2`>xVS;)g@+(03DQP6dPVDMckyY+Hv1bX`zvjm0SEp&-mz zw?C;338QPGZYUOmAQDAB8G4B7SMkO7Fez9ms)puqUVel|OaPJ@?M}U{#zG8`WL+gK z${^35LlaaTQDP?*9z|95j(WFV932?@!#ep?AeF*y89`@VwkUrXBA&pp2|F)g>1X8N zDR}_U*G(4)xnf|srWHNS^2>^};}hg2dWY`M^e6=Q*L&cJKLAeTLQ1B#hxhQf&&Dk- z7tG;h@J9cW8UO#9@|uGTOh{ot$2Om{|36_MgOqWbeijsohj%zeJ=rTg8xovrHk@ZN zhohAw>T=TbxNU~(hcx$61NHCyGZXr8wNhIpE1D%);*So{26GhgIo6B@;gt&%NN&gS zDAa{#w*$MIzZ{21);c+MZ0Ay7db$@o8UnlmmXZBUu@V;Mv-yFy$0wB`)h0Lb^I?06 zBo?jJXOACcwG+-L2bURDM?Q>VPmz-z5c+2Bac`~@@ zzVSgTMPx>UA;}c`iKt-nT}{&TpL!A^C2!bDlw(LzZ|h6Ef`%QpG-KO+b3-W*l=K6t zC~TDIY;%}aC!>J9&q@Ikcv>0wPgWCN8qrvpAd1LoHIhX?uzD&Q(@Drk&L6oVhYY5Z zj4%e{Ii&)@varD=X0n3q7)n2=A(PA0U}4;O^^*@JSPMV|ifvH-v9N}v*-=v%eky)o zekxV4Mi>uZ)EER4S6cJ&Z?A9fZK)2_QQKj}NV&n@^83U`@AwY>&5MXxJzxQ`2T>;o zZ|lj#q!jmm=j@C_(I=%gpWuXBbTz&sc#um-!(v1&c<80= zgTu(H7JpCtMs)oE-`(g>gO-Fe@o2a|gmhC;W+xnTxgKY)(8zPw;_61|SVQSt?CJ=P z8&l(GN%gUcG>H-VWXt|$4~4e1_2#M5_4a)8%!(9O%?!llnBU%t9<2U!R*INbwV9cL zWz2hs5}(k=ynExDQ(m52jEVSW_(FYWpUK3L zm?QCNkQpiVneuzMDnE^O(5^BMNU(qxSsVj`DHMB*sJP9M%VJ zZXqK^OcL*yR&{1%grzrTTjQTZJ<)zLnOlf;amU!o@ArIjDl zbZ<4@VeZfm>D|bA z)^OR2Ouz>?*l%nG(3JzJz<;}J8>AT|6#ieU@(oje%7VR~(LQJ(BNYoR#o3d6>Qpdf zffP51#Bid=h=-XzIx6$v)~~ZPPp-o`>(_DcUf#X_xgRz`h0o^m_|r)4WDSu2=(;r=|lSh zA``2gJK(I>LucL0Il}hG{k+=MSfX{O{S|V51E7^GfcHybsMU*>Y2Ah4e@E-*BMlu~ zlOW-zU+_yNT_tV=WaEZ?KWSw*vF>J=HLE_VLNqpjMR=nN%N_p^jC*Gq;h6L_iHnVo zYk*S)ELs#QHIRV@k~fiZJCjB|AEsCocO=L~S+Y2hT}%;j8YXupQG%tQJW1tB;bWc| z%>`C)1b^j2BV0Hwo))Fp(iLSzMQ~CyBM$Ccp?=VSNb(?wWNN8kJCFKQI4r}mS^dMW zC;irm^0J8(S}~!K-7WdjLf(klVq7)53V_<05<`nS2F`dUMWWAyIwr_`tSV6_2HGHm zGMk}kiY}7@EnQpDn}fk~!Bl(O`;N!EOlUGQdpgski6B}5)#WsK=1ZR0I085;)Pz2+ zMj`leIi&d`vM6x8KZup4X8Jz25oA#{y~)UU~Xs{ z8gh<{`21+=M|&6BUbFqnYVHP^k5o8)PsQ6=yUo<(r|1I2&C0(1UtY!pLAa1oe`N#7 z1(V_es3PliSzDJar_>+om6M3XYZPe(~Gv#?WmB#f$9kpelyMvIJN9t!GegePuK?+@uuz0Ke{Qo=| zn=2_N!1^C8%c!g;t@ag1$a0GBh;0s`X#QrN&{o`BMI00%TSe2$(N}G-W_5Eo#YE^n zSH9Z*dT_e$Tq%AKZUIW7g0m5SQdW{6!N7%t6r8t(I9L+3N_j`_j`;X^&--{$7O$36 z#$f#ARB|;tIOLBsD{q6m&j(QNnTT)Hi0%@W=@%r^U;pBy^UliDFg#NRbnExDNMNq* zUE_Nk#;#nP<0~7Ab!kMem2X2EcNk`lxp<}NXQHzRLkU~6oI}R9xRM?j;cD4=?<@)- zH|>`~Y!e9iV~v{e7#*FRjdH(L-`G5!IQOmaq`T(V)^}?mKMuWPbLPNB#bKPr4;~?v34yf!&bfQv|G6~ef#y6XpUgbLsdyE~|-=hX%wyVK5jw!VVDsfd73*Rjw+ zvL2*#0PlZ{ljPp`V3toOQa~cXfeVTTCKCk>ayik!Gwu+4-or_z*dC6^? z_vDrR?MJ-Pyg6e>(xX(77dW{!KP>{nu`y2~{Tkm-iP;Tedn>90CTZUhlPkAJ*0spe zqkC;_u^V!w>w=z#6Mlnc2xu=Z1au&c1bnb(~>!v1gGhj z2w2yjCgI=pY4eFAlJ&&b7nOpRnaN_d(*JIzrgGWYb#2!TJ^#*a=~wkk4X>YhF`XmN z1rX&WfV{b}Ja_tyb#-X(Bi40bKRlII=WNykR&s?L^M*`vR?hc4IQmZ?gym97et%g@ZgmNQ{o6Dh1wPd+rv_-Tse{NaA6FoDz+ z=d%*0TEMhjQ)v8t_>J@v#n|pM*~1*-HI+_8LmTC%Il{S)mdN$JB3ZOuYz^M#LG zE!H-+!GDU{7^#l?%>n#1ayD?BG%5BsDACo7w27hfi5v}-1@f~+R-^?iqA^3W++1(o zZrCF0d( z8ieRYiVUoNh5!)!AG8kZf2Qh>J!61T{`}NTttD??hBeu~`HMP#x|K2OerPGv_znj6Ijw9smf9hsbx=QX@rL@9pO~^E5&`b^eDD&zUy^l7pp?+7kY-!jke0$I zlGy~S&Na}JEZok6@Zus;)6DHag01M9+yB}`wo9Zmi(ONdv-fFm@t!UKmFAqsJ&YyC zrwPS51FU6uBDda)@fw_{{i7?I87*y5T)*{69c*>h&zvwWm&X4c7;!LjOm`%O0-*$u z%0s!|cse7&w3-Bv>U{-2697P@@t^Gm=YY@n85_%g^j)e!OqR(1bG}^Le=;~v#TJRd zltm@Zo~2u~)`29c%M;6RTef0|96)j;C6D3CpKZv>xjt6 z$i`aSQi;XiJFhDL_siMVTg%c(08gArSA3}Un^ThG_$w1pw1dEk();?&+HyPb)b>_0 z-(^<6eF{14kLurpPv8*`_$wM`)Rk=8jjBNoVDWlbOAc&#FBLHlY_GWHN`rkD>`{GoY)Jy3f$ ztl9eD?O{9AF%5s}SxtO8yxGs8xDf;Ne2t4lWCQgApKb|x@Tc}+`wyv=1sy|K5Y}(# z1q?MbP%1pcq$AN)p=yYEe?<&9CCQ?Nv0Prrxg3Tgwd@`|*a=%A^0OC#o8@iD#($Nx zPaPhtF(gCavHoWDRd(D-opxM@Cz&(H37eJN%xHbD)N-1zmOr!S_HTN3NZ*xWy8}`I z4`Ac5zl!E$VbP?V4ngv=LCw_b=v0wLcu8wQY*_HuB3NznGW2qx-6(qoVnjycr}J$< zN)sG5HHD8c6@_`OmU4@|#Gf*t>ldM+8bZqU6~ac(h2{UfriklM z($?!xvToI{9H9EYWF!D2+e9d7A|*J&>IpKD35jatGLH`8N5FLXal`7_`9CUgU5ep7 zpX^`m7wxSM?#t5Ec9e9C>Se*z#hUfe@p-0{A>v_+X|Zsex|(CYi;uElzwy+4Ic&-4 z2@yUWCH-9|J)Kzbxbkd@y81LV@x_|!*RXsOG<>6Ncje?#FQ zBWepx9?lYoAaRvLjPyDqMW80dlw_(mW%vK2bc#oq7G?uMGEhv_)Kgr=PSfDRx}_7J80Mq>>ILk0FTVjTgY zk1s}*0`8Io`DLr9H(5IZEe-)g4L7AJW)O#75CmsNU1ud{1|3p3nlg_$FKcZqlI0Dd ztAoj-WM&{1QL8<;AQz|&ty^G5cT%953N~_~1C7oLuA=Occ9SY)vc(iWl3dk0}u`N&mV{LxzA}U#cZHg`+!N*svFo{4P z&lGBSEASjnK5T7sgvKv1OG(eE&d5uzDTRy`Wyg_XVNTI6$^ij>jAQ{yhYJ#kh5xP? z9g>(Dnx>D=6GFwq793`d(9bhm7G)7#C>k7rOkKM_K6tnH@{}wG6WLNr)dRe-8N}rphfeOXUiT z$Q`uF>-mdLY$*7(*-by9J8^Ji=3&)liw7Cw!{4fmbOs`b*h*-uc*W+0eG`9 zNX^6y5w0(69FWbK#R~A7#8$80^I7$pF4sj&bsY{~)>k4vM{k`v9(ydJaH}U;d?;NlAi+@4C%Du@7VF5UJ+zO_VsT*urOf_4feHZD}%|=gMlD$=XZs{rGj5N$DSA>X2oFnF4%j1N!(dlbt`cNi1ckJ9c)Wn?+a3kA#Eq)FGgObu!$qRG^J@G8!N=FL#oN`Mm=6ysq-4 z3~!ejbhEs$eZ3X&6oD+3@c`Bk+cDG!3>U$|QbzZRr06h_hy;UYr~qb*ysgxuAHrY9y%x=oWd(H9 z7@ZGBPi;K9A2T}jr3K&0kurgu6NTQp-O`Ypm_G zi%1mBO9xe$YPL2JWO*3draqJ?9K38 z?CcW6r(0^bO;Tyw^2@J0g#?|Uk130AfA?Q8aYl}ok0O-_y+TQl(qFPPaBJnfiEuN5 zCS62wljn(=Ndycs(PS0UeT{Il9w?M7`-X!3u*9((Q$yviG9~$h-f=MbX^)cweoE#W zZCAh*7k_&6b?!*g!q;vmAj@HD!S&3pA_$jKEMso^bqrn8=USX& zKIM*=?5D55hGfUBY}K8P63>yU}_KU?WzHW?}LZ$=SFG%h?NB5&IL9eluG zg}4Pq$mGV7bmFaPGPDy>UnoX@vRJ4IB8Ex5*I=#=D@OXRl_VEf@q;=S9qn+bCuqRx z*tq6P*se~Fl^Bu*BZB;HA6(gpqz+TqRWT*O$E2@Y4LMr@| zPBsxn&?4lfDdY8{kyVI!!K^MS9+1G3!7s#S8F+-JkyYng2Qo&g;i%-vC^Rl9ot>Ks zgOSQ1(JvQ?@~&w$9+A**G{o=nM+8H ztH#yT#e4Qgt6L0?a>ZarNgLk+N-vy1V=D9);)1M^(G1SiF&dytdJVM1v{_&=2d5*t zS+;t2-djRF7QON-EQb=FLZhid=$bWDl+dg-9^&GMo8X-RxTgWZFpk^PD=QDL6VG=Ut)oE_%WHf zEk-L#EC;3XD4fZd83a{ zMRu-e*Je0CmH?ix2Znm2Ch@%aj{lPC<>lr~&v9F1(wmjJPgz3GJTUm1mk}~FX<_s{ zoa`RNJjAHsn9f#=!|~^chC=40a3s(GMxEU}-!6DvIsH=*-prov2DgZ74MkJ6Vx}A6 z%kM>EPi~g?a!{z;V93MT5RJ15cVq7DyT5C#?L5@ZYDi(o6ks!DQc`Pz?V=&4X4sSXWrnY+QU9?{3Y zM}T_v$Z&xV0l&M)OLw{4stNvr*wsS$HbnE&%NjGWEH)l?%dyK{gs~-su~V5F&meu4 z|1X!}vRWsKBb>|PxGD7hWG$E7 z0nasScQv@KBD*s$2}b~LWOllo7ocB<`)3cz-7bR9)MYE+wSIzj6M6l+BF=R7-{I+8 zqHc!S>}=EE4h5%OO~opQH1r4qbb=GPU{ihKpzX~#HANU^M@%0F%|oadKH3Jn6tYd8 zNh^TuiHL3R%4|iLkH_ccwfEDKS%zdjVPcNA(8@bcRszWtxd2(&T7?H5qp_4SG z12DM=@+_aLbGZ?vy#W84-hod+%E@xw)Sa@S%j2d6TgZGhsgtGG=~NG{p4Hr5jF)s954vA3QIR zt$mYk&5a@M^16Ax?422XSGh%tIz6aD; zf^O1d>>0rN-XW3o>&PQPq9~t9f0ajM_@X@QoIIvH+$^T7=A6bR>^!_2yk@NITwHA2 zY-VPrWu1tXhZp;%d^@?Z_sv_a>I*o*pT1Waa+M7XKC{wb$wuT!aMir;C1R^f@N>(i{`v;$x5^I(B)i6HzgwFK)CZa_ixj_Dd0vNqO3FH_ zb|xg)KK(^sczB}@`4s*R^|}8m+K!_+kTt%El%7!qw6ZCitfWcYCo0~2t_QuW!W;nR ztw_nbmTVKyH?7{PC$C0*59N17*)YQP-&>J@qygNliJP_q78!>3uC#*WHb3LX_o#?) z39nO$3>kLU(?#Rtrt_pHr+1G~3XP`dwF8+h7^B?CHN1BMt>1fVt`G#UQZm;^N@u8& zH!ww)tSrRwVLKF0*WMimUgzch!4#WO-78?vUVeoX!uyp`Yl8wSn7irf3 zz9`2N@N+dNt$ueW#)s@^$Iz24i?%2|_$>}?iqX8()g7gStI~h$6i8CpVXe@25=puO0RwxK(|8_9^7Ho{SNQ)DyHF*Wsuz1p$xgj$1?*0WZ7 zQ+_krF)39mPj6FpGu|;JHP5TcvGiiVQ+jOkWAs_^nWdn7JEDPdM= zYj_~(L+WJs=->){JEM8+S>{>dHI*m*ed^iz+59z@hwF9aS?5{fHJiudZT8vw+5I(` zN0F#5ASnR9ha%nR^^VX(9uN4~yfM8&1}G5#@d5D**>PGK!bK-P-r9LqyPMvFYb>8Y+o$(AcUo?OJ3Uwj`3Jz_=AXOM56%Bm z)V0Sm*}s1x$5_cBVS7{#g*-Z8%#?&wq^IVP(Nm8-9b{sxvE9xK#gmi@Lx>7f5)U?q zIs7W+*jCAgJr6sSZQ0to8NYphuixwU`|tC|{rcSZb-%9n^}eq6_4&N6vh$BPi^+)y zQMVc9oHRx15;>#>>knHc`s%tV{Hk1Zsp&KM!T`S;*PnMYh^Nm zGzb5}ZLJ%4OVC5;C;LAwd%0NS+Iz}o|IcOS1n(WTq(-G95@KjOX-M|55XjnRLIOb8O>ufsw>C}C2Y>0RtwFVVF6JY zg+(vFIW-nOc4jQu#B$t)=Xte?&;XCsQ$jA!K_V$iasmH7R!JSy-|>yf39s;X9K&cP;WIJ&g`?-h|5B&omo{aP#{=%-6~W zq`Ojc+dKT)7$Klb>Vx)c)zk!cl z-V@(QeM!GZTJLPeqVR-Ke%(1#GZx>uF|Lx+^MJt&vj;cMIJk_e73kS8)_0f(a&pkQDswFb2m#_0J2 z5Qa!=ekL8G+(EM?9Ub>eenEOjNvpUm)g5Cc+(TO+?f3~TjTLovvt~PpA4VFYYJ}H+ z7S+Tl-++H~P)ex&U^;I#;qGD|H2}GIxq7;9v0u2Lx;dlRRl#vq=QOF`GwVG2s^q=Kz>Dmn_#_N&lT~FF= zKqc`AYw3GJJj?0DY6jZ~*tsbE%#0e7r7FX}gpDbe3?fHZaRbw{Lrl(?$BbwInC{G# z74pl)kh%A30X3*+o1n*kuBk&fpR>2kQ9wlJ{(EdIs_kN!s1a2s@8|Z@_HhUXgt)H9 z?X2XN=zL24P<{%gNTvz?;(7AR>GjOZ6J)Hi{Z5GA7c*o_#GQ7WJsR~z9ur3OgB952 zFMmsBp5j%as)>1>{kYHLWAmpdZy=Amsm`MG`Ah)`TT^? z3;gYiGlhU`fmWK$9h4}v!XRUHT=TitO)n_{6}c?4poP6mi%|^MU|?cF&a@a?m<^jV zAD<$e2iJAw;=ixGBb)*cbv?j87B#cW=vziiM~djoh|!Wcrvc#9sw*>M3^ms{aLSz6 z9m{(rc{S%g-b3&pm{U}DfXy1(>Pom){Rtv7rpGvoTi(9}o)VVxP4H%tm6<29CaDwN zRkGp?uj=`h#e%)bu*mMWeTRm67yd)@*B5V_{82 zuU~F*Uzo63MLVgI6H!-)8H+APjTz|VQqcjMFM8!row7(V?}N9z(_756edytx;oT80%yqkrg8HEG zO05EB*u0vD&gwQ@E9J${8xXZt&#WL7&t=KdFhz<4`0)lDlK#GusQ}jGx6w*}d;?$t zP9v8@hU;%f{mt<0UmMz*blH)nNwr;FJN6P?PS+{Cm=?txN8@6=wQf91P9!T@P2K2leDm{ls_TdgmyagTp>>PDH7{0+`jkc=&s;%xb5!h(-2uXV zq#F1f&G*b!N&qs8RnpUl7aH*V#5qQI_%LBRc+xX)orwONeV=3*w=EqO^@?3g+8Sq@ z-ksmdE+d(a-0LaPRbhRE>trK-=OAoUaShW*G1AGL8l}#}+5n-kw`57u%lHD#I~mNW zi8!v+j{A$x*|$k%q8+`1W8WqokYJ*1z09>MGzX>LzsQFvVolh5IP5s})Xtu!fg;^Ru{X2M zvvl!BlnlaGxP}amGZeT8)^*ue1;+olUxFWIEB?@(&ZopTjV{ljY^2)=T3ttAX;Ea? z9a5TQr_8p^us^PM$_RYff0YI>8Z#xGMqn$4pt!VcwdKD)+75dZlNGjG*za5CKihq` zKTCp|2WCC-s~b`TDzpSA|J9vL$r+JJ0L+NYxG?)e71V|zaV)ieSGD+jM8a%#8mNpNQJ1!f1gM(bZB}(h4=$aj4e%JGxgYe>JJ&t-sM7#Zq0MPy0%W^tKc%7xg zjji$1dthRQbT?kHpM^bq#0~hT-7G2n`IjLBW$`7v?G;UniD%s7(Wj1DvddUYdGZ(K zXbt8+*Kwtub(3?epNv((dYt<=WH%VP4hk$#+k17$(-Lol0ySbWLc0_6@bS+XQmqyL4536gZaw{h|JE{oj| zntSan+EvBi;$GHlj2i`Ak+L{{8x_1&j8d7L)ae}u=vc(BO^FSCIkHGR#H-SE5Z31> z)}`sLZb}{GMm-jirZya?6MCJ!Q*_JDdm2;3cfu<7MHb&{*VZ~mBshG0cugaz_GND; zgVO9ub7GqrrfH~L(Hd)Sd1NI0+s?Kb&!gI1n!D5As)~e=cB7`p$$f8U!b4ApHgpDG zW$XfuqE@ze8pB&KfW8qE$lXnDGC{F{Q9PdeC(6MSXwG%ZPGOimV=6Riq5ZRV`Ow*=d4%Z$uPTgmz zZ#P=kcd>Y#+k=oBLD|`!^iuTUFowVq@P3W=HD9wjceaRWSY#nUjkt2) zU)@x_im`mjg4ibYc!dVe`Jo@6!3mk?5}MX}S~U6k;+S7cLo(X38lx@1L+v+;G(18~ zxslPy^%Y#BE-%N-%c>e4hedqxW>vqr_U1@?Zb)8SPQ=UsQ15Kv4>&31SX3@DJ*cW6 z=uGd2Vpee5@YWT? zo$9OItPWbGY0p~Y??(vxjNfefqB~JlfO#rbo0PmhnQCaMA+wL)0IfTg0q*48ex)Ng z;QY9ve}R#Wbx|5Oap(vvQn}C5$6ZtAc-@q>@L|X^5J`^8%C{$6Va0Lww3jti|3a%H z`AIF}by=c;==utP`^Q;Wlya9+k7R%*yYdLa{q;)I$&*Zj6{uyO-7`OaX}g606R$64 zs7<=e#^T9Ey11_dGnVM0X(4qXJEi!n+ZIEWeBkFz^BP~uC;*`$Qp>u9J&3&m^H|G5 zD%S>4;*^$ONqP|^w!!Y4{6=M&5z0gLP$87rXO$#C4U7H@CXgVuIu zQD-iLF7@0?v|XO+xHa=YAaIPeQv3*Y1N`b-MTuhj&~{CB6a2=`&!;F{mIBXju^93{ zV!3pUF(OM_DnS3cpL?c?Gf&;!S0D|oXXOgT%gyjY$9CxH#D=ExUw_YIw`dhMM9`tB zJ^)o0msO4V>0XS7{tc&V-RsqCHx=L>(J6=9p^MqemFT_9^Z>D%r;f1iKOdJZt1KWb za9@kpb!j>?jCpCOSp!~{YgNIN+3b^G0EXA+^zKu*$c^i#zO0w&oorhR$wOPb${@(b za+*-~?!nYe(#@04-oD4W57#YM761=$``m7;EQ9Zw82JMpNhQX3TWxQw6yk(u+BMFM z%O1LH7Mwn(adlc-)-vj_m?_?P)|bWEhW1vTw$=xAI;7&IM%X7=rszg@fF9D{Zf=5k4F^#Jrtws$S$jGzWF5Z4~8~A5XlXocbhnS47uy{1BzX12U8uVh>M}0G$-} zs{tfEfsWshFWi)H%()kt0oVHI&*Ff)@TSv@ibDtor+KDBu>6?S&gnGxkBRLyl-?0< zt89U2w!?4wF^`%7K5-(~29Fp!%|9CF?zTQM7p#Rv%Rq7oXE65~mNjtbDBkb4BOtL|=&qtjY#$dDV z6}{5l`DUm86R17@SD>zJ`t_Tp2V?h2#Lf3Btkzon8Sjr)mqZ3QgNsogVe^cGSRG3} zoXz7Vo~3SGuM5_)Os%dj7rSTjG&wsM_nWjQ_vd!3i`PA?Thbd+ z?;tzF*b{2#FhgkHB-q;FgthphF7G?qZb3<3K4;>o1M!J;sB@T3Bz_5a^=k1!$BVC) zU24v~7Gk|FEo4SpCDcyTYbRDu)x`a_X6!|Fo=s6~rT@F1m;6uW1*zh4M6FHp)|=$` zX4|jok-;e7B>&;gNb6c*Y2xYPru3%}9Pv(5%y?^H$9I3017A>cFBk>o!?#DCuDP6% zXmh*CV*K=h4qJbeln4JMQZ}KUlvy5a76bAhKJ*P{4M;PH(MVN5Ow*`p3Vof)n9*@F zEy(y8%qqG`UXL|$%s4f(ul|{5Oix(zmU}&aW4(YbwYQZ`>SHFb4!REt!+U5L+56l; zAlML@U*+JOIGxq>YP8ivyQ-;l^t4fj?IF}Y9$Y6S6d0pRJpD=)nX@9T53i|?=M_>pG z-sJ<039oQDuijIcVV~gI5g13|%B6Cv#)PLhEu8B|ZB;IJKXC6x=WKWhUTxBAOF`Oo z?3T$edUdpyDn;m(G^+_#rgmbt0*)C2Sgo@4B@ETia7=$Yv#nhdooO+v*RI!;ZZQ+y zZn&6JIup}wvY0V7djh{ZpBGS3~*_FiO@7(e0(P$>ecuq6y_=VFke5xWPhjtfCVt#_ATz94ckO7tvnj?aeY!ITzG8ZCjVFq{boqcEIbnqGtBUr33l6RNZvlX&rPc! zbMwq^ZktZzES*?HNqAk!UpcME3xH_Crh}vUJo%ebsen7FIYZaCw5QO zj;vJ-B>h9Qr>da^R9V>eT?o}?X7Bvf3Vv?uq$W@svebYCqrdwQrdL1T|HOe`BCFXCarQ+v`<;}{^D?U=8p4kx{uKL z*~;yX9h+x|KWuvMWj^T2IuQAY>Af7J;@9^Ue^5IDNy z{5wSF$e*w6mu*Adh%{O- zz@T0AyM-KO=1=@<#rMFa^+l3G;yXM4!L^l=pW9w5-dnzQyQm}avgv9g6Ue{(d-N8gIu8l;TaDXph9U6*=mLZS; delta 39621 zcmYh?Lx3$jkSO5Ww(Y)c+rDkvwr!ubZQHhO+qP}@``^rF7GG9bB%7qFQrV1-0=oN8 z-4HNj3`~YidZ*62@ds7bNB>|8IX%mhVyR9eXG8PRyr4&-DH(k8SS(H~e zU3767Y=1&D48Fe=8Di*K31tn$M?ltikhv}{#Dpd|9CbS)34p>jPAmWHwm%KN;D_FaNh@g8}?qRgXx7!vbtmGSJA`213m8c=FNEh?j5K3#1%^h*aN3oI+<0&+})8p8AY(Qu2?M!^|bOk*dDwb^D)1JIfhILo~}+?03G3r+1= zZTrSFOmVldPWaV}P!*R{?l)jRIV3o@TbtzWN;x+C)S0`r5J7;XiO{8zqs9SCaiCLQ z9T>B4^3HfEea8BAduhIlq6=!kBQ2NNLkKeJ+!{^;wq}w7mZqFbagTd*!7aj>!Rh$K zv~DR6?ER1X1cR=@5!UT%wi}@h4rOTw`nF7(wG_<69YIY4 zOWBQ(tfnbx0}@*8ej^kyU5IdGBb&p{-xnw!)`F@`$+eW8xV-eGjzU0`EB4r*L23&t zu62vgsitNntO1cuf41{96qF4^XMJbca4aT!wX}r@C_XDovy03~5g3PSVF@7P1m`E6GfLP> zjH1QjBk)GLq(`Y7XHUS@o4T8^4ae={%KRSxG2B_QePN5tKWOcVk=yzocskZ!UIeuo z{>KCmX6#R-5A;3T(yu0md)FLW5IlzSN1c50!v*J47Pe&4hj!#e4t>Zqt9rZiZZK75 zhLiYDF4Zx#Lqe{qA}_b9k{4jczaf$BemJfWmZqPyR|p)&`py7;rrjl`%?flfFR2ZT z;OH9P&?p~(aZdTh8J+P;Y1*gJUr!m=$w$XLO_HUSVmML;My>UwBy!23`6s!=?sjS0 zWx+FV(gO#{wYlzujld4_4%r(ng@H;#nbL_=-5s{RMQMK9P1@LM^VPvXC3gmT*7BYQ zSKF3;e<}ez_)q{t#NQd??dfT+`z2UrzECtTj^JIjP}k_vj( z^PDW-+tUgUk@2F7Fbydm^!B}S4ywcK1jx7M(kEe##<}Ch`58u)TlsAwi zK89)3g#!1EZk=7yKzE2-KC6@F)57(8xEn+Tj=i|5nH0DX5EIlI(6R{wx@wQd`b{OI z;AoagHwQQSZ)Exf*sYRzFniikyC;*pPeP&dcc#(?$Nqso}6(b2JaAHwOSTTSbC5{D}7T9dFJ-rx!3aFSAr!7ez!9Y6{V5{IR$EwOwj)JmNPBIyEtZ~`eAt= z{3HMZ2o6MQsh)fIQqu&bG*VXN*64<*4RzJ!q?UN(9X)bH1gDW%SkJZh%U)?fc$L1j z(6J4&XLI($=>wC*H_3uA-Qudq3NfkJB0FK_p)}Z6!yWf@!=h_U7V2U*uE+-?yRX=-;5l|1Vo&wjrba5@)I?;*0Y49kgeHsGeo1s{{^tYGV!lruH838s;d z8&>P@)7sr{n4a+pt2joAX{{j0C_mQy>^drWnzul?`LYyh;dJ{36U7A10(e@f+m9sn0l@1tK&Hb0*Y zpI?Wii=lQ+oEFWb$xr8t&qamXNzCMRnJPa|=MRAILPgcn-bs|9ukF&W(j>=^b09%m zKP%g|qgm$eCVAZhKL{gfJjIU1L^#RxEiu3dAHVm<%~PpdD8-KOHeA}}G?$wvg$$j_ z)bnX6L?!f&J|t^yTQT7uvf2V3)Tl|SkIMj;{zjUWoc86M%LOAH&+~(W#lY8c*a$f! z{8NCx0dHMDP4+z{FLV;(h+jPvn!<7%D0a-8%}*4vy@iF>a3zhv1jE>;kpl#;JO(!E z9+Vc8bQ&YmDc4~!g8sxw>#D3yxC<8626Es5C1mejJe=|lPb24KrrI5onl2O40A^cj zT^9}-cG@YLH*qCci%d7l*5q9{FO@TkJrw18~ zllS2yX`7zcfF1^oN@^B*vE!WsAg(fZAgE%oe|)O|w%3q)QCt*nTy&1B}#k0S_?B z)jvEftV15JXe`*#Xz(?YWnyPMyp|piF4)nR4}TXArIc)NHPv6|t&o$EyXTRwJwcZ- z?0Ef`G79`kQM;;@ekW1y?LqsCR+CCf|z^CWoXEW*^rDorEfgG=afQYakcR5CH^co~(d6)Fe9SO>-%WKcMfSx2sPy_@#%CkLos zlZ=Jhg{Q#I$u~2)CR*_!BU6B*nOu*3OS|&|gTc&zQI-MHf-{5?miOAcn8mitib>)C z$J>Ros6ybft3myFy4aDrQXcRGxobELrxh_va=mO+eg|Wlzpsj?yrh2QIdGN279B!6 zI%3;A#n;nG(ROMULY_RCT|8jcV!G{bhhP1e+1%m&z@I(0k>Ad3;#qVi`^%MV`XOgi z!MAEhaG41KtjUkKFlx$SC+p!<#O34m@e}&xFdo=D4bVdu0LnW{R05n3Wy|=&iJQaW zE#1F?DH2@vcJ%y?nmkT0pTXV@?)GZ`-o0y_9s}OZ0O>J$11W}4CGym-Fb9BPCmgK? znACWQl>w+PaJGLu-|m(+!Dj&8>>o$V$~?*v55P0t_=^Mtteei#WuN2<)>$ zi$8P&zcLNRrpTAA9^eJZ_Fe5%{*n{dTH{sD3DtcCXohrekzD(svq&cfY|gVH)sR<8 z3tlGKbBQi?imioj-Cbkf#qD~=hDym^xGK%o8FXSGcX5?Q9U}FWB--!MT30{!oVsq* z&ct%w%KX+wJ`2c_p5ewAcSnrnSGBi`5)cok8-k?|V{LV44)|#N?lg1nn+bu?f`^U8 z?ehg`wpYyKzZP`xCSC*!+EGB1vGdBCKxAOAn}m$=m22z*4P2CJV%g?pw#52oeL#F< zdzMD8rJ6o!W*^rIWW4*VW6v~X=IohHlwzXM<6K8m{;3)jURr@zys&G8(JLG>H-@g)pK8Yeh+w+1IV6 zuwBs!jss2aj2CuA*#}_pM&w}#&t`U8IK^JjZQd-E#cbAQ*|(XL8N?O1w!-#K=KquO z;lsRTmh?Qpn`v-)->>rD7Wr&x0D00DiabXeIYz%F1$1g4?RJ-`DgM2AngV8JFT(b; zp8n!GiU>@$JlD@>*MK~=N|L=>zV9lu&*d;yyh^(-c51_6hAJsymL1}??!3iNxI+Z-m~ zjFRVnzzV>gBmaQu*!;JD|HmOiNK&b12vGj#OlFM;eN_VFyGY$k_4eE=LYJW`aue2pThZRo6KpXL5{sYBW*Z!1ufrO z9J$;;*;q0=|P}F*XHk#M7r_%TBbSiHL4R4S$q7I?XkNdwG`Ka9oHOjnGs;2 z5Fm>?fo!*6#y#{W9m6Xk1Z-*Qr3vg0T8H)dUm&a8Wld|Ha)KS?!1iv&x>zG@+*Erc z+bV@h6I-79yJi=0hK?ES0TNhG0sPm!ale-ZCyq4FQ)NJch7p{RgIgmb6j9kJdL+%+6`FKGsScq9Hzj3NuPIn%{S$IEC#wV8WDld#nOQcVAxo(nk0R@u3N#?qh`2k zq*bw%s!|hSf-G(=hOt!8!$B9Bj{r<$jd~P1-WP$&S`W5>U*i9k}4Bb0z#kL}lY%M0yhc8AY;^EZ^68ZW{3Og&A2LV+3uPull z>a!l*oWCh$F*^Iw;nOn)E_2#%DP}94=*VzVYPDUA+_Mja&y}1bCJ~F;rpH8<>K^M$ zuPOJ-O{>#dCn+iWmj~-G`0T$9RsD26@y+v+|QteY{azPzTN2aKGvFoBqj#pY!TM zu+vAK^ARZM;KHK1hf3uX=t7{Al=brh#o2WlB595MQ=A}K1~SCsV=bMNbWv7#uE?rb zO|;S_<ug=K#AT0d+LCTfjUr zB;#@C3hz|ITB@RvlsMwJ^e~w<@9-g^3Ee{8R7Hh?ys$i8?Po3 zf>xOCPS4|e+1r6n5}`bxr*obC=|;6LrupiUM^TLM1+v}UQXBh&HE5IGfKbwH5`l^i z9D_RghErG;a*qAn7AX5^+rAaL{-Q0|2&@y^J3xJ<@29q?4-kg3=#TKufa#Y^JZ^;< zC~KL$Ej5r=+ZwFer|W`%t>2dZr_*Wn!#7l>wrqbddvPZ@!1+>4`Gvb)iPpK_(b?nA zz~A-xXwVDZTot8D^&?*r%%>1uxhlfa2VZhJ=y{sXN$?gOHi4+8<;O2yXyh0MPq66= z9^&k`1Hr6-K7cDmEQ%(Jil~?#oF4UG^t#i0OCy)_g01DSfZ36?swMtmWS(Kzt&~y{ z71*nrh@{uBklqQjhqJdf@jd$=xP_WDTG>$5mS=9dAJHHfXkwUN1E9n>M}7yNx)~cY z#A!&D3@&b+Lkl+!0sIwkF|1_tbipmLlF-!?4r!O`JOE;EGsr(#B@TKe(HWW52~pSb zjWycntj9?!$}K=oLcn({n~2c>&UCCQJDn@0nF;3}kho|+Nkw=aW49z^yBjJ7cf4|- zL7DbZm2?OpBli7>`P*3n3aQlr^)twG)^pkXIeuz#rx<)~3oHaW7cH}?g7HJhLE3gS zQGosA6kur>55LF1HPc^p*LYba-8wGXH-Gj@TkCS-bqb?+1^O20UEl|Bu3#9q;L5jX zX2Gvl*6K=6e=PH^jjnc%>qx(janCt$$8I(B`G)%FY6q@RuC|gn@;)d zE=N6vDxpXjkjqk*Vlv}BH!Q@jN#wjaXo3ywl}YY3hmGkU#4tw*vpEV(j~+@olkq}n zuA!0PQf?6B^xNIG{)Zt2IqxYv3da0c0I_XR`NCz|nm{sMa9|@i?OIMv9n~TbAus#s zW+80nxOLi^c+?zM73oi{c;#x7SAHNOUpAm}OS{+;(!bm~BLUTW$MX#TaFRKx9TyyZ z?N4+)9G+g%C0tq95UP3v0Ip)A?K;B_(KXdnHCRj)jVCb6o|9LN_QYrE7Nf(Kfbrpp z9VFV06?^IsP5icX+7?CS>!$oJ>p7`gD*9e6|8wLBjbZ0&A`xyyo69-|3_5(JL6{i7 zM(;t@5K$*W2NczdUTh@`S`Ms6-4eX*0ZU%)$cibviru#Ikn^deRuT_86T_X;Y771y zr}wE~(Vi?fvX7_PVzlRzNp(j-09VwmrqX2Q-MC(E0g7h~mUu|`_7QCF(Bbm|csf{r z`qgEDO4C8!f3fcy0R3p+@l;H@DdlO#wg*mwuiGJW;rd}lO6J?(qJb(4QDa|U>U};+ zw@Z|2rs<~zo!0Oxo#EW=1emaPwKrPPZi9P*k)N{)wT)?r2cKhgGT2E40LJBxdeCq1 zXa9T4z*W8Y0;@(U*3E^9!M<#xfEL$s@~_ZV{n_V@*`)^7ZgMLrl zweCX!u|%Ny>Q>Dvs6Kf6?{QCOZ+oK9(^dE<5h@$NU>8jO)cd&B$LDLh7w8$*tT8qI z0T(5e@dJqrl$n#AJ=LKE6$4O~dJ91a8}O$dXqRn0bAQmBWkU*gXy$Kku3@|gIst9; zNF!T-KCf!zG}+~_XDfU!?$N(KevdooAC%D4-2KhhyH}TwugTQG(%T|F@p=)Y!T_9$H-vRMVp?yb=ZL-dh}7bRnpN#%Fb zGLv2H$~MqbvXj{3~bV#P6FdO7OMS>SPL^fN|;B=$+RE#xXhr25c3Fp@V{> ztHbO`XR%O+)J=X$r%@1x9OZ%`>W z|28OSIrGNPrjq)@?V)4avN`d`Gd*Iz(i$)M#{KbF2D4HT_nihX3@}?T$A#5F5&ZjL z`6IRv`h@h{wf7FRGC@6-<#H|%MrH-`RJGF-iOUTZYxzj^!4;IxN$B>2{ zD;>{u-AESC7O)mX!`6aWD!2CH#RRB&k%I%Re11Uvoj*OF_7kAFQaG5VmW>g>Hm$PX9D|b!!UAKlWm3y?y z{Jk%kPwf)`aGK1Nix@-*B>)7(!ti|Ye);IoR3u3@BbZ$p|viGlrB03kKPd#1%0H40N?`V5LfyPl>XKm+* zeU0z$@}tP}zYZK<-}3ciTCkr#`?wOmkzxqj;O&5yRe%&uk?ZbYI>A2v!a{UHb ziJ3CbU}k)0N6Ez9q}u7rtHe@(2~7RYK*e;>oSngwlP+=!8=EAIugFIYCSL!q#Dn=0l;>Li zWj%n=l*W&8uUr@F3ygdKe%fZ3nLpZT|Gbpgow7|3wGwU3nr)`MSTQYrlw16w!VS13 zRsrRg2ICg;m&E-*z!1OP)Tvg5VAyrUC+f^R=;|arV8c)-+n5ikMlrXXjb*kSwU%k+ zGqt6JELODH{I7^?1dl*!v{(H>{U-4W?*$+xK;-P~RW}o38~E`gP(La)8*QD3$!Y&B z5rKD6Iw6!zzE%XMLl^}sRsIWb!a^|Vv1hP&G$siPIWz4=+*;qRNa`H-u;h0nP2aDn zQR&owG&Lb8t09Ctn{C#y7!Ff&Nl!XP^s>jZ8_aZl&POQts}S=~DzK2t`u#k~B_8l3 z!^=z%JtrEg)rowY1{0Zd#B>sW5IwX>oY8@r15F8$qv~F$H7M0ec5+yDZZw5G?d)LI z6h*0Fc<#Za7eayfEu#$~F`B%|*F;p(?YxNmk~K=!aeS&q6k=awR?-c^%YF|fMm^o9k9<2Vm!u)kbq|uWo;jWPH5O$A7X0- zd(J3Mqfq&0m6%{T+a2BSuAIiCh*(S^6o3;lMnTmhkWB7^?S%FPf9}fX=I~X>)4ZjK z!DosxkYZkP1jux32AL z;@-Z_(MIm+ob9A{T|f*G-aUqg#+%K8!3KFtskGei6Y1n=%+@LDwnlfC)HubOZhEAc7 zWUI5*85IWmSMW;v9!)9#ZVXmwPf`{&G-&yNX9)F9%Br!Vu-ZOd8kZ>1n3zTZy}n3I z`B~_H$8E`)F(Xx2JYNsAI%O6NZ?|f^3f#pMoMiW-S{!-o(=KB%YY&hS&#d>9*H1P&8+@ExG!5Lex z7S`EXd~`om;H6J|c&uRbUk#M^z+6vgF+q{#*+92(+R>C}%DKT_1clcD8yw8b;H~a- zp>!Pdv67yb!mchC-U3Y6>%@O&l-DT!v6K}#8atML(0u8jd}>SoZ>dc65ZUm{?b zB5-^IHLk$>K&P$)P{&t)v~#$tbuG~+LPga7U9LW(vnKF_G8&Z#96Dv#f*0G)kk-jJ z1g(avcxWiXdVIPHU^zL0RYXW1yKF*woNvu=?i4S@pkv2am;g-CV7S2?Rij^COkri@ zy53pT#E@HWh()PVKTx>&xe0HmcD%jTO!G)3b~nuayk}&wPl1q@W}NzqhK>ZhTf#># z^61P9WWw|(6w}Tv(EHyI!B?u9L}n(9Cu`7^fmVvFb z^M)=X2n|41d)w8TCr-JmUV=UEqp6XSGPI$*j?PpE?nzQ>{B=r;R0rZ0wo5u@9z-z2 z;Je1pJjLin)!0a%jwTyC>90oys7ZJ`!rg#rd$G_@umIg9Juaptz8ZWw>zPZbt{*FA zy;l~>7d{D2vVAoOnL9=C#JqMbFQ^H@NEupu%Z6U$?AxxpoS)wwb#~JP;z&0U&5hSXallrV3eiyR#pHUZ zp)W)cD*%(b7K(gKUX#=diS1_%l~ge!T0{hHQnYGz^OlC6g887W;2w|tdS+i`M9ocx z6ZFmWijmmkG z^6&}1X^WXIY{k>-im2`rSajCM;L);olU{NmF91|1!&eS3mh~ipjVvT%PcNrG&~vmW z(@*N$&!H!iH|)%hEH4(pL_EUv_#B(xcg$`RW#OjLRbN>*NaYVyo9DMpHmYK}4A89? zAzxlHQ8OX9#Yga`ZJ67$;#WuvYC^+Ce8Xn=zo+XLfX+XHV-O$QS|Nf_h!@MN%GlRe zOTZZ_AEn&QCX7^?KD&_ivXjmc_<{_nKhJ~e=%@?lNcZxM3)`EC@ofqI0Z+juwEO7w zZC4eR7bAPY%94)Mc}haL)}ZJ-n+b#?co9#k_Zp(97}a*ImAi{ni7me_bidDQ8XdJ|4XAplklSs-D$;NH{1XXL zn+b9Hvcr+wP(9gr5}g^X6dw)OhsWo9Dm>B4G<|2=`X*Deh%*Lysp9@b)SooMBq0m> z{1W-|Ga_EW(fTkcVVc-$+t6W|Hu2IgKPjTK+I#()NbzG5cVd-0>Oiz{X~mHf3GX=*msZ2~;LR^#c#d7_@L~ z-19`D;>)QdGtfIibW$rgIY*9((IJ2en+ep64lPEydMOX8@#ruCzmitK|+Ip32dR zD)Za4#OvI<8pcj>2D?IHAVYEj9@;3jrcTCa`S^~wBx10sRD)fys!W<)5kP`XL={BQ zQ%6|4Uge*&75)RXqwGq`$(SSrr>lUp#s>Qtbgtr%oxP%SZLU-zJ zn5R?Y^w=XCvBe2np$oWXGdnk9L*pK|QakBQK;jqms{pr_kB{rD&ei=TS1Mwvj|%0s zjf#Xy%-YoS0ttn;i#5&W2H@yQiJ_fLSUz$?oAQF?&2U*>ft;QV8X8m40p?DR?D5)kK4fSnkzN-;>* ztuqSC8thjy^n`5Vum)~bLCGS)B#;bGVs}JGz{RMpk5H)`qT5n(Sxy+%sjw(3!+hsC zNySml&_WdGQ3X;u^c4tUrJ4?6v(n8;UAcEirgci}G@$b88sAf%BkkyXoP(l;P0kv2 zZJuiee@Plj;3?Cg3dnqD<*t>GY8A1$#Q8Fkj0>Av@MwhuLJEtp3=@DXZl|nUS+0>r zP*!WlEe#Rz86LQ|7pNB+fmyP7yje4~x5d-auD7x_sJw&!eHny0X5NxAGb~^PelK(i zImN2w0wOHFHncMLeQm8;nwz#NM`Mw>r6}IO$t23^wVn)+=VOn}vNb?=OFCn@yDXi{S3s9e3&Q@GtC z+DAfqg@q+IVeP!xU{jC`^8c7mxF4Xoy$qr_dFl`E+Sh%+W@{x@HDhejp?Wnp4sPlaE^!T>OGI%_Ox_3I;oj?vYzoB6=JFkI)nn6Qu8 z!oPp!<0nxhS9F;1wA4e59G=%GDv*dM5Kva6=wYaX{`4J?{Gd#Z>fLR=zI|FezSa_? zxb6CD3RL|ARp-;jxbs94rB$reTss~-CO{B0@7tX$e0p04|3VYQbmx%>#W+Hv*9P3( za{kv_v?Gm>m85tazs3Vtl!Xko*)y_yTnr^h>GfGNxnJ3(836WF*_a>!s@h09Mh#}l z7uWwbibH5unknNU)>;v5$$?IkH&%2!qJ1{uvPte~(iX8VrZ*w*L1m%phc2QJDgu;H zhdZ}ZO)fjD9qP$>o9GhfDrh`N$^nK{RepP%3*}4M*rd2(k%fuamSzrHHz+Om`H*gh zZlmYfG!Op9RwZX0y8|jj$xIDsE0O5mMiW=4VuhHn%?e3|1CXz`v`}9sydo1w!QQ_j zo0$CvIz@k!FSgxgolL}P%0j=SOB6_=3u)$bmn>PxU4H;i`XQ~Vg|IboEF><)t7o;e!3jgn=`b!nAE(Y$h8;Mpt#q2qJeJ? zm|YAtpL4!9_%Cp*l)$|-!!3-1X0b4|B3h_cUNdMrUdBh})-cn+89wg}e*G1R*HS!k zV>qa3J)hJzE_bx9FJ~IuBSsnvyTy?vy({~aqx zX4dG(as3lzFYnlVn@12xPaRDxuV)^xzB<9GN>F&XK z`tyFlS5SqxFRVj|SfIk-%cjt@SYqHsy-awh-ElP}-Yha!<-aBKPtJ&&r4qf@=T~>n z%!PfM{Ii=V81>argwLXN_iQtVxyOSBV@z5n@Z0%G0lj;P!z-@Jiib48c5OYO}o2oyR96kWc%HKu$k za3qs|>lYnpBe=s%pWBm@v@%nOnG5DL2?F6ulIAF;XUD=aUQ=ld4Tqi?E`gAyhfF4gG=RAB7d_^0-p9I-Oc3^ z?(L7ZIgzSfr39_ayri=@R`Dj#H13%)eCtiUM&v@foxciD0Mmyr?x?zS(1xh z{8M5hngPgi*X3vm&uH?nJt!_`*IdPFcT}g%Sf}5DA93tP(QCvu7vxr-eTX{lc= zV>Q$@{K00A46<`{SCp+mjKE-D?CYiJ+Ji3@Hl!vEr*KgGG#N(~iKJ|EfJO1|yoTK> zd4y^%q|vgRk3J2G$eb>rxo9_ytxRqnnyaSqXKJhS_*GQGOdv{FDbGS6Ytgi2YfQlv z0;s5~{t{Z&gIyVE&z0(q^h?vj>ly>g!U`pY3`_8FqKq3iE#sRYpjC?7CXP;hWvypW zV#QVAJx~5iHzAwyvnl4#wqQar5X4Ybq)Ns%D;*&1K+SZuZ^fVv-ysZHc0ZVEJ!fn; zXg8UfDeM4aw&4Rx-m*=*YLLCQz_YX90ytjCR}pijO(+T-SSA*!j?U@W*vDig)UouK z`6kz}1PwFY=Tv8M&?YY(<$`6xX}YP;Ms-{DjO=se?m?BO*9ug;@p}ol!1KEqf_T=6 zn&UaGKd+3AQpRmag6o>ImkFXz3PiW?1Y}V3OMlL}(8m_=2ME~^kFmO(o#a>^0SY-u z%#lcZF&?9noN@(feMK?`C8*ig81=Bw8?Io^Z1MWCOJA=wHFI)hcR%#gT*n}s!N$xxa~2t;O2XRZJz> zX$eRX{6(-`_`+>FnU%Pma@C)x0Bkr>_Y!Rtf#q~VxIFzTY7!Rc&}kQE|GmPH;+$$R z6=cnx>sw&eOlTcwI#cL#d5btKzj{JnPzqkqF0MR>jx6vs7{_LTX%lSf!r0{hsY0GY zes0u6O3_P6+p}-cdG~mC@BqZ2CHB{@+!_zFegAbqvtA`Q5c*M zd0-2DD{3-0l3x#j)kNxN3oOgh>VDF5dJT7ZN0<0bGjvrr)PK5cHNaHTGk-mQC3#`r z@M-WB`Ta_M$=Pw|dDuaz`s@9&lc;D5_AAnwGeXz%JcDw2O3R*uxjnn>7GcnxxDPPj zJ%4!qx>I%g10h3dE3z{}Ex5n6M693R z^#KZOw~zKx9CgvzTG{gQN1qaxde?{vCv;-Fp9wj2!B#y4DN#(T17c)-<;F1YnHGWPBcZdv>FIZ3V7_rZ1z9*6*DPLxqfl ziGNT6jjRkB`DGQ(2mDb`Q5<%!ud#?RDw}Z7CT*$|u!E-516fdB@;>7}V_g4R;*GN2 zB%=V(t%Kq4M%x>jb=ZtSnQB;?*nsN!Vq!}7vr0B#0=xHMVhqqO@mcz;xEaApxOAa^ zfuH*VpSys+WihO@IFVQ@tM?o7<`x=g9Z{Omsnc{-Lg^yy2V|(uJN?kM6MEh(+@4KU zdi>cA7!>&g%S>l{HMuY)+vUi>qpFY2cSs~!<&G-f(1tY}ZD=%-JSi3-v_T+s0acq! zPf*iUol6b19wEO9*g&C(-Dv)X|7KgpX=kRH&g^yYnE3Wu=<@BX9ys6ph$dhT(~RJ@ zdAFGO81+Gu1TdW};Ld2RT)>z1l(XC9FLASgzGrgD#qemCeXBRm=Y%V38qAMDtc&zW ziikvay6%K6nqYoxyTxR7fp=xURdi|I+IO8?3sAK-86dwKu6Lr8>T z4g#ZQp&4L&hipM?3d7)_pS&o;qUzDvw|4X|01!x}>pGAuhAgY@Be!L5z_lSo*<3cd zuVdg%n3zZ{8ZuaJq6IHU-_#pgT@)c|G8N8Tz7!%gr%@r2k`guYhGD%nXYPJO)8yTcXXS`r>gksb}&mke7=#zgVp2ZRsCm@Qpr!>~fO0rFQCb{pl10n4`W zQ~5nx*+@o;`dY4;$@Vriq^D*b6PnCR?J=(GfsLBQL+yK%%EcBoN+%405t-Sp?izyo z*~z@v?c4>~c-ZSJ4ex0eh#xBM1LrqXQ=F{L{F=cUy``7{h-$KC)0c$>JxE~6vPK?|p07MI6*^fNmKNmKVB8m-C8D|!1Mv^2d&k}BTbV=ux zoL82DFdNYo<$dac2~qQbL}GZAw>H(V;S-1^Z<1~m2fam3cuc?>ysK)V=D|So;$K#M4kuPyw9b3x^i&79=RV8qaTLGA%5_}rW9I2z z+Y$xRs^jCOKb^-*gdUu%(#=o@CT3H8`L}9!?I?3K`k}2)eND;)`mRGHFg^z3pdNVf zo2EeigZ5CagQRCWuAo~*fGsDGZLD`0!I{J$KLJrY*n+lGYN^0n4;2S)EI$5hrsuNr zp@EaPoP^NeSxe6V-5B%MLnEzAZ}%DgJR~qHR(hr;OrKS^N}UCd(r?G%x*r<$37i7?h7#%=pocYm<2yd3HcrsK*Llu4}#ri{#Jr& z~{M}@VgU5t|QDl-d$EEeVg(?o= z_ciN-&+>Wern&ZJz$5DSe%w0DH5Uw;1@XSIOI6Jy4vNp_eHCrwey00tIy|Ge+afC;%;6o+VYzIx z_BH4&MS3m2WD6VB^#cDiGmkyHQT=nB_0rhQ&YG9k7FPIb3>7w6=x74SG2!Bm)t;#P zZ-O6~@cVfC|EX1kN?;@Z2c=a48#O{5!18~;LtJZb+Tw^I`|Q?Y>gzQCEiEp;>VkqB znq@;m)`eVyp)*8*(K?unpo&Q?$bP+g$tuO0H`6z4HPPij_%k0lt1XvHsj0k*TbFV} zWw)(KTtvNQAI*raVr{oaA)E*74LZ*s47!eI&a}~qdG8ryyO=QmcEX&&ozx>ggWk2z zq;G~o*EABu%Nv2Qu@`X=`(sxEB3ALpQ~bOTxYA|~%LcvK0zmOw^l98T*I|+Mr{jfR zvImK=r#N|t(uVetB=>MjV&0z8GG@V~q5l3Yj3zwbEJnyaRo-ysGob1>8&TG$5^#?6 z2+*&l>=NNFTFH%*xBeZ`bBOE@3~_V%a3_>H#&;M_Huq~8>HMmYfNIFh6< z$kMYY^2q>NmS*Y)b4Q!CbFj{o3sMRU@Eo)rlqwpjQlz0A%&|=Rm zNfNo1q7iIOG-9ewOsI!9d!Wyske7o!3WRTP6wa9p;NQU_Ofp9Sn~a^c?}mwVwiaRu zSI4UDARLesvICFikNwR99SE6);vP@;jKh1bc*|%kiV`FKrVipMkFC~Dop~y zxFnna*s|m^!n|NX4WJ$o(eow!nZH+y8T(>IQnTDebjklBV{Fmj6XFtNX9>>;JBsK> zc?mrY0~y=LI52^>yb}UByMv_^G#_HD4(B3H`)}Ja8q-LKP-;Ue6KMCP*AEDZNq1IZ z{LThg^9C+anYi)10Mef)+%#HNpqR660{nBF6(w%;`gL&2DW|{r{6l?6BDqj(wjg50?%BmNC`R)2bHx^2MLgVMFy-Io)3M$D7sl0~G*39bYzemIYnuyX&`j_m*G}{N}yu7ilo( z>DRMsw)a-IW|h3M_w{?9L22-z45J#e(=(4E$_yR$ymz~El|Ki+D%amEx%@N^jVAxm z5KSeas^R3l+Y8XYg%I*y=k3VEndSKsi3oy5; zC@-)Ca}N3kt$N%iqP%gu;_M`%hJ2=c~x9} zOVxhXL6-pQBTgNfgn`9gG!qRNS49E=OgJ5@(4fVoQpc|tNLm^gC}y;iML@QRogO(^MK ztFTQ6hA1;GIL@<5KO#}bbF5j{u{E`rdCfP(EmLSw5rUMYL`M@U)(ZaIiNf)!~5+mv$`Jg-$!@~>0p(%|Xms=l5kM1Ly z!5g%Xkss|V3mmGULMKXOG?0lBeBZ4K|961!3b){!y#;1O*@k1@XcZr$4B3IXxZzlNJh}S8UXVmIG@dCU++>;gBMs00m8+%rmLg3lSBNM!KUYTPPZn=#;o5 z9MfYrxhELtp#=kvi&i(;DuyE9Q zUB=j5pi}8WXDjrJDlDA9M(;nkpbwn(sAFRw|6V!F&8^`?+0$4FeKHj|p7#ZXcH_yz z_OTB%8*Ts{Pn3gXQ8zeYgQCK5I8Y>Ro(d?oy9hiCmc)f>{X6p0Br954s~i-mg}1MX z^9kR%f`Z^kUA_jy*ED|gC6zWM#6ff3Fk?c}TvMvK;>A6JzRc{m;K&ko+Q_XhF)^Q0 zc3&2C9qPg)1U3b3RNDdwFYm9St@5hcH;oXx{~uw08C5y3v<<_9ySuY-cXxMpXK;7d zJ-EAU+;wngV1U8h2ZzDk-QneY=g)nfKVOn7E4!1mlI*^^s;j!X;_$jtOD=@*d_n#r`RJ97IX&0 z4Ql+=X{{@LQJ{kCu^VB>{)mYxI0~Dc$zPFL6`wL*+pHM3Xi<8FznQ(B=ej`X9MwXm z@26xjS%xv!a3JaXGh2zYpRuz*K5Md7eT@G{$B6|WD+YU8cK*euq5)PVQv&8@8r32NB|9T~88! zWPgsFTg<2#!QkN_Wl*&Ni1CkCXHxXDXQ?Sfd&~Kk7W2~ZE&D^eYMR*}IZKUDw_iVI z%9Cbi;yu=LS09kWcXyX!R$k73fxi|XzX*qo9&dNr<1+~DYrsxJTuH?3{K6iF-BP!s zLJ9A$^kvuY%A3$WU5aQD4O;R-Hoj^GJW6_JO_L5P&=fLcM31&veq})*be^`c*T7X(1TA0VyqFNNI(tyY zwdv_BJf@-#(CG3mWGQ=`X-xrE%Ci?_J?&*hVTVQMrSKUJRl7894(US*ro6e;R!(IT z9^r$wDJhf4Wibox3q9VQZCQ6p$KAFmWZVh@`s6Zwazoapz~7dO?QRq5oy5F2%0rDa zCT;5k4-Z*uZesJ33&uDl6*%AGIiQ8gZP<*X1LvJa&FVUXu-F4F04=I}rQtOf=)=2e&PH7~C% zRAhnuS z8=GeDKmqXVJix6x2DfxM>GJ6!Q~TYHULH=;xoE*fUl-)A{tk@`8~Mdlpp$^!1LY96 z_~zn2Rdj~S!`!Cnl8Nejs88ng)qDN9b1Qxnm#%dfzxEVc`G_pnIs2_gV3*k8D#pP3 zj3br`$df+V#y-vecrzPSXC8c6xjA%FtgFPMw~vb}z3ymzXnT71Cu1>I%X_19fjqdA zPS)|7-<_Lon0TAOY%6kYQkP$9JuCbdN)7{&U3)9BZZaM+o*k|oF0S80fFIm^7m;iKS?{|wUV^l}q#=brfZw~* z#OFU@prW(|K&qygm=RaN{{ZU?*k8c;0`3>^zJUJ)f-ew$f#?gwUm$6_0+J?yfGq#l zxXRU)Pp7Ox%JIYc1&%02vK%fw9XQPIJ1OfeA|yCKim%DR=`Q z^VQgP;x~BiB-%is#g^`E_iifIITYrVV}1kwr4d*ev5YFNju5@7I-Y^p5^i zM4~s86Ic6&cqK+ZV`VO^u zEAoUvUKkTc4h_lF5ASHyUNn2NN?RJx>$J{zqk}N1I;>X>YtJ+maLnu9f2>aw-$y*j z8^+`i;Ek`xhg9-&&Ny!{Kesjxk<{XuPpXv_g}_2=WSftc?O>3(fHoaYLw&3maFVzq z0%2qXJHe#{{ATuZhJmkq$C`(oV@WEYbVgB$mZ*>;trIB~iW4OR&zSNr?7Gl*?9WZL5Q?9$RKZt{Mz{W-j0i%!WD(9C=<~ zCX_Y{7>5T1l|>*3*JBMZ!v7t#j5fBch;Ut`QYZGCqh0;jo?*X@OY2A8$q(XE&CEzr zk{Z!e=R9mPsN$&s2wT4FhnYZcDG!~#qvdC4>&X-kOB@`(A=#A%Sk zB&}x=?3CurKiItazRQcvO5MO-EV3V7m*n340b(u%wfr$B(y7WYg|I`6wjd-djz{x{ zpTuPqXRZ4#0l&ikqxko&LX5WW0yz=n->VTFZ0VZ zF%VUId4wTBV3?a63X0GUn;Z!6m{a`2;QW)7IPqnRN~MI?22w}#oHPu^-=bH5j8=yw z0azru8v2r$EX6{KMd~nV#9@{D>wAI8sTAR#1{%H)Nd9Ov2RoibD~pn0?i+b=M;|!TsW;-8)^|z05phVqm7S(tFkq zI_2rV;Y9z~PZl8RzWFF0*>)?<+`d418lz}X_`#s=xh)yX&jp?=m40YlV3Sd+`vDjZdTT$6XKEh>J*`s`@UEL-hO7-nf{h9AgsK4nxb+h-> zl^dBb@r1yLVQ|xNs`bUv=fV8k<+i+kL7?VRcIxi}9NwKm&MPR)Y7C#tk=@Dq#`Pv# zfWp&9;=TD15)Sjq{4&IE=@JKq=N72HJ>iM7&8dZgjngW*$;4!za4GSPA?ISzb#v`! z4zWqUr&*RINFYB-r_re3fnmuj535y}o@y!TB;81oRmp|!(NAE5;+bHaZ*Wbo`_DcB zl*=OCgZ;Qz2|7yJ8AWn3wM@|fbtM8430%Vg?~|9<@1sF*Bkd*lRU*HE`SIXg9yLS@JZPo60kv5`O zl6i*HpOo~WV}2n-6N>2ysHH%`g)TRUP45v8uOFGRg7;pqedR9;em||2w$2X;ayS{x zL4yr<$_YfFy-{tq*@k-E5pqvHmEKuD$p7l7FfzrAzDCm+q~zGgpYXV7$^$kZ1KKf- z5yn!bu|(BAyFJw1wXF^>Tj6#zW}JU@;gb5;GD7U1{JqR(Q9h*CO34M@3sI3(k;(}_ z<`b@y@28vwgd|5GUt~f0s~XhgKQ65@U+?-2yLMHx9%W}A_P?M+z8oCz)@eUot_Qj` z+)cJjb1!ja>ZC3;YURsayH);6yV;EJiujtV>qqNG^8QIaYJmK-zzkB5R7N^affkBb zXX6n;vx3%OZezb8o@D|W+D&~!I6{n z;GZZK9^K0ZcV=!lKyS$11r=@W@#IDUE`@}br3Yms5~o_6H+vw{qW?}0dqWv|!ofM+ zxzj1gD|+xi@9qjZQZBG?wQ^4T&+YHzRK*^wY<omN2|U5P>s#yz%A&uJ--ALH{07wZN5 z?A&dA!%Lt9dQpsj8w4JGSq zP(?1^;7QtkYW3ot#bHX0;i#23>T|BNYJ)39H-kxx06x37xHrU;(2skUZw1W!T34JN z6$L9+9=jP)0#yz>Dt&==mjTBMqsAvxb5TD}Tv6da_gjvNRt{Q@y0NwEEQdEcH|p~9 zdwvr~0}sk}4?SLu1bc|w95nZ*C5TCKwWF>A{k+$qfg9Y1T8!99YE2}&18s%CigL|` zytne>jkfNafDMDc^J@pF{|GM(A1~^<@iYh-K_+~0dMjEVi&&+XF$X)vk^(~VEhEEL zc+X`omz^Gn{JG=8lEPu9_qfEvl}6C3kd0z%K#?e{C;dm?14UX(gu9e#&3~y8G$%*wWBZ@JnjgJ5FLJ*>aYO?wn)6xp=uL^s6#?@ zQc$|66KXp%n4Gm(SJIlc@?KU0c4!{Z-F-hfM*o`I2{MBHdLpFYYj%~pcNA#d6; zr6AE9TZT%f;~j~@!^_D?+K9?b)Ce}*I?6BZKxUUN&pl(eJt(1n*zBI!&Y^5TuJw)c zAx6AQ&#gy(U-(7oN*v#mvv&Mlxovis$U@`aYv6CHy*gGVaG5f(rcsn4l&z01fbevN{>2soL#` zV1{kJWBHslVk%Ox7n24{K^1N=wQM}%N^4iJN(3DBY?^nABM_)OSsqLY9!^b~>)5Af zzqreX_pHgcAhqo||9o_4H@a}ZN;c%lI}y#Id{y_r82mgj;0iIhHsIr~RPJ&z=_-Zef9K}6;et3^PmHpx@TQ)D6jM!N} zf4>+=g>w6DffIOV#(XZ+T>g?F@Ed21r?HEBQko~?B|R3pNq3z|(#T^a!cJYQknz+E zS3!D%UB2w}A`?lh>(ePP8Kae7132DloX6C$4=h&AnAQ%5c{Od$`el$YdBaV%L+oG}5Uk=Tv4=LSD3ZSGtVdk*GbSMA~|enyk`btwq_jxo%1LdW;JG7 zem+LQqnTsLqh@dCqdPJWlzaChj+|!k@Ah~>vVEpe$qel1K;e4Fq^R2fxgUi{a&ON_` zQ%T@wMe+NMU!0WICb|1j(I%%nwMN;|t=0PiI@}|@0AuB$-mYON+Mz6>z7L>v=eor z?r!GE(&OTtOA^g;53T=lGr;nToBxlP->_{GK@FeoiWan|9o*co0l-#Lk@_ENo4SEn zZj^`_T9_fbJ}v}AVA4@solQ;iv&WmLrlp-zp#`>!E?J_NPqj`NgjdZ=5l;SU63vNh zoySP|Tnb=^HfgXMdMx86^RM$-__(@rY9o0W8k%+E1afZX1`7E*no;Vx1z#UJaFChQ zj=gwhDj2WKlWJ9oL^=x(cYj4u5-*-Rb0mzf0GIHWR+_wdFk6Hx>vo?Ue9frQpnNX+ z2UW@=77d1^2$q(c;IwAn_DoxH^95L1-`$ug*W;<*7up8}0<$NJX=2=z!>FO;)KtLr z`q`j*fy%7C%!VOy%D08(NN;R2*ntHcL%EQY?PhB2>ZE-{^9VN$`}C1!jcnj94>+h+ zFcxU;>7^!4Z=*+39B$AF=#15n27Rv0S5NU@c zT0*1H4*NNx*uR?&U=>1(NuqP2(veYF0~ErZ7)7Y9Cojj}a|>@CL*Kc3sKbnL{>50h zq=)rfc6Re|*X4iGJq;Rp);Aq|Y~x0_T;KGNB(%ZC|F_l)tiNiV>;F;icKs}f;g`=? zLXNS?%4_tgBC8xKM?%(}{hsm|EeH%s&hz4*@8~^6AyDYv_VT`zy4Tv-{$^RCPnWG# z4;+!|X14O63tM`0X+G{D1aejGg+F`Un)(lUJ-)QBOO2GQ5#f$#cZu3(`-V!wkR5oP@>!GPVU&>71SjwBy20KKJ6=UkJmZ0$NWK5Sqq`cr| zQ@*?HDnJY=o582Yt5!e*Em?p_ZH5Xw!^Ak-K}_Yx$04dQ0sVkq4%$KWL&r2pkPX4K zj)%1$*5in5VR89wg*psDN$7;U(Pz7?1xQ~FFs;ZV<(vHs%f@>Rm0`W&Z;mFu#)iT0rD}l!+1*wVmAc60eq?X6qbh>b zpnIX;ZzBnoI~(-w_;~g5u;A5_DX3)@;CR0qs6C{{;VyA;!IdbJQMK^kiC0-Q(SUR7 zLn`sK4=iCW?uzP^oF_R7Tz#!aT3O5)*a-Y}&%bucl2b{}9!*07&x}*dyTR>_XRFxC zMGb$Dq#u?6a>N45JTMkWqv0pK_i`xznru)it%{A4m!3yKqf43|oJgCQn8_qUuk1KK zkMDt3AwfhFhc+$>XQ}{CA?lw8-f(~s$tj9w2b>bA9=(GUv%<5h6*3mw%;<)^Vb!8@?Xkd4AnU46*qWOFXgJC-N z{@PZK-+X-oNnTd9faR-7Y#n~(yZaiQozn?wwzG3!j3i4*5);4af1dgj z1zMqm=+r>~`hL~$D__t#a-G+gukEkI*o}HT&^QX+jtN&X?RppGolz8#j=#C06K5Be z-s*7g+4_}yCz{lzTHN=y09$z&_9H5E09tq3wxy1r8xTuIO$hAgaj0+80vGdkaMM_2 z3X^R@yx>DQIWZPB2xcJYFjS)C5|h0_!3E`+1?3l__-W2%h;*43s-pq)sPy&95T^MG zXHf96p-#*qXZBF0Rtj*io7~xtY5J%+l)SK092kBkP!D~fnUpA`dj+DjIh2(DDa@hW z1DRU7g-}0nC|sf6W?cc3T}gi9QcX}w&f%Yg!=2D3FRE}W%&2G74jEvw&8a9SMN3JA z!x>@Lfip+nvw$#HY$pbPAo7O2+d_7WwOy%cfWF26e+ z1CMeHP-^^JVemXT)M>loIbL`jV99}VcrbaYj16R9;BRlb3wT0^?QeH~ekI{&$Km}C zE3iO^jsWWa&Btw+w&wW7itx)@OasrBpQZ$BKQJZ13AB<{1xq*l`80g;I@-S2&G z97>U?5}V%0pHJ-^1f4b~LOLH8N(+nkz1@zUx%~M|hWo+XUKQC;IK8#CFHuKreCg+= zHhJR@RzB{%H^-c>*O$|e<&AaOz{B||k4d+c9^ns4|ZxQ*hSn zAxGiqE`G7-u|kUWD7r=H54y*MUwhK zU&Uh{39XP&H+`*I`s@(>>g6k4m@3n!YMk1Y$)N~n+A{~^E)dbLnBIUV;J#fEBxcB$ z)@Ca}G#3qzv@22xB1?qcCq*hBYC1bq(v>Uazo9M6`T~!P=*&T5(^rTNggDX(lCcu;n7$Og=6^DmZ87lU#pL;p@AKh zkm$wc!!uuLJ+)15GlY2yyr-xM-8r#U1u(4YQ!otatLgY#hE3?LALBC?w$1QWjeM0h z-1%@Ya4(qY?D*XC{HnUJQk=3N=n`1tQ-SthM(??NG5UXvB9&gpep1A)TPz{Z zpJj=18?@0JrQ@mMoi;YYKYqw2VT*(l-aI03oS4AGzP;t09~K=e<#M7$JGnLv!>;N` z;;t*8oBWy8(IOVX!)s%Z=7pP%K45s0RDd0v-e30*Jfl5Qxmj9kVcZlc3{+8u z_whObp}L$@d#Y$6YF)3gO6YxmtX==X4EIVFW_||SsXuR3lHc_?2n;9;0*jUGj;6_jOr|uO?wkOAI-GR%}z)pD%~F1xmEi2TrzfvLNDsj`QLZNa074x zS$O}iP-j%pm%#+X%++1Wa%Z1MBqzDm)GdtCz?Te_O42b2E)4BF?>F?1y*TSv^$NI{ z+MPNZcWFZ>q0bUb=TKE4pGbJ211}t*p}8s!q|9g#wbt%{nHugoG`irWDbgaRi7wOJ ztfuSnyiZNzNE)<4&y@$d@{y4&kh&t%9sb-~FCmVT6DqPye@EuUv(4ym7ILlKLe#^RW14Al~(?`*<-jjJ`;P_6MHG(>2YXxGiuM=dhDgG z%(^W_+;x9=-zW4Avg7b3t&|2Gq@>1?@2c@4aaxh;^OO0|Wo8YnjoT1E<1RNF)-M}^ z=??pf_IVYHTDQdzWPz=1LBM&;1EJBlBB{kdxur*D17ht@i!oxhm6fFGRn0_r+5B;kz>urN^ zvyWE@ToqU~$r=VFB}OXAHecau;OW2SNp3;`;6=g$n0V1&LwGdd;qRhXL4Oc}g)=5^ zNh$t3>jdrde(!}c47up8HEQdeURc}r2qGBQC@^b(6?OUnM4l5Zn_jp)al@gFNJEz_ zK7*=mG%*z-kq|`;6(>$Y1IrF%6XIH6RC`7y_4DPcd;sHj|K4)BD)g1}h}4GCUY?KZ znuC8L3_yrtE$J`FE8M}tj+d=Zq#NWdagp)PN^}L?71VH@6p;i_h{Soykl{Kk_M!Tq zh9Nw3UNfB1y3miIET%35mm@mFXR%RR8O09;!`&19TuGf14kWrjWfSCJU`Tf8D^q3cb8nodLKmjWL$6o7t)jnEgl@l5o zLI%{AVIrPtWj!=zo6%<$HpJ}^-dtLB7Dm9C&)oVY=QW03{+cCj#L!(SiZCLOb0dm{e_NW+gN4oS%-rJ)GWMiSPUEG|e-?ExLBPukt&n??b7Z z0lCn?uGmwJCS)-+@WLP$3*3(-Ru?P}T zK1b7Aha`0Jo)*#VlbA2McKjdH<;#e10@eEipg~YR|1a?Z()H~KWKqL5@97U%O;}HA zyC)EFdkuOKR?L^Ue9}u>wZA6}==fgsY#zJW5)sNka`~T}oVfk8)oZ$Ne91m`W?I}l z*uCJ&jT!E5&YwTMX1i3oPRv7|ACqekKAVzz>hW92(>lEvf4EzEpu{@u=>dMZQa3-Z z5BHzz-(7R!wLeSB$8SBmJ9-El7#@z3X1$!sH6m{mfv*p~O3d8zyAAE#Mp%QsE1uqh z(@ulsmOy`*{97;M!+NLImB zg8o-W4azo5BZO~b>4&di9Ymb3n6j;`IF%iTE95U^Ohjv5Y;#!%xOn@5h;P!ZC5>OZ zpR&&81bL`iBdu6p<%VN|;j5`={=V)i8Wt_208FcKk^X zJ7FRI@q+!zMAwm3>=Ri|nQ~cZbRs!v(_8~_Q$_=XpDR8M6pMXv6eqUw=o<)4cN1h6 zZOC0wD}~%Djz1HS-<8`!kXEUCpL;y;D6~C8wD$*rO0T(IGJ>};zP0~kf zkPYVfshn%1P)^5!R>Sv1A(|o+c_xGTTBMwiAsYEauUIs6zXqlce;n$iHzv*~{SfPW-o0 zOP&^sNO3YyL*_HE1vGrTUbJ`5|L4_F#+NzBPEF+i(CU*&e2~G7(luIlt+ArS2Nar_ z>P7{nYJU0}4Q`ELhVYxHssv^%z3jF#Rnq<~P-q<&r)h015kXfIpBsq}WgGob6owrJ zr^k`r-Ef{D?NxY@8<;WD)A8)F{qA7mm3g?|MsSJgO+O;Mg%&~E)#I5HU;Y~b_z6Y_ zctih>>=6K6djar(Y+u607e0u|L3*eou1xUkXj#tE+P;`4;_Y?C@yG-m@9r(Hq`c(k zV~ZAYvJ+d8C`|5LvNHz;Tqw3*scw3RMjxZ5|KJ}+`JWhV`Tim@M%npo{jc-G$M(>* zZQ1M(^KtVBzPy(DiOUqCM_vtgC2jnWyokZ z`cL#Y(QK&foOlX66B`?2&l_Jo`(y|iabyf0N232q!wt?#kE)CVKVyEL4=|Vi2^;p>o+Ph_eZpMzf~&JTdvIr%gTs$MMt!L*r3>k?vSG)1+K@yR-C=1W z=*hnJ9+z0l;wa+q-q|L96D5t~OPgg76BlD)dbh0z zJ2rJ)yv&oPkIO_3D&stJDWhC#H22R2USD=A*W`A5Fy#Fk7wlQt9KJTKYt5G=tkEJ= zDr&W~K6j`l;9q!Oks4nXq;IHRZ;H0x{P3znT#qk5@DgnJ<#}+CO0O&z1ltToO9eCx z;!xN6fvDaB?I0+t$wtYVq9lsm4CMlyxnB@kDe*u75!ShmF?hvJ7{x+Dwz zjJPDL+rEp~ER`ExRffKr8&d9oxO1iv#y?eC0*O_iGM*JRL#fUN6=2z)8tT7}lNL^c zr4ANA>m^%*kq8N}9DDf--KC_P{}T)qq#p#p2kQZO1_5YPSi@FnAOHl|UA>N?i{22xsOafmjc|Ms6U20kmKoAVk+M;`h4@dBO)JGND?xvbIGK5$Ve!#W@fj zCiWPgg%f)wiYQ;o`WAWk*~cM^^mL^WLLjcvBs3ZRmN;_x8(vSCnr>33mY(7qx|r*n zZz@(m{qZ{MK221|m)>PCh2#el)}QNYL?qU|be>e__NS6FB&>+^+nrT54@^&Ap<3&3 zxj|%rPnc0Q8Zs!0I+S^8!&wZ2l-we7sNq#{jxHxR@hA*02~$@~Y?gykwD{xRQ&M=O z>Wbjj!|cEbOMaaw?&r~^i89kaC%<`&>1fT$O z3m5P1@fANE5dvTXgVe%zCH?=MjF<}rw9SQ*b*p`O3zL?}NP%dui0q---e>l8!rqZV zG62h6bI!L{!SbKuj%}SG{D3(!UZ$npzcqf-T^?2AQnnWKsy2mUSoV}H(VFgWg!Fh6 zbj`Kq8WppRYX6#swCNxh3s#GD33QLY>yXp!l0~eInNrv)>{A5A)#Q*hdZvLSxEgNg z0IzhgWcr3snZQH`EJ=J~QYG6P%{zOxqU1goEf~}!iT*b=s+DDJ%kBDa`xxOnmJ4%2!b_8?*03a!MtE$fedgFapdBr!#}nBFEqMNGVP$YPWP?;KcUq zp-XX-{X5h`=laB=)Li06k`D;AH05Zg&=}>i+(aoq-f4r^#+}KEg4!*h8%TkIU$Gh>wMjCJ|loag~GBF0Z znR|Z(fpIL3@wv~A!b7qM$%Y9pQV1yQu_)ln6m*fvekUg?Ftnl3Qz^+8w+r=Dh2fNx zHRRRC112>i$l-~}Vu-My(FmSden(x@O(j$P0pqibLV}b&z?W)mUXU@CQDVq2q;vdB zgOoo=QlE?;7gI5>q_#jy4gq3yf_!G|=N})kQ*=K6uctNwAK;sTr&QNPNh`t>37qE3 z7{QASPOi!+7eGhwVwFf&*yoH=wuMZF9Mimm0uHN5z+wD??~qH$q7w;8s|ki+XBn6$ z246=)vyG@yA^Gn2*PR!xNE)GGYmN9Ige3#i_YFCix?EJWKb?ZDLhg2K&*q97ow#cF z=GaQC6e>tw2P{;CS%=$nl4dyrU;IWICGLCUUS1@G+Ng-Z({GJY_2bO3q?gKKY6J>H zb)cjSeF_MH4ZaIEdy95%*2clsQpd#|a94CV%T36uq%IFyrcGwjtt_-1)otMOt(P$` z&g7sc$3rdx;Hr4BbT(_iLYf+Ub5kP>EupC1%ld=I(VK+Ez+i?u#4Dx9p^k}!zTPA3 z!*0yPG%Y*@G7uAK4q*3reP8pxv3S2#ZQ*d34%)w!hM+8-#iE?JUx_1Z-tBgxJ+;P==sy+WY(@g!es3YYE%#0%j6F%+ z?`CgYn_MGz+g^cni0PP)P@?`#rwbJ3RWhYwKQK)8hS)v#{f&8kjmPLT`Kuu1JCHuJ zd@|bbGa3dDWWuGjZed_4I@I>#{bO%SwcVX*j~z_?gZG}}%a z-P%!Vyf&>v?YUI9VQN3Vn`3L~(SiBGxf9Nb-pSrkE7cgn$^K9`5`*@%fraNo6vwZd zepYvb#=S>Agq=V$Wg1W!r469d1(K>W)dvqiHi9J<(pD@`IOsini0r~Z#H|#CT|(o} zyYg>dE(*o|x$N-J(jG#2cO?3I@l<%aShl}dm_J~WIKT_*u;rB0zR&gbQ#JO_CYj56 z+<;}sK;e_a6+iULZ`ri#Zk`}!iiZZ1oNLCR!N8$G(V>-^8b(h%D}8+{;F*;HBKcKk zY?EzRLQXfzCTt6PH=5zlzRbo}cHo=n(0;BJM9(;no&Hl-EW6s*gRo6?Y~Wh0nIs(k zk-#MWsO@jp!Noz?H8nA4A~?j7U+CE}8S)627-1Z$3CM_8HF{$K2gbOZnq!pzF!C?; z9M(1*;+^fgw93IZH~4o6|lHNM%w>-0J0xj4z@>VWE^QFT?<|>aWzci3SW^eT`6CsTj1x*bmGsXYpk^6 z%}larX{3?Irgm%GH*Y-}#S%=b9!dQ>^R=}X0jae`3>$vXV>=ImD<&^4Sp0MH_4tKV z@2a%CXhBcP^*oN0m(4#$pilT%}{+<{(ShxRW?IuSY2)LwaOFGU_5n* zBB*SG3>SD)`YLT#oe#(Lou>vWAY^6 z*&*=ZikyFGB_c1!Kp}+^1!wqnv~&M$e}C|J6c2HH?667ruv|XY&*j-e7XdS#>JWvv zLc{xQ3oMok=)?L7U#>9y2B$OBMCGTlGn!=^#h+k_(=8^LE-bY`kxm zaMw$Q2dAghGD?!0gRhyQ9m~Qe7~;7VKdRW^Nm@B5WL1-)r_PW0T!Kn6Pajk;3PyqQ z(|hI+LdIg_Z`hZKD3~)`6fI%d!p-UA5AK_;3JFIB48gQdfR_AwO7K2Z>jIe zKX1r0eYXvhD^l$#gl;MyTKHFAC}qp#f$SUc5t`>axbt_7Plo2t61JO}MRls0m=U|f zghUhoSU3#H2bWzPRvZ;}V$Dd=HZh-ya-5bvM5TiOZ;1h;YuL1~FP{sU`5n!3<&1?I zhWh=_+3z_wHZVOKHYEQJ>`FqJkQZ|2qkM;JG#XmT*}#NrMpZ!-qR@yq7A?(CHgQ%&{RY3LkaY1GcIfWLYU6FnFdl*6=Hh z8;PdGC%_vdOF`0X6U5C#;f*+53@Z~>!{SwOHUhZ}*@<%47b<&bKEnK4RvanWFHXV%Wle5uTX=-LB7^zL$oLT?p+jh31$nq5_ZD=l&o zdUEHP>VzpR{Y}=HY6gWO9RY$$Uj1AObx~nn^)wpo#_l!OYN@tq&9rZyD7K=yon0I& zb_|5ExEe^7j|~5X&s`*`UljUe82{e_kXDP5tr*w-VMr>tgd|1a$1N&V32r(j8KzwU zYRn-0!$fppJ%u!TBN}N}d84W$Mj}%jF79SRhw{i{x`mF_;}d{@rqLB4o{e|NimJ|z>&*2 zhYCf#?<3Ox;)}g7Y*=}fQtg#e>v_lU^R>^#j5v|Oy(7%Cs@z+|H59-w(eEU>3ll+N zXCedidGi?O?i*3AD-LRj*?mb7W(IQup5AN7c7gy#CwXCHD<6F_ESZEm;v4>eh)#`o zJs;|mC{YdbD1P1Qj!@&uI+B6hMtk%2#4 zRzzl@SBj!1Wq*)jp-O5!kXM#HdjBRaLJ#rw|JZ8q!=EEtPId9lQCr5^1~&;FPryG# zoFIJ)k`u$+iUANs>E?FheEYW(Qt4y&M_OM?Rx6axnYv^G->=4^!;G+p2AJ40-}e>* zMrdx5C~win%c3XV`b{->SAxamJGP08vx&~PV^pr^k{BPH-^L|zgNI1uPRxLT-?KC? zZa=bjI5m->W!I3GLDk{GPViZlZVcaV6Qjds+{2ZrQ%tPJa+3r|Z+tQTxM9+Dx33iT zEhz%hvHfA;NeB_B=Eov(pn%)vCR&Tq%j%~ns$93ye9R_f$$17W3REoe5^o$c&|K*1 zwa}TKpr!l$u(vnj@iC8tcycOT z?d+UcDPiUQ==H|*<9=nOT#_#bD5PtY1MIoI^1eQNyV%=*zJ7b#JG;%b8s@RgGw|<; z(d`c4&js#Rs&D-j0iF%t?hoIlIPqNUGpAg+Up+x^39vqY)k>p}$|fPZPy3rpGwFJ0 z3&Z88HI;PYso>?6^VrkF>D%5dX#IE_C=BG`?S2A(&j@XqCO;y+O%%-WrayjGWQtn% zyg@8aNl8GN7RsNZXZ3OAdyR#NRiA?|01hYJ2q|$|#q7TUyJ zQ&Q%AUWOFh!Vp`gp3g{M@=EIvTSCGfqIVtxa|v?-3<&#iQ?v}Vmah@X7@l%Ud?cPd zuP@FZyACH7?ljr%QuZI;ae6)<@QZ%y`se1#w!oMgm-W=~->3gT7LOMD zj_eMl93}v}R)oEc2BO;VoU*E(uzgB8;Cza3DH7IXY+|W=G`dFyO179W1nP;p9-)B8hjYE0H3Y6X`|H6CHM!ltQt*Tb#^z@$`GH3D zcr*LZ9`+G@X0F?TZw(W)n+BYDj9rp)Lq?yj-SVVd*@9tDeOjz zx%os>Ox^2L*?+YT>!NQMubyvqWSw#-{H8jJZ)>GX`o1K%SP8-7?r6c`s|9MMn7)p;@V^uNfcou=UC(zdz(#uoVXb) z!#Ao+e{*gum95BxCsHuT6j&if<=n~Na@bM(=arFt zWENh^g<(#$cfxx-knwFNM2m3(o3nX0cBw6wyz3i2PmEuuwdO+C5dZp~<`g=)PhIs# z{H+(oJC*x~8!!#Hw*;*nk`V&mZ?3CQE-&6aeSF#Y4RRQ{w0_$-H|af0RzQxC(v#1u z4bEF7pjd5c(Z2(HiVR_{1P6AK*1Cm^Bfbn&E{@EadZ`dH%~!=AIf_$ zXv`aDPnID9Asq(ll=j!Y{kWy-vWe{tK<**v)9R zYpDo?E`2_07cz-dxHr{vMu|)?C`XCRdOV9*TnvjBYFr`<|LOkuEnv<^ja%2u=)Jwp zp)XAxMd0(!#wiZWW1g_UOaFa|uji76@*B_Wt{ap-aohv7A4lLz8aJ|PX{u{XgUbW(3EZt;_kMBHBuy`bH2r5wTUaaews&9TQpdOS zQPL{bfY+4t*nhdF*>G6tO6XG&ohz<+M*Q<`b=v*Z+xu>~H>KY%LK+3dFG1s?{5eyH z3w1`7;QBN`?uFJ0>F# z<>p~w=c6fX>kl&SZy@2$JkT-nzx3N~*y5_j1-{sKO z>fm%aC2-0ADbREHIAOjwk?GdW?oZzO6U+R z{@^rW)FGhiH9z`6I|HX)h|p08<6DUGV)6~zB=WK4+f+!*wwNQ5yuq7`UxLl=VWag9 zM5e;>e!hC9YM9f0=z74!kGSt<%aB}Qli%Hz!GW!zHQ())p>GE7O@{W;!m~itH18X;BZ`FpJl0`tAg>vZBRAOl|eiT4VDfzskakn^f z*pAM0n5XLuNk}VO{<%SHf|a7r&dgIxIg|vs{%cLK2~zT2gMY zNIgq^g%3}YLV0YFwZRvrPkrssH5{V>@b3kC z!t37d?bmE&rvR`3^CRoN=I;E7OE&Pi^#1%V_X%0{!;$)w|G4woF!>E4;(p_f z%s+wR^C0A&>_y1Gjsl4GDs@>*(g%EuDfV?bg*lSG3fZ|DX#E7dsJ_+noFvo-h6WNc zV@qdG*N~Lv56BP9e)=sY%*tQy?%?LyzeBzg2C5M@Mc3pP8UK+VY^YAYpTCp$&g9`5 z))f}-3C_oop2b<5o~_$H9CSI!yGOWleJkRrtKj)jsmNt^)3Oul2of zz688=@N{!-ydb@Zzm@R>@{IcOzS9QE6ZSj>-LKspJ`uUR@jiTgg`sEQQdVwo+2u*- zo%2IPEqSa)xTI&0L^k@e=zjRxWx+CAI4L!p@<936*AhrYTk|>o;?|M3Z~Xrib?xy? zw*Ox!XA2?66$+1XNFj%Bl8PmTo%ZA1xe61;unpGZTq|< zj==g)tT$~`B2!Zau7egCpztyS9>lizkIQGY8MLz;T9s;iun$F4WVi zYUr&d-w_t|w3oF0e3S3KKkH4$_2yNh-T}5ObDr|F`AAjp72j(6p&*8`)|I&NVuoRq z-O67x-VqNr2A=CoL9pm>=Y1oP2h^K=%l6^%f#a>u`7vmZt{eyLz`x;z zvpNLRkz}?%!I%BOem8>d#!_K+bCsjCFmq^QbZ}R*L-ux9w?a2`_F_qx59{MHAj4f` zbhQnjl|+7B)egZo{3G1KIqh0Y_JpeuZs4SL&83=P{|FCo8X{}0=5RxMP419W=2{#$ zfPEUA8>hYm&AGxpQ<@p~Wa2flKCaq#sMGUxcpiV1_X-87oodpa_(}CR&jPLsBpKY% z9Bkg#*r$9k@3~OQ^QX?#T^WFRU%1cnu=(!aV1hB@LQyiT<5o?kg zauA~p@jkze4|T~U$x*an-=9(u;{rzXz|)CdQJ@H$fF}mB>nSzh0qxAX)hLz{b5Lj$ z)hc?zALOYgJRo)qwe_DDMI}5ZiiY7!_eACiX~dyNO{6@muGMbXY7G@ON|~=4Y~2?- z?e9j;BxurxfN&~p)M|k>*lM*dvj0S2=nY=FJSsXULMF5j8wb|g5A%vq<;2y3fH^O6 zN`wY&3h2etU4@<{q!&JjPx!$vDTfVHvf@Xsv6hyPan~4d zK7ysajE0lURt+vS1Xr-`|9(RR4X&43#AstLO)mvsA)lhH@sUw;4{_ReKk*YV7p4J9 z_!X-f$&=5BWc-aSyCBN@xPdLtAEUK^$wzP4HCC3n-{SnW5ELnOm#Nj_2 z)`}XJzMC?hObP_%l9wn07sB)TOT0y)5|^kK0C-A1WWha}`LmS3M3b<__z#o@ay5d% z9vE*S^K+LCI0DAMV$9zFtX5y=>`t*>?)29OMvUj8=MtQ=vtYX^_1n$xC$k0w6MVII z1MH<>pe_@!u$Og-xy6;`{z$lW|J+EEBm z6FjgdwIZRIKMZ$A{DcO8#-cfoQCq*M{X8b>1*#a{g7+zXKvRntE~K)?);MU!&!9mx zMikhUgp%`ZnSBfaQ+BhLuTu3!wHc2Fowl<02YG|23tY>8TW24V_C#3D@`0w=WO!ox z9yWe*;||~+{HR@vJqo8zeWEe$491Ha_^~`b>LrT3S;}AMJwnNGNupqu0W%F{%Ed0E z@JD!eP}*Fq)w*NnSls-~z()S0cpOJkV(*`&Q2g1Rb14FKHWYD%eReKapcZ`n5(~qW z<6;@nGp)0w*uCI=B%Ur+ZY-O7k`aFSE`YJ_mIWJ;*5}?p3b5+ngCx8mtDjkodM1?A zJ&NSfI*{`T3&B^w?$8WGc7zDas$^<&Y#7Dc7g(XpLQWLJBC}h}<*|gaT+N|2%AcaM z338A3X>Yhf6S@%h6%PtG$5$`C{4910=!# z$?852fg(wGrH%iEr!CayZke=U7RQ3=YXgEQb=De_&DqJ=i2qSbd@ME$HW6nvZ|xV= z{YqVCe^U!K5?@tmu&Rdj6h4>(JBbg~!1`dBQ9~U?X%AUc%iJ~n-#!>Clm`| zgR|_|4)EN5aUYf%H$gb>-JtJB8*erV$(M#jYG~Uo|4lGD0O}Qy1Qcd&F9kPaAI>U5EyYk$8#Z}%7t~w~ z47IJ9qn)}gN&uYF6;`1eHCo6lqy#XX`sXe|Ki zAzgQUYRwX3g7uXyrd%QWf>WT6dq`X=cx;%SYvT9Iij~XM;FzjA=uL@znfV-qIuVc9 zI*w5kyGjcXR{>ATV6f*rQeqNbKx6>pq=mfUx$rQgcFgHqqP5>{*hDfLDl`QZqq+4f8e>O0gyw%Lt;$@?}6~sR~sR0t6X*h6^PUPG1>QDg+ zpMTuyHUPTyDFu%^QzTHILdhu{dw8cbhu4WRRcQ5UnthH1vyJv|#XZlAtA-AAde%lj zSu;#uuA%z7uXnmlw~o(xyK007u+IVy1W!KIJ5o2sf)}<-{x!E?HJi1&#*Nq`6^lMmS1Qw(Z`0lA76H+5-TkFI3mysS;t9xI;DHgR6xpz`Nf#dL2I=kQ{FHBU=;M8Qh* zL39tTmynhU1GhA8D^9CgJ?1PfNeF&wq3%GJQ>;m_8#|NmltZtPpxkMJRc>f%@9JWA zHy!PKC^dj?S3BHq;Fp`!36vQM)=#)lf2N@mra+*c6u;bvjB>;Ata8I)uX!7VLdf4R zYzb`EfEG&gL@7RVb%}j?(glu7LqBu`S)CSM4~qYg?R?XBGcT1rFyc@s@%Aj#v4&1E z@M=Lnp_ipDUNP(B?`l`=iRim0=`eSreU?EzDZHbwO>E)+^Z8GpuV%FQY-+oifP2{b z4X$pa+4tMYsst;?XPJJvJ|M0(=h#H$JL6ix!xEN;cpT4CFa%k+x_CK%ztZOS;>1j7 zDgAIr_~f(3;U4YHOZz7<3kOIBD;6}DZ<-{f73{AU9s$D^`bl$@iKVf4>Oi>U##|L1X-u?vX*WPq}o)LyTtnU|sOuFb8d z;1z>nFtUe5=mcwJ))?RRR!`@w7ngxxy5H`<9|PuH_@h}R;)3*awEC7EHpg&4dyI8r zMs>e9_7LTsCcZ2qL^n)B@YZ`2v#2|*I6TUVq;xy~^70B2dkJ)A?k+L;*D$NWsuAaS zL38PGz`P6EZ4;6p1s=8K40FtLfd`EncS0vq8#f{~y)Ja=PGAl`m{q3vj=TSr6CWZ^ zEpJaeY)%V7cv(m;=c@5z0SnzBP>00XU0~&mz7Sqplfn0cCEouIX!jh5)aiC1No)0d z=BWy=5>*>(;!<&D-z~`_#^~VJb$9(aaR5G9@$<69UazUF!hWYi{)3uH9IYN-!!>j$W4GGOa-)<)Gvg z^Nx?~3+aCAJ>48Bj2U*X)`fKXFx}Jt6j+t7iBBmsH%2{^OGtU$cZ(k!BsO&R#L@ro+h9aa;e zW%##m%1Facc;-Sghg~@}zG>rT8uK^2R3Vy+9HAlFGR$~d)_%NZAuUpG!j`7&kpD(+ zwfaM!pg+Z#bhp|0ov~0BQoXbQQ0A3{SrEMy_|ZbKE~)%OKR<9Ak5Cw0T6h$4;hl8X z@!LBBMz#Cg3)-4o!fa+0V$(#&Eqhr#t&s*8bJC8xsm06ai&uQUD7X7vo|gcdm_kyg zRd(mh8ICD&JU9vy+<*TdzWAlM^6W|qImNMUbTpf^h%QLCP9dpAC>H~Li!m?iWOG{{4sH^B&SSLt;CT(v`D>b{ruh@-=w>>3(wV^<&g>ZluK1S++4i$ zGfd6$%dm>*s*h>Qocodc1J76u@~7HChE=8MVFkv1lsrTv29Eh)%WDztBxY6& z$8N13PI=FCR2++6iTjhRrX95fS56ikhxhThp9!C=7GQMX7z)?e4o~|U;c5^TG|cYl zO?ZPYASK0@VYTeJQp&Cd8qfLz3Sw$QX;Vb3uO3H;h7;YGAi3Uh2~BBDu#8=-mTTD% zcS;o6a@@8OKRWbF=m;N+{*pkHUoqW~50)-;oe`rk<+KMD*LHk2Cn>Jflo31#yZKX5 zyI0`AmOfO`d)`K*BvdC=fHNE$sdat%eu7dPp8X!oM_)5^S}jE^z4H6J!9<Sj-eT}B&1^qI91fB4n z7o6SB%Hh40O|ph5t>rn`CAufaxl7*aKj{xPk1UdoIAPFk)ra!~z$lryzKcRN!JgWw z>79JVbM4#bv*3DdiD>?4RwK;pPC49o*|Zi`Xh6SLbXMSIV9WYnq>(#eH}c|3p!9uA z2Ylm0qT{Kno-~%E>|A@=jTSx>QwvK&zU50zP+SQ_P``1cW)P5#Qsu+ab_oN7YVifD zpV60!PL5*y+u_E6?Zr7}SI3YyKI^un7%ZRVST^bX@T3J>zc|O!t%AA_hoZZIJuBkM z(roehbEifr%hD5}NWBj1EfL`LN8h^wJBck&L4rnY;0Gt_9@1kl+LiON4v+8(NbvHB z(w$D{9T}Y=Y7^|796iuUj0Y~t0J_X}R^VASS-1naW9$OBlS%(Yahp@OQ?>CA<<7DA zd33ndWMSh}@OvqTq6%6%`oIy5kqSZYTA3lR_-TU?U7l0DG5Qn@K)x#QVNMuJgD_^% z>&!-)gXn#FPFf6@8qM>{TK#u02Gi zQ}ZJzx;25^DNp<9w~3GOkE~KQQ0t4lQQ|K{O7+|;8$U{u<07q+>kv4cB%s@NqM{J>}1e;!Be@JTDAAFEx`-qQMZ zV(Zu?LK}}*4oee-=ZcSv=Rjm28KOD@eE&$&8vT05DpC}XWO#>18%+oVU)i?Hl_)B* z{Eb>f{&AvsrNU#E3w9(8joUlmU7iye6Ic~mp1}il3PWo{6F z-|bdLQYM~^A!|dSF0Ly&UCJwF7Xc8><#kB~SpuLo{l-M}OS8l}laI&j9Ca0DvfuRf zniaD{Z~RK)_RHn;gN08QWEL_&`u8E$SB2M%Q*T+TUCxkb*G1Cd{U$}q2A||`)|wq< zdH}jid*#*zsB+Ifwkqq*CWn*-S(%Ss(T8qILz@@Cwb3!xI``V7cU6M4TSM9ouX{?a_)AIIi zlB|7|)x^$uEKzPXEsV48P*O&S%|z?Hjtgt(E;~_nI6mN_;s45!+dQNq){cA?>6(e@y+P5lN}Wv zv>nXXrDrC0#wOy5m^IaYbu7}C%?`oOf>!5zqEy(+bs!w9R zggc~bP6mCqkr_$;9l4`KW~p~A5;#0@Y+nb%jTX1Oq8v0{Zs8DnA_!L=ZWHr8t+Dvi zXRVGlhV=weqr=OU_UCfet{}PcI>V8ZL8Fn*#D z_FT1Aqb6dmNv%AL!2yjeACZm35o_A-Z#sTUS*#C{IJw3aB678Tgm+g7sntI6g{t$_ zk$e>q#?rryYp!3bL&p9+@`|c65p>OJQf2*`NZUXKSnsh&jX*j3p6*DcX~p(_ zBcjG?`Y;`Wk}^#0U@XczD?G&Nd`K7Vv6GH8EA^d95NvLCB=x;-Z%m9ZUTX zpq0RrIA+b74AQP_Qb~*K0`XO-45*yrK)Z%jzQ-$zD^e07H>nnQn(j#R{c6szSM>>}%n)dx0Y4{;& zoPNeZd$IQm&?GgIp;SJiN4qlT2n$4{vo-^8Vcq`^0^D}j|AWBM_V+$#*Fd$~PG^H_qjfj>lk)6ZPw|TJ`Fdfi?G+{WP2P14 zpBoXo7eoi2dRyjNkUiK&KkXSX=6v-T=;6IV-^xSsf4*Iu`vCzeP3{=vlEn*V_Gt|W z@2`u8*7QB6e!czuKTnH~M@!YXwu_-AKNDQmx-uhRHy}{P z_{U-IuVm-NY$MW$M0%zf{zW><5PUH8LXQ^_9`kNC)1aPXrb8lK&(fpg32&+>&LJcS z1F$VMV*YmfU~lc-b@a`#v9;~H)qZ1yR=d(anD((n?1w@@rJ(D}P}a!tX;r~#k(Jf( b;1*P&e5JIod6)5ig`+l#2M)OVo>Kfj<&qa6 diff --git a/docs/IntroLean.html b/docs/IntroLean.html index 905af4e..37d4391 100644 --- a/docs/IntroLean.html +++ b/docs/IntroLean.html @@ -291,7 +291,7 @@

Term Mode

Even though this example is a triviality, there are some things to be learned from it. First of all, although we have been describing the letter h as an identifier for the hypothesis P, this example illustrates that Lean also considers h to be a proof of P. In general, when we see h : P in a Lean proof, where P is a proposition, we can think of it as meaning, not just that h is an identifier for the statement P, but also that h is a proof of P.

We can learn something else from this example by changing it slightly. If you change the final h to a different letter—say, f—you will see that Lean puts a red squiggly line under the f, like this:

theorem extremely_easy (P : Prop) (h : P) : P := **f::
-

This indicates that Lean has detected an error in the proof. Lean always indicates errors by putting a red squiggle under the offending text. Lean also puts a message in the Lean Infoview pane explaining what the error is. (If you don’t see the Infoview pane, choose “Command Palette …” in the “View” menu, and then type “Lean” in the text box that appears. You will see a list of commands that start with “Lean”. Click on “Lean 4: Infoview: Toggle” to make the Infoview pane appear.) In this case, the message is unknown identifier 'f'. The message is introduced by a heading, in red, that identifies the file, the line number, and the character position on that line where the error appears. If you change f back to h, the red squiggle and error message go away.

+

This indicates that Lean has detected an error in the proof. Lean always indicates errors by putting a red squiggle under the offending text. Lean also puts a message in the Lean Infoview pane explaining what the error is. (If you don’t see the Infoview pane on the right side of the window, click on the “\(\forall\)” icon near the top of the window and select “Infoview: Toggle Infoview” from the popup menu to make the Infoview pane appear.) In this case, the message is unknown identifier 'f'. The message is introduced by a heading, in red, that identifies the file, the line number, and the character position on that line where the error appears. If you change f back to h, the red squiggle and error message go away.

Let’s try a slightly less trivial example. You can type the next theorem below the previous one, leaving a blank line between them to keep them visually separate. To type the → symbol in the next example, type \to and then hit either the space bar or the tab key; when you type either space or tab, the \to will change to →. Alternatively, you can type \r (short for “right arrow”) or \imp (short for “implies”), again followed by either space or tab. Or, you can type ->, and Lean will interpret it as →. (There is a list in the appendix showing how to type all of the symbols used in this book.)

theorem very_easy
     (P Q : Prop) (h1 : P → Q) (h2 : P) : Q := h1 h2
diff --git a/docs/search.json b/docs/search.json index 141d2de..7a1bea3 100644 --- a/docs/search.json +++ b/docs/search.json @@ -88,7 +88,7 @@ "href": "IntroLean.html#term-mode", "title": "Introduction to Lean", "section": "Term Mode", - "text": "Term Mode\nNow that you have seen an example of a proof in Lean, it is time for you to write your first proof. Lean has two modes for writing proofs, called term mode and tactic mode. The example above was written in tactic mode, and that is the mode we will use for most proofs in this book. But before we study the construction of proofs in tactic mode, it will be helpful to learn a bit about term mode. Term mode is best for simple proofs, so we begin with a few very short proofs.\nIf you have not yet installed Lean on your computer, go back and follow the instructions for installing it now. Then in VS Code, open the folder containing the HTPI Lean Package that you downloaded, and click on the file Blank.lean. The file starts with the line import HTPILib.HTPIDefs. Click on the blank line at the end of the file; this is where you will be typing your first proofs.\nNow type in the following theorem and proof:\ntheorem extremely_easy (P : Prop) (h : P) : P := h\nThis theorem and proof are so short we have put everything on one line. In this theorem, the letter P is used to stand for a proposition. The theorem has one hypothesis, P, which has been given the identifier h, and the conclusion of the theorem is also P. The notation := indicates that what follows will be a proof in term mode.\nOf course, the proof of the theorem is extremely easy: to prove P, we just have to point out that it is given as the hypothesis h. And so the proof in Lean consists of just one letter: h.\nEven though this example is a triviality, there are some things to be learned from it. First of all, although we have been describing the letter h as an identifier for the hypothesis P, this example illustrates that Lean also considers h to be a proof of P. In general, when we see h : P in a Lean proof, where P is a proposition, we can think of it as meaning, not just that h is an identifier for the statement P, but also that h is a proof of P.\nWe can learn something else from this example by changing it slightly. If you change the final h to a different letter—say, f—you will see that Lean puts a red squiggly line under the f, like this:\ntheorem extremely_easy (P : Prop) (h : P) : P := **f::\nThis indicates that Lean has detected an error in the proof. Lean always indicates errors by putting a red squiggle under the offending text. Lean also puts a message in the Lean Infoview pane explaining what the error is. (If you don’t see the Infoview pane, choose “Command Palette …” in the “View” menu, and then type “Lean” in the text box that appears. You will see a list of commands that start with “Lean”. Click on “Lean 4: Infoview: Toggle” to make the Infoview pane appear.) In this case, the message is unknown identifier 'f'. The message is introduced by a heading, in red, that identifies the file, the line number, and the character position on that line where the error appears. If you change f back to h, the red squiggle and error message go away.\nLet’s try a slightly less trivial example. You can type the next theorem below the previous one, leaving a blank line between them to keep them visually separate. To type the → symbol in the next example, type \\to and then hit either the space bar or the tab key; when you type either space or tab, the \\to will change to →. Alternatively, you can type \\r (short for “right arrow”) or \\imp (short for “implies”), again followed by either space or tab. Or, you can type ->, and Lean will interpret it as →. (There is a list in the appendix showing how to type all of the symbols used in this book.)\ntheorem very_easy\n (P Q : Prop) (h1 : P → Q) (h2 : P) : Q := h1 h2\nIndenting the second line is not necessary, but it is traditional. When stating a theorem, we will generally indent all lines after the first with two tabs in VS Code. Once you indent a line, VS Code will maintain that same indenting in subsequent lines until you delete tabs at the beginning of a line to reduce or eliminate indenting.\nThis time there are two hypotheses, h1 : P → Q and h2 : P. As explained in Section 3.2 of HTPI, the conclusion Q follows from these hypotheses by the logical rule modus ponens. To use modus ponens to complete this proof in term mode, we simply write the identifiers of the two hypotheses—which, as we have just seen, can also be thought of as proofs of the two hypotheses—one after the other, with a space between them. It is important to write the proof of the conditional hypothesis first, so the proof is written h1 h2; if you try writing this proof as h2 h1, you will get a red squiggle. In general, if a is a proof of any conditional statement X → Y, and b is a proof of the antecedent X, then a b is a proof of the consequent Y. The proofs a and b need not be simply identifiers; any proofs of a conditional statement and its antecedent can be combined in this way.\nWe’ll try one more proof in term mode:\ntheorem easy (P Q R : Prop) (h1 : P → Q)\n (h2 : Q → R) (h3 : P) : R :=\nNote that in the statement of the theorem, you can break the lines however you please; this time we have put the declaration of P, Q, and R and the first hypothesis on the first line and the other two hypotheses on the second line. How can we prove the conclusion R? Well, we have h2 : Q → R, so if we could prove Q then we could use modus ponens to reach the desired conclusion. In other words, h2 _ will be a proof of R, if we can fill in the blank with a proof of Q. Can we prove Q? Yes, Q follows from P → Q and P by modus ponens, so h1 h3 is a proof of Q. Filling in the blank, we conclude that h2 (h1 h3) is a proof of R. Type it in, and you’ll see that Lean will accept it. Note that the parentheses are important; if you write h2 h1 h3 then Lean will interpret it as (h2 h1) h3, which doesn’t make sense, and you’ll get an error." + "text": "Term Mode\nNow that you have seen an example of a proof in Lean, it is time for you to write your first proof. Lean has two modes for writing proofs, called term mode and tactic mode. The example above was written in tactic mode, and that is the mode we will use for most proofs in this book. But before we study the construction of proofs in tactic mode, it will be helpful to learn a bit about term mode. Term mode is best for simple proofs, so we begin with a few very short proofs.\nIf you have not yet installed Lean on your computer, go back and follow the instructions for installing it now. Then in VS Code, open the folder containing the HTPI Lean Package that you downloaded, and click on the file Blank.lean. The file starts with the line import HTPILib.HTPIDefs. Click on the blank line at the end of the file; this is where you will be typing your first proofs.\nNow type in the following theorem and proof:\ntheorem extremely_easy (P : Prop) (h : P) : P := h\nThis theorem and proof are so short we have put everything on one line. In this theorem, the letter P is used to stand for a proposition. The theorem has one hypothesis, P, which has been given the identifier h, and the conclusion of the theorem is also P. The notation := indicates that what follows will be a proof in term mode.\nOf course, the proof of the theorem is extremely easy: to prove P, we just have to point out that it is given as the hypothesis h. And so the proof in Lean consists of just one letter: h.\nEven though this example is a triviality, there are some things to be learned from it. First of all, although we have been describing the letter h as an identifier for the hypothesis P, this example illustrates that Lean also considers h to be a proof of P. In general, when we see h : P in a Lean proof, where P is a proposition, we can think of it as meaning, not just that h is an identifier for the statement P, but also that h is a proof of P.\nWe can learn something else from this example by changing it slightly. If you change the final h to a different letter—say, f—you will see that Lean puts a red squiggly line under the f, like this:\ntheorem extremely_easy (P : Prop) (h : P) : P := **f::\nThis indicates that Lean has detected an error in the proof. Lean always indicates errors by putting a red squiggle under the offending text. Lean also puts a message in the Lean Infoview pane explaining what the error is. (If you don’t see the Infoview pane on the right side of the window, click on the “\\(\\forall\\)” icon near the top of the window and select “Infoview: Toggle Infoview” from the popup menu to make the Infoview pane appear.) In this case, the message is unknown identifier 'f'. The message is introduced by a heading, in red, that identifies the file, the line number, and the character position on that line where the error appears. If you change f back to h, the red squiggle and error message go away.\nLet’s try a slightly less trivial example. You can type the next theorem below the previous one, leaving a blank line between them to keep them visually separate. To type the → symbol in the next example, type \\to and then hit either the space bar or the tab key; when you type either space or tab, the \\to will change to →. Alternatively, you can type \\r (short for “right arrow”) or \\imp (short for “implies”), again followed by either space or tab. Or, you can type ->, and Lean will interpret it as →. (There is a list in the appendix showing how to type all of the symbols used in this book.)\ntheorem very_easy\n (P Q : Prop) (h1 : P → Q) (h2 : P) : Q := h1 h2\nIndenting the second line is not necessary, but it is traditional. When stating a theorem, we will generally indent all lines after the first with two tabs in VS Code. Once you indent a line, VS Code will maintain that same indenting in subsequent lines until you delete tabs at the beginning of a line to reduce or eliminate indenting.\nThis time there are two hypotheses, h1 : P → Q and h2 : P. As explained in Section 3.2 of HTPI, the conclusion Q follows from these hypotheses by the logical rule modus ponens. To use modus ponens to complete this proof in term mode, we simply write the identifiers of the two hypotheses—which, as we have just seen, can also be thought of as proofs of the two hypotheses—one after the other, with a space between them. It is important to write the proof of the conditional hypothesis first, so the proof is written h1 h2; if you try writing this proof as h2 h1, you will get a red squiggle. In general, if a is a proof of any conditional statement X → Y, and b is a proof of the antecedent X, then a b is a proof of the consequent Y. The proofs a and b need not be simply identifiers; any proofs of a conditional statement and its antecedent can be combined in this way.\nWe’ll try one more proof in term mode:\ntheorem easy (P Q R : Prop) (h1 : P → Q)\n (h2 : Q → R) (h3 : P) : R :=\nNote that in the statement of the theorem, you can break the lines however you please; this time we have put the declaration of P, Q, and R and the first hypothesis on the first line and the other two hypotheses on the second line. How can we prove the conclusion R? Well, we have h2 : Q → R, so if we could prove Q then we could use modus ponens to reach the desired conclusion. In other words, h2 _ will be a proof of R, if we can fill in the blank with a proof of Q. Can we prove Q? Yes, Q follows from P → Q and P by modus ponens, so h1 h3 is a proof of Q. Filling in the blank, we conclude that h2 (h1 h3) is a proof of R. Type it in, and you’ll see that Lean will accept it. Note that the parentheses are important; if you write h2 h1 h3 then Lean will interpret it as (h2 h1) h3, which doesn’t make sense, and you’ll get an error." }, { "objectID": "IntroLean.html#tactic-mode",