fix some headings

[topbloke-formulae.git] / article.tex

diff --git a/article.tex b/article.tex
index 7630745d41eaf60ca7369bd99e7ec29ea03cbe98..f69420fc071f170952b9e5a60ca9a60916658ec5 100644 (file)
--- a/article.tex
+++ b/article.tex
@@ -459,6 +459,13 @@ $\qed$
 If $D = C$, trivial.  For $D \neq C$:
 $D \isin C \equiv D \isin A \equiv D \le A \equiv D \le C$.  $\qed$
 
+\subsection{Foreign Contents:}
+
+Only relevant if $\patchof{C} = \bot$.  Trivial by Foreign Contents of
+$A$.  $\qed$
+
+xxx fixme not trivial use Totally Foreign Contents
+
 \section{Create Base}
 
 Given $L$, create a Topbloke base branch initial commit $B$.
@@ -628,6 +635,10 @@ Thus $D \isin C \equiv D \le C$.
 
 $\qed$
 
+\subsection{Foreign Contents}
+
+Not applicable. $\qed$
+
 \section{Merge}
 
 Merge commits $L$ and $R$ using merge base $M$:
@@ -673,17 +684,24 @@ We will occasionally use $X,Y$ s.t. $\{X,Y\} = \{L,R\}$.
     \bigforall_{E \in \pendsof{X}{\py}} E \le Y
    \right]
 }\]
+\[ \eqn{ Foreign Merges }{
+    \patchof{L} = \bot \equiv \patchof{R} = \bot
+}\]
 
 \subsection{Non-Topbloke merges}
 
-We require both $\patchof{L} = \bot$ and $\patchof{R} = \bot$.
+We require both $\patchof{L} = \bot$ and $\patchof{R} = \bot$
+(Foreign Merges, above).
 I.e. not only is it forbidden to merge into a Topbloke-controlled
 branch without Topbloke's assistance, it is also forbidden to
 merge any Topbloke-controlled branch into any plain git branch.
 
 Given those conditions, Tip Merge and Merge Acyclic do not apply.
 And $Y \not\in \py$ so $\neg [ Y \haspatch \p ]$ so neither
-Merge Ends condition applies.  Good.
+Merge Ends condition applies.
+
+So a plain git merge of non-Topbloke branches meets the conditions and
+is therefore consistent with our scheme.
 
 \subsection{No Replay}
 
@@ -888,4 +906,11 @@ OK
 
 $\qed$
 
+\subsection{Foreign Contents}
+
+xxx use Totally Foreign Contents
+
+If $\patchof{C} = \bot$, by Foreign Merges
+$\patchof{L} = \patchof{R} = \bot$.
+
 \end{document}