[STATEMENT]
lemma fill_count_item [rule_format]:
  assumes A: "index_less index key"
  shows
   "(\<forall>x \<in> set xs. key x \<in> {mi..ma}) \<longrightarrow>
    ns \<noteq> [] \<longrightarrow>
    offs_pred ns ub xs index key mi ma \<longrightarrow>
    length xs \<le> ub \<longrightarrow>
      count (mset (map the (fill xs ns index key ub mi ma))) x =
      count (mset xs) x + (if the None = x then ub - length xs else 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>x\<in>set xs. key x \<in> {mi..ma}) \<longrightarrow> ns \<noteq> [] \<longrightarrow> offs_pred ns ub xs index key mi ma \<longrightarrow> length xs \<le> ub \<longrightarrow> count (mset (map the (fill xs ns index key ub mi ma))) x = count (mset xs) x + (if the None = x then ub - length xs else 0)
[PROOF STEP]
proof (induction xs arbitrary: ns, simp add: replicate_count, (rule impI)+,
 simp add: Let_def map_update del: count_add_mset mset_map split del: if_split,
 (erule conjE)+, subst add_mset_add_single, simp only: count_single count_union)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a xs ns. \<lbrakk>\<And>ns. ns \<noteq> [] \<longrightarrow> offs_pred ns ub xs index key mi ma \<longrightarrow> count (mset (map the (fill xs ns index key ub mi ma))) x = count (mset xs) x + (if the None = x then ub - length xs else 0); ns \<noteq> []; offs_pred ns ub (a # xs) index key mi ma; Suc (length xs) \<le> ub; mi \<le> key a; key a \<le> ma; \<forall>x\<in>set xs. mi \<le> key x \<and> key x \<le> ma\<rbrakk> \<Longrightarrow> count (mset ((map the (fill xs (ns[index key a (length ns) mi ma := Suc (ns ! index key a (length ns) mi ma)]) index key ub mi ma))[ns ! index key a (length ns) mi ma := a])) x = count (mset xs) x + (if a = x then 1 else 0) + (if the None = x then ub - length (a # xs) else 0)
[PROOF STEP]
fix y xs and ns :: "nat list"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a xs ns. \<lbrakk>\<And>ns. ns \<noteq> [] \<longrightarrow> offs_pred ns ub xs index key mi ma \<longrightarrow> count (mset (map the (fill xs ns index key ub mi ma))) x = count (mset xs) x + (if the None = x then ub - length xs else 0); ns \<noteq> []; offs_pred ns ub (a # xs) index key mi ma; Suc (length xs) \<le> ub; mi \<le> key a; key a \<le> ma; \<forall>x\<in>set xs. mi \<le> key x \<and> key x \<le> ma\<rbrakk> \<Longrightarrow> count (mset ((map the (fill xs (ns[index key a (length ns) mi ma := Suc (ns ! index key a (length ns) mi ma)]) index key ub mi ma))[ns ! index key a (length ns) mi ma := a])) x = count (mset xs) x + (if a = x then 1 else 0) + (if the None = x then ub - length (a # xs) else 0)
[PROOF STEP]
let ?i = "index key y (length ns) mi ma"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a xs ns. \<lbrakk>\<And>ns. ns \<noteq> [] \<longrightarrow> offs_pred ns ub xs index key mi ma \<longrightarrow> count (mset (map the (fill xs ns index key ub mi ma))) x = count (mset xs) x + (if the None = x then ub - length xs else 0); ns \<noteq> []; offs_pred ns ub (a # xs) index key mi ma; Suc (length xs) \<le> ub; mi \<le> key a; key a \<le> ma; \<forall>x\<in>set xs. mi \<le> key x \<and> key x \<le> ma\<rbrakk> \<Longrightarrow> count (mset ((map the (fill xs (ns[index key a (length ns) mi ma := Suc (ns ! index key a (length ns) mi ma)]) index key ub mi ma))[ns ! index key a (length ns) mi ma := a])) x = count (mset xs) x + (if a = x then 1 else 0) + (if the None = x then ub - length (a # xs) else 0)
[PROOF STEP]
let ?ns' = "ns[?i := Suc (ns ! ?i)]"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a xs ns. \<lbrakk>\<And>ns. ns \<noteq> [] \<longrightarrow> offs_pred ns ub xs index key mi ma \<longrightarrow> count (mset (map the (fill xs ns index key ub mi ma))) x = count (mset xs) x + (if the None = x then ub - length xs else 0); ns \<noteq> []; offs_pred ns ub (a # xs) index key mi ma; Suc (length xs) \<le> ub; mi \<le> key a; key a \<le> ma; \<forall>x\<in>set xs. mi \<le> key x \<and> key x \<le> ma\<rbrakk> \<Longrightarrow> count (mset ((map the (fill xs (ns[index key a (length ns) mi ma := Suc (ns ! index key a (length ns) mi ma)]) index key ub mi ma))[ns ! index key a (length ns) mi ma := a])) x = count (mset xs) x + (if a = x then 1 else 0) + (if the None = x then ub - length (a # xs) else 0)
[PROOF STEP]
assume
    B: "\<forall>x \<in> set xs. mi \<le> key x \<and> key x \<le> ma" and
    C: "mi \<le> key y" and
    D: "key y \<le> ma" and
    E: "ns \<noteq> []" and
    F: "offs_pred ns ub (y # xs) index key mi ma" and
    G: "Suc (length xs) \<le> ub"
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>set xs. mi \<le> key x \<and> key x \<le> ma
mi \<le> key y
key y \<le> ma
ns \<noteq> []
offs_pred ns ub (y # xs) index key mi ma
Suc (length xs) \<le> ub

goal (1 subgoal):
 1. \<And>a xs ns. \<lbrakk>\<And>ns. ns \<noteq> [] \<longrightarrow> offs_pred ns ub xs index key mi ma \<longrightarrow> count (mset (map the (fill xs ns index key ub mi ma))) x = count (mset xs) x + (if the None = x then ub - length xs else 0); ns \<noteq> []; offs_pred ns ub (a # xs) index key mi ma; Suc (length xs) \<le> ub; mi \<le> key a; key a \<le> ma; \<forall>x\<in>set xs. mi \<le> key x \<and> key x \<le> ma\<rbrakk> \<Longrightarrow> count (mset ((map the (fill xs (ns[index key a (length ns) mi ma := Suc (ns ! index key a (length ns) mi ma)]) index key ub mi ma))[ns ! index key a (length ns) mi ma := a])) x = count (mset xs) x + (if a = x then 1 else 0) + (if the None = x then ub - length (a # xs) else 0)
[PROOF STEP]
have H: "?i < length ns"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. index key y (length ns) mi ma < length ns
[PROOF STEP]
using A and C and D and E
[PROOF STATE]
proof (prove)
using this:
index_less index key
mi \<le> key y
key y \<le> ma
ns \<noteq> []

goal (1 subgoal):
 1. index key y (length ns) mi ma < length ns
[PROOF STEP]
by (simp add: index_less_def)
[PROOF STATE]
proof (state)
this:
index key y (length ns) mi ma < length ns

goal (1 subgoal):
 1. \<And>a xs ns. \<lbrakk>\<And>ns. ns \<noteq> [] \<longrightarrow> offs_pred ns ub xs index key mi ma \<longrightarrow> count (mset (map the (fill xs ns index key ub mi ma))) x = count (mset xs) x + (if the None = x then ub - length xs else 0); ns \<noteq> []; offs_pred ns ub (a # xs) index key mi ma; Suc (length xs) \<le> ub; mi \<le> key a; key a \<le> ma; \<forall>x\<in>set xs. mi \<le> key x \<and> key x \<le> ma\<rbrakk> \<Longrightarrow> count (mset ((map the (fill xs (ns[index key a (length ns) mi ma := Suc (ns ! index key a (length ns) mi ma)]) index key ub mi ma))[ns ! index key a (length ns) mi ma := a])) x = count (mset xs) x + (if a = x then 1 else 0) + (if the None = x then ub - length (a # xs) else 0)
[PROOF STEP]
assume "\<And>ns. ns \<noteq> [] \<longrightarrow> offs_pred ns ub xs index key mi ma \<longrightarrow>
    count (mset (map the (fill xs ns index key ub mi ma))) x =
    count (mset xs) x + (if the None = x then ub - length xs else 0)"
[PROOF STATE]
proof (state)
this:
?ns \<noteq> [] \<longrightarrow> offs_pred ?ns ub xs index key mi ma \<longrightarrow> count (mset (map the (fill xs ?ns index key ub mi ma))) x = count (mset xs) x + (if the None = x then ub - length xs else 0)

goal (1 subgoal):
 1. \<And>a xs ns. \<lbrakk>\<And>ns. ns \<noteq> [] \<longrightarrow> offs_pred ns ub xs index key mi ma \<longrightarrow> count (mset (map the (fill xs ns index key ub mi ma))) x = count (mset xs) x + (if the None = x then ub - length xs else 0); ns \<noteq> []; offs_pred ns ub (a # xs) index key mi ma; Suc (length xs) \<le> ub; mi \<le> key a; key a \<le> ma; \<forall>x\<in>set xs. mi \<le> key x \<and> key x \<le> ma\<rbrakk> \<Longrightarrow> count (mset ((map the (fill xs (ns[index key a (length ns) mi ma := Suc (ns ! index key a (length ns) mi ma)]) index key ub mi ma))[ns ! index key a (length ns) mi ma := a])) x = count (mset xs) x + (if a = x then 1 else 0) + (if the None = x then ub - length (a # xs) else 0)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
?ns \<noteq> [] \<longrightarrow> offs_pred ?ns ub xs index key mi ma \<longrightarrow> count (mset (map the (fill xs ?ns index key ub mi ma))) x = count (mset xs) x + (if the None = x then ub - length xs else 0)

goal (1 subgoal):
 1. \<And>a xs ns. \<lbrakk>\<And>ns. ns \<noteq> [] \<longrightarrow> offs_pred ns ub xs index key mi ma \<longrightarrow> count (mset (map the (fill xs ns index key ub mi ma))) x = count (mset xs) x + (if the None = x then ub - length xs else 0); ns \<noteq> []; offs_pred ns ub (a # xs) index key mi ma; Suc (length xs) \<le> ub; mi \<le> key a; key a \<le> ma; \<forall>x\<in>set xs. mi \<le> key x \<and> key x \<le> ma\<rbrakk> \<Longrightarrow> count (mset ((map the (fill xs (ns[index key a (length ns) mi ma := Suc (ns ! index key a (length ns) mi ma)]) index key ub mi ma))[ns ! index key a (length ns) mi ma := a])) x = count (mset xs) x + (if a = x then 1 else 0) + (if the None = x then ub - length (a # xs) else 0)
[PROOF STEP]
have "offs_pred ?ns' ub xs index key mi ma"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. offs_pred (ns[index key y (length ns) mi ma := Suc (ns ! index key y (length ns) mi ma)]) ub xs index key mi ma
[PROOF STEP]
using F and H
[PROOF STATE]
proof (prove)
using this:
offs_pred ns ub (y # xs) index key mi ma
index key y (length ns) mi ma < length ns

goal (1 subgoal):
 1. offs_pred (ns[index key y (length ns) mi ma := Suc (ns ! index key y (length ns) mi ma)]) ub xs index key mi ma
[PROOF STEP]
by (rule_tac offs_pred_cons, simp_all)
[PROOF STATE]
proof (state)
this:
offs_pred (ns[index key y (length ns) mi ma := Suc (ns ! index key y (length ns) mi ma)]) ub xs index key mi ma

goal (1 subgoal):
 1. \<And>a xs ns. \<lbrakk>\<And>ns. ns \<noteq> [] \<longrightarrow> offs_pred ns ub xs index key mi ma \<longrightarrow> count (mset (map the (fill xs ns index key ub mi ma))) x = count (mset xs) x + (if the None = x then ub - length xs else 0); ns \<noteq> []; offs_pred ns ub (a # xs) index key mi ma; Suc (length xs) \<le> ub; mi \<le> key a; key a \<le> ma; \<forall>x\<in>set xs. mi \<le> key x \<and> key x \<le> ma\<rbrakk> \<Longrightarrow> count (mset ((map the (fill xs (ns[index key a (length ns) mi ma := Suc (ns ! index key a (length ns) mi ma)]) index key ub mi ma))[ns ! index key a (length ns) mi ma := a])) x = count (mset xs) x + (if a = x then 1 else 0) + (if the None = x then ub - length (a # xs) else 0)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
?ns \<noteq> [] \<longrightarrow> offs_pred ?ns ub xs index key mi ma \<longrightarrow> count (mset (map the (fill xs ?ns index key ub mi ma))) x = count (mset xs) x + (if the None = x then ub - length xs else 0)
offs_pred (ns[index key y (length ns) mi ma := Suc (ns ! index key y (length ns) mi ma)]) ub xs index key mi ma
[PROOF STEP]
have "count (mset (map the (fill xs ?ns' index key ub mi ma))) x =
    count (mset xs) x + (if the None = x then ub - length xs else 0)"
[PROOF STATE]
proof (prove)
using this:
?ns \<noteq> [] \<longrightarrow> offs_pred ?ns ub xs index key mi ma \<longrightarrow> count (mset (map the (fill xs ?ns index key ub mi ma))) x = count (mset xs) x + (if the None = x then ub - length xs else 0)
offs_pred (ns[index key y (length ns) mi ma := Suc (ns ! index key y (length ns) mi ma)]) ub xs index key mi ma

goal (1 subgoal):
 1. count (mset (map the (fill xs (ns[index key y (length ns) mi ma := Suc (ns ! index key y (length ns) mi ma)]) index key ub mi ma))) x = count (mset xs) x + (if the None = x then ub - length xs else 0)
[PROOF STEP]
using E
[PROOF STATE]
proof (prove)
using this:
?ns \<noteq> [] \<longrightarrow> offs_pred ?ns ub xs index key mi ma \<longrightarrow> count (mset (map the (fill xs ?ns index key ub mi ma))) x = count (mset xs) x + (if the None = x then ub - length xs else 0)
offs_pred (ns[index key y (length ns) mi ma := Suc (ns ! index key y (length ns) mi ma)]) ub xs index key mi ma
ns \<noteq> []

goal (1 subgoal):
 1. count (mset (map the (fill xs (ns[index key y (length ns) mi ma := Suc (ns ! index key y (length ns) mi ma)]) index key ub mi ma))) x = count (mset xs) x + (if the None = x then ub - length xs else 0)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
count (mset (map the (fill xs (ns[index key y (length ns) mi ma := Suc (ns ! index key y (length ns) mi ma)]) index key ub mi ma))) x = count (mset xs) x + (if the None = x then ub - length xs else 0)

goal (1 subgoal):
 1. \<And>a xs ns. \<lbrakk>\<And>ns. ns \<noteq> [] \<longrightarrow> offs_pred ns ub xs index key mi ma \<longrightarrow> count (mset (map the (fill xs ns index key ub mi ma))) x = count (mset xs) x + (if the None = x then ub - length xs else 0); ns \<noteq> []; offs_pred ns ub (a # xs) index key mi ma; Suc (length xs) \<le> ub; mi \<le> key a; key a \<le> ma; \<forall>x\<in>set xs. mi \<le> key x \<and> key x \<le> ma\<rbrakk> \<Longrightarrow> count (mset ((map the (fill xs (ns[index key a (length ns) mi ma := Suc (ns ! index key a (length ns) mi ma)]) index key ub mi ma))[ns ! index key a (length ns) mi ma := a])) x = count (mset xs) x + (if a = x then 1 else 0) + (if the None = x then ub - length (a # xs) else 0)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
count (mset (map the (fill xs (ns[index key y (length ns) mi ma := Suc (ns ! index key y (length ns) mi ma)]) index key ub mi ma))) x = count (mset xs) x + (if the None = x then ub - length xs else 0)

goal (1 subgoal):
 1. \<And>a xs ns. \<lbrakk>\<And>ns. ns \<noteq> [] \<longrightarrow> offs_pred ns ub xs index key mi ma \<longrightarrow> count (mset (map the (fill xs ns index key ub mi ma))) x = count (mset xs) x + (if the None = x then ub - length xs else 0); ns \<noteq> []; offs_pred ns ub (a # xs) index key mi ma; Suc (length xs) \<le> ub; mi \<le> key a; key a \<le> ma; \<forall>x\<in>set xs. mi \<le> key x \<and> key x \<le> ma\<rbrakk> \<Longrightarrow> count (mset ((map the (fill xs (ns[index key a (length ns) mi ma := Suc (ns ! index key a (length ns) mi ma)]) index key ub mi ma))[ns ! index key a (length ns) mi ma := a])) x = count (mset xs) x + (if a = x then 1 else 0) + (if the None = x then ub - length (a # xs) else 0)
[PROOF STEP]
have "ns ! ?i + offs_num (length ns) (y # xs)
    index key mi ma ?i \<le> ub"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ns ! index key y (length ns) mi ma + offs_num (length ns) (y # xs) index key mi ma (index key y (length ns) mi ma) \<le> ub
[PROOF STEP]
using F and H
[PROOF STATE]
proof (prove)
using this:
offs_pred ns ub (y # xs) index key mi ma
index key y (length ns) mi ma < length ns

goal (1 subgoal):
 1. ns ! index key y (length ns) mi ma + offs_num (length ns) (y # xs) index key mi ma (index key y (length ns) mi ma) \<le> ub
[PROOF STEP]
by (rule offs_pred_ub, simp add: offs_num_cons)
[PROOF STATE]
proof (state)
this:
ns ! index key y (length ns) mi ma + offs_num (length ns) (y # xs) index key mi ma (index key y (length ns) mi ma) \<le> ub

goal (1 subgoal):
 1. \<And>a xs ns. \<lbrakk>\<And>ns. ns \<noteq> [] \<longrightarrow> offs_pred ns ub xs index key mi ma \<longrightarrow> count (mset (map the (fill xs ns index key ub mi ma))) x = count (mset xs) x + (if the None = x then ub - length xs else 0); ns \<noteq> []; offs_pred ns ub (a # xs) index key mi ma; Suc (length xs) \<le> ub; mi \<le> key a; key a \<le> ma; \<forall>x\<in>set xs. mi \<le> key x \<and> key x \<le> ma\<rbrakk> \<Longrightarrow> count (mset ((map the (fill xs (ns[index key a (length ns) mi ma := Suc (ns ! index key a (length ns) mi ma)]) index key ub mi ma))[ns ! index key a (length ns) mi ma := a])) x = count (mset xs) x + (if a = x then 1 else 0) + (if the None = x then ub - length (a # xs) else 0)
[PROOF STEP]
hence "ns ! ?i < ub"
[PROOF STATE]
proof (prove)
using this:
ns ! index key y (length ns) mi ma + offs_num (length ns) (y # xs) index key mi ma (index key y (length ns) mi ma) \<le> ub

goal (1 subgoal):
 1. ns ! index key y (length ns) mi ma < ub
[PROOF STEP]
by (simp add: offs_num_cons)
[PROOF STATE]
proof (state)
this:
ns ! index key y (length ns) mi ma < ub

goal (1 subgoal):
 1. \<And>a xs ns. \<lbrakk>\<And>ns. ns \<noteq> [] \<longrightarrow> offs_pred ns ub xs index key mi ma \<longrightarrow> count (mset (map the (fill xs ns index key ub mi ma))) x = count (mset xs) x + (if the None = x then ub - length xs else 0); ns \<noteq> []; offs_pred ns ub (a # xs) index key mi ma; Suc (length xs) \<le> ub; mi \<le> key a; key a \<le> ma; \<forall>x\<in>set xs. mi \<le> key x \<and> key x \<le> ma\<rbrakk> \<Longrightarrow> count (mset ((map the (fill xs (ns[index key a (length ns) mi ma := Suc (ns ! index key a (length ns) mi ma)]) index key ub mi ma))[ns ! index key a (length ns) mi ma := a])) x = count (mset xs) x + (if a = x then 1 else 0) + (if the None = x then ub - length (a # xs) else 0)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
count (mset (map the (fill xs (ns[index key y (length ns) mi ma := Suc (ns ! index key y (length ns) mi ma)]) index key ub mi ma))) x = count (mset xs) x + (if the None = x then ub - length xs else 0)
ns ! index key y (length ns) mi ma < ub
[PROOF STEP]
show "count (mset ((map the (fill xs ?ns' index key ub mi ma))
    [ns ! ?i := y])) x = count (mset xs) x + (if y = x then 1 else 0) +
    (if the None = x then ub - length (y # xs) else 0)"
[PROOF STATE]
proof (prove)
using this:
count (mset (map the (fill xs (ns[index key y (length ns) mi ma := Suc (ns ! index key y (length ns) mi ma)]) index key ub mi ma))) x = count (mset xs) x + (if the None = x then ub - length xs else 0)
ns ! index key y (length ns) mi ma < ub

goal (1 subgoal):
 1. count (mset ((map the (fill xs (ns[index key y (length ns) mi ma := Suc (ns ! index key y (length ns) mi ma)]) index key ub mi ma))[ns ! index key y (length ns) mi ma := y])) x = count (mset xs) x + (if y = x then 1 else 0) + (if the None = x then ub - length (y # xs) else 0)
[PROOF STEP]
proof (subst mset_update, simp add: fill_length, subst add_mset_add_single, simp
   only: count_diff count_single count_union, subst nth_map, simp add: fill_length,
   subst add.assoc, subst (3) add.commute, subst add.assoc [symmetric],
   subst add_right_cancel)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>count (mset xs) x + (if the None = x then ub - length xs else 0) = count (mset xs) x + (if the None = x then ub - length xs else 0); True; True; True; count (mset (map the (fill xs (ns[index key y (length ns) mi ma := Suc (ns ! index key y (length ns) mi ma)]) index key ub mi ma))) x = count (mset xs) x + (if the None = x then ub - length xs else 0); ns ! index key y (length ns) mi ma < ub; count (mset (map the (fill xs (ns[index key y (length ns) mi ma := Suc (ns ! index key y (length ns) mi ma)]) index key ub mi ma))) x = count (mset xs) x + (if the None = x then ub - length xs else 0); ns ! index key y (length ns) mi ma < ub; count (mset (map the (fill xs (ns[index key y (length ns) mi ma := Suc (ns ! index key y (length ns) mi ma)]) index key ub mi ma))) x = count (mset xs) x + (if the None = x then ub - length xs else 0); ns ! index key y (length ns) mi ma < ub; count (mset (map the (fill xs (ns[index key y (length ns) mi ma := Suc (ns ! index key y (length ns) mi ma)]) index key ub mi ma))) x = count (mset xs) x + (if the None = x then ub - length xs else 0); ns ! index key y (length ns) mi ma < ub; count (mset (map the (fill xs (ns[index key y (length ns) mi ma := Suc (ns ! index key y (length ns) mi ma)]) index key ub mi ma))) x = count (mset xs) x + (if the None = x then ub - length xs else 0); ns ! index key y (length ns) mi ma < ub; count (mset (map the (fill xs (ns[index key y (length ns) mi ma := Suc (ns ! index key y (length ns) mi ma)]) index key ub mi ma))) x = count (mset xs) x + (if the None = x then ub - length xs else 0); ns ! index key y (length ns) mi ma < ub\<rbrakk> \<Longrightarrow> count (mset xs) x + (if the None = x then ub - length xs else 0) - (if the (fill xs (ns[index key y (length ns) mi ma := Suc (ns ! index key y (length ns) mi ma)]) index key ub mi ma ! (ns ! index key y (length ns) mi ma)) = x then 1 else 0) = count (mset xs) x + (if the None = x then ub - length (y # xs) else 0)
[PROOF STEP]
have "fill xs ?ns' index key ub mi ma ! (ns ! ?i) = None"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fill xs (ns[index key y (length ns) mi ma := Suc (ns ! index key y (length ns) mi ma)]) index key ub mi ma ! (ns ! index key y (length ns) mi ma) = None
[PROOF STEP]
using B and C and D and E
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>set xs. mi \<le> key x \<and> key x \<le> ma
mi \<le> key y
key y \<le> ma
ns \<noteq> []

goal (1 subgoal):
 1. fill xs (ns[index key y (length ns) mi ma := Suc (ns ! index key y (length ns) mi ma)]) index key ub mi ma ! (ns ! index key y (length ns) mi ma) = None
[PROOF STEP]
by (rule_tac fill_index_none [OF A _ _ F],
       simp_all)
[PROOF STATE]
proof (state)
this:
fill xs (ns[index key y (length ns) mi ma := Suc (ns ! index key y (length ns) mi ma)]) index key ub mi ma ! (ns ! index key y (length ns) mi ma) = None

goal (1 subgoal):
 1. \<lbrakk>count (mset xs) x + (if the None = x then ub - length xs else 0) = count (mset xs) x + (if the None = x then ub - length xs else 0); True; True; True; count (mset (map the (fill xs (ns[index key y (length ns) mi ma := Suc (ns ! index key y (length ns) mi ma)]) index key ub mi ma))) x = count (mset xs) x + (if the None = x then ub - length xs else 0); ns ! index key y (length ns) mi ma < ub; count (mset (map the (fill xs (ns[index key y (length ns) mi ma := Suc (ns ! index key y (length ns) mi ma)]) index key ub mi ma))) x = count (mset xs) x + (if the None = x then ub - length xs else 0); ns ! index key y (length ns) mi ma < ub; count (mset (map the (fill xs (ns[index key y (length ns) mi ma := Suc (ns ! index key y (length ns) mi ma)]) index key ub mi ma))) x = count (mset xs) x + (if the None = x then ub - length xs else 0); ns ! index key y (length ns) mi ma < ub; count (mset (map the (fill xs (ns[index key y (length ns) mi ma := Suc (ns ! index key y (length ns) mi ma)]) index key ub mi ma))) x = count (mset xs) x + (if the None = x then ub - length xs else 0); ns ! index key y (length ns) mi ma < ub; count (mset (map the (fill xs (ns[index key y (length ns) mi ma := Suc (ns ! index key y (length ns) mi ma)]) index key ub mi ma))) x = count (mset xs) x + (if the None = x then ub - length xs else 0); ns ! index key y (length ns) mi ma < ub; count (mset (map the (fill xs (ns[index key y (length ns) mi ma := Suc (ns ! index key y (length ns) mi ma)]) index key ub mi ma))) x = count (mset xs) x + (if the None = x then ub - length xs else 0); ns ! index key y (length ns) mi ma < ub\<rbrakk> \<Longrightarrow> count (mset xs) x + (if the None = x then ub - length xs else 0) - (if the (fill xs (ns[index key y (length ns) mi ma := Suc (ns ! index key y (length ns) mi ma)]) index key ub mi ma ! (ns ! index key y (length ns) mi ma)) = x then 1 else 0) = count (mset xs) x + (if the None = x then ub - length (y # xs) else 0)
[PROOF STEP]
thus "count (mset xs) x + (if the None = x then ub - length xs else 0) -
      (if the (fill xs ?ns' index key ub mi ma ! (ns ! ?i)) = x then 1 else 0) =
      count (mset xs) x + (if the None = x then ub - length (y # xs) else 0)"
[PROOF STATE]
proof (prove)
using this:
fill xs (ns[index key y (length ns) mi ma := Suc (ns ! index key y (length ns) mi ma)]) index key ub mi ma ! (ns ! index key y (length ns) mi ma) = None

goal (1 subgoal):
 1. count (mset xs) x + (if the None = x then ub - length xs else 0) - (if the (fill xs (ns[index key y (length ns) mi ma := Suc (ns ! index key y (length ns) mi ma)]) index key ub mi ma ! (ns ! index key y (length ns) mi ma)) = x then 1 else 0) = count (mset xs) x + (if the None = x then ub - length (y # xs) else 0)
[PROOF STEP]
using G
[PROOF STATE]
proof (prove)
using this:
fill xs (ns[index key y (length ns) mi ma := Suc (ns ! index key y (length ns) mi ma)]) index key ub mi ma ! (ns ! index key y (length ns) mi ma) = None
Suc (length xs) \<le> ub

goal (1 subgoal):
 1. count (mset xs) x + (if the None = x then ub - length xs else 0) - (if the (fill xs (ns[index key y (length ns) mi ma := Suc (ns ! index key y (length ns) mi ma)]) index key ub mi ma ! (ns ! index key y (length ns) mi ma)) = x then 1 else 0) = count (mset xs) x + (if the None = x then ub - length (y # xs) else 0)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
count (mset xs) x + (if the None = x then ub - length xs else 0) - (if the (fill xs (ns[index key y (length ns) mi ma := Suc (ns ! index key y (length ns) mi ma)]) index key ub mi ma ! (ns ! index key y (length ns) mi ma)) = x then 1 else 0) = count (mset xs) x + (if the None = x then ub - length (y # xs) else 0)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
count (mset ((map the (fill xs (ns[index key y (length ns) mi ma := Suc (ns ! index key y (length ns) mi ma)]) index key ub mi ma))[ns ! index key y (length ns) mi ma := y])) x = count (mset xs) x + (if y = x then 1 else 0) + (if the None = x then ub - length (y # xs) else 0)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma enum_offs_num:
 "i < n \<Longrightarrow> enum xs index key n mi ma ! i = offs_num n xs index key mi ma i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i < n \<Longrightarrow> enum xs index key n mi ma ! i = offs_num n xs index key mi ma i
[PROOF STEP]
by (induction xs, simp add: offs_num_def, simp add: Let_def offs_num_cons,
 subst nth_list_update_eq, simp_all add: enum_length)


[STATEMENT]
lemma offs_length:
 "length (offs ns i) = length ns"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (offs ns i) = length ns
[PROOF STEP]
by (induction ns arbitrary: i, simp_all)


[STATEMENT]
lemma offs_add [rule_format]:
 "i < length ns \<longrightarrow> offs ns k ! i = foldl (+) k (take i ns)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i < length ns \<longrightarrow> offs ns k ! i = foldl (+) k (take i ns)
[PROOF STEP]
by (induction ns arbitrary: i k, simp, simp add: nth_Cons split: nat.split)


[STATEMENT]
lemma offs_mono_aux:
 "i \<le> j \<Longrightarrow> j < length ns \<Longrightarrow> offs ns k ! i \<le> offs ns k ! (i + (j - i))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>i \<le> j; j < length ns\<rbrakk> \<Longrightarrow> offs ns k ! i \<le> offs ns k ! (i + (j - i))
[PROOF STEP]
by (simp only: offs_add take_add, simp add: add_le)


[STATEMENT]
lemma offs_mono:
 "i \<le> j \<Longrightarrow> j < length ns \<Longrightarrow> offs ns k ! i \<le> offs ns k ! j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>i \<le> j; j < length ns\<rbrakk> \<Longrightarrow> offs ns k ! i \<le> offs ns k ! j
[PROOF STEP]
by (frule offs_mono_aux, simp_all)


[STATEMENT]
lemma offs_update:
 "j < length ns \<Longrightarrow>
    offs (ns[i := Suc (ns ! i)]) k ! j = (if j \<le> i then id else Suc) (offs ns k ! j)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. j < length ns \<Longrightarrow> offs (ns[i := Suc (ns ! i)]) k ! j = (if j \<le> i then id else Suc) (offs ns k ! j)
[PROOF STEP]
by (simp add: offs_add not_le take_update_swap, rule impI, subst nth_take [symmetric],
 assumption, subst add_update, simp_all)


[STATEMENT]
lemma offs_equal_suc:
  assumes
    A: "Suc i < length ns" and
    B: "ns ! i = 0"
  shows "offs ns m ! i = offs ns m ! Suc i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. offs ns m ! i = offs ns m ! Suc i
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. offs ns m ! i = offs ns m ! Suc i
[PROOF STEP]
have "offs ns m ! i = foldl (+) m (take i ns)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. offs ns m ! i = foldl (+) m (take i ns)
[PROOF STEP]
using A
[PROOF STATE]
proof (prove)
using this:
Suc i < length ns

goal (1 subgoal):
 1. offs ns m ! i = foldl (+) m (take i ns)
[PROOF STEP]
by (subst offs_add, simp_all)
[PROOF STATE]
proof (state)
this:
offs ns m ! i = foldl (+) m (take i ns)

goal (1 subgoal):
 1. offs ns m ! i = offs ns m ! Suc i
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
offs ns m ! i = foldl (+) m (take i ns)

goal (1 subgoal):
 1. offs ns m ! i = offs ns m ! Suc i
[PROOF STEP]
have "\<dots> = foldl (+) m (take i ns @ [ns ! i])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. foldl (+) m (take i ns) = foldl (+) m (take i ns @ [ns ! i])
[PROOF STEP]
using B
[PROOF STATE]
proof (prove)
using this:
ns ! i = 0

goal (1 subgoal):
 1. foldl (+) m (take i ns) = foldl (+) m (take i ns @ [ns ! i])
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
foldl (+) m (take i ns) = foldl (+) m (take i ns @ [ns ! i])

goal (1 subgoal):
 1. offs ns m ! i = offs ns m ! Suc i
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
foldl (+) m (take i ns) = foldl (+) m (take i ns @ [ns ! i])

goal (1 subgoal):
 1. offs ns m ! i = offs ns m ! Suc i
[PROOF STEP]
have "\<dots> = foldl (+) m (take (Suc i) ns)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. foldl (+) m (take i ns @ [ns ! i]) = foldl (+) m (take (Suc i) ns)
[PROOF STEP]
using A
[PROOF STATE]
proof (prove)
using this:
Suc i < length ns

goal (1 subgoal):
 1. foldl (+) m (take i ns @ [ns ! i]) = foldl (+) m (take (Suc i) ns)
[PROOF STEP]
by (subst take_Suc_conv_app_nth, simp_all)
[PROOF STATE]
proof (state)
this:
foldl (+) m (take i ns @ [ns ! i]) = foldl (+) m (take (Suc i) ns)

goal (1 subgoal):
 1. offs ns m ! i = offs ns m ! Suc i
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
foldl (+) m (take i ns @ [ns ! i]) = foldl (+) m (take (Suc i) ns)

goal (1 subgoal):
 1. offs ns m ! i = offs ns m ! Suc i
[PROOF STEP]
have "\<dots> = offs ns m ! Suc i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. foldl (+) m (take (Suc i) ns) = offs ns m ! Suc i
[PROOF STEP]
using A
[PROOF STATE]
proof (prove)
using this:
Suc i < length ns

goal (1 subgoal):
 1. foldl (+) m (take (Suc i) ns) = offs ns m ! Suc i
[PROOF STEP]
by (subst offs_add, simp_all)
[PROOF STATE]
proof (state)
this:
foldl (+) m (take (Suc i) ns) = offs ns m ! Suc i

goal (1 subgoal):
 1. offs ns m ! i = offs ns m ! Suc i
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
offs ns m ! i = offs ns m ! Suc i
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
offs ns m ! i = offs ns m ! Suc i

goal (1 subgoal):
 1. offs ns m ! i = offs ns m ! Suc i
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
offs ns m ! i = offs ns m ! Suc i

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma offs_equal [rule_format]:
 "i < j \<Longrightarrow> j < length ns \<Longrightarrow>
    (\<forall>k \<in> {i..<j}. ns ! k = 0) \<longrightarrow> offs ns m ! i = offs ns m ! j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>i < j; j < length ns\<rbrakk> \<Longrightarrow> (\<forall>k\<in>{i..<j}. ns ! k = 0) \<longrightarrow> offs ns m ! i = offs ns m ! j
[PROOF STEP]
proof (erule strict_inc_induct, rule_tac [!] impI, simp_all, erule offs_equal_suc, simp)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i. \<lbrakk>j < length ns; i < j; offs ns m ! Suc i = offs ns m ! j; \<forall>k\<in>{i..<j}. ns ! k = 0\<rbrakk> \<Longrightarrow> offs ns m ! i = offs ns m ! j
[PROOF STEP]
fix i
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i. \<lbrakk>j < length ns; i < j; offs ns m ! Suc i = offs ns m ! j; \<forall>k\<in>{i..<j}. ns ! k = 0\<rbrakk> \<Longrightarrow> offs ns m ! i = offs ns m ! j
[PROOF STEP]
assume A: "i < j" and "j < length ns"
[PROOF STATE]
proof (state)
this:
i < j
j < length ns

goal (1 subgoal):
 1. \<And>i. \<lbrakk>j < length ns; i < j; offs ns m ! Suc i = offs ns m ! j; \<forall>k\<in>{i..<j}. ns ! k = 0\<rbrakk> \<Longrightarrow> offs ns m ! i = offs ns m ! j
[PROOF STEP]
hence "Suc i < length ns"
[PROOF STATE]
proof (prove)
using this:
i < j
j < length ns

goal (1 subgoal):
 1. Suc i < length ns
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Suc i < length ns

goal (1 subgoal):
 1. \<And>i. \<lbrakk>j < length ns; i < j; offs ns m ! Suc i = offs ns m ! j; \<forall>k\<in>{i..<j}. ns ! k = 0\<rbrakk> \<Longrightarrow> offs ns m ! i = offs ns m ! j
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
Suc i < length ns

goal (1 subgoal):
 1. \<And>i. \<lbrakk>j < length ns; i < j; offs ns m ! Suc i = offs ns m ! j; \<forall>k\<in>{i..<j}. ns ! k = 0\<rbrakk> \<Longrightarrow> offs ns m ! i = offs ns m ! j
[PROOF STEP]
assume "\<forall>k \<in> {i..<j}. ns ! k = 0"
[PROOF STATE]
proof (state)
this:
\<forall>k\<in>{i..<j}. ns ! k = 0

goal (1 subgoal):
 1. \<And>i. \<lbrakk>j < length ns; i < j; offs ns m ! Suc i = offs ns m ! j; \<forall>k\<in>{i..<j}. ns ! k = 0\<rbrakk> \<Longrightarrow> offs ns m ! i = offs ns m ! j
[PROOF STEP]
hence "ns ! i = 0"
[PROOF STATE]
proof (prove)
using this:
\<forall>k\<in>{i..<j}. ns ! k = 0

goal (1 subgoal):
 1. ns ! i = 0
[PROOF STEP]
using A
[PROOF STATE]
proof (prove)
using this:
\<forall>k\<in>{i..<j}. ns ! k = 0
i < j

goal (1 subgoal):
 1. ns ! i = 0
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
ns ! i = 0

goal (1 subgoal):
 1. \<And>i. \<lbrakk>j < length ns; i < j; offs ns m ! Suc i = offs ns m ! j; \<forall>k\<in>{i..<j}. ns ! k = 0\<rbrakk> \<Longrightarrow> offs ns m ! i = offs ns m ! j
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
Suc i < length ns
ns ! i = 0
[PROOF STEP]
have "offs ns m ! i = offs ns m ! Suc i"
[PROOF STATE]
proof (prove)
using this:
Suc i < length ns
ns ! i = 0

goal (1 subgoal):
 1. offs ns m ! i = offs ns m ! Suc i
[PROOF STEP]
by (rule offs_equal_suc)
[PROOF STATE]
proof (state)
this:
offs ns m ! i = offs ns m ! Suc i

goal (1 subgoal):
 1. \<And>i. \<lbrakk>j < length ns; i < j; offs ns m ! Suc i = offs ns m ! j; \<forall>k\<in>{i..<j}. ns ! k = 0\<rbrakk> \<Longrightarrow> offs ns m ! i = offs ns m ! j
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
offs ns m ! i = offs ns m ! Suc i

goal (1 subgoal):
 1. \<And>i. \<lbrakk>j < length ns; i < j; offs ns m ! Suc i = offs ns m ! j; \<forall>k\<in>{i..<j}. ns ! k = 0\<rbrakk> \<Longrightarrow> offs ns m ! i = offs ns m ! j
[PROOF STEP]
assume "\<dots> = offs ns m ! j"
[PROOF STATE]
proof (state)
this:
offs ns m ! Suc i = offs ns m ! j

goal (1 subgoal):
 1. \<And>i. \<lbrakk>j < length ns; i < j; offs ns m ! Suc i = offs ns m ! j; \<forall>k\<in>{i..<j}. ns ! k = 0\<rbrakk> \<Longrightarrow> offs ns m ! i = offs ns m ! j
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
offs ns m ! i = offs ns m ! j
[PROOF STEP]
show "offs ns m ! i = offs ns m ! j"
[PROOF STATE]
proof (prove)
using this:
offs ns m ! i = offs ns m ! j

goal (1 subgoal):
 1. offs ns m ! i = offs ns m ! j
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
offs ns m ! i = offs ns m ! j

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma offs_enum_last [rule_format]:
  assumes
    A: "index_less index key" and
    B: "0 < n" and
    C: "\<forall>x \<in> set xs. key x \<in> {mi..ma}"
  shows "offs (enum xs index key n mi ma) k ! (n - Suc 0) +
    offs_num n xs index key mi ma (n - Suc 0) = length xs + k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. offs (enum xs index key n mi ma) k ! (n - Suc 0) + offs_num n xs index key mi ma (n - Suc 0) = length xs + k
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. offs (enum xs index key n mi ma) k ! (n - Suc 0) + offs_num n xs index key mi ma (n - Suc 0) = length xs + k
[PROOF STEP]
let ?ns = "enum xs index key n mi ma"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. offs (enum xs index key n mi ma) k ! (n - Suc 0) + offs_num n xs index key mi ma (n - Suc 0) = length xs + k
[PROOF STEP]
from B
[PROOF STATE]
proof (chain)
picking this:
0 < n
[PROOF STEP]
have D: "last ?ns = offs_num n xs index key mi ma (n - Suc 0)"
[PROOF STATE]
proof (prove)
using this:
0 < n

goal (1 subgoal):
 1. last (enum xs index key n mi ma) = offs_num n xs index key mi ma (n - Suc 0)
[PROOF STEP]
by (subst last_conv_nth, subst length_0_conv [symmetric], simp_all add:
     enum_length, subst enum_offs_num, simp_all)
[PROOF STATE]
proof (state)
this:
last (enum xs index key n mi ma) = offs_num n xs index key mi ma (n - Suc 0)

goal (1 subgoal):
 1. offs (enum xs index key n mi ma) k ! (n - Suc 0) + offs_num n xs index key mi ma (n - Suc 0) = length xs + k
[PROOF STEP]
have "offs ?ns k ! (n - Suc 0) = foldl (+) k (take (n - Suc 0) ?ns)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. offs (enum xs index key n mi ma) k ! (n - Suc 0) = foldl (+) k (take (n - Suc 0) (enum xs index key n mi ma))
[PROOF STEP]
using B
[PROOF STATE]
proof (prove)
using this:
0 < n

goal (1 subgoal):
 1. offs (enum xs index key n mi ma) k ! (n - Suc 0) = foldl (+) k (take (n - Suc 0) (enum xs index key n mi ma))
[PROOF STEP]
by (rule_tac offs_add, simp add: enum_length)
[PROOF STATE]
proof (state)
this:
offs (enum xs index key n mi ma) k ! (n - Suc 0) = foldl (+) k (take (n - Suc 0) (enum xs index key n mi ma))

goal (1 subgoal):
 1. offs (enum xs index key n mi ma) k ! (n - Suc 0) + offs_num n xs index key mi ma (n - Suc 0) = length xs + k
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
offs (enum xs index key n mi ma) k ! (n - Suc 0) = foldl (+) k (take (n - Suc 0) (enum xs index key n mi ma))

goal (1 subgoal):
 1. offs (enum xs index key n mi ma) k ! (n - Suc 0) + offs_num n xs index key mi ma (n - Suc 0) = length xs + k
[PROOF STEP]
have "\<dots> = foldl (+) k (butlast ?ns)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. foldl (+) k (take (n - Suc 0) (enum xs index key n mi ma)) = foldl (+) k (butlast (enum xs index key n mi ma))
[PROOF STEP]
by (simp add: butlast_conv_take enum_length)
[PROOF STATE]
proof (state)
this:
foldl (+) k (take (n - Suc 0) (enum xs index key n mi ma)) = foldl (+) k (butlast (enum xs index key n mi ma))

goal (1 subgoal):
 1. offs (enum xs index key n mi ma) k ! (n - Suc 0) + offs_num n xs index key mi ma (n - Suc 0) = length xs + k
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
offs (enum xs index key n mi ma) k ! (n - Suc 0) = foldl (+) k (butlast (enum xs index key n mi ma))
[PROOF STEP]
have "offs ?ns k ! (n - Suc 0) + offs_num n xs index key mi ma
    (n - Suc 0) = foldl (+) k (butlast ?ns @ [last ?ns])"
[PROOF STATE]
proof (prove)
using this:
offs (enum xs index key n mi ma) k ! (n - Suc 0) = foldl (+) k (butlast (enum xs index key n mi ma))

goal (1 subgoal):
 1. offs (enum xs index key n mi ma) k ! (n - Suc 0) + offs_num n xs index key mi ma (n - Suc 0) = foldl (+) k (butlast (enum xs index key n mi ma) @ [last (enum xs index key n mi ma)])
[PROOF STEP]
using D
[PROOF STATE]
proof (prove)
using this:
offs (enum xs index key n mi ma) k ! (n - Suc 0) = foldl (+) k (butlast (enum xs index key n mi ma))
last (enum xs index key n mi ma) = offs_num n xs index key mi ma (n - Suc 0)

goal (1 subgoal):
 1. offs (enum xs index key n mi ma) k ! (n - Suc 0) + offs_num n xs index key mi ma (n - Suc 0) = foldl (+) k (butlast (enum xs index key n mi ma) @ [last (enum xs index key n mi ma)])
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
offs (enum xs index key n mi ma) k ! (n - Suc 0) + offs_num n xs index key mi ma (n - Suc 0) = foldl (+) k (butlast (enum xs index key n mi ma) @ [last (enum xs index key n mi ma)])

goal (1 subgoal):
 1. offs (enum xs index key n mi ma) k ! (n - Suc 0) + offs_num n xs index key mi ma (n - Suc 0) = length xs + k
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
offs (enum xs index key n mi ma) k ! (n - Suc 0) + offs_num n xs index key mi ma (n - Suc 0) = foldl (+) k (butlast (enum xs index key n mi ma) @ [last (enum xs index key n mi ma)])

goal (1 subgoal):
 1. offs (enum xs index key n mi ma) k ! (n - Suc 0) + offs_num n xs index key mi ma (n - Suc 0) = length xs + k
[PROOF STEP]
have "\<dots> = foldl (+) k ?ns"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. foldl (+) k (butlast (enum xs index key n mi ma) @ [last (enum xs index key n mi ma)]) = foldl (+) k (enum xs index key n mi ma)
[PROOF STEP]
using B
[PROOF STATE]
proof (prove)
using this:
0 < n

goal (1 subgoal):
 1. foldl (+) k (butlast (enum xs index key n mi ma) @ [last (enum xs index key n mi ma)]) = foldl (+) k (enum xs index key n mi ma)
[PROOF STEP]
by (subst append_butlast_last_id, subst length_0_conv [symmetric],
     simp_all add: enum_length)
[PROOF STATE]
proof (state)
this:
foldl (+) k (butlast (enum xs index key n mi ma) @ [last (enum xs index key n mi ma)]) = foldl (+) k (enum xs index key n mi ma)

goal (1 subgoal):
 1. offs (enum xs index key n mi ma) k ! (n - Suc 0) + offs_num n xs index key mi ma (n - Suc 0) = length xs + k
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
foldl (+) k (butlast (enum xs index key n mi ma) @ [last (enum xs index key n mi ma)]) = foldl (+) k (enum xs index key n mi ma)

goal (1 subgoal):
 1. offs (enum xs index key n mi ma) k ! (n - Suc 0) + offs_num n xs index key mi ma (n - Suc 0) = length xs + k
[PROOF STEP]
have "\<dots> = foldl (+) 0 ?ns + k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. foldl (+) k (enum xs index key n mi ma) = foldl (+) 0 (enum xs index key n mi ma) + k
[PROOF STEP]
by (rule add_base_zero)
[PROOF STATE]
proof (state)
this:
foldl (+) k (enum xs index key n mi ma) = foldl (+) 0 (enum xs index key n mi ma) + k

goal (1 subgoal):
 1. offs (enum xs index key n mi ma) k ! (n - Suc 0) + offs_num n xs index key mi ma (n - Suc 0) = length xs + k
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
foldl (+) k (enum xs index key n mi ma) = foldl (+) 0 (enum xs index key n mi ma) + k

goal (1 subgoal):
 1. offs (enum xs index key n mi ma) k ! (n - Suc 0) + offs_num n xs index key mi ma (n - Suc 0) = length xs + k
[PROOF STEP]
have "\<dots> = length xs + k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. foldl (+) 0 (enum xs index key n mi ma) + k = length xs + k
[PROOF STEP]
using A and B and C
[PROOF STATE]
proof (prove)
using this:
index_less index key
0 < n
\<forall>x\<in>set xs. key x \<in> {mi..ma}

goal (1 subgoal):
 1. foldl (+) 0 (enum xs index key n mi ma) + k = length xs + k
[PROOF STEP]
by (subst enum_add, simp_all)
[PROOF STATE]
proof (state)
this:
foldl (+) 0 (enum xs index key n mi ma) + k = length xs + k

goal (1 subgoal):
 1. offs (enum xs index key n mi ma) k ! (n - Suc 0) + offs_num n xs index key mi ma (n - Suc 0) = length xs + k
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
offs (enum xs index key n mi ma) k ! (n - Suc 0) + offs_num n xs index key mi ma (n - Suc 0) = length xs + k
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
offs (enum xs index key n mi ma) k ! (n - Suc 0) + offs_num n xs index key mi ma (n - Suc 0) = length xs + k

goal (1 subgoal):
 1. offs (enum xs index key n mi ma) k ! (n - Suc 0) + offs_num n xs index key mi ma (n - Suc 0) = length xs + k
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
offs (enum xs index key n mi ma) k ! (n - Suc 0) + offs_num n xs index key mi ma (n - Suc 0) = length xs + k

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma offs_enum_ub [rule_format]:
  assumes
    A: "index_less index key" and
    B: "i < n" and
    C: "\<forall>x \<in> set xs. key x \<in> {mi..ma}"
  shows "offs (enum xs index key n mi ma) k ! i \<le> length xs + k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. offs (enum xs index key n mi ma) k ! i \<le> length xs + k
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. offs (enum xs index key n mi ma) k ! i \<le> length xs + k
[PROOF STEP]
let ?ns = "enum xs index key n mi ma"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. offs (enum xs index key n mi ma) k ! i \<le> length xs + k
[PROOF STEP]
have "offs ?ns k ! i \<le> offs ?ns k ! (n - Suc 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. offs (enum xs index key n mi ma) k ! i \<le> offs (enum xs index key n mi ma) k ! (n - Suc 0)
[PROOF STEP]
using B
[PROOF STATE]
proof (prove)
using this:
i < n

goal (1 subgoal):
 1. offs (enum xs index key n mi ma) k ! i \<le> offs (enum xs index key n mi ma) k ! (n - Suc 0)
[PROOF STEP]
by (rule_tac offs_mono, simp_all add: enum_length)
[PROOF STATE]
proof (state)
this:
offs (enum xs index key n mi ma) k ! i \<le> offs (enum xs index key n mi ma) k ! (n - Suc 0)

goal (1 subgoal):
 1. offs (enum xs index key n mi ma) k ! i \<le> length xs + k
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
offs (enum xs index key n mi ma) k ! i \<le> offs (enum xs index key n mi ma) k ! (n - Suc 0)

goal (1 subgoal):
 1. offs (enum xs index key n mi ma) k ! i \<le> length xs + k
[PROOF STEP]
have "\<dots> \<le> offs ?ns k ! (n - Suc 0) +
    offs_num n xs index key mi ma (n - Suc 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. offs (enum xs index key n mi ma) k ! (n - Suc 0) \<le> offs (enum xs index key n mi ma) k ! (n - Suc 0) + offs_num n xs index key mi ma (n - Suc 0)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
offs (enum xs index key n mi ma) k ! (n - Suc 0) \<le> offs (enum xs index key n mi ma) k ! (n - Suc 0) + offs_num n xs index key mi ma (n - Suc 0)

goal (1 subgoal):
 1. offs (enum xs index key n mi ma) k ! i \<le> length xs + k
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
offs (enum xs index key n mi ma) k ! (n - Suc 0) \<le> offs (enum xs index key n mi ma) k ! (n - Suc 0) + offs_num n xs index key mi ma (n - Suc 0)

goal (1 subgoal):
 1. offs (enum xs index key n mi ma) k ! i \<le> length xs + k
[PROOF STEP]
have "\<dots> = length xs + k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. offs (enum xs index key n mi ma) k ! (n - Suc 0) + offs_num n xs index key mi ma (n - Suc 0) = length xs + k
[PROOF STEP]
using A and B and C
[PROOF STATE]
proof (prove)
using this:
index_less index key
i < n
\<forall>x\<in>set xs. key x \<in> {mi..ma}

goal (1 subgoal):
 1. offs (enum xs index key n mi ma) k ! (n - Suc 0) + offs_num n xs index key mi ma (n - Suc 0) = length xs + k
[PROOF STEP]
by (rule_tac offs_enum_last, simp_all)
[PROOF STATE]
proof (state)
this:
offs (enum xs index key n mi ma) k ! (n - Suc 0) + offs_num n xs index key mi ma (n - Suc 0) = length xs + k

goal (1 subgoal):
 1. offs (enum xs index key n mi ma) k ! i \<le> length xs + k
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
offs (enum xs index key n mi ma) k ! i \<le> length xs + k
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
offs (enum xs index key n mi ma) k ! i \<le> length xs + k

goal (1 subgoal):
 1. offs (enum xs index key n mi ma) k ! i \<le> length xs + k
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
offs (enum xs index key n mi ma) k ! i \<le> length xs + k

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma offs_enum_next_ge [rule_format]:
  assumes
    A: "index_less index key" and
    B: "i < n"
  shows "\<forall>x \<in> set xs. key x \<in> {mi..ma} \<Longrightarrow>
    offs (enum xs index key n mi ma) k ! i \<le>
      offs_next (offs (enum xs index key n mi ma) k) (length xs + k)
        xs index key mi ma i"
  (is "_ \<Longrightarrow> offs ?ns _ ! _ \<le> _")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>set xs. key x \<in> {mi..ma} \<Longrightarrow> offs (enum xs index key n mi ma) k ! i \<le> offs_next (offs (enum xs index key n mi ma) k) (length xs + k) xs index key mi ma i
[PROOF STEP]
proof (simp only: offs_next_def split: if_split, rule conjI, rule_tac [!] impI,
 rule offs_enum_ub [OF A B], simp)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>\<forall>x\<in>set xs. key x \<in> {mi..ma}; offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i \<noteq> {}\<rbrakk> \<Longrightarrow> offs (enum xs index key n mi ma) k ! i \<le> offs (enum xs index key n mi ma) k ! Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i)
[PROOF STEP]
assume "offs_set_next (offs ?ns k) xs index key mi ma i \<noteq> {}"
    (is "?A \<noteq> _")
[PROOF STATE]
proof (state)
this:
offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i \<noteq> {}

goal (1 subgoal):
 1. \<lbrakk>\<forall>x\<in>set xs. key x \<in> {mi..ma}; offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i \<noteq> {}\<rbrakk> \<Longrightarrow> offs (enum xs index key n mi ma) k ! i \<le> offs (enum xs index key n mi ma) k ! Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i)
[PROOF STEP]
hence C: "Min ?A \<in> ?A"
[PROOF STATE]
proof (prove)
using this:
offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i \<noteq> {}

goal (1 subgoal):
 1. Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i) \<in> offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i
[PROOF STEP]
by (rule_tac Min_in, simp)
[PROOF STATE]
proof (state)
this:
Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i) \<in> offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i

goal (1 subgoal):
 1. \<lbrakk>\<forall>x\<in>set xs. key x \<in> {mi..ma}; offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i \<noteq> {}\<rbrakk> \<Longrightarrow> offs (enum xs index key n mi ma) k ! i \<le> offs (enum xs index key n mi ma) k ! Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i)
[PROOF STEP]
hence "i \<le> Min ?A"
[PROOF STATE]
proof (prove)
using this:
Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i) \<in> offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i

goal (1 subgoal):
 1. i \<le> Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
i \<le> Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i)

goal (1 subgoal):
 1. \<lbrakk>\<forall>x\<in>set xs. key x \<in> {mi..ma}; offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i \<noteq> {}\<rbrakk> \<Longrightarrow> offs (enum xs index key n mi ma) k ! i \<le> offs (enum xs index key n mi ma) k ! Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
i \<le> Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i)

goal (1 subgoal):
 1. \<lbrakk>\<forall>x\<in>set xs. key x \<in> {mi..ma}; offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i \<noteq> {}\<rbrakk> \<Longrightarrow> offs (enum xs index key n mi ma) k ! i \<le> offs (enum xs index key n mi ma) k ! Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i)
[PROOF STEP]
have "Min ?A < length ?ns"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i) < length (enum xs index key n mi ma)
[PROOF STEP]
using C
[PROOF STATE]
proof (prove)
using this:
Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i) \<in> offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i

goal (1 subgoal):
 1. Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i) < length (enum xs index key n mi ma)
[PROOF STEP]
by (simp add: offs_length)
[PROOF STATE]
proof (state)
this:
Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i) < length (enum xs index key n mi ma)

goal (1 subgoal):
 1. \<lbrakk>\<forall>x\<in>set xs. key x \<in> {mi..ma}; offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i \<noteq> {}\<rbrakk> \<Longrightarrow> offs (enum xs index key n mi ma) k ! i \<le> offs (enum xs index key n mi ma) k ! Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
i \<le> Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i)
Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i) < length (enum xs index key n mi ma)
[PROOF STEP]
show "offs ?ns k ! i \<le> offs ?ns k ! Min ?A"
[PROOF STATE]
proof (prove)
using this:
i \<le> Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i)
Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i) < length (enum xs index key n mi ma)

goal (1 subgoal):
 1. offs (enum xs index key n mi ma) k ! i \<le> offs (enum xs index key n mi ma) k ! Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i)
[PROOF STEP]
by (rule offs_mono)
[PROOF STATE]
proof (state)
this:
offs (enum xs index key n mi ma) k ! i \<le> offs (enum xs index key n mi ma) k ! Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma offs_enum_zero_aux [rule_format]:
 "\<lbrakk>index_less index key; 0 < n; \<forall>x \<in> set xs. key x \<in> {mi..ma};
   offs_num n xs index key mi ma (n - Suc 0) = 0\<rbrakk> \<Longrightarrow>
     offs (enum xs index key n mi ma) k ! (n - Suc 0) = length xs + k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>index_less index key; 0 < n; \<forall>x\<in>set xs. key x \<in> {mi..ma}; offs_num n xs index key mi ma (n - Suc 0) = 0\<rbrakk> \<Longrightarrow> offs (enum xs index key n mi ma) k ! (n - Suc 0) = length xs + k
[PROOF STEP]
by (subst offs_enum_last [where key = key and mi = mi and ma = ma,
 symmetric], simp+)


[STATEMENT]
lemma offs_enum_zero [rule_format]:
  assumes
    A: "index_less index key" and
    B: "i < n" and
    C: "\<forall>x \<in> set xs. key x \<in> {mi..ma}" and
    D: "offs_num n xs index key mi ma i = 0"
  shows "offs (enum xs index key n mi ma) k ! i =
    offs_next (offs (enum xs index key n mi ma) k) (length xs + k)
      xs index key mi ma i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. offs (enum xs index key n mi ma) k ! i = offs_next (offs (enum xs index key n mi ma) k) (length xs + k) xs index key mi ma i
[PROOF STEP]
proof (simp only: offs_next_def split: if_split, rule conjI, rule_tac [!] impI,
 cases "i = n - Suc 0", simp)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<lbrakk>\<forall>x>n - Suc 0. x < length (offs (enum xs index key n mi ma) k) \<longrightarrow> offs_num (length (offs (enum xs index key n mi ma) k)) xs index key mi ma x = 0; i = n - Suc 0\<rbrakk> \<Longrightarrow> offs (enum xs index key n mi ma) k ! (n - Suc 0) = length xs + k
 2. \<lbrakk>offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i = {}; i \<noteq> n - Suc 0\<rbrakk> \<Longrightarrow> offs (enum xs index key n mi ma) k ! i = length xs + k
 3. offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i \<noteq> {} \<Longrightarrow> offs (enum xs index key n mi ma) k ! i = offs (enum xs index key n mi ma) k ! Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i)
[PROOF STEP]
assume "i = n - Suc 0"
[PROOF STATE]
proof (state)
this:
i = n - Suc 0

goal (3 subgoals):
 1. \<lbrakk>\<forall>x>n - Suc 0. x < length (offs (enum xs index key n mi ma) k) \<longrightarrow> offs_num (length (offs (enum xs index key n mi ma) k)) xs index key mi ma x = 0; i = n - Suc 0\<rbrakk> \<Longrightarrow> offs (enum xs index key n mi ma) k ! (n - Suc 0) = length xs + k
 2. \<lbrakk>offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i = {}; i \<noteq> n - Suc 0\<rbrakk> \<Longrightarrow> offs (enum xs index key n mi ma) k ! i = length xs + k
 3. offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i \<noteq> {} \<Longrightarrow> offs (enum xs index key n mi ma) k ! i = offs (enum xs index key n mi ma) k ! Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i)
[PROOF STEP]
thus "offs (enum xs index key n mi ma) k ! (n - Suc 0) = length xs + k"
[PROOF STATE]
proof (prove)
using this:
i = n - Suc 0

goal (1 subgoal):
 1. offs (enum xs index key n mi ma) k ! (n - Suc 0) = length xs + k
[PROOF STEP]
using A and B and C and D
[PROOF STATE]
proof (prove)
using this:
i = n - Suc 0
index_less index key
i < n
\<forall>x\<in>set xs. key x \<in> {mi..ma}
offs_num n xs index key mi ma i = 0

goal (1 subgoal):
 1. offs (enum xs index key n mi ma) k ! (n - Suc 0) = length xs + k
[PROOF STEP]
by (rule_tac offs_enum_zero_aux, simp_all)
[PROOF STATE]
proof (state)
this:
offs (enum xs index key n mi ma) k ! (n - Suc 0) = length xs + k

goal (2 subgoals):
 1. \<lbrakk>offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i = {}; i \<noteq> n - Suc 0\<rbrakk> \<Longrightarrow> offs (enum xs index key n mi ma) k ! i = length xs + k
 2. offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i \<noteq> {} \<Longrightarrow> offs (enum xs index key n mi ma) k ! i = offs (enum xs index key n mi ma) k ! Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i = {}; i \<noteq> n - Suc 0\<rbrakk> \<Longrightarrow> offs (enum xs index key n mi ma) k ! i = length xs + k
 2. offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i \<noteq> {} \<Longrightarrow> offs (enum xs index key n mi ma) k ! i = offs (enum xs index key n mi ma) k ! Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i)
[PROOF STEP]
let ?ns = "enum xs index key n mi ma"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i = {}; i \<noteq> n - Suc 0\<rbrakk> \<Longrightarrow> offs (enum xs index key n mi ma) k ! i = length xs + k
 2. offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i \<noteq> {} \<Longrightarrow> offs (enum xs index key n mi ma) k ! i = offs (enum xs index key n mi ma) k ! Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i)
[PROOF STEP]
assume E: "offs_set_next (offs ?ns k) xs index key mi ma i = {}"
    (is "?A = _")
[PROOF STATE]
proof (state)
this:
offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i = {}

goal (2 subgoals):
 1. \<lbrakk>offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i = {}; i \<noteq> n - Suc 0\<rbrakk> \<Longrightarrow> offs (enum xs index key n mi ma) k ! i = length xs + k
 2. offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i \<noteq> {} \<Longrightarrow> offs (enum xs index key n mi ma) k ! i = offs (enum xs index key n mi ma) k ! Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i)
[PROOF STEP]
assume "i \<noteq> n - Suc 0"
[PROOF STATE]
proof (state)
this:
i \<noteq> n - Suc 0

goal (2 subgoals):
 1. \<lbrakk>offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i = {}; i \<noteq> n - Suc 0\<rbrakk> \<Longrightarrow> offs (enum xs index key n mi ma) k ! i = length xs + k
 2. offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i \<noteq> {} \<Longrightarrow> offs (enum xs index key n mi ma) k ! i = offs (enum xs index key n mi ma) k ! Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i)
[PROOF STEP]
hence F: "i < n - Suc 0"
[PROOF STATE]
proof (prove)
using this:
i \<noteq> n - Suc 0

goal (1 subgoal):
 1. i < n - Suc 0
[PROOF STEP]
using B
[PROOF STATE]
proof (prove)
using this:
i \<noteq> n - Suc 0
i < n

goal (1 subgoal):
 1. i < n - Suc 0
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
i < n - Suc 0

goal (2 subgoals):
 1. \<lbrakk>offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i = {}; i \<noteq> n - Suc 0\<rbrakk> \<Longrightarrow> offs (enum xs index key n mi ma) k ! i = length xs + k
 2. offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i \<noteq> {} \<Longrightarrow> offs (enum xs index key n mi ma) k ! i = offs (enum xs index key n mi ma) k ! Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i)
[PROOF STEP]
hence "offs ?ns k ! i = offs ?ns k ! (n - Suc 0)"
[PROOF STATE]
proof (prove)
using this:
i < n - Suc 0

goal (1 subgoal):
 1. offs (enum xs index key n mi ma) k ! i = offs (enum xs index key n mi ma) k ! (n - Suc 0)
[PROOF STEP]
proof (rule offs_equal, simp_all add: enum_length le_less,
   erule_tac conjE, erule_tac disjE, rule_tac ccontr, drule_tac [2] sym, simp_all)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>k. \<lbrakk>k < n - Suc 0; i < k; 0 < enum xs index key n mi ma ! k\<rbrakk> \<Longrightarrow> False
 2. i < n - Suc 0 \<Longrightarrow> enum xs index key n mi ma ! i = 0
[PROOF STEP]
fix j
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>k. \<lbrakk>k < n - Suc 0; i < k; 0 < enum xs index key n mi ma ! k\<rbrakk> \<Longrightarrow> False
 2. i < n - Suc 0 \<Longrightarrow> enum xs index key n mi ma ! i = 0
[PROOF STEP]
assume G: "j < n - Suc 0"
[PROOF STATE]
proof (state)
this:
j < n - Suc 0

goal (2 subgoals):
 1. \<And>k. \<lbrakk>k < n - Suc 0; i < k; 0 < enum xs index key n mi ma ! k\<rbrakk> \<Longrightarrow> False
 2. i < n - Suc 0 \<Longrightarrow> enum xs index key n mi ma ! i = 0
[PROOF STEP]
hence "j < length (offs ?ns k)"
[PROOF STATE]
proof (prove)
using this:
j < n - Suc 0

goal (1 subgoal):
 1. j < length (offs (enum xs index key n mi ma) k)
[PROOF STEP]
by (simp add: offs_length enum_length)
[PROOF STATE]
proof (state)
this:
j < length (offs (enum xs index key n mi ma) k)

goal (2 subgoals):
 1. \<And>k. \<lbrakk>k < n - Suc 0; i < k; 0 < enum xs index key n mi ma ! k\<rbrakk> \<Longrightarrow> False
 2. i < n - Suc 0 \<Longrightarrow> enum xs index key n mi ma ! i = 0
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
j < length (offs (enum xs index key n mi ma) k)

goal (2 subgoals):
 1. \<And>k. \<lbrakk>k < n - Suc 0; i < k; 0 < enum xs index key n mi ma ! k\<rbrakk> \<Longrightarrow> False
 2. i < n - Suc 0 \<Longrightarrow> enum xs index key n mi ma ! i = 0
[PROOF STEP]
assume "i < j"
[PROOF STATE]
proof (state)
this:
i < j

goal (2 subgoals):
 1. \<And>k. \<lbrakk>k < n - Suc 0; i < k; 0 < enum xs index key n mi ma ! k\<rbrakk> \<Longrightarrow> False
 2. i < n - Suc 0 \<Longrightarrow> enum xs index key n mi ma ! i = 0
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
i < j

goal (2 subgoals):
 1. \<And>k. \<lbrakk>k < n - Suc 0; i < k; 0 < enum xs index key n mi ma ! k\<rbrakk> \<Longrightarrow> False
 2. i < n - Suc 0 \<Longrightarrow> enum xs index key n mi ma ! i = 0
[PROOF STEP]
assume "0 < ?ns ! j"
[PROOF STATE]
proof (state)
this:
0 < enum xs index key n mi ma ! j

goal (2 subgoals):
 1. \<And>k. \<lbrakk>k < n - Suc 0; i < k; 0 < enum xs index key n mi ma ! k\<rbrakk> \<Longrightarrow> False
 2. i < n - Suc 0 \<Longrightarrow> enum xs index key n mi ma ! i = 0
[PROOF STEP]
hence "0 < offs_num (length (offs ?ns k)) xs index key mi ma j"
[PROOF STATE]
proof (prove)
using this:
0 < enum xs index key n mi ma ! j

goal (1 subgoal):
 1. 0 < offs_num (length (offs (enum xs index key n mi ma) k)) xs index key mi ma j
[PROOF STEP]
using G
[PROOF STATE]
proof (prove)
using this:
0 < enum xs index key n mi ma ! j
j < n - Suc 0

goal (1 subgoal):
 1. 0 < offs_num (length (offs (enum xs index key n mi ma) k)) xs index key mi ma j
[PROOF STEP]
by (subst (asm) enum_offs_num, simp_all add:
       offs_length enum_length)
[PROOF STATE]
proof (state)
this:
0 < offs_num (length (offs (enum xs index key n mi ma) k)) xs index key mi ma j

goal (2 subgoals):
 1. \<And>k. \<lbrakk>k < n - Suc 0; i < k; 0 < enum xs index key n mi ma ! k\<rbrakk> \<Longrightarrow> False
 2. i < n - Suc 0 \<Longrightarrow> enum xs index key n mi ma ! i = 0
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
j < length (offs (enum xs index key n mi ma) k)
i < j
0 < offs_num (length (offs (enum xs index key n mi ma) k)) xs index key mi ma j
[PROOF STEP]
have "j \<in> ?A"
[PROOF STATE]
proof (prove)
using this:
j < length (offs (enum xs index key n mi ma) k)
i < j
0 < offs_num (length (offs (enum xs index key n mi ma) k)) xs index key mi ma j

goal (1 subgoal):
 1. j \<in> offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
j \<in> offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i

goal (2 subgoals):
 1. \<And>k. \<lbrakk>k < n - Suc 0; i < k; 0 < enum xs index key n mi ma ! k\<rbrakk> \<Longrightarrow> False
 2. i < n - Suc 0 \<Longrightarrow> enum xs index key n mi ma ! i = 0
[PROOF STEP]
thus False
[PROOF STATE]
proof (prove)
using this:
j \<in> offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i

goal (1 subgoal):
 1. False
[PROOF STEP]
using E
[PROOF STATE]
proof (prove)
using this:
j \<in> offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i
offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i = {}

goal (1 subgoal):
 1. False
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
False

goal (1 subgoal):
 1. i < n - Suc 0 \<Longrightarrow> enum xs index key n mi ma ! i = 0
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. i < n - Suc 0 \<Longrightarrow> enum xs index key n mi ma ! i = 0
[PROOF STEP]
show "?ns ! i = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. enum xs index key n mi ma ! i = 0
[PROOF STEP]
using B and D
[PROOF STATE]
proof (prove)
using this:
i < n
offs_num n xs index key mi ma i = 0

goal (1 subgoal):
 1. enum xs index key n mi ma ! i = 0
[PROOF STEP]
by (subst enum_offs_num, simp_all)
[PROOF STATE]
proof (state)
this:
enum xs index key n mi ma ! i = 0

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
offs (enum xs index key n mi ma) k ! i = offs (enum xs index key n mi ma) k ! (n - Suc 0)

goal (2 subgoals):
 1. \<lbrakk>offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i = {}; i \<noteq> n - Suc 0\<rbrakk> \<Longrightarrow> offs (enum xs index key n mi ma) k ! i = length xs + k
 2. offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i \<noteq> {} \<Longrightarrow> offs (enum xs index key n mi ma) k ! i = offs (enum xs index key n mi ma) k ! Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
offs (enum xs index key n mi ma) k ! i = offs (enum xs index key n mi ma) k ! (n - Suc 0)

goal (2 subgoals):
 1. \<lbrakk>offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i = {}; i \<noteq> n - Suc 0\<rbrakk> \<Longrightarrow> offs (enum xs index key n mi ma) k ! i = length xs + k
 2. offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i \<noteq> {} \<Longrightarrow> offs (enum xs index key n mi ma) k ! i = offs (enum xs index key n mi ma) k ! Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i)
[PROOF STEP]
from A and B and C
[PROOF STATE]
proof (chain)
picking this:
index_less index key
i < n
\<forall>x\<in>set xs. key x \<in> {mi..ma}
[PROOF STEP]
have "\<dots> = length xs + k"
[PROOF STATE]
proof (prove)
using this:
index_less index key
i < n
\<forall>x\<in>set xs. key x \<in> {mi..ma}

goal (1 subgoal):
 1. offs (enum xs index key n mi ma) k ! (n - Suc 0) = length xs + k
[PROOF STEP]
proof (rule_tac offs_enum_zero_aux, simp_all, rule_tac ccontr, simp)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>\<forall>x\<in>set xs. mi \<le> key x \<and> key x \<le> ma; 0 < offs_num n xs index key mi ma (n - Suc 0); index_less index key; i < n\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
have "n - Suc 0 < length (offs ?ns k)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n - Suc 0 < length (offs (enum xs index key n mi ma) k)
[PROOF STEP]
using B
[PROOF STATE]
proof (prove)
using this:
i < n

goal (1 subgoal):
 1. n - Suc 0 < length (offs (enum xs index key n mi ma) k)
[PROOF STEP]
by (simp add: offs_length enum_length)
[PROOF STATE]
proof (state)
this:
n - Suc 0 < length (offs (enum xs index key n mi ma) k)

goal (1 subgoal):
 1. \<lbrakk>\<forall>x\<in>set xs. mi \<le> key x \<and> key x \<le> ma; 0 < offs_num n xs index key mi ma (n - Suc 0); index_less index key; i < n\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
n - Suc 0 < length (offs (enum xs index key n mi ma) k)

goal (1 subgoal):
 1. \<lbrakk>\<forall>x\<in>set xs. mi \<le> key x \<and> key x \<le> ma; 0 < offs_num n xs index key mi ma (n - Suc 0); index_less index key; i < n\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
assume "0 < offs_num n xs index key mi ma (n - Suc 0)"
[PROOF STATE]
proof (state)
this:
0 < offs_num n xs index key mi ma (n - Suc 0)

goal (1 subgoal):
 1. \<lbrakk>\<forall>x\<in>set xs. mi \<le> key x \<and> key x \<le> ma; 0 < offs_num n xs index key mi ma (n - Suc 0); index_less index key; i < n\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
hence "0 < offs_num (length (offs ?ns k)) xs index key mi ma (n - Suc 0)"
[PROOF STATE]
proof (prove)
using this:
0 < offs_num n xs index key mi ma (n - Suc 0)

goal (1 subgoal):
 1. 0 < offs_num (length (offs (enum xs index key n mi ma) k)) xs index key mi ma (n - Suc 0)
[PROOF STEP]
by (simp add: offs_length enum_length)
[PROOF STATE]
proof (state)
this:
0 < offs_num (length (offs (enum xs index key n mi ma) k)) xs index key mi ma (n - Suc 0)

goal (1 subgoal):
 1. \<lbrakk>\<forall>x\<in>set xs. mi \<le> key x \<and> key x \<le> ma; 0 < offs_num n xs index key mi ma (n - Suc 0); index_less index key; i < n\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
n - Suc 0 < length (offs (enum xs index key n mi ma) k)
0 < offs_num (length (offs (enum xs index key n mi ma) k)) xs index key mi ma (n - Suc 0)
[PROOF STEP]
have "n - Suc 0 \<in> ?A"
[PROOF STATE]
proof (prove)
using this:
n - Suc 0 < length (offs (enum xs index key n mi ma) k)
0 < offs_num (length (offs (enum xs index key n mi ma) k)) xs index key mi ma (n - Suc 0)

goal (1 subgoal):
 1. n - Suc 0 \<in> offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i
[PROOF STEP]
using F
[PROOF STATE]
proof (prove)
using this:
n - Suc 0 < length (offs (enum xs index key n mi ma) k)
0 < offs_num (length (offs (enum xs index key n mi ma) k)) xs index key mi ma (n - Suc 0)
i < n - Suc 0

goal (1 subgoal):
 1. n - Suc 0 \<in> offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
n - Suc 0 \<in> offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i

goal (1 subgoal):
 1. \<lbrakk>\<forall>x\<in>set xs. mi \<le> key x \<and> key x \<le> ma; 0 < offs_num n xs index key mi ma (n - Suc 0); index_less index key; i < n\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
thus False
[PROOF STATE]
proof (prove)
using this:
n - Suc 0 \<in> offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i

goal (1 subgoal):
 1. False
[PROOF STEP]
using E
[PROOF STATE]
proof (prove)
using this:
n - Suc 0 \<in> offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i
offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i = {}

goal (1 subgoal):
 1. False
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
False

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
offs (enum xs index key n mi ma) k ! (n - Suc 0) = length xs + k

goal (2 subgoals):
 1. \<lbrakk>offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i = {}; i \<noteq> n - Suc 0\<rbrakk> \<Longrightarrow> offs (enum xs index key n mi ma) k ! i = length xs + k
 2. offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i \<noteq> {} \<Longrightarrow> offs (enum xs index key n mi ma) k ! i = offs (enum xs index key n mi ma) k ! Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
offs (enum xs index key n mi ma) k ! i = length xs + k
[PROOF STEP]
show "offs (enum xs index key n mi ma) k ! i = length xs + k"
[PROOF STATE]
proof (prove)
using this:
offs (enum xs index key n mi ma) k ! i = length xs + k

goal (1 subgoal):
 1. offs (enum xs index key n mi ma) k ! i = length xs + k
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
offs (enum xs index key n mi ma) k ! i = length xs + k

goal (1 subgoal):
 1. offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i \<noteq> {} \<Longrightarrow> offs (enum xs index key n mi ma) k ! i = offs (enum xs index key n mi ma) k ! Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i \<noteq> {} \<Longrightarrow> offs (enum xs index key n mi ma) k ! i = offs (enum xs index key n mi ma) k ! Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i)
[PROOF STEP]
let ?ns = "enum xs index key n mi ma"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i \<noteq> {} \<Longrightarrow> offs (enum xs index key n mi ma) k ! i = offs (enum xs index key n mi ma) k ! Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i)
[PROOF STEP]
assume "offs_set_next (offs ?ns k) xs index key mi ma i \<noteq> {}"
    (is "?A \<noteq> _")
[PROOF STATE]
proof (state)
this:
offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i \<noteq> {}

goal (1 subgoal):
 1. offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i \<noteq> {} \<Longrightarrow> offs (enum xs index key n mi ma) k ! i = offs (enum xs index key n mi ma) k ! Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i)
[PROOF STEP]
hence "Min ?A \<in> ?A"
[PROOF STATE]
proof (prove)
using this:
offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i \<noteq> {}

goal (1 subgoal):
 1. Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i) \<in> offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i
[PROOF STEP]
by (rule_tac Min_in, simp)
[PROOF STATE]
proof (state)
this:
Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i) \<in> offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i

goal (1 subgoal):
 1. offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i \<noteq> {} \<Longrightarrow> offs (enum xs index key n mi ma) k ! i = offs (enum xs index key n mi ma) k ! Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i)
[PROOF STEP]
thus "offs ?ns k ! i = offs ?ns k ! Min ?A"
[PROOF STATE]
proof (prove)
using this:
Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i) \<in> offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i

goal (1 subgoal):
 1. offs (enum xs index key n mi ma) k ! i = offs (enum xs index key n mi ma) k ! Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i)
[PROOF STEP]
proof (rule_tac offs_equal, simp_all add: le_less, simp add: offs_length,
   (erule_tac conjE)+, erule_tac disjE, rule_tac ccontr, drule_tac [2] sym, simp_all)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>ka. \<lbrakk>Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i) < length (offs (enum xs index key n mi ma) k); ka < Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i); 0 < offs_num (length (offs (enum xs index key n mi ma) k)) xs index key mi ma (Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i)); i < ka; 0 < enum xs index key n mi ma ! ka\<rbrakk> \<Longrightarrow> False
 2. \<And>ka. \<lbrakk>Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i) < length (offs (enum xs index key n mi ma) k); i < Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i); 0 < offs_num (length (offs (enum xs index key n mi ma) k)) xs index key mi ma (Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i)); ka = i\<rbrakk> \<Longrightarrow> enum xs index key n mi ma ! i = 0
