diff -r a63c3f8d7234 -r 67063c5365e1 thys/Abacus.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/thys/Abacus.thy	Sun Feb 10 19:49:07 2013 +0000
@@ -0,0 +1,4974 @@
+header {* 
+ {\em abacus} a kind of register machine
+*}
+
+theory Abacus
+imports Uncomputable
+begin
+
+(*
+declare tm_comp.simps [simp add] 
+declare adjust.simps[simp add] 
+declare shift.simps[simp add]
+declare tm_wf.simps[simp add]
+declare step.simps[simp add]
+declare steps.simps[simp add]
+*)
+declare replicate_Suc[simp add]
+
+text {*
+  {\em Abacus} instructions:
+*}
+
+datatype abc_inst =
+  -- {* @{text "Inc n"} increments the memory cell (or register) with address @{text "n"} by one.
+     *}
+     Inc nat
+  -- {*
+     @{text "Dec n label"} decrements the memory cell with address @{text "n"} by one. 
+      If cell @{text "n"} is already zero, no decrements happens and the executio jumps to
+      the instruction labeled by @{text "label"}.
+     *}
+   | Dec nat nat
+  -- {*
+  @{text "Goto label"} unconditionally jumps to the instruction labeled by @{text "label"}.
+  *}
+   | Goto nat
+  
+
+text {*
+  Abacus programs are defined as lists of Abacus instructions.
+*}
+type_synonym abc_prog = "abc_inst list"
+
+section {*
+  Sample Abacus programs
+  *}
+
+text {*
+  Abacus for addition and clearance.
+*}
+fun plus_clear :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> abc_prog"  
+  where
+  "plus_clear m n e = [Dec m e, Inc n, Goto 0]"
+
+text {*
+  Abacus for clearing memory untis.
+*}
+fun clear :: "nat \<Rightarrow> nat \<Rightarrow> abc_prog"
+  where
+  "clear n e = [Dec n e, Goto 0]"
+
+fun plus:: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> abc_prog"
+  where
+  "plus m n p e = [Dec m 4, Inc n, Inc p,
+                   Goto 0, Dec p e, Inc m, Goto 4]"
+
+fun mult :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> abc_prog"
+  where
+  "mult m1 m2 n p e = [Dec m1 e]@ plus m1 m2 p 1"
+
+fun expo :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> abc_prog"
+  where
+  "expo n m1 m2 p e = [Inc n, Dec m1 e] @ mult m2 n n p 2"
+
+
+text {*
+  The state of Abacus machine.
+  *}
+type_synonym abc_state = nat
+
+(* text {*
+  The memory of Abacus machine is defined as a function from address to contents.
+*}
+type_synonym abc_mem = "nat \<Rightarrow> nat" *)
+
+text {*
+  The memory of Abacus machine is defined as a list of contents, with 
+  every units addressed by index into the list.
+  *}
+type_synonym abc_lm = "nat list"
+
+text {*
+  Fetching contents out of memory. Units not represented by list elements are considered
+  as having content @{text "0"}.
+*}
+fun abc_lm_v :: "abc_lm \<Rightarrow> nat \<Rightarrow> nat"
+  where 
+    "abc_lm_v lm n = (if (n < length lm) then (lm!n) else 0)"         
+
+
+text {*
+  Set the content of memory unit @{text "n"} to value @{text "v"}.
+  @{text "am"} is the Abacus memory before setting.
+  If address @{text "n"} is outside to scope of @{text "am"}, @{text "am"} 
+  is extended so that @{text "n"} becomes in scope.
+*}
+
+fun abc_lm_s :: "abc_lm \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> abc_lm"
+  where
+    "abc_lm_s am n v = (if (n < length am) then (am[n:=v]) else 
+                           am@ (replicate (n - length am) 0) @ [v])"
+
+
+text {*
+  The configuration of Abaucs machines consists of its current state and its
+  current memory:
+*}
+type_synonym abc_conf = "abc_state \<times> abc_lm"
+
+text {*
+  Fetch instruction out of Abacus program:
+*}
+
+fun abc_fetch :: "nat \<Rightarrow> abc_prog \<Rightarrow> abc_inst option" 
+  where
+  "abc_fetch s p = (if (s < length p) then Some (p ! s)
+                    else None)"
+
+text {*
+  Single step execution of Abacus machine. If no instruction is feteched, 
+  configuration does not change.
+*}
+fun abc_step_l :: "abc_conf \<Rightarrow> abc_inst option \<Rightarrow> abc_conf"
+  where
+  "abc_step_l (s, lm) a = (case a of 
+               None \<Rightarrow> (s, lm) |
+               Some (Inc n)  \<Rightarrow> (let nv = abc_lm_v lm n in
+                       (s + 1, abc_lm_s lm n (nv + 1))) |
+               Some (Dec n e) \<Rightarrow> (let nv = abc_lm_v lm n in
+                       if (nv = 0) then (e, abc_lm_s lm n 0) 
+                       else (s + 1,  abc_lm_s lm n (nv - 1))) |
+               Some (Goto n) \<Rightarrow> (n, lm) 
+               )"
+
+text {*
+  Multi-step execution of Abacus machine.
+*}
+fun abc_steps_l :: "abc_conf \<Rightarrow> abc_prog \<Rightarrow> nat \<Rightarrow> abc_conf"
+  where
+  "abc_steps_l (s, lm) p 0 = (s, lm)" |
+  "abc_steps_l (s, lm) p (Suc n) = 
+      abc_steps_l (abc_step_l (s, lm) (abc_fetch s p)) p n"
+
+section {*
+  Compiling Abacus machines into Truing machines
+*}
+
+subsection {*
+  Compiling functions
+*}
+
+text {*
+  @{text "findnth n"} returns the TM which locates the represention of
+  memory cell @{text "n"} on the tape and changes representation of zero
+  on the way.
+*}
+
+fun findnth :: "nat \<Rightarrow> instr list"
+  where
+  "findnth 0 = []" |
+  "findnth (Suc n) = (findnth n @ [(W1, 2 * n + 1), 
+           (R, 2 * n + 2), (R, 2 * n + 3), (R, 2 * n + 2)])"
+
+text {*
+  @{text "tinc_b"} returns the TM which increments the representation 
+  of the memory cell under rw-head by one and move the representation 
+  of cells afterwards to the right accordingly.
+  *}
+
+definition tinc_b :: "instr list"
+  where
+  "tinc_b \<equiv> [(W1, 1), (R, 2), (W1, 3), (R, 2), (W1, 3), (R, 4), 
+             (L, 7), (W0, 5), (R, 6), (W0, 5), (W1, 3), (R, 6),
+             (L, 8), (L, 7), (R, 9), (L, 7), (R, 10), (W0, 9)]" 
+
+text {*
+  @{text "tinc ss n"} returns the TM which simulates the execution of 
+  Abacus instruction @{text "Inc n"}, assuming that TM is located at
+  location @{text "ss"} in the final TM complied from the whole
+  Abacus program.
+*}
+
+fun tinc :: "nat \<Rightarrow> nat \<Rightarrow> instr list"
+  where
+  "tinc ss n = shift (findnth n @ shift tinc_b (2 * n)) (ss - 1)"
+
+text {*
+  @{text "tinc_b"} returns the TM which decrements the representation 
+  of the memory cell under rw-head by one and move the representation 
+  of cells afterwards to the left accordingly.
+  *}
+
+definition tdec_b :: "instr list"
+  where
+  "tdec_b \<equiv>  [(W1, 1), (R, 2), (L, 14), (R, 3), (L, 4), (R, 3),
+              (R, 5), (W0, 4), (R, 6), (W0, 5), (L, 7), (L, 8),
+              (L, 11), (W0, 7), (W1, 8), (R, 9), (L, 10), (R, 9),
+              (R, 5), (W0, 10), (L, 12), (L, 11), (R, 13), (L, 11),
+              (R, 17), (W0, 13), (L, 15), (L, 14), (R, 16), (L, 14),
+              (R, 0), (W0, 16)]"
+
+text {*
+  @{text "sete tp e"} attaches the termination edges (edges leading to state @{text "0"}) 
+  of TM @{text "tp"} to the intruction labelled by @{text "e"}.
+  *}
+
+fun sete :: "instr list \<Rightarrow> nat \<Rightarrow> instr list"
+  where
+  "sete tp e = map (\<lambda> (action, state). (action, if state = 0 then e else state)) tp"
+
+text {*
+  @{text "tdec ss n label"} returns the TM which simulates the execution of 
+  Abacus instruction @{text "Dec n label"}, assuming that TM is located at
+  location @{text "ss"} in the final TM complied from the whole
+  Abacus program.
+*}
+
+fun tdec :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> instr list"
+  where
+  "tdec ss n e = shift (findnth n) (ss - 1) @ sete (shift (shift tdec_b (2 * n)) (ss - 1)) e"
+ 
+text {*
+  @{text "tgoto f(label)"} returns the TM simulating the execution of Abacus instruction
+  @{text "Goto label"}, where @{text "f(label)"} is the corresponding location of
+  @{text "label"} in the final TM compiled from the overall Abacus program.
+*}
+
+fun tgoto :: "nat \<Rightarrow> instr list"
+  where
+  "tgoto n = [(Nop, n), (Nop, n)]"
+
+text {*
+  The layout of the final TM compiled from an Abacus program is represented
+  as a list of natural numbers, where the list element at index @{text "n"} represents the 
+  starting state of the TM simulating the execution of @{text "n"}-th instruction
+  in the Abacus program.
+*}
+
+type_synonym layout = "nat list"
+
+text {*
+  @{text "length_of i"} is the length of the 
+  TM simulating the Abacus instruction @{text "i"}.
+*}
+fun length_of :: "abc_inst \<Rightarrow> nat"
+  where
+  "length_of i = (case i of 
+                    Inc n   \<Rightarrow> 2 * n + 9 |
+                    Dec n e \<Rightarrow> 2 * n + 16 |
+                    Goto n  \<Rightarrow> 1)"
+
+text {*
+  @{text "layout_of ap"} returns the layout of Abacus program @{text "ap"}.
+*}
+fun layout_of :: "abc_prog \<Rightarrow> layout"
+  where "layout_of ap = map length_of ap"
+
+
+text {*
+  @{text "start_of layout n"} looks out the starting state of @{text "n"}-th
+  TM in the finall TM.
+*}
+thm listsum_def
+
+fun start_of :: "nat list \<Rightarrow> nat \<Rightarrow> nat"
+  where
+  "start_of ly x = (Suc (listsum (take x ly))) "
+
+text {*
+  @{text "ci lo ss i"} complies Abacus instruction @{text "i"}
+  assuming the TM of @{text "i"} starts from state @{text "ss"} 
+  within the overal layout @{text "lo"}.
+*}
+
+fun ci :: "layout \<Rightarrow> nat \<Rightarrow> abc_inst \<Rightarrow> instr list"
+  where
+  "ci ly ss (Inc n) = tinc ss n"
+| "ci ly ss (Dec n e) = tdec ss n (start_of ly e)"
+| "ci ly ss (Goto n) = tgoto (start_of ly n)"
+
+text {*
+  @{text "tpairs_of ap"} transfroms Abacus program @{text "ap"} pairing
+  every instruction with its starting state.
+*}
+
+fun tpairs_of :: "abc_prog \<Rightarrow> (nat \<times> abc_inst) list"
+  where "tpairs_of ap = (zip (map (start_of (layout_of ap)) 
+                         [0..<(length ap)]) ap)"
+
+text {*
+  @{text "tms_of ap"} returns the list of TMs, where every one of them simulates
+  the corresponding Abacus intruction in @{text "ap"}.
+*}
+
+fun tms_of :: "abc_prog \<Rightarrow> (instr list) list"
+  where "tms_of ap = map (\<lambda> (n, tm). ci (layout_of ap) n tm) 
+                         (tpairs_of ap)"
+
+text {*
+  @{text "tm_of ap"} returns the final TM machine compiled from Abacus program @{text "ap"}.
+*}
+fun tm_of :: "abc_prog \<Rightarrow> instr list"
+  where "tm_of ap = concat (tms_of ap)"
+
+text {*
+  The following two functions specify the well-formedness of complied TM.
+*}
+(*
+fun t_ncorrect :: "tprog \<Rightarrow> bool"
+  where
+  "t_ncorrect tp = (length tp mod 2 = 0)"
+
+fun abc2t_correct :: "abc_prog \<Rightarrow> bool"
+  where 
+  "abc2t_correct ap = list_all (\<lambda> (n, tm). 
+             t_ncorrect (ci (layout_of ap) n tm)) (tpairs_of ap)"
+*)
+
+lemma length_findnth: 
+  "length (findnth n) = 4 * n"
+apply(induct n, auto)
+done
+
+lemma ci_length : "length (ci ns n ai) div 2 = length_of ai"
+apply(auto simp: ci.simps tinc_b_def tdec_b_def length_findnth
+                 split: abc_inst.splits)
+done
+
+subsection {*
+  Representation of Abacus memory by TM tape
+*}
+
+text {*
+  @{text "crsp acf tcf"} meams the abacus configuration @{text "acf"}
+  is corretly represented by the TM configuration @{text "tcf"}.
+*}
+
+fun crsp :: "layout \<Rightarrow> abc_conf \<Rightarrow> config \<Rightarrow> cell list \<Rightarrow> bool"
+  where 
+  "crsp ly (as, lm) (s, l, r) inres = 
+           (s = start_of ly as \<and> (\<exists> x. r = <lm> @ Bk\<up>x) \<and> 
+            l = Bk # Bk # inres)"
+
+declare crsp.simps[simp del]
+
+subsection {*
+  A more general definition of TM execution. 
+*}
+
+(*
+fun nnth_of :: "(taction \<times> nat) list \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> (taction \<times> nat)"
+  where
+  "nnth_of p s b = (if 2*s < length p 
+                    then (p ! (2*s + b)) else (Nop, 0))"
+
+thm nth_of.simps
+
+fun nfetch :: "tprog \<Rightarrow> nat \<Rightarrow> block \<Rightarrow> taction \<times> nat"
+  where
+  "nfetch p 0 b = (Nop, 0)" |
+  "nfetch p (Suc s) b = 
+             (case b of 
+                Bk \<Rightarrow> nnth_of p s 0 |
+                Oc \<Rightarrow> nnth_of p s 1)"
+*)
+
+                    
+text {*
+  The type of invarints expressing correspondence between 
+  Abacus configuration and TM configuration.
+*}
+
+type_synonym inc_inv_t = "abc_conf \<Rightarrow> config \<Rightarrow> cell list \<Rightarrow> bool"
+
+declare tms_of.simps[simp del] tm_of.simps[simp del]
+        layout_of.simps[simp del] abc_fetch.simps [simp del]  
+        tpairs_of.simps[simp del] start_of.simps[simp del]
+        ci.simps [simp del] length_of.simps[simp del] 
+        layout_of.simps[simp del]
+
+(*
+subsection {* The compilation of @{text "Inc n"} *}
+*)
+
+text {*
+  The lemmas in this section lead to the correctness of 
+  the compilation of @{text "Inc n"} instruction.
+*}
+
+declare abc_step_l.simps[simp del] abc_steps_l.simps[simp del]
+lemma [simp]: "start_of ly as > 0"
+apply(simp add: start_of.simps)
+done
+
+lemma abc_steps_l_0: "abc_steps_l ac ap 0 = ac"
+by(case_tac ac, simp add: abc_steps_l.simps)
+
+lemma abc_step_red: 
+ "abc_steps_l (as, am) ap stp = (bs, bm) \<Longrightarrow> 
+  abc_steps_l (as, am) ap (Suc stp) = abc_step_l (bs, bm) (abc_fetch bs ap) "
+proof(induct stp arbitrary: as am bs bm)
+  case 0
+  thus "?case"
+    by(simp add: abc_steps_l.simps abc_steps_l_0)
+next
+  case (Suc stp as am bs bm)
+  have ind: "\<And>as am bs bm. abc_steps_l (as, am) ap stp = (bs, bm) \<Longrightarrow> 
+    abc_steps_l (as, am) ap (Suc stp) = abc_step_l (bs, bm) (abc_fetch bs ap)"
+    by fact
+  have h:" abc_steps_l (as, am) ap (Suc stp) = (bs, bm)" by fact
+  obtain as' am' where g: "abc_step_l (as, am) (abc_fetch as ap) = (as', am')"
+    by(case_tac "abc_step_l (as, am) (abc_fetch as ap)", auto)
+  then have "abc_steps_l (as', am') ap (Suc stp) = abc_step_l (bs, bm) (abc_fetch bs ap)"
+    using h
+    by(rule_tac ind, simp add: abc_steps_l.simps)
+  thus "?case"
+    using g
+    by(simp add: abc_steps_l.simps)
+qed
+
+lemma tm_shift_fetch: 
+  "\<lbrakk>fetch A s b = (ac, ns); ns \<noteq> 0 \<rbrakk>
+  \<Longrightarrow> fetch (shift A off) s b = (ac, ns + off)"
+apply(case_tac b)
+apply(case_tac [!] s, auto simp: fetch.simps shift.simps)
+done
+
+lemma tm_shift_eq_step:
+  assumes exec: "step (s, l, r) (A, 0) = (s', l', r')"
+  and notfinal: "s' \<noteq> 0"
+  shows "step (s + off, l, r) (shift A off, off) = (s' + off, l', r')"
+using assms
+apply(simp add: step.simps)
+apply(case_tac "fetch A s (read r)", auto)
+apply(drule_tac [!] off = off in tm_shift_fetch, simp_all)
+done
+
+declare step.simps[simp del] steps.simps[simp del] shift.simps[simp del]
+
+lemma tm_shift_eq_steps: 
+  assumes exec: "steps (s, l, r) (A, 0) stp = (s', l', r')"
+  and notfinal: "s' \<noteq> 0"
+  shows "steps (s + off, l, r) (shift A off, off) stp = (s' + off, l', r')"
+  using exec notfinal
+proof(induct stp arbitrary: s' l' r', simp add: steps.simps)
+  fix stp s' l' r'
+  assume ind: "\<And>s' l' r'. \<lbrakk>steps (s, l, r) (A, 0) stp = (s', l', r'); s' \<noteq> 0\<rbrakk> 
+     \<Longrightarrow> steps (s + off, l, r) (shift A off, off) stp = (s' + off, l', r')"
+  and h: " steps (s, l, r) (A, 0) (Suc stp) = (s', l', r')" "s' \<noteq> 0"
+  obtain s1 l1 r1 where g: "steps (s, l, r) (A, 0) stp = (s1, l1, r1)" 
+    apply(case_tac "steps (s, l, r) (A, 0) stp") by blast
+  moreover then have "s1 \<noteq> 0"
+    using h
+    apply(simp add: step_red)
+    apply(case_tac "0 < s1", auto)
+    done
+  ultimately have "steps (s + off, l, r) (shift A off, off) stp =
+                   (s1 + off, l1, r1)"
+    apply(rule_tac ind, simp_all)
+    done
+  thus "steps (s + off, l, r) (shift A off, off) (Suc stp) = (s' + off, l', r')"
+    using h g assms
+    apply(simp add: step_red)
+    apply(rule_tac tm_shift_eq_step, auto)
+    done
+qed
+
+lemma startof_not0[simp]: "0 < start_of ly as"
+apply(simp add: start_of.simps)
+done
+
+lemma startof_ge1[simp]: "Suc 0 \<le> start_of ly as"
+apply(simp add: start_of.simps)
+done
+
+lemma start_of_Suc1: "\<lbrakk>ly = layout_of ap; 
+       abc_fetch as ap = Some (Inc n)\<rbrakk>
+       \<Longrightarrow> start_of ly (Suc as) = start_of ly as + 2 * n + 9"
+apply(auto simp: start_of.simps layout_of.simps  
+                 length_of.simps abc_fetch.simps 
+                 take_Suc_conv_app_nth split: if_splits)
+done
+
+lemma start_of_Suc2:
+  "\<lbrakk>ly = layout_of ap;
+  abc_fetch as ap = Some (Dec n e)\<rbrakk> \<Longrightarrow> 
+        start_of ly (Suc as) = 
+            start_of ly as + 2 * n + 16"
+apply(auto simp: start_of.simps layout_of.simps  
+                 length_of.simps abc_fetch.simps 
+                 take_Suc_conv_app_nth split: if_splits)
+done
+
+lemma start_of_Suc3:
+  "\<lbrakk>ly = layout_of ap;
+  abc_fetch as ap = Some (Goto n)\<rbrakk> \<Longrightarrow> 
+  start_of ly (Suc as) = start_of ly as + 1"
+apply(auto simp: start_of.simps layout_of.simps  
+                 length_of.simps abc_fetch.simps 
+                 take_Suc_conv_app_nth split: if_splits)
+done
+
+lemma length_ci_inc: 
+  "length (ci ly ss (Inc n)) = 4*n + 18"
+apply(auto simp: ci.simps length_findnth tinc_b_def)
+done
+
+lemma length_ci_dec: 
+  "length (ci ly ss (Dec n e)) = 4*n + 32"
+apply(auto simp: ci.simps length_findnth tdec_b_def)
+done
+
+lemma length_ci_goto: 
+  "length (ci ly ss (Goto n )) = 2"
+apply(auto simp: ci.simps length_findnth tdec_b_def)
+done
+
+lemma take_Suc_last[elim]: "Suc as \<le> length xs \<Longrightarrow> 
+            take (Suc as) xs = take as xs @ [xs ! as]"
+apply(induct xs arbitrary: as, simp, simp)
+apply(case_tac as, simp, simp)
+done
+
+lemma concat_suc: "Suc as \<le> length xs \<Longrightarrow> 
+       concat (take (Suc as) xs) = concat (take as xs) @ xs! as"
+apply(subgoal_tac "take (Suc as) xs = take as xs @ [xs ! as]", simp)
+by auto
+
+lemma concat_take_suc_iff: "Suc n \<le> length tps \<Longrightarrow> 
+       concat (take n tps) @ (tps ! n) = concat (take (Suc n) tps)"
+apply(drule_tac concat_suc, simp)
+done
+
+lemma concat_drop_suc_iff: 
+   "Suc n < length tps \<Longrightarrow> concat (drop (Suc n) tps) = 
+           tps ! Suc n @ concat (drop (Suc (Suc n)) tps)"
+apply(induct tps arbitrary: n, simp, simp)
+apply(case_tac tps, simp, simp)
+apply(case_tac n, simp, simp)
+done
+
+declare append_assoc[simp del]
+
+lemma  tm_append:
+  "\<lbrakk>n < length tps; tp = tps ! n\<rbrakk> \<Longrightarrow> 
+  \<exists> tp1 tp2. concat tps = tp1 @ tp @ tp2 \<and> tp1 = 
+  concat (take n tps) \<and> tp2 = concat (drop (Suc n) tps)"
+apply(rule_tac x = "concat (take n tps)" in exI)
+apply(rule_tac x = "concat (drop (Suc n) tps)" in exI)
+apply(auto)
+apply(induct n, simp)
+apply(case_tac tps, simp, simp, simp)
+apply(subgoal_tac "concat (take n tps) @ (tps ! n) = 
+               concat (take (Suc n) tps)")
+apply(simp only: append_assoc[THEN sym], simp only: append_assoc)
+apply(subgoal_tac " concat (drop (Suc n) tps) = tps ! Suc n @ 
+                  concat (drop (Suc (Suc n)) tps)", simp)
+apply(rule_tac concat_drop_suc_iff, simp)
+apply(rule_tac concat_take_suc_iff, simp)
+done
+
+declare append_assoc[simp]
+
+lemma map_of:  "n < length xs \<Longrightarrow> (map f xs) ! n = f (xs ! n)"
+by(auto)
+
+lemma [simp]: "length (tms_of aprog) = length aprog"
+apply(auto simp: tms_of.simps tpairs_of.simps)
+done
+
+lemma ci_nth: 
+  "\<lbrakk>ly = layout_of aprog; 
+  abc_fetch as aprog = Some ins\<rbrakk>
+  \<Longrightarrow> ci ly (start_of ly as) ins = tms_of aprog ! as"
+apply(simp add: tms_of.simps tpairs_of.simps 
+      abc_fetch.simps  map_of del: map_append split: if_splits)
+done
+
+lemma t_split:"\<lbrakk>
+        ly = layout_of aprog;
+        abc_fetch as aprog = Some ins\<rbrakk>
+      \<Longrightarrow> \<exists> tp1 tp2. concat (tms_of aprog) = 
+            tp1 @ (ci ly (start_of ly as) ins) @ tp2
+            \<and> tp1 = concat (take as (tms_of aprog)) \<and> 
+              tp2 = concat (drop (Suc as) (tms_of aprog))"
+apply(insert tm_append[of "as" "tms_of aprog" 
+                             "ci ly (start_of ly as) ins"], simp)
+apply(subgoal_tac "ci ly (start_of ly as) ins = (tms_of aprog) ! as")
+apply(subgoal_tac "length (tms_of aprog) = length aprog")
+apply(simp add: abc_fetch.simps split: if_splits, simp)
+apply(rule_tac ci_nth, auto)
+done
+
+lemma math_sub: "\<lbrakk>x >= Suc 0; x - 1 = z\<rbrakk> \<Longrightarrow> x + y - Suc 0 = z + y"
+by auto
+
+lemma start_more_one: "as \<noteq> 0 \<Longrightarrow> start_of ly as >= Suc 0"
+apply(induct as, simp add: start_of.simps)
+apply(case_tac as, auto simp: start_of.simps)
+done
+
+lemma div_apart: "\<lbrakk>x mod (2::nat) = 0; y mod 2 = 0\<rbrakk> 
+          \<Longrightarrow> (x + y) div 2 = x div 2 + y div 2"
+apply(drule mod_eqD)+
+apply(auto)
+done
+
+lemma div_apart_iff: "\<lbrakk>x mod (2::nat) = 0; y mod 2 = 0\<rbrakk> \<Longrightarrow> 
+           (x + y) mod 2 = 0"
+apply(auto)
+done
+
+lemma [simp]: "length (layout_of aprog) = length aprog"
+apply(auto simp: layout_of.simps)
+done
+
+lemma start_of_ind: "\<lbrakk>as < length aprog; ly = layout_of aprog\<rbrakk> \<Longrightarrow> 
+       start_of ly (Suc as) = start_of ly as + 
+                          length ((tms_of aprog) ! as) div 2"
+apply(simp only: start_of.simps, simp)
+apply(auto simp: start_of.simps tms_of.simps layout_of.simps 
+                 tpairs_of.simps)
+apply(simp add: ci_length take_Suc take_Suc_conv_app_nth)
+done
+
+lemma concat_take_suc: "Suc n \<le> length xs \<Longrightarrow>
+  concat (take (Suc n) xs) = concat (take n xs) @ (xs ! n)"
+apply(subgoal_tac "take (Suc n) xs =
+                   take n xs @ [xs ! n]")
+apply(auto)
+done
+
+lemma [simp]: 
+  "\<lbrakk>as < length aprog; (abc_fetch as aprog) = Some ins\<rbrakk>
+  \<Longrightarrow> ci (layout_of aprog) 
+  (start_of (layout_of aprog) as) (ins) \<in> set (tms_of aprog)"
+apply(insert ci_nth[of "layout_of aprog" aprog as], simp)
+done
+
+lemma [simp]: "length (tms_of ap) = length ap"
+by(auto simp: tms_of.simps tpairs_of.simps)
+
+lemma [intro]:  "n < length ap \<Longrightarrow> length (tms_of ap ! n) mod 2 = 0"
+apply(auto simp: tms_of.simps tpairs_of.simps)
+apply(case_tac "ap ! n", auto simp: ci.simps length_findnth tinc_b_def tdec_b_def)
+apply arith
+by arith
+
+lemma compile_mod2: "length (concat (take n (tms_of ap))) mod 2 = 0"
+apply(induct n, auto)
+apply(case_tac "n < length (tms_of ap)", simp add: take_Suc_conv_app_nth, auto)
+apply(subgoal_tac "length (tms_of ap ! n) mod 2 = 0")
+apply arith
+by auto
+
+lemma tpa_states:
+  "\<lbrakk>tp = concat (take as (tms_of ap));
+  as \<le> length ap\<rbrakk> \<Longrightarrow> 
+  start_of (layout_of ap) as = Suc (length tp div 2)"
+proof(induct as arbitrary: tp)
+  case 0
+  thus "?case"
+    by(simp add: start_of.simps)
+next
+  case (Suc as tp)
+  have ind: "\<And>tp. \<lbrakk>tp = concat (take as (tms_of ap)); as \<le> length ap\<rbrakk> \<Longrightarrow>
+    start_of (layout_of ap) as = Suc (length tp div 2)" by fact
+  have tp: "tp = concat (take (Suc as) (tms_of ap))" by fact
+  have le: "Suc as \<le> length ap" by fact
+  have a: "start_of (layout_of ap) as = Suc (length (concat (take as (tms_of ap))) div 2)"
+    using le
+    by(rule_tac ind, simp_all)
+  from a tp le show "?case"
+    apply(simp add: start_of.simps take_Suc_conv_app_nth)
+    apply(subgoal_tac "length (concat (take as (tms_of ap))) mod 2= 0")
+    apply(subgoal_tac " length (tms_of ap ! as) mod 2 = 0")
+    apply(simp add: Abacus.div_apart) 
+    apply(simp add: layout_of.simps ci_length  tms_of.simps tpairs_of.simps)
+    apply(auto  intro: compile_mod2)
+    done
+qed
+
+lemma append_append_fetch: 
+    "\<lbrakk>length tp1 mod 2 = 0; length tp mod 2 = 0;
+      length tp1 div 2 < a \<and> a \<le> length tp1 div 2 + length tp div 2\<rbrakk>
+    \<Longrightarrow>fetch (tp1 @ tp @ tp2) a b = fetch tp (a - length tp1 div 2) b "
+apply(subgoal_tac "\<exists> x. a = length tp1 div 2 + x", erule exE, simp)
+apply(case_tac x, simp)
+apply(subgoal_tac "length tp1 div 2 + Suc nat = 
+             Suc (length tp1 div 2 + nat)")
+apply(simp only: fetch.simps nth_of.simps, auto)
+apply(case_tac b, simp)
+apply(subgoal_tac "2 * (length tp1 div 2) = length tp1", simp)
+apply(subgoal_tac "2 * nat < length tp", simp add: nth_append, simp)
+apply(subgoal_tac "2 * (length tp1 div 2) = length tp1", simp)
+apply(subgoal_tac "2 * nat < length tp", simp add: nth_append, auto)
+apply(auto simp: nth_append)
+apply(rule_tac x = "a - length tp1 div 2" in exI, simp)
+done
+
+lemma step_eq_fetch':
+  assumes layout: "ly = layout_of ap"
+  and compile: "tp = tm_of ap"
+  and fetch: "abc_fetch as ap = Some ins"
+  and range1: "s \<ge> start_of ly as"
+  and range2: "s < start_of ly (Suc as)"
+  shows "fetch tp s b = fetch (ci ly (start_of ly as) ins)
+       (Suc s - start_of ly as) b "
+proof -
+  have "\<exists>tp1 tp2. concat (tms_of ap) = tp1 @ ci ly (start_of ly as) ins @ tp2 \<and>
+    tp1 = concat (take as (tms_of ap)) \<and> tp2 = concat (drop (Suc as) (tms_of ap))"
+    using assms
+    by(rule_tac t_split, simp_all)
+  then obtain tp1 tp2 where a: "concat (tms_of ap) = tp1 @ ci ly (start_of ly as) ins @ tp2 \<and>
+    tp1 = concat (take as (tms_of ap)) \<and> tp2 = concat (drop (Suc as) (tms_of ap))" by blast
+  then have b: "start_of (layout_of ap) as = Suc (length tp1 div 2)"
+    using fetch
+    apply(rule_tac tpa_states, simp, simp add: abc_fetch.simps split: if_splits)
+    done
+  have "fetch (tp1 @ (ci ly (start_of ly as) ins) @ tp2)  s b = 
+        fetch (ci ly (start_of ly as) ins) (s - length tp1 div 2) b"
+  proof(rule_tac append_append_fetch)
+    show "length tp1 mod 2 = 0"
+      using a
+      by(auto, rule_tac compile_mod2)
+  next
+    show "length (ci ly (start_of ly as) ins) mod 2 = 0"
+      apply(case_tac ins, auto simp: ci.simps length_findnth tinc_b_def tdec_b_def)
+      by(arith, arith)
+  next
+    show "length tp1 div 2 < s \<and> s \<le> 
+      length tp1 div 2 + length (ci ly (start_of ly as) ins) div 2"
+    proof -
+      have "length (ci ly (start_of ly as) ins) div 2 = length_of ins"
+        using ci_length by simp
+      moreover have "start_of ly (Suc as) = start_of ly as + length_of ins"
+        using fetch layout
+        apply(simp add: start_of.simps abc_fetch.simps List.take_Suc_conv_app_nth 
+          split: if_splits)
+        apply(simp add: layout_of.simps)
+        done
+      ultimately show "?thesis"
+        using b layout range1 range2
+        apply(simp)
+        done
+    qed
+  qed
+  thus "?thesis"
+    using b layout a compile  
+    apply(simp add: tm_of.simps)
+    done
+qed
+
+lemma step_eq_fetch: 
+  assumes layout: "ly = layout_of ap"
+  and compile: "tp = tm_of ap"
+  and abc_fetch: "abc_fetch as ap = Some ins" 
+  and fetch: "fetch (ci ly (start_of ly as) ins)
+       (Suc s - start_of ly as) b = (ac, ns)"
+  and notfinal: "ns \<noteq> 0"
+  shows "fetch tp s b = (ac, ns)"
+proof -
+  have "s \<ge> start_of ly as"
+  proof(cases "s \<ge> start_of ly as")
+    case True thus "?thesis" by simp
+  next
+    case False 
+    have "\<not> start_of ly as \<le> s" by fact
+    then have "Suc s - start_of ly as = 0"
+      by arith
+    then have "fetch (ci ly (start_of ly as) ins)
+       (Suc s - start_of ly as) b = (Nop, 0)"
+      by(simp add: fetch.simps)
+    with notfinal fetch show "?thesis"
+      by(simp)
+  qed
+  moreover have "s < start_of ly (Suc as)"
+  proof(cases "s < start_of ly (Suc as)")
+    case True thus "?thesis" by simp
+  next
+    case False
+    have h: "\<not> s < start_of ly (Suc as)"
+      by fact
+    then have "s > start_of ly as"
+      using abc_fetch layout
+      apply(simp add: start_of.simps abc_fetch.simps split: if_splits)
+      apply(simp add: List.take_Suc_conv_app_nth, auto)
+      apply(subgoal_tac "layout_of ap ! as > 0") 
+      apply arith
+      apply(simp add: layout_of.simps)
+      apply(case_tac "ap!as", auto simp: length_of.simps)
+      done
+    from this and h have "fetch (ci ly (start_of ly as) ins) (Suc s - start_of ly as) b = (Nop, 0)"
+      using abc_fetch layout
+      apply(case_tac b, simp_all add: Suc_diff_le)
+      apply(case_tac [!] ins, simp_all add: start_of_Suc2 start_of_Suc1 start_of_Suc3)
+      apply(simp_all only: length_ci_inc length_ci_dec length_ci_goto, auto)
+      using layout
+      apply(subgoal_tac [!] "start_of ly (Suc as) = start_of ly as + 2*nat1 + 16", simp_all)
+      apply(rule_tac [!] start_of_Suc2, auto)
+      done
+    from fetch and notfinal this show "?thesis"by simp
+  qed
+  ultimately show "?thesis"
+    using assms
+    apply(drule_tac b= b and ins = ins in step_eq_fetch', auto)
+    done
+qed
+
+
+lemma step_eq_in:
+  assumes layout: "ly = layout_of ap"
+  and compile: "tp = tm_of ap"
+  and fetch: "abc_fetch as ap = Some ins"    
+  and exec: "step (s, l, r) (ci ly (start_of ly as) ins, start_of ly as - 1) 
+  = (s', l', r')"
+  and notfinal: "s' \<noteq> 0"
+  shows "step (s, l, r) (tp, 0) = (s', l', r')"
+  using assms
+  apply(simp add: step.simps)
+  apply(case_tac "fetch (ci (layout_of ap) (start_of (layout_of ap) as) ins)
+    (Suc s - start_of (layout_of ap) as) (read r)", simp)
+  using layout
+  apply(drule_tac s = s and b = "read r" and ac = a in step_eq_fetch, auto)
+  done
+
+lemma steps_eq_in:
+  assumes layout: "ly = layout_of ap"
+  and compile: "tp = tm_of ap"
+  and crsp: "crsp ly (as, lm) (s, l, r) ires"
+  and fetch: "abc_fetch as ap = Some ins"    
+  and exec: "steps (s, l, r) (ci ly (start_of ly as) ins, start_of ly as - 1) stp 
+  = (s', l', r')"
+  and notfinal: "s' \<noteq> 0"
+  shows "steps (s, l, r) (tp, 0) stp = (s', l', r')"
+  using exec notfinal
+proof(induct stp arbitrary: s' l' r', simp add: steps.simps)
+  fix stp s' l' r'
+  assume ind: 
+    "\<And>s' l' r'. \<lbrakk>steps (s, l, r) (ci ly (start_of ly as) ins, start_of ly as - 1) stp = (s', l', r'); s' \<noteq> 0\<rbrakk>
+              \<Longrightarrow> steps (s, l, r) (tp, 0) stp = (s', l', r')"
+  and h: "steps (s, l, r) (ci ly (start_of ly as) ins, start_of ly as - 1) (Suc stp) = (s', l', r')" "s' \<noteq> 0"
+  obtain s1 l1 r1 where g: "steps (s, l, r) (ci ly (start_of ly as) ins, start_of ly as - 1) stp = 
+                        (s1, l1, r1)"
+    apply(case_tac "steps (s, l, r) (ci ly (start_of ly as) ins, start_of ly as - 1) stp") by blast
+  moreover hence "s1 \<noteq> 0"
+    using h
+    apply(simp add: step_red)
+    apply(case_tac "0 < s1", simp_all)
+    done
+  ultimately have "steps (s, l, r) (tp, 0) stp = (s1, l1, r1)"
+    apply(rule_tac ind, auto)
+    done
+  thus "steps (s, l, r) (tp, 0) (Suc stp) = (s', l', r')"
+    using h g assms
+    apply(simp add: step_red)
+    apply(rule_tac step_eq_in, auto)
+    done
+qed
+
+lemma tm_append_fetch_first: 
+  "\<lbrakk>fetch A s b = (ac, ns); ns \<noteq> 0\<rbrakk> \<Longrightarrow> 
+    fetch (A @ B) s b = (ac, ns)"
+apply(case_tac b)
+apply(case_tac [!] s, auto simp: fetch.simps nth_append split: if_splits)
+done
+
+lemma tm_append_first_step_eq: 
+  assumes "step (s, l, r) (A, off) = (s', l', r')"
+  and "s' \<noteq> 0"
+  shows "step (s, l, r) (A @ B, off) = (s', l', r')"
+using assms
+apply(simp add: step.simps)
+apply(case_tac "fetch A (s - off) (read r)")
+apply(frule_tac  B = B and b = "read r" in tm_append_fetch_first, auto)
+done
+
+lemma tm_append_first_steps_eq: 
+  assumes "steps (s, l, r) (A, off) stp = (s', l', r')"
+  and "s' \<noteq> 0"
+  shows "steps (s, l, r) (A @ B, off) stp = (s', l', r')"
+using assms
+proof(induct stp arbitrary: s' l' r', simp add: steps.simps)
+  fix stp s' l' r'
+  assume ind: "\<And>s' l' r'. \<lbrakk>steps (s, l, r) (A, off) stp = (s', l', r'); s' \<noteq> 0\<rbrakk>
+    \<Longrightarrow> steps (s, l, r) (A @ B, off) stp = (s', l', r')"
+    and h: "steps (s, l, r) (A, off) (Suc stp) = (s', l', r')" "s' \<noteq> 0"
+  obtain sa la ra where a: "steps (s, l, r) (A, off) stp = (sa, la, ra)"
+    apply(case_tac "steps (s, l, r) (A, off) stp") by blast
+  hence "steps (s, l, r) (A @ B, off) stp = (sa, la, ra) \<and> sa \<noteq> 0"
+    using h ind[of sa la ra]
+    apply(case_tac sa, simp_all)
+    done
+  thus "steps (s, l, r) (A @ B, off) (Suc stp) = (s', l', r')"
+    using h a
+    apply(simp add: step_red)
+    apply(rule_tac tm_append_first_step_eq, simp_all)
+    done
+qed
+
+lemma tm_append_second_fetch_eq:
+  assumes
+  even: "length A mod 2 = 0"
+  and off: "off = length A div 2"
+  and fetch: "fetch B s b = (ac, ns)"
+  and notfinal: "ns \<noteq> 0"
+  shows "fetch (A @ shift B off) (s + off) b = (ac, ns + off)"
+using assms
+apply(case_tac b)
+apply(case_tac [!] s, auto simp: fetch.simps nth_append shift.simps 
+  split: if_splits)
+done
+
+
+lemma tm_append_second_step_eq: 
+  assumes 
+  exec: "step0 (s, l, r) B = (s', l', r')"
+  and notfinal: "s' \<noteq> 0"
+  and off: "off = length A div 2"
+  and even: "length A mod 2 = 0"
+  shows "step0 (s + off, l, r) (A @ shift B off) = (s' + off, l', r')"
+using assms
+apply(simp add: step.simps)
+apply(case_tac "fetch B s (read r)")
+apply(frule_tac tm_append_second_fetch_eq, simp_all, auto)
+done
+
+
+lemma tm_append_second_steps_eq: 
+  assumes 
+  exec: "steps (s, l, r) (B, 0) stp = (s', l', r')"
+  and notfinal: "s' \<noteq> 0"
+  and off: "off = length A div 2"
+  and even: "length A mod 2 = 0"
+  shows "steps (s + off, l, r) (A @ shift B off, 0) stp = (s' + off, l', r')"
+using exec notfinal
+proof(induct stp arbitrary: s' l' r')
+  case 0
+  thus "steps0 (s + off, l, r) (A @ shift B off) 0 = (s' + off, l', r')"
+    by(simp add: steps.simps)
+next
+  case (Suc stp s' l' r')
+  have ind: "\<And>s' l' r'. \<lbrakk>steps0 (s, l, r) B stp = (s', l', r'); s' \<noteq> 0\<rbrakk> \<Longrightarrow> 
+    steps0 (s + off, l, r) (A @ shift B off) stp = (s' + off, l', r')"
+    by fact
+  have h: "steps0 (s, l, r) B (Suc stp) = (s', l', r')" by fact
+  have k: "s' \<noteq> 0" by fact
+  obtain s'' l'' r'' where a: "steps0 (s, l, r) B stp = (s'', l'', r'')"
+    by (metis prod_cases3)
+  then have b: "s'' \<noteq> 0"
+    using h k
+    by(rule_tac notI, auto simp: step_red)
+  from a b have c: "steps0 (s + off, l, r) (A @ shift B off) stp = (s'' + off, l'', r'')"
+    by(erule_tac ind, simp)
+  from c b h a k assms show "?case"
+    thm tm_append_second_step_eq
+    apply(simp add: step_red) by(rule tm_append_second_step_eq, simp_all)
+qed
+
+lemma tm_append_second_fetch0_eq:
+  assumes
+  even: "length A mod 2 = 0"
+  and off: "off = length A div 2"
+  and fetch: "fetch B s b = (ac, 0)"
+  and notfinal: "s \<noteq> 0"
+  shows "fetch (A @ shift B off) (s + off) b = (ac, 0)"
+using assms
+apply(case_tac b)
+apply(case_tac [!] s, auto simp: fetch.simps nth_append shift.simps 
+  split: if_splits)
+done
+
+lemma tm_append_second_halt_eq:
+  assumes 
+  exec: "steps (Suc 0, l, r) (B, 0) stp = (0, l', r')"
+  and wf_B: "tm_wf (B, 0)"
+  and off: "off = length A div 2"
+  and even: "length A mod 2 = 0"
+  shows "steps (Suc off, l, r) (A @ shift B off, 0) stp = (0, l', r')"
+proof -
+  thm before_final
+  have "\<exists>n. \<not> is_final (steps0 (1, l, r) B n) \<and> steps0 (1, l, r) B (Suc n) = (0, l', r')"
+    using exec by(rule_tac before_final, simp)
+ then obtain n where a: 
+   "\<not> is_final (steps0 (1, l, r) B n) \<and> steps0 (1, l, r) B (Suc n) = (0, l', r')" ..
+ obtain s'' l'' r'' where b: "steps0 (1, l, r) B n = (s'', l'', r'') \<and> s'' >0"
+   using a
+   by(case_tac "steps0 (1, l, r) B n", auto)
+ have c: "steps (Suc 0 + off, l, r) (A @ shift B off, 0) n = (s'' + off, l'', r'')"
+   using a b assms
+   by(rule_tac tm_append_second_steps_eq, simp_all)
+ obtain ac where d: "fetch B s'' (read r'') = (ac, 0)"
+   using  b a
+   by(case_tac "fetch B s'' (read r'')", auto simp: step_red step.simps)
+ then have "fetch (A @ shift B off) (s'' + off) (read r'') = (ac, 0)"
+   using assms b
+   by(rule_tac tm_append_second_fetch0_eq, simp_all)
+ then have e: "steps (Suc 0 + off, l, r) (A @ shift B off, 0) (Suc n) = (0, l', r')"
+   using a b assms c d
+   by(simp add: step_red step.simps)
+ from a have "n < stp"
+   using exec
+ proof(cases "n < stp")
+   case  True thus "?thesis" by simp
+ next
+   case False
+   have "\<not> n < stp" by fact
+   then obtain d where  "n = stp + d"
+     by (metis add.comm_neutral less_imp_add_positive nat_neq_iff)
+   thus "?thesis"
+     using a e exec
+     by(simp add: steps_add)
+ qed
+ then obtain d where "stp = Suc n + d"
+   by(metis add_Suc less_iff_Suc_add)
+ thus "?thesis"
+   using e
+   by(simp only: steps_add, simp)
+qed
+
+lemma tm_append_steps: 
+  assumes 
+  aexec: "steps (s, l, r) (A, 0) stpa = (Suc (length A div 2), la, ra)"
+  and bexec: "steps (Suc 0, la, ra) (B, 0) stpb =  (sb, lb, rb)"
+  and notfinal: "sb \<noteq> 0"
+  and off: "off = length A div 2"
+  and even: "length A mod 2 = 0"
+  shows "steps (s, l, r) (A @ shift B off, 0) (stpa + stpb) = (sb + off, lb, rb)"
+proof -
+  have "steps (s, l, r) (A@shift B off, 0) stpa = (Suc (length A div 2), la, ra)"
+    apply(rule_tac tm_append_first_steps_eq)
+    apply(auto simp: assms)
+    done
+  moreover have "steps (1 + off, la, ra) (A @ shift B off, 0) stpb = (sb + off, lb, rb)"
+    apply(rule_tac tm_append_second_steps_eq)
+    apply(auto simp: assms bexec)
+    done
+  ultimately show "steps (s, l, r) (A @ shift B off, 0) (stpa + stpb) = (sb + off, lb, rb)"
+    apply(simp add: steps_add off)
+    done
+qed
+       
+subsection {* Crsp of Inc*}
+
+fun at_begin_fst_bwtn :: "inc_inv_t"
+  where
+  "at_begin_fst_bwtn (as, lm) (s, l, r) ires = 
+      (\<exists> lm1 tn rn. lm1 = (lm @ 0\<up>tn) \<and> length lm1 = s \<and> 
+          (if lm1 = [] then l = Bk # Bk # ires
+           else l = [Bk]@<rev lm1>@Bk#Bk#ires) \<and> r = Bk\<up>rn)" 
+
+
+fun at_begin_fst_awtn :: "inc_inv_t"
+  where
+  "at_begin_fst_awtn (as, lm) (s, l, r) ires = 
+      (\<exists> lm1 tn rn. lm1 = (lm @ 0\<up>tn) \<and> length lm1 = s \<and>
+         (if lm1 = []  then l = Bk # Bk # ires
+          else l = [Bk]@<rev lm1>@Bk#Bk#ires) \<and> r = [Oc]@Bk\<up>rn)"
+
+fun at_begin_norm :: "inc_inv_t"
+  where
+  "at_begin_norm (as, lm) (s, l, r) ires= 
+      (\<exists> lm1 lm2 rn. lm = lm1 @ lm2 \<and> length lm1 = s \<and> 
+        (if lm1 = [] then l = Bk # Bk # ires
+         else l = Bk # <rev lm1> @ Bk # Bk # ires ) \<and> r = <lm2>@Bk\<up>rn)"
+
+fun in_middle :: "inc_inv_t"
+  where
+  "in_middle (as, lm) (s, l, r) ires = 
+      (\<exists> lm1 lm2 tn m ml mr rn. lm @ 0\<up>tn = lm1 @ [m] @ lm2
+       \<and> length lm1 = s \<and> m + 1 = ml + mr \<and>  
+         ml \<noteq> 0 \<and> tn = s + 1 - length lm \<and> 
+       (if lm1 = [] then l = Oc\<up>ml @ Bk # Bk # ires 
+        else l = Oc\<up>ml@[Bk]@<rev lm1>@
+                 Bk # Bk # ires) \<and> (r = Oc\<up>mr @ [Bk] @ <lm2>@ Bk\<up>rn \<or> 
+      (lm2 = [] \<and> r = Oc\<up>mr))
+      )"
+
+fun inv_locate_a :: "inc_inv_t"
+  where "inv_locate_a (as, lm) (s, l, r) ires = 
+     (at_begin_norm (as, lm) (s, l, r) ires \<or>
+      at_begin_fst_bwtn (as, lm) (s, l, r) ires \<or>
+      at_begin_fst_awtn (as, lm) (s, l, r) ires
+      )"
+
+fun inv_locate_b :: "inc_inv_t"
+  where "inv_locate_b (as, lm) (s, l, r) ires = 
+        (in_middle (as, lm) (s, l, r)) ires "
+
+fun inv_after_write :: "inc_inv_t"
+  where "inv_after_write (as, lm) (s, l, r) ires = 
+           (\<exists> rn m lm1 lm2. lm = lm1 @ m # lm2 \<and>
+             (if lm1 = [] then l = Oc\<up>m @ Bk # Bk # ires
+              else Oc # l = Oc\<up>Suc m@ Bk # <rev lm1> @ 
+                      Bk # Bk # ires) \<and> r = [Oc] @ <lm2> @ Bk\<up>rn)"
+
+fun inv_after_move :: "inc_inv_t"
+  where "inv_after_move (as, lm) (s, l, r) ires = 
+      (\<exists> rn m lm1 lm2. lm = lm1 @ m # lm2 \<and>
+        (if lm1 = [] then l = Oc\<up>Suc m @ Bk # Bk # ires
+         else l = Oc\<up>Suc m@ Bk # <rev lm1> @ Bk # Bk # ires) \<and> 
+        r = <lm2> @ Bk\<up>rn)"
+
+fun inv_after_clear :: "inc_inv_t"
+  where "inv_after_clear (as, lm) (s, l, r) ires =
+       (\<exists> rn m lm1 lm2 r'. lm = lm1 @ m # lm2 \<and> 
+        (if lm1 = [] then l = Oc\<up>Suc m @ Bk # Bk # ires
+         else l = Oc\<up>Suc m @ Bk # <rev lm1> @ Bk # Bk # ires) \<and> 
+          r = Bk # r' \<and> Oc # r' = <lm2> @ Bk\<up>rn)"
+
+fun inv_on_right_moving :: "inc_inv_t"
+  where "inv_on_right_moving (as, lm) (s, l, r) ires = 
+       (\<exists> lm1 lm2 m ml mr rn. lm = lm1 @ [m] @ lm2 \<and> 
+            ml + mr = m \<and> 
+          (if lm1 = [] then l = Oc\<up>ml @ Bk # Bk # ires
+          else l = Oc\<up>ml  @ [Bk] @ <rev lm1> @ Bk # Bk # ires) \<and> 
+         ((r = Oc\<up>mr @ [Bk] @ <lm2> @ Bk\<up>rn) \<or> 
+          (r = Oc\<up>mr \<and> lm2 = [])))"
+
+fun inv_on_left_moving_norm :: "inc_inv_t"
+  where "inv_on_left_moving_norm (as, lm) (s, l, r) ires =
+      (\<exists> lm1 lm2 m ml mr rn. lm = lm1 @ [m] @ lm2 \<and>  
+             ml + mr = Suc m \<and> mr > 0 \<and> (if lm1 = [] then l = Oc\<up>ml @ Bk # Bk # ires
+                                         else l =  Oc\<up>ml @ Bk # <rev lm1> @ Bk # Bk # ires)
+        \<and> (r = Oc\<up>mr @ Bk # <lm2> @ Bk\<up>rn \<or> 
+           (lm2 = [] \<and> r = Oc\<up>mr)))"
+
+fun inv_on_left_moving_in_middle_B:: "inc_inv_t"
+  where "inv_on_left_moving_in_middle_B (as, lm) (s, l, r) ires =
+                (\<exists> lm1 lm2 rn. lm = lm1 @ lm2 \<and>  
+                     (if lm1 = [] then l = Bk # ires
+                      else l = <rev lm1> @ Bk # Bk # ires) \<and> 
+                      r = Bk # <lm2> @ Bk\<up>rn)"
+
+fun inv_on_left_moving :: "inc_inv_t"
+  where "inv_on_left_moving (as, lm) (s, l, r) ires = 
+       (inv_on_left_moving_norm  (as, lm) (s, l, r) ires \<or>
+        inv_on_left_moving_in_middle_B (as, lm) (s, l, r) ires)"
+
+
+fun inv_check_left_moving_on_leftmost :: "inc_inv_t"
+  where "inv_check_left_moving_on_leftmost (as, lm) (s, l, r) ires = 
+                (\<exists> rn. l = ires \<and> r = [Bk, Bk] @ <lm> @  Bk\<up>rn)"
+
+fun inv_check_left_moving_in_middle :: "inc_inv_t"
+  where "inv_check_left_moving_in_middle (as, lm) (s, l, r) ires = 
+              (\<exists> lm1 lm2 r' rn. lm = lm1 @ lm2 \<and>
+                 (Oc # l = <rev lm1> @ Bk # Bk # ires) \<and> r = Oc # Bk # r' \<and> 
+                           r' = <lm2> @  Bk\<up>rn)"
+
+fun inv_check_left_moving :: "inc_inv_t"
+  where "inv_check_left_moving (as, lm) (s, l, r) ires = 
+             (inv_check_left_moving_on_leftmost (as, lm) (s, l, r) ires \<or>
+             inv_check_left_moving_in_middle (as, lm) (s, l, r) ires)"
+
+fun inv_after_left_moving :: "inc_inv_t"
+  where "inv_after_left_moving (as, lm) (s, l, r) ires= 
+              (\<exists> rn. l = Bk # ires \<and> r = Bk # <lm> @  Bk\<up>rn)"
+
+fun inv_stop :: "inc_inv_t"
+  where "inv_stop (as, lm) (s, l, r) ires= 
+              (\<exists> rn. l = Bk # Bk # ires \<and> r = <lm> @  Bk\<up>rn)"
+
+
+lemma halt_lemma2': 
+  "\<lbrakk>wf LE;  \<forall> n. ((\<not> P (f n) \<and> Q (f n)) \<longrightarrow> 
+    (Q (f (Suc n)) \<and> (f (Suc n), (f n)) \<in> LE)); Q (f 0)\<rbrakk> 
+      \<Longrightarrow> \<exists> n. P (f n)"
+apply(intro exCI, simp)
+apply(subgoal_tac "\<forall> n. Q (f n)", simp)
+apply(drule_tac f = f in wf_inv_image)
+apply(simp add: inv_image_def)
+apply(erule wf_induct, simp)
+apply(erule_tac x = x in allE)
+apply(erule_tac x = n in allE, erule_tac x = n in allE)
+apply(erule_tac x = "Suc x" in allE, simp)
+apply(rule_tac allI)
+apply(induct_tac n, simp)
+apply(erule_tac x = na in allE, simp)
+done
+
+lemma halt_lemma2'': 
+  "\<lbrakk>P (f n); \<not> P (f (0::nat))\<rbrakk> \<Longrightarrow> 
+         \<exists> n. (P (f n) \<and> (\<forall> i < n. \<not> P (f i)))"
+apply(induct n rule: nat_less_induct, auto)
+done
+
+lemma halt_lemma2''':
+ "\<lbrakk>\<forall>n. \<not> P (f n) \<and> Q (f n) \<longrightarrow> Q (f (Suc n)) \<and> (f (Suc n), f n) \<in> LE;
+                 Q (f 0);  \<forall>i<na. \<not> P (f i)\<rbrakk> \<Longrightarrow> Q (f na)"
+apply(induct na, simp, simp)
+done
+
+lemma halt_lemma2: 
+  "\<lbrakk>wf LE;  
+    Q (f 0); \<not> P (f 0);
+    \<forall> n. ((\<not> P (f n) \<and> Q (f n)) \<longrightarrow> (Q (f (Suc n)) \<and> (f (Suc n), (f n)) \<in> LE))\<rbrakk> 
+  \<Longrightarrow> \<exists> n. P (f n) \<and> Q (f n)"
+apply(insert halt_lemma2' [of LE P f Q], simp, erule_tac exE)
+apply(subgoal_tac "\<exists> n. (P (f n) \<and> (\<forall> i < n. \<not> P (f i)))")
+apply(erule_tac exE)+
+apply(rule_tac x = na in exI, auto)
+apply(rule halt_lemma2''', simp, simp, simp)
+apply(erule_tac halt_lemma2'', simp)
+done
+
+
+fun findnth_inv :: "layout \<Rightarrow> nat \<Rightarrow> inc_inv_t"
+  where
+  "findnth_inv ly n (as, lm) (s, l, r) ires =
+              (if s = 0 then False
+               else if s \<le> Suc (2*n) then 
+                  if s mod 2 = 1 then inv_locate_a (as, lm) ((s - 1) div 2, l, r) ires
+                  else inv_locate_b (as, lm) ((s - 1) div 2, l, r) ires
+               else False)"
+
+
+fun findnth_state :: "config \<Rightarrow> nat \<Rightarrow> nat"
+  where
+  "findnth_state (s, l, r) n = (Suc (2*n) - s)"
+  
+fun findnth_step :: "config \<Rightarrow> nat \<Rightarrow> nat"
+  where
+  "findnth_step (s, l, r) n = 
+           (if s mod 2 = 1 then
+                   (if (r \<noteq> [] \<and> hd r = Oc) then 0
+                    else 1)
+            else length r)"
+
+fun findnth_measure :: "config \<times> nat \<Rightarrow> nat \<times> nat"
+  where
+  "findnth_measure (c, n) = 
+     (findnth_state c n, findnth_step c n)"
+
+definition lex_pair :: "((nat \<times> nat) \<times> nat \<times> nat) set"
+  where
+  "lex_pair \<equiv> less_than <*lex*> less_than"
+
+definition findnth_LE :: "((config \<times> nat) \<times> (config \<times> nat)) set"
+  where
+   "findnth_LE \<equiv> (inv_image lex_pair findnth_measure)"
+
+lemma wf_findnth_LE: "wf findnth_LE"
+by(auto intro:wf_inv_image simp: findnth_LE_def lex_pair_def)
+
+declare findnth_inv.simps[simp del]
+
+lemma [simp]: 
+  "\<lbrakk>x < Suc (Suc (2 * n)); Suc x mod 2 = Suc 0; \<not> x < 2 * n\<rbrakk>
+ \<Longrightarrow> x = 2*n"
+by arith
+
+lemma [simp]: 
+  "\<lbrakk>0 < a; a < Suc (2 * n); a mod 2 = Suc 0\<rbrakk> 
+      \<Longrightarrow> fetch (findnth n) a Bk = (W1, a)"
+apply(case_tac a, simp_all)
+apply(induct n, auto simp: findnth.simps length_findnth nth_append)
+apply arith
+done
+
+lemma [simp]: 
+  "\<lbrakk>0 < a; a < Suc (2 * n); a mod 2 = Suc 0\<rbrakk> 
+      \<Longrightarrow> fetch (findnth n) a Oc = (R, Suc a)"
+apply(case_tac a, simp_all)
+apply(induct n, auto simp: findnth.simps length_findnth nth_append)
+apply(subgoal_tac "nat = 2 * n", simp)
+by arith
+
+lemma [simp]: 
+  "\<lbrakk>0 < a; a < Suc (2*n); a mod 2 \<noteq> Suc 0\<rbrakk>
+     \<Longrightarrow> fetch (findnth n) a Oc = (R, a)"
+apply(case_tac a, simp_all)
+apply(induct n, auto simp: findnth.simps length_findnth nth_append)
+apply(subgoal_tac "nat = Suc (2 * n)", simp)
+apply arith
+done
+
+lemma [simp]: 
+  "\<lbrakk>0 < a; a < Suc (2*n); a mod 2 \<noteq> Suc 0\<rbrakk>
+     \<Longrightarrow> fetch (findnth n) a Bk = (R, Suc a)"
+apply(case_tac a, simp_all)
+apply(induct n, auto simp: findnth.simps length_findnth nth_append)
+apply(subgoal_tac "nat = Suc (2 * n)", simp)
+by arith
+
+declare at_begin_norm.simps[simp del] at_begin_fst_bwtn.simps[simp del] 
+   at_begin_fst_awtn.simps[simp del] in_middle.simps[simp del] 
+   abc_lm_s.simps[simp del] abc_lm_v.simps[simp del]  
+   ci.simps[simp del] inv_after_move.simps[simp del] 
+   inv_on_left_moving_norm.simps[simp del] 
+   inv_on_left_moving_in_middle_B.simps[simp del]
+   inv_after_clear.simps[simp del] 
+   inv_after_write.simps[simp del] inv_on_left_moving.simps[simp del]
+   inv_on_right_moving.simps[simp del] 
+   inv_check_left_moving.simps[simp del] 
+   inv_check_left_moving_in_middle.simps[simp del]
+   inv_check_left_moving_on_leftmost.simps[simp del] 
+   inv_after_left_moving.simps[simp del]
+   inv_stop.simps[simp del] inv_locate_a.simps[simp del] 
+   inv_locate_b.simps[simp del]
+
+lemma [intro]: "\<exists>rn. [Bk] = Bk \<up> rn"
+by (metis replicate_0 replicate_Suc)
+
+lemma [intro]:  "at_begin_norm (as, am) (q, aaa, []) ires
+             \<Longrightarrow> at_begin_norm (as, am) (q, aaa, [Bk]) ires"
+apply(simp add: at_begin_norm.simps, erule_tac exE, erule_tac exE)
+apply(rule_tac x = lm1 in exI, simp, auto)
+done
+
+lemma [intro]: "at_begin_fst_bwtn (as, am) (q, aaa, []) ires 
+            \<Longrightarrow> at_begin_fst_bwtn (as, am) (q, aaa, [Bk]) ires"
+apply(simp only: at_begin_fst_bwtn.simps, erule_tac exE, erule_tac exE, erule_tac exE)
+apply(rule_tac x = "am @ 0\<up>tn" in exI, auto)
+done
+
+lemma [intro]: "at_begin_fst_awtn (as, am) (q, aaa, []) ires
+           \<Longrightarrow> at_begin_fst_awtn (as, am) (q, aaa, [Bk]) ires"
+apply(auto simp: at_begin_fst_awtn.simps)
+done 
+
+lemma [intro]: "inv_locate_a (as, am) (q, aaa, []) ires
+            \<Longrightarrow> inv_locate_a (as, am) (q, aaa, [Bk]) ires"
+apply(simp only: inv_locate_a.simps)
+apply(erule disj_forward)
+defer
+apply(erule disj_forward, auto)
+done
+
+lemma tape_of_nl_cons: "<m # lm> = (if lm = [] then Oc\<up>(Suc m)
+                    else Oc\<up>(Suc m) @ Bk # <lm>)"
+apply(case_tac lm, simp_all add: tape_of_nl_abv  tape_of_nat_abv split: if_splits)
+done
+
+
+lemma locate_a_2_locate_a[simp]: "inv_locate_a (as, am) (q, aaa, Bk # xs) ires
+       \<Longrightarrow> inv_locate_a (as, am) (q, aaa, Oc # xs) ires"
+apply(simp only: inv_locate_a.simps at_begin_norm.simps 
+                 at_begin_fst_bwtn.simps at_begin_fst_awtn.simps)
+apply(erule_tac disjE, erule exE, erule exE, erule exE, 
+      rule disjI2, rule disjI2)
+defer
+apply(erule_tac disjE, erule exE, erule exE, 
+      erule exE, rule disjI2, rule disjI2)
+prefer 2
+apply(simp)
+proof-
+  fix lm1 tn rn
+  assume k: "lm1 = am @ 0\<up>tn \<and> length lm1 = q \<and> (if lm1 = [] then aaa = Bk # Bk # 
+    ires else aaa = [Bk] @ <rev lm1> @ Bk # Bk # ires) \<and> Bk # xs = Bk\<up>rn"
+  thus "\<exists>lm1 tn rn. lm1 = am @ 0 \<up> tn \<and> length lm1 = q \<and> 
+    (if lm1 = [] then aaa = Bk # Bk # ires else aaa = [Bk] @ <rev lm1> @ Bk # Bk # ires) \<and> Oc # xs = [Oc] @ Bk \<up> rn"
+    (is "\<exists>lm1 tn rn. ?P lm1 tn rn")
+  proof -
+    from k have "?P lm1 tn (rn - 1)"
+      apply(auto simp: Oc_def)
+      by(case_tac [!] "rn::nat", auto)
+    thus ?thesis by blast
+  qed
+next
+  fix lm1 lm2 rn
+  assume h1: "am = lm1 @ lm2 \<and> length lm1 = q \<and> (if lm1 = [] 
+    then aaa = Bk # Bk # ires else aaa = Bk # <rev lm1> @ Bk # Bk # ires) \<and>
+    Bk # xs = <lm2> @ Bk\<up>rn"
+  from h1 have h2: "lm2 = []"
+    apply(auto split: if_splits)
+    apply(case_tac [!] lm2, simp_all add: tape_of_nl_cons split: if_splits)
+    done
+  from h1 and h2 show "\<exists>lm1 tn rn. lm1 = am @ 0\<up>tn \<and> length lm1 = q \<and> 
+    (if lm1 = [] then aaa = Bk # Bk # ires else aaa = [Bk] @ <rev lm1> @ Bk # Bk # ires) \<and>
+    Oc # xs = [Oc] @ Bk\<up>rn" 
+    (is "\<exists>lm1 tn rn. ?P lm1 tn rn")
+  proof -
+    from h1 and h2  have "?P lm1 0 (rn - 1)"
+      apply(auto simp: Oc_def
+                      tape_of_nl_abv tape_of_nat_list.simps)
+      by(case_tac "rn::nat", simp, simp)
+    thus ?thesis by blast
+  qed
+qed
+
+lemma [simp]: "inv_locate_a (as, am) (q, aaa, []) ires \<Longrightarrow> 
+               inv_locate_a (as, am) (q, aaa, [Oc]) ires"
+apply(insert locate_a_2_locate_a [of as am q aaa "[]"])
+apply(subgoal_tac "inv_locate_a (as, am) (q, aaa, [Bk]) ires", auto)
+done
+
+(*inv: from locate_b to locate_b*)
+lemma [simp]: "inv_locate_b (as, am) (q, aaa, Oc # xs) ires
+         \<Longrightarrow> inv_locate_b (as, am) (q, Oc # aaa, xs) ires"
+apply(simp only: inv_locate_b.simps in_middle.simps)
+apply(erule exE)+
+apply(rule_tac x = lm1 in exI, rule_tac x = lm2 in exI, 
+      rule_tac x = tn in exI, rule_tac x = m in exI)
+apply(rule_tac x = "Suc ml" in exI, rule_tac x = "mr - 1" in exI,
+      rule_tac x = rn in exI)
+apply(case_tac mr, simp_all, auto)
+done
+
+(*
+lemma zero_and_nil[intro]: "(Bk # Bk\<^bsup>n\<^esup> = Oc\<^bsup>mr\<^esup> @ Bk # <lm::nat list> @ 
+                             Bk\<^bsup>rn \<^esup>) \<or> (lm2 = [] \<and> Bk # Bk\<^bsup>n\<^esup> = Oc\<^bsup>mr\<^esup>)
+       \<Longrightarrow> mr = 0 \<and> lm = []"
+apply(rule context_conjI)
+apply(case_tac mr, auto simp:exponent_def)
+apply(insert BkCons_nil[of "replicate (n - 1) Bk" lm rn])
+apply(case_tac n, auto simp: exponent_def Bk_def  tape_of_nl_nil_eq)
+done
+
+lemma tape_of_nat_def: "<[m::nat]> =  Oc # Oc\<^bsup>m\<^esup>"
+apply(simp add: tape_of_nl_abv tape_of_nat_list.simps)
+done
+*)
+lemma [simp]:  "<[x::nat]> = Oc\<up>(Suc x)"
+apply(simp add: tape_of_nat_abv tape_of_nl_abv)
+done
+
+lemma [simp]: " <([]::nat list)> = []"
+apply(simp add: tape_of_nl_abv)
+done
+
+lemma [simp]: "\<lbrakk>inv_locate_b (as, am) (q, aaa, Bk # xs) ires; \<exists>n. xs = Bk\<up>n\<rbrakk>
+            \<Longrightarrow> inv_locate_a (as, am) (Suc q, Bk # aaa, xs) ires"
+apply(simp add: inv_locate_b.simps inv_locate_a.simps)
+apply(rule_tac disjI2, rule_tac disjI1)
+apply(simp only: in_middle.simps at_begin_fst_bwtn.simps)
+apply(erule_tac exE)+
+apply(rule_tac x = "lm1 @ [m]" in exI, rule_tac x = tn in exI, simp split: if_splits)
+apply(case_tac mr, simp_all)
+apply(case_tac "length am", simp_all, case_tac tn, simp_all)
+apply(case_tac lm2, simp_all add: tape_of_nl_cons split: if_splits)
+apply(case_tac am, simp_all)
+apply(case_tac n, simp_all)
+apply(case_tac n, simp_all)
+apply(case_tac mr, simp_all)
+apply(case_tac lm2, simp_all add: tape_of_nl_cons split: if_splits, auto)
+apply(case_tac [!] n, simp_all)
+done
+
+lemma [simp]: "(Oc # r = Bk \<up> rn) = False"
+apply(case_tac rn, simp_all)
+done
+
+lemma [simp]: "(\<exists>rna. Bk \<up> rn = Bk # Bk \<up> rna) \<or> rn = 0"
+apply(case_tac rn, auto)
+done
+
+lemma [simp]: "(\<forall> x. a \<noteq> x) = False"
+by auto
+
+lemma exp_ind: "a\<up>(Suc x) = a\<up>x @ [a]"
+apply(induct x, auto)
+done
+
+lemma [simp]: 
+      "inv_locate_a (as, lm) (q, l, Oc # r) ires
+       \<Longrightarrow> inv_locate_b (as, lm) (q, Oc # l, r) ires"
+apply(simp only: inv_locate_a.simps inv_locate_b.simps in_middle.simps
+          at_begin_norm.simps at_begin_fst_bwtn.simps
+          at_begin_fst_awtn.simps)
+apply(erule disjE, erule exE, erule exE, erule exE)
+apply(rule_tac x = lm1 in exI, rule_tac x = "tl lm2" in exI, simp)
+apply(rule_tac x = 0 in exI, rule_tac x = "hd lm2" in exI)
+apply(case_tac lm2, auto simp: tape_of_nl_cons )
+apply(rule_tac x = 1 in exI, rule_tac x = a in exI, auto)
+apply(case_tac list, simp_all)
+apply(case_tac rn, simp_all)
+apply(rule_tac x = "lm @ replicate tn 0" in exI, 
+      rule_tac x = "[]" in exI, 
+      rule_tac x = "Suc tn" in exI, 
+      rule_tac x = 0 in exI, auto)
+apply(simp only: replicate_Suc[THEN sym] exp_ind)
+apply(rule_tac x = "Suc 0" in exI, auto)
+done
+
+lemma length_equal: "xs = ys \<Longrightarrow> length xs = length ys"
+by auto
+
+lemma [simp]: "\<lbrakk>inv_locate_b (as, am) (q, aaa, Bk # xs) ires; 
+                \<not> (\<exists>n. xs = Bk\<up>n)\<rbrakk> 
+       \<Longrightarrow> inv_locate_a (as, am) (Suc q, Bk # aaa, xs) ires"
+apply(simp add: inv_locate_b.simps inv_locate_a.simps)
+apply(rule_tac disjI1)
+apply(simp only: in_middle.simps at_begin_norm.simps)
+apply(erule_tac exE)+
+apply(rule_tac x = "lm1 @ [m]" in exI, rule_tac x = lm2 in exI, simp)
+apply(subgoal_tac "tn = 0", simp , auto split: if_splits)
+apply(case_tac [!] mr, simp_all, auto)
+apply(simp add: tape_of_nl_cons)
+apply(drule_tac length_equal, simp)
+apply(case_tac "length am", simp_all, erule_tac x = rn in allE, simp)
+apply(drule_tac length_equal, simp)
+apply(case_tac "(Suc (length lm1) - length am)", simp_all)
+apply(case_tac lm2, simp, simp)
+done
+
+lemma locate_b_2_a[intro]: 
+       "inv_locate_b (as, am) (q, aaa, Bk # xs) ires
+    \<Longrightarrow> inv_locate_a (as, am) (Suc q, Bk # aaa, xs) ires"
+apply(case_tac "\<exists> n. xs = Bk\<up>n", simp, simp)
+done
+
+
+lemma [simp]:  "inv_locate_b (as, am) (q, l, []) ires 
+           \<Longrightarrow>  inv_locate_b (as, am) (q, l, [Bk]) ires"
+apply(simp only: inv_locate_b.simps in_middle.simps)
+apply(erule exE)+
+apply(rule_tac x = lm1 in exI, rule_tac x = lm2 in exI, 
+      rule_tac x = tn in exI, rule_tac x = m in exI, 
+      rule_tac x = ml in exI, rule_tac x = mr in exI)
+apply(auto)
+done
+
+(*inv: from locate_b to after_write*)
+
+lemma [simp]: "(a mod 2 \<noteq> Suc 0) = (a mod 2 = 0)  "
+by arith
+
+lemma [simp]: "(a mod 2 \<noteq> 0) = (a mod 2 = Suc 0)  "
+by arith
+
+lemma mod_ex1: "(a mod 2 = Suc 0) = (\<exists> q. a = Suc (2 * q))"
+by arith
+
+lemma mod_ex2: "(a mod (2::nat) = 0) = (\<exists> q. a = 2 * q)"
+by arith
+
+lemma [simp]: "(2*q - Suc 0) div 2 = (q - 1)"
+by arith
+
+lemma [simp]: "(Suc (2*q)) div 2 = q"
+by arith
+
+lemma mod_2: "x mod 2  = 0 \<or>  x mod 2 = Suc 0"
+by arith
+
+lemma [simp]: "x mod 2 = 0 \<Longrightarrow> Suc x mod 2 = Suc 0"
+by arith
+
+lemma [simp]: "x mod 2 = Suc 0 \<Longrightarrow> Suc x mod 2 = 0"
+by arith
+
+lemma [simp]:  "inv_locate_b (as, am) (q, l, []) ires 
+           \<Longrightarrow>  inv_locate_b (as, am) (q, l, [Bk]) ires"
+apply(simp only: inv_locate_b.simps in_middle.simps)
+apply(erule exE)+
+apply(rule_tac x = lm1 in exI, rule_tac x = lm2 in exI, 
+      rule_tac x = tn in exI, rule_tac x = m in exI, 
+      rule_tac x = ml in exI, rule_tac x = mr in exI)
+apply(auto)
+done
+
+lemma locate_b_2_locate_a[simp]: 
+    "\<lbrakk>q > 0;  inv_locate_b (as, am) (q - Suc 0, aaa, Bk # xs) ires\<rbrakk>
+   \<Longrightarrow>  inv_locate_a (as, am) (q, Bk # aaa, xs) ires"
+apply(insert locate_b_2_a [of as am "q - 1" aaa xs ires], simp)
+done
+
+
+lemma [simp]:  "inv_locate_b (as, am) (q, l, []) ires 
+           \<Longrightarrow>  inv_locate_b (as, am) (q, l, [Bk]) ires"
+apply(simp only: inv_locate_b.simps in_middle.simps)
+apply(erule exE)+
+apply(rule_tac x = lm1 in exI, rule_tac x = lm2 in exI, 
+      rule_tac x = tn in exI, rule_tac x = m in exI, 
+      rule_tac x = ml in exI, rule_tac x = mr in exI)
+apply(auto)
+done
+
+(*inv: from locate_b to after_write*)
+
+lemma [simp]:
+  "crsp (layout_of ap) (as, lm) (s, l, r) ires
+  \<Longrightarrow> findnth_inv (layout_of ap) n (as, lm) (Suc 0, l, r) ires"
+apply(auto simp: crsp.simps findnth_inv.simps inv_locate_a.simps
+               at_begin_norm.simps at_begin_fst_awtn.simps at_begin_fst_bwtn.simps)
+done
+
+lemma findnth_correct_pre: 
+  assumes layout: "ly = layout_of ap"
+  and crsp: "crsp ly (as, lm) (s, l, r) ires"
+  and not0: "n > 0"
+  and f: "f = (\<lambda> stp. (steps (Suc 0, l, r) (findnth n, 0) stp, n))"
+  and P: "P = (\<lambda> ((s, l, r), n). s = Suc (2 * n))"
+  and Q: "Q = (\<lambda> ((s, l, r), n). findnth_inv ly n (as, lm) (s, l, r) ires)"
+  shows "\<exists> stp. P (f stp) \<and> Q (f stp)"
+thm halt_lemma2
+proof(rule_tac LE = findnth_LE in halt_lemma2)
+  show "wf findnth_LE"  by(intro wf_findnth_LE)
+next
+  show "Q (f 0)"
+    using crsp layout
+    apply(simp add: f P Q steps.simps)
+    done
+next
+  show "\<not> P (f 0)"
+    using not0
+    apply(simp add: f P steps.simps)
+    done
+next
+  show "\<forall>n. \<not> P (f n) \<and> Q (f n) \<longrightarrow> Q (f (Suc n)) \<and> (f (Suc n), f n) 
+        \<in> findnth_LE"
+  proof(rule_tac allI, rule_tac impI, simp add: f, 
+      case_tac "steps (Suc 0, l, r) (findnth n, 0) na", simp add: P)
+    fix na a b c
+    assume "a \<noteq> Suc (2 * n) \<and> Q ((a, b, c), n)"
+    thus  "Q (step (a, b, c) (findnth n, 0), n) \<and> 
+        ((step (a, b, c) (findnth n, 0), n), (a, b, c), n) \<in> findnth_LE"
+      apply(case_tac c, case_tac [2] aa)
+      apply(simp_all add: step.simps findnth_LE_def Q findnth_inv.simps mod_2  lex_pair_def split: if_splits)
+      apply(auto simp: mod_ex1 mod_ex2)
+      done
+  qed
+qed
+            
+lemma [intro]: "inv_locate_a (as, lm) (0, Bk # Bk # ires, <lm> @ Bk \<up> x) ires"
+apply(auto simp: crsp.simps inv_locate_a.simps at_begin_norm.simps)
+done
+lemma [simp]: "crsp ly (as, lm) (s, l, r) ires \<Longrightarrow> inv_locate_a (as, lm) (0, l, r) ires"
+apply(auto simp: crsp.simps inv_locate_a.simps at_begin_norm.simps)
+done
+
+lemma findnth_correct: 
+  assumes layout: "ly = layout_of ap"
+  and crsp: "crsp ly (as, lm) (s, l, r) ires"
+  shows "\<exists> stp l' r'. steps (Suc 0, l, r) (findnth n, 0) stp = (Suc (2 * n), l', r')
+              \<and> inv_locate_a (as, lm) (n, l', r') ires"
+  using crsp
+  apply(case_tac "n = 0")
+  apply(rule_tac x = 0 in exI, auto simp: steps.simps)
+  using assms
+  apply(drule_tac findnth_correct_pre, auto)
+  apply(rule_tac x = stp in exI, simp add: findnth_inv.simps)
+  done
+
+
+fun inc_inv :: "nat \<Rightarrow> inc_inv_t"
+  where
+  "inc_inv n (as, lm) (s, l, r) ires =
+              (let lm' = abc_lm_s lm n (Suc (abc_lm_v lm n)) in
+                if s = 0 then False
+                else if s = 1 then 
+                   inv_locate_a (as, lm) (n, l, r) ires
+                else if s = 2 then 
+                   inv_locate_b (as, lm) (n, l, r) ires
+                else if s = 3 then 
+                   inv_after_write (as, lm') (s, l, r) ires
+                else if s = Suc 3 then 
+                   inv_after_move (as, lm') (s, l, r) ires
+                else if s = Suc 4 then 
+                   inv_after_clear (as, lm') (s, l, r) ires
+                else if s = Suc (Suc 4) then 
+                   inv_on_right_moving (as, lm') (s, l, r) ires
+                else if s = Suc (Suc 5) then 
+                   inv_on_left_moving (as, lm') (s, l, r) ires
+                else if s = Suc (Suc (Suc 5)) then 
+                   inv_check_left_moving (as, lm') (s, l, r) ires
+                else if s = Suc (Suc (Suc (Suc 5))) then 
+                   inv_after_left_moving (as, lm') (s, l, r) ires
+                else if s = Suc (Suc (Suc (Suc (Suc 5)))) then 
+                   inv_stop (as, lm') (s, l, r) ires
+                else False)"
+
+
+fun abc_inc_stage1 :: "config \<Rightarrow> nat"
+  where
+  "abc_inc_stage1 (s, l, r) = 
+            (if s = 0 then 0
+             else if s \<le> 2 then 5
+             else if s \<le> 6 then 4
+             else if s \<le> 8 then 3
+             else if s = 9 then 2
+             else 1)"
+
+fun abc_inc_stage2 :: "config \<Rightarrow> nat"
+  where
+  "abc_inc_stage2 (s, l, r) =
+                (if s = 1 then 2
+                 else if s = 2 then 1
+                 else if s = 3 then length r
+                 else if s = 4 then length r
+                 else if s = 5 then length r
+                 else if s = 6 then 
+                                  if r \<noteq> [] then length r
+                                  else 1
+                 else if s = 7 then length l
+                 else if s = 8 then length l
+                 else 0)"
+
+fun abc_inc_stage3 :: "config \<Rightarrow>  nat"
+  where
+  "abc_inc_stage3 (s, l, r) = (
+              if s = 4 then 4
+              else if s = 5 then 3
+              else if s = 6 then 
+                   if r \<noteq> [] \<and> hd r = Oc then 2
+                   else 1
+              else if s = 3 then 0
+              else if s = 2 then length r
+              else if s = 1 then 
+                      if (r \<noteq> [] \<and> hd r = Oc) then 0
+                      else 1
+              else 10 - s)"
+
+
+definition inc_measure :: "config \<Rightarrow> nat \<times> nat \<times> nat"
+  where
+  "inc_measure c = 
+    (abc_inc_stage1 c, abc_inc_stage2 c, abc_inc_stage3 c)"
+
+definition lex_triple :: 
+   "((nat \<times> (nat \<times> nat)) \<times> (nat \<times> (nat \<times> nat))) set"
+  where "lex_triple \<equiv> less_than <*lex*> lex_pair"
+
+definition inc_LE :: "(config \<times> config) set"
+  where
+  "inc_LE \<equiv> (inv_image lex_triple inc_measure)"
+
+declare inc_inv.simps[simp del]
+
+lemma wf_inc_le[intro]: "wf inc_LE"
+by(auto intro:wf_inv_image simp: inc_LE_def lex_triple_def lex_pair_def)
+
+lemma numeral_5_eq_5: "5 = Suc (Suc (Suc (Suc (Suc 0))))"
+by arith
+
+lemma numeral_6_eq_6: "6 = Suc (Suc (Suc (Suc (Suc 1))))"
+by arith
+
+lemma numeral_7_eq_7: "7 = Suc (Suc (Suc (Suc (Suc 2))))"
+by arith
+
+lemma numeral_8_eq_8: "8 = Suc (Suc (Suc (Suc (Suc 3))))"
+by arith
+
+lemma numeral_9_eq_9: "9 = Suc (Suc (Suc (Suc (Suc (Suc 3)))))"
+by arith
+
+lemma numeral_10_eq_10: "10 = Suc (Suc (Suc (Suc (Suc (Suc (Suc 3))))))"
+by arith
+
+lemma inv_locate_b_2_after_write[simp]: 
+      "inv_locate_b (as, am) (n, aaa, Bk # xs) ires
+      \<Longrightarrow> inv_after_write (as, abc_lm_s am n (Suc (abc_lm_v am n)))
+          (s, aaa, Oc # xs) ires"
+apply(auto simp: in_middle.simps inv_after_write.simps 
+                 abc_lm_v.simps abc_lm_s.simps  inv_locate_b.simps)
+apply(case_tac [!] mr, auto split: if_splits)
+apply(rule_tac x = rn in exI, rule_tac x = "Suc m" in exI,
+      rule_tac x = "lm1" in exI, simp)
+apply(rule_tac x = "lm2" in exI, simp)
+apply(simp only: Suc_diff_le exp_ind)
+apply(subgoal_tac "lm2 = []", simp)
+apply(drule_tac length_equal, simp)
+done
+
+lemma [simp]: "inv_locate_b (as, am) (n, aaa, []) ires \<Longrightarrow> 
+     inv_after_write (as, abc_lm_s am n (Suc (abc_lm_v am n))) 
+                     (s, aaa, [Oc]) ires"
+apply(insert inv_locate_b_2_after_write [of as am n aaa "[]"])
+by(simp)
+
+
+
+(*inv: from after_write to after_move*)
+lemma [simp]: "inv_after_write (as, lm) (x, l, Oc # r) ires
+                \<Longrightarrow> inv_after_move (as, lm) (y, Oc # l, r) ires"
+apply(auto simp:inv_after_move.simps inv_after_write.simps split: if_splits)
+done
+
+lemma [simp]: "inv_after_write (as, abc_lm_s am n (Suc (abc_lm_v am n)
+                )) (x, aaa, Bk # xs) ires = False"
+apply(simp add: inv_after_write.simps )
+done
+
+lemma [simp]: 
+ "inv_after_write (as, abc_lm_s am n (Suc (abc_lm_v am n))) 
+                        (x, aaa, []) ires = False"
+apply(simp add: inv_after_write.simps )
+done
+
+(*inv: from after_move to after_clear*)
+lemma [simp]: "inv_after_move (as, lm) (s, l, Oc # r) ires
+                \<Longrightarrow> inv_after_clear (as, lm) (s', l, Bk # r) ires"
+apply(auto simp: inv_after_move.simps inv_after_clear.simps split: if_splits)
+done
+
+(*inv: from after_move to on_leftmoving*)
+lemma [intro]: "Bk \<up> rn = Bk # Bk \<up> (rn - Suc 0) \<or> rn = 0"
+apply(case_tac rn, auto)
+done
+
+lemma inv_after_move_2_inv_on_left_moving[simp]:  
+   "inv_after_move (as, lm) (s, l, Bk # r) ires
+   \<Longrightarrow> (l = [] \<longrightarrow> 
+         inv_on_left_moving (as, lm) (s', [], Bk # Bk # r) ires) \<and>
+      (l \<noteq> [] \<longrightarrow> 
+         inv_on_left_moving (as, lm) (s', tl l, hd l # Bk # r) ires)"
+apply(simp only: inv_after_move.simps inv_on_left_moving.simps)
+apply(subgoal_tac "l \<noteq> []", rule conjI, simp, rule impI, 
+                rule disjI1, simp only: inv_on_left_moving_norm.simps)
+apply(erule exE)+
+apply(subgoal_tac "lm2 = []")
+apply(rule_tac x = lm1 in exI, rule_tac x = lm2 in exI,  
+    rule_tac x = m in exI, rule_tac x = m in exI, 
+    rule_tac x = 1 in exI,  
+    rule_tac x = "rn - 1" in exI, auto)
+apply(auto split: if_splits)
+apply(case_tac [1-2] rn, simp_all)
+apply(case_tac [!] lm2, simp_all add: tape_of_nl_cons split: if_splits)
+done
+
+
+lemma inv_after_move_2_inv_on_left_moving_B[simp]: 
+    "inv_after_move (as, lm) (s, l, []) ires
+      \<Longrightarrow> (l = [] \<longrightarrow> inv_on_left_moving (as, lm) (s', [], [Bk]) ires) \<and>
+          (l \<noteq> [] \<longrightarrow> inv_on_left_moving (as, lm) (s', tl l, [hd l]) ires)"
+apply(simp only: inv_after_move.simps inv_on_left_moving.simps)
+apply(subgoal_tac "l \<noteq> []", rule conjI, simp, rule impI, rule disjI1,
+        simp only: inv_on_left_moving_norm.simps)
+apply(erule exE)+
+apply(subgoal_tac "lm2 = []")
+apply(rule_tac x = lm1 in exI, rule_tac x = lm2 in exI,  
+      rule_tac x = m in exI, rule_tac x = m in exI, 
+      rule_tac x = 1 in exI, rule_tac x = "rn - 1" in exI, simp, case_tac rn)
+apply(auto split: if_splits)
+apply(case_tac [!] lm2, auto simp: tape_of_nl_cons split: if_splits)
+done
+
+(*inv: from after_clear to on_right_moving*)
+lemma [simp]: "Oc # r = replicate rn Bk = False"
+apply(case_tac rn, simp, simp)
+done
+
+lemma inv_after_clear_2_inv_on_right_moving[simp]: 
+     "inv_after_clear (as, lm) (x, l, Bk # r) ires
+      \<Longrightarrow> inv_on_right_moving (as, lm) (y, Bk # l, r) ires"
+apply(auto simp: inv_after_clear.simps inv_on_right_moving.simps )
+apply(subgoal_tac "lm2 \<noteq> []")
+apply(rule_tac x = "lm1 @ [m]" in exI, rule_tac x = "tl lm2" in exI, 
+      rule_tac x = "hd lm2" in exI, simp)
+apply(rule_tac x = 0 in exI, rule_tac x = "hd lm2" in exI)
+apply(simp, rule conjI)
+apply(case_tac [!] "lm2::nat list", auto)
+apply(case_tac rn, auto split: if_splits simp: tape_of_nl_cons)
+apply(case_tac [!] rn, simp_all)
+done
+
+lemma [simp]: "inv_after_clear (as, lm) (x, l, []) ires\<Longrightarrow> 
+               inv_after_clear (as, lm) (y, l, [Bk]) ires" 
+by(auto simp: inv_after_clear.simps)
+
+lemma [simp]: "inv_after_clear (as, lm) (x, l, []) ires
+             \<Longrightarrow> inv_on_right_moving (as, lm) (y, Bk # l, []) ires"
+by(insert 
+    inv_after_clear_2_inv_on_right_moving[of as lm n l "[]"], simp)
+
+(*inv: from on_right_moving to on_right_movign*)
+lemma [simp]: "inv_on_right_moving (as, lm) (x, l, Oc # r) ires
+      \<Longrightarrow> inv_on_right_moving (as, lm) (y, Oc # l, r) ires"
+apply(auto simp: inv_on_right_moving.simps)
+apply(rule_tac x = lm1 in exI, rule_tac x = lm2 in exI, 
+           rule_tac x = "ml + mr" in exI, simp)
+apply(rule_tac x = "Suc ml" in exI, 
+           rule_tac x = "mr - 1" in exI, simp)
+apply(case_tac mr, auto)
+apply(rule_tac x = lm1 in exI, rule_tac x = "[]" in exI, 
+      rule_tac x = "ml + mr" in exI, simp)
+apply(rule_tac x = "Suc ml" in exI, 
+      rule_tac x = "mr - 1" in exI, simp)
+apply(case_tac mr, auto split: if_splits)
+done
+
+lemma inv_on_right_moving_2_inv_on_right_moving[simp]: 
+     "inv_on_right_moving (as, lm) (x, l, Bk # r) ires
+     \<Longrightarrow> inv_after_write (as, lm) (y, l, Oc # r) ires"
+apply(auto simp: inv_on_right_moving.simps inv_after_write.simps )
+apply(case_tac mr, auto simp: split: if_splits)
+done
+      
+lemma [simp]: "inv_on_right_moving (as, lm) (x, l, []) ires\<Longrightarrow> 
+             inv_on_right_moving (as, lm) (y, l, [Bk]) ires"
+apply(auto simp: inv_on_right_moving.simps)
+apply(rule_tac x = lm1 in exI, rule_tac x = "[]" in exI, simp)
+done
+
+(*inv: from on_right_moving to after_write*)
+lemma [simp]: "inv_on_right_moving (as, lm) (x, l, []) ires
+       \<Longrightarrow> inv_after_write (as, lm) (y, l, [Oc]) ires"
+apply(rule_tac inv_on_right_moving_2_inv_on_right_moving, simp)
+done
+
+(*inv: from on_left_moving to on_left_moving*)
+lemma [simp]: "inv_on_left_moving_in_middle_B (as, lm) 
+               (s, l, Oc # r) ires = False"
+apply(auto simp: inv_on_left_moving_in_middle_B.simps )
+done
+
+lemma [simp]: "inv_on_left_moving_norm (as, lm) (s, l, Bk # r) ires 
+             = False"
+apply(auto simp: inv_on_left_moving_norm.simps)
+apply(case_tac [!] mr, auto simp: )
+done
+
+lemma [simp]: 
+  "\<lbrakk>inv_on_left_moving_norm (as, lm) (s, l, Oc # r) ires;
+    hd l = Bk; l \<noteq> []\<rbrakk> \<Longrightarrow> 
+     inv_on_left_moving_in_middle_B (as, lm) (s, tl l, Bk # Oc # r) ires"
+apply(case_tac l, simp, simp)
+apply(simp only: inv_on_left_moving_norm.simps 
+                 inv_on_left_moving_in_middle_B.simps)
+apply(erule_tac exE)+
+apply(rule_tac x = lm1 in exI, rule_tac x = "m # lm2" in exI, auto)
+apply(case_tac [!] ml, auto)
+apply(auto simp: tape_of_nl_cons split: if_splits)
+apply(rule_tac [!] x = "Suc rn" in exI, simp_all)
+done
+
+lemma [simp]: "\<lbrakk>inv_on_left_moving_norm (as, lm) (s, l, Oc # r) ires; 
+                hd l = Oc; l \<noteq> []\<rbrakk>
+            \<Longrightarrow> inv_on_left_moving_norm (as, lm) 
+                                        (s, tl l, Oc # Oc # r) ires"
+apply(simp only: inv_on_left_moving_norm.simps)
+apply(erule exE)+
+apply(rule_tac x = lm1 in exI, rule_tac x = lm2 in exI, 
+      rule_tac x = m in exI, rule_tac x = "ml - 1" in exI,
+      rule_tac x = "Suc mr" in exI, rule_tac x = rn in exI, simp)
+apply(case_tac ml, auto simp: split: if_splits)
+done
+
+lemma [simp]: "inv_on_left_moving_norm (as, lm) (s, [], Oc # r) ires
+     \<Longrightarrow> inv_on_left_moving_in_middle_B (as, lm) (s, [], Bk # Oc # r) ires"
+apply(auto simp: inv_on_left_moving_norm.simps 
+                 inv_on_left_moving_in_middle_B.simps split: if_splits)
+done
+
+lemma [simp]:"inv_on_left_moving (as, lm) (s, l, Oc # r) ires
+    \<Longrightarrow> (l = [] \<longrightarrow> inv_on_left_moving (as, lm) (s, [], Bk # Oc # r) ires)
+ \<and>  (l \<noteq> [] \<longrightarrow> inv_on_left_moving (as, lm) (s, tl l, hd l # Oc # r) ires)"
+apply(simp add: inv_on_left_moving.simps)
+apply(case_tac "l \<noteq> []", rule conjI, simp, simp)
+apply(case_tac "hd l", simp, simp, simp)
+done
+
+(*inv: from on_left_moving to check_left_moving*)
+lemma [simp]: "inv_on_left_moving_in_middle_B (as, lm) 
+                                      (s, Bk # list, Bk # r) ires
+          \<Longrightarrow> inv_check_left_moving_on_leftmost (as, lm) 
+                                      (s', list, Bk # Bk # r) ires"
+apply(auto simp: inv_on_left_moving_in_middle_B.simps 
+                 inv_check_left_moving_on_leftmost.simps split: if_splits)
+apply(case_tac [!] "rev lm1", simp_all)
+apply(case_tac [!] lista, simp_all add: tape_of_nl_abv tape_of_nat_abv tape_of_nat_list.simps)
+done
+
+lemma [simp]:
+    "inv_check_left_moving_in_middle (as, lm) (s, l, Bk # r) ires= False"
+by(auto simp: inv_check_left_moving_in_middle.simps )
+
+lemma [simp]: 
+ "inv_on_left_moving_in_middle_B (as, lm) (s, [], Bk # r) ires\<Longrightarrow> 
+  inv_check_left_moving_on_leftmost (as, lm) (s', [], Bk # Bk # r) ires"
+apply(auto simp: inv_on_left_moving_in_middle_B.simps 
+                 inv_check_left_moving_on_leftmost.simps split: if_splits)
+done
+
+lemma [simp]: "inv_check_left_moving_on_leftmost (as, lm) 
+                                       (s, list, Oc # r) ires= False"
+by(auto simp: inv_check_left_moving_on_leftmost.simps split: if_splits)
+
+lemma [simp]: "inv_on_left_moving_in_middle_B (as, lm) 
+                                         (s, Oc # list, Bk # r) ires
+ \<Longrightarrow> inv_check_left_moving_in_middle (as, lm) (s', list, Oc # Bk # r) ires"
+apply(auto simp: inv_on_left_moving_in_middle_B.simps 
+                 inv_check_left_moving_in_middle.simps  split: if_splits)
+done
+
+lemma inv_on_left_moving_2_check_left_moving[simp]:
+ "inv_on_left_moving (as, lm) (s, l, Bk # r) ires
+ \<Longrightarrow> (l = [] \<longrightarrow> inv_check_left_moving (as, lm) (s', [], Bk # Bk # r) ires)
+ \<and> (l \<noteq> [] \<longrightarrow> 
+      inv_check_left_moving (as, lm) (s', tl l, hd l # Bk # r) ires)"
+apply(simp add: inv_on_left_moving.simps inv_check_left_moving.simps)
+apply(case_tac l, simp, simp)
+apply(case_tac a, simp, simp)
+done
+
+lemma [simp]: "inv_on_left_moving_norm (as, lm) (s, l, []) ires = False"
+apply(auto simp: inv_on_left_moving_norm.simps)
+done
+
+lemma [simp]: "inv_on_left_moving (as, lm) (s, l, []) ires\<Longrightarrow> 
+     inv_on_left_moving (as, lm) (6 + 2 * n, l, [Bk]) ires"
+apply(simp add: inv_on_left_moving.simps)
+apply(auto simp: inv_on_left_moving_in_middle_B.simps)
+done
+
+lemma [simp]: "inv_on_left_moving (as, lm) (s, l, []) ires = False"
+apply(simp add: inv_on_left_moving.simps)
+apply(simp add: inv_on_left_moving_in_middle_B.simps)
+done
+
+lemma [simp]: "inv_on_left_moving (as, lm) (s, l, []) ires
+ \<Longrightarrow> (l = [] \<longrightarrow> inv_check_left_moving (as, lm) (s', [], [Bk]) ires) \<and>
+    (l \<noteq> [] \<longrightarrow> inv_check_left_moving (as, lm) (s', tl l, [hd l]) ires)"
+by simp
+
+lemma [intro]: "\<exists>rna. Bk # Bk \<up> rn = Bk \<up> rna"
+apply(rule_tac x = "Suc rn" in exI, simp)
+done
+
+lemma 
+inv_check_left_moving_in_middle_2_on_left_moving_in_middle_B[simp]:
+"inv_check_left_moving_in_middle (as, lm) (s, Bk # list, Oc # r) ires
+  \<Longrightarrow> inv_on_left_moving_in_middle_B (as, lm) (s', list, Bk # Oc # r) ires"
+apply(simp only: inv_check_left_moving_in_middle.simps 
+                 inv_on_left_moving_in_middle_B.simps)
+apply(erule_tac exE)+
+apply(rule_tac x = "rev (tl (rev lm1))" in exI, 
+      rule_tac x = "[hd (rev lm1)] @ lm2" in exI, auto)
+apply(case_tac [!] "rev lm1",simp_all add: tape_of_nat_abv tape_of_nl_abv tape_of_nat_list.simps)
+apply(case_tac [!] a, simp_all)
+apply(case_tac [1] lm2, simp_all add: tape_of_nat_list.simps tape_of_nat_abv, auto)
+apply(case_tac [3] lm2, simp_all add: tape_of_nat_list.simps tape_of_nat_abv, auto)
+apply(case_tac [!] lista, simp_all add: tape_of_nat_abv tape_of_nat_list.simps)
+done
+
+lemma [simp]: 
+ "inv_check_left_moving_in_middle (as, lm) (s, [], Oc # r) ires\<Longrightarrow>
+     inv_check_left_moving_in_middle (as, lm) (s', [Bk], Oc # r) ires"
+apply(auto simp: inv_check_left_moving_in_middle.simps )
+done
+
+lemma [simp]: 
+ "inv_check_left_moving_in_middle (as, lm) (s, [], Oc # r) ires
+   \<Longrightarrow> inv_on_left_moving_in_middle_B (as, lm) (s', [], Bk # Oc # r) ires"
+apply(insert 
+inv_check_left_moving_in_middle_2_on_left_moving_in_middle_B[of 
+                  as lm n "[]" r], simp)
+done 
+
+lemma [simp]: "inv_check_left_moving_in_middle (as, lm) 
+                       (s, Oc # list, Oc # r) ires
+   \<Longrightarrow> inv_on_left_moving_norm (as, lm) (s', list, Oc # Oc # r) ires"
+apply(auto simp: inv_check_left_moving_in_middle.simps 
+                 inv_on_left_moving_norm.simps)
+apply(rule_tac x = "rev (tl (rev lm1))" in exI, 
+      rule_tac x = lm2 in exI, rule_tac x = "hd (rev lm1)" in exI)
+apply(rule_tac conjI)
+apply(case_tac "rev lm1", simp, simp)
+apply(rule_tac x = "hd (rev lm1) - 1" in exI, auto)
+apply(rule_tac [!] x = "Suc (Suc 0)" in exI, simp)
+apply(case_tac [!] "rev lm1", simp_all)
+apply(case_tac [!] a, simp_all add: tape_of_nl_cons split: if_splits)
+done
+
+lemma [simp]: "inv_check_left_moving (as, lm) (s, l, Oc # r) ires
+\<Longrightarrow> (l = [] \<longrightarrow> inv_on_left_moving (as, lm) (s', [], Bk # Oc # r) ires) \<and>
+   (l \<noteq> [] \<longrightarrow> inv_on_left_moving (as, lm) (s', tl l, hd l # Oc # r) ires)"
+apply(case_tac l, 
+      auto simp: inv_check_left_moving.simps inv_on_left_moving.simps)
+apply(case_tac a, simp, simp)
+done
+
+(*inv: check_left_moving to after_left_moving*)
+lemma [simp]: "inv_check_left_moving (as, lm) (s, l, Bk # r) ires
+                \<Longrightarrow> inv_after_left_moving (as, lm) (s', Bk # l, r) ires"
+apply(auto simp: inv_check_left_moving.simps 
+ inv_check_left_moving_on_leftmost.simps inv_after_left_moving.simps)
+done
+
+
+lemma [simp]:"inv_check_left_moving (as, lm) (s, l, []) ires
+      \<Longrightarrow> inv_after_left_moving (as, lm) (s', Bk # l, []) ires"
+by(simp add: inv_check_left_moving.simps  
+inv_check_left_moving_in_middle.simps 
+inv_check_left_moving_on_leftmost.simps)
+
+(*inv: after_left_moving to inv_stop*)
+lemma [simp]: "inv_after_left_moving (as, lm) (s, l, Bk # r) ires
+       \<Longrightarrow> inv_stop (as, lm) (s', Bk # l, r) ires"
+apply(auto simp: inv_after_left_moving.simps inv_stop.simps)
+done
+
+lemma [simp]: "inv_after_left_moving (as, lm) (s, l, []) ires
+             \<Longrightarrow> inv_stop (as, lm) (s', Bk # l, []) ires"
+by(auto simp: inv_after_left_moving.simps)
+
+(*inv: stop to stop*)
+lemma [simp]: "inv_stop (as, lm) (x, l, r) ires \<Longrightarrow> 
+               inv_stop (as, lm) (y, l, r) ires"
+apply(simp add: inv_stop.simps)
+done
+
+lemma [simp]: "inv_after_clear (as, lm) (s, aaa, Oc # xs) ires= False"
+apply(auto simp: inv_after_clear.simps )
+done
+
+lemma [simp]: 
+  "inv_after_left_moving (as, lm) (s, aaa, Oc # xs) ires = False"
+by(auto simp: inv_after_left_moving.simps  )
+
+lemma [simp]: "inv_after_clear (as, abc_lm_s lm n (Suc (abc_lm_v lm n))) (s, b, []) ires = False"
+apply(auto simp: inv_after_clear.simps)
+done
+
+lemma [simp]: "inv_on_left_moving (as, abc_lm_s lm n (Suc (abc_lm_v lm n))) 
+           (s, b, Oc # list) ires \<Longrightarrow> b \<noteq> []"
+apply(auto simp: inv_on_left_moving.simps inv_on_left_moving_norm.simps split: if_splits)
+done
+
+lemma [simp]: "inv_check_left_moving (as, abc_lm_s lm n (Suc (abc_lm_v lm n))) (s, b, Oc # list) ires \<Longrightarrow> b \<noteq> []"
+apply(auto simp: inv_check_left_moving.simps inv_check_left_moving_in_middle.simps split: if_splits)
+done
+
+lemma tinc_correct_pre:
+  assumes layout: "ly = layout_of ap"
+  and inv_start: "inv_locate_a (as, lm) (n, l, r) ires"
+  and lm': "lm' = abc_lm_s lm n (Suc (abc_lm_v lm n))"
+  and f: "f = steps (Suc 0, l, r) (tinc_b, 0)"
+  and P: "P = (\<lambda> (s, l, r). s = 10)"
+  and Q: "Q = (\<lambda> (s, l, r). inc_inv n (as, lm) (s, l, r) ires)" 
+  shows "\<exists> stp. P (f stp) \<and> Q (f stp)"
+proof(rule_tac LE = inc_LE in halt_lemma2)
+  show "wf inc_LE" by(auto)
+next
+  show "Q (f 0)"
+    using inv_start
+    apply(simp add: f P Q steps.simps inc_inv.simps)
+    done
+next
+  show "\<not> P (f 0)"
+    apply(simp add: f P steps.simps)
+    done
+next
+  show "\<forall>n. \<not> P (f n) \<and> Q (f n) \<longrightarrow> Q (f (Suc n)) \<and> (f (Suc n), f n) 
+        \<in> inc_LE"
+  proof(rule_tac allI, rule_tac impI, simp add: f, 
+      case_tac "steps (Suc 0, l, r) (tinc_b, 0) n", simp add: P)
+    fix n a b c
+    assume "a \<noteq> 10 \<and> Q (a, b, c)"
+    thus  "Q (step (a, b, c) (tinc_b, 0)) \<and> (step (a, b, c) (tinc_b, 0), a, b, c) \<in> inc_LE"
+      apply(simp add:Q)
+      apply(simp add: inc_inv.simps)
+      apply(case_tac c, case_tac [2] aa)
+      apply(auto simp: Let_def step.simps tinc_b_def numeral_2_eq_2 numeral_3_eq_3  split: if_splits)
+      apply(simp_all add: inc_inv.simps inc_LE_def lex_triple_def lex_pair_def inc_measure_def numeral_5_eq_5
+                          numeral_6_eq_6 numeral_7_eq_7 numeral_8_eq_8 numeral_9_eq_9)         
+      done
+  qed
+qed
+         
+
+lemma tinc_correct: 
+  assumes layout: "ly = layout_of ap"
+  and inv_start: "inv_locate_a (as, lm) (n, l, r) ires"
+  and lm': "lm' = abc_lm_s lm n (Suc (abc_lm_v lm n))"
+  shows "\<exists> stp l' r'. steps (Suc 0, l, r) (tinc_b, 0) stp = (10, l', r')
+              \<and> inv_stop (as, lm') (10, l', r') ires"
+  using assms
+  apply(drule_tac tinc_correct_pre, auto)
+  apply(rule_tac x = stp in exI, simp)
+  apply(simp add: inc_inv.simps)
+  done
+
+declare inv_locate_a.simps[simp del] abc_lm_s.simps[simp del]
+        abc_lm_v.simps[simp del]
+
+lemma [simp]: "(4::nat) * n mod 2 = 0"
+apply(arith)
+done
+
+lemma crsp_step_inc_pre:
+  assumes layout: "ly = layout_of ap"
+  and crsp: "crsp ly (as, lm) (s, l, r) ires"
+  and aexec: "abc_step_l (as, lm) (Some (Inc n)) = (asa, lma)"
+  shows "\<exists> stp k. steps (Suc 0, l, r) (findnth n @ shift tinc_b (2 * n), 0) stp 
+        = (2*n + 10, Bk # Bk # ires, <lma> @ Bk\<up>k) \<and> stp > 0"
+proof -
+  thm tm_append_steps
+  have "\<exists> stp l' r'. steps (Suc 0, l, r) (findnth n, 0) stp = (Suc (2 * n), l', r')
+    \<and> inv_locate_a (as, lm) (n, l', r') ires"
+    using assms
+    apply(rule_tac findnth_correct, simp_all add: crsp layout)
+    done
+  from this obtain stp l' r' where a:
+    "steps (Suc 0, l, r) (findnth n, 0) stp = (Suc (2 * n), l', r')
+    \<and> inv_locate_a (as, lm) (n, l', r') ires" by blast
+  moreover have
+    "\<exists> stp la ra. steps (Suc 0, l', r') (tinc_b, 0) stp = (10, la, ra)
+                        \<and> inv_stop (as, lma) (10, la, ra) ires"
+    using assms a
+  proof(rule_tac lm' = lma and n = n and lm = lm and ly = ly and ap = ap in tinc_correct,
+      simp, simp)
+    show "lma = abc_lm_s lm n (Suc (abc_lm_v lm n))"
+      using aexec
+      apply(simp add: abc_step_l.simps)
+      done
+  qed
+  from this obtain stpa la ra where b:
+    "steps (Suc 0, l', r') (tinc_b, 0) stpa = (10, la, ra)
+    \<and> inv_stop (as, lma) (10, la, ra) ires" by blast
+  from a b show "\<exists>stp k. steps (Suc 0, l, r) (findnth n @ shift tinc_b (2 * n), 0) stp
+    = (2 * n + 10, Bk # Bk # ires, <lma> @ Bk \<up> k) \<and> stp > 0"
+    apply(rule_tac x = "stp + stpa" in exI)
+    using tm_append_steps[of "Suc 0" l r "findnth n" stp l' r' tinc_b stpa 10 la ra "length (findnth n) div 2"]
+    apply(simp add: length_findnth inv_stop.simps)
+    apply(case_tac stpa, simp_all add: steps.simps)
+    done
+qed 
+     
+lemma crsp_step_inc:
+  assumes layout: "ly = layout_of ap"
+  and crsp: "crsp ly (as, lm) (s, l, r) ires"
+  and fetch: "abc_fetch as ap = Some (Inc n)"
+  shows "\<exists>stp > 0. crsp ly (abc_step_l (as, lm) (Some (Inc n)))
+  (steps (s, l, r) (ci ly (start_of ly as) (Inc n), start_of ly as - Suc 0) stp) ires"
+proof(case_tac "(abc_step_l (as, lm) (Some (Inc n)))")
+  fix a b
+  assume aexec: "abc_step_l (as, lm) (Some (Inc n)) = (a, b)"
+  then have "\<exists> stp k. steps (Suc 0, l, r) (findnth n @ shift tinc_b (2 * n), 0) stp 
+        = (2*n + 10, Bk # Bk # ires, <b> @ Bk\<up>k) \<and> stp > 0"
+    using assms
+    apply(rule_tac crsp_step_inc_pre, simp_all)
+    done
+  thus "?thesis"
+    using assms aexec
+    apply(erule_tac exE)
+    apply(erule_tac exE)
+    apply(erule_tac conjE)
+    apply(rule_tac x = stp in exI, simp add: ci.simps tm_shift_eq_steps)
+    apply(drule_tac off = "(start_of (layout_of ap) as - Suc 0)" in tm_shift_eq_steps)
+    apply(auto simp: crsp.simps abc_step_l.simps fetch start_of_Suc1)
+    done
+qed
+    
+subsection{* Crsp of Dec n e*}
+declare sete.simps[simp del]
+
+type_synonym dec_inv_t = "(nat * nat list) \<Rightarrow> config \<Rightarrow> cell list \<Rightarrow>  bool"
+
+fun dec_first_on_right_moving :: "nat \<Rightarrow> dec_inv_t"
+  where
+  "dec_first_on_right_moving n (as, lm) (s, l, r) ires = 
+               (\<exists> lm1 lm2 m ml mr rn. lm = lm1 @ [m] @ lm2 \<and> 
+         ml + mr = Suc m \<and> length lm1 = n \<and> ml > 0 \<and> m > 0 \<and>
+             (if lm1 = [] then l = Oc\<up>ml @ Bk # Bk # ires
+                          else  l = Oc\<up>ml @ [Bk] @ <rev lm1> @ Bk # Bk # ires) \<and> 
+    ((r = Oc\<up>mr @ [Bk] @ <lm2> @ Bk\<up>rn) \<or> (r = Oc\<up>mr \<and> lm2 = [])))"
+
+fun dec_on_right_moving :: "dec_inv_t"
+  where
+  "dec_on_right_moving (as, lm) (s, l, r) ires =  
+   (\<exists> lm1 lm2 m ml mr rn. lm = lm1 @ [m] @ lm2 \<and> 
+                             ml + mr = Suc (Suc m) \<and>
+   (if lm1 = [] then l = Oc\<up>ml@ Bk # Bk # ires
+                else  l = Oc\<up>ml @ [Bk] @ <rev lm1> @ Bk # Bk # ires) \<and> 
+   ((r = Oc\<up>mr @ [Bk] @ <lm2> @ Bk\<up>rn) \<or> (r = Oc\<up>mr \<and> lm2 = [])))"
+
+fun dec_after_clear :: "dec_inv_t"
+  where
+  "dec_after_clear (as, lm) (s, l, r) ires = 
+              (\<exists> lm1 lm2 m ml mr rn. lm = lm1 @ [m] @ lm2 \<and> 
+                ml + mr = Suc m \<and> ml = Suc m \<and> r \<noteq> [] \<and> r \<noteq> [] \<and>
+               (if lm1 = [] then l = Oc\<up>ml@ Bk # Bk # ires
+                            else l = Oc\<up>ml @ [Bk] @ <rev lm1> @ Bk # Bk # ires) \<and> 
+               (tl r = Bk # <lm2> @ Bk\<up>rn \<or> tl r = [] \<and> lm2 = []))"
+
+fun dec_after_write :: "dec_inv_t"
+  where
+  "dec_after_write (as, lm) (s, l, r) ires = 
+         (\<exists> lm1 lm2 m ml mr rn. lm = lm1 @ [m] @ lm2 \<and> 
+       ml + mr = Suc m \<and> ml = Suc m \<and> lm2 \<noteq> [] \<and>
+       (if lm1 = [] then l = Bk # Oc\<up>ml @ Bk # Bk # ires
+                    else l = Bk # Oc\<up>ml @ [Bk] @ <rev lm1> @ Bk # Bk # ires) \<and> 
+       tl r = <lm2> @ Bk\<up>rn)"
+
+fun dec_right_move :: "dec_inv_t"
+  where
+  "dec_right_move (as, lm) (s, l, r) ires = 
+        (\<exists> lm1 lm2 m ml mr rn. lm = lm1 @ [m] @ lm2 
+            \<and> ml = Suc m \<and> mr = (0::nat) \<and> 
+              (if lm1 = [] then l = Bk # Oc\<up>ml @ Bk # Bk # ires
+                          else l = Bk # Oc\<up>ml @ [Bk] @ <rev lm1> @ Bk # Bk # ires) 
+           \<and> (r = Bk # <lm2> @ Bk\<up>rn \<or> r = [] \<and> lm2 = []))"
+
+fun dec_check_right_move :: "dec_inv_t"
+  where
+  "dec_check_right_move (as, lm) (s, l, r) ires = 
+        (\<exists> lm1 lm2 m ml mr rn. lm = lm1 @ [m] @ lm2 \<and> 
+           ml = Suc m \<and> mr = (0::nat) \<and> 
+           (if lm1 = [] then l = Bk # Bk # Oc\<up>ml @ Bk # Bk # ires
+                       else l = Bk # Bk # Oc\<up>ml @ [Bk] @ <rev lm1> @ Bk # Bk # ires) \<and> 
+           r = <lm2> @ Bk\<up>rn)"
+
+fun dec_left_move :: "dec_inv_t"
+  where
+  "dec_left_move (as, lm) (s, l, r) ires = 
+    (\<exists> lm1 m rn. (lm::nat list) = lm1 @ [m::nat] \<and>   
+    rn > 0 \<and> 
+   (if lm1 = [] then l = Bk # Oc\<up>Suc m @ Bk # Bk # ires
+    else l = Bk # Oc\<up>Suc m @ Bk # <rev lm1> @ Bk # Bk # ires) \<and> r = Bk\<up>rn)"
+
+declare
+  dec_on_right_moving.simps[simp del] dec_after_clear.simps[simp del] 
+  dec_after_write.simps[simp del] dec_left_move.simps[simp del] 
+  dec_check_right_move.simps[simp del] dec_right_move.simps[simp del] 
+  dec_first_on_right_moving.simps[simp del]
+
+fun inv_locate_n_b :: "inc_inv_t"
+  where
+  "inv_locate_n_b (as, lm) (s, l, r) ires= 
+    (\<exists> lm1 lm2 tn m ml mr rn. lm @ 0\<up>tn = lm1 @ [m] @ lm2 \<and> 
+     length lm1 = s \<and> m + 1 = ml + mr \<and> 
+     ml = 1 \<and> tn = s + 1 - length lm \<and>
+     (if lm1 = [] then l = Oc\<up>ml @ Bk # Bk # ires
+      else l = Oc\<up>ml @ Bk # <rev lm1> @ Bk # Bk # ires) \<and> 
+     (r = Oc\<up>mr @ [Bk] @ <lm2>@ Bk\<up>rn \<or> (lm2 = [] \<and> r = Oc\<up>mr))
+  )"
+(*
+fun dec_inv_1 :: "layout \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> dec_inv_t"
+  where
+  "dec_inv_1 ly n e (as, am) (s, l, r) ires = 
+           (let ss = start_of ly as in
+            let am' = abc_lm_s am n (abc_lm_v am n - Suc 0) in
+            let am'' = abc_lm_s am n (abc_lm_v am n) in
+              if s = start_of ly e then inv_stop (as, am'') (s, l, r) ires
+              else if s = ss then False
+              else if s = ss + 2 * n then 
+                  inv_locate_a (as, am) (n, l, r) ires
+                \<or> inv_locate_a (as, am'') (n, l, r) ires
+              else if s = ss + 2 * n + 1 then 
+                  inv_locate_b (as, am) (n, l, r) ires
+              else if s = ss + 2 * n + 13 then 
+                  inv_on_left_moving (as, am'') (s, l, r) ires
+              else if s = ss + 2 * n + 14 then 
+                  inv_check_left_moving (as, am'') (s, l, r) ires
+              else if s = ss + 2 * n + 15 then 
+                  inv_after_left_moving (as, am'') (s, l, r) ires
+              else False)"
+*)
+
+
+fun dec_inv_1 :: "layout \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> dec_inv_t"
+  where
+  "dec_inv_1 ly n e (as, am) (s, l, r) ires = 
+           (let ss = start_of ly as in
+            let am' = abc_lm_s am n (abc_lm_v am n - Suc 0) in
+            let am'' = abc_lm_s am n (abc_lm_v am n) in
+              if s = start_of ly e then inv_stop (as, am'') (s, l, r) ires
+              else if s = ss then False
+              else if s = ss + 2 * n + 1 then 
+                  inv_locate_b (as, am) (n, l, r) ires
+              else if s = ss + 2 * n + 13 then 
+                  inv_on_left_moving (as, am'') (s, l, r) ires
+              else if s = ss + 2 * n + 14 then 
+                  inv_check_left_moving (as, am'') (s, l, r) ires
+              else if s = ss + 2 * n + 15 then 
+                  inv_after_left_moving (as, am'') (s, l, r) ires
+              else False)"
+
+declare fetch.simps[simp del]
+lemma [simp]:
+  "fetch (ci ly (start_of ly as) (Dec n e)) (Suc (2 * n)) Bk = (W1,  start_of ly as + 2 *n)"
+apply(auto simp: fetch.simps length_ci_dec)
+apply(auto simp: ci.simps nth_append length_findnth sete.simps shift.simps tdec_b_def)
+using startof_not0[of ly as] by simp
+
+lemma [simp]:
+  "fetch (ci ly (start_of ly as) (Dec n e)) (Suc (2 * n)) Oc = (R,  Suc (start_of ly as) + 2 *n)"
+apply(auto simp: fetch.simps length_ci_dec)
+apply(auto simp: ci.simps nth_append length_findnth sete.simps shift.simps tdec_b_def)
+done
+
+lemma [simp]: 
+  "\<lbrakk>r = [] \<or> hd r = Bk; inv_locate_a (as, lm) (n, l, r) ires\<rbrakk>
+    \<Longrightarrow> \<exists>stp la ra.
+  steps (start_of ly as + 2 * n, l, r) (ci ly (start_of ly as) (Dec n e), 
+  start_of ly as - Suc 0) stp = (Suc (start_of ly as + 2 * n), la, ra) \<and>
+  inv_locate_b (as, lm) (n, la, ra) ires"
+apply(rule_tac x = "Suc (Suc 0)" in exI)
+apply(auto simp: steps.simps step.simps length_ci_dec)
+apply(case_tac r, simp_all)
+done
+
+lemma [simp]: 
+  "\<lbrakk>inv_locate_a (as, lm) (n, l, r) ires; r \<noteq> [] \<and> hd r \<noteq> Bk\<rbrakk>
+    \<Longrightarrow> \<exists>stp la ra.
+  steps (start_of ly as + 2 * n, l, r) (ci ly (start_of ly as) (Dec n e), 
+  start_of ly as - Suc 0) stp = (Suc (start_of ly as + 2 * n), la, ra) \<and>
+  inv_locate_b (as, lm) (n, la, ra) ires"
+apply(rule_tac x = "(Suc 0)" in exI, case_tac "hd r", simp_all)
+apply(auto simp: steps.simps step.simps length_ci_dec)
+apply(case_tac r, simp_all)
+done
+
+fun abc_dec_1_stage1:: "config \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat"
+  where
+  "abc_dec_1_stage1 (s, l, r) ss n = 
+       (if s > ss \<and> s \<le> ss + 2*n + 1 then 4
+        else if s = ss + 2 * n + 13 \<or> s = ss + 2*n + 14 then 3
+        else if s = ss + 2*n + 15 then 2
+        else 0)"
+
+fun abc_dec_1_stage2:: "config \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat"
+  where
+  "abc_dec_1_stage2 (s, l, r) ss n = 
+       (if s \<le> ss + 2 * n + 1 then (ss + 2 * n + 16 - s)
+        else if s = ss + 2*n + 13 then length l
+        else if s = ss + 2*n + 14 then length l
+        else 0)"
+
+fun abc_dec_1_stage3 :: "config \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat"
+  where
+  "abc_dec_1_stage3 (s, l, r) ss n  = 
+        (if s \<le> ss + 2*n + 1 then 
+             if (s - ss) mod 2 = 0 then 
+                         if r \<noteq> [] \<and> hd r = Oc then 0 else 1  
+                         else length r
+         else if s = ss + 2 * n + 13 then 
+             if r \<noteq> [] \<and> hd r = Oc then 2 
+             else 1
+         else if s = ss + 2 * n + 14 then 
+             if r \<noteq> [] \<and> hd r = Oc then 3 else 0 
+         else 0)"
+
+fun abc_dec_1_measure :: "(config \<times> nat \<times> nat) \<Rightarrow> (nat \<times> nat \<times> nat)"
+  where
+  "abc_dec_1_measure (c, ss, n) = (abc_dec_1_stage1 c ss n, 
+                   abc_dec_1_stage2 c ss n, abc_dec_1_stage3 c ss n)"
+
+definition abc_dec_1_LE ::
+  "((config \<times> nat \<times>
+  nat) \<times> (config \<times> nat \<times> nat)) set"
+  where "abc_dec_1_LE \<equiv> (inv_image lex_triple abc_dec_1_measure)"
+
+lemma wf_dec_le: "wf abc_dec_1_LE"
+by(auto intro:wf_inv_image simp:abc_dec_1_LE_def lex_triple_def lex_pair_def)
+
+lemma startof_Suc2:
+  "abc_fetch as ap = Some (Dec n e) \<Longrightarrow> 
+        start_of (layout_of ap) (Suc as) = 
+            start_of (layout_of ap) as + 2 * n + 16"
+apply(auto simp: start_of.simps layout_of.simps  
+                 length_of.simps abc_fetch.simps 
+                 take_Suc_conv_app_nth split: if_splits)
+done
+
+lemma start_of_less_2: 
+  "start_of ly e \<le> start_of ly (Suc e)"
+thm take_Suc
+apply(case_tac "e < length ly")
+apply(auto simp: start_of.simps take_Suc take_Suc_conv_app_nth)
+done
+
+lemma start_of_less_1: "start_of ly e \<le> start_of ly (e + d)"
+proof(induct d)
+  case 0 thus "?case" by simp
+next
+  case (Suc d)
+  have "start_of ly e \<le> start_of ly (e + d)"  by fact
+  moreover have "start_of ly (e + d) \<le> start_of ly (Suc (e + d))"
+    by(rule_tac start_of_less_2)
+  ultimately show"?case"
+    by(simp)
+qed
+
+lemma start_of_less: 
+  assumes "e < as"
+  shows "start_of ly e \<le> start_of ly as"
+proof -
+  obtain d where " as = e + d"
+    using assms by (metis less_imp_add_positive)
+  thus "?thesis"
+    by(simp add: start_of_less_1)
+qed
+
+lemma start_of_ge: 
+  assumes fetch: "abc_fetch as ap = Some (Dec n e)"
+  and layout: "ly = layout_of ap"
+  and great: "e > as"
+  shows "start_of ly e \<ge> start_of ly as + 2*n + 16"
+proof(cases "e = Suc as")
+  case True
+  have "e = Suc as" by fact
+  moreover hence "start_of ly (Suc as) = start_of ly as + 2*n + 16"
+    using layout fetch
+    by(simp add: startof_Suc2)
+  ultimately show "?thesis" by (simp)
+next
+  case False
+  have "e \<noteq> Suc as" by fact
+  then have "e > Suc as" using great by arith
+  then have "start_of ly (Suc as) \<le> start_of ly e"
+    by(simp add: start_of_less)
+  moreover have "start_of ly (Suc as) = start_of ly as + 2*n + 16"
+    using layout fetch
+    by(simp add: startof_Suc2)
+  ultimately show "?thesis"
+    by arith
+qed
+    
+lemma [elim]: "\<lbrakk>abc_fetch as ap = Some (Dec n e); as < e; 
+  Suc (start_of (layout_of ap) as + 2 * n) = start_of (layout_of ap) e\<rbrakk> \<Longrightarrow> RR"
+apply(drule_tac start_of_ge, simp_all)
+apply(auto)
+done
+
+lemma [elim]: "\<lbrakk>abc_fetch as ap = Some (Dec n e); as > e;
+  Suc (start_of (layout_of ap) as + 2 * n) = start_of (layout_of ap) e\<rbrakk> \<Longrightarrow> RR"
+apply(drule_tac ly = "layout_of ap" in start_of_less[of])
+apply(arith)
+done
+
+lemma [elim]: "\<lbrakk>abc_fetch as ap = Some (Dec n e);
+  Suc (start_of (layout_of ap) as + 2 * n) = start_of (layout_of ap) e\<rbrakk> \<Longrightarrow> RR"
+apply(subgoal_tac "as = e \<or> as < e \<or> as > e", auto)
+done
+
+lemma [simp]:"fetch (ci (ly) (start_of ly as) (Dec n e)) (Suc (2 * n))  Oc
+  = (R, start_of ly as + 2*n + 1)"
+apply(auto simp: ci.simps findnth.simps fetch.simps
+                  nth_of.simps shift.simps nth_append tdec_b_def length_findnth sete.simps)
+done
+
+lemma [simp]: "(start_of ly as = 0) = False"
+apply(simp add: start_of.simps)
+done
+
+lemma [simp]: "fetch (ci (ly) 
+  (start_of ly as) (Dec n e)) (Suc (2 * n))  Bk
+  = (W1, start_of ly as + 2*n)"
+apply(auto simp: ci.simps findnth.simps fetch.simps
+                  nth_of.simps shift.simps nth_append tdec_b_def length_findnth sete.simps)
+done
+
+lemma [simp]: 
+  "fetch (ci (ly) 
+                (start_of ly as) (Dec n e)) (Suc (Suc (2 * n)))  Oc
+      = (R, start_of ly as + 2*n + 2)"
+apply(auto simp: ci.simps findnth.simps fetch.simps
+                  nth_of.simps shift.simps nth_append tdec_b_def length_findnth sete.simps)
+done
+
+
+lemma [simp]: "fetch (ci (ly) 
+                  (start_of ly as) (Dec n e)) (Suc (Suc (2 * n))) Bk
+      = (L, start_of ly as + 2*n + 13)"
+apply(auto simp: ci.simps findnth.simps fetch.simps
+                  nth_of.simps shift.simps nth_append tdec_b_def length_findnth sete.simps)
+done
+
+
+lemma [simp]: "fetch (ci (ly) 
+             (start_of ly as) (Dec n e)) (Suc (Suc (Suc (2 * n))))  Oc
+     = (R, start_of ly as + 2*n + 2)"
+apply(auto simp: ci.simps findnth.simps fetch.simps
+                  nth_of.simps shift.simps nth_append tdec_b_def length_findnth sete.simps)
+done
+
+
+lemma [simp]: "fetch (ci (ly) (start_of ly as) (Dec n e)) 
+                             (Suc (Suc (Suc (2 * n))))  Bk
+     = (L, start_of ly as + 2*n + 3)"
+apply(auto simp: ci.simps findnth.simps fetch.simps
+                  nth_of.simps shift.simps nth_append tdec_b_def length_findnth sete.simps)
+done
+
+lemma [simp]:
+     "fetch (ci (ly) 
+                      (start_of ly as) (Dec n e)) (2 * n + 4) Oc
+    = (W0, start_of ly as + 2*n + 3)"
+apply(subgoal_tac "2*n + 4 = Suc (2*n + 3)", simp only: fetch.simps)
+apply(auto simp: ci.simps findnth.simps fetch.simps
+                  nth_of.simps shift.simps nth_append tdec_b_def length_findnth sete.simps)
+done
+
+lemma [simp]: "fetch (ci (ly) 
+                   (start_of ly as) (Dec n e)) (2 * n + 4) Bk
+    = (R, start_of ly as + 2*n + 4)"
+apply(subgoal_tac "2*n + 4 = Suc (2*n + 3)", simp only: fetch.simps)
+apply(auto simp: ci.simps findnth.simps fetch.simps
+                  nth_of.simps shift.simps nth_append tdec_b_def length_findnth sete.simps)
+done
+
+lemma [simp]:"fetch (ci (ly) 
+                          (start_of ly as) (Dec n e)) (2 * n + 5) Bk
+    = (R, start_of ly as + 2*n + 5)"
+apply(subgoal_tac "2*n + 5 = Suc (2*n + 4)", simp only: fetch.simps)
+apply(auto simp: ci.simps findnth.simps fetch.simps
+                  nth_of.simps shift.simps nth_append tdec_b_def length_findnth sete.simps)
+done
+
+
+lemma [simp]: 
+  "fetch (ci (ly)
+                (start_of ly as) (Dec n e)) (2 * n + 6) Bk
+    = (L, start_of ly as + 2*n + 6)"
+apply(subgoal_tac "2*n + 6 = Suc (2*n + 5)", simp only: fetch.simps)
+apply(auto simp: ci.simps findnth.simps fetch.simps
+                  nth_of.simps shift.simps nth_append tdec_b_def length_findnth sete.simps)
+done
+
+lemma [simp]: 
+  "fetch (ci (ly) (start_of ly as) 
+                      (Dec n e)) (2 * n + 6) Oc
+    = (L, start_of ly as + 2*n + 7)"
+apply(subgoal_tac "2*n + 6 = Suc (2*n + 5)", simp only: fetch.simps)
+apply(auto simp: ci.simps findnth.simps fetch.simps
+                  nth_of.simps shift.simps nth_append tdec_b_def length_findnth sete.simps)
+done
+
+lemma [simp]:"fetch (ci (ly) 
+             (start_of ly as) (Dec n e)) (2 * n + 7) Bk
+    = (L, start_of ly as + 2*n + 10)"
+apply(subgoal_tac "2*n + 7 = Suc (2*n + 6)", simp only: fetch.simps)
+apply(auto simp: ci.simps findnth.simps fetch.simps
+                  nth_of.simps shift.simps nth_append tdec_b_def length_findnth sete.simps)
+done
+
+lemma [simp]:
+  "fetch (ci (ly) 
+                   (start_of ly as) (Dec n e)) (2 * n + 8) Bk
+    = (W1, start_of ly as + 2*n + 7)"
+apply(subgoal_tac "2*n + 8 = Suc (2*n + 7)", simp only: fetch.simps)
+apply(auto simp: ci.simps findnth.simps fetch.simps
+                  nth_of.simps shift.simps nth_append tdec_b_def length_findnth sete.simps)
+done
+
+
+lemma [simp]: 
+  "fetch (ci (ly) 
+                   (start_of ly as) (Dec n e)) (2 * n + 8) Oc
+    = (R, start_of ly as + 2*n + 8)"
+apply(subgoal_tac "2*n + 8 = Suc (2*n + 7)", simp only: fetch.simps)
+apply(auto simp: ci.simps findnth.simps fetch.simps
+                  nth_of.simps shift.simps nth_append tdec_b_def length_findnth sete.simps)
+done
+
+lemma [simp]: 
+  "fetch (ci (ly) 
+  (start_of ly as) (Dec n e)) (2 * n + 9) Bk
+  = (L, start_of ly as + 2*n + 9)"
+apply(subgoal_tac "2*n + 9 = Suc (2*n + 8)", simp only: fetch.simps)
+apply(auto simp: ci.simps findnth.simps fetch.simps
+                  nth_of.simps shift.simps nth_append tdec_b_def length_findnth sete.simps)
+done
+
+lemma [simp]: 
+  "fetch (ci (ly) 
+  (start_of ly as) (Dec n e)) (2 * n + 9) Oc
+  = (R, start_of ly as + 2*n + 8)"
+apply(subgoal_tac "2*n + 9 = Suc (2*n + 8)", simp only: fetch.simps)
+apply(auto simp: ci.simps findnth.simps fetch.simps
+                  nth_of.simps shift.simps nth_append tdec_b_def length_findnth sete.simps)
+done
+
+
+lemma [simp]: 
+  "fetch (ci (ly) 
+  (start_of ly as) (Dec n e)) (2 * n + 10) Bk
+  = (R, start_of ly as + 2*n + 4)" 
+apply(subgoal_tac "2*n + 10 = Suc (2*n + 9)", simp only: fetch.simps)
+apply(auto simp: ci.simps findnth.simps fetch.simps
+                  nth_of.simps shift.simps nth_append tdec_b_def length_findnth sete.simps)
+done
+
+lemma [simp]: "fetch (ci (ly) 
+             (start_of ly as) (Dec n e)) (2 * n + 10) Oc
+    = (W0, start_of ly as + 2*n + 9)"
+apply(subgoal_tac "2*n + 10 = Suc (2*n + 9)", simp only: fetch.simps)
+apply(auto simp: ci.simps findnth.simps fetch.simps
+                  nth_of.simps shift.simps nth_append tdec_b_def length_findnth sete.simps)
+done
+
+
+lemma [simp]: 
+  "fetch (ci (ly) 
+  (start_of ly as) (Dec n e)) (2 * n + 11) Oc
+  = (L, start_of ly as + 2*n + 10)"
+apply(subgoal_tac "2*n + 11 = Suc (2*n + 10)", simp only: fetch.simps)
+apply(auto simp: ci.simps findnth.simps fetch.simps
+                  nth_of.simps shift.simps nth_append tdec_b_def length_findnth sete.simps)
+done
+
+
+lemma [simp]: 
+  "fetch (ci (ly) 
+  (start_of ly as) (Dec n e)) (2 * n + 11) Bk
+  = (L, start_of ly as + 2*n + 11)"
+apply(subgoal_tac "2*n + 11 = Suc (2*n + 10)", simp only: fetch.simps)
+apply(auto simp: ci.simps findnth.simps fetch.simps
+                  nth_of.simps shift.simps nth_append tdec_b_def length_findnth sete.simps)
+done
+
+lemma [simp]:
+  "fetch (ci (ly) 
+  (start_of ly as) (Dec n e)) (2 * n + 12) Oc
+  = (L, start_of ly as + 2*n + 10)"
+apply(subgoal_tac "2*n + 12 = Suc (2*n + 11)", simp only: fetch.simps)
+apply(auto simp: ci.simps findnth.simps fetch.simps
+                  nth_of.simps shift.simps nth_append tdec_b_def length_findnth sete.simps)
+done
+
+
+lemma [simp]: 
+  "fetch (ci (ly) 
+  (start_of ly as) (Dec n e)) (2 * n + 12) Bk
+  = (R, start_of ly as + 2*n + 12)"
+apply(subgoal_tac "2*n + 12 = Suc (2*n + 11)", simp only: fetch.simps)
+apply(auto simp: ci.simps findnth.simps fetch.simps
+                  nth_of.simps shift.simps nth_append tdec_b_def length_findnth sete.simps)
+done
+
+lemma [simp]: 
+  "fetch (ci (ly) 
+  (start_of ly as) (Dec n e)) (2 * n + 13) Bk
+  = (R, start_of ly as + 2*n + 16)"
+apply(subgoal_tac "2*n + 13 = Suc (2*n + 12)", simp only: fetch.simps)
+apply(auto simp: ci.simps findnth.simps fetch.simps
+                  nth_of.simps shift.simps nth_append tdec_b_def length_findnth sete.simps)
+done
+
+
+lemma [simp]: 
+  "fetch (ci (ly) 
+  (start_of ly as) (Dec n e)) (14 + 2 * n) Oc
+  = (L, start_of ly as + 2*n + 13)"
+apply(subgoal_tac "14 + 2*n = Suc (2*n + 13)", simp only: fetch.simps)
+apply(auto simp: ci.simps findnth.simps fetch.simps
+                  nth_of.simps shift.simps nth_append tdec_b_def length_findnth sete.simps)
+done
+
+lemma [simp]: 
+  "fetch (ci (ly) 
+  (start_of ly as) (Dec n e)) (14 + 2 * n) Bk
+  = (L, start_of ly as + 2*n + 14)"
+apply(subgoal_tac "14 + 2*n = Suc (2*n + 13)", simp only: fetch.simps)
+apply(auto simp: ci.simps findnth.simps fetch.simps
+                  nth_of.simps shift.simps nth_append tdec_b_def length_findnth sete.simps)
+done
+
+lemma [simp]: 
+  "fetch (ci (ly) 
+  (start_of ly as) (Dec n e)) (15 + 2 * n)  Oc
+  = (L, start_of ly as + 2*n + 13)"
+apply(subgoal_tac "15 + 2*n = Suc (2*n + 14)", simp only: fetch.simps)
+apply(auto simp: ci.simps findnth.simps fetch.simps
+                  nth_of.simps shift.simps nth_append tdec_b_def length_findnth sete.simps)
+done
+
+lemma [simp]: 
+  "fetch (ci (ly) 
+  (start_of ly as) (Dec n e)) (15 + 2 * n)  Bk
+ = (R, start_of ly as + 2*n + 15)"
+apply(subgoal_tac "15 + 2*n = Suc (2*n + 14)", simp only: fetch.simps)
+apply(auto simp: ci.simps findnth.simps fetch.simps
+                  nth_of.simps shift.simps nth_append tdec_b_def length_findnth sete.simps)
+done
+
+lemma [simp]: 
+  "abc_fetch as aprog = Some (Dec n e) \<Longrightarrow> 
+     fetch (ci (ly) (start_of (ly) as) 
+              (Dec n e)) (16 + 2 * n)  Bk
+ = (R, start_of (ly) e)"
+apply(subgoal_tac "16 + 2*n = Suc (2*n + 15)", simp only: fetch.simps)
+apply(auto simp: ci.simps findnth.simps fetch.simps
+                  nth_of.simps shift.simps nth_append tdec_b_def length_findnth sete.simps)
+done
+
+declare dec_inv_1.simps[simp del]
+
+
+lemma [simp]: 
+ "\<lbrakk>abc_fetch as aprog = Some (Dec n e); ly = layout_of aprog\<rbrakk>
+   \<Longrightarrow> (start_of ly e \<noteq> Suc (start_of ly as + 2 * n) \<and>
+        start_of ly e \<noteq> Suc (Suc (start_of ly as + 2 * n)) \<and>  
+        start_of ly e \<noteq> start_of ly as + 2 * n + 3 \<and> 
+        start_of ly e \<noteq> start_of ly as + 2 * n + 4 \<and>
+        start_of ly e \<noteq> start_of ly as + 2 * n + 5 \<and> 
+        start_of ly e \<noteq> start_of ly as + 2 * n + 6 \<and> 
+        start_of ly e \<noteq> start_of ly as + 2 * n + 7 \<and>
+        start_of ly e \<noteq> start_of ly as + 2 * n + 8 \<and> 
+        start_of ly e \<noteq> start_of ly as + 2 * n + 9 \<and> 
+        start_of ly e \<noteq> start_of ly as + 2 * n + 10 \<and>
+        start_of ly e \<noteq> start_of ly as + 2 * n + 11 \<and> 
+        start_of ly e \<noteq> start_of ly as + 2 * n + 12 \<and> 
+        start_of ly e \<noteq> start_of ly as + 2 * n + 13 \<and>
+        start_of ly e \<noteq> start_of ly as + 2 * n + 14 \<and> 
+        start_of ly e \<noteq> start_of ly as + 2 * n + 15)"
+using start_of_ge[of as aprog n e ly] start_of_less[of e as ly]
+apply(case_tac "e < as", simp)
+apply(case_tac "e = as", simp, simp)
+done
+
+lemma [simp]: "\<lbrakk>abc_fetch as aprog = Some (Dec n e); ly = layout_of aprog\<rbrakk>
+      \<Longrightarrow> (Suc (start_of ly as + 2 * n) \<noteq> start_of ly e \<and>
+          Suc (Suc (start_of ly as + 2 * n)) \<noteq> start_of ly e \<and> 
+          start_of ly as + 2 * n + 3 \<noteq> start_of ly e \<and> 
+          start_of ly as + 2 * n + 4 \<noteq> start_of ly e \<and>
+          start_of ly as + 2 * n + 5 \<noteq>start_of ly e \<and> 
+          start_of ly as + 2 * n + 6 \<noteq> start_of ly e \<and>
+          start_of ly as + 2 * n + 7 \<noteq> start_of ly e \<and> 
+          start_of ly as + 2 * n + 8 \<noteq> start_of ly e \<and> 
+          start_of ly as + 2 * n + 9 \<noteq> start_of ly e \<and> 
+          start_of ly as + 2 * n + 10 \<noteq> start_of ly e \<and>
+          start_of ly as + 2 * n + 11 \<noteq> start_of ly e \<and> 
+          start_of ly as + 2 * n + 12 \<noteq> start_of ly e \<and> 
+          start_of ly as + 2 * n + 13 \<noteq> start_of ly e \<and> 
+          start_of ly as + 2 * n + 14 \<noteq> start_of ly e \<and> 
+          start_of ly as + 2 * n + 15 \<noteq> start_of ly e)"
+using start_of_ge[of as aprog n e ly] start_of_less[of e as ly]
+apply(case_tac "e < as", simp, simp)
+apply(case_tac "e = as", simp, simp)
+done
+
+lemma [simp]: "inv_locate_b (as, lm) (n, [], []) ires = False"
+apply(auto simp: inv_locate_b.simps in_middle.simps split: if_splits)
+done
+
+lemma [simp]: "inv_locate_b (as, lm) (n, [], Bk # list) ires = False"
+apply(auto simp: inv_locate_b.simps in_middle.simps split: if_splits)
+done
+
+(*
+
+lemma  inv_locate_b_2_on_left_moving_b[simp]: 
+   "inv_locate_b (as, am) (n, l, []) ires
+     \<Longrightarrow> inv_on_left_moving (as, 
+                  abc_lm_s am n (abc_lm_v am n)) (s, [], [Bk]) ires"
+apply(auto simp: inv_locate_b.simps inv_on_left_moving.simps inv_on_left_moving_in_middle_B.simps
+                 in_middle.simps split: if_splits)
+apply(drule_tac length_equal, simp)
+
+apply(insert inv_locate_b_2_on_left_moving[of as am n l "[]" ires s])
+apply(simp only: inv_on_left_moving.simps, simp)
+apply(subgoal_tac "\<not> inv_on_left_moving_in_middle_B 
+         (as, abc_lm_s am n (abc_lm_v am n)) (s, tl l, [hd l]) ires", simp)
+*)
+
+(*
+lemma [simp]:
+  "inv_locate_b (as, am) (n, l, []) ires; l \<noteq> []\<rbrakk>
+ \<Longrightarrow> inv_on_left_moving (as, abc_lm_s am n 
+                  (abc_lm_v am n)) (s, tl l, [hd l]) ires"
+apply(auto simp: inv_locate_b.simps inv_on_left_moving.simps inv_on_left_moving_in_middle_B.simps
+                 in_middle.simps split: if_splits)
+apply(drule_tac length_equal, simp)
+
+apply(insert inv_locate_b_2_on_left_moving[of as am n l "[]" ires s])
+apply(simp only: inv_on_left_moving.simps, simp)
+apply(subgoal_tac "\<not> inv_on_left_moving_in_middle_B 
+         (as, abc_lm_s am n (abc_lm_v am n)) (s, tl l, [hd l]) ires", simp)
+
+apply(insert inv_locate_b_2_on_left_moving[of as am n l "[]" ires s])
+apply(simp only: inv_on_left_moving.simps, simp)
+apply(subgoal_tac "\<not> inv_on_left_moving_in_middle_B 
+         (as, abc_lm_s am n (abc_lm_v am n)) (s, tl l, [hd l]) ires", simp)
+apply(simp only: inv_on_left_moving_norm.simps)
+apply(erule_tac exE)+
+apply(erule_tac conjE)+
+apply(rule_tac x = lm1 in exI, rule_tac x = lm2 in exI, 
+      rule_tac x = m in exI, rule_tac x = ml in exI, 
+      rule_tac x = mr in exI, simp)
+apply(case_tac mr, simp, simp, case_tac nat, auto intro: nil_2_nil)
+done
+*)
+
+lemma [simp]: 
+ "\<lbrakk>dec_first_on_right_moving n (as, am) (s, aaa, Oc # xs) ires\<rbrakk>
+   \<Longrightarrow> dec_first_on_right_moving n (as, am) (s', Oc # aaa, xs) ires"
+apply(simp only: dec_first_on_right_moving.simps)
+apply(erule exE)+
+apply(rule_tac x = lm1 in exI, rule_tac x = lm2 in exI, 
+      rule_tac x = m in exI, simp)
+apply(rule_tac x = "Suc ml" in exI, 
+      rule_tac x = "mr - 1" in exI, auto)
+apply(case_tac [!] mr, auto)
+done
+
+lemma [simp]: 
+  "dec_first_on_right_moving n (as, am) (s, l, Bk # xs) ires \<Longrightarrow> l \<noteq> []"
+apply(auto simp: dec_first_on_right_moving.simps split: if_splits)
+done
+
+lemma [elim]: 
+  "\<lbrakk>\<not> length lm1 < length am; 
+    am @ replicate (length lm1 - length am) 0 @ [0::nat] = 
+                                                lm1 @ m # lm2;
+    0 < m\<rbrakk>
+   \<Longrightarrow> RR"
+apply(subgoal_tac "lm2 = []", simp)
+apply(drule_tac length_equal, simp)
+done
+
+lemma [simp]: 
+ "\<lbrakk>dec_first_on_right_moving n (as, 
+                   abc_lm_s am n (abc_lm_v am n)) (s, l, Bk # xs) ires\<rbrakk>
+\<Longrightarrow> dec_after_clear (as, abc_lm_s am n 
+                 (abc_lm_v am n - Suc 0)) (s', tl l, hd l # Bk # xs) ires"
+apply(simp only: dec_first_on_right_moving.simps 
+                 dec_after_clear.simps abc_lm_s.simps abc_lm_v.simps)
+apply(erule_tac exE)+
+apply(case_tac "n < length am")
+apply(rule_tac x = lm1 in exI, rule_tac x = lm2 in exI, 
+      rule_tac x = "m - 1" in exI, auto simp: )
+apply(case_tac [!] mr, auto)
+done
+
+lemma [simp]: 
+ "\<lbrakk>dec_first_on_right_moving n (as, 
+                   abc_lm_s am n (abc_lm_v am n)) (s, l, []) ires\<rbrakk>
+\<Longrightarrow> (l = [] \<longrightarrow> dec_after_clear (as, 
+             abc_lm_s am n (abc_lm_v am n - Suc 0)) (s', [], [Bk]) ires) \<and>
+    (l \<noteq> [] \<longrightarrow> dec_after_clear (as, abc_lm_s am n 
+                      (abc_lm_v am n - Suc 0)) (s', tl l, [hd l]) ires)"
+apply(subgoal_tac "l \<noteq> []", 
+      simp only: dec_first_on_right_moving.simps 
+                 dec_after_clear.simps abc_lm_s.simps abc_lm_v.simps)
+apply(erule_tac exE)+
+apply(case_tac "n < length am", simp)
+apply(rule_tac x = lm1 in exI, rule_tac x = "m - 1" in exI, auto)
+apply(case_tac [1-2] m, auto)
+apply(auto simp: dec_first_on_right_moving.simps split: if_splits)
+done
+
+lemma [simp]: "\<lbrakk>dec_after_clear (as, am) (s, l, Oc # r) ires\<rbrakk>
+                \<Longrightarrow> dec_after_clear (as, am) (s', l, Bk # r) ires"
+apply(auto simp: dec_after_clear.simps)
+done
+
+lemma [simp]: "\<lbrakk>dec_after_clear (as, am) (s, l, Bk # r) ires\<rbrakk>
+                \<Longrightarrow> dec_right_move (as, am) (s', Bk # l, r) ires"
+apply(auto simp: dec_after_clear.simps dec_right_move.simps split: if_splits)
+done
+
+lemma [simp]: "\<lbrakk>dec_after_clear (as, am) (s, l, []) ires\<rbrakk>
+             \<Longrightarrow> dec_right_move (as, am) (s', Bk # l, []) ires"
+apply(auto simp: dec_after_clear.simps dec_right_move.simps )
+done
+
+lemma [simp]: "\<lbrakk>dec_after_clear (as, am) (s, l, []) ires\<rbrakk>
+             \<Longrightarrow> dec_right_move (as, am) (s', Bk # l, [Bk]) ires"
+apply(auto simp: dec_after_clear.simps dec_right_move.simps split: if_splits)
+done
+
+lemma [simp]:"dec_right_move (as, am) (s, l, Oc # r) ires = False"
+apply(auto simp: dec_right_move.simps)
+done
+              
+lemma dec_right_move_2_check_right_move[simp]:
+     "\<lbrakk>dec_right_move (as, am) (s, l, Bk # r) ires\<rbrakk>
+      \<Longrightarrow> dec_check_right_move (as, am) (s', Bk # l, r) ires"
+apply(auto simp: dec_right_move.simps dec_check_right_move.simps split: if_splits)
+done
+
+lemma [simp]: "(<lm::nat list> = []) = (lm = [])"
+apply(case_tac lm, simp_all add: tape_of_nl_cons)
+done
+
+lemma [simp]: 
+ "dec_right_move (as, am) (s, l, []) ires= 
+  dec_right_move (as, am) (s, l, [Bk]) ires"
+apply(simp add: dec_right_move.simps)
+done
+
+lemma [simp]: "\<lbrakk>dec_right_move (as, am) (s, l, []) ires\<rbrakk>
+             \<Longrightarrow> dec_check_right_move (as, am) (s, Bk # l, []) ires"
+apply(insert dec_right_move_2_check_right_move[of as am s l "[]" s'], 
+      simp)
+done
+
+lemma [simp]: "dec_check_right_move (as, am) (s, l, r) ires\<Longrightarrow> l \<noteq> []"
+apply(auto simp: dec_check_right_move.simps split: if_splits)
+done
+ 
+lemma [simp]: "\<lbrakk>dec_check_right_move (as, am) (s, l, Oc # r) ires\<rbrakk>
+             \<Longrightarrow> dec_after_write (as, am) (s', tl l, hd l # Oc # r) ires"
+apply(auto simp: dec_check_right_move.simps dec_after_write.simps)
+apply(rule_tac x = lm1 in exI, rule_tac x = lm2 in exI, 
+      rule_tac x = m in exI, auto)
+done
+
+
+
+lemma [simp]: "\<lbrakk>dec_check_right_move (as, am) (s, l, Bk # r) ires\<rbrakk>
+                \<Longrightarrow> dec_left_move (as, am) (s', tl l, hd l # Bk # r) ires"
+apply(auto simp: dec_check_right_move.simps 
+                 dec_left_move.simps inv_after_move.simps)
+apply(rule_tac x = lm1 in exI, rule_tac x = m in exI, auto split: if_splits)
+apply(case_tac [!] lm2, simp_all add: tape_of_nl_cons split: if_splits)
+apply(rule_tac [!] x = "(Suc rn)" in exI, simp_all)
+done
+
+lemma [simp]: "\<lbrakk>dec_check_right_move (as, am) (s, l, []) ires\<rbrakk>
+             \<Longrightarrow> dec_left_move (as, am) (s', tl l, [hd l]) ires"
+apply(auto simp: dec_check_right_move.simps 
+                 dec_left_move.simps inv_after_move.simps)
+apply(rule_tac x = lm1 in exI, rule_tac x = m in exI, auto)
+done
+
+lemma [simp]: "dec_left_move (as, am) (s, aaa, Oc # xs) ires = False"
+apply(auto simp: dec_left_move.simps inv_after_move.simps)
+done
+
+lemma [simp]: "dec_left_move (as, am) (s, l, r) ires
+             \<Longrightarrow> l \<noteq> []"
+apply(auto simp: dec_left_move.simps split: if_splits)
+done
+
+lemma [simp]: "inv_on_left_moving_in_middle_B (as, [m])
+  (s', Oc # Oc\<up>m @ Bk # Bk # ires, Bk # Bk\<up>rn) ires"
+apply(simp add: inv_on_left_moving_in_middle_B.simps)
+apply(rule_tac x = "[m]" in exI, auto)
+done
+
+lemma [simp]: "inv_on_left_moving_in_middle_B (as, [m])
+  (s', Oc # Oc\<up>m @ Bk # Bk # ires, [Bk]) ires"
+apply(simp add: inv_on_left_moving_in_middle_B.simps)
+done
+
+
+lemma [simp]: "lm1 \<noteq> [] \<Longrightarrow> 
+  inv_on_left_moving_in_middle_B (as, lm1 @ [m]) (s', 
+  Oc # Oc\<up>m @ Bk # <rev lm1> @ Bk # Bk # ires, Bk # Bk\<up>rn) ires"
+apply(simp only: inv_on_left_moving_in_middle_B.simps)
+apply(rule_tac x = "lm1 @ [m ]" in exI, rule_tac x = "[]" in exI, simp)
+apply(simp add: tape_of_nl_cons split: if_splits)
+done
+
+lemma [simp]: "lm1 \<noteq> [] \<Longrightarrow> 
+  inv_on_left_moving_in_middle_B (as, lm1 @ [m]) (s', 
+  Oc # Oc\<up> m @ Bk # <rev lm1> @ Bk # Bk # ires, [Bk]) ires"
+apply(simp only: inv_on_left_moving_in_middle_B.simps)
+apply(rule_tac x = "lm1 @ [m ]" in exI, rule_tac x = "[]" in exI, simp)
+apply(simp add: tape_of_nl_cons split: if_splits)
+done
+
+lemma [simp]: "dec_left_move (as, am) (s, l, Bk # r) ires
+       \<Longrightarrow> inv_on_left_moving (as, am) (s', tl l, hd l # Bk # r) ires"
+apply(auto simp: dec_left_move.simps inv_on_left_moving.simps split: if_splits)
+done
+
+(*
+lemma [simp]: "inv_on_left_moving_in_middle_B (as, lm1 @ [m]) 
+                        (s', Oc # Oc\<^bsup>m\<^esup> @ Bk # <rev lm1> @ Bk\<^bsup>ln\<^esup>, [Bk])  ires"
+apply(auto simp: inv_on_left_moving_in_middle_B.simps)
+apply(rule_tac x = "lm1 @ [m]" in exI, rule_tac x = "[]" in exI, auto)
+done
+*)
+
+lemma [simp]: "dec_left_move (as, am) (s, l, []) ires
+             \<Longrightarrow> inv_on_left_moving (as, am) (s', tl l, [hd l]) ires"
+apply(auto simp: dec_left_move.simps inv_on_left_moving.simps split: if_splits)
+done
+
+lemma [simp]: "dec_after_write (as, am) (s, l, Oc # r) ires
+       \<Longrightarrow> dec_on_right_moving (as, am) (s', Oc # l, r) ires"
+apply(auto simp: dec_after_write.simps dec_on_right_moving.simps)
+apply(rule_tac x = "lm1 @ [m]" in exI, rule_tac x = "tl lm2" in exI, 
+      rule_tac x = "hd lm2" in exI, simp)
+apply(rule_tac x = "Suc 0" in exI,rule_tac x =  "Suc (hd lm2)" in exI)
+apply(case_tac lm2, auto split: if_splits simp: tape_of_nl_cons)
+done
+
+lemma [simp]: "dec_after_write (as, am) (s, l, Bk # r) ires
+       \<Longrightarrow> dec_after_write (as, am) (s', l, Oc # r) ires"
+apply(auto simp: dec_after_write.simps)
+done
+
+lemma [simp]: "dec_after_write (as, am) (s, aaa, []) ires
+             \<Longrightarrow> dec_after_write (as, am) (s', aaa, [Oc]) ires"
+apply(auto simp: dec_after_write.simps)
+done
+
+lemma [simp]: "dec_on_right_moving (as, am) (s, l, Oc # r) ires
+       \<Longrightarrow> dec_on_right_moving (as, am) (s', Oc # l, r) ires"
+apply(simp only: dec_on_right_moving.simps)
+apply(erule_tac exE)+
+apply(erule conjE)+
+apply(rule_tac x = lm1 in exI, rule_tac x = lm2 in exI,
+      rule_tac x = "m" in exI, rule_tac x = "Suc ml" in exI, 
+      rule_tac x = "mr - 1" in exI, simp)
+apply(case_tac mr, auto)
+done
+
+lemma [simp]: "dec_on_right_moving (as, am) (s, l, r) ires\<Longrightarrow>  l \<noteq> []"
+apply(auto simp: dec_on_right_moving.simps split: if_splits)
+done
+
+lemma [simp]: "dec_on_right_moving (as, am) (s, l, Bk # r) ires
+      \<Longrightarrow>  dec_after_clear (as, am) (s', tl l, hd l # Bk # r) ires"
+apply(auto simp: dec_on_right_moving.simps dec_after_clear.simps)
+apply(case_tac [!] mr, auto split: if_splits)
+done
+
+lemma [simp]: "dec_on_right_moving (as, am) (s, l, []) ires
+             \<Longrightarrow> dec_after_clear (as, am) (s', tl l, [hd l]) ires"
+apply(auto simp: dec_on_right_moving.simps dec_after_clear.simps)
+apply(simp_all split: if_splits)
+apply(rule_tac x = lm1 in exI, simp)
+done
+
+lemma [simp]: 
+ "inv_stop (as, abc_lm_s am n (abc_lm_v am n)) (s, l, r) ires \<Longrightarrow> l \<noteq> []"
+apply(auto simp: inv_stop.simps)
+done
+
+lemma dec_false_1[simp]:
+ "\<lbrakk>abc_lm_v am n = 0; inv_locate_b (as, am) (n, aaa, Oc # xs) ires\<rbrakk>
+  \<Longrightarrow> False"
+apply(auto simp: inv_locate_b.simps in_middle.simps)
+apply(case_tac "length lm1 \<ge> length am", auto)
+apply(subgoal_tac "lm2 = []", simp, subgoal_tac "m = 0", simp)
+apply(case_tac mr, auto simp: )
+apply(subgoal_tac "Suc (length lm1) - length am = 
+                   Suc (length lm1 - length am)", 
+      simp add: exp_ind del: replicate.simps, simp)
+apply(drule_tac xs = "am @ replicate (Suc (length lm1) - length am) 0"
+                and ys = "lm1 @ m # lm2" in length_equal, simp)
+apply(case_tac mr, auto simp: abc_lm_v.simps)
+apply(case_tac "mr = 0", simp_all split: if_splits)
+apply(subgoal_tac "Suc (length lm1) - length am = 
+                       Suc (length lm1 - length am)", 
+      simp add: exp_ind del: replicate.simps, simp)
+done
+
+lemma [simp]: 
+ "\<lbrakk>inv_locate_b (as, am) (n, aaa, Bk # xs) ires; 
+   abc_lm_v am n = 0\<rbrakk>
+   \<Longrightarrow> inv_on_left_moving (as, abc_lm_s am n 0) 
+                         (s, tl aaa, hd aaa # Bk # xs) ires"
+apply(simp add: inv_on_left_moving.simps)
+apply(simp only: inv_locate_b.simps in_middle.simps) 
+apply(erule_tac exE)+
+apply(simp add: inv_on_left_moving.simps)
+apply(subgoal_tac "\<not> inv_on_left_moving_in_middle_B 
+         (as, abc_lm_s am n 0) (s, tl aaa, hd aaa # Bk # xs) ires", simp)
+apply(simp only: inv_on_left_moving_norm.simps)
+apply(erule_tac conjE)+
+apply(rule_tac x = lm1 in exI, rule_tac x = lm2 in exI, 
+      rule_tac x =  m in exI, rule_tac x = m in exI, 
+      rule_tac x = "Suc 0" in exI, simp add: abc_lm_s.simps)
+apply(case_tac mr, simp_all, auto simp: abc_lm_v.simps)
+apply(simp only: exp_ind[THEN sym] replicate_Suc Nat.Suc_diff_le)
+apply(auto simp: inv_on_left_moving_in_middle_B.simps split: if_splits)
+done
+
+
+lemma [simp]:
+ "\<lbrakk>abc_lm_v am n = 0; inv_locate_b (as, am) (n, aaa, []) ires\<rbrakk>
+   \<Longrightarrow> inv_on_left_moving (as, abc_lm_s am n 0) (s, tl aaa, [hd aaa]) ires"
+apply(simp add: inv_on_left_moving.simps)
+apply(simp only: inv_locate_b.simps in_middle.simps) 
+apply(erule_tac exE)+
+apply(simp add: inv_on_left_moving.simps)
+apply(subgoal_tac "\<not> inv_on_left_moving_in_middle_B 
+         (as, abc_lm_s am n 0) (s, tl aaa, [hd aaa]) ires", simp)
+apply(simp only: inv_on_left_moving_norm.simps)
+apply(erule_tac conjE)+
+apply(rule_tac x = lm1 in exI, rule_tac x = lm2 in exI, 
+      rule_tac x =  m in exI, rule_tac x = m in exI, 
+      rule_tac x = "Suc 0" in exI, simp add: abc_lm_s.simps)
+apply(case_tac mr, simp_all, auto simp: abc_lm_v.simps)
+apply(simp_all only: exp_ind Nat.Suc_diff_le del: replicate_Suc, simp_all)
+apply(auto simp: inv_on_left_moving_in_middle_B.simps split: if_splits)
+apply(case_tac [!] m, simp_all)
+done
+
+lemma [simp]: "\<lbrakk>am ! n = (0::nat); n < length am\<rbrakk> \<Longrightarrow> am[n := 0] = am"
+apply(simp add: list_update_same_conv)
+done
+
+lemma  [intro]: "\<lbrakk>abc_lm_v (a # list) 0 = 0\<rbrakk> \<Longrightarrow> a = 0"
+apply(simp add: abc_lm_v.simps split: if_splits)
+done
+
+lemma [simp]: 
+ "inv_stop (as, abc_lm_s am n 0) 
+          (start_of (layout_of aprog) e, aaa, Oc # xs) ires
+  \<Longrightarrow> inv_locate_a (as, abc_lm_s am n 0) (0, aaa, Oc # xs) ires"
+apply(simp add: inv_locate_a.simps)
+apply(rule disjI1)
+apply(auto simp: inv_stop.simps at_begin_norm.simps)
+done
+
+lemma [simp]: 
+ "\<lbrakk>inv_stop (as, abc_lm_s am n 0) 
+          (start_of (layout_of aprog) e, aaa, Oc # xs) ires\<rbrakk>
+  \<Longrightarrow> inv_locate_b (as, am) (0, Oc # aaa, xs) ires \<or> 
+      inv_locate_b (as, abc_lm_s am n 0) (0, Oc # aaa, xs) ires"
+apply(simp)
+done
+
+lemma dec_false2: 
+ "inv_stop (as, abc_lm_s am n 0) 
+  (start_of (layout_of aprog) e, aaa, Bk # xs) ires = False"
+apply(auto simp: inv_stop.simps abc_lm_s.simps)
+apply(case_tac [!] am, auto)
+apply(case_tac [!] n, auto simp: tape_of_nl_cons split: if_splits)
+done
+
+lemma dec_false3:
+   "inv_stop (as, abc_lm_s am n 0) 
+              (start_of (layout_of aprog) e, aaa, []) ires = False"
+apply(auto simp: inv_stop.simps abc_lm_s.simps)
+done
+
+lemma [simp]:
+  "fetch (ci (layout_of aprog) 
+       (start_of (layout_of aprog) as) (Dec n e)) 0 b = (Nop, 0)"
+by(simp add: fetch.simps)
+
+declare dec_inv_1.simps[simp del]
+
+declare inv_locate_n_b.simps [simp del]
+
+lemma [simp]:
+  "\<lbrakk>0 < abc_lm_v am n; 0 < n; 
+    at_begin_fst_bwtn (as, am) (n, aaa, Oc # xs) ires\<rbrakk>
+ \<Longrightarrow> inv_locate_n_b (as, am) (n, Oc # aaa, xs) ires"
+apply(simp add: at_begin_fst_bwtn.simps inv_locate_n_b.simps )
+done
+ 
+lemma Suc_minus:"length am + tn = n
+       \<Longrightarrow> Suc tn = Suc n - length am "
+apply(arith)
+done
+
+lemma [simp]: 
+ "\<lbrakk>0 < abc_lm_v am n; 0 < n; 
+   at_begin_fst_awtn (as, am) (n, aaa, Oc # xs) ires\<rbrakk>
+ \<Longrightarrow> inv_locate_n_b (as, am) (n, Oc # aaa, xs) ires"
+apply(simp only: at_begin_fst_awtn.simps inv_locate_n_b.simps )
+apply(erule exE)+
+apply(erule conjE)+
+apply(rule_tac x = lm1 in exI, rule_tac x = "[]" in exI, 
+      rule_tac x = "Suc tn" in exI, rule_tac x = 0 in exI)
+apply(simp add: exp_ind del: replicate.simps)
+apply(rule conjI)+
+apply(auto)
+done
+
+lemma [simp]:
+ "\<lbrakk>inv_locate_n_b (as, am) (n, aaa, Oc # xs) ires\<rbrakk>
+ \<Longrightarrow> dec_first_on_right_moving n (as, abc_lm_s am n (abc_lm_v am n))  
+                                      (s, Oc # aaa, xs) ires"
+apply(auto simp: inv_locate_n_b.simps dec_first_on_right_moving.simps 
+                 abc_lm_s.simps abc_lm_v.simps)
+apply(rule_tac x = lm1 in exI, rule_tac x = lm2 in exI, 
+      rule_tac x = m in exI, simp)
+apply(rule_tac x = "Suc (Suc 0)" in exI, 
+      rule_tac x = "m - 1" in exI, simp)
+apply(case_tac m, auto)
+apply(rule_tac x = lm1 in exI, rule_tac x = lm2 in exI, 
+      rule_tac x = m in exI, 
+      simp add: Suc_diff_le exp_ind del: replicate.simps)
+apply(rule_tac x = "Suc (Suc 0)" in exI, 
+      rule_tac x = "m - 1" in exI, simp)
+apply(case_tac m, auto)
+apply(rule_tac x = lm1 in exI, rule_tac x = "[]" in exI, 
+      rule_tac x = m in exI, simp)
+apply(rule_tac x = "Suc (Suc 0)" in exI, 
+      rule_tac x = "m - 1" in exI, simp)
+apply(case_tac m, auto)
+apply(rule_tac x = lm1 in exI, rule_tac x = lm2 in exI, 
+      rule_tac x = m in exI, 
+      simp add: Suc_diff_le exp_ind del: replicate.simps, simp)
+done
+
+lemma [simp]: "inv_on_left_moving (as, am) (s, [], r) ires 
+  = False"
+apply(simp add: inv_on_left_moving.simps inv_on_left_moving_norm.simps
+                inv_on_left_moving_in_middle_B.simps)
+done
+
+lemma [simp]: 
+  "inv_check_left_moving (as, abc_lm_s am n 0)
+  (start_of (layout_of aprog) as + 2 * n + 14, [], Oc # xs) ires
+ = False"
+apply(simp add: inv_check_left_moving.simps inv_check_left_moving_in_middle.simps)
+done
+
+lemma [simp]: "inv_check_left_moving (as, abc_lm_s lm n (abc_lm_v lm n)) (s, [], Oc # list) ires = False"
+apply(simp add: inv_check_left_moving.simps inv_check_left_moving_in_middle.simps)
+done
+
+lemma [elim]: "\<lbrakk>abc_fetch as ap = Some (Dec n e);
+                start_of (layout_of ap) as < start_of (layout_of ap) e; 
+                start_of (layout_of ap) e \<le> Suc (start_of (layout_of ap) as + 2 * n)\<rbrakk>
+       \<Longrightarrow> RR"
+  using start_of_less[of e as "layout_of ap"] start_of_ge[of as ap n e "layout_of ap"]
+apply(case_tac "as < e", simp)
+apply(case_tac "as = e", simp, simp)
+done
+
+lemma crsp_step_dec_b_e_pre':
+  assumes layout: "ly = layout_of ap"
+  and inv_start: "inv_locate_b (as, lm) (n, la, ra) ires"
+  and fetch: "abc_fetch as ap = Some (Dec n e)"
+  and dec_0: "abc_lm_v lm n = 0"
+  and f: "f = (\<lambda> stp. (steps (Suc (start_of ly as) + 2 * n, la, ra) (ci ly (start_of ly as) (Dec n e), 
+            start_of ly as - Suc 0) stp, start_of ly as, n))"
+  and P: "P = (\<lambda> ((s, l, r), ss, x). s = start_of ly e)"
+  and Q: "Q = (\<lambda> ((s, l, r), ss, x). dec_inv_1 ly x e (as, lm) (s, l, r) ires)"
+  shows "\<exists> stp. P (f stp) \<and> Q (f stp)"
+proof(rule_tac LE = abc_dec_1_LE in halt_lemma2)
+  show "wf abc_dec_1_LE" by(intro wf_dec_le)
+next
+  show "Q (f 0)"
+    using layout fetch
+    apply(simp add: f steps.simps Q dec_inv_1.simps)
+    apply(subgoal_tac "e > as \<or> e = as \<or> e < as")
+    apply(auto simp: Let_def start_of_ge start_of_less inv_start)
+    done
+next
+  show "\<not> P (f 0)"
+    using layout fetch
+    apply(simp add: f steps.simps P)
+    done
+next
+  show "\<forall>n. \<not> P (f n) \<and> Q (f n) \<longrightarrow> Q (f (Suc n)) \<and> (f (Suc n), f n) \<in> abc_dec_1_LE"
+    using fetch
+  proof(rule_tac allI, rule_tac impI)
+    fix na
+    assume "\<not> P (f na) \<and> Q (f na)"
+    thus "Q (f (Suc na)) \<and> (f (Suc na), f na) \<in> abc_dec_1_LE"
+      apply(simp add: f)
+      apply(case_tac "steps (Suc (start_of ly as + 2 * n), la, ra)
+        (ci ly (start_of ly as) (Dec n e), start_of ly as - Suc 0) na", simp)
+    proof -
+      fix a b c 
+      assume "\<not> P ((a, b, c), start_of ly as, n) \<and> Q ((a, b, c), start_of ly as, n)"
+      thus "Q (step (a, b, c) (ci ly (start_of ly as) (Dec n e), start_of ly as - Suc 0), start_of ly as, n) \<and>
+               ((step (a, b, c) (ci ly (start_of ly as) (Dec n e), start_of ly as - Suc 0), start_of ly as, n), 
+                   (a, b, c), start_of ly as, n) \<in> abc_dec_1_LE"
+        apply(simp add: Q)
+        apply(case_tac c, case_tac [2] aa)
+        apply(simp_all add: dec_inv_1.simps Let_def split: if_splits)
+        using fetch layout dec_0
+        apply(auto simp: step.simps P dec_inv_1.simps Let_def abc_dec_1_LE_def lex_triple_def lex_pair_def)
+        using dec_0
+        apply(drule_tac dec_false_1, simp_all)
+        done
+    qed
+  qed
+qed
+
+lemma crsp_step_dec_b_e_pre:
+  assumes "ly = layout_of ap"
+  and inv_start: "inv_locate_b (as, lm) (n, la, ra) ires"
+  and dec_0: "abc_lm_v lm n  = 0"
+  and fetch: "abc_fetch as ap = Some (Dec n e)"
+  shows "\<exists>stp lb rb.
+       steps (Suc (start_of ly as) + 2 * n, la, ra) (ci ly (start_of ly as) (Dec n e), 
+       start_of ly as - Suc 0) stp = (start_of ly e, lb, rb) \<and>
+       dec_inv_1 ly n e (as, lm) (start_of ly e, lb, rb) ires"
+  using assms
+  apply(drule_tac crsp_step_dec_b_e_pre', auto)
+  apply(rule_tac x = stp in exI, simp)
+  done
+
+lemma [simp]:
+  "\<lbrakk>abc_lm_v lm n = 0;
+  inv_stop (as, abc_lm_s lm n (abc_lm_v lm n)) (start_of ly e, lb, rb) ires\<rbrakk>
+  \<Longrightarrow> crsp ly (abc_step_l (as, lm) (Some (Dec n e))) (start_of ly e, lb, rb) ires"
+apply(auto simp: crsp.simps abc_step_l.simps inv_stop.simps)
+done
+
+lemma crsp_step_dec_b_e:
+  assumes layout: "ly = layout_of ap"
+  and inv_start: "inv_locate_a (as, lm) (n, l, r) ires"
+  and dec_0: "abc_lm_v lm n = 0"
+  and fetch: "abc_fetch as ap = Some (Dec n e)"
+  shows "\<exists>stp > 0. crsp ly (abc_step_l (as, lm) (Some (Dec n e)))
+  (steps (start_of ly as + 2 * n, l, r) (ci ly (start_of ly as) (Dec n e), start_of ly as - Suc 0) stp) ires"
+proof -
+  let ?P = "ci ly (start_of ly as) (Dec n e)"
+  let ?off = "start_of ly as - Suc 0"
+  have "\<exists> stp la ra. steps (start_of ly as + 2 * n, l, r) (?P, ?off) stp = (Suc (start_of ly as) + 2*n, la, ra)
+             \<and>  inv_locate_b (as, lm) (n, la, ra) ires"
+    using inv_start
+    apply(case_tac "r = [] \<or> hd r = Bk", simp_all)
+    done
+  from this obtain stpa la ra where a:
+    "steps (start_of ly as + 2 * n, l, r) (?P, ?off) stpa = (Suc (start_of ly as) + 2*n, la, ra)
+             \<and>  inv_locate_b (as, lm) (n, la, ra) ires" by blast
+  term dec_inv_1
+  have "\<exists> stp lb rb. steps (Suc (start_of ly as) + 2 * n, la, ra) (?P, ?off) stp = (start_of ly e, lb, rb)
+             \<and>  dec_inv_1 ly n e (as, lm) (start_of ly e, lb, rb) ires"
+    using assms a
+    apply(rule_tac crsp_step_dec_b_e_pre, auto)
+    done
+  from this obtain stpb lb rb where b:
+    "steps (Suc (start_of ly as) + 2 * n, la, ra) (?P, ?off) stpb = (start_of ly e, lb, rb)
+             \<and>  dec_inv_1 ly n e (as, lm) (start_of ly e, lb, rb) ires"  by blast
+  from a b show "\<exists>stp > 0. crsp ly (abc_step_l (as, lm) (Some (Dec n e))) 
+    (steps (start_of ly as + 2 * n, l, r) (?P, ?off) stp) ires"
+    apply(rule_tac x = "stpa + stpb" in exI)
+    apply(simp add: steps_add)
+    using dec_0
+    apply(simp add: dec_inv_1.simps)
+    apply(case_tac stpa, simp_all add: steps.simps)
+    done
+qed    
+  
+fun dec_inv_2 :: "layout \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> dec_inv_t"
+  where
+  "dec_inv_2 ly n e (as, am) (s, l, r) ires =
+           (let ss = start_of ly as in
+            let am' = abc_lm_s am n (abc_lm_v am n - Suc 0) in
+            let am'' = abc_lm_s am n (abc_lm_v am n) in
+              if s = 0 then False
+              else if s = ss + 2 * n then 
+                      inv_locate_a (as, am) (n, l, r) ires
+              else if s = ss + 2 * n + 1 then 
+                      inv_locate_n_b (as, am) (n, l, r) ires
+              else if s = ss + 2 * n + 2 then 
+                      dec_first_on_right_moving n (as, am'') (s, l, r) ires
+              else if s = ss + 2 * n + 3 then 
+                      dec_after_clear (as, am') (s, l, r) ires
+              else if s = ss + 2 * n + 4 then 
+                      dec_right_move (as, am') (s, l, r) ires
+              else if s = ss + 2 * n + 5 then 
+                      dec_check_right_move (as, am') (s, l, r) ires
+              else if s = ss + 2 * n + 6 then 
+                      dec_left_move (as, am') (s, l, r) ires
+              else if s = ss + 2 * n + 7 then 
+                      dec_after_write (as, am') (s, l, r) ires
+              else if s = ss + 2 * n + 8 then 
+                      dec_on_right_moving (as, am') (s, l, r) ires
+              else if s = ss + 2 * n + 9 then 
+                      dec_after_clear (as, am') (s, l, r) ires
+              else if s = ss + 2 * n + 10 then 
+                      inv_on_left_moving (as, am') (s, l, r) ires
+              else if s = ss + 2 * n + 11 then 
+                      inv_check_left_moving (as, am') (s, l, r) ires
+              else if s = ss + 2 * n + 12 then 
+                      inv_after_left_moving (as, am') (s, l, r) ires
+              else if s = ss + 2 * n + 16 then 
+                      inv_stop (as, am') (s, l, r) ires
+              else False)"
+
+declare dec_inv_2.simps[simp del]
+fun abc_dec_2_stage1 :: "config \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat"
+  where
+  "abc_dec_2_stage1 (s, l, r) ss n = 
+              (if s \<le> ss + 2*n + 1 then 7
+               else if s = ss + 2*n + 2 then 6 
+               else if s = ss + 2*n + 3 then 5
+               else if s \<ge> ss + 2*n + 4 \<and> s \<le> ss + 2*n + 9 then 4
+               else if s = ss + 2*n + 6 then 3
+               else if s = ss + 2*n + 10 \<or> s = ss + 2*n + 11 then 2
+               else if s = ss + 2*n + 12 then 1
+               else 0)"
+
+fun abc_dec_2_stage2 :: "config \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat"
+  where
+  "abc_dec_2_stage2 (s, l, r) ss n = 
+       (if s \<le> ss + 2 * n + 1 then (ss + 2 * n + 16 - s)
+        else if s = ss + 2*n + 10 then length l
+        else if s = ss + 2*n + 11 then length l
+        else if s = ss + 2*n + 4 then length r - 1
+        else if s = ss + 2*n + 5 then length r 
+        else if s = ss + 2*n + 7 then length r - 1
+        else if s = ss + 2*n + 8 then  
+              length r + length (takeWhile (\<lambda> a. a = Oc) l) - 1
+        else if s = ss + 2*n + 9 then 
+              length r + length (takeWhile (\<lambda> a. a = Oc) l) - 1
+        else 0)"
+
+fun abc_dec_2_stage3 :: "config \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat"
+  where
+  "abc_dec_2_stage3 (s, l, r) ss n  =
+        (if s \<le> ss + 2*n + 1 then 
+            if (s - ss) mod 2 = 0 then if r \<noteq> [] \<and> 
+                                          hd r = Oc then 0 else 1  
+            else length r
+         else if s = ss + 2 * n + 10 then 
+             if  r \<noteq> [] \<and> hd r = Oc then 2
+             else 1
+         else if s = ss + 2 * n + 11 then 
+             if r \<noteq> [] \<and> hd r = Oc then 3 
+             else 0 
+         else (ss + 2 * n + 16 - s))"
+
+fun abc_dec_2_stage4 :: "config \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat"
+  where
+  "abc_dec_2_stage4 (s, l, r) ss n = 
+          (if s = ss + 2*n + 2 then length r
+           else if s = ss + 2*n + 8 then length r
+           else if s = ss + 2*n + 3 then 
+               if r \<noteq> [] \<and> hd r = Oc then 1
+               else 0
+           else if s = ss + 2*n + 7 then 
+               if r \<noteq> [] \<and> hd r = Oc then 0 
+               else 1
+           else if s = ss + 2*n + 9 then 
+               if r \<noteq> [] \<and> hd r = Oc then 1
+               else 0 
+           else 0)"
+
+fun abc_dec_2_measure :: "(config \<times> nat \<times> nat) \<Rightarrow> (nat \<times> nat \<times> nat \<times> nat)"
+  where
+  "abc_dec_2_measure (c, ss, n) = 
+  (abc_dec_2_stage1 c ss n, 
+  abc_dec_2_stage2 c ss n, abc_dec_2_stage3 c ss n,  abc_dec_2_stage4 c ss n)"
+
+definition lex_square:: 
+   "((nat \<times> nat \<times> nat \<times> nat) \<times> (nat \<times> nat \<times> nat \<times> nat)) set"
+  where "lex_square \<equiv> less_than <*lex*> lex_triple"
+
+definition abc_dec_2_LE ::
+  "((config \<times> nat \<times>
+  nat) \<times> (config \<times> nat \<times> nat)) set"
+  where "abc_dec_2_LE \<equiv> (inv_image lex_square abc_dec_2_measure)"
+
+lemma wf_dec2_le: "wf abc_dec_2_LE"
+by(auto intro:wf_inv_image simp:abc_dec_2_LE_def lex_square_def lex_triple_def lex_pair_def)
+
+lemma fix_add: "fetch ap ((x::nat) + 2*n) b = fetch ap (2*n + x) b"
+by (metis Suc_1 mult_2 nat_add_commute)
+
+lemma [elim]: 
+ "\<lbrakk>0 < abc_lm_v am n; inv_locate_n_b (as, am) (n, aaa, Bk # xs) ires\<rbrakk> 
+ \<Longrightarrow> RR"
+apply(auto simp: inv_locate_n_b.simps abc_lm_v.simps split: if_splits)
+apply(case_tac [!] m, auto)
+done
+ 
+lemma [elim]:
+ "\<lbrakk>0 < abc_lm_v am n; inv_locate_n_b (as, am) 
+                                (n, aaa, []) ires\<rbrakk> \<Longrightarrow> RR"
+apply(auto simp: inv_locate_n_b.simps abc_lm_v.simps split: if_splits)
+done
+
+lemma [simp]: "dec_after_write (as, am) (s, aa, r) ires
+           \<Longrightarrow> takeWhile (\<lambda>a. a = Oc) aa = []"
+apply(simp only : dec_after_write.simps)
+apply(erule exE)+
+apply(erule_tac conjE)+
+apply(case_tac aa, simp)
+apply(case_tac a, simp only: takeWhile.simps , simp_all split: if_splits)
+done
+
+lemma [simp]: 
+     "\<lbrakk>dec_on_right_moving (as, lm) (s, aa, []) ires; 
+       length (takeWhile (\<lambda>a. a = Oc) (tl aa)) 
+           \<noteq> length (takeWhile (\<lambda>a. a = Oc) aa) - Suc 0\<rbrakk>
+    \<Longrightarrow> length (takeWhile (\<lambda>a. a = Oc) (tl aa)) < 
+                       length (takeWhile (\<lambda>a. a = Oc) aa) - Suc 0"
+apply(simp only: dec_on_right_moving.simps)
+apply(erule_tac exE)+
+apply(erule_tac conjE)+
+apply(case_tac mr, auto split: if_splits)
+done
+
+lemma [simp]: 
+  "dec_after_clear (as, abc_lm_s am n (abc_lm_v am n - Suc 0)) 
+             (start_of (layout_of aprog) as + 2 * n + 9, aa, Bk # xs) ires
+ \<Longrightarrow> length xs - Suc 0 < length xs + 
+                             length (takeWhile (\<lambda>a. a = Oc) aa)"
+apply(simp only: dec_after_clear.simps)
+apply(erule_tac exE)+
+apply(erule conjE)+
+apply(simp split: if_splits )
+done
+
+lemma [simp]: 
+ "\<lbrakk>dec_after_clear (as, abc_lm_s am n (abc_lm_v am n - Suc 0))
+       (start_of (layout_of aprog) as + 2 * n + 9, aa, []) ires\<rbrakk>
+    \<Longrightarrow> Suc 0 < length (takeWhile (\<lambda>a. a = Oc) aa)"
+apply(simp add: dec_after_clear.simps split: if_splits)
+done
+
+lemma [elim]: 
+  "inv_check_left_moving (as, lm)
+  (s, [], Oc # xs) ires
+ \<Longrightarrow> RR"
+apply(simp add: inv_check_left_moving.simps inv_check_left_moving_in_middle.simps)
+done
+
+lemma [simp]:
+"\<lbrakk>0 < abc_lm_v am n; 
+  at_begin_norm (as, am) (n, aaa, Oc # xs) ires\<rbrakk>
+  \<Longrightarrow> inv_locate_n_b (as, am) (n, Oc # aaa, xs) ires"
+apply(simp only: at_begin_norm.simps inv_locate_n_b.simps)
+apply(erule_tac exE)+
+apply(rule_tac x = lm1 in exI, simp)
+apply(case_tac "length lm2", simp)
+apply(case_tac "lm2", simp, simp)
+apply(case_tac "lm2", auto simp: tape_of_nl_cons split: if_splits)
+done
+
+lemma [simp]: 
+ "\<lbrakk>0 < abc_lm_v am n; 
+   at_begin_fst_awtn (as, am) (n, aaa, Oc # xs) ires\<rbrakk>
+ \<Longrightarrow> inv_locate_n_b (as, am) (n, Oc # aaa, xs) ires"
+apply(simp only: at_begin_fst_awtn.simps inv_locate_n_b.simps )
+apply(erule exE)+
+apply(erule conjE)+
+apply(rule_tac x = lm1 in exI, rule_tac x = "[]" in exI, 
+      rule_tac x = "Suc tn" in exI, rule_tac x = 0 in exI)
+apply(simp add: exp_ind del: replicate.simps)
+apply(rule conjI)+
+apply(auto)
+done
+
+lemma [simp]: 
+ "\<lbrakk>0 < abc_lm_v am n; inv_locate_a (as, am) (n, aaa, Oc # xs) ires\<rbrakk>
+ \<Longrightarrow> inv_locate_n_b (as, am) (n, Oc#aaa, xs) ires"
+apply(auto simp: inv_locate_a.simps at_begin_fst_bwtn.simps)
+done
+
+lemma [simp]: 
+ "\<lbrakk>dec_on_right_moving (as, am) (s, aa, Bk # xs) ires; 
+   Suc (length (takeWhile (\<lambda>a. a = Oc) (tl aa)))
+   \<noteq> length (takeWhile (\<lambda>a. a = Oc) aa)\<rbrakk>
+  \<Longrightarrow> Suc (length (takeWhile (\<lambda>a. a = Oc) (tl aa))) 
+    < length (takeWhile (\<lambda>a. a = Oc) aa)"
+apply(simp only: dec_on_right_moving.simps)
+apply(erule exE)+
+apply(erule conjE)+
+apply(case_tac ml, auto split: if_splits )
+done
+
+lemma crsp_step_dec_b_suc_pre:
+  assumes layout: "ly = layout_of ap"
+  and crsp: "crsp ly (as, lm) (s, l, r) ires"
+  and inv_start: "inv_locate_a (as, lm) (n, la, ra) ires"
+  and fetch: "abc_fetch as ap = Some (Dec n e)"
+  and dec_suc: "0 < abc_lm_v lm n"
+  and f: "f = (\<lambda> stp. (steps (start_of ly as + 2 * n, la, ra) (ci ly (start_of ly as) (Dec n e), 
+            start_of ly as - Suc 0) stp, start_of ly as, n))"
+  and P: "P = (\<lambda> ((s, l, r), ss, x). s = start_of ly as + 2*n + 16)"
+  and Q: "Q = (\<lambda> ((s, l, r), ss, x). dec_inv_2 ly x e (as, lm) (s, l, r) ires)"
+  shows "\<exists> stp. P (f stp) \<and> Q(f stp)"
+  proof(rule_tac LE = abc_dec_2_LE in halt_lemma2)
+  show "wf abc_dec_2_LE" by(intro wf_dec2_le)
+next
+  show "Q (f 0)"
+    using layout fetch inv_start
+    apply(simp add: f steps.simps Q)
+    apply(simp only: dec_inv_2.simps)
+    apply(auto simp: Let_def start_of_ge start_of_less inv_start dec_inv_2.simps)
+    done
+next
+  show "\<not> P (f 0)"
+    using layout fetch
+    apply(simp add: f steps.simps P)
+    done
+next
+  show "\<forall>n. \<not> P (f n) \<and> Q (f n) \<longrightarrow> Q (f (Suc n)) \<and> (f (Suc n), f n) \<in> abc_dec_2_LE"
+    using fetch
+  proof(rule_tac allI, rule_tac impI)
+    fix na
+    assume "\<not> P (f na) \<and> Q (f na)"
+    thus "Q (f (Suc na)) \<and> (f (Suc na), f na) \<in> abc_dec_2_LE"
+      apply(simp add: f)
+      apply(case_tac "steps ((start_of ly as + 2 * n), la, ra)
+        (ci ly (start_of ly as) (Dec n e), start_of ly as - Suc 0) na", simp)
+    proof -
+      fix a b c 
+      assume "\<not> P ((a, b, c), start_of ly as, n) \<and> Q ((a, b, c), start_of ly as, n)"
+      thus "Q (step (a, b, c) (ci ly (start_of ly as) (Dec n e), start_of ly as - Suc 0), start_of ly as, n) \<and>
+               ((step (a, b, c) (ci ly (start_of ly as) (Dec n e), start_of ly as - Suc 0), start_of ly as, n), 
+                   (a, b, c), start_of ly as, n) \<in> abc_dec_2_LE"
+        apply(simp add: Q)
+        apply(erule_tac conjE)
+        apply(case_tac c, case_tac [2] aa)
+        apply(simp_all add: dec_inv_2.simps Let_def)
+        apply(simp_all split: if_splits)
+        using fetch layout dec_suc
+        apply(auto simp: step.simps P dec_inv_2.simps Let_def abc_dec_2_LE_def lex_triple_def lex_pair_def lex_square_def
+                         fix_add numeral_3_eq_3) 
+        done
+    qed
+  qed
+qed
+
+lemma [simp]: 
+  "\<lbrakk>inv_stop (as, abc_lm_s lm n (abc_lm_v lm n - Suc 0)) 
+  (start_of (layout_of ap) as + 2 * n + 16, a, b) ires;
+   abc_lm_v lm n > 0;
+   abc_fetch as ap = Some (Dec n e)\<rbrakk>
+  \<Longrightarrow> crsp (layout_of ap) (abc_step_l (as, lm) (Some (Dec n e))) 
+  (start_of (layout_of ap) as + 2 * n + 16, a, b) ires"
+apply(auto simp: inv_stop.simps crsp.simps  abc_step_l.simps startof_Suc2)
+apply(drule_tac startof_Suc2, simp)
+done
+  
+lemma crsp_step_dec_b_suc:
+  assumes layout: "ly = layout_of ap"
+  and crsp: "crsp ly (as, lm) (s, l, r) ires"
+  and inv_start: "inv_locate_a (as, lm) (n, la, ra) ires"
+  and fetch: "abc_fetch as ap = Some (Dec n e)"
+  and dec_suc: "0 < abc_lm_v lm n"
+  shows "\<exists>stp > 0. crsp ly (abc_step_l (as, lm) (Some (Dec n e)))
+              (steps (start_of ly as + 2 * n, la, ra) (ci (layout_of ap) 
+                  (start_of ly as) (Dec n e), start_of ly as - Suc 0) stp) ires"
+  using assms
+  apply(drule_tac crsp_step_dec_b_suc_pre, auto)
+  apply(rule_tac x = stp in exI, simp)
+  apply(simp add: dec_inv_2.simps)
+  apply(case_tac stp, simp_all add: steps.simps)
+  done
+
+lemma crsp_step_dec_b:
+  assumes layout: "ly = layout_of ap"
+  and crsp: "crsp ly (as, lm) (s, l, r) ires"
+  and inv_start: "inv_locate_a (as, lm) (n, la, ra) ires"
+  and fetch: "abc_fetch as ap = Some (Dec n e)"
+  shows "\<exists>stp > 0. crsp ly (abc_step_l (as, lm) (Some (Dec n e)))
+  (steps (start_of ly as + 2 * n, la, ra) (ci ly (start_of ly as) (Dec n e), start_of ly as - Suc 0) stp) ires"
+using assms
+apply(case_tac "abc_lm_v lm n = 0")
+apply(rule_tac crsp_step_dec_b_e, simp_all)
+apply(rule_tac crsp_step_dec_b_suc, simp_all)
+done
+
+lemma crsp_step_dec: 
+  assumes layout: "ly = layout_of ap"
+  and crsp: "crsp ly (as, lm) (s, l, r) ires"
+  and fetch: "abc_fetch as ap = Some (Dec n e)"
+  shows "\<exists>stp > 0. crsp ly (abc_step_l (as, lm) (Some (Dec n e)))
+  (steps (s, l, r) (ci ly (start_of ly as) (Dec n e), start_of ly as - Suc 0) stp) ires"
+proof(simp add: ci.simps)
+  let ?off = "start_of ly as - Suc 0"
+  let ?A = "findnth n"
+  let ?B = "sete (shift (shift tdec_b (2 * n)) ?off) (start_of ly e)"
+  have "\<exists> stp la ra. steps (s, l, r) (shift ?A ?off @ ?B, ?off) stp = (start_of ly as + 2*n, la, ra)
+                    \<and> inv_locate_a (as, lm) (n, la, ra) ires"
+  proof -
+    have "\<exists>stp l' r'. steps (Suc 0, l, r) (?A, 0) stp = (Suc (2 * n), l', r') \<and> 
+                     inv_locate_a (as, lm) (n, l', r') ires"
+      using assms
+      apply(rule_tac findnth_correct, simp_all)
+      done
+    then obtain stp l' r' where a: 
+      "steps (Suc 0, l, r) (?A, 0) stp = (Suc (2 * n), l', r') \<and> 
+      inv_locate_a (as, lm) (n, l', r') ires" by blast
+    then have "steps (Suc 0 + ?off, l, r) (shift ?A ?off, ?off) stp = (Suc (2 * n) + ?off, l', r')"
+      apply(rule_tac tm_shift_eq_steps, simp_all)
+      done
+    moreover have "s = start_of ly as"
+      using crsp
+      apply(auto simp: crsp.simps)
+      done
+    ultimately show "\<exists> stp la ra. steps (s, l, r) (shift ?A ?off @ ?B, ?off) stp = (start_of ly as + 2*n, la, ra)
+                    \<and> inv_locate_a (as, lm) (n, la, ra) ires"
+      using a
+      apply(drule_tac B = ?B in tm_append_first_steps_eq, auto)
+      apply(rule_tac x = stp in exI, simp)
+      done
+  qed
+  from this obtain stpa la ra where a: 
+    "steps (s, l, r) (shift ?A ?off @ ?B, ?off) stpa = (start_of ly as + 2*n, la, ra)
+                    \<and> inv_locate_a (as, lm) (n, la, ra) ires" by blast
+  have "\<exists>stp. crsp ly (abc_step_l (as, lm) (Some (Dec n e)))
+           (steps (start_of ly as + 2*n, la, ra) (shift ?A ?off @ ?B, ?off) stp) ires \<and> stp > 0"
+    using assms a
+    apply(drule_tac crsp_step_dec_b, auto)
+    apply(rule_tac x = stp in exI, simp add: ci.simps)
+    done
+  then obtain stpb where b: 
+    "crsp ly (abc_step_l (as, lm) (Some (Dec n e)))
+    (steps (start_of ly as + 2*n, la, ra) (shift ?A ?off @ ?B, ?off) stpb) ires \<and> stpb > 0" ..
+  from a b show "\<exists> stp>0. crsp ly (abc_step_l (as, lm) (Some (Dec n e)))
+    (steps (s, l, r) (shift ?A ?off @ ?B, ?off) stp) ires"
+    apply(rule_tac x = "stpa + stpb" in exI)
+    apply(simp add: steps_add)
+    done
+qed    
+  
+subsection{*Crsp of Goto*}
+
+lemma crsp_step_goto:
+  assumes layout: "ly = layout_of ap"
+  and crsp: "crsp ly (as, lm) (s, l, r) ires"
+  shows "\<exists>stp>0. crsp ly (abc_step_l (as, lm) (Some (Goto n)))
+  (steps (s, l, r) (ci ly (start_of ly as) (Goto n), 
+            start_of ly as - Suc 0) stp) ires"
+using crsp
+apply(rule_tac x = "Suc 0" in exI)
+apply(case_tac r, case_tac [2] a)
+apply(simp_all add: ci.simps steps.simps step.simps crsp.simps fetch.simps
+  crsp.simps abc_step_l.simps)
+done
+
+lemma crsp_step_in:
+  assumes layout: "ly = layout_of ap"
+  and compile: "tp = tm_of ap"
+  and crsp: "crsp ly (as, lm) (s, l, r) ires"
+  and fetch: "abc_fetch as ap = Some ins"
+  shows "\<exists> stp>0. crsp ly (abc_step_l (as, lm) (Some ins))
+                      (steps (s, l, r) (ci ly (start_of ly as) ins, start_of ly as - 1) stp) ires"
+  using assms
+  apply(case_tac ins, simp_all)
+  apply(rule crsp_step_inc, simp_all)
+  apply(rule crsp_step_dec, simp_all)
+  apply(rule_tac crsp_step_goto, simp_all)
+  done
+
+lemma crsp_step:
+  assumes layout: "ly = layout_of ap"
+  and compile: "tp = tm_of ap"
+  and crsp: "crsp ly (as, lm) (s, l, r) ires"
+  and fetch: "abc_fetch as ap = Some ins"
+  shows "\<exists> stp>0. crsp ly (abc_step_l (as, lm) (Some ins))
+                      (steps (s, l, r) (tp, 0) stp) ires"
+proof -
+  have "\<exists> stp>0. crsp ly (abc_step_l (as, lm) (Some ins))
+                      (steps (s, l, r) (ci ly (start_of ly as) ins, start_of ly as - 1) stp) ires"
+    using assms
+    apply(rule_tac crsp_step_in, simp_all)
+    done
+  from this obtain stp where d: "stp > 0 \<and> crsp ly (abc_step_l (as, lm) (Some ins))
+                      (steps (s, l, r) (ci ly (start_of ly as) ins, start_of ly as - 1) stp) ires" ..
+  obtain s' l' r' where e:
+    "(steps (s, l, r) (ci ly (start_of ly as) ins, start_of ly as - 1) stp) = (s', l', r')"
+    apply(case_tac "(steps (s, l, r) (ci ly (start_of ly as) ins, start_of ly as - 1) stp)")
+    by blast
+  then have "steps (s, l, r) (tp, 0) stp = (s', l', r')"
+    using assms d
+    apply(rule_tac steps_eq_in)
+    apply(simp_all)
+    apply(case_tac "(abc_step_l (as, lm) (Some ins))", simp add: crsp.simps)
+    done    
+  thus " \<exists>stp>0. crsp ly (abc_step_l (as, lm) (Some ins)) (steps (s, l, r) (tp, 0) stp) ires"
+    using d e
+    apply(rule_tac x = stp in exI, simp)
+    done
+qed
+
+lemma crsp_steps:
+  assumes layout: "ly = layout_of ap"
+  and compile: "tp = tm_of ap"
+  and crsp: "crsp ly (as, lm) (s, l, r) ires"
+  shows "\<exists> stp. crsp ly (abc_steps_l (as, lm) ap n)
+                      (steps (s, l, r) (tp, 0) stp) ires"
+(*
+proof(induct n)
+  case 0
+  have "crsp ly (abc_steps_l (as, lm) ap 0) (steps (s, l, r) (tp, 0) 0) ires"
+    using crsp by(simp add: steps.simps abc_steps_l.simps)
+  thus "?case"
+    by(rule_tac x = 0 in exI, simp)
+next
+  case (Suc n)
+  obtain as' lm' where a: "abc_steps_l (as, lm) ap n = (as', lm')"
+    by(case_tac "abc_steps_l (as, lm) ap n", auto) 
+  have "\<exists>stp\<ge>n. crsp ly (abc_steps_l (as, lm) ap n) (steps (s, l, r) (tp, 0) stp) ires"
+    by fact
+  from this a obtain stpa where b:
+    "stpa\<ge>n \<and> crsp ly (as', lm') (steps (s, l, r) (tp, 0) stpa) ires" by auto
+  obtain s' l' r' where "steps (s, l, r) (tp, 0) stpa = (s', l', r')"
+    by(case_tac "steps (s, l, r) (tp, 0) stpa")
+  then have "stpa\<ge>n \<and> crsp ly (as', lm') (s', l', r') ires" using b by simp
+  from a and this show "?case"
+  proof(cases "abc_fetch as' ap")
+    case None
+    
+  
+
+    have "crsp ly (abc_steps_l (as, lm) ap 0) (steps (s, l, r) (tp, 0) stp) ires"
+    apply(simp add: steps.simps abc_steps_l.simps)
+*)
+  using crsp
+  apply(induct n)
+  apply(rule_tac x = 0 in exI) 
+  apply(simp add: steps.simps abc_steps_l.simps, simp)
+  apply(case_tac "(abc_steps_l (as, lm) ap n)", auto)
+  apply(frule_tac abc_step_red, simp)
+  apply(case_tac "abc_fetch a ap", simp add: abc_step_l.simps, auto)
+  apply(case_tac "steps (s, l, r) (tp, 0) stp", simp)
+  using assms
+  apply(drule_tac s = ab and l = ba and r = c in crsp_step, auto)
+  apply(rule_tac x = "stp + stpa" in exI, simp add: steps_add)
+  done
+
+lemma tp_correct': 
+  assumes layout: "ly = layout_of ap"
+  and compile: "tp = tm_of ap"
+  and crsp: "crsp ly (0, lm) (Suc 0, l, r) ires"
+  and abc_halt: "abc_steps_l (0, lm) ap stp = (length ap, am)"
+  shows "\<exists> stp k. steps (Suc 0, l, r) (tp, 0) stp = (start_of ly (length ap), Bk # Bk # ires, <am> @ Bk\<up>k)"
+  using assms
+  apply(drule_tac n = stp in crsp_steps, auto)
+  apply(rule_tac x = stpa in exI)
+  apply(case_tac "steps (Suc 0, l, r) (tm_of ap, 0) stpa", simp add: crsp.simps)
+  done
+
+text{*The tp @ [(Nop, 0), (Nop, 0)] is nomoral turing machines, so we can use Hoare_plus when composing with Mop machine*}
+
+thm layout_of.simps
+lemma layout_id_cons: "layout_of (ap @ [p]) = layout_of ap @ [length_of p]"
+apply(simp add: layout_of.simps)
+done
+
+lemma [simp]: "length (layout_of xs) = length xs"
+by(simp add: layout_of.simps)
+
+thm tms_of.simps
+term ci
+thm tms_of.simps
+thm tpairs_of.simps
+
+lemma [simp]:  
+  "map (start_of (layout_of xs @ [length_of x])) [0..<length xs] =  (map (start_of (layout_of xs)) [0..<length xs])"
+apply(auto)
+apply(simp add: layout_of.simps start_of.simps)
+done
+
+lemma tpairs_id_cons: 
+  "tpairs_of (xs @ [x]) = tpairs_of xs @ [(start_of (layout_of (xs @ [x])) (length xs), x)]"
+apply(auto simp: tpairs_of.simps layout_id_cons )
+done
+
+lemma map_length_ci:
+  "(map (length \<circ> (\<lambda>(xa, y). ci (layout_of xs @ [length_of x]) xa y)) (tpairs_of xs)) = 
+  (map (length \<circ> (\<lambda>(x, y). ci (layout_of xs) x y)) (tpairs_of xs)) "
+apply(auto)
+apply(case_tac b, auto simp: ci.simps sete.simps)
+done
+
+lemma length_tp'[simp]: 
+  "\<lbrakk>ly = layout_of ap; tp = tm_of ap\<rbrakk> \<Longrightarrow>
+       length tp = 2 * listsum (take (length ap) (layout_of ap))"
+proof(induct ap arbitrary: ly tp rule: rev_induct)
+  case Nil
+  thus "?case"
+    by(simp add: tms_of.simps tm_of.simps tpairs_of.simps)
+next
+  fix x xs ly tp
+  assume ind: "\<And>ly tp. \<lbrakk>ly = layout_of xs; tp = tm_of xs\<rbrakk> \<Longrightarrow> 
+    length tp = 2 * listsum (take (length xs) (layout_of xs))"
+  and layout: "ly = layout_of (xs @ [x])"
+  and tp: "tp = tm_of (xs @ [x])"
+  obtain ly' where a: "ly' = layout_of xs"
+    by metis
+  obtain tp' where b: "tp' = tm_of xs"
+    by metis
+  have c: "length tp' = 2 * listsum (take (length xs) (layout_of xs))"
+    using a b
+    by(erule_tac ind, simp)
+  thus "length tp = 2 * 
+    listsum (take (length (xs @ [x])) (layout_of (xs @ [x])))"
+    using tp b
+    apply(auto simp: layout_id_cons tm_of.simps tms_of.simps length_concat tpairs_id_cons map_length_ci)
+    apply(case_tac x)
+    apply(auto simp: ci.simps tinc_b_def tdec_b_def length_findnth sete.simps length_of.simps
+                 split: abc_inst.splits)
+    done
+qed
+
+lemma [simp]: 
+  "\<lbrakk>ly = layout_of ap; tp = tm_of ap\<rbrakk> \<Longrightarrow>
+        fetch (tp @ [(Nop, 0), (Nop, 0)]) (start_of ly (length ap)) b = 
+       (Nop, 0)"
+apply(case_tac b)
+apply(simp_all add: start_of.simps fetch.simps nth_append)
+done
+(*
+lemma tp_correct: 
+  assumes layout: "ly = layout_of ap"
+  and compile: "tp = tm_of ap"
+  and crsp: "crsp ly (0, lm) (Suc 0, l, r) ires"
+  and abc_halt: "abc_steps_l (0, lm) ap stp = (length ap, am)"
+  shows "\<exists> stp k. steps (Suc 0, l, r) (tp @ [(Nop, 0), (Nop, 0)], 0) stp = (0, Bk # Bk # ires, <am> @ Bk\<up>k)"
+  using assms
+proof -
+  have "\<exists> stp k. steps (Suc 0, l, r) (tp @ [(Nop, 0), (Nop, 0)], 0) stp =
+    (start_of ly (length ap), Bk # Bk # ires, <am> @ Bk\<up>k)"
+  proof -
+    have "\<exists> stp k. steps (Suc 0, l, r) (tp, 0) stp =
+    (start_of ly (length ap), Bk # Bk # ires, <am> @ Bk\<up>k)"
+      using assms
+      apply(rule_tac tp_correct', simp_all)
+      done
+    from this obtain stp k where "steps (Suc 0, l, r) (tp, 0) stp =
+    (start_of ly (length ap), Bk # Bk # ires, <am> @ Bk\<up>k)" by blast
+    thus "?thesis"
+      apply(rule_tac x = stp in exI, rule_tac x = k in exI)
+      apply(drule_tac tm_append_first_steps_eq, simp_all)
+      done
+  qed
+  from this obtain stp k where 
+    "steps (Suc 0, l, r) (tp @ [(Nop, 0), (Nop, 0)], 0) stp =
+    (start_of ly (length ap), Bk # Bk # ires, <am> @ Bk\<up>k)"
+    by blast
+  thus "\<exists>stp k. steps (Suc 0, l, r) (tp @ [(Nop, 0), (Nop, 0)], 0) stp 
+    = (0, Bk # Bk # ires, <am> @ Bk \<up> k)"
+    using assms
+    apply(rule_tac x = "stp + Suc 0" in exI)
+    apply(simp add: steps_add)
+    apply(auto simp: step.simps)
+    done
+qed
+ *)   
+(********for mopup***********)
+fun mopup_a :: "nat \<Rightarrow> instr list"
+  where
+  "mopup_a 0 = []" |
+  "mopup_a (Suc n) = mopup_a n @ 
+       [(R, 2*n + 3), (W0, 2*n + 2), (R, 2*n + 1), (W1, 2*n + 2)]"
+
+definition mopup_b :: "instr list"
+  where
+  "mopup_b \<equiv> [(R, 2), (R, 1), (L, 5), (W0, 3), (R, 4), (W0, 3),
+            (R, 2), (W0, 3), (L, 5), (L, 6), (R, 0), (L, 6)]"
+
+fun mopup :: "nat \<Rightarrow> instr list"
+  where 
+  "mopup n = mopup_a n @ shift mopup_b (2*n)"
+(****)
+
+type_synonym mopup_type = "config \<Rightarrow> nat list \<Rightarrow> nat \<Rightarrow> cell list \<Rightarrow> bool"
+
+fun mopup_stop :: "mopup_type"
+  where
+  "mopup_stop (s, l, r) lm n ires= 
+        (\<exists> ln rn. l = Bk\<up>ln @ Bk # Bk # ires \<and> r = <abc_lm_v lm n> @ Bk\<up>rn)"
+
+fun mopup_bef_erase_a :: "mopup_type"
+  where
+  "mopup_bef_erase_a (s, l, r) lm n ires= 
+         (\<exists> ln m rn. l = Bk\<up>ln @ Bk # Bk # ires \<and> 
+                  r = Oc\<up>m@ Bk # <(drop ((s + 1) div 2) lm)> @ Bk\<up>rn)"
+
+fun mopup_bef_erase_b :: "mopup_type"
+  where
+  "mopup_bef_erase_b (s, l, r) lm n ires = 
+      (\<exists> ln m rn. l = Bk\<up>ln @ Bk # Bk # ires \<and> r = Bk # Oc\<up>m @ Bk # 
+                                      <(drop (s div 2) lm)> @ Bk\<up>rn)"
+
+fun mopup_jump_over1 :: "mopup_type"
+  where
+  "mopup_jump_over1 (s, l, r) lm n ires = 
+      (\<exists> ln m1 m2 rn. m1 + m2 = Suc (abc_lm_v lm n) \<and> 
+        l = Oc\<up>m1 @ Bk\<up>ln @ Bk # Bk # ires \<and> 
+     (r = Oc\<up>m2 @ Bk # <(drop (Suc n) lm)> @ Bk\<up>rn \<or> 
+     (r = Oc\<up>m2 \<and> (drop (Suc n) lm) = [])))"
+
+fun mopup_aft_erase_a :: "mopup_type"
+  where
+  "mopup_aft_erase_a (s, l, r) lm n ires = 
+      (\<exists> lnl lnr rn (ml::nat list) m. 
+          m = Suc (abc_lm_v lm n) \<and> l = Bk\<up>lnr @ Oc\<up>m @ Bk\<up>lnl @ Bk # Bk # ires \<and> 
+                                   (r = <ml> @ Bk\<up>rn))"
+
+fun mopup_aft_erase_b :: "mopup_type"
+  where
+  "mopup_aft_erase_b (s, l, r) lm n ires= 
+   (\<exists> lnl lnr rn (ml::nat list) m. 
+      m = Suc (abc_lm_v lm n) \<and> 
+      l = Bk\<up>lnr @ Oc\<up>m @ Bk\<up>lnl @ Bk # Bk # ires \<and> 
+     (r = Bk # <ml> @ Bk\<up>rn \<or>
+      r = Bk # Bk # <ml> @ Bk\<up>rn))"
+
+fun mopup_aft_erase_c :: "mopup_type"
+  where
+  "mopup_aft_erase_c (s, l, r) lm n ires = 
+ (\<exists> lnl lnr rn (ml::nat list) m. 
+     m = Suc (abc_lm_v lm n) \<and> 
+     l = Bk\<up>lnr @ Oc\<up>m @ Bk\<up>lnl @ Bk # Bk # ires \<and> 
+    (r = <ml> @ Bk\<up>rn \<or> r = Bk # <ml> @ Bk\<up>rn))"
+
+fun mopup_left_moving :: "mopup_type"
+  where
+  "mopup_left_moving (s, l, r) lm n ires = 
+  (\<exists> lnl lnr rn m.
+     m = Suc (abc_lm_v lm n) \<and> 
+   ((l = Bk\<up>lnr @ Oc\<up>m @ Bk\<up>lnl @ Bk # Bk # ires \<and> r = Bk\<up>rn) \<or>
+    (l = Oc\<up>(m - 1) @ Bk\<up>lnl @ Bk # Bk # ires \<and> r = Oc # Bk\<up>rn)))"
+
+fun mopup_jump_over2 :: "mopup_type"
+  where
+  "mopup_jump_over2 (s, l, r) lm n ires = 
+     (\<exists> ln rn m1 m2.
+          m1 + m2 = Suc (abc_lm_v lm n) 
+        \<and> r \<noteq> [] 
+        \<and> (hd r = Oc \<longrightarrow> (l = Oc\<up>m1 @ Bk\<up>ln @ Bk # Bk # ires \<and> r = Oc\<up>m2 @ Bk\<up>rn)) 
+        \<and> (hd r = Bk \<longrightarrow> (l = Bk\<up>ln @ Bk # ires \<and> r = Bk # Oc\<up>(m1+m2)@ Bk\<up>rn)))"
+
+
+fun mopup_inv :: "mopup_type"
+  where
+  "mopup_inv (s, l, r) lm n ires = 
+      (if s = 0 then mopup_stop (s, l, r) lm n ires
+       else if s \<le> 2*n then
+               if s mod 2 = 1 then mopup_bef_erase_a (s, l, r) lm n ires
+                   else mopup_bef_erase_b (s, l, r) lm n ires
+            else if s = 2*n + 1 then 
+                mopup_jump_over1 (s, l, r) lm n ires
+            else if s = 2*n + 2 then mopup_aft_erase_a (s, l, r) lm n ires
+            else if s = 2*n + 3 then mopup_aft_erase_b (s, l, r) lm n ires
+            else if s = 2*n + 4 then mopup_aft_erase_c (s, l, r) lm n ires
+            else if s = 2*n + 5 then mopup_left_moving (s, l, r) lm n ires
+            else if s = 2*n + 6 then mopup_jump_over2 (s, l, r) lm n ires
+            else False)"
+
+lemma mopup_fetch_0[simp]: 
+     "(fetch (mopup_a n @ shift mopup_b (2 * n)) 0 b) = (Nop, 0)"
+by(simp add: fetch.simps)
+
+lemma mop_bef_length[simp]: "length (mopup_a n) = 4 * n"
+apply(induct n, simp_all add: mopup_a.simps)
+done
+
+lemma mopup_a_nth: 
+  "\<lbrakk>q < n; x < 4\<rbrakk> \<Longrightarrow> mopup_a n ! (4 * q + x) = 
+                             mopup_a (Suc q) ! ((4 * q) + x)"
+apply(induct n, simp)
+apply(case_tac "q < n", simp add: mopup_a.simps, auto)
+apply(simp add: nth_append)
+apply(subgoal_tac "q = n", simp)
+apply(arith)
+done
+
+lemma fetch_bef_erase_a_o[simp]: 
+ "\<lbrakk>0 < s; s \<le> 2 * n; s mod 2 = Suc 0\<rbrakk>
+  \<Longrightarrow> (fetch (mopup_a n @ shift mopup_b (2 * n)) s Oc) = (W0, s + 1)"
+apply(subgoal_tac "\<exists> q. s = 2*q + 1", auto)
+apply(subgoal_tac "length (mopup_a n) = 4*n")
+apply(auto simp: fetch.simps nth_of.simps nth_append)
+apply(subgoal_tac "mopup_a n ! (4 * q + 1) = 
+                      mopup_a (Suc q) ! ((4 * q) + 1)", 
+      simp add: mopup_a.simps nth_append)
+apply(rule mopup_a_nth, auto)
+apply arith
+done
+
+lemma fetch_bef_erase_a_b[simp]:
+  "\<lbrakk>0 < s; s \<le> 2 * n; s mod 2 = Suc 0\<rbrakk>
+   \<Longrightarrow>  (fetch (mopup_a n @ shift mopup_b (2 * n)) s Bk) = (R, s + 2)"
+apply(subgoal_tac "\<exists> q. s = 2*q + 1", auto)
+apply(subgoal_tac "length (mopup_a n) = 4*n")
+apply(auto simp: fetch.simps nth_of.simps nth_append)
+apply(subgoal_tac "mopup_a n ! (4 * q + 0) = 
+                       mopup_a (Suc q) ! ((4 * q + 0))", 
+      simp add: mopup_a.simps nth_append)
+apply(rule mopup_a_nth, auto)
+apply arith
+done
+
+lemma fetch_bef_erase_b_b: 
+  "\<lbrakk>n < length lm; 0 < s; s \<le> 2 * n; s mod 2 = 0\<rbrakk> \<Longrightarrow> 
+     (fetch (mopup_a n @ shift mopup_b (2 * n)) s Bk) = (R, s - 1)"
+apply(subgoal_tac "\<exists> q. s = 2 * q", auto)
+apply(case_tac qa, simp, simp)
+apply(auto simp: fetch.simps nth_of.simps nth_append)
+apply(subgoal_tac "mopup_a n ! (4 * nat + 2) = 
+                     mopup_a (Suc nat) ! ((4 * nat) + 2)", 
+      simp add: mopup_a.simps nth_append)
+apply(rule mopup_a_nth, auto)
+done
+
+lemma fetch_jump_over1_o: 
+ "fetch (mopup_a n @ shift mopup_b (2 * n)) (Suc (2 * n)) Oc
+  = (R, Suc (2 * n))"
+apply(subgoal_tac "length (mopup_a n) = 4 * n")
+apply(auto simp: fetch.simps nth_of.simps mopup_b_def nth_append 
+                 shift.simps)
+done
+
+lemma fetch_jump_over1_b: 
+ "fetch (mopup_a n @ shift mopup_b (2 * n)) (Suc (2 * n)) Bk 
+ = (R, Suc (Suc (2 * n)))"
+apply(subgoal_tac "length (mopup_a n) = 4 * n")
+apply(auto simp: fetch.simps nth_of.simps mopup_b_def 
+                 nth_append shift.simps)
+done
+
+lemma fetch_aft_erase_a_o: 
+ "fetch (mopup_a n @ shift mopup_b (2 * n)) (Suc (Suc (2 * n))) Oc 
+ = (W0, Suc (2 * n + 2))"
+apply(subgoal_tac "length (mopup_a n) = 4 * n")
+apply(auto simp: fetch.simps nth_of.simps mopup_b_def 
+                 nth_append shift.simps)
+done
+
+lemma fetch_aft_erase_a_b: 
+ "fetch (mopup_a n @ shift mopup_b (2 * n)) (Suc (Suc (2 * n))) Bk
+  = (L, Suc (2 * n + 4))"
+apply(subgoal_tac "length (mopup_a n) = 4 * n")
+apply(auto simp: fetch.simps nth_of.simps mopup_b_def 
+                 nth_append shift.simps)
+done
+
+lemma fetch_aft_erase_b_b: 
+ "fetch (mopup_a n @ shift mopup_b (2 * n)) (2*n + 3) Bk
+  = (R, Suc (2 * n + 3))"
+apply(subgoal_tac "length (mopup_a n) = 4 * n")
+apply(subgoal_tac "2*n + 3 = Suc (2*n + 2)", simp only: fetch.simps)
+apply(auto simp: nth_of.simps mopup_b_def nth_append shift.simps)
+done
+
+lemma fetch_aft_erase_c_o: 
+ "fetch (mopup_a n @ shift mopup_b (2 * n)) (2 * n + 4) Oc 
+ = (W0, Suc (2 * n + 2))"
+apply(subgoal_tac "length (mopup_a n) = 4 * n")
+apply(subgoal_tac "2*n + 4 = Suc (2*n + 3)", simp only: fetch.simps)
+apply(auto simp: nth_of.simps mopup_b_def nth_append shift.simps)
+done
+
+lemma fetch_aft_erase_c_b: 
+ "fetch (mopup_a n @ shift mopup_b (2 * n)) (2 * n + 4) Bk 
+ = (R, Suc (2 * n + 1))"
+apply(subgoal_tac "length (mopup_a n) = 4 * n")
+apply(subgoal_tac "2*n + 4 = Suc (2*n + 3)", simp only: fetch.simps)
+apply(auto simp: nth_of.simps mopup_b_def nth_append shift.simps)
+done
+
+lemma fetch_left_moving_o: 
+ "(fetch (mopup_a n @ shift mopup_b (2 * n)) (2 * n + 5) Oc) 
+ = (L, 2*n + 6)"
+apply(subgoal_tac "length (mopup_a n) = 4 * n")
+apply(subgoal_tac "2*n + 5 = Suc (2*n + 4)", simp only: fetch.simps)
+apply(auto simp: nth_of.simps mopup_b_def nth_append shift.simps)
+done
+
+lemma fetch_left_moving_b: 
+ "(fetch (mopup_a n @ shift mopup_b (2 * n)) (2 * n + 5) Bk)
+  = (L, 2*n + 5)"
+apply(subgoal_tac "length (mopup_a n) = 4 * n")
+apply(subgoal_tac "2*n + 5 = Suc (2*n + 4)", simp only: fetch.simps)
+apply(auto simp: nth_of.simps mopup_b_def nth_append shift.simps)
+done
+
+lemma fetch_jump_over2_b:
+  "(fetch (mopup_a n @ shift mopup_b (2 * n)) (2 * n + 6) Bk) 
+ = (R, 0)"
+apply(subgoal_tac "length (mopup_a n) = 4 * n")
+apply(subgoal_tac "2*n + 6 = Suc (2*n + 5)", simp only: fetch.simps)
+apply(auto simp: nth_of.simps mopup_b_def nth_append shift.simps)
+done
+
+lemma fetch_jump_over2_o: 
+"(fetch (mopup_a n @ shift mopup_b (2 * n)) (2 * n + 6) Oc) 
+ = (L, 2*n + 6)"
+apply(subgoal_tac "length (mopup_a n) = 4 * n")
+apply(subgoal_tac "2*n + 6 = Suc (2*n + 5)", simp only: fetch.simps)
+apply(auto simp: nth_of.simps mopup_b_def nth_append shift.simps)
+done
+
+lemmas mopupfetchs = 
+fetch_bef_erase_a_o fetch_bef_erase_a_b fetch_bef_erase_b_b 
+fetch_jump_over1_o fetch_jump_over1_b fetch_aft_erase_a_o 
+fetch_aft_erase_a_b fetch_aft_erase_b_b fetch_aft_erase_c_o 
+fetch_aft_erase_c_b fetch_left_moving_o fetch_left_moving_b 
+fetch_jump_over2_b fetch_jump_over2_o
+
+declare 
+  mopup_jump_over2.simps[simp del] mopup_left_moving.simps[simp del]
+  mopup_aft_erase_c.simps[simp del] mopup_aft_erase_b.simps[simp del] 
+  mopup_aft_erase_a.simps[simp del] mopup_jump_over1.simps[simp del]
+  mopup_bef_erase_a.simps[simp del] mopup_bef_erase_b.simps[simp del]
+  mopup_stop.simps[simp del]
+
+lemma [simp]: 
+  "\<lbrakk>mopup_bef_erase_a (s, l, Oc # xs) lm n ires\<rbrakk> \<Longrightarrow> 
+  mopup_bef_erase_b (Suc s, l, Bk # xs) lm n ires"
+apply(auto simp: mopup_bef_erase_a.simps mopup_bef_erase_b.simps )
+apply(rule_tac x = "m - 1" in exI, rule_tac x = rn in exI)
+apply(case_tac m, simp, simp)
+done
+
+lemma mopup_false1:
+  "\<lbrakk>0 < s; s \<le> 2 * n; s mod 2 = Suc 0;  \<not> Suc s \<le> 2 * n\<rbrakk> 
+  \<Longrightarrow> RR"
+apply(arith)
+done
+
+lemma [simp]: 
+ "\<lbrakk>n < length lm; 0 < s; s \<le> 2 * n; s mod 2 = Suc 0; 
+   mopup_bef_erase_a (s, l, Oc # xs) lm n ires; r = Oc # xs\<rbrakk>
+ \<Longrightarrow> (Suc s \<le> 2 * n \<longrightarrow> mopup_bef_erase_b (Suc s, l, Bk # xs) lm n ires)  \<and>
+     (\<not> Suc s \<le> 2 * n \<longrightarrow> mopup_jump_over1 (Suc s, l, Bk # xs) lm n ires) "
+apply(auto elim: mopup_false1)
+done
+
+lemma drop_tape_of_cons: 
+  "\<lbrakk>Suc q < length lm; x = lm ! q\<rbrakk> \<Longrightarrow> <drop q lm> = Oc # Oc \<up> x @ Bk # <drop (Suc q) lm>"
+by (metis Suc_lessD append_Cons list.simps(2) nth_drop' replicate_Suc tape_of_nl_cons)
+
+lemma erase2jumpover1:
+  "\<lbrakk>q < length list; 
+             \<forall>rn. <drop q list> \<noteq> Oc # Oc \<up> abc_lm_v (a # list) (Suc q) @ Bk # <drop (Suc q) list> @ Bk \<up> rn\<rbrakk>
+       \<Longrightarrow> <drop q list> = Oc # Oc \<up> abc_lm_v (a # list) (Suc q)"
+apply(erule_tac x = 0 in allE, simp)
+apply(case_tac "Suc q < length list")
+apply(erule_tac notE)
+apply(rule_tac drop_tape_of_cons, simp_all add: abc_lm_v.simps)
+apply(subgoal_tac "length list = Suc q", auto)
+apply(subgoal_tac "drop q list = [list ! q]")
+apply(simp add: tape_of_nl_abv tape_of_nat_abv)
+by (metis append_Nil2 append_eq_conv_conj drop_Suc_conv_tl lessI)
+
+lemma erase2jumpover2:
+  "\<lbrakk>q < length list; \<forall>rn. <drop q list> @ Bk # Bk \<up> n \<noteq>
+  Oc # Oc \<up> abc_lm_v (a # list) (Suc q) @ Bk # <drop (Suc q) list> @ Bk \<up> rn\<rbrakk>
+  \<Longrightarrow> RR"
+apply(case_tac "Suc q < length list")
+apply(erule_tac x = "Suc n" in allE, simp)
+apply(erule_tac notE)
+apply(rule_tac drop_tape_of_cons, simp_all add: abc_lm_v.simps)
+apply(subgoal_tac "length list = Suc q", auto)
+apply(erule_tac x = "n" in allE, simp add: tape_of_nl_abv)
+by (metis append_Nil2 append_eq_conv_conj drop_Suc_conv_tl lessI replicate_Suc tape_of_nl_abv tape_of_nl_cons)
+
+lemma mopup_bef_erase_a_2_jump_over[simp]: 
+ "\<lbrakk>n < length lm; 0 < s; s mod 2 = Suc 0;  s \<le> 2 * n;
+   mopup_bef_erase_a (s, l, Bk # xs) lm n ires; \<not> (Suc (Suc s) \<le> 2 * n)\<rbrakk> 
+\<Longrightarrow> mopup_jump_over1 (s', Bk # l, xs) lm n ires"
+apply(auto simp: mopup_bef_erase_a.simps mopup_jump_over1.simps)
+apply(case_tac m, auto simp: mod_ex1)
+apply(subgoal_tac "n = Suc q", auto)
+apply(rule_tac x = "Suc ln" in exI, rule_tac x = 0 in exI, auto)
+apply(case_tac [!] lm, simp_all)
+apply(case_tac [!] rn, auto elim: erase2jumpover1 erase2jumpover2)
+apply(erule_tac x = 0 in allE, simp)
+apply(rule_tac classical, simp)
+apply(erule_tac notE)
+apply(rule_tac drop_tape_of_cons, simp_all add: abc_lm_v.simps)
+done
+
+lemma Suc_Suc_div:  "\<lbrakk>0 < s; s mod 2 = Suc 0; Suc (Suc s) \<le> 2 * n\<rbrakk>
+           \<Longrightarrow> (Suc (Suc (s div 2))) \<le> n"
+apply(arith)
+done
+
+lemma mopup_bef_erase_a_2_a[simp]: 
+ "\<lbrakk>n < length lm; 0 < s; s mod 2 = Suc 0; 
+   mopup_bef_erase_a (s, l, Bk # xs) lm n ires; 
+   Suc (Suc s) \<le> 2 * n\<rbrakk> \<Longrightarrow> 
+   mopup_bef_erase_a (Suc (Suc s), Bk # l, xs) lm n ires"
+apply(auto simp: mopup_bef_erase_a.simps)
+apply(subgoal_tac "drop (Suc (Suc (s div 2))) lm \<noteq> []")
+apply(case_tac m, simp_all)
+apply(rule_tac x = "Suc (abc_lm_v lm (Suc (s div 2)))" in exI, 
+      rule_tac x = rn in exI, auto simp: mod_ex1)
+apply(rule_tac drop_tape_of_cons)
+apply arith
+apply(simp add: abc_lm_v.simps)
+done
+
+lemma mopup_false2: 
+ "\<lbrakk>0 < s; s \<le> 2 * n; 
+   s mod 2 = Suc 0; Suc s \<noteq> 2 * n;
+   \<not> Suc (Suc s) \<le> 2 * n\<rbrakk> \<Longrightarrow> RR"
+apply(arith)
+done
+
+lemma [simp]: "mopup_bef_erase_a (s, l, []) lm n ires \<Longrightarrow> 
+                        mopup_bef_erase_a (s, l, [Bk]) lm n ires"
+apply(auto simp: mopup_bef_erase_a.simps)
+done
+
+lemma [simp]:
+   "\<lbrakk>n < length lm; 0 < s; s \<le> 2 * n; s mod 2 = Suc 0; \<not> Suc (Suc s) \<le> 2 *n;
+     mopup_bef_erase_a (s, l, []) lm n ires\<rbrakk>
+    \<Longrightarrow>  mopup_jump_over1 (s', Bk # l, []) lm n ires"
+by auto
+
+lemma "mopup_bef_erase_b (s, l, Oc # xs) lm n ires \<Longrightarrow> l \<noteq> []"
+apply(auto simp: mopup_bef_erase_b.simps)
+done
+
+lemma [simp]: "mopup_bef_erase_b (s, l, Oc # xs) lm n ires = False"
+apply(auto simp: mopup_bef_erase_b.simps )
+done
+ 
+lemma [simp]: "\<lbrakk>0 < s; s \<le> 2 *n; s mod 2 \<noteq> Suc 0\<rbrakk> \<Longrightarrow> 
+                                      (s - Suc 0) mod 2 = Suc 0"
+apply(arith)
+done
+
+lemma [simp]: "\<lbrakk>0 < s; s \<le> 2 *n; s mod 2 \<noteq> Suc 0\<rbrakk> \<Longrightarrow>
+                                       s - Suc 0 \<le> 2 * n"
+apply(simp)
+done
+
+lemma [simp]: "\<lbrakk>0 < s; s \<le> 2 *n; s mod 2 \<noteq> Suc 0\<rbrakk> \<Longrightarrow> \<not> s \<le> Suc 0"
+apply(arith)
+done
+
+lemma [simp]: "\<lbrakk>n < length lm; 0 < s; s \<le> 2 * n; 
+               s mod 2 \<noteq> Suc 0; 
+               mopup_bef_erase_b (s, l, Bk # xs) lm n ires; r = Bk # xs\<rbrakk> 
+           \<Longrightarrow> mopup_bef_erase_a (s - Suc 0, Bk # l, xs) lm n ires"
+apply(auto simp: mopup_bef_erase_b.simps mopup_bef_erase_a.simps)
+done
+
+lemma [simp]: "\<lbrakk>mopup_bef_erase_b (s, l, []) lm n ires\<rbrakk> \<Longrightarrow> 
+                   mopup_bef_erase_a (s - Suc 0, Bk # l, []) lm n ires"
+apply(auto simp: mopup_bef_erase_b.simps mopup_bef_erase_a.simps)
+done
+
+lemma [simp]: 
+   "\<lbrakk>n < length lm;
+    mopup_jump_over1 (Suc (2 * n), l, Oc # xs) lm n ires;
+    r = Oc # xs\<rbrakk>
+  \<Longrightarrow> mopup_jump_over1 (Suc (2 * n), Oc # l, xs) lm n ires"
+apply(auto simp: mopup_jump_over1.simps)
+apply(rule_tac x = ln in exI, rule_tac x = "Suc m1" in exI,
+       rule_tac x = "m2 - 1" in exI, simp)
+apply(case_tac "m2", simp, simp)
+apply(rule_tac x = ln in exI, rule_tac x = "Suc m1" in exI, 
+      rule_tac x = "m2 - 1" in exI)
+apply(case_tac m2, simp, simp)
+done
+
+lemma mopup_jump_over1_2_aft_erase_a[simp]:  
+ "\<lbrakk>n < length lm; mopup_jump_over1 (Suc (2 * n), l, Bk # xs) lm n ires\<rbrakk>
+  \<Longrightarrow> mopup_aft_erase_a (Suc (Suc (2 * n)), Bk # l, xs) lm n ires"
+apply(simp only: mopup_jump_over1.simps mopup_aft_erase_a.simps)
+apply(erule_tac exE)+
+apply(rule_tac x = ln in exI, rule_tac x = "Suc 0" in exI)
+apply(case_tac m2, simp)
+apply(rule_tac x = rn in exI, rule_tac x = "drop (Suc n) lm" in exI, 
+      simp)
+apply(simp)
+done
+
+lemma [simp]: 
+ "\<lbrakk>n < length lm; mopup_jump_over1 (Suc (2 * n), l, []) lm n ires\<rbrakk> \<Longrightarrow> 
+    mopup_aft_erase_a (Suc (Suc (2 * n)), Bk # l, []) lm n ires"
+apply(rule mopup_jump_over1_2_aft_erase_a, simp)
+apply(auto simp: mopup_jump_over1.simps)
+apply(rule_tac x = ln in exI, rule_tac x = "Suc (abc_lm_v lm n)" in exI, 
+      rule_tac x = 0 in exI, simp add: )
+done
+
+
+lemma [simp]: 
+ "\<lbrakk>n < length lm; 
+   mopup_aft_erase_a (Suc (Suc (2 * n)), l, Oc # xs) lm n ires\<rbrakk> 
+ \<Longrightarrow> mopup_aft_erase_b (Suc (Suc (Suc (2 * n))), l, Bk # xs) lm n ires"
+apply(auto simp: mopup_aft_erase_a.simps mopup_aft_erase_b.simps )
+apply(case_tac ml)
+apply(simp_all add: tape_of_nl_cons split: if_splits)
+apply(case_tac a, simp_all)
+apply(rule_tac x = rn in exI, rule_tac x = "[]" in exI, simp)
+apply(rule_tac x = rn in exI, rule_tac x = "[nat]" in exI, simp)
+apply(case_tac a, simp_all)
+apply(rule_tac x = rn in exI, rule_tac x = "list" in exI, simp)
+apply(rule_tac x = rn in exI)
+apply(rule_tac x = "nat # list" in exI, simp add: tape_of_nl_cons)
+done
+
+lemma [simp]:
+  "mopup_aft_erase_a (Suc (Suc (2 * n)), l, Bk # xs) lm n ires \<Longrightarrow> l \<noteq> []"
+apply(auto simp: mopup_aft_erase_a.simps)
+done
+
+lemma [simp]:
+  "\<lbrakk>n < length lm;
+    mopup_aft_erase_a (Suc (Suc (2 * n)), l, Bk # xs) lm n ires\<rbrakk>
+  \<Longrightarrow> mopup_left_moving (5 + 2 * n, tl l, hd l # Bk # xs) lm n ires"
+apply(simp only: mopup_aft_erase_a.simps mopup_left_moving.simps)
+apply(erule exE)+
+apply(case_tac lnr, simp)
+apply(case_tac ml, simp, simp add: tape_of_nl_cons split: if_splits)
+apply(auto)
+apply(case_tac ml, simp_all add: tape_of_nl_cons split: if_splits)
+apply(rule_tac x = "Suc rn" in exI, simp)
+done
+
+lemma [simp]:
+  "mopup_aft_erase_a (Suc (Suc (2 * n)), l, []) lm n ires \<Longrightarrow> l \<noteq> []"
+apply(simp only: mopup_aft_erase_a.simps)
+apply(erule exE)+
+apply(auto)
+done
+
+lemma [simp]:
+  "\<lbrakk>n < length lm; mopup_aft_erase_a (Suc (Suc (2 * n)), l, []) lm n ires\<rbrakk>
+  \<Longrightarrow> mopup_left_moving (5 + 2 * n, tl l, [hd l]) lm n ires"
+apply(simp only: mopup_aft_erase_a.simps mopup_left_moving.simps)
+apply(erule exE)+
+apply(subgoal_tac "ml = [] \<and> rn = 0", erule conjE, erule conjE, simp)
+apply(case_tac lnr, simp)
+apply(rule_tac x = lnl in exI, simp)
+apply(rule_tac x = 1 in exI, simp)
+apply(case_tac ml, simp, simp)
+done
+
+
+lemma [simp]: "mopup_aft_erase_b (2 * n + 3, l, Oc # xs) lm n ires = False"
+apply(auto simp: mopup_aft_erase_b.simps )
+done
+
+lemma tape_of_ex1[intro]: 
+  "\<exists>rna ml. Oc \<up> a @ Bk \<up> rn = <ml::nat list> @ Bk \<up> rna \<or> Oc \<up> a @ Bk \<up> rn = Bk # <ml> @ Bk \<up> rna"
+apply(case_tac a, simp_all)
+apply(rule_tac x = rn in exI, rule_tac x = "[]" in exI, simp)
+apply(rule_tac x = rn in exI, rule_tac x = "[nat]" in exI, simp)
+done
+
+lemma [intro]: "\<exists>rna ml. Oc \<up> a @ Bk # <list::nat list> @ Bk \<up> rn = 
+  <ml> @ Bk \<up> rna \<or> Oc \<up> a @ Bk # <list> @ Bk \<up> rn = Bk # <ml::nat list> @ Bk \<up> rna"
+apply(case_tac "list = []", simp add: replicate_Suc[THEN sym] del: replicate_Suc)
+apply(rule_tac rn = "Suc rn" in tape_of_ex1)
+apply(case_tac a, simp)
+apply(rule_tac x = rn in exI, rule_tac x = list in exI, simp)
+apply(rule_tac x = rn in exI, rule_tac x = "nat # list" in exI)
+apply(simp add: tape_of_nl_cons)
+done
+
+lemma [simp]: 
+ "\<lbrakk>n < length lm; 
+   mopup_aft_erase_c (2 * n + 4, l, Oc # xs) lm n ires\<rbrakk>
+  \<Longrightarrow> mopup_aft_erase_b (Suc (Suc (Suc (2 * n))), l, Bk # xs) lm n ires"
+apply(auto simp: mopup_aft_erase_c.simps mopup_aft_erase_b.simps )
+apply(case_tac ml, simp_all add: tape_of_nl_cons split: if_splits, auto)
+done
+
+lemma mopup_aft_erase_c_aft_erase_a[simp]: 
+ "\<lbrakk>n < length lm; mopup_aft_erase_c (2 * n + 4, l, Bk # xs) lm n ires\<rbrakk> 
+ \<Longrightarrow> mopup_aft_erase_a (Suc (Suc (2 * n)), Bk # l, xs) lm n ires"
+apply(simp only: mopup_aft_erase_c.simps mopup_aft_erase_a.simps )
+apply(erule_tac exE)+
+apply(erule conjE, erule conjE, erule disjE)
+apply(subgoal_tac "ml = []", simp, case_tac rn, 
+      simp, simp, rule conjI)
+apply(rule_tac x = lnl in exI, rule_tac x = "Suc lnr" in exI, simp)
+apply(rule_tac x = nat in exI, rule_tac x = "[]" in exI, simp)
+apply(case_tac ml, simp, simp add: tape_of_nl_cons split: if_splits)
+apply(rule_tac x = lnl in exI, rule_tac x = "Suc lnr" in exI, simp)
+apply(rule_tac x = rn in exI, rule_tac x = "ml" in exI, simp)
+done
+
+lemma [simp]: 
+ "\<lbrakk>n < length lm; mopup_aft_erase_c (2 * n + 4, l, []) lm n ires\<rbrakk> 
+ \<Longrightarrow> mopup_aft_erase_a (Suc (Suc (2 * n)), Bk # l, []) lm n ires"
+apply(rule mopup_aft_erase_c_aft_erase_a, simp)
+apply(simp only: mopup_aft_erase_c.simps)
+apply(erule exE)+
+apply(rule_tac x = lnl in exI, rule_tac x = lnr in exI, simp add: )
+apply(rule_tac x = 0 in exI, rule_tac x = "[]" in exI, simp)
+done
+
+lemma mopup_aft_erase_b_2_aft_erase_c[simp]:
+  "\<lbrakk>n < length lm; mopup_aft_erase_b (2 * n + 3, l, Bk # xs) lm n ires\<rbrakk>  
+ \<Longrightarrow> mopup_aft_erase_c (4 + 2 * n, Bk # l, xs) lm n ires"
+apply(auto simp: mopup_aft_erase_b.simps mopup_aft_erase_c.simps)
+apply(rule_tac x = "lnl" in exI, rule_tac x = "Suc lnr" in exI, simp)
+apply(rule_tac x = "lnl" in exI, rule_tac x = "Suc lnr" in exI, simp)
+done
+
+lemma [simp]: 
+ "\<lbrakk>n < length lm; mopup_aft_erase_b (2 * n + 3, l, []) lm n ires\<rbrakk> 
+ \<Longrightarrow> mopup_aft_erase_c (4 + 2 * n, Bk # l, []) lm n ires"
+apply(rule_tac mopup_aft_erase_b_2_aft_erase_c, simp)
+apply(simp add: mopup_aft_erase_b.simps)
+done
+
+lemma [simp]: 
+    "mopup_left_moving (2 * n + 5, l, Oc # xs) lm n ires \<Longrightarrow> l \<noteq> []"
+apply(auto simp: mopup_left_moving.simps)
+done
+
+lemma [simp]:  
+ "\<lbrakk>n < length lm; mopup_left_moving (2 * n + 5, l, Oc # xs) lm n ires\<rbrakk>
+  \<Longrightarrow> mopup_jump_over2 (2 * n + 6, tl l, hd l # Oc # xs) lm n ires"
+apply(simp only: mopup_left_moving.simps mopup_jump_over2.simps)
+apply(erule_tac exE)+
+apply(erule conjE, erule disjE, erule conjE)
+apply(case_tac rn, simp, simp add: )
+apply(case_tac "hd l", simp add:  )
+apply(case_tac "abc_lm_v lm n", simp)
+apply(rule_tac x = "lnl" in exI, rule_tac x = rn in exI, 
+      rule_tac x = "Suc 0" in exI, rule_tac x = 0 in exI)
+apply(case_tac lnl, simp, simp, simp add: exp_ind[THEN sym], simp)
+apply(case_tac "abc_lm_v lm n", simp)
+apply(case_tac lnl, simp, simp)
+apply(rule_tac x = lnl in exI, rule_tac x = rn in exI)
+apply(rule_tac x = nat in exI, rule_tac x = "Suc (Suc 0)" in exI, simp)
+done
+
+lemma [simp]: "mopup_left_moving (2 * n + 5, l, xs) lm n ires \<Longrightarrow> l \<noteq> []"
+apply(auto simp: mopup_left_moving.simps)
+done
+
+lemma [simp]:
+  "\<lbrakk>n < length lm; mopup_left_moving (2 * n + 5, l, Bk # xs) lm n ires\<rbrakk> 
+ \<Longrightarrow> mopup_left_moving (2 * n + 5, tl l, hd l # Bk # xs) lm n ires"
+apply(simp only: mopup_left_moving.simps)
+apply(erule exE)+
+apply(case_tac lnr, simp)
+apply(rule_tac x = lnl in exI, rule_tac x = nat in exI, simp)
+apply(rule_tac x = "Suc rn" in exI, simp)
+done
+
+lemma [simp]: 
+"\<lbrakk>n < length lm; mopup_left_moving (2 * n + 5, l, []) lm n ires\<rbrakk>
+    \<Longrightarrow> mopup_left_moving (2 * n + 5, tl l, [hd l]) lm n ires"
+apply(simp only: mopup_left_moving.simps)
+apply(erule exE)+
+apply(case_tac lnr, auto)
+done
+
+
+lemma [simp]: 
+ "mopup_jump_over2 (2 * n + 6, l, Oc # xs) lm n ires \<Longrightarrow> l \<noteq> []"
+apply(auto simp: mopup_jump_over2.simps )
+done
+
+lemma [simp]: 
+"\<lbrakk>n < length lm; mopup_jump_over2 (2 * n + 6, l, Oc # xs) lm n ires\<rbrakk>
+ \<Longrightarrow>  mopup_jump_over2 (2 * n + 6, tl l, hd l # Oc # xs) lm n ires"
+apply(simp only: mopup_jump_over2.simps)
+apply(erule_tac exE)+
+apply(simp add:  , erule conjE, erule_tac conjE)
+apply(case_tac m1, simp)
+apply(rule_tac x = ln in exI, rule_tac x = rn in exI, 
+      rule_tac x = 0 in exI, simp)
+apply(case_tac ln, simp, simp, simp only: exp_ind[THEN sym], simp)
+apply(rule_tac x = ln in exI, rule_tac x = rn in exI, 
+      rule_tac x = nat in exI, rule_tac x = "Suc m2" in exI, simp)
+done
+
+lemma [simp]: 
+ "\<lbrakk>n < length lm; mopup_jump_over2 (2 * n + 6, l, Bk # xs) lm n ires\<rbrakk> 
+  \<Longrightarrow> mopup_stop (0, Bk # l, xs) lm n ires"
+apply(auto simp: mopup_jump_over2.simps mopup_stop.simps)
+apply(simp_all add: tape_of_nat_abv exp_ind[THEN sym])
+done
+
+lemma [simp]: "mopup_jump_over2 (2 * n + 6, l, []) lm n ires = False"
+apply(simp only: mopup_jump_over2.simps, simp)
+done
+
+lemma mopup_inv_step:
+  "\<lbrakk>n < length lm; mopup_inv (s, l, r) lm n ires\<rbrakk>
+  \<Longrightarrow> mopup_inv (step (s, l, r) (mopup_a n @ shift mopup_b (2 * n), 0)) lm n ires"
+apply(case_tac r, case_tac [2] a)
+apply(auto split:if_splits simp add:step.simps)
+apply(simp_all add: mopupfetchs)
+done
+
+declare mopup_inv.simps[simp del]
+lemma mopup_inv_steps: 
+"\<lbrakk>n < length lm; mopup_inv (s, l, r) lm n ires\<rbrakk> \<Longrightarrow> 
+     mopup_inv (steps (s, l, r) (mopup_a n @ shift mopup_b (2 * n), 0)  stp) lm n ires"
+apply(induct_tac stp, simp add: steps.simps)
+apply(simp add: step_red)
+apply(case_tac "steps (s, l, r) 
+                (mopup_a n @ shift mopup_b (2 * n), 0) na", simp)
+apply(rule_tac mopup_inv_step, simp, simp)
+done
+
+fun abc_mopup_stage1 :: "config \<Rightarrow> nat \<Rightarrow> nat"
+  where
+  "abc_mopup_stage1 (s, l, r) n = 
+           (if s > 0 \<and> s \<le> 2*n then 6
+            else if s = 2*n + 1 then 4
+            else if s \<ge> 2*n + 2 \<and> s \<le> 2*n + 4 then 3
+            else if s = 2*n + 5 then 2
+            else if s = 2*n + 6 then 1
+            else 0)"
+
+fun abc_mopup_stage2 :: "config \<Rightarrow> nat \<Rightarrow> nat"
+  where
+  "abc_mopup_stage2 (s, l, r) n = 
+           (if s > 0 \<and> s \<le> 2*n then length r
+            else if s = 2*n + 1 then length r
+            else if s = 2*n + 5 then length l
+            else if s = 2*n + 6 then length l
+            else if s \<ge> 2*n + 2 \<and> s \<le> 2*n + 4 then length r
+            else 0)"
+
+fun abc_mopup_stage3 :: "config \<Rightarrow> nat \<Rightarrow> nat"
+  where
+  "abc_mopup_stage3 (s, l, r) n = 
+          (if s > 0 \<and> s \<le> 2*n then 
+              if hd r = Bk then 0
+              else 1
+           else if s = 2*n + 2 then 1 
+           else if s = 2*n + 3 then 0
+           else if s = 2*n + 4 then 2
+           else 0)"
+
+fun abc_mopup_measure :: "(config \<times> nat) \<Rightarrow> (nat \<times> nat \<times> nat)"
+  where
+  "abc_mopup_measure (c, n) = 
+    (abc_mopup_stage1 c n, abc_mopup_stage2 c n, 
+                                       abc_mopup_stage3 c n)"
+
+definition abc_mopup_LE ::
+   "(((nat \<times> cell list \<times> cell list) \<times> nat) \<times> 
+    ((nat \<times> cell list \<times> cell list) \<times> nat)) set"
+  where
+  "abc_mopup_LE \<equiv> (inv_image lex_triple abc_mopup_measure)"
+
+lemma wf_abc_mopup_le[intro]: "wf abc_mopup_LE"
+by(auto intro:wf_inv_image simp:abc_mopup_LE_def lex_triple_def lex_pair_def)
+
+lemma [simp]: "mopup_bef_erase_a (a, aa, []) lm n ires = False"
+apply(auto simp: mopup_bef_erase_a.simps)
+done
+
+lemma [simp]: "mopup_bef_erase_b (a, aa, []) lm n ires = False"
+apply(auto simp: mopup_bef_erase_b.simps) 
+done
+
+lemma [simp]: "mopup_aft_erase_b (2 * n + 3, aa, []) lm n ires = False"
+apply(auto simp: mopup_aft_erase_b.simps)
+done
+
+declare mopup_inv.simps[simp del]
+term mopup_inv
+
+lemma [simp]: 
+  "\<lbrakk>0 < q; q \<le> n\<rbrakk> \<Longrightarrow> 
+     (fetch (mopup_a n @ shift mopup_b (2 * n)) (2*q) Bk) = (R, 2*q - 1)"
+apply(case_tac q, simp, simp)
+apply(auto simp: fetch.simps nth_of.simps nth_append)
+apply(subgoal_tac "mopup_a n ! (4 * nat + 2) = 
+                     mopup_a (Suc nat) ! ((4 * nat) + 2)", 
+      simp add: mopup_a.simps nth_append)
+apply(rule mopup_a_nth, auto)
+done
+
+(* FIXME: is also in uncomputable *)
+lemma halt_lemma: 
+  "\<lbrakk>wf LE; \<forall>n. (\<not> P (f n) \<longrightarrow> (f (Suc n), (f n)) \<in> LE)\<rbrakk> \<Longrightarrow> \<exists>n. P (f n)"
+by (metis wf_iff_no_infinite_down_chain)
+
+
+lemma mopup_halt:
+  assumes 
+  less: "n < length lm"
+  and inv: "mopup_inv (Suc 0, l, r) lm n ires"
+  and f: "f = (\<lambda> stp. (steps (Suc 0, l, r) (mopup_a n @ shift mopup_b (2 * n), 0) stp, n))"
+  and P: "P = (\<lambda> (c, n). is_final c)"
+  shows "\<exists> stp. P (f stp)"
+proof(rule_tac LE = abc_mopup_LE in halt_lemma)
+  show "wf abc_mopup_LE" by(auto)
+next
+  show "\<forall>n. \<not> P (f n) \<longrightarrow> (f (Suc n), f n) \<in> abc_mopup_LE"
+  proof(rule_tac allI, rule_tac impI)
+    fix na
+    assume h: "\<not> P (f na)"
+    show "(f (Suc na), f na) \<in> abc_mopup_LE"
+    proof(simp add: f)
+      obtain a b c where g:"steps (Suc 0, l, r) (mopup_a n @ shift mopup_b (2 * n), 0) na = (a, b, c)"
+        apply(case_tac "steps (Suc 0, l, r) (mopup_a n @ shift mopup_b (2 * n), 0) na", auto)
+        done
+      then have "mopup_inv (a, b, c) lm n ires"
+        thm mopup_inv_steps
+        using inv less mopup_inv_steps[of n lm "Suc 0" l r ires na]
+        apply(simp)
+        done
+      moreover have "a > 0"
+        using h g
+        apply(simp add: f P)
+        done
+      ultimately have "((step (a, b, c) (mopup_a n @ shift mopup_b (2 * n), 0), n), (a, b, c), n) \<in> abc_mopup_LE"
+        apply(case_tac c, case_tac [2] aa)
+        apply(auto split:if_splits simp add:step.simps mopup_inv.simps)
+        apply(simp_all add: mopupfetchs abc_mopup_LE_def lex_triple_def lex_pair_def )
+        done
+      thus "((step (steps (Suc 0, l, r) (mopup_a n @ shift mopup_b (2 * n), 0) na) 
+        (mopup_a n @ shift mopup_b (2 * n), 0), n),
+        steps (Suc 0, l, r) (mopup_a n @ shift mopup_b (2 * n), 0) na, n)
+        \<in> abc_mopup_LE"
+        using g by simp
+    qed
+  qed
+qed     
+
+lemma mopup_inv_start: 
+  "n < length am \<Longrightarrow> mopup_inv (Suc 0, Bk # Bk # ires, <am> @ Bk \<up> k) am n ires"
+apply(auto simp: mopup_inv.simps mopup_bef_erase_a.simps mopup_jump_over1.simps)
+apply(case_tac [!] am, auto split: if_splits simp: tape_of_nl_cons)
+apply(rule_tac x = "Suc a" in exI, rule_tac x = k in exI, simp)
+apply(case_tac [!] n, simp_all add: abc_lm_v.simps)
+apply(case_tac k, simp, simp_all)
+done
+      
+lemma mopup_correct:
+  assumes less: "n < length (am::nat list)"
+  and rs: "abc_lm_v am n = rs"
+  shows "\<exists> stp i j. (steps (Suc 0, Bk # Bk # ires, <am> @ Bk \<up> k) (mopup_a n @ shift mopup_b (2 * n), 0) stp)
+    = (0, Bk\<up>i @ Bk # Bk # ires, Oc # Oc\<up> rs @ Bk\<up>j)"
+using less
+proof -
+  have a: "mopup_inv (Suc 0, Bk # Bk # ires, <am> @ Bk \<up> k) am n ires"
+    using less
+    apply(simp add: mopup_inv_start)
+    done    
+  then have "\<exists> stp. is_final (steps (Suc 0, Bk # Bk # ires, <am> @ Bk \<up> k) (mopup_a n @ shift mopup_b (2 * n), 0) stp)"
+    using less mopup_halt[of n am  "Bk # Bk # ires" "<am> @ Bk \<up> k" ires
+      "(\<lambda>stp. (steps (Suc 0, Bk # Bk # ires, <am> @ Bk \<up> k) (mopup_a n @ shift mopup_b (2 * n), 0) stp, n))"
+      "(\<lambda>(c, n). is_final c)"]
+    apply(simp)
+    done
+  from this obtain stp where b:
+    "is_final (steps (Suc 0, Bk # Bk # ires, <am> @ Bk \<up> k) (mopup_a n @ shift mopup_b (2 * n), 0) stp)" ..
+  from a b have
+    "mopup_inv (steps (Suc 0, Bk # Bk # ires, <am> @ Bk \<up> k) (mopup_a n @ shift mopup_b (2 * n), 0) stp)
+    am n ires"
+    apply(rule_tac mopup_inv_steps, simp_all add: less)
+    done    
+  from b and this show "?thesis"
+    apply(rule_tac x = stp in exI, simp)
+    apply(case_tac "steps (Suc 0, Bk # Bk # ires, <am> @ Bk \<up> k) 
+      (mopup_a n @ shift mopup_b (2 * n), 0) stp")
+    apply(simp add: mopup_inv.simps mopup_stop.simps rs)
+    using rs
+    apply(simp add: tape_of_nat_abv)
+    done
+qed
+
+(*we can use Hoare_plus here*)
+
+lemma wf_mopup[intro]: "tm_wf (mopup n, 0)"
+apply(induct n, simp add: mopup.simps shift.simps mopup_b_def tm_wf.simps)
+apply(auto simp: mopup.simps shift.simps mopup_b_def tm_wf.simps)
+done
+
+lemma length_tp:
+  "\<lbrakk>ly = layout_of ap; tp = tm_of ap\<rbrakk> \<Longrightarrow> 
+  start_of ly (length ap) = Suc (length tp div 2)"
+apply(frule_tac length_tp', simp_all)
+apply(simp add: start_of.simps)
+done
+
+lemma compile_correct_halt: 
+  assumes layout: "ly = layout_of ap"
+  and compile: "tp = tm_of ap"
+  and crsp: "crsp ly (0, lm) (Suc 0, l, r) ires"
+  and abc_halt: "abc_steps_l (0, lm) ap stp = (length ap, am)"
+  and rs_loc: "n < length am"
+  and rs: "abc_lm_v am n = rs"
+  and off: "off = length tp div 2"
+  shows "\<exists> stp i j. steps (Suc 0, l, r) (tp @ shift (mopup n) off, 0) stp = (0, Bk\<up>i @ Bk # Bk # ires, Oc\<up>Suc rs @ Bk\<up>j)"
+proof -
+  have "\<exists> stp k. steps (Suc 0, l, r) (tp, 0) stp = (Suc off, Bk # Bk # ires, <am> @ Bk\<up>k)"
+    using assms tp_correct'[of ly ap tp lm l r ires stp am]
+    by(simp add: length_tp)
+  then obtain stp k where "steps (Suc 0, l, r) (tp, 0) stp = (Suc off, Bk # Bk # ires, <am> @ Bk\<up>k)"
+    by blast
+  then have a: "steps (Suc 0, l, r) (tp@shift (mopup n) off , 0) stp = (Suc off, Bk # Bk # ires, <am> @ Bk\<up>k)"
+    using assms
+    by(auto intro: tm_append_first_steps_eq)
+  have "\<exists> stp i j. (steps (Suc 0, Bk # Bk # ires, <am> @ Bk \<up> k) (mopup_a n @ shift mopup_b (2 * n), 0) stp)
+    = (0, Bk\<up>i @ Bk # Bk # ires, Oc # Oc\<up> rs @ Bk\<up>j)"
+    using assms
+    by(auto intro: mopup_correct)
+  then obtain stpb i j where 
+    "steps (Suc 0, Bk # Bk # ires, <am> @ Bk \<up> k) (mopup_a n @ shift mopup_b (2 * n), 0) stpb
+    = (0, Bk\<up>i @ Bk # Bk # ires, Oc # Oc\<up> rs @ Bk\<up>j)" by blast
+  then have b: "steps (Suc 0 + off, Bk # Bk # ires, <am> @ Bk \<up> k) (tp @ shift (mopup n) off, 0) stpb
+    = (0, Bk\<up>i @ Bk # Bk # ires, Oc # Oc\<up> rs @ Bk\<up>j)"
+    using assms wf_mopup
+   thm tm_append_second_halt_eq
+    apply(drule_tac tm_append_second_halt_eq, auto)
+    done
+  from a b show "?thesis"
+    by(rule_tac x = "stp + stpb" in exI, simp add: steps_add)
+qed
+ 
+declare mopup.simps[simp del]
+lemma abc_step_red2:
+  "abc_steps_l (s, lm) p (Suc n) = (let (as', am') = abc_steps_l (s, lm) p n in
+                                    abc_step_l (as', am') (abc_fetch as' p))"
+apply(case_tac "abc_steps_l (s, lm) p n", simp)
+apply(drule_tac abc_step_red, simp)
+done
+
+lemma crsp_steps2:
+  assumes 
+  layout: "ly = layout_of ap"
+  and compile: "tp = tm_of ap"
+  and crsp: "crsp ly (0, lm) (Suc 0, l, r) ires"
+  and nothalt: "as < length ap"
+  and aexec: "abc_steps_l (0, lm) ap stp = (as, am)"
+  shows "\<exists>stpa\<ge>stp. crsp ly (as, am) (steps (Suc 0, l, r) (tp, 0) stpa) ires"
+using nothalt aexec
+proof(induct stp arbitrary: as am)
+  case 0
+  thus "?case"
+    using crsp
+    by(rule_tac x = 0 in exI, auto simp: abc_steps_l.simps steps.simps crsp)
+next
+  case (Suc stp as am)
+  have ind: 
+    "\<And> as am.  \<lbrakk>as < length ap; abc_steps_l (0, lm) ap stp = (as, am)\<rbrakk> 
+    \<Longrightarrow> \<exists>stpa\<ge>stp. crsp ly (as, am) (steps (Suc 0, l, r) (tp, 0) stpa) ires" by fact
+  have a: "as < length ap" by fact
+  have b: "abc_steps_l (0, lm) ap (Suc stp) = (as, am)" by fact
+  obtain as' am' where c: "abc_steps_l (0, lm) ap stp = (as', am')" 
+    by(case_tac "abc_steps_l (0, lm) ap stp", auto)
+  then have d: "as' < length ap"
+    using a b
+    by(simp add: abc_step_red2, case_tac "as' < length ap", simp,
+      simp add: abc_fetch.simps abc_steps_l.simps abc_step_l.simps)
+  have "\<exists>stpa\<ge>stp. crsp ly (as', am') (steps (Suc 0, l, r) (tp, 0) stpa) ires"
+    using d c ind by simp
+  from this obtain stpa where e: 
+    "stpa \<ge> stp \<and>  crsp ly (as', am') (steps (Suc 0, l, r) (tp, 0) stpa) ires"
+    by blast
+  obtain s' l' r' where f: "steps (Suc 0, l, r) (tp, 0) stpa = (s', l', r')"
+    by(case_tac "steps (Suc 0, l, r) (tp, 0) stpa", auto)
+  obtain ins where g: "abc_fetch as' ap = Some ins" using d 
+    by(case_tac "abc_fetch as' ap",auto simp: abc_fetch.simps)
+  then have "\<exists>stp> (0::nat). crsp ly (abc_step_l (as', am') (Some ins)) 
+    (steps (s', l', r') (tp, 0) stp) ires "
+    using layout compile e f 
+    by(rule_tac crsp_step, simp_all)
+  then obtain stpb where "stpb > 0 \<and> crsp ly (abc_step_l (as', am') (Some ins)) 
+    (steps (s', l', r') (tp, 0) stpb) ires" ..
+  from this show "?case" using b e g f c
+    by(rule_tac x = "stpa + stpb" in exI, simp add: steps_add abc_step_red2)
+qed
+    
+lemma compile_correct_unhalt: 
+  assumes layout: "ly = layout_of ap"
+  and compile: "tp = tm_of ap"
+  and crsp: "crsp ly (0, lm) (Suc 0, l, r) ires"
+  and off: "off = length tp div 2"
+  and abc_unhalt: "\<forall> stp. (\<lambda> (as, am). as < length ap) (abc_steps_l (0, lm) ap stp)"
+  shows "\<forall> stp.\<not> is_final (steps (Suc 0, l, r) (tp @ shift (mopup n) off, 0) stp)"
+using assms
+proof(rule_tac allI, rule_tac notI)
+  fix stp
+  assume h: "is_final (steps (Suc 0, l, r) (tp @ shift (mopup n) off, 0) stp)"
+  obtain as am where a: "abc_steps_l (0, lm) ap stp = (as, am)"
+    by(case_tac "abc_steps_l (0, lm) ap stp", auto)
+  then have b: "as < length ap"
+    using abc_unhalt
+    by(erule_tac x = stp in allE, simp)
+  have "\<exists> stpa\<ge>stp. crsp ly (as, am) (steps (Suc 0, l, r) (tp, 0) stpa) ires "
+    using assms b a
+    apply(rule_tac crsp_steps2, simp_all)
+    done
+  then obtain stpa where
+    "stpa\<ge>stp \<and> crsp ly (as, am) (steps (Suc 0, l, r) (tp, 0) stpa) ires" ..
+  then obtain s' l' r' where b: "(steps (Suc 0, l, r) (tp, 0) stpa) = (s', l', r') \<and> 
+       stpa\<ge>stp \<and> crsp ly (as, am) (s', l', r') ires"
+    by(case_tac "steps (Suc 0, l, r) (tp, 0) stpa", auto)
+  hence c:
+    "(steps (Suc 0, l, r) (tp @ shift (mopup n) off, 0) stpa) = (s', l', r')"
+    by(rule_tac tm_append_first_steps_eq, simp_all add: crsp.simps)
+  from b have d: "s' > 0 \<and> stpa \<ge> stp"
+    by(simp add: crsp.simps)
+  then obtain diff where e: "stpa = stp + diff"   by (metis le_iff_add)
+  obtain s'' l'' r'' where f:
+    "steps (Suc 0, l, r) (tp @ shift (mopup n) off, 0) stp = (s'', l'', r'') \<and> is_final (s'', l'', r'')"
+    using h
+    by(case_tac "steps (Suc 0, l, r) (tp @ shift (mopup n) off, 0) stp", auto)
+
+  then have "is_final (steps (s'', l'', r'') (tp @ shift (mopup n) off, 0) diff)"
+    by(auto intro: after_is_final)
+  then have "is_final (steps (Suc 0, l, r) (tp @ shift (mopup n) off, 0) stpa)"
+    using e
+    by(simp add: steps_add f)
+  from this and c d show "False" by simp
+qed
+
+end
+