1043   Now assuming  @{term "x @ z \<in> A ;; B"} there are only two possible ways how this string

  1044   is `split'  over @{term "A ;; B"}:

  1045 

  1046   \begin{center}

  1047   \scalebox{0.7}{

  1048   \begin{tikzpicture}

  1049     \node[draw,minimum height=3.8ex] (xa) { $\hspace{4em}x'\hspace{4em}$ };

  1050     \node[draw,minimum height=3.8ex, right=-0.03em of xa] (xxa) { $\hspace{0.5em}x - x'\hspace{0.5em}$ };

  1051     \node[draw,minimum height=3.8ex, right=-0.03em of xxa] (z) { $\hspace{10.1em}z\hspace{10.1em}$ };

  1052 

  1053     \draw[decoration={brace,transform={yscale=3}},decorate]

  1054            (xa.north west) -- ($(xxa.north east)+(0em,0em)$)

  1055                node[midway, above=0.5em]{$x$};

  1056 

  1057     \draw[decoration={brace,transform={yscale=3}},decorate]

  1058            (z.north west) -- ($(z.north east)+(0em,0em)$)

  1059                node[midway, above=0.5em]{$z$};

  1060 

  1061     \draw[decoration={brace,transform={yscale=3}},decorate]

  1062            ($(xa.north west)+(0em,3ex)$) -- ($(z.north east)+(0em,3ex)$)

  1063                node[midway, above=0.8em]{@{term "x @ z \<in> A ;; B"}};

  1064 

  1065     \draw[decoration={brace,transform={yscale=3}},decorate]

  1066            ($(z.south east)+(0em,0ex)$) -- ($(xxa.south west)+(0em,0ex)$)

  1067                node[midway, below=0.5em]{@{term "(x - x') @ z \<in> B"}};

  1068 

  1069     \draw[decoration={brace,transform={yscale=3}},decorate]

  1070            ($(xa.south east)+(0em,0ex)$) -- ($(xa.south west)+(0em,0ex)$)

  1071                node[midway, below=0.5em]{@{term "x' \<in> A"}};

  1072   \end{tikzpicture}}

  1073 

  1074   \scalebox{0.7}{

  1075   \begin{tikzpicture}

  1076     \node[draw,minimum height=3.8ex] (x) { $\hspace{6.5em}x\hspace{6.5em}$ };

  1077     \node[draw,minimum height=3.8ex, right=-0.03em of x] (za) { $\hspace{2em}z'\hspace{2em}$ };

  1078     \node[draw,minimum height=3.8ex, right=-0.03em of za] (zza) { $\hspace{6.1em}z - z'\hspace{6.1em}$  };

  1079 

  1080     \draw[decoration={brace,transform={yscale=3}},decorate]

  1081            (x.north west) -- ($(za.north west)+(0em,0em)$)

  1082                node[midway, above=0.5em]{$x$};

  1083 

  1084     \draw[decoration={brace,transform={yscale=3}},decorate]

  1085            ($(za.north west)+(0em,0ex)$) -- ($(zza.north east)+(0em,0ex)$)

  1086                node[midway, above=0.8em]{$z$};

  1087 

  1088     \draw[decoration={brace,transform={yscale=3}},decorate]

  1089            ($(x.north west)+(0em,3ex)$) -- ($(zza.north east)+(0em,3ex)$)

  1090                node[midway, above=0.8em]{@{term "x @ z \<in> A ;; B"}};

  1091 

  1092     \draw[decoration={brace,transform={yscale=3}},decorate]

  1093            ($(za.south east)+(0em,0ex)$) -- ($(x.south west)+(0em,0ex)$)

  1094                node[midway, below=0.5em]{@{text "x @ z' \<in> A"}};

  1095 

  1096     \draw[decoration={brace,transform={yscale=3}},decorate]

  1097            ($(zza.south east)+(0em,0ex)$) -- ($(za.south east)+(0em,0ex)$)

  1098                node[midway, below=0.5em]{@{text "(z - z') \<in> B"}};

  1099   \end{tikzpicture}}

  1100   \end{center}

  1101 

  1102   \noindent

  1103   Either there is a prefix of @{text x} in @{text A} and the rest in @{text B},

  1104   or @{text x} and a prefix of @{text "z"} is in @{text A} and the rest in @{text B}.

  1105   In bot cases we have to show that @{term "y @ z \<in> A ;; B"}. For this we use the 

  1106   following tagging-function

  1107 

  1108   \begin{center}

  1109   @{thm tag_str_SEQ_def[where ?L1.0="A" and ?L2.0="B", THEN meta_eq_app]}

  1110   \end{center}

  1111 

  1112   \noindent

  1113   with the idea ???