From bbd5959ab8e208bcfda055860411baef06ac9810 Mon Sep 17 00:00:00 2001 From: Janis Hutz Date: Sat, 1 Nov 2025 16:29:11 +0100 Subject: [PATCH] [TI] Compact: Add theorem 5.3 --- .../ti-compact/parts/04_computability.tex | 3 +++ semester3/ti-compact/ti-compact.pdf | Bin 297284 -> 297506 bytes 2 files changed, 3 insertions(+) diff --git a/semester3/ti-compact/parts/04_computability.tex b/semester3/ti-compact/parts/04_computability.tex index 3cc788b..fea1343 100644 --- a/semester3/ti-compact/parts/04_computability.tex +++ b/semester3/ti-compact/parts/04_computability.tex @@ -41,3 +41,6 @@ Since $M$ is a Turing Machine in the canonical ordering of all Turing Machines, This however leads to a contradiction, as $w_i \in L_\text{diag} \Longleftrightarrow d_{ii} = 0 \Longleftrightarrow w_i \notin L(M_i)$. In other words, $w_i$ is in $L_\text{diag}$ if and only if $w_i$ is not in $L(M_i)$, which contradicts our statement above. + +\setLabelNumber{theorem}{3} +\inlinetheorem $L_\text{diag} \notin \mathcal{L}_{RE}$ diff --git a/semester3/ti-compact/ti-compact.pdf b/semester3/ti-compact/ti-compact.pdf index f119fd19749177975e1a1208bbd962ab47e11031..d0fea01ef74b37f3960f29a2df8f52da6825d66d 100644 GIT binary patch delta 11112 zcmaiZRajly(k!qR5F`-X-QC^Y-66QUyR6{uvT%3TAVGp#aCdjtAOUXnIcNW`_pQ3W zuIe81Wsa^fkc3*8f?7Z64&dbCOrCM41?eQOaiRt+)ori2*f3yYiA?{fSXJO0=4Gqp zUR+y7ZXU=eC^8jQb} zLXWC4a|VwDQCB8)CKQh}nKj5d%ngdQ*jCmWq@7i@e<6J{Y4u+B)Cl%u^>3=K0$nsV z#vghhTBeL&+DvK`XumYBFV^_qPISK>oNnwMoR1Hl590tht@^^uaf~~p)3R1B_%f@v zSH?q7RgU+IGTH+(qLeANeR4W8x^ib4s8uQDQAsd}#*=808v4eP^e1rkGSCYA4C~G= zW$W+JZq4ABRn0O;gp+x&#Mw?ZK@{slLX;P1)XX4dj^8vi2Hj1SCcj|7q)<7$`pEPR}C;O=_aU zY1D@LhPe4|R+R5hs^;l@&4au$QX?p5V;o|uN}iUZ@5 z?ZffrXEv1;=k`*#63xmo>NfJld*1(44?^XnSmI zfJ|0l1@0K72q@x`i4T}uAy8+}>r$f`(4ut|G2N0UT^1EdSq3n98ctjwJuL_0WsAL6 zJPj?!t)eRvI2vx5iG1}NFm9H{M#`!mV*yFwG#4btlbIpc2VdZ``qpJgB-75)^UDYO zwi+>npsxSc0R(Y;Z`VPRKNr0#;nowr_pXtDoAB#0X~ni^3*g@u!Ikn23ynGH*NilG zV8_Sa*}+hzHK~G^$({U{G2#h285tx4Sn|)ep~{5#BMP^!G06T6w#1d6YteNf(gqdc zy0|m4B`-aMQPcbdBDlF&Cw)l_sV=uT;YxY(a^kZWnL$M2%-gno$nEh(k<2GV7Em9m z>4C&|7$-tS8Gt;$rpeKokq63VWCt&}IIu zF?1bwT(R?lfvqG@r7+?ch|087X5(E)WjL-x2$C|>g`8aq#{J^{d%4(`n!xOlx@R3% z%2`%f>M1|BJUIiGr_$r}+w*a`cSn!O3CtX&4Ro!27jq>GK5OOJtL=6SV3M-^rzP67KTuA>b7WKZh75yDz|J(w$G4YSSbW|`Z)~p zB^STUYaGlMUUTONWF=<1+VrtuoK%8|j!0$-4n=tHsQTgvRG(i-tq&9wwmi0bd7$x$y$+X!Qz_Gro|Pc&K8KlCJ8il2plsul zan+;uJ?e{`^j8VJYf`DPG*W56*U|^~?{K3?BOC{n2AQVZS{mRv16P6-!gMIRBC+Y7 z%JJ6-CWvSVm|;B5);L!J78tdVvo9!q$P(%==7?}V-wSS8jIpqnFe(`+znn*3qkdF5mFWOG%RJ_1vMEV?L>T_p))O(6+0!h`ZAaT0^UUZ13ujz>zpd7Z-`IeESB zMM!{c*M!axGuG(-o5K%g*oF!)jv)FUtklS%vz8UK5p}6G1pMjj!VC6l^c)qx3x8$V zl43_UphPelrQtTA%mKZ)33m&Wy~?RRq6T|RZl*A!S)K-|^WFTvM6>8ak`|J#TgF%& zv3=rK7QI>a?tEr=iPBJp-d;2Q)F!EXP0xt9H>1!5@gfSXd^-P~MwFcg`U|LzDvNIh zyE`&3ZI;yi0WZSh4e_8wNLg{DJNw(KGY^Ue#AL=-SmOxglPp}mPH-2ajz#Z>cV`CV z94^bF3t-&k$6CiE+xlg_#m}V+I7sLPEQ#g&>)4!G(^(^xwjRh|5od=M8;g)D9!r3w z(p%|PhaZo~@Fwpcu+FDrIGB zf4ZV*l19TC$_XM;h+t$x)Ks|~_(uQ8zdJ$*>(<5AO$49c$zz2akZMjsQ>rMd0x>8- ztW+T!kzO7p__Jcp075=8C zfnCqdoAE_YD5#&JV2#^gtVkwev=+e>hw4ibfkibKUv7gQjoglj(@h94%J`)Y8OlMOWD)qXVrXx~)P64!+R|w~fArf0!ql8-P`%Qj5@Fejg7phJ z3!syPN)bhg(};X|f%bgek%sD($)^rZ45`ki8{!dU;-OCTj`VT~J>V3;) zfMovuxaQXM89Q=GMQQY5f0jTNgVa^=SSjOCCZ> z6aSZt)>;Sy1+DjAGJ0#LF_bzD6z6|>W3*C5L!IIMt3Xu-HZZsrUNt*L2>;@0KK(d4j}P=Bfwh$jD-Ic0F?uXsQ;b6X&S(R^6&ibJAhdvDDM9$ z99{$V;r=@UTI=Qu;12y?g+pXu1_HQ+5IE8*g%5Oq0-uop(OX9efusO10|gMR^_>LB z1OVGn{e{95KsqR}8!ZsCHINE;4+ZvT01mbC(E&xFz@f~4p%~*oFqRFd44z;BdbG;1 z{1c~g{^jPg0Uw~iqdb4B^tk@%^TrQE2NUZ6CBT=QK>OBs-hYy4!a(#g6agRrEGY)$ z`uhd{?iMuQaxoyr-*a_~0r5Fd^9FZ~0wYY42Te9~2Gfc}=_^G;)wT7?%cHPQ#?i;D zUP=qLPu4JW(NgN*FCf$4%K-l2U}SM1HlzobS{$eb;!6*rUQk2KShcPbMod^-OJp{Qw>AVtItlFDs9?U z)hq%IL@*o0b}Y=md2S`;J!5Z^UB1kDkEtW2(-JKTk zn`c9DY8LfP;*Cu5sZizH*2D?LFoPJwK3<%G-!qbr(_9{#gGX&|3`<|i)zmIcuBXG( zL22&OFpCPw^@;PEg~SwX;>*03DurVK>h8pXB;qx_q{1pkn^WVrBdW9PV4dpYe!5V# zR~prz0+6e%RPi5-qA+}BG6{AeH8G9Ln7=~vB)VzL*Gs=^&%&qxJp&h@3=!c?ol-w_ z8&y?Q8a>wg9MsnarIyy;tvT`?7~H5NQdjP3sC4^&6x3H7MSe0hQ9`Mld2o6fp1kS- zZGEcpj}LL8(?<1WN$e6y)LN!E^kN>o-8k{{be!hR@7r|l zOMp15sK{J|1N^StAFr(z^AG-j}2 z0iJ-noLL<_Z+o2xP|IGrAdo)1TqzjMYOxsx+}}}&PHVf4y4D#!XHlZd-&dU z{eUrYwPlehRvJvDLRPKsA<7B-N#C~cVuwO*$iiI`nj6`su2Q6y@+|)Rabtb~*_N#n zC@G%7T`9k*5T?YBy%J#veJe#X8N!)m*v&e@xuv%BpHln7Tp$&usQg=7NlN0`$&a6L zg!SE7g8#8kh$K0zePEs$JaULiC&$f|?uno&9}Q(RWeeidF7f3)b^x3e!H{wFQ*OC_ zYbiKdxUkAkuCwfs5`*uuIw58ORccY(fetwtj;u0V$HP}0=1%Z8kQQ8&c*9VvL47=K zEtmKwmN{f^QoK^DeLS-;!M~X~-TAa%D0w#E(;8cHSJ7Xy>fHpzWf`&;1#D+8jOb?P zE~M*2G%KzWn17Q|F8#@h%Tsi;=FvE#wkBd7@q3^wvuU>)_rB_@n5|R;kuYrbRW#4i zDV8)Tzc*#Wm-N}^RDSktQnL@aaH_UfG;c!E_9pz_iymS8=|(YB&yau1WXw z{3E4*$hqp{>9Z&pn3j7d5Y0GNb=UO4b24WXmsr-MJ)M-YcpaSrk+S380^h4_AiM8_k%|FB6_K-jA#cN`|(7fg)x<3FRj%P^#G# zTres)<+(-I4gDH;rzXlb*7wHbo=VRt=z7#H)t;X&z+q753rkQc)6&Dw50T<369PWn za4W)vLO#pKab@CYfs`GX(}y&mW>$Ay#MTnB+?TDo>}iXw>($kN<7Y^^(#y$)#6I`c z(-&_I+?&>HTYqoFDw!jPv2Jo0xe!Hh)3#xZx=XaPiWArEC4in3rlJr1X~AToK;9E0 zwa5{>YRq9rZi>b2pdpdm!9h;y5M|u8g{qoPC+-8eSz~9)35v!twKKWJ$1-CeG2c`b zHKsvYZm$d?J?I@jf%rIPuX(vTvJ{L++Rwl}3SzlljMLOXI+Jxp_ndriI;9zi&+49C zt$dF2gHjPTWj>jrX=s})aE0_GuC2304o;%+2UP< zR+8!TsA2-@NBdRb+H#LVRZ3*E`5I$4#_690fw}b`0-!nFRl;Bx1qVlMGxj4G?^va4 zpu>rsTek8wR-Bh3ihcZNU`p0R(cN1b+2`$p zCUFF7uAo~EJ~5x==4O`0`t}2H8M{2aKqE~GS`HI6I#HF)DAjN!E{1SsRz<1|+y#yh z3X-*0e6WEW&Mk`3cCJCUoLfb5Ty zD04Zn&4_Vo#!^I6v#jQ7OFR)83_G28Nm<@TlE6E!*oYj!j4Y-CH>l8@i`CAY(1+r! zKzR>!;!Xus8;pp?71wiDfSfadA*j1vbjF@_ZT z6cri{7iWkSY2IUjD*hfl9~_?lw__SWV+>K_L$#@VvVs>_MB(qQjKZ!;3VPxP-09098*c7R-F7%G{NJMX=JSG?g3aYs= zn`=8}0FOh8iFuv&pz?s#!G9KEHOsI1j+{*R{OQzag$;iQeCLf3FB_4VXts;r55*at zkMHqRzw_>*xSSveYAq)eu>9^2Xwgb9~rBE33a_*m>Jk`L2E9iwcs% zaBCf854*6}ApyP?k4k9vc!fmXZ%gcPj&IFD4Lr8^+ega|h4-BHLn~J1b(AqNz=ocv zI)xC+aPDs@KyYsa%r#43kq_kUbb`o!7I8%pZaTTj&Vx6sI;ZfA@}>xJyF%oiis^u> z>U@f=8m&UE8Iaesiy^nM6U%ghBMpR1YMnXHTlKy7sae;GUN1hQ?lD)5GETJZdPh$O z$$OR(cC&;-c9wdQF<9?a9K5dxWCbN_F_n+ZyCjj<#C-Bpxp^qQmgtUDkFNP<>baYc zm+%X_BI3ENg4jyAi{!>N9L`@73FvWWQxxSP5r2V&DXe8MWW9k%88xw1% zs_RbVIJ1HI;ggy95QC?TM4qEhGXk)0>jBWctY1d znNU;epz$c^lwUaA1^q1rlW(Ad>;yW0Yj2@WedVtw()RQmOvBkDB*Dog5=s^Ur4!gC z2V7Xo!#IOdUv&A4c2l^Ji;==&vjdBCbD{|ozqAwMg^Tv__Y{e{#L&*VI*dXjZe57n zG5)^khV@L1Gejl{&<&Gw>8fzm(k1E-vN@kikxVA*WK@blcjp3)8#{tNZ^=2)FUh@o zvlpZ$4%{BOBWPy~SBZC)vsbrIXQIK$2(^~K-~_As1mijt&b6(l9c7UTg7fkdy z&r?NcNCSE<;qnKSdns@r3p1@!pg>x@OKL=--l&C|Eom&s_?>di}$`e_@r8e8W zb{KCVpZ?iSOA(4P*DTN=U}jXKvVO44D`1e}q;#F;%hzset82It@)qU5n89bd>k&sD z4NR}0EAi~R*7|3a+Uc~I+DBYcBQqVm*Z?tK{?*wEgWZuzCwr?v=Imwc(GhWy*cCgO zTSeW?Q6{@W_o=ZS9PRgJXrZ#@sxqqN-UU1U#5^tjGsD?m{m3B4t1jL@2k$$Vd>S(Y z^&mlpYT@%+N814R?k5c~gRwmfvVbQSN1vd)#RR~4%I{Y#*oW;uCSl`gIjCz!ms+8t zQcdqpPA-mag4GD3AoePztuLgR-e4>gK*(O9Q12A=yUHfh?=jeetg8&UBn7ug{RmE}Zw|2tRx!xrg%}GW|cm2uknDMh)*XNc$n(t?Mq~ULnDs{1c zQtBR(3mn?JeQtM7b^wW0mkCvYUvFq9ihm^9rt%*6#8ZHN7z&Ox`b*CGYY--e7=j(K zRJ%LR!DR<0`ML9Ry(z$e@1#f3j#^mc4I-G2qLZYvJ$1uPx*>=s0fwdDS0zh*rQ(r@ zt{UXyiQILn6jyXP97MCN??h_{Swcy9IRN1*0u3jc}C}$}33@@1EnSZbZeiTOanH zQxDyft1&C~*uHm)rPrBr-B)R)_;`Z#QWb5%H{%is>{^Ae=7k+ORwWRmSL^nciY_}^rRY|cW?TF zMjBo5BrHYK@B{L^xRT^F%Jv!8s_ig1x6Utn{O{6qZt!$eY%Vu7H&Ezi+#5wJ9a#3h zM`KSDfmprzTYgdrDg33aJt{$;oCjc&@w7iqj%MKOYvnesa4{l zcIG;gem&^FH6{}IBqSTq`AKt%<|{#}RIqC%&!pvRnasyN*jOEi2KpT?4Y+o!&-G$Z z>=0_5`dJ&cq^62w`ME4F43Pu$J^&`r?~r;={?^ zUbv%S(5t$UNSfyia@^_~U3C^KGZUV(G129Lcg>lnnIbMGGfSZAW9$39_PGw^kycia+oiUb_jW{>H-_VgoB&U0Q;uq)*kYiKu58a;)} z2Ihcf!~029>lIQ$C}CGmMfdhOE{OO`kX}^K{;jE0`o(042Z*M;hx#>n^l6-5bdo5< zKOpI{>^&sdx9ig#k6Z41@D4;)F2f6}NCH?~U&qj3qFcfC)Q>>^#*+&W^~_U}`qzzl zelyd}`$au>RIM2nzIWFv16n4^nf$RQtY#Cg&)9Rw0_q#zJs-+x(m1JH$ zWXZDs1v4j|*1<-7kGI|4H!ffLG(6Pi5Fv7{G^XiG zQTkFf`ugS2Pw(A?ewWB+GcsBI^%@}`*E<){{wbmxSRmjKgGpys5&rxzUa|uXdEOBo zcwr5*+bnUuGFAEQp=+eIQ)Sz(jG?7w_k(V14LOdaWp5H69AY6K_;J%qwUv;e%8;?+ zOu|<4@Q8B>mlq!Kx|j9z-l$p`QUmptyw~L!&ov>|Iazc-7LyBL&GjL-Gaf+u!+VV>2xX4Hii4$>@JxDMjeu& zkiXy4CAjEKE4;1es(wIPWo27wi6NC~l)cbp2^4C8g;$$uqh4d=r|>NC3eV(#A#o|N z>F;{I4Q6^fX`S33RbIY-V$y(mHzio&_0V%TSZ!@;KID}Ajw)kipOyESWw-a(%uf~v z<${x&ugKIRq=)6bJZ1{@*)->4hzQO!fpgKp#_VU!TAPc-w%rE6iS!3ByJJ@ z1M*%qpeL)8T+tB>L-jhj4!_wfQBU?1ffY()sbpaH`=69!~7Q&?@3>j5iDhx&L$JpMLtP}73bWjn28L$}W#wpW@O z`@BUfV9OcX3L=4Y_h_`yKf7FtoXc7FZ%ESwJ!YP4sY%NHlqci zfDv{6x{g%BKq3HG@GB6bl}HCj0svze0Vi5N>jOUlz^A6bU#&YvKsW%n$MUbA_+|?1 z1AyOc{=!*HAUyzlW&hV&9I*Yzq1<-*n}u=!ZbE@w+<;@PmCnEsC@|3LZ#L8o2m*k~ zeg8r%FCZcSiiNqA!WVc23B|?=#`FgU!LV?$aogi>n(k zI}0~Flf1curJEJ;-(r?zV<0uSHvotZs_;`6*2%ALZkFm=7M0Zs(r?C_wElR@XxK9v zrd%M^aQEP63pgYgmdT$_ic+S5!w6Cyf@6b`6aoHSG{tQss5!*hWT{&Rs1>ZB1u>vu zCyi8f+rC*DM53gktKsy~rmLc(YBASfki`TIQp<8f6OCU((QCSzP&~QH(ubmeFxhcC zImlqVuiB0l(P)219U4*yS+EO!e<5od<8pceg94a7>6jpdf6 zW9{_D3d*;)|DZTRyEsu?qDtwlHYQ(_83 zL}}3$?A=~}X4>+sii>V0?ezB$ajvp+azVVyt2xD8QoJTx@A1>}rKz=MkYYpOA|3YB7s*>=pePK7({H}P*xgvj9_0x2M z-9*m586G5Gk)Fv%PoXQGY|(!9i#?<0v6tx}K|j}g$F1&c|8$7y`}%q29DD1r+>Kd! zD%32r93q2rBKbrsUGkT4P^pE+d^1$ydiL?2+tq0~g$Z<_of<;wmj-FFM6`;DNXp^4 zI;n8I?@24(4E+^mMTQdrR`JamRc6g=`CI?3kZf5pv z&UX8GKB;4nvpx?U$}D;LVYd8vMIg>(a_Ch(NPmQGB)ISsT;6(d1bu&3J1rW0#!NczvAa8cMJH=CUx#m-jkCD_zQ zl44KW3emtyHSN(rX+o9LK1t=A^(f4_wh>a{vif-dFB}0HIp|ep&{uDcB*$zCJ%f{? z__qKJIyGNtD1#&~GtHg!3=RFha$v&%Yk)2^p<%wfBlenxD zP%wI_9|#o#g!t+R?-4xd)U+>&J1C-!bM z^RpVsq)Ebr$~QoIB2K&zEg}fwOm}o6<)B?Opv!-uRJVarwpK;U4+99LLo9x8tR(`u zoiG>t`b74v+Y;O2Q+qidwTi7{m>W#s``{&DJ!k*-1=VCW#-Nj1|-oGAl<9 z{6s00tS#$>#NKmy06*p1`Yc+NTkU}G;Fp6rUpc>eY00A;L?#Qx`p!(_YP$T8Qf)n3$&PcRkY89@x@f2jzAM<-8=em?HEJ7$WBv(qFL3 zcguYZe}wE^JA$+fe!yhwrDElF(R|w8%;9MIad0sLk`nZH2~!$4UYK@IzoYHs*<3_> zvLZCBJuAB!oeTH5*|f(r`O!M^0r^&nn@bpo7ewU>(5b;L72oqsx`3twMnNPqk_sWQEY4!m+Bl}9^=1W!<#=F5 zdGaA4VKmIkukFkYf?Grmg3mdYhuJ)?hok8$FAKlu-9@kIWU#(Idho3r(({g>EjWVnlx zFM1V|HMd=}xUH-4DT_lB0{k^tFF(EFT?h~@4gq@7X9a|k6)lOl`6xr>0unYsRND|O z6U7$G5W^KMNt~hxzf{)5eNa;-)#jABnq(`>N^w9wU-+c)%B^Ya8*^4AZG3cL?MfC! z71owva^`g_tjpF!wrYYi4FZ|8AC=c+6&zO({ObWP#t>oarxtG68Wx@Mt1`MF=9uLW zmYK_D?Fex{>(@HgGWq%zj%0qcx5Kn07z9OsT^3^q&fYQb!hP)J=KpIinMS_a$Y4pk ze@zE{dt-)E`${bXYmAH3Yn&cf#EjhJp!Ytn7~czbSWA)_r)^^Aq>hh4#rWDT?yV>Nc)F z9-k83^iR#gFiR3qV^ge(#mOjeX)65ZdGKX$LrAb;GAS$MB#jY0`U&%KP$v?s!o=Cg zGf66Np02HX*23vlry*O3s8T35-gC4vUFtApVK*#?Q%X04x+~pA-dx|BXN`Xo8EAnr zok90mvnW%vMY2t~3{x}&59i5ssd3(q3tY0p0%a9bOV@kyWA~uS`=MylR|ARWp`($5qT_?)wxH`8=MR>GxOxz4*Wqh7 z5o_(?YqyX$Uq_$TU#vNV`HnvdiN-jUrR>5PkHZL$Lj{*1-DFkbCQ~=*~}v crXGo=#zxq{c#%LNcs3qxcnS&$B}w@I2jRmr4gdfE delta 10932 zcmai&WmH_-mW81xBsjs{-QC??gS$Hf4O+o9I90ei!GaVPJh&4A1a}MW-nsqW?Z5qR z&VAPU_C7MkI%5{4y&p(oMxBY+ED7LxE;Gq|!N% zj$r=?Onre#P69%JxG?cs&yRVH_?XJ9G+Zuae#7xLfB?aO)2CdM=^eJh5ojYjq;X;0 zJr}1$!p? z8J;OPj!2?9VVX|e;aXk&y`J69xIA@B$Rj)z>lO7@bG%oJ5>+HyU}v=shM0t>JI&c$ zV^r5v+b-xi1#TYt3fCv8EsQBYnesUak9zHt^<&~tE_Y%cB98ib@h)f1V5EVV_$kzJ zT2rS5Bp4LAm?Xtz@YEXl>zUvv@k7fxRKuCZ6b2iudEj-;6ZkpH)V$a>K|i>}6Jn8i zb8z6*@rpy#eDZGZ(m(XQZuZ*u3J7(s6WE;G22&8gBEeyu8=6>CB!47Tp41A7)=y_8 zsFe{9TgrFA`Dvn4C-ADRQaJ@;Y$}kkQ_Ej^cpNwVX@|F9*CV{BgLo7lcQJZY;xz)3 z_EU&A{k70lOoJ}Fy^c@KVEG%N4*m2<%)D@z{sMp&(Fw3%yUJcYfi5qO9^0~WGF5i! zzZ`;PJq~v}aFK+w1q~%X%c-VDIp;7aV^qH4u;~k0X@tPb{Eil&K>atAzQ<5?uPO1;gblr=Q zGgB-m-;kx5MYh6JFT#*+bJV0!#8UrqQtKV-C?|HdK-enyDw=ZOUsz#HkIXr0ZO2+@ zP-vxW|7soMd!aKdsI&*t+MMC}6X;7O4UhXQ6IpAy#JeB98|d63F7MouggRs~8LE;* z&c|rgvb>5A#-L7)__q3Gt2fINX)y?UV49eib>U}a9Q?Zt_8HbN#`JHAbwxr0&A}N8 zblQT~PX|m{9XvvrN^Qf@=3D&ZrR9HA)jcZ9qcRSWI2m^Y7NRpi!74o_U8?a@BxwC;1E%7R3h%6-U%2*3L~%*Ykn_`1jUrgsbk zF?~A8z`ke_cII;+Uf5ho9QL9oQP(@|kkKHn4pmz{xo-K#a6C5#SZr*Ll<^q_fzR#T z7gvr>6FkXuA`P;1NH$4(=_NFXb#N&N4^j-|B*SQzR`D1?%}$h6Xtg+oFyJ4m3E%zr z1i!4DMANVYcw>IFur@}OGNnB=O9l4lOtHzSIb~o_5uEdaHiuS*W@Iw16S+h3acn7u z17#li7NjE#G^({lUb9}J? zZ3X>(L0&~_CXry3&(Y_Lg9^X){6?=h2kd6RREsIWJOMi42b(*;6{^{&UqVi3je)8h z?j1Q{xVI-1lQwOAKhBQJ{HfL*KZss;#UHqk%Jc&cP;Y?kpNi-liui-`3atE7)B(R| z#C6O+fm&ytepj04)l}A4KcXG==%F>UM$j;{CI$$g8g`HgsikH{ejW=ejt~MLBBwYB zimBcMP=a#52@FJ$p=JweKL`|mqc3KoR#E&CCY49U!dMhe*0|#$TKait(J*J4CGAby zE8Bfz2*U%ud7ROig6X=v+gF;^&gI#&Eof1v7GxO2bNiOc8cq8LFKjBZIh=8r5ZuM$ zeJY+X+Z)qn)&$4yQR2)P%F|;bWM-G0^e4pFsP;HrFw*mbx8Mmce)35OV-KGY@a4F@ zGwvQxk7VxNY2kS+fRAOxA=`?M)r+AaQ))Jp1oMZSi5%M}bP8&mu7!@bHPz!LiFfigd#kCCu^{>A75nG_!*v(V5Y?5(64M zw|Q<#!>g=bm*6?JW2k!x@sL8_1$HKm#Z&;?$9IH~q{Efg7e4g|ta*)ap}eYZPw-?^ zV_C5;)H7w9Y`f-ddPniXsX^(1I67uHo260Ri;SXlXm}BK%02O|uCBjMNRm!`;M`r9 z6TOaW&tBCf$KReP)JzEHPinyOyP%CUmXFHFHF+0@i!G=fBqCS%jdZ6`^7RX*l^)0& zZAi??yWi_*&oF2uadTi?syt54@O*nG^4SR@9XH)^{U*hxyd?G6EO(8~-^0_&YFJ$2 zdrIl2W}H!ME!kDk2(HBEYg7%s7l?|DAWff|+IM^Kcoi!SOaM2<4!5=&z<^Nodo39S z%w;)!LP;mbCJF((n$Nq2Z=V73u&%5$qIdq3nCNW7E7zB(@9YJjbYi;kdGZBHehdJwAkzw|o{G>xt1)(( z00VD*A>TqPKKb}9g*?ZM2N}EYLp9gt#LgayufAUu)v`Z1IwhV2!tRK93I;Aogen&; z8q@*nOXdahT~x_#E@v30g{Q*RCOC)j@>v4JHUlaJcQfBnWGYj6qM;DJZ#xNg`7x15 z`+%XFfeTKZfx`xH^EZC}+$9O%7HpL0!xn+%gd}aj;WXO6=CQ(Z|F4D;v%nIQ!1Dgb zC@a7+h`{pyV{oA{;jm~V03N~rxS9gk4wC-@ph4eZjTrwWob16WP{8u0e*TODRYC*+ zjs63`fm&GtbQl4={{>9O0gj3P1x%I$yjlJQ=>G)Fv;2DmDOflG=6?x^EO6h*0et^U zz=7(iz{&pK5gP2_%q9LM&{e{bGyF?1oPp!Tg5`()y@`Ev0RMlRzg)oWyo2S0dOX1) z;Qrh91rwNw^0)7!5D**UP7Z8>o{|7v0T4P8;4qYi;vZ>D4#a_$Q32WDASqNpZ0J5M zkQo4(qy4)|#{j$qK(HBrxDY`$U;}iE87KvSkT3%Wp+{{0NE)`k@{;o($-)WLfQIt` zTLBOrp1&A%ejp_rM1=ou0iW6s zurv@3NgxTYW&V#X^NQY=+c5jy%t6&0}rhy6IC_Kzin8;5hahS+I! z$S1I1b)(zWYa43Gt8+`=A@JitNTLrYP>BdwN)=0CnYvo z>es4BYe>BTpMy5jk!No5#iXdAu$a*; z!M9lwugjEV!xc=1D5oE+1!2v2df*d^xHs}&hi^F%5Mz4G8pb}?A-AZ}VHnq|{y~Vg zPFa6Af#zOHUMMD?==?Y?3VhqNve2Hw7Nj{Kt1KWeL5l+Yd47Frt_S_TQy}3Foj1Kn zQRWZ(&|;@(%^yPR6A+U2ky`)EKk~Wqol)A|Q2)iw`8SYp>eNLFij!^I|a zskq+&q>CTwQNBW)X#2yh8+SJ^fyFCwIc#EP2Kf$L%E{a2$}=xfD(&D-+s2QN{591^~Rh>N}L2owo8Xbw_ zk2A$cQ$e;h^9D*^ZptaPnPeq*>`*QD^b*z?6HVRC2te7No^SUoSr(FiO!P`S)pPBYZ-pJ}99MQx!HU5y7S+owOmzVj5f^qA;A zyg$4KgSDFzQf?{3#`WAhs=#qAId^P1Of^Edm)op4N+9OuEgd10UGcF>4W^Z!mA~s3 zgy-cJ(aRlst76CJI{Ji#Mz^|$l!y@;Ex)aDk~V{v?YmbQ^`3ML{QDEXHZibIslDyD zsv}Y~daSTdzr6V7;bKO%<>UmhiLr)jiB)u?CLAv$`n>g!iIA0ZuwS!U3 z*jyIGQd8ej)YaVCI79FbHI)jAdsZ4U&)8?pn@Awfnr_UK!W5OOX{8nKslzSQXG6-+ zux73b!-kEst+kkVh&sr<9^%)gy1Z8xFvtie)&_E!Y677;ZMx??MoV#8*6+ib4ET3^3Xz0Z zc=3NcDDd&fQ`KxF0PG5|!BXap_ziR^W`oqnS#l@!M0_a?C?wFTBE?mr_gMTt>et-f zF^=O>eTO;IZQ;!R5y#2L>6d`=4V=W~#t2fZ$3gsK{6RALa%0zv0pyXT`*L^22Z~PF z$t2njLDQzpebR+aX7`;&{|aJ2^&CBTW!=F zN)Mf(mW!F-Gq#H*myOXQOV?uO1mkAnll=$S0nEj0D z#oTHp2AZuIn3=_j75!y2y)wx%QS!Wx{RWsvI1jAp6=L32d}mz#te1Qk9r*Fh1%DmM z`}H8t;dC|6fz>5ZGK}u;+vdvh34fJwU4~9gcC)O@j&cH8oey+%_J7&`o;;@7?YQ%5ut+7ESi~{K8u{P$%Xa< zFBd)?mTdE#pz#*h1ZNHxiz@oGX5%vP*y3^y6D8rP}~JHokTw z=QmZuUyWZ1(vVxe%2U&lE+zGBelZ`Igk?Wv+K2{$SBLA<{SMNvqolql^GwMrnwxN0 zZzLh0xErGqtr3opa?SNDOoS4*N1{5Pw_%)G-D3WLSSPshB{;mbfD|d zP{k^EqB^!s$HvC_!3oM@3&vO+$8k-HnfNgdMr)rF7i~I9NH8VX=c&_ixjG}w$cUXt zmkJCT_`K(PgqhJsuqG6@J~kN27>qNA^eg@SwLs`Z;YaeFxx{kC^MpEZPs+vRl2of1 zipV>)TE_>vD-0sdQ)5ftzsoTs5{rXzzzwISq(&IyGBB1yLYf}+So_TV-t8yJ_a67^ zv}*8J>y0A2z1wBOWNJK2!*+F;&6GQV+2sBQ5hhAGxs(`BRFp-MP>;pU{>Y~>K?~`} z6;P4?b3YQ$F?>$I6?#H- zPKDIu?$4sBC+_%NA_>FZ#T;Jrb5G|5P5)HBZRe(Mdf0Mup^Iie7U=pKrAZ`|LQza* z;O;YeG{3|6*$-1(swVx^L{mwrIDhPfBi1UgXE>usS}7a2sNmcZWON*DW=yA3=K|z5 ztl_B}ti?6#5yi*u$w)7G5P4Vx8nW_$Ylg=40;U+TyA#&Sr^d9dPU* zy)`eg5PKCM7l^&iR3o`^mqyW$5bLyP>sWC!E)csC&j@ztbbwNvGLusa>*}NS$G(h= zn^gCIze}LO&Fv}1#7F)5?xHDRx}p&!WI6JMWFGfLc{T zm!n0!U{0#`VP^bkfW=bz*KM%(Tn?^*qM2bC;G^0{A<*^u?VGgn;{g94>OTF!uFeY{ zYyJ3Js61Wx&+$E7xzG?h!dnD=)1>Q_fR?_2h^sc5(@-;SwTCWm5a2CW$Z6~RBWVVQ&`|oEa=kPEAfBRAH0xKMEszP9Q z0uW9p0{nWQ-OI>(4hV#haNx^pb3^Q_mTbbCQMIv>25 zV(fOblKyL`zJTb7r*viqsjdf`T6T3J-(%6JA9VMgWb7sdM5bzQL(}l=w+hhRyI{g% zXF_vgYub~Mnw?^;3LY#-TPr}wIpAS~?mp~APtmqTZdQlxtRi2=)KbM8 zqq(%!!@Ta=s9_7|Vdonezb`HF`_S4+n(PApPN#E4*UNkQ`%|st+SFP-&zXV7$l;3Z z1xUinBb~|lf-%qRqjEc=FES9~Mnn`S#i+=tLt*vt6Gw*6}3r7r^5 zOs{u=k?iN(_Q-|@U*7NnbKV`h{oc%wFX+yc{MqBp{O)^|z2%~KHl8kp&%+Z}w~*QM zs9BaSSslTJ4LD%VD$pd7#Js$7y?dn&(QcpHxaCjUB7$c(lZsg0O;p%+Kyjmm3Fc$J zLC^&lb7uUhGn#;cWdG$|m)u3-W$;5mpuQMuemdgr*k#2ZNdDON0 zl=I8%NK=qBklAkcPoUPq?w{kSMPkgG-^2VdhGuX_;N#=QW;x^q%?b$pdhhhCgi0WkZDv4yi2Gwdyh8ICk z8-J#hZuAHajcYfF0z}OjV}a`W)^^91kHRQG%lozWAs?2bH)g^xI>=8`kw9cV?bR(b zp9jPZ-0w$2OqF_cRbh3|Zi7B}6QsLby6U9fUA_J}-Y8+KlY5Ch7A0 z#Gj)4p?rt!_g80JzV*}7?*UH<1{cHznvSPyI|9D_N?y5Nld6`-opI|-zrWo(zKL;T z^JQP>5aOQ36MBDU$+=8su5tWERE@le~p2G6$CckzzHF;=scnf>aU&xW3%bs0^NAi;5G!HVniBf<&cdO6) z#H!XV4xQ>@i_+89Lbn5<(dS2@@`5mX(!(tc%}~SFY_|9?N>6mC5$7+>Zmd^+z33+2 zEX5VepRLuO3a1EI(Z(oqu6;S`2%8aOd}yN~`dVYC!)b4ADR?|8wK(vqJ9B@r4XwLf z4-Hzt>fQspRgtG7%zs%-Tm@s){(4wqqB!dcym*`!yFZK`@(%`SFx8yN&CutpbbbSdjVGFMAdGUFhzk0z>QkGxgi)(dxUL7tKcBIZXRkF>LG9y<8 zzi)Fyv8>jA`*YKA_cSbpA#SW^=I--_94UMQTtw0Kynde8fKXYR&a3l$dmd zXpx^^^3*22xnT-o?+ZlF9l9|W=qW3Y>r%nof!Eagg%4>wo68bfN6>x-+e&bXmp6I9 zpfYsls~m3=+C1jWkDj{+@(G+`JQb(<`HC>IBT#eA##L`Ry9+*>CLA@2ffWnzyd~+v zvtrL5z4SrZra^mADD24>KeM~NKHI?@{DQHO>Vw2r^& zXa1H<_N(_yer_GJIfoEwJVN7{K{WGhdk!kwQHy@dSgn~@=i4o8+-??-b<=KZ^b-EJ zN%Rk|Sa`e+%-(gqF!mPYTOu3>(* zYA9>q2oV1DS~M#y^!u()qUQes%+UdM3=m zsinhrFWBx)#@-43>Sc1^-LPp`DL0QisF!BeRCm6mtGTn5x(a>506qN94?a`LLyb^P zeDkE=5Fh(kV+GyStpx=MD?7PbS~Dky|7v+y!lWikNEo6|!JNYwI>?oQgp8bBAiA>LR^p5-q9DSoj z?*D!j@^Gh%A z9;-Es3@;aybu^KC=#E=blRG)y!i`ITRR87RBd<;B1 zd1u&`VnS=bT47`atSlRR7Lv3L2-S7f)_Z5jeN@Gb<5Do>`nL;hok`S*?+X+}I`g|0 z`x<+uJ!rp0D$%Ubo|yQ$H4?TGZRc60!qqIZCZ&)Juo`A=vI z3D*4^C~EKnWua(>z-0iW$>47|Ic*MXhc=r4k>DT)#=r?^ti?a_yE$+iYH9;~_cxrh z{+lZL+XGqPAa?eD8>(D^jZkOjf5OT#r@twqiQ7LC;`;Xzt2Yn|)$#xi10c~KfuqnJ z?|&qb_g_HwCm<>ur25m}baOobxC#s45`=UG0Ye!%1ULk^c$qmk={Y#)8Ijpl-K=FS zylf~KWQ4dlxOh1^IXM4Q0&xfib`$a;v&%VnczRKA3vwc}tJt{OdD&BN^8QV7B|$(D zPz(T91MFd5*d+g5fwD9iY|=#R{~H9d{UadIknI@Ipv09&D1Mc&O`}{&178@A%>*QY zw-|iSgo~AfrG%Djh&{?WbD&LNi4(uAFG-stf%zdxQmd6=ARL#2hQ}CpqnrY^*uAil zE+;hq*Czm8KTAVWFM%qHvC;6ma!d?Qkh=hpY*U1NCB5N$1bW~s7kWJMbE}0+NPbd| z!g*>EPOL>NF3>zIYCTX=X3p#>g;;BGj6&qO6f&L(cjzA>kOX80I@adW>7 zZ4(@lX-HKO#}I9<|E^dD2|@E5dv^34VrF;?CTvchVMeGT6$(SLG_oRVq!Se(XcE0y z$@XC9=6J;G^|*m*&bQizJM-_Xc3Gh%I<$UlS>TQ7ub?Rswl zPox~5+$}-v^Zq3^E0>I;!cRCR&`)m6XfBv7*#^<+-lwaFkwUmxLNe|_YM1b0Es}Q8 z$(x7G*PD?35grwMX%c5mQ}V2tC>Mj}-?A$S5dG~Y@10Q{Q)L;T29wj=&hKJED-U%m&!aapG)}pAolweid+A{Y zJMEII%dX!lWlz=gFrSI0Kx5wUcK19!n`g%zXb%f#FXz!4uMAD%Oh<`>kHy|Y?9|%R z>#Dt-=2i_t_gZE#0e%WrVj{e8{xKG641rx8ej4Jag)*$z{eW9PZVy8-_D>aZmR7%f{FP9;D?UptbWfmao{+CEbZX zS#Jz(8hd@Kc~r4x?Q>PPskvd==QOXd9IRC^iMG9w-POwR*bW8|Q@w*UUc|z$UD?tZ zHN26T1>cWQE9Dv>RizruI1}M#!XMy({blG2twPuQwJv`D@=~E+;+4J4en0z^XN{be z+t+7HO`4JBP;!8S2lDvZqrX*<#a_RA0YCbR){pR)j>#jQImYh)MSz){X;IUZy1 zGMgMTLt==L)=<$T z&#)XP^^YKW{*r0l0LfJ+L;i7ThF?SNSZaBr!Gs$ZrBtaejH5I(Tc{QcRs1ZJ$;Gr< z`>Xm#k@4H_^wz8l&}lNh?>yAsfd9s^ZES_BScw0#v50W!XR2&eMfj=sf%frUP4?nD%>kK-08)WCO_15O9sF%5xVirh6g>(fP6}>{e-^de-2P4( zE&&P-3N2)IMORz5zfSPKPKLrrM226MkDFhLk6%_=kb_^AS6V=hSBgtOlAlvril3KP zMvUVBFEK&=zab{T%aMu&Ui1itPQA;KA!WGVUZ=f@dG0=ySY5T6pI)Hs;2e`u-k(h#?AMw`%BtdRWPBROMP(*8{V>h0j=$OJzW!u3 zQdd>iiI8+8t~k_;GAH2cNBU{LQsZDcBsfaCuV7UYWswQ5r2ivH6@1qNP-(3RmcDbf zxuu--VPhl6i;~~OqASaAA0}8sx$EUw!NBN2KdtaIiSWw$IXnPT%Lp-8oREQYz!>i} zT|~TchXI>+8=X!4K9m#~|E^j>?T(Y6$vynAI<&!pO|L+E*t&dOp)2?fBa|$wk?Gi- z=(^KR0>vGH_BdT=)#ek4m(*7XNd+xB{YST1KCcus)A2)6T6C(56zv~1ubqw}@{S1K zsk6jqE@SZX4{~Hc3#I5#`uthaT#?e#0vBwT?4RXcmReCat)fqbY^VE{tX1Hm`P>*X^9vsg9K7aZkGVt9I!m9S`d{!zD0Cx32vG!${ExcTLm6zE$%;F0T)ImHiIXr z3+X;>FHc>wUjt6Q&br=3=%wAZnmrjiOuporrQf!%Kk7Sx@}EvVmikSNLelX>jDqzX zy6yO{50w!`0_sc-3+&cAOPdbbO!S0y{7#rl`}5elD!m4-P(Tc%H_v<6N<$)VmoBBW zQ{CM)UMpAYT^d504`%s{xz|M}Z@(GYf0^*IKZ+qef{?44%?~U&F1Xfs;zRMwEn zOwr23(R`kDNymMFH+vfqyBp&w?zP+kZ&vP`#T#4Vy`^TMW9#r!#^`x*cgDtq)8Ym2 z*E2^EV$*lBA&9P