X-Git-Url: http://www.chiark.greenend.org.uk/ucgi/~ian/git?p=topbloke-formulae.git;a=blobdiff_plain;f=article.tex;h=1cf0e76e61e8b48c3eb083eafdcf590929e74891;hp=d9689c228d88ea26770ab65d88d85f4b192a9c9d;hb=0b0cb39339f1f3c4fd43e8dbfa2efd3f5b5eddf2;hpb=1c388950414d09bff217345d1219eaed13df4806 diff --git a/article.tex b/article.tex index d9689c2..1cf0e76 100644 --- a/article.tex +++ b/article.tex @@ -1,5 +1,6 @@ \documentclass[a4paper,leqno]{strayman} \let\numberwithin=\notdef +\usepackage{amsmath} \usepackage{mathabx} \usepackage{stmaryrd} \usepackage{slashed} @@ -14,10 +15,8 @@ \newcommand{\has}{\sqsupseteq} \newcommand{\isin}{\sqsubseteq} -\newcommand{\nothaspatch}{{% - \declareslashed{}{\sslash}{-0.04}{0}{\sqSupset}\slashed{\sqSupset}}} -\newcommand{\notpatchisin}{{% - \declareslashed{}{\sslash}{-0.04}{0}{\sqSubset}\slashed{\sqSubset}}} +\newcommand{\nothaspatch}{\mathrel{\,\not\!\not\relax\haspatch}} +\newcommand{\notpatchisin}{\mathrel{\,\not\!\not\relax\patchisin}} \newcommand{\haspatch}{\sqSupset} \newcommand{\patchisin}{\sqSubset} @@ -36,11 +35,13 @@ \newcommand{\hasparents}{>_{\mkern-7.0mu _1}} \newcommand{\areparents}{<_{\mkern-14.0mu _1\mkern+5.0mu}} -\newcommand{\implies}{\Rightarrow} +\renewcommand{\implies}{\Rightarrow} \newcommand{\pancs}[2]{{\mathcal A} ( #1 , #2 ) } \newcommand{\pends}[2]{{\mathcal E} ( #1 , #2 ) } +\renewcommand{\land}{\wedge} + \begin{document} \section{Notation} @@ -74,11 +75,22 @@ where the context requires a set, in which case the statement is to be taken as applying to both $\py$ and $\pn$. All these sets are distinct. +\item[ $ \pancs{C}{\set P} $ ] +$ \{ A \; | \; A \le C \land A \in \set P \} $ +i.e. all the ancestors of $C$ +which are in $\set P$. + +\item[ $ \pends{C}{\set P} $ ] +$ \{ E \; | \; E \in \pancs{C}{\set P} + \land \mathop{\not\exists}_{A \in \pancs{C}{\set P}} + A \neq E \land E \le A \} $ +i.e. all $\le$-maximal commits in $\pancs{C}{\set P}$. + \end{basedescript} \section{Invariants} -$$ C \has D \implies C \ge D \eqno{No replay} $$ +\[ C \has D \implies C \ge D \tag*{\mbox{No replay:}} \] Unique base: \[ \mathop{\forall}_{C \in \py} \pends{C}{\pn} = \{ B \} \] @@ -88,6 +100,10 @@ $ C \haspatch \p $ $ C \nothaspatch \p $ +$ \p \patchisin C $ + +$ \p \notpatchisin C $ + $ \{ B \} \areparents C $ \end{document}