# HG changeset patch
# User Chengsong
# Date 1635882172 0
# Node ID 78cc255e286fac1702c5f01f4375ea18f4d88871
# Parent  f65444d29e74de48cd9b2366a430a0f789d4f23d
some more writing

diff -r f65444d29e74 -r 78cc255e286f thys2/Journal/Paper.tex
--- a/thys2/Journal/Paper.tex	Tue Nov 02 13:57:59 2021 +0000
+++ b/thys2/Journal/Paper.tex	Tue Nov 02 19:42:52 2021 +0000
@@ -59,9 +59,9 @@
 \endisadelimdocument
 %
 \begin{isamarkuptext}%
-This works builds on previous work by Ausaf and Urban using 
+This paper builds on previous work by Ausaf and Urban using 
 regular expression'd bit-coded derivatives to do lexing that 
-is both fast and satisfied the POSIX specification.
+is both fast and satisfies the POSIX specification.
 In their work, a bit-coded algorithm introduced by Sulzmann and Lu
 was formally verified in Isabelle, by a very clever use of
 flex function and retrieve to carefully mimic the way a value is 
@@ -81,45 +81,15 @@
 
 However what is not certain is whether we can add simplification
 to the bit-coded algorithm, without breaking the correct lexing output.
-This might sound trivial in the case of producing a YES/NO answer,
-but once we require a lexing output to be produced (which is required
-in applications like compiler front-end, malicious attack domain extraction, 
-etc.), it is not straightforward if we still extract what is needed according
-to the POSIX standard.
-
-By simplification, we mean specifically the following rules:
-
-\begin{center}
-  \begin{tabular}{lcl}
-  \isa{\mbox{}\inferrule{\mbox{}}{\mbox{ASEQ\ bs\ AZERO\ r\isactrlsub {\isadigit{2}}\ {\isasymleadsto}\ AZERO}}}\\
-  \isa{\mbox{}\inferrule{\mbox{}}{\mbox{ASEQ\ bs\ r\isactrlsub {\isadigit{1}}\ AZERO\ {\isasymleadsto}\ AZERO}}}\\
-  \isa{\mbox{}\inferrule{\mbox{}}{\mbox{ASEQ\ bs\ {\isacharparenleft}{\kern0pt}AONE\ bs\isactrlsub {\isadigit{1}}{\isacharparenright}{\kern0pt}\ r\isactrlsub {\isadigit{1}}\ {\isasymleadsto}\ fuse\ {\isacharparenleft}{\kern0pt}bs\ {\isacharat}{\kern0pt}\ bs\isactrlsub {\isadigit{1}}{\isacharparenright}{\kern0pt}\ r\isactrlsub {\isadigit{1}}}}}\\
-  \isa{\mbox{}\inferrule{\mbox{bs\ {\isasymleadsto}\ r\isactrlsub {\isadigit{1}}}}{\mbox{ASEQ\ bs\ bs\ r{\isadigit{3}}{\isachardot}{\kern0pt}{\isadigit{0}}\ {\isasymleadsto}\ ASEQ\ bs\ r\isactrlsub {\isadigit{1}}\ r{\isadigit{3}}{\isachardot}{\kern0pt}{\isadigit{0}}}}}\\
-  \isa{\mbox{}\inferrule{\mbox{bs\ {\isasymleadsto}\ r\isactrlsub {\isadigit{2}}}}{\mbox{ASEQ\ bs\ r{\isadigit{1}}{\isachardot}{\kern0pt}{\isadigit{0}}\ bs\ {\isasymleadsto}\ ASEQ\ bs\ r{\isadigit{1}}{\isachardot}{\kern0pt}{\isadigit{0}}\ r\isactrlsub {\isadigit{2}}}}}\\
-  \isa{\mbox{}\inferrule{\mbox{bs\ {\isasymleadsto}\ r\isactrlsub {\isadigit{1}}}}{\mbox{AALTs\ bs\ {\isacharparenleft}{\kern0pt}rs{\isadigit{1}}{\isachardot}{\kern0pt}{\isadigit{0}}\ {\isacharat}{\kern0pt}\ {\isacharbrackleft}{\kern0pt}bs{\isacharbrackright}{\kern0pt}\ {\isacharat}{\kern0pt}\ rs{\isadigit{2}}{\isachardot}{\kern0pt}{\isadigit{0}}{\isacharparenright}{\kern0pt}\ {\isasymleadsto}\ AALTs\ bs\ {\isacharparenleft}{\kern0pt}rs{\isadigit{1}}{\isachardot}{\kern0pt}{\isadigit{0}}\ {\isacharat}{\kern0pt}\ {\isacharbrackleft}{\kern0pt}r\isactrlsub {\isadigit{1}}{\isacharbrackright}{\kern0pt}\ {\isacharat}{\kern0pt}\ rs{\isadigit{2}}{\isachardot}{\kern0pt}{\isadigit{0}}{\isacharparenright}{\kern0pt}}}}\\
-  \isa{\mbox{}\inferrule{\mbox{}}{\mbox{AALTs\ bs\ {\isacharparenleft}{\kern0pt}r\isactrlsub {\isadigit{2}}\ {\isacharat}{\kern0pt}\ AZERO\mbox{$\,$}{\isacharcolon}{\kern0pt}{\isacharcolon}{\kern0pt}\mbox{$\,$}rsb{\isacharparenright}{\kern0pt}\ {\isasymleadsto}\ AALTs\ bs\ {\isacharparenleft}{\kern0pt}r\isactrlsub {\isadigit{2}}\ {\isacharat}{\kern0pt}\ rsb{\isacharparenright}{\kern0pt}}}}\\
-  \isa{\mbox{}\inferrule{\mbox{}}{\mbox{AALTs\ bs\ {\isacharparenleft}{\kern0pt}r\isactrlsub {\isadigit{1}}\ {\isacharat}{\kern0pt}\ AALTs\ bs{\isadigit{1}}{\isachardot}{\kern0pt}{\isadigit{0}}\ rs{\isadigit{1}}{\isachardot}{\kern0pt}{\isadigit{0}}\mbox{$\,$}{\isacharcolon}{\kern0pt}{\isacharcolon}{\kern0pt}\mbox{$\,$}rsb{\isacharparenright}{\kern0pt}\ {\isasymleadsto}\ AALTs\ bs\ {\isacharparenleft}{\kern0pt}r\isactrlsub {\isadigit{1}}\ {\isacharat}{\kern0pt}\ map\ {\isacharparenleft}{\kern0pt}fuse\ bs{\isadigit{1}}{\isachardot}{\kern0pt}{\isadigit{0}}{\isacharparenright}{\kern0pt}\ rs{\isadigit{1}}{\isachardot}{\kern0pt}{\isadigit{0}}\ {\isacharat}{\kern0pt}\ rsb{\isacharparenright}{\kern0pt}}}}\\
-  \isa{\mbox{}\inferrule{\mbox{}}{\mbox{AALTs\ bs\ {\isacharparenleft}{\kern0pt}map\ {\isacharparenleft}{\kern0pt}fuse\ r\isactrlsub {\isadigit{2}}{\isacharparenright}{\kern0pt}\ rs{\isacharparenright}{\kern0pt}\ {\isasymleadsto}\ AALTs\ {\isacharparenleft}{\kern0pt}bs\ {\isacharat}{\kern0pt}\ r\isactrlsub {\isadigit{2}}{\isacharparenright}{\kern0pt}\ rs}}}\\
-  \isa{\mbox{}\inferrule{\mbox{}}{\mbox{AALTs\ {\isacharparenleft}{\kern0pt}bs\ {\isacharat}{\kern0pt}\ r\isactrlsub {\isadigit{1}}{\isacharparenright}{\kern0pt}\ rs\ {\isasymleadsto}\ AALTs\ bs\ {\isacharparenleft}{\kern0pt}map\ {\isacharparenleft}{\kern0pt}fuse\ r\isactrlsub {\isadigit{1}}{\isacharparenright}{\kern0pt}\ rs{\isacharparenright}{\kern0pt}}}}\\
-  \isa{\mbox{}\inferrule{\mbox{}}{\mbox{AALTs\ bs\ {\isacharbrackleft}{\kern0pt}{\isacharbrackright}{\kern0pt}\ {\isasymleadsto}\ AZERO}}}\\
-  \isa{\mbox{}\inferrule{\mbox{}}{\mbox{AALTs\ bs\ {\isacharbrackleft}{\kern0pt}r\isactrlsub {\isadigit{1}}{\isacharbrackright}{\kern0pt}\ {\isasymleadsto}\ fuse\ bs\ r\isactrlsub {\isadigit{1}}}}}\\
-  \isa{\mbox{}\inferrule{\mbox{bs\mbox{$^\downarrow$}\ {\isacharequal}{\kern0pt}\ r\isactrlsub {\isadigit{2}}\mbox{$^\downarrow$}}}{\mbox{AALTs\ bs\ {\isacharparenleft}{\kern0pt}rsa\ {\isacharat}{\kern0pt}\ {\isacharbrackleft}{\kern0pt}bs{\isacharbrackright}{\kern0pt}\ {\isacharat}{\kern0pt}\ rsb\ {\isacharat}{\kern0pt}\ {\isacharbrackleft}{\kern0pt}r\isactrlsub {\isadigit{2}}{\isacharbrackright}{\kern0pt}\ {\isacharat}{\kern0pt}\ rsc{\isacharparenright}{\kern0pt}\ {\isasymleadsto}\ AALTs\ bs\ {\isacharparenleft}{\kern0pt}rsa\ {\isacharat}{\kern0pt}\ {\isacharbrackleft}{\kern0pt}bs{\isacharbrackright}{\kern0pt}\ {\isacharat}{\kern0pt}\ rsb\ {\isacharat}{\kern0pt}\ rsc{\isacharparenright}{\kern0pt}}}}\\
 
 
-  \isa{\mbox{}\inferrule{\mbox{}}{\mbox{Empty\ {\isacharcolon}{\kern0pt}\ \isactrlbold {\isadigit{1}}}}} & 
-  \isa{\mbox{}\inferrule{\mbox{}}{\mbox{Char\ c\ {\isacharcolon}{\kern0pt}\ c}}}\\[4mm]
-  \isa{\mbox{}\inferrule{\mbox{v\isactrlsub {\isadigit{1}}\ {\isacharcolon}{\kern0pt}\ r\isactrlsub {\isadigit{1}}}}{\mbox{Left\ v\isactrlsub {\isadigit{1}}\ {\isacharcolon}{\kern0pt}\ r\isactrlsub {\isadigit{1}}\ {\isacharplus}{\kern0pt}\ r\isactrlsub {\isadigit{2}}}}} &
-  \isa{\mbox{}\inferrule{\mbox{v\isactrlsub {\isadigit{2}}\ {\isacharcolon}{\kern0pt}\ r\isactrlsub {\isadigit{1}}}}{\mbox{Right\ v\isactrlsub {\isadigit{2}}\ {\isacharcolon}{\kern0pt}\ r\isactrlsub {\isadigit{2}}\ {\isacharplus}{\kern0pt}\ r\isactrlsub {\isadigit{1}}}}}\\[4mm]
-  \isa{\mbox{}\inferrule{\mbox{v\isactrlsub {\isadigit{1}}\ {\isacharcolon}{\kern0pt}\ r\isactrlsub {\isadigit{1}}}\\\ \mbox{v\isactrlsub {\isadigit{2}}\ {\isacharcolon}{\kern0pt}\ r\isactrlsub {\isadigit{2}}}}{\mbox{Seq\ v\isactrlsub {\isadigit{1}}\ v\isactrlsub {\isadigit{2}}\ {\isacharcolon}{\kern0pt}\ r\isactrlsub {\isadigit{1}}\ {\isasymcdot}\ r\isactrlsub {\isadigit{2}}}}}  &
-  \isa{\mbox{}\inferrule{\mbox{{\isasymforall}v{\isasymin}vs{\isachardot}{\kern0pt}\ v\ {\isacharcolon}{\kern0pt}\ r\ {\isasymand}\ {\isacharbar}{\kern0pt}v{\isacharbar}{\kern0pt}\ {\isasymnoteq}\ {\isacharbrackleft}{\kern0pt}{\isacharbrackright}{\kern0pt}}}{\mbox{Stars\ vs\ {\isacharcolon}{\kern0pt}\ r\isactrlsup {\isasymstar}}}}
-
-
-  \end{tabular}
-\end{center}
-
-
-And these can be made compact by the following simplification function:
-
+The reason that we do need to add a simplification phase
+after each derivative step of  $\textit{blexer}$ is
+because it produces intermediate
+regular expressions that can grow exponentially.
+For example, the regular expression $(a+aa)^*$ after taking
+derivative against just 10 $a$s will have size 8192.
+%TODO: add figure for this?
 \begin{center}
   \begin{tabular}{lcl}
   \isa{bsimp\ {\isacharparenleft}{\kern0pt}ASEQ\ bs\ r\isactrlsub {\isadigit{1}}\ r\isactrlsub {\isadigit{2}}{\isacharparenright}{\kern0pt}} & $\dn$ & \isa{bsimp{\isacharunderscore}{\kern0pt}ASEQ\ bs\ {\isacharparenleft}{\kern0pt}bsimp\ r\isactrlsub {\isadigit{1}}{\isacharparenright}{\kern0pt}\ {\isacharparenleft}{\kern0pt}bsimp\ r\isactrlsub {\isadigit{2}}{\isacharparenright}{\kern0pt}}\\
