391 \end{center}

   391 \end{center}

   392 

   392 

   393 \noindent

   393 \noindent

   394 This algorithm keeps the regular expression size small, for example,

   394 This algorithm keeps the regular expression size small, for example,

   395 with this simplification our previous $(a + aa)^*$ example's 8000 nodes

   395 with this simplification our previous $(a + aa)^*$ example's 8000 nodes

   397 input string is.

   397 input string is.

   398 

   398 

   399 

   399 

   400 

   400 

   401 

   401 

   425 \section{Correctness of Bit-coded Algorithm (Without Simplification)}

   425 \section{Correctness of Bit-coded Algorithm (Without Simplification)}

   426 We now give the proof the correctness of the algorithm with bit-codes.

   426 We now give the proof the correctness of the algorithm with bit-codes.

   427 

   427 

   428 Ausaf and Urban cleverly defined an auxiliary function called $\flex$,

   428 Ausaf and Urban cleverly defined an auxiliary function called $\flex$,

   429 defined as

   429 defined as

   434 which accumulates the characters that needs to be injected back, 

   436 which accumulates the characters that needs to be injected back, 

   435 and does the injection in a stack-like manner (last taken derivative first injected).

   437 and does the injection in a stack-like manner (last taken derivative first injected).

   436 $\flex$ is connected to the $\lexer$:

   438 $\flex$ is connected to the $\lexer$:

   437 \begin{lemma}

   439 \begin{lemma}

   438 $\flex \; r \; \textit{id}\; s \; \mkeps (r\backslash s) = \lexer \; r \; s$

   440 $\flex \; r \; \textit{id}\; s \; \mkeps (r\backslash s) = \lexer \; r \; s$