[STATEMENT]
lemma hypext_fun_polyn:
    fixes coef :: "nat \<Rightarrow> 'a :: {real_normed_field}"
      and n :: nat
  assumes "f twice_field_differentiable_at (Base x)"
    shows "(*h* (\<lambda>x. \<Sum>i<n. coef i * (f x)^i)) x = (\<Sum>i<n. (coef i) *\<^sub>H (((*h* f) x)^i))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (*h* (\<lambda>x. \<Sum>i<n. coef i * f x ^ i)) x = (\<Sum>i<n. coef i *\<^sub>H (*h* f) x ^ i)
[PROOF STEP]
using assms hypext_compose[of f x "\<lambda>x. (\<Sum>i<n. coef i * x^i)"]
[PROOF STATE]
proof (prove)
using this:
f twice_field_differentiable_at Base x
\<lbrakk>f twice_field_differentiable_at Base x; (\<lambda>x. \<Sum>i<n. coef i * x ^ i) twice_field_differentiable_at f (Base x)\<rbrakk> \<Longrightarrow> (*h* (\<lambda>x. \<Sum>i<n. coef i * f x ^ i)) x = (*h* (\<lambda>x. \<Sum>i<n. coef i * x ^ i)) ((*h* f) x)

goal (1 subgoal):
 1. (*h* (\<lambda>x. \<Sum>i<n. coef i * f x ^ i)) x = (\<Sum>i<n. coef i *\<^sub>H (*h* f) x ^ i)
[PROOF STEP]
by (simp add: hypext_polyn)


[STATEMENT]
lemma fresh2_notIn: "finite xs \<Longrightarrow> fresh2 xs x y \<notin> xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite xs \<Longrightarrow> fresh2 xs x y \<notin> xs
[PROOF STEP]
by (induct xs x y rule: fresh2.induct) auto


[STATEMENT]
lemma fresh2_eq: "x \<notin> xs \<Longrightarrow> fresh2 xs x y = x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<notin> xs \<Longrightarrow> fresh2 xs x y = x
[PROOF STEP]
by auto


[STATEMENT]
lemma fresh2_list[code]:
  "fresh2 (set xs) x y =
     (if x \<notin> set xs then x else
      if y \<notin> set xs then y else
      fresh2 (set xs) (x-1) (y+1))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fresh2 (set xs) x y = (if x \<notin> set xs then x else if y \<notin> set xs then y else fresh2 (set xs) (x - 1) (y + 1))
[PROOF STEP]
by (auto simp: fresh2.simps)


[STATEMENT]
lemma iexec_offset_aux:
 "(i :: int) + 1 - j = i - j + 1 \<and> i + j - k + 1 = i - k + j + 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i + 1 - j = i - j + 1 \<and> i + j - k + 1 = i - k + j + 1
[PROOF STEP]
by simp


[STATEMENT]
lemma iexec_offset [intro]:
 "(ins, pc, s, stk) \<mapsto> (pc', s', stk') \<Longrightarrow>
    (ins, pc - i, s, stk) \<mapsto> (pc' - i, s', stk')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (ins, pc, s, stk) \<mapsto> (pc', s', stk') \<Longrightarrow> (ins, pc - i, s, stk) \<mapsto> (pc' - i, s', stk')
[PROOF STEP]
by (erule iexec.cases, auto simp: iexec_offset_aux)


[STATEMENT]
lemma execl_next:
 "\<lbrakk>P \<Turnstile> cfs; k < length cfs; k \<noteq> length cfs - 1\<rbrakk> \<Longrightarrow>
    (P !! fst (cfs ! k), cfs ! k) \<mapsto> cfs ! Suc k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>P \<Turnstile> cfs; k < length cfs; k \<noteq> length cfs - 1\<rbrakk> \<Longrightarrow> (P !! fst (cfs ! k), cfs ! k) \<mapsto> cfs ! Suc k
[PROOF STEP]
by (induction cfs arbitrary: k rule: execl.induct, auto
 simp: nth_Cons exec1_def split: nat.split)


[STATEMENT]
lemma execl_last:
 "\<lbrakk>P \<Turnstile> cfs; k < length cfs; fst (cfs ! k) \<notin> {0..<size P}\<rbrakk> \<Longrightarrow>
    length cfs - 1 = k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>P \<Turnstile> cfs; k < length cfs; fst (cfs ! k) \<notin> {0..<size P}\<rbrakk> \<Longrightarrow> length cfs - 1 = k
[PROOF STEP]
by (induction cfs arbitrary: k rule: execl.induct, auto
 simp: nth_Cons exec1_def split: nat.split_asm)


[STATEMENT]
lemma execl_drop:
 "P \<Turnstile> cfs \<Longrightarrow> P \<Turnstile> drop n cfs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<Turnstile> cfs \<Longrightarrow> P \<Turnstile> drop n cfs
[PROOF STEP]
by (induction cfs arbitrary: n rule: execl.induct,
 simp_all add: drop_Cons split: nat.split)


[STATEMENT]
lemma execl_all_N [simplified, intro]:
 "[LOADI i] \<Turnstile> cfs\<box> \<Longrightarrow> apred (N i) (cfs ! 0) (cfs ! (length cfs - 1))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [LOADI i] \<Turnstile> cfs\<box> \<Longrightarrow> apred (N i) (cfs ! 0) (cfs ! (length cfs - 1))
[PROOF STEP]
by (clarsimp simp: execl_all_def apred_def, cases "cfs ! 0",
 subgoal_tac "length cfs - 1 = 1", frule_tac [!] execl_next,
 ((rule ccontr)?, fastforce, (rule execl_last)?)+)


[STATEMENT]
lemma execl_all_V [simplified, intro]:
 "[LOAD x] \<Turnstile> cfs\<box> \<Longrightarrow> apred (V x) (cfs ! 0) (cfs ! (length cfs - 1))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [LOAD x] \<Turnstile> cfs\<box> \<Longrightarrow> apred (V x) (cfs ! 0) (cfs ! (length cfs - 1))
[PROOF STEP]
by (clarsimp simp: execl_all_def apred_def, cases "cfs ! 0",
 subgoal_tac "length cfs - 1 = 1", frule_tac [!] execl_next,
 ((rule ccontr)?, fastforce, (rule execl_last)?)+)


[STATEMENT]
lemma execl_all_Bc [simplified, intro]:
 "\<lbrakk>if v = f then [JMP i] else [] \<Turnstile> cfs\<box>; 0 \<le> i\<rbrakk> \<Longrightarrow>
    bpred (Bc v, f, i) (cfs ! 0) (cfs ! (length cfs - 1))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>if v = f then [JMP i] else [] \<Turnstile> cfs\<box>; 0 \<le> i\<rbrakk> \<Longrightarrow> bpred (Bc v, f, i) (cfs ! 0) (cfs ! (length cfs - 1))
[PROOF STEP]
by (clarsimp simp: execl_all_def bpred_def split: if_split_asm, cases "cfs ! 0",
 subgoal_tac "length cfs - 1 = 1", frule_tac [1-2] execl_next,
 ((rule ccontr)?, force, (rule execl_last)?)+, rule execl.cases [of "([], cfs)"],
 auto simp: exec1_def)


[STATEMENT]
lemma execl_all_SKIP [simplified, intro]:
 "[] \<Turnstile> cfs\<box> \<Longrightarrow> cpred SKIP (cfs ! 0) (cfs ! (length cfs - 1))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [] \<Turnstile> cfs\<box> \<Longrightarrow> cpred SKIP (cfs ! 0) (cfs ! (length cfs - 1))
[PROOF STEP]
by (rule execl.cases [of "([], cfs)"], auto simp: execl_all_def exec1_def cpred_def)


[STATEMENT]
lemma execl_sub_aux:
 "\<lbrakk>\<And>m n. \<forall>k \<in> {m..<n}. Q P' (((pc, s, stk) # cfs) ! k) \<Longrightarrow> P' \<Turnstile>
    map (off P) (case m of 0 \<Rightarrow> (pc, s, stk) # take n cfs | Suc m \<Rightarrow> F cfs m n);
    \<forall>k \<in> {m..<n+m+length cfs'}. Q P' ((cfs' @ (pc, s, stk) # cfs) ! (k-m))\<rbrakk> \<Longrightarrow>
  P' \<Turnstile> (pc - size P, s, stk) # map (off P) (take n cfs)"
  (is "\<lbrakk>\<And>_ _. \<forall>k \<in> _. Q P' (?F k) \<Longrightarrow> _; \<forall>k \<in> ?A. Q P' (?G k)\<rbrakk> \<Longrightarrow> _")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>m n. \<forall>k\<in>{m..<n}. Q P' (((pc, s, stk) # cfs) ! k) \<Longrightarrow> P' \<Turnstile> map (off P) (case m of 0 \<Rightarrow> (pc, s, stk) # take n cfs | Suc m \<Rightarrow> F cfs m n); \<forall>k\<in>{m..<n + m + length cfs'}. Q P' ((cfs' @ (pc, s, stk) # cfs) ! (k - m))\<rbrakk> \<Longrightarrow> P' \<Turnstile> (pc - size P, s, stk) # map (off P) (take n cfs)
[PROOF STEP]
by (subgoal_tac "\<forall>k \<in> {0..<n}. Q P' (?F k)", fastforce, subgoal_tac
 "\<forall>k \<in> {0..<n}. k + m + length cfs' \<in> ?A \<and> ?F k = ?G (k + m + length cfs')",
 fastforce, simp add: nth_append)


[STATEMENT]
lemma execl_sub:
 "\<lbrakk>P @ P' @ P'' \<Turnstile> cfs; \<forall>k \<in> {m..<n}.
     size P \<le> fst (cfs ! k) \<and> fst (cfs ! k) - size P < size P'\<rbrakk> \<Longrightarrow>
   P' \<Turnstile> map (off P) (drop m (take (Suc n) cfs))"
  (is "\<lbrakk>_; \<forall>k \<in> _. ?P P' cfs k\<rbrakk> \<Longrightarrow> P' \<Turnstile> map _ (?F cfs m (Suc n))")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>P @ P' @ P'' \<Turnstile> cfs; \<forall>k\<in>{m..<n}. size P \<le> fst (cfs ! k) \<and> fst (cfs ! k) - size P < size P'\<rbrakk> \<Longrightarrow> P' \<Turnstile> map (off P) (drop m (take (Suc n) cfs))
[PROOF STEP]
proof (induction cfs arbitrary: m n rule: execl.induct [of _ P'], auto
 simp: take_Cons drop_Cons exec1_def split: nat.split, force, force, force,
 erule execl_sub_aux [where m = 0], subst append_Cons [of _ "[]"], simp,
 erule execl_sub_aux [where m = "Suc 0" and cfs' = "[]"], simp)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>Pa a aa b ab ac ba cfs x2 x2b. \<lbrakk>\<And>m n. \<forall>k\<in>{m..<n}. size P \<le> fst (((ab, ac, ba) # cfs) ! k) \<and> fst (((ab, ac, ba) # cfs) ! k) - size P < size Pa \<Longrightarrow> Pa \<Turnstile> map (off P) (case m of 0 \<Rightarrow> (ab, ac, ba) # take n cfs | Suc m \<Rightarrow> drop m (take n cfs)); \<forall>k\<in>{Suc (Suc x2b)..<Suc x2}. size P \<le> fst (cfs ! (k - Suc (Suc 0))) \<and> fst (cfs ! (k - Suc (Suc 0))) - size P < size Pa; (if a < size P then P !! a else (Pa @ P'') !! (a - size P), a, aa, b) \<mapsto> (ab, ac, ba); 0 \<le> a; a < size P + (size Pa + size P''); P @ Pa @ P'' \<Turnstile> (ab, ac, ba) # cfs\<rbrakk> \<Longrightarrow> Pa \<Turnstile> map (off P) (drop x2b (take x2 cfs))
[PROOF STEP]
fix P' pc s stk cfs m n
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>Pa a aa b ab ac ba cfs x2 x2b. \<lbrakk>\<And>m n. \<forall>k\<in>{m..<n}. size P \<le> fst (((ab, ac, ba) # cfs) ! k) \<and> fst (((ab, ac, ba) # cfs) ! k) - size P < size Pa \<Longrightarrow> Pa \<Turnstile> map (off P) (case m of 0 \<Rightarrow> (ab, ac, ba) # take n cfs | Suc m \<Rightarrow> drop m (take n cfs)); \<forall>k\<in>{Suc (Suc x2b)..<Suc x2}. size P \<le> fst (cfs ! (k - Suc (Suc 0))) \<and> fst (cfs ! (k - Suc (Suc 0))) - size P < size Pa; (if a < size P then P !! a else (Pa @ P'') !! (a - size P), a, aa, b) \<mapsto> (ab, ac, ba); 0 \<le> a; a < size P + (size Pa + size P''); P @ Pa @ P'' \<Turnstile> (ab, ac, ba) # cfs\<rbrakk> \<Longrightarrow> Pa \<Turnstile> map (off P) (drop x2b (take x2 cfs))
[PROOF STEP]
let ?cf = "(pc, s, stk) :: config"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>Pa a aa b ab ac ba cfs x2 x2b. \<lbrakk>\<And>m n. \<forall>k\<in>{m..<n}. size P \<le> fst (((ab, ac, ba) # cfs) ! k) \<and> fst (((ab, ac, ba) # cfs) ! k) - size P < size Pa \<Longrightarrow> Pa \<Turnstile> map (off P) (case m of 0 \<Rightarrow> (ab, ac, ba) # take n cfs | Suc m \<Rightarrow> drop m (take n cfs)); \<forall>k\<in>{Suc (Suc x2b)..<Suc x2}. size P \<le> fst (cfs ! (k - Suc (Suc 0))) \<and> fst (cfs ! (k - Suc (Suc 0))) - size P < size Pa; (if a < size P then P !! a else (Pa @ P'') !! (a - size P), a, aa, b) \<mapsto> (ab, ac, ba); 0 \<le> a; a < size P + (size Pa + size P''); P @ Pa @ P'' \<Turnstile> (ab, ac, ba) # cfs\<rbrakk> \<Longrightarrow> Pa \<Turnstile> map (off P) (drop x2b (take x2 cfs))
[PROOF STEP]
assume "\<And>m n. \<forall>k \<in> {m..<n}. ?P P' (?cf # cfs) k \<Longrightarrow> P' \<Turnstile>
    map (off P) (case m of 0 \<Rightarrow> ?cf # take n cfs | Suc m \<Rightarrow> ?F cfs m n)"
[PROOF STATE]
proof (state)
this:
\<forall>k\<in>{?m..<?n}. size P \<le> fst (((pc, s, stk) # cfs) ! k) \<and> fst (((pc, s, stk) # cfs) ! k) - size P < size P' \<Longrightarrow> P' \<Turnstile> map (off P) (case ?m of 0 \<Rightarrow> (pc, s, stk) # take ?n cfs | Suc m \<Rightarrow> drop m (take ?n cfs))

goal (1 subgoal):
 1. \<And>Pa a aa b ab ac ba cfs x2 x2b. \<lbrakk>\<And>m n. \<forall>k\<in>{m..<n}. size P \<le> fst (((ab, ac, ba) # cfs) ! k) \<and> fst (((ab, ac, ba) # cfs) ! k) - size P < size Pa \<Longrightarrow> Pa \<Turnstile> map (off P) (case m of 0 \<Rightarrow> (ab, ac, ba) # take n cfs | Suc m \<Rightarrow> drop m (take n cfs)); \<forall>k\<in>{Suc (Suc x2b)..<Suc x2}. size P \<le> fst (cfs ! (k - Suc (Suc 0))) \<and> fst (cfs ! (k - Suc (Suc 0))) - size P < size Pa; (if a < size P then P !! a else (Pa @ P'') !! (a - size P), a, aa, b) \<mapsto> (ab, ac, ba); 0 \<le> a; a < size P + (size Pa + size P''); P @ Pa @ P'' \<Turnstile> (ab, ac, ba) # cfs\<rbrakk> \<Longrightarrow> Pa \<Turnstile> map (off P) (drop x2b (take x2 cfs))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<forall>k\<in>{?m..<?n}. size P \<le> fst (((pc, s, stk) # cfs) ! k) \<and> fst (((pc, s, stk) # cfs) ! k) - size P < size P' \<Longrightarrow> P' \<Turnstile> map (off P) (case ?m of 0 \<Rightarrow> (pc, s, stk) # take ?n cfs | Suc m \<Rightarrow> drop m (take ?n cfs))

goal (1 subgoal):
 1. \<And>Pa a aa b ab ac ba cfs x2 x2b. \<lbrakk>\<And>m n. \<forall>k\<in>{m..<n}. size P \<le> fst (((ab, ac, ba) # cfs) ! k) \<and> fst (((ab, ac, ba) # cfs) ! k) - size P < size Pa \<Longrightarrow> Pa \<Turnstile> map (off P) (case m of 0 \<Rightarrow> (ab, ac, ba) # take n cfs | Suc m \<Rightarrow> drop m (take n cfs)); \<forall>k\<in>{Suc (Suc x2b)..<Suc x2}. size P \<le> fst (cfs ! (k - Suc (Suc 0))) \<and> fst (cfs ! (k - Suc (Suc 0))) - size P < size Pa; (if a < size P then P !! a else (Pa @ P'') !! (a - size P), a, aa, b) \<mapsto> (ab, ac, ba); 0 \<le> a; a < size P + (size Pa + size P''); P @ Pa @ P'' \<Turnstile> (ab, ac, ba) # cfs\<rbrakk> \<Longrightarrow> Pa \<Turnstile> map (off P) (drop x2b (take x2 cfs))
[PROOF STEP]
assume "\<forall>k \<in> {Suc (Suc m)..<Suc n}. ?P P' cfs (k - Suc (Suc 0))"
[PROOF STATE]
proof (state)
this:
\<forall>k\<in>{Suc (Suc m)..<Suc n}. size P \<le> fst (cfs ! (k - Suc (Suc 0))) \<and> fst (cfs ! (k - Suc (Suc 0))) - size P < size P'

goal (1 subgoal):
 1. \<And>Pa a aa b ab ac ba cfs x2 x2b. \<lbrakk>\<And>m n. \<forall>k\<in>{m..<n}. size P \<le> fst (((ab, ac, ba) # cfs) ! k) \<and> fst (((ab, ac, ba) # cfs) ! k) - size P < size Pa \<Longrightarrow> Pa \<Turnstile> map (off P) (case m of 0 \<Rightarrow> (ab, ac, ba) # take n cfs | Suc m \<Rightarrow> drop m (take n cfs)); \<forall>k\<in>{Suc (Suc x2b)..<Suc x2}. size P \<le> fst (cfs ! (k - Suc (Suc 0))) \<and> fst (cfs ! (k - Suc (Suc 0))) - size P < size Pa; (if a < size P then P !! a else (Pa @ P'') !! (a - size P), a, aa, b) \<mapsto> (ab, ac, ba); 0 \<le> a; a < size P + (size Pa + size P''); P @ Pa @ P'' \<Turnstile> (ab, ac, ba) # cfs\<rbrakk> \<Longrightarrow> Pa \<Turnstile> map (off P) (drop x2b (take x2 cfs))
[PROOF STEP]
hence "\<forall>k \<in> {Suc m..<n}. ?P P' (?cf # cfs) k"
[PROOF STATE]
proof (prove)
using this:
\<forall>k\<in>{Suc (Suc m)..<Suc n}. size P \<le> fst (cfs ! (k - Suc (Suc 0))) \<and> fst (cfs ! (k - Suc (Suc 0))) - size P < size P'

goal (1 subgoal):
 1. \<forall>k\<in>{Suc m..<n}. size P \<le> fst (((pc, s, stk) # cfs) ! k) \<and> fst (((pc, s, stk) # cfs) ! k) - size P < size P'
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
\<forall>k\<in>{Suc m..<n}. size P \<le> fst (((pc, s, stk) # cfs) ! k) \<and> fst (((pc, s, stk) # cfs) ! k) - size P < size P'

goal (1 subgoal):
 1. \<And>Pa a aa b ab ac ba cfs x2 x2b. \<lbrakk>\<And>m n. \<forall>k\<in>{m..<n}. size P \<le> fst (((ab, ac, ba) # cfs) ! k) \<and> fst (((ab, ac, ba) # cfs) ! k) - size P < size Pa \<Longrightarrow> Pa \<Turnstile> map (off P) (case m of 0 \<Rightarrow> (ab, ac, ba) # take n cfs | Suc m \<Rightarrow> drop m (take n cfs)); \<forall>k\<in>{Suc (Suc x2b)..<Suc x2}. size P \<le> fst (cfs ! (k - Suc (Suc 0))) \<and> fst (cfs ! (k - Suc (Suc 0))) - size P < size Pa; (if a < size P then P !! a else (Pa @ P'') !! (a - size P), a, aa, b) \<mapsto> (ab, ac, ba); 0 \<le> a; a < size P + (size Pa + size P''); P @ Pa @ P'' \<Turnstile> (ab, ac, ba) # cfs\<rbrakk> \<Longrightarrow> Pa \<Turnstile> map (off P) (drop x2b (take x2 cfs))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<forall>k\<in>{?m..<?n}. size P \<le> fst (((pc, s, stk) # cfs) ! k) \<and> fst (((pc, s, stk) # cfs) ! k) - size P < size P' \<Longrightarrow> P' \<Turnstile> map (off P) (case ?m of 0 \<Rightarrow> (pc, s, stk) # take ?n cfs | Suc m \<Rightarrow> drop m (take ?n cfs))
\<forall>k\<in>{Suc m..<n}. size P \<le> fst (((pc, s, stk) # cfs) ! k) \<and> fst (((pc, s, stk) # cfs) ! k) - size P < size P'
[PROOF STEP]
show "P' \<Turnstile> map (off P) (?F cfs m n)"
[PROOF STATE]
proof (prove)
using this:
\<forall>k\<in>{?m..<?n}. size P \<le> fst (((pc, s, stk) # cfs) ! k) \<and> fst (((pc, s, stk) # cfs) ! k) - size P < size P' \<Longrightarrow> P' \<Turnstile> map (off P) (case ?m of 0 \<Rightarrow> (pc, s, stk) # take ?n cfs | Suc m \<Rightarrow> drop m (take ?n cfs))
\<forall>k\<in>{Suc m..<n}. size P \<le> fst (((pc, s, stk) # cfs) ! k) \<and> fst (((pc, s, stk) # cfs) ! k) - size P < size P'

goal (1 subgoal):
 1. P' \<Turnstile> map (off P) (drop m (take n cfs))
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
P' \<Turnstile> map (off P) (drop m (take n cfs))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma execl_all_sub [rule_format]:
  assumes
    A: "P @ P' x @ P'' \<Turnstile> cfs\<box>" and
    B: "k < length cfs" and
    C: "fst (cfs ! k) = size P" and
    D: "\<forall>cfs. P' x \<Turnstile> cfs\<box> \<longrightarrow> Q x (cfs ! 0) (cfs ! (length cfs - 1))"
  shows "\<exists>k' < length cfs. Q x (off P (cfs ! k)) (off P (cfs ! k'))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>k'<length cfs. Q x (off P (cfs ! k)) (off P (cfs ! k'))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>k'<length cfs. Q x (off P (cfs ! k)) (off P (cfs ! k'))
[PROOF STEP]
let ?P = "\<lambda>k. size P \<le> fst (cfs ! k) \<and> fst (cfs ! k) - size P < size (P' x)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>k'<length cfs. Q x (off P (cfs ! k)) (off P (cfs ! k'))
[PROOF STEP]
let ?A = "{k'. k' \<in> {k..<length cfs} \<and> \<not> ?P k'}"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>k'<length cfs. Q x (off P (cfs ! k)) (off P (cfs ! k'))
[PROOF STEP]
have E: "Min ?A \<in> ?A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Min {k' \<in> {k..<length cfs}. \<not> (size P \<le> fst (cfs ! k') \<and> fst (cfs ! k') - size P < size (P' x))} \<in> {k' \<in> {k..<length cfs}. \<not> (size P \<le> fst (cfs ! k') \<and> fst (cfs ! k') - size P < size (P' x))}
[PROOF STEP]
using A and B
[PROOF STATE]
proof (prove)
using this:
P @ P' x @ P'' \<Turnstile> cfs\<box>
k < length cfs

goal (1 subgoal):
 1. Min {k' \<in> {k..<length cfs}. \<not> (size P \<le> fst (cfs ! k') \<and> fst (cfs ! k') - size P < size (P' x))} \<in> {k' \<in> {k..<length cfs}. \<not> (size P \<le> fst (cfs ! k') \<and> fst (cfs ! k') - size P < size (P' x))}
[PROOF STEP]
by (rule_tac Min_in, simp_all add: execl_all_def,
     rule_tac exI [of _ "length cfs - 1"], auto)
[PROOF STATE]
proof (state)
this:
Min {k' \<in> {k..<length cfs}. \<not> (size P \<le> fst (cfs ! k') \<and> fst (cfs ! k') - size P < size (P' x))} \<in> {k' \<in> {k..<length cfs}. \<not> (size P \<le> fst (cfs ! k') \<and> fst (cfs ! k') - size P < size (P' x))}

goal (1 subgoal):
 1. \<exists>k'<length cfs. Q x (off P (cfs ! k)) (off P (cfs ! k'))
[PROOF STEP]
hence "map (off P) (drop k (take (Suc (Min ?A)) cfs)) ! 0 = off P (cfs ! k)"
    (is "?cfs ! _ = _")
[PROOF STATE]
proof (prove)
using this:
Min {k' \<in> {k..<length cfs}. \<not> (size P \<le> fst (cfs ! k') \<and> fst (cfs ! k') - size P < size (P' x))} \<in> {k' \<in> {k..<length cfs}. \<not> (size P \<le> fst (cfs ! k') \<and> fst (cfs ! k') - size P < size (P' x))}

goal (1 subgoal):
 1. map (off P) (drop k (take (Suc (Min {k' \<in> {k..<length cfs}. \<not> (size P \<le> fst (cfs ! k') \<and> fst (cfs ! k') - size P < size (P' x))})) cfs)) ! 0 = off P (cfs ! k)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
map (off P) (drop k (take (Suc (Min {k' \<in> {k..<length cfs}. \<not> (size P \<le> fst (cfs ! k') \<and> fst (cfs ! k') - size P < size (P' x))})) cfs)) ! 0 = off P (cfs ! k)

goal (1 subgoal):
 1. \<exists>k'<length cfs. Q x (off P (cfs ! k)) (off P (cfs ! k'))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
map (off P) (drop k (take (Suc (Min {k' \<in> {k..<length cfs}. \<not> (size P \<le> fst (cfs ! k') \<and> fst (cfs ! k') - size P < size (P' x))})) cfs)) ! 0 = off P (cfs ! k)

goal (1 subgoal):
 1. \<exists>k'<length cfs. Q x (off P (cfs ! k)) (off P (cfs ! k'))
[PROOF STEP]
have "length cfs \<le> Suc (Min ?A) \<longrightarrow> Min ?A = length cfs - 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length cfs \<le> Suc (Min {k' \<in> {k..<length cfs}. \<not> (size P \<le> fst (cfs ! k') \<and> fst (cfs ! k') - size P < size (P' x))}) \<longrightarrow> Min {k' \<in> {k..<length cfs}. \<not> (size P \<le> fst (cfs ! k') \<and> fst (cfs ! k') - size P < size (P' x))} = length cfs - 1
[PROOF STEP]
using E
[PROOF STATE]
proof (prove)
using this:
Min {k' \<in> {k..<length cfs}. \<not> (size P \<le> fst (cfs ! k') \<and> fst (cfs ! k') - size P < size (P' x))} \<in> {k' \<in> {k..<length cfs}. \<not> (size P \<le> fst (cfs ! k') \<and> fst (cfs ! k') - size P < size (P' x))}

goal (1 subgoal):
 1. length cfs \<le> Suc (Min {k' \<in> {k..<length cfs}. \<not> (size P \<le> fst (cfs ! k') \<and> fst (cfs ! k') - size P < size (P' x))}) \<longrightarrow> Min {k' \<in> {k..<length cfs}. \<not> (size P \<le> fst (cfs ! k') \<and> fst (cfs ! k') - size P < size (P' x))} = length cfs - 1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