@@ -129,12 +99,76 @@
 \end{tabular}
 \end{center}
 
+
+This might sound trivial in the case of producing a YES/NO answer,
+but once we require a lexing output to be produced (which is required
+in applications like compiler front-end, malicious attack domain extraction, 
+etc.), it is not straightforward if we still extract what is needed according
+to the POSIX standard.
+
+
+
+
+
+By simplification, we mean specifically the following rules:
+
+\begin{center}
+  \begin{tabular}{lcl}
+  \isa{\mbox{}\inferrule{\mbox{}}{\mbox{ASEQ\ bs\ AZERO\ r\isactrlsub {\isadigit{2}}\ {\isasymleadsto}\ AZERO}}}\\
+  \isa{\mbox{}\inferrule{\mbox{}}{\mbox{ASEQ\ bs\ r\isactrlsub {\isadigit{1}}\ AZERO\ {\isasymleadsto}\ AZERO}}}\\
+  \isa{\mbox{}\inferrule{\mbox{}}{\mbox{ASEQ\ bs\ {\isacharparenleft}{\kern0pt}AONE\ bs\isactrlsub {\isadigit{1}}{\isacharparenright}{\kern0pt}\ r\isactrlsub {\isadigit{1}}\ {\isasymleadsto}\ fuse\ {\isacharparenleft}{\kern0pt}bs\ {\isacharat}{\kern0pt}\ bs\isactrlsub {\isadigit{1}}{\isacharparenright}{\kern0pt}\ r\isactrlsub {\isadigit{1}}}}}\\
+  \isa{\mbox{}\inferrule{\mbox{r\isactrlsub {\isadigit{1}}\ {\isasymleadsto}\ r\isactrlsub {\isadigit{2}}}}{\mbox{ASEQ\ bs\ r\isactrlsub {\isadigit{1}}\ r\isactrlsub {\isadigit{3}}\ {\isasymleadsto}\ ASEQ\ bs\ r\isactrlsub {\isadigit{2}}\ r\isactrlsub {\isadigit{3}}}}}\\
+  \isa{\mbox{}\inferrule{\mbox{r\isactrlsub {\isadigit{3}}\ {\isasymleadsto}\ r\isactrlsub {\isadigit{4}}}}{\mbox{ASEQ\ bs\ r\isactrlsub {\isadigit{1}}\ r\isactrlsub {\isadigit{3}}\ {\isasymleadsto}\ ASEQ\ bs\ r\isactrlsub {\isadigit{1}}\ r\isactrlsub {\isadigit{4}}}}}\\
+  \isa{\mbox{}\inferrule{\mbox{r\ {\isasymleadsto}\ r{\isacharprime}{\kern0pt}}}{\mbox{AALTs\ bs\ {\isacharparenleft}{\kern0pt}rs\isactrlsub {\isadigit{1}}\ {\isacharat}{\kern0pt}\ {\isacharbrackleft}{\kern0pt}r{\isacharbrackright}{\kern0pt}\ {\isacharat}{\kern0pt}\ rs\isactrlsub {\isadigit{2}}{\isacharparenright}{\kern0pt}\ {\isasymleadsto}\ AALTs\ bs\ {\isacharparenleft}{\kern0pt}rs\isactrlsub {\isadigit{1}}\ {\isacharat}{\kern0pt}\ {\isacharbrackleft}{\kern0pt}r{\isacharprime}{\kern0pt}{\isacharbrackright}{\kern0pt}\ {\isacharat}{\kern0pt}\ rs\isactrlsub {\isadigit{2}}{\isacharparenright}{\kern0pt}}}}\\
+  \isa{\mbox{}\inferrule{\mbox{}}{\mbox{AALTs\ bs\ {\isacharparenleft}{\kern0pt}rs\isactrlsub a\ {\isacharat}{\kern0pt}\ AZERO\mbox{$\,$}{\isacharcolon}{\kern0pt}{\isacharcolon}{\kern0pt}\mbox{$\,$}rs\isactrlsub b{\isacharparenright}{\kern0pt}\ {\isasymleadsto}\ AALTs\ bs\ {\isacharparenleft}{\kern0pt}rs\isactrlsub a\ {\isacharat}{\kern0pt}\ rs\isactrlsub b{\isacharparenright}{\kern0pt}}}}\\
+  \isa{\mbox{}\inferrule{\mbox{}}{\mbox{AALTs\ bs\ {\isacharparenleft}{\kern0pt}rs\isactrlsub a\ {\isacharat}{\kern0pt}\ AALTs\ bs\isactrlsub {\isadigit{1}}\ rs\isactrlsub {\isadigit{1}}\mbox{$\,$}{\isacharcolon}{\kern0pt}{\isacharcolon}{\kern0pt}\mbox{$\,$}rs\isactrlsub b{\isacharparenright}{\kern0pt}\ {\isasymleadsto}\ AALTs\ bs\ {\isacharparenleft}{\kern0pt}rs\isactrlsub a\ {\isacharat}{\kern0pt}\ map\ {\isacharparenleft}{\kern0pt}fuse\ bs\isactrlsub {\isadigit{1}}{\isacharparenright}{\kern0pt}\ rs\isactrlsub {\isadigit{1}}\ {\isacharat}{\kern0pt}\ rs\isactrlsub b{\isacharparenright}{\kern0pt}}}}\\
+  \isa{\mbox{}\inferrule{\mbox{}}{\mbox{AALTs\ bs\ {\isacharparenleft}{\kern0pt}map\ {\isacharparenleft}{\kern0pt}fuse\ r\isactrlsub {\isadigit{2}}{\isacharparenright}{\kern0pt}\ rs{\isacharparenright}{\kern0pt}\ {\isasymleadsto}\ AALTs\ {\isacharparenleft}{\kern0pt}bs\ {\isacharat}{\kern0pt}\ r\isactrlsub {\isadigit{2}}{\isacharparenright}{\kern0pt}\ rs}}}\\
+  \isa{\mbox{}\inferrule{\mbox{}}{\mbox{AALTs\ {\isacharparenleft}{\kern0pt}bs\ {\isacharat}{\kern0pt}\ r\isactrlsub {\isadigit{1}}{\isacharparenright}{\kern0pt}\ rs\ {\isasymleadsto}\ AALTs\ bs\ {\isacharparenleft}{\kern0pt}map\ {\isacharparenleft}{\kern0pt}fuse\ r\isactrlsub {\isadigit{1}}{\isacharparenright}{\kern0pt}\ rs{\isacharparenright}{\kern0pt}}}}\\
+  \isa{\mbox{}\inferrule{\mbox{}}{\mbox{AALTs\ bs\ {\isacharbrackleft}{\kern0pt}{\isacharbrackright}{\kern0pt}\ {\isasymleadsto}\ AZERO}}}\\
+  \isa{\mbox{}\inferrule{\mbox{}}{\mbox{AALTs\ bs\ {\isacharbrackleft}{\kern0pt}r\isactrlsub {\isadigit{1}}{\isacharbrackright}{\kern0pt}\ {\isasymleadsto}\ fuse\ bs\ r\isactrlsub {\isadigit{1}}}}}\\
+  \isa{\mbox{}\inferrule{\mbox{a\isactrlsub {\isadigit{1}}\mbox{$^\downarrow$}\ {\isacharequal}{\kern0pt}\ a\isactrlsub {\isadigit{2}}\mbox{$^\downarrow$}}}{\mbox{AALTs\ bs\ {\isacharparenleft}{\kern0pt}rs\isactrlsub a\ {\isacharat}{\kern0pt}\ {\isacharbrackleft}{\kern0pt}a\isactrlsub {\isadigit{1}}{\isacharbrackright}{\kern0pt}\ {\isacharat}{\kern0pt}\ rs\isactrlsub b\ {\isacharat}{\kern0pt}\ {\isacharbrackleft}{\kern0pt}a\isactrlsub {\isadigit{2}}{\isacharbrackright}{\kern0pt}\ {\isacharat}{\kern0pt}\ rs\isactrlsub c{\isacharparenright}{\kern0pt}\ {\isasymleadsto}\ AALTs\ bs\ {\isacharparenleft}{\kern0pt}rs\isactrlsub a\ {\isacharat}{\kern0pt}\ {\isacharbrackleft}{\kern0pt}a\isactrlsub {\isadigit{1}}{\isacharbrackright}{\kern0pt}\ {\isacharat}{\kern0pt}\ rs\isactrlsub b\ {\isacharat}{\kern0pt}\ rs\isactrlsub c{\isacharparenright}{\kern0pt}}}}\\
+
+  \end{tabular}
+\end{center}
+
+
+And these can be made compact by the following simplification function:
+
+where the function $\mathit{bsimp_AALTs}$
+
 The core idea of the proof is that two regular expressions,
 if "isomorphic" up to a finite number of rewrite steps, will
-remain so when we take derivative on both of them.
+remain "isomorphic" when we take the same sequence of
+derivatives on both of them.
 This can be expressed by the following rewrite relation lemma:
 \begin{lemma}
 \isa{{\isacharparenleft}{\kern0pt}r\mbox{$\bbslash$}s{\isacharparenright}{\kern0pt}\ {\isasymleadsto}{\isacharasterisk}{\kern0pt}\ bders{\isacharunderscore}{\kern0pt}simp\ r\ s}
