From 01b09a1cebd263cc3b678494fb26ad35ba17fa2c Mon Sep 17 00:00:00 2001 From: djvelleman <110697570+djvelleman@users.noreply.github.com> Date: Sat, 30 Nov 2024 16:33:45 -0500 Subject: [PATCH] Improve introduction of tactics --- IntroLean.qmd | 2 +- docs/How-To-Prove-It-With-Lean.pdf | Bin 2295471 -> 2295536 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 7d1fc19..1e98a2e 100644 --- a/IntroLean.qmd +++ b/IntroLean.qmd @@ -211,7 +211,7 @@ No goals Congratulations! You've written your first proof in tactic mode. If you move your cursor around in the proof, you will see that Lean always displays in the Infoview the tactic state at the point in the proof where the cursor is located. Try clicking on different lines of the proof to see how the tactic state changes over the course of the proof. If you want to try another example, you could try typing in the first example in this chapter. You will learn the most from this book if you continue to type the examples into Lean and see for yourself how the tactic state gets updated as the proof is written. -We have now seen four tactics: `contrapos`, `assume`, `have`, and `show`. If the goal is a conditional statement, the `contrapos` tactic replaces it with its contrapositive. If `h` is a given that is a conditional statement, then `contrapos at h` will replace `h` with its contrapositive. If the goal is a conditional statement `P → Q`, you can use the `assume` tactic to assume the antecedent `P`, and Lean will set the goal to be the consequent `Q`. You can use the `have` tactic to make an inference from your givens, as long as you can justify the inference with a proof. The `show` tactic is similar, but it is used to infer the goal, thus completing the proof. And we have learned how to use one rule of inference in term mode: modus ponens. In the rest of this book we will learn about other tactics and other term-mode rules. +In each step of a tactic-mode proof, we invoke a *tactic*. In the proofs above, we have used four tactics: `contrapos`, `assume`, `have`, and `show`. If the goal is a conditional statement, the `contrapos` tactic replaces it with its contrapositive. If `h` is a given that is a conditional statement, then `contrapos at h` will replace `h` with its contrapositive. If the goal is a conditional statement `P → Q`, you can use the `assume` tactic to assume the antecedent `P`, and Lean will set the goal to be the consequent `Q`. You can use the `have` tactic to make an inference from your givens, as long as you can justify the inference with a proof. The `show` tactic is similar, but it is used to infer the goal, thus completing the proof. And we have learned how to use one rule of inference in term mode: modus ponens. In the rest of this book we will learn about other tactics and other term-mode rules. Before continuing, it might be useful to summarize how you type statements into Lean. We have already told you how to type the symbols `→` and `¬`, but you will want to know how to type all of the logical connectives. In each case, the command to produce the symbol must be followed by space or tab, but there is also a plain text alternative: diff --git a/docs/How-To-Prove-It-With-Lean.pdf b/docs/How-To-Prove-It-With-Lean.pdf index 65424c347384ac701af0695836a8b69b506f7579..f58159445d65ea1bb2d37ea1c99b161eb9fbd6fa 100644 GIT binary patch delta 28729 zcmZ6yQGP5ow z8tC>Pzk`8-frCMUL4(19!Gj@!A%mfUp@U(9VT0j<;e!!^5rdJMk;dN4Qe4q-}TC8jBFzV&ES6OpLIaz^*tx_JQzvdU~Cbp=1P~eh@*h%%i62 zPt5ngCZ%Pa>86bA!{gZtbrgQeuM&B{y9RFF-(bCdVFChI{6CLJk5g^y+0E;T((jK) z-t%+z;~6NcQ`CTW=eIq85>?gR$vqVD_ch8lWl8q;<1ZkH-AE9OPu{dJ^m`HQTf^uI znfu54Dew~5>A4x!lM#lUyzkE=#G#@Y1BEQ9xtwpWd2f&_d4zRaBnW>ltgfNmjlP+( z-duhRiajrnE80W+3%gtud)k* zygb&#p9O*ULDx?JVk@c%YlaRdLpb33ev9`WXTM|3RB55bIg15fZk(ZvJ-y@m0m`j6 zLFqZ2{hI-CtTc#g4@<(NleO4Oy)@7NttM0T_n*JRgjdl|SAB`O0Zwgz&HEn`14NTW<^~+|r>uW5TR$2Wt56S!hzI-CD#p!_g;|^by_0Z=H znH-}7vyf@MNV#?2Y{}uAa9LsuCr^ls^%D?a5Z&T|UWnAW^0N2G-TC8tNgyySYV3VA z#(d@wEU@=Ax74}koSbIviZ5$(djmLVtiWn?#KX_DC*NV>nW3xc8zcnG)nt4t4a1m5 z`fixqZD4Q!5<t^SFI}s!2DF^>(}Xq(BQH=hi?c$EI{6P} z$e#Fi&@+fR)tSJxb`O$%fc$8~Z!J**Bk4y^RBK!@NWI+CkxCjo3Ern0?mMFgZrNR_ zw?}0+0YRWpXB^CxXF}#`FK>o(^s6QrpZ0JbT!L&s>8)DkeLDNNfG`=jDbcz$kCI@9 z@^XBfBGsAVG$!iwBL~Z|@_FMMq(_ws{j8s5t5Jo>!O04g z-?uto?F2#G$n>Bl`fN^6+~gYKY&>6}Q6>5MpbRpOEF_*wiDTK=VRMX=$_c z2zMA@Bm%zwWZp>E9!4h&e#_F@X_($HmB(CX=~K89Lk{b+PPc|*g}~pYf6Pa2sBd-P zN9$y!=yEKgHA9Uj@^Ryf`z$np8HY4DLRhMkQ?~J8xyQ{T(^)*UCadT#v&Q%>y?RW_ zOzYfS%CaW-3Xq9yUA;d@a2nO}5R`~kAN&L0)6m*|Oi^k65vu$V!NN8S41LS^%0X$~ z5hG+18Z@y|)it-o0Zj{%(hUe5!cdnrneqV3Ad-DeWdW45JDoJOLZbh)a5u?cXtriR z06wTatv>ns!!dYuupVj;F4{hpKA?F%mT=tIquwiQ{*>)TR0Uho%#;+5@>6P{xWoXW zdS4=m{byRy4jvFk*E{!Z9#nKo>iBhbmCHpHo(=74Il(D!S#SgMBK@Y(q;2eS_oAL^ z9Ua|$oT+U1YL1jF#E@8*L&$GUcz#*DaD##HzR>m^YFiIa4#^r-^Ou6)-6;{&u@ zwVvy%?B(Ar4t+Z4F;X0SKDsy{OF@H;E@cvF6DB@dCWmW>#ytED4 zA>8tlo~#liKhTfnxMajpfsRc~gD`}=z@sYF&&F*eTcCBKI6Fq=Lo1l1WZ>(agDIpI z6J3-9apDQI9=&sGu*c%F&Rgb;X4o55+rT}_?3MW3x9^Zli?%7@Lw>J` zs?FgWf>>BJr_*mY-Q5^I6-)ufr1uKZT3cvWwel5d5p|%}fRi?$hbamSgGpHits?dd zQpj8kFB)Aqc#CJ&Hfef=SKv}fiigB3NMb3GIY$$q!EH_IM*632_Og_Da zvF&-5S-EXcq?n(QQo+JMt~Uh^dR(y0PF8b(z(6?4nJ_=B-2R#FUA| zS*3yVi{Ae7xrDcEIi4n{`&Zbc)o$g2%`KZeeC%~F+lJpKcRDw5U@<*B3P z#`~VWQ_`QR6O?TMU0Ar4gwc*##pGKi0A&O<7yuDk4GFsMgI&B7lpwKx`G&QkI{X=| z=Xkg$Q3$3OHHZpC!FK6F8&z-sBRY?VmgasME!DAe9vCY7s|-MZy*Rwth{rzdI0?V6 zV@k+(iHnLcK#SLXb>CdXSiHNHh}CK1UCv~CY%_GinxeO2k<__rtg&jxo`_=8;a86( zVDdfT;e{}ukaNlM8+{{RyJNAv#agiX`K|~bIJ_MEGh5|%+>*0dMjCJUNrN1f%Y6a; z!PZT9w&nO3PcgtvT{*TlV^i#8(zMWGnzHGwSfE_;bnPHjvu2C$;%3qW;lk%z!Gdn8HQ$icy-ukC z!a|shT_dM=NM!qXI_wtH#S@xpd$9#=d)i^Hw2PT-?xxjjh;~DIh&Fb=imH@NTf2xg zEE6mshfP{ayJ)d`E_josTFJYcO&dQuxcag*?;66iVBzc6ee&`ld@EK8g-12UfMZrD zt0!1f`7~f`KolldCSaEs+0f=%d+HSY<^#OUa_*zcCm^9OV8Gu-M^gttKY8L7F&LiR z`9^j6jP~Afl#-DR4+qlFxcVw_JNaCd};!?5I1KkCH=D9<;s|pfTpRV#I#K6Wuo8(+b%5Shn zl~<=B^ihl=rXpGg?Xm(NcH*3S5}Br<=t|iH-n_Hi6|~C~ZPJEIwLaa1#PSX--G_`v zMi%gJXI^f}G|_UKN{Q{)1ogrODLBmB2i~XdFmN0YB~wx-o3q4eg#(=Dg!sRuQ-nY1;6UyqQbU+)5UaQbVnXXKS&;^Lv zm8jSUrE4t5d?3}P(!je@J7#76>DR)HSae4clGP)W!|E88LDR=H&YxB8!e(qVIZiYW zM?UXKYH@Yw-=y^kYdcKpxpUUKh5zu#Jm)HWmzpJ0=jObzo!>W|mxV4=n+l6@eHhQl zjt#wh4K@oKt@D&9iit;cxTn41UIdtdj+^R4jTA%u;n?eWUQ9Qq#H%{6qgp!5Supo| zIDUb)^p?p4S@&IdcB}ZkWd1zQq1o<07ox*Az-lRNeRVV;jmR;i!t1LzF>c%2%NQve zG)p9`f$-#0W07EuW$OHUec&&+P$~Y@RPIX2ubpuq{Z6#Nrb}MS4B2MG@MXX&Sr0R} zl@Z^Gn>XawQzIh7j^U-@3(nTu({OK7bU`IGs%)9A!;J7DN_#u*ON+*RWSpR9&>C7#nbZ(V_8d`0|Dfs~3xg_9^<(d84b}>%Buywo34|dOa zEB#>@Bju4@EnT=+AmDEFOcwwUY*@`w7DOjb_D-f_CjwqC_P9;X)*oOejm#qgjr$eB zHiyXx*Tg7CVv8x`!@kv4MB0a9VYlP>hy=fAQ&LCOFKcmV@=jkf1!g7#ps;{2GtqiS zZ;=rtg2R6BrZ?}W-V8Gw4x5hV(j4}ykZfH!y%VcWjFP`%En8Ik4?hW-5(`V4})XJbRxFgB{Wj?yzo?V$OQ5(6o4X?<~V=LIT{1q&DZsFF)**)eI zaMy{A-!%BA%~YNk2-Q@43F)oAobO4|XH2P=DR8#C;O`aG_>V-X?=6;@K<7YP=21}F zU`joYlCZNlf+rlMFt`9YT*my$stx1pz2h{8+Y?D0AFpq_^Gt>tb^b$d%_zX_WjfG7 zON$GpW&plCHNut;(zaLc+U|zyb1K=#>%ATP(#94Mjq(a>E6+jBYT54dc&KoRg1#TEt}Fn;KZPlQaZ4+tEosE4uo)O$+D6CD~$1KuCLc!)dhkNYFB8nWIXh8Ro-T=FV9NdT2) zV(N!?M><3MasqBu!9J&a8?a613tc@88&B3LtD+M__zU2!{nuYBHMJpU<=vzr(A{xF zC%*Q|!lAz@Sm6mtH^k;h38CnJ^0+7AVNmLWw$G~@eBg%SXU*Zn!ZL(6D^6EZEV8uF zc8~h#X$>5N(4y9G@Do7G#=O>)PkKA- zd;s2jzXyAN-I+$!r!`O`qo%EKBa;JIIoSSh3E!eQ6}!m}+w(&8349=lO19Q#2oIF` ztGi`YXKrwMT3&&#`33+fm4JNpG+inbWooD+fcn!DwZI!j};yP#kvVb-7?)>tH2O{~h#{g)ac2_^b5FL7Q36%h~ zFZ9LauCPb+B{l9PE6>yY`Qv8LoDN^JA(`EK_9cBY3$P?^h-IfCVqE6myL3n4?uwycIm zLrl}DqDe9z><73%gXwFY#7bM=|0m73+Dx>iX%kc?oFcwspW@2I%g?P?K5AAt21Yqd zwd9jjD3cajbk^JwxEm@xZn)Rx@#XLml`ARAPz09vE}<{YWgX6@LdT!M_CTAR&m3^~ z1vo@AP*wIeC-^?f(_iuq*REqxwA@7d*%!iC8K=Gzqku+DVJGncuh(WT$KPdBrPfj# zD>jXqi|eP)QAg36WfVEu6Z(OrSsNzx^{@Be%@bkn(yoeY(s-$GTUzr*ywKfg%~J5X zbeNy)i6%VXj9mA+i8Ama=WYkjS#yEyHTEdb3!v-T=9RFFN8+c0(2G zwOE2d^PDkQ1RNF4-U{T(N?$tgq;4SIL4i!GXxMEypViTAPl{zpji?Z_5V5K$qk3%i z?HY1JOD2fP!@_yvT)2w@C}W~zS#{+7oOyboH$VaL08g6|PqgN*{an_FFfA;|^w_}q zNi(9z^NYy?;VX&XF)pH;qeFwc(@4uPx&@X@jS@;hHl1fk?t4qNfp&R+_uSPb$%j-=vK>e8 zfdL*Sd2G279gMW$iL|&z^@HE>ledJy#Ew(bLT@^tnT@#6RtbF_g4Q%3l@$CM(AFc{@k0;0HSz=29h5(3ZCXMK zbcu26oh?uNG9{o};;kF)Y;2L}Xca6V?iH-`rh{>Ue9?Er5X`k&1)O6yi zT(4NLdE?N%(z>JCm~qPL+kBgf5*GzlzV@A=yMJf6V#S4x`(s6R5BEdcQS zWLMJ(M`ao_O!^mBqa*G?7h>K#@R4EoyBql&ZnR-_Vh$T|&!#{Y(dk>tv!hK0N6kK` z7#uw|-_L3W-&~!UYV_EuaK@l#;b@?7y4$spQ8GJ13D=#Tj&PvXG}c_)utta?=a7;( zy!RNqal zbYNd89kX`52G0(Y{FJ=HKovGVsTTNXH-BRBf%-3-wPe@F#xyz%Qvciyo~If#A-jY`t}*V$tZqN{_pQn**p_K&r;n z7|_lrQ)TQFTNAQLe;W0=DjPy4jTfCuS16R@<>=M$tWt)4a!OO)$P-A-DnLDwBtJ@~ zSmlpWuBI1qhm~-Ng@hMAyhd>wm3&ZW9Yc*q~o}R%6nUhi2XJ>Ny_Y$ zD0f@hu)2KruTz<5e`yTioFE`L#vLU0SD7py)b0@(k=)yLGg8LuU$T$N%L%-%^cw)) z!KIe`um7X+C}HY?$p1iTQx`;4W(F{`{$I7f(%rDfkwEs_slzlhXarhZSbEV11vj?H zfrP9Ny#hmLj0U4~G8;yfkeQeNeDRT2Nw92TXxwb3&xHtJIds)ns*ur8dy%v)WD@-3)~%ao!cLDAIq97L47 z{|#H!N|dZ<0>;K(z(MSfTMmp|!J|n1?SsIbK4V-y=*u1mir;ET>$$N8i)=WRAo`p$ zNP<1d#Y>$2cMnN=7q>L_^)Wqj222);h^Q!raG$FLA?HMO-Id>ny5C}0)sR}yHOec{ zuoAP&kWo!u4^W>j>=@?+H3=%4bEnv+%59|kcMW=2w{HR| zkwG&dls6)k8tXvk9)05Dii>UvMlTR-f!VVTx{=Aos;A8Kp!JzGnD7vMMO@ zEFNK;yl)zDDfk1GiS+CgVUF)5bM6e`fCSj9_+c1z!qLSjlHQf0KNlOA^dSkx-;QgL8tmVV;c1%(lOnG5{;y;U-98 z7)Q;8?f}dhp>t9NOu%-~YVl5j;K4BOpk3vH*B~Fkl?=s@&ww(2Ba%l!8QmrSKBk;S zAT1F+oD1D|!4)!z|BIC2E65O!5HDRyi&I8>pKv0Z!RN`IJtp>EbQ})KH}^?swd;{A zja*0B1hy(3Iax0u(!-ZC&=)|+$H@^5!aq0y=L#SX=wuZoou!0L!Oq_Ez(hJ-4Yh`= zXVY~O4NMN*hDQs){^ErWg3LzoOrU?l;X6~lVKNm*iIseGKIgCkf><;wq=$9Opfv$; z%fP*5T{I*15A6(=GX{0ba5hC842SjGqehY=v;t0W5uBezcQ%9#AOO)ImXbS>B?Vzx z6a^%1TJxJ=p0lC`(hQ3k_>+Cl-D$**ezGBHSnnXZ6?~F2wQBK;a0_#=Mr4K`M)spT zhn<9jjP7CVn?YOOih!Kn!cqxa{$;9(;3i4`H*7hrDI`QFjlXK+Xm@2-_XtVJw>IGd zu0~jMMsCqrxCwj!vhPRSbUHSm*wfMBIe;h_AyL6%!3AQGmYIVIC5CW;NSrW5ljt|tfPbO2c( z_n$$8uZ1>>h3}CeW6c)@{a($7>y@>AH2^>pUp{Sy6_1m8xq`}0|FJF6%Duegs7&Vw(-uaZ#7U-~Ny<1%?0=f9rc>xwF6({j%v;_~w zXljYojmK}@K7jsBgwVHoUuR~nbbvejA;Akm*bw%Pz+dC04vFL)-B)@CdPJFEjr<2o zE?nM>+PtSYfA3X+obQI~mpBTE1&FM;kF2;a741Bd9$S0%{U2Uly!X5w9#1YVErqll z8W(b6(E^QkSf~l?0#?-UWRVien9*86OLp2Gjpu0E(K$EY`^aNTQB)y5OMnt%-?FQo z7zef*aDG@I-h42s+Gqotp26Ic)W1^~Bxi3;NmpnYNt@1w!izuq+$hPLNIs_RF~t}bF4$ft%G4Tu;(BRW;SHkE}mjq6k+&D30IA#=o4mnAhf z)E%dt^og*3k~Cq-7+4&|(}0*UbtDkLxXY0mEn0jUO~SH~w6&3ua%KkwZfXGZS@(eT zrf$b^p>vMt5VmkQd-8>$%II4bO095lkeZbd*$J8pJVceS(qgtF8i`#fpO|^^xQgMG z8v9gGs4COE^BkM(0}@RF=c;WzdvmLW&s<~t5~U6`AxLR@o@mMj0{}{S$eh${s4$+H z3LRdulF-2=iCrySw5C>?AAG_XEj(M1Y$3ZoDY71tAIeKPBBC$?n#$y1sqLQZ@Gi0i zyixZE`N6TO(5VJ0Y`j!X3z-;2pBBkBi|{6TYNc3HX0m-!dQQmr*#~*Q1S%$HOwW~k zu-;Y+)g)oIxn37m0j!Of(w)qVLxzL`6g+V}$E?vHLR?4|<%yzdrEE&7SL&8{ z#DLxGnP_By76LpbUej!sH?E!_f|%UIV258FS*uDbU%M|w2RJusPZBZ9tygWt!qMb& z8|83=PNNT-sWdFEv~mF(xqIh^-gnuhiHn6Kx^$YIUB!uZq_q+GU@mk%>kAI+##4mt z;}~c$UI#iFuK>xWX>`E`MTO&ZqD>xz8auiywIr_d72(|u z!faSxP!ajYAhR-f%9E>NlO}4Ltx*_?R=(7Sg%LQ@A$IGa5dBEbm(tC{uUyiu*V7F;WDmxG_2D6O!N z%WyEVGieymFSnmQ&#BWrX8jF}=xHC>k3T;B2hcvhaXUJ9kdhb<&Pzn6fwa9BMAt1c z;}4m{WTrM2qYevReS+adEh%2B z{G%_AUWH{cYU|Y8hX1U7F}Cm6$h%46VDSgCrZpQDj(kE@M8tl^Xd$ufLZZ_6!GiUu7KJ?&V zC2H;csss3==b2IN*WX1@b{1aeo!h8!Vuu)>=~r#p92<66?0o?9>o3inVHt(*jjLh8hY5!39 zet*qi^ajv}-VoS?j@^%bJ8_A4!5{}-{Ee~@`@&eunDZE#=8r+2`P->-;mk|r1E^UJ zN%v;Pb?$$=SQ@Bi(f7jV5@j=&L7Q%(3vV11ty@&>B<<=&n9!i1HglVfJVv6D zb)+&TvQU`2Chl!7Eets+yeffCx2rm!bg@evmNn+eskU$^opcKwvQA2xf-j9)a$V~6 z>}tz=lt1gSP9o-z<<%jP9FQKi1Q`D@Uv77qRO!O!!cZ7)oHc6O#Cd+s-1sD0%TkCV zcR98>!9uk5$a3b2J5=a;PmQQ?qb_3t=_ILok%(V~N8iDu)+ucS8?dBHYfil{lxb%w z`{n<3!&uGa-Rai8j9mqM*rr62HjdOX8f%7Z*5bRhEPkv5SxbYIc0=JM3efB+7@E3I z?xklSH#sw%K{p>r)A-iS^)waiay7AgCID0e{2Ozt%MP1YH$Eb~3ny%}%NCL` zTI3DhC}B)`1{-!=9QoohHxT`()pb<}zWn%^b^54|UARYikbA-GVwOLhe5VU9F*zC9)SNO9 zy-#$AJ^t-pEB7BnPGeHlPhvM-qbpwErMu>S_3|Fz+ucU#dS0?d1IRg3r`lL%cwX-3 zBI-;7Zz^_%&x^F=Ikk^4F(o$bEl;d39{bXlqt!jPx|T=+yQrn??|57}s7LVka7=c? zH>R|B#5XfTI}oyI@od^#xt_xJ!uK>cwid}(mirGC!iL{_Rii(s4Ib5JTm51cW7iJb zTR4b0i8=S#_u1M15D)+6;Jyyu_|Ny$qxv48;UNJk@C`8RNfBB2fdGrp;7tpVMnwsm z1fc!{?H}m>!1xE|Kd}CR{STaf;Qj;eANcHeQ+=ph2)=$u#&qFdml)Dy#T4MK zlEC@HHkkpOf=CwNstj!`_xN-4dN$KPGw4h7*pDM$kFe%W`wm!+W; zIqvw1`pV%V%_DN?So`r7JY3qpV7+2qqwnEQVzOK>T9%I5nxfZQa%Sh~RGt8TBMgs7 z*WPK^hyp9sR|ACiCDP-IPxwez_+g&D`s;6xJ&(C9_%4fp&hB{r27_Mf*SD0Um+y&% zxNE}Ad>$5#wtjMg&C3f&h;HTLbGQ%f)3e zA`0GoLKC!As`q1F#-NIgV<;Ef>#(i0Y5>beHUo){68-e-a%_ntAfNTGKJc3Ow5~b4 z$nll0z4Xu__$!`tR(Jz!Zv4)c#thEM=OZf5oe`mbj#^F&*N$6Gd(buN%tv;*w(9co zdjH@@0**@$PTW59`FinO?9`5CMDYo7G$L;OeLOe80b3j=>U8J{%1s0Zf7=QGmX-3>J+H30H%V;GxQOEm5V!Zq^Eu$kA zSZ}58H(hS9JUJ5rVgex-Pnh^475d=oppC*C%z_bc$)uv>@kGj&LmVJXWoX9oO@XG< zaLp#V&_~fh(Z@RA30u$!TYm&oC3#~=lutv_D2#~M0G&bQwP?n0;AyZItYP)7!kRem zxk_73f`rSv!HhDa@kXg*oRiszY!jRJT9;|KJa#pwZ`^#g^mzI90jXal}CP_R95;H>V*P6UhLSY=RgO zM|QqYUsjnShg%y1{-xyIPInzU0YO=LjB=^)_gM#lBuN7I_`aKKz}|f?BSVyOB+!6E zk!A=8tFUuWH#VF|c>@|VA(LZ&XvXFgcV!TxfRbM+p0MX;P8@+iU0zw#c{%Cbec+X6 znYmXNz9cX%PF)W_t1z#NmMS35zppkqCXf~G*Fc5bV~|&$@q}6o1N(~^CpM9e=H~sl zS*6kik2@tqcp$CI43Yr83a*bF7B;mG?7U?p?EE0A*6+lhs-)4jCAg20;c+Scu_8*M zj1tcq%Wn7PNI$y+OTLA!vJ?$_zV0{eYpaurTUF0>o^?;NODZnTby8ycRWE9u)~63E z4xE?_{+rZ&+ZK4ph?#Dy61y}W0Nqj4$$#bvEiLgCpA5jx%Je@AB1Oq&Ul289=L^m2 zvJq8|oTZ2`P#mmai@s&+1ye$!oJrL0w0Fm}M+62(@zwlzn(t(K%2d-fHS66~CbV}$ zrUkC;(6RExu3i7y4lPlSGxuC5lk7vq4Q1%(T$eq_=uVftcicrXRN-PNZ)su%Pd&ie;rgR`-lV@iTE>^(Iayh&@5UQFL@EzCwmy@2k*1XEUGi$$jN z;yMFPxckS!KM|#sM-?#9YLH70=sYS?%AF=gOUSmwqH;-SL}CqN-e(>~q{w8kAY|r5 z!isiR3I*0iN)xf!Cro0tAZp}6TARXbyo`W22p z-Mu2zdC3-PY!EaN0tw&wd_IM6I>IrTfe@DqDb|@f{a`fWP-yK)=r7kHz;o2;P?VEd zIkYJHp^5VxoMdk_!qK$+&yW%ZB9w%FF-xH|x&+o6Ek1LzCa>mI1O$UJ0~HT99pCBf znb>Kwr{n1(u^YmZ>nUq?vq)KiLAGn+Ou@oDL+te(u_}(4U`qnJs!r#$k{3hay*k!m z_@#cVsB^G9g9Nc!?zy)bKtGs7riL%}Pq==gYtBd>#@W^G=cn$?+)CG>PuztV;HSLk z>)t0uTz!Yc^|Ww@O@>0X^z^~vYY7?Zg@%`|Vx9Loxzt3R+Y*UtssK2$MFE3SugN)L zP|O!%zQxE4=qUb}mNgWYH6pFje&*Zzsu#u}FXVi?b&Cv70RQeC<;LM$1+S-vVXEY; zX#a*lt;|jRztO2{PDJtl7wawSCPBo|neIqFTdJX*Eh{3(3UWf_NcA*t>J)y~_50tw9PdT>awENoeK zSR7|%wFydn?(@*NB`1%UvGvP^fowCD;%ljWh}S=Bs)#bmMInR&Oj=nHSbLBetRJAj z)X$(7B(3mJPzLwOJd5t1&pMm~O4e?o+^#}6fVTj1-*7||ZqmpM?DUL*XaQk{{{1>eNTv!a54Uw9d+>%H(Moa&KV}7_z6Wj5nFqoko_gNv6>2O>5ONYq*Mu zwM^QzH4U-^H^(pxi4w_jO{X3f2KySJPap3d?1?T%Hxm99d84x<1GV6~wS>W&DjzK(t5tm$6Mv^AOD-!p0P zp!u-b`B9WHM+`_Soz{bNQ`1-|VW4R&;Ywf zW({v)boyg~I08b3>j1y+DLcw81RpW5jSNZ$#f+`j#YeuJ7^Deh5JV* zzz_Z@qo_W;5?3y5TM2l4Yxg!-mV`Ct+wZ=rs^x&N^Ct-B&I%hxrvrbDVP#fV(d%pWc**pt zrDu1nimJ&5j0Z15(buD5hNA9>F0loIQ~&jkdbqXa?7v(79Zx(P7mV2zBrK7Xl+X+q zMO<4Pu2|M`t?U%g#|b(i>1p<8KpDpdyeX7CxKAE-Wsk3GB@#;L7`dsrq?B5Ose$oS z8SxqPf;0dH`-KH;H>`3|JjxiP2_YzBS!hxr-(28^W0Y_QohDfOHL&pKOQxn-+?ju>((%qem;)lalr6J9x8o70v&T1B zc9|RB_sSW>38f3H9NctLAo2GcIskq?y}kVj-q+OuW$W_Hojzp;N2*<2GjYn+bMruS z1S<)mlYeL`FT4up+MGI%;?nuBq+WujWpip zF+UnantBBg<2>0*Fleb@2L{1QTQFk_St!UIj;xmy9mH%hF34$C6dxn7=Yil1G6cfI zd?BiAGP3^|v#Ac#jLltwC|+4*Z;>A|ZvlzU1b;BeC&|R-vCl)H&Z!cY6***QRnlvR zby1n;6%`U9#l=IR^ik`886uw;(@@u}Cx?E+@&pC$)rn<-|6m0DgPtx z5W-@b#JLO#@YCdDh7dBTciHg+M>xBFJno5UHQ0)8v4`&;tXfMn^Re1M z@NktQs2}o{JL42p4+?hCQLm-R3eu@wz14!KGJdVbs9l>H4g;sUv@_^V!|RCZ_j?5# z*%X4J2K`Iq%=xgULZRU{g^B^h@!&^YEhX}=0O+nT;RhNUIXgk`{b+&wK zbWF4SW4g$u}w3YF+rq-(6#d?3Co1gVRC@cs(%SZ ziSda)Bp$;Cx8vqUzfWLt&%-AFKHW6~)@lYV=oHUh7Ht5Rdn)%vmwQ4+^oFe1pjC5? z*nPzYr^^mP4fk%Ns)4pRw31+{rqdt<3$!Q|LKoF;CtP9=qtGMEHdDDNvY!4LW)KJS z&x(6_e4W%a$T**O8?;k!K@ z+Yb`Lc0Zu;yH}RROK(v{vX)FFi*#983H<&om4Gf7ihKV8!+LH65&ij@dv#KHCZEHG z6zSmHI0Ct@DTcWzi)_?4r>TxFh=tWgE5QXd6M0PgDJBa!G;_4+>wiggs(8P$(L%Q) zSm3W%8zsRBu=VmdPeXJ%uXa~dgH^vea59AbJ2*`>2!QJmNPGX!M^ zI(^RFMnk|ORmSK^ln{)Upq9O&*kU&|TM1~9W3u$Z_*-dW?A+rY(N!Ro^2v8KmSLHb z6&H_JvNyc{Aiw=qJbr^fBV^b0f0D9U8lEu`WZH`}ksQWKrYp+=ED6DbnpQ!CDz;d# zc!H);U_qLW3y}~&ZKs;L*ZnCug*9Qw0y#&ZAJ ze~1Q_9XHBcc-}0=?vR<8#hrE3c6Af>t+Y(lwyu1$lDZ6_Xswl}Zte`~liSGF`P^3g z;w-qQ8L@YMGy29_a?_eL=58=_;0Jsk-hO0Nz)@3;eo_BYTkLW7unN9Qe(&>FuOGin`s$)p0<$0@HpLRy|H5g(jxak0K)qSe1Md*IZLv@=&C9Gj^JLejoB&442=!+tQm zpzEGm{kE=|rHv!E0GtWce3SMMA&1}a^FpOFOE>2(7*t^?$YMp8VAYLA#{2}LLa@Oi z_z6frS^muY>`QdYZ}5aZ-rN<>Ks>I7EjR1@M^a#fR%Es^-0XL(JZTPYL^LMsCq-W5 z-xLtICypC>)7LstWJMGOz|wdp*o;=nYh&2KK$wRDKWoYJ0{(c{u$+D1+UKEYv-#^>U4J4BWY?OP-gkUZ(_Yxq@jz)dVPMi0(up z01vImycoLhS!*z(E`s&zEpii$fBlx{SwJrniubBuFvY`kmJ_qTQd$e9`98pEOgmjl z0J7F7(PQej?k+bZLo_78>gA~a+A7ryLu}6bsW_qkf-i@_)5b?bf(gZdVM`iE4|iT= zJTg3=v;qPcsk3g{l}V;iwHSj`s@LCi0OpC+GQxf1!98%@#9G;LK786nxS-=Bd1H{{(Q8bE2C05kBNM1Aa%d%#1%z_h?af0t8TuiwuN} zlrdE-W2^YOW+a|nLUyC@(XcXd;RO0v2dDE(iX_>5|2+1CWk|4>Q+RNjguIraIBW`Q zeX_VD)UYz?q>f1rYLz_Rm14w?d_yCqp0Wnk(6}6p-b`vKebH?;sQbz~Z%hux$LYie zEO0JKNwIe0UYn z$~hENVhW<0dfzwq9gD2N=Mg{4K}%%;v9FZMN%HV`3?jvZWiPo|Yizb9sqY;Iiz1r~ zsvi+qm%|fThl+oF7^vwn0KmkaZLn6ozLiOzBPH}6Kk8{L3K{wE$lfApEQ8{@xGoB* zj|fbcojdg_!%&$yz*jQw!NcIhFB4%wuDBFWT+UvMyr`)RW*wp$#J#oh+ncWrB*t4QJE80K1gjoUc89!$uA08Md z^56nVbNERQBpq^cz8JBZgk^&CO1_x3cib#79uGR8Kn#4DTR1AZ6P#{(-oRF}vIGq3 zOKfr7DuvkkDlj)po2N!uv_?;)jm-LLU9ge#n09Z*icI>|g`_F@_5|)jaUjnF8w#*( zBmepk@SvQGe<`#D!L3vDzxAJQ4vIM@*zk?2$Qc&9%TXtaFOy!m%gkpO zrH)#`>n`w+JJyIJT#N^-haL)nG=;}=P6YzETf`mUK^nP*ZW&dzGQtT@exGQkHpb5? zV9oX$Sqgb3UNNdi|Lt))?2(t8TszZ-t8|uUYDY-*W0P!Np^MnMl0jDM%Khs%7w>8e z9>2X-OOg@|OM3pdhS=-xuHMVtvaM_0wnt|vcg7G41-TuO`haNsvm|DOmj0%5jRl!K zHc^3zu~tMtvf7Wg{?P6?Y7mc+lA?e5%KJe(eFfEGzHIA+2xV()u^_Ut$oyz*F!R{& z!VvTjC~el%o`$P936Fy79RKvu-p)6-y)Qc>kBpO}Hk=z&PnuDI-7u=|Uia+SvOh3@ zA0TR?PvrkDyewZL%CrR!A}j#&Ke_RS4xqP_819TI<-0sxl{UAuE#eIO{8+O;H3G(Z z{LC#bE3SNLQHM`-U@jDb$eB-cWJQ4rM)xVvN)1vSpi}c5>Z6mXL}|+6vurrH`j*JeYqBDZni%y*A(Y>d8Y{BR$T#HGWK)O{I^T$F$snv)n)oB;epRbKsN zDC_edD{V>La4!`N`<63$ z1X9R$E0Y1QwzW@~bmM8>zBP5~wA=7?b-mj?{#^#0?`EfACr^%6c{>OxtpBnZARQmS z2o2S1$1VVwI1kp?b3^(st+DqYid6w(Qu0uc5>J_&S+JK{^1k z8HkEpFMw4={Wq*i3%DJhlo~S`fGJ5{2)P-|2|VK{Ke$5lnG__XYZGPY-*ej#R$4fT z0#d{kDeyPg6)COu1K4KqoY1OLDppYw0y;h%!pYs6=pC$^TFg` z-%X5^P)alvAU`S(sT!1cP$Kj3_eJn-d9A!kL^3l!?qLlnt-NI-Xqx$2z?du+<>7=E z;{fPr?*rnogz_MpB?uAD zoBf1c3Kwx?x4wsQW@KVSFE3IFA>6%^q&d~6aq0X^ps9R5a-v zo&3+a_|JcJ=9!CivFDkYJ^Nkn-tS&(jeC9J#e>iC8%sN6r#w-K5J zrL^+@?||5iA&4LUC$QGhY=EFs(ez!2hwQTr1&xML#bip}`L9E!Gl`qq-hlSCAJQV{dB<4I zD`-T5Qy~Lg-aC`@YSZ;8!vFd|n$K@|PFtH6OnDclN}o^3CuoOCmSs8Y8FrLhHXhe&H$p z^m(~9v#(HlidD!ZmpHrNy-!UZmbKF#&6nFoZSIlIm;J7^9 zJlPVAdEHpV|1s=M-Xn$9<9mD;_bB-79mxtZ{g`z*cz8`-99v<0Wh=4=gRIH#WIY^P z7}3*05pD7cqHCL0ZOJLMH+_NI)oj^O-RAK#gWAdFLFr$zx4EpX48IwvEZIAyw!H|JQ%~{Bhnk(aRPC zAuYP}V5PKI4iA1-RcvudO2h*^xUcARv6-XIZO ztVqqnheK}#Wor#j#y6iIDl+oaj~%1DwX4ZujBIbkYf0HEx_uX2$Okxdj`iqYyL{X% zc|~IWRm%a_Yx&gzRWP1~ud5WH7Id`G)fdmnqn4%WV=G)0o0)#@_rl9ID1;AFu`{j6 zrEFqhl(!(3EooO*{^F}$s|ut=-=nhNfw%xWT?HSTS-5o1Crb)aHwU6%bFTO*!G_Iu z{p=40vKa2)cV`<_er&A&z~U|~;~#`(gq*Xat@m<=Y`_zUU1`}c@lBH;VyvK$xjf|~CsjyEaf?0K#V)_*)5ydI8rUZu6grOn!> zwK$HVSStNAHySu&Ry-Z%uQDX&Yb&O^#8NuCtDP68Y(>J5%}Z{+-!_U~c!hS~#mlcJ z$}{%JbvHf!7$+}x+Wdt(l>xWJ%pSr0TGj6De)BPd;-at~HrQUFJb!g+&y_zcQ=8Y50;m_k(bDRfyPVIkrZNvjmP18)wh|^jr>rgnnjjd18Jg_*FE2aDo`)_3Zr}S-W|OJ#N#P|kry#Qpd+Gg!?{R6j^c!{KTsc|p zt$2{#+l+3{22=p$B2ekXDJ$@kG<@MF)ROkN^5lHqEeLiqdpRq@H=!4^Dws*Oy0orN zQ67J1c`bOt57qX?Q;{{wT$F26<;vywbaOq#sYSc#Oe3S!7-1=#_~N%?Nh-FbnvPQLbRU2biSpuV!xd>h|s)7+^sN{b9S54EGdn=ZUV&r@p& zzFfVP1}H?xTu{|KnYyI39c>eiG+Y1r?nSa{h8Jtw?8wgMmi8V>D)h%Cx^K*R%O?Xf zz|T(k%%uG*sJMv3D#s>GT17oBY&HF>acdZF-H3*FWBxM>)w}0acR;h^F=bzG3DSQ6 z|JWhX_gtDwAguG$i^eKa9(lDZ$_GRdL*70mr3Con?)qkt(cCIQy?>f3_I_G8D?+PA z>&xkTY2PK9N6O9VV+qXp-*l=i+qY&NG}I4A%LZGC5BLz`PlM_8wZ`Way6UJBS1mS; z&X$xf99`XnC-ZdX}Hr%0XA_TMcA{PMMUZEEhTI zoIi3;>P!%~>Q?9J$xiTm;!ga?+IRogg!h?!6nCBU&@N?i*LbS4m9^T#?<5&iMidhTER4?Ee9`EWy+I1|S+`7w% zc?2)d%+uc28Wt~^W%?Vkl>G9SpLu5CU{;d5!_06Pc#+OWolhdbNR!Sx!k(X5KLf*a ztO`x)u}ps!A+neJ(9$DW)vlpC-nlM2x&g@T_&2;@)nN5PsAf{U!mY@bR=+G_=D&B` za{MD&!~F{0-0ty*#t--2_tU14RW*gu{aOeen9H2MJ*qquz1kYdF~h%*8w4&gUtnG% zc8&d(!GWfk;KjulYTsQ=<>OAaD~7WYEw9JbMfmjV*;^Y}$EyU2R84S1HhOlub0GlH zOvLQqW!x<;57$g1&p~DBXF453Ph&S8Ne8*GxatSG+7hAeD4bWNMzHoeSG^wDp%n;_ z;v4Rr7R3ig7p}`&(cLy!q+7^qNQ@1jdgm2<-{mATCE-U%qNzxZtM_fdR}kA0!{x^;Y3eG%9TI6#6kLru(Z*m z%LhMhD==D|xH1~q5&M;?p3Yk<;crpDexkA-M`J8!$y)xbvMa&0Y9NLsz4%z568*`s zTZOlQ_xndG)mt9kn{kGpVP$+>N6Gnbvz|)){zU#U=BN)fent0p^MMjuA(1YC1r*Nj zNnM@)sHZ8TXN)V5zs;9ADdfREi`t_&Bi-5jI=xlODkcJ)=9m8B6~1WOQfr4_?F3{c)m}*HQ)a$Ws>m=yL)l$c8&e@t43F)2+*)|DgqEEhv1`~%YU0&=SP>9oBJol z-eXE$B@R)DR696SwHVl{vsj(u*V-RD*%~{^2~hgCC6#j+a)={QP?I?)e3g$8W-DBB z5nXxCoBS*Q`f~Fm?+8Xr&tSz|MNkK>A+{WAN5FdFh=%_@uBa;F(RtX>zkSlaor#|q zD_Km=*4Y&+;^vg2qSr2}xY(eb+|8k6axx%6x?G1%Y}lA$W1rXgQ@{yX&pHnRc+=F~ z!itB%yB>a65U-W39iZ(VrtQ|})BEB1Ut()6rFyQ+hSGaHj#eg z`2gorVLJ2CVFk|+DjAe``gM(kmsy;|xPG~6ZmWQ(+=C(8asBBbcGVI&sdT#1z6fNt zi1>-M=thSqlfO2*YOi>~kM}f_69uwr%5kz`IkJ&6myW!wX(|he>P`-+8am^DTrv(? zMABWR`bjIlRzkjPjOOfQ0DZqS!A`@;odA2lyLuc;L{&FsL@Bb+H-WkmhnP^66K+jJ9J}X+JR+#ZU8d)+o+?abz z#YOGxvHzx9?}{gR6b+f>ntlLn+%_C)aew3u+$66s?- z|E=M@$I3wq@&m1KL8VbFgXr~=(pLQ8@#FHH7YY6?wK@FtGGfPXX48ao4)`p3A6H!Z z-=HEl|F)&($T`gymvT=^!t=Ve`2~R?%9Ee(d}sATXT0R^`N3b7OrM*cSiGX;Cp!{| z*z~&Tl@e)`I%!ThmN+~=UZ2kUr92@Up<$nA;}dbRemFfF7rFDz)JUwO&JCuO*1pt- zNf36^Wt{%yZ#l$PJ-_(<9VnUWmHhatakTrt22 z5pmP-W_WofSh}u*j%)8RIh`PLoKuZrHc^q>ouOG%x(NNB_!>=ew9R@VB9xBf#l*u( zR@kRP<)sZTB)FyZX3zOz%6cY#k!B8pE-DWQnLHdynrnH;jy7CogHG{by>`+FU*)_) zb%#cMyGTZQ06egf;uU4=zJWK|uCBowTBp9i)*JN;fuI?gLD z@MCdg);ojVd&OG(iZ7zVk^E47cs*MV&l0iV%^mPaHRYtlKSR-d<~Z;5y;|5YE=K*@ zbd#JxYH1(m6{i;0?O-8PDo0famT6p~IHj3v;q->^lqUM9eP7VTZ;+q{0`eSo`Pl)9 zM+LXY{2vvxuzRMlF?r%e*tk8TriNx$fuifi;JzPUvA(uD5Yc8q*!lVrnw9*lL{kkv zgsp;vAuUZWm8Lg>$?SPvpNd32fZ^XL(wRHensl%#w)GXzHbyn~WoDJ*{-(0(FCi!U z#w`^>`EG!XmOo&8uodsya#FYD7wTf=P5PIc*ovTL736hQhjuG_Th`go!KPK~PTfnc zh}x859jkqw518LmA!sldGd7Sj6q%$)Pam0K`L8BV2F1^HCsQwE0mJ&Ft!~YF?3NxSb z=f0mTNA*1^aLP3s$iFcX*AWUjulRDsltGhmj7z2Pne_GUq|157$@7kWC!np$%k|qX zlt)PSeBBZ=|7E9(QF5omE|8Q<%%J9GiO2PBhBPCHwr!0~$vRuIxHB?+qvZFP(M;n) zeX$lO$uzgB#&cd|TI7&}N;F3Z<@s(&CBa_g$gghTd7F1Z9HTWl#CF!4sNFEz1R0uHRuBF@JFi2C(yL>|abVj?UoPUj(g+>N#@E zz9dP)E@AkiG6Zk76&K8$t1YFmw8FXHXr#3v8#{|J z0v9MLjM-`GAYx0I^`=?pr>2|Nc1D8sO0d+JmzNbvO$r^bWEdynetMD<+GaQWs2*4c zFAn16@zBd|CAj<&o))ij`CbX8^cA9fB?dF%Lf~Ssi4VXCJJqvq99&?uvp{GH+*n+$(FOep$!6? z7oxs_$j*(?{CNGY$@@kzTUG@){R=Zfo?NRMd`*UCXjGutR{N@aYZ?BU-%*A{CK6J- zKg%ccXMa4XTjDScUu72D+7v@GqfC0Us~qxO`(&5mY_f7MG8$~EFAhl!&TA{NFEB(U zqGF(xHm72qK_C5bdW!~RRn1zv;Fh;|1M)p`C`WM1^lyX6Eaxg+&^RE67Q@i|5u2=X zwll3(9Cci$VX+IJEnMdbQrLUGWE7BmF7oxc8E5f_nl+2 z!^-Ui*bsI%rx{-w{m^3v>k{0CDbZRZ6|_ z?4#_{T(&IoG(msg1xSvz*LypLA=G%Y-fAUh58D7;Pr@$o@bdlo8IjqnU1Z@TBxrc-Gv9(1!48)6pJ-4?fx0f0#Nj zeeGfk>)hXYJ##eRc1DOv4nBls{|&3A9z6VJZUFCqheefi zIUF=h)qsXsU)BE$LQ|tgaQs2-_$=%QhA}F+t9!I#$Q&OORnUbWbJ}@{7mG^h8hzaY z&xUbG-Ld&sGjB6JwOT*Y&Kvf}RtNE_nHf0>_{<}xr8dwb?NXK|2c1E>r!NS~sr9CoSs2#5o*blxOl1u)^@R-g+# zmcFQmIyhns>g4cJmwor)G-vk>csL`q$EOaqi^^@rrcxp&UC=wb@<%7@PFQa=>n_9zF8Yt#s?oUu9dZ7#i+<#^R6K+gX7y*s z*$(j-d4dfMT1hKr_5Xp5f?E6mrhM$AY6vagb|FeUt`r=nzJ(888SH~!<~flgME>2R zcfv}WcF^SO*T(yim`sAHw|?!juXK{%w6i6$p0#jxCPuhuYS_Xj2fKsW#!(-2aoPh0 zgd2$;J$UuEv>63~!vsnurWz5|-s=a$vuy}$#xD2a+4|RO=qJFYmW$n(?3y#<&+laZ z^#XhW0p|xPHg~2PZd#qPmbse+OR9|;ZQh>^*T3@KU_)D>u8v5L_WfV~^>1TouGr?Eq^FtUE z_#L>=sjbAMG#SYdFqSuuo;f*$tp9Z!fk5#Ny)j^N)3)VI4baq`gWYHIoYSo9uSZm` zQn1395wOLPB$z?3ivK;Fa-Ff$*WZ}XO&~<*@$#O95G{5)*x$ZX-dEJN& z!(hSh!3US6*i+1FF!>Q2?~LX~C4fbaU>kARNsJ$u^#~?)s?swPzPdDgk+X0;TMVZ@ z;9H)WvOO?Zi92IF(Db%DFkZxb9=^ z4?v~+NJ0GY)0K}JxiChMFua5ZJ%p+Tzr_*q@$eK7b`A5W4QD%$u4a;VY5*RFu0*jO z%B&aOSfJfed51yk;;;Iyk1%K)=@Ij2$J8Udaa1-g1!7zJ1d(9Mu)@%)@did-Dh!u% zww)?p844b;x%MGoKI4#mJ(A(029R@2S}Fu@9)?RrV7$R_0d0Tt`=e9nkF= z=e3jJvqeVq3F_dGZ2cl~zqTv$n#Wo2I;HiB4_|*Azk9IB;LLyhjJ8p#+NM7*c?G0; zeZR(L(B>6lzzHpmq6Ej_?5k{@bxntDQV|xufRj#hOfxf3`jmitA7BkVqWK_u_F2I}NSygny&dBZyTav^~lxst{*0vV0KM4O-#59)!(@&&1&*k67DV z;e{pX2Mj=vGg=qZjdMCGE%AVY`ZVCqms_n@Yeao~Ftf`k_lq??h`?nF4q-KhXMo7{ z+FpVn_L_zPF+kp{n;qv?SlTj`rsTCIyaN`yd|OlO8W`<35re4qS`xn@aQyr5;ctSg zqMu-i%j}xsG5yUArIqMk=e?w|Zp}NyedMsG#08EG&J|~aQbuLS2m-Z359=A(xLRPZ zH7F30F*3-;l`{H)07KrLx7e3>>C3mI+t>YgKL`r|(<82TTRf433c^f@3#aT5rl2^@ z%zpUMJZNTYEkn@kSPGqiVmcIIRN`E`HbvzedNX#FcwZ?)sjjt&&%B=j22&%>2CJb2 zm+(%51Q3V`i1NRZfU;bh5SLyr;Po(3mwluf7m=TA)Hv9E5`ee;2-PRAuE)8>_+vEZ zfHwOL6!jq$BhFrc!0V}phKvn?lMqilV{ZznPf?508#s+=W|?<7f!CSA6{NE@_RS{F zamY-UdYyTn86<(%7ohRj-xykOHfhpaXUUV5cvZptVsG^XI9a%1pdmB54)eFmDE7Rw zu?M9ZltG%;(ebbPU=+&e5INFaN=N`B7wmHH!SX^uJlU($3uu~I`nBhbYO@m%l`9G- zy;w!gXU#^MDaf4Fob!3~Y{nX`Ag-w!n}}foCz2vgmLUT8=e@0@H*()0OnCO*I#S@R zYaja+*Rn$_;;I$Pf=LA%QC|P;nYSnKOrwzHS{GIUQxCSM{JH<4j~nRYn##@Wi6cOL z5ll`gpXOJZj_Co5P_`SkEEm8)2mE|j;RUb4t2Kvv3~B>3(Mu@PBOb=_-+p}}SIWyq z+Dtz72gX41S=NsRmHCSq=Z!1DPolpd0Ny?-I({CQ!fQ1N&ygF{e(`CtVL!s%p?s6p zu954+01_^5i)*9@YHUW^1VbcFVOZyd`gH-J5a2ELDP|Ac5${y;N#mUp6G))E8Tu1% z3-OC8iof27#vX-`YdqA}JRihA>SjU$;zcwy`n!s)P}3Xej|9`4ADYw+J3p?#P4V^D z%iWW=DAwf!i+&TVI}{sjf?P09^^B7A9iy%wRdgFF6gX05^bh{tJt_L%tErs8Go$&P zSk1 zbW)jz+dBk;U)-n{>QxOBbk;d|)%@mgt%iVd)eUqxkBFkSx`KZqMD2dO{hC7U*bui_ zMobS-#&dS6r9S^R0TQ)HPv0MBmJyIt&NG`*&NF7XDnps4@yP~OWV6hTbVnM1sorX< zhrM~I?o^xrNmHSh(#N?uMoy%vd6`~j#~%z&D&-Mod*X~R9#s;j>a(Hd0W{E^?#C@Gb< zugo$`=#N+r<>xBL1!~XIiqK5gvn6Os9(r+Ybwjl+yAHE=T1)PwYZ9(L3vZjo`dKfn z_~xJ+LU8UqaisbtGn{%4cKlAyeoUMzW~CAl6Cn1>H)bt294wg;$g!tUdEhVGX$_1K z3L%W8qKXd*17!bIdf;_`kkmTy#^((3+oH^eA+{ieDw|=VUMp>Y1@WI?#w!I_I?pic3|ec6j_*3`{?tq6lCmUM z4o{}D&qmYGZH_-wW7FussXn!1Lqo@F!!!0J{~Z+81^UmKF5oG~aV0SvSXGDUTxvuS zfu`jS#}36ZfaInNKlg?Bri(ykLyKOHIjC^*G7ZvnR`+>&q$|aId1thQ7}C|-P@J$h zr;D7i-{^DIREl1{4WdaJbj5VEaBm408GRjQ?H3AU?^A~pv-JPO(BYnS(KXeC#}|uk zwZzY`Ytor&T_x^?m)`|SV!Tm!6RAP*!`pqF`*hfz*&O?THWAAT%wT;#scrExXEP-> z7!{{lMh!thT{Tnwopb}IH68=LwHG@?QT#P~cnIAh$Hx9;}d7Z%8IY z3S%*Pe4kznGQX=0N(zs|*S#K#99(VzL5Yj>*(s9DF!_}S-BNSzWhI|KmchreFk(1S zrQ7K>rU|p6OsgJ-bQ;Xthd3UHq^H0iQpMStjf6nXIXNVaQqD)tf7KI%XG3vnaQ{}d zaRD5uM)l4HFttjJOVQxmb9#_>%>gf;7{WT-lz3B4?`*twwHPPvRrbAQKg~L*o7>T% z?kTfO8J2)omK;F$w+C`V#o)L6;|q5omUbq;XgbZTR|&xGii0yEEBn${cxI>%^$scL zj=tXOdUs5<_tq{B5vS5IJ)H{QhU6wn$HD0WXbOSB?GW{Gzi3XBM45k|F_?3K&T9r+ zJYTcRpfi?&m&hj)nW0{@{-0hS^B)R!kt{M;u#27aJXNKMp1A^MQ`z2uP$%ew9HtFN*7d4lEbQu3BJLYXg=!{p zFZ>aLfi>vLi6$1W>@zgJrHwWvoO0~0I(TG_P4iiIFMsio;sWI|DiY=A~9=b_vwFkct?%KXP~l$ zlqaseJRP>PW^kz1OCj|?(x1(0Xg+a(7I&xAV6hnh0+Xx^TH+Ya?$$2;A;VHV?YuEh zapLTVhG3^tnruY<%AEvuMQUyGxYu6h8=vWL%c1`ZIXq8}0nWOf8n!E{)ggxffK97AO8zn>7R{D;#} z+fF9|ht9%u(PuNE9zQuc;<$H>4<%bT_YIKF((j&PII1*t$J`-(z}>y;%F@(p^QVue zr*?_w+(S9LVK4B2;l07}Tm^zJpbe#;mT?lEt4~`CfwESvk}AC}p$rA>YL$|ynyak$ zxH8Ngq^EPzKZNQP2XSle9;i`bBwNIFfsC1hTqjk*A0*EZ?1W|I7|||zn=}nnSqQu|0;uTnIz<`$=B|%Ua@RyUCCQD zcVN28Z4&T48P~G2=^7*&N%;C^C%(y;lQp;Qf1!B$7#=?iayrTZWOt*GK~Pjku@|-8 zIm%tvdlh=O)nStfkYcuBqw@5?5Qi%F@+1sEhI6lVkNzHV)!3ZrJ*|F8IoCGh=HEvX zIyILy6I$!8sjj`p-b=G5Y6;LI)jt$fAP4~J;A)D7ycdnG7yK@-pu$19l=^XCK(z3{ z-QzgsXox(02!wmHL9&rV&lRB|{S47baQ`4LmS*lQ;{+gO zta~pkG->*IX$GWyiDq57ZCU5zu&x#hcf9%^x5)Ss+YfoQ{ErtNv~E%NC0QH{lV;kZ znx!M;`wSySb|(Nwdle8}v}5^ci5W8UG!g2mz(qkmRBmSDwwE%=5XiwrJ2rR}c&~^; zM8}a3nHsuP*%VwveX{CXD?SoJ_>WSP!5s4|BbQqaw+Z1!b)6hd320ZoKNN~OgkXBw zf6+awurBg{37&_%_hXV=W#-yncF!0i$BNy2&?R-^-zEo74*7fOq=xDbWqK*GN)hB5 zv1h9!wUv00L-wd!D+4x%w9O9@0tZ5ki_Ly--u6>T-?EOia#7rk?M^X70#8s>VvZ|S z^%WtsmfW@I!VvkKCdZjKdfiS2HX`y#-N*V!cGL%cN2V(ATq#V;vAEnvCS)t2sqn{7mhO&q z>A6s*ZbNP4qurF-j^yR_Jd+O{rvr)i?j^b(3aU{Xxw6}l~m ziQ#L|S~NRIySTdfqNd4v?q{k>kJFixV<|4HiuO;y$!2KD=gHSdpy00x$jKWa(*I1F zVLlq_LbR6_QVcY;eGhHwnv_PKZ?c>1q@X7Pi^-eXxc}f6cT1RzW=T z_C#~}7PmH>)Q5(Bnyi~=pL2APTA)33k^D{+MK=IC> z$1#;nB8rJ?1|0GMdhdR_K;{4G46;CW2hzO$`an4cN}B=sKqd!r#s0oP>OWMSL;PJ# z{}RX6G{8hWvEA$26lzqVw5d&9(^%Q=@yE!yA_7Vyz*&urks~Cv^^PHasZAc!p`zUo zUF3(}m~J}VGjB)tii?&e@#%usR)LOu6~T7}D$Dl&DF6abcbN9>KPnF1jaDf&^QPZ( zcvy_8IUxyED4YB|QxIyh8_UBMtHBnnvLit|AA=?A-4JIcqgJS?TbD8{uczrH@*K00u{M)UNxFj!i0`EV+h@H zwsd2hC+t+#JcY92>qW0H)W7CMa4l|1-g&gU1GdJ(e_AjPNxP zr<#!z4Ma>XLbhZO7l8jsth|dvKFyLe*?a9`CR-4mFa&M{E$H75sI)Nq63G!>n31qq zYz><76)~quf0((}H*!l72GVR>dk&ZQe1N#}ZXK(4#UXGYn-lur`ADy;Sbi&CPWM&v-!=L7_U~OrooKJD4xTh^ucV@$EqncSGdMH zAXmzdI@g&{l-BKi@KJu|0_$@2P>weW&i*H delta 28635 zcmZUZV{|4#*RChFZQHhOTN68(*m)+l@x-=mOl;c|+n(s;UGMqvedqkRdiARAwYsaj z_FZ@F+BY%LAhqB84h9JZ4F(Ga4~7Va42BAZ4u%Pa4TcMb4@L+^3`Pn@4n}E0J);F@ zXJ+RB#+RUD08WUIr=G#E=>va6fb4LtWhM+*v9CuF3{I2u=9(l(V6NH8ur*GD^<7;^ z+cg-{FGnqPel(OT^b<8hAOH@Z?$~_a2>pAm{J(Z5p0;w6*OJj?D4YG-9cXn)ve%k0 zH2+;r9F9=YR0rlxP!a4lD&3G3yPhq`Kw-~nVYmIc2Do@xx%r2~DGsM~kSj6m*u~HP z!G8>N`TTbnb{S`cD8v8nV}epX(&6p6Bzbn+p2}Q2I3SnHR06&S;l1g@{7qlm4XjjF z8@SRJFE@Ca*cJ=_GxLC_fjUbbjg?afwj3?(VsAXD*PwNWHRPSj^6o}M0g~?SmmwP$0qergcz6&a!7sf(<$_@? zg4hs;U9F|>t0sl~Uz#)2tM5_qz*^as;jB$~#*ZqB{2?-NV%SAwTzZmcp4=Rf?{gzX zYgB#@uVOz_SGnPIIX}T$tXtg7^Oq`7F_SBe^Dv}%(d-m8BS%U7p#AsNd(P#YBwV@Vc5#cOE^r${DdLC7APsgt ze1MBa{T2=f3Wk2cQ_AhcJt#(->Xv(rKS0M8G?)ta0)C|Y&-eim4aw#xH*zjzLcu54 z@*Tn{tfy!!S6a&nnP>!ItY}POeBK1xr?%J7K6L4)0hJ(hZ9h0+iV}myGZ?-wHC2-n z0#t+X)V+^P>(5++^#O?W$J;(@SR;=lqJ`mCskY$X^x}H#joR5ArWRlRZmYthYK*gfRxQTmV*A&QX#d`;{a25XBt^~k z8RAa+ge6U{pibw13pJ=EU+tHc<;ueLxfD25;W+#;%fk8PW85vINF5!-Z8s|1g-W>* z=(7lFR{bGgO^a?}bMKg=#h&%oqYwZCrbw6Ao$&O><=kuA6!aj4bGsB(6OzYLFzvBw zo~7<+w#GMH<>Bxc?8YgY9NIF0&Wy_m{5d778 zU<6c;Tv-2ujJQipqV**+dv;+R$Nf#m!_G(O8tZWW)qw!-_-E+{$5Sp^}7wpQo)8A6O5xuYl|8fbQ!@5XBqJ^?Z zR2<2@#VyB{b~Q&4$sI#NZ#IZo_g0!<>)SC=$43L&etY}|8}v93f2PR#st-HZI9 z-cPdHiN_(2OwEEUMZ5rza21-b1P zPU$s@mYqLgtOW_V6G^z1Yzx7rIUCelAw5bRR0Q4D=1|BBx498R0@lQrss-{SbKB=g zd!Q|ocKXi5GLusJB_`}_b?O?0^RC zm2(^0f&LO!s!2_ExJ}bCGiFN(4x`9WD;~kiioQX!MNwppdh~@O4-3&8o9-oUoAsv2M%A|U87W!3+dW3UEF$`mfp)O1a3 z@FLX{#j(kLwAzV|-H}{&%-XvEdZ+r@!WTmGRcA;oZ9q;z2*jXd3cN*_i{bsK0jCzd zaRlut%Tp3|Qv?Bn(xn(xoCS@E6+KeFZwu}2Ux*m78l$+vo?35fD&LLAiOLN7=J_UnqzOSz}TG5;f~?RQ!}%@$G~*$_M0? zLP`lKo?Hti$t!g&bY$5vlzzi9?c?jZ9S~9%J5c88MaJ3IL%OW+847BQguVS=K>ge3s zvH%LyGm+lD`Dnh~tpkQh+IaSi!?7xX>wf1-9#S1;+-m7-rB1G#4@Tlm7ca!UQ^+TzTJfqjRDS~tX{c= zY^ABMxOKCfBTPShR>j+y?g?IqU4-sed9kkf_NbU#=YYN>E<8K9xX6pQoNrdZdLn9V zMfZ!@rGxEDOtaaLDq5vRW!>YRFwUjRK?P;?VUsCF>Sd=S>LmX`gSgHBM}18@6Cj`0 z1&i8RrVmoER|gRmm5XItl^6|UmFYh92G_MKH)#JaGR>jGnCwnQj(RLtB62L_v zjD!CurZf3$<>-dfH3)y9q&#|eKLVKFBs8Cw3U#d19`lQ~>V6ve&jjn@P?A}g)4?0O zKriz#cE@UJw!Bf|5D8Ew?kuXWR#k*jf*UhA77>dGwKsLu6lyu(XXJ7;*lEA2(Si_P;PrzSTLvKJ<#z^^ zzf6z<-6YIVWcb0WuPNV04-H#RgG`z~j3fCLqu4dPbwgq+E|2=|%!DSFn8gRC)QAs7 zM}Aoxk#f-Ud(*(RL5Rh9mhXDjiTP~{#_W>4T2*9)jOJf4$)|$2&2m*%5}bm`6gyg_ zx-HcK+)511Uzj!T5f_0MdVs7;J=hD?cUfQSUvxCv=z8m0 zA(XTnM`JC9NO`Qt4n=;atsDmg4HSRV6d33*ms{u8x_L8E%PDNyOYiF!|Io6%9pjO1 z8kq#^wW?Svr!F$GGF8U3wF_{tr1qa0fIGLD%d!xNIy)7mRHtOLssnCs5=9p<**T&4 zF{}ljyK3NHGzo4d`_Q=+N;kGt{rka|Fd=twdy9Z!v<#zE=bN5`49XLENxgI{eOD-3 zbB~n0Y)EAlwCJ+w#r&+$`9#^?Ni}0a^N)5;d>uckd}gjCvk1mzHYF~zvvz6jej%2y z=kNfB{G`}4yy;PHCID!WF&l3Ce~E(*J@NRj1er{qQMA}T`u{1L&VuZSfNQ0{8QU}V zL*?SBxJ31+`JKE7i0j&7^mwn~xyV55$wDL#Ya-qA?o3!MUn_&FOCcgUCe+iimMdrT zpqr2@4M40FT!cZ41)n$ru(1jdM4>pK>k(N<6q$m#yV!UFmH=ppj~isTcp=TMaYb3I zmmhKZ#snq`KnrhY1&XEn_JkkM#`7>tjZ0q5aYMGXON4%~^l>#7kqxag8DW!e@K zmv=qrYRRgr3JPim97<%flFAATC_kfS@T+Vn+C&|^UhOErQi2z+69YI78^|dW;-mnH zFk5Ic7fH69x&SM#y110PJj8PKxI}BnGALg>lq7#F@y}QSSYepz&Mt&BdOx)v8V1?n zPNA7QkH2%t?3+*h&N6%?D)CK_Dchhks0H z{{5FAP$^10hzsr3_D{Vfd##}XEk;^$pn4Wuue6Ry06QRA!%si>qFQ69LB7R!w5Ot` z6XgfSI$@V`+54?xC+U#uU!4e4!NeTTR@9g#!@!Ky4iMxVu*xx#kxD$U(^5}18ev<> zxy3rgaq0oxyXMptt}x5L$1fwDBod!H)5>zVw|mB>=V#}r!+Q8=fP8XF+kVPwdn7x* zrpDKGEhjKzW^LMPc>;c%U#3qK+xw<418|28fed6KtNs`x;R#5&k2O*u`8GqEG0^co zvOYm~cLh%w|DOKcXZasZa0(bIV4S_Z8Wy)8PI?2LS04gj3=r4L&H4pZH=0wRso##J0g8P1dwT!0VsEj35l z!VGMsJK8PhTTp{~Nmu7^`p9^_xUh@v=$>YyYg`xr+8&2b0^oI>GK+xn`fo@G^us|6 znkt|<`nEYf0&-=g#m45cnvBQk2i_6&2a=g*y8<7w8I!s47b z+}-a5W0f8fr3?-y)%RAiytnH`)55e1obs@=02j@n59}#}IJ{S$Pn_07t-7naj=qBE z?OeaBbV4n5-g>e9KDT;*(Dn|x0_$l}(Sd2asFVOUHV#2SSQl4kb7Om0&-G^QF$Z!9 zpUI}`8cCTBxX0CHnnT$+zO|)CtgC*f7Jf|vG zF0p$zTvm$kS48^TY_-6qC*eUV_Qmj-Ji^sG9cdiJjc(>Vio-vNcJyEI6aun3>v8~v z{j3?C$nKhYObB&sk`mf0EXk7?Z4=3x%BvA0qK2kwtKpyJ5Ba~m(2^=>0d8n1a3aK@F1Rsnd zk3Hp!&3QdgZ{V#H#&xBaB<3K?^Ynl^;)93qz@Fu8D6l||!4-4y0bqj1`DV=Ot}z$DZN8!P|n|g^Ver|kI0elEaJNO8cJ*6ampGk^jP~}tu zq}GIQvz_0z7%S%IR2OuWhh+jQZKRhx{i!@%n}5HApH6?GdW9I8;)w~N6YloJCrol$ zs^xh<;&?Z7MEc~l#tvUrhYui->jR$V#0934?3ezz_jQrJtHZ*YJ^nolACvxO+=ahrSqDx2Ic0CUS;x zF%ZR?R<3v!9x3)EUodP&!*#iiwg;8~4QhnqiZS7!R4dn{Yxyl<<`Mw8;+JN0qq7#0 zN`6I9C!Sk(d_Vqx@vEh7X)hp^SE{t?vi~HiJmu>(v*-P_?A~6TuH~@FI3f%Mln8_| z#?xb(@4nD>n23Gtw`J46zg6&TbVa+L)>zRG5HpQ4v|cr(v3ex+S!KKC`M_y5I`Zoe zu=RF_U_4Kr!L<4orh7oHF&I;>fjV|20^N(I?ed$nBp0_vmuyVtVvMTN5qY3*lS0m8 zx+G5a${MyAGoL*tmHp;R^qa-~FASLYV^v;3A6g#v>S%p)oMt-ZV{SeEWEl1xcXSsXUowi2<*(SO_YJ%m4bD@=k z_LIl7fI392@I*)FS*Om1G}Np;tA}yI3SUo3OhSIoSj+ksz#9k>jIaV>)NjyQ3xv^C zSic4Kf9mUHmaQYY6lQ4eb*+_kuNj$&+VcdhsO%_ZJ-RhY-MlPxHKY$_RvJ#NK>WeZ z_5CvP#w-lB)kx?A6x$Y?ftzCXgb$-e3|tU_KA}E+P-T#k^)Gv93dC*1`rF;mi1AwK@x&5&FX@c&ec#MDY#Nnfi1NE_089Ol^vT7TFjlp- z@wWcOR42FJ_Bpokzdh^4WPNou<5|z?NXP!k{w9CWR&AO6K35ovw~I!jX;LN5)^-gr z3r)8n(b!ie*|H;~9j~7a3fVJ}kcb!d2=5XHhU%u_9@(18o^VR9sD}>UBanJ8k`Re& zboW?}m-&37y@{NO<_Cg9tCJC>e;%{;x5X7OUq-c5_AB{cKZ zmS-})l;;~@u>-65(b?0b$`CKvdY4k9DRrnb+*^c~@_j7na9ymn`V#zO3TDm>(5Xb8 zLb>r7W-WV#*388nRmrcR1=J72k4^Vy}4tD=PQ-Vqwv)5C%rfcwyVx zu$l*v{C{MLQPqBm(i_sn^YA_l$TpMSVmm+c#Kg0-RiG&N=3y;|NgFKax+|`&P~~JU zXZ>BXEzv%R(;Z=95&l$$si8l8u#QaeSb0AXr3|o^$s}hNgru-B2 zhnhVAFc^fzt5s{nA&Pp$YQiaT9#QzppR1X>+y!cr3XTI4q2D`N@XU!jZAzjA(H?cZ>KB( z-G^_E(43t<%Kjb+p)H+1cOoAq z>+XrWtt*SxcSkNH&Zt_U4L}F~c8#JS*QZ?sJw-v~qPB4y3gnmSxUr2BT7p2x?5@Q} zJB+0ni5AO?dJ>IBU7$Efs$F*9WN8TiPs%lli{J+uEaZVI17#~K#}<1*X2lpRdx#q) zeUZ2rbb5vZ&RonG_4I+&FT=V&@k$B`&9P;WPy|%*{S~D8=%%Kb84h@JZWz45>3^I- zvd{x%)YRPE#g`?~QZ$#WBGGi&7ZNjPSi|{{GR~y3&H^MRJB!%7yoXyj@9b9CX+2dEdIkK@xT)yR`M3f%8-e zO;gd@-~944LNp}`M5vq4nKI*m4vCPg=p}D8v+ktKCZaxap6=6E?9^h~_^jD@Ek#1# zt?)V*U)h7DGP8V5uA=B9shtF-gb}t()at;9*`t8nLm@oRlF~d)~xodRaR_o9S+-$!82a zv~5hJGTL`6XuLv2e|nhq5XSjvOf8#Nvo7SPrdr-pbmIJyJQ32l^lb8DaEPIW8Y&IS z4@N4f3C?~*E#V1#_2A6yA}ewO|1)yBZim^$hj0g!QqN6t8v z_L@kFj_2DVnls}~8r5`wmT2*}w_92e?ylKZH{5eGS8PPGS+FN-u=8)!s^RXULLaLQI&|vDKrum zI@R$tPGH*9zXkw&$<XaSyA*9{sB_7-Kn2}!FwKWx3KgS}YJRmtS# z;@K4R`&`9$kTh2(A$=4RJ^N=)5XtJ$P}U`&Q=^0wLK1dP)!LG&SGsZd@28jZFS)Ml z+dZ@94>Rn$m1SD%ynb_1E>flr*!E3c-I`oizBz!wpv@E3mydtj7a4wz-PFQmVzLvwYMR!}k{l(h-<P3du!HbMUUY0mn6lr~&|zQE8gjMpI!3kXwMz^SX> z*3SGGnb~l>b_8yua9=(>`D<3KRK2ejyxHn9m7X%$bo(9_LJdE`nD%v!KH_sQMV{De zJ1O`*?A#>`a40&tl0$h7(ZnZ=8OA6(R=K|#@k*3PhV%HEjPt3jN-*TmDFLpFHH9+Y zJ7w%s7x5adwU8eJy-q`(k1SMrGUq;Wz%ARmB^*|$DtBNdN2oIQ^`s_pr}fksAq%xy z8tEjNC_5!zBAiA^tjL~c@(R~Ncj$B3?6P<7obk|sAk#`cD9#eZyc>VbWvB5_0|g_a zZwq{ng5O|aJJx;(@z3Pg-vEO2J+GK1DY>yGh%9qFt_~Z~dVw&Xk{_H}L`jFijT+N` zxF;?{-D?=LaMBhs)?jOW;=EJ;YNU`8-DbLQ(T?N{ahd+5Z_PyGvuIaIdO6Ge*-LZemxAPtbyDCrU69o{=4I=c`j?izPsgEg^C)x$ z-m`Ik+Bx%(bK=t5h~gs~%iR*D=M?~WZN$&`6jBn@0M==uqlY2>{tp=6V19%34fZ!U z-{5|O_YM9x1m6&TL)41+oA@Ogz^Cte_uH|bKf6|2!F~BHExam_`ePH|{3|Y5spc6$ zmXNp27WGELso8(q$hLPd?wVlYv0*sR(IE%vT!{EAGxNC1aJSdxZE9$qYejHJf5Xf~ z#c)E`k9KIL*jsBHK(zgbp`zx%HvR47i%90k`A@BXyBV#wja4rD4bMR;pbsRHn=Q|~ zJv-q!-2GJ7JhpL*MG9!IgmZR^x_U6=hV_=mYdl{SSYZfA({0-&zEA37=^ z%Itg@Aj7T=?dZ@=O+Ks#7<(`Fwg7BiJYBl~TDsI9p?zgXaHM#$J8D@2^m@D0=s8yk z!nlOh@8FgcQ+hyij#G;4{#CDTR*Z*^Pn0Y!N;rJJ-zFHW;;bV`3Gw?E$ehLr%$mmK z_3nuAZ%dGWJv8(~b;0#UUAeCcz%5>eJVbo_(-@ek&FXqK%JFw4K8D;%Z*RvC?CJ5< zhq=4jE<;P1_n@(V6?UokpP4NJpXe+Y>;eVyTObuyz@c#u*xD! zKaq+H9pJl&+~RI-ZM>0bN|&BrAG6PYurssVemMXSga0P`d}1imIOWi3dnPhv_^)O2 zO@!dQ9w93Q&uJ1_CDgV~SBiVKZtXAz30-HHR$@j;m#@t@?M=+?EN)fUAbn0eTuB+d z_Bbe>UD-DxIX15P9x`^C0y?2NC|U`br1F%qkYvrp0{{I z31Sa-3Ud1&z2W2b)tSKTL3P;k?ehj9Wl>4dMv-Zn_A&#~7GPOQbwpT?A-&D?VGpB& zqL1_-6SiOzw)llprTJsXR8Incmc}F;fPc^`26ThC@QgUi)`-UTA$6P&0)-v>zlE#% zV2o4aNe1YXoYHtmY*OpR=-0B5*Vx>{DLTGjKYr$8zR`6m5U5xb1?q*TcBi4Aw0P##n zu!xS$)eYbLy9oPJFc@=AW6SWqyei%7xnf{@0Xd+QLqHW15;?$DWDqlQ$hBW&`=&V! z?#4J{_^ge2$mQqa6UaPwM?gk!8J6E02hQmbBKgf!7EBVGu^~oEB3bZ`W)!ZJRj~~{ zqIU!6Ze+GPNK}4;iT>zL!7(NDJsDSSmlX8#kk6}&*DH69>kLMe7S%-wUTft>Z@eA+yVOuU>S= zN*7^T--{`${f_rnFw%smzyJA87{EDG5-I@u{|bl{6~}dE^pKrb46h4zjd<=B5m9Mm zVKKdx@}{JxG{}K?*>F()haIL{k44!i@OjI(e>pCG`|wdy&T2%pV>enpH7&at7jcg@ z2*CU5YSBAf#1Zd!i?J(h1Bu&S-ju1I+Wg5=Gk55TyVuuBfFAo^z^A7tZ|*oR!In_S zz-6`FwNcJWxtzQ4%-QiXC3(7M<7SUh&2Cfq^RXE(0r^-R9G_v$rH?b$PPWki(Ep-- zE96O=D6tc0f+y9|TH*y)s%(@r_meYfqjy|*HNSVji zl#+A5;q%f?!zHj35asY{m0a2=EkRDDD><%TWCuQ#AKeDeIv8;@i4zX5C=OX@kevTp zbMSCBgL|}SQYZXEQQVy^l-_5rk9+UtC%;nxi_^L}C`~TEr!=8>87G}|MT$X1zCMSZ z=pA#wfk<#zR);G^xC<%%Asn=nVsK#=>=Cy!sh6_57qSx~fQQf-p9dv2I(e6R|D8Uz zqfh$#B0dhSqthaUcz*)cX>?iQkcy;WR2V!1CX(j&Q==B;#$y%bka%6aQFs{$@p-$Y zx5NYpcoC>BXRS}LsIm`SPMRK~3Vphumn3nN?Ta9mQfpk)x1-9sG$46MJAq^g`1uPH z3DPO09fp7utld#n+c+|&0wBG?@$IpMHy^i<(2CE)E#vFXB=PgX<7=RuDGmA*>97}1qj)dD*e4*C_4eJ_S!na zJViWkF(gn5d&LzSjlG6%*Zm`w`5n#n9x@|wQe9}DZ<+tJ!{V;xTpa$Dy}Ut*{d5D8 z)RLkDffgh*0M7q4I+HhSf`pMnzazWbj%H~8stFmq5C&RcjveXevI6a*2Imo}qtO;X zI$soY=L-Kb-3fl8qr#pm;${HB+mh1h!tQ+1tBu=!urG@jZ!p4&Pk`kWu*GGHoLW2e zviu+!ywu^j=16F0C=}LH@AROpGzCy9C3-g6(2iKfH-2{`h>=b^xA72ADyhA6Lax*x z7JuOx5mdUOy^3__PJ27N*lHejdm_JjI-JhEVBCK(^){tKf$+K-7*Z|`Th1Dh#9LWS zg3+9NKQL*|&gExr`S4((*hG~2*lHW%H=H?ANgir1olgR#prHoAsFN4DQ3J@|$iXQe zS_?ij1sFlD_ah|_w2q-dW#CS_(D3#Yf2JNe}eB_rl>5$@1(cCqdqJL59;ZcI}rUjYeut3UhFw(%{}7bP0PEHbM~0oI(*Q|^fk>8dGXoMkis2oXK60B^=QP1 zKr_JI4@oG?wE5}0Q^DXfV{|$G*=;BDa(?O1>*uq5g=nCcG4w7B1Z*f-9~D|gMjXzg^%G5Hod3KwNnP5C$SG+?(o3?Rl$h+%lxlVEdi+3Y zHiJa*v_9JmQPy(fFnDVq)yshMn)vCfT2DVr^*Flt^;8_VcB=0Obmt}Pi5&?dhEbEE zlY&Jb%7aecHG>b#2ABjIWCb`&?H3esT%an0@G0Y)C~P!Y^$<<~*4)AD z|Ly{tI{*z$NT7jdHs5p8|JuDUNSd%2U`CdB{)A=FlfBiGCB~j7hZOrqY>jEadq>VO z*r1Xn@!8XG)f5G5$DNU0dHYDMuW>%!R0u6(SNqH!sb-5SxAJMh5kZ!%hxQ%*x&o}P ztygCx&|0;RH<}*g{g*2i9xvYOJy-u~IPZ^bssK#Y{(`=#_2>xM@o!#4(&Up%-hkfN zMUA7ys3B5h(oLSzbF1q;X*N)+R4jh0xlga~?Wn1R^xNFxVXW=`c2nq?Q8k z|Dg%Bfc9S>F<|%oul^rnE#g@C9}o5pOVp{W@e|&iOhOt49j1KiDphld5JtX1x{o*v z|Lz*jzfk}^LYipuMc`-%@xG$WPAKZ86>lTM!s){P_=MHaKyFXCbQ_Wt(_m*>{9&a!C`b zf)j*Jo9^yeDy*%>W~|T*CQ!f%l2Qgv6X8Jv?VSPReFjpb0%JLzmv{=2ve^n!5BkPV z{4_Rbm=`bp@&r0K%}MM&oc#O7FUrfP9jZ?!G3c*6TRoQMPbT>^ojYhzMBLe;SJxcF#bi0dOXkS{MKm&2wLralgJQd3C-+T3!yRHG4>S2BO(K`&by>l*-z^rY|>G0VWh(id8aKh|Kv1L6Up zzie*}ef-JxF}YmKc+8GnSLL#ODtdFr5jwB60P;F|?PIbrXEF6?czzu|MKj|gP z0uI3>B%bgH5?$XO&)Z#;l)wFat>n|tTY-A(SaZAb?Ql(j+uq7|z|;rt>^P$;*g4Z~ zi7NJ@-8jBG2|T=?*dYQ$UJFeCdK_{T`BpfT%)f45HV7DV&7WVMbbk?CY!b568dbv$ z4&rrw@IGI)SwEHjY}N(ubB3;*@q5PLFX~+AeB)d<>>#n-!Ve7NYNVKWns3RyI>`|H z8TFVk?-X7I33J?1rLV;a)v8^;+lZ(+bfd$h-NNo)0QPj4&>Oss7uUG$aefnbuSCCVH4Y5Jn+JKCN4%<=2_%c&=_!JV-CYe*(Cf?=s6Iy#xNnQy z^b1jy_-w1Bi8f0%p>(RQMLz%?Iwu`c2ibZzP<;bG$2H|wszP^M1L`?c7L$o8#mn zBH@!Ah#7jz?z)#r*&$Lyv)}q3lQZzU7!?-C>OvxqrIqQ*wg68?bg!Y4AEAyb5v-aZ ztrA!aOmQI*ky_EO?s0B?DoSBbpeRMlj&g=1C7L64W~4nXKj7&xgT4aQFg#lO8BXJ;wCZAlt;KMXZ%o;%Gk;zG zxC)BE^AE*JTNgRG`oqFm0F7!@ zQMOj1b-)t~XlnBU(OobJXn_zvI!p#$aINkjpi^g}blnBrE=fpuF36_)}E!!^oD z$d~zF{v2pebpg;yN7-ZNX72@zwrfg*U!0L#%n3EX{y$|oplr3Rc|Ze5_>N)i<>}q06K`d}7_&CfqF5D^J%%c2o|yI9yfEpA+gjH!OsKAVq*=OD zH~^4C7nkIfuw+<<*TrCIB>DUFFuRIT!c-}vbQuX-SdskZZZj2b4o?eIa*7-KyUNnM zugf`6<9=Kqe$R;C*}66Mi@9;MaDW~O6!$naHZ^fj72nt{sHqv9Z=Hn4JY>AOn0%0y zk6ddgp|e(;HX$~ZGfj$)d@@Rmyi34&98}V@tSF$ET~wAimDG3}(ofYjn|Hks^((ue z5xcTz8b{*Th0b6mwS=+oh70E1dh(s!-SDE2>3Tu#1&^lsA<_Jq=`p$d7jVvlgdh0s zOM(Mnkrf;sMkHZYl?A)x%)m@7{BI6&@7pR_cIJn{n9bh%B<3VmY%l5ZNcW6|LlQj5 z%Jq*;k|XotCtK(ss=~Bt-eQoo(w8f4`ro0D@HE-qF9;GTS+Y5Q^a$)T?{M4K0{xyK zQQ!Dp8?=LctIrJ@;#KWZ)koRktZY*{&cC%2xo6>=E7Iu zlh)B0c3<=3GbUF|g(I(lGLtwf3^utgG%Gvo{nA)^+ykop>^;iKE@9F!tM#0P=tb%@ zp}bqzS1G8i3!Hyx%jDoJGx-E5%W!`AucQ)tk#Ga{rIADalYiwNK;1O(O91c7TZU+u zm_$qp_H(~b9F8BAtS7p=*5WPY6oa%tfbqRLJ9DX!wXfdDyt3fWih684ZR?ym-n(VK zDt-6vlJC^#KPVk&Yf!yF>TE>)yf$npUF!H~5b)dTIWYOq`nSIGbw82|JRW$OaN;-g zn*k^Rk1t)_09>ou7x!d^*V~Hi$cLF%PnVBbMh?RxrcQp{w2_Zpmp9%y+mT9BpD*!3 zOgkR}m-nvNxsgiGmkd4a-C2q=uM}~|{Z*WJMUBa=d{_79)}0dz?!M!dwrl{-p+{x_ zXC?m?KnE#jgOJces0FS617Gl~H8UiO3;LC2u&9RvA?l z!N$!9?ChZnll=sSfF|KzNY&gZ$bqghbKa|VJjEk9cS8UnDE?aF`1hfLvM<5jQ}j1k zCM_!dTI#r{#Jt}xGd^C}U*w^sQdTH4eki)+)FM&h6|u9VDK#Qd zWnR%J_zp;h>3JhN=?aQ~;7?MU%O+WrW_OVpvFdD1nu6t;{0-D*cba(m2p+i?7u^Wd z&&@yd6z^UGg2^|>*^>Ra&lzZ+zJI%tF=Uj&gow%;gN1hJ6Ix6KoyuX^(3egyI}S&E3O5FK6%l;>W=?uaNc$GlB-B7%QL4p4YaN`d!5OYLD%e@Rz( z<4ZICNMB~ClgCuatY3=HryHk^S|jQ&@KOG%mP9%q4^S1m%gfObm(H>f0c0o6We)tV zQbgu|SSpYgk8d1tVQ|rrJ}G@T`ME=doMX0ugh5vCh}~9;f$GxIp&3*`QHs3@b>D+a zzJ4xl;?bEXzEnfzWW-LMokm#X(PAq@K?WAV>r^?)YI0Na=4s2>p>)k>pq4$kmyVXi ziAHBkD(yoaJxD*}(7s%c>JSq@%Tiw@uB5B} zi$SQeoxMx|c~NLl0t1YBBB2BvObCoFdumVp>2V>S+MA+~0)21C#CiYQM*kJ7!o4Hc zHqDJ@-TQB%;rGvVC*GV?gO@j~Akw$b{|4TYF9{V0D-h9>1RvlH8<2>~%)Vu{J`fvQ zZ5BGr8R;_GYjhDxNEt6O^X*z>Y5n&keZIwJ98=(7ow|Q)njD1}zsXn!QC6;3<2I%6 z7kxSI?sr*%^jXEO(9~Od`?^Znz-Q#ZJ91O+&e_Ee*f*-z7Vco*%GYuO$~ZEv?vR3? zKgMVml1d@mrHsw_eBoBHXvpm$SGOuTNiQ!p!KBy;RW(!V4W2d?bwiTSP-W6UbP{S* zL{(~4SlQ2ZzDmx#U+Jjpgzi(aONeyL9RH&=Or6e@x}_t9;zq_0_BU=^mIlg0?_gFS z&fWj*GO|C30_5$lNBG=S_!>+>>N!`fBeE!x;_lp z!M|E?t=HnCCynLAL!?sC<8y!F5RQ~tA)ZRcARbV66yZ}+O_7%YOctrdgI@|~iCFMZ8`CBTj0x{DK8v%w z!%LAM$PK7a!wkA5iU)Ckw+Brm9+cO~t(ZMeek{jTQC%)I^-W2Bv?eI1BfZQ3 zOeP12_GCek$^U+5Lo)U!Hy6w++N^6%?8ALl{ooT)4dWrM-9|angiwp!PFf*Hi!mhU zP%DdJMQ%vAZrNN)Co5PzccUsPr%r#FKvRL8CngFpOYLW}p!H*tJ_4r|`RDlPFY>Mn zuygatwQRNMdh7b*zw)oo|6M?S|DgK?@)>U|9s%S(V*vw57Wn_=os|1*f|-%KkLixu zij%SBd{9Nu`+_d#FI2sw$4($^P)+z>o;h^Z#E{sS9k(;nxtgvrrcZu6TvQ)m|6G*x z(!V&P=>I>3y=7EXU-&jmNy8{9N+{jk9nuIWBApT{-7v(VksKvONlB$aQig7jk#K+? z9m2pMFfaq-z`(=*UGI9|=lS%kbw2E~*52!!d++-?*S=%lCpt?u{!htwYTcaXf&{Mb zM+ujArHH(uaA$JBQP}U6!$06ROG^B#$Jvv+cTa(`qX#`AgnQFzOewJhzZxR9=&nes z43-FsInVbQ!Ct)bb{<7{dlWBHr9Kg`2uw<6tomfW+}w(PA~qFYKGsZ^(k4Rj0Mih{ zpZIJoem%cINeZa3++u(ILK^^u`(vWkKNr1c9scv*#dsz_5a`J=S>2S zsq$XLJvJf>NJi6;gW&B|agQYliG1|)N;w`gBpt^;Za@+O*8IqT4;a;RSiEMyqa%Z1Ze? zqs|LpM4PrfXIO9k=ekqLh5RESMs#tX?p`Q-fG? zdBT&hT}%6jGdb~Jg;8@;!_8}k5xWRc`{Om}dVs?QZ zp4DKckv7!c5?-1LiJm1K)6j!Iv+Hl7rHdZ}mZ%LRxc>!KkXIxm&{b@)e&G43Q2Q$Mow)9>!Z}!UqE}h#}<7*kZfcw=tEW--5HQ6~SL5(Tqwn;KM{;`UUL_8)Gp3$gZ z(SPRBM1KnK7DE(eNTsyN*M^XL9tm*d>J+&k_`QI+4&N%fv{%j^*OAv>Xvn3rN%d^tzJ&0e1%goVxYc+S)}Fh;_zCzrJ)kJ-=-K zw}Uy9y0M*ti3JR~OqLD*;}Ohl-Px(mH$I2Km~RazzuM4~4LND&Vb80&ywm?UyRT{l=WBIk(|@U^p&qQv9LNk)&wLqwVFW zktL0heG#2S(e1$0nYLm-czWNlq$u)wl*!}8%kPiYdfXLmN00TsNS-VkxE+M+9EHkcmMaF zmwgioPBwXU(Th7`HrU|1>t36mMSFZUFQcyHiPQp7gWk5UU(77dGHXc#R#v%U3`z;t z@+?zFDYUEd`__KK3=fl{(&IJKv2`NSfihbQ0@33S2brRb9|jNlG-osQ;8@a=29EiI zm03K&#Ue|W6KehgKQhCv#{06j+eP$h1{0+gG)SSb-%DFR)GR*w+A)E3>Gx)Lp;mt@ z@_>4|(exj$km+Nx+MKI7V0`mxC-B@C74pj#jKYdR4z_r#p zVCCmQB*rVM=jKBp@=(jfSgdM1GbuIe-_EN4^})gEA(}PO^-t=O!&wW@2(%m5ReOh0 zH!GD4^g@tTIh3Fbcxpf0GaxW01rX(;YRB2LLz^qDx2DUM{v3Lu6v8^+gK;)&(l_8^ zl*PaQxFQ?%bYgSOyiRrbs&szuFmk0C!%EmXUiq8Vvgy5Tf>{Yw!sltVRRxAd(FTuR z`xA`E39_UA5j?k&3o6|m37R|bt(VC>Ny8y7;YX!ou+46Z3} zzU#ZN{}Q;{3>BcZkt2RKU9;`ybZ7U})Uv59;?ram+1mXV@-H`3c0zdG9uZRLE&WF- zXWoA|A|*ngH+=k#QJty2^nu*Gnqqu|p&)K^+ zE$6wxm`7!LKEDLOjsB?4=akjzE8S$uR+q4o8}{k+F?4ozk;Frz-*f9xjYnHo#Mi7x z^uhz8pV@YIHp)3Z7FvLfdDVrUR>qhtaOM!dF)f}-bYcB&O~d7ko2vgw&A_RV`Rwto zd7?`%>D|v>&852u?upvVU>^`yQgZuh44#Bu5FIN989DPXy_R$>aI_?=bXrt3-NLmg`UoL^!C2q$~^d zlPWm2DFP+22AGqw&@J2gZ@+mTL~PyZ@`hjUgi_Q^?re^K&UWUv@)JMShgkxlK~=vE z1O=SET1`ZUACqUa1}v3*9De?CM`o!^T>sMxS*8+YrwTrkCt502#az$3Mz_7b8#WAC z7h~e%gg;fn;SXL3Gm-TqmWyTuK9NQTA)+~x;;82#GTlIpS*?MKj>O_&dOC@|8gCfE z-eV&@31NXJ{BZThOsN)!`HWgl`WbF6TsP2XPx~E_?HU!odU9DR2%+F=zhyeazZ;UZL$A0 zsrn-kKQ|&dLhG?u!eY!j3*{=l|Mt7+|1>X`Kaxw}0*!W*C;vTZV}pY=t=Dp+Sf@|h zo(R5Y-@jE?9Bs%~*49(wdHT5OF}jdu%OHy0=RAZ~fPmL(a#M|E&Afqep~aJ7`KAZ& z)z8Xjq?O#Bq{O_7@tRf~A>aHQJO4E1;e9GSJ0xp!6EgPe<2stOfJDOnR~ORd+KmF+ zC-N1ILIZaONb)#j;4B|CPHs=c^Y<}pDf%BMMv4)150jal!J{E7| zg{kjg_@npuUqtw|XeBg!))W@O-epjgXELhH0Vx1f1LFg=wUEXtIL8;yT}Yt)z!Pqj zPREZ%j=Ar!Z%Sx9xhr=ExpSLI{!VJyM=Zjs z^hZ}`;mwc0AazTPPp*u?L}SxqWI6tLbuHg*dI=G(GVAYeKrY1F;d42cZ2yhF@fDXP zOu0S)yiU#Sac89#Eb1KGq*5N#noNa;W0I9~zwaGUOpj-k)%1#*8DAep7cV{H1-Va# zy;ZrsI8$@z>ABcCc^%x7?R>nsbr^34=@ApV&2lINtjh=g?alr9Gkl?R$(P!@8^YHh zYP`!_wO4$stkf@YhCaQtn>ziwymTdGQb<$J?o`i!tJ0vi+UvHY#(dY1*j^$>v7)~()#OI3jKnGR%MOuaWM0V zkCdC|F$PPF?Y<$409gLjXu$5q=5=Za#OBn+b&b+>g~@f`DgUda5FYyfvitKD0JB6s zcheE?=WZsS0Lq=%XJpHbqp8JTVDBa67PplSlere9#QR^LRx zJse&A1>!{tH{dqlYSa9~E`pkV#XFX(-QPK=tU&(o(}tx39qTrZoZ;q8fxl*GSlO=t zsHU9dy#9yZ9~u7r_eLjc{NlYp2H)JI#ZA=p^*EHdWpXaS9&T5_F)iAgce=~T4a5oK zVtALOpBH|&O4t9~Q0yLfJ$J?69H*yorN`d6q;@>1kDR=!`4T}D(bOG*b`2(MF|wb6 z|M_jbb{&P?!45)G|5Q~lEWeOYdo=Rjkv&e6zKJs#;VJjcDeXD(uiH<^6WXB%u225t zFMo%Pls4UGBFI|J@9y~_do{v25(ca$zSR*YbkpSK?5A@R z>`@P$ptH2tpSNEBf%W5ZIyQX@;}RbP{6Zvf{B<+F=vXpQUJM0CM4FfnnjD!^GrKrngu+i@X9e3mDZ$^wuEU)1gs~|t~Mt} zk5yMLw+{{jgFECMJZnSeHr!edKR=_$)_AE?(w@3r%*Hz1Q}+_5b^7E7?MC>!VIFt1 z$Y~=?aqV3&!=B12yU$4ZAF+q#ruZEcarl+P7>LupYYFv}G>kN;v(iA-ok14mZ2jZj zAxnXi+%#HQl|~IEy**ww2)K_XB@7n^_O}5dsYSW+ zPSQzg;=V*IA2EGehGfs)=9?2W;~RLVJz@teTN|K~y^w^cf)qpX+iR)#vR4aP2TOKl zDyZ!z5E!FpnDl?ehcnoHi#2(@uu{b(`<1D4H`(u}&~wd^gsnI=t8?JyOniA;lU^FkUWjM zw;72w`H)HH z|9dQ1roc7Sb}wHY^T{=zM5=72#N~bdGdJFG;WDF4jm&(JEa7FzNh8V0M^Y10hqA*@ zTb{Ok_mX}3*(+t)`@hQNqp7grKjd(#Q13k5+z!2^ezZw!oQan;X!T`H;( z9NLJ=69^K1sR1+;*BKZ`hMIx)a0s-n7D@!7M?MtQ!W>guj%&lol(!nboAT`ljt zO!(~>WJ#kbz4NrCyy&VN=K1`96M+XCOs^BYQVOsu=cU6W1ocytT8*%@37<`|M8As!VPJe!ks9_R2mU#*R<_((~M& z(EV-v#iXx=`&>UCGmh5pP9&OONRIsAX;{^KYo@|~)V44I^@+$$MR-A?PrSCT)XLDT zr##!P-XR(CFUtJ{Ylh0FyF`KNU|;q&z$A;Ydj^Nhv^IQ@Ah)f5beHYNR>fKiz5fxm z&+Hl4q6KW+*^xV&XFQ?;FdPw%HKKG#CekbNo?UNF>Ly*X;pJkksO#5rSGonEIh;T4 zc|^jH>mkt6lUZLJ8Z-1XBZ8?0A%yx(mj}$_9^f8C)D6|W_Kak+YX?e)y!M?VRU%dF zx&4yltk%`nqkXbF0#<8%z99L`h5g#8>U=7FhTHX4Qk8BiPql9^b01v-jXi}u^y`oP z)UFdTg=o9b$)A%>EWnfG3YK-Fj%= z9`!DYT1^=B7iOiVsTPxGa8*Kw)ZMQ-c|}+JZw=>%Q@DyBf*H3*W!h&HXJRWLwZ)YV zLzCQ5gLX)FL>{Vzt{2&c2|(9i!;;nVeV_$V^u3Qzd4M;b6E7R3zjds8el>|!!UBxR z0NxO3v43&mL3d-ycv5`OYpKlIW9DYLJt ztV0*oI0O~}6EuiWsQvo|W&=ywThK)<^@CNwTFNi!uJ>T@ZN%5mZb06p6+;51UwNFd zmSB>(7 zaz#?F>9ZDJuYuihmfflHQSA%h2a%j>=By5o_OMaHmEsiFL! z0h~C_Hljm*FVZ=ZBvMuNd4b1)HHWrCEQD$A+!{XmD{nJ@Yo&b+XNjYXD3FJ&e^)KC zk2bmM9<~#Zuji0%LbsQ`3~xasU|sxFSDYd#q2$Ga(-!NEs_8xVibbc7Rho;Qij4#e z{mU|`g8?Nz{q8Aeav!z_g>keIZSptl--`^z`p<^U>&h?@IPZvzj)O?oNYO|!RTJC# zbok!f#WvN@Z^u|n0(ub3>DQ{_9Vu}eRN|~>|M0glJBr$Yw_fAJLT5n~ox|gL3QTQ7 zdGQFA;z#!G=_9A>5XMhMxup~4-pF| z>04b4OY5>TJ{!YZ-#+?8Nbv_mA!|ln)vat(SCA?~nmaQ6u)jfEYV~b}C zcX|vDnc>*}F^nEJp>r89 z=66YsSFsmN_VTa+***PzB^|-Xe)=kN@l`Ws8~qJSq0jo<8_x|@j544bm9HzVT)0KK zpYsl;pmbpXX0TQ82@abi#E;9NHLb<9G4Z4bKLpy0%}*Ul@b}{;$7cqhgYBgDc*3 zROKws8lc%jUHxFHub`ArW_$A$!)5CRo#QwQ=8zAAU>e*bW$P8Cs8>+lNOE?rquFV= z$IM(Ou%iD}Nl>L~5YvBytd%R-+oIw5dTfJCM+Bf==o^46eT<4Bav#d4jxBu*9Nx)gm9uo- z0-bqVg!_$tGbR^Z5h|oF*zE+BffD#|>GOQJSkCQv0Qm6f>ki%G+`2oCyKvnR$_2f9 z%&pIOQ5RClylKb1|3?J*2JPHk!yS3~4&#j$2@TQ5ai1!N|7zb<;n|-XyPiw!AwCw- z?=5zNf}kYFLi#taUqd+}#nv2@W!9}Y)Yl;(28c%!Mgtv(bwqIkleoJ$r-*@9) zV=-V@YG^L33gd*P$NHks*NZrEoIpf*=xn-8tLvE43e4vG_K}cZVqJq;8VIGK9RO{AX4);hlsHi>v8jv>T=c%H? zBu3Y;R+w#WT5?B`=isS_E{)a7R6-I+EaKm8uG4v z#{?cSYj#41Vy}0OWQG#<*mPH^z%PD1+zcNM=W13vER!3#NWFODqNc3wlfuDp91`V( zzYFDwvg}s-=7J}O%Ge980WdimH3Oei4*KI_xQ&{z52X0+@xq6{5t(cE)OdQn<-<+p z=1wG0!xybliEA`!LaOW9$UOu&SXHct_rrpj@o~DtU5C+zI*0O$VX@=}pA5_-`WnlK zqQN&|YS5)v8C3e`S9nDg;@-zShj-vUvq{_SLvk0@m}T^b&;%^-QoC)B4fp!09xLl+ z)2qvow9dR<^yHS*=}(fjgd&~s_af=8EhF5ymTxE`C9hvZEIhCRbc$2dnAf4Cw>S?t z$=eENRG9Am0vmEjJzid@?Jb3ktfw4r)5F(i&Q312E@f`$p78{}%-nFl`o?0dn8dkt zIS4G>BK=OND}ai`cp%LYsVCpI8VbCi4kt*y$*JxPn=#1P3Y76G+q7u_X5%Lb0ut6H*Uas(5 zcPGH<_m}zA-u-%%7bTJGq~zixy3o2Xiet|SoMO6;OW+kiE{WXeQr4>srN zEQqptJfIx-J8KR^Em2O91b9YOQzEKfpUAs-8dXc8grr)~rnhEfHHm?$#KMm>gV010 zgF<-HOwGn1k8fKg<{tVjR*%9KNbh#QGoL@ezNT35cpXU%WhxSgVa}?BR4nw5>Tkq} zz(?nhoAlf#gZJQkv)d?rIxM;gBiu#200*7&q(}Dj8yAF; zXZuf4cj#EbYdB4CK*R@<(LCz~pus0u?8C<4H9T+DW_yymqk0AB4-St=AhCe7*WXaC z+!K4hF(L!Em{HoU;pvd_=XTIC8C)uD_& z3s#EvdkK9EPRaspz^N5lsAamVrS-a`Bi=7+v<}Php{f1=Xq`lBxpRc|^2t%s1mC7d z@?8u9O#sk3XsCQsj_-0q*mB@G&TSzmgGS2vvLX5+SNaNtd6jd4HPW^?HUyYDV%mXG zYgNvE!=|*ye^twVOR40DuOak%Q1`$ytR2n+o0vJybYCMZb?=0{s`N+-cU0N8Y2LL?!HBB3KgjNuTXXN8Pskksv5W|-;s??-#0(uZ4{^wTq{^Oi@j(rw5NHw z7Z&tcxnkZC&%}T~Y@02!YLUdNDC;+jD<))1UZ3AnA%%Y_F3~l6yZyUFHLu=^tbuB~ zB(9$49@t3|%AQss9p5T|YhQITS^Ufnxkw=1cm#lnR7u>_BV8hc`2uG!_r4>LsJ=&@ z>I*RboDgV!W_)qQvGc>}vhb3;=Q&=XpSNE997iu>6}mVa^cp}xN+j52l=38FXaRft zcs5OKK+>1XDf12%MwnR45+$!=OcM@*XR~Z=Ct1=@bwean)uKxo7VSxXSaod z7OBol+XpZEV|>M-Dn+zO{hMgoMy@}k1%~_aV$p^hl3@3UJHpX5`*tU-zHGwfRsHqZ zpBuAhY1Bv|TKL3+kWB_g7B}v>&(I3l>!36WKN{TvlG$SEp`(`K! zU)BP>V$v!z-hP2>&xi+8yQoz(tHHe$0=ZfDjbUG^d8q{>`P63mqspm~ivhfHk9U*p zgckO`YU$pl$z}jHvj`L<27EFE?l_q3Zi4FpSPKc_4CU5%$CYr6vMteTpK6oSfNU|p z`Tj9wxH_ISZv(Sw-I3A5-~dY9Anjr|&oz@Bc$&?Kb?dm}UDhy!dEKz!147)v-ah02 zGcMTi>6Gpu*D9_z0qj*~A%^?(@cDy5-dpOBS|n=wf_&z!BK!qtPwc|TZv4H?VNb3< z{(eszavxk*y&iijw>`C-Szz&kN-$LsO~3{SC6SArg=4 zJRHK9@3;7r=4~v8Uh!fDy6i;?65UJeDG+NtN&f8iC5OXe1Cu9$ksMKlqYGsS;jSp% zx9ZT8IiYIe6X20D38>|}Xj&O-KfNR8JTm|J?Y9WG!(Rj%)l@NHjT;rnDvhE9m;a3E z`gw-nLxuT1wlz{qK(_mUR!r1rCi#;}ig;ifxNh7>cZ562zvJDP(O~?!NZjN;n6cdB zAmmB!J!W6LJ#_+3!F~vX`YkpmwrR0p9-3Zn*l^24awYbzc7sBWip90;6%E_o)y2a! zD`a@n1`3}6n{0;ah5B|sd{N~o7HnT#LLIBMDUM@{;GVzaQV~O#udAdKZKG`~-E~yT z()Umpus+Q7Y?HIP_)sf?!j>}V5{XY(Kwu)=(8e>s(*G*bkZzaMb%4kOEN#yySDNM|#bdB-A0a}WXI1`B&#m@5A zrD1eqSwV=zN~oE^+ZabTF`LwF3?hK40GdrZX% ze=Qm2AcUQr3N}b}!kHF_I+5%qrQZmuUih1OOCjrI_JeZ2DAt=Q)mL{#t3%#(;q#uO z*BWK!e?Zy-p<4R{7n&dXb<|x*>e>0~86W!@e3YKUXy8T3&jnKl5KJ$B!MdPK`UCl>p4t!x%B#N6%44bumV4AO|8F>$4w^M zQ|+tP?jdp*R(O^KF3HLP4q(NXBM+1-S%V2Ksg- zqI~>37kq$fcCSEq&NX|-1LIqSUG(8iIi9xvRj{P3>Nh+QoIgvAqG~R^{`4)x2E6j? zhbF#N7s%h&E2b#c!2h;5zPs1=&sW0kLJ?o54w1znU$fUkZfist!bX!c@u~+)F0}Q% zU5F1Fkm7*SH9j25%(TH5-KE!%!2XMQ15#p740x6!eIkdIQ;#+wrA0YREoi!V6|;uy zdJX9L99MZ!|73}M!ol%om+opgq9GRdRU}EMq)32rLr_0hVbFprhR3NggSv%L%2qR6 z(|nN)p7{T`st*`7pWY|-=vQnMHHyYK3g7DPFJiV|6n5hGx}50dmn!WMaZ&f9H9i8A z|DRu)YVp2o%u^?+Mb@@B5htO=2W>H4PVS5B!O?6^eAQA$|Kpd=0a9l^+$gpOsHxZ1KQ^5uL0&(jDd2ukm+0a2SU6GJmup@j&}KungZLnH;25 zC{!i28W^>r-_~}Nuh?=ZtPB$C^EjdFCgSLSXbQ<6BRoQ%vbJ;4`~qq!^;_&b}YP zQ&>1pc`(IQ=w9BE5@`H>ntL`(OL0{$)j{$fxNpjZh{p#Q4%4 zq$O^fx=XMo@NHOyQsy?bzCzhFvf9VzZ9WZUv`;eG^a>?gi&HE{5zarubpZzvI)%{c zGGx&4?|;e1++kzB5BVClr-D4YGdveiCyF?g2k-=mM%hCE6ltnkj>HDAdDXuf4vO#0 z;PW90s=fVP*Mi@MVv5aZ6jJY))>PLI`O%B5v~Ig5=tWybKm6XLVvn`1F7o4BHjP!b z^8^(qpOIPW5es!TL*=_~IVg1psO4D?_}6bIBO@+rlSH240K5FvS8*yP%$K)-CT~!| zm)-VO0ki>Mif$sgfgE2(TVlDsAYYXg8oB$rD@9z_1{ei$z{7YH zo0}BtrJe+)IU@vLPpNr5`I5mm|LmROt~mQas3yRsQvK>qPu24eN zO#$R9YmYjkj|&S!4`OQamskP21ONiL$Mr z9t|Q1;$}w``LWOgkye`W*Du3Km&s(B*F=!8#1AkMMvEz_OK5enyH7^%L=>pW2GB2(|Bt9Q+;ew%2XT!eMhQ#@_wtT{oL)Tlo<6t z`m?W@namzNk9Rh2cm#Nk`SWv}^*c{<{z>b17CH5(>{JbS*x%GJvITT7=ITu_QH`{Q;?UYTactic Mode

