# HG changeset patch
# User urbanc
# Date 1298189533 0
# Node ID 62925473bf6be19260214085c407a1283c980a69
# Parent  8233510cab6c6bf1257b4c545edf42247f3e61ef
added pictures for seq-case

diff -r 8233510cab6c -r 62925473bf6b Myhill_2.thy
--- a/Myhill_2.thy	Sun Feb 20 07:33:54 2011 +0000
+++ b/Myhill_2.thy	Sun Feb 20 08:12:13 2011 +0000
@@ -302,7 +302,7 @@
   tag_str_SEQ :: "lang \<Rightarrow> lang \<Rightarrow> string \<Rightarrow> (lang \<times> lang set)"
 where
   "tag_str_SEQ L1 L2 \<equiv>
-     (\<lambda>x. (\<approx>L1 `` {x}, {(\<approx>L2 `` {x - xa}) | xa.  xa \<le> x \<and> xa \<in> L1}))"
+     (\<lambda>x. (\<approx>L1 `` {x}, {(\<approx>L2 `` {x - x'}) | x'.  x' \<le> x \<and> x' \<in> L1}))"
 
 text {* The following is a techical lemma which helps to split the @{text "x @ z \<in> L\<^isub>1 ;; L\<^isub>2"} mentioned above.*}
 
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]
diff -r 8233510cab6c -r 62925473bf6b Paper/document/root.tex
--- a/Paper/document/root.tex	Sun Feb 20 07:33:54 2011 +0000
+++ b/Paper/document/root.tex	Sun Feb 20 08:12:13 2011 +0000
@@ -5,6 +5,10 @@
 \usepackage{amssymb}
 \usepackage{tikz}
 \usepackage{pgf}
+\usetikzlibrary{arrows,automata,decorations,fit,calc}
+\usetikzlibrary{shapes,shapes.arrows,snakes,positioning}
+\usepgflibrary{shapes.misc} % LATEX and plain TEX and pure pgf
+\usetikzlibrary{matrix}
 \usepackage{pdfsetup}
 \usepackage{ot1patch}
 \usepackage{times}