X-Git-Url: http://www.chiark.greenend.org.uk/ucgi/~ian/git?a=blobdiff_plain;f=article.tex;h=1a1e9d14363d2b3b629a21e6320029754bdcc614;hb=11f4dd11cebc837935410fb336c610a906fd1f27;hp=92e1f1010b77f5022f606af2de2a4842dcf9efd9;hpb=1f8eb7a95b12515aa6b4d33ccfdabee2ff042e0f;p=topbloke-formulae.git

diff --git a/article.tex b/article.tex
index 92e1f10..1a1e9d1 100644
--- a/article.tex
+++ b/article.tex
@@ -12,6 +12,9 @@
 \pagestyle{fancy}
 \lhead[\rightmark]{}
 
+\let\stdsection\section
+\renewcommand\section{\newpage\stdsection}
+
 \renewcommand{\ge}{\geqslant}
 \renewcommand{\le}{\leqslant}
 \newcommand{\nge}{\ngeqslant}
@@ -130,7 +133,7 @@ A patch $\p$ consists of two sets of commits $\pn$ and $\py$, which
 are respectively the base and tip git branches.  $\p$ may be used
 where the context requires a set, in which case the statement
 is to be taken as applying to both $\py$ and $\pn$.
-None of these sets overlap.  Hence:
+All of these sets are disjoint.  Hence:
 
 \item[ $ \patchof{ C } $ ]
 Either $\p$ s.t. $ C \in \p $, or $\bot$.
@@ -211,8 +214,8 @@ We maintain these each time we construct a new commit. \\
 
 \section{Some lemmas}
 
-\[ \eqn{Alternative (overlapping) formulations defining
-  $\mergeof{C}{L}{M}{R}$:}{
+\subsection{Alternative (overlapping) formulations of $\mergeof{C}{L}{M}{R}$}
+$$
  D \isin C \equiv
   \begin{cases}
     D \isin L  \equiv D \isin R  : & D = C \lor D \isin L     \\
@@ -221,7 +224,7 @@ We maintain these each time we construct a new commit. \\
     D \isin L \nequiv D \isin M  : & D = C \lor D \isin L     \\
     \text{as above with L and R exchanged}
   \end{cases}
-}\]
+$$
 \proof{ ~ Truth table (ordered by original definition): \\
   \begin{tabular}{cccc|c|cc}
      $D = C$ &
@@ -243,11 +246,12 @@ We maintain these each time we construct a new commit. \\
   And original definition is symmetrical in $L$ and $R$.
 }
 
-\[ \eqn{Exclusive Tip Contents:}{
+\subsection{Exclusive Tip Contents}
+$$
   \bigforall_{C \in \py}
     \neg \Bigl[ D \isin \baseof{C} \land ( D \in \py \land D \le C )
       \Bigr]
-}\]
+$$
 Ie, the two limbs of the RHS of Tip Contents are mutually exclusive.
 
 \proof{
@@ -262,9 +266,10 @@ So by Base Acyclic $D \isin B \implies D \notin \py$.
   \end{cases}
 }\]
 
-\[ \eqn{Tip Self Inpatch:}{
+\subsection{Tip Self Inpatch}
+$$
   \bigforall_{C \in \py} C \haspatch \p
-}\]
+$$
 Ie, tip commits contain their own patch.
 
 \proof{
@@ -273,18 +278,20 @@ $ \bigforall_{C \in \py}\bigforall_{D \in \py}
   D \isin C \equiv D \le C $
 }
 
-\[ \eqn{Exact Ancestors:}{
+\subsection{Exact Ancestors}
+$$
   \bigforall_{ C \hasparents \set{R} }
   D \le C \equiv
     ( \mathop{\hbox{\huge{$\vee$}}}_{R \in \set R} D \le R )
     \lor D = C
-}\]
+$$
 \proof{ ~ Trivial.}
 
-\[ \eqn{Transitive Ancestors:}{
+\subsection{Transitive Ancestors}
+$$
   \left[ \bigforall_{ E \in \pendsof{C}{\set P} } E \le M \right] \equiv
   \left[ \bigforall_{ A \in \pancsof{C}{\set P} } A \le M \right]
-}\]
+$$
 
 \proof{
 The implication from right to left is trivial because
@@ -299,7 +306,8 @@ commits, this terminates with $A'' \in \pends()$, ie $A'' \le M$
 by the LHS.  And $A \le A''$.
 }
 
