--- a/twtsevms/twtsevms.tex	Wed Mar 04 13:00:59 2020 +0000
+++ b/twtsevms/twtsevms.tex	Wed Mar 04 13:25:52 2020 +0000
@@ -89,18 +89,70 @@
 \begin{document}
 
 \maketitle
+Suppose (basic) regular expressions are given by the following grammar:
 
-Hello.
-Let us play with the function $f$ on annotated regular expressions:
+\[			r ::=   \ZERO \mid  \ONE
+			 \mid  c  
+			 \mid  r_1 \cdot r_2
+			 \mid  r_1 + r_2   
+			 \mid r^*         
+\]
+
+
+If we let the alphabet
+where $c$ is selected from
+be $\sum = \{0,1\}$,
+then bitcodes can be defined in a 
+regular expression style:
+
+
+\[			 bs ::=   \ZERO \mid  \ONE
+			 \mid  1
+			 \mid  0  
+			 \mid  bs_1 \cdot bs_2
+			 \mid  \sum{bs_{list}}
+			 \mid bs^*         
+\]
+
+We can define an isomorphism between the regex
+definition of bitcodes and our list definition of bitcodes:
 \begin{center}
-$f(\ZERO) = \ZERO$
+		$b ::=   1 \mid  0 \qquad
+bs ::= [] \mid b::bs    
+$
+\end{center}
+For example we can let $\sigma([])= \ONE$.
+But how to define such isomorphism in detail is not explicitly needed for now.
+
+\emph{Annotated regular expressions} can be defined by the following
+grammar using new $bs$ definition:
+
+\begin{center}
+\begin{tabular}{lcl}
+  $\textit{a}$ & $::=$  & $\ZERO$\\
+                  & $\mid$ & $_{bs}\ONE$\\
+                  & $\mid$ & $_{bs}{\bf c}$\\
+                  & $\mid$ & $_{bs}\sum\,as$\\
+                  & $\mid$ & $_{bs}a_1\cdot a_2$\\
+                  & $\mid$ & $_{bs}a^*$
+\end{tabular}    
+\end{center}  
+Let the set of all bitcoded regular expressions be $\textit{BS}$.
+Let the set of all annotated regular expression be $\textit{AR}$.
+Let us play with the function $f: \textit{AR} \rightarrow \textit{BS}$ on annotated regular expressions:
+\begin{center}
+$f(\ZERO) = \ZERO$\\
 $f(_{bs}\ONE) = \textit{bs}$\\
 $f(_{bs}a) = \textit{bs} $\\
-$f(_{bs}r_1\cdot r_2) = \textit{bs} \cdot $
+$f(_{bs}r_1\cdot r_2) = \textit{bs} \cdot( f(r_1) \cdot f(r_2))$\\
 $f(_{bs}\sum{rs}) = \textit{bs} \cdot \sum\limits_{r \in rs}{f(\textit{r})}$\\
-$f(_{bs}r*) = \textit{bs} \cdot((0 \cdot f(r))\cdot 1) $
+$f(_{bs}r^*) = \textit{bs} \cdot((0 \cdot f(r))^*\cdot 1) $
 \end{center}
 
+We claim that:
+\begin{center}
+$f(a) = \{bs \mid a \gg bs\}$.
+\end{center}
 
 \bibliographystyle{plain}
 \bibliography{root}