X-Git-Url: http://www.chiark.greenend.org.uk/ucgi/~ian/git?p=topbloke-formulae.git;a=blobdiff_plain;f=article.tex;h=4c5f6751682c83a13e478fdb11d64496abd1bd22;hp=1f7a59bd4018b2ed9aba33b8a46989dd24cb33c4;hb=1059b2343f8b2979915db881a067cd3307cdead2;hpb=ad024e0c6f90bfc35314f88d63e367309e48d57c diff --git a/article.tex b/article.tex index 1f7a59b..4c5f675 100644 --- a/article.tex +++ b/article.tex @@ -248,12 +248,12 @@ by the LHS. And $A \le A''$. $\eqn{Calculation Of Ends:}{ \bigforall_{C \hasparents \set A} \pendsof{C}{\set P} = - \Bigl\{ E \Big| + \left\{ E \Big| \Bigl[ \Largeexists_{A \in \set A} E \in \pendsof{A}{\set P} \Bigr] \land \Bigl[ \Largenexists_{B \in \set A} E \neq B \land E \le B \Bigr] - \Bigr\} + \right\} }$ XXX proof TBD. @@ -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} @@ -440,9 +449,9 @@ Merge commits $L$ and $R$ using merge base $M$ ($M < L, M < R$): \end{cases} }\] -\subsection{Merge Results} +\subsection{No Replay} -As above. +See No Replay for Merge Results. \subsection{Unique Base}