diff -r dfcf3fa58d7f -r c8ef391dd6f7 twtsevms/twtsevms.tex
--- a/twtsevms/twtsevms.tex	Wed Mar 04 13:25:52 2020 +0000
+++ b/twtsevms/twtsevms.tex	Fri Apr 10 11:58:11 2020 +0100
@@ -1,13 +1,12 @@
 \documentclass[a4paper,UKenglish]{lipics}
+\usepackage{data}
 \usepackage{graphic}
-\usepackage{data}
 \usepackage{tikz-cd}
 \usepackage{tikz}
 
 %\usetikzlibrary{graphs}
 %\usetikzlibrary{graphdrawing}
 %\usegdlibrary{trees}
-
 %\usepackage{algorithm}
 \usepackage{amsmath}
 \usepackage{xcolor}
@@ -15,7 +14,7 @@
 \usepackage{enumitem}
 \usepackage{nccmath}
 \usepackage{soul}
-
+%works?
 \definecolor{darkblue}{rgb}{0,0,0.6}
 \hypersetup{colorlinks=true,allcolors=darkblue}
 \newcommand{\comment}[1]%
@@ -102,30 +101,38 @@
 If we let the alphabet
 where $c$ is selected from
 be $\sum = \{0,1\}$,
-then bitcodes can be defined in a 
-regular expression style:
+then we can define the regular expression 
+style bitcodes:
 
 
-\[			 bs ::=   \ZERO \mid  \ONE
+\[			 rbs ::=   \ZERO \mid  \ONE
 			 \mid  1
 			 \mid  0  
-			 \mid  bs_1 \cdot bs_2
-			 \mid  \sum{bs_{list}}
-			 \mid bs^*         
+			 \mid  rbs_1 \cdot rbs_2
+			 \mid  \sum{rbs_{list}}
+			 \mid rbs^*         
 \]
 
-We can define an isomorphism between the regex
-definition of bitcodes and our list definition of bitcodes:
+This is our list definition of bitcodes:
+\begin{center}
+$b ::=   1 \mid  0 \qquad
+bs ::= [] \mid b::bs    $
+\end{center}
+
+Define an isomorphism between bitcodes based on lists
+and bitcodes based on regular expressions:
 \begin{center}
-		$b ::=   1 \mid  0 \qquad
-bs ::= [] \mid b::bs    
-$
+\begin{tabular}{lcl}
+$\sigma: bit \; list$ & $\Rightarrow$ & $bit \; regex$\\
+$\delta: bit$ & $\Rightarrow$ & $bit \; regex$\\
+$\sigma([])$ & $=$ & $ \ONE$\\
+$\sigma(b::bs)$ & $=$ & $\delta(b) \cdot \sigma(bs)$\\
+$\delta(b) $ & $=$ & $b\; as \;a \;regex$
+\end{tabular}
 \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:
+grammar using the  list definition of $bs$ :
 
 \begin{center}
 \begin{tabular}{lcl}
@@ -137,23 +144,75 @@
                   & $\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:
+%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{annotated}\; \textit{regex} \Rightarrow \textit{bit}\; \textit{regex}$ 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(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) $
+\begin{tabular}{lcl}
+$f(\ZERO)$ & $=$ & $\ZERO$\\
+$f(_{bs}\ONE)$ & $=$ & $\sigma(\textit{bs})$\\
+$f(_{bs}a)$ & $=$ & $\sigma(\textit{bs}) $\\
+$f(_{bs}r_1\cdot r_2)$ & $=$ & $\sigma(\textit{bs}) \cdot( f(r_1) \cdot f(r_2))$\\
+$f(_{bs}\sum{rs})$ & $=$ & $\sigma(\textit{bs}) \cdot \sum\limits_{r \in rs}{f(\textit{r})}$\\
+$f(_{bs}r^*)$ & $=$ & $\sigma(\textit{bs}) \cdot((0 \cdot f(r))^*\cdot 1) $
+\end{tabular}
+\end{center}
+
+Now define function $L: bit\;regex \Rightarrow set \; bs$ as follows:
+\begin{center}
+\begin{tabular}{lcl}
+$L(\ZERO)$ & $=$ & $\emptyset$\\
+$L(\ONE) $ & $= $ & $\{[]\}$\\
+$L(b\;as \; a\;regex) $ & $=$ & $\{b\; as \; a \; bit\}$\\
+$L(bs_1 \cdot bs_2)$ & $=$ & $L(bs_1) \times L(bs_2)$\\
+$L(\sum bss) $ & $=$ &$\bigcup\limits_{bs \in bss}{L(bs)}$\\
+$L(bs^*)$ & $= $ & $\bigcup\limits_{0 \leq n}{(L(bs))^n}$
+\end{tabular}
 \end{center}
 
 We claim that:
 \begin{center}
-$f(a) = \{bs \mid a \gg bs\}$.
+$L(f(a) )= \{bs \mid a \gg bs\}$.
 \end{center}
 
+where contains is defined this way:
+\begin{center}
+\begin{tabular}{llclll}
+& & & $_{bs}\ONE$ & $\gg$ & $\textit{bs}$\\
+& & & $_{bs}{\bf c}$ & $\gg$ & $\textit{bs}$\\
+$\textit{if} \; r_1 \gg \textit{bs}_1$ & $r_2 \; \gg \textit{bs}_2$
+& $\textit{then}$  &
+ $_{bs}{r_1 \cdot r_2}$ &
+ $\gg$ &
+ $\textit{bs} @ \textit{bs}_1 @ \textit{bs}_2$\\
+
+ $\textit{if} \; r \gg \textit{bs}_1$ &  & $\textit{then}$  &
+ $_{bs}{\sum(r :: \textit{rs}})$ &
+ $\gg$ &
+ $\textit{bs} @ \textit{bs}_1 $\\
+
+ $\textit{if} \; _{bs}(\sum \textit{rs}) \gg \textit{bs} @ \textit{bs}_1$ &  & $\textit{then}$  &
+ $_{bs}{\sum(r :: \textit{rs}})$ &
+ $\gg$ &
+ $\textit{bs} @ \textit{bs}_1 $\\
+
+ $\textit{if} \; r \gg \textit{bs}_1\; \textit{and}$ &  $_{bs}r^* \gg \textit{bs} @ \textit{bs}_2$ & $\textit{then}$  &
+ $_{bs}r^* $ &
+ $\gg$ &
+ $\textit{bs} @ [0] @ \textit{bs}_1@ \textit{bs}_2 $\\
+
+ & & & $_{bs}r^*$ & $\gg$ & $\textit{bs} @ [1]$\\
+\end{tabular}
+\end{center}
+
+Moreover, we claim the fact that
+\begin{center}
+	$L(f(a^*)) != L(f(a^* \backslash a))$
+\end{center}
+This is by $\exists bs \in f(a^*), s.t. bs \notin f(a^* \backslash a)$.
+Proof for the fact
+$L(f(a) )= \{bs \mid a \gg bs\}$:
+
 \bibliographystyle{plain}
 \bibliography{root}