anticommit desired contents

[topbloke-formulae.git] / article.tex

diff --git a/article.tex b/article.tex
index 4c5f6751682c83a13e478fdb11d64496abd1bd22..4c7f22cbc50446b5a2997c39107e60932727085c 100644 (file)
--- a/article.tex
+++ b/article.tex
@@ -10,6 +10,8 @@
 
 \renewcommand{\ge}{\geqslant}
 \renewcommand{\le}{\leqslant}
 
 \renewcommand{\ge}{\geqslant}
 \renewcommand{\le}{\leqslant}

+\newcommand{\nge}{\ngeqslant}
+\newcommand{\nle}{\nleqslant}

 
 \newcommand{\has}{\sqsupseteq}
 \newcommand{\isin}{\sqsubseteq}
 
 \newcommand{\has}{\sqsupseteq}
 \newcommand{\isin}{\sqsubseteq}


@@ -53,7 +55,8 @@
 \newcommand{\pancsof}[2]{\pancs ( #1 , #2 ) }
 \newcommand{\pendsof}[2]{\pends ( #1 , #2 ) }
 
 \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}}
 %\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.
 
 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
 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
 
 If we are constructing $C$, given
 \gathbegin

-  \merge{C}{L}{M}{R}
+  \mergeof{C}{L}{M}{R}

 \gathnext
   L \le C
 \gathnext
 \gathnext
   L \le C
 \gathnext


@@ -397,7 +400,7 @@ Used for removing a branch dependency.
 \gathnext
  \patchof{C} = \patchof{L}
 \gathnext
 \gathnext
  \patchof{C} = \patchof{L}
 \gathnext

- \merge{C}{L}{R^+}{R^-}
+ \mergeof{C}{L}{R^+}{R^-}

 \end{gather}
 
 \subsection{Conditions}
 \end{gather}
 
 \subsection{Conditions}


@@ -408,10 +411,9 @@ Used for removing a branch dependency.
 \[ \eqn{ Currently Included }{
  L \haspatch \pry
 }\]
 \[ \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}
 
 
 \subsection{No Replay}
 


@@ -419,6 +421,40 @@ 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$
 
 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$.
 \subsection{Unique Base}
 
 Need to consider only $C \in \py$, ie $L \in \py$.


@@ -433,7 +469,7 @@ Merge commits $L$ and $R$ using merge base $M$ ($M < L, M < R$):
 \gathnext
  \patchof{C} = \patchof{L}
 \gathnext
 \gathnext
  \patchof{C} = \patchof{L}
 \gathnext

- \merge{C}{L}{M}{R}
+ \mergeof{C}{L}{M}{R}

 \end{gather}
 
 \subsection{Conditions}
 \end{gather}
 
 \subsection{Conditions}