From a87e20577e179e14ff58b63fc638d2bfe85fc4de Mon Sep 17 00:00:00 2001 From: arnaudgolfouse Date: Fri, 13 Dec 2024 11:34:45 +0100 Subject: [PATCH] Update tests --- .../creusot-contracts/creusot-contracts.coma | 481 ++++++++++++++---- .../creusot-contracts/why3session.xml | 10 + .../creusot-contracts/why3shapes.gz | Bin 24505 -> 23838 bytes creusot/tests/should_succeed/bug/387.coma | 2 +- .../syntax/10_mutual_rec_types.coma | 2 +- 5 files changed, 399 insertions(+), 96 deletions(-) diff --git a/creusot/tests/creusot-contracts/creusot-contracts.coma b/creusot/tests/creusot-contracts/creusot-contracts.coma index 95709096a..1671c2a8f 100644 --- a/creusot/tests/creusot-contracts/creusot-contracts.coma +++ b/creusot/tests/creusot-contracts/creusot-contracts.coma @@ -92,11 +92,304 @@ module M_creusot_contracts__stdqy35z1__array__qyi15505960269205342033__produces_ goal vc_produces_trans'0 : ([%#sarray1] produces'0 b bc c) -> ([%#sarray0] produces'0 a ab b) -> ([%#sarray2] produces'0 a (Seq.(++) ab bc) c) end -module M_creusot_contracts__stdqy35z1__cmp__qyi16241606109483467814__cmp_le_log [#"../../../creusot-contracts/src/std/cmp.rs" 88 4 88 35] (* as logic::ord::OrdLogic> *) - let%span scmp0 = "../../../creusot-contracts/src/std/cmp.rs" 87 14 87 64 - let%span scmp1 = "../../../creusot-contracts/src/std/cmp.rs" 85 4 85 10 +module M_creusot_contracts__stdqy35z1__cmp__extern_spec_std_cmp_max_body [#"../../../creusot-contracts/src/std/cmp.rs" 83 12 84 66] + let%span scmp0 = "../../../creusot-contracts/src/std/cmp.rs" 83 22 83 24 + let%span scmp1 = "../../../creusot-contracts/src/std/cmp.rs" 83 29 83 31 + let%span scmp2 = "../../../creusot-contracts/src/std/cmp.rs" 83 39 83 40 + let%span scmp3 = "../../../creusot-contracts/src/std/cmp.rs" 78 22 78 60 + let%span scmp4 = "../../../creusot-contracts/src/std/cmp.rs" 79 22 79 60 + let%span scmp5 = "../../../creusot-contracts/src/std/cmp.rs" 80 22 80 50 + let%span scmp6 = "../../../creusot-contracts/src/std/cmp.rs" 81 22 81 73 + let%span scmp7 = "../../../creusot-contracts/src/std/cmp.rs" 82 22 82 72 + let%span scmp8 = "../../../creusot-contracts/src/std/cmp.rs" 53 26 53 66 + let%span scmp9 = "../../../creusot-contracts/src/std/cmp.rs" 54 26 54 63 + let%span scmp10 = "../../../creusot-contracts/src/std/cmp.rs" 7 0 101 1 + let%span sord11 = "../../../creusot-contracts/src/logic/ord.rs" 29 14 29 64 + let%span sord12 = "../../../creusot-contracts/src/logic/ord.rs" 40 14 40 61 + let%span sord13 = "../../../creusot-contracts/src/logic/ord.rs" 51 14 51 61 + let%span sord14 = "../../../creusot-contracts/src/logic/ord.rs" 62 14 62 64 + let%span sord15 = "../../../creusot-contracts/src/logic/ord.rs" 67 14 67 45 + let%span sord16 = "../../../creusot-contracts/src/logic/ord.rs" 72 15 72 32 + let%span sord17 = "../../../creusot-contracts/src/logic/ord.rs" 73 15 73 32 + let%span sord18 = "../../../creusot-contracts/src/logic/ord.rs" 74 14 74 31 + let%span sord19 = "../../../creusot-contracts/src/logic/ord.rs" 81 15 81 45 + let%span sord20 = "../../../creusot-contracts/src/logic/ord.rs" 82 14 82 47 + let%span sord21 = "../../../creusot-contracts/src/logic/ord.rs" 89 15 89 48 + let%span sord22 = "../../../creusot-contracts/src/logic/ord.rs" 90 14 90 44 + let%span sord23 = "../../../creusot-contracts/src/logic/ord.rs" 95 14 95 59 + + type t_T'0 + + predicate inv'0 [#"../../../creusot-contracts/src/invariant.rs" 41 0 41 35] (_1 : t_T'0) + + type t_DeepModelTy'0 + + function deep_model'0 [#"../../../creusot-contracts/src/model.rs" 29 4 29 45] (self : t_T'0) : t_DeepModelTy'0 + + type t_Ordering'0 = + | C_Less'0 + | C_Equal'0 + | C_Greater'0 + + function cmp_log'0 [#"../../../creusot-contracts/src/logic/ord.rs" 19 4 19 46] (self : t_DeepModelTy'0) (other : t_DeepModelTy'0) : t_Ordering'0 + + + function eq_cmp'0 [#"../../../creusot-contracts/src/logic/ord.rs" 96 4 96 32] (x : t_DeepModelTy'0) (y : t_DeepModelTy'0) : () + + + axiom eq_cmp'0_spec : forall x : t_DeepModelTy'0, y : t_DeepModelTy'0 . [%#sord23] (x = y) + = (cmp_log'0 x y = C_Equal'0) + + function antisym2'0 [#"../../../creusot-contracts/src/logic/ord.rs" 91 4 91 34] (x : t_DeepModelTy'0) (y : t_DeepModelTy'0) : () + + + axiom antisym2'0_spec : forall x : t_DeepModelTy'0, y : t_DeepModelTy'0 . ([%#sord21] cmp_log'0 x y = C_Greater'0) + -> ([%#sord22] cmp_log'0 y x = C_Less'0) + + function antisym1'0 [#"../../../creusot-contracts/src/logic/ord.rs" 83 4 83 34] (x : t_DeepModelTy'0) (y : t_DeepModelTy'0) : () + + + axiom antisym1'0_spec : forall x : t_DeepModelTy'0, y : t_DeepModelTy'0 . ([%#sord19] cmp_log'0 x y = C_Less'0) + -> ([%#sord20] cmp_log'0 y x = C_Greater'0) + + function trans'0 [#"../../../creusot-contracts/src/logic/ord.rs" 75 4 75 53] (x : t_DeepModelTy'0) (y : t_DeepModelTy'0) (z : t_DeepModelTy'0) (o : t_Ordering'0) : () + + + axiom trans'0_spec : forall x : t_DeepModelTy'0, y : t_DeepModelTy'0, z : t_DeepModelTy'0, o : t_Ordering'0 . ([%#sord16] cmp_log'0 x y + = o) -> ([%#sord17] cmp_log'0 y z = o) -> ([%#sord18] cmp_log'0 x z = o) + + function refl'0 [#"../../../creusot-contracts/src/logic/ord.rs" 68 4 68 21] (x : t_DeepModelTy'0) : () + + axiom refl'0_spec : forall x : t_DeepModelTy'0 . [%#sord15] cmp_log'0 x x = C_Equal'0 + + function gt_log'0 [#"../../../creusot-contracts/src/logic/ord.rs" 57 4 57 36] (self : t_DeepModelTy'0) (o : t_DeepModelTy'0) : bool + + + function cmp_gt_log'0 [#"../../../creusot-contracts/src/logic/ord.rs" 63 4 63 36] (x : t_DeepModelTy'0) (y : t_DeepModelTy'0) : () + + + axiom cmp_gt_log'0_spec : forall x : t_DeepModelTy'0, y : t_DeepModelTy'0 . [%#sord14] gt_log'0 x y + = (cmp_log'0 x y = C_Greater'0) + + function ge_log'0 [#"../../../creusot-contracts/src/logic/ord.rs" 46 4 46 36] (self : t_DeepModelTy'0) (o : t_DeepModelTy'0) : bool + + + function cmp_ge_log'0 [#"../../../creusot-contracts/src/logic/ord.rs" 52 4 52 36] (x : t_DeepModelTy'0) (y : t_DeepModelTy'0) : () + + + axiom cmp_ge_log'0_spec : forall x : t_DeepModelTy'0, y : t_DeepModelTy'0 . [%#sord13] ge_log'0 x y + = (cmp_log'0 x y <> C_Less'0) + + function lt_log'0 [#"../../../creusot-contracts/src/logic/ord.rs" 35 4 35 36] (self : t_DeepModelTy'0) (o : t_DeepModelTy'0) : bool + + + function cmp_lt_log'0 [#"../../../creusot-contracts/src/logic/ord.rs" 41 4 41 36] (x : t_DeepModelTy'0) (y : t_DeepModelTy'0) : () + + + axiom cmp_lt_log'0_spec : forall x : t_DeepModelTy'0, y : t_DeepModelTy'0 . [%#sord12] lt_log'0 x y + = (cmp_log'0 x y = C_Less'0) + + function le_log'0 [#"../../../creusot-contracts/src/logic/ord.rs" 24 4 24 36] (self : t_DeepModelTy'0) (o : t_DeepModelTy'0) : bool + + + function cmp_le_log'0 [#"../../../creusot-contracts/src/logic/ord.rs" 30 4 30 36] (x : t_DeepModelTy'0) (y : t_DeepModelTy'0) : () + + + axiom cmp_le_log'0_spec : forall x : t_DeepModelTy'0, y : t_DeepModelTy'0 . [%#sord11] le_log'0 x y + = (cmp_log'0 x y <> C_Greater'0) + + let rec max'0 (self:t_T'0) (other:t_T'0) (return' (ret:t_T'0))= {[@expl:max 'self' type invariant] inv'0 self} + {[@expl:max 'other' type invariant] inv'0 other} + any + [ return' (result:t_T'0)-> {inv'0 result} + {[%#scmp8] ge_log'0 (deep_model'0 result) (deep_model'0 self)} + {[%#scmp9] ge_log'0 (deep_model'0 result) (deep_model'0 other)} + {[%#scmp10] result = self \/ result = other} + {[%#scmp10] le_log'0 (deep_model'0 self) (deep_model'0 other) -> result = other} + {[%#scmp10] lt_log'0 (deep_model'0 other) (deep_model'0 self) -> result = self} + (! return' {result}) ] + + + use prelude.prelude.Intrinsic + + meta "compute_max_steps" 1000000 + + let rec extern_spec_std_cmp_max_body'0 (v1:t_T'0) (v2:t_T'0) (return' (ret:t_T'0))= {[@expl:extern_spec_std_cmp_max_body 'v1' type invariant] [%#scmp0] inv'0 v1} + {[@expl:extern_spec_std_cmp_max_body 'v2' type invariant] [%#scmp1] inv'0 v2} + (! bb0 + [ bb0 = bb1 + | bb1 = bb2 + | bb2 = bb3 + | bb3 = bb4 + | bb4 = bb5 + | bb5 = s0 [ s0 = max'0 {v1} {v2} (fun (_ret':t_T'0) -> [ &_0 <- _ret' ] s1) | s1 = bb6 ] + | bb6 = bb7 + | bb7 = bb8 + | bb8 = return' {_0} ] + ) [ & _0 : t_T'0 = any_l () | & v1 : t_T'0 = v1 | & v2 : t_T'0 = v2 ] + [ return' (result:t_T'0)-> {[@expl:extern_spec_std_cmp_max_body result type invariant] [%#scmp2] inv'0 result} + {[@expl:extern_spec_std_cmp_max_body ensures #0] [%#scmp3] ge_log'0 (deep_model'0 result) (deep_model'0 v1)} + {[@expl:extern_spec_std_cmp_max_body ensures #1] [%#scmp4] ge_log'0 (deep_model'0 result) (deep_model'0 v2)} + {[@expl:extern_spec_std_cmp_max_body ensures #2] [%#scmp5] result = v1 \/ result = v2} + {[@expl:extern_spec_std_cmp_max_body ensures #3] [%#scmp6] le_log'0 (deep_model'0 v1) (deep_model'0 v2) + -> result = v2} + {[@expl:extern_spec_std_cmp_max_body ensures #4] [%#scmp7] lt_log'0 (deep_model'0 v2) (deep_model'0 v1) + -> result = v1} + (! return' {result}) ] + +end +module M_creusot_contracts__stdqy35z1__cmp__extern_spec_std_cmp_min_body [#"../../../creusot-contracts/src/std/cmp.rs" 94 12 95 66] + let%span scmp0 = "../../../creusot-contracts/src/std/cmp.rs" 94 22 94 24 + let%span scmp1 = "../../../creusot-contracts/src/std/cmp.rs" 94 29 94 31 + let%span scmp2 = "../../../creusot-contracts/src/std/cmp.rs" 94 39 94 40 + let%span scmp3 = "../../../creusot-contracts/src/std/cmp.rs" 89 22 89 60 + let%span scmp4 = "../../../creusot-contracts/src/std/cmp.rs" 90 22 90 60 + let%span scmp5 = "../../../creusot-contracts/src/std/cmp.rs" 91 22 91 50 + let%span scmp6 = "../../../creusot-contracts/src/std/cmp.rs" 92 22 92 72 + let%span scmp7 = "../../../creusot-contracts/src/std/cmp.rs" 93 22 93 73 + let%span scmp8 = "../../../creusot-contracts/src/std/cmp.rs" 60 26 60 66 + let%span scmp9 = "../../../creusot-contracts/src/std/cmp.rs" 61 26 61 63 + let%span scmp10 = "../../../creusot-contracts/src/std/cmp.rs" 7 0 101 1 + let%span scmp11 = "../../../creusot-contracts/src/std/cmp.rs" 64 26 64 77 + let%span sord12 = "../../../creusot-contracts/src/logic/ord.rs" 29 14 29 64 + let%span sord13 = "../../../creusot-contracts/src/logic/ord.rs" 40 14 40 61 + let%span sord14 = "../../../creusot-contracts/src/logic/ord.rs" 51 14 51 61 + let%span sord15 = "../../../creusot-contracts/src/logic/ord.rs" 62 14 62 64 + let%span sord16 = "../../../creusot-contracts/src/logic/ord.rs" 67 14 67 45 + let%span sord17 = "../../../creusot-contracts/src/logic/ord.rs" 72 15 72 32 + let%span sord18 = "../../../creusot-contracts/src/logic/ord.rs" 73 15 73 32 + let%span sord19 = "../../../creusot-contracts/src/logic/ord.rs" 74 14 74 31 + let%span sord20 = "../../../creusot-contracts/src/logic/ord.rs" 81 15 81 45 + let%span sord21 = "../../../creusot-contracts/src/logic/ord.rs" 82 14 82 47 + let%span sord22 = "../../../creusot-contracts/src/logic/ord.rs" 89 15 89 48 + let%span sord23 = "../../../creusot-contracts/src/logic/ord.rs" 90 14 90 44 + let%span sord24 = "../../../creusot-contracts/src/logic/ord.rs" 95 14 95 59 + + type t_T'0 + + predicate inv'0 [#"../../../creusot-contracts/src/invariant.rs" 41 0 41 35] (_1 : t_T'0) + + type t_DeepModelTy'0 + + function deep_model'0 [#"../../../creusot-contracts/src/model.rs" 29 4 29 45] (self : t_T'0) : t_DeepModelTy'0 + + type t_Ordering'0 = + | C_Less'0 + | C_Equal'0 + | C_Greater'0 + + function cmp_log'0 [#"../../../creusot-contracts/src/logic/ord.rs" 19 4 19 46] (self : t_DeepModelTy'0) (other : t_DeepModelTy'0) : t_Ordering'0 + + + function eq_cmp'0 [#"../../../creusot-contracts/src/logic/ord.rs" 96 4 96 32] (x : t_DeepModelTy'0) (y : t_DeepModelTy'0) : () + + + axiom eq_cmp'0_spec : forall x : t_DeepModelTy'0, y : t_DeepModelTy'0 . [%#sord24] (x = y) + = (cmp_log'0 x y = C_Equal'0) + + function antisym2'0 [#"../../../creusot-contracts/src/logic/ord.rs" 91 4 91 34] (x : t_DeepModelTy'0) (y : t_DeepModelTy'0) : () + + + axiom antisym2'0_spec : forall x : t_DeepModelTy'0, y : t_DeepModelTy'0 . ([%#sord22] cmp_log'0 x y = C_Greater'0) + -> ([%#sord23] cmp_log'0 y x = C_Less'0) + + function antisym1'0 [#"../../../creusot-contracts/src/logic/ord.rs" 83 4 83 34] (x : t_DeepModelTy'0) (y : t_DeepModelTy'0) : () + + + axiom antisym1'0_spec : forall x : t_DeepModelTy'0, y : t_DeepModelTy'0 . ([%#sord20] cmp_log'0 x y = C_Less'0) + -> ([%#sord21] cmp_log'0 y x = C_Greater'0) + + function trans'0 [#"../../../creusot-contracts/src/logic/ord.rs" 75 4 75 53] (x : t_DeepModelTy'0) (y : t_DeepModelTy'0) (z : t_DeepModelTy'0) (o : t_Ordering'0) : () + + + axiom trans'0_spec : forall x : t_DeepModelTy'0, y : t_DeepModelTy'0, z : t_DeepModelTy'0, o : t_Ordering'0 . ([%#sord17] cmp_log'0 x y + = o) -> ([%#sord18] cmp_log'0 y z = o) -> ([%#sord19] cmp_log'0 x z = o) + + function refl'0 [#"../../../creusot-contracts/src/logic/ord.rs" 68 4 68 21] (x : t_DeepModelTy'0) : () + + axiom refl'0_spec : forall x : t_DeepModelTy'0 . [%#sord16] cmp_log'0 x x = C_Equal'0 + + function gt_log'0 [#"../../../creusot-contracts/src/logic/ord.rs" 57 4 57 36] (self : t_DeepModelTy'0) (o : t_DeepModelTy'0) : bool + + + function cmp_gt_log'0 [#"../../../creusot-contracts/src/logic/ord.rs" 63 4 63 36] (x : t_DeepModelTy'0) (y : t_DeepModelTy'0) : () + + + axiom cmp_gt_log'0_spec : forall x : t_DeepModelTy'0, y : t_DeepModelTy'0 . [%#sord15] gt_log'0 x y + = (cmp_log'0 x y = C_Greater'0) + + function ge_log'0 [#"../../../creusot-contracts/src/logic/ord.rs" 46 4 46 36] (self : t_DeepModelTy'0) (o : t_DeepModelTy'0) : bool + + + function cmp_ge_log'0 [#"../../../creusot-contracts/src/logic/ord.rs" 52 4 52 36] (x : t_DeepModelTy'0) (y : t_DeepModelTy'0) : () + + + axiom cmp_ge_log'0_spec : forall x : t_DeepModelTy'0, y : t_DeepModelTy'0 . [%#sord14] ge_log'0 x y + = (cmp_log'0 x y <> C_Less'0) + + function lt_log'0 [#"../../../creusot-contracts/src/logic/ord.rs" 35 4 35 36] (self : t_DeepModelTy'0) (o : t_DeepModelTy'0) : bool + + + function cmp_lt_log'0 [#"../../../creusot-contracts/src/logic/ord.rs" 41 4 41 36] (x : t_DeepModelTy'0) (y : t_DeepModelTy'0) : () + + + axiom cmp_lt_log'0_spec : forall x : t_DeepModelTy'0, y : t_DeepModelTy'0 . [%#sord13] lt_log'0 x y + = (cmp_log'0 x y = C_Less'0) + + function le_log'0 [#"../../../creusot-contracts/src/logic/ord.rs" 24 4 24 36] (self : t_DeepModelTy'0) (o : t_DeepModelTy'0) : bool + + + function cmp_le_log'0 [#"../../../creusot-contracts/src/logic/ord.rs" 30 4 30 36] (x : t_DeepModelTy'0) (y : t_DeepModelTy'0) : () + + + axiom cmp_le_log'0_spec : forall x : t_DeepModelTy'0, y : t_DeepModelTy'0 . [%#sord12] le_log'0 x y + = (cmp_log'0 x y <> C_Greater'0) + + let rec min'0 (self:t_T'0) (other:t_T'0) (return' (ret:t_T'0))= {[@expl:min 'self' type invariant] inv'0 self} + {[@expl:min 'other' type invariant] inv'0 other} + any + [ return' (result:t_T'0)-> {inv'0 result} + {[%#scmp8] le_log'0 (deep_model'0 result) (deep_model'0 self)} + {[%#scmp9] le_log'0 (deep_model'0 result) (deep_model'0 other)} + {[%#scmp10] result = self \/ result = other} + {[%#scmp10] lt_log'0 (deep_model'0 self) (deep_model'0 other) -> result = self} + {[%#scmp11] le_log'0 (deep_model'0 other) (deep_model'0 self) -> result = other} + (! return' {result}) ] + + + use prelude.prelude.Intrinsic + + meta "compute_max_steps" 1000000 + + let rec extern_spec_std_cmp_min_body'0 (v1:t_T'0) (v2:t_T'0) (return' (ret:t_T'0))= {[@expl:extern_spec_std_cmp_min_body 'v1' type invariant] [%#scmp0] inv'0 v1} + {[@expl:extern_spec_std_cmp_min_body 'v2' type invariant] [%#scmp1] inv'0 v2} + (! bb0 + [ bb0 = bb1 + | bb1 = bb2 + | bb2 = bb3 + | bb3 = bb4 + | bb4 = bb5 + | bb5 = s0 [ s0 = min'0 {v1} {v2} (fun (_ret':t_T'0) -> [ &_0 <- _ret' ] s1) | s1 = bb6 ] + | bb6 = bb7 + | bb7 = bb8 + | bb8 = return' {_0} ] + ) [ & _0 : t_T'0 = any_l () | & v1 : t_T'0 = v1 | & v2 : t_T'0 = v2 ] + [ return' (result:t_T'0)-> {[@expl:extern_spec_std_cmp_min_body result type invariant] [%#scmp2] inv'0 result} + {[@expl:extern_spec_std_cmp_min_body ensures #0] [%#scmp3] le_log'0 (deep_model'0 result) (deep_model'0 v1)} + {[@expl:extern_spec_std_cmp_min_body ensures #1] [%#scmp4] le_log'0 (deep_model'0 result) (deep_model'0 v2)} + {[@expl:extern_spec_std_cmp_min_body ensures #2] [%#scmp5] result = v1 \/ result = v2} + {[@expl:extern_spec_std_cmp_min_body ensures #3] [%#scmp6] lt_log'0 (deep_model'0 v1) (deep_model'0 v2) + -> result = v1} + {[@expl:extern_spec_std_cmp_min_body ensures #4] [%#scmp7] le_log'0 (deep_model'0 v2) (deep_model'0 v1) + -> result = v2} + (! return' {result}) ] + +end +module M_creusot_contracts__stdqy35z1__cmp__qyi16241606109483467814__cmp_le_log [#"../../../creusot-contracts/src/std/cmp.rs" 127 4 127 35] (* as logic::ord::OrdLogic> *) + let%span scmp0 = "../../../creusot-contracts/src/std/cmp.rs" 126 14 126 64 + let%span scmp1 = "../../../creusot-contracts/src/std/cmp.rs" 124 4 124 10 let%span sord2 = "../../../creusot-contracts/src/logic/ord.rs" 25 20 25 56 - let%span scmp3 = "../../../creusot-contracts/src/std/cmp.rs" 78 8 82 9 + let%span scmp3 = "../../../creusot-contracts/src/std/cmp.rs" 117 8 121 9 let%span sord4 = "../../../creusot-contracts/src/logic/ord.rs" 29 14 29 64 let%span sord5 = "../../../creusot-contracts/src/logic/ord.rs" 40 14 40 61 let%span sord6 = "../../../creusot-contracts/src/logic/ord.rs" 51 14 51 61 @@ -172,7 +465,7 @@ module M_creusot_contracts__stdqy35z1__cmp__qyi16241606109483467814__cmp_le_log axiom cmp_le_log'1_spec : forall x : t_T'0, y : t_T'0 . [%#sord4] le_log'1 x y = (cmp_log'1 x y <> C_Greater'0) - function cmp_log'0 [#"../../../creusot-contracts/src/std/cmp.rs" 77 4 77 41] (self : t_Reverse'0) (o : t_Reverse'0) : t_Ordering'0 + function cmp_log'0 [#"../../../creusot-contracts/src/std/cmp.rs" 116 4 116 41] (self : t_Reverse'0) (o : t_Reverse'0) : t_Ordering'0 = [%#scmp3] match cmp_log'1 self.t_Reverse__0'0 o.t_Reverse__0'0 with @@ -190,16 +483,16 @@ module M_creusot_contracts__stdqy35z1__cmp__qyi16241606109483467814__cmp_le_log constant y : t_Reverse'0 - function cmp_le_log'0 [#"../../../creusot-contracts/src/std/cmp.rs" 88 4 88 35] (x : t_Reverse'0) (y : t_Reverse'0) : () + function cmp_le_log'0 [#"../../../creusot-contracts/src/std/cmp.rs" 127 4 127 35] (x : t_Reverse'0) (y : t_Reverse'0) : () goal vc_cmp_le_log'0 : [%#scmp0] le_log'0 x y = (cmp_log'0 x y <> C_Greater'0) end -module M_creusot_contracts__stdqy35z1__cmp__qyi16241606109483467814__cmp_lt_log [#"../../../creusot-contracts/src/std/cmp.rs" 93 4 93 35] (* as logic::ord::OrdLogic> *) - let%span scmp0 = "../../../creusot-contracts/src/std/cmp.rs" 92 14 92 61 - let%span scmp1 = "../../../creusot-contracts/src/std/cmp.rs" 90 4 90 10 +module M_creusot_contracts__stdqy35z1__cmp__qyi16241606109483467814__cmp_lt_log [#"../../../creusot-contracts/src/std/cmp.rs" 132 4 132 35] (* as logic::ord::OrdLogic> *) + let%span scmp0 = "../../../creusot-contracts/src/std/cmp.rs" 131 14 131 61 + let%span scmp1 = "../../../creusot-contracts/src/std/cmp.rs" 129 4 129 10 let%span sord2 = "../../../creusot-contracts/src/logic/ord.rs" 36 20 36 53 - let%span scmp3 = "../../../creusot-contracts/src/std/cmp.rs" 78 8 82 9 + let%span scmp3 = "../../../creusot-contracts/src/std/cmp.rs" 117 8 121 9 let%span sord4 = "../../../creusot-contracts/src/logic/ord.rs" 29 14 29 64 let%span sord5 = "../../../creusot-contracts/src/logic/ord.rs" 40 14 40 61 let%span sord6 = "../../../creusot-contracts/src/logic/ord.rs" 51 14 51 61 @@ -275,7 +568,7 @@ module M_creusot_contracts__stdqy35z1__cmp__qyi16241606109483467814__cmp_lt_log axiom cmp_le_log'0_spec : forall x : t_T'0, y : t_T'0 . [%#sord4] le_log'0 x y = (cmp_log'1 x y <> C_Greater'0) - function cmp_log'0 [#"../../../creusot-contracts/src/std/cmp.rs" 77 4 77 41] (self : t_Reverse'0) (o : t_Reverse'0) : t_Ordering'0 + function cmp_log'0 [#"../../../creusot-contracts/src/std/cmp.rs" 116 4 116 41] (self : t_Reverse'0) (o : t_Reverse'0) : t_Ordering'0 = [%#scmp3] match cmp_log'1 self.t_Reverse__0'0 o.t_Reverse__0'0 with @@ -293,16 +586,16 @@ module M_creusot_contracts__stdqy35z1__cmp__qyi16241606109483467814__cmp_lt_log constant y : t_Reverse'0 - function cmp_lt_log'0 [#"../../../creusot-contracts/src/std/cmp.rs" 93 4 93 35] (x : t_Reverse'0) (y : t_Reverse'0) : () + function cmp_lt_log'0 [#"../../../creusot-contracts/src/std/cmp.rs" 132 4 132 35] (x : t_Reverse'0) (y : t_Reverse'0) : () goal vc_cmp_lt_log'0 : [%#scmp0] lt_log'0 x y = (cmp_log'0 x y = C_Less'0) end -module M_creusot_contracts__stdqy35z1__cmp__qyi16241606109483467814__cmp_ge_log [#"../../../creusot-contracts/src/std/cmp.rs" 98 4 98 35] (* as logic::ord::OrdLogic> *) - let%span scmp0 = "../../../creusot-contracts/src/std/cmp.rs" 97 14 97 61 - let%span scmp1 = "../../../creusot-contracts/src/std/cmp.rs" 95 4 95 10 +module M_creusot_contracts__stdqy35z1__cmp__qyi16241606109483467814__cmp_ge_log [#"../../../creusot-contracts/src/std/cmp.rs" 137 4 137 35] (* as logic::ord::OrdLogic> *) + let%span scmp0 = "../../../creusot-contracts/src/std/cmp.rs" 136 14 136 61 + let%span scmp1 = "../../../creusot-contracts/src/std/cmp.rs" 134 4 134 10 let%span sord2 = "../../../creusot-contracts/src/logic/ord.rs" 47 20 47 53 - let%span scmp3 = "../../../creusot-contracts/src/std/cmp.rs" 78 8 82 9 + let%span scmp3 = "../../../creusot-contracts/src/std/cmp.rs" 117 8 121 9 let%span sord4 = "../../../creusot-contracts/src/logic/ord.rs" 29 14 29 64 let%span sord5 = "../../../creusot-contracts/src/logic/ord.rs" 40 14 40 61 let%span sord6 = "../../../creusot-contracts/src/logic/ord.rs" 51 14 51 61 @@ -378,7 +671,7 @@ module M_creusot_contracts__stdqy35z1__cmp__qyi16241606109483467814__cmp_ge_log axiom cmp_le_log'0_spec : forall x : t_T'0, y : t_T'0 . [%#sord4] le_log'0 x y = (cmp_log'1 x y <> C_Greater'0) - function cmp_log'0 [#"../../../creusot-contracts/src/std/cmp.rs" 77 4 77 41] (self : t_Reverse'0) (o : t_Reverse'0) : t_Ordering'0 + function cmp_log'0 [#"../../../creusot-contracts/src/std/cmp.rs" 116 4 116 41] (self : t_Reverse'0) (o : t_Reverse'0) : t_Ordering'0 = [%#scmp3] match cmp_log'1 self.t_Reverse__0'0 o.t_Reverse__0'0 with @@ -396,16 +689,16 @@ module M_creusot_contracts__stdqy35z1__cmp__qyi16241606109483467814__cmp_ge_log constant y : t_Reverse'0 - function cmp_ge_log'0 [#"../../../creusot-contracts/src/std/cmp.rs" 98 4 98 35] (x : t_Reverse'0) (y : t_Reverse'0) : () + function cmp_ge_log'0 [#"../../../creusot-contracts/src/std/cmp.rs" 137 4 137 35] (x : t_Reverse'0) (y : t_Reverse'0) : () goal vc_cmp_ge_log'0 : [%#scmp0] ge_log'0 x y = (cmp_log'0 x y <> C_Less'0) end -module M_creusot_contracts__stdqy35z1__cmp__qyi16241606109483467814__cmp_gt_log [#"../../../creusot-contracts/src/std/cmp.rs" 103 4 103 35] (* as logic::ord::OrdLogic> *) - let%span scmp0 = "../../../creusot-contracts/src/std/cmp.rs" 102 14 102 64 - let%span scmp1 = "../../../creusot-contracts/src/std/cmp.rs" 100 4 100 10 +module M_creusot_contracts__stdqy35z1__cmp__qyi16241606109483467814__cmp_gt_log [#"../../../creusot-contracts/src/std/cmp.rs" 142 4 142 35] (* as logic::ord::OrdLogic> *) + let%span scmp0 = "../../../creusot-contracts/src/std/cmp.rs" 141 14 141 64 + let%span scmp1 = "../../../creusot-contracts/src/std/cmp.rs" 139 4 139 10 let%span sord2 = "../../../creusot-contracts/src/logic/ord.rs" 58 20 58 56 - let%span scmp3 = "../../../creusot-contracts/src/std/cmp.rs" 78 8 82 9 + let%span scmp3 = "../../../creusot-contracts/src/std/cmp.rs" 117 8 121 9 let%span sord4 = "../../../creusot-contracts/src/logic/ord.rs" 29 14 29 64 let%span sord5 = "../../../creusot-contracts/src/logic/ord.rs" 40 14 40 61 let%span sord6 = "../../../creusot-contracts/src/logic/ord.rs" 51 14 51 61 @@ -481,7 +774,7 @@ module M_creusot_contracts__stdqy35z1__cmp__qyi16241606109483467814__cmp_gt_log axiom cmp_le_log'0_spec : forall x : t_T'0, y : t_T'0 . [%#sord4] le_log'0 x y = (cmp_log'1 x y <> C_Greater'0) - function cmp_log'0 [#"../../../creusot-contracts/src/std/cmp.rs" 77 4 77 41] (self : t_Reverse'0) (o : t_Reverse'0) : t_Ordering'0 + function cmp_log'0 [#"../../../creusot-contracts/src/std/cmp.rs" 116 4 116 41] (self : t_Reverse'0) (o : t_Reverse'0) : t_Ordering'0 = [%#scmp3] match cmp_log'1 self.t_Reverse__0'0 o.t_Reverse__0'0 with @@ -499,15 +792,15 @@ module M_creusot_contracts__stdqy35z1__cmp__qyi16241606109483467814__cmp_gt_log constant y : t_Reverse'0 - function cmp_gt_log'0 [#"../../../creusot-contracts/src/std/cmp.rs" 103 4 103 35] (x : t_Reverse'0) (y : t_Reverse'0) : () + function cmp_gt_log'0 [#"../../../creusot-contracts/src/std/cmp.rs" 142 4 142 35] (x : t_Reverse'0) (y : t_Reverse'0) : () goal vc_cmp_gt_log'0 : [%#scmp0] gt_log'0 x y = (cmp_log'0 x y = C_Greater'0) end -module M_creusot_contracts__stdqy35z1__cmp__qyi16241606109483467814__refl [#"../../../creusot-contracts/src/std/cmp.rs" 108 4 108 20] (* as logic::ord::OrdLogic> *) - let%span scmp0 = "../../../creusot-contracts/src/std/cmp.rs" 107 14 107 45 - let%span scmp1 = "../../../creusot-contracts/src/std/cmp.rs" 105 4 105 10 - let%span scmp2 = "../../../creusot-contracts/src/std/cmp.rs" 78 8 82 9 +module M_creusot_contracts__stdqy35z1__cmp__qyi16241606109483467814__refl [#"../../../creusot-contracts/src/std/cmp.rs" 147 4 147 20] (* as logic::ord::OrdLogic> *) + let%span scmp0 = "../../../creusot-contracts/src/std/cmp.rs" 146 14 146 45 + let%span scmp1 = "../../../creusot-contracts/src/std/cmp.rs" 144 4 144 10 + let%span scmp2 = "../../../creusot-contracts/src/std/cmp.rs" 117 8 121 9 let%span sord3 = "../../../creusot-contracts/src/logic/ord.rs" 29 14 29 64 let%span sord4 = "../../../creusot-contracts/src/logic/ord.rs" 40 14 40 61 let%span sord5 = "../../../creusot-contracts/src/logic/ord.rs" 51 14 51 61 @@ -583,7 +876,7 @@ module M_creusot_contracts__stdqy35z1__cmp__qyi16241606109483467814__refl [#"../ axiom cmp_le_log'0_spec : forall x : t_T'0, y : t_T'0 . [%#sord3] le_log'0 x y = (cmp_log'1 x y <> C_Greater'0) - function cmp_log'0 [#"../../../creusot-contracts/src/std/cmp.rs" 77 4 77 41] (self : t_Reverse'0) (o : t_Reverse'0) : t_Ordering'0 + function cmp_log'0 [#"../../../creusot-contracts/src/std/cmp.rs" 116 4 116 41] (self : t_Reverse'0) (o : t_Reverse'0) : t_Ordering'0 = [%#scmp2] match cmp_log'1 self.t_Reverse__0'0 o.t_Reverse__0'0 with @@ -594,16 +887,16 @@ module M_creusot_contracts__stdqy35z1__cmp__qyi16241606109483467814__refl [#"../ constant x : t_Reverse'0 - function refl'0 [#"../../../creusot-contracts/src/std/cmp.rs" 108 4 108 20] (x : t_Reverse'0) : () + function refl'0 [#"../../../creusot-contracts/src/std/cmp.rs" 147 4 147 20] (x : t_Reverse'0) : () goal vc_refl'0 : [%#scmp0] cmp_log'0 x x = C_Equal'0 end -module M_creusot_contracts__stdqy35z1__cmp__qyi16241606109483467814__trans [#"../../../creusot-contracts/src/std/cmp.rs" 115 4 115 52] (* as logic::ord::OrdLogic> *) - let%span scmp0 = "../../../creusot-contracts/src/std/cmp.rs" 112 15 112 32 - let%span scmp1 = "../../../creusot-contracts/src/std/cmp.rs" 113 15 113 32 - let%span scmp2 = "../../../creusot-contracts/src/std/cmp.rs" 114 14 114 31 - let%span scmp3 = "../../../creusot-contracts/src/std/cmp.rs" 110 4 110 10 - let%span scmp4 = "../../../creusot-contracts/src/std/cmp.rs" 78 8 82 9 +module M_creusot_contracts__stdqy35z1__cmp__qyi16241606109483467814__trans [#"../../../creusot-contracts/src/std/cmp.rs" 154 4 154 52] (* as logic::ord::OrdLogic> *) + let%span scmp0 = "../../../creusot-contracts/src/std/cmp.rs" 151 15 151 32 + let%span scmp1 = "../../../creusot-contracts/src/std/cmp.rs" 152 15 152 32 + let%span scmp2 = "../../../creusot-contracts/src/std/cmp.rs" 153 14 153 31 + let%span scmp3 = "../../../creusot-contracts/src/std/cmp.rs" 149 4 149 10 + let%span scmp4 = "../../../creusot-contracts/src/std/cmp.rs" 117 8 121 9 let%span sord5 = "../../../creusot-contracts/src/logic/ord.rs" 29 14 29 64 let%span sord6 = "../../../creusot-contracts/src/logic/ord.rs" 40 14 40 61 let%span sord7 = "../../../creusot-contracts/src/logic/ord.rs" 51 14 51 61 @@ -679,7 +972,7 @@ module M_creusot_contracts__stdqy35z1__cmp__qyi16241606109483467814__trans [#".. axiom cmp_le_log'0_spec : forall x : t_T'0, y : t_T'0 . [%#sord5] le_log'0 x y = (cmp_log'1 x y <> C_Greater'0) - function cmp_log'0 [#"../../../creusot-contracts/src/std/cmp.rs" 77 4 77 41] (self : t_Reverse'0) (o : t_Reverse'0) : t_Ordering'0 + function cmp_log'0 [#"../../../creusot-contracts/src/std/cmp.rs" 116 4 116 41] (self : t_Reverse'0) (o : t_Reverse'0) : t_Ordering'0 = [%#scmp4] match cmp_log'1 self.t_Reverse__0'0 o.t_Reverse__0'0 with @@ -696,16 +989,16 @@ module M_creusot_contracts__stdqy35z1__cmp__qyi16241606109483467814__trans [#".. constant o : t_Ordering'0 - function trans'0 [#"../../../creusot-contracts/src/std/cmp.rs" 115 4 115 52] (x : t_Reverse'0) (y : t_Reverse'0) (z : t_Reverse'0) (o : t_Ordering'0) : () + function trans'0 [#"../../../creusot-contracts/src/std/cmp.rs" 154 4 154 52] (x : t_Reverse'0) (y : t_Reverse'0) (z : t_Reverse'0) (o : t_Ordering'0) : () goal vc_trans'0 : ([%#scmp1] cmp_log'0 y z = o) -> ([%#scmp0] cmp_log'0 x y = o) -> ([%#scmp2] cmp_log'0 x z = o) end -module M_creusot_contracts__stdqy35z1__cmp__qyi16241606109483467814__antisym1 [#"../../../creusot-contracts/src/std/cmp.rs" 121 4 121 33] (* as logic::ord::OrdLogic> *) - let%span scmp0 = "../../../creusot-contracts/src/std/cmp.rs" 119 15 119 45 - let%span scmp1 = "../../../creusot-contracts/src/std/cmp.rs" 120 14 120 47 - let%span scmp2 = "../../../creusot-contracts/src/std/cmp.rs" 117 4 117 10 - let%span scmp3 = "../../../creusot-contracts/src/std/cmp.rs" 78 8 82 9 +module M_creusot_contracts__stdqy35z1__cmp__qyi16241606109483467814__antisym1 [#"../../../creusot-contracts/src/std/cmp.rs" 160 4 160 33] (* as logic::ord::OrdLogic> *) + let%span scmp0 = "../../../creusot-contracts/src/std/cmp.rs" 158 15 158 45 + let%span scmp1 = "../../../creusot-contracts/src/std/cmp.rs" 159 14 159 47 + let%span scmp2 = "../../../creusot-contracts/src/std/cmp.rs" 156 4 156 10 + let%span scmp3 = "../../../creusot-contracts/src/std/cmp.rs" 117 8 121 9 let%span sord4 = "../../../creusot-contracts/src/logic/ord.rs" 29 14 29 64 let%span sord5 = "../../../creusot-contracts/src/logic/ord.rs" 40 14 40 61 let%span sord6 = "../../../creusot-contracts/src/logic/ord.rs" 51 14 51 61 @@ -781,7 +1074,7 @@ module M_creusot_contracts__stdqy35z1__cmp__qyi16241606109483467814__antisym1 [# axiom cmp_le_log'0_spec : forall x : t_T'0, y : t_T'0 . [%#sord4] le_log'0 x y = (cmp_log'1 x y <> C_Greater'0) - function cmp_log'0 [#"../../../creusot-contracts/src/std/cmp.rs" 77 4 77 41] (self : t_Reverse'0) (o : t_Reverse'0) : t_Ordering'0 + function cmp_log'0 [#"../../../creusot-contracts/src/std/cmp.rs" 116 4 116 41] (self : t_Reverse'0) (o : t_Reverse'0) : t_Ordering'0 = [%#scmp3] match cmp_log'1 self.t_Reverse__0'0 o.t_Reverse__0'0 with @@ -794,16 +1087,16 @@ module M_creusot_contracts__stdqy35z1__cmp__qyi16241606109483467814__antisym1 [# constant y : t_Reverse'0 - function antisym1'0 [#"../../../creusot-contracts/src/std/cmp.rs" 121 4 121 33] (x : t_Reverse'0) (y : t_Reverse'0) : () + function antisym1'0 [#"../../../creusot-contracts/src/std/cmp.rs" 160 4 160 33] (x : t_Reverse'0) (y : t_Reverse'0) : () goal vc_antisym1'0 : ([%#scmp0] cmp_log'0 x y = C_Less'0) -> ([%#scmp1] cmp_log'0 y x = C_Greater'0) end -module M_creusot_contracts__stdqy35z1__cmp__qyi16241606109483467814__antisym2 [#"../../../creusot-contracts/src/std/cmp.rs" 127 4 127 33] (* as logic::ord::OrdLogic> *) - let%span scmp0 = "../../../creusot-contracts/src/std/cmp.rs" 125 15 125 48 - let%span scmp1 = "../../../creusot-contracts/src/std/cmp.rs" 126 14 126 44 - let%span scmp2 = "../../../creusot-contracts/src/std/cmp.rs" 123 4 123 10 - let%span scmp3 = "../../../creusot-contracts/src/std/cmp.rs" 78 8 82 9 +module M_creusot_contracts__stdqy35z1__cmp__qyi16241606109483467814__antisym2 [#"../../../creusot-contracts/src/std/cmp.rs" 166 4 166 33] (* as logic::ord::OrdLogic> *) + let%span scmp0 = "../../../creusot-contracts/src/std/cmp.rs" 164 15 164 48 + let%span scmp1 = "../../../creusot-contracts/src/std/cmp.rs" 165 14 165 44 + let%span scmp2 = "../../../creusot-contracts/src/std/cmp.rs" 162 4 162 10 + let%span scmp3 = "../../../creusot-contracts/src/std/cmp.rs" 117 8 121 9 let%span sord4 = "../../../creusot-contracts/src/logic/ord.rs" 29 14 29 64 let%span sord5 = "../../../creusot-contracts/src/logic/ord.rs" 40 14 40 61 let%span sord6 = "../../../creusot-contracts/src/logic/ord.rs" 51 14 51 61 @@ -879,7 +1172,7 @@ module M_creusot_contracts__stdqy35z1__cmp__qyi16241606109483467814__antisym2 [# axiom cmp_le_log'0_spec : forall x : t_T'0, y : t_T'0 . [%#sord4] le_log'0 x y = (cmp_log'1 x y <> C_Greater'0) - function cmp_log'0 [#"../../../creusot-contracts/src/std/cmp.rs" 77 4 77 41] (self : t_Reverse'0) (o : t_Reverse'0) : t_Ordering'0 + function cmp_log'0 [#"../../../creusot-contracts/src/std/cmp.rs" 116 4 116 41] (self : t_Reverse'0) (o : t_Reverse'0) : t_Ordering'0 = [%#scmp3] match cmp_log'1 self.t_Reverse__0'0 o.t_Reverse__0'0 with @@ -892,15 +1185,15 @@ module M_creusot_contracts__stdqy35z1__cmp__qyi16241606109483467814__antisym2 [# constant y : t_Reverse'0 - function antisym2'0 [#"../../../creusot-contracts/src/std/cmp.rs" 127 4 127 33] (x : t_Reverse'0) (y : t_Reverse'0) : () + function antisym2'0 [#"../../../creusot-contracts/src/std/cmp.rs" 166 4 166 33] (x : t_Reverse'0) (y : t_Reverse'0) : () goal vc_antisym2'0 : ([%#scmp0] cmp_log'0 x y = C_Greater'0) -> ([%#scmp1] cmp_log'0 y x = C_Less'0) end -module M_creusot_contracts__stdqy35z1__cmp__qyi16241606109483467814__eq_cmp [#"../../../creusot-contracts/src/std/cmp.rs" 132 4 132 31] (* as logic::ord::OrdLogic> *) - let%span scmp0 = "../../../creusot-contracts/src/std/cmp.rs" 131 14 131 59 - let%span scmp1 = "../../../creusot-contracts/src/std/cmp.rs" 129 4 129 10 - let%span scmp2 = "../../../creusot-contracts/src/std/cmp.rs" 78 8 82 9 +module M_creusot_contracts__stdqy35z1__cmp__qyi16241606109483467814__eq_cmp [#"../../../creusot-contracts/src/std/cmp.rs" 171 4 171 31] (* as logic::ord::OrdLogic> *) + let%span scmp0 = "../../../creusot-contracts/src/std/cmp.rs" 170 14 170 59 + let%span scmp1 = "../../../creusot-contracts/src/std/cmp.rs" 168 4 168 10 + let%span scmp2 = "../../../creusot-contracts/src/std/cmp.rs" 117 8 121 9 let%span sord3 = "../../../creusot-contracts/src/logic/ord.rs" 29 14 29 64 let%span sord4 = "../../../creusot-contracts/src/logic/ord.rs" 40 14 40 61 let%span sord5 = "../../../creusot-contracts/src/logic/ord.rs" 51 14 51 61 @@ -976,7 +1269,7 @@ module M_creusot_contracts__stdqy35z1__cmp__qyi16241606109483467814__eq_cmp [#". axiom cmp_le_log'0_spec : forall x : t_T'0, y : t_T'0 . [%#sord3] le_log'0 x y = (cmp_log'1 x y <> C_Greater'0) - function cmp_log'0 [#"../../../creusot-contracts/src/std/cmp.rs" 77 4 77 41] (self : t_Reverse'0) (o : t_Reverse'0) : t_Ordering'0 + function cmp_log'0 [#"../../../creusot-contracts/src/std/cmp.rs" 116 4 116 41] (self : t_Reverse'0) (o : t_Reverse'0) : t_Ordering'0 = [%#scmp2] match cmp_log'1 self.t_Reverse__0'0 o.t_Reverse__0'0 with @@ -989,7 +1282,7 @@ module M_creusot_contracts__stdqy35z1__cmp__qyi16241606109483467814__eq_cmp [#". constant y : t_Reverse'0 - function eq_cmp'0 [#"../../../creusot-contracts/src/std/cmp.rs" 132 4 132 31] (x : t_Reverse'0) (y : t_Reverse'0) : () + function eq_cmp'0 [#"../../../creusot-contracts/src/std/cmp.rs" 171 4 171 31] (x : t_Reverse'0) (y : t_Reverse'0) : () goal vc_eq_cmp'0 : [%#scmp0] (x = y) = (cmp_log'0 x y = C_Equal'0) end @@ -17692,10 +17985,10 @@ module M_creusot_contracts__stdqy35z1__vec__qyi12862303518309667396__produces_re goal refines : [%#svec0] forall self : t_IntoIter'0 . forall result : () . produces'0 self (Seq.empty : Seq.seq t_T'0) self -> produces'0 self (Seq.empty : Seq.seq t_T'0) self end -module M_creusot_contracts__stdqy35z1__cmp__qyi16241606109483467814__cmp_lt_log__refines [#"../../../creusot-contracts/src/std/cmp.rs" 93 4 93 35] (* as logic::ord::OrdLogic> *) - let%span scmp0 = "../../../creusot-contracts/src/std/cmp.rs" 93 4 93 35 +module M_creusot_contracts__stdqy35z1__cmp__qyi16241606109483467814__cmp_lt_log__refines [#"../../../creusot-contracts/src/std/cmp.rs" 132 4 132 35] (* as logic::ord::OrdLogic> *) + let%span scmp0 = "../../../creusot-contracts/src/std/cmp.rs" 132 4 132 35 let%span sord1 = "../../../creusot-contracts/src/logic/ord.rs" 36 20 36 53 - let%span scmp2 = "../../../creusot-contracts/src/std/cmp.rs" 78 8 82 9 + let%span scmp2 = "../../../creusot-contracts/src/std/cmp.rs" 117 8 121 9 let%span sord3 = "../../../creusot-contracts/src/logic/ord.rs" 29 14 29 64 let%span sord4 = "../../../creusot-contracts/src/logic/ord.rs" 40 14 40 61 let%span sord5 = "../../../creusot-contracts/src/logic/ord.rs" 51 14 51 61 @@ -17771,7 +18064,7 @@ module M_creusot_contracts__stdqy35z1__cmp__qyi16241606109483467814__cmp_lt_log_ axiom cmp_le_log'0_spec : forall x : t_T'0, y : t_T'0 . [%#sord3] le_log'0 x y = (cmp_log'1 x y <> C_Greater'0) - function cmp_log'0 [#"../../../creusot-contracts/src/std/cmp.rs" 77 4 77 41] (self : t_Reverse'0) (o : t_Reverse'0) : t_Ordering'0 + function cmp_log'0 [#"../../../creusot-contracts/src/std/cmp.rs" 116 4 116 41] (self : t_Reverse'0) (o : t_Reverse'0) : t_Ordering'0 = [%#scmp2] match cmp_log'1 self.t_Reverse__0'0 o.t_Reverse__0'0 with @@ -17788,9 +18081,9 @@ module M_creusot_contracts__stdqy35z1__cmp__qyi16241606109483467814__cmp_lt_log_ goal refines : [%#scmp0] forall x : t_Reverse'0 . forall y : t_Reverse'0 . forall result : () . lt_log'0 x y = (cmp_log'0 x y = C_Less'0) -> lt_log'0 x y = (cmp_log'0 x y = C_Less'0) end -module M_creusot_contracts__stdqy35z1__cmp__qyi16241606109483467814__antisym1__refines [#"../../../creusot-contracts/src/std/cmp.rs" 121 4 121 33] (* as logic::ord::OrdLogic> *) - let%span scmp0 = "../../../creusot-contracts/src/std/cmp.rs" 121 4 121 33 - let%span scmp1 = "../../../creusot-contracts/src/std/cmp.rs" 78 8 82 9 +module M_creusot_contracts__stdqy35z1__cmp__qyi16241606109483467814__antisym1__refines [#"../../../creusot-contracts/src/std/cmp.rs" 160 4 160 33] (* as logic::ord::OrdLogic> *) + let%span scmp0 = "../../../creusot-contracts/src/std/cmp.rs" 160 4 160 33 + let%span scmp1 = "../../../creusot-contracts/src/std/cmp.rs" 117 8 121 9 let%span sord2 = "../../../creusot-contracts/src/logic/ord.rs" 29 14 29 64 let%span sord3 = "../../../creusot-contracts/src/logic/ord.rs" 40 14 40 61 let%span sord4 = "../../../creusot-contracts/src/logic/ord.rs" 51 14 51 61 @@ -17866,7 +18159,7 @@ module M_creusot_contracts__stdqy35z1__cmp__qyi16241606109483467814__antisym1__r axiom cmp_le_log'0_spec : forall x : t_T'0, y : t_T'0 . [%#sord2] le_log'0 x y = (cmp_log'1 x y <> C_Greater'0) - function cmp_log'0 [#"../../../creusot-contracts/src/std/cmp.rs" 77 4 77 41] (self : t_Reverse'0) (o : t_Reverse'0) : t_Ordering'0 + function cmp_log'0 [#"../../../creusot-contracts/src/std/cmp.rs" 116 4 116 41] (self : t_Reverse'0) (o : t_Reverse'0) : t_Ordering'0 = [%#scmp1] match cmp_log'1 self.t_Reverse__0'0 o.t_Reverse__0'0 with @@ -17878,9 +18171,9 @@ module M_creusot_contracts__stdqy35z1__cmp__qyi16241606109483467814__antisym1__r goal refines : [%#scmp0] forall x : t_Reverse'0 . forall y : t_Reverse'0 . cmp_log'0 x y = C_Less'0 -> cmp_log'0 x y = C_Less'0 /\ (forall result : () . cmp_log'0 y x = C_Greater'0 -> cmp_log'0 y x = C_Greater'0) end -module M_creusot_contracts__stdqy35z1__cmp__qyi16241606109483467814__eq_cmp__refines [#"../../../creusot-contracts/src/std/cmp.rs" 132 4 132 31] (* as logic::ord::OrdLogic> *) - let%span scmp0 = "../../../creusot-contracts/src/std/cmp.rs" 132 4 132 31 - let%span scmp1 = "../../../creusot-contracts/src/std/cmp.rs" 78 8 82 9 +module M_creusot_contracts__stdqy35z1__cmp__qyi16241606109483467814__eq_cmp__refines [#"../../../creusot-contracts/src/std/cmp.rs" 171 4 171 31] (* as logic::ord::OrdLogic> *) + let%span scmp0 = "../../../creusot-contracts/src/std/cmp.rs" 171 4 171 31 + let%span scmp1 = "../../../creusot-contracts/src/std/cmp.rs" 117 8 121 9 let%span sord2 = "../../../creusot-contracts/src/logic/ord.rs" 29 14 29 64 let%span sord3 = "../../../creusot-contracts/src/logic/ord.rs" 40 14 40 61 let%span sord4 = "../../../creusot-contracts/src/logic/ord.rs" 51 14 51 61 @@ -17956,7 +18249,7 @@ module M_creusot_contracts__stdqy35z1__cmp__qyi16241606109483467814__eq_cmp__ref axiom cmp_le_log'0_spec : forall x : t_T'0, y : t_T'0 . [%#sord2] le_log'0 x y = (cmp_log'1 x y <> C_Greater'0) - function cmp_log'0 [#"../../../creusot-contracts/src/std/cmp.rs" 77 4 77 41] (self : t_Reverse'0) (o : t_Reverse'0) : t_Ordering'0 + function cmp_log'0 [#"../../../creusot-contracts/src/std/cmp.rs" 116 4 116 41] (self : t_Reverse'0) (o : t_Reverse'0) : t_Ordering'0 = [%#scmp1] match cmp_log'1 self.t_Reverse__0'0 o.t_Reverse__0'0 with @@ -17968,9 +18261,9 @@ module M_creusot_contracts__stdqy35z1__cmp__qyi16241606109483467814__eq_cmp__ref goal refines : [%#scmp0] forall x : t_Reverse'0 . forall y : t_Reverse'0 . forall result : () . (x = y) = (cmp_log'0 x y = C_Equal'0) -> (x = y) = (cmp_log'0 x y = C_Equal'0) end -module M_creusot_contracts__stdqy35z1__cmp__qyi16241606109483467814__refl__refines [#"../../../creusot-contracts/src/std/cmp.rs" 108 4 108 20] (* as logic::ord::OrdLogic> *) - let%span scmp0 = "../../../creusot-contracts/src/std/cmp.rs" 108 4 108 20 - let%span scmp1 = "../../../creusot-contracts/src/std/cmp.rs" 78 8 82 9 +module M_creusot_contracts__stdqy35z1__cmp__qyi16241606109483467814__refl__refines [#"../../../creusot-contracts/src/std/cmp.rs" 147 4 147 20] (* as logic::ord::OrdLogic> *) + let%span scmp0 = "../../../creusot-contracts/src/std/cmp.rs" 147 4 147 20 + let%span scmp1 = "../../../creusot-contracts/src/std/cmp.rs" 117 8 121 9 let%span sord2 = "../../../creusot-contracts/src/logic/ord.rs" 29 14 29 64 let%span sord3 = "../../../creusot-contracts/src/logic/ord.rs" 40 14 40 61 let%span sord4 = "../../../creusot-contracts/src/logic/ord.rs" 51 14 51 61 @@ -18046,7 +18339,7 @@ module M_creusot_contracts__stdqy35z1__cmp__qyi16241606109483467814__refl__refin axiom cmp_le_log'0_spec : forall x : t_T'0, y : t_T'0 . [%#sord2] le_log'0 x y = (cmp_log'1 x y <> C_Greater'0) - function cmp_log'0 [#"../../../creusot-contracts/src/std/cmp.rs" 77 4 77 41] (self : t_Reverse'0) (o : t_Reverse'0) : t_Ordering'0 + function cmp_log'0 [#"../../../creusot-contracts/src/std/cmp.rs" 116 4 116 41] (self : t_Reverse'0) (o : t_Reverse'0) : t_Ordering'0 = [%#scmp1] match cmp_log'1 self.t_Reverse__0'0 o.t_Reverse__0'0 with @@ -18058,9 +18351,9 @@ module M_creusot_contracts__stdqy35z1__cmp__qyi16241606109483467814__refl__refin goal refines : [%#scmp0] forall x : t_Reverse'0 . forall result : () . cmp_log'0 x x = C_Equal'0 -> cmp_log'0 x x = C_Equal'0 end -module M_creusot_contracts__stdqy35z1__cmp__qyi16241606109483467814__trans__refines [#"../../../creusot-contracts/src/std/cmp.rs" 115 4 115 52] (* as logic::ord::OrdLogic> *) - let%span scmp0 = "../../../creusot-contracts/src/std/cmp.rs" 115 4 115 52 - let%span scmp1 = "../../../creusot-contracts/src/std/cmp.rs" 78 8 82 9 +module M_creusot_contracts__stdqy35z1__cmp__qyi16241606109483467814__trans__refines [#"../../../creusot-contracts/src/std/cmp.rs" 154 4 154 52] (* as logic::ord::OrdLogic> *) + let%span scmp0 = "../../../creusot-contracts/src/std/cmp.rs" 154 4 154 52 + let%span scmp1 = "../../../creusot-contracts/src/std/cmp.rs" 117 8 121 9 let%span sord2 = "../../../creusot-contracts/src/logic/ord.rs" 29 14 29 64 let%span sord3 = "../../../creusot-contracts/src/logic/ord.rs" 40 14 40 61 let%span sord4 = "../../../creusot-contracts/src/logic/ord.rs" 51 14 51 61 @@ -18136,7 +18429,7 @@ module M_creusot_contracts__stdqy35z1__cmp__qyi16241606109483467814__trans__refi axiom cmp_le_log'0_spec : forall x : t_T'0, y : t_T'0 . [%#sord2] le_log'0 x y = (cmp_log'1 x y <> C_Greater'0) - function cmp_log'0 [#"../../../creusot-contracts/src/std/cmp.rs" 77 4 77 41] (self : t_Reverse'0) (o : t_Reverse'0) : t_Ordering'0 + function cmp_log'0 [#"../../../creusot-contracts/src/std/cmp.rs" 116 4 116 41] (self : t_Reverse'0) (o : t_Reverse'0) : t_Ordering'0 = [%#scmp1] match cmp_log'1 self.t_Reverse__0'0 o.t_Reverse__0'0 with @@ -18150,9 +18443,9 @@ module M_creusot_contracts__stdqy35z1__cmp__qyi16241606109483467814__trans__refi /\ cmp_log'0 x y = o -> cmp_log'0 y z = o /\ cmp_log'0 x y = o /\ (forall result : () . cmp_log'0 x z = o -> cmp_log'0 x z = o) end -module M_creusot_contracts__stdqy35z1__cmp__qyi16241606109483467814__antisym2__refines [#"../../../creusot-contracts/src/std/cmp.rs" 127 4 127 33] (* as logic::ord::OrdLogic> *) - let%span scmp0 = "../../../creusot-contracts/src/std/cmp.rs" 127 4 127 33 - let%span scmp1 = "../../../creusot-contracts/src/std/cmp.rs" 78 8 82 9 +module M_creusot_contracts__stdqy35z1__cmp__qyi16241606109483467814__antisym2__refines [#"../../../creusot-contracts/src/std/cmp.rs" 166 4 166 33] (* as logic::ord::OrdLogic> *) + let%span scmp0 = "../../../creusot-contracts/src/std/cmp.rs" 166 4 166 33 + let%span scmp1 = "../../../creusot-contracts/src/std/cmp.rs" 117 8 121 9 let%span sord2 = "../../../creusot-contracts/src/logic/ord.rs" 29 14 29 64 let%span sord3 = "../../../creusot-contracts/src/logic/ord.rs" 40 14 40 61 let%span sord4 = "../../../creusot-contracts/src/logic/ord.rs" 51 14 51 61 @@ -18228,7 +18521,7 @@ module M_creusot_contracts__stdqy35z1__cmp__qyi16241606109483467814__antisym2__r axiom cmp_le_log'0_spec : forall x : t_T'0, y : t_T'0 . [%#sord2] le_log'0 x y = (cmp_log'1 x y <> C_Greater'0) - function cmp_log'0 [#"../../../creusot-contracts/src/std/cmp.rs" 77 4 77 41] (self : t_Reverse'0) (o : t_Reverse'0) : t_Ordering'0 + function cmp_log'0 [#"../../../creusot-contracts/src/std/cmp.rs" 116 4 116 41] (self : t_Reverse'0) (o : t_Reverse'0) : t_Ordering'0 = [%#scmp1] match cmp_log'1 self.t_Reverse__0'0 o.t_Reverse__0'0 with @@ -18240,10 +18533,10 @@ module M_creusot_contracts__stdqy35z1__cmp__qyi16241606109483467814__antisym2__r goal refines : [%#scmp0] forall x : t_Reverse'0 . forall y : t_Reverse'0 . cmp_log'0 x y = C_Greater'0 -> cmp_log'0 x y = C_Greater'0 /\ (forall result : () . cmp_log'0 y x = C_Less'0 -> cmp_log'0 y x = C_Less'0) end -module M_creusot_contracts__stdqy35z1__cmp__qyi16241606109483467814__cmp_le_log__refines [#"../../../creusot-contracts/src/std/cmp.rs" 88 4 88 35] (* as logic::ord::OrdLogic> *) - let%span scmp0 = "../../../creusot-contracts/src/std/cmp.rs" 88 4 88 35 +module M_creusot_contracts__stdqy35z1__cmp__qyi16241606109483467814__cmp_le_log__refines [#"../../../creusot-contracts/src/std/cmp.rs" 127 4 127 35] (* as logic::ord::OrdLogic> *) + let%span scmp0 = "../../../creusot-contracts/src/std/cmp.rs" 127 4 127 35 let%span sord1 = "../../../creusot-contracts/src/logic/ord.rs" 25 20 25 56 - let%span scmp2 = "../../../creusot-contracts/src/std/cmp.rs" 78 8 82 9 + let%span scmp2 = "../../../creusot-contracts/src/std/cmp.rs" 117 8 121 9 let%span sord3 = "../../../creusot-contracts/src/logic/ord.rs" 29 14 29 64 let%span sord4 = "../../../creusot-contracts/src/logic/ord.rs" 40 14 40 61 let%span sord5 = "../../../creusot-contracts/src/logic/ord.rs" 51 14 51 61 @@ -18319,7 +18612,7 @@ module M_creusot_contracts__stdqy35z1__cmp__qyi16241606109483467814__cmp_le_log_ axiom cmp_le_log'1_spec : forall x : t_T'0, y : t_T'0 . [%#sord3] le_log'1 x y = (cmp_log'1 x y <> C_Greater'0) - function cmp_log'0 [#"../../../creusot-contracts/src/std/cmp.rs" 77 4 77 41] (self : t_Reverse'0) (o : t_Reverse'0) : t_Ordering'0 + function cmp_log'0 [#"../../../creusot-contracts/src/std/cmp.rs" 116 4 116 41] (self : t_Reverse'0) (o : t_Reverse'0) : t_Ordering'0 = [%#scmp2] match cmp_log'1 self.t_Reverse__0'0 o.t_Reverse__0'0 with @@ -18336,10 +18629,10 @@ module M_creusot_contracts__stdqy35z1__cmp__qyi16241606109483467814__cmp_le_log_ goal refines : [%#scmp0] forall x : t_Reverse'0 . forall y : t_Reverse'0 . forall result : () . le_log'0 x y = (cmp_log'0 x y <> C_Greater'0) -> le_log'0 x y = (cmp_log'0 x y <> C_Greater'0) end -module M_creusot_contracts__stdqy35z1__cmp__qyi16241606109483467814__cmp_ge_log__refines [#"../../../creusot-contracts/src/std/cmp.rs" 98 4 98 35] (* as logic::ord::OrdLogic> *) - let%span scmp0 = "../../../creusot-contracts/src/std/cmp.rs" 98 4 98 35 +module M_creusot_contracts__stdqy35z1__cmp__qyi16241606109483467814__cmp_ge_log__refines [#"../../../creusot-contracts/src/std/cmp.rs" 137 4 137 35] (* as logic::ord::OrdLogic> *) + let%span scmp0 = "../../../creusot-contracts/src/std/cmp.rs" 137 4 137 35 let%span sord1 = "../../../creusot-contracts/src/logic/ord.rs" 47 20 47 53 - let%span scmp2 = "../../../creusot-contracts/src/std/cmp.rs" 78 8 82 9 + let%span scmp2 = "../../../creusot-contracts/src/std/cmp.rs" 117 8 121 9 let%span sord3 = "../../../creusot-contracts/src/logic/ord.rs" 29 14 29 64 let%span sord4 = "../../../creusot-contracts/src/logic/ord.rs" 40 14 40 61 let%span sord5 = "../../../creusot-contracts/src/logic/ord.rs" 51 14 51 61 @@ -18415,7 +18708,7 @@ module M_creusot_contracts__stdqy35z1__cmp__qyi16241606109483467814__cmp_ge_log_ axiom cmp_le_log'0_spec : forall x : t_T'0, y : t_T'0 . [%#sord3] le_log'0 x y = (cmp_log'1 x y <> C_Greater'0) - function cmp_log'0 [#"../../../creusot-contracts/src/std/cmp.rs" 77 4 77 41] (self : t_Reverse'0) (o : t_Reverse'0) : t_Ordering'0 + function cmp_log'0 [#"../../../creusot-contracts/src/std/cmp.rs" 116 4 116 41] (self : t_Reverse'0) (o : t_Reverse'0) : t_Ordering'0 = [%#scmp2] match cmp_log'1 self.t_Reverse__0'0 o.t_Reverse__0'0 with @@ -18432,10 +18725,10 @@ module M_creusot_contracts__stdqy35z1__cmp__qyi16241606109483467814__cmp_ge_log_ goal refines : [%#scmp0] forall x : t_Reverse'0 . forall y : t_Reverse'0 . forall result : () . ge_log'0 x y = (cmp_log'0 x y <> C_Less'0) -> ge_log'0 x y = (cmp_log'0 x y <> C_Less'0) end -module M_creusot_contracts__stdqy35z1__cmp__qyi16241606109483467814__cmp_gt_log__refines [#"../../../creusot-contracts/src/std/cmp.rs" 103 4 103 35] (* as logic::ord::OrdLogic> *) - let%span scmp0 = "../../../creusot-contracts/src/std/cmp.rs" 103 4 103 35 +module M_creusot_contracts__stdqy35z1__cmp__qyi16241606109483467814__cmp_gt_log__refines [#"../../../creusot-contracts/src/std/cmp.rs" 142 4 142 35] (* as logic::ord::OrdLogic> *) + let%span scmp0 = "../../../creusot-contracts/src/std/cmp.rs" 142 4 142 35 let%span sord1 = "../../../creusot-contracts/src/logic/ord.rs" 58 20 58 56 - let%span scmp2 = "../../../creusot-contracts/src/std/cmp.rs" 78 8 82 9 + let%span scmp2 = "../../../creusot-contracts/src/std/cmp.rs" 117 8 121 9 let%span sord3 = "../../../creusot-contracts/src/logic/ord.rs" 29 14 29 64 let%span sord4 = "../../../creusot-contracts/src/logic/ord.rs" 40 14 40 61 let%span sord5 = "../../../creusot-contracts/src/logic/ord.rs" 51 14 51 61 @@ -18511,7 +18804,7 @@ module M_creusot_contracts__stdqy35z1__cmp__qyi16241606109483467814__cmp_gt_log_ axiom cmp_le_log'0_spec : forall x : t_T'0, y : t_T'0 . [%#sord3] le_log'0 x y = (cmp_log'1 x y <> C_Greater'0) - function cmp_log'0 [#"../../../creusot-contracts/src/std/cmp.rs" 77 4 77 41] (self : t_Reverse'0) (o : t_Reverse'0) : t_Ordering'0 + function cmp_log'0 [#"../../../creusot-contracts/src/std/cmp.rs" 116 4 116 41] (self : t_Reverse'0) (o : t_Reverse'0) : t_Ordering'0 = [%#scmp2] match cmp_log'1 self.t_Reverse__0'0 o.t_Reverse__0'0 with diff --git a/creusot/tests/creusot-contracts/creusot-contracts/why3session.xml b/creusot/tests/creusot-contracts/creusot-contracts/why3session.xml index e070cf024..35b07896d 100644 --- a/creusot/tests/creusot-contracts/creusot-contracts/why3session.xml +++ b/creusot/tests/creusot-contracts/creusot-contracts/why3session.xml @@ -36,6 +36,16 @@ + + + + + + + + + + diff --git a/creusot/tests/creusot-contracts/creusot-contracts/why3shapes.gz b/creusot/tests/creusot-contracts/creusot-contracts/why3shapes.gz index 5ca92942f814d334cea05c482fc7f82fdd7f5216..9e703dcdbd4cf56b458da4060f14fa069a932931 100644 GIT binary patch literal 23838 zcmV)FK)=5qiwFP!00000|Lnb4kDNJ@Ao%XTBHwDKg#u^?uSKdb+FZqW0NLFS({K#- zMc`Q#T}nx*2xV8zuU{Cy!@twrLkiVgS*XnP;9(@~qS4IA@BjLzA0Gb_K9$EGek-3J zA3lEgzke`4{L_CrgioJ8<}ax{{z08oD8GDq`uj=UZWSriD}JU8}CivhJk9t5+vD(TVT3i|^jd%1>~@SqZNDZnwFU|4rr|Wa6)0 zg%CqbLt(mKGzf9{Gft|aR84x#mK)Ac)BU_cN@qn~E16aL<V2ohM(U3Tpl0)pzdcic%tyryZ`dJgs1ZP4{Fg*pLkk3@5(1V0$ubo zCwKDm)^=TFPWI#%Jwg6|Ue2->PJq)H{Tg0}KR?ZC|Lyaaa(DQbc|SSK1QmrP(NyC2I2Zn(6<%iM4YtIy(wox%6H;kFKY-0&4EzJZUP#SPC|@$DVHjT=Ul z0@u|$?5cOTsNUg{dWU`W4r}!eYxNEr>K!hsclb*64qu_(;cL`8TvYEcQ}2sy!3zWJ zZVP^7udnMShRUpG_*?k7$@d?h}X+ug>xws7yKqV~)#y}`Cb!@AEI2RAYj z%ou5#N?Y7_jj|W}?2&cdX^*BCxL8JdRjy5)@j-mtno?2K!-=ev0_nbqygbZ4Qf>h1Y%47=pUZONGI#;s_3^ku6Z&ObMk zf`xMFcK?ZR{MZbD`F*HFQax2zEE-u6E1bB0Ldo z+b3Ps2Cj)uq_-`nu4;22b0WJ#SL|!IY$0+d^1B9MSG!>j-P&!XKh|nz(ogC(2D_!p zQdRez1|0s_bnvwXSIp5Lo94X)WJBpbuldy(tX1vp^1W-|U*I|XN}hum&u#L~7Jr}l z?fG4#IMn4I`Estdnm`*(XBv8Y`05}s(u zLwKTvvq1vHwD3P{_1tc?a_`8jSe+PFb8V%I!JEXL7#5{|2gHT8>xsbWk`HBGxyH$k z-)35~TDkA&u`}eVdJ7jj!_MorSGwufn$&Erac8cJ%Dt6tPIXqdv&KCXEvvWH@Z3AH zHS>l4WP?Y^&zrTP?b$3_3Am?U`-qmh8-5(byYs$$`18|W`c#M$413;h@BaDCe`{Ln zb9wyu{C5Nv{@tuqA4J=0a8BdElL`;{q~0uNg5#DwnThDS zCn^41>buACYbVm-;X^Ke6AV10uH-)ac)|hPytxdNy2-!ZZZVq%G*{Ln6@~ho8oJ*s zy<4_^_3FgpXu97no@d99__Ssvdfj)s%{)5>P9SK766lKK70u82Zq2!W%}~@ zbCK?S^^8Gi${@7IAT%%t?KPOLWQRdun?WwD1TL=xrVRGWm#3Z|#6cN9e*XONKROPZ zbK3x$vB}d0N$2 zdbe!->eWe$fAoI4c+R6N{5C5w>%QAl6Hm(T3~{+qii%@1L_LHOgz zoy%M8Y!%jL!nC!o%hxK`t*ExrY|=4o27Tl)~{YkIOqiGey99y ztG;i5#$IB=u!j02~T-+uV=OZgn0O5gsZ?ytxj4G?L7NDF!6 z0R+$FO;6=b@5!4U1VZmMxLb&j8G4wrB)YAo**CL=*kK`dScshw9fl0)1=%L$3pRm{ zQF}M$veTq$&MeUL{=5)3pj zDno+x-64GW@S!|Dwe8W|pa0UczdGGB{%KEk`lstqw=oAdXn=|G{xnZuz`(7Vx5USrPcWBFmQ|b+k|R!p6O^Zb{u6KY|kZK-jBE$=N-E&pL43` zXjSxEw`!E@LFj>Jkz0oDl5@q$sNc?c7e~d3wBT4ASBhrIv1rFSyWlk^9E<)$;^muL z2Wq1bU2Cis7RPu@r3uCQnRT~3Ccp2eOBybItf@Nd{^#=4Jc?#kDqh0QQTYTX(kHSf zGH>MkV+YH#&1*RK*thL)G?=?58jNW&cW-+0zF&yzhdje}t*_ezEJv9i$EK|21Ds*_ zNt>?kq)y>qZw(2<~Lu* z?=$T!BG{qTE*1NvYQFQgAVZ_Wv`}wCxzMuT`Il>m!;dtdeZ0s+am_&S7Ve4ZIjj@Y z4SaJ3`5l<11AYs~#0k5kw<}yO(H=&$&6|dcXb+vPQYXT5(Ofr*jy@4K-8i~7LL9UT zb&3&3y*26^9MK+PuMSV7&QQ5^HGr1aDWkT>QC9g>(bjXWSlc;r0F7$fY}@ z{qX5?`Q_oU9Ja(KJdVxRqgQi_N zo(zuz1U)0uM7QXbnY`AA5FUm2Tl!F7+Y>gEWm9!^{9$IxO}&M;f&TD##@vW5n2_=j z&Ip5^3Az?jl);TGFyc&9gX-4`0}N74devGrsLNOj10;!5ZwXd|jwgaQQ>8T-06TRC z^JPm7>>%#dE1CI>*#sRA&8hql{#~&7?`v=7fV0j;Dk_#A!mIF~Lk)kNX~pwQq*CcW=$?(< z&qyfx@BJiRX3-C~aQn!BbB>=)@)73qk_?Nc*D;3{K}wPH$U`bYyX72c!VOl(HZpzoUVEXM1sP0g?gJo`6g6&v! zVeK83$HNuTi2r?6Ao^n%;#Mhcjs1L>vD}?oOwr1NKhbZa)s5{t=i=rOm!5}FbYhKf zVzhSvt2Z;V`D{?b+nFtYLU*?1-%L*dI1Dv{#rr)YeZ-$M<2mTDoX#yK_-i#=o`=p@ zo9g_{Q>wdgO1*(K#nZgQnx@gtzS$L-M$xx3*6LV!WU3Wwj$Y$&2*1xegOm8jq4B6A z`(eg%b#5_bP4n%#Ri^q3)@)kD@42p8wrrDziFbUlVpeZw80jc5;-a&rMual-qn<~A z{S~J^SNF$rYnl&puE0r~nKMi3?q_@V9H}^VI5F-a)jkWU&v#5MR(+FuYDDUFC)E=C zcW_nBkoruARoZanpFM#KHL)3o{M{dWn?Lpfo|k^_i+GM}aD9?w%7Hz|zoswy^> z#3VA_Qo*Kw-R;NyTY~6?%6T|QZraR1t3~a4;K`pb`3n|J7j=vD6W(6{Ur9fiWeV+s z(buwAxlF=J;;#W?)*6n=X5FCRY$$YFLrz5A~pe~~p@Omu6B7GEBR z+^)?e(AQlO?(nYTiH9G$f87hlnlZ_9o)fX1_Xq1_KIn6p=b1z>B#JGr3BZsX1bDww zzRWDcmXt)@W!Gh=N!8tEYS_GxH=$f;*>iJGA<3FiXEMRvPR8IL8VkQ}k9%}99_oig ztsyfPPc3_f&OrI?&~`|Xk%Xn!Cp{y(8Pjz1Kz2PO>DXabPC(mPKlgT$@i$|H@rk$Y zmA{svHsK&p<1bj`sP0k-wh#{Iti5IOSD@nvPh-CE&c5-7 z!4ExT1Vc+TJ#T%p1V*!$PJB)d-fM8qK)o`>tt|e2isw5^vngIltK8YUTXyEfbe_q5 zm-=`%Fek-}(vCDO8u1wZctT3&3r=0>5Mie?;AW*li>p7ZV4UHnG47Gt-N+f(G@1Q6 zSdq>Xjwz|_^YC(>?YI=$kLi?#3OU8LU93zDrwc&V=a{%|y_I|*2U6Z3)A<-QBh$no zH>J~}c)B7GO6e7)V3o>H`_MSFT!tmB;7qI#&%}yrVnLcL;`Mqx=V^y{8@1#arVi8X z*KArtmE^{lD+HUv**bcz+u!fy>rAhUy?WI!be5uX1pC_R#;(2BWQ;4Ioh)>#)!=Kn zxabSuudRRD^{V$~&Ms$s{Bhamf}D@NE;CS?;k^SYd*b%^Cv*$mpRB8M8Mzf12RYdB z6s@8dZ)Q_!Ro}u0y~kW0f!O8&x8MPHD-TQ{KZE>hG|kBG{--9t-zUFcc?{>|-%hX& zA_;5CZ^*~nYrTKxir=~7QtxlrSQ zWc|-zixb*!<%c%niPW4CWbTV>#kN&8($ijy>l{R!k$xo`JEY(4y=I&nh)#XRYM16e zUF}daA-cXy^f|1nM5mQSxg@$?5uKh#bozFplSsc=5}lTo-Vopt6L62{yh*lIQqm65 zw|lQ*f>$C@FQEm*bpGD*e>R*iO8%vz#Z{SKoGktU(jGUZJ;ZBr9yjIuYB+3z*mHN% zaAhCnPi0KXmk!}}=kNRm`fk<2A>6x(=GTbSCX@>;mluwjyX5}EZ|~lX6kQdiSqgti`u9NZ*p3AD~ zaEr_0A~O%&UR>RdpxYG;SYOZRjzovu)8)h7;Z8tpn23iP*)z3h)n@m-BkLOM{G@ZS@IJe?x&12NY8EfnckU@ z)S}6p7ge`zREus4%V1j7ZJYDLD|r3h(|yhsJMX!;oN~_aA2!~3?cpXL)|`vZ7pQJx zrM~%Xobcj9ZYqO^*-8Cb^O84X))SM`=gmxdY`Ph7Hn;YLqubn!FE+2+rG7ek+dFZo zWrrOUpXaW;ZmeJ41#aDOp6S+HMr0@JUj$}XZq4pe)JtsJZ@$`ac;Pq-O&G2{@=Z7K z+6l2;1m9+VTChLe%KqOto3CQ}HPL5GPybsmJ?}I9BILeedj4jn@AcmWeix;4iPblh z(sfVo?`-}%oByxR<}VcKl6TW)T-QFja2wZAOTd{rigC#6IWzyoOrVz-|7Nc523wJP z#_qiGu;bV9d6UWS$>42ftL&t<#(5~IvEPuJ^zFP%S9zJP@bXri=9?6Hm)beyqVD4* zH*pd8)V@}IMr;Rd&c*5?7r(&xw{vkDZ0?F&a50cV6^MTnzp)7sDz%KjmUrhp#Uac#XOn;*;M=cZ>V>e=4oLo56f98NXeI z@by=d`PVVgdiXKT6!zPh!tEQRC%2a=Jlr`sU&2!DO3Cc~)!E-_`5r6DgWJ;r?h@d) z9%${;H;jgpOcl|A&F^RoBw%R4X_ej-EqsuRzS|KA^#m_#y zWQ6@CA`&?qe=XjF*W+EF@m2`x`D=~sUQY{lwEnm)F8i-z^}BXkq5Bw<+~?f50!3zW2a5ENA5VI`5~IiaGw#h#v%3N9n@l~l zNoxM^2?Mgzne}15uG2W6yMGSwZatF$g_*x*y zw+lrB+@2xyaH~w8;FfQ!?0h+8PRHpx`sZ2F$#-L#lfN5&^!)7Q&ewRo4*KO-c`1DS zbryR(f!UV({vl*@0=*~uled!3!fRVl^!&G5{B2t}`&@vk`=;8t0J?XnH|B)h7k;VB zdS8ftdx>;Y{LinMzLt!MUi{nLkau$>-)>rWoCD$U!^d<%mk;SI8v{NY%Ei5|eQ2#C zDEd7he=R3uZGuD7N3UDTZPoUIkte} z#y67}6@D_E_H4vjmknPm8!yr@53M`(tjMP&&b<42VH|P+hW?H+C=4Fqdnd>`dQNA1bVyoI{@sqhFjAQFJ=?& zehcGnnu}4_Owv6#Fr3}D8hlAt5?{KTsl#R#%0`O@~^{Z!icKh9v&Z_O1_kU(%SE!^n6!wL|t7Mje~47FBh9%L-yq}{gSBjw^q+Ho+s~2 zm$J?}n$|vSuBe~>P6E;eZ2rqtXgd?xa)ixgV!f{2fi@I&N9#@8-O4`~Pe4%1$@rG2IF9D?LjH^~@LDZg1Vl%Muz^v)f)v$U7o;@&4CK&+h95Y?ose0=B$f_P?)ynM(q; zc(Pzaz|0E?Sg*7%%ay3cE8=uXd)|-=^Sc=RE=IqL(G@Y;+`KNGz^+Da<=xmBJBy3{ zc6Qe76_si5mdEE=)-rbSX_pt8%X37l8*-0D77}Gv2|4`jg47hkKURL)yyY4$tWYt3 zA!hiT5_B*7zKoFQTZBYk7m|Gq`1Yl?q~C?(cj5RyRXDCP$~B+s>NqyIHTrg!eBwMh z*7XIR?p@=2X2m`K_)YL`q2VpQ-kYd64eMT@=eWdc(z4w~zGiwWNj6_F{+%S>ha?-1 zrM8}*OL!{b)oJnydG~1@JkdjFw+Byjg3z9dm-jACaQE}%4qgW!LH|9TlRkA{^H{&a zs^0$VbU?El(4O2dpgWm1pbJ0B@7aKTFlc8ze z>)*m(%O!G62{CQE`L2Brw@(>{Ho*UPCf?;oglM?B6|3*whIVWJ)A^67Jw8%Znww9i-)r_pZm}3Vk=&Etk`0w@~^yu3FF9 zbhBG_+FrPf{UR%-ofXshI_TBAnwKt8U0CA@@$KH~=-TQA1newpeos}C?39&mz1VzW8XB(2%J`Dy2a1Kk4EX>z~gwHOZ5`y0dM zCp$~Mv?sc|pMUeIw>j_UA9T@oS4a2L(Z!V68h({qIYJ2^{{HU$2y6JTj9=yWE}9NG zq3g2AB8HEftRQvmm(9lB{Y9GI%F-wJd9eE~(pgV2H+KTW=*vWZ_i*wU|?T}^K%6Es62`Z$ATgYJOoEYxn&0BiC{lb$H! zFSTGhQ0?14uTPV!Qts}}1dnxlejUp0=ilf!kI>-tRGboJJw-i*e}4wif2-(jekV;0 zx0KXyOGynZfjM;LYSi+(bT<75(uQVhF*m0n9e?=Ied24%u6(!n5MT#RK5cZG;L_ee zawGanZ>>R}$AFRQ-PgwWCc>K8C#lYAf26P;zjD@7*i0xqyX*Kg=m{M31g@xVrb|E3 zKy@0ZPAjR`bE)4!(6Ds^Ttp@GTfy{0eR|Z_+j<|?a=&BPaQOj-d zE-ZJl@l#vl6qBZ;g+{>?7#k1zR7mpx88pKd@BR*+baDh`nEUwHX^94 zE#s0Zzsf=OOxKey<7qpgYG(bl|RWK5R#J+0B(42!9;NvH7vh0)mLK?Zrl z*i>7_=2xCDI;q9w-S?T*DS@f|BStUR?YjNvFJ(rJGd7#=f0s6Q;r-*z7;B5~%pK#v zt^doOb2j$7YrHp^;_8FT=gIJMR=eC`zU5FfZY3ye_%yJM8rWuS)zbHMa!ky|tKN=@ z*#4v39#h(HOz4^Z54hF;f&T#i$MQ5hUndg3wu3TXj3Ojk|r@>OR)qyD`j=JTx;}o(XO6%6vs9KDp5Y%H#8A zgHlsxrKa|knxtNYoIguO+(YV;!hRKW_bGapYPI+ zi1@Fl!||M&m*^T#23YRh~a60YP8qWcd| zAMaZV+?Z^&8AF??b3deG`5_(4A7;nD`C)MHbMsT5_imHBISMYVN0QC{%U?b|KK(x* z|JJW(>qON55M%MA&xZH#_ua&xe;88&Hy+-bg&Ss*+=@{RbfWbnxA6URel2L;S`R)_ zJ@|C`618qRTi7W~uj z)>9{e%i%^Xu2(gk+TD2n>7*0vPI06&3}+%3&O|UGbf1h@&sZ}*PEIG=Y5tB!8e@2fz>%#w!S@xDO^FL@Rdzf+G zajDy|r~4+)yky(ECQP=aojsFx)ILnr{+<;=gO<{RmeRf2AJv#1)R-RBm>#!ayH<;4 z*hb8-jhG>Kd)d})>Gg=i{Uy!L zo;NCT$wYq+i@B5EU@>>Au5~-Q)@=hF&M}J>|6^BngL-Ua_2;$Z!GW=>9yfaI9=_Dx z%r=i>yRByl9ZSAm;9_X&Z*7W$Ol*kJcq@VKZm^9vF2#%x)}Zg&t8D#&2ZkRg*O*Sw z-6;A~I~U3DawRA9e}yj}dOx__sp(sA|6kpwkiPr!;ql?Ww|j|`<|p&;aP}0;nl%;t zI;4*up2EY2{;}#V9yV{s%XZwiYmYbPhsS^a_|QGDd(y*2s@Fl@T`s@27=|0qkaNJc zH#yEFu2Hc?N$$5`+#Obnef$!iK8N)5?yu$VkHgdRC%}gV=oSf_`oJd(>O7a{qwJ!m zT;+LK4l8#*fwuvMk57LopQXCNd^1_fK%Aiobr(cCzswAqKwXB|es?q3S&SLkrGqQo0+17lj?@F8zJBnjXy04}CDPzdYFAn`}+{ z-(8Q1Sn1)1X<{YEscE$xez;cMebr#}hd}u9;XgiyPwka?1SEZAZ9x5Msl=UcfOwq7@Ey>26SZx-M4g8||P1H>;5 zZf7IsY~{#>9pQng$TUA%Q(b2v`1S0nycBk9x z7xIcNv9hsRfBv4t5NLFE;n~+e@r6w&t}akqEsnH2zVJOh@V#l=!D;+}!ub6J@r{cW zd%yU5JV=juQ1$}@U`ukgrl!*p5`$ahwIIB3$cUCXSfq_+A)S-hu^~cPJ>Gf zA$)rJ-0Sl()1i6L_nVy~KR=I89j`ZU7P#C9Kh@1uw*_GvExj{ed%| zWZ3WrZjHe*1`h_;`S0@wKqkiAYF_id$38fn>HJ#y3Fd#|uhSh*Ot^EwxL_Co-}RGd z^OAP2n$>qh!$02I@SkpNm>+(-wdpS(^VOz}%<`c&I5)dH95RuL!J2A3SzVRl0+?J% zJ{tDg{s2dH$jW8!4CSa&&N>>l-efKqgH>$&4{)SIFhp2#Md!5goDEw=Dr&6}E9(3M z9Pv<1QqF)WRaXZ!I*vZEtr#m-vib)&@*!nyP2rG=Rb*97He~>C)-hIs@&g>r!4uYk zT$NXeOhAJ^E2{yFaVDtr1040iR|hGiVsh15Q7SqmghI+_b{J&hV2+@Vz(=4X;1S>m z>gbQ|Xb(kO3k9_Ws>+uXNm(>CS!;9F#z}9x+dB~vDk5clQaMEAs#&wr(O^Yo1RwT@ z=7{=;d_+1T9ubbHj^K~r4qU1RizdpvO|(t}2J37jN0y6B9^EAXm`xzZl?<>+5fYUY z&|;*7g_IJq!I9Jv{WgH;Rkp@jgUNa#pCV=FqBoFiNdN)>F9A@_s^XHzU}`YrDrk?P z0JAE}WZ^F220$N)HUJc@Q_=*;UR83GYtgD8R$YB8QAj}g5&$14paMo0ATcGN{5`c|ps8%2>$r|#30|!*LB;**hFeAB308)t>7$8D698_`?vjI&( zzO7Mo6afAVV7&y20j)L)y|O6)a;*-03MT28DhL2pmjHMjybZC|=zZ1NYk;VNh)k}r zWI-asB>;%gdk)cN)EJ5~DPSy^vi602647S71R!E1Pqm=aI=h;jHw9uY)&?V36##Sz zK=Ga0A?Ko18XTEu61qgp=)Eu!^CbW_1@B5Cr%F+5*%U)TDWkLlP1FGBO8_9Llyy?Z zI@B3rK+#Xm2ZN4$6=`I134keys!_&NZEQ5D7Gs^NB_+icx*6DuGtgXe%vymf36n3O z*iw|rzEtOH5CHBHfB?ZF#RNuW$HC@QT@dwab--fuRgF}W0`}3{s(fPSTun9Tq%0N% zkm;&MN>+RAtTn8(EitJm8VaoEoTIm*k=P%cu@y{arK&GRY0s=o)V3%lq9STXs{^x( zuGYlWa#o66aRte9QlzzU*uk=#9cm`Wnh2AL(FWsybhZ|&=MI)CrsjmfL>p0u=pt65 zauO}6Y9p?O1F52dssy%%>>w29lp&6&AR{#{)_CA7l+GBEO^ig~yo)NUpsaC;TnEe8 z>T}Rc)=+fb78^ZeQ=zz6sc8j`2UJN#bP=Pf+PL7cgakDp_=MQCf`fumE9DeRW~00} ziV{_=Y=#^-mJU|6k)wf_TtH=X#T=^g#92G9DTW?a3RJjS56&v0oH^Q{OyXoUQRNO+ z@--(_Tu{-nQpwq>$YxZ986c+-Uz{nFsIniOHFKDbp~G^UzNF->MFY!oXI}f zP$(JJC42O!I#}8J>;l@F5EU09PYF|HW0Uqd^>j?70NO;z(VAE&vsbyQ#Iy;ym1(L}=CN>7pC=OoMXyItp(fFfrM`Mr1 z9F0C2J{me2JQ_F}b=3Z--BH`4Hb4XJ(@_xyU|M z5W?qL1qXQ02o<8Ojd3ZLP_Raos*jLsVQi~8C`}ATgHxtj6UkF?&RCbkwxp)XG#p~o zq+;^kWsFpk!WgMAr4VaYu6Fa1oe_fwi$<+TDGdg6D5hA}9C}{1DJ5eQCeY0+1RpRv zM?M6N#r11^Nj(C^nG&gbl_2H}x-e&#$)d?vDqXeSoFhkyVht2@s4iP}I)xC#LN=tY zT5qfk>&jYbsMSLDPN%{tCmU;Y?QCF4%oCH4T+lwChmb3%7}z*v73d^-#qxoat^rUM zEG8+N;-Xi{IA0uL%pI&KB$ktfF~+4_Ss9xdOiF@?nmbrASu9EGSRF$0HGn55%*BZ` zg*Ku-WP_e;jTn;#=dqYz3sB5dOjL~))*O7MOfF#%1#4=A1nk&XUD-q;-@#&QJk@|Y zMg$}>Hl}2w&m~r}Dt54P)XWa8C?=g#)zz{|l$0WeHkS@oA~VvdHY7k;bNE74ZY)}Wy{hTwGv%T=El#VROPc|?`HO%4^K)&QlSS5;OSG{q;t zis(!6j;(U&Gbdux!7>p{EG`=Bl}A^SFmAS5R+VhioiB_pGQQ-T*#)-RD~`S(F?r8o zU+dJbF~=+{>tm2TrYNT!JFmRs?5n9AEcx&vdRHs6b{a~|**e436Ppa!&#RVfzz23k z#~gJ4uZ>PrY6``3(LKH*v8$p$y)7X?ByXX3t|eMaEL`Z+(fXrx+Zxr{U5%=>D+DE{ zB%53|G1=r5cuPe?#Lx-l*TJ?$S23Jo)!8WzO6*$*RLB|3Dt9;tERQ@=aZpmtItMYC zj0dX88ZbQ$QoKd6$b~O*c)9vWhf4O1`|Ddi?K4s8rlgH z57{UnRsfEJYvy0Iq;<}^l$ZxPdvdmtlY?$x=K`3Fj@X7$vaUY#JY&5txmfK%Cq}3x zidN5x5i{wY&J?n7UKdr2&01Uofr|97*~_>cte4ayCC1`&N|*yCbOk+R;4G9zQmR}% z>DEF6hrY8b8;rTShGW?z;>_# znW&s*lbr@~488_cvxj7=Wo`O-IWZ}#wV6|4NLp;fS|J&gN(%iNGeWeW8PJI1Eme<& zVp3M6Xt9)+#~0*CHnI*m*-A$CIh`np7enz%Q}(F5sG_KI_EAOE;lN^zI=PC`6RVWTSUCx?Q=u5!&ccEN2QlkfvsXZ- zm`Vy!42@t@@kVIl>A*ymj93Z9TeewyFN_l{dK-;xI!YhBF``45xe{lWTufD4%qb{i z4ED6)WR(huA!bvpau6*Brpk%E!eYC5nTS3GopUvzV&$AnC8()ngT^(>!|{P~^{8A* zDf^(r)dpz2b3_KKY4)(wFRDkBgMyV5AS6z*S5i>HQxtEnMSayPn4)tr7I4~H$Hr7; zDT*u0s{+;0b+2G`>`S&j8ed4URoQz|nu`{rxlxP{C41t?S(jQ;VMP=)YQx5f`50vw zuMf#likh7v@w_`7vqKBU*#P3Yj6EzlTx73HsR_X=tS(utm5WtlO16VV1&qq_xQc!c9W3v}8^J*t=W8h@HFTz$ zL#QRI5mv;6wHh?J0D5xC*%ZBTF<0F*gy0KZ2A#91lwHYy$qR z#)RBFCd?hIREts+G9i=EoNcfKRR>+Q&8+%08VAZ|u0cG)9IJSd$&&Yh5?kN2weK~m zaYygAHLCU-8ddCmsGuW9^w~M@h}oy4(K1KPolt%qY^Wtu5hte*mc$ick}H-?^ku{+ zU<^TrEC(cuU_7%YP0^=hO72!?50s(;vWht&$l1rX9ge8fS_{gF29!F;d4@FSz^de` zb9P+hRH;G~uTxV}?og|9R7jlb(I!xoG2sH=g!J!deR0_CO5=VR}fjIVyd_hH$MaHWm z+4>n(#*}o??aWMK23-xIVAe%N_P!JpuR}CBd!>?BS(8iYY6!&y;-VE|pjk_Q13X zu867TBT`Cip+rV9IvGqp^uWZW<)TDXLpBtERj_h|DTIRd0ay~RR{&qVv7UX13Kc_D zth6uIV+X8a)GDS@*em78SYKknXroS=w8kEoMWjLyN$QedOH`)D zP$M8g5|`mHvtX6hNkV>>J(z5SeMPNlwoY|~KG=*^<&2baLYpF(%350;h5IY<0IVkE zeI})1$kCe!HiGgcO6V|y{|-3AP)wj2Tuv!kpLHRRHKOJeFg3@C03)AJ1=-+j)R4V5 zWGk{kEJ_us9WWqI1`30Nz(qj_g+VFL#eu0^{93`m1UV7vtaZfXa{Dq|=&Z3Ghj26Y7GkD%NUls$qnM^O3*ijSb^2>P+~Nt zSdO6@7bw$;KgGd4aao2<#?N{H3v2rk#4oq?bMzk{0Ln6%eg;nx%9X8mR)-!~ zf+AYjW%+0r8Hp|__Ew9lk(`1K7-S4pu{d)jwIra4HKAmhFozoTKuztS2Au;J$SOwMi%vESz}P0IC@^TKMpqM(_Oa$nL_tO0FEfxY#MOe*Kyp}C zT1W{xk>c)10+Q79jjEQFcyO74D~UFDm6I0#q_xgs>;&~22LaGV1(lMhbaA+<1S)%1 z#BG@r_ju91#%z-YQYKkewG;>jlTtQN^_|iR2sf(lHokktizhN@E>>#iUBf zu2#)dB9fD0;>lErQ%=Zy2;LCsLc zXe%2JIiv^@wxSXwcgvUBS;v>tdxH1kO;U2&5WINIMO$Z`PbnpRJ-sKexTc*d;;>?C zaum)_XqC$7pc7g?h>u@FYD$h>!Bra~IAM!Q0KQ`ZK4fF799k7s3ZB?0Ws@zjWUEvG z-2=-KvPoJgODRS`uqj2(7~2t)O9zb5g2#jkvyy9~m7_~yf%L${@0_Y}3PO@y zg0&6kl7NjNwb%{w0jviWhSHf3q9k9bh?#>c62!?punI*(MldBfX9#0VIV4A+7)ZSe z<^vXM0%+^mXb_{zK;RfuVUi=E>47oS5RIhJnWB=Zp1dPST4dSA!2L3_55`8q>K$e! z`I1^|Hm)(4@jWn$$&y1VHfgPG24iB4Kqlt|u`{XpApW}O6&e!XVk*tDO60UvNhJ*f zHK_yu&{~qJjIpVfppDZeSQpTI51eI`Og^K?SLc+3TBD7!IY5!@tbxx2p)5`lNutTs zu#wPvi7u;{DGke%$YvC?+AG;eD;P=mu`Q5lYV3i9m;=k^X~j8ToieOlE>?Ed=yVTE zLrjUYmF$ERN={sgBZaPptPwkXuD?~)1}d3}YUG5bdci}`#LA`;ifQ3X=5HND`|MRM z4kLSINtdX(urna(sE7mk(SXf5R`9`tm$YT@I*R)xqt~^^OOc(lTIUQ$s~8!R0~5I* zdhyxyz*NXNm{gP|2fn#xB(@?chtaq}Gcd&%s*XX_XYsOIR|8f{E@nwQh)j@3Q1lsW z%n&I^5Z2aW#VxI4fDTxS2wJ?rRYi>%OhM+X#Wfimt3l29Y)y(bpal5=(P0U>pdtpB zvv%J>%{XL`1S0L6__H)>lE6w^yV!-l|xlL5fxqZ@p{roh!+b zQS_04L^+`mJynTy2}T0)wm)r}gVZZY=96@?#4(ZNyjhn;MyNYfn?o#4qLv{bNk&ns zmbl7ZL6D>BZB26^1TP1Pi0mYpFcj@H8FsO%>Pqf_X@l9DsL5f9rTU^`wJ6HQNwBUIWeFsvJOFd-#p6qak(9R4prple(3P?`%_L=W z$Vr9h(fXP)=ipS5KvHEajtd0tfytyqo>H|~VpWkHDFeQEtul8Tw-K#Tyh;VFW<|!L zFE%4%&XGdE0cY77G%;q$ATpr5#C|MklYDd;S_u55aYn_5A`Aht>uImi>!8Hvo@3}z z{c#%w2(JS_f#T7v=D+)&C&dbk6l9Xk~;zGrRD1NM*d{voaRNCYLXEv3V5SGEJ ztg^U#SV1Ohx!4Ll&LBheEyddz4Jsu`iegA9f&=J0j&l3p+f=Qs8Yvh^;9~Pz#^MVF zn{;u-w;VAx-#SP{%2|?@#hs!mWCn0SP9$R9g+cz9QbJZ4Kt*S4O2%tW9F;_InA3pd zU`S#)WF?qsVo}+0u$&WRsICWwp;ngTW#y2-nqW*oPBlTa&a{nMGy@}sT&+?u7Y$qr zRkAjljMn-0YOX5EYder1 zfP9sVW{@zE))K9>wu0vpBWLp+)J)1YOIS*4#opxNQ>r1DB4#R?mb7&x^*l->Jw&i7 zMwQxLS&Iz>889?FT~0lB9;_Unl1ZYKRI-^^@_t=SF@{cP-N9$%z|1}ruSCF8MD1%< z5(zH0O;l24#IMAz8VJri<#hC93&pH+>9UUn7$=DvRFh0b$?(+ZfZPiTkfKef-{*^f@GwE9PUH6ak_(!6e3F|n-OkALySI_ znyV)7dVZ3`O6?Pd;KXt@$%M+mIA=5}rEI4G+#xs%*&(8Lpdl8efon!km~&PJdtihT znvl&KL@EkeuUIkpY=eW)T?;rQ<*ZSGqBBe=$t5a!pCOuvLHCMI0wq|{=#Y*0RGLj` za>_~B>LcfVnWl&*#yDbce6SQlh@gZ4-W(z0Pf2W!*aOQXXGtpy43xBj#93V1Oon3~ zX7-{u6B*&`Lsh{-QYu=NnQc@6m}4GhCI=I7p{S^RrsSNp0k!p#Ne(X64wy1XXp*vG z2$Dr5SGpWl65iK-z*+K2dtJP7h+?QX$F+*hRiouXJ)Z>w%2e55604di6(A}abFeiz z)0vL`n@#6zY`_`|1!FObQb=-F076dSd@rcqI7m)f88%2&EGhPyy{RsWPXd(h_c?b! z<*Y6>CD~Mxf}*vPy1P>EQWf| zOF6Pw~f(xBHZU`UuEJKstD%B>a;l zb1VYn=Fl-NMr}OWcF3WzF{%=kPO&Ph6+xCHd6%o-;)Rsv|=dd945F(OU2 zWr8!duoa*=H&-eZizOSQ4R~--!sQ`~J3vEI;OE8>vX@Afb5gyaMQG!Sz1`#?h zna@RbdGHL7*rj=6=gFrKw4~&)5nbtZuv&wHY&*~O1S2Xrr=sNgXtX}Z=zOIDNy70M zEzK6Gw1<*ok|cA2Mm8ycv!!a5LtluVyPLA;kAUt7 zXd7E$5T)p1(xTFHRM8mgt)#!EMD3IdL`NVz0?BW6&?K=V3!a&w>RN)BS)9a+?p@Ly zZl)ca*xkxTSB;$Sv(03pk8%q_cL`AQ4hb+@iFrwi8Agmy!Po?BwMn5RIsoyki_yjx z#}Xkk7^)-%2qwIZWQzQ--e+ zkp}IGsR?xufe8-9`O`K#afokpl|?9Blvjbg_bRHAa`HB~tV(w?X5Q5ufow-Hk_G5P zDcYCBk~x&g6cJab&U;7R7Ej&8;UWm~RxT^*F#2jjHhoTK=n!!2SrLF|`LsS*48GN3A7cJrrxi(dx75 zpWZ(J zLNtXHSeqRu%GHKyT}yWZZO7)dC|3h$!>CkBk{qw(#ydK++&M4L6L~HPwfia(YX21^ z)c&hTsQp)vQ2T?8R-1M!7MzMXQYjWQ$7&Ig+ODh)L4lUb8kMb8+OS-qmJp1i94t0# zfetxg%hf3ra*DYsR~?aDStMm*cMv-$jDQxkvXY8x2&^euGWon@?lq1v2V|GL1Y3+k zt3w44H-N25A}kf#Mt0E6y0s`-;bILLO|?inFDd`3DFZ`CFn9zbzm?>>`-~}LtyR3& zhFC`<*F;>^olg#oIfBtgFg$XL&te7{r#)genvo(qG%6*utXnjZR-L$HWu%*S-dCmw z;1@ z80f4~YmZ>f5v)Ffki(q$^l}5DDH=9B%d53fIPfWpqbqszY4U= ztX$G;y~H~tcOuD6m6Dm2HMW~I--G}O!XQJ?!2)AMjMWFpx0P%X+s-5AHcTeDSl}rr zOUj!dUW-T?eaPSfw|n%mjott%v&-Jc>Pi45P8{!3O%3*-&<}7MaKl9+et{u@bq3g~A_)}QDpu&)y=E~|1T=MXM)V$d+7O-{lv66BN&7`ayBN*mU^_^=stDoJ~eTy2({4YFsL7$Q*Bsavgn z@nPkHAL}9xGw~!EiBV>wD0q)G+cqrViw~?=pP!B~=dE*A$B*?~IdYTK@mu&g@8z zo7uweZG}uo^{QoW`n%%KUltuM!vTr;ls&R4!eqVq-^(QnR`k_ zJ<9C}!mq;b@65WP^5J^i34EO?iZmzBHRt)JGk`?AxidlrS(iZ1np`Lsim&y!Y(stL zA1nw*%YQO5)VGw>A~VWC{_&tzBT(Nbo%FJflwTps1~22AHqDN*kg^M@tSsf$jj$p* znS}JkD#*LX>cvi0$=X*Jj&nbzF9K|#&oOn+J^EQD$VcDhzsI5bF?*d;$~=H9=m8i6 z{1sYDyx$e%MawBt;Mjaa@QM2MEP~Maa#}QKteZk+jaP!;kR_BDs>ZqI7`yk4vOup9 zU*Z9dkAvy9>a^owa(rfyIcppc9F`zeeOs+B8_C@^iJ{E;3Ne-y?EX>z{8TIA)n}!# z(W_UJUW%Q?+^crV0T!`nw_=mhA^kb_thy{38+ci0SsR<&Gu)EdQM8=3ShI{tPAD(%>3|m8 z{o~ILTx0vBa^{&)ILc7LO$oUI;^_BwwEXFz6h4Cnoj{&IHguwW4j(n_9O1h?`q_b% zWcBoEGoyfsMq#Ql&m89x#o2+#69D3?sezipydDy1%z z=)0m!k?Pv@)Uy-iaQD&i{IdxM>C79uHFj<6(%88%?s7-&tG*73Ig1TGfKx)K?K}Zb z9J31DA|%G!;%_wBg9hk3!GR}Rb-AMo5GcU&)X+0tLVu&lwaRBPb=sm&nkGYFQR8S4hcWjYAv9&u>JYc~u|7KyFjKh>)S*-Dq{W z;x&%=v5D}nO`y6@OS*DFN_t4QF^UXF?Z>&#Iwv(oq~IgY#euXrgaAT@(*sIm+5I?( zlf}j@3;ZD-^iAM_QyM2X&hnyUwOu!=4SXLyMQilK-l;%1@M9R~7Y!kO;fD0Q>q536 z-Ig6k@{G1px=YgZ-&$Ph+=TH##I|vxzjUOZd^;_isowL%*Gja zn&$MzX^r!*4GY*MMvzgsY*nvh+m;lhJ5iK#zs-BQKvsJ~O+6fiql?5K^jkD*thfhQxaM2C zFxF-@t*6YhSBH{rd1doFzUk`w7%Rg!cEJ|Z@M>do$`w*7qb{|C2lu<)6XLHg;~&Dl z6M9mOMRj7ULgySnXzN)W_}FLu|HZ*;Nv2X4$L6odCWua#Rfvsk#_tbi4AiW#IeCn2 zrv{QE?mHvKP1(?|4nT?O*hynPMh5yyTm1)<6xX~8%ZBz!;gn%kW z?7IRHiC-Qbd;k}qI*?)N5WZ;db6|NsA4QfFZ&IvD(I!Qj6mEh|!^fqU0u?x<3RnEplcSl1%}5imkuc+Z#(^>>dupA*Quzd8lzXUy>iu{ivWG+>1%M3 zSmdc%KzexTs#gCNwzH9F)#cYo-4l0OgWrPi+bW1#hbmk_E-}JU_L>352u~|Ybb1%D& zH3QJRt;7#1UYqdyZo@HATHuS804)tJ*cK>$&+?D@YhiD~?|TbI@Z6_HOfDeKFfe+D z__!hoeBT2cZ|%a^YdTdM8#V~lm(_(W2C0wmCvHIrcpr7H>IUI8059;Q(jCHjvV$~tYMCH~Y$zGi!gSXDj10ejR7y-t5`OrMf})w4X=P&jp4I%L z8~??KB!jrMYiB(m$<_fiPX|A|l9m0XEC102szV2m2v~|MPwz#5PcK>I#(h6Zd<5hp z0Z!&%$3mA^4)g?HSyZSvx!F&_a<&l z9E?0^;@reb6Q?Ftn^-onXky;Ptcht8lO~8)uAvKB0MJw-0A~?YU))lvyc%1H@-@Qr zLt<(V6ys;d5ny4gK!$3n~f7VZGv_>_p7kPUotc`G9J;Nl26U^+peB zG#drEsNM^gvRV4vDz?Us{qRz#Nz^8hO(L3vHwkMJ`u{dR*?CMs8Qs}uLbQKG2^1r! zO70ld`swB)bB?Z8Y)y87CMcYM^3M)mbd2QZdk^>$2+^#Yj_gfJUR6aP{i<`qfQ2$s?co_$`~0QN&|PMxAuCj? zoH1ydFO;LKn?#c2&-WgVP^Fp%mDPDLYEN`{Cy4&X^KSV3;9$<4b}S)3*$jg!Fp?eb z1VkTi@8$E4mG?fD0;^s_jtuTgt|kyLHOoPc^g z-$efLY0gj%t{n(i+hyMQM!o3qrQ-_e{*BXAOgIa~f7Hfv9k$QP7)QV*j_2*F|9sG@ zZRXWWFIqa5G`+656Kgh-=TZC@P6JTj+6Uo;8EY$vLQ)4(-77=y!nF-7j?CH(^eDe{L*bA-MyHq&L_tLvk6fULbgrJ zM=Q0m1wgvFP!;yS+29wD%iGpIo@bDiCAA*XGSBrgx~K`L6F)xA&P41AnYGkDoeXTQ ztb|u)d9H*0*?QP^=rkNw5fDa_u#_N0u;?Lv(Knre&s43!F%EIAc>qbz1Q=n=hi(Fy zfG$hww;Ct?Ie@>*pu&9SKX2Te1Z zQoK<81OzWt@va*j?1Hj+<)TF&d2XSmRPV>v0K#%!{$|0AdI`I$JM;n=+Vab*AJt(egnqZxsKc; zI*4wv>)6!iEwlucb7KRwwhhwmE39AL6Qa@X^+U8#Mll$M!8>bP(9wXtuQ-Gmw>}OI z02`h^l89c6F{Wb}mbz$-N3ZX%?FvZ9VnCq=mS9063hga~@A91n{(Dx@5H4go0e!=ylJtfMVl6RZD9Nl6YkJOtEBYUf@fAwDf>~y{p`TJb&;Z_ z>{(%9hj}1_AqLfc;bvOu&(CSo(_>YzManTjxdmTEtZh9{dC1QWoZyWvUNf#m)j5Zw zY-F}J+l=wc1OM)rGQD=@QM=m)kp+iCMmDL#8ty#do*%}P%QG~9x8w11?mEs8l=xtu zEZl28v+qw2G#QX&3J1-;r>2%&!3!=FaUSOH_hb5TC~3EtI$+MS$-oWEgt`-@cRKaQ zq50C;!mIM|gwGNL`hDT%-)?oC5AQp!O*xx#G-YqfI9!{uG-ZCxx#sB+dN_Oc>>;_q z+*&p(U3XFWZ38C&m7dZoX0e0aK`G>1)g3yx3w@*CHUZFKud~NFeGPaexz(Mp0I=!t zWD9@S034Pk_9s+EECZbbRO@+0Bwhd)XQaPvVxd%bnRmbvCTj5vo=wjfQn@ThlZz|SQw5do_;igi4d#bUZhfjy`Aa$|PS79&%VL(I=CQtcaIaMf>_(L}8 zfcoMbHRO_(LA26`Kvn*gQ>_bnlS*Tr(}k7;6u7~daySy+Q$i00sHxVbny*^AR5H4TsZyis8NQR}Ior>84)LaDO--AcG({~O&$4qci$H^uA5>E(6h z9IG?9JabVuVXQ-ExU=8qSKXVsHFdpTf4FNMgX)>xA;|Es8c95lWbY4fC!g=)aXV%x z>sjeWKEOL!(Q6g+0_6L+Nd*mV8u(33z22|iLDn5-O|wi$oWb-(2}J1Dp7;BNH4SYV z^6HgU5D``vhsUZ7-^D{a5Q+~5IPpVGqc)9f8qqZTWpb2YYQ+lrb?FSlGL@cXK=E=9 z^`>c0CsUiIG);ajDggAKS(hmm09**((539!^D67$S%PMOEn=bOxwuPB}4vb=F=k`Qnw!g*viw0e4B35iY>u18;oz`hGW_WUC8Ev|f%@E5@BsPgH7;&L3>^KgUxRo=-KNCDA_w zV*s!<-`qv`yYU=Cr!rQjeFs}=j0HX4IF>L8|86|jfHftN9K+mpc%~+-YHAVKXx;H7 z)3Oz1z&I~>eiM?eP?Tu*@+|SEoK8u2Rq7;Iee}#29A1paE$!BqWyf_!$`JfLpc{~} z8f467&pP;3wj98%K(Ag1wrec|mW*npD3|ZY6SSQQ25?0(Y~rRcAi1%>i#5I*PpG80 zBQo9x{L;@U>0mF)X5ohw_04#KOGvz>l)xsgwr}rod;u+|8i@`H*hcDaqzP;b1lXs9Z;#u zAN!JU(aKFL42G#`))%%RV@YM~DBznFIY7!YPVVxkzpFQ`*0gHVDz62&$>QiYFB^zh z2FwvA9CFWoo>bDl&t3z0pH0k}D9hhwFjSF`I}7FnXRXy2th5f_Z3PU@3#dQ$rr{UR zX81bTFLFdLgXRp>$sB<8Ze`$$uzsc;w3wAKmz`Ru6j84u&wZ7>4wjlS;7APQ$e4Xo zx|CiktX=lAA5xtlTx{56TR<}pfLD;zc^(Tzf8mkwQDoOBpu*O?@_hm3Y1?CP0l_6^ z+nP;bMdN}BHAr@^sti(ZFWCcIMZG22M$a`e;%0=u;e>$KmNRaWTMkA`>gD>@vmefz zkvGGg>iDBqSg6Vs2LOo0?%eocxNl`9xTf&f^kJW?TXG1hQs7 z9=-BEqo};Ols*Cgt;(>Y0Ynqzaw6W36?8T$(X4p0^3l=qbQHu_Xc}RX3-9fLKV*Zj zxo6e5{`woWt1asum=VZ9S$NnlA)%*?+D0M?ng;^lVD0i2(wCu7_ANm zM&;w{)%(!^@VSmNeGiRTfQ(fw!4*li=jM;+Yn5@J*hhVyDKQGQ*@gfS0MCwl2gkz? l12BQoYdH>J@tC>6_2A_i^O27m)HzJA{{tWPt0#kW0RZQkmCgVF literal 24505 zcmV)MK)AmjiwFP!00000|Lnb4b0s&HCis4Th2At%vNXfKjHS{#MiXq(OqKo6Wwf?= z3B#Jn%E$;QBBaXfUq9ag-2M7`dC4Hv%cv@;Al-oj;NUFZ0S@5*$G?2@`LE%p^7)%z z%csu|A3ywG-vw45yYKG#y}Va<`;TwlES}?`SUeHiy8C5r=>KMY z57cq|FT@bj_%PkA3gGSVXPmu?^lDaXG2C#bn(me_=;`87FGamdfB)&-`;UM5mQ(-3 z5AWXo{7ZQME&DlqPY-UEMdZCeksr%v(70Q?!BFw$KYuFWOZoIITh-I|YW{XvRo&}} z=&GK%clUl-+HM~iJoKxY9Gz$9;jG`{e`4Mv3^)AcOMA$cL-oLrw}je=bH3R>q}!|Cw_9u>pX) zt4dwr7yfu%RlE_6ORKTaR`XSML;Aj0U~h> zh{P5Ui7g-!JAg=B1VrMQfJi(85Q*mi0PzGsv~)~I8nP@VFkk!#+0yF^*jA`}A&({# zuOT98e>(9}-wS&$+^UM%eX83FwH1hC| z%?3YK;1M|b$7Xpi5!o@iPb>at54NWEdi_2G_!neOJX7ZQLgsd5XHUM*^7iy9kBGpm z&Ln3~D}E%*W0gN0d-`RO$Kr%P9sBrMk?S1%r3zQ{;}O?>eZX?1zvIvFcgqEUtL-*> zj@=f|u-p7lhxR1);CX7@t*1BILM`cFq@cU|W381qj@#&=QXD*Jo6 z#x-5Js1=u`PAsJEai{v1Yi;9WwH}|XS+z?R@^X!xW@f-~O>d5**Xn)^LfLIc`2D3dl;z7UPY%{?=5ID5 z_kBJNn%unJ6i57mrvpSyG5x^UmO)U@AC=F_CvmBZ`M5#lgpmcc078U8T`lF8?47Jf!~Q4)LBC$t{ahL#cQE`~4D&Zt%90HQTF{!=|ge+kJYo zF8$qi_lg#p?)D!qw@)RlX)T`UZQcDc%k5Kio7l=XY~_0syebmv!-w#G6bP|;nSS~7 zsZjOd^+G`8TtMWJfXGom-HkN?pn zY$d}zV93O#^UpC@t1Yopv!Kl%6@q4?{=TwtV>f84-6lz*W4YxS*pKp z&-vn6TL;?ExKMB~1hWC{<{9x#_7LycL(95)7@uAa&kT>v-R{$yb!l|KwqD;IJipmm zw8ay*Q~RJ$XTU-uKK}G@Q6m--xKnr`fpf}lKm79d@(C7XC{I~rm-S7K6y-=!uJlcf zB-BFR^jzQck-q6sA@os!o0STgv4%NoqT3sqeX|&d9S35^f!M{Q^D%{PHEpx!D>30+ zP={sAb*0&>rLgcp_LmREE|m)<2fdjAB^3Mk`AhovAwPV1`1pYg@)-Kwi?=_o-hTX$ z%J7{IJ7QCGO={oCn`rt+jFf*R&%_x@=vv>3GzD;kR zIvVnP?)YT&`DFIF7zLyL@}Xh=jKfrK7qRzP~cr%7B9Qz-LxDZ64aoIpeHe*B2dK&QT_q+L!#?0XDtS+hp8MhThvv^9Ygngm%3p%0i zrA3K16#v)}dA5FyagTl5f};`cg5vnbw2+A4{V)(WGt-9LrHv3r zt0KE$6qDVW?2VY%jFV-f7Q;;g!rNhg_n---(<5zFo~6dDfRm$;7IM@Ll*%p@u&!tm3&R z^pfo6%52^YZM_t+86h&4GeYJ9A+xf#H+|$U)TucGiQ7c_VQ-1J&HuE*`!N0edCYS0tBqartt|tFKXl7FoSn%g}n9_n!x5UE>q>nX`5eugRP>)DNdZyZaAc{`t*c|M}C$FMlncA3i@pcBx}~bNn(h z0P2rT!QEP%saF$+MnrYCEVN8;U|J}*Vb)oHp|hS^^^49nbaq~YSod_oXuUBd?v*?@ zrsQ#Bc=yLeft!29cLqEouI|;$NT>@&LXnYB3nQUs-c6Z%WoMM^1xl7E*=0B1th}Xi z_iDytb%DoW*XR5zhE_^LGO)GA0F4xy^`t230?yNlE zvT9j^Ev&jQ_Ri%gxRP?>|FJ0``!P0gtroY!e%Z|Q+?`9z*{a6%M8D5gHTiA-X+`T=&%6H-Yj7A8Bp`L3oH*(XDt6_9tDW8sfnyutSrny`oupfrk13q=ki=) z#=rJvZ{?wbwYkmTjZ)o(DD?`_q?P6a(KK!D?3+WCX*2qEAzEFOC!yMi=Co=&HQ|qC zXIv!y<5+mIkwY`nb9OE<7fti^ww1d21kr3(#2+nPwQSj@4YSqp)rb{)yWmKlfr%F# zO-&3{d}#ID0zV#c8gh02crGoM&75C|S((LR7QMS$`0gcB#Z&>mA2HQFiK$Otm|Bhc zs^zJPsgEyGt;xT_Qq_W~Ph7A{J4^ZJmB5vm*xiTxeLeQN_1Fu1Uaxy!zsn|6Vvz_sl3O4`i=6K(~C5T>lx!ew-lQs*|Z1r~A@a#`M`-`uNuHLQE zPt@@M)FbI9i%g+oGWxMBmYzs9e?MkUylI*AVqNvWiEVO{aG5B zycbh;P58H8etKWT{XuT!M10uy+)Kh5HbBo>&L7Xy`=sOd>ueimi?b@G&`vi@Ss8>&!CIl9FUU?7FTrdv&v$8n%3>cBxz_IY{#`LzFec z&eOzi4l)M6Z6f@AyWFGC@%VmB)EYB$#eK`3k!Pan?O1k9k)ed8@9*_u+Rc=vqsM92 zW0H;?d*z6;z_jhw5=c%Oxss*9(h3n@5XH|L=$Hjlx>*kxy z5GP7MY?wQCb|xnEY(BQVpIW(ElP)R7N*`DA)K3Dmq`^1stm=8f4qib~)5pKV5PzXu zUA&)b-nr6nVbRq^`#GP5;p3y><7>mmmxgcXYtMc8Q2z0SrswmQ^3&&WG_!6D-eKL5 zUb$By5_|sV%e#LKKTY|@2Y%z*aUFWh2<9!-^z8Z;35@0_o%oy_d{p3^f%-@n_pA1r#&x9LF zjUm*Y3_~%t0UAnRt%TZzn@?oNE5a*zoQ>-AFKVlRQxU#mui27V` zeA=YTub*^D+HcmAF4stJ+~6Vzcr@v1ciJ{dNe7d@UwgAB_{dJwOIQJd&abWiXW)EM z^Dl)KkLvs?viJ?OJ??6Ih>z)c+|~0(x5IWOd%2u69@*#1t1@QK*9*e!%-{JA^ut%H z1>s?tXnBl??NYf=a(&>aEtlMV`1RepX+}4X(jsa5{CajuVDqpoUOb?cPqTLemE7zG zwC%$CNZG)fHF(A_l#u{?uTujVW9(m ze<=U)D7ykWN@W)-E8LGOEBvCh`TBO>TokEIQ*Fvt2f7-ai?SJZXkV7ib|zyhv5yF6 zd}P#NOyOOx`LMk;pJwa?JIm*^=EELe^Vtq~fAwdFS34rQ$G~T;4e^DnvpaaWracJVwpZ#wy!0^WMI z$xdoxTy7;b@f&lKzFwB)qp~a?k>$O8ny)hGJ+*T#Mg8L?S4k1~H1BN2*iLOJ#q6RK zzd-xfOL1##xfHpUVz!oI?w%>d+`Y0CQ_t=NUr8~Iak*gEa&Eg6^RJiUzKVWHin+fm z#eB0pKbK;@-M+p&!CTf{u|N4rwwso3|EIFrhZ)Rwl=0g$gde{(S&ccwYRn;4^GspC zpDEnFL3;0wGKI%8C+9<0tQ{#?+`qc`o2~C-m2~0u{DJBT@Ou}u4(ahd=N%LDxqSLH z3@4M?cHz&9r|#^XJ5{S^=qK0kc;%lq=>Ox_*yZ@w*y5Z-9aGqc&ZG) zT=R{UgD89}Mx3k*Al9+wHA1*?M zs_7%$pWT&wR$kjSMbCe`)!(*lXP+Mk*1xHCe!%;^)H{6={R_XcXT7h~zuiQ-tN!QP zOuwg$i9!9_*^qZjBi~M1cgf-5^M{Y=f-N7@S#}zHGL?(Iu6<~&PpI%mM5YFt;rM=D zckNzU_T@}7*KVGuomF(Wdt+hVR)-8_lknj-mDQ&q^xi|+?;KlEanqg2s~3LOopx=+ z)|QQ5ESnC}C^hQ3l3Sy$R(H9p;qWGJ*Cw2QU7jyh=I8OO;BW~z{Wh}>yghXH%8llM zqb)l+3}tVo-%fv~?ZC;1XnC(;K4yQvIkIoc-)l2|_r<>%4k}IU>G`3g;hQp$k-z_K z#RZKw z?)iZWocSWn^m(yQtzdR1a;GQ6*3AcpE=s}0aXr$xl`teR9mhMLCcHrYby$42&|gLR z+l~j%j*n}xI$}B3*KRS^ZmebbwY0sT*S#LT*L8LV>@3-cI>t_pF87j0ITJZ2N6qR_ zO$`}&dvVZXG!`zV4XSmN{xjk6=I9qmi!G`bU#JakDG&QnQyj(2)7_%?O^y^7o-nDw}@iKX5K9p_N(fsYh?udr& zA0!}M;O3tnrFPJfy@jx)PHe|@*wBu_?sL7%yKCj=0t+u}KrKox(p_fqb4_wa>%+X( zb!j25+y24aJglA!EPi5tm&;)DrmtHM+v)N0RQ0N@-9A5d+WOV|duc82l3Z?fV>UxO z+LrlBHCyjVUZLervoaTL%$wtpY)_jn*tI$%G<$dT4$m_T`sJna>wNl~r+TF)DWP7h zMYq#iSIRPN4YS2*uQlZZmAiQU>!o}5d<8p{n3aO9kC*-Lt6=7mf~~GB*ikU^LJBq* z?aO*artuMVx@0}CNQL=bjeb|7-___5HQIGvmm;u7cW&w4*o8RL68-h!tlKRr^UYf| zUC*-Bv5Qx`yii}BqFTMlBN16?l-VTYsIOO~W)OZ`{b~KCW4L_7iscP4nB>HhBIktdrU&9b9l{K?^Uxn-`2e_pVJT@)0X`*^fl9Kr)2jAjv$;8yj?ZOAR_Sh~F0t4x2#-The#}{|B1Mu+qT_ZA;ru**uDgN)^Lig*2PlxS=Pl+e? z^M*325aj@Oeew1F^Set!T=!K?v)1Vg@rU*G-foBu{K`lsPVVzbL>R}}ZIQy+HYhfJcQOU*S6-q0Q9i^L$idD4>P zR`*l0@j{x_R_^Ss^SguR>lvSjcr|N_G)#5&2V-0@}bd2Sd28VRJx|`{ONHBp{o?N8!%gyloAOXWhz;R>WF%J^w=;6I7^V{vw~!^bT9k&gLJ*iU>s^YN3|9Iu!k ztk`__7GeUY^war|IUb*8m5QAINQ++2y3H5;UfoPQ=H~Nd$ERyoeiDyebF$O*&^j;; zWVi33^<^5#K^e+_L9zKTH+O)AsU#Ym^KAPar1gpSUSoEIzBhKw;q=8Rl%bEC(u*>^ zck4>~1E;oMWW@4d#PWO`^wG1Lmkv^07$Zu*JsO>SY;+?74u-WnC^DWh8I}E!!+4jD zjqME<#SRC;A0G(2RwA2a8h+zXlEImB?hWL8mmYmAaDO1`tcynjk!O{jedubnhqAn+ za=FEEHXQn9clBa<5uZF4*za~6Z)rW|KixvU<$t@4chPOLxOI1VlkVaU-C6$@UxhzE zK3`dB-=4mViOOuuQ{EnZ5PL@-_y|1k%PO(i+{;;7vw8Ew!3PKW0NMTQe8=|$9OmaY z#=}o`k$P#-!rk(lPXp$>TYk_5^Y~cne%?AknZ4#Wxs?-@@Bv}NL~H!8jNjz=u8NL1 zq1$J(L5v?a*-+}`*TtsVeOlyzvVewu9C6>pdDe5zjo&unO+8?9DUm8e#T3C z#grSeUwUs0`rHPeX1#xHOkFjxX7Nd?v)P|!SWjO$8)n$dW_WSd@ylo@#AqkPX4cJo z==XA*bve$u+-SXCYW)F&M%T&tMON~`70f@>rzd;8Z}<6D@7DssX9};T-}qMH^+G1h zIE%yA;TC4#v4P6R2db8HdmiZKkmN*tfkVdSly=N|s{=czL+>IHGZ#`jXULpZWL5M$8mcHAB%7qfBZW?TC|oSU2Q{_{Z_Tf}#kj;Y~R z|7GKx9e?+j?9IBk`QY-oGwLa$U3-|X35q6HB1jCsjAFw^vDuc8|weGWcG+BS)7b@7Fg5j8;vJR!wcZ zm^f<|yqF#@_R!*R6qsad(#7qNKw{X!AW8acPgZnR?V zZeNA`&A!r#1Jtl<#CE@W{^RboL|;bhB1h{Ymj=s>7R`(n&0KGO&hYA?wxDGCF!Y;@}cCI9fKe*6=}F@9i=SV+95K3O|^G! z%Q&_>L*!s?cE|NS8P*Oz_gFm5$BvLqmpss132}KQh9rb`ecJhohH)kYe`F>$@a_o) z`Z{AiuwnqjyBFXz^VD|`IO)H?I zEj>pC>}=H7u~DPci;(jt%7}ZQ`=fd$-;f%2ckyk{Pno}O$*4WmZs&2!NE>!4dotuE zH*Iwj+Fmd@DPS@K_x7$q@F7~Y555I)>@BjJ#eEK+MPwm0SG2x2tAiDeT z<>OsTft!-8cK6U0=G>3zSbj{$@~1`kw+sf4J~uyK^FAzcvt+@g@ldkafBq|!;{X2m zk6}D}5z+7qfyH}$2HxY}H#0y#{IY-X-eS99(aF6%s&Ss=wv&7O{&K!8Xjxj1YovNy z(;1$yZP77jPhDWmqLX_e!D5eW_+^S$+cwad^t*TLTQ+2hcHWJhYu5!1jK0v{J^J_K zT~A#D*Ue2N<; zibLI}J@=bxu}Ze@HTldf9r#RjVD|ak>>r^JIa(<_S}8r4{mG2!(TwTQjOob*+pSqN zqZ=`!8!=<<_PVUw@eHlk>q}+%7#;F4Ivg#tSz2a3x6F&3;)SKxqovoQrPmV=kB78~ zJ+Cz6l!^Wn5p%F;TM={D+FEyDYu!H4F^*Y{__rO|73Q%`t3Qt=j|&)w=5eRSVerL{ zdbS&m9hP1sbgboi#f!15zqY6tbz(=2rc(*><_c`Qb0}t_uqA!dZe<$+9zOme=or&I z?)Z!v)o{r>%;ji$^hhZI@&eRMg)bOt!Qb^zZ^5OHte{bg!XT|T$!^3%{U{S1@ z;O_%M)-UMsa9MTV4_lT~>vC!+*Di0&51;@2<3qn-_g;?&slE?%?{fLM?P0hnhFlW1 z1LQbAacvgcF3H^n!j0jr^5Hs2kvjhuv^!|4A{&wlg-ROGV=z85w?%ra5&yN7aj{wB4 z0=F~BIinmputPF1SDChs)=bw~34T5=Ro+Zn&g$-AS!%IEAKrib__tqvnyXu1TbqBJ z0F}SrG(L#h5P#415ahJjCC+R8v$e39F8JOBcl>_(fWq|s1X>#> z6nnS&dkUndJScl}s&|!~&wQCKeEey)_PXf)rxMa%Lwrwv4Li>tf4Zx0W=zK4qyvpc zf3#WcJD-dF@XP!6=f|Vfeb}zG9YMlrt!nCxa2dQiMT%i!_e&TzFTnG zLkK^8`83$`Dbt~?pdS}I@BI8YU3I*5-h5p15aX6NYo{G|mqj;hWEa?|MmDMgHZC&O zMoew1#o{9bS zz{Q&6f(aK^Ar-ZuM!u=qyJt_2(TVbM1MVn}y1_HItM(Lzgg@(=TVQrC3kWN);xH2j7Bufgy3Q!Y8 zGDiGhx7^=yw^KWMmaVbYh-AH#K1G?Gi{9{LOX8er^TXQASyo)~BAAMKag}TQUbs@M zFq3Ikg>1Fetq|+lMeCHbr;E3pWuf-lM^(jLhVYe(pXm(T~Nb#^s5ZwimOSc}es zjZ|A4)-Jy5w1j|Jrn!?Qnj~D3N(t{tTBJOz4OV$ql60&TrmQl>$iSFk+JW=3)mDeK z0ctSD#Ef;Y5gao>YVUk7!bxA7Y0-zZ4ce`S8B?{f=yNTg!)i$hJ>k7=bKJI8CC988 zNB>3gB@~M>u zE*7#O(w~%a(bbw%wJO8@yW)zFUL_{AHcoU}c!vp6Fld-lkxYybEytzK){5#?r^Sk? zIl<~g=&=sbK`_CdMD~u=Hk*o_B#cmiW#P7l?06{7F(Xxk)yP6NX;u6L4}#gvkO!NT zkdiy^BFm_04Mfv*S{S0wP;Ut-kIvg-qlfZWUR(Nn6k0 zfJNa6U5iN>!-ZiAW{8jhyVd?yyIXBCBuTB^PqL_mMl^W)T zl#2r{N$1HR3JIrB93v=}q_<|0WoO`Ip~YD#qqB4o9-?xZ_*^UTfS{)030!X|rdU9(Fvzk^DM3C&;<{*SIrl*T*uc?azKa{i_>y)6 zl5I+q6*v(t5xs+MWtSm9CW}(#WgLdCImu+KKs7p4m#xA?h7bs58mTYiFr}e0RcY{| zR?7jRbt)?5WFxR|L)S(S?tr@mI?`Zj**QFhYTQ;A$wnBRvYOMRm%+ z)Y4X1%>)sF%{0Ll4oD@7fgz{lu8W(_A{OBDLZS?5VIS6&;R*aYF(? zLd|rlrRm_AD zruc*j5W<(@9l{%jm_q?2nNG_@4g=?+fr0V@n1Vz$TTP<^!`aL8OB!D?e2WVTh=3uO zg6mciNRlA4PQw^6I+9l(19_LioQBOoADzm+n%Zg6rwfG#5>QGb(kajt>x`;!Z6vgVaJ10~ZE6a|tD*;fMX6jR(+Lj~0*7U>9Pew1*1}a%DSvC+t+D&I z)R;qC3a0@JT5?L{-m-x#C(pRIvS<#w-8J%gw867VkSSKcX!s&VIF`fKO1Rm~a_0d| zYASf>cu6(u90)8K&m|&N*v)|l2}Ujo8LWn9Mr?o(k|By>h$#x90`e!8odEtkK!leW za>;#$1bO8VC02!>(4s^RO=Mgu07C#x*MMKO@QaAW3+8E@XD=b(=qVyqOc25^7&s>t ze0RxcA`CKPJ%pw}USL}k+(e0F&oe|`z}XJ-EJKFC=mJY@v!>u01Ev}_duq4SdPzG{ zVniSUu4QdIs->355fa4c%IPf+9p-B}J7CF>Z`BZ59p>_65kBbkf4tN6e%LQ=p5k0-G2G zeJQzykP%IlP79q1imW*qX~+-s4hB5{k-?1oZj_E;P z0M;U{86cQ&5|dsEp19b&3~1pwz@ufRu>ktWK%)pa9OJgr3W!NDxiCerP4Isl!p3U$z<}@( z+6?`21S2cvM8VJUqzM;7qhX0t0e3pBEP#v<{J}iYq7@h?3IaLUcucn_<>mRsa|CWz zI>7T+X~@IDXeL^fV1sOfRs?!;09Qs>h%lmYz#AY(COD>7Hk=Py5poA3PBNn?*e(K? z-Te#LIx7O|0QfqH5{;M~b*8o@oKL=PKj$zOe61;n4z||0T-Zk=hv_TK}$-t3v zm?Xp`%##s{uuML($T|-Ym_`lF!mPk}rVJ-a(T{QrsMNOjmw4a+3n8i*PDFyA6$}>y zF@jA6vPnD;Cq&E^QveAs-YS?x?@4eVFW$o8H|qooYz)~DrBsEN1B{NqFjnM*(9fXu zps&d?2DpNDA-oLjTW}pgA$$Q7#rA%gD4@_7Q3Xv=6=V@mwLNbN+nxFM9@G62!L;WuIn zAaUaeGDd2{sT0h2f<8lvXuaA2&Oj}>aTb14)*1&|6iUG56(AhJF+J5Gg4Yc83884R zotA{R0AO_)GQ$E~upJ-$Kv)6u5*>^jVk?&64&V=%S5{E$A81CMIgum? zfTSdumk50jt8@4@i#P-V(xO1nLWcxG9*TY-TN3gM@JH(b2#1qskp*ah$-rqaJPe@} zT6DCc33HKQkRX$`(?UcSIk*9DiH6at_ln`lM&cvu01Dh1dQc-UFE5}2_JRLlo{35ReE z5U>uLB|We(N9YG1$Be?LRa+lXs?$ofAh-!x3Wa!EWg9G%9B2e~ zBSUmME#o)>YlV2A0*xTX6R>6$I6p`X(KkEo23rcu>+HTQ1?Jt_Qo{O}SRD~KdxYX1 zd{aKbcUo9$t-3}&k2b(1Kpw4U(!@#%{7rHNK^CN`hy!8u^*S`mm~7GThUP%;K14K33nQtPxZ!LATC z^N6_;lmY=PED>T;Ba#mTEn2q%4mG7BypaKRB3O!609uLN1Fb|WTL@*UMU%@gBmnnd-l}Ds#NMy;9X;?+p=l5i@sEDz_Q3PQy(A-oY zI;$f|JRr_Mt0rhh29S**!-z+2BWGX-ZTMyGU!Gr38i*KzC&Y{36J%9-fIZ+#j3~9$ z5zvxQZHNUt5E|jI>jqJ%P{3iZxkc7ai%Vc@1g#wIK@~*%0lzb-6QUFYVBKk%K%t+` zfSCf*gqQ|_B1b3yKF82j*FlTSlNSgtXvqp514fl2%HWs;fYoMwK>F7ETkmeYz4hkS z>szmGy}b3})*tWi(WXm*;lxzJD8LIiU_D-R#?+z#)%EcigcXbwVi4%1fDR!luh0XC z9NA>}aXYAlB0pYf85q73wh$b577!ByL-;kQ1at*Kvx6jf=qTsWi$I%*j$kZenSoY> zfrc771F>O1+#GZ;x3K?QmIhgAiV;@xjL3$gL5s)>{y+dGC?gRg^U!HkiTDNm!Q8-Y zJwpxKhfLh@M8Gs2>Ia28Q&BZNa2{wBG9iWj^1E2#sEWvehWYPBx z=i_+?`a%e)$fYq>qpyGgj5h5vOcMSAeG0Zx0N^gIkrRLe zKxK9aEP*W@oCYK85uQxXSa+>on;MS~#Gb}iy|coPeok+X~qXo47p`49v+NpKZH zR1m1B%z&^Evz0IsbLgmu8M6-XSCsJ8hLi(DFk`|R9sn^zQ6~qyF9NnGAovB2j2cjs zk$bHJu^b>}0Z^hS3=BarIt2O0P!(FKx)ZD1W9~3P23-_FXYZ2n@aWE<`Q%1o6(AZY zIM60YApoh-b~2m;ufTY8VlW|;!lGf7WN--k07rm?;RX=DSseyq0HS1HU8c`w!QC6c z9t91cr9ug`(TO2S36L&YjHM)xAPgo*P|k-^un>BjP3>T_U^Eos8cY!|y7n$xP2WX{ z(Y^-H0%x?gt#wWwa#c(rNprOD2z?uQW-UTUi6NCxiM5E=E$7KNLBOT0wt$#65Fbn~ zyawF8PK8!a&{xpXh%`oG3S0)LR$TLHAb|mD79pP!oMzDv!$en$RM3B>xulSnX_`s| zl87vOc)^)?mQ7WRR$Y|>$dhEM9elf{l|=--R>ZEE&mhdXHY~7|$X?UJC<9SQVWCCF z#MCf;ji4hV$l#J808>Csg$Lju#w@(1@0J0Q1^tI?#A*?jz>6XFh15nytH+{_#3C#v zR1kmyffj*w0apsy#(y9lWe~uMKEYc;>roRf973;HW-UX@^tFQ~Gqmpq1MZ?x4oD6` zpp?#WM+?2K2|b9x5x5!?tS4M4d2OeHgh7YoB1SK4G$#xJq*Sz#r%mAi8*q`CASXy7 z{(J>QQvjnK*j`Aq39#4DG)D0OF$E~E0L@v4NC)WrkwlxI zXbBmhh!&O**urH(wt>qSz&-T34Md)36`nS|7zIg)_$`o&BY{BZ%YC1GdCJCC3Ne|i z2z{i2UcvPNk!6sB#UF@e+EhszFA;tLLvjnirND$1Fsjmt!3lG4LNEchN*Q+uJP_Z( zP`X6GVjxEA!+`fNS|O1iP}&B#J|c_YpzW@J7`L7)5+#kG7}G_99Yt19c-m&k1F;J5 z1FHu|jA+P65hG?RAzTBVNQ04;Czw?exP}jgVI=$nR}Kut3ZiXT7&8!qYYx#+(wZp< zcB+Tc0xoOPT$ma)3^PL-EP_R-5Jp-7akbV8Hi|^c_<@)efa4B201X6KhMk5nj1E@qGU#!p)j{({!yFuF$QA9P(@1|l;8rFrwr|kmk33QS*CHAwD%YZ6$9$QRaSsK z4A8c%PE+GRETEJk_h@Mm9Z|GV8ZOV0??lu-5YvcyfRij`4gh>)*udf>6AoBR!{at$ z>N$oLZY(P};HVJmS5IRP8h*?sXt!ybiqOnw5Qd-ju)jb;2z#v5C4z?v7KQRV5h)Dg z2ZXm7mYDnCxu+Cd?qQKNg}PqXVf=-BVzrn%6%lC&m~F%;Q56AKZ`$@a5o4$o44fk( zb+khZCbZW<8Gb-6qXkehBA7rUWFU(tzYDMp;9-(3NsX!zXlDih4KY+kToY(J)B`0D4Dh&ekAc3xc-WIU+n!LWX6Qh`w^x?iI|5 z!`LZ_M>|KWOj;n2K%khJgSqP)Z5PrLD=kz5OM8sQdxRk+!sSFu`K$ncEjjK&dSWDt z1KpBv)rKq)VrE@nL=c16Aso~vde118j*__&f&xhyXMpph1+u4CYefH!_76jVk4BV} zD*RL>Zyu(Syi+a!E%OXdc?>Wj>-cu#H|ue z-6TK^2&{n(ivs?{Qert`nNCb8-K<#l73eM-N84tIC#>YOwL21ntkDWAqytqof(bz> zs4D0RD{UIA1hJf0K-g#j&NHGzSTowv0YE7Z2so&L7;;Fl2yYT)U}X!isrcVuQTlJ-!*7fEt~z}Tu_Rff*<>IPy6-oS88q8Sp0 zp)e*0l`8Opb*8yovH%E-V2%OMAT)^cN&$GYHk&N0^+68Afb=n&aEY`Hh-g6?N$D|# zc<#Gsk<56?ZG{1dA;LnySRm}D1Xxy>*LIv{&fy9vZ~^h2j4YbU~Gjpw-*f$O%vlTB{t~YJl5? zpN(GHA|ni3>Dj$ROeI>X2a?A;QUMNp|&^^1S~pC3Rout!W2#? zcLwXzq}R3#L7D`WC160Hj89G>c<4?Ms00=Z@tFZ~AC2IOWLYw0xFX=e#AR4iv?9lz zY3&o3<_LYFe}D)G5~0b0AtLBH4(#MCM_dN;gxDG26X7(bQy_NE87@o=#H64-0dmZo z^Z{lRCWt8sOb{FoJ=^}2V6_n9O6ZgV4xl}-=z%_>i6ZF1l+pHts0h|WHnj55a3RbT z%)PB1VmS=c6k0DaPC|}+0Qw1#3q}$u2~Wg<7>pJoK}!P+62T4!#-z1nNSgvK4X?m6 z(heYsP+71XaXH{zRtj*Ja{>;&>4 z3yh9EL5L*@zV;)}5=7NQff26=f+EhTS_x0p2%9YjIfF?>AWuFdDOS;F;qV*4biq~_ z@eT{!v!F0y&Va^XrQtj?nSez3_Z*@Q%QR@_GYDtQ8Nv@CD`6r9I}AhWBCQ<2{|+7t zG6T`lr9x8RDiT9913jYTYKU9NEyWz;hd2R?2}Cxqg*FySiJ|je+9K! z031{nF=9pF0_mmQcEo9&7>DFRr5!DYz?f7R5|!YxC_7uFVZ91%I-3dOcmcG>WTL%G zIAMftA`{piWF{kq0O&_tq@4}4$_?X=P!1)57VAh1AVL&cPlOu+(l)eiuW3o9Ab4my zJ1=fdK#aGuECpS3lu&~}kTQx8{qT15kJE%<#xNl#PJ+dtH(*wxker!938_9XG}g}d zahhnFX)aFQFxqL!l#LZRz%DJj02fA$fYP==MNWkgiUX!3fH({H!C{%9f^-&06^t&G zMPZ-@OB+?*g0Gp`Vn}Oj%d1wRZ4hxff-@FpK!4zEHo#%r19;FzGyo=?jONWyo2hW* z@QAeZ0-+OvQbvF);fw$RT?E!#6o&9dS`-BkqqHIKBh(^e!it2;?(2Fpj^LRE4nP^$ zRC!DNq<H;hpZhnOAUxpqYjFHWZ@+szA(rq|*et zrxq|62Byv` zU=nR2+kwy=@k@e5%L?cfU818TZQ!&jNgMXG`GRcR1R!)U>Ldhc0e1rFH5nP*mp6DEtQm?=sOqZy;LE}>2cM|??&a&o}NLh1^) zYv zR}Y`fIW79;AcBHy_a#FmHr2R;zXc<$qcgvS0hQAVe>>Y(Tnih_rV>1lp|a1KLgk(@g{btL zDMYoWPa!JV2(!@6m2%isMEC{%2I!(%z-!sOGCKjEXgc~(6($fYro+axQQ{;pn&@Z& zm`JpAn1TQ{#auBTPD(oZCz**Y)KVwRGjvL5W+}ZDXvreVq8vF-IdM&5%n5)adD;>& z3~nq`$QJ^7_GG+$T;nV$VS6WM+9sJQU=k|eQ$45NfiVlR87OW zR0SoW z6F;b8Ve~EdWyB&WP zX+R4Y8?68=DA7DsndtOKLG;F~vAx&V@sc)7gaStq0xCcQ5dpF(la&%XY>P*(6O)iA zS>H>*XVf%-RwrP<1#l^MLA9Jma-&y}%7`w2KC1)FXS7V?eX6Mf#TIUB-$-(F*b&7Y zxaQD92eM9GMV=BW0c;Z;<}?WKD+Z4_my8ZFg?6e)i06|}bnS(KEJ8#*yn`|kkdDy~ z8;o2=?B;26miGoc8ydKdxIv8Uw1w4A5E=tFgiyl+OIxPk*jhd%ffSGyV(7c4AKD+F z9R_)IQ?wy&h-ygaJ1v|5idE~ig~2N1252144L{FsNLE1UOgDXKg3Yi?bnKc510+Xz zBW+BkkBLzx5~X|+>%MM$fsSJUo+>2}Rnu+?ZAel+3LVvOEm@QB-3vFHxlRQxNkyQG zOlJnjXPAg6O;#B6)~tH*X6d+`(uEerXvNUb-eNXP26*j?po*Gh{KcC^P%V`)5c~*? zE-2QIkuf^|lcH;uN-&Kdg&&C@@$y}OuLf8rte~vqFz^ZDhR6!GMD{dIghsF0h0IjU zJ~@rh6xKQb?B?PMZQubhHG?LYebp||)+_)=@`VnlYVSlc(Bnv7Gu*v;XC%{fU`o;%QNR}FG9^HxXA)6TWeS}^<3jue$jv@p6(PpR%l-j`yM}h1RxwV97Nvo5N(Kbcqw1aK| zmUVS-y?~5C3fofSrGx>Gbae+%bb;E0nzf{zb6LsdT{x-D3jV zFM;O?LAJx!k~Xs`_@+aYltb>|bOquNKtXt@nETyc(wrRKhX5A={6mKYG4U~$5DF#l z0m<8OJpgf}pd}U{)}*Vk2supx)s#F!Q_7H)wCUWax)U6L2)dwYN_uYR9WV-t{wW)| z=M<9ZQ$*FDg4Z%|a3u>7yb272tu#S(i{?i>q!n@Shjh)@|=B4*B|a4V{u zNy_x0jFM0_=wXa1AzGxH!+MxZRB1!7h$2FjK!Bc7<8#E{nHS1!Sj7yZL;=_>x&olZk9!p{4wD#12m!GbF!M^1P|}eBT1W3!$=Thi2&a;T zWK>K01hUWxOo*b1-lE4+wD4%JqGu9AH%TKL;B=W7vjAR*(-I=ie(Ynu9J)sWkg)iK z$!?i#fd|i%HFT!SHASIr8-9^QfP>{eQ^LGalv2oiF1~sQKBcZT)zS7$LSrx*WHiWV zI`|4Qn#w?O6zrXHnCDFEv{6*LERhaB8c{cIaqizko_;4oceV-a^kvmv|2 zP{tlzmsfj6yC5U<1d_P`)F#?Wf)qO|WrUCOmeH+f5bQ?MuqTl;G71Ab5@=BhqXu}3 zDp6)DY#HxI6k$FE%%?D7cRECJ?es;|bOV|qLqt3AB_J*gvY!t#W=q28i3DZnDVT5t zsAM$sHRy=QAsWi=sG<)H9j29nVVz4D+8(F0eE1S-p04=OE|_ZQCPvI z=J!@H4oHa#Q%5&ErED-MhOR6OwFY23I%27|s~87_$gk3&APqa8A`E2IDN{6GH06!< zV?pe?KCxn06tq6vmg+dubV`m+(?N|{9ab>}T(7_|1+7@YJtK(64`$60If$mkGg=pd zn-&&=U{T&)#}>K|L^C?n0JNZ#@eIxZ8cW-qly*a-dF3uJ$eN>b%8*b5_8G2^PSj-v z|CnuCfffW(Ua<>>5|C*pG*h-a;$C2ogc;4*qboh)cKUU@V4Xv(L4L|7QsDwohv${h z9=iLnb-})B7h*2ZTjeW25&$k8XM@tg@Iea;Ye(z^kl|}~L1#K=t~6i;w35y&DnS{h z+`{ySj`uvDjPYjKH_^FGWiwy}g(|GV0|WKJ#s|7$wfp~r$^e26KqE*)!5^0xatVN_ zo{sbCWG`11#3)ECIxc_%HJ}o0ju=y%wXvU56^GT~D-)gFqiaWC^cbKX-AWLvp)~;0 zcj1pJd)N^KM8Ly3qtBZ0$h@QDOg6%Kv~)FbT-}OF$M%_zw8IqWc!~-@Fa*!ja6XD@ z{3!fL{0RKeGj^VO1P_SG@PnyG;2;n<2(Ql5?~gf$nF3Tt0E3Z7fGm+HSGY2uV4#P7 zbVIye^9~pnOs|fPCr3J*KzoMp?TYQN4`$X9C~p>jklho~8WbfkMWbAp-3bUQ}j?UqF; z#H%$AGhqM(L<%Y?%BPAE@sutIV*mu(RhqBaytkkrwRP1iPPZvZT7aWVJ4~py-FAZ@ z>eZT$bU+>&FA?#0x>1H=Z#o1F$&0*SE6nWcDIP5h#17xdv_t%&qI*CM#ZL|VAXs?4 zxi?C3%yqOHj)&8l77R6Tw@ZTC*v}r)4?~mw)w*F3ulph?SfXs@z>AL=p=wOJAn5L= z7SSw!Ju!@lQVR?Wfut*%>8`CJ>HKYl_wO0j;1qsd&k9-?z5 zlQ1ySx!;&gON+1E4WG9ua+mvZSFKl2$igxhu&c+Oh_2F=cNw z9fPKY*D4d`NV_<7#s4PVVT30G-QHF`Pjn|op;Lzr##ALAI%oLnbA{VPPQoC%j+~Na zymOi-3g4aAX6VLm!4W6uE~^5+p(@?W>LZ=Y33LxPqDfw+uKYF=98Nl(W=srh~t2OtaYL?=`{n( z5cn`*6Cz?>;GBpw#)qgFKOl>7ON?7;kkuedgV9t5WEILOlv60DP)?y7nvn|S6w1+h zWsZokjWKkk2|ONby`=1mmP+ONd04}y6{gL`REd;y?|87%21Hm%%K+yAU+!v88@g1z zT^M5N7_0F#DKKz!uoIKum2$4%&rc-KS#uod(YZ1mIqgM-zy;?;$dHPXz>WnIPh=c; zVZaLmUKsEK;ip9SiIDnH@(Eps5KtN&TtK3u^$0~6-4;ZrM;ecudp3E5`Y8t04n{NG zt{0)i2|B~4t7td4Kvthko-R3}`<8_&43T@v*29qsPq)Fv@7Jj ztTD0z`Jr@_tozvz{`}t47mB#o=r7MfL_xVHD#9+(0sYu*!}FO#K09gPemZ_q1br}x z?j1H{6KM6Z^f+>rfp4VqRhb-o45Bvy()RgU%spMs=IBFN zlCH?Yq@!q|n=7Mpw%H)-zp4qRxTd@Eg!FV)iLSS|jv{VB7lXI&ZXnLUPv41tHnRdy z7=jf6+Bw3P(v3wh-4;SXw;{G>#8)>{qY@TIlrC4*(81$|ik1gcbV*V|0ZC2LwY9meJG=eL7B2)TlzX36Gfav9~dg_CO5hf9MH%K zphYG7cj6fMo7%QjqI34Bn`pZmKHq}{ZI8vADsi1|`UD;@v?z(eYD-ttx=dMN%iZ7; zU1MByF4ee-Zt^TW0%pZiZQlfHZj7=whT_08j0vOYAT_iRk*=njvYcmRGI^f|d8Q6n zXy}}Vp${+6VMqpUbITMh7WMnL{H!zdy(V~20WoF5x^oauj08DqTLNK+8{hSg;EOYz(UbV0v3=^0$kMJBZ zBi`-41Hp*&=0w>~bh#}<>=#s_yQMj$%_{*_QvDb%;ui#Dt$2=fS7d6pTyhfBc6V*& zE;D6wU*VYwM?9iqEr{-FsE!V)wM(pYbs-kkKSIQ&;*vhN;{r2u2ceGil^(jKKGGdF zte=fBQ(;Q3FLc`}uy%AM+CcZKA#elXkXoW8J5^CAfXYQjrhx0M4(;3%twtN;heI12 z-i|)JMc<%;gJo4&I^V|)9n5I?aq6V$^ksp((dtEvF&Sb5q!U4k?I-fhsTf7qePlrw zI7NbBmPLg41;RmN`DS?@LorTwYFeH-9TN2cYQhq2yjq=L?z3->3+@>|20t1<3O^D* z;#BBr{E7e+5}FyN0FqZE>8z>%u>DlrUPagPA`w0Dl01F;jr;(dBpn6?Fl_@ySi9S% zPR1DvK+fnU1uZGvLbMaHx~SUIL-r~ry4e$qNw$6Jsn#kiFSN5&gibadR(vu~{i!%$ z8r{MM2`eaQs^}06ePXTl<(>^sIqR&UJJCt~j0jMQC@IB<;$#2`@4ENht*B+BBbjK2 zrBIRrS}2|_EhpLcFZGlVaQzwOKy5kGRS}RAXcPgnZYsSuU0CNHBPhTyf zgZLqn@WVLxT>CfV5R>8uW96vMQJqtD41o*$@Kb_ItBBVzbuI)@vOwN+KUUVsv-Yt~ zd67W1bYC;zgC{RmDLUYs8N|Pc$s=zzi~EZt=-NS453q3<0DXA~11OHJ)rYj%zFT;S z0DZ40QGCL9v{}>r8+2iGsu6|{27vk?FApPAsxB~Upi2=F<>G1j0uqIqhUb?327`Tz zuoFLEsQ@VfQUas|NC~=lo8F_GU>BQ;na;yQi3EKgN$MCf7j&~9ea?rq95*HTi!@~w zoy3o_P##bKq>SFmcAqibN~PN8-6VUFrgFQK4Ui=!Oe1`uq3iq#-4kW#%YLmXRF$Yo zxr>xlWXQ?WCI66P_#66OPN0iNWINQY6k3$%nMBVdpd<$}W}3B+io$!rl1Ie60__2k z#a@MOK}W~v9(09{Q7#-^p#XD@Sp^(PbXo|Af!rGc1whkQ4K2`TiIh1hg#1vy1O#5; zoXPK!(}s^rbo)d5&LGT<()2GnsQk$Q-oUZKWpnx<1PibNghSDm5vJ)ckP3d#F)iEh zfxnbTtm|tEh7M#Hs}W5w3`Rl^8_?3Wj|HfYI;JVDCp)77PUv2f40r(5gRd+C*rt8L z&Cm}z1#k!q+=d_MhTB*(kQu^k`fybZEd>IRH^5jM5700C7=FYlc%dY%2;+gF&ys5J z7>-Z{y6&*8<-q=;C|UrBR)#+2gbo^w4kD1GPechtw@kyy(&xXFghoX=@zSb-4OaC| zB5qX(kCnw7F-}+C17|@F2mlD!_o~T@A#`jf>*;b|7U=+o5%et}2ywC@ak|^Z&=+ai z7T2l7cI6X5Mxomo=u}PR)keBmSq0ucPIqz{A!wjoIZIz@6f&bhIAcSHHkoM#_k_Qr zu88mG#!pX|DZ{!`GQSXX=c!yFSflCwbEPP5i&ip7PN8r_qZ3}{v_i1-y<4C^>na17 zGl=Zl@c_E7$kMl=R|uBwI|>-476M2MSTcdB&N}+2o;A#_ASuF%NS71QMQ|9Rkk!!_ z&B%KO4XtVXgv~T62fDnN>^*=_wSg2wlj&>U-KA684p3RzN>?K}OojkRqYsc!a%hqr z8_}h&65OFHs|br?@Ie8RGKi<|-(LY1r0cDV1VBeybbgV(nhO~ti%*}zUGbA?1j2ML zECgJ64HplCQ4@Uy&4zwS#GIcplYT-o6L-` zrhxt?I`XR>I<8mz%#l9vh)A+(@@-Wh%yRVk7tbYqnyT>=hKU0Lxmc-Px|1)_kuJDa z)$X8c{7kY2<`|huAWr&-2ISjfvJ6HTTWUA3CIU*q+m<2Sp+{FY(2f-XBY_7U2cH1& zDqUYicS&bjY*)Z7^npW|Cawfu^OJ7X@pL1vr_HcLLZRtuY>Mw}jw^oBDJdWx4O9?; zNMU2SGjxBVEWlEIgJ8x_x?7NmA|Y-R#Bm2WP8Wp)s}Y(fzT#)1fK`hMk(Nb8`ot+> zN<^55R{>0$x3z}8x62{|SeED}tRU%o4}r%bY=Im;t8hGNXk&7BfITX86EY8&;?7O zqG~DG$`5no>36D1-y9&bWdsRHO9x|^tab;luchDQ22+C{)m!tjZ85d`&%m=n-|))S z(`TWgW{MUWS?E5|n@u%d3=lcpZttsXpI{X9eI#I9`nqQSt}J5kbu|YA;So~OK>_;6 zpV8USRRD0IhIvO8LNofIDv&$xnhOQX1%iF;7>pmP8rT?saBb=8x>8)LCKg--;t~)J z$enY>3;NItU582ch%+d2XjLqJ41P3zdPg>&Dd5aj>s>I|}F1z{jM|Ep0TBFhof{V(C&8+-Hz_UQpiR7fgF zsxEg1V&gI7i7XSpq+1$!di{)5r?5*RDe*a3#*hlRC@qSUp9YDR%`s9~stn{g)Z@Aj zKWZ}n9vDS>5~N9?&hXBl?H6#MTA;gjSpjeEirImqT;TSVrLh`hPBCNSq1SwZ)q`Geeb~W4FJSBdV+R;Jz}Q|&?j8w-Rc*5-s1xBY zOk;lE&&M8%=l@Qv$^da%{j88SW-=4qQBF2T{yA$O*O;WFKlY%g^jZxX(nqL^-FV6? zrrcQZl)F{+5A&UYok7PO{>N}2cnHA{*(X(dB6_=c^{DG4a@&C+yq*2)2`n98>1Y_5 z+xfXfYyarAG`Y_S-W#2hiAeC*rCKF$WX}$+Hj-6Hkpo%v*AZ`;hFfz>+me5?W^ql( z{@|lf4=G3^&#o+)yT0E|DeFzT`%o2tp_vNJVYS1rD9BH}*ZI7DBMN*Ec;vpgxto~; zep~+;bP6kij2`4-wO#{r&$T4_Cc(*EJ6xNkX}dvwPZYn8?z*OMYX z@+1bM99*;KVvlkRmnt477qpuG$fo_*bYsF2hVTV0Ve)G++Q6Uf_^Yf)*}lOa-)-&8BZ&h$v!rdsjoKw