From: Ian Jackson Date: Sun, 27 May 2012 23:20:12 +0000 (+0100) Subject: psueomerge: sort out foreign ends X-Git-Url: http://www.chiark.greenend.org.uk/ucgi/~ian/git?p=topbloke-formulae.git;a=commitdiff_plain;h=e284656ebfa338be8bc3a02de60391063d9f8f3d psueomerge: sort out foreign ends --- diff --git a/pseudomerge.tex b/pseudomerge.tex index 0decb5f..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 \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{ -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}