1233 	We do an induction on $r$, generalising over $v$.

  1233 	We do an induction on $r$, generalising over $v$.

  1234 	The induction principle in our formalisation

  1234 	The induction principle in our formalisation

  1235 	is function $\erase$'s cases.

  1235 	is function $\erase$'s cases.

  1236 \end{proof}

  1236 \end{proof}

  1237 \noindent

  1237 \noindent

  1238 Before we move on to the next

  1244 Before we move on to the next

  1239 helper function, we rewrite $\blexer$ in

  1245 helper function, we rewrite $\blexer$ in

  1240 the following way which makes later proofs more convenient:

  1246 the following way which makes later proofs more convenient:

  1241 \begin{lemma}\label{blexer_retrieve}

  1247 \begin{lemma}\label{blexer_retrieve}

  1242 $\blexer \; r \; s = \decode  \; (\retrieve \; (\internalise \; r) \; (\mkeps \; (r \backslash s) )) \; r$

  1248 $\blexer \; r \; s = \decode  \; (\retrieve \; (\internalise \; r) \; (\mkeps \; (r \backslash s) )) \; r$

  1338 \].

  1344 \].

  1339 \end{proof}

  1345 \end{proof}

  1340 \noindent

  1346 \noindent

  1341 With this pivotal lemma we can now link $\flex$ and $\blexer$

  1347 With this pivotal lemma we can now link $\flex$ and $\blexer$

  1342 and finally give the correctness of $\blexer$--it outputs the same result as $\lexer$:

  1348 and finally give the correctness of $\blexer$--it outputs the same result as $\lexer$:

  1344 	$\blexer\; r \; s = \lexer \; r \; s$

  1350 	$\blexer\; r \; s = \lexer \; r \; s$

  1345 \end{theorem}

  1351 \end{theorem}

  1346 \begin{proof}

  1352 \begin{proof}

  1347 	From \ref{flex_retrieve} we have that 

  1353 	From \ref{flex_retrieve} we have that 

  1348 	$\textit{flex} \; r \; \textit{id} \; s \; \mkeps(r \backslash s)  = \blexer \; r \; s$,

  1354 	$\textit{flex} \; r \; \textit{id} \; s \; \mkeps(r \backslash s)  = \blexer \; r \; s$,