--- a/etnms/etnms.aux	Thu Jan 09 22:21:04 2020 +0000
+++ b/etnms/etnms.aux	Fri Jan 10 13:03:37 2020 +0000
@@ -33,7 +33,7 @@
 \@writefile{toc}{\contentsline {section}{\numberline {2}The Algorithm by Brzozowski based on Derivatives of Regular Expressions}{6}{section.2}}
 \citation{Sulzmann2014}
 \newlabel{graph:*}{{1}{7}{The Algorithm by Brzozowski based on Derivatives of Regular Expressions}{equation.2.1}{}}
-\@writefile{toc}{\contentsline {section}{\numberline {3}Values and the Algorithm by Sulzmann and Lu}{7}{section.3}}
+\@writefile{toc}{\contentsline {section}{\numberline {3}Values and the Algorithm by Sulzmann and Lu}{8}{section.3}}
 \newlabel{graph:2}{{2}{8}{Values and the Algorithm by Sulzmann and Lu}{equation.3.2}{}}
 \citation{nielson11bcre}
 \citation{AusafDyckhoffUrban2016}

--- a/etnms/etnms.log	Thu Jan 09 22:21:04 2020 +0000
+++ b/etnms/etnms.log	Fri Jan 10 13:03:37 2020 +0000
@@ -1,4 +1,4 @@
-This is pdfTeX, Version 3.14159265-2.6-1.40.19 (TeX Live 2018) (preloaded format=pdflatex 2019.2.7)  9 JAN 2020 22:19
+This is pdfTeX, Version 3.14159265-2.6-1.40.19 (TeX Live 2018) (preloaded format=pdflatex 2019.2.7)  10 JAN 2020 13:02
 entering extended mode
  restricted \write18 enabled.
  file:line:error style messages enabled.