+\end{lemma}
+
+This isomorphic relation implies a property that leads to the 
+correctness result: 
+if two (nullable) regular expressions are "rewritable" in many steps
+from one another, 
+then a call to function $\textit{bmkeps}$ gives the same
+bit-sequence :
+\begin{lemma}
+\isa{{\normalsize{}If\,}\ \mbox{r{\isadigit{1}}{\isachardot}{\kern0pt}{\isadigit{0}}\ {\isasymleadsto}{\isacharasterisk}{\kern0pt}\ r{\isadigit{2}}{\isachardot}{\kern0pt}{\isadigit{0}}}\ {\normalsize \,and\,}\ \mbox{nullable\mbox{$_b$}\ r{\isadigit{1}}{\isachardot}{\kern0pt}{\isadigit{0}}}\ {\normalsize \,then\,}\ mkeps\mbox{$_b$}\ r{\isadigit{1}}{\isachardot}{\kern0pt}{\isadigit{0}}\ {\isacharequal}{\kern0pt}\ mkeps\mbox{$_b$}\ r{\isadigit{2}}{\isachardot}{\kern0pt}{\isadigit{0}}{\isachardot}{\kern0pt}}
+\end{lemma}
+
+Given the same bit-sequence, the decode function
+will give out the same value, which is the output
+of both lexers:
+\begin{lemma}
+\isa{lexer\mbox{$_b$}\ r\ s\ {\isasymequiv}\ \textrm{if}\ nullable\mbox{$_b$}\ {\isacharparenleft}{\kern0pt}r\mbox{$^\uparrow$}\mbox{$\bbslash$}s{\isacharparenright}{\kern0pt}\ \textrm{then}\ decode\ {\isacharparenleft}{\kern0pt}mkeps\mbox{$_b$}\ {\isacharparenleft}{\kern0pt}r\mbox{$^\uparrow$}\mbox{$\bbslash$}s{\isacharparenright}{\kern0pt}{\isacharparenright}{\kern0pt}\ r\ \textrm{else}\ None}
+\end{lemma}
+
+\begin{lemma}
+\isa{blexer{\isacharunderscore}{\kern0pt}simp\ r\ s\ {\isasymequiv}\ \textrm{if}\ nullable\mbox{$_b$}\ {\isacharparenleft}{\kern0pt}bders{\isacharunderscore}{\kern0pt}simp\ {\isacharparenleft}{\kern0pt}r\mbox{$^\uparrow$}{\isacharparenright}{\kern0pt}\ s{\isacharparenright}{\kern0pt}\ \textrm{then}\ decode\ {\isacharparenleft}{\kern0pt}mkeps\mbox{$_b$}\ {\isacharparenleft}{\kern0pt}bders{\isacharunderscore}{\kern0pt}simp\ {\isacharparenleft}{\kern0pt}r\mbox{$^\uparrow$}{\isacharparenright}{\kern0pt}\ s{\isacharparenright}{\kern0pt}{\isacharparenright}{\kern0pt}\ r\ \textrm{else}\ None}
+\end{lemma}
+
+And that yields the correctness result:
+\begin{lemma}
+\isa{blexer{\isacharunderscore}{\kern0pt}simp\ r\ s\ {\isacharequal}{\kern0pt}\ lexer\ r\ s}
 \end{lemma}%
 \end{isamarkuptext}\isamarkuptrue%
 %
@@ -1745,45 +1779,45 @@
 %:%136=210%:%
 %:%137=211%:%
 %:%138=212%:%
-%:%147=217%:%
-%:%159=223%:%
-%:%160=224%:%
-%:%161=225%:%
-%:%162=226%:%
-%:%162=227%:%
-%:%163=228%:%
-%:%164=229%:%
-%:%165=230%:%
-%:%166=231%:%
-%:%167=232%:%
-%:%168=233%:%
-%:%169=234%:%
-%:%170=235%:%
-%:%171=236%:%
-%:%172=237%:%
-%:%173=238%:%
-%:%174=239%:%
-%:%175=240%:%
-%:%176=241%:%
-%:%177=242%:%
-%:%178=243%:%
-%:%179=244%:%
-%:%180=245%:%
-%:%181=246%:%
-%:%182=247%:%
-%:%183=248%:%
-%:%184=249%:%
-%:%185=250%:%
-%:%186=251%:%
-%:%187=252%:%
-%:%188=253%:%
-%:%189=254%:%
-%:%190=255%:%
-%:%191=256%:%
-%:%192=257%:%
-%:%193=258%:%
-%:%194=259%:%
-%:%195=260%:%
+%:%139=213%:%
+%:%140=214%:%
+%:%141=215%:%
+%:%142=216%:%
+%:%143=217%:%
+%:%144=218%:%
+%:%145=219%:%
+%:%146=220%:%
+%:%147=221%:%
+%:%148=222%:%
+%:%149=223%:%
+%:%150=224%:%
+%:%151=225%:%
+%:%152=226%:%
+%:%153=227%:%
+%:%154=228%:%
+%:%155=229%:%
+%:%156=230%:%
+%:%157=231%:%
+%:%158=232%:%
+%:%159=233%:%
+%:%160=234%:%
+%:%161=235%:%
+%:%162=236%:%
+%:%163=237%:%
+%:%164=238%:%
+%:%165=239%:%
+%:%166=240%:%
+%:%167=241%:%
+%:%168=242%:%
+%:%169=243%:%
+%:%170=244%:%
+%:%171=245%:%
+%:%172=246%:%
+%:%181=251%:%
+%:%193=257%:%
+%:%194=258%:%
+%:%195=259%:%
+%:%196=260%:%
 %:%196=261%:%
 %:%197=262%:%
 %:%198=263%:%
@@ -1815,40 +1849,40 @@
 %:%224=289%:%
 %:%225=290%:%
 %:%226=291%:%
-%:%226=292%:%
-%:%227=293%:%
-%:%228=294%:%
-%:%229=295%:%
-%:%230=296%:%
-%:%231=297%:%
-%:%232=298%:%
-%:%233=299%:%
-%:%234=300%:%
-%:%235=301%:%
-%:%236=302%:%
-%:%237=303%:%
-%:%238=304%:%
-%:%239=305%:%
-%:%240=306%:%
-%:%241=307%:%
-%:%242=308%:%
-%:%243=309%:%
-%:%244=310%:%
-%:%245=311%:%
-%:%246=312%:%
-%:%247=313%:%
-%:%248=314%:%
-%:%249=315%:%
-%:%250=316%:%
-%:%251=317%:%
-%:%252=318%:%
-%:%253=319%:%
-%:%254=320%:%
-%:%255=321%:%
-%:%256=322%:%
-%:%257=323%:%
-%:%258=324%:%
-%:%259=325%:%
+%:%227=292%:%
+%:%228=293%:%
+%:%229=294%:%
+%:%230=295%:%
+%:%231=296%:%
+%:%232=297%:%
+%:%233=298%:%
+%:%234=299%:%
+%:%235=300%:%
+%:%236=301%:%
+%:%237=302%:%
+%:%238=303%:%
+%:%239=304%:%
+%:%240=305%:%
+%:%241=306%:%
+%:%242=307%:%
+%:%243=308%:%
+%:%244=309%:%
+%:%245=310%:%
+%:%246=311%:%
+%:%247=312%:%
+%:%248=313%:%
+%:%249=314%:%
+%:%250=315%:%
+%:%251=316%:%
+%:%252=317%:%
+%:%253=318%:%
+%:%254=319%:%
+%:%255=320%:%
+%:%256=321%:%
+%:%257=322%:%
+%:%258=323%:%
+%:%259=324%:%
+%:%260=325%:%
 %:%260=326%:%
 %:%261=327%:%
 %:%262=328%:%
@@ -1921,89 +1955,89 @@
 %:%329=395%:%
 %:%330=396%:%
 %:%331=397%:%
-%:%340=404%:%
-%:%352=406%:%
-%:%353=407%:%
-%:%353=408%:%
-%:%354=409%:%
-%:%355=410%:%
-%:%356=411%:%
-%:%357=412%:%
-%:%358=413%:%
-%:%359=414%:%
-%:%360=415%:%
-%:%361=416%:%
-%:%362=417%:%
-%:%363=418%:%
-%:%364=419%:%
-%:%365=420%:%
-%:%366=421%:%
-%:%367=422%:%
-%:%368=423%:%
-%:%369=424%:%
-%:%370=425%:%
-%:%371=426%:%
-%:%372=427%:%
-%:%373=428%:%
-%:%374=429%:%
-%:%375=430%:%
-%:%376=431%:%
-%:%377=432%:%
-%:%378=433%:%
-%:%379=434%:%
-%:%380=435%:%
-%:%381=436%:%
-%:%382=437%:%
-%:%383=438%:%
-%:%384=439%:%
-%:%385=440%:%
-%:%386=441%:%
+%:%332=398%:%
+%:%333=399%:%
+%:%334=400%:%
+%:%335=401%:%
+%:%336=402%:%
+%:%337=403%:%
+%:%338=404%:%
+%:%339=405%:%
+%:%340=406%:%
+%:%341=407%:%
+%:%342=408%:%
+%:%343=409%:%
+%:%344=410%:%
+%:%345=411%:%
+%:%346=412%:%
+%:%347=413%:%
+%:%348=414%:%
+%:%349=415%:%
+%:%350=416%:%
+%:%351=417%:%
+%:%352=418%:%
+%:%353=419%:%
+%:%354=420%:%
+%:%355=421%:%
+%:%356=422%:%
+%:%357=423%:%
+%:%358=424%:%
+%:%359=425%:%
+%:%360=426%:%
+%:%361=427%:%
+%:%362=428%:%
+%:%363=429%:%
+%:%364=430%:%
+%:%365=431%:%
+%:%374=438%:%
+%:%386=440%:%
+%:%387=441%:%
 %:%387=442%:%
 %:%388=443%:%
 %:%389=444%:%
 %:%390=445%:%
 %:%391=446%:%
 %:%392=447%:%
-%:%392=448%:%
-%:%393=449%:%
-%:%394=450%:%
-%:%395=451%:%
-%:%396=452%:%
-%:%397=453%:%
-%:%397=454%:%
-%:%398=455%:%
-%:%399=456%:%
-%:%400=457%:%
-%:%401=458%:%
-%:%402=459%:%
-%:%403=460%:%
-%:%404=461%:%
-%:%405=462%:%
-%:%406=463%:%
-%:%407=464%:%
-%:%408=465%:%
-%:%409=466%:%
-%:%410=467%:%
-%:%411=468%:%
-%:%412=469%:%
-%:%413=470%:%
-%:%414=471%:%
-%:%415=472%:%
-%:%416=473%:%
-%:%417=474%:%
-%:%418=475%:%
-%:%419=476%:%
-%:%420=477%:%
-%:%421=478%:%
-%:%422=479%:%
-%:%423=480%:%
-%:%424=481%:%
-%:%425=482%:%
-%:%426=483%:%
-%:%427=484%:%
-%:%428=485%:%
-%:%429=486%:%
-%:%430=487%:%
+%:%393=448%:%
+%:%394=449%:%
+%:%395=450%:%
+%:%396=451%:%
+%:%397=452%:%
+%:%398=453%:%
+%:%399=454%:%
+%:%400=455%:%
+%:%401=456%:%
+%:%402=457%:%
+%:%403=458%:%
+%:%404=459%:%
+%:%405=460%:%
+%:%406=461%:%
+%:%407=462%:%
+%:%408=463%:%
+%:%409=464%:%
+%:%410=465%:%
+%:%411=466%:%
+%:%412=467%:%
+%:%413=468%:%
+%:%414=469%:%
+%:%415=470%:%
+%:%416=471%:%
+%:%417=472%:%
+%:%418=473%:%
+%:%419=474%:%
+%:%420=475%:%
+%:%421=476%:%
+%:%422=477%:%
+%:%423=478%:%
+%:%424=479%:%
+%:%425=480%:%
+%:%426=481%:%
+%:%426=482%:%
+%:%427=483%:%
+%:%428=484%:%
+%:%429=485%:%
+%:%430=486%:%
+%:%431=487%:%
 %:%431=488%:%
 %:%432=489%:%
 %:%433=490%:%
