chiark
/
gitweb
/
~ian
/
topbloke-formulae.git
/ blobdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
raw
|
inline
| side by side
strategy: wip traversal.
[topbloke-formulae.git]
/
pseudomerge.tex
diff --git
a/pseudomerge.tex
b/pseudomerge.tex
index 0decb5f023c73c701f4d940c0ffc28d923791f54..0f93abc241c2d171c15c31ca4a5e5920eb003747 100644
(file)
--- a/
pseudomerge.tex
+++ b/
pseudomerge.tex
@@
-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}