From e600e19a18c0f5b4595c68dd305f093b62fed9e4 Mon Sep 17 00:00:00 2001 From: Ian Jackson Date: Tue, 6 Mar 2012 17:46:30 +0000 Subject: [PATCH] use \p rather than just P --- article.tex | 24 ++++++++++++------------ 1 file changed, 12 insertions(+), 12 deletions(-) diff --git a/article.tex b/article.tex index 2f512f4..6a5023c 100644 --- a/article.tex +++ b/article.tex @@ -536,19 +536,19 @@ $\qed$ \subsection{Coherence and patch inclusion} -Need to determine $C \haspatch P$ based on $L,M,R \haspatch P$. +Need to determine $C \haspatch \p$ based on $L,M,R \haspatch \p$. This involves considering $D \in \py$. -\subsubsection{For $L \nothaspatch P, R \nothaspatch P$:} +\subsubsection{For $L \nothaspatch \p, R \nothaspatch \p$:} $D \not\isin L \land D \not\isin R$. $C \not\in \py$ (otherwise $L -\in \py$ ie $L \haspatch P$ by Tip Self Inpatch). So $D \neq C$. -Applying $\merge$ gives $D \not\isin C$ i.e. $C \nothaspatch P$. +\in \py$ie$L \haspatch \p$by Tip Self Inpatch). So$D \neq C$. +Applying$\merge$gives$D \not\isin C$i.e.$C \nothaspatch \p$. -\subsubsection{For$L \haspatch P, R \haspatch P$:} +\subsubsection{For$L \haspatch \p, R \haspatch \p$:}$D \isin L \equiv D \le L$and$D \isin R \equiv D \le R$. (Likewise$D \isin X \equiv D \le X$and$D \isin Y \equiv D \le Y$.) -Consider$D = C$:$D \isin C$,$D \le C$, OK for$C \haspatch P$. +Consider$D = C$:$D \isin C$,$D \le C$, OK for$C \haspatch \p$. For$D \neq C$:$D \le C \equiv D \le L \lor D \le R \equiv D \isin L \lor D \isin R$. @@ -556,23 +556,23 @@ For$D \neq C$:$D \le C \equiv D \le L \lor D \le R Consider $D \neq C, D \isin X \land D \isin Y$: By $\merge$, $D \isin C$. Also $D \le X$ -so $D \le C$. OK for $C \haspatch P$. +so $D \le C$. OK for $C \haspatch \p$. Consider $D \neq C, D \not\isin X \land D \not\isin Y$: By $\merge$, $D \not\isin C$. And $D \not\le X \land D \not\le Y$ so $D \not\le C$. -OK for $C \haspatch P$. +OK for $C \haspatch \p$. Remaining case, wlog, is $D \not\isin X \land D \isin Y$. $D \not\le X$ so $D \not\le M$ so $D \not\isin M$. Thus by $\merge$, $D \isin C$. And $D \le Y$ so $D \le C$. -OK for $C \haspatch P$. +OK for $C \haspatch \p$. -So indeed $L \haspatch P \land R \haspatch P \implies C \haspatch P$. +So indeed $L \haspatch \p \land R \haspatch \p \implies C \haspatch \p$. -\subsubsection{For (wlog) $X \not\haspatch P, Y \haspatch P$:} +\subsubsection{For (wlog) $X \not\haspatch \p, Y \haspatch \p$:} -$C \haspatch P \equiv C \nothaspatch M$. +$C \haspatch \p \equiv C \nothaspatch M$. \proofstarts -- 2.1.4