@@ -1119,27 +1119,27 @@
 (./etnms.aux)
 \openout1 = `etnms.aux'.
 
-LaTeX Font Info:    Checking defaults for OML/cmm/m/it on input line 76.
-LaTeX Font Info:    ... okay on input line 76.
-LaTeX Font Info:    Checking defaults for T1/cmr/m/n on input line 76.
-LaTeX Font Info:    ... okay on input line 76.
-LaTeX Font Info:    Checking defaults for OT1/cmr/m/n on input line 76.
-LaTeX Font Info:    ... okay on input line 76.
-LaTeX Font Info:    Checking defaults for OMS/cmsy/m/n on input line 76.
-LaTeX Font Info:    ... okay on input line 76.
-LaTeX Font Info:    Checking defaults for OMX/cmex/m/n on input line 76.
-LaTeX Font Info:    ... okay on input line 76.
-LaTeX Font Info:    Checking defaults for U/cmr/m/n on input line 76.
-LaTeX Font Info:    ... okay on input line 76.
-LaTeX Font Info:    Checking defaults for TS1/cmr/m/n on input line 76.
-LaTeX Font Info:    Try loading font information for TS1+cmr on input line 76.
+LaTeX Font Info:    Checking defaults for OML/cmm/m/it on input line 77.
+LaTeX Font Info:    ... okay on input line 77.
+LaTeX Font Info:    Checking defaults for T1/cmr/m/n on input line 77.
+LaTeX Font Info:    ... okay on input line 77.
+LaTeX Font Info:    Checking defaults for OT1/cmr/m/n on input line 77.
+LaTeX Font Info:    ... okay on input line 77.
+LaTeX Font Info:    Checking defaults for OMS/cmsy/m/n on input line 77.
+LaTeX Font Info:    ... okay on input line 77.
+LaTeX Font Info:    Checking defaults for OMX/cmex/m/n on input line 77.
+LaTeX Font Info:    ... okay on input line 77.
+LaTeX Font Info:    Checking defaults for U/cmr/m/n on input line 77.
+LaTeX Font Info:    ... okay on input line 77.
+LaTeX Font Info:    Checking defaults for TS1/cmr/m/n on input line 77.
+LaTeX Font Info:    Try loading font information for TS1+cmr on input line 77.
  (/usr/local/texlive/2018/texmf-dist/tex/latex/base/ts1cmr.fd
 File: ts1cmr.fd 2014/09/29 v2.5h Standard LaTeX font definitions
 )
-LaTeX Font Info:    ... okay on input line 76.
-LaTeX Font Info:    Checking defaults for PD1/pdf/m/n on input line 76.
-LaTeX Font Info:    ... okay on input line 76.
-LaTeX Font Info:    Try loading font information for T1+lmr on input line 76.
+LaTeX Font Info:    ... okay on input line 77.
+LaTeX Font Info:    Checking defaults for PD1/pdf/m/n on input line 77.
+LaTeX Font Info:    ... okay on input line 77.
+LaTeX Font Info:    Try loading font information for T1+lmr on input line 77.
 
 (/usr/local/texlive/2018/texmf-dist/tex/latex/lm/t1lmr.fd
 File: t1lmr.fd 2009/10/30 v1.6 Font defs for Latin Modern
@@ -1177,9 +1177,9 @@
 \c@lstlisting=\count176
 Package lastpage Info: Please have a look at the pageslts package at
 (lastpage)             https://www.ctan.org/pkg/pageslts
-(lastpage)             ! on input line 76.
+(lastpage)             ! on input line 77.
 \AtBeginShipoutBox=\box48
-Package hyperref Info: Link coloring ON on input line 76.
+Package hyperref Info: Link coloring ON on input line 77.
 
 (/usr/local/texlive/2018/texmf-dist/tex/latex/hyperref/nameref.sty
 Package: nameref 2016/05/21 v2.44 Cross-referencing by name of section
@@ -1189,9 +1189,9 @@
 )
 \c@section@level=\count177
 )
-LaTeX Info: Redefining \ref on input line 76.
-LaTeX Info: Redefining \pageref on input line 76.
-LaTeX Info: Redefining \nameref on input line 76.
+LaTeX Info: Redefining \ref on input line 77.
+LaTeX Info: Redefining \pageref on input line 77.
+LaTeX Info: Redefining \nameref on input line 77.
 
 (./etnms.out) (./etnms.out)
 \@outlinefile=\write5
@@ -1206,92 +1206,96 @@
 Package pgfplots Warning: running in backwards compatibility mode (unsuitable t
 ick labels; missing features). Consider writing \pgfplotsset{compat=1.16} into 
 your preamble.
- on input line 76.
+ on input line 77.
 
-LaTeX Font Info:    Try loading font information for T1+lmss on input line 78.
+LaTeX Font Info:    Try loading font information for T1+lmss on input line 79.
 (/usr/local/texlive/2018/texmf-dist/tex/latex/lm/t1lmss.fd
 File: t1lmss.fd 2009/10/30 v1.6 Font defs for Latin Modern
 )
-LaTeX Font Info:    Try loading font information for OT1+lmr on input line 78.
+LaTeX Font Info:    Try loading font information for OT1+lmr on input line 79.
 
 (/usr/local/texlive/2018/texmf-dist/tex/latex/lm/ot1lmr.fd
 File: ot1lmr.fd 2009/10/30 v1.6 Font defs for Latin Modern
 )
-LaTeX Font Info:    Try loading font information for OML+lmm on input line 78.
+LaTeX Font Info:    Try loading font information for OML+lmm on input line 79.
 
 (/usr/local/texlive/2018/texmf-dist/tex/latex/lm/omllmm.fd
 File: omllmm.fd 2009/10/30 v1.6 Font defs for Latin Modern
 )
-LaTeX Font Info:    Try loading font information for OMS+lmsy on input line 78.
+LaTeX Font Info:    Try loading font information for OMS+lmsy on input line 79.
 
 
 (/usr/local/texlive/2018/texmf-dist/tex/latex/lm/omslmsy.fd
 File: omslmsy.fd 2009/10/30 v1.6 Font defs for Latin Modern
 )
-LaTeX Font Info:    Try loading font information for OMX+lmex on input line 78.
+LaTeX Font Info:    Try loading font information for OMX+lmex on input line 79.
 
 
 (/usr/local/texlive/2018/texmf-dist/tex/latex/lm/omxlmex.fd
 File: omxlmex.fd 2009/10/30 v1.6 Font defs for Latin Modern
 )
 LaTeX Font Info:    External font `lmex10' loaded for size