[PROOF STEP]
fix j
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>ka. \<lbrakk>Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i) < length (offs (enum xs index key n mi ma) k); ka < Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i); 0 < offs_num (length (offs (enum xs index key n mi ma) k)) xs index key mi ma (Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i)); i < ka; 0 < enum xs index key n mi ma ! ka\<rbrakk> \<Longrightarrow> False
 2. \<And>ka. \<lbrakk>Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i) < length (offs (enum xs index key n mi ma) k); i < Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i); 0 < offs_num (length (offs (enum xs index key n mi ma) k)) xs index key mi ma (Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i)); ka = i\<rbrakk> \<Longrightarrow> enum xs index key n mi ma ! i = 0
[PROOF STEP]
assume E: "j < Min ?A" and "Min ?A < length (offs ?ns k)"
[PROOF STATE]
proof (state)
this:
j < Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i)
Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i) < length (offs (enum xs index key n mi ma) k)

goal (2 subgoals):
 1. \<And>ka. \<lbrakk>Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i) < length (offs (enum xs index key n mi ma) k); ka < Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i); 0 < offs_num (length (offs (enum xs index key n mi ma) k)) xs index key mi ma (Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i)); i < ka; 0 < enum xs index key n mi ma ! ka\<rbrakk> \<Longrightarrow> False
 2. \<And>ka. \<lbrakk>Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i) < length (offs (enum xs index key n mi ma) k); i < Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i); 0 < offs_num (length (offs (enum xs index key n mi ma) k)) xs index key mi ma (Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i)); ka = i\<rbrakk> \<Longrightarrow> enum xs index key n mi ma ! i = 0
