From 1aa4dce9dace603365ff1b302c938b6bfe9bbc1e Mon Sep 17 00:00:00 2001
From: Ian Jackson <ijackson@chiark.greenend.org.uk>
Date: Sun, 11 Mar 2012 11:48:14 +0000
Subject: [PATCH] move alternative formulation of merge results into lemmas

---
 article.tex | 29 +++++++++++++++++------------
 1 file changed, 17 insertions(+), 12 deletions(-)

diff --git a/article.tex b/article.tex
index 28d02a0..b778663 100644
--- a/article.tex
+++ b/article.tex
@@ -171,18 +171,6 @@ $\displaystyle D \isin C \equiv
   \end{cases}
 $ 
 
-Some (overlapping) alternative formulations:
-
-$\displaystyle D \isin C \equiv
-  \begin{cases}
-    D \isin L \equiv D \isin R     : & D = C \lor D \isin L \\
-    D \isin L \equiv D \isin R     : & D = C \lor D \isin R \\
-    D \isin L \nequiv D \isin R  : & D = C \lor D \not\isin M \\
-    D \isin M \equiv D \isin L     : & D = C \lor D \isin R \\
-    D \isin M \equiv D \isin R     : & D = C \lor D \isin L \\
-  \end{cases}
-$
-
 \end{basedescript}
 \newpage
 \section{Invariants}
@@ -211,6 +199,23 @@ We maintain these each time we construct a new commit. \\
 
 \section{Some lemmas}
 
+\[ \eqn{Alternative (overlapping) formulations defining
+  $\mergeof{C}{L}{M}{R}$:}{
+ D \isin C \equiv
+  \begin{cases}
+    D \isin L  \equiv D \isin R  : & D = C \lor D \isin L     \\
+    D \isin L \nequiv D \isin R  : & D = C \lor D \not\isin M \\
+    D \isin L  \equiv D \isin M  : & D = C \lor D \isin R     \\
+    D \isin L \nequiv D \isin M  : & D = C \lor D \isin L     \\
+    \text{as above with L and R exchanged}
+  \end{cases}
+}\]
+\proof{
+  Truth table xxx
+
+  Original definition is symmetrical in $L$ and $R$.
+}
+
 \[ \eqn{Exclusive Tip Contents:}{
   \bigforall_{C \in \py} 
     \neg \Bigl[ D \isin \baseof{C} \land ( D \in \py \land D \le C )
-- 
2.30.2