length cfs \<le> Suc (Min {k' \<in> {k..<length cfs}. \<not> (size P \<le> fst (cfs ! k') \<and> fst (cfs ! k') - size P < size (P' x))}) \<longrightarrow> Min {k' \<in> {k..<length cfs}. \<not> (size P \<le> fst (cfs ! k') \<and> fst (cfs ! k') - size P < size (P' x))} = length cfs - 1

goal (1 subgoal):
 1. \<exists>k'<length cfs. Q x (off P (cfs ! k)) (off P (cfs ! k'))
[PROOF STEP]
with A and B and E
[PROOF STATE]
proof (chain)
picking this:
P @ P' x @ P'' \<Turnstile> cfs\<box>
k < length cfs
Min {k' \<in> {k..<length cfs}. \<not> (size P \<le> fst (cfs ! k') \<and> fst (cfs ! k') - size P < size (P' x))} \<in> {k' \<in> {k..<length cfs}. \<not> (size P \<le> fst (cfs ! k') \<and> fst (cfs ! k') - size P < size (P' x))}
length cfs \<le> Suc (Min {k' \<in> {k..<length cfs}. \<not> (size P \<le> fst (cfs ! k') \<and> fst (cfs ! k') - size P < size (P' x))}) \<longrightarrow> Min {k' \<in> {k..<length cfs}. \<not> (size P \<le> fst (cfs ! k') \<and> fst (cfs ! k') - size P < size (P' x))} = length cfs - 1
[PROOF STEP]
have F: "?cfs ! (length ?cfs - 1) = off P (cfs ! Min ?A)"
[PROOF STATE]
proof (prove)
using this:
P @ P' x @ P'' \<Turnstile> cfs\<box>
k < length cfs
Min {k' \<in> {k..<length cfs}. \<not> (size P \<le> fst (cfs ! k') \<and> fst (cfs ! k') - size P < size (P' x))} \<in> {k' \<in> {k..<length cfs}. \<not> (size P \<le> fst (cfs ! k') \<and> fst (cfs ! k') - size P < size (P' x))}
length cfs \<le> Suc (Min {k' \<in> {k..<length cfs}. \<not> (size P \<le> fst (cfs ! k') \<and> fst (cfs ! k') - size P < size (P' x))}) \<longrightarrow> Min {k' \<in> {k..<length cfs}. \<not> (size P \<le> fst (cfs ! k') \<and> fst (cfs ! k') - size P < size (P' x))} = length cfs - 1

goal (1 subgoal):
 1. map (off P) (drop k (take (Suc (Min {k' \<in> {k..<length cfs}. \<not> (size P \<le> fst (cfs ! k') \<and> fst (cfs ! k') - size P < size (P' x))})) cfs)) ! (length (map (off P) (drop k (take (Suc (Min {k' \<in> {k..<length cfs}. \<not> (size P \<le> fst (cfs ! k') \<and> fst (cfs ! k') - size P < size (P' x))})) cfs))) - 1) = off P (cfs ! Min {k' \<in> {k..<length cfs}. \<not> (size P \<le> fst (cfs ! k') \<and> fst (cfs ! k') - size P < size (P' x))})
[PROOF STEP]
by (subst nth_map, auto simp: min_def execl_all_def, arith)
[PROOF STATE]
proof (state)
this:
map (off P) (drop k (take (Suc (Min {k' \<in> {k..<length cfs}. \<not> (size P \<le> fst (cfs ! k') \<and> fst (cfs ! k') - size P < size (P' x))})) cfs)) ! (length (map (off P) (drop k (take (Suc (Min {k' \<in> {k..<length cfs}. \<not> (size P \<le> fst (cfs ! k') \<and> fst (cfs ! k') - size P < size (P' x))})) cfs))) - 1) = off P (cfs ! Min {k' \<in> {k..<length cfs}. \<not> (size P \<le> fst (cfs ! k') \<and> fst (cfs ! k') - size P < size (P' x))})

goal (1 subgoal):
 1. \<exists>k'<length cfs. Q x (off P (cfs ! k)) (off P (cfs ! k'))
[PROOF STEP]
hence "?cfs \<noteq> [] \<and> fst (?cfs ! (length ?cfs - 1)) \<notin> {0..<size (P' x)}"
[PROOF STATE]
proof (prove)
using this:
map (off P) (drop k (take (Suc (Min {k' \<in> {k..<length cfs}. \<not> (size P \<le> fst (cfs ! k') \<and> fst (cfs ! k') - size P < size (P' x))})) cfs)) ! (length (map (off P) (drop k (take (Suc (Min {k' \<in> {k..<length cfs}. \<not> (size P \<le> fst (cfs ! k') \<and> fst (cfs ! k') - size P < size (P' x))})) cfs))) - 1) = off P (cfs ! Min {k' \<in> {k..<length cfs}. \<not> (size P \<le> fst (cfs ! k') \<and> fst (cfs ! k') - size P < size (P' x))})

goal (1 subgoal):
 1. map (off P) (drop k (take (Suc (Min {k' \<in> {k..<length cfs}. \<not> (size P \<le> fst (cfs ! k') \<and> fst (cfs ! k') - size P < size (P' x))})) cfs)) \<noteq> [] \<and> fst (map (off P) (drop k (take (Suc (Min {k' \<in> {k..<length cfs}. \<not> (size P \<le> fst (cfs ! k') \<and> fst (cfs ! k') - size P < size (P' x))})) cfs)) ! (length (map (off P) (drop k (take (Suc (Min {k' \<in> {k..<length cfs}. \<not> (size P \<le> fst (cfs ! k') \<and> fst (cfs ! k') - size P < size (P' x))})) cfs))) - 1)) \<notin> {0..<size (P' x)}
[PROOF STEP]
using E
[PROOF STATE]
proof (prove)
using this:
map (off P) (drop k (take (Suc (Min {k' \<in> {k..<length cfs}. \<not> (size P \<le> fst (cfs ! k') \<and> fst (cfs ! k') - size P < size (P' x))})) cfs)) ! (length (map (off P) (drop k (take (Suc (Min {k' \<in> {k..<length cfs}. \<not> (size P \<le> fst (cfs ! k') \<and> fst (cfs ! k') - size P < size (P' x))})) cfs))) - 1) = off P (cfs ! Min {k' \<in> {k..<length cfs}. \<not> (size P \<le> fst (cfs ! k') \<and> fst (cfs ! k') - size P < size (P' x))})
Min {k' \<in> {k..<length cfs}. \<not> (size P \<le> fst (cfs ! k') \<and> fst (cfs ! k') - size P < size (P' x))} \<in> {k' \<in> {k..<length cfs}. \<not> (size P \<le> fst (cfs ! k') \<and> fst (cfs ! k') - size P < size (P' x))}

