chiark / gitweb /
in simple commit rename parent from A to L
authorIan Jackson <ijackson@chiark.greenend.org.uk>
Mon, 12 Mar 2012 15:36:53 +0000 (15:36 +0000)
committerIan Jackson <ijackson@chiark.greenend.org.uk>
Mon, 12 Mar 2012 15:37:09 +0000 (15:37 +0000)
article.tex

index b26a120098b953606abe0fdee77d83abe9543735..ed6ce526885a0729b74c091398edf032659c8b04 100644 (file)
@@ -416,9 +416,9 @@ because $\forall_{\py \ni C} \; \pendsof{C}{\py} = \{C\}$.
 
 A simple single-parent forward commit $C$ as made by git-commit.
 \begin{gather}
-\tag*{} C \hasparents \{ A \} \\
-\tag*{} \patchof{C} = \patchof{A} \\
-\tag*{} D \isin C \equiv D \isin A \lor D = C
+\tag*{} C \hasparents \{ L \} \\
+\tag*{} \patchof{C} = \patchof{L} \\
+\tag*{} D \isin C \equiv D \isin L \lor D = C
 \end{gather}
 This also covers Topbloke-generated commits on plain git branches:
 Topbloke strips the metadata when exporting.
@@ -428,24 +428,24 @@ Topbloke strips the metadata when exporting.
 Ingredients Prevent Replay applies.  $\qed$
 
 \subsection{Unique Base}
-If $A, C \in \py$ then by Calculation of Ends for
+If $L, C \in \py$ then by Calculation of Ends for
 $C, \py, C \not\in \py$:
-$\pendsof{C}{\pn} = \pendsof{A}{\pn}$ so
-$\baseof{C} = \baseof{A}$. $\qed$
+$\pendsof{C}{\pn} = \pendsof{L}{\pn}$ so
+$\baseof{C} = \baseof{L}$. $\qed$
 
 \subsection{Tip Contents}
-We need to consider only $A, C \in \py$.  From Tip Contents for $A$:
-\[ D \isin A \equiv D \isin \baseof{A} \lor ( D \in \py \land D \le A ) \]
+We need to consider only $L, C \in \py$.  From Tip Contents for $L$:
+\[ D \isin L \equiv D \isin \baseof{L} \lor ( D \in \py \land D \le L ) \]
 Substitute into the contents of $C$:
-\[ D \isin C \equiv D \isin \baseof{A} \lor ( D \in \py \land D \le A )
+\[ D \isin C \equiv D \isin \baseof{L} \lor ( D \in \py \land D \le L )
     \lor D = C \]
 Since $D = C \implies D \in \py$,
 and substituting in $\baseof{C}$, this gives:
 \[ D \isin C \equiv D \isin \baseof{C} \lor
-    (D \in \py \land D \le A) \lor
+    (D \in \py \land D \le L) \lor
     (D = C \land D \in \py) \]
 \[ \equiv D \isin \baseof{C} \lor
-   [ D \in \py \land ( D \le A \lor D = C ) ] \]
+   [ D \in \py \land ( D \le L \lor D = C ) ] \]
 So by Exact Ancestors:
 \[ D \isin C \equiv D \isin \baseof{C} \lor ( D \in \py \land D \le C
 ) \]
@@ -453,12 +453,12 @@ $\qed$
 
 \subsection{Base Acyclic}
 
-Need to consider only $A, C \in \pn$.
+Need to consider only $L, C \in \pn$.
 
 For $D = C$: $D \in \pn$ so $D \not\in \py$. OK.
 
-For $D \neq C$: $D \isin C \equiv D \isin A$, so by Base Acyclic for
-$A$, $D \isin C \implies D \not\in \py$.
+For $D \neq C$: $D \isin C \equiv D \isin L$, so by Base Acyclic for
+$L$, $D \isin C \implies D \not\in \py$.
 
 $\qed$
 
@@ -466,7 +466,7 @@ $\qed$
 
 Need to consider $D \in \py$
 
-\subsubsection{For $A \haspatch P, D = C$:}
+\subsubsection{For $L \haspatch P, D = C$:}
 
 Ancestors of $C$:
 $ D \le C $.
@@ -474,24 +474,24 @@ $ D \le C $.
 Contents of $C$:
 $ D \isin C \equiv \ldots \lor \true \text{ so } D \haspatch C $.
 
-\subsubsection{For $A \haspatch P, D \neq C$:}
-Ancestors: $ D \le C \equiv D \le A $.
+\subsubsection{For $L \haspatch P, D \neq C$:}
+Ancestors: $ D \le C \equiv D \le L $.
 
-Contents: $ D \isin C \equiv D \isin A \lor f $
-so $ D \isin C \equiv D \isin A $.
+Contents: $ D \isin C \equiv D \isin L \lor f $
+so $ D \isin C \equiv D \isin L $.
 
 So:
-\[ A \haspatch P \implies C \haspatch P \]
+\[ L \haspatch P \implies C \haspatch P \]
 
-\subsubsection{For $A \nothaspatch P$:}
+\subsubsection{For $L \nothaspatch P$:}
 
-Firstly, $C \not\in \py$ since if it were, $A \in \py$.
+Firstly, $C \not\in \py$ since if it were, $L \in \py$.
 Thus $D \neq C$.
 
-Now by contents of $A$, $D \notin A$, so $D \notin C$.
+Now by contents of $L$, $D \notin L$, so $D \notin C$.
 
 So:
-\[ A \nothaspatch P \implies C \nothaspatch P \]
+\[ L \nothaspatch P \implies C \nothaspatch P \]
 $\qed$
 
 \subsection{Foreign Inclusion:}