[PROOF STEP]
hence F: "j < length (offs ?ns k)"
[PROOF STATE]
proof (prove)
using this:
j < Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i)
Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i) < length (offs (enum xs index key n mi ma) k)

goal (1 subgoal):
 1. j < length (offs (enum xs index key n mi ma) k)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
j < length (offs (enum xs index key n mi ma) k)

goal (2 subgoals):
 1. \<And>ka. \<lbrakk>Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i) < length (offs (enum xs index key n mi ma) k); ka < Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i); 0 < offs_num (length (offs (enum xs index key n mi ma) k)) xs index key mi ma (Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i)); i < ka; 0 < enum xs index key n mi ma ! ka\<rbrakk> \<Longrightarrow> False
 2. \<And>ka. \<lbrakk>Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i) < length (offs (enum xs index key n mi ma) k); i < Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i); 0 < offs_num (length (offs (enum xs index key n mi ma) k)) xs index key mi ma (Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i)); ka = i\<rbrakk> \<Longrightarrow> enum xs index key n mi ma ! i = 0
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
j < length (offs (enum xs index key n mi ma) k)

goal (2 subgoals):
 1. \<And>ka. \<lbrakk>Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i) < length (offs (enum xs index key n mi ma) k); ka < Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i); 0 < offs_num (length (offs (enum xs index key n mi ma) k)) xs index key mi ma (Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i)); i < ka; 0 < enum xs index key n mi ma ! ka\<rbrakk> \<Longrightarrow> False
 2. \<And>ka. \<lbrakk>Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i) < length (offs (enum xs index key n mi ma) k); i < Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i); 0 < offs_num (length (offs (enum xs index key n mi ma) k)) xs index key mi ma (Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i)); ka = i\<rbrakk> \<Longrightarrow> enum xs index key n mi ma ! i = 0
