$\displaystyle \bigforall_{D \in \py} D \not\isin C $.
~ Informally, $C$ has none of the contents of $\p$.
-Non-Topbloke commits are $\nothaspatch \p$ for all $\p$; if a Topbloke
+Non-Topbloke commits are $\nothaspatch \p$ for all $\p$. This
+includes commits on plain git branches made by applying a Topbloke
+patch. If a Topbloke
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 relevant Topbloke branches, we hope that
+if the user still cares about the Topbloke patch,
+git's merge algorithm will DTRT when trying to re-apply the changes.
\item[ $\displaystyle \mergeof{C}{L}{M}{R} $ ]
The contents of a git merge result:
\subsubsection{For $D \not\in \py, R \in \py$:}
-xxx up to here
+$D \neq C$.
-%D \in \py$:}
+By Tip Contents
+$D \isin L \equiv D \isin \baseof{L}$ and
+$D \isin R \equiv D \isin \baseof{R}$.
+If $\baseof{L} = M$, trivially $D \isin M \equiv D \isin \baseof{L}.$
+Whereas if $\baseof{L} = \baseof{M}$, by definition of $\base$,
+$\patchof{M} = \patchof{L} = \py$, so by Tip Contents of $M$,
+$D \isin M \equiv D \isin \baseof{M} \equiv D \isin \baseof{L}$.
+So $D \isin M \equiv D \isin L$ and by $\merge$,
+$D \isin C \equiv D \isin R$. But from Unique Base,
+$\baseof{C} = R$ so $D \isin C \equiv D \isin \baseof{C}$. OK.
-xxx the coherence is not that useful ?
-
-$L \haspatch \p$ by
-
-xxx need to recheck this
-
-$C \in \py$ $C \haspatch P$ so $D \isin C \equiv D \le C$. OK.
-
-\subsubsection{For $L \in \py, D \not\in \py, R \in \py$:}
-
-Tip Contents for $L$: $D \isin L \equiv D \isin \baseof{L}$.
-
-Tip Contents for $R$: $D \isin R \equiv D \isin \baseof{R}$.
+$\qed$
-But by Tip Merge, $\baseof{R} \ge \baseof{L}$
+xxx up to here, need to prove other things about merges
\end{document}
~ian / topbloke-formulae.git / blobdiff