(*<*)

theory Slides2

imports "../thys/UTM" "../thys/Abacus_Defs"

begin

declare [[show_question_marks = false]]

hide_const (open) s 

abbreviation

  "update2 p a \<equiv> update a p"

notation (Rule output)

  "==>"  ("\<^raw:\mbox{}\inferrule{\mbox{>_\<^raw:}}>\<^raw:{\mbox{>_\<^raw:}}>")

syntax (Rule output)

  "_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop"

  ("\<^raw:\mbox{}\inferrule{>_\<^raw:}>\<^raw:{\mbox{>_\<^raw:}}>")

  "_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms" 

  ("\<^raw:\mbox{>_\<^raw:}\\>/ _")

  "_asm" :: "prop \<Rightarrow> asms" ("\<^raw:\mbox{>_\<^raw:}>")

notation (Axiom output)

  "Trueprop"  ("\<^raw:\mbox{}\inferrule{\mbox{}}{\mbox{>_\<^raw:}}>")

notation (IfThen output)

  "==>"  ("\<^raw:{\normalsize{}>If\<^raw:\,}> _/ \<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")

syntax (IfThen output)

  "_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop"

  ("\<^raw:{\normalsize{}>If\<^raw:\,}> _ /\<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")

  "_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms" ("\<^raw:\mbox{>_\<^raw:}> /\<^raw:{\normalsize \,>and\<^raw:\,}>/ _")

  "_asm" :: "prop \<Rightarrow> asms" ("\<^raw:\mbox{>_\<^raw:}>")

notation (IfThenNoBox output)

  "==>"  ("\<^raw:{\normalsize{}>If\<^raw:\,}> _/ \<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")

syntax (IfThenNoBox output)

  "_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop"

  ("\<^raw:{\normalsize{}>If\<^raw:\,}> _ /\<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")

  "_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms" ("_ /\<^raw:{\normalsize \,>and\<^raw:\,}>/ _")

  "_asm" :: "prop \<Rightarrow> asms" ("_")

context uncomputable

begin

notation (latex output)

  Cons ("_::_" [48,47] 68) and

  append ("_@_" [65, 64] 65) and

  Oc ("1") and

  Bk ("0") and

  exponent ("_\<^bsup>_\<^esup>" [107] 109) and

  inv_begin0 ("I\<^sub>0") and

  inv_begin1 ("I\<^sub>1") and

  inv_begin2 ("I\<^sub>2") and

  inv_begin3 ("I\<^sub>3") and

  inv_begin4 ("I\<^sub>4") and 

  inv_begin ("I\<^bsub>cbegin\<^esub>") and

  inv_loop1 ("J\<^sub>1") and

  inv_loop0 ("J\<^sub>0") and

  inv_end1 ("K\<^sub>1") and

  inv_end0 ("K\<^sub>0") and

  recf.id ("Id\<^raw:\makebox[0mm]{\,\,\,\,>\<^sup>_\<^raw:}>\<^sub>_") and

  Pr ("Pr\<^sup>_") and

  Cn ("Cn\<^sup>_") and

  Mn ("Mn\<^sup>_") and

  tcopy ("copy") and 

  tcontra ("contra") and

  tape_of ("\<langle>_\<rangle>") and 

  code_tcontra ("code contra") and

  tm_comp ("_ ; _") 

lemma inv_begin_print:

  shows "s = 0 \<Longrightarrow> inv_begin n (s, tp) = inv_begin0 n tp" and

        "s = 1 \<Longrightarrow> inv_begin n (s, tp) = inv_begin1 n tp" and 

        "s = 2 \<Longrightarrow> inv_begin n (s, tp) = inv_begin2 n tp" and 

        "s = 3 \<Longrightarrow> inv_begin n (s, tp) = inv_begin3 n tp" and 

        "s = 4 \<Longrightarrow> inv_begin n (s, tp) = inv_begin4 n tp" and

        "s \<notin> {0,1,2,3,4} \<Longrightarrow> inv_begin n (s, l, r) = False"

apply(case_tac [!] tp)