Congratulations! You’ve written your first proof in tactic mode. If you move your cursor around in the proof, you will see that Lean always displays in the Infoview the tactic state at the point in the proof where the cursor is located. Try clicking on different lines of the proof to see how the tactic state changes over the course of the proof. If you want to try another example, you could try typing in the first example in this chapter. You will learn the most from this book if you continue to type the examples into Lean and see for yourself how the tactic state gets updated as the proof is written.

-

We have now seen four tactics: contrapos, assume, have, and show. If the goal is a conditional statement, the contrapos tactic replaces it with its contrapositive. If h is a given that is a conditional statement, then contrapos at h will replace h with its contrapositive. If the goal is a conditional statement P → Q, you can use the assume tactic to assume the antecedent P, and Lean will set the goal to be the consequent Q. You can use the have tactic to make an inference from your givens, as long as you can justify the inference with a proof. The show tactic is similar, but it is used to infer the goal, thus completing the proof. And we have learned how to use one rule of inference in term mode: modus ponens. In the rest of this book we will learn about other tactics and other term-mode rules.

+

In each step of a tactic-mode proof, we invoke a tactic. In the proofs above, we have used four tactics: contrapos, assume, have, and show. If the goal is a conditional statement, the contrapos tactic replaces it with its contrapositive. If h is a given that is a conditional statement, then contrapos at h will replace h with its contrapositive. If the goal is a conditional statement P → Q, you can use the assume tactic to assume the antecedent P, and Lean will set the goal to be the consequent Q. You can use the have tactic to make an inference from your givens, as long as you can justify the inference with a proof. The show tactic is similar, but it is used to infer the goal, thus completing the proof. And we have learned how to use one rule of inference in term mode: modus ponens. In the rest of this book we will learn about other tactics and other term-mode rules.

