chiark / gitweb /
index 40cc5f4..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 & @@ -133,12 +133,12 @@$$
\Big[
C \hasparents \{ A \}
\Big] \implies \left[
-   \bigforall_{P \patchisin C} \pendsof{C}{\p} = \{ T \}
+   \bigforall_{P \patchisin C} \pendsof{C}{\py} = \{ T \}
\right]
$$\proof{ - Trivial for C \in \p. - For C \not\in \p, \pancsof{C}{\p} = \pancsof{A}{\p}, + Trivial for C \in \py. + For C \not\in \py, \pancsof{C}{\py} = \pancsof{A}{\py}, so Unique Tips of A suffices. } @@ -175,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. @@ -192,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}$.
}