From bba1bf255aa8a2cd0083e22ec1569158caaabbf5 Mon Sep 17 00:00:00 2001 From: polybeandip Date: Mon, 29 Jul 2024 12:13:40 -0400 Subject: [PATCH] Fix well-formedness (again!) --- pieo-trees/notes.pdf | Bin 153065 -> 153098 bytes pieo-trees/notes.tex | 10 +++++----- 2 files changed, 5 insertions(+), 5 deletions(-) diff --git a/pieo-trees/notes.pdf b/pieo-trees/notes.pdf index 7ee10696e0644b2118c64e92176722dc287f9834..b597b0e5adcfcbcdd5a160ae34d105c96b9bb8d8 100644 GIT binary patch delta 3637 zcmV-54$ATAs|kv%39xGq0y#C4u|6n&-C0|28dng0=T~gs7Rh^h?w4BbLzK8mRJCb~ zluEX%(y+v&7;Ml8ipu5`Q7a5_j#cs> zK{4m?HKnY0_p$tmjx=#b*wQP1#yf>bCj)!KTN6%Y)DrrpRMmE{BHGlRdHed+kCUryjJ&pI-QRbBl>*61!1-}?;cU7h=lup>~})oNh}S( z2k?VD4b+e{D1|PNv%I^Q=^hr`DL*W{lJ33IQRW6}947*<-ID4HM{UjPRhDj6(`8RI z1XQ-DEqj21bn$kaSP`F(6Q(s9ARgq;=S0XpJwmo!^Nd)^A|?n|df$mu+4fy+yhXGb zVyNm^&RI|xj8F--3!(vkfOENDF(?At0g55e7gQ5;WnGFjM;aoky$`+MD3< zcG`xoAhiWCt`%;qX-O)YuC?0$pn+3&Oam~dZvb#h5iiO(S{8PHW!DHl=1u_;F<<+4 zo>tU7WCTk9C_8C84Zj1@!qvVzD`GKASL>`gHUtAm7~?wm5GEyIwD#Tw zk}yz}(qVl)Fnp)4KcKd2p*yxO=B1~z;`4NNn{Lu=@i1E#53}2}craftmupYf9v7<* z#iPxqWx6ex)~m^X=walYOd|j#1$gXCq#<0=$mspu=<0?>Gx+jNM8S(Tddx-dA_-ue z)2LG)iT_wUhT;4%VI1{x2{RRDnYv$>22xr}QX zc10Hg9S)#>Ob%}83Bo51ws{97)?|BMm>fFisC}fruZydmE?(MPw({i?qhfx0va{1@ z&jE!$fa9~$3W|aXH#(mLDyeJA6^2g%5)7bJSi|GYo{B`N?!_f>mWcu=oN%DbSsh+H zY|qSrDu5-&1_p`j+h!%)059M!-)HHvIwrSiPO~0PzW;$1BPCk8;F&NRD-42uLb z%7(>ccqe7U2ZMYlSl@$zEM6l#oqOQboxqB2U~6^ve_|#9n5w404-YGqlJ3MHnCzyQ z>a%2q&P>(}cg@RbHpM)`L5L5wWA3q*7m#bvQe~1D=#B$wRRy>|~)cK^N-|3DeaK zYrJrOc*8utoI%q)Vbd76z}HD7vipj|6*Wuz=#JS7 zK%j;sKWh=H+yONynw9@q%nH6S9kY0a!X+iP*|(gKxc*PP9Aw%4LKYhOD2xCJRFkaM zuHFTFP$Ao$LNr>cyj~asb(90 z-ba(=@vZk5n%u$u-Ob}LU|QezR1AaJ$cb*r^s@~G;tIKPXQAV#!0^f^K$;am&54ob z6bbl%W`-|`T{neXaK}w&#Z4dKqJ9U9Z8Bt=pnn;0&57hi@#4+F0aZXD&@P~2zRS^> zoh--p;4DxiL5T*aZckosH|zC06f71hJev3XhZg= z;UP4CQoJ?|j?|CKwPG`fA3Xt?^Ijfi|GB&DE8b%=5>vGSHyIdFr4%m*89BN#JYErT zJ85FY(HCePq#c(70;)fuHYA9R;Ug#HO{)#{Ax@6(8smeQT)J(Pv7g8cJzQ z8*)r1tyVW47@_gCH0=i&*`o}gy`%@Foh`C|{blJ6$$gn=mn=rxBp)P;HQ5H-C+eVD z{MeE)IZD_zM&?Vg(fj|GEVh}s_GhTgEcVE3)xvJJYW{KAs`T=dp0zp*eG03+qH8Z& z?NeB-$IMoqN+o8PblFzG(F2ZI4}pBO$>kG9q682!_%$aI8@P0kk>jIusg}lwGLJxi z(epk=_@VtGcZE|bBVv~HkrBz>RxgJb`2rZ7P=;b6`I0&YL@Qbe^3>HaU4$d1ZxU0a zavu1II7HRs*#nGxf%M&ni8$&i3e#1XhyamEPNpZPC-X?$_wEzm*R$kDA%E?qZoM$Am!p+q zqPvLJ|4EOwDaG~F4KT%NiXKiK^p);K{+&sa#4=4AZ>^v4H`=z#Uvft_RakBLswqAIBG1rYg4r3a|Jd9-+ z>o5-UWSA#@7-bm4Fb?aq$B0dk`8WTSQ+r($z)Z^;lJ6SLU|Vz7!7aRx`=! ztMuHcsEA%)y>;k85xUC#j5S31&2}Rz9=Vt*w zOD4j=m7uSbBk{YRiRV9_AGM$ZQq&oh0meXh;1WkHUOk&zX0PcMbn3pWJFZ)4NT|Y0xxTz7V2Ol7bciCF-|kvgI(WGcn%!z<i~ZEkl9u`?lwHbfhu4bg^ZLxiLrATAM?=tX^Qi?3sY zqT5nMO#NL_$#Ji_tHvCBkuPtYo<~6m;ZMuxqtPT#@zqb z#x(A^hI#W`<5HsOO(OkJ&*hgBtzQxy9}@*GbpA|qzf1H!i1*F_VTy)CL!u$kkZ4FW zBpMP8iH1Z&<+RIG7rT@RsZ2R#$|+M$IsL<$_?>Q39xGq0yZ*}(JLu`S;=l2M-aX1D<-!gpy~9!L~ssUHea)+kCoz%D3A< zyga}Wr@8j}87E4KBx9C1Uh99BUsEPmi(;`}jWQu^$_XQp7GZi?3?+;U_@#XQa`DLv z!%3=tk|tD{MrKw^^tD*Rbn`nOW!%{GvJwjpV+KrijUX9iQi{gr98oI_agH_e??Ex= z={2RSdiTD5L?@a!BWxWNFdt5x*_tcW&kWM02`{?mBmc)H1R zM4^<#TH6R;Q$>+DNEO2F{2E;_ScVOgL=(bkSXN8F`< zBL`*7Fv4U4*@X17CI^_+lDF!9%qO!^X2ehoxFF27=G`Ic6p`T1{vZT@k;KXXVgL`6 zWuT5JgIeeba+VJlGx1@8Pvv2uOM1|ylgtg&I8Fq(-IE$hM{CWCRgrI2ljT4*1a!7& zE&Bis>C){evm(71WlU={K|H9R&&iN|c!q4h=NYk-B}@>m^u80RvVC7|x<#}ZVyKEN z=PYOpMyLea1L62n**8*G9}D!LK2I}Ko(Q+LWVFpobCN-r0Gby6)0N3`pN@5=}Q zqnNGzJI^LCpoJ{)HjVdWLkb+Qxrm2<1lYp0p*ydPoI)b<)w*a74zU4Lnl_eyAmstD zWF0oe1Jib<_y^QF-ObDMs%jRqI+R8Ac`}{nn|xbW(YpGwnCI0Ov-NUW#_@i!0=M2( z-)=rG^KC_~o{!IeKAidLq6wf7)S7fA(U1~pWb*d*?CORlQ~2>^LLpQ(xi3X;6A5mX zylI*IdiHb8A%j+JbWsh+&-cg6p3ZuX8rJgAux1BFfdjaN-en322TKVfnv2I`U9zz_b2`1ing`A^l=tH_NERPhKo1DD`0`U4DWDMW zxHTm~J_7K7QNm6o_aGi1D{)YcUkdTQ9v=qsBA{f1_KOq%pdBVJh#i6$XCuBMLcZc; zE3nvB3X!>g-^}A2CfCqBX4FSW#846fr&W5NJ^RLN;iqf$RsLzQEw;!3P#L`~>oe{c zARD%8`|ZcK^Jbh+it}cmm(i(b|8j|eqUbOGGh|JuSPzJ?n!r*Ng1FJ;qR>cPQ?4*H z3vlBImW7Q+&g_w-O2vLj;w%#tYB=F{OlNiIS2(MGfs+G5Id)`4kbO5RVCf=t4X6I-VX$marvmol2*wS?LTXd56!blF~K6jL5Lr1$7wha zdK}z;HP(nUSxvD?3fm!<|M~53HwM1k84iW`TE=$QvO`lKIB;*zN2|S)(Ch#s%zL7{ zV6euSp-u;s5Z&y1fpJ;~HKIFin0cr1ixt!1!Qs66tNBSW$EFSgC*;@2X`tl1T~$|@ zQI>GkHrw6D?R#4VD`dTQ76^( z4)K}ReB2Rw$SOOW-W3^@w2E&X)g4?1I`k(4Gncz!kJ7Aa--h=|jLD*q&yn zJ&(A`#E4Z7XiivN4(-0*5By)!jU0-?9*-};3aGq2UD++J>$`!%VveYe@imoI)&#nL zpDGZSkJ>!`w(IETIXEaH_U!Yw%br8BQ0`TI_FUuLeYsE|8?Wrsx5o`_bQ9}o$CK*C zAA&cufWn}0Lu276(SafHh^~y{c%0tn@VJKEQMiC@zuv6Zvrw>F?>Fy~>dh}Z5Fz}? zYfl+JeHMX&p?!;>>P<(Xt|=9Pc=P%Qe0=r~d(tR6voaQJIs-8|IkTZqYXpB;0z+s zLoavk#Voxf#Xl|6`R-?1N@LoPV>)TIy79mWjjyF?Kgh@)WdQ9ZJt*yLk?nskOLs`_%S^ju zG1?~iAX%)*HsC%{2i4-omW;_!!nQFoUy6<1|G#9h&CInwLv3cUM`o)QcC%IUkIPo2 zm#6fs)nVvUSnU;Ed(mp2!fHKcw(?XeF~g+GwgQeGaLjrL9m?D+)z(>R(svgfCVB`y=?>wm7M!9lgFuZIaG~665Jo_*-owP6^T#J1f>LVx25OXS^~Hd%dQ1SSFuL$L zhoJf{>`y z!t0B!hNmgH_=SD?E^!nU5bQ(=4@-{p_3;0 zaw3$fbT;}y5G9%e-34H9#ApCAvC09LIAZbY*)&>vO}C&^_pJtfmVPlqq2j!p#vH!s zD+T@Zso6}`qc126c}xnyanA|%(TmrRJe%paNzR7uTOmrEtVa|2CjUe(;ZwgS+Lxl= zXKCUhbyQoUJOm{E2TWBbvy<_M6N7SDw{lql|MmwoF*7kYG&z@ePy!qWG%+(VH#9l7 zn@|E}0#PzIHZem*I5agiH#smfG&4d*GC?#sI5#&lG(<&0LNq=gJTf;nF+)W-G&MCh zIWRLcGeSl(K{PoyH#ajhL`6bEG(KGlFHB`_XLM*FHZeGtQBwjde>qQ-Q51*qb4Fhg z1xH*EML|GO7DZ7(_H96MV-Zx`mBd7QYD@D^Tw@GKVq=W0iG^Rl#74h>h1(afna08d z?{jQ^Idk84?hN;R7&Cjck~7mmXoEwE%-kl&jj5cqIVOi3>|*T_(<)dEyiFIGGFSuS ztX*I#fwfQy>!8NXfAaAe>!FOBPs0f~$=U{{GjNWVdDsXQu!##3Oq-b|nYJ)ZF>QrP z*v8sfrYhLZ%Tr7{pc;0vHVv)3+zYjC`Puk>yP*#1p#k=AGk;*V5B5V7G(!u-RtJF7 z&5lDCbU>q9WkYPwv1f;&9ge_JI0oI&1HI4({V)Ip7=>Zze{`$si%kb%2*!Xj&1NB< zM?9$WFyhv-81IM^k8|NEWE^`Irxs@)=Nv~Ir^{JokwCO@8Lq%pxCYnZ2Hb>Oa2w`1 zIzCb)rO0B&t$!)jC`@!Ex)L>snpEPs-q&#p`G{y#W@e995>MbMJcGrEI@*nfC`Xi| ziga~}TVBF4e^}fcHAP6#5c!CF6!}n&q8y?TPgfO0;pI{bQozMWTB?-a7+?DH;+DiH1Z&q9M_cXh<|9 z8WIf^(=JmL>{2A8BIOh*r${-)^n*3=Io&dS-~ItQ`jeKI;Z*`33Nbk`3MC~)Peuyo CzPS(p diff --git a/pieo-trees/notes.tex b/pieo-trees/notes.tex index 81be05b..74b78af 100644 --- a/pieo-trees/notes.tex +++ b/pieo-trees/notes.tex @@ -231,7 +231,7 @@ \section{Well-Formedness} |\Leaf(p)|_f = |p|_f && |\Internal(qs, p)|_f = \sum_{i=1}^{|qs|} |qs[i]|_f \end{align*} - We say that $q \in \PIEOTree(t)$ is \emph{well-formed} w.r.t $f$, denoted $\vdash_f q$, if it adheres to the following rules. + We say $q \in \PIEOTree(t)$ is \emph{well-formed} w.r.t. $f$, denoted $\models_f q$, if it adheres to the following rules. \begin{align*} \axiom{} {\vdash_f \Leaf(p)} @@ -245,14 +245,14 @@ \section{Well-Formedness} } \end{align*} - We say $q$ is well-formed, denoted $\vdash q$, if there exists $f \in \mathcal F$ such that, for all $f^\prime \geq f$, $\vdash_{f^\prime} q$. + We say $q$ is $f$-well-formed, denoted $\vdash_f q$, if for all $f^\prime \geq f$, $\models_{f^\prime} q$. \end{dfn} \begin{thm} - Let $t \in \Topo$, $\pkt \in \Pkt$, $d \in \Data$, $f \in \mathcal F$, and $q \in \PIEOTree(t)$ such that $\vdash q$. + Let $t \in \Topo$, $\pkt \in \Pkt$, $d \in \Data$, $f,f^\prime \in \mathcal F$, and $q \in \PIEOTree(t)$ such that $\vdash_f q$. \begin{enumerate} - \item If $pt \in \Path(t)$, then $\push(q, \pkt, d, pt)$ is well-defined and $\vdash \push(q, \pkt, d, pt)$. - \item If $|q|_f > 0$, then $\pop(q, f)$ is well-defined and $\vdash q^\prime$, where $\pop(q, f) = (\pkt, q^\prime)$. + \item If $pt \in \Path(t)$, then $\push(q, \pkt, d, pt)$ is well-defined and $\vdash_f \push(q, \pkt, d, pt)$. + \item If $|q|_{f^\prime} > 0$ and $f^\prime \geq f$, then $\pop(q, f^{\prime})$ is well-defined and $\vdash_{f^\prime} q^\prime$, where $\pop(q, f^{\prime}) = (\pkt, q^\prime)$. \end{enumerate} \end{thm}