notation: define \stmtmergeof and \setmergeof

diff --git a/article.tex b/article.tex
index 12d7bbcf13fad3b6a4932efb0fbb5845339a211f..7bff6920bd91db6129b61de48da10bb779183756 100644 (file)
--- 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 bb12b5ffc5e2faa17090b5b4e6dfe1a9745bb941..b5e0e9d5549c85d32514ae3e2756e56c33f7b0b2 100644 (file)
--- 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: