From 398d83b6d5f667122e46f0e478134e4cb85ee6ca Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 16 Jan 2014 02:06:53 -0800 Subject: [PATCH] chore(builtin/Nat): use iff Signed-off-by: Leonardo de Moura --- src/builtin/Nat.lean | 2 +- src/builtin/obj/Nat.olean | Bin 22602 -> 22599 bytes 2 files changed, 1 insertion(+), 1 deletion(-) diff --git a/src/builtin/Nat.lean b/src/builtin/Nat.lean index 1c75d7b47..e2408ba85 100644 --- a/src/builtin/Nat.lean +++ b/src/builtin/Nat.lean @@ -36,7 +36,7 @@ axiom add_zeror (a : Nat) : a + 0 = a axiom add_succr (a b : Nat) : a + (b + 1) = (a + b) + 1 axiom mul_zeror (a : Nat) : a * 0 = 0 axiom mul_succr (a b : Nat) : a * (b + 1) = a * b + a -axiom le_def (a b : Nat) : a ≤ b = ∃ c, a + c = b +axiom le_def (a b : Nat) : a ≤ b ⟷ ∃ c, a + c = b axiom induction {P : Nat → Bool} (H1 : P 0) (H2 : ∀ (n : Nat) (iH : P n), P (n + 1)) : ∀ a, P a theorem induction_on {P : Nat → Bool} (a : Nat) (H1 : P 0) (H2 : ∀ (n : Nat) (iH : P n), P (n + 1)) : P a diff --git a/src/builtin/obj/Nat.olean b/src/builtin/obj/Nat.olean index 296a70a140c184e8029e3cc497b684e7b04aabcc..7fe8f45c51e52ddfe5a8a93bd89c537b955dea67 100644 GIT binary patch literal 22599 zcmb7MYmgnqb)N2-S*>7~hr~l*r%-@hR5(1OxDbVfkVIJB6z|0tQWR{iv{&Nd)vmO= zLgHbt2n)E3p+peI*nrF6!pPVWIKn0`zycGTI00-^A&FA~^24cEKtvq!0Fv{4XKr^- z-`Ts%7PR_t`kd3})u(%A?$}79KDw?s(nyLw)7-FeY!mxS}tH+}3203ChWkSnaoM8NbHZH#Dxj2|y z0IYXp68|Lo=Pg$97As1OWd@L5ihMDuNl%&bvO)wHIwbMP*LOyKI8mYKE#q4r;9C&j zYYuynVVcV3H&{hcV$0g=6ZvnB^e?6Td_1XdO>`*}o7b)#8okzI>$7&Wu?aW?t6y^u z+VfD@^4#X=RerM5UYD&Ug2^Gm#Q7)|_Mtomg@O9WPw($;*oYqXTVosrvD2Yz8{=c+ zoa{?3PKD9c9FGX z;{}yyDQwzfBpS&E$iK-@0O&avg^A`B4vZmEpC>39vIzW53L}k8Cu_aGW&A_U(aG^K zb{1-$2{HAn!BAE(v3boz!6KDFG1PJ(REY;1atX9JLJ`M85%+jw-AKU!{<%q*o495} z!8WmSF)az#MjI!`s#Ad-=T@b<12*yNHTbt(R_GiI#ESOkQLN7G7W|93HLcyzkM`%Z z6J;kUf#og$afS02p}GwP*D@bv-bq4UPFxnT6v6_QDHOr(L~G)>ix{f`;oWSwIk9%U zxuGe^60(g|K#bD<<@=GWv*E>-gJeF31^%pqACEJuq0h2;6 z^?ECyRXM2bK;dM0g*0SacHy_REsuyKxs;M+dEKeG5*63_SyT<_HQ6!14iwLz=$UJ; ztY0l*XY0oCPAG}jT01%3yt-L09H%1iJR{yYIbI)a?Qaoh^R*rI_JR}I(tMTV@#rWL zmB^4^#7J+jls#wYREe5~IEWu#{P)UA>E8)t$%x7CPUV8Nbp3@E{6LrIOU!a{)9G@5o9l zQrJ5Heanl%%ew3XYsX|4bWx_t1%T*8&nR6$U6P_z7hrbQ(FK6!j0g?a8`?d9)YMR; z_y00ln1%#3_^SXV@gdHLOl&XjC}B^Yrb3w%RtH2hwOV9qDo7bMN1#X}OWKRh1=X6C zq2vP;v3F5pJ>`X&BL&bLp&?PvhstCrWYs4o#@1Hot83{m4?>MOghP?UiSNZ}C2p{tm|hZ@ z!hAYBh?v9L4P{9sUq!sa>>7$b$1;r|Y(r~FxH@T?(-q#&T0kfiaBQl5?d*bDaP|-bY&4g^pqoK=En(0 zBOhZRS*iIE#v5%rb(-askx)I9esnZ>cdpaAPzZMWK0t6o)7`cUZEmBaXvzIe=xjHB zbgscrPdgvv+#@4K7SD4+y9urdj3JuLfV2nmYyc!pbEOI>f~RYc*dC1|Ct+@7YGs-n z;VK7E4R@7F-=IsqNYd~)kjsbVgeHC$M9 zJ}{80xtWW3lht;U*;dIkx8wFyt4ok*7~`tA6u;>io@q2^)Z7y^@6e^Tl^z$-)PPzM zV%GM6tu`#^_(Lg@y(kz4@0ks}Mi|21+X>z)hg3X&oO)mNRN=&Y75qSU=Kg9RV&=*z zVPYoy0~j$pbm<7^yDZQ=h~cl&ZU>~=(Zzh0d4pSt-b-m4R>7^zd>yr(K6>JHsOt)9 zsA}HhIrtiezcM2SnUZA5g$@E)pDWme9OF#J+}|Dm1W} ztKRp{%sWth2L$E`!q)KEF9USP>{&?O2l7fm-5af& z>gtUQ=5Eltb7p$ZLUeUrTY+CQ_llQ%Poxq!zquRe)Qpv@2hZ}bQ2C=75*CqX@NA`0o)jhV=}t-2RLk={5@>f< zFA_?T$U4gNy-ImIg+CsK+!2H@xrW>=>K7US)#K$ z>@M{pp?p=rj8=L&f}2)YZJ;5H-x#6caCF!$k^z7tA2YZ0OBsYrbS831kAE1JDh|6g zI_#P|NmygL*Fp_AG>>K{6&4+KnG6^#&oYJoS)?7vz)pYIH9t|xphU?HvOR^i!T%Io zbfU1x*X>`U?EXy_In$44;Gq`(-Y0te}BSjvbdwnk~)7+R#ncRy)HH$5( zsNTnFKgt<1O)NGz_gchWOWO}mh7<-l;6iyMy~;^U4WJ%47m$2Xie!)cZ?38uA)-CV z740E_3Fwn3r)Q@o;&-gN)Ypzrr8TRO?3njvr^3ziA8p3|28i<&k>67&Dm%hf0aK zybzG*TJxi-%N=qvz5xv)JSBjhd+N}%8>Qr5Xx=FySHR-^N5&uS1NB31_g z+40#l>2(R1K6ueBGQ+fxRkZH{klu()p-N*~9kB+f+5sT--j?)L?4ChtKD*tM7pcLc zDsv;4SV{|c09C^(4!K43>#R~Dnr=(mKEwrMfkeP<(LNjl0dg^lN2^BgMuA2bm2lfpxwPST zsCnA8K7i@zH`eZ>5vg9MNE`@0^5uUQc%)2xPHT@xrydu+fvT$UAzyu%RodA!Sp!!^ zHgEh^R}Nrk(5HD1VUbr9xy$ozKAm659|OB z_Hcij9$eN!3dYTakO@;9l@8Fw7qvS5pd3R3DBAN;^cHyxs(gW{xNqSQifB7YInJC; zU3*@{3i#8J=unHi6pQH@T$|KpSMMR;}WS&^x zlIes3fE`|EoG_?Sh@O|8AOIbs+0BJ`Wcded&dGAM;MWR5ReW7;hPJb0!0X!h9_q(&Uth00iQ zv?TC^z_m%Bu_<_6J&2ugjL_Q#?n0AX><>WIu=Wsil|1K$wXPA-$9%Za-8noKM+x2mthYEXIDU>_)om*o$$> zHb+7h8h@yK^|CVgj$RCQaidkdzB7fYk^fVmPZve#YZxwGNLz@yS{cKyEdv-2N2iKOGX~1$FVU+KV@h#4m`t~L=|Y|4GQAC*>Gf#4 zPXEs8kEATY;JH^4c4?;=!R zK;ajdei!Y%6l?}~lB1JEZxf_{q(E8@m)TBP6;_Ml@tS0mxmH`T#rI zr0!XvE32$A{a}tvaTc&}m*;fn$$yLf$dmCYV3nDX@#J*(0E5`Ofq;&C26@Ceu230I zT&lf)MDOVY_yqxuL#gVON_s7EL6QY7aH)zTRWc1jk#3+bzCcK?QMIWAFhn&Inh&leQ@(1cHn+u?4SSQX#VGu4w4H|R2NcZf=u|6v!&e!T z)!_a`deeW84UV|LbOQF%m#Tu$HNhm(Y70V``Vf$8Cq4}_MED4L>58h}s-W{;)d^MK zHnKGA6@nw(1x$NUgjt@mMn9hJiaJAhnV!Dy##M0;Wx8t-PqBb zz|XRT;+ft?HNMd$;}hTe5SIo)u2d;SMEGQUdnY2EU&iNYgJ6c$Qs?oDqUi@RknZAs z2J=aG=@Aaqi*@VzzSLWr8EVlDV7l9Lu^Z!1efnLl#S1tF!p@%^T85cHc@`N*ZR7SfZZ5ah{EDdNB*+ko{ifj+*0I=AAXitcrl%BK9Qj) zf91q*l6_LXLDs`qVFhFw!b;vk5&4XE?yDSe$_{Ti<^hy3YF}CJis>C0%{~=L9G%Hq z&JXmsKpc7{<(!QdTiI!y`~awE{J1zux01&xbaILOsvtO42iGfQ`O-26$kQ%*z?W_OktM5rQy8r^yJb4R-h@S#-iOjozC?ztJ zosJ~lNEHp+)1OYfs!5-Qtqb^X@S_X(A7A}nsb-gf&GZq@O)*Bc0};18>%U|y^epkJ zk*Xg+C{C8yWx%WH`G>%(bW^^N6mFLf!fG&_Db3nlfJR5FH!m`V~c4&D( zlbyB*^IkyVb7xv+cAC<~&%@&(dor7S9t>uuq70lz!&x9r z45KqU4K?l_tEhn$XhV3#NO?}Sk;7j06mt~rvW;#$JrwZN&0qzlY!e9Gf?}M*K1dO9 z$Gu5rDf-~zdZBa{Pj;qIh03z%O&r~uh@Vo5ZjUlf9CW*8!m0+b)(=V;cw%ft=hl?;(jdr3AzuwaVU(TSS)aOMM5Q!(TgU!v zryo&a<-(mgfXuUcpsya}s|QOp+ev_Vtj^x*Rh_i@;@D3X81~2l5GH-#GrI{@cGgg< zI{#-+%${^|7qF1@4icT?NpHsxN%JZ|Nh2#$`c+o}*$?!t2OCOpVkeexJ0}5ubkyvY zWcI~FyMTs6)N*u1kUg#NAO%QzZuV^CZv~J8&He&NAv}fuVKqF)0hxUY#d8GmUb>GX zQ1*0ZOGhu=4Ja<+*RC`B5jx{!@@YgOf7T`Ggrv@b?wRL@?3bC!_6W>uE;|HF>8r72 z(pLV0fC7uiUM9a&7-v9v4mFx#aOCjnX{8ee%8Jv8k8%f>?QA(?db^;?z70X^2Lif9 zGZokBkusEM^<#il5B#`POBZh#`W^~sBYU#qz*_PeO#e0@{}i?FRGmM0>6QIC#(8L> zomXCZsmk^O@^LAW*o=$oFd3l=xorg3TVCVwt1h$9IFP;sqBNlBPAg;5juCgyU=R_@ zx@+K|GP{_HxzyNW)Y#F$th(X0pj8@`RzX^FG2BteU$!%dTNwE!I-#)iTNMgR!)s1J zK7|4b%l@oFVG^1!)InhwhL*BtrI=1ju-xYg;qU0t%Mmc{3Gv<;!Y*J zKByu5elfftp#pRI>f05;AjgiI?L+ZyIkf1=9>`x^napu9AN_%^Um|tIJ+TNSulTck6co};2E2dDu(wE(c5m;-+7aDZ)r|57tj&29glP{ASpOT)W zv$zk{q<{{iJ+!niGxpm2DUe~D`Ehas4dVrLVh_q!I!NZTx`*G=8HgEw&OG1muKAfn z=Zr(sW6C))j#*wDa0B4QL3EQ$O4+K25=EeDg>RLSooSpfdae6X8$Mg=OV)F4akm{#sQ-G&g4}s_4wV3E(22HT@a|M~N zsU}RY4S%#U&EO%JA|@BNDdrQ>6CUv7W1O+k^>T4l^}BQuyGDTmkL~Ny*x(zeE#RhK zLsfrDhQ=!gtvb5Y#8yLOW+~eIbvSdX)bg9$k4Db5%7J_hgbUF6=rBO#XPc&>Hi$v} z#5#PL71GUb!Pq&|Or*Q1I~LFMbq?1+#^q=4$_vaGPH&xS*UGy}AaGaSf)K0L-@nXG zf=Q+NjR2jSG;r~d-ztSXutq)kHxx;);F7oQyxi2Slso`>@HWgSUU=kBtPzk)wp}u+ zZ-wwC#=r`*lL)|YqDun~t+l-tnBP%aHy|%6tr+r1xCA5|e4RaiV6OZqop3De{8n5J z3vYOrVFVD;)d>Msl|KMD`JJk!q=3pem!s7{Y9v|1a*DtZ5F0NdqDD+$eH>UJOdxIP z1a=p#;RYgP?jr~3Lc30Pxjr|Tp!g|Ctg{GUY;TrkjlI`o*76kf3o%vJcC{aA| z%LS^45|~vySU@LZppQSyFLaXJ#>>x?X~$6j4Oro#=w^M~Xz9e7oD`EWA+RkKp?+vi z<6!c{`=I=5V2Ob)J(M#TU`(PK~EX y!jE1eQ8V_F&rzkFz>9<;Q{=3@c#qs1U)SP literal 22602 zcmb7MYmgnqb)N2-S!rPx^Z+EBq$~ov0&HXn7pO2oFSC*Y7_=BeiUL+w+ADF*YFFA_ z2_YU{l8dMqLkS~-F%MV3!N`~hh=|DxWC4ntI00-^A&FB_lpjvT0s?W!0|+_acjiv_ z^qsxCY(eXE_vv#^pI1L-<_-;1D}(E61Jx+|GqsJIhK5I@>#D8Gl zeu^WP*@T4AUmUS<%Rn&VbdFe&jX-~Kgos~cvFNP;qdQ#TQMNg)c)%F zNTu0OjoNGljge`yYZb6|`OuK?Oi?`+g&{bN;3+7lf*mQEBBR9(Nzi{xlN7)2q?k@A zfYv!MihrV`(}pN%LlkAkG66~_RlWdV)KTQTC{qEtj*A@e4XugKA}JJ|MS6=pdb2%x zwSK2E3{&0w8bK5Vv8=r*lK-Yi`$GE9uSS(^kxpe~%er-agWDaoE^7y?n?XaUx;b~C zJ_Cg|p3dLcxCt$6x5nfg#83OSSBHm& z9Sd)KARS3{6vkq9-q>8cQX-v@V2%=Xq}i&o&q+%#Oe9tth;bOja!SM4$%;iHO=7uL z((la08mRWc~ZlW5BgG*uP~R6HS|4 z&9O&`^%tm(RRdB#Q^aB_LWtK^X|Iwy8GaCB<`2bu@fqp;U|+y*6{)oNb?^ zIFEClM;an@2o%Au~tR2BoxO=Z(?wZ9O9Py==INsNVhGFPJY&SPVqorp-DM4W?OodES`RKCTU zNP9RI#d;JSDdH56 zC724U_GC#&vIg>R#Fqmt7ojl0xGaXzMHS2t5>=T5{zgQQ>gM?hcQ>5BuQoV3JjBM# z%o7o&eKjA-3`VxB9mzzb5vYchDG2tU@FnCF60{PFH0Fr9hpX!c(3%Dr{~(E43X-wseiv zsyM@$rviTr1?MsoW!g$ZPEVW`sbtCml{yM9HPM^cpJ$8}z;I#KUmICBT-#Wa{Sr1D z%RwM&&r=SQRvvjSpgMp?t#^e{(c#+GT4ex3na;w*^MXX@=x}AQvA#L4B88b+4_dio(3fVaCQm1Mj_3>=`5?MF zy{UAeL0zJhIQyF%8H0X^qNAW<>=Zl|x8A@o1gPuJP#*5$)Z6G+rb+EhvOp^Iyvl0GY)B8P3=DdmtS`K~o+C^z&e1 zZ0uBruK_{wL%1U{(*u8bTNyj{q)(k>UI#*SwUyye^gzXCHVVt`F#*-mM*z$!w=|GG zKoLe4E!I(-m^o1p&1_AHdSFu_3n{BIGBUKT#9nO^pDZ#PIvr5^Fq-3 z{w*!*D8e_)X?fjD14VM^^0b=w>%u<|NS=coM7;y4#?T=10*#a2!ErTiPQ%C!GO2?U z0}@Qk@y(91pj56bUtu(Tq$?MhP7rx@SS|8rCsngZ@!hCd#6p3n(EqZ(X7FEz{26M8AmN5;uxbY_7(jFb~6mM2$` z=2zxGX1-JOxL(m@K$?zzqgZU!w4>;OCm@jhm-hl6JeyoAa6Iy_DALBmg4c0@TsPNZig= z&OkRafdmg=z&9q8K=X)~P26s@3mjZx4t6r;!R7=AmddvqV|SpSI=%tm0T491QP3Nl zoq|2I+WpAHvV+w3P+THK6doejrHa%pr^x#?NAfN}cPYB}8v`9m{JQ{lO3Cwkm3^aF5%rEy4ot?9m7uVc-g;TyaFbRU++yipz#wt~SbT_(pI{BF~ zH0lfKeh81(@}mUs{gZkd>Qs&9UC#2WXe?h}5235&`buI90~RlFKy$J@_Z!NuG{bKVE8 zy1m2_m4WvYq&+6wX=1Y8xz{51T57;Q8B#fvfcBh+LA6|C>Huq~@dM-yBA*4cU;a0> zvK|uJ51+HNCul}56|KhYzZqu^zz6v#*weGo9$!Xj4VBh|L4I_iy3x&M0R7aU4rNfUJ|b`GJ;gI+asvn4vj0XJJoNkR=i5IkdSupl4V)f$*$uKkrdVAQ}DfdPy`~-+_X>foU&uQhG)Sq+AWm zFH9^Y(E7RNYjEp|Q&1=Fm_iRe{iurs!Nc!&LsS>yH!7-^RlV{W4T4awU;(`F4QH9rur2R;AG zCCnaRa>fX_>=K$8imk&hoWOok)?9UVnV`*Zo*GWqX`}geWM!5q81L1W6>>C=C52BU( zjq(L}!kkVuk)d~JVW@>G7ulYaM+#n^koP8Ao)((lMA3}07*cmrZ{Go^DeiFxG7B^x zu;twqS~I)wz(||{4EG|gF;fM|=}Tl!zy-YigQz}VbOt5N9?fhAfCPnW&yN5dESe%> zV;2HPAEJ>Dv}cZMx*@S2$}2CS_}S(fw6X7wy4vkU3krTDjb^pyObO9YFhulZpUc`n z&5>|p8c!`wwSc6gfzRVTh{i{akI&nFA_bYmCrTvj3*tbPK9V~;C}-jyGd^eP7WcRD zw4xQ_>C$Lcqn|gPs$-Cgf_smM!;ekT)q}!cqnskLeGCxz0#SC~f;x2`B)NDxhMIlo zSFV95R4jXfLwO8Wi95^CgFDjrXi(oeq2!=erkvOe@xC+1 zQwm7!@|1*nuVx_xKoox(#TfuGt?0tWo1%|NB{so(SCTqfZj}(~@@LM5oL=ZsPQ5C6 zh6q&2A3AWa1D_SpoUQMULWnGql|<3e;wf%s`T5qI79xQlo)^bUfv)PLfTZc^SZOpg z@HB>m8mMme-dOkcieZk3c-w#_T3-A_`F#|I;ByZAV*%p}bh1}RQ_(@mIIv4n&jK{* zdwKp{fV2~jHe|ZvT;|BDo0YXATZa2f-)rSTF|xr(`nWQbSJtYV`v$9h{)=nEUr(4^ z&BF(KZr7$;8>B8XyJ!LvATciD%R?lL#10|8f<0pbYAUCMGpV~CHhME~9>Ayvs{I5T z>y7a`?J$b30QD0=N%IeluTfTH-!h72c#PF7dwnP88H0R0Hy}?VWiO=7!6-AU;cb5; zHUBk7d8J-o4bC4Lc;2=SWAQ%wDgsM5->HDfLD$cHsH?~Qz=8W6_#(h1colgwzJef; z^IZ4Y1WQ#-gD_u!U%c6+_IB1$Y}X^nnV^!1g-&@zONw|qhv=&`sNaAtnt){Uw?AJ% zryqo(7rtCvrWVzPzA%zar15IJHw{oc0qj&w2LP&?{=$I=0WN}&@m8l@Qh}85?P!c| zltKehMQ<4MWoZtK$(O8ip&dz`ZVEzwg~Dhuz`V1RObp%$@|m}HZ7;gOH!AMAk|WD_ z)`QGngA%u8@jU>w3y}9Bk$V;(L^b+zVM`rv0SLr*@Wo_8jyJtSmHP^?RJpG@@HGei zSitxWP9K~1*ng{-tv@7g7fMZb1!xd&=wqb0*f4VO(jP*_Cmt=G4$toNF2;wul`Sd1moRws(TOxj93moaw*1o0mzQZRHS#sfco3gR)(DN*eq(=qAM-Nw@b#CuZIdr&m* zvz#alWz{t>r?IEbQBuUu00K|<9{1l!C5&Wz4Or%8t1vQJls~{Ab!bZicQIweIW999 zPh4ufe?aRZBK(X9b5W{!1&D7TEod^M1u4~VR0@TLqewHzXI~)1+th3vouG?mCN>{z z`+MdbDW=nRYCUh&p|qop_lz%uQ;)EF;N|j%;&E|X0s1<&dJ*zlc~-&a5w~iG>MC5pfOBH z8fFUbkz*te=WB0BCCI;(!O@z0)l%+mniRy}=86H0ZB0EV>lMIAY-(@JOdCQW{du1n7 zecQ;=v6q0-9?(C6!r$fP-st+{Jwc<7FT>;a^L{lPlh7WT-??yxl%pzrYKr(D5`PTx z(8myG@kdlo4;wN4a8=O!#*hq8eD4EalOSiRoB}3%GQP7F6DRMJ;6Hv6{0QBYG2DB8 zARX}@u4izcc#j_80A8j`7q){Q?d&Cbr@OsQioL*u>EkB@1&2sj`IF;{IU+e8BlkL4 z_7)YQ+l7|z`M@|w$^Vhfg-Uo<2n>)MUu3O$5JKsi+S}MZ{S#<;M^E_*uWw+qZ@vp& ziaSbnv-0tlR{I6&Mm}r9sO;-HB2Goe926FJI`WsCIhnAFxTMGzKm05)i{i&HekKZ) zzp!91og|-?&ye*nmU#h%hO+dlgdk?L@g0&Z+A(@F*K6e6a?AiK^XfYxK6>7k|C7%J z8b@RFW*!H+FDH%g(gkx%&S@0~AVufL#Zi1cWvru-Q{-0#W*_QGKVa&l=Poqf0L&x# zMWvW~QpX=q^)4D{DqU~s7YuRTiv9;MHGBWkf&b~i_XJEXfx>j3ycJ!f&k5v5l6Qeo zIFgLEI+9Q?6h_IgKK|*1-3eHeKR25?f&WIMPT+qW_`d=sS3=DAF^-MVN3lH>HzMo5 zq|c8mQS(6AZy;nR%j8PX)$RF*psVbeBNarBORk(SjC58`KH7!y=>*v`1srmPC+i9^ zg}&q}XB~PT$Ry`@-miRsi~i&sSHBsJw7^QR(ESjJl&A^$IZ)GJOEppIPl5%VUnh~G zN^?+GCSgBYQ6yJFx?}-byYs7_?ogLp%F4H6oD&sDMVzHe2W;FpaRX}J%qCxffXPCX zUhrr-^R$U>%>#hAdMu*_mY}X0W>0ZUGQ@7Dd#X7|cgaxRA0G#N+NQUJQnE>UliN^i zX7`wYs%H{zxi$%=lJ_pI=U}|n>i}W0BzO}?*Cx`ZmVy;L;lN&I^uwS*P?K2WHzf=d z7J5b5HFjmnzw9a?`M%!uybCPdw~~s# zoRf_{8%=U7vUw-$+5-S+K_cbR_DX^Oz^(=MWK@Yf-{-R z4nb4?>THSBRX#7Fz$21ZDQ_M9Oeik`q8oZg4riXmcEVtAxSjYocW}w>Mli;A2&v?| zP_%v^pkc?YxPm82R~C$)0Io*huLxMUcth7SC}54`*^&cmA!;!EyTJStK;J7nfAZ2R z`7`uCDTN*iOE10DWJiGc6fpyj%dW$uizei<;azVzi-)heOv2(I`U;rRfr2}&|nSR}YTp_d-{v~@c+)>D1vfImB==nApVX*i+ zB?c>8a{}`@6fjuwrzHlH)P$}U217Tjl+N8qY%A_8Tq`b-3F+w{hWac6BP< z=2Jk@$ojMc&k!&@iwJmvo1X1O8Cvx#CVx9FZOJX@fwv}np+Ogast#vk{Mga;_*d9v z*U9O*a^n*PWa1wKr&l)x3>a;p_WYf(a}2;llbkM>;ptKsN>5H8mmTbj&X^q-sH+|z`IF2A*9CwV2f)Kl?RZE zNr`slmWkrvdHHs*j7ErbDTui9jb1PA%tvPRqBhtV>m^`W4{z?!og5p?+k#okw_BxO zQ-`}J(|WMAiNPeg9R;VnE47R7uY#z)%2NkBCXH(#v)PBbI!0g$ z9%NfSSCEmq)r1Q+(GO;(J9rYsW-V&`nwmLXD*gdaKE@du+#nZMWxq=&xoZ%k@z}m1 zm5r_fXf{`R<_!HQ89J{Vv?_{+az!eIIU68<9nLHiD7`iR-N<&U63Ev;xB#sT_5)SM zjl-=Mo%)Hj|1vAIo8E@L3&$DgqQCJGqK@GlD7gIWU2%d5)9H?OyH4I!0)xBL28M*K z{sd++PvaKE^t4I;M`Wct(AJ?}d;J^Ws8eXkTX#-x8dl042pxDEW)Lqt@+a1a$SGSy zg1!}E2=+)lnMVYs6SAeP6>54dFujuxK(FHgU3GP7Va9F>BttiQs9k=PP9zp)=?+{D zi)?t8VL%$t)QSLRl|BSK`JJkoYynkpPDergvVtj*ELUPWSz_>*4QClqGbX4$1*%Xc zh&F5jzYFGYGYLLP>}K1g`rKfc>Zc|#&n$tlJ}T7|+s^b^){&~y=fwE>Tb=21K@`&x zdi4qWsHL+93#c;(y8IK7GY83fD?d}F4Z*HJ&+QDeE-thTVu@)`)WLu}-%=Iohvr1! z=85+~=>xe+;^XK@mt(NnuwZZMPq(yJWDFZ xT(YU6t9vJ&q