From 751f225f809960b2b01ea91032b4e244fdb193ba Mon Sep 17 00:00:00 2001 From: Ian Jackson Date: Thu, 1 Mar 2012 01:37:48 +0000 Subject: [PATCH] haspatch --- article.tex | 35 +++++++++++++++++++++++++++++++---- 1 file changed, 31 insertions(+), 4 deletions(-) diff --git a/article.tex b/article.tex index 4160bd7..5cde60f 100644 --- a/article.tex +++ b/article.tex @@ -34,16 +34,20 @@ \newcommand{\areparents}{<_{\mkern-14.0mu _1\mkern+5.0mu}} \renewcommand{\implies}{\Rightarrow} +\renewcommand{\equiv}{\Leftrightarrow} +\renewcommand{\land}{\wedge} +\renewcommand{\lor}{\vee} \newcommand{\pancs}[2]{{\mathcal A} ( #1 , #2 ) } \newcommand{\pends}[2]{{\mathcal E} ( #1 , #2 ) } \newcommand{\patchof}[1]{{\mathcal P} ( #1 ) } - -\renewcommand{\land}{\wedge} +\newcommand{\baseof}[1]{{\mathcal B} ( #1 ) } \newcommand{\eqn}[2]{ #2 \tag*{\mbox{#1}} } +\newcommand{\bigforall}{\mathop{\hbox{\huge$\forall$}}} + \begin{document} \section{Notation} @@ -92,14 +96,37 @@ $ \{ E \; | \; E \in \pancs{C}{\set P} A \neq E \land E \le A \} $ i.e. all $\le$-maximal commits in $\pancs{C}{\set P}$. +\item[ $ \baseof{C} $ ] +$ \pends{C}{\pn} = \{ \baseof{C} \} $ where $ C \in \py $. +A partial function from commits to commits. +See ``unique base'', below. + +\item[ $ C \haspatch \p $ ] +$ \bigforall_{D \in \py} D \isin C \equiv D \le C $. +Informally, $C$ has the contents of $\p$. + +\item[ $ C \nothaspatch \p $ ] +$ \bigforall_{D \in \py} D \not\isin C $. +Informally, $C$ has none of the contents of $\p$. + \end{basedescript} \section{Invariants} \[ \eqn{No replay:}{ - C \has D \implies C \ge D } \] + C \has D \implies C \ge D +}\] \[\eqn{Unique base:}{ - \mathop{\forall}_{C \in \py} \pends{C}{\pn} = \{ B \} }\] + \bigforall_{C \in \py} \pends{C}{\pn} = \{ B \} +}\] +\[\eqn{Tip contents:}{ + \bigforall_{C \in \py} D \isin C \equiv + { D \isin \baseof{C} \lor \atop + (D \in \py \land D \le C) } +}\] +\[\eqn{Base non-circ:}{ + \bigforall_{B \in \pn} D \isin B \implies D \notin \py +}\] \section{Test more symbols} -- 2.30.2