718 \begin{center} |
718 \begin{center} |
719 \begin{tabular}{@ {}c@ {\hspace{3mm}}c@ {\hspace{3mm}}c} |
719 \begin{tabular}{@ {}c@ {\hspace{3mm}}c@ {\hspace{3mm}}c} |
720 \begin{tabular}[t]{@ {}l@ {}} |
720 \begin{tabular}[t]{@ {}l@ {}} |
721 @{thm (lhs) tcopy_begin_def} @{text "\<equiv>"}\\ |
721 @{thm (lhs) tcopy_begin_def} @{text "\<equiv>"}\\ |
722 \hspace{2mm}@{text "["}@{text "(W\<^bsub>Bk\<^esub>, 0), (R, 2), (R, 3),"}\\ |
722 \hspace{2mm}@{text "["}@{text "(W\<^bsub>Bk\<^esub>, 0), (R, 2), (R, 3),"}\\ |
723 \hspace{2mm}\phantom{@{text "["}}@{text "(R, 2), (W1, 3), (L, 4),"}\\ |
723 \hspace{2mm}\phantom{@{text "["}}@{text "(R, 2), (W\<^bsub>Oc\<^esub>, 3), (L, 4),"}\\ |
724 \hspace{2mm}\phantom{@{text "["}}@{text "(L, 4), (L, 0)"}@{text "]"} |
724 \hspace{2mm}\phantom{@{text "["}}@{text "(L, 4), (L, 0)"}@{text "]"} |
725 \end{tabular} |
725 \end{tabular} |
726 & |
726 & |
727 \begin{tabular}[t]{@ {}l@ {}} |
727 \begin{tabular}[t]{@ {}l@ {}} |
728 @{thm (lhs) tcopy_loop_def} @{text "\<equiv>"}\\ |
728 @{thm (lhs) tcopy_loop_def} @{text "\<equiv>"}\\ |