diff -r 1734bd5975a3 -r 4969ef817d92 ChengsongTanPhdThesis/Chapters/Bitcoded1.tex --- a/ChengsongTanPhdThesis/Chapters/Bitcoded1.tex Tue Aug 23 22:59:49 2022 +0100 +++ b/ChengsongTanPhdThesis/Chapters/Bitcoded1.tex Sat Aug 27 00:37:03 2022 +0100 @@ -568,7 +568,7 @@ $\textit{bmkeps}\,(_{bs} a_1 \cdot a_2)$ & $\dn$ & $bs \,@\,\textit{bmkeps}\,a_1\,@\, \textit{bmkeps}\,a_2$\\ $\textit{bmkeps}\,(_{bs}a^*)$ & $\dn$ & - $bs \,@\, [Z]$ + $bs \,@\, [S]$ \end{tabular} \end{center} \noindent @@ -606,8 +606,8 @@ $\textit{let}\,(v_1, bs_1) = \textit{decode}'\,bs\,r_1\;\textit{in}$\\ & & $\textit{let}\,(v_2, bs_2) = \textit{decode}'\,bs_1\,r_2$\\ & & \hspace{35mm}$\textit{in}\;(\Seq\,v_1\,v_2, bs_2)$\\ - $\textit{decode}'\,(Z\!::\!bs)\,(r^*)$ & $\dn$ & $(\Stars\,[], bs)$\\ - $\textit{decode}'\,(S\!::\!bs)\,(r^*)$ & $\dn$ & + $\textit{decode}'\,(S\!::\!bs)\,(r^*)$ & $\dn$ & $(\Stars\,[], bs)$\\ + $\textit{decode}'\,(Z\!::\!bs)\,(r^*)$ & $\dn$ & $\textit{let}\,(v, bs_1) = \textit{decode}'\,bs\,r\;\textit{in}$\\ & & $\textit{let}\,(\Stars\,vs, bs_2) = \textit{decode}'\,bs_1\,r^*$\\ & & \hspace{35mm}$\textit{in}\;(\Stars\,v\!::\!vs, bs_2)$\bigskip\\ @@ -1148,10 +1148,10 @@ $\dn$ & $\textit{bs}\; @\; (\retrieve \; (_{[]}\Sigma \textit{as}) \; v)$\\ $\retrieve \; \, _{bs} a^* $ & $ (\Stars \; (v :: vs)) $ & $\dn$ & - $\textit{bs}\; @\; (\retrieve \; a \; v)\; @ \; + $\textit{bs}\; @\; [Z] \; @ \; (\retrieve \; a \; v)\; @ \; (\retrieve \; (_{[]} a^*) \; (\Stars \; vs) )$\\ - $\retrieve \; \, _{bs} a^* $ & $ (\Stars \; []) $ & $\dn$ & $\textit{bs} \; @ \; [Z]$ + $\retrieve \; \, _{bs} a^* $ & $ (\Stars \; []) $ & $\dn$ & $\textit{bs} \; @ \; [S]$ \end{tabular} \end{center} \noindent