chiark / gitweb /
 author Ian Jackson Thu, 8 Mar 2012 16:40:16 +0000 (16:40 +0000) committer Ian Jackson Thu, 8 Mar 2012 16:40:16 +0000 (16:40 +0000)
 article.tex patch | blob | history

index b2f943b..080e482 100644 (file)
@@ -491,10 +491,13 @@ We will occasionally use $X,Y$ s.t. $\{X,Y\} = \{L,R\}$.
$\eqn{ Merge Ends }{ X \not\haspatch \p \land Y \haspatch \p - \implies \left[ - \bigforall_{E \in \pendsof{X}{\py}} - E \le Y - \right] + \implies + \begin{cases} + M \haspatch \p : & \displaystyle + \bigforall_{E \in \pendsof{Y}{\py}} E \le M \\ + M \nothaspatch \p : & \displaystyle + \bigforall_{E \in \pendsof{X}{\py}} E \le Y + \end{cases} }$

\subsection{No Replay}
@@ -599,22 +602,8 @@ Transitive Ancestors $D \le Y$ --- a contradiction, so $D \not\le X$.
Thus $D \not\le C$.  By $\merge$, $D \not\isin C$.  OK.

Consider $D \neq C, M \haspatch P, D \isin Y$:
-$D \le Y$ so $D \le M$
-
-%anyway     D \not\isin X
-%           D \isin Y
-%           D \le Y
-
-%           D \not\le M
-%           D \not\isin M
-% results
-%           D \isin C    wrong
-
-%ok case
-%           D \le M
-%           D \isin M
-% results
-%           D \not\isin C  OK
+$D \le Y$ so $D \in \pancsof{Y}{\py}$ so by Merge Ends
+and Transitive Ancestors $D \le M$.
+Thus $D \isin M$.  By $\merge$, $D \not\isin C$.  OK.

\end{document}