From faf5a856ba919cb1eb6a24331601d57940c41eff Mon Sep 17 00:00:00 2001 From: matitaweb Date: Tue, 6 Mar 2012 12:45:54 +0000 Subject: [PATCH] Pictures --- weblib/tutorial/acUbc.gif | Bin 0 -> 26666 bytes weblib/tutorial/chapter9.ma | 12 +++++++----- 2 files changed, 7 insertions(+), 5 deletions(-) create mode 100644 weblib/tutorial/acUbc.gif diff --git a/weblib/tutorial/acUbc.gif b/weblib/tutorial/acUbc.gif new file mode 100644 index 0000000000000000000000000000000000000000..5812fc8f462a99d6f138ae01d7758fca10b2bd8f GIT binary patch literal 26666 zcma%i`y-S6|NnJeyLMp1HN-G%j&p2t3aPHy977`&CC#CdP7{@i`@VK!ghncrYJ?=! z=%nL4tkQXkZgqDUsZ^?|?rwGWc7J{TgYWa_>-yn!UC-0w@QR9w3=YXS2rmNPegyy! z03ZN_0SFJmLD&+ML{VYu2vM zUAJNF`i<*0h}Lh++mM$p+EkF2zj;%^mi*0I3$_$)-nwl|;r6ZDb`)+e+P0&3d(m$@ zihnQq4J-a#{2M0uT`a{UGO<)Hk(Eg0rLq!*ytJ%DQC?cMQ&C<~wzIOlqH1U5u8JyU z<*w=~WzDYY-O8HU>fL*4YWMEmv#)k<-JX5>_tqWQci>>%!9)A&4<9^qr2eq#(2<72 zs>UM?M^%kY4M&?Bn_7-GA8Tr9Z9aCqrM2zY@e{3W?Z;1?Y->Mt;^gV}Q|goI&Ql#{ zPIsQ|ICHM^?D;e2E}T8zb?(B&^IexNT)fB_~+S1(<;cKPZbSFUwm)%0BJ?){@j z+ueJ;M|-39`c3VPzUwz{-RQf0^VXfd+jno>xqtiKgFE+icOUfM*FAjD|48?6p#Ra} z!-2<-2LBv*JTy4;^zoCw{(SoE$zRW(K6~-k^Ow(F=%2qFexVp&8ydM zN8gOSe*5mt*!#EdK8(E|fA`_j`;VVLd@_9eJn_l!<@3Z>!#dbn2s&iXQ6nf4NRVLtzG+{MnWHh zd$vsnfdtCoGuiFuKK|8}|KY{GWj+dE({{3B!j-OxSA9{3Kb&A){Q6dRbpDawLYJ-x z8aT7|<^8Ldx3&!YoO1Y)aP7*EuVark^8Z{S4wk(gxN~H|AJ_gj;`{S)2HEr|4ZU7Ngk z&FeiWtB$|ko3`cM>wUr!k2iJMd)K_#pVM;u&4G32-@Q2~y5VtbgP{Uv8mL3Ql6_9r zb{e^2&~_42W|iB@6hpZ&9w&9?6`X+_|El!-#kudAMTZu~vrl18M$CL=#&v2)tD1{r zwQLvS+B+|aiBswuo*#~%48pKBRuG#@nh6ZU*138y%cEn`Jie&T?ZkLzz|}|boRcZ$ z(RQiGa5#a`^d2Mn8q|ENoM(w7*QVO=ojzJRFFxp1)6weLuL^mU{@Wjp#CjYG{&Lf9 zMHr|hJBBISK-v|d%xWXO^Ol#k0B3dviSp*~U(qal9J5?NDSj7K36i-2@ePMc%xOO7 z&w${8kS8?fJMKG26K`0|u4jW_F;&z}nXj6->DI~q`a;XMHd!64t*=qo#!r~ z)@mESCzkX4?CVNSJ703s3au5bT|sKq@a?L)9^MU&yzp_$-f^}xmbs#jy#=t;v9C|j zt2I3pmlb<@E4+92f!E2c-&caBsRm{&$MX-LAEUE-7T)u&QgQf1;$fYZzPoRP^4Ia| zg%utpN)Aj4CaSo|8Z>EVQ0<=^F3X{%ZWF-_A{s!8treY=*-!WQQ&`)=CYAxzNnNCyR=MGSzrI<#jrW%D zJFelmUE(r!^=z|HNk&i3bFyltqY`4~P)(tgI4hYd zob=ON;^`7@-B+$MUP7zO9~v=>8aqsC6_J)HdHm5UnXg(k_P5aeNYR$!{B(Q=zGEuFB%Rq3gIr+BZ2qmyK6m%dU(Ub%zrSV#h7qYso*q z?E4aYgIS{Vu~awAn8jZh6gnZN+A>HA0fBwY=*GJ2Mq_glitp5wy}KG?ccd@;tFIoP zM5#P5R=;9)?nH^X>-Z%G2of~JH+2joOMIYu_ zCa?jpTxg`z{jCmmigGJK0g@85o^{AAG#Zqz`=K#^g|@GXDyR~$x&ew_;{EgXgMwNo zb+Rjd;jBALp^MTPNrtJo8Og&BTlP9zprmH2OzzXiKdt8UMDt*h2u^DKTm3vmMp2fR ztoZf);_Hi%jA#U#!OGlwtuoTFbq5rgHsg}MvMPk#Ed}CKCO1hlx#bN65&{^X8alT9 ztrtBlEu&446R~mdFVlr|=IMM9p_o{7a08Ml+jq}fOnq1xF8GtMS1}@SueT}G^ccad zfPG}_u>6-3h0I2+iu#Amo!{8*=tF@jW%>UObTQr;U{gp1MMqCw4=y2xr6kILbt*Hv zdwIOQc_nxTN;yaEthwq`#Y@RC>Qs!^*hx(1Uts|LI&JQ;yDMAhugHW#jNabAvYgaQ zCgcE9c5vF8Ao6wlqjeo*cE`$D^JVl3)h8sKxpMZu+uWY(d3cflZ~os8r!$iqNwmCI zyxH4bZ|WtWw~n}R?o+4!6e(n>BABlD`G}cEbU#Ib7k{%Eu*@L3?=6%jbXB%w0zmo!P3jt%KM|`X5JE{WTn0b$!c=$pw zYg_~1`??=Ki9E+XjIB(r4}E4Ea+B#R#Mp(l&#Qc|@7X2HF%R*w)pp^%_*^62Shq>0 zQbH{-NF=`li!FtNj|ex~)_2F^@y9@L(JbpGq0GKZD4QWb7u~Z0DMfhiFq)^i_%`38B;i}b?@ozQr&>q-^q8Y` z6IeO`mwXO0AJ-VKW5Mp(4V3W>M2FToE>I*Q@7{XRzK#Zh?TiQD{#UeP!7>{KL$c03 z2Nw|CV{OnW634=q@6L@0>FlNm+k4D^ibPgh1+Cy)TsRT*2D zXL_kLHb#39e`MoOk9k2|IOWo6z=F;+DG$caREa;T)XsLjBDw2()pq~P4*2vEnP+3( zh7lIdIAu%3+xd5^qGahNd-pvEA$1WPv;6_?4lq+6 z{_Wa|`jyd4z&HB(7o&R9a1;f1u)VjdsO6z9;{5SfxLl!;MzCY!u<1R4@ismD;T14j zNT|`1zc|w$GYGIAtTp6*-I_8E7&Yu8jK8&isW;xnh8LCs{s3X8fSkUX_KrHD zvJ3%&1Y0smi(60#W)P-UN89%^j22*?bcE1^$S>uYb}5MghQe8D;#HNnxu4QUguQ1e zTo)O;i4um2Kco2YtoXUSCQ^M7m@AlY_ zD2<{RDWQ6zhOy#lhRI$A9y$sYtL5$87TPYdEe-;`J`u4g&;>2+Id5j}4e)qkxaWc%a{;T8~Tl1~(w3Z$Psv8iJ=4RKTXR zgT{0ffQiz6PDZ>3NF+UI4h4KMa(~A*GS18LSUPI{|%~1m;!1Rx!eV+Jk`dn zplKEYgaUP4Hk^CPWvPs^UXE#=5O84_cTSZ#-$plZmDw$z$$vBO@*nkgHkq!u2wei~ z$3-O08l!raOEA4 zNC>zJ$^T3BxX-Rg12){Gnl@I$HMd+oAtZttYRIwuQv*L8s+m#l_FhEHO>Ml-C0hx= z7Nu)Hs@$emDf*4+8lYNz$m^+Vvk;^LdvqP9r>Xdtdt57oK!B!l->|7n2zUxMa%0^d z8&+fjiMOgvIBGy;aMd9=W5K4u{;X8h?@NBVCOzH$!N&dy3bKIalpfPN?}+FDTDuZ7 zRg<<|YDw5c2}FUZeEq?j!$vTQH+t{7UkD@_)*fVa=_-JhM4=V{^V1amztfK zD&a$>5vVp=8*XCFhTA>37hMTUY})xfM&?Qoh_P=#fGWhiXeI5f$atxy*}4F%bwIU75J#l<|T>;HTdwq&dh8yA{#(StNkSeIA)-Zi69ocbHl`n_+{qF z0^F8m$kOTcK%ds30-;1g@oan%3L5udMBLsS#BhV1wjF`>^O4I4Qhqw0lt5<|rlU)fu3_X2Bt82g9$CSxi9 zExv89Lx2l!sMmDXw|5|ah+s!OVS@%F7zoAJNhhUV#of4imQ{9!RSu`yyq((eFZs@( zgIKSMO|x2EZAHj1DW+bu7&hsT#@zt$r*%-az&OK;YEXhj8oOpaU~g#g4r9D!A5TV4 z{RNU}3^j#mOT&<i^jrU4O{Io)gMcw?0DMHV z7VD8+aUMn8Gy)i#ET9t10Y8!HCjj?_LAj6#EWSe(38AZ8lMoarLNDcCvA?MYO&P{- zJ8&xj^Ep}^35<F74A zxA-IkBA-&zD0aj|)8a%Jt|k?CuTlxO_Wz=VV#uKhn+A?;Ege`8_HbVslBS!ob~WTW zu5W9k0{J0Gw$6I!FJxR#_RJ!JXu}u1NylC42NcNjqTkm+WZ*97<2ZogNIG3^-u1Zl z>+?9hfyLA=owX1{cB1efEaceu#V?{#yGkcJ{lU}yeK5yPzm58Q-NW%ECcFC26Z0N- za_xv*VzJoRW*X|Kh%REt^|{?AH4!wxh4ll^Cyb1BP{xyypeXAQLj|LCoH6 z0%jc^S)dDZRgJJ5h~tMY;5$gg;42b$#O)JOC3-Qh8(ylU*JFSmdJO)Jj2|VapG;l zgvpZv5)8iif^K+c4-vZ^upL8d?jpJOAAgKTN_5uOmB`^w4u%ZmEcpf656TVn_v*Xh zzuw;JAY1FehI>|D*PjTRFl`p$KqXYKIbsEj(u{fi-&X;oS?UPgt`9TH# z%|QOgc_@y5@0WnAMgS%tdvfg~zW?KIe_3z3Zt(&E{`o~eX#fHRhr4{~pAE+sBkz}q zUxiJKCeD3LYJe94=ASQsMDYbRiX5>8$TN}Gub&{Q#$y!>;~vI~4Y%}fOg+CFkrOBE zLlAO}s<&(E#k>w1n9I}8HJ0F<9X zDsO*AxWl0EGbF|rbKu$$3>06wU*wpZiR8OU`Yb|)R&rbgT(UZ)OC*n%HHHXa=@ zRU$yL<{3WmXWOQqaNZz6bU7r?l!X25$NdMY?%eu^)dd0Qi;fnbwlSbX$--~xQ+c0$ zO?+p8hNMqlOqqDM&s2wJcp`VG7z6`$nyTi(vsz37*_)4V5^ukU_=P(!ul#8@Lj-`iK#xlBCJy{MK}HYHxX(vMOKjBGftJ*7R0evX%zn;q z@P6Gg1b;OAFn@p2>)5?M%dg377QTr)5V-z@_DOZUIaIo7YTfbZqu_2>dK@Jd?5DwI zZ<7BV@&?-K3^E35tNNgK`bR>|PW(rque*CtHqs!aUaoqP+y8}N+1w>;U$>n6&T2z= z0WF|z_l_^mq;teG7GDWAC?cy$?5zv_al`0acloTiQJ?yC)%`J8l@R?#p?2TxNZ2o$DbJ6p07y2QT5@XiW`v9lON~L|8&ykl6p7{I zwj`+4FXl(xMF!{H!tW4}ZK zkWw1T(Ijf*K}YM*QkzuoHAhPc5L;gol=H4~LHw-O-)KadSROCF2*`7uMVO+XQT_3H>W1hjxAkX9 z`_k{+(A}8BBemjN7n5k>d-;AO23PW|mKZ7^6{_%X@)^mCi~vT1jd)gm)E@VsPunScAJqaL_b*;N!#XxKUgNgffz@;3@UAU)YXExnS}9P+AXNcY zed`(J4PP~u;(-v}x#Y3`-5}yy!);r0-VdE8&Oe1Kw_nsIzyOa`;$!PBe?EWfPyl4W zeZDC$0q~3R%p*aM7ZbDd>i9;O*~Q!att5$gf8YMH>OnRjFdhj%Y7Tv>wfBP%e%}6d zR42gnyZ&#^mbu4U0 zI_PIdrb}0M@RwPdd9ViAFD80V)y)8wCeKXm_lQOUI^D$+;Si_q1z^3YoC@!vwM^Ww zM;PLWL)|USH23CUT$`};@7Ze__DWxKsGS0|7o1oiC zX z%W`|Y(A1g6usl%PH`T;%exS)R12IW3y3Id|#voSa-E_YD8n+Phb-T#|AzK&a9IJ_4 zh>OBKU@G(Kf$7hmi#|hd1L7sjT^0yU>}klas5slO;)J$kO9m+j8zo1`Lfd)3k_m8c&owzBg)TPQn&69;426xU*g4r(gyoQJOA>gS}Ky z4uxs`Y0Fy`F%AJWuIXPM?fVn=2EAkj{cZn|Mn}M@(TSZvLF3lFY}BLA$1t!_vv9AF>&%<1_Hs~F8x6k8 zwJjS*Ya{W0G-MeOg5~H?HRQ;M-$U>yA$nu?nag_#Bo=p9W)q95LG zeMM`b$*ecA!NGBNfTCHHvlju})AFtk#Y8a>gLwR~%>JB_hRn)~-_sNx=rPUpA5a@r z76{4d26t|OE#^^o+g?cmW{fU9zmV{j1}n7vLQ(0IL+qbN_Q*gI^(v)~#Q)6Y!QYFcNB4 zG~S%V(31wu^IKkLm{`g*niDQ3*WBE;pR@+XmLq(Rs{WZGMXixdx6}t;V>|-^D3=EU zR^7-@kl8A;fAVg{EyT$Vwq$!P{}G!a2_cQmkoj&Y`}ACefDv^{E3$zb^0XgvXy20_ zh4i39iFk*lYiSl3*FXR2i;Ssc1|bS=E{b|@vsso&OZAAJ*(d}^cQa-%RA`S&Quz!R zBQcj=$T-zc@OZ~;@M}1+e4_1P+z}~atjQYO+aR_`>9rxS`1hL3cb=Tl4PMS!5*V!$ zZ+E+LrmfYi#edtVis^1&TgU}A2#hz6XP}dx`n+SwxCQM)uQ^5pE0S6qQE|X+05~N& zer%2CZZ}|~;;+0kAu*=#sD!Qt%?%YKRyY%^$JSrg4NHw={~J3%k9u~QYjVj>O4Cl_ zeMS(>sZU~cp=&m$p8HR(wwOL_v7$9mv~*m+GoehgqjQH$9BD!-%cI1K!Vrh@|NZEb z8098JFk9JF_+$TVq6n9`490361=a(uFSw?T-a@M|A@{&ZyeTeCK@UX#?YrM0H5PsU zdi86GU#_@3K48Qw58+vs2yhlcVb-ti-@czaT@0Zb+{|g^>b$aKHcevQq`W?}o!NWv z*1r{fMw^XT;*F`%01PjRIT51yN5GhxWPk*J5rCV7Vmd1V4<0-4FJ~>g#)2i^G6X>a z7~hB6PK8MV;$}5yO0wN-fKF!YE9e8slV|@sv;X6me4$7dHYsr~6q5zj4NAes@b`MlFJq)j!pQ*fINmFn=O#~DyASto!CN$ zxj!NiSYmrM6vToP>hLQCvrPL-9AXvDUfkiFb30-j#Uf%L3G)(NvfhqoF#!CSWLaH+ zMVumM5=SKg)*={uTCpibmf;n|$s$~C1edW}To~Am&b?dIz}6&*5nG*`BR0Ysw{S{n zL%;(ZKOwbrRiQkpQ0gWG>-tGB38Z6^fJteb2%jaed=N}rt-~j#z@bADCjrRqCqZL? zBOpadcwsPaycKW60w3Ec1hc^#yG_%FE|7+#l&5EHQjYEiN+X0~KnZYE@<;#9TMfvp z^j3kIzz2#hzyO4+x*W+R6@Vn{|H>HrZ|X10I5x1+0O8r1Sh8eCwsl?#Xg+yrVVwC^ z0U^E*=iLR81tt`o*mqJY(BpHI7k3qw=BWvnvPv%75!~bCNy1xu3&K})UCxRQ7YXO> zDkQFF6PAeJAc4d}LyZj)y9lHaN_i<<8A8F>t+$krcpHyhf9805uAC?kpFLW(E(K;V z09-JX(AE3k6+Td8iwxmj@l4kbNlD5}aYylAQ^hBQhu^mg|f#5YXBSC|v zO6=G`Tw%ppfvlW?+39f0bysmxLbOQozae0jK@Q1x1umP0n&`7l#Q9wqFoY@3?q=#9 z>c{Y86l}g^vy=qHb}g8kT@o_{nd=l378EizE#uA?vxr%2JdY)1q7PCmL3)nFUoVZ0 z#;;Hi=3K4VqASTP#K$w>pf1P}1*aa8$QrTt5H3NF->7|+1sl%n9{Cc)4 zgh9fr*kiR-8;5YT3P~`Zw5kp~Q&dr)l85w#K!xHEmD~^S6{~3rRb5-)v*`%$a zk|dp!g@OP1VHVMMBZTsmsvE?-(p)uuek;yX)Y!lRol|i0NhKc&h^y2xU*Q120DbFZ zS%pjX(1@{D!o-LxyoUFv)eEPOTz;==oeuUMvLa!U2ogbrZ_b&N`R6Rbk)Uu|$-x=b z3TKQwB=x!Dwv|?zn-ZQ$BDe?0lSp!31uj;&?7RtnZ!+GUa%B~(XL3?P7z6TxiJlCA zcm1Hd8aQpA(%VOv-z90G0MsEUHiayc!x0bUXPXJSZc7Aofl;~W*3 z=|V{;f}dIm91`W=XY0k4T)?ppmoA9fMJh2-V~{xM_t%sH6>P2cI3_n+l><8!`ry>y zEEay3?a_RV9F2yGoN8xx$z#r0oK3!y6T#dns!Y+tbA>pza_%(mV=EWj55NfQmtO;4 z(#GT9I>2^R?5q|9Gh~83{3=28oiPH$0J4N7)K;MOtKB9Y;7UvDO(8BV#90PgGgP?6 zT`R=y9j4l?s1CTYPDl{e$&=JF{*W|iQsPxF zHpi}WJ1{G@#7BvXFvymv2_{>N=8Toao&g)r*<~<*NS3~yQ8LHi2LVtxgD~r3$s#qb z!wA3wk`MzNv&S(v1sUKha~i_ zM-7vhod^mr;No)dnL`oVPY_l_%cFEs_Efaw%uepK2a-vXhO_XQti^SLQbHegb-#4z zstq;#MRbYL77Xv#>OpFi#P>b3n3D6AP^g#KR}HUZkG|+HSy+gp1B)45xW$63kh}6w z{qob9FfCG%i;3}t(ubFBOo~f$3*|fmWSas&f}DEM;+(6kTYeCh31#e7@t;nB1xb)B zG&{JhbZwVB5|OqzShh~#l2aZ&O7GNxztdSFa%W;fv9@1G)GS80*;kIsiKmFB$<~;eB>A4 zs*)x!O1fLhRQ5|Rca$uq!CvgUz;srtpwK!v6(hVWR*JsM=1oG52vVuXoa>|uL~p>h z6DL0|jo((9!gsPSHYz~mADl2J4Sdy8u@?DL7x-t=cp<6C%lMk~~Yj;bvdPXn^Jihj>3i=AQ!D8L$tp zURei2GyA0BDw!Y!zl>3mGgjhMQnr~y%nc@_EASzUW%Ht??p+{)2_Q9K#gh2wr3qtl z$noeF)x+>6c;QMZpa^`_SCWKD=|eOk3z{>SRG`kY0v48>Ff1Z(;@% z*7faZ2$38u<$YG<4oMF@1?RKBtw5}{ufwHGe)(HM%w)j!!PXuuxpG`SJ>_wQ5T69G z`lN}pjZPl_tWEyz8(x}Yz%Qzk%?*~i_lakW0luTV@Ld?SP~7kj$N(fR3aTecb3fBLX$si1cF67B+qeV8sh&St6+?flM}wMPZlvL4N?7%Lo@SM zP~8z6G5kt(Nz{Vie3i^X?U5rUSh33Ph)N;_lFA0m8Gx5* zp0nPUBr9?Dg+AmV$$~M_=(bYJG1~Qcr1ct{5qsNW14qchaYMv&M3?`CiSucalW~#- z0BQ3Vf@ymRk&iidko?w-8JJpyx!uF^aJ0u^y~V6e<6{%feM+aO8t*k<|Li=(O4v<>$bE1=?M^g6-6cA|Qc;z(6F_6neONom9?_Ot zA00R!1&LW_X)U=rr>BD%`O~vVpM`J=E28Yuqvj_FadVJV=Z~RIm9D2(KY9^-CknG^ zeii~hz79aXS92|9-q#&$)UX(b*3x_`L8IRfe_!bq2||HuD)T>o`rqZ@EzKC5!!>%Y zSsRF8p+7&E5L-58H{&)szMhr1j1FU5(%0hRtLB&=Xj?bvDW-~d@?Hhkg#W&~E}tP^ z@3Wh*Wi|T|61+Va!{{TeukROv_2@0xjJ7VPonX*W0%WY{XqdfYNOm}O>Z7^_|NAWO z@c5nFSlDc4ZW@9Ta}7?TiGJDLF13yyGkHKl${-T3lBUtvEQ$QFGWKn>L?S#LP+;mr zWh11j#BFCv@zp*?ZihBMO|1>7t!E5vXb%&Fi``AKBJpnTsbhx(*Rtl@Sl0DLtu3pv zGzOnU8@u@z+9y`f4jnj3Xi9}({MnO%^;Fclz18zV2uK&EZ=cCS-gJ8{&R zR^2WXig88w!;sxw%6*Q1z4mkoyVS(w0&|Oc{_He6m(O(=Y$GMuzypSzyzZi>Jg>$z zJ3gWJD>6{h0d1%tWD5=J$@XqI6KzyvRpR@{|0MfLL2rIu)RcR-zJRxpH}T!wm7ygjJD2qu!v#0W_ycOHvyHaUp~+_fq6VE_ z8 zeyq9BOYxKzB;tNg&S!e^?go!{JKfv!pfPZxH-^~_*Do^$e{KEa9GZnEDP_D(84^6j zDHB&)>y?B75p@*XSq#i6%+D*lz}eG|gnlMLrGU54-YkrHPt#A1>jTX^YKQ@+rdfyj z@I|b&{t&AM5Y`V1yJCrucV6#_90+7%H}+pcFn9h&Ma?E6lcJKCP)F^H7^r#A7bU$0 zU6JHL94yx;`2wGH31QBEv~}PiEntoa6v-KsE)+#{KN8o)Q1C2!=)0b#dYQ;(R&xKy2iY6v-5eVi}= znz<$*_H7*mGWwA?7%(xk-U$7xu_}1lH7kEI%AMc#=;>LWsif>(LN{-x85^D2R`Xs; ztTHbPxx0q(Hdt=O52$Vqnz5uC)gZNQX3JS9$~h6d(Jjvt<$4B`m-45g~e7#KUHqH=9C~6Re$kh@9xWA;4v^ z(}k;xf&%o?Jd0L_2;w#0=cv7x zGsGgNNtb?+tf--f1f_M$HizQO?%QGArm*H}W%Lf$MRMbmTBa@qv$lQKxJYq!#@%0wD!Raoh#ZEYTUyq)#K($Xn(nI(F&n;f(JaCKn$f zu}gzd**)_oXeCJ#PU@+mb*c6w#>n3#p>iZ3!y@^E#wzLA>ku;+8e-te-aV`KhJpR5 z8IgocRRjxsb^82CKWVTO><|a7$exIO5TUe&3G9w5{ z+fJP=F6+SD5bHsUkP_<>4#J1A9Ql+1`lYI=MA|i_aeh(2DvtS4X8Z{p_jKb?kenXO z*5XocvR6?}d{2*&?R1`=n+}*St-F}Npwct>_U2mRk?qcJb($Hr;Uu_yug`NOekNmn zRSKhjaLxt-EEA;mik3yZeB+gcEytj)H197Q6Lw^%M zoR#hT-MYW&00d=pBD^dTSr6U~MameQqkpXKM6Ht=tNd$0)itm24fEnGc}PQzHAPn}X@ zp>dHu*e=`gB7Z7(a_F~pk@NTGsu&vFQVe*MDrSE4nP%<~uepMgCO+FGCUkQJ0Z7~H zuAKd2)4{K;wLQ4%+eSzJ=Uu}(t7->Zw?5>V?b-571Dmhj8R&4@>DI#kvG)8?6mz?w z-1ja>S}5$D`Mr2g7LBniv8Klo{nCw?X3Jc^&3+D!g9|CyZ(8Q#xw?N>_FBm3Ek_IZ zIIO%xnFWf`m|1g$rFLyg-bOr;5l_uEPr0+y;q3XqQ(W^(fc;0g6H7Ywbz|)uhR~+W z=)cL1=pPaIpU00xW6~K6z^PzavO3w9UuHL^iNX@+RVLanSJZ-ai6*eMAl^uOd*e!+ zDBG4hRR|7Z4)QUO7|frhCO_4|q4j_M7?HCJuPh_d*aRBTVbM zGHG+3Il&LcexwD~-S@d`UpledB3K)eBH_4{%&fJGu0ZL*GLydjG2Zn)hjf+>5kUw> zSMeXOU;bzD@}bJ*Pqy*BX|~(~9)Q%C|CSk}LrsR#mN7Dw-kFI3BhFQD!Yxfm7mm^= zWse^M&mLJ^z{BalT7d+v)%q9H!}FeP50rg{0p<{s%g}mWBFv^Qo}y^Gy%fx-6dr() zc{$Sadte_JLkhH^wbM>*)R->zWH8rb-Nay~uD#n-p)nokR?dMvZ6h9pF=G21K0a~y z^e#QBiwCzlbM@G7VkfRd>zN#pxh`wgeL^TS8gao|;SI~P!6|9z8y{jeD7BW0&-!xCfj7DcVC)Nf_ISDv)mBG_8X)GhcP%i&Ln(}^n11o#hW$sQ z2Y}~XS*RK$j9U#N0IU%Ug5VC1if%j9!9I0B)&7L;i@-zxztiWSO#-|q zVHv+L9C)UQo!&Z@X7KskryLo*3+29;S{Zc(wPX#nqvROloOVz#jE8uPlDJ{q`{z+|E%93x*qijE|li(iXnoHxo z6+qpRyn)g9H`#);Onx8NJBUvoT@^D44a%B%*}Xl5%}Yiqewb*lFHd;0?tWD5vs=y2 zZp&pEHCnq?)4T)saRP{6Sa)-OLSJ`tej~kxe~c%{3aWvva+%iKnY7qfd|D5ob_Qs0 zPJetX>>CvBRI-r(h@4ixW*xh+ZTgsRGYIJ7*wr_S)4I#*u>5c2~GS686;o#XI|#oB7qI>BC$t zF;N_IcEsz(i1!x4s_il_7%(^I0h+_b=hxU=!7@i#eAweznb}^#;k|Ai5(idvj&RQ> z`@wJaQQ7aRHyq~`cvP8V`xzy{G{A#&%NIsp#qe|R=vEVWjZ;?RaThKP8blwiZ@~4% zw=Il-!vwgtmbSK2o+r+?ow(+C!m8Ir#Qh5aOa{c>IeU-_F>e&Bso@u8*YQU+yVKu> z`)Lgv+0;bp5I@e5m*O}m8;y)x9jy+>S)N#ugkJ7u4tlTndZ_#BdfA!9FaMqcTf!); z9ElP%MZ8!YdAm1qOH&lg0|NT#HOU8`y5rN{XTVWt%M?CKz|JPX=X^aD z4jlQKX!0%a#NnE?XG66YTRy~09>}0`4fwK+Zr=Q8>&+RtYxb-nYE?u>M`xO69 z10xv5=Dc2e@cs%%Cqn;R{-dSBfxRC|LGaU6K1ck<3Ad#~HS76xCx;KKcv(S7e&f{m{ZDN{JXSksLVrwB zidkdNPJMrWx?J{#0OUu&t4G&`TQc3M7XvO%e0_t%m*K!v{1a9GEKfcptilSXX63 z;mxA+92ls_)yR-qiR~3&@QQ}6lLXvv<*~Z0>SXzNjbA7nRsehUcvy>3+7EPk{A)hyST~*d z2GfJ@kt1(;IeF2+9CLq;J+Gsuu{|s;kNUx2wRNJr2={_uv%%b17h(H}2z{HOm{}WYyxl?uyAofO3Z&b)}mU%(v5FF(MIg*PCD1Tg{kB z5Pdphn#`qg_}c8m?OLNttkMR4z*ngjn_O$+{*kzD|+`^Kv{o3rYD%)Uj`SD-aOwD`_01Qa%s$vI(#_Pyef!9I3l~OH zMrPp!;w=7l|I;E1{*Eax&5oP1E`0x-_s>7S6T5iXlO?ld;uT%Rg*+g6Pr0(Y!?V^Q z8@uNdj=QoU>I&|6ikJ`hfAIu)igx)%*`1ztUZ3|!xpqc!n`fWVgHlE<(9!JF+ z!WIna{^gl`M{dKd=>2~!-HBgJ`~L^7J=1Bq4-ucP4v6TrSt8`O$n#|4_dgtrYrN4jjlP7i6DhuJXUYO{H*W3uG?skh^QD1(DM0-hY3PsfN44+f zzxS1C;xTfHmREwV8dx}yH`Qlsw=X+_r2!=C^0lfrVYOf>}%&N}BF^^%@k zvNez56G6O5X?K=7DjDtsvp}F=K4HJKu3*9{%w*gI8sf{fcCRWr<%jees2nflpU(w$uwHf~OjI<>e9w>bGrI|M|Gxx%t|zZ_?21SC)8R^^$r4-X#Q(PbmU(v%~J4T3&`H907wm z@VgsaJwF!RIfL}TX@E`IforuEAyVsaHq)zi~2>`7Yneeo|Q!Mh#d!P_OhAk`+npA6htD@U~PR#+=thZS`oc6751L1*S z_XFP@zJb52=jT3*`?aJ0%KftxSNrur;Yv#6pVLDHK}|33g>U&VZwBrKa**9Kx1i3u zR8$6zAtvcQ&ThSTcLYE_YVR3jml5ADf6o879btb7NbP)UlP)ct-9OXcGZ$NMyF0+l zd${C~0|C%YBR!uleffIRtA)Am7BMFTHg7@*wIBqxP>eunn^p7@}>)5DKNUanjn zQaxMITjjAg;ZC7f;cyIfAtgJFbM@xfLzeh*^kAsl_NE6%kZjUo+q{g8v3|#vI3L>P zV6bjUsZyH3^V;9s5lBd%VM6Z8zq)VKc0x>DxWr`o!WZAOm+b#|J-N8e#Hg_-=8w`% zxDluA;T+{M>hJFz&ZT_1yl7d^tVbQSn-cFHUV5JfO*qF~R)rssHoIR4@ufIj%J;Zl zl>BVRrNF^slfrCAyUjD)w;XU^n?SHuZt;^>bh*(RjC#|15EPhJlK8mu;6Dk|W{qUA z=5<`%_~PZ9WxiVSwIF)l(;G`NQ>3iTv?ZLv?)wj?NNYcXRYkRQF31$%J7s}Yz`UiU z!ibYs?J??%=8CIH3|Q*%ubtgG4Chr9K;ahBKEdm7Z?5-1jkQS8B=o})eGvIypfjpJ zTpSxHC%UYHD#i}xCWvA7!1flFmuYSC{h(@=BO)A3?)h}HHsgz9PjBFDM=tKe)rihm z?r>~h?mV%!^jhS7f4cDck<`-P=dHVr&J6Z$5)k^{Oi-+zGa?6(6E(2$;7IPK!Kzm- z_x1sm4>p#X@cr)c@eO@{!b=#a`N3exuYLnuzx+>CwCCJS=jU579zI<1%hvoq_&vHqhAtGl%FSB{^$91>|zpsWmm^zZO($V z*4Z%TH>@jD-NZ<-wRT6c3+6mX$R{U<_nErjD2Gh;6XT?Z2mQE{s*qfv zX8DGp=&x8+&X7mktH>$b*^$K?wnWQ$w=d)s>;~?)dq@$x=(JQ$zMk~LgKK&I{l(dzy%a*s&d+#HRbuc# zCtP6c#(f_hFhX?e-E*QDICtEPT&+?HLaYsCi!<0K6A~WXy8BzV3_{gLzlax#sVK4{ ztj-TO31W3GeDpQ>+=kYTc>qNzq%k1(F*(4Sm?^%|0)lTUyfUkvGl(%f71x09E~zhj zR_Q|5G&w5uzMJ=%Qy{=0q~aAfXH8Pz+==bhth0j@(Vbm(pYWD{B zcch@IsQ^b${a9V-vnU^|@fnqyHqO{ndR=(~X0&9lsygRWSBMZ-a+*@wO3P-SBk}Z! zs|34vfj0$%62fl`NxK=eKGf3XLbB4P@+6Ccx2@+PsI6tVai$6Y+J1vc~ zngFm_wJ5jVmtzDY!p`FciA^9_Gj=^1&Vp{{X}5Y^822NL6?w~aL|RSl<{!ZB4J{hL z0`OaW_T=78Ko`i9O9js@Sww95Y2(ZrHu`>>xwpUgJ(M>?f))Hbw9oSOu(Wcb=x)jz z9jI^b{)$Os1s{Qd*{Yu7Ee4CX#-ozl(=%O@Bt;%38a&4bqqm|3Hc}X%yuqrV2BwP; z!xsx{6B8@T+#C>GQDB1V$0Yh}>@V~4G97iw(lI6ziDU8gJ!vy=>Bt#h-jbwoZoJ}( zJVpudzIVH)*(e!hKyPKJ&~u5b#o)Xw^+pH zRBW&uBZ4gwoAf7@tJD6fHQy0r*6f^jq8)GWj`u3}&!uG!LUUgK_j9*w_AG(r*%X2- z(ZA1;LKDLDPx#ONBZ^|nb8vM_Yc@rjwK}gRhhswlsH~0Jt&=`XE(N9j)e=yh6~~!F z0l;#MI%!QXJ6~vt>zI;BTH7tu;H17dW4Cu}dMxQtkc7b)%#JAZINcBB;2=0Z7Bk1$ zRQ%~b{HaJp07$hm`=jiJviWip2uJHq=X20Ssw@i(z~dF5RJScl;{E)oVR=K9_pCS zwyCGq20HrGoh#rF!MTNM>K&NrjYiu@Wv_uKBSN$MjD9g)^L6`rzmQFmTL81mFaN? z|5{^^iEc8d!$OD-gCK4Yw6!xADlW#jcyA;LA`1v>WjO`9l9oLlhD)Ke}gCGLWz($H8M+o8=U zYUA4U4jfw&jp*~zq!ATYI*~M>;{#%9bP2E$W4Nn<-5O}S$}=8iH@|_il}6ePcB4uj zcN`BbP!5Vk+a)|}HG4oyO_dWpRbc1Z1ilvMuMa{FlF`}JtlhNIyWiVX-wwgwlTgwk z6;b?=$kF105mLE|J|X8IprA(c#Qo-dhXoI~=AvaPFk;-c9)zM{0LJK232o~Pk-3E0 zjHlS>u+}^_LsdDp(5gwnK~0!7Dj~G_y!b;0pB5X+)hLcK+!eV#(N<>2p(oXaBknfncsa*zjU82d4jHFss$fr zZKK>7=wa?_qJqir_!)B%O-(-8NPL0vuPiL;QgXXceAiv-7uD7ec>)}4Fg9t`qvUpI z^`kScK?PA>nGdN21`1j*@L5k|^r$$=nvYehO^cO=V{%H}8g;&w6|H2xREoScj3n(q zmI|_Wu%Ku>8L*G1iZY5BWa-8jzOCGiFVcEVPpbKLYSuA?1j`fbw4{?LlcqF`ml(N3 zxJ?a!qAg0UP|doCP^7R=&uhwkgcBt(I$5^9Rl(Y6OH0yi9hCg@mmDA0Wm>3&P~h{2 z3clU!ZMT%;Nw3DC21it}q65Sq(wZgu7_oGeiQPZ~$_&VYtQN4;)R9tP8Ni%()~Zm6=VAba(jWz^0V9Oo zCp5^}!Ajx%aJ!yzpwIr$hwGwc3aD95EKbEGp|m%0gLqJM>#np-E%4T{J2A4iisGTA zywVz$D`q*8-VcR2NR*&if%6rOVHC1RN-io zQKK5Nzt;9stCdP=cnc-M3-KpaoI=T#ex1NZ%*=+5H9rSe>g(59PK?sXexuKbMwBWs z{0pI{!%v%YaBJmshM51C^TRL=bFIqLT23X21t0cWbtrJ>upcNE(5n&Hfvj@**s^!T zA4g{IpYe39-SSQiUnpj*#ZFN$!VxW7rZhqv!$x(Y6g8(u8}u<&XkdIWO`f5QDBahb}0y%iJEKEOpz z9~28n5~{U!AQGdI)I18u!gFefpHfLnHy{NeAd77*_{;Mf^B8gvZ}!*DU7!&{7f1lZ%mhwVX7K)$B2o zas|&)$?ij_Nie>i!(S>Vmt(X(Ig6y@cuIIF3c+s*lVm<((O{bVDB-k1s8Dci)X>xi zgxRkBwo;3)KR0bLB6=(5NHv0%m*yi%BYz!hKdi%{U^>9G6ARB&S*NRUK3ZXe@&p%Q zX7gO6oJHFuGOg0cNx|sjL56COrTMYZ;#AXZq>j0%|WWH9$com^{RzR~-|DaLK z7cbw9vfB1~`RdP9N`pZad15v&PfmSwer|ZSfFWn?x8mVYj@cH+L2$`kge=57tua!I zob9d_G(=hSD2-BdhFm3UP(^P5C`kaZP`@v(P7rA`_I%4Ism_Sg(?D|S89C#XmhGhB zl}e1$gG_4_JpDvhDkl_I5RSl*-D2lXF@+)LywFUU*yuvv5nbi2tv0%KGjfeYN=k<< zKu+~zLIRwaYN;KF(y~&-3&>V8pO?(!UG&8?{Pv-c#z@)(W{{#0^``p`Ym8RvI3rq$ zn@XxwG3_Km!V;@6iP?si$Wv|le7yVBZ7YY!;@?oGzNDV>I6dvQa2sp1k8ww2%Gx?Fhp}$7hV&h7Ci>RssgbjQ;L+MN#}OM$gdZtm5F~ zVQLq`HWTxk8ulPYO;NQayrKjEBveIh(=uM6`bwUmOv$gSF=`SY@75&rw=bmJ*}LWc^5iHh5ie9ncu1Yq$;)&JT=)6R3SoS%Xuslc7Dkx<5pF;xE8FC*t1n-OlKY-5 zIhEy)Pz|I1AA0``*D494F8J&vQ#A{n?*X}GKz&lisxb~@|jq=EH*S`G9w zS1WdmOzqisgBfS)uA}cUN$ZmT6S~qYL86XD3^NWr$_DBDWX{tL>(={s+D%@E=kUz5 zgjcP;ZEDuS-^VqFEIUm>KEh0d1m5R6Ca7B+CdKcc#n=3P*;Ofc{Z`toY* zh*-|z&YtkHFpf-O?w{x7t^-50TH=%+I~O6oEHfUc>PL$ zpyAk~;1AWa#8?xG;(4Yq9Pc2>`%{Jext|_ zH59__!5L>30KzLxPp_5CSu@80Otssaxt^5=geR@nk6%ZM%yfRN$X+~Q)L3oaGaK-vIn-k!e#tNKbBTX;hL8lPUoFn#; zl+Do>KEFh2zrw(4lk1N_xWA~^#ZfZNUg7jF%j~mij##oIx6hr?cmG{`~vP z0^dbBa;0cp#kIGsga89`NLv{)dvf}qdn5rN1$~`MQG3^U!#)mBnQtKl9G20%!q&{G zShw3RFt$jK4+Ihkfg4NW9}e9^acN0$v1M+fh0k-M6q^aN4qV2U+2(KGm_u29GfhKk zf6@11&8Uq8F$%n!7nzouI6YeqkY^zon=VKb&{Ep zU|H{~;9qGyJxruCoYt~M-z1Kc5$ z5L1PF(`CLp^z)*voqXe!H=Z*6$)6RT+?3!a%JPRZSlFZ=O+ZRfeOZp_IXn6d09Vd>1vPq}yQ zIDdU#xTpjYGbF|BL$^N`6Q?1^@QW9z_$xM`1UnVTbDI-sb=1V7UGrD==XR&&*#R>* z_NymiDdykrTKiK_aZ>CQ1&7+&PNIGqoVF1K7e@c?7zoAq6yk5C=DRej>u;T-uu5m< zxhrpQ?6u6J(a#CUUc)#$o7#vBRf_9PAHXhr?@Vu%XrZ{kJQXeIQpANE9*Gb^s_r;yIp6@?sY)v~fZ-LmOiMN|AV`_fWmP$G#Q8AwPEr`5z%zbD zke=+DVp~~N|4kpVwb;wV^@*)}-Ekm>g@Xx`s1E;IebIc2hO&7hD9KT!WPSi{6@`j{ z%N0Q$k@xaE00k}iJMp`4i_#ot#kS9kbNqJmy4q@ySp{7~VA6(EG}oo?guQkRoU2E- zN0>)sXd>3O_~cBSTr#vNFno7iWLI*4+LTygSchOCI>j$R$fAq-MCBr?Bs3PBJfSnIj22Q!;)p>32 zb00m*UDbZXh@z?P{QmOn6@Koy^1NiS<*A22s_TW>;u;Nf5!&)X)qKzbptSoz_vg8_ zlFyOCJoK_yppw*!cFkOdAASwxim7ca_Ft1jJ`jEY^_TJP&O{164;FkpH#!tN&~7 zR|K>q>D&8+aGU?y`)wYhFg>&H_!_B_>Qjz;KQ%lfWI>_9u@v0+x%L0@d@VrjgUvHojPh%Gd3%?DZ#=W7mVLB^go zt2^;L5PPy9{*~U!<(Mkz7$h}p{%?J1|G)Jql=-0kL)(g0$Jwdeo=yddR6g zx5hwGF#Ah<0WjAw7qj1%5{9Qvx;-G(_$hb286M$~Zj)k9}4UHe#O zIH%(&{JJIAapL|;H~p&9U|qjIkW|Z!X(uo!wTG{65TPm7(mz`41AqH>hxVaa`z|7= z3L!*83d^g_l#D!Yn}H3xrscBiCD%ifAz&_W6rYD(y0f8tlYtTjp4%1hD*Ky@QTTNudo9GSn)z|&H?r!@V= z22R8epuW?3YT=t}9}hbyWB={^R#V^SH_Hee6IfC!XIIeEe%n^y-Zgow$cN{@``5&} zf31g7Z*pojm9CojVtpZ%Y6KbdD_A`>w6|03Rk(?=RjIZ6t8eh?J{nlG|N9U7ZBB@% zQZz4>^eg}+CZS9v%U%t<>E3VzWP-^0J30g7DCip(_`7ZArL7RvCWMi+(P&PBfFRQY zP9zT+eK|x<9+49QRxD|hY(0tQBo^j3ehZu; zInan4hOKPz9=$Br!i|6c<5Xzd!zH^eKD?dLARRkqVr~>mZ8coV^ho@I<3aUTmQV1UrzYIqjKg?RY(AUJF)NmL2voSRYK{r8sJD3F42pQ?x#m(Go=2sm<& zPLOTt2|D<2&88*@XihkI2Lc}_9{huPsGd}RKz?v274+3+=}sJaR~x1Hx;HL2>J z7EeMb+%1j1!ADLSlE4ar&yBMGSky_JaLJKy+oLIX#wZRYx}7U>yJ) z=c(o$x^?oj=X5<-YlHv`Th?z#WTrzP2_x=(d-B@&sX3onO_;TH3uPc`!-p1HFl3NF z+3?$V^W9+cfk6_-;nbOmLp~S(=jNVCZ5pJV(b3G_qqJAKz#5e2XiqMgZ<=@sAo2Do&U)tBHFqSv(lG+@9ac#s+=T<{T{q9@A1>-)(a zYg+^*=WdHxwU_~+0>2Yrtf~uoB&UYUSJ)1ci)zo!yxrO#&N>Q{qBXz*i0TsT{{p40 zZrMar5z6J~XVKdv2Sj@BIBXCAF;Icf)@RLqjnXp_yj+3bHmD!p+m@7E$o$08Op?72 zSfC~79p#@_=KRl5u5e3K(NbzJY@lCi{KV?VsA~ZOPzHv#P&(wEDZZCtoym}e@;z8LVq1ut)*T!7C0UdifKQ8&N@!w|qBl~ga^S2XiV0|$crGLHoe^`2IlD;G4%C&b_k8fmYcfK$c-6u%53*JJc&GqG6{UHxkBs|c-BPL7f5`_sb1zMwgP zN3?_(6)6Lu_T5b8l0?Pw}(pu4ASkQU@k^ADvKIrQuV$gvR7SB}@O0d~Lhpv!Px za^jL?8KoYk-;!OP-Q2s5A^teXyoWF@VYCK>ny(_Kz@!K{!D|w?<0ojQ1-XNOqru*s n2>_h{Z3l0-0)+5EViH2m1*r9MS{uaZPi0>2>wRYg0bc(H;H4@^ literal 0 HcmV?d00001 diff --git a/weblib/tutorial/chapter9.ma b/weblib/tutorial/chapter9.ma index 6126269d8..c68c8f1a0 100644 --- a/weblib/tutorial/chapter9.ma +++ b/weblib/tutorial/chapter9.ma @@ -34,7 +34,7 @@ lemma move_star: ∀S:a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)" // qed. (* -Example. Let us consider the item +bExample/b. Let us consider the item (•a + ϵ)((•b)*•a + •b)b @@ -154,10 +154,11 @@ e. This is one of the advantages of pointed regular expressions w.r.t. derivativ whose finite nature only holds after a suitable quotient. Let us discuss a couple of examples. + +bExample/b. Below is the DFA associated with the regular expression (ac+bc)*. -\includegraphics[width=.8\textwidth]{acUbc.pdf} -\caption{DFA for $(ac+bc)^*$\label{acUbc}} +img src="acUbc.gif" alt="some_text"/ The graphical description of the automaton is the traditional one, with nodes for states and labelled arcs for transitions. Unreachable states are not shown. @@ -171,10 +172,11 @@ behaviour of the automaton. As a consequence, the construction of the automaton only direct, but also extremely intuitive and locally verifiable. Let us consider a more complex case. + +bExample/b. Starting form the regular expression (a+ϵ)(b*a + b)b, we obtain the following automaton. -\includegraphics[width=.8\textwidth]{automaton.pdf} -\caption{DFA for $(a+\epsilon)(b^*a + b)b$\label{automaton}} +img src="automaton.pdf" alt="some_text"/ 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$ -- 2.39.2