equal
deleted
inserted
replaced
1264 %By unfolding the definitions and using Lemmas~\ref{lemtwo} and \ref{lemthree}. |
1264 %By unfolding the definitions and using Lemmas~\ref{lemtwo} and \ref{lemthree}. |
1265 %\end{proof} |
1265 %\end{proof} |
1266 |
1266 |
1267 \noindent |
1267 \noindent |
1268 This means that if the algorithm is called with a regular expression @{term r} and a string |
1268 This means that if the algorithm is called with a regular expression @{term r} and a string |
1269 @{term s} with $@{term s} \in L(@{term r})$, it will return @{term "Some v"} for the |
1269 @{term s} with $@{term s} \in L(@{term r})$, it will return @{term "Some v"} for the unique |
1270 @{term v} we defined by the POSIX relation $(@{term s}, @{term r}) \rightarrow @{term v}$; otherwise |
1270 @{term v} we defined by the POSIX relation $(@{term s}, @{term r}) \rightarrow @{term v}$; otherwise |
1271 the algorithm returns @{term "None"} when $s \not\in L(r)$ and no such @{text v} exists. |
1271 the algorithm returns @{term "None"} when $s \not\in L(r)$ and no such @{text v} exists. |
1272 This completes the correctness proof for the second POSIX lexing algorithm by Sulzmann and Lu. |
1272 This completes the correctness proof for the second POSIX lexing algorithm by Sulzmann and Lu. |
1273 The interesting point of this algorithm is that the sizes of derivatives do not grow arbitrarily big but |
1273 The interesting point of this algorithm is that the sizes of derivatives do not grow arbitrarily big but |
1274 can be finitely bounded, which |
1274 can be finitely bounded, which |