pres/document/fig_seq.tex
author urbanc
Sun, 12 Feb 2012 23:20:06 +0000
changeset 304 bd05c5011c0f
parent 62 d94209ad2880
permissions -rw-r--r--
contribution section
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
62
d94209ad2880 Copy Myhill.thy into Myhill_2.thyand put Myhill_2.thy into logic ListP. Myhill.thy is now almost empty ready to be extended by new manuscripts.
zhang
parents:
diff changeset
     1
\begin{figure}[h!]
d94209ad2880 Copy Myhill.thy into Myhill_2.thyand put Myhill_2.thy into logic ListP. Myhill.thy is now almost empty ready to be extended by new manuscripts.
zhang
parents:
diff changeset
     2
\centering
d94209ad2880 Copy Myhill.thy into Myhill_2.thyand put Myhill_2.thy into logic ListP. Myhill.thy is now almost empty ready to be extended by new manuscripts.
zhang
parents:
diff changeset
     3
d94209ad2880 Copy Myhill.thy into Myhill_2.thyand put Myhill_2.thy into logic ListP. Myhill.thy is now almost empty ready to be extended by new manuscripts.
zhang
parents:
diff changeset
     4
\subfigure[First possible way to split $x@z$]{\label{seq_first_split}
d94209ad2880 Copy Myhill.thy into Myhill_2.thyand put Myhill_2.thy into logic ListP. Myhill.thy is now almost empty ready to be extended by new manuscripts.
zhang
parents:
diff changeset
     5
\scalebox{0.7}{
d94209ad2880 Copy Myhill.thy into Myhill_2.thyand put Myhill_2.thy into logic ListP. Myhill.thy is now almost empty ready to be extended by new manuscripts.
zhang
parents:
diff changeset
     6
\begin{tikzpicture}
d94209ad2880 Copy Myhill.thy into Myhill_2.thyand put Myhill_2.thy into logic ListP. Myhill.thy is now almost empty ready to be extended by new manuscripts.
zhang
parents:
diff changeset
     7
    \node[draw,minimum height=3.8ex] (xa) { $\hspace{4em}xa\hspace{4em}$ };
d94209ad2880 Copy Myhill.thy into Myhill_2.thyand put Myhill_2.thy into logic ListP. Myhill.thy is now almost empty ready to be extended by new manuscripts.
zhang
parents:
diff changeset
     8
    \node[draw,minimum height=3.8ex, right=-0.03em of xa] (xxa) { $\hspace{0.5em}x - xa\hspace{0.5em}$ };
d94209ad2880 Copy Myhill.thy into Myhill_2.thyand put Myhill_2.thy into logic ListP. Myhill.thy is now almost empty ready to be extended by new manuscripts.
zhang
parents:
diff changeset
     9
    \node[draw,minimum height=3.8ex, right=-0.03em of xxa] (z) { $\hspace{21em}$ };
d94209ad2880 Copy Myhill.thy into Myhill_2.thyand put Myhill_2.thy into logic ListP. Myhill.thy is now almost empty ready to be extended by new manuscripts.
zhang
parents:
diff changeset
    10
d94209ad2880 Copy Myhill.thy into Myhill_2.thyand put Myhill_2.thy into logic ListP. Myhill.thy is now almost empty ready to be extended by new manuscripts.
zhang
parents:
diff changeset
    11
    \draw[decoration={brace,transform={yscale=3}},decorate]
d94209ad2880 Copy Myhill.thy into Myhill_2.thyand put Myhill_2.thy into logic ListP. Myhill.thy is now almost empty ready to be extended by new manuscripts.
zhang
parents:
diff changeset
    12
           (xa.north west) -- ($(xxa.north east)+(0em,0em)$)
d94209ad2880 Copy Myhill.thy into Myhill_2.thyand put Myhill_2.thy into logic ListP. Myhill.thy is now almost empty ready to be extended by new manuscripts.
zhang
parents:
diff changeset
    13
               node[midway, above=0.5em]{$x$};
d94209ad2880 Copy Myhill.thy into Myhill_2.thyand put Myhill_2.thy into logic ListP. Myhill.thy is now almost empty ready to be extended by new manuscripts.
zhang
parents:
diff changeset
    14
d94209ad2880 Copy Myhill.thy into Myhill_2.thyand put Myhill_2.thy into logic ListP. Myhill.thy is now almost empty ready to be extended by new manuscripts.
zhang
parents:
diff changeset
    15
    \draw[decoration={brace,transform={yscale=3}},decorate]
d94209ad2880 Copy Myhill.thy into Myhill_2.thyand put Myhill_2.thy into logic ListP. Myhill.thy is now almost empty ready to be extended by new manuscripts.
zhang
parents:
diff changeset
    16
           (z.north west) -- ($(z.north east)+(0em,0em)$)
d94209ad2880 Copy Myhill.thy into Myhill_2.thyand put Myhill_2.thy into logic ListP. Myhill.thy is now almost empty ready to be extended by new manuscripts.
zhang
parents:
diff changeset
    17
               node[midway, above=0.5em]{$z$};
d94209ad2880 Copy Myhill.thy into Myhill_2.thyand put Myhill_2.thy into logic ListP. Myhill.thy is now almost empty ready to be extended by new manuscripts.
zhang
parents:
diff changeset
    18
d94209ad2880 Copy Myhill.thy into Myhill_2.thyand put Myhill_2.thy into logic ListP. Myhill.thy is now almost empty ready to be extended by new manuscripts.
zhang
parents:
diff changeset
    19
    \draw[decoration={brace,transform={yscale=3}},decorate]
d94209ad2880 Copy Myhill.thy into Myhill_2.thyand put Myhill_2.thy into logic ListP. Myhill.thy is now almost empty ready to be extended by new manuscripts.
zhang
parents:
diff changeset
    20
           ($(xa.north west)+(0em,3ex)$) -- ($(z.north east)+(0em,3ex)$)
d94209ad2880 Copy Myhill.thy into Myhill_2.thyand put Myhill_2.thy into logic ListP. Myhill.thy is now almost empty ready to be extended by new manuscripts.
zhang
parents:
diff changeset
    21
               node[midway, above=0.8em]{$x @ z \in L_1 ;; L_2$};
d94209ad2880 Copy Myhill.thy into Myhill_2.thyand put Myhill_2.thy into logic ListP. Myhill.thy is now almost empty ready to be extended by new manuscripts.
zhang
parents:
diff changeset
    22
d94209ad2880 Copy Myhill.thy into Myhill_2.thyand put Myhill_2.thy into logic ListP. Myhill.thy is now almost empty ready to be extended by new manuscripts.
zhang
parents:
diff changeset
    23
    \draw[decoration={brace,transform={yscale=3}},decorate]
d94209ad2880 Copy Myhill.thy into Myhill_2.thyand put Myhill_2.thy into logic ListP. Myhill.thy is now almost empty ready to be extended by new manuscripts.
zhang
parents:
diff changeset
    24
           ($(z.south east)+(0em,0ex)$) -- ($(xxa.south west)+(0em,0ex)$)
d94209ad2880 Copy Myhill.thy into Myhill_2.thyand put Myhill_2.thy into logic ListP. Myhill.thy is now almost empty ready to be extended by new manuscripts.
zhang
parents:
diff changeset
    25
               node[midway, below=0.5em]{$(x - xa) @ z \in L_2$};
d94209ad2880 Copy Myhill.thy into Myhill_2.thyand put Myhill_2.thy into logic ListP. Myhill.thy is now almost empty ready to be extended by new manuscripts.
zhang
parents:
diff changeset
    26
d94209ad2880 Copy Myhill.thy into Myhill_2.thyand put Myhill_2.thy into logic ListP. Myhill.thy is now almost empty ready to be extended by new manuscripts.
zhang
parents:
diff changeset
    27
    \draw[decoration={brace,transform={yscale=3}},decorate]
d94209ad2880 Copy Myhill.thy into Myhill_2.thyand put Myhill_2.thy into logic ListP. Myhill.thy is now almost empty ready to be extended by new manuscripts.
zhang
parents:
diff changeset
    28
           ($(xa.south east)+(0em,0ex)$) -- ($(xa.south west)+(0em,0ex)$)
d94209ad2880 Copy Myhill.thy into Myhill_2.thyand put Myhill_2.thy into logic ListP. Myhill.thy is now almost empty ready to be extended by new manuscripts.
zhang
parents:
diff changeset
    29
               node[midway, below=0.5em]{$xa \in L_1$};
d94209ad2880 Copy Myhill.thy into Myhill_2.thyand put Myhill_2.thy into logic ListP. Myhill.thy is now almost empty ready to be extended by new manuscripts.
zhang
parents:
diff changeset
    30
\end{tikzpicture}}}
d94209ad2880 Copy Myhill.thy into Myhill_2.thyand put Myhill_2.thy into logic ListP. Myhill.thy is now almost empty ready to be extended by new manuscripts.
zhang
parents:
diff changeset
    31
