chiark / gitweb /
 author Ian Jackson Fri, 16 Mar 2012 23:00:00 +0000 (23:00 +0000) committer Ian Jackson Fri, 16 Mar 2012 23:00:00 +0000 (23:00 +0000)
 merge.tex patch | blob | history

@@ -115,7 +115,8 @@ This involves considering $D \in \py$.
\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 for $L$).  So $D \neq C$.
+\in \py$ie$\neg[ L \nothaspatch \p ]$by Tip Self Inpatch for$L$). +So$D \neq C$. Applying$\merge$gives$D \not\isin C$i.e.$C \nothaspatch \p$. \subsubsection{For$L \haspatch \p, R \haspatch \p$:} @@ -158,9 +159,9 @@ We will show for each of various cases that$D \isin C \equiv M \nothaspatch \p \land D \le C$(which suffices by definition of$\haspatch$and$\nothaspatch$). -Consider$D = C$: Thus$C \in \py, L \in \py$. By Tip Contents -for$L$,$L \isin L$so$\neg [ L \nothaspatch \p ]$. -Therefore we must have$L=Y$,$R=X$. +Consider$D = C$: Thus$C \in \py, L \in \py$. +By Tip Self Inpatch,$\neg[ L \nothaspatch \p ]$so$L \neq R$, +therefore we must have$L=Y$,$R=X$. By Tip Merge$M = \baseof{L}$so$M \in \pn$so by Base Acyclic$M \nothaspatch \p$. By$\merge$,$D \isin C$, and$D \le C$, consistent with$C \haspatch \p\$.  OK.