chiark / gitweb /
 author Ian Jackson Sun, 11 Mar 2012 11:04:59 +0000 (11:04 +0000) committer Ian Jackson Sun, 11 Mar 2012 11:04:59 +0000 (11:04 +0000)
 article.tex patch | blob | history

index 5459b88..0f1a24b 100644 (file)
@@ -559,7 +559,7 @@ That is, $\baseof{C} = R$.

$\qed$

-\subsection{Coherence and patch inclusion}
+\subsection{Coherence and Patch Inclusion}

Need to determine $C \haspatch \p$ based on $L,M,R \haspatch \p$.
This involves considering $D \in \py$.
@@ -647,13 +647,13 @@ R$. And$D \neq C$. So$D \not\isin C$.$\qed$We need worry only about$C \in \py$. And$\patchof{C} = \patchof{L}$-so$L \in \py$so$L \haspatch \p$. We will use the unique base, -and coherence and patch inclusion, of$C$as just proved. +so$L \in \py$so$L \haspatch \p$. We will use the Unique Base +of$C$, and its Coherence and Patch Inclusion, as just proved. Firstly we show$C \haspatch \p$: If$R \in \py$, then$R \haspatch
-\p$and by coherence/inclusion$C \haspatch \p$. If$R \not\in \py$+\p$ and by Coherence/Inclusion $C \haspatch \p$ .  If $R \not\in \py$
then by Tip Merge $M = \baseof{L}$ so by Base Acyclic and definition
-of $\nothaspatch$, $M \nothaspatch \p$.  So by coherence/inclusion $C +of$\nothaspatch$,$M \nothaspatch \p$. So by Coherence/Inclusion$C
\haspatch \p$(whether$R \haspatch \p$or$\nothaspatch$). We will consider some$D\$ and prove the Exclusive Tip Contents form.