lemmas.tex

   1 \section{Some lemmas}
   2
   3 \subsection{Alternative (overlapping) formulations of $\mergeof{C}{L}{M}{R}$}
   4 $$
   5  D \isin C \equiv
   6   \begin{cases}
   7     D \isin L  \equiv D \isin R  : & D = C \lor D \isin L     \\
   8     D \isin L \nequiv D \isin R  : & D = C \lor D \not\isin M \\
   9     D \isin L  \equiv D \isin M  : & D = C \lor D \isin R     \\
  10     D \isin L \nequiv D \isin M  : & D = C \lor D \isin L     \\
  11     \text{as above with L and R exchanged}
  12   \end{cases}
  13 $$
  14 \proof{ ~ Truth table (ordered by original definition): \\
  15   \begin{tabular}{cccc|c|cc}
  16      $D = C$ &
  17           $\isin L$ &
  18                $\isin M$ &
  19                     $\isin R$ & $\isin C$ &
  20                                       $L$ vs. $R$ & $L$ vs. $M$
  21   \\\hline
  22      y &  ? &  ? &  ?      &      y   & ?         & ?            \\
  23      n &  y &  y &  y      &      y   & $\equiv$  & $\equiv$     \\
  24      n &  y &  n &  y      &      y   & $\equiv$  & $\nequiv$    \\
  25      n &  n &  y &  n      &      n   & $\equiv$  & $\nequiv$    \\
  26      n &  n &  n &  n      &      n   & $\equiv$  & $\equiv$     \\
  27      n &  y &  y &  n      &      n   & $\nequiv$ & $\equiv$     \\
  28      n &  n &  y &  y      &      n   & $\nequiv$ & $\nequiv$    \\
  29      n &  y &  n &  n      &      y   & $\nequiv$ & $\nequiv$    \\
  30      n &  n &  n &  y      &      y   & $\nequiv$ & $\equiv$     \\
  31   \end{tabular} \\
  32   And original definition is symmetrical in $L$ and $R$.
  33 }
  34
  35 \subsection{Exclusive Tip Contents}
  36 Given Base Acyclic for $C$,
  37 $$
  38   \bigforall_{C \in \py}
  39     \neg \Bigl[ D \isin \baseof{C} \land ( D \in \py \land D \le C )
  40       \Bigr]
  41 $$
  42 Ie, the two limbs of the RHS of Tip Contents are mutually exclusive.
  43
  44 \proof{
  45 Let $B = \baseof{C}$ in $D \isin \baseof{C}$.  Now $B \in \pn$.
  46 So by Base Acyclic $D \isin B \implies D \notin \py$.
  47 }
  48 \[ \eqntag{{\it Corollary - equivalent to Tip Contents}}{
  49   \bigforall_{C \in \py} D \isin C \equiv
  50   \begin{cases}
  51     D \in \py : & D \le C \\
  52     D \not\in \py : & D \isin \baseof{C}
  53   \end{cases}
  54 }\]
  55
  56 \subsection{Tip Self Inpatch}
  57 Given Exclusive Tip Contents and Base Acyclic for $C$,
  58 $$
  59   \bigforall_{C \in \py} C \haspatch \p
  60 $$
  61 Ie, tip commits contain their own patch.
  62
  63 \proof{
  64 Apply Exclusive Tip Contents to some $D \in \py$:
  65 $ \bigforall_{C \in \py}\bigforall_{D \in \py}
  66   D \isin C \equiv D \le C $
  67 }
  68
  69 \subsection{Exact Ancestors}
  70 $$
  71   \bigforall_{ C \hasparents \set{R} }
  72   \left[
  73   D \le C \equiv
  74     ( \mathop{\hbox{\huge{$\vee$}}}_{R \in \set R} D \le R )
  75     \lor D = C
  76   \right]
  77 $$
  78 \proof{ ~ Trivial.}
  79
  80 \subsection{Transitive Ancestors}
  81 $$
  82   \left[ \bigforall_{ E \in \pendsof{C}{\set P} } E \le M \right] \equiv
  83   \left[ \bigforall_{ A \in \pancsof{C}{\set P} } A \le M \right]
  84 $$
  85
  86 \proof{
  87 The implication from right to left is trivial because
  88 $ \pends() \subset \pancs() $.
  89 For the implication from left to right:
  90 by the definition of $\mathcal E$,
  91 for every such $A$, either $A \in \pends()$ which implies
  92 $A \le M$ by the LHS directly,
  93 or $\exists_{A' \in \pancs()} \; A' \neq A \land A \le A' $
  94 in which case we repeat for $A'$.  Since there are finitely many
  95 commits, this terminates with $A'' \in \pends()$, ie $A'' \le M$
  96 by the LHS.  And $A \le A''$.
  97 }
  98
  99 \subsection{Calculation of Ends}
 100 $$
 101   \bigforall_{C \hasparents \set A}
 102     \pendsof{C}{\set P} =
 103       \begin{cases}
 104        C \in \p : & \{ C \}
 105       \\
 106        C \not\in \p : & \displaystyle
 107        \left\{ E \Big|
 108            \Bigl[ \Largeexists_{A \in \set A}
 109                        E \in \pendsof{A}{\set P} \Bigr] \land
 110            \Bigl[ \Largenexists_{B \in \set A, F \in \pendsof{B}{\p}}
 111                        E \neq F \land E \le F \Bigr]
 112        \right\}
 113       \end{cases}
 114 $$
 115 \proof{
 116 Trivial for $C \in \set P$.  For $C \not\in \set P$,
 117 $\pancsof{C}{\set P} = \bigcup_{A \in \set A} \pancsof{A}{\set P}$.
 118 So $\pendsof{C}{\set P} \subset \bigcup_{E in \set E} \pendsof{E}{\set P}$.
 119 Consider some $E \in \pendsof{A}{\set P}$.  If $\exists_{B,F}$ as
 120 specified, then either $F$ is going to be in our result and
 121 disqualifies $E$, or there is some other $F'$ (or, eventually,
 122 an $F''$) which disqualifies $F$.
 123 Otherwise, $E$ meets all the conditions for $\pends$.
 124 }
 125
 126 \subsection{Ingredients Prevent Replay}
 127 $$
 128   \left[
 129     {C \hasparents \set A} \land
 130    \\
 131     \bigforall_{D}
 132     \left(
 133        D \isin C \implies
 134        D = C \lor
 135        \Largeexists_{A \in \set A} D \isin A
 136     \right)
 137   \right] \implies \left[ \bigforall_{D}
 138     D \isin C \implies D \le C
 139   \right]
 140 $$
 141 \proof{
 142   Trivial for $D = C$.  Consider some $D \neq C$, $D \isin C$.
 143   By the preconditions, there is some $A$ s.t. $D \in \set A$
 144   and $D \isin A$.  By No Replay for $A$, $D \le A$.  And
 145   $A \le C$ so $D \le C$.
 146 }
 147
 148 \subsection{Simple Foreign Inclusion}
 149 $$
 150   \left[
 151     C \hasparents \{ L \}
 152    \land
 153     \bigforall_{D} D \isin C \equiv D \isin L \lor D = C
 154   \right]
 155  \implies
 156   \left[
 157    \bigforall_{D \text{ s.t. } \patchof{D} = \bot}
 158      D \isin C \equiv D \le C
 159   \right]
 160 $$
 161 \proof{
 162 Consider some $D$ s.t. $\patchof{D} = \bot$.
 163 If $D = C$, trivially true.  For $D \neq C$,
 164 by Foreign Inclusion of $D$ in $L$, $D \isin L \equiv D \le L$.
 165 And by Exact Ancestors $D \le L \equiv D \le C$.
 166 So $D \isin C \equiv D \le C$.
 167 }
 168
 169 \subsection{Totally Foreign Contents}
 170 $$
 171    \left[
 172     C \hasparents \set A \land
 173     \patchof{C} = \bot \land
 174       \bigforall_{A \in \set A} \patchof{A} = \bot
 175    \right]
 176   \implies
 177    \left[
 178   \bigforall_{D}
 179     D \le C
 180    \implies
 181     \patchof{D} = \bot
 182    \right]
 183 $$
 184 \proof{
 185 Consider some $D \le C$.  If $D = C$, $\patchof{D} = \bot$ trivially.
 186 If $D \neq C$ then $D \le A$ where $A \in \set A$.  By Foreign
 187 Contents of $A$, $\patchof{D} = \bot$.
 188 }
 189