diff --git a/chapters/3_rewriting.tex b/chapters/3_rewriting.tex
index f86157c..c353870 100644
--- a/chapters/3_rewriting.tex
+++ b/chapters/3_rewriting.tex
@@ -92,7 +92,7 @@ The translation from \minizinc\ to \microzinc{} involves the following steps:
 		In contrast to \minizinc{}, the evaluation of \microzinc\ will implement strict semantics for partial expressions, whereas \minizinc\ uses relational semantics.
 		Stuckey and Tack have extensively examined these problems and describe how to transform any partial function into a total function.
 		\autocite*{stuckey-2013-functions}.
-		A general approach for describing the partially in \microzinc\ functions is to make the function return both a boolean variable that indicates the totality of the input variables and the resulting value of the function that is adjusted that is adjusted to return a predefined value when it would normally be undefined.
+		A general approach for describing the partially in \microzinc\ functions is to make the function return both a Boolean variable that indicates the totality with regards to the input variables and the resulting value of the function that is adjusted to return a predefined value when it would normally be undefined.
 		For example, The function
 
 		\begin{mzn}
@@ -105,15 +105,21 @@ The translation from \minizinc\ to \microzinc{} involves the following steps:
 		\begin{mzn}
 			function tuple(var int, var bool): element_safe(array of int: a, var int: x) =
 			let {
-				var bool: total = x in index_set(x);
-				var index_set(a): xs;
-				constraint total -> x = xs; % Give xs the value of x when result is total
-				var res = element(a, xs); % Use of element that is guaranteed to be total
+				set of int: idx = index_set(x)
+				var bool: total = x in idx;
+				var idx: xs;
+				int: m = min(idx);
+				% Give xs the value of x when result is total
+				constraint total -> xs = x; 
+				% Otherwise, give xs the value m instead.
+				constraint not total -> xs = m;
+				% element constraint that is guaranteed to be total
+				var res = element(a, xs); 
 				tuple(var int, var bool): ret = (res, total);
 			} in ret;
 		\end{mzn}
 
-		Similar to the replacement of optional values, all usage of the \mzninline{element} function are replaced by \mzninline{element_safe} and the usage of its result should be guarded by the returned totality variable in the surrounding boolean context.
+		Similar to the replacement of optional values, all usage of the \mzninline{element} function are replaced by \mzninline{element_safe} and the usage of its result should be guarded by the returned totality variable in the surrounding Boolean context.
 		This means that, for example, the expression \mzninline{element(e, v) = 5 \/ b} would be transformed into:
 
 		\begin{mzn}
@@ -134,9 +140,9 @@ The translation from \minizinc\ to \microzinc{} involves the following steps:
 			function f_int(int: x) = /* original body */;
 			function f_varint(varint: x) =
 			if is_fixed(x) then
-			f_int(x)
+				f_int(x)
 			else
-			/* original body */;
+				/* original body */;
 			endif;
 		\end{mzn}
 
@@ -840,27 +846,27 @@ These are very encouraging results, given that we are comparing a largely unopti
 \end{figure}
 
 
-\section{Summary}%
-\label{sec:rew-summary}
+% \section{Summary}%
+% \label{sec:rew-summary}
 
-In this chapter, we introduced a systematic view of the execution of \minizinc{}, revisiting the rewriting from high-level \minizinc\ to solver-level \flatzinc{}.
-We first introduced the intermediate languages \microzinc{} and \nanozinc{} and explained how \minizinc\ can be transformed into a set of \microzinc\ definitions and a \nanozinc\ program.
-We then, crucially, discussed how to partially evaluate a \nanozinc\ program using \microzinc\ definitions and present formal definitions of the rewriting rules applied during partial evaluation.
+% In this chapter, we introduced a systematic view of the execution of \minizinc{}, revisiting the rewriting from high-level \minizinc\ to solver-level \flatzinc{}.
+% We first introduced the intermediate languages \microzinc{} and \nanozinc{} and explained how \minizinc\ can be transformed into a set of \microzinc\ definitions and a \nanozinc\ program.
+% We then, crucially, discussed how to partially evaluate a \nanozinc\ program using \microzinc\ definitions and present formal definitions of the rewriting rules applied during partial evaluation.
 
