48   but not equivalent with, the

    48   but not equivalent with, the

    49   definition given by Sulzmann and Lu~\cite{Sulzmann2014}.

    49   definition given by Sulzmann and Lu~\cite{Sulzmann2014}.

    50   The advantage of the definition based on the

    50   The advantage of the definition based on the

    51   ordering is that it implements more directly the informal rules from the

    51   ordering is that it implements more directly the informal rules from the

    52   POSIX standard.

    52   POSIX standard.

    55   expressions.}  \renewcommand{\thefootnote}{\arabic{footnote}}

    55   expressions.}  \renewcommand{\thefootnote}{\arabic{footnote}}

    56 

    56 

    57 

    57 

    58 \title{POSIX {L}exing with {D}erivatives of {R}egular {E}xpressions}

    58 \title{POSIX {L}exing with {D}erivatives of {R}egular {E}xpressions}

    59 \author{Fahad Ausaf\inst{1} \and Roy Dyckhoff\inst{2} \and Christian Urban\inst{3}}

    59 \author{Fahad Ausaf\inst{1} \and Roy Dyckhoff\inst{2} \and Christian Urban\inst{3}}

    80 algorithm always generates such a value (provided that the regular

    80 algorithm always generates such a value (provided that the regular

    81 expression matches the string). We show that $(iii)$ our inductive

    81 expression matches the string). We show that $(iii)$ our inductive

    82 definition of a POSIX value is equivalent to an alternative definition

    82 definition of a POSIX value is equivalent to an alternative definition

    83 by Okui and Suzuki which identifies POSIX values as least elements

    83 by Okui and Suzuki which identifies POSIX values as least elements

    84 according to an ordering of values.  We also prove the correctness of

    84 according to an ordering of values.  We also prove the correctness of

    86 results to additional constructors for regular expressions.  \smallskip

    86 results to additional constructors for regular expressions.  \smallskip

    87 

    87 

    88 {\bf Keywords:} POSIX matching, Derivatives of Regular Expressions,

    88 {\bf Keywords:} POSIX matching, Derivatives of Regular Expressions,

    89 Isabelle/HOL

    89 Isabelle/HOL

    90 \end{abstract}

    90 \end{abstract}