@@ -2060,41 +2094,41 @@
 %:%484=541%:%
 %:%485=542%:%
 %:%486=543%:%
-%:%495=547%:%
-%:%507=551%:%
-%:%508=552%:%
-%:%509=553%:%
-%:%510=554%:%
-%:%511=555%:%
-%:%512=556%:%
-%:%513=557%:%
-%:%514=558%:%
-%:%515=559%:%
-%:%516=560%:%
-%:%517=561%:%
-%:%518=562%:%
-%:%519=563%:%
-%:%520=564%:%
-%:%521=565%:%
-%:%522=566%:%
-%:%523=567%:%
-%:%524=568%:%
-%:%525=569%:%
-%:%526=570%:%
-%:%527=571%:%
-%:%528=572%:%
-%:%529=573%:%
-%:%530=574%:%
-%:%531=575%:%
-%:%532=576%:%
-%:%533=577%:%
-%:%534=578%:%
-%:%535=579%:%
-%:%536=580%:%
-%:%537=581%:%
-%:%538=582%:%
-%:%539=583%:%
-%:%540=584%:%
+%:%487=544%:%
+%:%488=545%:%
+%:%489=546%:%
+%:%490=547%:%
+%:%491=548%:%
+%:%492=549%:%
+%:%493=550%:%
+%:%494=551%:%
+%:%495=552%:%
+%:%496=553%:%
+%:%497=554%:%
+%:%498=555%:%
+%:%499=556%:%
+%:%500=557%:%
+%:%501=558%:%
+%:%502=559%:%
+%:%503=560%:%
+%:%504=561%:%
+%:%505=562%:%
+%:%506=563%:%
+%:%507=564%:%
+%:%508=565%:%
+%:%509=566%:%
+%:%510=567%:%
+%:%511=568%:%
+%:%512=569%:%
+%:%513=570%:%
+%:%514=571%:%
+%:%515=572%:%
+%:%516=573%:%
+%:%517=574%:%
+%:%518=575%:%
+%:%519=576%:%
+%:%520=577%:%
+%:%529=581%:%
 %:%541=585%:%
 %:%542=586%:%
 %:%543=587%:%
@@ -2176,45 +2210,45 @@
 %:%619=663%:%
 %:%620=664%:%
 %:%621=665%:%
-%:%621=666%:%
-%:%622=667%:%
-%:%622=668%:%
-%:%623=669%:%
-%:%624=670%:%
-%:%624=671%:%
-%:%625=672%:%
-%:%626=673%:%
-%:%627=674%:%
-%:%628=675%:%
-%:%629=676%:%
-%:%630=677%:%
-%:%631=678%:%
-%:%632=679%:%
-%:%633=680%:%
-%:%634=681%:%
-%:%635=682%:%
-%:%636=683%:%
-%:%637=684%:%
-%:%638=685%:%
-%:%639=686%:%
-%:%640=687%:%
-%:%641=688%:%
-%:%642=689%:%
-%:%643=690%:%
-%:%644=691%:%
-%:%645=692%:%
-%:%646=693%:%
-%:%647=694%:%
-%:%648=695%:%
-%:%649=696%:%
-%:%650=697%:%
-%:%651=698%:%
-%:%652=699%:%
-%:%653=700%:%
-%:%654=701%:%
-%:%655=702%:%
-%:%656=703%:%
-%:%657=704%:%
+%:%622=666%:%
+%:%623=667%:%
+%:%624=668%:%
+%:%625=669%:%
+%:%626=670%:%
+%:%627=671%:%
+%:%628=672%:%
+%:%629=673%:%
+%:%630=674%:%
+%:%631=675%:%
+%:%632=676%:%
+%:%633=677%:%
+%:%634=678%:%
+%:%635=679%:%
+%:%636=680%:%
+%:%637=681%:%
+%:%638=682%:%
+%:%639=683%:%
+%:%640=684%:%
+%:%641=685%:%
+%:%642=686%:%
+%:%643=687%:%
+%:%644=688%:%
+%:%645=689%:%
+%:%646=690%:%
+%:%647=691%:%
+%:%648=692%:%
+%:%649=693%:%
+%:%650=694%:%
+%:%651=695%:%
+%:%652=696%:%
+%:%653=697%:%
+%:%654=698%:%
+%:%655=699%:%
+%:%655=700%:%
+%:%656=701%:%
+%:%656=702%:%
+%:%657=703%:%
+%:%658=704%:%
 %:%658=705%:%
 %:%659=706%:%
 %:%660=707%:%
@@ -2238,116 +2272,116 @@
 %:%678=725%:%
 %:%679=726%:%
 %:%680=727%:%
-%:%680=728%:%
-%:%680=729%:%
-%:%681=730%:%
-%:%682=731%:%
-%:%683=732%:%
-%:%684=733%:%
-%:%685=734%:%
-%:%686=735%:%
-%:%687=736%:%
-%:%688=737%:%
-%:%689=738%:%
-%:%689=739%:%
-%:%690=740%:%
-%:%691=741%:%
-%:%692=742%:%
-%:%693=743%:%
-%:%694=744%:%
-%:%695=745%:%
-%:%696=746%:%
-%:%697=747%:%
-%:%698=748%:%
-%:%699=749%:%
-%:%700=750%:%
-%:%701=751%:%
-%:%702=752%:%
-%:%703=753%:%
-%:%704=754%:%
-%:%705=755%:%
-%:%706=756%:%
-%:%707=757%:%
-%:%708=758%:%
-%:%709=759%:%
-%:%710=760%:%
-%:%711=761%:%
-%:%712=762%:%
-%:%713=763%:%
-%:%714=764%:%
-%:%715=765%:%
-%:%716=766%:%
-%:%717=767%:%
-%:%718=768%:%
-%:%719=769%:%
-%:%720=770%:%
-%:%721=771%:%
-%:%722=772%:%
+%:%681=728%:%
+%:%682=729%:%
+%:%683=730%:%
+%:%684=731%:%
+%:%685=732%:%
+%:%686=733%:%
+%:%687=734%:%
+%:%688=735%:%
+%:%689=736%:%
+%:%690=737%:%
+%:%691=738%:%
+%:%692=739%:%
+%:%693=740%:%
+%:%694=741%:%
+%:%695=742%:%
+%:%696=743%:%
+%:%697=744%:%
+%:%698=745%:%
+%:%699=746%:%
+%:%700=747%:%
+%:%701=748%:%
+%:%702=749%:%
+%:%703=750%:%
+%:%704=751%:%
+%:%705=752%:%
+%:%706=753%:%
+%:%707=754%:%
+%:%708=755%:%
+%:%709=756%:%
+%:%710=757%:%
+%:%711=758%:%
+%:%712=759%:%
+%:%713=760%:%
+%:%714=761%:%
+%:%714=762%:%
+%:%714=763%:%
+%:%715=764%:%
+%:%716=765%:%
+%:%717=766%:%
+%:%718=767%:%
+%:%719=768%:%
+%:%720=769%:%
+%:%721=770%:%
+%:%722=771%:%
+%:%723=772%:%
 %:%723=773%:%
 %:%724=774%:%
-%:%724=775%:%
-%:%725=776%:%
-%:%726=777%:%
-%:%727=778%:%
-%:%728=779%:%
-%:%729=780%:%
-%:%730=781%:%
-%:%731=782%:%
-%:%731=783%:%
-%:%732=784%:%
-%:%733=785%:%
-%:%734=786%:%
-%:%734=787%:%
-%:%735=788%:%
-%:%736=789%:%
-%:%737=790%:%
-%:%738=791%:%
-%:%739=792%:%
-%:%740=793%:%
-%:%741=794%:%
-%:%742=795%:%
-%:%743=796%:%
-%:%744=797%:%
-%:%745=798%:%
-%:%745=799%:%
-%:%746=800%:%
-%:%747=801%:%
-%:%748=802%:%
-%:%749=803%:%
-%:%749=804%:%
-%:%750=805%:%
-%:%751=806%:%
-%:%752=807%:%
-%:%753=808%:%
-%:%754=809%:%
-%:%755=810%:%
-%:%756=811%:%
-%:%757=812%:%
-%:%758=813%:%
-%:%759=814%:%
-%:%760=815%:%
-%:%761=816%:%
-%:%762=817%:%
-%:%763=818%:%
-%:%764=819%:%
-%:%765=820%:%
-%:%766=821%:%
-%:%767=822%:%
-%:%768=823%:%
-%:%769=824%:%
-%:%770=825%:%
-%:%771=826%:%
-%:%772=827%:%
-%:%773=828%:%
-%:%774=829%:%
-%:%775=830%:%
-%:%776=831%:%
-%:%777=832%:%
-%:%778=833%:%
-%:%779=834%:%
-%:%780=835%:%
-%:%781=836%:%
-%:%782=837%:%
+%:%725=775%:%
+%:%726=776%:%
+%:%727=777%:%
+%:%728=778%:%
+%:%729=779%:%
+%:%730=780%:%
+%:%731=781%:%
+%:%732=782%:%
+%:%733=783%:%
+%:%734=784%:%
+%:%735=785%:%
+%:%736=786%:%
+%:%737=787%:%
+%:%738=788%:%
+%:%739=789%:%
+%:%740=790%:%
+%:%741=791%:%
+%:%742=792%:%
+%:%743=793%:%
+%:%744=794%:%
+%:%745=795%:%
+%:%746=796%:%
+%:%747=797%:%
+%:%748=798%:%
+%:%749=799%:%
+%:%750=800%:%
+%:%751=801%:%
+%:%752=802%:%
+%:%753=803%:%
+%:%754=804%:%
+%:%755=805%:%
+%:%756=806%:%
+%:%757=807%:%
+%:%758=808%:%
+%:%758=809%:%
+%:%759=810%:%
+%:%760=811%:%
+%:%761=812%:%
+%:%762=813%:%
+%:%763=814%:%
+%:%764=815%:%
+%:%765=816%:%
+%:%765=817%:%
+%:%766=818%:%
+%:%767=819%:%
+%:%768=820%:%
+%:%768=821%:%
+%:%769=822%:%
+%:%770=823%:%
+%:%771=824%:%
+%:%772=825%:%
+%:%773=826%:%
+%:%774=827%:%
+%:%775=828%:%
+%:%776=829%:%
+%:%777=830%:%
+%:%778=831%:%
+%:%779=832%:%
+%:%779=833%:%
+%:%780=834%:%
+%:%781=835%:%
+%:%782=836%:%
+%:%783=837%:%
 %:%783=838%:%
 %:%784=839%:%
 %:%785=840%:%
@@ -2373,239 +2407,239 @@
 %:%805=860%:%
 %:%806=861%:%
 %:%807=862%:%
