diff --git a/paper/figures/quickselect-split.tex b/paper/figures/quickselect-split.tex
index 3d97357..7ef061b 100644
--- a/paper/figures/quickselect-split.tex
+++ b/paper/figures/quickselect-split.tex
@@ -10,7 +10,7 @@
   case l of
     Empty => Leaf
   | Cons ht => 
-      let (left,right,i) = partition ht in
+      let val (left,right,i) = partition ht in
       Branch (i, #1 ht, qs1 left, qSelect1 right)`
 
 2`fun qs2 (p : tree, k : int) : int = 
diff --git a/paper/splitting.tex b/paper/splitting.tex
index 1cb52b5..a8b9c1f 100644
--- a/paper/splitting.tex
+++ b/paper/splitting.tex
@@ -190,7 +190,7 @@ \subsection{Term Splitting at \bbonem}
 As a simple first case, consider splitting the unit value, $\tup{}$
 which masks to $\mval {\tup{}} {\tup{}}$.
 %Units trivial contain unit split into more units: $\tup{} \vsplito \mval {\tup{}} {\tup{}}$.
-Splitting must produce a $c$ and $l.r$ satisfying,
+Splitting must produce a $c$ and $l.r$ satisfying
 \[
 	\reduce c {\tup{\tup{},b}} \text{ and } [b/l]r \equiv \tup{}
 \]
@@ -199,13 +199,13 @@ \subsection{Term Splitting at \bbonem}
 component of $c$ now becomes the result of evaluating the \bbonep\ term $e$.
 
 \paragraph {Injections.}
-Now consider splitting the non-terminal, $\inl {e}$, where $\diaone
-{e} \xi v$ and $\rtab \xi v \vsplito \mval i q$. Therefore:
+Now consider splitting the non-terminal $\inl {e}$, where $\diaone
+{e} \xi v$ and $\rtab \xi v \vsplito \mval i q$, and thus:
 \[
 	\splitone e A c {l.r} \text{ and } \reduce c {\tup{i,b}} \text{ and } [b/l]r \equiv q
 \]
 Since $\diaone {\inl e} \xi {\inl v}$ and $\rtab \xi {\inl v} \vsplito \mval {\inl i} q$,
-splitting must produce a $c'$ and $l.r'$ satisfying,
+splitting must produce a $c'$ and $l.r'$ satisfying
 \[
 	\reduce {c'} {\tup{\inl i,b'}} \text{ and } [b'/l]r' \equiv q
 \]
@@ -215,7 +215,7 @@ \subsection{Term Splitting at \bbonem}
 c' = \letin {\tup {x,y}} c {\tup{\inl x, y}}
 \]
 Splitting the injection also generates the same resumer as splitting
-the subterm $e$: ($l.r' = l.r$).
+the subterm $e$ (that is, $l.r' = l.r$).
 
 \paragraph{Tuple.} For an example of splitting terms with more than one argument, consider the tuple $\tup{e_1,e_2}$,
 where $\diaone {e_k} {\xi_k} {v_k}$ and 
@@ -232,11 +232,11 @@ \subsection{Term Splitting at \bbonem}
 \]
 The resulting boundary value is the tuple of the boundary values of
 the subterms, $b = \tup{b_1,b_2}$.  The value is 
-constructed using,
+constructed using
 \[
 c = \letin{\tup{y_1,z_1}}{c_1}{\letin{\tup{y_2,z_2}}{c_2}{\tup{\tup{y_1, y_2},\tup{z_1, z_2}}}}
 \]
-And deconstructed in the resumer with the tuple pattern,
+and deconstructed in the resumer with a tuple pattern:
 \[
 l.r = \tup{l_1,l_2}.\tup{r_1,r_2}
 \]
@@ -254,12 +254,11 @@ \subsection{Term Splitting at \bbonem}
 Additionally, the first branch evaluates $\diaone {[v_1/x_2]e_2} {\xi_2} {v_2}$
 and $\rtab {\xi_1,\xi_2} {v_2} \vsplito \mval {i_2} {q_2}$.
 Therefore:
-\[
-	\splitone {e_2} A {c_2} {l_2.r_2} \text{ and } \reduce {[i_1/x_2]c_2} {\tup{i_2,b_2}} 
-\]
-\[
+\begin{gather*}
+	\splitone {e_2} A {c_2} {l_2.r_2} \text{ and } \reduce {[i_1/x_2]c_2}
+  {\tup{i_2,b_2}} \\
 \text{ and } [q_1/x_2][b_2/l_2]r_2 \equiv q_2
-\]
+\end{gather*}
 (Because $e_2$ is open on $x_2$, $\pipeM{c_2}{l_2}{r_2}$ is also open on $x_2$.
 When we substitute some $v_1$ for $x_2$ in $e_2$, we must substitute the masks
 of $v_1$ into $c_2$ and $l_2.r_2$.)
@@ -305,8 +304,8 @@ \subsection{Term Splitting at \bbonem}
 \paragraph {Function.} 
 Function introduction has a $\tup{}$ boundary value, since functions
 are already fully reduced in our semantics.  However, since the body
-of a function may itself be multistage, splitting must continue into
-it.  The first pass generated by split produces an $i$ that is a new
+of a function may itself be multistage, splitting must descend into
+it.  The first pass generated by splitting produces an $i$ that is a new
 function formed from the first-stage part of the original body.  The
 resumer is a new function formed out of the second-stage part of the
 original body.  It is the responsibility of the application site to
@@ -323,20 +322,20 @@ \subsection{Term Splitting at \bbtwo}
 Consider any $n$-ary \bbtwo-term $e = \scriptCapp {e_1 \ttsemi \ldots
   \ttsemi e_n}$ (except \texttt{prev}, which is discussed shortly).
 Note that for any $\diatwo e q$, the residual $q$ must have the form
-$\scriptCapp {q_1 \ttsemi \ldots \ttsemi q_n}$, even under binders and
-for nullary terms.  For each $k \in \{1,\ldots,n\}$ splitting the
-subterm $e_k$ yields $p_k$ and $l_k.r_k$ where:
+$\scriptCapp {q_1 \ttsemi \ldots \ttsemi q_n}$, even if $\mathcal{C}$ is
+nullary or the $q_i$ have binders.
+For each $k$, splitting the subterm $e_k$ yields $p_k$ and $l_k.r_k$ where
 \[
 	\reduce {p_k} {b_k} \text{ and } [{b_k}/{l_k}]{r_k} \equiv {q_k}
 \]
-Correspondingly, splitting the $n$-ary $\scriptCapp {e_1 \ttsemi \ldots \ttsemi e_n}$ generates $p$ and $l.r$ where:
+Correspondingly, splitting $\scriptCapp {e_1 \ttsemi \ldots \ttsemi e_n}$ generates $p$ and $l.r$ where
 \[
 	\reduce p b \text{ and } [b/l]r \equiv \scriptCapp {q_1 \ttsemi \ldots \ttsemi q_n}
 \]
 Our algorithm accomplishes this by using $p = \tup {p_1, \ldots, p_n}$ and
 $l.r = \tup {l_1, \ldots, l_n}.\scriptCapp {r_1 \ttsemi \ldots \ttsemi r_n}$.
 
-Again, this holds even for nullary terms and under binders.
+%Again, this holds even for nullary terms and under binders.
 In particular, $\caseof{e_1}{x_2.e_2}{x_3.e_3}$ splits into:
 \[
 \pipeS {\tup{p_1,p_2,p_3}} {\tup{l_1,l_2,l_3}} {\caseof{r_1}{x_2.r_2}{x_3.r_3}}
@@ -346,16 +345,16 @@ \subsection{Term Splitting at \bbtwo}
 first stage. This occurs regardless of what branch is eventually
 executed in the second stage.
 
-\paragraph{Next and Prev.}
+\paragraph{Staging constructs.}
 Since \texttt{next} and \texttt{prev} do nothing more than convert between 
 second-stage terms at \bbtwo\ and encapsulated second-stage terms at \bbonem,
 their splitting rules are relatively simple.
-Given $\diatwo e q$, splitting yields $p$ and $l.r$ where:
+Given $\diatwo e q$, splitting yields $p$ and $l.r$ where
 \[
 	\reduce p b \text{ and } [b/l]r \equiv q
 \]
 Then for $\diaone {\next {e}} {{\hat y} \mapsto q} {\next {\hat y}}$
-and\\ $\rtab {{\hat y} \mapsto q} {\next {\hat y}} \vsplito \mval {\tup{}} {\letin {\hat y} q {\hat y}}$, splitting must produce $c'$ and $l'.r'$ where:
+and\\ $\rtab {{\hat y} \mapsto q} {\next {\hat y}} \vsplito \mval {\tup{}} {\letin {\hat y} q {\hat y}}$, splitting must produce $c'$ and $l'.r'$ where
 \[
 	\reduce {c'} {\tup {\tup{},b'}} \text{ and } [b'/l']r' \equiv \letin {\hat y} q {\hat y}
 \]