Paper/Paper.thy
changeset 136 13b0f3dac9a2
parent 135 604518f0127f
child 137 06bafc710423
equal deleted inserted replaced
135:604518f0127f 136:13b0f3dac9a2
  1189            ($(za.south east)+(0em,0ex)$) -- ($(xxa.south west)+(0em,0ex)$)
  1189            ($(za.south east)+(0em,0ex)$) -- ($(xxa.south west)+(0em,0ex)$)
  1190                node[midway, below=0.5em]{@{text "(x - x'\<^isub>m\<^isub>a\<^isub>x) @ z\<^isub>a \<in> A"}};
  1190                node[midway, below=0.5em]{@{text "(x - x'\<^isub>m\<^isub>a\<^isub>x) @ z\<^isub>a \<in> A"}};
  1191 
  1191 
  1192     \draw[decoration={brace,transform={yscale=3}},decorate]
  1192     \draw[decoration={brace,transform={yscale=3}},decorate]
  1193            ($(xa.south east)+(0em,0ex)$) -- ($(xa.south west)+(0em,0ex)$)
  1193            ($(xa.south east)+(0em,0ex)$) -- ($(xa.south west)+(0em,0ex)$)
  1194                node[midway, below=0.5em]{@{text "x'\<^isub>m\<^isub>a\<^isub>x \<in> A\<star>"}};
  1194                node[midway, below=0.5em]{@{term "x'\<^isub>m\<^isub>a\<^isub>x \<in> A\<star>"}};
  1195 
  1195 
  1196     \draw[decoration={brace,transform={yscale=3}},decorate]
  1196     \draw[decoration={brace,transform={yscale=3}},decorate]
  1197            ($(zb.south east)+(0em,0ex)$) -- ($(zb.south west)+(0em,0ex)$)
  1197            ($(zb.south east)+(0em,0ex)$) -- ($(zb.south west)+(0em,0ex)$)
  1198                node[midway, below=0.5em]{@{text "z\<^isub>b \<in> A\<star>"}};
  1198                node[midway, below=0.5em]{@{term "z\<^isub>b \<in> A\<star>"}};
  1199 
  1199 
  1200     \draw[decoration={brace,transform={yscale=3}},decorate]
  1200     \draw[decoration={brace,transform={yscale=3}},decorate]
  1201            ($(zb.south east)+(0em,-4ex)$) -- ($(xxa.south west)+(0em,-4ex)$)
  1201            ($(zb.south east)+(0em,-4ex)$) -- ($(xxa.south west)+(0em,-4ex)$)
  1202                node[midway, below=0.5em]{@{text "(x - x'\<^isub>m\<^isub>a\<^isub>x) @ z \<in> A\<star>"}};
  1202                node[midway, below=0.5em]{@{term "(x - x'\<^isub>m\<^isub>a\<^isub>x) @ z \<in> A\<star>"}};
  1203   \end{tikzpicture}}
  1203   \end{tikzpicture}}
  1204   \end{center}
  1204   \end{center}
  1205   %
  1205   %
  1206   \noindent
  1206   \noindent
  1207   We can find a strict prefix @{text "x'"} of @{text x} such that @{term "x' \<in> A\<star>"},
  1207   We can find a strict prefix @{text "x'"} of @{text x} such that @{term "x' \<in> A\<star>"},