| changeset 271 | f46ebc84408d |
| parent 270 | 462d893ecb3d |
| child 272 | f16019b11179 |
| 270:462d893ecb3d | 271:f46ebc84408d |
|---|---|
1275 |
1275 |
1276 |
1276 |
1277 \end{itemize} |
1277 \end{itemize} |
1278 |
1278 |
1279 \end{proof} |
1279 \end{proof} |
1280 |
|
1281 To sum up, we have shown that minimal elements according to the ordering |
|
1282 by Okui and Suzuki are exactly the @{text POSIX}-values we defined inductively |
|
1283 in Section ??? |
|
1280 *} |
1284 *} |
1281 |
1285 |
1282 |
1286 |
1283 section {* Extensions and Optimisations*} |
1287 section {* Extensions and Optimisations*} |
1284 |
1288 |