diff --git a/assets/shorthands.tex b/assets/shorthands.tex
index d2cdca7..5574d76 100644
--- a/assets/shorthands.tex
+++ b/assets/shorthands.tex
@@ -8,8 +8,6 @@
 \newcommand{\cml}{\gls{constraint-modelling} language\xspace{}}
 \newcommand{\cmls}{\gls{constraint-modelling} languages\xspace{}}
 
-\newcommand{\vari}{\mzninline{var}}
-\newcommand{\pari}{\mzninline{par}}
 \renewcommand{\phi}{\varphi}
 \newcommand{\tuple}[1]{\ensuremath{\langle #1 \rangle}}
 \newcommand{\Prog}{\ensuremath{\mathcal{P}}}
@@ -17,17 +15,11 @@
 \newcommand{\Env}{\ensuremath{\sigma}}
 \newcommand{\Sem}[2]{\ptinline{[\!\![#1]\!\!]\tuple{#2}}}
 \newcommand{\Cbind}{\ensuremath{\wedge}}
-\newcommand{\true}{\mzninline{true}}
-\newcommand{\false}{\mzninline{false}}
-
-\newcommand{\mdiv}{\mzninline{div}}
-\newcommand{\element}{\mzninline{element}}
-\newcommand{\alldiff}{\mzninline{all_different}}
 
 % Half-reification math things
 
-\newcommand{\VV}{{\cal V}}
-\newcommand{\PP}{{\cal P}}
+\newcommand{\VV}{{\cal\ V}}
+\newcommand{\PP}{{\cal\ P}}
 \newcommand{\range}[2]{\left[\,#1\,..\,#2\,\right]}
 \newcommand{\gfp}{\textup{gfp}}
 \newcommand{\lfp}{\textup{lfp}}
diff --git a/chapters/4_rewriting.tex b/chapters/4_rewriting.tex
index 0c2aed5..7ace930 100644
--- a/chapters/4_rewriting.tex
+++ b/chapters/4_rewriting.tex
@@ -134,7 +134,7 @@ have omitted the definitions of \syntax{<type-inst>} and \syntax{<ident>}, which
 you can assume to be the same as in the definition of \minizinc. While we omit
 the typing rules here for space reasons, we will assume that in well-typed
 \microzinc\ programs, the conditions \syntax{<exp>} in if-then-else and where
-expressions have \pari\ type.
+expressions have \mzninline{par} type.
 
 \begin{figure}
   \begin{grammar}
@@ -353,13 +353,14 @@ that introduces the variable.
 A \nanozinc\ model (\cref{fig:4-nzn-syntax}) consists of a topologically-ordered
 list of definitions. Each definition binds a variable to the result of a call or
 another variable, and it is associated with a list of identifiers of auxiliary
-constraints. The \nanozinc\ model contains a special definition $\true$,
-containing all ``root-context'' constraints of the model, i.e., those that have
-to hold globally and are not just used to define an auxiliary variable. Only
-root-context constraints (attached to $\true$) can effectively constrain the
-overall problem. Constraints attached to definitions originate from function
-calls, and since all functions are guaranteed to be total, attached constraints
-can only define the function result.
+constraints. The \nanozinc\ model contains a special definition
+\mzninline{true}, containing all ``root-context'' constraints of the model,
+i.e., those that have to hold globally and are not just used to define an
+auxiliary variable. Only root-context constraints (attached to \mzninline{true})
+can effectively constrain the overall problem. Constraints attached to
+definitions originate from function calls, and since all functions are
+guaranteed to be total, attached constraints can only define the function
+result.
 
 \begin{example}\label{ex:4-absnzn}
 
diff --git a/chapters/5_half_reif.tex b/chapters/5_half_reif.tex
index 786249b..8af06ce 100644
--- a/chapters/5_half_reif.tex
+++ b/chapters/5_half_reif.tex
@@ -13,7 +13,7 @@ formulated. Modelling languages map the more expressive formulations to
 existentially quantified conjunction through a combination of loop unrolling,
 and flattening using reification.
 
-\begin{example}\label{ex:cons}
+\begin{example}\label{ex:hr-cons}
   Consider the following ``complex constraint'' written in \minizinc\ syntax
 
   \begin{mzn}
@@ -74,7 +74,7 @@ This is known as the \emph{strict} semantics
 The usual choice for modeling partial functions in modelling languages is the
 \emph{relational} semantics \autocite{frisch-2009-undefinedness}. In the
 relational semantics the value $\bot$ percolates up through the term until it
-reaches a Boolean subterm where it becomes $\false$. For the example
+reaches a Boolean subterm where it becomes $\mzninline{false}$. For the example
 
 \begin{mzn}
 /* t1 @\(\equiv\)@ */ a[7] = ⊥;
@@ -91,7 +91,7 @@ original complex constraint needs to be far more complex.
   The \minizinc\ compiler unrolls, flattens, and reifies \minizinc\ models
   implementing the relational semantics. Assuming \texttt{i} takes values in the
   set \mzninline{1..8}, and \texttt{a} has an index set \mzninline{1..5}, its
-  translation of the constraint in \cref{ex:cons} is
+  translation of the constraint in \cref{ex:hr-cons} is
 
   \begin{mzn}
     constraint b1 <-> i <= 4;   % b1 holds iff i <= 4
@@ -120,7 +120,7 @@ functions, is that each reified version of a constraint requires further
 implementation to create, and indeed most solvers do not provide any reified
 versions of their global constraints.
 
-\begin{example}\label{ex:alldiff}
+\begin{example}\label{ex:hr-alldiff}
   Consider the complex constraint
 
   \begin{mzn}
@@ -201,19 +201,22 @@ expressiveness in using global constraints.
 
 \section{Propagation Based Constraint Solving}
 
+\jip{This section looks like background and should probably be moved}
+
 We consider a typed set of variables $\VV = \VV_I \cup \VV_B$ made up of
 \emph{integer} variables, $\VV_I$, and \emph{Boolean} variables, $\VV_b$. We use
 lower case letters such as $x$ and $y$ for integer variables and letters such as
 $b$ for Booleans.
 %
-A \emph{domain} $D$ is a complete mapping from $\VV$ to finite sets of integers
-(for the variables in $\VV_I$) and to subsets of $\{\true,\false\}$ (for the
-variables in $\VV_b$).
+A \gls{domain} $D$ is a complete mapping from $\VV$ to finite sets of integers
+(for the variables in $\VV_I$) and to subsets of
+$\{\mzninline{true},\mzninline{false}\}$ (for the variables in $\VV_b$).
 %
-We can understand a domain $D$ as a formula $\wedge_{v \in \VV} (v \in D(v))$
-stating for each variable $v$ that its value is in its domain. A \emph{false
-  domain} $D$ is a domain where $\exists_{v \in \VV} D(v) = \emptyset$, and
-corresponds to an unsatisfiable formula.
+We can understand a \gls{domain} $D$ as a formula
+$\wedge_{v \in \VV} (v \in D(v))$ stating for each variable $v$ that its value
+is in its domain. A \emph{false domain} $D$ is a domain where
+$\exists_{v \in \VV} D(v) = \emptyset$, and corresponds to an unsatisfiable
+formula.
 
 Let $D_1$ and $D_2$ be domains and $V\subseteq\VV$. We say that $D_1$ is
 \emph{stronger} than $D_2$, written $D_1 \sqsubseteq D_2$, if
@@ -281,7 +284,7 @@ $\theta \in solns(c) \cap D$ s.t. $\theta(v_i) = \min D(v_i)$ and
 $\min D(v_j) \leq \theta(v_j) \leq \max D(v_j), 1 \leq j \neq i \leq n$, and
 similarly exists $\theta \in solns(c) \cap D$ s.t. $\theta(v_i) = \max D(v_i)$
 and $\min D(v_j) \leq \theta(v_j) \leq \max D(v_j), 1 \leq j \neq i \leq n$. For
-Boolean variables $v$ we assume $\false < \true$.
+Boolean variables $v$ we assume $\mzninline{false} < \mzninline{true}$.
 
 % A domain $D$ is \emph{bounds(R) consistent} for constraint $c$ if the same
 % conditions as for bounds(Z) consistency hold except $\theta \in solns(c')$ where
@@ -323,7 +326,10 @@ fixpoint w.r.t $\sqsubseteq$ lifted to functions.
 % not going up from an empty one.)
 
 
-\subsection{A Language of Constraints}\label{sec:syntax}
+\subsection{A Language of Constraints}\label{sec:hr-syntax}
+
+\jip{This introduces a subset of \minizinc, but we can probably use \microzinc\
+  instead.}
 
 \newcommand{\nonterm}[1]{\textsc{#1}}
 \newcommand{\subs}[1]{[\![ #1 ]\!] }
@@ -414,13 +420,13 @@ Given a \syntax{<cons>} term defining the constraints of the model we can split
 its \syntax{<cons>} subterms as occurring in different kinds of places: root
 contexts, positive contexts, negative contexts, and mixed contexts. A Boolean
 subterm $t$ of constraint $c$ is in a \emph{root context} iff there is no
-solution of $c\subs{t/\false}$, that is $c$ with subterm $t$ replaced by
-$\false$.\footnote{For the definitions of context we assume that the subterm $t$
+solution of $c\subs{t/\mzninline{false}}$, that is $c$ with subterm $t$ replaced by
+$\mzninline{false}$.\footnote{For the definitions of context we assume that the subterm $t$
   is uniquely defined by its position in $c$, so the replacement is of exactly
   one subterm.} Similarly, a subterm $t$ of constraint $c$ is in a
 \emph{positive context} iff for any solution $\theta$ of $c$ then $\theta$ is
-also a solution of $c\subs{t/\true}$; and a \emph{negative context} iff for any
-solution $\theta$ of $c$ then $\theta$ is also a solution of $c\subs{t/\false}$.
+also a solution of $c\subs{t/\mzninline{true}}$; and a \emph{negative context} iff for any
+solution $\theta$ of $c$ then $\theta$ is also a solution of $c\subs{t/\mzninline{false}}$.
 The remaining Boolean subterms of $c$ are in \emph{mixed} contexts. While
 determining contexts according to these definitions is hard, there are simple
 syntactic rules which can determine the correct context for most terms, and the
@@ -432,7 +438,7 @@ Consider the constraint expression
   constraint x > 0 /\ (i <= 4 -> x + bool2int(b) = 5);
 \end{mzn}
 
-then $x > 0$ is in the root context, $i \leq 4$ is in a negative context,
+then \mzninline{x > 0} is in the root context, $i \leq 4$ is in a negative context,
 $x + \texttt{bool2int}(b) = 5$ is in a positive context, and $b$ is in a mixed
 context. If the last equality were $x + \texttt{bool2int}(b) \geq 5$ then $b$
 would be in a positive context.
@@ -452,10 +458,10 @@ for each subterm bottom up using approximation.
 % \cons{} subterms as occurring in kinds of places: positive contexts, negative
 % contexts, and mixed contexts. A Boolean subterm $t$ of constraint $c$, written
 % $c[t]$, is in a \emph{positive context} iff for any solution $\theta$ of $c$
-% then $\theta$ is also a solution of $c[\true]$, that is $c$ with subterm $t$
-% replaced by $\true$. Similarly, a subterm $t$ of constraint $c$ is in a
+% then $\theta$ is also a solution of $c[\mzninline{true}]$, that is $c$ with subterm $t$
+% replaced by $\mzninline{true}$. Similarly, a subterm $t$ of constraint $c$ is in a
 % \emph{negative context} iff for any solution $\theta$ of $c$ then $\theta$ is
-% also a solution of $c[\false]$. The remaining Boolean subterms of $c$ are in
+% also a solution of $c[\mzninline{false}]$. The remaining Boolean subterms of $c$ are in
 % mixed contexts.
 
 % \begin{example}
@@ -486,7 +492,7 @@ set of possible values of $t$ are included in the domain of $a$,
 $poss(t) \subseteq \dom(a)$.
 
 \section{Flattening with Full Reification}
-\label{sec:translation}
+\label{sec:hr-translation}
 
 Constraint problems formulated in \minizinc\ are solved by translating them to a
 simpler, solver-specific subset of \minizinc, called \flatzinc. \flatzinc
@@ -534,13 +540,13 @@ detailed discussion) but makes the pseudo-code much longer.
 
 The complex part of flattening arises in flattening the constraints, we shall
 ignore the declarations part for flattening and assume that any objective
-function term $e$ is replaced by a new variable $obj$ and a constraint item
-$\texttt{constraint}~obj = e$ which will then be flattened as part of the
-model.
+function term \mzninline{e} is replaced by a new variable \mzninline{obj} and a
+constraint item \mzninline{constraint obj = e} which will then be flattened as
+part of the model.
 
 \subsection{Flattening Constraints}
 
-Flattening a constraint $c$ in context $\ctxt$, $\flatc(c,\ctxt)$, returns a
+Flattening a constraint $c$ in context \ctxt, $\flatc(c,\ctxt)$, returns a
 Boolean literal $b$ representing the constraint and as a side effect adds a set
 of constraints (the flattening) $S$ to the store such that
 $S \models b \full c$.
@@ -616,7 +622,7 @@ actual flattening rules only differentiate between $\rootc$ and other contexts.
 The importance of the $\pos$ context is that \texttt{let} expressions within a
 $\pos$ context can declare new variables. The important of the $\negc$ context
 is to track $\pos$ context arising under double negations. Note that flattening
-in the root context always returns a Boolean $b$ made equivalent to $\true$ by
+in the root context always returns a Boolean $b$ made equivalent to $\mzninline{true}$ by
 the constraints in $S$. For succinctness we use the notation $\new b$ ($\new v$)
 to introduce a fresh Boolean (resp.\ integer) variable and return the name of
 the variable.
@@ -628,7 +634,7 @@ again. We retrieve the result of the previous flattening $h$ and the previous
 context $prev$. If the expression previously appeared at the root then we simply
 reuse the old value, since regardless of the new context the expression must
 hold. If the new context is $\rootc$ we reuse the old value but require it to be
-$\true$ in $S$, and modify the hash table to record the expression appears at
+$\mzninline{true}$ in $S$, and modify the hash table to record the expression appears at
 the root. If the expression appeared in a mixed context we simply reuse the old
 result since this is the most constrained context. Similarly if the previous
 context is the same as the current one we reuse the old result. In the remaining
@@ -683,7 +689,7 @@ expression using function \textsf{flatlet} which returns the extracted
 constraint and a rewritten term (not used in this case, but used in \flatt{}).
 The constraints returned by function \textsf{flatlet} are then flattened.
 Finally if we are in the root context, we ensure that the Boolean $b$ returned
-must be $\true$ by adding $b$ to $S$.
+must be $\mzninline{true}$ by adding $b$ to $S$.
 
 {
 \begin{tabbing}
@@ -701,8 +707,8 @@ $\tuple{h,\rootc}$;  \textbf{return} $h$
 \> \textbf{if} ($\fixed(c)$) $b$ := $\eval(c)$ \\
 \> \textbf{else} \\
 \> \> \textbf{switch} $c$ \\
-%\> \> \textbf{case} \texttt{true}: $b$ := $\true$;\\
-%\> \> \textbf{case} \texttt{false}: $b$ := $\false$;\\
+%\> \> \textbf{case} \texttt{true}: $b$ := $\mzninline{true}$;\\
+%\> \> \textbf{case} \texttt{false}: $b$ := $\mzninline{false}$;\\
 \> \> \textbf{case} $b'$ (\syntax{<bvar>}): $b$ := $b'$; \\
 \> \> \textbf{case} $t_1$ $r$ $t_2$ (\syntax{<relop>}):  \\
 \>\>\> $\tuple{v_1, b_1}$ := $\flatt(t_1,\ctxt)$;
@@ -739,7 +745,7 @@ $S$ \cupp  $\{ \new b \full (\flatc(c_1,\mix) \full
 %\mathit{safeelement}(v, [b_1, \ldots, b_n],  b'),
 %b'' \full v \in \{1,..,n\} \} $ \\
 \>\>\> \textbf{if} ($\ctxt = \rootc$) $S$ \cupp $\{\texttt{element}(v', [b_1, \ldots, b_n],
-\true)\}$; $b$ := $\true$  \\
+\mzninline{true})\}$; $b$ := $\mzninline{true}$  \\
 \>\>\> \textbf{else} \\
 \>\>\>\> $S$ \cupp
 $\{ \new b \full (b_{n+1} \wedge \new b' \wedge \new b''), \new v' \in \{1,
@@ -755,7 +761,7 @@ b'' \full v  = v', b'' \full v \in \{1,\ldots,n\} \} $
 \> \> \> \> \textbf{else} $S$ \cupp $\{ p\_reif(v_1,\ldots,v_n,\new b'),
 \new b \Leftrightarrow b' \wedge \bigwedge_{j=1}^n b_j\}$ \\
 \> \> \> \textbf{else} \\
-\>\> \> \> $b$ := $\true$; $S$ \cupp  $\{ p(v_1, \ldots, v_n) %, \bigwedge_{j=1}^n b_j
+\>\> \> \> $b$ := $\mzninline{true}$; $S$ \cupp  $\{ p(v_1, \ldots, v_n) %, \bigwedge_{j=1}^n b_j
 \}$
 \\
 \>\> \textbf{case} $p$ ($t_1, \ldots, t_n$) (\syntax{<pred>}): user-defined predicate \\
@@ -771,7 +777,7 @@ b_j\}$
 \>\> \textbf{case} $p$ ($t_1, \ldots, t_n$) (\syntax{<pred>}) built-in predicate: \\
 \> \> \> \textbf{if} ($\ctxt \neq \rootc$) \textbf{abort} \\
 \> \> \> \textbf{foreach}($j \in 1..n$) $\tuple{v_j, \_}$ := $\flatt(t_j,\rootc)$; \\
-\>\> \> $b$ := $\true$; $S$ \cupp  $\{ p(v_1, \ldots, v_n)\}$
+\>\> \> $b$ := $\mzninline{true}$; $S$ \cupp  $\{ p(v_1, \ldots, v_n)\}$
 \\
 \>\> \textbf{case} $p$ ($t_1, \ldots, t_n$) (\syntax{<pred>}): user-defined predicate \\
 \>\> \> \textbf{let} $p(x_1, \ldots, x_n) = c_0$ be defn of $p$ \\
@@ -886,7 +892,7 @@ $\flatt(t,\ctxt)$ flattens an integer term $t$ in context $\ctxt$. It returns a
 tuple $\tuple{v,b}$ of an integer variable/value $v$ and a Boolean literal $b$,
 and as a side effect adds constraints to $S$ so that
 $S \models b \full (v = t)$. Note that again flattening in the root context
-always returns a Boolean $b$ made equivalent to $\true$ by the constraints in
+always returns a Boolean $b$ made equivalent to $\mzninline{true}$ by the constraints in
 $S$.
 
 Flattening first checks if the same expression has been flattened previously and
@@ -936,13 +942,13 @@ $\tuple{h,b',\rootc}$;  \textbf{return} $\tuple{h,b'}$
 \>\> \textbf{if} ($prev = \mix \vee prev = \ctxt$)
 \textbf{return} $\tuple{h,b'}$  \\
 \>\> $\ctxt$ := $\mix$ \\
-\> \textbf{if} ($\fixed(t)$) $v$ := $\eval(t)$; $b$ := $\true$ \\
+\> \textbf{if} ($\fixed(t)$) $v$ := $\eval(t)$; $b$ := $\mzninline{true}$ \\
 \> \textbf{else} %\\
 %% \> \> \textbf{if} ($t$ is marked \emph{total}) $\ctxt$ := $\rootc$ \\
 %\> \>
 \textbf{switch} $t$ \\
-%\> \> \textbf{case} $i$ (\intc): $v$ := $i$; $b$ := $\true$ \\
-\> \> \textbf{case} $v'$ (\syntax{<ivar>}):  $v$ := $v'$; $b$ := $\true$\\
+%\> \> \textbf{case} $i$ (\intc): $v$ := $i$; $b$ := $\mzninline{true}$ \\
+\> \> \textbf{case} $v'$ (\syntax{<ivar>}):  $v$ := $v'$; $b$ := $\mzninline{true}$\\
 \> \> \textbf{case} $t_1$ $a$ $t_2$ (\syntax{<arithop>}): \\
 \> \> \>
 $\tuple{v_1,b_1}$ := $\flatt(t_1,\ctxt)$;
@@ -1035,14 +1041,16 @@ $S$ \cupp $\{ \new b \full (b_1 \wedge b_2)\}$
 \> \textbf{return} $\tuple{v,b}$
 \end{tabbing}
 
-\begin{example}\label{ex:flat}
+\begin{example}\label{ex:hr-flat}
   Consider the flattening of the expression
   $$
   a[x] + bool2int(x > y) - bool2int(x > z) \geq 4 \vee
   (a[x] \leq 2 \wedge x > y \wedge (x > z \rightarrow b))
   $$
-  The different terms and subterms of the expression are
-  illustrated and numbered in Figure~\ref{fig:tree}.
+
+  The different terms and subterms of the expression are illustrated and
+  numbered in \cref{fig:hr-tree}.
+
   \begin{figure}[t]
     $$
     \xymatrix@R=1em@C=0.6em{
@@ -1060,7 +1068,7 @@ $S$ \cupp $\{ \new b \full (b_1 \wedge b_2)\}$
     }
     $$
     \caption{An expression to be flattened with non-leaf (sub-)terms
-      numbered.\label{fig:tree}}
+      numbered.\label{fig:hr-tree}}
   \end{figure}
   Note that positions 0 is in the $\rootc$ context, while position 10 is in a
   $\negc$ context, positions 13 and 15 are in a $\mix$ context, and the rest are
@@ -1171,7 +1179,7 @@ $S$ \cupp $\{ \new b \full (b_1 \wedge b_2)\}$
 
 % The pseudo-code for \flatc($b$,$c$) flattens a constraint expression $c$ to be
 % equal to $b$, returning a set of constraints implementing $b \full c$. We
-% flatten a whole model $c$ using $\flatc(\true, c)$. In the pseudo-code the
+% flatten a whole model $c$ using $\flatc(\mzninline{true}, c)$. In the pseudo-code the
 % expressions $\new b$ and $\new v$ create a new Boolean and integer variable
 % respectively.
 
@@ -1193,8 +1201,8 @@ $S$ \cupp $\{ \new b \full (b_1 \wedge b_2)\}$
 % \> \textbf{case} \texttt{not} $c_1$:
 % \textbf{return} $\flatc(\new b_1, c_1) \cup \{ b \full \neg b_1 \}$ \\
 % \> \textbf{case} $c_1$ \verb+/\+ $c_2$: \=
-% \textbf{if} ($b \equiv \true$)  \textbf{return} $\flatc(\true, c_1) \cup
-%            \flatc(\true, c_2)$ \\
+% \textbf{if} ($b \equiv \mzninline{true}$)  \textbf{return} $\flatc(\mzninline{true}, c_1) \cup
+%            \flatc(\mzninline{true}, c_2)$ \\
 % \> \> \textbf{else} \textbf{return} $\flatc(\new b_1, c_1) \cup
 %            \flatc(\new b_2, c_2) \cup \{ b \full (b_1 \wedge b_2)\}$ \\
 % xx\=xx\=xx\=xx\=xx\=xx\=xx\= \kill
@@ -1208,7 +1216,7 @@ $S$ \cupp $\{ \new b \full (b_1 \wedge b_2)\}$
 %            \flatc(\new b_2, c_2) \cup \{ b \full (b_1 \full
 %            b_2)\}$ \\
 % \> \textbf{case} $p$ ($t_1, \ldots, t_n$) (\syntax{<pred>}): \\
-% \> \> \textbf{if} ($b \equiv \true$) \textbf{return} $\safen(b,
+% \> \> \textbf{if} ($b \equiv \mzninline{true}$) \textbf{return} $\safen(b,
 % \cup_{j=1}^n \flatt(\new v_j, t_j)) \cup \{ p(v_1, \ldots, v_n) \}$ \\
 % \> \> \textbf{else} \textbf{abort}
 % \end{tabbing}
@@ -1237,21 +1245,22 @@ The procedure \safen($b, C$) enforces the relational semantics for unsafe
 expressions, by ensuring that the unsafe relational versions of partial
 functions are made safe. Note that to implement the \emph{strict semantics} as
 opposed to the relational semantics we just need to define $\safen(b,C) = C$. If
-$b \equiv \true$ then the relational semantics and the strict semantics
+$b \equiv \mzninline{true}$ then the relational semantics and the strict semantics
 coincide, so nothing needs to be done. The same is true if the set of
 constraints $C$ is safe. For $div(x,y,z)$, the translation introduces a new
 variable $y'$ which cannot be 0, and equates it to $y$ if $y \neq 0$. The
 constraint $div(x,y',z)$ never reflects a partial function application. The new
 variable $b'$ captures whether the partial function application returns a non
-$\bot$ value. For $\element(v,a,x)$, it introduces a new variable $v'$ which
-only takes values in $\dom(a)$ and forces it to equal $v$ if $v \in \dom(a)$. A
-partial function application forces $b = \false$ since it is the conjunction of
-the new variables $b'$. The \%HALF\% comments will be explained later.
+$\bot$ value. For \mzninline{element(v, a, x)}, it introduces a new variable $v'$
+which only takes values in $\dom(a)$ and forces it to equal $v$ if
+$v \in \dom(a)$. A partial function application forces $b = \mzninline{false}$ since it is
+the conjunction of the new variables $b'$. The \%HALF\% comments will be
+explained later.
 
 \begin{tabbing}
 xx\=xx\=xx\=xx\=xx\=xx\=xx\= \kill
 \safen($b$,$C$) \\
-\> \textbf{if} ($b \equiv \true$) \textbf{return} $C$ \\
+\> \textbf{if} ($b \equiv \mzninline{true}$) \textbf{return} $C$ \\
 \> \textbf{if} ($C$ is a set of safe constraints) \textbf{return} $C$ \\
 \> $B$ := $\emptyset$; $S$ := $\emptyset$  \\
 \> \textbf{foreach} $c \in C$ \\
@@ -1261,13 +1270,13 @@ xx\=xx\=xx\=xx\=xx\=xx\=xx\= \kill
 = y', div(x,y',z) \}$ \\
 \> \> \> \%HALF\% $S$ := $S \cup \{ b' \full y \neq 0, b' \half
 div(x,y,z)\}$ \\
-\> \> \textbf{else if} $c \equiv \element(v,a,x)$  and $v$ can take a value outside the domain of $a$) \\
+\> \> \textbf{else if} \(c \equiv \mzninline{element(v, a, x)}\) and $v$ can take a value outside the domain of $a$) \\
 \> \> \> $B$ := $B \cup \{ \new b' \}$ \\
 \> \> \> $S$ := $S \cup \{ \new v' \in \dom(a),
 b' \full v \in \dom(a), b' \full v = v',
-\element(v',a,x)\}$ \\
+\mzninline{element(v', a, x)}\}$ \\
 \> \> \> \%HALF\% $S$ := $S \cup \{ b' \full v \in \dom(a), b' \half
-\element(v,a,x)\}$ \\
+\mzninline{element(v, a, x)}\}$ \\
 \> \> \textbf{else} $S$ := $S \cup \{c\}$ \\
 \> \> \textbf{return} $S \cup \{b \full \wedge_{b' \in B} b'
 \})$
@@ -1279,7 +1288,7 @@ renamed-apart copies of already-generated constraints, but for simplicity of
 presentation, we omit the algorithms we use to do this.
 
 \section{Half Reification}
-\label{sec:halfreif}
+\label{sec:hr-halfreif}
 
 Given a constraint $c$, the \emph{half-reified version} of $c$ is a constraint
 of the form $b \half c$ where $b \not\in vars(c)$ is a Boolean variable.
@@ -1288,11 +1297,11 @@ We can construct a propagator $f_{b \half c}$ for the half-reified version of
 $c$, $b \half c$, using the propagator $f_c$ for $c$.
 $$
 \begin{array}{rcll}
-f_{b \half c}(D)(b) & = &  \{ \false \} \cap D(b) & \text{if~} f_c(D) \text{~is a false domain} \\
+f_{b \half c}(D)(b) & = &  \{ \mzninline{false} \} \cap D(b) & \text{if~} f_c(D) \text{~is a false domain} \\
 f_{b \half c}(D)(b) & = & D(b) & \text{otherwise} \\
-f_{b \half c}(D)(v) & = & D(v) & \text{if~} v \in vars(c) \text{~and~} \false \in D(b) \\
+f_{b \half c}(D)(v) & = & D(v) & \text{if~} v \in vars(c) \text{~and~} \mzninline{false} \in D(b) \\
 f_{b \half c}(D)(v) & = & f_c(D)(v) & \text{if~} v \in vars(c)
-\text{~and~} \false \not\in D(b)
+\text{~and~} \mzninline{false} \not\in D(b)
 \end{array}
 $$
 
@@ -1325,27 +1334,28 @@ $$
 % Given this separation we can improve the definition of $f_{b \half c}$ above by
 % replacing the check ``$f_c(D)$ is a false domain'' by ``$f_{check(c)}(D)$ is a
 % false domain''. In practice it means that the half-reified propagator can be
-% implemented to only perform the checking part until $D(b) = \{\true\}$, when it
+% implemented to only perform the checking part until $D(b) = \{\mzninline{true}\}$, when it
 % needs to perform both.
 
-In practice most propagator implementations for $c$ first check whether $c$ is
-satisfiable, before continuing to propagate. For example,
-$\sum_i a_i x_i \leq a_0$ determines $L = \sum_i min_D(a_i x_i) - a_0$ and fails
-if $L > 0$ before propagating; Regin's domain propagator for
-\alldiff$([x_1, \ldots, x_n]$) determines a maximum matching between variables
-and values first, if this is not of size $n$ it fails before propagating; the
-timetable \texttt{cumulative} constraint determines a profile of necessary
-resource usage, and fails if this breaks the resource limit, before considering
-propagation. We can implement the propagator for $f_{b \half c}$ by only
-performing the checking part until $D(b) = \{\true\}$.
+In practice most propagator implementations for \mzninline{c} first check
+whether \mzninline{c} is satisfiable, before continuing to propagate. For
+example, \mzninline{sum(i in N)(a[i] * x[i]) <= C} determines \mzninline{L =
+  sum(i in N)(lb(a[i] * x[i])) - C} and fails if \mzninline{L > 0} before
+propagating; Regin's domain propagator for \mzninline{all_different(X)}
+determines a maximum matching between variables and values first, if this is not
+of size \mzninline{length(X)} it fails before propagating; the timetable
+\texttt{cumulative} constraint determines a profile of necessary resource usage,
+and fails if this breaks the resource limit, before considering propagation. We
+can implement the propagator for $f_{\mzninline{b -> c}}$ by only performing the
+checking part until $D(\texttt{b}) = \{\mzninline{true}\}$.
 
 Half reification naturally encodes the relational semantics for partial function
-applications in positive contexts. We associate a Boolean variable $b$ with each
+applications in positive contexts. We associate a Boolean variable \texttt{b} with each
 Boolean term in an expression, and we ensure that all unsafe constraints are
 half-reified using the variable of the nearest enclosing Boolean term.
 
 \begin{example}
-  Consider flattening of the constraint of \cref{ex:cons}. First we will convert
+  Consider flattening of the constraint of \cref{ex:hr-cons}. First we will convert
   it to an equivalent expression with only positive contexts
 
   \begin{mzn}
@@ -1364,10 +1374,10 @@ half-reified using the variable of the nearest enclosing Boolean term.
     constraint b1 \/ b2;
   \end{mzn}
 
-  The unsafe $\element$ constraint is half reified with the name of its nearest
+  The unsafe \mzninline{element} constraint is half reified with the name of its nearest
   enclosing Boolean term. Note that if $i = 7$ then the second constraint makes
-  $b2 = \false$. Given this, the final constraint requires $b1 = \true$, which
-  in turn requires $i > 4$. Since this holds, the whole constraint is $\true$
+  $b2 = \mzninline{false}$. Given this, the final constraint requires $b1 = \mzninline{true}$, which
+  in turn requires $i > 4$. Since this holds, the whole constraint is $\mzninline{true}$
   with no restrictions on $x$.
 \end{example}
 
@@ -1376,7 +1386,7 @@ assume that each global constraint predicate $p$ is available in half-reified
 form. Recall that this places no new burden on the solver implementer.
 
 \begin{example}
-  Consider the constraint of \cref{ex:alldiff}. Half reification results in
+  Consider the constraint of \cref{ex:hr-alldiff}. Half reification results in
 
   \begin{mzn}
     constraint b1 -> i > 4;
@@ -1385,14 +1395,15 @@ form. Recall that this places no new burden on the solver implementer.
     constraint b1 \/ b2         % b1 or b2
   \end{mzn}
 
-  We can easily modify any existing propagator for \alldiff to support the
-  half-reified form, hence this model is executable by our constraint solver.
+  We can easily modify any existing propagator for \mzninline{all_different} to
+  support the half-reified form, hence this model is executable by our
+  constraint solver.
 \end{example}
 
 Half reification can lead to more efficient constraint solving, since it does
 not propagate unnecessarily.
 
-\begin{example}\label{ex:cumul}
+\begin{example}\label{ex:hr-cumul}
   Consider the task decomposition of a \texttt{cumulative} constraint (see \eg\
   \autocite{schutt-2009-cumulative}) which includes constraints of the form
 
@@ -1415,7 +1426,7 @@ not propagate unnecessarily.
   \end{mzn}
 
   Whenever the start time of task $i$ is constrained so that it does not overlap
-  time $s[j]$, then $b3[i]$ is fixed to $\false$ and $a[i]$ to 0, and the long
+  time $s[j]$, then $b3[i]$ is fixed to $\mzninline{false}$ and $a[i]$ to 0, and the long
   linear sum is awoken. But this is useless, since it cannot cause failure.
 
   % Half-reification of this expression which appears in a negative context produces
@@ -1442,7 +1453,7 @@ not propagate unnecessarily.
 \pjs{Add linearization example here!}
 
 Half reification can cause propagators to wake up less frequently, since
-variables that are fixed to $\true$ by full reification will never be fixed by
+variables that are fixed to $\mzninline{true}$ by full reification will never be fixed by
 half reification. This is advantageous, but a corresponding disadvantage is that
 variables that are fixed can allow the simplification of the propagator, and
 hence make its propagation faster. We can reduce this disadvantage by fully
@@ -1463,7 +1474,7 @@ rewriting used with full reification.
 
 The procedure $\halfc(b,c)$ defined below returns a set of constraints
 implementing the half-reification $b \half c$. We flatten a constraint item
-$\texttt{constraint}~c$ using $\halfc(\true, c)$. The half-reification
+$\texttt{constraint}~c$ using $\halfc(\mzninline{true}, c)$. The half-reification
 flattening transformation uses half reification whenever it is in a positive
 context. If it encounters a constraint $c_1$ in a negative context, it negates
 the constraint if it is safe, thus creating a new positive context. If this is
@@ -1541,8 +1552,8 @@ $\tuple{h,\rootc}$; \textbf{return} $h$
 \> \textbf{if} ($\fixed(c)$) $b$ := $\eval(c)$ \\
 \> \textbf{else} \\
 \> \> \textbf{switch} $c$ \\
-%\> \> \textbf{case} \texttt{true}: $b$ := $\true$;\\
-%\> \> \textbf{case} \texttt{false}: $b$ := $\false$;\\
+%\> \> \textbf{case} \texttt{true}: $b$ := $\mzninline{true}$;\\
+%\> \> \textbf{case} \texttt{false}: $b$ := $\mzninline{false}$;\\
 \> \> \textbf{case} $b'$ (\syntax{<bvar>}): $b$ := $b'$; \\
 \> \> \textbf{case} $t_1$ $r$ $t_2$ (\syntax{<relop>}):  \\
 \> \> \> \textbf{switch} $r$ \\
@@ -1586,7 +1597,7 @@ $S$ \cupp  $\{ \new b \half (\flatc(c_1,\mix) \full
 %\mathit{safeelement}(v, [b_1, \ldots, b_n],  b'),
 %b'' \full v \in \{1,..,n\} \} $ \\
 \>\>\> \textbf{if} ($\ctxt = \rootc$)
-$S$ \cupp $\{\texttt{element}(v, [b_1, \ldots, b_n], \true), \new b\}$ \\
+$S$ \cupp $\{\texttt{element}(v, [b_1, \ldots, b_n], \mzninline{true}), \new b\}$ \\
 \>\>\> \textbf{else}
 $S$ \cupp $\{ \new b \half (b_{n+1} \wedge \new b'), b \half
 \texttt{element}(v, [b_1, \ldots, b_n],  b') \}$ \\
@@ -1601,7 +1612,7 @@ $S$ \cupp $\{ \new b \half (b_{n+1} \wedge \new b'), b \half
 \> \> \> \textbf{foreach}($j \in 1..n$) $\tuple{v_j, b_j}$ :=
 $\halft(t_j,\ctxt,\iboth)$; \\
 \> \> \> \textbf{if} ($\ctxt = \rootc$)
-$b$ := $\true$; $S$ \cupp  $\{ p(v_1, \ldots, v_n) %, \bigwedge_{j=1}^n b_j
+$b$ := $\mzninline{true}$; $S$ \cupp  $\{ p(v_1, \ldots, v_n) %, \bigwedge_{j=1}^n b_j
 \}$
 \\
 \>\>\> \textbf{else} %($\ctxt = \pos$) \\ \> \> \> \>
@@ -1626,7 +1637,7 @@ b_j\}$
 \>\> \textbf{case} $p$ ($t_1, \ldots, t_n$) (\syntax{<pred>}) built-in predicate: \\
 \> \> \> \textbf{if} ($\ctxt \neq \rootc$) \textbf{abort} \\
 \> \> \> \textbf{foreach}($j \in 1..n$) $\tuple{v_j, \_}$ := $\flatt(t_j,\rootc)$; \\
-\>\> \> $b$ := $\true$; $S$ \cupp  $\{ p(v_1, \ldots, v_n)\}$
+\>\> \> $b$ := $\mzninline{true}$; $S$ \cupp  $\{ p(v_1, \ldots, v_n)\}$
 \\
 \>\> \textbf{case} $p$ ($t_1, \ldots, t_n$) (\syntax{<pred>}): user-defined predicate \\
 \>\> \> \textbf{let} $p(x_1, \ldots, x_n) = c_0$ be defn of $p$ \\
@@ -1689,8 +1700,8 @@ $\tuple{h,\rootc}$; \textbf{return} $h$\\
 \> \textbf{if} ($\fixed(c)$) $b$ := $\neg \eval(c)$ \\
 \> \textbf{else} \\
 \> \> \textbf{switch} $c$ \\
-%\> \> \textbf{case} \texttt{true}: $b$ := $\true$;\\
-%\> \> \textbf{case} \texttt{false}: $b$ := $\false$;\\
+%\> \> \textbf{case} \texttt{true}: $b$ := $\mzninline{true}$;\\
+%\> \> \textbf{case} \texttt{false}: $b$ := $\mzninline{false}$;\\
 \> \> \textbf{case} $b'$ (\syntax{<bvar>}): $S$ \cupp $\{\new b \half \neg b'\}$; \\
 \> \> \textbf{case} $t_1$ $r$ $t_2$ (\syntax{<relop>}):  \\
 \> \> \> \textbf{if} ($t_1$ and $t_2$ are safe) \\
@@ -1786,7 +1797,7 @@ bounds. If the previous context was root or the context are the same we examine
 the bounds. If they are the same we reuse the result, otherwise we set the
 $\bnds$ to $\iboth$ and reflatten since we require both bounds (perhaps in
 different situations). Otherwise the new context is $\rootc$ and the previous
-$\pos$, we force $b'$ to be $\true$ in $S$, and then reuse the result if the
+$\pos$, we force $b'$ to be $\mzninline{true}$ in $S$, and then reuse the result if the
 bounds are the same, or set $\bnds$ to $\iboth$ and reflatten. We store the
 result found at the end of flattening, note that we only need one entry: context
 can move from $\pos$ to $\rootc$ and bounds can move from one of $\iabove$ or
@@ -1853,13 +1864,13 @@ xx\=xx\=xx\=xx\=xx\=xx\=xx\= \kill
 \> \> \> \textbf{if} ($pbnds = \bnds$) hhash[$t$] := $\tuple{h,b',\rootc,\bnds}$; \textbf{return} $\tuple{h,b'}$
 \\
 \> \> \> \textbf{else} $\bnds$ := $\iboth$ \\
-\> \textbf{if} ($\fixed(t)$) $v$ := $\eval(t)$; $b$ := $\true$ \\
+\> \textbf{if} ($\fixed(t)$) $v$ := $\eval(t)$; $b$ := $\mzninline{true}$ \\
 \> \textbf{else} %\\
 %% \> \> \textbf{if} ($t$ is marked \emph{total}) $\ctxt$ := $\rootc$ \\
 %\> \>
 \textbf{switch} $t$ \\
-%\> \> \textbf{case} $i$ (\intc): $v$ := $i$; $b$ := $\true$ \\
-\> \> \textbf{case} $v'$ (\syntax{<ivar>}):  $v$ := $v'$; $b$ := $\true$\\
+%\> \> \textbf{case} $i$ (\intc): $v$ := $i$; $b$ := $\mzninline{true}$ \\
+\> \> \textbf{case} $v'$ (\syntax{<ivar>}):  $v$ := $v'$; $b$ := $\mzninline{true}$\\
 \> \> \textbf{case} $t_1$ $a$ $t_2$ (\syntax{<arithop>}): \\
 \> \> \> \textbf{switch} $a$ \\
 \> \> \> \textbf{case} $+$:
@@ -1957,8 +1968,8 @@ $S$ \cupp $\{ \new b \half (b_1 \wedge b_2)\}$
 % context, negates $c_1$ and half-reifies the result if $c_1$ is safe and in a
 % negative context, and uses full flattening otherwise.
 
-\begin{example}\label{ex:half}
-  Now lets consider half reifying the expression of \cref{ex:flat}.
+\begin{example}\label{ex:hr-half}
+  Now lets consider half reifying the expression of \cref{ex:hr-flat}.
 
   The result of flattening with half reification is:
 
@@ -2029,7 +2040,7 @@ $S$ \cupp $\{ \new b \half (b_1 \wedge b_2)\}$
 transformation will construct many implications of the form $b \half b'$, note
 that the constraint $b \half b_1 \wedge \cdots \wedge b_n$ is equivalent to
 $b \half b_1, b \half b_2, \ldots, b \half b_n$. Just as in
-Example~\ref{ex:half} above we can simplify the result of half reification. For
+\cref{ex:hr-half} above we can simplify the result of half reification. For
 each $b'$ which appears only on the right of one constraint of the form
 $b \half b'$ and other constraints of the form $b' \half c_i$ we remove the
 first constraint and replace the others by $b \half c_i$.
@@ -2047,17 +2058,17 @@ To do so independent of propagation strength, we define the behaviour of the
 propagators of the half-reified forms in terms of the full reified propagator.
 $$
 \begin{array}{rcll}
-f_{b \half c}(D)(b) & = & D(b) \cap ( \{ \false \} \cup f_{b \full c}(D)(b)) \\
-f_{b \half c}(D)(v) & = & D(v) & \texttt{if}~v \in vars(c),~\false \in D(b) \\
+f_{b \half c}(D)(b) & = & D(b) \cap ( \{ \mzninline{false} \} \cup f_{b \full c}(D)(b)) \\
+f_{b \half c}(D)(v) & = & D(v) & \texttt{if}~v \in vars(c),~\mzninline{false} \in D(b) \\
 f_{b \half c}(D)(v) & = & f_{b \full c}(D)(v) & \texttt{if}~v \in vars(c),~\text{otherwise}
 \end{array}
 $$
 and
 $$
 \begin{array}{rcll}
-f_{b' \half \neg c}(D)(b') & = & D(b') & \texttt{if}~\{ \false \} \in f_{b \full c}(D)(b) \\
-f_{b' \half \neg c}(D)(b') & = & D(b') \cap \{ \false\} &  \text{otherwise}\\
-f_{b' \half \neg c}(D)(v) & = & D(v) & \texttt{if}~v \in vars(c),~\false \in D(b') \\
+f_{b' \half \neg c}(D)(b') & = & D(b') & \texttt{if}~\{ \mzninline{false} \} \in f_{b \full c}(D)(b) \\
+f_{b' \half \neg c}(D)(b') & = & D(b') \cap \{ \mzninline{false}\} &  \text{otherwise}\\
+f_{b' \half \neg c}(D)(v) & = & D(v) & \texttt{if}~v \in vars(c),~\mzninline{false} \in D(b') \\
 f_{b' \half \neg c}(D)(v) & = & f_{b \full c}(D)(v) & \texttt{if}~v \in vars(c),~\text{otherwise}
 \end{array}
 $$
@@ -2067,7 +2078,7 @@ half reified split versions of the propagator should act.
 In order to prove the same behaviour of the split reification versions we must
 assume that $f_{b \full c}$ is \emph{reified-consistent} which is defined as
 follows: suppose $f_{b \full c}(D)(v) \neq D(v), v \not\equiv b$, then
-$f_{b \full c}(D)(b) \neq \{ \false, \true\}$. That is if the propagator ever
+$f_{b \full c}(D)(b) \neq \{ \mzninline{false}, \mzninline{true}\}$. That is if the propagator ever
 reduces the domain of some variable, then it must also fix the Boolean variable
 $b$. This is sensible since if $b$ is not fixed then every possible value of $v$
 is consistent with constraint $b \full c$ regardless of the domain $D$. This is
@@ -2105,14 +2116,14 @@ the usual case for such a trivial propagator.
 %   $D'' = \solv(\{ f_{b \half c}, f_{b' \half \neg c}, f_{b' \full \neg b}\}, D)$.
 %   The proof is by cases of $D$.
 
-%   \textbf{(a)} Suppose $D(b) = \{\true,\false\}$. \textbf{(a-i)} Suppose
+%   \textbf{(a)} Suppose $D(b) = \{\mzninline{true},\mzninline{false}\}$. \textbf{(a-i)} Suppose
 %   $f_{b \full c}(D) = D$. Then clearly $f_{b \half c}(D) = D$ by definition, and
 %   similarly $f_{b' \half \neg c}(D) = D$. Hence $D_1 = D_2 = D$. Note that since
 %   $f_{b \full c}$ is reified consistent, then $f_{b \full c}(D) \neq D$ implies
-%   that $f_{b \full c}(D)(b) \neq \{ \false, \true \}$. \textbf{(a-ii)} Suppose
-%   $f_{b \full c}(D)(b) = \{ \true \}$. Let $D_1 = f_{b' \half \neg c}(D)$, then
-%   $D_1(b') = \{ \false \}$ by definition and $D_1(v) = D(v), v \not\equiv b'$.
-%   Let $D_2 = f_{b' \full \neg b}(D_1)$ then $D_2(b)= \{ \true \}$ and
+%   that $f_{b \full c}(D)(b) \neq \{ \mzninline{false}, \mzninline{true} \}$. \textbf{(a-ii)} Suppose
+%   $f_{b \full c}(D)(b) = \{ \mzninline{true} \}$. Let $D_1 = f_{b' \half \neg c}(D)$, then
+%   $D_1(b') = \{ \mzninline{false} \}$ by definition and $D_1(v) = D(v), v \not\equiv b'$.
+%   Let $D_2 = f_{b' \full \neg b}(D_1)$ then $D_2(b)= \{ \mzninline{true} \}$ and
 %   $D_2(v) = D(v), v \not\in \{b,b'\}$. Then
 %   $D_3 = f_{b \half c}(D_2) = f_{b \full c}(D_2)$ by definition, and by
 %   idempotence of $f_{b \full c}$ and since $D_2$ and $D$ differ only on $b$ and
@@ -2121,9 +2132,9 @@ the usual case for such a trivial propagator.
 %   $f_{b \half c}$, $f_{b' \full \neg b}$ and $f_{b' \half \neg c}$ and hence
 %   $D'' = D_3$. But also $D' = f_{b' \full \neg b}(f_{b \full c}(D)) = D_3$ since
 %   $D_3$ and $f_{b \full c}(D)$ only differ on $b'$. \textbf{(a-iii)} Suppose
-%   $f_{b \full c}(D)(b) = \{ \false \}$. Let $D_1 = f_{b \half c}(D)$, then
-%   $D_1(b) = \{ \false \}$ by definition and $D_1(v) = D(v), v \not\equiv b$. Let
-%   $D_2 = f_{b' \full \neg b}(D_1)$ then $D_2(b')= \{ \true \}$ and
+%   $f_{b \full c}(D)(b) = \{ \mzninline{false} \}$. Let $D_1 = f_{b \half c}(D)$, then
+%   $D_1(b) = \{ \mzninline{false} \}$ by definition and $D_1(v) = D(v), v \not\equiv b$. Let
+%   $D_2 = f_{b' \full \neg b}(D_1)$ then $D_2(b')= \{ \mzninline{true} \}$ and
 %   $D_2(v) = D(v), v \not\in \{b,b'\}$. Then
 %   $D_3 = f_{b' \half \neg c}(D_2) = f_{b \full c}(D_2)$ by definition, and by
 %   idempotence of $f_{b \full c}$ and since $D_2$ and $D$ differ only on $b$ and
@@ -2132,10 +2143,10 @@ the usual case for such a trivial propagator.
 %   $D' = f_{b' \full \neg b}(f_{b \full c}(D)) = D_3$ since $D_3$ and
 %   $f_{b \full c}(D)$ only differ on $b'$.
 
-%   \textbf{(b)} If $D(b) = \{\true\}$ then clearly $f_{b \full c}$ and
+%   \textbf{(b)} If $D(b) = \{\mzninline{true}\}$ then clearly $f_{b \full c}$ and
 %   $f_{b \half c}$ act identically on variables in $vars(c)$.
 
-%   \textbf{(c)} If $D(b) = \{\false\}$ then $D(b') = \{\true\}$ and clearly
+%   \textbf{(c)} If $D(b) = \{\mzninline{false}\}$ then $D(b') = \{\mzninline{true}\}$ and clearly
 %   $f_{b \full c}$ and $f_{b' \half \neg c}$ act identically on variables in
 %   $vars(c)$. \qed
 % \end{proof}
@@ -2181,7 +2192,7 @@ still fixed at the same time, but there is less overhead.
 
 Implementing half-reification within the \minizinc\ distribution consists of two
 parts: the \minizinc\ compiler needs to be extended with an implementation of
-the half-reification flattening algorithm as described in \cref{sec:halfreif}
+the half-reification flattening algorithm as described in \cref{sec:hr-halfreif}
 and for any target solver that supports half-reification its library needs to be
 appended with definitions for the predicates that are half-reified. Because the
 \minizinc\ language allows for the definition of new predicates, we allow any
@@ -2220,35 +2231,34 @@ has propagators for half-reified constraints we have declared the corresponding
 predicates as solver builtins. Gecode provides half-reified propagators for
 almost all \flatzinc\ builtins. The other targeted solvers use the linear
 library. The linear library \jip{,as seen before + reference???,} already has
-redefinition for their fully reified predicates, \(b \full c\). These generally
-consist of two parts which are equivalent to the implications
-\(b \half c \land \lnot b \half \lnot c \). Because of this, the implementations
-of the half-reified version of the same predicates usually consist of using only
+redefinition for their fully reified predicates, \mzninline{b <-> c}. These
+generally consist of two parts which are equivalent to the implications
+\mzninline{b -> c /\ not b -> not c}. Because of this, the implementations of
+the half-reified version of the same predicates usually consist of using only
 one of these two parts, which will eliminate the need of many constraints. We
 added half-reified versions for all predicates for which a full reification was
 provided.
 
 \subsection{Implication Chain Compression}
 
-As shown in \cref{ex:half}, flattening with half reification will in many cases
-result in implication chains: \((b \half b') \land (b' \half c)\), where \(b'\)
-has no other occurrences. In this case the conjunction can be replaced by
-\(b \half c\) and \(b'\) can be removed from the model. The case shown in the
-example can be generalised to
-\((b \half b') \land \left(\forall_{i \in N} b' \half c_i \right)\), which, if
-\(b'\) has no other usage in the instance, can be resolved to
-\(\forall_{i \in N} b \half c_i\) after which \(b'\) can be removed from the
-model.
+As shown in \cref{ex:hr-half}, flattening with half reification will in many
+cases result in implication chains: \mzninline{b1 -> b2 /\ b2 -> c}, where
+\texttt{b2} has no other occurrences. In this case the conjunction can be
+replaced by \mzninline{b1 -> c} and \texttt{b2} can be removed from the model.
+The case shown in the example can be generalised to \mzninline{b1 -> b2 /\
+  forall(i in N)(b2 -> c[i])}, which, if \texttt{b2} has no other usage in the
+instance, can be resolved to \mzninline{forall(i in N)(b1 -> c[i])} after which
+\texttt{b1} can be removed from the model.
 
 An algorithm to remove these chains of implications is best visualised through
 the use of an implication graph. An implication graph \(\tuple{V,E}\) is a
 directed graph where the vertices \(V\) represent the variables in the instance
 and an edge \(\tuple{x,y} \in E\) represents the presence of an implication
-\(x \half y\) in the instance. Additionally, for the benefit of the algorithm, a
-vertex is marked when it is used in other constraints in the constraint model.
-The goal of the algorithm is now to identify and remove vertices that are not
-marked and have only one incoming edge. The following pseudo code provides a
-formal specification for this algorithm.
+\mzninline{x -> y} in the instance. Additionally, for the benefit of the
+algorithm, a vertex is marked when it is used in other constraints in the
+constraint model. The goal of the algorithm is now to identify and remove
+vertices that are not marked and have only one incoming edge. The following
+pseudo code provides a formal specification for this algorithm.
 
 \newcommand{\setminusp}{\ensuremath{\setminus}\text{:=}~}
 \begin{tabbing}
@@ -2266,12 +2276,12 @@ formal specification for this algorithm.
 \jip{Here we could actually show an example using a drawn graph}
 
 The algorithm can be further improved by considering implied conjunctions. These
-can be split up into multiple implications: \(b' \half \forall_{i \in N} b_i\)
-is equivalent to \(\forall_{i \in N} (b' \half b_i)\). This transformation both
-simplifies a complicated constraint and possibly allows for the further
-compression of implication chains. It should however be noted that although this
-transformation can result in an increase in the number of constraints, it
-generally increases the propagation efficiency.
+can be split up into multiple implications: \mzninline{b -> forall(i in
+  N)(bs[i])} is equivalent to \mzninline{forall(i in N)(b -> bs[i])}. This
+transformation both simplifies a complicated constraint and possibly allows for
+the further compression of implication chains. It should however be noted that
+although this transformation can result in an increase in the number of
+constraints, it generally increases the propagation efficiency.
 
 To adjust the algorithm to simplify implied conjunctions more introspection from
 the \minizinc\ compiler is required. The compiler must be able to tell if a
@@ -2289,8 +2299,8 @@ available \jip{Insert new link} has our experimental \minizinc\ instances and
 the infrastructure that performs the benchmarks.
 
 The first experiment considers ``QCP-max'' problems which are defined as
-quasi-group completion problems where the \alldiff constraints are soft, and the
-aim is to satisfy as many of them as possible.
+quasi-group completion problems where the \mzninline{all_different} constraints
+are soft, and the aim is to satisfy as many of them as possible.
 
 \begin{mzn}
 int: n; % size
@@ -2308,20 +2318,21 @@ predicate all_different(array[int] of var int: x) =
     forall(i,j in index_set(x) where i < j)(x[i] != x[j]);
 \end{mzn}
 
-Note that this is not the same as requiring the maximum number of
-disequality constraints to be satisfied. The \alldiff constraints, while
+Note that this is not the same as requiring the maximum number of disequality
+constraints to be satisfied. The \mzninline{all_different} constraints, while
 apparently in a mixed context, are actually in a positive context, since the
-maximization in fact is implemented by inequalities forcing at least some number
+maximisation in fact is implemented by inequalities forcing at least some number
 to be true.
 
-In Table~\ref{tab:qcp} we compare three different resulting programs on QCP-max
-problems: full reification of the model above, using the \alldiff decomposition
-defined by the predicate shown (\textsf{full}), half reification of the model
-using the \alldiff decomposition (\textsf{half}), and half reification using a
-half-reified global \alldiff (\textsf{half-g}) implementing arc consistency
-(thus having the same propagation strength as the decomposition). \jip{is this
-  still correct??} We use standard QCP examples from the literature, and group
-them by size.
+In \cref{tab:hr-qcp} we compare three different resulting programs on QCP-max
+problems: full reification of the model above, using the
+\mzninline{all_different} decomposition defined by the predicate shown
+(\textsf{full}), half reification of the model using the
+\mzninline{all_different} decomposition (\textsf{half}), and half reification
+using a half-reified global \mzninline{all_different} (\textsf{half-g})
+implementing arc consistency (thus having the same propagation strength as the
+decomposition). \jip{is this still correct??} We use standard QCP examples from
+the literature, and group them by size.
 % and whether they are satisfiable or unsatisfiable as QCP problems.
 We compare both a standard finite domain solver (FD) and a learning lazy clause
 generation solver (FD + Explanations). We use the same fixed search strategy of
@@ -2329,7 +2340,7 @@ labeling the matrix in order left-to-right from highest to lowest value for all
 approaches to minimize differences in search.
 
 \begin{table} [tb] \begin{center}
-\caption{\label{tab:qcp} QCP-max problems:
+\caption{\label{tab:hr-qcp} QCP-max problems:
 Average time (in seconds), number of solved instances (300s timeout).}
 \begin{tabular}{|l||rr|rr|rr|}
 \hline
@@ -2359,7 +2370,7 @@ The second experiment shows how half reification can reduce the overhead of
 handling partial functions correctly. Consider the following model for
 determining a prize collecting path, a simplified form of prize collecting
 travelling salesman problem
-\autocite{balas-1989-pctsp}, %shown in Figure~\ref{fig:pct}
+\autocite{balas-1989-pctsp}, %shown in \cref{fig:hr-pct}
 where the aim is define an acyclic path from node 1 along weighted edges to
 collect the most weight. Not every node needs to be visited ($pos[i] = 0$).
 
@@ -2382,12 +2393,12 @@ constraint alldifferent_except_0(next) /\ pos[1] = 1;
 solve minimize sum(i in 1..n)(prize[i]);
 \end{mzn}
 
-It uses the global constraint \texttt{alldifferent\_except\_0} which constrains
-each element in the $next$ array to be different or equal 0. The model has one
-unsafe array lookup $pos[next[i]]$. We compare using full reification
-(\textsf{full}) and half reification (\textsf{half}) to model this problem. Note
-that if we extend the $pos$ array to have domain $0..n$ then the model becomes
-safe, by replacing its definition with the following two lines
+It uses the global constraint \mzninline{alldifferent_except_0} which constrains
+each element in the \mzninline{next} array to be different or equal 0. The model
+has one unsafe array lookup \mzninline{pos[next[i]]}. We compare using full
+reification (\textsf{full}) and half reification (\textsf{half}) to model this
+problem. Note that if we extend the $pos$ array to have domain $0..n$ then the
+model becomes safe, by replacing its definition with the following two lines
 
 \begin{mzn}
   array[0..n] of var 0..n: pos; % posn on node i in path, 0=notin
@@ -2397,18 +2408,18 @@ safe, by replacing its definition with the following two lines
 We also compare against this model (\textsf{extended}).
 
 We use graphs with both positive and negative weights for the tests. The search
-strategy fixes the $next$ variables in order of their maximum value. First we
-note that \textsf{extended} is slightly better than \textsf{full} because of the
-simpler translation, while \textsf{half} is substantially better than
-\textsf{extended} since most of the half reified \texttt{element} constraints
-become redundant. Learning increases the advantage because the half reified
-formulation focusses on propagation which leads to failure which creates more
-reusable nogoods.
+strategy fixes the \mzninline{next} variables in order of their maximum value.
+First we note that \textsf{extended} is slightly better than \textsf{full}
+because of the simpler translation, while \textsf{half} is substantially better
+than \textsf{extended} since most of the half reified \texttt{element}
+constraints become redundant. Learning increases the advantage because the half
+reified formulation focuses on propagation which leads to failure which creates
+more reusable nogoods.
 
 \begin{table} [tb] \begin{center}
-\caption{\label{tab:pctsp} Prize collecting paths:
-Average time (in seconds) and number of solved
-instances with a 300s timeout for various number of nodes.}
+    \caption{\label{tab:hr-pctsp} Prize collecting paths: Average time (in seconds)
+      and number of solved instances with a 300s timeout for various number of
+      nodes.}
 \begin{tabular}{|l||rr|rr|rr||rr|rr|rr|}
 \hline
  & \multicolumn{6}{|c||}{FD} & \multicolumn{6}{|c|}{FD + Explanations} \\
@@ -2457,11 +2468,11 @@ Nodes  &
 
 In the final experiment we compare resource constrained project scheduling
 problems (RCPSP) where the \texttt{cumulative} constraint is defined by the task
-decomposition as in \cref{ex:cumul} above, using both full reification and
+decomposition as in \cref{ex:hr-cumul} above, using both full reification and
 half-reification. We use standard benchmark examples from PSPlib
-\autocite{kolisch-1997-psplib}. \Cref{tab:rcpsp} compares RCPSP instances using
-\textsf{full} reification and \textsf{half} reification. We compare using J30
-instances (\textsf{J30} ) and instances due to Baptiste and Le Pape
+\autocite{kolisch-1997-psplib}. \Cref{tab:hr-rcpsp} compares RCPSP instances
+using \textsf{full} reification and \textsf{half} reification. We compare using
+J30 instances (\textsf{J30} ) and instances due to Baptiste and Le Pape
 (\textsf{BL}). Each line in the table shows the average run time and number of
 solved instances. The search strategy tries to schedule the task with the
 earliest possible start time. We find a small and uniform speedup for
@@ -2469,7 +2480,7 @@ earliest possible start time. We find a small and uniform speedup for
 learning, again because learning is not confused by propagations that do not
 lead to failure.
 
-\begin{table} [tb] \caption{\label{tab:rcpsp} RCPSP:
+\begin{table} [tb] \caption{\label{tab:hr-rcpsp} RCPSP:
 Average time (in seconds) and number of solved instances with a 300s timeout.}
 \begin{center}
 \begin{tabular}{|l||rr|rr||rr|rr|}
@@ -2494,15 +2505,13 @@ To verify the effectiveness of the half reification implementation within the
 \minizinc{} translator (rev. \jip{add revision}) against the equivalent version
 for which we have implemented half reification. We use the model instances used
 by the \minizinc{} challenges
-\autocite{stuckey-2010-challenge,stuckey-2014-challenge} from 2012 until 2017.
-Note that the instances that the instances without any reifications have been
-excluded from the experiment as they would not experience any change. The
+\autocite{stuckey-2010-challenge,stuckey-2014-challenge} from 2019 and 2020. The
 performance of the generated \flatzinc{} models will be tested using Gecode,
 flattened with its own library, and Gurobi and CBC, flattened with the linear
 library.
 
 \begin{table} [tb]
-  \caption{\label{tab:flat_results} Flattening results: Average changes in the
+  \caption{\label{tab:hr-flat-results} Flattening results: Average changes in the
   generated the \flatzinc{} models}
   \begin{center}
   \begin{tabular}{|l|r||r|r|r||r|}
@@ -2517,9 +2526,9 @@ library.
   \end{tabular}
   \end{center}
 \end{table}
-\jip{Better headers for \cref{tab:flat_results} and update with current results}
+\jip{Better headers for \cref{tab:hr-flat-results} and update with current results}
 
-\Cref{tab:flat_results} shows the average change on the number of full
+\Cref{tab:hr-flat-results} shows the average change on the number of full
 reification, constraints, and variables between the \flatzinc\ models generated
 by the different versions of the translator using the different libraries. We
 find that the number full reifications is reduced by a significant amount.
@@ -2535,8 +2544,7 @@ of memory running the Ubuntu 16.04.3 LTS operating system.
 \jip{Scatter plot of the runtimes + discussion!}
 
 %=============================================================================%
-\section{Related Work and Conclusion}
-\label{conclusion}
+\section{Related Work and Conclusion}\label{sec:hr-conclusion}
 %=============================================================================%
 
 Half reification on purely Boolean constraints is well understood, this is the
@@ -2546,33 +2554,28 @@ clausal representation of the circuit (see \eg\
 total) and the calculation of polarity for Booleans terms inside
 \texttt{bool2int} do not arise in pure Boolean constraints.
 
-Half reified constraints have been used in constraint modeling but are typically
-not visible as primitive constraints to users, or produced through flattening.
-Indexicals \autocite{van-hentenryck-1992-indexicals} can be used to implement
-reified constraints by specifying how to propagate a constraint
-$c$, %($prop(c)$),
-propagate its negation,
-%$prop(\neg c)$,
-check disentailment, % $check(c)$,
-and check entailment, %$check(\neg c)$,
-and this is implemented in SICstus Prolog \autocite{carlsson-1997-sicstus}. A
-half reified propagator simply omits entailment and propagating the negation.
-% $prop(\neg c)$ and $check(\neg c)$. Half reification was briefly discussed in
-% our earlier work \autocite{cp2009d}, in terms of its ability to reduce
-% propagation.
+Half reified constraints have been used in constraint modelling but are
+typically not visible as primitive constraints to users, or produced through
+flattening. Indexicals \autocite{van-hentenryck-1992-indexicals} can be used to
+implement reified constraints by specifying how to propagate a constraint,
+propagate its negation, check disentailment, and check entailment, and this is
+implemented in SICstus Prolog \autocite{carlsson-1997-sicstus}. A half reified
+propagator simply omits entailment and propagating the negation.
+
 Half reified constraints appear in some constraint systems, for example SCIP
 \autocite{gamrath-2020-scip} supports half-reified real linear constraints of
-the form $b \half \sum_i a_i x_i \leq a_0$ exactly because the negation of the
-linear constraint $\sum_i a_i x_i > a_0$ is not representable in an LP solver so
-full reification is not possible.
+the form \mzninline{b -> sum(i in N)(a[i] * x[i]) <= C} exactly because the
+negation of the linear constraint \mzninline{sum(i in N)(a[i] * x[i]) > C} is
+not representable in an LP solver so full reification is not possible.
 
 While flattening is the standard approach to handle complex formula involving
 constraints, there are a number of other approaches which propagate more
-strongly. Schulte proposes a generic implementation of $b \full c$ propagating
-(the flattened form of) $c$ in a separate constraint space which does not affect
-the original variables \autocite*{schulte-2000-deep}; entailment and
-disentailment of $c$ fix the $b$ variable appropriately, although when $b$ is
-made $\false$ the implementation does not propagate $\neg c$. This can also be
+strongly. Schulte proposes a generic implementation of \mzninline{b <-> c}
+propagating (the flattened form of) \mzninline{c} in a separate constraint space
+which does not affect the original variables \autocite*{schulte-2000-deep};
+entailment and disentailment of \mzninline{c} fix the \mzninline{b} variable
+appropriately, although when \mzninline{b} is made \mzninline{false} the
+implementation does not propagate \mzninline{not c}. This can also be
 implemented using propagator groups \autocite{lagerkvist-2009-groups}. Brand and
 Yap define an approach to propagating complex constraint formulae called
 controlled propagation which ensures that propagators that cannot affect the