equal
deleted
inserted
replaced
1381 \] |
1381 \] |
1382 do not to contribute a POSIX lexical value, |
1382 do not to contribute a POSIX lexical value, |
1383 and therefore can be thrown away. |
1383 and therefore can be thrown away. |
1384 |
1384 |
1385 Ausaf et al. \cite{AusafDyckhoffUrban2016} |
1385 Ausaf et al. \cite{AusafDyckhoffUrban2016} |
1386 have come up with some simplification steps, however those steps |
1386 have come up with some simplification steps, |
|
1387 and incorporated the simplification into $\lexer$. |
|
1388 They call this lexer $\textit{lexer}_{simp}$ and proved that |
|
1389 \[ |
|
1390 \lexer \; r\; s = \textit{lexer}_{simp} \; r \; s |
|
1391 \] |
|
1392 The function $\textit{lexer}_{simp}$ |
|
1393 involves some fiddly manipulation of value rectification, |
|
1394 which we omit here. |
|
1395 however those steps |
1387 are not yet sufficiently strong, to achieve the above effects. |
1396 are not yet sufficiently strong, to achieve the above effects. |
1388 And even with these relatively mild simplifications, the proof |
1397 And even with these relatively mild simplifications, the proof |
1389 is already quite a bit more complicated than the theorem \ref{lexerCorrectness}. |
1398 is already quite a bit more complicated than the theorem \ref{lexerCorrectness}. |
1390 One would need to prove something like this: |
1399 One would need to prove something like this: |
1391 \[ |
1400 \[ |