by (auto)

lemma inv1: 

  shows "0 < (n::nat) \<Longrightarrow> Turing_Hoare.assert_imp (inv_begin0 n) (inv_loop1 n)"

unfolding Turing_Hoare.assert_imp_def

unfolding inv_loop1.simps inv_begin0.simps

apply(auto)

apply(rule_tac x="1" in exI)

apply(auto simp add: replicate.simps)

done

lemma inv2: 

  shows "0 < n \<Longrightarrow> inv_loop0 n = inv_end1 n"

apply(rule ext)

apply(case_tac x)

apply(simp add: inv_end1.simps)

done

lemma measure_begin_print:

  shows "s = 2 \<Longrightarrow> measure_begin_step (s, l, r) = length r" and

        "s = 3 \<Longrightarrow> measure_begin_step (s, l, r) = (if r = [] \<or> r = [Bk] then 1 else 0)" and

        "s = 4 \<Longrightarrow> measure_begin_step (s, l, r) = length l" and 

        "s \<notin> {2,3,4} \<Longrightarrow> measure_begin_step (s, l, r) = 0"

by (simp_all)

lemma inv_begin01:

  assumes "n > 1"

  shows "inv_begin0 n (l, r) = (n > 1 \<and> (l, r) = (Oc \<up> (n - 2), [Oc, Oc, Bk, Oc]))"

using assms by auto                          

lemma inv_begin02:

  assumes "n = 1"

  shows "inv_begin0 n (l, r) = (n = 1 \<and> (l, r) = ([], [Bk, Oc, Bk, Oc]))"

using assms by auto

(*>*)

