From c517a34b73ff5df3f28591b2a2b1c0c312f13df8 Mon Sep 17 00:00:00 2001 From: Ian Jackson Date: Mon, 12 Mar 2012 15:36:53 +0000 Subject: [PATCH 1/1] in simple commit rename parent from A to L --- article.tex | 48 ++++++++++++++++++++++++------------------------ 1 file changed, 24 insertions(+), 24 deletions(-) diff --git a/article.tex b/article.tex index b26a120..ed6ce52 100644 --- a/article.tex +++ b/article.tex @@ -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:} -- 2.30.2