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 

    87 

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

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

    88 Isabelle/HOL

    89 Isabelle/HOL

    89 \end{abstract}

    90 \end{abstract}

    90 

    91