From ceff335bb8dd0bd4ee6b15a0ce2db08adf244773 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 26 Jan 2014 19:50:12 -0800 Subject: [PATCH] doc(doc/lean/tutorial): update tutorial Signed-off-by: Leonardo de Moura --- doc/lean/calc.md | 15 +- doc/lean/tutorial.md | 361 +++++++++++++++++++++++++++++++---- src/builtin/kernel.lean | 9 + src/builtin/obj/kernel.olean | Bin 29094 -> 29457 bytes src/kernel/kernel_decls.cpp | 3 + src/kernel/kernel_decls.h | 9 + 6 files changed, 361 insertions(+), 36 deletions(-) diff --git a/doc/lean/calc.md b/doc/lean/calc.md index 0937f7c664..3fe592999b 100644 --- a/doc/lean/calc.md +++ b/doc/lean/calc.md @@ -81,4 +81,17 @@ The Lean `let` construct can also be used to build calculational-like proofs. in s3. ``` -Finally, the [Nat (natural number) builtin library](../../src/builtin/Nat.lean) makes extensive use of calculational proofs. \ No newline at end of file +Finally, the [Nat (natural number) builtin library](../../src/builtin/Nat.lean) makes extensive use of calculational proofs. + +The Lean simplifier can be used to reduce the size of calculational proofs. +In the following example, we create a rewrite rule set with basic theorems from the Natural number library, and some of the axioms +declared above. + +```lean + import tactic + rewrite_set simple + add_rewrite Nat::add_comm Nat::add_assoc Nat::add_left_comm Ax1 Ax2 Ax3 eq_id : simple + theorem T'' : a = e + := calc a = 1 + d : (by simp simple) + ... = e : symm Ax4 +``` diff --git a/doc/lean/tutorial.md b/doc/lean/tutorial.md index 367e3cabb8..00a1e0c83a 100644 --- a/doc/lean/tutorial.md +++ b/doc/lean/tutorial.md @@ -55,9 +55,9 @@ type of a given expression. The last command returns `Nat → Nat`. That is, the type of double is a function from `Nat` to `Nat`, where `Nat` is the type of the natural numbers. -The command `import` loads existing libraries and extensions. For example, -the following command imports the command `find` that searches the Lean environment -using regular expressions +The command `import` loads existing libraries and extensions. The +following command imports the command `find` that searches the Lean +environment using regular expressions ```lean import find @@ -89,7 +89,7 @@ The command `variables n m o : Nat` can be used a shorthand for the three comman In Lean, proofs are also expressions, and all functionality provided for manipulating expressions is also available for manipulating proofs. For example, `refl n` is a proof -for `n == n`. In Lean, `refl` is the reflexivity axiom. +for `n = n`. In Lean, `refl` is the reflexivity axiom. ```lean check refl n @@ -105,7 +105,7 @@ The following commands postulate two axioms `Ax1` and `Ax2` that state that `n = ``` `Ax1` and `Ax2` are not just names. For example, `trans Ax1 Ax2` is a proof that -`n == o`, where `trans` is the transitivity axiom. +`n = o`, where `trans` is the transitivity axiom. ```lean check trans Ax1 Ax2 @@ -120,7 +120,7 @@ will reject the type incorrect term `trans Ax2 Ax1`. Because we use _proposition as types_, we must support _empty types_. For example, the type `false` must be empty, since we don't have a proof for `false`. -Most systems based on _propositions as types_ paradigm are based on constructive logic. +Most systems based on the _propositions as types_ paradigm are based on constructive logic. Lean on the other hand is based on classical logic. The _excluded middle_ is a theorem in Lean, and `em p` is a proof for `p ∨ ¬ p`. @@ -141,7 +141,7 @@ called `nat_trans3` := trans (trans H1 (symm H2)) H3 ``` -The theorem `nat_trans3` has 7 parameters, it takes for natural numbers `a`, `b`, `c` and `d, +The theorem `nat_trans3` has 7 parameters, it takes for natural numbers `a`, `b`, `c` and `d`, and three proofs showing that `a = b`, `c = b` and `c = d`, and returns a proof that `a = d`. In the example above, `symm` is the symmetry theorem. Now, we use `nat_trans3` in a simple example. @@ -155,8 +155,9 @@ example. ``` The theorem `nat_trans3` is somewhat inconvenient to use because it has 7 parameters. -However, the first four parameters can be inferred from the last 3. We can `_` as placeholder -that instructs Lean to synthesize this expression. +However, the first four parameters can be inferred from the last 3. We can use `_` as placeholder +that instructs Lean to synthesize this expression. The synthesis process is based on type inference, and it is +the most basic forms of automation provided by Lean. ```lean check nat_trans3 _ _ _ _ Hxy Hzy Hzw @@ -180,8 +181,8 @@ is quite simple, we are just instructing Lean to automatically insert the placeh check nat_trans3i Hxy Hzy Hzw ``` -Sometimes, Lean will not be able to infer the parameters automatically. So, whenever we -define a theorem/definition/axiom/variable containing implicit arguments, Lean will +Sometimes, Lean will not be able to infer the parameters automatically. +So, whenever we define a theorem/definition/axiom/variable containing implicit arguments, Lean will automatically create an _explicit_ version where all parameters are explicit. The explicit version uses the same name with a `@` prefix. @@ -197,8 +198,8 @@ The axiom `refl`, and the theorems `trans` and `symm` all have implicit argument check @symm ``` -We can also instruct Lean to display all implicit arguments. This is useful -when debugging non-trivial problems. +We can also instruct Lean to display all implicit arguments when it prints expressions. +This is useful when debugging non-trivial problems. ```lean set_option pp::implicit true -- show implicit arguments @@ -206,27 +207,10 @@ when debugging non-trivial problems. set_option pp::implicit false -- hide implicit arguments ``` -Note that, in the examples above, we have seen two symbols for equality: `=` and `==`. -Moreover, in the previous example, the `check` command stated that `nat_trans3i Hxy Hzy Hzw` -has type `@eq ℕ x w`. For technical reasons, in Lean, we have heterogenous and homogeneous -equality. In a nutshell, heterogenous is mainly used internally, and homogeneous are used externally -when writing programs and specifications in Lean. Heterogenous equality allows us to compare -elements of any type, and homogenous equality is just a definition on top of the heterogenous -equality that expects arguments of the same type. The expression `t == s` is a heterogenous equality that is true -iff `t` and `s` have the same interpretation. On the other hand `t = s` is a homogeneous equality, -and is only type correct if `t` and `s` have the same type. The symbol `=` is actually notation for -`eq t s`, where `eq` is defined (using heterogenous equality) as: +In the previous example, the `check` command stated that `nat_trans3i Hxy Hzy Hzw` +has type `@eq ℕ x w`. The expression `x = w` is just notational convenience. -``` - definition eq {A : TypeU} (a b : A) : Bool - := a == b -``` - -We strongly discourage users from directly using heterogeneous equality. The main problem is that it is very easy to -write nonsensical expressions such as `2 == true`. On the other hand, the expression `2 = true` is type incorrect, -and Lean will report the mistake to the user. - -We have seen many occurrences of `TypeU`. It is just a definition: `(Type U)`, where `U` is a _universe variable_. +We have seen many occurrences of `TypeU`. It is just a definition for: `(Type U)`, where `U` is a _universe variable_. In Lean, the type of `Nat` and `Bool` is `Type`. ```lean @@ -244,12 +228,319 @@ Lean returns `(Type 1)`. Similarly, the type of `(Type 1)` is `(Type 2)`. In Lea That is, we can provide an element of type `(Type i)` where an element of type `(Type j)` is expected when `i ≤ j`. This makes the system more convenient to use. Otherwise, we would need a reflexivity axiom for `Type` (i.e., `(Type 0)`), `Type 1`, `Type 2`, etc. Universe cumulativity improves usability, but it is not enough because -We would still have the question: how big should `i` be? Moreover, if we choose an `i` that is not big enough +we would still have the question: how big should `i` be? Moreover, if we choose an `i` that is not big enough we have to go back and correct all libraries. This is not satisfactory and not modular. So, in Lean, we allow user to declare _universe variables_ and simple constraints between them. The Lean kernel defines one universe variable `U`, and states that `U ≥ 1` using the command `universe U ≥ 1`. The Lean type casting library defines another universe variable called `M` and states that `universe M ≥ 1` and `universe M ≥ U + 1`. -Lean reports an universe inconsistency if the universe constraints are inconsistency. For example, it will return an error +Lean reports an universe inconsistency if the universe constraints are inconsistent. For example, it will return an error if execute the command `universe M ≥ U`. We can view universe variables as placeholders, and we can always solve the universe constraints and find and assignment for the universe variables used in our developments. This assignment allows us to produce a Lean specification that is not based on this particular feature. + +Propositional logic +------------------- + +To manipulate formulas with a richer logical structure, it is important to master the notation Lean uses for building +composite logical expressions out of basic formulas using _logical connectives_. The logical connectives (`and`, `or`, `not`, etc) +are defined in the Lean [kernel](../../src/builtin/kernel.lean). The kernel also defines notational convention for rewriting formulas +in a natural way. Here is a table showing the notation for the so called propositional (or Boolean) connectives. + + +| Ascii | Ascii alt. | Unicode | Definition | +|-------|--------------|---------|--------------| +| true | | ⊤ | true | +| false | | ⊥ | false | +| not | | ¬ | not | +| /\ | && | ∧ | and | +| ‌\/ | || | ∨ | or | +| -> | | → | implies | +| <-> | | ↔ | iff | + +`true` and `false` are logical constants to denote the true and false propositions. Logical negation is a unary operator just like +arithmetical negation on numbers. The other connectives are all binary operators. The meaning of the operators is the usual one. +The table above makes clear that Lean supports unicode characters. We can use Ascii or/and unicode versions. +Here is a simple example using the connectives above. + +```lean + variable q : Bool + check p → q → p ∧ q + check ¬ p → p ↔ false + check p ∨ q → q ∨ p + -- Ascii version + check p -> q -> p && q + check not p -> p <-> false + check p || q -> q \/ p +``` + +Depending on the platform, Lean uses unicode characters by default when printing expressions. The following commands can be used to +change this behavior. + +```lean + set_option pp::unicode false + check p → q → p ∧ q + set_option pp::unicode true + check p → q → p ∧ q +``` + +Note that, it may seem that the symbols `->` and `→` are overloaded, and Lean uses them to represent Boolean implication and the type +of functions. Actually, they are not overloaded, they are the same symbols. In Lean, the Boolean `p → q` expression is also the type +of the functions that given a proof for `p`, returns a proof for `q`. This is very convenient for writing proofs. + +```lean + -- Hpq is a function that takes a proof for p and returns a proof for q + axiom Hpq : p → q + -- Hq is a proof/certificate for p + axiom Hp : p + -- The expression Hpq Hp is a proof/certificate for q + check Hpq Hp +``` + +In composite expressions, the precedences of the various binary +connectives are in order of the above table, with `and` being the +strongest and `iff` the weakest. For example, `a ∧ b → c ∨ d ∧ e` +means `(a ∧ b) → (c ∨ (d ∧ e))`. All of them are right-associative. +So, `p ∧ q ∧ r` means `p ∧ (q ∧ r)`. The actual precedence and fixity of all +logical connectives is defined in the Lean [kernel definition file](../../src/builtin/kernel.lean). + +Finally, `not`, `and`, `or` and `iff` are the actual names used when +defining the Boolean connectives. They can be used as any other function. + +```lean + check and + check or + check not +``` + +Lean supports _currying_ `and true` is a function from `Bool` to `Bool`. + +```lean + check and true + definition id := and true + eval id true + eval id false +``` + +Functions +--------- + +There are many variable-binding constructs in mathematics. Lean expresses +all of them using just one _abstraction_, which is a converse operation to +function application. Given a variable `x`, a type `A`, and a term `t` that +may or may not contain `x`, one can construct the so-called _lambda abstraction_ +`fun x : A, t`, or using unicode notation `λ x : A, t`. Here is some simple +examples. + +```lean + check fun x : Nat, x + 1 + check fun x y : Nat, x + 2 * y + check fun x y : Bool, not (x ∧ y) + check λ x : Nat, x + 1 + check λ (x : Nat) (p : Bool), x = 0 ∨ p +``` + +In many cases, Lean can automatically infer the type of the variable. Actually, +In all examples above, the type can be automatically inferred. + +```lean + check fun x, x + 1 + check fun x y, x + 2 * y + check fun x y, not (x ∧ y) + check λ x, x + 1 + check λ x p, x = 0 ∨ p +``` + +However, Lean will complain that it cannot infer the type of the +variable in `fun x, x` because any type would work in this example. + +The following example shows how to use lambda abstractions in +function applications + +```lean + eval (fun x y, x + 2 * y) 1 + eval (fun x y, x + 2 * y) 1 2 + eval (fun x y, not (x ∧ y)) true false +``` + +Lambda abstractions are also used to create proofs for propositions of the form `A → B`. +This should be natural since Lean views `A → B` as the type of functions that given +a proof for `A` returns a proof for `B`. +For example, a proof for `p → p` is just `fun H : p, H` (the identity function). + +```lean + check fun H : p, H +``` + +Definitional equality +--------------------- + +Recall that the command `eval t` computes a normal form for the term `t`. +In Lean, we say two terms are _definitionally equal_ if the have the same +normal proof. For example, the terms `(λ x : Nat, x + 1) a` and `a + 1` +are definitionally equal. The Lean type/proof checker uses the normalizer/evaluator when +checking types/proofs. So, we can prove that two definitionally equal terms +are equal using just `refl`. Here is a simple example. + +```lean + theorem def_eq_th (a : Nat) : ((λ x : Nat, x + 1) a) = a + 1 + := refl (a+1) +``` + +Provable equality +----------------- + +In the previous examples, we have used `nat_trans3 x y z w Hxy Hzy Hzw` +to show that `x = w`. In this case, `x` and `w` are not definitionally equal, +but they are provably equal in the environment that contains `nat_trans3` and +axioms `Hxy`, `Hzy` and `Hzw`. + +Proving +------- + +The Lean kernel contains basic theorems for creating proof terms. The +basic theorems are useful for creating manual proofs. The are also the +basic building blocks used by all automated proof engines available in +Lean. The theorems can be broken into three different categories: +introduction, elimination, and rewriting. First, we cover the introduction +and elimination theorems for the basic Boolean connectives. + +### And (conjuction) + +The expression `and_intro H1 H2` creates a proof for `a ∧ b` using proofs +`H1 : a` and `H2 : b`. We say `and_intro` is the _and-introduction_ operation. +In the following example we use `and_intro` for creating a proof for +`p → q → p ∧ q`. + +```lean + check fun (Hp : p) (Hq : q), and_intro Hp Hq +``` + +The expression `and_eliml H` creates a proof `a` from a proof `H : a ∧ b`. +Similarly `and_elimr H` is a proof for `b`. We say they are the _left/right and-elimination_. + +```lean + -- Proof for p ∧ q → p + check fun H : p ∧ q, and_eliml H + -- Proof for p ∧ q → q + check fun H : p ∧ q, and_elimr H +``` + +Now, we prove `p ∧ q → q ∧ p` with the following simple proof term. + +```lean + check fun H : p ∧ q, and_intro (and_elimr H) (and_eliml H) +``` + +Note that the proof term is very similar to a function that just swaps the +elements of a pair. + +### Or (disjuction) + +The expression `or_introl H1 b` creates a proof for `a ∨ b` using a proof `H1 : a`. +Similarly, `or_intror a H2` creates a proof for `a ∨ b` using a proof `H2 : b`. +We say they are the _left/right or-introduction_. + +```lean + -- Proof for p → p ∨ q + check fun H : p, or_introl H q + -- Proof for q → p ∨ q + check fun H : q, or_intror p H +``` + +The or-elimination rule is slightly more complicated. The basic idea is the +following, we can prove `c` from `a ∨ b`, by showing we can prove `c` +by assuming `a` or by assuming `b`. It is essentially a proof by cases. +`or_elim Hab Hac Hbc` takes three arguments `Hab : a ∨ b`, `Hac : a → c` and `Hbc : b → c` and produces a proof for `c`. +In the following example, we use `or_elim` to prove that `p v q → q ∨ p`. + +```lean + check fun H : p ∨ q, + or_elim H + (fun Hp : p, or_intror q Hp) + (fun Hq : q, or_introl Hq p) +``` + +### Not (negation) + +`not_intro H` produces a proof for `¬ a` from `H : a → false`. That is, +we obtain `¬ a` if we can derive `false` from `a`. The expression +`absurd_elim b Ha Hna` produces a proof for `b` from `Ha : a` and `Hna : ¬ a`. +That is, we can deduce anything if we have `a` and `¬ a`. +We now use `not_intro` and `absurd_elim` to produce a proof term for +`(a → b) → ¬ b → ¬ a` + +```lean + variables a b : Bool + check fun (Hab : a → b) (Hnb : ¬ b), + not_intro (fun Ha : a, absurd_elim false (Hab Ha) Hnb) +``` + +Here is the proof term for `¬ a → b → (b → a) → c` + +```lean + variable c : Bool + check fun (Hna : ¬ a) (Hb : b) (Hba : b → a), + absurd_elim c (Hba Hb) Hna +``` + +### Iff (if-and-only-if) + +The expression `iff_intro H1 H2` produces a proof for `a ↔ b` from `H1 : a → b` and `H2 : b → a`. +`iff_eliml H` produces a proof for `a → b` from `H : a ↔ b`. Similarly, +`iff_elimr H` produces a proof for `b → a` from `H : a ↔ b`. +Note that, in Lean, `a ↔ b` is definitionally equal to `a = b` when `a` and `b` have type `Bool`. +Here is the proof term for `a ∧ b ↔ b ∧ a` + +```lean + check iff_intro (fun H : a ∧ b, and_intro (and_elimr H) (and_eliml H)) + (fun H : b ∧ a, and_intro (and_elimr H) (and_eliml H)) +``` + +### True and False + +The expression `trivial` is a proof term for `true`, and `false_elim a H` +produces a proof for `a` from `H : false`. + +Other basic operators used in proof construction are `eqt_intro`, `eqt_elim`, `eqf_intro` and `eqf_elim`. +`eqt_intro H` produces a proof for `a ↔ true` from `H : a`. +`eqt_elim H` produces a proof for `a` from `H : a ↔ true`. +`eqf_intro H` produces a proof for `a ↔ false` from `H : ¬ a`. +`eqf_elim H` produces a proof for `¬ a` from `H : a ↔ false`. + +```lean + check @eqt_intro + check @eqt_elim + check @eqf_intro + check @eqf_elim +``` + +### Rewrite rules + +The Lean kernel also contains many theorems that are meant to be used as rewriting/simplification rules. +The conclusion of these theorems is of the form `t = s` or `t ↔ s`. For example, `and_id a` is proof term for +`a ∧ a ↔ a`. The Lean simplifier can use these theorems to automatically create proof terms for us. +The expression `(by simp [rule-set])` is similar to `_`, but it tells Lean to synthesize the proof term using the simplifier +using the rewrite rule set named `[rule-set]`. In the following example, we create a simple rewrite rule set +and use it to prove a theorem that would be quite tedious to prove by hand. + +```lean + -- import module that defines several tactics/strategies including "simp" + import tactic + -- create a rewrite rule set with name 'simple' + rewrite_set simple + -- add some theorems to the rewrite rule set 'simple' + add_rewrite and_id and_truer and_truel and_comm and_assoc and_left_comm iff_id : simple + theorem th1 (a b : Bool) : a ∧ b ∧ true ∧ b ∧ true ∧ b ↔ a ∧ b + := (by simp simple) +``` + +In Lean, we can combine manual and automated proofs in a natural way. We can manually write the proof +skeleton and use the `by` construct to invoke automated proof engines like the simplifier for filling the +tedious steps. Here is a very simple example. + +```lean + theorem th2 (a b : Bool) : a ∧ b ↔ b ∧ a + := iff_intro + (fun H : a ∧ b, (by simp simple)) + (fun H : b ∧ a, (by simp simple)) +``` diff --git a/src/builtin/kernel.lean b/src/builtin/kernel.lean index 93c9252cbe..35111d0b1d 100644 --- a/src/builtin/kernel.lean +++ b/src/builtin/kernel.lean @@ -242,6 +242,12 @@ theorem boolext {a b : Bool} (Hab : a → b) (Hba : b → a) : a = b theorem iff_intro {a b : Bool} (Hab : a → b) (Hba : b → a) : a ↔ b := boolext Hab Hba +theorem iff_eliml {a b : Bool} (H : a ↔ b) : a → b +:= (λ Ha : a, eqmp H Ha) + +theorem iff_elimr {a b : Bool} (H : a ↔ b) : b → a +:= (λ Hb : b, eqmpr H Hb) + theorem skolem_th {A : TypeU} {B : A → TypeU} {P : ∀ x : A, B x → Bool} : (∀ x, ∃ y, P x y) ↔ ∃ f, (∀ x, P x (f x)) := iff_intro @@ -264,6 +270,9 @@ theorem neq_elim {A : TypeU} {a b : A} (H : a ≠ b) : a = b ↔ false theorem eq_id {A : TypeU} (a : A) : (a = a) ↔ true := eqt_intro (refl a) +theorem iff_id (a : Bool) : (a ↔ a) ↔ true +:= eqt_intro (refl a) + theorem or_comm (a b : Bool) : (a ∨ b) = (b ∨ a) := boolext (assume H, or_elim H (λ H1, or_intror b H1) (λ H2, or_introl H2 a)) (assume H, or_elim H (λ H1, or_intror a H1) (λ H2, or_introl H2 b)) diff --git a/src/builtin/obj/kernel.olean b/src/builtin/obj/kernel.olean index 9eb02226890703ab1f5b10d08a2239d43d896108..6ded4aa9261e367c7dc6f4ad3410f481e6193ae9 100644 GIT binary patch delta 7708 zcmai233yf25x(c%ckfNYLkQ%BY-AyM#Dwe#TgW3D*+_|mkg!NdLP#Kx1jM+|*2bk) zMT_E4TU%@kMHF}If=Y@XQu}GEwIZ~r*h<~1whC42_gT=Mf6jgHzQlfQzVA)`GiPSb zoS8Xu?!Eio5m<~L7+SCC(tbxzf8W3sdbl#7RDWO2h`ns<`%qA3x4ZCW3EAu# z@HFpqLsFq>FszH4Xh&B6lv^>A$VLdTo#9T3$?g?j(zmkPb;C=qWzP~jD0)Vv_vesN z3+<-WGvkIgyT=Q1gfTb=eOkJ-Ru43QcAElI>&NsKz$ojV}vXhL3=Xr#G$$)bst=dH>7 z6$`W8As0T)Fl545MW^!O#47qCFMDD)=4@F4g#bo3mE_kHGy(4f!A^``IjvIJfGrq} z%#=ji$>S#4pPwAhTsF59^DR;dB1SvCnV%}UNfgA7gJGi=WCQsN@)H5I1`xOqzD5&m zD)7m@U0aYo4whNU*h-HS%t`qj#-_U;lqws*f8#oeDlC%m2o%<)yaY~|fXURWz$AyFKYaXU*v)>f&11X%Nc*y&t7zo(@|WiyV0<77GA)Gx=7 zlWgn(vf-0nWfI05t1P^L=2-~!nNDOEel_%WJYTWAq0 zlBwb#y;pMa@H;HeZoKQl_ZWseGG38m<5)1{ueeSj?Z#1M6*^o7DWS2b1XJ}fS1D{K zvAh+fB_)klS#^Xyo;hXsSV+S$6B>_QM%C3(tmVW4Fl?F7Dn^(PGnJ5(Hcp{Sb`7rW z7}|14&lb(16GfBh=8~u;l!y$WB;rHBu;}tQ6x|O)`&L_a6jh*Y#N30Qe*>Yo;O7l zP~W@-B0vw!+fy(Jg51va$$*>}JqFO54tf?O)wu)oXu7g&ZqY)?5)UGSdMu`u{uDr^ z9|y>{iXJbKXCZx9mZV3k%TD*v^gyFG5i-i#B)TGyAr8=A-HaL+o^vL|mGlOSlsB1dUEb#Oit~JvYCBqwg#|9ZTDF zeBs2>-GMB7kAqJH=6G*c80PC~q`X>Od259)X$BTjp69qQ7gASJVTCX9HnnJmvuHN0 zt0;hX`ul7z3rZ^G9K(E!mAwM#PAUylM$tbjeqeD&wkd6X678={FWMc_7Mv>;;F+%W zEEmp}(6gJqtW1r3N_ms#cvC{rRi z!1?u@#u%NUAHZ{(?3!MAItOdw#Ui@CCQ07=ch)SJ)`D4O3>U7ZjI{#txikzKR~s+B zAb)L%SVAjnw`Z=zq~Jv_1k7f*3NVRbyF}(BnoyT)n~1yVqmsHTpMxP6d_>Y$(3ZMo zX?$fXi`|&cK3@|389*2`{q#Xy^5jfEHl|mDt*w?nGlvrE)5Hu4)W=EMR-Ym=>C*Z< z;ipp@V(7{GiKXiyt1R~cDqlB9WctUHzt#zEnaWp}ldpA@*ie-=AZHvagMefGtE2BU zq{x8&v|(;Ro#kBIXzXSw2Shy%GQ5cO8E%0<9oY+0Bb(K#{m!bJsD5FYx0S0GCt4Tu zaBU3jUFa{n1o|ppmjbE{T?VMC8&3^pYo?_7#o(euROGwJYz&BAs%}gZTdAipe-a+a zde|eg*DvLaCfe6{!}La|U?Fo8AHr)T6k9PKl0-e=%X_5t8#!W#uKvb1=bJISp(`<~ ze7g!z`F1s+^6eUl%xy@n*e;1KFz%$%MOC7cu2|GBh(1`9AV$b+$`!*@+!R=XN;J2z z`5Ps4%-;m4%zq!y%YMEkk=bf710)aQPUki;Tlob-AENf`q$qQn8Vx%gcH1N71v5qF z4ydUe+zRE#c;O!aKFRP$fQPATake-@H!V(yel}F9DndtSWN}LDOYleB4Z?AI8EQx9 z%;F5|4}ia?#OB2obDyG%nx~3e=;r2tI7Tlvr_TL_lyExDUKifUFw2ntbbbI;kN>z% zjL*RpZ`1T8wTs$ARm0B!qJ#aui?tcTE64nPhFKW%Qvl|*X!$dCvBeR3a>-TlYMs}T zu;gCMsm^wv3-5Q~11`iXk9n3?dl>LsDCHWOjL`$;mvmQ)U-Zz6Eor)C(&?6(ax22p zyX2hn+5jJ{$WVZJ!&U^Qc_wP?3=J)$FD4Sl_!TLcT8Av#j=^p~qvvZIHQUm1!yxS6X7F+C9$LJ7d-a!Gy3fcNr{a&e@YgPU)`h>3&|1oB&jGek+KL4E38HL8 zmTuX!ZbgQzyoWe|#{ zFIFZu!yJcI*EolKc&&Cgu8N}p2yI>!2Uqo4Ih6O(*xf;hqm%akqEkV4T$t=vZt#YR zq^^nzS5^&7;fdPn58FT|BHyR7zz3%Dzj&ZJ3s2)twQ?Y%5eSmYr-xUv3gyTu8huWb z4<5{1LRYNHk6#0br&X&*60IXxW`|{&`RKJ(1&i_gWq!qla}*+~!@lCeV=g@I!aquA z;p0fh8V;vyv3$_)p@L2yZEBB*;RX5SGW4+ZGTqo-Gkn%^way}Z{H@QxJ!N#WBkEHD z!`Csdd^+jEH(dB<%&S)a7lsI!bu0Rd`UtTT2qDpyGLtS?ohZBhrjB&lzWO}zD&4WV zdAJ2Wb#+6^Y6JNRul`ps)aq}!@NE~qYbY_ zmZL`l9eLsu?dn*-`LK4e8FeKx{5!OiBmZ#WM=tzW!cqA+tCoLN<|BRr*H0)7AJE}0 z9}RRCjz1TcigR>tXDXGiN$7PJ`pmWdFA2?a?8)a0xpMg!gQ=N_to|qC;ihGZMr52vcl4}J zw>duijBX@DNawKfF;P)VrNWId!$^pY0NPocn`a;kQJZHFaC;o0VWQ`0DVWl3WGIQ9 zIc6LY+)_%0oHlkrFc&0+-}H?0fStn%L=SDWVps|hwxfcZm`cZc`||84b{eLfMEL>v zEx~|O;fX4v{&iV)8QAhoX4ks7Vg9zX5Mmu5xk2C5$LbOAM$M|c20~)Wlq<$#Hj2Y! zbER-$@Mm0u4TjC|UV|;dNTFi@i zpI;oJ1AWQfb&%rEHpU2@>YGxyJX12l-UxjhrxJ*v0PQXWOL>K~o3V7LKbFcjOsXlC zLv1IE^V&Nx=2p#bUFzE~Do@wg2JabTdp#t%h-^B%F`gdW&^c`xc&gIyOy*=twKC3M z87ghn)pE*S4sy+yO5+*a5%zNR3b#UHwTyig*sZ~osH#H49931hw0om3hS^+3%YtPz zmwvl(QzQDFy^LL{fT}w4m4K?0ssO{z{B0H(FlE9mGd6hUZ=>(_7u#lxWZK;_oKwUd z^vC|5;oTgjrceUJR;qXhOoxxi(7xSfbMhM9sW2Y>%) zBkJ742t73rRq#VZm756rXU2w1sB-uz?BMGW9&y{vUxCYZt(LIBi8GIU4xi+$rB#w<>cFO6q!Oh7s zx^l{ZzLOc`%gIa|N~iH<-U_=`A*XCqoPBgm6@>|vg@pbzR!DwEitlGjT&w6!_6fw* zzFrbeiTwu*Uvp~?*Q1V|2OEj%W#!C4{7o))?wIa_r3o+03L0#Sr7Jd1D{~TpwKP2cD_`y|Gl@@Ib*jCKok HT~zZQGW*la delta 7730 zcmbVRdw3Pq5#O_WcQ?vKh$P%3KyE^EB?)i$e1bIsg1VP@!Xsg(-2CGnG z`9L~STR~JPh@i!milWu}tdA-J{jB%^t2}(mOHmZC=Qn5X-Eh_ZQNAy8e`n5|nK?6a z=Ik!3j)+YM#lvgT>A{RP->sVb*UywhbOE+7yo~~bXNk{f`QR2^|CT--JXHLe24)WT z{thxG%iKweGE2m2+L~G6UE{LX(y7b|;x1~;Y8Y`Z*h=|*fHp5&59npMK_c-?s)3)o zz!uv;?Yaf+Ji3S8&MJ!A2&~j>0<_hF)s&H)NTaeY)E9M-D2$^$*@5KE5Ks<2!0-}D z^@Ea#Vo8i_^5rZL*|an#UF6fYoJ3JbyK>qp|IEVd)L&e|dN^FbOhzJtewsnRDYJCB*qdDr9!3jeoSc|5Icpd;#qp7pmgxd;F#Ejk)C4e*JG%e7;@3t za7cr1#&XIV5*+p_#%6@IRhVaagEid@A>>3el&zQOp&@zRUEnyj=#wF%lXo)%*2Er$ z;q43L%~(fM3Y#<6fopJWb7s7}`3+crdeKz6n7NVOEUXH=0dBWYK8$fVln*aan!n&%LjewCMtkV*u&2Cccjgpe$#!K|suwjAs zu(Vr9_hK9l>0Y&2sx3lDXB9ORA7uH6GC@QQwNe%3>yXk65T_^)&?iOZfy3Z*vvvq$ zPbdP1RD7thc;2v&Su(=T7m{hHHC&DdcsYn;7Nq4 zm_^T(6vc@%EMrP4&W6SHSUh<&y}Z9}Y9uoH>G}n< zw!FdH3*vlp=)LJ&RT9+6vmIBFW50t0Y0>mWWs&y_h2_|jLz}9TX?sP==$bH-?**+V z`x1*)N@HIa`mnSH=Rtca1r#oGX?vz}!RZ&#s;W2pf$E(YR4;+0}nAzPcJ~T>Wl9YFpCu8YV5nc)0!k%9$uj1INMA|<* zmsX6paFFU1Y$6?cRK4-Wd0WavDx8KqwTxJ8f zS8%XIo-UeGl@zsJIW&+RN~0}RwcadOFk4z|5m7X?db4kc%SNR+s)ka(U_#XMN=qhd zDWD0#tOC!i5e}(57P(7{U3jU4o?B^0FjEYpgTcu|OEITPuMF^7jzu}3I={yy^6bMH zJ!w9GXCHOc%qrS%>U<4qb;y9e6jS4PIk#mz1E{{q2f*t*9_c02dt`O#NX#m`wSdYl zcWT$J9=_AruD%e4JRi{QBZr6@dST>>K}}dI*yw1$42EL>`!j5o$n!1TP@8Cbz5_l> z_td7xIv8@H=Qh2O_Sa7IP5@77oJf^*G5I}Jy<5%&?hTi}mMtaCUI9b?=)inV?y$;z>CnXK`%IfgFe{-32oNm62Hx$bpBUbIrxX zC5XlPuOLvY>`!C+GicptAHC8L5M^|%p}KSq7OPCo1yqXX0ji^c+?i#AB-O707fI&$ zn|0Jas!TM|pGGB%1+;rq&c#i##%5j(DYGdcsZmJLja`@EdCx>_%!%-oYfUW1m}BP$ z(^yYWH)e|2?4GA-M!Dwj?Qk@(#EC{qLw~t zn&1By=i5||qt2rewU5pc*GQXXV{v}W4z}4Tp<{Cipt5-rAeRF_+nZ$;GeEeMYMqP3 zEW3njYBnvY@%7^4VRk6iHBR@xaeMoiLNRD5)~eVqlgPZAt#<+5$8b5|1N3ThhS*A9 zH~XU>!an(FR>f~C4I1nBJ&GN2jVkU=EZZ88H%&||7HEWd4)|l3+Cj_4j!HE2!f@?&8+cZsWFC%#x3YP7{F8l26jpwTO47G5ltlA#5H|tBS@Rgi z1_H%N)V%85;S0%-tt*^-C42&01Di0<(9#Ko!3QN&>kPKzjw9`yIA4{s2%5g7?#6DvA$CS(kI#~nqblcS?K zekOu#LEZ|`6_azaaU`sPAb2RU`k?@U3T3@A@{lSxvmiW<9uXH*;+%^C;)>)C&+ z7D7K(hFqXlE!=fKneZB?K%uD>B!;%N#9Q%z3AC#vUbN84NjdTLVE8~9CDB?#1^0+7 zxZs!)$ud9W()kCbRabt|g)h1AWf#68p;dx-wq42G!)Zu~zK$-M**})Mw)3eYWbOqz zbwzOIAh^os2x0QJaQL=8Jds_?T-SGCb z6gu5{k$8=wrZsn#!18qNC>9>Zt()20za@0cz3IYzE_};{Z%b&c=4I~!ma9EK0tqV! z%4PZ+AU}wg3yuRs`=(`!H^`n|%^|mLVKwhTN`?GCE_~mGAGq+Kgy)6)kTU-ot(hL* z>lY9VKX@OY=cd>6JlrkVhpBH{Qs)s@-G?sx$b}!f@DmBm!|dj#47mhRFX~*H-1j$Q zjBa2BL!A-l$>JbzJzF<~L=2gf9c_aoJ+XmsFy#)gz(d;bqWZfN1?Mk%S*Tt>XxX`f`SDuPv0h z$FFsqzMq*jbbuVTW9)ovLu+#1<*d_kdLhq?J^?wy--E5w)HW-ppLH_y;!}qdxJ^sW zKR7E@ev;iY%NJ#xR_o~4ET7OR>Z;kD7C(3JBe{WVN0XmAr0PC^98e<$us{S& z_m;#u2^4YpsTscIPGaLGx{BuKNQ8^t?iCt0t5aYd3%T#dfj4f(A~Zo6353?*i`qFb zVB4-3H_Q`G3o)Xpa`v2T>jdv24x;>^ZlL9<7XpKyN8PO0sr2UT^rTdHt3G8efUL~T z_4swZmT#n_IRnH7Dxc$<7zj_fYtTWpRvvEzM4ei=?NqwehtdrgN6v&i_tArMmNny1 zz;QVRP~`x-?N&&3xdn#JlvCxtAA8PWD)iOQE~ldl;%V*N$#$)Bmd?x#bh3+RL@KWA zo%)o3V``6v3g=Y|u$!b)v3BJk$?x`Nd6r!q0%@FWTm6p(Zy0S(c_qJPTn7nSThoKK z&Wjd<=*fBh?DgO&8v%)ouy^(t%y63wwJjrAhAENK=8v^1FzKbNxyhXo)j3yA*p(pj zeryJ<-L6!xc6{Hl340FMWue@vLOdXO=M`cy7?FkOHCPUnXjhP!A5Xyrtqtf;c7-Xa z!EsTA$cLKWOpT#(s(V&%