--- a/ChengsongTanPhdThesis/Chapters/Inj.tex	Wed Aug 31 23:57:42 2022 +0100
+++ b/ChengsongTanPhdThesis/Chapters/Inj.tex	Thu Sep 01 23:47:37 2022 +0100
@@ -659,10 +659,10 @@
 			\multicolumn{3}{@{}l}{\textbf{Values}}\medskip\\
 			$v$ & $::=$  & \\
 			&        & $\Empty$   \\
-			& $\mid$ & $\Char(c)$          \\
+			& $\mid$ & $\Char \; c$          \\
 			& $\mid$ & $\Seq\,v_1\, v_2$\\
-			& $\mid$ & $\Left(v)$   \\
-			& $\mid$ & $\Right(v)$  \\
+			& $\mid$ & $\Left \;v$   \\
+			& $\mid$ & $\Right\;v$  \\
 			& $\mid$ & $\Stars\,[v_1,\ldots\,v_n]$ \\
 		\end{tabular}
 	\end{tabular}
@@ -674,28 +674,28 @@
 	\begin{tabular}{lcl}
 		$|\Empty|$ & $\dn$ &  $[]$\\
 		$|\Char \; c|$ & $ \dn$ & $ [c]$\\
-		$|\Seq(v_1, v_2)|$ & $ \dn$ & $ v_1| @ |v_2|$\\
-		$|\Left(v)|$ & $ \dn$ & $ |v|$\\
-		$|\Right(v)|$ & $ \dn$ & $ |v|$\\
-		$|\Stars([])|$ & $\dn$ & $[]$\\
-		$|\Stars(v::vs)|$ &  $\dn$ & $ |v| @ |\Stars(vs)|$
+		$|\Seq \; v_1, \;v_2|$ & $ \dn$ & $ v_1| @ |v_2|$\\
+		$|\Left \; v|$ & $ \dn$ & $ |v|$\\
+		$|\Right \; v|$ & $ \dn$ & $ |v|$\\
+		$|\Stars \; []|$ & $\dn$ & $[]$\\
+		$|\Stars \; v::vs|$ &  $\dn$ & $ |v| @ |\Stars(vs)|$
 	\end{tabular}
 \end{center}
 Sulzmann and Lu used a binary predicate, written $\vdash v:r $,
 to indicate that a value $v$ could be generated from a lexing algorithm
 with input $r$. They call it the value inhabitation relation. 
 \begin{mathpar}
-	\inferrule{\mbox{}}{\vdash \Char(c) : \mathbf{c}} \hspace{2em}
+	\inferrule{\mbox{}}{\vdash \Char \; c : \mathbf{c}} \hspace{2em}
 
 	\inferrule{\mbox{}}{\vdash \Empty :  \ONE} \hspace{2em}
 
-\inferrule{\vdash v_1 : r_1 \;\; \vdash v_2 : r_2 }{\vdash \Seq(v_1, v_2) : (r_1 \cdot r_2)}
+\inferrule{\vdash v_1 : r_1 \;\; \vdash v_2 : r_2 }{\vdash \Seq \; v_1,\; v_2 : (r_1 \cdot r_2)}
 
-\inferrule{\vdash v_1 : r_1}{\vdash \Left(v_1):r_1+r_2}
+\inferrule{\vdash v_1 : r_1}{\vdash \Left \; v_1 : r_1+r_2}
 
-\inferrule{\vdash v_2 : r_2}{\vdash \Right(v_2):r_1 + r_2}
+\inferrule{\vdash v_2 : r_2}{\vdash \Right \; v_2:r_1 + r_2}
 
-\inferrule{\forall v \in vs. \vdash v:r \land  |v| \neq []}{\vdash \Stars(vs):r^*}
+\inferrule{\forall v \in vs. \vdash v:r \land  |v| \neq []}{\vdash \Stars \; vs : r^*}
 \end{mathpar}
 \noindent
 The condition $|v| \neq []$ in the premise of star's rule