chiark / gitweb /
index efffe6b..23e22f3 100644 (file)
@@ -1,6 +1,6 @@
\section{Some lemmas}

-\subsection{Alternative (overlapping) formulations of $\mergeof{C}{L}{M}{R}$}
+\subsection{Alternative (overlapping) formulations of $\commitmergeof{C}{L}{M}{R}$}
$$D \isin C \equiv \begin{cases} @@ -11,7 +11,7 @@$$
\text{as above with L and R exchanged}
\end{cases}
$$-\proof{ ~ Truth table (ordered by original definition): \\ +\proof{ ~ Truth table (ordered by original definitions): \\ \begin{tabular}{cccc|c|cc} D = C & \isin L & @@ -103,13 +103,13 @@$$
\bigforall_{C \hasparents \set A}
\pendsof{C}{\set P} =
\begin{cases}
-       C \in \p : & \{ C \}
+       C \in \set P : & \{ C \}
\\
-       C \not\in \p : & \displaystyle
+       C \not\in \set P : & \displaystyle
\left\{ E \Big|
\Bigl[ \Largeexists_{A \in \set A}
E \in \pendsof{A}{\set P} \Bigr] \land
-           \Bigl[ \Largenexists_{B \in \set A, F \in \pendsof{B}{\p}}
+           \Bigl[ \Largenexists_{B \in \set A, F \in \pendsof{B}{\set P}}
E \neq F \land E \le F \Bigr]
\right\}
\end{cases}
@@ -117,14 +117,31 @@ $$\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}. +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. +an F'') which disqualifies F and E. Otherwise, E meets all the conditions for \pends. } +\subsection{Single Parent Unique Tips} + +Unique Tips is satisfied for single-parent commits. Formally, +given a conformant commit A, +$$
+ \Big[
+   C \hasparents \{ A \}
+ \Big] \implies \left[
+   \bigforall_{P \patchisin C} \pendsof{C}{\py} = \{ T \}
+ \right]
+$$+\proof{ + Trivial for C \in \py. + For C \not\in \py, \pancsof{C}{\py} = \pancsof{A}{\py}, + so Unique Tips of A suffices. +} + \subsection{Ingredients Prevent Replay} Given conformant commits A \in \set A,$$
@@ -158,12 +175,12 @@ $$\right] \implies \left[ - \bigforall_{D \text{ s.t. } \patchof{D} = \bot} + \bigforall_{D \in \foreign} D \isin C \equiv D \le C \right]$$
\proof{
-Consider some $D$ s.t. $\patchof{D} = \bot$.
+Consider some $D \in \foreign$.
If $D = C$, trivially true.  For $D \neq C$,
by Foreign Inclusion of $D$ in $L$, $D \isin L \equiv D \le L$.
And by Exact Ancestors $D \le L \equiv D \le C$.
@@ -175,20 +192,20 @@ Given conformant commits $A \in \set A$,
$$\left[ C \hasparents \set A \land - \patchof{C} = \bot \land - \bigforall_{A \in \set A} \patchof{A} = \bot + \isforeign{C} \land + \bigforall_{A \in \set A} \isforeign{A} \right] \implies \left[ \bigforall_{D} D \le C \implies - \patchof{D} = \bot + \isforeign{D} \right]$$
\proof{
-Consider some $D \le C$.  If $D = C$, $\patchof{D} = \bot$ trivially.
+Consider some $D \le C$.  If $D = C$, $\isforeign{D}$ trivially.
If $D \neq C$ then $D \le A$ where $A \in \set A$.  By Foreign
-Contents of $A$, $\patchof{D} = \bot$.
+Contents of $A$, $\isforeign{D}$.
}