529 @{text "["}@{text "(W0, 0), (R, 2), (R, 3),"}\\ |
529 @{text "["}@{text "(W0, 0), (R, 2), (R, 3),"}\\ |
530 \phantom{@{text "["}}@{text "(R, 2), (W1, 3), (L, 4),"}\\ |
530 \phantom{@{text "["}}@{text "(R, 2), (W1, 3), (L, 4),"}\\ |
531 \phantom{@{text "["}}@{text "(L, 4), (L, 0)"}@{text "]"} |
531 \phantom{@{text "["}}@{text "(L, 4), (L, 0)"}@{text "]"} |
532 \end{tabular} |
532 \end{tabular} |
533 & |
533 & |
534 \begin{tabular}{@ {}p{3.6cm}@ {}} |
534 \begin{tabular}{@ {}l@ {}} |
535 @{thm (lhs) tcopy_loop_def} @{text "\<equiv>"}\\ |
535 @{thm (lhs) tcopy_loop_def} @{text "\<equiv>"}\\ |
536 @{thm (rhs) tcopy_loop_def}\\ |
536 @{text "["}@{text "(R, 0), (R, 2), (R, 3),"}\\ |
|
537 \phantom{@{text "["}}@{text "(W0, 2), (R, 3), (R, 4),"}\\ |
|
538 \phantom{@{text "["}}@{text "(W1, 5), (R, 4), (L, 6),"}\\ |
|
539 \phantom{@{text "["}}@{text "(L, 5), (L, 6), (L, 1)"}@{text "]"} |
537 \end{tabular} |
540 \end{tabular} |
538 & |
541 & |
539 \begin{tabular}{@ {}p{3.6cm}@ {}} |
542 \begin{tabular}{@ {}p{3.6cm}@ {}} |
540 @{thm (lhs) tcopy_end_def} @{text "\<equiv>"}\\ |
543 @{thm (lhs) tcopy_end_def} @{text "\<equiv>"}\\ |
541 @{thm (rhs) tcopy_end_def} |
544 @{thm (rhs) tcopy_end_def} |