X-Git-Url: http://www.chiark.greenend.org.uk/ucgi/~ian/git?p=topbloke-formulae.git;a=blobdiff_plain;f=article.tex;h=a7b27094e0fb09243c554881a1d588a13156b5d0;hp=e6cc12aca29c8002485a2f6f5f8c486bac9abb47;hb=acef012c91c8ce7129b0093e7645d052c77aa74f;hpb=53c2225544614b126196dff87b6c086fd02c3561 diff --git a/article.tex b/article.tex index e6cc12a..a7b2709 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,18 +224,34 @@ 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 xxx - - Original definition is symmetrical in $L$ and $R$. +$$ +\proof{ ~ Truth table (ordered by original definition): \\ + \begin{tabular}{cccc|c|cc} + $D = C$ & + $\isin L$ & + $\isin M$ & + $\isin R$ & $\isin C$ & + $L$ vs. $R$ & $L$ vs. $M$ + \\\hline + y & ? & ? & ? & y & ? & ? \\ + n & y & y & y & y & $\equiv$ & $\equiv$ \\ + n & y & n & y & y & $\equiv$ & $\nequiv$ \\ + n & n & y & n & n & $\equiv$ & $\nequiv$ \\ + n & n & n & n & n & $\equiv$ & $\equiv$ \\ + n & y & y & n & n & $\nequiv$ & $\equiv$ \\ + n & n & y & y & n & $\nequiv$ & $\nequiv$ \\ + n & y & n & n & y & $\nequiv$ & $\nequiv$ \\ + n & n & n & y & y & $\nequiv$ & $\equiv$ \\ + \end{tabular} \\ + 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{ @@ -243,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{ @@ -254,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 -}\] -xxx proof tbd +$$ +\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 @@ -280,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} @@ -290,14 +317,24 @@ by the LHS. And $A \le A''$. \left\{ E \Big| \Bigl[ \Largeexists_{A \in \set A} E \in \pendsof{A}{\set P} \Bigr] \land - \Bigl[ \Largenexists_{B \in \set A} - E \neq B \land E \le B \Bigr] + \Bigl[ \Largenexists_{B \in \set A, F \in \pendsof{B}{\p}} + E \neq F \land E \le F \Bigr] \right\} \end{cases} -}\] -xxx proof tbd +$$ +\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}$. +So $\pendsof{C}{\set P} \subset \bigcup_{E in \set E} \pendsof{E}{\set P}$. +Consider some $E \in \pendsof{A}{\set P}$. If $\exists_{B,F}$ as +specified, then either $F$ is going to be in our result and +disqualifies $E$, or there is some other $F'$ (or, eventually, +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 \\ @@ -309,7 +346,7 @@ xxx proof tbd \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$ @@ -317,16 +354,19 @@ xxx proof tbd $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$, @@ -335,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 @@ -347,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 @@ -392,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. @@ -404,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 ) \] @@ -429,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$ @@ -442,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 $. @@ -450,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:}