d94209ad2880 Copy Myhill.thy into Myhill_2.thyand put Myhill_2.thy into logic ListP. Myhill.thy is now almost empty ready to be extended by new manuscripts.
zhang
parents:
diff changeset
    32
\subfigure[Transferred structure corresponding to the first way of splitting]{\label{seq_trans_first_split}
d94209ad2880 Copy Myhill.thy into Myhill_2.thyand put Myhill_2.thy into logic ListP. Myhill.thy is now almost empty ready to be extended by new manuscripts.
zhang
parents:
diff changeset
    33
\scalebox{0.7}{
d94209ad2880 Copy Myhill.thy into Myhill_2.thyand put Myhill_2.thy into logic ListP. Myhill.thy is now almost empty ready to be extended by new manuscripts.
zhang
parents:
diff changeset
    34
\begin{tikzpicture}
d94209ad2880 Copy Myhill.thy into Myhill_2.thyand put Myhill_2.thy into logic ListP. Myhill.thy is now almost empty ready to be extended by new manuscripts.
zhang
parents:
diff changeset
    35
    \node[draw,minimum height=3.8ex] (xa) { $\hspace{4em}ya\hspace{4em}$ };
d94209ad2880 Copy Myhill.thy into Myhill_2.thyand put Myhill_2.thy into logic ListP. Myhill.thy is now almost empty ready to be extended by new manuscripts.
zhang
parents:
diff changeset
    36
    \node[draw,minimum height=3.8ex, right=-0.03em of xa] (xxa) { $\hspace{0.5em}y - ya\hspace{0.5em}$ };
d94209ad2880 Copy Myhill.thy into Myhill_2.thyand put Myhill_2.thy into logic ListP. Myhill.thy is now almost empty ready to be extended by new manuscripts.
zhang
parents:
diff changeset
    37
    \node[draw,minimum height=3.8ex, right=-0.03em of xxa] (z) { $\hspace{21em}$ };
d94209ad2880 Copy Myhill.thy into Myhill_2.thyand put Myhill_2.thy into logic ListP. Myhill.thy is now almost empty ready to be extended by new manuscripts.
zhang
parents:
diff changeset
    38
d94209ad2880 Copy Myhill.thy into Myhill_2.thyand put Myhill_2.thy into logic ListP. Myhill.thy is now almost empty ready to be extended by new manuscripts.
zhang
parents:
diff changeset
    39
    \draw[decoration={brace,transform={yscale=3}},decorate]
d94209ad2880 Copy Myhill.thy into Myhill_2.thyand put Myhill_2.thy into logic ListP. Myhill.thy is now almost empty ready to be extended by new manuscripts.
zhang
parents:
diff changeset
    40
           (xa.north west) -- ($(xxa.north east)+(0em,0em)$)
d94209ad2880 Copy Myhill.thy into Myhill_2.thyand put Myhill_2.thy into logic ListP. Myhill.thy is now almost empty ready to be extended by new manuscripts.
zhang
parents:
diff changeset
    41
               node[midway, above=0.5em]{$y$};
d94209ad2880 Copy Myhill.thy into Myhill_2.thyand put Myhill_2.thy into logic ListP. Myhill.thy is now almost empty ready to be extended by new manuscripts.
zhang
parents:
diff changeset
    42
d94209ad2880 Copy Myhill.thy into Myhill_2.thyand put Myhill_2.thy into logic ListP. Myhill.thy is now almost empty ready to be extended by new manuscripts.
zhang
parents:
diff changeset
    43
    \draw[decoration={brace,transform={yscale=3}},decorate]
d94209ad2880 Copy Myhill.thy into Myhill_2.thyand put Myhill_2.thy into logic ListP. Myhill.thy is now almost empty ready to be extended by new manuscripts.
zhang
parents:
diff changeset
    44
           (z.north west) -- ($(z.north east)+(0em,0em)$)
d94209ad2880 Copy Myhill.thy into Myhill_2.thyand put Myhill_2.thy into logic ListP. Myhill.thy is now almost empty ready to be extended by new manuscripts.
zhang
parents:
diff changeset
    45
               node[midway, above=0.5em]{$z$};
d94209ad2880 Copy Myhill.thy into Myhill_2.thyand put Myhill_2.thy into logic ListP. Myhill.thy is now almost empty ready to be extended by new manuscripts.
zhang
parents:
diff changeset
    46
d94209ad2880 Copy Myhill.thy into Myhill_2.thyand put Myhill_2.thy into logic ListP. Myhill.thy is now almost empty ready to be extended by new manuscripts.
zhang
parents:
diff changeset
    47
    \draw[decoration={brace,transform={yscale=3}},decorate]
d94209ad2880 Copy Myhill.thy into Myhill_2.thyand put Myhill_2.thy into logic ListP. Myhill.thy is now almost empty ready to be extended by new manuscripts.
zhang
parents:
diff changeset
    48
           ($(xa.north west)+(0em,3ex)$) -- ($(z.north east)+(0em,3ex)$)
d94209ad2880 Copy Myhill.thy into Myhill_2.thyand put Myhill_2.thy into logic ListP. Myhill.thy is now almost empty ready to be extended by new manuscripts.
zhang
parents:
diff changeset
    49
               node[midway, above=0.8em]{$y @ z \in L_1 ;; L_2$};
d94209ad2880 Copy Myhill.thy into Myhill_2.thyand put Myhill_2.thy into logic ListP. Myhill.thy is now almost empty ready to be extended by new manuscripts.
zhang
parents:
diff changeset
    50
d94209ad2880 Copy Myhill.thy into Myhill_2.thyand put Myhill_2.thy into logic ListP. Myhill.thy is now almost empty ready to be extended by new manuscripts.
zhang
parents:
diff changeset
    51
    \draw[decoration={brace,transform={yscale=3}},decorate]
d94209ad2880 Copy Myhill.thy into Myhill_2.thyand put Myhill_2.thy into logic ListP. Myhill.thy is now almost empty ready to be extended by new manuscripts.
zhang
parents:
diff changeset
    52
           ($(z.south east)+(0em,0ex)$) -- ($(xxa.south west)+(0em,0ex)$)
d94209ad2880 Copy Myhill.thy into Myhill_2.thyand put Myhill_2.thy into logic ListP. Myhill.thy is now almost empty ready to be extended by new manuscripts.
zhang
parents:
diff changeset
    53
               node[midway, below=0.5em]{$(y - ya) @ z \in L_2$};
d94209ad2880 Copy Myhill.thy into Myhill_2.thyand put Myhill_2.thy into logic ListP. Myhill.thy is now almost empty ready to be extended by new manuscripts.
zhang
parents:
diff changeset
    54
d94209ad2880 Copy Myhill.thy into Myhill_2.thyand put Myhill_2.thy into logic ListP. Myhill.thy is now almost empty ready to be extended by new manuscripts.
zhang
parents:
diff changeset
    55
    \draw[decoration={brace,transform={yscale=3}},decorate]
d94209ad2880 Copy Myhill.thy into Myhill_2.thyand put Myhill_2.thy into logic ListP. Myhill.thy is now almost empty ready to be extended by new manuscripts.
zhang
parents:
diff changeset
    56
           ($(xa.south east)+(0em,0ex)$) -- ($(xa.south west)+(0em,0ex)$)
d94209ad2880 Copy Myhill.thy into Myhill_2.thyand put Myhill_2.thy into logic ListP. Myhill.thy is now almost empty ready to be extended by new manuscripts.
zhang
parents:
diff changeset
    57
               node[midway, below=0.5em]{$ya \in L_1$};
d94209ad2880 Copy Myhill.thy into Myhill_2.thyand put Myhill_2.thy into logic ListP. Myhill.thy is now almost empty ready to be extended by new manuscripts.
zhang
parents:
diff changeset
    58
\end{tikzpicture}}}
d94209ad2880 Copy Myhill.thy into Myhill_2.thyand put Myhill_2.thy into logic ListP. Myhill.thy is now almost empty ready to be extended by new manuscripts.
zhang
parents:
diff changeset
    59
