From d6167eae32efa252159b217365b8a959ce39eb95 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 8 Feb 2014 22:28:15 -0800 Subject: [PATCH] feat(builtin/num): define add and mul Signed-off-by: Leonardo de Moura --- src/builtin/num.lean | 29 +++++++++++++++++++++++++++++ src/builtin/obj/num.olean | Bin 16323 -> 25180 bytes 2 files changed, 29 insertions(+) diff --git a/src/builtin/num.lean b/src/builtin/num.lean index 74b126305..cef353259 100644 --- a/src/builtin/num.lean +++ b/src/builtin/num.lean @@ -476,11 +476,40 @@ theorem prim_rec_thm {A : (Type U)} (x : A) (f : A → num → A) show prim_rec x f zero = x ∧ ∀ m, prim_rec x f (succ m) = f (prim_rec x f m) m, from and_intro Hz Hs +theorem prim_rec_zero {A : (Type U)} (x : A) (f : A → num → A) : prim_rec x f zero = x +:= and_eliml (prim_rec_thm x f) + +theorem prim_rec_succ {A : (Type U)} (x : A) (f : A → num → A) (m : num) : prim_rec x f (succ m) = f (prim_rec x f m) m +:= and_elimr (prim_rec_thm x f) m + set_opaque simp_rec_rel true set_opaque simp_rec_fun true set_opaque simp_rec true set_opaque prim_rec_fun true set_opaque prim_rec true + +definition add (a b : num) : num +:= prim_rec a (λ x n, succ x) b +infixl 65 + : add + +theorem add_zeror (a : num) : a + zero = a +:= prim_rec_zero a (λ x n, succ x) + +theorem add_succr (a b : num) : a + succ b = succ (a + b) +:= prim_rec_succ a (λ x n, succ x) b + +definition mul (a b : num) : num +:= prim_rec zero (λ x n, x + a) b +infixl 70 * : mul + +theorem mul_zeror (a : num) : a * zero = zero +:= prim_rec_zero zero (λ x n, x + a) + +theorem mul_succr (a b : num) : a * (succ b) = a * b + a +:= prim_rec_succ zero (λ x n, x + a) b + +set_opaque add true +set_opaque mul true end definition num := num::num diff --git a/src/builtin/obj/num.olean b/src/builtin/obj/num.olean index ff668ea828d940d75ee1856e4a693f9d2ce0bf1c..1ecd933e5c503e620318a650c41945f4487b03bb 100644 GIT binary patch literal 25180 zcmb7Ndz4;Pb-$1AF=PP4&>Dlb*ac)_sx}GQnCR*hC1k)5k^lvQI2|(Iz`)Em$;=mC zRaZ;3rH)t^MijMHkrqe(#uN9nWw=v-(|fM$ z+_n@EzL zY?#ZXXwzmk%BR}tc{U96GcfI%*3Qn@b&f9~WD<&o9V3VB&h=UvO=pEdT4G@87OWD2* z9eo5jw$v+Qi)lh8UjdwCL$g@P{P!kyZNdg4v>9#ihb?9guf?8hP>gK{Qj=>DJeQoF ziQbgps{mfoy$;cvw4fXoI4g;M3c$1n?TZN#H+ETa&S^DLU{hsX#2bea~n{63tTOz~*2R~3OvUR9xnci%0 zX!`2O>x(IlF-(6ynxGF$lIVcJ6A=9H}|>*G-F}+ z;_*{x?i8~Z15O60p3ea6L(}ZdOsPYbZj_z1ICn>BS#FUB&!7rlf~m_vN7 zM1taLYxM^osbVzjKUt#)5~vxnC`!@PV?*dttem>L8WT!7v%WJv> z1>1L`*{}-jr_lt5p$;{SfzOimHh^B@JR2PzpKh^;vpu+H%GNA}X&PYzC&>~o1?&_z zJTfvgHI*Rm4(}Q7xMH`E)qAGZw|lHmooq8gdiMmKjh5)vL@9XIp4WzbT;RIkjT!rj zK5FbFs(k_j2MJCBe3BqH^|zXCH@veqGvR%FIvsd*G%gaCLj;CMX0J`$A-!(0podyE zig*{&kaUAtOnDs5Qk!z2rfl{rHnVLiUUyUdcTmX+G?ty-NfzV~!g(q!~mnr0an zq*JH_nZt_DqOt8TxXU&o3HOvqa^8YHS;hh#?oqlA8zZ~rh9W>=d?^{>?*A{YbzBt{ zZaESdIHqk{MT2@JjZVA~tMY}gz+SPRDe#=cM*lolc*g55O~`z2#lqZ0$zD3iU7U-i z&k9k?i9T0R4N;(}Ae78wB6*vqH?707EOdMoK6f(lX$8(P18f_1lNwc%7|ZsS-2=Vp z^8Oqvz79=X&EWAN&iHG9A#9lMLcOJ+`p)vQW!XWbgGP3UGkaCy6IL%KT&8S!2=M$$ zYg7py(~6OHF`YEHZKSs%8e8=rmux;B4Y`nnxd(k*2_cE3770lw(T^zdK7#c30WSP! zBuMbj0V;FeVod-;-q-R-CX(#_82$BI64J6D` zVjnQ~x!je$kvLCOV$#b8l$en;la$Az;QW0T>{2vb8xDx-FEoWUCCaVn@y?s>=;n0ZKZ-9- z<)&dHZ~Y)B$VERCzz+l5NXh=nptMEsBLK(yF-Ae8(D&il>CB*XM_D)X)Jmiq?i&f> zb#4GG2LjhI+-RI`vu2?wIJ%#NwRxgNVWw1>6357tR8`+1ZKZEP^Hx$`2Jny2yv-U{ z1hZ2}82RI3H{M}Sc^d6Uv!059D)V{UScwBNW*jSS$T9tBsXd>mXKz40^qv{-Uskj>hawMy7K5~mWq`&g=so4KeJH%w4l^aW_5n9 z2YbXer-5X1a`cQ*PU%Y@#Uj*(KVaW&Jy3G7-ERwrZBuu9sx>+u;-4HVD2}o#06qxP zGaNeCpmcvT+k&oizj7js>DDF#2k>Y&j?QcbxWlF?H{06AsOdIq8>m&;(hWO`aKM06 zP9Rqvqhn0>z@C3!8(WV%y1FnGZU5mU$VGcYIJXfW235Jj=LFh~k^M^_?niq+8b(rx zmbR=}T(s#4=adwPPS%l}nEOC)wspd)50HQz(`Dd_Q7FYeN&0%xUX})C=j=IMwlYWm z-Dnc^0HPPrADVdVHvL1^6Caz9XG}x9G4P5ZCntv0NN1MqKY=7q`{^6lp^Rsp>DMvT zRT@SlW-&Oc#PjihU>gkcx~o+<;=M%(0(n}=kX zJ`4Q8V3G7cR-)%oOoSPTpz2NO3IipB@IX8<*`73CuFUiCM%RY$7L#`Nk>WQ&TYLVX zK<)Xg)^Cs8^P$Ag>OkoVXT{|i<5{uifz`d+x0SuZv^6;u-we>U?&OO3I%LsQIIC29 z%eHAcPI{@Gq9&&n8WMz5Nz*+K!>|f4`=E_%Nn~{3LQxs3a2JNqY4Q%Tpw9a2Fl=R2 z`BrBD$7zyEnG9gGjA0D^G3FfL5NIu>rKx%PY0geG7*3a&Q%>JFp|C9{f}f>CYualN z6Oy%osSdIvhtVigge}(L5F}2QU>pM21Y_#th@Uz14A3daD_xECO!k|=J*A`@y{8~m zv13-TC@=5UwE>lUC}Pvp)=ec_4brQ*>My|nw2-YP!}A1f&up76t~iuj}#<$EIg9%8x=E8etTWG6Nv(20*@s{E0opI&ByFjL*(wc7*fL z?5A1(7hq)xkulvh;djYb>?W~P8f4Q-=P;+MYgDwwwVoLkZ%3<63q0j!diUg$qjMT? zmLhV=vWhX5fd|pGF#OBuF?JuCU&X#MAWi0Xsp9K=VbGgP2Bl4sf$p8CIdfF$f}M!y zp-s@Y!l3NMct&)I>cqm7DKd6!N-H#=MOKE3D6*SHM7+!i~=mA!IX7oJiC<1}4(mMJk8dpQdpGt$V|G+sw3McO5b z+cCJ52qKX0{dmrp0pYUFL@zSXnP|B{=kfRT1L=PB(G1`?;x&<(K16xo?AA$R3 zFi&=~_mu2r&z3+&TeltT1DKX1%Wk%v=v;@JBU@YYz&R}8gI)SX!*92gZv9qwWGz!K zsK0D>QYT4|t?dK4+1nQ_xdw}p%W9$G)lr~8Gan||HK6ka$_99g&9?c%bTr0eM9d#HTOQA&F&C30)Z1At_JQ>FGbP4_9+>-j3HkP;(RrVE* zvJyyh@_a8s;|bjXh&S)qV@<3b0+5QV{pbu?;}C*S@(jraeh{Rx$3S1<7SAqdnZkWB zh2F!J1StF=5}@h%%vC!moVt@J`wvTc>Z@#T&Sp`pczd`|hxm?fSB)dtgLO+9YByPK zO}C&96_d_}FvS@eT$GD$YC`3Zwn7dhl2sx4Lp=Y0mUz@ahi}jkOCY*_9QY78j$Qyco%fB1n~Ha-Vh!sE6t*-K^Vz{{cCFL=8A} z(dUa7M7xL;4h1-2xg&O%0@q9*0cNw51w(1W;OHw;C86wY%;8p&4;PVowROi@Ebaj8 z)Xjo&kx-0T_aP<&cx&KKE0D|AVobS`Z<0`YP{-MQ22sV?TkSkF)ta6hzpiCNr5)_K z&0olLqhJ>aAwdgCHh`5hy2zg%o7iRVk#^dDxcoZ{{3N&ZWTVK6fKfk0 zHIW70n5J*wY)W>vf%)kK&p~e=!AOkAwjYo$H!rq_=z`xn9$rmU z+rTD7oY`f`*yw1&0w-CHF{G6I4P_r%+K+BpB~p&{DaTa!74To~ohg|Q1n5yAXwcoA zgB=-3-hMe&l?vYkP%6B_Ag97Nqt{*~LbBq$A4V@Cb^0aW6D%$cS<)W2fMHh+#q1>S z+P`+laE>$@Xj8l<=0q}v;m!(Bqb8$qpmV{pcEbwBiCgTdUb%XrV#fy#I{O@Sp8p;Q z;@O>F;rvC(hM~*Sz|mabXfB`u3kd0UV-LIMtX z;%vXckZr3rSnGyk+Fw}jB2Y|sTjSi8!pd!NNOx{aUKgH-xD&ZEN4>yD@isb=)x&0u z6!h2o)BqmrlZnydT3h)6y-#uoi>U%5H}*DQ)NYx(@&z!y7WVZV<~?;9S|~HUu~{6T z%wH!MWz(-g;prg~9|0yAoHZc79gprE{-c1q-p?o^T}%D#v9bKxeze@eT$m#)S82)F zVCidt_)%+;0d}hHguE`V(bnK0nWtmj1aOAn9~l(O2p>+*gpBepc#&kl`tW;Y8>=() z)j|Fq@R{WJ?=9YHM{!eLm`dVfouljau|g#3 zXuEt{t{pNLD0A1(0skP#=f7c%Ljr_zgHr9kS{j(T-kcY6^9wyMjQhOjPdCH$_Oz^U zfr^XI8bBuh4(t;y>2%;2M3IK0RHT%daKlYp}n z%>gp^C4=(s2WNxZX#6mZL1%N<`rUHqXE7QSwGo{^v!-HKLgp6)_R6~wL=t|lp$iYbs&aQL+>!IqT;ReIIl1`n5<~yV zVMvlchK5{F57)xn^V{}S4C?7`*rt)RoT#~MF)Wz@;R zbN)0M&Z0PuN>D$Lx+ay>4@@@+n7wF@57KHnkU~(bonVjo)4@+&P=xwbAR}7W$}hoQ zYMt3Ap23xBCyOh?N}AnE(fkZCQy9&^<+r)lqeNhax9bx_(mOt-{DFQ}(2jy6AiiPA*&N2*~Yz5pcO>FEOBYX^Elj z90q+xOtBZl-(Y`Au7zqLH0$+sYiBFJGty^u6{xBXYU70qAbv3y1& zzRnScdu%*qfuwr(Rw_gc*-+N&HBMFPpr!@O2esld4~nfi)Q`6&CWhA>^TGZKh?aib z8h5b23!o16e`An4*#9khaUa#%?fxh;htcvY__cew1Ha|pxRe_U^<%8Ff&~i zSPI-wv0QGJ%tvQKAk|R5rpvl+Y63$|8;rl@IviHOo>b)lGP0j8V@>IX9SxILySp2~b{hw*iM z+L!GxI=v?H8@lIG^hVyK`xm=V!~5!>Zn}oP+WHoj(=#9(?iSQSNrXyH$rMoWN2}qJ zz%=(}QaOjRudmXv<{IT@=g@k=Wc^Hb-GxxzyL<6_B)=lJXl>Pr5}MG=wI?v>(NS;NI~n>j2kt5 zH|1^_ytY-|cx!V>RXdSMN=W*?G(_L3;cT@JoE)x8!NJU>Nx|0j69Ti}HIRs+fs3*F z@z&4@5(*veQtBsSn6v#WfO~)({;I>jW9wXvzk^yd$6|}buVDuiF!9FD^oT~89*{DI zkKW#{I*04y3PzDIZ$EcC*{>W|D*ZgDE5UvNpnCt&p!_uqFkN@MQML;UH4Rzcjf+b% zhoYgrc7a!RhlNys0}PEPQ8~aE=cN&8Meu0-Dx~0`CHw{(-%`}Iv*l@Ot?^1*1cnKvA7*m2kvRuSrY1}SCC$I{BpJ8yk)0JA9 zv^vYC{a7oz8;CGbLb7?C&z#tmXy|LyvQQSLmqlt5zaW#HZbss_xpTH)$ffnoSigK* zvIuFz6h3TX#S7ZF2#CBXaPfRlaR_=Yniv81bw4zuHyZM+MT?m__haN)mGXe_!i2MU z@mR;zMH0O^8GH2!mz=A+HcKC&rWO@f zI?)#)JoHx)(IL{U1V(r;kB!*9sB{PiueTx|IkO);pKncUB8))qooT%en=%s17gwpjo#(V^O?p77lh=jJ_f4g&Z~OS>rT8< z6{FeWo15XK(_^zzf-~M-b-hF)VZZ1WO%Z|D`jz9&6=35T`>*~sG=GZ6kUe~+dc?Zp zk5ueWTY#C|?js5a>0Q^1LFscC)qw&=&>NAxz8v2Fu7TXI zNe79EN4?JzdSGNmn#qA-zbl0Q0ZRSDXxmRU2 zYPlVv1oZm*yPw_kpiBD&lwnMEvkl;~`P0}~jt=cTG&TY>hZtD{hT!b_#|^08jRp1j z5saDawQo%9>#f!e%$J7gHKHXq8jhP8jhx27z!hgG!Iwbm%V0`>Q^#>$R@YvFA+9xR zK>Z#xpYq>>!>POf#MK+s{yYaJH}A$jZU&W8PvRNLy0tqArv?0dej6k1GqvELoNB)} zP(4ak`}%EO{qH#&&}Y#+j^==$M~B*pK9t_|uNLo5>yLqD{lOT61hWTTuTELNAqI0& z4Qv7;i;E_4`1XDVTC77?$v*0W7UQHvBL!tBCoN2=fAd&L>^E$d9QCKLVEy*U4kU!; z+kwrEc>Yca=_z!g$)8>YaGy2Kk0^z=N&TCpXU_aK<~&tW7b6M&xRHeG9||nE7*ec} z{s0i2?Ax@JY8!MO@FU`|#9V1-J3^2xY}JTHU~}=Eo&Epyu_h5xh)!06{WcTJ5= z@QdDK`?xhf*QVziAW-`6Af+SNGXNDczHd;2!Gak-Ki6+-;0*YWhC)9@($9AAuW_^` zsWV>ye9z`~7XV^=@pEb;wJEkbCeB;qIHl`~(;r%A!+z0p0;9#JsaVKeY;~U$8;#<2 z`Z+_0j?G?!M?5w+c#T$ZYzDPo@z~sW5vKTqrV1wh>5fkQmE+PU)xk1RhI<~Aq>i5$ z)JW|c8hcTR-lVa_BLBj}XC-w;QM~2szS+yyBR(BPvB)7al5mgGzhJT-|GX-Wh)?iM9td*(R0K;ZuZM68&=hXKC=S=LA@C{?*RiL3z z!>tb_`=KDT3^h>@;Wx@+iCZD?1qteV1IHD^G*{!*xnZVX)5S55G$0~DqTn1#{jwRb zlJrNd9p!#O)+li!7w7##R(5Diy8ROM5kzRiy_ zTQy#3&kI-#Za0T@q(xAcoX~f=nejL>WQjaChQ8_KX|alkuCb!aD6G-AtlwHGxtpe5 zH-K>C@`y!0N3L7u(}uZDWjO&iVyzmjy5Of zkfmr}P~Fv{gC!cav4abtiPAdBUD1o)MULy0djT$%=(zq1fFT;_xXwwz>dv!*=_|*Z zpwxsWcxG?Vir3?jiqUY9CVy<*RcVsH!LsP}GShbB6p+#hlX)sbGFP6;(5(U^Vd6Li z&!;NLW6iE)S}^l})?LMnI}x45c?;erimyXF+#(aw7ZJh zJ%`#oIcV3GJ(_kuO-|7;V6c41u%l#%#>WVvIXY(pUh!D?SQSqWq07jbbN6WIF!o{EisqfdIxWXl6FHN6x|jqs0FMd2SSD literal 16323 zcmb7L4{V*+RloOsuYFFOrjA7x!Y2Nui_^d&k~9rVi@dhDcGKWE&YJYkChNt1ZeC_T zJATh=npUVPY$|=Cn@R*L3|68JNZd{;47Q>%Kp<0u5&;uyr%ghF3Qu@j1E_T;jfwO7 zo%`K;-{t##nW#Hf>Co zt8hDu)|TBQd!?H)R{{F_vFucJyjlCW=SvYC&}6bcQy**0&vn26LK%$%iOE{M)_hb( z@(s#vsMf%=>Fz_Dp^^Os2SArQqksrepJ{Th>S+!cyA8W@K^YJ^a>9&oOsVDs9jMo% zQGNmSicl&$dVc0TfXZd}2>uTSh7{T?$U%Fe&gR?vwu;9;(x2t?~)dou=l339F{ zC}UVOp(fuB9CM(Y?LyrGA*bM3!EK9|1p5J3+;Oe5;t{Oa?WKXQeaam`?xQ0<~q^RZY*a)*povQb!6}Q z7^Qw_p&`=IsW?MwThUi(7<wC!x{Yd5R!BphGe9!bOMhv92HZgf)x-vCYZ8XJtiCY16Fi+x#62n$7V~&#@ z$)6%fyYVoTI7vAVED^1)j&q!4scb}15nV&@uF+L#|77X#Ee*+Sc*f{53m)qew{x&f6h30AkCtEy%F zB+$6_Tu>CK>)v4tk|3wg5&0OFwYuH#SX~Z6bU68$e3Ox}PTO?5p|QrvnMd*^o-r){ zEi_Rda!6tT-e=73qv5vYb{^$W5iL|OZCYLKL=L2p+0qO}_Iw(<06a|?j8H02eV@BL zgn3oyM-+5J)zg{*UKAOsr}y{+GKqaXND5+*==q(A;l;g9fo3Y~IduOR&3R?^KES4* z>iJWEy=cnaPLw(($BmxOx;dkxuq{L6<@ZyC@555_3YwSEl)KSBkdUDG8d`nPM>;VY z<4>)TCkfOHF3A#fp!(Tp8#4JpY|PCT$k}1FDLuSZcB4r;RV?5yQs2AVM8^1eGzWH~ z{UVy^I@G34W8zEP>j=Ogd*&u9Q;jOiIf=&kIpKjU#)M6C9N;3g$xj0IDhysIwd}kU zr89MA!{Ca*9FRk8cXHe=N`Fs`*&Np=YOJ`Jk5T$fR55+!HG*=e8}mBBX@K7>d(VHm z+lhD~7u|%(>(KbDTTBO-BAIit@Ilqwpd>idtx0w}O82A57qR3Y(DcZXqq^i!*s<)6 zXt6RR#+nsdu`CWeFLe)%0zfI+D;fABwM$3&QfZs+Vu0J#@K}W(}MUq^% zD*lRCpu>2igRl{@!)Nkjg!vva!bpFcd#&q4h2cd4{nr$dooG<6q|r=+uG86|SYR)Y zT?)LUVq<)nJG>F}XAPO}?yxcA#GIp(yuh_+dZp-;^DmrBR6~+fIuJ6;SV-QM=}r65 zR|{?EgwI$dKCQqtVt^wRzv%i-i^;P}+!2%h+^@$ijzVJ(qK$6e zdw8~j5i@9WXlsDp6QIKZ8nv<3n?kA0jIW2Mo(7)=IXN}GvKY@>G4@(sU%$pNxx1(t zq(1VuKiXmexDP1`Wu|7erK*@evAUjU* zcL1L1!yE-sg+7bE*O@@}{-SP{sg*=Gj1Uzh=v)9;4g{J^EILoO*}d8noLwMc4U=S3 zn91syh|8g!09CD8aX{I#XdWZwEdU=y^SCq~iGzxSnP1N1?l+~E*(CDBdV1`4GGDNb z6f+x)3R>}W&2q)zlTkzjgXgL zkP#?35BE>SL?`O5&s8UOusi7xP-2} zBYLw5;IELPTsKn3tmxL&1=L;H(hZw*rOUv8R9>J^>I&Qb*6DLm65|yUnP=LB1U}k$ ze^Jx_8OTb`(j5HdJ|Mk_hUpUg+i_{u=D#uRJ&#;7OE*;*to=f_8=0130wiE8y9Hb^ z)mQ|B>Fq}QfQ`&9N#AbSkzxD=G)6}N(bP0Lq$$|6acY&aqor){BKf5ct(!WNmJeHO{ope(mv z&pqnv-L8J4F1SYVLg~M2Bz#7Jf@(W~WA{j% z!dwA7J^n??y2zt$9#2I3AHcsmTEs4~;{0nYgc*pyxF{CO(IC9HPtVk6#FslB=4qg7 z!V4Bt?OdcK{t26E%>T238uQNeffK}hWWr_Ww&kq+-HS;pk9lCVNBfbYSBSP|=F+P? zZR;f>oG3|8fQPZKqX&E*c7$3Q*paMdKY(n2Mj<9ZWkF|CMYp; zq>;Z=#-Q1f)j$@nYaMlQ1N8RL>=Ws1CK~&y%^!M56v7m>e=_ zgN%$&Of+7r?wg@i@} z#)3|90;D>v=lV>q!cl)@VS(-UL8oI0;Z9?!48JpfD-VN((!ib8;~eJnbq$Zdcn+vx z@nN&mm7s!U&QV+8aP;|{oc%8l)UrQRa4pNK(*x%vH2)v_ssYJFNK%@Gmve(YQ7|Y2 z!}PaDqOMsY_~kBz0miyHKi095*}I^uA#_w_I-^Rl%f^1 zPa0rQKk%V~)^E=4+2F>4>qfzt9apKN&(P}%Qu{zpq>lI;WFjD><;mATJAb>e*GnfA zwXKp%-f$vOlpuzVYi|J9*>TTf3cEU-^ytKj)}2?kMa1~BSKZcMZ0!aaZok&Do)H^N z)Ef9uG|iRr5aKE0VIgwJgtvgc>jEM?(pz8?`gCYZto#n+7W#nnBBrTjFyz?1CRdjH zq{e0o3id1TPPY-w6TuPO6M-!S`H14ZU4EKURmt2F(KG1#PJcoX;v@B1Z1z`zU$5$E z8Y0<~m4kRyc_nMib#$+Qtkq8iF8Dk*jHPdSkSt++z6cw=y1rQ9H?WjX2{ zA)qzE6&bY$iL5``2y|G0^4N1sz`aRX!V|RzO4OHB^=>&L!pF2ghUwa_r(XZY*=8c`ZWq*}3UB&mn1Ad57sZ;In$T)TLm>ka$!eWRrTr%@0cY^|0$sJjvG9vD zuOV@~dyS(UV(GJJ-~^6uS$3y@K5_hvg8n4@VF+`dXSfC^k~s8YU|!N_p)Er3WDn}) zpUMn3(1=49eKY@@GYg8s0UG+eq}4O%_%|hzg=^ZcV6Y7TNe($)l(>#*53J1rPtO?l zdBB`jAI=l;%`%*7F~8!=rJD8P8mSno7LbzxJQhXL9mwS^nA1eOPeCLU`R5jdw>^X& zlk3i0wJ|gG@v2O#_I9qOWWOL__R|E3)l2Y07~K|*Lg>UNU?wHKlaV0L z*Z$;;OOH0tGQB|+{(+Qk*oJvUb2^+}?i@oW9d`C%vLv;BM@wGhQu z;2<9DZ+dfS2V}UDv};Hz*x9W?K++`JhXJZwBLG#dBLaE3Mlsq_wyRfwM&c@-YVsC@W?Wcjx{%#M<}M%Q)>tSOGh z7RZD=tE)}c7Qb?b@QySQX;Zv17AG>sX@2n0t&@46Gb%KVg|6(M?;xqmgVk6GZieT=4{wbnJr`OG8)w| zWsgUB6C~h}C$0_wc2tHt1z7dWHN_Y98wEvsN*eFB9|Ndvi^m}Ewye%qUw9aajLeB3 z@Vj^$9ZBk8aTg2v`@_+IjpZeAGJmz!^8ur;a|)Yj1xC%iE~xT|+;(07L!a@vcnRyi zfwGYrw~v(b3zYclG_$O|1clr0kvMA!GPo#%**Prq-{HRsxb5?cW~3VR2U1zB4=v5a zjXA?|m6lwLmaYMjpWOO6sP!^f_U9UjfCsZo$KvCEiy+-Tkr6&@_r}uraja4$0}{Wd zobeKxJp(=s%FXO-u-d!0Dc?g?;%i-_ujw)FWL=&kh1p;eB*kVGyvY?O zCg+xPeQg({w7A(C`K{LE?lx~>K+{{6q<(D9RqE87zcOJWdmbzKVIlhxKwSbeWG{#Q zC3OD;>$_pzVy_iBVWCS^nkdxw;$3>6^#^Fkg|zT!Opk^=cr}X!aMJX=ft)b2(kBr`yh;SEygGBv0o!p~n1g3^4-Ey-Z|J zuRdglQ_llwi7t8UJ7#BB)1ilN#U`k+ z1Cad7z6Na3Li5u&cCX=)?H1~)&FV<#90xv8O`HXK5 z!u95>Qn*0H`A-u-Ci^Dr6R#(F;ol{`IzCf>cy14HM0KHI9-zw!(;9PSygK5lSw; zUts8eI1T#Qt7yoj@=wYC74xu`>WGTu*EQ;uucfN;x2SD6HU`DGRQD7Aswxq3dsoqHOWS$ zeUyAq221j_au~Cvee#5NsA=@Rko-_Y9a`Twt_LO~*lmUdV+!RtqMv&CmD%@!&X2a{ zGPh)D2iEn>=;6HTS<+cV;imhccYPa*Q6)c=M)KXO*cq?IZ-Y#dY~Pj|MxKZYpQ^E~ z+pbUlKfnrBqYiQy)nUk}GE(9fR6QQ`w{wVR`2;R4#a4GZ1k`&&4EjMJ`N$B+ppH@R zz8BEd(1WY#L54u0cO}b*gWLMuLIjurkUuQV8X0p_WNfss)8Atif7OsNQRzcx@>;A{ zKon=CQQ#sclTeYIW7ATrPss9)rg;FOXvRSLcKWvx&tU5o znqQa36z^!n&z{HBN|!YD69Bc|{UjBl49TEd7c@>)YQ3u)YQ2l4G+VgT*JPyArGBb9 zJ&nJ1?eumjOOkgp^d16H{S~A>NByq!<&427Zl3;L|2d4}IjVZv|FvWWn`IC2r|I@6 vrdK_x=^Xf6J(oX8@)yeaZ%6HI0U8L