chiark / gitweb /
 author Ian Jackson Mon, 12 Mar 2012 15:53:40 +0000 (15:53 +0000) committer Ian Jackson Mon, 12 Mar 2012 15:59:38 +0000 (15:59 +0000)
 article.tex patch | blob | history

index 92e1f10..a7b2709 100644 (file)
@@ -12,6 +12,9 @@
\pagestyle{fancy}

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