X-Git-Url: http://www.chiark.greenend.org.uk/ucgi/~ian/git?a=blobdiff_plain;f=article.tex;h=d852fb8a7be17b2b5acb9245c97997c7db40717c;hb=151d200011cb73c9869fd9fe85e794bd324ffc86;hp=b26a120098b953606abe0fdee77d83abe9543735;hpb=e855f75b357a56be5f66cd8adb8deb08b10c55a9;p=topbloke-formulae.git

diff --git a/article.tex b/article.tex
index b26a120..d852fb8 100644
--- a/article.tex
+++ b/article.tex
@@ -8,6 +8,13 @@
 \usepackage{mdwlist}
 %\usepackage{accents}
 
+\usepackage{fancyhdr}
+\pagestyle{fancy}
+\lhead[\rightmark]{}
+
+\let\stdsection\section
+\renewcommand\section{\newpage\stdsection}
+
 \renewcommand{\ge}{\geqslant}
 \renewcommand{\le}{\leqslant}
 \newcommand{\nge}{\ngeqslant}
@@ -207,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     \\
@@ -217,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$ &
@@ -239,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{
@@ -258,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{
@@ -269,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
@@ -295,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}
@@ -309,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}$.
@@ -321,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
    \\
@@ -333,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$
@@ -341,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$,
@@ -359,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
@@ -371,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
@@ -416,9 +433,9 @@ because $\forall_{\py \ni C} \; \pendsof{C}{\py} = \{C\}$.
 
 A simple single-parent forward commit $C$ as made by git-commit.
 \begin{gather}
-\tag*{} C \hasparents \{ A \} \\
-\tag*{} \patchof{C} = \patchof{A} \\
-\tag*{} D \isin C \equiv D \isin A \lor D = C
+\tag*{} C \hasparents \{ L \} \\
+\tag*{} \patchof{C} = \patchof{L} \\
+\tag*{} D \isin C \equiv D \isin L \lor D = C
 \end{gather}
 This also covers Topbloke-generated commits on plain git branches:
 Topbloke strips the metadata when exporting.
@@ -428,24 +445,24 @@ Topbloke strips the metadata when exporting.
 Ingredients Prevent Replay applies.  $\qed$
 
 \subsection{Unique Base}
-If $A, C \in \py$ then by Calculation of Ends for
+If $L, C \in \py$ then by Calculation of Ends for
 $C, \py, C \not\in \py$:
-$\pendsof{C}{\pn} = \pendsof{A}{\pn}$ so
-$\baseof{C} = \baseof{A}$. $\qed$
+$\pendsof{C}{\pn} = \pendsof{L}{\pn}$ so
+$\baseof{C} = \baseof{L}$. $\qed$
 
 \subsection{Tip Contents}
-We need to consider only $A, C \in \py$.  From Tip Contents for $A$:
-\[ D \isin A \equiv D \isin \baseof{A} \lor ( D \in \py \land D \le A ) \]
+We need to consider only $L, C \in \py$.  From Tip Contents for $L$:
+\[ D \isin L \equiv D \isin \baseof{L} \lor ( D \in \py \land D \le L ) \]
 Substitute into the contents of $C$:
-\[ D \isin C \equiv D \isin \baseof{A} \lor ( D \in \py \land D \le A )
+\[ D \isin C \equiv D \isin \baseof{L} \lor ( D \in \py \land D \le L )
     \lor D = C \]
 Since $D = C \implies D \in \py$,
 and substituting in $\baseof{C}$, this gives:
 \[ D \isin C \equiv D \isin \baseof{C} \lor
-    (D \in \py \land D \le A) \lor
+    (D \in \py \land D \le L) \lor
     (D = C \land D \in \py) \]
 \[ \equiv D \isin \baseof{C} \lor
-   [ D \in \py \land ( D \le A \lor D = C ) ] \]
+   [ D \in \py \land ( D \le L \lor D = C ) ] \]
 So by Exact Ancestors:
 \[ D \isin C \equiv D \isin \baseof{C} \lor ( D \in \py \land D \le C
 ) \]
@@ -453,12 +470,12 @@ $\qed$
 
 \subsection{Base Acyclic}
 
-Need to consider only $A, C \in \pn$.
+Need to consider only $L, C \in \pn$.
 
 For $D = C$: $D \in \pn$ so $D \not\in \py$. OK.
 
-For $D \neq C$: $D \isin C \equiv D \isin A$, so by Base Acyclic for
-$A$, $D \isin C \implies D \not\in \py$.
+For $D \neq C$: $D \isin C \equiv D \isin L$, so by Base Acyclic for
+$L$, $D \isin C \implies D \not\in \py$.
 
 $\qed$
 
@@ -466,7 +483,7 @@ $\qed$
 
 Need to consider $D \in \py$
 
-\subsubsection{For $A \haspatch P, D = C$:}
+\subsubsection{For $L \haspatch P, D = C$:}
 
 Ancestors of $C$:
 $ D \le C $.
@@ -474,24 +491,24 @@ $ D \le C $.
 Contents of $C$:
 $ D \isin C \equiv \ldots \lor \true \text{ so } D \haspatch C $.
 
-\subsubsection{For $A \haspatch P, D \neq C$:}
-Ancestors: $ D \le C \equiv D \le A $.
+\subsubsection{For $L \haspatch P, D \neq C$:}
+Ancestors: $ D \le C \equiv D \le L $.
 
-Contents: $ D \isin C \equiv D \isin A \lor f $
-so $ D \isin C \equiv D \isin A $.
+Contents: $ D \isin C \equiv D \isin L \lor f $
+so $ D \isin C \equiv D \isin L $.
 
 So:
-\[ A \haspatch P \implies C \haspatch P \]
+\[ L \haspatch P \implies C \haspatch P \]
 
-\subsubsection{For $A \nothaspatch P$:}
+\subsubsection{For $L \nothaspatch P$:}
 
-Firstly, $C \not\in \py$ since if it were, $A \in \py$.
+Firstly, $C \not\in \py$ since if it were, $L \in \py$.
 Thus $D \neq C$.
 
-Now by contents of $A$, $D \notin A$, so $D \notin C$.
+Now by contents of $L$, $D \notin L$, so $D \notin C$.
 
 So:
-\[ A \nothaspatch P \implies C \nothaspatch P \]
+\[ L \nothaspatch P \implies C \nothaspatch P \]
 $\qed$
 
 \subsection{Foreign Inclusion:}
@@ -516,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}
@@ -538,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}
@@ -826,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}