diff --git a/.chktexrc b/.chktexrc
index d1fd2ad..c9a9413 100644
--- a/.chktexrc
+++ b/.chktexrc
@@ -1,4 +1,5 @@
 # Exclude these environments from syntax checking
 VerbEnvir { pgfpicture tikzpicture mzn nzn grammar proof }
+MathCmd { hypo infer1 infer2 infer3 }
 
 WipeArg { \mzninline:{} \nzninline:{} \Sem:{} \texttt:{} }
diff --git a/assets/packages.tex b/assets/packages.tex
index f2fc2b9..6c1cc50 100644
--- a/assets/packages.tex
+++ b/assets/packages.tex
@@ -84,7 +84,7 @@ style=apa,
 
 % Proof Tree
 \usepackage[nounderscore]{syntax}
-\usepackage{bussproofs}
+\usepackage{ebproof}
 
 % Half Reif packages (maybe we should get rid of these)
 \usepackage[all]{xy}
diff --git a/chapters/4_rewriting.tex b/chapters/4_rewriting.tex
index 256e3be..42fbf32 100644
--- a/chapters/4_rewriting.tex
+++ b/chapters/4_rewriting.tex
@@ -308,57 +308,35 @@ suitable alpha renaming.
 \begin{figure*}
 \centering
 \begin{prooftree}
