chiark / gitweb /
index 577f513..8509c89 100644 (file)
@@ -53,8 +53,8 @@ So by Base Acyclic $D \isin B \implies D \notin \py$.
\end{cases}
}\]

-\subsection{Tip Self Inpatch}
-Given Exclusive Tip Contents and Base Acyclic for $C$,
+\subsection{Tip Own Contents}
+Given Base Acyclic for $C$,
$$\bigforall_{C \in \py} C \haspatch \p$$
@@ -63,7 +63,9 @@ 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$
+  D \isin C \equiv D \le C $. +Thus$C \zhaspatch \p$. +And we can set$F=C$giving$F \in \py \land F \le C$, so$C \haspatch \p$. } \subsection{Exact Ancestors} @@ -101,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} @@ -115,15 +117,16 @@$$ \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{Ingredients Prevent Replay} +Given conformant commits$A \in \set A$, $$\left[ {C \hasparents \set A} \land @@ -140,12 +143,13 @@$$ $$\proof{ Trivial for D = C. Consider some D \neq C, D \isin C. - By the preconditions, there is some A s.t. D \in \set A + By the preconditions, there is some A s.t. A \in \set A and D \isin A. By No Replay for A, D \le A. And A \le C so D \le C. } \subsection{Simple Foreign Inclusion} +Given a conformant commit L,$$ \left[ C \hasparents \{ L \} @@ -167,6 +171,7 @@ So$D \isin C \equiv D \le C$. } \subsection{Totally Foreign Contents} +Given conformant commits$A \in \set A$,$\$
\left[
C \hasparents \set A \land