X-Git-Url: http://www.chiark.greenend.org.uk/ucgi/~ian/git?p=topbloke-formulae.git;a=blobdiff_plain;f=pseudomerge.tex;h=0f93abc241c2d171c15c31ca4a5e5920eb003747;hp=d884be84896b2ded5681bf2026f093c8f45db009;hb=504314d4eb8beba3ea97850f02e89500bfd9b2bf;hpb=fd4fcf610bbe38767f7aba836c233bdc46e513e3

diff --git a/pseudomerge.tex b/pseudomerge.tex
index d884be8..0f93abc 100644
--- a/pseudomerge.tex
+++ b/pseudomerge.tex
@@ -25,23 +25,15 @@ but whose contents are exactly those of $L$.
 }\]
 
 \[ \eqn{ Foreign Unaffected }{
- \bigforall_{ D \text{ s.t. } \patchof{D} = \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}
 
-$\patchof{D} = \foreign \implies \big[ D \le C \equiv D \le L \big]$.
+$\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}