add some xxx's

[topbloke-formulae.git] / article.tex

diff --git a/article.tex b/article.tex
index 4c5f6751682c83a13e478fdb11d64496abd1bd22..023a18a9340c7670e3ee89011177eb9010165e69 100644 (file)
--- a/article.tex
+++ b/article.tex
@@ -10,6 +10,8 @@
 
 \renewcommand{\ge}{\geqslant}
 \renewcommand{\le}{\leqslant}
+\newcommand{\nge}{\ngeqslant}
+\newcommand{\nle}{\nleqslant}
 
 \newcommand{\has}{\sqsupseteq}
 \newcommand{\isin}{\sqsubseteq}
@@ -53,7 +55,8 @@
 \newcommand{\pancsof}[2]{\pancs ( #1 , #2 ) }
 \newcommand{\pendsof}[2]{\pends ( #1 , #2 ) }
 
-\newcommand{\merge}[4]{{\mathcal M}(#1,#2,#3,#4)}
+\newcommand{\merge}{{\mathcal M}}
+\newcommand{\mergeof}[4]{\merge(#1,#2,#3,#4)}
 %\newcommand{\merge}[4]{{#2 {{\frac{ #1 }{ #3 } #4}}}}
 
 \newcommand{\patch}{{\mathcal P}}
@@ -152,7 +155,7 @@ patch is applied to a non-Topbloke branch and then bubbles back to
 the Topbloke patch itself, we hope that git's merge algorithm will
 DTRT or that the user will no longer care about the Topbloke patch.
 
-\item[ $\displaystyle \merge{C}{L}{M}{R} $ ]
+\item[ $\displaystyle \mergeof{C}{L}{M}{R} $ ]
 The contents of a git merge result:
 
 $\displaystyle D \isin C \equiv
@@ -261,7 +264,7 @@ XXX proof TBD.
 
 If we are constructing $C$, given
 \gathbegin
-  \merge{C}{L}{M}{R}
+  \mergeof{C}{L}{M}{R}
 \gathnext
   L \le C
 \gathnext
@@ -397,7 +400,7 @@ Used for removing a branch dependency.
 \gathnext
  \patchof{C} = \patchof{L}
 \gathnext
- \merge{C}{L}{R^+}{R^-}
+ \mergeof{C}{L}{R^+}{R^-}
 \end{gather}
 
 \subsection{Conditions}
@@ -408,10 +411,9 @@ Used for removing a branch dependency.
 \[ \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$.
+\[ \eqn{ Not Self }{
+ L \not\in \{ R^+ \}
+}\]
 
 \subsection{No Replay}
 
@@ -419,12 +421,48 @@ 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{Desired Contents}
+
+\[ D \isin C \equiv [ D \notin \pry \land D \isin L ] \lor D = C \]
+{\it Proof.}
+
+\subsubsection{For $D = C$:}
+
+Trivially $D \isin C$.  OK.
+
+\subsubsection{For $D \neq C, D \not\le L$:}
+
+By No Replay $D \not\isin L$.  Also $D \not\le R^-$ hence
+$D \not\isin R^-$.  Thus $D \not\isin C$.  OK.
+
+\subsubsection{For $D \neq C, D \le L, D \in \pry$:}
+
+By Currently Included, $D \isin L$.
+
+By Tip Self Inpatch, $D \isin R^+ \equiv D \le R^+$, but by
+by Unique Tip, $D \le R^+ \equiv D \le L$.  
+So $D \isin R^+$.
+
+By Base Acyclic, $D \not\isin R^-$.
+
+Apply $\merge$: $D \not\isin C$.  OK.
+
+\subsubsection{For $D \neq C, D \le L, D \notin \pry$:}
+
+By Tip Contents for $R^+$, $D \isin R^+ \equiv D \isin R^-$.
+
+Apply $\merge$: $D \isin C \equiv D \isin L$.  OK.
+
+$\qed$
+
 \subsection{Unique Base}
 
 Need to consider only $C \in \py$, ie $L \in \py$.
 
 xxx tbd
 
+xxx need to finish anticommit
+
 \section{Merge}
 
 Merge commits $L$ and $R$ using merge base $M$ ($M < L, M < R$):
@@ -433,7 +471,7 @@ Merge commits $L$ and $R$ using merge base $M$ ($M < L, M < R$):
 \gathnext
  \patchof{C} = \patchof{L}
 \gathnext
- \merge{C}{L}{M}{R}
+ \mergeof{C}{L}{M}{R}
 \end{gather}
 
 \subsection{Conditions}
@@ -487,4 +525,10 @@ That is, $\baseof{C} = R$.
 
 $\qed$
 
+\subsection{Coherence and patch inclusion}
+
+xxx tbd
+
+xxx need to finish merge
+
 \end{document}