text_raw {*

  \renewcommand{\slidecaption}{ITP, 24 July 2013}

  \newcommand{\bl}[1]{#1}                        

  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

  \mode<presentation>{

  \begin{frame}

  \frametitle{%

  \begin{tabular}{@ {}c@ {}}

  \\[-3mm]

  {\fontsize{20}{20}\selectfont{}Mechanising Turing Machines and}\\[-2mm] 

  {\fontsize{20}{20}\selectfont{}Computability Theory in Isabelle}\\[-3mm] 

  \end{tabular}}

  \bigskip\medskip\medskip

  \begin{center}

  \begin{tabular}{c@ {\hspace{1cm}}c}

  \includegraphics[scale=0.29]{jian.jpg}  &

  \includegraphics[scale=0.034]{xingyuan.jpg} \\

  Jian Xu & Xingyuan Zhang\\[-3mm]

  \end{tabular}\\[3mm]

  \small PLA University of Science and Technology

  \end{center}

  \begin{center}

  Christian Urban\\[0mm]

  \small King's College London

  \end{center}

  \end{frame}}

  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

*}

text_raw {*

  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

  \mode<presentation>{

  \begin{frame}[c]

  \frametitle{Why Turing Machines?}%

  \begin{itemize}

  \item At the beginning, it was just a student project

  about computability.\smallskip

  \begin{center}

  \begin{tabular}{c}

  \includegraphics[scale=0.3]{boolos.jpg}\\[-2mm]

  \footnotesize Computability and Logic (5th.~ed)\\[-2mm]

  \footnotesize Boolos, Burgess and Jeffrey\\[2mm]

  \end{tabular}

  \end{center}

  \item found an inconsistency in the definition of halting computations

  (Chap.~3 vs Chap.~8)

  \end{itemize}

  \end{frame}}

  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

*}

text_raw {*

  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

  \mode<presentation>{

  \begin{frame}[c]

  \frametitle{Some Previous Works}%

  \begin{itemize}

  \item Norrish formalised computability theory in HOL starting

  from the lambda-calculus\smallskip 

  \begin{itemize}

  \item \textcolor{gray}{for technical reasons we could not follow his work}

  \item \textcolor{gray}{some proofs use TMs (Wang tilings)}

  \end{itemize}

  \bigskip

  \item Asperti and Ricciotti formalised TMs in Matita\smallskip

  \begin{itemize}

  \item \textcolor{gray}{no undecidability result $\Rightarrow$ interest in complexity}

  \item \textcolor{gray}{their UTM operates on a different alphabet than the TMs it simulates}

  \begin{quote}

  \textcolor{gray}{"In particular, the fact that the universal machine operates with a different 

  alphabet with respect to the machines it simulates is annoying." [Asperti and Ricciotti]}

  \end{quote}

  \end{itemize}

  \end{itemize}

  \end{frame}}

  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

*}

text_raw {*

  \tikzstyle{every node}=[node distance=25mm,text height=1.5ex, text depth=.25ex]

  \tikzstyle{node1}=[rectangle, minimum size=12mm, rounded corners=3mm, very thick, 

                     draw=black!50, top color=white, bottom color=black!20]

  \tikzstyle{node2}=[rectangle, minimum size=12mm, rounded corners=3mm, very thick, 

                     draw=red!70, top color=white, bottom color=red!50!black!20]

  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

  \mode<presentation>{

  \begin{frame}[c]

  \frametitle{The Big Picture}%

  \begin{center}

  \begin{tikzpicture}

  \matrix[ampersand replacement=\&,column sep=13mm, row sep=5mm]

  { \node (def1)   [node1] {\large\hspace{1mm}TMs\hspace{1mm}\mbox{}}; \&

    \node (proof1) [node1] {\begin{tabular}{c}Register\\Machines\end{tabular}}; \&

    \node (alg1)   [node1] {\begin{tabular}{c}Recursive\\ Functions\end{tabular}}; \\    

  };

  \draw[->,black!50,line width=2mm] (proof1) -- (def1);

  \draw[<-,black!50,line width=2mm] (proof1) -- (alg1);

  \end{tikzpicture}

  \end{center}

  \only<2->{

  \begin{textblock}{3}(8.3,4.0)

  \begin{tikzpicture}

  \node at (0,0) [single arrow, shape border rotate=270, fill=black!50,text=white]{};

  \draw (0,1) node {\begin{tabular}{l}verified\\[-1mm] translator\end{tabular}};

  \end{tikzpicture}

  \end{textblock}

  \begin{textblock}{3}(3.1,4.0)

  \begin{tikzpicture}

  \node at (0,0) [single arrow, shape border rotate=270, fill=black!50,text=white]{};

  \draw (0,1) node {\begin{tabular}{l}verified\\[-1mm] translator\end{tabular}};

  \end{tikzpicture}

  \end{textblock}}

  \only<3->{

  \begin{textblock}{4}(10.9,9.4)

  \begin{tikzpicture}

  \draw (0,0) node {\begin{tabular}{l}UF\end{tabular}};

  \end{tikzpicture}

  \end{textblock}

  \begin{textblock}{3}(1,10.0)

  \begin{tikzpicture}

  \draw (0,0) node {\small\begin{tabular}{l}undecidability\\of the halting\\ problem\end{tabular}};

  \end{tikzpicture}

  \end{textblock}}

  \only<4->{

  \begin{textblock}{4}(4.2,12.4)

  \begin{tikzpicture}

  \draw (0,0) node {\begin{tabular}{l}a correct UTM by translation\end{tabular}};

  \end{tikzpicture}

  \end{textblock}}

  \end{frame}}

  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

*}

text_raw {*

  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

  \mode<presentation>{

  \begin{frame}[c]

  \frametitle{Turing Machines}%

  \begin{itemize}

  \item tapes are lists and contain @{text 0}s or @{text 1}s only

  \begin{center}

\begin{tikzpicture}[scale=1]

  \draw[very thick] (-3.0,0)   -- ( 3.0,0);

  \draw[very thick] (-3.0,0.5) -- ( 3.0,0.5);

  \draw[very thick] (-0.25,0)   -- (-0.25,0.5);

  \draw[very thick] ( 0.25,0)   -- ( 0.25,0.5);

  \draw[very thick] (-0.75,0)   -- (-0.75,0.5);

  \draw[very thick] ( 0.75,0)   -- ( 0.75,0.5);

  \draw[very thick] (-1.25,0)   -- (-1.25,0.5);

  \draw[very thick] ( 1.25,0)   -- ( 1.25,0.5);

  \draw[very thick] (-1.75,0)   -- (-1.75,0.5);

  \draw[very thick] ( 1.75,0)   -- ( 1.75,0.5);

  \draw[very thick] ( 3.0,0)   -- ( 3.0,0.5);

  \draw[very thick] (-3.0,0)   -- (-3.0,0.5);

  \draw[rounded corners=1mm] (-0.35,-0.1) rectangle (0.35,0.6);

  \draw[fill]     (1.35,0.1) rectangle (1.65,0.4);

  \draw[fill]     (0.85,0.1) rectangle (1.15,0.4);

  \draw[fill]     (-0.35,0.1) rectangle (-0.65,0.4);

  \draw[fill]     (-1.65,0.1) rectangle (-1.35,0.4);

  \draw (-0.25,0.8) -- (-0.25,-0.8);

  \draw[<->] (-1.25,-0.7) -- (0.75,-0.7);

  \node [anchor=base] at (-0.85,-0.5) {\small left list\;\;\;\;\mbox{}};

  \node [anchor=base] at (0.40,-0.5) {\small \mbox{}\;\;\;\;right list};

  \node [anchor=base] at (0.1,0.7) {\small \;\;head};

  \node [anchor=base] at (-2.2,0.2) {\ldots};

  \node [anchor=base] at ( 2.3,0.2) {\ldots};

  \end{tikzpicture}

  \end{center}\pause

  \item @{text steps} function:

  \begin{quote}\rm

  What does the TM calculate after it has executed @{text n} steps?

  \end{quote}\pause

  \item designate the @{text 0}-state as "halting state" and remain there 

  forever, i.e.~have a @{text Nop}-action

  \end{itemize}

  \end{frame}}

  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

*}

text_raw {*

  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

  \mode<presentation>{

  \begin{frame}[c]

  \frametitle{Register Machines}%

  \begin{itemize}

  \item programs are lists of instructions

  \begin{center}

  \begin{tabular}{@ {}rcl@ {\hspace{8mm}}l}

  @{text "I"} & $::=$  & @{term "Goto L\<iota>"}

  & \textcolor{black!60}{jump to instruction @{text L}}\\[1mm]

  & $\mid$ & @{term "Inc R\<iota>"} & \textcolor{black!60}{increment register @{text "R"} by one}\\[1mm]

  & $\mid$ & @{term "Dec R\<iota> L\<iota>"} & \textcolor{black!60}{if the content of @{text R} is non-zero,}\\

  & & & \textcolor{black!60}{then decrement it by one}\\

  & & & \textcolor{black!60}{otherwise jump to instruction @{text L}}

  \end{tabular}

  \end{center}

  \end{itemize}

  \only<2->{

  \begin{textblock}{4}(0.3,11.8)

  \begin{tikzpicture}

  \node[ellipse callout, fill=red, callout absolute pointer={(-0.2,1)}] 

   at (0, 0){\large\fontspec{Chalkduster}\textcolor{yellow}{Spaghetti Code!}};

  \end{tikzpicture}

  \end{textblock}}

  \end{frame}}

  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

*}

text_raw {*

  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

  \mode<presentation>{

  \begin{frame}[c]

  \frametitle{Recursive Functions}%

  \begin{itemize}

  \item[] 

  \begin{center}

  \begin{tabular}{@ {}rcl@ {\hspace{8mm}}l}

  @{text "rec"} & $::=$  & @{term "Z"} & \textcolor{black!60}{zero-function}\\[1mm]

  & $\mid$ & @{term "S"} & \textcolor{black!60}{successor-function}\\[1mm]

  & $\mid$ & @{term "id n m"} & \textcolor{black!60}{projection}\\[1mm]

  & $\mid$ & @{term "Cn n f gs"} & \textcolor{black!60}{composition}\\[1mm]

  & $\mid$ & @{term "Pr n f g"} & \textcolor{black!60}{primitive recursion}\\[1mm]

  & $\mid$ & @{term "Mn n f"} & \textcolor{black!60}{minimisation}

  \end{tabular}

  \end{center}\bigskip

  \item @{text "eval :: rec \<Rightarrow> nat list \<Rightarrow> nat"}\\ 

  can be defined by simple recursion\\ (HOL has @{term "Least"})

  \item \small you define

  \begin{itemize}

  \item addition, multiplication, logical operations, quantifiers\ldots

  \item coding of numbers (Cantor encoding), UF

  \end{itemize}

  \end{itemize}

  \end{frame}}

  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

*}

text_raw {*

  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

  \mode<presentation>{

  \begin{frame}[c]

  \frametitle{Copy Turing Machine}%

  \begin{itemize}

  \item TM that copies a number on the input tape

  \begin{center}

  @{text "copy \<equiv> cbegin ; cloop ; cend"}

  \end{center}\smallskip

  \begin{center}

  \begin{tikzpicture}[scale=0.7]

  \node [anchor=base] at (2.2,0.1) {\small$\Rightarrow$};

  \node [anchor=base] at (5.6,0.1) {\small$\Rightarrow$};

  \node [anchor=base] at (10.5,0.1) {\small$\Rightarrow$};

  \node [anchor=base] at (2.2,-0.8) {\small$\overbrace{@{text cbegin}}^{}$};

  \node [anchor=base] at (5.6,-0.8) {\small$\overbrace{@{text cloop}}^{}$};

  \node [anchor=base] at (10.5,-0.8) {\small$\overbrace{@{text cend}}^{}$};

  \begin{scope}[shift={(0.5,0)}]

  \draw[very thick] (-0.25,0)   -- ( 1.25,0);

  \draw[very thick] (-0.25,0.5) -- ( 1.25,0.5);

  \draw[very thick] (-0.25,0)   -- (-0.25,0.5);

  \draw[very thick] ( 0.25,0)   -- ( 0.25,0.5);

  \draw[very thick] ( 0.75,0)   -- ( 0.75,0.5);

  \draw[very thick] ( 1.25,0)   -- ( 1.25,0.5);

  \draw[rounded corners=1mm] (-0.35,-0.1) rectangle (0.35,0.6);

  \draw[fill]     (-0.15,0.1) rectangle (0.15,0.4);

  \draw[fill]     ( 0.35,0.1) rectangle (0.65,0.4);

  \draw[fill]     ( 0.85,0.1) rectangle (1.15,0.4);

  \end{scope}

  \begin{scope}[shift={(2.9,0)}]

  \draw[very thick] (-0.25,0)   -- ( 2.25,0);

  \draw[very thick] (-0.25,0.5) -- ( 2.25,0.5);

  \draw[very thick] (-0.25,0)   -- (-0.25,0.5);

  \draw[very thick] ( 0.25,0)   -- ( 0.25,0.5);

  \draw[very thick] ( 0.75,0)   -- ( 0.75,0.5);

  \draw[very thick] ( 1.25,0)   -- ( 1.25,0.5);

  \draw[very thick] ( 1.75,0)   -- ( 1.75,0.5);

  \draw[very thick] ( 2.25,0)   -- ( 2.25,0.5);

  \draw[rounded corners=1mm] (0.15,-0.1) rectangle (0.85,0.6);

  \draw[fill]     (-0.15,0.1) rectangle (0.15,0.4);

  \draw[fill]     ( 0.35,0.1) rectangle (0.65,0.4);

  \draw[fill]     ( 0.85,0.1) rectangle (1.15,0.4);

  \draw[fill]     ( 1.85,0.1) rectangle (2.15,0.4);

  \end{scope}

  \begin{scope}[shift={(6.8,0)}]

  \draw[very thick] (-0.75,0)   -- ( 3.25,0);

  \draw[very thick] (-0.75,0.5) -- ( 3.25,0.5);

  \draw[very thick] (-0.75,0)   -- (-0.75,0.5);

  \draw[very thick] (-0.25,0)   -- (-0.25,0.5);

  \draw[very thick] ( 0.25,0)   -- ( 0.25,0.5);

  \draw[very thick] ( 0.75,0)   -- ( 0.75,0.5);

  \draw[very thick] ( 1.25,0)   -- ( 1.25,0.5);

  \draw[very thick] ( 1.75,0)   -- ( 1.75,0.5);

  \draw[very thick] ( 2.25,0)   -- ( 2.25,0.5);

  \draw[very thick] ( 2.75,0)   -- ( 2.75,0.5);

  \draw[very thick] ( 3.25,0)   -- ( 3.25,0.5);

  \draw[rounded corners=1mm] (-0.35,-0.1) rectangle (0.35,0.6);

  \draw[fill]     (-0.15,0.1) rectangle (0.15,0.4);

  \draw[fill]     ( 2.35,0.1) rectangle (2.65,0.4);

  \draw[fill]     ( 2.85,0.1) rectangle (3.15,0.4);

  \draw[fill]     ( 1.85,0.1) rectangle (2.15,0.4);

  \end{scope}

  \begin{scope}[shift={(11.7,0)}]

  \draw[very thick] (-0.75,0)   -- ( 3.25,0);

  \draw[very thick] (-0.75,0.5) -- ( 3.25,0.5);

  \draw[very thick] (-0.75,0)   -- (-0.75,0.5);

  \draw[very thick] (-0.25,0)   -- (-0.25,0.5);

  \draw[very thick] ( 0.25,0)   -- ( 0.25,0.5);

  \draw[very thick] ( 0.75,0)   -- ( 0.75,0.5);

  \draw[very thick] ( 1.25,0)   -- ( 1.25,0.5);

  \draw[very thick] ( 1.75,0)   -- ( 1.75,0.5);

  \draw[very thick] ( 2.25,0)   -- ( 2.25,0.5);

  \draw[very thick] ( 2.75,0)   -- ( 2.75,0.5);

  \draw[very thick] ( 3.25,0)   -- ( 3.25,0.5);

  \draw[rounded corners=1mm] (-0.35,-0.1) rectangle (0.35,0.6);

  \draw[fill]     (-0.15,0.1) rectangle (0.15,0.4);

  \draw[fill]     ( 2.35,0.1) rectangle (2.65,0.4);

  \draw[fill]     ( 2.85,0.1) rectangle (3.15,0.4);

  \draw[fill]     ( 1.85,0.1) rectangle (2.15,0.4);

  \draw[fill]     ( 0.35,0.1) rectangle (0.65,0.4);

  \draw[fill]     ( 0.85,0.1) rectangle (1.15,0.4);

  \end{scope}

  \end{tikzpicture}

  \end{center}\bigskip

  \footnotesize

  \begin{center}

  \begin{tabular}{@ {\hspace{-8mm}}c@ {\hspace{2mm}}c@ {\hspace{2mm}}c}

  \begin{tabular}[t]{@ {}l@ {}}

  @{text cbegin} @{text "\<equiv>"}\\

  \hspace{2mm}@{text "["}@{text "(W\<^bsub>0\<^esub>, 0), (R, 2), (R, 3),"}\\

  \hspace{2mm}\phantom{@{text "["}}@{text "(R, 2), (W\<^bsub>1\<^esub>, 3), (L, 4),"}\\

  \hspace{2mm}\phantom{@{text "["}}@{text "(L, 4), (L, 0)"}@{text "]"} 

  \end{tabular}

  &

  \begin{tabular}[t]{@ {}l@ {}}

  @{text cloop} @{text "\<equiv>"}\\

  \hspace{2mm}@{text "["}@{text "(R, 0), (R, 2), (R, 3),"}\\

  \hspace{2mm}\phantom{@{text "["}}@{text "(W\<^bsub>0\<^esub>, 2), (R, 3), (R, 4),"}\\

  \hspace{2mm}\phantom{@{text "["}}@{text "(W\<^bsub>1\<^esub>, 5), (R, 4), (L, 6),"}\\

  \hspace{2mm}\phantom{@{text "["}}@{text "(L, 5), (L, 6), (L, 1)"}@{text "]"}