goal (1 subgoal):
 1. map (off P) (drop k (take (Suc (Min {k' \<in> {k..<length cfs}. \<not> (size P \<le> fst (cfs ! k') \<and> fst (cfs ! k') - size P < size (P' x))})) cfs)) \<noteq> [] \<and> fst (map (off P) (drop k (take (Suc (Min {k' \<in> {k..<length cfs}. \<not> (size P \<le> fst (cfs ! k') \<and> fst (cfs ! k') - size P < size (P' x))})) cfs)) ! (length (map (off P) (drop k (take (Suc (Min {k' \<in> {k..<length cfs}. \<not> (size P \<le> fst (cfs ! k') \<and> fst (cfs ! k') - size P < size (P' x))})) cfs))) - 1)) \<notin> {0..<size (P' x)}
[PROOF STEP]
by (auto simp: min_def)
[PROOF STATE]
proof (state)
this:
map (off P) (drop k (take (Suc (Min {k' \<in> {k..<length cfs}. \<not> (size P \<le> fst (cfs ! k') \<and> fst (cfs ! k') - size P < size (P' x))})) cfs)) \<noteq> [] \<and> fst (map (off P) (drop k (take (Suc (Min {k' \<in> {k..<length cfs}. \<not> (size P \<le> fst (cfs ! k') \<and> fst (cfs ! k') - size P < size (P' x))})) cfs)) ! (length (map (off P) (drop k (take (Suc (Min {k' \<in> {k..<length cfs}. \<not> (size P \<le> fst (cfs ! k') \<and> fst (cfs ! k') - size P < size (P' x))})) cfs))) - 1)) \<notin> {0..<size (P' x)}

goal (1 subgoal):
 1. \<exists>k'<length cfs. Q x (off P (cfs ! k)) (off P (cfs ! k'))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
map (off P) (drop k (take (Suc (Min {k' \<in> {k..<length cfs}. \<not> (size P \<le> fst (cfs ! k') \<and> fst (cfs ! k') - size P < size (P' x))})) cfs)) \<noteq> [] \<and> fst (map (off P) (drop k (take (Suc (Min {k' \<in> {k..<length cfs}. \<not> (size P \<le> fst (cfs ! k') \<and> fst (cfs ! k') - size P < size (P' x))})) cfs)) ! (length (map (off P) (drop k (take (Suc (Min {k' \<in> {k..<length cfs}. \<not> (size P \<le> fst (cfs ! k') \<and> fst (cfs ! k') - size P < size (P' x))})) cfs))) - 1)) \<notin> {0..<size (P' x)}

goal (1 subgoal):
 1. \<exists>k'<length cfs. Q x (off P (cfs ! k)) (off P (cfs ! k'))
[PROOF STEP]
have "\<not> (\<exists>k'. k' \<in> {k'. k' \<in> {k..<Min ?A} \<and> \<not> ?P k'})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<nexists>k'. k' \<in> {k' \<in> {k..<Min {k' \<in> {k..<length cfs}. \<not> (size P \<le> fst (cfs ! k') \<and> fst (cfs ! k') - size P < size (P' x))}}. \<not> (size P \<le> fst (cfs ! k') \<and> fst (cfs ! k') - size P < size (P' x))}
[PROOF STEP]
by (rule notI, erule exE, frule rev_subsetD [of _ _ ?A], rule subsetI,
     insert E, simp, subgoal_tac "finite ?A", drule Min_le, force+)
[PROOF STATE]
proof (state)
this:
\<nexists>k'. k' \<in> {k' \<in> {k..<Min {k' \<in> {k..<length cfs}. \<not> (size P \<le> fst (cfs ! k') \<and> fst (cfs ! k') - size P < size (P' x))}}. \<not> (size P \<le> fst (cfs ! k') \<and> fst (cfs ! k') - size P < size (P' x))}

goal (1 subgoal):
 1. \<exists>k'<length cfs. Q x (off P (cfs ! k)) (off P (cfs ! k'))
[PROOF STEP]
hence "P' x \<Turnstile> ?cfs"
[PROOF STATE]
proof (prove)
using this:
\<nexists>k'. k' \<in> {k' \<in> {k..<Min {k' \<in> {k..<length cfs}. \<not> (size P \<le> fst (cfs ! k') \<and> fst (cfs ! k') - size P < size (P' x))}}. \<not> (size P \<le> fst (cfs ! k') \<and> fst (cfs ! k') - size P < size (P' x))}

goal (1 subgoal):
 1. P' x \<Turnstile> map (off P) (drop k (take (Suc (Min {k' \<in> {k..<length cfs}. \<not> (size P \<le> fst (cfs ! k') \<and> fst (cfs ! k') - size P < size (P' x))})) cfs))
[PROOF STEP]
using A
[PROOF STATE]
proof (prove)
using this:
\<nexists>k'. k' \<in> {k' \<in> {k..<Min {k' \<in> {k..<length cfs}. \<not> (size P \<le> fst (cfs ! k') \<and> fst (cfs ! k') - size P < size (P' x))}}. \<not> (size P \<le> fst (cfs ! k') \<and> fst (cfs ! k') - size P < size (P' x))}
P @ P' x @ P'' \<Turnstile> cfs\<box>

goal (1 subgoal):
 1. P' x \<Turnstile> map (off P) (drop k (take (Suc (Min {k' \<in> {k..<length cfs}. \<not> (size P \<le> fst (cfs ! k') \<and> fst (cfs ! k') - size P < size (P' x))})) cfs))
[PROOF STEP]
by (subst (asm) execl_all_def, rule_tac execl_sub, blast+)
[PROOF STATE]
proof (state)
this:
P' x \<Turnstile> map (off P) (drop k (take (Suc (Min {k' \<in> {k..<length cfs}. \<not> (size P \<le> fst (cfs ! k') \<and> fst (cfs ! k') - size P < size (P' x))})) cfs))

goal (1 subgoal):
 1. \<exists>k'<length cfs. Q x (off P (cfs ! k)) (off P (cfs ! k'))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
map (off P) (drop k (take (Suc (Min {k' \<in> {k..<length cfs}. \<not> (size P \<le> fst (cfs ! k') \<and> fst (cfs ! k') - size P < size (P' x))})) cfs)) ! 0 = off P (cfs ! k)
map (off P) (drop k (take (Suc (Min {k' \<in> {k..<length cfs}. \<not> (size P \<le> fst (cfs ! k') \<and> fst (cfs ! k') - size P < size (P' x))})) cfs)) \<noteq> [] \<and> fst (map (off P) (drop k (take (Suc (Min {k' \<in> {k..<length cfs}. \<not> (size P \<le> fst (cfs ! k') \<and> fst (cfs ! k') - size P < size (P' x))})) cfs)) ! (length (map (off P) (drop k (take (Suc (Min {k' \<in> {k..<length cfs}. \<not> (size P \<le> fst (cfs ! k') \<and> fst (cfs ! k') - size P < size (P' x))})) cfs))) - 1)) \<notin> {0..<size (P' x)}
P' x \<Turnstile> map (off P) (drop k (take (Suc (Min {k' \<in> {k..<length cfs}. \<not> (size P \<le> fst (cfs ! k') \<and> fst (cfs ! k') - size P < size (P' x))})) cfs))
[PROOF STEP]
have "Q x (?cfs ! 0) (?cfs ! (length ?cfs - 1))"
[PROOF STATE]
proof (prove)
using this:
map (off P) (drop k (take (Suc (Min {k' \<in> {k..<length cfs}. \<not> (size P \<le> fst (cfs ! k') \<and> fst (cfs ! k') - size P < size (P' x))})) cfs)) ! 0 = off P (cfs ! k)
map (off P) (drop k (take (Suc (Min {k' \<in> {k..<length cfs}. \<not> (size P \<le> fst (cfs ! k') \<and> fst (cfs ! k') - size P < size (P' x))})) cfs)) \<noteq> [] \<and> fst (map (off P) (drop k (take (Suc (Min {k' \<in> {k..<length cfs}. \<not> (size P \<le> fst (cfs ! k') \<and> fst (cfs ! k') - size P < size (P' x))})) cfs)) ! (length (map (off P) (drop k (take (Suc (Min {k' \<in> {k..<length cfs}. \<not> (size P \<le> fst (cfs ! k') \<and> fst (cfs ! k') - size P < size (P' x))})) cfs))) - 1)) \<notin> {0..<size (P' x)}
P' x \<Turnstile> map (off P) (drop k (take (Suc (Min {k' \<in> {k..<length cfs}. \<not> (size P \<le> fst (cfs ! k') \<and> fst (cfs ! k') - size P < size (P' x))})) cfs))

goal (1 subgoal):
 1. Q x (map (off P) (drop k (take (Suc (Min {k' \<in> {k..<length cfs}. \<not> (size P \<le> fst (cfs ! k') \<and> fst (cfs ! k') - size P < size (P' x))})) cfs)) ! 0) (map (off P) (drop k (take (Suc (Min {k' \<in> {k..<length cfs}. \<not> (size P \<le> fst (cfs ! k') \<and> fst (cfs ! k') - size P < size (P' x))})) cfs)) ! (length (map (off P) (drop k (take (Suc (Min {k' \<in> {k..<length cfs}. \<not> (size P \<le> fst (cfs ! k') \<and> fst (cfs ! k') - size P < size (P' x))})) cfs))) - 1))
[PROOF STEP]
using C and D
[PROOF STATE]
proof (prove)
using this:
map (off P) (drop k (take (Suc (Min {k' \<in> {k..<length cfs}. \<not> (size P \<le> fst (cfs ! k') \<and> fst (cfs ! k') - size P < size (P' x))})) cfs)) ! 0 = off P (cfs ! k)
map (off P) (drop k (take (Suc (Min {k' \<in> {k..<length cfs}. \<not> (size P \<le> fst (cfs ! k') \<and> fst (cfs ! k') - size P < size (P' x))})) cfs)) \<noteq> [] \<and> fst (map (off P) (drop k (take (Suc (Min {k' \<in> {k..<length cfs}. \<not> (size P \<le> fst (cfs ! k') \<and> fst (cfs ! k') - size P < size (P' x))})) cfs)) ! (length (map (off P) (drop k (take (Suc (Min {k' \<in> {k..<length cfs}. \<not> (size P \<le> fst (cfs ! k') \<and> fst (cfs ! k') - size P < size (P' x))})) cfs))) - 1)) \<notin> {0..<size (P' x)}
P' x \<Turnstile> map (off P) (drop k (take (Suc (Min {k' \<in> {k..<length cfs}. \<not> (size P \<le> fst (cfs ! k') \<and> fst (cfs ! k') - size P < size (P' x))})) cfs))
fst (cfs ! k) = size P
\<forall>cfs. P' x \<Turnstile> cfs\<box> \<longrightarrow> Q x (cfs ! 0) (cfs ! (length cfs - 1))

goal (1 subgoal):
 1. Q x (map (off P) (drop k (take (Suc (Min {k' \<in> {k..<length cfs}. \<not> (size P \<le> fst (cfs ! k') \<and> fst (cfs ! k') - size P < size (P' x))})) cfs)) ! 0) (map (off P) (drop k (take (Suc (Min {k' \<in> {k..<length cfs}. \<not> (size P \<le> fst (cfs ! k') \<and> fst (cfs ! k') - size P < size (P' x))})) cfs)) ! (length (map (off P) (drop k (take (Suc (Min {k' \<in> {k..<length cfs}. \<not> (size P \<le> fst (cfs ! k') \<and> fst (cfs ! k') - size P < size (P' x))})) cfs))) - 1))
[PROOF STEP]
by (auto simp: execl_all_def)
[PROOF STATE]
proof (state)
this:
Q x (map (off P) (drop k (take (Suc (Min {k' \<in> {k..<length cfs}. \<not> (size P \<le> fst (cfs ! k') \<and> fst (cfs ! k') - size P < size (P' x))})) cfs)) ! 0) (map (off P) (drop k (take (Suc (Min {k' \<in> {k..<length cfs}. \<not> (size P \<le> fst (cfs ! k') \<and> fst (cfs ! k') - size P < size (P' x))})) cfs)) ! (length (map (off P) (drop k (take (Suc (Min {k' \<in> {k..<length cfs}. \<not> (size P \<le> fst (cfs ! k') \<and> fst (cfs ! k') - size P < size (P' x))})) cfs))) - 1))

goal (1 subgoal):
 1. \<exists>k'<length cfs. Q x (off P (cfs ! k)) (off P (cfs ! k'))
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
Q x (map (off P) (drop k (take (Suc (Min {k' \<in> {k..<length cfs}. \<not> (size P \<le> fst (cfs ! k') \<and> fst (cfs ! k') - size P < size (P' x))})) cfs)) ! 0) (map (off P) (drop k (take (Suc (Min {k' \<in> {k..<length cfs}. \<not> (size P \<le> fst (cfs ! k') \<and> fst (cfs ! k') - size P < size (P' x))})) cfs)) ! (length (map (off P) (drop k (take (Suc (Min {k' \<in> {k..<length cfs}. \<not> (size P \<le> fst (cfs ! k') \<and> fst (cfs ! k') - size P < size (P' x))})) cfs))) - 1))

goal (1 subgoal):
 1. \<exists>k'<length cfs. Q x (off P (cfs ! k)) (off P (cfs ! k'))
[PROOF STEP]
using E and F
[PROOF STATE]
proof (prove)
using this:
Q x (map (off P) (drop k (take (Suc (Min {k' \<in> {k..<length cfs}. \<not> (size P \<le> fst (cfs ! k') \<and> fst (cfs ! k') - size P < size (P' x))})) cfs)) ! 0) (map (off P) (drop k (take (Suc (Min {k' \<in> {k..<length cfs}. \<not> (size P \<le> fst (cfs ! k') \<and> fst (cfs ! k') - size P < size (P' x))})) cfs)) ! (length (map (off P) (drop k (take (Suc (Min {k' \<in> {k..<length cfs}. \<not> (size P \<le> fst (cfs ! k') \<and> fst (cfs ! k') - size P < size (P' x))})) cfs))) - 1))
Min {k' \<in> {k..<length cfs}. \<not> (size P \<le> fst (cfs ! k') \<and> fst (cfs ! k') - size P < size (P' x))} \<in> {k' \<in> {k..<length cfs}. \<not> (size P \<le> fst (cfs ! k') \<and> fst (cfs ! k') - size P < size (P' x))}
map (off P) (drop k (take (Suc (Min {k' \<in> {k..<length cfs}. \<not> (size P \<le> fst (cfs ! k') \<and> fst (cfs ! k') - size P < size (P' x))})) cfs)) ! (length (map (off P) (drop k (take (Suc (Min {k' \<in> {k..<length cfs}. \<not> (size P \<le> fst (cfs ! k') \<and> fst (cfs ! k') - size P < size (P' x))})) cfs))) - 1) = off P (cfs ! Min {k' \<in> {k..<length cfs}. \<not> (size P \<le> fst (cfs ! k') \<and> fst (cfs ! k') - size P < size (P' x))})

goal (1 subgoal):
 1. \<exists>k'<length cfs. Q x (off P (cfs ! k)) (off P (cfs ! k'))
