From bb24aca8157917c528a3262843803ad7aeb783b7 Mon Sep 17 00:00:00 2001 From: Marco Realacci Date: Wed, 30 Apr 2025 18:33:22 +0200 Subject: [PATCH] vault backup: 2025-04-30 18:33:22 --- .obsidian/workspace.json | 2 +- .../notes/13 - Weak Bisimilarity.md | 3 +++ Pasted image 20250430183304.png | Bin 0 -> 22239 bytes 3 files changed, 4 insertions(+), 1 deletion(-) create mode 100644 Pasted image 20250430183304.png diff --git a/.obsidian/workspace.json b/.obsidian/workspace.json index d8d6c46..4588df4 100644 --- a/.obsidian/workspace.json +++ b/.obsidian/workspace.json @@ -193,6 +193,7 @@ }, "active": "ec8d1a91f1f0cc7e", "lastOpenFiles": [ + "Pasted image 20250430183304.png", "Pasted image 20250430175412.png", "Pasted image 20250430171336.png", "Concurrent Systems/slides/class 13.pdf", @@ -209,7 +210,6 @@ "Concurrent Systems/notes/images/Pasted image 20250429091029.png", "Concurrent Systems/notes/images/Pasted image 20250429085319.png", "Concurrent Systems/notes/images/Pasted image 20250429084950.png", - "Concurrent Systems/notes/images/Pasted image 20250429084921.png", "Concurrent Systems/slides/class 12.pdf", "Concurrent Systems/notes/11 - LTSs and Bisimulation.md", "HCIW/slides/HCI in the car.pdf", diff --git a/Concurrent Systems/notes/13 - Weak Bisimilarity.md b/Concurrent Systems/notes/13 - Weak Bisimilarity.md index 4b83116..f3e2394 100644 --- a/Concurrent Systems/notes/13 - Weak Bisimilarity.md +++ b/Concurrent Systems/notes/13 - Weak Bisimilarity.md @@ -152,3 +152,6 @@ $$A_{i}=a_{i}.B_{i} \quad B_{i}=\bar{c}_{(i \space mod \space n)+1}.C_{i} \quad Is the implementation correct? Or, in other words, $S ≈ S_{1,∅}$? No (ci sono rimasto male anche io). +Ma il fatto è che questo porta a questo LTS: +![](../../Pasted%20image%2020250430183304.png) + diff --git a/Pasted image 20250430183304.png b/Pasted image 20250430183304.png new file mode 100644 index 0000000000000000000000000000000000000000..d45784f5e775be5a6961092413ebbbada0bf86f5 GIT binary patch literal 22239 zcmYhjWmKD8&@PMw2rUxa-QBggJH_3KySqEZp*Y3e9g4e4a4inSiWi4+(&v4@@0_)g z+*$dtW#pQ@XRgWD&q~tBAMigwK|vwQ%1Ed}K|v=$zBdD5AfM|R5p0kLqLYk{D-;yU z(7!iyDgz1u6cj0xtc0k#*Z1>o#0*MlcTz%c68Ag72mb^q{OMS!Q7b?P73W?uU=L*6 z3_pk;BcCDJiUa%0=(j;1BX=b7*4r{E^d5*?Oy&z^Vpte1k(Gs;?L|}BW#z;tj=gt7 z2~AB+_Xjt3PYq9Z<(|wseg+2io5RT{oXc)61ZkisB4wfo3bwxA1cNw5Y>W{-i0euy4K&#v70B31Qw$lg#y5`Lr;Nwv zVH%kJDiz{%+bp3ND#cr~=gRnRynO3mXXYM8XBFIAV;?4iqwSsBo;QUG$j zIBk?AVqWRF(=PY0VLq9TuheD{p z$(_dP2Z}|c<^?(hAri#7Jvy@j_;U9_B_>|7vFSMlBD6%uGzg)I^HVecSZLS~M6fFi zQHaP8h<2&W@9(lA58zkq*E59DbM5$jj99c?xk1{44L5zKsC{okHB18yGyag7-*c)F zP#D5}rS==OXU{@Yv%( zfXg#;v*kp))^>dBRCX$+O^6gTu!fiT@yLK;kq~xdyek3Pn}S3+#4$1@OgKdicS%k2 zBm@U+`gM*?Jj;Vyx4n8Y6>`!kvXHO)2-rly@t3I;(xYUbqELmUL_qieL-eqeN*h)f zs$3LaYT+pdPZ|j-1@2yuSbzxQ3Wwe3_0PV@CjzBibm+B~SO;^M4_#v)qZ!LMHBu#w z4b|;o7;!B_x3a;)lXq{0hgoTdUc_U&0Xqn8v)?tp9AxBb!>C}YW@RmNN}_{{;ZQYM zX!=Uc2}%#213;k*z3EZ*(02e)bV)_Eg^to(9RQ$Su-9shJI679=21kt)hX972uBjl zN?J=jEkHU{|GUt7J@?W(_i`X*5P;f-HpCKp2jUK*Nf((>rIKAqiLH(460yHk?2u9n zP%#I`BeL1iIBM78h=BleS={)CRVcX7k}8m#OxYZCxGajZzaYzopy*`)v_MJf)ZY_gm^t4-i^aK4Gy^=x9KLx6o7pi4J0$t0+{+>8@zdH7Bn`fxQl^uh(`c_ES!H#fJ;` zpKAAgYd>o84-j)T6R2O8qR|kXftDpnUTO(wqtD@nUz$%wZ{fg?j7GP{{>%gHgC#u!L{r zvdW|wGKia!^2-0WX#xU9#=fuQq{C!s(N`XZeq^UD&Y03eAJ#yBa9Nt=z^}^;IrQ>4 zJGZ$wZjd(NN;+lU%yw+8rJDx2$c+`?W`7wOQA~0YZwyCZ+w(Zlq>)rDmL^K#L_FDC zCxVJ4Tj`K9uGXW;+K~}63wiWx@>DAb(%y5TR6MBHAB0T7~|ASGKxU1vWTV=2NrIQ_~1!%F2ecCF|Ol2Bi1_}+&~ z?&^qjREZUrtdnJM>`ROSQ;4olyVK`5St|eOx#fP1(v2W47P>z)B9ljf)rb#;DEKZ` z>_MMp{T}F)C|^dtW{-Uw0VLbFdyf22&!$MGzaS^Jz{{TiZ`cm~0cM*WmT|luPBtW7 zUn#hzWtHk@%4x*a&{H9oHtS9>QKu-%AKtz+^H4)Y;NDZKIz8t8NganGYsXEg z;AdLiTH6io{)~>c#WfC~soh5F<%=B+zO+qNeJo+Yb#UfJ%H) zR`2GL1wxXo?jA>*2}Bt}@FmHVUajK>HkUNi;&p+x)=oL>0KtW%z9ln_S^`v`Nk-nE zA(6-5mcn`zLJ*zPPx(Y90S6);a>>;yH#aFoNyFu>6=qHG6vSmq64@dR z!U{jchX;R{vOf6jvhvi7=HxN$c3{bdCEXS3Pzl5R5aE`E+XMV z58Vzu5)%J z)L{@2*S}_^r~z*BuB!m%cro`pDCw)9yupd4L*D@$!S5IGwA~+6-`480m6G*a_Bh(5 z#W}f+^P%ut>_71WF^U8b8Xj`a8*e&l z&`5w#9~1o5euHoi{zkH*M$)Vkbk}*SK0;_L_8jpc;!L}h2oNxoP9QHUW;goF%OT$w z7*Z|=b2n5CCNlE79+oEdHhUDZU{3da+1O_8%T@6Y`l9ekdJM)IC_T@8^2sVbo;Hn;H)DwG_PL&piVDCqRgYU)6XmFddXiO53Io^kUF zLKp})7$%Pew`L7#!I^rNX5_K9^Wu3fA>hwfWxu^#-wQUReOsd!UFvTYM0w)^S^M4* z=4>Q=U#IgCi*|Xj!9^j~w2ibeyX6^9d0giN=n{4-3_&CacJ!ll-?OGswjT_@47#P2 zGFglX*xBq`Gjv=zqr|?kN8Y2*j-mD&t>#T@_@C;oFJgak?>KfcKbl;-UAlib#`Z3S z7ZrIDvRrjh(mK0)ZnfX=*z!I?6N86`ul=zXT^IOvR;5*E0WDRCi&E($n6>``ccl+M zsv$8^QrUUn?oLXVo_>RU9uY2Rr3CJ-S56JkU!wHWNxDtaiN zGW_JVO%R>+!FQp4{e6q}EzCI-VICJhz0Ydeo_p%fp38*pDvbW#q_>zF?r(})dQP?q zf<5$sYfOl|$R&DSo-o{A5}+T*&pjr(0V3wrK5op>g|%lD>JzOd2<_e7IsQwWamYhH zg7{?RRwBk2UN8d|E`ulBT_v`k0zd~b@ErQe`O1rcI_~#*dt#;!UO`V>X7Cxh4FN7XY zl&x?1R(w52rV7#uGTHpv{1hR#DfNGvZt(a#c*Z7R(ri)p?gpn+-F>B47g!JZb>WMQ zXdbLgpxRHKsJ%Kmp%vX!Fb4i0s&vy%IrH`f1z*mc=OfobqrJEXhxV^$Yi^%j?`3T)tB&$2<;B(krDdgYc>opEzP?~{x7_+H03Xw;)Efu-F zs40F3T~+HMdr%?9BX=Yc3MhV*bQMdb>dNvlb@;~0CZWQ~D6e(a>iFET((N#v#RV36 z`JF@|4Y4l?mDq(6VknksD{T;>bf(bx_chDa%ez%|W4iUi_%C%|;}rS*`&Sk*hC{4v zD#@3*$|L8PvfPtcjnZe>;Je}ByUyYsmKNv6rh=RIq6&?5Td5}p9>*LN8!VLXkC|=FoVbaDQTsMGUGY4t4bn`JH1{OYcfO4#^uF%NOQVvY=qo2t z#x@-FKN8gW0d?7EznT-=n*nsgW*O?bTtqJh!u1hGY~7=QQ=RJ&(b)Eu6m%zty`=SyE54mAIW|`rN~sEZbV$xXovc% zRKsd6ern|}rNAKoCJg%$+8WKcPb{Eb1h0cNmD~>?p5~m!G4wJSj6lv*_>~a&T4cXb zYAy8kXCYjyzp*-!*eA+Jf02;ikDQhyfyL2gMG{hfbZLI`|s)UZCjLgy8X3>i$djlExi%nvWN}h?j9|25|hSE)r3I;Ad-VpG{hM0IEXaoWKg{l&;=8zSE#P7MuULYp!+LIm#^2kiUtmV?CL@waej zF?zJ2T@z8Vd_1_|OP}acO)}OlD)8-G{6Q2@oYo!W#amA(o#sYg8NWZro;ejy^oiK# zm`qYdLPfvTZVf|OpuuK|UMJ1Ou-b@(Zsl7cf!5soE$ruHtNR}MQ|Ob7J9y^|YL7U1 z?`tJH0&bGRyu#aj^?7JTmVEEVW4$642S6Cx^bgz4ToTY%2V><`c%uS>v=JfG`JraA zT-z?@OMo*Bxp2qXOy27sOOm(M(HX%9eHC=%L0<2h1JsMxzk{gfuVeNkn_b=<^x-Ir zKwJwaV}1|nlIS~-1)M0WVpCb!(c|?#EG+EH!zGU*M~)H)>@;NyLE2g92OUu;fsY{K zUR6IT)s>VXrPkXU4?|IvsL~E3tm}gn@p)!Y4{gbB~qq_*h z%m&S|cbLjJ01&&b7HfrHd*5Fiv$=D8x1NrwPEyKg*IHZMEpy&*Ai93OJL^==*&`KS z<~4J_N5s?eOZe4Y5$fRea^7~i+OR+K>C(>L{_XWhSlDug@Rw7H++6+Y>ZjbOY7|3! z=*c~t^FntIx0#dE*C%iwci`4fhPv)&CZ4UU*9*bGw@mN>0z3tVS~bFq^QIqh;joTR zqSsM!;dj>=K9=4;1GO}PfhQ&DhTco5IQAR&dokec>usU8NuyWtt3LadQ*?S8Z)o^Q zF(P+y#f6@$a26yaB)=V4l37m3k-~m%o!6NtQV};1(@M3K)|aFo_44P__WQ3oNzost z6IEMIo9<`JHE$#kEh%605Hwb(Z-wvkf^XsBp9^W*Osx9!u>ret+kfx3-_JWo6NpXc zl;)i3?8c??FX0o%ID~j@vT%SUsuhQm=`6aG%8yXcsnkSFYqdcrzK{deLfiJ%=BED>R=Sb=EYN+HRaMu1@l13Ckx}4#Rd2_Ov~W~$J3SNn zFW3>3YLY=Z0hP_fH<@8c<9WuOZaG6DwXi|atH=F>JpQF_mqQoBoy=;P^y&PjsxxKb zM@v+JE8}K=Zsw=N5}y_#CweVUt04U%y3|B!kE?5($eBjO~wq5UK&W%GI-j7eGq<`YDzcqhSOu4$dM-SoAUL~ zNc_3JzRqQN(PvCT1C-b?Q}kc)-CCHNdrGbIqbfPm(sy?kxFk}OqJtLI=AABz+sBhn z`Of3G)z)*zG}*|{&rfb*a>I{O?1m6a7fLFF8J3L7hDons zFO=l9DewKarJYfy9198$ntW)@2jpk5N3ov#Dtfa1w};Ia9FmtX`M#U6Tsz)@sh}O7 zTxNO3lKvq#La8=n0`AxI?Y~T95(WFaZVt)&i^zzgLLn2j0Ms?U-bzU3#OQ|I}f`%-2L}LU5^f z$!+qU)N|;dYvhgpn2&@k>cD$QUDm0RkEdD?1`QT3mCHQ}CH--jrpKw6t#E|NHxn5` z)odgCL>c^3vvBOx!-VZLdE6=ow*F6X1!nP?Npdi0RJuXH)9?oK z>o4K=h1otR-)tng z?`AR0USq;VCAeyb5T)fECsj0%m?4RekR=`pS)h5 zB%|X|+olF1s$zN%PaGywzU_|FysvD(gH0n7yy6*LSQXd0bUQulmqzsCzL0gogBZ}7 zr=meL){XjX=v z852ZchFz3$_*)#ed)jY*g(?#1gPqE8u3k%TXD}$8hdPIr5=|y3ZuHBnFd=*2a#>LH z_wV+7_+6kPO*R*4I$RoxnuihCjA-lE(kijbRwb#z4>s9;-{$~N8L1pO6`WMnG-9J3!@w?OCJE(waR2#xR1ni)pcRlXi_C6o7 zkobzt3-6%vyB|5nQ&*V@9X3Bj|RdRuPi4?(Yj2 zf-emO39&TYQx9)`Wbdm*32z4%BzJCk-#Hu|3XH>gv;=CVF=&Wx6^s9TR909mb6XA3 zd6O&5tJFmi79m`0&EN>!iWIs*)6fXKot-h2PIx=6{dDH6e|dyWughO_wXwkG)R-PqQWiIQH!048SdKgEJ>l`isymKKzrt8c@pGB_F8uRalQGm_LW!~c-qj$xl z?|fI5gF0>-GHLISb(BeAMmEnG>7WQRt*?$%rKdiLw;dVZ}( z2E3hZzyG}s{@YWQ>vvN@^L}+TlSA_MNW=0oz?l4WoCT4Q|xm8@l^N!h@XkAcb};d;CEI+unP>)_%r>> zrLOm8BBs@m2WdaEEcf|IP}u(>v&?9<^X0Pl&v5V4&m*3^Hus-tUL7|#UG)KP&s?^e zkzVY4y!SG5KDdS|w-g%ieMk#O@>!zQ3yr_u<|kQL^jd#I?wH#@oQrDD&d=?|(*%Eq z4|W{95LXGu0Ep*B`IMNmlPKpJXD^O&DR4t^n9U4`Vf9zIkU07>=q26cgE4abJyvFN zdV5an9n-Py+Bd;9+6}K&MsKH{;-1crhcSstv_^L0Zz1a zicuZyLStSqoNjO+V517)+#BGYs)=E zZ@ovB!f(G;dV4NgwEh8g9089rC!6H?jmeKs(}NK)NGkGoltYvzlfS07U$!3Tx8fw@ zq)HIw!$~dQd){i#+)0ER%*ItmZ;7AI9gn7R9+tDWMi9Fw<#Td!3T%Cs{?rx1k3Qu- zOvtkk@%aJKTwago;%9363;MMT{Z1}O{yM!y#5ww|bbfdWF~P4p-|n^8)a_uBG&qp| zMHGBwX5HvpbQkVMf7cH7XI2uiWHoB+gnkp)-f;Q5{IL0K)bnt;{j#pr<8u3HE7N}b z?g5pM-^&S-_WFRCE{=}r6Q;|uJ3mkxhmmN1+Jj%_syoVD-^k;c1OjC{K(k`dqdh_Gb*4^{k6tb-%&ZCc#Nm#{58$HG zJzX(y*0I&|rA~DwDyyrz?6BP?9haj#4ozaPFs&(4o~6`72^>k52AXrYO~C`Y--s^t zTm6PPlm+jOixL?1yKqgrT<$8(C(|&TpoRpy{Uc24gpcg#w}wh(7QN}FZXX*=3&#)u zc>>N~)}m9Rb}lY1uo$#T7AgiKQ6IkZyZ0}DRQk?qICa$KxLs?FZ>l{dBC}to-FW%+ z#d0ZUfYv9wpmh*Y;gwmKH}SY}lKJv9>-Lx;LEw4_19Du`;$q64Hth2M!~zr=i7*l2 zb^5LrS4=PubF)=27};vKNk4uQ916M8@db_ov4_-@~Z^* zw*r?w&>CXoZ=8JbG#*E%-m@KCzJUOj76Ffg-y|}RI-lngbk9AqYhi> zdQcC%5+*fBOZX0|wsPv0ftC)fhKPu#cb}+>w0@N#UL41;D{i?rL_sUwoP^g)My29$ zP&2i@?6lT9WPRh4N7uEYW5Ai7jyD7T6IoDGEF&9EOn-3yOQ3h&kuL%&q2FX24@}ER zl?m^XmZl>J2$PceMalKhnhuC#=y&~uV`zmL6DID4qhQ?1Bn)I;4{%;H9*R}`DN~V! zrrYjwSGiPW4e#jGzUNhId-2n=_fi=^jEe_G9QOM=Cr!+yXxbkFm*aX=s#-B$iMUl0 zC$FH7u(R_7hqC1^;FpT{9h%J2ezo3VP$$A<{=hklk-;u~HV z9%L0>bFKFIlp(!@2NcQXcp0ClLt#S~T|wa}`e-&V3MRp2;jyRLdYR(i#l(}=qVPt0 z$i$*6qhSIcPy?OjT4OqXO()oM_H`UQ^^isrfY&l6TOJup)XzJ}%)!x^(T6QDDGT$e zL0P9zobah(c;8Q=&_T&^4gtF!#9}9QztSGMwJ?Y4qtsf6YJT$VCKk^FC47{khS$6o zCB~ff^`tit-p?X4`(f}ur<}YT;IWh+>XfDrB-76SQEHIjNx_Z{FR}Wvry5SiE$~?D z?P~fKb~@^Gn6+$ZE)lw_4WHC88p{z~+G8?`Lim`N+uWQ3b0Gd5Q*q!}Y2UAzF2BC- zwjNey+kMypN^GYxhSy+a4X?G-B}z@h{R|EVbPD8Kuf%pArZA)%R*ETs#x2E?0E&G} zV}_>iKRgcK9Uc5ajEX^6=b*itr?IXZB9#odSYH&Z{$q>$7n9M7JAJz6ap2?j^N27i zGSYk-;d4+_*VP#UN!QN6$GWcP)5^YlU44#YyN~jbOJ1_)IV`foFQ5Z?Ji9;s^vjRA&kPHwWv(8>eAl*iiE4sWj*fP(Q4{X8q)vl@1S=*iE}J`8MW|T(H@RGp+z8GK7rVod zCR_$mS2>+ac++nH@g*l(xc9;Z0U^7>tgr2*3MlO8@8hVtTpo|(#ck)qUr54$X)?`R zN4adJ+OXSt;g_3yTBXFknl&6qT$PBa-A>May&oOcYaDL!gaDV*di>k9)L?@U>qv^F zBDQhRwZKrTwT+goLn(;WQQJRMywqHgR0NASQ-sT-M_t_-9m)?RWlX=6JN;{ZU4fL; zPmG&0H}ShA_Au+pu~NXhtW(Ua|Q7KCQm?58%qAi)EfVV&haJ^MXj;*yO8O zFWdAB?mn{R;0W@lvmP^V;C|XP)iz=x5?`=ogZus_HX509O8&&oz2IG^?!F_UZDJ`a zj2xrw<|BXECqYIGY}ejw%7LH{;4-eb6Sb-MWk0u=773YD3E5<-tRxG8oJdjTFmVB4 zG3IVWvMDK2ER2lL+;h^|>>nlz%Vi4BVy5T?p~-{FhcS1@$rONNkIA$)jfABL8KBLP zT1Q&ME^_%=7GI^HuSV<6wc{32F+D+s3}0Q$MB{v-eDRj&X~HnZ8p$WoQ!I$uP8>RP zqXp_JD&-g2B@shxe}C^LU!5nBht$y#Ua{wQQL`N;lJAs?&_wLgSr z!SzYx^HR$AEYqU4vLm8=MYO~w(OPQD#>f2xy@KZi@DQ#cxg6`hY9--?(TZI|c2C;x zemrP0Tck(p6rdUbbY?Zw(Ksc@Vl*h2)SN4|9h-}7b1wnaXo0?3opDLwV1V1=s9~px zpA<;D(TC@#M@t_GKF?FVj-DI-4 z44c%)?x3hm6^&IZ3n6rzGx};5jgiGtIBo?l5rRj}HFRO@A#U|EQyPSA9?4}a4b#7% zZyaRGL{2-a-zSUBWt01E1Rbhr>=DfLeta*KiKZ-Bcm_D(q6}C<(%342#f;*~5~J?0 zVj+lBr`eRVU0+xs^aMOQY)nD5AfKZTwP#8 zsFG5I{mP{-(_7L~*;(MHG9LG~k2WL`j8EuW=<2yXqo`46bvs(4fc*KMeBkEJr3z}B-k`|DfD4|{=uHm<8 zztFu*Tp<x8wG^vW(pFSX+&1T`na%>Y)1ddaR?^{b% z6v>^x1|4Dka2OMRw%)o)Y7*S7+u=yoW~Rz?f~g_8HkIf7xnu$b&mypA=c&hjEv}w6 zk|QiKheR?(m%T!PpX(OsvM2}#&x|3$$bdcp*jOr)oUw2hTl#ss7>(7A*l}MMMXb#_ z#7*OlFTjcx^|TdM((&xkYOd25iJ_)qEoEk}N{4u39WB?RBQ;XuRe&7N-~o*u6ImiC z=sM)iT{IN!^8#t;2TCEulPMQ{cG1R^V0T>f1u+v@kZxmU5GE-s)o6S3kemNpkiQKY zcO{mN!=zcU>K28jM_4$mQicPP&C*Ip7m80&0DNbku8|e*$q#Kzw?vf{ zDy?z=DKOX23haZwoweiT>wg6lRMRu~)e0LONcOuLfT4wx6YCTKtD2;rL5-wQFpEBk zCI1MDSm;>c5lxw9e8gDgrVe^?S^(#KZA^)Acl+}5nPf90d49u>yV`Vci5J%E4zpHf zIvNN1_^}m-9fC>U`M)8KJAbE^chz$Zm29HD`kdb9Tu*|%oz0p8D}21g{9A3XRXG~| zn>1CmvKGCwKC93sE6nKaZG^Q5y4d#h&mc|WysJ;)DafE4SVnoZ6zqDF>8POq41|?Y z??G0(QD=j(s`ID%3XHU9Je>MrWYPJL`S~&i4XV$NYV*=_nF;6h;+Cf{hUOo%ZlI!R<1jdlvO}Sk@c(beaK~H%97ei z$^?(`H-5}R){%Ww!|*!dk<#;DiVL?p1qLg~`2(&xhEeLNADAj`?io!&8AX?|CDT;- zGY};^QBxV5n6TRPq`Q9@-Z9Sn5iUqfV0XeN?V=36*_GvAgx zuqGk3PK&f9fu$$l4lfcvu6jgA9EucbrlZ#noO{R44DPXghe}%I#8pdP=*UvlU^Dz2 zX}ESp#@51w2Dbs*GX0;L_qBJZB`sTs7v;A*Q^CyF(UUi za)e{&u&=pP$M7)ockDH1(S-1boS4)F1o7lH@PKwh+9Cv8n{&Wb7gVB1BsO&dx>!td zeh3`dR49Mw!KoB2Ol%M?G&B(yp;aWpSuk*RVe~RJ8{qjlk`b1r{GR%hqNzB#EAOuz}Rf!%vG^52C)wq_5k|lUyg3e^y zTdYvN@R^ss5WSTVM=sMREW7wHgW{Xhm`9GdG)njkFBX6#G-%-yWoaW7eNvT;R637~ z90C^F#+ zXuH=y4g+cbICw3#>HEA~h8w&caXET?!2k<{SuzroXTS&oA&>eP3BQXM4AurdbXisB zLiM3`7EByq_m}k=rPY)}7)AN@x>SC@M2!TG0x0(o*d%J?K05{EF_MobT2ks8nPZwm z#^9wej<)5QV&4J%upX{jRc4{=FbTQB3wGjMv-mJDy@Vdl+HF;zo^c$3IM776`#772 z2ISF`uT6QYytgHgZi9@y6C1<}mNWhWVvnT``Zt#l1t?zgBs0Y6TZ;tRqL)3ztT784 zWUeqvzJYS|ERtOd+wp!;+(-5OmbfB4a!V>8WKd}%OUQi7=&2`KXDx9ep$#<>Gjjiy zT_k4}5SCp-g)`4ueBf4;w7P@A%VErWE0?bcwOy_HHS7OQYFtYCQ=JLAu(!ov1IW2L z@a=zAZNj}r!B_Q!=Fpm^uMN+BptB(V-?|k-=Bwq6yFeOX2Y4B`LBKAxWKldY(r7$Z z^v9YmdD>zNWwR0vK2q@iFF+Eau0Qkg5F$rgUcmFov0oF}Pdg?)P0}#U7KpG%=4zDO zJt2KT?PR*OXkv|w+ulbx(h0pvp>vhQ|fVp1Hgw%Yr7n*Z(a~DAM&TjH{SBL|afPsQKSiwuE_}@JAR1D_7#Y=K_TM*17Ver2zWUe8yiE) zje2bkai1=@G0_S9LarF4Gmzafl>UHBr<{LIq%vq|9P&E6J>Q+5p9?>YE8A^2poeAG zn`42*?k_ewzYIs~IkZcvq$mg6e1i-X;|cK`s(&W^TiWZuo-%`D&mwWV&?gL>t7t(I|-A;##?Ot?V)@l>uOSMsY&;)b9h_!^r zdy7TcZ%hS+gYa>2X)!;f8+c@vT0__`eYSPo+|xg}Nu0{NMEilbfd12^sx>W16>KKm zKR1&sI5ES)!O*&Ooehb<|7p-AZ1OfP#e4bh+l%4?rsVaO@8$XFX~#v!nVF7*qhmsL zGx~?3M^RbE0ZejBG_k157khhqV1e&NyXF2!TsDuR0|*}pnr&SVF}$w%k8zORcr2T{OZ=OG$r7bOKXo&3H!LVA>3`Bvl=EQrn&L3fnq-pJ4*b%y2jgldXHI_ zg^`hwvNCv@XS)l+=#x|t0COOPo{w+?k>S4vYQi*;3>#L;yxq5)QMF#iL3Y-p(rMqF`j@({3@!OW)+BK(6mW%VEQaKM=C z=rnLoCqOPZ61#2A`VauiC{O)g*u9y}Bl`!t@%wvs$Ytpc|7oU_bgE~HG%UN4sxqHE zlbI8DL++p&u&WdAgmq-|A7pBwJK4|}i_ghGP~bb-XRd4Xa-#A!8HL#_hyNyBOK{Sk z$@&k_F->(LQRe>v&E0u@`PZgd0GbrxK4FW||F{v1<%hl~mXCUfu>|x#-kZh#Ln4~O;%B_GzvlhG{Yt_KvW>lXo37^7?TQPgt5;_+QF;5 z@%^AHSnvT-iy#*8V$B|hP={L<;%1OwRg>Mw)7Z`v|99(fAF=(;ZH*wc%}ogPAXel@ zg)Vv6^UF&Dp-_m|1*8OP(B?oSufWd)Esvx-D{;!zYCVutGEEHhllJeE!$uNqCDcn+$1iC~a+R zt*xzv1Ve~UfJ}O=3M+S`#QuLmJ~AhodqcJ{rUMCz0F$Ud3#0y*q}dOjFnN_Qhk1IR zraNjQZQV0=pnD_=dJ)4_+;WLi?Jk@wuJ?u^;3nwtTYKd@-xT_cmHb<4sqBm#X)qq@ zoQ=SI!tJkV-_cLoI{uQsIfB{4FcCTWnr`M|u$clbeYaQU=h0i}n?PY@8PO(pZ2@5i45Sr6sNHhFWCKk#=j}b;y`& zM`fwHPH9seCK92VheZ*q)PQi92p;Q!Pw)wE={awYG7RD8Qw=m$a-t$)@NI?-zPO{vvPDLxwqk&bSVe6mmOc|2`b!sg$TCF#7FA*?@#o z1=B@Od^g8sA1K6vk4#yvh`?HY zD-Q}A*5k!)lDWgar}39ZF{Qh!xksN`V?v=OY9p2kC;f`Cp{D2DO@={`F2%I7QgyEM zW%JKi1ciju9VRdwNH8Hc5q#>5&jH4tJa)u^ob^Rlp4@9AYFWiV50xfu|L6-AeW4%%hQ zxhZr2NH*#5atk+lOE`Kh!14t?1(G~Mj%~2l(N19Mi{0b+g*D+)N?y! zWo2QNt|c==jM%16sU!J#UMlI&SSzHL4+s(G*b0-^exnfD`vNH^kgV0-w^oa@rpsI! z!{V1JF4=)8NW~t^VgK!UEg8N5dW$AtXEpx312()6!S}~+fh>Vd$QcHP18VhmBavhI z=Vqdn)|xTlDizPL&-{BC-1DI~EE&1TFbU(T181phRy3PMHZcZ*%j9QYNt^N=by;3}SE;U#I@L5OheDlmQp%?MA zHZEgUsN`TNt2xi1$ndhd&Z*US377fJy%)93zr&CdME%! zh;^Sg?F`ZigwQgQ+JpH*MjSdm(`jj~Q0vN5|A zmW-Y9^EtW|VAHjA--G{(`)#RCb51F}qArE8*iD2*4Ig7%E#CIkAwz@%maN>;$!e^bae;E@nHQP#sw-FSq;h^~8KxGM0|Cg( z!`lt}RA}CLv1lERb_Fz<1z{PeeA0EH)5ukDR9KYzcYe2!2vy=S{v2_pQ+w38QzcmF z!UhM#i0vboy0sh45yg~>`UoWERAlKBav!$A99V3gp~$)^Xr$6J^#ecn^;+pn36{7G zOUwrCL#!#E4jP_^y4>(3d}qSPcva8yD3iFVTiU0oD5ff{%ej}ZY2Oe5 zFzlsoZ`TM9Q#cx2NTSIaV85}~_wXPA%VL&TFoB@7LFmh$?6mZqh>AWn zpq3FL5*o`~T_cPwj0fr=3ksL3Nrga-;^+C*!To3&cKQ*9pi5xZ4_#i)0P<|?CXZPb zlUA7ee6mYQ&7F*1i0MBd{=&*v&2^$jC7*>UB(j|@svQ5Q-yXMMfm*}7=g`J&uktD? z+<_-zT?yi0hbZ1OI5^R7yY1L(st(m(=Y(}vporkvm}@)F=s1a7nsk3qrTcU&B;-Or z13KqFhsyF`i9QACFRTz|d;Aq=afVO*10LV+v2^%1w8(R@Cs2}SHn;aNI7gjDu2}UJ zSV67RmnWN+Chy!>3@_?WFdKEHc+BFt-QsosKHYjCoE>^6d*w8m8@=;!{>(Y_88&LC zYnzuP&2lv1Z8(j>?&LS}nyr!|$;anaupdf1>MAGrQZt}ZIDPuF#&$+^`)?H>Ek3%; zXiF$x{S{I@8Wp@D? zZdnmh3*C#IzuHRb3q2e>4?SAq=AP?#=L2PbsELpeRqQIvl9Ar|0Yt5bhlc?LU_X1T zughfguAd^AmT@u4)P{(U=1eiQqmxdIDuwsZbhV!D+xUvVwX@sg;u7EV+_baXK215c z^WSY6d3n^K*5=MSTUq4@7FZ&>NXdV|0m101$}&%`w}5V0m-lFXHq%R|vZFpy?sY4f za?io1&=gt319nlIG6gMSc*^^;d48n2s88F!GY{tVf}d{)=%*hXAKC?tl3UpOeQER# z>Rz|MIs@X%=-qw$pri6q^0gzw86s`L`fBGhm`mJE7#!Y=8cYW~Ta~k!`RVlj-R1Ke zH5AmRn-HIC9X|?0L=wtUsiE)O{6-nU%9FUUKmLv#j83Q1TuMNxVEb}`Zm58M>ZD6G zS}Gkb>vB`K2+v+5NL@)$b7%S}dj6{2@-s~y?SmsLjb3Ulacc%JP`6a@-yyu6zrr~%d7bwN+04vH z)xv(dE$f3NL*gvUHh>9+te!FmKT9a98HyV6v4nu^?i0rzNS@6oD$Sp6+0bsi+#KG1 zNe4ITH&T;Ml}?rxW}*R-Yt#LVLW(m=C=4!mkB*;^$LDkKy}P<(k%N@9AS*on7sH2B z_E#k5?c1)|1G{Mcn7HI`bE8|6fd9QSxr@t8R+(NJ<5nIKXNd=NY4BdGkkKu*(ebH2 za28CY&Vvg0!WVg0E{LX<3tln|i~+UHbEIHoym71pmSK?X29RjiC}F6bldw>2dWi`BFT zUPhd1Kz^LIZC}i;s2)GJKZ~v(R^>2DdR}zQ(Vn-f%C4#Ok8b7AzRui7oOV5n3Q`@R z0V3`54%WhPT|Q`AI(DRd(Tfn?bHBGseTlOGS(ww@gtM?QjwFOLSXmU#G@J2Bq_hi&^hjjg5|8=0pcpKm5~f+x|ynbtVdC=a#-K zP8WAZ{P>zv5$=OcoPGU`4eB7W@gfbnDjjH2eReZIEu`upv=xv(K?%&F(-5TL;=O%xs&c$B z+s1J|M>C@KZiKF}p-K7gPB(PZyme+Fwjn#FOPHZv^j9T9^$G|?GE+xB#Z3n+uF@A` z)j|(GZ{G^}1)TL09A3dQP8PPYVAWdh`O)s^d|Y6V>`lYrf+lHc82ki4I5&G2`w0ah}ayqYiuoKd8(iD6p`Q2 z;T@_N3Eo;?SGwwo|6Zl!esy^Ae_H%C}kYz3h zGP29jdsoZXUg|)OyY?l3*enirs~h&Ob?ps5_b`Io3p;K*6Q$h&u%y)f3R_#SN?+&Y zAE2V zeEyFSN;F@gE@L3qS@)nN%yTd2LtY$jeOZaVT(-Yl-V>|ln7%~up^igIZH#-lxo3l}NW#yQ6@p}YlRcUp^N5xd8c0}&i1aCm&YJzH;+o<_2? z`SvZ7*rS3l^8yYz6mZ9XLcu!}wvxoB>u(cRx_N~CwTXfEiUV+D&UOHkKcpL($RCz)d0pGoJsR_q_Q zh?NDb8gX7k6Tg~5e(y;_MvbjVTmfrXI%NSPR>QK<*$^m^q`*?Qk!y}@N`?NsQyyCb z71f<=|1~t#iIrmn@O8GKNwHp&81Wp?>#V3}C&)A>V$;nL_Ug~I&tLVu!%*-dpB?2aMnFN_o+R6MHSpI&>E4qQ0 zyW1)BwJFqE^o>%y5m3*z9bi+_tI6qS!7xOY{J)l)@w+q~Xc(6xc@^dd^z#OVHC`j32^X%SS;>1gZ;NWT|ILm5~g!cKls*ET1H#nI>+naR_tyCAOmEUKWa^q>JB(CB>o6Pz)Or)LT`Kda_qovvRPSaJ*4 zWMhsbA{*NTN(WPPCIr zIE~rFz#R|m7F=xLf$l^=bzKdS`q$m1UHDG{caJnL265+YvR0CSN$e-D!f;QE{yM0> zslI4cXR7BEFtf+ufE=s z>+Vqi%P6Vl8T6sy{Fg0QX_C%_ z>|YHQtkUkMTpv@JAQFjy^^nmH_+_KUlAGb^&RyjPWsO^6UY2D@2oTn0Di=@b$FB|T z^x{d;2`?z44Eh>9`}Tk6fW>%d>G>nHpidjjZRAu?LSsQIgqM^Q6b6F_A>0GGsS&~1 z8hM`1Fa}I%oq*p^LQZzm)P66BB`}e2;3fBhYCD=%@qE-5rv*GQxb+W-@w%20-nJyX-3bB= z{OUg9l8=&y1yb} z2|Sa!BB%VLN{wqcgs=oh!eIn&x1{IHA$npTJt72k(D(v*ssR(q;2%t;9^P`3OGz&4 zJMth$U>%fD-I&^2JUEWpu%1{c7Fsz=C;A9YX6^npAhscbTIXD18n8{O(QH6*s^c`~ z_gf=OHh_)*@buf>7Gf(k16wJA5i0f=dZMaKbZCtZE%sa?E~Oc&82Nr&~U!q&Pb} z4}K9Gy{8$8;7#d=K5Px@jbru{uQHHIJkC)kGrOiLSmLx|82?+VMEkDFo8|Br3Pz;On{>^&frt2Wl_YWm9_CVEVIdTDv=cws_xfHR1qk%F}R8fw8aVXQ!a!t zx~u`IEq`ROVBLwSk<7Ey}oOzmb5d&&DePD zJ**DMWCq-b$U&UF9~OC;k78QC^YnG6t!OnUMc^mCJiElrv&ysLLA4fmDp3Xoo19ns zIx};=R#C%39ceBq`*b)L<+t+N+S-4O$}%IBhbs3E!IZSVgLj|0uZ;g$OKQ5VD~>w| zw@o%rJ=su5q$Amb$%H{WI2$`+81!Y0^;}pvHtTOTTLxO}++D&}-^)&>0SC5`7}&D? z1(WHifBJxM?%gLVy7yZ=!czC}doe+0qNW#k$4U5=q0iE5dhD8rEp`U$jha7nu5?@#C*u zTv8vj&wR^vdxe#qBt9&(qya9dQ+I>YS^2`>@PkYM(wQYWM ziAEw(#?f~lp{e+dIkcjxGYJqgW4>M92wy&8oZwSF>`AvwwfWgYZF%QO_N+WJaw2vj ze0%~XzW#MV6ByIoodwcFr&5ex#r+dr$D25y}>rGPZkaAxl!K6oya2~zx|9~^j0H@E`!d{tG|2D