From 0660cdbdb7bc4676e01f1b69d748e461bfc331ec Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 17 Jan 2014 14:31:45 -0800 Subject: [PATCH] feat(builtin/cast): use heq in the cast library Signed-off-by: Leonardo de Moura --- src/builtin/CMakeLists.txt | 3 +- src/builtin/cast.lean | 99 ++++++++--------------------------- src/builtin/heq.lean | 22 ++------ src/builtin/obj/cast.olean | Bin 3585 -> 1878 bytes src/builtin/obj/heq.olean | Bin 0 -> 1981 bytes src/builtin/obj/kernel.olean | Bin 24965 -> 25020 bytes 6 files changed, 29 insertions(+), 95 deletions(-) create mode 100644 src/builtin/obj/heq.olean diff --git a/src/builtin/CMakeLists.txt b/src/builtin/CMakeLists.txt index 56d2f1a904..7b918ae741 100644 --- a/src/builtin/CMakeLists.txt +++ b/src/builtin/CMakeLists.txt @@ -93,7 +93,8 @@ add_theory("if_then_else.lean" "${CMAKE_CURRENT_BINARY_DIR}/Nat.olean") add_theory("Int.lean" "${CMAKE_CURRENT_BINARY_DIR}/if_then_else.olean") add_theory("Real.lean" "${CMAKE_CURRENT_BINARY_DIR}/Int.olean") add_theory("specialfn.lean" "${CMAKE_CURRENT_BINARY_DIR}/Real.olean") -## add_theory("cast.lean" "${CMAKE_CURRENT_BINARY_DIR}/Nat.olean") +add_theory("heq.lean" "${CMAKE_CURRENT_BINARY_DIR}/Nat.olean") +add_theory("cast.lean" "${CMAKE_CURRENT_BINARY_DIR}/heq.olean") update_interface("kernel.olean" "kernel" "-n") update_interface("Nat.olean" "library/arith" "-n") diff --git a/src/builtin/cast.lean b/src/builtin/cast.lean index e95a686242..b429bfca80 100644 --- a/src/builtin/cast.lean +++ b/src/builtin/cast.lean @@ -1,90 +1,35 @@ --- "Type casting" library. +import heq --- Heterogeneous substitution -axiom hsubst {A B : TypeU} {a : A} {b : B} (P : ∀ T : TypeU, T → Bool) : P A a → a == b → P B b +variable cast {A B : TypeH} : A = B → A → B -universe M >= 1 -universe U >= M + 1 -definition TypeM := (Type M) +axiom cast_heq {A B : TypeH} (H : A = B) (a : A) : cast H a == a --- Type equality axiom, if two values are equal, then their types are equal -theorem type_eq {A B : TypeM} {a : A} {b : B} (H : a == b) : A == B -:= hsubst (λ (T : TypeU) (x : T), A == T) (refl A) H +theorem cast_app {A A' : TypeH} {B : A → TypeH} {B' : A' → TypeH} (f : ∀ x, B x) (a : A) (Ha : A = A') (Hb : (∀ x, B x) = (∀ x, B' x)) : + cast Hb f (cast Ha a) == f a +:= let s1 : cast Hb f == f := cast_heq Hb f, + s2 : cast Ha a == a := cast_heq Ha a + in hcongr s1 s2 --- Heterogenous symmetry -theorem hsymm {A B : TypeU} {a : A} {b : B} (H : a == b) : b == a -:= hsubst (λ (T : TypeU) (x : T), x == a) (refl a) H +-- The following theorems can be used as rewriting rules --- Heterogenous transitivity -theorem htrans {A B C : TypeU} {a : A} {b : B} {c : C} (H1 : a == b) (H2 : b == c) : a == c -:= hsubst (λ (T : TypeU) (x : T), a == x) H1 H2 +theorem cast_eq {A : TypeH} (H : A = A) (a : A) : cast H a = a +:= to_eq (cast_heq H a) --- The cast operator allows us to cast an element of type A --- into B if we provide a proof that types A and B are equal. -variable cast {A B : TypeU} : A == B → A → B +theorem cast_trans {A B C : TypeH} (Hab : A = B) (Hbc : B = C) (a : A) : cast Hbc (cast Hab a) = cast (trans Hab Hbc) a +:= let s1 : cast Hbc (cast Hab a) == cast Hab a := cast_heq Hbc (cast Hab a), + s2 : cast Hab a == a := cast_heq Hab a, + s3 : cast (trans Hab Hbc) a == a := cast_heq (trans Hab Hbc) a, + s4 : cast Hbc (cast Hab a) == cast (trans Hab Hbc) a := htrans (htrans s1 s2) (hsymm s3) + in to_eq s4 --- The CastEq axiom states that for any cast of x is equal to x. -axiom cast_eq {A B : TypeU} (H : A == B) (x : A) : x == cast H x +theorem cast_pull {A : TypeH} {B B' : A → TypeH} (f : ∀ x, B x) (a : A) (Hb : (∀ x, B x) = (∀ x, B' x)) (Hba : (B a) = (B' a)) : + cast Hb f a = cast Hba (f a) +:= let s1 : cast Hb f a == f a := hcongr (cast_heq Hb f) (hrefl a), + s2 : cast Hba (f a) == f a := cast_heq Hba (f a) + in to_eq (htrans s1 (hsymm s2)) --- The CastApp axiom "propagates" the cast over application -axiom cast_app {A A' : TypeU} {B : A → TypeU} {B' : A' → TypeU} - (H1 : (∀ x, B x) == (∀ x, B' x)) (H2 : A == A') - (f : ∀ x, B x) (x : A) : - cast H1 f (cast H2 x) == f x --- Heterogeneous congruence -theorem hcongr - {A A' : TypeM} {B : A → TypeM} {B' : A' → TypeM} - {f : ∀ x, B x} {g : ∀ x, B' x} {a : A} {b : A'} - (H1 : f == g) - (H2 : a == b) - : f a == g b -:= let L1 : A == A' := type_eq H2, - L2 : A' == A := symm L1, - b' : A := cast L2 b, - L3 : b == b' := cast_eq L2 b, - L4 : a == b' := htrans H2 L3, - L5 : f a == f b' := congr2 f L4, - S1 : (∀ x, B' x) == (∀ x, B x) := symm (type_eq H1), - g' : (∀ x, B x) := cast S1 g, - L6 : g == g' := cast_eq S1 g, - L7 : f == g' := htrans H1 L6, - L8 : f b' == g' b' := congr1 b' L7, - L9 : f a == g' b' := htrans L5 L8, - L10 : g' b' == g b := cast_app S1 L2 g b - in htrans L9 L10 -theorem hfunext - {A : TypeM} {B B' : A → TypeM} {f : ∀ x : A, B x} {g : ∀ x : A, B' x} (H : ∀ x : A, f x == g x) : f == g -:= let L1 : (∀ x : A, B x = B' x) := λ x : A, type_eq (H x), - L2 : (∀ x : A, B x) = (∀ x : A, B' x) := allext L1, - g' : (∀ x : A, B x) := cast (symm L2) g, - Hgg : g == g' := cast_eq (symm L2) g, - Hggx : (∀ x : A, g x == g' x) := λ x : A, hcongr Hgg (refl x) , - L3 : (∀ x : A, f x == g' x) := λ x : A, htrans (H x) (Hggx x), - Hfg : f == g' := funext L3 - in htrans Hfg (hsymm Hgg) -exit -- Stop here, the following axiom is not sound --- The following axiom is unsound when we treat Pi and --- forall as the "same thing". The main problem is the --- rule that says (Pi x : A, B) has type Bool if B has type Bool instead of --- max(typeof(A), typeof(B)) --- --- Here is the problematic axiom --- If two (dependent) function spaces are equal, then their domains are equal. -axiom dominj {A A' : (Type U)} {B : A → (Type U)} {B' : A' → (Type U)} - (H : (∀ x : A, B x) == (∀ x : A', B' x)) : - A == A' --- Here is a derivation of false using the dominj axiom -theorem unsat : false := -let L1 : (∀ x : true, true) := (λ x : true, trivial), - L2 : (∀ x : false, true) := (λ x : false, trivial), - -- When we keep Pi/forall as different things, the following two steps can't be used - L3 : (∀ x : true, true) = true := eqt_intro L1, - L4 : (∀ x : false, true) = true := eqt_intro L2, - L5 : (∀ x : true, true) = (∀ x : false, true) := trans L3 (symm L4), - L6 : true = false := dominj L5 -in L6 diff --git a/src/builtin/heq.lean b/src/builtin/heq.lean index 8ed6aa1829..87c973708e 100644 --- a/src/builtin/heq.lean +++ b/src/builtin/heq.lean @@ -8,13 +8,13 @@ universe H ≥ 1 universe U ≥ H + 1 definition TypeH := (Type H) -axiom heq_eq {A : TypeH} (a : A) : a == a ↔ a = a +axiom heq_eq {A : TypeH} (a b : A) : a == b ↔ a = b -definition to_eq {A : TypeH} {a : A} (H : a == a) : a = a -:= (heq_eq a) ◂ H +definition to_eq {A : TypeH} {a b : A} (H : a == b) : a = b +:= (heq_eq a b) ◂ H -definition to_heq {A : TypeH} {a : A} (H : a = a) : a == a -:= (symm (heq_eq a)) ◂ H +definition to_heq {A : TypeH} {a b : A} (H : a = b) : a == b +:= (symm (heq_eq a b)) ◂ H theorem hrefl {A : TypeH} (a : A) : a == a := to_heq (refl a) @@ -34,15 +34,3 @@ axiom hpiext {A A' : TypeH} {B : A → TypeH} {B' : A' → TypeH} : axiom hallext {A A' : TypeH} {B : A → Bool} {B' : A' → Bool} : A = A' → (∀ x x', x == x' → B x == B' x') → (∀ x, B x) == (∀ x, B' x) - -variable cast {A B : TypeH} : A = B → A → B - -axiom cast_eq {A B : TypeH} (H : A = B) (a : A) : a == cast H a - -theorem cast_app {A A' : TypeH} {B : A → TypeH} {B' : A' → TypeH} {f : ∀ x, B x} {a : A} (Ha : A = A') (Hb : (∀ x, B x) = (∀ x, B' x)) : - cast Hb f (cast Ha a) == f a -:= let s1 : cast Hb f == f := hsymm (cast_eq Hb f), - s2 : cast Ha a == a := hsymm (cast_eq Ha a) - in hcongr s1 s2 - - diff --git a/src/builtin/obj/cast.olean b/src/builtin/obj/cast.olean index 3712292705c70fdad4189342efa5778892fab4e9..363cd6d3b92a57ae797348d9e8b28a42198c5a13 100644 GIT binary patch literal 1878 zcmZuyO>fgc5M8ewH;9A}5!Gpgs7q;DRa~I-62ze(P`Ct;xPwXEG$LOl7Ha=J^WNCm z#juCTe7t!(Gdot6vpic|O=r0&PcWUYmg~a&%-4&2W=d<66_t9O|1!U`wXx%DQ<&IZ z7;C@YuJWM~u@~WqWpBN&9h$yNXn_|h0#dUdOwp#gDUK|6hEmhZ%1x;$K6Wc4X zZis6g5)BbmEs8RfIl#x(Eo1{`B9R|{1T=`or0D_^vGP5rU3wFG`;d3lLA{N<9e8^X zA%sU0v)Fc3XUa?>IgiJHQ{%J_7}mkD());O(GQ&Z5Nd~jM^5cP-KBRIYNEYD-J{CB z_M3L|!UWm}Vl3fEdx3qlb-KD*`mT7ie*r@H(kDzYk)|U&M^XwAL$JFR!)LJT;pehc z zd~}Ks(WqMAdoThy+XXJx*<$0b@b+7LhfKLnw(+l}qZ1;;I*y^4QMK#|p8>raomCqu zD`8=wE14}Y!j8%b0M1D3#9A#5F2fJhrRc69pbc`UDQw-k1E)T9>LJt-vCo{!l9T#= zxjB9Y^b-r`%X{50QePxi*>jEZJ+&v`S+LH5boH>%o%wso%+%4PAnBe!eu3a*QfQ9J zmB`t~u6P1T`5h^--1f@9jT~O_#M7C$65Q@rTl!$CRwXDjwI$W02sVgd8g8<8cVjoZad%VF z*Mzc^1q1q2p(PJR5J7zEgMv@>k5POR`da7v=AL_YLm#}*$#>?=%$@npoVnX(J&7BY zwR&RG$F8k!G+P~WJ83nNx=B|z;*N>8jH|UbSK1wubC->CH}7sFi$)f+>YH=1u>x(* ztxzN2Gugg5xGkQu&1M~rv6;Z0gVzv*gDwyBlKe9fwtmWhzEfU&8S&1i*9-jUZ z=S-d|2uGL$EHL9EfF}r#26zn6QhPkWQNXct4uAB~K)_7T4tp+#-4-nzxuTh!aITe9 zgjYO_MZNQ!9Tqh?Ly@)i-Su^rNb`X+gl4cnXvRX75i@@kT0NK70(>1%OFI?dX~3~_ zkc9uEFxZlc9Gl=xtm&pF<*Pa=>QGgu6*t;1Eb9vVwde3R@;xeG6$)tPru8V5Y*}CA z&P+H|t^5tDNdnVS5}2mKNd~0BRDh)b&jQZSfTYX>YR0iugeX8nFF14PX-0m~^(H&z zGqT9xW>|YCZW*^4r}q_BStAS3MjrEkHAkM+3u5c6#g#_@e;xM6n4>~sXg5YA%1tpX zgzz;04W>CQn*JBW8yo${c9~phzCJ?+Kn1$@m7bS>cY!CtDrAVH`B0}X&Q9}{oU2F_ zwJ6d;?}^uq=lOy~YCnW`L@Q;S+K*7sIJG<}7R=+aJa3tb#*}FUp;-Yfdx9^?BDC#l zvr%nj^~;n=>lZXD>KLv{AT(Nk2X)}Nm2*`O)UxQCTY&U5o{_BnnS97wNn=Uc*&oAJ z$JNyUuK{-0tvqps*P*>d?I!_#3Rt9eKEMUQ5o&J$&J^7Iw6UCC1yGzXkweTVW40l7 zAoL0VIq|qC9>Cl17@2a8Lkt?7cU>Sli}gxL=YBDq2={w1;>&Up^6fOF9;0@yGS>rHCOZK}XPsjc$i#umK|kOh z(1tGV_P^fS<}5VR&u4CKj~f8R6CoXhl&;86CA%W1>q7@PA8Y(1gXFMzCvuIfac zB>904%L4R}*sD95aEPFL47LOBKOlbNK7FbD9ZGFM2|oRnk51yZ>7m^ww94u@#ArzP zDZ@R1oeSDOseMW<1mlw!O}Z~r8a)p7-4O5*A@f%Q4MQytg6xp=>>G4N-j>&IkhT1^ zQQ2%HTl%{ZsSM0Da=dS@`F2rN{sZpu%P0LdOgbk&1NrdAFv^O*nZ*)z?m_4VDPa?^BF#)f%G8>K)xQv< zK03c92~;&1WO2O?e)x;%?46g8BikZJET=^_*To%+mY($y=0je`)F z{)(8;b6J{a5G-I>imQ0u$VQ>$T-xcdGQChokBRi4Wp--MrM{H(u0gR&QyrYLw5NQ^ oP}!3(As_T$9H$>oZrRiHffe^?mHoeIRn)`0nO7U-Yxr;9e@STyod5s; diff --git a/src/builtin/obj/heq.olean b/src/builtin/obj/heq.olean new file mode 100644 index 0000000000000000000000000000000000000000..6ece1454a2c21e47d9c31b434d38acc421af835c GIT binary patch literal 1981 zcmb7FT~8B16rCA#LDm9MOZ*^e#G&PwU>7Re-MU>!c{2WU?>Tp; zvo=xVK3vY+uQ}(=Oeym;DY9Xnn&z{^(YUN?bCFg>nww^|pVa0msf;^MznjSI8s`qL z$LW!g#Xu_~ml!M10^qaG4azb%=HqBg2aL0JzpRsbSQc1Xx3goMfY&hcT^7Tuw3?*G z?HS8<*0|%cZUv5J0Te8qrkNp`J+r74aJxm?WJ=0kJ!?2);jB~z9K&PmbLWOxX3Q2= zi`bWZI#^<5;+}KTgkQ_+rQMc*wWLy)em5j9`)S0py&{o@Z>0yjiuMaY+V&>kU6^IU zdw?-v7tj)}1Fmd=6Nam_;bRU>V7cC-7;tP7LM-+Q?nrFG1`Yn8QS%oOYlv@<(*vdw zJ_J@fz?6hk*wPfxLuc50d#aY8^q~ z+y&nos3Gx=-}4#VqFlGFtE8B;wa@l_hte>Ojwc}CgdqW*33lKhwh>V}{<7{WC8Y2j z^^u}^p3+P4M4;4=Iw^~@s!eM51&VYmzAsf_P#XIjxlBr?Ozdvr4|&L2$uwi%SM~*{ z3#b{UFCA>6afJGq_6^_x8}W_#2qb)IWLc&>iA)=}gLVZdX8c4AZ)E0s@M?&)r%ZpH> z5#PE`eH0}(OK;mYeWWq_efcC!!YfPi{2vk*X2&Ne0R=N{pUs>k#IFNKhc(SS`w;no ToS*&-zQ}_7-WR7I@Gtup`@olQ literal 0 HcmV?d00001 diff --git a/src/builtin/obj/kernel.olean b/src/builtin/obj/kernel.olean index 958e9faac68707745cc9244aa12ca58393a1fe25..395f6b4f808ba1dd36335c95adb0edc929441e48 100644 GIT binary patch delta 4601 zcmbVQd2E!|5&zz|`+YXPu))U07$4ZXJ{G(_u!)T?Fb0DS_WH)y_#il3wn#{0lqMw! zA~97$fC)jA2C71(1`!U?^b!R^A|bULiXuX3M1@4vB!yIJBUNbvcIP*5*H@za(LZ)P zZ|<2l^S<}I>wR_peRZa14qXn5q0r=r62mae@-&8q2cQ%n#bTh!fm(uAjG>Ew#tC&X z?Vj_3+Dsv-FRRVx_N5l7(9O(LQ4GvIbTh4A?V(CnrrJ;au0(Z!UUltEf`oa@W@v;1 z+~=RFw#;fQ%wv@8&Wbz%JcwzzLOekm+*LUTfNul{;-C2rvwN{JN?lm*2Y3hTjj}#K zcif3Hg(~J?-~36y&vA-QPj(3-1v+rn1H^9)&cvE|mR6^GbH%XK29o3b9+28igQ^5q zt)rperKg6%yHwP?M4zTtMoaG3L4+0jHLp`yMjn^u$qb)n-T}U?10DwT3;I`Pd(^*y3ac0~n)j$9Yo&TXC$iS-eG+3M6z}oP z9f7jL!N8DugoEdBVlBI*izGyw4tiF_BNYcWdNdVBl%GA~NiZD_nmzZ89U?Ugq6z*K z9J9tep`MO-tp!WE_eR%hCWzubXiRBxcv^`C9Vw!Tm;;(S7!Oq1kuYk*&mLV*b}Va0 zJS*#hJ8Yoe<#@c16iW-Sv?KHB4F;W_SFS6S4-2EA5LE|B&BnGm%IS!=y;v&UIzg!wO2%IS^ma-bQqKqwrI{Q~%FB6C zJOuG-APfiMHnDg`0QBC__w%rj7Hx>M$LepA&m{k~xJDah#>Q z^Z%n>qLjjDx?fPBh8SC-{y=?&ISdaLCaaI>w}l_7jr8LMw}Zb*Gg(P}Ko<++Xy;>I zb)L>WmJ@b9gQ+HBG%R{AWICBeAE+?8Qj}z)AkL}upeQSVCKT^dNwm)qlK}Y~@Kao3 z_67(>11N6#sCce&?OzzDTr_iGl1ibXh1smv(-}?AE%d}DP0Ge-g4zPQu&`HUQA$ac zs-)VIB!*i`il$cD=62YYHgguxuS$}cbF(Blc%{zh?~+kWX{qv2W9gO3HHtCc)(mo0 zcg+eLt%X>Zf@tf}bhNs7K?Fo+%ZNV@T?s+Pu95erYhWFS=E-kG61jX%@>ry3MJsNi zE6YO-%eN>GU0fcYI|MWOE+A%mvG$wo170m_2G$e+n?hE^+i+lo(t9i8>G`_&9a96v z!+pY%$fq-=uya<%_k{}q#HhZWoCp(jIXsg&0cXK1VZtNbSrHYfL*kXS7@(YnS9r5g zJ_{cN3j<^oNd4zBD&@AaL0quBe=GkrOgEjWi=nMGrQAfPYG&9EnaG{;$C|>hX6dIY zh__H!Z9Jdj>9tvE3N_Taip4Yb_j{7~R>#0pIGwGHjt+F5q#|3vjHA^tVitpCO{cGF ziw96v9d_iTuISc%#(dc=xz$kGqQLn(S6XF8ufw5mRhkC|=tZL=TQWAsO|f$(5n0ysgR z)fZ0Fhn9Q_9w97?D92a8>V3Y!#Ad%b{tQT=^+|>%wSG$9_zH`3lftugDgz%P6SXp| zV}RAbjsr`Py@Hs2GFZQ$O$`n9YrM4HqRR~vQ+PyHW3qaK+>K4)!{bsIrdJw$zG0b* zr&(2>v;KPlOj|Ys6Q6wD)19)GPaE1o$0A3pMFAo6BxN?GbH=`=qthOad9zxeah1&G z!s5S)%O8Qzf+|gLIqnRXv{fQZYcKE8Q_a4RzXYazkd8LR(80%I=uCZlkR|C~qqvrd z=?~MImfP~uvV)O;{z76Djb5%J{@TIR*jnk9N0l@@jwCyhxdU>p824RFkXMx*N#|R0 zR0w_18mA)3Zc9rRHL(LVb)D7n7-0iii&nI~$mh(}wt_BXD*lvc- zOa}VtX|xNY8^1On5=EA+xTZk0)taSzfPP$HHW@z z|Giw}ZM1;h7O>rd^PDe4SJuqqLeA@o4eIme6`628`PS0Vt#%-Q(bawi_^%3*+?bUvk5xY51#}tIcuawBO?oj!cf^1YPEn2%> zu6uSXU0mzd<$4{OdjsWq-CwSewHY>=mowm+@ngBFD}RBUCU{W|%52z0q|9&RgM*!r>F~+ywVxoTO1s-emUdg2lX~%6Cj$NZIW-p#o`% z!x=HQD=4pX57l*7)?gcz&w?m=Tlr8FLoT5GSpOMI*<2H|<`uElsA-MECv9cQ3EHE!j=( z`JeB+&-u>xdh3!ncu8F7Nz2kSO|LQa9{JTY)6_Qw5nqo&6HMK=sYj!C)1DQ*v?BdE z(fh`g^fF=Zm69S_0)2!cT-(J6J>$xD9EH9UpaLL7Y8L^~oGuCUQM%+BwxFt?q6T+@ zI7M6CIde}#0VXop8Osh_9O%zSZ{-px#mAI*SZ3;;*tQ}*Z|ndx>; z7n$l8DJ82qmNR<~qR0kc{XKdzt4NH}*(|?eU!TFgPLbK^bDs%FYauEZs>*J+ZbJP! zy_Wq{^k=N&27Cq7zfx9CTlC+6GRun?^;<+atHo{lQ_fa3J#1`({JH)`6HwOgOQ5Dl zRpkN3k&{IBZWDAhw{a;_u|o5p%wGicj)-L+~5G&7zbbKH)+x)2j zP%vBElre4mVsiCt7!ToAtt zHPnu$1KQ=E>tQ=Wdy8KV89_i=JZ&q=iqt<-1BmRS)k}&aZcY(~>G>tq;y8Vkf-DiVjs=%tg?n-FogbDluS>1(#6l|RZoG0S3M5#A^qL+q1Zyd zF1;bXqF0tSil5QvOA91iQ1+<^q5Ea2R;biA!YSRG6GU6Q2SpMcv&GSu-mrPeF7|p2 zUNltCa8mfPMM(}*-^;W}WGh|*Zpy#mpr&Q1BAIq9%adltmMxd?<7IK7MJoK89DZzh zwQx~ud5*JkvP@bLY!q?{_5o#cmGr~%vZzWc;0>*06wsY=hp4283WxB~;))K@K!+>7 zmC%sMu{xm4?P_p#trSsNA-brp(jU_$`(^7B;2T}sF{AY3%3Y$LoXZ_qM?oG0=yS8B zTnGw3DBFQLk*jRSf#qjK7{yfO<{rqB6oJ+fD3P%qAWQ;YV!UIEYtS-wQh!xe$ofp+ zophqAV#!EAY!AMgPe#U=aa74mnsUt>YhZCx=!(a!2FWrG(9EvY7P~+FjEw;^~8$?ZQiywGCp7 zj?{X@pDDIB!-|&Da>xFn_Iu(k?S8c0d5>dR3?t){CFc`OKLg?fee$SFoFQvvt`M}M zZa(=|7F3#+-Xpnzv&kzF)0&K)`^$t~jX5E+IrQer)tOFb@jP=`; z<8w#w+3H0@o6*$a>y}IGEnlLDB4=Y9-SN3fVZlt8WdRPf7CC#}gPVcsXTA~0%2jEO zsX$R_bKYdVRUU2{S+yfTtBm^k_b9UcoCD;$8==#{$U`uk2JU^1*Y)rIpUohuT{%UUt z+C=4IpVcevJe9X4f9f`8VuhM<)Z?2M!BjH|ga!2W>cq4jo~JEP&~D7GIm9s6N#VfC z0On9~V@f=BSuU=)#`;`4vz7dfu@*N=8$I5b^#7Nlg5GIN8Bz{8qhaY#RfNm%2>j!! zVfOv6_}it_LuZ0J&}@H5&VdfBhW(uY*$~qD0WiB-sQhy@W*$iSGZ&SL6Efxw8e5ZZ z?*zICU?bgF)2AC>(<4ou$U_KSHlO?%<8-hoLvBw$YHD40FVK{r-$V8qjv4(Tz-dbL zdt%gP*C7eUJ%nbyKz;rass5^ePfF9Yo*v|hQ9B@-+B`u;&7LyV)bMPc%fdmXS4yCn zrvQDx#(+7e)%FgkKcLr|o2^4YPtthv%oOfXd5c55NS!TfBgdzuFiyW}@kfmFI@&E& zWv&a>rn*}#iR*j-^3r9Gc9o6faOdl1Xye*Unb)DUV==+CDtRVOT=O!Ot@A{D%!a?q zRQmS1h0#btq)4DCYZvI;I=}dczFya;Lcc<59`nS`sJ<$~AU)rdOh0|>O@3opHhN-x zg0Ruy_0?{EP9aWyA6a%;nZX?xYIj@`=tm{6?DW<8f+YD4R2QELB*RBP-!&w=qBX<8 zmQZ81B(6$Je6O+W$`I{u-7j|%+lG>EY%;vzS{ZB#M=Cd<#T*;6(R&7Wi4&F3+5oUV zt+ZKVJs6l1;_~!7vB7P>1#zq?%b+V8c1h3WZElr+DfPEyJ4)d|J$<;DHU+KlLsC9> zUT>2(@CS6QExu;yByUQo5)N80R+r~iiCMVy1}+>d$*%y#p`7+#^8MYyBwIN5AZ+=u zfy;~0{r1JePM>tl54BpA7pm(>9}*CPBp*NOIb~q+awA#T1p;qb_BBm1=%7V8fFLH? z2LoIWWLt0`D!o=Ew6S=r^b