d94209ad2880 Copy Myhill.thy into Myhill_2.thyand put Myhill_2.thy into logic ListP. Myhill.thy is now almost empty ready to be extended by new manuscripts.
zhang
parents:
diff changeset
    60
\subfigure[The second possible way to split $x@z$]{\label{seq_snd_split}
d94209ad2880 Copy Myhill.thy into Myhill_2.thyand put Myhill_2.thy into logic ListP. Myhill.thy is now almost empty ready to be extended by new manuscripts.
zhang
parents:
diff changeset
    61
\scalebox{0.7}{
d94209ad2880 Copy Myhill.thy into Myhill_2.thyand put Myhill_2.thy into logic ListP. Myhill.thy is now almost empty ready to be extended by new manuscripts.
zhang
parents:
diff changeset
    62
\begin{tikzpicture}
d94209ad2880 Copy Myhill.thy into Myhill_2.thyand put Myhill_2.thy into logic ListP. Myhill.thy is now almost empty ready to be extended by new manuscripts.
zhang
parents:
diff changeset
    63
    \node[draw,minimum height=3.8ex] (x) { $\hspace{6.5em}x\hspace{6.5em}$ };
d94209ad2880 Copy Myhill.thy into Myhill_2.thyand put Myhill_2.thy into logic ListP. Myhill.thy is now almost empty ready to be extended by new manuscripts.
zhang
parents:
diff changeset
    64
    \node[draw,minimum height=3.8ex, right=-0.03em of x] (za) { $\hspace{2em}za\hspace{2em}$ };
d94209ad2880 Copy Myhill.thy into Myhill_2.thyand put Myhill_2.thy into logic ListP. Myhill.thy is now almost empty ready to be extended by new manuscripts.
zhang
parents:
diff changeset
    65
    \node[draw,minimum height=3.8ex, right=-0.03em of za] (zza) { $\hspace{6.1em}z - za\hspace{6.1em}$  };
d94209ad2880 Copy Myhill.thy into Myhill_2.thyand put Myhill_2.thy into logic ListP. Myhill.thy is now almost empty ready to be extended by new manuscripts.
zhang
parents:
diff changeset
    66
d94209ad2880 Copy Myhill.thy into Myhill_2.thyand put Myhill_2.thy into logic ListP. Myhill.thy is now almost empty ready to be extended by new manuscripts.
zhang
parents:
diff changeset
    67
    \draw[decoration={brace,transform={yscale=3}},decorate]
d94209ad2880 Copy Myhill.thy into Myhill_2.thyand put Myhill_2.thy into logic ListP. Myhill.thy is now almost empty ready to be extended by new manuscripts.
zhang
parents:
diff changeset
    68
           ($(za.north west)+(0em,0ex)$) -- ($(zza.north east)+(0em,0ex)$)
d94209ad2880 Copy Myhill.thy into Myhill_2.thyand put Myhill_2.thy into logic ListP. Myhill.thy is now almost empty ready to be extended by new manuscripts.
zhang
parents:
diff changeset
    69
               node[midway, above=0.8em]{$z$};
d94209ad2880 Copy Myhill.thy into Myhill_2.thyand put Myhill_2.thy into logic ListP. Myhill.thy is now almost empty ready to be extended by new manuscripts.
zhang
parents:
diff changeset
    70
d94209ad2880 Copy Myhill.thy into Myhill_2.thyand put Myhill_2.thy into logic ListP. Myhill.thy is now almost empty ready to be extended by new manuscripts.
zhang
parents:
diff changeset
    71
    \draw[decoration={brace,transform={yscale=3}},decorate]
d94209ad2880 Copy Myhill.thy into Myhill_2.thyand put Myhill_2.thy into logic ListP. Myhill.thy is now almost empty ready to be extended by new manuscripts.
zhang
parents:
diff changeset
    72
           ($(x.north west)+(0em,3ex)$) -- ($(zza.north east)+(0em,3ex)$)
d94209ad2880 Copy Myhill.thy into Myhill_2.thyand put Myhill_2.thy into logic ListP. Myhill.thy is now almost empty ready to be extended by new manuscripts.
zhang
parents:
diff changeset
    73
               node[midway, above=0.8em]{$x @ z \in L_1 ;; L_2$};
d94209ad2880 Copy Myhill.thy into Myhill_2.thyand put Myhill_2.thy into logic ListP. Myhill.thy is now almost empty ready to be extended by new manuscripts.
zhang
parents:
diff changeset
    74
d94209ad2880 Copy Myhill.thy into Myhill_2.thyand put Myhill_2.thy into logic ListP. Myhill.thy is now almost empty ready to be extended by new manuscripts.
zhang
parents:
diff changeset
    75
    \draw[decoration={brace,transform={yscale=3}},decorate]
d94209ad2880 Copy Myhill.thy into Myhill_2.thyand put Myhill_2.thy into logic ListP. Myhill.thy is now almost empty ready to be extended by new manuscripts.
zhang
parents:
diff changeset
    76
           ($(za.south east)+(0em,0ex)$) -- ($(x.south west)+(0em,0ex)$)
d94209ad2880 Copy Myhill.thy into Myhill_2.thyand put Myhill_2.thy into logic ListP. Myhill.thy is now almost empty ready to be extended by new manuscripts.
zhang
parents:
diff changeset
    77
               node[midway, below=0.5em]{$x @ za \in L_1$};
d94209ad2880 Copy Myhill.thy into Myhill_2.thyand put Myhill_2.thy into logic ListP. Myhill.thy is now almost empty ready to be extended by new manuscripts.
zhang
parents:
diff changeset
    78
\end{tikzpicture}}}
d94209ad2880 Copy Myhill.thy into Myhill_2.thyand put Myhill_2.thy into logic ListP. Myhill.thy is now almost empty ready to be extended by new manuscripts.
zhang
parents:
diff changeset
    79
