566 & &$\textit{then}\;bs\,@\,\textit{bmkeps}\,a$\\ |
566 & &$\textit{then}\;bs\,@\,\textit{bmkeps}\,a$\\ |
567 & &$\textit{else}\;bs\,@\,\textit{bmkeps}\,(_{[]}\sum \textit{as})$\\ |
567 & &$\textit{else}\;bs\,@\,\textit{bmkeps}\,(_{[]}\sum \textit{as})$\\ |
568 $\textit{bmkeps}\,(_{bs} a_1 \cdot a_2)$ & $\dn$ & |
568 $\textit{bmkeps}\,(_{bs} a_1 \cdot a_2)$ & $\dn$ & |
569 $bs \,@\,\textit{bmkeps}\,a_1\,@\, \textit{bmkeps}\,a_2$\\ |
569 $bs \,@\,\textit{bmkeps}\,a_1\,@\, \textit{bmkeps}\,a_2$\\ |
570 $\textit{bmkeps}\,(_{bs}a^*)$ & $\dn$ & |
570 $\textit{bmkeps}\,(_{bs}a^*)$ & $\dn$ & |
571 $bs \,@\, [Z]$ |
571 $bs \,@\, [S]$ |
572 \end{tabular} |
572 \end{tabular} |
573 \end{center} |
573 \end{center} |
574 \noindent |
574 \noindent |
575 $\bmkeps$, just like $\mkeps$, |
575 $\bmkeps$, just like $\mkeps$, |
576 visits a regular expression tree respecting |
576 visits a regular expression tree respecting |
604 (\Right\,v, bs_1)$\\ |
604 (\Right\,v, bs_1)$\\ |
605 $\textit{decode}'\,bs\;(r_1\cdot r_2)$ & $\dn$ & |
605 $\textit{decode}'\,bs\;(r_1\cdot r_2)$ & $\dn$ & |
606 $\textit{let}\,(v_1, bs_1) = \textit{decode}'\,bs\,r_1\;\textit{in}$\\ |
606 $\textit{let}\,(v_1, bs_1) = \textit{decode}'\,bs\,r_1\;\textit{in}$\\ |
607 & & $\textit{let}\,(v_2, bs_2) = \textit{decode}'\,bs_1\,r_2$\\ |
607 & & $\textit{let}\,(v_2, bs_2) = \textit{decode}'\,bs_1\,r_2$\\ |
608 & & \hspace{35mm}$\textit{in}\;(\Seq\,v_1\,v_2, bs_2)$\\ |
608 & & \hspace{35mm}$\textit{in}\;(\Seq\,v_1\,v_2, bs_2)$\\ |
609 $\textit{decode}'\,(Z\!::\!bs)\,(r^*)$ & $\dn$ & $(\Stars\,[], bs)$\\ |
609 $\textit{decode}'\,(S\!::\!bs)\,(r^*)$ & $\dn$ & $(\Stars\,[], bs)$\\ |
610 $\textit{decode}'\,(S\!::\!bs)\,(r^*)$ & $\dn$ & |
610 $\textit{decode}'\,(Z\!::\!bs)\,(r^*)$ & $\dn$ & |
611 $\textit{let}\,(v, bs_1) = \textit{decode}'\,bs\,r\;\textit{in}$\\ |
611 $\textit{let}\,(v, bs_1) = \textit{decode}'\,bs\,r\;\textit{in}$\\ |
612 & & $\textit{let}\,(\Stars\,vs, bs_2) = \textit{decode}'\,bs_1\,r^*$\\ |
612 & & $\textit{let}\,(\Stars\,vs, bs_2) = \textit{decode}'\,bs_1\,r^*$\\ |
613 & & \hspace{35mm}$\textit{in}\;(\Stars\,v\!::\!vs, bs_2)$\bigskip\\ |
613 & & \hspace{35mm}$\textit{in}\;(\Stars\,v\!::\!vs, bs_2)$\bigskip\\ |
614 |
614 |
615 $\textit{decode}\,bs\,r$ & $\dn$ & |
615 $\textit{decode}\,bs\,r$ & $\dn$ & |
1146 |
1146 |
1147 $\retrieve \; \, _{bs} \Sigma (a :: \textit{as})$ & $ (\Right \; v) $ & |
1147 $\retrieve \; \, _{bs} \Sigma (a :: \textit{as})$ & $ (\Right \; v) $ & |
1148 $\dn$ & $\textit{bs}\; @\; (\retrieve \; (_{[]}\Sigma \textit{as}) \; v)$\\ |
1148 $\dn$ & $\textit{bs}\; @\; (\retrieve \; (_{[]}\Sigma \textit{as}) \; v)$\\ |
1149 |
1149 |
1150 $\retrieve \; \, _{bs} a^* $ & $ (\Stars \; (v :: vs)) $ & $\dn$ & |
1150 $\retrieve \; \, _{bs} a^* $ & $ (\Stars \; (v :: vs)) $ & $\dn$ & |
1151 $\textit{bs}\; @\; (\retrieve \; a \; v)\; @ \; |
1151 $\textit{bs}\; @\; [Z] \; @ \; (\retrieve \; a \; v)\; @ \; |
1152 (\retrieve \; (_{[]} a^*) \; (\Stars \; vs) )$\\ |
1152 (\retrieve \; (_{[]} a^*) \; (\Stars \; vs) )$\\ |
1153 |
1153 |
1154 $\retrieve \; \, _{bs} a^* $ & $ (\Stars \; []) $ & $\dn$ & $\textit{bs} \; @ \; [Z]$ |
1154 $\retrieve \; \, _{bs} a^* $ & $ (\Stars \; []) $ & $\dn$ & $\textit{bs} \; @ \; [S]$ |
1155 \end{tabular} |
1155 \end{tabular} |
1156 \end{center} |
1156 \end{center} |
1157 \noindent |
1157 \noindent |
1158 As promised, $\retrieve$ collects the right bit-codes from the |
1158 As promised, $\retrieve$ collects the right bit-codes from the |
1159 final derivative $a_n$, guided by $v_n$: |
1159 final derivative $a_n$, guided by $v_n$: |