From b4e0205d32b8d7fd7176523f07f5acb8cff6df02 Mon Sep 17 00:00:00 2001 From: Ian Jackson Date: Sun, 11 Mar 2012 14:21:01 +0000 Subject: [PATCH] fix up some lemmas re ends --- article.tex | 9 ++++++++- 1 file changed, 8 insertions(+), 1 deletion(-) diff --git a/article.tex b/article.tex index 9a0cf07..b4f7beb 100644 --- a/article.tex +++ b/article.tex @@ -254,6 +254,7 @@ $\bigforall_{C \in \py}\bigforall_{D \in \py} ( \mathop{\hbox{\huge{$\vee\$}}}_{R \in \set R} D \le R ) \lor D = C }\] +xxx proof tbd $\eqn{Transitive Ancestors:}{ \left[ \bigforall_{ E \in \pendsof{C}{\set P} } E \le M \right] \equiv @@ -272,17 +273,23 @@ in which case we repeat for A'. Since there are finitely many commits, this terminates with A'' \in \pends(), ie A'' \le M by the LHS. And A \le A''. } + \[ \eqn{Calculation Of Ends:}{ \bigforall_{C \hasparents \set A} \pendsof{C}{\set P} = + \begin{cases} + C \in \p : & \{ C \} + \\ + C \not\in \p : & \displaystyle \left\{ E \Big| \Bigl[ \Largeexists_{A \in \set A} E \in \pendsof{A}{\set P} \Bigr] \land \Bigl[ \Largenexists_{B \in \set A} E \neq B \land E \le B \Bigr] \right\} + \end{cases} }$ -XXX proof TBD. +xxx proof tbd \subsection{No Replay for Merge Results} -- 2.1.4