diff -r 01d223421ba0 -r 44c4450152e3 utm/uncomputable.thy
--- a/utm/uncomputable.thy	Wed Dec 12 11:45:04 2012 +0000
+++ b/utm/uncomputable.thy	Fri Mar 01 17:13:32 2013 +0000
@@ -37,136 +37,110 @@
 *}
 fun tcopy_F0 :: "nat \<Rightarrow> tape \<Rightarrow> bool"
   where
-  "tcopy_F0 x tp = (let (ln, rn) = tp in 
-           list_all isBk ln & rn = replicate x Oc 
-                                   @ [Bk] @ replicate x Oc)"
+  "tcopy_F0 x (l, r) = (\<exists> i. l = Bk\<^bsup>i\<^esup> \<and> r = Oc\<^bsup>x\<^esup> @ Bk # Oc\<^bsup>x\<^esup>)"
 
 fun tcopy_F1 :: "nat \<Rightarrow> tape \<Rightarrow> bool"
   where
-   "tcopy_F1 x (ln, rn) = (ln = [] & rn = replicate x Oc)"
+   "tcopy_F1 x (l, r) = (l = [] \<and> r = Oc\<^bsup>x\<^esup>)"
 
 fun tcopy_F2 :: "nat \<Rightarrow> tape \<Rightarrow> bool"
-  where
-  "tcopy_F2 0 tp = False" |
-  "tcopy_F2 (Suc x) (ln, rn) = (length ln > 0 & 
-             ln @ rn = replicate (Suc x) Oc)"
+  where 
+  "tcopy_F2 x (l, r) = (\<exists> i j. i > 0 \<and> i + j = x \<and> l = Oc\<^bsup>i\<^esup> \<and> r = Oc\<^bsup>j\<^esup>)"
 
 fun tcopy_F3 :: "nat \<Rightarrow> tape \<Rightarrow> bool"
   where
