1568 $\textit{if} \models v:r \; \textit{then} \; \rup \gg \textit{code}(v)$

  1568 \begin{center}

  1569 \begin{equation}\label{contains1}

  1570 \textit{if}\; \models v:r \; \textit{then} \; \rup \gg \textit{code}(v)

  1571 \end{equation}

  1572 \end{center}

  1573 This lemma states that the set

  1574 $\{\textit{bs}\; | \rup \gg \textit{bs} \}$ 

  1575 "contains" all the underlying value $v$ of $r$ in which they are 

  1576 in a coded form.

  1577 These values include the ones created in the 

  1578 lexing process, for example, when the regular

  1579 expression $r$ is nullable, then we have:

  1580 \item

  1581 \begin{center}

  1582 $r \gg \textit{bmkeps}(r)$

  1583 \end{center}

  1584 This can be seen as a corollary of the previous lemma,

  1585 because $\models \textit{mkeps}((r\downarrow)):(r\downarrow)$

  1586 and $\textit{code}(\mkeps((r\downarrow))) = \bmkeps(r)$.

  1587 Another corollary we have of \eqref{contains1}

  1588 \item

  1589 \begin{center}

  1590 $\textit{if}\; \models v:r \; \textit{then} \; \rup \gg \textit{retrieve} \; \rup \; v$

  1591 \end{center}

  1592 as $\textit{retrieve} \; \rup \; v = \textit{code}(v)$

  1593 It says that if you can extract a bitsequence using 

  1594 retrieve guided by $v$, then such bitsequence is already there in the set 

  1595 $\{\textit{bs}\; | \rup \gg \textit{bs} \}$.

  1596 This lemma has a slightly different form:

  1597 \item

  1598 \begin{center}

  1599 $\textit{if}\; \models v:a\downarrow \; \textit{then} \; a \gg \textit{retrieve} \; a \; v$

  1600 \end{center}

  1601 This is almost identical to the previous lemma, except

  1602 this time we might have arbitrary bits attached 

  1603 to anywhere of the annotated regular expression $a$.

  1604 $a$ can be any "made up" annotated regular expressions

  1605 that does not belong to the "natural" ones created by 

  1606 internalising an unannotated regular expression.

  1607 For example, a regular expression $r = (a+b)$ after internalisation

  1608 becomes $\rup = (_0a+_1b)$. For an underlying value $v = \Left(\Char(a))$

  1609 we have $\retrieve \; (_0a+_1b) \;v = 0$ and $(_0a+_1b) \gg 0$. We could 

  1610 attach arbitrary bits to the regular expression $\rup$

  1611 without breaking the structure,

  1612  for example  we could make up $a = _{0100111}(_{1011}a+1b)$,

  1613  and we still have $\models v:a\downarrow$, and

  1614  therefore  $a \gg \retrieve \; a \; v$, this time the bitsequence

  1615  being $01001111011$.

  1616 This shows that the inductive clauses defining $\gg$

  1617 simulates what $\retrieve$ does guided by different 

  1618 values.

  1619 Set $\{\textit{bs}\; | \rup \gg \textit{bs} \}$ contains

  1620 a wide range of values coded as bitsequences,

  1621 the following property can be routinely established 

  1622 from the previous lemma

  1623 \item

  1624 \begin{center}

  1625 $r \gg \retrieve \; r \; (\inj \; (r\downarrow) \; c \; v) \;\;\; \textit{if} \; \models v: \textit{der} \; c \; (\erase(r))$

  1626 \end{center}

  1627 because $\inj \; (r\downarrow)\; c\; v$ is a value

  1628 underlying $r$.

  1629 Using this we can get something that looks much

  1630 less obvious:

  1631 \item

  1632 

  1633 \begin{center}

  1634 \begin{tabular}{c}

  1635 $\textit{if} \models v: \erase(r)\backslash c \; \textit{then}$\\

  1636 $r\backslash c \gg \retrieve \; r \; (\inj \; (r\downarrow) \; c \; v) \; \textit{and}$\\

  1637 $r \gg \retrieve \; r \; (\inj \; (r\downarrow) \; c \; v)$\\

  1638 \end{tabular}

  1639 \end{center}

  1640 It says that the derivative operation $\backslash c$ is basically

  1641 an operation that does not change the bits an annotated regular

  1642 expression is able to produce, both

  1643 $r\backslash c$ and $r$ can produce 

  1644 the bitsequence $\inj \; (r\downarrow) \; c \;v)$.

  1645 This invariance with respect to derivative can be

  1646 further extended to a more surprising property:

  1647 \item

  1648 \begin{center}

  1649 \begin{tabular}{c}

  1650 $\textit{if} \models v: \erase(r) \backslash s$\\

  1651 $r\backslash s \gg \retrieve \; r \; (\flex \; (r\downarrow) \; \textit{id} \; s \; v) \; \textit{and}$\\

  1652 $r \gg \retrieve \; r \; (r\downarrow) \; \textit{id} \; s \; v) \; c \; v)$\\

  1653 \end{tabular}

  1654 \end{center}

  1655 Here $\gg$ is almost like an $\textit{NFA}$ in the sense that 

  1656 it simulates the lexing process with respect to different strings.