-%:%807=863%:%
-%:%808=864%:%
-%:%809=865%:%
-%:%810=866%:%
-%:%811=867%:%
-%:%812=868%:%
-%:%813=869%:%
-%:%814=870%:%
-%:%815=871%:%
-%:%816=872%:%
-%:%817=873%:%
-%:%818=874%:%
-%:%819=875%:%
-%:%820=876%:%
-%:%821=877%:%
-%:%822=878%:%
-%:%823=879%:%
-%:%824=880%:%
-%:%825=881%:%
-%:%826=882%:%
-%:%827=883%:%
-%:%828=884%:%
-%:%829=885%:%
-%:%830=886%:%
-%:%831=887%:%
-%:%832=888%:%
-%:%833=889%:%
-%:%834=890%:%
-%:%835=891%:%
-%:%836=892%:%
-%:%837=893%:%
-%:%838=894%:%
-%:%839=895%:%
-%:%840=896%:%
-%:%840=897%:%
-%:%841=898%:%
-%:%842=899%:%
-%:%843=900%:%
-%:%844=901%:%
-%:%845=902%:%
-%:%846=903%:%
-%:%847=904%:%
-%:%848=905%:%
-%:%849=906%:%
-%:%850=907%:%
-%:%851=908%:%
-%:%852=909%:%
-%:%853=910%:%
-%:%854=911%:%
-%:%855=912%:%
-%:%856=913%:%
-%:%857=914%:%
-%:%858=915%:%
-%:%859=916%:%
-%:%860=917%:%
-%:%861=918%:%
-%:%862=919%:%
-%:%863=920%:%
-%:%864=921%:%
-%:%865=922%:%
-%:%866=923%:%
-%:%867=924%:%
-%:%868=925%:%
-%:%869=926%:%
-%:%870=927%:%
-%:%870=928%:%
-%:%871=929%:%
-%:%872=930%:%
-%:%873=931%:%
-%:%874=932%:%
-%:%875=933%:%
-%:%876=934%:%
-%:%877=935%:%
-%:%878=936%:%
-%:%878=937%:%
-%:%879=938%:%
-%:%880=939%:%
-%:%881=940%:%
-%:%882=941%:%
-%:%883=942%:%
-%:%884=943%:%
-%:%885=944%:%
-%:%886=945%:%
-%:%887=946%:%
-%:%888=947%:%
-%:%889=948%:%
-%:%890=949%:%
-%:%891=950%:%
-%:%892=951%:%
-%:%893=952%:%
-%:%894=953%:%
-%:%895=954%:%
-%:%896=955%:%
-%:%897=956%:%
-%:%898=957%:%
-%:%899=958%:%
-%:%900=959%:%
-%:%901=960%:%
-%:%902=961%:%
-%:%903=962%:%
-%:%904=963%:%
-%:%905=964%:%
-%:%906=965%:%
-%:%907=966%:%
-%:%908=967%:%
-%:%909=968%:%
-%:%910=969%:%
-%:%911=970%:%
+%:%808=863%:%
+%:%809=864%:%
+%:%810=865%:%
+%:%811=866%:%
+%:%812=867%:%
+%:%813=868%:%
+%:%814=869%:%
+%:%815=870%:%
+%:%816=871%:%
+%:%817=872%:%
+%:%818=873%:%
+%:%819=874%:%
+%:%820=875%:%
+%:%821=876%:%
+%:%822=877%:%
+%:%823=878%:%
+%:%824=879%:%
+%:%825=880%:%
+%:%826=881%:%
+%:%827=882%:%
+%:%828=883%:%
+%:%829=884%:%
+%:%830=885%:%
+%:%831=886%:%
+%:%832=887%:%
+%:%833=888%:%
+%:%834=889%:%
+%:%835=890%:%
+%:%836=891%:%
+%:%837=892%:%
+%:%838=893%:%
+%:%839=894%:%
+%:%840=895%:%
+%:%841=896%:%
+%:%841=897%:%
+%:%842=898%:%
+%:%843=899%:%
+%:%844=900%:%
+%:%845=901%:%
+%:%846=902%:%
+%:%847=903%:%
+%:%848=904%:%
+%:%849=905%:%
+%:%850=906%:%
+%:%851=907%:%
+%:%852=908%:%
+%:%853=909%:%
+%:%854=910%:%
+%:%855=911%:%
+%:%856=912%:%
+%:%857=913%:%
+%:%858=914%:%
+%:%859=915%:%
+%:%860=916%:%
+%:%861=917%:%
+%:%862=918%:%
+%:%863=919%:%
+%:%864=920%:%
+%:%865=921%:%
+%:%866=922%:%
+%:%867=923%:%
+%:%868=924%:%
+%:%869=925%:%
+%:%870=926%:%
+%:%871=927%:%
+%:%872=928%:%
+%:%873=929%:%
+%:%874=930%:%
+%:%874=931%:%
+%:%875=932%:%
+%:%876=933%:%
+%:%877=934%:%
+%:%878=935%:%
+%:%879=936%:%
+%:%880=937%:%
+%:%881=938%:%
+%:%882=939%:%
+%:%883=940%:%
+%:%884=941%:%
+%:%885=942%:%
+%:%886=943%:%
+%:%887=944%:%
+%:%888=945%:%
+%:%889=946%:%
+%:%890=947%:%
+%:%891=948%:%
+%:%892=949%:%
+%:%893=950%:%
+%:%894=951%:%
+%:%895=952%:%
+%:%896=953%:%
+%:%897=954%:%
+%:%898=955%:%
+%:%899=956%:%
+%:%900=957%:%
+%:%901=958%:%
+%:%902=959%:%
+%:%903=960%:%
+%:%904=961%:%
+%:%904=962%:%
+%:%905=963%:%
+%:%906=964%:%
+%:%907=965%:%
+%:%908=966%:%
+%:%909=967%:%
+%:%910=968%:%
+%:%911=969%:%
+%:%912=970%:%
 %:%912=971%:%
 %:%913=972%:%
 %:%914=973%:%
 %:%915=974%:%
-%:%915=975%:%
-%:%915=976%:%
-%:%916=977%:%
-%:%916=978%:%
-%:%916=979%:%
-%:%917=980%:%
-%:%918=981%:%
-%:%918=982%:%
-%:%919=983%:%
-%:%920=984%:%
-%:%921=985%:%
-%:%922=986%:%
-%:%923=987%:%
-%:%924=988%:%
-%:%925=989%:%
-%:%926=990%:%
-%:%927=991%:%
-%:%928=992%:%
-%:%929=993%:%
-%:%930=994%:%
-%:%931=995%:%
-%:%932=996%:%
-%:%933=997%:%
-%:%934=998%:%
-%:%935=999%:%
-%:%936=1000%:%
-%:%937=1001%:%
-%:%938=1002%:%
-%:%939=1003%:%
-%:%940=1004%:%
-%:%941=1005%:%
-%:%942=1006%:%
-%:%943=1007%:%
-%:%944=1008%:%
-%:%945=1009%:%
-%:%946=1010%:%
-%:%947=1011%:%
-%:%948=1012%:%
-%:%949=1013%:%
-%:%950=1014%:%
-%:%951=1015%:%
+%:%916=975%:%
+%:%917=976%:%
+%:%918=977%:%
+%:%919=978%:%
+%:%920=979%:%
+%:%921=980%:%
+%:%922=981%:%
+%:%923=982%:%
+%:%924=983%:%
+%:%925=984%:%
+%:%926=985%:%
+%:%927=986%:%
+%:%928=987%:%
+%:%929=988%:%
+%:%930=989%:%
+%:%931=990%:%
+%:%932=991%:%
+%:%933=992%:%
+%:%934=993%:%
+%:%935=994%:%
+%:%936=995%:%
+%:%937=996%:%
+%:%938=997%:%
+%:%939=998%:%
+%:%940=999%:%
+%:%941=1000%:%
+%:%942=1001%:%
+%:%943=1002%:%
+%:%944=1003%:%
+%:%945=1004%:%
+%:%946=1005%:%
+%:%947=1006%:%
+%:%948=1007%:%
+%:%949=1008%:%
+%:%949=1009%:%
+%:%949=1010%:%
+%:%950=1011%:%
+%:%950=1012%:%
+%:%950=1013%:%
+%:%951=1014%:%
+%:%952=1015%:%
 %:%952=1016%:%
-%:%952=1017%:%
-%:%953=1018%:%
-%:%954=1019%:%
-%:%955=1020%:%
-%:%955=1021%:%
-%:%955=1022%:%
-%:%955=1023%:%
-%:%956=1024%:%
-%:%957=1025%:%
-%:%958=1026%:%
-%:%959=1027%:%
-%:%960=1028%:%
-%:%961=1029%:%
-%:%962=1030%:%
-%:%963=1031%:%
-%:%964=1032%:%
-%:%965=1033%:%
-%:%966=1034%:%
-%:%967=1035%:%
-%:%968=1036%:%
-%:%969=1037%:%
-%:%970=1038%:%
-%:%971=1039%:%
-%:%972=1040%:%
-%:%973=1041%:%
-%:%974=1042%:%
-%:%975=1043%:%
-%:%976=1044%:%
-%:%977=1045%:%
-%:%978=1046%:%
-%:%979=1047%:%
-%:%980=1048%:%
-%:%981=1049%:%
-%:%982=1050%:%
-%:%983=1051%:%
-%:%984=1052%:%
-%:%985=1053%:%
-%:%986=1054%:%
-%:%987=1055%:%
-%:%988=1056%:%
+%:%953=1017%:%
+%:%954=1018%:%
+%:%955=1019%:%
+%:%956=1020%:%
+%:%957=1021%:%
+%:%958=1022%:%
+%:%959=1023%:%
+%:%960=1024%:%
+%:%961=1025%:%
+%:%962=1026%:%
+%:%963=1027%:%
+%:%964=1028%:%
+%:%965=1029%:%
+%:%966=1030%:%
+%:%967=1031%:%
+%:%968=1032%:%
+%:%969=1033%:%
+%:%970=1034%:%
+%:%971=1035%:%
+%:%972=1036%:%
+%:%973=1037%:%
+%:%974=1038%:%
+%:%975=1039%:%
+%:%976=1040%:%
+%:%977=1041%:%
+%:%978=1042%:%
+%:%979=1043%:%
+%:%980=1044%:%
+%:%981=1045%:%
+%:%982=1046%:%
+%:%983=1047%:%
+%:%984=1048%:%
+%:%985=1049%:%
+%:%986=1050%:%
+%:%986=1051%:%
+%:%987=1052%:%
+%:%988=1053%:%
+%:%989=1054%:%
+%:%989=1055%:%
+%:%989=1056%:%
 %:%989=1057%:%
 %:%990=1058%:%
 %:%991=1059%:%
 %:%992=1060%:%
