diff -r 0c666a0c57d7 -r aef235b965bb thys2/Journal/root.aux
--- a/thys2/Journal/root.aux	Fri Jan 07 22:25:26 2022 +0000
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,96 +0,0 @@
-\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}