--- a/Paper/Paper.thy	Tue Feb 05 09:22:56 2013 +0000
+++ b/Paper/Paper.thy	Tue Feb 05 09:36:21 2013 +0000
@@ -1231,7 +1231,7 @@
   corresponding register is @{text 0}. For this we have a Turing machine program
   with @{text 16} states. 
 
-  Finally, having a turing machine for each abacus instruction we need
+  Finally, having a Turing machine for each abacus instruction we need
   to ``stitch'' the Turing machines together into one so that each
   Turing machine component transitions to next one, just like in
   the abacus programs. One last problem to overcome is that an abacus
@@ -1243,29 +1243,37 @@
   While generating the Turing machine program for an abacus
   program is not too difficult to formalise, the problem is that it
   contains @{text Goto}s all over the place. The unfortunate result is
-  are needed to translate each abacus instructionthat we cannot
+  are needed to translate each abacus instruction that we cannot
   use our Hoare-rules for reasoning about sequentially composed
-  programs. Instead we have to treat the Turing machine as one ``block''
+  programs. Instead we have to treat the Turing machine as one
+  are needed to translate each abacus instruction``block''
   and show as invariant that it performs the same operations
-  as the abacus program. For this we have to show that for each 
+  as the abacus program. For this we have to show that for each
   configuration of an abacus machine the @{term step}-function
   is simulated by zero or more steps in our constructed Turing
-  machine. 
+  machine. This leads to a rather large ``monolithic'' overall
+  correctness proof that on the conceptual level is difficult to 
+  break down into smaller components. 
+  
+  %We were able to simplify the proof somewhat
+*}
 
 
+section {* Recursive Functions and a Universal Turing Machine *}
+
+text {*
+
 *}
 
-
-section {* Recursive Functions *}
-
+(*
 section {* Wang Tiles\label{Wang} *}
 
 text {*
   Used in texture mapings - graphics
 *}
-
+*)
 
-section {* Related Work *}
+section {* Conclusion *}
 
 text {*
   We have formalised the main results from three chapters in the
@@ -1282,7 +1290,7 @@
 
   The most closely related work is by Norrish \cite{Norrish11}, and
   Asperti and Ricciotti \cite{AspertiRicciotti12}. Norrish bases his
-  approach on lambda-terms. For this he introduced a clever rewriting
+  approach on $\lambda$-terms. For this he introduced a clever rewriting
   technology based on combinators and de-Bruijn indices for rewriting
   modulo $\beta$-equivalence (to keep it manageable)
 

Binary file paper.pdf has changed