\\△\bigtriangleup∆\symmdiff∅You may plug in any value of type U, say a, for x and use this given to conclude that P a is true.
This strategy says that if you have h : ∀ (x : U), P x and a : U, then you can infer P a. Indeed, in this situation Lean will recognize h a as a proof of P a. For example, you can write have h' : P a := h a in a Lean tactic-mode proof, and Lean will add h' : P a to the tactic state. Note that a here need not be simply a variable; it can be any expression denoting an object of type U.
Let’s try these strategies out in a Lean proof. In Lean, if you don’t want to give a theorem a name, you can simply call it an example rather than a theorem, and then there is no need to give it a name. In the following theorem, you can enter the symbol ∀ by typing \forall or \all, and you can enter ∃ by typing \exists or \ex.
Let’s try these strategies out in a Lean proof. In Lean, if you don’t want to give a theorem a name, you can simply call it an example rather than a theorem, and then there is no need to give it a name. In the following example, you can enter the symbol ∀ by typing \forall or \all, and you can enter ∃ by typing \exists or \ex.
example (U : Type) (P Q : Pred U)
@@ -824,8 +824,8 @@ To use
\\
△\bigtriangleup∆\symmdiff∅theorem Exercise_3_5_24a (U : Type) (A B C : Set U) :
- (A ∪ B) △ C ⊆ (A △ C) ∪ (B △ C) := sorryIt takes a few seconds for Lean to search its library of theorems, but eventually a blue squiggle appears under apply?, indicating that the tactic has produced an answer. You will find the answer in the Infoview pane: Try this: exact or_comm. The word exact is the name of a tactic that we have not discussed; it is a shorthand for show _ from, where the blank gets filled in with the goal. Thus, you can think of apply?’s answer as a shortened form of the tactic
It takes a few seconds for Lean to search its library of theorems, but eventually a blue squiggle appears under apply?, indicating that the tactic has produced an answer. You will find the answer in the Infoview pane: Try this: exact Or.comm. The word exact is the name of a tactic that we have not discussed; it is a shorthand for show _ from, where the blank gets filled in with the goal. Thus, you can think of apply?’s answer as a shortened form of the tactic
show x ∈ X ∨ x ∈ Y ↔ x ∈ Y ∨ x ∈ X from or_commshow x ∈ X ∨ x ∈ Y ↔ x ∈ Y ∨ x ∈ X from Or.commOf course, this is precisely the step we used earlier to complete the proof.
+The command #check @Or.comm will tell you that Or.comm is just an alternative name for the theorem or_comm. So the step suggested by the apply? tactic is essentially the same as the step we used earlier to complete the proof.
Usually your proof will be more readable if you use the show tactic to state explicitly the goal that is being proven. This also gives Lean a chance to correct you if you have become confused about what goal you are proving. But sometimes—for example, if the goal is very long—it is convenient to use the exact tactic instead. You might think of exact as meaning “the following is a term-mode proof that is exactly what is needed to prove the goal.”
The apply? tactic has not only come up with a suggested tactic, it has applied that tactic, and the proof is now complete. You can confirm that the tactic completes the proof by replacing the line apply? in the proof with apply?’s suggested exact tactic.
The apply? tactic is somewhat unpredictable; sometimes it is able to find the right theorem in the library, and sometimes it isn’t. But it is always worth a try. Another way to try to find theorems is to visit the documentation page for Lean’s mathematics library, which can be found at https://leanprover-community.github.io/mathlib4_docs/.
theorem Exercise_3_6_6b (U : Type) :
diff --git a/docs/Chap4.html b/docs/Chap4.html
index 3b99727..cf9df52 100644
--- a/docs/Chap4.html
+++ b/docs/Chap4.html
@@ -238,7 +238,7 @@ In This Chapter
$$
\newcommand{\setmin}{\mathbin{\backslash}}
-\newcommand{\symmdiff}{\bigtriangleup}
+\newcommand{\symmdiff}{\mathbin{∆}}
$$
diff --git a/docs/Chap5.html b/docs/Chap5.html
index 14f9a44..72bba00 100644
--- a/docs/Chap5.html
+++ b/docs/Chap5.html
@@ -238,7 +238,7 @@ In This Chapter
$$
\newcommand{\setmin}{\mathbin{\backslash}}
-\newcommand{\symmdiff}{\bigtriangleup}
+\newcommand{\symmdiff}{\mathbin{∆}}
$$
diff --git a/docs/Chap6.html b/docs/Chap6.html
index 32e1c29..cbc4362 100644
--- a/docs/Chap6.html
+++ b/docs/Chap6.html
@@ -238,7 +238,7 @@ In This Chapter
$$
\newcommand{\setmin}{\mathbin{\backslash}}
-\newcommand{\symmdiff}{\bigtriangleup}
+\newcommand{\symmdiff}{\mathbin{∆}}
$$
@@ -902,7 +902,7 @@ 6.3. Recursion
So we have three inequalities that we need to prove before we can justify the steps of the calculational proof: n + 1 > 0, n + 1 > 2, and 2 ^ n > 0. We’ll insert have steps before the calculational proof to assert these three inequalities. If you try it, you’ll find that linarith can prove the first two, but not the third.
How can we prove 2 ^ n > 0? It is often helpful to think about whether there is a general principle that is behind a statement we are trying to prove. In our case, the inequality 2 ^ n > 0 is an instance of the general fact that if m and n are any natural numbers with m > 0, then m ^ n > 0. Maybe that fact is in Lean’s library:
example (m n : Nat) (h : m > 0) : m ^ n > 0 := by ++apply?::
-The apply? tactic comes up with exact Nat.pos_pow_of_pos n h, and #check @pos_pow_of_pos gives the result
+The apply? tactic comes up with exact Nat.pos_pow_of_pos n h, and #check @Nat.pos_pow_of_pos gives the result
@Nat.pos_pow_of_pos : ∀ {n : ℕ} (m : ℕ), 0 < n → 0 < n ^ m
@@ -947,7 +947,7 @@ 6.3. Recursion
_ = 2 ^ (n + 1) := by ring
done
doneThe next example in HTPI is a proof of one of the laws of exponents: a ^ (m + n) = a ^ m * a ^ n. Lean’s definition of exponentiation with natural number exponents is recursive. For some reason, the definitions are slightly different for different kinds of bases. The definitions Lean uses are essentially as follows:
The next example in HTPI is a proof of one of the laws of exponents: a ^ (m + n) = a ^ m * a ^ n. Lean’s definition of exponentiation with natural number exponents is recursive. The definitions Lean uses are essentially as follows:
--For natural numbers b and k, b ^ k = nat_pow b k:
def nat_pow (b k : Nat) : Nat :=
match k with
@@ -958,7 +958,7 @@ 6.3. Recursion
def real_pow (b : Real) (k : Nat) : Real :=
match k with
| 0 => 1
- | n + 1 => b * (real_pow b n)Let’s prove the addition law for exponents:
theorem Example_6_3_2_cheating : ∀ (a : Real) (m n : Nat),
a ^ (m + n) = a ^ m * a ^ n := by
@@ -984,13 +984,12 @@ 6.3. Recursion
show a ^ (m + (n + 1)) = a ^ m * a ^ (n + 1) from
calc a ^ (m + (n + 1))
_ = a ^ ((m + n) + 1) := by rw [add_assoc]
- _ = a * a ^ (m + n) := by rfl
- _ = a * (a ^ m * a ^ n) := by rw [ih]
- _ = a ^ m * (a * a ^ n) := by
- rw [←mul_assoc, mul_comm a, mul_assoc]
- _ = a ^ m * (a ^ (n + 1)) := by rfl
- done
- doneFinally, we’ll prove the theorem in Example 6.3.4 of HTPI, which again involves exponentiation with natural number exponents. Here’s the beginning of the proof:
For the second sorry step, we’ll need to know that n * x ^ 2 ≥ 0. To prove it, we start with the fact that the square of any real number is nonnegative:
@sq_nonneg : ∀ {R : Type u_1} [inst : LinearOrderedRing R]
- (a : R), 0 ≤ a ^ 2@sq_nonneg : ∀ {α : Type u_1} [inst : LinearOrderedSemiring α]
+ [inst_1 : ExistsAddOfLE α]
+ (a : α), 0 ≤ a ^ 2As usual, we don’t need to pay much attention to the implicit arguments; what is important is the last line, which tells us that sq_nonneg x is a proof of x ^ 2 ≥ 0. To get n * x ^ 2 ≥ 0 we just have to multiply both sides by n, which we can justify with the rel tactic, and then one more application of rel will handle the remaining sorry. Here is the complete proof:
theorem Example_6_3_4 : ∀ (x : Real), x > -1 →
@@ -1138,10 +1138,10 @@ 6.3. Recursion
_ = 0 := by ring
show (1 + x) ^ (n + 1) ≥ 1 + (n + 1) * x from
calc (1 + x) ^ (n + 1)
- _ = (1 + x) * (1 + x) ^ n := by rfl
- _ ≥ (1 + x) * (1 + n * x) := by rel [ih]
- _ = 1 + x + n * x + n * x ^ 2 := by ring
- _ ≥ 1 + x + n * x + 0 := by rel [h4]
+ _ = (1 + x) ^ n * (1 + x) := by rfl
+ _ ≥ (1 + n * x) * (1 + x) := by rel [ih]
+ _ = 1 + n * x + x + n * x ^ 2 := by ring
+ _ ≥ 1 + n * x + x + 0 := by rel [h4]
_ = 1 + (n + 1) * x := by ring
done
doneSection 6.4 of HTPI ends with an example of an application of the well ordering principle. The example gives a proof that \(\sqrt{2}\) is irrational. If \(\sqrt{2}\) were rational, then there would be natural numbers \(p\) and \(q\) such that \(q \ne 0\) and \(p/q = \sqrt{2}\), and therefore \(p^2 = 2q^2\). So we can prove that \(\sqrt{2}\) is irrational by showing that there do not exist natural numbers \(p\) and \(q\) such that \(q \ne 0\) and \(p^2 = 2q^2\).
+Section 6.4 of HTPI ends with an example of an application of the well-ordering principle. The example gives a proof that \(\sqrt{2}\) is irrational. If \(\sqrt{2}\) were rational, then there would be natural numbers \(p\) and \(q\) such that \(q \ne 0\) and \(p/q = \sqrt{2}\), and therefore \(p^2 = 2q^2\). So we can prove that \(\sqrt{2}\) is irrational by showing that there do not exist natural numbers \(p\) and \(q\) such that \(q \ne 0\) and \(p^2 = 2q^2\).
The proof uses a definition from the exercises of Section 6.1:
def nat_even (n : Nat) : Prop := ∃ (k : Nat), n = 2 * kWe will also use the following lemma, whose proof we leave as an exercise for you:
@@ -1376,7 +1376,7 @@@mul_left_cancel_iff_of_pos : ∀ {α : Type u_1} {a b c : α}
[inst : MulZeroClass α] [inst_1 : PartialOrder α]
- [inst_2 : PosMulMonoRev α],
+ [inst_2 : PosMulReflectLE α],
0 < a → (a * b = a * c ↔ b = c)To show that \(\sqrt{2}\) is irrational, we will prove the statement
@@ -1387,7 +1387,7 @@S = {q : Nat | ∃ (p : Nat), p * p = 2 * (q * q) ∧ q ≠ 0}would be nonempty, and therefore, by the well ordering principle, it would have a smallest element. We then show that this leads to a contradiction. Here is the proof.
+would be nonempty, and therefore, by the well-ordering principle, it would have a smallest element. We then show that this leads to a contradiction. Here is the proof.
theorem Theorem_6_4_5 :
¬∃ (q p : Nat), p * p = 2 * (q * q) ∧ q ≠ 0 := by
set S : Set Nat :=
diff --git a/docs/Chap7.html b/docs/Chap7.html
index dcca3a5..f68f104 100644
--- a/docs/Chap7.html
+++ b/docs/Chap7.html
@@ -238,7 +238,7 @@ In This Chapter
$$
\newcommand{\setmin}{\mathbin{\backslash}}
-\newcommand{\symmdiff}{\bigtriangleup}
+\newcommand{\symmdiff}{\mathbin{∆}}
$$
@@ -282,11 +282,11 @@ 7.1. Greatest Com
theorem dvd_a_of_dvd_b_mod {a b d : Nat}
(h1 : d ∣ b) (h2 : d ∣ (a % b)) : d ∣ a := sorry
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
- | 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?
+ | 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?
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:
Clearly this calculation will go on forever and will never produce an answer. So the definition of loop does not actually succeed in defining a function from Nat to Nat.
Lean insists that recursive definitions must avoid such nonterminating calculations. Why did it accept all of our previous recursive definitions? The reason is that in each case, the definition of the value of the function at a natural number n referred only to values of the function at numbers smaller than n. Since a decreasing list of natural numbers cannot go on forever, such definitions lead to calculations that are guaranteed to terminate.
What about our recursive definition of gcd a b? This function has two arguments, a and b, and when b = n + 1, the definition asks us to compute gcd (n + 1) (a % (n + 1)). The first argument here could actually be larger than the first argument in the value we are trying to compute, gcd a b. But the second argument will always be smaller, and that will suffice to guarantee that the calculation terminates. We can tell Lean to focus on the second argument by adding a termination_by clause to the end of our recursive definition:
What about our recursive definition of gcd a b? This function has two arguments, a and b, and when b = n + 1, the definition asks us to compute gcd (n + 1) (a % (n + 1)). The first argument here could actually be larger than the first argument in the value we are trying to compute, gcd a b. But the second argument will always be smaller, and that will suffice to guarantee that the calculation terminates. We can tell Lean to focus on the second argument b by adding a termination_by clause to the end of our recursive definition:
def gcd (a b : Nat) : Nat :=
match b with
| 0 => a
| n + 1 => **gcd (n + 1) (a % (n + 1))::
- termination_by gcd a b => bUnfortunately, Lean still isn’t satisfied, but the error message this time is more helpful. The message says that Lean failed to prove termination, and at the end of the message it says that the goal it failed to prove is a % (n + 1) < Nat.succ n. Here Nat.succ n denotes the successor of n—that is, n + 1—so Lean was trying to prove that a % (n + 1) < n + 1, which is precisely what is needed to show that the second argument of gcd (n + 1) (a % (n + 1)) is smaller than the second argument of gcd a b when b = n + 1. We’ll need to provide a proof of this goal to convince Lean to accept our recursive definition. Fortunately, it’s not hard to prove:
Unfortunately, Lean still isn’t satisfied, but the error message this time is more helpful. The message says that Lean failed to prove termination, and at the end of the message it says that the goal it failed to prove is a % (n + 1) < n + 1, which is precisely what is needed to show that the second argument of gcd (n + 1) (a % (n + 1)) is smaller than the second argument of gcd a b when b = n + 1. We’ll need to provide a proof of this goal to convince Lean to accept our recursive definition. Fortunately, it’s not hard to prove:
lemma mod_succ_lt (a n : Nat) : a % (n + 1) < n + 1 := by
have h : n + 1 > 0 := Nat.succ_pos n
show a % (n + 1) < n + 1 from Nat.mod_lt a h
@@ -313,7 +313,7 @@ 7.1. Greatest Com
| n + 1 =>
have : a % (n + 1) < n + 1 := mod_succ_lt a n
gcd (n + 1) (a % (n + 1))
- termination_by gcd a b => 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.
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
@@ -444,10 +443,10 @@ 7.1. Greatest Com
++#eval:: gcd_c1 672 161 --Answer: 6
++#eval:: gcd_c2 672 161 --Answer: -25
--Note 6 * 672 - 25 * 161 = 4032 - 4025 = 7 = gcd 672 161
-
Finally, we turn to Theorem 7.1.6 in HTPI, which expresses one of the senses in which gcd a b is the greatest common divisor of a and b. Our proof follows the strategy of the proof in HTPI, with one additional step: we begin by using the theorem Int.coe_nat_dvd to change the goal from d ∣ gcd a b to ↑d ∣ ↑(gcd a b) (where the coercions are from Nat to Int), so that the rest of the proof can work with integer algebra rather than natural-number algebra.
+Finally, we turn to Theorem 7.1.6 in HTPI, which expresses one of the senses in which gcd a b is the greatest common divisor of a and b. Our proof follows the strategy of the proof in HTPI, with one additional step: we begin by using the theorem Int.natCast_dvd_natCast to change the goal from d ∣ gcd a b to ↑d ∣ ↑(gcd a b) (where the coercions are from Nat to Int), so that the rest of the proof can work with integer algebra rather than natural-number algebra.
theorem Theorem_7_1_6 {d a b : Nat} (h1 : d ∣ a) (h2 : d ∣ b) :
d ∣ gcd a b := by
- rewrite [←Int.coe_nat_dvd] --Goal : ↑d ∣ ↑(gcd a b)
+ rewrite [←Int.natCast_dvd_natCast] --Goal : ↑d ∣ ↑(gcd a b)
set s : Int := gcd_c1 a b
set t : Int := gcd_c2 a b
have h3 : s * ↑a + t * ↑b = ↑(gcd a b) := gcd_lin_comb b a
@@ -555,7 +554,7 @@ 7.2. Prime Factorizati
show p ∣ n from dvd_trans h7.right h8
done
done
-Of course, by the well ordering principle, an immediate consequence of this lemma is that every number greater than or equal to 2 has a smallest prime factor.
+Of course, by the well-ordering principle, an immediate consequence of this lemma is that every number greater than or equal to 2 has a smallest prime factor.
lemma exists_least_prime_factor {n : Nat} (h : 2 ≤ n) :
∃ (p : Nat), prime_factor p n ∧
∀ (q : Nat), prime_factor q n → p ≤ q := by
@@ -659,7 +658,7 @@ 7.2. Prime Factorizati
List.length (a :: as) = Nat.succ (List.length as)
@List.exists_cons_of_ne_nil : ∀ {α : Type u_1} {l : List α},
- l ≠ [] → ∃ (b : α), ∃ (L : List α), l = b :: L
+ l ≠ [] → ∃ (b : α) (L : List α), l = b :: L
And we’ll need one more lemma, which follows from the three theorems above; we leave the proof as an exercise for you:
lemma exists_cons_of_length_eq_succ {A : Type}
@@ -812,7 +811,7 @@ 7.2. Prime Factorizati
theorem Theorem_7_2_2 {a b c : Nat}
(h1 : c ∣ a * b) (h2 : rel_prime a c) : c ∣ b := by
- rewrite [←Int.coe_nat_dvd] --Goal : ↑c ∣ ↑b
+ rewrite [←Int.natCast_dvd_natCast] --Goal : ↑c ∣ ↑b
define at h1; define at h2; define
obtain (j : Nat) (h3 : a * b = c * j) from h1
set s : Int := gcd_c1 a c
@@ -1871,7 +1870,7 @@ 7.5. Public-Key Cr
done
We will also need to use Lemma 7.4.5 from HTPI. To prove that lemma in Lean, we will use Theorem_7_2_2, which says that for natural numbers a, b, and c, if c ∣ a * b and c and a are relatively prime, then c ∣ b. But we will need to extend the theorem to allow b to be an integer rather than a natural number. To prove this extension, we use the Lean function Int.natAbs : Int → Nat, which computes the absolute value of an integer. Lean knows several theorems about this function:
-@Int.coe_nat_dvd_left : ∀ {n : ℕ} {z : ℤ}, ↑n ∣ z ↔ n ∣ Int.natAbs z
+@Int.natCast_dvd : ∀ {n : ℤ} {m : ℕ}, ↑m ∣ n ↔ m ∣ Int.natAbs n
Int.natAbs_mul : ∀ (a b : ℤ),
Int.natAbs (a * b) = Int.natAbs a * Int.natAbs b
@@ -1881,9 +1880,9 @@ 7.5. Public-Key Cr
With the help of these theorems, our extended version of Theorem_7_2_2 follows easily from the original version:
theorem Theorem_7_2_2_Int {a c : Nat} {b : Int}
(h1 : ↑c ∣ ↑a * b) (h2 : rel_prime a c) : ↑c ∣ b := by
- rewrite [Int.coe_nat_dvd_left, Int.natAbs_mul,
+ rewrite [Int.natCast_dvd, Int.natAbs_mul,
Int.natAbs_ofNat] at h1 --h1 : c ∣ a * Int.natAbs b
- rewrite [Int.coe_nat_dvd_left] --Goal : c ∣ Int.natAbs b
+ rewrite [Int.natCast_dvd] --Goal : c ∣ Int.natAbs b
show c ∣ Int.natAbs b from Theorem_7_2_2 h1 h2
done
With that preparation, we can now prove Lemma_7_4_5.
@@ -1951,44 +1950,43 @@ 7.5. Public-Key Cr
ring
done
have h8 : [m]_p = [0]_p := (cc_eq_iff_congr _ _ _).rtl h7
- have h9 : 0 < (e * d) := by
+ have h9 : e * d ≠ 0 := by
rewrite [h2]
- have h10 : 0 ≤ (p - 1) * s := Nat.zero_le _
- linarith
- done
- have h10 : (0 : Int) ^ (e * d) = 0 := zero_pow h9
- have h11 : [c ^ d]_p = [m]_p :=
- calc [c ^ d]_p
- _ = [c]_p ^ d := by rw [Exercise_7_4_5_Nat]
- _ = ([m]_p ^ e) ^ d := by rw [h5]
- _ = [m]_p ^ (e * d) := by ring
- _ = [0]_p ^ (e * d) := by rw [h8]
- _ = [0 ^ (e * d)]_p := Exercise_7_4_5_Int _ _ _
- _ = [0]_p := by rw [h10]
- _ = [m]_p := by rw [h8]
- show c ^ d ≡ m (MOD p) from (cc_eq_iff_congr _ _ _).ltr h11
- done
- · -- Case 2. h6 : ¬p ∣ m
- have h7 : rel_prime m p := rel_prime_of_prime_not_dvd h1 h6
- have h8 : rel_prime p m := rel_prime_symm h7
- have h9 : NeZero p := prime_NeZero h1
- have h10 : (1 : Int) ^ s = 1 := by ring
- have h11 : [c ^ d]_p = [m]_p :=
- calc [c ^ d]_p
- _ = [c]_p ^ d := by rw [Exercise_7_4_5_Nat]
- _ = ([m]_p ^ e) ^ d := by rw [h5]
- _ = [m]_p ^ (e * d) := by ring
- _ = [m]_p ^ ((p - 1) * s + 1) := by rw [h2]
- _ = ([m]_p ^ (p - 1)) ^ s * [m]_p := by ring
- _ = ([m]_p ^ (phi p)) ^ s * [m]_p := by rw [phi_prime h1]
- _ = [1]_p ^ s * [m]_p := by rw [Theorem_7_4_2 h8]
- _ = [1 ^ s]_p * [m]_p := by rw [Exercise_7_4_5_Int]
- _ = [1]_p * [m]_p := by rw [h10]
- _ = [m]_p * [1]_p := by ring
- _ = [m]_p := Theorem_7_3_6_7 _
- show c ^ d ≡ m (MOD p) from (cc_eq_iff_congr _ _ _).ltr h11
- done
- done
+ show (p - 1) * s + 1 ≠ 0 from Nat.add_one_ne_zero _
+ done
+ have h10 : (0 : Int) ^ (e * d) = 0 := zero_pow h9
+ have h11 : [c ^ d]_p = [m]_p :=
+ calc [c ^ d]_p
+ _ = [c]_p ^ d := by rw [Exercise_7_4_5_Nat]
+ _ = ([m]_p ^ e) ^ d := by rw [h5]
+ _ = [m]_p ^ (e * d) := by ring
+ _ = [0]_p ^ (e * d) := by rw [h8]
+ _ = [0 ^ (e * d)]_p := Exercise_7_4_5_Int _ _ _
+ _ = [0]_p := by rw [h10]
+ _ = [m]_p := by rw [h8]
+ show c ^ d ≡ m (MOD p) from (cc_eq_iff_congr _ _ _).ltr h11
+ done
+ · -- Case 2. h6 : ¬p ∣ m
+ have h7 : rel_prime m p := rel_prime_of_prime_not_dvd h1 h6
+ have h8 : rel_prime p m := rel_prime_symm h7
+ have h9 : NeZero p := prime_NeZero h1
+ have h10 : (1 : Int) ^ s = 1 := by ring
+ have h11 : [c ^ d]_p = [m]_p :=
+ calc [c ^ d]_p
+ _ = [c]_p ^ d := by rw [Exercise_7_4_5_Nat]
+ _ = ([m]_p ^ e) ^ d := by rw [h5]
+ _ = [m]_p ^ (e * d) := by ring
+ _ = [m]_p ^ ((p - 1) * s + 1) := by rw [h2]
+ _ = ([m]_p ^ (p - 1)) ^ s * [m]_p := by ring
+ _ = ([m]_p ^ (phi p)) ^ s * [m]_p := by rw [phi_prime h1]
+ _ = [1]_p ^ s * [m]_p := by rw [Theorem_7_4_2 h8]
+ _ = [1 ^ s]_p * [m]_p := by rw [Exercise_7_4_5_Int]
+ _ = [1]_p * [m]_p := by rw [h10]
+ _ = [m]_p * [1]_p := by ring
+ _ = [m]_p := Theorem_7_3_6_7 _
+ show c ^ d ≡ m (MOD p) from (cc_eq_iff_congr _ _ _).ltr h11
+ done
+ doneHere, finally, is the proof of Theorem_7_5_1:
theorem Theorem_7_5_1 (p q n e d k m c : Nat)
(p_prime : prime p) (q_prime : prime q) (p_ne_q : p ≠ q)
diff --git a/docs/Chap8.html b/docs/Chap8.html
index 34aaa63..09a0301 100644
--- a/docs/Chap8.html
+++ b/docs/Chap8.html
@@ -237,7 +237,7 @@ In This Chapter
$$
\newcommand{\setmin}{\mathbin{\backslash}}
-\newcommand{\symmdiff}{\bigtriangleup}
+\newcommand{\symmdiff}{\mathbin{∆}}
$$
@@ -804,7 +804,7 @@ 8.1. Equinumerous Sets show ∃ (n : Nat), R n x from fcnl_exists h3.right.right h4
done
done
For the proof of 2 → 3, suppose we have A : Set U and S : Rel Nat U, and the statement fcnl_onto_from_nat S A is true. We need to come up with a relation R : Rel U Nat for which we can prove fcnl_one_one_to_nat R A. You might be tempted to try R = invRel S, but there is a problem with this choice: if x ∈ A, there might be multiple natural numbers n such that S n x holds, but we must make sure that there is only one n for which R x n holds. Our solution to this problem will be to define R x n to mean that n is the smallest natural number for which S n x holds. (The proof in HTPI uses a similar idea.) The well ordering principle guarantees that there always is such a smallest element.
For the proof of 2 → 3, suppose we have A : Set U and S : Rel Nat U, and the statement fcnl_onto_from_nat S A is true. We need to come up with a relation R : Rel U Nat for which we can prove fcnl_one_one_to_nat R A. You might be tempted to try R = invRel S, but there is a problem with this choice: if x ∈ A, there might be multiple natural numbers n such that S n x holds, but we must make sure that there is only one n for which R x n holds. Our solution to this problem will be to define R x n to mean that n is the smallest natural number for which S n x holds. (The proof in HTPI uses a similar idea.) The well-ordering principle guarantees that there always is such a smallest element.
def least_rel_to {U : Type} (S : Rel Nat U) (x : U) (n : Nat) : Prop :=
S n x ∧ ∀ (m : Nat), S m x → n ≤ m
@@ -965,7 +965,7 @@ 8.1. Equinumerous Sets have h3 : fzn q1.num = fzn q2.num ∧ q1.den = q2.den :=
Prod.mk.inj h2
have h4 : q1.num = q2.num := fzn_one_one _ _ h3.left
- show q1 = q2 from Rat.ext q1 q2 h4 h3.right
+ show q1 = q2 from Rat.ext h4 h3.right
done
lemma image_fqn_unbdd :
diff --git a/docs/How-To-Prove-It-With-Lean.pdf b/docs/How-To-Prove-It-With-Lean.pdf
index 39381a6d8d13d1097044d0fa7040d0a58c59070d..b36c75519330bc1b0eabb7054451c988c9a7a18e 100644
GIT binary patch
delta 952112
zcmY(}Q)4Asv?bu!wr$(CwPU+tTRXPRifuco*fuM+?YgJ?zH~o)>o1Ho=a|*Kv7qID
zV?i4R!GJt096~~Hu5KL;@ci-J
z7e(LyB;WDWN+`A_ixnM0eZl3MBxjxCPn>!1eu#$ud<(PU-2HpMd&&_0-1ztXZkaDE
zfb{nt1=OB`t;*1$1xj$C+R%WEWhVjAT)(hW-8Jy+4=|c~R@5av-4*sw)aJULZhuaJ
zhy4dZ=^XC&w?ETY9g!{0Kd&!~w|i$rl!2^6B?U;-L6)>*l>mpCrOZWhZza`qhwXQ-
z3Ld~ZvX=n~Cm{$z^Wev4sWE{8k!bEKP1N_}{$^Kp+Gc0U+O>zo$opd&SR
zAr+AKZ;3y&drZqSZEwMz8x|*q$&qbo3Lp6WIpOniO7bxIGlWDzYhHHW2y;@
z-UMN*#wqAxhjpceO`!x$nWN=|hoy|h{F`1+#~WOD^vW^Ht5WW|L6Hw{I4^fna&x>>
z_|e8aqK3%=&+~k+yZJE=iM%X0KpQaEdbPT
zp#n&w8J`>)3UG_8xWfcZ3>XKQeJJY58qwlxReDkcScSHZW|LoW0l?JQrwY?^p(B`L
zDRr?dePS_g81A_TV5Ou^C1#z#+ZUrrjob^f3)4xbNLGxB@HOSLUp%}~HX6ajeQ*Do6
zH+w^g!1MD$>YgNJJKdCCdDF6w@#|v;7@Ule8(CsK-#RS2cE^t^!5AlVJ$^Mm`okfN40vHl~902t+<&tJy_PwIuw3u6Tsq
zkGF3t2`8JiT(2_&Zd>kAev#cRll`vY1ZDSvvb@k+eEAU0Nx_vEw6ZP0B85#_Rfg|_
zX&NJa1%B~dtz)1D-Z_9a1*nujNPHPzgLo?FNJ#ht*bOwK<-S-~FZoky_eFGhyQlVk
z>)q+{os~h5xv*Y8-wtxKdQ=`au;uNBe+H5w^cNGu-XQxXceSiZT}aCY4;lf~m+^(M
zxjk?N0mo82RjLjLdSO7W%QIqS*@%QHa-R&_Y3NqOqV4bCzd&&)Dc~#pqhi>GW~=cP
zV+%7JKHwXP?d6;FQDH~QQ`B;2c$*l0!M4fwcLsP>Sm-9!rV1E(^LSaA7a3XHv@oTw
zYtD96#QeKl=osxl_)QuI(X!xz`%xXaoR>z;x%&I!zCE}X-s550&I3=hhoF}e9MNA%%_Svr(hc0XJ4)Pr3Jrx8AZ*LgXV_`+us@0%Y9-Q
zZKXZiOHSi4`zTt=
zxd&fxvOgHBD!3fq4*n9S*|D|UHB6zP|~)z#>Rq+ZZ&a5upO*7jZ`z6+6ml
zzwUz*JtZphJIQmlY`Buw68S6oY_CC70`Cztht78lA
zYLzjGz#L%5;6*DaJz>hf7Jsjt!QcVa1KTZ$(>3t1tZ?`=u&~?fDknClyxUABpmLJf
zz8b$@HC@w~sS-Hxy4X&W;&ZNGBvnmR1!OY(QXdkS*b6rE!dlqE*A!
zBFV0J6-pn_uG$rFH&5~k5L3FP6j11*8v0!8|IS7JA%!L@yR>)P*5$LR#9{tU*~d&F
zDWkoWwdKe28KdpzCA|DrUEu28UwW+qeiw*TlF_n~m%@CR?AnqB_G3?ER=z;Ay#E(@^JokrDX
zAA4%`%==gM^rXl}Q+oBR5mW^_4-eJC?Nmv>M@=ua<_1t|LoGm*e{F4b#ah>AT#(i>
z#XS^xYb#7prH7|CT*ZCC|08;gj2CAGGSMk|=)hhh8i3l04hXv((t@BQhaUHJ1r
z7|7TM^!Xj|B{?qZbkc#o^k{*m#8&4FWALNypU2tLA_ew*4Ms|txKeE~op3267f2mH`ur=I
z9t&S^r*!g!@vH_QOMFkhD{etY5oB}7Z^%(BhNb-XQ7MjE){PgkUu53rLbR|f*V9W8NOfl8VSyiwK)tk5
zJvk|~JmG)Qu!MMf+{@r@_g0mje55V^}3c=^U*
zYdiC%zaZu1UW2>*o+|}>bU7cpqDsF}MVSaq2aohYLSsP{<5JR><i(de#L?TV8$*z^x?GT(5Snw2
zEb0LseQgqeKZRg~RiY6uv`L)`wPc9KfQS;0)t{1z|8v!*O`@}>A{&hM63Ny#BYRNS
zk|o8-;_-cv52c967WJ&r@$UM}UQOOV*AqunxDC(MWW(0Df!JAF+p3Etg5zb9kKelfqEXqT0V!x2L^)BN>s42
zl$6L!%5mJ&+;PTbe%0&ap1~tLTlR!@rSP^h90SgAV(y%dd(FR>ys6xXH(-Hnc&`tn
zC!|rtpM+4M#3`jm)8d#D9ZJ4cOAN(Sx~Q?D
z->QGRIQY3K!JfP7T{syG`0jS2|B3*9y|Om!P;5)B5vuD9r3O(}4R5$b<*(&7r9+ap
zz~{a$&}@Kb@SmXu(8?2Z@321BEeU;_OQufPQz9nAQ;8tZTuv~S3afc*)NXbg4tLZz
z&oj3&*!uI^UK2TumADqub?bTfki#A*nNG6m
zmoloeDQ5ax)*Qxqs!}~KX7v%&7R~=zo#tE#3Fmr1x!Ye!lc8mrxv3#zD5t5+|pfR1j##|TWZ
zu|JpFY!RSK(&{LboAd%=H%~=AAIAgyy=A*pQ2}~osnJSmF@2Pf${W4ISl_p#H2Gvb
zPv$;Z)cybg%rcl+$s2%ua~tM^H3mjqh4&50WY$QaiuyDr(17%#?NR41t9{z_chMZ$Lh1`${}04}ApZmPAL#$U{0H_waQ}h-
z55j*C|AX`&(=Y6u}5
z>d
zf3e2mgxgpr`vgsjDRhO(=M9g4=h~(yuwhkg4!@Ss3K$1K4jQYBGs7j1n~B;S?+&zN
zO+?z|ourHXUOODS8M?2sXm2|R((^SghC}HBSMH=B+PnG$2iaiD9bFvaP4v(1W&4#4
zZ`aSC)Ep#zw6k~VmsPymF^0l?aE!y32-@MhuI-QuKn3TeYWU^!3#vmV
zB97x77x+yUn-w-1x%MQodo?X+w!3b^6xm3KuCHdCv#6j;6ReksNCTloi5n}J5F2fY
znp{DGZ?dZaD-{%_Xt55!O>^~FfLW?510OChEzzWh_rirJ*Mb4_`Xsqa0r}#XNblnM
zfu;bobiu4?uX=oNYYCoVH^jF%th@7{^zQ&KX@V@iDd^27h
z>NOA_6~TPIaKFS6?bE)vcM;KMi3-}Kgw^I~gA943Fh3}>#v69-8F|%b+4Dh2d$V22
zCi{6864k(KnTr1v(fOSY53B_dSDj%r%uUq!2aG}
zbn;|sv0)$-G4d6prZ=BWD#@4Vyd%H_G`iEA#x{X@q_tYUQ;erh9_x8aIRS^v)PcmY@pD7abe5;F@^Il)nGD_-Dor9d8V%0U
z+$@%g9NX9K&oO^9eLUS@2NWXTW;9yCqqh&;qej4ivG8Une4z>ewWr7%H=ZqfwYMB|
zHYvUUdh>Vr+lGCA>XGl>zjl6pu9seh5^R>#yy|ye&f91yYh1SgEM#)c{#`$Q$%}Mv
z`lU~>LTYm5zw={5p+BJD??jBw3Rm7ub`kLXcoyg!#*DaRtc??V1_b;4KCC}K%aich
zX=#%cs>-D*N%WeCBY$z*StA(F@S(mvf0b_Cl#s|BK=NGubjeK(-DWc6cf+
z=W*0pPZgqH47F*IUy$JMeYD)J&%v*uv1GfeAV0Y8E@O!+nk3=?gkFReq(K~HG_s!=
z`T>}%(a_Yf)4ePSeP=4yuPgIH?gj=^I<%+CJ-j2r;7B2$raE5=?z7x91)CySu?7f1
zvyyp{)#EErGEZQHgPWOg|e0~Kz*?GMlO!7AuV`r;|C@2JmdPyRL9_KAP}nfACzF=
zKEFMbEd_yZ+mP4Uf=dlYfi%C~YzbZ9v$_72L7MzX+asK~B$6}n7OU{U&@TOUBm6}!
zG+`pr_#Uk6l2Y}Boo^9Tx9HyMHPx*c>v@yBy!#_iq9YE0_ZG2@P_aa!-YF-14Wlh)
zZBV@08^{}M;Yh+AQnMy*E-#By3Ku~)^yC%ppOkA3IKr{PI7e(m
zta}F1A5>znj$Fg?V6;tgR{U~%XwFk<(I$k5W&>OWYq;kN#cQp2FBt(yiTII^OI56K
zA>tMRC=fxru)$AHN+_{|qLU*P^U#;-iA}$#9C*O*(zxLwMqXDVxAG}`s%xL_Lu;Z*
zp40VuqdxlZZ5P5iG&R;X)Fh+e8SIKiZ!SBpcYBk)J%%+OrFnpdQg?%^;8}aOcG!
za8;5zW7f-=gH+g6|M!*Eyy^0d6U5WBq<5NBrD9t+lY?HOp(MIPNx5h3yt(?&8JX5{
z1X?1R;_sixhKjI+GU_Wu=Vr9Hhd*h7Xs|%DUBbWdPOGqv*9h)v2LOIO&lamazfm2-
zn2?&>NIE3B`^}n$(e_3@ayRwfYX%mvK(-4I(sJ%n6>VKHj7kk}Xr5H4x@_#5q6N4T
zO|tNT1A|sCcI_V6p^w3XF=GV7rU`Ic5cXb~K0t4)v=
zTNi8hO|SP){QjNX?q^^F%y!qr^&9x$9|@_ymiEu~rLzns5=IFOpNMn55g<-m#=7XB
zmM(P!>SaQI)F?$oOg_E|>b7|Gd!2wC{q}<;XKlhEp~xnmi_F$6TFu{G
z->#oLJ>a7A^RDG?0VBLJ5&n970hF-#2XAnU*M>oeq#Z#`ZOec*JJ{g8c72y%Z1`5E
zizy-hY)s9V(d^?)3#pQH=pd~VA?#aXcmu#bG9-ssSBh2^H{JG+4A0s}!4vRA$V44L
z+>+>453qP*BVG3VEP!bD5Hy1ZGy_@ru_I34PVF7$rZsxgejK92IMNgUboc{EdjHY~
zzp(Y%&&{9Uo548l2WP;WgSof!*$h-2o{0HW2=et87ap`to5Ru)U4lqM^3!k0ad+B^
zP2J$pdzy)!p4qdPFvwxn1Jrgs^lTYx&x{@QlF^-^(<6@ih3dw$z%h6K8-~
zdQQ_@bE=^8wsBrmDGyR}I#%`TBDY_(SFWvm)$>h|H<
z%=--{0|IRclQAO=4S}9!n-VXy`RiN^)NzwKQBVq-%oO3
z_OA8z2{g~)U1I|O+6Vs4cLe(LigPvk|0w%r#uM8lnTC?RB5z}N{rf%~>UrRwr?qQJ
zjHSaQ9dn))O9x;#F9UZ-Mk?)4;$iRq=~GU^VNOdCE*wL;?WVntG52RA>rZ_}hb1@A
zKh-v#Y0VdA<|Kb$>Wgvgabv!1)BCsAyCyN;8x4@I@#r(59|A+geaLH<)TY)Dw6a~n
zUPHW6o3Tq%=ztdQ)x-n#7*+&qYPR4MYi_^l2=+9fa;e^0Qq;MY9qXSIH@pl?eC4xA
z;ViBq8O_9Cizw#KQJK_+xvrDjJyUB{lh;U308mi)C?PiSUCvr0ZD4nq+!WF}
zn*(4t+yzZ-tOuzRP-B)D(Se-c+cAloFRZr9L<4H;`j@R#T(Yh=wQBdwph~UNS}nTL
zucaxDP2;v?zy96N>Noc=2G?EUBB$FL3JNwuSUBo9-AJ$tBwNMX}JL4u{LcZHD;@bxT
zgB0$|%66XB>6t0p%i@KK3P~qa#yYE8odCzAe#v>@eDGDNNn4?j<
z9Q4*8Ke#2;zF=q|u0~@h%+B-OjXJ=@Tvo4->Anq_!BCIXKge^Y99dfNQ5#EX@QCY~
zx89Wew$<5$lV3alt`u!%X+CV@nzw7|49K#fSx(w{Md!Lk>CXM^UXnS+RC|NB{INJQ
zmfk7-FlxzJ_*#xq-@WLc6-u)*#qY&~km%=g7^-f~ITS7q^bU`^)wZ%Ah&Z!czoVUL
z*q>K`b>R@f@p?06wFBrr!l07y_H1{uN_ZLZ|4wLX0c5Bm+yIKf97ejLZd^k)fX2t7
zB7LU13LbN21R-H^sP=6tGX83j{OI3(A2s|j`=_cbpSn0LoIQrtY^giE$o*OwGU=AT
zz1ecC1zlN+sW)44pzIJJ|9i?g
z9Av2A-URVrYyvcKu{Jdxd{euwCWLZ-D2cy+S6RPem;W;&+tV(vX;Su+@ehnN_O0xH
zKkf7|Xoo1E92v;CXw*P>Kb%@A->8sv-lJD>&Bk%EoSp2A*lUP^8cnpEgeud<-R1MK
z6rswea%K7w;KkE>#MAZG(?^r{zr*sS2*(y)>sATO=kulSk`RMbcIt*0ji0CUm$eu*
z&GNNtSh0^QGauU0+yK6zY`neScn;^^a>$HF5j=Z#v9#hYo*zI^9kd?JAkNM34u6MRxM0~1
z{j^R&awpXNu;E(l+J>}4lL9uO*oa{6
zK;4JzajGCg?;wrjYVqbc=8CGObFJSAI<(Dyz}5HJ^M|N}-UJ|fCC1f`#?XHY2?Uf&
z#Nlk88{97)Xe0?}K^L8ntox-1eY9u-efkYmwT=FdM56Itjus&-)f3{$w1TlYi
zl4B?tXruvBAZ)6C9&(fTGXNpm|8b|{UUE2R-wX-&ZU4J_*P&kS|7sSD{X{m2B85ny
zP5Y=l=obd^w|%7+=-ahmDeYl5pbnl#0PLqA{%xH%quBnS
z&IujPb(UuhWeut_YM5NNmUv+^V?3%$l&9YLg
z*4O|!pKNvmy-Upg#PdPvdAP+A{NVy?Ey!MZ&@)WV5EqP7PX28VhdD6y{d8JHv4W0|
zd`t`GlEQ92@7n*oXqQ$~T^a{SW0)E6U??oh!IWa`wU=5gXzj|Hj@2NTutlE8fr&PQ
zmS=nfEOuKqL{+U|$vY0$;?xsfifadZ*!2J{SMzi_Vidmypd27|ES3;q;aVVWcw3u-
z>c7Hfs)M*2i1m1^l4;q@-gORhOa)kP-%Nj=`XmcEH&dp2I+!PgP4&T!4ZRwRRfYBk;>7RwC+H-?Zuv2He$FEDsGay;?piVz9(T1b-OU3Xl=Ny-gaXxnFFV-5B-5)
zvgo%RP4S(J)7NhpZ3fp?#isCL&h_6Yc)OX;9>YGYys2@|+I&J(V(XDvuvS?r8~=_3
zr}G~xjXkdY7FXmdTSCrAq4#~BjcYImRZ2Imt|$ds1Mu<9iJ0#~XEe9**ps=}_j!Yi
z73=)xEgq`ss6;5LN3?gMK#GK#P4s|C@gUBb8kV5F&g&2vqZiQw>mTFb4m{vk6?
z--#iGhsHCT3vD3CwqyXAysrzk_+oC{C<_`vHT6nEw`5}3vw
zxyD%X>OX(sDS8wgXSl?>Gp}Zz6%Vpwi3PmYSRYj4dI%Hw4HJ-&&QL_nK}nAK)hEa2
z>{h?Pv++G{Y7KLnI1|8|zh8Qry3`a{#(XB0(v;wo6cpo^K_Qp7B|Dt49u7c(fEM8Dzuo9Y?{8-
zyjNExGrQ)@d!{^S7OXd!K^Al;zx;XKcw?1g9f%3S
zJJvn0s{DqIC4TP>aaR+h#>>Ulu>-R0eT*|a=(pTqNtb2$up!rO$&O``JrnC$JD;I;
zZ_wOObgX?Ty_3A$_Bt{uh|vUqVKIVEU4?qZ^#F88b{
zczR5G56id1YCq2ru9{{60QOY00+i{H+V$Y*2vd;f8D|98nsr!g=9wiN8=eGRmQ&cN
zLAwo<5p7n?JBkLol{Nk13||s78hrW#v{Fy%BToi3+!0e!?VZ9CnCTAMN({`^_KZFf
zG$ObY@!KihdhFA`2N@?MXxd~K35C`zx3h?1!4?qQn!@Y>+PU~mAKiY|TJ0;xWKPr1
z)EUO4XevNbIoQ^}x=syp8%QUevtb1p1*`4zNhRij`!F%}bj_JW4JDukvE9OXV5Q8fMortI4DWRt{}RvcRyKg3%X8`vcm1I+^%^e?OhVLEz^tkW&mELH-}wpge+idF
zI8FJ@4~2S%{gp3;;8%jx#7D!oy8l=}N^xm+z)OKCP6@V6m(6T1v(;Llrs
z|2bq@#~^rVukMXqcN@OSG4D#_`1vn{H99x?a$@iHF>R##bY&?9)_T~ZcAoG#sO_$+
zxqD>g$a_`0@9kKy!$VuA-WB#-=6Z7LhVK$~UT)C1KhmgylW_dw*|OFL|KJSWDw;BY09(*$NLov^!BiZRZU%ZRDYn%d;iY*0Eqn8$~1SSQAO=^ELd7
zEHp?YQBR_)Q(g{`RbFR#3v4~fKh$Ya2b2DbsPU)S)xO?fWz@|PfzZsdWtVg6Sef)w
ziB!?yv7N>OAyjqr=oBWrUmn5RtwZ5}n;;;hqtXIid~tF$;L~Ck#tEwMbf24qC07l2
zqeZ^vj(yD|xdN6}HX997f)L@AII+2+DpLAik6hL3s_^S`&AYOW3ho}D2;-7E=#9(j
zVlXfpZV=7m0bo2G#cS53Iy*WB!_)e>wT~Y4;=UlRMY?gq`DMYmH=BwO9HowKBJQ_B
zdbHb-S9mQ|j|+#*OK(Oh6D!xVi>nEA<<1o2+)q0Q@`*QHK6{It(69SDAkSdXB{pW=
z!w|`1sD%%nbAXk*FEfL2Zx@R6TvR<}
zx@vh5gVFil2b-pL`SO)%<4PUB3o>49n04Bl0`tP`;=i2UBEOBKuNq1##wB&}!#`a3
z-Nu~tEWOn2n$7XkS~V9eVi<*fQJhN{*O$q-mE{UgUg&&t&Y4bqcBF1kn3xzHCMD;q0cF#Ef>U@c&&BKLQw1=hI`gPr21;i!0
zUY=j7N-ndWtK0Oqkwm9Jh2+XcFJn-skLE4;Q!dgm$*wk-&Z^0Z`K}Vh7DKdu3J9=r
z^!Dr8iW}M+(7$5pI0<-FmqK$4#A+p1lwIjCD4%kOaF_}+vjAGmYRjoMBSVAQ
zogK=E%sgOq53rZGcr(9;_w`3wCvr5b7?LOv2}+%IO|~ffv8*D;vuDNt&b~
z+hdwt(S|ODQHAtPiip^{XIqyS@*5H#H28_J$Fq+4jFSx|E0C8q7yGj@)hmV#%RpN_
zVJ09F8wxU_dg|+o4$yUZt9nKjGy)}
zksYc{?p{rmx;!K@i0R?#6ElW5#)q!hnibHc==-u$X6NjHg55E-N(uiFeO$``eXV)q
zmE{|zh7ZJ^t*L4#3MhPKWlJI&fsMbXJMXOUfm7?^;r_!jd*2P!=h2tP?gn+EbFVsf
z2>jTt3ZJmR1T)*pZclc@Fu}K^guXH*Dc2E1a-$GSU4#hbMQ>M_JrqxxxE)l1U0qwul-LoS!>0f0dlr@tVrwX=
z6NZ+5+Vsi(csUI-Y^Pm1_d5Kp{pu}!z~_!n?o&pBf4vbf!$Z#XJLY>iNaE>}56A!G
z%p3gKIkRyx*`By3geW@0_DmR2MY%p*$VL4<6fXJKQ`mNH@Qq2>f4?H{%NgWFRR^l+
zsl>|AjJJm1+*mt*qjP_+phMghyNrTRC@8IGa72`~j|;P#GZ)pTWQXZjkGiW!ugxZn
ze)v~!n2uD5O2KxEt(HL;UEqwt=LXU%w)Ntw&*5WX!#OxTjY!sGTK~iIJ@-GTL*Osw
z|DCwgY0<(#fwm(_Wt30%L-mqjf$6YONkp77pb8s;XPKOleR73{BGM3yEg53@%#tHZCqX+u1jRDC|OJW$P5*|3!a>i0y?NYhsEoS9MHT980j+*^{$?p;6BH@mca=$3ARuGQ8`P|GiJhl~Qx_BcmD=X?KtQq>w!$(>qDS`Ejn@52=dcIT3Ai<-i*Z%vn&>4m})X{FI=It%B=VRh_CLg76LU5vw*&M?RRtVG3Hh+B6&pJ@F#mP
z$WCnirRtk$&Ee_QZ(B0bm=QI}X0q35mU!Nw9?$P+0UCJ5OwDAaf4n
zZ?QuGa$1`8g*@vL7*D8GS7T*5F&WcuC+{bDETZZZ{H8&*_nqKe)O0IyaRNkn1-|x2
z;aOb0Cm40;?_gw5(_E=Z@L4M6n!%)4!W%6FdYLjfNp|vUR4Ig}cdKn!A}-T)gdEFJlMQ}$P=wpc(E
zfc}E7{S(8E&DvwJz+vL|@0kN(1^7URbJ&c`9^AnJ~1G(H-*WMu*_(5@WpbwH`azamD
zIXDulajN=Q+W@<8%Kp|eNC&T}i))8dx;VBEQGSoc+*HXIn#V9C%o3YLouoI;gO-8d
zZ$Lu4O&8iT&5*m~i*0lW(83U%
z+Us32X^0Rhv_3~{Y6fEun3fbJc!n@jqgW8u-c)TMs=c=@%2Sw27&zrxz9UK1`(T2q
zIsfA>oJJcOu$Of^mB|VyxaU>m4pHMiMboCy8N3{>>S44F_w(y6jOF#pGR4fAy!1eM
zSnLdm@sp_p=X7&ZuGU_sO>DMlY3DYx(!Iaf(kGM^=t{tunrZq02JPg7qabrS1_%(a
z&nK5SUb6@KDbC_s1|<^|h+C4jj2nay8~1W@h_xx`9PaBam`EH85x%PTx7ck_h5g_?ly4
zy>FvwFmj4@zP-m6nuGTg8FfJh<}Oz{L>DGToL`bhP5lcy7>9Yu*P
z{4sTj4`-CSQO#ct+Nr;uvfoy-vfeB{pC)!G0s^-EFH?+wFDA?9{_(D}{dKq5yQN9w
zykjhG8P{TLeD0Pum1`}brP1&h!&lE#WT@WPX
z9PRp5Blk)-U3mdc&!3m`=i52&;IxAVogQrlxN63Vj8&|l^-o7J2lJ{jN%?(33N%v6
z8>K#Kp8lG^mE#5Vnc_-reoD+*EvvRBVKW$Ug6k%m`JVUWe2maluGmgVA|5NwM#x7`
zMz$I1GPje|y#<5d@)Ioneh_I|EV%_`))7(RhO2x<*<7a2Q;YcdeHL%`X(3zAE(T83
zjdI?ZEG_Yi9`U?^hjc^vE>uq-{Kc)FhiMDBa0@-@@Ed*?8lH+#
zHTEHL=*#U|+`gI9i=MlgABD6~8zH&aJVdwuN&rH@=(?XOKeT2q`rY|)ySu84g$L$0
z$T0Mis*KqSiDJL=U-oMNCMf>hk4BpF((mC+@fn3NhvfX6NGoHX
zdYpfN%A11vg$I3t&7rU!?86#@YmyEmJL+iTdo7aZFLX4zdnBoJJh!*Uj
z{SM-l4Oe4(y$Yt!bGvM5chuP2ZP#fw%dSLb15@26A`neHN|FVlBqzJ+!}tVG@|=%Y
zZm+7u)%EnJB@l-4a$V_PRhvxd4tWK!uEQ^Y6(N}&;fj}RM;O*jTo3#Lod82Ui5jK9
z34wd$;0rx9^qyql8nSH!tN`Z=)q#cfa%N{8^4DoLf3Njz?$&YFT#O2h!x&HL5c0hJed5BbL?zHu>be+DIW7n^6r-x=J6g
zKfOjAVubKE@+i^Hi%LeDLBn=R`vl!%0lTai^p#FQ5(le~Q(vnc`VYvf%k&msVfDoF
z3d*HT5q1bE`+6wjp(F^(OuV*4Rkz*n2z?
zGjbP(LXM<-4FiX
z(JB0IcFzZybDoh3*#NNQqYhbVy?JNXoY>|E(pEWUd3Y!x&57Ug&@jgN3eHs?HoHuO
z8b_;|>~A}=uVtV0Og-|P#6?ulCUlhibn%=mT^tF3l-{IN61bUk^S^Sn*(^pt*%Z6z
z8mN+|uE-A4>fp20o(cMKSslG>a(cp}buiXaYokJXze&{oLD_}g)zOq5d)-g%_yKjj
z<6AoN%b6K2^0}>87IDEA+*-iA9OTVJ9>d$Lx?@zt9>u@^+ORyuGyWUX1f#Xi&<=uX
zxpRkVIXc&2ONVqS(1Y(2#MM3E8r84-;0aFBVBO^tIgRoGPwi7DZb$KGN)OENn?yC7Mn*oFB1=aGg8oY`G3pMEz&8fVux@>JZudV|)oB|T;-;v8^$zrPyT{V@F
zNdj0U{sZ&?{$@w_Q3M0l%Powa&iZ{V0T+{f4Q{opy3%pCS_!~A=;;$s^)fMt7%wGy
zjb@0c*I*2RGc2%f_^!{)eI3fSik3r`O(YG8!tscSn2%N47`a+K+_0_evXU&aTy;rF
zk^RnRijJp}rHw4aTMt?(>Kz(+wT2CPWotobj$lmFZVKC@ancTU{~L7H^12sw8jpiXp+dl#eeSIiEgjvjRMJoN=rsXt>)_hX_BSg1yw>V=FJ
zRSDZ3EL$ra@n8fu>@aWNBJ-dN24^@J^H_Et4y2=UqC?z@uf~@sGcEnfAd<=;RI|4)
zHW*&b2l-Ox3x0s(t(pfcfJ*2QC-^@hyEx3%Wy!i$zO&C+mz%a2-Dv^NXRJ%QmVET^
zHrT7D`-)7A($ILP7fj)1MS4;EFWo29*UzN9J@_l;faI95nClFo&fFq~IX3NOk$EEl
zI6MoKH@v4imttSLwzow-Si>0_@Se7~jkQq!_Gj3S2hX~JsITnab&Xqdk%)1}S$UNc|M?)0
zelKqTp+#T`e?_V7hVVyPZGJC}(4>4DKA@D)q_^lw9_w9zyq9K}F!n=CD*UtZdgEpB
zp(4um+}jNe&S!)Imb3DXkP7u%J76_S^3LApL(CxvzkWwG)SgDDlg+|W?v&8o5Va=t
zitm(KouHP{vt<17*i8F5Oeq}%N&~N(oq@iCZ^Vys=&t}Jp=G!*`aFwv87e%ah{YK6
zZrRFs!#M5VXGX+^)u6!;d6PYG>t>1Nw_V|x$9Ls_;O8qq$NxL|Wq|Rb(SmYkkObji
z0hd{M-E?lHS#Tgg(ZKucd)og*TwhxoU6FVoy?+);s1~VL-Tcn_t>YNGv2m^`iy^B@
zLFr$0oFT~s7I1Wc`Gr1pn!mr*e)oBJa%&{a^!Ll)LNb~&nkFORR1&Hgt{U4ylYIN(
z{%H=HG&c0_QZd}!hU6QjnD)Du3K85gt|6S#-D@OroE)-iNXTjzhwRFI&b^pb1-bAk
zpRnJT!~52l0oLme7i+10TVJ0cnzruZl@&S-sTIg}A@N9=y507e7$&*0c^xF(N2oKh$&(bmRY>kgAB)de{v7{=>
z`^N~Q7FSZlxUCv}@lr|d>o4O1L&Y^bEdat2E*
zY%i~%%*CL4xRnJ++HH9&YgkLV>P`$by0~cd{b>x9RIzBahh}@asU2?jlT}qay%ZNc
zTS^hq0voBIHDLA{HIteF@a)EmQGa{H_N&^j1Bc5Vn-gC4lElj=I@`Y>iLf=5WGD3PSFa->FBlx
zb2QyiR#xCuC8Jxb+%{W=iffvvcm|K-&6z;gqJ@PkJv)z*pyEQ*#>y~P)RHYuYiX$l
z-(qdg?YxxzePLHk9ex<8YS{ulu|kbtK2uJ~iu*!=vO@pOQbLo_#T*RD`-H6(R=v22
zpudt#v^4Q*5J+|b+z7PkKHoF0Hh2_k6A+{diRLkf*7+}m;B=IpE90t7kpbmR>7jSw
z@I@TB5L%e33s!fXqaI@6W$PS<(AS#uh`K?HL&J>xdM&NUsr1<1HHXnlBl>w1zeK>Z
zE{~G~A5K9hOY<-~BRG)Nb_95L{&?3V@sNwlwE7rUwYg3JfBqbgWmit8oja7`m3MPm
zC~=Ke(my3q_}CRu3VL-d2=ct(>h}xZ
zGYGs&`+2C@j94gp87pH7U|X12&TB^@f2gl$aar>S2W+(5f-4BE-dv3OlhG
z?7c^eTZ(^TOd=l|yheWgqROgm+bq5SjL@moZN?EjxSF#98YP-Mmd8TaX6$k)+tLnH
z7R{*!Qw=%}4*fOoeK468D%Uw|o~gK@{sx7{n?{bJJNDhf>Dp_Lepj)r`MASdZu)`Q
zwC(`!HZAfl03^~vPvVakP1@2PENP|bQJ2n6{{v(|o4@h-e(J6_d5)Tra5TP0UP>h`
z!)l`d_R#_-OiQf{IcULVgE3vMXUEW4e_H)fK7`bAO54<7ntQ4%AH#Ek
zwt|H3nD>Zbn$+BJ^ef6j1Vt@rI(Q7YGn^^4)+-4tcJPOx0O
zwxJSSqh_~sPGnF)TmnV^}dA;b%sP
zl&%^+e+V8UTWQqkBqU#wBDEuTiAAkKY-E6z@~kh+bRp)slRTR$DNRBlr#iZ2x}jv_
zbjvn`+c{lYT1Kn#mbn&P5-^*Ht|+d$-au=5S|Rm@>1z0)u`Cva-dxQVT%T!s?U#j4
zO{83vOk0~uuGX97=OyiLc-KmPTE1UCT-Xy+m$E++Ie$2@F7L6~pLUmh(zvwd<%chf
zsW&=u`kKW4LWfQ+tl*#D>B#BMbQ=5k;-^lWp}QVCF~YAs
zcT%v3cG3PH9XwqhA*IzSwoFM;Ocvj0d}0cOy?$j%hgNW{L}6p(wzjcefw)p`!?GN6@(HWp
zhJyBew`PszQZ5J;jO&s??ad0g+zqTkTQ4^0pnp+2iK>U}+=ad?zq)XNJ9w^m1DMRv
zz}&zav^1N6zhP~%$zGccMGdNYkL-2Q>zj;6NnRlY=`hV**PsmiZ)B25%7B^}3u`pfJaeiHL*^NvF6DRARPrUMnNEt2
zeSZgiCU!BEyo+oOV?T!Kk`lfs&4kZU^#oBCn|5b*vdXuS$;UNHE>je*lZg@JGVSNO
zFY0cXAgMPcPVRq
z{4IMx)b7+Dwg(0KQA(>ZHHEbLStw=n?RhyxJ8Q~5I3UD
zE>p741%I@oliZO!JI<6kb2vc{3)zfM+)ZW=QU}nkn{18_`6RGs+5Rqm;{uiEx9snR
z?QsgH@9MV%Oz{ux+%%oAVQbp$PvLVM3F$PlSFd9S{Pt){yg7>g;IO|q*icMy=Py59cYtS|@l%lYyG=&=YR2*e4E1_l(
z$=WrTHu2fG%)o)L`qVJ%0y>(WjP)E;{1>XNpycYwuW4{BJS6Q7
z?((go6V``Egb^Z+7@
z7J5)J9nSUVzC0d;hsk^y76q$pxd_k5$7BnV7V!+<@C
z@E)3GPThnV8!qN;SkZFZsejo>KPF>aSQbZn;n9DGR+?hKsBVV^s|Va8P;2U=Ahl#R
zjbZ!Iii#nc>NKoInCmk&C_bSM&IJl0=@ZZOM;|NKXgW_w>e>$4uGf>hUQcpNPQi*5
zWS$Xu19m`miN_uueQKChO6ZmMUCPzWraauEtV-+64{#f7lR(hr**r~0c$|uEfP7O@-lwlb>{gcPW~g^FcB`&^cN^o_6k2S4
zg;mlpq79#EHc(Xi!1yOPzckF65I;wC8#uP&#-+WaGF5@08&Hqbmw*}4?gBF;1vun(
z
zQ(OC^FwFWrr1f_+dbW>pYWrV$v)`bndjf`CTGXxHj%UQD7Y1?YN7tQ;+3kWvBXQC%
z>W4(VO{qjmb$^>CX4=)bC6eKMs$5&V`ECnn*~YeLx4P~HCgey)q=<|b!Sd6m*}$6E
zC&hM-DG%&oTT?R!dl$vGTRr8fnq5OW&)(d2>TdeP&MgKpfP=fMnqiYH2l<@4NI|p_
znl4Ziu)@9K%8=tsqCk?VuY&QB?Qugj$k~=@F5SeK+~E+vFhguaxsnZtKyFd~sU_W*_)V6a
z2PGrqF@I*f?{qBQ`OJ2~j~q?hE`-l7rA!@azNoOdwx`uaz_XrSoL6JA+wpM=#@Py+
zc263_xfEPOINOBjG3J>F=hj;RICs5m@y)e9!JDseN9g9ByIaxCHh_x_@jcPatjpgH
z%$G6sM(F0RN$lSPy7|uIaYuBsHSod6H$^vZ`hWP+=;n^0d!m~;;n$*@tu=Xof0yWH
zF8m(4`8n`i>r&bCGPV~2sco>U_3rgZ>Q@sgQ0mvyDOl=@gq}4T#T~vin0i0r+yJI-
zxfEfkuO&wWH|n#a7eT36=LJc*d!2jYe5+5
zYkzDKgnGz`uR*9;M~I-_;|u}RwR*)*U*oI5rw6uP1E01)(%bjNPqRLMJ5XZA)LS8_
zzb3hV9~kPpj>x-!sIB&^6yfba)Vzat22oopR!6TLya$My6Z}FTY73zxEoAQoqUHqO
z0YptRWJFPKRk+{XD^S$?-s#%QEjxI11b@+@gA9wULY;zSfZhy!%5VG2TW^pq`G|jA
zdK;k0rw>o;^%C@ggFsJVt$@c=`I|dG2K&G_;MqO&b*LDA
zQ5_p9H=jHa!pi8`+Xml+dBs-3(*zt=Q%v6;vPln?>mY3uGBRLde&b?d-Z@NKeSe_$
z>gAFIT6E&kN_smZ!7lStQ?f<{V`uWKl4KIud6rRTC9;=#m)BNUd>_#x9)O;SBD7b8
zp(sb?w!G=j@^m^45xzAp^ZlvOY_zmwuM_ECjWSG-t%ZsVr#(26)f=2wex`g
zS{N!)^4rRMqG0x=T%n|4PMdVZ6s+kq
z7D|!ElzOVfL)KnWam@Fv0ctuCm;98P%XgV6f9i?!t+_5w4nq!w)!;0Wm`{UnunF0}_s)k^qaxU#f?C3E2+z$N}wVO3tJ_qjfscND}2LionCMt+RsaQ3@U656OM(#V+f?ZmkDm@{ye-mqlY)$cfb9QtT(p2d{K1+RgOdlhUQk!Q9
z0d3RL5P)Z?AgX+)OgPY$-_)B6Xm`*AU_YB!Oye_M4JMGEgl_z$r_}w{X60*N3<;9s
zn#dHbaNbp!EK>DKYP(0{!|(ke%lR1d^TXqed*g(1x^kb)P{#Z0v69n_%Kr3?be-rcjXayM!y4wh)ahvDB4{<4;Bs^Xqur0;
z6Hm{DrTV6uJ{M0Lh1HCi%fTo}o&Ghukfw|ods8b=0(^X_CvGzUJaHiSe|0BxL__!=
z1$3a$B0@-^=&w6%L_iw{3R>m;bhxar-5R7(&pbEiC7||Ni-L`Q$g`QoZdNFFQ2-Dn)K$(eCe{N062#+7XB4bcIaCNd9#3TUl_9f6k6M1C6Tjc`Q>j
zgfkz79XSM{$cV0s8yuFp^jF%D^ENC96T+koV=U2E7NY<-niN%H^o5HLDeo0dv}I9(
zcj$tBy?QPsXg;3sb5>@IZCzLjjZGy%lfaMh8bOt#F#;oDl*3&^3>R3@r+F5G5~#Ew
z$0Xs{>7eL^byXH{e?@Dl{ie|z(a3de)^DrLQ(s4+FaJC*&spsGV1C=GFj40J@u@QDwEGkCYVPU?ZtPV6CQ6
zfX(K+#F$UxWV?@t0OeY>I3pa`(`&tJM!ruw3=8@kQ%~%7f6<2GHq_XL+F2T3uE=0g
z8|cfOOJVn)|N56}2sw&CZa@e}uD%H!WXP#Agf8mlGW~3>FHh`Y-e!*fce!YFYb+{p
z3U{UtUeO5ztcEUKf9XV_4rZ9xs4tt&K@Eo^D
z8Ne;MRjXz5f0|22D=$B^X+$(9;(L5=Tp!?TZv;l@=efk1UM@rYycV2r=5a0P!q5(m
z{IJa!zJ{(i4qz;9&a;K}%(AER#y)Sbj4Ri&!d@*#s?A^oC4y1!u^O4R`T8i((*o1e
zlFU1}JS?9vb>rp8cPaNbT90@NcXS#PZ@C_Mn=UB}e-fN`beOJ3L;!>T8`}I8N`*c{U;kKrbJ&p~G(aFi>!A)dC9#qs_n1o^eRZ9oFjxZ7|
zyO%L;t`y!zCgX%Ry-ZQQPNt4vFVpt=_gtV`ct0TDRt82(EM|j@LJh*d<
zhRdVAe;2sYW!N{_??nBl;5%yJE$8gL%0V3M0vp9iTi(_;DoplxF_tLVg0weWpXAhY
zmp{lwm`qJASk*S?%}|6lxl6my!jA2f6QvYFtb4>f%2t^~+K=FUC^NQB%ehJG^Aw5hWKBt%)IVz9
z>$=bBmLBaB@zox9JDl{z>A~C^DaVlWR2HK-?KX1qH7^z6zU8A>1MSTu&A-q~zyYjb
z-7C_K9%8kANnyS0g6!66N*J~Fi)1NtCMPznYsGEAMt+^|W)=%5MoVyR7>pGt&Y1nr
ze_V3DxweuLaDxULlQjuuO717F)4VxXWTd|=f1Rd2-}gq^*f9DrC$76*0lM>SyVOvc
zOsK@LiFKzP4pdr^_J-8@nNr>-`WXi;UJg1#jVuroMwtzSPJYvTpPl-kE^WB)w3pJN
zOYlr->(Ia@lsU`es`Zy4I#r=o0^Fqux3rN72YOOYIE?6O9=wJ-Ws5@0b~S(Dpm(-e>0n)
zHq%cL&jnam`^C6H|`^2m?INK?6>Z
zbu?_9zs$V+wt1ByNYiq#1zpp^FsY8N?`GyoLrykkfCqdMVg*<3
zmmBycemg-c%@n2<@S!CrCgFWfKtA;f&sHHVYsAmYFe&f|VGOw;uMihGf4q5s>Aigs
zOa)>P8f9rX6@GFKr~=Un?d^p~m9D)4RTbm;E^1%4l2y$ibOPsQmN0*8y@~O{f5JUQee0
za!wMu#0+?XeQQ9@b`xn(S3p%drrrvo^F7J^t=3=!=Ed0Vy&yU_?UHwa=xB)a
zyTCU?=ydeo8K9$$e-<*t+W~ZXg5LVre=$IshW^h&F{`inkH5yv1p`pWy
z9O{8Sa&Zb6?L^g+E+hkH3M?lfC>imW6k^H|T)<7Q#?hNF4_%6Dx(}*UuWygDj>qZJ
zX)C0v2&m`Grmx3A;Uwg%S4>Z=PENwAGUUA+e~ynTmX*9(#=DTn&UagSNr~N=Z{@%<
zn~`4+Hu>ITJv<7%Fr)Ia)#Vb%k?r?1H6L!0`F?CP8!fFmFF2kyx3Ji?h2k>8kcArB
zmJTZuy={NilEv^Xy?y2b+3Em1G~5+Cc6I^z;I(oXQl8*k<@K?&v(InR0ZKixlus_o
zQ-iOQsvqVIBPt*=h(jAzx9Q9E$KjZMVq-T_CeeCEV3Pn=hvzg65JKpF5zoO0OJksG
z8QaSq9uJtpu5|=gciP|u2V_LeUVGBur$7B4#!6XHm$7II6PMLk5-9;Sm;YE2904qs
z99a?@e>1br1Hta>NNloREY^$FyZy4MO~N0w1r2}Y_VP1)`yPJ2?tcH_%l6%$l-ZON
zNhY;@xo#?2A)VQ@6;}G~%jL%>DXoH^%O@S-vrq6NrF81kNe39vR~Wd!?{j%*b$*Bo
zPR5wJBu_8jY>?8x9QA^8{`%#I?T=p$Nj&=ff6FFJif;Sorj*diZ6{?!gn^$oV?_+U
z4g9qIW&2!MbpxkLSeMtqkW0krlDLixV4LJQvM8KP6EZeG3aJyD@4RqU-z5&#X`d$I
zj4#r)F%#K|qYZBy=^#MXdFOxGP+};uO%hdkxcrqu*6;Px=lbMSfYx6K=`$1l4U{)m
zf6DEL?Z>~uuL~^x9)7;AfLbZE44cy;_(%#|c<7*Rtlty$x&EpA{XeozoNJc>e)spU
z*WbT9D`5ZYKl;OT{7{P&V>DS>FfXuw{`~zs@+;6OY_g!~N;=_;2b1#i)&{fGf7(Fz
z8yf}3g!sQ;ON0t$gEJ1sbZJQQtjs@tfB3bURIs|R#KyqwjP*jASdOx}Dyd(=W=11T
zP|}<)<+FX=8^rvlqL6D8pfNVaJql}G2CtkwgPFD&yfn}0(+Ld8lX6Z=WnRiRscdMU
zUh51SFDr8Ha%__Dabg)TA)Cl9(C`j6mCpx64{(7C{~lOIfu5@ELmB8Nw|HrmLL!iHG{zCzpm#K6?rb8JHKapw9!JUk$0)B
zk=CVm!BZkY5OE4dC_~^}Rcv=gO+*EksC{Mp^1MI=u2i?3t6$cd0O5%SJHv4*urm2a
zN(eVH4#cNPq^SRZwR}Um0-liLe+{NB`iM}XhoeyAC?x3ej6YUh@i@Y%f7gi*!mBWW
zN99vX)%^em5XuQ{T*HBESo8c|(k<9$m-cXhc71$sn!?xJd^T6
z+k`%Us~`6HgOL!~c*|pYFp$xh`$4)i;E(JSrTh3P>Zg)I@SLa{Yla&z8D|FEURdvs
z6AI%X4jVEMuY}3A;2yOAS!+L2s|tmg+Wed66%8l&-Dtvq(~4woq&@K5dY<=~0C}a2
z_o;-HLC%>EW<9HP4D7%2e{sMAmN6a^29GtHZdIOc?~?`V?7Y(@EzV{F^IOb@;UiL;
zlgO~h(VEU=1L6NIIobl{$0OsAv+e+n7_5eQd#Q_BT$@
zev=KU2^t(rBjYkd6FRsYOu`B}0zbn+_^H_ET%okq<{7?N
z?+OQIwL1SHL0zI|^aB{CxFhFz93{0-2X3AX59LDNnI^dB`;;(|J
z{%6PiA#X?!;}2&@)EkK&(OGhJxD~Pk$y=cz{5FV;_%*FUY_5fbGIAg;0D+6rg0r$P
z?;KS;ZEOgtf9(heWzm>M)>zD~nDARf?~EALOOaUc8FHRQe^qVN7hT9N`dDQ=%)G^X
zdMrw)koJN*Qk^b`DRyH#`owpV&fS0m^}|`VDV3Q@4ozt+Hhu0OZXSp7IPapVnw_Wh
zg?ms3I$58V9ckYpKRRbFh_ZqC7}?-iP@chps#U)78dR+!*0P;cWJkl)grv9xNIAkY
zXKE?A$e<0xe~%)1T&Anj*)CW@nvVyLWXMhR+US6@jV#rz!QH7_luuoDbOgz$H;zML
zU^Y>8YY(W=XKu8JFT&a6cd+`<=47RC(K6dw7VIogC>DsU1iu2~Xqn&>Q!pfwgy9q?
z@zBbmIk0uvxf>qT=WOn!UlE$rB(1y#t#i^dS#_ive=@|u^&O$L6W<^->Eg)j7R%@{
z{WN0@w;gL7owW&fGWC;|HxTgd+&|I2a~cJ6?9Kp#fg9XelBJ%_Xy2;P9iq)*i*dzJ
zL`61D1-Ys9^c+1wpl`eFjgf6{H!z>grrmbeYg?oHW5z#@+|t9&*61q;
z;nMNOf5Z+0YG&M7s)9K%lfMuLw*-}@Kv;KHE=~^l$aF4Ep3z4p4{x!Xc}rC!<)-_>
z{Heaq9*L&msOHz>P5#E*^ryyfFKBK@w|G=C(iVghE*4f#XM+w&;i*T7J)I~s$*PuFmJ&_H6QIJ&IEPjpxd%$Ao5?4a#y21z^zhWP
zPM>^NfR&OdpG#0(nO9=T*T4P5*@3^T7v)pdqL~EDnpIe&bd2-HwR))<Ih^i^^F7l~t9qQeRUKGqU
zTJ3+*TY@kHr|Q1C7WzgZTcXx~YN=M4H}cTZ?l6~;1_KQNQ4qe~5+7%vwxqFIM~{i*H#HSDtE!<1LD!
zW7}wU?o>SZ#lp;tqfHB2AT^R-vP6yLqrY*$;Cy4AF4&6iB(yF`SvX
zNDT{*UdjS)!O$aKYB(P3P@lI?WB5ounkr`@a;WnJN{TndmUe%4p@~Y3
zd9tn71E>sy8);wqZ4G&cYza7KQ_G5l^{sSvug<1KYKdCz>3l3Tu*%H-`GyGhml)yJ
zZB!bRCAEvp%W5NTZcj~&rEq!|fgEm`QcQ=CTpVd-Yo+EbRXn_;(6j}O4FXR^n$JD2
zD+9h&2Rw5y1y0lHcDIzD@IZgHg+aK+FX`o>N(=JIIyWA13)C{`b3WZW;DUS?7=trmCq-*kzbUj<#jxGS}-t)T=XNPhUcTsyMXLyP{oP#NiXU=7D
z-_cB!9!muL@`PgJcHKBQ$Y43%29LYX%h-Ly)l9#zKGYa=z;_VARpx(wSeuLR!RJQQ
z+@kMPA3A;yk=9y;uU_`XTvCC!QURs0)x*5b_cEIGI}`!ck%PlqWUPuzDpY3o_K3ztVJ+PwDW^<(|07pe
zSE-v7s+ZJQU(~L;D~x}i0prAIg-iWr;5wo^scc}K8;+!wwp1d#28GcaDwf%DySy*O
z6r~h)Q_~cA&C>|95meK31lZy;2di2Mu8><^K3mB^B_Z{@WMECXEQv|vcg^TWxxuy5?TdDu)<^YC#a39Wzk8ws#J41n&($sx)-(y=&*RNID!9Lw#f|Ab5x1
z(<0H}%|!efaO@e)t5=sw1tz5+73ab)QkGaC4P{jy7a@CVRk19SZ5Xnzs_Sk9K!vsk
zFBB?&ywk2oF&%$+R-%NDq$l33L?f-2peD98HCr`PP&mN*;o?kyW_=`1@|el-k{{i-
zjD3ByW*5RXNIV1XI5?vP4>cVVTdi)<;vOe?!;;%YY6azk=^X~9CHnTP!Yv8T&@NF%
zY;SlOiYi@#HK204VqB5r{Vpb|Cyuvova>XFG|HjxPRf7f&eD^2AJmk1$TwWGvbNUQ
zvPC1b8t!XOAi#Qi=5lEpUnR_+hOyUW%SaHmU&S$Err8-TCr6l0_2|3-k`j^
zsJ*7Xz5YC>pZT&)k5^NL`hLDwsjUOE-aR(GAikGmd29JGX->4%8q3h~Hvp3#t}U`R$)ubMI?U&}?fMYmK?4oXPUdUq40n)SJqvCdQMz
zO1E6RKv%30og5;IBIMTNA$u>QZ|&E+M#A5Oc+FnqU%s{pXNSo^|h^${K2zr>WuCoEiX~)9_RHa8T#cRGypQ7(
zz2rYpS2;74_%)}VcdQWRA(m(y=*86^d#xcoO(k)Ljys;cP1?t;7Pi(KpASXu4Ipcl
zq1pHTFGin#_b=^(#2A;cXbTg!>u3_>5&x0byQ)M{Bt=o;*X+%28@UnqPi~yT|HS6`SN!w?{(YUj{{745yYD4z
zq?m#Ta`R=skzP;2z((mw3%mKU`{|PqTH@dCQF(lC1O5pijC_1h4lk%ZUfAL5Hs91L
z-b@W1e*mB~iI3+`+6e*pjC@Yd{QTv|%|E`ZvUren({U~*ZOrB&UNWI@9=nEp?l3YH
zIgju47TMA2Q)WW}jwKE*J+h0<;_bw{$_>)6<155F@ma0-bLo?!Px6_!*QrCKuJP69
z&u*9Lsy#jF#AA|Y>P@tkRhEg}_z4`f0hFqYe{FSYXCX)LHm5^jSp4hLVB;XH;$>OlKBQ=iMfGQMwd*ferwBEj$e^L78X=O>B7|N7r{
zGpyfKQ}EtHlomec*#G|d!+7O)DN)@E{1;Jfkr0j
zAkq#vEf>SV_*fi&dh>gUu6n0me>n3fKyY~~C+CcTf%1@@^>&xv>z8?07yp$m#Bvu#
zO&V8bj@e;`jcnat=Qa94*EiSdPyo&Ogt_#>b<#nTPa|v63a&vO?5G=B1
z%aUPYScp*w`m*TKcKMyuzPv+j_E{EtNl)#!c^G?S+1S#;zzp!yWTFz;h5Vk_0Pz!AcD5g2M$l62!S69ny>8Wm?w${MWx+LdV9X?0Pz=Xt)I#WXHM$S29I%zl$Ek0w=#1WxlP*xwZNqn*ur&v
z>M7_0Q6k>gmWPSpaHpXCaW1i?6JwyrHm5yj4tI0bcm24@`gO+ef3{+eMba
zogOuv&qCrRJZ)+7rb%ROW6bRqLfUFGXr`!o`x-IrQlHny5-x62Tny~JhVz5FC8lm1
z)PBfuzfn}1rj60=&Qa}sR8qoPKUti@OHu9Q74GqIsg8q^(q~zW7wZxRJai(CU6^D&
zOzZ-_O9C-6sC2**?mZ|ea1}IVOF_}^MI*!aLG=Wg23G>;`;1A3$qPOvjLEMW6C=1Z
zrsHA#Mct3SA)l@8?2%o;4dTZWobnhzE}p-MXzLPpuO^rpe-5%EY^hitAqIy=*2Bqi
zm$CvWut;rypY>-7VL08Da4f-5d+vk1eD(`Dyh;H~%44Lb)xPl=xk|0-Vduz8ra9+@
zo^#^Sm`{z0R+Mm|^S`yTd)#(TM%tEuSUC|l7^2cMM-F|lSJOjeBMd^52xTBJg
z!r(BgDAaNy!=o!Q2SibZnON+^k*=f+SYiJr1B?kJ4SJkhi9k0sMA1_wJx(mKHYMzg
z8mC|4eDzq;gz--DMEixbiIM%htfrAI9X&1NjZ`!Qe{vahvV$0T7_Ka)aTe6+H;X1(OqqV|&B<<+8GTbzD6?sMIcZxNq{8Mq>$&b1cz
zl?<*+q^?Oz3fz@Dby!@BOe>sCEJ>6ypNS!3u)}9&4>M&}|Cz21X&a&~Dlj!By{XoNBJPw|zUzq%>!?-CfmYRJ=phpH4e+&-kP%%ScLrJ+&F!
zFF3q~<>}0h59l~sI9*|!jWarX4BPMv3uA0!Z=q+$=1boG4cf;
z&i^c`#qLo()sNh_A=F3Dt1Jh1g%Bg
zfN^U(1q1SrHhd~Dhi!BGNuTLX2eoiwNiX?1&G06^4zVc6h2oaWQX%)2CPE}YIF0Be
z^~^-ZjvI4iu4E82&Dyk}w$*G?JCFyk7@6`C7K2k-!eSWQ9GnZq(7i*-+K~B_GP6^c
ze_6_1!X1m^GV%@T}me&}gdLRjp8h5=PLHn*5A1V-S*_tqVY=MXq_rBHVPR)3;J=xygJH
ztvHI6Fe{izxxm7cRi6!0d#+*c6v1MmPa?mRmfsaQtXi64n7-^4G#Y~&j3L`>f5IlM
z%u7Np2{vOWViqHMsl`OIoo2c+YAr4PS{HxGLXfmVETN<76~&ftHk;?T#&{>rxN5PD
zYZi7^A4WKNvXf-+6>|kZe)x#5(fIi^nEN-@qY;pJVIzUMUISHv5LW!;%
zgD5HQC*j?h7$w$U0V(zU%~49Ne+9vmj&VphrJlo6flA;p2J+!Gfl92)_k-ABOx+2n
z^pS@BZ2*;StdSc6l|b2a+ICN*QrE{jf+_)o$!Ylku}WZIQsED%5|hIkQt2Eh4p=*R
zI3Y|wlfH42jVP3!K8sDyGy?|{23aG$)#Mh&1FF(2A6A?~m}EqVaKh4ne~o|1exp~=
z+6@ImS)L0z%#(@YYe@vMxI?ws6fxIr&F+J2ML{J@nvDU
zH~4IQ^*;f8#$sDSpB)WVDQVfqsu$tUc=rW>wi;U#0*$pH2-;DW34=DUd=3bWcUw?s
ztE>_XjkO^h+EG>sh&Jq1e~uy1cvl&Uw#r?`qO}GUjCPc_f<_xyy9SO1F-0WhtHRM(
zpYI2j#hAJm9PJ~G`x}9y-Bcy70!IUdI}fREjYs2T-y0w;tvnWPgGl4V-WHMuI!w6H
zxE&;o6MQ2`8dykRsGC93IKeiidq&}BLDtBBya8lw-Ep4;S<9hoe=w6b>^Qc5r9T~W
z+oj{{23S}*JYP#1)T8w=OW(dz+a*bWW2!(cr2`rtbKnHDlv+A&ZwLMdvh?MNF5R>;
z&V$KH=+aEkml2>V>j;S~J=WK18dG!-qVv+2Iu|O~j<}lmsRoiM85Cx^5n}=?gIYRm
z$%W)&*0tn`Gw71&f9cb~BzmU1lthQaNpz(#v}cL2v(xAejMQiI!b}*FU<=uZmcH+<
zI%w7b#o=~%{+<5{p~;!Onjr?tqc?z971@p{$dz2RFZnwYCJ{GiUH-1+k~5lAXP8Vw
z1e7cDoMJy6bV4M$UBfBHNuVoSg`j!)Ihr>4lX~Iz^b;Fdf0cO4=w+H2wMque?~ueY
zHJWhq+;i=(w=UNd-OcMnd2SJ6hLLdqwS>rH
zL!;!W-q8T$b5SsEEraocf_o_PQp%jAu|ds5+e%OH@-C{>=x9mXf)%UJYc={-BNss$
z7}40!!Bp2*e|!0CPFQ}&w5N@G^;5E*+Qbv}t}a8lanzMsq0>H*DKkMwS-
zRz~=IwH|f|d8=~Xk=7ZijC){5hlK`Of;Or(&Q2=*M%SYn)J1((HFSMmuGSDw`Q=FO
zmTF~$f3H#N6mZ39{h
z;~d*h*2*~DhVrt~IIMfBjkC4^uElX$n_3;`7|XRhPS5gL^>J9YR3K-K)mkB^wW%d?
zjS)ziy=**5~_4(KDv*
z1x@%!At3VTUkdxFmFO|c|zBg!s5qh%WM#XYCvA2aL80jaaZ&)pd6MQ3R
zg28Ce1$#Sa0w;LFm@bUG&w?Y6&v*kk!n(5_L(PNr`~$c362)4D0TP`x?w)H6d5k1o
zf5@-)i3-KX!%m)(&)>kU)$XCIOTT~ghE?aLdNjIa7O7IV7=Kkj=KNOs@-MNK;u=jE
z{PN9p&8ouWvi**}(@wuca1ZABUU_kMA|;nM?iMs|IUg*>(?SN8CXZ~Ubf2|3o_Dnf
zO1ctL=vF)$S@O58e$k(bFQnu@>Q1Nce;La-Wb0U!JxWHJ1B
zyscl#0Mi|U98hs3O{Hh{<4;Y*B)%_6{KD%K;Vr2APD_fXuU1nAH%~q`s`h2|PyS~s
zV$Gb;^OBzDfqrwOjX;&eeoff#n*<&oQm4dBt^1(nB~w}z{&lF7
zM%7xdaZ=#w3^e_d3NHQSlFxtoKXU}Amoe@U6PLD&5-I^Ox8aKt7zBUaW
zCFe(-8!Pz{s9F1*+OfaEXo0<%c(UZ#)|nao|I$6s93)$jF|Z(=YVU`4^&d
zN!(zc%e^i~@xnOX=MjG{QMVdD_I?fKHlPi*6?69f982_bRy>|hl{PbCn`4LF(a4(T
zI$B2RhFcB9TeCNu1@g2Te7L2(U?KUSmJtdpsn&8AK#iJU5T3{A4u5ok9UPBI^(X|}
zR=Hd7U6{QNBm5k|-Ju8=(P8v4!fQgn9v;R4P+;bV9ka0DQjLE-VC{^j4{I>l1#6v1
zcw2KonbWWiI{lMg)?C%J^WHjnu{Z<9L>^uir{6J;4=J4M=eb|3(XciT@S0rV4jhrt
zIm8j>S7aOa%<0{XR_5&(qoYEJF58@W8-d=zUDU5~5dej8az#NUaozWrZ&=?OXo$Pn6cM3OhPn^j()6MNs3VuKP
zG!7&8E?xC{HsmC4VT+If{D`ft`g#3H50ly?Yw{3D>*X0x4uo14H_WKa&Kda
zBZC^#*wLvR$);0QD?KJj8`EB?#0spE)nTKXx#S$VEGg2n%>Cgy1!(>!D2mp4I7
zhXDz8+7)k#
zH0n|6w)w4;T~-x6#>7gcfH9~g+E_}o%T>(Uk)>!XHM9h{Ee__&DQOP6BQuma3X^~<
zW9KzPOLYpk5O_{RvtW*ia7H2=s@zLq7c9SSP=i%5mBH@U4*7LCF#r{hzS7=Qta6W1
z+TedDxU^3Jn!4hph51I*bJdlLjYik{Y6&5wic=8nxiOTMHw(zBFDuEC>iA%FQ)1e#
zvNnugD>IL0m9)C8H6ClBBNeZy2i#KH3~f(o695>>{XD1^bM-(vi-t#jonl(k7Q$aN
zwUo{a_9)-9vX9pXS^KJZhuZ?nqUbkI-buh#qcIu9$Pn&hoJ
z5tpFUbF=t89A4sU%1Yfh63~mQt>E^x-*j5TG?FO?34B{wtyS3VgAZo(o27oc%jtiv
zM>%lCt?5|8xa4J#2wwGY&w9QVQqT3r2R68;{R*hDn4x+2o+Z#`%GbxJ06?+Z1eo84
zaDO?lLFyY7LH|r-|DbHi;W$V1e4i@ln@Xf6OD^iy)t>WmX|nF0>~pJq-IY<>2m+3rNe5wPCBenT{D|
zxoeJD^VE79nPKO`dU;bc-miZ&-ruiC;LU8Ty`f0N!dO^X_FTMd(sZYj{jlHQ^(MY)
z?KEeTUqq#(W1MnsSc*&~=He8!Ej#;K7!5S3tB3x?d4(mnT$U>OJeKQy7fDd5bt|n(
zeQS!B_-55zwxmv6(V!*L?l!cBGNI&H4e{-hjLA$$Vh#X-Kz_g7N{lFI3UpQW=5V`Z>xKTS}!`8uTgCk
zZ*vjQg}dTMD9+hrqixw(uPya|7f(#NQ`H?bUskLAh2$rl^I*1Y?6NvKznELQnT?JDVrBw{QCEKhWHD=`3%#X0W@}yobSfi>b6SPRD%LEN|-A
zVyN0Jsh+~!TUF&ULw)L$r`?as;=U2`axl7}0xx7unpo7MBA3gW=Tq5#;zd-#lD^4G
zrfpzKb7fuF_QE2+#o(J2FFpCoBVU*iWpC|(z{q&3;pQb9@JqYpC}@e?#09X%+ICaf
zY#Ebpf_$4MZze2SxBL#C%YP5v&{>_O@g{^OFBk9AL7Gr5;BgCi8jQA_?3V}GL*=(N
zZ-}QF9A94K03$TVT$qV}%{|*>^%6vc~mKG$#*6tb`)14Rw-4A#1fTl
z>xAo**bXVT)OeI5Cb1N0@tt}LA2+Ngh1W|rhcm+!tFD4mOogo$Gq-b
z9#6MQ5-C!A=qqvhZIY9~A2~U|e`0$6jNjhj@29){{g*tM5+r|5M&UPsf92^xNotTn
zD2I)3`sKq<(?37#(U5vp+Coc1f}FjtL~u5bzkpL)i!E}YPp)}p&-9m=5eLlVff`%%
zB7_s^srKo!hSaXkrROt#18PCS_}PZk%j6mAob;4h;DuY@srG}HG;TdUj`AZxMFE*f
ziaCfNI{_Ir3y^;-AelIX^B#A8BSydB*LUKimQW-YIs4&9*Yl!g83J;exKJNcZ%6Y7
zL$mplvyWK~u_Y30Un#zEDnDl+8xok)KiDY(2(LLNiZS9{?>20sTE
z@PnF-4tf1Lua~G175})uhau?4{Ow>5r=Bfu5VZp5TlR1^!)SF*o;*Az4MR|mz1C=s
zsu!l8WSMmV{KVX#&oqz9+GC19E9ntC6|qN>ai*O(O8RtlH6iWo%->Qt
zCf$jZ(s+MiaXZi!QZU*=iYC^s*?LP9X`T`tvI2c*_dI=P^Kt6Y?uDy;bkp)#EuzelyixvEMLMEOI}in(ya`50kIL|lya@z52W{A&
zNQG1lMlq1j=JbGEVw-j&KLlY0S6!YlBgd#`(5ioPi`FOCr{!o;1+$j2^KS9CtXks~
z%I7^?TCBl7$Sgb$
zxI5I4<05LzFw6|(7-l6QkFIfB$QQff+LeFI(bwoo-zhh6mU@K8N+;)Lxpf^!(`+0^
zQy<_QMWo+4XY}k#&hb)Th0&MOpAth|Xq{1Fr-{BrX@$|N0$c2@yX6ex^n*#Fvq^*{
z2$qEwml$VoOI|3n%eusq%QIszAO+6GxOJwnG;8$z>PH(4Ey~*xe?WW`YI%ykTD*S<
zg|P;_8U`+dhmh)TIiYLQ5jeLzq=SHHQdrkGub4`?oO#nC;M^}F#q=V;*c!#NGW=+D
zeLgg@D<@|MM|KrvRSzDWfp5rb-ZcxaGWF-aQ64Yr<4R7)7EV|9y_Sjir$naVodRK6+6Kc%c{n|vp
zkIqK%d;wv7zVNQ`9WitF#gy{C(2Zw_Lia75p0ek2!Bd-Kb6<8YndhZ$fO78Y=45}|
z@U(BuNnGb%gap!5lym!m{qISlsd$hD=U5EQ%^#F;gTy39Sv^ayr_Ym?v%n9f<=5%o)B6h;k3uS7nq1v;jxktxM;lWdD|AO2
zQ!Z)Ow3`ulW>K~sVZ&^!JLZ2DM`~v`+{(>X*>H&zgm*1XrzjQKM&JO`+Q1aXRlN@MiItouFySBE}Ytk^LgW7wu~x;Vchg&
z9j3_s0;^;n!FOXE<=0nmibI|9dy3z2ZG~$_uz9m8I)EU+~X@gWuurr_rRspoPICQF`cpGa{eX
zP^Y>ue#_MR{FB%BS6nu)91KnP!+$@${Qda}-RSh`fAwM5e~5?9v7c-H``5d5
z%kRi18iUp_DLY$5dG&wiskD*Mf1S`6$|@3x72R*I5j0zLAOVkqVf`ny3DZgF4u#qQx-$T7s_gHvxBinq)UoVs
z0G(-YoiinD$6w>a0iAsg{p$b@R|asRrR<74x@zb4eK}Z*S$=;PPay#M@+%@FO^&(J
zmqc+062;g;Ye^C!
zBq0iR-B^gIjtDQmiS_YV{RMdg#Dk^oCrc;uk~noo&r5=yoYccwC_ZjJ-=p{FXqH|KY9;zPJNrJSP#ks
z%n)r4>JMLX9o_2~O00c*sPk->P)_ZAOc*N4$t{0JC?_VUv$WKuN318CP2j#6-E7HcbaTj&~3
z!|3KA%ZzT`9=!{?*^)4syC_oZ7EsN$&y56}AeJt}Bvuc-u#vOF3G5g;(;m
zaV|m2H-HnGg^WoG(H-&`FLxKgb+tmOs}({48}r!T?c7$mG2&IfjjtDOu4Jbxj;dbv
zEiibgNxC%OeIRhPg}}>#hE+&FptOH=udGAzg$OZ3Yg2nwN5dkUfO|DqIv7=3w-|s0
zoBBdp)Q}56hywkkx?-iH^gdREn9VW4)DfFh46jDnznr|`{gN*(r*gYdDIKlcgx2G{
zRBKD9D>TJ{aIOV~e8D_gvgQ&CE}DwfeQ&}%G%<}_aE=AC!~#@bBX4Ih%m9B1oG$9i
zFsjpybzM}a>-##eT&F7^M|EI2r_Q(sa>2DM)zWQR&3E|Y_odE=Gnx42<)u`Xoljtz
z+BfQ%E7MGStRxjhSC#mFs&m%4(3$MisSb;ax*eL2X;zyEDXzEZef3#-=8aD#MumM)
zo|ya|j+_sdAoC^g;)FE6i}PgsE-vxBz>IjoCPwCoy
zp}}?brKA^H?)eE9LA7Pe9A(oAhLx~c0#shxFr&{^49pk@n`_F)G^*CpO8|@Mi&ahW
znLQtQwB2m!Z~q5=8t4L-L6s8|w?3s3HVS`PB1}KD{PgpC$=^(Iw6J8U0JqhbY8v(F
z?Xpd(-7(j+$m|SWTq!~A-NJ*q+^@q+|0oY_ENd64Afz*}P7!KH$F+CpY$}^7rhYcq
z`c8vQu#B6)qiXhkUw3PV{&gJeCkFSZyYH}wG`TkZJyu)CoMRclQYnl&KovVcQ2l=x
zvo25uCL}Obq)in1Y@GAq4M`5sv4?v7^!Nk5?0;Dl;&O$^$y!jAfy?A
zTA|>;%PZVfB^G_y6X?
z{~!Yn7+O$a`?s~<-)KwNfMXc`UITxwP0aBIS@59jz6BRS1O5++D5O-#be$V35HkSb
z<)gtRJzH}L?{E`ziX&m1tklS$pRo23?jgjqMa}(4_g?n$24Cok+#wdTFS4Hp0Ec?i
zyRMEu<-KB9BskaS2Y_0>-T%2aR}#?>wgd|wV9tk`t0E5*Yn^C}cNd88nx=p1U|uPo
zt;N{gOW;IpJ4WDMVO=q<)OiIVK6lw1N*^m*R}jABWRl2j5
z*HVIA4F$QnJ0PSZIIe2QhaPG;V9>X!LsI{I^j)e$Kp$3zC`%=C@Ia-5_QGlyvd7`1v$!lTpGU-z%^eIaC31;y&?6UbHg%vn9n|PL^G6@4HvP-dvxzRs=;_(
zSZ~Io8r%%NHlh!Y*3kH1JWHAVfknn+8$BG`G^AR++#|J0Q}N1;V;r;xQh(twPQ3(X
zsodI5^^o3n1uRH1?bLsQNl~qKs(Pj0bC1epbG>I_NmG6d{K<~I6i!i(xBg88cd#9E@=h1IrG&+p-9@!wWmwBCc@&rlX5IDYX3%;
zp_(`Kz>O}oy`M2cI=r8Ou2WbzLSw;(UKVVqpv#oT^*xZ5ofHBDt6h4
zbd{lAV{m`r#fS0QL;CwhFO~z+@!A8F6OvR=o)m>T*Gmp+Ecxzp1w13pWOK%*UZg;y
zX1gmN)Uy~#+h-kUi}JO8S8nj|oNX?n_HJw~OZEp2EvIn~Y^oTUS@i4fXYF}zw_4y6
z*Y4J<0hea4S=X9tpGPrM0cpYYm4!9G(WX_bCT~&rJY;9ORm~oWs~6;6bR1ytpTTNZ
zI(qEqTq%c=;d#1PmR+~`YIvalDWB)*a(xGGQNn+CDFbk89Yul;{ak0dD;=nF-uY*-
zKK$uFSA=*%mqC>i6PHc35-9;Nm&+Ox8n=*R-<(m}r7~!8Te*LoQhh}Z#Q2s*c
z#?>#1q9Mu*pqHSs7fRQqjbM2Bfc}*|xj$P!m4?RLQk$=y%M+A9UBG;mF2RamW}tDaM2tj~hxis^fOJB;
ziQ;{K=lE+DLuWa9g=={&B1W=hEuhou@GmrBI+cdwN=|T0n`JH=GM4Y`ldLQ_pQE{2&MOA7wkCGTVIra-#waW8H4xV;m`xeJakmCwTHJ3Bo4B(~Q;#>D}D
z+zwSW$rqtIM>Ua+up^WBY3D^tqbE;s0P9X
z=v59_3bJQ(m&*`L`6f
z%1$?Ss-+Tb;2D$`&U^N6*p?N$pA5*)jM$j|z4pEPx~oZhjIdB$37jzmw<-GpR#$JI
zvNS0(BQX{aDl*T)vePACFyps>wrXwBDipjmiM~X$G`Uz|z>Vz)x8>0f-lBGKdZQb%
z1oe9FxcyEpn_0V(f}Y9`yI(b!cyRf$aMv||(6$8d-j1uMYcidLFVg!w4r8xQ_8dCi
z^_No4spOWhN6dW8pYDN16E4r=8}3Oa0^db0EET0hg_rxlKTE-NSe7M!UZd1S&lNa_*!X7Bl*{8?k&Fv;ko}O-8ChWq`n)IT1-@W_04xtCim;Jb}8jyo6ErWHWlMv
zctv`>&YoJU1wENNbMhyD>nS>--0SB`0h8BkYf<5I-E1;*?4Co>Ive6pLz$AWW6_U2
z&-!Fxe0o{KJo8T{)W+#^`{|L|wExoAev8Pr7rryB4_xKUcR;r`<|mqC>i6PKCA5-EQ*K0XR_baG{3Z3=kW
z<(x~88@UmH@A(ydOb+6b#rMJxf&j?^dvoI3Vh_@2@t>G1;D0{7{EmP9gg>88j(__!{qPSVC&8KLUQC~k_);)w
z-2{p$Zl+I%Up{|uZg!k&hd;30NGY*J9P+FDp4roJyHQGEtCrZp@hG+%aMU0;mlhj~
z2!$=`umy{+E#H>2l%v1#2=qSo+EWjp9xwP8PzxG>uZ@pqgn)+dr_R0Us#(~FSW#g(clr6n!l{u!lACxucJI28`=WD~Xf{VssKQMkUPMS1V
zj*P6v*IsWI2r@zyykLjIF6q*h}(#OX6XH=f;$)}&E
zUw*~I0Xu*Hgg>9>ges20?4&HSQDz-O6?LZnsZk%(zcjw@aoBm}ph@5l|M`6U>&s5y
z@IU{zzUi0W1m>M{lDviI+2+?je;QlE?I-`F)9&Nmo*=4nzoJS@Fvj#aBx-ZqaqpVXM>3rMELKFA5ObUQt
zRzo*p4vGTF-y{#kVbZg)c+Qr17?U@Jy=6w&LHsLk!uQm#cZ|Yw
zCb)XoC_3?B6k;~Y?ic}HRm^DB&1<;mL8pIpNbkei6xJht(^_OHbo8hzjOQfT6Iq_<
z<%vn-m4`W8v|W*V1aM|TCiLeY|8k2QL)p*$a&S?QYlxv`N}QMTrm0Q$z36UZ%XH30
zWq({Jx%hW_ahjn^j=6(TZPqM-IVmrv!5Boq)sP1pw{?(e57^i0qAq%kZqy{T>~wz{
zri@um*(J`B>vDX9a~@*wg0(0az>L<4Xko6S+RVM^G#ve5JDrMob*8Yu_mycY3uzVO
zbVt2pCHAy@tSw>n(l{74&As`MlDlI_@UVqa71}vXxWfc^n|!1v_CI47z?(e?~lbOw?pAA7_%d%x+1P2i*!2SZ%8ASv|BXrK-zi%4rR$(LqgWfy{qtvH@h0R`G`j
zK&*Jq@R`sn(x70;MoP=9kIA`KCCA<;c$EEbI>4hpv?Oj^jE4y1OR_tAnI92X5IN%k;nko3@_e?BAHIddtox2(Q87PR`9)41}I^5
z`g_7M?U2{tGJu(_kdH$ez5K_K8Nk}!IQh77bn+j=W-t?H=&z@+nO@g&&3Lu#Sg>1H
zcR0cv;G%V_-!YSxSeTs1MLXrG-xu~d`pYi1mnGs{nSb@D9jJB@VY_
zT>^2XLnU#SY|DQrt~c!-76%^hph7>D#WgxtgHm|o6mSQWYHWHGi+e}I{#x}frqLk1
z*3W`*t4_&NU>si0%v$j{8rLd#GL8fEV3Yjbh2t7o-w=)iu*{hifm|!_Nk|S9C7^CS
zDAx*n0+s`f*@Lm`ak*CD1u(aY{RSI_?Q5^Q>~91P_CJ5^x^Td_F@0rq*O(fC-I!kQ
zf~EO>@nl%Ke3!l+mP(||B~CT&cPhsmMkF6MsGQ8Jxl{crH;kH=6es4W;T$)`auH0g
zO^wv-=3(3$B?vdG0a}I!+;|=*8WRj|8Lfe2Cio?+8pCXn(dVb^$h%V12ib}S
zJ|9$ynbVlU<)UA5hH-)qSzVc5u_#}%2JWK+X|I2<>~+%Kps|BG{7d$Ez@Xe{hH=+{
zdYg?n!~hB)JU9$w3XkYr*X#wv$xo5wb715-=wNr~H=x~gUMSO{{*_-X#AkWClJ3D}
zc1eCyWi8WzgEFdpWu=j+>?m+%2Sf+
zeQn`h;w?SaaY{avcy~J93-RuZUXysYg6}2X3a3%#k1&59#Je5x8pK-x?dikANO3R!
zal~8U-C23@xN&syA49xxU10n<4+|k6jnZSTkZEqH3to8$N2T;#qip3~wUcw%X6wSoYkJwR-`Bg>ZMSlIcGtR5Zo8VD
z+daG1(>Y6eG&f()MXvzowaUue{8HJJchma1=_YL6C{NUUsm9CDy!Ob<{F1pDnGb*F
zz6F^#N)s_(GBX47+9UJwOJ-(VKGe#WaCxIB(()zCA}lYb7gm1Bu7t`5v+hCV(&KVy
zp8MEpqjNQ8Ea(x%;pKl_b~
z9rZ82xH;mf25FZm{F
z$jpF)jfttTEtg?viQj3t)goaX%AI66U!~j>V*o1@BA0@OY;2Ra1}7eBsvR!OBoQTP
z_>jm{kcj<3Hvvj#CZ?*}q@AWHEIZNeU6om75h(Bsn@)&$_(7diLyR%8nEiIL3=UMWMcfL*t$!4_S-}a