From 5b5cebe750874139acc6974aaeda7603249ef110 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 3 Jan 2014 10:33:57 -0800 Subject: [PATCH] refactor(builtin/Nat): use obtain-from instead of ExistsElim, and use more user-friendly argument order for Induction Signed-off-by: Leonardo de Moura --- src/builtin/Nat.lean | 282 ++++++++++++++++++-------------------- src/builtin/kernel.lean | 2 + src/builtin/obj/Nat.olean | Bin 15930 -> 15904 bytes 3 files changed, 139 insertions(+), 145 deletions(-) diff --git a/src/builtin/Nat.lean b/src/builtin/Nat.lean index 50c0867b9..058eea4dc 100644 --- a/src/builtin/Nat.lean +++ b/src/builtin/Nat.lean @@ -37,22 +37,20 @@ Axiom PlusSucc (a b : Nat) : a + (b + 1) = (a + b) + 1. Axiom MulZero (a : Nat) : a * 0 = 0. Axiom MulSucc (a b : Nat) : a * (b + 1) = a * b + a. Axiom LeDef (a b : Nat) : a ≤ b ⇔ ∃ c, a + c = b. -Axiom Induction {P : Nat → Bool} (Hb : P 0) (iH : Π (n : Nat) (H : P n), P (n + 1)) (a : Nat) : P a. +Axiom Induction {P : Nat → Bool} (a : Nat) (H1 : P 0) (H2 : Π (n : Nat) (iH : P n), P (n + 1)) : P a. Theorem ZeroNeOne : 0 ≠ 1 := Trivial. Theorem NeZeroPred' (a : Nat) : a ≠ 0 ⇒ ∃ b, b + 1 = a -:= Induction (show 0 ≠ 0 ⇒ ∃ b, b + 1 = 0, - assume H : 0 ≠ 0, FalseElim (∃ b, b + 1 = 0) H) - (λ (n : Nat) (iH : n ≠ 0 ⇒ ∃ b, b + 1 = n), - assume H : n + 1 ≠ 0, - DisjCases (EM (n = 0)) - (λ Heq0 : n = 0, ExistsIntro 0 (calc 0 + 1 = n + 1 : { Symm Heq0 })) - (λ Hne0 : n ≠ 0, - ExistsElim (MP iH Hne0) - (λ (w : Nat) (Hw : w + 1 = n), - ExistsIntro (w + 1) (calc w + 1 + 1 = n + 1 : { Hw })))) - a. +:= Induction a + (assume H : 0 ≠ 0, FalseElim (∃ b, b + 1 = 0) H) + (λ (n : Nat) (iH : n ≠ 0 ⇒ ∃ b, b + 1 = n), + assume H : n + 1 ≠ 0, + DisjCases (EM (n = 0)) + (λ Heq0 : n = 0, ExistsIntro 0 (calc 0 + 1 = n + 1 : { Symm Heq0 })) + (λ Hne0 : n ≠ 0, + obtain (w : Nat) (Hw : w + 1 = n), from (MP iH Hne0), + ExistsIntro (w + 1) (calc w + 1 + 1 = n + 1 : { Hw }))). Theorem NeZeroPred {a : Nat} (H : a ≠ 0) : ∃ b, b + 1 = a := MP (NeZeroPred' a) H. @@ -60,107 +58,106 @@ Theorem NeZeroPred {a : Nat} (H : a ≠ 0) : ∃ b, b + 1 = a Theorem Destruct {B : Bool} {a : Nat} (H1: a = 0 → B) (H2 : Π n, a = n + 1 → B) : B := DisjCases (EM (a = 0)) (λ Heq0 : a = 0, H1 Heq0) - (λ Hne0 : a ≠ 0, ExistsElim (NeZeroPred Hne0) - (λ (w : Nat) (Hw : w + 1 = a), H2 w (Symm Hw))). + (λ Hne0 : a ≠ 0, obtain (w : Nat) (Hw : w + 1 = a), from (NeZeroPred Hne0), + H2 w (Symm Hw)). Theorem ZeroPlus (a : Nat) : 0 + a = a -:= Induction (show 0 + 0 = 0, Trivial) - (λ (n : Nat) (iH : 0 + n = n), - calc 0 + (n + 1) = (0 + n) + 1 : PlusSucc 0 n - ... = n + 1 : { iH }) - a. +:= Induction a + (show 0 + 0 = 0, Trivial) + (λ (n : Nat) (iH : 0 + n = n), + calc 0 + (n + 1) = (0 + n) + 1 : PlusSucc 0 n + ... = n + 1 : { iH }). Theorem SuccPlus (a b : Nat) : (a + 1) + b = (a + b) + 1 -:= Induction (calc (a + 1) + 0 = a + 1 : PlusZero (a + 1) - ... = (a + 0) + 1 : { Symm (PlusZero a) }) - (λ (n : Nat) (iH : (a + 1) + n = (a + n) + 1), - calc (a + 1) + (n + 1) = ((a + 1) + n) + 1 : PlusSucc (a + 1) n - ... = ((a + n) + 1) + 1 : { iH } - ... = (a + (n + 1)) + 1 : { show (a + n) + 1 = a + (n + 1), Symm (PlusSucc a n) }) - b. +:= Induction b + (calc (a + 1) + 0 = a + 1 : PlusZero (a + 1) + ... = (a + 0) + 1 : { Symm (PlusZero a) }) + (λ (n : Nat) (iH : (a + 1) + n = (a + n) + 1), + calc (a + 1) + (n + 1) = ((a + 1) + n) + 1 : PlusSucc (a + 1) n + ... = ((a + n) + 1) + 1 : { iH } + ... = (a + (n + 1)) + 1 : { show (a + n) + 1 = a + (n + 1), Symm (PlusSucc a n) }). Theorem PlusComm (a b : Nat) : a + b = b + a -:= Induction (calc a + 0 = a : PlusZero a - ... = 0 + a : Symm (ZeroPlus a)) - (λ (n : Nat) (iH : a + n = n + a), - calc a + (n + 1) = (a + n) + 1 : PlusSucc a n - ... = (n + a) + 1 : { iH } - ... = (n + 1) + a : Symm (SuccPlus n a)) - b. +:= Induction b + (calc a + 0 = a : PlusZero a + ... = 0 + a : Symm (ZeroPlus a)) + (λ (n : Nat) (iH : a + n = n + a), + calc a + (n + 1) = (a + n) + 1 : PlusSucc a n + ... = (n + a) + 1 : { iH } + ... = (n + 1) + a : Symm (SuccPlus n a)). Theorem PlusAssoc (a b c : Nat) : a + (b + c) = (a + b) + c -:= Induction (calc 0 + (b + c) = b + c : ZeroPlus (b + c) - ... = (0 + b) + c : { Symm (ZeroPlus b) }) - (λ (n : Nat) (iH : n + (b + c) = (n + b) + c), - calc (n + 1) + (b + c) = (n + (b + c)) + 1 : SuccPlus n (b + c) - ... = ((n + b) + c) + 1 : { iH } - ... = ((n + b) + 1) + c : Symm (SuccPlus (n + b) c) - ... = ((n + 1) + b) + c : { show (n + b) + 1 = (n + 1) + b, Symm (SuccPlus n b) }) - a. +:= Induction a + (calc 0 + (b + c) = b + c : ZeroPlus (b + c) + ... = (0 + b) + c : { Symm (ZeroPlus b) }) + (λ (n : Nat) (iH : n + (b + c) = (n + b) + c), + calc (n + 1) + (b + c) = (n + (b + c)) + 1 : SuccPlus n (b + c) + ... = ((n + b) + c) + 1 : { iH } + ... = ((n + b) + 1) + c : Symm (SuccPlus (n + b) c) + ... = ((n + 1) + b) + c : { show (n + b) + 1 = (n + 1) + b, Symm (SuccPlus n b) }). Theorem ZeroMul (a : Nat) : 0 * a = 0 -:= Induction (show 0 * 0 = 0, Trivial) - (λ (n : Nat) (iH : 0 * n = 0), - calc 0 * (n + 1) = (0 * n) + 0 : MulSucc 0 n - ... = 0 + 0 : { iH } - ... = 0 : Trivial) - a. +:= Induction a + (show 0 * 0 = 0, Trivial) + (λ (n : Nat) (iH : 0 * n = 0), + calc 0 * (n + 1) = (0 * n) + 0 : MulSucc 0 n + ... = 0 + 0 : { iH } + ... = 0 : Trivial). Theorem SuccMul (a b : Nat) : (a + 1) * b = a * b + b -:= Induction (calc (a + 1) * 0 = 0 : MulZero (a + 1) - ... = a * 0 : Symm (MulZero a) - ... = a * 0 + 0 : Symm (PlusZero (a * 0))) - (λ (n : Nat) (iH : (a + 1) * n = a * n + n), - calc (a + 1) * (n + 1) = (a + 1) * n + (a + 1) : MulSucc (a + 1) n - ... = a * n + n + (a + 1) : { iH } - ... = a * n + n + a + 1 : PlusAssoc (a * n + n) a 1 - ... = a * n + (n + a) + 1 : { show a * n + n + a = a * n + (n + a), Symm (PlusAssoc (a * n) n a) } - ... = a * n + (a + n) + 1 : { PlusComm n a } - ... = a * n + a + n + 1 : { PlusAssoc (a * n) a n } - ... = a * (n + 1) + n + 1 : { Symm (MulSucc a n) } - ... = a * (n + 1) + (n + 1) : Symm (PlusAssoc (a * (n + 1)) n 1)) - b. +:= Induction b + (calc (a + 1) * 0 = 0 : MulZero (a + 1) + ... = a * 0 : Symm (MulZero a) + ... = a * 0 + 0 : Symm (PlusZero (a * 0))) + (λ (n : Nat) (iH : (a + 1) * n = a * n + n), + calc (a + 1) * (n + 1) = (a + 1) * n + (a + 1) : MulSucc (a + 1) n + ... = a * n + n + (a + 1) : { iH } + ... = a * n + n + a + 1 : PlusAssoc (a * n + n) a 1 + ... = a * n + (n + a) + 1 : { show a * n + n + a = a * n + (n + a), Symm (PlusAssoc (a * n) n a) } + ... = a * n + (a + n) + 1 : { PlusComm n a } + ... = a * n + a + n + 1 : { PlusAssoc (a * n) a n } + ... = a * (n + 1) + n + 1 : { Symm (MulSucc a n) } + ... = a * (n + 1) + (n + 1) : Symm (PlusAssoc (a * (n + 1)) n 1)). Theorem OneMul (a : Nat) : 1 * a = a -:= Induction (show 1 * 0 = 0, Trivial) - (λ (n : Nat) (iH : 1 * n = n), - calc 1 * (n + 1) = 1 * n + 1 : MulSucc 1 n - ... = n + 1 : { iH }) - a. +:= Induction a + (show 1 * 0 = 0, Trivial) + (λ (n : Nat) (iH : 1 * n = n), + calc 1 * (n + 1) = 1 * n + 1 : MulSucc 1 n + ... = n + 1 : { iH }). Theorem MulOne (a : Nat) : a * 1 = a -:= Induction (show 0 * 1 = 0, Trivial) - (λ (n : Nat) (iH : n * 1 = n), - calc (n + 1) * 1 = n * 1 + 1 : SuccMul n 1 - ... = n + 1 : { iH }) - a. +:= Induction a + (show 0 * 1 = 0, Trivial) + (λ (n : Nat) (iH : n * 1 = n), + calc (n + 1) * 1 = n * 1 + 1 : SuccMul n 1 + ... = n + 1 : { iH }). Theorem MulComm (a b : Nat) : a * b = b * a -:= Induction (calc a * 0 = 0 : MulZero a - ... = 0 * a : Symm (ZeroMul a)) - (λ (n : Nat) (iH : a * n = n * a), - calc a * (n + 1) = a * n + a : MulSucc a n - ... = n * a + a : { iH } - ... = (n + 1) * a : Symm (SuccMul n a)) - b. - +:= Induction b + (calc a * 0 = 0 : MulZero a + ... = 0 * a : Symm (ZeroMul a)) + (λ (n : Nat) (iH : a * n = n * a), + calc a * (n + 1) = a * n + a : MulSucc a n + ... = n * a + a : { iH } + ... = (n + 1) * a : Symm (SuccMul n a)). Theorem Distribute (a b c : Nat) : a * (b + c) = a * b + a * c -:= Induction (calc 0 * (b + c) = 0 : ZeroMul (b + c) - ... = 0 + 0 : Trivial - ... = 0 * b + 0 : { Symm (ZeroMul b) } - ... = 0 * b + 0 * c : { Symm (ZeroMul c) }) - (λ (n : Nat) (iH : n * (b + c) = n * b + n * c), - calc (n + 1) * (b + c) = n * (b + c) + (b + c) : SuccMul n (b + c) - ... = n * b + n * c + (b + c) : { iH } - ... = n * b + n * c + b + c : PlusAssoc (n * b + n * c) b c - ... = n * b + (n * c + b) + c : { Symm (PlusAssoc (n * b) (n * c) b) } - ... = n * b + (b + n * c) + c : { PlusComm (n * c) b } - ... = n * b + b + n * c + c : { PlusAssoc (n * b) b (n * c) } - ... = (n + 1) * b + n * c + c : { Symm (SuccMul n b) } - ... = (n + 1) * b + (n * c + c) : Symm (PlusAssoc ((n + 1) * b) (n * c) c) - ... = (n + 1) * b + (n + 1) * c : { Symm (SuccMul n c) }) - a. +:= Induction a + (calc 0 * (b + c) = 0 : ZeroMul (b + c) + ... = 0 + 0 : Trivial + ... = 0 * b + 0 : { Symm (ZeroMul b) } + ... = 0 * b + 0 * c : { Symm (ZeroMul c) }) + (λ (n : Nat) (iH : n * (b + c) = n * b + n * c), + calc (n + 1) * (b + c) = n * (b + c) + (b + c) : SuccMul n (b + c) + ... = n * b + n * c + (b + c) : { iH } + ... = n * b + n * c + b + c : PlusAssoc (n * b + n * c) b c + ... = n * b + (n * c + b) + c : { Symm (PlusAssoc (n * b) (n * c) b) } + ... = n * b + (b + n * c) + c : { PlusComm (n * c) b } + ... = n * b + b + n * c + c : { PlusAssoc (n * b) b (n * c) } + ... = (n + 1) * b + n * c + c : { Symm (SuccMul n b) } + ... = (n + 1) * b + (n * c + c) : Symm (PlusAssoc ((n + 1) * b) (n * c) c) + ... = (n + 1) * b + (n + 1) * c : { Symm (SuccMul n c) }). Theorem Distribute2 (a b c : Nat) : (a + b) * c = a * c + b * c := calc (a + b) * c = c * (a + b) : MulComm (a + b) c @@ -169,34 +166,34 @@ Theorem Distribute2 (a b c : Nat) : (a + b) * c = a * c + b * c ... = a * c + b * c : { MulComm c b }. Theorem MulAssoc (a b c : Nat) : a * (b * c) = a * b * c -:= Induction (calc 0 * (b * c) = 0 : ZeroMul (b * c) - ... = 0 * c : Symm (ZeroMul c) - ... = (0 * b) * c : { Symm (ZeroMul b) }) - (λ (n : Nat) (iH : n * (b * c) = n * b * c), - calc (n + 1) * (b * c) = n * (b * c) + (b * c) : SuccMul n (b * c) - ... = n * b * c + (b * c) : { iH } - ... = (n * b + b) * c : Symm (Distribute2 (n * b) b c) - ... = (n + 1) * b * c : { Symm (SuccMul n b) }) - a. +:= Induction a + (calc 0 * (b * c) = 0 : ZeroMul (b * c) + ... = 0 * c : Symm (ZeroMul c) + ... = (0 * b) * c : { Symm (ZeroMul b) }) + (λ (n : Nat) (iH : n * (b * c) = n * b * c), + calc (n + 1) * (b * c) = n * (b * c) + (b * c) : SuccMul n (b * c) + ... = n * b * c + (b * c) : { iH } + ... = (n * b + b) * c : Symm (Distribute2 (n * b) b c) + ... = (n + 1) * b * c : { Symm (SuccMul n b) }). Theorem PlusInj' (a b c : Nat) : a + b = a + c ⇒ b = c -:= Induction (assume H : 0 + b = 0 + c, - calc b = 0 + b : Symm (ZeroPlus b) - ... = 0 + c : H - ... = c : ZeroPlus c) - (λ (n : Nat) (iH : n + b = n + c ⇒ b = c), - assume H : n + 1 + b = n + 1 + c, - let L1 : n + b + 1 = n + c + 1 - := (calc n + b + 1 = n + (b + 1) : Symm (PlusAssoc n b 1) - ... = n + (1 + b) : { PlusComm b 1 } - ... = n + 1 + b : PlusAssoc n 1 b - ... = n + 1 + c : H - ... = n + (1 + c) : Symm (PlusAssoc n 1 c) - ... = n + (c + 1) : { PlusComm 1 c } - ... = n + c + 1 : PlusAssoc n c 1), - L2 : n + b = n + c := SuccInj L1 - in MP iH L2) - a. +:= Induction a + (assume H : 0 + b = 0 + c, + calc b = 0 + b : Symm (ZeroPlus b) + ... = 0 + c : H + ... = c : ZeroPlus c) + (λ (n : Nat) (iH : n + b = n + c ⇒ b = c), + assume H : n + 1 + b = n + 1 + c, + let L1 : n + b + 1 = n + c + 1 + := (calc n + b + 1 = n + (b + 1) : Symm (PlusAssoc n b 1) + ... = n + (1 + b) : { PlusComm b 1 } + ... = n + 1 + b : PlusAssoc n 1 b + ... = n + 1 + c : H + ... = n + (1 + c) : Symm (PlusAssoc n 1 c) + ... = n + (c + 1) : { PlusComm 1 c } + ... = n + c + 1 : PlusAssoc n c 1), + L2 : n + b = n + c := SuccInj L1 + in MP iH L2). Theorem PlusInj {a b c : Nat} (H : a + b = a + c) : b = c := MP (PlusInj' a b c) H. @@ -222,36 +219,31 @@ Theorem LeRefl (a : Nat) : a ≤ a := LeIntro (PlusZero a). Theorem LeZero (a : Nat) : 0 ≤ a := LeIntro (ZeroPlus a). Theorem LeTrans {a b c : Nat} (H1 : a ≤ b) (H2 : b ≤ c) : a ≤ c -:= ExistsElim (LeElim H1) - (λ (w1 : Nat) (Hw1 : a + w1 = b), - ExistsElim (LeElim H2) - (λ (w2 : Nat) (Hw2 : b + w2 = c), - LeIntro (calc a + (w1 + w2) = a + w1 + w2 : PlusAssoc a w1 w2 - ... = b + w2 : { Hw1 } - ... = c : Hw2))). +:= obtain (w1 : Nat) (Hw1 : a + w1 = b), from (LeElim H1), + obtain (w2 : Nat) (Hw2 : b + w2 = c), from (LeElim H2), + LeIntro (calc a + (w1 + w2) = a + w1 + w2 : PlusAssoc a w1 w2 + ... = b + w2 : { Hw1 } + ... = c : Hw2). Theorem LeInj {a b : Nat} (H : a ≤ b) (c : Nat) : a + c ≤ b + c -:= ExistsElim (LeElim H) - (λ (w : Nat) (Hw : a + w = b), - LeIntro (calc a + c + w = a + (c + w) : Symm (PlusAssoc a c w) - ... = a + (w + c) : { PlusComm c w } - ... = a + w + c : PlusAssoc a w c - ... = b + c : { Hw })). +:= obtain (w : Nat) (Hw : a + w = b), from (LeElim H), + LeIntro (calc a + c + w = a + (c + w) : Symm (PlusAssoc a c w) + ... = a + (w + c) : { PlusComm c w } + ... = a + w + c : PlusAssoc a w c + ... = b + c : { Hw }). Theorem LeAntiSymm {a b : Nat} (H1 : a ≤ b) (H2 : b ≤ a) : a = b -:= ExistsElim (LeElim H1) - (λ (w1 : Nat) (Hw1 : a + w1 = b), - ExistsElim (LeElim H2) - (λ (w2 : Nat) (Hw2 : b + w2 = a), - let L1 : w1 + w2 = 0 - := PlusInj (calc a + (w1 + w2) = a + w1 + w2 : { PlusAssoc a w1 w2 } - ... = b + w2 : { Hw1 } - ... = a : Hw2 - ... = a + 0 : Symm (PlusZero a)), - L2 : w1 = 0 := PlusEq0 L1 - in calc a = a + 0 : Symm (PlusZero a) - ... = a + w1 : { Symm L2 } - ... = b : Hw1)). +:= obtain (w1 : Nat) (Hw1 : a + w1 = b), from (LeElim H1), + obtain (w2 : Nat) (Hw2 : b + w2 = a), from (LeElim H2), + let L1 : w1 + w2 = 0 + := PlusInj (calc a + (w1 + w2) = a + w1 + w2 : { PlusAssoc a w1 w2 } + ... = b + w2 : { Hw1 } + ... = a : Hw2 + ... = a + 0 : Symm (PlusZero a)), + L2 : w1 = 0 := PlusEq0 L1 + in calc a = a + 0 : Symm (PlusZero a) + ... = a + w1 : { Symm L2 } + ... = b : Hw1. SetOpaque ge true. SetOpaque lt true. diff --git a/src/builtin/kernel.lean b/src/builtin/kernel.lean index 7086b72c4..8ae590ae9 100644 --- a/src/builtin/kernel.lean +++ b/src/builtin/kernel.lean @@ -106,6 +106,8 @@ Theorem Absurd {a : Bool} (H1 : a) (H2 : ¬ a) : false Theorem EqMP {a b : Bool} (H1 : a == b) (H2 : a) : b := Subst H2 H1. +(* assume is a 'macro' that expands into a Discharge *) + Theorem ImpTrans {a b c : Bool} (H1 : a ⇒ b) (H2 : b ⇒ c) : a ⇒ c := assume Ha, MP H2 (MP H1 Ha). diff --git a/src/builtin/obj/Nat.olean b/src/builtin/obj/Nat.olean index 50bf3901e9720003055162abec77d415b178f709..5a341daf346c46389367389258eeed0a7ebb8a67 100644 GIT binary patch literal 15904 zcmb7LdyHL089y^~?{;@%Fi~1SWcygQB@nPcVwFI-rIfa0DTM-s@+jN(wtLHVx81u7 zHEMkD3RY>r2OjSTfc&AN0j0DkV0@s7qCDiSBw8f;AAY~zckaxbx#zB>f!S|n zzW4XdH#6s)J2p}u8r|3!sb~2=vwX|evGIxQvikUFeIz??Xgsqkh9(cG!^jah{zZK`Kob_fKS>9Xq- zu=bR(u@T{cZVwtmu$SQBXsZxJj;1JRVXgxm)14^z@^$wFEe@a-U^8uG0)MjZYD<-B zOO<|WN5$hAg&qJTD$!FEdZKcr%mcE(cT;D+VD&*Yr4!eM5!Vk#TpJsL&p@lrIhY`t zf^yb=CX@fB$@l{5cTl!ydsYG7v{jSq*RQCrsgI8Zh67@7eH*5QG4*o*dzeai;c@QD$SG=X}QG$kaMjpbm+sQ*fP7?x#v*(WX)uCHG#h(qJ9= z*S@F@x3;lyBh<;V>C&lhZ!{;G+Ba3Zo{%Z^2L}@|%SSg%u4g^zvMWhDO=7+->j$g` zciF}=QG^u-t9zMFDz|<_oT=6CbtUamGH7MN@zOKqoZ&oU;p`RlGe_$gxf}*uRswpr z&)Rdw8<#hRq;_}`P4JcD^$qiaSKy2-TSppoaX`XJb!XU5B70v8h^YC7iJ546t7sK* zE|oYwtJ>`tRK-@yDmb;#Tt7TCF10Qdrb)5C!faK1h<_J}{-+I%H0w)78e2G$t;L_7 zYRlVI_#XdOQ|k-a26xfZHkJ$AQ_#dIfPTIX0Fp^xONk9f(6Y^ohnn7v!8^pYl=DH* zZhpVQm)YllJXgk#^yFSkrcOh2|jWsfQ*CP2Gq=Lva^ypvD0-yL)VNcO0$E8_-7Tf#objR2*8Z6==+}NS%52irqTZuDYCvzYex89~-CSw_ zTk9ubNe*pG2?WogN!AYz97T`%^BNhYuH`}`kB`xltaqAQtaI&Nj;dvy3Iu%@qTfd| ze+4jI@bq_^`yZBRSfo$?dt@Kd*}eh z)G>fwMDtRq74%NQfMC3?0njp7eL9oOQ-|0?!2ef@N--go{>}Mc165~|MEVbA-ibYv zGUWD0GfNZczhKalaD4}Z?{?xE?Be-oX zWIK+E?>Z0{);;>i1Z~Mf7aeavn(DeAwiOg+*usQ(Aj%9de-#ab#RdJ3#2j7an%H%q z%93x@exBgyx{!TXLuN)I<6YGuXhM1POrB?8%;Z{{l41sqHrP>2H>blUz7K*dyjFlEmgz#Sc_m#sfeF zWR^ry(NFOib+g#xF9RoaJ$zsm7ae1kW3c25?iGkM&RAhI*&!gwOLIB~)4W_FVu(nHq8daRC>(|4fk7x{biURF z%Bw&LW+5pp)&2|y+fy8ajdm>(K4iwG!x_jlqOd2#EH--~-bP3eJVs2H;BzTZ*j}v` zM}oHWWMsB-rbApRo{SzM%Ofc)M1ZB8_N!&y%Qzktyxj40L@_k7hs+(sE5(X> zg#_~zP$Y+U^JV3Lsn-ckS(&Z|%C%7*1S2~fnP?E#G_9m*VJkB?L9m_x)hiJ24K=;3 z4ZO&PT$LfHZjRJynU?FB(BppxGlnM`oguy7@y&NJeODFuH8h252N{Ob;sm82+4P>F{jkoy$C&}H z!AZcXHzS~@+#vUEOz-L-SF1%-Ggxi8K-h%hn^ymO+RGdSskG#XIOR3)43TtwE%|p?%>bDbIxq z^&2Gd3xW#zN&`r1_0<5&cgZ)~(}$J^K1^;lop#AL>DaV-Q;Gasmaz22NzZNS7vd++ z2+TjBd8cOtK}ULl4AM;a7Z~Us<2ONZARe##Yg4HYNu!Reg2#1e%6<6WR6eBV$Y)9) zzE|o)?hWzMqRGL12pvp&zWMT+b+(~j2gi9k{29U=0!UVRPA2ezuV`65Ph=H zaB|nx^TYMji7O(0oYf6YuStm0gS(yqfQfoyb|&jePf~giU z14;|W<%JbcC?4{XW@5atZgL_@et!V$cn_s@Opy2<8b;v_a}ABS5%M&sUk%{b2)4(U zW|9x`BD#lKTqf=GC=3CWtB9AyZ5+hrtg#=C@Iil)G}&HEZ!4Q2qrHfl{U|Vbw>^uP ze$(dh+-yw(M5bAC=H{SHHhrZZPUy{K(41!tn!i0s-C-!DVWob_BU%OoNyUfF_LD$9 zA+j@g3?`bzUZicS$xLVR3)kcvs{#Sc>}28D70NJT3k}W$K3G}xq(8j2<3sld|J+D- z%(U^J?M3m5ACa!!e^RC57ECSIOhxJi+Sy*$KzeaGDKIaQh7SYmrR7NEToEiTQ=%&V z5N5&xPM;g_m6^Sy3d$Oq@=9(7F*WG*XBo-+zKrN&ryjV0r$K6+KRuz=eihiYf@3f0 zAXV#PR2{)lUY?+(iR{yFJVXI9Yd9TrxwM%4_98*DYlCi40219U1m^jjbi-tR9|y?o zK($ckXiF?8&+Bc!w`_&f7l?_!LFeDD}gdqRDxtCnj^{^mh`N zm;`Hcfr-hqHl7OMSPi11l9=H5XU`1^vUKW#PZV4U%(FWvSdmG6ZJ{~hfXu*z=So($ zI4T^pIxA7=Y*4NQQdlu8K3RCI6t+CPa~u*}iRJ$7d1gM4!_yBQ4zdL_>zm|5@a6#G z6rVrc3We`}bvtIRk;YC(^8h^-Az| z33`Z(3dy^;us0d<*=Z118YTFjo;bcu?BYi%Y5e079mAI)!+Dnqkn(rz@lK z7xv-v80G`&g`N_ABY^#Flwn@a{0Tbk&^^vi@#vaAkH$RDB0)Am#+ZT$Cv9DtKZ(M;j0e$*;wIhwg6LkBAstF24R{P$G_BGBV zh2|w0w6Ex5y9o$tocbxzt3z?FfNCdbqbmc~Rl40!*ipa?RSfTs#p_^M#Ii7 z23*U;!s4J_4Rlr92|2nH?h4@D1lv|csRTR&F(2v%1;zBT)sL}!;$?hM^aQbZ+LXiW zGLX0r(0#rTDi31Euc175ByjdjF+3Ru2e6RzEfh6?Z_P)Ft3eHr2}e!lmZ@rH5esE2 zKllpT?DCH%{3er;yyOiP zaKmvyzp@Dr=JXVs>^F{=W1i#kcUg%7bSJe)UZy#GE#>;k(37*EV<8`@LcJQAXj9Z6 z%#uMjkDl~J#~p^gYNjzwL}}tkrX5$vv=9#>>`eMiEm-8}a2a+BrO6*0=x1P>)q#%I z?@0PPp-uFC$PRS1lmTK9Yb#Y#9k%lC*_;LWTsrGMfQI1x0em2U-xttX=25IVs1^fj zADX#p@h-rc15{lrPU{=2du7g<=p!r?*Cq1NW!dpC-9hy!0Ttg&Z6AavRUD7hbMRq- z+{OB_>;)N%4K*R*fYgp-fvcaW#rJv{C!WRyD2(h(`TB9uy5{8g2K|1rh{M}nW{ZQG z;wn!*p`lYivu{BqN@NYKtJF7G5VTWKMCNY0sJYzlkt`C zHhdaOCRpY<(QyR3In3RR9@is>Ou4H&|)hROS#|$on(PQDkyfk=K+YgugtXGKKE`GgB zD2Qfesn>rA*6MXV)X~hR!zj*nZWl+NB}ms^84#WzNC(d$NIA@4ZaVZ0B)Uhm+&>1a zaKy(G{wuV;^0RM(?$P%lh8rBk=$1-lIoO0+?q`rkU2?wd4c&prQ%Qfp49@r(>=w%HSQ&7rXiyF=rSenS0e<#-Jk*TzSMvMn?KZQzv3eU-Rq#$LXkiB z!~k=F5mWjkY|))FI-_}f_tq5n!kw2mmwZ?0-j*5n2IW2Ebx>oA0axnN@Xmp~% zpP-c0s{B+Xxg|d^ph#*G9DNY`e})XrsOJOt7l4{ve-)_GohDZ|5PV9x*UGBQ4G|G# zJpm#^d$pKJ*Ks@FL4I0AFs~`gg2F*LCAL+S$^m7!O+EWs-9+w%K(`0&J~Z*s&PO54 zyFJNZj4$Ms1O2>~FgVlgVc4~fMMxf1`O{axugoZ>N##Hc9!v+-1dKD1g-cgpa(}BF z2sdeUqkYOhVSNzz?PzBmblVLKE!+a6)vaDbXCG4(s3i`n=zXu*I`;laMr4Vexphci_Dqvs07gCe)p695-wH=P P`HinxGP>b3{3`r^27xV; literal 15930 zcmb7LX^>q-6~5i~y-8+%pj8S%kz~j)31ERCl!Z$OFUVxk5P_t`04AA9UWOMYGh`ML zEiIQ41vP3!t3(u)04}9~dzD+^8WRP64l}0K3Wq;pyUw7ZW_YH9>>FMQc zefpf!r~CFyO|(ZRcXuY*S@B~w?7eAfdN#YUJw4f;$X+ozo!L#Jv)KZZ*|DkFY|TVx zbSAUM-~7JJ3gxo7&ctkIa&vn&%O@S=imd2ibNlG7UD>9o+0og~)Fcp$eJ(NApplnA z_s&fupyv^EEkGM3P$zJi=&DOHS>xvFRH5}s?Uh1c6J4w0awa7omCVi z;jDda=Kd{k{TEZdMcJAISp#qjHqY(cxv70^dwMDm9Cj0K@58VoO!;zD`)O7eqMF$f zfen*;0=8emKD$11q-rQpe~Uq9$uP>LC=8a9;te?4M^6S2YmDc0<;2`fA}YXy9tnz0 zQtB_EVy-oEMj`|n6mf~#NiVH&v8Q~++{FAcH6RX=C{s|K!#qimNTMQA=q2?5FVe;~ z?62xnXItCZy&K|W*{QD4KG2z&ol)B~?M~KAtv=Y9u-P!VYi=jwNuRxvxC`8xk7Yxs zYr=iDv)&29hy(9luR&28!iv+hhPz5=xSt%YF&T`&d9g*&7CypcrVP z6yP!naZ%Q^2hb_OuIaZkH%#r{-ac^Cbm34}CmdxNC(F?~x4OJDv-5`0X%{^Ca~;ZU zO{ZY|T<0dYc64H2nb=E+&}KOUBDqyrKiOW9nxb^HygQY!p3Yy#M4BK=Jr~;KT%<~j9B{0!a6U@d z;4)&Lz`hj-1ava(N5gF|cD-tES%x;%adNus13Wb{bPlSoM!~t${hLj+TPR{Zj-#W{ zBdV`M5$#1Z8jj1PYg|2eI>HWqHb)bkS9`-0>XpFJB)1ZsQ@<@yA)_)^@V+7bS_Rl5 zMd*gGYg|th!Y*&m%uc(|=|sGY(0xAsIax2Hgv>YMRCFR+$I1t%9N#nhG36T$QGc?LX;Fin~9lf zB>On4<-Idf3`UQmc(isFR7q(9Ve+zm;Bv7RYa|(`46%j)|IZYZY=SBMo8vzQs74Y) z`VU6_6>BCXcrze4&00hHFNXUQs{caglf9^hdCdVX(5_|h@2WonODvMbdXghy%0aJ* zsl&`)GUYbnDC~{_Ig9-s?F)jmq#>u9CMYLJAFqZITG;9Yc{s8RP>^wy#x0(fWOa$5O4CnVG6Pxb@kc;8t3+Fi~o!Sihu~ zjQS}$vl>M$X6&jeNuj{;1`!1?Sc6&V=^7rrrJ^)|S;%++3lFaq?}y&a862YWLvlnB zA4#=~YZdcMQVH4xX>;a$reR(HkQYYl8w4q05@euN4ErH2dlt26YKak>wSo^=gCIra z!=X)LRTX$7JIR)E|VNkSnhG&7cJ%EU4HG-t`Fg{{oo z0mjMzr4=xEzouR(11*vvRS^W%osn1-D(Lu-D>CeZ3SA#L8F(}3;qRUgUa~q^aS8G< zO5RhC3h;YDAG$Lis|O-w&YT)1Wx{_PBZg;tjSxQsy-#5HUPh0WtJXMI$QEz*@+(}a z9sKN*AkaTdA0(FK<_ajw4Seqdufsj~Dq2J_gVB}_!XgCUB-b||qXSift+>%A{aMr; zh6wk8p!qxsu6$UNBm*{s4kkO%OJX->zJy{cz|wS|LsFWCg3|6${M!dK-7si(4XXO6 z8!#V!O2!BR)$0}D-kr=*E|D0*U4Xo!7Z<={&F*mv)s3{h|nAycVu1BAJcr{@GYKZt^c`7J4jK!*TqhvJ0+)Gx%(Rb{!l z1`h%BE{>FEYO#X$Y+zc77i0`e=DxPfPIt!UW+UVG31H82C}&3liO->-7o5zkoW$*r zOiAH;L-l>EQr_x0lyqPh(K*!OFliS>%Yb?5g9g3m0>IC(6Ptk6eoqANI_;&d$c|xn zrf!6Uj$zd-Z5}kUtI7++^xRA*3q+z>l5?}u4%XrCN$}17AUU%JPX9IK1vPsh55Fr( zzT}FQ3$he2xHhpbMzJcIXV4g?Xhu9sTbzXh08NGT!ZEpkYB*e3cH(&UN)e36LIQ3P zAZ0g4vY=go2WA9+%~Qb_TZzNs5kErRdh)2k;ucIPub&S!%#BvUxdqhi^{AND4p*2F z)W+(8NV(wv7_SK`_?^@W7X(FmZ(w(U=#C~ZTPW%yx!HuFP2>XqU>GUdK8)BlN1z5~ zgOs|sJ)zV-Oz|y=-PVJv;$jpXK`~Rz;uP7Y-k3z8X0E4fL6)(y@!M?<$c_ftq6J7~ zdlewB?Ijxqi}N_D+zup#l;c%onT~RQO0F~Pb^w|0179YPNWjlIuRJ*kc$XtFYV~k^ zdCG;QCk!Ev)z`h2tCo$RSPp=2N|71ND0oNjv*z9N z%t`=<+YcrO*~Od|_Vr?;`#`AP$tsoMvj_Wt)DHMtU11lYcrXP*C%(DbFVu}Fy6fD; zjHi%IC(rjdydqV=nq)~5&E2%vpj#N{mm|Bw%Oyj&D$({TD)x&&pj#xDhnz>DjTV5q zp$OFvxx$JdmQx2!X)-M57ZL^o{+7xm=>PX^dBgG1;)i_GJ|CSr13{!>#b{j0Qa;RH z+SNR%iG4nG0~SJL2_fK+GOSHYOmzv>UnnKJ?Zn zAS7xRk%`wQ69zjt-#wN630V9zvM?`aHWaGb<9u5;a7qmtAV4Ea^MT`p58HrV!~oR( z9!2~?5$zP7JE1@c|3}aZsjU5dSuyr84F7@7*m6~GeqQY21|1TI8+7|;iHS~FbIA&l96}U)8jo z6Vr<8K`&qqtq&^N=n5g2gxNO^fOb`Hal^c9M{pV@qMQ!SH+k|NfkDDti*aTWnmEW6k0(O- zBYMpjD!|H-xKMPga51MWHra1-9*&vEDIP3N1fV)8Me;E%U*fpsgLUA^&1Fs+lTC=% zLJ@6>S_F7uelFM02c4XkR+3C>ny`}LI7?euvb10c1UQtm=M=C=F~?yzZ@HrQQm6-D ziU|Ravp<-$4?&vZjuEwkC=|+2Q*z+wq z-k{^hq62FLP$y6<(~R#%T{b|`6>+++uRi6*auYqjg2W^4xn*5?=-z&Vmh^-gZwV}F z6O{I|s7mn9g(_~>^X+;@dtJ5=1EfR5VHZ0tM3)|?#pin0pYY?#E^+T3*Nn}~P4Cjn z$ubO2d&RCC1m#kSpL@tPvTsv6e$3^V>yUUB4qD}L0sv8@NYbyl?#sCr0_%B5sYRgi(Qhp!NZy>4FE+^A>Xb^2NlO!w9w<@_R?3lQn= zo2be&zZI(AM)g$4n7=)!of8>|=>x3LAYero0QtKyBm~s_gudY#Wdq>DX+NL9jT%+{ zbp#}g0tGZugi}H&$$XrhKD=&B{>mj#rLT+XQQ+`GJ!dr45DCH7l_iC1;f+OT@S;|e zOFrmzsQF>O+hr}Vre#U%xF#vI{)13eK0#Z4n7FJW&C3rj2iPqrv{>I^br>ZANBoGA zae=x4$NWnQ_fUM4;^T&Yzv3$&e6yN={r_OY4UTNIrBYaS&OxmFA@HLt#l-D?nu?o% zdtlCL{wf1;mYIFd4`z1$7ww1E?91Ac+~FONAG!2|Mp0!mQVb>Z`45RWlX zL^VPpKJeyPq5LT4)Bw^j(1{B|vn z*QFK|&<3kgJ>qk%9_Nsd5>&=G;U~)$ojIc%&BNz^nFk*7z@qZxU1k1vbpDzAkZlC< z)9W9h|FsFA7K-kIqYkrV0+oN0(+R8mceIt0f=R}6o%UCnzQj*#>j^;4Rapg9(GN%v ztCQXX=YIhKA5wqn8s(6>W^%T}KR&68RYg|iY|H&=0a;R#py+3@{cG@$as4J#e~YS& z>vyi!7)Xt4AppEd<$tP+GPg%a?riIu3* zczWGwQ@O9zCh{pz$&aEufg(=r{3?X;{Akh{!#niGX?|RJKa`mtEgNhX$b*VLbp`l_ zp7Z(;)Hn^D&u+T1Vv!77^1$T$);JAnQgq||M89l-jc0-A!7Aw>+Yvx0aJxzx-5Srv zFgT@8DjSPjUw#xDD4&GoM|B`WZ$~@PXD}9M7f;F+?*aC3kOJEveKtQ*R%QjrI>5&B zm{l=Z!xqt4;fnm>Aj`vLHDo}_4pr3vWcq{kqBJf7Y^v-PWrhkbq^jMaoA&<7;W`(6 i`AwtxJiB1LokcD8_sCIeywq}k{cA=hcdf