author | zhang |
Sun, 13 Feb 2011 10:36:53 +0000 | |
changeset 99 | 54aa3b6dd71c |
parent 62 | d94209ad2880 |
permissions | -rw-r--r-- |
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} |