chiark
/
gitweb
/
~ian
/
topbloke-formulae.git
/ commitdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
| commitdiff |
tree
raw
|
patch
|
inline
| side by side (parent:
e855f75
)
in simple commit rename parent from A to L
author
Ian Jackson
<ijackson@chiark.greenend.org.uk>
Mon, 12 Mar 2012 15:36:53 +0000
(15:36 +0000)
committer
Ian Jackson
<ijackson@chiark.greenend.org.uk>
Mon, 12 Mar 2012 15:37:09 +0000
(15:37 +0000)
article.tex
patch
|
blob
|
history
diff --git
a/article.tex
b/article.tex
index b26a120098b953606abe0fdee77d83abe9543735..ed6ce526885a0729b74c091398edf032659c8b04 100644
(file)
--- 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}
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.
\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}
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$:
$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}
\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$:
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
\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 = 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
) \]
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}
\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 = 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$
$\qed$
@@
-466,7
+466,7
@@
$\qed$
Need to consider $D \in \py$
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 $.
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 $.
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:
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$.
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:
So:
-\[
A
\nothaspatch P \implies C \nothaspatch P \]
+\[
L
\nothaspatch P \implies C \nothaspatch P \]
$\qed$
\subsection{Foreign Inclusion:}
$\qed$
\subsection{Foreign Inclusion:}