diff --git a/chapters/4_rewriting.tex b/chapters/4_rewriting.tex
index 5c80b50..65457ee 100644
--- a/chapters/4_rewriting.tex
+++ b/chapters/4_rewriting.tex
@@ -82,6 +82,7 @@ and where expressions have \mzninline{par} type.
       \alt "let" "{" <item>* "}" "in" <literal>
       \alt "if" <exp> "then" <exp> "else" <exp> "endif"
       \alt "[" <exp> "|" <gen-exp> "where" <exp> "]"
+      \lat <ident>"[" <literal> "]"
 
     <item> ::= <param> [ "=" <exp> ]";"
       \alt "tuple(" <type-inst> ["," <type-inst>]* "):" <ident> = "(" <exp> ["," <exp>]* ")";
@@ -303,19 +304,19 @@ suitable alpha renaming.
 \centering
 \begin{prooftree}
   \hypo{\texttt{function} ~t\texttt{:}~\ptinline{F(\(p_1, \ldots{}, p_k\)) = E;} \in{} \Prog{} \text{~where the~} p_i \text{~are fresh}}
-  \infer[no rule]1{\Sem{\(\ptinline{E}_{[p_i \mapsto a_i, \forall{} 1 \leq{} i \leq{} k]}\)}{\Prog, \Env}} \Rightarrow \tuple{v, \Env'}
+  \infer[no rule]1{\Sem{\(\ptinline{E}_{[p_i \mapsto a_i, \forall{} 1 \leq{} i \leq{} k]}\)}{\Prog, \Env}} \Rightarrow{} \tuple{v, \Env'}
   \infer1[(Call)]{\Sem{F(\(a_1, \ldots, a_k\))}{\Prog, \Env} \Rightarrow{} \tuple{v, \Env'}}
 \end{prooftree} \\
 \bigskip
 \begin{prooftree}
   \hypo{\ptinline{F} \in \text{Builtins}}
-  \infer1[(CallBuiltin)]{\Sem{F(\(a_1, \ldots, a_k\))}{\Prog, \Env} \Rightarrow{} \tuple{ \mathit{eval}(\ptinline{F}(a_1,\ldots, a_k)), \Env}}
+  \infer1[(CallBuiltin)]{\Sem{F(\(a_1, \ldots, a_k\))}{\Prog, \Env} \Rightarrow{} \tuple{\ensuremath{\mathit{eval}(\ptinline{F}(a_1,\ldots, a_k))}, \Env}}
 \end{prooftree} \\
 \bigskip
 \begin{prooftree}
   \hypo{\texttt{predicate}~\ptinline{F(\(p_1, \ldots, p_k\));} \in \Prog}
-  \infer1[(CallPredicate)]{\Sem{F(\(a_1, \ldots, a_k\))}{\Prog, \Env_0} \Rightarrow
-    \tuple{\texttt{constraint}~\ptinline{F}(a_1, \ldots, a_k), \Env_k}}
+  \infer1[(CallPredicate)]{\Sem{F(\(a_1, \ldots, a_k\))}{\Prog, \Env_0} \Rightarrow{}
+    \tuple{\ensuremath{\texttt{constraint}~\ptinline{F}(a_1, \ldots, a_k), \Env_k}}}
 \end{prooftree}
 \caption{\label{fig:4-rewrite-to-nzn-calls} Rewriting rules for partial evaluation
   of \microzinc\ calls to \nanozinc.}
@@ -347,13 +348,13 @@ considered primitives, and as such simply need to be transferred into the
 \end{prooftree} \\
 \bigskip
 \begin{prooftree}
-  \hypo{\Sem{\(\mathbf{X}\)}{\Prog, \{ t : x \} \cup{} \Env} \Rightarrow \tuple{x, \{ t : x \} \cup{} \Env'}}
-  \infer1[(Item0)]{\Sem{\(\epsilon{} \mid{} \mathbf{X}\)}{\Prog, \{ t : x \}\cup{}\Env, \Ctx} \Rightarrow \tuple{x, \{ t : x_{\texttt{~└──~}} \Ctx \} \cup \Env'}}
+  \hypo{\Sem{\(\mathbf{X}\)}{\Prog, \{ t : x \} \cup{} \Env} \Rightarrow \tuple{x, \{ t: x \} \cup{} \Env'}}
+  \infer1[(Item0)]{\Sem{\(\epsilon{} \mid{} \mathbf{X}\)}{\Prog, \{ t: x \}\cup{}\Env, \Ctx} \Rightarrow{} \tuple{x, \{ t: x_{\texttt{~└──~}} \Ctx{} \} \cup{} \Env'}}
 \end{prooftree} \\
 \bigskip
 \begin{prooftree}
   \hypo{\Sem{\(\mathbf{I} \mid{} \mathbf{X}\)}{\Prog, \Env\ \cup\ \{t : x\}, \Ctx} \Rightarrow \tuple{x, \Env'}}
-  \infer1[(ItemT)]{\Sem{\(t\texttt{:}~x\texttt{;} \mathbf{I} \mid{} \mathbf{X}\)}{\Prog, \Env, \Ctx} \Rightarrow \tuple{x, \Env'}}
+  \infer1[(ItemT)]{\Sem{\(t\texttt{:}~x\texttt{;} \mathbf{I} \mid{} \mathbf{X}\)}{\Prog, \Env, \Ctx} \Rightarrow{} \tuple{x, \Env'}}
 \end{prooftree} \\
 \bigskip
 \begin{prooftree}
@@ -365,7 +366,7 @@ considered primitives, and as such simply need to be transferred into the
 \begin{prooftree}
   \hypo{\Sem{\(E_{i}\)}{\Prog,\Env^{i-1}} \Rightarrow \tuple{v_{i}, \Env^{i}}, \forall{} 1 \leq{} i \leq{} k}
   \infer[no rule]1{\Sem{\(\mathbf{I}_{[x_{\langle{}i\rangle} \mapsto v_{i}, \forall{} 1 \leq{} i \leq{} k]} \mid{} \mathbf{X}_{[x_{\langle{}i\rangle} \mapsto v_{i}, \forall{} 1 \leq{} i \leq{} k]}\)}{\Prog, \Env^{k}, \Ctx} \Rightarrow\ \tuple{x, \Env'}}
-  \infer1[(ItemTupC)]{\Sem{\( \texttt{tuple(}t_{1}, \ldots, t_{k}\texttt{):}~x = \left(E_{1}, \ldots, E_{k}\right)\)}{\Prog, \Env^{0}, \Ctx} \Rightarrow \tuple{x, \Env'}}
+  \infer1[(ItemTupC)]{\Sem{\( \texttt{tuple(}t_{1}, \ldots, t_{k}\texttt{):}~x = \left(E_{1}, \ldots, E_{k}\right)\)}{\Prog, \Env^{0}, \Ctx} \Rightarrow{} \tuple{x, \Env'}}
 \end{prooftree} \\
 \bigskip
 \begin{prooftree}
@@ -408,40 +409,47 @@ notation.
   \hypo{x \in \langle \text{ident} \rangle}
   \hypo{v}
   \hypo{\phi \text{~otherwise}}
-  \infer3[(IdX)]{\Sem{\(x\)}{\Prog, \{t: x^{\texttt{~└──~}} \phi\ \} \cup\ \Env} \Rightarrow \tuple{x, \{t: x^{\texttt{~└──~}} \phi \cup \phi}}
+  \infer3[(IdX)]{\Sem{\(x\)}{\Prog, \{t: x^{\texttt{~└──~}} \phi\ \} \cup\ \Env} \Rightarrow{} \tuple{x, \{t: x^{\texttt{~└──~}} \phi{} \cup{} \Env}}
+\end{prooftree} \\
+\bigskip
+\begin{prooftree}
+  \hypo{\Sem{\(x\)}{\Prog, \Env} \Rightarrow \tuple{[x_{1}, \ldots, x_{n}], \Env'}}
+  \hypo{\Sem{\(i\)}{\Prog, \Env'} \Rightarrow \tuple{v, \Env''}}
+  \hypo{v \in [1 \ldots{} n]}
+  \infer3[(Access)]{\Sem{\(x\texttt{[}i\texttt{]}\)}{\Prog, \Env} \Rightarrow{} \tuple{x_{v}, \Env''}}
 \end{prooftree} \\
 \bigskip
 \begin{prooftree}
   \hypo{c \text{~constant}}
-  \infer1[(Const)]{\Sem{\(c\)}{\Prog, \Env} \Rightarrow \tuple{c, \Env}}
+  \infer1[(Const)]{\Sem{\(c\)}{\Prog, \Env} \Rightarrow{} \tuple{c, \Env}}
 \end{prooftree} \\
 \bigskip
 \begin{prooftree}
   \hypo{\Sem{\(C\)}{\Prog, \Env} \Rightarrow \tuple{\ptinline{true}, \_}}
-  \infer1[(If\(_T\))]{\Sem{if \(C\) then \(E_t\) else \(E_e\) endif}{\Prog, \Env} \Rightarrow \Sem{\(E_t\)}{\Prog, \Env}}
+  \infer1[(If\(_T\))]{\Sem{if \(C\) then \(E_t\) else \(E_e\) endif}{\Prog, \Env} \Rightarrow{} \Sem{\(E_t\)}{\Prog, \Env}}
 \end{prooftree} \\
 \bigskip
 \begin{prooftree}
   \hypo{\Sem{\(C\)}{\Prog, \Env} \Rightarrow \tuple{\ptinline{false}, \_}}
-  \infer1[(If\(_F\))]{\Sem{if \(C\) then \(E_t\) else \(E_e\) endif}{\Prog, \Env} \Rightarrow \Sem{\(E_e\)}{\Prog, \Env}}
+  \infer1[(If\(_F\))]{\Sem{if \(C\) then \(E_t\) else \(E_e\) endif}{\Prog, \Env} \Rightarrow{} \Sem{\(E_e\)}{\Prog, \Env}}
 \end{prooftree} \\
 \bigskip
 \begin{prooftree}
   \hypo{\Sem{G}{\Prog,\Env} \Rightarrow \tuple{ \ptinline{true}, \_}}
   \hypo{\Sem{\(E\)}{\Prog, \Env} \Rightarrow \tuple {v, \Env'}}
-  \infer2[(WhereT)]{\Sem{\([E ~|~ \mbox{where~} G]\)}{\Prog, \Env} \Rightarrow \tuple{[v], \Env'}}
+  \infer2[(WhereT)]{\Sem{\([E ~|~ \mbox{where~} G]\)}{\Prog, \Env} \Rightarrow{} \tuple{[v], \Env'}}
 \end{prooftree} \\
 \bigskip
 \begin{prooftree}
   \hypo{\Sem{G}{\Prog,\Env} \Rightarrow \tuple{\ptinline{false}, \_}}
-  \infer1[(WhereF)]{\Sem{\([E ~|~ \mbox{where~} G]\)}{\Prog, \Env} \Rightarrow \tuple{[], \Env}}
+  \infer1[(WhereF)]{\Sem{\([E ~|~ \mbox{where~} G]\)}{\Prog, \Env} \Rightarrow{} \tuple{[], \Env}}
 \end{prooftree} \\
 \bigskip
 \begin{prooftree}
   \hypo{\Sem{\(\mathit{PE}\)}{\Prog,\Env} \Rightarrow \tuple{S, \_}}
-  \infer[no rule]1{\Sem{\([E ~|~ \mathit{GE} \mbox{~where~} G]\)}{\Prog, \Env_{[x \mapsto v]}} \Rightarrow \tuple{A_v, \Env_{[x \mapsto v]} \cup \Env_v}, \forall{} v \in S }
-  \infer1[(ListG)]{\Sem{\([E~|~ x \mbox{~in~} \mathit{PE}, \mathit{GE} \mbox{~where~} G]\)}{\Prog, \Env} \Rightarrow
-    \tuple{\mbox{concat} [ A_v ~|~ v \in S ], \Env \cup \bigcup_{v \in S} \Env_v}}
+  \infer[no rule]1{\Sem{\([E ~|~ \mathit{GE} \mbox{~where~} G]\)}{\Prog, \Env_{[x \mapsto{} v]}} \Rightarrow{} \tuple{A_v, \Env_{[x \mapsto{} v]} \cup{} \Env{}_{v}}, \forall{} v \in{} S }
+  \infer1[(ListG)]{\Sem{\([E~|~ x \mbox{~in~} \mathit{PE}, \mathit{GE} \mbox{~where~} G]\)}{\Prog, \Env} \Rightarrow{}
+    \tuple{\mbox{concat} [ A_v~|~v \in{} S ], \Env{} \cup{} \bigcup{}_{v \in{} S} \Env{}_{v}}}
 \end{prooftree}
 \caption{\label{fig:4-rewrite-to-nzn-other} Rewriting rules for partial evaluation
   of other \microzinc\ expressions to \nanozinc.}