
diff -r 447b433b67fa -r b49ff5328a66 Slides/Slides3.thy
--- a/Slides/Slides3.thy	Sat Nov 23 13:23:53 2013 +0000
+++ b/Slides/Slides3.thy	Sun Nov 24 14:04:04 2013 +0000
@@ -120,7 +120,7 @@
 
 
 text_raw {*
-  \renewcommand{\slidecaption}{ITP, 24 July 2013}
+  \renewcommand{\slidecaption}{Imperial College, 24 November 2013}
   \newcommand{\bl}[1]{#1}                        
   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
   \mode<presentation>{
@@ -128,8 +128,9 @@
   \frametitle{%
   \begin{tabular}{@ {}c@ {}}
   \\[-3mm]
-  {\fontsize{20}{20}\selectfont{}Mechanising Turing Machines and}\\[-2mm] 
-  {\fontsize{20}{20}\selectfont{}Computability Theory in Isabelle}\\[-3mm] 
+  {\fontsize{30}{30}\selectfont{}Turing Machines and}\\[-1mm]  
+  {\fontsize{30}{30}\selectfont{}Separation Logic}\\[0mm]
+  {\fontsize{22}{22}\selectfont{}(Work in Progress)}\\[-3mm] 
   \end{tabular}}
   
   \bigskip\medskip\medskip
@@ -159,8 +160,8 @@
   \frametitle{Why Turing Machines?}%
 
   \begin{itemize}
-  \item At the beginning, it was just a student project
-  about computability.\smallskip
+  \item we wanted to formalise computability theory
+  \item at the beginning, it was just a student project\smallskip
 
   \begin{center}
   \begin{tabular}{c}
@@ -174,6 +175,28 @@
   (Chap.~3 vs Chap.~8)
   \end{itemize}
 
+  \only<2->{
+  \begin{textblock}{1}(0.7,4)
+  \begin{tikzpicture}
+  \draw (0,0) node[inner sep=2mm,fill=cream, ultra thick, draw=red, rounded corners=2mm] 
+  {\normalsize
+  \begin{minipage}{11cm}
+  \begin{quote}\rm
+  \begin{itemize}
+  \item is a fantastic model of low-level code
+  \item completely unstructured\makebox[0mm][10mm]{\mbox{}}\;\; 
+  \only<2>{\textcolor{cream}{\fontspec{Chalkduster}Spaghetti Code}}%
+  \only<3->{\textcolor{red}{\fontspec{Chalkduster}Spaghetti Code}}
+  \bigskip
+  \item good testbed for verification techniques
+  \item Can we verify a program with 38 Mio instructions?
+  \item we can delay implementing a concrete machine model (for OS/low-level code verification)
+  \end{itemize}
+  \end{quote}
+  \end{minipage}};
+  \end{tikzpicture}
+  \end{textblock}}
+
   \end{frame}}
   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
 *}
@@ -182,7 +205,10 @@
   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
   \mode<presentation>{
   \begin{frame}[c]
-  \frametitle{Some Previous Works}%
+  \frametitle{
+  \begin{tabular}{c}Some Previous Works\\[-5mm]
+  \hspace{3.5cm}\small (but not interested in low-level code)
+  \end{tabular}}%
 
   \begin{itemize}
   \item Norrish formalised computability theory in HOL starting
@@ -199,7 +225,7 @@
   \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]}
+  alphabet with respect to the machines it simulates is annoying." (Asperti and Ricciotti)}
   \end{quote}
   \end{itemize}
   \end{itemize}
@@ -216,53 +242,66 @@
                      draw=red!70, top color=white, bottom color=red!50!black!20]
   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
   \mode<presentation>{
-  \begin{frame}[c]
+  \begin{frame}[t]
   \frametitle{The Big Picture}%
 
+  \mbox{}\\[19mm]
   \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}}; \\    
+  { \node (tm)   [node1] {\large\hspace{1mm}TMs\hspace{1mm}\mbox{}}; \&
+    \node (reg) [node1] {\begin{tabular}{c}Register\\Machines\end{tabular}}; \&
+    \node (rf)   [node1] {\begin{tabular}{c}Recursive\\ Functions\end{tabular}}; \\    
   };
 
-  \draw[->,black!50,line width=2mm] (proof1) -- (def1);
-  \draw[<-,black!50,line width=2mm] (proof1) -- (alg1);
+  \only<2->{\draw[->,black!50,line width=2mm] (reg) -- (tm);}
+  \only<2->{\draw[<-,black!50,line width=2mm] (reg) -- (rf);}
+
+  \only<4->{
+   \draw [<-, black!50,line width=2mm, rounded corners]
+     %  start right of digit.east, that is, at the point that is the
+     %  linear combination of digit.east and the vector (2mm,0pt). We
+     %  use the ($ ... $) notation for computing linear combinations
+     ($ (rf.south) + (0mm,0) $)
+     %  Now go down
+     -- ++(0,-2.5)
+     %  And back to the left of digit.west
+     -| ($ (tm.south) - (0mm,0) $);}
   
   \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)