[PROOF STEP]
assume "i < j"
[PROOF STATE]
proof (state)
this:
i < j

goal (2 subgoals):
 1. \<And>ka. \<lbrakk>Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i) < length (offs (enum xs index key n mi ma) k); ka < Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i); 0 < offs_num (length (offs (enum xs index key n mi ma) k)) xs index key mi ma (Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i)); i < ka; 0 < enum xs index key n mi ma ! ka\<rbrakk> \<Longrightarrow> False
 2. \<And>ka. \<lbrakk>Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i) < length (offs (enum xs index key n mi ma) k); i < Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i); 0 < offs_num (length (offs (enum xs index key n mi ma) k)) xs index key mi ma (Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i)); ka = i\<rbrakk> \<Longrightarrow> enum xs index key n mi ma ! i = 0
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
i < j

goal (2 subgoals):
 1. \<And>ka. \<lbrakk>Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i) < length (offs (enum xs index key n mi ma) k); ka < Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i); 0 < offs_num (length (offs (enum xs index key n mi ma) k)) xs index key mi ma (Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i)); i < ka; 0 < enum xs index key n mi ma ! ka\<rbrakk> \<Longrightarrow> False
 2. \<And>ka. \<lbrakk>Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i) < length (offs (enum xs index key n mi ma) k); i < Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i); 0 < offs_num (length (offs (enum xs index key n mi ma) k)) xs index key mi ma (Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i)); ka = i\<rbrakk> \<Longrightarrow> enum xs index key n mi ma ! i = 0
