From 238a47397f398b566cee18268fa96135ebb7ed01 Mon Sep 17 00:00:00 2001 From: kl-i Date: Tue, 20 Jul 2021 11:38:49 +0100 Subject: [PATCH] Started Trinitarianism.AsTypes.Quest0. --- Trinitarianism/AsTypes/Quest0.agda | 227 ++++++++++++++++++ .../AsProps/Quest0Preamble.agdai | Bin 0 -> 23259 bytes .../agda/Trinitarianism/AsTypes/Quest0.agdai | Bin 0 -> 12382 bytes 3 files changed, 227 insertions(+) create mode 100644 Trinitarianism/AsTypes/Quest0.agda create mode 100644 _build/2.6.3/agda/Trinitarianism/AsProps/Quest0Preamble.agdai create mode 100644 _build/2.6.3/agda/Trinitarianism/AsTypes/Quest0.agdai diff --git a/Trinitarianism/AsTypes/Quest0.agda b/Trinitarianism/AsTypes/Quest0.agda new file mode 100644 index 0000000..774efe7 --- /dev/null +++ b/Trinitarianism/AsTypes/Quest0.agda @@ -0,0 +1,227 @@ +module Trinitarianism.AsTypes.Quest0 where + +open import Cubical.Core.Everything hiding (_∨_) +-- ------------------------------ + +{- + In this branch, + we develop the point of view of types as constructions / programs. + + Here is our first construction. +-} +data Unit : Type where + trivial : Unit +{- + This reads 'Unit is a type of construction and + there is a recipe for it, called "trivial"'. + + Here is another construction. +-} + +data Empty : Type where + +{- + This says that Empty is a construction and + there are no recipes for it. +-} + +{- + Given two constructions A and B, + 'converting recipes of A into recipes of B' is itself a type of construction, + written A → B. + To give a recipe of A → B, + we assume a recipe x of A and give a recipe y of B. + + Here is an example demonstrating → in action +-} + +UnitToUnit : Unit → Unit +UnitToUnit = {!!} + +{- + * press C-c C-l (this means Ctrl-c Ctrl-l) to load the document, + and now you can fill the holes + * navigate to the hole { } using C-c C-f (forward) or C-c C-b (backward) + * press C-c C-r and agda will try to help you (r for refine) + * you should see λ x → { } + * navigate to the new hole + * C-c C-, to check what agda wants in the hole (C-c C-comma) + * the Goal area should look like + + Goal: Unit + ———————————————————————————————————————————————————————————— + x : Unit + + * this means you have a proof of Unit 'x : Unit' and you need to give a proof of Unit + * you can now give it a proof of Unit and press C-c C-SPC to fill the hole + + There is more than one proof (see solutions) - are they the same? +-} + +{- + We can also encode "natural numbers" as a type of construction. +-} +data ℕ : Type where + zero : ℕ + suc : ℕ → ℕ +{- + This reads ' + - ℕ is a type of construction + - "zero" is a recipe for ℕ + - "suc" takes an existing recipe for ℕ and gives + another recipe for ℕ. + ' +-} +{- + Let's write a program that + "given a recipe n of ℕ, tells us whether it is zero". + + TODO finish this. +-} +isZero : ℕ → Type +isZero zero = {!!} +isZero (suc n) = {!!} + +{- +Here's how: + * when x is zero, we give the proposition Unit + (try typing it in by writing \top then pressing C-c C-SPC) + * when x is suc n (i.e. 'n + 1', suc for successor) we give Empty (\bot) +This is technically using induction - see AsTypes. + +In general a 'predicate on ℕ' is just a 'function' P : ℕ → Type +-} + +{- +You can check if zero is indeed zero by clicking C-c C-n, +which brings up a thing on the bottom saying 'Expression', +and you can type the following +isZero zero +isZero (suc zero) +isZero (suc (suc zero)) +... +-} + +{- +We can prove that 'there exists a natural number that isZero' +in set theory we might write + ∃ x ∈ ℕ, x = 0 +which in agda noation is + Σ ℕ isZero + +In general if we have predicate P : ℕ → Type we would write + Σ ℕ P +for + ∃ x ∈ ℕ, P x + +To formulate the result Σ ℕ isZero we need to define +a proof of it +-} +ExistsZero : Σ ℕ isZero +ExistsZero = {!!} + +{- +To fill the hole, we need to give a natural and a proof that it is zero. +Agda will give the syntax you need: + * navigate to the correct hole then refine using C-c C-r + * there are now two holes - but which is which? + * navigate to the first holes and type C-c C-, + - for the first hole it will ask you to give it a natural 'Goal: ℕ' + - for the second hole it will ask you for a proof that + whatever you put in the first hole is zero 'Goal: isZero ?0' for example + * try to fill both holes, using C-c C-SPC as before + * for the second hole you can try also C-c C-r, + Agda knows there is an obvious proof! +-} + +{- +Let's show 'if all natural numbers are zero then we have a contradiction', +where 'a contradiction' is a proof of Empty. +In maths we would write + (∀ x ∈ ℕ, x = 0) → Empty +and the agda notation for this is + ((x : ℕ) → isZero x) → Empty + +In general if we have a predicate P : ℕ → Type then we write + (x : ℕ) → P x +to mean + ∀ x ∈ ℕ, P x +-} + +AllZero→Empty : ((x : ℕ) → isZero x) → Empty +AllZero→Empty = {!!} + +{- +Here is how we prove it in maths + * assume hypothesis h, a proof of (x : ℕ) → isZero x + * apply the hypothesis h to 1, deducing isZero 1, i.e. we get a proof of isZero 1 + * notice isZero 1 IS Empty + +Here is how you can prove it here + * navigate to the hole and check the goal + * to assume the hypothesis (x : ℕ) → isZero x, + type an h in front like so + AllZero→Empty h = { } + * now do + * C-c C-l to load the file + * navigate to the new hole and check the new goal + * type h in the hole, type C-c C-r + * this should give h { } + * navigate to the new hole and check the Goal + * Explanation + * (h x) is a proof of isZero x for each x + * it's now asking for a natural x such that isZero x is Empty + * Try filling the hole with 0 and 1 and see what Agda says +-} + +{- +Let's try to show the mathematical statement +'any natural n is 0 or not' +but we need a definition of 'or' +-} +data OR (P Q : Type) : Type where + left : P → OR P Q + right : Q → OR P Q +{- +This reads + * Given propositions P and Q we have another proposition P or Q + * There are two ways of proving P or Q + * given a proof of P, left sends this to a proof of P or Q + * given a proof of Q, right sends this to a proof of P or Q + +Agda supports nice notation using underscores. +-} + +data _∨_ (P Q : Type) : Type where + left : P → P ∨ Q + right : Q → P ∨ Q + +{- +[Important note] +Agda is sensitive to spaces so these are bad + +data _ ∨ _ (P Q : Type) : Type where + left : P → P ∨ Q + right : Q → P ∨ Q + +data _∨_ (P Q : Type) : Type where + left : P → P∨Q + right : Q → P∨Q + +it is also sensitive to indentation so these are also bad + +data _∨_ (P Q : Type) : Type where +left : P → P ∨ Q +right : Q → P ∨ Q + +-} + +{- +Now we can prove it! +This technically uses induction - see AsTypes. +Fill the missing part of the theorem statement. +You need to first uncomment this by getting rid of the -- in front (C-x C-;) +-} +-- DecidableIsZero : (n : ℕ) → {!!} +-- DecidableIsZero zero = {!!} +-- DecidableIsZero (suc n) = {!!} diff --git a/_build/2.6.3/agda/Trinitarianism/AsProps/Quest0Preamble.agdai b/_build/2.6.3/agda/Trinitarianism/AsProps/Quest0Preamble.agdai new file mode 100644 index 0000000000000000000000000000000000000000..6bcced3a1c9da145053b5840a6b1d6b0b7967ee6 GIT binary patch literal 23259 zcmXV23p`ZY_uuE7d0{Z#BjM15o=B1RAu>u#`TeTfLxUcA>YAvd}uQz`o2 z?oIdVojekHOLNOr!lgoa>-UVE+Y`mVM2*;BIPii;kRM=NT= z1_INJ7yX0aKfYGWEX%_@<||?uu*x->n+Cpfd#gWvO&axjleBr`Zx_G6N_w-w-0i>C z=2?fj*DlIm(UE63;bZcQZwFjeiKY7|?zd_?)MhiXedPVT4>do3yOQi`a4LV~754@wYqhA(pA*`XZ7q* z8Vz!1#!RjHoklt=<_n9Y_abfc!;V^lGAnxj(FaR$UbBP>sGga6fkqa1RC`X<3<~M8 zV`73LO;6zXY`pe`H>LAo8&?L*`wl0HDVxm~>K$vo!N);bRUqE@IdRT=4EN4oQ3rX+5;7c!}PzXLV=5iVM zAOvH+c+uz?!F;&~U%(od%aUj`9nFmSe2hTY3SN8rY=LeiNH@X8x$R=6c@D~c20LMw zIWuF%r_Vu{2eOCY7TieEy>;z-!dQDH;S`9Z8cQ@h_VScO>_mtlr zv!;3@?&?cojmV{Ymk^rROteCWw-!l|uy@Ag>bSd{3F#Qd5^O44Ls!gH^u|#EShF^* z6Fbqyfz1m$I0fxgc!OyMMcHx!1Cd-k<%?%2*c#VUcol4@~0Wwiu=U z`X!8NNrVNx)2+F<(FPDoEhEV46*A z*2b+)(lVFc%?V~r_j!?25$1wx-a(q)2rQSxYp2)nPT;AhwrVMQ;UUKx;}3f!rCGKV z2*de2=a#utxTfT$5wkqDg3zIgyvdvFQrs{}oA;{Og~q(A?Z3?bZVXP;Uf%2UT}NU^ z5s2!If6L)DJ5yU-w-7VGTW+Z~r!~-b3<=6Cv3+we?cR0F>?3#-?TEIk?GN0T9{;X! zlw~-=;k{~^PKEQ^?a+5Z5-U;=uOfhTxOe%4F`k6)iRE1})vMM@$(xqE|&r ziEhwG7lvpmi0RezBxJ(;UhAv^&V$p^BbJOU|w(4*f## zt}i@Jr~I<-X?@V<10ZLA{H2s%w0Kf4Qkn3U-ACxi38Iz)AZhpix({RMT#Q34m8J#5J77<~fHR#>(ezSV9$@S%%wf z;-pR9Fo~?6H;tI7I6)||Sqr*2Ic2%ZXF2n`bm(({!qP?YNK=6MG?dKd*V1k{GG|lf8oa@Zm2?HTrSJd& zI4T6*>YetaYNmqNQn6_&H!Y5}bE=}S6_q=8#+Ff@>2CYo_Q#2?0hkK+D90X&xXBxv>E=%1iXy;q2(-9@AAxpC{4hg1M|ug+J33+aUIAI8TU} zvVR?=dZaS4&jTKY2jGx0vb2}9`Ls3|Oe1AK4MpIa58}8&B`Y{~((3qezVZ%g4 z(RhiHO&`S-XLQ=>CE;c7Xi3P$GniecHC6auv zBedlC#l^U$E#~I1apK~$$UJAK@#1i2Qn};ON9<4>KxU#+3lRh3J7>aY9}_#*eu>jl z6l!7RYd2_<_2Lqt;Bvuq_Dn?>PHQ}oj2;Z!Fby4wn?x$tE8VCT9wO~*dW>Pv+;7uL= z@!1w2vj|m3f|~J#zheF+CW21=&O|yT&Sj_3PNRXOA8IBdhZNJ!y*c@>a7E!pboTdi zUMxEgzC?MAaf%nD@ARSM+YB7LIBICvNTPJ6icYF*0mO~K`k|w^;eZ)ccy2_ScYV=tWtNi0iIgTN0nwB+1I)vcHBZhx+C!VW#bSf6Tu-gjDmh_HY^<351B zR!=|4wVPoHmiXJkLEcqlwEQ6s8nMjAdfI#dYt1Nh0jT{4&q2Nq$i184ZmGdZ zmf;8d&|6FJ&T4S6o5_x=;{|_A_}fUbS_68|&=%HAU+wr)&2u!o)<+~@MwMt2b;fbz zAIwP`9~g}B+x)f*UDHn=0%Og!@ChahFyGt|9j@UuO|V$o3s^Y0Havjht~mS?6c2sE z?Hol-BxV(m>4XtK1uo9`Z`)J`9H)aVxIEYNWl$Sr{)v^x^|7c7$SH?TYw@mU+T!En zwg3j#10JTe^z8#4>{|L4n-DgD!oy-m%^t=Y+5*tSQZm~@(#9k@c>(c<$~HcIx_8I3 z`^f(c#(R}<7?~GNaj*ny6y6B;GRAz*1fF5r{V@)3vBz0TnnZfOI{tAirBl=K7{%`u z31E*i{%5#$eF;?Iv^F-K;$dQTHRG-Tn5^7pyPkp=2zye!h^qOwW*n7aLildB%Emc; zd2J5cg?lu>YG4XRl9%jjy}96z{g(;Dul9_j8D&)1yafwG+tx4%p-sQf`i~QL#|t`l zF*2`9_1W$8a)*PMpl@E^WGZ6`;d@kc1>>*wyd_^Do?Z>62YYalc42&tkg>)U z#v17kfzC)#^9fm*WWFXe-!OUD8Q=c2+(g~^#69?{t)j*Zs?Y5}*hl@Vq5e6Ye$=0q zyBuFYTSsG%0^ey0YfeEG`tXed!xZEa+)X;s?IN-|RpXBQ-)Zo!9a_N_*1Wl@XZG;U zSQl&P(#($uB7EQZ{LV4lV^1n4_j#33@Ag9d^X?c!dLNHZfy_TU<}-(P>z5UTU7r+! zlh75GNA@nHb@~mqIoM!UtE^VB4Zn_q)Yq1bh_5rgTEoYU5&N5s3l2nmFJ+9V6AT1> z{(aM^h07U>-XnNYHraNk4VZts-9-tl(`FYGu0yuPuhvr33}NNYeMA|x#l|J$RE;jf zxZBOY>Pc~@Hsc@qRnziQH6du90p_2?0SfEeK@}!GgoLNuUBrU|QH>5em85b_=I8{ymanNUSXz8g8ny))fw%-e#Qz*`Y80u>|wme%pMIAr+M zoov(T)1_KgQyH5fcao#5w1({4rjn&x2%vbRO@B9&EakORxw5Z9boMM}_#3hsdVvdT zN^45m!j>^Rfr6wUb?WUSuVBN@;cZrIfdq5W!NdTTxBbb36;#xp>vtgkQ>?VN0dI61 zYS(7mdDvKdiy^d-zXSL`9=GGh> z6ro2JUnpKfpPR;Iy@|SmaT;d6iuByPdn_G9%}3@%M#ppTwCm~DZ52`RSnB5D5{%fa zyQy++12Km8bJL(gE_FD#o{EaE1G3(n3^v_`q>8S?0C;zX8qPi|fKG~WHdk%QVs#Xk zIJApL*3XR>NEPOOo6lc=p~JYb;5S9roOrUUoJMO2U-$IutlE^%GXE%AXSJhoxH}bf z;N?+d*d+$OC_ayfuCv7t;B$Z}JBtt0TIhg92uKYxyM$1tLd{9Stnytm-xGp6F(W$f#2g8bvHNf;V}8wL}GU6YvV%+p9v_7`1y zW-dghba2aTGbs5!muz!hi}`-jZD7;qJk6ozYuHDp?DFdJXxLM{j-hDfh6aBKg4*d- zqHD$=)`l$pH|jZv#v&S{tS%EMD@`I7+KH(%}JLUg-gzsMhbA9VGKd ztgfAO{&+5|ZgBFB(;Cq?AJU6XAptx@W(apZd2x)UhH7E5&|3~_qUn8L44 zA=gJw{D9b-cIm&G!2Fr~D$*6&&gWvhhBu6=?=WHU%k`h&vo7M0DS2>DgF9wEzxYoF zD`QMhtWD?tR#2iPh@C-3^>9GyE*%o%qRc^y2ptJEt-6~>Vb@G|RnMU6-UYbp3W|q_ z%%ut_z@vIDY))`G+!(X&7s=bGa%MN3K z-)tPYc8VsGZzN*(bHgpC5~8kU4Lf0knY0&7bSn6OTqpLS2f^*1xb-IUv1k#DSHDb4MKFf5(4bRt?0$#G2)sNzwuH-21 z3+k+0o)>el%)9czDGa7w=g6}`YAGh_DkyHk@enSnYc3%0i6K`MDkOxMMZ&*-#Dr)q=q_wmtiazH^7 zkZ`V%!}A~n#qMYyQfy|4nsSOWqrrLjAtq6_n{tK18R}M zhKXe1e`%3%;a{}RZ;BHO9~VCT5l+`QAZ_zejjKFbaUF@Sr8npcVr|I6-!Raynb5DR?x5Sg^$q^hzybU07=$r-Od6)^5dl@qhBGFY-KoJ>Swise)oBnlQ zEHlpGnh9B00%0l9#rU1xg`Sr@FD3q1@_+=qea(K%f^k9;9;i{uN0b`J0tQh|z%=SD z_VX6L(HhCKIV~lOcHG#z~oD4L{F=ac(~V z8OMPjcM}@)Ekdk;AZk&_Ik2FIu0XkiS@9VyaoGr+uVV#tR2?GJ8iK!mxQsjud6WX_K))xs9%Tul$7e#!cHP+9?`{W5{c#;Wb|S(sM_-5$h0Z zCr)0PaLE8m`ADR?X)r3RrtmOL@dk5-5%OdQz*7C8U$zFJz>C$YfDAh9AIFZ{v(Lfg1*^ zz@Z5yQ$X6V)nYiBykx&<70w!1L;bV8a|-Q~m~#8j?L(@`4CdSpsm6gcm7BnwAmKzP zaHW4DA&7M(3!`yOj7rp!Qyw~U<<83S3VK#)1qaleXg%P`U~UN8t8(5s zZRfNB;zzPl3t;VP-WcZ8Lb>vqG6bdEM?UH?%q1g@dR@8Fo(Z+Cn73w_og(*Od?dbe5)O-{pUNac95$E>^qxi1yfS!mMKO8)wwEn z&mSaRg1Mb&-#139z*xxzx>WN8T4B%7^gUcopTYuH1p=!s-822DKhj+KRd4*^pXvN7 z7o#~m)i|(a|5I%5y+dASL)w@BP*HUPNKmzSj09D$==_lO-8kzgVyT}o>GTF$)ErIc zM+Y!62Ut@f@m-D^XM9y(-rv=+n_wk!8JXtT-lQd}mF>IFHkpqZ^JNbP0oju_re_ad z49|vGtT51FIwSQpt}pAt0!v*WB&7qky*9A&zp|SbK-jAi+lSaJbrR&1_8~4`wWWV$ z$DO*})njzn5AUE(wCh$fVOeX*603gi_e3e#MCynoBi52HCa+_n#AwE#o#(e{LXp<# z(rkDc7bRM%=3qWeCXiXw;j~XOFVS8V*026S-0Bv_1QW*Usr~>w^PWj!GSw`GDYPM! z)Q*t;2zh_C{tg;n{PxfU0sPrisVAiKM{U*HXoa^0BUOX;@s=kcHBu!rwa>vlDj!Cw z!5DY@s8%@@Q@B-;-#U{0Pyra-yaVLySXJMT?-=7Tirzo*QGj9zyv|2ddblkw^j zoTGl zn@a+kf(0gfCh7_LTbXJ$1eE>MUR`(WLY|B%XFha9qnN2LLMq0b8p08&m#QYwiL#Zl zL|L_gt^TKjI}U2e9v_U(%uR6k8qv48&8Y20OEHx&n&LqHcuxZ}#u<^OVQU-YFQ^)XD4ARxZCZBr%a>hrX70U)XZa`9=1N8)usi z-?LRO?6-ZXd$BYvX=b9iLY5~e6(t3{<%m_MYFI4wQ(E-<`8-X#?OJ`$+8Q5z19bRx zgMSR=ZQE6FHaF6i(&p3VgaTKE+!F};Z{V44PbImLmqIc=VLsl3y!cdmG#4_|RVT82 z9iBPzAC)_nn>0>6t^dZ0CLeFDB3^tJ?M+hNwoo7|#C-l6d;hP!miqpBF>bc~he# z*$%ns=!ImVLwip_UV!(p5j_TfTNKGmZt}J?Kvb~Z! zpnl90E0+saK`t1PU8~oT_uJQ&0w2A`0xw@!r7i5gqVK~}n=!pMDOO>;z9uG0OWDvp z^;*52y#LCJD+EjZh8Df5De(REiYteQVM9dg__^_2dN?M;Meo2AN#E^CCMfIX#% zBcZ*++1FVjbwIx*gcQV9vUqe7*^!M&Ym=$ctfWcmb^W8|e0hJ*%VZti3Jvj!pwWqp zK}tag@)DJrKU)`-K8#B7rvfJ z(o(#%KR=4MCxhKbd1BRtes2uFg0YSQqjUI*QPcJtxZ0jsSTr%SZ2fF)`I0R=yFItu z>U1%|Qt#=>XQ$lL5X2${x)M;mfx?1)s&i4`sJq&dR*V|R`%7PpvW5Mn5$3O6j2?mD zt&CIIKrjF5UBHEVGid2ds&2H(u1w0BUiBdTDAR+(^ms;9dtwj8Rof|t#VB*crHbVs zeB54oc69$$eaII_QXGZ9qCj)sCKjZFpJwa8hGpQ^Y@NsG;nMr{;|1x{P~hb?n>55K zb0kcE+J56@^tw$C>c=@zGZs5_Ggi<8E4+5<=C}8|3*Sg9>WxwPO)awHhSPO|1v`Ce z)XCvGSG5X?T@(mkPC|5U{J6=PQ(T)KA}_HbCY zYA;q^uLYQ`dPkSn8^E#k7XcGYubc)E>pI4YWH!x0UBXaM5UzclD{3uIKR~2@;Zgb< zO^>noRdY`N;8i7KnzHASJKma0s1^I40&kgytcG)tFCu0p;OEv9a6+|{ zPQ>`iSk2Z_P_cDedI64qLJ#YYeTktWCbXK;ob^(4*d|77|ckEtR|L+($m z`V$kRe?*yA-CJ+bN0%QYt{zI#L#f+%)44C_y9rK1$(Yn!OsA%K@EUduP?_%hR)GK(*4khF(4XS*)wnAuRPsea&nJRtE>5 zKl>(sW05&&8sHG7!K=ba(*sVh=SW{7@L{$7H5TpC@vzUxzRCgLf07kW7-J8+y^@+xGmfr3jd)cD$0jFW^6J@Vwt2LQ zz;T9=XTFT9+LnGCD#X-nLec@Tl`FUDLZ#Dy4N)+cP1Px^e72E1-DO5F!LM?wI-5Sn zbbk78j6n^n3 z2A)qG!cS{}`UY|kv<~`Q=Q5D#!P}l+PwI^fF75re1f_o2LjA+4a;5R_xWQ$PVe{)8 z>3nL&yZf>Bq_77n&J)`#qz=y>%-yv5uH_FS?tn7i(*`IreQ1Uki&u33D058$gs`P3 zl~)zO)TQ-hv$+zwRGONL9u5myTWRSEB#xNYYCx9{3txqsw;unW5nbsrAOSC?u4;9n z@lBPiJ1FzZwyFoTG{Kkw|3|d<%cLs*^uxkDrsi|>Dx00R&8k(O!huR#XE2KYvwBks z$Buj_o92KX-b~##krXb0(-y5(ExP>X>21!fo2pDqmq&8MRTt9jvD9sPz^Px1DE)G{ zI|ETQ3k>)A2RJuC<{3zjMs8}Is%*#b6$EGj*89`637@G*-oKO;GgYrzT5(ecl@B|U z2lon_FlY%4628VrAw&2xTE9U_^v@=yWi&)^x-8n+SQ90^8@l^(<+Ef?hUuM$&gb;z z{%y13!pzM#lGdMF*m&;Y5#z~5vkDy_e7!gKVcIF<$!8~xdn;PF{;cW-yfK(2zT=to z&4ZLjV}2C}9(r^8g&Nrr+5-#%&iO<{C@wPmhPSr zEtHaAPyS=rmq@d2vW<3N8oe9;vq@9d#;wuC@vl}?esbD(2l9ANb;s=7?;$}BY`@D^ zO@|br~~z+x@HVIEj4~e?Dp4@f5PP%wRzSN}zexY3mq7<9>vbLYI79jK5E4Fi~ zV;Q|@+?voJEMue474YXcJ^F1^w}D(k5uoAt<;7GKVqhNUFfl2%A^o#R*W zqU`}quLP~9#yufKW!u^vEd`T8&TZoIvbwO0Kj=RQGW7a|O>_R<|HlNI9Nc=(q&2oM z(;tGL?~X?)e>jnguAlWV6%^?U?CvnGdp`-hbK4w*T9!Sze}We8nY?B< zrTC1=ve;Rk*vUW4*66{<@qZ%iL1f>|C-Q89l$_C#W%*~7U@5~wM#(|8Um2+VcOE0N z*X}yS6;u3rTw5^dxnexxWf6>)+XZCk3CZC3&jDX`8GrRHdQ?tZOn84X$I6~dDLk|U zlfEs~0fceHJe2hjS%)v_i=gm-w$$sJlh`)-4=RNurOX*uhibSyU%ObQ4+O0fDcT6VxL8jqp&I3YJh>ES+O zirc?iaufn~QgkK%JqxiOEypsp3*T?1=^-3{?+4+hxJw8+X6$h!vGu#BR(Qaw-Yrf0 z4SMOnUrj0Qnh7Rp+4W$nAKkI*$-jI24}F6mEaPt0c1?&uSEC(F4B8c7*6(w(K;U8w zAhO1Y)K3(UlLKZVr>kVT5=05jDBE{75KWho=_xH2@1oP=JRz6MCWa(yH5v>aR z=`ceLXXbykW7IMszyPdAdjP7L+r3E1m|E{6X|Y>I0+7rWzd5>M`c$n0=wy%;0(J+vN-eR=q=6X`TW-7*y9xjU`c z+ECpzic^XN3&A$cHGsEpj#G}7n5ySF)e8laR^`K`(yS>cqe$L2k-C_G>9$xsiW_5{ zvzG}GxoN-YCJ39yla>(p`(%viwuZX6!k?E$-Qs|;^*%0qh3N~7rJOfl<_(XQU@6

s@?2Xqfn0QN-d7GOxd&XlFUt%&*|+o2nyklm zO%=dm=T-!M)qKx+bOX!SV)@98D&x?sVdKfpn5b;`LPuS}B$v>8zz#iNYMV#8=w#o@ zv9W)S;j>4Q1hn@U=@o<~@nvb$R}JzXt4AT2xg?1LbkuY1EnI*d(RuV70~R~xFz1#L zxKoSDUorQVwxH%Q(!l7x`9P!$!2hDDTjor7!CMH@!)(V@fMCn5oWl#SjK1ZMdSGBY zm48|B9g|Ngz4+GW*52*544u4>dbE;>{Vh+omqw;y_SJO&R@>u--}9b6BS}cuH3WOu2v< z51o)o9O8X>uis}RQ)*u_!|(wOhA0|^@=H!i?Lsq&OF8&ZWPia+4+3V(A=kF|h^GXk zZ&rQZD^{I4c;n*G$7D@V6zm7sRYcq z{3tD6>DQ<&C=6lyRrq#x(?N+d1|}&BBtvCC6z$e%cU)u=xu1#b+a@F&-R5z4u>wX^ zJYl`k<_cmZ2n2=S80y%WOyRfBJ6IaY>2B?uW7=4TirW4o!q*|L;GUc4Y=Nwk&4wP~CmpD5z zG|#{Bz-`@uTMUww>lS6>_)d7O-}x_Ai+$bHsfEnt&(GZxFj-j1WCP_#t3{&*C`A=P z<#*3X)F7qWq-2#Q)6ajNi+(i+7osTaaAn*YmCAxAE4n8kEF0?;? zFa7rTF~&R;CjxIIPUQ401ONPrGE_4zfKLRfjfdx6?_UjTZqzjU1WsXMkNO${6Mi{0EZErw$#U$_||h zD$yR{1BtZw#>AaQ3Mge`0`R!>n8$)kzk+%_T)*3M;NBstb2&o=aWRq& z{jV|oX2&NAuBfav$A|6Lc}w{(N`b4dbxpo%OX^}$mfNC$&T1ycFKxVJg7BT%;CNf6 z;__66;7qPmO&ZIU_7MM$C#>kAw1J!{C5Rn?RmvTCe}Q-ry>GC`jI$KQWA}rSbL3~R2g;d zRDLRK`d_Ri82~A~ll>rtXt3Y7&Knp8FLeg)Ff){B2(SQTJrLioOXwFp^xozO*gf^# z%wz&#J-}7|L@7oD0u8N8-uUXyp-V2I(HBRA40t`VRR%z3s!)F0Qy>a&u)tI0a)d!W zHL#dr-4PsE*UFwFDs#2VflB(=IjIwsKa#1M0wTvj1yOi|m@zO~cw=Go`4J|mK?MPK zb*shdX=62EGFPU2Q&fosG&;ri#wYUNp)9rWw^4W5i@w=9bP9nm)$x%0Ln&3iJ7i%Ts=1gsTKl1XT0m zDEzyzQz0!@+Yaba3NNU!P8A-*W(@dr-d7&DG|FVl{DcFlXlCuR*V^5{$yyMLEkgkH zqhp&J#ZFp0v}_p!OGj`8v)fUuq4M3&EQTWfwv&T=9VUp<7IXw(&}O3Mmayhe#4C1% z;MnhM0-m}fB=#7il*FKAWp!ufz2OR?+zB^D7njzlS@&{~8$)>=hFeU) z!Nu!PTzYY$W33LN6y`ixao2h-uyV}MxkVP$h61<}W!-4G{yD^JAU0-3xFA*M85Hjf zuxjA_Xt5(RHM?$san>&%%Zm;FqKuix1{1)d#b%tosR-}dM~fRW2CbPE*4UuI2ujrD zAFlyo;w*mjxd4@8&MqNY3-8}qs9^@h+C<2T?@#)Kusjy40SFtTuaAe~%lH&f5SgHV zN;-$iFUcI7OesnL{w^;@wB+jpYLDid2gYlU6*2C`uYnhf&pRC0J_WRhg6^jW-9U?& z*<&?ByeF9%7Ua$m^iBd97-Y++YTUZ{JS~o&0OrQtTYWwZoYOaZ5U#`Jmz;!qI|_4M z#>fWfpgTaI0Ec+%nn`hUtWg}R;TwV-SQ+dCm;1Y$*IJ>?vq(t@ zKxrJ6|J%7-tX)9wvLOZ2S$++ZFJm!0>J)Ch+2|Po-8Z*0~I7OxmK^ccO% zg2aDk`!$TpmmvMx>-SUIF^#ChTS;f!4=(#0Bk(Q*I4W51O+>!*n(Lki*SC8XrbxV_Az$C5NIX0^t>Nj|VlNc;K*Ycm zA{}N|3o$0Xlj00@Y^E0{D*&+Ijr-O8U2F;3=g)t!&;oYSYC}PwNnH|$H#{CT=e0>X zviz^ip@*G&a|e%RWv%RuF{JVv=YI2szWQ*MQJciBDPC2(1>OsNo5djeLhTmVZmusa zr}p45rw;U<_iY+1^)`nok!zE5W%-ZSCj*5BHesqMpv7*mPh3MIL}|yz9}F3fGWrR) zWCRw={n1hiS$;`zDPZ>_V!TvJxRrg|YD3mF&I#l5Zn6YXLj+?V4D55FUZ{mMWXmHX zH*saf2cmQV40()w;#q?ALpb@e`@E+(UOs5o@EWv?g( zD(}O+qSe&u*m3t?VkzO#uz!=*bLFOktLqPk+wV`*I28d&_PpsJ(SI{LJb7#fS60Ll zm<~!~Ib`!;x@;>6xN{iKl2uNzdyFu6k3MS43qw}YPv8B%BADbtbW6A0MMO5mvy2lRruMuh8s3i;Bo$))eev8S(OE7ak zl-g>X$auy4 zIJ$p(-Qz&r*8k1&5!1LXUX^ZD!a;f+^O0jmQr#*fs<*y1J~8u-1J^I#l(cd6i(|>9 zheZMNhA`xpzmd*q`xv+b)XOxU)W}7GjNgff%+~yB1fs(BWpxusCceU|6ur*0;I0VV zp4zrCCXX6A&_3eOxJnV9)*W4|7B-e%_%;;d?LYJ~#(VzIzcHo3J=^-9ogMOvd!9eE zA}+q&Tyevv$1SdOUeDA1q`Y?p9iBlwZ~E`e_rBP4Az4RlTbn#XUGQQwN%j0}GMzLx zdEV%n{^XM*1O2P!jGFg{)Q$?&$NNW*j3m#HnTq%-KE5~9^mKXiRL)0-SbVRoQ|!3C zEBVtSwmR-LnNj~(`g1wP$#z=0ZtKLo3pl0En$7v$5nEHsewLF5~eHh-TR@&u1hrh?wu{)Ra|eA++46=YnebB1r_J5fQ&2fNKMy^g==oDnVY z6|6F*TQMXgtxJprfA$JG=3|a(m&^pVAY)_|6*RiGE*pz*GZO)~)h$60nRD{5u=>RX z`Pve_Lue3im#E;99wiI+E9)5PXJwf&?`bCpXnCRZYcD>sn z1*5avZoJ&%T5{uM$?34b;^WV>#Jm6K)vhyn8E>$+r>^AKyFWW}=Z-qM4avjiCg?U^ z(O>DSN{E{uGyTG-F=r#cn@p0oR|k5{kN$bz6yaxS%YWjoh(-)cTyqN?hR3VdUF~J7 zvg=%rl~0TL7-Nwi@0=T1*|fT4NY+!3Y^=^M+UlZZxw?0uDlgwVyybYmw|HG}jJrBp zzvN`QP2G-z&Ze7+dKVd2_4l0H;g%~ae8~^IjVq!Lh`Y%W3&HUOiyPD08KA`q%zrSc`e=r=e&(hvC6QW&Rc0M1r(d z&!U39$J8xHE9+KGOf>KKB#wTtAO}KWS{=yUlriEKfha$C6&$2;t7}4){4l@M`0f1Y zwJrL_)5BW?TPns2jzc$NvfQ{MdIASRD;leuy24lG4zs!hM#D^{!KybjyKa=5AI+|$ zRL*6%g|&L62VX3{E{?WNbZ=fr1^wX<+v}jAzmT}de{@kL0*K`ThIRx-L-_XKe*O0B zsqzs_K4L|3>b&u(%~o~ZRrl$%5&e#y<0Bf3h~$I)AmaN5i2QRqbP=+yyMr8ay{!^m z0DoqJ7q_@YR2(iIKmS~ok!zFOWL z&NSkcG0AED_h~kGL9v%d_fMd6+W&L=Iqnw=DyfBIZ5YLs-Ai-oh4TT~y;P^(L@=8{ zelqagsE)wEb8r7~dU{7dpm(rpTU}{EykG}dX470a#1~-p}X{ z2XS%pc`>@oP)+jUkU{<`Hi)}%h#G>^1M}#dcUE;!t!;V{ zKXL!q$V5ZI%Qqr51EdnyA5H3LDyS!}E}CGv87#W(&a9Oycv*6|KN%>$y~I4FTMayI zNmTYHokEOewu1It7Ud@cWq0ct1DUrc>dlFpg{*yXS%=!`tQNDR<-$5RXVFuE5=(dl zXs=oqE@o8qMV0;BG%HX+z0RtZS@zb+TYk@KV;K z#^oT&f-CD-6+BxDR2cbR(=I$hwJ~kSSTDm#jk!q1JI1Z--&g^^NPvNCM>Xt}tvxgZ zFPp4AOqqczg=3y;xdigvH9`n5;iwP4gR%6m7tp0e1(a`_UW|&yETIRlh&qzfdijk0 zZ^kTLp^HVRM*ZNnHZ0%@)_5Q0^yWjaj3OQrSB|VWTTnKMC3u;fw$%%I?KKzHmKg1T z2_S$**=g%A{Y{Rs7K=FE0QKHY)RX3KyyuvxKB8#9RmpJ>_nckHPdd@-0h4mf{-^I( zI;T9X7iXGoNXP705rRcn=ow2NsAyeWXCmYd5uN&%!T)-XeES|iiV z>yXu$!X`unr^j{$E-re|yhGfPs{@MoLbuSg`IyGuXounHKfv)BG`SbN6qK`WJcvEa zcI5h{{g+8970;1=oo&XM!(*|TMnFIvOxsJdn#e@2{rww|U)p2fO?Db=NUw|S@5{rq zVFqg|==R~>9iT|QebtYqf1$kbZh1g!iJL;=EIU>me;1+($sY|;xz^dsy~HX(M|R-o z-hQ+EWAYJ`j!}71wm{D<&BAKpY2VqoTWwl4RSXHvh+{Qd;x)XfVV{ayY5(#}1WD<= zt!a7WcTr1$#{4wTv^5oL(h}3uX>-!@CXTnc3$9spE`ADW{oNXXhx>BCP#JBHX_*6F z*&l6l8H=dU^VPXYzccCZ-22Y9J@N2}b7R5F(Q*IFe7BGHi#iT>lpHMI-SIA<=kNaD z^P|F!H8G|0m~7YIR3SZ5ZZ68ZaO07bTe76?loONOUX*5y<+bM*nOx>DY^M&X%c~tF z)!CV69!vL*tmMC|YTiS$E9?bF^gKcfSum4?9e+ODvmd4qgpbJ z*McyPOv9;SKBkqHO|%%%Lf#b?B!~+8)^N&qI}z?1YsBP-?L>CALqn`=`1DRvOrNz#V4c{E8FU1!4btc z^IjVy898t(;oB8%W#u;{m%j}fo|RzQYX?g@xmAm_`6^;2O4efX=kQKQPltPLm=M`b zLXu2tVpa0r1;#p&Hs3idHxQ74!%d=y8s1FaWebRw-D7i^!Cd`K;@Al-qnHJ|lKDD? zZ2nbLI_I{(Dn5UA=7?)}Q0%N0?X=|@(S#^g-g^fj*%$Hy02)$ZR_lG5x0|r8fL|T? zp|m%cd0Cf`#9~lS1zJf34HFfXxOIgk7O`Ufa3q!8`z>v^-aG$c1I8~^d(+&J)>6e1 zoLsxrvn2#`w1x~R)tP;~{8x?L`rSDEyGCW>9jeFgxSQI$rJ|9}*=pOuB7G{G-TY`* zDYyd2dV=*`u0ZddmMo>$i{htwb1P*UJ(yowDXWr-^#+rc&_d4&E^=(K=Rrk7GQCGM zVfj}uM}Zeh_F_VUP@vb%txSvOS+Zap#zLqffM@w&{0@&pus7H9;>c3AdXv@(=c2cAdwme1SfI~Q*AKDmmd3PFcBSZs!3bp5k@VicGQ4Gom#j;t z@tRpu9oY-p(=Z88S7llVzS1&CYZxqfx^03onf-!P@HsQM# z%&Q}aq=r4ns$+V=U`rF^n3UFgg%*1I%+`?cbnys}1HC=8@D9%wBw11E9}VuY+M5&n za#|C?M{6kGVSY2KWePaWx?%}*@kWl*MG4x1Ruc_ogc(Q*7!ILQUB?vMme$LIl%Xlh z(7VT$)e?SbqnxRvRe~8q;Fc8kxs^))L%t=`&K9NhpkTp0En4W>;z(5r$SS@4dSunY ziV3u=1t;e|DK0f4-3MN zx)9d;3o!kPb;wqDMu!$&35U&S#7#obx@`YCJmULgW_YYIS+&vhjJE8H*_Z%VS{N-I z_Jsd4w&mx+LYMRNc(V2pO(~{v-!@W5CiG(0mhZV~&g)@1aKu6{qphheZ~{?vN0?+u zMhvTI;SHzn7?tiV^1z`x%&03IAr*TqMP6yHC5JJ+`|EK1{UPkr(%9)J;`^lgmK;C6 z3FbH=YXQ;{#m<6wXn}hm&+gwzX>+D3djnuOY81oqUa*l&-h^dYD3fzVWd9N$&a^tX-lQe}e-l?8mvpwpe@N++rA-?anl?_W zOId-WseC?@nUzgeU?^&tiVCQxsHhdaW~wJHuiQn=hqeJqf?_Bxuf`3OG6MxmH1{Di zGb_{V{m^FK;}5v!oO{3L+;h)4zlGoLS|;6kw|7AETg2K0#s%=nuO5PlNs;6oWmVk1 zq(e`4*d;kUH4pe~x#~*6z^{AfL$4?5Ai&A2`UL!RT}n6kW<-A)Z`{ZDH1KQ+_W8Kj z{L>rgV`K9_{0DebTa!#a4O)JNC#^Ss3jK_7zS_{F9?1BdI1fGf=FDfe`E|~z&-(97 z;pPpUZ#=sQ_it=?qkdL*tQ8m7qe z#`V{}HN{Pt{K&ewbGx_2pKG=q_GNAHyc2@XT)UjLwR6|u`)do2#5iMF9MKA?(p?(lB8I6__63B%DBk}8_+wEEk#+YDFuz7XBuN@NI z4%uta2#$lKKiv*2Y&O;#(EfG>%KPzmv6Vi z8IEZma@vm78=X66>w_NUvqB+leWdB5Al>GTu5od3khzgPv*<(U3g$$>aPQm*KiL2B8r5?n84JVV4y;2*cnQ3{y7Zra&BOIojzUi^{qhtv zVFDQoSfu90Z;d(FRHTfe{pP|*o zS8$ypRAe|{Xb`*(-E*cxQpL4l^C3Ui^71#p>5=Y8=Nh6`!rtkFzVeJ~TIGt-yAJD? zle{+&bAr6=>5pEW&0rU8vC3ajTSe!q?3JHAuI*TGQ z*vmd(g9j!sDnSZl32lXMgldiwBf7DAD-LfzlPIR98C^Zt2P(=958qvt5a3T z>L8-8;8WAgcQZCdN`_uV%{BMR)b$H98Q?S>zd<9c!5M0k8qY_Ci!Ke4hd<8n?vT{+ zy|eV+-NC!y_HE@j_V#s+PfB+}>fAkTF&Qf?@)WbGkJM`5_C2nO2r&fRXmUW%`KD6V zE#%cMUsG*!{@>&~E5>9J3c|r?4A1P|U?D>CIJ$MXO_Z|9KwaXbUwi(&&5)W;eRU`h z9-T1xnn85!QZ(I~n_N~3avx(4kbO;OTgmiDP}Jn@Cv>f)eJlJwYW7wy&{h|>2Pyc` zLRCMpvGM%e^>vIAuIca~h_Ol-fvP}BB%aO-AV!Q%^f!JCRui`J=4F#LX8MPFyBo~b zfLkn))$wo;X26WTP-(ken#foSvOe!_e6rky1}XNcly=nbGdL`z2a1$lBlL+V0k3@z z5R=2a6tqx6AL1ujf;Z|pxYrw%CeQsl{uH)0bLfExVtSdLgMt11gXag(eR{XAF}vok z!XbrF+FWBQT?R%W@>XuSHT<` zR{rf^Kg zu0?v=ae3g%qiJR~%@@)50^^$uL%`6L20S{IX^A$01zmomx+LfJ0KbJQwm6>C)`ww9 zfP-E|i#@=}39%6>ScMn_Gl#O2^)!n*JA(- zSjKRj5Ce)$=?h&P>lkyZ$mdE46aDHX!Zs*;P!c(FG@ zldzf3UW zu8&Gw8n%#hR!)R%pgM;!Qcd5L4o6wSVMK%JgwvTgpR>dNgF4^R#|ll3`pTLQ0S{=N zS*y>t9FtFMPUmo@tA?W{xrIR&8`CaziSdPIn_wlrZuvsl5u5&$zd7=no>rCVyG(gl zf!wuLq?=&-@VT|Co!3r96QZQI-q}O{QvnJIf}!Gjn?@92SsU5Wu#BvQ&LMq zHKdn%Cmml74T?jvrT01{o<^vdMIo+?k;?6Wq^qf=d2%8L*E>QLxio}fU(y7pwGBf+ z|0~~)Folrjy9Je9hVimLj!{<5kX~YE>Jt#eUa_q)DH|g?2ziT_NIw1*Rg=A~8Yt#9 zl5TcJGwPyWts2*EnN#f_72o2L!SZdP*JAnE?LOr(|DYDG#RbcaND|p(YMcd1&FVr1ep_O#qWgv+w9vj zI`)0@EQ=fd0Vs$#z3S_}p@3g@e1`#mUkQ{=;iXm+7SanT4?!|};7H9IBfe>K?n>a@ zJS(k_Dr|l7PxbH;Fse3rinF@q_jL_YIP)KdPQW|TWviSD>wwj@-!!};6@p2I(m=03YoSx z1>T&SoF^~SaPP`w+$I~{U^X4lT3Xe e7ic7c&AN!qzT=k|Ea%(>^j&hzzpJzvW?w~qg|**(9cICbhPIY6QJ zz7K$ZBEoN1t7OoLuYfE`ZWiLJgw4?=`hI_#n~#sZwL7P(%Amb)OU}F5xhtnCtJ7`P zI=x?OLvxkOKVSB*nOoh`y0vv*f1lSp?=)8*QD9SA^v8VR{X&d^g_x`|6O7=z9zdb< z&_o*=n}?Wjv_t?!77(8Zr4WU;^=VwZ7N^oR0Hu)3_EqK~AI<~H3r3GVGry3j#ea?` z-(}w-v3*r}=k$}PTKrqY02L?cPz~8-m4J(nBce%Ht3-Lg37LLxd^T$2>erW_l(9-t z9x8^luz6_qnwBs4-A6AdEFBvAq@O#6fYB_?Gf_jA7EEJ&uu5}YC22Xb21)!E&jv&B zxLB0F{4JCn*?t!H)x-ScW~heX3W>c7uz*Mvt;`_nkp5j+E>2=^-mcCmB$4+3C4^5r zCM$oE#EA7zz$O5EObm#GCR}OTs+cO?j+4SMKc&s2#H*mWnOJ2Fes>-MvXJF^B&UGn zD9-ckmdfdHV)CI-mKf4|BcW#O%8iYMKUA@nU=ubIB{ONgG6#RY^KuZ~tO)30H1_5p zI;PKLDGH6yK{hFzPfirVXgX^u$=s-=*$6p@1a(DyQyqo^6tf(*A2r}r$~%C>b=ZUl z<^U#4Fxpt6uMGB9R*^~H2-qjz{=;YGG>4jq<#f=uL$KL^{0(XDBEY8MVjgL}>bww( zjTG`lgmHgjDWB!cUuHsaZijPQs!W8O5i(*30DEJH98NloXkEE0hbOO^G&~KxJ@g6S zBny<=Z6ZKvaSN4Qrufia%#UJ3N;Kf90TUV4UfKxG^h3&k(nP2Z-v)cT#YBZ=p};j^ zb|WI8Vn%+Fx_koEYWT=g1X}wWPzq6!_FcvcvC<`xyJ_r4Ez*2eciXPL?ZSj}JW{f7 zu^J)aN(EksxGt5fM};$-fNcZ)X<@sQ0pUJXUWgDBN2Pls(16}TBltC6WCpNx+b@IW z%Sh6<33)zCucNeveXR|yjYOhs-4=VSlEv~AgAcp`BUr4&NncXW;Tc1nW)k++u|b^G zAjI`ZGDef5EGzg@QNs4JD7A*A*Lr`#tU;cQcyo*6&%;I}>4j{=ZQQR)~oVw}w$nCJ&J0hn@lm+X@Z94K~tx znSGWMf9fCo8MuTGnL%Gv(8%V%tS2Gu-$GJ2Z$bWYC5!u$6b#75B*u-OOMFwiw@Vtm z)yUMRvNykr!DzpVD;Z8mlETDJY(fh2llGyAOsel~-xVjSmWd=q)F`vogT(#7jD#;B zP@dG~N@3o_&NyLKoC3G7?I5s?QyOeFp7eqO4PRw$o3O-?lPKf%Fckdf9&$~*+fSf>qapsNDESTte#B9i4q*94DVf;sl^#|qFP#4G|lTC%~ zhVw}w^!cvX+pj;FoS%BU5YaEF$Yg>?#!WJ$0^@Ut9uL)R0re z? zWPC4EYyDfOO!8n`Gt9{?DsO!sAncdN#>n(7R4DiiVtf7g7#7K?&%J6uWuM~QN6=Tc zk!_0->yh*^Y%{cwG)#A#<%npA8RSv%wYt4C*OwPhuE09yK$6rB`JTfTGQ#?l5$u*P zB27vkvzwtF9YdjXIezX~+J+bZ*vtBfXkF2Giu>wvcC3a8KroMs3Eq3)XMo*|#&5*t zIi%c<1UTF2dG2ZfvN&DsDV%fD1DC>={62OBsD1`XTc$96u3~E7`urm>pnEzC6)|P9 z7C#O^%ZOYaY`CHXEtzU0srhZJ0$g zyiAiUNZYYv(*id>er3r;KdYAj&(%cI6&=os&`%=rxfe-A997kU@F5c)F=W;fnmD5 z%2O7?+!y~mq8W0!sTdlj94+RH$99?)I_LtdGYMa^JNF|=K3APc5-&x{i}%*g^z_9G zb{Er*TBvY6*4zSSLmvxMmSMD4+0hAxEKZ3DLqJ2 zhlLJ>9W7o0P_}9V|OJL`{p@Mw0K^!`7KS`wPbC;BWF|`XOk?<+k zuw}KG4HT}&KM-oJjGuxbG`_^%BdWa4XM%lr?jDe|Kle78EYJ=UuTAxIy45br6T8h$sD za5;%SYeM{%#Kn4@tH_XNaWxe73n1oqI>=|V)-`B=!0#FrQ!D?(I#NbCw#AF4=~ zj6qi5l+qy%s-jBgJt;*})}dzH3!~ z9Q$34EJC`Nj3c|sO$(PQ09Fu*E3gXE<#-_U)kM>^T7_G4Vm)fcUG+j-wCC{FBT5D` z++I@99;|#HNE#?l!c}idt+w0Xl0gu9hvm%`zPMbF`J&fv%5rdYB7_l2)KTe|GROA+xMp8sB?R;@`LvQe6 zYAlO{75i)2`xoNeUfo_ttlSdj#vm!*wc{IM{_LG27Vl*Q$#XrhaqsFaLIz|bI3qJRcjL(=vJt#{pn zu!0gW7pF@!U^7nSiwF)cL=M`Mms7=*M$LMDbXa*%wMGy3Hsf3-3EK2In%rwP%7Iri zA^rN<7&s3Q+N5y;J!pq=)BH4s>(GU4Brltchmy}H%B*p+yyFXZf6b>%-U`vXv zK44FqjGAEO?~tS|qhx+=j81K$=bAG_^<5&_`wl@La5epuw~%qJGYt4dGdb2PCIN{} zRFxI5r<6Nj0K)lw`ZC{uon>0gN>1-4m{_>Z&?isJH(lCv=_%1&3a<9b5yV+#ufv&Hw6IGFU-syvjr~TF>G2{u0pPJNB&iSLKy& z=#9p?-EiM==^ND5bMIY^(U*T6{s;-@3~ZNhLhQ~sc+u(8o-oJ6DEqGU!XLg^zmI6i z{gfiac<7ewbz{&EHbKIiUSUXzQOL;Yxb@rrixDTEc;iuYbJOH!5;*Ax5EF7{JfqY^Ufa=ANd(@5o- zB0+d zpt1Ku-x^IzW96G*bHS@1v7ft`BR1JY(^5x;9fimy5Bdlu*1?ARvWOMaVp#b>5@S#K zK_t0%p#1ix{TJV4K@Xmvx$p*+^-Ye^`>+X;bo3B@zM||6lRiT}`ildzNN)X*q)Z zyA6uB3gg^jls)Y?YKE2P5Lxb!G8b1v><%4Xk0u@h=Yoll{slXL>F~W7?_pK2-<$Co zv3tG#kPvJ1J}j8iQvBSy!*ywOX}`4pCYd`_h`NsQt&0kd{xaj0Zy8mcTwI%O0UbPlVObs)2EFI_)REd;vdXqp%vCRs>)q&*o+?O_SIVt^)Q}J zz_|+ul(_&yD#2xeH^1g}3ei|RGlUTp&}ytD~#eVFBM@wD+@p*A_Vy*%sLjFbH;P1PH?t(Q~Vv=x)#LL$&%9 z`)#n01T0{HaO!{<*8~5IG{-|1^xUF_^UVzo!~J!Guwt2i%fMv-%fdJ|~&!Pbyw%0X>J)WPFw2smVA}je>JZbge7rmB_MBp7+dL z9CzOK*PPWf61DK0Qs%6H1dh&du*aL9K1UPhkaLz~!lbrv0R}H1B`**Q0mO40O^tR zaTmNtnbW;*jD9EYmeEl395*7f{GrZS@4`EoqMYzwz%%!-!%exHW2CGAnXf~t@kBlRB zu`9=y;XP*=u-hSMQ_w_e$KQ+N56u$ME@Gc@v$(Sr_U9K6b&eIdyWTvfdV zJNFRLj{j$XJ`(V>S`=P=+n2>)rHUKPnYpq(k7)NC0lQxVE8WL~X*5KZ*Yk!wDOQtL(wG#fI&Rb7 z=8>+>TRm@3ttbNy z7X*Ao-S~~TW306i&>p&vJN^bnKpu>1V?g)|f8_%jxpHWuP74VuJ(N46ik03R|m+HVP7$?G-0Eyll9*H^JEd9He;hvc9~zBJ2D2SMD>7WHRl zq_A_Zg$RH20jWv~H!vYX6bB#Xlv9=<$b(qL6n{;ubk1^I1p>;!)7z>ONa58@C5O(; zMD!mbToJlryckJC#ua2s_L871W_k6sr+0+3Oi0{-K`MdT9A}t_a03TR$Cz|ZN)#f` z!B5{6)+d!$e|?1&w60jgtUOjFiLJY3LC>BE80Bf2KZ_a$Yt!f9t zufJFDNO#EP)q{R02d8xNGmhavTBkXqN|^T~-uXAm>rqDCbjs$$dmhgh%xI0f^cPn` zTMuvTU$lzeU#rZi@SZ4_T8e4G-tr#=8pQ=UF=P5ll+Jt5AuGYc$=t7ex(%Od zy#bQoT>}T0v09h-`}q3|za$8;Y*2HC2Js@Y=Pbxj5{;X7DD5LjI~yUup%|*u?vJ%q z9G^od9e@$af}xq(L?UyG6JJ*{IruNPvEyT8D8gF z2YEENdv9BX!Mg9QezGN3$e5}(y}Z?R*bYzs`uMEaT9MS2D!?qEv4_8A+5nPc2(>Gi!OEb(!V*-^<|R;+KI^)oGJFle{QOC<(IZf#yc?(opuKb|zOE zT2m9z4qZAKgf+umx``aI`Z7Eb7;-kESlg!ZSd@_sPc*!R2`_F&NdYupA43f66PmH3 zmA7tbeTmy-qS|5_j}W)vaHzgq>nV82`>%itDPtnYy3-p^XBdpC0msy+A3mTdpZSX zw-YfS)QV%kG4jidp##Pw6;m%ug@>pHqA))UKg83$7G)xg$<2f-_oHO)LgvL1gcLw= z?to6xUGhdutJNGx(Imf;!&|qd3a1IDWh|y1CWpw^t-CT^m2X)VRkNvC_t z$9KDKyl~n!TJrtV>LMx6f7cQXhAJ*_#cG#lO@>yUUwO zDEm~eUTi#iD{p3NzgfRR;McOof*HAf_rSsPbIF*+;V84JqfrK-X&G`B!HFu8%T;_i@X-otY^ddb)&eobRujLdk%@k44;`6V((e;sjL3(|g{n^?SeyT_Hr7%brBp@9^+-PZ zlLL7Ea+9i9n`-p{koqmDLN(;v8ur76Got9JdjK~z2WWp;QbB>EuF@ol9ByO_JyZ!s z56m>it)h6V+VMjMHl8%x<`upCcw=e~D$m-sY&o)S%X(9>?X597o;m zQCgMoRy@quK5ZZ5-ACj^n8G9lL;aV(SH=9Xm)YXO8F0J+NEL`5L?zIBdiupLs1Oxe ze!Q6Vg9Jym%c|c(cq|`^+r9m%*ANMG)FM-20IJvoN8Ys#5+h&!&RGEEy=PJr;7R2z zS0*LT|S#Azrwn`Kv!83DLA1qE7j=1}05-Y~hxR>sy(Lfq9 zZJ5dGgDVa~_|n6_A^aF!`?LXso0>pz8$H!}1gExc9(_iPtJ|lk03K^Wth{&Ga0)RZ z*`E3vVoL!hVpdG5K@}T?x3?aGDvDvHZyf*7VC{I5V&Ja;qoo*kY)tvN435mRN)}Dt z1Wx?gH~eu?zB5D;Y_C2KkH>yec*E4;0x13$-9B|21Om&>^vBi(n25JF(?gd-VRWAB z0`^B5R_jPO0zExxj+H)Co0lQHvW>J>B;a?6L;}E6VfE=(ZdD;Fu$`=0Fa=Yc7b&kk zlG;S{L6fp-gspR6Rol4~f;SgcYmER}J1B1bLOW2{YV;w5_10shXY3*&o=7Ve^hD<@ z%$k@kSnRLV;{k4y4O<;jm-N{2jNkLSQVtk|WU6Q{Z^;U3x9VU8}%*Qo)gd ze(txFRU;n#B352K&}9j=haJKqz8_?_{=Tk8V#IwBU#>Ia){hF_Kmao`nc|Rwxz13l z62Vibl|j1W9|R=5lHsP=TS1SrVz)2)*GiI`=GCj7RvwdCbG!3ILc6#UK61S@haVII$;k@8H=n8+-8R^S7(wsy4s z-#l2u1WE9nM%uEeXbA5`ropfkV8g?CbzRN^HH0(iGQ7Q2Gu2tVSi{Qc)w)-9ai@MV zCL@NwrX?)-qIqXST)|J7;lb4L)||9rmbIF)M!emhL91Wi%ME&rzJ1eqQq;nI1B-(_Wu=vkHlv|bT zDFnw>>8tdhjM=SlQFV7zJK8K-gO_(1&btBUom8Z;rxY>uZjLizIHeONS}V;xtVoit z&9sn_#2xpxt;AF{LE7q(uD)aWP)pki)a?qaBhK(KHl}6_OhwDFM?n6O`fdYcZJ3m) z-6JFhQ+J1_!BT@LB>sSk6kO^Xa^e=PRtS=)q#RQ7jyUAh9U*R)aqfPqTmO8k7Vnr0 zn3cvTQ&;ii16{ZMNV(OAI=^)aBdcIUq%_cb{4BpLt2 zG8Hyui94QMb4P~j5-P$QT1xooD=l0gB{(5C;c*n2RccQs6KH?P|4MS>ufx-A;#u5I z*b>XXmjUGh>8Td{!afIQZ&AT!%uW@)m6%fdJ0J`PY}e$F*0QI}z<1d3i1NG_>{2%M7Kpg=5KfJkYgyu5?CKSdT*Gw^SwZ8-f$m6zv! zYyj?9R`K$z?;7BV@M!fF0{f;ZYoIi{eM(c{TuFC&jA}p6g&P)=v_B-CYS*65Vnn+( z>5m@Pwoc#zIe#d;yr!j16j=&qq3Dm)tk=}hzzK=ZKE*@<<>wu{{t1gh~Q-=h$f`z;Us$tlwSsAeO4cSDh z2ZbchK^aPz-MQs>BAH!B4Om-;F}1>l=wp!dy8+|11@O6=d~`Lt{z@b(mv~KC8iY)vmNcRr8vtYHBniQ#ICah z>-vz5rLht~dvnjYkXCpsqAgY$yOLvoE@CPBG(%fK<*COUa(xD5Ds-I+OK6DhG)c;q_Q5b?cgW0!-j$hsfyP|^|uvXe+hR!7i;!<)yP@9+eg1(b+(_xO3d?uO(V*f! zjMgx=O{|HdyT5CBk-ld_+%qF**vvCWVZz{5YR)^!7s*8v>*5&3@1*18Zx64k5iM>T z|Ec(ef99vf9lRc#`0~$p{Np(XX1FHLAx9a;=@OXClz}Dj3s?ePhe!;h>n3G8rU~6L zh8HUpgDu{Gqlk0s8(<>82anU7O@JBqhhyEp*g**Z?$A>Uu9(KI_I=~@FzN==s%cOyb)*fm9t*L0hd2KA`AZS?SEa*aLV$sl>C;L zZ`(upk{b(^D-<48oK>#yHa>ld{2;dLfzU_itZq=}{wS;a!3=KVKlk0lcgM^2$xq*Q z_lfmgMKZ4xDsL3qoubgO81X%7@0=?v%_zoN@3 z4Z@F_9YHa3zYc)+wRjkVHx|{Ag@?)W#%cs5`1N}G8 zdq~)9=;dzoxKe>9J%Dy+0^>Kl9h*A!t}hF{7l!E;o5sI3;cc@z@TYDPMP4u7P$742 z?=a4G1|P0^SX!EUS|Wu_{?p&bLZ(|8ScQjWeI$jm(Ig>Av1fBuH)-nVw~Osf(Lx;f zBmSENcKT*~7(+iHD8?kZ^;g$2EZceG!?R3Txkrjk!ErAIy<@ZZ>^p@I$qG5Ax6x$f z7S-}!)GG8*h(D?4(Wz6Ef^N{uS3ebHwkmg z2*+d~weQX^Ke@ibiph=K8*j}y=o#LYcdGUVFfdqkP?|Ro`dG@zD9ia8P0(64`Dq%D zzVWmrtL2#_etr8lQ9OE2_f~7un>#u_D1d!IdwBIcFTd#a0;mS+CF4NZVc^?RP+)C z6Ths-qEej=EIV!n1|WFB<@kyF538b1wj;PP@qK06aP(e_oxrzhl-6`*gRL-V@SZ;6 zV-?t|(>#A3@bCX?{d1>ehSOd)@VN4;S?}Nz0U5;Igp*%oSvdmWeH9MYyTyqNGeE;u z_+;eEm;*&@@H2&Yuwb8rI~a<2#*DA+`?$BFUdKxh@crS>Xp23Y!BEkL(@Q<-+4~44M!Qg_(CFtM0t-q%Q$Wp~8?HK$w_~mc1TT|@Iu!lU zIQsp{xW=1BwJWTd@(14;cpNyObG9@T42^$W^Dfwex+n6bMkoc$2Nopm_;w$z=QQj0 zeczOqwiPvW1>j$Xcnfxp(uDg-KqYcZo%gLzYYyypdFAQ}L6d-$;_#;R-J#1HPj2uW zkok81su3i@JgeA0CVShbn|p_KDP1252oWUEV8s^QdhdUZ>`OVn#_472u!I5ycq^q- zSNzZJ^+ns|4%AB?d^qWyAirYI%d+1pKLEe!&G9oed$NDusQy%|vq|S{NBgGv(+7tu zOuy(Ev^g)RLW{1SZD&?-cqNO?sDnm#(kx&0d4x*Q^73_dYag zyIFJe-$&5D*C5OGK0FuD;|g&1V#Ak;Dd~+BZ8qx(XMvM+AACjGWyK-c63;gxNh zWLKMki7(#8H)?}7d6q>nO6+Oi&LZ`V=N{J?WWA3U*$VK_v4 zrk~8#-iB``-+Xz0;WOv8#{BI?Vt)M*_9P-Vxaefy6P+`<-Tf8_82mfKsBMw1gqiCb zPlqdA7%217{$O;<=j85vFiL*>mAD}#ApgVp`!|f70l(<)v{KH?Kaf4I@2~4yQ@2P< zNSX1)RsTjuu%4zD?USv*s^CECpA6b}p;?6?oh?9>TQ<__88> zTl!xnFbysn?lz@*QROmVyu4OD$=29MgtGr*n1$Z5oEZ7Hibnn`4RxB_=*0jN4;LqV z?S0>!w;_8CoHE5V3|MBpbx#!vyp;(OOCGU<;{Hef3Cq{oXlkr^nBnOUU1d^$jk**ykUb zmh~n`a%sl4bm;k={jK@X%)!4@chZ3O{^4~Bx7QiZPXmk0tNzzTPt@S?ag?Jukxv!x;R=0-Du^RL|rSXHNZ3PoOb>G^$ zrR(jy+#|gD{(t^8di-&2EdRd^SN`lRHQSZ;aCT7o-{~v=Ud~T8bc=r;v{t&&@nX=* zLlsXhP2J~}=DCWRMr`@zIv4xwf`>&;*0%Kb@BCf