-\[ \eqn{Calculation Of Ends:}{
+\subsection{Calculation Of Ends}
+$$
   \bigforall_{C \hasparents \set A}
     \pendsof{C}{\set P} =
       \begin{cases}
@@ -313,7 +321,7 @@ by the LHS.  And $A \le A''$.
                        E \neq F \land E \le F \Bigr]
        \right\}
       \end{cases}
-}\]
+$$
 \proof{
 Trivial for $C \in \set P$.  For $C \not\in \set P$,
 $\pancsof{C}{\set P} = \bigcup_{A \in \set A} \pancsof{A}{\set P}$.
@@ -325,7 +333,8 @@ an $F''$) which disqualifies $F$.
 Otherwise, $E$ meets all the conditions for $\pends$.
 }
 
-\[ \eqn{Ingredients Prevent Replay:}{
+\subsection{Ingredients Prevent Replay}
+$$
   \left[
     {C \hasparents \set A} \land
    \\
@@ -337,7 +346,7 @@ Otherwise, $E$ meets all the conditions for $\pends$.
   \right] \implies \left[
     D \isin C \implies D \le C
   \right]
-}\]
+$$
 \proof{
   Trivial for $D = C$.  Consider some $D \neq C$, $D \isin C$.
   By the preconditions, there is some $A$ s.t. $D \in \set A$
@@ -345,16 +354,19 @@ Otherwise, $E$ meets all the conditions for $\pends$.
   $A \le C$ so $D \le C$.
 }
 
-\[ \eqn{Simple Foreign Inclusion:}{
+\subsection{Simple Foreign Inclusion}
+$$
   \left[
     C \hasparents \{ L \}
    \land
     \bigforall_{D} D \isin C \equiv D \isin L \lor D = C
   \right]
  \implies
+  \left[
    \bigforall_{D \text{ s.t. } \patchof{D} = \bot}
      D \isin C \equiv D \le C
-}\]
+  \right]
+$$
 \proof{
 Consider some $D$ s.t. $\patchof{D} = \bot$.
 If $D = C$, trivially true.  For $D \neq C$,
@@ -363,7 +375,8 @@ And by Exact Ancestors $D \le L \equiv D \le C$.
 So $D \isin C \equiv D \le C$.
 }
 
-\[ \eqn{Totally Foreign Contents:}{
+\subsection{Totally Foreign Contents}
+$$
   \bigforall_{C \hasparents \set A}
    \left[
     \patchof{C} = \bot \land
@@ -375,7 +388,7 @@ So $D \isin C \equiv D \le C$.
    \implies
     \patchof{D} = \bot
    \right]
-}\]
+$$
 \proof{
 Consider some $D \le C$.  If $D = C$, $\patchof{D} = \bot$ trivially.
 If $D \neq C$ then $D \le A$ where $A \in \set A$.  By Foreign
@@ -520,11 +533,8 @@ Given $L$, create a Topbloke base branch initial commit $B$.
 
 \subsection{Conditions}
 
-\[ \eqn{ Ingredients }{
- \patchof{L} = \pa{L} \lor \patchof{L} = \bot
-}\]
 \[ \eqn{ Create Acyclic }{
- L \not\haspatch \pq
+ \pendsof{L}{\pqy} = \{ \}
 }\]
 
 \subsection{No Replay}
@@ -542,7 +552,8 @@ Not applicable.
 \subsection{Base Acyclic}
 
 Consider some $D \isin B$.  If $D = B$, $D \in \pqn$.
-If $D \neq B$, $D \isin L$, and by Create Acyclic
+If $D \neq B$, $D \isin L$, so by No Replay $D \le L$
+and by Create Acyclic
 $D \not\in \pqy$.  $\qed$
 
 \subsection{Coherence and Patch Inclusion}
@@ -830,7 +841,7 @@ And $Y \not\in \py$ so $\neg [ Y \haspatch \p ]$ so neither
 Merge Ends condition applies.
 
 So a plain git merge of non-Topbloke branches meets the conditions and
-is therefore consistent with our scheme.
+is therefore consistent with our model.
 
 \subsection{No Replay}