From 211d2f726523131260cbd173d6ea28f66ba17cac Mon Sep 17 00:00:00 2001 From: Terence Tao Date: Thu, 26 Sep 2024 10:55:00 -0700 Subject: [PATCH] added two requests to blueprint --- blueprint/src/chapter/counterexamples.tex | 12 ++++++++++++ blueprint/src/print.pdf | Bin 37435 -> 38012 bytes equational_theories/Basic.lean | 6 ++++++ 3 files changed, 18 insertions(+) diff --git a/blueprint/src/chapter/counterexamples.tex b/blueprint/src/chapter/counterexamples.tex index 6ac6e36d..b530037b 100644 --- a/blueprint/src/chapter/counterexamples.tex +++ b/blueprint/src/chapter/counterexamples.tex @@ -66,3 +66,15 @@ \chapter{Counterexamples} \begin{proof}\leanok Use the natural numbers $\N$ with operation $x \circ y := x + y$. \end{proof} + +\begin{theorem}[Equation 387 does not imply Equation 42]\label{387_not_imply_42}\lean{Equation387_not_implies_Equation42}\leanok\uses{eq387,eq42} Definition \ref{eq387} does not imply Definition \ref{eq42}. +\end{theorem} + +\begin{proof} ??? +\end{proof} + +\begin{theorem}[Equation 43 does not imply Equation 387]\label{43_not_imply_387}\lean{Equation43_not_implies_Equation387}\leanok\uses{eq43,eq387} Definition \ref{eq43} does not imply Definition \ref{eq387}. +\end{theorem} + +\begin{proof} ??? +\end{proof} diff --git a/blueprint/src/print.pdf b/blueprint/src/print.pdf index c801ebaa86bfbd8420d0d810543e9ea75155d2b6..2528f0acbba7e259d88d9d48f6e9c0bb7545782b 100644 GIT binary patch delta 14721 zcmajGWl-L|_63T&ySux)I}|Tav^d4x?N{9O!5xYgN^y609*Vnbad+VV|Ea;7&KzsrZx z^}u)wr6H@?-9r%pwF>LI%GX>Jp~!Vy;87G8-Odki32_)zJ zA;zp84oJXi_0p4qggWcDsDZ$Xzz=8j%@2g)WL2_GAwwLPIK=t*B2`7wsqQX<-4O!7 z>3(X2`;>Ig$(-TRYwg4HQ87TE!LQWz6LBN-qT{jJtKp<3L_q(Cp<< z{$SX)7jYS`9}0WFf!~_>-nZg6He^J2+=ON6cib3JW8v~bagx*?d2 z88eqg0m@A0w78)$>nnq_aj1LuUc_l&G`{xqg5#1clKmhxgfNdpsb(l9Rt<84re&!* z%$N1xGZ%eQlvfST7mgJ_uQ)rQ{%NJp(W-A1EWWuIV-=lWpyrM`pQYc5#CVY;p$`_* z9;{%g95g$W+K@CNVB-2HS~a#FGNktZXsfr+&6(;lI1Ha`eWD!F^z4@$-5#w6a=wSq zFvqhLhOzkm7S+~s?@+bf7Qoq)LOiuUCry4fZC8!nZ&bKSZm;}Fo$^J%Q_7Pqb&#)} zA&ma5r{s8i#er=^9?CrsrACzi>JWEUD);s(Bz6|=jAi_hFBE4=nxiDf>MY3%598%& z_wmwlCVbZoJh)^GV_o}#iRJbv%O-jEmDu)b{UH2S+?2HhAQ-w~6z zO10HFXcY{%s0}zKmu&lGd}3}fc{6RILZwV?eisL65{Ef24w%82Fd{_(8>(zM;nc(9 zJ3h23xFL8=B0Co5i0w%Yv_NCf_;8OqPpf3E@>XtU%Bo4Kx9y~*x z&%w2-i1^6WS<=I&j(?XNn^jkOQcfY2=~q&_TADE8EngawU{JmdN{Xh?h%uwA6NVU5 zw`)!k{3tG?pv&pk{}I^+m@Dq`zyV~leyGfrb0LDB$SELKf_H2;+s?> zQqiaO;Zr2G0%azA)NaF!xI*p>^;Rj zdO?!h#k4vm!Co~{xCqW`NyV8}3gyEH{X0ZS;e(%IIjW5K)u^f6FUm2V@bF!*u}u(! zEEw!HUrgvEvOi8axw$r;7BjyGtB!6ww)DWrxY1EucXk}|e@fElzJ|FDnAjS@Ui4eu zoQ57wGUf3lYc)>=!kytMmE;fdY#RBUp@@Eu&YBCFHXT>^cl~qvOTx=jGLFp1ogM>< z!CR9ICl!&nTP_`%j74lR+IdElKdmypkF}A4oR})2_E&a$sz+BoHuZk*uxnkrq_#=>x zK0sGuJAK?pjE&`IK*^p&pIW64Dzr^87M`!DKH47CFD=Nps6_va{f`cFI)oT#?u#mD ztiXVauK=2wQ^b$+jH2TmgfnkTz|%!6m4_0F$S|OdkmBmp)_C(7vQ3FM%R)~=L7-$b zu!jHolI0ebY<(>P*QCUDw7<3dO<9!4Eevf=qKINTKrniES6{-30DfExSrSi$nqE&Z zP6UGXeef7-mJRj8a)GsMut6jmD@&NQV$n7(nv<_m#-T&U%|2$O0BMd)>~5!VC`&PF z#iyjj7^~0>XF)l=oYgk0FY9>4*iNjwz2NUeC#Qddr!U>6*e1k-j%IIXzZ`M;ez*8X zdJ5FP+X%(`pQr%M&BY56BB20O=@A_GZC~n|3DoH42#UmRSJf_x(UEB`$JfO__ShVg z%UT`f4+2-e;&Rlr&8LPH=2t=KNX^R8X|s~SKMtGRm`eC{oXq4cJC(8MW&YC z16&hGHqY_-^7y*S(7&u+*E;OeWoxKg^<6Au-1JX!uQwj}PZVM&YLjJFTg&6d zv%kzr^f z(31Gufs{Yv)jc9rAL-!mH;>dmg|5mSbTm4)9G|W|`apqG~^B@Der|0+1# zx~t3Aetv;Y45~@~FJrm>&0|2{$Vma&xDS1d!e1VkP3t91e$7IjVMNjm5rHrB9pHXA zoWRTnI?(7+yU3)hFxQL0owg*koxTP$(R0MlNTcHgr1AYK$I6++_b*0_tbSe$`?aT$ z%MrWN!%w&GJ_2_}jE3J@&o1t+U8mL(=jSAR1C`9yob&LeO^ey^Ri<~A%q9RamCOhY z(PgvG4_|z%By5Saq_DU$#85rF42zd9jSTT;pjL-KlDvd1=a!jIDnv~oL-6n&AWhxv%tq%OVw69Aa}uDtyZhpkxY03Lqc|Km_o z)@^q=Fv2e0aN6wkq5+FIeT48iMT+sJ_PMkBm0Ef|X;$LF){)iUzql<-Q4#(BOyvAX z8g^;jJT>C4cuXhHil+BCHT?S|V(8z0(o;4iYg4*Xof+B(%r2Vaq_f{W>OWNNES|hv z98Nolf87AWyF6{KFNey;znqbaZFn(Oq$NZKcE?w7ZNHVa<d_ z{XTJAM}zM&UI=_n3pi9gIsZ}Br{qC6%znPC!W0!vmGa5-H=({*f=7RsCw;um=qrwG zV|G53+2VV%6VD&C;RCg^^vhcxG__Hqe z{4Jbz!ELy~ZF1=dCq(PCM})T^un}`;mvsdcyZ-Ig;FbqtGz!nC2;^!(-0~&ljf>lwFF8H!gy4nN7I1R&ViyF9a_fE#t8s@lM9!E(GaS zmoLaPB2Yd5JxVm3H&eY0m-Yj{TwLa7dJRvYXr2lZq~?@iPSJFzYJF4ov~?A zc~qTeW4hk#E0GP@trWKEi;cUJP8%kaW>f|?MhjQ^WwKP~u&Vo2bR<;4o_$5Jb4I+P zBd?Wt32C{GPmfc66!!-$G2_$CsQE&*q_&A>z*kp2B49XOp zt^VyzNYXgkio(u%YMVa;hxzgX%_OZ*0RNY1M$ z@haATvy#6R5Qe;AitjJ4oOnPrOd5XuFBH80g@T{^f1xl+{y*X5V-$(XU0+hSS;OGo zezy_ZHf8SL2<;|Cj;H>(zv1Vq=DJ=r@o8RV;%y%~(Ui`6Z_2T1m?4!*M`nb+%eeZr|t-&fUr4XWT})UV&_oTQ_#9_3%%YsAg-H2P&1DlJ|18 zKH^(QcK^k;N3+qPnTB(tM5;O2?Oh|e+?v|m`1Q}5z3PL=c^NY7MFBH@Gd}tD6nHNU{BhHR>)XIrv(Gw`>W<5cq;U6*oF9Jc9~zF z%!RP)@N~3&;f5gtkypBDLb~ioaA22%P5a;l7Fy7;JK;b6aDoq|-iPiS4#dQd4C{?c}J2DbZLhC zpW#|kbBG`n^M4ZsVvw3L56Hj?1>{4=0r2wk{U5Izrw8wiJ>2wFFKyvF=awvt=V&!U zp}FrTsh(17Uv{`Jtz#-_hPABtdX_Y;4@?GZRdEinDiL7290;3480?mmHA7o0F1w+J zKqpJ3kx$nfskgsw25u~$W?clZq!+J)u~$+aC!b5-y5C94-Fe; zf_j5a`BMR+SIag5+NYA*S{2g$o?s$m<>BC!I;8?i#*K=ZjfyM#ik@a9jx%c1E1Fq) zKAqE}-hdnv9g==hSw<^VbW>2n- zh=byW=}fRW@$IqrV6&rD`mN0BYnGQtPND6|_{iP*)6B+e6KZjnlow6$fnTKv4|=3*;x9>%uK^?%K?zf+h1A zD8odXLwkJNZ;kD=ue#oofl+T{Gww5FoRsfq`6m<}46fEEVGmi0e`7YHIyLem#mY$J z1>gk5&fANfd^Ufm{>Z(*|M6^eOuqQB0Pz9IpEE27kkgi8qC%6x4=I*@5`s_d;(jN+ zGcj`}w0A#If@E16a}_RvHToK|r0ee?<@qB^@|rEFoWm%eRBiAt58^S(_3=BSXUueU zTsWocYbN225N3>%wyxd8kjRfHL6}WUNeZzby69Makld&6D){XN5`KPTSU*M{j02@a zC6u#m05u7_?6bj+uCD7v)Tc zI&QiU+L^GSDz>8-VdK|`iZNu_P41(RU93IJk{8{&OvsU=uutP-o8sBD`F`+K>;#TO}u4j5lEVh@FLn|0yPUFK&m zg8F;Mx>%oP`1e7vgLxa!urrA-JGOKG%UGjknmwT)G}9sF@%T%`dGWqRT|peqcJpj^ z8*Q>;Im`hUmhbLn|I^DW1|?mSmHiW!guSfT~07$GAfue!84e}8?8SN*-;$74>bo=ELJDP!^6eJ(;!sW)z#JpaMSCW+O~1Mb=1ph(aVkm0H?z zBX_;w?f4sVL$1=Az$SJD+#)LbQ=P7$Tqtb`$@DT>Zy3w}QAH6C>{-SixQe#jcCq@%S|fBD%>!2~&$5UN!Y8CQ3*S7ZdSP%? z`(nhfD@}@xId^Z#j2gH|yLJf9)mu@A`J$7@&_sIkz(uo@ug#iRrfm=SGt?%)`g)M4 zG&rI!S6ml+J};ieSx~LGe_I*Bn|*o?;W21!zM`3*>$0OC-y4PuU^$)xc+=JPZ%!TX zrgq-QeDNLY`>u5AwU=nap0L6QS{YItt;NE^JCwSk{T};Yw=!dK(-;T1=dN9DaWd|i z>}bsdYCWONln5#XP=3m+A8tbEJi*oc9$*L26=SvO!Fc3ylK&y7e74B&B>`*&PX5`8D3i`)CX_j{KDEf-D7RInZeEvdkQlO)?? zye;Bc5M86|bsJo9()O$edp69JAi2&-*$f@XV538x(m2bRdgViY;r3Xxe?(8Z7gF(! zE+KGpo_3+3em!?e%~nHqmt-M)N>@Cb*pR$N*>% z+%D$T-C0@FhpAH(_7b{{pNUnDUQD_$Zk)S*U3Z#1ldaoKp2 zYdo=Xj}g~SGamkBL@fK6_|cO^0TDrtNYmXtypXg&6 z2m7L6tu&d%1^h2sv!V>r?ee?A+d9bpWo|P+YT6iL1XrGbrQPy&ZgS~SBQq1gk$R0X zDBwUua>;Z05dt7`972pxQjs;+hlYJI>NL(M8CN!s{7L{0awpBj>SXn0lwC3v6Ru-k z&(x~NgGgQyrXwsK;yz*^L)MI`Q#q(YX`|`h-+P#&Um&d&RF29Y^!;OdtX)p*nND=T-aBoQHPgb9jVFJqZ^AD?$FPmL36o_ZsqECjV1 zAo5!1_JX%b5QVc=uI+sWyNmFZv9Zii-j+u1G|L*zo4F=rU33-Or zm6%GAOK{Tiwdqe-N99&qJ$$9oPl|G-pRVDvU2v~}TY&sdN>tm@lG(zl6_`tRf zZ9-8%EVDAxDD!l6(Tr56VjpU6JC3{NPp*lGEVMkWc_QNIUnnkmMv0%bn-kig<(LVr z7uV(MT(%c#f8ddeyI4DoLvjbG`V+5&5H|S^l&vLx357eWmRQE!`BWYBtziis}o)WcT85+ZMY~3r#JM2mS$xYBH|wJH*f8Mb5UH6g}gqCN^CxI zAdFN7d4lkEOzK=*z-9lpDCV_J7s1QVE``4)E~LuuUmv9eBI5?c>-JH<#PMfe|DK&^ z$zqO&2w&oX3-idAr(7dU3R9Dy4Lj)CMkFOeTa#Z|II|4zv`2`8iLfKAUXGNW>^_r; z%FJZ+(drVU7Z3RsTir!v{=j=>XUo~_4@_Zy`uj~{u}{DwU>-Vo<(ld1tKF9Rj`iZ` z2eoybz=3M8-Mi}8w!4*gLA1LS$v)wZBZ~z2xqty`RL!lL0mX#&d(*>L}nxB*WHlSIKZ?r zKM@ztTIhL12*@=q-2NwmMLPGIMh70rduCwfiqp2t+(*FI?x6iK0P)k?W}9L4&*Lly z+?@B!n@7DR+7NUaFm_x7_l#=;jEc-`6908Dn>CjqN_zj5Gtru20!wlM*X?MGq#jMs?i5oQ|Wb8nC{;Ze!j`fk-0oEO-(F7b^|bRizY2i0;?hrAB^L zEFdhugUPtEFi*_EbavZ%bGqs<0 zik&I@4G+Z6xnX+SIWGY;crb&uLp4(q@mAjS^Fo{mDb2*KB;z96s9z)C?a2hhIfIx{V*Ga zfmIHeLAlN)Tvl&?9R#OB9w3S^V@Jt{7A-eqTVEh4)X}ey_!J%<90uECL08{srE;A@ z8>uVpB*{`cKg2tn zMQ6%)^6NU6l%VIt1a?bZ@)f6^4du--n_Nd-vj~L5YnTeh7K%x4p%8Bo@9kZLVPQ?8 z*rmOHE)EP24gDF%E2sNK<#p|0{8=5rb^M5qL`b}2K}#B&@y3psDSK6s=8Wx`xh$ef ztZ`a6Z-F7jL0%UwbGf>;NB}StX*A-#i z)kB=(zr^=Hzm|l38!gRhS_QMYMX$*af4=q+T`<3z1;|2X?yLblTOd^>0P;1(YMhY3l`T{C}zf6&dc;YmxM zrNib(O%?Vg6|gQZrU*Q$XSX-oz!+Tb+UUv84D(MXT;}KB4ry{VwB28NWEFZn zLfoEq4HWOK^&Gvm58ncG4)6WIcVCx8i?W@FMST8bKC{yp?lfEa@fgMRvn+K#d3&_e zfu%04A%*wn+gWJa-3+GvNHXK#sG^;wsMKNI0o_Mx>73xc{C7ln?$5EwXC`(z;+;Yk z@@>ibn66#A{R3oho2g0sM0sn>f-pLD?wRCEb#YFFua8wmxUl@S!B)%@t;lXw&=H=k zt_C!mO`ed^=84f>_)`o_j-k61bwmZz=1h$ezi6JOcra*C$^z_nZV3fsNS|BfbDp>Q z0m&J%?2&Q^SxdqO#%{cn&(8iX7+D$?<}_W@FBC+jb?@xmIg*tgJYy7ywu zpwEe@ZVZsl)BhxfQS0*b=`@rw4}=R+{;Ac6$5pKnFYx6&c`(7AgH*SJmeAEfF zz&(AtEz*WCB7=Ar#5ml}p>J*78H!YT2CUAOD>sw*%W}!YZ8uJQB-1i{oBA|?3DVP| zggVl&Nv&1J`4pPB6$ErT3%>$YQ)iB1xs%y)E$J-EOs#Jrn$O=Kt;UmUt&eup(WjqE z4xuti-52W8?a_WC#G$BOX1wllF??5jxDfw~`M5~_H6jKG7!x9YxtsaDC3Y3;1SqdP z((#MZOj7%#OWUq+6%>IruWs^Xow|QxRH#5LdE9&MGv4lOGrLQ6 ziRde$ia;N^bJ5v;Gyiu-rjVg+w_Xc@?c1QXn7dn?oQ&y3PzQq}7Bj;kfE8*;$DjP5 z@Ee7fq2ib?UmxXZjDSn__x#V}2X(Z%2vjN+$`J?)6=sGXJ{Pb;8Z8MkIDI2mp9qP3 zD52%47?ei1O7Jzq2wQzRoCDxDMt(7^Z<>Y!1X`6NL{sv%X?2Fn0lRITGwy5}79-$qmdWkY!9;1Q3_ZbkrC2nNIaTuo$(=gD$S^?f8jVY72|ufTLOL<531L6!es) z9+NQ|I|E5rr(uL#2AW%1RaV;P0TH^-Ao65VZs-#9JP2l)V-XL_j=b@ZmHLBPC?gK1 zU);|sDTy|!`;ferxRzXMrZ?PkRGQyzQ8N8F&SAURg@^F?t_a+8dhXXyp{m>qae<_a>=}Q=fANyt%{# zIgO-$=LkPkFwmlB)Q#-ytRYdW;9SF*32CIX&)`g{b=&e(iA{*eVLi-CTy!~(ten~1 zYIJb$%-0MNozQ3dQXf=K*n|xhmvmkA;otKAkQF@X^G3}~2I`pCB(R0Ll+CR)94aNd zvulru**`6_nrw^c9$p&^^orBd+A&0ZP8@{`@Wm2EB22{4mst@Bkb~2kg&O<#qDjUG z4=Ia6vdF4lh3TLk#`>N?Rb9p`sfW^UwWq5zl9hpF*}%kU@vZ%%_LIZ6DXm#&N`5u> zii4KgP}iLW2!NSC5r4&yo$`Tf6T~!7?xmCh?^>Yl#AzWYui@Cm>K;}>ktSyxJ#P&+ zeLP(^W>7#1J7_isUjLHP$E_%onK)?xFFg1=8$)5up^1^`@hkihh3efJmw&}hsDP^~ z<{V%hg!`z860|Gqbf*Cml;33h+~r<@ZmfHT>$I z`;$!G5Dq?8$3M_Fqk>zWuy8Egia!!INuHzW{N3y%l}JHFacc1t=5C&;w$}8kfYF=a zn9E$d1VQ*@&6}UBP$kP+uqHuPz9r^t=NW&f;5}4)z|zK-XWdx3AEOo%e3=vYB&5F_ z4p=^?E!$5`j5(jah;t=(%KlR=$ASF!^+F7p(CNLy78-)b48iJOD@YkYuGce%Mgi5* z(1C)TBq0Srj&#EHA5O~XPy+v7xVpJhaB_19f?QaM0Ul0)|07hJ zG_Z49ZNYupFb;BREX78;kf#R`(mS@D3oY}EIyPzFN!oG8mp1JwU3=bK_@PNC7PI-++}DG1C)w@qQAj)Nd2MO8D0_#p_*34PA^t*(^_O4W&yDfAAls0c)rWgQx!plT)}a}5x&${=Bou{aEvBsL%}1YPBX{;5g) zyoEfU6RyrFA+tswsoMU%v7RD}W5ZM|7D4X@HWcMZ1M4&OnW6_Mt)*ZML$iXRBN#`C z)*8Z%5mf`Vl*t=R?ELvMtC(^Db`nu#BezSLdlm< zfCU&Hiz)GYwm{T`6H1xTi4?ek5W-kwNcKN)An(@zTI;gRZbdPd5=K7Wq-C1&qXnYu@Fj8_#?zXTp(D5_=(oPb% zm=^UsZf*0?a;}EJuwVuk>TwG8cwv5qvH;YXq}LF1*=6Lp%^hP2chsdMUBL=H<$WFs z&TX2Iwm}WSKZ+VCkb|fx73F20zx2i?4Qc9*Ct49=>TvR zsM9dQv`^^ zmmpm!(UO!e!Fe)mW!O+MTahxYkrGOIam7)nsb}!847vA7SD|Y4fHiH~S4%CfdvyYH z#fZqey+rGW0f=GwWt$|caOsxPDge@6yI6zd2MRk?&&})8<(+?%Sx95N!c*X5R`Sly zV9a*=;Onb&ClTsqZU_M1NauJTU@%jEInV2pUfk$Q+!q(+_LOvAp?jPGPg zAxXqx1N&2gvD3-+l|7#^s`%P_-Ol>5`~AiC_|s0&*I0%+67+83JT&7tEud9!r~$pd zdrEvNf?mFo{mx&*_{$hd&vQUP7tt{Wv(z%7HtabRrw&{%N@ZL0f(Wm9qp5vx1Ks(B15^#wJ&sr^Ok zB3u+IQ_U$PkU~B~1*DKT?{f&qFUX_rHb$Tiv{>5MV3zd|a7s}HNeAiJ?AH%!`(DpU zcn0G%o5rw8?dz9Ir9uiSm*fWucl_q~Ge1@^r^{@gT%qnjHZ^D$ra|?kDr=D_yPWC4 zVs!@X6R`yu7^QMiJLordhED+x2LjVo;;N)FZj(3*)#tDtBA`r4FF!=#_SpHkTC@t2 z)G|<1QzWO}`Rd@0oY%5Yl+g#Fc zUlZQ@OL$9D-;ZF>VZWBON;Foe8R-w{Mt}KN=INsDD-I>^hL`z>4>iPiI|rHS9pNF0 zr0$_)TU~rvFwmx{Al@4EJQL@Vi(rgSRQpIXL^w+W9K38 z$q9!~x8aFbV`i!T?%f%-P_fIxgF%Jl`!|hb?>&;dU#{?L*R*xIDFtY-nd9tIw616t zJ`5wTko|*lrVA!x_Bftsis?c*h5XM4446&N`bM%|%>bD#Y-sL9<$|QeCWQ-MXI^#M zj~}3?r+W0tQ8Qivp%1QBy?Nx6%H8eNQIGXwR6*;;A((!6ukv5*cWGJcnydG4i-lHj zyJ}^ncm*H@5ldvVI zA>HxMIz53o*-ioc8G&DZ7#YoCi8b7)SN@VD68e>Mi04-zKZ3Y;uH*>*HEYHP2ky0c z#_0?#;0Xj!R zTQ@82e^{-?kM;-FKm9`ZzB=<(zAV?Iv(@R?mADc-Sos$DgGtV6cJ&w3-zB2~t=F>lJH%lL&C6+r<$>L%{OlQzbv%bzq=8Z~b zib^JrN?wgjZi%d`@n%a*X=BP5)~^w8Fx&`Yxrr*gL;MV_C~3DZ`@|Ff|&J^Nwz{(~MHrC=PD zzV_hVL&ldF-?}XJ_$fN_zxjheSta`pvH&aI-67;AAZ)ajw;1zdlPxfJ!_dF$UFG$! z!Y7B4)NSJs$xPAQX;r$)=cB#pR%RO*ti9g%OcWsHIw7R*C?ea}(|@X0MeNeIjp$q0 z#svGxcEb2`#OnOKJKWpjrTz7%fX0E2=H|umqzTHSy+P#0uJ4Z}J0tKAicX>d#PQZu zai;Zez*iL=Q00@Qo*(t!KTD;UYWup!!yBiO@)cjv}kCF)%PmY_4ZrekS@!R z_0yjH`B4np10_zi)0QYvo4MMzxXjT+B$LTE4%DK8r!^)a>IE!EmVBfgmbXdMgt_qD zC3e?ZFsJFmxG=G<=2^c|9!BkjJ0 z&wvO}`0Jx+qg-?rr=$n-MMgrvTzt?vd?;f$5uh+{JuY;qNuboSeBRHT;+|=npgatv z2JAzYg~Asm%EIeGEYp5NuL)W`#q)9`EACS9;D<-fbwp+go@7vkx%~OO$P2EW zJL36{0Y(yG4WTzQ^4_VTp`8Ymzs?y{fit#grS(?2SUO|54n5>_30b|ZS=gU5fCy}x zEv4ddt=P@PN#@NXRN@i{bf@|NpC*csglQXNwcf>`9CAp$P13Kqd6#*lu8*#DRc;rX z;+?PWhx~w$-%VhkXlBLbX+VIFAFrPCW5n-q?SKHG7m;bdxqbImeScA*u8a>&^l#8ZDWE&Zp|UuYru_@j&M*PiN1SmvSJzLz;Uroj zvrjyo+Z9d&G24t#x3{m}o<7>hg8l)#tukm3ZN^DsV)6?4lj(PEt?#=Qz~OX^9KR#V z+x>3j;%w!L#B`kpxQO?DD_MF?!*91#{`qiu<#f7>_}$V|tou82_^)q+CivJ0oYPUC zmMg@kfE*RhwxRgD0)qA#*ZccB@q}r)>qF-)>jS`*V*WJJN`|+>12@v->=jWl1kBy$UJs$Hh9Db=up)rKfVxT)|%y! zFt@8L4Jnq}z|mNGuGBYM^C%qB6La1-T?a8n`qCTafro7y+fy!%iyM9gyb z=*c*xq#OSX>XiW?VQ%RZdDR3W0B0pd`^^vxL8Rq$@0K5szy5 zy3~GO<-XGzla`Wq_xI%&f_KQ~^){~RiHz-s+`|LzO*fY*H>)Ymp`6@SLMLwM*{$H; zmxNvY{G5E|4AeK;`WM^qEdA_{h<|I~02Ao<-n2-g2LK5r>LrS8-2{fMN7fl0{WA2^ z7VO3rbk|N}CH!MA!D9$2)D{;^A8rehBnAqlGpf|KP-rhILIgr2&T0)>bTDFMI6-8X zKx71rLMRQQ7}#M{9W^x(3Vj<>Bs}{PhD05<0u1#FjMm(Pmb(?Ys*b>`j%=e2uU1I* zrx2288z8jkA+-*+8VRNHMq}S%YmkKR2=xQQ{w^S{qagm;Puzk&2!`%Vgr-$TvP?uq zFCbx}K))`8cs9X!Hig*e6V3=m=Rg5*Anjr`eS2HKG>eH0h$)whAs~-w(TaKecvd&2 zaWSydInCDpWG4P63sm*_7w)LzLRNaR^e=73UmD$N0&ooo0zf@ev>{uf| zHM~bx%G+riRN2&78J&?NXsbdYSvp$$zn>`o>HW(LH+NH4cW+lqDV6Fu1!jxNdB4mpA9!s`u{wdOt}j zo#bP!PExhH`@I~zs~Eg~9UGjRI}w!Ko-m?HzJ`2M9V)k3?v2R5yL%iVc2d#%VjxJtAXY4%xiEh+Z!> zTaUOecol!4$xX0tcuCC#3R*El^hBftzil`nXvGpDQbZ1zf!j4}=VPPp!&$w|X%p!> zBXqH{E749k67qLS9(6z4=IYmJ+q zuB=xv2XRX1B+CNnV+?7+&|6NTgYbK_c9yLkSTSJnoxL4&co0x+fcuG!^r#*(tQcd- z7+`_%bm|FlVfYJ-DB=_?L@}W(KXK(Zjznay4|T|QN#RCQ>6WewpElG0N0OudNeG+S z39*=`7b*gjFM}uivZZ8 zxZrPCY81*VZ!maeNE_j4H*{H;kL&5Gk}}e+m?$RVP-)S?tf>ph^t$fnZsGG zb?9=;+u1+PNkE}T!A1f_|q zgd{(J8QMdb@Jt4>5G5U0>|LdFmfv(WqaHj%>LY4X5roj{o+PAY$?>s?j=H4>7N{0lcb!+LaP88Z8+X?a=5E~ES{%wM zf!wTo0z8X07jg!K^01@LA6s(Z5k33)hH~hm@PlV@zv~hU)CERlbTASqvIlhw6Es(o z;5EsnjdKhXg3ea~k4chN5r9HdO69Uq zzNdiiKpG*&{Od_SpBL}IAD0a4u|r?n(W|UUrNDvyeCokq{esJ4X>oFXVP;prHpk`5 za3V-~1>#1TBr@;d?QYLoRS3vwke8nWaGa`UIZ2|H5D8sB>4HXQu6=w6z%8gVFOo_1 zF|XyoA(3*Uslq9!y*5AT{q=2eJhhrx^3w85_MG6JR2tpe=W61IAh8xW^fWInwcd53 zF)`oxgwG+d%ngeYPy5BjwUMPgKhyC&sf@K_OM%jlU+`?LTL{$YVrA%nLoC0IhnDyX-_@3Lb$X~SvG@!^b69+{dw+&IBE-l+s$pVn(` z)Vl7FeB~sA{|}O!|B!^>VCM$f5s?BEwNO_amr@&gO2$E9_~J{Efp4Ikdy`c?* zyg$RU(cP@m{qM@F73k2KTv7t3UGsFtIOPNfF2CK2BEp?DYMOKNE=z>Qu+#GZAIUqB zqfZ|Vb|rhJ0b#z~a&5wSo`RP=M_rgP9@+pib#g&3KSOOj`$TYQeQE5 z>E>y2A96fpclL59AyH)#sF#6%mI<~dZ`MK>5bv!mSS2^LZ@E~B_* zT!Jv6Bo2vx9H;)Fp>U6i%B5wO3PkG|MM(6MDI1!c24@_-z3O0flm3gOQRJrP({Q=g z-Z2sz{5D&klcT}=^^Np7ck_Qh1|;%q2Q5u0Dz!J_djuw!6a zH7h&8MFRgMo%w`v~) zRF3lg&>AbXaRoWear+WaTl3VL5Ami zVP@wcMPU;cQ0yJ&?5rv6KlLOn;%J7_FClgFg`N;`%H(#2b3@hl|6_t-9ZiU;Pd+3D za~PZ-G^T*xO=7XJe)@RSF{*qKdwS6?hn>7U+29^sXYSfx7rUw z7vx{Byr10wVx_{m_H)Lz{cT2;lRvTA;!MRSWt7Kw%#F8vzm{;iu^43;M=k)1$v(Kt zKql_k_Jz&vrxJWsqP~V<3$3%9Te71Z-+c=mzQ!pxyxW+CdK-K|zW*4WSr>A~b)C_AgpNX=eKksR> za?B>{KX3lTCiF|fUupc2E#4d8&_foEkNzy1>Ek3t zJbL8VaELh=oqC2~~cTAv3)9cPG$Fb}=O^NxL)k|E|?q4z63<}dfMD}pG;mhJ z_0a4Xi2=}A34BcrIAJ~mX%i1j>~Y8C{b|ZlN5_(sNgFWaX!a*Mj|jMACag(%pO zFlFm>TWR_##_Kh00vIfCzxgbt{m{02W*eBEe)Gv6$dCMCP+IBs{*3)=uw5d2$Ecj; z>-ay6gK;LJPysl&`TjTI0ZEE61FWbKe?PGJIvE$JKjuO(Ukga9t{Ts_%>-(|vQnFg z-=DI~_17QjgRyg`rUabQUG6*@QcWqZBF`p-eidUksq{kAF_4 zKE-7@`Scwyp?ak`c{&-@5eUO~T+*w!0wzcA?lCgY!>d3y^@V5^`6HQwH82BL-OP_| zCSjgT=W&eK$Yiz57=z`G=1H1caE4P`T?>_B+~%%RPmh*>%Qu8(Qt5p@S<@rhOvaY* zf)grQW&&sITwyq!>U&wjgk?3sfl4)l+>XZehM7k}Ze_+288+3pWU`us)YQ`jK#~!u z$&}GXu9wH_;<-tzYL=Av)Z^7UZkh5*NQ#Zo)JOf;$Gy>B0+bY+`AreIDPYJ-dA}(L zq%LJ<`Cb;xHlj^T{*w9*OV=cEBJ+G@YDsG*PY?qxE*X*e>eDxsiI#?A*Z}> zm9d4!p+vUV5FN0ZMgJB6p>H+{_WmC#fKvoC03NRYO@u*`k=+0*=J3uN-R&vv0w7Z% zA*2d>!X2Y3RA}Y?44xawCg6IrZW>OQac+R+X&dO5bYAwtujMiO-eY4SD%7=9$-dO$ zMe#ESq|3naOIu@dJMm+(bSXFQO7264d+0qr&*8NPuyuv(pjOG6ejEVssXDrMpAws) z?<9SBo*N<`ed+Xe7vk#ZY_{*X$Gt-d^<2$@$*Qh=RA4#SPOBJOI-8&_YpxdOosJI!V^zkwWkNoP_UVnj;41$Xrjg~msWG(vI?%WWH{nQuBWNVI>@y!ey| zGn6~kl0zi|mo`qsEdlV&WiG2^Z5W$$X&PL99{*7N-{=PO(AOoyZf;~j5YmFQeCV1r zo@p9lZYs$+41>Jf`JS8{RUNY1Z3$^aaIF~E&+3qK5 zHSluK9=iwnLl7I!i@f9Zc(|2rf_V|PK}K*=pm|Sdx^>nt0UZda>FDeFFCEjwh)tC= zSI|Htaw;G|5fwPiOa;!x1$LhdoW2|oEq9%z- zs*h;rG;p|7bhWFt)M&W0(KEMeBy&}pAi%}IhEbXG$*w(dp<=^8N;t1})|F^<+2}R+ zE2!%hwlv;X?_{q5d)n}%ie^HU&2<*n0iVJ4pf(D-jG zjh~wb(|5!VaCe3g%=91;+Qg0UO7+WLwxfwT77O7Y(Ed5M-Z_YPM8W~(QOs}RQjg&p zcMXUpI1`S4NssWwwIT_+`op-@4?=2xwr1pRX<;8ypd?5^$_SZfl~h`1kn7@?N2y3k#d{_CLPAN)n^9mEsD7%E0Vn+n zEk0E>+WQp9G@!?e<$0=~5}1F&YRPFqzl{$RSuBhLOBSp%6!44HrFwY)7SXC$r|1Q+ z+35YVKXb_eY;?ZSmtMfM_PWRPZr7KA;i^>@&mSXnC17aq6@3aI490lR7mVgQ7)@!~ z0slkXufqDhH5q$MZnUg0#S#5_x;0LFer^aqoUHKakz?b(W_R^3=>)Badcgr@X-ZGHqJw(SdpyMtC)2IY#K1LG%VnG7{L& zqv(zeG1K^AcxTbnoF;?zoaL+1Yl=OMx01&$Ne;=b;jm``|IW~*g0+GUlx-`+JeF7L z2g#4Z*Bp1kBi#Mx`mcpgtdDr!SdR(fdh`B+U;^lE+(Y5=37<~D9kVH9qMRV{l$>A$ zFG>UA%O%r?3OF~PM;SP_qe+KDLx^J@nZ4juZu(-eWkR!grFcHc^)NtDhJi zDZ&T67+u`Y+u#r|1X@ZZVr1;`TigHRjr3~pxgbaB(%?l|hIxL|0w2pS;YS)1k?Rd( zjbLB0`QDc7SaQsGqfe~aQPkSo-Pp=nWRsO>Q!Ai4Cqu+{`8@}&pXVI=Tr+}i3PscY zmK^TE?+FV>0Od+ZT@=GHFvCMQvb^$cc!%Tk!wh|Z*Tw{J{TLsR6`y-?8sgSyQ+72i z2$_SuHo`Anijdp!_c4lhZn{67vhBn_HZ1)9BYHBem)uFYBRFDC$nzHeh6~7_0IK*6 z@opeH#f;eO2Ea|AT)fBA*PXj;MIxs=K4gY3H(Kuzzh>reE8F z;`yLGwCoQ|ddJL{U$*1&-JtT9bp6)iG9r8mZ?$#Go9i`?x;FKE#%UsJuI^(W;9#*{ zJA2X+5CyF$ii;lw{hbhoh;$v6=+1^_EX0a+KVx@=gY14cn-XcBYj1CUes7O!9tnwy z3yBlZ>G)N~_NiqZi1_DP;ai$s*xV#-2j<(+ z021!t55)IU3bWN3BJo%sG*(BHZGuJVeS|cCMob*r+sa|b43(dFnWb{WH6@9l=Jwvy zf!4h2SbHWJV=ph$3GCoU2u6w15YqTfs`K9sB+N4bSHUFG{olN_z3#?dMJYOQ7wY&Fmt0or7btW zi@NaWw&@<@_TN3P-BC^6dD~X_u9A9@LR1Qz@CBslvbp*+kd_ZlpAqUSvsw5Nd_$G4 zaBwd4qLF2d1R~9<4{2#~Lo`Lc+>+ZBm$612*qhutxy?XjewL)l4wRaJk)>iL9fd}n z?BZfkXlXE}ZOl%sCKZM!u6t`j{SSKpTWDn@!Bvsyn8}3or`#t$*!~>o8>S}f9DIkvHH2);YfyD)T$S9|mv!ABPK~rM zh!T(;=zF&Igxx-r)#~NF05x6%e~uj4vR8XPnn;n$_=Xi7c=Z}<2$?6d^5O*WKq;K> z|0}WSY2%fac=G+S{q?9s5dl<5{L}pRyP}&uj^Qc)qBjVJI2z1N^1&r?K=TeZeiu!6 zXdqNj2eI$K>ts^^o`KMUO1ERDy(Y;p9r+WFn$3ih#|Xwj{Y@y}&SVWWTbl*ML16+ovP|mT=fP#6zf19*@QwyFNQAoWto@7jmxmZgf*@ZA(aG z0e`O9<)({3dJgtW zPg>ADI=>D+wt%O2HvA zn>T42m?N-1(2bbPzRF8Xg%pWrFHAh8w2`hSF$ALa55vTYMG1!l3F4_pM4VFW2d^id zBwwl!a(Fh2sl_&gT4wp{FI96^EM+1)HF800JK5 zpP~TkuhXD%hvd!911m28>(KiPbkn+u2v>@Zovo*~IC|(p8=J(k%IYM>^XvZgp;1Ep z%kRja=6o8}--!F@55@Kf;RI4QqqRaV!qkaml#1p%a*Y!SHK&@PY`};paI!YPgAu8Z zy5!pdkTx9r(HKPe*_K=a>`M?{GzUGbkk!*P#Z_|jFA=T$k)EFb#s!)E%ld*mN~)=U zPD##7ZXOEYiXCrn*s5sLsN{w38^@~I6c%Ql6G&AJDb37mo`?#z0}lrxiRa)RKaSQO zj)%;$&OxuScE4@q_K<#o6s#=~H)SkC&Kl+T3u_FtL_geLZd+EuG$py3x=N_3vdOnq zLkW$!=WHD!_%r?hekAK>8YQYJ7D>VaCGf?(=uZzhEy75+Fa#@WIk;1`@%EECS=%}T zSv&}SX|T`LmgSib7BU@-GV*!8@8+(2SiV+2V>iRpw)zg0{i#n2gT7=IU$@wouT8XS zR)nvg?C*bgX6m2NJ8c|Fm}psIWO?d`9Qj5P^YhIKyS#A~Ku5$Aure4XQ|JSH~kjSZcoG^H;$40N0> znG{<2P40fI0c4v8{*bXS9e##lqyfOfC>rS_!NLt4Saaxnab zM65&z621XIDz=7pgMRSq2&@Qqizf}g*&woYmHkR!> z1u+aZ0oZ>wmJC*gWf{ zF{rm}HPwWuDf88p4LIVx{{Ziqmw0B@4Nff_x2C?86rO`p442=9=S7M7#v~shTlF`^5c%vK8D^gnG^8-Xv!1T_A0k!X#wO-bfs22 zK-*cEv&6gBTu|joQS_m^HbvAIJaZa|G7RSYwhNM#1vJ}2!zO z0p<(*b-8z-{VICef@{}DD6J_FXmr|5>}dog9^C@E)f?PtKBIYS zkFC4YbMses*Ru*vy`sMN-(81Q$06->uXKs4d<{2YKabOIQrH+C;WNnM#$trVa}nC` zN(J}?LZjbsBZ}X!&3cW%6X&80WYHR!0-#HYEV|JnX9}E|vK7SIgyxWtgF;UW#f;g3 ze7a5478|M()df5hUFMY8k~2&qAIjutvC!FFE#!FCIKvmLTkwhIw1zlPMslP$5`IbCfqO>~M`eSG>0iGZh>>KeuMdTvCOh0hjOv z*VOA(X+}{;2Y{6crR)c)LJZ#)UyucvRw%ceA=|1A7IPMTrSfghvv4?}l#+<}T>hI` z{$R>u01`GdQvifcFLWRcTx`6G6Y`o}pk;sTrF0OQXy^LL$)_T8cONFuM^aW=5fpDTE#z@o9J%A8bJ zJCmYI^-Asb^zgg2J4XLHL+7&vtF+w-c`+pfEqP+5KDMePsZgEyO7t%bt1$+e8KcO* zdUF?->&+vuoKWg$W0l6c+}((W<%>uWhwl8=Ipt(iZ2|nlFis;;>!Vw>0BLrp4YP4A z&!v*Ta&;)q<pHM$I8)GPXCaI43{DIV*{?ys$j3!q$}ty<2wV+7c~M-U3w3Kh9ml`k1IYFkf~NJ%K=_1~gTYLrw)~vGv3<)( z)|l(oZRoaARy}9V0oV4NxIg^mF~jK#1`G3W_y38a@5;Q%8J5ZRP(c(fa6;Nr?XAc%K5|eyhtf-1bDQW^I!zqI5eV!EQgWHXU>; z43G+8q4TWRgMSL)0#5d_X*wEiU(4xVrM5B{c9M83vom=ubKkmA<@F)-Y;1VX;5-+k*JcW_ zD?f^DbsGa6l5sFvxwOkzd2tsCA3*AvWLpVhm2M( zyLIta3C#%UNNQij4;wyAkutxh-1~_$yQjL}RDHshfSmZx*Ig~=c<-4u2uFXr47Aj% zl*UCerT{*bAJ!Sq>uPA(@E|uD;zSj}OM$~M34~GwBLHUlWG2F<-GN=`!hL^!(f1nR zdEbc6w!b}mh&P}&J>hF@NeUE9a@DF};mkv4w!IN~D6B~XW0am#o0C626TPVj0UqT$ zb{#>)fIaKOuqPUy!d}hxxMS#^1!Gf#IdIY<^SfZasKnJ>7IQ5CVQdg`lo95>7a(Mx zeM2Aa_A%*Nz8jA4R0FQH_LCLisiz=F>z+P*JC|52do6P0Qz=0HIzun5b9#aJHH?~Y z4~2LBbAR((geON7YTM$JWJ*{)lbBX*9%71RXmkRr%D9<3GtuV_Dw(6%c?|-$;@18@&z-G#i=+&le^ z0ttpmEQx8r^akK3x^Q5-R{KQcupD>&01TTOOwjWFycJ-tzbJj_CkRF%N|-p)8^=1i zRmL~jQT&eLvBg zrfdZBOE2~rkJ;>fLUbk1rnbr4SVjVNpN^#03oVJwX5iPh{aAxMm=Ax2#WCzR0m8ML z$hMdA%~9cSE;gD@WE3x1TT6Nl6Xt`xDCnn9CBq#!@qpfUur?{eJaoYdGO`nMb5+MP z0gQ6fFs1g5#gugmG8mHG!Rbnv2R59Nw~KYSNLP{Rkuv)r-@ z>XN`#8*0W+kj<8mhfz_E+Rlc%F` zM5=cU_3@c}Ky&?jos%#2>$P;mn+yj20ZTm94f60L_1dBM+uN*Fb{u8 zON(7JlKWYxo-4~fHbl71zeW{E^+D!RHe71GE0B{90);2|>#lD(L_qOh~meN`tu4vM*a$C5HX@j0HyB+Qcb z-JsntbnzyXPqr7a@>87VWrC8a>Wqu79@zdBA^PBQjg0dCg}nb)&b5ETy!mE2@h(Z6Q5bV>_yWbKvHpk0#>(%T&3 zDePxse$CJ$wACX<;F#+Txf}V#!;T8~H;`;TxqgqCH|Naw#YYW%=`Jd2*~)g9;Le)X zS9gAw;u|MFtl>WsCQw)Le}rgOi$w&m|71-7 zXTzUBYbcT+4b&0wJeIOLzSTORga&Qj!|; zx$aj?_|Nc0GHmQrU)fM&O2!a5teZ*ObdZa(0L2v(V{&Ib>u|q}JjVPObo!~{9;8B; z6Ed|l8GIQ6g>e}NE7k}ah*|J#_oA2_`BV*a*yh%p8F= z`-XHm<|(0&f+e0YyBwT-^$Hjcwv>1iW_crQXfo>#7=r8@s5%)LCwOk)uKx<2S@M|y zjh^OPf<%3GSO@x^D?BeuJbI~o!5%RB+CY8)?FWlC%0WGC#3j2W07R+B4L_v3iH8z4u zuiRKz0eu`C0j#MXv)iYpVn!wDG!6okLYi;$4xpT%YUqn(LRltVB`Tq}dn4$eAN&^h zO>=s*4lOmCu*NY6~t++znk}Ot}k>ZGdR( z{!PF1IRt>45Ip#!k(w7?G!ItcTeY!yFh_7bWah4kgoI-Ct`4U$~Fc0u?kcVkn1GVF;?E zUmV0vY47fNp#`gIc>d?{f!RRue3Uqj{DD+pW4jH+s?IF#_!<|pCF7IgHhB*#8o&>O( zAdb>Vs^s|+{dveBffI2guPESIXQOxH)MvQ747~AXuiMuDVmsNov3}1x1DX43D!*~+ zAXes87M&_Q_j9yga6wUzYta7vCf?=v= z^k6=d#`oe3sSLv#=c>-|2DBr^1|bXpBbF$&v65}Cy7=d&CmZ3u%nxmiw859M@e|+I z8`E1WzS@)JdUj0-6NbNkCa8a93m1mdMPoDwn2x=ULIc*8yKLHx=5?%;+%@mDJRZjeNxHUPloZUe6iAFOJu~ z@y&zTKfPzNdjS+0BmTsKA*GRk&_ zXpFfAqU0CAxW}>tJ3|?N5TQkCQ#EM4OH=+SLB(ulAo(Yyg1nLL_a!TLX324c^Bybu;sRt_ z7b*+UNNefgu@|TTxv?3gmC!*%m*OtS3b&{A-k+g=3c`;eR+j3*l@GRI=r&TcSbmnt zf-#oI1|5$1YG%hG49ikFaohC}wv16*n73uB29}{pE|CWyOE)mlq1tIsx*h||k)oI} zLp~tau`ouYYKLY*)y_ElZ{s%}&q#3_Jd=x5`A7?se?6-_%f%H1W8xlfuZ^|@?xscZ z<|WFPEL@xeqeSarl^9DxUqrSoE&+UC~Mo~tyyCt7IuUse5;7(@}ezODpj zBF_cx4P}G{{Xmr3(kTRvdKRbL^hoO%w^1Fr-2P zpyyrAkeq*!aCEE0a!lig#8Y9Xd?bjACV7)zfhDt5Vl$@oW9Xr<3*s>K9kbln&04kk z1t3X=^~o#{Ag;7#T=sW(t(E@%Iq(BH(S=F%Cla|?{NJN2c8&NvVqIm4_`erjE#*?E zDV;S?5B{S&NwQpC!3FsF^j)H*S2tB6@};1gE|K%Z%NvB>AFRr@su#~Wk$d}gU-}XH z6J6e=`r@fO#*OE)>(uy}Hv+>%?1Q?;5rDm5+rVw>pAs^6#XF~C@iJR-_y=Z#*WW5D zg?7JH+5(|-=>j4npeJrxp@Z@_29X>qxJ`CbZl55(*Y2m|4BSI8r&<2sJ}DN|*C5WH z6gih1#B%(YDmq);5yqseVPahHtct#Q7#`m33dG*3JVx&5+F-3at(DpcMr>`;B?TaW zRvgl=z0SE=r#;V)x3@jcEu{{%I-P#+$M%2LG(E-I0<2olo-S(`&tBHC@p`w^o%}%! zXxC%9JQ`*+VHO#B+bIXW0;7mx`(11&#EkA{wP;Cev3y1;(O2Gf=`2@sObHxb=bB&{ zmTiuX$}Jba(!*`IJ*BFJ5FNEb6#$kPhh(C0OfQ+XZT!Gv$D+-rGY8#-w@cqU1~AyR zf>*{m z{@yg7LK39iZv{5#MvbnpRweQ*?;3iQs}iX9WUk~b>I6p^`bBnGC9tUEGP|EKIm~Tw zrAaXzjoK8cfCz4U~o-{`Q?yE#@Ki*x(O9v1lc4X`W|7L z8drJP{-D^}Z;qhw|25lonHQ1cfom6$)2jBVrcIdt@-YC6!+UO#ff*J6h1HU3|qvmw+6Bp#_aAG8Rj+v%3NR3G{n_`a?yuE zVFIK)rQTv5Id1ZBL`l|0#L1_l+0qAR;fyOHl%176Y(U&`UbONYXU+S8!}H`Mlq?nOTej zx3P;Cb&}gIdUIW2SK!yecAED5z1jF?52~E(2?6PAClzoMfBHeaDXzPOQuVmrDF}JQ z&>6bYn7@$=&+Y7>+47?xE?yUy9@8o=NfF{r^Bs2ZIaoWLnu%~@ibavCWxQ6(sJ9jG7 z7C^5I#Ke$2oFEk#4DX!{zj^Y4mM1Vk-psrPp?L$xTF-`Ol}!pwy$-{tUT-bWxP~iG zxs>S>ejb_dr|lj691QF%!T&C42JbqI0zsKEqG-1*Fe8^gbRG}AC2V$ZUjWo zy7&8OMxBA2HOn?uXXC$jKfgpC;MCEi4L01r)t%p+$Lu9f@A&6TpHCLujLPcf%}6)B z+@Eg)o5o2z>U_s%VTx{Ew&(FQQ|908P%>+4na|{z*};L-M-(vMbK+`Q0e{PYx!J@h z+h%$+l}{i<8^0dgr}Eq>B{~M!Nqu31zmwKgJoRU3V$ceWTHlw8?vy*GfwL!nrLD9z ztFL93)R?8;#@J#4hMNjO{+ufK>eA`i(q+mcCpaEtm4h*Re5nRwAJOU$Xr*^I=9=Hp zCjpwxpF)PuBa#IK-&=VJ0R~HgHJNEhH;a0&Evm^{(3HG3&x^e7H%b1-ICWG5HiG|Rx>9%2ClG@>yXAPQSYGyyU- z3}e%@8Ba>>ZK_iB#XGtUJIA|~scxN6 zZ}av~VNND2VF~mB<9@STS{K;*>$LuMwf5TKe;)N;UIxdzRwI%0Jlo)pm^^{Zds&(V zGa18~YvwVQGw6#XS4O-;CcG1@aQlNSpP7 zrN(QHB!HjOB!)z^^yW5G&`?#(AefsN+x!sN9@?j_WQFm2nuUQrEP{n6p z{tw;O2IZxEuAV#lnK2IK?Y@(uuz?CUXmKX!gB#B|^4Y-$IE&Tn)07SV1w&OGI}UH* zX#U@VCt#%_0vIn4ISE&coy&yHg3sL4gw>Rf!`y<$l#7jrixBzZn^$_5N(Y z6UTEQu|^tXXZ%h79)_eHYE%!`RnL@EXa@z58amHI7BWVx4WjY>t#KV;w+qp`3-h_} zR!9KZ@7IpZ4I4&)3dysF4H-)0I7kE=tO6VA92L}sO4mv!L<>(%hHpxWy+0IKtG2(# zrY-`mE{3HpPQE0 z6?Tyoo;f|lB|TwI=-ev;MpxoOPa;)Y;-ewz#SYD@eD+QQJ)*^Oc)sevfKXbOgz8QG zJo1pzW?B~HRD(s=WH%kd@x#s_8$nklulQWdPQEioH*a{kw1uM9jH#{tyc)qF7w?WF pE>?Eq|MdWe|BReWZT}U(nYg-pyINSnb8z#r@xfD3Nh(Xh|3AI(A;bUx diff --git a/equational_theories/Basic.lean b/equational_theories/Basic.lean index d2728607..219ef672 100644 --- a/equational_theories/Basic.lean +++ b/equational_theories/Basic.lean @@ -243,3 +243,9 @@ theorem Equation4512_not_implies_Equation42 : ∃ (G: Type) (_: Magma G), Equati replace h := h 0 0 1 dsimp [hG] at h linarith + +theorem Equation387_not_implies_Equation42 : ∃ (G: Type) (_: Magma G), Equation387 G ∧ ¬ Equation42 G := by + sorry + +theorem Equation43_not_implies_Equation387 : ∃ (G: Type) (_: Magma G), Equation387 G ∧ ¬ Equation42 G := by + sorry