formalise foreign merges

diff --git a/article.tex b/article.tex
index 3d8bd8179a5f26dc787fa70a4de9046f32709f6d..ad3a1bae8579d8cf92685644f392209ef1ec882e 100644 (file)
--- a/article.tex
+++ b/article.tex
@@ -684,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}