equal
deleted
inserted
replaced
1353 |
1353 |
1354 \noindent This theorem shows that our @{text POSIX} value for a |
1354 \noindent This theorem shows that our @{text POSIX} value for a |
1355 regular expression @{text r} and string @{term s} is in fact a |
1355 regular expression @{text r} and string @{term s} is in fact a |
1356 minimal element of the values in @{text "LV r s"}. By |
1356 minimal element of the values in @{text "LV r s"}. By |
1357 Proposition~\ref{ordlen}\textit{(2)} we also know that any value in |
1357 Proposition~\ref{ordlen}\textit{(2)} we also know that any value in |
1358 @{text "LV s' r"}, with @{term "s'"} being a strict prefix, cannot be |
1358 @{text "LV r s'"}, with @{term "s'"} being a strict prefix, cannot be |
1359 smaller than @{text "v\<^sub>1"}. The next theorem shows the |
1359 smaller than @{text "v\<^sub>1"}. The next theorem shows the |
1360 opposite---namely any minimal element in @{term "LV r s"} must be a |
1360 opposite---namely any minimal element in @{term "LV r s"} must be a |
1361 @{text POSIX} value. This can be established by induction on @{text |
1361 @{text POSIX} value. This can be established by induction on @{text |
1362 r}, but the proof can be drastically simplified by using the fact |
1362 r}, but the proof can be drastically simplified by using the fact |
1363 from the previous section about the existence of a @{text POSIX} value |
1363 from the previous section about the existence of a @{text POSIX} value |