[PROOF STEP]
assume "0 < ?ns ! j"
[PROOF STATE]
proof (state)
this:
0 < enum xs index key n mi ma ! j

goal (2 subgoals):
 1. \<And>ka. \<lbrakk>Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i) < length (offs (enum xs index key n mi ma) k); ka < Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i); 0 < offs_num (length (offs (enum xs index key n mi ma) k)) xs index key mi ma (Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i)); i < ka; 0 < enum xs index key n mi ma ! ka\<rbrakk> \<Longrightarrow> False
 2. \<And>ka. \<lbrakk>Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i) < length (offs (enum xs index key n mi ma) k); i < Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i); 0 < offs_num (length (offs (enum xs index key n mi ma) k)) xs index key mi ma (Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i)); ka = i\<rbrakk> \<Longrightarrow> enum xs index key n mi ma ! i = 0
[PROOF STEP]
hence "0 < offs_num (length (offs ?ns k)) xs index key mi ma j"
[PROOF STATE]
proof (prove)
using this:
0 < enum xs index key n mi ma ! j

goal (1 subgoal):
 1. 0 < offs_num (length (offs (enum xs index key n mi ma) k)) xs index key mi ma j
[PROOF STEP]
using F
[PROOF STATE]
proof (prove)
using this:
0 < enum xs index key n mi ma ! j
j < length (offs (enum xs index key n mi ma) k)

