chiark / gitweb /
 author Ian Jackson Sun, 27 May 2012 23:20:12 +0000 (00:20 +0100) committer Ian Jackson Sun, 27 May 2012 23:20:12 +0000 (00:20 +0100)
 pseudomerge.tex patch | blob | history

index 0decb5f..0f93abc 100644 (file)
@@ -25,23 +25,15 @@ but whose contents are exactly those of $L$.
}\]

$\eqn{ Foreign Unaffected }{ }$

$\eqn{ Foreign Unaffected }{ - \bigforall_{ D \in \foreign } - \left[ \bigexists_{A \in \set A} D \le A \right] - \implies - D \le L + \pendsof{C}{\foreign} = \pendsof{L}{\foreign} }$
}\]
- TODO THAT IS IMPOSSIBLE TO CALCULATE

\subsection{Lemma: Foreign Identical}

$\isforeign{D} \implies \big[ D \le C \equiv D \le L \big]$.

\proof{

\subsection{Lemma: Foreign Identical}

$\isforeign{D} \implies \big[ D \le C \equiv D \le L \big]$.

\proof{
-If $D \le L$, trivially $D \le C$; so conversely
-$D \not\le C \implies D \not\le L$.
-Whereas if $D \le C$, either $D \le L$ or
-$\exists{A \in \set A} D \le A$ (since $D \neq C$),
-in which case by Foreign Unaffected $D \le L$.
+Trivial by Foreign Unaffected and the definition of $\pends$
}

\subsection{No Replay}
}

\subsection{No Replay}