anticommit desired contents

[topbloke-formulae.git] / article.tex

diff --git a/article.tex b/article.tex
index 20ab3613b294a18dd8bf09d8f49e4f7bc9ab8700..4c7f22cbc50446b5a2997c39107e60932727085c 100644 (file)
--- a/article.tex
+++ b/article.tex
@@ -55,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}}
@@ -154,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
@@ -263,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
@@ -399,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}
@@ -422,19 +423,37 @@ Merge Results applies. $\qed$
 
 \subsection{Desired Contents}
 
-\[ $D \isin C \equiv [ D \not\in \pry \land D \isin L$ ] \lor D = C \]
+\[ 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 \not\le C$:}
+\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$:}
 
-\subsubsection{For $D \in R^+$:}
-By Currently Included, 
+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}
 
@@ -450,7 +469,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}