+  \only<1->{
+  \begin{textblock}{3}(1,4.9)
   \begin{tikzpicture}
   \draw (0,0) node {\small\begin{tabular}{l}undecidability\\of the halting\\ problem\end{tabular}};
   \end{tikzpicture}
   \end{textblock}}
 
+  \only<2->{
+  \begin{textblock}{3}(8.3,8.4)
+  \begin{tikzpicture}
+  \node at (0,0) [single arrow, shape border rotate=90, 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,8.4)
+  \begin{tikzpicture}
+  \node at (0,0) [single arrow, shape border rotate=90, 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}(12.5,5.8)
+  \begin{tikzpicture}
+  \draw (0,0) node {\begin{tabular}{l}UF\end{tabular}};
+  \end{tikzpicture}
+  \end{textblock}}
+
   \only<4->{
-  \begin{textblock}{4}(4.2,12.4)
+  \begin{textblock}{4}(3.3,13.3)
   \begin{tikzpicture}
   \draw (0,0) node {\begin{tabular}{l}a correct UTM by translation\end{tabular}};
   \end{tikzpicture}
@@ -379,7 +418,7 @@
   \end{center}\bigskip
 
   \item @{text "eval :: rec \<Rightarrow> nat list \<Rightarrow> nat"}\\ 
-  can be defined by simple recursion\\ (HOL has @{term "Least"})
+  \hspace{3mm}can be defined by recursion (HOL has @{term "Least"})
   
   \item \small you define
   \begin{itemize}
@@ -524,6 +563,80 @@
 *}
 
 text_raw {*
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+  \mode<presentation>{
+  \begin{frame}[c]
+  \frametitle{Dither Machine}%
+
+  \begin{itemize}
+  \item TM that is the identity with @{text "1"} and loops with @{text "0"}
+  \smallskip
+
+\begin{center}
+  \begin{tabular}{l@ {\hspace{3mm}}lcl}
+  & \multicolumn{1}{c}{start tape}\\[1mm]
+  \raisebox{2mm}{halting case:} &
+  \begin{tikzpicture}[scale=0.8]
+  \draw[very thick] (-2,0)   -- ( 0.75,0);
+  \draw[very thick] (-2,0.5) -- ( 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] ( 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);
+  \node [anchor=base] at (-1.7,0.2) {\ldots};
+  \end{tikzpicture} 
+  & \raisebox{2mm}{$\;\;\large\Rightarrow\;\;$} &
+  \begin{tikzpicture}[scale=0.8]
+  \draw[very thick] (-2,0)   -- ( 0.75,0);
+  \draw[very thick] (-2,0.5) -- ( 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] ( 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);
+  \node [anchor=base] at (-1.7,0.2) {\ldots};
+  \end{tikzpicture}\\
+
+  \raisebox{2mm}{non-halting case:} &
+  \begin{tikzpicture}[scale=0.8]
+  \draw[very thick] (-2,0)   -- ( 0.25,0);
+  \draw[very thick] (-2,0.5) -- ( 0.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);
+  \node [anchor=base] at (-1.7,0.2) {\ldots};
+  \end{tikzpicture} 
+  & \raisebox{2mm}{$\;\;\large\Rightarrow\;\;$} &
+  \raisebox{2mm}{loops}
+  \end{tabular}
+  \end{center}\bigskip
+
+  \small
+  \begin{center}
+  \begin{tabular}[t]{@ {}l@ {}}
+  @{text dither} @{text "\<equiv>"} @{text "["}@{text "(W\<^bsub>0\<^esub>, 1), (R, 2), (L, 1), (L, 0)"}@{text "]"}
+  \end{tabular}
+  \end{center}
+
+
+  \end{itemize}
+
+
+  \end{frame}}
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
+*}
+
+text_raw {*
   \definecolor{mygrey}{rgb}{.80,.80,.80}
   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
   \mode<presentation>{
@@ -609,7 +722,7 @@
   
   \only<2>{
   \begin{itemize}
-  \item Suppose @{text H} decides @{text contra} called with the code 
+  \item Suppose @{text H} decides whether @{text contra} called with the code 
   of @{text contra} halts, then\smallskip
 
   \begin{center}\small
@@ -634,8 +747,8 @@
   \end{itemize}}
   \only<3>{
   \begin{itemize}
-  \item Suppose @{text H} decides @{text contra} called with the code 
-  of @{text contra} does \emph{not} halt, then\\[-8mm]\mbox{}
+  \item Suppose @{text H} decides wether @{text contra} called with the code 
+  of @{text contra} does \alert{not} halt, then\\[-8mm]\mbox{}
 
   \begin{center}\small
   \begin{tabular}{@ {}l@ {}}
@@ -723,10 +836,8 @@
   URM      & @{text 2} Mio instructions\\
   UTM      & @{text 38} Mio states\\
   \end{tabular}
-  \end{center}\smallskip\pause
+  \end{center}\smallskip
 
-  \item an observation: our treatment of recursive functions is a mini-version
-  of the work by\\ Myreen \& Owens about deeply embedding HOL
   \end{itemize}
  
   \only<1>{
@@ -745,6 +856,35 @@
   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
   \mode<presentation>{
   \begin{frame}[c]
+  \frametitle{{\fontsize{20}{20}\selectfont{}The Trouble With Hoare-Triples}}%
+
+  \begin{itemize}
+  \item Whenever we wanted to prove 
+
+  \begin{center}
+  \large @{text "{P} p {Q}"}
+  \end{center}\bigskip\medskip
+ 
+  \item[@{text "(1)"}] we had to find invariants for each state\\ \textcolor{gray}{(not easy)}
+
+  
+  
+  \item[@{text "(2)"}] we had to find a termination order proving that @{text p} terminates
+  \textcolor{gray}{(not easy either)}
+  \end{itemize}\pause
+  
+  \begin{center}
+  \alert{very little opportunity for automation}
+  \end{center}
+
+  \end{frame}}
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
+*} 
+
+text_raw {*
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+  \mode<presentation>{
+  \begin{frame}[c]
   \frametitle{\begin{tabular}{@ {}c@ {}}\Large Inspiration from other Works\end{tabular}}%
 
   \onslide<3->{
@@ -777,9 +917,9 @@
 
   \begin{itemize}
   \item an idea from Jensen, Benton \& Kennedy who looked at X86 
-  assembly programs and macros\bigskip
+  assembler programs and macros\bigskip
   
-  \item assembly for TMs:\medskip
+  \item assembler for TMs:\medskip
   \begin{center}
   \begin{tabular}{l}
   @{text "move_one_left"} @{text "\<equiv>"}\\ 
@@ -829,26 +969,90 @@
 text_raw {*
   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
   \mode<presentation>{
-  \begin{frame}[c]
-  \frametitle{{\large The Trouble With Hoare-Triples}}%
+  \begin{frame}[t]
+  \frametitle{An RM-API with TMs}%
+
+  \begin{center}
+  \begin{tikzpicture}
+  \matrix[ampersand replacement=\&,column sep=13mm, row sep=5mm]
+  { \node (tm)   [node1, minimum size=44mm] {\mbox{}}; \&
+    \node (rf)   [node1] {\begin{tabular}{c}Recursive\\ Functions\end{tabular}}; \\    
+  };
+
+  \draw[->,black!50,line width=2mm] (rf) -- (tm);
+  
+  \node [above, rotate=90] at (tm.east) {\textcolor{gray}{Reg.Mach. API}};
+  \node [below right] at (tm.north west) {\textcolor{gray}{Macros}};
+  \node [node1] at (tm) {\large\hspace{1mm}TMs\hspace{1mm}\mbox{}}; 
+  
+
+  \end{tikzpicture}
+  \end{center}
 
   \begin{itemize}
-  \item Whenever we wanted to prove 
+  \item Suppose the first four registers of an RM contain 1,2,0 and 3, then the encoding is
 
   \begin{center}
-  \large @{text "{P} p {Q}"}
-  \end{center}\bigskip\medskip
- 
-  \item[@{text "(1)"}] we had to find invariants for each state\\ \textcolor{gray}{(not easy)}
+  \begin{tikzpicture}[scale=1]
+
+  \draw[very thick] (-0.25,0)   -- ( 8.25,0);
+  \draw[very thick] (-0.25,0.5) -- ( 8.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[very thick] ( 2.75,0)   -- ( 2.75,0.5);  
+  \draw[very thick] ( 3.25,0)   -- ( 3.25,0.5); 
+  \draw[very thick] ( 3.75,0)   -- ( 3.75,0.5); 
+  \draw[very thick] ( 4.25,0)   -- ( 4.25,0.5); 
+  \draw[very thick] ( 4.75,0)   -- ( 4.75,0.5); 
+  \draw[very thick] ( 5.25,0)   -- ( 5.25,0.5); 
+  \draw[very thick] ( 5.75,0)   -- ( 5.75,0.5); 
+  \draw[very thick] ( 6.25,0)   -- ( 6.25,0.5); 
+  \draw[very thick] ( 6.75,0)   -- ( 6.75,0.5); 
 
-  
-  
-  \item[@{text "(2)"}] we had to find a termination order proving that @{text p} terminates
-  \textcolor{gray}{(not easy either)}
-  \end{itemize}\pause
-  
+  \draw[fill]     (-0.15,0.1) rectangle (0.15,0.4);
+  \draw[fill]     ( 0.35,0.1) rectangle (0.65,0.4);
+  \draw[fill]     ( 1.35,0.1) rectangle (1.65,0.4);
+  \draw[fill]     ( 1.85,0.1) rectangle (2.15,0.4);
+  \draw[fill]     ( 2.35,0.1) rectangle (2.65,0.4);
+  \draw[fill]     ( 3.35,0.1) rectangle (3.65,0.4);
+  \draw[fill]     ( 4.35,0.1) rectangle (4.65,0.4);
+  \draw[fill]     ( 4.85,0.1) rectangle (5.15,0.4);
+  \draw[fill]     ( 5.35,0.1) rectangle (5.65,0.4);
+  \draw[fill]     ( 5.85,0.1) rectangle (6.15,0.4);
+  \end{tikzpicture}
+
+  \end{center}
+  \end{itemize}
+
+  \end{frame}}
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
+*}
+
+text_raw {*
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+  \mode<presentation>{
+  \begin{frame}[c]
+  \frametitle{Inc a}%
+
   \begin{center}
-  \alert{very little opportunity for automation}
+  \begin{tabular}{@ {\hspace{-10mm}}l}
+  @{text "Inc a"} @{text "\<equiv>"} \\
+  \hspace{16mm} @{text "locate a"} @{text ";"}\\
+  \hspace{16mm} @{text "right_until_zero"} @{text ";"}\\
+  \hspace{16mm} @{text "move_right"} @{text ";"}\\
+  \hspace{16mm} @{text "shift_right"} @{text ";"}\\
+  \hspace{16mm} @{text "move_left"} @{text ";"}\\
+  \hspace{16mm} @{text "left_until_double_zero"} @{text ";"}\\
+  \hspace{16mm} @{text "write_one"} @{text ";"}\\
+  \hspace{16mm} @{text "left_until_double_zero"} @{text ";"}\\
+  \hspace{16mm} @{text "move_right"} @{text ";"}\\
+  \hspace{16mm} @{text "move_right"}\\
+  \end{tabular}
   \end{center}
 
   \end{frame}}
@@ -896,8 +1100,81 @@
   \end{center}\bigskip\bigskip
 
   \normalsize
-  @{text "c"} can be\;\;\; @{text "i:[move_left_until_zero]:j"}
-  
+  \begin{center}
+  @{text "\<lbrace> st i \<star> hd v \<star> zero u \<star> ones (u + 1) v \<rbrace>"}\\
+  @{text "i:[left_until_zero]:j"}\\
+  @{text "\<lbrace> st j \<star> hd u \<star> zero u \<star> ones (u + 1) v \<rbrace>"}\\
+  \end{center}
+
+  \end{frame}}
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
+*}
+
+text_raw {*
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+  \mode<presentation>{
+  \begin{frame}[c]
+  \frametitle{Inductions over \textit{ones}}%
+
+  \begin{itemize}
+  \item What most simplifies the work is that we can do inductions over
+  the ''input'' (inductively defined assertions)\pause\medskip
+
+  \item Suppose @{text "right_until_zero"}:\bigskip
+
+    \begin{center}
+  \begin{tikzpicture}[scale=1]
+
+  \draw[very thick] (-0.25,0)   -- ( 8.25,0);
+  \draw[very thick] (-0.25,0.5) -- ( 8.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[very thick] ( 2.75,0)   -- ( 2.75,0.5);  
+  \draw[very thick] ( 3.25,0)   -- ( 3.25,0.5); 
+  \draw[very thick] ( 3.75,0)   -- ( 3.75,0.5); 
+  \draw[very thick] ( 4.25,0)   -- ( 4.25,0.5); 
+  \draw[very thick] ( 4.75,0)   -- ( 4.75,0.5); 
+  \draw[very thick] ( 5.25,0)   -- ( 5.25,0.5); 
+  \draw[very thick] ( 5.75,0)   -- ( 5.75,0.5); 
+  \draw[very thick] ( 6.25,0)   -- ( 6.25,0.5); 
+  \draw[very thick] ( 6.75,0)   -- ( 6.75,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);
+  \draw[fill]     ( 1.35,0.1) rectangle (1.65,0.4);
+  \draw[fill]     ( 1.85,0.1) rectangle (2.15,0.4);
+  \draw[fill]     ( 2.35,0.1) rectangle (2.65,0.4);
+  \draw[fill]     ( 3.35,0.1) rectangle (3.65,0.4);
+  \draw[fill]     ( 3.85,0.1) rectangle (4.15,0.4);
+  \draw[fill]     ( 4.35,0.1) rectangle (4.65,0.4);
+  \draw[fill]     ( 4.85,0.1) rectangle (5.15,0.4);
+  \draw[fill]     ( 5.35,0.1) rectangle (5.65,0.4);
+  \draw[fill]     ( 5.85,0.1) rectangle (6.15,0.4);
+
+  \path (2.75,0) edge [decorate,decoration={brace,amplitude=14pt}, thick] node[below=8pt] 
+  {\small\textcolor{gray}{@{text "ones u v"}}} (-0.25,0);
+
+  \end{tikzpicture}
+  \end{center}
+
+  \begin{center}
+  @{text "\<lbrace> st i \<star> hd u \<star> zero (v + 1) \<star> ones u v \<rbrace>"}\\
+  @{text "i:[right_until_zero]:j"}\\
+  @{text "\<lbrace> st j \<star> hd (v + 1) \<star> zero (v + 1) \<star> ones u v \<rbrace>"}\\
+  \end{center}
+  \end{itemize}
+
+  \begin{textblock}{3}(11,10)
+  \begin{tikzpicture}
+  \only<2>{\node at (0,0) [single arrow, shape border rotate=270, fill=red,text=white]{\mbox{\alert{a}}};}
+  \end{tikzpicture}
+  \end{textblock}
 
   \end{frame}}
   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
@@ -917,9 +1194,10 @@
   \end{center}\bigskip\bigskip
 
   \item for loops we often only have to do inductions on the length 
-  of the input (e.g.~how many @{text "1"}s are on the tape)\pause
+  of the input (e.g.~how many @{text "0"}s/@{text "1"}s are on the tape)
   
-  \item these macros allow us to completely get rid of register machines
+  \item no termination measures are needed
+
   \end{itemize}
   
 
@@ -931,6 +1209,58 @@
   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
   \mode<presentation>{
   \begin{frame}[c]
+  \frametitle{Register Machines}%
+
+  \begin{itemize}
+  \item We could also use Jensen's et al work to give
+  a more appropriate \alert{view}  on register machines
+
+  \begin{center}
+  @{text "\<lbrace>p\<rbrace> i:[rm_c]:j \<lbrace>q\<rbrace>"}
+  \end{center}\bigskip
+  \end{itemize}
+  
+  \small
+  \begin{itemize}
+      \item Rule for @{text "Inc"}
+
+             \begin{tabular}{rl}
+               @{text "RM."} & @{text "\<lbrace> pc i \<star> m a v \<rbrace>"} \\
+               & @{text "i:[ Inc a ]:j"} \\
+               & @{text "\<lbrace> pc j \<star> m a (Suc v)\<rbrace>"}
+             \end{tabular}
+     \item Rules for @{text "Dec"}
+     \begin{tabular}{c c}
+       \begin{tabular}{r l}
+            @{text "RM."} & @{text "\<lbrace>(pc i \<star> m a (Suc v))\<rbrace>"} \\
+          & @{text "i :[ Dec a e ]: j"} \\
+          & @{text "\<lbrace>pc j \<star> m a v\<rbrace>"}
+       \end{tabular} &
+       \begin{tabular}{r l}
+         @{text "RM."} & @{text "\<lbrace> pc i \<star> m a 0 \<rbrace>"} \\
+         & @{text "i:[ Dec a e ]:j"} \\
+         & @{text "\<lbrace> pc e \<star> m a 0 \<rbrace>"}
+       \end{tabular}
+     \end{tabular}
+    %\item Rule for @{text "Goto"}
+    %
+    %   \begin{tabular}{r l}
+    %     @{text "RM."} & @{text "\<lbrace> pc i \<rbrace>"} \\
+    %    &@{text "i:[ (Goto e) ]:j"} \\
+    %    &@{text "\<lbrace> pc e \<rbrace>"}
+    %   \end{tabular} 
+  \end{itemize}
+
+
+  \end{frame}}
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
+*}
+
+
+text_raw {*
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+  \mode<presentation>{
+  \begin{frame}[c]
   \frametitle{Conclusion}%
 
   \begin{itemize}




