diff -r 56781ad291cf -r e00950ba4514 thys2/Journal/root.aux
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/thys2/Journal/root.aux	Mon Nov 01 10:40:21 2021 +0000
@@ -0,0 +1,96 @@
+\relax 
+\providecommand\hyper@newdestlabel[2]{}
+\providecommand\HyperFirstAtBeginDocument{\AtBeginDocument}
+\HyperFirstAtBeginDocument{\ifx\hyper@anchor\@undefined
+\global\let\oldcontentsline\contentsline
+\gdef\contentsline#1#2#3#4{\oldcontentsline{#1}{#2}{#3}}
+\global\let\oldnewlabel\newlabel
+\gdef\newlabel#1#2{\newlabelxx{#1}#2}
+\gdef\newlabelxx#1#2#3#4#5#6{\oldnewlabel{#1}{{#2}{#3}}}
+\AtEndDocument{\ifx\hyper@anchor\@undefined
+\let\contentsline\oldcontentsline
+\let\newlabel\oldnewlabel
+\fi}
+\fi}
+\global\let\hyper@last\relax 
+\gdef\HyperFirstAtBeginDocument#1{#1}
+\providecommand\HyField@AuxAddToFields[1]{}
+\providecommand\HyField@AuxAddToCoFields[2]{}
+\citation{AusafDyckhoffUrban2016}
+\citation{OkuiSuzuki2010,OkuiSuzukiTech}
+\citation{Sulzmann2014}
+\@writefile{toc}{\contentsline {section}{\numberline {1}Bit-Encodings}{2}{section.1.1}}
+\@writefile{toc}{\contentsline {section}{\numberline {2}Annotated Regular Expressions}{3}{section.1.2}}
+\citation{Brzozowski1964}
+\citation{Owens2008}
+\citation{Krauss2011}
+\citation{Coquand2012}
+\@writefile{toc}{\contentsline {section}{\numberline {3}Introduction}{41}{section.1.3}}
+\citation{Frisch2004}
+\citation{POSIX,Kuklewicz,OkuiSuzuki2010,Sulzmann2014,Vansummeren2006}
+\citation{POSIX}
+\citation{Sulzmann2014}
+\citation{HosoyaVouillonPierce2005}
+\citation{Sulzmann2014}
+\citation{Frisch2004}
+\citation{Sulzmann2014}
+\citation{Kuklewicz}
+\citation{Sulzmann2014}
+\citation{CrashCourse2014}
+\citation{Sulzmann2014}
+\citation{Vansummeren2006}
+\citation{Sulzmann2014}
+\citation{Sulzmann2014}
+\citation{OkuiSuzuki2010}
+\@writefile{toc}{\contentsline {section}{\numberline {4}Preliminaries}{44}{section.1.4}}
+\citation{Krauss2011}
+\citation{Brzozowski1964}
+\newlabel{SemDer}{{1}{45}{Preliminaries}{equation.1.4.1}{}}
+\citation{Sulzmann2014}
+\citation{Sulzmann2014}
+\citation{Frisch2004}
+\citation{Sulzmann2014}
+\citation{AusafDyckhoffUrban2016}
+\newlabel{derprop}{{1}{46}{Preliminaries}{proposition.1.1}{}}
+\newlabel{posixsec}{{5}{46}{POSIX Regular Expression Matching}{section.1.5}{}}
+\@writefile{toc}{\contentsline {section}{\numberline {5}POSIX Regular Expression Matching}{46}{section.1.5}}
+\citation{OkuiSuzuki2010}
+\citation{Frisch2004}
+\citation{Sulzmann2014}
+\citation{Sulzmann2014}
+\newlabel{prfintros}{{5}{47}{POSIX Regular Expression Matching}{section.1.5}{}}
+\newlabel{inhabs}{{2}{47}{POSIX Regular Expression Matching}{proposition.1.2}{}}
+\citation{Sulzmann2014}
+\@writefile{lof}{\contentsline {figure}{\numberline {1}{\ignorespaces The two phases of the algorithm by Sulzmann \& Lu \cite  {Sulzmann2014}, matching the string \emph  {\sfcode 42 1000 \sfcode 63 1000 \sfcode 33 1000 \sfcode 58 1000 \sfcode 59 1000 \sfcode 44 1000 \it  {\emph  {$[$}}{\kern 0pt}a{\emph  {$\mathord ,$}}{\kern 0pt}\ b{\emph  {$\mathord ,$}}{\kern 0pt}\ c{\emph  {$]$}}{\kern 0pt}}. The first phase (the arrows from left to right) is Brzozowski's matcher building successive derivatives. If the last regular expression is \emph  {\sfcode 42 1000 \sfcode 63 1000 \sfcode 33 1000 \sfcode 58 1000 \sfcode 59 1000 \sfcode 44 1000 \it  nullable}, then the functions of the second phase are called (the top-down and right-to-left arrows): first \emph  {\sfcode 42 1000 \sfcode 63 1000 \sfcode 33 1000 \sfcode 58 1000 \sfcode 59 1000 \sfcode 44 1000 \it  mkeps} calculates a value \emph  {\sfcode 42 1000 \sfcode 63 1000 \sfcode 33 1000 \sfcode 58 1000 \sfcode 59 1000 \sfcode 44 1000 \it  v\emph  {\isascriptstyle  ${}\sb {4}$}} witnessing how the empty string has been recognised by \emph  {\sfcode 42 1000 \sfcode 63 1000 \sfcode 33 1000 \sfcode 58 1000 \sfcode 59 1000 \sfcode 44 1000 \it  r\emph  {\isascriptstyle  ${}\sb {4}$}}. After that the function \emph  {\sfcode 42 1000 \sfcode 63 1000 \sfcode 33 1000 \sfcode 58 1000 \sfcode 59 1000 \sfcode 44 1000 \it  inj} ``injects back'' the characters of the string into the values. }}{48}{figure.1.1}}
+\newlabel{Sulz}{{1}{48}{The two phases of the algorithm by Sulzmann \& Lu \cite {Sulzmann2014}, matching the string \isa {{\isacharbrackleft }{\kern 0pt}a{\isacharcomma }{\kern 0pt}\ b{\isacharcomma }{\kern 0pt}\ c{\isacharbrackright }{\kern 0pt}}. The first phase (the arrows from left to right) is \Brz 's matcher building successive derivatives. If the last regular expression is \isa {nullable}, then the functions of the second phase are called (the top-down and right-to-left arrows): first \isa {mkeps} calculates a value \isa {v\isactrlsub {\isadigit {4}}} witnessing how the empty string has been recognised by \isa {r\isactrlsub {\isadigit {4}}}. After that the function \isa {inj} ``injects back'' the characters of the string into the values}{figure.1.1}{}}
+\newlabel{Prf_injval_flat}{{2}{49}{POSIX Regular Expression Matching}{lemma.1.2}{}}
+\citation{Sulzmann2014}
+\citation{Vansummeren2006}
+\newlabel{posixdeterm}{{1}{50}{POSIX Regular Expression Matching}{theorem.1.5.1}{}}
+\@writefile{lof}{\contentsline {figure}{\numberline {2}{\ignorespaces Our inductive definition of POSIX values.}}{51}{figure.1.2}}
+\newlabel{POSIXrules}{{2}{51}{Our inductive definition of POSIX values}{figure.1.2}{}}
+\newlabel{LVposix}{{3}{51}{POSIX Regular Expression Matching}{lemma.1.3}{}}
+\newlabel{lemmkeps}{{4}{51}{POSIX Regular Expression Matching}{lemma.1.4}{}}
+\newlabel{Posix2}{{5}{52}{POSIX Regular Expression Matching}{lemma.1.5}{}}
+\newlabel{lexercorrect}{{2}{52}{POSIX Regular Expression Matching}{theorem.1.5.2}{}}
+\citation{Sulzmann2014}
+\citation{Sulzmann2014}
+\citation{OkuiSuzuki2010,OkuiSuzukiTech}
+\newlabel{lexercorrectcor}{{1}{53}{POSIX Regular Expression Matching}{corollary.1.1}{}}
+\@writefile{toc}{\contentsline {section}{\numberline {6}Ordering of Values according to Okui and Suzuki}{53}{section.1.6}}
+\citation{OkuiSuzuki2010}
+\citation{OkuiSuzuki2010}
+\citation{OkuiSuzuki2010}
+\newlabel{transitivity}{{6}{55}{Ordering of Values according to Okui and Suzuki}{lemma.1.6}{}}
+\newlabel{ordlen}{{4}{56}{Ordering of Values according to Okui and Suzuki}{proposition.1.4}{}}
+\newlabel{ordintros}{{5}{56}{Ordering of Values according to Okui and Suzuki}{proposition.1.5}{}}
+\newlabel{orderone}{{3}{56}{Ordering of Values according to Okui and Suzuki}{theorem.1.6.3}{}}
+\citation{Sulzmann2014}
+\citation{Sulzmann2014}
+\@writefile{toc}{\contentsline {section}{\numberline {7}Bitcoded Lexing}{58}{section.1.7}}
+\@writefile{toc}{\contentsline {section}{\numberline {8}Optimisations}{58}{section.1.8}}
+\newlabel{Simpl}{{2}{58}{Optimisations}{equation.1.8.2}{}}
+\newlabel{slexeraux}{{7}{63}{Optimisations}{lemma.1.7}{}}
+\@writefile{toc}{\contentsline {section}{\numberline {9}HERE}{64}{section.1.9}}
+\bibstyle{plain}
+\bibdata{root}