From 6256831867d9cb3c135bbc73dad80db2a8677754 Mon Sep 17 00:00:00 2001
From: Ian Jackson <ijackson@chiark.greenend.org.uk>
Date: Sat, 7 Jul 2012 17:23:02 +0100
Subject: [PATCH 1/1] notation: define \stmtmergeof and \setmergeof

---
 article.tex  |  1 +
 notation.tex | 26 ++++++++++++++++++++++++++
 2 files changed, 27 insertions(+)

diff --git a/article.tex b/article.tex
index 12d7bbc..7bff692 100644
--- a/article.tex
+++ b/article.tex
@@ -111,6 +111,7 @@
 \newcommand{\alg}[1]{\text{\bf #1}}
 \newcommand{\setmerge}{\alg{merge}}
 \newcommand{\setmergeof}[3]{\setmerge\mergeof{#1}{#2}{#3}}
+\newcommand{\stmtmergeof}[3]{\setmerge\mergeof{#1}{#2}{#3}}
 
 %\newcommand{\setmergeof}[3]{\setmerge\left\lgroup #1 \;\middle\lmoustache\; #2 \;\middle\rmoustache\; #3 \right\rgroup}
 %\newcommand{\setmergeof}[3]{\setmerge\left\rmoustache #1 \middle\rmoustache #2 \middle\lmoustache #3 \right\lmoustache}
diff --git a/notation.tex b/notation.tex
index bb12b5f..b5e0e9d 100644
--- a/notation.tex
+++ b/notation.tex
@@ -86,6 +86,32 @@ the relevant Topbloke branches, we hope that
 if the user still cares about the Topbloke patch,
 git's merge algorithm will DTRT when trying to re-apply the changes.
 
+\item[ $\displaystyle \stmtmergeof{L}{M}{R} $ ]
+The proper results of a merge.  Formally,
+where $L$, $M$ and $R$ are statements:
+
+$$
+  \stmtmergeof{L}{M}{R}
+    \equiv
+  \begin{cases}
+         (L \land R)      : & \true \\
+    (\neg L \land \neg R) : & \false \\
+    \text{otherwise} : & \neg M
+  \end{cases}
+$$
+
+May also be used where $L$, $M$ and $R$ are sets, in which case
+$$
+  \setmergeof{L}{M}{R}
+     =
+  \left\{
+    \;
+    D \; \middle| \;
+      \setmergeof{ D \in L }{ D \in M }{ D \in R }
+    \;
+  \right\}
+$$
+
 \item[ $\displaystyle \commitmergeof{C}{L}{M}{R} $ ]
 The contents of a git merge result:
 
-- 
2.30.2