-%:%1001=1064%:%
-%:%1013=1068%:%
-%:%1014=1069%:%
-%:%1015=1070%:%
-%:%1016=1071%:%
-%:%1017=1072%:%
-%:%1018=1073%:%
-%:%1019=1074%:%
-%:%1020=1075%:%
-%:%1021=1076%:%
-%:%1022=1077%:%
-%:%1023=1078%:%
-%:%1024=1079%:%
-%:%1025=1080%:%
-%:%1026=1081%:%
-%:%1027=1082%:%
-%:%1028=1083%:%
-%:%1029=1084%:%
-%:%1030=1085%:%
-%:%1031=1086%:%
-%:%1032=1087%:%
-%:%1033=1088%:%
-%:%1034=1089%:%
-%:%1035=1090%:%
-%:%1036=1091%:%
-%:%1037=1092%:%
-%:%1038=1093%:%
-%:%1039=1094%:%
-%:%1040=1095%:%
-%:%1041=1096%:%
-%:%1042=1097%:%
-%:%1043=1098%:%
-%:%1044=1099%:%
-%:%1045=1100%:%
-%:%1046=1101%:%
+%:%993=1061%:%
+%:%994=1062%:%
+%:%995=1063%:%
+%:%996=1064%:%
+%:%997=1065%:%
+%:%998=1066%:%
+%:%999=1067%:%
+%:%1000=1068%:%
+%:%1001=1069%:%
+%:%1002=1070%:%
+%:%1003=1071%:%
+%:%1004=1072%:%
+%:%1005=1073%:%
+%:%1006=1074%:%
+%:%1007=1075%:%
+%:%1008=1076%:%
+%:%1009=1077%:%
+%:%1010=1078%:%
+%:%1011=1079%:%
+%:%1012=1080%:%
+%:%1013=1081%:%
+%:%1014=1082%:%
+%:%1015=1083%:%
+%:%1016=1084%:%
+%:%1017=1085%:%
+%:%1018=1086%:%
+%:%1019=1087%:%
+%:%1020=1088%:%
+%:%1021=1089%:%
+%:%1022=1090%:%
+%:%1023=1091%:%
+%:%1024=1092%:%
+%:%1025=1093%:%
+%:%1026=1094%:%
+%:%1035=1098%:%
 %:%1047=1102%:%
 %:%1048=1103%:%
 %:%1049=1104%:%
@@ -2688,52 +2722,52 @@
 %:%1126=1181%:%
 %:%1127=1182%:%
 %:%1128=1183%:%
-%:%1128=1184%:%
-%:%1129=1185%:%
-%:%1130=1186%:%
-%:%1131=1187%:%
-%:%1132=1188%:%
-%:%1133=1189%:%
-%:%1134=1190%:%
-%:%1135=1191%:%
-%:%1136=1192%:%
-%:%1137=1193%:%
-%:%1138=1194%:%
-%:%1139=1195%:%
-%:%1139=1196%:%
-%:%1140=1197%:%
-%:%1141=1198%:%
-%:%1142=1199%:%
-%:%1143=1200%:%
-%:%1144=1201%:%
-%:%1145=1202%:%
-%:%1146=1203%:%
-%:%1147=1204%:%
-%:%1148=1205%:%
-%:%1149=1206%:%
-%:%1150=1207%:%
-%:%1151=1208%:%
-%:%1152=1209%:%
-%:%1153=1210%:%
-%:%1154=1211%:%
-%:%1155=1212%:%
-%:%1156=1213%:%
-%:%1157=1214%:%
-%:%1158=1215%:%
-%:%1159=1216%:%
-%:%1160=1217%:%
-%:%1161=1218%:%
-%:%1162=1219%:%
-%:%1163=1220%:%
-%:%1164=1221%:%
-%:%1165=1222%:%
-%:%1166=1223%:%
-%:%1167=1224%:%
-%:%1168=1225%:%
-%:%1169=1226%:%
-%:%1170=1227%:%
-%:%1171=1228%:%
-%:%1172=1229%:%
+%:%1129=1184%:%
+%:%1130=1185%:%
+%:%1131=1186%:%
+%:%1132=1187%:%
+%:%1133=1188%:%
+%:%1134=1189%:%
+%:%1135=1190%:%
+%:%1136=1191%:%
+%:%1137=1192%:%
+%:%1138=1193%:%
+%:%1139=1194%:%
+%:%1140=1195%:%
+%:%1141=1196%:%
+%:%1142=1197%:%
+%:%1143=1198%:%
+%:%1144=1199%:%
+%:%1145=1200%:%
+%:%1146=1201%:%
+%:%1147=1202%:%
+%:%1148=1203%:%
+%:%1149=1204%:%
+%:%1150=1205%:%
+%:%1151=1206%:%
+%:%1152=1207%:%
+%:%1153=1208%:%
+%:%1154=1209%:%
+%:%1155=1210%:%
+%:%1156=1211%:%
+%:%1157=1212%:%
+%:%1158=1213%:%
+%:%1159=1214%:%
+%:%1160=1215%:%
+%:%1161=1216%:%
+%:%1162=1217%:%
+%:%1162=1218%:%
+%:%1163=1219%:%
+%:%1164=1220%:%
+%:%1165=1221%:%
+%:%1166=1222%:%
+%:%1167=1223%:%
+%:%1168=1224%:%
+%:%1169=1225%:%
+%:%1170=1226%:%
+%:%1171=1227%:%
+%:%1172=1228%:%
+%:%1173=1229%:%
 %:%1173=1230%:%
 %:%1174=1231%:%
 %:%1175=1232%:%
@@ -2755,52 +2789,52 @@
 %:%1191=1248%:%
 %:%1192=1249%:%
 %:%1193=1250%:%
-%:%1193=1251%:%
-%:%1193=1252%:%
-%:%1194=1253%:%
-%:%1195=1254%:%
-%:%1195=1255%:%
-%:%1195=1256%:%
-%:%1195=1257%:%
-%:%1196=1258%:%
-%:%1197=1259%:%
-%:%1198=1260%:%
-%:%1199=1261%:%
-%:%1200=1262%:%
-%:%1200=1263%:%
-%:%1201=1264%:%
-%:%1202=1265%:%
-%:%1203=1266%:%
-%:%1204=1267%:%
-%:%1205=1268%:%
-%:%1206=1269%:%
-%:%1207=1270%:%
-%:%1208=1271%:%
-%:%1209=1272%:%
-%:%1210=1273%:%
-%:%1211=1274%:%
-%:%1212=1275%:%
-%:%1213=1276%:%
-%:%1214=1277%:%
-%:%1215=1278%:%
-%:%1216=1279%:%
-%:%1217=1280%:%
-%:%1218=1281%:%
-%:%1219=1282%:%
-%:%1220=1283%:%
-%:%1221=1284%:%
-%:%1222=1285%:%
-%:%1223=1286%:%
-%:%1224=1287%:%
-%:%1225=1288%:%
-%:%1226=1289%:%
-%:%1227=1290%:%
-%:%1228=1291%:%
-%:%1229=1292%:%
-%:%1230=1293%:%
-%:%1231=1294%:%
-%:%1232=1295%:%
-%:%1233=1296%:%
+%:%1194=1251%:%
+%:%1195=1252%:%
+%:%1196=1253%:%
+%:%1197=1254%:%
+%:%1198=1255%:%
+%:%1199=1256%:%
+%:%1200=1257%:%
+%:%1201=1258%:%
+%:%1202=1259%:%
+%:%1203=1260%:%
+%:%1204=1261%:%
+%:%1205=1262%:%
+%:%1206=1263%:%
+%:%1207=1264%:%
+%:%1208=1265%:%
+%:%1209=1266%:%
+%:%1210=1267%:%
+%:%1211=1268%:%
+%:%1212=1269%:%
+%:%1213=1270%:%
+%:%1214=1271%:%
+%:%1215=1272%:%
+%:%1216=1273%:%
+%:%1217=1274%:%
+%:%1218=1275%:%
+%:%1219=1276%:%
+%:%1220=1277%:%
+%:%1221=1278%:%
+%:%1222=1279%:%
+%:%1223=1280%:%
+%:%1224=1281%:%
+%:%1225=1282%:%
+%:%1226=1283%:%
+%:%1227=1284%:%
+%:%1227=1285%:%
+%:%1227=1286%:%
+%:%1228=1287%:%
+%:%1229=1288%:%
+%:%1229=1289%:%
+%:%1229=1290%:%
+%:%1229=1291%:%
+%:%1230=1292%:%
+%:%1231=1293%:%
+%:%1232=1294%:%
+%:%1233=1295%:%
+%:%1234=1296%:%
 %:%1234=1297%:%
 %:%1235=1298%:%
 %:%1236=1299%:%
@@ -2816,143 +2850,143 @@
 %:%1246=1309%:%
 %:%1247=1310%:%
 %:%1248=1311%:%
