(* Title: thys/Recursive.thy
   Author: Jian Xu, Xingyuan Zhang, and Christian Urban
*)

header {* Translating Recursive Functions into Abacus Machines *}

theory Recursive
imports Rec_Def Abacus
begin


text {*
  Some auxilliary Abacus machines used to construct the result Abacus machines.
*}

text {*
  @{text "get_paras_num recf"} returns the arity of recursive function @{text "recf"}.
*}
fun get_paras_num :: "recf \<Rightarrow> nat"
  where
  "get_paras_num z = 1" |
  "get_paras_num s = 1" |
  "get_paras_num (id m n) = m" |
  "get_paras_num (Cn n f gs) = n" |
  "get_paras_num (Pr n f g) = Suc n"  |
  "get_paras_num (Mn n f) = n"  

fun addition :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> abc_prog"
  where
  "addition m n p = [Dec m 4, Inc n, Inc p, Goto 0, Dec p 7, Inc m, Goto 4]"

fun mv_box :: "nat \<Rightarrow> nat \<Rightarrow> abc_prog"
  where
  "mv_box m n = [Dec m 3, Inc n, Goto 0]"

fun abc_inst_shift :: "abc_inst \<Rightarrow> nat \<Rightarrow> abc_inst"
  where
  "abc_inst_shift (Inc m) n = Inc m" |
  "abc_inst_shift (Dec m e) n = Dec m (e + n)" |
  "abc_inst_shift (Goto m) n = Goto (m + n)"

fun abc_shift :: "abc_inst list \<Rightarrow> nat \<Rightarrow> abc_inst list" 
  where
  "abc_shift xs n = map (\<lambda> x. abc_inst_shift x n) xs" 

fun abc_append :: "abc_inst list \<Rightarrow> abc_inst list \<Rightarrow> 
                           abc_inst list" (infixl "[+]" 60)
  where
  "abc_append al bl = (let al_len = length al in 
                           al @ abc_shift bl al_len)"

text {* The compilation of @{text "z"}-operator. *}
definition rec_ci_z :: "abc_inst list"
  where
  "rec_ci_z \<equiv> [Goto 1]"

text {* The compilation of @{text "s"}-operator. *}
definition rec_ci_s :: "abc_inst list"
  where
  "rec_ci_s \<equiv> (addition 0 1 2 [+] [Inc 1])"


text {* The compilation of @{text "id i j"}-operator *}
fun rec_ci_id :: "nat \<Rightarrow> nat \<Rightarrow> abc_inst list"
  where
  "rec_ci_id i j = addition j i (i + 1)"

fun mv_boxes :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> abc_inst list"
  where
  "mv_boxes ab bb 0 = []" |
  "mv_boxes ab bb (Suc n) = mv_boxes ab bb n [+] mv_box (ab + n) (bb + n)"

fun empty_boxes :: "nat \<Rightarrow> abc_inst list"
  where
  "empty_boxes 0 = []" |
  "empty_boxes (Suc n) = empty_boxes n [+] [Dec n 2, Goto 0]"

fun cn_merge_gs ::
  "(abc_inst list \<times> nat \<times> nat) list \<Rightarrow> nat \<Rightarrow> abc_inst list"
  where
  "cn_merge_gs [] p = []" |
  "cn_merge_gs (g # gs) p = 
      (let (gprog, gpara, gn) = g in 
         gprog [+] mv_box gpara p [+] cn_merge_gs gs (Suc p))"


text {*
  The compiler of recursive functions, where @{text "rec_ci recf"} return 
  @{text "(ap, arity, fp)"}, where @{text "ap"} is the Abacus program, @{text "arity"} is the 
  arity of the recursive function @{text "recf"}, 
  @{text "fp"} is the amount of memory which is going to be
  used by @{text "ap"} for its execution. 
*}