-(Font)              <10> on input line 78.
+(Font)              <10> on input line 79.
 LaTeX Font Info:    External font `lmex10' loaded for size
-(Font)              <7> on input line 78.
+(Font)              <7> on input line 79.
 LaTeX Font Info:    External font `lmex10' loaded for size
-(Font)              <5> on input line 78.
-LaTeX Font Info:    Try loading font information for U+msa on input line 78.
+(Font)              <5> on input line 79.
+LaTeX Font Info:    Try loading font information for U+msa on input line 79.
 
 (/usr/local/texlive/2018/texmf-dist/tex/latex/amsfonts/umsa.fd
 File: umsa.fd 2013/01/14 v3.01 AMS symbols A
 )
-LaTeX Font Info:    Try loading font information for U+msb on input line 78.
+LaTeX Font Info:    Try loading font information for U+msb on input line 79.
 
 (/usr/local/texlive/2018/texmf-dist/tex/latex/amsfonts/umsb.fd
 File: umsb.fd 2013/01/14 v3.01 AMS symbols B
 )
-LaTeX Font Info:    Try loading font information for T1+lmtt on input line 78.
+LaTeX Font Info:    Try loading font information for T1+lmtt on input line 79.
 
 (/usr/local/texlive/2018/texmf-dist/tex/latex/lm/t1lmtt.fd
 File: t1lmtt.fd 2009/10/30 v1.6 Font defs for Latin Modern
 )
 LaTeX Font Info:    Font shape `T1/lmtt/bx/n' in size <9.5> not available
-(Font)              Font shape `T1/lmtt/b/n' tried instead on input line 78.
+(Font)              Font shape `T1/lmtt/b/n' tried instead on input line 79.
 \openout3 = `etnms.vtc'.
 
 LaTeX Font Info:    External font `lmex10' loaded for size
-(Font)              <9> on input line 112.
+(Font)              <9> on input line 113.
 LaTeX Font Info:    External font `lmex10' loaded for size
-(Font)              <6> on input line 112.
+(Font)              <6> on input line 113.
 
-Underfull \hbox (badness 10000) in paragraph at lines 136--138
+Underfull \hbox (badness 10000) in paragraph at lines 137--139
 
  []
 