-%:%1248=1312%:%
-%:%1249=1313%:%
-%:%1249=1314%:%
-%:%1250=1315%:%
-%:%1250=1316%:%
-%:%1251=1317%:%
-%:%1252=1318%:%
-%:%1253=1319%:%
-%:%1254=1320%:%
-%:%1255=1321%:%
-%:%1256=1322%:%
-%:%1257=1323%:%
-%:%1257=1324%:%
-%:%1258=1325%:%
-%:%1258=1326%:%
-%:%1259=1327%:%
-%:%1259=1328%:%
-%:%1260=1329%:%
-%:%1261=1330%:%
-%:%1262=1331%:%
-%:%1263=1332%:%
-%:%1264=1333%:%
-%:%1265=1334%:%
-%:%1266=1335%:%
-%:%1267=1336%:%
-%:%1268=1337%:%
-%:%1269=1338%:%
-%:%1270=1339%:%
-%:%1271=1340%:%
-%:%1272=1341%:%
-%:%1273=1342%:%
-%:%1274=1343%:%
-%:%1275=1344%:%
-%:%1276=1345%:%
-%:%1277=1346%:%
-%:%1278=1347%:%
-%:%1279=1348%:%
-%:%1280=1349%:%
-%:%1281=1350%:%
-%:%1282=1351%:%
-%:%1283=1352%:%
-%:%1284=1353%:%
-%:%1285=1354%:%
-%:%1286=1355%:%
-%:%1287=1356%:%
-%:%1288=1357%:%
-%:%1289=1358%:%
-%:%1290=1359%:%
-%:%1290=1360%:%
-%:%1291=1361%:%
-%:%1292=1362%:%
-%:%1293=1363%:%
-%:%1294=1364%:%
-%:%1295=1365%:%
-%:%1296=1366%:%
-%:%1297=1367%:%
-%:%1297=1368%:%
-%:%1298=1369%:%
-%:%1299=1370%:%
-%:%1300=1371%:%
-%:%1300=1372%:%
-%:%1301=1373%:%
-%:%1302=1374%:%
-%:%1303=1375%:%
-%:%1303=1376%:%
-%:%1304=1377%:%
-%:%1304=1378%:%
-%:%1305=1379%:%
-%:%1305=1380%:%
-%:%1306=1381%:%
-%:%1307=1382%:%
-%:%1308=1383%:%
-%:%1308=1384%:%
-%:%1309=1385%:%
-%:%1309=1386%:%
-%:%1310=1387%:%
-%:%1310=1388%:%
-%:%1310=1389%:%
-%:%1310=1390%:%
-%:%1311=1391%:%
-%:%1311=1392%:%
-%:%1312=1393%:%
-%:%1313=1394%:%
-%:%1313=1396%:%
-%:%1313=1397%:%
-%:%1313=1398%:%
-%:%1313=1399%:%
-%:%1313=1400%:%
-%:%1314=1401%:%
-%:%1314=1402%:%
-%:%1315=1403%:%
-%:%1315=1404%:%
-%:%1316=1405%:%
-%:%1316=1406%:%
-%:%1317=1407%:%
-%:%1318=1408%:%
-%:%1319=1409%:%
-%:%1320=1410%:%
-%:%1320=1411%:%
-%:%1321=1412%:%
-%:%1321=1413%:%
-%:%1322=1414%:%
-%:%1323=1415%:%
-%:%1323=1416%:%
-%:%1324=1417%:%
-%:%1325=1418%:%
-%:%1326=1419%:%
-%:%1327=1420%:%
-%:%1328=1421%:%
-%:%1329=1422%:%
-%:%1330=1423%:%
-%:%1331=1424%:%
-%:%1332=1425%:%
-%:%1333=1426%:%
-%:%1334=1427%:%
-%:%1335=1428%:%
-%:%1336=1429%:%
-%:%1337=1430%:%
-%:%1338=1431%:%
-%:%1339=1432%:%
-%:%1340=1433%:%
-%:%1341=1434%:%
-%:%1342=1435%:%
-%:%1343=1436%:%
-%:%1344=1437%:%
-%:%1345=1438%:%
-%:%1346=1439%:%
-%:%1347=1440%:%
-%:%1348=1441%:%
-%:%1349=1442%:%
-%:%1350=1443%:%
-%:%1351=1444%:%
-%:%1352=1445%:%
-%:%1353=1446%:%
-%:%1354=1447%:%
-%:%1355=1448%:%
-%:%1356=1449%:%
+%:%1249=1312%:%
+%:%1250=1313%:%
+%:%1251=1314%:%
+%:%1252=1315%:%
+%:%1253=1316%:%
+%:%1254=1317%:%
+%:%1255=1318%:%
+%:%1256=1319%:%
+%:%1257=1320%:%
+%:%1258=1321%:%
+%:%1259=1322%:%
+%:%1260=1323%:%
+%:%1261=1324%:%
+%:%1262=1325%:%
+%:%1263=1326%:%
+%:%1264=1327%:%
+%:%1265=1328%:%
+%:%1266=1329%:%
+%:%1267=1330%:%
+%:%1268=1331%:%
+%:%1269=1332%:%
+%:%1270=1333%:%
+%:%1271=1334%:%
+%:%1272=1335%:%
+%:%1273=1336%:%
+%:%1274=1337%:%
+%:%1275=1338%:%
+%:%1276=1339%:%
+%:%1277=1340%:%
+%:%1278=1341%:%
+%:%1279=1342%:%
+%:%1280=1343%:%
+%:%1281=1344%:%
+%:%1282=1345%:%
+%:%1282=1346%:%
+%:%1283=1347%:%
+%:%1283=1348%:%
+%:%1284=1349%:%
+%:%1284=1350%:%
+%:%1285=1351%:%
+%:%1286=1352%:%
+%:%1287=1353%:%
+%:%1288=1354%:%
+%:%1289=1355%:%
+%:%1290=1356%:%
+%:%1291=1357%:%
+%:%1291=1358%:%
+%:%1292=1359%:%
+%:%1292=1360%:%
+%:%1293=1361%:%
+%:%1293=1362%:%
+%:%1294=1363%:%
+%:%1295=1364%:%
+%:%1296=1365%:%
+%:%1297=1366%:%
+%:%1298=1367%:%
+%:%1299=1368%:%
+%:%1300=1369%:%
+%:%1301=1370%:%
+%:%1302=1371%:%
+%:%1303=1372%:%
+%:%1304=1373%:%
+%:%1305=1374%:%
+%:%1306=1375%:%
+%:%1307=1376%:%
+%:%1308=1377%:%
+%:%1309=1378%:%
+%:%1310=1379%:%
+%:%1311=1380%:%
+%:%1312=1381%:%
+%:%1313=1382%:%
+%:%1314=1383%:%
+%:%1315=1384%:%
+%:%1316=1385%:%
+%:%1317=1386%:%
+%:%1318=1387%:%
+%:%1319=1388%:%
+%:%1320=1389%:%
+%:%1321=1390%:%
+%:%1322=1391%:%
+%:%1323=1392%:%
+%:%1324=1393%:%
+%:%1324=1394%:%
+%:%1325=1395%:%
+%:%1326=1396%:%
+%:%1327=1397%:%
+%:%1328=1398%:%
+%:%1329=1399%:%
+%:%1330=1400%:%
+%:%1331=1401%:%
+%:%1331=1402%:%
+%:%1332=1403%:%
+%:%1333=1404%:%
+%:%1334=1405%:%
+%:%1334=1406%:%
+%:%1335=1407%:%
+%:%1336=1408%:%
+%:%1337=1409%:%
+%:%1337=1410%:%
+%:%1338=1411%:%
+%:%1338=1412%:%
+%:%1339=1413%:%
+%:%1339=1414%:%
+%:%1340=1415%:%
+%:%1341=1416%:%
+%:%1342=1417%:%
+%:%1342=1418%:%
+%:%1343=1419%:%
+%:%1343=1420%:%
+%:%1344=1421%:%
+%:%1344=1422%:%
+%:%1344=1423%:%
+%:%1344=1424%:%
+%:%1345=1425%:%
+%:%1345=1426%:%
+%:%1346=1427%:%
+%:%1347=1428%:%
+%:%1347=1430%:%
+%:%1347=1431%:%
+%:%1347=1432%:%
+%:%1347=1433%:%
+%:%1347=1434%:%
+%:%1348=1435%:%
+%:%1348=1436%:%
+%:%1349=1437%:%
+%:%1349=1438%:%
+%:%1350=1439%:%
+%:%1350=1440%:%
+%:%1351=1441%:%
+%:%1352=1442%:%
+%:%1353=1443%:%
+%:%1354=1444%:%
+%:%1354=1445%:%
+%:%1355=1446%:%
+%:%1355=1447%:%
+%:%1356=1448%:%
+%:%1357=1449%:%
 %:%1357=1450%:%
 %:%1358=1451%:%
 %:%1359=1452%:%
@@ -2971,49 +3005,49 @@
 %:%1372=1465%:%
 %:%1373=1466%:%
 %:%1374=1467%:%
-%:%1383=1471%:%
-%:%1395=1478%:%
-%:%1396=1479%:%
-%:%1397=1480%:%
-%:%1398=1481%:%
-%:%1399=1482%:%
-%:%1400=1483%:%
-%:%1401=1484%:%
-%:%1410=1489%:%
-%:%1422=1493%:%
-%:%1423=1494%:%
-%:%1424=1495%:%
-%:%1425=1496%:%
-%:%1426=1497%:%
-%:%1427=1498%:%
-%:%1428=1499%:%
-%:%1429=1500%:%
-%:%1430=1501%:%
-%:%1431=1502%:%
-%:%1432=1503%:%
-%:%1433=1504%:%
-%:%1434=1505%:%
-%:%1435=1506%:%
-%:%1436=1507%:%
-%:%1437=1508%:%
-%:%1438=1509%:%
-%:%1439=1510%:%
-%:%1440=1511%:%
-%:%1441=1512%:%
-%:%1442=1513%:%
-%:%1443=1514%:%
-%:%1444=1515%:%
-%:%1445=1516%:%
-%:%1446=1517%:%
-%:%1447=1518%:%
-%:%1448=1519%:%
-%:%1449=1520%:%
-%:%1450=1521%:%
-%:%1451=1522%:%
-%:%1452=1523%:%
-%:%1453=1524%:%
-%:%1454=1525%:%
-%:%1455=1526%:%
+%:%1375=1468%:%
+%:%1376=1469%:%
+%:%1377=1470%:%
+%:%1378=1471%:%
+%:%1379=1472%:%
+%:%1380=1473%:%
+%:%1381=1474%:%
+%:%1382=1475%:%
+%:%1383=1476%:%
+%:%1384=1477%:%
+%:%1385=1478%:%
+%:%1386=1479%:%
+%:%1387=1480%:%
+%:%1388=1481%:%
+%:%1389=1482%:%
+%:%1390=1483%:%
+%:%1391=1484%:%
+%:%1392=1485%:%
+%:%1393=1486%:%
+%:%1394=1487%:%
+%:%1395=1488%:%
+%:%1396=1489%:%
+%:%1397=1490%:%
+%:%1398=1491%:%
+%:%1399=1492%:%
+%:%1400=1493%:%
+%:%1401=1494%:%
+%:%1402=1495%:%
+%:%1403=1496%:%
+%:%1404=1497%:%
+%:%1405=1498%:%
+%:%1406=1499%:%
+%:%1407=1500%:%
+%:%1408=1501%:%
+%:%1417=1505%:%
+%:%1429=1512%:%
+%:%1430=1513%:%
+%:%1431=1514%:%
+%:%1432=1515%:%
+%:%1433=1516%:%
+%:%1434=1517%:%
+%:%1435=1518%:%
+%:%1444=1523%:%
 %:%1456=1527%:%
 %:%1457=1528%:%
 %:%1458=1529%:%
@@ -3070,118 +3104,118 @@
 %:%1509=1580%:%
 %:%1510=1581%:%
 %:%1511=1582%:%
