From c1fbb6fd4c98751f685a244905b4684f71399c9a Mon Sep 17 00:00:00 2001 From: matitaweb Date: Tue, 6 Mar 2012 13:44:53 +0000 Subject: [PATCH 1/1] chapter 9 --- weblib/tutorial/acUbc.gif | Bin 26666 -> 8453 bytes weblib/tutorial/chapter9.ma | 26 +++++++++++++++++++++----- 2 files changed, 21 insertions(+), 5 deletions(-) diff --git a/weblib/tutorial/acUbc.gif b/weblib/tutorial/acUbc.gif index 5812fc8f462a99d6f138ae01d7758fca10b2bd8f..9222a3418585ed44c08c9d813cd7f6b8603d1d41 100644 GIT binary patch delta 7674 zcmWldc|6mP<)5szM#R=uOWI7x&4`0?r0@woE^$S}sm`J=EFy{x`YjVdJ2iZ68O{`UPg* zm+AG-^5XiPzP<>#EFA5tdHwKK=HSjNP-1GVT!GOKP}5Dl4oA!s%yhZ_Gks~~+)}O^ zogz^UoDS;MEc`THce|@gbYZm7dV5?zUEH$n<{k{}4#0sd$K}7>5hrG~%7@(nt09vI zE7ys2;|EX}Mq%?8KddJ5Qs>h8Fd)Z)uu4ciriFk%WcVCEq-v$P-A; z`g6?En4!@+6j51};1mYSyqqr_SSD6s>#A(5@+;YLk0n#p@!mj4;qv$Ax;k4g7$*E3 zK8UgW1${U#&u`5GPisB|Qjp&JAL@@wTXV5THfNXVz!5ng8;h!IVN45fs!RtL;s5FK zLR!7M0f}9&!MmKG`TzbDWSf=c_+IoV*Wl@HrR%% z&&?&Qjr)CZ;AEB}FYAqQf*)|I;_?!|T3B-bCZXK32c7Ck`Qo)HLiw(nc%=pi_=Ou+ zue5YAQFu1P-1{n$4qOTzUhzxjOiHkDxKj^n4hvtQcL^4I3uAkUOS8D{n3qhoM9a8~ z>q$>Sd+>{g8jtC%b`Xz?=5AJ@3ex6&mIp5tr=ImPyUAal=rzr0EnXBN<3Gnnif9wz z!5YQ#>qi(O$H?~)lb9n>>GOO1``ICRAWq~!3=ip0v^UGL4m@?v=171AMmuu6%+dn} zFjgBj#(H$`j!7;8$0~G(D4>gUYv`AV7Gr}~-tGD1qUGX90$3^zD`S8wKu&mLo?K!U z;sx^Fr+MoDOJfe0<$=}mzaBBcDe4pAR^`t6mB`eSC#(F~e8T2bSTwNyvkQ7<*6FC? zQ1~C8z^YaLLiDEK4a#x-OQ*#oGdwY3wp&;Os|g`33>oF;|0Ybu;Tz;^=5mmpJ<3=q zk2xzw%8dIdwK(aMxskb$TCg z!H!@O3iPNu?gH4)1Z+shNrxX3Hq62ZqN|Qpb@n~0g&KSx>FhiaLr*z$;-@!I^+cCl zTwvfSA)vjI-a(eMIK~0sjS33RvBW08KYI}>dy-f1b+TaHM{htW@ES-m1Ev8YbJLV; z=W`QlVMU=9BdsKM;I37E)gsRhe(eRmG-pTP5N*b{(p=VTGN$l?f{ykVCftp~JK#VO z6?S4v%1Ab5Azf79w)y9P1w3Tn*T33b7me?Zu)_RA6a-M4@1M zq~8ySF@{-4mAPlId+9|Ec=$ryVMe1!kF+|CeT5-i{Rremj<#@M4gy}9x?I5clMMp* zFrVY|b4&g_a_4A2uJNSo))@@0X91BcGKzyP@!wVtmmGc-*K$T1v?y86|4P?4Nf(l-Fvz81>?g%ophm z@T^vUZ1mbY98yr#Q>8$Z@s`P~oDb>j-M*h#kbLy+uVp158}^}k6xI&Dtw*z~!w%L+ zPoB!hROb|hR83ZtnX90N?Y_4NG_8w-zmD+kUHU9$&F9^8GXXM6b3JT-`gBtgu4<*` zg<18$SJ{$+==MS9HW!^HNdgmBmAks7{BptU5jHLB^`b-mqbLbB0%u1YJ@H{yc)0ES zV#E+?9n_ye~re|UkaN5L-9E_^Wpa5fm*lj=QfKT={0 z#F^~-#}A>=0PX1#Udzi-D6p%UJ{IBy^(*jE<8kGg<816D7P7(66k5lz078>IfR!3- z_Q8=%*ui`8iCg2Zoo?_k!(TE=2>xYxL1u0y-l+*8VDH`&)>9EngJ$Boy7>uAL^brf)SMp@@M%S>)Grvq|ASNBU%3j=c8rqHLwNJXlDldt!wz0$8XTqfX$|yqaw$OvIf;tdS0XoReXJ6a z4vBhTM9AwT@dvI5BkpRadVBiqPR!XZSBTBaj|Z7(zus(T>GnYp_6fLBtf(cxSy8RG zRZ~|(!|v0D^J(5A+j8tZ7?eM-^6BCDL*H(iRWEC4fsBg5EADCeOOtTM6vW$oL60h# zE>Dd=ZIsa*@W;l}BBjlpfz5o9l5}jlid>bP74{m0>7n9Cv)lpv?d!XO zE$o^09@Yh`@*bjYpHJIQ(C2-nK_O8jV%?Mh`|NsGW4Gh`;$N8dR^26*7-IcCYruHc zz+yzry>H(Gnr$g$F!Lcx>rxxH zINmArq@H?vCb`73%5$RgH}~^63|ed0@8#=2;%liIF*rv?hv)N!)Li|DF1s-{U@_1P z7*82lMmB-G#FpGsC#(!E4BVwI;WO}EVm3YwfGv~U_a`UZ{eH)X)Wani`x)Y(9s$)RGozsl7#urqO@`wsEouOPQna<-iTKz8D3XYN_U1)1p;tucN@54B8(u zEq^8L2?tz8#Vp@qFeArD2*L4TY>hAuUt=(&G`J!l)GNikBGRZtAjZ#8`ZS0?pJgS- zU3^S^Snq%8J+*?LhM5C?*P@OAFiyhXR)YfpcjFo|Rh=F^5d?GemP(;??%rfcfx|Fp z-^aYk!4bJYh>Y;aQu`U7z;R)N3UI-hgH2N+7dWI*nc-Vy!0qpaeM-VnuGU61#+c90 zcHsKCC4*q&Z0GXK;E)u(ZM-#h6Et0wHkfUM{=#GIKW4Ntc|BV5#mDu zkko-Q^+AW!Sda@HQwEUBVd{G6BC$IWCp@&M2CoZ%hc$-4ZQO+p~c_qrkiUgdNOvK8pePwHE#JEFo8fwc;~$ zWQD0pq=7?v#i6t(pg%%3_v>}^Luq7eX=FGKIJ zv7{vYtS|k71OsZyF%y&~C)haxeWC#HKlGl6kQI`0>Ks{LS-_bim+7E5$+E}Ns= zV2g1C&7nqa$%^KD>kqWg8oUpmWi7`wDtYD;L@5fBC!vGFqp%cj#Xjal-CS%!!0};u zI$3}Mai}z;h7y2q?Pv-*8=y4OiR%rvZj!A#J;DUXZ1cvdE7U3BtNUq~+ z-PnC{n}YDbg`RAE5=uSBN)?kfE1e={32TQ*i#!B>6$E2(^his_6E(O>_MaJvEDfj( z)9aOE2A8AVv%oqO&Yn$RnH;u~x%x^ew>kK&GE9Msqd5llL$PuE^O2gB{wE<~)*=fL zoB*3@q<9K} za~yPX%RWPaOsi;dgf03R1qQ6B6#!_!KNaRqzH5WKYD0gVr0d4P;773tT2VR-J+RUq z76M`k)s6dK>hbFX9>g@MEAej z`aFlYQ*LCWIhJ6JZkGcOiWuv}3NXq~M_!<3$Hrq~p~o4_tFk~S6>}{C#dhvR=eALf z?|2STsw7%aD%MePBBvQaWDT5&Ea5N(ctWHrnX4rTG(lu?QP<8|bS_1ev2?q9ZG{S< zDXv&j7YK^yxw3Z?FR+puIr{Qb%?cWeYlNBvb-g?d3X z0Q`v=JbH;D5K-zckMuy-Pcc6!c5zY@-K2Qp26Vw+XH0|n=c9=;H}#^EKkU?L$Ud^ zAvpm`rOfo9TQ#jNb6&AiXaT#9Sl&SZiFn&q$ea?HOWhPo6YfjAN4$zGaNQ-KlpXPh5q{>s!gU1CV0WNJXef}SG z*FN~!KRz$^q0Q*Zl)o3R0J^lBd$gO=(BVrU8xxiTbTFvx1vHn_U0V8`Vu%X6Ib1J$ zLhS%R#C62AL<>J6UZ1s}}} zb=-f~m33>LOS*i@0}Kwjvrcx0`qT;fvJ*SV`MqqkZUQz|oZ`i5vRygHkLuZ=vQ3EW-u~?v*-;aG*n@ ziDSs;ERY>oRofd86z!&?ss&Zjo2`NR4(eH+#|pU$ABc!|-yCHR5b(mpXNA=5&APh7&RP<}(rk4SP8tl#L zmt|A@`owtEL&1hsRGXoZ>bGkBh189hiI@BS=abcaYfqQ@@%Y$ScTnK)xbXxzd$pM6 zG3&YS78=5R0Xu*^-7==pCi4DGU9Mqx6~xPbJT$%OYv~X}8rDW$#p&WRs^u8)@w_lr zi#oLDGtX!Rcf2J>ZTxT|M9Oumx_WwiIVT52aZd0um`C;quuZ#epk<0QC5dt3L@kZyJS9~N5 zb!P&$`)@}*&};vGtIbbUVq#xd6rhe7R0kmV$QsmPLzULtG)4+C?WygRe>#fO7Q|oeZK(Jyt7QD>^ex(pV76Sxr3Q|wM9ibCZ|T|PK$LMx~EM=%!veE z%?GR45A2%q7%JIz%>*KC*)ri^AO(EBUMHF;-}DU81Y12!K3Ucv>vqx_jCHRo3%+9v zVD1v{JnFKN#qVWVwXviqHSOXn6Hjy0MOJqvmYi_ncjj<>>pzPhqHrxpezTv}nyL3e z2u#fr_O&qsL|TxzhV<|K-|drbbM{+2WkWS{gz87Plcmtr7BFoe^Q={%w_@boYxSGQ zo9tIHy*c$u1kaMoiN98E1l3oMf|O2Mw4V#~gi>_6w+8c`OdrJ*DVWvvkIe;9sqWY# z-9%7xvzWR-CJ3+1D=0+a>LEYCZxz+<*}x~$RaFldu43iH(z!o&OCe+D85lr{hL{U{fIkqIo7Xi+7=l~SDX>{H1wj>hd+Ea*I#iX+Jr{wc;Z2kCu8 z#by@P+C?bv51#r;26DN7X$hthcf3^6a2L6jQO}p-91tA(yLf`)riA{Drftw1IS7&v zIlS#J0%aCDj@27gz?05szZ_hy{7!Mu!p*9PiU$EK{E1wrgWVFW`%WSLU+hwnIUj64Lha=O$!boNtu|4n#+vNhrs;`}B_I-v z|5BYQW5%Z`aKQ|{#_k1TYb#dgV9Cb3D*l8=0cn>7em3WryC*JzwVW}u*|QAy2K)(J zed~MFV%7OS9Y2!FDBvbs$Lu6lW-jO*AEjXtnZAud7mq(#Xv7x}1sZ#u`YLC@_Ym(C z5uFb#eNz#A&wp76z<%9w&}-lVGomH&LGhn7HeqS*C)#m@Ut8|m8u2XE0Q$4+S%nvk*QckrcA>7!2 zrra0fj4BSY*=HBdA1HrMEc;VG{MI&LerHzyu99S!Gq?5cUwL1476~MP4Zr-z+GBcn zp*(llgXE(+(0~U6b8VRwN+3mep3WWG7TZ&R&T@F-{*Y`_0NXcUQ4?=&l3UP&2q%zb zxQ|nnNqx+%CafzHi4`8BqRIRoh#z~{Yrp$IwV)D_fGcwRF6G3J^5v&m-f;jw?TPyd z*!I2Da`Q~5xq1BNp49`@hW^%D-BMmxu_b11Cl|;;x%=JUN`XpEnMw3JMXMZuEWX;M zi0Q8974-4Kd$t8nYYM8OlWgkg{!1+C>5(E6OM~48E$@ykwwK!<4tffv9I>COv5M$Y>NPS4*vHA9nn7qOaN%V$eeX7*uk8S zNuRE?&n#$$OAQI0LYUoFg`tHOnurSwlKYsYY}Uo10!Fm2dvB?=XjUTmTr7{LZ%uxH z<7E$-fNNSb;Qh$QS39M^nzTQhY?96(O7fEeox4DsttC?B(<4*GU;gr>}@H@e}%Pljj`Qw9^vK6qg@bWI9(>gUV&=PC{Qa?S|Jk*l5SxF$ z=P@IPFG;M6BmFSk(;^;~))dqpPkWzF8EEdF&4Bn@-8@SWx9sUvA@N{}&=KGVCnPmi z0FR=Ln^v*_hi7NmPth5$q{nCN|9T(fyhqSByks(Gi;3pv*ZYxm(n-HhKi-xr z*B;WFajw}3vklq=p8FPX9m?sGwV2BR1Zv$qI3O!m2UJSLb|k2Cxr5AJs04kkx=U{y zPvG}jmuUTLEyB7q*`MKX)uAq)qmI8Fj2OnUcp4fuL`qs={{SPekg2jBndctur^=9C z4Lj$*7;qL^(aWCXdf>T%V zk_zGdCi^*S-@LmJ;^Dh~pf>!XrY^n`EHof}w5XqlFNL@U)NLL%e`MVwNHRGOiT9BSh9TZ0a$w>{v*#Az`<Pq13T&L>J;EYS?F_uGwU$Ej9zWPtQP`Q;yn;gha;u?c$w&xjDVQmFq*3YVUJ@Em* z=lV#EHu>CQon<9%<#~D@)?@}UNZn`4GjuMLl5bv=73kHmHUp61)CE~`rTD)!-iNii zk+S7^zJ`Lx}sH0iGO`@scSrd|T! z+=>BQ6~}+$!Q<>H1Q6%aX<>~xdBuelh-b`4n%4m4+TO(o-Bc-aR7j4@bAcr*Tb|{1 z^wK^cN;JXtNahe5aQGnGoVe=cYx_CY)msERhNo=%uO9P`*(p==uj@F>UUIN?VWg{V zSi$oVi%736wuc6OI$gJ77I4J|V_t(xn>HMc%$jH5)_)1lT}kUpORqVbel1|(vdj&r zGI#s1tHANULpfT*ZjOqu44kJRDK;u>s?_RV#dzQ2(FW|8WZ&}Hbqm@$aPPc2C*SA% zTk`kk{T6dvF)*YqU9IS`XZ)CQgzF>2VIl3GeP;p+QiYAnGEE+>@m)E7x|XfoIe>Ln z7C(&3S#)A-C`RfF6hu`TuwjMBs05H3^>gcctPhxCO%y0YF-nJy9rK4N z(K|KelaYKob|Qkxa?L#cZer3^oKofeKN%_Mq+GoiGD58&kniWiOtX(x9;Q( z$1KlUQ04PaeJi8kh9@`r95=eW3QTTvdUgkw5dzIVxY=X+SmmA3qVFNayx2oJ$j@l2 zua>#+YOdmvzO}Wl*|8gD8#mNM*bfpjo90w#2arB#N~I=TU6r78J~Q+P_T97gevo^ zt+u{a_N@md1;7fEmxG>IgpLl$Zj8TDJ$DDr$j<-PeV1m7D4EtD)6U-d$1qz6KuSJQ zR`03ffdC}S$GaO2t-j(Wxv#fUH8a85grRzIBwz>Ua6{&+-{)QWObYo7j9No1Rbw61 zK}XX#@wx|P5Pnk{xLB0)DW-ql>*--~oFa#|7tN(6OoD`8y%xA6iPq}b90MLm&eOn) OtH8wWw=3Ads{aF@q&#E* delta 26031 zcmWifX7?)byQn9S5M@qBCF z(fD0HOMY&Ap;_4Xl5;TeLfgQ}%yaoK?p!$e`x#o3*+Ok@JZ@gAZCi5p;;BC_iC*0~ zm}Hyl0)#X?FQ0$+xOMKyrT6WR9RO0Pht4f;zwq&o&cY8b?=SXO0voqcoKvrLj=$=SJM`fs z>+;vP`lCsQe~DPMEVTdJnm-?0zq+NR|L3IBkJMkU{rEcicmx0U1(GoN+y1+U=lu5T zzrz7PpM;Y?JpA`R0AU$$x%Z>J;8C%)b(QHTI%<%iv8XJj>jqDP{dcUsEn7{h=TxR;yx3tOIuwl{$KK~X9|9$;c`3rrW(w0;8q6^In z3rq^Ju=u?usErQYG`CWj@odWP)&2Fcf5Eat;n$KkA{G$I2wH8aI!ldwwmXQ*+8Q;! z7@$q)V?A}M_5c3!&FXE6pOoM6E0NnNsbJSeT11GY*%iS?10Q5ctWC3bZ0!FmL8Ht< zk_$*~8S3fID##^|W)7_&*vQq<?vddh_;I{f85M%n|ORj z?CQAba4k$0(nuRvF`+f})oHCD66OHf`gKv+&&F#)63YF*>t$;+`HJ6vMF)VEgkMy%zM=-(8? zd^S<_>+TcK3{}YX$q7Zq zquUQJt?02#>D+DlMn#z$JH|N4?jb>Xz`JC)@!zVvv(Gyy5q@GCn5@=${%KPkhwcJq z3i!e9iI2iA%WPJL^^u=rJC?ru#Axo7YLl_@W!7hog?Y@4NR=oMR7$HIR$QNol= zz|tu7>92j{(9|<| zx5>fym6_tV`R=0l91^I(?ed0t;}7wyQ`rDmDKydR|I&oH#(9=u09ggv&N%295f3WX z{?J;!!rE8H71an>T>#Y}_4|3}VNt!SCc}d`cgEdC&}G@QbmL_5w2YxgEqmOoFmkg^ z4)@uUpEfhQ<9RSy1gE$DrFoGlr>ZK;mi;6Ce);v~SY|wmPh;im`L#OMxpg}fn>Fo< zp}HoV-6aE()n>QI)47#R2pI)TPY)j7_STn?m6hEl$cx!9@Q3+ahRc~k5mHJjIj|nh zk?+0lC!sy6ju!lm>`@L&y&CO`wcRFgE8rNLIHdT;l}ce_HYI&SmTqtCxA$UzxJFg^ z@BU8aJ0olksiFAzi5p>Ml&H)!Ij~l3;c&lzx2K?t$i%1@XlLuLyVmeB^Gwbv$LbuU z=1JF>K#*RSfBfEx7RDcx77#7}6aR2MH?e_CFL=d^+~#r1AO-#Oqz$v4x%OqsAZs;ZzU=2? zmjaU4X(~Mbn_a(kHpy#Gu`IolKA`!fH^MI)8XR+d;#fhXL2M|o-{yDieC3R9C`dft zWZ(6j9DGLzn4;a1+cn=YHTcHDZ}{Y+m&zGqT7cNw_2_Br1-AGQz9OSB;<i9&)fzX49+AT1y?R?vP6vEuf!yav!TMnq!8CJo%-f`UHF5H#W_$KN3@3LY z&dY-U+ukmliAjCMQoh)CLmbido))}*>v9F0f4|-=oBhfzBb>3$+<0# zpHV8VA%s2VD^wJu!Tz&`x(7vk^tNs|(x%V5m}a&Z1wsXzbI9{sFbHNMldIw#`|n7_V-aD2*9DPmH%W=qcu72b~_HMOyZcC5eAZ$x$IfC*&ZelItrC) z6zyGae+M%T<^s$Mcif~Qk_@~e$8UqkDT%d6Jj8j%=IUXv~jZXUxu@Qnr$ddl* zeq;#r~sF3$)>$BC>y{-I$7OE}R7S7^-Y0wX?v*So0K@}LHxAmR%}v=wR= z?yoD@Wu^v?8TZx6DBeO~t6|?wnpu<*Y8JWQ18RIUrmdiPE($~d4V`wJ`>MqYnH4=8 z^8z8@&NMwcS>bjEThCQ3ZvoBzn?_XpXuP}8eD!7M3g9>y%0Wrxdbh-@TzK6O8(-KSuyl}+X)Lcl{v`FElB19nvwu>Ka! z{75Zacia6FN=7tLQ=a|rTKL&u-Ly*2_aajM!Xpp36dM89qVnj&R9g*dWuGZS3)E^3 z`abh$7J@Wjw^-j{euhT;bGJv85D3;*?;SFi3jrU&25zF~6XUWRAnkUo8Ak)CjUIZG zU@F)+(3iVVEne``BmLR74|a~%Fpvc_XLg(4eMiFf)7w>`xrV&;N=xcSY6u2Q78(xR z8Zv<~qRD%YeL^7JxaNS1c@7FhGc)l09-}Bp42uZsY#j?xKrZs^0>B`3OUpRLO9)h` z>-U;^oY#Y9m`OjE4C)zq8>!PogtGm1AGM_Xca5i>x&Nu%k)swqaxnolCTpV2Y}s(T zH}|p!vcRsL-)&;40)Yg_CKRYaElXC=--=8ZX`3A-`P)|wi`Z(8IrN!13rQ7R6{tPS=rD28Xv_+zOM%)iI2qKgR2Ya?eP~%~ z@Nt{npBNF;5~Ke(H~okS#Ry7U9j~CkaU*S11hLp>*N-ntS!|ghAZ%WYE}A+n7_vIl zAe4rb4t3aZ%&mn;XPW7hD44P1qW`d25(;bv#3vpPK?#6m*&h`9TC?jy%6w~$U`P>$7u#3k<3)PNUrUvba;s$d6f8@9TC6wfv8Acfd(vP$y>Dtg5v^ zvdv0qm#v1(`r-*U0pb}wv|M1C?MpMNz!I%PvjK24w)jOc-?C3+V5k28$#kZM>S9mF z(aBR7;HD0ItIqL?M9=G^VxMz5n$Rt^w%hw`#kDjsEvgFyOkpG7FPbsmfbLB8F6p8p zU}A=VhFAiDBJ)oG;R};`DF>K;mnITI*STil7*K*;DZJ)*%K(})P2YA9RsfbWbp$e) zn2ez!6rf-cpV-kms$4CAqr?vSE7iDqn?~XK6f?Qxk3nFnuiNIx-1&4J_&)?XS6J; z11ZhCG!2Gp$)#N@)xs@(|Ij0F^x(K%6UV-u0nCYdv^NXQ(ofoY81tRiwH=`Wh2iLO zz3t#1=$L`xlS=}zrY~ZHS;sxv2Mj3iWjxSB6yP4{@7#|O$a;N#!Hwkh8?!k*A*HlV zy{!;OcVO^uEcE!;`!+|q>y)ehYu$A^=?W3^;W;^>Xk_w)jV@repvyW7-JrK!qeAbF|7O84DW#F^v)f&1#CamdYXK2tldhCJzuHG( z2*IW8HvW!}*!Qi@v)vekYqlKIQZC7)$-Dpn>ZFJUGH$#w*BM~88kb!d2w zKFUKq%yJ@)9lS*BAeVx#$lPJiPpG&?^m29=yhz1p#DPHUIQ$EP;0Pnt(~6d$`KPRg zF|rc|q-iPLDB!$^c0q5u97k_4L%$9VK`t*}RRdRj(V>nUx4tKI@DF&X>su+hYL=5l zAE~s@1gj;4|H8N>f+j75Eis=Me`3i>)b^s8^<5P)JCxLW(+)IbiJiKrrD=DNakHmI zWEgz&1zZ2l5h8Ut;oApS-$U~sJo%V{mg#M8sL(^7oQ&D%dCE(y4^$W#?=|h5+iXZ=Wv2(H}J6f7$52 zoJW$B_kpSCDlrPU0P?55ekAsN{N)eZjW?`bqQKw(FishP5W%6&0LEwIiTUXJ#gbQ1 z<0EOaUXz>Pxq#*8OCU*dNrRz>?E%Vk^!4kfsQSq9DyC^S^X2;6hBxLu-%TiKv~RcxZo)2{Hu(YdhYnUs`sjj@>-; z8^RHr!>FnAxOv=b6QtI3XD#H~4( zSD`?L_Bk=_XWPb~aKQi~x*A?!PR9QVrJxuL-eInu4bNyX3t?|Mu~D+^J{lP9wxs%}-MINd z=H?qt1Vj(@{6IhcM-P#r#Rn0>i}BQzR{T2r3%NH zzrg$Si&5gy=tKN{>8}&__%HcYZa4Q$^8S!@FLh6A8!e&ojgxCn#2*EBiDB6Zj8wFb z4qLp*_}`!((AHp-Gg(_S2mF?PMCx`BKMDi9yh4|wO)}cmnwR-~Ul8l&PGS4nC6sqI z>!XY4!412%e|avODVa9^T9{E8TT|v}TlBXl&e*ckf7#8(gN0zCB z4u4g1@O{}YYF=}-K5wt4i>J*ME!q;8XmXK#eI9G=qR#u_;CeH!;y7;D1Eop8OXc&G zKEzqSCfsrgTN1qVn9b9Dk7KJE*stzBPt%>47PRT?p{(C$l^)VYy9jpi&sxRysLOJE(P2_j-XB} znfs(tfSlP>iHXx`u?L)OBg*X-`mH`%jzDZfS!mw7>NzPhUVl5bzDTIuox0?a@9F({ z=gcncHG~gCbF;S*71^lZhg>bwgrb=SdoEK)&BL`5nw03R#3h|{SDU!>8BJX*OIR=_Eo@k`4 zkB{?Qcb>d=>D`<9n=^UjR$}XXGF@`NFp$jTN}t!0A_U}OH4)A@Cw-Y6%xtog%qWc8 z?G^f|i&nelk>@UN8#1#zPHT60<$>m-I>7tE<;&+-$0x_?JXblfx=$Y3x%pllz^Gj# z0~(lQaSdS8yN+4e^i^vu=?~{!$Qb?iCW+V@ZQq*re()kG=`^9zabBAM2fSBGj<3D? z`Qq(^!H|*g`If*8AkHhWj0L@4jz<!(W`uvre=sQmaC*Z~j9(?Wbosvh?!5v!iE`fn}GA7Gf0<+vA*E zn?JCp-ao{MZw0np&bn6_;?tnc&xlMFCb!I-wRNX~<533S>gG@P8#p}x1sPgc@?(6~ zN*PVJ-`R6z1N5^a$Gx*F?8^-8Y*>r#laTx-8>Rt^GNv!=^NvS@&w5G5qajZ3OEF-( zv62Swq_>RUbVQkwn2Z#e*IHXIszyH1gnHmsjV8_nGYcHE3%KSOaT>!ZOUf9PTF~j( zO^meiGzYFt2A&9m*7X9=WoosqFF5u)b~5`@ii1zDYp`Ycfm3c2xEEf2n%VZF^r$Il z03Bag)da!-$$4$A=j*xVZgi&g{`%g@WBlfa+FT0|mxf_mgW~8+Qgy*Cw|lP%bMXMr zTPzT=cUR4{8Q+PzE4_jzbFS~7`UCmcbLUqM3Z+ZLKE}eTs`E|DPU>1#x7A8b z{&77(mbiEFzdBpwcBc zoqFtYG{`GfVvlH25BKTz+`LsS##~d=V)fy7y3yRVxh$TquMl9W&8mVc_T*=l@K4C7pzv!<`4jp+csl!IW=K(e8M6hob;Sz~h)Jk&wxr zcX9J~k1FNhigO7LOgOc%heP7!hwV8F-g(UonQ&#}a>Q$~8g46xd)b}plavk?Lh&rtb*%<32{u+C>c8>cf4St zrLYQ8b{~rl@t$G>`!y!jMMBC_qZhZx9`|mzz{Wh-k8>Y$ZF(zQa1ZW$xREw|S zz%mV@N;y{(BhZ3M^^!z`_nd8~N9ye*T7`b-JU|_qWxYMlYo)r@TBim4@iQ;Zavppx zXbLRGu!eOjcL07eCQim2O2(SgnFjKJWns(fY%^=QSgSqheroltt^3HUVSEY7_pa%i zE>hN;*mcSLiFKyaP=I>1KX~QMY$b)Qw)nf?cJf?;{6Ncc-z7g1Go|6=(P{F4%@vJkXK~C+vm&T#p*kBsbY0(}gCj*6p5NISt0iE{iT@pYB7v-?=meHl18D-u5W@unaZT<__#>l2~Q- z*dZ+b{bQCpPEG3qujVZXiPuZEd0so$)@sobv~@)7;^kOh%mvm9OgD{XV-ufx{SqmJ zIqie5IVOk=StE(5+V9y9oEDupzFKro+y&UF`75rBOHHXf8q(RMy{U#IN;kxIblp|` zkjzB>@92I;-1DnkvnviVx^9B#KaAq8y;7S?ospbI?%(;kQpS+gveq=wqA>x_j5_6` z&KfjxrVD8-?=l-IQxd`d-$(znI8Pyp+sh}Tp9F0c#kePDGgtAbumKQzyyTiY`w4BL zgxvk7h~|VWB_jm;U+;qsnW^ae*Xv))0`n!6DZ#@Q1t`zDOhB*_3UmMI`sMqDGo=uw zB}|{AF|{}wPOCzv1-BmxK% zP{P@&kORl}|BthVEv~a-DK-y6kN_t361LG`vVgQn1DccVHyNQ**?Wt6LCVDW|IY3E zII5T{l1EKQ-HIg?L2Z)?wI4F&iXSdfe+V8DU8rHDV}~1*bL;R|sa9_mw#%D&2g!LwOgr zCpb$)q!2RhE4pI4jmTmG#8K(uhG45?W!?mVMh0v}F!-!$W2QXYHb}o(!!Xh+Juxj4ju@1>3P5fj85#wg0U1Un3d49~twa+R_{2dehy-u$GG97)i99Hy zK09xhd2}C89wU?hDuAO_JpSM8Re;>aU=yMZd8q6Jj6k%y)0t9M1xTa*e>a2wP5xn> z%my|XAtGCwNRf)SFSjko1T7~{&rP=6B0y4l34Wa*MPNqNO9Ccj0s}Emb$MrTd4UGG zl3RAw0r5&!qziBFDT-d!c{MjaS|pskvzWAwjVutsp#rIumX;VUaTmy9REl!AI-H8L zTW_l%$yOe_@!W~_d<97$Ie)ZbZ6?fQ0)#LqRovP0@D(vcWRDIKUh&M=4a&%>E6GQR zUl&SFEhlW|O4w=w0Si0!TsHgIv<;)UBRfJVw^$=0Mt4dt9jmttlQykYtZYqCgq7!w zDl*veD3NT`SIQ897J|DUU)_74`xP+&)@qQ6Ljf2ef+?R&=_IZ!zA4uuO9$bZ;!df( z_BfycTyR+mv+QO`)%rn@AUrA+_Kf8roJ;^l3IDh$H>-IehWqTNL(JRt3xg3GieiT1^tlmr@abQWkQ9}3xAyzM+t5#&=W$u2_ zJ^$ksvZFS{N9VK4vhe5xCLF<*`DIF-ib0Fa)4AuT_#Nbr%lM=6g~DVdt9+>n4$@1! ztU#85Fqf&nrHn z{~ZKo7!{CWXUO6y9g02QNJ{F&fk9k#ewT~>kztfb!NBG#c8kbBV&|NR$g+e%$WpJQ zvY_zMDFmD(VUcp#L>^1#f<4T%1{rzMAcHJEp14ej%)DN;Szne@OiW?Ip`DP}83QLD zktte<-yk8?K-{2vl*yL+<$;WaxQm{UiSZlR9uN)*a}$r(*K8Oh(5s|jeDcZ$@LWk% zky;Vn8x9pq!qtjEqHm%SB9n0{Doe*_Fuh5MEbzdiq*IGXF;mXMXnigjAQeLrCJaqB zNIzK9W0<%gDntBW0-3LoISn=tnbKKmMR_E7i>NGJFJs~0e}TAF{Jj{VVuku9sh~Vx zLriKV_=t`)u|T&>LK3;`LlJ4EMjjyS2bf?$gFLr*!EQP!@miDw^?+CN9=G}u46#e@ z*R0jUeuFk-TpB}0M8xL233*W70s{{$k(10^o#GUp>3$+R?9x8FIkL*+=T(CNy zaW^lmvhmCr`gPzrsNm^7)unx0jstNNumr0Dfl9>bt;~Yz+be15!z1j9s zCd^hzs$Hh`GQ>A1YIc*hFw0_FrRIwOFAY2wu83g+E)!)dE-W1zJp3y8!StN6WICZo zhqL14OM#0&RzFQ)%A~%(dxgPE*pu_t&>oTxXr5(@NvkpkxT1N^VUlP4N|Sid^nyOD zSCGP1m@CTGv!m3zl(oUv)(R0}gCboc=MTz4C#1fO5=;CBw*$9fOZ`=Z7^8f#1~J=g zGIO*d@f>*MfcWCYS;d@9RJx!dr_=lY{mE@?>^%);pd;ZOvi$TcoG zM!UylB~RnxPHI_(aO8kD(vk^qGWQ+oD_c4W&l;36Iv+Pp;0_`v*homuBjyaoY&(f8 zi&wA4+T2mr+{bXhcun8TXiASg$A@$36!gV*h7(J$l6Og7`hz*cW^t2Cwe zxz(hCuYw|cB>@_E1$*RWU)kJZ0t1-O>?F(=QKw$${yy%6wcxES5dGa&tmb zo?oos86o>j021Uiist8CZ{7R@SuB*ZTP44{0#;-}hFEBEU~BoBPDLy#YjLt}og`#r zK6bRte1xQ{<7~ zDYSCHm=MzLxJ4jw6OHZ-Bc-dQo#Wtaav4;O#0#N@Y}{o~mf86_c_V2uI}i44^@hZ) z;7ojp%vhE>2vwDUm}b5#Pl0p-$19+PqO!SUxvxla_#ePSElXvVb+uHe9T#2gD4S1* zecAVbsoGXU5e@J{9C=r&5`CA?o`9TDwAz5XHOS_O-hgcxCPp6lW-dGp+B1=cb@N6w)qoomw!GJLN!rqliyu6mB6d_t1pi5>7j8-i&E*CJJDWOwA&sNzS zHiDN>U%XzDv;ED{AA^g~r{1im3$IIjP+qEPk{EQarVtmGEnyO4TV?(zM4Lz;uqAHs zgqTd?isIpanwAbl$H^N}N-O5`VZ^RG}jJU;sfRO>bBuL6L~T`A%fHkojrtStO|e+IVA%zZ3tnLZVtv zh^Nuv>p!grrgVl#8c9~5TeGHzvLIx;9 z9`}}|<1)q|oy3A>PO^xrm}|tx5=c3Ed8h_tRN!t#*+TX=2@{Iy{B|^)M2VO2J}dJF zW&59jN$hXSP@8RQ37HdL{*sb%n6P7*tv5@d8dFS7eL^wBCqt}WSsHzVtM}h)GQI~y zm**LY^BUx{!em~(l4+wrz{pNwCr&GtH2n=S0jax^=0o4vEVd>1D{H;j+n8!e(;Ug6 z1B}ZEd~Ww2vt#mX>>wL-ndnM zxiC}iGdO$SfHY1sf1TkVcov4xjI!C}&7-jIIUq8xXR}b@H@MRwQ$B0&p@O-q}+ zyI{s7gqa$qr?@OvbZ^6g=)E##yd}f*sv<@ippXI(&{GM4S*MGU$EYnWvB>_#r~8* z>6}r~$kuY}QTmP98WJt9Duy(3u4}0M&jdc z9pu2Zqed5<($e8kWi;09w9abA#<9_Hw_cTNT%F(QFYb5heHLtNkJok|+CY7J!bBCr zyj%T*6(d10SwnhYp{0L*y?e+ZDpX94_{8dOWiBL!dH&_|q&-fN;4-P=>cxVx*G?zM z!r?hVr}BS4dytj7iw048;X?Y|c!0K3ba92UCVdBhC0_WjW`aGetF%4Ze=!b{u+Gz4 z^7XFI2C@sM29qHdb#73eN-=nY+^1D7hwW>$!4b zt-p!q!A;K=)`!8+zl`RMc3Tf=}a3J%frJ z)2evgjM@ca_rI1z}5*hSPZ;B}Qe=i*IDY{~+D`&YWR9Q5NC#7%mMy98c4L*+tDYn3{cnYq9)vqB(b zdDD*HqOUxzv_||?WkGg#3BB;=%B;r73btCpGUo*Gfe2yA*^5sbxERSlX!(6>6R@~$ z)8GkOVA?D6+?{}RkFEtjwo2pOab5sBU;z5uaD#cAPB7g{XR4t-tKDw5JN%-eQy=@+ ziN7jMq)jZ*Vo3yu+=%= zi{=d2pdQ0M!8thc@yDT)fm~QWDVCqQL9o<}F;@h|5jQ#wn1XJG;#35@*Aew&^`#!F zkE|$-AkHXs@!{PI8|!ktzx&~lkPUt~?l9E2*cAL{%WoI3Tq0Q|=WWcE5~;2^g!+2l zbR39jpxV!1;;vDFzR^W)J`QB;GZ`ue{Dh7cQ7-qjeU#*0(89ZpBo013xYP}Nd1+K6Kb6SM68qGHrx%hJ6` z1C?48U*NwsHOlR`whkhs18nk^r$sU)65?3bFP)WA`kxKEHp?YIA-;I}EKD+Qv>>D3 zAOX?r(~=4CYb2NZIi6t1xw+1*RF}#PQDF>l%L}uAsKgKeIG_ z*Fse$4tr+z!L!$0b(tm1{X)UFkPk&VuP z)#THe%NO@Hkr{?;IoPl=$}0bGPOlaS$Y3dsa20^C%i&nJgwDKDn~iCayxd++6aYYnwx-E$G6uXuYS!5*9{wHp{O!r{R&oFupAQ9w!k8rVm*+2}@6A z*LO*YdC+Mj{gwm7CZ2fdZ41&p)13Blw+e^JhwB^pv#(l9Tr=x$u z;5|*s*4}R5RnR^04D}{*O5)?QE%PYuQH9lyk@zY2hflX`HixJuSvz)@H}1>E=bXSpQ-U% z!jys|DjxUK#3BlDD(T-ITj z$2lpn&CF%~>EbDn%3*Y8bLCFOy`~O^fJBabjFmNjlFGYre~MG9?Jf{eq#PX zGFx08hRN?+KE#!P!9rY8SjW%V)@}Iwx9u+ZenRhVC?e`Jz@{bl{FTK zki7Nu`O=CG+!M7OunI4;E#sj4srBb6CXLWP>bh#QU0a?U7zeE6SRQprIZ5E2IdT-F zEDdAp2n%nqSJKP^&WutV^gcct_ggM%xLi1=+9%`Arh3xhZEkP%+G+ODWVn5g{|gmy zIy0#zli4>gb3Fpf1q*vbi(~$L=fQTO_D zj5oog8OzyQC=>YVgT<&pcPEc(ce~`#cb1$)CARo>R)}w*3VA1=Alg$ zew@Grp=5=$^A*gwG~>~LtGR`N`FrWUt@pj6xSq-p%t8`__M!#;T zpUD*3RhaxY(GmY6hWPWu;dop&jS09GEzZzn1n?^yMzwKx+U)8yJC|kkU_+W2Y%54H z(cRgwLQD`Xx93h4g9EseViY8W@uy78PYrNHBVfu_zhy1T5OB@(%s8~M>o%d=o6)0? zTTNg*KZtOC|D?xI0*e5$qjPiy>P4lQ6Vd#=kY6nGhzHH+1nXR}o!gS%8QjUAs^m>Q*DvS{(H|yP(;MeGX zP;c!N6N=&tHUG)FCBK(08LVFNbSvMFZqF^^0cf4&FF6T%%xo}gF*8Tymy;Ge>{bJ( z-qwb95~#g0_Six2{NedUJc1sq7f9iHT~H|_y5RY?5cyXaa2a&rGIe5~D@Y_`{v=h` z<*Rgw%j5w#g_kG0xEuC|akNMmQ9qRe$4nU#AEwJXyo(g(qHpgqS8C1syHqn_AN!bx zQOv|%r;ksaKD}ES*U5uh-M9w)7l|uZs`JT+$yu8_;{g%@jl|t^OY46X-_8Xz_bBVcME;#W<<^jyTQO}=DHKh95*a#!!GL?i2iSbqm z(fEGg1y>%S0g*AA0Th6>54x_DBX;6C$L_apb00SyZZ`bSdUEEi3%7h7MK;Fz--qT&&ykNNMhuBPa zV@c|pwGZOzpWkkNen%nCuG2ZRniuSUKoCIu;)YxMQhU3a3y(1B_{VvI+|WAMCf~(& zn+rYh6`$UX)K3GAZcCpWkNO5hyOwQ00Fmpe*R10=w@xkeZ8n0P6x={82jR`BvCq@)ARr0)jtz_N)YL{LXD2aFI0X znd8fMj(=|A*P1UK;_66gl7#cazBh;cHX|#y$$eqK(vk;g50zeAZFfzK=ZvuUu=n!{ zi#^DpJ)YiDCsur(aQ7$2fp3m+%iqVuCc`TG0Vc}fH(Pe0F1p#;O7ysEoSg) z*W4o~+_`jU0DH8qiO`$UHa7;25)j&2+S*S0oV?g}@>ideHa+el?jI;%)-UnP+l^L9 zcq4dS9lvCG1Ajy--nH~?bfC`2kxz~<9ONfE^D>uQx=wy>{-1x%gsou=Rt?7qj>WuO6?>;AcJr|~m(Fztx=wTWJc6H3g)ann&+R|_HO=f>$jL)>YtBdLF1LITCrs?mW^j$fiVdEA{CL|< z+4-w?uS7P!$M7}ehPxXalYss%p0?YW4{Ned-hb)$VAu~7bv+ye7-29aGcTcGl~b(F z-;ekp0$YN@#5Yqx!#`GYrOOzFu?S!7^u8q;D4g@giaWo{!{E_}NPT!+~SS z9ob;rI)1~cp+jn3`?_D|D_yg2l_46qCd{^>^Uy*4>iqJi_DK0duLeJ*J+_XYxMc)@9)ouE9GwxpfCnrHL^C^+QqYWKH%=kH#9kY z89G$SZ*n<<^e$k8>KN%Mj;unyjnMslI&mUk_3$?S_dwlu1p9l|hTZ%Pe}?KN^8c*lw}JLbKNwpWp{v@xzj~9n zxn@YtUjG5hj0Pr)z28UdCN5I5G{#n61=;e&w3Sq547|eXUL6aERN-j?$~c;U+lHRM{+n$xqSL~910EO ztx7DG966-JsqOpEdjHRI#JS=B>)&X8;5~ZyEibPiK8#}-#Bt$PZ+L3EfmXW%m+k6w`$q4`ic+{0mkI7gY|A5iIp-}3hB>+Q1mAlS3JIXz zWyf9XqK5Gu^mu|u1l;rE7x&aMrz4_I=gc#>G!9?4JZ+oKqUW8MZ_rxI8EZM@$<-X2 zOj=)?EY-OS?*Dy4ezQ{dI#lP4YPE+r+>2au7UFw#Bfoyczh``(`?>gUU(Ubp;Ka!T z{@2X+D+GcI71wwG-)~0=1mU{l^Qv2G_n(;gC9b{Xm$0+qu-uVT=?ve%FfP-h5 zm+TAW7P~w`CuX5|cpVh8SH}`m2Sm$*Fv=GnEF@T$JkXyq^o7^yxwcGa)gGKQ6_Tu4 zmvrV^ej-eTgT|`^I2QbTM4KE5C(7h*%C9-SD|r3QA-}JphkeXmUIeWD#;ZD?xAJ|$ z+>}HaKl#kJq`lgCe}CKjemu1>g!j++IQXvs2Qnlsj#l|amq>M2Z!G?+Z_jnqF+l=bj0UNO&K5A|LoM*3mEl+jocP1vCOr|&{k79nmA-(O&6$LELXHa^I~ z9~H9}?>o)yss`A_6<)U~4RD^|R@@)y3dpt?TbW@H9X#Nk^k?@#;lwL_R^ zj+nn0NdC^t3st7Fc&!%`<=^MMA732@7i{ORA!*kvP(~Kzs755yr(5{x+!E@6Oxv7< z^I4=M*zCNdc;}3*d$;%m@teP#%$O~2wPBpN!{hI0ej=4SG8 z0PY=sx4!wplRJhv#Cn?Bd2JhBXXVa3CeF?&zC@bA-xhR6WX0b;>8ss-YsRJTp9}u} zTTJTYEuSchluMR%mKO7XjNO&0t`47ir{(y4|7gOs^>Nn-Vyc7>1by)VdCGRh2Kn9Y zc3!XFaHVeE!s)x3j@)VUBxV+n0`3BjHqh0^_WZYHQajSZuqG$2(T%bLKPwq*2 zwU#*XC)=SR3O{|62dAD`&pUs*I!<1&MK?aY_STn64|cBy8c*|+f4+aR@53xPstnBK z6V`?BP3bv%#W|rFM|03COfxgR$1wA2T`c19(Os?BuOuLo-qbm4OLK$Xbku*mekEAfNT z3!b$T8l3TWA*4BB5l6QJtyfKsYA%c|+3#Ft(*R%~D!6fF3PPQCh!tN&U*7xr z@(#Ai-`lVL?{i5|`*rc({N$1=3!<(@@*{z$9WZD^t^noI)V`C8s|oNiFyR_u=aG;$WfVJ_!^?hzhe9ymGURSTikAaVDPQrfqJpLE=1%cC|ntAZQo6KkO@=k-g zyk!&f{xyT6IMHM*{B8jop80;lmk|f$eeEJ-2%dIRCwW1N_)_=VM+e zFaBT8+46zhe@pLOd31&x60j~IO+wE2>XmGp(E7SBZS$vD-p~kk&_Xw}e1BAxeKk0Y zF^ZytLT^4SjYFfGqP$7L&w1az&i-72S$vBV{rZko#IKru&o?$gEZ3&o?TK@W8r*S+ z4Ff~Y$gA1>*KZ5o%#nYXYc^)f8cl-V6V79wx5P2T;^IlHch(MSH$k)&7bqTkXUy=! zKX(lw8K>g3GPKjcr(2L%K*46fmA-NDU5Bjg@@0hY*;F1itnwX-gVvIZkuavD+`RK7 zWGjj0nbE2jFZN&b(#Dft&XrxBy5_vHpFWwEBwKHC&f9RVc6q`sue6qo%XKS~_D;{f zSs%V@<$YzOaxlwe4q3X9cJ=n~fVs=%Onq`_N$cZdm=u}kqxip;?!+(V#Qy{M=QH=+ zXQsKD4xj1TB&k%o*w1w7!jvQwpQ%(xl2AG3Gu@XY=@MpgrERH%koGf`ge2r{+nHF~ zCd9I9E$wgi_xSz~^Z7hJ@Av!ldQRrnxPVhD=O5kW#M`v8Oy!>`@UCv@3L<69Hly|w zTs<^qKP9CvTWR*)vX`H8R#q$DT~8_LFf%z`9P>-rHo~aO?r^SZHT~x|PHn00FE3x+ zH}_Fj-L|B=$5!2EKvVN$E~~>2`?q*p2=$}6Tq^LqUYzoL&!wQ@Q`6!cXNT>xJ$4-S z*qBJNRqY5sD|+0SjVApWeFz53DouLaedM3SS#w9TIg7fkZhiUdg4KRH>NRCBGymC* zm079&ob8O2+@jw54`(PFKY&%mbxc0U77@GUK~=z_Rb}Fc=Bti4eRfO5)npdz@AEQAFh1veIrlE$bA@PSdc2wQd{Tbw^8G1GL)9V zpFEi(Xq@?H#j3+kOsoJI-##C3;K!Cdw5hoh^}M^|cer5NMfT%UG5eb?_O2(u%SP`O zs8EU*cal;_>4j4EX72W$=chu1ENbcG*I5DRDQPg1@S|@So`p6=^E^vopX;gJ9(e_9=yC)TdnG7|j>ugV?qjDHn5 zLpV3OV#|(bRB-!3e&K%Ley68D;t*ZG?MRhO3q}Yd))Off+;1NRyA)c?hf%%Q)QSf8 zeN_HP43Iju%#r>1^uW7e^96*~7oT6A``S+<#q9k+^in5<9C0B8#ce(G&Iu<)x8H4( z819cAgxPsIl|Kk^w(MJxY1EvU_~_Q%pL*pGrZM?OzEDEPkl3a50YEc|*T3{NwDj{D z+qdQeG?kdaf;`4iKrl5&dZQHtCn~(Ns$Q_jF#|G+I2 z5fDmA>`jJulP2uZ0qXnfaZ;^ZujGY&?tNbLfB?& zUKV2jvv$2u?&p9Kj}O!4H6j?fNUwb4tMC;nj(nq49#j_>FtkADQf2CIVo%`bWdt(S z$bV~<-TQnt0n5K2C5ilLIAf8lH|kk}IGhI1thMEN9acP1Gy?k<9Y}=;L=fcL%7`r*3SZUmso!)Jf*fhJoWxox`$!R)QWO|#Shcvfv$(`{{<-2{Lw>g9P2eq0k6 z5qF>FB{hLy?fCU*I2*c|uiNQ;VKRU;UhJck>&cATy6sbB8tT|--yB|%nZrB;>be2AW(l=24Y#Cno@5mwR-=6qaP8HuxozR1Z*6_EObWX?# z7?`K-JKf4#u`>aa<^4FvEm>CVX{IG|eQ{)lf24k0T^%A`J%B*Uo~pN`D$>J_YjOgX{>kw2X3w=tp z>)Q&sB$Svg?@zK0U3ELI`WKs(MN0Sj=NmZ@Rur1fKXgb%_g<%FXV*DxZ^LFb*>w@d z4rT9i3tL*b#ow3uV?M!dsv@~VIVfxK6;-j9{- zf_2H}UEWKFR15J^J`>e`SxaF1q@7iLoajNEim~9W2F)i!rV~TPdQ*Led5_KmFc4#(dWY#4S4Vm~4K0lJEIL6B88I zJQ;I&LL7H*ZSR{KFvS^_GQ!gc5H{s z!AKU37^2veQ8nLxDtSmR1f=xnQeZ94^3VYLwa{+0R|00#G6CnPOmtfu##93SBoSJo z8kS0S%LKL>qahtV4JCW2!S0QTLLDK{5Um`hDzSO=?EQ?gyPrGMe;tKCCu5Z5YO?el znX4m&Ae3@7a|-1mpr}^+)Z^xTrzH>gmXg(KFk;fa0feGq0LGdAGRDr?5=$Aqg-Em0 zb9d41 z4E3=OHPOKoB|Lf7Qo_(sn~#%UV!|uSihET29*o#?m;O<`^KHI}0Q1JDZTeLFE}dbr zCN!!c+AGTujfkgUga985LPwvPo1%SJwcfl$Wjv13>NjW#bew1v`&X63N6Sjq4P~n# zM<*+q){6!EdZ}q+I4@g2&hl&LZ+)5GuQYGg2pu$>QwRk{6CHGvW{k~H87Ih0TqE3P zhCs;<6<@63TtsO8uy5aQwEGA*N@mi$Z*#kXv)7)Htlv2-`{z%T7~f-Fq=GQu!`lj> z!@OO$RFlcCCZR@WOcC1!5|8REl6*}#dfL=}AQ5AS=q0~u%**x0fwz_BM3jIbY_Uqv zk{&)Pm85*&97RYixnMfRvXqHVER#Obh&UShXc@2?U@tmnQ=}sDaR9;?kb={Qlfv$k z8d0MVmH2+RLti;C;CS@yb;)W4)Pj;r(g?{IV*=$RfRbBx{W~-wAH7jGPW4gKJax2J zI^%N1T%|MR&B#(GnF_QhoPR}Y+<{-Vz-eD#q1Uz@XEihYF@W0qg7gFzWWIqb)da?L z)R>kUsI!0HZlhKi-@?f7GGeouTO`{ts2ABu**Wm3mKWe!L-kw7jZv96ZuK42O44M; zepL)diJx84r{u#La~&!5&waPlTPT24M*dg`9DfWT&nfQgA!p z*459qEJ=5+Rq(FpNGV_h521O&Fajm>&Mue%Aj0_$n7@_WUu`5hpvfzc?P6c16nq7*JM+dE! z>1ZP;H(Fuh9w{A?iXCL^-RO68gmNF??>=uk1{%ek5zP3LBo5L?dU2q_=q)neYntdc zykb};;(!bf`vWZYjwniwpl9>$?quFUn^?;)pAs25~$}?!+HV+W&mslsrYP_ZH9*6s}nb> z&hQa-j=_I5k{rrCKW z5*4k>9-yWLuptpaO1IVxMd>)H(j`=zIWJ1*2rl~JT4Co%=bavjn!DOxrDi+G#H5urOJx>YenphebQ#|hJ+A&m3j^$zqx4Z7H%`ikjWfq(;$oFJ zTP4Ig`FS43cABDnwfwv%0!%E*&J^uxvl-D!cI%D5pv*MW7a&K^8-GTb=`+}@cZ0;;2+K?_WKG&HeFCM}h*&r~`m_5LMajQ7 zGgFtlj!R5{={<;%g;cOxE1B5o+$A$fP#H5+?Cd7e%sZDgI=T+vp;{A`hg*ym4ADKf zB?O1uH-{>7p^B9EM z6!n~J?t_mb4ticl5b4&?rcv-@C15lUXD2211{>UMAgWugW!so2VNBLMnKrB5F3 zSx>a^k#D1G4qkmB;Y+`zB1Rdi@-;LGtfl8{CXV8-!V+RvK8Q8%SDIo{frZSd2c{=r z4-@+V!)Ta{&>8{OC}zah@?TYL$0 z!AQ|p=Hm!e08Wx%=)=-~O-T zL=_QH#TJ=$NKb1t*HyKGgqWguuxPucc+PWEpDu4770{3Oy~yR!P`1aHzV}KqNhAs; zZkBdGs~Z!!6&XJ9u_;G4X$eTOhAa9T&0sy#W(Hw>sOY@nbPh(?ff4RN7AME-uA84w zj8O-l1?!|`XKy|TkF^?7F;W1l9&hxXhg+8lTI3OIJZ{zu1Fz7lYb?cG>ND-QF!Se= zjd~-82V^t-F@5 z=NmMqq0Iq0E%Y_?>6)2Wv3o{m4jj6{jyLzvGY^=h_n`lTt+hy$Y2py$%%hKTK&CK- z`>e~h{r;U!v){sV1r|Eet9HK*4QJWUliH)!-R7VWVRK@K>9GXE1Lg^W2}u32M*inV zbk{Ov{sj%k3O zhl}Ay;V&M_FsMU2I)eXb6es*T%^b40t9-2B+NnW?zIw&D_~W(MUsl*!DmasCEgXpR z(`MOR(a;GxI^p{n?|vCuEFZu6{Ws^hsoRVGzTLg&W(M=ya#083YoD_3H9f#*<5w6WxAPYjHXlv!KbV! z1kyy5%c;RS*GxJb4CBt+NeH0L zY0fS}*@&8C>{*?WwdO`~0A?(PJ3}(hE&;?>nx0)NU9e$+6PV_3Fl#d>9|%w0Y?#bW z`ox`B-95|%vRRG_mw!1HA3SAT zsPBFE-!Yaf%1{E+==<)ke}7!!w>%eBNj6nn`@NmCm}d#;DnsW@E594|h$JDD;7;Yc6fg&2%lL^X0(H4P$mP#3E>JMw!@P;ZU5zRdy9c6K?cZxo@j_ zex?<~#MgKo2e_D$npb6<*pNOHoD|V=nQ}PgWd8BRKx|P|k~%`sh;Y{NUUGvhJv(h? zLP%M&lTX}|884>nS?GIw`OBvC>xUvoEH^YYmP>x$^Y@zt^&SCYfN|#REB-#Z@Nr`*sz9CUpC_Mv4A*)D%w_W@pB+#;cB%XOE6oG7mX1g5EEk zWR&uNSxXPSh~ScJ#w+I+Gk>YYw8~1%dYQct&61$=&f@nlH?;&Yb`0~k_kn~w;FoU~n|i*rwU!fC<%N!?^@nXt zKiJR_N~nvjOo7!#A+j5Exl^|jJJcnzNoFr?%m?grq7Oy+6jB7GM%i`JddLa5QmE|=5OYRz12ZBVL)oz??C_| ztaKAeW|2Yz2+iuc+EE$!o^)$L!*<#~mtWS-`FaXr=_})cwy8;Tn`9572MSqMK%1N~ zmjIKdF+K6824(U0R*m}>jbapMwTk@~xK$h`1ujN_XHG-l+WbP;vFhWf{l@5 zR=o3HH?M1KmRnRXwInuUM9pwp^;+ET(8#@da(9GfM5Z=kW2m%zs z6OG(VqT0%Tg)&=Y#G~7860b~$WW@;1&{n--Clfexl!oHThLZzQK5o}gL=%$gazj5$ zZaUgNFt7g7CpRj6()Wli@rwqG3ZTlM8Q1)J@7)6)V<-9RI!~C;v^CwIe?50anAcXG zpF*|%;USRbc43~hRtsH(cDz)#9I*muodMAOMegm?Hp)^@gLxLDqV!`ub58 zPYZeP3po8}U4_Amm{^!7V(brw^))d1T)>LwD;iDM8$#C5xHSLgL)YLRa$M(SKipM; z@2RoeU#0aN1&LWSs|}Qi7hxS(kXm`75&0hS+HMfft)_5z?4nSad*E6hC5VRI)z0OHE0OA=lgY+tUqiit!1 z#x4JCS{?tlX@#;LG`#JIZFioR#_#I}v4TjuO?Ptq;l07{Hvd;Twd%YTpaYzC88`$=(dPbmrCa6ovCXCKLiseBm*t_hEft zuv(enC+x~R<1@fzuDji9oZECv*2iTh=my7*neVy<4``^AHnZ6d53BLs%yJ>cm z^U3q&D@wRB+sZEeo`?b$P|oxY+TPv0qc*pdzknvVO)U2#_-?2p53*i+fmW7>i~?hu;)zQq&`tHHDmvzudTikG5FW( zkqy4Wmz*!drAO`WrO{0zACxbX*KDNKts3f%(97V?~XaC z;{NUatF~bvV6F)^F0!Uq&Z}Ui|Fo;nqi6b5v9BO-|F@}4|JshE-Q?D8D_b}9(e^?b z-2~zdDmZ<$jNfNEs|Zv3)}_@|*C=lY>fiCKI{*F0==a=EFO_6b8s+(7jGTT}_N z)uNH*-(TSDE66m_xhx&XC3Ex1+)%J$<#E~0W-K?UsNnctK{FI52ARvUm#;WraPM0A z5fEUS2JL#dQh5Q|^rV3FzF?~z_x)d+O232h1VBMPlnN-;QP+n~@KPoU(vl%x2w1vZ zauwgYVW9X(<~HST6{d~~O7AfHMg^7DDmZDN`_hu!z+E7+g~*L94~%^z0G^y&@Ksm> zI+dKvEIAWh$h(|rC(#k=f6`+kD}0=s11&kc$dI_ZOkZt=n$)gAH!b zds;bFlSYv*JE71A&J$yHrKr~94kr;5q(6%r|5>ymrUiv6`|3wIT>S?^e zI8SU`8MxtY`i8n!(3p-8ygZ765v~V0aDV4nUrq-rC`|^X(J%?nt7KWxV{&E(ka$`N zGC|#D1T^x+fV4R1MN}$Ll{(oE`ERJY1#bBec#!p;D{KWQt$+Y0lns|eXH}6@9I+ZK zxM(ts5{`XWwJo?N<9EW>8vd9Z?D_2SDvi}4XElh7_mb03f(8}Refyc((#!kmKNkjT zm<&i2-^VgQBd0+Q7p0WlRMs6SE?DmbQtAA&t>E{;frDw_9e+ub8k{##caDCzF^K~M zq((R6a~L7i)2|O9;4{gRN;tP|c0=#qJ8ok@D$akVCSP2&Fur2(iF-_vd|O}ek%t?$ zH9K+6i6UWs*UP{uOXlvX5Mh~KlXJmpfSCrSzpC= z#(|zwwf_mJy2Iurjk80L*AO*NT94c`RL+Tl=0>-T#~+?&TFAlml&X6=A_bxGcO3T% zIiYMerhpYB-y8e>BV4Bm;*}@D?N6o>S#wb!9XNEduWNz;%UU;YNn&R}AO$BM{Jr_w4mKK9PKpK8-YbSlEHrd zdS$`??B@#iBsC+o?!p%4rQ`28gE)O7zysxAcq^?7^-A@-6o(Q>J>aU=O9`fz3QIc= zzGt7Up!(s!TUR35O1l7^`?*rd=~dIWz$D{Pz$uN=fF3HIbLIG^SsFPtcv`^K5&z?` z(awzV|8dygCjOtpo|$Iu3B7Xd_0`i`Ia-vyNk<&w0ip`x8k~A$m>IUoa&NI=K}HF1 zBFxpFh)JWJ*LD4L``XW;l3!3}H9}nu5iceKwrQjdY9;M7&K#b;(xl})bz+@G>D!TR z2r9Oz=r;Vx!M*7p$Cxf;(H04$R diff --git a/weblib/tutorial/chapter9.ma b/weblib/tutorial/chapter9.ma index c68c8f1a0..fb11216e5 100644 --- a/weblib/tutorial/chapter9.ma +++ b/weblib/tutorial/chapter9.ma @@ -158,7 +158,7 @@ Let us discuss a couple of examples. bExample/b. Below is the DFA associated with the regular expression (ac+bc)*. -img src="acUbc.gif" alt="some_text"/ +img src="http://www.cs.unibo.it/~asperti/FIGURES/acUbc.gif" alt="DFA for (ac+bc)"/ The graphical description of the automaton is the traditional one, with nodes for states and labelled arcs for transitions. Unreachable states are not shown. @@ -176,16 +176,24 @@ Let us consider a more complex case. bExample/b. Starting form the regular expression (a+ϵ)(b*a + b)b, we obtain the following automaton. -img src="automaton.pdf" alt="some_text"/ +img src="http://www.cs.unibo.it/~asperti/FIGURES/automaton.gif" alt="DFA for (a+ϵ)(b*a + b)b"/ Remarkably, this DFA is minimal, testifying the small number of states produced by our -technique (the pair ofstates $6-8$ and $7-9$ differ for the fact that $6$ and $7$ -are final, while $8$ and $9$ are not). +technique (the pair ofstates 6-8 and 7-9 differ for the fact that 6 and 7 +are final, while 8 and 9 are not). *) -(************************ pit state ***************************) +(* +h2Move to pit/h2. + +We conclude this chapter with a few properties of the move opertions in relation +with the pit state. *). + definition pit_pre ≝ λS.λi.〈blank S (|i|), false〉. +(* The following function compute if a symbol in S occurs in a given +item i *). + let rec occur (S: DeqSet) (i: re S) on i ≝ match i with [ z ⇒ [ ] @@ -195,6 +203,9 @@ let rec occur (S: DeqSet) (i: re S) on i ≝ | c e1 e2 ⇒ unique_append ? (occur S e1) (occur S e2) | k e ⇒ occur S e]. +(* If a symbol a does not occur in i, then move(i,a) gets to the +pit state. *). + lemma not_occur_to_pit: ∀S,a.∀i:pitem S. memb S a (occur S (|i|)) ≠ true → move S a i = pit_pre S i. #S #a #i elim i // @@ -209,6 +220,8 @@ lemma not_occur_to_pit: ∀S,a.∀i:pitem S. memb S a (occur S (|i|)) ≠ true ] qed. +(* We cannot escape form the pit state. *). + lemma move_pit: ∀S,a,i. move S a (\fst (pit_pre S i)) = pit_pre S i. #S #a #i elim i // [#i1 #i2 #Hind1 #Hind2 >move_cat >Hind1 >Hind2 // @@ -221,6 +234,9 @@ lemma moves_pit: ∀S,w,i. moves S w (pit_pre S i) = pit_pre S i. #S #w #i elim w // qed. +(* If any character in w does not occur in i, then moves(i,w) gets +to the pit state. *). + lemma to_pit: ∀S,w,e. ¬ sublist S w (occur S (|\fst e|)) → moves S w e = pit_pre S (\fst e). #S #w elim w -- 2.39.2