goal (1 subgoal):
 1. 0 < offs_num (length (offs (enum xs index key n mi ma) k)) xs index key mi ma j
[PROOF STEP]
by (subst (asm) enum_offs_num, simp_all add:
       offs_length enum_length)
[PROOF STATE]
proof (state)
this:
0 < offs_num (length (offs (enum xs index key n mi ma) k)) xs index key mi ma j

goal (2 subgoals):
 1. \<And>ka. \<lbrakk>Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i) < length (offs (enum xs index key n mi ma) k); ka < Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i); 0 < offs_num (length (offs (enum xs index key n mi ma) k)) xs index key mi ma (Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i)); i < ka; 0 < enum xs index key n mi ma ! ka\<rbrakk> \<Longrightarrow> False
 2. \<And>ka. \<lbrakk>Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i) < length (offs (enum xs index key n mi ma) k); i < Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i); 0 < offs_num (length (offs (enum xs index key n mi ma) k)) xs index key mi ma (Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i)); ka = i\<rbrakk> \<Longrightarrow> enum xs index key n mi ma ! i = 0
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
j < length (offs (enum xs index key n mi ma) k)
i < j
0 < offs_num (length (offs (enum xs index key n mi ma) k)) xs index key mi ma j
[PROOF STEP]
have "j \<in> ?A"
[PROOF STATE]
proof (prove)
using this:
j < length (offs (enum xs index key n mi ma) k)
i < j
0 < offs_num (length (offs (enum xs index key n mi ma) k)) xs index key mi ma j

