diff -r 8233510cab6c -r 62925473bf6b Paper/Paper.thy
--- a/Paper/Paper.thy	Sun Feb 20 07:33:54 2011 +0000
+++ b/Paper/Paper.thy	Sun Feb 20 08:12:13 2011 +0000
@@ -1040,12 +1040,81 @@
 
   \noindent
   where @{text c} and @{text d} are characters, and @{text x} and @{text y} are strings.
+  Now assuming  @{term "x @ z \<in> A ;; B"} there are only two possible ways how this string
+  is `split'  over @{term "A ;; B"}:
 
-  \begin{proof}[@{const SEQ}-Case]
+  \begin{center}
+  \scalebox{0.7}{
+  \begin{tikzpicture}
+    \node[draw,minimum height=3.8ex] (xa) { $\hspace{4em}x'\hspace{4em}$ };
+    \node[draw,minimum height=3.8ex, right=-0.03em of xa] (xxa) { $\hspace{0.5em}x - x'\hspace{0.5em}$ };
+    \node[draw,minimum height=3.8ex, right=-0.03em of xxa] (z) { $\hspace{10.1em}z\hspace{10.1em}$ };
+
+    \draw[decoration={brace,transform={yscale=3}},decorate]
+           (xa.north west) -- ($(xxa.north east)+(0em,0em)$)
+               node[midway, above=0.5em]{$x$};
+
+    \draw[decoration={brace,transform={yscale=3}},decorate]
+           (z.north west) -- ($(z.north east)+(0em,0em)$)
+               node[midway, above=0.5em]{$z$};
+
+    \draw[decoration={brace,transform={yscale=3}},decorate]
+           ($(xa.north west)+(0em,3ex)$) -- ($(z.north east)+(0em,3ex)$)
+               node[midway, above=0.8em]{@{term "x @ z \<in> A ;; B"}};
+
+    \draw[decoration={brace,transform={yscale=3}},decorate]
+           ($(z.south east)+(0em,0ex)$) -- ($(xxa.south west)+(0em,0ex)$)
+               node[midway, below=0.5em]{@{term "(x - x') @ z \<in> B"}};
+
+    \draw[decoration={brace,transform={yscale=3}},decorate]
+           ($(xa.south east)+(0em,0ex)$) -- ($(xa.south west)+(0em,0ex)$)
+               node[midway, below=0.5em]{@{term "x' \<in> A"}};
+  \end{tikzpicture}}
+
+  \scalebox{0.7}{
+  \begin{tikzpicture}
+    \node[draw,minimum height=3.8ex] (x) { $\hspace{6.5em}x\hspace{6.5em}$ };
+    \node[draw,minimum height=3.8ex, right=-0.03em of x] (za) { $\hspace{2em}z'\hspace{2em}$ };
+    \node[draw,minimum height=3.8ex, right=-0.03em of za] (zza) { $\hspace{6.1em}z - z'\hspace{6.1em}$  };
+
+    \draw[decoration={brace,transform={yscale=3}},decorate]
+           (x.north west) -- ($(za.north west)+(0em,0em)$)
+               node[midway, above=0.5em]{$x$};
+
+    \draw[decoration={brace,transform={yscale=3}},decorate]
+           ($(za.north west)+(0em,0ex)$) -- ($(zza.north east)+(0em,0ex)$)
+               node[midway, above=0.8em]{$z$};
+
+    \draw[decoration={brace,transform={yscale=3}},decorate]
+           ($(x.north west)+(0em,3ex)$) -- ($(zza.north east)+(0em,3ex)$)
+               node[midway, above=0.8em]{@{term "x @ z \<in> A ;; B"}};
+
+    \draw[decoration={brace,transform={yscale=3}},decorate]
+           ($(za.south east)+(0em,0ex)$) -- ($(x.south west)+(0em,0ex)$)
+               node[midway, below=0.5em]{@{text "x @ z' \<in> A"}};
+
+    \draw[decoration={brace,transform={yscale=3}},decorate]
+           ($(zza.south east)+(0em,0ex)$) -- ($(za.south east)+(0em,0ex)$)
+               node[midway, below=0.5em]{@{text "(z - z') \<in> B"}};
+  \end{tikzpicture}}
+  \end{center}
+
+  \noindent
+  Either there is a prefix of @{text x} in @{text A} and the rest in @{text B},
+  or @{text x} and a prefix of @{text "z"} is in @{text A} and the rest in @{text B}.
+  In bot cases we have to show that @{term "y @ z \<in> A ;; B"}. For this we use the 
+  following tagging-function
 
   \begin{center}
   @{thm tag_str_SEQ_def[where ?L1.0="A" and ?L2.0="B", THEN meta_eq_app]}
   \end{center}
+
+  \noindent
+  with the idea ???
+
+  \begin{proof}[@{const SEQ}-Case]
+
+
   \end{proof}
 
   \begin{proof}[@{const STAR}-Case]