-<cc-by.pdf, id=32, 88.33pt x 31.11626pt>
+
+LaTeX Warning: Citation `AusafDyckhoffUrban2016' on page 1 undefined on input l
+ine 152.
+
+<cc-by.pdf, id=7, 88.33pt x 31.11626pt>
 File: cc-by.pdf Graphic file (type pdf)
 <use cc-by.pdf>
-Package pdftex.def Info: cc-by.pdf  used on input line 156.
+Package pdftex.def Info: cc-by.pdf  used on input line 157.
 (pdftex.def)             Requested size: 39.74274pt x 14.0pt.
-LaTeX Font Info:    Try loading font information for TS1+lmr on input line 156.
+LaTeX Font Info:    Try loading font information for TS1+lmr on input line 157.
 
 (/usr/local/texlive/2018/texmf-dist/tex/latex/lm/ts1lmr.fd
 File: ts1lmr.fd 2009/10/30 v1.6 Font defs for Latin Modern
 )
-<lipics-logo-bw.pdf, id=35, 591.44762pt x 144.42657pt>
+<lipics-logo-bw.pdf, id=10, 591.44762pt x 144.42657pt>
 File: lipics-logo-bw.pdf Graphic file (type pdf)
 <use lipics-logo-bw.pdf>
-Package pdftex.def Info: lipics-logo-bw.pdf  used on input line 156.
+Package pdftex.def Info: lipics-logo-bw.pdf  used on input line 157.
 (pdftex.def)             Requested size: 64.00354pt x 14.0pt.
  [1
 
 {/usr/local/texlive/2018/texmf-var/fonts/map/pdftex/updmap/pdftex.map} <./cc-by
 .pdf> <./lipics-logo-bw.pdf>]
 
-LaTeX Warning: Command \textbar invalid in math mode on input line 202.
+LaTeX Warning: Command \textbar invalid in math mode on input line 203.
 
 
-Overfull \hbox (44.9729pt too wide) in paragraph at lines 219--223
+Overfull \hbox (44.9729pt too wide) in paragraph at lines 220--224
 \T1/lmr/m/n/10 By us-ing a prop-erty of re-trieve we have the $[]$ of the above
  equal-ity is $\OML/lmm/m/it/10 decode\OT1/lmr/m/n/10 (\OML/lmm/m/it/10 retriev
 e\OT1/lmr/m/n/10 (\OML/lmm/m/it/10 r[]\OMS/lmsy/m/n/10 n\OT1/lmr/m/n/10 (\OML/l
@@ -1300,7 +1304,7 @@
  []
 
 
-Overfull \hbox (84.166pt too wide) in paragraph at lines 240--255
+Overfull \hbox (84.166pt too wide) in paragraph at lines 241--262
 \T1/lmr/m/n/10 equal-it-ies, $[] \OML/lmm/m/it/10 a v$ \T1/lmr/m/n/10 is not al
 -ways defined. for ex-ample, $[] []\OT1/lmr/m/n/10 (\OML/lmm/m/it/10 Z; []\OT1/
 lmr/m/n/10 (\OML/lmm/m/it/10 S\OT1/lmr/m/n/10 )\OML/lmm/m/it/10 ; []\OT1/lmr/m/
@@ -1308,12 +1312,12 @@
  []
 
 [2]
-Underfull \hbox (badness 10000) in paragraph at lines 265--271
+Underfull \hbox (badness 10000) in paragraph at lines 279--284
 
  []
 
 
-Overfull \hbox (67.75871pt too wide) in paragraph at lines 275--290
+Overfull \hbox (67.75871pt too wide) in paragraph at lines 288--303
 []\T1/lmr/m/n/10 we used re-trieve for the key in-duc-tion: $\OML/lmm/m/it/10 d
 ecode\OT1/lmr/m/n/10 (\OML/lmm/m/it/10 retrieve\OT1/lmr/m/n/10 (\OML/lmm/m/it/1
 0 r\OMS/lmsy/m/n/10 n\OT1/lmr/m/n/10 (\OML/lmm/m/it/10 s\OT1/lmr/m/n/10 @[\OML/
@@ -1325,36 +1329,106 @@
  []
 
 [3]
-Underfull \hbox (badness 10000) in paragraph at lines 400--403
+Underfull \hbox (badness 10000) in paragraph at lines 413--416
 
  []
 
+
+Underfull \vbox (badness 1881) has occurred while \output is active []
+
+ [4]
 PGFPlots: reading {re-js.data}
 PGFPlots: reading {re-python2.data}
 PGFPlots: reading {re-java.data}
 
-Overfull \hbox (2.08597pt too wide) in paragraph at lines 427--493
+Overfull \hbox (2.08597pt too wide) in paragraph at lines 440--506
  [] 
  []
 
 
-Underfull \vbox (badness 10000) has occurred while \output is active []
+LaTeX Warning: Citation `Davis18' on page 5 undefined on input line 520.
+
+
+LaTeX Warning: Citation `17Bir' on page 5 undefined on input line 521.
 
- [4]
-LaTeX Font Info:    Calculating math sizes for size <8.5> on input line 516.
+LaTeX Font Info:    Calculating math sizes for size <8.5> on input line 529.
+LaTeX Font Info:    External font `lmex10' loaded for size
+(Font)              <8.5> on input line 529.
+LaTeX Font Info:    External font `lmex10' loaded for size
+(Font)              <5.94997> on input line 529.
 LaTeX Font Info:    External font `lmex10' loaded for size
