equal
deleted
inserted
replaced
789 |
789 |
790 \noindent In (2) we further know by Thm.~\ref{posixdeterm} that the |
790 \noindent In (2) we further know by Thm.~\ref{posixdeterm} that the |
791 value returned by the lexer must be unique. A simple corollary |
791 value returned by the lexer must be unique. A simple corollary |
792 of our two theorems is: |
792 of our two theorems is: |
793 |
793 |
794 \begin{corollary}\mbox{}\smallskip\\\label{lexercorrect} |
794 \begin{corollary}\mbox{}\smallskip\\\label{lexercorrectcor} |
795 \begin{tabular}{ll} |
795 \begin{tabular}{ll} |
796 (1) & @{thm (lhs) lexer_correctness(2)} if and only if @{thm (rhs) lexer_correctness(2)}\\ |
796 (1) & @{thm (lhs) lexer_correctness(2)} if and only if @{thm (rhs) lexer_correctness(2)}\\ |
797 (2) & @{thm (lhs) lexer_correctness(1)} if and only if @{thm (rhs) lexer_correctness(1)}\\ |
797 (2) & @{thm (lhs) lexer_correctness(1)} if and only if @{thm (rhs) lexer_correctness(1)}\\ |
798 \end{tabular} |
798 \end{tabular} |
799 \end{corollary} |
799 \end{corollary} |