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 Own Contents}
  57 Given 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 Thus $C \zhaspatch \p$.
  68 And we can set $F=C$ giving $F \in \py \land F \le C$, so $C \haspatch \p$.
  69 }
  70
  71 \subsection{Exact Ancestors}
  72 $$
  73   \bigforall_{ C \hasparents \set{R} }
  74   \left[
  75   D \le C \equiv
  76     ( \mathop{\hbox{\huge{$\vee$}}}_{R \in \set R} D \le R )
  77     \lor D = C
  78   \right]
  79 $$
  80 \proof{ ~ Trivial.}
  81
  82 \subsection{Transitive Ancestors}
  83 $$
  84   \left[ \bigforall_{ E \in \pendsof{C}{\set P} } E \le M \right] \equiv
  85   \left[ \bigforall_{ A \in \pancsof{C}{\set P} } A \le M \right]
  86 $$
  87
  88 \proof{
  89 The implication from right to left is trivial because
  90 $ \pends() \subset \pancs() $.
  91 For the implication from left to right:
  92 by the definition of $\mathcal E$,
  93 for every such $A$, either $A \in \pends()$ which implies
  94 $A \le M$ by the LHS directly,
  95 or $\exists_{A' \in \pancs()} \; A' \neq A \land A \le A' $
  96 in which case we repeat for $A'$.  Since there are finitely many
  97 commits, this terminates with $A'' \in \pends()$, ie $A'' \le M$
  98 by the LHS.  And $A \le A''$.
  99 }
 100
 101 \subsection{Calculation of Ends}
 102 $$
 103   \bigforall_{C \hasparents \set A}
 104     \pendsof{C}{\set P} =
 105       \begin{cases}
 106        C \in \set P : & \{ C \}
 107       \\
 108        C \not\in \set P : & \displaystyle
 109        \left\{ E \Big|
 110            \Bigl[ \Largeexists_{A \in \set A}
 111                        E \in \pendsof{A}{\set P} \Bigr] \land
 112            \Bigl[ \Largenexists_{B \in \set A, F \in \pendsof{B}{\set P}}
 113                        E \neq F \land E \le F \Bigr]
 114        \right\}
 115       \end{cases}
 116 $$
 117 \proof{
 118 Trivial for $C \in \set P$.  For $C \not\in \set P$,
 119 $\pancsof{C}{\set P} = \bigcup_{A \in \set A} \pancsof{A}{\set P}$.
 120 So $\pendsof{C}{\set P} \subset \bigcup_{E \in \set E} \pendsof{E}{\set P}$.
 121 Consider some $E \in \pendsof{A}{\set P}$.  If $\exists_{B,F}$ as
 122 specified, then either $F$ is going to be in our result and
 123 disqualifies $E$, or there is some other $F'$ (or, eventually,
 124 an $F''$) which disqualifies $F$.
 125 Otherwise, $E$ meets all the conditions for $\pends$.
 126 }
 127
 128 \subsection{Ingredients Prevent Replay}
 129 Given conformant commits $A \in \set A$,
 130 $$
 131   \left[
 132     {C \hasparents \set A} \land
 133    \\
 134     \bigforall_{D}
 135     \left(
 136        D \isin C \implies
 137        D = C \lor
 138        \Largeexists_{A \in \set A} D \isin A
 139     \right)
 140   \right] \implies \left[ \bigforall_{D}
 141     D \isin C \implies D \le C
 142   \right]
 143 $$
 144 \proof{
 145   Trivial for $D = C$.  Consider some $D \neq C$, $D \isin C$.
 146   By the preconditions, there is some $A$ s.t. $A \in \set A$
 147   and $D \isin A$.  By No Replay for $A$, $D \le A$.  And
 148   $A \le C$ so $D \le C$.
 149 }
 150
 151 \subsection{Simple Foreign Inclusion}
 152 Given a conformant commit $L$,
 153 $$
 154   \left[
 155     C \hasparents \{ L \}
 156    \land
 157     \bigforall_{D} D \isin C \equiv D \isin L \lor D = C
 158   \right]
 159  \implies
 160   \left[
 161    \bigforall_{D \text{ s.t. } \patchof{D} = \bot}
 162      D \isin C \equiv D \le C
 163   \right]
 164 $$
 165 \proof{
 166 Consider some $D$ s.t. $\patchof{D} = \bot$.
 167 If $D = C$, trivially true.  For $D \neq C$,
 168 by Foreign Inclusion of $D$ in $L$, $D \isin L \equiv D \le L$.
 169 And by Exact Ancestors $D \le L \equiv D \le C$.
 170 So $D \isin C \equiv D \le C$.
 171 }
 172
 173 \subsection{Totally Foreign Contents}
 174 Given conformant commits $A \in \set A$,
 175 $$
 176    \left[
 177     C \hasparents \set A \land
 178     \patchof{C} = \bot \land
 179       \bigforall_{A \in \set A} \patchof{A} = \bot
 180    \right]
 181   \implies
 182    \left[
 183   \bigforall_{D}
 184     D \le C
 185    \implies
 186     \patchof{D} = \bot
 187    \right]
 188 $$
 189 \proof{
 190 Consider some $D \le C$.  If $D = C$, $\patchof{D} = \bot$ trivially.
 191 If $D \neq C$ then $D \le A$ where $A \in \set A$.  By Foreign
 192 Contents of $A$, $\patchof{D} = \bot$.
 193 }
 194