From: Ian Jackson <ijackson@chiark.greenend.org.uk>
Date: Mon, 12 Mar 2012 14:29:08 +0000 (+0000)
Subject: create tip wip
X-Git-Tag: f0.2~58
X-Git-Url: http://www.chiark.greenend.org.uk/ucgi/~ian/git?p=topbloke-formulae.git;a=commitdiff_plain;h=259a2d309ccfbde19838df143ff1fc88843c7d4d;ds=sidebyside

create tip wip
---

diff --git a/article.tex b/article.tex
index 69f530a..36233ae 100644
--- a/article.tex
+++ b/article.tex
@@ -538,6 +538,9 @@ Given a Topbloke base $B$, create a tip branch initial commit B.
 \[ \eqn{ Ingredients }{
  \patchof{B} = \pqn
 }\]
+\[ \eqn{ No Sneak }{
+ \pendsof{B}{\pqy} = \{ \}
+}\]
 
 \subsection{No Replay}
 
@@ -557,6 +560,19 @@ So $D \isin C \equiv D \isin \baseof{B}$.
 
 $\qed$
 
+\subsection{Base Acyclic}
+
+Not applicable.
+
+\subsection{Coherence and Patch Inclusion}
+
+Consider some $D \in \py$.
+
+\subsubsection{For $\p = \pq$:}
+
+By Base Acyclic, $D \not\isin B$.  So $D \isin C \equiv D = C$.
+By No Sneak, $D \le B \equiv D = C$.  Thus $C \haspatch \pq$.
+
 xxx up to here
 
 \section{Anticommit}