From acef012c91c8ce7129b0093e7645d052c77aa74f Mon Sep 17 00:00:00 2001
From: Ian Jackson <ijackson@chiark.greenend.org.uk>
Date: Mon, 12 Mar 2012 15:53:40 +0000
Subject: [PATCH] formatting: a couple of extra [ ]

---
 article.tex | 51 ++++++++++++++++++++++++++++++++-------------------
 1 file changed, 32 insertions(+), 19 deletions(-)

diff --git a/article.tex b/article.tex
index 92e1f10..a7b2709 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}
@@ -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
-- 
2.30.2