-(Font)              <8.5> on input line 516.
-LaTeX Font Info:    External font `lmex10' loaded for size
-(Font)              <5.94997> on input line 516.
-LaTeX Font Info:    External font `lmex10' loaded for size
-(Font)              <4.25> on input line 516.
+(Font)              <4.25> on input line 529.
+[5]
+
+LaTeX Warning: Citation `AusafDyckhoffUrban2016' on page 6 undefined on input l
+ine 577.
+
+
+LaTeX Warning: Citation `OkuiSuzuki2010' on page 6 undefined on input line 577.
+
+
+
+LaTeX Warning: Citation `Vansummeren2006' on page 6 undefined on input line 577
+.
+
+
+LaTeX Warning: Citation `Sulzmann2014' on page 6 undefined on input line 578.
+
+
+LaTeX Warning: Citation `AusafDyckhoffUrban2016' on page 6 undefined on input l
+ine 580.
+
 
-[5] [6] [7] [8]
+LaTeX Warning: Citation `CrashCourse2014' on page 6 undefined on input line 585
+.
+
+
+LaTeX Warning: Citation `Kuklewicz' on page 6 undefined on input line 595.
+
+
+LaTeX Warning: Citation `Sulzmann2014' on page 6 undefined on input line 600.
+
+
+LaTeX Warning: Citation `Brzozowski1964' on page 6 undefined on input line 602.
+
+
+[6]
+
+LaTeX Warning: Citation `Sulzmann2014' on page 7 undefined on input line 722.
+
+[7]
+
+LaTeX Warning: Reference `graph:*' on page 8 undefined on input line 800.
+
+[8] [9]
 
 Package amsfonts Warning: Obsolete command \bold; \mathbf should be used instea
-d on input line 884.
+d on input line 897.
+
+[10]
+
+LaTeX Warning: Citation `nielson11bcre' on page 11 undefined on input line 1053
+.
+
+[11]
+
+LaTeX Warning: Citation `AusafDyckhoffUrban2016' on page 12 undefined on input 
+line 1079.
+
 
-[9] [10] [11] [12] [13] [14] [15] [16] [17]
+LaTeX Warning: Citation `Antimirov95' on page 12 undefined on input line 1087.
+
+[12]
+
+LaTeX Warning: Citation `Sulzmann2014' on page 13 undefined on input line 1206.
+
+
+[13] [14] [15]
+
+LaTeX Warning: Citation `Sulzmann2014' on page 16 undefined on input line 1480.
+
+
+[16] [17]
 PGFPlots: reading {bad-scala.data}
 PGFPlots: reading {good-java.data}
  [18] (./etnms.bbl
@@ -1367,23 +1441,40 @@
 (Font)              <4.75> on input line 38.
  [19])
 
+Package lastpage Warning: Rerun to get the references right on input line 1714.
+
+
+
 AED: lastpage setting LastPage
 [20]
-Package atveryend Info: Empty hook `BeforeClearDocument' on input line 1701.
-Package atveryend Info: Empty hook `AfterLastShipout' on input line 1701.
+Package atveryend Info: Empty hook `BeforeClearDocument' on input line 1714.
+Package atveryend Info: Empty hook `AfterLastShipout' on input line 1714.
  (./etnms.aux)
-Package atveryend Info: Executing hook `AtVeryEndDocument' on input line 1701.
-Package atveryend Info: Executing hook `AtEndAfterFileList' on input line 1701.
+Package atveryend Info: Executing hook `AtVeryEndDocument' on input line 1714.
+Package atveryend Info: Executing hook `AtEndAfterFileList' on input line 1714.
+
+
+
+Package rerunfilecheck Warning: File `etnms.out' has changed.
+(rerunfilecheck)                Rerun to get outlines right
+(rerunfilecheck)                or use package `bookmark'.
 
