more lemmas

diff --git a/article.tex b/article.tex
index 3f8bbff36113fc34d2434a6eb3e54505a51db462..9ca8012f6589cffebe568008215f152fafe1083c 100644 (file)
--- a/article.tex
+++ b/article.tex
@@ -44,7 +44,8 @@
 \newcommand{\patchof}[1]{{\mathcal P} ( #1 ) }
 \newcommand{\baseof}[1]{{\mathcal B} ( #1 ) }
 
-\newcommand{\eqn}[2]{ #2 \tag*{\mbox{#1}} }
+\newcommand{\eqn}[2]{ #2 \tag*{\mbox{\bf #1}} }
+\newcommand{\corrolary}[1]{ #1 \tag*{\mbox{\it Corrolary.}} }
 
 %\newcommand{\bigforall}{\mathop{\hbox{\huge$\forall$}}}
 \newcommand{\bigforall}{%
@@ -55,6 +56,8 @@
     {\hbox{\scriptsize$\forall$}}}%
 }
 
+\newcommand{\proof}[1]{{\it Proof.} #1 $\square$}
+
 \begin{document}
 
 \section{Notation}
@@ -124,21 +127,73 @@ it, we hope that git's merge algorithm will DTRT.
 
 \section{Invariants}
 
-\[ \eqn{No replay:}{
+\[ \eqn{No Replay:}{
   C \has D \implies C \ge D
 }\]
-\[\eqn{Unique base:}{
+\[\eqn{Unique Base:}{
  \bigforall_{C \in \py} \pends{C}{\pn} = \{ B \}
 }\]
-\[\eqn{Tip contents:}{
+\[\eqn{Tip Contents:}{
   \bigforall_{C \in \py} D \isin C \equiv
     { D \isin \baseof{C} \lor \atop
       (D \in \py \land D \le C) }
 }\]
-\[\eqn{Base acyclic:}{
+\[\eqn{Base Acyclic:}{
   \bigforall_{B \in \pn} D \isin B \implies D \notin \py
 }\]
 
+\section{Some lemmas}
+
+\[ \eqn{Exclusive Tip Contents:}{
+  \bigforall_{C \in \py} 
+    \neg \left[ D \isin \baseof{C} \land (D \in \py \land D \le C
+      \right )]
+}\]
+Ie, the two limbs of the RHS of Tip Contents are mutually exclusive.
+
+\proof{
+Let $B = \baseof{C}$ in $D \isin \baseof{C}$.  Now $B \in \pn$.
+So by Base Acyclic $D \isin B \implies D \notin \py$.
+}
+\[ \corrolary{
+  \bigforall_{C \in \py} D \isin C \equiv
+  \begin{cases}
+    D \in \py : & D \le C \\
+    D \not\in \py : & D \isin \baseof{C}
+  \end{cases}
+}\]
+
+\[ \eqn{Tip Self Inpatch:}{
+  \bigforall_{C \in \py} C \haspatch \p
+}\]
+Ie, tip commits contain their own patch.
+
+\proof{
+Apply Exclusive Tip Contents to some $D \in \py$:
+$ \bigforall_{C \in \py}\bigforall_{D \in \py}
+  D \isin C \equiv D \le C $
+}
+
+\[ \eqn{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
+}\]
+
+\[ \eqn{Transitive Ancestors:}{
+  \left[ \bigforall_{ E \in \pends{C}{\set P} } E \le C \right] \implies
+  \left[ \bigforall_{ A \in \pancs{C}{\set P} } A \le C \right]
+}\]
+
+\proof{
+By the definition of $\mathcal E$,
+for every such $A$, either $A \in \pends{C}{\set P}$ which implies
+$A \le C$, or $\exists_{A' \in \pancs{C}{\set P}} \; A' \neq A \land A \le C $
+in which case we repeat for $A'$.  Since there are finitely many
+commits, this terminates.
+}
+
 \section{Test more symbols}
 
 $ C \haspatch \p $