d94209ad2880 Copy Myhill.thy into Myhill_2.thyand put Myhill_2.thy into logic ListP. Myhill.thy is now almost empty ready to be extended by new manuscripts.
zhang
parents:
diff changeset
    80
d94209ad2880 Copy Myhill.thy into Myhill_2.thyand put Myhill_2.thy into logic ListP. Myhill.thy is now almost empty ready to be extended by new manuscripts.
zhang
parents:
diff changeset
    81
\subfigure[Transferred structure corresponding to the second way of splitting]{\label{seq_trans_snd_split}
d94209ad2880 Copy Myhill.thy into Myhill_2.thyand put Myhill_2.thy into logic ListP. Myhill.thy is now almost empty ready to be extended by new manuscripts.
zhang
parents:
diff changeset
    82
\scalebox{0.7}{
d94209ad2880 Copy Myhill.thy into Myhill_2.thyand put Myhill_2.thy into logic ListP. Myhill.thy is now almost empty ready to be extended by new manuscripts.
zhang
parents:
diff changeset
    83
\begin{tikzpicture}
d94209ad2880 Copy Myhill.thy into Myhill_2.thyand put Myhill_2.thy into logic ListP. Myhill.thy is now almost empty ready to be extended by new manuscripts.
zhang
parents:
diff changeset
    84
    \node[draw,minimum height=3.8ex] (x) { $\hspace{6.5em}y\hspace{6.5em}$ };
d94209ad2880 Copy Myhill.thy into Myhill_2.thyand put Myhill_2.thy into logic ListP. Myhill.thy is now almost empty ready to be extended by new manuscripts.
zhang
parents:
diff changeset
    85
    \node[draw,minimum height=3.8ex, right=-0.03em of x] (za) { $\hspace{2em}za\hspace{2em}$ };
d94209ad2880 Copy Myhill.thy into Myhill_2.thyand put Myhill_2.thy into logic ListP. Myhill.thy is now almost empty ready to be extended by new manuscripts.
zhang
parents:
diff changeset
    86
    \node[draw,minimum height=3.8ex, right=-0.03em of za] (zza) { $\hspace{6.1em}z - za\hspace{6.1em}$  };
d94209ad2880 Copy Myhill.thy into Myhill_2.thyand put Myhill_2.thy into logic ListP. Myhill.thy is now almost empty ready to be extended by new manuscripts.
zhang
parents:
diff changeset
    87
d94209ad2880 Copy Myhill.thy into Myhill_2.thyand put Myhill_2.thy into logic ListP. Myhill.thy is now almost empty ready to be extended by new manuscripts.
zhang
parents:
diff changeset
    88
    \draw[decoration={brace,transform={yscale=3}},decorate]
d94209ad2880 Copy Myhill.thy into Myhill_2.thyand put Myhill_2.thy into logic ListP. Myhill.thy is now almost empty ready to be extended by new manuscripts.
zhang
parents:
diff changeset
    89
           ($(za.north west)+(0em,0ex)$) -- ($(zza.north east)+(0em,0ex)$)
d94209ad2880 Copy Myhill.thy into Myhill_2.thyand put Myhill_2.thy into logic ListP. Myhill.thy is now almost empty ready to be extended by new manuscripts.
zhang
parents:
diff changeset
    90
               node[midway, above=0.8em]{$z$};
d94209ad2880 Copy Myhill.thy into Myhill_2.thyand put Myhill_2.thy into logic ListP. Myhill.thy is now almost empty ready to be extended by new manuscripts.
zhang
parents:
diff changeset
    91
d94209ad2880 Copy Myhill.thy into Myhill_2.thyand put Myhill_2.thy into logic ListP. Myhill.thy is now almost empty ready to be extended by new manuscripts.
zhang
parents:
diff changeset
    92
    \draw[decoration={brace,transform={yscale=3}},decorate]
d94209ad2880 Copy Myhill.thy into Myhill_2.thyand put Myhill_2.thy into logic ListP. Myhill.thy is now almost empty ready to be extended by new manuscripts.
zhang
parents:
diff changeset
    93
           ($(x.north west)+(0em,3ex)$) -- ($(zza.north east)+(0em,3ex)$)
d94209ad2880 Copy Myhill.thy into Myhill_2.thyand put Myhill_2.thy into logic ListP. Myhill.thy is now almost empty ready to be extended by new manuscripts.
zhang
parents:
diff changeset
    94
               node[midway, above=0.8em]{$y @ z \in L_1 ;; L_2$};
d94209ad2880 Copy Myhill.thy into Myhill_2.thyand put Myhill_2.thy into logic ListP. Myhill.thy is now almost empty ready to be extended by new manuscripts.
zhang
parents:
diff changeset
    95
d94209ad2880 Copy Myhill.thy into Myhill_2.thyand put Myhill_2.thy into logic ListP. Myhill.thy is now almost empty ready to be extended by new manuscripts.
zhang
parents:
diff changeset
    96
    \draw[decoration={brace,transform={yscale=3}},decorate]
d94209ad2880 Copy Myhill.thy into Myhill_2.thyand put Myhill_2.thy into logic ListP. Myhill.thy is now almost empty ready to be extended by new manuscripts.
zhang
parents:
diff changeset
    97
           ($(za.south east)+(0em,0ex)$) -- ($(x.south west)+(0em,0ex)$)
d94209ad2880 Copy Myhill.thy into Myhill_2.thyand put Myhill_2.thy into logic ListP. Myhill.thy is now almost empty ready to be extended by new manuscripts.
zhang
parents:
diff changeset
    98
               node[midway, below=0.5em]{$y @ za \in L_1$};
d94209ad2880 Copy Myhill.thy into Myhill_2.thyand put Myhill_2.thy into logic ListP. Myhill.thy is now almost empty ready to be extended by new manuscripts.
zhang
parents:
diff changeset
    99
\end{tikzpicture}}}
d94209ad2880 Copy Myhill.thy into Myhill_2.thyand put Myhill_2.thy into logic ListP. Myhill.thy is now almost empty ready to be extended by new manuscripts.
zhang
parents:
diff changeset
   100
d94209ad2880 Copy Myhill.thy into Myhill_2.thyand put Myhill_2.thy into logic ListP. Myhill.thy is now almost empty ready to be extended by new manuscripts.
zhang
parents:
diff changeset
   101
\caption{The case for $SEQ$}
d94209ad2880 Copy Myhill.thy into Myhill_2.thyand put Myhill_2.thy into logic ListP. Myhill.thy is now almost empty ready to be extended by new manuscripts.
zhang
parents:
diff changeset
   102
\end{figure}