diff -r e6f395eccfe7 -r 046c9ecf9150 Paper/Paper.thy
--- a/Paper/Paper.thy	Sat Jan 26 11:50:40 2013 +0000
+++ b/Paper/Paper.thy	Sat Jan 26 12:00:21 2013 +0000
@@ -531,9 +531,12 @@
   \phantom{@{text "["}}@{text "(L, 4), (L, 0)"}@{text "]"} 
   \end{tabular}
   &
-  \begin{tabular}{@ {}p{3.6cm}@ {}}
+  \begin{tabular}{@ {}l@ {}}
   @{thm (lhs) tcopy_loop_def} @{text "\<equiv>"}\\
-  @{thm (rhs) tcopy_loop_def}\\
+  @{text "["}@{text "(R, 0), (R, 2), (R, 3),"}\\
+  \phantom{@{text "["}}@{text "(W0, 2), (R, 3), (R, 4),"}\\
+  \phantom{@{text "["}}@{text "(W1, 5), (R, 4), (L, 6),"}\\
+  \phantom{@{text "["}}@{text "(L, 5), (L, 6), (L, 1)"}@{text "]"} 
   \end{tabular}
   &
   \begin{tabular}{@ {}p{3.6cm}@ {}}