From 27933646234b0671bb585bf9208ebc7494d5aea0 Mon Sep 17 00:00:00 2001 From: mrwulf Date: Fri, 10 Jul 2026 20:53:43 +0200 Subject: [PATCH] =?UTF-8?q?paper=20v4.2:=20visual=20PDF=20inspection=20pas?= =?UTF-8?q?s=20=E2=80=94=20fix=20broken=20hyphenation=20minima?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Read all 18 rendered pages with own eyes (per author order: never trust tex->pdf as a given). Found: this portable TeX install's format ships a broken righthyphenmin (verified: \showhyphens{its} -> 'it-s'), which produced 'a receipt for a leaf is it-/s index' on p.7. Fixed globally (\lefthyphenmin=2 \righthyphenmin=3); document-wide rescan shows zero short-tail breaks. Everything else verified as intended: title block, narrowed abstract, T1-T4 with x=0 note, Def 1, G1-G3, honest-width 4.4, ConsRec display, frontier Lemma 2, Thm 2/3, claim matrix (auto-numbered Table 1, refs consistent), exact 8|4 Figure 1, forks Table 2 caption, acknowledgments both assistants, all 20 refs w/ pages, App A verbatim values, App B code block, App C boundary order, App D namespace note. 18 pages, 106 tests green, accumulator untouched. Co-Authored-By: Claude Fable 5 --- paper/ltl.pdf | Bin 562270 -> 562266 bytes paper/ltl.tex | 2 ++ 2 files changed, 2 insertions(+) diff --git a/paper/ltl.pdf b/paper/ltl.pdf index a5722a249cf0602918e9eaa745028f9014e98195..c4ba9a324a58d0645a2a2cd5d40827e3296e3048 100644 GIT binary patch delta 6150 zcmajjMN||F)bMd~Xc#FO8j)^>uA#ddMx?tN6d1Y@q#FcjiJ_!nKmi#*x;v%2MZV`f z=Ucs-ckw&tzqreL?&7XhzFDe#(~$3yCG&*EmiE)-73}ky*$kT$pHv(`=YmXYSfKJ{ zajStrZmVtbTYn?2z3n?{T2*paT`vP)BJzc-M)?b`fYaBFsXtfWnEc%}u!6w??hcQN z3>qy|@>xWoU7coqdgGgn0^ItvS5c{)h6h`#ZWqvN>jyY{hm$#vkz;jf_4|Jpr}eyY zLWP^c_ptJk#=}$OV2IYr*&B^gjoEbP{6q7of)nE`qL|(IBW$Vkyt16~fXds>`5DXg z33nMtXSHk1sU@8+pM5$(CQBSnyx)GRJpDBTgeG+hRZUCMl*TY7Zjc#q9*FvQhVyu z$BVCr6Kdx3tS2gQoad#)b5j`d{pqpJJ0ycwH~M3H$mztSui#E+2UK4$#e{9)VLX|qPs@eJ0GNo1 z-s(~yOv}dVm!Hub_A0#Eae89LPs3y#hUgMh#y=&xmrkzA*k#YGDjuVuT>ACz77*=C z%rstdLmau^gHr8MiAWv0)(x(I>OYQPM5o*X|IVv6W7NM>u#REr)15e1UO(9wXf@8d zdpa4U&!C!Goo=$s&ozZmTvO$5i75|X4kDv-G%aiVtX+*L0vaV`$x2F|TTLM_v_lHs z9ve|OQIPA%vb8fd4o|cVJ;#wN>ZQk1+YG0yS?OgZ?`1rCXzDIR+6FqHEb&-Xd@{A~ z2XmRTg?u;btnKK2#pJ;0oN_2wTgipK(Pm|Idp%O%TJ@H^>Z>b*Tg?FZpQM>_?ae9o z`KbX~nFkvvPTkbspyG1BRs9%PT{lCL!y*qlYFBBD*{r}*bauvvW9V`PSLdyuBr(4S zCh^>0T@N?q6a`4rOpseW+F^XohTOTp)J6RMxZbe!P zR6(zji2Sq4|2lMcYC^f+FhRq)NTw>YO|MAy$3v=d{~NoW7gq6lCh1jJu3|5Sz7u<5 ziM}Eo0ttJ$e2yQ8R-Sz^F6pTxusNS(_o{K%OUELU^keD{8!fpkD>zaE3NZjJdMGnS zqW8jfjm`+H2arQ$={j)9Tf1@L3-ohTBuZ+^V(eM~Un#h+5REh5m^rs0VEu0NHT$@M zm6$3o{sa*h=;9}Rkt-3Vi)Pf?3-QkR2QJk*YfV23@pt5iq_<#u? zmo+xB{ANEn09Mpck~jvNY5Pvg9&x44wdhi8Hl|+F^K5$p@Cu-zq>PLl_6KM-yxWV$ z4=kjcF4PEdC>g0SAXj#%*tw^#T*lZYz3YPL2{`d#6y~**wm?(%3=Wt2;wfiw#oF-u zgKECSj+#O~3f?CNv>odZ%n;3Ps(M6t1JM?9qk#PF1JzMQw9=oPgLY+Pft+n{Q`=qa! z6;R$01gk=IQ*ZFO3k!B$?7T-~UPvdhoH^+q59-6`oA@OC`VTP+h~@DwfevZ7eR!F_ z@W0(j+Aif?s8ZzUIyi9>Psk>e2zeOgCOI8bybMz69ya*krZc`>C=#YqBQehZY$c{1 z{%q20y@1*C7B-jm5-xG+?feXjIlOM7=dVJ+feEaf6I^gID+YuLlUQH2kD4pHKqN)> z8J9nzvTG5zaCU?n6vpb_2035DGO7w0ID=9RD72ZCMWdXekiay@tQziWOwBc24@~A& zLtNIT@())yBh6ay;MpmxG`PWJ4^+@t0p%&+7>RX$b89@ktnbKZTa4)266bhv0wY#o z_@h-8@VR~(>XOBV5)?kGQJU*l;37%?GZ$==<-6Xou+P??3e7?h*hGVPI$cWElo@n2 z1a?S+naQj%_`(zm#=ob5Lw*Pw{Q_`_T*!r~dQE?@t+zi!C7&y|Q{mO!~qJG`mANf`Hd|wM<0oWzYMlsTv3mz8cyug=EAe9k|C$Z_`%gQ zJ@t2;a(o5Qm8j{wqU!gvl9QO6-ZIsL$jJktMtB_rsOE>^kOR3 zFV%gUPtLwfdUoE=Ra)1hv6iH?pd{>GS<$>;%M#0sFW{oJ_=)_i3oT#O;aV^64^ zq<23tJs2g(eF>+B0@sbZj4S~(9sKNJH(i`1v!UldGg=O2`R!}cb%NkK&_B>z-A|y% zNTjdhZZ)p`_;pauV19Q`uv`5QCS7PH^sC@6m6t-$M#OxPO+Qwza}sHa3b$f+A8%ZP zWrr7=Pz-xrV7{EYy*P7^)#N(gvg2pJ7zHTw?E$iHLOsdYfs)LSp}&!AHaw)R(N0!& z1$S;V41;X2p8h?!6DYb=1`aQ!eq^tx(g*79&p6uzEvG0eYY(PIs1QWKk~S1WgDUJKRtQ=UX~EckM-$Oy|b4D7s1LB&LgwOS#a`J|CB zGs?K!yhf+-+z!sTLsuNbOl>ax&0HR1uKr_>`4t`y^DDI-8`{X{@u| z{}bcJtHh4xHLR|ME9@hy=DJ{t#V;APjg1Iavl0wM6Dv*tbyoJscs>zY`x;8k znBR^HrEko3ZKlNu1f8irqYZo~W=qy%`@)iN)zh{{yI%V9X{3A+5G+8dI!wovTh9J; z`0KQxc5XK1t6U&uBMfFk_nY~MX;+_wgKp3}cJpn{@2jAr`SN(o>RF10P%raeZ}*lS zAtbk!>}WS%pgVBgDd$QaT&IHt?PcYP*3ZA8e-EhEm)G}l9J#*X($_2B!-uE^a3FS( zSEJ$QX6t~#cl$gJ)0-jd*RJ>;ndL=+n>ZF-HzuytMQHLWqp-PTN_|OiU&GyP(?5=bH$J0xv*z~(^sbstSRr#yynkHrfmd`Cgjy^j9c1MGSJ%e;EF z9PRPvc%DR|7fjX!1;Rm&8E%C5{-=0Vb~6c#gCs8`<7S}ZT}UuW2l0eEDh*fv=M13(f9?%v$u=?_AVPKyW^H%>DF8NV~4@vj@I8*^~ z_lGJM&u$MdMw$aHxaaxA-5Y%_>I+R52t718>fs5AveQZ;Fb5wYyodCZo+NPRIm|IY zgob0-7dA*0ajhlPWV56p5nFl;N3;Dzw$lOW=xmWI=jRk1ApMN4F4=@$h@P|yYNRJ7 z%c(-1k z%V2kQ@F$8QLe7qh3_bZ9oVRTR(!52|hmK)BRxP7+ZxU19((C>}7kanPX_Z`YURaRY%M{8qbt-eSwXOftxi9 za}lGWa=RM>=!JJTla>qpRVFwIwnTPc_tY$zP3Bmwb{o;>jBm>iORd`1VQp?*c$HDC z3PN!T6XQeC++}O$vqgpDuIdVG*guE%ep~fj8;95bxD@opG8vdJP`5Q9aS8Ay0{h;( zxJ?05noOyQ&KhUTcJV4N2K_T>Bo=C5>_HWJ=x@l2tEnxxvie$8VDI6MVWJE6Cpp2N zB%5lSd?Qvr=d??ZEeMcrO#K=|ODOGp4#JI*K{7eqt`s~%Bh{3CIrmnwdHnPK=;*Sp ze)uncNNoBv$~-f zDN?+uXT@8c`RFVFZ*~pQZ0lW}_;x!%9Jvdwv<(f7z|ufP1e z*f2jpr>F5w3pwDYg_YQVj}P>K>4AlICzui*<5^?s2cD^dzB~yp~mwF_ZUHS>S~VFFl%=Oq&aCq4pw#5suLb0yz zU8V;|bf5y!TDrBRG(t4uSL>WhGQ>7oUeXw^qg_n@q>0|o96vSINzPSh+K%_!1|8~U z75xqF*fXwA&n~K@^6rSVsd#x;5ZpqNEsKX7D>f#^ON$Tg3GykUXyNq?~ zzbk!YWE9tnB4`2S4xHU#sbZUXo04?Acz9Z%Q6_o25K`JKE_zDB@&o1QI%vhNe$(J; zGk1E4Qo2Xrx=8!wFdBY3pxQ0jx0{O@Vd#^j!jM|t4K&QOFm(#5+bY$FLzt`ae5A3b zw_7wf#iYcnUq1fB+Wj&2~2{_NIXXtcf9~(-Gz3OT2$N!WUq{C;WV4}Z%@%b z3!F@*Hup_~PloqI)Mzif$~(9H8RY}v=hkO>1A4YNW;)ui;4i@fvAxveuU$uC=AU0M z5ZOl7tbaqCg8H+vrkdOola zZyFrQ3S-Jdx@Rho4(Loz~RlA0DU<^xu;7*fqLbciIj5O06jX|AOyj>;d;Dae8%G#l`a z0U!I`PXKPio;Oe&uxK`be=viK>F`6{@GQUJdjWkeh0w#Y%+a$znQ?W%F~$ygeN0t+ zdxSunvKs>y!uo=JqxUllF_@(=HrGV`j0Qu_f+8_=U;~>1Qwc$ljV4J>8GU`s$4lsQ z?6rU)f~py=*Y!uDtxxOR`$6DU$&a+qq91G?fPBoQ#Of_h5v=hDM-S9@s746Ethy9z zDj1qQr^HoLs~|dexJgKfn3a3o;TOAif^ubT>R|};y@}5AD z0poJ=KFU7vV$8Omk&HG#b5mr`Uv&)LrI-I{vcSua^NA(PcA}B+YpcrP@+|$9eO2Yxp}fLhL2iv7hMdkmfooR;|R1fb5uZ0)K{Z9!*fjw;S6KdVj;H zQCz2#m*8}C-O@(uf^prjkekI#GiC)h*421aeB17T8y<(Gt5MMK;_x@ z?IJ%UTx|IY)8Ux(CiY_4 z(L5Gr@RvP}T)|1wjW9WrlPniENtYR1Cd<5rF<`o z_)(DM1NEF{qO_h;h+2u`iTWz;gf%fXgR9M}!at*0nE@1NL6z71lS!DJ)K0$U=GSeY z6SL@S&L-w?`&CY-BBO3yd&ag*_@BXyYZ*}?`yqVldl9>sOJ&Wv-}x)|Aw$t>PF z$Km(tv%T?|3h%>Ni5n?&-*5!%+X%rO%R2 Q$0o++#bshr&{D+xe^Mj3Jpcdz delta 6140 zcmajjWm6OkxQB5%b}8vzx5>qn5osirR{A`1 z=Da_1&u`{>@&5$(N;%6$IZJ)^d-PXG4-#~)w4wJe;OC{aY~jUe8iGqhM2&=#@~ODZ zHI;K;`9HF?cf!D+-u*M37N@kvs>+Y`eLd;yR>aefa)zRvS@uo6UE^ygVw6?TW7BsB zKJ`!4&?diDVSgTRZ@Fy^D(*bzF}k%fgbVTv!v(m!4mpdPiIDa@bm& zr@8LqzE>>?!-&BtrWA$(%nBPeQ<#Sl_f|aSlyxOudqux~V>$;`A$}9k9()(W1-WWU3z+y-))wfH$`x~rkvEmNIHVnX9@}`j#ew%!+q%B$<$Jyvrrm+bqa~k?fC;IW)fpJH#ntUr0m~Q zcj+Vcd$202%llKN66XfW@8@#ESuxG_nx?Bd%vlWn+8>oV_UX->sXV$~xLOKS-Jb;5 zr;PI-o*pg>Y01}s`0n_%JV0!AK4f8YVPrMa zP3T5T$GRUP`RuJKPGh45l8LxA$!mag{#A#H8gHFAI+y7qrb0_o{9sz1nuLIl-)c~2 zbyV~EhUL0j4VSF#LWsdjXXR~bwEfRnuzcg+4C;;*qwEYo4|CMdH*Uo(a*^u2LCVDD zSi5QO*xPvSFGDjs?9EYkr%@vCLR%SZ41Z+UtJBplAEBoQjm!uopw#nx7v_*Zq5u62i?N_yDMW>I zTj+z>ODt%6qe!azyyrr@qfRA7u1GP7M>pT+`dCYpOr^9FzE11j*vl92&zZm~uI2^h zvx{H7fxVmVOnTQcM&&PQfi&I{il>%#>cB}~QxOtUG`tU;M0^pogNZPbxk!~W{#w35{ulNm->xzM3hp!-~(=cH-nSF&S zu*oPeJX^Il9Q%t&iQFG>Ae_W3N0V%{a}Lz%7b!-4yhA)g(L8Yv-VrR^c(mz-d)6SLg-Z5C?t#91CacZ z${B}GybwP*DU#wJ_qA&n4)B|FOx6rE)QQ6NfD>=1vQ0CNL0@&gq=(VUmVOCRmwo{u zf1v}_4CmU4G>y*X_sMtbI_B2r zTg!kRqTsCiqMq*O*nIVsj9cZagE_Y`G;i}6LInibrpP((9td^G!yUs)#KeA|%rbVV z>`E#}O#Tv%p9K=xg(gk>`QrL|HadTmM!9>`Cm5!ywVf*xZu*JEaJ(ynC=CjyJfZdr zogS;hxyVaV4tA}1M(O0(P%3axFoh!MdYE&E2H|)~XATaU(#RoTEJG>oexTjQ={LLW zkqPX^_2Xo^3}P)8@Vjb3ko>aiBf)C1iAi zpuO*U+$*JzSFS{kd*~vgW-9IR`z|qe8vKY$!~o`L{`+4?4eGR^(~p;+!uP=1Rjkuf zqO~oyOiX4Wyz*lq&_u$qPQqb$mbkh+z0nt9Ro^1*{KdFzG=WL@(ZTj(ihO=c_q0l^(_w9zx{ik{3T}%Z&oTujc1Q(1b%vw zoask7N-&hW9bfyD2Lof*pe4=V9lEVyd2*4o0Jck@OC`ei=vJJA#2YK3exx_qDUHM- zC_}M+s_3vRZRaVy;Yl5tE_bJy38u4lnWJw7pOO0#FE@xbm%J;lkc=0K@oGvW#>jWo zKVR!@*ScoHt~0GTe3+)eSvxPE;Dqfg%xC>a)9HBqD05aqyVRyxEMS zF)4oNS3i0>>xLav#)-E|=Rjc%Zz_R3)Tva7Pb2|QMPkz)2UC?XHWg-OcEx_TCmROX zHYTY9mXTnul#qoL(MR!=wa=62QHj9p0y{HQRCI<@!&MU^6E>AX;x^{tuPxm|@a114 z(s30&pZE%o82}EZzY?44*d%BTyvpt%c`BwWOt$wF7!AQdQvkaHVfQWaFv{3>X0Cr* zp4L{!?}>``NL5$#TN4g{Q;{`9Y7Tz;q&Y|mF-5cK^(q)}W!5(3u>y(2+;FjC1>mp} z12Xo1grb--P?ZInR+5zPaQ`5AZKr4AAxFt5*Zg|c&aD^T7dKU|GguTF;#SIiywsYz zUBvz#e_tSWovi-~Hp&By?d@@kyc0>WrVH4%JhE-oa>PMco=q4=gqJ?KC32Efai;}N z;w*rs$+TxrLiR^`Hv$bFXKX|)5Pqosek_E)N#iaJHez#9TayS!hDZ=|n9DS1rz_1x z)0!w!ywmKNJZ~iFKxrWS(xj_+=HvuH*?+0NC%;SctbJ51=UrL&4Vx>whe2E9@vW>y z1BKEMsO}PL=s!x9eP;pocspk>`C{ke$FKg@?INqPAO-;YP7=b!+*tnFuE~6H;x4&Z z{)2?w^Qd$#pD0{qyn(~$b^Ibpbe0|S^reeQ7L2mO$hHq-Jczj|oo@eGV=1})NWI_B@r0>b!q zZmSuGt?eF~73xjCX_?DmvOcV%rePx)?3mOx6B(H9wFR6hA{LoO8Hx2sA$y%KTX8++0?-l7tZ=N^;6hfbJSe(v0TTEg0o;UM-ILWm{Qqhe`fJ@137M+ z?cT4rPG}+SIrSLNYwW3%D+?^{A6I9C4=O}&lBKHlEqU->uW48W0+6tTnvmdzdyb@$ z?Buvj$9{OKiU+~ORsLpOc|t+J&fLII8sFguJcKnUjG?hZ|CqH&y!Vd{!Y>>n`@*!sD{LIrIO2lWssL1ZXI13CtegHx@W@#iwUrNF|M<`i#S$dTMzeHemDFjXx{|gp- ze&#JZH^cVV`trpCD$238{_lW4RGxlxMr!w|nwZM>E&bad?gv%T3$7^Ok2Ci!Bb|)j ziDEd1c@_?1Evx<{j_vQTSFCusCf$AfPD(ZGO#o5cEW{am-|+p>MG%~$VJZfKKJ5mn z6d_LV)9IY9C`fIbyFFo+*s`KI_9qJg2})<3T&?_Etzw3oR}#C5!7ZpORrIDfT<|?T zSlY_uYMZw%hL%*toh}5*94hhy<8TPZL(dYQ%*LcQ2o#mwqVAZG**kmcaW(GOW|#?F zIXb%83S9pE%1gH`i9CXoN_Uz`&~8&S02m3crW3zy50r+58L_IfM>rv?hfSEFxv9<| zGr8tYn9!G=ERYiSZ|tVrklRB-!UI{CD_rpo!p2B z&s>8Q{NuUM>Gu5)i)OwVxwOU8qr(~aqFeE7Kf|&^txb>@!A-OEf*g-rpuj?cj?NX{ zdQYhz7XCH8Mf5?1a6Ra7y!)!BqEmBu_3e6)4$~LzIgL@~bw?TEZ&N>R<%I8kzGwCq z<-q_vkiyyrC)+i%|E{y?#}Yi)Z=)`6NblA7tcBsJ!hw&o21bPaQP!t6r9^orND-_Z zMgByjpXn*;0(;({u496T@z{`}XS)WDo&wM@WUNnA-&`t|sT2R&M}OS(eNuYl%d%l} zNBDZmc(4=&M1*qlVr&58Q&Hz*AYeq6m(A(soAsS}#01;&QGL0y`xEf*>{3h4{3Et@ zg3wd?k%7#FDU3GurIz<}K7L>gmLn&FTOf|HCx(R7{gya^8K5b+XuJh}S$Y?(YFszH5g&Rh$*wzRBE z;WE3%r$p<54mUx|j&lB}+PtJC$vQd((lp6K`t()KPHO4Rn^MC;=U}tzpUj>oQHnK`QipR(r6C=9$ zTL4~Bi5$qS28}jU%&+9}m?AffiX*8K<2BcA9jP|m9*3Sv-}KwvS5|Pl{y`s_anAQc zxory(OZ(g{0ZW^DHYREK9m=IAuZ8-mY)$4TM0`rlF^DVBzt}Yq4~c_ntoN2 zP48p>?v_oAV;TCRr}cTNP*Np~UWF)T^IPf^o|g!2-pYy2PoKrRtA^xYra2c09AM~vC(YZ#9#k|-jcoe2KK0dOQRMtG;7cbwGZcgnnYi8v zN-5AXuu*qG?48{|CX&i6uKkSoEt74T5u$WNzxoMBEyrSU;IlD&ewKJ<8Gfo0CbVpD zIU7i20L5&aV1G-I(K9O@;3{yZgN@b3nbzkh**iThq@kXGG7R+Q2LC%c*p(iEkTlUs zn_<%`%Cs)e7zR9xuHKe7lPzG+14*@gQ4#iNyad(U|4ya6{xZh!0?;;eX$g|M)pfY& zM!n~c1W^5HpPbOV$6^N1ha50nqMk-Z58j2#Q`8*r+a!8Ei z(P8sE_jsU`EOEReaU1fzzuliITh-nF^74dlJf{#R{`u<`=~|$P;U-))b`8lpQUPW*%$Jqjn#8;~*NI-n&v-jXhlidsqOJ*ASpwsm{+R1!`#U~#{^SQ+rvN=uH>6k~#d9VrAl{zNphlcmhxD zSG>1bxo`B*4l+j_fF9@#7gCJ-J`derNA6mD6g(k(JY27O#=fq5lj6a|IEz~T^j zMTnrFoVUTWC8I(j=XfrUlE|ND%Bvm?~sBNWM_ z_8(4u_3D@bc8vg@(OT^kfUh$MD<^ezZfrGR`a5-&SX~VbHdq+G5QjiK^7EEbICwU) z)}oEg!?qCoLOWf7Y`xRNc~jjzx7AV#;&lhVoSMAP6}HCvd0S1+SA#wUb>WWitQTA( ziRtjFbz&9L!O-7f(WQWwe?OzxF{44q61IQd@fEBNG4re%b#ZLNeve!eYofTQ2p9VdHNk*c3P zI4o~sKZb-o7yW@vE1bri(Mh;6?s5~O4bP#UT@ZJ#pAcD{j7JB@6sF9*H(c!?s12!l zQ1BVtuvn0vYJ)|oc^JkW^DkPq&YUOwl$-hoYgy?_Eaj8xN~laZ83BfP#U2lMbXGBO zVV1emUrLtjnQU-tjT~q}Bq^^g(J((YMUG8hSp}jp8QY7jDpCjg5zWRv~_mF_BdEAenI-pZZFr93aAzZ`WkJA>EdHL@%-Aft>p5 z*nIPwQaj`d2F?awhBzf&E$FhE;2^>|-lQdZ@0wup!1F0}vOU1%!2XV0dkv453TEon zxbI|_za@c=7_N{p>V>X^6vq)sCMv7OY#T0hbV%E@8NFf#HZAp}VF|WcSMiBOTQ0YFBNk9GeB8(INYzaGnv>a2?sPDi%#(9RYcywu>s7|} zW8sK5=Q}+KV;K4YVuruKT<=J}E5bjvQJX6bo(yKzF8s|-uCew(wUt85vJlK+X)v1e zPfw+z$QNT>qZ1v#p&Dg|-%J`-N)$4Rzdpy@bpEUPOsgsDB(7ufG^p&LemTumQMuat z(q3`hD8TVI<)4PR$J9bA-k|4_!Xl%9tCT`%-pA#t@?Vu!cdD}?hL82`H{nLzb%wKG zcvWz->TI&%^FwW+4KHy#H*LekK8Q=gbr%lerESif%HyJK$~@IoDA}IB9D5X*%zOhNY+cKT6obw`_)Kf~C?Xs(gKIhZmmWZ*SxG^@oAhc55BT z^KpyelZ|+>OySc9q(|#yCE&dgv