From 3633c1fc18eec0733f3f64a119041795cf4d8c28 Mon Sep 17 00:00:00 2001 From: Ian Jackson Date: Wed, 21 Mar 2012 18:20:04 +0000 Subject: [PATCH] wip exclusive haspatch - fix Tip Own Contents --- lemmas.tex | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/lemmas.tex b/lemmas.tex index 44dd260..efffe6b 100644 --- a/lemmas.tex +++ b/lemmas.tex @@ -56,7 +56,7 @@ So by Base Acyclic $D \isin B \implies D \notin \py$. \subsection{Tip Own Contents} Given Base Acyclic for $C$, $$ - \bigforall_{C \in \py} C \haspatch \p \land \neg[ C \nothaspatch \p ] + \bigforall_{C \in \py} C \haspatch \p $$ Ie, tip commits contain their own patch. @@ -64,8 +64,8 @@ Ie, tip commits contain their own patch. Apply Exclusive Tip Contents to some $D \in \py$: $ \bigforall_{C \in \py}\bigforall_{D \in \py} D \isin C \equiv D \le C $. -Thus $C \haspatch \p$. -And, since $C \le C$, $C \isin C$. Therefore $\neg[ C \nothaspatch \p ]$ +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} -- 2.30.2