From dde916f71cda54a50bf35b073d6c970601218d0f Mon Sep 17 00:00:00 2001 From: djvelleman <110697570+djvelleman@users.noreply.github.com> Date: Tue, 13 Aug 2024 13:25:57 -0400 Subject: [PATCH] Update to v4.11.0-rc1 --- Chap7.qmd | 17 ++++--- Chap8.qmd | 4 +- docs/Chap7.html | 69 +++++++++++++++-------------- docs/Chap8.html | 4 +- docs/How-To-Prove-It-With-Lean.pdf | Bin 2292987 -> 2293479 bytes docs/search.json | 6 +-- lean.xml | 3 +- 7 files changed, 55 insertions(+), 48 deletions(-) diff --git a/Chap7.qmd b/Chap7.qmd index 4cd6fd6..4f393c4 100644 --- a/Chap7.qmd +++ b/Chap7.qmd @@ -32,13 +32,13 @@ theorem dvd_a_of_dvd_b_mod {a b d : Nat} These theorems tell us that the gcd of `a` and `b` is the same as the gcd of `b` and `a % b`, which suggests that the following recursive definition should compute the gcd of `a` and `b`: ```lean -def gcd (a b : Nat) : Nat := +def **gcd:: (a b : Nat) : Nat := match b with | 0 => a - | n + 1 => **gcd (n + 1) (a % (n + 1)):: + | n + 1 => gcd (n + 1) (a % (n + 1)) ``` -Unfortunately, Lean puts a red squiggle under `gcd (n + 1) (a % (n + 1))`, and it displays in the Infoview a long error message that begins `fail to show termination`. What is Lean complaining about? +Unfortunately, Lean puts a red squiggle under `gcd`, and it displays in the Infoview a long error message that begins `fail to show termination`. What is Lean complaining about? The problem is that recursive definitions are dangerous. To understand the danger, consider the following recursive definition: @@ -77,9 +77,10 @@ lemma mod_succ_lt (a n : Nat) : a % (n + 1) < n + 1 := by done ``` -Lean's error message suggests several ways to fix the problem with our recursive definition. We'll use the first suggestion: ``Use `have` expressions to prove the remaining goals``. Here, finally, is the definition of `gcd` that Lean is willing to accept: +Lean's error message suggests several ways to fix the problem with our recursive definition. We'll use the first suggestion: ``Use `have`-expressions to prove the remaining goals``. Here, finally, is the definition of `gcd` that Lean is willing to accept. (You can ignore the initial line `@[semireducible]`. For technical reasons that we won't go into, this line is needed to make this complicated recursive definition work in proofs the same way that our previous, simpler recursive definitions did.) ```lean +@[semireducible] def gcd (a b : Nat) : Nat := match b with | 0 => a @@ -180,6 +181,7 @@ The functions `gcd_c1` and `gcd_c2` will be *mutually recursive*; in other words ```lean mutual + @[semireducible] def gcd_c1 (a b : Nat) : Int := match b with | 0 => 1 @@ -189,6 +191,7 @@ mutual --Corresponds to s = t' termination_by b + @[semireducible] def gcd_c2 (a b : Nat) : Int := match b with | 0 => 0 @@ -528,10 +531,10 @@ Before we can prove the existence of prime factorizations, we will need one more ::: {.ind} ``` @List.length_eq_zero : ∀ {α : Type u_1} {l : List α}, - List.length l = 0 ↔ l = [] + l.length = 0 ↔ l = [] @List.length_cons : ∀ {α : Type u_1} (a : α) (as : List α), - List.length (a :: as) = Nat.succ (List.length as) + (a :: as).length = as.length + 1 @List.exists_cons_of_ne_nil : ∀ {α : Type u_1} {l : List α}, l ≠ [] → ∃ (b : α) (L : List α), l = b :: L @@ -563,7 +566,7 @@ lemma list_elt_dvd_prod_by_length (a : Nat) : ∀ (n : Nat), done · -- Induction Step fix n : Nat - assume ih : ∀ (l : List Nat), List.length l = n → a ∈ l → a ∣ prod l + assume ih : ∀ (l : List Nat), l.length = n → a ∈ l → a ∣ prod l fix l : List Nat assume h1 : l.length = n + 1 --Goal : a ∈ l → a ∣ prod l obtain (b : Nat) (h2 : ∃ (L : List Nat), diff --git a/Chap8.qmd b/Chap8.qmd index d0dcddf..8df7099 100644 --- a/Chap8.qmd +++ b/Chap8.qmd @@ -2021,7 +2021,7 @@ lemma sbl_base {U : Type} (A : Set U) : seq_by_length A 0 = {[]} := by apply Iff.intro · -- (→) assume h1 : l ∈ seq_by_length A 0 - define at h1 --h1 : l ∈ seq A ∧ List.length l = 0 + define at h1 --h1 : l ∈ seq A ∧ l.length = 0 rewrite [List.length_eq_zero] at h1 define show l = [] from h1.right @@ -2029,7 +2029,7 @@ lemma sbl_base {U : Type} (A : Set U) : seq_by_length A 0 = {[]} := by · -- (←) assume h1 : l ∈ {[]} define at h1 --h1 : l = [] - define --Goal : l ∈ seq A ∧ List.length l = 0 + define --Goal : l ∈ seq A ∧ l.length = 0 apply And.intro _ (List.length_eq_zero.rtl h1) define --Goal : ∀ x ∈ l, x ∈ A fix x : U diff --git a/docs/Chap7.html b/docs/Chap7.html index f68f104..a3538fb 100644 --- a/docs/Chap7.html +++ b/docs/Chap7.html @@ -282,11 +282,11 @@
These theorems tell us that the gcd of a
and b
is the same as the gcd of b
and a % b
, which suggests that the following recursive definition should compute the gcd of a
and b
:
def gcd (a b : Nat) : Nat :=
+def **gcd:: (a b : Nat) : Nat :=
match b with
- | 0 => a**gcd (n + 1) (a % (n + 1)):: | n + 1 =>
-Unfortunately, Lean puts a red squiggle under gcd (n + 1) (a % (n + 1))
, and it displays in the Infoview a long error message that begins fail to show termination
. What is Lean complaining about?
+ | n + 1 => gcd (n + 1) (a % (n + 1))
Unfortunately, Lean puts a red squiggle under gcd
, and it displays in the Infoview a long error message that begins fail to show termination
. What is Lean complaining about?
The problem is that recursive definitions are dangerous. To understand the danger, consider the following recursive definition:
def loop (n : Nat) : Nat := loop (n + 1)
Suppose we try to use this definition to compute loop 3
. The definition would lead us to perform the following calculation:
Lean’s error message suggests several ways to fix the problem with our recursive definition. We’ll use the first suggestion: Use `have` expressions to prove the remaining goals
. Here, finally, is the definition of gcd
that Lean is willing to accept:
def gcd (a b : Nat) : Nat :=
-match b with
-
- | 0 => a
- | n + 1 =>have : a % (n + 1) < n + 1 := mod_succ_lt a n
-
- gcd (n + 1) (a % (n + 1))termination_by b
Lean’s error message suggests several ways to fix the problem with our recursive definition. We’ll use the first suggestion: Use `have`-expressions to prove the remaining goals
. Here, finally, is the definition of gcd
that Lean is willing to accept. (You can ignore the initial line @[semireducible]
. For technical reasons that we won’t go into, this line is needed to make this complicated recursive definition work in proofs the same way that our previous, simpler recursive definitions did.)
@[semireducible]
+def gcd (a b : Nat) : Nat :=
+match b with
+
+ | 0 => a
+ | n + 1 =>have : a % (n + 1) < n + 1 := mod_succ_lt a n
+
+ gcd (n + 1) (a % (n + 1))termination_by b
Notice that in the have
expression, we have not bothered to specify an identifier for the assertion being proven, since we never need to refer to it. Let’s try out our gcd
function:
++#eval:: gcd 672 161 --Answer: 7. Note 672 = 7 * 96 and 161 = 7 * 23.
To establish the main properties of gcd a b
we’ll need several lemmas. We prove some of them and leave others as exercises.
We will use these equations as the basis for recursive definitions of Lean functions gcd_c1
and gcd_c2
such that the required coefficients can be obtained from the formulas s = gcd_c1 a b
and t = gcd_c2 a b
. Notice that s
and t
could be negative, so they must have type Int
, not Nat
. As a result, in definitions and theorems involving gcd_c1
and gcd_c2
we will sometimes have to deal with coercion of natural numbers to integers.
The functions gcd_c1
and gcd_c2
will be mutually recursive; in other words, each will be defined not only in terms of itself but also in terms of the other. Fortunately, Lean allows for such mutual recursion. Here are the definitions we will use.
mutual
-def gcd_c1 (a b : Nat) : Int :=
- match b with
-
- | 0 => 1
- | n + 1 =>have : a % (n + 1) < n + 1 := mod_succ_lt a n
-
- gcd_c2 (n + 1) (a % (n + 1))--Corresponds to s = t'
- termination_by b
-
-def gcd_c2 (a b : Nat) : Int :=
- match b with
-
- | 0 => 0
- | n + 1 =>have : a % (n + 1) < n + 1 := mod_succ_lt a n
-
- gcd_c1 (n + 1) (a % (n + 1)) -
- (gcd_c2 (n + 1) (a % (n + 1))) * ↑(a / (n + 1))--Corresponds to t = s' - t'q
- termination_by b
- end
Notice that in the definition of gcd_c2
, the quotient a / (n + 1)
is computed using natural-number division, but it is then coerced to be an integer so that it can be multiplied by the integer gcd_c2 (n + 1) (a % (n + 1))
.
Our main theorem about these functions is that they give the coefficients needed to write gcd a b
as a linear combination of a
and b
. As usual, stating a few lemmas first helps with the proof. We leave the proofs of two of them as exercises for you (hint: imitate the proof of gcd_nonzero
above).
lemma gcd_c1_base (a : Nat) : gcd_c1 a 0 = 1 := by rfl
@@ -652,10 +655,10 @@ 7.2. Prime Factorizati
Before we can prove the existence of prime factorizations, we will need one more fact: every member of a list of natural numbers divides the product of the list. The proof will be by induction on the length of the list, so we will need to know how to work with lengths of lists in Lean. If l
is a list, then the length of l
is List.length l
, which can also be written more briefly as l.length
. We’ll need a few more theorems about lists:
@List.length_eq_zero : ∀ {α : Type u_1} {l : List α},
- List.length l = 0 ↔ l = []
+ l.length = 0 ↔ l = []
@List.length_cons : ∀ {α : Type u_1} (a : α) (as : List α),
- List.length (a :: as) = Nat.succ (List.length as)
+ (a :: as).length = as.length + 1
@List.exists_cons_of_ne_nil : ∀ {α : Type u_1} {l : List α},
l ≠ [] → ∃ (b : α) (L : List α), l = b :: L
@@ -679,7 +682,7 @@ 7.2. Prime Factorizati
done
-- Induction Step
· fix n : Nat
- assume ih : ∀ (l : List Nat), List.length l = n → a ∈ l → a ∣ prod l
+ assume ih : ∀ (l : List Nat), l.length = n → a ∈ l → a ∣ prod l
fix l : List Nat
assume h1 : l.length = n + 1 --Goal : a ∈ l → a ∣ prod l
obtain (b : Nat) (h2 : ∃ (L : List Nat),
diff --git a/docs/Chap8.html b/docs/Chap8.html
index 09a0301..c953240 100644
--- a/docs/Chap8.html
+++ b/docs/Chap8.html
@@ -1922,7 +1922,7 @@ 8.2. Counta
apply Iff.intro
-- (→)
· assume h1 : l ∈ seq_by_length A 0
- define at h1 --h1 : l ∈ seq A ∧ List.length l = 0
+ define at h1 --h1 : l ∈ seq A ∧ l.length = 0
rewrite [List.length_eq_zero] at h1
define
show l = [] from h1.right
@@ -1930,7 +1930,7 @@ 8.2. Counta
-- (←)
· assume h1 : l ∈ {[]}
define at h1 --h1 : l = []
- define --Goal : l ∈ seq A ∧ List.length l = 0
+ define --Goal : l ∈ seq A ∧ l.length = 0
apply And.intro _ (List.length_eq_zero.rtl h1)
define --Goal : ∀ x ∈ l, x ∈ A
fix x : U
diff --git a/docs/How-To-Prove-It-With-Lean.pdf b/docs/How-To-Prove-It-With-Lean.pdf
index f909684031227039ef16373d95401e34d968901c..ebc1d60a3056a753f8308ed50c1988e163d7491a 100644
GIT binary patch
delta 228828
zcmY(~Q;;T5a0bws*&W-qZQHhO@7VlzY}>YN+qP}n*(8-p@^D`J?N;^I-S^`y0{G-B
z0=O0x3c$?H#|P!)>}YCe1LeMcr9Ea#!Vc4QLVXUd6<3PO@Qy%$Nzn4U8 }Ky3ku+V!$2KGgBPJd
zjVngdz{%%}D0+NEg82swaogu{pJj2;&{|+f*9E%DXmXAQ)d#Bat);n7JcI4hnCnqa
z0|EmajtA1E1NXzxAe0Q@Ew05Rva}@1z|NA%1Bp9f`l0XNqOypl=Js@*rUf#PD^X_Q
ztlY+NLtPxN5k7(uF3htD$X0}9xQ3f>34)_kLi;Ewbpn42LGAh9j?cD3!rurl_?{Yx
zk8pEp$JF_L5%djCUN9DeG7lx9N45oF0WuP%5}YcUtF`+_tYTEQpOS^O=@(m4BYe6R
zPuvH03?djxvJZR2e0G7UCL*7gni;0UsFbTi$6E7$h8_@;L?nfX>niUsa*
zaKoH9QGHEq6y-EzXtaw9k|2x05u9^E7!heXZaczaUTY-9{k@?k(uCI$z+6qo@cLf7
z_@bTsLW7&9g`q21hoCY{MP=|W2N)BYa1@kts55tpnL^m6skvTSjLd@1X${ny29~YB
zLL_ARVInRkAP_qq2CLgrowP7$3W1Uj&<}>{di`YUzQ%<1z_y;J{AwDz5SuD8;Xov=
z-UM@${%s<6NSH3}{+Iml5XktY1I;U@y+S`fvaaabb5bGD0k{g~5*jCj0x&KeT{AT&
z$S==nQETVu$n3gDc}K${Fnk!6tR
z-+5?C>c$v!HL5gTxva3Z=i@=Sw>Q$QN`D;P(IToC%(i^6pVq;
z)-12vz-7MSx?G@FQ|S%$UkI+pq)P>2%&jDELHU+AQf;!j@kBhRAMWd1tgn2!s$BBw
zOIT;$!B8n=|T2j4RkDKMeuKU1N2*wEd`JXha~|Oa*R6
z2_kn~gKjf^G`pYA#ojfJ5opg;+H~`dIV9+yH4R2e$g9#J5Ao>pgfTe5zmhYCcCX+<
z-Dq1rArQu%HRYfV6@MM3vWqnZZwV0eE?&Qp3djg%0RBc0ig!v=swl})ZA@y6VCGPz
z1*cR`9-XqZfmMrDm*Jsoj4Jnr$g2|-wX&>f${P(y6iShG1{$ddmm06kv$=3T{E+gn
zn0CBAt=;I~kM$g0g}QcE8B!_q2E?U1D0Xjn${MX>P%vA5Y^YdEyD81zmx^xhB~wuz
zC@0B^0V?TVGS4TZXQRSX*O`h`oa41%Xf55xk4c*`eBn7>5BG}L7e;u_B)(DT5Hlk-
zOV-V7pbsn$QL0Nlt`Wx5ltUGY(&(Stg&u8I8amVb8vFx{er_fs1A>3_`~+VOva&r>riq!?~v
zBL|oxhL|G){{!;RuYZ331NslxKj8mB`~&$9)IZSw!2ARI58OZS{~-MHpEZ#FLH-Bj
zAJl)){z3l-;~&g_uv*L!u}l6vXinA?8!#ly6u>JI1RxA}hixrmZ{TsUk=_A;JLK~#
zHnCJ)^~u<68JaxR#?37$Jf9-`lTYgE=tPtj>3b20*rzQ
zD5Hm}fr2t##_G*oGclsSwAF&T@^ND1>4TiID`{TT-O?Mtr)j-c?%~Icw7pmE88kx)
zcz%_d0gxNRG|tbCQ&L`W_MARw-E{Y{Ti~1cj+obhjz7J>g~aU80^VBZK2Ebn*8b!s
z)=txwPy{vM+1xz{O_hBS1xe1){%GDhev=2$>`auvA5BwE(Abfj4e0Xf`6$rs(C+*I
z*wC8@DO^|x&IM+7Sm(rdqcU2Z06z71xEXu-=gt>M)`>17db$_58klJA1^CXkl)t{l0=2611wZ#AQXqwfYQg3P}80}JrR2yqzL0dhA3BpyOTc&zozUw
z{1^I%Ib8kHwI#@Jvt?;^>fiFX8GKkjW`j#0qC&6AFF0QOkyeY`wLDM4t=pEl1D!5P
zU`8o44$7;WE;n|q4Va4#OczX*4`|#&PZ-NxLQttt
zg!$|kH9~{4mO5~*4?{jNL1AuOaIWLlrLQR62C6tmpJ>=8u|3G;wn5*3WO#7_|3$Z7
zbp8yNPmWT0zt1qxfytOsf;}U_bPf=)5z(mJFlKhmMFf2R1gR5upD(#A9QQ+5Q|HuR
z#8%$9>`|}QK$^^Wq>Yd?HZm-B0zMD5Em>hWAvIJtgWp@I$9Cc%?nc`bK((Am6jc2%
zuW{i=(KW)ztkuV0-m@lw2v&w3W0&1h37=hgJx)Ai`%4Ps2pHel2$hHh;9?I=W<3He
zXfN4lNY(?$8YsqyP^8}t#0s3;LxC-=(
zV@mR>Rt`>?z>dagAJYgu7Wyu;rhb8}6Lq4}73S%?5vUfFRhr1@doo1RQAQlvo^oFl
zuER?okh*?xS&IvCH5ex%w|m3!VYA16qy?&-d){&aXco42<8uz!7b=l|XD&aKGY@Xp
zT|Az~LUy|a_0?K-zjdX20BB=xI~dRE`J8+Zm`PF}EFt1|1XFKGW`%c|yIZ49c;NHn
zU;@0|eVhGcW{CwD7UhT*RG~nWK>Cvc3qZa~a5A8)_#)rmF@RSTPCbm8ZNXU3AOoWs
zXfCkH0vkO)K~CY;Myb{u*~fY@p3S>@;?M;fRvoS;7{RcEtD^fVRf#JNUV1fR9kXi}87oE<4yWEUZ4
zbyr$>pQ(PpGCV0U0zkIma^Rf%MORQSn9VW50IKMAr%KhJ3c)&;
zS`cDA=noF;fc9A&;CG-JKUr%?QWo$aqDc{JnckakP#Su-xXS?u7a||i>yVyoQm-fD
z?V}@lYM;OCxVj0OXz>~oT)rbt95-y0FhJC1BFI5WOus$8WvaX%fw}$ptCxAYI^eYK
zPj}6`B?Xd{VAk!EiI685(=gp@7R#jASPf5JnxzGDAh0hJfC+Y^A%ZFFc$4_kC)qE$
z#`rAStPCMc=`QD(m^6@{2m1skjgrhVdPOA!I=rWfUZt*o9AvPj8g{9wcG)1}x0|gZ
zM$gIp+BJ_g^X*5EQ~80ExbiX=43WNKiGFeZntiVv8xzJMcy^r{zuWEKW;VKE92&218FZX>EKO
z&eUt%Qry@#y8V{xVE_8wZqi+&%C}*<`dQw3JH%IL#Vmw!6$p2O;n^?iyk@$+23Z!?
zl2r4-8fmI};>B2p0aU6(-drb3Nk7!$J306(Db#EmpfG=@PLzJbMXb)Yh)14Yxkj7+
z1`&v7vag0wB<|f+$Sd(d_q&4RVx#M-_r~q_%!uvx+3uPIxqx-_JE^rHnJb!-=We2&
zD^lecVGpRiwT>h@#y+s@0IGhqK|1x$vR?2F5=_aX_fz)$MfNB4(K0WK4KL84*1)FB
zpHMh507Dt?q-i5VYs;cw_3mV#IUX(ywsSS9`2iCgQLYQ7ELR%wK^20iz32F;3m+!Y
zBg|O#PQ_+4v*2Hn=EE6`dyb+VF3|?%zFrTYN4rY2`Hg_I!7lIgvGJlBIn8IY<0R5
za83AD6Ytzd0;T~T@KpW|kX6m2h@J~Ykz!Ckw|&)KE{hW{l2V!M3oUp)T7Nh}p&VH<
z#%eGJO~{||jS8$1<>`r=@nrm67#EbtXSQPk$&TS``XLw>j;OsVQ!%9jD-Yo??_3p8
zz$$$?{?ZjKTPfXO{xUmN#-;l~w5D11s(7N5_p~_npG7H0ot>zIY3Py*FpZqvmsLk3
zT=i>^V;=n4-N<(JQw=L%_I!jtwQ#Vt_Jy6y2g}pEPf5XQ-g{Kawv5QSSD(L7q`5zU
z=4iQ+Y;>nL+SFeblLB(V$v&H3MX$>|0CHPcbZ)EohL>E<=CF=nR>`LYNFNHVt=T-BKFI5E1ErFCjt`mO#2z0bVO@3JYjen%OH)~LVHE%ZfG}w+V452-*
zZON*xYs?jF!1i_1FBsZuau1zgeNyFpV8w2h4IUM63(2Wm&v5cByllH>G43#{04J>#
zN9H4236Pd(((1i|Lp2YNbBsZrFUt$;#F~lnSq?(`91<&D`X^;mp7tB8yoj
z%aI;7DD%^*G%Wg^wtRF}BS>wR0FTK~RJT!vHZO-(PA`dFG^rhiFZW=g0C@FYaPclE
zQ(}^0uUqG1TD~&(_K6XOM7(a+D%KZ(Q{|)rhi68v=1ty!bR0uQ
zGGua@^IUAYiS!qA^D7}^|2T60dM%kwZcis;j4;Dl(oTaJkyG6jVlY#+$eB$a$ZRH(w$!>jXZx~qlB##;^h8~P=Q~qNtq*}V7OD~P+Nu2
z#wbMT=2+4B8wfSU3CN8{S2`^Nca)?ulSy-yxpLAg-nyqt)m_PP7ofAouXBR8@`cYn
z)359{tqG^?d6FfZ=JIh(_2A;L33Uu^t&{RahrN>}0DN;<g_CXcWOmd?P#R`
zff$eH^O<9tz^<1|N}Fg!PPDfyoMay7dp;`QFb$BH#vMHKyyYLWc35wBxY;0;B5s$L
z$w)Udi5?FtQzNF|1bkOhhI!Vws^*aAP?3pG<9raK%>DVKNv{BE3@mG;%p1~G5mbLk
zGTub_S1Z!BoKPJ6f=i~s8=pe3AI&Xq+6+3Qnnxw$50mZRjPdUYkI>G$?M7<^mt?Ie
zQT3J*5)=F}m-5^s>bMgfql!HJl9DZ87%>iK3E~^4(JWFjz;2%d7<@7k9-DVmOz^)qY+TxQd*Nc+GQhE9dzVn{G(h~l*%sAMs%*JvTpWF8Q71NdAb5u0{
zWT|gOEZfAZKR9;vwJ!;S?S1RQ+!vXgwjuzrt6OamxIHLw=SzBs$qtut;qt;89Y*e=
zh#+agNvy>a03*^&>>9*3+Nrvy)DofrKqs7-Z)t~sZeE%xZME(oc5yAa{0K^1u?7^n
znTun4w=}rjf*8PJY;xFNV8QRyr#q)keR%hhtFXwc6O`q>aHw`tE*=PX<0K61S<{S=
zYMq<&wH~NSkNV=qK}-LZr2D{>4m>$4Row2MqMe8X5SMVn1S%)OL&j~>%bF#as<@HZ
zYg=W=tH9$?i4GF$Z||>NwmQtcWX-JCbMSpvE_X9FvTxnV@~ID#A_m8%MI<)r#Jem#
z1p%Ihf@0!5UrA8S=Q>~86&>O_`PWpTCKFM$@TVJR`_0iap1nh;he08mSt`ughLp|d
zra)q;bLSV>oE+VJWT>pYviIV|G$~aIMGb>$PV6|JSH*wiA)h1$Z@!^*JLtgvD=(%T
zRbW%3d{rUg0H_sja_1mGNPb<~#JABt&)T+}#KYES2!H!ZNG=wXe^y`j8O$BjRVgWw
zh$yCH~z5m?TkKHjc-0N&{>pTU2i
zkfZ!4nUOaiCsZ~hj(*aM0dlILJcEBW?fzvqh@*rWAk396C>P?pg^-4A?1psRS=gNfH}TK%zsJb-6N#?P*U?zmtg0f9a1dC
z6&bEb7Vl+I_`INh`+D=q6*jDz$wv}CH&A?}V?hyv!d5MV9gl$dhwNr91k_LnLo%V$
z&HhZl{Xkr4SOZc#p{+AUIGgd1#WQ2HyenL^0%4pc&i2mbkaJ+o%Yfk|FzC%dX~PE>
zAfpZz%?xHXK!v9kHBdgbudzK>+qY-MxG;SHr6Mr!eK!MW50Fz4n)CNag}X1@2xT51p%*3dh~Sz{
zk|xnQ2?i~I=UK2@GSho
zfav-NK8*{@
z3tc%yE39o%31j-a##jU?wkM83v(HrJ4Q4OQqntRUOacNwGT8JlVh>Ya{AsCCvdw1P
zgJC=K3PVposTJTodg7ghA+oJpw`uWu{V?h|O+|%so2Sm2i9WtEufyp#SZ~I9bF>cRi9@pJ4N7_P`TL#vvS%KMXn9NbwNzRHrZDBKoP=u
zq6f-Rfff+)I=|&olcOB~md7|@VqN;6)Ff1Yth%5kdVd{2R-wG`?emy%vPvzZe~*H`
zxL-LO6lJBlmyJmCS*V4h1
z@Jd^4b5iEA_g8(@YM8M;DbjSOp?Ou>%W6!8;z^xtaufK8TuK3k1~M6q9)(jWm$(gY
zxuey)hz4quZl_^F{-xpKo-~uWcGIQ9GizeO-H9M|n5q%rqyRo?hb8#*)P4R*LeH^v
z!Ry1_mA1!QgJVEHU@DM;HY>tk8@U48rYi~ULm)TyMOqbI=0tabh2I9;^GKx=2seY)|>c;DF?Ktd-7D}LGEkMImrZ}UYcdJBkPfG`?`b?a$5LRc5N>2jK?G<4^A=>x}
zuP7JhBT5>x_%l8e+B`Y$EFj#(cJ;p#Cw%w}A4veZj;n+8^N##(jr2~c|E7GkTF5Vz
z)MT&iJ6=!*fzVXf1bis=E_|$iF%W1_NjXk41=rAqGLL8V&fh0F5lCIfRpUrm?{Gg8
z+p{eTt@2=jpNOqxY6?$JJ93;-r!+$oGK)fabd^1JeA2fxA}}9>WlE;|6amp1kS*qI
zt^@%NgPxNJJ+6IBC9;*kCMi#D`^Hoz$Q!SE%L~y`$-B#j+-QnRd0x1gWq*miw5PA;
z%R4p~2bZ_1X@PO;pvj+VzdS_wuO}|i1^o)vLFL@`frP)k7Rk$d8X`={3_LKV22j6{
zrj&OmzClRs)Z6WW-zio6`uw(%k{_Q=fF=aA2wndY*B=Y()64^bk*t&LZS}P_%bX-8
zKeYhE=ulv_%3PtFF)}dzy|DzOL@NO6mF3_t!%P6`zQ7eyg-@NgjTjrSH#PJ2misUH+pH^u66g}BFgO6<&O=B
z&+vR?s?4wE)?z(V5jKakqIXc;y*2%6#8Ru%SvRv9^}j-yPRhl)(H4yY$t`&ywncs-
z+PnEG#Y0#jvtH798XExKnO1b}_Ax`g)b*NK^?DJ?QwzCYf>~MgG4I_EM;}>Z`2{wL
zrgn{KURaR$@ygt4mr!`%=dxE$V(AA!cY#mc1@U)m4oP`l^Gy?8cFcnGm)xZFlFb7|
zaogJ#f2fo@ME0S}rudTEv!hu7n{uz9K3nZgR@ohUo9>BhdLQ7X&27Eiu0x0KJRX;o
zm8v`YMX6V?qBr8$f~{c@fQ9G(bW7c6_}rAEv+Eib>qC@sjY*f7;58flu;p
zU!;1=f6O`E^H#yak7IK=e;JY=!B&&OnLn`i1BZ?BPf6V0peyapm3DFC#10d3QEFJbl?
zen!CqXGj0K4*7{x@3$Pf-Jw>u)CLg(rt8%L0jIP*83Zy&CaNiH2gVJqIzd}rzQ$4O
zBPha^7~gBcB=!x)IUyhI4b=36G_ccUL|a#%_B`$dX6C6@pSq3d^Q91U-MS_N
zlkQ=L;^wACJiU3w%M0gtJdu+jMfnDgL;4S3LGbiwA@3(S{o-L=e{rM#a0p+X=3@|P
z;^~Y1Yo&R=K+|;|of8e9b)0&ivxA0etr1%^F@NjM>XSG-<-+So=hK=60e>5PtiyKf
z;DMrD==(JS!d1LY>GPRA_$_uu?CzJnmJUCT$DV~ajmP*MWyR_x6T@SqcKRnwBRCjY
z9+asB?yE)<;JZ)PFNfjTYvk0AVU2mT6HrSW^9UEnXgr60wjB#_Xiz;;*|VQ)qJ}bd
zOgi-g>Ll+%`YX)xTK^iayPK({PW{+lEK35f+ntF(3w6{l!&aeNKD9?S(A1Jyb6nbf
z^bkggY)`Jzd*%aG5jlF|6xW1pJ4sSW)t
z%NPyl5u3Rh!ri?k~YW`6g{0Lo*^g0Wgi6}D?$c@Tl+P0<7`eB36DH#5iQ_i
zW}8yercMbh7qpUA?fX8QkcD&6Ri>IuAleXcnS0uW%|(>*BRc0cY>Za-Vb42?M|ar14B<-;K^`R
zAcfD`cNhaWedTE@A7t0mx*hI&yQe4B
zB3HfDQ7r>`jFcP=_**l~%#+i;C>xt_r3OUwL#XGt(JJRYb@Agqzrp{2XR6!5K$+T_
zI60@7Z)3xz?6qN&1DH8k{_jQ3k+x*b0UJ{HOwBAlgD_eIwgE-}Fd6LOGV=}Ep#eYt
z3n``y)4xq$*?#qqw6rU@;H?&ISUz998d}BS-ijb>{P*JS-|w-#FZA{gk&%?OH+;JR
zw;gI;3QB(%EB6kVare9=d>~LM?#?X0rnIFZK!D*az=0OW*Ym^h^<-n|O`n?`kAieI)vzQJ
z5g`@52d+;0l3gM%fPLWR7kddnY1BKXhVO*DBQQ-K@$5mEc-vbMjvt2qTcm`!>mw{0
zKuQH9fbkgM)}K#{Bum0ldT}#z^2qsPdj9Pxg5KW8u!n71A$i9l9po1gj3ra<)$N1=cG?L){6J5Llqi-l(=9$NLXc3~DNUsM
zgl$j<N6C4G^Xw7K|eToVip4A5d(8u
z(SHu9QaQL2KG)2-Y(^aKu9lhbGKsKf*!X(%;u7`UsXhMQk?V4iuggJkac276nK&^y
z{5PLI;-}?vB7@NfNYP6wgh;^)Ltc`FFtXYneB*c|kZjC&OPHaXB
zEU$XR=4sYQV6#p?$ZB&=AtMe>Jv5-K1mS2`%XwDlp?0%@HQzG%t`bhQ54tPn4>=u@
zkBwYT!3co~z(b(S?{w#>z*@99sCs`%v_RsXCHTC^BvJfRPe?TkNK~#J08KwQeWfC@
zyUkl{ys&f1W6sz6N~IYwsJ_BL$M+#)pmq20_J*}=9)ymhxXo)~Q;pGl5DZraaG7h#
zy!Nt6e5wMlUR`N)9%lT~(RX=z_JYbNL-Oypzv7>+)R!VnBhXrw3k}T`(3!VtPAE4#
zHx!MMUVkkQ?#FG;2+JuC0Bf>L1!-;0l{#SL9e>qJr9&p6qTg2=NkP{v2N%jBI;txZ
z+ybtiw?kSQn$aansuPIe_=qy^-Y7qoehwot)^M1mj!{N)LkoF)EIC#jk9DRDOX3+418|?+(wl*a2>lPho86rto4=Id0oR)P5u62|SjNRT
zNIm{Gwv)SQ_8c(8^XUD$M-e_F)Qgw~gLt?iwF*Fv-RaK298JUwS(DENQOk0D7c+QY!m2}eJhx)Y?SDwh`+;1
zzXR?=(@WFdg4uO#GeXi80pfv2lm@hNj5?YH1HKllIF5{
zjkDl5m?eR+{kzSFZ&Ls657Ur+M5*3+=-ie9G2dtJ0fkeGw&r;?ihz~7lr$@1l3wZf
zayjVmtr6qKN~^+G4tW_mRM3`VeN=Pj(>oKY3Cz_&d$rDKz}6#Ek*v!X8#EXvhVmAa
zJ>!nGeDXO(}{aZv^DJR#YiBSB@$G+5GESjLS5kmneBW;Ab+Iv}u
z%U!`80NlpL376!J$nA12J_v;wN=$SaCi%Te0Ef+Y>5HgoklJ^
zQzQ-{gx!^NmmR;@eYd`HN=~r!nv>n*2xp++qJN-E2_73PaP`vQQUU87cel6GluxJl
zMn2wfxPdHe7?FJb%NE*~yhDogc7-%!8$@jpK!H`gP1f7FFbXPXW(1P%PEq#F-3I)=
zRBmhgV`t~=52pDCI~n}7>1+YP@6`8M1aT_AW7m5cG
zkYyap^A>Ej4F2H8HkHPg`wN=akq41;Mro^*@-IqvS&5H`Vt!xdyf2Ka59f>3nt>{(
z`h5!TFaa%SQSI?$UkXzyZ^}Lvy4jLf_3~1DM!=%dxJ{D*We1*4&kh-47YL!;A)nRS<=rG*NzottO0tC-4`gO&ym0IrA7
z#9LhX@H??=0;+=cgz!gzbi0DqXjDTvRub#rSS9ow{6C!?&u*z?NQ!|_t-)14DysD@%?SE
z?5DifRi()eZhR)-Tpb)i%ot<4N^Iuz@v+d$;T3hfFHGe
zY*3%wWq|eUSsz8m?P`>i5kCq<6jH7NBAF;)WIE^P8E~zWKls0$7+gyG05%zborC%R
zbz(YG(IhRf-6xdipjyeL00RaH5Dw_q=CMr}{Nj?57bNgHr_qa$!tV-|E#59>J?_5t
zttC~ea3accV$rGliF~xMpT&LPpM;5tnb!+s-|j!%KlhE^FX~0;q@sz6wDKpSYXpr@
z&=`h=+Szjad;p2F$V9eX@Y9bwgUG&)cg!4#&*6@9&>G`**T=9J@G913kUyqLiN~pY
z-ah5>`giEfFHAlQ9gF^_T<)J|XCX%)CA!})-5D^6NW<$#2!#y8aWuY~t(Yy^g|m#S
zNBq!RazB!U4>#UVocx?5>2DE~KHX&_5%l9nAx9%Qw}6Yl8{ht!KPW&1m5>o}AOh%7
z#e^(MA2)U$@0mYGb6-EO?UC3tb063G`qKbk4>gWg`X5{PgKuF3#=u-jwbg02pO1}_
zr!4(AS;KtBS`xEPZC|}}UZgkvS*HuXF+7Vqv?)(>=N
zK|hqUH9(iia4#eSV;j1U+9f!FMOjz;ySvoNvC9R}ss6RlbVn_L41_WItr3X^ZJ&qf
z9Q0lb%W2Q;$KBuVW5G0gDfL{THuJe1KX2I{5{xce>Z3OaS__EP^}U3X@2zF)ygB6p
zcE^jA-DO&V2jLOF$zF+qN)#;%)08jx!2hu*`L+5f3&A
zT5aMmg}hn{`Pdrau?TY
z*Z^{;{KxKucciK44{C-pU9}0oaYTg1Je&ekLZqC#C37MR=(k63ET5n_2iYscBgrf>
zSi%Vi)W2Dzwd^~B2uW$`HsH7X<8)C`h;vBaA>H)y_F{P`u5z|%Y7Q@);(H9bDz
zEH8yTIM;6_UCX#rM4aa7lQ`1y#h>IGHh`69a8If&=u|!UOcCrhx0)uR3|kfJSfzlO
zu2;TW)j2>>`=)v3N;qG!mvbz!urSYl$W=5|@IWSl6itI#Oc*T_U@?iP4CdJguNk_I
zeyLBv_~2bq_H@^)gr_f|MAD{?6x;rXgr^pj#HM||4pS)J$c5%0HXypUfY)Hr7+_yD
z&i=LCmptqrbEEZF2t5R9`#mAP1^e|84lgXw%L9_ym=)>
zp7X1fTx7RjLgf<8+_cu3LgYON1i(DHfq0~!B~JnyVQIjEbtrC@Rh~P%gth7ZoUs=*
z1ys@X7zUA!qju44scyPhKzN*9h#BSARO!OPKBeP^G2~)K8L3%#*xaG1RlPiT;)`3c
zYyH(GiTv}j&mG*GTsE;!HQ|^?rVpoGEg09l5f6HUD>6)N>6(cMj7KgOJV1}pL?V6K
zE;>D%5MXT%&Am0{Y!kEG=E5{SZ)B9n2w}cdweV|4*%rt6C~Sn|Hr@bn=i~3)BzYQ9
z>a`DUtPkM_``S!=n(B)8_+Npt!>e{s+#4x9sRqq?uOa&Sf)p0>uQF|h!Yg!;?;Gte^maUn(9)9Jyp_qUZ2dFyc}DZA|7wwXv-Fai5!k#2`Q%gIl9
z?-w7f<^1OfOs4diw15wvQ~QKwUvONx;kRhb1|K&Mz&cDODiA4}k0m65m?{Fh13*we
z5FPV^aW$5gNw%jSkET>5_)E_lYoddbOs;hs{tvfsc2BRTf5KuMX=jm{ACSAD;0ihh
z-;rVy%tGv{bf;hlw(eMzOq@Bc*Tm{$JykCyFj-r|$lM5D1t1ALUo6U_y_zrzG&PDH
zqGr+;hdsWKM|?JFpCwTU*h-y}DW8WlE=bX&z`#*~S~NHD6QO_B0J7rRz9@6Hx=co_
z8J|+oW!&)g4=Pq#eyfbpBSiM9Ld_f0kkHf}x;Xqjss7&X>(CmI1FBnHP`Hk#KzKh;
zL$P$c(9DS&Qr(qGw3T?{K*&iCsIvf$&=0jE~MsmG|!jGo5Yv{(p|<)8n0DMq6AIZ*>X%X9OU*SPqhyn@sMv4VEX2K$Bgx!?SO=K5NWl7&y_UQA_W9oA>E5KX(*R7G
z-nR=Y2-{j@dK>wA3EJhdcSGG5SzsOfm(~0|j{P;$pv;w(UXJz>OIO`Rr|-Em>dGQa
z{o_(=IW{Sw>`Z#YUpb?ZZgjnc$v?yaMF<~%u4ptj7_AbkP1*y?_?x4Ww|EXL61Jh>
zSI`0|Z~&_rRXDR!S4l$x5gNz`oHfW&dL{ZF^8#Ln1}G*s%E-ir7OHl#SF%q^L8?kL
zGY8S)35u4Q*}Zjn2}Y7WLYxlulBff9q?O|rQF%rXVSCiUwP;nza0ikf+3Q>w=`Zuq
z!>$d>or-JFSFZ}QLV`EdsA@Xkw`yT9_nR}eo+jS6xf1AE
z!2o?{<#p5
zKFYwjoMljaic|;4*i+=O^KAjVh+B9u*%)wX8;GItN;pU%7eWJ80G)&z;%KOT297(X
zJ20Lp?y|Lu(1gB)iM8pq!wqE8M9l9>?$fsl-|w244XS(O7u9bQ-347ib6AOH!RdwzIHMG|1nZliHh
zMi26sM@2y=5U(KG^ArUo3OB8Ij0nh5f1Q1tV!u`V(WW|)42mD7h!#>HucX70CVuQ7
z9vqg-*m;6zz&(P?Zu1Z6z(O^0zLV@8t#9C;{A6R*MQ5
zXq##8|1?pdhtsz2+SEKhO5HwxDf7{`2yFqQTMR~%5xgdqM;tECI-Bpu?Hjhc+rbXP
zSFl53)L$&Nc*?+R^zF>!V|wjuVat4(N$+61FE*oAhq2sIaW$c%7|95n8mU2fG%Jsz
z6`Tf(SSewsqlycJDFwG{tO07*a>?H6J3;5Pu_`0%hsisCk`G2~@_i;BUwXhcrZOOn
z3C*pb+ZH*G6fZW|kN4+4NFivFoWbbsG#`3DCtg*9(WUO1s9iipD4Qe=3!)RfYxK+-
zVE?%ALevFQg(?>G)cHDQcVs-H9m&}_FAH81Uj{TUOi7Wil*_suS^y}Dr5hdX4;FDf
zE+z+eDcd?2&-xlA8BGj|w5qPiP~l7zD`@;yzunUX9Xke9=_B!A0%BOBy&zp
zqQl_ZxPWS0Wr_HY%71mIrxf8es-LDU`eGUAMNJn;G-dz#5a>*5oA=#uzE?h$x=}Cm
za`y3snY1Z4_Q7_ZQCg@He%j)6mYm3wa!c0`8M;sk)PW}1z?W5NGfT0qk4
zG2Ob&2;kk;q1C0mdE(5AWC{4AvDOr9v%5S;zdL1d$@%4P*x1>kSmykVL`V=X3b@Fm)MFOnt8H?^yR+B6cGBVp;J5P}C
zeD0Bs;F9bJxSB!FUzHGt|u*aC9m5KNQZn
z=jGh2{BYLdZ_Ge58{A~Q`PtK>(3VsaZ89X&0^HeWw@Nx%>dG-wFy+a6tdm6Di;H^tbhAi
z`QUssy0m`hopk3rFL++hgft@dPKugA&I-0fV=my{;$GOA@mXq1SVf{x-4-(Bqc}G}
zNqq8cf2_Fh{hakwOXNKNcLM&eufYGd5-E1u*kCE{3)ti!%#0~@k7yWx6q;^eK?sn+
z|4F^#^LqOPu5jO9DyW(y9ZU0*R(Kb^t8?WUCMzF;YE8xZLx7WIfhWZjJI`b_giWB39DLu*?{E90?+ouZ
zP;D{7PD^oNK4|UHcwXeW5L|az8baJXiQhz)PKINC2wM{GkH5xQDQ}cWb_vT7c#O>_zag-j+-XlZhjKwAM}q!;K0f*A(cI{7j7aA-C2
z*+Gg1gQ$@RSdMBWV_}EFJ2IU8;fDG^BY$^^fZ^U1M4-X#o>eQw=j>N}2Rd?jL5~R7
zJN-%{MaZ1&QO?&)>MauD_9G2#;SpZ8N_TZ;L3pwEyEEt~O^bLBA}2E9nW!bl6hyHr
z&SqUyiQ)klDvOY^@JqXcj~1$gSiFP--5IG8HIYymN7Wvw)l@*~bx)SqBPANF3d_io
ze9&r%Gi4;hG&1^VGFi=Ryj-n?@m5$;$tO!&wvOa1m*`k>aITR8;X^ZdbZA9A`(4p3Rf*nEH*Ryz4=Y~Z8nH3)}1
zUI{a%2j77_P?7U}_sQS8FG;F?c{-QQT0_l!iXil{H2fqR&yYVq8#ybPTYtbH#(lyNShQc1W&?+CjZ_fiF$AuEtkEo}+lL#@>8L@gkd`yGB^Ot+7bK#{wbiow!OIvpNvsUxE~EP)2;m{y_Z@-7RSJLlWJM?MCv1F~D
zCdxLGBAuY#T>`&XF?fm!?5-};;kQR>=EHBx8>UhMT3I*rGl?ZD1d)1&JA6FKLgVAu
zZ%1iP!EeWti5NMkOfQpmFF{PEx|YCzwa;>Tu8?%H$W%l8g{qF@qIYNmBbJ$_Wwrs#
ziihvVs&7b>R+_<HPS?R$@768s(gvu%_
zhyF%?z-eW}{qp{|S9$+~bsJa4IG|D3V*lMQB=f2YL>X%l;7Wt-sH$eJGtXo~Qb;2f7R6vrdXH`Fh8-zPy7gf=$P!q!aA?i_d5lBuS9CPtVfY*|-%
zvXGx{9+9rlZr4_}%h+CEh+`D#{3+$u>ywcm&I2aU^>Q=4)zg7HeSO3r$t-pzUl?#0
zXY6NH788kfEkB!aDx-*GjiF7ZmWeS{hda)=SeoS33PjqN6tn_wPV43Hd4Gy~(xwXi
z%ecFBQU1k;Z$4diaZ@w}L~~9f^X|q82iF@;jUhv4dCK}?4Egu!Trtt#^%-iI$#Rc^
zrV^}=sZ}LHlFyzlIq_^AK(3NFVfvp2mrN)ubg+g!F0&hAgR7vICmC+dS3HAI(
zslxKZs|*Eqmm!5V><)s^nv!OV&|14$=a!StgqpC`@cEziZu5TT`7AJ3q>g9^hw^us
zU5PNB5pv%@Mu1oCW{TlH(^P=_t`7wi?@0~v1finA;%1ZHXJv1q
zvItP1IhybradIGI){er6!HO^J)U6pH-xFW5TaREY=rrC@&$^~KOk(S&>S~uUxi#bh
z|BxLb90#q7^3e7JCpa#mpl7|SWPVRQsy_FH=ug&8^39Pk>X+ZpCsmdv#^
z5pw*>_T`cUv*W3F)g$H|*6}7xhURTJMVt<+XJ0jL8UwxQvmDc8wOEE;AghPLPM^_v
zmQZfLg|&3$V&;BI6x^zsAMkXmveV)8sxcuHOM%Ewc=r6m48oqR(wo_yzuptM%v2+*
zQ|2J;a!>>PR5;53x=9qTCiFj`V%&ZS{>NEx0qhK{|4)*mJr#4%`d^as?^{(;De!;E
zi|#M-;_@tAnr+nXyXO}?ZzB0o=9E-n9)RG*<2J@5szf3>o)e}I#VYYnIp_<$2z%1M
zeucx^u6=;Rd-#{KvK!Vz`PHn+kFxUMMf{Jx!1#~8xCXplPc@~?3mZWZbMGd8GeT-V
zU~k2H468lFtT5_wbL~z1UdHkUeXN&~VlEE)>ac7g{tJ2Uk}>y6_WGd!!SV0G
zweM-UZB*0sKlWkd)Jll
zpZJLbvA}>l|Nd!XYLOHQNHD9Rf})6RxCq+rxzH;wkM9(q+5X9&7x~8^Vhi!}!|mhl
zEkkIx=e=YrYJ**H@JAq-t|9;Szo#eqyX5US-mfHwfyAs3&kwVhP3eU{Y!`okL&KE@VM2UGK*6h3X3+t){C{yJ%>Vz0^Hbwle8hHCthh=1OO+lwY>{3@ik}
z_IJSy_6qq|C-=A^SKfZ?$Jp~V1DjoyJ1gDfz~-+EJvi^r@t@j}6b<$rnIJ<^h932D
z6cn5R>YhWzs`#vBXoujZ>SIt+Km{wSa;|kZwe_+=?g2z9l7e0Cw`dUh9m*LHt2~=L
zo)j&QPO?uBoRyAbl!_x91Gt6zTL>X>?_tiVK^t^X;^=6|q{a);1DNHtzoN@+CM^+K
zB`T4-Djh;mVWu}T6~g;OxjTEK2jrHWEcIPH^*Lh8#*%$UXQ7N`4A!t6KvY?L`-1)C
z{xj0N?(}l@Y+(pwZ;}}CTOItKv|iX?7u~JvJRaWCGKDYcV{1h?AWt=1H#zS6eH4
z1}uY=|4r5zE^7B8w{HAY>a2s3laA)4(3t5+A=qrw(|k3Y>ub?_x{6eRMzfZ>9=v&_
zI4IL4JJ#`E5r+Yc*&=E|KQbmr@872}q+KZ7z1X)*DS1
zu}9+kTK`j+`m(b?<7mw+9T8zNS2fHKZxl^iWO@<1X19rIXJK_{qqK&=dNAAP)T_c0
z<15*Q{Oh)Xnn|;Q=u9UI@!U;
z&_8m*@HK3#`&9d5_D=gPbd7AoNziJJ)fttq=b3M*m6?3!%y`v
zs$Kr@KRwEfHc?1Bq-wt_mK>1whpnEurzGjZ9NQjd)dyPChhQrj4P2|?rhl~zwK7aS
z2-5w&q6DFZM(MYS@`M~KdR|jd)L|NDVM{uk*h5#jwxu<@?*!cb&}H0AZ^R3!VN%C=
zCL4EHRiasHPuZ!4+OooU0ix}(kM+N*mn>2`^$Ob*lP+tSXoJFAYu(C;Z_i1OT?11!
zyo%zpMf=rU?-Mu`ExpxD^+TSt6c!8nP0UE@S#D+a@b~(REhcfIBHHU54DicHC78{P
z|I{7{+dz?v|=0K3r3N2ipmb^ux5)uw4uA
zNaNWwwVO7!+Bw?y8SN}um}rDP{pD_bh3TF!WAJJ^e*|D*#p&mfRt87teK^j!a;2+v
zv~T`894K2_Z`}70qco1MmjDcFyehqy+-YS)lq*7FIsYaHk6>g}TMp$Go^;2ZH1(F3
z;tOk%NBXd~+J+>%*m7}qJgWF@I1DH^WG|l*voUm`-3VbXr1>YRDD2fw4$RSs+HYMH
zw#5HElmvKd#AMR{HN8KUb;WvU(|fsLOXt2@EMQ1WQf^HVw$DKuONGkVpGuuM`sshM-a#+&*SE<7<`Yf%BLp#VICE=sr2~O$d5p9BC~Hg^NeyF~*E~8)+?t
z&<+rO)DDUU6$)S5Sgr_t(B-5HDYSxQO}C#VT=7_pF{r36$V0r-&NOCDYN^C8*p9hm
zpE_MWwR6?$H|ptVv=V}cEqLk3Mv&!RUC^OnE)eDtCXC-5Ikyq}>DuhlM0Rhp9@lLZ
zSt9({e71LyZG@Yb^EME$iL&|wujU0)_W;0Xw$3Y`YTs$n(zj~a{%O0u(WO{9+&X^1
z%kiH4jdW|j+2~;jPHoOp+yxsN5XMmsf_tAiv$l0NuY3Z+wKgaRZ)taf)ZEL7mu7hmA0F*WU)xAxs*3T%lQv+E
zk1mh6S_(nj8H>2xQ_lsBVEFX0v{m(VyY7R(`SB0Kp&vJHNoWBAlABB+o>GGclR1jQ
z@Duh#5oz6w21A8;B==Ss2COlV=&-}=yC{`E(dQqqX$;2Og>FWNE!hvg+0MW=gy}|cB%V;10rFai&EFNEoyeFqkj9k7KExh0-Br}DkbQ0S9
zs%}|?%MirGF{CZmBLSz7DJjj(>pg>*f-3kjm7fB0>1Ed=&2@*AIfScEU&iV*F)S+X
zg{~^IJBCtmO_LmW7IU2K+K7vr{i0TP8vkYfVr;64UDjcmV+tzbDkXO|=hW^vN4`ZbsZ2R|L&f~Zr_xzJ_<&*yl2=ks|lY=pT
zjb9Nfv2g$b_&|`GZ{4=_>;q7iBp0OLjgI5C<gbCUY)Z4vpaEEe%YNCQubrH|Htn1
zZ1K;}w{BUeVr>8$W_z}LYlm~LVMN}`mvI;nphxJ+OqjO^7Hdlm>n6WbXV&
z8W-VSy~r7n9|i^9eL60l^i^O+BApLpZtDWJA?7|*a{#_D`+h_06?}#`s|X#(_Iny2
zdOdt)p<`x!Ig*GZ-L`}W=d8@Hk2VG&Q7ptL8XiSR72E)O8puw@@{0iT2n&`H=E2!*
z5HLnA%`N}Nfztp|>3Z+eOaX7>?R!IanRusE(ZYL{I4?bvyxt109D-jpc#>HYKNJE#;=m(Ef)t@lBHtzGnB7{v@
zy+UNEeGMrTAW*Ag8?T6rVY(2I4Pq-Uf4#ogOnm=D9O^-81fio7Alx759qpywcs?qk
z%A1YpPVy~$^12#fn4-}fhQgai`a;GHs}%OxX3;XZ4D{&`YYx|oTtq|gt!)SxD0`Jg
z8GuvEZP-B*K4XC{9mYFWk4}W(@7KrPZK|-yL{yqUDW|0{C(^oRe@3@)PTsP{zh+MK
zM*+Py@JGNcSQFG4_cL)bmY*MIp7rfCdMxsSlI$edppO)|Ck9aYbN6ODekbz0A@%^s+TR-YF&aaW$OF;1R^xH7Y$R)1Chv!&XnR8?%5+43
zE4ZMEhDjh%#jL}8+2&deE9KfHLENgkv~=8psOl*+5;mJB+@6ZHD)l_=US+EldwPn`
zNHXgdCZbdy4!N-$fvc+Z
zK%}u>k|G0(;6Uz~)P4WM^{p)xT*_awFtG7o;~S;JHe}Ep^I_+-qpXO5)u5qLhK+_l
zi$)pQ4_xHZj>TFzCr4>F&KQg{f4&+kz6~&?md;X9?}5a^>lYyQ;wL>fiA_*H1ETp=QzPDy$fRTy~YA89}|gSOE_h6
z1eK_p_uDWTr!}bc|LEj%CNh40)9Pj_oMAoc;y4_NcX~B^y&-?*>fibDu5p2sH;G-!
ztp~Y@ZmIl0U@pD50W0K7;ScHl6t7Qn3P%FjasT}A`k2_z1APJXKbd=EHs}dwBN?#{
z(C^`<_<_$xn-{ceR5r~D@{$nu>+SnHm5sR5&&*;#CJ8p(i1Esv4hbSsa8z3@Yu>?`
z8a2J!0goo*d6w;;R&$t^?DtyO?hQOE@~9Pyci`V$PIAYLHi)-jH1N&f+5!FF2?~h!
zy@Wi7O(Mfp{}ezZ=JAr(f0`UeMGb8qWZewe%FW^pYb6cR;ZKX%j5E-z)jPiyu%%Pr
z1Oj;;9uhlo4)ZtX;QO|swdRNyDgoI7TJ){444DWoR|rJbw8uY#W)g83jL!WSjuJA1
zeY5@eIf=&yB-qJ6Yz6~TynRe~2(4Pf1E3A2JXj3c!=gYdejWUN@X}0O6y&{`&coOI
zs_4#ZqBq+g)n}5|!ap0r^k}JShVyD!ral$rinJ
zlbGht`Dr+I;$f6lxWU#5?(O-~mX+-hWXO&k@M=DslEzY8VLR8;GcL4b42&0e^*{97
z7l}PG!@I)|9qv+sD>Vn?Jnz`n&PW1Te3=k+h$(=2$Bs-tO!H^l(6JC-*58Mrnz3?f
zkjwt7;b(Em`*QJAhgX8{CjLPX0$TQFtk&H$`-L;wMQDEw&2Hc|QX9kT$zJ2w!E9z3
z_~U*x7Ly6FYy9lC{9H(b>V5Bk@DM=@9!I-Arnlt)3&1#Hn4X$!}kvVLb`FaORmNKNL7AG
zL0Y3S5~WT=Y{+oDTkj8vl+GkA*`Q$lJ{zWb+W<0ZC*qdxsSo|*4uiLJ!=_4FPqz>F
zqu23A>Lsk#P{hXLFw*(PY6K3py{TD2#t%hXy;DuIxDE&Z7F*_H!AKFtE+xj9dy76*q}53`d&Gf7lUQ+W
z$8{3x_vy?BiwYXar{dsJN33n8^`QZfTGvb$UiznHQiENYkIuEiq?Olx!{ENq<>4yy
zXq!U4N-#}1FmIbe^IgF+(S()5P-8h1s;+wG%mSZ~?|YHeFV7Gsc%oy>@lyrVI2k*c~Xcqtb(ce(#H%@g0wZnfV)^tG)jGJ}f$5t_rEABi%)&ORV
z*);@krEWU}o_V{#j*#>1)x2jVcI$ByG~2!NB8sj&{M`9kO-6&io`-F6xHHy|6>pY;
z1P@&bW0XBNs(PfoYL%kUR(4om(LX;ppL?W-(M()4$(_cTwV)Hwu}v#RY*e}t$`tx`*8&G
zrIUqq69gID9Erq^WOZNt4k>+L)Tw%hUyBxBeh&+ZHuRBYW}9zpL6-@rlhmlnIWyYe
zR0}h^atWj2*kuS>l6T7C_DQY(LyW~dEs@EsYSd$ZJVx76F&T>-p1_T0(ZMN
zja-nNFL||ajr>($w60FM!wrACFB#9>FZ~)I!|k`9uM(2BBc`_Z
znOknxUMZ$t-V~SUU-v;Ux$Atca*!@Bk>Yr3r5*b^avE~yxeZ`KQWD__)%U@Uy;Xjs
zw%AewD&K~d6=s-IY+7l*FqTT5*y