From abaf9e52109447fda8609b7d7748ede9ad48ec15 Mon Sep 17 00:00:00 2001 From: Ian Jackson Date: Mon, 5 Mar 2012 19:51:09 +0000 Subject: [PATCH] wip anticommit --- article.tex | 19 ++++++++++++++----- 1 file changed, 14 insertions(+), 5 deletions(-) diff --git a/article.tex b/article.tex index 1f7a59b..be6d475 100644 --- a/article.tex +++ b/article.tex @@ -389,7 +389,7 @@ $D \isin C \equiv D \isin A \equiv D \le A \equiv D \le C$. $\qed$ \section{Anticommit} Given $L, R^+, R^-$ where -$\patchof{R^+} = \pry, \patchof{R^-} = \prn$. +$R^+ \in \pry, R^- = \baseof{R^+}$. Construct $C$ which has $\pr$ removed. Used for removing a branch dependency. \gathbegin @@ -405,16 +405,25 @@ Used for removing a branch dependency. \[ \eqn{ Unique Tip }{ \pendsof{L}{\pry} = \{ R^+ \} }\] -\[ \eqn{ Correct Base }{ - \baseof{R^+} = R^- -}\] \[ \eqn{ Currently Included }{ L \haspatch \pry }\] +\subsection{Desired Contents} + +xxx need to prove $D \isin C \equiv D \not\in \pry \land D \isin L$. + +\subsection{No Replay} + +By Unique Tip, $R^+ \le L$. By definition of $\base$, $R^- \le R^+$ +so $R^- \le L$. So $R^+ \le C$ and $R^- \le C$ and No Replay for +Merge Results applies. $\qed$ + +\subsection{Unique Base} +Need to consider only $C \in \py$, ie $L \in \py$. -xxx want to prove $D \isin C \equiv D \not\in \pry \land D \isin L$. +xxx tbd \section{Merge} -- 2.30.2