fun rec_ci :: "recf \<Rightarrow> abc_inst list \<times> nat \<times> nat"
  where
  "rec_ci z = (rec_ci_z, 1, 2)" |
  "rec_ci s = (rec_ci_s, 1, 3)" |
  "rec_ci (id m n) = (rec_ci_id m n, m, m + 2)" |
  "rec_ci (Cn n f gs) = 
      (let cied_gs = map (\<lambda> g. rec_ci g) gs in
       let (fprog, fpara, fn) = rec_ci f in 
       let pstr = Max (set (Suc n # fn # (map (\<lambda> (aprog, p, n). n) cied_gs))) in
       let qstr = pstr + Suc (length gs) in 
       (cn_merge_gs cied_gs pstr [+] mv_boxes 0 qstr n [+] 
          mv_boxes pstr 0 (length gs) [+] fprog [+] 
            mv_box fpara pstr [+] empty_boxes (length gs) [+] 
             mv_box pstr n [+] mv_boxes qstr 0 n, n,  qstr + n))" |
  "rec_ci (Pr n f g) = 
         (let (fprog, fpara, fn) = rec_ci f in 
          let (gprog, gpara, gn) = rec_ci g in 
          let p = Max (set ([n + 3, fn, gn])) in 
          let e = length gprog + 7 in 
           (mv_box n p [+] fprog [+] mv_box n (Suc n) [+] 
               (([Dec p e] [+] gprog [+] 
                 [Inc n, Dec (Suc n) 3, Goto 1]) @
                     [Dec (Suc (Suc n)) 0, Inc (Suc n), Goto (length gprog + 4)]),
             Suc n, p + 1))" |
  "rec_ci (Mn n f) =
         (let (fprog, fpara, fn) = rec_ci f in 
          let len = length (fprog) in 
            (fprog @ [Dec (Suc n) (len + 5), Dec (Suc n) (len + 3),
             Goto (len + 1), Inc n, Goto 0], n, max (Suc n) fn))"

declare rec_ci.simps [simp del] rec_ci_s_def[simp del] 
        rec_ci_z_def[simp del] rec_ci_id.simps[simp del]
        mv_boxes.simps[simp del] abc_append.simps[simp del]
        mv_box.simps[simp del] addition.simps[simp del]
  
declare abc_steps_l.simps[simp del] abc_fetch.simps[simp del] 
        abc_step_l.simps[simp del] 

lemma abc_steps_add: 
  "abc_steps_l (as, lm) ap (m + n) = 
         abc_steps_l (abc_steps_l (as, lm) ap m) ap n"
apply(induct m arbitrary: n as lm, simp add: abc_steps_l.simps)
proof -
  fix m n as lm
  assume ind: 
    "\<And>n as lm. abc_steps_l (as, lm) ap (m + n) = 
                   abc_steps_l (abc_steps_l (as, lm) ap m) ap n"
  show "abc_steps_l (as, lm) ap (Suc m + n) = 
             abc_steps_l (abc_steps_l (as, lm) ap (Suc m)) ap n"
    apply(insert ind[of as lm "Suc n"], simp)
    apply(insert ind[of as lm "Suc 0"], simp add: abc_steps_l.simps)
    apply(case_tac "(abc_steps_l (as, lm) ap m)", simp)
    apply(simp add: abc_steps_l.simps)
    apply(case_tac "abc_step_l (a, b) (abc_fetch a ap)", 
          simp add: abc_steps_l.simps)
    done
qed

(*lemmas: rec_ci and rec_calc_rel*)

lemma rec_calc_inj_case_z: 
  "\<lbrakk>rec_calc_rel z l x; rec_calc_rel z l y\<rbrakk> \<Longrightarrow> x = y"
apply(auto elim: calc_z_reverse)
done

lemma  rec_calc_inj_case_s: 
  "\<lbrakk>rec_calc_rel s l x; rec_calc_rel s l y\<rbrakk> \<Longrightarrow> x = y"
apply(auto elim: calc_s_reverse)
done

lemma rec_calc_inj_case_id:
  "\<lbrakk>rec_calc_rel (recf.id nat1 nat2) l x;
    rec_calc_rel (recf.id nat1 nat2) l y\<rbrakk> \<Longrightarrow> x = y"
apply(auto elim: calc_id_reverse)
done

lemma rec_calc_inj_case_mn:
  assumes ind: "\<And> l x y. \<lbrakk>rec_calc_rel f l x; rec_calc_rel f l y\<rbrakk> 
           \<Longrightarrow> x = y" 
  and h: "rec_calc_rel (Mn n f) l x" "rec_calc_rel (Mn n f) l y"
  shows "x = y"
  apply(insert h)
  apply(elim  calc_mn_reverse)
  apply(case_tac "x > y", simp)
  apply(erule_tac x = "y" in allE, auto)
proof -
  fix v va
  assume "rec_calc_rel f (l @ [y]) 0" 
    "rec_calc_rel f (l @ [y]) v"  
    "0 < v"
  thus "False"
    apply(insert ind[of "l @ [y]" 0 v], simp)
    done
next
  fix v va
  assume 
    "rec_calc_rel f (l @ [x]) 0" 
    "\<forall>x<y. \<exists>v. rec_calc_rel f (l @ [x]) v \<and> 0 < v" "\<not> y < x"
  thus "x = y"
    apply(erule_tac x = "x" in allE)
    apply(case_tac "x = y", auto)
    apply(drule_tac y = v in ind, simp, simp)
    done
qed 

lemma rec_calc_inj_case_pr: 
  assumes f_ind: 
  "\<And>l x y. \<lbrakk>rec_calc_rel f l x; rec_calc_rel f l y\<rbrakk> \<Longrightarrow> x = y"
  and g_ind:
  "\<And>x xa y xb ya l xc yb. 
  \<lbrakk>x = rec_ci f; (xa, y) = x; (xb, ya) = y; 
  rec_calc_rel g l xc; rec_calc_rel g l yb\<rbrakk> \<Longrightarrow> xc = yb"
  and h: "rec_calc_rel (Pr n f g) l x" "rec_calc_rel (Pr n f g) l y"  
  shows "x = y"
  apply(case_tac "rec_ci f")
proof -
  fix a b c
  assume "rec_ci f = (a, b, c)"
  hence ng_ind: 
    "\<And> l xc yb. \<lbrakk>rec_calc_rel g l xc; rec_calc_rel g l yb\<rbrakk>
    \<Longrightarrow> xc = yb"
    apply(insert g_ind[of "(a, b, c)" "a" "(b, c)" b c], simp)
    done
  from h show "x = y"
    apply(erule_tac calc_pr_reverse, erule_tac calc_pr_reverse)
    apply(erule f_ind, simp, simp)
    apply(erule_tac calc_pr_reverse, simp, simp)
  proof -
    fix la ya ry laa yaa rya
    assume k1:  "rec_calc_rel g (la @ [ya, ry]) x" 
      "rec_calc_rel g (la @ [ya, rya]) y"
      and k2: "rec_calc_rel (Pr (length la) f g) (la @ [ya]) ry"
              "rec_calc_rel (Pr (length la) f g) (la @ [ya]) rya"
    from k2 have "ry = rya"
      apply(induct ya arbitrary: ry rya)
      apply(erule_tac calc_pr_reverse, 
        erule_tac calc_pr_reverse, simp)
      apply(erule f_ind, simp, simp, simp)
      apply(erule_tac calc_pr_reverse, simp)
      apply(erule_tac rSucy = rya in calc_pr_reverse, simp, simp)
    proof -
      fix ya ry rya l y ryb laa yb ryc
      assume ind:
        "\<And>ry rya. \<lbrakk>rec_calc_rel (Pr (length l) f g) (l @ [y]) ry; 
                   rec_calc_rel (Pr (length l) f g) (l @ [y]) rya\<rbrakk> \<Longrightarrow> ry = rya"
        and j: "rec_calc_rel (Pr (length l) f g) (l @ [y]) ryb"
        "rec_calc_rel g (l @ [y, ryb]) ry" 
        "rec_calc_rel (Pr (length l) f g) (l @ [y]) ryc" 
        "rec_calc_rel g (l @ [y, ryc]) rya"
      from j show "ry = rya"
	apply(insert ind[of ryb ryc], simp)
	apply(insert ng_ind[of "l @ [y, ryc]" ry rya], simp)
	done
    qed 
    from k1 and this show "x = y"
      apply(simp)
      apply(insert ng_ind[of "la @ [ya, rya]" x y], simp)
      done
  qed  
qed

lemma Suc_nth_part_eq:
  "\<forall>k<Suc (length list). (a # xs) ! k = (aa # list) ! k
       \<Longrightarrow> \<forall>k<(length list). (xs) ! k = (list) ! k"
apply(rule allI, rule impI)
apply(erule_tac x = "Suc k" in allE, simp)
done


lemma list_eq_intro:  
  "\<lbrakk>length xs = length ys; \<forall> k < length xs. xs ! k = ys ! k\<rbrakk> 
  \<Longrightarrow> xs = ys"
apply(induct xs arbitrary: ys, simp)
apply(case_tac ys, simp, simp)
proof -
  fix a xs ys aa list
  assume ind: 
    "\<And>ys. \<lbrakk>length list = length ys; \<forall>k<length ys. xs ! k = ys ! k\<rbrakk>
    \<Longrightarrow> xs = ys"
    and h: "length xs = length list" 
    "\<forall>k<Suc (length list). (a # xs) ! k = (aa # list) ! k"
  from h show "a = aa \<and> xs = list"
    apply(insert ind[of list], simp)
    apply(frule Suc_nth_part_eq, simp)
    apply(erule_tac x = "0" in allE, simp)
    done
qed

lemma rec_calc_inj_case_cn: 
  assumes ind: 
  "\<And>x l xa y.
  \<lbrakk>x = f \<or> x \<in> set gs; rec_calc_rel x l xa; rec_calc_rel x l y\<rbrakk>
  \<Longrightarrow> xa = y"
  and h: "rec_calc_rel (Cn n f gs) l x" 
         "rec_calc_rel (Cn n f gs) l y"
  shows "x = y"
  apply(insert h, elim  calc_cn_reverse)
  apply(subgoal_tac "rs = rsa")
  apply(rule_tac x = f and l = rsa and xa = x and y = y in ind, 
        simp, simp, simp)
  apply(intro list_eq_intro, simp, rule allI, rule impI)
  apply(erule_tac x = k in allE, rule_tac x = k in allE, simp, simp)
  apply(rule_tac x = "gs ! k" in ind, simp, simp, simp)
  done

lemma rec_calc_inj:
  "\<lbrakk>rec_calc_rel f l x; 
    rec_calc_rel f l y\<rbrakk> \<Longrightarrow> x = y"
apply(induct f arbitrary: l x y rule: rec_ci.induct)
apply(simp add: rec_calc_inj_case_z)
apply(simp add: rec_calc_inj_case_s)
apply(simp add: rec_calc_inj_case_id)
apply (metis rec_calc_inj_case_cn)
apply(erule rec_calc_inj_case_pr, auto)
apply(erule rec_calc_inj_case_mn, auto)
done


lemma calc_rel_reverse_ind_step_ex: 
  "\<lbrakk>rec_calc_rel (Pr n f g) (lm @ [Suc x]) rs\<rbrakk> 
  \<Longrightarrow> \<exists> rs. rec_calc_rel (Pr n f g) (lm @ [x]) rs"
apply(erule calc_pr_reverse, simp, simp)
apply(rule_tac x = rk in exI, simp)
done

lemma [simp]: "Suc x \<le> y \<Longrightarrow> Suc (y - Suc x) = y - x"
by arith

lemma calc_pr_para_not_null: 
  "rec_calc_rel (Pr n f g) lm rs \<Longrightarrow> lm \<noteq> []"
apply(erule calc_pr_reverse, simp, simp)
done

lemma calc_pr_less_ex: 
 "\<lbrakk>rec_calc_rel (Pr n f g) lm rs; x \<le> last lm\<rbrakk> \<Longrightarrow> 
 \<exists>rs. rec_calc_rel (Pr n f g) (butlast lm @ [last lm - x]) rs"
apply(subgoal_tac "lm \<noteq> []")
apply(induct x, rule_tac x = rs in exI, simp, simp, erule exE)
apply(rule_tac rs = xa in calc_rel_reverse_ind_step_ex, simp)
apply(simp add: calc_pr_para_not_null)
done

lemma calc_pr_zero_ex:
  "rec_calc_rel (Pr n f g) lm rs \<Longrightarrow> 
             \<exists>rs. rec_calc_rel f (butlast lm) rs"
apply(drule_tac x = "last lm" in calc_pr_less_ex, simp,
      erule_tac exE, simp)
apply(erule_tac calc_pr_reverse, simp)
apply(rule_tac x = rs in exI, simp, simp)
done


lemma abc_steps_ind: 
  "abc_steps_l (as, am) ap (Suc stp) =
          abc_steps_l (abc_steps_l (as, am) ap stp) ap (Suc 0)"
apply(insert abc_steps_add[of as am ap stp "Suc 0"], simp)
done

lemma abc_steps_zero: "abc_steps_l asm ap 0 = asm"
apply(case_tac asm, simp add: abc_steps_l.simps)
done

lemma abc_append_nth: 
  "n < length ap + length bp \<Longrightarrow> 
       (ap [+] bp) ! n =
         (if n < length ap then ap ! n 
          else abc_inst_shift (bp ! (n - length ap)) (length ap))"
apply(simp add: abc_append.simps nth_append map_nth split: if_splits)
done

lemma abc_state_keep:  
  "as \<ge> length bp \<Longrightarrow> abc_steps_l (as, lm) bp stp = (as, lm)"
apply(induct stp, simp add: abc_steps_zero)
apply(simp add: abc_steps_ind)
apply(simp add: abc_steps_zero)
apply(simp add: abc_steps_l.simps abc_fetch.simps abc_step_l.simps)
done

lemma abc_halt_equal: 
  "\<lbrakk>abc_steps_l (0, lm) bp stpa = (length bp, lm1); 
    abc_steps_l (0, lm) bp stpb = (length bp, lm2)\<rbrakk> \<Longrightarrow> lm1 = lm2"
apply(case_tac "stpa - stpb > 0")
apply(insert abc_steps_add[of 0 lm bp stpb "stpa - stpb"], simp)
apply(insert abc_state_keep[of bp "length bp" lm2 "stpa - stpb"], 
      simp, simp add: abc_steps_zero)
apply(insert abc_steps_add[of 0 lm bp stpa "stpb - stpa"], simp)
apply(insert abc_state_keep[of bp "length bp" lm1 "stpb - stpa"], 
      simp)
done  

lemma abc_halt_point_ex: 
  "\<lbrakk>\<exists>stp. abc_steps_l (0, lm) bp stp = (bs, lm');
    bs = length bp; bp \<noteq> []\<rbrakk> 
  \<Longrightarrow> \<exists> stp. (\<lambda> (s, l). s < bs \<and> 
              (abc_steps_l (s, l) bp (Suc 0)) = (bs, lm')) 
      (abc_steps_l (0, lm) bp stp) "
apply(erule_tac exE)
proof -
  fix stp
  assume "bs = length bp" 
         "abc_steps_l (0, lm) bp stp = (bs, lm')" 
         "bp \<noteq> []"
  thus 
    "\<exists>stp. (\<lambda>(s, l). s < bs \<and> 
      abc_steps_l (s, l) bp (Suc 0) = (bs, lm')) 
                       (abc_steps_l (0, lm) bp stp)"
    apply(induct stp, simp add: abc_steps_zero, simp)
  proof -
    fix stpa
    assume ind: 
     "abc_steps_l (0, lm) bp stpa = (length bp, lm')
       \<Longrightarrow> \<exists>stp. (\<lambda>(s, l). s < length bp  \<and> abc_steps_l (s, l) bp 
             (Suc 0) = (length bp, lm')) (abc_steps_l (0, lm) bp stp)"
    and h: "abc_steps_l (0, lm) bp (Suc stpa) = (length bp, lm')" 
           "abc_steps_l (0, lm) bp stp = (length bp, lm')" 
           "bp \<noteq> []"
    from h show 
      "\<exists>stp. (\<lambda>(s, l). s < length bp \<and> abc_steps_l (s, l) bp (Suc 0)
                    = (length bp, lm')) (abc_steps_l (0, lm) bp stp)"
      apply(case_tac "abc_steps_l (0, lm) bp stpa", 
            case_tac "a = length bp")
      apply(insert ind, simp)
      apply(subgoal_tac "b = lm'", simp)
      apply(rule_tac abc_halt_equal, simp, simp)
      apply(rule_tac x = stpa in exI, simp add: abc_steps_ind)
      apply(simp add: abc_steps_zero)
      apply(rule classical, simp add: abc_steps_l.simps 
                             abc_fetch.simps abc_step_l.simps)
      done
  qed
qed  


lemma abc_append_empty_r[simp]: "[] [+] ab = ab"
apply(simp add: abc_append.simps abc_inst_shift.simps)
apply(induct ab, simp, simp)
apply(case_tac a, simp_all add: abc_inst_shift.simps)
done

lemma abc_append_empty_l[simp]:  "ab [+] [] = ab"
apply(simp add: abc_append.simps abc_inst_shift.simps)
done


lemma abc_append_length[simp]:  
  "length (ap [+] bp) = length ap + length bp"
apply(simp add: abc_append.simps)
done

declare Let_def[simp]

lemma abc_append_commute: "as [+] bs [+] cs = as [+] (bs [+] cs)"
apply(simp add: abc_append.simps abc_shift.simps abc_inst_shift.simps)
apply(induct cs, simp, simp)
apply(case_tac a, auto simp: abc_inst_shift.simps Let_def)
done

lemma abc_halt_point_step[simp]: 
  "\<lbrakk>a < length bp; abc_steps_l (a, b) bp (Suc 0) = (length bp, lm')\<rbrakk>
  \<Longrightarrow> abc_steps_l (length ap + a, b) (ap [+] bp [+] cp) (Suc 0) = 
                                        (length ap + length bp, lm')"
apply(simp add: abc_steps_l.simps abc_fetch.simps abc_append_nth)
apply(case_tac "bp ! a", 
                      auto simp: abc_steps_l.simps abc_step_l.simps)
done

lemma abc_step_state_in:
  "\<lbrakk>bs < length bp;  abc_steps_l (a, b) bp (Suc 0) = (bs, l)\<rbrakk>
  \<Longrightarrow> a < length bp"
apply(simp add: abc_steps_l.simps abc_fetch.simps)
apply(rule_tac classical, 
      simp add: abc_step_l.simps abc_steps_l.simps)
done


lemma abc_append_state_in_exc: 
  "\<lbrakk>bs < length bp; abc_steps_l (0, lm) bp stpa = (bs, l)\<rbrakk>
 \<Longrightarrow> abc_steps_l (length ap, lm) (ap [+] bp [+] cp) stpa = 
                                             (length ap + bs, l)"
apply(induct stpa arbitrary: bs l, simp add: abc_steps_zero)
proof -
  fix stpa bs l
  assume ind: 
    "\<And>bs l. \<lbrakk>bs < length bp; abc_steps_l (0, lm) bp stpa = (bs, l)\<rbrakk>
    \<Longrightarrow> abc_steps_l (length ap, lm) (ap [+] bp [+] cp) stpa = 
                                                (length ap + bs, l)"
    and h: "bs < length bp" 
           "abc_steps_l (0, lm) bp (Suc stpa) = (bs, l)"
  from h show 
    "abc_steps_l (length ap, lm) (ap [+] bp [+] cp) (Suc stpa) = 
                                                (length ap + bs, l)"
    apply(simp add: abc_steps_ind)
    apply(case_tac "(abc_steps_l (0, lm) bp stpa)", simp)
  proof -
    fix a b
    assume g: "abc_steps_l (0, lm) bp stpa = (a, b)" 
              "abc_steps_l (a, b) bp (Suc 0) = (bs, l)"
    from h and g have k1: "a < length bp"
      apply(simp add: abc_step_state_in)
      done
    from h and g and k1 show 
   "abc_steps_l (abc_steps_l (length ap, lm) (ap [+] bp [+] cp) stpa) 
              (ap [+] bp [+] cp) (Suc 0) = (length ap + bs, l)"
      apply(insert ind[of a b], simp)
      apply(simp add: abc_steps_l.simps abc_fetch.simps 
                      abc_append_nth)
      apply(case_tac "bp ! a", auto simp: 
                                 abc_steps_l.simps abc_step_l.simps)
      done
  qed
qed

lemma [simp]: "abc_steps_l (0, am) [] stp = (0, am)"
apply(induct stp, simp add: abc_steps_zero)
apply(simp add: abc_steps_ind)
apply(simp add: abc_steps_zero abc_steps_l.simps 
                abc_fetch.simps abc_step_l.simps)
done

lemma abc_append_exc1:
  "\<lbrakk>\<exists> stp. abc_steps_l (0, lm) bp stp = (bs, lm');
    bs = length bp; 
    as = length ap\<rbrakk>
    \<Longrightarrow> \<exists> stp. abc_steps_l (as, lm) (ap [+] bp [+] cp) stp 
                                                 = (as + bs, lm')"
apply(case_tac "bp = []", erule_tac exE, simp,
      rule_tac x = 0 in exI, simp add: abc_steps_zero)
apply(frule_tac abc_halt_point_ex, simp, simp,
      erule_tac exE, erule_tac exE) 
apply(rule_tac x = "stpa + Suc 0" in exI)
apply(case_tac "(abc_steps_l (0, lm) bp stpa)", 
      simp add: abc_steps_ind)
apply(subgoal_tac 
  "abc_steps_l (length ap, lm) (ap [+] bp [+] cp) stpa 
                                   = (length ap + a, b)", simp)
apply(simp add: abc_steps_zero)
apply(rule_tac abc_append_state_in_exc, simp, simp)
done

lemma abc_append_exc3: 
  "\<lbrakk>\<exists> stp. abc_steps_l (0, am) bp stp = (bs, bm); ss = length ap\<rbrakk>
   \<Longrightarrow>  \<exists> stp. abc_steps_l (ss, am) (ap [+] bp) stp = (bs + ss, bm)"
apply(erule_tac exE)
proof -
  fix stp
  assume h: "abc_steps_l (0, am) bp stp = (bs, bm)" "ss = length ap"
  thus " \<exists>stp. abc_steps_l (ss, am) (ap [+] bp) stp = (bs + ss, bm)"
  proof(induct stp arbitrary: bs bm)
    fix bs bm
    assume "abc_steps_l (0, am) bp 0 = (bs, bm)"
    thus "\<exists>stp. abc_steps_l (ss, am) (ap [+] bp) stp = (bs + ss, bm)"
      apply(rule_tac x = 0 in exI, simp add: abc_steps_l.simps)
      done
  next
    fix stp bs bm
    assume ind: 
      "\<And>bs bm. \<lbrakk>abc_steps_l (0, am) bp stp = (bs, bm);
                 ss = length ap\<rbrakk> \<Longrightarrow> 
          \<exists>stp. abc_steps_l (ss, am) (ap [+] bp) stp = (bs + ss, bm)"
    and g: "abc_steps_l (0, am) bp (Suc stp) = (bs, bm)"
    from g show 
      "\<exists>stp. abc_steps_l (ss, am) (ap [+] bp) stp = (bs + ss, bm)"
      apply(insert abc_steps_add[of 0 am bp stp "Suc 0"], simp)
      apply(case_tac "(abc_steps_l (0, am) bp stp)", simp)
    proof -
      fix a b
      assume "(bs, bm) = abc_steps_l (a, b) bp (Suc 0)" 
             "abc_steps_l (0, am) bp (Suc stp) = 
                       abc_steps_l (a, b) bp (Suc 0)" 
              "abc_steps_l (0, am) bp stp = (a, b)"
      thus "?thesis"
	apply(insert ind[of a b], simp add: h, erule_tac exE)
	apply(rule_tac x = "Suc stp" in exI)
	apply(simp only: abc_steps_ind, simp add: abc_steps_zero)
      proof -
	fix stp
	assume "(bs, bm) = abc_steps_l (a, b) bp (Suc 0)"
	thus "abc_steps_l (a + length ap, b) (ap [+] bp) (Suc 0)
                                              = (bs + length ap, bm)"
	  apply(simp add: abc_steps_l.simps abc_steps_zero
                          abc_fetch.simps split: if_splits)
	  apply(case_tac "bp ! a", 
                simp_all add: abc_inst_shift.simps abc_append_nth
                   abc_steps_l.simps abc_steps_zero abc_step_l.simps)
	  apply(auto)
	  done
      qed
    qed
  qed
qed

lemma abc_add_equal:
  "\<lbrakk>ap \<noteq> []; 
    abc_steps_l (0, am) ap astp = (a, b);
    a < length ap\<rbrakk>
     \<Longrightarrow> (abc_steps_l (0, am) (ap @ bp) astp) = (a, b)"
apply(induct astp arbitrary: a b, simp add: abc_steps_l.simps, simp)
apply(simp add: abc_steps_ind)
apply(case_tac "(abc_steps_l (0, am) ap astp)")
proof -
  fix astp a b aa ba
  assume ind: 
    "\<And>a b. \<lbrakk>abc_steps_l (0, am) ap astp = (a, b); 
             a < length ap\<rbrakk> \<Longrightarrow> 
                  abc_steps_l (0, am) (ap @ bp) astp = (a, b)"
  and h: "abc_steps_l (abc_steps_l (0, am) ap astp) ap (Suc 0)
                                                            = (a, b)"
        "a < length ap" 
        "abc_steps_l (0, am) ap astp = (aa, ba)"
  from h show "abc_steps_l (abc_steps_l (0, am) (ap @ bp) astp)
                                        (ap @ bp) (Suc 0) = (a, b)"
    apply(insert ind[of aa ba], simp)
    apply(subgoal_tac "aa < length ap", simp)
    apply(simp add: abc_steps_l.simps abc_fetch.simps
                     nth_append abc_steps_zero)
    apply(rule abc_step_state_in, auto)
    done
qed


lemma abc_add_exc1: 
  "\<lbrakk>\<exists> astp. abc_steps_l (0, am) ap astp = (as, bm); as = length ap\<rbrakk>
  \<Longrightarrow> \<exists> stp. abc_steps_l (0, am) (ap @ bp) stp = (as, bm)"
apply(case_tac "ap = []", simp, 
      rule_tac x = 0 in exI, simp add: abc_steps_zero)
apply(drule_tac abc_halt_point_ex, simp, simp)
apply(erule_tac exE, case_tac "(abc_steps_l (0, am) ap astp)", simp)
apply(rule_tac x = "Suc astp" in exI, simp add: abc_steps_ind, auto)
apply(frule_tac bp = bp in abc_add_equal, simp, simp, simp)
apply(simp add: abc_steps_l.simps abc_steps_zero 
                abc_fetch.simps nth_append)
done

declare abc_shift.simps[simp del] 

lemma abc_append_exc2: 
  "\<lbrakk>\<exists> astp. abc_steps_l (0, am) ap astp = (as, bm); as = length ap; 
    \<exists> bstp. abc_steps_l (0, bm) bp bstp = (bs, bm'); bs = length bp;
    cs = as + bs; bp \<noteq> []\<rbrakk>
  \<Longrightarrow> \<exists> stp. abc_steps_l (0, am) (ap [+] bp) stp = (cs, bm')"
apply(insert abc_append_exc1[of bm bp bs bm' as ap "[]"], simp)
apply(drule_tac bp = "abc_shift bp (length ap)" in abc_add_exc1, simp)
apply(subgoal_tac "ap @ abc_shift bp (length ap) = ap [+] bp", 
      simp, auto)
apply(rule_tac x = "stpa + stp" in exI, simp add: abc_steps_add)
apply(simp add: abc_append.simps)
done
lemma exponent_add_iff: "a\<up>b @ a\<up>c@ xs = a\<up>(b+c) @ xs"
apply(auto simp: replicate_add)
done

lemma exponent_cons_iff: "a # a\<up>c @ xs = a\<up>(Suc c) @ xs"
apply(auto simp: replicate_add)
done

lemma  [simp]: "length lm = n \<Longrightarrow>  
  abc_steps_l (Suc 0, lm @ Suc x # 0 # suf_lm) 
       [Inc n, Dec (Suc n) 3, Goto (Suc 0)] (Suc (Suc 0))
                                  = (3, lm @ Suc x # 0 # suf_lm)"
apply(simp add: abc_steps_l.simps abc_fetch.simps 
                abc_step_l.simps abc_lm_v.simps abc_lm_s.simps 
                nth_append list_update_append)
done

lemma [simp]: 
  "length lm = n \<Longrightarrow> 
  abc_steps_l (Suc 0, lm @ Suc x # Suc y # suf_lm) 
     [Inc n, Dec (Suc n) 3, Goto (Suc 0)] (Suc (Suc 0))
  = (Suc 0, lm @ Suc x # y # suf_lm)"
apply(simp add: abc_steps_l.simps abc_fetch.simps 
                abc_step_l.simps abc_lm_v.simps abc_lm_s.simps 
                nth_append list_update_append)
done

lemma pr_cycle_part_middle_inv: 
  "\<lbrakk>length lm = n\<rbrakk> \<Longrightarrow> 
  \<exists> stp. abc_steps_l (0, lm @ x # y # suf_lm) 
                         [Inc n, Dec (Suc n) 3, Goto (Suc 0)] stp 
  = (3, lm @ Suc x # 0 # suf_lm)"
proof -
  assume h: "length lm = n"
  hence k1: "\<exists> stp. abc_steps_l (0, lm @ x # y # suf_lm) 
                           [Inc n, Dec (Suc n) 3, Goto (Suc 0)] stp 
    = (Suc 0, lm @ Suc x # y # suf_lm)"
    apply(rule_tac x = "Suc 0" in exI)
    apply(simp add: abc_steps_l.simps abc_step_l.simps 
                    abc_lm_v.simps abc_lm_s.simps nth_append 
                    list_update_append abc_fetch.simps)
    done
  from h have k2: 
    "\<exists> stp. abc_steps_l (Suc 0, lm @ Suc x # y # suf_lm)
                      [Inc n, Dec (Suc n) 3, Goto (Suc 0)] stp 
    = (3, lm @ Suc x # 0 # suf_lm)"
    apply(induct y)
    apply(rule_tac x = "Suc (Suc 0)" in exI, simp, simp, 
          erule_tac exE)
    apply(rule_tac x = "Suc (Suc 0) + stp" in exI, 
          simp only: abc_steps_add, simp)
    done      
  from k1 and k2 show 
    "\<exists> stp. abc_steps_l (0, lm @ x # y # suf_lm) 
                       [Inc n, Dec (Suc n) 3, Goto (Suc 0)] stp 
    = (3, lm @ Suc x # 0 # suf_lm)"
    apply(erule_tac exE, erule_tac exE)
    apply(rule_tac x = "stp + stpa" in exI, simp add: abc_steps_add)
    done
qed

lemma [simp]: 
  "length lm = Suc n \<Longrightarrow> 
  (abc_steps_l (length ap, lm @ x # Suc y # suf_lm) 
           (ap @ [Dec (Suc (Suc n)) 0, Inc (Suc n), Goto (length ap)]) 
                    (Suc (Suc (Suc 0))))
  = (length ap, lm @ Suc x # y # suf_lm)"
apply(simp add: abc_steps_l.simps abc_fetch.simps abc_step_l.simps 
         abc_lm_v.simps list_update_append nth_append abc_lm_s.simps)
done

lemma switch_para_inv:
  assumes bp_def:"bp =  ap @ [Dec (Suc (Suc n)) 0, Inc (Suc n), Goto ss]"
  and h: "rec_ci (Pr n f g) = (aprog, rs_pos, a_md)" 
         "ss = length ap" 
         "length lm = Suc n"
  shows " \<exists>stp. abc_steps_l (ss, lm @ x # y # suf_lm) bp stp =
                               (0, lm @ (x + y) # 0 # suf_lm)"
apply(induct y arbitrary: x)
apply(rule_tac x = "Suc 0" in exI,
  simp add: bp_def mv_box.simps abc_steps_l.simps 
            abc_fetch.simps h abc_step_l.simps 
            abc_lm_v.simps list_update_append nth_append
            abc_lm_s.simps)
proof -
  fix y x
  assume ind: 
    "\<And>x. \<exists>stp. abc_steps_l (ss, lm @ x # y # suf_lm) bp stp = 
                                     (0, lm @ (x + y) # 0 # suf_lm)"
  show "\<exists>stp. abc_steps_l (ss, lm @ x # Suc y # suf_lm) bp stp = 
                                  (0, lm @ (x + Suc y) # 0 # suf_lm)"
    apply(insert ind[of "Suc x"], erule_tac exE)
    apply(rule_tac x = "Suc (Suc (Suc 0)) + stp" in exI, 
          simp only: abc_steps_add bp_def h)
    apply(simp add: h)
    done
qed

lemma [simp]:
  "length lm = rs_pos \<and> Suc (Suc rs_pos) < a_md \<and> 0 < rs_pos \<Longrightarrow> 
      a_md - Suc 0 < Suc (Suc (Suc (a_md + length suf_lm - 
                                         Suc (Suc (Suc 0)))))"
apply(arith)
done

lemma [simp]: 
  "Suc (Suc rs_pos) < a_md \<and> 0 < rs_pos \<Longrightarrow> 
                           \<not> a_md - Suc 0 < rs_pos - Suc 0"
apply(arith)
done

lemma [simp]: 
  "Suc (Suc rs_pos) < a_md \<and> 0 < rs_pos \<Longrightarrow> 
           \<not> a_md - rs_pos < Suc (Suc (a_md - Suc (Suc rs_pos)))"
apply(arith)
done

lemma butlast_append_last: "lm \<noteq> [] \<Longrightarrow> lm = butlast lm @ [last lm]"
apply(auto)
done

lemma [simp]: "rec_ci (Pr n f g) = (aprog, rs_pos, a_md)
           \<Longrightarrow> (Suc (Suc rs_pos)) < a_md"
apply(simp add: rec_ci.simps)
apply(case_tac "rec_ci f", simp)
apply(case_tac "rec_ci g", simp)
apply(arith)
done

lemma ci_pr_para_eq: "rec_ci (Pr n f g) = (aprog, rs_pos, a_md)
                  \<Longrightarrow> rs_pos = Suc n"
apply(simp add: rec_ci.simps)
apply(case_tac "rec_ci g",  case_tac "rec_ci f", simp)
done

lemma [intro]:  
  "\<lbrakk>rec_ci z = (aprog, rs_pos, a_md); rec_calc_rel z lm xs\<rbrakk>
  \<Longrightarrow> length lm = rs_pos"
apply(simp add: rec_ci.simps rec_ci_z_def)
apply(erule_tac calc_z_reverse, simp)
done

lemma [intro]: 
  "\<lbrakk>rec_ci s = (aprog, rs_pos, a_md); rec_calc_rel s lm xs\<rbrakk>
  \<Longrightarrow> length lm = rs_pos"
apply(simp add: rec_ci.simps rec_ci_s_def)
apply(erule_tac calc_s_reverse, simp)
done

lemma [intro]: 
  "\<lbrakk>rec_ci (recf.id nat1 nat2) = (aprog, rs_pos, a_md); 
    rec_calc_rel (recf.id nat1 nat2) lm xs\<rbrakk> \<Longrightarrow> length lm = rs_pos"
apply(simp add: rec_ci.simps rec_ci_id.simps)
apply(erule_tac calc_id_reverse, simp)
done

lemma [intro]: 
  "\<lbrakk>rec_ci (Cn n f gs) = (aprog, rs_pos, a_md); 
    rec_calc_rel (Cn n f gs) lm xs\<rbrakk> \<Longrightarrow> length lm = rs_pos"
apply(erule_tac calc_cn_reverse, simp)
apply(simp add: rec_ci.simps)
apply(case_tac "rec_ci f",  simp)
done

lemma [intro]:
  "\<lbrakk>rec_ci (Pr n f g) = (aprog, rs_pos, a_md); 
    rec_calc_rel (Pr n f g) lm xs\<rbrakk> \<Longrightarrow> length lm = rs_pos"
apply(erule_tac  calc_pr_reverse, simp)
apply(drule_tac ci_pr_para_eq, simp, simp)
apply(drule_tac ci_pr_para_eq, simp)
done

lemma [intro]: 
  "\<lbrakk>rec_ci (Mn n f) = (aprog, rs_pos, a_md);
    rec_calc_rel (Mn n f) lm xs\<rbrakk> \<Longrightarrow> length lm = rs_pos"
apply(erule_tac calc_mn_reverse)
apply(simp add: rec_ci.simps)
apply(case_tac "rec_ci f",  simp)
done

lemma para_pattern: 
  "\<lbrakk>rec_ci f = (aprog, rs_pos, a_md); rec_calc_rel f lm xs\<rbrakk>
  \<Longrightarrow> length lm = rs_pos"
apply(case_tac f, auto)
done

lemma ci_pr_g_paras:
  "\<lbrakk>rec_ci (Pr n f g) = (aprog, rs_pos, a_md);
    rec_ci g = (a, aa, ba);
    rec_calc_rel (Pr n f g) (lm @ [x]) rs; x > 0\<rbrakk> \<Longrightarrow> 
    aa = Suc rs_pos "
apply(erule calc_pr_reverse, simp)
apply(subgoal_tac "length (args @ [k, rk]) = aa", simp)
apply(subgoal_tac "rs_pos = Suc n", simp)
apply(simp add: ci_pr_para_eq)
apply(erule para_pattern, simp)
done

lemma ci_pr_g_md_less: 
  "\<lbrakk>rec_ci (Pr n f g) = (aprog, rs_pos, a_md); 
    rec_ci g = (a, aa, ba)\<rbrakk> \<Longrightarrow> ba < a_md"
apply(simp add: rec_ci.simps)
apply(case_tac "rec_ci f",  auto)
done

lemma [intro]: "rec_ci z = (ap, rp, ad) \<Longrightarrow> rp < ad"
  by(simp add: rec_ci.simps)

lemma [intro]: "rec_ci s = (ap, rp, ad) \<Longrightarrow> rp < ad"
  by(simp add: rec_ci.simps)

lemma [intro]: "rec_ci (recf.id nat1 nat2) = (ap, rp, ad) \<Longrightarrow> rp < ad"
  by(simp add: rec_ci.simps)

lemma [intro]: "rec_ci (Cn n f gs) = (ap, rp, ad) \<Longrightarrow> rp < ad"
apply(simp add: rec_ci.simps)
apply(case_tac "rec_ci f",  simp)
done

lemma [intro]: "rec_ci (Pr n f g) = (ap, rp, ad) \<Longrightarrow> rp < ad"
apply(simp add: rec_ci.simps)
by(case_tac "rec_ci f", case_tac "rec_ci g",  auto)

lemma [intro]: "rec_ci (Mn n f) = (ap, rp, ad) \<Longrightarrow> rp < ad"
apply(simp add: rec_ci.simps)
apply(case_tac "rec_ci f", simp)
apply(arith)
done

lemma ci_ad_ge_paras: "rec_ci f = (ap, rp, ad) \<Longrightarrow> ad > rp"
apply(case_tac f, auto)
done

lemma [elim]: "\<lbrakk>a [+] b = []; a \<noteq> [] \<or> b \<noteq> []\<rbrakk> \<Longrightarrow> RR"
apply(auto simp: abc_append.simps abc_shift.simps)
done

lemma [intro]: "rec_ci z = ([], aa, ba) \<Longrightarrow> False"
by(simp add: rec_ci.simps rec_ci_z_def)

lemma [intro]: "rec_ci s = ([], aa, ba) \<Longrightarrow> False"
by(auto simp: rec_ci.simps rec_ci_s_def addition.simps)

lemma [intro]: "rec_ci (id m n) = ([], aa, ba) \<Longrightarrow> False"
by(auto simp: rec_ci.simps rec_ci_id.simps addition.simps)

lemma [intro]: "rec_ci (Cn n f gs) = ([], aa, ba) \<Longrightarrow> False"
apply(case_tac "rec_ci f", auto simp: rec_ci.simps abc_append.simps)
apply(simp add: abc_shift.simps mv_box.simps)
done

lemma [intro]: "rec_ci (Pr n f g) = ([], aa, ba) \<Longrightarrow> False"
apply(simp add: rec_ci.simps)
apply(case_tac "rec_ci f", case_tac "rec_ci g")
by(auto)

lemma [intro]: "rec_ci (Mn n f) = ([], aa, ba) \<Longrightarrow> False"
apply(case_tac "rec_ci f", auto simp: rec_ci.simps)
done

lemma rec_ci_not_null:  "rec_ci g = (a, aa, ba) \<Longrightarrow> a \<noteq> []"
by(case_tac g, auto)

lemma calc_pr_g_def:
 "\<lbrakk>rec_calc_rel (Pr rs_pos f g) (lm @ [Suc x]) rsa;
   rec_calc_rel (Pr rs_pos f g) (lm @ [x]) rsxa\<rbrakk>
 \<Longrightarrow> rec_calc_rel g (lm @ [x, rsxa]) rsa"
apply(erule_tac calc_pr_reverse, simp, simp)
apply(subgoal_tac "rsxa = rk", simp)
apply(erule_tac rec_calc_inj, auto)
done

lemma ci_pr_md_def: 
  "\<lbrakk>rec_ci (Pr n f g) = (aprog, rs_pos, a_md);
    rec_ci g = (a, aa, ba); rec_ci f = (ab, ac, bc)\<rbrakk>
  \<Longrightarrow> a_md = Suc (max (n + 3) (max bc ba))"
by(simp add: rec_ci.simps)

lemma  ci_pr_f_paras: 
  "\<lbrakk>rec_ci (Pr n f g) = (aprog, rs_pos, a_md);
    rec_calc_rel (Pr n f g) lm rs;
    rec_ci f = (ab, ac, bc)\<rbrakk>  \<Longrightarrow> ac = rs_pos - Suc 0"
apply(subgoal_tac "\<exists>rs. rec_calc_rel f (butlast lm) rs", 
      erule_tac exE)
apply(drule_tac f = f and lm = "butlast lm" in para_pattern, 
      simp, simp)
apply(drule_tac para_pattern, simp)
apply(subgoal_tac "lm \<noteq> []", simp)
apply(erule_tac calc_pr_reverse, simp, simp)
apply(erule calc_pr_zero_ex)
done

lemma ci_pr_md_ge_f:  "\<lbrakk>rec_ci (Pr n f g) = (aprog, rs_pos, a_md);
        rec_ci f = (ab, ac, bc)\<rbrakk> \<Longrightarrow> Suc bc \<le> a_md"
apply(case_tac "rec_ci g")
apply(simp add: rec_ci.simps, auto)
done

lemma ci_pr_md_ge_g:  "\<lbrakk>rec_ci (Pr n f g) = (aprog, rs_pos, a_md);
        rec_ci g = (ab, ac, bc)\<rbrakk> \<Longrightarrow> bc < a_md"
apply(case_tac "rec_ci f")
apply(simp add: rec_ci.simps, auto)
done 

lemma rec_calc_rel_def0: 
  "\<lbrakk>rec_calc_rel (Pr n f g) lm rs; rec_calc_rel f (butlast lm) rsa\<rbrakk>
  \<Longrightarrow> rec_calc_rel (Pr n f g) (butlast lm @ [0]) rsa"
  apply(rule_tac calc_pr_zero, simp)
apply(erule_tac calc_pr_reverse, simp, simp, simp)
done

lemma [simp]:  "length (mv_box m n) = 3"
by (auto simp: mv_box.simps)


lemma [simp]: "\<lbrakk>rec_ci (Pr n f g) = (aprog, rs_pos, a_md); rec_calc_rel (Pr n f g) lm rs\<rbrakk>
    \<Longrightarrow> rs_pos = Suc n"
apply(simp add: ci_pr_para_eq)
done


lemma [simp]: "\<lbrakk>rec_ci (Pr n f g) = (aprog, rs_pos, a_md); rec_calc_rel (Pr n f g) lm rs\<rbrakk>
    \<Longrightarrow> length lm = Suc n"
apply(subgoal_tac "rs_pos = Suc n", rule_tac para_pattern, simp, simp)
apply(case_tac "rec_ci f", case_tac "rec_ci g", simp add: rec_ci.simps)
done

lemma [simp]: "rec_ci (Pr n f g) = (a, rs_pos, a_md) \<Longrightarrow> Suc (Suc n) < a_md"
apply(case_tac "rec_ci f", case_tac "rec_ci g", simp add: rec_ci.simps)
apply arith
done

lemma [simp]: "rec_ci (Pr n f g) = (aprog, rs_pos, a_md) \<Longrightarrow> 0 < rs_pos"
apply(case_tac "rec_ci f", case_tac "rec_ci g")
apply(simp add: rec_ci.simps)
done

lemma [simp]: "Suc (Suc rs_pos) < a_md \<Longrightarrow> 
       butlast lm @ (last lm - xa) # (rsa::nat) # 0 # 0\<up>(a_md - Suc (Suc (Suc rs_pos))) @ xa # suf_lm =
       butlast lm @ (last lm - xa) # rsa # 0\<up>(a_md - Suc (Suc rs_pos)) @ xa # suf_lm"
apply(simp add: replicate_Suc[THEN sym])
done

lemma pr_cycle_part_ind: 
  assumes g_ind: 
  "\<And>lm rs suf_lm. rec_calc_rel g lm rs \<Longrightarrow> 
  \<exists>stp. abc_steps_l (0, lm @ 0\<up>(ba - aa) @ suf_lm) a stp = 
                    (length a, lm @ rs # 0\<up>(ba - Suc aa) @ suf_lm)"
  and ap_def: 
  "ap = ([Dec (a_md - Suc 0) (length a + 7)] [+]
        (a [+] [Inc (rs_pos - Suc 0), Dec rs_pos 3, Goto (Suc 0)])) @
         [Dec (Suc (Suc n)) 0, Inc (Suc n), Goto (length a + 4)]"
  and h: "rec_ci (Pr n f g) = (aprog, rs_pos, a_md)" 
         "rec_calc_rel (Pr n f g) 
                   (butlast lm @ [last lm - Suc xa]) rsxa" 
         "Suc xa \<le> last lm" 
         "rec_ci g = (a, aa, ba)"
         "rec_calc_rel (Pr n f g) (butlast lm @ [last lm - xa]) rsa"
         "lm \<noteq> []"
  shows 
  "\<exists>stp. abc_steps_l 
     (0, butlast lm @ (last lm - Suc xa) # rsxa # 
               0\<up>(a_md - Suc (Suc rs_pos)) @ Suc xa # suf_lm) ap stp =
     (0, butlast lm @ (last lm - xa) # rsa
                 # 0\<up>(a_md - Suc (Suc rs_pos)) @ xa # suf_lm)"
proof -
  have k1: "\<exists>stp. abc_steps_l (0, butlast lm @ (last lm - Suc xa) #
    rsxa # 0\<up>(a_md - Suc (Suc rs_pos)) @ Suc xa # suf_lm) ap stp =
         (length a + 4, butlast lm @ (last lm - xa) # 0 # rsa #
                           0\<up>(a_md - Suc (Suc (Suc rs_pos))) @ xa # suf_lm)"
    apply(simp add: ap_def, rule_tac abc_add_exc1)
    apply(rule_tac as = "Suc 0" and 
      bm = "butlast lm @ (last lm - Suc xa) # 
      rsxa # 0\<up>(a_md - Suc (Suc rs_pos)) @ xa # suf_lm" in abc_append_exc2,
      auto)
  proof -
    show 
      "\<exists>astp. abc_steps_l (0, butlast lm @ (last lm - Suc xa) # rsxa 
                   # 0\<up>(a_md - Suc (Suc rs_pos)) @ Suc xa # suf_lm) 
              [Dec (a_md - Suc 0)(length a + 7)] astp =
      (Suc 0, butlast lm @ (last lm - Suc xa) # 
             rsxa # 0\<up>(a_md - Suc (Suc rs_pos)) @ xa # suf_lm)"
      apply(rule_tac x = "Suc 0" in exI, 
          simp add: abc_steps_l.simps abc_step_l.simps
                     abc_fetch.simps)
      apply(subgoal_tac "length lm = Suc n \<and> rs_pos = Suc n \<and>
                              a_md > Suc (Suc rs_pos)")
      apply(simp add: abc_lm_v.simps nth_append abc_lm_s.simps)
      apply(insert nth_append[of 
                 "(last lm - Suc xa) # rsxa # 0\<up>(a_md - Suc (Suc rs_pos))" 
                 "Suc xa # suf_lm" "(a_md - rs_pos)"], simp)
      apply(simp add: list_update_append del: list_update.simps)
      apply(insert list_update_append[of "(last lm - Suc xa) # rsxa # 
                                          0\<up>(a_md - Suc (Suc rs_pos))" 
                    "Suc xa # suf_lm" "a_md - rs_pos" "xa"], simp)
      apply(case_tac a_md, simp, simp)
      apply(insert h, simp)
      apply(insert para_pattern[of "Pr n f g" aprog rs_pos a_md 
                    "(butlast lm @ [last lm - Suc xa])" rsxa], simp)
      done
  next
    show "\<exists>bstp. abc_steps_l (0, butlast lm @ (last lm - Suc xa) # 
           rsxa # 0\<up>(a_md - Suc (Suc rs_pos)) @ xa # suf_lm) (a [+] 
            [Inc (rs_pos - Suc 0), Dec rs_pos 3, Goto (Suc 0)]) bstp =
         (3 + length a, butlast lm @ (last lm - xa) # 0 # rsa #
                          0\<up>(a_md - Suc (Suc (Suc rs_pos))) @ xa # suf_lm)"
      apply(rule_tac as = "length a" and
               bm = "butlast lm @ (last lm - Suc xa) # rsxa # rsa #
                     0\<up>(a_md - Suc (Suc (Suc rs_pos))) @ xa # suf_lm" 
        in abc_append_exc2, simp_all)
    proof -
      from h have j1: "aa = Suc rs_pos \<and> a_md > ba \<and> ba > Suc rs_pos"
	apply(insert h)
	apply(insert ci_pr_g_paras[of n f g aprog rs_pos
                 a_md a aa ba "butlast lm" "last lm - xa" rsa], simp)
	apply(drule_tac ci_pr_md_ge_g, auto)
	apply(erule_tac ci_ad_ge_paras)
	done
      from h have j2: "rec_calc_rel g (butlast lm @ 
                                  [last lm - Suc xa, rsxa]) rsa"
	apply(rule_tac  calc_pr_g_def, simp, simp)
	done
      from j1 and j2 show 
        "\<exists>astp. abc_steps_l (0, butlast lm @ (last lm - Suc xa) #
                rsxa # 0\<up>(a_md - Suc (Suc rs_pos)) @ xa # suf_lm) a astp =
        (length a, butlast lm @ (last lm - Suc xa) # rsxa # rsa 
                         # 0\<up>(a_md - Suc (Suc (Suc rs_pos))) @ xa # suf_lm)"
	apply(insert g_ind[of
          "butlast lm @ (last lm - Suc xa) # [rsxa]" rsa 
          "0\<up>(a_md - ba - Suc 0) @ xa # suf_lm"], simp, auto)
	apply(simp add: exponent_add_iff)
	apply(rule_tac x = stp in exI, simp add: numeral_3_eq_3)
	done
    next
      from h have j3: "length lm = rs_pos \<and> rs_pos > 0"
	apply(rule_tac conjI)
	apply(drule_tac lm = "(butlast lm @ [last lm - Suc xa])"
                          and xs = rsxa in para_pattern, simp, simp, simp)
        done
      from h have j4: "Suc (last lm - Suc xa) = last lm - xa"
	apply(case_tac "last lm", simp, simp)
	done
      from j3 and j4 show
      "\<exists>bstp. abc_steps_l (0, butlast lm @ (last lm - Suc xa) # rsxa #
                     rsa # 0\<up>(a_md - Suc (Suc (Suc rs_pos))) @ xa # suf_lm)
            [Inc (rs_pos - Suc 0), Dec rs_pos 3, Goto (Suc 0)] bstp =
        (3, butlast lm @ (last lm - xa) # 0 # rsa #
                       0\<up>(a_md - Suc (Suc (Suc rs_pos))) @ xa # suf_lm)"
	apply(insert pr_cycle_part_middle_inv[of "butlast lm" 
          "rs_pos - Suc 0" "(last lm - Suc xa)" rsxa 
          "rsa # 0\<up>(a_md - Suc (Suc (Suc rs_pos))) @ xa # suf_lm"], simp)
	done
    qed
  qed
  from h have k2: 
    "\<exists>stp. abc_steps_l (length a + 4, butlast lm @ (last lm - xa) # 0 
           # rsa # 0\<up>(a_md - Suc (Suc (Suc rs_pos))) @ xa # suf_lm) ap stp =
    (0, butlast lm @ (last lm - xa) # rsa # 0\<up>(a_md - Suc (Suc rs_pos)) @ xa # suf_lm)"
    apply(insert switch_para_inv[of ap 
      "([Dec (a_md - Suc 0) (length a + 7)] [+] 
      (a [+] [Inc (rs_pos - Suc 0), Dec rs_pos 3, Goto (Suc 0)]))"
      n "length a + 4" f g aprog rs_pos a_md 
      "butlast lm @ [last lm - xa]" 0 rsa 
      "0\<up>(a_md - Suc (Suc (Suc rs_pos))) @ xa # suf_lm"])
    apply(simp add: h ap_def)
    apply(subgoal_tac "length lm = Suc n \<and> Suc (Suc rs_pos) < a_md", 
          simp)
    apply(insert h, simp)
    apply(frule_tac lm = "(butlast lm @ [last lm - Suc xa])" 
      and xs = rsxa in para_pattern, simp, simp)
    done   
  from k1 and k2 show "?thesis"
    apply(auto)
    apply(rule_tac x = "stp + stpa" in exI, simp add: abc_steps_add)
    done
qed

lemma ci_pr_ex1: 
  "\<lbrakk>rec_ci (Pr n f g) = (aprog, rs_pos, a_md);
    rec_ci g = (a, aa, ba);
    rec_ci f = (ab, ac, bc)\<rbrakk>
\<Longrightarrow> \<exists>ap bp. length ap = 6 + length ab \<and>
    aprog = ap [+] bp \<and>
    bp = ([Dec (a_md - Suc 0) (length a + 7)] [+] (a [+]
         [Inc (rs_pos - Suc 0), Dec rs_pos 3, Goto (Suc 0)])) @ 
         [Dec (Suc (Suc n)) 0, Inc (Suc n), Goto (length a + 4)]"
apply(simp add: rec_ci.simps)
apply(rule_tac x = "mv_box n (max (Suc (Suc (Suc n)))
    (max bc ba)) [+] ab [+] mv_box n (Suc n)" in exI,
     simp)
apply(auto simp add: abc_append_commute numeral_3_eq_3)
done

lemma pr_cycle_part:
  "\<lbrakk>\<And>lm rs suf_lm. rec_calc_rel g lm rs \<Longrightarrow>
     \<exists>stp. abc_steps_l (0, lm @ 0\<up>(ba - aa) @ suf_lm) a stp = 
                        (length a, lm @ rs # 0\<up>(ba - Suc aa) @ suf_lm);
  rec_ci (Pr n f g) = (aprog, rs_pos, a_md); 
  rec_calc_rel (Pr n f g) lm rs;
  rec_ci g = (a, aa, ba);
  rec_calc_rel (Pr n f g) (butlast lm @ [last lm - x]) rsx;
  rec_ci f = (ab, ac, bc);
  lm \<noteq> [];
  x \<le> last lm\<rbrakk> \<Longrightarrow> 
  \<exists>stp. abc_steps_l (6 + length ab, butlast lm @ (last lm - x) #
              rsx # 0\<up>(a_md - Suc (Suc rs_pos)) @ x # suf_lm) aprog stp =
  (6 + length ab, butlast lm @ last lm # rs #
                                0\<up>(a_md - Suc (Suc rs_pos)) @ 0 # suf_lm)"
proof -
  assume g_ind:
    "\<And>lm rs suf_lm. rec_calc_rel g lm rs \<Longrightarrow> 
    \<exists>stp. abc_steps_l (0, lm @ 0\<up>(ba - aa) @ suf_lm) a stp =
                      (length a, lm @ rs # 0\<up>(ba - Suc aa) @ suf_lm)"
    and h: "rec_ci (Pr n f g) = (aprog, rs_pos, a_md)" 
           "rec_calc_rel (Pr n f g) lm rs" 
           "rec_ci g = (a, aa, ba)"
           "rec_calc_rel (Pr n f g) (butlast lm @ [last lm - x]) rsx" 
           "lm \<noteq> []"
           "x \<le> last lm" 
           "rec_ci f = (ab, ac, bc)" 
  from h show 
    "\<exists>stp. abc_steps_l (6 + length ab, butlast lm @ (last lm - x) # 
            rsx # 0\<up>(a_md - Suc (Suc rs_pos)) @ x # suf_lm) aprog stp =
    (6 + length ab, butlast lm @ last lm # rs #
                               0\<up>(a_md - Suc (Suc rs_pos)) @ 0 # suf_lm)" 
  proof(induct x arbitrary: rsx, simp_all)
    fix rsxa
    assume "rec_calc_rel (Pr n f g) lm rsxa" 
           "rec_calc_rel (Pr n f g) lm rs"
    from h and this have "rs = rsxa"
      apply(subgoal_tac "lm \<noteq> [] \<and> rs_pos = Suc n", simp)
      apply(rule_tac rec_calc_inj, simp, simp)
      apply(simp)
      done
    thus "\<exists>stp. abc_steps_l (6 + length ab, butlast lm @  last lm # 
             rsxa # 0\<up>(a_md - Suc (Suc rs_pos)) @ 0 # suf_lm) aprog stp =
      (6 + length ab, butlast lm @ last lm # rs #
                               0\<up>(a_md - Suc (Suc rs_pos)) @ 0 # suf_lm)"
      by(rule_tac x = 0 in exI, simp add: abc_steps_l.simps)
  next
    fix xa rsxa
    assume ind:
   "\<And>rsx. rec_calc_rel (Pr n f g) (butlast lm @ [last lm - xa]) rsx 
  \<Longrightarrow> \<exists>stp. abc_steps_l (6 + length ab, butlast lm @ (last lm - xa) #
             rsx # 0\<up>(a_md - Suc (Suc rs_pos)) @ xa # suf_lm) aprog stp =
      (6 + length ab, butlast lm @ last lm # rs # 
                               0\<up>(a_md - Suc (Suc rs_pos)) @ 0 # suf_lm)"
      and g: "rec_calc_rel (Pr n f g) 
                      (butlast lm @ [last lm - Suc xa]) rsxa"
      "Suc xa \<le> last lm"
      "rec_ci (Pr n f g) = (aprog, rs_pos, a_md)" 
      "rec_calc_rel (Pr n f g) lm rs"
      "rec_ci g = (a, aa, ba)" 
      "rec_ci f = (ab, ac, bc)" "lm \<noteq> []"
    from g have k1: 
      "\<exists> rs. rec_calc_rel (Pr n f g) (butlast lm @ [last lm - xa]) rs"
      apply(rule_tac rs = rs in  calc_pr_less_ex, simp, simp)
      done
    from g and this show 
      "\<exists>stp. abc_steps_l (6 + length ab, 
           butlast lm @ (last lm - Suc xa) # rsxa # 
              0\<up>(a_md - Suc (Suc rs_pos)) @ Suc xa # suf_lm) aprog stp =
              (6 + length ab, butlast lm @ last lm # rs # 
                                0\<up>(a_md - Suc (Suc rs_pos)) @ 0 # suf_lm)"
    proof(erule_tac exE)
      fix rsa
      assume k2: "rec_calc_rel (Pr n f g) 
                           (butlast lm @ [last lm - xa]) rsa"
      from g and k2 have
      "\<exists>stp. abc_steps_l (6 + length ab, butlast lm @ 
       (last lm - Suc xa) # rsxa # 
               0\<up>(a_md - Suc (Suc rs_pos)) @ Suc xa # suf_lm) aprog stp
        = (6 + length ab, butlast lm @ (last lm - xa) # rsa # 
                               0\<up>(a_md - Suc (Suc rs_pos)) @ xa # suf_lm)"
	proof -
	  from g have k2_1: 
            "\<exists> ap bp. length ap = 6 + length ab \<and>
                   aprog = ap [+] bp \<and> 
                   bp = ([Dec (a_md - Suc 0) (length a + 7)] [+]
                  (a [+] [Inc (rs_pos - Suc 0), Dec rs_pos 3, 
                  Goto (Suc 0)])) @
                  [Dec (Suc (Suc n)) 0, Inc (Suc n), Goto (length a + 4)]"
            apply(rule_tac ci_pr_ex1, auto)
	    done
	  from k2_1 and k2 and g show "?thesis"
	    proof(erule_tac exE, erule_tac exE)
	      fix ap bp
	      assume 
                "length ap = 6 + length ab \<and> 
                 aprog = ap [+] bp \<and> bp =
                ([Dec (a_md - Suc 0) (length a + 7)] [+] 
                (a [+] [Inc (rs_pos - Suc 0), Dec rs_pos 3,
                Goto (Suc 0)])) @ 
                [Dec (Suc (Suc n)) 0, Inc (Suc n), Goto (length a + 4)]" 
	      from g and this and k2 and g_ind show "?thesis"
		apply(insert abc_append_exc3[of 
                  "butlast lm @ (last lm - Suc xa) # rsxa #
                  0\<up>(a_md - Suc (Suc rs_pos)) @ Suc xa # suf_lm" bp 0
                  "butlast lm @ (last lm - xa) # rsa #
                0\<up>(a_md - Suc (Suc rs_pos)) @ xa # suf_lm" "length ap" ap],
                 simp)
		apply(subgoal_tac 
                "\<exists>stp. abc_steps_l (0, butlast lm @ (last lm - Suc xa)
                           # rsxa # 0\<up>(a_md - Suc (Suc rs_pos)) @ Suc xa # 
                              suf_lm) bp stp =
	          (0, butlast lm @ (last lm - xa) # rsa #
                           0\<up>(a_md - Suc (Suc rs_pos)) @ xa # suf_lm)",
                      simp, erule_tac conjE, erule conjE)
		apply(erule pr_cycle_part_ind, auto)
		done
	    qed
	  qed  
      from g and k2 and this show "?thesis"
	apply(erule_tac exE)
	apply(insert ind[of rsa], simp)
	apply(erule_tac exE)
	apply(rule_tac x = "stp + stpa" in exI, 
              simp add: abc_steps_add)
	done
    qed
  qed
qed

lemma ci_pr_length: 
  "\<lbrakk>rec_ci (Pr n f g) = (aprog, rs_pos, a_md); 
    rec_ci g = (a, aa, ba);  
    rec_ci f = (ab, ac, bc)\<rbrakk>
    \<Longrightarrow>  length aprog = 13 + length ab + length a"
apply(auto simp: rec_ci.simps)
done

fun mv_box_inv :: "nat \<times> nat list \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat list \<Rightarrow> bool"
  where
  "mv_box_inv (as, lm) m n initlm = 
         (let plus = initlm ! m + initlm ! n in
           length initlm > max m n \<and> m \<noteq> n \<and> 
              (if as = 0 then \<exists> k l. lm = initlm[m := k, n := l] \<and> 
                    k + l = plus \<and> k \<le> initlm ! m 
              else if as = 1 then \<exists> k l. lm = initlm[m := k, n := l]
                             \<and> k + l + 1 = plus \<and> k < initlm ! m 
              else if as = 2 then \<exists> k l. lm = initlm[m := k, n := l] 
                              \<and> k + l = plus \<and> k \<le> initlm ! m
              else if as = 3 then lm = initlm[m := 0, n := plus]
              else False))"

fun mv_box_stage1 :: "nat \<times> nat list \<Rightarrow> nat \<Rightarrow> nat"
  where
  "mv_box_stage1 (as, lm) m  = 
            (if as = 3 then 0 
             else 1)"

fun mv_box_stage2 :: "nat \<times> nat list \<Rightarrow> nat \<Rightarrow> nat"
  where
  "mv_box_stage2 (as, lm) m = (lm ! m)"

fun mv_box_stage3 :: "nat \<times> nat list \<Rightarrow> nat \<Rightarrow> nat"
  where
  "mv_box_stage3 (as, lm) m = (if as = 1 then 3 
                                else if as = 2 then 2
                                else if as = 0 then 1 
                                else 0)"
 
fun mv_box_measure :: "((nat \<times> nat list) \<times> nat) \<Rightarrow> (nat \<times> nat \<times> nat)"
  where
  "mv_box_measure ((as, lm), m) = 
     (mv_box_stage1 (as, lm) m, mv_box_stage2 (as, lm) m,
      mv_box_stage3 (as, lm) m)"

definition lex_pair :: "((nat \<times> nat) \<times> nat \<times> nat) set"
  where
  "lex_pair = less_than <*lex*> less_than"

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 mv_box_LE :: 
 "(((nat \<times> nat list) \<times> nat) \<times> ((nat \<times> nat list) \<times> nat)) set"
  where 
  "mv_box_LE \<equiv> (inv_image lex_triple mv_box_measure)"

lemma wf_lex_triple: "wf lex_triple"
  by (auto intro:wf_lex_prod simp:lex_triple_def lex_pair_def)

lemma wf_mv_box_le[intro]: "wf mv_box_LE"
by(auto intro:wf_inv_image wf_lex_triple simp: mv_box_LE_def)

declare mv_box_inv.simps[simp del]

lemma mv_box_inv_init:  
"\<lbrakk>m < length initlm; n < length initlm; m \<noteq> n\<rbrakk> \<Longrightarrow> 
  mv_box_inv (0, initlm) m n initlm"
apply(simp add: abc_steps_l.simps mv_box_inv.simps)
apply(rule_tac x = "initlm ! m" in exI, 
      rule_tac x = "initlm ! n" in exI, simp)
done

lemma [simp]: "abc_fetch 0 (mv_box m n) = Some (Dec m 3)"
apply(simp add: mv_box.simps abc_fetch.simps)
done

lemma [simp]: "abc_fetch (Suc 0) (mv_box m n) =
               Some (Inc n)"
apply(simp add: mv_box.simps abc_fetch.simps)
done

lemma [simp]: "abc_fetch 2 (mv_box m n) = Some (Goto 0)"
apply(simp add: mv_box.simps abc_fetch.simps)
done

lemma [simp]: "abc_fetch 3 (mv_box m n) = None"
apply(simp add: mv_box.simps abc_fetch.simps)
done

lemma [simp]: 
  "\<lbrakk>m \<noteq> n; m < length initlm; n < length initlm;
    k + l = initlm ! m + initlm ! n; k \<le> initlm ! m; 0 < k\<rbrakk>
 \<Longrightarrow> \<exists>ka la. initlm[m := k, n := l, m := k - Suc 0] = 
     initlm[m := ka, n := la] \<and>
     Suc (ka + la) = initlm ! m + initlm ! n \<and> 
     ka < initlm ! m"
apply(rule_tac x = "k - Suc 0" in exI, rule_tac x = l in exI, 
      simp, auto)
apply(subgoal_tac 
      "initlm[m := k, n := l, m := k - Suc 0] = 
       initlm[n := l, m := k, m := k - Suc 0]")
apply(simp add: list_update_overwrite )
apply(simp add: list_update_swap)
apply(simp add: list_update_swap)
done

lemma [simp]:
  "\<lbrakk>m \<noteq> n; m < length initlm; n < length initlm; 
    Suc (k + l) = initlm ! m + initlm ! n;
    k < initlm ! m\<rbrakk>
    \<Longrightarrow> \<exists>ka la. initlm[m := k, n := l, n := Suc l] = 
                initlm[m := ka, n := la] \<and> 
                ka + la = initlm ! m + initlm ! n \<and> 
                ka \<le> initlm ! m"
apply(rule_tac x = k in exI, rule_tac x = "Suc l" in exI, auto)
done

lemma [simp]: 
  "\<lbrakk>length initlm > max m n; m \<noteq> n\<rbrakk> \<Longrightarrow> 
   \<forall>na. \<not> (\<lambda>(as, lm) m. as = 3) 
    (abc_steps_l (0, initlm) (mv_box m n) na) m \<and> 
  mv_box_inv (abc_steps_l (0, initlm) 
           (mv_box m n) na) m n initlm \<longrightarrow>
  mv_box_inv (abc_steps_l (0, initlm) 
           (mv_box m n) (Suc na)) m n initlm \<and>
  ((abc_steps_l (0, initlm) (mv_box m n) (Suc na), m),
   abc_steps_l (0, initlm) (mv_box m n) na, m) \<in> mv_box_LE"
apply(rule allI, rule impI, simp add: abc_steps_ind)
apply(case_tac "(abc_steps_l (0, initlm) (mv_box m n) na)",
      simp)
apply(auto split:if_splits simp add:abc_steps_l.simps mv_box_inv.simps)
apply(auto simp add: mv_box_LE_def lex_triple_def lex_pair_def 
                     abc_step_l.simps abc_steps_l.simps
                     mv_box_inv.simps abc_lm_v.simps abc_lm_s.simps
                split: if_splits )
apply(rule_tac x = k in exI, rule_tac x = "Suc l" in exI, simp)
done

lemma mv_box_inv_halt: 
  "\<lbrakk>length initlm > max m n; m \<noteq> n\<rbrakk> \<Longrightarrow> 
  \<exists> stp. (\<lambda> (as, lm). as = 3 \<and> 
  mv_box_inv (as, lm) m n initlm) 
             (abc_steps_l (0::nat, initlm) (mv_box m n) stp)"
apply(insert halt_lemma2[of mv_box_LE
    "\<lambda> ((as, lm), m). mv_box_inv (as, lm) m n initlm"
    "\<lambda> stp. (abc_steps_l (0, initlm) (mv_box m n) stp, m)"
    "\<lambda> ((as, lm), m). as = (3::nat)"
    ])
apply(insert wf_mv_box_le)
apply(simp add: mv_box_inv_init abc_steps_zero)
apply(erule_tac exE)
apply(rule_tac x = na in exI)
apply(case_tac "(abc_steps_l (0, initlm) (mv_box m n) na)",
      simp, auto)
done

lemma mv_box_halt_cond:
  "\<lbrakk>m \<noteq> n; mv_box_inv (a, b) m n lm; a = 3\<rbrakk> \<Longrightarrow> 
  b = lm[n := lm ! m + lm ! n, m := 0]"
apply(simp add: mv_box_inv.simps, auto)
apply(simp add: list_update_swap)
done

lemma mv_box_ex:
  "\<lbrakk>length lm > max m n; m \<noteq> n\<rbrakk> \<Longrightarrow> 
  \<exists> stp. abc_steps_l (0::nat, lm) (mv_box m n) stp
  = (3, (lm[n := (lm ! m + lm ! n)])[m := 0::nat])"
apply(drule mv_box_inv_halt, simp, erule_tac exE)
apply(rule_tac x = stp in exI)
apply(case_tac "abc_steps_l (0, lm) (mv_box m n) stp",
      simp)
apply(erule_tac mv_box_halt_cond, auto)
done

lemma [simp]: 
  "\<lbrakk>a_md = Suc (max (Suc (Suc n)) (max bc ba)); 
   length lm = rs_pos \<and> rs_pos = n \<and> n > 0\<rbrakk>
  \<Longrightarrow> n - Suc 0 < length lm + 
  (Suc (max (Suc (Suc n)) (max bc ba)) - rs_pos + length suf_lm) \<and>
   Suc (Suc n) < length lm + (Suc (max (Suc (Suc n)) (max bc ba)) -
  rs_pos + length suf_lm) \<and> bc < length lm + (Suc (max (Suc (Suc n)) 
 (max bc ba)) - rs_pos + length suf_lm) \<and> ba < length lm + 
  (Suc (max (Suc (Suc n)) (max bc ba)) - rs_pos + length suf_lm)"
apply(arith)
done

lemma [simp]:
  "\<lbrakk>a_md = Suc (max (Suc (Suc n)) (max bc ba)); 
   length lm = rs_pos \<and> rs_pos = n \<and> n > 0\<rbrakk>
 \<Longrightarrow> n - Suc 0 < Suc (length suf_lm + max (Suc (Suc n)) (max bc ba)) \<and>
     Suc n < length suf_lm + max (Suc (Suc n)) (max bc ba) \<and> 
     bc < Suc (length suf_lm + max (Suc (Suc n)) (max bc ba)) \<and> 
     ba < Suc (length suf_lm + max (Suc (Suc n)) (max bc ba))"
apply(arith)
done

lemma [simp]: "n - Suc 0 \<noteq> max (Suc (Suc n)) (max bc ba)"
apply(arith)
done

lemma [simp]: 
  "a_md \<ge> Suc bc \<and> rs_pos > 0 \<and> bc \<ge> rs_pos \<Longrightarrow> 
 bc - (rs_pos - Suc 0) + a_md - Suc bc = Suc (a_md - rs_pos - Suc 0)"
apply(arith)
done

lemma [simp]: "length lm = n \<and> rs_pos = n \<and> 0 < rs_pos \<and> 
                                                  Suc rs_pos < a_md 
       \<Longrightarrow> n - Suc 0 < Suc (Suc (a_md + length suf_lm - Suc (Suc 0))) 
        \<and> n < Suc (Suc (a_md + length suf_lm - Suc (Suc 0)))"
apply(arith)
done
     
lemma [simp]: "length lm = n \<and> rs_pos = n \<and> 0 < rs_pos \<and> 
               Suc rs_pos < a_md \<Longrightarrow> n - Suc 0 \<noteq> n"
by arith

lemma ci_pr_ex2: 
  "\<lbrakk>rec_ci (Pr n f g) = (aprog, rs_pos, a_md);
    rec_calc_rel (Pr n f g) lm rs; 
    rec_ci g = (a, aa, ba); 
    rec_ci f = (ab, ac, bc)\<rbrakk>
  \<Longrightarrow> \<exists>ap bp. aprog = ap [+] bp \<and> 
         ap = mv_box n (max (Suc (Suc (Suc n))) (max bc ba))"
apply(simp add: rec_ci.simps)
apply(rule_tac x = "(ab [+] (mv_box n (Suc n) [+]
              ([Dec (max (n + 3) (max bc ba)) (length a + 7)] 
      [+] (a [+] [Inc n, Dec (Suc n) 3, Goto (Suc 0)])) @ 
      [Dec (Suc (Suc n)) 0, Inc (Suc n), Goto (length a + 4)]))" in exI, auto)
apply(simp add: abc_append_commute numeral_3_eq_3)
done

lemma [simp]: 
  "max (Suc (Suc (Suc n))) (max bc ba) - n < 
     Suc (max (Suc (Suc (Suc n))) (max bc ba)) - n"
apply(arith)
done

lemma [simp]: "length lm = n \<and> rs_pos = n \<and> 0 < n \<Longrightarrow> 
                      lm[n - Suc 0 := 0::nat] = butlast lm @ [0]"
apply(auto)
apply(insert list_update_append[of "butlast lm" "[last lm]" 
                                   "length lm - Suc 0" "0"], simp)
done

lemma [simp]: "\<lbrakk>length lm = n; 0 < n\<rbrakk>  \<Longrightarrow> lm ! (n - Suc 0) = last lm"
apply(insert nth_append[of "butlast lm" "[last lm]" "n - Suc 0"],
      simp)
apply(insert butlast_append_last[of lm], auto)
done
lemma exp_suc_iff: "a\<up>b @ [a] = a\<up>(b + Suc 0)"
apply(simp add: exp_ind del: replicate.simps)
done

lemma less_not_less[simp]: "n > 0 \<Longrightarrow> \<not> n < n - Suc 0"
by auto

lemma [simp]:
  "Suc n < length suf_lm + max (Suc (Suc n)) (max bc ba) \<and> 
  bc < Suc (length suf_lm + max (Suc (Suc n)) 
  (max bc ba)) \<and> 
  ba < Suc (length suf_lm + max (Suc (Suc n)) (max bc ba))"
  by arith

lemma [simp]: "length lm = n \<and> rs_pos = n \<and> n > 0 \<Longrightarrow> 
(lm @ 0\<up>(Suc (max (Suc (Suc n)) (max bc ba)) - n) @ suf_lm) 
  [max (Suc (Suc n)) (max bc ba) :=
   (lm @ 0\<up>(Suc (max (Suc (Suc n)) (max bc ba)) - n) @ suf_lm) ! (n - Suc 0) + 
       (lm @ 0\<up>(Suc (max (Suc (Suc n)) (max bc ba)) - n) @ suf_lm) ! 
                   max (Suc (Suc n)) (max bc ba), n - Suc 0 := 0::nat]
 = butlast lm @ 0 # 0\<up>(max (Suc (Suc n)) (max bc ba) - n) @ last lm # suf_lm"
apply(simp add: nth_append nth_replicate list_update_append)
apply(insert list_update_append[of "0\<up>((max (Suc (Suc n)) (max bc ba)) - n)"
         "[0]" "max (Suc (Suc n)) (max bc ba) - n" "last lm"], simp)
apply(simp add: exp_suc_iff Suc_diff_le del: list_update.simps)
done

lemma exp_eq: "(a = b) = (c\<up>a = c\<up>b)"
apply(auto)
done

lemma [simp]:
  "\<lbrakk>length lm = n; 0 < n;  Suc n < a_md\<rbrakk> \<Longrightarrow> 
   (butlast lm @ rsa # 0\<up>(a_md - Suc n) @ last lm # suf_lm)
    [n := (butlast lm @ rsa # 0\<up>(a_md - Suc n) @ last lm # suf_lm) ! 
        (n - Suc 0) + (butlast lm @ rsa # (0::nat)\<up>(a_md - Suc n) @ 
                                last lm # suf_lm) ! n, n - Suc 0 := 0]
 = butlast lm @ 0 # rsa # 0\<up>(a_md - Suc (Suc n)) @ last lm # suf_lm"
apply(simp add: nth_append list_update_append)
apply(case_tac "a_md - Suc n", auto)
done

lemma [simp]: 
  "Suc (Suc rs_pos) \<le> a_md \<and> length lm = rs_pos \<and> 0 < rs_pos
  \<Longrightarrow> a_md - Suc 0 < 
          Suc (Suc (Suc (a_md + length suf_lm - Suc (Suc (Suc 0)))))"
by arith

lemma [simp]: 
  "Suc (Suc rs_pos) \<le> a_md \<and> length lm = rs_pos \<and> 0 < rs_pos \<Longrightarrow> 
                                   \<not> a_md - Suc 0 < rs_pos - Suc 0"
by arith

lemma [simp]: "Suc (Suc rs_pos) \<le> a_md \<Longrightarrow> 
                                \<not> a_md - Suc 0 < rs_pos - Suc 0"
by arith

lemma [simp]: "\<lbrakk>Suc (Suc rs_pos) \<le> a_md\<rbrakk> \<Longrightarrow> 
               \<not> a_md - rs_pos < Suc (Suc (a_md - Suc (Suc rs_pos)))"
by arith 

lemma [simp]: 
  "Suc (Suc rs_pos) \<le> a_md \<and> length lm = rs_pos \<and> 0 < rs_pos
 \<Longrightarrow> (abc_lm_v (butlast lm @ last lm # rs # 0\<up>(a_md - Suc (Suc rs_pos)) @
        0 # suf_lm) (a_md - Suc 0) = 0 \<longrightarrow>
      abc_lm_s (butlast lm @ last lm # rs # 0\<up>(a_md - Suc (Suc rs_pos)) @ 
        0 # suf_lm) (a_md - Suc 0) 0 = 
         lm @ rs # 0\<up>(a_md - Suc rs_pos) @ suf_lm) \<and>
     abc_lm_v (butlast lm @ last lm # rs # 0\<up>(a_md - Suc (Suc rs_pos)) @ 
               0 # suf_lm) (a_md - Suc 0) = 0"
apply(simp add: abc_lm_v.simps nth_append abc_lm_s.simps)
apply(insert nth_append[of "last lm # rs # 0\<up>(a_md - Suc (Suc rs_pos))" 
               "0 # suf_lm" "(a_md - rs_pos)"], auto)
apply(simp only: exp_suc_iff)
apply(subgoal_tac "a_md - Suc 0 < a_md + length suf_lm", simp)
apply(case_tac "lm = []", auto)
done

lemma pr_prog_ex[simp]: "\<lbrakk>rec_ci (Pr n f g) = (aprog, rs_pos, a_md); 
      rec_ci g = (a, aa, ba); rec_ci f = (ab, ac, bc)\<rbrakk>
    \<Longrightarrow> \<exists>cp. aprog = mv_box n (max (n + 3) 
                    (max bc ba)) [+] cp"
apply(simp add: rec_ci.simps)
apply(rule_tac x = "(ab [+] (mv_box n (Suc n) [+]
              ([Dec (max (n + 3) (max bc ba)) (length a + 7)] 
             [+] (a [+] [Inc n, Dec (Suc n) 3, Goto (Suc 0)]))
             @ [Dec (Suc (Suc n)) 0, Inc (Suc n), Goto (length a + 4)]))" in exI)
apply(auto simp: abc_append_commute)
done

lemma [simp]: "mv_box m n \<noteq> []"
by (simp add: mv_box.simps)
(*
lemma [simp]: "\<lbrakk>rs_pos = n; 0 < rs_pos ; Suc rs_pos < a_md\<rbrakk> \<Longrightarrow> 
                        n - Suc 0 < a_md + length suf_lm"
by arith
*)
lemma [intro]: 
  "\<lbrakk>rec_ci (Pr n f g) = (aprog, rs_pos, a_md); 
    rec_ci f = (ab, ac, bc)\<rbrakk> \<Longrightarrow> 
   \<exists>ap. (\<exists>cp. aprog = ap [+] ab [+] cp) \<and> length ap = 3"
apply(case_tac "rec_ci g", simp add: rec_ci.simps)
apply(rule_tac x = "mv_box n 
              (max (n + 3) (max bc c))" in exI, simp)
apply(rule_tac x = "mv_box n (Suc n) [+]
                 ([Dec (max (n + 3) (max bc c)) (length a + 7)]
                 [+] a [+] [Inc n, Dec (Suc n) 3, Goto (Suc 0)])
               @ [Dec (Suc (Suc n)) 0, Inc (Suc n), Goto (length a + 4)]" in exI, 
      auto)
apply(simp add: abc_append_commute)
done

lemma [intro]: 
  "\<lbrakk>rec_ci (Pr n f g) = (aprog, rs_pos, a_md);
    rec_ci g = (a, aa, ba); 
    rec_ci f = (ab, ac, bc)\<rbrakk> \<Longrightarrow> 
    \<exists>ap. (\<exists>cp. aprog = ap [+] mv_box n (Suc n) [+] cp)
      \<and> length ap = 3 + length ab"
apply(simp add: rec_ci.simps)
apply(rule_tac x = "mv_box n (max (n + 3)
                                (max bc ba)) [+] ab" in exI, simp)
apply(rule_tac x = "([Dec (max (n + 3) (max bc ba))
  (length a + 7)] [+] a [+] 
  [Inc n, Dec (Suc n) 3, Goto (Suc 0)]) @ 
  [Dec (Suc (Suc n)) 0, Inc (Suc n), Goto (length a + 4)]" in exI)
apply(auto simp: abc_append_commute)
done

lemma [intro]: 
  "\<lbrakk>rec_ci (Pr n f g) = (aprog, rs_pos, a_md);
    rec_ci g = (a, aa, ba); 
    rec_ci f = (ab, ac, bc)\<rbrakk>
    \<Longrightarrow> \<exists>ap. (\<exists>cp. aprog = ap [+] ([Dec (a_md - Suc 0) (length a + 7)]
             [+] (a [+] [Inc (rs_pos - Suc 0), Dec rs_pos 3, 
             Goto (Suc 0)])) @ [Dec (Suc (Suc n)) 0, Inc (Suc n),
             Goto (length a + 4)] [+] cp) \<and>
             length ap = 6 + length ab"
apply(simp add: rec_ci.simps)
apply(rule_tac x = "mv_box n
    (max (n + 3) (max bc ba)) [+] ab [+] 
     mv_box n (Suc n)" in exI, simp)
apply(rule_tac x = "[]" in exI, auto)
apply(simp add: abc_append_commute)
done

lemma [simp]: 
  "n < Suc (max (n + 3) (max bc ba) + length suf_lm) \<and> 
   Suc (Suc n) < max (n + 3) (max bc ba) + length suf_lm \<and> 
   bc < Suc (max (n + 3) (max bc ba) + length suf_lm) \<and> 
   ba < Suc (max (n + 3) (max bc ba) + length suf_lm)"
by arith

lemma [simp]: "n \<noteq> max (n + (3::nat)) (max bc ba)"
by arith

lemma [simp]:"length lm = Suc n \<Longrightarrow> lm[n := (0::nat)] = butlast lm @ [0]"
apply(subgoal_tac "\<exists> xs x. lm = xs @ [x]", auto simp: list_update_append)
apply(rule_tac x = "butlast lm" in exI, rule_tac x = "last lm" in exI)
apply(case_tac lm, auto)
done

lemma [simp]:  "length lm = Suc n \<Longrightarrow> lm ! n =last lm"
apply(subgoal_tac "lm \<noteq> []")
apply(simp add: last_conv_nth, case_tac lm, simp_all)
done

lemma [simp]: "length lm = Suc n \<Longrightarrow> 
      (lm @ (0::nat)\<up>(max (n + 3) (max bc ba) - n) @ suf_lm)
           [max (n + 3) (max bc ba) := (lm @ 0\<up>(max (n + 3) (max bc ba) - n) @ suf_lm) ! n + 
                  (lm @ 0\<up>(max (n + 3) (max bc ba) - n) @ suf_lm) ! max (n + 3) (max bc ba), n := 0]
       = butlast lm @ 0 # 0\<up>(max (n + 3) (max bc ba) - Suc n) @ last lm # suf_lm"
apply(auto simp: list_update_append nth_append)
apply(subgoal_tac "(0\<up>(max (n + 3) (max bc ba) - n)) = 0\<up>(max (n + 3) (max bc ba) - Suc n) @ [0::nat]")
apply(simp add: list_update_append)
apply(simp add: exp_suc_iff)
done

lemma [simp]: "Suc (Suc n) < a_md \<Longrightarrow>  
      n < Suc (Suc (a_md + length suf_lm - 2)) \<and>
        n < Suc (a_md + length suf_lm - 2)"
by(arith)

lemma [simp]: "\<lbrakk>length lm = Suc n; Suc (Suc n) < a_md\<rbrakk>
        \<Longrightarrow>(butlast lm @ (rsa::nat) # 0\<up>(a_md - Suc (Suc n)) @ last lm # suf_lm)
          [Suc n := (butlast lm @ rsa # 0\<up>(a_md - Suc (Suc n)) @ last lm # suf_lm) ! n +
                  (butlast lm @ rsa # 0\<up>(a_md - Suc (Suc n)) @ last lm # suf_lm) ! Suc n, n := 0]
    = butlast lm @ 0 # rsa # 0\<up>(a_md - Suc (Suc (Suc n))) @ last lm # suf_lm"
apply(auto simp: list_update_append)
apply(subgoal_tac "(0\<up>(a_md - Suc (Suc n))) = (0::nat) # (0\<up>(a_md - Suc (Suc (Suc n))))", simp add: nth_append)
apply(simp add: replicate_Suc[THEN sym])
done

lemma pr_case:
  assumes nf_ind:
  "\<And> lm rs suf_lm. rec_calc_rel f lm rs \<Longrightarrow> 
  \<exists>stp. abc_steps_l (0, lm @ 0\<up>(bc - ac) @ suf_lm) ab stp = 
                (length ab, lm @ rs # 0\<up>(bc - Suc ac) @ suf_lm)"
  and ng_ind: "\<And> lm rs suf_lm. rec_calc_rel g lm rs \<Longrightarrow> 
        \<exists>stp. abc_steps_l (0, lm @ 0\<up>(ba - aa) @ suf_lm) a stp = 
                       (length a, lm @ rs # 0\<up>(ba - Suc aa) @ suf_lm)"
    and h: "rec_ci (Pr n f g) = (aprog, rs_pos, a_md)"  "rec_calc_rel (Pr n f g) lm rs" 
           "rec_ci g = (a, aa, ba)" "rec_ci f = (ab, ac, bc)" 
  shows "\<exists>stp. abc_steps_l (0, lm @ 0\<up>(a_md - rs_pos) @ suf_lm) aprog stp = (length aprog, lm @ rs # 0\<up>(a_md - Suc rs_pos) @ suf_lm)"
proof -
  from h have k1: "\<exists> stp. abc_steps_l (0, lm @ 0\<up>(a_md - rs_pos) @ suf_lm) aprog stp
    = (3, butlast lm @ 0 # 0\<up>(a_md - rs_pos - 1) @ last lm # suf_lm)"
  proof -
    have "\<exists>bp cp. aprog = bp [+] cp \<and> bp = mv_box n 
                 (max (n + 3) (max bc ba))"
      apply(insert h, simp)
      apply(erule pr_prog_ex, auto)
      done
    thus "?thesis"
      apply(erule_tac exE, erule_tac exE, simp)
      apply(subgoal_tac 
           "\<exists>stp. abc_steps_l (0, lm @ 0\<up>(a_md - rs_pos) @ suf_lm)
              ([] [+] mv_box n
                  (max (n + 3) (max bc ba)) [+] cp) stp =
             (0 + 3, butlast lm @ 0 # 0\<up>(a_md - Suc rs_pos) @ 
                                        last lm # suf_lm)", simp)
      apply(rule_tac abc_append_exc1, simp_all)
      apply(insert mv_box_ex[of "n" "(max (n + 3) 
                 (max bc ba))" "lm @ 0\<up>(a_md - rs_pos) @ suf_lm"], simp)
      apply(subgoal_tac "a_md = Suc (max (n + 3) (max bc ba))",
            simp)
      apply(subgoal_tac "length lm = Suc n \<and> rs_pos = Suc n", simp)
      apply(insert h)
      apply(simp add: para_pattern ci_pr_para_eq)
      apply(rule ci_pr_md_def, auto)
      done
  qed
  from h have k2: 
  "\<exists> stp. abc_steps_l (3,  butlast lm @ 0 # 0\<up>(a_md - rs_pos - 1) @ 
             last lm # suf_lm) aprog stp 
    = (length aprog, lm @ rs # 0\<up>(a_md - Suc rs_pos) @ suf_lm)"
  proof -
    from h have k2_1: "\<exists> rs. rec_calc_rel f (butlast lm) rs"
      apply(erule_tac calc_pr_zero_ex)
      done
    thus "?thesis"
    proof(erule_tac exE)
      fix rsa
      assume k2_2: "rec_calc_rel f (butlast lm) rsa"
      from h and k2_2 have k2_2_1: 
       "\<exists> stp. abc_steps_l (3, butlast lm @ 0 # 0\<up>(a_md - rs_pos - 1) 
                 @ last lm # suf_lm) aprog stp
        = (3 + length ab, butlast lm @ rsa # 0\<up>(a_md - rs_pos - 1) @ 
                                             last lm # suf_lm)"
      proof -
	from h have j1: "
          \<exists> ap bp cp. aprog = ap [+] bp [+] cp \<and> length ap = 3 \<and> 
              bp = ab"
	  apply(auto)
	  done
	from h have j2: "ac = rs_pos - 1"
	  apply(drule_tac ci_pr_f_paras, simp, auto)
	  done
	from h and j2 have j3: "a_md \<ge> Suc bc \<and> rs_pos > 0 \<and> bc \<ge> rs_pos"
	  apply(rule_tac conjI)
	  apply(erule_tac ab = ab and ac = ac in ci_pr_md_ge_f, simp)
	  apply(rule_tac context_conjI)
          apply(simp_all add: rec_ci.simps)
	  apply(drule_tac ci_ad_ge_paras, drule_tac ci_ad_ge_paras)
	  apply(arith)
	  done	  
	from j1 and j2 show "?thesis"
	  apply(auto simp del: abc_append_commute)
	  apply(rule_tac abc_append_exc1, simp_all)
	  apply(insert nf_ind[of "butlast lm" "rsa" 
                "0\<up>(a_md - bc - Suc 0) @ last lm # suf_lm"], 
               simp add: k2_2 j2, erule_tac exE)
	  apply(simp add: exponent_add_iff j3)
	  apply(rule_tac x = "stp" in exI, simp)
	  done
      qed
      from h have k2_2_2: 
      "\<exists> stp. abc_steps_l (3 + length ab, butlast lm @ rsa # 
                  0\<up>(a_md - rs_pos - 1) @ last lm # suf_lm) aprog stp
        = (6 + length ab, butlast lm @ 0 # rsa # 
                       0\<up>(a_md - rs_pos - 2) @ last lm # suf_lm)"
      proof -	     
	from h have "\<exists> ap bp cp. aprog = ap [+] bp [+] cp \<and> 
          length ap = 3 + length ab \<and> bp = mv_box n (Suc n)"
	  by auto
	thus "?thesis"
	proof(erule_tac exE, erule_tac exE, erule_tac exE, 
              erule_tac exE)
	  fix ap cp bp apa
	  assume "aprog = ap [+] bp [+] cp \<and> length ap = 3 + 
                    length ab \<and> bp = mv_box n (Suc n)"
	  thus "?thesis"
	    apply(simp del: abc_append_commute)
	    apply(subgoal_tac 
              "\<exists>stp. abc_steps_l (3 + length ab, 
               butlast lm @ rsa # 0\<up>(a_md - Suc rs_pos) @
                 last lm # suf_lm) (ap [+] 
                   mv_box n (Suc n) [+] cp) stp =
              ((3 + length ab) + 3, butlast lm @ 0 # rsa # 
                  0\<up>(a_md - Suc (Suc rs_pos)) @ last lm # suf_lm)", simp)
	    apply(rule_tac abc_append_exc1, simp_all)
	    apply(insert mv_box_ex[of n "Suc n" 
                    "butlast lm @ rsa # 0\<up>(a_md - Suc rs_pos) @ 
                          last lm # suf_lm"], simp)
	    apply(subgoal_tac "length lm = Suc n \<and> rs_pos = Suc n \<and> a_md > Suc (Suc n)", simp)
	    apply(insert h, simp)
            done
	qed
      qed
      from h have k2_3: "lm \<noteq> []"
	apply(rule_tac calc_pr_para_not_null, simp)
	done
      from h and k2_2 and k2_3 have k2_2_3: 
      "\<exists> stp. abc_steps_l (6 + length ab, butlast lm @ 
          (last lm - last lm) # rsa # 
            0\<up>(a_md - (Suc (Suc rs_pos))) @ last lm # suf_lm) aprog stp
        = (6 + length ab, butlast lm @ last lm # rs # 
                        0\<up>(a_md - Suc (Suc (rs_pos))) @ 0 # suf_lm)"
	apply(rule_tac x = "last lm" and g = g in pr_cycle_part, auto)
	apply(rule_tac ng_ind, simp)
	apply(rule_tac rec_calc_rel_def0, simp, simp)
	done
      from h  have k2_2_4: 
       "\<exists> stp. abc_steps_l (6 + length ab,
             butlast lm @ last lm # rs # 0\<up>(a_md - rs_pos - 2) @
                  0 # suf_lm) aprog stp
        = (13 + length ab + length a,
                   lm @ rs # 0\<up>(a_md - rs_pos - 1) @ suf_lm)"
      proof -
	from h have 
        "\<exists> ap bp cp. aprog = ap [+] bp [+] cp \<and>
                     length ap = 6 + length ab \<and> 
                    bp = ([Dec (a_md - Suc 0) (length a + 7)] [+] 
                         (a [+] [Inc (rs_pos - Suc 0), 
                         Dec rs_pos 3, Goto (Suc 0)])) @ 
                        [Dec (Suc (Suc n)) 0, Inc (Suc n), Goto (length a + 4)]"
	  by auto
	thus "?thesis"
	  apply(auto)
	  apply(subgoal_tac  
            "\<exists>stp. abc_steps_l (6 + length ab, butlast lm @ 
                last lm # rs # 0\<up>(a_md - Suc (Suc rs_pos)) @ 0 # suf_lm)
                (ap [+] ([Dec (a_md - Suc 0) (length a + 7)] [+] 
                (a [+] [Inc (rs_pos - Suc 0), Dec rs_pos 3, 
                Goto (Suc 0)])) @ [Dec (Suc (Suc n)) 0, Inc (Suc n), 
                Goto (length a + 4)] [+] cp) stp =
            (6 + length ab + (length a + 7) , 
                 lm @ rs # 0\<up>(a_md - Suc rs_pos) @ suf_lm)", simp)
	  apply(subgoal_tac "13 + (length ab + length a) = 
                              13 + length ab + length a", simp)
	  apply(arith)
	  apply(rule abc_append_exc1, simp_all)
	  apply(rule_tac x = "Suc 0" in exI, 
                simp add: abc_steps_l.simps abc_fetch.simps
                         nth_append abc_append_nth abc_step_l.simps)
	  apply(subgoal_tac "a_md > Suc (Suc rs_pos) \<and> 
                            length lm = rs_pos \<and> rs_pos > 0", simp)
	  apply(insert h, simp)
	  apply(subgoal_tac "rs_pos = Suc n", simp, simp)
          done
      qed
      from h have k2_2_5: "length aprog = 13 + length ab + length a"
	apply(rule_tac ci_pr_length, simp_all)
	done
      from k2_2_1 and k2_2_2 and k2_2_3 and k2_2_4 and k2_2_5 
      show "?thesis"
	apply(auto)
	apply(rule_tac x = "stp + stpa + stpb + stpc" in exI, 
              simp add: abc_steps_add)
	done
    qed
  qed	
  from k1 and k2 show 
    "\<exists>stp. abc_steps_l (0, lm @ 0\<up>(a_md - rs_pos) @ suf_lm) aprog stp 
               = (length aprog, lm @ rs # 0\<up>(a_md - Suc rs_pos) @ suf_lm)"
    apply(erule_tac exE)
    apply(erule_tac exE)
    apply(rule_tac x = "stp + stpa" in exI)
    apply(simp add: abc_steps_add)
    done
qed

lemma eq_switch: "x = y \<Longrightarrow> y = x"
by simp

lemma [simp]: 
  "\<lbrakk>rec_ci f = (a, aa, ba); 
    rec_ci (Mn n f) = (aprog, rs_pos, a_md)\<rbrakk> \<Longrightarrow> \<exists>bp. aprog = a @ bp"
apply(simp add: rec_ci.simps)
apply(rule_tac x = "[Dec (Suc n) (length a + 5), 
      Dec (Suc n) (length a + 3), Goto (Suc (length a)), 
      Inc n, Goto 0]" in exI, auto)
done

lemma ci_mn_para_eq[simp]: 
  "rec_ci (Mn n f) = (aprog, rs_pos, a_md) \<Longrightarrow> rs_pos = n"
apply(case_tac "rec_ci f", simp add: rec_ci.simps)
done

lemma [simp]: "rec_ci f = (a, aa, ba) \<Longrightarrow> aa < ba"
apply(simp add: ci_ad_ge_paras)
done

lemma [simp]: "\<lbrakk>rec_ci f = (a, aa, ba); 
                rec_ci (Mn n f) = (aprog, rs_pos, a_md)\<rbrakk>
    \<Longrightarrow> ba \<le> a_md"
apply(simp add: rec_ci.simps)
by arith

lemma mn_calc_f: 
  assumes ind: 
  "\<And>aprog a_md rs_pos rs suf_lm lm.
  \<lbrakk>rec_ci f = (aprog, rs_pos, a_md); rec_calc_rel f lm rs\<rbrakk>  
  \<Longrightarrow> \<exists>stp. abc_steps_l (0, lm @ 0\<up>(a_md - rs_pos) @ suf_lm) aprog stp    
           = (length aprog, lm @ [rs] @ 0\<up>(a_md - rs_pos - 1) @ suf_lm)"
  and h: "rec_ci f = (a, aa, ba)" 
         "rec_ci (Mn n f) = (aprog, rs_pos, a_md)"  
         "rec_calc_rel f (lm @ [x]) rsx" 
         "aa = Suc n"
  shows "\<exists>stp. abc_steps_l (0, lm @ x # 0\<up>(a_md - Suc rs_pos) @ suf_lm) 
                  aprog stp = (length a, 
                   lm @ x # rsx # 0\<up>(a_md - Suc (Suc rs_pos)) @ suf_lm)"
proof -
  from h have k1: "\<exists> ap bp. aprog = ap @ bp \<and> ap = a"
    by simp
  from h have k2: "rs_pos = n"
    apply(erule_tac ci_mn_para_eq)
    done
  from h and k1 and k2 show "?thesis"
  
  proof(erule_tac exE, erule_tac exE, simp, 
        rule_tac abc_add_exc1, auto)
    fix bp
    show 
      "\<exists>astp. abc_steps_l (0, lm @ x # 0\<up>(a_md - Suc n) @ suf_lm) a astp
      = (length a, lm @ x # rsx # 0\<up>(a_md - Suc (Suc n)) @ suf_lm)"
      apply(insert ind[of a "Suc n" ba  "lm @ [x]" rsx 
             "0\<up>(a_md - ba) @ suf_lm"], simp add: exponent_add_iff h k2)
      apply(subgoal_tac "ba > aa \<and> a_md \<ge> ba \<and> aa = Suc n", 
            insert h, auto)
      done
  qed
qed

fun mn_ind_inv ::
  "nat \<times> nat list \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat list \<Rightarrow> nat list \<Rightarrow> bool"
  where
  "mn_ind_inv (as, lm') ss x rsx suf_lm lm = 
           (if as = ss then lm' = lm @ x # rsx # suf_lm
            else if as = ss + 1 then 
                 \<exists>y. (lm' = lm @ x # y # suf_lm) \<and> y \<le> rsx
            else if as = ss + 2 then 
                 \<exists>y. (lm' = lm @ x # y # suf_lm) \<and> y \<le> rsx
            else if as = ss + 3 then lm' = lm @ x # 0 # suf_lm
            else if as = ss + 4 then lm' = lm @ Suc x # 0 # suf_lm
            else if as = 0 then lm' = lm @ Suc x # 0 # suf_lm
            else False
)"

fun mn_stage1 :: "nat \<times> nat list \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat"
  where
  "mn_stage1 (as, lm) ss n = 
            (if as = 0 then 0 
             else if as = ss + 4 then 1
             else if as = ss + 3 then 2
             else if as = ss + 2 \<or> as = ss + 1 then 3
             else if as = ss then 4
             else 0
)"

fun mn_stage2 :: "nat \<times> nat list \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat"
  where
  "mn_stage2 (as, lm) ss n = 
            (if as = ss + 1 \<or> as = ss + 2 then (lm ! (Suc n))
             else 0)"

fun mn_stage3 :: "nat \<times> nat list \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat"
  where
  "mn_stage3 (as, lm) ss n = (if as = ss + 2 then 1 else 0)"

 
fun mn_measure :: "((nat \<times> nat list) \<times> nat \<times> nat) \<Rightarrow>
                                                (nat \<times> nat \<times> nat)"
  where
  "mn_measure ((as, lm), ss, n) = 
     (mn_stage1 (as, lm) ss n, mn_stage2 (as, lm) ss n,
                                       mn_stage3 (as, lm) ss n)"

definition mn_LE :: "(((nat \<times> nat list) \<times> nat \<times> nat) \<times>
                     ((nat \<times> nat list) \<times> nat \<times> nat)) set"
  where "mn_LE \<equiv> (inv_image lex_triple mn_measure)"

lemma wf_mn_le[intro]: "wf mn_LE"
by(auto intro:wf_inv_image wf_lex_triple simp: mn_LE_def)

declare mn_ind_inv.simps[simp del]

lemma mn_inv_init: 
  "mn_ind_inv (abc_steps_l (length a, lm @ x # rsx # suf_lm) aprog 0)
                                         (length a) x rsx suf_lm lm"
apply(simp add: mn_ind_inv.simps abc_steps_zero)
done

lemma mn_halt_init: 
  "rec_ci f = (a, aa, ba) \<Longrightarrow> 
  \<not> (\<lambda>(as, lm') (ss, n). as = 0) 
    (abc_steps_l (length a, lm @ x # rsx # suf_lm) aprog 0) 
                                                       (length a, n)"
apply(simp add: abc_steps_zero)
apply(erule_tac rec_ci_not_null)
done

lemma [simp]: 
  "\<lbrakk>rec_ci f = (a, aa, ba); 
    rec_ci (Mn n f) = (aprog, rs_pos, a_md)\<rbrakk>
    \<Longrightarrow> abc_fetch (length a) aprog =
                      Some (Dec (Suc n) (length a + 5))"
apply(simp add: rec_ci.simps abc_fetch.simps, 
                erule_tac conjE, erule_tac conjE, simp)
apply(drule_tac eq_switch, drule_tac eq_switch, simp)
done

lemma [simp]: "\<lbrakk>rec_ci f = (a, aa, ba); rec_ci (Mn n f) = (aprog, rs_pos, a_md)\<rbrakk>
    \<Longrightarrow> abc_fetch (Suc (length a)) aprog = Some (Dec (Suc n) (length a + 3))"
apply(simp add: rec_ci.simps abc_fetch.simps, erule_tac conjE, erule_tac conjE, simp)
apply(drule_tac eq_switch, drule_tac eq_switch, simp add: nth_append)
done

lemma [simp]:
  "\<lbrakk>rec_ci f = (a, aa, ba);
    rec_ci (Mn n f) = (aprog, rs_pos, a_md)\<rbrakk>
    \<Longrightarrow> abc_fetch (Suc (Suc (length a))) aprog = 
                                     Some (Goto (length a + 1))"
apply(simp add: rec_ci.simps abc_fetch.simps,
      erule_tac conjE, erule_tac conjE, simp)
apply(drule_tac eq_switch, drule_tac eq_switch, simp add: nth_append)
done

lemma [simp]: 
  "\<lbrakk>rec_ci f = (a, aa, ba);
    rec_ci (Mn n f) = (aprog, rs_pos, a_md)\<rbrakk>
    \<Longrightarrow> abc_fetch (length a + 3) aprog = Some (Inc n)"
apply(simp add: rec_ci.simps abc_fetch.simps, 
      erule_tac conjE, erule_tac conjE, simp)
apply(drule_tac eq_switch, drule_tac eq_switch, simp add: nth_append)
done

lemma [simp]: "\<lbrakk>rec_ci f = (a, aa, ba); rec_ci (Mn n f) = (aprog, rs_pos, a_md)\<rbrakk>
    \<Longrightarrow> abc_fetch (length a + 4) aprog = Some (Goto 0)"
apply(simp add: rec_ci.simps abc_fetch.simps, erule_tac conjE, erule_tac conjE, simp)
apply(drule_tac eq_switch, drule_tac eq_switch, simp add: nth_append)
done

lemma [simp]: 
  "0 < rsx
   \<Longrightarrow> \<exists>y. (lm @ x # rsx # suf_lm)[Suc (length lm) := rsx - Suc 0]   
    = lm @ x # y # suf_lm \<and> y \<le> rsx"
apply(case_tac rsx, simp, simp)
apply(rule_tac x = nat in exI, simp add: list_update_append)
done

lemma [simp]: 
  "\<lbrakk>y \<le> rsx; 0 < y\<rbrakk>
   \<Longrightarrow> \<exists>ya. (lm @ x # y # suf_lm)[Suc (length lm) := y - Suc 0] 
          = lm @ x # ya # suf_lm \<and> ya \<le> rsx"
apply(case_tac y, simp, simp)
apply(rule_tac x = nat in exI, simp add: list_update_append)
done

lemma mn_halt_lemma: 
  "\<lbrakk>rec_ci f = (a, aa, ba);
    rec_ci (Mn n f) = (aprog, rs_pos, a_md);
     0 < rsx; length lm = n\<rbrakk>
    \<Longrightarrow>
  \<forall>na. \<not> (\<lambda>(as, lm') (ss, n). as = 0)
  (abc_steps_l (length a, lm @ x # rsx # suf_lm) aprog na) 
                                                       (length a, n)
 \<and> mn_ind_inv (abc_steps_l (length a, lm @ x # rsx # suf_lm)
                       aprog na) (length a) x rsx suf_lm lm 
\<longrightarrow> mn_ind_inv (abc_steps_l (length a, lm @ x # rsx # suf_lm) aprog 
                         (Suc na)) (length a) x rsx suf_lm lm
 \<and> ((abc_steps_l (length a, lm @ x # rsx # suf_lm) aprog (Suc na), 
                                                    length a, n), 
    abc_steps_l (length a, lm @ x # rsx # suf_lm) aprog na,
                              length a, n) \<in> mn_LE"
apply(rule allI, rule impI, simp add: abc_steps_ind)
apply(case_tac "(abc_steps_l (length a, lm @ x # rsx # suf_lm) 
                                                   aprog na)", simp)
apply(auto split:if_splits simp add:abc_steps_l.simps 
                           mn_ind_inv.simps abc_steps_zero)
apply(auto simp add: mn_LE_def lex_triple_def lex_pair_def 
            abc_step_l.simps abc_steps_l.simps mn_ind_inv.simps
            abc_lm_v.simps abc_lm_s.simps nth_append
           split: if_splits)
apply(drule_tac  rec_ci_not_null, simp)
done

lemma mn_halt:
  "\<lbrakk>rec_ci f = (a, aa, ba);
    rec_ci (Mn n f) = (aprog, rs_pos, a_md);
    0 < rsx; length lm = n\<rbrakk>
    \<Longrightarrow> \<exists> stp. (\<lambda> (as, lm'). (as = 0 \<and> 
           mn_ind_inv (as, lm')  (length a) x rsx suf_lm lm))
            (abc_steps_l (length a, lm @ x # rsx # suf_lm) aprog stp)"
apply(insert wf_mn_le)	  
apply(insert halt_lemma2[of mn_LE
  "\<lambda> ((as, lm'), ss, n). mn_ind_inv (as, lm') ss x rsx suf_lm lm"
  "\<lambda> stp. (abc_steps_l (length a, lm @ x # rsx # suf_lm) aprog stp, 
  length a, n)"
  "\<lambda> ((as, lm'), ss, n). as = 0"], 
   simp)
apply(simp add: mn_halt_init mn_inv_init)
apply(drule_tac x = x and suf_lm = suf_lm in mn_halt_lemma, auto)
apply(rule_tac x = n in exI, 
      case_tac "(abc_steps_l (length a, lm @ x # rsx # suf_lm)
                              aprog n)", simp)
done

lemma [simp]: "Suc rs_pos < a_md \<Longrightarrow> 
                Suc (a_md - Suc (Suc rs_pos)) = a_md - Suc rs_pos"
by arith

lemma mn_ind_step: 
  assumes ind:  
  "\<And>aprog a_md rs_pos rs suf_lm lm.
  \<lbrakk>rec_ci f = (aprog, rs_pos, a_md);
   rec_calc_rel f lm rs\<rbrakk> \<Longrightarrow> 
  \<exists>stp. abc_steps_l (0, lm @ 0\<up>(a_md - rs_pos) @ suf_lm) aprog stp
            = (length aprog, lm @ [rs] @ 0\<up>(a_md - rs_pos - 1) @ suf_lm)"
  and h: "rec_ci f = (a, aa, ba)" 
         "rec_ci (Mn n f) = (aprog, rs_pos, a_md)"  
         "rec_calc_rel f (lm @ [x]) rsx" 
         "rsx > 0" 
         "Suc rs_pos < a_md" 
         "aa = Suc rs_pos"
  shows "\<exists>stp. abc_steps_l (0, lm @ x # 0\<up>(a_md - Suc rs_pos) @ suf_lm) 
             aprog stp = (0, lm @ Suc x # 0\<up>(a_md - Suc rs_pos) @ suf_lm)"
proof -
  have k1: 
    "\<exists> stp. abc_steps_l (0, lm @ x #  0\<up>(a_md - Suc (rs_pos)) @ suf_lm)
         aprog stp = 
       (length a, lm @ x # rsx # 0\<up>(a_md  - Suc (Suc rs_pos)) @ suf_lm)"
    apply(insert h)
    apply(auto intro: mn_calc_f ind)
    done
  from h have k2: "length lm = n"
    apply(subgoal_tac "rs_pos = n")
    apply(drule_tac  para_pattern, simp, simp, simp)
    done
  from h have k3: "a_md > (Suc rs_pos)"
    apply(simp)
    done
  from k2 and h and k3 have k4: 
    "\<exists> stp. abc_steps_l (length a,
       lm @ x # rsx # 0\<up>(a_md  - Suc (Suc rs_pos)) @ suf_lm) aprog stp = 
        (0, lm @ Suc x # 0\<up>(a_md - rs_pos - 1) @ suf_lm)"
    apply(frule_tac x = x and 
       suf_lm = "0\<up>(a_md - Suc (Suc rs_pos)) @ suf_lm" in mn_halt, auto)
    apply(rule_tac x = "stp" in exI, 
          simp add: mn_ind_inv.simps rec_ci_not_null)
    apply(simp only: replicate.simps[THEN sym], simp)
    done
  from k1 and k4 show "?thesis"
    apply(auto)
    apply(rule_tac x = "stp + stpa" in exI, simp add: abc_steps_add)
    done
qed

lemma [simp]: 
  "\<lbrakk>rec_ci f = (a, aa, ba); rec_ci (Mn n f) = (aprog, rs_pos, a_md);
    rec_calc_rel (Mn n f) lm rs\<rbrakk> \<Longrightarrow> aa = Suc rs_pos"
apply(rule_tac calc_mn_reverse, simp)
apply(insert para_pattern [of f a aa ba "lm @ [rs]" 0], simp)
apply(subgoal_tac "rs_pos = length lm", simp)
apply(drule_tac ci_mn_para_eq, simp)
done

lemma [simp]: "\<lbrakk>rec_ci (Mn n f) = (aprog, rs_pos, a_md);      
                rec_calc_rel (Mn n f) lm rs\<rbrakk>  \<Longrightarrow> Suc rs_pos < a_md"
apply(case_tac "rec_ci f")
apply(subgoal_tac "c > b \<and> b = Suc rs_pos \<and> a_md \<ge> c")
apply(arith, auto)
done

lemma mn_ind_steps:  
  assumes ind:
  "\<And>aprog a_md rs_pos rs suf_lm lm. 
  \<lbrakk>rec_ci f = (aprog, rs_pos, a_md); rec_calc_rel f lm rs\<rbrakk> \<Longrightarrow> 
  \<exists>stp. abc_steps_l (0, lm @ 0\<up>(a_md - rs_pos) @ suf_lm) aprog stp = 
              (length aprog, lm @ [rs] @ 0\<up>(a_md - rs_pos - 1) @ suf_lm)"
  and h: "rec_ci f = (a, aa, ba)" 
  "rec_ci (Mn n f) = (aprog, rs_pos, a_md)" 
  "rec_calc_rel (Mn n f) lm rs"
  "rec_calc_rel f (lm @ [rs]) 0" 
  "\<forall>x<rs. (\<exists> v. rec_calc_rel f (lm @ [x]) v \<and> 0 < v)"
  "n = length lm" 
  "x \<le> rs"
  shows "\<exists>stp. abc_steps_l (0, lm @ 0 # 0\<up>(a_md - Suc rs_pos) @ suf_lm)
                 aprog stp = (0, lm @ x # 0\<up>(a_md - Suc rs_pos) @ suf_lm)"
apply(insert h, induct x, 
      rule_tac x = 0 in exI, simp add: abc_steps_zero, simp)
proof -
  fix x
  assume k1: 
    "\<exists>stp. abc_steps_l (0, lm @ 0 # 0\<up>(a_md - Suc rs_pos) @ suf_lm)
                aprog stp = (0, lm @ x # 0\<up>(a_md - Suc rs_pos) @ suf_lm)"
  and k2: "rec_ci (Mn (length lm) f) = (aprog, rs_pos, a_md)" 
          "rec_calc_rel (Mn (length lm) f) lm rs" 
          "rec_calc_rel f (lm @ [rs]) 0" 
          "\<forall>x<rs.(\<exists> v. rec_calc_rel f (lm @ [x]) v \<and> v > 0)" 
          "n = length lm" 
          "Suc x \<le> rs" 
          "rec_ci f = (a, aa, ba)"
  hence k2:
    "\<exists>stp. abc_steps_l (0, lm @ x # 0\<up>(a_md - rs_pos - 1) @ suf_lm) aprog
               stp = (0, lm @ Suc x # 0\<up>(a_md - rs_pos - 1) @ suf_lm)"
    apply(erule_tac x = x in allE)
    apply(auto)
    apply(rule_tac  x = x in mn_ind_step)
    apply(rule_tac ind, auto)      
    done
  from k1 and k2 show 
    "\<exists>stp. abc_steps_l (0, lm @ 0 # 0\<up>(a_md - Suc rs_pos) @ suf_lm)
          aprog stp = (0, lm @ Suc x # 0\<up>(a_md - Suc rs_pos) @ suf_lm)"
    apply(auto)
    apply(rule_tac x = "stp + stpa" in exI, simp only: abc_steps_add)
    done
qed
    
lemma [simp]: 
"\<lbrakk>rec_ci f = (a, aa, ba); 
  rec_ci (Mn n f) = (aprog, rs_pos, a_md); 
  rec_calc_rel (Mn n f) lm rs;
  length lm = n\<rbrakk>
 \<Longrightarrow> abc_lm_v (lm @ rs # 0\<up>(a_md - Suc rs_pos) @ suf_lm) (Suc n) = 0"
apply(auto simp: abc_lm_v.simps nth_append)
done

lemma [simp]: 
  "\<lbrakk>rec_ci f = (a, aa, ba); 
    rec_ci (Mn n f) = (aprog, rs_pos, a_md); 
    rec_calc_rel (Mn n f) lm rs;
     length lm = n\<rbrakk>
    \<Longrightarrow> abc_lm_s (lm @ rs # 0\<up>(a_md - Suc rs_pos) @ suf_lm) (Suc n) 0 =
                           lm @ rs # 0\<up>(a_md - Suc rs_pos) @ suf_lm"
apply(auto simp: abc_lm_s.simps list_update_append)
done

lemma mn_length: 
  "\<lbrakk>rec_ci f = (a, aa, ba);
    rec_ci (Mn n f) = (aprog, rs_pos, a_md)\<rbrakk>
  \<Longrightarrow> length aprog = length a + 5"
apply(simp add: rec_ci.simps, erule_tac conjE)
apply(drule_tac eq_switch, drule_tac eq_switch, simp)
done

lemma mn_final_step:
  assumes ind:
  "\<And>aprog a_md rs_pos rs suf_lm lm.
  \<lbrakk>rec_ci f = (aprog, rs_pos, a_md); 
  rec_calc_rel f lm rs\<rbrakk> \<Longrightarrow> 
  \<exists>stp. abc_steps_l (0, lm @ 0\<up>(a_md - rs_pos) @ suf_lm) aprog stp =
              (length aprog, lm @ [rs] @ 0\<up>(a_md - rs_pos - 1) @ suf_lm)"
  and h: "rec_ci f = (a, aa, ba)" 
         "rec_ci (Mn n f) = (aprog, rs_pos, a_md)" 
         "rec_calc_rel (Mn n f) lm rs" 
         "rec_calc_rel f (lm @ [rs]) 0" 
  shows "\<exists>stp. abc_steps_l (0, lm @ rs # 0\<up>(a_md - Suc rs_pos) @ suf_lm) 
     aprog stp = (length aprog, lm @ rs # 0\<up>(a_md - Suc rs_pos) @ suf_lm)"
proof -
  from h and ind have k1:
    "\<exists>stp.  abc_steps_l (0, lm @ rs # 0\<up>(a_md - Suc rs_pos) @ suf_lm) 
        aprog stp = (length a,  lm @ rs # 0\<up>(a_md - Suc rs_pos) @ suf_lm)"
    apply(insert mn_calc_f[of f a aa ba n aprog 
                               rs_pos a_md lm rs 0 suf_lm], simp)
    apply(subgoal_tac "aa = Suc n", simp add: exponent_cons_iff)
    apply(subgoal_tac "rs_pos = n", simp, simp)
    done
  from h have k2: "length lm = n"
    apply(subgoal_tac "rs_pos = n")
    apply(drule_tac f = "Mn n f" in para_pattern, simp, simp, simp)
    done
  from h and k2 have k3: 
  "\<exists>stp. abc_steps_l (length a, lm @ rs # 0\<up>(a_md - Suc rs_pos) @ suf_lm)
    aprog stp = (length a + 5, lm @ rs # 0\<up>(a_md - Suc rs_pos) @ suf_lm)"
    apply(rule_tac x = "Suc 0" in exI, 
          simp add: abc_step_l.simps abc_steps_l.simps)
    done
  from h have k4: "length aprog = length a + 5"
    apply(simp add: mn_length)
    done
  from k1 and k3 and k4 show "?thesis"
    apply(auto)
    apply(rule_tac x = "stp + stpa" in exI, simp add: abc_steps_add)
    done
qed

lemma mn_case: 
  assumes ind: 
  "\<And>aprog a_md rs_pos rs suf_lm lm.
  \<lbrakk>rec_ci f = (aprog, rs_pos, a_md); rec_calc_rel f lm rs\<rbrakk> \<Longrightarrow> 
  \<exists>stp. abc_steps_l (0, lm @ 0\<up>(a_md - rs_pos) @ suf_lm) aprog stp = 
               (length aprog, lm @ [rs] @ 0\<up>(a_md - rs_pos - 1) @ suf_lm)"
  and h: "rec_ci (Mn n f) = (aprog, rs_pos, a_md)" 
         "rec_calc_rel (Mn n f) lm rs"
  shows "\<exists>stp. abc_steps_l (0, lm @ 0\<up>(a_md - rs_pos) @ suf_lm) aprog stp 
  = (length aprog, lm @ [rs] @ 0\<up>(a_md - rs_pos - 1) @ suf_lm)"
apply(case_tac "rec_ci f", simp)
apply(insert h, rule_tac calc_mn_reverse, simp)
proof -
  fix a b c v
  assume h: "rec_ci f = (a, b, c)" 
            "rec_ci (Mn n f) = (aprog, rs_pos, a_md)" 
            "rec_calc_rel (Mn n f) lm rs" 
            "rec_calc_rel f (lm @ [rs]) 0" 
            "\<forall>x<rs. \<exists>v. rec_calc_rel f (lm @ [x]) v \<and> 0 < v"
            "n = length lm"
  hence k1:
    "\<exists>stp. abc_steps_l (0, lm @ 0 # 0\<up>(a_md - Suc rs_pos) @ suf_lm) aprog
                  stp = (0, lm @ rs # 0\<up>(a_md - Suc rs_pos) @ suf_lm)"
    apply(auto intro: mn_ind_steps ind)
    done
  from h have k2: 
    "\<exists>stp. abc_steps_l (0, lm @ rs # 0\<up>(a_md - Suc rs_pos) @ suf_lm) aprog
         stp = (length aprog, lm @ rs # 0\<up>(a_md - Suc rs_pos) @ suf_lm)"
    apply(auto intro: mn_final_step ind)
    done
  from k1 and k2 show 
    "\<exists>stp. abc_steps_l (0, lm @ 0\<up>(a_md - rs_pos) @ suf_lm) aprog stp = 
  (length aprog, lm @ rs # 0\<up>(a_md - Suc rs_pos) @ suf_lm)"
    apply(auto, insert h)
    apply(subgoal_tac "Suc rs_pos < a_md")
    apply(rule_tac x = "stp + stpa" in exI, 
      simp only: abc_steps_add exponent_cons_iff, simp, simp)
    done
qed

lemma z_rs: "rec_calc_rel z lm rs \<Longrightarrow> rs = 0"
apply(rule_tac calc_z_reverse, auto)
done

lemma z_case:
  "\<lbrakk>rec_ci z = (aprog, rs_pos, a_md); rec_calc_rel z lm rs\<rbrakk>
  \<Longrightarrow> \<exists>stp. abc_steps_l (0, lm @ 0\<up>(a_md - rs_pos) @ suf_lm) aprog stp =
           (length aprog, lm @ [rs] @ 0\<up>(a_md - rs_pos - 1) @ suf_lm)"
apply(simp add: rec_ci.simps rec_ci_z_def, auto)
apply(rule_tac x = "Suc 0" in exI, simp add: abc_steps_l.simps 
                               abc_fetch.simps abc_step_l.simps z_rs)
done

fun addition_inv :: "nat \<times> nat list \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow>     
                     nat list \<Rightarrow> bool"
  where
  "addition_inv (as, lm') m n p lm = 
        (let sn = lm ! n in
         let sm = lm ! m in
         lm ! p = 0 \<and>
             (if as = 0 then \<exists> x. x \<le> lm ! m \<and> lm' = lm[m := x,
                                    n := (sn + sm - x), p := (sm - x)]
             else if as = 1 then \<exists> x. x < lm ! m \<and> lm' = lm[m := x,
                            n := (sn + sm - x - 1), p := (sm - x - 1)]
             else if as = 2 then \<exists> x. x < lm ! m \<and> lm' = lm[m := x, 
                               n := (sn + sm - x), p := (sm - x - 1)]
             else if as = 3 then \<exists> x. x < lm ! m \<and> lm' = lm[m := x,
                                   n := (sn + sm - x), p := (sm - x)]
             else if as = 4 then \<exists> x. x \<le> lm ! m \<and> lm' = lm[m := x,
                                       n := (sn + sm), p := (sm - x)] 
             else if as = 5 then \<exists> x. x < lm ! m \<and> lm' = lm[m := x, 
                                  n := (sn + sm), p := (sm - x - 1)] 
             else if as = 6 then \<exists> x. x < lm ! m \<and> lm' =
                     lm[m := Suc x, n := (sn + sm), p := (sm - x - 1)]
             else if as = 7 then lm' = lm[m := sm, n := (sn + sm)]
             else False))"

fun addition_stage1 :: "nat \<times> nat list \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat"
  where
  "addition_stage1 (as, lm) m p = 
          (if as = 0 \<or> as = 1 \<or> as = 2 \<or> as = 3 then 2 
           else if as = 4 \<or> as = 5 \<or> as = 6 then 1
           else 0)"

fun addition_stage2 :: "nat \<times> nat list \<Rightarrow> nat \<Rightarrow>  nat \<Rightarrow> nat"
  where
  "addition_stage2 (as, lm) m p = 
              (if 0 \<le> as \<and> as \<le> 3 then lm ! m
               else if 4 \<le> as \<and> as \<le> 6 then lm ! p
               else 0)"

fun addition_stage3 :: "nat \<times> nat list \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat"
  where
  "addition_stage3 (as, lm) m p = 
             (if as = 1 then 4  
              else if as = 2 then 3 
              else if as = 3 then 2
              else if as = 0 then 1 
              else if as = 5 then 2
              else if as = 6 then 1 
              else if as = 4 then 0 
              else 0)"

fun addition_measure :: "((nat \<times> nat list) \<times> nat \<times> nat) \<Rightarrow> 
                                                 (nat \<times> nat \<times> nat)"
  where
  "addition_measure ((as, lm), m, p) =
     (addition_stage1 (as, lm) m p, 
      addition_stage2 (as, lm) m p,
      addition_stage3 (as, lm) m p)"

definition addition_LE :: "(((nat \<times> nat list) \<times> nat \<times> nat) \<times> 
                          ((nat \<times> nat list) \<times> nat \<times> nat)) set"
  where "addition_LE \<equiv> (inv_image lex_triple addition_measure)"

lemma [simp]: "wf addition_LE"
by(simp add: wf_inv_image wf_lex_triple addition_LE_def)

declare addition_inv.simps[simp del]

lemma addition_inv_init: 
  "\<lbrakk>m \<noteq> n; max m n < p; length lm > p; lm ! p = 0\<rbrakk> \<Longrightarrow>
                                   addition_inv (0, lm) m n p lm"
apply(simp add: addition_inv.simps)
apply(rule_tac x = "lm ! m" in exI, simp)
done

lemma [simp]: "abc_fetch 0 (addition m n p) = Some (Dec m 4)"
by(simp add: abc_fetch.simps addition.simps)

lemma [simp]: "abc_fetch (Suc 0) (addition m n p) = Some (Inc n)"
by(simp add: abc_fetch.simps addition.simps)

lemma [simp]: "abc_fetch 2 (addition m n p) = Some (Inc p)"
by(simp add: abc_fetch.simps addition.simps)

lemma [simp]: "abc_fetch 3 (addition m n p) = Some (Goto 0)"
by(simp add: abc_fetch.simps addition.simps)

lemma [simp]: "abc_fetch 4 (addition m n p) = Some (Dec p 7)"
by(simp add: abc_fetch.simps addition.simps)

lemma [simp]: "abc_fetch 5 (addition m n p) = Some (Inc m)"
by(simp add: abc_fetch.simps addition.simps)

lemma [simp]: "abc_fetch 6 (addition m n p) = Some (Goto 4)"
by(simp add: abc_fetch.simps addition.simps)

lemma [simp]:
  "\<lbrakk>m \<noteq> n; p < length lm; lm ! p = 0; m < p; n < p; x \<le> lm ! m; 0 < x\<rbrakk>
 \<Longrightarrow> \<exists>xa<lm ! m. lm[m := x, n := lm ! n + lm ! m - x, 
                    p := lm ! m - x, m := x - Suc 0] =
                 lm[m := xa, n := lm ! n + lm ! m - Suc xa,
                    p := lm ! m - Suc xa]"
apply(case_tac x, simp, simp)
apply(rule_tac x = nat in exI, simp add: list_update_swap 
                                         list_update_overwrite)
done

lemma [simp]:
  "\<lbrakk>m \<noteq> n; p < length lm; lm ! p = 0; m < p; n < p; x < lm ! m\<rbrakk>
   \<Longrightarrow> \<exists>xa<lm ! m. lm[m := x, n := lm ! n + lm ! m - Suc x,
                      p := lm ! m - Suc x, n := lm ! n + lm ! m - x]
                 = lm[m := xa, n := lm ! n + lm ! m - xa, 
                      p := lm ! m - Suc xa]"
apply(rule_tac x = x in exI, 
      simp add: list_update_swap list_update_overwrite)
done

lemma [simp]: 
  "\<lbrakk>m \<noteq> n; p < length lm; lm ! p = 0; m < p; n < p; x < lm ! m\<rbrakk>
   \<Longrightarrow> \<exists>xa<lm ! m. lm[m := x, n := lm ! n + lm ! m - x, 
                          p := lm ! m - Suc x, p := lm ! m - x]
                 = lm[m := xa, n := lm ! n + lm ! m - xa, 
                          p := lm ! m - xa]"
apply(rule_tac x = x in exI, simp add: list_update_overwrite)
done

lemma [simp]: 
  "\<lbrakk>m \<noteq> n; p < length lm; lm ! p = (0::nat); m < p; n < p; x < lm ! m\<rbrakk>
  \<Longrightarrow> \<exists>xa\<le>lm ! m. lm[m := x, n := lm ! n + lm ! m - x,
                                   p := lm ! m - x] = 
                  lm[m := xa, n := lm ! n + lm ! m - xa, 
                                   p := lm ! m - xa]"
apply(rule_tac x = x in exI, simp)
done

lemma [simp]: 
  "\<lbrakk>m \<noteq> n; p < length lm; lm ! p = 0; m < p; n < p;
    x \<le> lm ! m; lm ! m \<noteq> x\<rbrakk>
  \<Longrightarrow> \<exists>xa<lm ! m. lm[m := x, n := lm ! n + lm ! m, 
                       p := lm ! m - x, p := lm ! m - Suc x] 
               = lm[m := xa, n := lm ! n + lm ! m, 
                       p := lm ! m - Suc xa]"
apply(rule_tac x = x in exI, simp add: list_update_overwrite)
done

lemma [simp]:
  "\<lbrakk>m \<noteq> n; p < length lm; lm ! p = 0; m < p; n < p; x < lm ! m\<rbrakk>
  \<Longrightarrow> \<exists>xa<lm ! m. lm[m := x, n := lm ! n + lm ! m,
                             p := lm ! m - Suc x, m := Suc x]
                = lm[m := Suc xa, n := lm ! n + lm ! m, 
                             p := lm ! m - Suc xa]"
apply(rule_tac x = x in exI, 
     simp add: list_update_swap list_update_overwrite)
done

lemma [simp]: 
  "\<lbrakk>m \<noteq> n; p < length lm; lm ! p = 0; m < p; n < p; x < lm ! m\<rbrakk>
  \<Longrightarrow> \<exists>xa\<le>lm ! m. lm[m := Suc x, n := lm ! n + lm ! m, 
                             p := lm ! m - Suc x] 
               = lm[m := xa, n := lm ! n + lm ! m, p := lm ! m - xa]"
apply(rule_tac x = "Suc x" in exI, simp)
done

lemma addition_halt_lemma: 
  "\<lbrakk>m \<noteq> n; max m n < p; length lm > p; lm ! p = 0\<rbrakk> \<Longrightarrow>
  \<forall>na. \<not> (\<lambda>(as, lm') (m, p). as = 7) 
        (abc_steps_l (0, lm) (addition m n p) na) (m, p) \<and> 
  addition_inv (abc_steps_l (0, lm) (addition m n p) na) m n p lm 
\<longrightarrow> addition_inv (abc_steps_l (0, lm) (addition m n p) 
                                 (Suc na)) m n p lm 
  \<and> ((abc_steps_l (0, lm) (addition m n p) (Suc na), m, p), 
     abc_steps_l (0, lm) (addition m n p) na, m, p) \<in> addition_LE"
apply(rule allI, rule impI, simp add: abc_steps_ind)
apply(case_tac "(abc_steps_l (0, lm) (addition m n p) na)", simp)
apply(auto split:if_splits simp add: addition_inv.simps
                                 abc_steps_zero)
apply(simp_all add: abc_steps_l.simps abc_steps_zero)
apply(auto simp add: addition_LE_def lex_triple_def lex_pair_def 
                     abc_step_l.simps addition_inv.simps 
                     abc_lm_v.simps abc_lm_s.simps nth_append
                split: if_splits)
apply(rule_tac x = x in exI, simp)
done

lemma  addition_ex: 
  "\<lbrakk>m \<noteq> n; max m n < p; length lm > p; lm ! p = 0\<rbrakk> \<Longrightarrow> 
  \<exists> stp. (\<lambda> (as, lm'). as = 7 \<and> addition_inv (as, lm') m n p lm) 
                        (abc_steps_l (0, lm) (addition m n p) stp)"
apply(insert halt_lemma2[of addition_LE
  "\<lambda> ((as, lm'), m, p). addition_inv (as, lm') m n p lm"
  "\<lambda> stp. (abc_steps_l (0, lm) (addition m n p) stp, m, p)"
  "\<lambda> ((as, lm'), m, p). as = 7"], 
  simp add: abc_steps_zero addition_inv_init)
apply(drule_tac addition_halt_lemma, simp, simp, simp,
      simp, erule_tac exE)
apply(rule_tac x = na in exI, 
      case_tac "(abc_steps_l (0, lm) (addition m n p) na)", auto)
done

lemma [simp]: "length (addition m n p) = 7"
by (simp add: addition.simps)

lemma [elim]: "addition 0 (Suc 0) 2 = [] \<Longrightarrow> RR"
by(simp add: addition.simps)

lemma [simp]: "(0\<up>2)[0 := n] = [n, 0::nat]"
apply(subgoal_tac "2 = Suc 1", 
      simp only: replicate.simps)
apply(auto)
done

lemma [simp]: 
  "\<exists>stp. abc_steps_l (0, n # 0\<up>2 @ suf_lm) 
     (addition 0 (Suc 0) 2 [+] [Inc (Suc 0)]) stp = 
                                      (8, n # Suc n # 0 # suf_lm)"
apply(rule_tac bm = "n # n # 0 # suf_lm" in abc_append_exc2, auto)
apply(insert addition_ex[of 0 "Suc 0" 2 "n # 0\<up>2 @ suf_lm"], 
      simp add: nth_append numeral_2_eq_2, erule_tac exE)
apply(rule_tac x = stp in exI,
      case_tac "(abc_steps_l (0, n # 0\<up>2 @ suf_lm)
                      (addition 0 (Suc 0) 2) stp)", 
      simp add: addition_inv.simps nth_append list_update_append numeral_2_eq_2)
apply(simp add: nth_append numeral_2_eq_2, erule_tac exE)
apply(rule_tac x = "Suc 0" in exI,
      simp add: abc_steps_l.simps abc_fetch.simps 
      abc_steps_zero abc_step_l.simps abc_lm_s.simps abc_lm_v.simps)
done

lemma s_case:
  "\<lbrakk>rec_ci s = (aprog, rs_pos, a_md); rec_calc_rel s lm rs\<rbrakk>
  \<Longrightarrow> \<exists>stp. abc_steps_l (0, lm @ 0\<up>(a_md - rs_pos) @ suf_lm) aprog stp =
               (length aprog, lm @ [rs] @ 0\<up>(a_md - rs_pos - 1) @ suf_lm)"
apply(simp add: rec_ci.simps rec_ci_s_def, auto)
apply(rule_tac calc_s_reverse, auto)
done

lemma [simp]: 
  "\<lbrakk>n < length lm; lm ! n = rs\<rbrakk>
    \<Longrightarrow> \<exists>stp. abc_steps_l (0, lm @ 0 # 0 #suf_lm)
                     (addition n (length lm) (Suc (length lm))) stp 
             = (7, lm @ rs # 0 # suf_lm)"
apply(insert addition_ex[of n "length lm"
                           "Suc (length lm)" "lm @ 0 # 0 # suf_lm"])
apply(simp add: nth_append, erule_tac exE)
apply(rule_tac x = stp in exI)
apply(case_tac "abc_steps_l (0, lm @ 0 # 0 # suf_lm) (addition n (length lm)
                 (Suc (length lm))) stp", simp)
apply(simp add: addition_inv.simps)
apply(insert nth_append[of lm "0 # 0 # suf_lm" "n"], simp)
done

lemma [simp]: "0\<up>2 = [0, 0::nat]"
apply(auto simp:numeral_2_eq_2)
done

lemma id_case: 
  "\<lbrakk>rec_ci (id m n) = (aprog, rs_pos, a_md); 
    rec_calc_rel (id m n) lm rs\<rbrakk>
  \<Longrightarrow> \<exists>stp. abc_steps_l (0, lm @ 0\<up>(a_md - rs_pos) @ suf_lm) aprog stp = 
               (length aprog, lm @ [rs] @ 0\<up>(a_md - rs_pos - 1) @ suf_lm)"
apply(simp add: rec_ci.simps rec_ci_id.simps, auto)
apply(rule_tac calc_id_reverse, simp, simp)
done   

lemma list_tl_induct:
  "\<lbrakk>P []; \<And>a list. P list \<Longrightarrow> P (list @ [a::'a])\<rbrakk> \<Longrightarrow> 
                                            P ((list::'a list))"
apply(case_tac "length list", simp)
proof -
  fix nat
  assume ind: "\<And>a list. P list \<Longrightarrow> P (list @ [a])"
  and h: "length list = Suc nat" "P []"
  from h show "P list"
  proof(induct nat arbitrary: list, case_tac lista, simp, simp)
    fix lista a listaa
    from h show "P [a]"
      by(insert ind[of "[]"], simp add: h)
  next
    fix nat list
    assume nind: "\<And>list. \<lbrakk>length list = Suc nat; P []\<rbrakk> \<Longrightarrow> P list" 
    and g: "length (list:: 'a list) = Suc (Suc nat)"
    from g show "P (list::'a list)"
      apply(insert nind[of "butlast list"], simp add: h)
      apply(insert ind[of "butlast list" "last list"], simp)
      apply(subgoal_tac "butlast list @ [last list] = list", simp)
      apply(case_tac "list::'a list", simp, simp)
      done
  qed
qed      
  
lemma nth_eq_butlast_nth: "\<lbrakk>length ys > Suc k\<rbrakk> \<Longrightarrow> 
                                        ys ! k = butlast ys ! k"
apply(subgoal_tac "\<exists> xs y. ys = xs @ [y]", auto simp: nth_append)
apply(rule_tac x = "butlast ys" in exI, rule_tac x = "last ys" in exI)
apply(case_tac "ys = []", simp, simp)
done

lemma [simp]: 
"\<lbrakk>\<forall>k<Suc (length list). rec_calc_rel ((list @ [a]) ! k) lm (ys ! k);
  length ys = Suc (length list)\<rbrakk>
   \<Longrightarrow> \<forall>k<length list. rec_calc_rel (list ! k) lm (butlast ys ! k)"
apply(rule allI, rule impI)
apply(erule_tac  x = k in allE, simp add: nth_append)
apply(subgoal_tac "ys ! k = butlast ys ! k", simp)
apply(rule_tac nth_eq_butlast_nth, arith)
done

lemma cn_merge_gs_tl_app: 
  "cn_merge_gs (gs @ [g]) pstr = 
        cn_merge_gs gs pstr [+] cn_merge_gs [g] (pstr + length gs)"
apply(induct gs arbitrary: pstr, simp add: cn_merge_gs.simps, simp)
apply(case_tac a, simp add: abc_append_commute)
done

lemma cn_merge_gs_length: 
  "length (cn_merge_gs (map rec_ci list) pstr) = 
      (\<Sum>(ap, pos, n)\<leftarrow>map rec_ci list. length ap) + 3 * length list "
apply(induct list arbitrary: pstr, simp, simp)
apply(case_tac "rec_ci a", simp)
done

lemma [simp]: "Suc n \<le> pstr \<Longrightarrow> pstr + x - n > 0"
by arith

lemma [simp]:
  "\<lbrakk>Suc (pstr + length list) \<le> a_md; 
    length ys = Suc (length list);
    length lm = n;
     Suc n \<le> pstr\<rbrakk>
   \<Longrightarrow>  (ys ! length list # 0\<up>(pstr - Suc n) @ butlast ys @
             0\<up>(a_md - (pstr + length list)) @ suf_lm) ! 
                      (pstr + length list - n) = (0 :: nat)"
apply(insert nth_append[of "ys ! length list # 0\<up>(pstr - Suc n) @
     butlast ys" "0\<up>(a_md - (pstr + length list)) @ suf_lm"
      "(pstr + length list - n)"], simp add: nth_append)
done

lemma [simp]:
  "\<lbrakk>Suc (pstr + length list) \<le> a_md; 
    length ys = Suc (length list);
    length lm = n;
     Suc n \<le> pstr\<rbrakk>
    \<Longrightarrow> (lm @ last ys # 0\<up>(pstr - Suc n) @ butlast ys @
         0\<up>(a_md - (pstr + length list)) @ suf_lm)[pstr + length list := 
                                        last ys, n := 0] =
        lm @ (0::nat)\<up>(pstr - n) @ ys @ 0\<up>(a_md - Suc (pstr + length list)) @ suf_lm"
apply(insert list_update_length[of 
   "lm @ last ys # 0\<up>(pstr - Suc n) @ butlast ys" 0 
   "0\<up>(a_md - Suc (pstr + length list)) @ suf_lm" "last ys"], simp)
apply(simp add: exponent_cons_iff)
apply(insert list_update_length[of "lm" 
        "last ys" "0\<up>(pstr - Suc n) @ butlast ys @ 
      last ys # 0\<up>(a_md - Suc (pstr + length list)) @ suf_lm" 0], simp)
apply(simp add: exponent_cons_iff)
apply(case_tac "ys = []", simp_all add: append_butlast_last_id)
done

lemma cn_merge_gs_ex: 
  "\<lbrakk>\<And>x aprog a_md rs_pos rs suf_lm lm.
    \<lbrakk>x \<in> set gs; rec_ci x = (aprog, rs_pos, a_md);
     rec_calc_rel x lm rs\<rbrakk>
     \<Longrightarrow> \<exists>stp. abc_steps_l (0, lm @ 0\<up>(a_md - rs_pos) @ suf_lm) aprog stp 
           = (length aprog, lm @ [rs] @ 0\<up>(a_md - rs_pos - 1) @ suf_lm); 
   pstr + length gs\<le> a_md;
   \<forall>k<length gs. rec_calc_rel (gs ! k) lm (ys ! k);
   length ys = length gs; length lm = n;
   pstr \<ge> Max (set (Suc n # map (\<lambda>(aprog, p, n). n) (map rec_ci gs)))\<rbrakk>
  \<Longrightarrow> \<exists> stp. abc_steps_l (0, lm @ 0\<up>(a_md - n) @ suf_lm)
                   (cn_merge_gs (map rec_ci gs) pstr) stp 
   = (listsum (map ((\<lambda>(ap, pos, n). length ap) \<circ> rec_ci) gs) +
  3 * length gs, lm @ 0\<up>(pstr - n) @ ys @ 0\<up>(a_md - (pstr + length gs)) @ suf_lm)"
apply(induct gs arbitrary: ys rule: list_tl_induct)
apply(simp add: exponent_add_iff, simp)
proof -
  fix a list ys
  assume ind: "\<And>x aprog a_md rs_pos rs suf_lm lm.
    \<lbrakk>x = a \<or> x \<in> set list; rec_ci x = (aprog, rs_pos, a_md); 
     rec_calc_rel x lm rs\<rbrakk>
    \<Longrightarrow> \<exists>stp. abc_steps_l (0, lm @ 0\<up>(a_md - rs_pos) @ suf_lm) aprog stp =
                (length aprog, lm @ rs # 0\<up>(a_md - Suc rs_pos) @ suf_lm)"
  and ind2: 
    "\<And>ys. \<lbrakk>\<And>x aprog a_md rs_pos rs suf_lm lm.
    \<lbrakk>x \<in> set list; rec_ci x = (aprog, rs_pos, a_md);
     rec_calc_rel x lm rs\<rbrakk>
    \<Longrightarrow> \<exists>stp. abc_steps_l (0, lm @ 0\<up>(a_md - rs_pos) @ suf_lm) aprog stp
        = (length aprog, lm @ rs # 0\<up>(a_md - Suc rs_pos) @ suf_lm);
    \<forall>k<length list. rec_calc_rel (list ! k) lm (ys ! k); 
    length ys = length list\<rbrakk>
    \<Longrightarrow> \<exists>stp. abc_steps_l (0, lm @ 0\<up>(a_md - n) @ suf_lm) 
                   (cn_merge_gs (map rec_ci list) pstr) stp =
    (listsum (map ((\<lambda>(ap, pos, n). length ap) \<circ> rec_ci) list) +
     3 * length list,
                lm @ 0\<up>(pstr - n) @ ys @ 0\<up>(a_md - (pstr + length list)) @ suf_lm)"
    and h: "Suc (pstr + length list) \<le> a_md" 
            "\<forall>k<Suc (length list). 
                   rec_calc_rel ((list @ [a]) ! k) lm (ys ! k)" 
            "length ys = Suc (length list)" 
            "length lm = n"
            "Suc n \<le> pstr \<and> (\<lambda>(aprog, p, n). n) (rec_ci a) \<le> pstr \<and> 
            (\<forall>a\<in>set list. (\<lambda>(aprog, p, n). n) (rec_ci a) \<le> pstr)"
  from h have k1: 
    "\<exists>stp. abc_steps_l (0, lm @ 0\<up>(a_md - n) @ suf_lm)
                     (cn_merge_gs (map rec_ci list) pstr) stp =
    (listsum (map ((\<lambda>(ap, pos, n). length ap) \<circ> rec_ci) list) +
     3 * length list, lm @ 0\<up>(pstr - n) @ butlast ys @
                               0\<up>(a_md - (pstr + length list)) @ suf_lm) "
    apply(rule_tac ind2)
    apply(rule_tac ind, auto)
    done
  from k1 and h show 
    "\<exists>stp. abc_steps_l (0, lm @ 0\<up>(a_md - n) @ suf_lm) 
          (cn_merge_gs (map rec_ci list @ [rec_ci a]) pstr) stp =
        (listsum (map ((\<lambda>(ap, pos, n). length ap) \<circ> rec_ci) list) + 
        (\<lambda>(ap, pos, n). length ap) (rec_ci a) + (3 + 3 * length list),
             lm @ 0\<up>(pstr - n) @ ys @ 0\<up>(a_md - Suc (pstr + length list)) @ suf_lm)"
    apply(simp add: cn_merge_gs_tl_app)
    apply(rule_tac as = 
  "(\<Sum>(ap, pos, n)\<leftarrow>map rec_ci list. length ap) + 3 * length list"    
      and bm = "lm @ 0\<up>(pstr - n) @ butlast ys @ 
                              0\<up>(a_md - (pstr + length list)) @ suf_lm" 
      and bs = "(\<lambda>(ap, pos, n). length ap) (rec_ci a) + 3" 
      and bm' = "lm @ 0\<up>(pstr - n) @ ys @ 0\<up>(a_md - Suc (pstr + length list)) @ 
                                  suf_lm" in abc_append_exc2, simp)
    apply(simp add: cn_merge_gs_length)
  proof -
    from h show 
      "\<exists>bstp. abc_steps_l (0, lm @ 0\<up>(pstr - n) @ butlast ys @ 
                                  0\<up>(a_md - (pstr + length list)) @ suf_lm) 
              ((\<lambda>(gprog, gpara, gn). gprog [+] mv_box gpara 
              (pstr + length list)) (rec_ci a)) bstp =
              ((\<lambda>(ap, pos, n). length ap) (rec_ci a) + 3, 
             lm @ 0\<up>(pstr - n) @ ys @ 0\<up>(a_md - Suc (pstr + length list)) @ suf_lm)"
      apply(case_tac "rec_ci a", simp)
      apply(rule_tac as = "length aa" and 
                     bm = "lm @ (ys ! (length list)) # 
          0\<up>(pstr - Suc n) @ butlast ys @ 0\<up>(a_md - (pstr + length list)) @ suf_lm" 
        and bs = "3" and bm' = "lm @ 0\<up>(pstr - n) @ ys @
             0\<up>(a_md - Suc (pstr + length list)) @ suf_lm" in abc_append_exc2)
    proof -
      fix aa b c
      assume g: "rec_ci a = (aa, b, c)"
      from h and g have k2: "b = n"
	apply(erule_tac x = "length list" in allE, simp)
	apply(subgoal_tac "length lm = b", simp)
	apply(rule para_pattern, simp, simp)
	done
      from h and g and this show 
        "\<exists>astp. abc_steps_l (0, lm @ 0\<up>(pstr - n) @ butlast ys @ 
                         0\<up>(a_md - (pstr + length list)) @ suf_lm) aa astp =
        (length aa, lm @ ys ! length list # 0\<up>(pstr - Suc n) @ 
                       butlast ys @ 0\<up>(a_md - (pstr + length list)) @ suf_lm)"
	apply(subgoal_tac "c \<ge> Suc n")
	apply(insert ind[of a aa b c lm "ys ! length list" 
          "0\<up>(pstr - c) @ butlast ys @ 0\<up>(a_md - (pstr + length list)) @ suf_lm"], simp)
	apply(erule_tac x = "length list" in allE, 
              simp add: exponent_add_iff)
	apply(rule_tac Suc_leI, rule_tac ci_ad_ge_paras, simp)
	done
    next
      fix aa b c
      show "length aa = length aa" by simp 
    next
      fix aa b c
      assume "rec_ci a = (aa, b, c)"
      from h and this show     
      "\<exists>bstp. abc_steps_l (0, lm @ ys ! length list #
          0\<up>(pstr - Suc n) @ butlast ys @ 0\<up>(a_md - (pstr + length list)) @ suf_lm)
                 (mv_box b (pstr + length list)) bstp =
       (3, lm @ 0\<up>(pstr - n) @ ys @ 0\<up>(a_md - Suc (pstr + length list)) @ suf_lm)"
	apply(insert mv_box_ex [of b "pstr + length list" 
         "lm @ ys ! length list # 0\<up>(pstr - Suc n) @ butlast ys @ 
         0\<up>(a_md - (pstr + length list)) @ suf_lm"], simp)
        apply(subgoal_tac "b = n")
	apply(simp add: nth_append split: if_splits)
	apply(erule_tac x = "length list" in allE, simp)
        apply(drule para_pattern, simp, simp)
	done
    next
      fix aa b c
      show "3 = length (mv_box b (pstr + length list))" 
        by simp
    next
      fix aa b aaa ba
      show "length aa + 3 = length aa + 3" by simp
    next
      fix aa b c
      show "mv_box b (pstr + length list) \<noteq> []" 
        by(simp add: mv_box.simps)
    qed
  next
    show "(\<lambda>(ap, pos, n). length ap) (rec_ci a) + 3 = 
        length ((\<lambda>(gprog, gpara, gn). gprog [+]
           mv_box gpara (pstr + length list)) (rec_ci a))"
      by(case_tac "rec_ci a", simp)
  next
    show "listsum (map ((\<lambda>(ap, pos, n). length ap) \<circ> rec_ci) list) +
      (\<lambda>(ap, pos, n). length ap) (rec_ci a) + (3 + 3 * length list)=
      (\<Sum>(ap, pos, n)\<leftarrow>map rec_ci list. length ap) + 3 * length list + 
                ((\<lambda>(ap, pos, n). length ap) (rec_ci a) + 3)" by simp
  next
    show "(\<lambda>(gprog, gpara, gn). gprog [+] 
      mv_box gpara (pstr + length list)) (rec_ci a) \<noteq> []"
      by(case_tac "rec_ci a", 
         simp add: abc_append.simps abc_shift.simps)
  qed
qed
 
lemma [simp]: "length (mv_boxes aa ba n) = 3*n"
by(induct n, auto simp: mv_boxes.simps)

lemma exp_suc: "a\<up>Suc b = a\<up>b @ [a]"
by(simp add: exp_ind del: replicate.simps)

lemma [simp]: 
  "\<lbrakk>Suc n \<le> ba - aa;  length lm2 = Suc n;
    length lm3 = ba - Suc (aa + n)\<rbrakk>
  \<Longrightarrow> (last lm2 # lm3 @ butlast lm2 @ 0 # lm4) ! (ba - aa) = (0::nat)"
proof -
  assume h: "Suc n \<le> ba - aa"
  and g: "length lm2 = Suc n" "length lm3 = ba - Suc (aa + n)"
  from h and g have k: "ba - aa = Suc (length lm3 + n)"
    by arith
  from  k show 
    "(last lm2 # lm3 @ butlast lm2 @ 0 # lm4) ! (ba - aa) = 0"
    apply(simp, insert g)
    apply(simp add: nth_append)
    done
qed

lemma [simp]: "length lm1 = aa \<Longrightarrow>
      (lm1 @ 0\<up>n @ last lm2 # lm3 @ butlast lm2 @ 0 # lm4) ! (aa + n) = last lm2"
apply(simp add: nth_append)
done

lemma [simp]: "\<lbrakk>Suc n \<le> ba - aa; aa < ba\<rbrakk> \<Longrightarrow> 
                    (ba < Suc (aa + (ba - Suc (aa + n) + n))) = False"
apply arith
done

lemma [simp]: "\<lbrakk>Suc n \<le> ba - aa; aa < ba; length lm1 = aa; 
       length lm2 = Suc n; length lm3 = ba - Suc (aa + n)\<rbrakk>
     \<Longrightarrow> (lm1 @ 0\<up>n @ last lm2 # lm3 @ butlast lm2 @ 0 # lm4) ! (ba + n) = 0"
using nth_append[of "lm1 @ (0\<Colon>'a)\<up>n @ last lm2 # lm3 @ butlast lm2" 
                     "(0\<Colon>'a) # lm4" "ba + n"]
apply(simp)
done

lemma [simp]: 
 "\<lbrakk>Suc n \<le> ba - aa; aa < ba; length lm1 = aa; length lm2 = Suc n;
                 length lm3 = ba - Suc (aa + n)\<rbrakk>
  \<Longrightarrow> (lm1 @ 0\<up>n @ last lm2 # lm3 @ butlast lm2 @ (0::nat) # lm4)
  [ba + n := last lm2, aa + n := 0] = 
  lm1 @ 0 # 0\<up>n @ lm3 @ lm2 @ lm4"
using list_update_append[of "lm1 @ 0\<up>n @ last lm2 # lm3 @ butlast lm2" "0 # lm4" 
                            "ba + n" "last lm2"]
apply(simp)
apply(simp add: list_update_append)
apply(simp only: exponent_cons_iff exp_suc, simp)
apply(case_tac lm2, simp, simp)
done

lemma mv_boxes_ex:
  "\<lbrakk>n \<le> ba - aa; ba > aa; length lm1 = aa; 
    length (lm2::nat list) = n; length lm3 = ba - aa - n\<rbrakk>
     \<Longrightarrow> \<exists> stp. abc_steps_l (0, lm1 @ lm2 @ lm3 @ 0\<up>n @ lm4)
       (mv_boxes aa ba n) stp = (3 * n, lm1 @ 0\<up>n @ lm3 @ lm2 @ lm4)"
apply(induct n arbitrary: lm2 lm3 lm4, simp)
apply(rule_tac x = 0 in exI, simp add: abc_steps_zero, 
              simp add: mv_boxes.simps del: exp_suc_iff)
apply(rule_tac as = "3 *n" and bm = "lm1 @ 0\<up>n @ last lm2 # lm3 @
               butlast lm2 @ 0 # lm4" in abc_append_exc2, simp_all)
apply(simp only: exponent_cons_iff, simp only: exp_suc, simp)
proof -
  fix n lm2 lm3 lm4
  assume ind:
    "\<And>lm2 lm3 lm4. \<lbrakk>length lm2 = n; length lm3 = ba - (aa + n)\<rbrakk> \<Longrightarrow>
    \<exists>stp. abc_steps_l (0, lm1 @ lm2 @ lm3 @ 0\<up>n @ lm4) 
       (mv_boxes aa ba n) stp = (3 * n, lm1 @ 0\<up>n @ lm3 @ lm2 @ lm4)"
  and h: "Suc n \<le> ba - aa" "aa < ba" "length (lm1::nat list) = aa" 
         "length (lm2::nat list) = Suc n" 
         "length (lm3::nat list) = ba - Suc (aa + n)"
  from h show 
    "\<exists>astp. abc_steps_l (0, lm1 @ lm2 @ lm3 @ 0\<up>n @ 0 # lm4) 
                       (mv_boxes aa ba n) astp = 
        (3 * n, lm1 @ 0\<up>n @ last lm2 # lm3 @ butlast lm2 @ 0 # lm4)"
    apply(insert ind[of "butlast lm2" "last lm2 # lm3" "0 # lm4"], 
          simp)
    apply(subgoal_tac "lm1 @ butlast lm2 @ last lm2 # lm3 @ 0\<up>n @ 
              0 # lm4 = lm1 @ lm2 @ lm3 @ 0\<up>n @ 0 # lm4", simp, simp)
    apply(case_tac "lm2 = []", simp, simp)
    done
next
  fix n lm2 lm3 lm4
  assume h: "Suc n \<le> ba - aa"
            "aa < ba" 
            "length (lm1::nat list) = aa" 
            "length (lm2::nat list) = Suc n" 
            "length (lm3::nat list) = ba - Suc (aa + n)"
  thus " \<exists>bstp. abc_steps_l (0, lm1 @ 0\<up>n @ last lm2 # lm3 @
                       butlast lm2 @ 0 # lm4) 
                         (mv_box (aa + n) (ba + n)) bstp
               = (3, lm1 @ 0 # 0\<up>n @ lm3 @ lm2 @ lm4)"
    apply(insert mv_box_ex[of "aa + n" "ba + n" 
       "lm1 @ 0\<up>n @ last lm2 # lm3 @ butlast lm2 @ 0 # lm4"], simp)
    done
qed

lemma [simp]: "\<lbrakk>Suc n \<le> aa - ba; ba < aa; length lm1 = ba; 
        length lm2 = aa - Suc (ba + n); length lm3 = Suc n\<rbrakk>
   \<Longrightarrow> (lm1 @ butlast lm3 @ 0 # lm2 @ 0\<up>n @ last lm3 # lm4) ! (aa + n) = last lm3"
using nth_append[of "lm1 @ butlast lm3 @ 0 # lm2 @ 0\<up>n" "last lm3 # lm4" "aa + n"]
apply(simp)
done

lemma [simp]: "\<lbrakk>Suc n \<le> aa - ba; ba < aa; length lm1 = ba; 
        length lm2 = aa - Suc (ba + n); length lm3 = Suc n\<rbrakk>
     \<Longrightarrow> (lm1 @ butlast lm3 @ 0 # lm2 @ 0\<up>n @ last lm3 # lm4) ! (ba + n) = 0"
apply(simp add: nth_append)
done

lemma [simp]: "\<lbrakk>Suc n \<le> aa - ba; ba < aa; length lm1 = ba; 
        length lm2 = aa - Suc (ba + n); length lm3 = Suc n\<rbrakk> 
     \<Longrightarrow> (lm1 @ butlast lm3 @ 0 # lm2 @ 0\<up>n @ last lm3 # lm4)[ba + n := last lm3, aa + n := 0]
      = lm1 @ lm3 @ lm2 @ 0 # 0\<up>n @ lm4"
using list_update_append[of "lm1 @ butlast lm3" "(0\<Colon>'a) # lm2 @ (0\<Colon>'a)\<up>n @ last lm3 # lm4"]
apply(simp)
using list_update_append[of "lm1 @ butlast lm3 @ last lm3 # lm2 @ (0\<Colon>'a)\<up>n"
                            "last lm3 # lm4" "aa + n" "0"]
apply(simp)
apply(simp only: replicate_Suc[THEN sym] exp_suc, simp)
apply(case_tac lm3, simp, simp)
done

lemma mv_boxes_ex2:
  "\<lbrakk>n \<le> aa - ba; 
    ba < aa; 
    length (lm1::nat list) = ba;
    length (lm2::nat list) = aa - ba - n; 
    length (lm3::nat list) = n\<rbrakk>
     \<Longrightarrow> \<exists> stp. abc_steps_l (0, lm1 @ 0\<up>n @ lm2 @ lm3 @ lm4) 
                (mv_boxes aa ba n) stp =
                    (3 * n, lm1 @ lm3 @ lm2 @ 0\<up>n @ lm4)"
apply(induct n arbitrary: lm2 lm3 lm4, simp)
apply(rule_tac x = 0 in exI, simp add: abc_steps_zero, 
                   simp add: mv_boxes.simps del: exp_suc_iff)
apply(rule_tac as = "3 *n" and bm = "lm1 @ butlast lm3 @ 0 # lm2 @
                  0\<up>n @ last lm3 # lm4" in abc_append_exc2, simp_all)
apply(simp only: exponent_cons_iff, simp only: exp_suc, simp)
proof -
  fix n lm2 lm3 lm4
  assume ind: 
"\<And>lm2 lm3 lm4. \<lbrakk>length lm2 = aa - (ba + n); length lm3 = n\<rbrakk> \<Longrightarrow> 
  \<exists>stp. abc_steps_l (0, lm1 @ 0\<up>n @ lm2 @ lm3 @ lm4) 
                 (mv_boxes aa ba n) stp = 
                            (3 * n, lm1 @ lm3 @ lm2 @ 0\<up>n @ lm4)"
  and h: "Suc n \<le> aa - ba" 
         "ba < aa"  
         "length (lm1::nat list) = ba" 
         "length (lm2::nat list) = aa - Suc (ba + n)" 
         "length (lm3::nat list) = Suc n"
  from h show
    "\<exists>astp. abc_steps_l (0, lm1 @ 0\<up>n @ 0 # lm2 @ lm3 @ lm4)
        (mv_boxes aa ba n) astp = 
          (3 * n, lm1 @ butlast lm3 @ 0 # lm2 @ 0\<up>n @ last lm3 # lm4)"
    apply(insert ind[of "0 # lm2" "butlast lm3" "last lm3 # lm4"],
          simp)
    apply(subgoal_tac
      "lm1 @ 0\<up>n @ 0 # lm2 @ butlast lm3 @ last lm3 # lm4 =
           lm1 @ 0\<up>n @ 0 # lm2 @ lm3 @ lm4", simp, simp)
    apply(case_tac "lm3 = []", simp, simp)
    done
next
  fix n lm2 lm3 lm4
  assume h:
    "Suc n \<le> aa - ba" 
    "ba < aa"
    "length lm1 = ba"
    "length (lm2::nat list) = aa - Suc (ba + n)" 
    "length (lm3::nat list) = Suc n"
  thus
    "\<exists>bstp. abc_steps_l (0, lm1 @ butlast lm3 @ 0 # lm2 @ 0\<up>n @ 
                               last lm3 # lm4) 
           (mv_box (aa + n) (ba + n)) bstp =
                 (3, lm1 @ lm3 @ lm2 @ 0 # 0\<up>n @ lm4)"
    apply(insert mv_box_ex[of "aa + n" "ba + n" "lm1 @ butlast lm3 @ 
                          0 # lm2 @ 0\<up>n @ last lm3 # lm4"], simp)
    done
qed

lemma cn_merge_gs_len: 
  "length (cn_merge_gs (map rec_ci gs) pstr) = 
      (\<Sum>(ap, pos, n)\<leftarrow>map rec_ci gs. length ap) + 3 * length gs"
apply(induct gs arbitrary: pstr, simp, simp)
apply(case_tac "rec_ci a", simp)
done

lemma [simp]: "n < pstr \<Longrightarrow>
     Suc (pstr + length ys - n) = Suc (pstr + length ys) - n"
by arith

lemma save_paras':  
  "\<lbrakk>length lm = n; pstr > n; a_md > pstr + length ys + n\<rbrakk>
  \<Longrightarrow> \<exists>stp. abc_steps_l (0, lm @ 0\<up>(pstr - n) @ ys @
               0\<up>(a_md - pstr - length ys) @ suf_lm) 
                 (mv_boxes 0 (pstr + Suc (length ys)) n) stp
        = (3 * n, 0\<up>pstr @ ys @ 0 # lm @ 0\<up>(a_md - Suc (pstr + length ys + n)) @ suf_lm)"
apply(insert mv_boxes_ex[of n "pstr + Suc (length ys)" 0 "[]" "lm" 
         "0\<up>(pstr - n) @ ys @ [0]" "0\<up>(a_md - pstr - length ys - n - Suc 0) @ suf_lm"], simp)
apply(erule_tac exE, rule_tac x = stp in exI,
                            simp add: exponent_add_iff)
apply(simp only: exponent_cons_iff, simp)
done

lemma [simp]:
 "(max ba (Max (insert ba (((\<lambda>(aprog, p, n). n) o rec_ci) ` set gs))))
 = (Max (insert ba (((\<lambda>(aprog, p, n). n) o rec_ci) ` set gs)))"
apply(rule min_max.sup_absorb2, auto)
done

lemma [simp]:
  "((\<lambda>(aprog, p, n). n) ` rec_ci ` set gs) = 
                  (((\<lambda>(aprog, p, n). n) o rec_ci) ` set gs)"
apply(induct gs)
apply(simp, simp)
done

lemma ci_cn_md_def:  
  "\<lbrakk>rec_ci (Cn n f gs) = (aprog, rs_pos, a_md); 
  rec_ci f = (a, aa, ba)\<rbrakk>
    \<Longrightarrow> a_md = max (Suc n) (Max (insert ba (((\<lambda>(aprog, p, n). n) o 
  rec_ci) ` set gs))) + Suc (length gs) + n"
apply(simp add: rec_ci.simps, auto)
done

lemma save_paras_prog_ex:
  "\<lbrakk>rec_ci (Cn n f gs) = (aprog, rs_pos, a_md); 
    rec_ci f = (a, aa, ba); 
    pstr = Max (set (Suc n # ba # map (\<lambda>(aprog, p, n). n)
                                    (map rec_ci (gs))))\<rbrakk>
    \<Longrightarrow> \<exists>ap bp cp. 
      aprog = ap [+] bp [+] cp \<and>
      length ap = (\<Sum>(ap, pos, n)\<leftarrow>map rec_ci gs. length ap) + 
              3 * length gs \<and> bp = mv_boxes 0 (pstr + Suc (length gs)) n"
apply(simp add: rec_ci.simps)
apply(rule_tac x = 
  "cn_merge_gs (map rec_ci gs) (max (Suc n) (Max (insert ba 
      (((\<lambda>(aprog, p, n). n) o rec_ci) ` set gs))))" in exI,
      simp add: cn_merge_gs_len)
apply(rule_tac x = 
  "mv_boxes (max (Suc n) (Max (insert ba (((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs))))
   0 (length gs) [+] a [+]mv_box aa (max (Suc n) 
   (Max (insert ba (((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs)))) [+]
   empty_boxes (length gs) [+] mv_box (max (Suc n) 
  (Max (insert ba (((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs)))) n [+]
   mv_boxes (Suc (max (Suc n) (Max (insert ba (((\<lambda>(aprog, p, n). n) \<circ> rec_ci) 
   ` set gs))) + length gs)) 0 n" in exI, auto)
apply(simp add: abc_append_commute)
done

lemma save_paras: 
  "\<lbrakk>rec_ci (Cn n f gs) = (aprog, rs_pos, a_md);
    rs_pos = n;
    \<forall>k<length gs. rec_calc_rel (gs ! k) lm (ys ! k);
    length ys = length gs;
    length lm = n;
    rec_ci f = (a, aa, ba);
    pstr = Max (set (Suc n # ba # map (\<lambda>(aprog, p, n). n)
                                          (map rec_ci (gs))))\<rbrakk>
  \<Longrightarrow> \<exists>stp. abc_steps_l ((\<Sum>(ap, pos, n)\<leftarrow>map rec_ci gs. length ap) +
          3 * length gs, lm @ 0\<up>(pstr - n) @ ys @
                 0\<up>(a_md - pstr - length ys) @ suf_lm) aprog stp = 
           ((\<Sum>(ap, pos, n)\<leftarrow>map rec_ci gs. length ap) +
                      3 * length gs + 3 * n, 
             0\<up>pstr @ ys @ 0 # lm @ 0\<up>(a_md - Suc (pstr + length ys + n)) @ suf_lm)"
proof -
  assume h:
    "rec_ci (Cn n f gs) = (aprog, rs_pos, a_md)"
    "rs_pos = n" 
    "\<forall>k<length gs. rec_calc_rel (gs ! k) lm (ys ! k)" 
    "length ys = length gs"  
    "length lm = n"    
    "rec_ci f = (a, aa, ba)"
    and g: "pstr = Max (set (Suc n # ba # map (\<lambda>(aprog, p, n). n) 
                                        (map rec_ci (gs))))"
  from h and g have k1: 
    "\<exists> ap bp cp. aprog = ap [+] bp [+] cp \<and> 
    length ap = (\<Sum>(ap, pos, n)\<leftarrow>map rec_ci gs. length ap) + 
                3 *length gs \<and> bp = mv_boxes 0 (pstr + Suc (length ys)) n"
    apply(drule_tac save_paras_prog_ex, auto)
    done
  from h have k2: 
    "\<exists> stp. abc_steps_l (0, lm @ 0\<up>(pstr - n) @ ys @ 
                         0\<up>(a_md - pstr - length ys) @ suf_lm)
         (mv_boxes 0 (pstr + Suc (length ys)) n) stp = 
        (3 * n, 0\<up>pstr @ ys @ 0 # lm @ 0\<up>(a_md - Suc (pstr + length ys + n)) @ suf_lm)"
    apply(rule_tac save_paras', simp, simp_all add: g)
    apply(drule_tac a = a and aa = aa and ba = ba in 
                                        ci_cn_md_def, simp, simp)
    done
  from k1 show 
    "\<exists>stp. abc_steps_l ((\<Sum>(ap, pos, n)\<leftarrow>map rec_ci gs. length ap) + 
         3 * length gs, lm @ 0\<up>(pstr - n) @ ys @ 
                 0\<up>(a_md - pstr - length ys) @ suf_lm) aprog stp =
             ((\<Sum>(ap, pos, n)\<leftarrow>map rec_ci gs. length ap) + 
               3 * length gs + 3 * n, 
                0\<up> pstr @ ys @ 0 # lm @ 0\<up>(a_md - Suc (pstr + length ys + n)) @ suf_lm)"
  proof(erule_tac exE, erule_tac exE, erule_tac exE, erule_tac exE)
    fix ap bp apa cp
    assume "aprog = ap [+] bp [+] cp \<and> length ap = 
            (\<Sum>(ap, pos, n)\<leftarrow>map rec_ci gs. length ap) + 3 * length gs
            \<and> bp = mv_boxes 0 (pstr + Suc (length ys)) n"
    from this and k2 show "?thesis"
      apply(simp)
      apply(rule_tac abc_append_exc1, simp, simp, simp)
      done
  qed
qed
 
lemma ci_cn_para_eq:
  "rec_ci (Cn n f gs) = (aprog, rs_pos, a_md) \<Longrightarrow> rs_pos = n"
apply(simp add: rec_ci.simps, case_tac "rec_ci f", simp)
done

lemma calc_gs_prog_ex: 
  "\<lbrakk>rec_ci (Cn n f gs) = (aprog, rs_pos, a_md); 
    rec_ci f = (a, aa, ba);
    Max (set (Suc n # ba # map (\<lambda>(aprog, p, n). n) 
                         (map rec_ci (gs)))) = pstr\<rbrakk>
   \<Longrightarrow> \<exists>ap bp. aprog = ap [+] bp \<and> 
                 ap = cn_merge_gs (map rec_ci gs) pstr"
apply(simp add: rec_ci.simps)
apply(rule_tac x = "mv_boxes 0 (Suc (max (Suc n)  
   (Max (insert ba (((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs))) + length gs)) n [+]
   mv_boxes (max (Suc n) (Max (insert ba 
  (((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs)))) 0 (length gs) [+]
   a [+] mv_box aa (max (Suc n)
    (Max (insert ba (((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs)))) [+]
   empty_boxes (length gs) [+] mv_box (max (Suc n)
    (Max (insert ba (((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs)))) n [+]
    mv_boxes (Suc (max (Suc n) (Max 
    (insert ba (((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs))) + length gs)) 0 n"
   in exI)
apply(auto simp: abc_append_commute)
done

lemma cn_calc_gs: 
  assumes ind: 
  "\<And>x aprog a_md rs_pos rs suf_lm lm.
  \<lbrakk>x \<in> set gs; 
   rec_ci x = (aprog, rs_pos, a_md); 
   rec_calc_rel x lm rs\<rbrakk>
  \<Longrightarrow> \<exists>stp. abc_steps_l (0, lm @ 0\<up>(a_md - rs_pos) @ suf_lm) aprog stp = 
     (length aprog, lm @ [rs] @ 0\<up>(a_md - rs_pos - 1) @ suf_lm)"
  and h:  "rec_ci (Cn n f gs) = (aprog, rs_pos, a_md)"  
          "\<forall>k<length gs. rec_calc_rel (gs ! k) lm (ys ! k)"
          "length ys = length gs" 
          "length lm = n" 
          "rec_ci f = (a, aa, ba)" 
          "Max (set (Suc n # ba # map (\<lambda>(aprog, p, n). n) 
                               (map rec_ci (gs)))) = pstr"
  shows  
  "\<exists>stp. abc_steps_l (0, lm @ 0\<up>(a_md - rs_pos) @ suf_lm) aprog stp =
  ((\<Sum>(ap, pos, n)\<leftarrow>map rec_ci gs. length ap) + 3 * length gs, 
   lm @ 0\<up>(pstr - n) @ ys @ 0\<up>(a_md -pstr - length ys) @ suf_lm) "
proof -
  from h have k1:
    "\<exists> ap bp. aprog = ap [+] bp \<and> ap = 
                        cn_merge_gs (map rec_ci gs) pstr"
    by(erule_tac calc_gs_prog_ex, auto)
  from h have j1: "rs_pos = n"
    by(simp add: ci_cn_para_eq)
  from h have j2: "a_md \<ge> pstr"
    by(drule_tac a = a and aa = aa and ba = ba in 
                                ci_cn_md_def, simp, simp)
  from h have j3: "pstr > n"
    by(auto)    
  from j1 and j2 and j3 and h have k2:
    "\<exists>stp. abc_steps_l (0, lm @ 0\<up>(a_md - rs_pos) @ suf_lm) 
                         (cn_merge_gs (map rec_ci gs) pstr) stp 
    = ((\<Sum>(ap, pos, n)\<leftarrow>map rec_ci gs. length ap) + 3 * length gs, 
                  lm @ 0\<up>(pstr - n) @ ys @ 0\<up>(a_md - pstr - length ys) @ suf_lm)"
    apply(simp)
    apply(rule_tac cn_merge_gs_ex, rule_tac ind, simp, simp, auto)
    apply(drule_tac a = a and aa = aa and ba = ba in 
                                 ci_cn_md_def, simp, simp)
    apply(rule min_max.le_supI2, auto)
    done
  from k1 show "?thesis"
  proof(erule_tac exE, erule_tac exE, simp)
    fix ap bp
    from k2 show 
      "\<exists>stp. abc_steps_l (0, lm @ 0\<up>(a_md - rs_pos) @ suf_lm)
           (cn_merge_gs (map rec_ci gs) pstr [+] bp) stp =
      (listsum (map ((\<lambda>(ap, pos, n). length ap) \<circ> rec_ci) gs) +
         3 * length gs, 
         lm @ 0\<up>(pstr - n) @ ys @ 0\<up>(a_md - (pstr + length ys)) @ suf_lm)"
      apply(insert abc_append_exc1[of 
        "lm @ 0\<up>(a_md - rs_pos) @ suf_lm" 
        "(cn_merge_gs (map rec_ci gs) pstr)" 
        "length (cn_merge_gs (map rec_ci gs) pstr)" 
        "lm @ 0\<up>(pstr - n) @ ys @ 0\<up>(a_md - pstr - length ys) @ suf_lm" 0 
        "[]" bp], simp add: cn_merge_gs_len)
      done      
  qed
qed

lemma reset_new_paras': 
  "\<lbrakk>length lm = n; 
    pstr > 0; 
    a_md \<ge> pstr + length ys + n;
     pstr > length ys\<rbrakk> \<Longrightarrow>
   \<exists>stp. abc_steps_l (0, 0\<up>pstr @ ys @ 0 # lm @  0\<up>(a_md - Suc (pstr + length ys + n)) @
          suf_lm) (mv_boxes pstr 0 (length ys)) stp =
  (3 * length ys, ys @ 0\<up>pstr @ 0 # lm @ 0\<up>(a_md - Suc (pstr + length ys + n)) @ suf_lm)"
apply(insert mv_boxes_ex2[of "length ys" "pstr" 0 "[]"
     "0\<up>(pstr - length ys)" "ys" 
     "0 # lm @ 0\<up>(a_md - Suc (pstr + length ys + n)) @ suf_lm"], 
     simp add: exponent_add_iff)
done

lemma [simp]:  
  "\<lbrakk>rec_ci (Cn n f gs) = (aprog, rs_pos, a_md);
  rec_calc_rel f ys rs; rec_ci f = (a, aa, ba);
  pstr = Max (set (Suc n # ba # map (\<lambda>(aprog, p, n). n) 
               (map rec_ci (gs))))\<rbrakk>
  \<Longrightarrow> length ys < pstr"
apply(subgoal_tac "length ys = aa", simp)
apply(subgoal_tac "aa < ba \<and> ba \<le> pstr", 
      rule basic_trans_rules(22), auto)
apply(rule min_max.le_supI2)
apply(auto)
apply(erule_tac para_pattern, simp)
done

lemma reset_new_paras_prog_ex: 
  "\<lbrakk>rec_ci (Cn n f gs) = (aprog, rs_pos, a_md); 
   rec_ci f = (a, aa, ba);
   Max (set (Suc n # ba # map (\<lambda>(aprog, p, n). n) 
  (map rec_ci (gs)))) = pstr\<rbrakk>
  \<Longrightarrow> \<exists> ap bp cp. aprog = ap [+] bp [+] cp \<and> 
  length ap = (\<Sum>(ap, pos, n)\<leftarrow>map rec_ci gs. length ap) +
           3 *length gs + 3 * n \<and> bp = mv_boxes pstr 0 (length gs)"
apply(simp add: rec_ci.simps)
apply(rule_tac x = "cn_merge_gs (map rec_ci gs) (max (Suc n) 
          (Max (insert ba (((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs)))) [+] 
          mv_boxes 0 (Suc (max (Suc n) (Max (insert ba 
           (((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs))) + length gs)) n" in exI, 
       simp add: cn_merge_gs_len)
apply(rule_tac x = "a [+]
     mv_box aa (max (Suc n) (Max (insert ba 
     (((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs)))) [+]
     empty_boxes (length gs) [+] mv_box 
     (max (Suc n) (Max (insert ba (((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs)))) n
      [+] mv_boxes (Suc (max (Suc n) (Max (insert ba 
     (((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs))) + length gs)) 0 n" in exI,
       auto simp: abc_append_commute)
done

lemma reset_new_paras:
       "\<lbrakk>rec_ci (Cn n f gs) = (aprog, rs_pos, a_md);
        rs_pos = n;
        \<forall>k<length gs. rec_calc_rel (gs ! k) lm (ys ! k);
        length ys = length gs;
        length lm = n;
        length ys = aa;
        rec_ci f = (a, aa, ba);
        pstr = Max (set (Suc n # ba # map (\<lambda>(aprog, p, n). n)
                                    (map rec_ci (gs))))\<rbrakk>
\<Longrightarrow> \<exists>stp. abc_steps_l ((\<Sum>(ap, pos, n)\<leftarrow>map rec_ci gs. length ap) + 
                                               3 * length gs + 3 * n,
        0\<up>pstr @ ys @ 0 # lm @ 0\<up>(a_md - Suc (pstr + length ys + n)) @ suf_lm) aprog stp =
  ((\<Sum>(ap, pos, n)\<leftarrow>map rec_ci gs. length ap) + 6 * length gs + 3 * n,
           ys @ 0\<up>pstr @ 0 # lm @ 0\<up>(a_md - Suc (pstr + length ys + n)) @ suf_lm)"
proof -
  assume h:
    "rec_ci (Cn n f gs) = (aprog, rs_pos, a_md)"
    "rs_pos = n" 
    "length ys = aa"
    "\<forall>k<length gs. rec_calc_rel (gs ! k) lm (ys ! k)"
    "length ys = length gs"  "length lm = n"    
    "rec_ci f = (a, aa, ba)"
    and g: "pstr = Max (set (Suc n # ba # map (\<lambda>(aprog, p, n). n)
                                         (map rec_ci (gs))))"
  from h and g have k1:
    "\<exists> ap bp cp. aprog = ap [+] bp [+] cp \<and> length ap = 
    (\<Sum>(ap, pos, n)\<leftarrow>map rec_ci gs. length ap) +
          3 *length gs + 3 * n \<and> bp = mv_boxes pstr 0 (length ys)"
    by(drule_tac reset_new_paras_prog_ex, auto)
  from h have k2:
    "\<exists> stp. abc_steps_l (0, 0\<up>pstr @ ys @ 0 # lm @ 0\<up>(a_md - Suc (pstr + length ys + n)) @
              suf_lm) (mv_boxes pstr 0 (length ys)) stp = 
    (3 * (length ys), 
     ys @ 0\<up>pstr @ 0 # lm @ 0\<up>(a_md - Suc (pstr + length ys + n)) @ suf_lm)"
    apply(rule_tac reset_new_paras', simp)
    apply(simp add: g)
    apply(drule_tac a = a and aa = aa and ba = ba in ci_cn_md_def,
      simp, simp add: g, simp)
    apply(subgoal_tac "length gs = aa \<and> aa < ba \<and> ba \<le> pstr", arith,
          simp add: para_pattern)
    apply(insert g, auto intro: min_max.le_supI2)
    done
  from k1 show 
    "\<exists>stp. abc_steps_l ((\<Sum>(ap, pos, n)\<leftarrow>map rec_ci gs. length ap) + 3
    * length gs + 3 * n, 0\<up>pstr @ ys @ 0 # lm @ 0\<up>(a_md - Suc (pstr + length ys + n)) @ 
     suf_lm) aprog stp =
    ((\<Sum>(ap, pos, n)\<leftarrow>map rec_ci gs. length ap) + 6 * length gs +
      3 * n, ys @ 0\<up>pstr @ 0 # lm @ 0\<up>(a_md - Suc (pstr + length ys + n)) @ suf_lm)"
  proof(erule_tac exE, erule_tac exE, erule_tac exE, erule_tac exE)
    fix ap bp apa cp
    assume "aprog = ap [+] bp [+] cp \<and> length ap = 
      (\<Sum>(ap, pos, n)\<leftarrow>map rec_ci gs. length ap) + 3 * length gs +
                  3 * n \<and> bp = mv_boxes pstr 0 (length ys)"
    from this and k2 show "?thesis"
      apply(simp)
      apply(drule_tac as = 
        "(\<Sum>(ap, pos, n)\<leftarrow>map rec_ci gs. length ap) + 3 * length gs +
        3 * n" and ap = ap and cp = cp in abc_append_exc1, auto)
      apply(rule_tac x = stp in exI, simp add: h)
      using h
      apply(simp)
      done
  qed
qed

lemma calc_f_prog_ex: 
  "\<lbrakk>rec_ci (Cn n f gs) = (aprog, rs_pos, a_md);
    rec_ci f = (a, aa, ba);
    Max (set (Suc n # ba # map (\<lambda>(aprog, p, n). n) 
                   (map rec_ci (gs)))) = pstr\<rbrakk>
   \<Longrightarrow> \<exists> ap bp cp. aprog = ap [+] bp [+] cp \<and>
  length ap = (\<Sum>(ap, pos, n)\<leftarrow>map rec_ci gs. length ap) +
                                6 *length gs + 3 * n \<and> bp = a"
apply(simp add: rec_ci.simps)
apply(rule_tac x = "cn_merge_gs (map rec_ci gs) (max (Suc n) (Max (insert ba
     (((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs)))) [+] 
     mv_boxes 0 (Suc (max (Suc n) (Max (insert ba 
            (((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs))) + length gs)) n [+]
     mv_boxes (max (Suc n) (Max (insert ba 
      (((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs)))) 0 (length gs)" in exI,
     simp add: cn_merge_gs_len)
apply(rule_tac x = "mv_box aa (max (Suc n) (Max (insert ba 
     (((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs)))) [+]
     empty_boxes (length gs) [+] mv_box (max (Suc n) (
     Max (insert ba (((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs)))) n [+]
     mv_boxes (Suc (max (Suc n) (Max (insert ba 
     (((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs))) + length gs)) 0 n" in exI,
  auto simp: abc_append_commute)
done

lemma calc_cn_f:
  assumes ind: 
  "\<And>x ap fp arity r anything args.
    \<lbrakk>x = map rec_ci gs; rec_ci f = (ap, arity, fp); rec_calc_rel f args r\<rbrakk>
    \<Longrightarrow> \<exists>stp. abc_steps_l (0, args @ 0 \<up> (fp - arity) @ anything) ap stp =
    (length ap, args @ [r] @ 0 \<up> (fp - arity - 1) @ anything)"  
  and h: "rec_ci (Cn n f gs) = (aprog, rs_pos, a_md)"
  "rec_calc_rel (Cn n f gs) lm rs"
  "length ys = length gs"
  "rec_calc_rel f ys rs"
  "length lm = n"
  "rec_ci f = (a, aa, ba)" 
  and p: "pstr = Max (set (Suc n # ba # map (\<lambda>(aprog, p, n). n)
                                (map rec_ci (gs))))"
  shows "\<exists>stp. abc_steps_l   
  ((\<Sum>(ap, pos, n)\<leftarrow>map rec_ci gs. length ap) + 6 * length gs + 3 * n,
  ys @ 0\<up>pstr @ 0 # lm @ 0\<up>(a_md - Suc (pstr + length ys + n)) @ suf_lm) aprog stp =
  ((\<Sum>(ap, pos, n)\<leftarrow>map rec_ci gs. length ap) + 6 * length gs + 
                3 * n + length a,
  ys @ rs # 0\<up>pstr @ lm @ 0\<up>(a_md - Suc (pstr + length ys + n)) @ suf_lm)"
proof -
  from h have k1: 
    "\<exists> ap bp cp. aprog = ap [+] bp [+] cp \<and> 
    length ap = (\<Sum>(ap, pos, n)\<leftarrow>map rec_ci gs. length ap) + 
    6 *length gs + 3 * n \<and> bp = a"
    by(drule_tac calc_f_prog_ex, auto)
  from h and k1 show "?thesis"
  proof (erule_tac exE, erule_tac exE, erule_tac exE, erule_tac exE)
    fix ap bp apa cp
    assume
      "aprog = ap [+] bp [+] cp \<and> 
      length ap = (\<Sum>(ap, pos, n)\<leftarrow>map rec_ci gs. length ap) + 
      6 * length gs + 3 * n \<and> bp = a"
    from h and this show "?thesis"
      apply(simp, rule_tac abc_append_exc1, simp_all)
      thm ind
      apply(insert ind[of "map rec_ci gs" a aa ba ys rs 
        "0\<up>(pstr - ba + length gs) @ 0 # lm @ 
        0\<up>(a_md - Suc (pstr + length gs + n)) @ suf_lm"], simp)
      apply(subgoal_tac "ba > aa \<and> aa = length gs\<and> pstr \<ge> ba", simp)
      apply(simp add: exponent_add_iff)
      apply(case_tac pstr, simp add: p)
      apply(simp only: exp_suc, simp)
      apply(rule conjI, rule ci_ad_ge_paras, simp, rule conjI)
      apply(subgoal_tac "length ys = aa", simp,
        rule para_pattern, simp, simp)
      apply(insert p, simp)
      apply(auto intro: min_max.le_supI2)
      done
  qed
qed

lemma [simp]: 
  "\<lbrakk>pstr + length ys + n \<le> a_md; ys \<noteq> []\<rbrakk> \<Longrightarrow> 
                          pstr < a_md + length suf_lm"
apply(case_tac "length ys", simp)
apply(arith)
done

lemma [simp]: 
  "pstr > length ys 
  \<Longrightarrow> (ys @ rs # 0\<up>pstr @ lm @
  0\<up>(a_md - Suc (pstr + length ys + n)) @ suf_lm) ! pstr = (0::nat)"
apply(simp add: nth_append)
done

(*
lemma [simp]: "\<lbrakk>length ys < pstr; pstr - length ys = Suc x\<rbrakk>
  \<Longrightarrow> pstr - Suc (length ys) = x"
by arith
*)

lemma [simp]: "pstr > length ys \<Longrightarrow> 
      (ys @ rs # 0\<up>pstr @ lm @ 0\<up>(a_md - Suc (pstr + length ys + n)) @ suf_lm)
                                         [pstr := rs, length ys := 0] =
       ys @ 0\<up>(pstr - length ys) @ (rs::nat) # 0\<up>length ys @ lm @ 0\<up>(a_md - Suc (pstr + length ys + n)) @ suf_lm"
apply(auto simp: list_update_append)
apply(case_tac "pstr - length ys",simp_all)
using list_update_length[of 
  "0\<up>(pstr - Suc (length ys))" "0" "0\<up>length ys @ lm @ 
  0\<up>(a_md - Suc (pstr + length ys + n)) @ suf_lm" rs]
apply(simp only: exponent_cons_iff exponent_add_iff, simp)
apply(subgoal_tac "pstr - Suc (length ys) = nat", simp, simp)
done

lemma save_rs': 
  "\<lbrakk>pstr > length ys\<rbrakk>
  \<Longrightarrow> \<exists>stp. abc_steps_l (0, ys @ rs # 0\<up>pstr @ lm @ 
  0\<up>(a_md - Suc (pstr + length ys + n)) @ suf_lm) 
  (mv_box (length ys) pstr) stp =
  (3, ys @ 0\<up>(pstr - (length ys)) @ rs # 
  0\<up>length ys  @ lm @ 0\<up>(a_md - Suc (pstr + length ys + n)) @ suf_lm)"
apply(insert mv_box_ex[of "length ys" pstr 
  "ys @ rs # 0\<up>pstr @ lm @ 0\<up>(a_md - Suc(pstr + length ys + n)) @ suf_lm"], 
  simp)
done


lemma save_rs_prog_ex:
  "\<lbrakk>rec_ci (Cn n f gs) = (aprog, rs_pos, a_md);
  rec_ci f = (a, aa, ba);
  Max (set (Suc n # ba # map (\<lambda>(aprog, p, n). n) 
                        (map rec_ci (gs)))) = pstr\<rbrakk>
  \<Longrightarrow> \<exists> ap bp cp. aprog = ap [+] bp [+] cp \<and>
  length ap = (\<Sum>(ap, pos, n)\<leftarrow>map rec_ci gs. length ap) +
              6 *length gs + 3 * n + length a
  \<and> bp = mv_box aa pstr"
apply(simp add: rec_ci.simps)
apply(rule_tac x =
  "cn_merge_gs (map rec_ci gs) (max (Suc n) (Max (insert ba 
   (((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs))))
   [+] mv_boxes 0 (Suc (max (Suc n) (Max (insert ba 
   (((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs))) + length gs)) n [+]
   mv_boxes (max (Suc n) (Max (insert ba (((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs))))
    0 (length gs) [+] a" 
  in exI, simp add: cn_merge_gs_len)
apply(rule_tac x = 
  "empty_boxes (length gs) [+]
   mv_box (max (Suc n) (Max (insert ba 
    (((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs)))) n [+]
   mv_boxes (Suc (max (Suc n) (Max (insert ba (((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs)))
    + length gs)) 0 n" in exI, 
  auto simp: abc_append_commute)
done

lemma save_rs:  
  assumes h: 
  "rec_ci (Cn n f gs) = (aprog, rs_pos, a_md)" 
  "rec_calc_rel (Cn n f gs) lm rs"
  "\<forall>k<length gs. rec_calc_rel (gs ! k) lm (ys ! k)"
  "length ys = length gs" 
  "rec_calc_rel f ys rs" 
  "rec_ci f = (a, aa, ba)"  
  "length lm = n"
  and pdef: "pstr = Max (set (Suc n # ba # map (\<lambda>(aprog, p, n). n) 
                                            (map rec_ci (gs))))"
  shows "\<exists>stp. abc_steps_l
           ((\<Sum>(ap, pos, n)\<leftarrow>map rec_ci gs. length ap) + 6 * length gs
          + 3 * n + length a, ys @ rs # 0\<up>pstr @ lm @
             0\<up>(a_md - Suc (pstr + length ys + n)) @ suf_lm) aprog stp =
  ((\<Sum>(ap, pos, n)\<leftarrow>map rec_ci gs. length ap) + 6 * length gs 
  + 3 * n + length a + 3,
  ys @ 0\<up>(pstr - length ys) @ rs # 0\<up>length ys @ lm @ 
                               0\<up>(a_md - Suc (pstr + length ys + n)) @ suf_lm)"
proof -
  from h and pdef have k1: 
    "\<exists> ap bp cp. aprog = ap [+] bp [+] cp \<and>
    length ap = (\<Sum>(ap, pos, n)\<leftarrow>map rec_ci gs. length ap) +
    6 *length gs + 3 * n + length a \<and> bp = mv_box (length ys) pstr "
    apply(subgoal_tac "length ys = aa")
    apply(drule_tac a = a and aa = aa and ba = ba in save_rs_prog_ex, 
      simp, simp, simp)
    by(rule_tac para_pattern, simp, simp)
  from k1 show 
    "\<exists>stp. abc_steps_l
    ((\<Sum>(ap, pos, n)\<leftarrow>map rec_ci gs. length ap) + 6 * length gs + 3 * n
    + length a, ys @ rs # 0\<up>pstr @ lm @ 0\<up>(a_md - Suc (pstr + length ys + n)) 
    @ suf_lm) aprog stp =
    ((\<Sum>(ap, pos, n)\<leftarrow>map rec_ci gs. length ap) + 6 * length gs + 3 * n
    + length a + 3, ys @ 0\<up>(pstr - length ys) @ rs # 
    0\<up>length ys @ lm @ 0\<up>(a_md - Suc (pstr + length ys + n)) @ suf_lm)"
  proof (erule_tac exE, erule_tac exE, erule_tac exE, erule_tac exE)
    fix ap bp apa cp
    assume "aprog = ap [+] bp [+] cp \<and> length ap = 
      (\<Sum>(ap, pos, n)\<leftarrow>map rec_ci gs. length ap) + 6 * length gs + 
      3 * n + length a \<and> bp = mv_box (length ys) pstr"
    thus"?thesis"
      apply(simp, rule_tac abc_append_exc1, simp_all)
      apply(rule_tac save_rs', insert h)
      apply(subgoal_tac "length gs = aa \<and> pstr \<ge> ba \<and> ba > aa",
            arith)
      apply(simp add: para_pattern, insert pdef, auto)
      apply(rule_tac min_max.le_supI2, simp)
      done
  qed
qed

lemma [simp]: "length (empty_boxes n) = 2*n"
apply(induct n, simp, simp)
done

lemma mv_box_step_ex: "length lm = n \<Longrightarrow> 
      \<exists>stp. abc_steps_l (0, lm @ Suc x # suf_lm) [Dec n 2, Goto 0] stp
  = (0, lm @ x # suf_lm)"
apply(rule_tac x = "Suc (Suc 0)" in exI, 
  simp add: abc_steps_l.simps abc_step_l.simps abc_fetch.simps 
         abc_lm_v.simps abc_lm_s.simps nth_append list_update_append)
done

lemma mv_box_ex': 
  "\<lbrakk>length lm = n\<rbrakk> \<Longrightarrow> 
  \<exists> stp. abc_steps_l (0, lm @ x # suf_lm) [Dec n 2, Goto 0] stp =
  (Suc (Suc 0), lm @ 0 # suf_lm)"
apply(induct x)
apply(rule_tac x = "Suc 0" in exI, 
  simp add: abc_steps_l.simps abc_fetch.simps abc_step_l.simps
            abc_lm_v.simps nth_append abc_lm_s.simps, simp)
apply(drule_tac x = x and suf_lm = suf_lm in mv_box_step_ex, 
      erule_tac exE, erule_tac exE)
apply(rule_tac x = "stpa + stp" in exI, simp add: abc_steps_add)
done

lemma [simp]: "drop n lm = a # list \<Longrightarrow> list = drop (Suc n) lm"
apply(induct n arbitrary: lm a list, simp)
apply(case_tac "lm", simp, simp)
done

lemma empty_boxes_ex: "\<lbrakk>length lm \<ge> n\<rbrakk>
     \<Longrightarrow> \<exists>stp. abc_steps_l (0, lm) (empty_boxes n) stp = 
                                          (2*n, 0\<up>n @ drop n lm)"
apply(induct n, simp, simp)
apply(rule_tac abc_append_exc2, auto)
apply(case_tac "drop n lm", simp, simp)
proof -
  fix n stp a list
  assume h: "Suc n \<le> length lm"  "drop n lm = a # list"
  thus "\<exists>bstp. abc_steps_l (0, 0\<up>n @ a # list) [Dec n 2, Goto 0] bstp =
                       (Suc (Suc 0), 0 # 0\<up>n @ drop (Suc n) lm)"
    apply(insert mv_box_ex'[of "0\<up>n" n a list], simp, erule_tac exE)
    apply(rule_tac x = stp in exI, simp, simp only: exponent_cons_iff)
    apply(simp add:exp_ind del: replicate.simps)
    done
qed


lemma mv_box_paras_prog_ex:
  "\<lbrakk>rec_ci (Cn n f gs) = (aprog, rs_pos, a_md);
  rec_ci f = (a, aa, ba); 
  Max (set (Suc n # ba # map (\<lambda>(aprog, p, n). n) 
                    (map rec_ci (gs)))) = pstr\<rbrakk>
  \<Longrightarrow> \<exists> ap bp cp. aprog = ap [+] bp [+] cp \<and> 
  length ap = (\<Sum>(ap, pos, n)\<leftarrow>map rec_ci gs. length ap) + 
  6 *length gs + 3 * n + length a + 3 \<and> bp = empty_boxes (length gs)"
apply(simp add: rec_ci.simps)
apply(rule_tac x = "cn_merge_gs (map rec_ci gs) (max (Suc n) 
    (Max (insert ba (((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs)))) [+] 
    mv_boxes 0 (Suc (max (Suc n) (Max 
     (insert ba (((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs))) + length gs)) n
    [+] mv_boxes (max (Suc n) (Max (insert ba 
    (((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs)))) 0 (length gs) [+]
     a [+] mv_box aa (max (Suc n) 
   (Max (insert ba (((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs))))" 
    in exI, simp add: cn_merge_gs_len)
apply(rule_tac x = " mv_box (max (Suc n) (Max (insert ba
     (((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs)))) n [+]
     mv_boxes (Suc (max (Suc n) (Max (insert ba 
     (((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs))) + length gs)) 0 n" in exI, 
  auto simp: abc_append_commute)
done

lemma mv_box_paras: 
 assumes h: 
  "rec_ci (Cn n f gs) = (aprog, rs_pos, a_md)" 
  "rec_calc_rel (Cn n f gs) lm rs" 
  "\<forall>k<length gs. rec_calc_rel (gs ! k) lm (ys ! k)"
  "length ys = length gs" 
  "rec_calc_rel f ys rs" 
  "rec_ci f = (a, aa, ba)" 
  and pdef: "pstr = Max (set (Suc n # ba # map (\<lambda>(aprog, p, n). n) 
                                             (map rec_ci (gs))))"
  and starts: "ss = (\<Sum>(ap, pos, n)\<leftarrow>map rec_ci gs. length ap) +
                              6 * length gs + 3 * n + length a + 3"
  shows "\<exists>stp. abc_steps_l
           (ss, ys @ 0\<up>(pstr - length ys) @ rs # 0\<up>length ys 
               @ lm @ 0\<up>(a_md - Suc (pstr + length ys + n)) @ suf_lm) aprog stp =
   (ss + 2 * length gs, 0\<up>pstr @ rs # 0\<up>length ys  @ lm @ 
                                0\<up>(a_md - Suc (pstr + length ys + n)) @ suf_lm)"
proof -
  from h and pdef and starts have k1: 
    "\<exists> ap bp cp. aprog = ap [+] bp [+] cp \<and>
    length ap = (\<Sum>(ap, pos, n)\<leftarrow>map rec_ci gs. length ap) + 
                               6 *length gs + 3 * n + length a + 3
    \<and> bp = empty_boxes (length ys)"
    by(drule_tac mv_box_paras_prog_ex, auto)
  from h have j1: "aa < ba"
    by(simp add: ci_ad_ge_paras)
  from h have j2: "length gs = aa"
    by(drule_tac f = f in para_pattern, simp, simp)
  from h and pdef have j3: "ba \<le> pstr"
    apply simp 
    apply(rule_tac min_max.le_supI2, simp)
    done
  from k1 show "?thesis"
  proof (erule_tac exE, erule_tac exE, erule_tac exE, erule_tac exE)
    fix ap bp apa cp
    assume "aprog = ap [+] bp [+] cp \<and> 
      length ap = (\<Sum>(ap, pos, n)\<leftarrow>map rec_ci gs. length ap) +
      6 * length gs + 3 * n + length a + 3 \<and> 
      bp = empty_boxes (length ys)"
    thus"?thesis"
      apply(simp, rule_tac abc_append_exc1, simp_all add: starts h)
      apply(insert empty_boxes_ex[of 
        "length gs" "ys @ 0\<up>(pstr - (length gs)) @ rs #
        0\<up>length gs @ lm @ 0\<up>(a_md - Suc (pstr + length gs + n)) @ suf_lm"], 
        simp add: h)
      apply(erule_tac exE, rule_tac x = stp in exI, 
        simp add: replicate.simps[THEN sym]
        replicate_add[THEN sym] del: replicate.simps)
      apply(subgoal_tac "pstr >(length gs)", simp)
      apply(subgoal_tac "ba > aa \<and> length gs = aa \<and> pstr \<ge> ba", simp)
      apply(simp add: j1 j2 j3)
      done     
  qed
qed

lemma restore_rs_prog_ex:
  "\<lbrakk>rec_ci (Cn n f gs) = (aprog, rs_pos, a_md);
  rec_ci f = (a, aa, ba);
  Max (set (Suc n # ba # map (\<lambda>(aprog, p, n). n)
  (map rec_ci (gs)))) = pstr;
  ss = (\<Sum>(ap, pos, n)\<leftarrow>map rec_ci gs. length ap) +
  8 * length gs + 3 * n + length a + 3\<rbrakk>
  \<Longrightarrow> \<exists> ap bp cp. aprog = ap [+] bp [+] cp \<and> length ap = ss \<and> 
                                           bp = mv_box pstr n"
apply(simp add: rec_ci.simps)
apply(rule_tac x = "cn_merge_gs (map rec_ci gs) (max (Suc n) 
      (Max (insert ba (((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs)))) [+] 
      mv_boxes 0 (Suc (max (Suc n) (Max (insert ba (((\<lambda>(aprog, p, n). n)
        \<circ> rec_ci) ` set gs))) + length gs)) n [+]
     mv_boxes (max (Suc n) (Max (insert ba 
      (((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs)))) 0 (length gs) [+]
     a [+] mv_box aa (max (Suc n)
       (Max (insert ba (((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs)))) [+]
     empty_boxes (length gs)" in exI, simp add: cn_merge_gs_len)
apply(rule_tac x = "mv_boxes (Suc (max (Suc n) 
       (Max (insert ba (((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs))) 
        + length gs)) 0 n" 
  in exI, auto simp: abc_append_commute)
done

lemma exp_add: "a\<up>(b+c) = a\<up>b @ a\<up>c"
apply(simp add:replicate_add)
done

lemma [simp]: "n < pstr \<Longrightarrow> (0\<up>pstr)[n := rs] @ [0::nat] = 0\<up>n @ rs # 0\<up>(pstr - n)"
using list_update_length[of "0\<up>n" "0::nat" "0\<up>(pstr - Suc n)" rs]
apply(simp add: replicate_Suc[THEN sym] exp_add[THEN sym] exp_suc[THEN sym])
done

lemma restore_rs:
  assumes h: "rec_ci (Cn n f gs) = (aprog, rs_pos, a_md)" 
  "rec_calc_rel (Cn n f gs) lm rs" 
  "\<forall>k<length gs. rec_calc_rel (gs ! k) lm (ys ! k)"
  "length ys = length gs"
  "rec_calc_rel f ys rs" 
  "rec_ci f = (a, aa, ba)" 
  and pdef: "pstr = Max (set (Suc n # ba # map (\<lambda>(aprog, p, n). n)
                                        (map rec_ci (gs))))"
  and starts: "ss = (\<Sum>(ap, pos, n)\<leftarrow>map rec_ci gs. length ap) + 
                              8 * length gs + 3 * n + length a + 3" 
  shows "\<exists>stp. abc_steps_l
           (ss, 0\<up>pstr @ rs # 0\<up>length ys  @ lm @
                    0\<up>(a_md - Suc (pstr + length ys + n)) @ suf_lm) aprog stp =
  (ss + 3, 0\<up>n @ rs # 0\<up>(pstr - n) @ 0\<up>length ys  @ lm @ 
                                   0\<up>(a_md - Suc (pstr + length ys + n)) @ suf_lm)"
proof -
 from h and pdef and starts have k1:
   "\<exists> ap bp cp. aprog = ap [+] bp [+] cp \<and> length ap = ss \<and> 
                                            bp = mv_box pstr n"
   by(drule_tac restore_rs_prog_ex, auto)
 from k1 show "?thesis"
 proof (erule_tac exE, erule_tac exE, erule_tac exE, erule_tac exE)
   fix ap bp apa cp
   assume "aprog = ap [+] bp [+] cp \<and> length ap = ss \<and> 
                                 bp = mv_box pstr n"
   thus"?thesis"
     apply(simp, rule_tac abc_append_exc1, simp_all add: starts h)
     apply(insert mv_box_ex[of pstr n "0\<up>pstr @ rs # 0\<up>length gs @
                     lm @ 0\<up>(a_md - Suc (pstr + length gs + n)) @ suf_lm"], simp)
     apply(subgoal_tac "pstr > n", simp)
     apply(erule_tac exE, rule_tac x = stp in exI, 
                         simp add: nth_append list_update_append)
     apply(simp add: pdef)
     done
  qed
qed

lemma [simp]:"xs \<noteq> [] \<Longrightarrow> length xs \<ge> Suc 0"
by(case_tac xs, auto)

lemma  [simp]: "n < max (Suc n) (max ba (Max (((\<lambda>(aprog, p, n). n) o 
                                                  rec_ci) ` set gs)))"
by(simp)

lemma restore_paras_prog_ex: 
  "\<lbrakk>rec_ci (Cn n f gs) = (aprog, rs_pos, a_md); 
  rec_ci f = (a, aa, ba);
  Max (set (Suc n # ba # map (\<lambda>(aprog, p, n). n)
                          (map rec_ci (gs)))) = pstr;
  ss = (\<Sum>(ap, pos, n)\<leftarrow>map rec_ci gs. length ap) +
                         8 * length gs + 3 * n + length a + 6\<rbrakk>
  \<Longrightarrow> \<exists> ap bp cp. aprog = ap [+] bp [+] cp \<and> length ap = ss \<and> 
                      bp = mv_boxes (pstr + Suc (length gs)) (0::nat) n"
apply(simp add: rec_ci.simps)
apply(rule_tac x = "cn_merge_gs (map rec_ci gs) (max (Suc n) 
      (Max (insert ba (((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs))))
      [+] mv_boxes 0 (Suc (max (Suc n) 
       (Max (insert ba (((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs))) 
     + length gs)) n [+] mv_boxes (max (Suc n) 
    (Max (insert ba (((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs)))) 0 (length gs) [+]
     a [+] mv_box aa (max (Suc n) 
      (Max (insert ba (((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs)))) [+]
     empty_boxes (length gs) [+]
     mv_box (max (Suc n) (Max (insert ba 
     (((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs)))) n" in exI, simp add: cn_merge_gs_len)
apply(rule_tac x = "[]" in exI, auto simp: abc_append_commute)
done

lemma restore_paras: 
  assumes h: "rec_ci (Cn n f gs) = (aprog, rs_pos, a_md)" 
  "rec_calc_rel (Cn n f gs) lm rs" 
  "\<forall>k<length gs. rec_calc_rel (gs ! k) lm (ys ! k)"
  "length ys = length gs"
  "rec_calc_rel f ys rs" 
  "rec_ci f = (a, aa, ba)"
  and pdef: 
  "pstr = Max (set (Suc n # ba # map (\<lambda>(aprog, p, n). n) 
                         (map rec_ci (gs))))"
  and starts: "ss = (\<Sum>(ap, pos, n)\<leftarrow>map rec_ci gs. length ap) + 
                              8 * length gs + 3 * n + length a + 6" 
  shows "\<exists>stp. abc_steps_l (ss, 0\<up>n @ rs # 0\<up>(pstr - n+ length ys) @
                         lm @ 0\<up>(a_md - Suc (pstr + length ys + n)) @ suf_lm)
  aprog stp = (ss + 3 * n, lm @ rs # 0\<up>(a_md - Suc n) @ suf_lm)"
proof -
  from h and pdef and starts have k1:
    "\<exists> ap bp cp. aprog = ap [+] bp [+] cp \<and> length ap = ss \<and>
                     bp = mv_boxes (pstr + Suc (length gs)) (0::nat) n"
    by(drule_tac restore_paras_prog_ex, auto)
  from k1 show "?thesis"
  proof (erule_tac exE, erule_tac exE, erule_tac exE, erule_tac exE)
    fix ap bp apa cp
    assume "aprog = ap [+] bp [+] cp \<and> length ap = ss \<and> 
                              bp = mv_boxes (pstr + Suc (length gs)) 0 n"
    thus"?thesis"
      apply(simp, rule_tac abc_append_exc1, simp_all add: starts h)
      apply(insert mv_boxes_ex2[of n "pstr + Suc (length gs)" 0 "[]" 
        "rs # 0\<up>(pstr - n + length gs)" "lm" 
        "0\<up>(a_md - Suc (pstr + length gs + n)) @ suf_lm"], simp)
      apply(subgoal_tac "pstr > n \<and> 
        a_md > pstr + length gs + n \<and> length lm = n" , simp add: exponent_add_iff h)
      using h pdef
      apply(simp)     
      apply(frule_tac a = a and 
        aa = aa and ba = ba in ci_cn_md_def, simp, simp)
      apply(subgoal_tac "length lm = rs_pos",
        simp add: ci_cn_para_eq, erule_tac para_pattern, simp)
      done
  qed
qed

lemma ci_cn_length:
  "\<lbrakk>rec_ci (Cn n f gs) = (aprog, rs_pos, a_md); 
  rec_calc_rel (Cn n f gs) lm rs;
  rec_ci f = (a, aa, ba)\<rbrakk>
  \<Longrightarrow> length aprog = (\<Sum>(ap, pos, n)\<leftarrow>map rec_ci gs. length ap) +
                             8 * length gs + 6 * n + length a + 6"
apply(simp add: rec_ci.simps, auto simp: cn_merge_gs_len)
done

lemma  cn_case: 
  assumes ind1:
  "\<And>x aprog a_md rs_pos rs suf_lm lm.
  \<lbrakk>x \<in> set gs;
  rec_ci x = (aprog, rs_pos, a_md);
  rec_calc_rel x lm rs\<rbrakk>
  \<Longrightarrow> \<exists>stp. abc_steps_l (0, lm @ 0\<up>(a_md - rs_pos) @ suf_lm) aprog stp = 
               (length aprog, lm @ [rs] @ 0\<up>(a_md - rs_pos - 1) @ suf_lm)"
  and ind2: 
  "\<And>x ap fp arity r anything args.
    \<lbrakk>x = map rec_ci gs; rec_ci f = (ap, arity, fp); rec_calc_rel f args r\<rbrakk>
    \<Longrightarrow> \<exists>stp. abc_steps_l (0, args @ 0 \<up> (fp - arity) @ anything) ap stp =
    (length ap, args @ [r] @ 0 \<up> (fp - arity - 1) @ anything)"
  and h: "rec_ci (Cn n f gs) = (aprog, rs_pos, a_md)"
         "rec_calc_rel (Cn n f gs) lm rs"
  shows "\<exists>stp. abc_steps_l (0, lm @ 0\<up>(a_md - rs_pos) @ suf_lm) aprog stp 
  = (length aprog, lm @ [rs] @ 0\<up>(a_md - rs_pos - 1) @ suf_lm)"
apply(insert h, case_tac "rec_ci f",  rule_tac calc_cn_reverse, simp)
proof -
  fix a b c ys
  let ?pstr = "Max (set (Suc n # c # (map (\<lambda>(aprog, p, n). n) 
                                         (map rec_ci (gs)))))"  
  let ?gs_len = "listsum (map (\<lambda> (ap, pos, n). length ap) 
                                                (map rec_ci (gs)))"
  assume g: "rec_ci (Cn n f gs) = (aprog, rs_pos, a_md)"
    "rec_calc_rel (Cn n f gs) lm rs"
    "\<forall>k<length gs. rec_calc_rel (gs ! k) lm (ys ! k)" 
    "length ys = length gs" 
    "rec_calc_rel f ys rs"
    "n = length lm"
    "rec_ci f = (a, b, c)"  
  hence k1:
    "\<exists> stp. abc_steps_l (0, lm @ 0\<up>(a_md - rs_pos) @ suf_lm) aprog stp = 
    (?gs_len + 3 * length gs, lm @ 0\<up>(?pstr - n) @ ys @
                               0\<up>(a_md - ?pstr - length ys) @ suf_lm)"	
    apply(rule_tac a = a and aa = b and ba = c in cn_calc_gs)
    apply(rule_tac ind1, auto)
    done  
  from g have k2: 
    "\<exists> stp. abc_steps_l (?gs_len + 3 * length gs,  lm @ 
        0\<up>(?pstr - n) @ ys @ 0\<up>(a_md - ?pstr - length ys) @ suf_lm) aprog stp = 
    (?gs_len + 3 * length gs + 3 * n, 0\<up>?pstr @ ys @ 0 # lm @ 
                              0\<up>(a_md - Suc (?pstr + length ys + n)) @ suf_lm)"
    apply(erule_tac ba = c in save_paras, auto intro: ci_cn_para_eq)
    done
  from g have k3: 
    "\<exists> stp. abc_steps_l (?gs_len + 3 * length gs + 3 * n,
    0\<up>?pstr @ ys @ 0 # lm @ 0\<up>(a_md - Suc (?pstr + length ys + n)) @ suf_lm) aprog stp =
    (?gs_len + 6 * length gs + 3 * n,  
           ys @ 0\<up>?pstr @ 0 # lm @ 0\<up>(a_md - Suc (?pstr + length ys + n)) @ suf_lm)"
    apply(erule_tac ba = c in reset_new_paras, 
          auto intro: ci_cn_para_eq)
    using para_pattern[of f a b c ys rs]
    apply(simp)
    done
  from g have k4: 
    "\<exists>stp. abc_steps_l  (?gs_len + 6 * length gs + 3 * n,  
    ys @ 0\<up>?pstr @ 0 # lm @ 0\<up>(a_md - Suc (?pstr + length ys + n)) @ suf_lm) aprog stp =
    (?gs_len + 6 * length gs + 3 * n + length a, 
   ys @ rs # 0\<up>?pstr  @ lm @ 0\<up>(a_md - Suc (?pstr + length ys + n)) @ suf_lm)"
    apply(rule_tac ba = c in calc_cn_f, rule_tac ind2, auto)
    done
  from g h have k5:
    "\<exists> stp. abc_steps_l (?gs_len + 6 * length gs + 3 * n + length a,
    ys @ rs # 0\<up>?pstr @ lm @ 0\<up>(a_md - Suc (?pstr + length ys + n)) @ suf_lm)
    aprog stp =
    (?gs_len + 6 * length gs + 3 * n + length a + 3,
    ys @ 0\<up>(?pstr - length ys) @ rs # 0\<up>length ys @ lm @ 
    0\<up>(a_md  - Suc (?pstr + length ys + n)) @ suf_lm)"
    apply(rule_tac save_rs, auto simp: h)
    done
  from g have k6: 
    "\<exists> stp. abc_steps_l (?gs_len + 6 * length gs + 3 * n + 
    length a + 3, ys @ 0\<up>(?pstr - length ys) @ rs # 0\<up>length ys @ lm @ 
    0\<up>(a_md  - Suc (?pstr + length ys + n)) @ suf_lm) 
    aprog stp =
    (?gs_len + 8 * length gs + 3 *n + length a + 3,
    0\<up>?pstr @ rs # 0\<up>length ys @ lm @ 
                        0\<up>(a_md -Suc (?pstr + length ys + n)) @ suf_lm)"
    apply(drule_tac suf_lm = suf_lm in mv_box_paras, auto)
    apply(rule_tac x = stp in exI, simp)
    done
  from g have k7: 
    "\<exists> stp. abc_steps_l (?gs_len + 8 * length gs + 3 *n + 
    length a + 3, 0\<up>?pstr  @ rs # 0\<up>length ys @ lm @ 
    0\<up>(a_md -Suc (?pstr + length ys + n)) @ suf_lm) aprog stp =
    (?gs_len + 8 * length gs + 3 * n + length a + 6, 
    0\<up>n @ rs # 0\<up>(?pstr  - n) @ 0\<up>length ys @ lm @
                        0\<up>(a_md -Suc (?pstr + length ys + n)) @ suf_lm)"
    apply(drule_tac suf_lm = suf_lm in restore_rs, auto)
    apply(rule_tac x = stp in exI, simp)
    done
  from g have k8: "\<exists> stp. abc_steps_l (?gs_len + 8 * length gs + 
    3 * n + length a + 6,
    0\<up>n @ rs # 0\<up>(?pstr  - n) @ 0\<up>length ys @ lm @
                      0\<up>(a_md -Suc (?pstr + length ys + n)) @ suf_lm) aprog stp =
    (?gs_len + 8 * length gs + 6 * n + length a + 6,
                           lm @ rs # 0\<up>(a_md - Suc n) @ suf_lm)"
    apply(drule_tac suf_lm = suf_lm in restore_paras, auto)
    apply(simp add: exponent_add_iff)
    apply(rule_tac x = stp in exI, simp)
    done
  from g have j1: 
    "length aprog = ?gs_len + 8 * length gs + 6 * n + length a + 6"
    by(drule_tac a = a and aa = b and ba = c in ci_cn_length,
      simp, simp, simp)
  from g have j2: "rs_pos = n"
    by(simp add: ci_cn_para_eq)
  from k1 and k2 and k3 and k4 and k5 and k6 and k7 and k8
    and j1 and j2 show 
    "\<exists>stp. abc_steps_l (0, lm @ 0\<up>(a_md - rs_pos) @ suf_lm) aprog stp = 
    (length aprog, lm @ [rs] @ 0\<up>(a_md - rs_pos - 1) @ suf_lm)"
    apply(auto)
    apply(rule_tac x = "stp + stpa + stpb + stpc +
      stpd + stpe + stpf + stpg" in exI, simp add: abc_steps_add)
    done
qed

text {*
  Correctness of the complier (terminate case), which says if the execution of 
  a recursive function @{text "recf"} terminates and gives result, then 
  the Abacus program compiled from @{text "recf"} termintes and gives the same result.
  Additionally, to facilitate induction proof, we append @{text "anything"} to the
  end of Abacus memory.
*}

lemma recursive_compile_correct:
  "\<lbrakk>rec_ci recf = (ap, arity, fp);
    rec_calc_rel recf args r\<rbrakk>
  \<Longrightarrow> (\<exists> stp. (abc_steps_l (0, args @ 0\<up>(fp - arity) @ anything) ap stp) = 
              (length ap, args@[r]@0\<up>(fp - arity - 1) @ anything))"
apply(induct arbitrary: ap fp arity r anything args
  rule: rec_ci.induct)
prefer 5
proof(case_tac "rec_ci g", case_tac "rec_ci f", simp)
  fix n f g ap fp arity r anything args  a b c aa ba ca
  assume f_ind:
    "\<And>ap fp arity r anything args.
    \<lbrakk>aa = ap \<and> ba = arity \<and> ca = fp; rec_calc_rel f args r\<rbrakk> \<Longrightarrow> 
    \<exists>stp. abc_steps_l (0, args @ 0\<up>(fp - arity) @ anything) ap stp =
    (length ap, args @ r # 0\<up>(fp - Suc arity) @ anything)"
    and g_ind:
    "\<And>x xa y xb ya ap fp arity r anything args.
    \<lbrakk>x = (aa, ba, ca); xa = aa \<and> y = (ba, ca); xb = ba \<and> ya = ca; 
    a = ap \<and> b = arity \<and> c = fp; rec_calc_rel g args r\<rbrakk>
    \<Longrightarrow> \<exists>stp. abc_steps_l (0, args @ 0\<up>(fp - arity) @ anything) ap stp =
    (length ap, args @ r # 0\<up>(fp - Suc arity) @ anything)"
    and h: "rec_ci (Pr n f g) = (ap, arity, fp)" 
    "rec_calc_rel (Pr n f g) args r" 
    "rec_ci g = (a, b, c)" 
    "rec_ci f = (aa, ba, ca)"
  from h have nf_ind: 
    "\<And> args r anything. rec_calc_rel f args r \<Longrightarrow> 
    \<exists>stp. abc_steps_l (0, args @ 0\<up>(ca - ba) @ anything) aa stp = 
    (length aa, args @ r # 0\<up>(ca - Suc ba) @ anything)"
    and ng_ind: 
    "\<And> args r anything. rec_calc_rel g args r \<Longrightarrow> 
    \<exists>stp. abc_steps_l (0, args @ 0\<up>(c - b) @ anything) a stp = 
         (length a, args @ r # 0\<up>(c - Suc b)  @ anything)"
    apply(insert f_ind[of aa ba ca], simp)
    apply(insert g_ind[of "(aa, ba, ca)" aa "(ba, ca)" ba ca a b c],
      simp)
    done
  from nf_ind and ng_ind and h show 
    "\<exists>stp. abc_steps_l (0, args @ 0\<up>(fp - arity) @ anything) ap stp = 
    (length ap, args @ r # 0\<up>(fp - Suc arity) @ anything)"
    apply(auto intro: nf_ind ng_ind pr_case)
    done
next
  fix ap fp arity r anything args
  assume h:
    "rec_ci z = (ap, arity, fp)" "rec_calc_rel z args r"
  thus "\<exists>stp. abc_steps_l (0, args @ 0\<up>(fp - arity) @ anything) ap stp =
    (length ap, args @ [r] @ 0\<up>(fp - arity - 1) @ anything)"
    by (rule_tac z_case)    
next
  fix ap fp arity r anything args
  assume h: 
    "rec_ci s = (ap, arity, fp)" 
    "rec_calc_rel s args r"
  thus 
    "\<exists>stp. abc_steps_l (0, args @ 0\<up>(fp - arity) @ anything) ap stp =
    (length ap, args @ [r] @ 0\<up>(fp - arity - 1) @ anything)"
    by(erule_tac s_case, simp)
next
  fix m n ap fp arity r anything args
  assume h: "rec_ci (id m n) = (ap, arity, fp)" 
    "rec_calc_rel (id m n) args r"
  thus "\<exists>stp. abc_steps_l (0, args @ 0\<up>(fp - arity) @ anything) ap stp 
    = (length ap, args @ [r] @ 0\<up>(fp - arity - 1) @ anything)"
    by(erule_tac id_case)
next
  fix n f gs ap fp arity r anything args
  assume ind1: "\<And>x ap fp arity r anything args.
    \<lbrakk>x \<in> set gs; 
    rec_ci x = (ap, arity, fp); 
    rec_calc_rel x args r\<rbrakk>
    \<Longrightarrow> \<exists>stp. abc_steps_l (0, args @ 0\<up>(fp - arity) @ anything) ap stp =
    (length ap, args @ [r] @ 0\<up>(fp - arity - 1) @ anything)"
  and ind2: 
    "\<And>x ap fp arity r anything args.
    \<lbrakk>x = map rec_ci gs; rec_ci f = (ap, arity, fp); rec_calc_rel f args r\<rbrakk>
    \<Longrightarrow> \<exists>stp. abc_steps_l (0, args @ 0 \<up> (fp - arity) @ anything) ap stp =
    (length ap, args @ [r] @ 0 \<up> (fp - arity - 1) @ anything)"
  and h: "rec_ci (Cn n f gs) = (ap, arity, fp)" 
    "rec_calc_rel (Cn n f gs) args r"
  from h show
    "\<exists>stp. abc_steps_l (0, args @ 0\<up>(fp - arity) @ anything) 
       ap stp = (length ap, args @ [r] @ 0\<up>(fp - arity - 1) @ anything)"
    apply(rule_tac cn_case)
    apply(rule_tac ind1, simp, simp, simp)
    apply(rule_tac ind2, auto)    
    done
next
  fix n f ap fp arity r anything args
  assume ind:
    "\<And>ap fp arity r anything args.
    \<lbrakk>rec_ci f = (ap, arity, fp); rec_calc_rel f args r\<rbrakk> \<Longrightarrow> 
    \<exists>stp. abc_steps_l (0, args @ 0\<up>(fp - arity) @ anything) ap stp =
    (length ap, args @ [r] @ 0\<up>(fp - arity - 1) @ anything)"
  and h: "rec_ci (Mn n f) = (ap, arity, fp)" 
    "rec_calc_rel (Mn n f) args r"
  from h show 
    "\<exists>stp. abc_steps_l (0, args @ 0\<up>(fp - arity) @ anything) ap stp = 
              (length ap, args @ [r] @ 0\<up>(fp - arity - 1) @ anything)"
    apply(rule_tac mn_case, rule_tac ind, auto)
    done    
qed

lemma abc_append_uhalt1:
  "\<lbrakk>\<forall> stp. (\<lambda> (ss, e). ss < length bp) (abc_steps_l (0, lm) bp stp);
    p = ap [+] bp [+] cp\<rbrakk>
  \<Longrightarrow> \<forall> stp. (\<lambda> (ss, e). ss < length p) 
                     (abc_steps_l (length ap, lm) p stp)"
apply(auto)
apply(erule_tac x = stp in allE, auto)
apply(frule_tac ap = ap and cp = cp in abc_append_state_in_exc, auto)
done


lemma abc_append_unhalt2:
  "\<lbrakk>abc_steps_l (0, am) ap stp = (length ap, lm); bp \<noteq> [];
  \<forall> stp. (\<lambda> (ss, e). ss < length bp) (abc_steps_l (0, lm) bp stp);
  p = ap [+] bp [+] cp\<rbrakk>
  \<Longrightarrow> \<forall> stp. (\<lambda> (ss, e). ss < length p) (abc_steps_l (0, am) p stp)"
proof -
  assume h: 
    "abc_steps_l (0, am) ap stp = (length ap, lm)" 
    "bp \<noteq> []"
    "\<forall> stp. (\<lambda> (ss, e). ss < length bp) (abc_steps_l (0, lm) bp stp)"
    "p = ap [+] bp [+] cp"
  have "\<exists> stp. (abc_steps_l (0, am) p stp) = (length ap, lm)"
    using h
    apply(simp add: abc_append.simps)
    apply(rule_tac abc_add_exc1, auto)
    done
  from this obtain stpa where g1: 
    "(abc_steps_l (0, am) p stpa) = (length ap, lm)" ..
  moreover have g2: "\<forall> stp. (\<lambda> (ss, e). ss < length p) 
                          (abc_steps_l (length ap, lm) p stp)"
    using h
    apply(erule_tac abc_append_uhalt1, simp)
    done
  moreover from g1 and g2 have
    "\<forall> stp. (\<lambda> (ss, e). ss < length p) 
                    (abc_steps_l (0, am) p (stpa + stp))"
    apply(simp add: abc_steps_add)
    done
  thus "\<forall> stp. (\<lambda> (ss, e). ss < length p) 
                           (abc_steps_l (0, am) p stp)"
    apply(rule_tac allI, auto)
    apply(case_tac "stp \<ge>  stpa")
    apply(erule_tac x = "stp - stpa" in allE, simp)
  proof - 	
    fix stp a b
    assume g3:  "abc_steps_l (0, am) p stp = (a, b)" 
                "\<not> stpa \<le> stp"
    thus "a < length p"
      using g1 h
      apply(case_tac "a < length p", simp, simp)
      apply(subgoal_tac "\<exists> d. stpa = stp + d")
      using  abc_state_keep[of p a b "stpa - stp"]
      apply(erule_tac exE, simp add: abc_steps_add)
      apply(rule_tac x = "stpa - stp" in exI, simp)
      done
  qed
qed

text {*
  Correctness of the complier (non-terminating case for Mn). There are many cases when a 
  recursive function does not terminate. For the purpose of Uiversal Turing Machine, we only 
  need to prove the case for @{text "Mn"} and @{text "Cn"}.
  This lemma is for @{text "Mn"}. For @{text "Mn n f"}, this lemma describes what 
  happens when @{text "f"} always terminates but always does not return zero, so that
  @{text "Mn"} has to loop forever.
  *}

lemma Mn_unhalt:
  assumes mn_rf: "rf = Mn n f"
  and compiled_mnrf: "rec_ci rf = (aprog, rs_pos, a_md)"
  and compiled_f: "rec_ci f = (aprog', rs_pos', a_md')"
  and args: "length lm = n"
  and unhalt_condition: "\<forall> y. (\<exists> rs. rec_calc_rel f (lm @ [y]) rs \<and> rs \<noteq> 0)"
  shows "\<forall> stp. case abc_steps_l (0, lm @ 0\<up>(a_md - rs_pos) @ suf_lm)
               aprog stp of (ss, e) \<Rightarrow> ss < length aprog"
  using mn_rf compiled_mnrf compiled_f args unhalt_condition
proof(rule_tac allI)
  fix stp
  assume h: "rf = Mn n f" 
            "rec_ci rf = (aprog, rs_pos, a_md)"
            "rec_ci f = (aprog', rs_pos', a_md')" 
            "\<forall>y. \<exists>rs. rec_calc_rel f (lm @ [y]) rs \<and> rs \<noteq> 0" "length lm = n"
  have "\<exists>stpa \<ge> stp. abc_steps_l (0, lm @ 0 # 0\<up>(a_md - Suc rs_pos) @ suf_lm) aprog stpa 
         = (0, lm @ stp # 0\<up>(a_md - Suc rs_pos) @ suf_lm)"
  proof(induct stp, auto)
    show "\<exists>stpa. abc_steps_l (0, lm @ 0 # 0\<up>(a_md - Suc rs_pos) @ suf_lm) 
          aprog stpa = (0, lm @ 0 # 0\<up>(a_md - Suc rs_pos) @ suf_lm)"
      apply(rule_tac x = 0 in exI, simp add: abc_steps_l.simps)
      done
  next
    fix stp stpa
    assume g1: "stp \<le> stpa"
      and g2: "abc_steps_l (0, lm @ 0 # 0\<up>(a_md - Suc rs_pos) @ suf_lm)
                            aprog stpa
               = (0, lm @ stp # 0\<up>(a_md - Suc rs_pos) @ suf_lm)"
    have "\<exists>rs. rec_calc_rel f (lm @ [stp]) rs \<and> rs \<noteq> 0"
      using h
      apply(erule_tac x = stp in allE, simp)
      done
    from this obtain rs where g3:
      "rec_calc_rel f (lm @ [stp]) rs \<and> rs \<noteq> 0" ..
    hence "\<exists> stpb. abc_steps_l (0, lm @ stp # 0\<up>(a_md - Suc rs_pos) @
                     suf_lm) aprog stpb 
      = (0, lm @ Suc stp # 0\<up>(a_md - Suc rs_pos) @ suf_lm)"
      using h
      apply(rule_tac mn_ind_step)
      apply(rule_tac recursive_compile_correct, simp, simp)
    proof -
      show "rec_ci f = ((aprog', rs_pos', a_md'))" using h by simp
    next
      show "rec_ci (Mn n f) = (aprog, rs_pos, a_md)" using h by simp
    next
      show "rec_calc_rel f (lm @ [stp]) rs" using g3 by simp
    next
      show "0 < rs" using g3 by simp
    next
      show "Suc rs_pos < a_md"
        using g3 h
        apply(auto)
        apply(frule_tac f = f in para_pattern, simp, simp)
        apply(simp add: rec_ci.simps, auto)
        apply(subgoal_tac "Suc (length lm) < a_md'")
        apply(arith)
        apply(simp add: ci_ad_ge_paras)
        done
    next
      show "rs_pos' = Suc rs_pos"
        using g3 h
        apply(auto)
        apply(frule_tac f = f in para_pattern, simp, simp)
        apply(simp add: rec_ci.simps)
        done
    qed
    thus "\<exists>stpa\<ge>Suc stp. abc_steps_l (0, lm @ 0 # 0\<up>(a_md - Suc rs_pos) @
                 suf_lm) aprog stpa 
      = (0, lm @ Suc stp # 0\<up>(a_md - Suc rs_pos) @ suf_lm)"
      using g2
      apply(erule_tac exE)
      apply(case_tac "stpb = 0", simp add: abc_steps_l.simps)
      apply(rule_tac x = "stpa + stpb" in exI, simp add:
        abc_steps_add)
      using g1
      apply(arith)
      done
  qed
  from this obtain stpa where 
    "stp \<le> stpa \<and> abc_steps_l (0, lm @ 0 # 0\<up>(a_md - Suc rs_pos) @ suf_lm)
         aprog stpa = (0, lm @ stp # 0\<up>(a_md - Suc rs_pos) @ suf_lm)" ..
  thus "case abc_steps_l (0, lm @ 0\<up>(a_md - rs_pos) @ suf_lm) aprog stp
    of (ss, e) \<Rightarrow> ss < length aprog"
    apply(case_tac "abc_steps_l (0, lm @ 0\<up>(a_md - rs_pos) @ suf_lm) aprog
      stp", simp, case_tac "a \<ge> length aprog", 
        simp, simp)
    apply(subgoal_tac "\<exists> d. stpa = stp + d", erule_tac exE)
    apply(subgoal_tac "lm @ 0\<up>(a_md - rs_pos) @ suf_lm = lm @ 0 # 
             0\<up>(a_md - Suc rs_pos) @ suf_lm", simp add: abc_steps_add)
    apply(frule_tac as = a and lm = b and stp = d in abc_state_keep, 
          simp)
    using h  
    apply(simp add: rec_ci.simps, simp, 
              simp only: replicate_Suc[THEN sym])
    apply(case_tac rs_pos, simp, simp)
    apply(rule_tac x = "stpa - stp" in exI, simp, simp)
    done
qed   

lemma abc_append_cons_eq[intro!]: 
  "\<lbrakk>ap = bp; cp = dp\<rbrakk> \<Longrightarrow> ap [+] cp = bp [+] dp"
by simp 

lemma cn_merge_gs_split: 
  "\<lbrakk>i < length gs; rec_ci (gs!i) = (ga, gb, gc)\<rbrakk> \<Longrightarrow> 
     cn_merge_gs (map rec_ci gs) p = 
        cn_merge_gs (map rec_ci (take i gs)) p [+] ga [+] 
       mv_box gb (p + i) [+] 
      cn_merge_gs (map rec_ci (drop (Suc i) gs)) (p + Suc i)"
apply(induct i arbitrary: gs p, case_tac gs, simp, simp)
apply(case_tac gs, simp, case_tac "rec_ci a", 
       simp add: abc_append_commute[THEN sym])
done

text {*
  Correctness of the complier (non-terminating case for Mn). There are many cases when a 
  recursive function does not terminate. For the purpose of Uiversal Turing Machine, we only 
  need to prove the case for @{text "Mn"} and @{text "Cn"}.
  This lemma is for @{text "Cn"}. For @{text "Cn f g1 g2 \<dots>gi, gi+1, \<dots> gn"}, this lemma describes what 
  happens when every one of @{text "g1, g2, \<dots> gi"} terminates, but 
  @{text "gi+1"} does not terminate, so that whole function @{text "Cn f g1 g2 \<dots>gi, gi+1, \<dots> gn"}
  does not terminate.
  *}

lemma cn_gi_uhalt: 
  assumes cn_recf: "rf = Cn n f gs"
  and compiled_cn_recf: "rec_ci rf = (aprog, rs_pos, a_md)"
  and args_length: "length lm = n"
  and exist_unhalt_recf: "i < length gs" "gi = gs ! i"
  and complied_unhalt_recf: "rec_ci gi = (ga, gb, gc)"  "gb = n"
  and all_halt_before_gi: "\<forall> j < i. (\<exists> rs. rec_calc_rel (gs!j) lm rs)" 
  and unhalt_condition: "\<And> slm. \<forall> stp. case abc_steps_l (0, lm @ 0\<up>(gc - gb) @ slm) 
     ga stp of (se, e) \<Rightarrow> se < length ga"
  shows " \<forall> stp. case abc_steps_l (0, lm @ 0\<up>(a_md - rs_pos) @ suflm) aprog
  stp of (ss, e) \<Rightarrow> ss < length aprog"
  using cn_recf compiled_cn_recf args_length exist_unhalt_recf complied_unhalt_recf
        all_halt_before_gi unhalt_condition
proof(case_tac "rec_ci f", simp)
  fix a b c
  assume h1: "rf = Cn n f gs" 
    "rec_ci (Cn n f gs) = (aprog, rs_pos, a_md)" 
    "length lm = n" 
    "gi = gs ! i" 
    "rec_ci (gs!i) = (ga, n, gc)" 
    "gb = n" "rec_ci f = (a, b, c)"
    and h2: "\<forall>j<i. \<exists>rs. rec_calc_rel (gs ! j) lm rs"
    "i < length gs"
  and ind:
    "\<And> slm. \<forall> stp. case abc_steps_l (0, lm @ 0\<up>(gc - n) @ slm) ga stp of (se, e) \<Rightarrow> se < length ga"
  have h3: "rs_pos = n"
    using h1
    by(rule_tac ci_cn_para_eq, simp)
  let ?ggs = "take i gs"
  have "\<exists> ys. (length ys = i \<and> 
    (\<forall> k < i. rec_calc_rel (?ggs ! k) lm (ys ! k)))"
    using h2
    apply(induct i, simp, simp)
    apply(erule_tac exE)
    apply(erule_tac x = ia in allE, simp)
    apply(erule_tac exE)
    apply(rule_tac x = "ys @ [x]" in exI, simp add: nth_append, auto)
    apply(subgoal_tac "k = length ys", simp, simp)
    done
  from this obtain ys where g1:
    "(length ys = i \<and> (\<forall> k < i. rec_calc_rel (?ggs ! k)
                        lm (ys ! k)))" ..
  let ?pstr = "Max (set (Suc n # c # map (\<lambda>(aprog, p, n). n)
    (map rec_ci (gs))))"
  have "\<exists>stp. abc_steps_l (0, lm @ 0\<up>(a_md - n) @ suflm) 
    (cn_merge_gs (map rec_ci ?ggs) ?pstr) stp =
    (listsum (map ((\<lambda>(ap, pos, n). length ap) \<circ> rec_ci) ?ggs) +
    3 * length ?ggs, lm @ 0\<up>(?pstr - n) @ ys @ 0\<up>(a_md -(?pstr + length ?ggs)) @
    suflm) "
    apply(rule_tac  cn_merge_gs_ex)
    apply(rule_tac  recursive_compile_correct, simp, simp)
    using h1
    apply(simp add: rec_ci.simps, auto)
    using g1
    apply(simp)
    using h2 g1
    apply(simp)
    apply(rule_tac min_max.le_supI2)
    apply(rule_tac Max_ge, simp, simp, rule_tac disjI2)
    apply(subgoal_tac "aa \<in> set gs", simp)
    using h2
    apply(rule_tac A = "set (take i gs)" in subsetD, 
      simp add: set_take_subset, simp)
    done
  from this obtain stpa where g2: 
    "abc_steps_l (0, lm @ 0\<up>(a_md - n) @ suflm) 
    (cn_merge_gs (map rec_ci ?ggs) ?pstr) stpa =
    (listsum (map ((\<lambda>(ap, pos, n). length ap) \<circ> rec_ci) ?ggs) +
    3 * length ?ggs, lm @ 0\<up>(?pstr - n) @ ys @ 0\<up>(a_md -(?pstr + length ?ggs)) @
    suflm)" ..
  moreover have 
    "\<exists> cp. aprog = (cn_merge_gs
    (map rec_ci ?ggs) ?pstr) [+] ga [+] cp"
    using h1
    apply(simp add: rec_ci.simps)
    apply(rule_tac x = "mv_box n (?pstr + i) [+] 
      (cn_merge_gs (map rec_ci (drop (Suc i) gs)) (?pstr + Suc i))
      [+]mv_boxes 0 (Suc (max (Suc n) (Max (insert c 
     (((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs))) +
      length gs)) n [+] mv_boxes (max (Suc n) (Max (insert c 
      (((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs)))) 0 (length gs) [+]
      a [+] mv_box b (max (Suc n) 
      (Max (insert c (((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs)))) [+]
     empty_boxes (length gs) [+] mv_box (max (Suc n) 
      (Max (insert c (((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs)))) n [+]
      mv_boxes (Suc (max (Suc n) (Max (insert c 
    (((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs))) + length gs)) 0 n" in exI)
    apply(simp add: abc_append_commute [THEN sym])
    apply(auto)
    using cn_merge_gs_split[of i gs ga "length lm" gc 
      "(max (Suc (length lm))
       (Max (insert c (((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs))))"] 
      h2
    apply(simp)
    done
  from this obtain cp where g3: 
    "aprog = (cn_merge_gs (map rec_ci ?ggs) ?pstr) [+] ga [+] cp" ..
  show "\<forall> stp. case abc_steps_l (0, lm @ 0\<up>(a_md - rs_pos) @ suflm) 
    aprog stp of (ss, e) \<Rightarrow> ss < length aprog"
  proof(rule_tac abc_append_unhalt2)
    show "abc_steps_l (0, lm @ 0\<up>(a_md - rs_pos) @ suflm) (
      cn_merge_gs (map rec_ci ?ggs) ?pstr) stpa =
         (length ((cn_merge_gs (map rec_ci ?ggs) ?pstr)),  
          lm @ 0\<up>(?pstr - n) @ ys @ 0\<up>(a_md -(?pstr + length ?ggs)) @ suflm)"
      using h3 g2
      apply(simp add: cn_merge_gs_length)
      done
  next
    show "ga \<noteq> []"
      using h1
      apply(simp add: rec_ci_not_null)
      done
  next
    show "\<forall>stp. case abc_steps_l (0, lm @ 0\<up>(?pstr - n) @ ys
      @ 0\<up>(a_md - (?pstr + length (take i gs))) @ suflm) ga  stp of
          (ss, e) \<Rightarrow> ss < length ga"
      using ind[of "0\<up>(?pstr - gc) @ ys @ 0\<up>(a_md - (?pstr + length (take i gs)))
        @ suflm"]
      apply(subgoal_tac "lm @ 0\<up>(?pstr - n) @ ys
        @ 0\<up>(a_md - (?pstr + length (take i gs))) @ suflm
                       = lm @ 0\<up>(gc - n) @ 
        0\<up>(?pstr - gc) @ ys @ 0\<up>(a_md - (?pstr + length (take i gs))) @ suflm", simp)
      apply(simp add: replicate_add[THEN sym])
      apply(subgoal_tac "gc > n \<and> ?pstr \<ge> gc")
      apply(erule_tac conjE)
      apply(simp add: h1)
      using h1
      apply(auto)
      apply(rule_tac min_max.le_supI2)
      apply(rule_tac Max_ge, simp, simp)
      apply(rule_tac disjI2)
      using h2
      apply(rule_tac x = "gs!i" in rev_image_eqI, simp, simp)
      done
  next
    show "aprog = cn_merge_gs (map rec_ci (take i gs)) 
              ?pstr [+] ga [+] cp"
      using g3 by simp
  qed
qed

lemma recursive_compile_correct_spec: 
  "\<lbrakk>rec_ci re = (ap, ary, fp); 
    rec_calc_rel re args r\<rbrakk>
  \<Longrightarrow> (\<exists> stp. (abc_steps_l (0, args @ 0\<up>(fp - ary)) ap stp) = 
                     (length ap, args@[r]@0\<up>(fp - ary - 1)))"
using recursive_compile_correct[of re ap ary fp args r "[]"]
by simp

definition dummy_abc :: "nat \<Rightarrow> abc_inst list"
where
"dummy_abc k = [Inc k, Dec k 0, Goto 3]"

definition abc_list_crsp:: "nat list \<Rightarrow> nat list \<Rightarrow> bool"
  where
  "abc_list_crsp xs ys = (\<exists> n. xs = ys @ 0\<up>n \<or> ys = xs @ 0\<up>n)"

lemma [intro]: "abc_list_crsp (lm @ 0\<up>m) lm"
apply(auto simp: abc_list_crsp_def)
done

lemma abc_list_crsp_lm_v: 
  "abc_list_crsp lma lmb \<Longrightarrow> abc_lm_v lma n = abc_lm_v lmb n"
apply(auto simp: abc_list_crsp_def abc_lm_v.simps 
                 nth_append)
done

lemma  rep_app_cons_iff: 
  "k < n \<Longrightarrow> replicate n a[k:=b] = 
          replicate k a @ b # replicate (n - k - 1) a"
apply(induct n arbitrary: k, simp)
apply(simp split:nat.splits)
done

lemma abc_list_crsp_lm_s: 
  "abc_list_crsp lma lmb \<Longrightarrow> 
      abc_list_crsp (abc_lm_s lma m n) (abc_lm_s lmb m n)"
apply(auto simp: abc_list_crsp_def abc_lm_v.simps abc_lm_s.simps)
apply(simp_all add: list_update_append, auto)
proof -
  fix na
  assume h: "m < length lmb + na" " \<not> m < length lmb"
  hence "m - length lmb < na" by simp
  hence "replicate na 0[(m- length lmb):= n] = 
           replicate (m - length lmb) 0 @ n # 
              replicate (na - (m - length lmb) - 1) 0"
    apply(erule_tac rep_app_cons_iff)
    done
  thus "\<exists>nb. replicate na 0[m - length lmb := n] =
                 replicate (m - length lmb) 0 @ n # replicate nb 0 \<or>
                 replicate (m - length lmb) 0 @ [n] =
                 replicate na 0[m - length lmb := n] @ replicate nb 0"
    apply(auto)
    done
next
  fix na
  assume h: "\<not> m < length lmb + na"
  show 
    "\<exists>nb. replicate na 0 @ replicate (m - (length lmb + na)) 0 @ [n] =
           replicate (m - length lmb) 0 @ n # replicate nb 0 \<or>
          replicate (m - length lmb) 0 @ [n] =
            replicate na 0 @
            replicate (m - (length lmb + na)) 0 @ n # replicate nb 0"
    apply(rule_tac x = 0 in exI, simp, auto)
    using h
    apply(simp add: replicate_add[THEN sym])
    done
next
  fix na
  assume h: "\<not> m < length lma" "m < length lma + na"
  hence "m - length lma < na" by simp
  hence 
    "replicate na 0[(m- length lma):= n] = replicate (m - length lma) 
                  0 @ n # replicate (na - (m - length lma) - 1) 0"
    apply(erule_tac rep_app_cons_iff)
    done
  thus "\<exists>nb. replicate (m - length lma) 0 @ [n] =
                 replicate na 0[m - length lma := n] @ replicate nb 0 
           \<or> replicate na 0[m - length lma := n] =
                 replicate (m - length lma) 0 @ n # replicate nb 0"
    apply(auto)
    done
next
  fix na
  assume "\<not> m < length lma + na"
  thus " \<exists>nb. replicate (m - length lma) 0 @ [n] =
            replicate na 0 @
            replicate (m - (length lma + na)) 0 @ n # replicate nb 0 
        \<or>   replicate na 0 @ 
               replicate (m - (length lma + na)) 0 @ [n] =
            replicate (m - length lma) 0 @ n # replicate nb 0"
    apply(rule_tac x = 0 in exI, simp, auto)
    apply(simp add: replicate_add[THEN sym])
    done
qed

lemma abc_list_crsp_step: 
  "\<lbrakk>abc_list_crsp lma lmb; abc_step_l (aa, lma) i = (a, lma'); 
    abc_step_l (aa, lmb) i = (a', lmb')\<rbrakk>
    \<Longrightarrow> a' = a \<and> abc_list_crsp lma' lmb'"
apply(case_tac i, auto simp: abc_step_l.simps 
       abc_list_crsp_lm_s abc_list_crsp_lm_v Let_def 
                       split: abc_inst.splits if_splits)
done

lemma abc_list_crsp_steps: 
  "\<lbrakk>abc_steps_l (0, lm @ 0\<up>m) aprog stp = (a, lm'); aprog \<noteq> []\<rbrakk> 
      \<Longrightarrow> \<exists> lma. abc_steps_l (0, lm) aprog stp = (a, lma) \<and> 
                                          abc_list_crsp lm' lma"
apply(induct stp arbitrary: a lm', simp add: abc_steps_l.simps, auto)
apply(case_tac "abc_steps_l (0, lm @ 0\<up>m) aprog stp", 
      simp add: abc_step_red)
proof -
  fix stp a lm' aa b
  assume ind:
    "\<And>a lm'. aa = a \<and> b = lm' \<Longrightarrow> 
     \<exists>lma. abc_steps_l (0, lm) aprog stp = (a, lma) \<and>
                                          abc_list_crsp lm' lma"
    and h: "abc_steps_l (0, lm @ 0\<up>m) aprog (Suc stp) = (a, lm')" 
           "abc_steps_l (0, lm @ 0\<up>m) aprog stp = (aa, b)" 
           "aprog \<noteq> []"
  hence g1: "abc_steps_l (0, lm @ 0\<up>m) aprog (Suc stp)
          = abc_step_l (aa, b) (abc_fetch aa aprog)"
    apply(rule_tac abc_step_red, simp)
    done
  have "\<exists>lma. abc_steps_l (0, lm) aprog stp = (aa, lma) \<and> 
              abc_list_crsp b lma"
    apply(rule_tac ind, simp)
    done
  from this obtain lma where g2: 
    "abc_steps_l (0, lm) aprog stp = (aa, lma) \<and> 
     abc_list_crsp b lma"   ..
  hence g3: "abc_steps_l (0, lm) aprog (Suc stp)
          = abc_step_l (aa, lma) (abc_fetch aa aprog)"
    apply(rule_tac abc_step_red, simp)
    done
  show "\<exists>lma. abc_steps_l (0, lm) aprog (Suc stp) = (a, lma) \<and> abc_list_crsp lm' lma"
    using g1 g2 g3 h
    apply(auto)
    apply(case_tac "abc_step_l (aa, b) (abc_fetch aa aprog)",
          case_tac "abc_step_l (aa, lma) (abc_fetch aa aprog)", simp)
    apply(rule_tac abc_list_crsp_step, auto)
    done
qed

lemma recursive_compile_correct_norm: 
  "\<lbrakk>rec_ci re = (aprog, rs_pos, a_md);  
   rec_calc_rel re lm rs\<rbrakk>
  \<Longrightarrow> (\<exists> stp lm' m. (abc_steps_l (0, lm) aprog stp) = 
  (length aprog, lm') \<and> abc_list_crsp lm' (lm @ rs # 0\<up>m))"
apply(frule_tac recursive_compile_correct_spec, auto)
apply(drule_tac abc_list_crsp_steps)
apply(rule_tac rec_ci_not_null, simp)
apply(erule_tac exE, rule_tac x = stp in exI, 
  auto simp: abc_list_crsp_def)
done

lemma [simp]: "length (dummy_abc (length lm)) = 3"
apply(simp add: dummy_abc_def)
done

lemma [simp]: "dummy_abc (length lm) \<noteq> []"
apply(simp add: dummy_abc_def)
done

lemma dummy_abc_steps_ex: 
  "\<exists>bstp. abc_steps_l (0, lm') (dummy_abc (length lm)) bstp = 
  ((Suc (Suc (Suc 0))), abc_lm_s lm' (length lm) (abc_lm_v lm' (length lm)))"
apply(rule_tac x = "Suc (Suc (Suc 0))" in exI)
apply(auto simp: abc_steps_l.simps abc_step_l.simps 
  dummy_abc_def abc_fetch.simps)
apply(auto simp: abc_lm_s.simps abc_lm_v.simps nth_append)
apply(simp add: butlast_append)
done

lemma [simp]: 
  "\<lbrakk>Suc (length lm) - length lm' \<le> n; \<not> length lm < length lm'; lm @ rs # 0 \<up> m = lm' @ 0 \<up> n\<rbrakk> 
  \<Longrightarrow> lm' @ 0 \<up> Suc (length lm - length lm') = lm @ [rs]"
apply(subgoal_tac "n > m")
apply(subgoal_tac "\<exists> d. n = d + m", erule_tac exE)
apply(simp add: replicate_add)
apply(drule_tac length_equal, simp)
apply(simp add: replicate_Suc[THEN sym] del: replicate_Suc)
apply(rule_tac x = "n - m" in exI, simp)
apply(drule_tac length_equal, simp)
done

lemma [elim]: 
  "lm @ rs # 0\<up>m = lm' @ 0\<up>n \<Longrightarrow> 
  \<exists>m. abc_lm_s lm' (length lm) (abc_lm_v lm' (length lm)) = 
                            lm @ rs # 0\<up>m"
proof(cases "length lm' > length lm")
  case True 
  assume h: "lm @ rs # 0\<up>m = lm' @ 0\<up>n" "length lm < length lm'"
  hence "m \<ge> n"
    apply(drule_tac length_equal)
    apply(simp)
    done
  hence "\<exists> d. m = d + n"
    apply(rule_tac x = "m - n" in exI, simp)
    done
  from this obtain d where "m = d + n" ..
  from h and this show "?thesis"
    apply(auto simp: abc_lm_s.simps abc_lm_v.simps 
                     replicate_add)
    done
next
  case False
  assume h:"lm @ rs # 0\<up>m = lm' @ 0\<up>n" 
    and    g: "\<not> length lm < length lm'"
  have "take (Suc (length lm)) (lm @ rs # 0\<up>m) = 
                        take (Suc (length lm)) (lm' @ 0\<up>n)"
    using h by simp
  moreover have "n \<ge> (Suc (length lm) - length lm')"
    using h g
    apply(drule_tac length_equal)
    apply(simp)
    done
  ultimately show 
    "\<exists>m. abc_lm_s lm' (length lm) (abc_lm_v lm' (length lm)) =
                                                       lm @ rs # 0\<up>m"
    using g h
    apply(simp add: abc_lm_s.simps abc_lm_v.simps min_def)
    apply(rule_tac x = 0 in exI, 
      simp add:replicate_append_same replicate_Suc[THEN sym]
                                      del:replicate_Suc)
    done    
qed

lemma [elim]: 
  "abc_list_crsp lm' (lm @ rs # 0\<up>m)
  \<Longrightarrow> \<exists>m. abc_lm_s lm' (length lm) (abc_lm_v lm' (length lm)) 
             = lm @ rs # 0\<up>m"
apply(auto simp: abc_list_crsp_def)
apply(simp add: abc_lm_v.simps abc_lm_s.simps)
apply(rule_tac x =  "m + n" in exI, 
      simp add: replicate_add)
done

lemma abc_append_dummy_complie:
  "\<lbrakk>rec_ci recf = (ap, ary, fp);  
    rec_calc_rel recf args r; 
    length args = k\<rbrakk>
  \<Longrightarrow> (\<exists> stp m. (abc_steps_l (0, args) (ap [+] dummy_abc k) stp) = 
                  (length ap + 3, args @ r # 0\<up>m))"
apply(drule_tac recursive_compile_correct_norm, auto simp: numeral_3_eq_3)
proof -
  fix stp lm' m
  assume h: "rec_calc_rel recf args r"  
    "abc_steps_l (0, args) ap stp = (length ap, lm')" 
    "abc_list_crsp lm' (args @ r # 0\<up>m)"
  have "\<exists>stp. abc_steps_l (0, args) (ap [+] 
    (dummy_abc (length args))) stp = (length ap + 3, 
    abc_lm_s lm' (length args) (abc_lm_v lm' (length args)))"
    using h
    apply(rule_tac bm = lm' in abc_append_exc2,
          auto intro: dummy_abc_steps_ex simp: numeral_3_eq_3)
    done
  thus "\<exists>stp m. abc_steps_l (0, args) (ap [+] 
    dummy_abc (length args)) stp = (Suc (Suc (Suc (length ap))), args @ r # 0\<up>m)"
    using h
    apply(erule_tac exE)
    apply(rule_tac x = stpa in exI, auto)
    done
qed

lemma [simp]: "length (dummy_abc k) = 3"
apply(simp add: dummy_abc_def)
done

lemma [simp]: "length args = k \<Longrightarrow> abc_lm_v (args @ r # 0\<up>m) k = r "
apply(simp add: abc_lm_v.simps nth_append)
done

lemma [simp]: "crsp (layout_of (ap [+] dummy_abc k)) (0, args)
  (Suc 0, Bk # Bk # ires, <args> @ Bk \<up> rn) ires"
apply(auto simp: crsp.simps start_of.simps)
done

(* cccc *)

fun tm_of_rec :: "recf \<Rightarrow> instr list"
where "tm_of_rec recf = (let (ap, k, fp) = rec_ci recf in
                         let tp = tm_of (ap [+] dummy_abc k) in 
                             tp @ (shift (mopup k) (length tp div 2)))"

lemma recursive_compile_to_tm_correct: 
  "\<lbrakk>rec_ci recf = (ap, ary, fp); 
    rec_calc_rel recf args r;
    length args = k;
    ly = layout_of (ap [+] dummy_abc k);
    tp = tm_of (ap [+] dummy_abc k)\<rbrakk>
  \<Longrightarrow> \<exists> stp m l. steps0 (Suc 0, Bk # Bk # ires, <args> @ Bk\<up>rn)
  (tp @ shift (mopup k) (length tp div 2)) stp
  = (0, Bk\<up>m @ Bk # Bk # ires, Oc\<up>Suc r @ Bk\<up>l)"
  using abc_append_dummy_complie[of recf ap ary fp args r k]
apply(simp)
apply(erule_tac exE)+
apply(frule_tac tp = tp and n = k 
               and ires = ires in compile_correct_halt, simp_all add: length_append)
apply(simp_all add: length_append)
done

lemma recursive_compile_to_tm_correct2: 
  assumes "rec_ci recf = (ap, ary, fp)" 
  and     "rec_calc_rel recf args r"
  and     "length args = k"
  and     "tp = tm_of (ap [+] dummy_abc k)"
  shows "\<exists> m n. {\<lambda>tp. tp = ([Bk, Bk], <args>)}
             (tp @ (shift (mopup k) (length tp div 2)))
             {\<lambda>tp. tp = (Bk \<up> m, Oc \<up> (Suc r) @ Bk \<up> n)}"
using recursive_compile_to_tm_correct[where ires="[]" and rn="0", OF assms(1-3) _ assms(4)]
apply(simp add: Hoare_halt_def)
apply(drule_tac x="layout_of (ap [+] dummy_abc k)" in meta_spec)
apply(auto)
apply(rule_tac x="m + 2" in exI)
apply(rule_tac x="l" in exI)
apply(rule_tac x="stp" in exI)
apply(auto)
by (metis append_Nil2 replicate_app_Cons_same)

lemma recursive_compile_to_tm_correct3: 
  assumes "rec_calc_rel recf args r"
  shows "{\<lambda>tp. tp = ([Bk, Bk], <args>)} tm_of_rec recf {\<lambda>tp. \<exists>k l. tp = (Bk \<up> k, <r> @ Bk \<up> l)}"
using recursive_compile_to_tm_correct2[OF _ assms] 
apply(auto)
apply(case_tac "rec_ci recf")
apply(auto)
apply(drule_tac x="a" in meta_spec)
apply(drule_tac x="b" in meta_spec)
apply(drule_tac x="c" in meta_spec)
apply(drule_tac x="length args" in meta_spec)
apply(drule_tac x="tm_of (a [+] dummy_abc (length args))" in meta_spec)
apply(auto)
apply(simp add: tape_of_nat_abv)
apply(subgoal_tac "b = length args")
apply(simp add: Hoare_halt_def)
apply(auto)[1]
apply(rule_tac x="na" in exI)
apply(auto)[1]
apply(case_tac "steps0 (Suc 0, [Bk, Bk], <args>)
                                   (tm_of (a [+] dummy_abc (length args)) @
                                    shift (mopup (length args))
                                     (listsum
 (layout_of (a [+] dummy_abc (length args)))))
                                   na")
apply(simp)
by (metis assms para_pattern)


lemma [simp]:
  "list_all (\<lambda>(acn, s). s \<le> Suc (Suc (Suc (Suc (Suc (Suc (2 * n))))))) xs \<Longrightarrow>
  list_all (\<lambda>(acn, s). s \<le> Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (2 * n))))))))) xs"
apply(induct xs, simp, simp)
apply(case_tac a, simp)
done

lemma shift_append: "shift (xs @ ys) n = shift xs n @ shift ys n"
apply(simp add: shift.simps)
done

lemma [simp]: "length (shift (mopup n) ss) = 4 * n + 12"
apply(auto simp: mopup.simps shift_append mopup_b_def)
done

lemma length_tm_even[intro]: "length (tm_of ap) mod 2 = 0"
apply(simp add: tm_of.simps)
done

lemma [simp]: "k < length ap \<Longrightarrow> tms_of ap ! k  = 
 ci (layout_of ap) (start_of (layout_of ap) k) (ap ! k)"
apply(simp add: tms_of.simps tpairs_of.simps)
done

lemma start_of_suc_inc:
  "\<lbrakk>k < length ap; ap ! k = Inc n\<rbrakk> \<Longrightarrow> start_of (layout_of ap) (Suc k) =
                        start_of (layout_of ap) k + 2 * n + 9"
apply(rule_tac start_of_Suc1, auto simp: abc_fetch.simps)
done

lemma start_of_suc_dec:
  "\<lbrakk>k < length ap; ap ! k = (Dec n e)\<rbrakk> \<Longrightarrow> start_of (layout_of ap) (Suc k) =
                        start_of (layout_of ap) k + 2 * n + 16"
apply(rule_tac start_of_Suc2, auto simp: abc_fetch.simps)
done

lemma inc_state_all_le:
  "\<lbrakk>k < length ap; ap ! k = Inc n; 
       (a, b) \<in> set (shift (shift tinc_b (2 * n)) 
                            (start_of (layout_of ap) k - Suc 0))\<rbrakk>
       \<Longrightarrow> b \<le> start_of (layout_of ap) (length ap)"
apply(subgoal_tac "b \<le> start_of (layout_of ap) (Suc k)")
apply(subgoal_tac "start_of (layout_of ap) (Suc k) \<le> start_of (layout_of ap) (length ap) ")
apply(arith)
apply(case_tac "Suc k = length ap", simp)
apply(rule_tac start_of_less, simp)
apply(auto simp: tinc_b_def shift.simps start_of_suc_inc length_of.simps startof_not0)
done

lemma findnth_le[elim]: 
  "(a, b) \<in> set (shift (findnth n) (start_of (layout_of ap) k - Suc 0))
  \<Longrightarrow> b \<le> Suc (start_of (layout_of ap) k + 2 * n)"
apply(induct n, simp add: findnth.simps shift.simps)
apply(simp add: findnth.simps shift_append, auto)
apply(auto simp: shift.simps)
done

lemma findnth_state_all_le1:
  "\<lbrakk>k < length ap; ap ! k = Inc n;
  (a, b) \<in> 
  set (shift (findnth n) (start_of (layout_of ap) k - Suc 0))\<rbrakk> 
  \<Longrightarrow> b \<le> start_of (layout_of ap) (length ap)"
apply(subgoal_tac "b \<le> start_of (layout_of ap) (Suc k)")
apply(subgoal_tac "start_of (layout_of ap) (Suc k) \<le> start_of (layout_of ap) (length ap) ")
apply(arith)
apply(case_tac "Suc k = length ap", simp)
apply(rule_tac start_of_less, simp)
apply(subgoal_tac "b \<le> start_of (layout_of ap) k + 2*n + 1 \<and> 
     start_of (layout_of ap) k + 2*n + 1 \<le>  start_of (layout_of ap) (Suc k)", auto)
apply(auto simp: tinc_b_def shift.simps length_of.simps startof_not0 start_of_suc_inc)
done

lemma start_of_eq: "length ap < as \<Longrightarrow> start_of (layout_of ap) as = start_of (layout_of ap) (length ap)"
apply(induct as, simp)
apply(case_tac "length ap < as", simp add: start_of.simps)
apply(subgoal_tac "as = length ap")
apply(simp add: start_of.simps)
apply arith
done

lemma start_of_all_le: "start_of (layout_of ap) as \<le> start_of (layout_of ap) (length ap)"
apply(subgoal_tac "as > length ap \<or> as = length ap \<or> as < length ap", 
      auto simp: start_of_eq start_of_less)
done

lemma findnth_state_all_le2: 
  "\<lbrakk>k < length ap; 
  ap ! k = Dec n e;
  (a, b) \<in> set (shift (findnth n) (start_of (layout_of ap) k - Suc 0))\<rbrakk>
  \<Longrightarrow> b \<le> start_of (layout_of ap) (length ap)"
apply(subgoal_tac "b \<le> start_of (layout_of ap) k + 2*n + 1 \<and> 
     start_of (layout_of ap) k + 2*n + 1 \<le>  start_of (layout_of ap) (Suc k) \<and>
      start_of (layout_of ap) (Suc k) \<le> start_of (layout_of ap) (length ap)", auto)
apply(subgoal_tac "start_of (layout_of ap) (Suc k) = 
  start_of  (layout_of ap)  k + 2*n + 16", simp)
apply(simp add: start_of_suc_dec)
apply(rule_tac start_of_all_le)
done

lemma dec_state_all_le[simp]:
  "\<lbrakk>k < length ap; ap ! k = Dec n e; 
  (a, b) \<in> set (shift (shift tdec_b (2 * n))
  (start_of (layout_of ap) k - Suc 0))\<rbrakk>
       \<Longrightarrow> b \<le> start_of (layout_of ap) (length ap)"
apply(subgoal_tac "2*n + start_of (layout_of ap) k + 16 \<le> start_of (layout_of ap) (length ap) \<and> start_of (layout_of ap) k > 0")
prefer 2
apply(subgoal_tac "start_of (layout_of ap) (Suc k) = start_of (layout_of ap) k + 2*n + 16
                 \<and> start_of (layout_of ap) (Suc k) \<le> start_of (layout_of ap) (length ap)")
apply(simp add: startof_not0, rule_tac conjI)
apply(simp add: start_of_suc_dec)
apply(rule_tac start_of_all_le)
apply(auto simp: tdec_b_def shift.simps)
done

lemma tms_any_less: 
  "\<lbrakk>k < length ap; (a, b) \<in> set (tms_of ap ! k)\<rbrakk> \<Longrightarrow> 
  b \<le> start_of (layout_of ap) (length ap)"
apply(case_tac "ap!k", auto simp: tms_of.simps tpairs_of.simps ci.simps shift_append adjust.simps)
apply(erule_tac findnth_state_all_le1, simp_all)
apply(erule_tac inc_state_all_le, simp_all)
apply(erule_tac findnth_state_all_le2, simp_all)
apply(rule_tac start_of_all_le)
apply(rule_tac dec_state_all_le, simp_all)
apply(rule_tac start_of_all_le)
done

lemma concat_in: "i < length (concat xs) \<Longrightarrow> \<exists>k < length xs. concat xs ! i \<in> set (xs ! k)"
apply(induct xs rule: list_tl_induct, simp, simp)
apply(case_tac "i < length (concat list)", simp)
apply(erule_tac exE, rule_tac x = k in exI)
apply(simp add: nth_append)
apply(rule_tac x = "length list" in exI, simp)
apply(simp add: nth_append)
done 

lemma [simp]: "length (tms_of ap) = length ap"
apply(simp add: tms_of.simps tpairs_of.simps)
done

declare length_concat[simp]

lemma in_tms: "i < length (tm_of ap) \<Longrightarrow> \<exists> k < length ap. (tm_of ap ! i) \<in> set (tms_of ap ! k)"
apply(simp only: tm_of.simps)
using concat_in[of i "tms_of ap"]
apply(auto)
done

lemma all_le_start_of: "list_all (\<lambda>(acn, s). 
  s \<le> start_of (layout_of ap) (length ap)) (tm_of ap)"
apply(simp only: list_all_length)
apply(rule_tac allI, rule_tac impI)
apply(drule_tac in_tms, auto elim: tms_any_less)
done

lemma length_ci: 
"\<lbrakk>k < length ap; length (ci ly y (ap ! k)) = 2 * qa\<rbrakk>
      \<Longrightarrow> layout_of ap ! k = qa"
apply(case_tac "ap ! k")
apply(auto simp: layout_of.simps ci.simps 
  length_of.simps tinc_b_def tdec_b_def length_findnth adjust.simps)
done

lemma [intro]: "length (ci ly y i) mod 2 = 0"
apply(case_tac i, auto simp: ci.simps length_findnth
  tinc_b_def adjust.simps tdec_b_def)
done

lemma [intro]: "listsum (map (length \<circ> (\<lambda>(x, y). ci ly x y)) zs) mod 2 = 0"
apply(induct zs rule: list_tl_induct, simp)
apply(case_tac a, simp)
apply(subgoal_tac "length (ci ly aa b) mod 2 = 0")
apply(auto)
done

lemma zip_pre:
  "(length ys) \<le> length ap \<Longrightarrow>
  zip ys ap = zip ys (take (length ys) (ap::'a list))"
proof(induct ys arbitrary: ap, simp, case_tac ap, simp)
  fix a ys ap aa list
  assume ind: "\<And>(ap::'a list). length ys \<le> length ap \<Longrightarrow> 
    zip ys ap = zip ys (take (length ys) ap)"
  and h: "length (a # ys) \<le> length ap" "(ap::'a list) = aa # (list::'a list)"
  from h show "zip (a # ys) ap = zip (a # ys) (take (length (a # ys)) ap)"
    using ind[of list]
    apply(simp)
    done
qed

lemma length_start_of_tm: "start_of (layout_of ap) (length ap) = Suc (length (tm_of ap)  div 2)"
using tpa_states[of "tm_of ap"  "length ap" ap]
apply(simp add: tm_of.simps)
done

lemma [elim]: "list_all (\<lambda>(acn, s). s \<le> Suc q) xs
        \<Longrightarrow> list_all (\<lambda>(acn, s). s \<le> q + (2 * n + 6)) xs"
apply(simp add: list_all_length)
apply(auto)
done

lemma [simp]: "length mopup_b = 12"
apply(simp add: mopup_b_def)
done
(*
lemma [elim]: "\<lbrakk>na < 4 * n; tshift (mop_bef n) q ! na = (a, b)\<rbrakk> \<Longrightarrow> 
  b \<le> q + (2 * n + 6)"
apply(induct n, simp, simp add: mop_bef.simps nth_append tshift_append shift_length)
apply(case_tac "na < 4*n", simp, simp)
apply(subgoal_tac "na = 4*n \<or> na = 1 + 4*n \<or> na = 2 + 4*n \<or> na = 3 + 4*n",
  auto simp: shift_length)
apply(simp_all add: tshift.simps)
done
*)

lemma mp_up_all_le: "list_all  (\<lambda>(acn, s). s \<le> q + (2 * n + 6)) 
  [(R, Suc (Suc (2 * n + q))), (R, Suc (2 * n + q)), 
  (L, 5 + 2 * n + q), (W0, Suc (Suc (Suc (2 * n + q)))), (R, 4 + 2 * n + q),
  (W0, Suc (Suc (Suc (2 * n + q)))), (R, Suc (Suc (2 * n + q))),
  (W0, Suc (Suc (Suc (2 * n + q)))), (L, 5 + 2 * n + q),
  (L, 6 + 2 * n + q), (R, 0),  (L, 6 + 2 * n + q)]"
apply(auto)
done

lemma [simp]: "(a, b) \<in> set (mopup_a n) \<Longrightarrow> b \<le> 2 * n + 6"
apply(induct n, auto simp: mopup_a.simps)
done

lemma [simp]: "(a, b) \<in> set (shift (mopup n) (listsum (layout_of ap)))
  \<Longrightarrow> b \<le> (2 * listsum (layout_of ap) + length (mopup n)) div 2"
apply(auto simp: mopup.simps shift_append shift.simps)
apply(auto simp: mopup_a.simps mopup_b_def)
done

lemma [intro]: " 2 \<le> 2 * listsum (layout_of ap) + length (mopup n)"
apply(simp add: mopup.simps)
done

lemma [intro]: " (2 * listsum (layout_of ap) + length (mopup n)) mod 2 = 0"
apply(auto simp: mopup.simps)
apply arith
done

lemma [simp]: "b \<le> Suc x
          \<Longrightarrow> b \<le> (2 * x + length (mopup n)) div 2"
apply(auto simp: mopup.simps)
done

lemma t_compiled_correct: 
  "\<lbrakk>tp = tm_of ap; ly = layout_of ap; mop_ss = start_of ly (length ap)\<rbrakk> \<Longrightarrow> 
    tm_wf (tp @ shift( mopup n) (length tp div 2), 0)"
  using length_start_of_tm[of ap] all_le_start_of[of ap]
apply(auto simp: tm_wf.simps List.list_all_iff)
done

end

    
  


  

