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

index 47e0a9b..90304e0 100644 (file)
@@ -61,7 +61,7 @@ $D \not\isin R^-$.  Thus $D \not\isin C$.  OK.

By Currently Included, $D \isin L$.

-By Tip Self Contents for $R^+$, $D \isin R^+ \equiv D \le R^+$, but by
+By Tip Own Contents for $R^+$, $D \isin R^+ \equiv D \le R^+$, but by
by Unique Tip, $D \le R^+ \equiv D \le L$.
So $D \isin R^+$.

index 044e937..44dd260 100644 (file)
@@ -53,7 +53,7 @@ So by Base Acyclic $D \isin B \implies D \notin \py$.
\end{cases}
}\]

-\subsection{Tip Self Contents}
+\subsection{Tip Own Contents}
Given Base Acyclic for $C$,

\bigforall_{C \in \py} C \haspatch \p \land \neg[ C \nothaspatch \p ]
index 6786dd0..2403a49 100644 (file)
--- a/merge.tex
+++ b/merge.tex
@@ -117,7 +117,7 @@ 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 $\neg[ L \nothaspatch \p ]$ by Tip Self Contents for $L$).
+\in \py$ie$\neg[ L \nothaspatch \p ]$by Tip Own Contents for$L$). So$D \neq C$. Applying$\merge$gives$D \not\isin C$i.e.$C \nothaspatch \p$. @@ -162,7 +162,7 @@ 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 Self Contents,$\neg[ L \nothaspatch \p ]$so$L \neq X$, +By Tip Own Contents,$\neg[ L \nothaspatch \p ]$so$L \neq X$, 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\$,