\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}