equal
deleted
inserted
replaced
742 an ``error'' iff the string is not in the language of the regular expression, |
742 an ``error'' iff the string is not in the language of the regular expression, |
743 and returning a unique POSIX value iff the string \emph{is} in the language): |
743 and returning a unique POSIX value iff the string \emph{is} in the language): |
744 |
744 |
745 \begin{theorem}\mbox{}\smallskip\\ |
745 \begin{theorem}\mbox{}\smallskip\\ |
746 \begin{tabular}{ll} |
746 \begin{tabular}{ll} |
747 (1) & @{thm (lhs) lex_correct1a} if and only if @{thm (rhs) lex_correct1a}\\ |
747 (1) & @{thm (lhs) lexer_correct_None} if and only if @{thm (rhs) lexer_correct_None}\\ |
748 (2) & @{thm (lhs) lex_correct3b} if and only if @{thm (rhs) lex_correct3b}\\ |
748 (2) & @{thm (lhs) lexer_correct_Some} if and only if @{thm (rhs) lexer_correct_Some}\\ |
749 \end{tabular} |
749 \end{tabular} |
750 \end{theorem} |
750 \end{theorem} |
751 |
751 |
752 \begin{proof} |
752 \begin{proof} |
753 By induction on @{term s} using Lem.~\ref{lemmkeps} and \ref{Posix2}.\qed |
753 By induction on @{term s} using Lem.~\ref{lemmkeps} and \ref{Posix2}.\qed |