thys3/Paper.thy
changeset 498 ab626b60ee64
parent 496 f493a20feeb3
child 499 6a100d32314c
equal deleted inserted replaced
497:04b5e904a220 498:ab626b60ee64
  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