Prove that plain git merges on non-tb branches are ok

diff --git a/article.tex b/article.tex
index afefebd90d7aaf60e5de2f8da98c4fee810a4aa8..28d02a02c7153d08724d0d451ac2fe922024a6b9 100644 (file)
--- a/article.tex
+++ b/article.tex
@@ -526,6 +526,17 @@ We will occasionally use $X,Y$ s.t. $\{X,Y\} = \{L,R\}$.
    \right]
 }\]
 
+\subsection{Non-Topbloke merges}
+
+We require both $\patchof{L} = \bot$ and $\patchof{R} = \bot$.
+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.
+
 \subsection{No Replay}
 
 See No Replay for Merge Results.