-Package rerunfilecheck Info: File `etnms.out' has not changed.
-(rerunfilecheck)             Checksum: 43E8D84961F15C811B4165A2AF60EF5A;395.
-Package atveryend Info: Empty hook `AtVeryVeryEnd' on input line 1701.
+Package rerunfilecheck Info: Checksums for `etnms.out':
+(rerunfilecheck)             Before: D41D8CD98F00B204E9800998ECF8427E;0
+(rerunfilecheck)             After:  43E8D84961F15C811B4165A2AF60EF5A;395.
+
+LaTeX Warning: There were undefined references.
+
+
+LaTeX Warning: Label(s) may have changed. Rerun to get cross-references right.
+
+Package atveryend Info: Empty hook `AtVeryVeryEnd' on input line 1714.
  ) 
 Here is how much of TeX's memory you used:
- 32731 strings out of 492649
- 760798 string characters out of 6129623
- 948443 words of memory out of 5000000
- 35948 multiletter control sequences out of 15000+600000
+ 32725 strings out of 492649
+ 760734 string characters out of 6129623
+ 946443 words of memory out of 5000000
+ 35942 multiletter control sequences out of 15000+600000
  218552 words of font info for 126 fonts, out of 8000000 for 9000
  1141 hyphenation exceptions out of 8191
  69i,24n,107p,719b,2460s stack positions out of 5000i,500n,10000p,200000b,80000s
@@ -1415,10 +1506,10 @@
 /usr/local/texlive/2018/texmf-dist/fonts/type1/public/lm/lmtk10.pfb></usr/local
 /texlive/2018/texmf-dist/fonts/type1/public/lm/lmtt10.pfb></usr/local/texlive/2
 018/texmf-dist/fonts/type1/public/lm/lmtt9.pfb>
-Output written on etnms.pdf (20 pages, 555273 bytes).
+Output written on etnms.pdf (20 pages, 554160 bytes).
 PDF statistics:
- 317 PDF objects out of 1000 (max. 8388607)
- 258 compressed objects within 3 object streams
+ 279 PDF objects out of 1000 (max. 8388607)
+ 220 compressed objects within 3 object streams
  42 named destinations out of 1000 (max. 500000)
- 77 words of extra memory for PDF output out of 10000 (max. 10000000)
+ 29 words of extra memory for PDF output out of 10000 (max. 10000000)
 

Binary file etnms/etnms.pdf has changed

Binary file etnms/etnms.synctex.gz has changed

--- a/etnms/etnms.tex	Thu Jan 09 22:21:04 2020 +0000
+++ b/etnms/etnms.tex	Fri Jan 10 13:03:37 2020 +0000
@@ -37,6 +37,7 @@
 \def\lexer{\mathit{lexer}}
 \def\blexer{\textit{blexer}}
 \def\blexers{\mathit{blexer\_simp}}
+\def\simp{\mathit{simp}}
 \def\mkeps{\mathit{mkeps}}
 \def\bmkeps{\textit{bmkeps}}
 \def\inj{\mathit{inj}}
@@ -250,6 +251,12 @@
 is defined, but not $\retrieve \; \AONE(\Z\S) \; \Left(\Empty)$,
 though we can extract the same POSIX
 bits from the two annotated regular expressions.
+The latter might occur when we try to retrieve from 
+a simplified regular expression using the same value
+as the unsimplified one.
+This is because $\Left(\Empty)$ corresponds to
+the regular expression structure $\AALTS$ instead of
+$\AONE$, this v
 That means, if we 
 want to prove that 
 \begin{center}
@@ -265,6 +272,11 @@
 \noindent
 we would need to rectify the value $\mkeps(r\backslash s)$ into something simpler
 to make the retrieve function defined.\\
+One way to do this is to prove the following:
+\begin{center}
+$\retrieve \; \rup\backslash_{simp} s \; \mkeps(\simp(r\backslash s))=\textit{retrieve} \; \rup\backslash s \; \mkeps(r\backslash s)$
+\end{center}
+\noindent
 %HERE CONSTRUCTION SITE
 The vsimp function, defined as follows
 tries to simplify the value in lockstep with