[STATEMENT]
lemma mopup_bef_erase_a_2_jump_over[simp]:
  "\<lbrakk>n < length lm; 0 < s; s mod 2 = Suc 0;  s \<le> 2 * n;
   mopup_bef_erase_a (s, l, Bk # xs) lm n ires; \<not> (Suc (Suc s) \<le> 2 * n)\<rbrakk>
\<Longrightarrow> mopup_jump_over1 (s', Bk # l, xs) lm n ires"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n < length lm; 0 < s; s mod 2 = Suc 0; s \<le> 2 * n; mopup_bef_erase_a (s, l, Bk # xs) lm n ires; \<not> Suc (Suc s) \<le> 2 * n\<rbrakk> \<Longrightarrow> mopup_jump_over1 (s', Bk # l, xs) lm n ires
[PROOF STEP]
proof(cases n)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>n < length lm; 0 < s; s mod 2 = Suc 0; s \<le> 2 * n; mopup_bef_erase_a (s, l, Bk # xs) lm n ires; \<not> Suc (Suc s) \<le> 2 * n; n = 0\<rbrakk> \<Longrightarrow> mopup_jump_over1 (s', Bk # l, xs) lm n ires
 2. \<And>nat. \<lbrakk>n < length lm; 0 < s; s mod 2 = Suc 0; s \<le> 2 * n; mopup_bef_erase_a (s, l, Bk # xs) lm n ires; \<not> Suc (Suc s) \<le> 2 * n; n = Suc nat\<rbrakk> \<Longrightarrow> mopup_jump_over1 (s', Bk # l, xs) lm n ires
[PROOF STEP]
case (Suc nat)
[PROOF STATE]
proof (state)
this:
n = Suc nat

goal (2 subgoals):
 1. \<lbrakk>n < length lm; 0 < s; s mod 2 = Suc 0; s \<le> 2 * n; mopup_bef_erase_a (s, l, Bk # xs) lm n ires; \<not> Suc (Suc s) \<le> 2 * n; n = 0\<rbrakk> \<Longrightarrow> mopup_jump_over1 (s', Bk # l, xs) lm n ires
 2. \<And>nat. \<lbrakk>n < length lm; 0 < s; s mod 2 = Suc 0; s \<le> 2 * n; mopup_bef_erase_a (s, l, Bk # xs) lm n ires; \<not> Suc (Suc s) \<le> 2 * n; n = Suc nat\<rbrakk> \<Longrightarrow> mopup_jump_over1 (s', Bk # l, xs) lm n ires
[PROOF STEP]
assume assms: "n < length lm" "0 < s" "s mod 2 = Suc 0" "s \<le> 2 * n"
    "mopup_bef_erase_a (s, l, Bk # xs) lm n ires" "\<not> (Suc (Suc s) \<le> 2 * n)"
[PROOF STATE]
proof (state)
this:
n < length lm
0 < s
s mod 2 = Suc 0
s \<le> 2 * n
mopup_bef_erase_a (s, l, Bk # xs) lm n ires
\<not> Suc (Suc s) \<le> 2 * n

goal (2 subgoals):
 1. \<lbrakk>n < length lm; 0 < s; s mod 2 = Suc 0; s \<le> 2 * n; mopup_bef_erase_a (s, l, Bk # xs) lm n ires; \<not> Suc (Suc s) \<le> 2 * n; n = 0\<rbrakk> \<Longrightarrow> mopup_jump_over1 (s', Bk # l, xs) lm n ires
 2. \<And>nat. \<lbrakk>n < length lm; 0 < s; s mod 2 = Suc 0; s \<le> 2 * n; mopup_bef_erase_a (s, l, Bk # xs) lm n ires; \<not> Suc (Suc s) \<le> 2 * n; n = Suc nat\<rbrakk> \<Longrightarrow> mopup_jump_over1 (s', Bk # l, xs) lm n ires
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
n < length lm
0 < s
s mod 2 = Suc 0
s \<le> 2 * n
mopup_bef_erase_a (s, l, Bk # xs) lm n ires
\<not> Suc (Suc s) \<le> 2 * n
[PROOF STEP]
obtain a lm' where Cons:"lm = Cons a lm'"
[PROOF STATE]
proof (prove)
using this:
n < length lm
0 < s
s mod 2 = Suc 0
s \<le> 2 * n
mopup_bef_erase_a (s, l, Bk # xs) lm n ires
\<not> Suc (Suc s) \<le> 2 * n

goal (1 subgoal):
 1. (\<And>a lm'. lm = a # lm' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (cases lm,auto)
[PROOF STATE]
proof (state)
this:
lm = a # lm'

goal (2 subgoals):
 1. \<lbrakk>n < length lm; 0 < s; s mod 2 = Suc 0; s \<le> 2 * n; mopup_bef_erase_a (s, l, Bk # xs) lm n ires; \<not> Suc (Suc s) \<le> 2 * n; n = 0\<rbrakk> \<Longrightarrow> mopup_jump_over1 (s', Bk # l, xs) lm n ires
 2. \<And>nat. \<lbrakk>n < length lm; 0 < s; s mod 2 = Suc 0; s \<le> 2 * n; mopup_bef_erase_a (s, l, Bk # xs) lm n ires; \<not> Suc (Suc s) \<le> 2 * n; n = Suc nat\<rbrakk> \<Longrightarrow> mopup_jump_over1 (s', Bk # l, xs) lm n ires
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
n < length lm
0 < s
s mod 2 = Suc 0
s \<le> 2 * n
mopup_bef_erase_a (s, l, Bk # xs) lm n ires
\<not> Suc (Suc s) \<le> 2 * n
[PROOF STEP]
have n:"Suc s div 2 = n"
[PROOF STATE]
proof (prove)
using this:
n < length lm
0 < s
s mod 2 = Suc 0
s \<le> 2 * n
mopup_bef_erase_a (s, l, Bk # xs) lm n ires
\<not> Suc (Suc s) \<le> 2 * n

goal (1 subgoal):
 1. Suc s div 2 = n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Suc s div 2 = n

goal (2 subgoals):
 1. \<lbrakk>n < length lm; 0 < s; s mod 2 = Suc 0; s \<le> 2 * n; mopup_bef_erase_a (s, l, Bk # xs) lm n ires; \<not> Suc (Suc s) \<le> 2 * n; n = 0\<rbrakk> \<Longrightarrow> mopup_jump_over1 (s', Bk # l, xs) lm n ires
 2. \<And>nat. \<lbrakk>n < length lm; 0 < s; s mod 2 = Suc 0; s \<le> 2 * n; mopup_bef_erase_a (s, l, Bk # xs) lm n ires; \<not> Suc (Suc s) \<le> 2 * n; n = Suc nat\<rbrakk> \<Longrightarrow> mopup_jump_over1 (s', Bk # l, xs) lm n ires
[PROOF STEP]
have [simp]:"s = Suc (2 * q) \<longleftrightarrow> q = nat" for q
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (s = Suc (2 * q)) = (q = nat)
[PROOF STEP]
using assms Suc
[PROOF STATE]
proof (prove)
using this:
n < length lm
0 < s
s mod 2 = Suc 0
s \<le> 2 * n
mopup_bef_erase_a (s, l, Bk # xs) lm n ires
\<not> Suc (Suc s) \<le> 2 * n
n = Suc nat

goal (1 subgoal):
 1. (s = Suc (2 * q)) = (q = nat)
[PROOF STEP]
by presburger
[PROOF STATE]
proof (state)
this:
(s = Suc (2 * ?q)) = (?q = nat)

goal (2 subgoals):
 1. \<lbrakk>n < length lm; 0 < s; s mod 2 = Suc 0; s \<le> 2 * n; mopup_bef_erase_a (s, l, Bk # xs) lm n ires; \<not> Suc (Suc s) \<le> 2 * n; n = 0\<rbrakk> \<Longrightarrow> mopup_jump_over1 (s', Bk # l, xs) lm n ires
 2. \<And>nat. \<lbrakk>n < length lm; 0 < s; s mod 2 = Suc 0; s \<le> 2 * n; mopup_bef_erase_a (s, l, Bk # xs) lm n ires; \<not> Suc (Suc s) \<le> 2 * n; n = Suc nat\<rbrakk> \<Longrightarrow> mopup_jump_over1 (s', Bk # l, xs) lm n ires
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
n < length lm
0 < s
s mod 2 = Suc 0
s \<le> 2 * n
mopup_bef_erase_a (s, l, Bk # xs) lm n ires
\<not> Suc (Suc s) \<le> 2 * n
[PROOF STEP]
obtain ln m rn where ln:"l = Bk \<up> ln @ Bk # Bk # ires"
    and "Bk # xs = Oc \<up> m @ Bk # <drop (Suc s div 2) lm> @ Bk \<up> rn"
[PROOF STATE]
proof (prove)
using this:
n < length lm
0 < s
s mod 2 = Suc 0
s \<le> 2 * n
mopup_bef_erase_a (s, l, Bk # xs) lm n ires
\<not> Suc (Suc s) \<le> 2 * n

goal (1 subgoal):
 1. (\<And>ln m rn. \<lbrakk>l = Bk \<up> ln @ Bk # Bk # ires; Bk # xs = Oc \<up> m @ Bk # <drop (Suc s div 2) lm> @ Bk \<up> rn\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp: mopup_bef_erase_a.simps mopup_jump_over1.simps)
[PROOF STATE]
proof (state)
this:
l = Bk \<up> ln @ Bk # Bk # ires
Bk # xs = Oc \<up> m @ Bk # <drop (Suc s div 2) lm> @ Bk \<up> rn

goal (2 subgoals):
 1. \<lbrakk>n < length lm; 0 < s; s mod 2 = Suc 0; s \<le> 2 * n; mopup_bef_erase_a (s, l, Bk # xs) lm n ires; \<not> Suc (Suc s) \<le> 2 * n; n = 0\<rbrakk> \<Longrightarrow> mopup_jump_over1 (s', Bk # l, xs) lm n ires
 2. \<And>nat. \<lbrakk>n < length lm; 0 < s; s mod 2 = Suc 0; s \<le> 2 * n; mopup_bef_erase_a (s, l, Bk # xs) lm n ires; \<not> Suc (Suc s) \<le> 2 * n; n = Suc nat\<rbrakk> \<Longrightarrow> mopup_jump_over1 (s', Bk # l, xs) lm n ires
[PROOF STEP]
hence xs:"xs = <drop n lm> @ Bk \<up> rn"
[PROOF STATE]
proof (prove)
using this:
l = Bk \<up> ln @ Bk # Bk # ires
Bk # xs = Oc \<up> m @ Bk # <drop (Suc s div 2) lm> @ Bk \<up> rn

goal (1 subgoal):
 1. xs = <drop n lm> @ Bk \<up> rn
[PROOF STEP]
by(cases m;auto simp: n mod_ex1)
[PROOF STATE]
proof (state)
this:
xs = <drop n lm> @ Bk \<up> rn

goal (2 subgoals):
 1. \<lbrakk>n < length lm; 0 < s; s mod 2 = Suc 0; s \<le> 2 * n; mopup_bef_erase_a (s, l, Bk # xs) lm n ires; \<not> Suc (Suc s) \<le> 2 * n; n = 0\<rbrakk> \<Longrightarrow> mopup_jump_over1 (s', Bk # l, xs) lm n ires
 2. \<And>nat. \<lbrakk>n < length lm; 0 < s; s mod 2 = Suc 0; s \<le> 2 * n; mopup_bef_erase_a (s, l, Bk # xs) lm n ires; \<not> Suc (Suc s) \<le> 2 * n; n = Suc nat\<rbrakk> \<Longrightarrow> mopup_jump_over1 (s', Bk # l, xs) lm n ires
[PROOF STEP]
have [intro]:"nat < length lm' \<Longrightarrow>
    \<forall>rna. xs \<noteq> Oc # Oc \<up> (lm' ! nat) @ Bk # <drop (Suc nat) lm'> @ Bk \<up> rna \<Longrightarrow>
    <drop nat lm'> @ Bk \<up> rn = Oc # Oc \<up> (lm' ! nat)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>nat < length lm'; \<forall>rna. xs \<noteq> Oc # Oc \<up> lm' ! nat @ Bk # <drop (Suc nat) lm'> @ Bk \<up> rna\<rbrakk> \<Longrightarrow> <drop nat lm'> @ Bk \<up> rn = Oc # Oc \<up> lm' ! nat
[PROOF STEP]
by(cases rn, auto elim: erase2jumpover1 erase2jumpover2 simp:xs Suc Cons)
[PROOF STATE]
proof (state)
this:
\<lbrakk>nat < length lm'; \<forall>rna. xs \<noteq> Oc # Oc \<up> lm' ! nat @ Bk # <drop (Suc nat) lm'> @ Bk \<up> rna\<rbrakk> \<Longrightarrow> <drop nat lm'> @ Bk \<up> rn = Oc # Oc \<up> lm' ! nat

goal (2 subgoals):
 1. \<lbrakk>n < length lm; 0 < s; s mod 2 = Suc 0; s \<le> 2 * n; mopup_bef_erase_a (s, l, Bk # xs) lm n ires; \<not> Suc (Suc s) \<le> 2 * n; n = 0\<rbrakk> \<Longrightarrow> mopup_jump_over1 (s', Bk # l, xs) lm n ires
 2. \<And>nat. \<lbrakk>n < length lm; 0 < s; s mod 2 = Suc 0; s \<le> 2 * n; mopup_bef_erase_a (s, l, Bk # xs) lm n ires; \<not> Suc (Suc s) \<le> 2 * n; n = Suc nat\<rbrakk> \<Longrightarrow> mopup_jump_over1 (s', Bk # l, xs) lm n ires
[PROOF STEP]
have [intro]:"<drop nat lm'> \<noteq> Oc # Oc \<up> (lm' ! nat) @ Bk # <drop (Suc nat) lm'> @ Bk \<up> 0 \<Longrightarrow> length lm' \<le> Suc nat"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. <drop nat lm'> \<noteq> Oc # Oc \<up> lm' ! nat @ Bk # <drop (Suc nat) lm'> @ Bk \<up> 0 \<Longrightarrow> length lm' \<le> Suc nat
[PROOF STEP]
using drop_tape_of_cons[of nat lm']
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>Suc nat < length lm'; ?x = lm' ! nat\<rbrakk> \<Longrightarrow> <drop nat lm'> = Oc # Oc \<up> ?x @ Bk # <drop (Suc nat) lm'>

goal (1 subgoal):
 1. <drop nat lm'> \<noteq> Oc # Oc \<up> lm' ! nat @ Bk # <drop (Suc nat) lm'> @ Bk \<up> 0 \<Longrightarrow> length lm' \<le> Suc nat
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
<drop nat lm'> \<noteq> Oc # Oc \<up> lm' ! nat @ Bk # <drop (Suc nat) lm'> @ Bk \<up> 0 \<Longrightarrow> length lm' \<le> Suc nat

goal (2 subgoals):
 1. \<lbrakk>n < length lm; 0 < s; s mod 2 = Suc 0; s \<le> 2 * n; mopup_bef_erase_a (s, l, Bk # xs) lm n ires; \<not> Suc (Suc s) \<le> 2 * n; n = 0\<rbrakk> \<Longrightarrow> mopup_jump_over1 (s', Bk # l, xs) lm n ires
 2. \<And>nat. \<lbrakk>n < length lm; 0 < s; s mod 2 = Suc 0; s \<le> 2 * n; mopup_bef_erase_a (s, l, Bk # xs) lm n ires; \<not> Suc (Suc s) \<le> 2 * n; n = Suc nat\<rbrakk> \<Longrightarrow> mopup_jump_over1 (s', Bk # l, xs) lm n ires
[PROOF STEP]
from assms(1,3)
[PROOF STATE]
proof (chain)
picking this:
n < length lm
s mod 2 = Suc 0
[PROOF STEP]
have [intro!]:"
            0 + Suc (lm' ! nat) = Suc (lm' ! nat) \<and>
            Bk # Bk \<up> ln = Oc \<up> 0 @ Bk \<up> Suc ln \<and>
            ((\<exists>rna. xs = Oc \<up> Suc (lm' ! nat) @ Bk # <drop (Suc nat) lm'> @ Bk \<up> rna) \<or>
             xs = Oc \<up> Suc (lm' ! nat) \<and> length lm' \<le> Suc nat)"
[PROOF STATE]
proof (prove)
using this:
n < length lm
s mod 2 = Suc 0

goal (1 subgoal):
 1. 0 + Suc (lm' ! nat) = Suc (lm' ! nat) \<and> Bk # Bk \<up> ln = Oc \<up> 0 @ Bk \<up> Suc ln \<and> ((\<exists>rna. xs = Oc \<up> Suc (lm' ! nat) @ Bk # <drop (Suc nat) lm'> @ Bk \<up> rna) \<or> xs = Oc \<up> Suc (lm' ! nat) \<and> length lm' \<le> Suc nat)
[PROOF STEP]
by (auto simp:Cons ln xs Suc)
[PROOF STATE]
proof (state)
this:
0 + Suc (lm' ! nat) = Suc (lm' ! nat) \<and> Bk # Bk \<up> ln = Oc \<up> 0 @ Bk \<up> Suc ln \<and> ((\<exists>rna. xs = Oc \<up> Suc (lm' ! nat) @ Bk # <drop (Suc nat) lm'> @ Bk \<up> rna) \<or> xs = Oc \<up> Suc (lm' ! nat) \<and> length lm' \<le> Suc nat)

goal (2 subgoals):
 1. \<lbrakk>n < length lm; 0 < s; s mod 2 = Suc 0; s \<le> 2 * n; mopup_bef_erase_a (s, l, Bk # xs) lm n ires; \<not> Suc (Suc s) \<le> 2 * n; n = 0\<rbrakk> \<Longrightarrow> mopup_jump_over1 (s', Bk # l, xs) lm n ires
 2. \<And>nat. \<lbrakk>n < length lm; 0 < s; s mod 2 = Suc 0; s \<le> 2 * n; mopup_bef_erase_a (s, l, Bk # xs) lm n ires; \<not> Suc (Suc s) \<le> 2 * n; n = Suc nat\<rbrakk> \<Longrightarrow> mopup_jump_over1 (s', Bk # l, xs) lm n ires
[PROOF STEP]
from assms(1,3)
[PROOF STATE]
proof (chain)
picking this:
n < length lm
s mod 2 = Suc 0
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
n < length lm
s mod 2 = Suc 0

goal (1 subgoal):
 1. mopup_jump_over1 (s', Bk # l, xs) lm n ires
[PROOF STEP]
unfolding Cons ln Suc
[PROOF STATE]
proof (prove)
using this:
Suc nat < length (a # lm')
s mod 2 = Suc 0

goal (1 subgoal):
 1. mopup_jump_over1 (s', Bk # Bk \<up> ln @ Bk # Bk # ires, xs) (a # lm') (Suc nat) ires
[PROOF STEP]
by(auto simp: mopup_bef_erase_a.simps mopup_jump_over1.simps simp del:split_head_repeat)
[PROOF STATE]
proof (state)
this:
mopup_jump_over1 (s', Bk # l, xs) lm n ires

goal (1 subgoal):
 1. \<lbrakk>n < length lm; 0 < s; s mod 2 = Suc 0; s \<le> 2 * n; mopup_bef_erase_a (s, l, Bk # xs) lm n ires; \<not> Suc (Suc s) \<le> 2 * n; n = 0\<rbrakk> \<Longrightarrow> mopup_jump_over1 (s', Bk # l, xs) lm n ires
[PROOF STEP]
qed auto


[STATEMENT]
lemma Suc_Suc_div:  "\<lbrakk>0 < s; s mod 2 = Suc 0; Suc (Suc s) \<le> 2 * n\<rbrakk>
           \<Longrightarrow> (Suc (Suc (s div 2))) \<le> n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < s; s mod 2 = Suc 0; Suc (Suc s) \<le> 2 * n\<rbrakk> \<Longrightarrow> Suc (Suc (s div 2)) \<le> n
[PROOF STEP]
by(arith)


[STATEMENT]
lemma mopup_bef_erase_a_2_a[simp]:
  assumes "n < length lm" "0 < s" "s mod 2 = Suc 0"
    "mopup_bef_erase_a (s, l, Bk # xs) lm n ires"
    "Suc (Suc s) \<le> 2 * n"
  shows "mopup_bef_erase_a (Suc (Suc s), Bk # l, xs) lm n ires"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mopup_bef_erase_a (Suc (Suc s), Bk # l, xs) lm n ires
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. mopup_bef_erase_a (Suc (Suc s), Bk # l, xs) lm n ires
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
n < length lm
0 < s
s mod 2 = Suc 0
mopup_bef_erase_a (s, l, Bk # xs) lm n ires
Suc (Suc s) \<le> 2 * n
[PROOF STEP]
obtain rn m ln where
    rn:"l = Bk \<up> ln @ Bk # Bk # ires" "Bk # xs = Oc \<up> m @ Bk # <drop (Suc s div 2) lm> @ Bk \<up> rn"
[PROOF STATE]
proof (prove)
using this:
n < length lm
0 < s
s mod 2 = Suc 0
mopup_bef_erase_a (s, l, Bk # xs) lm n ires
Suc (Suc s) \<le> 2 * n

goal (1 subgoal):
 1. (\<And>ln m rn. \<lbrakk>l = Bk \<up> ln @ Bk # Bk # ires; Bk # xs = Oc \<up> m @ Bk # <drop (Suc s div 2) lm> @ Bk \<up> rn\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp: mopup_bef_erase_a.simps)
[PROOF STATE]
proof (state)
this:
l = Bk \<up> ln @ Bk # Bk # ires
Bk # xs = Oc \<up> m @ Bk # <drop (Suc s div 2) lm> @ Bk \<up> rn

goal (1 subgoal):
 1. mopup_bef_erase_a (Suc (Suc s), Bk # l, xs) lm n ires
[PROOF STEP]
hence m:"m = 0"
[PROOF STATE]
proof (prove)
using this:
l = Bk \<up> ln @ Bk # Bk # ires
Bk # xs = Oc \<up> m @ Bk # <drop (Suc s div 2) lm> @ Bk \<up> rn

goal (1 subgoal):
 1. m = 0
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
l = Bk \<up> ln @ Bk # Bk # ires
Bk # xs = Oc \<up> m @ Bk # <drop (Suc s div 2) lm> @ Bk \<up> rn
n < length lm
0 < s
s mod 2 = Suc 0
mopup_bef_erase_a (s, l, Bk # xs) lm n ires
Suc (Suc s) \<le> 2 * n

goal (1 subgoal):
 1. m = 0
[PROOF STEP]
by (cases m,auto)
[PROOF STATE]
proof (state)
this:
m = 0

goal (1 subgoal):
 1. mopup_bef_erase_a (Suc (Suc s), Bk # l, xs) lm n ires
[PROOF STEP]
hence d:"drop (Suc (Suc (s div 2))) lm \<noteq> []"
[PROOF STATE]
proof (prove)
using this:
m = 0

goal (1 subgoal):
 1. drop (Suc (Suc (s div 2))) lm \<noteq> []
[PROOF STEP]
using assms(1,3,5)
[PROOF STATE]
proof (prove)
using this:
m = 0
n < length lm
s mod 2 = Suc 0
Suc (Suc s) \<le> 2 * n

goal (1 subgoal):
 1. drop (Suc (Suc (s div 2))) lm \<noteq> []
[PROOF STEP]
by auto arith
[PROOF STATE]
proof (state)
this:
drop (Suc (Suc (s div 2))) lm \<noteq> []

goal (1 subgoal):
 1. mopup_bef_erase_a (Suc (Suc s), Bk # l, xs) lm n ires
[PROOF STEP]
hence "Bk # l = Bk \<up> Suc ln @ Bk # Bk # ires \<and>
    xs = Oc \<up> Suc (lm ! (Suc s div 2)) @ Bk # <drop ((Suc (Suc s) + 1) div 2) lm> @ Bk \<up> rn"
[PROOF STATE]
proof (prove)
using this:
drop (Suc (Suc (s div 2))) lm \<noteq> []

goal (1 subgoal):
 1. Bk # l = Bk \<up> Suc ln @ Bk # Bk # ires \<and> xs = Oc \<up> Suc (lm ! (Suc s div 2)) @ Bk # <drop ((Suc (Suc s) + 1) div 2) lm> @ Bk \<up> rn
[PROOF STEP]
using rn
[PROOF STATE]
proof (prove)
using this:
drop (Suc (Suc (s div 2))) lm \<noteq> []
l = Bk \<up> ln @ Bk # Bk # ires
Bk # xs = Oc \<up> m @ Bk # <drop (Suc s div 2) lm> @ Bk \<up> rn

goal (1 subgoal):
 1. Bk # l = Bk \<up> Suc ln @ Bk # Bk # ires \<and> xs = Oc \<up> Suc (lm ! (Suc s div 2)) @ Bk # <drop ((Suc (Suc s) + 1) div 2) lm> @ Bk \<up> rn
[PROOF STEP]
by(auto intro:drop_tape_of_cons simp:m)
[PROOF STATE]
proof (state)
this:
Bk # l = Bk \<up> Suc ln @ Bk # Bk # ires \<and> xs = Oc \<up> Suc (lm ! (Suc s div 2)) @ Bk # <drop ((Suc (Suc s) + 1) div 2) lm> @ Bk \<up> rn

goal (1 subgoal):
 1. mopup_bef_erase_a (Suc (Suc s), Bk # l, xs) lm n ires
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
Bk # l = Bk \<up> Suc ln @ Bk # Bk # ires \<and> xs = Oc \<up> Suc (lm ! (Suc s div 2)) @ Bk # <drop ((Suc (Suc s) + 1) div 2) lm> @ Bk \<up> rn

goal (1 subgoal):
 1. mopup_bef_erase_a (Suc (Suc s), Bk # l, xs) lm n ires
[PROOF STEP]
unfolding mopup_bef_erase_a.simps
[PROOF STATE]
proof (prove)
using this:
Bk # l = Bk \<up> Suc ln @ Bk # Bk # ires \<and> xs = Oc \<up> Suc (lm ! (Suc s div 2)) @ Bk # <drop ((Suc (Suc s) + 1) div 2) lm> @ Bk \<up> rn

goal (1 subgoal):
 1. \<exists>ln m rn. Bk # l = Bk \<up> ln @ Bk # Bk # ires \<and> xs = Oc \<up> m @ Bk # <drop ((Suc (Suc s) + 1) div 2) lm> @ Bk \<up> rn
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
mopup_bef_erase_a (Suc (Suc s), Bk # l, xs) lm n ires

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma mopup_false2:
  "\<lbrakk>0 < s; s \<le> 2 * n;
   s mod 2 = Suc 0; Suc s \<noteq> 2 * n;
   \<not> Suc (Suc s) \<le> 2 * n\<rbrakk> \<Longrightarrow> RR"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < s; s \<le> 2 * n; s mod 2 = Suc 0; Suc s \<noteq> 2 * n; \<not> Suc (Suc s) \<le> 2 * n\<rbrakk> \<Longrightarrow> RR
[PROOF STEP]
by(arith)


[STATEMENT]
lemma ariths[simp]: "\<lbrakk>0 < s; s \<le> 2 *n; s mod 2 \<noteq> Suc 0\<rbrakk> \<Longrightarrow>
                                      (s - Suc 0) mod 2 = Suc 0"
  "\<lbrakk>0 < s; s \<le> 2 *n; s mod 2 \<noteq> Suc 0\<rbrakk> \<Longrightarrow>
                                       s - Suc 0 \<le> 2 * n"
  "\<lbrakk>0 < s; s \<le> 2 *n; s mod 2 \<noteq> Suc 0\<rbrakk> \<Longrightarrow> \<not> s \<le> Suc 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lbrakk>0 < s; s \<le> 2 * n; s mod 2 \<noteq> Suc 0\<rbrakk> \<Longrightarrow> (s - Suc 0) mod 2 = Suc 0) &&& (\<lbrakk>0 < s; s \<le> 2 * n; s mod 2 \<noteq> Suc 0\<rbrakk> \<Longrightarrow> s - Suc 0 \<le> 2 * n) &&& (\<lbrakk>0 < s; s \<le> 2 * n; s mod 2 \<noteq> Suc 0\<rbrakk> \<Longrightarrow> \<not> s \<le> Suc 0)
[PROOF STEP]
by(arith)+


[STATEMENT]
lemma take_suc[intro]:
  "\<exists>lna. Bk # Bk \<up> ln = Bk \<up> lna"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>lna. Bk # Bk \<up> ln = Bk \<up> lna
[PROOF STEP]
by(rule_tac x = "Suc ln" in exI, simp)


[STATEMENT]
lemma mopup_bef_erase[simp]: "mopup_bef_erase_a (s, l, []) lm n ires \<Longrightarrow>
                        mopup_bef_erase_a (s, l, [Bk]) lm n ires"
  "\<lbrakk>n < length lm; 0 < s; s \<le> 2 * n; s mod 2 = Suc 0; \<not> Suc (Suc s) \<le> 2 *n;
     mopup_bef_erase_a (s, l, []) lm n ires\<rbrakk>
    \<Longrightarrow>  mopup_jump_over1 (s', Bk # l, []) lm n ires"
  "mopup_bef_erase_b (s, l, Oc # xs) lm n ires \<Longrightarrow> l \<noteq> []"
  "\<lbrakk>n < length lm; 0 < s; s \<le> 2 * n;
               s mod 2 \<noteq> Suc 0;
               mopup_bef_erase_b (s, l, Bk # xs) lm n ires; r = Bk # xs\<rbrakk>
           \<Longrightarrow> mopup_bef_erase_a (s - Suc 0, Bk # l, xs) lm n ires"
  "\<lbrakk>mopup_bef_erase_b (s, l, []) lm n ires\<rbrakk> \<Longrightarrow>
                   mopup_bef_erase_a (s - Suc 0, Bk # l, []) lm n ires"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((mopup_bef_erase_a (s, l, []) lm n ires \<Longrightarrow> mopup_bef_erase_a (s, l, [Bk]) lm n ires) &&& (\<lbrakk>n < length lm; 0 < s; s \<le> 2 * n; s mod 2 = Suc 0; \<not> Suc (Suc s) \<le> 2 * n; mopup_bef_erase_a (s, l, []) lm n ires\<rbrakk> \<Longrightarrow> mopup_jump_over1 (s', Bk # l, []) lm n ires)) &&& (mopup_bef_erase_b (s, l, Oc # xs) lm n ires \<Longrightarrow> l \<noteq> []) &&& (\<lbrakk>n < length lm; 0 < s; s \<le> 2 * n; s mod 2 \<noteq> Suc 0; mopup_bef_erase_b (s, l, Bk # xs) lm n ires; r = Bk # xs\<rbrakk> \<Longrightarrow> mopup_bef_erase_a (s - Suc 0, Bk # l, xs) lm n ires) &&& (mopup_bef_erase_b (s, l, []) lm n ires \<Longrightarrow> mopup_bef_erase_a (s - Suc 0, Bk # l, []) lm n ires)
[PROOF STEP]
by(auto simp: mopup_bef_erase_b.simps mopup_bef_erase_a.simps)


[STATEMENT]
lemma mopup_jump_over1_in_ctx[simp]:
  assumes "mopup_jump_over1 (Suc (2 * n), l, Oc # xs) lm n ires"
  shows "mopup_jump_over1 (Suc (2 * n), Oc # l, xs) lm n ires"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mopup_jump_over1 (Suc (2 * n), Oc # l, xs) lm n ires
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. mopup_jump_over1 (Suc (2 * n), Oc # l, xs) lm n ires
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
mopup_jump_over1 (Suc (2 * n), l, Oc # xs) lm n ires
[PROOF STEP]
obtain ln m1 m2 rn where
    "m1 + m2 = Suc (lm ! n)"
    "l = Oc \<up> m1 @ Bk \<up> ln @ Bk # Bk # ires"
    "(Oc # xs = Oc \<up> m2 @ Bk # <drop (Suc n) lm> @ Bk \<up> rn \<or>
         Oc # xs = Oc \<up> m2 \<and> drop (Suc n) lm = [])"
[PROOF STATE]
proof (prove)
using this:
mopup_jump_over1 (Suc (2 * n), l, Oc # xs) lm n ires

goal (1 subgoal):
 1. (\<And>m1 m2 ln rn. \<lbrakk>m1 + m2 = Suc (lm ! n); l = Oc \<up> m1 @ Bk \<up> ln @ Bk # Bk # ires; Oc # xs = Oc \<up> m2 @ Bk # <drop (Suc n) lm> @ Bk \<up> rn \<or> Oc # xs = Oc \<up> m2 \<and> drop (Suc n) lm = []\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding mopup_jump_over1.simps
[PROOF STATE]
proof (prove)
using this:
\<exists>ln m1 m2 rn. m1 + m2 = Suc (lm ! n) \<and> l = Oc \<up> m1 @ Bk \<up> ln @ Bk # Bk # ires \<and> (Oc # xs = Oc \<up> m2 @ Bk # <drop (Suc n) lm> @ Bk \<up> rn \<or> Oc # xs = Oc \<up> m2 \<and> drop (Suc n) lm = [])

goal (1 subgoal):
 1. (\<And>m1 m2 ln rn. \<lbrakk>m1 + m2 = Suc (lm ! n); l = Oc \<up> m1 @ Bk \<up> ln @ Bk # Bk # ires; Oc # xs = Oc \<up> m2 @ Bk # <drop (Suc n) lm> @ Bk \<up> rn \<or> Oc # xs = Oc \<up> m2 \<and> drop (Suc n) lm = []\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
m1 + m2 = Suc (lm ! n)
l = Oc \<up> m1 @ Bk \<up> ln @ Bk # Bk # ires
Oc # xs = Oc \<up> m2 @ Bk # <drop (Suc n) lm> @ Bk \<up> rn \<or> Oc # xs = Oc \<up> m2 \<and> drop (Suc n) lm = []

goal (1 subgoal):
 1. mopup_jump_over1 (Suc (2 * n), Oc # l, xs) lm n ires
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
m1 + m2 = Suc (lm ! n)
l = Oc \<up> m1 @ Bk \<up> ln @ Bk # Bk # ires
Oc # xs = Oc \<up> m2 @ Bk # <drop (Suc n) lm> @ Bk \<up> rn \<or> Oc # xs = Oc \<up> m2 \<and> drop (Suc n) lm = []

goal (1 subgoal):
 1. mopup_jump_over1 (Suc (2 * n), Oc # l, xs) lm n ires
[PROOF STEP]
unfolding mopup_jump_over1.simps
[PROOF STATE]
proof (prove)
using this:
m1 + m2 = Suc (lm ! n)
l = Oc \<up> m1 @ Bk \<up> ln @ Bk # Bk # ires
Oc # xs = Oc \<up> m2 @ Bk # <drop (Suc n) lm> @ Bk \<up> rn \<or> Oc # xs = Oc \<up> m2 \<and> drop (Suc n) lm = []

goal (1 subgoal):
 1. \<exists>ln m1 m2 rn. m1 + m2 = Suc (lm ! n) \<and> Oc # l = Oc \<up> m1 @ Bk \<up> ln @ Bk # Bk # ires \<and> (xs = Oc \<up> m2 @ Bk # <drop (Suc n) lm> @ Bk \<up> rn \<or> xs = Oc \<up> m2 \<and> drop (Suc n) lm = [])
[PROOF STEP]
apply(rule_tac x = ln in exI, rule_tac x = "Suc m1" in exI
        ,rule_tac x = "m2 - 1" in exI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m1 + m2 = Suc (lm ! n); l = Oc \<up> m1 @ Bk \<up> ln @ Bk # Bk # ires; Oc # xs = Oc \<up> m2 @ Bk # <drop (Suc n) lm> @ Bk \<up> rn \<or> Oc # xs = Oc \<up> m2 \<and> drop (Suc n) lm = []; m1 + m2 = Suc (lm ! n); l = Oc \<up> m1 @ Bk \<up> ln @ Bk # Bk # ires; Oc # xs = Oc \<up> m2 @ Bk # <drop (Suc n) lm> @ Bk \<up> rn \<or> Oc # xs = Oc \<up> m2 \<and> drop (Suc n) lm = []; m1 + m2 = Suc (lm ! n); l = Oc \<up> m1 @ Bk \<up> ln @ Bk # Bk # ires; Oc # xs = Oc \<up> m2 @ Bk # <drop (Suc n) lm> @ Bk \<up> rn \<or> Oc # xs = Oc \<up> m2 \<and> drop (Suc n) lm = []\<rbrakk> \<Longrightarrow> \<exists>rn. Suc m1 + (m2 - 1) = Suc (lm ! n) \<and> Oc # l = Oc \<up> Suc m1 @ Bk \<up> ln @ Bk # Bk # ires \<and> (xs = Oc \<up> (m2 - 1) @ Bk # <drop (Suc n) lm> @ Bk \<up> rn \<or> xs = Oc \<up> (m2 - 1) \<and> drop (Suc n) lm = [])
[PROOF STEP]
by(cases "m2", auto)
[PROOF STATE]
proof (state)
this:
mopup_jump_over1 (Suc (2 * n), Oc # l, xs) lm n ires

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma mopup_jump_over1_2_aft_erase_a[simp]:
  assumes "mopup_jump_over1 (Suc (2 * n), l, Bk # xs) lm n ires"
  shows "mopup_aft_erase_a (Suc (Suc (2 * n)), Bk # l, xs) lm n ires"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mopup_aft_erase_a (Suc (Suc (2 * n)), Bk # l, xs) lm n ires
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. mopup_aft_erase_a (Suc (Suc (2 * n)), Bk # l, xs) lm n ires
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
mopup_jump_over1 (Suc (2 * n), l, Bk # xs) lm n ires
[PROOF STEP]
obtain ln m1 m2 rn where
    "m1 + m2 = Suc (lm ! n)"
    "l = Oc \<up> m1 @ Bk \<up> ln @ Bk # Bk # ires"
    "(Bk # xs = Oc \<up> m2 @ Bk # <drop (Suc n) lm> @ Bk \<up> rn \<or>
        Bk # xs = Oc \<up> m2 \<and> drop (Suc n) lm = [])"
[PROOF STATE]
proof (prove)
using this:
mopup_jump_over1 (Suc (2 * n), l, Bk # xs) lm n ires

goal (1 subgoal):
 1. (\<And>m1 m2 ln rn. \<lbrakk>m1 + m2 = Suc (lm ! n); l = Oc \<up> m1 @ Bk \<up> ln @ Bk # Bk # ires; Bk # xs = Oc \<up> m2 @ Bk # <drop (Suc n) lm> @ Bk \<up> rn \<or> Bk # xs = Oc \<up> m2 \<and> drop (Suc n) lm = []\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding mopup_jump_over1.simps
[PROOF STATE]
proof (prove)
using this:
\<exists>ln m1 m2 rn. m1 + m2 = Suc (lm ! n) \<and> l = Oc \<up> m1 @ Bk \<up> ln @ Bk # Bk # ires \<and> (Bk # xs = Oc \<up> m2 @ Bk # <drop (Suc n) lm> @ Bk \<up> rn \<or> Bk # xs = Oc \<up> m2 \<and> drop (Suc n) lm = [])

goal (1 subgoal):
 1. (\<And>m1 m2 ln rn. \<lbrakk>m1 + m2 = Suc (lm ! n); l = Oc \<up> m1 @ Bk \<up> ln @ Bk # Bk # ires; Bk # xs = Oc \<up> m2 @ Bk # <drop (Suc n) lm> @ Bk \<up> rn \<or> Bk # xs = Oc \<up> m2 \<and> drop (Suc n) lm = []\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
m1 + m2 = Suc (lm ! n)
l = Oc \<up> m1 @ Bk \<up> ln @ Bk # Bk # ires
Bk # xs = Oc \<up> m2 @ Bk # <drop (Suc n) lm> @ Bk \<up> rn \<or> Bk # xs = Oc \<up> m2 \<and> drop (Suc n) lm = []

goal (1 subgoal):
 1. mopup_aft_erase_a (Suc (Suc (2 * n)), Bk # l, xs) lm n ires
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
m1 + m2 = Suc (lm ! n)
l = Oc \<up> m1 @ Bk \<up> ln @ Bk # Bk # ires
Bk # xs = Oc \<up> m2 @ Bk # <drop (Suc n) lm> @ Bk \<up> rn \<or> Bk # xs = Oc \<up> m2 \<and> drop (Suc n) lm = []

goal (1 subgoal):
 1. mopup_aft_erase_a (Suc (Suc (2 * n)), Bk # l, xs) lm n ires
[PROOF STEP]
unfolding mopup_aft_erase_a.simps
[PROOF STATE]
proof (prove)
using this:
m1 + m2 = Suc (lm ! n)
l = Oc \<up> m1 @ Bk \<up> ln @ Bk # Bk # ires
Bk # xs = Oc \<up> m2 @ Bk # <drop (Suc n) lm> @ Bk \<up> rn \<or> Bk # xs = Oc \<up> m2 \<and> drop (Suc n) lm = []

goal (1 subgoal):
 1. \<exists>lnl lnr rn ml m. m = Suc (lm ! n) \<and> Bk # l = Bk \<up> lnr @ Oc \<up> m @ Bk \<up> lnl @ Bk # Bk # ires \<and> xs = <ml> @ Bk \<up> rn
[PROOF STEP]
apply( rule_tac x = ln in exI, rule_tac x = "Suc 0" in exI,rule_tac x = rn in exI
        , rule_tac x = "drop (Suc n) lm" in exI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m1 + m2 = Suc (lm ! n); l = Oc \<up> m1 @ Bk \<up> ln @ Bk # Bk # ires; Bk # xs = Oc \<up> m2 @ Bk # <drop (Suc n) lm> @ Bk \<up> rn \<or> Bk # xs = Oc \<up> m2 \<and> drop (Suc n) lm = []; m1 + m2 = Suc (lm ! n); l = Oc \<up> m1 @ Bk \<up> ln @ Bk # Bk # ires; Bk # xs = Oc \<up> m2 @ Bk # <drop (Suc n) lm> @ Bk \<up> rn \<or> Bk # xs = Oc \<up> m2 \<and> drop (Suc n) lm = []; m1 + m2 = Suc (lm ! n); l = Oc \<up> m1 @ Bk \<up> ln @ Bk # Bk # ires; Bk # xs = Oc \<up> m2 @ Bk # <drop (Suc n) lm> @ Bk \<up> rn \<or> Bk # xs = Oc \<up> m2 \<and> drop (Suc n) lm = []; m1 + m2 = Suc (lm ! n); l = Oc \<up> m1 @ Bk \<up> ln @ Bk # Bk # ires; Bk # xs = Oc \<up> m2 @ Bk # <drop (Suc n) lm> @ Bk \<up> rn \<or> Bk # xs = Oc \<up> m2 \<and> drop (Suc n) lm = []\<rbrakk> \<Longrightarrow> \<exists>m. m = Suc (lm ! n) \<and> Bk # l = Bk \<up> Suc 0 @ Oc \<up> m @ Bk \<up> ln @ Bk # Bk # ires \<and> xs = <drop (Suc n) lm> @ Bk \<up> rn
[PROOF STEP]
by(cases m2, auto)
[PROOF STATE]
proof (state)
this:
mopup_aft_erase_a (Suc (Suc (2 * n)), Bk # l, xs) lm n ires

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma mopup_aft_erase_a_via_jump_over1[simp]:
  "\<lbrakk>mopup_jump_over1 (Suc (2 * n), l, []) lm n ires\<rbrakk> \<Longrightarrow>
    mopup_aft_erase_a (Suc (Suc (2 * n)), Bk # l, []) lm n ires"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mopup_jump_over1 (Suc (2 * n), l, []) lm n ires \<Longrightarrow> mopup_aft_erase_a (Suc (Suc (2 * n)), Bk # l, []) lm n ires
[PROOF STEP]
proof(rule mopup_jump_over1_2_aft_erase_a)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. mopup_jump_over1 (Suc (2 * n), l, []) lm n ires \<Longrightarrow> mopup_jump_over1 (Suc (2 * n), l, [Bk]) lm n ires
[PROOF STEP]
assume a:"mopup_jump_over1 (Suc (2 * n), l, []) lm n ires"
[PROOF STATE]
proof (state)
this:
mopup_jump_over1 (Suc (2 * n), l, []) lm n ires

goal (1 subgoal):
 1. mopup_jump_over1 (Suc (2 * n), l, []) lm n ires \<Longrightarrow> mopup_jump_over1 (Suc (2 * n), l, [Bk]) lm n ires
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
mopup_jump_over1 (Suc (2 * n), l, []) lm n ires
[PROOF STEP]
obtain ln where ln:"length lm \<le> Suc n \<Longrightarrow> l = Oc # Oc \<up> (lm ! n) @ Bk \<up> ln @ Bk # Bk # ires"
[PROOF STATE]
proof (prove)
using this:
mopup_jump_over1 (Suc (2 * n), l, []) lm n ires

goal (1 subgoal):
 1. (\<And>ln. (length lm \<le> Suc n \<Longrightarrow> l = Oc # Oc \<up> lm ! n @ Bk \<up> ln @ Bk # Bk # ires) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding mopup_jump_over1.simps
[PROOF STATE]
proof (prove)
using this:
\<exists>ln m1 m2 rn. m1 + m2 = Suc (lm ! n) \<and> l = Oc \<up> m1 @ Bk \<up> ln @ Bk # Bk # ires \<and> ([] = Oc \<up> m2 @ Bk # <drop (Suc n) lm> @ Bk \<up> rn \<or> [] = Oc \<up> m2 \<and> drop (Suc n) lm = [])

goal (1 subgoal):
 1. (\<And>ln. (length lm \<le> Suc n \<Longrightarrow> l = Oc # Oc \<up> lm ! n @ Bk \<up> ln @ Bk # Bk # ires) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
length lm \<le> Suc n \<Longrightarrow> l = Oc # Oc \<up> lm ! n @ Bk \<up> ln @ Bk # Bk # ires

goal (1 subgoal):
 1. mopup_jump_over1 (Suc (2 * n), l, []) lm n ires \<Longrightarrow> mopup_jump_over1 (Suc (2 * n), l, [Bk]) lm n ires
[PROOF STEP]
show "mopup_jump_over1 (Suc (2 * n), l, [Bk]) lm n ires"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mopup_jump_over1 (Suc (2 * n), l, [Bk]) lm n ires
[PROOF STEP]
unfolding mopup_jump_over1.simps
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>ln m1 m2 rn. m1 + m2 = Suc (lm ! n) \<and> l = Oc \<up> m1 @ Bk \<up> ln @ Bk # Bk # ires \<and> ([Bk] = Oc \<up> m2 @ Bk # <drop (Suc n) lm> @ Bk \<up> rn \<or> [Bk] = Oc \<up> m2 \<and> drop (Suc n) lm = [])
[PROOF STEP]
apply(rule_tac x = ln in exI, rule_tac x = "Suc (lm ! n)" in exI,
        rule_tac x = 0 in exI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>rn. Suc (lm ! n) + 0 = Suc (lm ! n) \<and> l = Oc \<up> Suc (lm ! n) @ Bk \<up> ln @ Bk # Bk # ires \<and> ([Bk] = Oc \<up> 0 @ Bk # <drop (Suc n) lm> @ Bk \<up> rn \<or> [Bk] = Oc \<up> 0 \<and> drop (Suc n) lm = [])
[PROOF STEP]
using a ln
[PROOF STATE]
proof (prove)
using this:
mopup_jump_over1 (Suc (2 * n), l, []) lm n ires
length lm \<le> Suc n \<Longrightarrow> l = Oc # Oc \<up> lm ! n @ Bk \<up> ln @ Bk # Bk # ires

goal (1 subgoal):
 1. \<exists>rn. Suc (lm ! n) + 0 = Suc (lm ! n) \<and> l = Oc \<up> Suc (lm ! n) @ Bk \<up> ln @ Bk # Bk # ires \<and> ([Bk] = Oc \<up> 0 @ Bk # <drop (Suc n) lm> @ Bk \<up> rn \<or> [Bk] = Oc \<up> 0 \<and> drop (Suc n) lm = [])
[PROOF STEP]
by(auto simp: mopup_jump_over1.simps tape_of_list_def )
[PROOF STATE]
proof (state)
this:
mopup_jump_over1 (Suc (2 * n), l, [Bk]) lm n ires

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma mopup_aft_erase_b_via_a[simp]:
  assumes "mopup_aft_erase_a (Suc (Suc (2 * n)), l, Oc # xs) lm n ires"
  shows "mopup_aft_erase_b (Suc (Suc (Suc (2 * n))), l, Bk # xs) lm n ires"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mopup_aft_erase_b (Suc (Suc (Suc (2 * n))), l, Bk # xs) lm n ires
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. mopup_aft_erase_b (Suc (Suc (Suc (2 * n))), l, Bk # xs) lm n ires
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
mopup_aft_erase_a (Suc (Suc (2 * n)), l, Oc # xs) lm n ires
[PROOF STEP]
obtain lnl lnr rn ml where
    assms:
    "l = Bk \<up> lnr @ Oc \<up> Suc (lm ! n) @ Bk \<up> lnl @ Bk # Bk # ires"
    "Oc # xs = <ml::nat list> @ Bk \<up> rn"
[PROOF STATE]
proof (prove)
using this:
mopup_aft_erase_a (Suc (Suc (2 * n)), l, Oc # xs) lm n ires

goal (1 subgoal):
 1. (\<And>lnr lnl ml rn. \<lbrakk>l = Bk \<up> lnr @ Oc \<up> Suc (lm ! n) @ Bk \<up> lnl @ Bk # Bk # ires; Oc # xs = <ml> @ Bk \<up> rn\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding mopup_aft_erase_a.simps
[PROOF STATE]
proof (prove)
using this:
\<exists>lnl lnr rn ml m. m = Suc (lm ! n) \<and> l = Bk \<up> lnr @ Oc \<up> m @ Bk \<up> lnl @ Bk # Bk # ires \<and> Oc # xs = <ml> @ Bk \<up> rn

goal (1 subgoal):
 1. (\<And>lnr lnl ml rn. \<lbrakk>l = Bk \<up> lnr @ Oc \<up> Suc (lm ! n) @ Bk \<up> lnl @ Bk # Bk # ires; Oc # xs = <ml> @ Bk \<up> rn\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
l = Bk \<up> lnr @ Oc \<up> Suc (lm ! n) @ Bk \<up> lnl @ Bk # Bk # ires
Oc # xs = <ml> @ Bk \<up> rn

goal (1 subgoal):
 1. mopup_aft_erase_b (Suc (Suc (Suc (2 * n))), l, Bk # xs) lm n ires
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
l = Bk \<up> lnr @ Oc \<up> Suc (lm ! n) @ Bk \<up> lnl @ Bk # Bk # ires
Oc # xs = <ml> @ Bk \<up> rn
[PROOF STEP]
obtain a list where ml:"ml = a # list"
[PROOF STATE]
proof (prove)
using this:
l = Bk \<up> lnr @ Oc \<up> Suc (lm ! n) @ Bk \<up> lnl @ Bk # Bk # ires
Oc # xs = <ml> @ Bk \<up> rn

goal (1 subgoal):
 1. (\<And>a list. ml = a # list \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (cases ml,cases rn,auto)
[PROOF STATE]
proof (state)
this:
ml = a # list

goal (1 subgoal):
 1. mopup_aft_erase_b (Suc (Suc (Suc (2 * n))), l, Bk # xs) lm n ires
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
l = Bk \<up> lnr @ Oc \<up> Suc (lm ! n) @ Bk \<up> lnl @ Bk # Bk # ires
Oc # xs = <ml> @ Bk \<up> rn
ml = a # list
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
l = Bk \<up> lnr @ Oc \<up> Suc (lm ! n) @ Bk \<up> lnl @ Bk # Bk # ires
Oc # xs = <ml> @ Bk \<up> rn
ml = a # list

goal (1 subgoal):
 1. mopup_aft_erase_b (Suc (Suc (Suc (2 * n))), l, Bk # xs) lm n ires
[PROOF STEP]
unfolding mopup_aft_erase_b.simps
[PROOF STATE]
proof (prove)
using this:
l = Bk \<up> lnr @ Oc \<up> Suc (lm ! n) @ Bk \<up> lnl @ Bk # Bk # ires
Oc # xs = <ml> @ Bk \<up> rn
ml = a # list

goal (1 subgoal):
 1. \<exists>lnl lnr rn ml m. m = Suc (lm ! n) \<and> l = Bk \<up> lnr @ Oc \<up> m @ Bk \<up> lnl @ Bk # Bk # ires \<and> (Bk # xs = Bk # <ml> @ Bk \<up> rn \<or> Bk # xs = Bk # Bk # <ml> @ Bk \<up> rn)
[PROOF STEP]
apply(auto simp add: tape_of_nl_cons split: if_splits)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ml = [a]; l = Bk \<up> lnr @ Oc # Oc \<up> lm ! n @ Bk \<up> lnl @ Bk # Bk # ires; list = []; xs = Oc \<up> a @ Bk \<up> rn\<rbrakk> \<Longrightarrow> \<exists>rna ml. Oc \<up> a @ Bk \<up> rn = <ml> @ Bk \<up> rna \<or> a = 0 \<and> Bk # <ml> @ Bk \<up> rna = Bk \<up> rn
 2. \<lbrakk>ml = a # list; l = Bk \<up> lnr @ Oc # Oc \<up> lm ! n @ Bk \<up> lnl @ Bk # Bk # ires; list \<noteq> []; xs = Oc \<up> a @ Bk # <list> @ Bk \<up> rn\<rbrakk> \<Longrightarrow> \<exists>rna ml. Oc \<up> a @ Bk # <list> @ Bk \<up> rn = <ml> @ Bk \<up> rna \<or> a = 0 \<and> <ml> @ Bk \<up> rna = <list> @ Bk \<up> rn
[PROOF STEP]
apply(cases a, simp_all)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>ml = [0]; l = Bk \<up> lnr @ Oc # Oc \<up> lm ! n @ Bk \<up> lnl @ Bk # Bk # ires; list = []; xs = Bk \<up> rn; a = 0\<rbrakk> \<Longrightarrow> \<exists>rna ml. Bk \<up> rn = <ml> @ Bk \<up> rna \<or> Bk # <ml> @ Bk \<up> rna = Bk \<up> rn
 2. \<And>nat. \<lbrakk>ml = [Suc nat]; l = Bk \<up> lnr @ Oc # Oc \<up> lm ! n @ Bk \<up> lnl @ Bk # Bk # ires; list = []; xs = Oc # Oc \<up> nat @ Bk \<up> rn; a = Suc nat\<rbrakk> \<Longrightarrow> \<exists>rna ml. Oc # Oc \<up> nat @ Bk \<up> rn = <ml> @ Bk \<up> rna
 3. \<lbrakk>ml = a # list; l = Bk \<up> lnr @ Oc # Oc \<up> lm ! n @ Bk \<up> lnl @ Bk # Bk # ires; list \<noteq> []; xs = Oc \<up> a @ Bk # <list> @ Bk \<up> rn\<rbrakk> \<Longrightarrow> \<exists>rna ml. Oc \<up> a @ Bk # <list> @ Bk \<up> rn = <ml> @ Bk \<up> rna \<or> a = 0 \<and> <ml> @ Bk \<up> rna = <list> @ Bk \<up> rn
[PROOF STEP]
apply(rule_tac x = rn in exI, rule_tac x = "[]" in exI, force)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>nat. \<lbrakk>ml = [Suc nat]; l = Bk \<up> lnr @ Oc # Oc \<up> lm ! n @ Bk \<up> lnl @ Bk # Bk # ires; list = []; xs = Oc # Oc \<up> nat @ Bk \<up> rn; a = Suc nat\<rbrakk> \<Longrightarrow> \<exists>rna ml. Oc # Oc \<up> nat @ Bk \<up> rn = <ml> @ Bk \<up> rna
 2. \<lbrakk>ml = a # list; l = Bk \<up> lnr @ Oc # Oc \<up> lm ! n @ Bk \<up> lnl @ Bk # Bk # ires; list \<noteq> []; xs = Oc \<up> a @ Bk # <list> @ Bk \<up> rn\<rbrakk> \<Longrightarrow> \<exists>rna ml. Oc \<up> a @ Bk # <list> @ Bk \<up> rn = <ml> @ Bk \<up> rna \<or> a = 0 \<and> <ml> @ Bk \<up> rna = <list> @ Bk \<up> rn
[PROOF STEP]
apply(rule_tac x = rn in exI, rule_tac x = "[a-1]" in exI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>nat. \<lbrakk>ml = [Suc nat]; l = Bk \<up> lnr @ Oc # Oc \<up> lm ! n @ Bk \<up> lnl @ Bk # Bk # ires; list = []; xs = Oc # Oc \<up> nat @ Bk \<up> rn; a = Suc nat\<rbrakk> \<Longrightarrow> Oc # Oc \<up> nat @ Bk \<up> rn = <[a - 1]> @ Bk \<up> rn
 2. \<lbrakk>ml = a # list; l = Bk \<up> lnr @ Oc # Oc \<up> lm ! n @ Bk \<up> lnl @ Bk # Bk # ires; list \<noteq> []; xs = Oc \<up> a @ Bk # <list> @ Bk \<up> rn\<rbrakk> \<Longrightarrow> \<exists>rna ml. Oc \<up> a @ Bk # <list> @ Bk \<up> rn = <ml> @ Bk \<up> rna \<or> a = 0 \<and> <ml> @ Bk \<up> rna = <list> @ Bk \<up> rn
[PROOF STEP]
apply(cases "a"; force simp add: tape_of_list_def tape_of_nat_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ml = a # list; l = Bk \<up> lnr @ Oc # Oc \<up> lm ! n @ Bk \<up> lnl @ Bk # Bk # ires; list \<noteq> []; xs = Oc \<up> a @ Bk # <list> @ Bk \<up> rn\<rbrakk> \<Longrightarrow> \<exists>rna ml. Oc \<up> a @ Bk # <list> @ Bk \<up> rn = <ml> @ Bk \<up> rna \<or> a = 0 \<and> <ml> @ Bk \<up> rna = <list> @ Bk \<up> rn
[PROOF STEP]
apply(cases "a")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ml = a # list; l = Bk \<up> lnr @ Oc # Oc \<up> lm ! n @ Bk \<up> lnl @ Bk # Bk # ires; list \<noteq> []; xs = Oc \<up> a @ Bk # <list> @ Bk \<up> rn; a = 0\<rbrakk> \<Longrightarrow> \<exists>rna ml. Oc \<up> a @ Bk # <list> @ Bk \<up> rn = <ml> @ Bk \<up> rna \<or> a = 0 \<and> <ml> @ Bk \<up> rna = <list> @ Bk \<up> rn
 2. \<And>nat. \<lbrakk>ml = a # list; l = Bk \<up> lnr @ Oc # Oc \<up> lm ! n @ Bk \<up> lnl @ Bk # Bk # ires; list \<noteq> []; xs = Oc \<up> a @ Bk # <list> @ Bk \<up> rn; a = Suc nat\<rbrakk> \<Longrightarrow> \<exists>rna ml. Oc \<up> a @ Bk # <list> @ Bk \<up> rn = <ml> @ Bk \<up> rna \<or> a = 0 \<and> <ml> @ Bk \<up> rna = <list> @ Bk \<up> rn
[PROOF STEP]
apply(rule_tac x = rn in exI, rule_tac x = list in exI, force)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>nat. \<lbrakk>ml = a # list; l = Bk \<up> lnr @ Oc # Oc \<up> lm ! n @ Bk \<up> lnl @ Bk # Bk # ires; list \<noteq> []; xs = Oc \<up> a @ Bk # <list> @ Bk \<up> rn; a = Suc nat\<rbrakk> \<Longrightarrow> \<exists>rna ml. Oc \<up> a @ Bk # <list> @ Bk \<up> rn = <ml> @ Bk \<up> rna \<or> a = 0 \<and> <ml> @ Bk \<up> rna = <list> @ Bk \<up> rn
[PROOF STEP]
apply(rule_tac x = rn in exI,rule_tac x = "(a-1) # list" in exI, simp add: tape_of_nl_cons)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
mopup_aft_erase_b (Suc (Suc (Suc (2 * n))), l, Bk # xs) lm n ires

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma mopup_left_moving_via_aft_erase_a[simp]:
  assumes "mopup_aft_erase_a (Suc (Suc (2 * n)), l, Bk # xs) lm n ires"
  shows "mopup_left_moving (5 + 2 * n, tl l, hd l # Bk # xs) lm n ires"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mopup_left_moving (5 + 2 * n, tl l, hd l # Bk # xs) lm n ires
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. mopup_left_moving (5 + 2 * n, tl l, hd l # Bk # xs) lm n ires
[PROOF STEP]
from assms[unfolded mopup_aft_erase_a.simps]
[PROOF STATE]
proof (chain)
picking this:
\<exists>lnl lnr rn ml m. m = Suc (lm ! n) \<and> l = Bk \<up> lnr @ Oc \<up> m @ Bk \<up> lnl @ Bk # Bk # ires \<and> Bk # xs = <ml> @ Bk \<up> rn
[PROOF STEP]
obtain lnl lnr rn ml where
    "l = Bk \<up> lnr @ Oc \<up> Suc (lm ! n) @ Bk \<up> lnl @ Bk # Bk # ires"
    "Bk # xs = <ml::nat list> @ Bk \<up> rn"
[PROOF STATE]
proof (prove)
using this:
\<exists>lnl lnr rn ml m. m = Suc (lm ! n) \<and> l = Bk \<up> lnr @ Oc \<up> m @ Bk \<up> lnl @ Bk # Bk # ires \<and> Bk # xs = <ml> @ Bk \<up> rn

goal (1 subgoal):
 1. (\<And>lnr lnl ml rn. \<lbrakk>l = Bk \<up> lnr @ Oc \<up> Suc (lm ! n) @ Bk \<up> lnl @ Bk # Bk # ires; Bk # xs = <ml> @ Bk \<up> rn\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
l = Bk \<up> lnr @ Oc \<up> Suc (lm ! n) @ Bk \<up> lnl @ Bk # Bk # ires
Bk # xs = <ml> @ Bk \<up> rn

goal (1 subgoal):
 1. mopup_left_moving (5 + 2 * n, tl l, hd l # Bk # xs) lm n ires
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
l = Bk \<up> lnr @ Oc \<up> Suc (lm ! n) @ Bk \<up> lnl @ Bk # Bk # ires
Bk # xs = <ml> @ Bk \<up> rn

goal (1 subgoal):
 1. mopup_left_moving (5 + 2 * n, tl l, hd l # Bk # xs) lm n ires
[PROOF STEP]
unfolding mopup_left_moving.simps
[PROOF STATE]
proof (prove)
using this:
l = Bk \<up> lnr @ Oc \<up> Suc (lm ! n) @ Bk \<up> lnl @ Bk # Bk # ires
Bk # xs = <ml> @ Bk \<up> rn

goal (1 subgoal):
 1. \<exists>lnl lnr rn m. m = Suc (lm ! n) \<and> (tl l = Bk \<up> lnr @ Oc \<up> m @ Bk \<up> lnl @ Bk # Bk # ires \<and> hd l # Bk # xs = Bk \<up> rn \<or> tl l = Oc \<up> (m - 1) @ Bk \<up> lnl @ Bk # Bk # ires \<and> hd l # Bk # xs = Oc # Bk \<up> rn)
[PROOF STEP]
by(cases lnr;cases ml,auto simp: tape_of_nl_cons)
[PROOF STATE]
proof (state)
this:
mopup_left_moving (5 + 2 * n, tl l, hd l # Bk # xs) lm n ires

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma mopup_aft_erase_a_nonempty[simp]:
  "mopup_aft_erase_a (Suc (Suc (2 * n)), l, xs) lm n ires \<Longrightarrow> l \<noteq> []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mopup_aft_erase_a (Suc (Suc (2 * n)), l, xs) lm n ires \<Longrightarrow> l \<noteq> []
[PROOF STEP]
by(auto simp only: mopup_aft_erase_a.simps)


[STATEMENT]
lemma mopup_left_moving_via_aft_erase_a_emptylst[simp]:
  assumes "mopup_aft_erase_a (Suc (Suc (2 * n)), l, []) lm n ires"
  shows "mopup_left_moving (5 + 2 * n, tl l, [hd l]) lm n ires"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mopup_left_moving (5 + 2 * n, tl l, [hd l]) lm n ires
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. mopup_left_moving (5 + 2 * n, tl l, [hd l]) lm n ires
[PROOF STEP]
have [intro!]:"[Bk] = Bk \<up> 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [Bk] = Bk \<up> 1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
[Bk] = Bk \<up> 1

goal (1 subgoal):
 1. mopup_left_moving (5 + 2 * n, tl l, [hd l]) lm n ires
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
mopup_aft_erase_a (Suc (Suc (2 * n)), l, []) lm n ires
[PROOF STEP]
obtain lnl lnr where "l = Bk \<up> lnr @ Oc # Oc \<up> (lm ! n) @ Bk \<up> lnl @ Bk # Bk # ires"
[PROOF STATE]
proof (prove)
using this:
mopup_aft_erase_a (Suc (Suc (2 * n)), l, []) lm n ires

goal (1 subgoal):
 1. (\<And>lnr lnl. l = Bk \<up> lnr @ Oc # Oc \<up> lm ! n @ Bk \<up> lnl @ Bk # Bk # ires \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding mopup_aft_erase_a.simps
[PROOF STATE]
proof (prove)
using this:
\<exists>lnl lnr rn ml m. m = Suc (lm ! n) \<and> l = Bk \<up> lnr @ Oc \<up> m @ Bk \<up> lnl @ Bk # Bk # ires \<and> [] = <ml> @ Bk \<up> rn

goal (1 subgoal):
 1. (\<And>lnr lnl. l = Bk \<up> lnr @ Oc # Oc \<up> lm ! n @ Bk \<up> lnl @ Bk # Bk # ires \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
l = Bk \<up> lnr @ Oc # Oc \<up> lm ! n @ Bk \<up> lnl @ Bk # Bk # ires

goal (1 subgoal):
 1. mopup_left_moving (5 + 2 * n, tl l, [hd l]) lm n ires
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
l = Bk \<up> lnr @ Oc # Oc \<up> lm ! n @ Bk \<up> lnl @ Bk # Bk # ires

goal (1 subgoal):
 1. mopup_left_moving (5 + 2 * n, tl l, [hd l]) lm n ires
[PROOF STEP]
by(case_tac lnr, auto simp add:mopup_left_moving.simps)
[PROOF STATE]
proof (state)
this:
mopup_left_moving (5 + 2 * n, tl l, [hd l]) lm n ires

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma mopup_aft_erase_b_no_Oc[simp]: "mopup_aft_erase_b (2 * n + 3, l, Oc # xs) lm n ires = False"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mopup_aft_erase_b (2 * n + 3, l, Oc # xs) lm n ires = False
[PROOF STEP]
by(auto simp: mopup_aft_erase_b.simps)


[STATEMENT]
lemma tape_of_ex1[intro]:
  "\<exists>rna ml. Oc \<up> a @ Bk \<up> rn = <ml::nat list> @ Bk \<up> rna \<or> Oc \<up> a @ Bk \<up> rn = Bk # <ml> @ Bk \<up> rna"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>rna ml. Oc \<up> a @ Bk \<up> rn = <ml> @ Bk \<up> rna \<or> Oc \<up> a @ Bk \<up> rn = Bk # <ml> @ Bk \<up> rna
[PROOF STEP]
by(rule_tac x = rn in exI, rule_tac x = "if a = 0 then [] else [a-1]" in exI,
      simp add: tape_of_list_def tape_of_nat_def)


[STATEMENT]
lemma mopup_aft_erase_b_via_c_helper: "\<exists>rna ml. Oc \<up> a @ Bk # <list::nat list> @ Bk \<up> rn =
  <ml> @ Bk \<up> rna \<or> Oc \<up> a @ Bk # <list> @ Bk \<up> rn = Bk # <ml::nat list> @ Bk \<up> rna"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>rna ml. Oc \<up> a @ Bk # <list> @ Bk \<up> rn = <ml> @ Bk \<up> rna \<or> Oc \<up> a @ Bk # <list> @ Bk \<up> rn = Bk # <ml> @ Bk \<up> rna
[PROOF STEP]
apply(cases "list = []", simp add: replicate_Suc[THEN sym] del: replicate_Suc split_head_repeat)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. list = [] \<Longrightarrow> \<exists>rna ml. Oc \<up> a @ Bk \<up> Suc rn = <ml> @ Bk \<up> rna \<or> Oc \<up> a @ Bk \<up> Suc rn = Bk # <ml> @ Bk \<up> rna
 2. list \<noteq> [] \<Longrightarrow> \<exists>rna ml. Oc \<up> a @ Bk # <list> @ Bk \<up> rn = <ml> @ Bk \<up> rna \<or> Oc \<up> a @ Bk # <list> @ Bk \<up> rn = Bk # <ml> @ Bk \<up> rna
[PROOF STEP]
apply(rule_tac rn = "Suc rn" in tape_of_ex1)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. list \<noteq> [] \<Longrightarrow> \<exists>rna ml. Oc \<up> a @ Bk # <list> @ Bk \<up> rn = <ml> @ Bk \<up> rna \<or> Oc \<up> a @ Bk # <list> @ Bk \<up> rn = Bk # <ml> @ Bk \<up> rna
[PROOF STEP]
apply(cases a, simp)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>list \<noteq> []; a = 0\<rbrakk> \<Longrightarrow> \<exists>rna ml. Bk # <list> @ Bk \<up> rn = <ml> @ Bk \<up> rna \<or> <list> @ Bk \<up> rn = <ml> @ Bk \<up> rna
 2. \<And>nat. \<lbrakk>list \<noteq> []; a = Suc nat\<rbrakk> \<Longrightarrow> \<exists>rna ml. Oc \<up> a @ Bk # <list> @ Bk \<up> rn = <ml> @ Bk \<up> rna \<or> Oc \<up> a @ Bk # <list> @ Bk \<up> rn = Bk # <ml> @ Bk \<up> rna
[PROOF STEP]
apply(rule_tac x = rn in exI, rule_tac x = list in exI, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>nat. \<lbrakk>list \<noteq> []; a = Suc nat\<rbrakk> \<Longrightarrow> \<exists>rna ml. Oc \<up> a @ Bk # <list> @ Bk \<up> rn = <ml> @ Bk \<up> rna \<or> Oc \<up> a @ Bk # <list> @ Bk \<up> rn = Bk # <ml> @ Bk \<up> rna
[PROOF STEP]
apply(rule_tac x = rn in exI, rule_tac x = "(a-1) # list" in exI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>nat. \<lbrakk>list \<noteq> []; a = Suc nat\<rbrakk> \<Longrightarrow> Oc \<up> a @ Bk # <list> @ Bk \<up> rn = <(a - 1) # list> @ Bk \<up> rn \<or> Oc \<up> a @ Bk # <list> @ Bk \<up> rn = Bk # <(a - 1) # list> @ Bk \<up> rn
[PROOF STEP]
apply(simp add: tape_of_nl_cons)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma mopup_aft_erase_b_via_c[simp]:
  assumes "mopup_aft_erase_c (2 * n + 4, l, Oc # xs) lm n ires"
  shows "mopup_aft_erase_b (Suc (Suc (Suc (2 * n))), l, Bk # xs) lm n ires"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mopup_aft_erase_b (Suc (Suc (Suc (2 * n))), l, Bk # xs) lm n ires
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. mopup_aft_erase_b (Suc (Suc (Suc (2 * n))), l, Bk # xs) lm n ires
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
mopup_aft_erase_c (2 * n + 4, l, Oc # xs) lm n ires
[PROOF STEP]
obtain lnl rn lnr ml where assms:
    "l = Bk \<up> lnr @ Oc # Oc \<up> (lm ! n) @ Bk \<up> lnl @ Bk # Bk # ires"
    "Oc # xs = <ml::nat list> @ Bk \<up> rn"
[PROOF STATE]
proof (prove)
using this:
mopup_aft_erase_c (2 * n + 4, l, Oc # xs) lm n ires

goal (1 subgoal):
 1. (\<And>lnr lnl ml rn. \<lbrakk>l = Bk \<up> lnr @ Oc # Oc \<up> lm ! n @ Bk \<up> lnl @ Bk # Bk # ires; Oc # xs = <ml> @ Bk \<up> rn\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding mopup_aft_erase_c.simps
[PROOF STATE]
proof (prove)
using this:
\<exists>lnl lnr rn ml m. m = Suc (lm ! n) \<and> l = Bk \<up> lnr @ Oc \<up> m @ Bk \<up> lnl @ Bk # Bk # ires \<and> (Oc # xs = <ml> @ Bk \<up> rn \<or> Oc # xs = Bk # <ml> @ Bk \<up> rn)

goal (1 subgoal):
 1. (\<And>lnr lnl ml rn. \<lbrakk>l = Bk \<up> lnr @ Oc # Oc \<up> lm ! n @ Bk \<up> lnl @ Bk # Bk # ires; Oc # xs = <ml> @ Bk \<up> rn\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
l = Bk \<up> lnr @ Oc # Oc \<up> lm ! n @ Bk \<up> lnl @ Bk # Bk # ires
Oc # xs = <ml> @ Bk \<up> rn

goal (1 subgoal):
 1. mopup_aft_erase_b (Suc (Suc (Suc (2 * n))), l, Bk # xs) lm n ires
[PROOF STEP]
hence "Oc # xs = Bk \<up> rn \<Longrightarrow> False"
[PROOF STATE]
proof (prove)
using this:
l = Bk \<up> lnr @ Oc # Oc \<up> lm ! n @ Bk \<up> lnl @ Bk # Bk # ires
Oc # xs = <ml> @ Bk \<up> rn

goal (1 subgoal):
 1. Oc # xs = Bk \<up> rn \<Longrightarrow> False
[PROOF STEP]
by(cases rn,auto)
[PROOF STATE]
proof (state)
this:
Oc # xs = Bk \<up> rn \<Longrightarrow> False

goal (1 subgoal):
 1. mopup_aft_erase_b (Suc (Suc (Suc (2 * n))), l, Bk # xs) lm n ires
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
Oc # xs = Bk \<up> rn \<Longrightarrow> False

goal (1 subgoal):
 1. mopup_aft_erase_b (Suc (Suc (Suc (2 * n))), l, Bk # xs) lm n ires
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
Oc # xs = Bk \<up> rn \<Longrightarrow> False
l = Bk \<up> lnr @ Oc # Oc \<up> lm ! n @ Bk \<up> lnl @ Bk # Bk # ires
Oc # xs = <ml> @ Bk \<up> rn

goal (1 subgoal):
 1. mopup_aft_erase_b (Suc (Suc (Suc (2 * n))), l, Bk # xs) lm n ires
[PROOF STEP]
unfolding mopup_aft_erase_b.simps
[PROOF STATE]
proof (prove)
using this:
Oc # xs = Bk \<up> rn \<Longrightarrow> False
l = Bk \<up> lnr @ Oc # Oc \<up> lm ! n @ Bk \<up> lnl @ Bk # Bk # ires
Oc # xs = <ml> @ Bk \<up> rn

goal (1 subgoal):
 1. \<exists>lnl lnr rn ml m. m = Suc (lm ! n) \<and> l = Bk \<up> lnr @ Oc \<up> m @ Bk \<up> lnl @ Bk # Bk # ires \<and> (Bk # xs = Bk # <ml> @ Bk \<up> rn \<or> Bk # xs = Bk # Bk # <ml> @ Bk \<up> rn)
[PROOF STEP]
by(cases ml)
      (auto simp add: tape_of_nl_cons split: if_splits intro:mopup_aft_erase_b_via_c_helper
        simp del:split_head_repeat)
[PROOF STATE]
proof (state)
this:
mopup_aft_erase_b (Suc (Suc (Suc (2 * n))), l, Bk # xs) lm n ires

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma mopup_aft_erase_c_aft_erase_a[simp]:
  assumes "mopup_aft_erase_c (2 * n + 4, l, Bk # xs) lm n ires"
  shows "mopup_aft_erase_a (Suc (Suc (2 * n)), Bk # l, xs) lm n ires"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mopup_aft_erase_a (Suc (Suc (2 * n)), Bk # l, xs) lm n ires
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. mopup_aft_erase_a (Suc (Suc (2 * n)), Bk # l, xs) lm n ires
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
mopup_aft_erase_c (2 * n + 4, l, Bk # xs) lm n ires
[PROOF STEP]
obtain lnl lnr rn ml where
    "l = Bk \<up> lnr @ Oc \<up> Suc (lm ! n) @ Bk \<up> lnl @ Bk # Bk # ires"
    "(Bk # xs = <ml::nat list> @ Bk \<up> rn \<or> Bk # xs = Bk # <ml> @ Bk \<up> rn)"
[PROOF STATE]
proof (prove)
using this:
mopup_aft_erase_c (2 * n + 4, l, Bk # xs) lm n ires

goal (1 subgoal):
 1. (\<And>lnr lnl ml rn. \<lbrakk>l = Bk \<up> lnr @ Oc \<up> Suc (lm ! n) @ Bk \<up> lnl @ Bk # Bk # ires; Bk # xs = <ml> @ Bk \<up> rn \<or> Bk # xs = Bk # <ml> @ Bk \<up> rn\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding mopup_aft_erase_c.simps
[PROOF STATE]
proof (prove)
using this:
\<exists>lnl lnr rn ml m. m = Suc (lm ! n) \<and> l = Bk \<up> lnr @ Oc \<up> m @ Bk \<up> lnl @ Bk # Bk # ires \<and> (Bk # xs = <ml> @ Bk \<up> rn \<or> Bk # xs = Bk # <ml> @ Bk \<up> rn)

goal (1 subgoal):
 1. (\<And>lnr lnl ml rn. \<lbrakk>l = Bk \<up> lnr @ Oc \<up> Suc (lm ! n) @ Bk \<up> lnl @ Bk # Bk # ires; Bk # xs = <ml> @ Bk \<up> rn \<or> Bk # xs = Bk # <ml> @ Bk \<up> rn\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
l = Bk \<up> lnr @ Oc \<up> Suc (lm ! n) @ Bk \<up> lnl @ Bk # Bk # ires
Bk # xs = <ml> @ Bk \<up> rn \<or> Bk # xs = Bk # <ml> @ Bk \<up> rn

goal (1 subgoal):
 1. mopup_aft_erase_a (Suc (Suc (2 * n)), Bk # l, xs) lm n ires
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
l = Bk \<up> lnr @ Oc \<up> Suc (lm ! n) @ Bk \<up> lnl @ Bk # Bk # ires
Bk # xs = <ml> @ Bk \<up> rn \<or> Bk # xs = Bk # <ml> @ Bk \<up> rn

goal (1 subgoal):
 1. mopup_aft_erase_a (Suc (Suc (2 * n)), Bk # l, xs) lm n ires
[PROOF STEP]
unfolding mopup_aft_erase_a.simps
[PROOF STATE]
proof (prove)
using this:
l = Bk \<up> lnr @ Oc \<up> Suc (lm ! n) @ Bk \<up> lnl @ Bk # Bk # ires
Bk # xs = <ml> @ Bk \<up> rn \<or> Bk # xs = Bk # <ml> @ Bk \<up> rn

goal (1 subgoal):
 1. \<exists>lnl lnr rn ml m. m = Suc (lm ! n) \<and> Bk # l = Bk \<up> lnr @ Oc \<up> m @ Bk \<up> lnl @ Bk # Bk # ires \<and> xs = <ml> @ Bk \<up> rn
[PROOF STEP]
apply(clarify)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Bk # xs = <ml> @ Bk \<up> rn \<or> Bk # xs = Bk # <ml> @ Bk \<up> rn; l = Bk \<up> lnr @ Oc \<up> Suc (lm ! n) @ Bk \<up> lnl @ Bk # Bk # ires\<rbrakk> \<Longrightarrow> \<exists>lnla lnra rn ml m. m = Suc (lm ! n) \<and> Bk # Bk \<up> lnr @ Oc \<up> Suc (lm ! n) @ Bk \<up> lnl @ Bk # Bk # ires = Bk \<up> lnra @ Oc \<up> m @ Bk \<up> lnla @ Bk # Bk # ires \<and> xs = <ml> @ Bk \<up> rn
[PROOF STEP]
apply(erule disjE)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>l = Bk \<up> lnr @ Oc \<up> Suc (lm ! n) @ Bk \<up> lnl @ Bk # Bk # ires; Bk # xs = <ml> @ Bk \<up> rn\<rbrakk> \<Longrightarrow> \<exists>lnla lnra rn ml m. m = Suc (lm ! n) \<and> Bk # Bk \<up> lnr @ Oc \<up> Suc (lm ! n) @ Bk \<up> lnl @ Bk # Bk # ires = Bk \<up> lnra @ Oc \<up> m @ Bk \<up> lnla @ Bk # Bk # ires \<and> xs = <ml> @ Bk \<up> rn
 2. \<lbrakk>l = Bk \<up> lnr @ Oc \<up> Suc (lm ! n) @ Bk \<up> lnl @ Bk # Bk # ires; Bk # xs = Bk # <ml> @ Bk \<up> rn\<rbrakk> \<Longrightarrow> \<exists>lnla lnra rn ml m. m = Suc (lm ! n) \<and> Bk # Bk \<up> lnr @ Oc \<up> Suc (lm ! n) @ Bk \<up> lnl @ Bk # Bk # ires = Bk \<up> lnra @ Oc \<up> m @ Bk \<up> lnla @ Bk # Bk # ires \<and> xs = <ml> @ Bk \<up> rn
[PROOF STEP]
apply(subgoal_tac "ml = []", simp, case_tac rn,
        simp, simp, rule conjI)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>nat. \<lbrakk>l = Bk \<up> lnr @ Oc # Oc \<up> lm ! n @ Bk \<up> lnl @ Bk # Bk # ires; xs = Bk \<up> nat; ml = []; rn = Suc nat\<rbrakk> \<Longrightarrow> \<exists>lnla lnra. Bk # Bk \<up> lnr @ Oc # Oc \<up> lm ! n @ Bk \<up> lnl = Bk \<up> lnra @ Oc # Oc \<up> lm ! n @ Bk \<up> lnla
 2. \<And>nat. \<lbrakk>l = Bk \<up> lnr @ Oc # Oc \<up> lm ! n @ Bk \<up> lnl @ Bk # Bk # ires; xs = Bk \<up> nat; ml = []; rn = Suc nat\<rbrakk> \<Longrightarrow> \<exists>rn ml. Bk \<up> nat = <ml> @ Bk \<up> rn
 3. \<lbrakk>l = Bk \<up> lnr @ Oc \<up> Suc (lm ! n) @ Bk \<up> lnl @ Bk # Bk # ires; Bk # xs = <ml> @ Bk \<up> rn\<rbrakk> \<Longrightarrow> ml = []
 4. \<lbrakk>l = Bk \<up> lnr @ Oc \<up> Suc (lm ! n) @ Bk \<up> lnl @ Bk # Bk # ires; Bk # xs = Bk # <ml> @ Bk \<up> rn\<rbrakk> \<Longrightarrow> \<exists>lnla lnra rn ml m. m = Suc (lm ! n) \<and> Bk # Bk \<up> lnr @ Oc \<up> Suc (lm ! n) @ Bk \<up> lnl @ Bk # Bk # ires = Bk \<up> lnra @ Oc \<up> m @ Bk \<up> lnla @ Bk # Bk # ires \<and> xs = <ml> @ Bk \<up> rn
[PROOF STEP]
apply(rule_tac x = lnl in exI, rule_tac x = "Suc lnr" in exI, simp)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>nat. \<lbrakk>l = Bk \<up> lnr @ Oc # Oc \<up> lm ! n @ Bk \<up> lnl @ Bk # Bk # ires; xs = Bk \<up> nat; ml = []; rn = Suc nat\<rbrakk> \<Longrightarrow> \<exists>rn ml. Bk \<up> nat = <ml> @ Bk \<up> rn
 2. \<lbrakk>l = Bk \<up> lnr @ Oc \<up> Suc (lm ! n) @ Bk \<up> lnl @ Bk # Bk # ires; Bk # xs = <ml> @ Bk \<up> rn\<rbrakk> \<Longrightarrow> ml = []
 3. \<lbrakk>l = Bk \<up> lnr @ Oc \<up> Suc (lm ! n) @ Bk \<up> lnl @ Bk # Bk # ires; Bk # xs = Bk # <ml> @ Bk \<up> rn\<rbrakk> \<Longrightarrow> \<exists>lnla lnra rn ml m. m = Suc (lm ! n) \<and> Bk # Bk \<up> lnr @ Oc \<up> Suc (lm ! n) @ Bk \<up> lnl @ Bk # Bk # ires = Bk \<up> lnra @ Oc \<up> m @ Bk \<up> lnla @ Bk # Bk # ires \<and> xs = <ml> @ Bk \<up> rn
[PROOF STEP]
apply (insert tape_of_list_empty,blast)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>l = Bk \<up> lnr @ Oc \<up> Suc (lm ! n) @ Bk \<up> lnl @ Bk # Bk # ires; Bk # xs = <ml> @ Bk \<up> rn; <[]> = []\<rbrakk> \<Longrightarrow> ml = []
 2. \<lbrakk>l = Bk \<up> lnr @ Oc \<up> Suc (lm ! n) @ Bk \<up> lnl @ Bk # Bk # ires; Bk # xs = Bk # <ml> @ Bk \<up> rn; <[]> = []\<rbrakk> \<Longrightarrow> \<exists>lnla lnra rn ml m. m = Suc (lm ! n) \<and> Bk # Bk \<up> lnr @ Oc \<up> Suc (lm ! n) @ Bk \<up> lnl @ Bk # Bk # ires = Bk \<up> lnra @ Oc \<up> m @ Bk \<up> lnla @ Bk # Bk # ires \<and> xs = <ml> @ Bk \<up> rn
[PROOF STEP]
apply(case_tac ml, simp, simp add: tape_of_nl_cons split: if_splits)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>l = Bk \<up> lnr @ Oc \<up> Suc (lm ! n) @ Bk \<up> lnl @ Bk # Bk # ires; Bk # xs = Bk # <ml> @ Bk \<up> rn; <[]> = []\<rbrakk> \<Longrightarrow> \<exists>lnla lnra rn ml m. m = Suc (lm ! n) \<and> Bk # Bk \<up> lnr @ Oc \<up> Suc (lm ! n) @ Bk \<up> lnl @ Bk # Bk # ires = Bk \<up> lnra @ Oc \<up> m @ Bk \<up> lnla @ Bk # Bk # ires \<and> xs = <ml> @ Bk \<up> rn
[PROOF STEP]
apply(rule_tac x = lnl in exI, rule_tac x = "Suc lnr" in exI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>l = Bk \<up> lnr @ Oc \<up> Suc (lm ! n) @ Bk \<up> lnl @ Bk # Bk # ires; Bk # xs = Bk # <ml> @ Bk \<up> rn; <[]> = []\<rbrakk> \<Longrightarrow> \<exists>rn ml m. m = Suc (lm ! n) \<and> Bk # Bk \<up> lnr @ Oc \<up> Suc (lm ! n) @ Bk \<up> lnl @ Bk # Bk # ires = Bk \<up> Suc lnr @ Oc \<up> m @ Bk \<up> lnl @ Bk # Bk # ires \<and> xs = <ml> @ Bk \<up> rn
[PROOF STEP]
apply(rule_tac x = rn in exI, rule_tac x = "ml" in exI, simp)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
mopup_aft_erase_a (Suc (Suc (2 * n)), Bk # l, xs) lm n ires

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma mopup_aft_erase_a_via_c[simp]:
  "\<lbrakk>mopup_aft_erase_c (2 * n + 4, l, []) lm n ires\<rbrakk>
 \<Longrightarrow> mopup_aft_erase_a (Suc (Suc (2 * n)), Bk # l, []) lm n ires"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mopup_aft_erase_c (2 * n + 4, l, []) lm n ires \<Longrightarrow> mopup_aft_erase_a (Suc (Suc (2 * n)), Bk # l, []) lm n ires
[PROOF STEP]
by (rule mopup_aft_erase_c_aft_erase_a)
    (auto simp:mopup_aft_erase_c.simps)


[STATEMENT]
lemma mopup_aft_erase_b_2_aft_erase_c[simp]:
  assumes "mopup_aft_erase_b (2 * n + 3, l, Bk # xs) lm n ires"
  shows "mopup_aft_erase_c (4 + 2 * n, Bk # l, xs) lm n ires"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mopup_aft_erase_c (4 + 2 * n, Bk # l, xs) lm n ires
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. mopup_aft_erase_c (4 + 2 * n, Bk # l, xs) lm n ires
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
mopup_aft_erase_b (2 * n + 3, l, Bk # xs) lm n ires
[PROOF STEP]
obtain lnl lnr ml rn where
    "l = Bk \<up> lnr @ Oc \<up> Suc (lm ! n) @ Bk \<up> lnl @ Bk # Bk # ires"
    "Bk # xs = Bk # <ml::nat list> @ Bk \<up> rn \<or> Bk # xs = Bk # Bk # <ml> @ Bk \<up> rn"
[PROOF STATE]
proof (prove)
using this:
mopup_aft_erase_b (2 * n + 3, l, Bk # xs) lm n ires

goal (1 subgoal):
 1. (\<And>lnr lnl ml rn. \<lbrakk>l = Bk \<up> lnr @ Oc \<up> Suc (lm ! n) @ Bk \<up> lnl @ Bk # Bk # ires; Bk # xs = Bk # <ml> @ Bk \<up> rn \<or> Bk # xs = Bk # Bk # <ml> @ Bk \<up> rn\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding  mopup_aft_erase_b.simps
[PROOF STATE]
proof (prove)
using this:
\<exists>lnl lnr rn ml m. m = Suc (lm ! n) \<and> l = Bk \<up> lnr @ Oc \<up> m @ Bk \<up> lnl @ Bk # Bk # ires \<and> (Bk # xs = Bk # <ml> @ Bk \<up> rn \<or> Bk # xs = Bk # Bk # <ml> @ Bk \<up> rn)

goal (1 subgoal):
 1. (\<And>lnr lnl ml rn. \<lbrakk>l = Bk \<up> lnr @ Oc \<up> Suc (lm ! n) @ Bk \<up> lnl @ Bk # Bk # ires; Bk # xs = Bk # <ml> @ Bk \<up> rn \<or> Bk # xs = Bk # Bk # <ml> @ Bk \<up> rn\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
l = Bk \<up> lnr @ Oc \<up> Suc (lm ! n) @ Bk \<up> lnl @ Bk # Bk # ires
Bk # xs = Bk # <ml> @ Bk \<up> rn \<or> Bk # xs = Bk # Bk # <ml> @ Bk \<up> rn

goal (1 subgoal):
 1. mopup_aft_erase_c (4 + 2 * n, Bk # l, xs) lm n ires
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
l = Bk \<up> lnr @ Oc \<up> Suc (lm ! n) @ Bk \<up> lnl @ Bk # Bk # ires
Bk # xs = Bk # <ml> @ Bk \<up> rn \<or> Bk # xs = Bk # Bk # <ml> @ Bk \<up> rn

goal (1 subgoal):
 1. mopup_aft_erase_c (4 + 2 * n, Bk # l, xs) lm n ires
[PROOF STEP]
unfolding mopup_aft_erase_c.simps
[PROOF STATE]
proof (prove)
using this:
l = Bk \<up> lnr @ Oc \<up> Suc (lm ! n) @ Bk \<up> lnl @ Bk # Bk # ires
Bk # xs = Bk # <ml> @ Bk \<up> rn \<or> Bk # xs = Bk # Bk # <ml> @ Bk \<up> rn

goal (1 subgoal):
 1. \<exists>lnl lnr rn ml m. m = Suc (lm ! n) \<and> Bk # l = Bk \<up> lnr @ Oc \<up> m @ Bk \<up> lnl @ Bk # Bk # ires \<and> (xs = <ml> @ Bk \<up> rn \<or> xs = Bk # <ml> @ Bk \<up> rn)
[PROOF STEP]
by (rule_tac x = "lnl" in exI) auto
[PROOF STATE]
proof (state)
this:
mopup_aft_erase_c (4 + 2 * n, Bk # l, xs) lm n ires

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma mopup_aft_erase_c_via_b[simp]:
  "\<lbrakk>mopup_aft_erase_b (2 * n + 3, l, []) lm n ires\<rbrakk>
 \<Longrightarrow> mopup_aft_erase_c (4 + 2 * n, Bk # l, []) lm n ires"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mopup_aft_erase_b (2 * n + 3, l, []) lm n ires \<Longrightarrow> mopup_aft_erase_c (4 + 2 * n, Bk # l, []) lm n ires
[PROOF STEP]
by(auto simp add: mopup_aft_erase_b.simps intro:mopup_aft_erase_b_2_aft_erase_c)


[STATEMENT]
lemma mopup_left_moving_nonempty[simp]:
  "mopup_left_moving (2 * n + 5, l, Oc # xs) lm n ires \<Longrightarrow> l \<noteq> []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mopup_left_moving (2 * n + 5, l, Oc # xs) lm n ires \<Longrightarrow> l \<noteq> []
[PROOF STEP]
by(auto simp: mopup_left_moving.simps)


[STATEMENT]
lemma exp_ind: "a\<up>(Suc x) = a\<up>x @ [a]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<up> Suc x = a \<up> x @ [a]
[PROOF STEP]
by(induct x, auto)


[STATEMENT]
lemma mopup_jump_over2_via_left_moving[simp]:
  "\<lbrakk>mopup_left_moving (2 * n + 5, l, Oc # xs) lm n ires\<rbrakk>
  \<Longrightarrow> mopup_jump_over2 (2 * n + 6, tl l, hd l # Oc # xs) lm n ires"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mopup_left_moving (2 * n + 5, l, Oc # xs) lm n ires \<Longrightarrow> mopup_jump_over2 (2 * n + 6, tl l, hd l # Oc # xs) lm n ires
[PROOF STEP]
apply(simp only: mopup_left_moving.simps mopup_jump_over2.simps)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>lnl lnr rn m. m = Suc (lm ! n) \<and> (l = Bk \<up> lnr @ Oc \<up> m @ Bk \<up> lnl @ Bk # Bk # ires \<and> Oc # xs = Bk \<up> rn \<or> l = Oc \<up> (m - 1) @ Bk \<up> lnl @ Bk # Bk # ires \<and> Oc # xs = Oc # Bk \<up> rn) \<Longrightarrow> \<exists>ln rn m1 m2. m1 + m2 = Suc (lm ! n) \<and> hd l # Oc # xs \<noteq> [] \<and> (hd (hd l # Oc # xs) = Oc \<longrightarrow> tl l = Oc \<up> m1 @ Bk \<up> ln @ Bk # Bk # ires \<and> hd l # Oc # xs = Oc \<up> m2 @ Bk \<up> rn) \<and> (hd (hd l # Oc # xs) = Bk \<longrightarrow> tl l = Bk \<up> ln @ Bk # ires \<and> hd l # Oc # xs = Bk # Oc \<up> (m1 + m2) @ Bk \<up> rn)
[PROOF STEP]
apply(erule_tac exE)+
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>lnl lnr rn m. m = Suc (lm ! n) \<and> (l = Bk \<up> lnr @ Oc \<up> m @ Bk \<up> lnl @ Bk # Bk # ires \<and> Oc # xs = Bk \<up> rn \<or> l = Oc \<up> (m - 1) @ Bk \<up> lnl @ Bk # Bk # ires \<and> Oc # xs = Oc # Bk \<up> rn) \<Longrightarrow> \<exists>ln rn m1 m2. m1 + m2 = Suc (lm ! n) \<and> hd l # Oc # xs \<noteq> [] \<and> (hd (hd l # Oc # xs) = Oc \<longrightarrow> tl l = Oc \<up> m1 @ Bk \<up> ln @ Bk # Bk # ires \<and> hd l # Oc # xs = Oc \<up> m2 @ Bk \<up> rn) \<and> (hd (hd l # Oc # xs) = Bk \<longrightarrow> tl l = Bk \<up> ln @ Bk # ires \<and> hd l # Oc # xs = Bk # Oc \<up> (m1 + m2) @ Bk \<up> rn)
[PROOF STEP]
apply(erule conjE, erule disjE, erule conjE)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>lnl lnr rn m. \<lbrakk>m = Suc (lm ! n); l = Bk \<up> lnr @ Oc \<up> m @ Bk \<up> lnl @ Bk # Bk # ires; Oc # xs = Bk \<up> rn\<rbrakk> \<Longrightarrow> \<exists>ln rn m1 m2. m1 + m2 = Suc (lm ! n) \<and> hd l # Oc # xs \<noteq> [] \<and> (hd (hd l # Oc # xs) = Oc \<longrightarrow> tl l = Oc \<up> m1 @ Bk \<up> ln @ Bk # Bk # ires \<and> hd l # Oc # xs = Oc \<up> m2 @ Bk \<up> rn) \<and> (hd (hd l # Oc # xs) = Bk \<longrightarrow> tl l = Bk \<up> ln @ Bk # ires \<and> hd l # Oc # xs = Bk # Oc \<up> (m1 + m2) @ Bk \<up> rn)
 2. \<And>lnl lnr rn m. \<lbrakk>m = Suc (lm ! n); l = Oc \<up> (m - 1) @ Bk \<up> lnl @ Bk # Bk # ires \<and> Oc # xs = Oc # Bk \<up> rn\<rbrakk> \<Longrightarrow> \<exists>ln rn m1 m2. m1 + m2 = Suc (lm ! n) \<and> hd l # Oc # xs \<noteq> [] \<and> (hd (hd l # Oc # xs) = Oc \<longrightarrow> tl l = Oc \<up> m1 @ Bk \<up> ln @ Bk # Bk # ires \<and> hd l # Oc # xs = Oc \<up> m2 @ Bk \<up> rn) \<and> (hd (hd l # Oc # xs) = Bk \<longrightarrow> tl l = Bk \<up> ln @ Bk # ires \<and> hd l # Oc # xs = Bk # Oc \<up> (m1 + m2) @ Bk \<up> rn)
[PROOF STEP]
apply (simp add: Cons_replicate_eq)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>lnl lnr rn m. \<lbrakk>m = Suc (lm ! n); l = Oc \<up> (m - 1) @ Bk \<up> lnl @ Bk # Bk # ires \<and> Oc # xs = Oc # Bk \<up> rn\<rbrakk> \<Longrightarrow> \<exists>ln rn m1 m2. m1 + m2 = Suc (lm ! n) \<and> hd l # Oc # xs \<noteq> [] \<and> (hd (hd l # Oc # xs) = Oc \<longrightarrow> tl l = Oc \<up> m1 @ Bk \<up> ln @ Bk # Bk # ires \<and> hd l # Oc # xs = Oc \<up> m2 @ Bk \<up> rn) \<and> (hd (hd l # Oc # xs) = Bk \<longrightarrow> tl l = Bk \<up> ln @ Bk # ires \<and> hd l # Oc # xs = Bk # Oc \<up> (m1 + m2) @ Bk \<up> rn)
[PROOF STEP]
apply(rename_tac Lnl lnr rn m)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>Lnl lnr rn m. \<lbrakk>m = Suc (lm ! n); l = Oc \<up> (m - 1) @ Bk \<up> Lnl @ Bk # Bk # ires \<and> Oc # xs = Oc # Bk \<up> rn\<rbrakk> \<Longrightarrow> \<exists>ln rn m1 m2. m1 + m2 = Suc (lm ! n) \<and> hd l # Oc # xs \<noteq> [] \<and> (hd (hd l # Oc # xs) = Oc \<longrightarrow> tl l = Oc \<up> m1 @ Bk \<up> ln @ Bk # Bk # ires \<and> hd l # Oc # xs = Oc \<up> m2 @ Bk \<up> rn) \<and> (hd (hd l # Oc # xs) = Bk \<longrightarrow> tl l = Bk \<up> ln @ Bk # ires \<and> hd l # Oc # xs = Bk # Oc \<up> (m1 + m2) @ Bk \<up> rn)
[PROOF STEP]
apply(cases "hd l", simp add:  )
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>Lnl rn. \<lbrakk>l = Oc \<up> lm ! n @ Bk \<up> Lnl @ Bk # Bk # ires \<and> xs = Bk \<up> rn; hd (Oc \<up> lm ! n @ Bk \<up> Lnl @ Bk # Bk # ires) = Bk\<rbrakk> \<Longrightarrow> \<exists>ln rna m1 m2. m1 + m2 = Suc (lm ! n) \<and> tl (Oc \<up> lm ! n @ Bk \<up> Lnl @ Bk # Bk # ires) = Bk \<up> ln @ Bk # ires \<and> Oc # Bk \<up> rn = Oc \<up> (m1 + m2) @ Bk \<up> rna
 2. \<And>Lnl lnr rn m. \<lbrakk>m = Suc (lm ! n); l = Oc \<up> (m - 1) @ Bk \<up> Lnl @ Bk # Bk # ires \<and> Oc # xs = Oc # Bk \<up> rn; hd l = Oc\<rbrakk> \<Longrightarrow> \<exists>ln rn m1 m2. m1 + m2 = Suc (lm ! n) \<and> hd l # Oc # xs \<noteq> [] \<and> (hd (hd l # Oc # xs) = Oc \<longrightarrow> tl l = Oc \<up> m1 @ Bk \<up> ln @ Bk # Bk # ires \<and> hd l # Oc # xs = Oc \<up> m2 @ Bk \<up> rn) \<and> (hd (hd l # Oc # xs) = Bk \<longrightarrow> tl l = Bk \<up> ln @ Bk # ires \<and> hd l # Oc # xs = Bk # Oc \<up> (m1 + m2) @ Bk \<up> rn)
[PROOF STEP]
apply(cases "lm ! n", simp)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>Lnl rn. \<lbrakk>l = Bk \<up> Lnl @ Bk # Bk # ires \<and> xs = Bk \<up> rn; hd (Bk \<up> Lnl @ Bk # Bk # ires) = Bk; lm ! n = 0\<rbrakk> \<Longrightarrow> \<exists>ln rna m1 m2. m1 + m2 = Suc 0 \<and> tl (Bk \<up> Lnl @ Bk # Bk # ires) = Bk \<up> ln @ Bk # ires \<and> Oc # Bk \<up> rn = Oc \<up> (m1 + m2) @ Bk \<up> rna
 2. \<And>Lnl rn nat. \<lbrakk>l = Oc \<up> lm ! n @ Bk \<up> Lnl @ Bk # Bk # ires \<and> xs = Bk \<up> rn; hd (Oc \<up> lm ! n @ Bk \<up> Lnl @ Bk # Bk # ires) = Bk; lm ! n = Suc nat\<rbrakk> \<Longrightarrow> \<exists>ln rna m1 m2. m1 + m2 = Suc (lm ! n) \<and> tl (Oc \<up> lm ! n @ Bk \<up> Lnl @ Bk # Bk # ires) = Bk \<up> ln @ Bk # ires \<and> Oc # Bk \<up> rn = Oc \<up> (m1 + m2) @ Bk \<up> rna
 3. \<And>Lnl lnr rn m. \<lbrakk>m = Suc (lm ! n); l = Oc \<up> (m - 1) @ Bk \<up> Lnl @ Bk # Bk # ires \<and> Oc # xs = Oc # Bk \<up> rn; hd l = Oc\<rbrakk> \<Longrightarrow> \<exists>ln rn m1 m2. m1 + m2 = Suc (lm ! n) \<and> hd l # Oc # xs \<noteq> [] \<and> (hd (hd l # Oc # xs) = Oc \<longrightarrow> tl l = Oc \<up> m1 @ Bk \<up> ln @ Bk # Bk # ires \<and> hd l # Oc # xs = Oc \<up> m2 @ Bk \<up> rn) \<and> (hd (hd l # Oc # xs) = Bk \<longrightarrow> tl l = Bk \<up> ln @ Bk # ires \<and> hd l # Oc # xs = Bk # Oc \<up> (m1 + m2) @ Bk \<up> rn)
[PROOF STEP]
apply(rule exI, rule_tac x = "length xs" in exI,
      rule_tac x = "Suc 0" in exI, rule_tac x = 0 in exI)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>Lnl rn. \<lbrakk>l = Bk \<up> Lnl @ Bk # Bk # ires \<and> xs = Bk \<up> rn; hd (Bk \<up> Lnl @ Bk # Bk # ires) = Bk; lm ! n = 0\<rbrakk> \<Longrightarrow> Suc 0 + 0 = Suc 0 \<and> tl (Bk \<up> Lnl @ Bk # Bk # ires) = Bk \<up> ?ln13 Lnl rn @ Bk # ires \<and> Oc # Bk \<up> rn = Oc \<up> (Suc 0 + 0) @ Bk \<up> length xs
 2. \<And>Lnl rn nat. \<lbrakk>l = Oc \<up> lm ! n @ Bk \<up> Lnl @ Bk # Bk # ires \<and> xs = Bk \<up> rn; hd (Oc \<up> lm ! n @ Bk \<up> Lnl @ Bk # Bk # ires) = Bk; lm ! n = Suc nat\<rbrakk> \<Longrightarrow> \<exists>ln rna m1 m2. m1 + m2 = Suc (lm ! n) \<and> tl (Oc \<up> lm ! n @ Bk \<up> Lnl @ Bk # Bk # ires) = Bk \<up> ln @ Bk # ires \<and> Oc # Bk \<up> rn = Oc \<up> (m1 + m2) @ Bk \<up> rna
 3. \<And>Lnl lnr rn m. \<lbrakk>m = Suc (lm ! n); l = Oc \<up> (m - 1) @ Bk \<up> Lnl @ Bk # Bk # ires \<and> Oc # xs = Oc # Bk \<up> rn; hd l = Oc\<rbrakk> \<Longrightarrow> \<exists>ln rn m1 m2. m1 + m2 = Suc (lm ! n) \<and> hd l # Oc # xs \<noteq> [] \<and> (hd (hd l # Oc # xs) = Oc \<longrightarrow> tl l = Oc \<up> m1 @ Bk \<up> ln @ Bk # Bk # ires \<and> hd l # Oc # xs = Oc \<up> m2 @ Bk \<up> rn) \<and> (hd (hd l # Oc # xs) = Bk \<longrightarrow> tl l = Bk \<up> ln @ Bk # ires \<and> hd l # Oc # xs = Bk # Oc \<up> (m1 + m2) @ Bk \<up> rn)
[PROOF STEP]
apply(case_tac Lnl, simp,simp,  simp add: exp_ind[THEN sym])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>Lnl rn nat. \<lbrakk>l = Oc \<up> lm ! n @ Bk \<up> Lnl @ Bk # Bk # ires \<and> xs = Bk \<up> rn; hd (Oc \<up> lm ! n @ Bk \<up> Lnl @ Bk # Bk # ires) = Bk; lm ! n = Suc nat\<rbrakk> \<Longrightarrow> \<exists>ln rna m1 m2. m1 + m2 = Suc (lm ! n) \<and> tl (Oc \<up> lm ! n @ Bk \<up> Lnl @ Bk # Bk # ires) = Bk \<up> ln @ Bk # ires \<and> Oc # Bk \<up> rn = Oc \<up> (m1 + m2) @ Bk \<up> rna
 2. \<And>Lnl lnr rn m. \<lbrakk>m = Suc (lm ! n); l = Oc \<up> (m - 1) @ Bk \<up> Lnl @ Bk # Bk # ires \<and> Oc # xs = Oc # Bk \<up> rn; hd l = Oc\<rbrakk> \<Longrightarrow> \<exists>ln rn m1 m2. m1 + m2 = Suc (lm ! n) \<and> hd l # Oc # xs \<noteq> [] \<and> (hd (hd l # Oc # xs) = Oc \<longrightarrow> tl l = Oc \<up> m1 @ Bk \<up> ln @ Bk # Bk # ires \<and> hd l # Oc # xs = Oc \<up> m2 @ Bk \<up> rn) \<and> (hd (hd l # Oc # xs) = Bk \<longrightarrow> tl l = Bk \<up> ln @ Bk # ires \<and> hd l # Oc # xs = Bk # Oc \<up> (m1 + m2) @ Bk \<up> rn)
[PROOF STEP]
apply(cases "lm ! n", simp)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>Lnl rn nat nata. \<lbrakk>l = Oc \<up> lm ! n @ Bk \<up> Lnl @ Bk # Bk # ires \<and> xs = Bk \<up> rn; hd (Oc \<up> lm ! n @ Bk \<up> Lnl @ Bk # Bk # ires) = Bk; lm ! n = Suc nat; lm ! n = Suc nata\<rbrakk> \<Longrightarrow> \<exists>ln rna m1 m2. m1 + m2 = Suc (lm ! n) \<and> tl (Oc \<up> lm ! n @ Bk \<up> Lnl @ Bk # Bk # ires) = Bk \<up> ln @ Bk # ires \<and> Oc # Bk \<up> rn = Oc \<up> (m1 + m2) @ Bk \<up> rna
 2. \<And>Lnl lnr rn m. \<lbrakk>m = Suc (lm ! n); l = Oc \<up> (m - 1) @ Bk \<up> Lnl @ Bk # Bk # ires \<and> Oc # xs = Oc # Bk \<up> rn; hd l = Oc\<rbrakk> \<Longrightarrow> \<exists>ln rn m1 m2. m1 + m2 = Suc (lm ! n) \<and> hd l # Oc # xs \<noteq> [] \<and> (hd (hd l # Oc # xs) = Oc \<longrightarrow> tl l = Oc \<up> m1 @ Bk \<up> ln @ Bk # Bk # ires \<and> hd l # Oc # xs = Oc \<up> m2 @ Bk \<up> rn) \<and> (hd (hd l # Oc # xs) = Bk \<longrightarrow> tl l = Bk \<up> ln @ Bk # ires \<and> hd l # Oc # xs = Bk # Oc \<up> (m1 + m2) @ Bk \<up> rn)
[PROOF STEP]
apply(case_tac Lnl, simp, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>Lnl lnr rn m. \<lbrakk>m = Suc (lm ! n); l = Oc \<up> (m - 1) @ Bk \<up> Lnl @ Bk # Bk # ires \<and> Oc # xs = Oc # Bk \<up> rn; hd l = Oc\<rbrakk> \<Longrightarrow> \<exists>ln rn m1 m2. m1 + m2 = Suc (lm ! n) \<and> hd l # Oc # xs \<noteq> [] \<and> (hd (hd l # Oc # xs) = Oc \<longrightarrow> tl l = Oc \<up> m1 @ Bk \<up> ln @ Bk # Bk # ires \<and> hd l # Oc # xs = Oc \<up> m2 @ Bk \<up> rn) \<and> (hd (hd l # Oc # xs) = Bk \<longrightarrow> tl l = Bk \<up> ln @ Bk # ires \<and> hd l # Oc # xs = Bk # Oc \<up> (m1 + m2) @ Bk \<up> rn)
[PROOF STEP]
apply(rule_tac x = Lnl in exI, rule_tac x = "length xs" in exI, auto)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>Lnl rn. \<lbrakk>hd (Oc \<up> lm ! n @ Bk \<up> Lnl @ Bk # Bk # ires) = Oc; l = Oc \<up> lm ! n @ Bk \<up> Lnl @ Bk # Bk # ires; xs = Bk \<up> rn\<rbrakk> \<Longrightarrow> \<exists>m1 m2. m1 + m2 = Suc (lm ! n) \<and> tl (Oc \<up> lm ! n @ Bk \<up> Lnl @ Bk # Bk # ires) = Oc \<up> m1 @ Bk \<up> Lnl @ Bk # Bk # ires \<and> [Oc, Oc] = Oc \<up> m2
[PROOF STEP]
apply(cases "lm ! n", simp)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>Lnl rn. \<lbrakk>hd (Bk \<up> Lnl @ Bk # Bk # ires) = Oc; l = Bk \<up> Lnl @ Bk # Bk # ires; xs = Bk \<up> rn; lm ! n = 0\<rbrakk> \<Longrightarrow> \<exists>m1 m2. m1 + m2 = Suc 0 \<and> tl (Bk \<up> Lnl @ Bk # Bk # ires) = Oc \<up> m1 @ Bk \<up> Lnl @ Bk # Bk # ires \<and> [Oc, Oc] = Oc \<up> m2
 2. \<And>Lnl rn nat. \<lbrakk>hd (Oc \<up> lm ! n @ Bk \<up> Lnl @ Bk # Bk # ires) = Oc; l = Oc \<up> lm ! n @ Bk \<up> Lnl @ Bk # Bk # ires; xs = Bk \<up> rn; lm ! n = Suc nat\<rbrakk> \<Longrightarrow> \<exists>m1 m2. m1 + m2 = Suc (lm ! n) \<and> tl (Oc \<up> lm ! n @ Bk \<up> Lnl @ Bk # Bk # ires) = Oc \<up> m1 @ Bk \<up> Lnl @ Bk # Bk # ires \<and> [Oc, Oc] = Oc \<up> m2
[PROOF STEP]
apply(case_tac Lnl, simp_all add: numeral_2_eq_2)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma mopup_left_moving_nonempty_snd[simp]: "mopup_left_moving (2 * n + 5, l, xs) lm n ires \<Longrightarrow> l \<noteq> []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mopup_left_moving (2 * n + 5, l, xs) lm n ires \<Longrightarrow> l \<noteq> []
[PROOF STEP]
apply(auto simp: mopup_left_moving.simps)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma mopup_left_moving_hd_Bk[simp]:
  "\<lbrakk>mopup_left_moving (2 * n + 5, l, Bk # xs) lm n ires\<rbrakk>
 \<Longrightarrow> mopup_left_moving (2 * n + 5, tl l, hd l # Bk # xs) lm n ires"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mopup_left_moving (2 * n + 5, l, Bk # xs) lm n ires \<Longrightarrow> mopup_left_moving (2 * n + 5, tl l, hd l # Bk # xs) lm n ires
[PROOF STEP]
apply(simp only: mopup_left_moving.simps)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>lnl lnr rn m. m = Suc (lm ! n) \<and> (l = Bk \<up> lnr @ Oc \<up> m @ Bk \<up> lnl @ Bk # Bk # ires \<and> Bk # xs = Bk \<up> rn \<or> l = Oc \<up> (m - 1) @ Bk \<up> lnl @ Bk # Bk # ires \<and> Bk # xs = Oc # Bk \<up> rn) \<Longrightarrow> \<exists>lnl lnr rn m. m = Suc (lm ! n) \<and> (tl l = Bk \<up> lnr @ Oc \<up> m @ Bk \<up> lnl @ Bk # Bk # ires \<and> hd l # Bk # xs = Bk \<up> rn \<or> tl l = Oc \<up> (m - 1) @ Bk \<up> lnl @ Bk # Bk # ires \<and> hd l # Bk # xs = Oc # Bk \<up> rn)
[PROOF STEP]
apply(erule exE)+
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>lnl lnr rn m. m = Suc (lm ! n) \<and> (l = Bk \<up> lnr @ Oc \<up> m @ Bk \<up> lnl @ Bk # Bk # ires \<and> Bk # xs = Bk \<up> rn \<or> l = Oc \<up> (m - 1) @ Bk \<up> lnl @ Bk # Bk # ires \<and> Bk # xs = Oc # Bk \<up> rn) \<Longrightarrow> \<exists>lnl lnr rn m. m = Suc (lm ! n) \<and> (tl l = Bk \<up> lnr @ Oc \<up> m @ Bk \<up> lnl @ Bk # Bk # ires \<and> hd l # Bk # xs = Bk \<up> rn \<or> tl l = Oc \<up> (m - 1) @ Bk \<up> lnl @ Bk # Bk # ires \<and> hd l # Bk # xs = Oc # Bk \<up> rn)
[PROOF STEP]
apply(rename_tac lnl Lnr rn m)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>lnl Lnr rn m. m = Suc (lm ! n) \<and> (l = Bk \<up> Lnr @ Oc \<up> m @ Bk \<up> lnl @ Bk # Bk # ires \<and> Bk # xs = Bk \<up> rn \<or> l = Oc \<up> (m - 1) @ Bk \<up> lnl @ Bk # Bk # ires \<and> Bk # xs = Oc # Bk \<up> rn) \<Longrightarrow> \<exists>lnl lnr rn m. m = Suc (lm ! n) \<and> (tl l = Bk \<up> lnr @ Oc \<up> m @ Bk \<up> lnl @ Bk # Bk # ires \<and> hd l # Bk # xs = Bk \<up> rn \<or> tl l = Oc \<up> (m - 1) @ Bk \<up> lnl @ Bk # Bk # ires \<and> hd l # Bk # xs = Oc # Bk \<up> rn)
[PROOF STEP]
apply(case_tac Lnr, auto)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma mopup_left_moving_emptylist[simp]:
  "\<lbrakk>mopup_left_moving (2 * n + 5, l, []) lm n ires\<rbrakk>
    \<Longrightarrow> mopup_left_moving (2 * n + 5, tl l, [hd l]) lm n ires"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mopup_left_moving (2 * n + 5, l, []) lm n ires \<Longrightarrow> mopup_left_moving (2 * n + 5, tl l, [hd l]) lm n ires
[PROOF STEP]
apply(simp only: mopup_left_moving.simps)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>lnl lnr rn m. m = Suc (lm ! n) \<and> (l = Bk \<up> lnr @ Oc \<up> m @ Bk \<up> lnl @ Bk # Bk # ires \<and> [] = Bk \<up> rn \<or> l = Oc \<up> (m - 1) @ Bk \<up> lnl @ Bk # Bk # ires \<and> [] = Oc # Bk \<up> rn) \<Longrightarrow> \<exists>lnl lnr rn m. m = Suc (lm ! n) \<and> (tl l = Bk \<up> lnr @ Oc \<up> m @ Bk \<up> lnl @ Bk # Bk # ires \<and> [hd l] = Bk \<up> rn \<or> tl l = Oc \<up> (m - 1) @ Bk \<up> lnl @ Bk # Bk # ires \<and> [hd l] = Oc # Bk \<up> rn)
[PROOF STEP]
apply(erule exE)+
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>lnl lnr rn m. m = Suc (lm ! n) \<and> (l = Bk \<up> lnr @ Oc \<up> m @ Bk \<up> lnl @ Bk # Bk # ires \<and> [] = Bk \<up> rn \<or> l = Oc \<up> (m - 1) @ Bk \<up> lnl @ Bk # Bk # ires \<and> [] = Oc # Bk \<up> rn) \<Longrightarrow> \<exists>lnl lnr rn m. m = Suc (lm ! n) \<and> (tl l = Bk \<up> lnr @ Oc \<up> m @ Bk \<up> lnl @ Bk # Bk # ires \<and> [hd l] = Bk \<up> rn \<or> tl l = Oc \<up> (m - 1) @ Bk \<up> lnl @ Bk # Bk # ires \<and> [hd l] = Oc # Bk \<up> rn)
[PROOF STEP]
apply(rename_tac lnl Lnr rn m)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>lnl Lnr rn m. m = Suc (lm ! n) \<and> (l = Bk \<up> Lnr @ Oc \<up> m @ Bk \<up> lnl @ Bk # Bk # ires \<and> [] = Bk \<up> rn \<or> l = Oc \<up> (m - 1) @ Bk \<up> lnl @ Bk # Bk # ires \<and> [] = Oc # Bk \<up> rn) \<Longrightarrow> \<exists>lnl lnr rn m. m = Suc (lm ! n) \<and> (tl l = Bk \<up> lnr @ Oc \<up> m @ Bk \<up> lnl @ Bk # Bk # ires \<and> [hd l] = Bk \<up> rn \<or> tl l = Oc \<up> (m - 1) @ Bk \<up> lnl @ Bk # Bk # ires \<and> [hd l] = Oc # Bk \<up> rn)
[PROOF STEP]
apply(case_tac Lnr, auto)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>lnl nat. l = Bk # Bk \<up> nat @ Oc # Oc \<up> lm ! n @ Bk \<up> lnl @ Bk # Bk # ires \<Longrightarrow> \<exists>rn. [Bk] = Bk \<up> rn
[PROOF STEP]
apply(rule_tac x = 1 in exI, simp)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma mopup_jump_over2_Oc_nonempty[simp]:
  "mopup_jump_over2 (2 * n + 6, l, Oc # xs) lm n ires \<Longrightarrow> l \<noteq> []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mopup_jump_over2 (2 * n + 6, l, Oc # xs) lm n ires \<Longrightarrow> l \<noteq> []
[PROOF STEP]
apply(auto simp: mopup_jump_over2.simps )
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma mopup_jump_over2_context[simp]:
  "\<lbrakk>mopup_jump_over2 (2 * n + 6, l, Oc # xs) lm n ires\<rbrakk>
 \<Longrightarrow>  mopup_jump_over2 (2 * n + 6, tl l, hd l # Oc # xs) lm n ires"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mopup_jump_over2 (2 * n + 6, l, Oc # xs) lm n ires \<Longrightarrow> mopup_jump_over2 (2 * n + 6, tl l, hd l # Oc # xs) lm n ires
[PROOF STEP]
apply(simp only: mopup_jump_over2.simps)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>ln rn m1 m2. m1 + m2 = Suc (lm ! n) \<and> Oc # xs \<noteq> [] \<and> (hd (Oc # xs) = Oc \<longrightarrow> l = Oc \<up> m1 @ Bk \<up> ln @ Bk # Bk # ires \<and> Oc # xs = Oc \<up> m2 @ Bk \<up> rn) \<and> (hd (Oc # xs) = Bk \<longrightarrow> l = Bk \<up> ln @ Bk # ires \<and> Oc # xs = Bk # Oc \<up> (m1 + m2) @ Bk \<up> rn) \<Longrightarrow> \<exists>ln rn m1 m2. m1 + m2 = Suc (lm ! n) \<and> hd l # Oc # xs \<noteq> [] \<and> (hd (hd l # Oc # xs) = Oc \<longrightarrow> tl l = Oc \<up> m1 @ Bk \<up> ln @ Bk # Bk # ires \<and> hd l # Oc # xs = Oc \<up> m2 @ Bk \<up> rn) \<and> (hd (hd l # Oc # xs) = Bk \<longrightarrow> tl l = Bk \<up> ln @ Bk # ires \<and> hd l # Oc # xs = Bk # Oc \<up> (m1 + m2) @ Bk \<up> rn)
[PROOF STEP]
apply(erule_tac exE)+
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>ln rn m1 m2. m1 + m2 = Suc (lm ! n) \<and> Oc # xs \<noteq> [] \<and> (hd (Oc # xs) = Oc \<longrightarrow> l = Oc \<up> m1 @ Bk \<up> ln @ Bk # Bk # ires \<and> Oc # xs = Oc \<up> m2 @ Bk \<up> rn) \<and> (hd (Oc # xs) = Bk \<longrightarrow> l = Bk \<up> ln @ Bk # ires \<and> Oc # xs = Bk # Oc \<up> (m1 + m2) @ Bk \<up> rn) \<Longrightarrow> \<exists>ln rn m1 m2. m1 + m2 = Suc (lm ! n) \<and> hd l # Oc # xs \<noteq> [] \<and> (hd (hd l # Oc # xs) = Oc \<longrightarrow> tl l = Oc \<up> m1 @ Bk \<up> ln @ Bk # Bk # ires \<and> hd l # Oc # xs = Oc \<up> m2 @ Bk \<up> rn) \<and> (hd (hd l # Oc # xs) = Bk \<longrightarrow> tl l = Bk \<up> ln @ Bk # ires \<and> hd l # Oc # xs = Bk # Oc \<up> (m1 + m2) @ Bk \<up> rn)
[PROOF STEP]
apply(simp, erule conjE, erule_tac conjE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>ln rn m1 m2. \<lbrakk>m1 + m2 = Suc (lm ! n); l = Oc \<up> m1 @ Bk \<up> ln @ Bk # Bk # ires; Oc # xs = Oc \<up> m2 @ Bk \<up> rn\<rbrakk> \<Longrightarrow> \<exists>lna rna m1a m2a. m1a + m2a = Suc (lm ! n) \<and> (hd (Oc \<up> m1 @ Bk \<up> ln @ Bk # Bk # ires) = Oc \<longrightarrow> tl (Oc \<up> m1 @ Bk \<up> ln @ Bk # Bk # ires) = Oc \<up> m1a @ Bk \<up> lna @ Bk # Bk # ires \<and> Oc # Oc \<up> m2 @ Bk \<up> rn = Oc \<up> m2a @ Bk \<up> rna) \<and> (hd (Oc \<up> m1 @ Bk \<up> ln @ Bk # Bk # ires) = Bk \<longrightarrow> tl (Oc \<up> m1 @ Bk \<up> ln @ Bk # Bk # ires) = Bk \<up> lna @ Bk # ires \<and> Oc \<up> m2 @ Bk \<up> rn = Oc \<up> (m1a + m2a) @ Bk \<up> rna)
[PROOF STEP]
apply(rename_tac Ln Rn M1 M2)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>Ln Rn M1 M2. \<lbrakk>M1 + M2 = Suc (lm ! n); l = Oc \<up> M1 @ Bk \<up> Ln @ Bk # Bk # ires; Oc # xs = Oc \<up> M2 @ Bk \<up> Rn\<rbrakk> \<Longrightarrow> \<exists>ln rn m1 m2. m1 + m2 = Suc (lm ! n) \<and> (hd (Oc \<up> M1 @ Bk \<up> Ln @ Bk # Bk # ires) = Oc \<longrightarrow> tl (Oc \<up> M1 @ Bk \<up> Ln @ Bk # Bk # ires) = Oc \<up> m1 @ Bk \<up> ln @ Bk # Bk # ires \<and> Oc # Oc \<up> M2 @ Bk \<up> Rn = Oc \<up> m2 @ Bk \<up> rn) \<and> (hd (Oc \<up> M1 @ Bk \<up> Ln @ Bk # Bk # ires) = Bk \<longrightarrow> tl (Oc \<up> M1 @ Bk \<up> Ln @ Bk # Bk # ires) = Bk \<up> ln @ Bk # ires \<and> Oc \<up> M2 @ Bk \<up> Rn = Oc \<up> (m1 + m2) @ Bk \<up> rn)
[PROOF STEP]
apply(case_tac M1, simp)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>Ln Rn M1. \<lbrakk>l = Bk \<up> Ln @ Bk # Bk # ires; xs = Oc \<up> lm ! n @ Bk \<up> Rn; M1 = 0\<rbrakk> \<Longrightarrow> \<exists>ln rn m1 m2. m1 + m2 = Suc (lm ! n) \<and> (hd (Bk \<up> Ln @ Bk # Bk # ires) = Oc \<longrightarrow> tl (Bk \<up> Ln @ Bk # Bk # ires) = Oc \<up> m1 @ Bk \<up> ln @ Bk # Bk # ires \<and> Oc # Oc # Oc \<up> lm ! n @ Bk \<up> Rn = Oc \<up> m2 @ Bk \<up> rn) \<and> (hd (Bk \<up> Ln @ Bk # Bk # ires) = Bk \<longrightarrow> tl (Bk \<up> Ln @ Bk # Bk # ires) = Bk \<up> ln @ Bk # ires \<and> Oc # Oc \<up> lm ! n @ Bk \<up> Rn = Oc \<up> (m1 + m2) @ Bk \<up> rn)
 2. \<And>Ln Rn M1 M2 nat. \<lbrakk>M1 + M2 = Suc (lm ! n); l = Oc \<up> M1 @ Bk \<up> Ln @ Bk # Bk # ires; Oc # xs = Oc \<up> M2 @ Bk \<up> Rn; M1 = Suc nat\<rbrakk> \<Longrightarrow> \<exists>ln rn m1 m2. m1 + m2 = Suc (lm ! n) \<and> (hd (Oc \<up> M1 @ Bk \<up> Ln @ Bk # Bk # ires) = Oc \<longrightarrow> tl (Oc \<up> M1 @ Bk \<up> Ln @ Bk # Bk # ires) = Oc \<up> m1 @ Bk \<up> ln @ Bk # Bk # ires \<and> Oc # Oc \<up> M2 @ Bk \<up> Rn = Oc \<up> m2 @ Bk \<up> rn) \<and> (hd (Oc \<up> M1 @ Bk \<up> Ln @ Bk # Bk # ires) = Bk \<longrightarrow> tl (Oc \<up> M1 @ Bk \<up> Ln @ Bk # Bk # ires) = Bk \<up> ln @ Bk # ires \<and> Oc \<up> M2 @ Bk \<up> Rn = Oc \<up> (m1 + m2) @ Bk \<up> rn)
[PROOF STEP]
apply(rule_tac x = Ln in exI, rule_tac x = Rn in exI,
      rule_tac x = 0 in exI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>Ln Rn M1. \<lbrakk>l = Bk \<up> Ln @ Bk # Bk # ires; xs = Oc \<up> lm ! n @ Bk \<up> Rn; M1 = 0\<rbrakk> \<Longrightarrow> \<exists>m2. 0 + m2 = Suc (lm ! n) \<and> (hd (Bk \<up> Ln @ Bk # Bk # ires) = Oc \<longrightarrow> tl (Bk \<up> Ln @ Bk # Bk # ires) = Oc \<up> 0 @ Bk \<up> Ln @ Bk # Bk # ires \<and> Oc # Oc # Oc \<up> lm ! n @ Bk \<up> Rn = Oc \<up> m2 @ Bk \<up> Rn) \<and> (hd (Bk \<up> Ln @ Bk # Bk # ires) = Bk \<longrightarrow> tl (Bk \<up> Ln @ Bk # Bk # ires) = Bk \<up> Ln @ Bk # ires \<and> Oc # Oc \<up> lm ! n @ Bk \<up> Rn = Oc \<up> (0 + m2) @ Bk \<up> Rn)
 2. \<And>Ln Rn M1 M2 nat. \<lbrakk>M1 + M2 = Suc (lm ! n); l = Oc \<up> M1 @ Bk \<up> Ln @ Bk # Bk # ires; Oc # xs = Oc \<up> M2 @ Bk \<up> Rn; M1 = Suc nat\<rbrakk> \<Longrightarrow> \<exists>ln rn m1 m2. m1 + m2 = Suc (lm ! n) \<and> (hd (Oc \<up> M1 @ Bk \<up> Ln @ Bk # Bk # ires) = Oc \<longrightarrow> tl (Oc \<up> M1 @ Bk \<up> Ln @ Bk # Bk # ires) = Oc \<up> m1 @ Bk \<up> ln @ Bk # Bk # ires \<and> Oc # Oc \<up> M2 @ Bk \<up> Rn = Oc \<up> m2 @ Bk \<up> rn) \<and> (hd (Oc \<up> M1 @ Bk \<up> Ln @ Bk # Bk # ires) = Bk \<longrightarrow> tl (Oc \<up> M1 @ Bk \<up> Ln @ Bk # Bk # ires) = Bk \<up> ln @ Bk # ires \<and> Oc \<up> M2 @ Bk \<up> Rn = Oc \<up> (m1 + m2) @ Bk \<up> rn)
[PROOF STEP]
apply(case_tac Ln, simp, simp, simp only: exp_ind[THEN sym], simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>Ln Rn M1 M2 nat. \<lbrakk>M1 + M2 = Suc (lm ! n); l = Oc \<up> M1 @ Bk \<up> Ln @ Bk # Bk # ires; Oc # xs = Oc \<up> M2 @ Bk \<up> Rn; M1 = Suc nat\<rbrakk> \<Longrightarrow> \<exists>ln rn m1 m2. m1 + m2 = Suc (lm ! n) \<and> (hd (Oc \<up> M1 @ Bk \<up> Ln @ Bk # Bk # ires) = Oc \<longrightarrow> tl (Oc \<up> M1 @ Bk \<up> Ln @ Bk # Bk # ires) = Oc \<up> m1 @ Bk \<up> ln @ Bk # Bk # ires \<and> Oc # Oc \<up> M2 @ Bk \<up> Rn = Oc \<up> m2 @ Bk \<up> rn) \<and> (hd (Oc \<up> M1 @ Bk \<up> Ln @ Bk # Bk # ires) = Bk \<longrightarrow> tl (Oc \<up> M1 @ Bk \<up> Ln @ Bk # Bk # ires) = Bk \<up> ln @ Bk # ires \<and> Oc \<up> M2 @ Bk \<up> Rn = Oc \<up> (m1 + m2) @ Bk \<up> rn)
[PROOF STEP]
apply(rule_tac x = Ln in exI, rule_tac x = Rn in exI,
      rule_tac x = "M1-1" in exI, rule_tac x = "Suc M2" in exI, simp)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma mopup_stop_via_jump_over2[simp]:
  "\<lbrakk>mopup_jump_over2 (2 * n + 6, l, Bk # xs) lm n ires\<rbrakk>
  \<Longrightarrow> mopup_stop (0, Bk # l, xs) lm n ires"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mopup_jump_over2 (2 * n + 6, l, Bk # xs) lm n ires \<Longrightarrow> mopup_stop (0, Bk # l, xs) lm n ires
[PROOF STEP]
apply(auto simp: mopup_jump_over2.simps mopup_stop.simps tape_of_nat_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>ln rn m1 m2. \<lbrakk>m1 + m2 = Suc (lm ! n); xs = Oc # Oc \<up> lm ! n @ Bk \<up> rn; l = Bk \<up> ln @ Bk # ires\<rbrakk> \<Longrightarrow> \<exists>lna. Bk # Bk \<up> ln = Bk \<up> lna @ [Bk]
[PROOF STEP]
apply(simp add: exp_ind[THEN sym])
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma mopup_jump_over2_nonempty[simp]: "mopup_jump_over2 (2 * n + 6, l, []) lm n ires = False"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mopup_jump_over2 (2 * n + 6, l, []) lm n ires = False
[PROOF STEP]
by(auto simp: mopup_jump_over2.simps)


[STATEMENT]
lemma mod_ex2: "(a mod (2::nat) = 0) = (\<exists> q. a = 2 * q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_even a = (\<exists>q. a = 2 * q)
[PROOF STEP]
by arith


[STATEMENT]
lemma mod_2: "x mod 2  = 0 \<or>  x mod 2 = Suc 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_even x \<or> x mod 2 = Suc 0
[PROOF STEP]
by arith


[STATEMENT]
lemma mopup_inv_step:
  "\<lbrakk>n < length lm; mopup_inv (s, l, r) lm n ires\<rbrakk>
  \<Longrightarrow> mopup_inv (step (s, l, r) (mopup_a n @ shift mopup_b (2 * n), 0)) lm n ires"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n < length lm; mopup_inv (s, l, r) lm n ires\<rbrakk> \<Longrightarrow> mopup_inv (step0 (s, l, r) (mopup_a n @ shift mopup_b (2 * n))) lm n ires
[PROOF STEP]
apply(cases r;cases "hd r")
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<lbrakk>n < length lm; mopup_inv (s, l, r) lm n ires; r = []; hd r = Bk\<rbrakk> \<Longrightarrow> mopup_inv (step0 (s, l, r) (mopup_a n @ shift mopup_b (2 * n))) lm n ires
 2. \<lbrakk>n < length lm; mopup_inv (s, l, r) lm n ires; r = []; hd r = Oc\<rbrakk> \<Longrightarrow> mopup_inv (step0 (s, l, r) (mopup_a n @ shift mopup_b (2 * n))) lm n ires
 3. \<And>a list. \<lbrakk>n < length lm; mopup_inv (s, l, r) lm n ires; r = a # list; hd r = Bk\<rbrakk> \<Longrightarrow> mopup_inv (step0 (s, l, r) (mopup_a n @ shift mopup_b (2 * n))) lm n ires
 4. \<And>a list. \<lbrakk>n < length lm; mopup_inv (s, l, r) lm n ires; r = a # list; hd r = Oc\<rbrakk> \<Longrightarrow> mopup_inv (step0 (s, l, r) (mopup_a n @ shift mopup_b (2 * n))) lm n ires
[PROOF STEP]
apply(auto split:if_splits simp add:step.simps mopupfetchs fetch.simps(1))
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<lbrakk>r = []; hd [] = Bk; n < length lm; 0 < s; s \<le> 2 * n; s mod 2 = Suc 0; mopup_bef_erase_a (s, l, []) lm n ires; Suc s \<noteq> 2 * n; \<not> Suc (Suc s) \<le> 2 * n\<rbrakk> \<Longrightarrow> mopup_aft_erase_a (Suc (Suc s), Bk # l, []) lm n ires
 2. \<lbrakk>r = []; hd [] = Oc; n < length lm; 0 < s; s \<le> 2 * n; s mod 2 = Suc 0; mopup_bef_erase_a (s, l, []) lm n ires; Suc s \<noteq> 2 * n; \<not> Suc (Suc s) \<le> 2 * n\<rbrakk> \<Longrightarrow> mopup_aft_erase_a (Suc (Suc s), Bk # l, []) lm n ires
 3. \<And>list. \<lbrakk>r = Bk # list; n < length lm; 0 < s; s \<le> 2 * n; s mod 2 = Suc 0; mopup_bef_erase_a (s, l, Bk # list) lm n ires; Suc s \<noteq> 2 * n; \<not> Suc (Suc s) \<le> 2 * n\<rbrakk> \<Longrightarrow> mopup_aft_erase_a (Suc (Suc s), Bk # l, list) lm n ires
 4. \<And>list. \<lbrakk>r = Oc # list; n < length lm; 0 < s; s mod 2 = Suc 0; mopup_bef_erase_a (s, l, Oc # list) lm n ires; Suc s mod 2 = Suc 0; Suc s \<le> 2 * n\<rbrakk> \<Longrightarrow> mopup_bef_erase_a (Suc s, l, Bk # list) lm n ires
 5. \<And>list. \<lbrakk>r = Oc # list; n < length lm; 0 < s; s \<le> 2 * n; mopup_bef_erase_b (s, l, Oc # list) lm n ires; even s\<rbrakk> \<Longrightarrow> mopup_inv (case fetch (mopup_a n @ shift mopup_b (2 * n)) s Oc of (a, s') \<Rightarrow> (s', update a (l, Oc # list))) lm n ires
[PROOF STEP]
apply(drule_tac mopup_false2, simp_all add: mopup_bef_erase_b.simps)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>r = []; hd [] = Oc; n < length lm; 0 < s; s \<le> 2 * n; s mod 2 = Suc 0; mopup_bef_erase_a (s, l, []) lm n ires; Suc s \<noteq> 2 * n; \<not> Suc (Suc s) \<le> 2 * n\<rbrakk> \<Longrightarrow> mopup_aft_erase_a (Suc (Suc s), Bk # l, []) lm n ires
 2. \<And>list. \<lbrakk>r = Bk # list; n < length lm; 0 < s; s \<le> 2 * n; s mod 2 = Suc 0; mopup_bef_erase_a (s, l, Bk # list) lm n ires; Suc s \<noteq> 2 * n; \<not> Suc (Suc s) \<le> 2 * n\<rbrakk> \<Longrightarrow> mopup_aft_erase_a (Suc (Suc s), Bk # l, list) lm n ires
 3. \<And>list. \<lbrakk>r = Oc # list; n < length lm; 0 < s; s mod 2 = Suc 0; mopup_bef_erase_a (s, l, Oc # list) lm n ires; Suc s mod 2 = Suc 0; Suc s \<le> 2 * n\<rbrakk> \<Longrightarrow> mopup_bef_erase_a (Suc s, l, Bk # list) lm n ires
[PROOF STEP]
apply(drule_tac mopup_false2, simp_all)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>list. \<lbrakk>r = Bk # list; n < length lm; 0 < s; s \<le> 2 * n; s mod 2 = Suc 0; mopup_bef_erase_a (s, l, Bk # list) lm n ires; Suc s \<noteq> 2 * n; \<not> Suc (Suc s) \<le> 2 * n\<rbrakk> \<Longrightarrow> mopup_aft_erase_a (Suc (Suc s), Bk # l, list) lm n ires
 2. \<And>list. \<lbrakk>r = Oc # list; n < length lm; 0 < s; s mod 2 = Suc 0; mopup_bef_erase_a (s, l, Oc # list) lm n ires; Suc s mod 2 = Suc 0; Suc s \<le> 2 * n\<rbrakk> \<Longrightarrow> mopup_bef_erase_a (Suc s, l, Bk # list) lm n ires
[PROOF STEP]
apply(drule_tac mopup_false2, simp_all)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>list. \<lbrakk>r = Oc # list; n < length lm; 0 < s; s mod 2 = Suc 0; mopup_bef_erase_a (s, l, Oc # list) lm n ires; Suc s mod 2 = Suc 0; Suc s \<le> 2 * n\<rbrakk> \<Longrightarrow> mopup_bef_erase_a (Suc s, l, Bk # list) lm n ires
[PROOF STEP]
by presburger


[STATEMENT]
lemma mopup_inv_steps:
  "\<lbrakk>n < length lm; mopup_inv (s, l, r) lm n ires\<rbrakk> \<Longrightarrow>
     mopup_inv (steps (s, l, r) (mopup_a n @ shift mopup_b (2 * n), 0)  stp) lm n ires"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n < length lm; mopup_inv (s, l, r) lm n ires\<rbrakk> \<Longrightarrow> mopup_inv (steps0 (s, l, r) (mopup_a n @ shift mopup_b (2 * n)) stp) lm n ires
[PROOF STEP]
proof(induct stp)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>n < length lm; mopup_inv (s, l, r) lm n ires\<rbrakk> \<Longrightarrow> mopup_inv (steps0 (s, l, r) (mopup_a n @ shift mopup_b (2 * n)) 0) lm n ires
 2. \<And>stp. \<lbrakk>\<lbrakk>n < length lm; mopup_inv (s, l, r) lm n ires\<rbrakk> \<Longrightarrow> mopup_inv (steps0 (s, l, r) (mopup_a n @ shift mopup_b (2 * n)) stp) lm n ires; n < length lm; mopup_inv (s, l, r) lm n ires\<rbrakk> \<Longrightarrow> mopup_inv (steps0 (s, l, r) (mopup_a n @ shift mopup_b (2 * n)) (Suc stp)) lm n ires
[PROOF STEP]
case (Suc stp)
[PROOF STATE]
proof (state)
this:
\<lbrakk>n < length lm; mopup_inv (s, l, r) lm n ires\<rbrakk> \<Longrightarrow> mopup_inv (steps0 (s, l, r) (mopup_a n @ shift mopup_b (2 * n)) stp) lm n ires
n < length lm
mopup_inv (s, l, r) lm n ires

goal (2 subgoals):
 1. \<lbrakk>n < length lm; mopup_inv (s, l, r) lm n ires\<rbrakk> \<Longrightarrow> mopup_inv (steps0 (s, l, r) (mopup_a n @ shift mopup_b (2 * n)) 0) lm n ires
 2. \<And>stp. \<lbrakk>\<lbrakk>n < length lm; mopup_inv (s, l, r) lm n ires\<rbrakk> \<Longrightarrow> mopup_inv (steps0 (s, l, r) (mopup_a n @ shift mopup_b (2 * n)) stp) lm n ires; n < length lm; mopup_inv (s, l, r) lm n ires\<rbrakk> \<Longrightarrow> mopup_inv (steps0 (s, l, r) (mopup_a n @ shift mopup_b (2 * n)) (Suc stp)) lm n ires
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>n < length lm; mopup_inv (s, l, r) lm n ires\<rbrakk> \<Longrightarrow> mopup_inv (steps0 (s, l, r) (mopup_a n @ shift mopup_b (2 * n)) stp) lm n ires
n < length lm
mopup_inv (s, l, r) lm n ires
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>n < length lm; mopup_inv (s, l, r) lm n ires\<rbrakk> \<Longrightarrow> mopup_inv (steps0 (s, l, r) (mopup_a n @ shift mopup_b (2 * n)) stp) lm n ires
n < length lm
mopup_inv (s, l, r) lm n ires

goal (1 subgoal):
 1. mopup_inv (steps0 (s, l, r) (mopup_a n @ shift mopup_b (2 * n)) (Suc stp)) lm n ires
[PROOF STEP]
by ( cases "steps (s, l, r)
                (mopup_a n @ shift mopup_b (2 * n), 0) stp"
        , auto simp add: steps.simps intro:mopup_inv_step)
[PROOF STATE]
proof (state)
this:
mopup_inv (steps0 (s, l, r) (mopup_a n @ shift mopup_b (2 * n)) (Suc stp)) lm n ires

goal (1 subgoal):
 1. \<lbrakk>n < length lm; mopup_inv (s, l, r) lm n ires\<rbrakk> \<Longrightarrow> mopup_inv (steps0 (s, l, r) (mopup_a n @ shift mopup_b (2 * n)) 0) lm n ires
[PROOF STEP]
qed (auto simp add: steps.simps)


[STATEMENT]
lemma wf_abc_mopup_measure:
  shows "wf abc_mopup_measure"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf abc_mopup_measure
[PROOF STEP]
unfolding abc_mopup_measure_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf (measures [\<lambda>(x, y). abc_mopup_stage1 x y, \<lambda>(x, y). abc_mopup_stage2 x y, \<lambda>(x, y). abc_mopup_stage3 x y])
[PROOF STEP]
by auto