-%:%1511=1698%:%
-%:%1512=1699%:%
-%:%1513=1700%:%
-%:%1514=1701%:%
-%:%1515=1702%:%
-%:%1515=1863%:%
-%:%1516=1864%:%
-%:%1517=1865%:%
-%:%1518=1866%:%
-%:%1519=1867%:%
-%:%1520=1868%:%
-%:%1521=1869%:%
-%:%1522=1870%:%
-%:%1523=1871%:%
-%:%1524=1872%:%
-%:%1525=1873%:%
-%:%1526=1874%:%
-%:%1527=1875%:%
-%:%1528=1876%:%
-%:%1529=1877%:%
-%:%1530=1878%:%
-%:%1531=1879%:%
-%:%1532=1880%:%
-%:%1533=1881%:%
-%:%1534=1882%:%
-%:%1534=1883%:%
-%:%1535=1884%:%
-%:%1535=1885%:%
-%:%1535=1886%:%
-%:%1536=1887%:%
-%:%1536=1888%:%
-%:%1537=1889%:%
-%:%1538=1890%:%
-%:%1539=1891%:%
-%:%1540=1892%:%
-%:%1541=1893%:%
-%:%1542=1894%:%
-%:%1543=1895%:%
-%:%1544=1896%:%
-%:%1545=1897%:%
-%:%1546=1898%:%
-%:%1547=1899%:%
-%:%1548=1900%:%
-%:%1549=1901%:%
-%:%1550=1902%:%
-%:%1551=1903%:%
-%:%1552=1904%:%
-%:%1553=1905%:%
-%:%1553=1906%:%
-%:%1554=1907%:%
-%:%1555=1908%:%
-%:%1556=1909%:%
-%:%1556=1910%:%
-%:%1556=1911%:%
-%:%1557=1912%:%
-%:%1558=1913%:%
-%:%1559=1914%:%
-%:%1559=1915%:%
-%:%1560=1916%:%
-%:%1560=1917%:%
-%:%1561=1918%:%
-%:%1562=1919%:%
-%:%1563=1920%:%
-%:%1564=1921%:%
-%:%1565=1922%:%
-%:%1566=1923%:%
-%:%1567=1924%:%
-%:%1568=1925%:%
-%:%1569=1926%:%
-%:%1570=1927%:%
-%:%1571=1928%:%
-%:%1572=1929%:%
-%:%1573=1930%:%
-%:%1574=1931%:%
-%:%1575=1932%:%
-%:%1576=1933%:%
-%:%1577=1934%:%
-%:%1586=1939%:%
-%:%1598=1943%:%
-%:%1599=1944%:%
-%:%1600=1945%:%
-%:%1601=1946%:%
-%:%1602=1947%:%
-%:%1603=1948%:%
-%:%1604=1949%:%
-%:%1605=1950%:%
-%:%1606=1951%:%
-%:%1607=1952%:%
-%:%1608=1953%:%
-%:%1609=1954%:%
-%:%1610=1955%:%
-%:%1611=1956%:%
-%:%1612=1957%:%
-%:%1613=1958%:%
-%:%1614=1959%:%
-%:%1615=1960%:%
-%:%1616=1961%:%
-%:%1617=1962%:%
-%:%1618=1963%:%
-%:%1619=1964%:%
-%:%1620=1965%:%
-%:%1621=1966%:%
-%:%1622=1967%:%
-%:%1623=1968%:%
-%:%1624=1969%:%
-%:%1625=1970%:%
-%:%1626=1971%:%
-%:%1627=1972%:%
-%:%1628=1973%:%
-%:%1629=1974%:%
-%:%1630=1975%:%
-%:%1631=1976%:%
+%:%1512=1583%:%
+%:%1513=1584%:%
+%:%1514=1585%:%
+%:%1515=1586%:%
+%:%1516=1587%:%
+%:%1517=1588%:%
+%:%1518=1589%:%
+%:%1519=1590%:%
+%:%1520=1591%:%
+%:%1521=1592%:%
+%:%1522=1593%:%
+%:%1523=1594%:%
+%:%1524=1595%:%
+%:%1525=1596%:%
+%:%1526=1597%:%
+%:%1527=1598%:%
+%:%1528=1599%:%
+%:%1529=1600%:%
+%:%1530=1601%:%
+%:%1531=1602%:%
+%:%1532=1603%:%
+%:%1533=1604%:%
+%:%1534=1605%:%
+%:%1535=1606%:%
+%:%1536=1607%:%
+%:%1537=1608%:%
+%:%1538=1609%:%
+%:%1539=1610%:%
+%:%1540=1611%:%
+%:%1541=1612%:%
+%:%1542=1613%:%
+%:%1543=1614%:%
+%:%1544=1615%:%
+%:%1545=1616%:%
+%:%1545=1732%:%
+%:%1546=1733%:%
+%:%1547=1734%:%
+%:%1548=1735%:%
+%:%1549=1736%:%
+%:%1549=1897%:%
+%:%1550=1898%:%
+%:%1551=1899%:%
+%:%1552=1900%:%
+%:%1553=1901%:%
+%:%1554=1902%:%
+%:%1555=1903%:%
+%:%1556=1904%:%
+%:%1557=1905%:%
+%:%1558=1906%:%
+%:%1559=1907%:%
+%:%1560=1908%:%
+%:%1561=1909%:%
+%:%1562=1910%:%
+%:%1563=1911%:%
+%:%1564=1912%:%
+%:%1565=1913%:%
+%:%1566=1914%:%
+%:%1567=1915%:%
+%:%1568=1916%:%
+%:%1568=1917%:%
+%:%1569=1918%:%
+%:%1569=1919%:%
+%:%1569=1920%:%
+%:%1570=1921%:%
+%:%1570=1922%:%
+%:%1571=1923%:%
+%:%1572=1924%:%
+%:%1573=1925%:%
+%:%1574=1926%:%
+%:%1575=1927%:%
+%:%1576=1928%:%
+%:%1577=1929%:%
+%:%1578=1930%:%
+%:%1579=1931%:%
+%:%1580=1932%:%
+%:%1581=1933%:%
+%:%1582=1934%:%
+%:%1583=1935%:%
+%:%1584=1936%:%
+%:%1585=1937%:%
+%:%1586=1938%:%
+%:%1587=1939%:%
+%:%1587=1940%:%
+%:%1588=1941%:%
+%:%1589=1942%:%
+%:%1590=1943%:%
+%:%1590=1944%:%
+%:%1590=1945%:%
+%:%1591=1946%:%
+%:%1592=1947%:%
+%:%1593=1948%:%
+%:%1593=1949%:%
+%:%1594=1950%:%
+%:%1594=1951%:%
+%:%1595=1952%:%
+%:%1596=1953%:%
+%:%1597=1954%:%
+%:%1598=1955%:%
+%:%1599=1956%:%
+%:%1600=1957%:%
+%:%1601=1958%:%
+%:%1602=1959%:%
+%:%1603=1960%:%
+%:%1604=1961%:%
+%:%1605=1962%:%
+%:%1606=1963%:%
+%:%1607=1964%:%
+%:%1608=1965%:%
+%:%1609=1966%:%
+%:%1610=1967%:%
+%:%1611=1968%:%
+%:%1620=1973%:%
 %:%1632=1977%:%
 %:%1633=1978%:%
 %:%1634=1979%:%
@@ -3201,4 +3235,38 @@
 %:%1648=1993%:%
 %:%1649=1994%:%
 %:%1650=1995%:%
-%:%1663=2001%:%
\ No newline at end of file
+%:%1651=1996%:%
+%:%1652=1997%:%
+%:%1653=1998%:%
+%:%1654=1999%:%
+%:%1655=2000%:%
+%:%1656=2001%:%
+%:%1657=2002%:%
+%:%1658=2003%:%
+%:%1659=2004%:%
+%:%1660=2005%:%
+%:%1661=2006%:%
+%:%1662=2007%:%
+%:%1663=2008%:%
+%:%1664=2009%:%
+%:%1665=2010%:%
+%:%1666=2011%:%
+%:%1667=2012%:%
+%:%1668=2013%:%
+%:%1669=2014%:%
+%:%1670=2015%:%
+%:%1671=2016%:%
+%:%1672=2017%:%
+%:%1673=2018%:%
+%:%1674=2019%:%
+%:%1675=2020%:%
+%:%1676=2021%:%
+%:%1677=2022%:%
+%:%1678=2023%:%
+%:%1679=2024%:%
+%:%1680=2025%:%
+%:%1681=2026%:%
+%:%1682=2027%:%
+%:%1683=2028%:%
+%:%1684=2029%:%
+%:%1697=2035%:%
\ No newline at end of file
diff -r f65444d29e74 -r 78cc255e286f thys2/Journal/Paper.thy
--- a/thys2/Journal/Paper.thy	Tue Nov 02 13:57:59 2021 +0000
+++ b/thys2/Journal/Paper.thy	Tue Nov 02 19:42:52 2021 +0000
@@ -155,12 +155,42 @@
 
 However what is not certain is whether we can add simplification
 to the bit-coded algorithm, without breaking the correct lexing output.
+
+
+The reason that we do need to add a simplification phase
+after each derivative step of  $\textit{blexer}$ is
+because it produces intermediate
+regular expressions that can grow exponentially.
+For example, the regular expression $(a+aa)^*$ after taking
+derivative against just 10 $a$s will have size 8192.
+
+%TODO: add figure for this?
+
+\begin{lemma}
+@{thm blexer_simp_def}
+\end{lemma}
+
+
+\begin{center}
+  \begin{tabular}{lcl}
+  @{thm (lhs) bsimp.simps(1)[of  "bs" "r\<^sub>1" "r\<^sub>2"]} & $\dn$ & @{thm (rhs) bsimp.simps(1)[of  "bs" "r\<^sub>1" "r\<^sub>2"]}\\
+  @{thm (lhs) bsimp.simps(2)} & $\dn$ & @{thm (rhs) bsimp.simps(2)}\\
+  @{thm (lhs) bsimp.simps(3)} & $\dn$ & @{thm (rhs) bsimp.simps(3)}\\
+  @{thm (lhs) intern.simps(4)[of "r\<^sub>1" "r\<^sub>2"]} & $\dn$ & @{thm (rhs) intern.simps(4)[of "r\<^sub>1" "r\<^sub>2"]}\\
+\end{tabular}
+\end{center}
+
+
 This might sound trivial in the case of producing a YES/NO answer,
 but once we require a lexing output to be produced (which is required
 in applications like compiler front-end, malicious attack domain extraction, 
 etc.), it is not straightforward if we still extract what is needed according
 to the POSIX standard.
 
+
+
+
+
 By simplification, we mean specifically the following rules:
 
 \begin{center}
@@ -169,10 +199,10 @@
   @{thm[mode=Axiom] rrewrite.intros(2)[of "bs" "r\<^sub>1"]}\\
   @{thm[mode=Axiom] rrewrite.intros(3)[of  "bs" "bs\<^sub>1" "r\<^sub>1"]}\\
   @{thm[mode=Rule] rrewrite.intros(4)[of  "r\<^sub>1" "r\<^sub>2" "bs" "r\<^sub>3"]}\\
-  @{thm[mode=Rule] rrewrite.intros(5)[of "bs" "r\<^sub>2"]}\\
-  @{thm[mode=Rule] rrewrite.intros(6)[of "bs" "r\<^sub>1"]}\\
-  @{thm[mode=Axiom] rrewrite.intros(7)[of "bs" "r\<^sub>2"]}\\
-  @{thm[mode=Axiom] rrewrite.intros(8)[of "bs" "r\<^sub>1"]}\\
+  @{thm[mode=Rule] rrewrite.intros(5)[of "r\<^sub>3" "r\<^sub>4" "bs" "r\<^sub>1"]}\\
+  @{thm[mode=Rule] rrewrite.intros(6)[of "r" "r'" "bs" "rs\<^sub>1" "rs\<^sub>2"]}\\
+  @{thm[mode=Axiom] rrewrite.intros(7)[of "bs" "rs\<^sub>a" "rs\<^sub>b"]}\\
+  @{thm[mode=Axiom] rrewrite.intros(8)[of "bs" "rs\<^sub>a" "bs\<^sub>1" "rs\<^sub>1" "rs\<^sub>b"]}\\
   @{thm[mode=Axiom] rrewrite.intros(9)[of "bs" "r\<^sub>2"]}\\
   @{thm[mode=Axiom] rrewrite.intros(10)[of "bs" "r\<^sub>1"]}\\
   @{thm[mode=Axiom] rrewrite.intros(11)[of "bs" ]}\\
@@ -185,15 +215,6 @@
 
 And these can be made compact by the following simplification function:
 
-\begin{center}
-  \begin{tabular}{lcl}
-  @{thm (lhs) bsimp.simps(1)[of  "bs" "r\<^sub>1" "r\<^sub>2"]} & $\dn$ & @{thm (rhs) bsimp.simps(1)[of  "bs" "r\<^sub>1" "r\<^sub>2"]}\\
-  @{thm (lhs) bsimp.simps(2)} & $\dn$ & @{thm (rhs) bsimp.simps(2)}\\
-  @{thm (lhs) bsimp.simps(3)} & $\dn$ & @{thm (rhs) bsimp.simps(3)}\\
-  @{thm (lhs) intern.simps(4)[of "r\<^sub>1" "r\<^sub>2"]} & $\dn$ & @{thm (rhs) intern.simps(4)[of "r\<^sub>1" "r\<^sub>2"]}\\
-\end{tabular}
-\end{center}
-
 where the function $\mathit{bsimp_AALTs}$
 
 The core idea of the proof is that two regular expressions,
@@ -209,7 +230,7 @@
 correctness result: 
 if two (nullable) regular expressions are "rewritable" in many steps
 from one another, 
-then a call to function $textit{bmkeps}$ gives the same
+then a call to function $\textit{bmkeps}$ gives the same
 bit-sequence :
 \begin{lemma}
 @{thm [mode=IfThen] rewrites_bmkeps}
diff -r f65444d29e74 -r 78cc255e286f thys2/Journal/session_graph.pdf
Binary file thys2/Journal/session_graph.pdf has changed
diff -r f65444d29e74 -r 78cc255e286f thys2/journal.pdf
Binary file thys2/journal.pdf has changed