670   is just an abbreviation for \mbox{@{text "ALTs bs [r\<^sub>1, r\<^sub>2]"}}. 

   670   is just an abbreviation for \mbox{@{text "ALTs bs [r\<^sub>1, r\<^sub>2]"}}. 

   671   For bitsequences we use lists made up of the

   671   For bitsequences we use lists made up of the

   672   constants @{text Z} and @{text S}.  The idea with bitcoded regular

   672   constants @{text Z} and @{text S}.  The idea with bitcoded regular

   673   expressions is to incrementally generate the value information (for

   673   expressions is to incrementally generate the value information (for

   674   example @{text Left} and @{text Right}) as bitsequences. For this 

   674   example @{text Left} and @{text Right}) as bitsequences. For this 

   676   function for how values can be coded into bitsequences.

   677   function for how values can be coded into bitsequences.

   677 

   678 

   678   \begin{center}

   679   \begin{center}

   679   \begin{tabular}{cc}

   680   \begin{tabular}{cc}

   680   \begin{tabular}{lcl}

   681   \begin{tabular}{lcl}

   706   then we can always decode the value accurately (see Fig.~\ref{decode}).

   707   then we can always decode the value accurately (see Fig.~\ref{decode}).

   707   The function \textit{decode} checks whether all of the bitsequence is

   708   The function \textit{decode} checks whether all of the bitsequence is

   708   consumed and returns the corresponding value as @{term "Some v"}; otherwise

   709   consumed and returns the corresponding value as @{term "Some v"}; otherwise

   709   it fails with @{text "None"}. We can establish that for a value $v$

   710   it fails with @{text "None"}. We can establish that for a value $v$

   710   inhabited by a regular expression $r$, the decoding of its

   711   inhabited by a regular expression $r$, the decoding of its

   712 

   713 

   713   %The decoding can be

   714   %The decoding can be

   714   %defined by using two functions called $\textit{decode}'$ and

   715   %defined by using two functions called $\textit{decode}'$ and

   715   %\textit{decode}:

   716   %\textit{decode}:

   716 

   717