diff --git a/chapters/4_rewriting.tex b/chapters/4_rewriting.tex
index 44b0106..7d045a6 100644
--- a/chapters/4_rewriting.tex
+++ b/chapters/4_rewriting.tex
@@ -164,7 +164,7 @@ The translation from \minizinc\ to \microzinc\ involves the following steps:
         \mzninline{int_plus(x,y)}. As mentioned above, more complex rules for
         rewriting conditionals with variables, such as \mzninline{if x then A
         else B endif} and \mzninline{A[x]} where \mzninline{x} is a variable,
-        are also replaced by function calls (\eg \mzninline{if_then_else([x,
+        are also replaced by function calls (\eg\ \mzninline{if_then_else([x,
         true], [A, B])} and \mzninline{element(a, x)} respectively).
 
   \item Replace optional variables into non-optional forms. As shown by Mears et
@@ -908,17 +908,17 @@ can then be fully simplified by constraint propagation, before the Boolean and
 reified constraints are rewritten into lower-level linear primitives suitable
 for MIP\@.
 
-\subsection{Common Subexpression Elimination}\label{sec:4-cse}
+\subsection{\titlecap{\glsentrytext{gls-cse}}}\label{sec:4-cse}
 
 The simplifications introduced above remove definitions from the model when we
 can detect that they are no longer needed. In some cases, it is even possible to
-not generate definitions in the first place through the use of common
-subexpression elimination (CSE). This simplification is a well understood
-technique that originates from compiler optimisation \autocite{cocke-1970-cse}
-and has proven to be very effective in discrete optimisation
+not generate definitions in the first place through the use of
+\glsaccesslong{cse}. This simplification is a well understood technique that
+originates from compiler optimisation \autocite{cocke-1970-cse} and has proven
+to be very effective in discrete optimisation
 \autocite{marinov-2005-sat-optimisations, araya-2008-cse-numcsp}, including
-during the evaluation of constraint modelling languages such as
-\minizinc\ \autocite{rendl-2009-enhanced-tailoring}.
+during the evaluation of constraint modelling languages such as \minizinc\
+\autocite{rendl-2009-enhanced-tailoring}.
 
 For instance, in the constraint\\
 \mzninline{(abs(x)*2 >= 20) \/ (abs(x)+5 >= 15)}\\
@@ -949,22 +949,22 @@ in the following example.
 
   Although the expressions \mzninline{pow(a, 2)} and \mzninline{pow(b, 2)} are
   not syntactically equal, the function call \mzninline{pythagoras(i,i)} using
-  the same variable for \mzninline{a} and \mzninline{b} makes them equivalent.
-  A straightforward approach to ensure that the same instantiation of a
-  function is only evaluated once is through memorisation. After the evaluation
-  of a \microzinc\ call, the instantiated call and its result are stored in a
-  lookup table, the CSE table. Before a call is evaluated the CSE table is
+  the same variable for \mzninline{a} and \mzninline{b} makes them equivalent. A
+  straightforward approach to ensure that the same instantiation of a function
+  is only evaluated once is through memorisation. After the evaluation of a
+  \microzinc\ call, the instantiated call and its result are stored in a lookup
+  table, the \gls{cse} table. Before a call is evaluated the \gls{cse} table is
   consulted. If the call is found, then the accompanying result is used;
   otherwise, the evaluation proceeds as normal.
 
   In our example, the evaluation of \mzninline{pythagoras(i, i)} would proceed
   as normal to evaluate \mzninline{x = pow(i, 2)}. However, the expression
-  defining \mzninline{y}, \mzninline{pow(i, 2)}, will be found in the CSE table
-  and replaced by the earlier stored result: \mzninline{y = x}.
+  defining \mzninline{y}, \mzninline{pow(i, 2)}, will be found in the \gls{cse}
+  table and replaced by the earlier stored result: \mzninline{y = x}.
 \end{example}
 
-It is worth noting that the CSE approach based on memorisation also covers the
-static example above, where the compiler can enforce sharing of common
+It is worth noting that the \gls{cse} approach based on memorisation also covers
+the static example above, where the compiler can enforce sharing of common
 subexpressions before evaluation begins. However, since the static analysis is
 cheap and can potentially avoid many dynamic table lookups, it is valuable to
 combine both approaches. The static approach can be further improved by
@@ -991,17 +991,17 @@ detect that a reified constraint is in fact not required.
 If a constraint is present in the root context, it means that it must hold
 globally. If the same constraint is used in a reified context, it can therefore
 be replaced with the constant \mzninline{true}, avoiding the need for
-reification (or in fact any evaluation). We can harness CSE to store the
+reification (or in fact any evaluation). We can harness \gls{cse} to store the
 evaluation context when a constraint is added, and detect when the same
-constraint is used in both contexts. Whenever a lookup in the CSE table is
+constraint is used in both contexts. Whenever a lookup in the \gls{cse} table is
 successful, action can be taken depending on both the current and stored
 evaluation context. If the stored expression was in root context, the constant
 \mzninline{true} can be used, independent of the current context. If the stored
-expression was in reified context and the current context is reified, the
-stored result variable can be used. If the stored expression was in reified
-context and the current context is root context, then the previous result can
-be replaced by the constant \mzninline{true} (and all its dependencies removed)
-and the evaluation will proceed as normal with the root context constraint.
+expression was in reified context and the current context is reified, the stored
+result variable can be used. If the stored expression was in reified context and
+the current context is root context, then the previous result can be replaced by
+the constant \mzninline{true} (and all its dependencies removed) and the
+evaluation will proceed as normal with the root context constraint.
 \begin{example}
   Consider the fragment:
 
@@ -1016,7 +1016,7 @@ and the evaluation will proceed as normal with the root context constraint.
   \mzninline{q(x)} for the original call. Suppose processing the second
   constraint we discover \mzninline{t(x,y)} is \mzninline{true}, setting
   \mzninline{b1}. When we process \mzninline{q(x)} in the call
-  \mzninline{t(x,y)} we find it is the root context. So CSE needs to set
+  \mzninline{t(x,y)} we find it is the root context. So \gls{cse} needs to set
   \mzninline{b0} to \mzninline{true}.
 \end{example}