notation: define \stmtmergeof and \setmergeof

[topbloke-formulae.git] / notation.tex

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: