From 0deda3531f4d811efd8215e54b82cdfc5d3f38f2 Mon Sep 17 00:00:00 2001
From: djvelleman <110697570+djvelleman@users.noreply.github.com>
Date: Sat, 28 Dec 2024 17:58:43 -0500
Subject: [PATCH] Suggest obtain for proof by cases

---
 Appendix.qmd                       |   4 ++--
 docs/Appendix.html                 |   4 ++--
 docs/How-To-Prove-It-With-Lean.pdf | Bin 2295515 -> 2295377 bytes
 docs/search.json                   |   2 +-
 4 files changed, 5 insertions(+), 5 deletions(-)

diff --git a/Appendix.qmd b/Appendix.qmd
index 413408f..92efb9c 100644
--- a/Appendix.qmd
+++ b/Appendix.qmd
@@ -67,7 +67,7 @@ We have mostly used these tactics to reexpress negative statements as more usefu
 
 * #### `by_cases on`
 
-If you have `h : P ∨ Q`, then you can break your proof into cases by using the tactic `cases' h with hP hQ`.  In case 1, `h : P ∨ Q` will be replaced by `hP : P`, and in case 2 it will be replaced by `hQ : Q`.  In both cases, you have to prove the original goal.  You may also want to learn about the tactics `cases` and `rcases`.
+If you have `h : P ∨ Q`, then you can break your proof into cases by using the tactic `obtain hP | hQ := h`.  In case 1, `h : P ∨ Q` will be replaced by `hP : P`, and in case 2 it will be replaced by `hQ : Q`.  In both cases, you have to prove the original goal.  You may also want to learn about the tactics `cases` and `rcases`.
 
 * #### `by_induc`, `by_strong_induc`
 
@@ -136,7 +136,7 @@ If your goal is `∃! (x : U), P x` and you think that `a` is the unique value o
 
 * #### `obtain`
 
-There is an `obtain` tactic in standard Lean, but it is slightly different from the one used in this book.  If you have `h : ∃ (x : U), P x`, then the tactic `obtain ⟨u, h1⟩ := h` will introduce both `u : U` and `h1 : P u` into the tactic state.  Note that `u` and `h1` must be enclosed in angle brackets, `⟨ ⟩`.  To enter those brackets, type `\<` and `\>`.
+If you have `h : ∃ (x : U), P x`, then the tactic `obtain ⟨u, h1⟩ := h` will introduce both `u : U` and `h1 : P u` into the tactic state.  Note that `u` and `h1` must be enclosed in angle brackets, `⟨ ⟩`.  To enter those brackets, type `\<` and `\>`.
 
 If you have `h : ∃! (x : U), P x`, then `obtain ⟨u, h1, h2⟩ := h` will also introduce `u : U` and `h1 : P u` into the tactic state.  In addition, it will introduce `h2` as an identifier for a statement that is equivalent to `∀ (y : U), P y → y = u`.  (Unfortunately, the statement introduced is more complicated.)
 
diff --git a/docs/Appendix.html b/docs/Appendix.html
index f702c1b..a56817d 100644
--- a/docs/Appendix.html
+++ b/docs/Appendix.html
@@ -428,7 +428,7 @@ <h2 class="anchored" data-anchor-id="transitioning-to-standard-lean">Transitioni
 <ul>
 <li><h4 id="by_cases-on" class="anchored"><code>by_cases on</code></h4></li>
 </ul>
-<p>If you have <code>h : P ∨ Q</code>, then you can break your proof into cases by using the tactic <code>cases' h with hP hQ</code>. In case 1, <code>h : P ∨ Q</code> will be replaced by <code>hP : P</code>, and in case 2 it will be replaced by <code>hQ : Q</code>. In both cases, you have to prove the original goal. You may also want to learn about the tactics <code>cases</code> and <code>rcases</code>.</p>
+<p>If you have <code>h : P ∨ Q</code>, then you can break your proof into cases by using the tactic <code>obtain hP | hQ := h</code>. In case 1, <code>h : P ∨ Q</code> will be replaced by <code>hP : P</code>, and in case 2 it will be replaced by <code>hQ : Q</code>. In both cases, you have to prove the original goal. You may also want to learn about the tactics <code>cases</code> and <code>rcases</code>.</p>
 <ul>
 <li><h4 id="by_induc-by_strong_induc" class="anchored"><code>by_induc</code>, <code>by_strong_induc</code></h4></li>
 </ul>
@@ -480,7 +480,7 @@ <h2 class="anchored" data-anchor-id="transitioning-to-standard-lean">Transitioni
 <ul>
 <li><h4 id="obtain" class="anchored"><code>obtain</code></h4></li>
 </ul>
-<p>There is an <code>obtain</code> tactic in standard Lean, but it is slightly different from the one used in this book. If you have <code>h : ∃ (x : U), P x</code>, then the tactic <code>obtain ⟨u, h1⟩ := h</code> will introduce both <code>u : U</code> and <code>h1 : P u</code> into the tactic state. Note that <code>u</code> and <code>h1</code> must be enclosed in angle brackets, <code>⟨ ⟩</code>. To enter those brackets, type <code>\&lt;</code> and <code>\&gt;</code>.</p>
+<p>If you have <code>h : ∃ (x : U), P x</code>, then the tactic <code>obtain ⟨u, h1⟩ := h</code> will introduce both <code>u : U</code> and <code>h1 : P u</code> into the tactic state. Note that <code>u</code> and <code>h1</code> must be enclosed in angle brackets, <code>⟨ ⟩</code>. To enter those brackets, type <code>\&lt;</code> and <code>\&gt;</code>.</p>
 <p>If you have <code>h : ∃! (x : U), P x</code>, then <code>obtain ⟨u, h1, h2⟩ := h</code> will also introduce <code>u : U</code> and <code>h1 : P u</code> into the tactic state. In addition, it will introduce <code>h2</code> as an identifier for a statement that is equivalent to <code>∀ (y : U), P y → y = u</code>. (Unfortunately, the statement introduced is more complicated.)</p>
 <p>You may also find the theorems <code>ExistsUnique.exists</code> and <code>ExistsUnique.unique</code> useful:</p>
 <div class="ind">
diff --git a/docs/How-To-Prove-It-With-Lean.pdf b/docs/How-To-Prove-It-With-Lean.pdf
index 5216efea2db616eb6c536505dc3c885754925fd7..c957fb969fd28821886e80128b05c6ecf4e0954e 100644
GIT binary patch
delta 25210
zcmY&<Q*>rQ+iWtiZQGpKwr$(iBzY&v8{3-Lwl%SB+qRQ4|M|{Z=l|}y*V;Gxd8(_c
zs=L>tqd;e)qCkHGL4iMjU_fvn1P~Gk1%w8|0AYb}KzJYm5D|z3L<XV&QGsYcbRY&0
z6Nm-G2I2s5fp|cCAOVmNNYqH|*Z|;W6A*xPb#pN{wukjvYtk8yA?rZcJf`~q)7Q-3
z`n@audjrla)yP8_^U{O2f<EEf5XjV3ZWjBCG6<)jLX9?@6sb(KT;ZF0HL(})lmzmf
zIX~QUdxiAzd4BUey{*vm>99GPQI%$*xP3+S_uOs{=Hp17&#&Wi-!7^P7Y)Go$><nY
z*Bij{WdXl&%Va<Wcs*|E$^N>#+*MN)hb{nLau5K{<FN<lqk2UqQfBb)=tp2ly>J@Y
zb}Cm;(Fop5#W^(*jmk0f%6yxN>7j1wYaeX;LvbB4y!^4c`@?~TCL=K)ILT#Rdu1mI
zvJW<sC8(R@IOkx;_(E?o-T~nIx#V|(@t8_e{7BIODwZWuh^a1MsQ<${`3s9fl>X70
zzEg$(bi;_svnrC1Fp|f_Pd~?%4xvcq*FGex3pq?p;*%Tm+0|9SQeqpBc_nBo&(_H+
ztL<3ierF7`SG|i*$zZG2aDKD%40?{$DoMgi6yGrg<<O})f;v^L{|In*)ayQp=t<5m
zi=fZYl$CVcTalG9)P+@*SU<wYs-^TY2DeiErkN^pEU8o1Yd?70ZUS7Fp)+onY5HN0
zuz2C(xuB>&c{rI35%6Y^AU=V+y04;ZY=;3iE_DMRo*(W#VgsM1uL+r^&LyH{AT={9
zQQ>=a?8uQcS;!Xj;|j3V>Lkvm>w6t?zk89F6zb##%H%iiJ3<}(jLTx(R@sY7@4Pxy
z#deBcnxhQ&)bvb!6aUqTsARNhYb)Nf)ypWL=}D2BnDHjNsBb%t8~vvB*nOwvgeP*y
zOZaP`IEt49Oieus6uV?wR2c)hd`Yfn$p@_nE}>Z2NX=4I*BFrK9QQj6&%njYm;<UC
z5*t?26QP+FkBKC`i_vtEF|^$lilmYgcg-U2%p9UKm=RR;0E81%t^qro6P7hnBA`ry
z*1C+4!gG?alEB{&CoXE!#G3W@E8Er6l%V6)(5oWYDudsk<7nGrcS~Q&;JCo};~1?E
z2n!xZ>ij`)00Q80kD|W~EZ<h#bg=0P6jqego}LaV`XX-`G;G$-e1G94hSmd5$Fl|J
z)pi)$xZNZ)Ki47MQORU8MF_yDA4s$n2hyh$$9YD%d`)Pl@mR#hmG&b~-k^pw3dIAR
zHOrFoYMvF4*uu-B*&J(pe>>hC-}2{93?U{vtS5FcDGVTgeAj>jp$zTW-Up4ewOCOL
z{3Ru2*uh6Akr_7^Btd&L4Q7t2u0S3ezwfe<9~t<E`Dbo&0qN9+bw5iEJ?!pSq{x>~
zjc4q;_p?q<lL$Ssx9EXqy3GT@U5Kf`?{ulLKS<#4=?dE)Qn9RvgrIX)o1GN7Ra>Su
z#`S0YyaoU;8QJ=K9b!tnnSvLd{d=Suy1GQ`_+BjRXST&}F6*^F*Vr-PP=z-miFtia
zPB1yU?HS<agI9)GK*$m<xe8aO0%^cx#0L9_SpAQ{UYGom;v&5UGdB1mF&g!G(l{;~
z)rXrTDd)<+D+Sye;?|;mYx!R0{@UJo2&(id1~!1>$|A|~FEb3Ty@eo?&KCS}xnqk_
z&pjQ<t7~>l%~1vGsco**N-MK7dYTd1P5%~a$C2h4i;SnHWXdq~F$>k@*;Z5aL#aY2
zl+jXbz#Jo@pXA;Kc{TkiyAONftR_rS6Q(nI2=wt*q!aQ1>5Vnvj{lF`XWb}gSm}Af
z9!o&E`~*R1p}QQ7WwU-k&z<5n&8YAtVmBrxXurwBEma?>QE7nDFRh2X+B<4CjlkjA
z^QUSO1F$1F!s<bMA*5K2t8#9{y$D-juZw#)a$u`BmJa%d*k$M+n`Fvkoy1-ap)u8U
zUma3XV%bU8?jO!rEFYI`7ib}^MCvFuYC8ZbXa2xIsJ;etErShJMFohGQ@TIc-n0^m
znMID`cUmjX_7g{c<RNOfsp|hQNUn3h0pYHtMlhh2#s~%|%~+b_YX7KsZR6!fcIn7%
z{wUJhSfpwr0|SHk?WqCZ!$FO~YB_g%q_2TrA8p4|8m+_4*w;#Q<rG>U)hk+Cl3xZG
z3FJpts*}tY=rb64sE*1fywk%&0u48>St*ARWmkn$^053G^noQdZR&VbdwtKiXw$aM
z*-c0I^i9gy93Ik7R~4&HCdRnT^)*;>znH|~dlopO_~hv_x)EW_qLT9<&mUA{pUns@
z7GFdc#ERH}7w*=j*nKIb&(c{upR5PuCuQGIrdKY<-qmY#pKW`dQx+|4Y$y?=uocT(
zB}FeBgnTm9F9@d@r1H@HvQ`;xPkH0`39UQquZEH8`376&C|{|g-#$sbc&hx^LUN5d
zKMC_*3FkG1r&$+N4#K~yXV-XshXhY^<w-|vBwKRcqG{RtSd1=F+C3qzgoX!js21!M
z*PF;3lsgy^XWJ|!5512`G5fMxVw3AjuFReu0}_3efiO{URqtGoFrnh73Z1$J@wLPp
z{z~PdsdcR@*8HV|BqLZaG0AqPn0MHeqZWL=N#aJ{!Yh~Pzs)T-pR5!vRpd<*UUtv!
zkod9HrE<LFqC`^E;Z6XR)#wZm=I)7<p1#HpmhDb-n*6!xV4_{u$(N(}SW0A&{HD9a
z5w$83{%b=yqapZ#%d7Np;%o)UxUD3CQh-+_-gpJ%h#SBL#c1_Lv!mC-M=T%GTp*U%
z^x|D(Y%SjHU`{C@s3KKcv=SI=`_;h<{t#4-G_IwhgN7LBA3cW|nIZ>J-Nd_>|LTn<
zg?1@0LJT7vka{Shchkq|-xx7(iEVXDXk6_SY$;^kSxlydu;I;66R59Ppi3UzysWR+
zN4#<XoLp>}ATuFa97jrL#hwUkhu@3;IQXQEC|px^<vhJ#*sLGkoS&A~(Mh>{{bO-Q
zV(on*+UWsfa#V)2=*$CnX+5MM^0~SC(duFWGJ+}hAq-p3nmkNSCpgTS<r4$BwwpHd
z_kE`z$Ol`X5ZhMZQLY$E#%P7Uy!z7nM*rAA<pPeXGIVXqNu^GN&BuaJfz&{AAw$Z@
z<K~qfIcZ=qL6rFKCWY#ty)(xuQUebnrKN|1boOQ{O$9p&PSGZSC;{GA>h6~f(U|Bv
zev4fhu*PZSBN)g2<wK8f=%q?14Kb8b=K=iZupM~z5rGp|y5TXwmGjmu``o3fu$%9<
zo|$wXoK45T$*_+8K>T`%At!8bHdb(il=#<>r_G`LQ3Kwrt<6{&k)XH(LtAyyuWPI?
zrQxQDu7*CIkm?P<MfbPK-LGpLs`It}w&hJ*4JPqL1ESQjwk>-$6+J-mjf|$&>jT8r
z_V-NW_mbn~Md>v<XATI)RiB03JM*dPzyTjItMq6pIdmCAz<7A75e8?O53k^(4j)Kk
z7E_3zWS*rohBnwGwnWpz2-%(#=tB@O4$8J8h4d<F5tIx7-DbcTY~!4SXZ&+(_`;NX
zy$5gOGKy|O5qgm81SU_wj^YqZ?7Qd5jvwPi4QAk_N<FnM&alVs{*moeKrO8^o1`|;
z6&yu-+ntdAtp>vcvCq?(!cN7x+gQDewZOtIlpTwD9>4c;I$z>+cuk9~D|f?&-yWj&
zg*4aZcT6MI^gR`Zf11Nawqdx<79M%m1-gGEdpS!2`PIjcXEES?{u|_XqOoFX{2e}8
z3sg6;CLDl+jq`tN*2#aG^(QaN);+p+0Gr1vV|2YxAXy#QBw}5f9Hr&pk1c?(zFu?3
zdY1GQh{(5~Ov`#|ds}yTz2Z0D|JSU?f;X2~AMftZ@1f80*WYIUG;7g6&3gTew&Tii
z3hsYPnZ4x*`1NzhAQ}LZ{l#cGva<6R8}JkI>Lqe|)bQ);>v*1M8!7eeDpfkbZA|ut
z8-;?A2?lRUOpjUwX26V?7i^iX`Z5|$(`TD;Dls^o!4?Z`*X_x}d52Dyg^bE`@5set
zOIcRfLNLCjf)CBn>F_k32fGxm7CqI8J$vlkXlERnUz4CV9|QmaJ9`R(_Cp52?6W;W
z>S@a=Kp}RFheJlckDI<ZZO!C5#-dZG{B75{?y=`t!^(E1lNC<D@I0;4FsNsZHyvd9
zWE*&<fTS$Tzy|kikzO@B+zHN`NKx3SrK!ddo79O?{!>;a4+g`bQOiqJ!c5sDYgNc%
zQ(b&Ri<<9t^$_s;$zpa3A5~*POlSyI7qMNr(G&G|5a%ipIklPc6ZH8xW%EKuJ$Y2K
z6cUBoiSnog45mGXx5lq3hBq<S7a3x-^kIK7um)$es=0D`Q+0ZhNMfh$_j#O&T4k$m
zPF0%CG_AG(cm)Kce<XpHE*++S`7(5=G+CA~Mt%ohP6Dt<)y=I=aHwx5I;feb9q~G{
zh~e|-I?Kf?W=(Hj6)H0mzLP@HV?U_yAI(Hqz4#r>S-plomdJN<;g@-BiT7T1=7gY<
zYGrHRpu1mp8^)BmP$~5O=)pc;HKpNukNs92GSPYORpYkanld>6v7(k@QgCJF*;NNe
z+%q<P013Eynn6f{2%g{gyAjzCoYQ4WqGKHWwPO8y^-Ya3WA#~`8v|TD&Tm8JlC-_L
zkOyt@T;;tR7lm_7BZuxRBm5k`nLe)kNc1stQPbzy7)*utWfm+iIL4^FDx?ry_~SA4
z?WP8&SRxd09!04Chqx&O#wGQK#pwkN!KJ*5_cFlJiI;wL_>y!{lOI3gcc#nVco5mf
zc5Z=r<-$ASA28ma?jiK*2@jY3T(;VC4;P}s-Hs2>zFa0ht5e452~m{QBh9X}p`ai$
z?MJ#|?X3ndmHzZJVTQ)3Z%O<;f!qKMg8n^i3C53d40~kk9G^$AZ{Rt>MhXXsc_h)X
z@umk@o3gy6948eID&|08-_UXTO}OiVSk$>IWd^zG2bP)0w~FkP^qRm4wzc@Qw5%1{
zJr&Wi+av%RL&_uImJ|c!Ccd8j*B|opOdzzoD(gL=b7D-qXUfez;O3NK;^W)IcYA6d
zYN#J{8+8@MFl+id_>N(GC+$00glKF>G6Dcl2NC21?_dEgN9}0sB1IYPe@xv)#r$QM
z5^?uuG^qb|4gyah2=<p!<AT&FnFafoNG$cboM*TK=j}E<CW+nU>c~F|W1)t_<_<eK
zk$ytv4|gh@EWzndqw}%En?sD>qQ~j`SnpUo8?@83WJiYhsrSs)%R_|<W4AXtx|Re`
z7{mmAPB0|$Y1G?x%2_ps^a*M~kO8$sxPl9n#^^`qYGrtqT3{?^iFY`L5EmL(s-IFt
z;Nj&kGxw21;Eyj7tW-33#JfR#(gNa{zUp(k+9H>89hd)JPiqMAz3nzc)~@6>`XI>q
ztzP2GZ*jAh!k953Csh}RcP46!ptS-%+bz%GxS`>H&WwW8g*sMyn@LVlCxS&Rf^rYi
z;P!t~(T>;V9;aVc(nzkA^9qYn(<CPOU9s&}z7!o`auBt0!8?6yWh~1|C0N<i7L6LW
zE{TYr$4=2!%HUSi3{yJF_o3(Ee8z)oCS9pWD&IG$C+fIcS3e=ACS{boYxn^yk<4!e
z6j8P0X)+6#98yp%c~xCF*11yOtLj;;aolHhvMWGzCIH0IDMHA!fCB=sF(!+t%i{I)
z3%};%)omNbVLymm>t;7A=akKEqRnOQ13oj1Nmy}<nRB<!yf*bb_a8~><-fFJ8^ZZI
z=-GAK)GQe=DBYG$Y+8z%n<4=?vbI%e{bi%hETIhMM^PIlyscsC0%3~CUkH2%%O1U9
z6&@)ok^3ypF6Kl&HGlNrhF;4am$AoU?9D=APn(%T5Sd8QBtZ~qzCn6BB|j#rmmHbJ
z{)Q>paI~_Na|_0*2teo<hpITA&G*aR>PtnkdxX`FNPDZJ@{<@Wmc#(mMPqB#$^2C<
zkCC$Uo&OalotwRf4(0VF!FJ3ni6MzwMdFag{EiQdiruE4sb$KOz30u3u%84Qi3*<=
zY2TFTr!ejZpQNj`ChIbZUiQpQwNDxjbLe232Dn%XWKrF^aV?GWrH4|yt5(#M;Pnry
z1x7<D1`|c`dk7!WIZA*m;?yrXau5G^6*4{$`VZK|4EEHJQus4#j&E*gclP~#>=DR~
z;?<aXfjHxrc=!^oP?|B~G9SC*nJHm7*V)SApGyi1H9GR=;*5wmZJKnt4Is&Oo&;m-
z?x1xBDBaYNq~wF7+_T($<e5&f5*SFAeKv)NKl7|K&C%AvrVjvgrRs<YcNG1ZB9v@H
z9sErVnd+;xkp)<gITm%3>ikZXC4;A2lZcRhT@G4oG=FB>z_O0-GC{O0g4-z4A^I4%
zdC7QXNuc-8m|Mh&k6c29NDq%us2TYuEkJaZokD=pXI!u%H3O)w$TH)_9JNdYL<^7?
zsCF-ys=#=RVkf{zep<Z)O>w@QxgER<q7vjI9<R@}@=$LYT`x9wcOd`I-@-)ZMi9)l
zO#}fjNi51QL;fhms7F)AevR`&6crFaI}EjxQ)IQ5++CL13s#cfp?~+fp)mPxK>1rJ
zZ_n)GFG;HZ6e2*~xo;@6$Sor^K@%1w8tWSI{?5o2d^QElfnrHy>~woJb`ySbgu>PG
zTUIvkCsY`4ocw&|qwV)B>7j_CfcAG4%?ps;NWykwDZ`zk{=WGE73|*~?4JNZVH-+M
ztzGINt7tn-!C*G}vG68~*=TKwmekxfm>6_poD3n&5?-@0FzpW`5<9XIW&>kE@idX0
zU6&+>9_<6@P}a&&EU%Qgg}AR$9xWA`<>eBfH>BG#999*41YRBuEAcJg-^3f~q$8S(
zeq8;IO>7nkE(i-)iEA)!>}sSl<*c`w_6OIL5%=E@-Ga=YhjRxKs_k4FB%lp0W{N(`
zYBVe+Dq+-5DetaVUPq2vKlm*)B@|J?UHZh76$Jz8yDTVh_q6VN#Q1zYuN*F^uhFq`
zoVHE9y3#!AFS~&gVgtj}0Y+oE&@Qq&zpqg35DXI5U;&Tp7$6J(Bq`I^Op6)>_tGIc
zhD|z`l&>F*ovUXS%CKs)9utzxG;RjuV}9lDU*e#7?*-GV$1YFM!o}vnWx;Q?Ng9VI
zly88X#p9(LFu%{asGj6n2UNqBNZlE-T7O}rhBW^i8LQ8kdFI!A7N4Np^D~kCzl&Pb
zrtHo6n-F6*(K{Te3r2+oJys-BH8Um$AQnZvv;iK6x!VE{{Vt}yH*zF!`!RzSTj+%M
z3Y%X<`H-oA^UsBzkE?AqI`3Ura|g43Noi`@9X@=E(*kj8BtYJ=fEiin`U93ox2oI-
z-h)g${!Y1Z)}dpucrhD>i$(=3EKc<6GjQ7uDKbe4X(;;`XT4$4p~Ln}c+%j#dE;G}
z;Jo<kv#9H-ND~TBo+(9DUOp~N{gHZ{A8C<!od1hv%3#u<`};M%$N&AclPM!IhG^;1
z^6};?#kPVL03g4+T=GtazHWYBH@`X7cePtIL7`!P=U4E>dCP3qRln@rR=oCqOujxp
zD!kg_e7~^(T(&C$o+fkmtlHq`try0c?^3I&{S4Wth#2;6wadi?1ja`=7XjN<rYpNz
z{^+0R)yt+{_$59#R%j!z_FxnoN(sp6LLpLl7~AjzfIk{x+>@{g+?+FL`zq9y_-1U|
ztYH@#VHZaz^<sP0`0*mKVq>k`<TwLs!X^yl774-=xoj2)x>9_{abB=R$hJhOsHDrt
zOB&GUN$rJNx+J$rzI!xc?(<Y(XF4QHMoy!(3a-$$bik&(Yn(*_C~y-51?UDKJdQ<r
zRR07FK)E4`z-06aIFel_O23+g{0i?^yD%{$FZ&errQLoCbYfwJW0bg4E{f7ODoY6Z
zlNR3_j<cGT1|v<e0ul4YU4G8&>b5p2P++0ZZt{HzM=+(0dcIS>oOawR<hTlRK4X}r
zOM1M^HQttm_~eG?r!R5XbUl1dqNlyPmwpw7+<t4=qO<HVUwZQnch*grlbYvCf}Sd6
zLP8DtGu7FI1RJoz5;4?V9{`=zEUML_qB}%5f8Z8?E4mQs|DOKm!59kW<LV2G@f+^G
zp1KK_m~Tx%jZ3Jiv2n$-00UanE(uW!UM1X^5)he^Nj!nH;d_TkLciUEG@NrB+h1ne
zW^sE5ob=lF@aDeO{()+%l5-77lHEpM{!7qE_pCjL4FLesS0?`$)YWf7*Fh)Hwvn1_
zmF!^TJW7{SCSmHZl21qsTR$N<Y{fS#eSv^w)#kt~RY1ck^{i?JYV%q%MQYQrw3n(&
zW%)`Tn-4UP*~=<<T$`sYUK^VCDb~!#plK0fQX3E73WLoLv^usH9ZREL{k2B!zv4~H
z*?j+Q+=7E$l_hYUx@Yf>NF5#9l|I$V2>1fg@r?rePpKMANvHuV|J%;#Co4zpF{1}>
ze`5G;nBz3cCsK#yE(S6;bVU7p-zuBM7}6;hnCRK&*fxf2&b^^%YdhZ9DBd^e*y1SB
zW&PUJKhtle2vu#k?t65(K8x!N-Y>%`(ykX=<W&BsnO5h;#Zpv%Z{P_v`}lY%@udau
z2>|#Fr_>V_2($ZdzYN@wYM9K=68yMo-wq29q$#(mJ&Bfexg0b5DblAUrF#^6ULTkI
z$hTA8$8}!>qCU@_@_5;Y57uq#BFQ>_t#^mIS~-lGHEIo9svIn)`n5Kz6SS9ehs^rU
z2}YV3JWZRRXM6(g8~)U`h<>)5g&dxi8v+E<4^Bx{P)5U-;#sk1GKFNR$ryv+o%1PN
zAxVSK;(M*I%&Bt`oVnFdq0*DM;o>*LM;wad%oX{tCGiQPs1(>J6gnn|4-=t~MuVUi
zEx@Fk>SfuJDlBZJ2rc6H!fxVJQ@g>P6@Uf45W6GcPD!f0_>v0bNMnphq*ElrqJS7O
zs=oMmR($h6IfKfA*f5d`Kr+!ohM2eCQe1bWSt#oDTw^1aw{dxcd%ZS_d|vTB(yO!9
zr^2BMOd=(NL82vCWxq;GL`!xH33w1b_X-nz5wlYKo!w%w^46%q%A*@|*XG<~#(tqB
zw~P@>nmxOaCy=@MaHE#psV!IBkpl3wZ7!V;#2*rh&iTGNr5vG-k5heO1-2;!z34Uj
zKMP`>&TH6lSAC;r@+yp%>9ds6O-6DMG-b&*9B&$nZN^(wGZeH>bJYvkLSd<w1oZP7
z%?@!xD_#%_i;T@d595yL*@E%eB2&v9rgwb^y5Vwig5S2>KPd<V32)zs98k_w(FA&!
zE{h2A_pXU@cic_>gH1mR5-I=}^M8ReN!NB=2w7tLk?x752wdNj6O_!!tfQ6OIy|v^
zd~OY6AR+D$>ib>h7bFyI?e4|YVJ1#=pGn7B^JHn?wy5UiMk%7aF4EP8e#lr^7cYlB
zGF7=lx$?-jW=TC#-(Jy$;dr9z?%U&VPR{gpj^S22Ky`I!_S1u2F!Std-wzE>y#s9M
zdU>l%%&TKff4YFzeqFQ#Gg7GR#y-N2FtnmwcWHCWFLT--p$RYJsq{)9B1>>p|Lto&
zOOLmldc>88Q9^%l@#-H9;Eg?<1d6lqx9QjwQz7Z;etXuiJG_fNw%}XbzgV-z=F?B{
zV`Revk_wf6Fx1JBd_*DppQ7q`XCU%d-HzuX_$%SMmgE6>N&2$_=siV{4$#IWrA#7N
z;iR9Sr0PYrfm0adI)o&%q)EaHsd*E8!qnrX9HQwc3E9$+%9LWM6SyLlG6K<<4FNL=
ztQeDOZs2(nu-3Hs0?|`qCi(OvITDc+#d&CsDbjfLwidP{4#8phr%ieH8eul7b>yP7
zEM-fqEOf7F#mVq;6EflpMrBf}K}Do=K+JKq%1#KkKE^}8wyvKZkM5*j=QW9aHIWyC
zom}^Q+fQBX@coVcUllu8zqWdd-CK|(w;vl)zdykk6rer+)A?Mhf2_pu-;I~I?PrD$
zxqihEaEOXmT&GJCT4GabXIi_e-JBD<{1J_|@h}7E8K^li3IHcuPcV?y_!y)$Ot(P(
z3cW06K-il}Tbpa^Scw?Oj)}hQlUk5xXKr&`OzApiG8q4=vXg!>+|GRTdA+%7KV6%f
zAmjwNb^eige`%u=p|IiExw%?P3`^5|eexkJ)lV0tI&xKn2C&&q1$9MqR9-!~308Hj
zXV{s>>|MFmxznx7Zs(Lz{0#dmt9r}`Y%i}k-AKh)ox>l^gxXJx@MaMxlPvyfVZxYr
z3Oy@noWH&C<|71`PUF$xQpu%;6wigHGDQYlprc*v!6*GAOacbu)Zefx0ei^5P|=NJ
zrGwC|LZI!2b=bn1n4LSRkcYu2@EsxdyyQkWgb~C0wthnEpqjC@d;F5Cq=2f!q*N1O
z5LUt@%LZbq|IVe5IHYJC0ZHPTlM5s4ErG2KC8T*tI*ABWoCHRZ4yfLcDk}z`*-!$^
z&>IL?Be;L?FwBw#f3Tt5CE|l7r=H|kWXV;+6U_f1@?qm~^(ajUv6%!4NIgj1X9?-M
z4Lu)vSh{_+{CLMd`zdM6qRySc*i`_Y)X}>OlP+O}`?-FgiDf%1?Dh@Cxi`<o5#rDj
z*L_Y!_x$z4ff-Kw|4F?6ISfy&^d*5wov`_bgrEO~gv3dker9CgwLdI@uFOr(f)I0|
zv>v=XUdGW}CYhs(C<ERg_rWEdZ8N``QGdxMLDg`DlX?~1d<^Nvs=>82ddU)73ghRZ
z4XPwh3uPGEY@?6ao#W=BC~|f4<Bg6ddEfN$=2h)4uhs5n{eSVXO(md5m!H=+sSX_>
zEAHJHPl|kE@t+BZT2Mb)h#VwECiV54OP$>s*sMQ|brZboS`D$Yo!YyqU3<^^bjR*4
zBl{UaO%2P0RlvQ;>4sw?-^^hNiy5yQtd-<|0h)ef$d^pboBg0^U-IxWS|q8AiIuI9
zO-`*%ni3dClOC7OC=9SwbeNxqbjK+bBcP5(85f2zk%J`{_RaoLcSIJ(E{tP4C0sfB
z04-vPV_PkJqT|4Kh@vKg%toPlHd^F0#zzw;mL(%pI=-7A#uNe5b>P&;eqt(j!*eL-
zR=g9rhqe=GBL9-#ip7<;V-(Yq&v9{l{XAUc#w(3J{poarE=OX@D*wFgbY9Wqu=0U%
zW6CG5XM1v;0{_XZ{(1~0gF27&pH*9E_peu6|JAD`L)!`=<iYJv^!F86n)d1`4rHJh
z9m2*JNwbq-w1Wysbv+Bx>yzfQ+`CfmUq#C&{9`lD3D3bPk3{J0%^5Wd)ZwY-DZP*i
z+bFIyRZB3O$Yxtg%J21uM{MA$EPwY>7s~Gade8Ca*Vpy9|B0<GAj_6_^u*XvVcGSP
zP(V;dI-gy#(RV|F%;ZR4d6O~m)boie?2!kV^v`<x_<_To!#pC?y`}flk<LEPFI3MQ
z@53CmWoN$3trcl8;gr`yay|}GTSn7OY|ZsVn59`?a})h3O-$_dFCRseHN@eg3J=+~
zjj2QBq>%~LtMD{ffFg@`gsIvPaj;A=!WIqk5;<jM8AmRa8f7kOGBL$1BZP2lT5buU
zFi?g|6*pNfw)CJIBMf7u1hP(%^65t~d0z__u}AZdx}U}1!0XJ(_b~?OsRVp*%Ygv{
zt$;3OV~bHVXl`Wc;D$o*UL2O*bP<0V3l2`Nf2$XqiKPYxz(n)h8)?y}r$R2Tv@EBj
z7|$lG|5I4exE<I=Z6@|_4ogDz@6!m)0IWfuG}#C{7}r_i$*J7jSKIjFp>J_A76kX`
z0XD_dZnR{7tbzCk!~;x!nVxF;xRa%0a#@kXF-MLq_3>t1#OR!#1#LW>js}4G7gOWa
z-Yj;(&}mq%DB0AWZ!p11tW*|dOtjPk2NGHU`+tEVc|B&089C(IJ3_CyTw^8Xk{ngU
z<w8vSta-8i9c0yLMM^eIq;;jmkrfaDN-nhRh4}r_+KAU;ok^neb*cEcgf!c2?b#)m
z!{~Qe;0dr=gTR`tE(=XRX%W!)cl{uz;>y$gVYYrFN$@_EsHZ&78jz#NyWKLqcys%(
zhm<;94)FQK&=%w2ADgyZGbL$q6us`B1qIk>d{=GMVaT`Q4q-pe`;O>N-#py}<k$h;
zSZwDB^Bo;MWK%AS&ILYaTSNyi&)JLik+ow{r}Wj|yKRvC>rD173980!8w_4No|y$W
zq>QiM-wMt~^`ox#0ZfKy=DFx*LO3IVE^%Pmq}Aaj5HdozYQOPI!7;>OxzP^PZsc~-
z<+Q=kGH}x|3?D=N<Ktvcgtu0{YFIzZd=&zSKbfKGvKHs@2L>ydDQPjJ<jA#QO~lLv
z5@bye?f&$tfJb&MP7=9~Cq#^~!lB$LP{tCu(PsRM`!iSu0V4d;ba}1qI%@Edh?p>u
z2$*29Bb9O5k-Yke6o{BQmdW6eK#F9N*pS0wA6VHpE&j=?@=)!>*oI<khENj{ktuyv
z+#TU&dgeHjzyA^z1+~56)(%~eS1&Ep(GrHypE_S+u*mk&V$-H<+Ue1bh$<F`lftYl
z_IABAQ^X~;09bUi-4pC|)M(xWYDqoVzAX=!cv=?7If(e&G8V|}5RS0A5mwteOfw-w
zo!kl15^+qZtREPEK!hVj`6cd6U?D~HKouoE58(-{A;*N=Zd?NBbpn<2$rNn!)q;+E
z)c6&Td~l%o2Nvud(Dg~Vx>JPVj)@`ix3cooccb|9C1aWnVGD(BCfG*;q~Nd$*D!7h
zD}W8YSAHs!-YYMMg~WFEr`g%r>F0E+hHw6zm!}N*o@VWLnM;QMz_cK*{O}32?oo34
zKQxDtdf-e#1<H~N??OTZaDo9}vu8Vn;%ZL7#athmA_4TQAn;!p;qZ4+ot7bAmNij|
z+=?o=V;i$+ph338iC{airX)+wNDT6iD^Jcfi0Bo5C;Swd<rLAIu0bDCx@*zhP9n;6
z_EmaYB*TC1<af6X<7)A6Q&NY|ZFL|JEyO^~Swnb9sCAr^8d7jlZ4GB6+uZwPnzABu
z(pYZOe_fI0j_#EWCcgw$?sbNgTib+ad{<mX7^`_oSNbT*O|>vNd$N@!^px;7A=|s&
zqtq9$ZD{#!jq>KGy?%l+klT0t=O@uzN!S6*-2Z#sGAQXvp@X7lX=`S>{hWs<Bf3}D
z&I?z=6$hfmOB)B~0Xr`H^?jqRF8Y-{{jR3=r!K~wTTqGUGWb*2l$FRPV&7<g<c&~M
z-xT;$q}2&qX|_X64R;+ITyaz9YmiY#6fYZ8l$N%6ugPSLBs7FinFF}N;$y9mxv`S(
z)m#izY9uI#)EmY!^&V5RQV#gQh5hkmZk~f+wkD*Ug#V~jq)VYj7}UF~BikbuBsU`4
zw~op*?p0ChIkxabk^ATLRYY@Sg<JJ0p26KF+}*i)MT<KwX(M<g7s)$T6R*)!6ph-g
zXD**Tfcs}LbMU%z6aXIOL<}{6hW6II&urul><L3J#-g(TFlVTi{p%!RT8uzaS~s#!
zCfit<*-~E<+WY5=r^ZJ1^Q`z=Jne{$&LB%e7PT$wN{(e-JRvB;o15&oC-Gq(`aT`E
z!_~KsI~O~OW>UspS$K(6<tLP*5<fSA)IN}YR{Z{YHs(&wIsmLs`Ig#pIlDF91f<Bh
zUBE9Pg}G^#DI}N)dHP`khVIYWZkBI*Yu5|@k3e}F^$PN2bUJISWHX&yzo_5lmxw?<
z<FMZ+NJx?)WF}ms5qT&8WMAT&z#XKc8$M_lCjkv3Z$vF8;pe!Ho{s6uE6+#wU-~;k
z_2?(~r`|JIxqu+IxKmGr*0;^UF_a>;S?YI?3Y$NA)F8^pV7qaWW@3LWvgM)_pTpDw
zz(%&V7|Ts(5VN#4JDwC@RY;_CVAfM&6a^+>T#ccJ!E`VT6&a!!rW6K`mL)Vv2;+Gz
z0CG^B!j4A1CJ)AD*l2qY0+b2;uU6UN-=m<z+#4RL4I0NwDyJ(nr9jr<R|&Zc6_18c
zBjk{mX+U#fRIH(7`wzt0fRuLI(juObCylYaMtIcUMe7B;JW`{I>V|1E7f9AB-tszZ
z>=~Gk)7FSmf=J(BU2sB4{{c9&2MGs2**1t7dHA0?@!r4|kJivd&Rc|yaX+^i&z?WH
z0A>KKh~6$s+Gau_NIzV@J3hMp7%rGIbi}_v6?lP>S@Y7s!=E{D#lh+Eo(3m{#l*&3
zq(002@~^XeOMDdiczeHb^#{DK5UEd_VbeFCQDPpeVo-_+Mb6EOg5|}W*Lwrt$sU^Q
zFh*Hpk-xdr2_^1{neg%$Z+LS2a6pR_HSb&)aevKiG<6FjxsV5>9yjZSZMC8@TMhLx
zdqXh66(=WFW@uampnvZz6zS`HjZe^*tV{p%5lOmh+7YI*D1$4g*5))WjS?<nu*r0?
z&SC0HQq>V;o`&ISq?hyzEKJH}am-Ax@i!i4Nf1Ly>EJ0U5$LA$;(eVIZ*nv4XI4Qn
zAJ5=f;#w5$Q>bnNO>>WS4rhF@)6zShro|<7_a;Ps{y7SLu7!<rt|^;<L8LOB|I~KO
zlY}aD)0YGZ@PAEP*SqG)3X6=u&=4XCvkEKgk~`b!RZNvx$Q#%{rM}JNA&P`Hl6(A2
z&QGE4Y87=C=bMPZ;DenM4@}IGCVt?e?XSl#MD?%Oqhs@=FN@jmbB>O46TB{Y+rPc{
zYR<@9{=^x69kT|Uo?SqYBXYX5Z~=WQGDSP&2m$V<kZ|I?APMTll!|Z{TZNamBt}#T
zQe#oI9cuPsYpZQ^Hf)3{8Yy-99_tEP;feb{!ZT5{<ExcLlxvh(+3vQ#i_f5L$7yPF
z?vt~M6}8PAy=EYKJUdJ%bxMW{#0-rg%y0ZTE%lWKKfpXf{?++E5%vH0mwzM2)LLH>
z$W#dLe>ui~U77Gp(Y3{sMh^ZLV;r#<!<<!jPrzgM>h)^7tg0t?YTNvRc#?`L`j=y5
z36$*Z{H^{QqNuO$r=TuxyR>N!;3Z%hd^`7DbDS?~6;uf2=Fh3V7r^j5-Q}vPL=WBn
z$_IYGmuz}BT?t%H<#;NVX#qaY0mDzzx3RIy!~0kB);xYMy!?7Zp7){G+Y)$@qV1Ls
zEvc@wVz15H-F${~^OtS_S_cOW@j8QMf*huM+1qOFKUZ__ADgMKaYy?PN}cap_P3Ky
zJ_3TpC2abz4QqCBQz~0uZc_i8lfY!hDM^*X#N8@7=l<Pl<(%7#J-?R&prd2^yCD<h
zD)r{DXVc6jhP*KQK**omTWMhgq#RcTd@)2V5LdQbs4C7zspK73spi-{S6T5yn!$R+
zELtLlcsU>tlwmlK-kP{K9^nCbXCy@pb7w?@9VW)EAMFSJYBOnX{ADS<8u=!aWOGRY
zh@^>^4-oTq11nEF5VcVXP<RH-pmK`aC?$K1qEl!(Oxif|S4Yw+UU@lpQ2Q+sLAt4t
zIIky6hqp>atV)08UdgsZJ)*S9_N4jW6i+H;;19(Ica<0nz`-m9^{dmENap2UfoymB
z*CY%;z{y}NqOhbtCw4)*FUQfP@KSqvj<m$Kfz`I+LQ!sWFK-5L+9H?(;pb6FJRvh_
zz*R7-*Yb4P&;YNK4NDVRX`h#^7UY&;Mm(G6M!q!4PQKLFl$()-C2PX4A(da<Og`Ji
zEIUoV_qCkI$-?^pIVS(Ol=pq<Q7imT&Lyao^{W+{(WMH?yBsEJp;}seZX}~{(?Oc&
z=L9PEWPq*DFnBd!@x)l4TWLLx&&miB1+_$5sbuM7(pX4?3Ysv4mJSW&0RKjBTm=*L
zjRuT|3!VX5v7TTkB7TK4W@8y9oSRp_LRfu@2J*SLz6LV<shy&(!%sTjW;wBy2{%Du
z0%VSN-Mug&K0qw1Rh>K*yYpOND<k@9{#{{NjjF-xXrK^}VL&DgdX5l=jAcAhxB9VC
zjEvk(j-HMsuKp}lz?TGD_VNxnqKbhg4!97<R!^2E$C_)ECvF^w8C~RP_kKRBU;3-a
zkn*m^!C&9YPj|)e*!%Tzh!<iD_73UAS*E6j;CP<<x^KH@>h}lK|FDocz%)s3=negc
z{+f`{W_$4`$gl>hsGqPi;oWoO=1eGz*~~3>LQFzAH=BgF)RdWcB%zNv`K}ceDl`G&
zSS>wN8PKre1$L4^wj9mVP>+mU@Hp1g&-as0zw*eUrE7<IliS{LnP)v<;7hoB3X#O{
z{AgyXKyou}OGKIZw^@9d#q2zMW>+IYH~2*+c>*h#or5}FyobwG3~qF2QnI;SDt|MY
z#@<P*(4K{mMxkty(t>OfeDue2PkFn+hYRe*v#)W<sV?R!9idzA^?Y?&Sjy=w^{l3r
zFplrmq&Ais%QuKxp-aVo8284HL>|%&;r8)qxkc2UL>Cm4Cp8B^!Vh5iFA1lgv>CC^
zj2wLZiQc|ZL|-RSZzl@Pr2tQ}*-YLsqdTloA2PrZ;~L*m!zQV}hD-WV`O3SWPCvG3
zvFzEP_3<a<$jH+9?9HRTWmkY*1OKw^oJ>0ZGJ_jAXR?W~K>SrFcKf^nBhoSS)8YGk
zeEGcyP+=JA@1>2D`gHhNl_1gh1U}y~Yy|<aWsexUZdcRs#TItRifU5l8Si-ifUGFa
zi+|Ywcs8}UTzIs+eJ~(=ncNkK!TQzoNxx^+wC9A{#4c*<Xu7#lb~VkRGjydLZhn}p
zZub7v^UHk4gO8o)ao}hzy+gH{j|PHt2C^^>;07@#rwz&~w}{*LNUlDbG$6+VAw7dR
zfMb>tgj$Tcnh1}6<)Vn*KkbA*SIdSUoFJq}g>&#zkIH;E=I0EqJ8pG`jFl&1b~8&@
zgDS=qS4RS>+HVmCTS}2sxl#0obOcq@J7+^R+<Y}Th=-yLiY5giRA3s-xhmcRkGWqt
zKqM*Y@f6#T!rV_Ml)6%?gYu_&ZXDBbFEkqQ_k?H~k#sr|H4Ud-m09gjm)iGK?1C}k
zNQEb`UA;G{;Q4@kRIC6?dJx^F03K*}(8186eiTOi<g*!WO)EqBbtje-$TlKLl3sKZ
znJ%*pm%tq$6ZfUtWr*Cfl%u=3Q8HSEg>x;yRJ+|&-I4=9+GqA*`uc<nk3wKc%>(>%
zG7y3PHm3g$*ObN`fXwin$8^3M<>ex!YiJ@ON{!qzSRF*jsG?-a<gmMcw^Pk#34LlQ
zVlC}rttasu+(6z=t1ejnmPX&Tt}My|L8<Ja$AztNVrb2|;Uuj#VV)T+z<mTbKQ7Pf
z&MRWf6_;hl4TN{S3iLQa<A?z4j&JrbT&_QLs9}Ey^*o2m-r)VAHHY#ITM5-XX-eO5
zt9l1MRJitV6~M&B*URm%TvA$NFe*qr^vOv@(9`8vttaFvfBS@*U?0Zb@ZNh{9x-9a
zZh%FXpIkdAR&QPZnnz10Xw}2({2tZDQm6R>Nsh8-`~UlNY6XA<E|o2aL=N))#_84#
zp(P}U<R>UN3!KZpBeH*03Y`Ozw9ElXXH)>A&7T52`8@>4W6oVfn$R?SKj6(q$l?ER
z`+f9^!i&MOa4N)v007J7XZ7osS38tq?NTx0k6KN(*G-<6XZ7(qt1@ajrAiRG(p4rH
z1cJjdkm0aZbT}9`jg?8ymAA>T0qmtuR!b5ZJlIQNW33~*&Gp#fxT@UJMy7NnVU+;=
zLyCC$%1)V)ZrH#P4NYN6GhOlc5U8-k3||cX%&5{rr$39JV&t>TJxS6WPs!R`^g^$|
zyoMPasVMe@I~-MMI&@sVA)QhGIHfggt<VItvK&zw+$GRyxN#o0TNEW85N_yEo^m>_
zCE-A1?o45t5b~UA^t{GerF^wNWc7eT?ojn)l?Yd{$b=*O8Q@%m>p<AQ5oVQy2_o1c
zbpcnXdvd)>9im2E#CdJ8ih>f9M(zPk00J{1Zmn;|Y!UZwd^;7GxS)M}L^4t=dG<0Z
z?oe6T9ekW@fDuS^Q$3=-Tm28vC`FasSaujBG;a7rNK~sDDby7yC@W3e2mmJf>G2G1
zp8kTcyt0bsl)41@WuQuk(i}Ll9JmZp2M#vS9kWOZeMgw^sb4aPq7IP)7l*o-mC_n3
zl10OZ5o1KbXf|a85mG#ns*J8Qd9Lp_$31joJ*`vrNIMYGur8t^6{HTaQDjtYNwkO>
zB5u0@k<tY+Klgz4m?n0h51<bpPoe59zn6#`Kpx<N;n!P-uG}Y99aueASPVO3WL~lJ
z7asn$F%-m86u7oay8yL9$gZytcrq(O|I!@#N(_Hg#QZyGXVhA0rj{ZczI?8e)f@LC
z8aRAb=lhnfWG%ddssTbW1Gf~d^%It(cqr~;R+KD_zKv?{w;C%l7C?YW{Z7rN*rm|_
z>}2$Z^s*Yt+}OckV3Y{c5T#dyo10E%295^4K6KZK_XC1t%>2R}g-1l8tcFdgj*CWR
z3?V)0suktrm{drR6*S}m!2}}%#*YAOtiONIp-5<8=-McqAmyFRz~RQRL!4uj(I(Nw
zgTRr96k?9Y2OkeZUjYfS&|%HPi7ngRQ&f@-iXX1rJ*{IXi42OESem6;O9_bu7Cfsx
zty+2vtAllWvjv7TVHgd!sfYqv4L=1+=X;SDeCK1YC3e;s{q1%`4SdN$Ztep)Z%m;C
znW*>i7GoVfhC>H=U&?!-PGF70NtT6_bj!WmJu(L5EG9b0Zvl`)>yKVEYx_TSwlZ9W
zsd_b76*Dn9zA%tj8T;)jTgO``0;3$?aV(*5N?NduJEG<pB-Z_hv^jtDjJH<4U+Y#X
zix)VnqT9R6_B7|zDO^+=b_}kh40A6|oVn3F*bX4rlK(rr(2q8QvbDG{jK?Co>7Zl1
zlVrOx)2{Csl>}_W#bWF7<#R<o7Ex{iOU(l0+Wx|#qK!Zbg%sy%BsN;_zJo;*!LwOJ
zVs_(M$&Fw7_UOJd|L8ei($>cjeCTjj>evsh*3C@O4fRJ26-GTKZVc!V-%D8s`lCv+
z`~XA_ICG+ABA|xuwe((NpWIWb554b!cgL*^hd2+lU<0t;aj>9pEL)nJSIqy|+h^6~
zII~3ky=I*%#}IIN6YwQln0k?L!$~D`4|06Fg~Cbo%trWN+^@9XeP*4KV)<7Fu5%C5
zKlY*g*<fhOUN7$`LxX*-TG&`{`x%>DHCpBWO8K+;+*HDW#o@A_Z{cY#6y-%XN|!2=
z3*upq4$#Egea1Q!j_EJBzd*cy=id^rZT`pBTTWpje8r5C($b%PL`A7cNh&^(6Vr~S
zRpq8gDb8J(17a23Of^pae-GNsREIFlbmQ!Wn;}*)4=9t*%NtoH6lf;}7B$MYW=DP3
zN7drxKjRW{v^D4=>&={5sdN<p7LnO{v#O&Ja?%L$(g@LXJ}wXo7;vp7pqlhE<ktH7
zN1w%-sk)$a$3T1i<{u`BJ$Ae6!oDrRj_ohq!PoD%`_LaVgGe3DdCKCZvWD=pX6D-6
zN*CyF`)14?bUbeRg|>rrN_O~f?5L3Jdo9f~GmBw{B_NcJ@VYPD_A3a0o>3K@morH=
zLfD>ym0PpgQ@>`jYr5|dm}{A%TPiTsnC)ibDnz`g4RD+X*tw7;iE5Le!adskM2HUW
zI2MqyCM#yUev!k>N}*u<T8%qJs?huShSmMSZT4OQ4|gK<ppOF=fesx#fe)_l7iH*s
zVPY;AGf=M<FC-Ca5}+sG1>aTojoxK-5+Vm3HndJbFr$;dgC_^8GVZ)<+SG2IDLFhZ
z!z1<BgujxZ)B5d&k4msZB8EJN!BsHh!qCvq0M1cIWUzQY)M5wz`W|wnYF!VMPd|uI
zpHZPkaDwUj)9-D&p{9hW=R^PVI2#q#I<@w@4Ip@aVds47=D`l=d42$_kSD{=^<!En
zt^lBKW8byA9J{BOo&;-Mv;0nWE^IRBy<54m6u-2lw)G6Na`gY!R{HY4+xmA8v~E}T
z(Ax&|jUL?1k|o0`67dJlQua)C|D~D#3HXt6TRBRY<W*m+vp1Evx_IGxOXJ-Z=kq2@
z!1nEPeXIGpM&<{om68ZdQMJF5q$-hEJis7}Qkc#qXf<_Ftt61LshifOD_&Ya6c?Zw
z7=Dl;wsHX(4WcD{cm+|>=5)_H>UTprt}7*t*S?gW#LM}eZH_J+I6@4eYX&O%+p^sn
z-8{m&QQC}fh6cI5iw0ho6HIxkV&B;q;^<C^M&16EEmaYK)X7rnRQdPU$hFME1{i8w
zeG`I1c_7IP`m2ina{^qNPF{l5f@5j#MVWIGr(J1$hJ4n)_o#w-B?fg|kIjgvus2PE
z8(KJYMM-hXa(F+LO{7j(0u=fvZFj9q@_2OMMj7te4n=*6it1pN0s~hEgf*7!++S6w
zgekRv`W(D~iP2tZL1x~Xhd*+^H8SMDa;n8?q2_W0(h)|vteS8o1|HJ&GjXWJ0?7+R
zCMw`Z{Sk;c*3CpG;YgBshdXnBB*+Q#-r=GM(cNZ-zh;khI`8k>d(dMX^2d`^fNjht
zv8^X1h?=r$y}(*V#P`W3->^f<VMy%+hV0&6L2S7L&e8^C=#kSQgtbrjm*j|EZ0uCz
z!au>Mel9jkoTb`@-Xk{%*(skM#=|#2*@xy`h%?D@+^^ow*qGufQjLdU5NV(J!bni<
zXJTD|o4)Ruc2>Z%k~g;<49ydtLpHjM&MC$1VCYRa9F-^+x8+xOhwX83P^#XXDO4n@
zsSK<EY;yD>L<@ljjK9zuw8kPjDSx3;N+*sD{Yav!d^iZVDy2Gi6_a`P>Wua{P1ZVZ
z$aabopI=zhF^wAB`@0;sV4e^Y7SfGKpmg9A7w}dW;^`it9zH=0nb}nrPkcH|j<mxE
zgrNzc2!<ZSr5-T3jo@!Ep{5_5jj{umx-PQ=sHwy#UNeTzF7)ex!j3lZ%mVQzbg<J#
zf-#ihqwDox_oZdIzKSxJ+$gL;ZCufs4iYjc7*+>}ee*psb{7zP5PwSyQKp(EqG;m@
zK$srnU%=jVxZ&9(Vq)LLx9p#6is{J3piyL^QP{=Q4;`y_#A!wcfozeaAJOVxB4elm
zK!U;f;~l9FijaAcZzGN$#CY{R^YuJ3(GQB94tB9q+3E<kn)`JWrN-Cip8K`8Qluc}
z$hty56t;I6lM6Jq!hKATF|_v-Fe?~$HOt9~>58g&Sv)XolXXVR?juUEsWiY)t+LrN
zEQX_`Sddw2C$)#MNqkk~+G(7?OhL;4wppSa9{SAeg-rp@Q_RF(7ug|=&>ZIYgeB-6
z;;lkyJ9h;`JYYYe{c{tLAzn<RBo*{at|5N6ycpSR;oi)qs3&0LA#T9XGz=Nore9$X
zGr=BQH!^=4fk0_vAE=}|Ax165F$g8?aG}WIr-@^u>S1FF@c`uoPEEETuCc5Ernlbx
zBkQuzERJjuU-&!4Uh>I7!gI}FPZSk-JDGvStN3s$e1#??Y+1YWqh>4VE|%m-VV#5!
zH~7I3Ob#BUH}0xoMG!=ReNe-Jqm6eYmcm@xX~~Z$PYZ9NNs}M(Q?hAcg;ZGZi7*qW
zD1r!$0nq~szG(w0DMENBF<ngnj2QpFB4mj%FT|qr@QdQ5OVkd=*w#+D!KNi2BPTre
zsnv+kbW#nKeF`9}IIp=X)kId%4!)$t=4NV<9G3xhM!t^iE<K{W+z5z6ltQzHUGm*y
zvH*bxTCkI#0V9iO;gNh-80{gqcAh?hoj-isZC~fKhX+hKcR%q44sPuL+=^8_U0&a3
zJ14#8{fVoCDiK}7k@u<|{IAWO831qZTjzMh<D97!&D8Cy%N)k9jP0DxHoh#wY<=JM
z=R5S_iG~WtXO{8hn&W#WK6ltZxM81e-5*ZgPZ+~pALgjph}qr4Aykyt_ntZ&NN1U*
zl<(t6VsL%(TH|-wQ5G(MA8lK=h)5+-HB3jAIReKD@86#fUl$K&KOam{mrMzTpVLAw
zb_aB&ryX6S51JEGxw8KFt@OOO3DgW6{GUS2J)Y_J|NjXIu@I6|IaWfEL)ez{sZidU
z4C76yoZneyw!M<WLQx^gIYfmi3d5Y~Xbp`L+bA|GjEx!N>+|RDuit;yAJ5zEx;>xQ
zb-x~u>v~>v%&Mfs!RkuIv)gIfzwL`|7%6>Px4*C@{+hFRq0y-%OMrY&O>SIC5Dc8V
znY!=o(E6Xlf|4r2zPHJ#s~OX4f#*t$12DctJqL3x1zZ|u?bABJFRDy%Sii*?>{mgP
zpS)rfhBEa(eVSVYWpAY%9n3V&H~X#S1Y{vPtu1YQ)3p~Kn7nEI5$-+kGs7hIfr;L`
zV-?<aT@kTdXt7E1p@<7kQj_KP)NP-Xs|;Lp%Fq}Z=M*KZPOQXtlA=E3<R$3m#=>(Y
zn|DH{^3GlJ-V-)^PNk&CR;A7L3HbWfu?Nyl>Jhyf#<;r>`;R|^vKJflvx3N7VnD@*
z3iSJ#ft)!qpxKG$)!tQDG?_XL;}|ZxAXS$gPPu3_KO8=Iez^woFx|D6e9yvODnh~O
z<M|#J@ST&Q3iou+wMLE~zNhI~06?Kuf|+ZELzCjF*WdA{7milN-q04$N;NiF{o@HW
z9^c3OFWKsyeetQ*80ePoZ0;gH>Lj3lFKj5&VjCTc@vl5{W>74?kp8}|$anI%zHFPG
zB{g4cum!TaA2?K9v_Ej_IQM7mR~aSb#ZWUnM^fxlO6W2;G-KvN+|n|=KV+|2n^hbA
z%H;2U#-I6>fH$s@RiEZBvEHcsB>fy%)lK-`o=^G_%5PJSEI!zn^jkFm{QeoRc<s%3
z?QgDy-wK-6XA_*}pkF+XnBP6nxAyB{p>Ty%)I|E+dHiE@SN^A0`lVs{CqMn-MFa%a
z{r=mXqd!Q{^f!VURgFK-SeHFTy|p&1{PeD(t3z1Z1(}dszi5kaoX&rTsYkVslYc(P
zn#<nrZ`f7vXX+Po>&KF6=E3#QnKhtd4cPqQ_U|I|Ou;{J30dSTQHe(xwuBK?*Ih#@
zcNr{wyiMf|;YevR&mgv!W+fqGHd{uKhW_|cv=G~<iE7}iPOex;7+miO*mI);IrO#J
zDvZytzcF5R52+h{k2LoH-F9=}!R`qRrTAu=#?7IF1wl3;5ulJ;*xGXH^5zM_Mq3U{
z0)*>;KnvB4jFeOjrcSq9Hr%-N&+aP^^5mF*r`JDK;~NRD@^Jb2+Dt7y5#@Y0rj`}}
zviZUnGC7UO-!6Zjyq?Q}U(lPHk13CLmoW55xoeUHeJNbOaMdMA^@3i6lZv*}QfSZ}
z%7uY78ylIe4HnI6OuE>goQAB&FS|_(!=gcmj)W!j_Ak$|ocZqo-e8W<A)Blik#PD)
z=^qN81)H*TNhr7a9{BU~>Q(cm<qlxgZXk7fOn=Zgd;8me3qH@^ypUeswvhdFzZz;G
z{;!JL;n}*!^7CnZo?Bk07hrQgN=GjpH4iag#_@~WkFVPJWNCwZUf-<An6%Fe+;|cN
zzJlU#e>c)J)k^+ou4=sa>A7P18ge_|tJMS=5j_mVl&vF-_ja%luWvr}+gjv-{`@!f
z-|PF1XUDfiTdTC4^N;M;I*@;#rFF>e%1M)8lVI~JXH0`l%}$*RvA7x%Y;I;^apuaY
z)0S64Eg&}kzleMmOUw2D{r7BE6z1#CN;sRK`_C>(G1HUhG`$uTd4U&f)y@8~6(6;}
zvDa+$LUhgARNE!-Z$8vp{?okrnep(j;`<#R>O-u*_kBNK^touQ7&>=`{3Q5evGp1*
zo{P;$PfuU(+<qmWvouohFvcOTpas##t&vwq)R_e!Rl7WrO&M{%Vqx8_F}Lyx3i=8T
z#u^!cO!f4R>7{AeTs3Z&s+9@}HuF`d-Zl$XyN8!-P^y(t2$ruE%?Xx@JF9;#_4-%w
zk#bdZnX;fvb5GENwYR&5k~0~0Q8KRQ@<LWMOi|g`7Nm;59XSOV4EEJDzbzB2J$}$U
z>3lF?I<EHawqdZr_@Q@6k-^pl;uF2H4cdRitb2{*71rK%EZ4U$<52PAGOG^?e!aL=
zTJke&SAA(n^ti-os$j2>u`8X^{HF8EY_x>?x!&z26R&@N<T<Q9@VMDq>&K5wSs^vS
zC0xIls>~*@PpG{}*dj1CMmH~9O3@r^gyUU$fP3d>&-}bupmRVt_0h}Kmvj=donqgs
zWwWaFx$nv4TkMmr{%h|smVmXL{3k!hg_TN=lstW{<}~P_V$7K}H4*2Y3y&~@ki-;<
zP0vxxzR#&43`<uMW@_O~N#c#t!yn?G5zMn88l^`+kUij~4&)iL+RAf}f8`%(LrOJ!
zOal{w+Z(xE-(uALKY^>KRT=0Om8fYd#!^PfWqHl*FQ<Bi@4ck*Xp=>*C08ob(PHCw
zl--u|J=#3w)}ADhAODK3*yvRwZhez&xetL|oX-3US!wZ<gCH*2e5WdZouf<ZR(-h4
z&SVPe{P*R%xXoR;#l9HzjdboJ+KD##A0W8c?tAgSlFJC&F;7fY<v9U~=fhRx-*9~*
zqzVoR4z)X6%y9NYxR3os96tt^swGqqddJ*9G76~{UoGgWy1zHiu?v|3*F4vclLl0a
zk>+W*&hOu0)aK#lnF*cW`WoyBmNiHH(J}~lN6H~d8|UW|N_=UKwB*Idx!ZL>2o@yV
zMS`ilo%f?TLsJ%&@zz8k=xa7zqMuUsmS@im;RnYyZItu0xeBOM%QqFYkqWLi|5WU+
ztq+1&LBeK=<yFIG+#{SER5z<?J5+dDXo7Q6Q^iFJPY93WJk;87*M&AhE1a#GKFGJz
zrSm>Qe()`dozIHr7)+x8E{#eUUYr^0<Cvpy?H<5g+WtY%hHs}UaE~TGNFe%ko(Ixs
za)XN{ex2?>5=~*yf<op%gt}X2i(Z%d0xrOPsC?LR6g!(0&C#FcM!nmz%`4!4pY`nj
zel2y~lvwh;G_x_Xil-b0{shZtoQS6)hI#k4-HMV+;J|rctZ`d4HY*+1MjPg}Z+jH2
zQx+-sICar><uI0}R=}mS?5TyKPA3~oxQSz5>s-pDU+O~FtBe(g7d&6|@xb#%${TQk
zNBoRg-}+Jw?`fQ|hW-$!gF3^)+1M6A!J!>W;Jaf=bH<&oOI*lZIeqK>mTV-G#|e$y
z!hb?b0Ubvc9{h9W`lM_0y=u1`%WHMjl)`BvSD6zHB_7dPZMtt=1K1kq@Sg@R)SpcZ
zI!9-2=)PTqQAN2YY>vLr#)X0%7Vn0+%#Z4@pKymz0j>cJ-_T$*tesR@-yYH-(qS>>
zb@9{jT8n3E{i^Qs^<mV)uNyPxb$LsKI*W?18Q_a9j|=!k+iIpX=Z>-~>YAT{`r+<3
zuC(*axeOHCRX9;houD{RUw$NDg;6I)oM+T^c+JPC*29DJVjUi6tuFq#XIGoceEh4r
z_$tr7HdntdzU)a>4oBnB?0i&*KKA&O^t|~WQDhr0r)dx9&z7(ifI!X;zgeyg8wmrZ
zMRn_7acwfsl&6z*BOMTIduAg?&9#s}EbtQeV+tz2Yzzrv1Q<+8W!?1<tPWNZ;x_!Q
zxe4-=w2z$Egq^F+E?1rj(f!N!tjn$-^bNZI=x5HEB#{o0bDH4LM##g!49`bR`WAJb
z&k2LoE<f17TSy*Bu2k<jRFKC5Fld#)!`C}sUd38rr6KmiTV`lXfh#SE{HQ5<!`HYn
zf5vh8C1gqvA&A0cwLAh-=Z4p&SNeVvuVEorDCw*}kLrtXf!;HghZVZ9Gg*p!`B-Fj
z6uxQ)9Fy29&WO4H1g`DA{xcJP2wUiV!U0%!2>TT?jPq^UZ$CH+s4YkIxc9v!{S^2K
z6x;vtPkcrI)P;vgf&SH<4WuNTDD7yy0Yw<8AXEy}t4~a<i+)b)ZNAI?Yg`vy1?_51
zXU{O#u2>7@NcR4n=^A0ThD+(crv*QvvC6_@B)I>!BDOe@na2-wCCoRHvbUsY#;jwM
znQak)>SkHx25<`wbpY_1kGXp&Gpllf#CE&kiKaIi8t3}~jaGTk#wpiD(vTn)ZMK<G
z2@<>)xT0k?b1SnKc0dPfK($#4&j@oTI+So8!*i#baU~^p5f8XNr8}UHtt{)h(gan!
zPjO&l#6zwqML2hSG8K`-l@6;zRI}FwX_d4LphP)pn1{i-50`FJ1d+s&{6!bR+E#?n
zD1iKFO-DGx<otqk7;T*$23Fu~5DQJh>97!vozB_+8)~t(6~RN8vpaKn$GUSjHtyBW
z{hpilINq>zXG)%MARcYVHvV6r?m`+xxMCJS9*gdqWDHVi!`Af0zR9-N01w0}URs+T
z61rBx>UPpz-<AW>exzzmmk1v2us)?uIKFUsv377car#?d$LTRN5*^*1)-o2~6qr+T
ze=t2U>=_RwIBaA4Q!#-WPQk|rTXHVKe=0-Y!WCMPM@w`T5*usB%0YuU{lZym_AxG{
z#r`L-24{N+4%+zq1WFAXN}M$DZGFNvLS6NUK0PWHSjj_zuv!a>o{H5-P3-XnWzS;I
zS_$Sl%FBjiOSR{+P-&>A`EYV2xsRPuy`sYAF;h`k4tKqSw};z`vghn$MRv$xAyd9K
ztw7UM3Tc1z@e-DGtwn|LKw)N>D}rsvbmu&tJ|?sV*mX<;4t4riHi>4={f2^b)Lw*j
zsCS5w<;khiJG{GdWT#u#q}l2$HpgQ+f%lp>#5HNpMB$c3(J+Bhdm##^fi0e7O)P0l
zuiFr}xs{7uiRp7RbHBy&#)BJo=YThLYgLQ=8|fBX?rb4zgCjDHRBtLd54{UI5Iq2B
z)`FgC4oGA+_XqBvuZYS*Sx>!z<l=T~>P-dG{4_nFsoDD%AF!#;!(@6zpEaYFN8zrZ
z>QU9k?;vS7IZcD9_2?b)5d(vn@s3=cXBn+)r4Oz&2~l7*FS$-n=3U2{2xTFT?Gn&t
zNFEMUsyEeGdYN1e?UL?G+yEq~)gz^J(>_&*PI##+kU^GTq&ajNr*h{|4^hyLNUV8>
ze5v*nxnd&BNT>+$Y)25@KuWh{5r?OuE1dgNxodnaj?euC&_hJtidJV19-Gd8G+k?4
z1?$gGCo6-uPE^BsGyBJ4%6W=hOH38t4;O+}1dAXHNk$Z50wB|29;ijaU8ar==PX_1
z{C3C=VKYDQ(VY8du3|;OGPI+lO;@S~WrSnGG34LpeTf5+95Jt+Eyf#6;-eK1m$i2U
zUIc^Z->UMXxsv-n^~blA^8&bNeiWy8AqorX5Fx=Z%{wLqg4V`#@&g^#dPTW<d|Qt2
zBvo((Kud2n@NpMt0y(rnyB%g5(=WJyR^2S%Z(;t2z4c}apOhIjm&0A<ALGE_!NSuW
zrZ}g~tS40RaNG1;-{Lljw-N`oM(hV>nCw=U#Z-hmfWOWA#D(w`Icwh|gvUEHapyOa
zw{HlouqSc$n<4R+J6*}$(dkg2lm|?3gZb(lGB!$RgcZYiZoYapu>!#!*gCtZ`l%LL
zncc6M4tOf>sQb*0x)b<sc_3y2-<wmK8MPh8b>-jW&<<V`iese$k8R;aYdd!=8li97
z3SE?NzBH**ZX1M)5E^2YwmddVNljZvI`#s_TeNNa%0Ugu?6-E?r-6q+{QJz!kLpHR
zTTq{7_^YqVbf5n1d@=TGt|Q7!@*l&-z+#dZ;YiXCU26DnJ|k8>2J~9P(|ABZ=fQU}
z+Hl9Ay%YO!qOrsUk*V)m76#u@clJ`K<gd|&5<A*$Yn=zyUx_&+Nzc5lUo^O9MRb3F
z{LvrL;9`<`ynE0KV1$S#DXh7bh2nQmS6;~PdZ)z}5op*PP12@}sXWu{GS!JO|A5vL
z?hl0RZl10ktI+IbyVF@G*)mLLPMSPw<1NpLJA(?5+~mLE>2XI;-jbVGMfR5+iJ6t>
zYfYi01qtm{VkF%44n?8-l;3WkHM~PcC^dEIj?b7c5bfNV7Up{L)U^(<(0t1F4ohPP
z^>~hle8hoCNHJ@TV<aCTG^Vx<Yfew<jJJ-X;{_q@c(DzOH&Z!V`xbS(<yLCfo_BU_
zxSU+{q;3o&riD6|22?a42*=zOQ{HOhMF`-SGBNj3U(LR6DS{x$$3R#;OvPtOP4ZIQ
z8vv54kqOG7x6V@WBd=z(bx>ddj)xczpRUm1pPUd}LmS$_?ii2xY1(`C4Z1BQ!gg36
z>mGDp%F(6je^p17h(WhM3mnkL>$fjis(3u4!zftKZS2=n&m8*pxrP$YHHNtS%XI~|
zmBiuO<Og0)Cx}D)_c9uF4p@bEJSYLum0fFId=f;U!I-R+A9?UG74iE^3G(x;Uj!Jm
z0wyVC&-Q&@D)%a1OY(l=)qw2|k~qo1u2HJaxT?7)-}M^BnVLT`!RVLw>-a(3GKfjU
zRHc}gydh;w$sr8Oiz(XchtOf|4t5frz6kfljC?z=M?D@L@pCT^<-5nC7clh7#!r-K
zh{m4<FXY*SsejYZm<j2%ZlPCpv_!eah^#$0%crYC-pVJKuz8Tsu3tY`udt+JBhDK~
z?wRMztBr<?ilZ*r<-hzM5;%P-aVB3k&KNz=YPXn)$ondd=Y?}c_(+t!ohI)cJo-QO
z*-fQ(!}8Ltib*scE-?ed>vF$Gu^F$@TRgQx3QsP2X-pRep{&P>LQ3CP#H=TTo{)R4
zQLHhu(+C)?_^42`wy%^uvo%%1J{BlGU<Y=ynYnC!;i>IpNa;*nFucHVEF?%5@Y#c;
zq0*yM1s{>1gw(~`#M1Uz3Uyh^c^brwro-Kg;6awZ)dRb<i-0sDnb}tOx$bSuq{$+u
zmurOLo5A88oGgLO!*9%bj2fiYV(p<-$4ewtyPUYb?WZE_UZh#f@Y;WML{!7@W~jhP
zJ@PTLR^Vm^?iQRC`?K-55NzX`JqM}EHQoFx!4>n(#NE+wesLd$7x<&e4mOg{yZ#|Q
zj$<aPaIH=PPcCXwpEGH<lEFd7MA1djjot{Nf~MHbGRPZ9;-NSSPp*l{=Jf2Zbsi(v
z99cx0_9vHCEdHxHRFPPoeer%IDt~&eB!?N#S>f&?JqT2uzqNO{c?R`3e900lW_nb$
zg^bNuFdbuDwJZtDPh6ON2=kifz;=?p)pnKuQUzkRCzfO#X}kaw2vTOzquJxUB-wFl
zO9V48gLuxyO&l<<U_<<qht;z2M6%8ZoG!RdJZcyV+SfzmUTQG=z2}eH_2hUwI5-*&
zZ#P!kB{4j~u%~-j-YXHG@Q&(k&6VZvZV@x8i0{i}xV1c;k~B^V4?fmm`p2$S#^7iG
zzzJEh-04^0ls&o|m(&7iEM1i1ROQ-ja5*j>eUlxqnsOr-f|5BX5l-2dPWOW5<61<C
zW%wyg*)k@Cun}f{MeK7b5s>ZE@A+`D6tcHeR+^zE2(nChHnDj`7k^PUz8A|a=i8zR
zO!h(dcy^g`8D0oR0xH$yQCLEs1yG}RuR6O&At<s2e)aUiZI7CbNFz1T!C~-MXO+Q5
zo9E2S6{=X9Dbe|AbCE@vjUExMjpaj=y|Z52f{H~VbTp)_q}AyxHoJo9y+nyQQFOLc
zs`|n*J=6^XQJh`jN1;WofPe0?7_OeV5+gloI=0U;=Z(U`^UpnNJwh8&6!6;aqXPc`
zq(YfN4%WpumdYTFpSlAwG_P3(x*i}mim_HW&l}EM5t)*IcPEl5&CqgF`r~r>UVPGI
zIWEh6iP#`kUuE1s*3F9%4ah$J>6j`*&+QaRB`RrxX%GYc!RG%xh1J~>gQQwPE{nsw
z18pZw!k6N`2F<O|lrevxba=1%b3%V%&uoKkK=yxZIvQ<I1CJJ+l6{9)X9_%2y|{PF
zLmY)lzq-@8CM{2%ZL}}EhA&}!cUAA)^-WQmY5YS1^LDYvcGxe({Dm?mdyITVzn<V$
zik0qAqYcbh40uwIO)-Z`Qmy2_c3?rjceguy&qSob7)SwR6VS^hI8&a)3A091tTIOA
zMnzEjHSXYB%_N_DWzjtfWRW)BNfKpQo>|k4jDt1K={wuyiu|ajZFZBmS95}#PzM4s
zO37qZ#|T&dCT*~)87d!-)P#L#Y=ICUvzG;DHnsd6C?RdQjmO=;<J84jV4n3e+Fkb+
zobeuep_(x;BjC@&Sg@t=C98JZF*w2YZ*y7Jn<)AkeLv(f*p1dV=>^S%w`lGu%aV-l
zwaz_P6EfD;g7Z{e=A#2!oIj)`GrR;?jMyk!8*I$1Sv=xMjzt@dm{ycf1~`1Hz~P(U
zF)e%N^*6*2yYuZPx6s(~vGo2J-QOxCsrl+MfZ$Bn&zpFyIUgw84c%=(zkt@oNFpfN
zw(2mp4@0tMgX}9%%^=NIALy_f4I`wWaS0N<mtNcRhK|`!7U}rU#`l9G)U;K;4LI0r
z`hzSNnLdHuQHp}dt$D3KE`;4Yt5|iM=D_m%JM0UNgY#AcM$eewS1a#{zu8@5+(Uqu
zvnBd*>G|}ThanuZ2C;$Ow_XGV9#5x>7i0WWg7@^b`MDGcx^012c9#_D05!=<P>k2_
zm0pr>-{)N>8klNPrZAOa6@^Htwi9CMG8pL*I{v43S=3GCQ3Hp`E%#&S$Z@IpZ_cX3
z!17Sr4yUi4UIZiS-rpzl7m}^6QUMCxAtUg}e9bv%J}a(c^@#}bUelfWu{t<I*4JY!
zeBfLSES1-S)Ep(-5n4b!_A!b9Kqg9r2TM)k!}&)Na~Hm$eZ~u(Z8Su6=(R*ys9$J$
z&VK*WFal&vDP&9rfyN8#JA<0am}V~Kj)NiS4nS;vtD-b>>tbx$vr-D+STi_(D^57d
z&Fkx#&%K4(T`P(NQBDO))WB4FSpp-cUK`8%QzG+_ujvr!ThHSL;(G$TI<2juY<BU~
zk^RWcvd)!0N?Z5B0U_9}(;NNw!R`_ML<zSfcc{VOkH=yvyAB%!5TgJ?QO5p^K-KxY
z_vb7#r$ELj=*=hgi$FFx)#|avS=jvgHS1BtUv6t$ZdJ(3fVhqU3c@_@MCC?9Nd?R+
z&J%KO3|1)0BW|4@MZnS+=q;J<V_XK`zs6aAXJg3uX`QRiPC@$|Oc5SM*Q?2f^`>(D
zF)BZM8=EV$yYoOOBcaFrRCL<6Q=J<32WPBgF?&l#kSVo*_MDy<?P1mvBsUSigNZ%w
zTE(k+?%K|aq{(O`Nn!ynxJHa5_h!Z%Z{JO@2X``?4{Od7UZCGr4a#&JA4Mc`^PjA8
zRhGm@5m=s7tZWfTc?3xqp-FMCRdi-4F?O!(&8gh){Gb||Gq~_`HxH%^HeqsZ8jZ61
zcHyLe`Mu7Aj#f(ObBNo(F66$3hxMJjJkALs9-4~2<oCG_R<`iO>LO7D`KQ|11)N-(
zWF_^D){D$0o~IzhdERi@%<__BmwJ32J-lUTa!7K(ahx76_b#a43*}j}r>*-(gH^3a
zxSjfuzFsk3X}umDW(qRM<Xn<0Gxfzu8DbD%6=x3`{q`Kf#ETqEIWoTgY7enNqZXvv
zHQOK;v9GY}d4o!XG`#C^gJOitL|0aW`sX`;gC%MV&RKU4HArtORhVugBUu>B{kQNx
z672)*e<-iwTVwXC?Z(>$q`xq*a_+evvrkPzzw1SeR?$A>w_wO<UN&(k*62h^V|o1n
zV1##@sCNN&*eJ<>VdA?FSv7UTcei`6ia*H0F2KH7JSy3m9_YKHVx}?B+S?M0;F|E?
zaaD!&+14MZRIoSfadEOTT^A)9m^4P0SW+6D`32^SL2hT4WzCoN%r(f9k_mLxz+{~B
zl)F>5#ydCnAfJO0ueuL4NW|F&I937S&*M^a>!XK#E)e&;G#cfdCq8u@Gh%(z4j@#%
z%JH)cNT_7ri}QI{FFBm&K#X#MeP=#B96+gH-;Vp{DKRc{>rOxct2+FKl5K$Ui1ccb
zkRD{YOE!i0udak_vNqk<Qfk&Nz}-Y+w%fH~mq*e_S^aW>NLaU4%dVlM6}mX!yBjHU
zx1Rr%r%tr8AB$s3Wkq_y!kB*h0usvEdU0=4>+3A{A}3SoAAL2GBR;bovt_=-uXw>u
ztKo?mjH5Op<Zkb!eQ;})PEq5YPfN$!WeB~6OJ~}p7klwuW2TTaD|f`2X8^h8l``^H
z$3h1Y!m<Bwke~V`XDngX$^r-sd&kD0iiH{yIYGN?Wj1V~qbe+`ZU3-BwtsAKaQ(^$
zRr_LtdedH{M$6DNwUuTyVl6#?BC5Et&a?@Mdpq=zdS=`z<nkPh{pVV-cb#cXTQ{UZ
z;!nT-(<IcX(bhiEveoVwvCm1pWkbvA;x`$-mXcZc1g|;TPBDT+fD?C2=_gv${#T6M
zE&Gh_xYNyA<mzv~q91AzsZV9oqgo`R(%=lE7WIXcLApi@NaHqfdUn6fPT4Z+TPQpe
z;zy^k(V}D+T^yBOSC`nYUGpj+E;6$|l!81;L_3bXY)>M}I<AEUgzTJ=J5PB}?wiE~
z9C>#0KyO7EMZzJ%>DiF}=;gasb6-V}kn$mo(bhXwBc5{-^ATr@Z&sPIFP2LagZHD$
zHRp?(_xUPQ@#ll>#}Cd&H0>CM2pQ|HcPFLuyT!Cs0A<-b|1*AvWbxXJ)0TU(k`?Ix
zSju^%tpq`eWW#z|8}<*S889#{`{&zZi+Oc7`;k{$hC07proIZ6Jdt`O2K;j`a%)AY
zMP}i4V(^)tGRUhtji3D*Y5GCpHhZGGyq9*{h>~rKlWJG+NGiwY-Mb;i=sK~PuD;`3
zlR$JpyC#w4%~!kB6ThU0>D6X$tp}Pw6RvDG;=5j+l)aQ}R;H@g73!<1*L|Qsw)mvX
zd{Nh)uhK%VZT%;LlcLnr$e^9P%v0-vZ;s2~!bb)x{n^#l?cp`}?aa<{N+j9}Y1akz
z#UlkW60QTe*B?d;ng->RMl)juU~)=MSN{N^pBGdZ{+=l-`i?C}$?q6PKlrvAUVL1f
z-O!SlVsOc!<@uAzu%^)5&-ZeNugcXUu7F`C=Kf~n{CnrW&xYvC{L)xa3Em#U)P@!z
z!UGSkA_}r|?qzRLF<GG)LiIZ81OMMQ>zfTwi_*g?+il~R3*%5Ta?a;U_N=>ZqsKGY
zy2FPE4c>GE;dH6a6NL)w`Ei3U`tGy$qCdOq-kjaLa_rG%6a`~HzAZm>=!s)RZLaI=
z+u~Vo-Iam4*$Lg1t8MSW(U0MjGkAD#YbZ`dRbge@{Oi)u{MUQ5HKi>qEzG5KbsasO
Gr2Y?mFS1Dh

delta 25337
zcmZ7dV{~QF(mf7$Y&#v>wr$(#oY-b3Il+l-+wR!5J5I-T$L7E9@4g?N`;M_cti9{Q
z8oTCPRW+;jo{NqKTaSqb3jl$Ez(EioNDveV8UzD^1;K&fK?op35E2L(gaSeZp@Gmr
z7$8g#76==J1HuL2f$%}!K?EQ|5D|#DiNvuH$ipfm1n=tRVs2s&@3q#fHyL};hO~K1
ze+HvRuIiYt67?+utU=z%Qxx0K&`{Sr;r)xu_r!Yg@{AvEL*Gh2l`>L5fQ;7o)0Gt`
z=4*-){BtEO4!FPR`24nVd6fq=@PAoajhdr7w__5{#pydQ-iOL|;WO|T_;g-c+h~3S
z#`?E%%dGwowSD@HpZkncSJe4&H)_lbd~xPks(|%R?!!Io>g`fZnw12%beflG{Mi+?
z3yt>WV~2!d<4$o1vt^B5`$(QqG5r0MxH(+DaGgKueX{ObT5*?r0+q7rDXJ=4Cbq%=
zZFjx)zM$1{;N`|r+kL!;z1oN+nEuuwFoWx{$UqgC0njt%fG0_&m9SAgd^sbNsk-m2
z#}lhn7C+KVMe9TMXn5*4*{v@pUtF1Vbtox_oZo5-j3$s7cq{H^!*y?+RXtbT?jpVr
zz530m)1|cGTHyUl7wVTLGt7iM{2S-ybQLlQW3ZGph<m7>Et)2(QB&fN4o9^k&=J{g
z<-$pNzH#yQlG?hgH?l#!`a+v)p}QJ(hBWjYRL?DV3(f~lTI33O4X&f6M@22}Zp(b6
zHgtzpeoaB9;pO9NMOAxuMit4gE*x{TMyZxIh8mWZ$PjZ19`Qme08s-zgvCk<m<3iW
zYAOzyThkof?8p1`bG2JEJI&51u<5~bsImWvh=+LQ(p3ml^x$=xdE_T%olPGtJ86!j
z)i7kP-#K60tnwbM_p8nuIxz13*j)r{xv@p-K8=6%+SOefoUfvyS7WoerFu?>2&cPF
z0J~bO+;_MBr`<#w23vl4B<r{Rdwm*gC^1#rLStLM@OdcN1sayh#sbDh;CMO($xbK^
zqmh+)zh)3=hYxlGW5W%4;no?O#$UFjO@3ID?z!Jw2%60FJB)5{G6@hHkSx;xiY=Nk
z27EMib2{q^B1+F`qH02aKUtZz^7t&oeBoxluDjXOvX)DA@dkNgXF9#kwI{7rHm^UH
z?c2JNFsSTCe=w<;@9nI<10CRM2~iE{L+CHvQD|5w7DBsjfA<mj5C`C1cyi5%U6li>
zes^R|k8Sdgz%F3%4+WV|`UVr6wLl&|(a1XueitJ_gz_$OaQV3W(OAhm+}{t6x_0nD
z*Eja7DE@}8(>X77pWC~$$kqI9Ck0{qF{W5eLEY-tlf=7Ub*Y4%9x!Xh0#kx?;}jl`
zD7!}6AI_7Q)%Wi$53aqK+*3#ek3W$ZmFgkp0jrB0Jl!hE*o`Y>lZ(bsMmG(?otY}E
zwh`t?-K>x2#_XS!*BUH9KoGZte_BPuRXq2_9oUovV9&RY+<fi!NLpZm#|tvN$UP}i
zM8A7*QLL;G#nKyz2FN%*V;hJXBOSMQ4w@A<(2dAYh(hxXbylW-C8my<=!o4#^%g0V
z&PBuu4My;LeX~JN#_9xmqT^?KrE6L4iY9%s(l>ZAV~oSYLQh60DayB7C|Ti7MF6Tx
zB}rIqF@EyM6{pk3|CB@aq&E@wThr;1@~;>Q8BsRS*i&P-1TyASye45egDPO0yV$49
zJ4P+$9{QSNH@0n64UjxsTtBg0$0J8%awws6OExdL{v!RsUQ<};X_<$F3TgPW=-#wi
zU+IEa41+daJ|^ruC~hp1ojJrQ*TUG989b*AL1T)zH->^}x!pKKf*aLWCe-%<DRQg<
zYf@Nj9k(r22~?ayDlc|dpgp$gYyd_G8=}a1*tA{?>OmF{?+je!ONvy2Ir1^`<>`7$
z#BlbRKKgXwL^6Y3g2K`O$oXL~7+gyP=L2-hE}yH%I5K@X*d^8s&k<`VDpeeAl$>}S
z;E3KQ@YF0!OlW8tGY&J_2CFQgKM5v@T5uDw*L4H)fGT1~d!q0R_&f@Mhr{+K;}s;m
zs|~cc^WgrL3RxwNlD9gm2|eoYa~ju~u3|HEuRZL41I^x#E$fkWt1)e=<!~|LruMSa
zR3HWsxoW6)uPZUvCJ41zkQL5Yi^P*=Oh&)Usm70K%{!E}t(}={piv+2Lea+D&q*+F
zilx;W0#!uwnh5imE8|DX?ek901S#v2u?#uQ%R_B2OSs*WhJDz6l^#8~y>Q#=QI}(a
z;@n=#+2TT!&`OtsW|E07O&w=;oAu9zKdOx`(tJc;2Vw?heiBtdPlrdR)BnNsv(k%7
zb6~<UnP3%*ztXbi5t@*1t$i;}<1Fz)=N&ie1_mXkF5PN=^%!&0$}deLKbXjxRUWhq
zk#lzM!jk-2Gy-%pxzpXqC-E&dFShcAvbbLqb+mOYXv_H7+APs6*h^I?$5jFmGt$x>
zl>S&6_IV$)?IBk}6k~)6Tr=Y)ZZO-@{BS{8C9azZI**x)Q}N@)7geOmo4*Q|vXhzk
z0c2{3lad>dwMMoiVw`^O_FiCtTWRo-qQ~%WQwKAWbG94#<EK~5!zBin|NWrdondEv
zOvB>HMX~Owi6}Xscp%d`T7;6N?xUE=;L2kW?e7tf;;Wx?ww9KdWFgtKytP73oh0|1
z{U-h6iC!#Su~%#DL4J~+aL!JMj?y*59FTGw&hSnlE=)&@fqC}WRq!lKyZtkD38^M!
z)+CBw&Mi4^^gz|KZ>fK~i&?JM$)lWX@E6#<H>B?9DJK8LnCqcS7zf^3G`iyQ-f?%N
zrp>K8{lf0M3TaSeK|-AUXD2VTTX3c4qz-iR+7;x7kxCYl9-C5%;}p*e3<>}>8W_{H
zMH-1pej)FD(!mw_CqdC;vdt~ESYa*K03E4qPmUAPhCg#rD6ytMdn&0j%iNy-YGd<#
z@w8nOeHPo|7@?kr_$bPSdIkqJezub)u~K?^vv{_mlQOLHm`X8fazHR|Q9+1;F-&O4
z76*NyOh{w&bZ0*`&G%$y6Uymu5%`To@AodXczjBQffiqmX~vA8G=#mAg4K@S^+`EV
zs50$HrLthkX$d+mS5&2~E1~boS{mlt0N#0R2Ya?=HEK+5MrdRB3RW{R1q=VP0C^BW
zyHNu<_=X|+(gt=}(g#n~{tp)m+qC}1505b$x4!UsyExfUFPV8a8)A5gbszzERr-e~
zVD&x*uf6sc9XL-)zw)TKx{g~=h94JrnK#VE%+ZQ>nBWY54~|=BxOMB-tC<-d$a2vG
zxj$y9BY?a$u9rw6Bo-$mGF<mF)YInB{;2W$T*_jyy0Cv_ee*$w+O^--vpV5A+Y=Gi
zGV8>|!w~`tvVWf7zL_C^8}M=B=k!@g^&0&F8>e=cyGi65F{Lk@w$95v($+SR9_OpZ
zcs)aPo0SF!49lT=zSJ-Co)+Ljgvui$+e!ml!I+B>$?XX50C@25Ka;!p_S=KW_LC$e
zcerp&u8BM*b&otQoZOox4{|*GS!gj{twrKA5dCF>$1cE9Q0iYc1iq#FG1$JQ1!v_r
zhrGZQj0MM{o^?&I{v~<+YPLMr4Ny)IIk-}D$CH0~Sm)B7P0AGy8DD}|w<*z1edwN2
zNB**nNtb=5RgJ(j{__&5`7oitYRX^RE}DCE?eP<zQ%-n!B<PazQ0v^9K46#|OcTPb
z+%HGC(rM6b|M4BZ3ZJ)(^~Ag^zfj-(>uH2v_@(4@`}1D7yb8eC3f4nng8<}VVf()o
z>a?DG96dkU)*byV4B(<+v!!H?A$~{hLc}smM}aD-69D!F6cse^ciYG~AQCyrR_)mI
zU!2r5PVsv^9?xO;bS;B?-p&>J3Uut<*{<{K1wK2!e&l5f^V&u-Uf%C}fcwsH<&dQR
zXkCaq-`=Wr2jbY8=J!6ao7r9euy4~t;C>%I#@zb)+@CEI{^T(@>olf<ny1aebs>}U
z<%0V@BVoWG24^=e_K3}dW5BON%zWQtoJ}1?u0Mm<*?&rqeS=D;uP>$KFf{%42S%9@
zD&s?<hv`<Kt3RYn`s_zOQxL7tu8n{u?A$;amJbu(4`AUpDEO=uFfOTN{IOSetb~i2
zIq)2!l!s-S2e@OWRe)_&r+4NJq1qBk+`8VEzGFxW^fZ0r&Rt3D_>=9mwkJ8p4&Gpv
z%H}DlO+|>s?lwas=WBY}iB<zBIp$8%{7z<^zre><EmE=EsbqLBi;XM_{d@|V?VOoz
zZ$xZ20yrxq-NYUCc$Dy~kP4hFb@ldlOksD@H-WD4PZCkms0L{rW9|BqtrSX=W=S8K
z0`WLGF8N<pRb!27w)S(>ndBPa8Dj#E<oM|^RaPll_V`tR2wlj)H=*pAA7L?KZ@n3E
zrz1lXF=kFSUNWfcd1DHD%S*A28^}x9bQKC@v%q|OfJZyj8Qm#eRha1K1Y%UQrNhyf
z>9HovCQHir@-(y@B|@Tf<W422@xA<({g?#|LznZ?kxK4?sO8oAyMIf4UM2DhiF-tg
zMb_r`xb@g)7ujj}CSyl!_RVv<y{ysS+MH%bIioNo>-LRy*i3yTfXH<>>bJ=h!*4H|
z{y-{jC)Y5Cd|XT=R|s3?8Ek*#+>jFx=c{QMn8%fRhLwe|#^EAKdC<i^RdduyN8*_R
zN1gKDHx9r$t-fDvxh-WadmDg6b9(fQyQ&WHb5OF_<GKh&EJ`q_qD7B_67pun_-wFO
zi`D(^ghdd_ibVyJzT8TBms{Ra`PAAm5jfc?fYDksZnDm-=C?Fhfa|0l%Y)u$r^G#K
z$tOmKf+{lwy@=PKAv?c<a-L%<yWkoQ_0luHedjb}Zors^MTDlR8D(~r3j+h)X+PE-
zXKxkFnD6|#rY8_ueai(M?a(Lq0~PH0h2b}bvyur>^fphE*~WQp#>iMu-++;I8n827
ze*J}E>p-X2>h~g5VW=$x%n91oY<)5}LBteEr{j)GA~g<qY=iNw1?ltJ)~nv}+zRgv
zSJ$$1zpBJ&SnT{wK&_Q9M%!$;@yGG+)@E1Z#IziP`*Q_t9N0Y3A4gv}`%ixb{C@}#
zT{DiwKA-u1GACc@K##s(VZN$B3j<4@wV|%>LU%kuuQSmI=-&g;F0!|EbLY^!_6aqP
zk6WKEwtc>ZCg#EQc~sR$1yx0hUceEmwq!U2DS19ShDg%1JlY*h@{PexkdeWl5ekkI
z6;h+cHia|+a9xLY45OML=JhGX(}6I;HAWZy?phG4zar1UsMB4^68eypnSjfsZZ@_g
z7snfH<EDv*`{tsJjgVhIz{xS|K~6!%Did_$YC4pJ=j%a@(||tvXu|UGw%W%u5@>LY
z{o6+j)WM&Y=!z3^)Cb=S1`#ECo+pElAE}Ijdko2Xh4sPUPQqsWA@&RB@i9|FU0Pi^
zye-XCFvg5XXbcq*ys2#g7{Io-4s#rMURV&`iCMtvAosRF1GQ!HIGFtsn0JgiN9Y@~
zMrwclvF_h$O6j#qeo@loWZ4P7%ch-bNOhOsX&5GCFr~KEBX2labbBcMOo9=4MvbP=
zlj=Q<`Sc#5tgc2lb&$oqG<r5ow>+Wbbefi;%~DD8+P;OFP41=s126{y6GP01;#Z~`
zm$dOa9p#Ke$${MyPuiQJZbnmdhZW<j<~PD4;dm+ed{jE%0U`N><7D<aV=McgHyirK
z-X(+BH@Se)Kl25{ydG~RZpO#yck!AW^q3i<bqhD4M_NcVQ6jn}KFsINTnUzGB^LBo
zOS<wQa5<bEYkn2>9za%8>l!Rq9!_4SqhBS}*$LdWFgW!SFwc;Ky&+|T&FtZAHkSQH
z(W67-DL+pHdE22!UMe265f4YW*ak=4_;Cvc<<S^^e2b<1l7K`2+qZmd_76q{Ln~Oc
zb28O%^)FD$Bdc*r!+ip$QQ~RS@~&F<J4{D49x^iW5!oVABn4`VhrIL&A}+>vCbVjT
z8Oyg}7M!JXB%jyqU4Zi_P5zYRSS>K>KJW`Rf~?ha_^pP~tS+hL(;}V~r&_4sO(-hZ
z{7#}DgP__mzrztytEG3ji1-j3xDqQciz}Tp3sW+ARMplq@(^(*!gqm?rFB06YxV;V
z&A^)x>en-Yi3o7Ftwvo9Qb{@7`b>S0-8Ig;N*>`D@!ky;6(PrcdKB+lRU3@wT$LtS
zUX)SBH|JLeag9{9(j5*KwLn4tc8``}@zW>Hsn!vsupgeH;Tf<=jK~4Pn>m$>MOhlZ
zQ-9EfM$U13k8f+b-A3CrQ0H)w{mss$gRdI{BdyFl6utxeFcfPy4%-jd21O1>p8TMd
zT*a~@RURdD3S%M8wmn<f?1x@K8SgM(@JD6?ec+FZ{E>8Yp)0ald2Tda+@=^!$${GU
z>5#5P7^&<cU~QjkbW?3E`WuyMV5v;iz4iwhL45o%%>$Y&Gy=0MC(5+WL6fjh2z(jd
z<bdQFb^;Pe7iOy$@}^cLeA<yL&e3yBx5xOh<2reTw}q+Mzb^C*arCFUc{@VUO01>F
zJS)F_?O9-}PXP&G=dKm2wWix);UHeO@t|?iq<ngfLgT<%Y<1wSfvmC&DV1r_Heq55
z?2y5hBuT>U0varPg;7MpGkeNQXtti5U#5C5IQI&Wl_taR<>b?CH{bU_!R_WPoeZ0Q
z2vf8fU;QW*KsiBUN{%cP&Q@+bG&8C?GMKJ3m~PO8|MPJe3{>Y4OVzj*TL_oTn)W{8
zk48*|VV^B1&)j0p8JM0EgzUo?Ngv4iBvh*~dV<ge7Pkj45J^wE+F=YiN#jQSLdUa7
ze2)Oc#uxn+-5G{@eP;vuA+2#;?sTfSHe6RDTc$~jujthI)Kp-EVnu}W1Bh*C`IADs
zJDx4zIn~zk`7%@_!Zagt`&}g(fbMBdBixUIk40p3TL7`~`&XXX#CSWYx)O5b=KR7%
zM{x*4MxGvUJlWIUE@-}`#p@Q8R4JnYli&rYxBU2rdE$hX?z<}Ef+8SoDl(YX(&6$_
z?3?_ZY>Fmr&yOCg<Y;)z?%-nttj4`Ta{)Xp?NtXDBp3!CO8`Z>R%!5Co1Z7_RD>U?
zQ>(p6wUDF8OsSeHWfby-v{Q-3f#=)r@1|}8CAlmC@LijRcZF>}ofnU}OLh-U1|iiz
z*TrZ1WBw2q(_OAJz47^lGLMkS<y-YX#>3wm55ACZt~WOkkEOiJra_=LB6S4Q^}jG*
zlx9?9{_Bu%REjkvlx&4REq$l_mb9L2%QL>^Uy9ZH@<#WR(2do5RH+saQC>&$V2E3^
z=;fk~iu*1gl+HH-7NBc&!CLX5K$meqA<MkU&LY?b20=w^o0rv#F47^U8uVqwd*Q0t
z<wkt};yPoW;QAEaI`CiXhe9W))y8{66s6nk7<$6@LmE9aGLEDth0?HHFVM9k0J^Gr
zERXF11zU;U&M{c>hgZp{<~Oru*Kbv~&M6|Dsq>EIp(gEU!~*IU5*sE4M~Y}zQ%CM^
zz;Jxu&l=D4uiH)_1V{2!U)sOg7_)VMfuuDGXy};5f+@27g5`g~q1lgnAr(n>SR|9N
zT!UZJq7AMTy7-Okpy11Y$8|l7lyW}Mc6<M)J+nvHM}fUmvlmfE<#iDsr@i2_t><^T
zy4cT+rUWI8O^qUz=Q<{HVnz>T^RJ>VujXf0ug{N~=hu%4n)RyKtJY0@zpvLs+bSC%
zknHxb`-u)s=pyRr{De8|aj{~FPR-`VHuISe`RdF;-BbF@-2ch7{Ns0%rTbF{{Xo{<
z@{{A|-n#1WoDX5?Lb;~l-#S0tmjb(4A-&;+My)DepXCI{^RFKL(O>%&ulmTYZCgsa
z&e><~`GzF)O(@B$BC=v;;CN&qT)yn6KvzA|BaZJfM;oGX(eee^&hc};lOzrLqzzdx
zW9SiO&Jyr~sI>d3@n)#DFcHo1>9WwQ!Sm^y7o;}^Vtcg7V%2_na^V|dI{Kv5>Su`n
z`;Z~^+lVsMB}HP=O4|^f;C{+MzG>3x8r0>`9!m{ReAIAG9?~gvHnVhdHe_~cpu{wr
zM>u6C2HDRM<a#qtu><z|el>P+ZpJ_Cua>8!7z4v&3~jjM(kW~nfhBUtE&wTLY6~+@
z02M{b4;-G?<MP_UsX1%vx9CjX)5woi9KP&EisgPyN7mWkz^z7%mV#csRtcs-=TujI
z;)@rq*RJTwbryvc@wSG6VfJk_RK;^)$L5~%W7XX!6m2f5mNYOcQmnL26H;p6|0pNJ
z1XbH$7Sz%056q`F*2s~ThCtYy76qNo0>%r@m@<S#3JJfH*1U09VvqQ~t4rYSZ7&OR
zl-fAjfMb<p40)3pCpL_rZlKe!Qf0vKZy8pm1IIa64A4tL7RD9YK%DxEx+ZhpsN9o5
zy_cp5_hy@+A#esJRV0|PV%9SlmDvFM!4J2dS+j~%5hB3JA!*R+>blAH9xKoAa+1rc
z<ZS0OaYaa7d1T|4G^ZG*Sq3n6&P$A&2bbx$%aTdFl&e`h(a{*V#&j=VRQcbvNMnbb
z?88QZNc2?R$fsPc@5<-tHu}n0AzR_g#T#hdYK+uA)U0&j@P*xFjI^eO2RqhT&n9UV
z8>=%{VVi&kkIydS$kruZ5-g!diza8o&v!6w&1kUy`i|Q4pYPcJuj({RnR8fU!3@3f
zjx_Mdq>~|7Cn2SPWvQ>R)m(#-2{w_TlmKITeUyLyuqlxQKW+5${rq|!!o$uwEEO_J
z+ExEq+p?Q^5%*Awly+BBBX*08Jn9o~F@C9ID0$P%mooiBM<97R?-nz0ca}J=t~a;m
z3+V49lsCagxG5Yq__y2c%Gh|hLf*q<_AD)qiXy|Sal_xBcDJeG>DY{qkYfB70>4r1
zUuhTa?VRm_R{x9o&5%bO;>6Asz<24E)>3bjG8N;bxgT6n>m_4VGo4P>6Ld}Hez3u(
z<v%UP-8KaqMaw<Erj=a=wjP(Z8~&!1MFAaNtdh$bWh5!6^`s^YitQk$3!>W)*@hyH
zrtrcMl_a2x43i52w1y6UXYz~{Pw9qVC`ov*hcf)!>*v|K{vqI8$m+ai4o;gV;3Y#O
zQO-p#Q<-8|Szy4aFLuikcpwT2%kFTa40k0XI7EPzRst1e!yoauka??kc%wQa^8$%n
z2zb$Aqmy@O_TL#|JNjk*842*{9Gw@TBnA?2PNT~chgGG7qQVdvu~D@C?HaWxKM|`W
zkHY8XgT}{5M8MZAvneh}$cIGz_qX*44t36f>q*mnRMF2a*d-}E75ieSrPNwijjgEi
zE=_1&vd%Q}1cHKv$po2{vJRsZAkOZXnr$38b72~T;qlF}qz^xju<**y`xmB{t$m-l
zZQ(Pk-gmvCgryZ&!j2Qq>3O&m+ShkoV6())2fVU;C087O$!U5DvYv#TYk2_R?*f$E
zO0~hB6WVs5o4t;%2yZbjLJTR4;$BJRdSkEA+tt9aWkE-?y{GJGoOIVG##`2_PT1^~
zysN`&`STl0qq)2Jf7y9uPD%yj=K3FcCa>EBi=c*H`9*fy(GKrlHlczfFi?FIGGSQG
zsj$xIzPl#0)?Er0tB?jddLn;K@q|ihYPAqbKJWT;vlsESv^XDa7-w_s{ZOhw+LPd@
zA<B5~y*wj@jau>Xs^TXfn6>Gwd_-ZcTkol|ClJ&!1%51?jee|9X%(_c;{pv~$kC4~
zHw<TsPU(JL3<J<$(HzQFkLL`BHych-j{Jpwdd4`{2u5`J)!$KfPO`kG&#bCSh~~aI
zu`ZtWupSpIk1Rc!1xa!Uw(HoHQlmuMe{RadwGOHRR~)$Fw3ECs&7ChRu8T!v;pIf+
zbxKK|fwWZ5CGsk#)_nI(p~lc_eJIHzZAtl%o(k}u@DgpNK4L;GzR=DJT2dr4pOAYO
z`3ylb=tFwBqSYa^5CuJm6N~VW=6IFU`3kJgvpf*=rebM}_>eiYx3X5M-%*>2(<6s8
z%pil<0Ey+W53(l;JXFb)W7Gv9sOkk6AX$1d+qCo=F%N(kW`q&FTW-3F{Y2_myo-W{
zd^)bPkU|m<1eKHlnhl8tg(^e=86XIIKqGt`+$|{ey=P+!kM2up75L$)_UyjfosMH^
z^t|449_705`cfBUeBlkFZ|guDTR?2V{PhMU`3&p(AJheaod1ir<9|Z=$o3oUZG$P|
z7nN=SY^@fJn|{Xk;O<7BzaTuyX6DzwW!|yKR5b628=J14ydMu-+nFAipIeXavi}e-
zt#`X*ZlQ9{SGVnAL08m|Q@GUkT-td#Keq9z;6wksbT#%(dFniF?Wvl&-Hib%rR7Zs
z`F7zHpd%4FKY#GWho`rCdke-b+E3TxRHaaZgfp6t=ZuEQY+oTZr)}$6NY^uybbPDj
zTh)w0cf<JDieS4q+%Lt-tKLFq#5I#@rXspDSp+L|uojYh%rb#*YW){Z)xGrm#3*^C
z`=arnilSz6s7Qbc<b)F&bU#puwV!E5q`k;`ZVuW5t~`K{2DzSE6zwscLnbgayw9Ur
zGFS%zWArDavw+ILO)5$3D98@uAfDzzFfgA|R4U1~b#zG21=ZF>jB*hg(wuegAJR~;
zdH@Y0u_#252=Zyr37T)^x1T2oLCO)eG|!6)V>Ds{P|WBL8s)VXVn8X@b<(1A^85vK
zLA5buc2ePSG!^fNPwVCJp^4wD(=P?mN$i$kbk^m|3Mau5aU9!li;|YU#txoR$3XgD
zvjsw~nAol<MKAOGaw6^D33B7TK}U1FivE7}9{3VZKqqn`WmDUeM+CfAlNOgN=FoBk
zV|a51v;W^@-aHM-iWDwQ+~!|m`k#TlVbY|{APcJG(<eNmzTAzz4GHco8}2Ka!|7TA
zbp>f^%pSw-Q;K_;p~jEFxhaE~I_cfgHLcPtiDw5G!v%`i9BW3y(5fX0WVbT~RO-UN
z_d^HU9gZU;8(kdxwhKwHy*<mF4gOyKe^C5PvE!B&v-yD^&o8PYYE5num!tL+2`t*{
zuO1oYbyLo$ljbB6ZJzUK<6A?Um4wJ{!dKmYQtd32_AXu3-*R60VlB_c70BQt2PTKD
zlu#HAN2HSMry_#P541>AOY|j0N<VOvDJPJnKQ>o+1&uoIX(sjt7DkdFDd~sQP}wLk
z*cPy?&c}iFK5GR`5GmylC9D8m8qsLkK#K5Lb&_RY@Omm5(`l%1&Wv1<69&_1Mp(ni
zoHBtRIk=!wGdaO_Oyvw}sKj!0I9PXHgTxa_)`Bzwr8a24XgH&??1&jmUsYdlU)5?j
zW6URTYD|Ku8|}r|kN1zywqytDh`kVE<lG={g(KqA&+iU?&C5txz2N@Q#}Vg<ADfBJ
zxW{x~@87_Z=b!!?qzUc*A;tZ_XLin^=pRzsFYv-GdYV5FJ;)_x;4mYWJoHnJAYc{L
zihsn56Wu-`^fda>peG<tJsTa3Am3G%+X+WqZ^qawHu5~QxVjNK)>1kbyE;PPMb$c5
zQhlu>Ph)~!Y}r5Tq0x7DKRk82KVI)%S&?IEn1L}l=J)ra$Ll4|%3-r=Hgj`ujCoHH
z5>p0P4<CFBDt{JeTGmCvovhF68at!H47rI;o&6q<_*}XLqr$|E-l!k!GnqKzb0q&&
zW5!AYru-gmIhm;jrn8uKMTZkZEe5p=B<mkub>vNi%73-@mtES8CyHniGRiiREa(J=
z*MRB-MQqTt8f<^Bl>&d2S`1{`!1#!ogVU+Psi9w~q26;~+%K}r6rs-~i&8GI)3rN7
z0H7YNMJ|#ex<yDMuKz-X=h%x}MAL%pzG2_>xS#|zQo!_QSOA!-`;5|A8V{gA1ROLW
zjm41v9tN?8ysJ&wSzklug~AyDj4+JUfS18IgP`_e89nh$7EwXTdHl0bI3M_hrSvE<
zDf}~9wYjk|mj0+c%^k^lqN7AI{g`&#coRz%miK0vg`F=ze0pGqC?K?~>WiB0gDIT+
zlyFS&J=xz-mt?McRyGws<$LcRFYTIj2SJXW+33fkjRx<J@x8bZcbKQt9+W(5`0QmS
z;1>jV9}dHRNP(GV>_AEb<oF*_q!`8({->_|z%rPzV6SJi4;)HQ#zs$a_GF*A5DZ=-
z#Y-SDn(8&?VWy9a$UMIH?JCQY?{v=UI14(=do;N8#UZHl*?ygTSxXgqz8<YKazeYP
zYWN=EKdC;)km{k&(HohBl4^0@0yOsT!8Fu#1kV24US2PJ^YwoiJ=dNS>g_!=fcXg&
znOgVUhhV)O`P;*sBW!;*$g5L>E&A(Xuu^`-A4b^%_<1c1y?)g)tG6_|bGmss*3ii{
zohJO!fv^hbE_EXyn=~3Ip_SXlewbs{s{X1D*4zRvBN$&<?)wE}K04C~N2P8^UTuBd
z0y$N|BSoQ;0~lzac;hMeGHEpOVT(oa#sXbbq>AI&#gw3CVRPr=C0Pn85>#&#zZRL%
zUEl=AzOQ|0h6<;|(xMhyx}vVB3Qmir$H0ph8UzlBBo32EC6@`d^JvV3!ZG|YtAFZv
zF=(BtD4$BA6%!ge*i|Si<PEDU##6Ve1X5d5Vrp|o!JEt_Ne%$0qXNw*s^fK|U<`vP
zvl*IZ=rS45Q+1TQIT$>bOm+6WA9%dWg{CvJXEOm!1d)npE*FV&-}1~R5g}Nirws5s
z3ei1>HwVGTUQ8k=h+8O>tzO7!MVdIt1Y_sSD7m`$Wg=2MVa7pC^-yIz!Px_JKouEK
zk*S%&;+0GxrZX$-&vi)&x=~yiONpS;5nM0)HIfms$?{>ncrae8K(?rCY+V93cnv3T
zNJiub-07%sTv%s30lbGaHn(Ct8nC&3d8h^}I5GDao|*^%68^dB0|)*&CCNRiT5E->
zTg1+@9yDWiFlM-qXQ);P`>h+T)N(3)Ja|9*5(x|$qd~k)T7Ob4`pkU&lPKr$!pJNP
z)B+dr<>_uldpFx*v;Et8?iQJkbSQmq<;UN4o0;i<@e3$nR{sBl5@wpAGbs%iTUw|y
zDKRh=U8Z1DXH7gVmeDeFn5)5cY@69b9ED#;O8H9Ghc5H-w=PD(Ga2>I==>N>Q2#Uq
z8Z<$S`5{qqg7c(Ha?*9RmC``oFi6FXxb^PlQ9(2;vDbjv{skKTA;(2mV8DN}Q@j@x
zu5Q^JTnYF#{Itd@q4(pdb|XL;?u{bE>_P*!({{nKIIsI_7|tGY=8UhE{)%6=jKzyI
z0YsRfnZ2UYY(M?G64<QB`VXRT&AN#3msiTmP%6#ar(e{Th3*bQVjjt%-=pIAy^oXV
zdW9ug?HB)hY@=LAxqz(ylXe+Z^kvk+aD^;q_)ggt5Q`S?771-7%vB}Q!sM!H`Z)$_
z3^%OqPG*=0-4`m>+ux5bj-0C`jzcZd5~$#9BwkdMB}p*xpr8a7Z6S|WMXi!PQF_9@
zzCQE5-c%%Nq*O2&JDf^y=7&f8kmnU_P>%S3)Q13xty<9o!g7OxMEctfPCD<bOiiP|
zDnPyZLv0e+TYJ~oUWbVr7w6cjhGIP$(OZ>!P~$$s+!+_I4E<bW79ohRHOo18a+fRN
znGwE@o%g|_5Ng|gHP|+ekU!eE8K1!?46UxY1)sq(f@{LWzMg00=)ngfFppZHRnP}m
zHeN4WR#!2iyl(fL89GErHJ>bKSN-Woa=s(?NXS^IMoLpCmKOQhP@9}AH{Ll<*-Pag
zCo4=9w9n>WuaV$bw_{!weO$}AqMIqeErJ3DdmWg5Y5hhv)i=5LzCT>i-ah4PVU!(W
ziHle-e&NTU5OyNxKnQ_2>4Z2r-**k{-=M=Sr*aK8v|Qf&g$tK63e6ozP?Gn<0M{j5
zVa7anw#&b@jpM=G!~2=>9b|4JT6SQKLK8BY;;WZ09vzTU`#1vbEE9kmi$Vd74iF%X
ztnYWi6eGC~LXAzm6M*G)BGvlgjjVGmX4yNt{b&E~rCTsZl==CW8q_7C$L3#P#BWu;
ziRbQaqu#5422I{#tK^4(C9XIn?LeCF1TO{>HnJc4C`sg|hGd$D&<&lP!8TW}{e;!K
zitAx=)+jQ3aBqx%3H&sOj`vV!p_@p0WRy{66^hx_nZvM2z9%s6`-n&f&HXT=;B{kW
z4S@R-gqlQiEXFZw_H_`jzaf;Sv$Ejs{rLOZhzExAl6*QnSxam3wE*SyB@XB>GkhhC
z;vuoI14-z<siWMSWbZL?R{w|=fYq)>@1vuwn=h2PXcuk`@1<x`Nurq!uWZ95x83><
z@u4bG^<RpYx|4DP`(uMx{%J@7$v6itXd2i|RCK66@rIr;ClHGsPO`=J@I=0EAxiru
zS;+_I@9ZBLvBrz$jGYP3(nVen<ktMOh=^w<Jn{4!e5WDF;jwYC7imulKmDD5yk<R!
zywCo<xpnsa;>*^UHN$1_JYz~tbH$>P5Q&<<Q->&sJ#X*^B9q@Y+hL8f#i4$2Xc9@?
zQAE|KXnSSN`bU3T82_$o5IK^|fl_nzJD5Or=dhg-r;xiA5;4=6MPaLNGRXRnqN+6I
zC&_RxkGu6s>K7aP<f%g<j41kH>SOBOs+t6Ai<q8%B!PW=c7xdAni>Hh1u3y=Z){VW
zEJfz0JpGisDjmgClo&-<4xf1-s|HnINix|mu6zQEV~7xjTMpk^A^Mk~s3n?~Y)&I&
zj&hBgU{)4i+<-0m^I-a^^+ngJbl!GZ(ltJ9&3(4{6LCCqh1h?6E8_VtNOGiEdy<j@
z;S2t9Wwu0b66nh!#n@vW#{-4ekpvY;f^)Z%?vphhN|z@@Zxy9DPV&|D&|@vg0)GSQ
zI3``<<=RRj>u}r5W!-lklTc2U-ts0dpS*!QnStj|4`^?vBi4RG_Kn=}tDECxf5;Bx
z4IMMR-FOx|*i|qQNp9FU`7%u&NEM@ul)>J}B8uHms$7>OiZiOacLUZ$CnnfhCNJ0F
z$eo)ENSrsx>D7oSG4+Wl#Tmaom@8W_w3PxsGJkqx_LwDf?}*~O3tdD;j48)SNAwK9
z%kA$wEU)HAzQCmOxt#v@eSN(C|EnCoRDIiZ5!8_F5BmF6wMb7(=0p<QrVbJC?%z$q
zef24e@ncf;#J5*ff|i+yVzx3ncQZ4&?Cg5Bn?{~13%dr@y)&bmf4!J4Q5O7(^5W9G
zxv@R>2Tk;JX&=Kjb>Y4|mDd++HvQLfg&gxn06A-yN5IlACs%I)J7L1I{ZYsL!9!<$
z;QNi=ulm)vr|8d57kmWOo=XSg+}Ztw2R9%?ZLOAMy-^Ec?(CiXP3<4ztC6RdPUbuR
zY?KA@n@j1RQH~DGWefYy97@Ln)m-0;8<Si4FGr6TJh*4pPfZLAGY%VRYeNqkbz>Gj
z>mGL6{{k=nb-ek>H<))Pft}+A1hO)O<ALuYxB2A>U>cmou$4#^kesO+fr;@pDphaz
zDrLvb`J&1vG7*cG4N~MV@wTG<0jZ{<sf$TFW6(aZPG<6S2u@~InUK;gyKrE!c9k+t
zX8LppSh7$334c#$`Vw$+i3%hIo+Paj@*x?~D}a1rQ5qf4jEN_LVo^;OIw0&*-E&w*
zwiEm&9(iCrX+<g|`fF5q^8%gZ;u@47O0$PvNw{8TsDu3CT8T&l#Sz2qtTm<Fvnxbn
z^7S#&o610*Cq5i-%U0?6F7QrGi$aj_)3<mA{nIyz+<w$26`R*^VxqdHL73HjK)hhV
z5eO7Uc)idOO;5?}c9JS;clf(*X^Gb)fTi}RyDmmp0e#9Lt6V5<EnA&rD^ndJpP!k7
zBM)HQ5GkzHNIWr0FEPb-{&GK2oI>snbW!hiKl$n)wEHatH-n;eOvDrvWpFN%YXeT+
zY^#>Q(LiP0iXm$ms!LYJ>!f&<-q(yT2&|@ukwY2}_OU=Cb<Tuxmy>cthG^guz5cDO
zn-NZ88F#Fg+7SO+`E;(oN0~%myoH!f3b4)MWK2(SWanN3t;t)4y8$!VgHN$`E&=fD
zOq5uvC3iOFpvXxlD)wx#m8B$yh~RUsk|ARCTJh`R{JvTClv7)wWN|YUA*&yr0%Soe
z7DSf<q~f$1oa;nL$(*F?XcbbMFMZ`|v$nAf?<nbDCOaNA`}5bz+rV?uB-!7gM%FOW
z#)B5)IT|Pn6y}SpNDEj*qekYrxjwwzaBPfE<09UxvW#(zwy{0Zyp8-jZ<GRCgWe(h
z(??cTVi#_bJ$J8gDE_=H{-<q_24zKxn#SZyDvDH+Y%uYP2~Jt^FE_QO`TCOL1BI5Q
zyk&aEBcTP|CS(TsV<}MeE>cW%k=5XOHEysn`BOD4FMHagWVV>Y@?K5vynFPfr~Q8p
z`};brZ8?_Np`dqCzi{z_d@IgP*^!9c?fDQS`@bdXmO?9IR3p!~v>~sCP$aSmR$ppj
zBv`mz2I9wrC8wC%r3toTXzlH^35)ENN^2FnCaYv0(cs~~Tme;^bDj?|R~=ublokxJ
z{~!>#^<Pca;zk^u-q6fx>xkm{ZcgjsXs~{LGvsn<{BM}C@*`D(zVmcOhFxmy@*~v;
zgAf4D{@26={Lk!z<$r`$vSCz~$o~^suI(iZ&NI<PVzA{A@$-LEEn0u2Nl{nCm*cwD
zfAz2*=P=oaAPUU9_{1HXY5r|}D=;29dlP7Z=?qsFc5Cd8d1`Oovzq-tl|?t)W(s_^
ztDDBGsVuX2T{fuE@$;hx3ibMZy7U6?rx$pl;|{$}iHwbHtR*a!S^T{7s`LBa{_cLX
zte*Sx!~nWuK{_8!367KROhl0m0&B{jn|B+3+KFfOcANRGvj+V#nI3JzB!}iK26riJ
zY)5CdN=utv*|Y7NVmBMn&esI9#*jCGPZNEAy=;J->{+&!mrCt7#hBqD`td-(Jf{r1
zIn)@-5~bC#Y-J>EM1~uDVm@Iw`xpZZr2<w1H6G2zVJ=N*-Y!kCi8T*AWnh~U+n8mW
z(!>CvWj?w)er+b5l_zqp2WxnvI^iWxXCk^rfEXhsMuB`O0RD9<l@{)$jhPNf)ut5u
zRqZm74kI3t)MDaw5xZMSHxF2eMrrQHH=-@8o3~5~Pd{Hfu7F2#FzL-Q068Xnhk7Kf
zb_5|efuv85SMAKa)O$zno(^$)Mp)pW$#Qri=&i^$cOt3A9<oLQLHhm0VbU;%mn^c|
z$P<tm85z+lfL20+bgL?3LHiCUop=f|Q_6=g{?fX_8LE32)oOk6_Q16r>6}Hl@T?)e
z7~LM^P}+(D_JYNPBeDILBEEtDlGOi>$5aFzK`e-yck}{AnwqGU9%3@#7;4b9#JnA0
zLrw{D=piiESMn|=p~x)<$4_>`mPq{UMG$6rTXL~rQufKC!?i|ah&<NfR$y|IP8zh6
zx;%-TIZimN<Yva3hh>(tgmwIxz4t4rJ;4JvO6?BF1w23-kE3;TCku-vl~hQQw=HU>
zen+Ru6vAs-0I^ZQibat6_BH5wsogkx4suLZv&8w{KdA{Ghnm92go?sES6ijUUh;Q2
zuv?rp`j+Z_#&<JgSYHw2Nu-GG_2+6*)zjP7J?MajX$6`X=&~%S87VwOZg28`nu=+N
z|LG}K2azg5BiuhAAUw2w1(C9YLE7lMu>3zSg~@?PTjfAxb80|Y><^*d!d^yLbHl4q
zcv2{~DG+HqB?RL7ISLVgL@oRek1o=e|7^us!}{OL9V!VuiqS)#><;&<_Erb?KQc9T
zlyr<5<v}&YTJ@2!d8U-X5+Tbe(eRvlS`$B)pXEaO@HKvN*pkx|BL0(61_w_1y3rCb
z71<QO>QmGumTQ5xiDOh+MwDj8P@-m4RU{Y<HH9*R5JR$xJ(0PJQW|PJGiTq(60OpW
zCn&zZO)wB(=lc%)*0o}!7{Ql)iLNNdf=41UtuYgpp|MA-79WpToGrjaIuAGwF(>SJ
zhNU44AOM*WE@2UzlZb|APv>KbCn{@4s_5y^sM5`#>COYQ2P@@hhj|MnWnGc2#H@#T
z0TTaKQCj4zVSzTus@a1ba=H~dFjYFk?mFtU)a4NLD!0jf(6}f_IzrPY^8_NuTosUG
z{m#f?XbDlJnHo*mgC&$sv52$6ECC~Wx?xOwx`E$Ds4K2VGeKby1fjAJa8242aCXHI
zP4q~T2*AjDSF4!cOlSF}G!^v6bmWO1qO{^P*5I&I;3Z+3h=>DxQEC+M*CZ%!yG8wp
zI$`KBh?welNlj71xb%W)@MhG%tmMsLf(yr!7O@uPtW89+ydm{;v3Qit48_9gbcUDY
z19V{Y3e4!v3)GUq$F6i?FnA$URa{c;lBEH=Ou*2w#ELGe8`&6<M3MH$o*kV?8WS>Y
zQEh8AbttP}4Vq3rphLaZ!~;4>#r`^Bok7^eWinBV-dmAk`>qfAqC(%P;r5AMA8^oE
zttLu9Yg!v+2q1k*4VXUY2z@A&H<38O(FdTOK%Glf<3W8_H<kH3DL_+5-N0}bp~DMD
z$OER)dD981^QsBE-<t&%+g8F_o8P*KN)_OkVhBj`@zp3!Bhtq*fsF12UPH-8t!+-x
z`6cHm={YqRdFi#JQLrQIIFc;PDF#J3AR*3>Ez(lq14W_{eker-$0vhQ3@~_tsd(6e
zLd+2dc}B}4EFud<gThd#>y9Re9}eGM5`prt;VpGky}%E)Jc3!F+u6hSJvwQH76DxY
zg93oAyi#oDsoB>az`5BBXEahe&R>jNYicBq@A=2{%yYgHjBwMnqHxdmK*!GK`VeBD
zn;6`IS%j^=IKua?{AfoF;hsN)#MoCmRnWxw^dQPm0|-(3ioMpx1qur`(=EyfZXnB6
z?Wp`5QQq9`ay9}VTuY+&TJ`Efomadwo`vbK;fOi5neX~65C0fX_b}|bdA0-V+9Uf+
z2io&L(<X2o5JQI_lT~O{rT^Oe5$z7}{8(cgX%U#Iu+S=#FEA!|&>^qqFFLoO;MZX{
z{fg|u4cs<NNZ2lNrk+gvP!!q&hWZYz?x79qRx@+nP)SfCm`y-w#ixsKePiQ*YR)WH
zMA#;_djFBns^4_IDPpSUaQwEp7WQxV)|s=3=Ys8;;59;Fx6QSt4Ziy%9>hc*m;$7C
zM)cMVs(-hUXwUi-v7HI4cJVxzy-5C}B6-{uY+E?g*C9hfT+!@3!)?IT**2arp3dgx
zVWxdM+w<s;=qM9N|1@W<n(Ksxr`_)b9wXd^lWhbQ-+dS2gvZ*t?(B9v@ht5TdefYx
z{%v45qTBj?-;V#{h9EtBU~v11g$a9Pc%V%OcjaQldsywCE7P3~iP>GEoNbAZ3R-Z4
zqx-f28+?C;X!CK5D}b9fnrY5TP1kRDWzcwOPn}5bO#23trY-=bAu4uO-n)ObdJtWR
zSY&or{SW#6lpyAiplXB$+OblStROr1|GS{fVrwB;53)mOU>s{9;jS>yE{QSmP_url
zXpwt}RXSQ%Dvh)|>&%`SYtYk8ri@DB{o}$0)W1K7%$3tJle4k<cNxqj(dXCd^kE^i
z0RpLH&(GMdxVt+x;B|PZ?amvpP_y365w?-{IvITzhMyRHx8sPVcfy$bS7Q+V@j(9-
z5Kcuuc^d*K`%O$8{Ks&v;5)S;eQXF||94#iOF3F^b4X~d)H@#(i?`|Oz^wJ4!!uAZ
zb$&p5yXZ#cnQ%CkI#}_lk@BbUi?ouLHd~x9Ub@SB3zW6{s?!nGSiW{VR}+^D)^`dl
zZM-~&)#>19Fqs<3V3Y6IblYZ7bO!;=i9kNy%)H!bBIeIZxXWKvZ{_$0)M<BrmiBIU
z!(PHr#L}O@`(;TG`Z|YyqKd(hb`1iL)7R%M6DA#)o{Lp@qTOHT4xSpT?!5cq+qd2X
zMz}uIGH@%cJ-wNh2iFF&O5<i-ZyRk7WN!bkJr#|AJ}i|rUzbv9*zxr^LeE?aIR<QY
zOk?#eaGu;8?%ltByx(pamwgGoxxDV)887u-(H6vez`b3)JvGkEVB^3vR=ohbgMq(f
z=}t@3R5JukzNm(_FD)N>-r0IrfwMF2j|F9x+6!jmMZ>4Qw?4c;Z$Ec`53s?8+n0;k
zmlyPXBLkq(GI&VR_+gPW9TqZ?V9*>Dvqj!+@@a-J*reC88H${Mt~#Uh@%V*}N6&M5
zmw}AnM+I^wu>0w`%J*-AkPeW7Ty(O6>!m13y~yS^5>2Yi@;CAZYdh^SGDY+1aW$5@
ztxXtN9_F5@4<#xGZ@_^l7Rsydw~Fel4wXBTj<7o&jfAo4$I_!1WszC7ND@)A_#noH
z0Mb78O^!&mVU9HlHk1=g*gspCp*2~7G{;LfZNI=>y~~p;TYNJo%V2<8xEefKJAwzE
zls1=Oa58_^pt&{sQGFwQX?uT;Ln+j#$a0)<FaCI3Y+L)zwJ0-PI`i*O*u3BBbvoHT
z`Y>=%&uajO>gW_TxiQ<)m<$?Liu-gCYLld9Cysg*!kUnSRPW4N((d{BRmgwR*KUub
z%C@D$w<3uIgJFOvi|`0|uv1K&o}=xfL?uG6SQ@CjLY4wyt&%qtYDUncheQr|ovNKi
z#3U0<R3$yq3^nV8M$NKsC^!m<pU5#aQUQ}K%_sDZfz3~Oo*wd5Hs5Nyx#8kZjl9hr
zOIQNCw3f@Xmm4o&#bfXdVIP*+EtPx5hbV=oa1tH7_Id)p;&TTo04TA;r-Jes?ul$m
zQG7YMXiJCu!H+X+^vNIOTL!(ubxB&v?{8&7{{*)Tsyr5^QD(hdcv&^G#*`(Q4@Jf?
zxc5L7CEZLTcm&n^-mq?ILgS&Y8@TLS$Gb!5wVPSf$XvrSS#aMi&@33tEeS|C6MRpi
z^>Qy;lB1&q*f#@}nTAQ##9Yz@BXt?fC5@5<;ggDG%}v23FtmJbB{&w79(c)0ehO?!
zb>7QWKj<p+j1^kj*w?U*0GxMhWzN`Sr6t6T!;ooQc*aCNbOt;5hASm3FoUPJR%PPv
zO%q|9hz3BIgNb4w01_sk-fK8lmlZShz)Fe>y!c6jiw;OTTIQKHWOZgz`z_=^H^)j0
z*@6*K;a~v1d`wE0DdeV@lHhAz(Y7P8>05Jqgr3XzbYiL<098npf7;0=%os+5+%##j
zemuMyDKCiCMb!i9#jpdZSr!5DWo+H~-hqsfYBVBoIs%<bT6h1h(r~P5MD*KLyn<^=
ztw(qyZ2(X#D0hq-^HwdKFx+d{)u%A0mS2^rQxV=po#)mmT0V0X*>T;ZhPwFB{&anp
z!BM^#{4`-p+`sI~DQ!ZP{z^iSH9V5RnL0`{?V4T_Jw9cAIS02hvRSU?V9{GrBO0R$
z430w?U$N0tsu(vMclD^+G#a&sR%R2kEwDadu^Bi+`n{7W9e;kUkH-=hRlq}8Tn{pf
z4LMF7zLU&=M8WAr)ifs%4^mh~HXPiSwV1rDcHs%UPv4h?(-G;}YLad|QU&G`l&ou7
z*R0?fy^jNR>#3IxWC;jnKy;~4;DM2{9m6J(bIOLLLY^W+gkwTPAR!!}%5!7A3VMoa
zss}!InH>D31f_H1O9GLd)VoS2`bn(U!QK*=RIU|87wlr8?1<FrQ8Q<*PtDja6x!Jn
zVI+*=z`bI{hH<$0HJ&?YhvtJ&M0bNt`_1%T;u}e_8Kx#)VSn0ukWN^9${bTFNX#c8
zgpNa6M1<%4`<_M$U?Zdepq0-@avR-Rg9l0r|0qb1mG+G<uns*V)3C*CWr^nC`8`mt
z?r-Ln(;}}81HvlS)iR+DxQO;up<O}YfaDfJTVP|Wl+1b*;bQ6GHf-N6$jOF=F~!I~
zsoSD5J}eO?_DKP|7X`31j*ytmwSyQ;`3wnnbN8|Zc-uek=nfCUVBV*oS-l1HXMpPG
z#9^b3c{u`J{%&lYI&$?-Ue5j#wbaIG+IO>IIK<eePM<e+-tI3CTc4+Uvo9axlamWC
zhku4ge}<LuSmYY|b;s%U`10lfk1Eu6{=Y)LJ)X(`{Xda2D@4NfCWnMX<vgoYh>+ej
z!YIYNgGNqkY`615@pdQ`hA1jbsR)~x!<XdTrW}TqZ6@2YHOA)a^L_jtzwhJs*YCgk
zkJsbA@9Xurp4aobp4aPjjUQV|UHdKm`Ath#_`Ap*<zR=(R`K?nS>U|81s=EU_54%B
z$<$0MZg}()s{Q4M%pHI@rw8`Z4#t+2VKxdKe{BlslZ|7qy@zw%{c`WhOoxKs;?$8w
z(Dpu~yh$(BC<pt5c7VrAL}d1jt$cIU4JpaLxJ_)9QwWNB_0i9q0Xns&)z#DP`epB3
zhefJ>KpDPtXv{Y3soB+<*uikQ5urKeT8*ChJGe%>ko|*^eNdQveoyG=tIvv#rN`5D
zlocGw-46t}k?dSJ_R&W%1<K;9Yl7}M2mx`t5S~3$MEGHF8o-Nx{}v#7&7!*Wd{5iJ
z6C(N_2b?oj_3i1hxfY{n#WKs0;LeBnq+0a5RX7&D*|-1j5wc&u+Xz|P5r25oDN(S>
zjrG9S4meiapM2)ota5FMTYvRLv9;ad@P6(O<^GAY{Y&mE@yUUQ7DIIYpm;%iZQlji
zghU)PN+v<p7}#?b{M7|)i+38Lfnj2*`!182Yi-x-=L3G^E!zCZyz;Np?S0R!p8hzu
zW}se>0ntWgXiOO2FDy>WL(5#2HQwX#_|9a*@jWp7AtcRNvUc60q*cjg^cJss`rH}%
z_-RF5rQoYe-^#Fo4cfy$Wn*vQ976BRVK?3kn9@MgAzr|qp%QBE5FSi2A1x^fO=&$F
z`QxHj?d^x^xFB_1wns{6AS8L7_Tapiyd`os`u0VpY_@~x+r0$_G`lbVSg(PtyLnf?
z!yN3;D;phK$;r1Jmh6L;Ibra!<@~cZ%z`d9ohkY<`{$?42g|<C3q<}`V=|5S54-EJ
ziaCwBcw7^}xD-U}ed+bRwx{Zg?a*O|&FfgjH^-~~A{pgQEtLs>Rtc_2E}SFnAO#|z
zYe!ns{Edgg*}rdC;Bsk1)Su;!pTEhzSrM-uBX@>I#9Lx2GX3&S#(dEEdg$~^L0sd4
ztAX5=2iDJi4@7(qrw{unD<$<UpUvSARNCL%i<%Km0umlO_`7SlBU;t?D<#=wdht_o
z)s<m3|Fl|CwCoj>s81jC^3o=k5h6Y_#cdiq?()F?AAV<U+~MkksU=77EnV0q{R?vQ
zz-U^l@;I7ZQh|&e<dSjY4ac?FXJ+<bhV%t-jQjdKKCC@+WGF)yN~{ibpn4|2Jxd}#
zm%5)8cQ<~_erqg)IJG*%iuEiGYU-HH9BKBqSdaUA`?Y@`?qUkNEpc+Ljh3$;Vhf5&
z7zV~tCPie1fdLTj^kwzuPYDcEwp+E;@qsngtiLNj?;!s+tGqjN=Q(4p>wB1Uzp`oM
zzW%f?`$N0r@yecuw%T)eTy+QFC=OttD+<`(8U_VE2=@*C&yE5*6@=%MwM9c;;-`;(
zRi}CJR|7j9xmJq%zz@o>KOdwPYP~A>)&1obGR(z{2Hdo~8n_=TS>_cNaV`xK`~S9y
z)!zi@4O1vl^!dLYRmfbKxnWvy+il}V{3$v%wqEQWk$&ayV)A9n4KKv*1pI;CJlv}Z
z`@g%FE6xzao=x~{2obd+;&zPmNzQTd`o)J}>TGG0!b7ta@*iWdoZQn*LCSEkWVd7W
z%b!3!D7<LpQFes+_D%^Xuwmc5qT|;MG>T+d276CjwL5&&F4WHUP^i_lqnEE7wzEHC
zf7R-+jg7Uf_0_APSDl^ye=CZvungS)-%}_@OX33qS$8Av{`;?to7*92GGA)<xQ{Cl
z{<n{-$^{=6mDur}H)<+pd^p7TI&?ty&0eD!lwL2w@g{QqY+UICjZrw=)i-b#zsA@Y
z<P048Iar!Nb3_MscXf4ba5j5-3?)ax40U(usBdOJ2EVcTnhSJIRcmxyk2Ee(&7L#2
z0}W<A$aK%j+{KvhKNNapv8T%?t#>KCxAR7W!~N8wA!q%RddM=5<!_Q54k=L51tHd+
z$*Rn>mxokZLL6dTK>QOBK6#t+Z_=6B#O6H*e^CDI>H;?kA9o}yk?TIss-cZ*K{}r@
z8g>n&Jh-erp<x50ez|OOODdrAV#Co}(vzKWhvYus^g>)G6yh?142>l^2|t7G{uFbU
z8+4ZRt@_UYa)y2!+7<}wooN6qDG7Fo$Wm%_<Tar9Gfnl;<65A}+ULsmho}Dh>$S4g
zAX=Z4X8_llRP!%|TMx*sG~M-OZv=M=UkWNq<Y5sZO{#f7mv-^MN;Bh-ySaq;up+-X
z@$#x96PIxcwRGyS`{C#%%H{lb%Xw>&lDIU(3-7X~816**VEnzQy%Jscr=L^NGP(+`
z?!Q^yzjmEok+0-h9fIVf(+$^t-)&`}mS1903~8C9@7qPF#Ak*u#|VrXF^SrcZ|$ES
zoW4XcopJy&k!<PZ^RjSqY@~&-Bnz3wo(pTv3{aXo;%C@bRyaxbX7H+K4;!vEw!e2S
zK%}vEg(x`(<hS4Xj>-Bsq@0*z2<S{h7DfexxK9!MyZQM(H-t}yFj>4E`SX465hu#B
zEei`@gx6U<V>jKg3N$b+E&5jH@$tgCwL4226Ayf5dGLJQ`x3%1JAz=mhxyj5bqah0
zKKt6}+Mpx*Ci5oO+TB#|I>sWX3HVrb%k(WNhol;8X^KN$q8+0pAqxvv4%Z={u}v=M
zo5mCTXr8nzWL_b>EP!@~mV+!PEJM{It2tfqZvC{)K9QH`V4JTm33~;jg#nQQd?i3N
zUI67wuOgzx>ya3Ucqb`XcbWMIb_|vR(QvJ#P(UNObGYu2WgI1U*n9TE{C_>bdgqRM
z&-HfYZMw31Sqz@~{NwjiB6rcLjY7Lel0ngR(Y1~Hb~YQ|MgF1-8zpve;!)9EQS3&F
zofo(Pn}^kDH_W-IK(QR-%)`3?9<#kR_&KeYkVy~XZ=gygJKObhAb;Lq3nY8mjdFrx
z-(!m<%I*7d0Q3#<LGcc(x9--cq#PlOz?GY?l^kY+SV*qxyyr}W*h;J?IaxCEg#ycZ
z;QlyN@^{Gt_+wZl`-%9Y-6ZLqB&9xlt!RGfPpJSN1EsfXGRhegfHo{x+Pqj2`i!<5
z9|PsIYlUCtC-AL;dbdHk{3STIqK9*pO^zJPT_D<1&s|Z=_LrM_M)gofqwxEi5T*F6
z-prLN0Q)HOcH0X(2>3lBd%2t5z4nHR-aegclC@HetEIk><2lT4{4A?889B^tncuim
zB0%#qP;c!v+dl(nMW|A|+pCgy%T=}==Z%i8ty9LBUm}aDWY5%Ak2OX$RoT=br(KW_
z5{%xv#H_C}Bcj@?{)oS$lkll>MzLMFwK%38Puacn5*2MsJd6nT_4sfJd5n`~TR8qO
zzSj1cu&2@R{j+{_C_1<;vuYU~Ml>bDW;}gCo8QsVXy72;;$`*bG+IgYSKIR{1SEpE
z8?%4rl5eoFAJPSq)AVq>edan*4`Ybm_p%Ign+U}mnK|wY6kj3k!zj<V`))?k(BUGP
zw(Kfw(|0snbh53u>g%i9L`RJEjLT@?be*uuyF20dbOxsUb`v(A!c3lShY2ma<lHWK
zB?|%pk!NCgl_2YO({cW{)ev``5vpjXNY}}G)R^?vxzHH|F}}Xi-soIH+6K|Te)GE@
z#637AH~-x)i@MwwmgE(q2%0@Rl=*zs&)rdSo=s<(@p$=hR-%ud<%Aw3!(SBIr7}0m
zUK9841;rGTF)IDM;jb_4er0E9_q+?<LBv2mTA#SxGXGt0w||)zEoJE6cR(f>5;ht?
z+i3V}(wP!IX2!b`^>q&tql&S0h6nb6*(=Nh-rD?~pm(Gs62x*BJoP9=YZOG!?)tj$
zT+q!wkeJ!r;@U*^6<H-dX}(iQh_)9SA`aB^BI*d`Wj*k$*UUG93;f2_8&MBW0=YUj
znMGXds5-(s(j)8+OD!s%$qsgH&md?~S(bIka@r@`EcTfgVDe;pI{Y4c2Ei_73Aq;Y
zXrTu?fCb`4%!`hQFyFj@G|o;c@>%bbQoaf5c{7O@KsyCwaWtvG$zTRp<dI0Ig0J|~
zT!9CiB7Py0x4BJhf%O4KF|BowXYIWp4|F9nYF%C|jWA+GT=ECyzEC6G3(UlcA6LZ(
zhl}l?sxW<4Dk)rSNHoTt8Fh_+i+zeuD$C<5j8LN=A#`9StmwwNvTBn#Ekn%Lq1xao
z_T9DoDx|nybgcznL~s)&GbPavmpcjWqVz@zVN8&SaTx`Wr-qblS!fc;h&8nNMHI2M
zl;b8c0p4PZ>KQ*1@+H^#s5@l{2=EuHeXUM_i-88i^7({HT4nEl9`pE{_rT%K&$hnx
zve`%^#+;_E{Em*ITD+B{%%}mT%lz+@;1NNh_|laBh<HUMXo!mJo}TNa&_*0*Io;Dh
zYo;KVRmug;4{o|w!C&tJpIzIO0@1#w8_eTH(AJ}mX7mWg%l@1?c(t&L-bFk@L#v>X
zZ7-Us@$V4X`0U>7gz$WUjOZ_?b5j>~P;QRlBE`)GzOGYRu*QIb=GgrR_>?frpWq6~
zG09&46;C<Otc=1nZ!R=ZO8HhO;8ios@(unp1lQUn_NMuHS9^b&o|mjpDNuf9Gu-Ko
z7u#9%_mm|b4Qm9KYt0|$t;+g?Myl!B^L_R2@a|=qR4s4DVT#UhI9;WCj3K1xj4<Z>
z=e0*C(V?R4ZJDUwn_tl9MJL*xpk8nqW=cqVhBSxrNtA%$qIrw%^MJ&b5-<Xvuj@Xq
zjcJcyzUF<Hw;%n4c0_CA_u-YaYMZKy=z3kz94(6DD3xB?wIVvtE@kaTY4J8@Ukd8^
z7ARZZhLgylb*yO)+O={jW|QSkOBSjPwcma>Q;f(I?ivCZmpC4@Y@s@`6HZwl6Vj!-
z*be_di?BN(`+=GJFh9si*nN;DGMh-j4Zr3(@#5O9VfKq<oITr!r1#DxSVf5bj6St4
zx2mkeH8Z}`pIx~{JBd86;9D4Fv4Qi&Hl-PVh->@(TrEx(lU;VKJz48slR*o{coaET
z(A8=-Cb}xpOUy!nu$M6h#9-&MZQ-ycgd32gl?e#{fNH&~VIAT3Y!lrm&IJ;UGNYOH
zENpPtSQ)*0UcB@{V9zgF4dh{WO*^kJ30ue)hdmVR;0sZisP+fo-CCot+3YU3MGNdC
z_QJt?8(!c)M)R+AkQh_qUXo`biOCDMhpJlc4yK%7n=yH-XL#>78n^I&GV%Rt%Sk}U
zILdcGJy{j~^b7VNWEW*yTB3CWT)lg!*~kGawhr_9>S^9?ueYR3d=C5`;fF27b_}|z
z$*apE(duF#q_c^;AJieM<+ytDlMioTOrYun4ceSJyOpWJot}4`o)&@8`w|JOw_Sxe
z48La;%Ol=f#>p|y@>1v5FUJCG9MghJo?k!Z!ggiWaS!ms^xbS%Rs=V6etpb-i{O88
z)#uj_wv>90PSUHpAWfa3>*(-}`>T3~>&l+TcMoOKHZg1l3mr%LOJckg3i4)@+6^VD
zQtToYhHEy@Y5XR-fQD^6U6tGH7R8D}HZoRwm)~Lw@Hm<pFb6oZn^<J7<9wNLN)#lL
z-@vcJPc<<xqWv4mtF{;Y05?cBOl=c?kOCR&rF(Y;3vRL@BTC%rd6?F;WQbY7Wz4r*
z4U3dS8XM17A*v0MEJRwn=4LT7YC#1fE4jD<TYV#l=licF@U}(_iF)~0Hd0rCO<^8F
z?1rk{4Tz>;D;(7wdBGpar@A(K_r~2cC(00vC7Yh_5Tzvf+=6586}RZ!gZosi=6o1Y
z6Qd2bloIY_EAV}t&TW4p-lBIx2ivXui#6Mw{~i^jz`u2q2*&8)&6C@nZh>7V5-0Op
z?o#}y?c7VX#~TUk>-@TAkL}&-b=6}{^xJ@fdF&<OaQr+%q3~D3awVrztTu7+7W5cx
zi`^p)MGh`}X;g;HAmu&Y9hOEd`c#Kvt1w-;8EPnp0rWo6IVX?p9MYSa$5>sYK{6!x
z!%QJ|FVZ-<J^TGk308CH(WfGXEvygGEsVHd%-D5XTtiV?9craa4ijc0jQoIz2ZA{M
zO;nCdK?-GZ3`y5Be7yW-CJ(E{G3@9W`8D<g3*i`aP&RK7&BXdMXH!Z&>f)<mJqd0N
zKqwo^8sZ|<bggJ;q)4ePS4K(l57AP*d&WDZ@l^oF8%PEHJKMP#4lR<XLiTt3HlfHx
z9j$QoOL<6p!oG0Y9B<MAyz-*pMqks(hNy#+qDZt#Vww!Wl}3;#C0HaD%0Lz_LCz8$
zFg&<lFKyAh`>LM;_Rd$49U7Y0CIfuv63MhkTmCz%RTfa@=G`rzDVmT?)ixYjIIMP1
z3-`L(21kLS#By$PJMkWSC5W+2hO4c1COUwsy<I=?QQC>{I$-EU_<Xn8jfJ<)xS4Hb
zW)*P{DY2)IhbEHJ(6<{&Ni!OjdBd~qZ%O~o=mr~BL=Dxl+o?^TiroI8++usM>bTd`
zF7cu4&s#9@Rj5Nm1a0nahLU_w=y>}FpW@sjJQ^Nk<|V3ZC1%DIsV23AEyR4T0Gm)<
zpf<PD&`z~LQt_N-O)ojZCpX!#94tIg0cOX!KuN#S*JrUcy-le;xz}+O;NDlW=M+j`
zy@g}%!)Mf~p;QHw8a@TR<RC3T#i}k^EpBhyU*Qq;=W!8gU}p82!gMx1s(yHV9&W@p
zK+CqBh9m{!Yz_HD-By8dlWG^TV^U4@uIo0D4AiCaTGd4FY3S7(29n1AnlK)4EX1uE
z@0l5Vzwq7U_x?aESlc7*rE7KXs>iDA;<=v+;|Uo<0v-@PB+$rB|GG6d0M9co-v6ay
z`OOfI(qJ)A!M5TW0T-lVX{dB$x~M-EboT)#simxKZiMn%(RCigM9w*$aSjNv`w2w=
zUHeKhT85ad#RGNkqo%DPTr&S4YV{~J^5khd;77AoT=JW#UKMfS4V3XM8J)4$^s^!7
z&*;vSP*<{qZ%Yx<lpl9vi=C>+=Oy1Xwu1F2{bTr1ksK-?{|VD?8ooN2%gk)B5z9dF
zzH$U9!ACyc9ToI=`+3%-(F#!5F#BA`)iW-BxM#qm%AX`6Q?(7W1d3*PCGH$Z75$fJ
z>H6>~s_XDGLa&lbgH#Z#(tJh`mL&&srFGkscneQJjB+ASMe_`N0W+Sr!rw;v7Xc}n
zTr<!G$`Y0r^58yux$rIH;#!X(<#nPqC%LMpXo4UV$hq9M2h!=vRUj%zb|v=EgI}<*
zlgc*LZ0Ep&{0An-ro;1D7Lnp3L4}W+<zz2o&}I`)??}fzf7j7U#y8j!EoQV-lccwN
zPCs(L?&+cAU#3m7PG{uWWDX{O-l_(Cn*p`@7xA5+XD|7Aag<wqZj%q3fp6?_QWfaD
zqNShbnmf5t<IxI;bXyiQ#Jh%8Ix~eXg6ijt$`KUkmm|=@P6~^RQBeFbE&lL2SxRG?
z5xY6?{C?7!k8mh?^`xD)=BV7<*xW6<BIiA-6-*nzt*`R$&gn=9W<Pc(_=PeV$n8+)
zDr4-%;V3Yo;{FeRFi+*x4s~WF_oScP;v?+`j^*l$*kVxcr#CSm{<$8Wd9Ep%!aNPh
z6()&Zp8b?SCPi)|Zu6>APPwZAU0}8@g9LkO!s~bW(CGU`8i_}Al}v`KJFgdRw|nAy
z&pSQciBya@=?}8~^nlMo?U(|#3kHr#4^}OuwVF0^iIK2eLclGXp9+bJWh2=<2G=O@
zY?*Yd<x^Kcn&!JeN7rwDYLsCqal;N3`=&Id)rIJYPBh=kmv;2kqz8q>*ObxK+MLZ(
zZ*CRqv60ZJW7Nw2JN>7dGkvp=83D64BE`VmKMvRg&)`g0vUf#}H*m4zYa!LAX<+XL
zbo|YO90dQUZPk&Cv&@^kutPc@s@Ugl>jiovcf_(IK23J~X^;-0UEh}lwu-5(p`~oM
z%R@-no{uS`LgSPW^4YU7qKk>Lxn=2u3MBb+i2XRVHi4y@MZ$^$<K{)L_}`j_&3F+`
zSoIB!AXla8Isck{fYkJ)(C6SMk3!<=HPmiIHHVD+y^7W-b*FONENUw4^p5K#$<67b
z9tW^HHTri=DU4O*gumi$8|U?%OH|dB7VM8w23LEgh)kJzALJKpEMJs$G05qWR$`5M
z8VMQ+6CZJMv6m5;-_@itzV<qKz;MB7+56GAs7RW1a|uvi`4_Po>&n-OQlN6WL$)^X
zS|B7?d_b&-RYBlvnP~RW8nNd1If}{#Shv&UwJWQ*S!XdkN=ZoGHf}W+fx_i0#4e$=
zsGRGXxdcXfLSdlY9@Q<K!1Wl>d2}TuM+Ele>sB+Yp@$c>BXn~KbR%eyMN)P-_N_P9
zC=xIo|3#o`p-cS~;lB8}*X3A65t^@fu3c}vV)?5jcVB}d_<4I8VfLoTs)l}pc)&?2
zc2nB}@ED<P6h4FB6D?U*;DcvehzG{o(XJz*3kj=MD;}YHbb8%R>#p1(4+)Z1au7d{
z(l1uf76=DBbNGHW)J!&ay}=>Zycv7}h^eg)UAmGr(<qx;8$bdlx)2m%(<;N)><dxg
zj}9c+M;$WFnv1c|NcfY@;N|r7a>QXuvO9O1lRUfgKR=f)D9^z%=zZMnZ8DZ*4Q3L2
zPKB9fTah!VHTTj7fS{CU9Y<EJgc>!IQ#%BT=bAQsvk*ETQqY2tjC%Nfz}|<ji?2TZ
z`tx9<{Xq44dCrsABX)UPmN^_48@lEYM8Jd{)7w{9&W>eYY?i(_DtKz8zIfrX^zCUm
zLF2I5aw>Oc;3+E20C7xwL0@TWCRkYRDDe_Ov3ToR5~Yr+LH+e&Ult`s&;Nb;ugfOr
z=r)}tsf00s)_qM4qHN!DfQj-X2y>531N`Wb-~)p`{KGBs0>9~;`m(2_{KW>@=X!W~
z_VH<#nEO<z#S1-=Eu`#`hHYMz@kuS9m}f&NrKY94twV$3oSYmT&@qf_P?R2w$#LTG
zZ#Oue0&+(=g$T#0Pe&vlOo%4W4=*XUjwQ^YZ$c)@>L-IgAF~6}o>4Q<M%L<s&xGV~
z7pP?5xv-aUT+ahkZYD^4r?*Im69qc-k6L{_*n*%lEp;3;M=^dwBWC+sOdv1VufL?C
zgMht@1T%6ZbTeaCLll_^9<MAw=r77!D7+YRJwZI6+=<nI!c}q6vnSBbB<1C~Zvmsd
zv;A^TMcC>d-~^Ps_&7MXhaROT=bSdgayUWBi#}h&aqAs$5E035g4!$4??x`bMG3Pv
z?6encXwpI#%#rC2jJZ>GyAjFME$`z8_{a;We-pot(lZdd7YR_&XU_zY^6K_Q0tuaN
zr*$wXo7F;PA$M%ODA+YS3UgIF`HgSC8d9@W<U@-Gx&?48s5O%p4IXEAZNn-q%DeWS
za?nJ3T6Vxv9Aqcls5H?5l;$+K>;%-zVu51jBlOfWolbK2Gq$e^-!XJdFMW|S*Wx<;
zf=Ngby|lnR_ZiYKn>)}K8Jl(gbP8_Yz$MMg9t)1?!Zf=H6-x5|sMCw``clT7-+}+A
z(_Vfc<NvrW;<4gbxzY<4TmG@2h{aUwo}}Y@Qv468Q*bIFE)()$<emnFTZ+XU3k??k
zSBZA~KT33Y{h?nnj^u+I0rv+tsPCUE%^sW3yTMV3Rk<EK0a+j)kCfL{j5T^u&(u|@
z?y!o~E!kGxnHdRKk6*y0`@o$S9eVFZ+LTDgK7U*<H-0p;WqXuDph8iHZ;hGYBH7wc
z)od2sylZi9i$$c)l$5aZOtTI?dHwQkCwY)dkXg0abPQ(7{lkalCoON6blbLBcIa>w
z+hk!WP32${PKOCsDp4l(?@bM7oaJ1?>R!^%qs;gpsaN^H>dk=XMh$!K<Dwdjm!yJx
z;OAIRO@s8Gvx{Rc6xJud0>xqq>cd9gd$jy^qnfc6s~-8l!7PV;K^LlSro<TK)$5F2
zuxT-NgY%gVe+3D~q~cObL$ty~tfx;;`B1z0DVPx0RzOUWuBi9xOC`_B+iB*ctocy$
z@8fnvs+j{R=Vy=9ymkuv<lnI8(Wj4*&TZR1m)A>;?1r?ET;So%r>a36Z&Vf+m4mV?
z%q(N3)9ODAzuzraQC~cKL9NC31pEloK|V+j30};~p!>kBbkj{{?NN&O%QsEv@w2B;
z+KBX~xmc9CGcJA(v$}H;-P7w6&SFbmvbAFc&jx{dDiKaK!J2EQKALd4TN+*;O^*$0
z9mG+;ad-^}J=0=CU`*VWxr{RQt>{v-`ojaU&Ue*oqPt_mng^w+{!<RZfN(V9SZQ}%
z^oQ7t4}%1X|2GG@fN*p6#*I?Fy69K2vaz-ka$8B;V~@i-Ez=!}P}|0x_v9qqjodTt
z50ENDoVRj>4qn5y#f?eR$i3z%-I1~-JBr9#dtsjZdDfs=29c^Wr`W7mpR6-`sabV7
zqj)x~dG~V4<eV2uc{zD~R;tGAwra;dA8G?LODD*(^7XBlvtR5{I}k}l6W?3lPAM(l
zPf<TG&u9kWp1p?0)b$6{uzg|x%2DGM0K{%lEB)rDPTg(b;A-Wh*gy16JJX@eCtQEA
z#6@m=EzKdphoQLW2`h!vG)lz|J{+v|NI%HTIL=JR)<n-(hhQdl+NAn7D2#vm=Uao(
zEfvR49}dZ>CY6SOCU(T7I<P$%_gS8er2D=Za}KEv5Y-fySs%N-s<?e~N9<&CfK>I_
zzwLH;WvpD*FHsHe{2vU!J9k9tkKd&`umc!b?19Kq;B{jy{C`2P!T4VgEDrn-bN_Nu
z_WpDLr96{VJ-Y)Xi%)fs_Gf_Dwe;7wB1*|GS7MPJj$Cl!cE~4JAK_><*FI5!My7Ht
za%+KghFsr<IaLx4O8y$+wAH$*&@t}3>L*7@H$9~1aCz^zee#2HEm4KU+gjzaY%OT=
zllg><O={g%GfJVAyk%-!(sYPP4SmsRLi$fCv0TDABCZ&`K9HVj7~0={n#4*M?=x>v
zpBwnPYtUJHuEg7*B;KZTM|*bU2yDVe7ckQHFxU(})AM^t-UD`W&sy#o!_Y6#)}ep;
z_OBcJ_H#}(>r>FAtG8}NAogn)W3M`&w)Xls5T1rfUGwW}-Wl%fxHLA<>)vBh`Gt`o
zPF+Lwt^W2{*^$r7#e6Yw>)G5WS~KWd{d{$0dtWV;l6ZXr^whg>V5z3)Oj!1w6?gZ1
zd#mqMw}mRnLV;2A!rqnN4VzPmSywf~i;?mPcTqR5YHoI(NxzDSf9(BmptyTsk}NrL
wXDGnS%z+VUR$Dkgh}-HILM~xAMN!w3)Qjw8_o*n^9kQ}gG%`BneOmFq0Xh!uJ^%m!

diff --git a/docs/search.json b/docs/search.json
index 7a1bea3..aa46713 100644
--- a/docs/search.json
+++ b/docs/search.json
@@ -375,7 +375,7 @@
     "href": "Appendix.html#transitioning-to-standard-lean",
     "title": "Appendix",
     "section": "Transitioning to Standard Lean",
-    "text": "Transitioning to Standard Lean\nIf you want to continue to use Lean to write mathematical proofs, you may want to learn more about Lean. A good place to start is the Lean Community website. The resources there use “standard” Lean, which is somewhat different from the Lean in this book.\nIn a few cases we have used notation in this book that differs from standard Lean notation. For example, if h is a proof of P ↔︎ Q, then we have used h.ltr and h.rtl to denote proofs of the left-to-right and right-to-left directions of the biconditional. The standard Lean notation for these is h.mp and h.mpr, respectively (“mp” and “mpr” stand for “modus ponens” and “modus ponens reverse”). As explained at the end of Section 5.4, the notations Pred U and Rel A B denote the types U → Prop and A → B → Prop, respectively. Although Rel is standard notation (defined in Lean’s math library mathlib), Pred is not; the notation BinRel A is also not standard Lean. In place of Pred U you should use U → Prop, and in place of BinRel A you should use Rel A A.\nHowever, the biggest difference between the Lean in this book and standard Lean is that the tactics marked with an asterisk in the table above are not a part of standard Lean. If you want to learn to write proofs in standard Lean, you’ll need to learn replacements for those tactics. We discuss some such replacements below. Some of these replacements are built into Lean, and some are defined in mathlib.\n\nassume, fix\n\nIf you are proving P → Q and you want to begin by assuming h : P, in standard Lean you would begin your proof by writing intro h. You don’t need to specify that h is an identifier for the assumption P; Lean will figure that out on its own.\nIf you are proving ∀ (x : U), P x and you want to begin by introducing the variable x to stand for an arbitrary object of type U, in standard Lean you would begin your proof by writing intro x. Again, you don’t need to specify the type of x, because Lean will figure it out.\nThus, the tactic intro does the job of both assume and fix. Furthermore, you can introduce multiple assumptions or objects with a single use of the intro tactic: intro a b c is equivalent to intro a; intro b; intro c.\n\nbicond_neg, demorgan, double_neg, quant_neg\n\nWe have mostly used these tactics to reexpress negative statements as more useful positive statements. The tactic push_neg can be used for this purpose.\n\nby_cases on\n\nIf you have h : P ∨ Q, then you can break your proof into cases by using the tactic cases' h with hP hQ. In case 1, h : P ∨ Q will be replaced by hP : P, and in case 2 it will be replaced by hQ : Q. In both cases, you have to prove the original goal. You may also want to learn about the tactics cases and rcases.\n\nby_induc, by_strong_induc\n\nWe saw in Section 7.2 that if you are proving a statement of the form ∀ (l : List U), ..., then you can begin a proof by induction on the length of l by using the tactic apply List.rec. Similarly, if you are proving ∀ (n : Nat), ..., you can begin a proof by induction by using the tactic apply Nat.recAux. For strong induction, you can use apply Nat.strongRec.\nThere are also tactics induction and induction' that you may want to learn about.\n\nconditional\n\nThe commands #check @imp_iff_not_or and #check @not_imp produce the results\n\n@imp_iff_not_or : ∀ {a b : Prop}, a → b ↔ ¬a ∨ b\n@not_imp : ∀ {a b : Prop}, ¬(a → b) ↔ a ∧ ¬b\n\nThus, rewrite [imp_iff_not_or] will convert a statement of the form P → Q into ¬P ∨ Q, and rewrite [←imp_iff_not_or] will go in the other direction. Similarly, rewrite [not_imp] will convert a statement of the form ¬(P → Q) into P ∧ ¬Q, and rewrite [←not_imp] will go in the other direction.\n\ncontradict\n\nSuppose your goal is False (as it would be if you are doing a proof by contradiction), and you have h : ¬P. Recall that Lean treats ¬P as meaning the same thing as P → False, and therefore h _ will prove the goal, if the blank is filled in which a proof of P. It follows that apply h will set P as the goal. In other words, in this situation apply h has the same effect as contradict h.\nYou could also get the same effect with the tactic suffices hP : P from h hP. Think of this as meaning “it would suffice now to prove P, because if hP were a proof of P, then h hP would prove the goal.” Lean therefore sets P to be the goal.\nSimilarly, in a proof by contradiction, if you have h : P, then suffices hnP : ¬P from hnP h will set ¬P as the goal.\nYet another possibility is contrapose! h. (This is a variant on the contrapose! tactic, discussed in the next section.)\n\ncontrapos\n\nIf your goal is a conditional statement, then the tactics contrapose and contrapose! will replace the goal with its contrapositive (contrapose! also uses push_neg to try to simplify the negated statements that arise when forming a contrapositive). You may also find the theorem not_imp_not useful:\n\n@not_imp_not : ∀ {a b : Prop}, ¬a → ¬b ↔ b → a\n\n\ndefine\n\nThe tactic whnf (which stands for “weak head normal form”) is similar to define, although it sometimes produces results that are a little confusing.\nAnother way to write out definitions is to prove a lemma stating the definition and then use that lemma as a rewriting rule in the rewrite tactic. See, for example, the use of the theorem inv_def in Section 4.2.\n\ndisj_syll\n\nThe following theorems can be useful:\n\n@Or.resolve_left : ∀ {a b : Prop}, a ∨ b → ¬a → b\n@Or.resolve_right : ∀ {a b : Prop}, a ∨ b → ¬b → a\n@Or.neg_resolve_left : ∀ {a b : Prop}, ¬a ∨ b → a → b\n@Or.neg_resolve_right : ∀ {a b : Prop}, a ∨ ¬b → b → a\n\nFor example, if you have h1 : P ∨ Q and h2 : ¬P, then Or.resolve_left h1 h2 is a proof of Q.\n\nexists_unique\n\nIf your goal is ∃! (x : U), P x and you think that a is the unique value of x that makes P x true, then you can use the tactic apply ExistsUnique.intro a. This will leave you with two goals to prove, P a and ∀ (y : U), P y → y = a.\n\nobtain\n\nThere is an obtain tactic in standard Lean, but it is slightly different from the one used in this book. If you have h : ∃ (x : U), P x, then the tactic obtain ⟨u, h1⟩ := h will introduce both u : U and h1 : P u into the tactic state. Note that u and h1 must be enclosed in angle brackets, ⟨ ⟩. To enter those brackets, type \\< and \\>.\nIf you have h : ∃! (x : U), P x, then obtain ⟨u, h1, h2⟩ := h will also introduce u : U and h1 : P u into the tactic state. In addition, it will introduce h2 as an identifier for a statement that is equivalent to ∀ (y : U), P y → y = u. (Unfortunately, the statement introduced is more complicated.)\nYou may also find the theorems ExistsUnique.exists and ExistsUnique.unique useful:\n\n@ExistsUnique.exists : ∀ {α : Sort u_1} {p : α → Prop},\n              (∃! (x : α), p x) → ∃ (x : α), p x\n@ExistsUnique.unique : ∀ {α : Sort u_1} {p : α → Prop},\n              (∃! (x : α), p x) → ∀ {y₁ y₂ : α}, p y₁ → p y₂ → y₁ = y₂\n\n\nor_left, or_right\n\nIf your goal is P ∨ Q, then the tactics or_left and or_right let you assume that one of P and Q is false and prove the other. Perhaps the easiest way to do that in standard Lean is to use proof by cases. For example, to assume P is false and prove Q you might proceed as follows:\n  -- Goal is P ∨ Q\n  by_cases hP : P\n  · -- Case 1. hP : P\n    exact Or.inl hP\n    done\n  · -- Case 2. hP : ¬P\n    apply Or.inr\n    --We now have hP : ¬P, and goal is Q\n    **done::\n\nshow\n\nThere is a show tactic in standard Lean, but it works a little differently from the show tactic we have used in this book. When our goal was a statement P and we had an expression t that was a proof of P, we usually completed the proof by writing show P from t. In standard Lean you can complete the proof by writing exact t, as explained near the end of Section 3.6."
+    "text": "Transitioning to Standard Lean\nIf you want to continue to use Lean to write mathematical proofs, you may want to learn more about Lean. A good place to start is the Lean Community website. The resources there use “standard” Lean, which is somewhat different from the Lean in this book.\nIn a few cases we have used notation in this book that differs from standard Lean notation. For example, if h is a proof of P ↔︎ Q, then we have used h.ltr and h.rtl to denote proofs of the left-to-right and right-to-left directions of the biconditional. The standard Lean notation for these is h.mp and h.mpr, respectively (“mp” and “mpr” stand for “modus ponens” and “modus ponens reverse”). As explained at the end of Section 5.4, the notations Pred U and Rel A B denote the types U → Prop and A → B → Prop, respectively. Although Rel is standard notation (defined in Lean’s math library mathlib), Pred is not; the notation BinRel A is also not standard Lean. In place of Pred U you should use U → Prop, and in place of BinRel A you should use Rel A A.\nHowever, the biggest difference between the Lean in this book and standard Lean is that the tactics marked with an asterisk in the table above are not a part of standard Lean. If you want to learn to write proofs in standard Lean, you’ll need to learn replacements for those tactics. We discuss some such replacements below. Some of these replacements are built into Lean, and some are defined in mathlib.\n\nassume, fix\n\nIf you are proving P → Q and you want to begin by assuming h : P, in standard Lean you would begin your proof by writing intro h. You don’t need to specify that h is an identifier for the assumption P; Lean will figure that out on its own.\nIf you are proving ∀ (x : U), P x and you want to begin by introducing the variable x to stand for an arbitrary object of type U, in standard Lean you would begin your proof by writing intro x. Again, you don’t need to specify the type of x, because Lean will figure it out.\nThus, the tactic intro does the job of both assume and fix. Furthermore, you can introduce multiple assumptions or objects with a single use of the intro tactic: intro a b c is equivalent to intro a; intro b; intro c.\n\nbicond_neg, demorgan, double_neg, quant_neg\n\nWe have mostly used these tactics to reexpress negative statements as more useful positive statements. The tactic push_neg can be used for this purpose.\n\nby_cases on\n\nIf you have h : P ∨ Q, then you can break your proof into cases by using the tactic obtain hP | hQ := h. In case 1, h : P ∨ Q will be replaced by hP : P, and in case 2 it will be replaced by hQ : Q. In both cases, you have to prove the original goal. You may also want to learn about the tactics cases and rcases.\n\nby_induc, by_strong_induc\n\nWe saw in Section 7.2 that if you are proving a statement of the form ∀ (l : List U), ..., then you can begin a proof by induction on the length of l by using the tactic apply List.rec. Similarly, if you are proving ∀ (n : Nat), ..., you can begin a proof by induction by using the tactic apply Nat.recAux. For strong induction, you can use apply Nat.strongRec.\nThere are also tactics induction and induction' that you may want to learn about.\n\nconditional\n\nThe commands #check @imp_iff_not_or and #check @not_imp produce the results\n\n@imp_iff_not_or : ∀ {a b : Prop}, a → b ↔ ¬a ∨ b\n@not_imp : ∀ {a b : Prop}, ¬(a → b) ↔ a ∧ ¬b\n\nThus, rewrite [imp_iff_not_or] will convert a statement of the form P → Q into ¬P ∨ Q, and rewrite [←imp_iff_not_or] will go in the other direction. Similarly, rewrite [not_imp] will convert a statement of the form ¬(P → Q) into P ∧ ¬Q, and rewrite [←not_imp] will go in the other direction.\n\ncontradict\n\nSuppose your goal is False (as it would be if you are doing a proof by contradiction), and you have h : ¬P. Recall that Lean treats ¬P as meaning the same thing as P → False, and therefore h _ will prove the goal, if the blank is filled in which a proof of P. It follows that apply h will set P as the goal. In other words, in this situation apply h has the same effect as contradict h.\nYou could also get the same effect with the tactic suffices hP : P from h hP. Think of this as meaning “it would suffice now to prove P, because if hP were a proof of P, then h hP would prove the goal.” Lean therefore sets P to be the goal.\nSimilarly, in a proof by contradiction, if you have h : P, then suffices hnP : ¬P from hnP h will set ¬P as the goal.\nYet another possibility is contrapose! h. (This is a variant on the contrapose! tactic, discussed in the next section.)\n\ncontrapos\n\nIf your goal is a conditional statement, then the tactics contrapose and contrapose! will replace the goal with its contrapositive (contrapose! also uses push_neg to try to simplify the negated statements that arise when forming a contrapositive). You may also find the theorem not_imp_not useful:\n\n@not_imp_not : ∀ {a b : Prop}, ¬a → ¬b ↔ b → a\n\n\ndefine\n\nThe tactic whnf (which stands for “weak head normal form”) is similar to define, although it sometimes produces results that are a little confusing.\nAnother way to write out definitions is to prove a lemma stating the definition and then use that lemma as a rewriting rule in the rewrite tactic. See, for example, the use of the theorem inv_def in Section 4.2.\n\ndisj_syll\n\nThe following theorems can be useful:\n\n@Or.resolve_left : ∀ {a b : Prop}, a ∨ b → ¬a → b\n@Or.resolve_right : ∀ {a b : Prop}, a ∨ b → ¬b → a\n@Or.neg_resolve_left : ∀ {a b : Prop}, ¬a ∨ b → a → b\n@Or.neg_resolve_right : ∀ {a b : Prop}, a ∨ ¬b → b → a\n\nFor example, if you have h1 : P ∨ Q and h2 : ¬P, then Or.resolve_left h1 h2 is a proof of Q.\n\nexists_unique\n\nIf your goal is ∃! (x : U), P x and you think that a is the unique value of x that makes P x true, then you can use the tactic apply ExistsUnique.intro a. This will leave you with two goals to prove, P a and ∀ (y : U), P y → y = a.\n\nobtain\n\nIf you have h : ∃ (x : U), P x, then the tactic obtain ⟨u, h1⟩ := h will introduce both u : U and h1 : P u into the tactic state. Note that u and h1 must be enclosed in angle brackets, ⟨ ⟩. To enter those brackets, type \\< and \\>.\nIf you have h : ∃! (x : U), P x, then obtain ⟨u, h1, h2⟩ := h will also introduce u : U and h1 : P u into the tactic state. In addition, it will introduce h2 as an identifier for a statement that is equivalent to ∀ (y : U), P y → y = u. (Unfortunately, the statement introduced is more complicated.)\nYou may also find the theorems ExistsUnique.exists and ExistsUnique.unique useful:\n\n@ExistsUnique.exists : ∀ {α : Sort u_1} {p : α → Prop},\n              (∃! (x : α), p x) → ∃ (x : α), p x\n@ExistsUnique.unique : ∀ {α : Sort u_1} {p : α → Prop},\n              (∃! (x : α), p x) → ∀ {y₁ y₂ : α}, p y₁ → p y₂ → y₁ = y₂\n\n\nor_left, or_right\n\nIf your goal is P ∨ Q, then the tactics or_left and or_right let you assume that one of P and Q is false and prove the other. Perhaps the easiest way to do that in standard Lean is to use proof by cases. For example, to assume P is false and prove Q you might proceed as follows:\n  -- Goal is P ∨ Q\n  by_cases hP : P\n  · -- Case 1. hP : P\n    exact Or.inl hP\n    done\n  · -- Case 2. hP : ¬P\n    apply Or.inr\n    --We now have hP : ¬P, and goal is Q\n    **done::\n\nshow\n\nThere is a show tactic in standard Lean, but it works a little differently from the show tactic we have used in this book. When our goal was a statement P and we had an expression t that was a proof of P, we usually completed the proof by writing show P from t. In standard Lean you can complete the proof by writing exact t, as explained near the end of Section 3.6."
   },
   {
     "objectID": "Appendix.html#typing-symbols",