Before continuing, it might be useful to summarize how you type statements into Lean. We have already told you how to type the symbols → and ¬, but you will want to know how to type all of the logical connectives. In each case, the command to produce the symbol must be followed by space or tab, but there is also a plain text alternative:

diff --git a/docs/search.json b/docs/search.json index 4d6a184..141d2de 100644 --- a/docs/search.json +++ b/docs/search.json @@ -95,7 +95,7 @@ "href": "IntroLean.html#tactic-mode", "title": "Introduction to Lean", "section": "Tactic Mode", - "text": "Tactic Mode\nFor more complicated proofs, it is easier to use tactic mode. Type the following theorem into Lean; to type the symbol ¬, type \\not, followed again by either space or tab. Alternatively, if you type Not P, Lean will interpret it as meaning ¬P.\ntheorem two_imp (P Q R : Prop)\n (h1 : P → Q) (h2 : Q → ¬R) : R → ¬P :=\nLean is now waiting for you to type a proof in term mode. To switch to tactic mode, type by after :=. We find it helpful to set off a tactic proof from the surrounding text by indenting it with one tab, and also by marking where the proof ends. To do this, leave a blank line after the statement of the theorem, adjust the indenting to one tab, and type done. You will type your proof between the statement of the theorem and the line containing done, so click on the blank line between them to position the cursor there. Lean can be fussy about indenting; it will be important to indent all steps of the proof by the same amount.\nOne of the advantages of tactic mode is that Lean displays, in the Lean Infoview pane, information about the status of the proof as your write it. As soon as you position your cursor on the blank line, Lean displays what it calls the “tactic state” in the Infoview pane. Your screen should look like this:\n\n\ntheorem two_imp (P Q R : Prop)\n (h1 : P → Q) (h2 : Q → ¬R) : R → ¬P := by\n\n **done::\n\n\nP Q R : Prop\nh1 : P → Q\nh2 : Q → ¬R\n⊢ R → ¬P\n\n\nThe red squiggle under done indicates that Lean knows that the proof isn’t done. The tactic state in the Infoview pane is very similar to the lists of givens and goals that are used in HTPI. The hypotheses h1 : P → Q and h2 : Q → ¬R are examples of what are called givens in HTPI. The tactic state above says that P, Q, and R stand for propositions, and then it lists the two givens h1 and h2. The symbol ⊢ in the last line labels the goal, R → ¬P. The tactic state is a valuable tool for guiding you as you are figuring out a proof; whenever you are trying to decide on the next step of a proof, you should look at the tactic state to see what givens you have to work with and what goal you need to prove.\nFrom the givens h1 and h2 it shouldn’t be hard to prove P → ¬R, but the goal is R → ¬P. This suggests that we should prove the contrapositive of the goal. Type contrapos (indented by one tab, to match the indenting of done) to tell Lean that you want to replace the goal with its contrapositive. As soon as you type contrapos, Lean will update the tactic state to reflect the change in the goal. You should now see this:\n\n\ntheorem two_imp (P Q R : Prop)\n (h1 : P → Q) (h2 : Q → ¬R) : R → ¬P := by\n contrapos\n **done::\n\n\nP Q R : Prop\nh1 : P → Q\nh2 : Q → ¬R\n⊢ P → ¬R\n\n\nIf you want to make your proof a little more readable, you could add a comment saying that the goal has been changed to P → ¬R. To prove the new goal, we will assume P and prove ¬R. So type assume h3 : P on a new line (after contrapos, but before done). Once again, the tactic state is immediately updated. Lean adds h3 : P as a new given, and it knows, without having to be told, that the goal should now be ¬R:\n\n\ntheorem two_imp (P Q R : Prop)\n (h1 : P → Q) (h2 : Q → ¬R) : R → ¬P := by\n contrapos --Goal is now P → ¬R\n assume h3 : P\n **done::\n\n\nP Q R : Prop\nh1 : P → Q\nh2 : Q → ¬R\nh3 : P\n⊢ ¬R\n\n\nWe can now use modus ponens to infer Q from h1 : P → Q and h3 : P. As we saw earlier, this means that h1 h3 is a term-mode proof of Q. So on the next line, type have h4 : Q := h1 h3. To make an inference, you need to provide a justification, so := here is followed by the term-mode proof of Q. Usually we will use have to make easy inferences for which we can give simple term-mode proofs. (We’ll see later that it is also possible to use have to make an inference justified by a tactic-mode proof.) Of course, Lean updates the tactic state by adding the new given h4 : Q:\n\n\ntheorem two_imp (P Q R : Prop)\n (h1 : P → Q) (h2 : Q → ¬R) : R → ¬P := by\n contrapos --Goal is now P → ¬R\n assume h3 : P\n have h4 : Q := h1 h3\n **done::\n\n\nP Q R : Prop\nh1 : P → Q\nh2 : Q → ¬R\nh3 : P\nh4 : Q\n⊢ ¬R\n\n\nFinally, to complete the proof, we can infer the goal ¬R from h2 : Q → ¬R and h4 : Q, using the term-mode proof h2 h4. Type show ¬R from h2 h4 to complete the proof. You’ll notice two changes in the display: the red squiggle will disappear from the word done, and the tactic state will say “No goals” to indicate that there is nothing left to prove:\n\n\ntheorem two_imp (P Q R : Prop)\n (h1 : P → Q) (h2 : Q → ¬R) : R → ¬P := by\n contrapos --Goal is now P → ¬R\n assume h3 : P\n have h4 : Q := h1 h3\n show ¬R from h2 h4\n done\n\n\nNo goals\n\n\nCongratulations! You’ve written your first proof in tactic mode. If you move your cursor around in the proof, you will see that Lean always displays in the Infoview the tactic state at the point in the proof where the cursor is located. Try clicking on different lines of the proof to see how the tactic state changes over the course of the proof. If you want to try another example, you could try typing in the first example in this chapter. You will learn the most from this book if you continue to type the examples into Lean and see for yourself how the tactic state gets updated as the proof is written.\nWe have now seen four tactics: contrapos, assume, have, and show. If the goal is a conditional statement, the contrapos tactic replaces it with its contrapositive. If h is a given that is a conditional statement, then contrapos at h will replace h with its contrapositive. If the goal is a conditional statement P → Q, you can use the assume tactic to assume the antecedent P, and Lean will set the goal to be the consequent Q. You can use the have tactic to make an inference from your givens, as long as you can justify the inference with a proof. The show tactic is similar, but it is used to infer the goal, thus completing the proof. And we have learned how to use one rule of inference in term mode: modus ponens. In the rest of this book we will learn about other tactics and other term-mode rules.\nBefore continuing, it might be useful to summarize how you type statements into Lean. We have already told you how to type the symbols → and ¬, but you will want to know how to type all of the logical connectives. In each case, the command to produce the symbol must be followed by space or tab, but there is also a plain text alternative:\n\n\n\n\nSymbol\nHow To Type It\nPlain Text Alternative\n\n\n\n\n¬\n\\not or \\n\nNot\n\n\n∧\n\\and\n/\\\n\n\n∨\n\\or or \\v\n\\/\n\n\n→\n\\to or \\r or \\imp\n->\n\n\n↔︎\n\\iff or \\lr\n<->\n\n\n\n\nLean has conventions that it follows to interpret a logical statement when there are not enough parentheses to indicate how terms are grouped in the statement. For our purposes, the most important of these conventions is that P → Q → R is interpreted as P → (Q → R), not (P → Q) → R. The reason for this is simply that statements of the form P → (Q → R) come up much more often in proofs than statements of the form (P → Q) → R. (Lean also follows this “grouping-to-the-right” convention for ∧ and ∨, although this makes less of a difference, since these connectives are associative.) Of course, when in doubt about how to type a statement, you can always put in extra parentheses to avoid confusion.\nWe will be using tactics to apply several logical equivalences. Here are tactics corresponding to all of the logical laws listed in Chapter 1, as well as one additional law:\n\n\n\n\n\n\n\n\n\n\n\nLogical Law\nTactic\n\nTransformation\n\n\n\n\n\nContrapositive Law\ncontrapos\nP → Q\nis changed to\n¬Q → ¬P\n\n\nDe Morgan’s Laws\ndemorgan\n¬(P ∧ Q)\nis changed to\n¬P ∨ ¬Q\n\n\n\n\n¬(P ∨ Q)\nis changed to\n¬P ∧ ¬Q\n\n\n\n\nP ∧ Q\nis changed to\n¬(¬P ∨ ¬Q)\n\n\n\n\nP ∨ Q\nis changed to\n¬(¬P ∧ ¬Q)\n\n\nConditional Laws\nconditional\nP → Q\nis changed to\n¬P ∨ Q\n\n\n\n\n¬(P → Q)\nis changed to\nP ∧ ¬Q\n\n\n\n\nP ∨ Q\nis changed to\n¬P → Q\n\n\n\n\nP ∧ Q\nis changed to\n¬(P → ¬Q)\n\n\nDouble Negation Law\ndouble_neg\n¬¬P\nis changed to\nP\n\n\nBiconditional Negation Law\nbicond_neg\n¬(P ↔︎ Q)\nis changed to\n¬P ↔︎ Q\n\n\n\n\nP ↔︎ Q\nis changed to\n¬(¬P ↔︎ Q)\n\n\n\n\nAll of these tactics work the same way as the contrapos tactic: by default, the transformation is applied to the goal; to apply it to a given h, add at h after the tactic name." + "text": "Tactic Mode\nFor more complicated proofs, it is easier to use tactic mode. Type the following theorem into Lean; to type the symbol ¬, type \\not, followed again by either space or tab. Alternatively, if you type Not P, Lean will interpret it as meaning ¬P.\ntheorem two_imp (P Q R : Prop)\n (h1 : P → Q) (h2 : Q → ¬R) : R → ¬P :=\nLean is now waiting for you to type a proof in term mode. To switch to tactic mode, type by after :=. We find it helpful to set off a tactic proof from the surrounding text by indenting it with one tab, and also by marking where the proof ends. To do this, leave a blank line after the statement of the theorem, adjust the indenting to one tab, and type done. You will type your proof between the statement of the theorem and the line containing done, so click on the blank line between them to position the cursor there. Lean can be fussy about indenting; it will be important to indent all steps of the proof by the same amount.\nOne of the advantages of tactic mode is that Lean displays, in the Lean Infoview pane, information about the status of the proof as your write it. As soon as you position your cursor on the blank line, Lean displays what it calls the “tactic state” in the Infoview pane. Your screen should look like this:\n\n\ntheorem two_imp (P Q R : Prop)\n (h1 : P → Q) (h2 : Q → ¬R) : R → ¬P := by\n\n **done::\n\n\nP Q R : Prop\nh1 : P → Q\nh2 : Q → ¬R\n⊢ R → ¬P\n\n\nThe red squiggle under done indicates that Lean knows that the proof isn’t done. The tactic state in the Infoview pane is very similar to the lists of givens and goals that are used in HTPI. The hypotheses h1 : P → Q and h2 : Q → ¬R are examples of what are called givens in HTPI. The tactic state above says that P, Q, and R stand for propositions, and then it lists the two givens h1 and h2. The symbol ⊢ in the last line labels the goal, R → ¬P. The tactic state is a valuable tool for guiding you as you are figuring out a proof; whenever you are trying to decide on the next step of a proof, you should look at the tactic state to see what givens you have to work with and what goal you need to prove.\nFrom the givens h1 and h2 it shouldn’t be hard to prove P → ¬R, but the goal is R → ¬P. This suggests that we should prove the contrapositive of the goal. Type contrapos (indented by one tab, to match the indenting of done) to tell Lean that you want to replace the goal with its contrapositive. As soon as you type contrapos, Lean will update the tactic state to reflect the change in the goal. You should now see this:\n\n\ntheorem two_imp (P Q R : Prop)\n (h1 : P → Q) (h2 : Q → ¬R) : R → ¬P := by\n contrapos\n **done::\n\n\nP Q R : Prop\nh1 : P → Q\nh2 : Q → ¬R\n⊢ P → ¬R\n\n\nIf you want to make your proof a little more readable, you could add a comment saying that the goal has been changed to P → ¬R. To prove the new goal, we will assume P and prove ¬R. So type assume h3 : P on a new line (after contrapos, but before done). Once again, the tactic state is immediately updated. Lean adds h3 : P as a new given, and it knows, without having to be told, that the goal should now be ¬R:\n\n\ntheorem two_imp (P Q R : Prop)\n (h1 : P → Q) (h2 : Q → ¬R) : R → ¬P := by\n contrapos --Goal is now P → ¬R\n assume h3 : P\n **done::\n\n\nP Q R : Prop\nh1 : P → Q\nh2 : Q → ¬R\nh3 : P\n⊢ ¬R\n\n\nWe can now use modus ponens to infer Q from h1 : P → Q and h3 : P. As we saw earlier, this means that h1 h3 is a term-mode proof of Q. So on the next line, type have h4 : Q := h1 h3. To make an inference, you need to provide a justification, so := here is followed by the term-mode proof of Q. Usually we will use have to make easy inferences for which we can give simple term-mode proofs. (We’ll see later that it is also possible to use have to make an inference justified by a tactic-mode proof.) Of course, Lean updates the tactic state by adding the new given h4 : Q:\n\n\ntheorem two_imp (P Q R : Prop)\n (h1 : P → Q) (h2 : Q → ¬R) : R → ¬P := by\n contrapos --Goal is now P → ¬R\n assume h3 : P\n have h4 : Q := h1 h3\n **done::\n\n\nP Q R : Prop\nh1 : P → Q\nh2 : Q → ¬R\nh3 : P\nh4 : Q\n⊢ ¬R\n\n\nFinally, to complete the proof, we can infer the goal ¬R from h2 : Q → ¬R and h4 : Q, using the term-mode proof h2 h4. Type show ¬R from h2 h4 to complete the proof. You’ll notice two changes in the display: the red squiggle will disappear from the word done, and the tactic state will say “No goals” to indicate that there is nothing left to prove:\n\n\ntheorem two_imp (P Q R : Prop)\n (h1 : P → Q) (h2 : Q → ¬R) : R → ¬P := by\n contrapos --Goal is now P → ¬R\n assume h3 : P\n have h4 : Q := h1 h3\n show ¬R from h2 h4\n done\n\n\nNo goals\n\n\nCongratulations! You’ve written your first proof in tactic mode. If you move your cursor around in the proof, you will see that Lean always displays in the Infoview the tactic state at the point in the proof where the cursor is located. Try clicking on different lines of the proof to see how the tactic state changes over the course of the proof. If you want to try another example, you could try typing in the first example in this chapter. You will learn the most from this book if you continue to type the examples into Lean and see for yourself how the tactic state gets updated as the proof is written.\nIn each step of a tactic-mode proof, we invoke a tactic. In the proofs above, we have used four tactics: contrapos, assume, have, and show. If the goal is a conditional statement, the contrapos tactic replaces it with its contrapositive. If h is a given that is a conditional statement, then contrapos at h will replace h with its contrapositive. If the goal is a conditional statement P → Q, you can use the assume tactic to assume the antecedent P, and Lean will set the goal to be the consequent Q. You can use the have tactic to make an inference from your givens, as long as you can justify the inference with a proof. The show tactic is similar, but it is used to infer the goal, thus completing the proof. And we have learned how to use one rule of inference in term mode: modus ponens. In the rest of this book we will learn about other tactics and other term-mode rules.\nBefore continuing, it might be useful to summarize how you type statements into Lean. We have already told you how to type the symbols → and ¬, but you will want to know how to type all of the logical connectives. In each case, the command to produce the symbol must be followed by space or tab, but there is also a plain text alternative:\n\n\n\n\nSymbol\nHow To Type It\nPlain Text Alternative\n\n\n\n\n¬\n\\not or \\n\nNot\n\n\n∧\n\\and\n/\\\n\n\n∨\n\\or or \\v\n\\/\n\n\n→\n\\to or \\r or \\imp\n->\n\n\n↔︎\n\\iff or \\lr\n<->\n\n\n\n\nLean has conventions that it follows to interpret a logical statement when there are not enough parentheses to indicate how terms are grouped in the statement. For our purposes, the most important of these conventions is that P → Q → R is interpreted as P → (Q → R), not (P → Q) → R. The reason for this is simply that statements of the form P → (Q → R) come up much more often in proofs than statements of the form (P → Q) → R. (Lean also follows this “grouping-to-the-right” convention for ∧ and ∨, although this makes less of a difference, since these connectives are associative.) Of course, when in doubt about how to type a statement, you can always put in extra parentheses to avoid confusion.\nWe will be using tactics to apply several logical equivalences. Here are tactics corresponding to all of the logical laws listed in Chapter 1, as well as one additional law:\n\n\n\n\n\n\n\n\n\n\n\nLogical Law\nTactic\n\nTransformation\n\n\n\n\n\nContrapositive Law\ncontrapos\nP → Q\nis changed to\n¬Q → ¬P\n\n\nDe Morgan’s Laws\ndemorgan\n¬(P ∧ Q)\nis changed to\n¬P ∨ ¬Q\n\n\n\n\n¬(P ∨ Q)\nis changed to\n¬P ∧ ¬Q\n\n\n\n\nP ∧ Q\nis changed to\n¬(¬P ∨ ¬Q)\n\n\n\n\nP ∨ Q\nis changed to\n¬(¬P ∧ ¬Q)\n\n\nConditional Laws\nconditional\nP → Q\nis changed to\n¬P ∨ Q\n\n\n\n\n¬(P → Q)\nis changed to\nP ∧ ¬Q\n\n\n\n\nP ∨ Q\nis changed to\n¬P → Q\n\n\n\n\nP ∧ Q\nis changed to\n¬(P → ¬Q)\n\n\nDouble Negation Law\ndouble_neg\n¬¬P\nis changed to\nP\n\n\nBiconditional Negation Law\nbicond_neg\n¬(P ↔︎ Q)\nis changed to\n¬P ↔︎ Q\n\n\n\n\nP ↔︎ Q\nis changed to\n¬(¬P ↔︎ Q)\n\n\n\n\nAll of these tactics work the same way as the contrapos tactic: by default, the transformation is applied to the goal; to apply it to a given h, add at h after the tactic name." }, { "objectID": "IntroLean.html#types",