goal (1 subgoal):
 1. j \<in> offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
j \<in> offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i

goal (2 subgoals):
 1. \<And>ka. \<lbrakk>Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i) < length (offs (enum xs index key n mi ma) k); ka < Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i); 0 < offs_num (length (offs (enum xs index key n mi ma) k)) xs index key mi ma (Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i)); i < ka; 0 < enum xs index key n mi ma ! ka\<rbrakk> \<Longrightarrow> False
 2. \<And>ka. \<lbrakk>Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i) < length (offs (enum xs index key n mi ma) k); i < Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i); 0 < offs_num (length (offs (enum xs index key n mi ma) k)) xs index key mi ma (Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i)); ka = i\<rbrakk> \<Longrightarrow> enum xs index key n mi ma ! i = 0
[PROOF STEP]
hence "Min ?A \<le> j"
[PROOF STATE]
proof (prove)
using this:
j \<in> offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i

goal (1 subgoal):
 1. Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i) \<le> j
[PROOF STEP]
by (rule_tac Min_le, simp)
[PROOF STATE]
proof (state)
this:
Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i) \<le> j

goal (2 subgoals):
 1. \<And>ka. \<lbrakk>Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i) < length (offs (enum xs index key n mi ma) k); ka < Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i); 0 < offs_num (length (offs (enum xs index key n mi ma) k)) xs index key mi ma (Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i)); i < ka; 0 < enum xs index key n mi ma ! ka\<rbrakk> \<Longrightarrow> False
 2. \<And>ka. \<lbrakk>Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i) < length (offs (enum xs index key n mi ma) k); i < Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i); 0 < offs_num (length (offs (enum xs index key n mi ma) k)) xs index key mi ma (Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i)); ka = i\<rbrakk> \<Longrightarrow> enum xs index key n mi ma ! i = 0