-  "tcopy_F3 0 tp = False" |
-  "tcopy_F3 (Suc x) (ln, rn) = 
-            (ln = Bk # replicate (Suc x) Oc & length rn <= 1)"
+  "tcopy_F3 x (l, r) = (x > 0 \<and> l = Bk # Oc\<^bsup>x\<^esup> \<and> tl r = [])"
 
 fun tcopy_F4 :: "nat \<Rightarrow> tape \<Rightarrow> bool"
   where
-  "tcopy_F4 0 tp = False" | 
-  "tcopy_F4 (Suc x) (ln, rn) = 
-           ((ln = replicate x Oc & rn = [Oc, Bk, Oc])
-           | (ln = replicate (Suc x) Oc & rn = [Bk, Oc])) "
+  "tcopy_F4 x (l, r) = (x > 0 \<and> ((l = Oc\<^bsup>x\<^esup> \<and> r = [Bk, Oc]) \<or> (l = Oc\<^bsup>x - 1\<^esup> \<and> r = [Oc, Bk, Oc])))"
+
+fun tcopy_F5_loop :: "nat \<Rightarrow> tape \<Rightarrow> bool"
+  where
+  "tcopy_F5_loop x (l, r) = 
+       (\<exists> i j. i + j + 1 = x \<and> l = Oc\<^bsup>i\<^esup> \<and> r = Oc # Oc # Bk\<^bsup>j\<^esup> @ Oc\<^bsup>j\<^esup> \<and> j > 0)"
+
+fun tcopy_F5_exit :: "nat \<Rightarrow> tape \<Rightarrow> bool"
+  where
+  "tcopy_F5_exit x (l, r) = 
+      (l = [] \<and> r = Bk # Oc # Bk\<^bsup>x\<^esup> @ Oc\<^bsup>x\<^esup> \<and> x > 0 )"
 
 fun tcopy_F5 :: "nat \<Rightarrow> tape \<Rightarrow> bool"
   where
-  "tcopy_F5 0 tp = False" |
-  "tcopy_F5 (Suc x) (ln, rn) = 
-        (if rn = [] then False 
-         else if hd rn = Bk then (ln = [] & 
-                   rn = Bk # (Oc # replicate (Suc x) Bk
-                             @ replicate (Suc x) Oc))
-         else if hd rn = Oc then 
-           (\<exists>n. ln = replicate (x - n) Oc 
-              & rn = Oc # (Oc # replicate n Bk @ replicate n Oc)
-               & n > 0 & n <= x)
-          else False)"
-  
+  "tcopy_F5 x (l, r) = (tcopy_F5_loop x (l, r) \<or> tcopy_F5_exit x (l, r))"
 
 fun tcopy_F6 :: "nat \<Rightarrow> tape \<Rightarrow> bool"
   where
-  "tcopy_F6 0 tp = False" |
-  "tcopy_F6 (Suc x) (ln, rn) = 
-            (\<exists>n. ln = replicate (Suc x -n) Oc 
-                     & tl rn = replicate n Bk @ replicate n Oc
-             & n > 0 & n <= x)"
-  
+  "tcopy_F6 x (l, r) = 
+       (\<exists> i j any. i + j = x \<and> x > 0 \<and> i > 0 \<and> j > 0 \<and> l = Oc\<^bsup>i\<^esup> \<and> r = any#Bk\<^bsup>j\<^esup> @ Oc\<^bsup>j\<^esup>)"
+
 fun tcopy_F7 :: "nat \<Rightarrow> tape \<Rightarrow> bool"
   where
-  "tcopy_F7 0 tp = False" |
-  "tcopy_F7 (Suc x) (ln, rn) = 
-            (let lrn = (rev ln) @ rn in 
-            (\<exists>n. lrn = replicate ((Suc x) - n) Oc @
-                        replicate (Suc n) Bk @ replicate n Oc
-             & n > 0 & n <= x & 
-               length rn >= n & length rn <= 2 * n ))"
-                 
+  "tcopy_F7 x (l, r) = 
+         (\<exists> i j k t. i + j = x \<and> i > 0 \<and> j > 0 \<and>  k + t = Suc j \<and> l = Bk\<^bsup>k\<^esup> @ Oc\<^bsup>i\<^esup> \<and> r = Bk\<^bsup>t\<^esup> @ Oc\<^bsup>j\<^esup>)"
+
 fun tcopy_F8 :: "nat \<Rightarrow> tape \<Rightarrow> bool"
   where
-  "tcopy_F8 0 tp = False" |
-  "tcopy_F8 (Suc x) (ln, rn) = 
-            (let lrn = (rev ln) @ rn in 
-            (\<exists>n. lrn = replicate ((Suc x) - n) Oc @ 
-                       replicate (Suc n) Bk @ replicate n Oc
-               & n > 0 & n <= x & length rn < n)) "
+  "tcopy_F8 x (l, r) = 
+           (\<exists> i j k t. i + j = x \<and> i > 0 \<and> j > 0 \<and>  k + t = j \<and> l = Oc\<^bsup>k\<^esup> @ Bk\<^bsup>Suc j\<^esup> @ Oc\<^bsup>i\<^esup> \<and> r = Oc\<^bsup>t\<^esup>)"
+
+fun tcopy_F9_loop :: "nat \<Rightarrow> tape \<Rightarrow> bool"
+where
+  "tcopy_F9_loop x (l, r) = 
+          (\<exists> i j k t. i + j = Suc x \<and> i > 0 \<and> j > 0 \<and> k + t = j \<and> t > 0\<and> l = Oc\<^bsup>k\<^esup> @ Bk\<^bsup>j\<^esup> @ Oc\<^bsup>i\<^esup> \<and> r = Oc\<^bsup>t\<^esup>)"
+
+fun tcopy_F9_exit :: "nat \<Rightarrow> tape \<Rightarrow> bool"
+  where
+  "tcopy_F9_exit x (l, r) = (\<exists> i j. i + j = Suc x \<and> i > 0 \<and> j > 0 \<and>  l = Bk\<^bsup>j - 1\<^esup> @ Oc\<^bsup>i\<^esup> \<and> r = Bk # Oc\<^bsup>j\<^esup>)"
 
 fun tcopy_F9 :: "nat \<Rightarrow> tape \<Rightarrow> bool"
   where
-  "tcopy_F9 0 tp = False" | 
-  "tcopy_F9 (Suc x) (ln, rn) =  
-            (let lrn = (rev ln) @ rn in 
-            (\<exists>n. lrn = replicate (Suc (Suc x) - n) Oc 
-                            @ replicate n Bk @ replicate n Oc
-             & n > Suc 0 & n <= Suc x & length rn > 0 
-                    & length rn <= Suc n))"
+  "tcopy_F9 x (l, r) = (tcopy_F9_loop x (l, r) \<or> 
+                        tcopy_F9_exit x (l, r))"
+
+fun tcopy_F10_loop :: "nat \<Rightarrow> tape \<Rightarrow> bool"
+  where
+  "tcopy_F10_loop x (l, r) = 
+     (\<exists> i j k t. i + j = Suc x \<and> i > 0 \<and> k + t + 1 = j \<and> l = Bk\<^bsup>k\<^esup> @ Oc\<^bsup>i\<^esup> \<and> r = Bk\<^bsup>Suc t\<^esup> @ Oc\<^bsup>j\<^esup>)"
+
+fun tcopy_F10_exit :: "nat \<Rightarrow> tape \<Rightarrow> bool"
+  where
+  "tcopy_F10_exit x (l, r) = 
+     (\<exists> i j. i + j = x \<and> j > 0 \<and> l =  Oc\<^bsup>i\<^esup> \<and> r = Oc # Bk\<^bsup>j\<^esup> @ Oc\<^bsup>j\<^esup>)"
 
 fun tcopy_F10 :: "nat \<Rightarrow> tape \<Rightarrow> bool"
   where
-  "tcopy_F10 0 tp = False" |
-  "tcopy_F10 (Suc x) (ln, rn) = 
-           (let lrn = (rev ln) @ rn in 
-             (\<exists>n. lrn = replicate (Suc (Suc x) - n) Oc
-                   @ replicate n Bk @ replicate n Oc & n > Suc 0 
-                & n <= Suc x & length rn > Suc n & 
-                  length rn <= 2*n + 1 ))"
+  "tcopy_F10 x (l, r) = (tcopy_F10_loop x (l, r) \<or> tcopy_F10_exit x (l, r))"
 
 fun tcopy_F11 :: "nat \<Rightarrow> tape \<Rightarrow> bool"
   where
-  "tcopy_F11 0 tp = False" |
-  "tcopy_F11 (Suc x) (ln, rn) = 
-            (ln = [Bk] & rn = Oc # replicate (Suc x) Bk 
-                              @ replicate (Suc x) Oc)"
+  "tcopy_F11 x (l, r) = (x > 0 \<and> l = [Bk] \<and> r = Oc # Bk\<^bsup>x\<^esup> @ Oc\<^bsup>x\<^esup>)"
 
 fun tcopy_F12 :: "nat \<Rightarrow> tape \<Rightarrow> bool"
   where
-  "tcopy_F12 0 tp = False" |
-  "tcopy_F12 (Suc x) (ln, rn) =  
-           (let lrn = ((rev ln) @ rn) in
-           (\<exists>n. n > 0 & n <= Suc (Suc x) 
-         & lrn = Bk # replicate n Oc @ replicate (Suc (Suc x) - n) Bk
-                 @ replicate (Suc x) Oc 
-         & length ln = Suc n))"
+  "tcopy_F12 x (l, r) = (\<exists> i j. i + j = Suc x \<and> x > 0 \<and> l = Oc\<^bsup>i\<^esup> @ [Bk] \<and> r = Bk\<^bsup>j\<^esup> @ Oc\<^bsup>x\<^esup>)"
 
 fun tcopy_F13 :: "nat \<Rightarrow> tape \<Rightarrow> bool"
   where
-  "tcopy_F13 0 tp = False" |
-  "tcopy_F13 (Suc x) (ln, rn) =  
-           (let lrn = ((rev ln) @ rn) in
-           (\<exists>n. n > Suc 0 & n <= Suc (Suc x) 
-         & lrn = Bk # replicate n Oc @ replicate (Suc (Suc x) - n) Bk
-                 @ replicate (Suc x) Oc
-         & length ln = n))"
-          
+  "tcopy_F13 x (l, r) =
+        (\<exists> i j. x > 0 \<and> i + j = x \<and> l = Oc\<^bsup>i\<^esup> @ [Bk] \<and> r = Oc # Bk\<^bsup>j\<^esup> @ Oc\<^bsup>x\<^esup> )"
+
 fun tcopy_F14 :: "nat \<Rightarrow> tape \<Rightarrow> bool"
   where
-  "tcopy_F14 0 tp = False" |
-  "tcopy_F14 (Suc x) (ln, rn) = 
-             (ln = replicate (Suc x) Oc @ [Bk] & 
-              tl rn = replicate (Suc x) Oc)"
+  "tcopy_F14 x (l, r) = (\<exists> any. x > 0 \<and> l = Oc\<^bsup>x\<^esup> @ [Bk] \<and> r = any#Oc\<^bsup>x\<^esup>)"
+
+fun tcopy_F15_loop :: "nat \<Rightarrow> tape \<Rightarrow> bool"
+  where
+  "tcopy_F15_loop x (l, r) = 
+         (\<exists> i j. i + j = x \<and> x > 0 \<and> j > 0 \<and> l = Oc\<^bsup>i\<^esup> @ [Bk] \<and> r = Oc\<^bsup>j\<^esup> @ Bk # Oc\<^bsup>x\<^esup>)"
+
+fun tcopy_F15_exit :: "nat \<Rightarrow> tape \<Rightarrow> bool"
+  where
+  "tcopy_F15_exit x (l, r) = (x > 0 \<and> l = [] \<and> r = Bk # Oc\<^bsup>x\<^esup> @ Bk # Oc\<^bsup>x\<^esup>)"
 
 fun tcopy_F15 :: "nat \<Rightarrow> tape \<Rightarrow> bool"
   where
-  "tcopy_F15 0 tp = False" |
-  "tcopy_F15 (Suc x) (ln, rn) = 
-            (let lrn = ((rev ln) @ rn) in
-             lrn = Bk # replicate (Suc x) Oc @ [Bk] @ 
-                   replicate (Suc x) Oc & length ln <= (Suc x))"
+  "tcopy_F15 x (l, r) = (tcopy_F15_loop x (l, r) \<or>  tcopy_F15_exit x (l, r))"
 
 text {*
   The following @{text "inv_tcopy"} is the invariant of the {\em Copying} TM.
@@ -208,17 +182,12 @@
         tcopy_F14.simps [simp del]
         tcopy_F15.simps [simp del]
 
-lemma list_replicate_Bk[dest]: "list_all isBk list \<Longrightarrow> 
-                            list = replicate (length list) Bk"
-apply(induct list)
-apply(simp+)
+lemma exp_zero_simp: "(a\<^bsup>b\<^esup> = []) = (b = 0)"
+apply(auto simp: exponent_def)
 done
 
-lemma [simp]: "dropWhile (\<lambda> a. a = b) (replicate x b @ ys) = 
-                  dropWhile (\<lambda> a. a = b) ys"
-apply(induct x)
-apply(simp)
-apply(simp)
+lemma exp_zero_simp2: "([] = a\<^bsup>b\<^esup> ) = (b = 0)"
+apply(auto simp: exponent_def)
 done
 
 lemma [elim]: "\<lbrakk>tstep (0, a, b) tcopy = (s, l, r); s \<noteq> 0\<rbrakk> \<Longrightarrow> RR"
@@ -300,6 +269,7 @@
 by(simp add: tstep.simps tcopy_def fetch.simps 
         split: block.splits list.splits)
 
+(*
 lemma min_Suc4: "min (Suc (Suc x)) x = x"
 by auto
 
@@ -330,22 +300,26 @@
                                         replicate n b @ b # xs"
 apply(simp)
 done
-
+*)
 
 lemma [elim]: "\<lbrakk>tstep (14, b, c) tcopy = (15, ab, ba); 
                 tcopy_F14 x (b, c)\<rbrakk> \<Longrightarrow> tcopy_F15 x (ab, ba)"
-apply(case_tac x)
 apply(auto simp: tstep.simps tcopy_def 
           tcopy_F14.simps tcopy_F15.simps fetch.simps new_tape.simps 
            split: if_splits list.splits block.splits)
+apply(erule_tac [!] x = "x - 1" in allE)
+apply(case_tac [!] x, simp_all add: exp_ind_def exp_zero)
+apply(erule_tac [!] x = "Suc 0" in allE, simp_all)
 done
 
+(*
 lemma dropWhile_drophd: "\<not> p a \<Longrightarrow> 
       (dropWhile p xs @ (a # as)) = (dropWhile p (xs @ [a]) @ as)"
 apply(induct xs)
 apply(auto)
 done
-
+*)
+(*
 lemma dropWhile_append3: "\<lbrakk>\<not> p a; 
   listall ((dropWhile p xs) @ [a]) isBk\<rbrakk> \<Longrightarrow> 
                listall (dropWhile p (xs @ [a])) isBk"
@@ -364,495 +338,341 @@
 apply(induct xs)
 apply(simp+)
 done
+*)
+lemma false_case1:
+  "\<lbrakk>Oc\<^bsup>j\<^esup> @ Bk # Oc\<^bsup>i + j\<^esup> = Oc # list;
+  0 < i; 
+  \<forall>ia. tl (Oc\<^bsup>i\<^esup> @ [Bk]) = Oc\<^bsup>ia\<^esup> @ [Bk] \<longrightarrow> (\<forall>ja. ia + ja = i + j 
+  \<longrightarrow> hd (Oc\<^bsup>i\<^esup> @ [Bk]) # Oc # list \<noteq> Oc\<^bsup>ja\<^esup> @ Bk # Oc\<^bsup>i + j\<^esup>)\<rbrakk>
+  \<Longrightarrow> RR"
+apply(case_tac i, auto simp: exp_ind_def)
+apply(erule_tac x = nat in allE, simp add:exp_ind_def)
+apply(erule_tac x = "Suc j" in allE, simp)
+done
+
+lemma false_case3:"\<forall>ja. ja \<noteq> i \<Longrightarrow> RR"
+by auto
 
 lemma [elim]: "\<lbrakk>tstep (15, b, c) tcopy = (15, ab, ba); 
-                tcopy_F15 x (b, c)\<rbrakk> \<Longrightarrow> tcopy_F15 x (ab, ba)" 
-apply(case_tac x)
+                tcopy_F15 x (b, c)\<rbrakk> \<Longrightarrow> tcopy_F15 x (ab, ba)"
 apply(auto simp: tstep.simps tcopy_F15.simps
                  tcopy_def fetch.simps new_tape.simps
-            split: if_splits list.splits block.splits)
-apply(case_tac b, simp+)
+            split: if_splits list.splits block.splits elim: false_case1)
+apply(case_tac [!] i, simp_all add: exp_zero exp_ind_def)
+apply(erule_tac [!] x = nat in allE, simp_all add: exp_ind_def)
+apply(auto elim: false_case3)
 done
 
 lemma [elim]: "\<lbrakk>tstep (14, b, c) tcopy = (14, ab, ba); 
                 tcopy_F14 x (b, c)\<rbrakk> \<Longrightarrow> tcopy_F14 x (ab, ba)"
-apply(case_tac x)
 apply(auto simp: tcopy_F14.simps tcopy_def tstep.simps 
                  tcopy_F14.simps fetch.simps new_tape.simps
            split: if_splits list.splits block.splits)
 done
 
-lemma [intro]: "list_all isBk (replicate x Bk)"
-apply(induct x, simp+)
-done
-
-lemma [elim]: "list_all isBk (dropWhile (\<lambda>a. a = Oc) b) \<Longrightarrow> 
-               list_all isBk (dropWhile (\<lambda>a. a = Oc) (tl b))"
-apply(case_tac b, auto split: if_splits)
-apply(drule list_replicate_Bk)
-apply(case_tac "length list", auto)
-done
-
-lemma [elim]: "list_all (\<lambda> a. a = Oc) list \<Longrightarrow> 
-               list = replicate (length list) Oc"
-apply(induct list)
-apply(simp+)
-done
-
-lemma append_length:  "\<lbrakk>as @ bs = cs @ ds; length bs = length ds\<rbrakk>
-                    \<Longrightarrow> as = cs & bs = ds"
-apply(auto)
-done
-
-lemma Suc_elim: "Suc (Suc m) - n = Suc na \<Longrightarrow> Suc m - n = na"
-apply(simp)
-done
-
-lemma [elim]: "\<lbrakk>0 < n; n \<le> Suc (Suc na);
-  rev b @ Oc # list = 
-         Bk # replicate n Oc @ replicate (Suc (Suc na) - n) Bk @ 
-         Oc # replicate na Oc;
-  length b = Suc n; b \<noteq> []\<rbrakk>
-       \<Longrightarrow> list_all isBk (dropWhile (\<lambda>a. a = Oc) (tl b))"
-apply(case_tac "rev b", auto)
-done
-
-lemma b_cons_same: "b#bs = replicate x a @ as \<Longrightarrow> a \<noteq> b \<longrightarrow> x = 0"
-apply(case_tac x, simp+)
-done
-
-lemma tcopy_tmp[elim]: 
-  "\<lbrakk>0 < n; n \<le> Suc (Suc na); 
-  rev b @ Oc # list = 
-    Bk # replicate n Oc @ replicate (Suc (Suc na) - n) Bk 
-    @ Oc # replicate na Oc; length b = Suc n; b \<noteq> []\<rbrakk>
-   \<Longrightarrow> list = replicate na Oc"
-apply(case_tac "rev b", simp+)
-apply(auto)
-apply(frule b_cons_same, auto)
-done
 
 lemma [elim]: "\<lbrakk>tstep (12, b, c) tcopy = (14, ab, ba); 
                 tcopy_F12 x (b, c)\<rbrakk> \<Longrightarrow> tcopy_F14 x (ab, ba)" 
-apply(case_tac x)
 apply(auto simp:tcopy_F12.simps tcopy_F14.simps 
                 tcopy_def tstep.simps fetch.simps new_tape.simps 
            split: if_splits list.splits block.splits)
-apply(frule tcopy_tmp, simp+)
-apply(case_tac n, simp+)
-apply(case_tac nata, simp+)
-done
-
-lemma replicate_app_Cons: "replicate a b @ b # replicate c b 
-                        = replicate (Suc (a + c)) b"
-apply(simp)
-apply(simp add: replicate_app_Cons_same)
-apply(simp only: replicate_add[THEN sym])
-done
-
-lemma replicate_same_exE_pref: "\<exists>x. bs @ (b # cs) = replicate x y
-                            \<Longrightarrow> (\<exists>n. bs = replicate n y)"
-apply(induct bs)
-apply(rule_tac x = 0 in exI, simp)
-apply(drule impI)
-apply(erule impE)
-apply(erule exE, simp+)
-apply(case_tac x, auto)
-apply(case_tac x, auto)
-apply(rule_tac x = "Suc n" in exI, simp+)
-done
-
-lemma replicate_same_exE_inf: "\<exists>x. bs @ (b # cs) = replicate x y \<Longrightarrow> b = y"
-apply(induct bs, auto)
-apply(case_tac x, auto)
-apply(drule impI)
-apply(erule impE)
-apply(case_tac x, simp+)
-done
-
-lemma replicate_same_exE_suf: 
-     "\<exists>x. bs @ (b # cs) = replicate x y \<Longrightarrow> \<exists>n. cs = replicate n y"
-apply(induct bs, auto)
-apply(case_tac x, simp+)
-apply(drule impI, erule impE)
-apply(case_tac x, simp+)
-done
-
-lemma replicate_same_exE: "\<exists>x. bs @ (b # cs) = replicate x y 
-    \<Longrightarrow> (\<exists>n. bs = replicate n y) & (b = y) & (\<exists>m. cs = replicate m y)"
-apply(rule conjI)
-apply(drule  replicate_same_exE_pref, simp)
-apply(rule conjI)
-apply(drule replicate_same_exE_inf, simp)
-apply(drule replicate_same_exE_suf, simp)
-done
-
-lemma replicate_same: "bs @ (b # cs) = replicate x y
-    \<Longrightarrow> (\<exists>n. bs = replicate n y) & (b = y) & (\<exists>m. cs = replicate m y)"
-apply(rule_tac replicate_same_exE)
-apply(rule_tac x = x in exI)
-apply(assumption)
-done
-
-lemma [elim]: "\<lbrakk> 0 < n; n \<le> Suc (Suc na);
-    (rev ab @ Bk # list) = Bk # replicate n Oc 
-   @ replicate (Suc (Suc na) - n) Bk @ Oc # replicate na Oc; ab \<noteq> []\<rbrakk>
-    \<Longrightarrow> n \<le> Suc na"
-apply(rule contrapos_pp, simp+)
-apply(case_tac "rev ab", simp+)
-apply(auto)
-apply(simp only: replicate_app_Cons)
-apply(drule replicate_same)
-apply(auto)
-done
-
-
-lemma [elim]: "\<lbrakk>0 < n; n \<le> Suc (Suc na); 
-   rev ab @ Bk # list = Bk # replicate n Oc @ 
-    replicate (Suc (Suc na) - n) Bk @ Oc # replicate na Oc; 
-   length ab = Suc n; ab \<noteq> []\<rbrakk>
-    \<Longrightarrow> rev ab @ Oc # list = Bk # Oc # replicate n Oc @ 
-               replicate (Suc na - n) Bk @ Oc # replicate na Oc"
-apply(case_tac "rev ab", simp+)
-apply(auto)
-apply(simp only: replicate_Cons_simp)
-apply(simp)
-apply(case_tac "Suc (Suc na) - n", simp+)
+apply(case_tac [!] j, simp_all add: exp_zero exp_ind_def)
 done
 
 lemma [elim]: "\<lbrakk>tstep (12, b, c) tcopy = (13, ab, ba); 
                 tcopy_F12 x (b, c)\<rbrakk> \<Longrightarrow> tcopy_F13 x (ab, ba)"
-apply(case_tac x)
-apply(simp_all add:tcopy_F12.simps tcopy_F13.simps 
-                   tcopy_def tstep.simps fetch.simps new_tape.simps)
-apply(simp split: if_splits list.splits block.splits)
-apply(auto)
+apply(auto simp:tcopy_F12.simps tcopy_F13.simps 
+                   tcopy_def tstep.simps fetch.simps new_tape.simps
+  split: if_splits list.splits block.splits)
+apply(case_tac x, simp_all add: exp_ind_def exp_zero)
+apply(rule_tac [!] x = i in exI, simp_all)
+apply(rule_tac [!] x = "j - 1" in exI)
+apply(case_tac [!] j, simp_all add: exp_ind_def exp_zero)
+apply(case_tac x, simp_all add: exp_ind_def exp_zero)
 done
 
-
 lemma [elim]: "\<lbrakk>tstep (11, b, c) tcopy = (12, ab, ba); 
                 tcopy_F11 x (b, c)\<rbrakk> \<Longrightarrow> tcopy_F12 x (ab, ba)" 
-apply(case_tac x)
 apply(simp_all add:tcopy_F12.simps tcopy_F11.simps 
                    tcopy_def tstep.simps fetch.simps new_tape.simps)
 apply(auto)
+apply(rule_tac x = "Suc 0" in exI, 
+  rule_tac x = x in exI, simp add: exp_ind_def exp_zero)
 done
 
-lemma equal_length: "a = b \<Longrightarrow> length a = length b"
-by(simp)
 
 lemma [elim]: "\<lbrakk>tstep (13, b, c) tcopy = (12, ab, ba); 
                 tcopy_F13 x (b, c)\<rbrakk> \<Longrightarrow> tcopy_F12 x (ab, ba)"
-apply(case_tac x)
-apply(simp_all add:tcopy_F12.simps tcopy_F13.simps 
-                   tcopy_def tstep.simps fetch.simps new_tape.simps)
-apply(simp split: if_splits list.splits block.splits)
-apply(auto)
-apply(drule equal_length, simp)
+apply(auto simp:tcopy_F12.simps tcopy_F13.simps 
+                   tcopy_def tstep.simps fetch.simps new_tape.simps
+  split: if_splits list.splits block.splits)
+apply(rule_tac [!] x = "Suc i" in exI, simp_all add: exp_ind_def)
 done
 
 lemma [elim]: "\<lbrakk>tstep (5, b, c) tcopy = (11, ab, ba); 
-                tcopy_F5 x (b, c)\<rbrakk> \<Longrightarrow> tcopy_F11 x (ab, ba)" 
-apply(case_tac x)
+                tcopy_F5 x (b, c)\<rbrakk> \<Longrightarrow> tcopy_F11 x (ab, ba)"
 apply(simp_all add:tcopy_F11.simps tcopy_F5.simps tcopy_def 
                    tstep.simps fetch.simps new_tape.simps)
 apply(simp split: if_splits list.splits block.splits)
 done
 
-lemma less_equal: "\<lbrakk>length xs <= b; \<not> Suc (length xs) <= b\<rbrakk> \<Longrightarrow> 
-                   length xs = b"
-apply(simp)
+lemma F10_false: "tcopy_F10 x (b, []) = False"
+apply(auto simp: tcopy_F10.simps exp_ind_def)
 done
 
-lemma length_cons_same: "\<lbrakk>xs @ b # ys = as @ bs; 
-                 length ys = length bs\<rbrakk> \<Longrightarrow> xs @ [b] = as & ys = bs"
-apply(drule rev_equal)
-apply(simp)
-apply(auto)
-apply(drule rev_equal, simp)
+lemma F10_false2: "tcopy_F10 x ([], Bk # list) = False"
+apply(auto simp:tcopy_F10.simps)
+apply(case_tac i, simp_all add: exp_ind_def exp_zero)
+done
+ 
+lemma [simp]: "tcopy_F10_exit x (b, Bk # list) = False"
+apply(auto simp: tcopy_F10.simps)
 done
 
-lemma replicate_set_equal: "\<lbrakk> xs @ [a] = replicate n b; a \<noteq> b\<rbrakk> \<Longrightarrow> RR"
-apply(drule rev_equal, simp)
-apply(case_tac n, simp+)
+declare tcopy_F10_loop.simps[simp del]  tcopy_F10_exit.simps[simp del]
+
+lemma [simp]: "tcopy_F10_loop x (b, [Bk]) = False"
+apply(auto simp: tcopy_F10_loop.simps)
+apply(simp add: exp_ind_def)
 done
 
 lemma [elim]: "\<lbrakk>tstep (10, b, c) tcopy = (10, ab, ba); 
                 tcopy_F10 x (b, c)\<rbrakk> \<Longrightarrow> tcopy_F10 x (ab, ba)"
-apply(case_tac x)
-apply(auto simp:tcopy_F10.simps tcopy_def tstep.simps fetch.simps 
-                new_tape.simps
+apply(simp add: tcopy_def tstep.simps fetch.simps 
+                new_tape.simps exp_ind_def exp_zero_simp exp_zero_simp2 F10_false F10_false2
            split: if_splits list.splits block.splits)
-apply(rule_tac x = n in exI, auto)
-apply(case_tac b, simp+)
-apply(rule contrapos_pp, simp+)
-apply(frule less_equal, simp+)
-apply(drule length_cons_same, auto)
-apply(drule replicate_set_equal, simp+)
+apply(simp add: tcopy_F10.simps del: tcopy_F10_loop.simps  tcopy_F10_exit.simps)
+apply(case_tac b, simp, case_tac aa)
+apply(rule_tac disjI1)
+apply(simp only: tcopy_F10_loop.simps)
+apply(erule_tac exE)+
+apply(rule_tac x = i in exI, rule_tac x = j in exI, 
+      rule_tac x = "k - 1" in exI, rule_tac x = "Suc t" in exI, simp)
+apply(case_tac k, simp_all add: exp_ind_def exp_zero)
+apply(case_tac i, simp_all add: exp_ind_def exp_zero)
+apply(rule_tac disjI2)
+apply(simp only: tcopy_F10_loop.simps tcopy_F10_exit.simps)
+apply(erule_tac exE)+
+apply(rule_tac x = "i - 1" in exI, rule_tac x = "j" in exI)
+apply(case_tac k, simp_all add: exp_ind_def exp_zero)
+apply(case_tac i, simp_all add: exp_ind_def exp_zero)
+apply(auto)
+apply(simp add: exp_ind_def)
 done
 
-lemma less_equal2: "\<not> (n::nat) \<le> m \<Longrightarrow> \<exists>x. n = x + m & x > 0"
-apply(rule_tac x = "n - m" in exI)
-apply(auto)
+(*
+lemma false_case4: "\<lbrakk>i + (k + t) = Suc x; 
+        0 < i;
+        Bk # list = Oc\<^bsup>t\<^esup>;
+        \<forall>ia j. ia + j = Suc x \<longrightarrow> ia = 0 \<or> (\<forall>ka. tl (Oc\<^bsup>k\<^esup>) @ Bk\<^bsup>k + t\<^esup> @ Oc\<^bsup>i\<^esup> = Bk\<^bsup>ka\<^esup> @ Oc\<^bsup>ia\<^esup> \<longrightarrow> (\<forall>ta. Suc (ka + ta) = j \<longrightarrow> Oc # Oc\<^bsup>t\<^esup> \<noteq> Bk\<^bsup>Suc ta\<^esup> @ Oc\<^bsup>j\<^esup>));
+        0 < k\<rbrakk>
+       \<Longrightarrow> RR"
+apply(case_tac t, simp_all add: exp_ind_def exp_zero)
+done
+
+lemma false_case5: "
+  \<lbrakk>Suc (i + nata) = x;
+   0 < i;
+   \<forall>ia j. ia + j = Suc x \<longrightarrow> ia = 0 \<or> (\<forall>k. Bk\<^bsup>nata\<^esup> @ Oc\<^bsup>i\<^esup> = Bk\<^bsup>k\<^esup> @ Oc\<^bsup>ia\<^esup> \<longrightarrow> (\<forall>t. Suc (k + t) = j \<longrightarrow> Bk # Oc # Oc # Oc\<^bsup>nata\<^esup> \<noteq> Bk\<^bsup>t\<^esup> @ Oc\<^bsup>j\<^esup>))\<rbrakk>
+       \<Longrightarrow> False"
+apply(erule_tac x = i in allE, simp)
+apply(erule_tac x = "Suc (Suc nata)" in allE, simp)
+apply(erule_tac x = nata in allE, simp, simp add: exp_ind_def exp_zero)
+done
+
+lemma false_case6: "\<lbrakk>0 < x; \<forall>i. tl (Oc\<^bsup>x\<^esup>) = Oc\<^bsup>i\<^esup> \<longrightarrow> (\<forall>j. i + j = x \<longrightarrow> j = 0 \<or> [Bk, Oc] \<noteq> Bk\<^bsup>j\<^esup> @ Oc\<^bsup>j\<^esup>)\<rbrakk>
+  \<Longrightarrow> False"
+apply(erule_tac x = "x - 1" in allE)
+apply(case_tac x, simp_all add: exp_ind_def exp_zero)
+apply(erule_tac x = "Suc 0" in allE, simp)
+done
+*)
+
+lemma [simp]: "tcopy_F9 x ([], b) = False"
+apply(auto simp: tcopy_F9.simps)
+apply(case_tac [!] i, simp_all add: exp_ind_def exp_zero)
 done
 
-lemma replicate_tail_length[dest]:
-    "\<lbrakk>rev b @ Bk # list = xs @ replicate n Bk @ replicate n Oc\<rbrakk> 
- \<Longrightarrow> length list >= n"
-apply(rule contrapos_pp, simp+)
-apply(drule less_equal2, auto)
-apply(drule rev_equal)
-apply(simp add: replicate_add)
-apply(auto)
-apply(case_tac x, simp+)
+lemma [simp]: "tcopy_F9 x (b, []) = False"
+apply(auto simp: tcopy_F9.simps)
+apply(case_tac [!] t, simp_all add: exp_ind_def exp_zero)
+done
+
+declare tcopy_F9_loop.simps[simp del] tcopy_F9_exit.simps[simp del]
+lemma [simp]: "tcopy_F9_loop x (b, Bk # list) = False"
+apply(auto simp: tcopy_F9_loop.simps)
+apply(case_tac [!] t, simp_all add: exp_ind_def exp_zero)
 done
 
+lemma [elim]: "\<lbrakk>tstep (9, b, c) tcopy = (10, ab, ba); 
+                tcopy_F9 x (b, c)\<rbrakk> \<Longrightarrow> tcopy_F10 x (ab, ba)"
+apply(auto simp:tcopy_def
+                tstep.simps fetch.simps new_tape.simps exp_zero_simp
+                exp_zero_simp2 
+           split: if_splits list.splits block.splits)
+apply(case_tac "hd b", simp add:tcopy_F9.simps tcopy_F10.simps )
+apply(simp only: tcopy_F9_exit.simps tcopy_F10_loop.simps)
+apply(erule_tac exE)+
+apply(rule_tac x = i in exI, rule_tac x = j in exI, simp)
+apply(rule_tac x = "j - 2" in exI, simp add: exp_ind_def)
+apply(case_tac j, simp, simp)
+apply(case_tac nat, simp_all add: exp_zero exp_ind_def)
+apply(case_tac x, simp_all add: exp_ind_def exp_zero)
+apply(simp add: tcopy_F9.simps tcopy_F10.simps)
+apply(rule_tac disjI2)
+apply(simp only: tcopy_F10_exit.simps tcopy_F9_exit.simps)
+apply(erule_tac exE)+
+apply(simp)
+apply(case_tac j, simp_all, case_tac nat, simp_all add: exp_ind_def exp_zero)
+apply(case_tac x, simp_all add: exp_ind_def exp_zero)
+apply(rule_tac x = nata in exI, rule_tac x = 1 in exI, simp add: exp_ind_def exp_zero)
+done
 
-lemma [elim]: "\<lbrakk>tstep (9, b, c) tcopy = (10, ab, ba); 
-                tcopy_F9 x (b, c)\<rbrakk> \<Longrightarrow> tcopy_F10 x (ab, ba)" 
-apply(case_tac x)
-apply(auto simp:tcopy_F10.simps tcopy_F9.simps tcopy_def
-                tstep.simps fetch.simps new_tape.simps 
-           split: if_splits list.splits block.splits)
-apply(rule_tac x = n in exI, auto)
-apply(case_tac b, simp+)
+lemma false_case7:
+  "\<lbrakk>i + (n + t) = x; 0 < i; 0 < t; Oc # list = Oc\<^bsup>t\<^esup>; k = Suc n;
+        \<forall>j. i + j = Suc x \<longrightarrow> (\<forall>k. Oc\<^bsup>n\<^esup> @ Bk # Bk\<^bsup>n + t\<^esup> = Oc\<^bsup>k\<^esup> @ Bk\<^bsup>j\<^esup> \<longrightarrow>
+         (\<forall>ta. k + ta = j \<longrightarrow> ta = 0 \<or> Oc # Oc\<^bsup>t\<^esup> \<noteq> Oc\<^bsup>ta\<^esup>))\<rbrakk>
+       \<Longrightarrow> RR"
+apply(erule_tac x = "k + t" in allE, simp)
+apply(erule_tac x = n in allE, simp add: exp_ind_def)
+apply(erule_tac x = "Suc t" in allE, simp)
+done
+
+lemma false_case8: 
+  "\<lbrakk>i + t = Suc x;
+   0 < i;
+    0 < t; 
+    \<forall>ia j. tl (Bk\<^bsup>t\<^esup> @ Oc\<^bsup>i\<^esup>) = Bk\<^bsup>j - Suc 0\<^esup> @ Oc\<^bsup>ia\<^esup> \<longrightarrow> 
+    ia + j = Suc x \<longrightarrow> ia = 0 \<or> j = 0 \<or> Oc\<^bsup>t\<^esup> \<noteq> Oc\<^bsup>j\<^esup>\<rbrakk> \<Longrightarrow> 
+  RR"
+apply(erule_tac x = i in allE, simp)
+apply(erule_tac x = t in allE, simp)
+apply(case_tac t, simp_all add: exp_ind_def exp_zero)
 done
 
 lemma [elim]: "\<lbrakk>tstep (9, b, c) tcopy = (9, ab, ba); 
                 tcopy_F9 x (b, c)\<rbrakk> \<Longrightarrow> tcopy_F9 x (ab, ba)"
-apply(case_tac x)
-apply(simp_all add: tcopy_F9.simps tcopy_def 
-                    tstep.simps fetch.simps new_tape.simps 
+apply(auto simp: tcopy_F9.simps tcopy_def 
+                    tstep.simps fetch.simps new_tape.simps exp_zero_simp exp_zero_simp2
+                    tcopy_F9_exit.simps tcopy_F9_loop.simps
   split: if_splits list.splits block.splits)
-apply(rule_tac x = n in exI, auto)
-apply(case_tac b, simp+)
-apply(rule contrapos_pp, simp+)
-apply(drule less_equal, simp+)
-apply(drule rev_equal, auto)
-apply(case_tac "length list", simp+)
+apply(case_tac [!] k, simp_all add: exp_ind_def exp_zero)
+apply(erule_tac [!] x = i in allE, simp)
+apply(erule_tac false_case7, simp_all)+
+apply(case_tac t, simp_all add: exp_zero exp_ind_def)
+apply(erule_tac false_case7, simp_all)+
+apply(erule_tac false_case8, simp_all)
+apply(erule_tac false_case7, simp_all)+
+apply(case_tac t, simp_all add: exp_ind_def exp_zero)
+apply(erule_tac false_case7, simp_all)
+apply(erule_tac false_case8, simp_all)
+apply(erule_tac false_case7, simp_all)
+done
+ 
+lemma [elim]: "\<lbrakk>tstep (8, b, c) tcopy = (9, ab, ba); 
+                tcopy_F8 x (b, c)\<rbrakk> \<Longrightarrow> tcopy_F9 x (ab, ba)"
+apply(auto simp:tcopy_F8.simps tcopy_F9.simps tcopy_def 
+                tstep.simps fetch.simps new_tape.simps tcopy_F9_loop.simps
+                tcopy_F9_exit.simps
+  split: if_splits list.splits block.splits)
+apply(case_tac [!] t, simp_all add: exp_ind_def exp_zero)
+apply(rule_tac x = i in exI)
+apply(rule_tac x = "Suc k" in exI, simp)
+apply(rule_tac x = "k" in exI, simp add: exp_ind_def exp_zero)
 done
 
-lemma app_cons_app_simp: "xs @ a # bs @ ys = (xs @ [a]) @ bs @ ys"
-apply(simp)
-done
-
-lemma [elim]: "\<lbrakk>tstep (8, b, c) tcopy = (9, ab, ba); 
-                tcopy_F8 x (b, c)\<rbrakk> \<Longrightarrow> tcopy_F9 x (ab, ba)" 
-apply(case_tac x)
-apply(auto simp:tcopy_F8.simps tcopy_F9.simps tcopy_def 
-                tstep.simps fetch.simps new_tape.simps
-  split: if_splits list.splits block.splits)
-apply(rule_tac x = "Suc n" in exI, auto)
-apply(rule_tac x = "n" in exI, auto)
-apply(simp only: app_cons_app_simp)
-apply(frule replicate_tail_length, simp)
-done
 
 lemma [elim]: "\<lbrakk>tstep (8, b, c) tcopy = (8, ab, ba); 
                 tcopy_F8 x (b, c)\<rbrakk> \<Longrightarrow> tcopy_F8 x (ab, ba)"
-apply(case_tac x)
-apply(simp_all add:tcopy_F8.simps tcopy_def tstep.simps 
-                   fetch.simps new_tape.simps)
-apply(simp split: if_splits list.splits block.splits)
-apply(rule_tac x = "n" in exI, auto)
-done
-
-lemma ex_less_more: "\<lbrakk>(x::nat) >= m ; x <= n\<rbrakk> \<Longrightarrow> 
-                        \<exists>y. x = m + y & y <= n - m"
-by(rule_tac x = "x -m" in exI, auto)
-
-lemma replicate_split: "x <= n \<Longrightarrow> 
-                      (\<exists>y. replicate n b = replicate (y + x) b)"
-apply(rule_tac x = "n - x" in exI)
-apply(simp)
-done
-
-lemma app_app_app_app_simp: "as @ bs @ cs @ ds = 
-                             (as @ bs) @ (cs @ ds)"
-by simp
-
-lemma lengthtailsame_append_elim: 
-     "\<lbrakk>as @ bs = cs @ ds; length bs = length ds\<rbrakk> \<Longrightarrow> bs = ds"
-apply(simp)
+apply(auto simp:tcopy_F8.simps tcopy_def tstep.simps 
+                   fetch.simps new_tape.simps exp_zero_simp exp_zero split: if_splits list.splits 
+                   
+         block.splits)
+apply(rule_tac x = i in exI, rule_tac x = "k + t" in exI, simp)
+apply(rule_tac x = "Suc k" in exI, simp)
+apply(rule_tac x = "t - 1" in exI, simp)
+apply(case_tac t, simp_all add: exp_zero exp_ind_def)
 done
 
-lemma rep_suc: "replicate (Suc n) x = replicate n x @ [x]" 
-by(induct n, auto)
-
-lemma length_append_diff_cons: 
- "\<lbrakk>b @ x # ba = xs @ replicate m y @ replicate n x; x \<noteq> y; 
-   Suc (length ba) \<le> m + n\<rbrakk>
-  \<Longrightarrow> length ba < n"
-apply(induct n arbitrary: ba, simp)
-apply(drule_tac b = y in replicate_split,
-      simp add: replicate_add, erule exE, simp del: replicate.simps)
-proof -
-  fix ba ya
-  assume h1: 
-     "b @ x # ba = xs @ y # replicate ya y @ replicate (length ba) y" 
-    and h2: "x \<noteq> y"
-  thus "False"  
-    using append_eq_append_conv[of "b @ [x]" 
-            "xs @ y # replicate ya y" "ba" "replicate (length ba) y"]
-    apply(auto)
-    apply(case_tac ya, simp, 
-           simp add: rep_suc del: rep_suc_rev replicate.simps)
-    done
-next
-  fix n ba
-  assume ind: "\<And>ba. \<lbrakk>b @ x # ba = xs @ replicate m y @ replicate n x;
-                      x \<noteq> y; Suc (length ba) \<le> m + n\<rbrakk> 
-                 \<Longrightarrow> length ba < n"
-    and h1: "b @ x # ba = xs @ replicate m y @ replicate (Suc n) x" 
-    and h2: "x \<noteq> y" and h3: "Suc (length ba) \<le> m + Suc n"
-  show "length ba < Suc n"
-  proof(cases "length ba")
-    case 0 thus "?thesis" by simp
-  next
-    fix nat
-    assume "length ba = Suc nat"
-    hence "\<exists> ys a. ba = ys @ [a]"
-      apply(rule_tac x = "butlast ba" in exI)
-      apply(rule_tac x = "last ba" in exI)
-      using append_butlast_last_id[of ba]
-      apply(case_tac ba, auto)
-      done
-    from this obtain ys where "\<exists> a. ba = ys @ [a]" ..
-    from this obtain a where "ba = ys @ [a]" ..
-    thus "?thesis"
-      using ind[of ys] h1 h2 h3
-      apply(simp del: rep_suc_rev replicate.simps add: rep_suc)
-      done
-  qed
-qed
-      
-lemma [elim]: 
-  "\<lbrakk>b @ Oc # ba = xs @ Bk # replicate n Bk @ replicate n Oc;  
-   Suc (length ba) \<le> 2 * n\<rbrakk>
-  \<Longrightarrow> length ba < n"
-  apply(rule_tac length_append_diff_cons[of b Oc ba xs "Suc n" Bk n])
-  apply(simp, simp, simp)
-  done
-
-lemma [elim]: "\<lbrakk>tstep (7, b, c) tcopy = (8, ab, ba); 
-                tcopy_F7 x (b, c)\<rbrakk> \<Longrightarrow> tcopy_F8 x (ab, ba)" 
-apply(case_tac x)
-apply(simp_all add:tcopy_F8.simps tcopy_F7.simps 
-                   tcopy_def tstep.simps fetch.simps new_tape.simps)
-apply(simp split: if_splits list.splits block.splits)
-apply(rule_tac x = "n" in exI, auto)
-done
 
 lemma [elim]: "\<lbrakk>tstep (7, b, c) tcopy = (7, ab, ba); 
                 tcopy_F7 x (b, c)\<rbrakk> \<Longrightarrow> tcopy_F7 x (ab, ba)"
-apply(case_tac x)
-apply(auto simp:tcopy_F7.simps tcopy_def tstep.simps 
-                fetch.simps new_tape.simps
-  split: if_splits list.splits block.splits)
-apply(rule_tac x = "n" in exI, auto)
-apply(simp only: app_cons_app_simp)
-apply(frule replicate_tail_length, simp)
+apply(auto simp:tcopy_F7.simps tcopy_def tstep.simps fetch.simps 
+                new_tape.simps exp_ind_def exp_zero_simp
+           split: if_splits list.splits block.splits)
+apply(rule_tac x = i in exI)
+apply(rule_tac x = j in exI, simp)
+apply(rule_tac x = "Suc k" in exI, simp)
+apply(rule_tac x = "t - 1" in exI)
+apply(case_tac t, simp_all add: exp_zero exp_ind_def)
+apply(case_tac j, simp_all add: exp_zero exp_ind_def)
 done
 
-lemma Suc_more: "n <= m \<Longrightarrow> Suc m - n = Suc (m - n)"
-by simp
+lemma [elim]: "\<lbrakk>tstep (7, b, c) tcopy = (8, ab, ba); 
+                tcopy_F7 x (b, c)\<rbrakk> \<Longrightarrow> tcopy_F8 x (ab, ba)"
+apply(auto simp:tcopy_F7.simps tcopy_def tstep.simps tcopy_F8.simps
+                fetch.simps new_tape.simps exp_zero_simp
+  split: if_splits list.splits block.splits)
+apply(rule_tac x = i in exI, simp)
+apply(rule_tac x =  "Suc 0" in exI, simp add: exp_ind_def exp_zero)
+apply(rule_tac x = "j - 1" in exI, simp)
+apply(case_tac t, simp_all add: exp_ind_def )
+apply(case_tac j, simp_all add: exp_ind_def exp_zero)
+done
 
 lemma [elim]: "\<lbrakk>tstep (6, b, c) tcopy = (7, ab, ba); 
                 tcopy_F6 x (b, c)\<rbrakk> \<Longrightarrow> tcopy_F7 x (ab, ba)" 
 apply(case_tac x)
 apply(auto simp:tcopy_F7.simps tcopy_F6.simps 
-                tcopy_def tstep.simps fetch.simps new_tape.simps
+                tcopy_def tstep.simps fetch.simps new_tape.simps exp_zero_simp
   split: if_splits list.splits block.splits)
+apply(case_tac i, simp_all add: exp_ind_def exp_zero)
+apply(rule_tac x = i in exI, simp)
+apply(rule_tac x = j in exI, simp)
+apply(rule_tac x = "Suc 0" in exI, simp add: exp_ind_def exp_zero)
 done
 
 lemma [elim]: "\<lbrakk>tstep (6, b, c) tcopy = (6, ab, ba); 
                 tcopy_F6 x (b, c)\<rbrakk> \<Longrightarrow> tcopy_F6 x (ab, ba)"
-apply(case_tac x)
 apply(auto simp:tcopy_F6.simps tcopy_def tstep.simps 
                 new_tape.simps fetch.simps
   split: if_splits list.splits block.splits)
 done
 
 lemma [elim]: "\<lbrakk>tstep (5, b, c) tcopy = (6, ab, ba); 
-                tcopy_F5 x (b, c)\<rbrakk> \<Longrightarrow> tcopy_F6 x (ab, ba)" 
-apply(case_tac x)
+                tcopy_F5 x (b, c)\<rbrakk> \<Longrightarrow> tcopy_F6 x (ab, ba)"
 apply(auto simp:tcopy_F5.simps tcopy_F6.simps tcopy_def 
-                tstep.simps fetch.simps new_tape.simps 
+                tstep.simps fetch.simps new_tape.simps exp_zero_simp2
   split: if_splits list.splits block.splits)
-apply(rule_tac x = n in exI, simp)
-apply(rule_tac x = n in exI, simp)
-apply(drule Suc_more, simp)
-done
-
-lemma ex_less_more2: "\<lbrakk>(n::nat) < x ; x <= 2 * n\<rbrakk> \<Longrightarrow> 
-                               \<exists>y. (x = n + y & y <= n)"
-apply(rule_tac x = "x - n" in exI)
-apply(auto)
-done
-
-lemma app_app_app_simp: "xs @ ys @ za = (xs @ ys) @ za"
-apply(simp)
-done
-
-lemma [elim]: "rev xs = replicate n b \<Longrightarrow> xs = replicate n b"
-using rev_replicate[of n b]
-thm rev_equal
-by(drule_tac rev_equal, simp)
-
-lemma app_cons_tail_same[dest]: 
-  "\<lbrakk>rev b @ Oc # list = 
-    replicate (Suc (Suc na) - n) Oc @ replicate n Bk @ replicate n Oc;
-  Suc 0 < n; n \<le> Suc na; n < length list; length list \<le> 2 * n; b \<noteq> []\<rbrakk>
-  \<Longrightarrow> list = replicate n Bk @ replicate n Oc 
-           & b = replicate (Suc na - n) Oc"
-using length_append_diff_cons[of "rev b" Oc list 
-                "replicate (Suc (Suc na) - n) Oc" n Bk n]
-apply(case_tac "length list = 2*n", simp)
-using append_eq_append_conv[of "rev b @ [Oc]" "replicate 
-      (Suc (Suc na) - n) Oc" "list" "replicate n Bk @ replicate n Oc"]
-apply(case_tac n, simp, simp add: Suc_more rep_suc 
-                             del: rep_suc_rev replicate.simps, auto)
-done
-
-lemma hd_replicate_false1: "\<lbrakk>replicate x Oc \<noteq> [];
-                             hd (replicate x Oc) = Bk\<rbrakk> \<Longrightarrow> RR"
-apply(case_tac x, auto)
-done
-
-lemma hd_replicate_false2: "\<lbrakk>replicate x Oc \<noteq> [];
-                            hd (replicate x Oc) \<noteq> Oc\<rbrakk> \<Longrightarrow> RR"
-apply(case_tac x, auto)
-done
-
-lemma Suc_more_less: "\<lbrakk>n \<le> Suc m; n >= m\<rbrakk> \<Longrightarrow> n = m | n = Suc m"
-apply(auto)
-done
-
-lemma replicate_not_Nil: "replicate x a \<noteq> [] \<Longrightarrow> x > 0"
-apply(case_tac x, simp+)
+apply(rule_tac x = "Suc 0" in exI, simp add: exp_ind_def exp_zero)
+apply(rule_tac x = "Suc i" in exI, simp add: exp_ind_def)
 done
 
 lemma [elim]: "\<lbrakk>tstep (10, b, c) tcopy = (5, ab, ba); 
                 tcopy_F10 x (b, c)\<rbrakk> \<Longrightarrow> tcopy_F5 x (ab, ba)"
-apply(case_tac x)
 apply(auto simp:tcopy_F5.simps tcopy_F10.simps tcopy_def 
-                tstep.simps fetch.simps new_tape.simps
-           split: if_splits list.splits block.splits)
-apply(frule app_cons_tail_same, simp+)
-apply(rule_tac x = n in exI, auto)
+                tstep.simps fetch.simps new_tape.simps exp_zero_simp exp_zero_simp2
+                exp_ind_def tcopy_F10.simps tcopy_F10_loop.simps tcopy_F10_exit.simps
+           split: if_splits list.splits block.splits )
+apply(erule_tac [!] x = "i - 1" in allE)
+apply(erule_tac [!] x = j in allE, simp_all)
+apply(case_tac [!] i, simp_all add: exp_ind_def)
 done
 
 lemma [elim]: "\<lbrakk>tstep (4, b, c) tcopy = (5, ab, ba); 
                 tcopy_F4 x (b, c)\<rbrakk> \<Longrightarrow> tcopy_F5 x (ab, ba)" 
-apply(case_tac x)
 apply(auto simp:tcopy_F5.simps tcopy_F4.simps tcopy_def 
-                tstep.simps fetch.simps new_tape.simps
+                tstep.simps fetch.simps new_tape.simps exp_zero_simp exp_zero_simp2
            split: if_splits list.splits block.splits)
+apply(case_tac x, simp, simp add: exp_ind_def exp_zero)
+apply(erule_tac [!] x = "x - 2" in allE)
+apply(erule_tac [!] x = "Suc 0" in allE)
+apply(case_tac [!] x, simp_all add: exp_ind_def exp_zero)
+apply(case_tac [!] nat, simp_all add: exp_ind_def exp_zero)
 done
 
 lemma [elim]: "\<lbrakk>tstep (3, b, c) tcopy = (4, ab, ba); 
                 tcopy_F3 x (b, c)\<rbrakk> \<Longrightarrow> tcopy_F4 x (ab, ba)"
-apply(case_tac x)
 apply(auto simp:tcopy_F3.simps tcopy_F4.simps 
                 tcopy_def tstep.simps fetch.simps new_tape.simps
            split: if_splits list.splits block.splits)
@@ -862,86 +682,68 @@
                 tcopy_F4 x (b, c)\<rbrakk> \<Longrightarrow> tcopy_F4 x (ab, ba)" 
 apply(case_tac x)
 apply(auto simp:tcopy_F3.simps tcopy_F4.simps 
-                tcopy_def tstep.simps fetch.simps new_tape.simps
+                tcopy_def tstep.simps fetch.simps new_tape.simps exp_zero_simp exp_zero_simp2 exp_ind_def
   split: if_splits list.splits block.splits)
 done
 
 lemma [elim]: "\<lbrakk>tstep (3, b, c) tcopy = (3, ab, ba); 
                 tcopy_F3 x (b, c)\<rbrakk> \<Longrightarrow> tcopy_F3 x (ab, ba)"
-apply(case_tac x)
 apply(auto simp:tcopy_F3.simps tcopy_F4.simps 
                 tcopy_def tstep.simps fetch.simps new_tape.simps 
   split: if_splits list.splits block.splits)
 done
 
-lemma replicate_cons_back: "y # replicate x y = replicate (Suc x) y"
-apply(simp)
-done
-
-lemma replicate_cons_same: "bs @ (b # cs) = y # replicate x y \<Longrightarrow> 
-        (\<exists>n. bs = replicate n y) & (b = y) & (\<exists>m. cs = replicate m y)"
-apply(simp only: replicate_cons_back)
-apply(drule_tac replicate_same)
-apply(simp)
-done
-
 lemma [elim]: "\<lbrakk>tstep (2, b, c) tcopy = (3, ab, ba); 
                 tcopy_F2 x (b, c)\<rbrakk> \<Longrightarrow> tcopy_F3 x (ab, ba)" 
 apply(case_tac x)
 apply(auto simp:tcopy_F3.simps tcopy_F2.simps 
                 tcopy_def tstep.simps fetch.simps new_tape.simps
+                exp_zero_simp exp_zero_simp2 exp_zero
   split: if_splits list.splits block.splits)
-apply(drule replicate_cons_same, auto)+
+apply(case_tac [!] j, simp_all add: exp_zero exp_ind_def)
 done
 
 lemma [elim]: "\<lbrakk>tstep (2, b, c) tcopy = (2, ab, ba); 
                 tcopy_F2 x (b, c)\<rbrakk> \<Longrightarrow> tcopy_F2 x (ab, ba)"
-apply(case_tac x)
 apply(auto simp:tcopy_F3.simps tcopy_F2.simps 
-                tcopy_def tstep.simps fetch.simps new_tape.simps
+                tcopy_def tstep.simps fetch.simps new_tape.simps 
+                exp_zero_simp exp_zero_simp2 exp_zero
   split: if_splits list.splits block.splits)
-apply(frule replicate_cons_same, auto)
-apply(simp add: replicate_app_Cons_same)
+apply(rule_tac x = "Suc i" in exI, simp add: exp_ind_def exp_zero)
+apply(rule_tac x = "j - 1" in exI, simp)
+apply(case_tac j, simp_all add: exp_ind_def exp_zero)
 done
 
 lemma [elim]: "\<lbrakk>tstep (Suc 0, b, c) tcopy = (2, ab, ba); 
-                tcopy_F1 x (b, c)\<rbrakk> \<Longrightarrow> tcopy_F2 x (ab, ba)" 
-apply(case_tac x)
-apply(simp_all add:tcopy_F2.simps tcopy_F1.simps 
-                   tcopy_def tstep.simps fetch.simps new_tape.simps)
-apply(auto)
+                tcopy_F1 x (b, c)\<rbrakk> \<Longrightarrow> tcopy_F2 x (ab, ba)"
+apply(auto simp:tcopy_F1.simps tcopy_F2.simps 
+                tcopy_def tstep.simps fetch.simps new_tape.simps 
+                exp_zero_simp exp_zero_simp2 exp_zero
+             split: if_splits list.splits block.splits)
+apply(rule_tac x = "Suc 0" in exI, simp)
+apply(rule_tac x = "x - 1" in exI, simp)
+apply(case_tac x, simp_all add: exp_ind_def exp_zero)
 done
 
 lemma [elim]: "\<lbrakk>tstep (Suc 0, b, c) tcopy = (0, ab, ba); 
                 tcopy_F1 x (b, c)\<rbrakk> \<Longrightarrow> tcopy_F0 x (ab, ba)"
-apply(case_tac x)
 apply(simp_all add:tcopy_F0.simps tcopy_F1.simps 
-                   tcopy_def tstep.simps fetch.simps new_tape.simps)
-done
-
-lemma ex_less: "Suc x <= y \<Longrightarrow> \<exists>z. y = x + z & z > 0"
-apply(rule_tac x = "y - x" in exI, auto)
-done
-
-lemma [elim]: "\<lbrakk>xs @ Bk # ba = 
-  Bk # Oc # replicate n Oc @ Bk # Oc # replicate n Oc; 
-  length xs \<le> Suc n; xs \<noteq> []\<rbrakk> \<Longrightarrow> RR"
-apply(case_tac xs, auto)
-apply(case_tac list, auto)
-apply(drule ex_less, auto)
-apply(simp add: replicate_add)
-apply(auto)
-apply(case_tac z, simp+)
+                   tcopy_def tstep.simps fetch.simps new_tape.simps
+                   exp_zero_simp exp_zero_simp2 exp_zero
+         split: if_splits list.splits block.splits )
+apply(case_tac x, simp_all add: exp_ind_def exp_zero, auto)
 done
 
 lemma [elim]: "\<lbrakk>tstep (15, b, c) tcopy = (0, ab, ba); 
                 tcopy_F15 x (b, c)\<rbrakk> \<Longrightarrow> tcopy_F0 x (ab, ba)"
-apply(case_tac x)
 apply(auto simp: tcopy_F15.simps tcopy_F0.simps 
                  tcopy_def tstep.simps new_tape.simps fetch.simps
            split: if_splits list.splits block.splits)
+apply(rule_tac x = "Suc 0" in exI, simp add: exp_ind_def exp_zero)
+apply(case_tac [!] j, simp_all add: exp_ind_def exp_zero)
 done
 
+
 lemma [elim]: "\<lbrakk>tstep (0, b, c) tcopy = (0, ab, ba); 
                 tcopy_F0 x (b, c)\<rbrakk> \<Longrightarrow> tcopy_F0 x (ab, ba)" 
 apply(case_tac x)
@@ -968,7 +770,7 @@
   Invariant under mult-step execution.
   *}
 lemma inv_tcopy_steps: 
-  "inv_tcopy x (steps (Suc 0, [], replicate x Oc) tcopy stp) "
+  "inv_tcopy x (steps (Suc 0, [], Oc\<^bsup>x\<^esup>) tcopy stp) "
 apply(induct stp)
 apply(simp add: tstep.simps tcopy_def steps.simps 
                 tcopy_F1.simps inv_tcopy.simps)
@@ -976,18 +778,6 @@
 done
   
 
-text {*
-  The followng lemmas gives the parital correctness of Copying TM.
-*}
-theorem inv_tcopy_rs: 
-  "steps (Suc 0, [], replicate x Oc) tcopy stp = (0, l, r)
-  \<Longrightarrow> \<exists> n. l = replicate n Bk \<and> 
-           r = replicate x Oc @ Bk # replicate x Oc"
-apply(insert inv_tcopy_steps[of x stp])
-apply(auto simp: inv_tcopy.simps tcopy_F0.simps isBk.simps)
-done
-
-
 
 
 (*----------halt problem of tcopy----------------------------------------*)
@@ -1183,7 +973,6 @@
  tcopy_state.simps tcopy_step.simps)
 apply(simp split: if_splits list.splits block.splits taction.splits)
 apply(auto)
-apply(case_tac x, simp+)
 done
 
 lemma [elim]: "tcopy_F4 x (b, c) \<Longrightarrow> 
@@ -1193,7 +982,7 @@
  lex_square_def lex_triple_def lex_pair_def tcopy_phase.simps 
  tcopy_stage.simps tcopy_state.simps tcopy_step.simps)
 apply(simp split: if_splits list.splits block.splits taction.splits)
-apply(auto)
+apply(auto simp: exp_ind_def)
 done
 
 lemma[simp]: "takeWhile (\<lambda>a. a = b) (replicate x b @ ys) = 
@@ -1226,7 +1015,7 @@
 apply(simp split: if_splits list.splits block.splits taction.splits)
 apply(auto)
 apply(simp_all add: tcopy_phase.simps tcopy_stage.simps 
-                    tcopy_state.simps tcopy_step.simps)
+                    tcopy_state.simps tcopy_step.simps exponent_def)
 done
 
 lemma [elim]: "tcopy_F7 x (b, c) \<Longrightarrow> 
@@ -1235,7 +1024,7 @@
 apply(simp add: tstep.simps tcopy_def tcopy_LE_def lex_square_def 
                 lex_triple_def lex_pair_def tcopy_phase.simps)
 apply(simp split: if_splits list.splits block.splits taction.splits)
-apply(auto)
+apply(auto simp: exp_zero_simp)
 apply(simp_all add: tcopy_phase.simps tcopy_stage.simps 
                     tcopy_state.simps tcopy_step.simps)
 done
@@ -1246,12 +1035,14 @@
 apply(simp add: tstep.simps tcopy_def tcopy_LE_def lex_square_def 
                 lex_triple_def lex_pair_def tcopy_phase.simps)
 apply(simp split: if_splits list.splits block.splits taction.splits)
-apply(auto)
+apply(auto simp: exp_zero_simp)
 apply(simp_all add: tcopy_phase.simps tcopy_stage.simps 
-                    tcopy_state.simps tcopy_step.simps)
-apply(simp only: app_cons_app_simp, frule replicate_tail_length, simp)
+                    tcopy_state.simps tcopy_step.simps exponent_def)
 done
 
+lemma rev_equal_rev: "rev a = rev b \<Longrightarrow> a = b"
+by simp
+
 lemma app_app_app_equal: "xs @ ys @ zs = (xs @ ys) @ zs"
 by simp
 
@@ -1266,34 +1057,40 @@
 apply(simp)
 done
 
+lemma[simp]: "takeWhile (\<lambda>a. a = b) (replicate x b @ ys) = 
+             replicate x b @ (takeWhile (\<lambda>a. a = b) ys)"
+apply(induct x)
+apply(simp+)
+done
+
 lemma [elim]: "tcopy_F9 x (b, c) \<Longrightarrow> 
                       (tstep (9, b, c) tcopy, 9, b, c) \<in> tcopy_LE"
-apply(case_tac x, simp)
 apply(simp add: tstep.simps tcopy_def tcopy_LE_def lex_square_def 
-                lex_triple_def lex_pair_def tcopy_phase.simps)
+                lex_triple_def lex_pair_def tcopy_phase.simps tcopy_F9.simps
+                tcopy_F9_loop.simps tcopy_F9_exit.simps)
 apply(simp split: if_splits list.splits block.splits taction.splits)
 apply(auto)
-apply(simp_all add: tcopy_phase.simps tcopy_stage.simps 
-                    tcopy_state.simps tcopy_step.simps)
-apply(drule_tac bs = b and as = "Bk # list" in rev_tl_hd_merge)
-apply(simp)
-apply(drule_tac bs = b and as = "Oc # list" in rev_tl_hd_merge)
-apply(simp)
+apply(simp_all add: tcopy_phase.simps tcopy_stage.simps  tcopy_F9_loop.simps
+                    tcopy_state.simps tcopy_step.simps tstep.simps exp_zero_simp
+                    exponent_def)
+apply(case_tac [1-2] t, simp_all add: rev_tl_hd_merge)
+apply(case_tac j, simp, simp)
+apply(case_tac nat, simp_all)
+apply(case_tac nata, simp_all)
 done
 
 lemma [elim]: "tcopy_F10 x (b, c) \<Longrightarrow> 
               (tstep (10, b, c) tcopy, 10, b, c) \<in> tcopy_LE"
-apply(case_tac x, simp)
 apply(simp add: tstep.simps tcopy_def tcopy_LE_def lex_square_def 
-                lex_triple_def lex_pair_def tcopy_phase.simps)
+                lex_triple_def lex_pair_def tcopy_phase.simps tcopy_F10_loop.simps
+                tcopy_F10_exit.simps exp_zero_simp)
 apply(simp split: if_splits list.splits block.splits taction.splits)
-apply(auto)
+apply(auto simp: exp_zero_simp)
 apply(simp_all add: tcopy_phase.simps tcopy_stage.simps 
-                    tcopy_state.simps tcopy_step.simps)
-apply(drule_tac bs = b and as = "Bk # list" in rev_tl_hd_merge)
-apply(simp)
-apply(drule_tac bs = b and as = "Oc # list" in rev_tl_hd_merge)
-apply(simp)
+                    tcopy_state.simps tcopy_step.simps exponent_def
+                    rev_tl_hd_merge)
+apply(case_tac k, simp_all)
+apply(case_tac nat, simp_all)
 done
 
 lemma [elim]: "tcopy_F11 x (b, c) \<Longrightarrow> 
@@ -1313,6 +1110,7 @@
 apply(auto)
 apply(simp_all add: tcopy_phase.simps tcopy_stage.simps 
                     tcopy_state.simps tcopy_step.simps)
+apply(simp_all add: exp_ind_def)
 done
 
 lemma [elim]: "tcopy_F13 x (b, c) \<Longrightarrow> 
@@ -1324,7 +1122,6 @@
 apply(auto)
 apply(simp_all add: tcopy_phase.simps tcopy_stage.simps 
                     tcopy_state.simps tcopy_step.simps)
-apply(drule equal_length, simp)+
 done
 
 lemma [elim]: "tcopy_F14 x (b, c) \<Longrightarrow> 
@@ -1349,24 +1146,37 @@
                     tcopy_state.simps tcopy_step.simps)
 done
 
+lemma exp_length: "length (a\<^bsup>b\<^esup>) = b"
+apply(induct b, simp_all add: exp_zero exp_ind_def)
+done
+
+declare tcopy_F9.simps[simp del] tcopy_F10.simps[simp del]
+
+lemma length_eq: "xs = ys \<Longrightarrow> length xs = length ys"
+by simp
+
 lemma tcopy_wf_step:"\<lbrakk>a > 0; inv_tcopy x (a, b, c)\<rbrakk> \<Longrightarrow> 
                      (tstep (a, b, c) tcopy, (a, b, c)) \<in> tcopy_LE"
 apply(simp add:inv_tcopy.simps split: if_splits, auto)
 apply(auto simp: tstep.simps tcopy_def  tcopy_LE_def lex_square_def 
                  lex_triple_def lex_pair_def tcopy_phase.simps 
                  tcopy_stage.simps tcopy_state.simps tcopy_step.simps
+                 exp_length exp_zero_simp exponent_def
            split: if_splits list.splits block.splits taction.splits)
+apply(case_tac [!] t, simp_all)
+apply(case_tac j, simp_all)
+apply(drule_tac length_eq, simp)
 done
 
 lemma tcopy_wf: 
-"\<forall>n. let nc = steps (Suc 0, [], replicate x Oc) tcopy n in 
-      let Sucnc = steps (Suc 0, [], replicate x Oc) tcopy (Suc n) in
+"\<forall>n. let nc = steps (Suc 0, [], Oc\<^bsup>x\<^esup>) tcopy n in 
+      let Sucnc = steps (Suc 0, [], Oc\<^bsup>x\<^esup>) tcopy (Suc n) in
   \<not> isS0 nc \<longrightarrow> ((Sucnc, nc) \<in> tcopy_LE)"
 proof(rule allI, case_tac 
-   "steps (Suc 0, [], replicate x Oc) tcopy n", auto simp: tstep_red)
+   "steps (Suc 0, [], Oc\<^bsup>x\<^esup>) tcopy n", auto simp: tstep_red)
   fix n a b c
   assume h: "\<not> isS0 (a, b, c)" 
-       "steps (Suc 0, [], replicate x Oc) tcopy n = (a, b, c)"
+       "steps (Suc 0, [], Oc\<^bsup>x\<^esup>) tcopy n = (a, b, c)"
   hence  "inv_tcopy x (a, b, c)"
     using inv_tcopy_steps[of x n] by(simp)
   thus "(tstep (a, b, c) tcopy, a, b, c) \<in> tcopy_LE"
@@ -1378,9 +1188,9 @@
   The termination of Copying TM:
 *}
 lemma tcopy_halt: 
-  "\<exists>n. isS0 (steps (Suc 0, [], replicate x Oc) tcopy n)"
+  "\<exists>n. isS0 (steps (Suc 0, [], Oc\<^bsup>x\<^esup>) tcopy n)"
 apply(insert halt_lemma 
-        [of tcopy_LE isS0 "steps (Suc 0, [], replicate x Oc) tcopy"])
+        [of tcopy_LE isS0 "steps (Suc 0, [], Oc\<^bsup>x\<^esup>) tcopy"])
 apply(insert tcopy_wf [of x])
 apply(simp only: Let_def)
 apply(insert wf_tcopy_le)
@@ -1390,20 +1200,20 @@
 text {*
   The total correntess of Copying TM:
 *}
-theorem tcopy_halt_rs: "\<exists>stp m. 
-  steps (Suc 0, [], replicate x Oc) tcopy stp = 
-       (0, replicate m Bk, replicate x Oc @ Bk # replicate x Oc)"
+theorem tcopy_halt_rs: 
+  "\<exists>stp m. 
+   steps (Suc 0, [], Oc\<^bsup>x\<^esup>) tcopy stp = 
+       (0, Bk\<^bsup>m\<^esup>, Oc\<^bsup>x\<^esup> @ Bk # Oc\<^bsup>x\<^esup>)"
 using tcopy_halt[of x]
 proof(erule_tac exE)
   fix n
-  assume h: "isS0 (steps (Suc 0, [], replicate x Oc) tcopy n)"
-  have "inv_tcopy x (steps (Suc 0, [], replicate x Oc) tcopy n)"
+  assume h: "isS0 (steps (Suc 0, [], Oc\<^bsup>x\<^esup>) tcopy n)"
+  have "inv_tcopy x (steps (Suc 0, [], Oc\<^bsup>x\<^esup>) tcopy n)"
     using inv_tcopy_steps[of x n] by simp
   thus "?thesis"
     using h
-    apply(cases "(steps (Suc 0, [], replicate x Oc) tcopy n)", 
+    apply(cases "(steps (Suc 0, [], Oc\<^bsup>x\<^esup>) tcopy n)", 
           auto simp: isS0_def inv_tcopy.simps)
-    apply(rule_tac x = n in exI, auto)
     done
 qed
 
@@ -1505,10 +1315,10 @@
   *}
   and h_case: 
   "\<And> M n. \<lbrakk>(haltP M n)\<rbrakk> \<Longrightarrow> 
-             \<exists> na nb. (steps (Suc 0, Bk\<^bsup>x\<^esup>, Oc\<^bsup>code M\<^esup> @ Bk # Oc\<^bsup>n\<^esup>) H na = (0, Bk\<^bsup>nb\<^esup>, [Oc]))"
+             \<exists> na nb. (steps (Suc 0, [], Oc\<^bsup>code M\<^esup> @ Bk # Oc\<^bsup>n\<^esup>) H na = (0, Bk\<^bsup>nb\<^esup>, [Oc]))"
   and nh_case: 
   "\<And> M n. \<lbrakk>(\<not> haltP M n)\<rbrakk> \<Longrightarrow>
-             \<exists> na nb. (steps (Suc 0, Bk\<^bsup>x\<^esup>, Oc\<^bsup>code M\<^esup> @ Bk # Oc\<^bsup>n\<^esup>) H na = (0, Bk\<^bsup>nb\<^esup>, [Oc, Oc]))"
+             \<exists> na nb. (steps (Suc 0, [],  Oc\<^bsup>code M\<^esup> @ Bk # Oc\<^bsup>n\<^esup>) H na = (0, Bk\<^bsup>nb\<^esup>, [Oc, Oc]))"
 begin
 
 term t_correct
@@ -1519,6 +1329,117 @@
 
 lemma [simp]: "a\<^bsup>0\<^esup> = []"
   by(simp add: exponent_def)
+
+lemma tinres_ex1:
+  "tinres (Bk\<^bsup>nb\<^esup>) b \<Longrightarrow> \<exists>nb. b = Bk\<^bsup>nb\<^esup>"
+apply(auto simp: tinres_def)
+proof -
+  fix n
+  assume "Bk\<^bsup>nb\<^esup> = b @ Bk\<^bsup>n\<^esup>"
+  thus "\<exists>nb. b = Bk\<^bsup>nb\<^esup>"
+  proof(induct b arbitrary: nb)
+    show "\<exists>nb. [] = Bk\<^bsup>nb\<^esup>"
+      by(rule_tac x = 0 in exI, simp add: exp_zero)
+  next
+    fix a b nb
+    assume ind: "\<And>nb. Bk\<^bsup>nb\<^esup> = b @ Bk\<^bsup>n\<^esup> \<Longrightarrow> \<exists>nb. b = Bk\<^bsup>nb\<^esup>"
+    and h: "Bk\<^bsup>nb\<^esup> = (a # b) @ Bk\<^bsup>n\<^esup>"
+    from h show "\<exists>nb. a # b = Bk\<^bsup>nb\<^esup>"
+    proof(case_tac a, case_tac nb, simp_all add: exp_ind_def)
+      fix nat
+      assume "Bk\<^bsup>nat\<^esup> = b @ Bk\<^bsup>n\<^esup>"
+      thus "\<exists>nb. Bk # b = Bk\<^bsup>nb\<^esup>"
+        using ind[of nat]
+        apply(auto)
+        apply(rule_tac x = "Suc nb" in exI, simp add: exp_ind_def)
+        done
+    next
+      assume "Bk\<^bsup>nb\<^esup> = Oc # b @ Bk\<^bsup>n\<^esup>"
+      thus "\<exists>nb. Oc # b = Bk\<^bsup>nb\<^esup>"
+        apply(case_tac nb, simp_all add: exp_ind_def)
+        done
+    qed
+  qed
+next
+  fix n
+  show "\<exists>nba. Bk\<^bsup>nb\<^esup> @ Bk\<^bsup>n\<^esup> = Bk\<^bsup>nba\<^esup>"
+    apply(rule_tac x = "nb + n" in exI)
+    apply(simp add: exponent_def replicate_add)
+    done
+qed
+
+lemma h_newcase: "\<And> M n. \<lbrakk>(haltP M n)\<rbrakk> \<Longrightarrow> 
+             \<exists> na nb. (steps (Suc 0, Bk\<^bsup>x\<^esup>, Oc\<^bsup>code M\<^esup> @ Bk # Oc\<^bsup>n\<^esup>) H na = (0, Bk\<^bsup>nb\<^esup>, [Oc]))"
+proof -
+  fix M n x
+  assume "haltP M n"
+  hence " \<exists> na nb. (steps (Suc 0, [], Oc\<^bsup>code M\<^esup> @ Bk # Oc\<^bsup>n\<^esup>) H na
+            = (0, Bk\<^bsup>nb\<^esup>, [Oc]))"
+    apply(erule_tac h_case)
+    done
+  from this obtain na nb where 
+    cond1:"(steps (Suc 0, [], Oc\<^bsup>code M\<^esup> @ Bk # Oc\<^bsup>n\<^esup>) H na
+            = (0, Bk\<^bsup>nb\<^esup>, [Oc]))" by blast
+  thus "\<exists> na nb. (steps (Suc 0, Bk\<^bsup>x\<^esup>, Oc\<^bsup>code M\<^esup> @ Bk # Oc\<^bsup>n\<^esup>) H na = (0, Bk\<^bsup>nb\<^esup>, [Oc]))"
+  proof(rule_tac x = na in exI, case_tac "steps (Suc 0, Bk\<^bsup>x\<^esup>, Oc\<^bsup>code M\<^esup> @ Bk # Oc\<^bsup>n\<^esup>) H na", simp)
+    fix a b c
+    assume cond2: "steps (Suc 0, Bk\<^bsup>x\<^esup>, Oc\<^bsup>code M\<^esup> @ Bk # Oc\<^bsup>n\<^esup>) H na = (a, b, c)"
+    have "tinres (Bk\<^bsup>nb\<^esup>) b \<and> [Oc] = c \<and> 0 = a"
+    proof(rule_tac tinres_steps)
+      show "tinres [] (Bk\<^bsup>x\<^esup>)"
+        apply(simp add: tinres_def)
+        apply(auto)
+        done
+    next
+      show "(steps (Suc 0, [], Oc\<^bsup>code M\<^esup> @ Bk # Oc\<^bsup>n\<^esup>) H na
+            = (0, Bk\<^bsup>nb\<^esup>, [Oc]))"
+        by(simp add: cond1)
+    next
+      show "steps (Suc 0, Bk\<^bsup>x\<^esup>, Oc\<^bsup>code M\<^esup> @ Bk # Oc\<^bsup>n\<^esup>) H na = (a, b, c)"
+        by(simp add: cond2)
+    qed
+    thus "a = 0 \<and> (\<exists>nb. b = Bk\<^bsup>nb\<^esup>) \<and> c = [Oc]"
+      apply(auto simp: tinres_ex1)
+      done
+  qed
+qed
+
+lemma nh_newcase: "\<And> M n. \<lbrakk>\<not> (haltP M n)\<rbrakk> \<Longrightarrow> 
+             \<exists> na nb. (steps (Suc 0, Bk\<^bsup>x\<^esup>, Oc\<^bsup>code M\<^esup> @ Bk # Oc\<^bsup>n\<^esup>) H na = (0, Bk\<^bsup>nb\<^esup>, [Oc, Oc]))"
+proof -
+  fix M n
+  assume "\<not> haltP M n"
+  hence "\<exists> na nb. (steps (Suc 0, [], Oc\<^bsup>code M\<^esup> @ Bk # Oc\<^bsup>n\<^esup>) H na
+            = (0, Bk\<^bsup>nb\<^esup>, [Oc, Oc]))"
+    apply(erule_tac nh_case)
+    done
+  from this obtain na nb where 
+    cond1: "(steps (Suc 0, [], Oc\<^bsup>code M\<^esup> @ Bk # Oc\<^bsup>n\<^esup>) H na
+            = (0, Bk\<^bsup>nb\<^esup>, [Oc, Oc]))" by blast
+  thus "\<exists> na nb. (steps (Suc 0, Bk\<^bsup>x\<^esup>, Oc\<^bsup>code M\<^esup> @ Bk # Oc\<^bsup>n\<^esup>) H na = (0, Bk\<^bsup>nb\<^esup>, [Oc, Oc]))"
+  proof(rule_tac x = na in exI, case_tac "steps (Suc 0, Bk\<^bsup>x\<^esup>, Oc\<^bsup>code M\<^esup> @ Bk # Oc\<^bsup>n\<^esup>) H na", simp)
+    fix a b c
+    assume cond2: "steps (Suc 0, Bk\<^bsup>x\<^esup>, Oc\<^bsup>code M\<^esup> @ Bk # Oc\<^bsup>n\<^esup>) H na = (a, b, c)"
+    have "tinres (Bk\<^bsup>nb\<^esup>) b \<and> [Oc, Oc] = c \<and> 0 = a"
+    proof(rule_tac tinres_steps)
+      show "tinres [] (Bk\<^bsup>x\<^esup>)"
+        apply(simp add: tinres_def)
+        apply(auto)
+        done
+    next
+      show "(steps (Suc 0, [], Oc\<^bsup>code M\<^esup> @ Bk # Oc\<^bsup>n\<^esup>) H na
+            = (0, Bk\<^bsup>nb\<^esup>, [Oc, Oc]))"
+        by(simp add: cond1)
+    next
+      show "steps (Suc 0, Bk\<^bsup>x\<^esup>, Oc\<^bsup>code M\<^esup> @ Bk # Oc\<^bsup>n\<^esup>) H na = (a, b, c)"
+        by(simp add: cond2)
+    qed
+    thus "a = 0 \<and> (\<exists>nb. b = Bk\<^bsup>nb\<^esup>) \<and> c = [Oc, Oc]"
+      apply(auto simp: tinres_ex1)
+      done
+  qed
+qed
+     
 lemma haltP_weaking: 
   "haltP (tcontra H) (code (tcontra H)) \<Longrightarrow> 
     \<exists>stp. isS0 (steps (Suc 0, [], Oc\<^bsup>code (tcontra H)\<^esup>) 
@@ -1541,7 +1462,7 @@
   assume h: "haltP (tcontra H) (code (tcontra H))"
   hence h1: "\<And> x. \<exists> na nb. steps (Suc 0, Bk\<^bsup>x\<^esup>, Oc\<^bsup>code (tcontra H)\<^esup> @ Bk # 
                        Oc\<^bsup>code (tcontra H)\<^esup>) H na = (0, Bk\<^bsup>nb\<^esup>, [Oc])"
-    by(drule_tac x = x in h_case, simp)
+    by(drule_tac x = x in h_newcase, simp)
   have "?P1 \<turnstile>-> \<lambda> tp. (\<exists> stp tp'. steps (Suc 0, tp) (tcopy |+| H) stp = (0, tp') \<and> ?Q2 tp')"
   proof(rule_tac turing_merge.t_merge_halt[of tcopy H "?P1" "?P2" "?P3" 
          "?P3" "?Q1" "?Q2"], auto simp: turing_merge_def)
@@ -1605,7 +1526,7 @@
   have h1: "\<And> x. \<exists> na nb. steps (Suc 0, Bk\<^bsup>x\<^esup>, Oc\<^bsup>?cn\<^esup> @ Bk # Oc\<^bsup>?cn\<^esup>)
                              H na = (0, Bk\<^bsup>nb\<^esup>, [Oc, Oc])"
     using uh
-    by(drule_tac x = x in nh_case, simp)
+    by(drule_tac x = x in nh_newcase, simp)
   let ?P1 = "\<lambda> tp. let (l, r) = tp in (l = [] \<and> 
                         (r::block list) = Oc\<^bsup>(?cn)\<^esup>)"
   let ?Q1 = "\<lambda> (l, r).(\<exists> na. l = Bk\<^bsup>na\<^esup> \<and> r = [Oc, Oc])"