\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}