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:
69f2ee3
)
unique tips: single parent unique tips lemma
author
Ian Jackson
<ijackson@chiark.greenend.org.uk>
Wed, 18 Apr 2012 17:27:03 +0000
(18:27 +0100)
committer
Ian Jackson
<ijackson@chiark.greenend.org.uk>
Wed, 18 Apr 2012 17:27:03 +0000
(18:27 +0100)
lemmas.tex
patch
|
blob
|
history
diff --git
a/lemmas.tex
b/lemmas.tex
index 8509c895ec46e213c6db96ade1442d814189f2a2..40cc5f488a6403581a1561936be982097dc5327f 100644
(file)
--- a/
lemmas.tex
+++ b/
lemmas.tex
@@
-125,6
+125,23
@@
an $F''$) which disqualifies $F$ and $E$.
Otherwise, $E$ meets all the conditions for $\pends$.
}
Otherwise, $E$ meets all the conditions for $\pends$.
}
+\subsection{Single Parent Unique Tips}
+
+Unique Tips is satisfied for single-parent commits. Formally,
+given a conformant commit $A$,
+$$
+ \Big[
+ C \hasparents \{ A \}
+ \Big] \implies \left[
+ \bigforall_{P \patchisin C} \pendsof{C}{\p} = \{ T \}
+ \right]
+$$
+\proof{
+ Trivial for $C \in \p$.
+ For $C \not\in \p$, $\pancsof{C}{\p} = \pancsof{A}{\p}$,
+ so Unique Tips of $A$ suffices.
+}
+
\subsection{Ingredients Prevent Replay}
Given conformant commits $A \in \set A$,
$$
\subsection{Ingredients Prevent Replay}
Given conformant commits $A \in \set A$,
$$