From 2f6d22b0c5f79efe583c8016b2860474261f4750 Mon Sep 17 00:00:00 2001
From: Ian Jackson <ijackson@chiark.greenend.org.uk>
Date: Sun, 11 Mar 2012 11:24:26 +0000
Subject: [PATCH] Prove that plain git merges on non-tb branches are ok

---
 article.tex | 11 +++++++++++
 1 file changed, 11 insertions(+)

diff --git a/article.tex b/article.tex
index afefebd..28d02a0 100644
--- 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.
-- 
2.30.2