[PROOF STEP]
thus False
[PROOF STATE]
proof (prove)
using this:
Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i) \<le> j

goal (1 subgoal):
 1. False
[PROOF STEP]
using E
[PROOF STATE]
proof (prove)
using this:
Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i) \<le> j
j < Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i)

goal (1 subgoal):
 1. False
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
False

goal (1 subgoal):
 1. \<And>ka. \<lbrakk>Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i) < length (offs (enum xs index key n mi ma) k); i < Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i); 0 < offs_num (length (offs (enum xs index key n mi ma) k)) xs index key mi ma (Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i)); ka = i\<rbrakk> \<Longrightarrow> enum xs index key n mi ma ! i = 0
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>ka. \<lbrakk>Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i) < length (offs (enum xs index key n mi ma) k); i < Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i); 0 < offs_num (length (offs (enum xs index key n mi ma) k)) xs index key mi ma (Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i)); ka = i\<rbrakk> \<Longrightarrow> enum xs index key n mi ma ! i = 0
[PROOF STEP]
show "?ns ! i = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. enum xs index key n mi ma ! i = 0
[PROOF STEP]
using B and D
[PROOF STATE]
proof (prove)
using this:
i < n
offs_num n xs index key mi ma i = 0

goal (1 subgoal):
 1. enum xs index key n mi ma ! i = 0
[PROOF STEP]
by (subst enum_offs_num, simp_all)
[PROOF STATE]
proof (state)
this:
enum xs index key n mi ma ! i = 0

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
offs (enum xs index key n mi ma) k ! i = offs (enum xs index key n mi ma) k ! Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i)

goal:
No subgoals!
[PROOF STEP]
qed