From f58769b862df3ecb387c5e209e8a947b244fa12f Mon Sep 17 00:00:00 2001 From: Marco Realacci Date: Mon, 28 Apr 2025 17:56:27 +0200 Subject: [PATCH] vault backup: 2025-04-28 17:56:27 --- .obsidian/app.json | 12 ++++++++++++ .obsidian/workspace.json | 5 +++-- .../notes/13 - Weak Bisimilarity.md | 7 +++++++ Pasted image 20250428175449.png | Bin 0 -> 18330 bytes 4 files changed, 22 insertions(+), 2 deletions(-) create mode 100644 Pasted image 20250428175449.png diff --git a/.obsidian/app.json b/.obsidian/app.json index e69de29..88a03a4 100644 --- a/.obsidian/app.json +++ b/.obsidian/app.json @@ -0,0 +1,12 @@ +{ + "alwaysUpdateLinks": true, + "pdfExportSettings": { + "includeName": true, + "pageSize": "A4", + "landscape": false, + "margin": "0", + "downscalePercent": 84 + }, + "useMarkdownLinks": true, + "newLinkFormat": "relative" +} \ No newline at end of file diff --git a/.obsidian/workspace.json b/.obsidian/workspace.json index f83ad92..9107af6 100644 --- a/.obsidian/workspace.json +++ b/.obsidian/workspace.json @@ -6,7 +6,7 @@ { "id": "ceb8ca67f2b32f40", "type": "tabs", - "dimension": 40.83094555873926, + "dimension": 59.43977591036415, "children": [ { "id": "56150e6df7869900", @@ -27,7 +27,7 @@ { "id": "e6a32eeb8d1da29c", "type": "tabs", - "dimension": 59.16905444126075, + "dimension": 40.56022408963585, "children": [ { "id": "6c4a39240e6da514", @@ -213,6 +213,7 @@ }, "active": "56150e6df7869900", "lastOpenFiles": [ + "Pasted image 20250428175449.png", "Concurrent Systems/slides/class 13.pdf", "Concurrent Systems/notes/13 - Weak Bisimilarity.md", "Pasted image 20250428085837.png", diff --git a/Concurrent Systems/notes/13 - Weak Bisimilarity.md b/Concurrent Systems/notes/13 - Weak Bisimilarity.md index d90616e..c3f701f 100644 --- a/Concurrent Systems/notes/13 - Weak Bisimilarity.md +++ b/Concurrent Systems/notes/13 - Weak Bisimilarity.md @@ -96,3 +96,10 @@ Furthermore, we should also consider commutativity of parallel in pairs of the s Thus, R is actually made up of 1+6+2+2+9+6+6+2 = 34 pairs. *exercise: write down the LTSs* +### EXAMPLE: Lottery +We want to model a lottery L where we can select any ball from a bag that contains n balls; after every extraction, the extracted ball is put back in the bag and the procedure is repeated. + +The specification is: $$L \triangleq \tau.\bar{p_{1}}L+\tau.\bar{p_{2}}.L+\dots+\tau.\bar{p_{n}}.L$$ +where $\tau$'s represent ball extractions and $\tilde{p_{i}}$ is the action that communicates with the value of the extracted ball. The LTS resulting from this specification is: +![](../../Pasted%20image%2020250428175449.png) + diff --git a/Pasted image 20250428175449.png b/Pasted image 20250428175449.png new file mode 100644 index 0000000000000000000000000000000000000000..0882ff4fa3795335d650ad31cf6a49dfebb6e54a GIT binary patch literal 18330 zcmb`vhdRCn6#`a9L4Kors9|I)2|nwg$MtV_R(b9x{5S`6#l_dJ|kz*{0iyf2DRk!au~=dp!f-!|Nv z%-8r!p^*Js!Cksy|Hb~rLc+wcPkMC5M6T;)+h&A4zS6=JEQ|${L#~2s z?*BG_o!DO52{AEoHN~GeGtm{;)s{usH<0MKx0e6ws}fv`%EUkN{F5K8B|v$o-cy#F zW-=m3r|RK;YWdFngl~UN&R5+k5gH2KUhn+ib^S>8P@Y}KCol1aru$LeFHGL<^ObgD zD(4f-VBh*07@NP9NJj7*Xym&u)>k)PX+7BHKS_AkHD>Vi>5sl_agD`w9uf11lfKfk z#c89tSs&#|FU^w?3g!+>&1>e)Nj|oe96cvLwBE6wkbC0t&PcCrXhI`ly>ai(0`Ydt zd$x>u=~w2XsqTCVV{a)^7R+v~E!fofDpKsJ;h6Usoo##Q-_=C3J&`;3iZ98fLeub! zS;eoqqQ+n6<`+F9_g>xEJUuMxp|)x8^k90@5M5VW>e^Cu)9kiJZlS=s$kt)-p75u@@@4K_LPrA_j%G& zg<1RD%G&W(qr1a-gls?kt*t$-d==F@U7U@Ihsc`5b8p?U*>Db0)ws=hr*f+^L{!H5 zL`_pmQ(>vI>a+b1?s0!J7;d*@I=PSh4EJwu>&R5z^Ag4CGQ#%r6b=@iB#%?>-b;;t zdeZ)k{YmEiX4VpWS$8Ic9=kSOAk2EbNVKzJNm%*L*W6H3Gqp_PI84OC!ouovl8v;1 zrY0)f-{j#a{zy>HcKqik14qgHeOtlPy;uGchxB;4KkLqM@~QrEwj3gyJjp zOhX3EObw+p^)&VSA}m~ymnSccnp8$t3sA~D`S9U`_ttL%YBotZHM$QfY3dnQZkG&#WZ=d^saz*`O8IAyMqC?HPM^3+Y_@Pgsx26-I$hp3{Dk3WSp7OZ((YEGh z@*^K!B&%n7?QE^+7F!>tr?(z>cf0B7i6i`a+GP&^2@q&$X^%>{6&lxtw70kS_iHOC zG$e{Shsbfr9w8)6STgfQO^=N&Zm!uAWFE?;MnxT#%_+!k%MdVjDl|LdpDS%Gg)WWLPztzDrBH z-4c5(MU~R3T0xCYhGtaiIuBiS07IA0tGqwnBCgfQv24=pQ~Hn6%_azX=5AG zIujBSrn)lhOZ9A9I=i~8?%gY!RA-a?WyvfQ_tmYgl9_syAuv;e7ysR$s559Z6)M%E z@}eap)EfxIDU#bWk>Y0Nd)~@=D@z8~omX=;Uvssn*{{4H4z?N~ROA5)FSril$ z!Ezi7bApsvIXPdxd|6&uIe+F%x%)~E{<^>aUKe{A85t9km+|q;_c-P<|^L2x3+Kc5Y|Z7i`4r~&-D7bo3FI0hQ{LjcuPn~NLg9g z$B!TD>n{n#eKyYTzxTeNpy1k>oSYo2uduN2S*Gl?2rFfO`ZGt}YE7TCj0Xe+9KZA^ z_MBz!og`1q8#f%6{|wkvu5od4zRJn@JKhrGPfBf;uRYpoZjSOepe3o|PSooavoM$0 zGhJU_Usza}rImZD)GqDq+eepP-qh6%3JhEq{)s35^XIFM7waqUo$b*hrFyqe1pUft zY7xnCg@tEn7@Lgq-4-Vg($Ue;(2UN`&W?={e!SGJ{O+v%OM77%FA{PkhF`zZW3AeE zFCF>qrRknS+$x+AijN;Z#;K2ph#1wdD0(iNLdh)rsNv_qGAi(>a%d67DlhB5nuuMMVO)fx(TyM>)um}q0WU^lk5FhSUp za;NQunwr{ig|Nbcf|p%WgKO;Bw=Z!;y0-e=@R-$;rvaiZ{^6`R~{Jj*hp5;^a8~weoEB#{5mSu(=xJ`lpQ4Mn_x! z(~&$hQVyyu&^*}OON(N|@p*w5FR3bnSj?%lITa%a=tS9)%9 zZQ;?QM`&A{o0|sSTaH*cVq)T&nwpf96bbj`!n{1gf`M#(Po=bXHY1h#4xZZ=ar$oz z_J^#qHTknQqU$ct3>{%(8)X~{)7KdFv zFi_UNxsg@<%R_NM!8Acscfm1lMI0sZcEd>*}6DRVUHh6xGnPd*J$S(*L7!JU-R%P-hcKz z3azk^a{vA~VXHwDip|%O`&jpqk`k;Y34!p4LC|<^v_}8D$gBhwd#{d^y6DKuPNo3a z`gsB>mzS<4h(xqablokqULGJWnJ+p(*z%^_7whdc$*4+qIJ6Gun~Ci~R#w)bLx&7L zxI`o+*_fNJwVoe&#CRs%o!axkFR>rkqp7J2#-AQ`cX#8&rlqA>efzLhwX-#wXH?5^ z{5TFwlUYG|+;(~JR_}PHUD4(M)i?#g59^@BNqhDD<0sFaEiO)7M;nh)!fXm}_|1Fl z5^IobN=a#{yn@2c`tRJ0<(YV4E1erRZrr=~2j4rIPj`8=W^a+sRe+D?zSeI&PA3i0 z)Dth*|N7M$|J;$rkb#Rfm|w4ioi-Rnf(LnjZ$JpRsa8$WN12P6nK>vZ$fiH=%~7e&_O$X(eXY!8X*E|><)cP-^~x17ug#K}n3(## z#N-qdkx!qxh~H9H{#nKt57{*JiMFKEF)io% z-vkB*=H=xP?)%`_(fph>7LiEJ%Oz=1oh0aA7@-nB#D& zW>$dgF@_02%DsEMlJ?4TbhJtBcr5(7Dirr;bTnC}fjQ8KHuzIR!$hBf_v42TCztsv zr~{O_HrCg3wDW)b87Q#-^;t&EVd%Y8M@L81*0S#H+iAD5zkHBFg^&jtSrnD!Qw)j}FKbPp_TUuIT zPTlN$=l;2~bH2u(l<8iSQrcjZw^V2ylZ2atrY3#kgUp%*XDKEoCd|sst*t4Cvc$yU z>7Fcu3bz1Zf5(H0mc4H~^ovcTeR9iFQj9PmvMv88rm15UPoF-`8#VarTeZL`8Zz2L zhrBocHJrKg1>nf`VR`w+tILtnKki)hWmi;F>liL~W|Q*z{PSP6X0P>ozib%>%D{|_ ziP0MW$B!P}`rvYZ;a4l(3~2h_n#YVO`HYB*8I=_Prjn8pfDb;sEm5q`4XBCz%9WPy zwL$)GZ_p5Y<+{}~3rk8wPM$o;&8={XzL<)b;k@Yw3`0AQe^s+!&2)o{JqJhfn(X`AOTU`BnOztm=|cEBqh8pl^&< zO7lxwjc!O?8r;_HQt{1`YG*ZMsQ+#&t#kMB-XE^~`elVyL+^o5u$8B8zI%o7QL?&o zFiv@StSM5z+-bPverH8fMQm25>iTaz6xpFE)<5BM=Y z?zp~aUeU^)ti?{Ie)DFj(~ORAyp^db-JwI*H8sajDEn>4rh9sO^eD3Sw0h>&XH(6PhhK7b#R#vjIA0xT1 zt$I`fcvZH>f^L3bCG(3_POqx+*4Ea>n41|YK155aeJZ-V-2INtO$9X#-YDU7=l-K3 zUmIyx4&4;p^9Tceb}0 z!r6k1ToxxgaB%;vtjvDkI|-B|=KNRr@@3boje^$GxfyRc)ipG_6E4^&!BLZ8Ex>`%uIIBzXd&hXB=q!iu1Lzy;9XH6_vsx?EiJH6ZH@>QahLXwA5*Um zQ<#{T*xTDn%PV>7pXMKRI3ay+x18LUrt1s^)|Y-e zug)2Pssoi0y37W^w!Y(NlbT zYi*sJmOlj_x_K%(IJgPrh;J>nVGj23%T@%COEx9%Yu?k#gs7MNS=E-2&~mDmvvk zuV42U+azUW{RZgnJ-qP!X_Kk9w|9!F3o7mD)2A33H?_4V^CU{mp5js+CYL9 z7vE-P8s%$q(q^_u+({&lb%9iXx5JSj^FxctF{pYG6?NO#*x1CRi;?2q?c2A5s95Lc z=b6Nu?r9BBuk@yEgQL5z{1s$))ZVVDFR4>@?!qE@kxpWCbZ@z{4bx+KV1<~NBZm$Z z0M|}WTM%R%hDEpJ`C}Ry8dm-e$JZFf#>clMNlBqsWolUTCVK+J``4^4c3nF`8~o+! zc$n?VUwthtEnVFq;PA;g|520eBzCf0@C`C?$J7+_+YBXwhH>D)0n5G|&-t#$K4fQuXJgg9YbXdN@ z!zVG3)uo?~TplOE@qJ@P7QaHSkI`!VW9G`r%2V`~pr(&JA6)J}HUP8pE9z)_a}8wS<)z0Vj~;>D>`m+oaw4W952!OfckbMj(c5oQ z>e|{2Y-|QvT0!g&WmAZnw4iAKAS5Iv?iVFKW2nK~gX4LMj}ObF^;Y|zX5Yb(RKWQ2 zf`Z2)6v15XU%q^q``o2d^lb?jB3s5^h`U0NI!s5WoG2RAYUaOs^V+qxi$PR?jE=_) zj{C85L`;GoUks!a6cjWPU;zH^$8(yS|3_KN=Jq}{m4l5f37{BYi~r7ymWIZuo9{mL z_cORiC~`gx3Ti-ybhtaioHHM#G#+>64n&O4t*wAy1O5H0&afc ziKoxs4g9$#xi*GDQC1O5^2Q@goso@g_U~V7Bcpt?*5`m~&XmUmDEqp*zkYD-s;jFT z8e%s6(&OR|NY;iau)S`{5UBeF-IYz!Lj(lp_3PJQ2$1+rp3FkC2t(i{;U3$5n?;{b*BjZlZA@9IN-yuNh6uo0pbDfLn1IH9_4-(JY32*iCxhlaj)R!mGcMfJl)YMzjzQeIyh z8}9-o&;}EfV*z*o`Bza#zVGDA02LSlL53nDBb{fzNqDTq9N#CyQ%DAR=<3{$a zignOzx6W&fUvEhi>3Gfz7NO-;K>)>h0DzitPrv+0;MDQsCcSTO=H99h#i?sx^M3oE z6kDJXHX8&1y$Nk?X=%xG;Q;&T$2!?xnwl=)J9&6~fWlcm{-L5`NnoIBg!skzOpSHS zC`|dUSWu8q=sg`B`PY&pcZp_K26a-~d0}Def)L_#{enAfUg&V2@xVT4!f#I|=X$c%!OH)7W$@ zO6f3p0Cc!Y&WRdIo8fPei@UoW#+#$i(AgYH(74K-_~MjbT(D19&$aQG*)v?pJkR6eO7YJgJRo4+?Y5=&LP#Q=tE5G~NFig9;B5S|<2+95T-+%x9{e$S&)^?hM<6~W2 z+V$&uQ+eKKX5HY8Qs%;Ax&8Yg4_y!v3CIp*Emjl94zy@wWankLBsn>`alwG0L9K2V z=`?jEi;Ebwrwl5;*4L-APN-#SjCk*CVf*PpzU;=89-C^mw6!G( znp|>pbVPwwRqeP-@-qbPC-?z~v*Hld)EGf`V}BdfevWu=g!U=^Q>O^~T{}BFAqEG? zro_d?;Vc9NDHs|i=jP@@zeA%yG zLnLLPYUtDtgs*>Lk6d<^(BZ(OMeCy(AL?`TJLS~#(wAL=d)1V!EbPsP|xjk#9`8L%F$2@ zV`F2ZqnDwyH#aK*O}y+7VF`mg{68fMB5`77W@eKC12eOKICcF{bkYuk2xm;o?|AdO zcXylZ+WhU%!8G;%V($aNi-?H0xVd3cEMq6@>jN*nbR1?SkQ}UC!K2*B(v-lXqC4Z! ze;fKT!G?eq0Dr;v@G8|e7ly#Dt}a2!ja7h1jY1j%`k~j#urov8)_lw95ziIYU^ym9 z4;QT?Qb4d>Q)ij@J}|=hkj1%sR?q;txFKc?lo?Wt3zO7wED6~V#5 zadC|Ct?7k({Mc`w3DM+<$Cl&V96o&bMr-4^9eIGPB`T*rlTkrI0Ye_#_h@*ZP-(lp z`?vO}k^cS?z!ykumsMocLN6vJ1a*q2i%kpy;7-@84Za9(>c2CxO&&xVo0A z^4znqXl`k7pC1cW=DN-s1cr{#?XMu zhv$c-WUTt3Nby!*l;?RZ$;RF?*M(ouQdig4|MutCwzOpZbPknGA?({H821^nr`Nx_ zBdltYfkprzVCaB`AXhVz;ZadNAhXY(Kc`}o{NOOviSz01=H@gtF@F`7&iylxhOM^K z)HA22r{Bb9f~o+wW@egOSoj$+&~fcM#*8vsKLTYIlj;K_RnT59fP80lVIzrGVkZrF zqmGK$8cuvkWVcoFH_ij;badReebn83!zqbA@cY=9X^{>q3(MD<&Mcf7pwdI+0q6!& zn{&0hU??GhERYz8V_}W2SMSPEuhD2y9}jI)p*SEW`--B|K87w1uJLo(KIPk(BcJN) zA?}{I5}n;^_Ur%80#GstNc)rIfe(gXD6Y4+*Ri#5mXbD@Q%WkS&e-?a64O0q zf($U~t_>NI3ckj7@?_U&)BQ5iVTCoAhTPnDASGfA!1x)3Ocn3g1Qiw)-N@>}mu5uh zYx8i-H#a>F9g6(YZ+3+vBK74<4C$`UPL)K_6Hpc1y%KU%R@5rxI0j1X?^s*o$e3g( z$E604XyEXH1w2S+mfYP^}bx$ElO_pe{|F7_w;n%Fi& zc^Ikm1O=idCx`9~ojHoW*PQRvsn;47P(#GNZU|6<_0f<$0I4;1dOEU)Amh2Q%zE~& zD&{>jrYNNo{9XyxX&78K!(~OVY=q-0Oq*zN+Gpgl{U3Zl?ZRli7>;=uepCVk4i%Kx zr*q~^fq7RtXtEwmBH*k};`XYcvFG&uL!XH?Ln$ehi=pr0)spN{k9mo!kW--zvmlo!=}lV`OHwoar>Q z5$0iClOZ)`;G!dkP=^H@sKV65Z(Ave^P@?-a7s(gTGeWGoNAdNX^BbaI2h5TUXqPx2D$mbe z-Uz|o;|_zJO8#A0^zhl%j`w^VD{SrfI3cCd~EC~ zox+E(?Fz$`xh|^Ft*%K5CfA7>pzI0W9upS)BX<{k3FKb)ZS+jROpyZNg?40z2*&I=_vEFAg_I^&g;% zGR5(U_=k1I1Q~!!$?mUk>SR+eUIzR7?<%axaoh*EsM?%wfyIwd6D(qx)5Pag3WUxW z9i}|UZsb4b;jxM5FZxp>NGRlFpbe(OWTm6)UY8G$%?F4CP2fZK{P2`0y zF)~^d}cEP?&ZtlG74wUo_*b8fdB$E>q3C65zKP*X1Kk*fkHxYEJu%eO}3{1=c5dU zYHDPt71Vg6m<}I?sybEniz$PS{2Y&nqGfc1Op3%Ekwp@4)SjLQMb5l;J@f13ZT?36 zQ75%Pmne-j9Ab@j9RZmq!ovd_>=0r&B2YbdikvfTg~!Oq$;k5Z^P7P3d3iY|nN(ktd`M3IYh&V`8#^hfGm@eX@MNd!z1dYHh=xQ@X5NnHMGnqqLdC$Qp(YA9y^x8I`H7^o?yA>LbpSLGPr}4>&X}* z>mI!jsOjuf=YA}x>`?kffh%&&V>^jBo@brv1cC$z|A2qUUAi<~`|B}c06%^hb43n> z39@~*R#sMa5HY%MYbziuta9yIj8d9taHKDLV_n?|e*VAc&p5I003x}rrgq#Fo$We6 zs?VFGlvY+!V#p938QIm{O-OL!34xVL8{GYFBX;lfQH4 z4(27br?#&_D`ZqHw30>~8W2NhGwd{X&-j&`ljG4l0)JSyWUJAv)&SvsYB)`Io$M)3*=%w3EMH)628 z15U)Mvw`9r9@fv)pg(-r{Fo1lW4NAbbTX!hx>*ggnj3*D%`-slHHOL{^I5r-c1}(t zv!z~JZkQ;_%8!DANM)#fjNr$G))>0DxOhx@9iyz3w)0}OKD#H{33}e+ODF&PFQR2U zv5$dH9)eJkggaN15@cflc886c`-}2x)m;m}bF1nR*Dy6*oEdUPuf+@UnYdrPSPT0H zhT+HB+9lH~a6DZhip9ieZ8SUj32Fw3QC0VBZEcyK)j?E7k#qW09*-)Q$G4b;qnr}# zG-S}aP!o_bJ1#RFP7t1~lNeoCgZKYQ;8DNw@Ba)CrEqgAD=sdUTwNvtS^{06qM)!` zQISc^)wxJx3K`kRNKIXxgEklm2GO6q7DelSyxSx_Vku7=RD4EnJfFw$(=cPjU@&G$uY1w|!0Hw6` zwY6ZmRFGqpG6H4oh0+Ur#LpQ5ak`6giT+br(byhQyKy5bApvU8#ful0j2PKUn6ZBK z6AO6jA^l0(M?r){bhJHt_EbN$;68`M6FBWMUCVC zii(z%mQIPQvOU2U5)%;~nFQCUJkvhqVEARysXs%N2V`&bP(@p1@Up%!i1}U;%Dlq& zKWzEL#U-HK)P1*|+b8ZRefrm$cLN3@(g6yOnbIO(4cert@(2kD!DvN#ZDV;zn&y)k zW_qWqj60bhBA6J%6OVx-*ETkiMDBB(J9mR4;=zLlNS^)fEeh`1_Y7bXRv_9e@R&m- z_Yu|W*CP`Wlry>zXrKuEi_ijqt;d@-<9sOHSCo`QPrI>=ZNif$q6$+fBUce?ABk53 zN7L563k?A_8~1XGG<#!P+sfSBWaA(IOD_)w%jIjowI4qdrwrhZ5E|T|f2Av87O#Cy z#8bUsQz)36-D>>u#cOFg3dx1?axod|YJoo(!C(p~Bl8g@Ns;|=%81us(I>+AxgyPP z-`?lM;+!WaK&hpvDe1la;msQ*se<(%4vdyk5QCA&!|}SN>=`UKKllA2oM#~A<+%0g zb<9I-5a7C~7FnXogk33$3zTQ}+sQTSXG-Hx@c_v6_4QjP7VdnG6*T+I;Q6qie#&i^ zTtQBB5FKu52~8$NV@pWbL=FKAY#B)YcmXxE&2c;U(_?m}5NfEng-nG8K7UrmfYs0_ zbe~4s(bVik)~-OPfQ%t}NxUFAxq5h5LO?*ZYo<<+$g&Fl-|5qB_$SwlmkyKHwZ@;v zHcPEf9;XWGint!pWC~DEkm2R!m6kUg4@#~%EW!~1bL4@MHcpJf+bzW0`rI0ZC+!fR3YuVWg8FBMhU_?d&Brje>o7@IK7XK3C?7 zR7zuSPxj;nd%6nO59%NK;-xT_;5*%2-ivB$(4oMV$q2~MC6+%Fq}+|v;oKp82Jbc_ zf;Amt=PCNEpXBsYKR%rv)g1qu>s|&dr6oX$QtRbT+*;J)O$f)D(`_xLv8n zdPep)Drh#a%;3E1@n>{RxxK61lYy?tA9Li$5qtplJdxW@nq~}G0y>a^$3OXUlcga; zBcmE56!@&5;R^2@76$3be*0GR+zDcW3}16hlPT*TRcU^S)*`BgIgbrw-cnOPzGc)e z9(O!Z1&OdB;oaIo&&$0q^f5^w5m@0_p7W}Cp*w6 z77-?+kIL4UpkLC3e5s@lyOk2&oST`62?m>{?C}tEgI$l6jDU2Xq@*Mh3vH9>JMf-of9)h-7FUU)ozIWotQ-+%7hLkw!yH3k?oNMCj6Y|tX{{+ek`m(fCM#fJ?jF&>(a{!eFgDYu`z#k+h(d2;6uoj6&V(Q23 zkSN~O(C6oMD8f}TbhWj~0zSeVr_Um#Y+*X@CqP-7u@V^k?LW3Zve=C>yFY!sy+~l} z$g4R3FNcMNK^vj01S5>qzDROGf9N;D}&g zVzNMR14C|gbyd=HUEF(n6Q&QGs^EtY``_ITHM6H@CreH2C;q?pwYPs#q{KE3 zzPnA4sIr4Bo|u>)jbCzgwKOb3$agTC7cmUR9se&`2dViK%)qt@;6iYEj6JlQ`=xrV z!g~XatS-@vPVRTh@W}fp$GKa~(WD%i8gA3w|M^M_7=3&oJY*uaUrbC4zB}eM)@5{b zlzt6^6dLlu;7{oBEv7==-a8Ow&~d+Xbf^^oW>O-CKRVPqYJPu_t)hISIw~zvZ4v?& z1Y2+h4EpzZdF`@Q$kGBoI6|L8)DqGNG}Bu!xm(8hkr9J9fC~=|KXK{9p*~DM*#llg zimI(ml1z$ov(5EV8Ot`~>({TtUp6xO4v!uvv8ZcSHM2V}PXJUNH4Rhmo%Y-4HVPS< z(7NeAgjdpQbmaT~P<<5mgJ)6CeAZ+t#6ZdPxZY4e`rQGfpE)7~C@(%Irigrg^^o7o ztBcl7q|^Dyt#@bO%uYki1X-XWBhxOiO%X0=*4EL%8|PG3!US9xG|)gcDNP+V!srbd znz139DmZ*I0|gm?62QF(4;RP5fP@VOg9dFJu!5RJ#1`%*ir$4?`iT5&{q7rbMHVq$ z4l~k*;D_QqNQi^yRQ`LSkeVy9P3#*x`JcbNN$-c?VTwkMHh%kkfi4bBOLdSGw`Qq`jH+ zav}`@dd6UBs%*-`(9qop1IHbWve4j9Pha18PzIn8gb$CNF?-a@!om=EIZYjL(w805 z>DT`!>;$ClGHgXohCm2w^b~iIoB(qL$;D}62;8-%dwYcuxE&Z^EM6;TL9Gd-5nRm+ z1=<<}{=hHKP)S6Z7i!Y!qNHzZ|4aOZORi6%g7Hbr;x2iR2YYj<=B+T3&M;7pY7bO; zmTT}96%>@a{7cp2XA`j`ltr#9mQUFPn*P9$&&S~%K4;;u3cxx=IYIq`!M1_ z!L)DOSX!G%!rH5Hw+w3Vp5x_h{`6@K+kuhU{wocNj8a-^*Hm>W+1CS5lM!Xr#c)O- z49QKb&EC{Ni1A2n4nHOJ1mu9CsG_1Wcuzp3_=aSZ668~K0FDTUX&-9ZZB{8SaY4ad zqZv_(G9^|DnI{DW3rOn$Jt5;Lc3g5N8~I!M&>Osm|98oPA@ByiQ(xc4+8Uz4rN9uo zsKJV>4FM`0u->1qr3(vfQY%YKbyv4?9)9~TNs;rN_Nh`me)>=`T_SKp zJSDQ{t3N_dpN)5%xF{$j^jy-jEFwY;3gy+SkA<%v!>(OALqouKg#Pu`pz5dy)4)C9 z@CM*J%b98$3kx0C<48$h)k<9c87Cf*tDfR&CZ$eLN~0wYNED4lYenL{=+!GzqyR+k z|0xPoFHQ}EjIgPdt$8I)oj+zsXg_Gz zQ90YU-M0ZV058+UBzE~xlL`h;rYC&wY9=y?Hx(h?HyL0 z5LmTBaraD2_E!2r%E$5cf5XfWIQ+r2ps>*4-;X-N9+^}0*W!h*W@;Q2b>KO5iqemL z?!^~t&ajlX(=aBJH-WI@lzSO_xNvjB>F?M7=tJ>ABe)*q`9z```uKEr=5DwaJ*wdm zW7ohzA>gQ-9LT>zgM(-h41xA`b`a)wZ;Tn%_yIA(N%cgMg#B_2a1m5ZA=Abu(6+M2 znVCf$CVhzaiWWtP1Pc8+L`J~Xn2as}Quv4U*Z66Jk!)N-Hsav%OP>=iT+e0EFcrFR z_N)W+-GPAtwClvg!`Jy^kcCm@p@XAH=7;-I=4S^{kF2b$TG={|=zcq!6H}2z- zNQi{iHMh03ZBU3i6#q_jHj(5Jx|-1i!gVeOK^s?O?Gcu9b#b}(?L%DK#P2pAYPg<= zINq|eo42Xjf)Fu2Gc)Yk2f+leo{qe(x0l{88P^c}+a};PQXLi7=8bx)2w8I<*8(T4 zIdYUX%W~_gKUp$190M3z2|{K!atdz%*xo8seuqZ6aZq{q%B-1fy~ZAg`_>M88R_4 z7A=4Gy_+OF=_EtQ(0#nd9^3HwGob%9|7OxPC)`QEBdp96kH8O>rYXcHK6*r%H=~iQ z>CaEJ8O+`Y`UP%R^WCCo*R@B&qc(_|+d;@dbT=@un@K^o106V!igoaEAjH9Fr8ERk zh_ASTL_y(Nl}+?b4sXurxGR428j^(q-#_5K-c&}?QE?ZVg9r0*SZUrxKY22TEM(Qv z7J}2$=MDKrCz8Bx6t#PY+}kgk^Ws&5vCs$N*K5>G;+eUyTzQhs%i0zI%^Az{szD#)2UbL7Hkw7X1Le zpOZA63Ak->7A-$7G2Opq(2&V{sxuAI8YB@g!P;wU_cFB65O7t7WZynG_aMaxV?h4K zeF@lw$n!xApbaiWfT~S$13@C(2db;7Aud#+0I9)M#HBt1fZG24{)7aU#|C=>zoR)o zB7k2m&ecHF(V(l6qFNnm0J2_I}0%6lUA#oIt=1M-CZ|fq~M3 z$k3mY-0QDBXj;uoOs)eOMhI5nDs1cXbJt#oBNFo&FQ_|FOn|lRD?K_hBjNm4kHo*m zI3H+hKVgrmWWVA?cADwmzcDmO4=~BK^F!&zyu(Hyr#W2VUQE*RCxz$vix)YnJb-Er z+Ep|PL6f=jFoxqHJ7;AL-4_W-1@+m@LF1kXy!`hbYxBj{AHgfp~@}Czn0VI9T{?a zaZd^;eSg45FnMUf@*`Wi)xVh*E|dh!}PF& z$qle0`l2)$g_54W8=%@Xv8_H$8BdyUQdc)M1=oIuPj!X!>B>J@BZlY~FDlWr@ci;} za&KW^_Vuj{+j#;l0cRR9Z2u`}lYYO3>pM$WwIz3$qi_`q6CUhbg_Z|1il2sT_b%J_ z@5FjfXT(6iP(XD8r-X#mbKmp+xO-UH0CA`pv=K-oHP-FURg8h(ccXu^BS|V5;S7Qt zVq(lPPn_9sou^dqFEXcw3|=5}P_F8X|HU7n4Xwj#0ZWV6FP0NdL1=I=LOuP+5Fkz=_QgN- zE))gG=+I}70GN9vN)q~lw<SWPjo6in~HIto1(9xwm!>Fd5li+$xj81)be_ zi_)Dv!(HXMA)M4Ut8+*n`2|!aB-nWj7bN$Pk7nc5X9)cH;|Joxh}#a_dtaHxT`joi zDhcBXK}$P3AwPB)6me+d@y3^EQ(M6A{daXkG{h!Nj z8l0aWH~1Fj=3>!VNN2{tZLTURqEhA-7HTWjNe-mvBE-G1v4Kku*n%vLH@!QM{Um^7 z@j5q8X+kqVZt8TD(#XPR_6CyP+dyXb@89>392p)4KLMHCdyo(u8j5@z+!Ex7raue+ zm=tpp1%7#e5Gu?e1mB=hf$h?l)79poog*eu*U(TaAP$ZM#|6i}%KH>k?3qJlxY2nV zO%a=mOM(EA+mk)f0&2yh=|; z>XMRGv~cN#Jj-6WT$?K7TySH}ZgEnLKPEmV1_77%NV@@mySTffIk?~nK_=LP5{N&3 zw?*b06w__0^91hFBkA*Dr~zgdkOFiXAmOp;>5yyl2UsdJD{k!hDrrjm4Ivk4&p?)d zBD~?Jt%#M-%-FAAD)GYE7-7I%qM}SYRQDG>Ka=ji;A^zg+d+w+#Q>LMH=JE+52cq& zLZSjt2`|AH$_iYLkF46+-ayQLH^juauf?{E#Z98E!Sx!9T;~x_Zu(G+O&P98T+$ST zH#|B65(@IceeK1Vtq6WR!r@)l+T{M?9*_55S&5n!Af?j~GPAOvDwWw!Q00Y#M}n7b zKn}nivIl{IOeMN>8T<6shKX^%XJX>W(WBOP?jXMKe;OYeJal5Dfz+>GKYsi;w{on{ zY*XEo(t<~VH^Gnn`07kz$DFIGD%=XliI6c8?7j-7BeLX*=$Gam>yYSQ>2(4TD&T z8fZQb9i#&1sqY^S|KCsZ_&fCf;HP{L_KxikeIV|5>-cv`5kG8)=(4xD literal 0 HcmV?d00001