From 3cfad6c692854d152b3bdf7ba93ab3aea524d84f Mon Sep 17 00:00:00 2001 From: Alan Jeffrey Date: Mon, 9 Oct 2023 16:42:44 -0500 Subject: [PATCH] Tidying up --- papers/incorrectness24/incorrectness24.pdf | Bin 405960 -> 405978 bytes papers/incorrectness24/incorrectness24.tex | 6 +++--- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/papers/incorrectness24/incorrectness24.pdf b/papers/incorrectness24/incorrectness24.pdf index 10d7fc78fcf5e01330f28094b323801e8177532e..006496d1257a318932f511cdbe650e411015e925 100644 GIT binary patch delta 16783 zcmaf(Q;aT5)TP_D?bEhx+c<68=G!(-+qP}nwr$(p^Zk>Vxt&T@@>FVHRCcOTt9JI- zA=btrR^1^V2rFl*Au0qVU|L%{?vm5VFIRt_2blRrOnZ{27?e!Vjmexbv!A5z>54at zMR2KQYXz@$tN!Tv#>UOhyF#-_bRyxJFCEOYo-8BPsQzs^M9l5cW6-YW{owUg|Ldmv z-^qwsi0RjfpL5}IOfor5QFpuku8*eAX4OmBplwf?U8-CCMMi}!z&=&Daacomdw!E} z@(wNr%bf&XZH4G+H3bMj_?OPhnC@C*!_8C^_%adr?)vORq;|kqxtvtJHKY5 zf?+o~hOqu)tca}P>R|d;pWWK)-TAu>T)1`r^7P^QrSwz4um7tH@R~Eo8&$jmsZ1*-OgGrX@$)penr5~$Dw6^qVC;8E zLGLr0g@$&Cz%6tc2_dul^2j{o-FDG1UA*G)0s!5Y2&mRu#QAaE<=Sbx?bF>kHA~3X z_{NwgIM8wdYN+*#i)sqcMIb)WJD0&32}?ttE-a3VrrO3MR>BH#(-`z1tX90KKbG3) zk`u<_zs-xVrCIijna7$J@KCA2CY{(W!aWA1!X+1Cv%PD&vz86HpY7a98UoD&KgFc6 zaoB&+V0D!`OU;MKk$N%QW(~U>w*9)c{L23|FOLKP3^1_zj3KsY1H>)6zanG}2#MD8 zd%3-UIjymhKfJ*DXmK<6@AszOTVPlLw`Yn{A--ineWrZOmXLTaa`{>5!ox=9=am~-{1)g5MOFzL9+>#d1-71$FE-U+9 zI94-P?V*qxIIa4Ek(rG6;Su}cN=Y?RT#_qo{fw$I7ty?9YsrJ{J7%1s;*V2VXDln= zfK~@nG97zX0IFy}ty{7biQTyFNQwd*`DsTeXaZDFI6kqkK`d(K+S!7IHZ=ZA9G%=4 z_!0Ergj`(b%}FuWnnL+zR!@Im6{tyd92z`{P+Py>kdHT;I-)OGy1QjCbknLz0 z(W}VY`vvG~X-IohO+gQxE%Rc}kn#)=`aNRoV!_tTikH&u-;XCh<*08OqMV7JMYd(Ssnj6=hCj=mPx8c8RJCx!V0AvXu^ z%4i88Qx<(y2%#|!-I7ZXG3O;tFIK^o)L?-1`P?Ca(H{GU!Xa^>-24kn#IzaUN_K!5 z57luS(W8H1cX=70PP*XEQ$b&1#=2l6-&7324n9wA8({`sKT=utS~~L3%q=sK*VvV_ zj+d!+dW6&ZRMMJiUUlS&&QU(Bs1@V7Binphlp$B)>FCK1l)QX#{$-a#bI6WV!HL8IbH64>XS)Z~8;r zc8(quo)K=p2$?klO?fBU5)eDRl+NJB&0zSw?B1J{LUqbCwmJ}NlGcV6#u{u z^AfN3GnIr^L*~DdB{B(W!dCkH{g0P;{L6@^Skxnm~d$TewI%ii%0E}VTw8} zFN|i72i0!bm@S(}O{Lvhpkluk&S_czyEhY#1p%kGBM{XHrTD^Cu}wrc8i{S3^%F8Q zBobDz@jxU}!x$Pzf8^S2#ql0ah^BbEw>5OL;!Vr5Rpv&)l99H6|M|WoOo2FgeImv` zt^vpyjQDMd49z*fhtxkTht<9GL^}lb-P{UdpQlpaMw?EN?hA3^l>RJd(i_AX(JUqT z!hik-{>!q%%s^wEH3H1#>Z7_6yR*mryyaWs~Ixe#BDA_7-gE60I8WNCj2 z=n7KNUTMt0RCcVbyOka`e+{~~$)DPVRV-e-H<0R8F5vr22}-VW^%HEYiSs-{?88(d z|A1jLn~fSi?s>WJVXV5sde6etZ*tXg5JR((ZF37$U`OJ zaHcwJn~gny>=a8hC=A$>x>vVCbdd|Wajfu%28Cy)ddEkMCe!r znoz3L%^=fVfw##ZX1 z;vTj?NctwYNQAan&l#6%S##9=kVv;)UNmmbI`5xayUbedf?{4C0*GG0$`RXcCP!f5 zHem3qrq06qm$1f@Qc=@^#8CUxkpv8K3jymui(`k9#1=9f%xN-U)TBb}Shqwr10t}m ztvGhTnEz9JF&?ltBWj7;Z1FZ3tp^^j`zbs56$PQ9k3^ilm-f7E*;B7425sR#-ZjA* z<1GOdSqOx5{@|C%?;<{8=3>(_)Mygk=eG)h0BdywjLvZTgk#cH$4o!{bnpQvRCb1Ez<7jVvWGRM zpd|D@s~+>pA2j6zQ=QGG_}$_o_iS7x(2O#r!%7Fq0A$K4DQ$$THam})_-7?TjeuY` zms870v_Bsqhk_P%W_1VBnrRvpLTMCC{`^0e2RjmBJQ$py59P2a*v1eH&v>N8{u2g( zy+1KGiTi*y&bo>I#Zybde*Ck5!C^n6J^w%g&OP5n!f?1gVEs{YVfeS7osj2`#+-OQ z!WH>VURe1PHiDj{wHfm3k7C6ZLA|}h)XHF4=w$4f#GPx;w?2f2~)J^ z1--TnicCmVjY&r~zJ{>XYjk-v}~@~@ZFe#>h(`a7%X_ScfC}Qe}8u_9nq#X?uUmr_X=^Y$6A200TJ~j-gM<|0V z3uhC*KNc}t)7#GiaI|QgC?*FW($O3zPBC@ytE~;gwH}vJuA`6^2jjuXhg>$gcgqwa zo5j^89{Y|a!Ectx*2XsP5w0MMwHp@gS&$2yo|%HHNVJ~pl&)W%;ZSaDki>^K0zrl` z?H>sA1_)d0B?hq+OtXi+Kxh>Y)ls0zxeO&Vv~>9I^9E+~C&h0lGPw=lL=Y2p3s`{N zZ7=#ySfNbPz+c=4_U-yqoLTHA(F=|LEtNN{L(2x*4n5?Cq@N5Q#LE(2BI_B~Yo`~()VKiCQFDg_Ci&Eeh6 z*Z1Wx>wI<~nim5S1y~4xS@J&+OUN39Q;XA%m;EK~_M`PVF_ixLODmq=xs%oaN^726-ULr~Gn$*D>CSM?;yE6g$2JhK=jDZZokri)Y=6 zBE8G|<#sQf--nxISrH&`jK~L|`~p|`daLs>(2SgnG^2&uxgyU(zoHSCSSuXhsFDGIPHfeWg37F!o%spE7AJx9ovI5GL5qUpJ=#TIa^JlmBfq9a6#g2>foU zxto9&Hq|d7+LwU$Pha)a=#qR81*9PIyVeufrf8mXZTuZ#yf` zBun{k&bVO})+7A^MsN1U@I56~&S~Lu6q5PFRZRKRhEnEqNC2zmV+GdqXnst-4>s&r z>t^fz+@lG=8yno`N&$s%qvj^IU(F3!0_B4$UwIu#bVrtsjgg*kMQLr^73{;aH+EOn zwNSUn=S*Cdj;W2^vlp5i6AiIWIOP1io{>kk*Y*hT)B>z=Z-%}6%y=4yrM{aT5uVe`$z-y z#(lyyk8r5{rM_YLOzOO1Zv?az=MlfhNNwdJ8*3h%2UJZWc;B{3KOk3wQB~KZ zEZd+A?>aL8+4zw1S|Q(v7NVy^^twIdU;~?-Lj1?Wy0QQHjZsV=VL;F4M3~MHb=vj` zdKk$({yhtH4*lnaqjkz0;b9mcvX1Z`xMgeX)3U4rz1LeXVGtbxg#PnR8~_1stYw`* zysT+R)dkk~z_M;z0o1Bk^lpDbwx51aODK0sK{8Q}O7g;GBHTi8(bq^ZQ;3@jOkw~p zWWBH{#;7GL=}s*lchJ-eRCG^tgsRnGhVc<9$&nV{ASwCrV3dT*j;@JD&B&OD{0}P;!5Ox3CXNvp^8YL)g2!|J zKNgSY{lDB85w8qP#>B$K#>L3SMaO2wVMfPl!o*3(#bIbl$I8U{-(Y6vU^8QG{7nFZ z17YF%-?g|zx?B_hi++Pp9^Ao7K6UYm{-s6>>4>&#N;6J(-|TK}WTG zmM;l(;9h^b-zgAT`j-6I(Iy20eQs8-k&c{;x`i-BDhKK~OZH^M2{lbyj*gzfjy%IG zS}wb}*GIih?(yQ~i_HjGdP+0jk521!OHT_XLkq6=LxUDzo9;BTy}N@Kb@*v?@P-QBbs9K=jjUSJ(VydzV9_1RUW zGb*=Nz}x+O8}*>%JdRPLpF&KXvc#b#WU44B5t|}?EIIpjOmOqsLRcJXA@x z^w*g$7{&{57Ok?oPqUj3#jThjMdy=hUIU9b`tL4f;I-_u??FGF;u1{^j$7u2C-opf_Wy;QZnN}JbpY2pDtG)YSEI)`VS!>pqN$+2{PfF?93HLeLP1EP|sI} zmXGJ0;h1&^*MtmLYfQ~mIMS0Xr@=w>d_jcjv?*z5??Tq+ut7PDOQA zByR5FAiURc7VF0Qe)2FbkZZt_4iuFRf^LLbT#c?@ozvwjLB8tn*a;1c@-Qy3=*pHK zXwC%?BWIw%RQS2!H7Nq-#BtKHOkkQB*%sfaJdSR}OUt*6>?A@S=6NW5{Jn{oUM1_*9}borFC0w%$^I;z#y|rgxFIXx2;@GgkDH@CPwi98LkzZkTIiLb zOf1Z&{bdPlnB7|@#859dcO=RzKsC zU{M0E|H|!*Czn1S>vHlTG}8rJ3c5VcO}Me{fVSWWXiQu64iusn6NdD>D$!yXdv5?_ zmxdPL;OXQby&9Aey-fkXQ+SB=7bUM9RzDlsR}|aXZ zp~;vS#b=Hv)m)OO*~OEcuw0PtjrRaD=un7>Ao34NSPT%11SM@ECk7-JLZ}gz(G&>~ zryxm)`%i5s(#e)NghMAFTX>v|g`r%(K5S$zSqgD^p^RY!lwqjB?~XOdC-XBSfLdB! z#NqC+!Xhk%fw(}K10e@0ar&f7l^FnQ^U7W^><@VH$^(meaQm~OD@CKQSv26tF5`lw z#Iv!wmR&6|i)=OB-~;VBsObH=gUWMFj>$m*3}^}24rU2qga?kt5Ka6%XyBO7;MBjL zNwv=tP3T|#`H;@jt)BzYj3v_vw+WW^AQ?xAxC$GDi))FA9~}2_`6_%9&1o*-G~~?p z+7(p218_NXn@`0sVbTJkNf7|#g>Wv-M|OkJaL4tdwTMI{WwqDFZUrL4<=$T~Hc1tq z-(e>BW{K}t(+vVW!316mTh=$4Nu*>h?)eNn2@l23wc#V;tmN%hNa4ngrnV3+hz*(P@7mmAPRID%Z_z^9Ivi z{&6{+RMFr5UHMKcWJ-X|EpO*M)7jhBQiOjhpB#)5BN=r@9to)Le{E`F$ zhYErwQD$Q|8nk(A@aAl;x!r=4D506xpN#&{gx5BT5wr{65ZlPqOgBh)xIkt_l_`n9 zazHB60!Qv!#~z^*P>&V1z{kMICH4{fMshcTYOJMDyAr3PS*$B76LYkBa^OroS` zuk?mEPbabzg!TwV%g(KCt$a22S9+X?;EgYfSWb)XO zckg2PS2EL-aq3D1yudb%*3$dROYP@%NGI=_8_N1J6$KqqxY#_y1(yIN-Pbd_X)kL$ z9!bl_pJxeB%KbW3Tm70X-FNXTkiU52Q%r?F(R{xKk^m?a9#KC6Hi4Gc5`fP5IIl?W zU=kN>UU-|xh?2^iNezIFKT*Y2^Pl6h1T3@+u>#XQ6qom$Ne0_+Dui?0I)Oe(yN#;m z@`})!gwVhZl7p71fi?edL^cAb^g!@RPy?EcJ}hW-;sS>ci%H^{%5T*``2yPK6En5> zt?a%8&jHS*WV2BR^F1aWNxGc5hZr}u>fV!X2Gi+#!zK_wu$5os4fs3-Hm}q6fBf`} z2?d)D&NitkWXrT#+#nFzaa%up+J)6g$B^6KTSgTO*XzFzlv5Gl-2Y*-7iSYD4W%$kW2jtk z5zz3sKv`V#@IQvMn<7%$^74cu7gPK?RvmS7!WePr)vChEc50PV49-zv_r2{&ux`EG zyarq#Ok)MuZ0J_Pjj911E+fNeWXbLy9ikb@lXcB*`ZF?G#}C@n;TU6r{!W>F&)F~z zo6qt7m=*DJ*ye=+K7fu0l z<7-LSqdEmF)+)4tV`CrNW66bInWoR$$9G%WKQlxxk_2gIz#MD=vV-y`qa!|W3X$h# zN_JoAOkTW~t9$zu&xE6>h(&Vd&H#>FyG`467yQ=SeW^<#C@0@@@wWQNa8`8SFLM+p zTPoxGmNPXn7MkD7hgB!t= zBHf@dE9`|AZ84IN{IM)h)O@_WfW3KxZ{C;QTqkfn;7eQScTy=fA7LT+l9 z>~o7M^K(R~aDM8d`FTo59l!?G%vu`czf`l%#!3|3!@j1j(|#OyOk(bR1E8IHhcJ%1 zY8|5sfAiI4hG3b@gF?aj)oGmlaPOjRJ>7HxX9N37kFDX&vG_(E|H)(~^x=Q1DVW%k zu3MMei}?)TT_HTz7Qo|iZdGq>Wi>!V^MP8w;S}ADgb93Mc!&vI7J#Nfhx{>@f2udz zy*Zeq7Qm|d0%&wV`Kl9;aL_*1f0j(?joerPe%oq;&&~jQ`5z3^QEJ zB-n}oI#(Bq4(^tBQUGbK(m~K7c~8Gu`@4<>lI%4#Ycp6_urBzfX)MS~2Xvq>gGeN1 z-{$S${7;;VinT1W_<|Q6Trdtyc?C&e>tKosoBCRjV8>61E(#T+AI~j}fnl&TQ{)Gkbr! zZkHbONd&z@!Su8u-Fy2rcydW^#XPQFPy9H?0t&?%EiZS&0nygi@Ru0I2^&IsA7*+j zG5SoGOYNDoz$8vGLB4X@&A3nxLY_o(uo=&lgIb859|RMszPfSXFjqCcZhm?##{vyz zzTSSPe-?5Wq$NuQ9ZL2;PV$6j$owGSh&vf~=B&tYEliM5zMedU?9bPp(EUIRK_4M>3iwBy z;10pN-643Vop_~Qk_98T+&cA#+Nx&6fKmn-#fr@iR!I@pX?=TqFIF(V<`{M7{Ue^$ z%idWNU{7sRTDTlH-qXC}R1B&zfFr$$y*Jk^S(|&eAsx-NUx@tJGX*zd4aCo;E zm2hG)AJse|`n^}|+r2+e7x z3bs%gFxl$T;`O$OgPy_X?bp)305T07_BLJH|GIXP8wrJuccZ0~1wkW_ZI)BDi5LH) zazLBO*_j~q(R=f+Cw9=#x3><$rVV~*48axXK-dim$8=ryqt#F|`}EIdLUU1))mL3r zyBkzSswf{9rZ`=W_CaxqXn>4DAot`M{&R@JL5?N!W9m2bHon@fo%UMCKG;Dj2cNWeVqP>NdNXD!tzt--2G}lq2UGYC9Dvm=4~O;(>11X0$6mfX=T4dUOq2d2ba3=HxDtVy(Z&cWmY>2Zdgw7_ybZH3 za(r%Y^paZlBL2FA2S{O^&h%^BcU1~IGx}y`PD|)7420Ga<6q3Nvgh^h&36IpR@eLm z2Ax19icz_aH2>Kn1HyK5cem;K13Qi}`i@`=pY7nY24w9paaGj&Q8!OPF5xs@zPQ?! z6o7hi*KcNRFMqMF8e42JGe>@rH>e6XQthuO5k;Iz$M3z0)%xC_&*$iFrP3%hJaBvl>VeZ1F}aeRPhWqk<4JS-7AK! zG9&ep?*@={u+#>OYo$HFE5N{}!S)Fdl5YC3hK(mLI}|EyCt+2J8ZR9dXn}5lx#1WI z{3wt8W3}!2o|a5q+K%=Twj8%qj_&~&LcGFbQL5UCYf#->lND!dn$&jSI zXhM_4F_fL40A$bzp74Zc5VFgZVKb=tnC>cK9YW(Zxm2O`sr$3Fctt>~QFFY1wF(z= z1+RvmPE#8>)E2RUuYLH_^5wYm;2|7luQZ{qX@_Ft?`DWSQQVQG2;xt_pZ&YB?$^M^ z#wndCfAH{I(f#BDnk-s<`Sa~1RUIC+CxBq;T~-j=**tkh}E<38Vmf3-o@FF%cT1+dgzjv0xy<>b_*C9;-QI zX7a^8e(E|RYUG%eZku^bsA%jt11jf9;2$6?GVJV7Va_j9&}^}%Ec^;kE1^c!*nxF%k|JbX!!q>zYGW2k0+a-WNzkKR?ncs<~p2C0%Emo%^^2ss|XOc8A^rXkylShY6Y)8#o zL~G4rV;}?9X2^47TXJu@)SUY)vS9(v&~0EFuD6!8p8Ylmr^$6Z?!wCSvejxY0kwld zz8@#WWjm4YPbD{VnssMt<{X%hPQQx|Pwg7rcnS=cmigkoWj}wrtM#%kokSiWogHI= zg8ozw8nw>wQ9)< z!m6R*LLdMBxGeT^5g?FLS!U5l0*b=@Rb}F^Y#A_052G&cTMzf+4Zo0wwDHGbMR^xU z5yV*OkOy|gqYwA}_w>Xe&R3*x|G^az(SfiXMn92Xj~x7uYZvflxzV4ErNOU_iLMyB zXC@_o!l4ebnAZxYINrv}-iE8|H`ny#?BFKgXE(*J+s&Rpab#%HU@me6a7!`Ta&Xs% zeP0Uvs3^pROZgZ4J#h*BME6a|NLN)|uWBAipEn*NqC22yc zyN1dcKQN054@#(d>BM>mfbw!g{kPga48KJB_A)|w;vPleK$Oo((9rX7e2dwuRFL&` zjagJwDIuUR8q|n05K80iOH%Rr+{zVT5UL-6*xl))`;gf~zwZ6sQS2UN>Oaojxulqb zlaZ+9ZW8AzrD_;PJ1)X-Nn9J^ptH;F0tl!bgTm8#|7H zfn~(Brh&x9HVzI5qr=lfD3xnl?B#FyCRR_!Zd71iM8Ib7Yyw_R{Gb=Ox6{<09U;wj z<|kpNnt&P>G|z8A$PZGHH(@Yrbw7MK5q&qe&$C&5-kkU0?&+f1;wI5!o#b^7H;_L_ zkC6=@ec69D{+>?*n43SR{#fwiu~yniB9fD~2ho~9!ij?*403fNPKgBrfA&X5IEdWH z*M)GgP)QL?c7z$-rUOc&K3{i?IHHvn)~mVl;{QaI9x80?u32CG+GOkLbF zraI;RyiAu=A9=0>MVs2y&BE{SQrLKHzm#0tZg#f3+7fO6_*;Bg@Z%seKi%}UXRHY< z0UW}HgeFIxRKf=&`~FG(ty(y)5>?L~IqDj@TH@0Q*;l&V1;X3Bb+&SGN59t za{`!)xdb0V`F|8R>vz%H52{q7F?eYmq!A-q2_}g|&+DA9iJ8zMzs7SY=JpiA-8st$ zV|-V7JFWy2j=h3rmxV{JKluM!%|9g2j}<%@#wLRchl9ay(> z5*iP%#ZTW%-FS$w9Bc;^Zy0LNrM+;yB)ZDLRz{6}U@G;mS;rE^WT-avqdQaagdTao zBfEqeMNb+|f0;i41Ahyn%bRMNLe>Y0Wza$EhK5EzG`+dX>(Dg>i(?%$?^E!1%!Jt1>a z`p89Y_=kUi#Sun09-L{Mlqbl}8j8z7G6W}*KbNw*u2mf;-nK-qwoI|txN z$f{#4ssV3WoB~r}Fa%Fzn*NAX`R9L>dsXpPl zaInV)FYqZxo3FV%-SnWx3@95PdIyNdQ84?;djdoas97sS^+6ByDWqBD`#@GS#(CH{ z*1muO1Kcf;N$E6O(2>*+yrVi~cxJeD3?1G|VhQA2CH1C@8rT19QOV$r(-9jk1w8u>Z1FnZ8KllnRdKS*cGc)pea-uXWQ*LT0OlE7GlSyVBHxc=JGyW-ZAn|E9iLe4-dO zIIEF$+8B38(pr$WS$@t~0cPSV=APbbm`_sV9LGy$8`p*BA-GU+GRR)-1uMn|rs66W zh!m|}0R>L0uOVK{g|^N3xk#E;fpr=nN}ZY$8ayxU&nEwblb#}Rj|WcUf6Ny3t2%k^fUMwcmDT_Kw8+FEzJsRWfb! z@LeZ*H>hsB+#l8OiPjzBq=D^XcmGbBodEh=v9cNbB^X}a;}Z8gbAz=8ieST-OJ9*R z*=|i(Lzq@9w>!^Ko+~I@BOeEVg^24Klx?5840iLh%A^kI>6r(XU4b3$9el-IXif|P zgXONr!;;s-%4N;u#8C+o+=E_o4)6AEB1gdS!dsHBxwb;=32L=CrPyXtrc5-Y0aczH zgimV|SrU4bsTOs%C9Pzb-N#aw2sYCy)bXc!IZ0?1W2(^~cn8V)CwwhVN4`)%3H&u4 zY}IDB{9nwkpkx|1kbI(7o^AnCDXlu9RkP6H{57zRXU!hq3KUk@j>$8*mQnW+~7WMML z0TXRdj0KS^x?_XpBl)u^%0z-r0HBsK0YY2T_XO$nDQJW2lSTQ%dUJ(mM@XsTofg1! zcPweB6mE+}Zi!gnE5!QPCmyZ@okx*zh>12oun5N4JV(5rb_(l1!g~(Paw1hMPNYN= zgImyyczk7QkZ&Qz7zhO4-PTYGg7UVOAf%I56%ABzA-EqX^!flD)<7@>0RX|&iTgoH zxn9tLDSC_h*k4gym^n>pb9(AmfihxyQ(LgImqV=J{fBV$*8#=f82BbQw52Y!X>G7h zr;u*;pRI&#y+5miPE8{mOPmNNXzvySKom;IU@jJA_PZ|-MKgSuA4to;t_;x`$|Dj? z3+4%CO%ABes1AacG6OgY4CMxCsSf7fxsOe-9PS}fKdT|JXPYZI2jh{@dbyV`x!(3&vjbI_Cvn9UwR&g*<(5UunY4 z0>&^4%km2+fjeL66~n+Lx+T8ePBn(=CCYF{firK>!>C2@2Nmb|kdyvkeQ3_w3*YpK zJ8Hzt%r5eRy3yz?Ep|~WWAD|6U>=%n>8m~3>?w3-NB}N-!P2Z?z~m`qXNSQ~PT2S( zd*&>QoV6IXBb+%g2_QUKDNRW{^9X~XhU_hilLPwlYBV2gCl`ZB!Ysdn~)-P6`{CP zxT`K_U%1hK8>Vq;pZB)`v$T;@Ylb28*+|a-y|FyUGE*}IwH%`YwS2)9)GpgdQ)pI6 z(LtkM!zJ#96riVYhWnAyQ%HF3iQSodj(+g!MM*MADJ1GwS@=M%YX&7pLH64TGXW+p zYEtsnZ2@k?vGVX1d(ueRE4GBbd*_^qEfSSWWppQj9`eMHSZoU$ys5c&HkgWtiMawo z^SfaKQci=)sQLzpYZ2FMyVq(%v|>8xP@Sm8&Y2fh2N-1X?QR&R;w!v8ha4qOeUh<6 z&t&e+G)m@oMmM| zu)>cf;7SdqSI0&W)K?=IGlrof)DHS}sA2PVYyklGH|Oc^o{r7!T7nX|8}e=2G+@_y z{m(OXGUYy^m5eN&JL=|@3$H(KllBtk3Q?V&06blI>mc}i_`fuGhjU}rCo8J)j@_c_;>2kTk)L>&j)7|J*qBTOhAHxgj;t~ZMx6ba zfJxf%`B9DP&x;zb2zn~Hze5!PUq0celVtKGio8ATOh|m}T<<~U@M1wwy~}-vE^_6-RqI>c=1^WgmS?xhw{RUctt-ayVp5t~+H;A#%t} zUuvE2z}c{0qB2nb!B&NJi+Z+E9ay^ze*Q)rf7n_n>_v#*_hWMJ;X<$~}J?WUw|6GuL3k#owGC_;c01^oM z*}3ZxR-bAmytFjE){VC+^TQ=)nS)K#77l~an<%6aE8}L`3V&DP&0IyI>qo6eRo~|D z1?(aiI{$`U`V>@qVso$E)*%oSG_!S7I^-GN|C(R9)Yl;Kzn!i6y^B0+>0usM`-Y#` zFigbwHtr9KSK6fHTG)c;NjRop0$Qw)V@F}`4-qD zj_Fl*Labui1F3Z!gw}7c`#mR=8^aq4qWgad=lJy05G!B&`XM_gI_bysq>UOv z8qigJwXIwDN&p`s!W`Bgzeq9@`|+}%4Od*b;4y^Q}iEb5BiMO zpQ3BSi?HYF;BX*eb-=u!0Q5T%R<<<@0bL_^C~sT^n|KCaw9#ZIgDRahs>|C{aOyZ+ zodV+KLT%QfpGk2#^;(RPGkz)K7mXt5Bg7V0`iWjK_1E-wAyFRx%3{67rijY@VpnD! z7Izw2Ixaal;n+2@FfOOiJ665-NY-N~MFi)2sP)vvCh&ixn@&ZffKWt>0SyzU7Qa8R z_&_>{;abR(PkCup$3Q?W1qrqV3C(3DvADH;$vKOxcFCt#kuzpAJsk7Z+0|=6n=}pI zhQ!MQ>g@Ho)<~EN2n+W&p2()d2<1lcyx5~5o-OWAp^c}bmaLPzbcO$A--OM6*WsQw zL%u*4_xbRa=SA=q&=W`DsP4-iVHQq*)QXSNf$|URz|x5`>h=JxlE#_s_Q1j|P6d@+ zO)YD|{hpVe+k+>u*G-K^pODb=;hkwMEj_VlY+<}X6r6Qp{XV9B|LeUyT|x>uuF^!^ zaAk%T30Sh=dq{aOOQKBQ+|nu5_^j>CqbaVnCcJTN>Vee|V2CB$c4gIy?W8|cH$%91 zspS=xts9iXFv@vz6vNb1wX;36Xlj-dQy8*+m<~kE^fuDUUZbW(G|F$xBN{rxw@Vy= zqgvL#ICYs%pKENb>n-#>d@bOHxa=8hn{>vTh@m~_S>_f#t36xAdE!dUp2^eb1(d0= zmi2C%u1U24sH0OWV1b1a19kB1M$sU_@rsS%yd`l}bTNNL?z|0%U**MUC7+)9O0Uxn ztNKJL82stM*Q$Q6%&rukv>G*1J4^W`Q;8AcQ|CAS6)_XBK)mtK3W#{oxAIa05LU0# zX2(`MC|vaTsV!uyYCahM;+D=NsW?aK1^P|Mv84O)#ZD_E5Ch2;Y!b z#-?VJwM|OO^T%Hjm!wk+`Cjsfx0-`7UIJMB+c3b#%Nq$(=BWx3S!zkVm;=TvXBuw; zW*;!M+LX+m1K+m$e*CM1XcMS+7BoGFsBHj*!+7w&0xSX3{#JXZVOwd+h)@HyXD&g5 zpkFX7=n@ULiPsu-4(`BRxCK|>Cd|VeXgjsfyI~LPg~KrFHu+8c_R*dd1#1h|8{ND( z2u(N-f7jtQ%)$*g0!QH(9ETHd5+-00PQesR!wj5pn`_q$?!ma*Qo&=eb)j9m0GHq@ zT!Yha7Vg6XeyoFf2n+Ctn$G+&Nmt+rJmpa*{fwk5@SLO@u}I3~g;2UyZG8+jh5hx3=4__SUv-V{6;CZTtS0uXi$M=46tWJY*)5oU9+< zj2__B9q@y(u%x2mf>HsebZuh~B%Hpl4VX_r>W`WBpJ+36i9wy9YxklYVRrA{25JHv z$gRX`Lo>n`r{ow;c5*6euFW~cWjg+%A5O&CJXyOwsVZVd4cHOduTF6qe13mN?Q~%` z{A1SsgVWQ#vuWvSVw#gYzqwg!FF@CAtNAgo*P^x9D%+^_WV;1)ZI#Vm+o#RHKD~}r z_pU-}m94?HS0mMWz3cSt+-|+z3j>DG(vBP7=`}jL0%N;w?5FmJR^C(HuKc`#mghA{ zN1YX}WXnY9No@3u9?m_QR~dHSn|yXg1v)>E&QES13tvP%hIU&$-ZMtoW*Wz&BjOLy zj^I6Y_;!%J+QUF45Jh7Dih+_@5llyTP2LsU1+(@2^7B^hr&(Xq4BvL!?qFJX-^rNq z;&D0cA_AiUgyp=){hd&H%Z~L(g>v!6nvL$Yf9zLe>b!srvmL&rM`v43J766xjA|(N zp;>&r$Sl?0jTw_pH}I;;Fg@Riwf-^JM!{J`xQ}KpuWjJc4VtHflYCLI`@Q*?dPxYW zuN6nD?9{3;q*VY|Lw`NRSBu@1n60cVl$s;bIY#SsDt@ zgbYe!VsNl$M5gXpG`#fu>s?E)>-temMa$NU%MZx8ykMEr9Kn{`F5_3r`B!%8kyUJh zZYSPM(H>CCNq4D6MqE#vHx$f`*R4_(MSubEq_QwOk>$Ws*x8qBJ>YHMEN#k5Q9Spz zchNkx6UGm&ZRkA0VH$!{HOB}#W}sOJo~u~HUXfVQpOJ0-6@?kRo-FfLUS;h**1j#u zVz8$$piFQ}*~S7p8hV)lbm?*Pu6#YoFP%( zszJ~C8<+zJ6V1~TjK6kslTSil`rU>(C)u4bN*sflMv{Wi4nZYZ(~;BMf%f(3_BoU$ zyowbSOhbbrqX)>9o_K00REbSKBwqYv?o}}I7ygo^?#vS0V}~=mw3~vtrB)NFsS2Q~ z-VfL*D8S=WliP2V|Ar^wBH{(MdQ90%oaEEf1LqDR7BUnBrsqk*ZYOf0l&a4-~r(d4V z5#1SnRm(I0)E;l;VqqH;OW-m?aXHX|X#nVtaK%&yp5;*jST@{*m1susGmi~BKN}+? z9!uahReQV&wF0kF*}R{r&}zCbcmd$Rr|O%|2s(-D>KH-ej5V=7G=+FB?gW zUh)^WBA~Y$h|ScX&dQ47G)8mgJ8;)^#y_p@*(iPlCr!XmPU{VXMvxkpWa%jsIVUpun6l~`v99i3@ByF2> z^EPs~RBoTM6Q0TMPO#E>ZV$@;W@ghc$>dbM;x0E&uu{;=LH0jhZZc_ISkyHrIF3Jx zue*!>`DuzL11ifrf{~GxI{~vYBB}{65GR|6W#btA^{c0UbLGT#P1d%at^>>jOrj=H9!qh@ z1p4MFEUDjAaECGco*R7(Z-Ce!HpVv3TiC5OHHpfQy%2=YL+ejGA+kpV&6|eqCT^~8 z?5A}&n@_EV3F90g;MWvudTBdb1x#zk2QF!z>2k7q@fh;4 zF&R$yP!+h5z?>jxPXYzpxza{G@)rb8Gb5|3-`K|f7K=#|kCmWnMM$+8fyR$GmYq$rgr+Xs-v0fn(jJZ0lb`aI`g zU(yERMsF5!uYB#NLX-)ilgsdrpyF`W;XfE? zCGyHUP#kBXxRkm^BGHrgP+ z5M-cwcH>cuV-QY9D;7v4c-Y#P8n=P7gJY6wzgHzm_tG4V#=L5yBSDkBTHVeo4U&JJ z!!WMJs1}F}zx4Mo`>ahc-gqXLk+j(S=~lb)Jzt`ONFtPlNP-bDhzIz3N|W`bf>O9h z+gG@LWpECz;q#IEfi7;;7sJJK z?^y`l+AE+f2~zXTSK#11BiW{Wc%R+K^Ls-{2FSN~5t4qFWlDLOVxn@>qJHRn|n>VHf^E8(xg1FI{0h!AjSZ3=E4( zk`_R~n;1mkRyy573IlE0yAU2%5^h+1w|Lg>k`WAQJOlsXMgDR!HgvT;ca$nLb{QZ8 z1ZHCQu|)cSFVztoyrrYDNKqljR~TIXnrazMO6iU{A$)b(tGq3!)YI0wBx_f%Eqn>3 zc4&Sw2^oz?WgRN8-?-4HVsM3;q}JaO3qO3)jXrGLJ$Yi?Ve@iL+FYFu_%;){0}WPK zOTu>QH$W>r1%sg`VIh+=(Gww|&>n7<2I9A?%0QiNhU3kO{lzl~5ru0@Ve(veiW_tt zutqS9eQ$#!Z_0L$Z;?|bwE=`hV7(z|=)%H3NG#DlkVDN50QLAjPFIHEQiJ@?6U;nw zkf(RKg=IjK1KueAUMKDW+qmjzdh?I}5aqZ+@79r|;Be&;gFtWE_j`whcVR`D0P*vo z_<;6>7JJF#qwUY$rSkEf2G@9!zh!JJ65Nbvlc<%kJl>9IC{#tvxKE_*$&s7uHtz&u zrVJ|dww~1_`Y05Mmt4DhhPATfpt)Oe*S}N_YUH1Qnr;#~hEa7bqorIJN_c z5nXz^5kO~DIe77yd(}(#A*(gIoMPYe)1YwcaPoAE;8x6>@Gs zQ1Ej{Di%8nJ43)UTg7zm6&xCr!2uSm5qWUx@wPYLMl<8G9>5PLf_zK&2$Pdf+}k)x zz$a=1F>@Pi|A3qwwID8qNZ;M_m?K&sSulY=)K)x9ws_Pez)&NucL^nvcul1p^7e?G z>VS5@*b2*aQWitq2>6UF0`9O%;Wr|>)qW9xElOcc8godo*J6e<+L9_6&)>V+~X_q~m_fedKCQyi-eB#y#P)R zOqus=XcH1N0GF~=M0=k0%KyA{ejRL(XGNgFq}|?uriMPvR%MSgb_vyUAIOpD|y-I=x?vjk; zi2{NHdEu@PI8!w&JSd-b8o8n|O}s=m_ghsGLtz64bx&Z)R^3T`VCwbswO~YTVgn32koWktnCJRa9Rybw5ekrjk#<5v|+}(F6v(hPPd-9Ob=_Pm08& zP`yXDlh@ko_E**;+wH7W-(Rp}x~L)h&<-Zdpf@b0O297IExx5BVa(qw0ghdoZMwn? z1H~~gHAk)@M~z9bRG}6zT(-T7@-5J3jSBcqAXx~`w2wz+W@#d$$LTR&jbfcg9k2G8 z^45CU7Q?%nJdKd6BjM74K72f;p-!Rxj0sN$=yW2~L-=$UD|66kLN4UvD%tUBZY1=x z4hWw~B)sf+HQxEi8zcGyrjTc7syJ)3)`J21{J|3_8nd!~kAR^TUyW^-#|P#<0yjPY z_%=U0T+os#qzA@y6hX(C3Zv2#(ENl4~LhqlQ#H;3mZxSv_ryJ zztebXM08hybaB1@Ba3sCWJv8tu(FRW&jH5j!s!(eXwiI^i;xBP`(Q-NXS^OUSKuIQ zj%Pmcu`vZX>j&d#c|Poyt?xP;{M=ha8;T$0cv}o+iy=pyq&o%?gVyJG@ov=lo99Z^ zW#v!fXyO4jktfeM!o5@pqpB<`P^lT1#?fTSrBHU{lLa+hxopPMS3QLm!v4aDp*{HF zdd0$=y6{1Lr%D~B>)HuNG=DjA_WR7-{_{>o6K;XUSPo`h9YecsGA)pT67SRT!iq6K zo`(5$^oKqY%)jz4q2eF8uQzoW+W~sykOkwt9DZ<023u%9@;!4~qk#T?*&-h8n_3`cX(1=cXL6;xT zK+m{roC&^Em<&Ky%#!5vgAVs+ho~O2OU-FG6xb@~^TjOPa_7J^2=*bR%$yO~K{Plkk!bD@1;sq=FmsZux<6{SRCbM*j_)(0YrhHd*&DK!V)o}K|DovpK z#GCnb4Z}=ux?cxxW_fv!^IiGcq^1Kybkf4gl6u$h^vUX>mFg6};5d-!ZZX?eQ%#51 zP~zw@v2#G`hlVxFb@Q7XlpTvc>l~!k0p0%VSHFX_C)*qwM|ajtEwk+bGBY zp8$&IRH49}~>owPgXtY6Pf-%R3!ay;?mT zUh%TDhlcIQ!^GwNBC=gr3I@XE{E3v)S76Bb-0~ik0ezYn&Zk#Gb3ZU-A*o4H^EWjbF%}(sn={uw zLx9tZi$E9Fu$}s>ECGGiCRO#6A(0e*4f3DTzz8@CeZ%T2Go9&P-YuWkwN4Y+otkWW zLFru*Wr6qZ|8m;o4f+vj=Q3*Am6VLa-EHTv8Ei>PjHY29D<4H5o&YZ?!s(3=4TaEi zOdbGblgc3mnIl}x#@W79#CMAqvjO;Lr2~p1V^oHQ%f|Vk2!LXrIIr`7;4o>>UtSo) zBbKuM`d4w>SyJD55rb^Q=+Z&XpyOc$uvDng5GU91x7d_qoEI?Kk6S0p!$GOZ?nYOOY)E9^3?c)%trDa6qQ}!$JV*_@P0p6q_c`**E zd2X{iMys%0Ofp0m3^$;>&u>u;#t|VW*bi(W4+ERS&cHJ^@%nBagGRH$tgp zf&mSeS3tkCzawWUlWcU? zoaD}2JHAnEASU@E(wMX@^4{y+xTBZWQ&EYS0=xh|z`sqES~aF|78}I&fF9KUy7_`z zg8m_P_!pD~VEUt_#%EQ0$xM4i4T(buK^3F4_89}+GtqZ{GTqSehnO<9PAGtu^}Y$v zHi8wjgV+$$$lOd{$Uj^xy{N(w4=^8;OtHb0dpER2YX|dXMk)vO_1^&;Vi%zISFF+{ z04Y2({-9Q=v&5fAgowB7`z9t)F>su`Ak4E0&-``K5im<>sb~EHo?n-WXQ-(GYMSX6A9T@2 z1_)=nudoC<{NVXVAmguExSiCMm7Y!%!=^G1(8Xs4HR@M8(L6aT7pBHND~|oqK&hU2 zAS0F2J)2-YQ5zx?kq#P27j&2}guao=`czI>3WS)Q^%aa(@9MYMoU5g;*aI{@ErKW$ zI&uY`kAf+V=D=pzf*rOYut+l+6E7(#kORg9q!Li20ozNnPBZ;o>;dbLrU0=Vc~)5M zzz>HNn;I!LT-2e7_y}<ury%d8)wLxafE;2sO&Q1tvi$LZyy?wxY0V}{%+)+?A6S-<==5!d{YFjv&z-+)1j+uSlApDhM zrl-51=umT&%1xl=caG<$JEFQ4QqYC9?|f{Y7By7@69_qF8w@WGCy_XQ_glhJ zu)Uj&WGwe&tw6zJ=BwZG(M~S;Xzy1|O&fj(rxSEA!HU>lo-kpe4%}xfMRc;eT;56^ZrQ&>NfiB*l4<24#Su(T=UG-?EnmY{DS+_6RER&vP32$f?quG zQJ~D}*(RYXneCWwXKa>{r=V1Qpr#HCB=9^en^)`yTkGMqK=mB=yz1^QoQzgRocL{H zLwI$UD%JJcA3W9V?XkPpT(xUIsiAUpUG4oKhL9#7%U`oALq5{pgP>i)BnLVBPzni2A1!?7 zCvElC+H@2=mpPw+UQ2$M*MwEAOE#)C>+DA<7%z3|{Z0!A$vA?eB<-ygSUg@3uI)mn zhfD1+D6CfAY-8c_N&W}PMt=#9Ol@hHqA1(_saXejICZ@mdbCq|k_jifj&A65V}k>< z3F}l)rC2xR{Hm@}ZwKW#ql_1Fw4+8E{Xhw8GM*<3K3$~5)DcyU|{Qu7W zfeWWF`XX~Gz{gXf8v>~r<02}hDFNWLvmS<40 zUyGa$4iFy$MIarS+^Epss;kD>*3Kvw-_iJpK03U3n{acUb_IJZ?ia309oj|RYkaP) zVHNfpj|nY6+karqK5+EN&g6S@{t6SRg&Xt;j8IZ%B)MRxUdTYn?5BrSL4hOgHVA^Q zmqo-rGpCloa4rT51Phxf@KM>utqt`6KS#sg z)hB&mh}a}-dxjv@CVPZ7yIsZ+p5QrpsXZtRdVaBBLmHgcgQVZd=H9Mmz=?qB?1MXO zdosr9CJ-R43C(1jT8aE{Q>0FpH_u}+NQ*-z0ejpV)l6h;)IHoRD*NP{Bp+_u9e=|~ z+^#S%6#K~yhc-S8@w2vW)SNvRCPU(4G;G-5rr2z2BHch)F;8j<)6rC@{P zIe8PrEpv`vl;+?!(ctl`{IZGRgOFaDk)b4C%IyNlXdcfD1bTJQOO8pW9p}INbdQ}Y zS6gUD2n`%4C>GZ@*=&W2vcS#QC_P_1J9kGfx?4Hurmk-^lAlr~0@!0EtTExFWAbzbpl>B?*yy^Y^x(YzP-$53~C|ibhbz$kd)L1WD>nyzr7tjlOh$YYf zh6f-FQ&x24(4RXHnPDf$&^?g|QTe=wd?nlZ9Y1X40kn0!!#A)TI?87{MULfPz{$JO zA$}jT_QD4d_m&gk&VVG-wQ5}rMNI)bVx;Ev={~ne&OB;)3%VSpdl!;;hxFhAVw<1C zd^tOtwcK^Ve9r&E&1Lj>As5&_8(Gf+r=lC}oP5$U~G{~;Ptvh`on4Yankwzog#B)kHtTGMVp?Ngka&8y>ss~3Lv$IvU2IT>d;=kK3zM3PJ&qnmUA}i zO=SBw`*<(C?L%or=5eXr>DcmH45_Z?oAN0jsOxjPp?}8B!G#5=kRiN;8~y%pU63g5 zkhW47>=*}tbz0|S=VHs>#a8L> zikH~l`u4h*E2KCr?>u9}R_K1H{{E1|8{LqxHo9#&;fAK~aghS`Iu}ZScor>UB#Gm^ zUeA0-Vsy;($+UIbrKobf`iL-5QOhvpzrPfB)=Sm6yPM#mr{HE>{?Yl4WCg1eVVZ*` zkYB?)qD%aOmi_PG`G(twZ5^$T(YgEjey%_>tP|IS?;!pyg|2>{ko^<*S=smBv;| zgjSr96Qelgm|-CJn41+`4f9MqwFAa>&h|K&kN#_5Gl_$yfjw;$E+E*-0v_4#5wRN@ zm9e7WO{;2rvKf@ugv!#SgmL_W8r64Zrq`hRQ)gW$ z9-O{pc&E}1xY7SQwETs&w5A++MmmFWb&k{UWnJ+&a$+6l(3w4WO4zlRg_`l^wkg;_ zYsb%lEXNd9MKBu0XWC6m^ucV%#t8G-)^dsy*RFQbPqcB79cNPVElrDsg14T)PQD_p zL?7zRO0lxjZ3>nFnq>OR56}MyD|M+*#tNoyD%bAuk9`&#G8w3ewu*P22Jql?nW2vhPD4L z<#7_n7oihQ9y@CN_2l1$bGHgHI!5(C^$j3s%^u&2Mv6KJiVi@U;IX$rtK0=z$ThM4 z)Mqhfws@`8pVfY!;WN_ijPDc=r?C+pYS}A&bPpqIaP`zzI!_CCN<#ZYCG5pO)Bd`x zac_&lZL~f}73(b*N}(kCCsbZ1GwjZfax05`OJH`;7fq9rUsi3?u^TBYlc^EQ6x-|t zf#HeZuNW2?{1T&FRMQgN3&jK!5fdSL-RSqP3kgvEdzKW_fo%9EM%=E}#h#kTeRvL^ zg!YzJbOsK#%7c|rbI4Yk`-1uE9GdN2%g5=L?@@spe&63Mo8uXdr>o7H;Emq2ilX2M zm@zHF1-IGNGE>~r0``_ludDt8lx0fJBB1lzp+O?m3E+QkTb;~|5+h;Z5?Pykz)u58 z8XKD6L4lB1LFIY;37vRi*o(r|;3U7b7)!x!0s?e zi%3O!ovVA3Pun?GlbFMxp5x_WWW);P8Fd~Z!2nc;O2-(@$FVR4x1mAPVqrkzyvFdH zMp4&-u*W>rxuAhKZ3HAhuNo*sLOJSXga={15b#sc2iCe|7eYS*m&!OkjYO%A*xVtc zBLib;L`Y7lJ||S4(u8aOZXjVeoJft^fe9Bz(u7U?oU?9bmd=X8VL@oktARyHc}x!; zp$yJ2d!p-PM%kJf+D9q6&1?T1I^%@B+OM+sXZDKGc9yp4@T|R9KR>V@3EFjW%uFE6gx5e+CwzE4yPi87etj<-18TWCXoO6 z9GEp^b?M9aw)A};t?oZnQiy-m1Xh{qFv2mWUf55kHZn*EB#O3H0R8&Las_YHZ+_Ai z3*Os->Ms?V2Xp@jr!2q}F#NmDn{xizmjrnYj}}CKR(AuQ4PtsCoI?Wg&Xy;|k`M+ZVGHw}UX0oBOqQKP#l?CnOBUoUGNw7Qt$B7_5Qnk50&Rs`vO9Syw-rAM z*Mi}ZzfqPd8_!+8fUaC+iaY->mUNhNw-*WU;IX>SFOLWQZT_$Ue6Q6RM;0c$ewQg@ zFBw#}E>$|~*-3pHGEAf9Nl)Q0YvZEglL{qZbuXL$YM$};CgCXN0u|iQdlLfeeyuo! zYyWNoUNniNCL`=7KFN@Jtw#15a@8Iwa(-nV>=`B`47Uf00V83gnjgc@pN$=Pz8(0# z-T3%eq6I}LAQBHDNeRzT!$>nyV2o}|hwmJOU?|CgTrP^l+e%gAu#EB@CA<>dOz!Rv zB@1)Aa9?UIMv`MzBqY@LJ@?}2YLJrj5^d=k7+ivh79=)B3mt12>PwKLdH34*x2$(M z(r&*t1_`+nIf5U1^F?iaYH*2?-V ztWbC}8niyz)gv&inWy57tBN|aT*O?~Gepo_#!;-FlDC-^rmoM4dZur>T|78?xUyCs z0dZm*dg{VV1BaN``oUPshr0vI%B2}zd2RM?ow#iKv%jC}uaN7<`S9+f&DTi| zC}KJCyi|6Mer+ROT&#H%#a9!dW@4BH|JV3RI$^VY)H!HUt5;iX|G1UE*YK$}T)*7d za$^|n;aX$Dv8Nhf2PbYlWN_0_Vy^}+M&1jVfiu(Rj9+s;T$UPJafEUbPSDz;NI20D zfKX>IqO>R&@aG_0^u5r{Y(scwbCrbgwE;u^aA6=y6=;QDX*yeqSN)P)&E-xgySN;U z%I{6$90gC$L=+;s<`UY%&IQwLTbg=%4qJ+uMnY3M=OACZ+hcB{g^LzWTlqF4|_pAb4C#_Z5z>4@JjRD^F){a*4BEN9z*L*D>I>0_S%MLmK@ z8WL+ND!Qs%x-sp@#I4dD67o}F{mi?jO6pgsuKn#BGma}iS5@jhA*e;2@LnrH?A{*c zrQ7$U;L^dLFY)!~TSt7f&euFmNAMJOJWx@IPmq&S!@KBXNf0g8_ra7H5s4?`c*h

&NvC6&Ag(+xm9AJ4(yc2)d zb!<(AYrX)EYH0vo0aGx}BlC8CYz;Y%%-M&D7dIi6ofU+V14G5RA`sV4yt@c&anSq= zro{M$d!klGni9t(wkw^i=T-|t zFUEEcQ7Jb1uJ^` z@ZbYf3&3IDzsrQ(t71dCN8)1$kPqGTjr;+R21MH*N^+4Gr*PX$kRjet<`M=gH0b|jR=-ZKp>)Jnky2L5L<8s*xgH4(ad7=+DeGX*gbYppJqu}N z#u3;{6Ssgrz*rN_r1T6_E}uZ@UWK=}fz6u4kk{d-N34nyzoTE3Xxn6p*Fw~@dl zBqnaopg}K!Z>0#h8qMjNJFp>QO|(Y$Nviq_^8Gyxa)s z=g-B{yk9#&#K1J3=xji(;$|sSFl;&jt#M758ce;dm8}RgjDDr z>fFaoehm53#tTxa=1D5)hd{B_;R3W|Lx{J^z)tcDU@OqI(GS^V6J&_A+KWVtjHrUG z;z?w3R~_te$o#^YRIbVxDr~v~_nv{nJx@DZ@jtDCU2{zmdM!~aS1oIEXq?tD1?=N5R=B@M zTiRA4L(In6I!0RXs8bnGXt!6{Vr@~#szL8od4yy6si_({DLYRwUx=p)txu;S#XVpM zJo}Z)iW$|+V&|Gl^2WbmnfOsZ$oqUC>2%=Ev>Z=lhKMfE-r+P zNf+*^ataN_k!IItmF(C?)+g_a#oY1eu`-WddV3?4m%S>?OTCsB|Mur&lFJ=z0%(!3 zom+kMQ#ssu2~t~|NZGEd_@akA5?PVB>F8CD_n`b5J(p{(ewz`=G@8Or8W%v5ZTRbk zY9HOq8<%&u{H=7T=wkr3G#DOHu~V_NxLQP2p5$ByWUbGij>|$qEYsSht#RIrkt{@i z>~fq~c*OJ5W9soQ%cQIuzwSkD2Oy1>pb?85>D-{m99_@z_KsoR2uaS+sGT5LLFOPi zE%45=GHI=$x7Ce4bqByt@UMWU_R~Y*`)uDK@q%UG5CLYD2snUXc(+?B61ESEEGwhj zJUOA6WgAdFK{WsJEec0u*Ew_ensfd=bzC&CwEscy`=?p`OY!C9P@b!uO~7ntZ8@>< zP0b1@yToyHj7A2h1!tKEx7$z3(fIsV_W^ME@=>oOlq4lvn`$IhnNku?|4% zJH^iN75o}y*m-#Ux2cYL-_}}z*m^%_Iz6HnUnsZQ{cfRNv%Sc@_UKL$Q~_A!~F+`#Y+C zsLkH%?pmNg++X5sQ6sepXOk%Z_!uWYSpl|Uwdd^JiztrxW+x@Yil?YudAXKig>U_) zo=I|+NwEiQ;TGtkwP&tLa~E`Ynd$A+6`hlj`6fIH7JmYF9z4Z3Dhfw6VkfJ#*(Nbk3MfVmKuoms5cQ(%;bJ`=gYizn`$sPab+bU$VN{ z6OOk}iL&z-a!*Ymk20Jld>6St`jr~rQH8!EketNF7N#;1nH9hMvalGb&Fzk=mDd=I z;QkxAv5+YIa0%D8#DL9_y4HrU7!-lhSrain0*zkZ65@tyZ-ddsanH9RfjPp?E$g-m zudSyB^t|gj@2`;MFRPSQ(l>QgF6c;_Xm(#Um$e&O?z2y|2iiA2-8~Yms*JYMH}Iv> zjHGt4#{i_l$O${h=@VDc^UG@eblAK8T0!>^>1X!@SdHmtP4Am>_uwo?c?PIYmUxxe z8e=LH{Vr1|l377)bB#2DuwRy5gZAWD>i?6TeYic)mn_ZL z=vdp0H)o>R%zQtzfqm`5T3_zGfQ+@=`FHKayeP(O5Z1MhK|<6PqTsH%>-xXZWA6%2 zK(69p8x~-O72JS_nUVkQoZ5$Pq1CcqqLFTX>@T02*BXkUq{d%x+Jee!hk} zOD&F1hL(=aK?!UvdH39EQJTCVS9k{)itkaY`zH@Qb+W5vc0LXmdkC`m>93E0jxOv~ zh#bKjmemf?qGYw{IuA*eNHP4?*DiWfs&>k$^seJM4b?MlA%_b`d*9Zli909Oi*tr} zrG#0m6kb=o)r1|@@|E$4K7To!x*QAWWPutrI7iFW4>!(D@)y>FPiWe>A%@*l*Up=R zuo_3^x`W}N+B|=<$?$Rc=irjQ z)Be7vs4-m}f8vx@JPXG$Im8EVHLs4LAL0D6QB&HGEBRz`u&)D3xxd+f8rCrq21Mc* zD;$cbgzFNp7K*=ctLNITt86rAXoKW6)VZk=^|Teop{nS5)pM1W-!m|^lS?BJ=`)HV zlkR3S4jqg?R3mV&j1JjIXFSF}aRJuDy z&7(!BWr>gQu<7{2Qd0g2lmvC@Saglq94h`Q z0iJ`HZym{uB}C?7!de2=JyG}1Hj3^`D}tJbh?ZlsQ^TGC9*^+l<!~ z4w2X0LW7SZWHafv~?CYjlEh>u^G``*e&znD@Q~i*r|Vlek|iv z!9Eg$@{Db?zF+G#N%97np0nDu$dO*zavE*fd~?+`iMnsm`HtwgT9n##9G+W#Bxvj6 z52ae_(*2(h_2)X^yKhzBv(`#>Qm5fp4)mz&^m!wL#?FNaB9LTr1t8w3^$|g(djZbx zj_K>Zw9WV`^kTXKxh5+u*P_%CSYdBH)iUy^2$VWCm;WI$mgeTWCycEMd&8#N=2mh; zsnCaO-oey>NzPmo&lUNGH@D4&>Gbd-*{bjt-bLZ?x5xv6`GuE2;a`=?ULqOUA4JgK z7su|msp#X-V!MsMf0zY~n_#C}N?n~|A(sFAr$t$+3}Nn2oKO40`~&tDWSbpzZy&$p zZ0?6LhqP-|zCvfaZ{_hPdvbbm3r<#60X-;=jAP6wCX0mcuVy!?d^;d%K$lPC`H1Zb z?r^jPa25{S1JAg{OwXz|7!!d8SphfJ7-Zq6D*4R~;$K~6nptK_Pm_KyOzTj5!gkbk zpQSgqW;66c+0opHiErpF-Xcg>^m}!j^4S@2e}7DvXPcj~plX#woi5?mK^xP|bIi8G z^C#C|^S4g3rcILMs^cqsh8)QS=_cz!zfa#0!qY9_%N_Z2#SG;f!d%E_i>QbuSb`9r zJd(woUY3!oS}P1ihAEMd6H&wJspx1M7l|mj(rkW0|Jr2hGjJrX?;*#@*1iP3gf|z5jkL=1FQ|)>M`Gnp2v&ye#0kc6hhnt9{GmERn zJ9tvfOdI2=7d~}7T}9Y?jLBi)r$ea`$zcPOO+K9j6PW|i)vp~)4i6o!M?KLiLW;b; z6fl0_XS&ZA*$D(Ol54{E zuwXj+Z%Q%{oAFdQi_v_JpGkwdbu{JpNVe$J^nH+=_i+(p4uW_$+?C#=hiR-bf&KnA z^}7c&ZgrRae+|E>(2P*}DlD9A!rbhv9HJte+!CCeT%6pTV*d@l?Cc_}>`cs@;sV5c z|KAinI7T@$I|~;}Vm3}@;{W}7PqDx)m!ymly60?u{5|QW zM_jNQXl-v)o18snD@P|!cU8PFJS}1p($&H-I4nlC`BLb4zs1^q(zB74Ufrp^wt0Vp zww87@DI#-2E3+haNy2@Ym$(k9LI_tE`7f_#Xia0rdU}uERWB10AQ%xfc$? zAvg}*Zlhn+uaEZZD6-Yq1lr|M7=V8ZFbg-}D$K!27=%-B8irsPMqm`qz*#s4V=(SE z_ggDif)j3Ueld(3UDT;f!3sAxTf* z5lJuNF^MM-&9lz8>BW9BEy&&0SCw+^EgzNg?$sws1^2ZjrQrFevr3s4K0jDfs`0S$ zTB+#a!{!D{9)2t;)q42z(>(lrk@#Ot-}N-iLVcq6HBt91QGS_dm`*egC0f60uAUE9 x8@bxZ)kfW={t)^H=*e@9alo_oe`#+2nr#4htyqJXu`vc92{SVaB_%~qMhb({pWgrg diff --git a/papers/incorrectness24/incorrectness24.tex b/papers/incorrectness24/incorrectness24.tex index 0f217175..ed154002 100644 --- a/papers/incorrectness24/incorrectness24.tex +++ b/papers/incorrectness24/incorrectness24.tex @@ -167,8 +167,8 @@ prohibitively expensive. The difficult part of non-strict mode error-reporting is predicting run-time errors. We do this using an error-reporting -pass that synthesizes a type context such that if any of the $x : T$ in -the type context are satisfied, then the program will +pass that synthesizes a type context $\Delta$ such that if any of the $x : T$ in +$\Delta$ are satisfied, then the program will produce a type error. For example in the program \begin{verbatim} function h(x, y) @@ -335,7 +335,7 @@ we call any function of type (S \fun T) \cap (\neg S \fun \ERROR) \] a \emph{checked} function, since it performs a run-time check -on its argument. They are called \emph{strong functions} +on its argument. They are called \emph{strong arrows} in Elixir~\cite{DesignElixir}. Note that this type system has the usual subtyping rule for