[PROOF STEP]
by (rule_tac exI [of _ "Min ?A"], auto)
[PROOF STATE]
proof (state)
this:
\<exists>k'<length cfs. Q x (off P (cfs ! k)) (off P (cfs ! k'))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma execl_all_sub2:
  assumes
    A: "P x @ P' x' @ P'' \<Turnstile> cfs\<box>"
      (is "?P \<Turnstile> _\<box>") and
    B: "\<And>cfs. P x \<Turnstile> cfs\<box> \<Longrightarrow> (\<lambda>(pc, s, stk) (pc', s', stk').
      pc' = pc + size (P x) + I s \<and> Q s s' \<and> stk' = F s stk)
        (cfs ! 0) (cfs ! (length cfs - 1))"
      (is "\<And>cfs. _ \<Longrightarrow> ?Q x (cfs ! 0) (cfs ! (length cfs - 1))") and
    C: "\<And>cfs. P' x' \<Turnstile> cfs\<box> \<Longrightarrow> (\<lambda>(pc, s, stk) (pc', s', stk').
      pc' = pc + size (P' x') + I' s \<and> Q' s s' \<and> stk' = F' s stk)
        (cfs ! 0) (cfs ! (length cfs - 1))"
      (is "\<And>cfs. _ \<Longrightarrow> ?Q' x' (cfs ! 0) (cfs ! (length cfs - 1))") and
    D: "I (fst (snd (cfs ! 0))) = 0"
  shows "\<exists>k < length cfs. \<exists>t. (\<lambda>(pc, s, stk) (pc', s', stk').
    pc = 0 \<and> pc' = size (P x) + size (P' x') + I' t \<and> Q s t \<and> Q' t s' \<and>
      stk' = F' t (F s stk)) (cfs ! 0) (cfs ! k)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>k<length cfs. \<exists>t. (case cfs ! 0 of (pc, s, stk) \<Rightarrow> \<lambda>(pc', s', stk'). pc = 0 \<and> pc' = size (P x) + size (P' x') + I' t \<and> Q s t \<and> Q' t s' \<and> stk' = F' t (F s stk)) (cfs ! k)
[PROOF STEP]
by (subgoal_tac "[] @ ?P \<Turnstile> cfs\<box>", drule execl_all_sub [where k = 0 and Q = ?Q],
 insert A B, (clarsimp simp: execl_all_def)+, insert A C D, drule execl_all_sub
 [where Q = ?Q'], simp+, clarify, rule exI, rule conjI, simp, rule exI, auto)


[STATEMENT]
lemma acomp_acomp:
 "\<lbrakk>acomp a\<^sub>1 @ acomp a\<^sub>2 @ P \<Turnstile> cfs\<box>;
    \<And>cfs. acomp a\<^sub>1 \<Turnstile> cfs\<box> \<Longrightarrow> apred a\<^sub>1 (cfs ! 0) (cfs ! (length cfs - 1));
    \<And>cfs. acomp a\<^sub>2 \<Turnstile> cfs\<box> \<Longrightarrow> apred a\<^sub>2 (cfs ! 0) (cfs ! (length cfs - 1))\<rbrakk> \<Longrightarrow>
  case cfs ! 0 of (pc, s, stk) \<Rightarrow> pc = 0 \<and> (\<exists>k < length cfs. cfs ! k =
    (size (acomp a\<^sub>1 @ acomp a\<^sub>2), s, aval a\<^sub>2 s # aval a\<^sub>1 s # stk))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>acomp a\<^sub>1 @ acomp a\<^sub>2 @ P \<Turnstile> cfs\<box>; \<And>cfs. acomp a\<^sub>1 \<Turnstile> cfs\<box> \<Longrightarrow> apred a\<^sub>1 (cfs ! 0) (cfs ! (length cfs - 1)); \<And>cfs. acomp a\<^sub>2 \<Turnstile> cfs\<box> \<Longrightarrow> apred a\<^sub>2 (cfs ! 0) (cfs ! (length cfs - 1))\<rbrakk> \<Longrightarrow> case cfs ! 0 of (pc, s, stk) \<Rightarrow> pc = 0 \<and> (\<exists>k<length cfs. cfs ! k = (size (acomp a\<^sub>1 @ acomp a\<^sub>2), s, aval a\<^sub>2 s # aval a\<^sub>1 s # stk))
[PROOF STEP]
by (drule execl_all_sub2 [where I = "\<lambda>s. 0" and I' = "\<lambda>s. 0" and Q = "\<lambda>s s'. s' = s"
 and Q' = "\<lambda>s s'. s' = s" and F = "\<lambda>s stk. aval a\<^sub>1 s # stk"
 and F' = "\<lambda>s stk. aval a\<^sub>2 s # stk"], auto simp: apred_def)


[STATEMENT]
lemma bcomp_bcomp:
 "\<lbrakk>bcomp (b\<^sub>1, f\<^sub>1, i\<^sub>1) @ bcomp (b\<^sub>2, f\<^sub>2, i\<^sub>2) \<Turnstile> cfs\<box>;
    \<And>cfs. bcomp (b\<^sub>1, f\<^sub>1, i\<^sub>1) \<Turnstile> cfs\<box> \<Longrightarrow>
      bpred (b\<^sub>1, f\<^sub>1, i\<^sub>1) (cfs ! 0) (cfs ! (length cfs - 1));
    \<And>cfs. bcomp (b\<^sub>2, f\<^sub>2, i\<^sub>2) \<Turnstile> cfs\<box> \<Longrightarrow>
      bpred (b\<^sub>2, f\<^sub>2, i\<^sub>2) (cfs ! 0) (cfs ! (length cfs - 1))\<rbrakk> \<Longrightarrow>
  case cfs ! 0 of (pc, s, stk) \<Rightarrow> pc = 0 \<and> (bval b\<^sub>1 s \<noteq> f\<^sub>1 \<longrightarrow>
    (\<exists>k < length cfs. cfs ! k = (size (bcomp (b\<^sub>1, f\<^sub>1, i\<^sub>1) @ bcomp (b\<^sub>2, f\<^sub>2, i\<^sub>2)) +
      (if bval b\<^sub>2 s = f\<^sub>2 then i\<^sub>2 else 0), s, stk)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>bcomp (b\<^sub>1, f\<^sub>1, i\<^sub>1) @ bcomp (b\<^sub>2, f\<^sub>2, i\<^sub>2) \<Turnstile> cfs\<box>; \<And>cfs. bcomp (b\<^sub>1, f\<^sub>1, i\<^sub>1) \<Turnstile> cfs\<box> \<Longrightarrow> bpred (b\<^sub>1, f\<^sub>1, i\<^sub>1) (cfs ! 0) (cfs ! (length cfs - 1)); \<And>cfs. bcomp (b\<^sub>2, f\<^sub>2, i\<^sub>2) \<Turnstile> cfs\<box> \<Longrightarrow> bpred (b\<^sub>2, f\<^sub>2, i\<^sub>2) (cfs ! 0) (cfs ! (length cfs - 1))\<rbrakk> \<Longrightarrow> case cfs ! 0 of (pc, s, stk) \<Rightarrow> pc = 0 \<and> (bval b\<^sub>1 s \<noteq> f\<^sub>1 \<longrightarrow> (\<exists>k<length cfs. cfs ! k = (size (bcomp (b\<^sub>1, f\<^sub>1, i\<^sub>1) @ bcomp (b\<^sub>2, f\<^sub>2, i\<^sub>2)) + (if bval b\<^sub>2 s = f\<^sub>2 then i\<^sub>2 else 0), s, stk)))
[PROOF STEP]
by (clarify, rule conjI, simp add: execl_all_def, rule impI, subst (asm) append_Nil2
 [symmetric], drule execl_all_sub2 [where I = "\<lambda>s. if bval b\<^sub>1 s = f\<^sub>1 then i\<^sub>1 else 0"
 and I' = "\<lambda>s. if bval b\<^sub>2 s = f\<^sub>2 then i\<^sub>2 else 0" and Q = "\<lambda>s s'. s' = s"
 and Q' = "\<lambda>s s'. s' = s" and F = "\<lambda>s stk. stk" and F' = "\<lambda>s stk. stk"],
 auto simp: bpred_def)


[STATEMENT]
lemma acomp_correct [simplified, intro]:
 "acomp a \<Turnstile> cfs\<box> \<Longrightarrow> apred a (cfs ! 0) (cfs ! (length cfs - 1))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. acomp a \<Turnstile> cfs\<box> \<Longrightarrow> apred a (cfs ! 0) (cfs ! (length cfs - 1))
[PROOF STEP]
proof (induction a arbitrary: cfs, simp_all, frule_tac [3] acomp_acomp, auto)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a1 a2 cfs a b k. \<lbrakk>\<And>cfs. acomp a1 \<Turnstile> cfs\<box> \<Longrightarrow> apred a1 (cfs ! 0) (cfs ! (length cfs - Suc 0)); \<And>cfs. acomp a2 \<Turnstile> cfs\<box> \<Longrightarrow> apred a2 (cfs ! 0) (cfs ! (length cfs - Suc 0)); acomp a1 @ acomp a2 @ [ADD] \<Turnstile> cfs\<box>; cfs ! 0 = (0, a, b); k < length cfs; cfs ! k = (size (acomp a1) + size (acomp a2), a, aval a2 a # aval a1 a # b)\<rbrakk> \<Longrightarrow> apred (Plus a1 a2) (0, a, b) (cfs ! (length cfs - Suc 0))
[PROOF STEP]
fix a\<^sub>1 a\<^sub>2 cfs s stk k
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a1 a2 cfs a b k. \<lbrakk>\<And>cfs. acomp a1 \<Turnstile> cfs\<box> \<Longrightarrow> apred a1 (cfs ! 0) (cfs ! (length cfs - Suc 0)); \<And>cfs. acomp a2 \<Turnstile> cfs\<box> \<Longrightarrow> apred a2 (cfs ! 0) (cfs ! (length cfs - Suc 0)); acomp a1 @ acomp a2 @ [ADD] \<Turnstile> cfs\<box>; cfs ! 0 = (0, a, b); k < length cfs; cfs ! k = (size (acomp a1) + size (acomp a2), a, aval a2 a # aval a1 a # b)\<rbrakk> \<Longrightarrow> apred (Plus a1 a2) (0, a, b) (cfs ! (length cfs - Suc 0))
[PROOF STEP]
assume A: "acomp a\<^sub>1 @ acomp a\<^sub>2 @ [ADD] \<Turnstile> cfs\<box>"
    (is "?ca\<^sub>1 @ ?ca\<^sub>2 @ ?i \<Turnstile> _\<box>")
[PROOF STATE]
proof (state)
this:
acomp a\<^sub>1 @ acomp a\<^sub>2 @ [ADD] \<Turnstile> cfs\<box>

goal (1 subgoal):
 1. \<And>a1 a2 cfs a b k. \<lbrakk>\<And>cfs. acomp a1 \<Turnstile> cfs\<box> \<Longrightarrow> apred a1 (cfs ! 0) (cfs ! (length cfs - Suc 0)); \<And>cfs. acomp a2 \<Turnstile> cfs\<box> \<Longrightarrow> apred a2 (cfs ! 0) (cfs ! (length cfs - Suc 0)); acomp a1 @ acomp a2 @ [ADD] \<Turnstile> cfs\<box>; cfs ! 0 = (0, a, b); k < length cfs; cfs ! k = (size (acomp a1) + size (acomp a2), a, aval a2 a # aval a1 a # b)\<rbrakk> \<Longrightarrow> apred (Plus a1 a2) (0, a, b) (cfs ! (length cfs - Suc 0))
[PROOF STEP]
assume B: "k < length cfs" and
    C: "cfs ! k = (size ?ca\<^sub>1 + size ?ca\<^sub>2, s, aval a\<^sub>2 s # aval a\<^sub>1 s # stk)"
[PROOF STATE]
proof (state)
this:
k < length cfs
cfs ! k = (size (acomp a\<^sub>1) + size (acomp a\<^sub>2), s, aval a\<^sub>2 s # aval a\<^sub>1 s # stk)

goal (1 subgoal):
 1. \<And>a1 a2 cfs a b k. \<lbrakk>\<And>cfs. acomp a1 \<Turnstile> cfs\<box> \<Longrightarrow> apred a1 (cfs ! 0) (cfs ! (length cfs - Suc 0)); \<And>cfs. acomp a2 \<Turnstile> cfs\<box> \<Longrightarrow> apred a2 (cfs ! 0) (cfs ! (length cfs - Suc 0)); acomp a1 @ acomp a2 @ [ADD] \<Turnstile> cfs\<box>; cfs ! 0 = (0, a, b); k < length cfs; cfs ! k = (size (acomp a1) + size (acomp a2), a, aval a2 a # aval a1 a # b)\<rbrakk> \<Longrightarrow> apred (Plus a1 a2) (0, a, b) (cfs ! (length cfs - Suc 0))
[PROOF STEP]
hence "cfs ! Suc k = (size (?ca\<^sub>1 @ ?ca\<^sub>2 @ ?i), s, aval (Plus a\<^sub>1 a\<^sub>2) s # stk)"
[PROOF STATE]
proof (prove)
using this:
k < length cfs
cfs ! k = (size (acomp a\<^sub>1) + size (acomp a\<^sub>2), s, aval a\<^sub>2 s # aval a\<^sub>1 s # stk)

goal (1 subgoal):
 1. cfs ! Suc k = (size (acomp a\<^sub>1 @ acomp a\<^sub>2 @ [ADD]), s, aval (Plus a\<^sub>1 a\<^sub>2) s # stk)
[PROOF STEP]
using A
[PROOF STATE]
proof (prove)
using this:
k < length cfs
cfs ! k = (size (acomp a\<^sub>1) + size (acomp a\<^sub>2), s, aval a\<^sub>2 s # aval a\<^sub>1 s # stk)
acomp a\<^sub>1 @ acomp a\<^sub>2 @ [ADD] \<Turnstile> cfs\<box>

goal (1 subgoal):
 1. cfs ! Suc k = (size (acomp a\<^sub>1 @ acomp a\<^sub>2 @ [ADD]), s, aval (Plus a\<^sub>1 a\<^sub>2) s # stk)
[PROOF STEP]
by (insert execl_next [of "?ca\<^sub>1 @ ?ca\<^sub>2 @ ?i" cfs k],
     simp add: execl_all_def, drule_tac impI, auto)
[PROOF STATE]
proof (state)
this:
cfs ! Suc k = (size (acomp a\<^sub>1 @ acomp a\<^sub>2 @ [ADD]), s, aval (Plus a\<^sub>1 a\<^sub>2) s # stk)

goal (1 subgoal):
 1. \<And>a1 a2 cfs a b k. \<lbrakk>\<And>cfs. acomp a1 \<Turnstile> cfs\<box> \<Longrightarrow> apred a1 (cfs ! 0) (cfs ! (length cfs - Suc 0)); \<And>cfs. acomp a2 \<Turnstile> cfs\<box> \<Longrightarrow> apred a2 (cfs ! 0) (cfs ! (length cfs - Suc 0)); acomp a1 @ acomp a2 @ [ADD] \<Turnstile> cfs\<box>; cfs ! 0 = (0, a, b); k < length cfs; cfs ! k = (size (acomp a1) + size (acomp a2), a, aval a2 a # aval a1 a # b)\<rbrakk> \<Longrightarrow> apred (Plus a1 a2) (0, a, b) (cfs ! (length cfs - Suc 0))
[PROOF STEP]
thus "apred (Plus a\<^sub>1 a\<^sub>2) (0, s, stk) (cfs ! (length cfs - Suc 0))"
[PROOF STATE]
proof (prove)
using this:
cfs ! Suc k = (size (acomp a\<^sub>1 @ acomp a\<^sub>2 @ [ADD]), s, aval (Plus a\<^sub>1 a\<^sub>2) s # stk)

goal (1 subgoal):
 1. apred (Plus a\<^sub>1 a\<^sub>2) (0, s, stk) (cfs ! (length cfs - Suc 0))
[PROOF STEP]
using A and B and C
[PROOF STATE]
proof (prove)
using this:
cfs ! Suc k = (size (acomp a\<^sub>1 @ acomp a\<^sub>2 @ [ADD]), s, aval (Plus a\<^sub>1 a\<^sub>2) s # stk)
acomp a\<^sub>1 @ acomp a\<^sub>2 @ [ADD] \<Turnstile> cfs\<box>
k < length cfs
cfs ! k = (size (acomp a\<^sub>1) + size (acomp a\<^sub>2), s, aval a\<^sub>2 s # aval a\<^sub>1 s # stk)

goal (1 subgoal):
 1. apred (Plus a\<^sub>1 a\<^sub>2) (0, s, stk) (cfs ! (length cfs - Suc 0))
[PROOF STEP]
by (insert execl_last [of "?ca\<^sub>1 @ ?ca\<^sub>2 @ ?i" cfs "Suc k"],
     simp add: execl_all_def apred_def, drule_tac impI, auto)
[PROOF STATE]
proof (state)
this:
apred (Plus a\<^sub>1 a\<^sub>2) (0, s, stk) (cfs ! (length cfs - Suc 0))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma bcomp_correct [simplified, intro]:
 "\<lbrakk>bcomp x \<Turnstile> cfs\<box>; 0 \<le> snd (snd x)\<rbrakk> \<Longrightarrow> bpred x (cfs ! 0) (cfs ! (length cfs - 1))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>bcomp x \<Turnstile> cfs\<box>; 0 \<le> snd (snd x)\<rbrakk> \<Longrightarrow> bpred x (cfs ! 0) (cfs ! (length cfs - 1))
[PROOF STEP]
proof (induction x arbitrary: cfs rule: bcomp.induct, simp_all add: Let_def,
 frule_tac [4] acomp_acomp, frule_tac [3] bcomp_bcomp, auto, force simp: bpred_def)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>b\<^sub>1 b\<^sub>2 f i cfs a b. \<lbrakk>\<And>cfs. bcomp (b\<^sub>2, f, i) \<Turnstile> cfs\<box> \<Longrightarrow> bpred (b\<^sub>2, f, i) (cfs ! 0) (cfs ! (length cfs - Suc 0)); \<And>x cfs. \<lbrakk>x = bcomp (b\<^sub>2, f, i); bcomp (b\<^sub>1, False, size (bcomp (b\<^sub>2, f, i)) + (if f then 0 else i)) \<Turnstile> cfs\<box>\<rbrakk> \<Longrightarrow> bpred (b\<^sub>1, False, size (bcomp (b\<^sub>2, f, i)) + (if f then 0 else i)) (cfs ! 0) (cfs ! (length cfs - Suc 0)); bcomp (b\<^sub>1, False, size (bcomp (b\<^sub>2, f, i)) + (if f then 0 else i)) @ bcomp (b\<^sub>2, f, i) \<Turnstile> cfs\<box>; 0 \<le> i; cfs ! 0 = (0, a, b); \<not> bval b\<^sub>1 a\<rbrakk> \<Longrightarrow> bpred (And b\<^sub>1 b\<^sub>2, f, i) (0, a, b) (cfs ! (length cfs - Suc 0))
 2. \<And>b\<^sub>1 b\<^sub>2 f i cfs a b k. \<lbrakk>\<And>cfs. bcomp (b\<^sub>2, f, i) \<Turnstile> cfs\<box> \<Longrightarrow> bpred (b\<^sub>2, f, i) (cfs ! 0) (cfs ! (length cfs - Suc 0)); \<And>x cfs. \<lbrakk>x = bcomp (b\<^sub>2, f, i); bcomp (b\<^sub>1, False, size (bcomp (b\<^sub>2, f, i)) + (if f then 0 else i)) \<Turnstile> cfs\<box>\<rbrakk> \<Longrightarrow> bpred (b\<^sub>1, False, size (bcomp (b\<^sub>2, f, i)) + (if f then 0 else i)) (cfs ! 0) (cfs ! (length cfs - Suc 0)); bcomp (b\<^sub>1, False, size (bcomp (b\<^sub>2, f, i)) + (if f then 0 else i)) @ bcomp (b\<^sub>2, f, i) \<Turnstile> cfs\<box>; 0 \<le> i; cfs ! 0 = (0, a, b); bval b\<^sub>1 a; k < length cfs; cfs ! k = (size (bcomp (b\<^sub>1, False, size (bcomp (b\<^sub>2, f, i)) + (if f then 0 else i))) + size (bcomp (b\<^sub>2, f, i)) + (if bval b\<^sub>2 a = f then i else 0), a, b)\<rbrakk> \<Longrightarrow> bpred (And b\<^sub>1 b\<^sub>2, f, i) (0, a, b) (cfs ! (length cfs - Suc 0))
 3. \<And>a\<^sub>1 a\<^sub>2 f i cfs a b k. \<lbrakk>acomp a\<^sub>1 @ acomp a\<^sub>2 @ (if f then [JMPLESS i] else [JMPGE i]) \<Turnstile> cfs\<box>; 0 \<le> i; cfs ! 0 = (0, a, b); k < length cfs; cfs ! k = (size (acomp a\<^sub>1) + size (acomp a\<^sub>2), a, aval a\<^sub>2 a # aval a\<^sub>1 a # b)\<rbrakk> \<Longrightarrow> bpred (Less a\<^sub>1 a\<^sub>2, f, i) (0, a, b) (cfs ! (length cfs - Suc 0))
[PROOF STEP]
fix b\<^sub>1 b\<^sub>2 f i cfs s stk
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>b\<^sub>1 b\<^sub>2 f i cfs a b. \<lbrakk>\<And>cfs. bcomp (b\<^sub>2, f, i) \<Turnstile> cfs\<box> \<Longrightarrow> bpred (b\<^sub>2, f, i) (cfs ! 0) (cfs ! (length cfs - Suc 0)); \<And>x cfs. \<lbrakk>x = bcomp (b\<^sub>2, f, i); bcomp (b\<^sub>1, False, size (bcomp (b\<^sub>2, f, i)) + (if f then 0 else i)) \<Turnstile> cfs\<box>\<rbrakk> \<Longrightarrow> bpred (b\<^sub>1, False, size (bcomp (b\<^sub>2, f, i)) + (if f then 0 else i)) (cfs ! 0) (cfs ! (length cfs - Suc 0)); bcomp (b\<^sub>1, False, size (bcomp (b\<^sub>2, f, i)) + (if f then 0 else i)) @ bcomp (b\<^sub>2, f, i) \<Turnstile> cfs\<box>; 0 \<le> i; cfs ! 0 = (0, a, b); \<not> bval b\<^sub>1 a\<rbrakk> \<Longrightarrow> bpred (And b\<^sub>1 b\<^sub>2, f, i) (0, a, b) (cfs ! (length cfs - Suc 0))
 2. \<And>b\<^sub>1 b\<^sub>2 f i cfs a b k. \<lbrakk>\<And>cfs. bcomp (b\<^sub>2, f, i) \<Turnstile> cfs\<box> \<Longrightarrow> bpred (b\<^sub>2, f, i) (cfs ! 0) (cfs ! (length cfs - Suc 0)); \<And>x cfs. \<lbrakk>x = bcomp (b\<^sub>2, f, i); bcomp (b\<^sub>1, False, size (bcomp (b\<^sub>2, f, i)) + (if f then 0 else i)) \<Turnstile> cfs\<box>\<rbrakk> \<Longrightarrow> bpred (b\<^sub>1, False, size (bcomp (b\<^sub>2, f, i)) + (if f then 0 else i)) (cfs ! 0) (cfs ! (length cfs - Suc 0)); bcomp (b\<^sub>1, False, size (bcomp (b\<^sub>2, f, i)) + (if f then 0 else i)) @ bcomp (b\<^sub>2, f, i) \<Turnstile> cfs\<box>; 0 \<le> i; cfs ! 0 = (0, a, b); bval b\<^sub>1 a; k < length cfs; cfs ! k = (size (bcomp (b\<^sub>1, False, size (bcomp (b\<^sub>2, f, i)) + (if f then 0 else i))) + size (bcomp (b\<^sub>2, f, i)) + (if bval b\<^sub>2 a = f then i else 0), a, b)\<rbrakk> \<Longrightarrow> bpred (And b\<^sub>1 b\<^sub>2, f, i) (0, a, b) (cfs ! (length cfs - Suc 0))
 3. \<And>a\<^sub>1 a\<^sub>2 f i cfs a b k. \<lbrakk>acomp a\<^sub>1 @ acomp a\<^sub>2 @ (if f then [JMPLESS i] else [JMPGE i]) \<Turnstile> cfs\<box>; 0 \<le> i; cfs ! 0 = (0, a, b); k < length cfs; cfs ! k = (size (acomp a\<^sub>1) + size (acomp a\<^sub>2), a, aval a\<^sub>2 a # aval a\<^sub>1 a # b)\<rbrakk> \<Longrightarrow> bpred (Less a\<^sub>1 a\<^sub>2, f, i) (0, a, b) (cfs ! (length cfs - Suc 0))
[PROOF STEP]
assume A: "bcomp (b\<^sub>1, False, size (bcomp (b\<^sub>2, f, i)) + (if f then 0 else i)) @
    bcomp (b\<^sub>2, f, i) \<Turnstile> cfs\<box>"
    (is "bcomp (_, _, ?n + ?i) @ ?cb \<Turnstile> _\<box>")
[PROOF STATE]
proof (state)
this:
bcomp (b\<^sub>1, False, size (bcomp (b\<^sub>2, f, i)) + (if f then 0 else i)) @ bcomp (b\<^sub>2, f, i) \<Turnstile> cfs\<box>

goal (3 subgoals):
 1. \<And>b\<^sub>1 b\<^sub>2 f i cfs a b. \<lbrakk>\<And>cfs. bcomp (b\<^sub>2, f, i) \<Turnstile> cfs\<box> \<Longrightarrow> bpred (b\<^sub>2, f, i) (cfs ! 0) (cfs ! (length cfs - Suc 0)); \<And>x cfs. \<lbrakk>x = bcomp (b\<^sub>2, f, i); bcomp (b\<^sub>1, False, size (bcomp (b\<^sub>2, f, i)) + (if f then 0 else i)) \<Turnstile> cfs\<box>\<rbrakk> \<Longrightarrow> bpred (b\<^sub>1, False, size (bcomp (b\<^sub>2, f, i)) + (if f then 0 else i)) (cfs ! 0) (cfs ! (length cfs - Suc 0)); bcomp (b\<^sub>1, False, size (bcomp (b\<^sub>2, f, i)) + (if f then 0 else i)) @ bcomp (b\<^sub>2, f, i) \<Turnstile> cfs\<box>; 0 \<le> i; cfs ! 0 = (0, a, b); \<not> bval b\<^sub>1 a\<rbrakk> \<Longrightarrow> bpred (And b\<^sub>1 b\<^sub>2, f, i) (0, a, b) (cfs ! (length cfs - Suc 0))
 2. \<And>b\<^sub>1 b\<^sub>2 f i cfs a b k. \<lbrakk>\<And>cfs. bcomp (b\<^sub>2, f, i) \<Turnstile> cfs\<box> \<Longrightarrow> bpred (b\<^sub>2, f, i) (cfs ! 0) (cfs ! (length cfs - Suc 0)); \<And>x cfs. \<lbrakk>x = bcomp (b\<^sub>2, f, i); bcomp (b\<^sub>1, False, size (bcomp (b\<^sub>2, f, i)) + (if f then 0 else i)) \<Turnstile> cfs\<box>\<rbrakk> \<Longrightarrow> bpred (b\<^sub>1, False, size (bcomp (b\<^sub>2, f, i)) + (if f then 0 else i)) (cfs ! 0) (cfs ! (length cfs - Suc 0)); bcomp (b\<^sub>1, False, size (bcomp (b\<^sub>2, f, i)) + (if f then 0 else i)) @ bcomp (b\<^sub>2, f, i) \<Turnstile> cfs\<box>; 0 \<le> i; cfs ! 0 = (0, a, b); bval b\<^sub>1 a; k < length cfs; cfs ! k = (size (bcomp (b\<^sub>1, False, size (bcomp (b\<^sub>2, f, i)) + (if f then 0 else i))) + size (bcomp (b\<^sub>2, f, i)) + (if bval b\<^sub>2 a = f then i else 0), a, b)\<rbrakk> \<Longrightarrow> bpred (And b\<^sub>1 b\<^sub>2, f, i) (0, a, b) (cfs ! (length cfs - Suc 0))
 3. \<And>a\<^sub>1 a\<^sub>2 f i cfs a b k. \<lbrakk>acomp a\<^sub>1 @ acomp a\<^sub>2 @ (if f then [JMPLESS i] else [JMPGE i]) \<Turnstile> cfs\<box>; 0 \<le> i; cfs ! 0 = (0, a, b); k < length cfs; cfs ! k = (size (acomp a\<^sub>1) + size (acomp a\<^sub>2), a, aval a\<^sub>2 a # aval a\<^sub>1 a # b)\<rbrakk> \<Longrightarrow> bpred (Less a\<^sub>1 a\<^sub>2, f, i) (0, a, b) (cfs ! (length cfs - Suc 0))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
bcomp (b\<^sub>1, False, size (bcomp (b\<^sub>2, f, i)) + (if f then 0 else i)) @ bcomp (b\<^sub>2, f, i) \<Turnstile> cfs\<box>

goal (3 subgoals):
 1. \<And>b\<^sub>1 b\<^sub>2 f i cfs a b. \<lbrakk>\<And>cfs. bcomp (b\<^sub>2, f, i) \<Turnstile> cfs\<box> \<Longrightarrow> bpred (b\<^sub>2, f, i) (cfs ! 0) (cfs ! (length cfs - Suc 0)); \<And>x cfs. \<lbrakk>x = bcomp (b\<^sub>2, f, i); bcomp (b\<^sub>1, False, size (bcomp (b\<^sub>2, f, i)) + (if f then 0 else i)) \<Turnstile> cfs\<box>\<rbrakk> \<Longrightarrow> bpred (b\<^sub>1, False, size (bcomp (b\<^sub>2, f, i)) + (if f then 0 else i)) (cfs ! 0) (cfs ! (length cfs - Suc 0)); bcomp (b\<^sub>1, False, size (bcomp (b\<^sub>2, f, i)) + (if f then 0 else i)) @ bcomp (b\<^sub>2, f, i) \<Turnstile> cfs\<box>; 0 \<le> i; cfs ! 0 = (0, a, b); \<not> bval b\<^sub>1 a\<rbrakk> \<Longrightarrow> bpred (And b\<^sub>1 b\<^sub>2, f, i) (0, a, b) (cfs ! (length cfs - Suc 0))
 2. \<And>b\<^sub>1 b\<^sub>2 f i cfs a b k. \<lbrakk>\<And>cfs. bcomp (b\<^sub>2, f, i) \<Turnstile> cfs\<box> \<Longrightarrow> bpred (b\<^sub>2, f, i) (cfs ! 0) (cfs ! (length cfs - Suc 0)); \<And>x cfs. \<lbrakk>x = bcomp (b\<^sub>2, f, i); bcomp (b\<^sub>1, False, size (bcomp (b\<^sub>2, f, i)) + (if f then 0 else i)) \<Turnstile> cfs\<box>\<rbrakk> \<Longrightarrow> bpred (b\<^sub>1, False, size (bcomp (b\<^sub>2, f, i)) + (if f then 0 else i)) (cfs ! 0) (cfs ! (length cfs - Suc 0)); bcomp (b\<^sub>1, False, size (bcomp (b\<^sub>2, f, i)) + (if f then 0 else i)) @ bcomp (b\<^sub>2, f, i) \<Turnstile> cfs\<box>; 0 \<le> i; cfs ! 0 = (0, a, b); bval b\<^sub>1 a; k < length cfs; cfs ! k = (size (bcomp (b\<^sub>1, False, size (bcomp (b\<^sub>2, f, i)) + (if f then 0 else i))) + size (bcomp (b\<^sub>2, f, i)) + (if bval b\<^sub>2 a = f then i else 0), a, b)\<rbrakk> \<Longrightarrow> bpred (And b\<^sub>1 b\<^sub>2, f, i) (0, a, b) (cfs ! (length cfs - Suc 0))
 3. \<And>a\<^sub>1 a\<^sub>2 f i cfs a b k. \<lbrakk>acomp a\<^sub>1 @ acomp a\<^sub>2 @ (if f then [JMPLESS i] else [JMPGE i]) \<Turnstile> cfs\<box>; 0 \<le> i; cfs ! 0 = (0, a, b); k < length cfs; cfs ! k = (size (acomp a\<^sub>1) + size (acomp a\<^sub>2), a, aval a\<^sub>2 a # aval a\<^sub>1 a # b)\<rbrakk> \<Longrightarrow> bpred (Less a\<^sub>1 a\<^sub>2, f, i) (0, a, b) (cfs ! (length cfs - Suc 0))
[PROOF STEP]
assume B: "cfs ! 0 = (0, s, stk)" and
   "\<And>cb cfs. \<lbrakk>cb = ?cb; bcomp (b\<^sub>1, False, ?n + ?i) \<Turnstile> cfs\<box>\<rbrakk> \<Longrightarrow>
      bpred (b\<^sub>1, False, ?n + ?i) (cfs ! 0) (cfs ! (length cfs - Suc 0))"
[PROOF STATE]
proof (state)
this:
cfs ! 0 = (0, s, stk)
\<lbrakk>?cb = bcomp (b\<^sub>2, f, i); bcomp (b\<^sub>1, False, size (bcomp (b\<^sub>2, f, i)) + (if f then 0 else i)) \<Turnstile> ?cfs\<box>\<rbrakk> \<Longrightarrow> bpred (b\<^sub>1, False, size (bcomp (b\<^sub>2, f, i)) + (if f then 0 else i)) (?cfs ! 0) (?cfs ! (length ?cfs - Suc 0))

goal (3 subgoals):
 1. \<And>b\<^sub>1 b\<^sub>2 f i cfs a b. \<lbrakk>\<And>cfs. bcomp (b\<^sub>2, f, i) \<Turnstile> cfs\<box> \<Longrightarrow> bpred (b\<^sub>2, f, i) (cfs ! 0) (cfs ! (length cfs - Suc 0)); \<And>x cfs. \<lbrakk>x = bcomp (b\<^sub>2, f, i); bcomp (b\<^sub>1, False, size (bcomp (b\<^sub>2, f, i)) + (if f then 0 else i)) \<Turnstile> cfs\<box>\<rbrakk> \<Longrightarrow> bpred (b\<^sub>1, False, size (bcomp (b\<^sub>2, f, i)) + (if f then 0 else i)) (cfs ! 0) (cfs ! (length cfs - Suc 0)); bcomp (b\<^sub>1, False, size (bcomp (b\<^sub>2, f, i)) + (if f then 0 else i)) @ bcomp (b\<^sub>2, f, i) \<Turnstile> cfs\<box>; 0 \<le> i; cfs ! 0 = (0, a, b); \<not> bval b\<^sub>1 a\<rbrakk> \<Longrightarrow> bpred (And b\<^sub>1 b\<^sub>2, f, i) (0, a, b) (cfs ! (length cfs - Suc 0))
 2. \<And>b\<^sub>1 b\<^sub>2 f i cfs a b k. \<lbrakk>\<And>cfs. bcomp (b\<^sub>2, f, i) \<Turnstile> cfs\<box> \<Longrightarrow> bpred (b\<^sub>2, f, i) (cfs ! 0) (cfs ! (length cfs - Suc 0)); \<And>x cfs. \<lbrakk>x = bcomp (b\<^sub>2, f, i); bcomp (b\<^sub>1, False, size (bcomp (b\<^sub>2, f, i)) + (if f then 0 else i)) \<Turnstile> cfs\<box>\<rbrakk> \<Longrightarrow> bpred (b\<^sub>1, False, size (bcomp (b\<^sub>2, f, i)) + (if f then 0 else i)) (cfs ! 0) (cfs ! (length cfs - Suc 0)); bcomp (b\<^sub>1, False, size (bcomp (b\<^sub>2, f, i)) + (if f then 0 else i)) @ bcomp (b\<^sub>2, f, i) \<Turnstile> cfs\<box>; 0 \<le> i; cfs ! 0 = (0, a, b); bval b\<^sub>1 a; k < length cfs; cfs ! k = (size (bcomp (b\<^sub>1, False, size (bcomp (b\<^sub>2, f, i)) + (if f then 0 else i))) + size (bcomp (b\<^sub>2, f, i)) + (if bval b\<^sub>2 a = f then i else 0), a, b)\<rbrakk> \<Longrightarrow> bpred (And b\<^sub>1 b\<^sub>2, f, i) (0, a, b) (cfs ! (length cfs - Suc 0))
 3. \<And>a\<^sub>1 a\<^sub>2 f i cfs a b k. \<lbrakk>acomp a\<^sub>1 @ acomp a\<^sub>2 @ (if f then [JMPLESS i] else [JMPGE i]) \<Turnstile> cfs\<box>; 0 \<le> i; cfs ! 0 = (0, a, b); k < length cfs; cfs ! k = (size (acomp a\<^sub>1) + size (acomp a\<^sub>2), a, aval a\<^sub>2 a # aval a\<^sub>1 a # b)\<rbrakk> \<Longrightarrow> bpred (Less a\<^sub>1 a\<^sub>2, f, i) (0, a, b) (cfs ! (length cfs - Suc 0))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
bcomp (b\<^sub>1, False, size (bcomp (b\<^sub>2, f, i)) + (if f then 0 else i)) @ bcomp (b\<^sub>2, f, i) \<Turnstile> cfs\<box>
cfs ! 0 = (0, s, stk)
\<lbrakk>?cb = bcomp (b\<^sub>2, f, i); bcomp (b\<^sub>1, False, size (bcomp (b\<^sub>2, f, i)) + (if f then 0 else i)) \<Turnstile> ?cfs\<box>\<rbrakk> \<Longrightarrow> bpred (b\<^sub>1, False, size (bcomp (b\<^sub>2, f, i)) + (if f then 0 else i)) (?cfs ! 0) (?cfs ! (length ?cfs - Suc 0))
[PROOF STEP]
have "\<exists>k < length cfs. bpred (b\<^sub>1, False, ?n + ?i)
    (off [] (cfs ! 0)) (off [] (cfs ! k))"
[PROOF STATE]
proof (prove)
using this:
bcomp (b\<^sub>1, False, size (bcomp (b\<^sub>2, f, i)) + (if f then 0 else i)) @ bcomp (b\<^sub>2, f, i) \<Turnstile> cfs\<box>
cfs ! 0 = (0, s, stk)
\<lbrakk>?cb = bcomp (b\<^sub>2, f, i); bcomp (b\<^sub>1, False, size (bcomp (b\<^sub>2, f, i)) + (if f then 0 else i)) \<Turnstile> ?cfs\<box>\<rbrakk> \<Longrightarrow> bpred (b\<^sub>1, False, size (bcomp (b\<^sub>2, f, i)) + (if f then 0 else i)) (?cfs ! 0) (?cfs ! (length ?cfs - Suc 0))

goal (1 subgoal):
 1. \<exists>k<length cfs. bpred (b\<^sub>1, False, size (bcomp (b\<^sub>2, f, i)) + (if f then 0 else i)) (off [] (cfs ! 0)) (off [] (cfs ! k))
[PROOF STEP]
by (rule_tac execl_all_sub, auto simp: execl_all_def)
[PROOF STATE]
proof (state)
this:
\<exists>k<length cfs. bpred (b\<^sub>1, False, size (bcomp (b\<^sub>2, f, i)) + (if f then 0 else i)) (off [] (cfs ! 0)) (off [] (cfs ! k))

goal (3 subgoals):
 1. \<And>b\<^sub>1 b\<^sub>2 f i cfs a b. \<lbrakk>\<And>cfs. bcomp (b\<^sub>2, f, i) \<Turnstile> cfs\<box> \<Longrightarrow> bpred (b\<^sub>2, f, i) (cfs ! 0) (cfs ! (length cfs - Suc 0)); \<And>x cfs. \<lbrakk>x = bcomp (b\<^sub>2, f, i); bcomp (b\<^sub>1, False, size (bcomp (b\<^sub>2, f, i)) + (if f then 0 else i)) \<Turnstile> cfs\<box>\<rbrakk> \<Longrightarrow> bpred (b\<^sub>1, False, size (bcomp (b\<^sub>2, f, i)) + (if f then 0 else i)) (cfs ! 0) (cfs ! (length cfs - Suc 0)); bcomp (b\<^sub>1, False, size (bcomp (b\<^sub>2, f, i)) + (if f then 0 else i)) @ bcomp (b\<^sub>2, f, i) \<Turnstile> cfs\<box>; 0 \<le> i; cfs ! 0 = (0, a, b); \<not> bval b\<^sub>1 a\<rbrakk> \<Longrightarrow> bpred (And b\<^sub>1 b\<^sub>2, f, i) (0, a, b) (cfs ! (length cfs - Suc 0))
 2. \<And>b\<^sub>1 b\<^sub>2 f i cfs a b k. \<lbrakk>\<And>cfs. bcomp (b\<^sub>2, f, i) \<Turnstile> cfs\<box> \<Longrightarrow> bpred (b\<^sub>2, f, i) (cfs ! 0) (cfs ! (length cfs - Suc 0)); \<And>x cfs. \<lbrakk>x = bcomp (b\<^sub>2, f, i); bcomp (b\<^sub>1, False, size (bcomp (b\<^sub>2, f, i)) + (if f then 0 else i)) \<Turnstile> cfs\<box>\<rbrakk> \<Longrightarrow> bpred (b\<^sub>1, False, size (bcomp (b\<^sub>2, f, i)) + (if f then 0 else i)) (cfs ! 0) (cfs ! (length cfs - Suc 0)); bcomp (b\<^sub>1, False, size (bcomp (b\<^sub>2, f, i)) + (if f then 0 else i)) @ bcomp (b\<^sub>2, f, i) \<Turnstile> cfs\<box>; 0 \<le> i; cfs ! 0 = (0, a, b); bval b\<^sub>1 a; k < length cfs; cfs ! k = (size (bcomp (b\<^sub>1, False, size (bcomp (b\<^sub>2, f, i)) + (if f then 0 else i))) + size (bcomp (b\<^sub>2, f, i)) + (if bval b\<^sub>2 a = f then i else 0), a, b)\<rbrakk> \<Longrightarrow> bpred (And b\<^sub>1 b\<^sub>2, f, i) (0, a, b) (cfs ! (length cfs - Suc 0))
 3. \<And>a\<^sub>1 a\<^sub>2 f i cfs a b k. \<lbrakk>acomp a\<^sub>1 @ acomp a\<^sub>2 @ (if f then [JMPLESS i] else [JMPGE i]) \<Turnstile> cfs\<box>; 0 \<le> i; cfs ! 0 = (0, a, b); k < length cfs; cfs ! k = (size (acomp a\<^sub>1) + size (acomp a\<^sub>2), a, aval a\<^sub>2 a # aval a\<^sub>1 a # b)\<rbrakk> \<Longrightarrow> bpred (Less a\<^sub>1 a\<^sub>2, f, i) (0, a, b) (cfs ! (length cfs - Suc 0))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<exists>k<length cfs. bpred (b\<^sub>1, False, size (bcomp (b\<^sub>2, f, i)) + (if f then 0 else i)) (off [] (cfs ! 0)) (off [] (cfs ! k))

goal (3 subgoals):
 1. \<And>b\<^sub>1 b\<^sub>2 f i cfs a b. \<lbrakk>\<And>cfs. bcomp (b\<^sub>2, f, i) \<Turnstile> cfs\<box> \<Longrightarrow> bpred (b\<^sub>2, f, i) (cfs ! 0) (cfs ! (length cfs - Suc 0)); \<And>x cfs. \<lbrakk>x = bcomp (b\<^sub>2, f, i); bcomp (b\<^sub>1, False, size (bcomp (b\<^sub>2, f, i)) + (if f then 0 else i)) \<Turnstile> cfs\<box>\<rbrakk> \<Longrightarrow> bpred (b\<^sub>1, False, size (bcomp (b\<^sub>2, f, i)) + (if f then 0 else i)) (cfs ! 0) (cfs ! (length cfs - Suc 0)); bcomp (b\<^sub>1, False, size (bcomp (b\<^sub>2, f, i)) + (if f then 0 else i)) @ bcomp (b\<^sub>2, f, i) \<Turnstile> cfs\<box>; 0 \<le> i; cfs ! 0 = (0, a, b); \<not> bval b\<^sub>1 a\<rbrakk> \<Longrightarrow> bpred (And b\<^sub>1 b\<^sub>2, f, i) (0, a, b) (cfs ! (length cfs - Suc 0))
 2. \<And>b\<^sub>1 b\<^sub>2 f i cfs a b k. \<lbrakk>\<And>cfs. bcomp (b\<^sub>2, f, i) \<Turnstile> cfs\<box> \<Longrightarrow> bpred (b\<^sub>2, f, i) (cfs ! 0) (cfs ! (length cfs - Suc 0)); \<And>x cfs. \<lbrakk>x = bcomp (b\<^sub>2, f, i); bcomp (b\<^sub>1, False, size (bcomp (b\<^sub>2, f, i)) + (if f then 0 else i)) \<Turnstile> cfs\<box>\<rbrakk> \<Longrightarrow> bpred (b\<^sub>1, False, size (bcomp (b\<^sub>2, f, i)) + (if f then 0 else i)) (cfs ! 0) (cfs ! (length cfs - Suc 0)); bcomp (b\<^sub>1, False, size (bcomp (b\<^sub>2, f, i)) + (if f then 0 else i)) @ bcomp (b\<^sub>2, f, i) \<Turnstile> cfs\<box>; 0 \<le> i; cfs ! 0 = (0, a, b); bval b\<^sub>1 a; k < length cfs; cfs ! k = (size (bcomp (b\<^sub>1, False, size (bcomp (b\<^sub>2, f, i)) + (if f then 0 else i))) + size (bcomp (b\<^sub>2, f, i)) + (if bval b\<^sub>2 a = f then i else 0), a, b)\<rbrakk> \<Longrightarrow> bpred (And b\<^sub>1 b\<^sub>2, f, i) (0, a, b) (cfs ! (length cfs - Suc 0))
 3. \<And>a\<^sub>1 a\<^sub>2 f i cfs a b k. \<lbrakk>acomp a\<^sub>1 @ acomp a\<^sub>2 @ (if f then [JMPLESS i] else [JMPGE i]) \<Turnstile> cfs\<box>; 0 \<le> i; cfs ! 0 = (0, a, b); k < length cfs; cfs ! k = (size (acomp a\<^sub>1) + size (acomp a\<^sub>2), a, aval a\<^sub>2 a # aval a\<^sub>1 a # b)\<rbrakk> \<Longrightarrow> bpred (Less a\<^sub>1 a\<^sub>2, f, i) (0, a, b) (cfs ! (length cfs - Suc 0))
[PROOF STEP]
assume C: "\<not> bval b\<^sub>1 s"
[PROOF STATE]
proof (state)
this:
\<not> bval b\<^sub>1 s

goal (3 subgoals):
 1. \<And>b\<^sub>1 b\<^sub>2 f i cfs a b. \<lbrakk>\<And>cfs. bcomp (b\<^sub>2, f, i) \<Turnstile> cfs\<box> \<Longrightarrow> bpred (b\<^sub>2, f, i) (cfs ! 0) (cfs ! (length cfs - Suc 0)); \<And>x cfs. \<lbrakk>x = bcomp (b\<^sub>2, f, i); bcomp (b\<^sub>1, False, size (bcomp (b\<^sub>2, f, i)) + (if f then 0 else i)) \<Turnstile> cfs\<box>\<rbrakk> \<Longrightarrow> bpred (b\<^sub>1, False, size (bcomp (b\<^sub>2, f, i)) + (if f then 0 else i)) (cfs ! 0) (cfs ! (length cfs - Suc 0)); bcomp (b\<^sub>1, False, size (bcomp (b\<^sub>2, f, i)) + (if f then 0 else i)) @ bcomp (b\<^sub>2, f, i) \<Turnstile> cfs\<box>; 0 \<le> i; cfs ! 0 = (0, a, b); \<not> bval b\<^sub>1 a\<rbrakk> \<Longrightarrow> bpred (And b\<^sub>1 b\<^sub>2, f, i) (0, a, b) (cfs ! (length cfs - Suc 0))
 2. \<And>b\<^sub>1 b\<^sub>2 f i cfs a b k. \<lbrakk>\<And>cfs. bcomp (b\<^sub>2, f, i) \<Turnstile> cfs\<box> \<Longrightarrow> bpred (b\<^sub>2, f, i) (cfs ! 0) (cfs ! (length cfs - Suc 0)); \<And>x cfs. \<lbrakk>x = bcomp (b\<^sub>2, f, i); bcomp (b\<^sub>1, False, size (bcomp (b\<^sub>2, f, i)) + (if f then 0 else i)) \<Turnstile> cfs\<box>\<rbrakk> \<Longrightarrow> bpred (b\<^sub>1, False, size (bcomp (b\<^sub>2, f, i)) + (if f then 0 else i)) (cfs ! 0) (cfs ! (length cfs - Suc 0)); bcomp (b\<^sub>1, False, size (bcomp (b\<^sub>2, f, i)) + (if f then 0 else i)) @ bcomp (b\<^sub>2, f, i) \<Turnstile> cfs\<box>; 0 \<le> i; cfs ! 0 = (0, a, b); bval b\<^sub>1 a; k < length cfs; cfs ! k = (size (bcomp (b\<^sub>1, False, size (bcomp (b\<^sub>2, f, i)) + (if f then 0 else i))) + size (bcomp (b\<^sub>2, f, i)) + (if bval b\<^sub>2 a = f then i else 0), a, b)\<rbrakk> \<Longrightarrow> bpred (And b\<^sub>1 b\<^sub>2, f, i) (0, a, b) (cfs ! (length cfs - Suc 0))
 3. \<And>a\<^sub>1 a\<^sub>2 f i cfs a b k. \<lbrakk>acomp a\<^sub>1 @ acomp a\<^sub>2 @ (if f then [JMPLESS i] else [JMPGE i]) \<Turnstile> cfs\<box>; 0 \<le> i; cfs ! 0 = (0, a, b); k < length cfs; cfs ! k = (size (acomp a\<^sub>1) + size (acomp a\<^sub>2), a, aval a\<^sub>2 a # aval a\<^sub>1 a # b)\<rbrakk> \<Longrightarrow> bpred (Less a\<^sub>1 a\<^sub>2, f, i) (0, a, b) (cfs ! (length cfs - Suc 0))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<exists>k<length cfs. bpred (b\<^sub>1, False, size (bcomp (b\<^sub>2, f, i)) + (if f then 0 else i)) (off [] (cfs ! 0)) (off [] (cfs ! k))
\<not> bval b\<^sub>1 s
[PROOF STEP]
obtain k where D: "k < length cfs" and
    E: "cfs ! k = (size (bcomp (b\<^sub>1, False, ?n + ?i)) + ?n + ?i, s, stk)"
[PROOF STATE]
proof (prove)
using this:
\<exists>k<length cfs. bpred (b\<^sub>1, False, size (bcomp (b\<^sub>2, f, i)) + (if f then 0 else i)) (off [] (cfs ! 0)) (off [] (cfs ! k))
\<not> bval b\<^sub>1 s

goal (1 subgoal):
 1. (\<And>k. \<lbrakk>k < length cfs; cfs ! k = (size (bcomp (b\<^sub>1, False, size (bcomp (b\<^sub>2, f, i)) + (if f then 0 else i))) + size (bcomp (b\<^sub>2, f, i)) + (if f then 0 else i), s, stk)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using B
[PROOF STATE]
proof (prove)
using this:
\<exists>k<length cfs. bpred (b\<^sub>1, False, size (bcomp (b\<^sub>2, f, i)) + (if f then 0 else i)) (off [] (cfs ! 0)) (off [] (cfs ! k))
\<not> bval b\<^sub>1 s
cfs ! 0 = (0, s, stk)

goal (1 subgoal):
 1. (\<And>k. \<lbrakk>k < length cfs; cfs ! k = (size (bcomp (b\<^sub>1, False, size (bcomp (b\<^sub>2, f, i)) + (if f then 0 else i))) + size (bcomp (b\<^sub>2, f, i)) + (if f then 0 else i), s, stk)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp: bpred_def)
[PROOF STATE]
proof (state)
this:
k < length cfs
cfs ! k = (size (bcomp (b\<^sub>1, False, size (bcomp (b\<^sub>2, f, i)) + (if f then 0 else i))) + size (bcomp (b\<^sub>2, f, i)) + (if f then 0 else i), s, stk)

goal (3 subgoals):
 1. \<And>b\<^sub>1 b\<^sub>2 f i cfs a b. \<lbrakk>\<And>cfs. bcomp (b\<^sub>2, f, i) \<Turnstile> cfs\<box> \<Longrightarrow> bpred (b\<^sub>2, f, i) (cfs ! 0) (cfs ! (length cfs - Suc 0)); \<And>x cfs. \<lbrakk>x = bcomp (b\<^sub>2, f, i); bcomp (b\<^sub>1, False, size (bcomp (b\<^sub>2, f, i)) + (if f then 0 else i)) \<Turnstile> cfs\<box>\<rbrakk> \<Longrightarrow> bpred (b\<^sub>1, False, size (bcomp (b\<^sub>2, f, i)) + (if f then 0 else i)) (cfs ! 0) (cfs ! (length cfs - Suc 0)); bcomp (b\<^sub>1, False, size (bcomp (b\<^sub>2, f, i)) + (if f then 0 else i)) @ bcomp (b\<^sub>2, f, i) \<Turnstile> cfs\<box>; 0 \<le> i; cfs ! 0 = (0, a, b); \<not> bval b\<^sub>1 a\<rbrakk> \<Longrightarrow> bpred (And b\<^sub>1 b\<^sub>2, f, i) (0, a, b) (cfs ! (length cfs - Suc 0))
 2. \<And>b\<^sub>1 b\<^sub>2 f i cfs a b k. \<lbrakk>\<And>cfs. bcomp (b\<^sub>2, f, i) \<Turnstile> cfs\<box> \<Longrightarrow> bpred (b\<^sub>2, f, i) (cfs ! 0) (cfs ! (length cfs - Suc 0)); \<And>x cfs. \<lbrakk>x = bcomp (b\<^sub>2, f, i); bcomp (b\<^sub>1, False, size (bcomp (b\<^sub>2, f, i)) + (if f then 0 else i)) \<Turnstile> cfs\<box>\<rbrakk> \<Longrightarrow> bpred (b\<^sub>1, False, size (bcomp (b\<^sub>2, f, i)) + (if f then 0 else i)) (cfs ! 0) (cfs ! (length cfs - Suc 0)); bcomp (b\<^sub>1, False, size (bcomp (b\<^sub>2, f, i)) + (if f then 0 else i)) @ bcomp (b\<^sub>2, f, i) \<Turnstile> cfs\<box>; 0 \<le> i; cfs ! 0 = (0, a, b); bval b\<^sub>1 a; k < length cfs; cfs ! k = (size (bcomp (b\<^sub>1, False, size (bcomp (b\<^sub>2, f, i)) + (if f then 0 else i))) + size (bcomp (b\<^sub>2, f, i)) + (if bval b\<^sub>2 a = f then i else 0), a, b)\<rbrakk> \<Longrightarrow> bpred (And b\<^sub>1 b\<^sub>2, f, i) (0, a, b) (cfs ! (length cfs - Suc 0))
 3. \<And>a\<^sub>1 a\<^sub>2 f i cfs a b k. \<lbrakk>acomp a\<^sub>1 @ acomp a\<^sub>2 @ (if f then [JMPLESS i] else [JMPGE i]) \<Turnstile> cfs\<box>; 0 \<le> i; cfs ! 0 = (0, a, b); k < length cfs; cfs ! k = (size (acomp a\<^sub>1) + size (acomp a\<^sub>2), a, aval a\<^sub>2 a # aval a\<^sub>1 a # b)\<rbrakk> \<Longrightarrow> bpred (Less a\<^sub>1 a\<^sub>2, f, i) (0, a, b) (cfs ! (length cfs - Suc 0))
[PROOF STEP]
assume "0 \<le> i"
[PROOF STATE]
proof (state)
this:
0 \<le> i

goal (3 subgoals):
 1. \<And>b\<^sub>1 b\<^sub>2 f i cfs a b. \<lbrakk>\<And>cfs. bcomp (b\<^sub>2, f, i) \<Turnstile> cfs\<box> \<Longrightarrow> bpred (b\<^sub>2, f, i) (cfs ! 0) (cfs ! (length cfs - Suc 0)); \<And>x cfs. \<lbrakk>x = bcomp (b\<^sub>2, f, i); bcomp (b\<^sub>1, False, size (bcomp (b\<^sub>2, f, i)) + (if f then 0 else i)) \<Turnstile> cfs\<box>\<rbrakk> \<Longrightarrow> bpred (b\<^sub>1, False, size (bcomp (b\<^sub>2, f, i)) + (if f then 0 else i)) (cfs ! 0) (cfs ! (length cfs - Suc 0)); bcomp (b\<^sub>1, False, size (bcomp (b\<^sub>2, f, i)) + (if f then 0 else i)) @ bcomp (b\<^sub>2, f, i) \<Turnstile> cfs\<box>; 0 \<le> i; cfs ! 0 = (0, a, b); \<not> bval b\<^sub>1 a\<rbrakk> \<Longrightarrow> bpred (And b\<^sub>1 b\<^sub>2, f, i) (0, a, b) (cfs ! (length cfs - Suc 0))
 2. \<And>b\<^sub>1 b\<^sub>2 f i cfs a b k. \<lbrakk>\<And>cfs. bcomp (b\<^sub>2, f, i) \<Turnstile> cfs\<box> \<Longrightarrow> bpred (b\<^sub>2, f, i) (cfs ! 0) (cfs ! (length cfs - Suc 0)); \<And>x cfs. \<lbrakk>x = bcomp (b\<^sub>2, f, i); bcomp (b\<^sub>1, False, size (bcomp (b\<^sub>2, f, i)) + (if f then 0 else i)) \<Turnstile> cfs\<box>\<rbrakk> \<Longrightarrow> bpred (b\<^sub>1, False, size (bcomp (b\<^sub>2, f, i)) + (if f then 0 else i)) (cfs ! 0) (cfs ! (length cfs - Suc 0)); bcomp (b\<^sub>1, False, size (bcomp (b\<^sub>2, f, i)) + (if f then 0 else i)) @ bcomp (b\<^sub>2, f, i) \<Turnstile> cfs\<box>; 0 \<le> i; cfs ! 0 = (0, a, b); bval b\<^sub>1 a; k < length cfs; cfs ! k = (size (bcomp (b\<^sub>1, False, size (bcomp (b\<^sub>2, f, i)) + (if f then 0 else i))) + size (bcomp (b\<^sub>2, f, i)) + (if bval b\<^sub>2 a = f then i else 0), a, b)\<rbrakk> \<Longrightarrow> bpred (And b\<^sub>1 b\<^sub>2, f, i) (0, a, b) (cfs ! (length cfs - Suc 0))
 3. \<And>a\<^sub>1 a\<^sub>2 f i cfs a b k. \<lbrakk>acomp a\<^sub>1 @ acomp a\<^sub>2 @ (if f then [JMPLESS i] else [JMPGE i]) \<Turnstile> cfs\<box>; 0 \<le> i; cfs ! 0 = (0, a, b); k < length cfs; cfs ! k = (size (acomp a\<^sub>1) + size (acomp a\<^sub>2), a, aval a\<^sub>2 a # aval a\<^sub>1 a # b)\<rbrakk> \<Longrightarrow> bpred (Less a\<^sub>1 a\<^sub>2, f, i) (0, a, b) (cfs ! (length cfs - Suc 0))
[PROOF STEP]
thus "bpred (And b\<^sub>1 b\<^sub>2, f, i) (0, s, stk) (cfs ! (length cfs - Suc 0))"
[PROOF STATE]
proof (prove)
using this:
0 \<le> i

goal (1 subgoal):
 1. bpred (And b\<^sub>1 b\<^sub>2, f, i) (0, s, stk) (cfs ! (length cfs - Suc 0))
[PROOF STEP]
using A and C and D and E
[PROOF STATE]
proof (prove)
using this:
0 \<le> i
bcomp (b\<^sub>1, False, size (bcomp (b\<^sub>2, f, i)) + (if f then 0 else i)) @ bcomp (b\<^sub>2, f, i) \<Turnstile> cfs\<box>
\<not> bval b\<^sub>1 s
k < length cfs
cfs ! k = (size (bcomp (b\<^sub>1, False, size (bcomp (b\<^sub>2, f, i)) + (if f then 0 else i))) + size (bcomp (b\<^sub>2, f, i)) + (if f then 0 else i), s, stk)

goal (1 subgoal):
 1. bpred (And b\<^sub>1 b\<^sub>2, f, i) (0, s, stk) (cfs ! (length cfs - Suc 0))
[PROOF STEP]
by (insert execl_last, auto simp:
     execl_all_def bpred_def Let_def)
[PROOF STATE]
proof (state)
this:
bpred (And b\<^sub>1 b\<^sub>2, f, i) (0, s, stk) (cfs ! (length cfs - Suc 0))

goal (2 subgoals):
 1. \<And>b\<^sub>1 b\<^sub>2 f i cfs a b k. \<lbrakk>\<And>cfs. bcomp (b\<^sub>2, f, i) \<Turnstile> cfs\<box> \<Longrightarrow> bpred (b\<^sub>2, f, i) (cfs ! 0) (cfs ! (length cfs - Suc 0)); \<And>x cfs. \<lbrakk>x = bcomp (b\<^sub>2, f, i); bcomp (b\<^sub>1, False, size (bcomp (b\<^sub>2, f, i)) + (if f then 0 else i)) \<Turnstile> cfs\<box>\<rbrakk> \<Longrightarrow> bpred (b\<^sub>1, False, size (bcomp (b\<^sub>2, f, i)) + (if f then 0 else i)) (cfs ! 0) (cfs ! (length cfs - Suc 0)); bcomp (b\<^sub>1, False, size (bcomp (b\<^sub>2, f, i)) + (if f then 0 else i)) @ bcomp (b\<^sub>2, f, i) \<Turnstile> cfs\<box>; 0 \<le> i; cfs ! 0 = (0, a, b); bval b\<^sub>1 a; k < length cfs; cfs ! k = (size (bcomp (b\<^sub>1, False, size (bcomp (b\<^sub>2, f, i)) + (if f then 0 else i))) + size (bcomp (b\<^sub>2, f, i)) + (if bval b\<^sub>2 a = f then i else 0), a, b)\<rbrakk> \<Longrightarrow> bpred (And b\<^sub>1 b\<^sub>2, f, i) (0, a, b) (cfs ! (length cfs - Suc 0))
 2. \<And>a\<^sub>1 a\<^sub>2 f i cfs a b k. \<lbrakk>acomp a\<^sub>1 @ acomp a\<^sub>2 @ (if f then [JMPLESS i] else [JMPGE i]) \<Turnstile> cfs\<box>; 0 \<le> i; cfs ! 0 = (0, a, b); k < length cfs; cfs ! k = (size (acomp a\<^sub>1) + size (acomp a\<^sub>2), a, aval a\<^sub>2 a # aval a\<^sub>1 a # b)\<rbrakk> \<Longrightarrow> bpred (Less a\<^sub>1 a\<^sub>2, f, i) (0, a, b) (cfs ! (length cfs - Suc 0))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>b\<^sub>1 b\<^sub>2 f i cfs a b k. \<lbrakk>\<And>cfs. bcomp (b\<^sub>2, f, i) \<Turnstile> cfs\<box> \<Longrightarrow> bpred (b\<^sub>2, f, i) (cfs ! 0) (cfs ! (length cfs - Suc 0)); \<And>x cfs. \<lbrakk>x = bcomp (b\<^sub>2, f, i); bcomp (b\<^sub>1, False, size (bcomp (b\<^sub>2, f, i)) + (if f then 0 else i)) \<Turnstile> cfs\<box>\<rbrakk> \<Longrightarrow> bpred (b\<^sub>1, False, size (bcomp (b\<^sub>2, f, i)) + (if f then 0 else i)) (cfs ! 0) (cfs ! (length cfs - Suc 0)); bcomp (b\<^sub>1, False, size (bcomp (b\<^sub>2, f, i)) + (if f then 0 else i)) @ bcomp (b\<^sub>2, f, i) \<Turnstile> cfs\<box>; 0 \<le> i; cfs ! 0 = (0, a, b); bval b\<^sub>1 a; k < length cfs; cfs ! k = (size (bcomp (b\<^sub>1, False, size (bcomp (b\<^sub>2, f, i)) + (if f then 0 else i))) + size (bcomp (b\<^sub>2, f, i)) + (if bval b\<^sub>2 a = f then i else 0), a, b)\<rbrakk> \<Longrightarrow> bpred (And b\<^sub>1 b\<^sub>2, f, i) (0, a, b) (cfs ! (length cfs - Suc 0))
 2. \<And>a\<^sub>1 a\<^sub>2 f i cfs a b k. \<lbrakk>acomp a\<^sub>1 @ acomp a\<^sub>2 @ (if f then [JMPLESS i] else [JMPGE i]) \<Turnstile> cfs\<box>; 0 \<le> i; cfs ! 0 = (0, a, b); k < length cfs; cfs ! k = (size (acomp a\<^sub>1) + size (acomp a\<^sub>2), a, aval a\<^sub>2 a # aval a\<^sub>1 a # b)\<rbrakk> \<Longrightarrow> bpred (Less a\<^sub>1 a\<^sub>2, f, i) (0, a, b) (cfs ! (length cfs - Suc 0))
[PROOF STEP]
fix b\<^sub>1 b\<^sub>2 f i cfs s stk k
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>b\<^sub>1 b\<^sub>2 f i cfs a b k. \<lbrakk>\<And>cfs. bcomp (b\<^sub>2, f, i) \<Turnstile> cfs\<box> \<Longrightarrow> bpred (b\<^sub>2, f, i) (cfs ! 0) (cfs ! (length cfs - Suc 0)); \<And>x cfs. \<lbrakk>x = bcomp (b\<^sub>2, f, i); bcomp (b\<^sub>1, False, size (bcomp (b\<^sub>2, f, i)) + (if f then 0 else i)) \<Turnstile> cfs\<box>\<rbrakk> \<Longrightarrow> bpred (b\<^sub>1, False, size (bcomp (b\<^sub>2, f, i)) + (if f then 0 else i)) (cfs ! 0) (cfs ! (length cfs - Suc 0)); bcomp (b\<^sub>1, False, size (bcomp (b\<^sub>2, f, i)) + (if f then 0 else i)) @ bcomp (b\<^sub>2, f, i) \<Turnstile> cfs\<box>; 0 \<le> i; cfs ! 0 = (0, a, b); bval b\<^sub>1 a; k < length cfs; cfs ! k = (size (bcomp (b\<^sub>1, False, size (bcomp (b\<^sub>2, f, i)) + (if f then 0 else i))) + size (bcomp (b\<^sub>2, f, i)) + (if bval b\<^sub>2 a = f then i else 0), a, b)\<rbrakk> \<Longrightarrow> bpred (And b\<^sub>1 b\<^sub>2, f, i) (0, a, b) (cfs ! (length cfs - Suc 0))
 2. \<And>a\<^sub>1 a\<^sub>2 f i cfs a b k. \<lbrakk>acomp a\<^sub>1 @ acomp a\<^sub>2 @ (if f then [JMPLESS i] else [JMPGE i]) \<Turnstile> cfs\<box>; 0 \<le> i; cfs ! 0 = (0, a, b); k < length cfs; cfs ! k = (size (acomp a\<^sub>1) + size (acomp a\<^sub>2), a, aval a\<^sub>2 a # aval a\<^sub>1 a # b)\<rbrakk> \<Longrightarrow> bpred (Less a\<^sub>1 a\<^sub>2, f, i) (0, a, b) (cfs ! (length cfs - Suc 0))
[PROOF STEP]
assume A: "bcomp (b\<^sub>1, False, size (bcomp (b\<^sub>2, f, i)) + (if f then 0 else i)) @
    bcomp (b\<^sub>2, f, i) \<Turnstile> cfs\<box>"
    (is "?cb\<^sub>1 @ ?cb\<^sub>2 \<Turnstile> _\<box>")
[PROOF STATE]
proof (state)
this:
bcomp (b\<^sub>1, False, size (bcomp (b\<^sub>2, f, i)) + (if f then 0 else i)) @ bcomp (b\<^sub>2, f, i) \<Turnstile> cfs\<box>

goal (2 subgoals):
 1. \<And>b\<^sub>1 b\<^sub>2 f i cfs a b k. \<lbrakk>\<And>cfs. bcomp (b\<^sub>2, f, i) \<Turnstile> cfs\<box> \<Longrightarrow> bpred (b\<^sub>2, f, i) (cfs ! 0) (cfs ! (length cfs - Suc 0)); \<And>x cfs. \<lbrakk>x = bcomp (b\<^sub>2, f, i); bcomp (b\<^sub>1, False, size (bcomp (b\<^sub>2, f, i)) + (if f then 0 else i)) \<Turnstile> cfs\<box>\<rbrakk> \<Longrightarrow> bpred (b\<^sub>1, False, size (bcomp (b\<^sub>2, f, i)) + (if f then 0 else i)) (cfs ! 0) (cfs ! (length cfs - Suc 0)); bcomp (b\<^sub>1, False, size (bcomp (b\<^sub>2, f, i)) + (if f then 0 else i)) @ bcomp (b\<^sub>2, f, i) \<Turnstile> cfs\<box>; 0 \<le> i; cfs ! 0 = (0, a, b); bval b\<^sub>1 a; k < length cfs; cfs ! k = (size (bcomp (b\<^sub>1, False, size (bcomp (b\<^sub>2, f, i)) + (if f then 0 else i))) + size (bcomp (b\<^sub>2, f, i)) + (if bval b\<^sub>2 a = f then i else 0), a, b)\<rbrakk> \<Longrightarrow> bpred (And b\<^sub>1 b\<^sub>2, f, i) (0, a, b) (cfs ! (length cfs - Suc 0))
 2. \<And>a\<^sub>1 a\<^sub>2 f i cfs a b k. \<lbrakk>acomp a\<^sub>1 @ acomp a\<^sub>2 @ (if f then [JMPLESS i] else [JMPGE i]) \<Turnstile> cfs\<box>; 0 \<le> i; cfs ! 0 = (0, a, b); k < length cfs; cfs ! k = (size (acomp a\<^sub>1) + size (acomp a\<^sub>2), a, aval a\<^sub>2 a # aval a\<^sub>1 a # b)\<rbrakk> \<Longrightarrow> bpred (Less a\<^sub>1 a\<^sub>2, f, i) (0, a, b) (cfs ! (length cfs - Suc 0))
[PROOF STEP]
assume "k < length cfs" and "0 \<le> i" and "bval b\<^sub>1 s" and
   "cfs ! k = (size ?cb\<^sub>1 + size ?cb\<^sub>2 + (if bval b\<^sub>2 s = f then i else 0), s, stk)"
[PROOF STATE]
proof (state)
this:
k < length cfs
0 \<le> i
bval b\<^sub>1 s
cfs ! k = (size (bcomp (b\<^sub>1, False, size (bcomp (b\<^sub>2, f, i)) + (if f then 0 else i))) + size (bcomp (b\<^sub>2, f, i)) + (if bval b\<^sub>2 s = f then i else 0), s, stk)

goal (2 subgoals):
 1. \<And>b\<^sub>1 b\<^sub>2 f i cfs a b k. \<lbrakk>\<And>cfs. bcomp (b\<^sub>2, f, i) \<Turnstile> cfs\<box> \<Longrightarrow> bpred (b\<^sub>2, f, i) (cfs ! 0) (cfs ! (length cfs - Suc 0)); \<And>x cfs. \<lbrakk>x = bcomp (b\<^sub>2, f, i); bcomp (b\<^sub>1, False, size (bcomp (b\<^sub>2, f, i)) + (if f then 0 else i)) \<Turnstile> cfs\<box>\<rbrakk> \<Longrightarrow> bpred (b\<^sub>1, False, size (bcomp (b\<^sub>2, f, i)) + (if f then 0 else i)) (cfs ! 0) (cfs ! (length cfs - Suc 0)); bcomp (b\<^sub>1, False, size (bcomp (b\<^sub>2, f, i)) + (if f then 0 else i)) @ bcomp (b\<^sub>2, f, i) \<Turnstile> cfs\<box>; 0 \<le> i; cfs ! 0 = (0, a, b); bval b\<^sub>1 a; k < length cfs; cfs ! k = (size (bcomp (b\<^sub>1, False, size (bcomp (b\<^sub>2, f, i)) + (if f then 0 else i))) + size (bcomp (b\<^sub>2, f, i)) + (if bval b\<^sub>2 a = f then i else 0), a, b)\<rbrakk> \<Longrightarrow> bpred (And b\<^sub>1 b\<^sub>2, f, i) (0, a, b) (cfs ! (length cfs - Suc 0))
 2. \<And>a\<^sub>1 a\<^sub>2 f i cfs a b k. \<lbrakk>acomp a\<^sub>1 @ acomp a\<^sub>2 @ (if f then [JMPLESS i] else [JMPGE i]) \<Turnstile> cfs\<box>; 0 \<le> i; cfs ! 0 = (0, a, b); k < length cfs; cfs ! k = (size (acomp a\<^sub>1) + size (acomp a\<^sub>2), a, aval a\<^sub>2 a # aval a\<^sub>1 a # b)\<rbrakk> \<Longrightarrow> bpred (Less a\<^sub>1 a\<^sub>2, f, i) (0, a, b) (cfs ! (length cfs - Suc 0))
[PROOF STEP]
thus "bpred (And b\<^sub>1 b\<^sub>2, f, i) (0, s, stk) (cfs ! (length cfs - Suc 0))"
[PROOF STATE]
proof (prove)
using this:
k < length cfs
0 \<le> i
bval b\<^sub>1 s
cfs ! k = (size (bcomp (b\<^sub>1, False, size (bcomp (b\<^sub>2, f, i)) + (if f then 0 else i))) + size (bcomp (b\<^sub>2, f, i)) + (if bval b\<^sub>2 s = f then i else 0), s, stk)

goal (1 subgoal):
 1. bpred (And b\<^sub>1 b\<^sub>2, f, i) (0, s, stk) (cfs ! (length cfs - Suc 0))
[PROOF STEP]
using A
[PROOF STATE]
proof (prove)
using this:
k < length cfs
0 \<le> i
bval b\<^sub>1 s
cfs ! k = (size (bcomp (b\<^sub>1, False, size (bcomp (b\<^sub>2, f, i)) + (if f then 0 else i))) + size (bcomp (b\<^sub>2, f, i)) + (if bval b\<^sub>2 s = f then i else 0), s, stk)
bcomp (b\<^sub>1, False, size (bcomp (b\<^sub>2, f, i)) + (if f then 0 else i)) @ bcomp (b\<^sub>2, f, i) \<Turnstile> cfs\<box>

goal (1 subgoal):
 1. bpred (And b\<^sub>1 b\<^sub>2, f, i) (0, s, stk) (cfs ! (length cfs - Suc 0))
[PROOF STEP]
by (insert execl_last, auto simp: execl_all_def bpred_def Let_def)
[PROOF STATE]
proof (state)
this:
bpred (And b\<^sub>1 b\<^sub>2, f, i) (0, s, stk) (cfs ! (length cfs - Suc 0))

goal (1 subgoal):
 1. \<And>a\<^sub>1 a\<^sub>2 f i cfs a b k. \<lbrakk>acomp a\<^sub>1 @ acomp a\<^sub>2 @ (if f then [JMPLESS i] else [JMPGE i]) \<Turnstile> cfs\<box>; 0 \<le> i; cfs ! 0 = (0, a, b); k < length cfs; cfs ! k = (size (acomp a\<^sub>1) + size (acomp a\<^sub>2), a, aval a\<^sub>2 a # aval a\<^sub>1 a # b)\<rbrakk> \<Longrightarrow> bpred (Less a\<^sub>1 a\<^sub>2, f, i) (0, a, b) (cfs ! (length cfs - Suc 0))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a\<^sub>1 a\<^sub>2 f i cfs a b k. \<lbrakk>acomp a\<^sub>1 @ acomp a\<^sub>2 @ (if f then [JMPLESS i] else [JMPGE i]) \<Turnstile> cfs\<box>; 0 \<le> i; cfs ! 0 = (0, a, b); k < length cfs; cfs ! k = (size (acomp a\<^sub>1) + size (acomp a\<^sub>2), a, aval a\<^sub>2 a # aval a\<^sub>1 a # b)\<rbrakk> \<Longrightarrow> bpred (Less a\<^sub>1 a\<^sub>2, f, i) (0, a, b) (cfs ! (length cfs - Suc 0))
[PROOF STEP]
fix a\<^sub>1 a\<^sub>2 f i cfs s stk k
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a\<^sub>1 a\<^sub>2 f i cfs a b k. \<lbrakk>acomp a\<^sub>1 @ acomp a\<^sub>2 @ (if f then [JMPLESS i] else [JMPGE i]) \<Turnstile> cfs\<box>; 0 \<le> i; cfs ! 0 = (0, a, b); k < length cfs; cfs ! k = (size (acomp a\<^sub>1) + size (acomp a\<^sub>2), a, aval a\<^sub>2 a # aval a\<^sub>1 a # b)\<rbrakk> \<Longrightarrow> bpred (Less a\<^sub>1 a\<^sub>2, f, i) (0, a, b) (cfs ! (length cfs - Suc 0))
[PROOF STEP]
assume A: "acomp a\<^sub>1 @ acomp a\<^sub>2 @
    (if f then [JMPLESS i] else [JMPGE i]) \<Turnstile> cfs\<box>"
    (is "?ca\<^sub>1 @ ?ca\<^sub>2 @ ?i \<Turnstile> _\<box>")
[PROOF STATE]
proof (state)
this:
acomp a\<^sub>1 @ acomp a\<^sub>2 @ (if f then [JMPLESS i] else [JMPGE i]) \<Turnstile> cfs\<box>

goal (1 subgoal):
 1. \<And>a\<^sub>1 a\<^sub>2 f i cfs a b k. \<lbrakk>acomp a\<^sub>1 @ acomp a\<^sub>2 @ (if f then [JMPLESS i] else [JMPGE i]) \<Turnstile> cfs\<box>; 0 \<le> i; cfs ! 0 = (0, a, b); k < length cfs; cfs ! k = (size (acomp a\<^sub>1) + size (acomp a\<^sub>2), a, aval a\<^sub>2 a # aval a\<^sub>1 a # b)\<rbrakk> \<Longrightarrow> bpred (Less a\<^sub>1 a\<^sub>2, f, i) (0, a, b) (cfs ! (length cfs - Suc 0))
[PROOF STEP]
assume B: "k < length cfs" and
    C: "cfs ! k = (size ?ca\<^sub>1 + size ?ca\<^sub>2, s, aval a\<^sub>2 s # aval a\<^sub>1 s # stk)"
[PROOF STATE]
proof (state)
this:
k < length cfs
cfs ! k = (size (acomp a\<^sub>1) + size (acomp a\<^sub>2), s, aval a\<^sub>2 s # aval a\<^sub>1 s # stk)

goal (1 subgoal):
 1. \<And>a\<^sub>1 a\<^sub>2 f i cfs a b k. \<lbrakk>acomp a\<^sub>1 @ acomp a\<^sub>2 @ (if f then [JMPLESS i] else [JMPGE i]) \<Turnstile> cfs\<box>; 0 \<le> i; cfs ! 0 = (0, a, b); k < length cfs; cfs ! k = (size (acomp a\<^sub>1) + size (acomp a\<^sub>2), a, aval a\<^sub>2 a # aval a\<^sub>1 a # b)\<rbrakk> \<Longrightarrow> bpred (Less a\<^sub>1 a\<^sub>2, f, i) (0, a, b) (cfs ! (length cfs - Suc 0))
[PROOF STEP]
hence D: "cfs ! Suc k =
    (size (?ca\<^sub>1 @ ?ca\<^sub>2 @ ?i) + (if bval (Less a\<^sub>1 a\<^sub>2) s = f then i else 0), s, stk)"
[PROOF STATE]
proof (prove)
using this:
k < length cfs
cfs ! k = (size (acomp a\<^sub>1) + size (acomp a\<^sub>2), s, aval a\<^sub>2 s # aval a\<^sub>1 s # stk)

goal (1 subgoal):
 1. cfs ! Suc k = (size (acomp a\<^sub>1 @ acomp a\<^sub>2 @ (if f then [JMPLESS i] else [JMPGE i])) + (if bval (Less a\<^sub>1 a\<^sub>2) s = f then i else 0), s, stk)
[PROOF STEP]
using A
[PROOF STATE]
proof (prove)
using this:
k < length cfs
cfs ! k = (size (acomp a\<^sub>1) + size (acomp a\<^sub>2), s, aval a\<^sub>2 s # aval a\<^sub>1 s # stk)
acomp a\<^sub>1 @ acomp a\<^sub>2 @ (if f then [JMPLESS i] else [JMPGE i]) \<Turnstile> cfs\<box>

goal (1 subgoal):
 1. cfs ! Suc k = (size (acomp a\<^sub>1 @ acomp a\<^sub>2 @ (if f then [JMPLESS i] else [JMPGE i])) + (if bval (Less a\<^sub>1 a\<^sub>2) s = f then i else 0), s, stk)
[PROOF STEP]
by (insert execl_next [of "?ca\<^sub>1 @ ?ca\<^sub>2 @ ?i" cfs k],
     simp add: execl_all_def, drule_tac impI, auto split: if_split_asm)
[PROOF STATE]
proof (state)
this:
cfs ! Suc k = (size (acomp a\<^sub>1 @ acomp a\<^sub>2 @ (if f then [JMPLESS i] else [JMPGE i])) + (if bval (Less a\<^sub>1 a\<^sub>2) s = f then i else 0), s, stk)

goal (1 subgoal):
 1. \<And>a\<^sub>1 a\<^sub>2 f i cfs a b k. \<lbrakk>acomp a\<^sub>1 @ acomp a\<^sub>2 @ (if f then [JMPLESS i] else [JMPGE i]) \<Turnstile> cfs\<box>; 0 \<le> i; cfs ! 0 = (0, a, b); k < length cfs; cfs ! k = (size (acomp a\<^sub>1) + size (acomp a\<^sub>2), a, aval a\<^sub>2 a # aval a\<^sub>1 a # b)\<rbrakk> \<Longrightarrow> bpred (Less a\<^sub>1 a\<^sub>2, f, i) (0, a, b) (cfs ! (length cfs - Suc 0))
[PROOF STEP]
assume "0 \<le> i"
[PROOF STATE]
proof (state)
this:
0 \<le> i

goal (1 subgoal):
 1. \<And>a\<^sub>1 a\<^sub>2 f i cfs a b k. \<lbrakk>acomp a\<^sub>1 @ acomp a\<^sub>2 @ (if f then [JMPLESS i] else [JMPGE i]) \<Turnstile> cfs\<box>; 0 \<le> i; cfs ! 0 = (0, a, b); k < length cfs; cfs ! k = (size (acomp a\<^sub>1) + size (acomp a\<^sub>2), a, aval a\<^sub>2 a # aval a\<^sub>1 a # b)\<rbrakk> \<Longrightarrow> bpred (Less a\<^sub>1 a\<^sub>2, f, i) (0, a, b) (cfs ! (length cfs - Suc 0))
[PROOF STEP]
with A and B and C and D
[PROOF STATE]
proof (chain)
picking this:
acomp a\<^sub>1 @ acomp a\<^sub>2 @ (if f then [JMPLESS i] else [JMPGE i]) \<Turnstile> cfs\<box>
k < length cfs
cfs ! k = (size (acomp a\<^sub>1) + size (acomp a\<^sub>2), s, aval a\<^sub>2 s # aval a\<^sub>1 s # stk)
cfs ! Suc k = (size (acomp a\<^sub>1 @ acomp a\<^sub>2 @ (if f then [JMPLESS i] else [JMPGE i])) + (if bval (Less a\<^sub>1 a\<^sub>2) s = f then i else 0), s, stk)
0 \<le> i
[PROOF STEP]
have "length cfs - 1 = Suc k"
[PROOF STATE]
proof (prove)
using this:
acomp a\<^sub>1 @ acomp a\<^sub>2 @ (if f then [JMPLESS i] else [JMPGE i]) \<Turnstile> cfs\<box>
k < length cfs
cfs ! k = (size (acomp a\<^sub>1) + size (acomp a\<^sub>2), s, aval a\<^sub>2 s # aval a\<^sub>1 s # stk)
cfs ! Suc k = (size (acomp a\<^sub>1 @ acomp a\<^sub>2 @ (if f then [JMPLESS i] else [JMPGE i])) + (if bval (Less a\<^sub>1 a\<^sub>2) s = f then i else 0), s, stk)
0 \<le> i

goal (1 subgoal):
 1. length cfs - 1 = Suc k
[PROOF STEP]
by (rule_tac execl_last, auto simp: execl_all_def, simp split: if_split_asm)
[PROOF STATE]
proof (state)
this:
length cfs - 1 = Suc k

goal (1 subgoal):
 1. \<And>a\<^sub>1 a\<^sub>2 f i cfs a b k. \<lbrakk>acomp a\<^sub>1 @ acomp a\<^sub>2 @ (if f then [JMPLESS i] else [JMPGE i]) \<Turnstile> cfs\<box>; 0 \<le> i; cfs ! 0 = (0, a, b); k < length cfs; cfs ! k = (size (acomp a\<^sub>1) + size (acomp a\<^sub>2), a, aval a\<^sub>2 a # aval a\<^sub>1 a # b)\<rbrakk> \<Longrightarrow> bpred (Less a\<^sub>1 a\<^sub>2, f, i) (0, a, b) (cfs ! (length cfs - Suc 0))
[PROOF STEP]
thus "bpred (Less a\<^sub>1 a\<^sub>2, f, i) (0, s, stk) (cfs ! (length cfs - Suc 0))"
[PROOF STATE]
proof (prove)
using this:
length cfs - 1 = Suc k

goal (1 subgoal):
 1. bpred (Less a\<^sub>1 a\<^sub>2, f, i) (0, s, stk) (cfs ! (length cfs - Suc 0))
[PROOF STEP]
using D
[PROOF STATE]
proof (prove)
using this:
length cfs - 1 = Suc k
cfs ! Suc k = (size (acomp a\<^sub>1 @ acomp a\<^sub>2 @ (if f then [JMPLESS i] else [JMPGE i])) + (if bval (Less a\<^sub>1 a\<^sub>2) s = f then i else 0), s, stk)

goal (1 subgoal):
 1. bpred (Less a\<^sub>1 a\<^sub>2, f, i) (0, s, stk) (cfs ! (length cfs - Suc 0))
[PROOF STEP]
by (simp add: bpred_def)
[PROOF STATE]
proof (state)
this:
bpred (Less a\<^sub>1 a\<^sub>2, f, i) (0, s, stk) (cfs ! (length cfs - Suc 0))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma bcomp_ccomp:
 "\<lbrakk>bcomp (b, f, i) @ ccomp c @ P \<Turnstile> cfs\<box>; 0 \<le> i;
    \<And>cfs. ccomp c \<Turnstile> cfs\<box> \<Longrightarrow> cpred c (cfs ! 0) (cfs ! (length cfs - 1))\<rbrakk> \<Longrightarrow>
  case cfs ! 0 of (pc, s, stk) \<Rightarrow> pc = 0 \<and> (bval b s \<noteq> f \<longrightarrow>
    (\<exists>k < length cfs. case cfs ! k of (pc', s', stk') \<Rightarrow>
      pc' = size (bcomp (b, f, i) @ ccomp c) \<and> (c, s) \<Rightarrow> s' \<and> stk' = stk))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>bcomp (b, f, i) @ ccomp c @ P \<Turnstile> cfs\<box>; 0 \<le> i; \<And>cfs. ccomp c \<Turnstile> cfs\<box> \<Longrightarrow> cpred c (cfs ! 0) (cfs ! (length cfs - 1))\<rbrakk> \<Longrightarrow> case cfs ! 0 of (pc, s, stk) \<Rightarrow> pc = 0 \<and> (bval b s \<noteq> f \<longrightarrow> (\<exists>k<length cfs. case cfs ! k of (pc', s', stk') \<Rightarrow> pc' = size (bcomp (b, f, i) @ ccomp c) \<and> (c, s) \<Rightarrow> s' \<and> stk' = stk))
[PROOF STEP]
by (clarify, rule conjI, simp add: execl_all_def, rule impI, drule execl_all_sub2
 [where I = "\<lambda>s. if bval b s = f then i else 0" and I' = "\<lambda>s. 0"
 and Q = "\<lambda>s s'. s' = s" and Q' = "\<lambda>s s'. (c, s) \<Rightarrow> s'" and F = "\<lambda>s stk. stk"
 and F' = "\<lambda>s stk. stk"], insert bcomp_correct [of "(b, f, i)"],
 auto simp: bpred_def cpred_def)


[STATEMENT]
lemma ccomp_ccomp:
 "\<lbrakk>ccomp c\<^sub>1 @ ccomp c\<^sub>2 \<Turnstile> cfs\<box>;
    \<And>cfs. ccomp c\<^sub>1 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c\<^sub>1 (cfs ! 0) (cfs ! (length cfs - 1));
    \<And>cfs. ccomp c\<^sub>2 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c\<^sub>2 (cfs ! 0) (cfs ! (length cfs - 1))\<rbrakk> \<Longrightarrow>
  case cfs ! 0 of (pc, s, stk) \<Rightarrow> pc = 0 \<and> (\<exists>k < length cfs. \<exists>t.
    case cfs ! k of (pc', s', stk') \<Rightarrow> pc' = size (ccomp c\<^sub>1 @ ccomp c\<^sub>2) \<and>
      (c\<^sub>1, s) \<Rightarrow> t \<and> (c\<^sub>2, t) \<Rightarrow> s' \<and> stk' = stk)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ccomp c\<^sub>1 @ ccomp c\<^sub>2 \<Turnstile> cfs\<box>; \<And>cfs. ccomp c\<^sub>1 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c\<^sub>1 (cfs ! 0) (cfs ! (length cfs - 1)); \<And>cfs. ccomp c\<^sub>2 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c\<^sub>2 (cfs ! 0) (cfs ! (length cfs - 1))\<rbrakk> \<Longrightarrow> case cfs ! 0 of (pc, s, stk) \<Rightarrow> pc = 0 \<and> (\<exists>k<length cfs. \<exists>t. case cfs ! k of (pc', s', stk') \<Rightarrow> pc' = size (ccomp c\<^sub>1 @ ccomp c\<^sub>2) \<and> (c\<^sub>1, s) \<Rightarrow> t \<and> (c\<^sub>2, t) \<Rightarrow> s' \<and> stk' = stk)
[PROOF STEP]
by (subst (asm) append_Nil2 [symmetric], drule execl_all_sub2 [where I = "\<lambda>s. 0"
 and I' = "\<lambda>s. 0" and Q = "\<lambda>s s'. (c\<^sub>1, s) \<Rightarrow> s'" and Q' = "\<lambda>s s'. (c\<^sub>2, s) \<Rightarrow> s'"
 and F = "\<lambda>s stk. stk" and F' = "\<lambda>s stk. stk"], auto simp: cpred_def, force)