-  \AxiomC{\(\ptinline{F(\(p_1, \ldots, p_k\)) = E;} \in \Prog\) where the \(p_i\)
-    are fresh}
-  \noLine{}
-  \UnaryInfC{\Sem{\(a_i\)}{\Prog, \Env_{i-1}} \(\Rightarrow~ \tuple{v_i,
-      \Env_i'}, \ \Env_0=\Env, \Env_i=\Env_i'\cup\{p_i\mapsto v_i\sep[]\}
-    \quad \forall
-    1 \leq
-    i \leq k\)}
-   \noLine{}
-   \UnaryInfC{\Sem{E}{\Prog, \Env_k}
-       \(\Rightarrow ~ \tuple{v, \Env'}\)}
-  \RightLabel{(Call)}
-  \UnaryInfC{\Sem{F(\(a_1, \ldots, a_k\))}{\Prog, \Env} \(\Rightarrow\)
-    \(\tuple{v, \Env'}\)}
-\end{prooftree}
+  \hypo{\ptinline{F(\(p_1, \ldots, p_k\)) = E;} \in \Prog \text{~where the~} p_i \text{~are fresh}}
+  \infer[no rule]1{\Sem{\(a_i\)}{\Prog, \Env_{i-1}} \Rightarrow \tuple{v_i,
+      \Env_i'}, \ \Env_0=\Env, \Env_i=\Env_i'\cup\{p_i\mapsto v_i\sep[]\}, \forall 1 \leq i \leq k}
+   \infer[no rule]1{\Sem{E}{\Prog, \Env_k} \Rightarrow \tuple{v, \Env'}}
+  \infer1[(Call)]{\Sem{F(\(a_1, \ldots, a_k\))}{\Prog, \Env_{0}} \Rightarrow \tuple{v, \Env'}}
+\end{prooftree} \\
+\medskip
 \begin{prooftree}
-  \AxiomC{\(\ptinline{F} \in\) Builtins}
-%  \noLine
-  \AxiomC{\Sem{\(a_i\)}{\Prog, \Env} \(\Rightarrow~ \tuple{v_i, \Env},
-    \forall
-    1 \leq
-    i \leq k\)}
-%    \(\ldots\), \Sem{\(a_k\)}{\Prog, \Env} \(\Rightarrow~\tuple{\Ctx_k,v_k}\)}
-  \RightLabel{(CallBuiltin)}
-  \BinaryInfC{\Sem{F(\(a_1, \ldots, a_k\))}{\Prog, \Env} \(\Rightarrow\)
-    \(\tuple{ \mathit{eval}(\ptinline{F}(v_1,\ldots, v_k)), \Env}\)}
-\end{prooftree}
+  \hypo{\ptinline{F} \in \text{Builtins}}
+  \hypo{\Sem{\(a_i\)}{\Prog, \Env} \Rightarrow \tuple{v_i, \Env}, \forall{} 1 \leq{} i \leq{} k}
+  \infer2[(CallBuiltin)]{\Sem{F(\(a_1, \ldots, a_k\))}{\Prog, \Env} \Rightarrow \tuple{ \mathit{eval}(\ptinline{F}(v_1,\ldots, v_k)), \Env}}
+\end{prooftree} \\
+\medskip
 \begin{prooftree}
-  \AxiomC{\(\ptinline{F(\(p_1, \ldots, p_k\));} \in \Prog\)}
-%  \noLine
-  \AxiomC{\Sem{\(a_i\)}{\Prog, \Env_{i-1}} \(\Rightarrow~ \tuple{v_i, \Env_i},
-    ~\forall
-    1 \leq
-    i \leq k\)}
-%    \(\ldots\), \Sem{\(a_k\)}{\Prog, \Env} \(\Rightarrow~\tuple{\Ctx_k,v_k}\)}
-  \RightLabel{(CallPrimitive)}
-  \BinaryInfC{\Sem{F(\(a_1, \ldots, a_k\))}{\Prog, \Env_0} \(\Rightarrow\)
-    \(\tuple{ x, \{ x \mapsto \ptinline{F}(v_1,\ldots, v_k) \sep [] \} \cup \Env_k}\)}
+  \hypo{\ptinline{F(\(p_1, \ldots, p_k\));} \in \Prog}
+  \hypo{\Sem{\(a_i\)}{\Prog, \Env_{i-1}} \Rightarrow \tuple{v_i, \Env_i}, \forall 1 \leq i \leq k}
+  \infer2[(CallPrimitive)]{\Sem{F(\(a_1, \ldots, a_k\))}{\Prog, \Env_0} \Rightarrow
+    \tuple{ x, \{ x \mapsto \ptinline{F}(v_1,\ldots, v_k) \sep [] \} \cup \Env_k}}
 \end{prooftree}
 \caption{\label{fig:4-rewrite-to-nzn-calls} Rewriting rules for partial evaluation
   of \microzinc\ calls to \nanozinc.}
 \end{figure*}
 
-The rules in \cref{fig:4-rewrite-to-nzn-calls} handle function calls.
-
-The first rule (Call) evaluates a function call expression in the context of a
-\microzinc\ program \(\Prog\) and \nanozinc\ program \(\Env\). The rule first
-evaluates all actual parameter expressions \(a_i\), creating new contexts where
-the evaluation results are bound to the formal parameters \(p_i\). It then
-evaluates the function body \(\ptinline{E}\) on this context, and returns the
-result.
+The rules in \cref{fig:4-rewrite-to-nzn-calls} handle function calls. The first
+rule (Call) evaluates a function call expression in the context of a \microzinc\
+program \(\Prog\) and \nanozinc\ program \(\Env\). The rule first evaluates all
+actual parameter expressions \(a_i\), creating new contexts where the evaluation
+results are bound to the formal parameters \(p_i\). It then evaluates the
+function body \(\ptinline{E}\) on this context, and returns the result.
 
 The (CallBuiltin) rule applies to ``built-in'' functions that can be evaluated
 directly, such as arithmetic and Boolean operations on fixed values. The rule
@@ -374,52 +352,41 @@ simply the function applied to the evaluated parameters.
 \begin{figure*}
 \centering
 \begin{prooftree}
-  \AxiomC{\Sem{\(\mathbf{I}\)}{\Prog, \Env} \(\Rightarrow (\Ctx, \Env')\)}
-  \AxiomC{\Sem{\(E\)}{\Prog, \Env'} \(\Rightarrow \tuple{v, \Env''}\)}
-  \AxiomC{\(x\) fresh}
-  \RightLabel{(LetC)}
-  \TrinaryInfC{\Sem{let \{  \(\mathbf{I}\) \} in \(E\)}{\Prog, \Env} \(\Rightarrow
-    \tuple{x, \{ x \mapsto v \sep \Ctx \} \cup \Env''}\)}
-\end{prooftree}
-% \begin{prooftree}
-%   \AxiomC{\Sem{\(E_1\)}{\Prog, \Env} \(\Rightarrow \Ctx_1, r_1\)}
-%   \AxiomC{\Sem{\(E_2\)}{\Prog, \Env} \(\Rightarrow \Ctx_2, r_2\)}
-%   \RightLabel{(Rel)}
-%   \BinaryInfC{\Sem{\(E_1 \bowtie E_2\)}{\Prog, \Env} \(\Rightarrow \Ctx_1 \wedge \Ctx_2 \wedge (r_1 \bowtie r_2)\)}
-% \end{prooftree}
+  \hypo{\Sem{\(\mathbf{I}\)}{\Prog, \Env} \Rightarrow (\Ctx, \Env')}
+  \hypo{\Sem{\(E\)}{\Prog, \Env'} \Rightarrow \tuple{v, \Env''}}
+  \hypo{x \text{~fresh}}
+  \infer3[(LetC)]{\Sem{let \{ \(\mathbf{I}\) \} in \(E\)}{\Prog, \Env} \Rightarrow
+    \tuple{x, \{ x \mapsto v \sep \Ctx \} \cup \Env''}}
+\end{prooftree} \\
+\medskip
 \begin{prooftree}
-  \AxiomC{}
-  \RightLabel{(Item0)}
-  \UnaryInfC{\Sem{\(\epsilon\)}{\Prog, \Env} \(\Rightarrow
-    (\ptinline{true}, \Env\))}
-\end{prooftree}
+  \hypo{}
+  \infer1[(Item0)]{\Sem{\(\epsilon\)}{\Prog, \Env} \Rightarrow \tuple{\ptinline{true}, \Env}}
+\end{prooftree} \\
+\medskip
 \begin{prooftree}
-  \AxiomC{\Sem{\(\mathbf{I}\)}{\Prog, \Env\ \cup\ \{x \mapsto\ \texttt{mkvar()} \sep\ []\}} \(\Rightarrow (\Ctx, \Env')\)}
-  \RightLabel{(ItemT)}
-  \UnaryInfC{\Sem{\(t:x, \mathbf{I}\)}{\Prog, \Env} \(\Rightarrow
-    (\Ctx, \Env')\)}
-\end{prooftree}
+  \hypo{\Sem{\(\mathbf{I}\)}{\Prog, \Env\ \cup\ \{x \mapsto\ \texttt{mkvar()} \sep\ []\}} \Rightarrow \tuple{\Ctx, \Env'}}
+  \infer1[(ItemT)]{\Sem{\(t:x, \mathbf{I}\)}{\Prog, \Env} \Rightarrow \tuple{\Ctx, \Env'}}
+\end{prooftree} \\
+\medskip
 \begin{prooftree}
-  \AxiomC{\Sem{\(E\)}{\Prog, \Env} \(\Rightarrow \tuple{v, \Env'}\)}
-  \AxiomC{\Sem{\(\mathbf{I}\)}{\Prog, \Env' \cup\ \{x \mapsto\ v \sep\ [] \}} \(\Rightarrow (\Ctx, \Env'')\)}
-  \RightLabel{(ItemTE)}
-  \BinaryInfC{\Sem{\(t:x = E, \mathbf{I}\)}{\Prog, \Env} \(\Rightarrow
-    (\Ctx, \Env'')\)}
-\end{prooftree}
+  \hypo{\Sem{\(E\)}{\Prog, \Env} \Rightarrow \tuple{v, \Env'}}
+  \hypo{\Sem{\(\mathbf{I}\)}{\Prog, \Env' \cup\ \{x \mapsto\ v \sep\ [] \}} \Rightarrow \tuple{\Ctx, \Env''}}
+  \infer2[(ItemTE)]{\Sem{\(t:x = E, \mathbf{I}\)}{\Prog, \Env} \Rightarrow \tuple{\Ctx, \Env''}}
+\end{prooftree} \\
+\medskip
 \begin{prooftree}
-  \AxiomC{\Sem{\(E\)}{\Prog, \Env} \(\Rightarrow \tuple{\left(v_{1}, \ldots, v_{n}\right), \Env'}\)}
-  \noLine{}
-  \UnaryInfC{\Sem{\(\mathbf{I}\)}{\Prog, \Env' \cup\ \{x_{1} \mapsto\ v_{1} \sep\ [] \} \cup\ \ldots\ \cup\ \{x_{n} \mapsto\ v_{n} \sep\ [] \}} \(\Rightarrow (\Ctx, \Env'')\)}
-  \RightLabel{(ItemTD)}
-  \UnaryInfC{\Sem{\(\left(t_{1}: x_{1}, \ldots, t_{n}: x_{n}\right) = E, \mathbf{I}\)}{\Prog, \Env} \(\Rightarrow
-    (\Ctx, \Env'')\)}
-\end{prooftree}
+  \hypo{\Sem{\(E\)}{\Prog, \Env} \Rightarrow \tuple{\left(v_{1}, \ldots, v_{n}\right), \Env'}}
+  \infer[no rule]1{\Sem{\(\mathbf{I}\)}{\Prog, \Env' \cup\ \{x_{1} \mapsto\ v_{1} \sep\ [] \} \cup\ \ldots\ \cup\ \{x_{n} \mapsto\ v_{n} \sep\ [] \}} \Rightarrow \tuple{\Ctx, \Env''}}
+  \infer1[(ItemTD)]{\Sem{\(\left(t_{1}: x_{1}, \ldots, t_{n}: x_{n}\right) = E, \mathbf{I}\)}{\Prog, \Env} \Rightarrow
+    \tuple{\Ctx, \Env''}}
+\end{prooftree} \\
+\medskip
 \begin{prooftree}
-  \AxiomC{\Sem{\(C\)}{\Prog, \Env} \(\Rightarrow \tuple{v, \Env'}\)}
-  \AxiomC{\Sem{\(\mathbf{I}\)}{\Prog, \Env'} \(\Rightarrow (\Ctx, \Env'')\)}
-  \RightLabel{(ItemC)}
-  \BinaryInfC{\Sem{\(\mbox{constraint~} C, \mathbf{I}\)}{\Prog, \Env} \(\Rightarrow
-    (\{v\}\cup\Ctx, \Env'')\)}
+  \hypo{\Sem{\(C\)}{\Prog, \Env} \Rightarrow \tuple{v, \Env'}}
+  \hypo{\Sem{\(\mathbf{I}\)}{\Prog, \Env'} \Rightarrow \tuple{\Ctx, \Env''}}
+  \infer2[(ItemC)]{\Sem{\(\mbox{constraint~} C, \mathbf{I}\)}{\Prog, \Env} \Rightarrow
+    \tuple{\{v\}\cup\Ctx, \Env''}}
 \end{prooftree}
 \caption{\label{fig:4-rewrite-to-nzn-let} Rewriting rules for partial evaluation
   of \microzinc\ let expressions to \nanozinc.}
@@ -439,64 +406,57 @@ is the base case for a list of let items.
 \begin{figure*}
 \centering
 \begin{prooftree}
-  \RightLabel{(IdC)}
-  \AxiomC{\(x \in \langle ident \rangle\)}
-  \AxiomC{\(v \in \langle literal \rangle\)}
-  \BinaryInfC{\Sem{\(x\)}{\Prog, \{x \mapsto\ v \sep\ []\} \cup\ \Env} \(\Rightarrow \tuple{v, \{x \mapsto v \sep [] \} \cup \Env}\)}
-\end{prooftree}
+  \hypo{x \in \syntax{<ident>}}
+  \hypo{v \in \syntax{<literal>}}
+  \infer2[(IdC)]{\Sem{\(x\)}{\Prog, \{x \mapsto\ v \sep\ []\} \cup\ \Env} \Rightarrow \tuple{v, \{x \mapsto v \sep [] \} \cup \Env}}
+\end{prooftree} \\
+\medskip
 \begin{prooftree}
-  \RightLabel{(IdX)}
-  \AxiomC{\(x \in \langle ident \rangle\)}
-  \AxiomC{\(v\)}
-  \AxiomC{\(\phi\) otherwise}
-  \TrinaryInfC{\Sem{\(x\)}{\Prog, \{x \mapsto\ v \sep\ \phi\ \} \cup\ \Env} \(\Rightarrow \tuple{x, \{x \mapsto v \sep \phi \} \cup \Env}\)}
-\end{prooftree}
+  \hypo{x \in \syntax{<ident>}}
+  \hypo{v}
+  \hypo{\phi \text{~otherwise}}
+  \infer3[(IdX)]{\Sem{\(x\)}{\Prog, \{x \mapsto\ v \sep\ \phi\ \} \cup\ \Env} \Rightarrow \tuple{x, \{x \mapsto v \sep \phi \} \cup \Env}}
+\end{prooftree} \\
+\medskip
 \begin{prooftree}
-  \RightLabel{(Const)}
-  \AxiomC{\(c\) constant}
-  \UnaryInfC{\Sem{c}{\Prog, \Env} \(\Rightarrow \tuple{c, \Env}\)}
-\end{prooftree}
+  \hypo{c \text{~constant}}
+  \infer1[(Const)]{\Sem{c}{\Prog, \Env} \Rightarrow \tuple{c, \Env}}
+\end{prooftree} \\
+\medskip
 \begin{prooftree}
-  \RightLabel{(Tuple)}
-  \AxiomC{\Sem{\(E_{1}\)}{\Prog,\Env} \(\Rightarrow \tuple{v_{1}, \Env^{1}}\)}
-  \AxiomC{\ldots}
-  \AxiomC{\Sem{\(E_{n}\)}{\Prog,\Env^{n-1}} \(\Rightarrow \tuple{v_{n}, \Env^{n}}\)}
-  \TrinaryInfC{\Sem{\(\left(E_{1}, \ldots, E_{n}\right)\)}{\Prog, \Env} \(\Rightarrow \tuple{x, \{x \mapsto \left(v_{1}, \ldots, v_{n}\right) \sep [] \} \cup \Env^{n})}\)}
-\end{prooftree}
+  \hypo{\Sem{\(E_{i}\)}{\Prog,\Env^{i-1}} \Rightarrow \tuple{v_{i}, \Env^{i}}, \forall{} 1 \leq{} i \leq{} k}
+  \infer1[(Tuple)]{\Sem{\(\left(E_{1}, \ldots, E_{k}\right)\)}{\Prog, \Env^{0}} \Rightarrow \tuple{x, \{x \mapsto \left(v_{1}, \ldots, v_{n}\right) \sep [] \} \cup \Env^{k}}}
+\end{prooftree} \\
+\medskip
 \begin{prooftree}
-  \RightLabel{(If\(_T\))}
-  \AxiomC{\Sem{\(C\)}{\Prog, \Env} \(\Rightarrow\) \(\tuple{\ptinline{true}, \_}\)}
-  \UnaryInfC{\Sem{if \(C\) then \(E_t\) else \(E_e\) endif}{\Prog, \Env} \(\Rightarrow\) \Sem{\(E_t\)}{\Prog, \Env}}
-\end{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}}
+\end{prooftree} \\
+\medskip
 \begin{prooftree}
-  \RightLabel{(If\(_F\))}
-  \AxiomC{\Sem{\(C\)}{\Prog, \Env} \(\Rightarrow\) \(\tuple{\ptinline{false}, \_}\)}
-  \UnaryInfC{\Sem{if \(C\) then \(E_t\) else \(E_e\) endif}{\Prog, \Env} \(\Rightarrow\) \Sem{\(E_e\)}{\Prog, \Env}}
-\end{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}}
+\end{prooftree} \\
+\medskip
 \begin{prooftree}
-  \AxiomC{\Sem{G}{\Prog,\Env} \(\Rightarrow \tuple{ \ptinline{true}, \_}\)}
-  \AxiomC{\Sem{\(E\)}{\Prog, \Env} \(\Rightarrow \tuple {v, \Env'}\)}
-    \RightLabel{(WhereT)}
-  \BinaryInfC{\Sem{\([E ~|~ \mbox{where~} G]\)}{\Prog, \Env} \(\Rightarrow
-    \tuple{[v], \Env'}\)}
-\end{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'}}
+\end{prooftree} \\
+\medskip
 \begin{prooftree}
-  \AxiomC{\Sem{G}{\Prog,\Env} \(\Rightarrow \tuple{ \ptinline{false}, \_}\)}
-    \RightLabel{(WhereF)}
-  \UnaryInfC{\Sem{\([E ~|~ \mbox{where~} G]\)}{\Prog, \Env} \(\Rightarrow
-    \tuple{[], \Env}\)}
-\end{prooftree}
+  \hypo{\Sem{G}{\Prog,\Env} \Rightarrow \tuple{\ptinline{false}, \_}}
+  \infer1[(WhereF)]{\Sem{\([E ~|~ \mbox{where~} G]\)}{\Prog, \Env} \Rightarrow \tuple{[], \Env}}
+\end{prooftree} \\
+\medskip
 \begin{prooftree}
-  \AxiomC{\Sem{\(\mathit{PE}\)}{\Prog,\Env} \(\Rightarrow \tuple{S, \_}\)}
-  \noLine\
-  \UnaryInfC{\Sem{\([E ~|~ \mathit{GE} \mbox{~where~} G]\)}{\Prog, \Env\ \cup\ \{ x\mapsto\
+  \hypo{\Sem{\(\mathit{PE}\)}{\Prog,\Env} \Rightarrow \tuple{S, \_}}
+  \infer[no rule]1{\Sem{\([E ~|~ \mathit{GE} \mbox{~where~} G]\)}{\Prog, \Env\ \cup\ \{ x\mapsto\
       v \sep\ []\}}}
-  \noLine\
-  \UnaryInfC{\hspace{8em} \(\Rightarrow \tuple{A_v, \Env \cup \{x \mapsto v \sep []\} \cup \Env_v}, \forall
-    v \in S \)}
-  \RightLabel{(ListG)}
-  \UnaryInfC{\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{\hspace{8em} \Rightarrow \tuple{A_v, \Env \cup \{x \mapsto v \sep []\} \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.}