chiark / gitweb /
 author Ian Jackson Wed, 21 Mar 2012 18:22:59 +0000 (18:22 +0000) committer Ian Jackson Wed, 21 Mar 2012 18:22:59 +0000 (18:22 +0000)
 simple.tex patch | blob | history

index 28dc6e5..9b556ed 100644 (file)
@@ -51,7 +51,7 @@ $\qed$

Need to consider $D \in \py$

-\subsubsection{For $L \haspatch P, D = C$:}
+\subsubsection{For $L \haspatch \p, D = C$:}

Ancestors of $C$:
$D \le C$.
@@ -59,16 +59,16 @@ $D \le C$.
Contents of $C$:
$D \isin C \equiv \ldots \lor \true \text{ so } D \haspatch C$.

-\subsubsection{For $L \haspatch P, D \neq C$:}
+\subsubsection{For $L \haspatch \p, D \neq C$:}
Ancestors: $D \le C \equiv D \le L$.

Contents: $D \isin C \equiv D \isin L \lor f$
so $D \isin C \equiv D \isin L$.

So:
-$L \haspatch P \implies C \haspatch P$
+$L \haspatch \p \implies C \haspatch \p$

-\subsubsection{For $L \nothaspatch P$:}
+\subsubsection{For $L \nothaspatch \p$:}

Firstly, $C \not\in \py$ since if it were, $L \in \py$.
Thus $D \neq C$.
@@ -76,7 +76,7 @@ Thus $D \neq C$.
Now by contents of $L$, $D \notin L$, so $D \notin C$.

So:
-$L \nothaspatch P \implies C \nothaspatch P$
+$L \nothaspatch \p \implies C \nothaspatch \p$
$\qed$

\subsection{Foreign Inclusion:}