-Continuously applying these rules would result in a correct solver-level model, but it is unlikely to be the best model for the solver.
-We, therefore, discuss multiple techniques to improve the solver-level constraint model during the partial evaluation of \nanozinc{}.
-First, we introduce a novel technique to eliminate all unused variables and constraints: we track all constraints that are introduced only to define a variable.
-This means we can keep an accurate count of when a variable becomes unused by counting only the references to a variable in constraints that do not help define it.
-Then, we discuss the use of \gls{propagation} during the partial evaluation of the \nanozinc\ program.
-This technique can help shrink the domains of the decision variable or even combine variables known to be equal.
-When a redefinition of a constraint requires the introspection into the current domain of a variable, it is often important to have the tightest possible domain.
-Hence, we discuss how in choosing the next \nanozinc\ constraint to rewrite, the interpreter can sometimes delay the rewriting of certain constraints to ensure the most amount of information is available.
-\Gls{cse}, our next optimisation technique, ensures that we do not create or evaluate the same constraint or function twice and reuse variables where possible.
-Finally, the last optimisation technique we discuss is the use of constraint \gls{aggregation}.
-The use of \gls{aggregation} ensures that individual functional constraints can be collected and combined into an aggregated form.
-This allows us to avoid the existence of intermediate variables in some cases.
-This optimisation is very important for \gls{mip} solvers.
+% Continuously applying these rules would result in a correct solver-level model, but it is unlikely to be the best model for the solver.
+% We, therefore, discuss multiple techniques to improve the solver-level constraint model during the partial evaluation of \nanozinc{}.
+% First, we introduce a novel technique to eliminate all unused variables and constraints: we track all constraints that are introduced only to define a variable.
+% This means we can keep an accurate count of when a variable becomes unused by counting only the references to a variable in constraints that do not help define it.
+% Then, we discuss the use of \gls{propagation} during the partial evaluation of the \nanozinc\ program.
+% This technique can help shrink the domains of the decision variable or even combine variables known to be equal.
+% When a redefinition of a constraint requires the introspection into the current domain of a variable, it is often important to have the tightest possible domain.
+% Hence, we discuss how in choosing the next \nanozinc\ constraint to rewrite, the interpreter can sometimes delay the rewriting of certain constraints to ensure the most amount of information is available.
+% \Gls{cse}, our next optimisation technique, ensures that we do not create or evaluate the same constraint or function twice and reuse variables where possible.
+% Finally, the last optimisation technique we discuss is the use of constraint \gls{aggregation}.
+% The use of \gls{aggregation} ensures that individual functional constraints can be collected and combined into an aggregated form.
+% This allows us to avoid the existence of intermediate variables in some cases.
+% This optimisation is very important for \gls{mip} solvers.
 
-Finally, we test the described system using an experimental implementation.
-We compare this experimental implementation against the current \minizinc\ interpreter, version 2.5.3, and look at both runtime and its memory usage.
-Although the experimental implementation there are instances where the experimental implementation uses more memory than the current \minizinc\ interpreter, it clearly outperforms the current \minizinc\ interpreter in terms of time.
+% Finally, we test the described system using an experimental implementation.
+% We compare this experimental implementation against the current \minizinc\ interpreter, version 2.5.3, and look at both runtime and its memory usage.
+% Although the experimental implementation there are instances where the experimental implementation uses more memory than the current \minizinc\ interpreter, it clearly outperforms the current \minizinc\ interpreter in terms of time.
diff --git a/chapters/3_rewriting_preamble.tex b/chapters/3_rewriting_preamble.tex
index 2ca1920..96047a2 100644
--- a/chapters/3_rewriting_preamble.tex
+++ b/chapters/3_rewriting_preamble.tex
@@ -48,8 +48,7 @@ This chapter is organised as follows. \Cref{sec:4-micronano} introduces the
 propose that enables more efficient flattening. \Cref{sec:4-simplification}
 describes how we can perform various processing and simplification steps on this
 representation, and in \cref{sec:4-experiments} we report on the experimental
-results of the prototype implementation. Finally, \Cref{sec:4-conclusion}
-presents our conclusions.
+results of the prototype implementation. 
 
 \begin{figure}
   \centering