equal
deleted
inserted
replaced
20 W0 ("W\<^bsub>\<^raw:\hspace{-2pt}>Bk\<^esub>") and |
20 W0 ("W\<^bsub>\<^raw:\hspace{-2pt}>Bk\<^esub>") and |
21 W1 ("W\<^bsub>\<^raw:\hspace{-2pt}>Oc\<^esub>") and |
21 W1 ("W\<^bsub>\<^raw:\hspace{-2pt}>Oc\<^esub>") and |
22 update2 ("update") and |
22 update2 ("update") and |
23 tm_wf0 ("wf") and |
23 tm_wf0 ("wf") and |
24 (*is_even ("iseven") and*) |
24 (*is_even ("iseven") and*) |
25 tcopy_init ("copy\<^bsub>begin\<^esub>") and |
25 tcopy_begin ("copy\<^bsub>begin\<^esub>") and |
26 tcopy_loop ("copy\<^bsub>loop\<^esub>") and |
26 tcopy_loop ("copy\<^bsub>loop\<^esub>") and |
27 tcopy_end ("copy\<^bsub>end\<^esub>") and |
27 tcopy_end ("copy\<^bsub>end\<^esub>") and |
28 step0 ("step") and |
28 step0 ("step") and |
29 steps0 ("steps") and |
29 steps0 ("steps") and |
30 exponent ("_\<^bsup>_\<^esup>") and |
30 exponent ("_\<^bsup>_\<^esup>") and |
527 |
527 |
528 \begin{figure}[t] |
528 \begin{figure}[t] |
529 \begin{center} |
529 \begin{center} |
530 \begin{tabular}{@ {}c@ {\hspace{3mm}}c@ {\hspace{3mm}}c} |
530 \begin{tabular}{@ {}c@ {\hspace{3mm}}c@ {\hspace{3mm}}c} |
531 \begin{tabular}[t]{@ {}l@ {}} |
531 \begin{tabular}[t]{@ {}l@ {}} |
532 @{thm (lhs) tcopy_init_def} @{text "\<equiv>"}\\ |
532 @{thm (lhs) tcopy_begin_def} @{text "\<equiv>"}\\ |
533 \hspace{2mm}@{text "["}@{text "(W\<^bsub>Bk\<^esub>, 0), (R, 2), (R, 3),"}\\ |
533 \hspace{2mm}@{text "["}@{text "(W\<^bsub>Bk\<^esub>, 0), (R, 2), (R, 3),"}\\ |
534 \hspace{2mm}\phantom{@{text "["}}@{text "(R, 2), (W1, 3), (L, 4),"}\\ |
534 \hspace{2mm}\phantom{@{text "["}}@{text "(R, 2), (W1, 3), (L, 4),"}\\ |
535 \hspace{2mm}\phantom{@{text "["}}@{text "(L, 4), (L, 0)"}@{text "]"} |
535 \hspace{2mm}\phantom{@{text "["}}@{text "(L, 4), (L, 0)"}@{text "]"} |
536 \end{tabular} |
536 \end{tabular} |
537 & |
537 & |