From 54e1d86039f0cb0e7db9e2e7be3f56a611a247f6 Mon Sep 17 00:00:00 2001 From: Ian Jackson Date: Mon, 28 May 2012 00:12:08 +0100 Subject: [PATCH] foreign notation: replace "D \text{ s.t. } \isforeign{D}" with "D \in \foreign" --- anticommit.tex | 2 +- invariants.tex | 4 ++-- lemmas.tex | 4 ++-- merge.tex | 2 +- pseudomerge.tex | 2 +- 5 files changed, 7 insertions(+), 7 deletions(-) diff --git a/anticommit.tex b/anticommit.tex index 39d13e5..b8a3993 100644 --- a/anticommit.tex +++ b/anticommit.tex @@ -131,7 +131,7 @@ Single Parent Unique Tips applies. $\qed$ \subsection{Foreign Inclusion} -Consider some $D$ s.t. $\isforeign{D}$. $D \neq C$. +Consider some $D \in \foreign$. $D \neq C$. So by Desired Contents $D \isin C \equiv D \isin L$. By Foreign Inclusion of $D$ in $L$, $D \isin L \equiv D \le L$. diff --git a/invariants.tex b/invariants.tex index 6cebb05..bb926ea 100644 --- a/invariants.tex +++ b/invariants.tex @@ -22,10 +22,10 @@ We maintain these each time we construct a new commit. \\ \bigforall_{C,\p} C \haspatch \p \implies \pendsof{C}{\py} = \{ T \} }\] \[\eqn{Foreign Inclusion}{ - \bigforall_{D \text{ s.t. } \isforeign{D}} D \isin C \equiv D \leq C + \bigforall_{D \in \foreign} D \isin C \equiv D \leq C }\] \[\eqn{Foreign Contents}{ - \bigforall_{C \text{ s.t. } \isforeign{C}} + \bigforall_{C \in \foreign} D \le C \implies \isforeign{D} }\] diff --git a/lemmas.tex b/lemmas.tex index 83fc3f6..b432f9a 100644 --- a/lemmas.tex +++ b/lemmas.tex @@ -175,12 +175,12 @@ $$ \right] \implies \left[ - \bigforall_{D \text{ s.t. } \isforeign{D}} + \bigforall_{D \in \foreign} D \isin C \equiv D \le C \right] $$ \proof{ -Consider some $D$ s.t. $\isforeign{D}$. +Consider some $D \in \foreign$. If $D = C$, trivially true. For $D \neq C$, by Foreign Inclusion of $D$ in $L$, $D \isin L \equiv D \le L$. And by Exact Ancestors $D \le L \equiv D \le C$. diff --git a/merge.tex b/merge.tex index 54f83da..b43d30f 100644 --- a/merge.tex +++ b/merge.tex @@ -280,7 +280,7 @@ $\qed$ \subsection{Foreign Inclusion} -Consider some $D$ s.t. $\isforeign{D}$. +Consider some $D \in \foreign$. By Foreign Inclusion of $L, M, R$: $D \isin L \equiv D \le L$; $D \isin M \equiv D \le M$; diff --git a/pseudomerge.tex b/pseudomerge.tex index 9318c30..0decb5f 100644 --- a/pseudomerge.tex +++ b/pseudomerge.tex @@ -25,7 +25,7 @@ but whose contents are exactly those of $L$. }\] \[ \eqn{ Foreign Unaffected }{ - \bigforall_{ D \text{ s.t. } \isforeign{D} } + \bigforall_{ D \in \foreign } \left[ \bigexists_{A \in \set A} D \le A \right] \implies D \le L -- 2.30.2