equal
deleted
inserted
replaced
14 L ("L _" [1000] 0) and |
14 L ("L _" [1000] 0) and |
15 flat ("|_|" [70] 73) and |
15 flat ("|_|" [70] 73) and |
16 Sequ ("_ @ _" [78,77] 63) and |
16 Sequ ("_ @ _" [78,77] 63) and |
17 injval ("inj _ _ _" [1000,77,1000] 77) and |
17 injval ("inj _ _ _" [1000,77,1000] 77) and |
18 projval ("proj _ _ _" [1000,77,1000] 77) and |
18 projval ("proj _ _ _" [1000,77,1000] 77) and |
19 length ("len _" [78] 73) and |
19 length ("len _" [78] 73) |
20 ValOrd ("_ \<succeq>\<^bsub>_\<^esub> _" [78,77,77] 73) |
20 (* and ValOrd ("_ \<succeq>\<^bsub>_\<^esub> _" [78,77,77] 73) *) |
21 (*>*) |
21 (*>*) |
22 |
22 |
23 section {* Introduction *} |
23 section {* Introduction *} |
24 |
24 |
25 text {* |
25 text {* |
326 \noindent |
326 \noindent |
327 The final case is that @{term " \<not> nullable r\<^sub>1"} holds. This case again similar |
327 The final case is that @{term " \<not> nullable r\<^sub>1"} holds. This case again similar |
328 to the cases above. |
328 to the cases above. |
329 *} |
329 *} |
330 |
330 |
331 text {* |
|
332 \noindent |
|
333 Things we have proved about our version of the Sulzmann ordering |
|
334 |
|
335 \begin{center} |
|
336 \begin{tabular}{c} |
|
337 @{thm[mode=IfThen] ValOrd_refl[of "v" "r"]}\medskip\\ |
|
338 %@ {thm[mode=IfThen] ValOrd_total[of "v\<^sub>1" "r" "v\<^sub>2"]} |
|
339 \end{tabular} |
|
340 \end{center}\bigskip |
|
341 |
|
342 \noindent |
|
343 Things we like to prove, but cannot:\bigskip |
|
344 |
|
345 If @{term "s \<in> r \<rightarrow> v\<^sub>1"}, @{term "\<turnstile> v\<^sub>2 : r"}, then @{term "v\<^sub>1 \<succ>r v\<^sub>2"} |
|
346 |
|
347 *} |
|
348 |
|
349 |
331 |
350 text {* |
332 text {* |
351 %\noindent |
333 %\noindent |
352 %{\bf Acknowledgements:} |
334 %{\bf Acknowledgements:} |
353 %We are grateful for the comments we received from anonymous |
335 %We are grateful for the comments we received from anonymous |