diff --git a/assets/c3po.png b/assets/c3po.png new file mode 100644 index 0000000000000000000000000000000000000000..83deb495c65086e2c8c908ed3e57b063868c1123 GIT binary patch literal 33194 zcmeAS@N?(olHy`uVBq!ia0y~yU>0FuV138I#=yYvDJt&@0|U##%#etZ2wxwokg&dz0$52&wyjcx zZ-9bxeo?A|sh+8xfs!4Uf=y9MnpKdC8&q>qN}8=wMoCG5mA-y?dAVM>v0i>ry1t>M zrKP@sk-m|UZc$2_ZgFK^Nn(X=Ua>OB2#6Ujsl~}fnFS@8`FRQ;GZT~YOG|8(l(-ZW z6rhHuR%9Yf&nt#{KRG{FA0(r1sAr&$th^*M4To}&42JT8jQo=P;*9(PxCc^8uZ=jNh#qqxMitOUP~;*iRMRQ;gT;{4L0AQ`xEU@4Frb4o#x9GaI|Vyk3?FfIZiXRBmsrf-Ol zio_}fj}a@dBYpEzQf-xt!MYGqp3cqzMfqu&IjOcvE}6vzIf<2E6&1M!R=)WunQ4_S zi6yDFN=61oCb|a3x`q}Z1}0X9CRPTfQ3!>pC5b7CC5d>H+JVxkO+{{judkIyW^qY= zQ6*RilDLCY3n4rRHzyOMT0ubp9Jf}9$)EtSRVpaTPbp1KO##~rmo3guD=AMbN_9+6 z%`350a!gCh%*!mPR0sg2R|P{oLjyfCR2}6Rsd+ejqz`e1jXo%g!CYmdkKt~J0;D_% z%IaWEK`w4~TsHdPA^}u9*l{7soz%P(Tcsi;d%JT-UPdx7@OWoBI|o2Roq@rlb7^>a zOz=sudC@_NEF207s$bMR)ElMzGO@GfM&kgYSa#kHtN1Y}^?5L0n?b|Gj(nGOkVB{YvBdujfDh=R`3jGRiZk zh&^(0WVDxmB*yUJYfa}C0fr>2C%Vf-yq@e}Ns`s%5qRWfc`oSD-J&@QkEn~9b$*oT zSkLGX_Wa|LNQR6Or+JY_&No?=?2J#}=%CVeLo(_ApFf^V9jXGioun(4pZ*#tdH-d~ zUti;7kIBbROC373RYS@$B1GZjV_)eQbx9UxK@A3>3G5XK9smAE*Uihhu-x>`tDBcT zR8;aM$mKuv>za~W+EIN}@}i+Yw)3Ajm4F-0JwcmOA9{LKU+IWH&}hk0C1A~6ad4u5 zw4;pHx$eH8kCHPN1?Wu(XLDHI#kI3j;I;FffCzy}3pU-YkTA#%h)`qM}T1Te2E_#yDVX9E3b;7qJ(lm ze)^%S*eBj~xM|9-h`?ngCUL3p%T{?w@Nct>KGGZZkh%3{=fhKf5_D_kDb?)|TNA61 zrq26{gZr2Z?>bin9=^bJvaiLuCJTjFy;p5@{CH}oMd&2))tio=ZLLf!x+jzLy=f84 z)fk(d0%9wI0M>{0qgdGfjFe@pp*>kYcu`5tfqv_9d#jwg!mYH1_m5%nrd=Pn5 zBfyy*#_@Q|8X0y7DYKefH;5uO|&h6@5&phipicDU#{93pw zCZ%RR_Z_LMst1lc-EvT@^(O`(DWZW1GLmW-{x!t>ib zUf^5Tyn92{t^?c`*zYy@b2Lp5kUHeRBM^LqtI#1vQ0!5Ei$b7>&7`g+%8?xs6BUgo z{PeKg#1z?{i5lFgizj9%S;?Js zQeS*DgL4qA_8$0rxq*-6fC)jxLqq4meAJ*@k??2r8Zu%1Qg zV8;W84~hkx$sCa_nk_+2tclhS1s?L;@s4fT?xGafpW*zasoHSr4Cgt1F+O)3?s(gH zzEQAK`!?A_g?SS5$$k;%M-#a`moC}5&-mx;f>I7oY0#iASGQKH>VL z_o?uc=qKY(>RoC_yB;}rF67X-tl_PBTf=wC=_z`r)K`gJZF}YJyX0BG^C0b&rB{rv zR9`XA%F23{buX(hOKGcR*3_)uSI(`r4f(xb-P*kM=K|%I>jlRz+UNXt$*pR~;e_8ki{!99o zt4%d$U7IE2JMWp!S*^2&XPKM+-YOBL7iAdrGpc)QS!V2oSJ%`sqqEyHxVLz3*`783 zTHTog5@I}j&F5#Fzj4gs@QX`|uWr03C@m^ERr>A4mX}{%X1(6^TJ5#p)wP#wm)&03 z{xb4);nz=JroEEAuzTV6!Wkb8z8O5+;ClE~Tdd?azxo|@3-$%<_o-k1uk>#}n@_Vq zb4>G7HeR;xyoJuyhb<0kwn_7zm-xnaUGkmv9Q!>vKN=sF_XH?cFRobp(k;3-s`po~ zZ_nW#)nnPc{?gxPy_m@|>&c8YMwWS(l1~|YH5Z+^&d4_L*PNB7Q;a{)n0iJmZT`%O zkvnFd$?1-qeN(+y`m@UC%4gMQ-$w`NMu^Q6Tdgxo_m_^Zu6y*k4QsaUNp{_s6qy>m zcB57L*K@aySskrvENw2`-n)H!bdE-0Qu0n@S=!t~t8q^F5aL3h!^;bKh(K zqvDsyFPRTNFJHfCe!YBp{&$VpfrkQbyV-s-{{Hx9?#I_((tj=go&W7Uj{)}s))00Z zt}PrQEP4Dj$F?Ou-%!3ep3Rcovzd=|@8cf@X+?f)$p;e;rXI{yyrt-=_}WRXWmbDy z>$SFTt(7gl{MM3w9Q{1;a&?ol&pa*8-cc(UCupo3rF2zUSn0Z}UDu}mNp7aSZtm_q zahAX0wuEl6*rmvJq#!x$*q#2ZopWWXRr(~vrNc$Po7_{abNjQC#qH3MmRQbw;bx)f zYWI9M`A$+bRlhv>xaxJ4{ob5@krOXjrahT4Gg)t`)UvK1>B}COCo^wf{&l>qC)Rdb z_MGE8E)|*|yWKP2>fa%j!6y=i#U^(IcxeT&~0Ep?mp;B&k0%(x@F zleto}vikGMpD%y5AHDS`rtq}NWY1vrQV$uGrIXH`w3{66|8BCI*LHCQ*2mmZ+@%lN zYgeBM`!@Ma;>7yE(2Kt{PX_b(U7e*h@0Qisx?77f&v!X@*U#+pf9{_@FVQUdT~E95 zP2=rnoYGRyWX;Pp+?`T(ea;3;>*qnwpPl=gJMZ%z(a-;8%{SV=^2m-9zmt#WAF5lW zdsSoVw0kiRb|+kRs#%zkcw1?^Yqof;uJDvtopQbP8vpmq*#G0vc|H5^e>NLbial=! zonIe$w4+0)nl-J@51_v@+!tMDOkG`C9kC6mHJ=yjC|c`qk>S ztF^ZYZ5PX}-KAT3duM#a{wq1=cjET_JCWfp*&Vklf3)ZR&&A?3dNTV??7C5K@^et_YWLR*@7vT_ zUwL*jtp4WfqU7D>)xpPC^gRw|S~q8xRL$2nrth|TUthew{Eo-2!q?As%$~cQW&5uD z=XdK$m%li-e0T9X!FN;dUf&b{@xTkmukXwDzkmDXjmH2!Me>ZQLFI)e5 z>X)krULVcpx%cMB>A&lr{k!pxJ^%Clx~lMR_a6K`$G?XEx!tmwns1q>(l0$frC%05 zYoA-)Uh@g|1_}>7E4%y|e@2R(J;U5cF zFREk;VBdfLan-}?XMGvIb|85k58 zJY5_^D(1Yo`?Bwj#U{3ZN`v?RPnFjHc(x?;E-dF6rHmcQQ@upC`!AVtoDno) zf{q;&_J_$cFhu{@_2ItMYzCo=nal=yI?P7{8dj9}X^!B3*WSc$E3eorO?_lp|FA1cl> zDh$>!`Ye0Q`e3S$<0JLQ(g#$mVi@L0imKW5THEfwF2QclcuuV0eHDAB_2VA-f8qkkHkp|=rAx{-pTYvw`jtTmB%+qeP^(`ypidRX7Gd`=dxHG46H&L_NMR(*>j39 zIKJ>;{1#X!6!&osL(s)WrYqs8p^rotG9@U^Rdobb5$JbjGKh2(xsoO`6cL#pu%Oh@RyKwv{w66uQnVsW&RpIT^&pe=Ib?+RCnB z#v;EZi+iL4Pd~SKG)3@$h?Q+a#Uh_+n|lNUPrY8Q^OU`y`y8J_ABXT`uE$O-MKvn| z<}u{Ie8G?uVad79M$CmneCla&2X%IV1FJmW=Os5>U^8go<4ah3b8^hzeGKdurk>+X zm^)KA`tRRjCfNhNR%Q*RX}&36KR@RvXXq`-V)%S^#-3OAZ*x>Jh`+qR@JvXps9-LG z-=&$1XN;>Rt@3|=-jw-=gFBnS@e`dZ_toeuWO~3mSK>g$As60t$_Ir1N7gbh9G%&6 zZQ&lqc^531dQ6o9UhKXuB`OpfuAn+s{D8$Fmsls(1OG1p2F<$8Be0ncNKf#-c z)xk$?x#ibAdE4w5H915WYQN0+!zs+LL@|KDAwEpAVeJlXwu1RrIp+oHH|RzzWY}?h z$;9v&{{(I(RtFxn`FoOI3kythU}SjA(dAHSWz|r&_np-1?$^QL4V%^kFfcHjz4MYG z<8hyH_)233&oB*!Ylem_3bu_*53KU+4runFJNh8V)(S_EoX!uOs4q8y+g*YSSQSLVEiyMSJh=%9g{bw2*ZYHpgNLd8@8};F)%Ec>A=XqU?Qx+ z5Vu)>?#y?2)j{!%sxTRYKK5Kj4S$%G3=YPPObm}cB$!R;b71^1r&E$)jzR!K&%?$X zhHVPqfPv|Rmn0|i&L&Ibiu7-bi64O*0C1$+ZznY(+ zVahz;C|1n|UQQ8)nxb!g<;NymtTMO%Rmte19Ki6wXML{mef#vUDtn%XEto%l>#sWu z(*!jbDkS!P|M&6dX7&5V^E5j|<}fT1(qNeJSK$4cgpIErJ_$X@nZVh|ln}rAKATC> zqrJc8>=V{$(B%+esNQAuai5XqzF#-v#qIZB|86(u=R0dh*9{C_mv=J$dHpW--HF=Q zQ;VYwPv-wTCwbrS_ipX$jteAY`3~$~<@fB|yz3p0LWUJ@&m1Xv_T=-&*!g|0?-sLPJooZyxqFp^ zOu~%+YwQ>p+B$7M{ww{oyMCVYlj2`1uWNBTWCU8pHh5^|nEx!{6YTrA@cI#}OO}7X zypxFzPrTO|Bj#Wjror&)q=;JI;`1L}te4Msv(snXFvWo};P~~4`aU*u?lOISm2Z5a zXb!{l3JvK6ZGq>-&hTmM_p5on;(eUtv3>t{%zx|WpvA=MP`6k8P`KI_`~SD+-JZVA zuKYsMx1DjEJ`9>Wx*0#L_bKnFZtIkl>#K{XUAKPUe)k6_0{%HDhG{T-dL^n>b>Fc5 zyR^{iwiH{VchhEqE82luZE9}B+PRR5jyxyw-f z@J=pKhb$|phWne^Iw$`A=AJXR>kHeO_hIu_Ki6#7QewjJ^N`E?@Tuqi{E2+*cdS@8 zkiYlyfdVV3hJV64=hwbo6<_x+^H__$*NPKW>lVLOawxBBXG++^F?m;{@L!JoEPF5S zWYYOQ|0+9!1Bb2i`Q_)MY&p-@tlRHbqkbTSiIw5Whu25{vqyL>V6b?9J@7N%$BxgP zQEs8FJUkaL6sVWCicWqW zdOb3L!An?!;hR~}B;6H^ISvaL5=6?MF`6j^FuXat#GZY%twRJ8E5q&;Li1M5VGn3= zU@W+IvvUsT{dDWQh4F>!tf%U4nBl-tieYfzF z7uv%2LGkCzDZ=pEqImi5*BP^Q=Kq}?S$=!DYpu5NX@Bax^dpme#>eHH^cdpa3Zs=#>YN$P1QJX!5^P}H$E`zBKj2pHG3P0?a{5tTs$j2DQ zWr7+E>sJ5xkhk8m@Qd|V+y3>((D!f6Fg{z^uEaKvg%p}>DG0L*s2fXJkgqE(50`1z0 zeW83eS{xWJJbROJVaY_fE6NHwjZ6>X!{yt)e$ZK5Bm4YtOBII>sP^y)Q*97|6ms_$ zGGsjGGg^B^b^(vJ2*cxNQE**BuO}3f*=HnE@0}f2A3_YqB7?yI1Fno_#%8-!F#L95w z*-uV|E&tcqF);K!{;}6<yu|9M~D z-JWM8y;W$T9m7LT5r&O>X3dxtu`d0$&;em4RtLUt_03EtDw~)N@G`MF*xPQi{c7~t z!l-4s#&y;OGL1|PyM3-5KOu01p(Kofc}Bwf*M{r9tzbTup}?vw!cfrLX?MWf%C*5T z?e4;DQkTNl7k+$KYG}ut`CyrnilRfJFty~t0BfG=5e8K!&*)e25_2FkS{;-xInkz zEvE>>$2pbUlR9-66gfl~3^_$VYSuS6FJNd8OFz_d|2DW@J(4<=so?_)SHq2#u8MQh zw!db|Ias7~Ktfw>@~oVs(&>Z{Ph$Su?sporSBR%BSXc@G=H{4yct2 z)XJ~?4xGl2&mqE4I+Nr6avnyzAMal=GbF4y-f}~_d7YpNgWo16#trPkPd+P6naaQc zYA(GwoSka_I?!%EUn9ef4qbl+!`fLB?#=vBH}}UM*{^)j``K#L94wev9c+x%e$QL` z=DV3cOz{edR@Q{z~@9S9}KwWtdnU!uG1qjXxguaM9D4^V5FLH4;&4 zC@G0yNba4rWn0a+P|@QZ*NlG0iKW{;j=Wj>Yj@XE-W-SLtOoaPdcL`8SNSZZtxlvbQ9>6eV(P8EjuU{Q0 zJJRKLr7-15G0)z*)l3UmWThP97JvJ6e`8V1Ow)_^OSiH=(3F*Qh}--9Q@>HsnwO<~ z#$l>a`=u33=1Mrk*~)*5`@8Fg^?B_tKklt~&Mz>Jk4ItqJ${b$^CI4#nZdK<3#e># z&{!=0h;4yHxidr2?5|wG50m&F8%^jFsu^RM>ay9H|Y5(rChmlD@gCR*!>D=c%j1CN-*6Y>gBQrbezZx-UcrIXA z&>pJI8m7r0Cal45t-CJ$UQ4Z>A}6R77NPAl!=Q5R^Xr0-XEB#32QXX-w>8+Yn190r z2gVKOPFP=+RKM}=9<$09aGh8#dH6_d6UPB1CRT@>{e8B~Obni&?C`ea`(M9`TPx=< z91_rAcxAYeEkUZ0NnxApVaKbwaq-9JT^H8yTfnel`Ky*cJsrYjj!YV7vy&Mg%)6JE z_}qa*MJ0ei;Nsl-OJ4kSE)Nq2w^DD++`v#U*?}>j`>j#^X$c9r<8PvvG+(S?xVGv4 zzr8(;2`yRIMKxU5SvQ28=Pcf87dzue_||M5k%ZI2468YKuGi{sUiI)%@ZJ?w_a;np z$nu33h!R5s{!W8UC5%`)uCsscrtGyq$^fEozb@lhf^zV1W&zB$jc=MZx^E88xa}yZn zX7Vt+U(3gDpBlv}QMqPff3EucblKe}jVGS9x%u{G zy5$$E_dTnH&vS?sOlD(vqgU1NL-TOiqWNL1UH)2qjmGLfuQJX4#nKy6mtcOA=?Eyv zIbXRibHa*m-Ml|x+`|0U*EKVqZQbaQI`i;huA8S`pV_udtIYEJ)v7&N-(Cx7-RR-s z4+*NgB$`?J==a7o{~R~3DxczhEp@f<^Se9wrk-NFx5DcSWf%NPh2+zzgphvmkFC6euIhCKVl(+QkR5E**u;Y z%kMhTJ!vODaov+sl8@Fe-|p}>z%9q)D4SBJiQwFy>;9Gh_id5iw7ZH&`<(iz!#8bT z7i=-C`hK-@e$@J}c~6h9tqEXI-XoO}&$~ph>BuTayF)wQCpKOT#qUbzg{n;rJ@;5EdclK$iH)y~{3JH7vpZw+?hJow{LgpR z$Hh~luWAWyd*+(PEpmI46XTqzsva(qbEr)SFh+5N8ZI`TY1 z=~O_x@dhoo$S{qD!1YJ>eA;QvJ7XsE#ZbY+M;`CLx$>M~^Hi==LK+G2f%n$$KkZQY z%tm>t>ucww_W$eJCfjzIlW*Ikl~I4(yF`{ZQ~N{ZyLG!lo}dl})xiaZ`7EvYpCyNV0s#{`$J5n|?2G zpSyK#=9;;$9(!!FpE&On$5&3_{G~EsVbMN`O(2 zQ*_CaPmaEu!_~@a3pO7wn-!ia{IuMuDtcqqwdCliBb(+p&RmmNIx}QVfP?Kl38UjL z1it=#AFVDvahuCbg@cuK4E-T2Tq{ytXWS?)UDUogwb(pn4VPG?Q_FMpj#JVLJRDn_ zrNaE~l<|n{z4yk%>P+vCbH++?*I&f9ug^HXO*Zt18SDSg^RKcq+!3?%F}Sw=@vqW9 zR>$_0zIv6ueGc=Rv@55L7I4qCc(Sd^`($6a!QwT3dy1C&oms`cc;EL`SKq46mc3nG z5~js*l8g1p)~cc>@4|h;-~G71w=FzeWsTbb+qK%Fzp~qeG!&L!O;oy7e)iJqzPCM_ zEUhc||7Ke`@3>LaX+sx_ydQa2UhiEvbGwbB-LyTAyG;td{}X*78ojD&*C(rU9mn~P zKfHdI(=DBIrwf;`^}h#KZx;7OnU(jy&iQ+~>~H^Le~M z_Y-8__Ah1O>d=p#VX$HEw6!@l=?s-Incb3kbrU)q7&p4|2(vBvQ)Q!{7|QhMqFSWW zf`%PRZJl@TYToy`evE&XW85wE%bX$tlMMvJzuq?zP-EEPvY?^DsJ&C;xZ$m-pU;G- z9b#da&M7kC{u$4C&(;4~1iuSadoXW$gUy%AKF`ZF6sE0aZuGntbxOYBZRElRixy6$ zpz{ml-p*Rb!qu_RX+}qd&z;A!ob=L<3*BDy!fQdpSFIM#SApjhrms%!3~)4OVqK%^ z!yq}c=h&qx+Zgv<0vZXjiA^i6n4Wm}dWSq$3s;`7hC(}suuU_cgUqj#LjoEJyv&T+ zdso*B9@730_ulZxj3c^CtY^|!3kR;u7P!CSH4Q?I$2!201(23QVLqx#)O6S~0)`WGN|K^=Oe0^_! z<5^A-gK2C1ToOx}KJ5@vTlZ;#*}BeZQ9Pl zC2{x_%fuV+SU#TR5!P+tiWAaE&=s~~IQPmntzur29t+nC|90*-4)NE|&)g(a%Ivk` zfmtKdwT)H>yz=2uOZu*QP*FRByVSCr_9?wrk0=$bWO?$R>QsGULlH|YQ; z*8j=@4)!`jfBo1q#4YMtKjzIKw!aHh+=>4rWP^O}NLxEf~h zyqVy=#o(ht$cKpzjNf0{FjlDlwh%OZBhUikW-wN$J`P)+ZnNa9HxugtJ0qW{4)?v1 ztFwM`iAoD7p_-(%>EA=K>f9H*VUJL3l|wQGX1()*q|WSY^MC; z{;!oG)8;LIV8PeOWU>4b1Bbz>KH;>5OpQ!p7iKbDeR2KV%BtdJuPO^CIWYc}2x=y5#^Zz+ix#@W8=S3vyqA6 zMdJ0757#~a+ZC`;v61Q8rHM>eww-=;q}+Pm=W8rnJKpDM2xv*1Jizz3=GFf4yn4Ay z_c|OH8Rl&L%rbLhOV<$=t{uz6*=OukK3n%kbO)QuhG5$*Rv%|R*ECZMaFDSIVpt`p zWu_3|uzT~|d+Qe;o4bnZIm3nKtDV^`U5{9}W<2+4UnR`C==YWBq3@5cntxxzDJ+qR zb<568R*b7x)Emq%yWaj_T89H;apY2l6W;%8`q%oqa*7n(y?d2&Vbi@U;%T>QZ(r69 zQ@0b=;u6weV6gkFP-gGsYRJSIbNThn&aTxWH~YjTyyqXVc5+o@VqFt#7{c)T#>>7v zS33=-L<=&p&e{IztlvbZ)^qm!*Sk2BzQ#XUZpW$`a3D&p)*)=S&$~5#J*lsQ8JSqu zq`wxPaCWMl=l`SXPOe2vtaFU3c25p))c)FZvussynEEq8Eg@kI1#wx84X3VOyvP1> zw}tZx53dCc=hJL^VjucVKPQ{@>f*M|U-`q-uLZ2*bbRej_1D?9dkf%eP- z8V~l0uJ1Z4pw;2~VsZQG=s8+nW5d+1ZThMy*~s+iQX|vin78qDe}CMcH~;LsmM#|- zu8Q2N{5NBN`p9Zr2tM6>UAH#j$-dLCTx6VFg``;bY%>aQv1&`_*-@Ax>u_~qMbxWH zt6xiOeQ)LbU(Emg+VYZR7as2PXnr^|Sy1EK1XG)srT@-cHTH=4dne<1)P1q(0fIA_ z+MjP??RwlHs`W)Tw~Ui#?UmL4+*&)e=gU9cm1cEK_Uw%=cjZ>z|6LZ1=gWM4O}pOG zw(rVTv&GFvuD*|~m2K^mY3W)ZV)94(6@$dv9V}hnS=vpn?EN0~`sv)F-fQKylOIa_ z^j*Q>p?G+|62H#GKHmjDoGUuAx9|FKs!QSGr@s?_Uws@ff02MzQ{aIQ+fOv#bDolX z=jTILMy2JaN;BitCo}!lMJsTL{}U@c@LTg#;k!*InyCi7t$x~Xc0$gJMI*d-t6@7TlXRE`;s-WK!HokF-Ec7*+R=@4!$5a2drO!PT z5xz=Liz#5mhv;nvA2(QqgjDn;g?5|>Fbh1pFD-C=Xn)a-mz5g=zp7>Zz0n!4aRyWC z{Y`9Lk0YeDHnDZh6uz_~HQ=Nlo@8y zJ8u1pcMiv**v+~cE@k1GJ~n6gL@zS6n(rtGTf&)>ANl&-tL#r}?u7XVM4wW5{q=q7 zSJT^lOey7}%ts54aETh9*83fuACdhv<=Z-~Qu9Z%uZQ^rd` zPdGalv;N*xPVvy!xkuVpE&j4HJanycI)~_F4U4ic+W?v4d(M?y-L^c({+VmsMW$nV zrRKM0-%R_ma^C+}-YaG}EZn$S_RtaM7Dj_Z^B%QxU7sS6*4i`ob#rO$%igbdivPd-ykmX%&vS3yzc_3v?eqNT zx^pEuqPLHq*ln_S{$c@@f2s3Lr@G#|bYr*v)?23YLc1D8#H?>+?!Iii_}!eoJKwfc z&xoi^U+ZN#$-PZp{k5s%+?)H#^G`b+Rp9E9eJiKYmwbn1?{}@EeU3?`6&A|HKPNd) ztJ`&)#q^Q%S}kEMwg8VeYNr)Uz29H$ifc?-t}s#2p=Q#?JDs}0@wMemS^;O&LrRu4 z-0)rIm^E!)zR#7i=9o0>XGa#XQuhoRKHa`S1`AXN9cUY zj<6#W_Ri0nxnSK5BhjsY!cKf(YWVPnkM&RP_j8Zl#jZEr_y3&h)!o_J%|}+`rk306 z)Bjc4eDhApiKS1=XKh;$aKrW6?zq)1(r=XF=ZCJgUfg3d|HSo)TebeUU3e3}XPZ;u z{I&k(ngV5t0b9C-v=+t97JMrFF{a$o|Juqc{^$9gs2%yPd01M6&3c82$J%X5F)n-c zcK`SK`tG@Z{ncNuW-dIGvV;HW4G+f+%~{PMBAcgwUHqc-Uf}uluIIP6Y+TQEdv2Z7 zRsX2ihfiQ@0q${%+&ooaws29S(*mo+q&;)D9lB$CeZ}*ulZ_UI9(5>``TWb{ajd=5 zQCIL>?fpMiNo8l^kN=ft=&6WPzGHh`}1E|h3;S1>e<%2 z)|i*a@xHm*^C2!<`r^7{H};+1K+^9njzvTUcj7)5X7sm!H3GAFCcRM#*K;Rtov?WKlE9sl0)>( zlJxk`FE?+QUY+LqBbb%DvB~R_$(|)zYy9SfK9tcakiFrVU2FdB?8dC7`Hy~8B%@gH`P?(S7Fr31oeAmW^w&?>r+J^ojc{aBU?9MLwCmH z*kfHHYK#0Y#CO)*abm4WyHlMXI^o4v$%Vhn8=KxZnXYJ3@;!6DtLV%`^(Wyjw*4NZ zd~Q-(y#zPLo)=K{u=#yvi;Xkmn~X2(=X?`;_%8HF?e6q%Gu&y|$M)dDs&3-qqt;PJG2nR1_;T9xem&F6Pk*Yxl2FFAXj!}!G~ap5P~EnQ|4e?8rN zf2v*xhe*n@WLfR#pX+Sy$(?>~T=RdP^>LXbhTrvSky~9?rbpIh$xpmhlz+47$ocoa zSJzjzHN9F@Hsw$5(_-PZbL-xJpM3t`Kab|SGmAS)_844xS8DspSV;GH!L?7>dI1xz zemWK$GlhNj`H0drYn#Jb8ec8v%9j+>y5YEGpYkj&$49$8j(?iw!1yM?Wk!Z&+lyxB z(}r$U+*1M=|99Pc|D|BN{HY7}^_#Zj3u~;+bJn?KH`$RGNKe zZbtv!XN%9cqXe@*B6loV@us{?c|%5d-)0Z2PK|rtA&g=QZPp z@|T8h&Foul-o5&^OYmzIt4=egNQlVV&k`2{(|?{3Ok3v{Q+Z4^YOnOts1*sl9ABGn ztlG=8t$o9D<$wvE#~3r77^ds=?_Si_c{hbibbgA(vDmjaww+rQW46uwuKC`0VT~1P zLFz_}9l!tLoBVvgX8-w3EnRch3)XyJsk)I3Qtc{V_7XkLzY<=`x*lpFbF{30x?@YqQqI=m|Trvi55S1a$T- zT_?J~WACqOqmu$!Yl0ls{PUim;j%!1nfY(kMeFyG(Q_9~KkOxX$}RrzyENP1*FV`d z9g%-{%5lMhu7cjzZPSV~Wm$}T78u#yIaj^<^v)oA#`Lv$<@fJKPE{~yY=KxL5&p(A&axVe3s$a@%&80+!X=)6{O#;TR+V(_1k+H+a2FHIYnI3 zf^7S)b{6yGh6RxgFS7%U?w&k4v@e;qIl4WDl3ZpxY z^-o_Jy4tiq&ahvnCH!^8b=B?{s~Il#^SkZ3wLdnO|Im>%7Osx;FD`0_TwcCQIroa? zfT{6z{ke(V!HWN5YZ(ff`(E&;UJT#z=}gu3_tyoj_taYLTdy2ec_=IWR?GC*oD*EE zg0Ax#zL@O}KD%e?n(01YS3ea`-QTxuf3)IZLnk)f+HW1XYY!b+#=<3${QWuqJBht_ zUrxT-9DCkDKrv#C-g*B;^71ZE#MghGVZ_EEk}`E+@T}6F^!>+Q9r?B4)43BT|Gx_O z==UVqy6?yF>Ajy~R;T~`|3~M#*)q+?vm6{vtd?YJ`Tr|7T71tvVr_%*m+aiIDYvip z|F1n>s_U~rVX@ZSpd<0e<6^fdhYKi8d2hVAKik!E&ARaUF7|d3OWp5^s|jdusJ?1h zfAz)ZotGTLwQmcC-Mf4HY4zryxR6D5m*-wTc1WsRZT-71Ps-CB-f!LXbn1!&Jili0 za)_jCu0DRH=wGDVvACUgGr#Vv|Mc#MQr_I%T24DGKhGA~yPv;G`r~c=i}n6(3@luW zR$PnR`lsxGwVHfs&%cSgj^Cg2bKXqh%E^=Vf7RlyWiFqaIeYEf@V_$ZA@y1T4mHMd zF4tb3H~d^R?igIacvL*t^|&>!~X*!&ft}b&Kidxc;4|RAJhB^Zx?3=dPW! z*lzwK7OqV9bXeT(d6(od5Kz@@ZZ~GTbIsPuU#j>nY)3Ho({X~a@UW(F3 z9j4w_W9cd0zV_X<>qT*=UnkoeZp-ml&``?rDf_I%mqmLvef#}=W%+N*;PY3wS0q=h z5Z36>yF9m#gSlwi)y@pzyc<)^8?PF_Vr$y9!SBW0 zUr!eLpW@2;eXl(G{RQ_I+n$tbL@1UlmN-zh-0WTs^UuG(zVUzFI%RkE(NreZD-&{e zUsjLo6SjEowY$ujVO_LY8JCF5)J!MIr`I`}-xwcRab(CtP<=A;2K|hug)Q zJ#YO2!_=!{Z_BbRl|3gI7x@2q&^;dY0D+0;^8LR>_HU0~psx1Sz^=B?&U^h#hl4(% z>=Uovp1Wv`-yKDdH;a?x4@mrK`MKr%jG!3t^}VeYM*Iszo6h>&+syBvfBLwvwusB- zJ%J@6PiMAzrFvQ0d$9hNy1VbIeDacrxfXnlO_i5Sy12vg%TJ|kXH4Jzd9Qcn+r;m6 z2Ew_MF0*iTC>9^jZ4#KD%`#`<`V;C${x~jBm?Y42eESmFMdm`IA$yCvo zHJ!Ruw_7EHzRqM~HC~b>(yYN87Wlp4aRztRA=%{|A{UlDS9zP&J~y{CDSiIBgD+10 zn|VImpP`8Bay_?5&xfy%{_huF7FZJSGUkN#SzG)2eN~|UiBnHX*7*MwtZd2B4%682`1Os=$+tev zdCzh6Wv%dAt8Z5GGM=+O5!=eYUMp2zFW^GfQ)8Biv9{B-|JQEWeQr+qw^?^`!^8jC zdD(Ur$vDiOBAoC`NMlFV_0Z0+Q(0?!CSRRqR`xYNZCbY(!_SQE8(XDsvvBQjQ}r+b#5qApg>J3A=;s;*Z}k%C1x}`uy#X|M7ME z-YLIz>3nQqbLK32m`2BuGOe-=Swgv={7PPB=!73jPX2DAc)Qc#V5G5i_X^p|tE^9l zslV%t(A(Uf=_=`xdz?XV={sXqu0^M|MHv?D7EWHfD&6?if%TsEFDtz&JjfSyYrfg; zxEt9IB)QJ*sBZsrt|j-I-1m$%epkNj$lL3D_SLTmFVh$p%p(^jw8h*1+o^RZ>*y)= z%$@mPS$2(W^L+K?WyiGw_ieMeczAB3 z!eKLw+jFyigq)Ar{`=gNg`LU{hD@yQ&&)|k&DKxGp0xjS~<2l7CqpTN~B$qcmr=upx)&^T@dmWOFt91(T)L zPtB5MVqNdD`h{)XhU_n8D>71#WwRZ!YvHU4aDP;wo1qj?aJ;K;dHRMQCX%yc1=jc- zQBv5qyk>z~vX4yWx>g6rFx#f1glT)h&Kowl8!?-XGTm3qqHjODWmVVU_q$YT=`uIf+Wu z)qg7g2%Zv|p&h$hT;qmk|J#7Q+pQz#p2(aYFj3PdgT-=+I%V&l+xFP-@RKGHRrC<=Qq{mQFBj}xc@)3^<+t0 zdTcJc_PP5hzsy&QJ8&?u{wYjVstjMsdGSoq?59~PD*pJET|9i`P1Uzoe->T)?on!( zCHZmQYcs!>n?yAp>=A7)Y3V$;ZXMgwGpj|7>vaG1-DCc^Ia%KF#`(I(cfP;xj8RvX zmtMa!@9`4d=tic0JFIS;pCOYnZ%J5yZHNoM(D94w=YF+%XT93OxK91~a-D}v9zF{g zD%Pup)cn8Qk+%2go4!l8nZ-J{sB)DB?Xwrwcra%wbHTRV_txLB?KhVFw4x}h)=%XY z%e!+6%wEe>$vobCKH_5EqL}aVjauSv_`cev5#TV}fAYL8ey#IjxlHxx@_$|>OjPuc zasM-Qa%gVV6JrVGSIhSCn<)nz$X8}NFfYHObD!5mV~4Ll=3G3u=&MBfJ;`^0eHYbV zUA*n0w%Iv<+o#5`XqKGDruo}e{1E^8uk_8${F;+VSMFZVSomn+_k4~oI{RO&7Lrt3 zy!X|;oBy7CoLjy&&No>$`I6Pk+p`@UyT6G3Uv@8l?#-3L^`p(DQFhJnItIk8`WWQWDeE)U#;*gzno5NL&T06tv$(%n? z{PXME`Eu)G)?fXr>9WbU8Z=CM@Ah1+-Bs^4Ti?34aM5#?ylJAx=Vmti{q=GG`hS0y z?~l(6-B6((ZQVH0YYTfL(~P(8mZW@Ho&NrmfKHffatr6TbyfS1p4`gv@3^tZ8@)&C zlRwAxw=YchS*C2K{P-tx)vuon+h6n4=UkOr6L27Vn|18<%{*??{-5dlcYR}?_mxxc z>vlw4yLc<`{r1XQ@wYM2v5^~B6rH=8WBQYKiBI(gC&t$=PyD}n>tx){;9ak_+g9y= z_W5f1`ml!!Ux%;yTd-7=?c9k=c99MX64GaGvrc_=;=Rwdx_QrUp3nNb`>MS}#k1YU z|MU)Y7#RNgv;NBM@c(yDEHHfibAIG~)~UJI+j1(K?2LTBEjqPHHGLZof2I8vn>Djv z{<&9K&KJ1NcJAMGf!CKDDs7AN+REO@G*A2L1@RN#{&;=~nCSRa*Kc>!-#@$)S{x3p zGs-PLm32*J$#d&(JM*50cE%Y^IeItwOhMm;!_$&G9T>m6{*P^$y2)2*Reb-vRex@k z^6!uP^MBs_+n?SqK2bEsz{95=rG=JWT(vG4D43Rz!&8vFXnx$8FF zv9Hx+IYmCqJZH9U;$+e5fAhuOAHY}dU8>fET{fb}3_p4p& zAJ=$t^VrVHQ%nh)PBpa--^v^K^0iuw!9A| zpEt{;&ULx{uYBG<<_D~eO#e=NOU^m+v38T>-ncLGB;4)qPjs92``lBm(5boCnOOHc z>r1Iwziq;ttI5)*{V#^;yIp-8_biH_T^XcqS5-81;-?dbw=%t3 zWwPx5;p}9_dAI*gpWE*&xkq?m42x`pzqJhu*SCwmsscI;3S$zFe~!EOu6j>bnaE#- zf-VQf&)cmfmvlY}uI&qm4{w`&_57|mKi@0IC_mWx$vlIFYoD>k(ZGG5Ej53oXuY1c zAm066^88%azg;!4O7hZY((ZlvZ!_gAUru?_miLp_bbLLovSEG4Q^~(;{f`K5T(6|r z*tEJ#enXl4|BFh#T}ra2MJ4+!o46*go>#ifsj^`HzbE^2PX#PUDBmpo>s<2}z4d*y z<@5H|rzdweW-VM%YWAv-arP%3)<3$36mlp1xVj?W)N70xDR;X~G~BGFmAlD3znT5_-TvsSKm6a;(cvR-umqF?R_tc6MEL(0xhon zAN6-}SGZmEu_LLgPhMoZlek=aeQzpz`F)=xg}JXU@BXrRZ|1YRAKh&EOaJYexBu^l zm&H;0)L*|}x#8Z-D&s}`-Er}YzuoqZT$muf+FC>QLjLOYhePkLzdbkkec`>Er}CC+ zzg_EfyXVg}^{gLNpZuS_U#Q&JG7iLx8oa)Cz~k9@7wzhqipy0&U>YR;9NtCGKn zWCqDUwK#Wcoi3Nin`fu^TXU}~s!UIeo^4g?d;Zg|Pm#8D0q+E;CEcS@q4kzj@c2cXjpskKgZ| zwecy-$_-a@Q&gfCifwdaG?dt|KC*QA_UGU0e(9|L{pPus<-EPeY~$JASQ&e_5Y;k(B2z}4L8ajv(2Tdm&}Hu07A{=0kC_SgL}zC8E+ z+`IK|@8sKsGAww0P5L2cHebGdY*9;BE@(o(Z}mFK+w;Qs->rW2{?zBbYiZ%v8v_?jEq1kT z?Q9QR=u~U#xS(OHR>`B)Zvx7!=RA(x8>aqlmvN)CW#Z2-H&?59t7R63yh_)a>kZmm z5x+X_@66n$X-_M{eFGNx^_2aTopPpXUxC8niTa*9KFA>sK!CPr6*W+9@YzKjHbpS5@2Qvs~_XU`&>%xV|#xTe{jQ$#eFH4d10a&7ZS^ zyXQjoRHwf-o(mpWn9K;hBYW!Q8Lguy%tU{h^QXP~`^M$<{aD*RSQGYwrX8&iKsa2JY4vc?aw%DyUS>S3vo#(4z zm1JD0T1Ltaz4Sl7zU@Enw#KrxpVupE^Yi$mKxCif%`$^`lB7!#qCpcC+C#S zVR&D0?lPwcgXLD9N$=HiCF>68o?7zx?yDnnlY5Hl?#I^3J-V9i5OV%j?2&B}vm6*} zU$%TJdM>(Y@vBpB!&ElK zw@;mNw|e#KvPve_^o))>8{H5L{A#P{^6e|0Ud>9A{LUfhV4eGdU0cN9dfwa%uR3$y zf9fmydrt2B^8b3bD(6m2EKNG{{cddS>58?D4_LSw_ASb-u8J_7D6{o$=9YW;{kx<+ z-sR+<5>W};F8poTKT{zMhIO4%68lbnXj|^%w$^XX&)>04EGY|pZ50C?;U>-R;cck8v)&byu2+^~^%$s&`pCXNa6%dheK` z2SXyK$bqbIb+14t*H-q;%Kib$Q-jy<&;NVw#C6WH1-x|%0S9aY)wYZF@QAM7zH)=Q zz1MZWXlr*%!6pYrmrKSWb0jm|d5%qF`?2}B(90Q%XYI6IpETiz)w}%{yUavi3m@bV z`F&~S`NhWj)gFIa{vztMX4KEHd~eZk)fNsVfe-A$8Wrx!NmI2JI!Uie{8B2SqOdIM zZIMJH(=ADzcjQ_hQhxz1+&(ekI>w|9J{J32uZsXcay{A4BOsoPodrnSUT5zvY zyvwHG?`#1_*QvK&6fm*&EOp+sK1uT2oEq2K3foDM{4wF&LdOla<%O&-Hx5~yzgc5@ zHw%|SbKKnO{_}<>S3ZBUKIwk!)D=fov3#&+V%=gm;hcGq)3x7KVQb{~s$ZIU>cqEY z_V3s_9zA~W3MzztrkfS-ShjMZT&_!CUJ#msU^C^-Wp4?w(4(fl{^5!ZTIY{^yeu)(T!<{pgA1 zsl(5I-LBW1{CUb%6(-gRvEC~>3fS#lIhbc9$t*lmy;@4;-5Rf$ztR!Dwr?C3G#Hiy z6uU;O?06I$IY)PO7vqBIU5<||p0RQsEB2jnDtcanmK^ho9?ti9`TeVo%%1)4s+7tM z{{`wQ+9CzL=WO=v7M>e-eTP%*OWVwtov$uF{w}N~q}Fhog=>M5@VxWyeAb1xF1_~t z>#fW6TUpkuN}YK0=If_YhI1V@&gUxkU3_`w@q+YEmv_(IW5rjRs!z<^jS=IJb$#R84nXQLg%-9+$ z+nVMZ@fuwDSbAhd_0{=ncO+jc7TMc$#BUROXU6##E)NrPE^TmPoG$3r)wAMxo!fbX8C!X(gw=|+cWz$eH(`>)K_1(CcMk1S@>kllH?8bR;kSQp zR$Q-Xm7O>J!>b4np9KrH3o;*CeqP43LF&$<4jHXJWxov(U;l=w9J{IL^I`VYPP?%0 zhoglwzD<02E~Wqd^@q<2o~}#z5>P1fxB2Mz^OB|S!tKgKqWkM&!#5n|Ja#e8N?7BE z-k~Flrb`NMyf}Yvch`o69U9?YG& zU;g4R?mgwU(sN2YUcVL6k~3=Wev`U?Qv3S<+ivFvzA0HZF(lvJn?q#JrCS%z=Bzls zZ}rn1+CCoIw{$~nQaHpzPgSWVHf@fnJ|wJBu`E?ccmC z`273lcF}V_%!=?5)cCRTl7slu>)kukx91AX-;-5deoCV%dfk#Bd2i{zl218AYQjqw zSX(PzJ$bzJsZ`pk*|u-1?#&E&n=I)pyW^O|z6tjiE^s~Ox9+)Ny3K#CbJKP^wsy2| z_BsFGGHaV@hr_|pnbOJ6lAoI|Y|2^pZ^eSTuEzoV9&QUBtkK$E6#Y=9Og&`6(W?pz z>sOs^zA;5L;DD*sFNqeeMVqw_mj7C`amxE7Cf4*2={Kw9o?q9(wMaFF;Gp%Z<1xS9 zE3j}aFk09&&qwT~>)#pfk^Tw+Z(J8AxjV7iatPNf;!libV%@;Ju*tfG(=O2c#w-WM z=QA>%sfS!R0m<>%hqKgH8N{`l7N&*#-b3R*iKNzFVJ6fYRP zY}b@o4vb#}EM5MngcP(HIOf0NOa(1l+Hhq3;grrgqiahy=RSCCzjV zwL<-MicGoJW+%osr@UCt&)Iu#Ki}jdSI@2K>C4*xi}i=wf*aRoHU_kxRNsANV(hu% z^6*0}m0$AqhuiztMmq2GR|#OS-fi@NLv$;r@Yc0i`(Jt2|9aHG!e!yF{%yO~Q^gPk zpEnELe}BEhVxt)F=JXMce+D1kd(TK<`I@Tx)PAM|vy@tMgvM-y9S;-=Of^-K*_B z+TwfP#HA}0@QMj&F#J;uxuWW`$2^Jqa^JzGe^(YBVBtzwdV;wnAh6%yONCJ+IQWriqq3-@5TYR%G14S5r6rthoAI-d6qC z{8L%m%YvTTEZTHvMuTXV?as$cxjYf3q5Id_{`wPt{Ac^T)zj5KG&>yBW@D*Z6*B+a zobC(z=Ix&KeY<%qr{MX2-zLYsUGmBFiA-sNVIxz=f=4WS9$BVtte){gROQ{OsC{P^ z%lkSlXvi+flWA|?qAaX-tM`{|yI5c!vxVb=278`_7{!nyn~P`c*sNt}^Uc$naFzupnw$wz_ix|s?9vi6_4tw{t$pq+ zSBj3{>+jcCxD*z>Y2FlI7EC)&s)k@>vw>XXI$U!C`Tvq@{>+X~6`Rk!v07u@LX^tM0sX`gJE zCQsepkog56aZ@YQUT@qTcwzn~Er$gUmamy>^ZDxvZKtF8H_sb(_52M#Ew;R8wb1z( z+xDF2Yhu4oefullbwNY@%Po&i+8J<*eh;bTsNNphnSO4b|B}yrB|0}>e(w^{Xt>IA zu3jSMf9O`9ve>B=&n{P{+Pz=(b$h#Z>g1h#IS)YxJ3RPd8&M+_v#;+?^QoD|Px3|Q z&)%T*F=kuwo=fvKe~(pu!QH*liScbo$LCc2;^_ImPMZV@t7R4D-rBO}oZuV>MwgAJ zZwI$@6|b^2Pwc*YZ_CU3EuD*4x@upXS$DB>?MCkv7Rl|!HLf!hy0x!oJvY1SWbNUy z;DL4TbdE9((Ob8&XRd#3e2C?K=<567Z))B>lu zeRoIR`>p@3admQt6r9f!-j}gy`u>2z*tX7NS2;u4iXYiV&!6{MsmYf^XRW=a7J6Wx(tGyGJ~?g+7#7`5 zoN)7@O#I4EcUpA)WR8E$jy4S85SA9wc(AXF*~!G(CVRtS%YQ090T&G{? z@9`4Ucwj3Vt9MoH&iN2a_r#`CW!3W*eU;hLsl>vi&@Ia*cRu)ulFtS2Yi4(MX%))c za?xaBop6%xc2gOLsA!ma3#Z-6e>O+wKEA5f1zNzocJe6?$@9t~enG7PyB zIn{zMcachC6Fcu8)6~OUqRy=b2m7>IyLKO6<}0Eaz##c{gIA%|L)FhC~|M> zY&SUQq5Jm7>lfkAtG>;=b?_Mr*NgS(?f&*x*LklO*s9c#x`Xc!i}4x`(I%F=H$Sn2 zYnZNiM zcv-q?cic9c7JlN`a^4Sfw{cwPbYNtt7q(;66VO;7zgpyD?Jl=3m!-c$Cf=1-SoTAmyu0C<6E+4J>OFvh8)KQ4O{OR_MZKE zvwb!LLoW+goZ-YIcD0ENpe@OdXRKjjc*-eKZFI5K-e%5T_UnQP0*y`OJO_$3(is$V z8<`#$FI;c7dK-f|hsbZEhI0$&6c@~8STNCnv7j%Mi=o14!2{vR8fA%7nHZ!vM5>J& znaUm<;{Y9{kS@`4vo-w0yW_p04YOGw=kgr9xx4t?nQei2Uw15H_|WUX_`y6nf#CsD zW7A`UMyaQ7=H@(|-yhm#6QkX5kcDfVfx%{OMScc9A&mr{hpX+bTi72IT)^De#Ll1o zy?AMlPsSsw;@mCl4BH?FFtBj#+w4_1|7vH{njnS)>`bg*Hb>96k*cH{^5p3*1|Nlh z50gW=64*tZY(cZJUpC%;btDg@lADS3e8kcnZZjS@&SprkW@5dg?6W8QV9S ztN)l@HnBaM!JyN@k$*SeoiO!pDj`pn+cK4?1bpao{BD}qWZc5Va7tL?#nB_3b7MF= zZ?Q2fltMvYC{Wp{5q z+{t+^i&J#!EiML7nQJ@Qc3l?d)K@oUnCuTQFtLWe-Q;z#==qJ5*7o@Jt6U6biUAiE zRjtUdOiOG^UlVp_=^F+y0gV}omlgDVE<|UqIB_M<=z%S-Q_p;RkJ=FHfzT_voC8?~DbZud|L8a)_iGi5FYKWU#; z?Xzpk^!;-+gHy}S-mTh|Tv@NRS@v{F`7gB@XSi5xU2C4#t+(F6CZD!rGw&;lH4zLO z8XO$+Cpx*VS5WjZn4NI3eH*vIK~Tx4`qyfmf12F?zjrwu&U;Qd$+6n@RYLaOcURXf z5}L)pB%mR&R5e7#{Wpupgat+iAMKiZPBcNYv1wwI^U;rw-{14)sk*<=gi~=-+`&h` z(^FGRnG`r0n=Za<>1vl0Zhtdb`&*HDM9u%`Qu&5xn<-~`E~@KX?B|br`SDW2dgc4h zcj8331v*5z(q3*1x;WdDJ@iY&#vebw-(qK2&LMI}L^WiFMqudrgpZ$%jkeD8InEW( zKb@yRHf=L_Dp&D=(;5S9d&XVjpXQG!v_K zZ`@jgoelPGTeqjrH(&KOaxMdh#{z|>dF6qv92NP;wjB&fN%qPqHG6;LF*FHiFl2l!USzM8P*KOEV9?0a5Eo_>ko%Ph)C6w0 zxMwHl0+3*6*#1DS2EKore=#sT*igy|DnuGITDTfopoIXVL)yH(3=ux4M{qG@s0A=_sLSN7fZuVIZBr z*vJG?&A@OLW(TsOsTG%n52S#06N1k8!nC88eKVsPXx|y=_%p~sU`UD@x@>0f8gx1^ zI;b=;I2bXp8caH=$RMH~z%b$L`m5{=2SA$x!Ka5s?eykh;1FS$@>Ei;fs=)c!Dy2c zn?MWf>@p;OE->OxV+I{tBXIQU$^Gn`8JPq$7*4o!FmSk`gki%gklhm;KmoiGM*ugn zFK3)2q``3F(K+TDOxy<)m{=KZR$dl9;Dp7;4Y8mAV`yY*xLW1&#dZeoh7Jct2R0^V zhX5v4gIT$13;{Es?rpHnaaNSpP6L%<3?YgSm~`NWr-f}|9~rC!G#FN#2(xMMWZ_~++ib)T z0P=}Tm;}Ql0S$(RyAi6*Ag6%OjyrJf&Pui&o(mWjXq`_4RT~TjlSLUDl32JB#DqQ1 zZQ8^D+N%5|fr*1*HnwzdM(FFoKP!&2PG|z9g1zz|z8_)$RcFX2(;>xf+9$KQwL8Bt zxN?d(=-*p*IQEr*11K^g92r4bB4F-Reo%RetXtyjXHJGzco=ZlSny7m;=p(&?Kd}r zh*AK9?atFaX@~S2m>ZcIWI1*-G=p~Wf)2WCn3$u?q~W)KA;I+aLx<||EsORnx~>a4FDk)YZ4QGhr^tb&CM8ZcG$G-(=ewmCG5@y^;ZgH1S5XT3A`qKr9{3qOTC?bm&so}an4L;B9~>ZvcM zq*T{W%VD;SjACNw20JkeWNd&hD3`6`6mejg_hk!TE$0TwMy7^~o9?X9mtmAq2w>Qo zswsD~yO8q&XqPNQ2&&FS1b6DvbQ0^?Os;Dk3f^0aVScrIXI2)n4o!y#JG z1j>RT!Ws=3F_J7w1v*X5EL;gH-vb$Da)=f*I50A-*VHP$;14R4dY-iSo1~qsI9|wo zPe7v~aL$zL%j##YO#8z*8RYn$1vi$6u*wwH)coB4-lFXwHxuiH*}{ewCMWaws0A?C zT3%$f-D+`c#?ppvaP-Xjy2e32eEl;^yRU(__22(`eB!y=+slh{g-U;ymp+yFyh6X1 zdBvCKZ+ID|rDQtj=>B^AI({qb`ckSwzCOGo#O|xh9UZE1e zu+~!Xyy>pLU(JAt_$1Cv7;Q}UBhrA}1-4cb5 z_Zu*YvT!Y!I&HJ?p6P}jE_a`G+&=Ptk*({Q8I9IVtOmD^Pp*HyBkbrI_nDX31Djb5 zCA9_S%-+-}R%N^Y?%DqR*?+?x+-#kt?)vduPq}l&E#WyT0Srg3|1z9;v1_T$LBrE! z>y&=n0<%7pi62OgWWv^M834{L$zYE=ur zUH4;og>>!nr$~A)FxqlD?+YiWR#T4A6ey2L3yKb~&0ZdtFZS+Z?Dq2=x1LYjp3Ay< zzSwo;GZMx+{tFm7l)WbG2>Ns9-?yy9WgNH9zcFA8DdJ}h$bPa{*jlHtLqILc&h6Xc znE!iL{FN)+ZPYEG_C-6y$eGb)!{=HN+cd#*b!qQc?_Haw8xh=Mz!;Oz#)reYz{OX!FsVJxpt#RWJTld*$sZ zg`y9venJ`zaUu-&zj6s}KX3QBaxTb6Q)9Eddb@0sa;%69&aDY`y) z&hUw@wbTE+Lq@lF#*c~*{+b)N2`(!LHWN76WuE@Mt|a@KLE&bv`PFCMX3uP9`OqfG z^`M8tJULy{E_=H9)J^^~c1Zqxw8vN}KUysEkjs-=7AH{3j?(`)^P$&-jMyt@cK!Ud z=EQA{kSnK!)Ec;1xE5@k%iScnS?K%yt*a&X|IJx(V`shB%IxO3{jw8gIWW3R$({Bn zYr+drwN0WK7q@R;HeadtvS3!T%a?uZaRM3*iJ&W~Nw%O|w`z0I$mlCJeU&%N}Y zXRrM>@kHdCOZ^4292ir~AFI@VJyrZ(Nh^5bw7|D(F0EpHIraPMHz`;Du{SbhtUAtn z)V;?duzs4E<0CI=*`M!3yS8}z{pa;I=jfZad8toqodfNxFO@q<+;e7hDgR>2y7wOQ zg+)KIH^%O6>CDNxzqs)C?4DY&$}+wg2Y6Tuj=a%cmA)=w`;BX2n+46eR#?rv_4d@6 z;AN8CFTDRoo!HPT&?m{YV5*1uqs`&<)gmRjw-3KLQatfqK<(|mscAYbSr2p@nNBQ9 z%k=#6T{Pw2Il-*y!e`4;cfbFi7q)*}*5}aUsvlY%7*mR#auww7?ONWk-*lG8W)XAU zW3NsWT&$Yo`no?%sn2wV-vS1su9Bx!Wrc>ne^;&z<*57i{o=juM4NqT6E>(cGF7O1 zJ^Xj|On~7kg^pX_lwG;{!@tam?Y?Bz^`!Ke)*Q6}2Hi7SYHs?CU127!x8?42@5x!; zX2`)IazLm`Ec0f5&t2DTOI2<*yDr;iciM*;lK7^PJGg!6#M?KE{@U%&HcWHB zc>jPi6YGXmXO5nKbLi8H@BLL=7xlt>l+Q(_-0Por(rh;CLrxKfpDr~nZ&$hA>bd{* z>u)#q9?{=|FFY17bfjLp`cmxv?yMCv)|MZ*kp4VI_W3vAY03c%PcH2ec==J{@=Wth z^MAfu=ayxKA6?{|SN2S$PWCvI|X=3|(n6u@xC{83iwd4t4hOm%{% zZuU7aGJKeuz`)Ka!Z790&cADp&uDQ3otPIT;<`9~2Kxaw7OsY!WjpsPe13ms&s&DO zoFWX_!94rZ%G#p7>HhFsz_6|;=b#LKnwFoW9)rl9873bg=+BUh?dy7r%sujIUbYJYFlF;ye(H{+3MrA$9*peYcwntiFurnosoUbE;T+4R6WgFom+kJKErHb4Tf(f zS{yNZowPR?9O63t4RmUo#p4&Ap@KWwHU6%-!8`+$7?y`FTz7$OfpsI3#c7?RR_nf8 zoVY)>aA)w5+(#0O(pG{R3>Mi}7eyWPTzg*sf8GD{H}|)fuy8GCi|n$w_x0*cJF8#& zMwA{d`hoiQ>8s>7vJsUUG^Y;Bh({6(#0!jBVmpy??Eo z(-Z<2bg#@2x%;+dna=+Y`!lg#2wuPXq;@NJ_?`aS4|VVKEbd<@*vRx^?e|YJLz|ASv$@&1 zLMHryLL-yJ(sIWgm)0EJd$o?Ap&K;a<97GW?yMaVXSp^DAG>kO?aO*YmntS!gTp75 zbJR}z!Khqx@Q(MDeLJ=%?|~>mTwqGIeCQ?a)Zg+i_#*3d_&dXZ#pc6apA7x^jrG z7Wuq6HOGBn8vkyVsuzcBMHr6P=xS7n%#!Ed_x!b4if+Mqv6P#2>Cg7o;9w{kZx4=_}W5zwed(mMxa{f$64oV9i5!2B!4`dQ`mgs@8quvAAQbOOSzriz<xW1EkJue}|!ph5VKGvkMQe>>~0>=obs-u6@N#B1-g3yw=% zJhwGD>zG7F?fpv^Yxy+_{Tvw5U3LY@tb8$})@T1MvCZ56cic=~|FvTF#b<)=BX>QQ z5as1)BA4}GVh4D#Pf05@l zDrh_trWxSfS-m*xbm{Ni->!GeT&45&+O4dIN!ROCESbemewbRFS69aHed}BiYh#PJ$+FWp?h>2N~+m++$$S`}yP3 z`8DtJHN8BnoDS~dujTazwVEXbb=I-W5bfR+xIgpgHfFJelfoOC&u@x1yjGQYCGTzd zwZ7Bu8N5I!nv6b%s$@}Z%8{6z#tI#EHx`~`)moL{#vut zHl~J)BHk&fZw@gtv2NhbzRd_4-i~No-3A)=WON8go5~;r?%aX;EyfYc*fwx9GTrD@ zH8~J^$e>0sfMIpPBzEvX2E&3`4vY>d(^fLFsDsYhP0eE92I+hxu*K7T0Yh0bCohAE zN&tg)VJg4G!s{E48TL$J;bLg`*}{2ANQ0r{oRR6KUmEY54^8~f+wu+6eMrcbcTGsB zWn%U=c4lM%b+H;`cPjBQ^m2$C$kNee0C$iZ?9Q}pVr^t<;1Nl4Nj4Ly1D%`ho5(f+ zG)7@LV=1GPkOo77-DVSqC??ho+TqoV3m6-jA||fh%U}TSxt%yDQhx@3lO)!KRTZVyfxSH6Ddh-H&-h8krat1L9@;a!lw8)PG|pUGk|1XcbGIV?^M4lG;@9li}+$9n|sz=Or1I&IpGHmJK8 z=56+q0v*%Z5F6RYz`zUl{I!HmIfGUQMuv}(i^SU>u*HMMq!tDwi!v!h3u-XL1wT2q zD1aF>1Xs4qf)&;yhMCIHSLiQlqY%Jwz)ED#=bh%=Z$a7@2-Nv6UiOo0~B-8*Jd}DAhZDeXVvBo!DZF2@_5TT%tiFt?m zmrbA>A;eo5wFT=M6+wq}yZ>N4B%r}C*A`nb4bC0{32Jm|Hk5U}%`rvTo-Vdr*r6l6S!ABH*~x zYpYwl35HCp3>PD2pYw6j2lW$bmM>t9E9_~ohKpM$cz$NlK~P+QGxGv=Z%@!n4ue7WQWbEi+8{gAwHeeCcrBu~0UBA5 z$c!s){bXZo#vlz(_{KASGDd(#nBN@RWRu~sfPvx1IUOk(70`e=C`(6en!=J`3=dJ0 z?8`Gx>PVTW1u!uD@q5uK3`Jvxo2elWF8SubUN!LS=!fQ|i2;ra7#6UG*E5=_1~BYd7La%RYJ3ALtju^| z6@HKL258I7nsb+2L7h7WP=Uz6Fip=1t=K(r`s}d-B}}XgYtHUv1g8nGJ1fo=37t4! z$1@ic!tZpro4HxI8nQ){7;<1^d<@`}4~Y!0dmE11WKDX}6Q}^XuH@QN%@j~?$-(xh z)R8nXb~e!9@!XvTpcz|aoi*uqO&LJpdS&A~DTXcwMh3~5uFRl}lHi+mu|biAtKt66 zPq+KGu|`aAU@VxYz5jluaDy-0qvGC039{ePC0rITFqEaPlrvEXV3@O*A<-=SUSj|_ z7iT7CJU3*CPmpM2Y6uhA2$}(8=nFPrJ|ND-+K_4i_AMlIjz_$^(kH3d(8?il;GM|! zT+X;!$@LBvps;aW!Q3XK!Ei5l0VC*W`VGdX-5DMzH8MRg-7H+oQOwW{TA8ky@muf^ z185&@ed3XMz+ks`I=Bq_JKPg4iDv{bGO%-qFr4QUW%$tM!1(6bn@a)q3+v0iC=>W&EA2!;uB92iqBXIq|K!L;{ka>imd?$dMEbzf`SdRsU* zhiUGOn~f*jM8h`sw@#dv66`Brs$)d`+VtOh|#CRZOhWL>?XrhDMG^K1Iu*xuc!Y+SuaMD2Zw{k_=C=Yjk0&ieYgYI|ba->px7 zbQIWg>73_bEpTf~dUDUJ_0ZI(0m{>+r$|fBy!s`1*}si4T$2Pf8q$qK6~2e*JFR2u zzIwa;ecGPYs+Uj8ycI8)D9f?qq?Cf!&EFAX4`mtCwtXS&=i=rQZ(>>Ay~tS*v6jE;pWOFA2lr_<2cwkOIMrWPW=(gT`l%+;^N8WL*;kv6 zoW1&6NA7RzmHS-Y8y6pxQWB}`Q{U(+q5QpP`g^x8fy>I|ZPSdm^0p*BZ@iNx+Sw;t z>B=c~?85u1@7~Y8$(g1ZZx{4QJt_R;sfu^6SpWN)?>_^bxU=8vKPJMW9^l|->%UH0 zL}AbM#U93GNs%k}Y9q-?SnyY&lZFu+B`u95vyI_WZD`c2Lo&8uIO$|xraG%`I3v|&isocG%D z*&$bGMb$7TrkADS{6-;AX$+~9HducTJiyAt%CNx*ls;fBDR6<#!0d_cMN7vR!It7G~+pD__>T^?kYfZU5Vjt@i2p z3=sl5^^mS9Mi@+1 zxOm@wYS6!3Q$Edi-H_opqrr`ZD`K+r4oTMu68;-@_|0f&W8u2dy!HAPHIFmu5myA& z78o`%eN#yY@Sf0dcHiGw28^;5IXZ7%F4nNIc=zwo<#[class]{sidefigure}{ +\tex{\usepackage{tikz-cd}\usetikzlibrary{decorations.pathreplacing}\usepackage{amsmath}}{ + \begin{tikzcd} + \infty\\ + 1\ar[u,thick,-,dotted] & & x\ar[ull,thick,-]\\ + 0\ar[u,thick,-] \\ + & \bot \ar[ul,thick,-]\ar[uur,thick,-] + \end{tikzcd} +} +} +\p{In the [cpo](dt-001D) on the right (seen also in \ref{dt-0040}), the element #{x} is not the [lub](dt-0017) of its [compact](dt-003U) approximations. The only [compact](dt-003U) element that approximates #{x} is #{\bot}, and the [least upper bound](dt-0017) of the set #{\Set{\bot}} is just #{\bot}, not #{x}. That is: +##{\downset{x} = \Set{\bot}} +but: +##{x \neq \bigsqcup\Set{\bot}} +} \ No newline at end of file diff --git a/trees/dt/dt-0044.tree b/trees/dt/dt-0044.tree new file mode 100644 index 0000000..e44cdab --- /dev/null +++ b/trees/dt/dt-0044.tree @@ -0,0 +1,22 @@ +\import{dt-macros} +\author{liamoc} +\taxon{Exercise} +\p{Let #{f : D \contto E} be a [continuous](dt-001J) function between [algebraic](dt-0041) [cpos](dt-001D). Define: +##{G_f = \Set{ (a,b) \in \compact{D} \times \compact{E} \mid b \sqsubseteq f(a) }} +Then for all #{x \in D}, prove that: +##{ +f(x) = \bigsqcup\ \Set{ b \mid (a,b) \in G_f \land a \sqsubseteq x } +} +} +\solnblock{ +##{ +\begin{array}{lclr} +f(x) & = & f(\bigsqcup \downset{x}) & \text{($D$ is {algebraic})}\\ +&=&\bigsqcup\ \{ f(a) \mid a \in \downset{x} \} & \text{($f$ is continuous)}\\ +&=&\bigsqcup\ \left\{ \bigsqcup \downset{f(a)} \mid a \in \downset{x} \right\} & \text{($E$ is {algebraic})}\\ +&=&\bigsqcup\ \Set{ b \in \compact{E} \mid b \sqsubseteq f(a) \land a \in \downset{x}} & \text{(lubs and defn of $\downarrow$)}\\ +&=&\bigsqcup\ \Set{ b \mid (a,b) \in G_f \land a \sqsubseteq x }&\text{(defn of $G_f$)} +\end{array} +} +} +\p{This is powerful. For example, the [continuous](dt-001J) function #{f : \pow{\mathbb{N}} \contto \pow{\mathbb{N}}} on an \em{uncountable} [cpo](dt-001D) #{\pow{\mathbb{N}}} is completely determined by the \em{countable} relation #{G_f}.} diff --git a/trees/dt/dt-0045.tree b/trees/dt/dt-0045.tree new file mode 100644 index 0000000..9546dcc --- /dev/null +++ b/trees/dt/dt-0045.tree @@ -0,0 +1,32 @@ +\import{dt-macros} +\author{liamoc} +\taxon{Theorem} +\title{Nothing suddenly invented at infinity} +\p{Let #{D} and #{E} be [algebraic](dt-0041) [cpos](dt-001D). Then a function #{f : D \rightarrow E} is [continuous](dt-001J) iff, for all #{x \in D}: ##{f(x) = \bigsqcup\ \Set{ f(a) \mid a \in \downset{x} }} +In other words, in an [algebraic](dt-0041) [cpo](dt-001D), [continuous functions](dt-001J) are completely defined by their behaviour for [compact](dt-003U) arguments.} +\p{This makes precise our earlier slogan in \ref{dt-001J}, that [continuous functions](dt-001J) don't suddenly behave differently for infinite (i.e. non-[compact](dt-003U)) elements.} +\proofblock{ +First, assuming #{f} is [continuous](dt-001J), we show that #{f(x) = \bigsqcup\ \Set{ f(a) \mid a \in \downset{x} }}: +##{ +\begin{array}{lclr} +f(x) & = & f(\bigsqcup \downset{x}) & \text{($D$ is {algebraic})}\\ +&=&\bigsqcup\ \{ f(a) \mid a \in \downset{x} \} & \text{($f$ is continuous)}\\ +\end{array} +} +It remains to show that if #{f(x) = \bigsqcup\ \Set{ f(a) \mid a \in \downset{x} }}, then #{f} is [continuous](dt-001J). Using the [alternative definition](dt-001O), we shall first show that #{f} is [monotone](dt-000J). Let #{a \sqsubseteq b} for #{a,b \in D}. Then #{\downset{a} \subseteq \downset{b}} and thus #{\Set{f(x) \mid x \in \downset{a}} \subseteq \Set{f(x) \mid x \in \downset{b}}}, therefore: +##{ +\begin{array}{lclr} +f(a) &=&\bigsqcup\ \Set{ f(x) \mid x \in \downset{a} } & \text{(assumption)}\\ + & \sqsubseteq &\bigsqcup\ \Set{ f(x) \mid x \in \downset{b} } & \text{(from above)}\\ + & = & f(b) & \text{(assumption)}\\ +\end{array} +} +Next, let #{X \subseteq D} be [directed](dt-0010). +##{\begin{array}{lclr} +f(\bigsqcup X) &=&\bigsqcup\ \Set{ f(x) \mid x \in \downset{\bigsqcup X} } & \text{(assumption)}\\ +&=&\bigsqcup\ \Set{ f(x) \mid x \in \compact{X} \land x \sqsubseteq \bigsqcup X } & \text{(defn.~of $\downarrow$)}\\ +&=&\bigsqcup\ \Set{ f(x) \mid \exists y \in X.\ x \in \compact{X} \land x \sqsubseteq y } & \text{(compactness)}\\ +&=&\bigsqcup\ \Set{ f(x) \mid \exists y \in X.\ x \in \downset{y}} & \text{(defn.~of $\downarrow$)}\\ +&=&\bigsqcup\ \Set{ f(x) \mid x \in X} & \text{(algebraicity)}\\ +\end{array}} +} \ No newline at end of file diff --git a/trees/dt/dt-0046.tree b/trees/dt/dt-0046.tree new file mode 100644 index 0000000..76e945b --- /dev/null +++ b/trees/dt/dt-0046.tree @@ -0,0 +1,9 @@ +\import{dt-macros} +\taxon{Definition} +\title{Ideal completion} +\author{liamoc} + \p{The \em{ideal completion} of a set #{A}, written sometimes as #{\mathsf{Id}(A)}, is the set of all [ideal](dt-0048) subsets of #{A}, i.e.: +##{ +\mathsf{Id}(A) = \Set{ X \subseteq A \mid X\ \text{is ideal}} +} +} \ No newline at end of file diff --git a/trees/dt/dt-0047.tree b/trees/dt/dt-0047.tree new file mode 100644 index 0000000..a178908 --- /dev/null +++ b/trees/dt/dt-0047.tree @@ -0,0 +1,4 @@ +\taxon{Definition} +\author{liamoc} +\title{Down-closure} +\p{ Given a [poset](dm-0004) #{Y}, a set #{X \subseteq Y} is \em{down-closed} iff, for all #{x \in X}, any #{y \sqsubseteq x} is in #{X}.} \ No newline at end of file diff --git a/trees/dt/dt-0048.tree b/trees/dt/dt-0048.tree new file mode 100644 index 0000000..0b21564 --- /dev/null +++ b/trees/dt/dt-0048.tree @@ -0,0 +1,4 @@ +\taxon{Definition} +\author{liamoc} +\title{Ideal} +\p{ A set is \em{ideal} iff it is both [down-closed](dt-0047) and [directed](dt-0010).} \ No newline at end of file diff --git a/trees/dt/dt-0049.tree b/trees/dt/dt-0049.tree new file mode 100644 index 0000000..b8ad5fc --- /dev/null +++ b/trees/dt/dt-0049.tree @@ -0,0 +1,7 @@ +\import{dt-macros} +\author{liamoc} +\taxon{Theorem} +\title{Representation theorem for [algebraic](dt-0041) [cpos](dt-001D)} +\p{ Every [algebraic](dt-0041) [cpo](dt-001D) #{D} is [isomorphic](dt-002E) to the [ideal completion](dt-0046) of its [compact](dt-003U) elements, ordered by subset inclusion. That is, #{\mathsf{Id}(K(D))} is an [algebraic](dt-0041) [cpo](dt-001D) such that #{D \simeq \mathsf{Id}(K(D)) +}. +} \ No newline at end of file diff --git a/trees/dt/dt-004A.tree b/trees/dt/dt-004A.tree new file mode 100644 index 0000000..15deb7c --- /dev/null +++ b/trees/dt/dt-004A.tree @@ -0,0 +1,6 @@ +\import{dt-macros} +\taxon{Definition} +\author{liamoc} +\title{Basis} +\p{A set of [compact](dt-003U) elements #{X \subseteq \compact{A}} is a \em{basis} for a [cpo](dt-001D) #{A} iff for all #{x\in A}, #{x= \bigsqcup\Set{a \in X \mid a \sqsubseteq x}}. +} diff --git a/trees/dt/dt-004B.tree b/trees/dt/dt-004B.tree new file mode 100644 index 0000000..14b27fe --- /dev/null +++ b/trees/dt/dt-004B.tree @@ -0,0 +1,9 @@ +\import{dt-macros} +\author{liamoc} +\taxon{Theorem} +\title{Compact basis for algebraic cpos} +\p{ If #{X} is a [basis](dt-004A) for #{A}, then #{A} is [algebraic](dt-0041) and #{\compact{A} = X}. +} +\proofblock{ +\p{If #{a \in \compact{A}}, then #{\bigsqcup M = a} where #{M = \Set{ x \in X \mid x \sqsubseteq a }}, as #{X} is a [basis](dt-004A). Since #{a} is [compact](dt-003U), #{a \sqsubseteq b} for some #{b \in M}. But since #{a} is the [lub](dt-0017) of #{M}, #{b \sqsubseteq a} as well. By [antisymmetry](dm-0003) #{a = b}, hence #{a \in X}. Thus #{\compact{A} \subseteq X}, so #{\compact{A} = X} and #{A} is [algebraic](dt-0041). +}} \ No newline at end of file diff --git a/trees/dt/dt-004C.tree b/trees/dt/dt-004C.tree new file mode 100644 index 0000000..4a4fc31 --- /dev/null +++ b/trees/dt/dt-004C.tree @@ -0,0 +1,37 @@ +\import{dt-macros} +\import{table-macros} +\author{liamoc} +\taxon{Theorem} +\title{Closure of algebraic cpos under product} +\p{If #{D} and #{E} are [algebraic](dt-0041) [cpos](dt-001D), then so is their product construction #{D \times E}.} +\proofblock{ +\p{In the following proof, we show that #{\compact{D} \times \compact{E}} is a [basis](dt-004A) for the [product](dt-0021) #{D \times E} and thereby show via \ref{dt-004B} that #{D \times E} is [algebraic](dt-0041) if #{D} and #{E} are.} +\ol{ +\li{ + #{\compact{D} \times \compact{E} \subseteq \compact{D \times E}}: Let #{(x,y) \in \compact{D} \times \compact{E}}. To show that #{(x,y)} is [compact](dt-003U), let us assume that #{(x,y) \in \bigsqcup X} where #{X \subseteq D \times E} is [directed](dt-0010). We must show that there exists some element #{e} of #{X} such that our #{(x,y) \sqsubseteq e}. As #{(x,y) \in \bigsqcup X}, by the definition of [lub](dt-0017) on [products](dt-0021) we can conclude that: + ##{\begin{array}{lcl} + x & \sqsubseteq & \bigsqcup \pi_0\lsquare X\rsquare \\ + y & \sqsubseteq & \bigsqcup \pi_1[X] + \end{array}} + Here we use the notation #{f[X]} to indicate the image of a function on a set, i.e. #{\Set{ f(v) \mid v \in X }}.\br + + Since #{x} and #{y} are both [compact](dt-003U), there must exist #{x' \in \pi_0\lsquare X\rsquare} and #{y' \in \pi_1\lsquare X\rsquare} such that #{x \sqsubseteq x'} and #{y \sqsubseteq y'}. While it does not follow that #{(x', y') \in X}, we know that there must exist a pair #{(a,b) \in X} such that #{x' \sqsubseteq a} and #{y' \sqsubseteq b} as #{X} is [directed](dt-0010). Hence #{(a,b)} can be our element #{e \in X} that is approximated by #{(x,y)}, i.e. #{(x,y) \sqsubseteq (a,b)}. +} +\li{ + #{\downset{x,y}} is directed for all #{(x,y) \in D \times E}: +##{\begin{array}{lcl} + \downset{x,y} &= & \Set{ (a,b) \in \compact{D} \times \compact{E} \mid (a,b) \sqsubseteq (x,y) } \\ + & = & \{ a \in \compact{D} \mid a \sqsubseteq x \} \times \Set{ b \in \compact{E} \mid b \sqsubseteq y }\\ + & = & \downset{x} \times \downset{y} + \end{array}} + Because #{D} and #{E} are [algebraic](dt-0041), #{\downset{x}} and #{\downset{y}} are [directed](dt-0010). As directedness is closed under [product](dt-002K), #{\downset{x,y}} is [directed](dt-0010) too. +} +\li{#{(x,y) = \bigsqcup\downset{x,y}} +Starting from the right hand side: +##{\begin{array}{lclr} +\bigsqcup \downset{x,y} & = & \bigsqcup(\downset{x} \times \downset{y}) & \text{(part 2)}\\ + & = & (\bigsqcup(\downset{x}, \bigsqcup\downset{y})) & \text{(lub on products)}\\ + & = & (x,y) & \text{($D$, $E$ are {algebraic})} +\end{array}}} +} +} \ No newline at end of file diff --git a/trees/dt/dt-004D.tree b/trees/dt/dt-004D.tree new file mode 100644 index 0000000..bf9ad26 --- /dev/null +++ b/trees/dt/dt-004D.tree @@ -0,0 +1,18 @@ +\import{dt-macros} +\taxon{Aside} +\author{liamoc} +\title{Scott's original solution: using complete lattices} +\p{The lack of closure of [algebraicity](dt-0041) under the ([continuous](dt-001J)) function arrow, [strict](dt-000K) or non-[strict](dt-000K), is not satisfying as it means that our semantic domains are not guaranteed to be [algebraic](dt-0041) even if they are composed from [algebraic](dt-0041) [cpos](dt-001D). Instead, we must replace [algebraic](dt-0041) [cpos](dt-001D) with something stronger still.} +\p{Scott's original solution to this lack of closure was to use a \em{complete lattice} instead of [cpos](dt-001D), i.e. requiring [lubs](dt-0017) for all subsets, not just [directed](dt-0010) ones. This solves the problem with #{\contto} but introduces new problems: +\ol{ +\li{ Complete lattices need a \em{top} element #{\top}, but adding a fictitious top (representing inconsistent information) to [cpos](dt-001D) like #{\mathbb{B}_\bot} is strange.} +\li{ Extending the functions that capture our primitive semantic operationsto complete lattices can spoil nice algebraic properties. Consider these two possible implementations of #{\mathsf{ite}}, the function for the semantics of an #{\syn{if}} expression: +##{ +\mathsf{ite}(\top,x,y) = x \sqcup y\quad\quad\quad \quad\quad \mathsf{ite}(\top,x,y) = \top +} +Either of these solutions results in the failure of useful and expected laws for #{\mathsf{if}} expressions. For example, the left definition above results in the failure of the common equation to eliminate unreachable cases: ##{\mathsf{ite}(b, \mathsf{ite}(b,x,y),z) = \mathsf{ite}(b,x,z) } +And the second definition above results in the failure of this equation that removes redundant checks: +##{\mathsf{ite}(b,x,x) = x} +} +\li{ The power domain construction (TODO) does not generalise to complete lattices, so semantics for non-deterministic programs are difficult in this setting. } +}} diff --git a/trees/dt/dt-004E.tree b/trees/dt/dt-004E.tree new file mode 100644 index 0000000..0541bb0 --- /dev/null +++ b/trees/dt/dt-004E.tree @@ -0,0 +1,5 @@ +\import{dt-macros} +\taxon{Definition} +\author{liamoc} +\title{Consistent completeness} +\p{A [poset](dm-0004) #{A} is \em{consistent complete} (or \em{bounded complete}) iff #{\bigsqcup X} exists for all [consistent](dt-0013) #{X \subseteq A}. That is, any set with \em{an} [upper bound](dm-000C) (a [consistent](dt-0013) set) has a [\em{least} upper bound](dt-0017).} \ No newline at end of file diff --git a/trees/dt/dt-004F.tree b/trees/dt/dt-004F.tree new file mode 100644 index 0000000..a056d4b --- /dev/null +++ b/trees/dt/dt-004F.tree @@ -0,0 +1,43 @@ +\import{dt-macros} +\import{table-macros} +\taxon{Example} +\author{liamoc} +\title{Consistent completeness vs directed completeness} +\figure{ +\tableW{ + \tr{ + \td{ + \tex{\usepackage{tikz-cd}}{\begin{tikzcd}[column sep=1em] + \quad \\ + 2 \ar[u,-,thick,dotted] \\ + 1 \ar[u,-,thick] \\ + 0 \ar[u,-,thick] \\ + \end{tikzcd}} + } + \td{ + \tex{\usepackage{tikz-cd}}{\begin{tikzcd}[column sep=1em] + \quad\\ + \bullet && \bullet \\ + \bullet \ar[u,-,thick]\ar[urr,-,thick] && \bullet \ar[ull,-,thick]\ar[u,-,thick] \\ + &\bullet \ar[ul,-,thick]\ar[ur,-,thick] \\ + \end{tikzcd} + }} + } + \tr{ + \td{ + [consistent complete](dt-004E) + } + \td{ + not [consistent complete](dt-004E) + } + } + \tr{ + \td{ + not [directed complete](dt-001D) + } + \td{ + [directed complete](dt-001D) + } + } +} +} diff --git a/trees/dt/dt-004G.tree b/trees/dt/dt-004G.tree new file mode 100644 index 0000000..db054e5 --- /dev/null +++ b/trees/dt/dt-004G.tree @@ -0,0 +1,26 @@ +\import{dt-macros} +\import{table-macros} +\taxon{Definition} +\title{Scott domain} +\author{liamoc} + +\[class]{sidefigure}[src]{\route-asset{assets/c3po.png}} + +\p{A [cpo](dt-001D) #{D} is a \em{Scott domain} iff: +\ol{ + \li{ #{D} is [#{\omega}-algebraic](dt-0041), } + \li{ #{D} is [consistent complete](dt-004E), } +} + In other words, \em{Scott domains} can be summed up by the acronym: +} +\[class]{constrainfigure}{ +\tex{\usepackage{tikz}\usepackage{amsmath}}{ +\begin{tikzpicture} +\node (a) at (5,3) {\Large $\text{ac}^3\text{po}$}; +\node (b1) at (0,-1) {\Large $\omega$-\textbf{\textcolor{orange}{a}}lgebraic }; +\node (b2) at (4,-1) {\Large \textbf{\textcolor{orange}{c}}onsistent-\textbf{\textcolor{orange}{c}}omplete }; +\node (b3) at (9.2,-1) {\Large \textbf{\textcolor{orange}{c}}omplete \textbf{\textcolor{orange}{p}}artial \textbf{\textcolor{orange}{o}}rder }; +\draw[thick,-] (b1) -- (a) (b2) -- (a) (b3) -- (a); +\end{tikzpicture} +} +} \ No newline at end of file diff --git a/trees/dt/dt-004H.tree b/trees/dt/dt-004H.tree new file mode 100644 index 0000000..de419a9 --- /dev/null +++ b/trees/dt/dt-004H.tree @@ -0,0 +1,3 @@ +\taxon{Remark} +\author{liamoc} +\p{The second requirement in \ref{dt-004G} can, in light of the first, be expressed equivalently as: #{x \sqcup y} exists for all [consistent](dt-0013) #{x,y \in D}. This is useful when needing to show that a given [cpo](dt-001D) is a [Scott domain](dt-004G).} diff --git a/trees/dt/dt-004I.tree b/trees/dt/dt-004I.tree new file mode 100644 index 0000000..54b6ef7 --- /dev/null +++ b/trees/dt/dt-004I.tree @@ -0,0 +1,5 @@ +\import{dt-macros} +\taxon{Theorem} +\author{liamoc} +\p{[Scott domains](dt-004G) are closed under all our [cpo](dt-001D) constructions, including [sums](dt-0031) #{+}, [products](dt-0021) #{\times}, [continuous functions](dt-002L) #{\contto}, [smash sums](dt-003H) #{\oplus}, [smash products](dt-003G) #{\otimes} and [strict functions](dt-003F) #{\strictto}. +} \ No newline at end of file diff --git a/trees/dt/dt-macros.tree b/trees/dt/dt-macros.tree index fe2c17f..32c0721 100644 --- a/trees/dt/dt-macros.tree +++ b/trees/dt/dt-macros.tree @@ -21,6 +21,12 @@ \subtree{\taxon{Upshot} \body }}} +\def\problemblock[body]{\scope{ +\put\transclude/toc{false} +\put\transclude/numbered{false} +\subtree{\taxon{Problem} +\body +}}} \def\solnblock[body]{\scope{ \put\transclude/toc{false} \put\transclude/numbered{false} @@ -28,6 +34,8 @@ \subtree{\taxon{Solution} \body }}} +\def\downset[body]{#{\mathop{\downarrow}(\body)}} +\def\downsetB[body]{#{\mathop{\downarrow}\left(\body\right)}} \def\pow[body]{#{\mathcal{P}(\body)}} \def\sems[body]{#{\llbracket \body \rrbracket}} \def\nat{#{\mathbb{N}}} diff --git a/trees/table-macros.tree b/trees/table-macros.tree index 1b890b0..0b41915 100644 --- a/trees/table-macros.tree +++ b/trees/table-macros.tree @@ -3,6 +3,10 @@ \def\table[body]{ \{\body} } +\def\tableW[body]{ + \[width]{100\startverb% + \stopverb}{\body} +} \def\small[body]{ \{\body} }